NatRel (nholz)

NatRel Module

Namespace: HOL
Assembly: nholz.dll

This module defines the classic natural number arithmetic relations and derives various basic properties about them.

Functions and values

Function or value	Description
`add_eq_cancel_thm` Full Usage: `add_eq_cancel_thm` Returns: `thm`	Returns: `thm`
`add_eq_zero_thm` Full Usage: `add_eq_zero_thm` Returns: `thm`	Returns: `thm`
`add_le_cancel_thm` Full Usage: `add_le_cancel_thm` Returns: `thm`	Returns: `thm`
`add_lt_cancel_thm` Full Usage: `add_lt_cancel_thm` Returns: `thm`	Returns: `thm`
`dest_ge` Full Usage: `dest_ge` Returns: `term -> term * term`	Returns: `term -> term * term`
`dest_gt` Full Usage: `dest_gt` Returns: `term -> term * term`	Returns: `term -> term * term`
`dest_le` Full Usage: `dest_le` Returns: `term -> term * term`	Returns: `term -> term * term`
`dest_lt` Full Usage: `dest_lt` Returns: `term -> term * term`	Returns: `term -> term * term`
`ge_def` Full Usage: `ge_def` Returns: `thm`	\|- !m n. m >= n <=> n <= m Returns: `thm`
`ge_fn` Full Usage: `ge_fn` Returns: `term`	Returns: `term`
`gt_def` Full Usage: `gt_def` Returns: `thm`	\|- !m n. m > n <=> n < m Returns: `thm`
`gt_fn` Full Usage: `gt_fn` Returns: `term`	Returns: `term`
`is_ge` Full Usage: `is_ge` Returns: `term -> bool`	Returns: `term -> bool`
`is_gt` Full Usage: `is_gt` Returns: `term -> bool`	Returns: `term -> bool`
`is_le` Full Usage: `is_le` Returns: `term -> bool`	Returns: `term -> bool`
`is_lt` Full Usage: `is_lt` Returns: `term -> bool`	Returns: `term -> bool`
`l` Full Usage: `l` Returns: `term`	Returns: `term`
`le_antisym_thm` Full Usage: `le_antisym_thm` Returns: `thm`	Returns: `thm`
`le_cases_thm` Full Usage: `le_cases_thm` Returns: `thm`	Returns: `thm`
`le_def` Full Usage: `le_def` Returns: `thm`	\|- !m n. m <= n <=> m < n \/ m = n Returns: `thm`
`le_fn` Full Usage: `le_fn` Returns: `term`	Returns: `term`
`le_refl_thm` Full Usage: `le_refl_thm` Returns: `thm`	Returns: `thm`
`le_trans_thm` Full Usage: `le_trans_thm` Returns: `thm`	Returns: `thm`
`le_zero_thm` Full Usage: `le_zero_thm` Returns: `thm`	Returns: `thm`
`load` Full Usage: `load` Returns: `(string * thm) list`	Force module evaluation Returns: `(string * thm) list`
`lt_asym_thm` Full Usage: `lt_asym_thm` Returns: `thm`	Returns: `thm`
`lt_def` Full Usage: `lt_def` Returns: `thm`	\|- (!m. m < 0 <=> false) /\ (!m n. m < SUC n <=> m = n \/ m < n) Returns: `thm`
`lt_fn` Full Usage: `lt_fn` Returns: `term`	Returns: `term`
`lt_irrefl_thm` Full Usage: `lt_irrefl_thm` Returns: `thm`	Returns: `thm`
`lt_suc_cases_thm` Full Usage: `lt_suc_cases_thm` Returns: `thm`	Returns: `thm`
`lt_suc_le_thm` Full Usage: `lt_suc_le_thm` Returns: `thm`	Returns: `thm`
`lt_suc_thm` Full Usage: `lt_suc_thm` Returns: `thm`	Returns: `thm`
`lt_trans_thm` Full Usage: `lt_trans_thm` Returns: `thm`	Returns: `thm`
`lt_zero_cases_thm` Full Usage: `lt_zero_cases_thm` Returns: `thm`	Returns: `thm`
`m` Full Usage: `m` Returns: `term`	Returns: `term`
`mk_ge (tm1, tm2)` Full Usage: `mk_ge (tm1, tm2)` Parameters: tm1 : `term` tm2 : `term` Returns: `term`	tm1 : `term` tm2 : `term` Returns: `term`
`mk_gt (tm1, tm2)` Full Usage: `mk_gt (tm1, tm2)` Parameters: tm1 : `term` tm2 : `term` Returns: `term`	tm1 : `term` tm2 : `term` Returns: `term`
`mk_le (tm1, tm2)` Full Usage: `mk_le (tm1, tm2)` Parameters: tm1 : `term` tm2 : `term` Returns: `term`	tm1 : `term` tm2 : `term` Returns: `term`
`mk_lt (tm1, tm2)` Full Usage: `mk_lt (tm1, tm2)` Parameters: tm1 : `term` tm2 : `term` Returns: `term`	tm1 : `term` tm2 : `term` Returns: `term`
`mult_eq_cancel_thm` Full Usage: `mult_eq_cancel_thm` Returns: `thm`	Returns: `thm`
`mult_eq_zero_thm` Full Usage: `mult_eq_zero_thm` Returns: `thm`	Returns: `thm`
`mult_le_cancel_thm` Full Usage: `mult_le_cancel_thm` Returns: `thm`	Returns: `thm`
`mult_lt_cancel_thm` Full Usage: `mult_lt_cancel_thm` Returns: `thm`	Returns: `thm`
`n` Full Usage: `n` Returns: `term`	Returns: `term`
`not_lt_cases_thm` Full Usage: `not_lt_cases_thm` Returns: `thm`	Returns: `thm`
`not_lt_zero_thm` Full Usage: `not_lt_zero_thm` Returns: `thm`	Returns: `thm`
`sub_floor_thm` Full Usage: `sub_floor_thm` Returns: `thm`	Returns: `thm`
`suc_le_cancel_thm` Full Usage: `suc_le_cancel_thm` Returns: `thm`	Returns: `thm`
`suc_le_lt_thm` Full Usage: `suc_le_lt_thm` Returns: `thm`	Returns: `thm`
`suc_lt_cancel_thm` Full Usage: `suc_lt_cancel_thm` Returns: `thm`	Returns: `thm`
`zero_le_thm` Full Usage: `zero_le_thm` Returns: `thm`	Returns: `thm`
`zero_lt_suc_thm` Full Usage: `zero_lt_suc_thm` Returns: `thm`	Returns: `thm`
`zero_lt_thm` Full Usage: `zero_lt_thm` Returns: `thm`	Returns: `thm`