NatArith (nholz)

NatArith Module

Namespace: HOL
Assembly: nholz.dll

This module defines some classic natural number arithmetic operators, using recursive function definition and the "SUC" and "ZERO" constants, and proves various basic properties about each operator.

Functions and values

Function or value	Description
`add_assoc_thm` Full Usage: `add_assoc_thm` Returns: `thm`	\|- !l m n. l + (m + n) = (l + m) + n Returns: `thm`
`add_comm_thm` Full Usage: `add_comm_thm` Returns: `thm`	Returns: `thm`
`add_def` Full Usage: `add_def` Returns: `thm`	\|- (!n. 0 + n = n) /\ (!m n. SUC m + n = SUC (m + n)) Returns: `thm`
`add_dist_left_suc_thm` Full Usage: `add_dist_left_suc_thm` Returns: `thm`	Returns: `thm`
`add_dist_right_suc_thm` Full Usage: `add_dist_right_suc_thm` Returns: `thm`	Returns: `thm`
`add_fn` Full Usage: `add_fn` Returns: `term`	Returns: `term`
`add_id_thm` Full Usage: `add_id_thm` Returns: `thm`	Returns: `thm`
`add_left_id_lemma` Full Usage: `add_left_id_lemma` Returns: `thm`	Returns: `thm`
`add_sub_cancel_thm` Full Usage: `add_sub_cancel_thm` Returns: `thm`	Returns: `thm`
`add_switch_lemma` Full Usage: `add_switch_lemma` Returns: `thm`	Returns: `thm`
`dest_add` Full Usage: `dest_add` Returns: `term -> term * term`	Returns: `term -> term * term`
`dest_even tm` Full Usage: `dest_even tm` Parameters: tm : `term` Returns: `term`	tm : `term` Returns: `term`
`dest_exp` Full Usage: `dest_exp` Returns: `term -> term * term`	Returns: `term -> term * term`
`dest_mult` Full Usage: `dest_mult` Returns: `term -> term * term`	Returns: `term -> term * term`
`dest_odd tm` Full Usage: `dest_odd tm` Parameters: tm : `term` Returns: `term`	tm : `term` Returns: `term`
`dest_pre tm` Full Usage: `dest_pre tm` Parameters: tm : `term` Returns: `term`	tm : `term` Returns: `term`
`dest_sub` Full Usage: `dest_sub` Returns: `term -> term * term`	Returns: `term -> term * term`
`even_def` Full Usage: `even_def` Returns: `thm`	\|- (EVEN 0 <=> true) /\ (!n. EVEN (SUC n) <=> ~ EVEN n) Returns: `thm`
`even_fn` Full Usage: `even_fn` Returns: `term`	Returns: `term`
`even_suc_thm` Full Usage: `even_suc_thm` Returns: `thm`	Returns: `thm`
`exp_def` Full Usage: `exp_def` Returns: `thm`	\|- (!n. n EXP 0 = 1) /\ (!m n. m EXP SUC n = m * m EXP n) Returns: `thm`
`exp_dist_right_add_thm` Full Usage: `exp_dist_right_add_thm` Returns: `thm`	Returns: `thm`
`exp_dist_right_suc_thm` Full Usage: `exp_dist_right_suc_thm` Returns: `thm`	Returns: `thm`
`exp_fn` Full Usage: `exp_fn` Returns: `term`	Returns: `term`
`exp_right_id_thm` Full Usage: `exp_right_id_thm` Returns: `thm`	Returns: `thm`
`exp_right_zero_thm` Full Usage: `exp_right_zero_thm` Returns: `thm`	Returns: `thm`
`is_add` Full Usage: `is_add` Returns: `term -> bool`	Returns: `term -> bool`
`is_even` Full Usage: `is_even` Returns: `term -> bool`	Returns: `term -> bool`
`is_exp` Full Usage: `is_exp` Returns: `term -> bool`	Returns: `term -> bool`
`is_mult` Full Usage: `is_mult` Returns: `term -> bool`	Returns: `term -> bool`
`is_odd` Full Usage: `is_odd` Returns: `term -> bool`	Returns: `term -> bool`
`is_pre` Full Usage: `is_pre` Returns: `term -> bool`	Returns: `term -> bool`
`is_sub` Full Usage: `is_sub` Returns: `term -> bool`	Returns: `term -> bool`
`l` Full Usage: `l` Returns: `term`	Returns: `term`
`load` Full Usage: `load` Returns: `(string * thm) list`	Force module evaluation Returns: `(string * thm) list`
`m` Full Usage: `m` Returns: `term`	Returns: `term`
`mk_add (tm1, tm2)` Full Usage: `mk_add (tm1, tm2)` Parameters: tm1 : `term` tm2 : `term` Returns: `term`	tm1 : `term` tm2 : `term` Returns: `term`
`mk_even tm` Full Usage: `mk_even tm` Parameters: tm : `term` Returns: `term`	tm : `term` Returns: `term`
`mk_exp (tm1, tm2)` Full Usage: `mk_exp (tm1, tm2)` Parameters: tm1 : `term` tm2 : `term` Returns: `term`	tm1 : `term` tm2 : `term` Returns: `term`
`mk_mult (tm1, tm2)` Full Usage: `mk_mult (tm1, tm2)` Parameters: tm1 : `term` tm2 : `term` Returns: `term`	tm1 : `term` tm2 : `term` Returns: `term`
`mk_odd tm` Full Usage: `mk_odd tm` Parameters: tm : `term` Returns: `term`	tm : `term` Returns: `term`
`mk_pre tm` Full Usage: `mk_pre tm` Parameters: tm : `term` Returns: `term`	tm : `term` Returns: `term`
`mk_sub (tm1, tm2)` Full Usage: `mk_sub (tm1, tm2)` Parameters: tm1 : `term` tm2 : `term` Returns: `term`	tm1 : `term` tm2 : `term` Returns: `term`
`mult_assoc_thm` Full Usage: `mult_assoc_thm` Returns: `thm`	Returns: `thm`
`mult_comm_thm` Full Usage: `mult_comm_thm` Returns: `thm`	Returns: `thm`
`mult_def` Full Usage: `mult_def` Returns: `thm`	\|- (!n. 0 * n = 0) /\ (!m n. SUC m * n = n + m * n) Returns: `thm`
`mult_dist_left_add_thm` Full Usage: `mult_dist_left_add_thm` Returns: `thm`	Returns: `thm`
`mult_dist_left_suc_thm` Full Usage: `mult_dist_left_suc_thm` Returns: `thm`	Returns: `thm`
`mult_dist_right_add_thm` Full Usage: `mult_dist_right_add_thm` Returns: `thm`	Returns: `thm`
`mult_dist_right_suc_thm` Full Usage: `mult_dist_right_suc_thm` Returns: `thm`	Returns: `thm`
`mult_fn` Full Usage: `mult_fn` Returns: `term`	Returns: `term`
`mult_id_thm` Full Usage: `mult_id_thm` Returns: `thm`	Returns: `thm`
`mult_left_flip_lemma` Full Usage: `mult_left_flip_lemma` Returns: `thm`	Returns: `thm`
`mult_left_id_lemma` Full Usage: `mult_left_id_lemma` Returns: `thm`	Returns: `thm`
`mult_left_zero_lemma` Full Usage: `mult_left_zero_lemma` Returns: `thm`	Returns: `thm`
`mult_zero_thm` Full Usage: `mult_zero_thm` Returns: `thm`	Returns: `thm`
`n` Full Usage: `n` Returns: `term`	Returns: `term`
`odd_def` Full Usage: `odd_def` Returns: `thm`	\|- !n. ODD n <=> ~ EVEN n Returns: `thm`
`odd_fn` Full Usage: `odd_fn` Returns: `term`	Returns: `term`
`odd_suc_thm` Full Usage: `odd_suc_thm` Returns: `thm`	Returns: `thm`
`one_odd_thm` Full Usage: `one_odd_thm` Returns: `thm`	Returns: `thm`
`pre_def` Full Usage: `pre_def` Returns: `thm`	\|- PRE 0 = 0 /\ (!n. PRE (SUC n) = n) Returns: `thm`
`pre_fn` Full Usage: `pre_fn` Returns: `term`	Returns: `term`
`pre_suc_thm` Full Usage: `pre_suc_thm` Returns: `thm`	Returns: `thm`
`pre_zero_thm` Full Usage: `pre_zero_thm` Returns: `thm`	Returns: `thm`
`sub_cancel_thm` Full Usage: `sub_cancel_thm` Returns: `thm`	Returns: `thm`
`sub_def` Full Usage: `sub_def` Returns: `thm`	\|- (!n. n - 0 = n) /\ (!m n. m - SUC n = PRE (m - n)) Returns: `thm`
`sub_dist_right_suc_thm` Full Usage: `sub_dist_right_suc_thm` Returns: `thm`	Returns: `thm`
`sub_fn` Full Usage: `sub_fn` Returns: `term`	Returns: `term`
`sub_right_id_thm` Full Usage: `sub_right_id_thm` Returns: `thm`	Returns: `thm`
`suc_add_thm` Full Usage: `suc_add_thm` Returns: `thm`	Returns: `thm`
`suc_sub_suc_thm` Full Usage: `suc_sub_suc_thm` Returns: `thm`	Returns: `thm`
`suc_twice_odd_thm` Full Usage: `suc_twice_odd_thm` Returns: `thm`	Returns: `thm`
`twice_even_thm` Full Usage: `twice_even_thm` Returns: `thm`	Returns: `thm`
`twice_suc_lemma` Full Usage: `twice_suc_lemma` Returns: `thm`	Returns: `thm`
`twice_thm` Full Usage: `twice_thm` Returns: `thm`	Returns: `thm`
`w` Full Usage: `w` Returns: `term`	Returns: `term`
`x` Full Usage: `x` Returns: `term`	Returns: `term`
`y` Full Usage: `y` Returns: `term`	Returns: `term`
`z` Full Usage: `z` Returns: `term`	Returns: `term`
`zero_even_thm` Full Usage: `zero_even_thm` Returns: `thm`	Returns: `thm`
`zero_not_odd_thm` Full Usage: `zero_not_odd_thm` Returns: `thm`	Returns: `thm`