Nat (nholz)

Nat Module

Namespace: HOL
Assembly: nholz.dll

This module extends the HOL logic with the theory of natural numbers. This involves giving theory object definitions for the naturals base type and the "ZERO" and "SUC" constants, based on the theory of individuals, and proving a few important properties.

Functions and values

Function or value	Description
`dest_suc tm` Full Usage: `dest_suc tm` Parameters: tm : `term` Returns: `term`	tm : `term` Returns: `term`
`e` Full Usage: `e` Returns: `term`	Returns: `term`
`exists_prg_defconj_tm` Full Usage: `exists_prg_defconj_tm` Returns: `term`	Returns: `term`
`f` Full Usage: `f` Returns: `term`	Returns: `term`
`f_x_n` Full Usage: `f_x_n` Returns: `term`	Returns: `term`
`f_y_n` Full Usage: `f_y_n` Returns: `term`	Returns: `term`
`fn_` Full Usage: `fn_` Returns: `term`	Returns: `term`
`fn_n` Full Usage: `fn_n` Returns: `term`	Returns: `term`
`ind_suc_is_nat_rep_lemma` Full Usage: `ind_suc_is_nat_rep_lemma` Returns: `thm`	Returns: `thm`
`ind_zero_is_nat_rep_lemma` Full Usage: `ind_zero_is_nat_rep_lemma` Returns: `thm`	Returns: `thm`
`is_nat_rep_def` Full Usage: `is_nat_rep_def` Returns: `thm`	"IsNatRep" is the characteristic function for the naturals base type, prescribing the subset of `:ind` used to represent naturals. It is defined as the function that returns `true` for a given `:ind` element iff any property that holds for "IND_ZERO" and all its successors under "IND_SUC" necessarily holds for the element. This gives the smallest subset of `:ind` containing "IND_ZERO" and closed under "IND_SUC". \|- !i. IsNatRep i <=> (!P. P IND_ZERO /\ (!j. P j ==> P (IND_SUC j)) ==> P i) Returns: `thm`
`is_nat_rep_lemma` Full Usage: `is_nat_rep_lemma` Returns: `thm`	Returns: `thm`
`is_suc tm` Full Usage: `is_suc tm` Parameters: tm : `term` Returns: `bool`	tm : `term` Returns: `bool`
`lemma1` Full Usage: `lemma1` Returns: `thm`	Returns: `thm`
`lemma2` Full Usage: `lemma2` Returns: `thm`	Returns: `thm`
`lemma3` Full Usage: `lemma3` Returns: `thm`	Returns: `thm`
`lemma4` Full Usage: `lemma4` Returns: `thm`	Returns: `thm`
`load` Full Usage: `load` Returns: `(string * thm) list`	Force module evaluation Returns: `(string * thm) list`
`m` Full Usage: `m` Returns: `term`	Returns: `term`
`mk_suc tm` Full Usage: `mk_suc tm` Parameters: tm : `term` Returns: `term`	tm : `term` Returns: `term`
`n` Full Usage: `n` Returns: `term`	Returns: `term`
`n'` Full Usage: `n'` Returns: `term`	Returns: `term`
`nat_bij_def1` Full Usage: `nat_bij_def1` Returns: `thm`	Returns: `thm`
`nat_bij_def2` Full Usage: `nat_bij_def2` Returns: `thm`	Returns: `thm`
`nat_cases_thm0` Full Usage: `nat_cases_thm0` Returns: `thm`	Returns: `thm`
`nat_def` Full Usage: `nat_def` Returns: `thm`	typer for natural numbers \|- ?(f:nat->ind). TYPE_DEFINITION IsNatRep f Returns: `thm`
`nat_induction_thm0` Full Usage: `nat_induction_thm0` Returns: `thm`	Returns: `thm`
`nat_recursion_thm0` Full Usage: `nat_recursion_thm0` Returns: `thm`	Returns: `thm`
`nat_rep_exists_lemma` Full Usage: `nat_rep_exists_lemma` Returns: `thm`	Returns: `thm`
`nat_rep_injective_lemma` Full Usage: `nat_rep_injective_lemma` Returns: `thm`	Returns: `thm`
`nat_rep_suc_lemma` Full Usage: `nat_rep_suc_lemma` Returns: `thm`	Returns: `thm`
`nat_rep_zero_lemma` Full Usage: `nat_rep_zero_lemma` Returns: `thm`	Returns: `thm`
`nat_ty` Full Usage: `nat_ty` Returns: `hol_type`	Returns: `hol_type`
`prg` Full Usage: `prg` Returns: `term`	Returns: `term`
`prg'` Full Usage: `prg'` Returns: `term`	Returns: `term`
`prg'_casesdef_weak_tm` Full Usage: `prg'_casesdef_weak_tm` Returns: `term`	Returns: `term`
`prg_case1_tm` Full Usage: `prg_case1_tm` Returns: `term`	Returns: `term`
`prg_case2_tm` Full Usage: `prg_case2_tm` Returns: `term`	Returns: `term`
`prg_case2_tm_body1_tm` Full Usage: `prg_case2_tm_body1_tm` Returns: `term`	Returns: `term`
`prg_case2_tm_body_tm` Full Usage: `prg_case2_tm_body_tm` Returns: `term`	Returns: `term`
`prg_casesdef_body` Full Usage: `prg_casesdef_body` Returns: `term`	Returns: `term`
`prg_casesdef_tm` Full Usage: `prg_casesdef_tm` Returns: `term`	Returns: `term`
`prg_casesdef_weak_tm` Full Usage: `prg_casesdef_weak_tm` Returns: `term`	Returns: `term`
`prg_defconj_tm` Full Usage: `prg_defconj_tm` Returns: `term`	Returns: `term`
`prg_fpdef_tm` Full Usage: `prg_fpdef_tm` Returns: `term`	Returns: `term`
`prg_n_x` Full Usage: `prg_n_x` Returns: `term`	Returns: `term`
`prg_recdef_tm` Full Usage: `prg_recdef_tm` Returns: `term`	Returns: `term`
`suc_def` Full Usage: `suc_def` Returns: `thm`	\|- !n. SUC n = NatAbs (IND_SUC (NatRep n)) Returns: `thm`
`suc_fn` Full Usage: `suc_fn` Returns: `term`	Returns: `term`
`suc_injective_thm` Full Usage: `suc_injective_thm` Returns: `thm`	Returns: `thm`
`suc_not_zero_thm0` Full Usage: `suc_not_zero_thm0` Returns: `thm`	Returns: `thm`
`x` Full Usage: `x` Returns: `term`	Returns: `term`
`x'` Full Usage: `x'` Returns: `term`	Returns: `term`
`y` Full Usage: `y` Returns: `term`	Returns: `term`
`y1` Full Usage: `y1` Returns: `term`	Returns: `term`
`y2` Full Usage: `y2` Returns: `term`	Returns: `term`
`zero_def` Full Usage: `zero_def` Returns: `thm`	\|- ZERO = NatAbs IND_ZERO Returns: `thm`
`zero_tm0` Full Usage: `zero_tm0` Returns: `term`	Returns: `term`