Ind (nholz)

Ind Module

Namespace: HOL
Assembly: nholz.dll

This module extends the HOL logic with an infinite-cardinality base type, together with a zero and a successor function for this type. These get used in the 'Nat' module as the basis for defining the natural numbers.

Functions and values

Function or value	Description
`ind_suc_fn` Full Usage: `ind_suc_fn` Returns: `term`	Returns: `term`
`ind_suc_injective_thm` Full Usage: `ind_suc_injective_thm` Returns: `thm`	\|- !i j. IND_SUC i = IND_SUC j <=> i = j Returns: `thm`
`ind_suc_not_zero_thm` Full Usage: `ind_suc_not_zero_thm` Returns: `thm`	\|- !i. ~(IND_SUC i = IND_ZERO) Returns: `thm`
`ind_suc_zero_exists_lemma` Full Usage: `ind_suc_zero_exists_lemma` Returns: `thm`	Returns: `thm`
`ind_suc_zero_spec` Full Usage: `ind_suc_zero_spec` Returns: `thm`	\|- ONE_ONE IND_SUC /\ (!i. ~ (IND_SUC i = IND_ZERO)) Returns: `thm`
`ind_ty` Full Usage: `ind_ty` Returns: `hol_type`	An infinite-cardinality base type, called "ind" and referred to as "the individual types Returns: `hol_type`
`ind_zero_tm` Full Usage: `ind_zero_tm` Returns: `term`	Returns: `term`
`infinity_ax` Full Usage: `infinity_ax` Returns: `thm`	Infinity axiom This states that the newly declared individuals type is infinite, by asserting that there is an injective total function from individuals to individuals that is not surjective. \|- ?(f:ind->ind). ONE_ONE f /\ ~ ONTO f Returns: `thm`
`load` Full Usage: `load` Returns: `(string * thm) list`	Force module evaluation Returns: `(string * thm) list`
`not_onto_lemma` Full Usage: `not_onto_lemma` Returns: `thm`	Returns: `thm`