NatNumrl (nholz)

NatNumrl Module

Namespace: HOL
Assembly: nholz.dll

This module defines the representation of natural number numerals. This is based on the HOL functions "BIT0" and "BIT1".

Nested modules

Modules	Description
Big_intExtension

Functions and values

Function or value	Description
`bit0_def` Full Usage: `bit0_def` Returns: `thm`	\|- (BIT0 ZERO = ZERO) /\ (!n. BIT0 (SUC n) = SUC (SUC (BIT0 n))) Returns: `thm`
`bit0_fn` Full Usage: `bit0_fn` Returns: `term`	Returns: `term`
`bit1_def` Full Usage: `bit1_def` Returns: `thm`	\|- !n. BIT1 n = SUC (BIT0 n) Returns: `thm`
`bit1_fn` Full Usage: `bit1_fn` Returns: `term`	Returns: `term`
`dest_bigint_nat tm` Full Usage: `dest_bigint_nat tm` Parameters: tm : `term` Returns: `BigInteger`	tm : `term` Returns: `BigInteger`
`dest_bigint_nat0 tm` Full Usage: `dest_bigint_nat0 tm` Parameters: tm : `term` Returns: `BigInteger`	tm : `term` Returns: `BigInteger`
`dest_int_nat tm` Full Usage: `dest_int_nat tm` Parameters: tm : `term` Returns: `int`	tm : `term` Returns: `int`
`dest_int_nat0 tm` Full Usage: `dest_int_nat0 tm` Parameters: tm : `term` Returns: `int`	tm : `term` Returns: `int`
`dest_numeral_tag tm` Full Usage: `dest_numeral_tag tm` Parameters: tm : `term` Returns: `term`	tm : `term` Returns: `term`
`is_nat tm` Full Usage: `is_nat tm` Parameters: tm : `term` Returns: `bool`	tm : `term` Returns: `bool`
`is_nat0 tm` Full Usage: `is_nat0 tm` Parameters: tm : `term` Returns: `bool`	tm : `term` Returns: `bool`
`is_numeral_tag tm` Full Usage: `is_numeral_tag tm` Parameters: tm : `term` Returns: `bool`	tm : `term` Returns: `bool`
`load` Full Usage: `load` Returns: `(string * thm) list`	Force module evaluation Returns: `(string * thm) list`
`mk_bigint_nat n` Full Usage: `mk_bigint_nat n` Parameters: n : `BigInteger` Returns: `term`	n : `BigInteger` Returns: `term`
`mk_bigint_nat0 n` Full Usage: `mk_bigint_nat0 n` Parameters: n : `BigInteger` Returns: `term`	n : `BigInteger` Returns: `term`
`mk_int_nat n` Full Usage: `mk_int_nat n` Parameters: n : `int` Returns: `term`	n : `int` Returns: `term`
`mk_int_nat0 n` Full Usage: `mk_int_nat0 n` Parameters: n : `int` Returns: `term`	n : `int` Returns: `term`
`mk_numeral_tag tm` Full Usage: `mk_numeral_tag tm` Parameters: tm : `term` Returns: `term`	tm : `term` Returns: `term`
`nat_cases_thm` Full Usage: `nat_cases_thm` Returns: `thm`	Returns: `thm`
`nat_induction_thm` Full Usage: `nat_induction_thm` Returns: `thm`	Returns: `thm`
`nat_recursion_thm` Full Usage: `nat_recursion_thm` Returns: `thm`	Returns: `thm`
`numeral_def` Full Usage: `numeral_def` Returns: `thm`	\|- !n. NUMERAL n = n Returns: `thm`
`numeral_fn` Full Usage: `numeral_fn` Returns: `term`	Returns: `term`
`numeral_one_thm` Full Usage: `numeral_one_thm` Returns: `thm`	Returns: `thm`
`numeral_zero_thm` Full Usage: `numeral_zero_thm` Returns: `thm`	Returns: `thm`
`numeralise_bin_rule th` Full Usage: `numeralise_bin_rule th` Parameters: th : `thm` Returns: `thm`	th : `thm` Returns: `thm`
`numeralise_bin_thm` Full Usage: `numeralise_bin_thm` Returns: `thm`	Returns: `thm`
`numeralise_mono_rule th` Full Usage: `numeralise_mono_rule th` Parameters: th : `thm` Returns: `thm`	th : `thm` Returns: `thm`
`numeralise_mono_thm` Full Usage: `numeralise_mono_thm` Returns: `thm`	Returns: `thm`
`numeralise_pred_rule th` Full Usage: `numeralise_pred_rule th` Parameters: th : `thm` Returns: `thm`	th : `thm` Returns: `thm`
`numeralise_rel_rule th` Full Usage: `numeralise_rel_rule th` Parameters: th : `thm` Returns: `thm`	th : `thm` Returns: `thm`
`numeralise_rel_thm` Full Usage: `numeralise_rel_thm` Returns: `thm`	Returns: `thm`
`one_not_zero_thm` Full Usage: `one_not_zero_thm` Returns: `thm`	Returns: `thm`
`one_numeral_thm` Full Usage: `one_numeral_thm` Returns: `thm`	Returns: `thm`
`suc_not_zero_thm` Full Usage: `suc_not_zero_thm` Returns: `thm`	Returns: `thm`
`suc_one_thm` Full Usage: `suc_one_thm` Returns: `thm`	Returns: `thm`
`suc_one_thm0` Full Usage: `suc_one_thm0` Returns: `thm`	Returns: `thm`
`suc_zero_thm` Full Usage: `suc_zero_thm` Returns: `thm`	Returns: `thm`
`suc_zero_thm0` Full Usage: `suc_zero_thm0` Returns: `thm`	Returns: `thm`
`two_not_zero_thm` Full Usage: `two_not_zero_thm` Returns: `thm`	Returns: `thm`
`zero_numeral_thm` Full Usage: `zero_numeral_thm` Returns: `thm`	Returns: `thm`
`zero_tm` Full Usage: `zero_tm` Returns: `term`	Returns: `term`