Utils2 (nholz)

Utils2 Module

Namespace: HOL
Assembly: nholz.dll

This module defines various basic useful operations on types, terms and theorems.

Types

Type	Description
Clash

Functions and values

Function or value	Description
`all_vars tm` Full Usage: `all_vars tm` Parameters: tm : `term` Returns: `term list`	tm : `term` Returns: `term list`
`avar tm` Full Usage: `avar tm` Parameters: tm : `term` Returns: `term`	tm : `term` Returns: `term`
`body tm` Full Usage: `body tm` Parameters: tm : `term` Returns: `term`	tm : `term` Returns: `term`
`dest_conj tm` Full Usage: `dest_conj tm` Parameters: tm : `term` Returns: `term * term`	Term destructor for conjunctions. `dest_conj("t1 /\ t2" \|> parse_term)` returns `("t1","t2")`. Fails with dest_conj if term is not a conjunction. tm : `term` Returns: `term * term`
`dest_eqthm th` Full Usage: `dest_eqthm th` Parameters: th : `thm` Returns: `term * term`	th : `thm` Returns: `term * term`
`dest_forall tm` Full Usage: `dest_forall tm` Parameters: tm : `term` Returns: `term * term`	tm : `term` Returns: `term * term`
`dest_select tm` Full Usage: `dest_select tm` Parameters: tm : `term` Returns: `term * term`	tm : `term` Returns: `term * term`
`eq_lhs tm` Full Usage: `eq_lhs tm` Parameters: tm : `term` Returns: `term`	tm : `term` Returns: `term`
`eq_rhs tm` Full Usage: `eq_rhs tm` Parameters: tm : `term` Returns: `term`	tm : `term` Returns: `term`
`eqthm_lhs th` Full Usage: `eqthm_lhs th` Parameters: th : `thm` Returns: `term`	th : `thm` Returns: `term`
`eqthm_rhs th` Full Usage: `eqthm_rhs th` Parameters: th : `thm` Returns: `term`	th : `thm` Returns: `term`
`find_subterm test_fn tm` Full Usage: `find_subterm test_fn tm` Parameters: test_fn : `term -> bool` tm : `term` Returns: `term`	test_fn : `term -> bool` tm : `term` Returns: `term`
`find_subterms test_fn tm` Full Usage: `find_subterms test_fn tm` Parameters: test_fn : `term -> bool` tm : `term` Returns: `term list`	test_fn : `term -> bool` tm : `term` Returns: `term list`
`find_subterms0 tms test_fn tm` Full Usage: `find_subterms0 tms test_fn tm` Parameters: tms : `term list` test_fn : `term -> bool` tm : `term` Returns: `term list`	tms : `term list` test_fn : `term -> bool` tm : `term` Returns: `term list`
`flatstrip_conj tm` Full Usage: `flatstrip_conj tm` Parameters: tm : `term` Returns: `term list`	tm : `term` Returns: `term list`
`genvar ty` Full Usage: `genvar ty` Parameters: ty : `hol_type` Returns: `term`	ty : `hol_type` Returns: `term`
`genvar_count` Full Usage: `genvar_count` Returns: `int ref`	Returns: `int ref`
`is_cbin x tm` Full Usage: `is_cbin x tm` Parameters: x : `string` tm : `term` Returns: `bool`	x : `string` tm : `term` Returns: `bool`
`is_cbinder x tm` Full Usage: `is_cbinder x tm` Parameters: x : `string` tm : `term` Returns: `bool`	x : `string` tm : `term` Returns: `bool`
`is_conj tm` Full Usage: `is_conj tm` Parameters: tm : `term` Returns: `bool`	Tests a term to see if it is a conjunction. is_conj ("t1 /\ t2" \|> parse_term) returns true. If the term is not a conjunction the result is false. Never fails. tm : `term` Returns: `bool`
`is_eqthm th` Full Usage: `is_eqthm th` Parameters: th : `thm` Returns: `bool`	th : `thm` Returns: `bool`
`is_forall tm` Full Usage: `is_forall tm` Parameters: tm : `term` Returns: `bool`	tm : `term` Returns: `bool`
`is_select tm` Full Usage: `is_select tm` Parameters: tm : `term` Returns: `bool`	tm : `term` Returns: `bool`
`list_all_vars tms` Full Usage: `list_all_vars tms` Parameters: tms : `term list` Returns: `term list`	tms : `term list` Returns: `term list`
`list_cvariant vs0 vs` Full Usage: `list_cvariant vs0 vs` Parameters: vs0 : `term list` vs : `term list` Returns: `term list`	vs0 : `term list` vs : `term list` Returns: `term list`
`list_free_vars tms` Full Usage: `list_free_vars tms` Parameters: tms : `term list` Returns: `term list`	tms : `term list` Returns: `term list`
`list_mk_abs (vs, tm0)` Full Usage: `list_mk_abs (vs, tm0)` Parameters: vs : `term list` tm0 : `term` Returns: `term`	vs : `term list` tm0 : `term` Returns: `term`
`list_mk_conj tms` Full Usage: `list_mk_conj tms` Parameters: tms : `term list` Returns: `term`	tms : `term list` Returns: `term`
`list_mk_forall (vs, tm0)` Full Usage: `list_mk_forall (vs, tm0)` Parameters: vs : `term list` tm0 : `term` Returns: `term`	vs : `term list` tm0 : `term` Returns: `term`
`list_mk_fun_type (tys, ty)` Full Usage: `list_mk_fun_type (tys, ty)` Parameters: tys : `hol_type list` ty : `hol_type` Returns: `hol_type`	tys : `hol_type list` ty : `hol_type` Returns: `hol_type`
`list_mk_imp (tms, tm)` Full Usage: `list_mk_imp (tms, tm)` Parameters: tms : `term list` tm : `term` Returns: `term`	tms : `term list` tm : `term` Returns: `term`
`list_variant vs0 vs` Full Usage: `list_variant vs0 vs` Parameters: vs0 : `term list` vs : `term list` Returns: `term list`	vs0 : `term list` vs : `term list` Returns: `term list`
`mk_conj (tm1, tm2)` Full Usage: `mk_conj (tm1, tm2)` Parameters: tm1 : `term` tm2 : `term` Returns: `term`	tm1 : `term` tm2 : `term` Returns: `term`
`mk_forall (v, tm0)` Full Usage: `mk_forall (v, tm0)` Parameters: v : `term` tm0 : `term` Returns: `term`	v : `term` tm0 : `term` Returns: `term`
`mk_select (v, tm0)` Full Usage: `mk_select (v, tm0)` Parameters: v : `term` tm0 : `term` Returns: `term`	v : `term` tm0 : `term` Returns: `term`
`rand tm` Full Usage: `rand tm` Parameters: tm : `term` Returns: `term`	tm : `term` Returns: `term`
`rator tm` Full Usage: `rator tm` Parameters: tm : `term` Returns: `term`	tm : `term` Returns: `term`
`rename_bvar x' tm` Full Usage: `rename_bvar x' tm` Parameters: x' : `string` tm : `term` Returns: `term`	x' : `string` tm : `term` Returns: `term`
`same_types tm1 tm2` Full Usage: `same_types tm1 tm2` Parameters: tm1 : `term` tm2 : `term` Returns: `bool`	tm1 : `term` tm2 : `term` Returns: `bool`
`strip_abs tm` Full Usage: `strip_abs tm` Parameters: tm : `term` Returns: `term list * term`	tm : `term` Returns: `term list * term`
`strip_comb tm` Full Usage: `strip_comb tm` Parameters: tm : `term` Returns: `term * term list`	tm : `term` Returns: `term * term list`
`strip_conj tm` Full Usage: `strip_conj tm` Parameters: tm : `term` Returns: `term list`	tm : `term` Returns: `term list`
`strip_forall tm` Full Usage: `strip_forall tm` Parameters: tm : `term` Returns: `term list * term`	tm : `term` Returns: `term list * term`
`strip_fun_type ty` Full Usage: `strip_fun_type ty` Parameters: ty : `hol_type` Returns: `hol_type list * hol_type`	ty : `hol_type` Returns: `hol_type list * hol_type`
`strip_imp tm` Full Usage: `strip_imp tm` Parameters: tm : `term` Returns: `term list * term`	tm : `term` Returns: `term list * term`
`subst theta tm` Full Usage: `subst theta tm` Parameters: theta : `(term * term) list` tm : `term` Returns: `term`	theta : `(term * term) list` tm : `term` Returns: `term`
`subst0 vs0 theta tm` Full Usage: `subst0 vs0 theta tm` Parameters: vs0 : `term list` theta : `(term * term) list` tm : `term` Returns: `term`	vs0 : `term list` theta : `(term * term) list` tm : `term` Returns: `term`
`term_free_in tm00 tm` Full Usage: `term_free_in tm00 tm` Parameters: tm00 : `term` tm : `term` Returns: `bool`	tm00 : `term` tm : `term` Returns: `bool`
`term_match patt tm` Full Usage: `term_match patt tm` Parameters: patt : `term` tm : `term` Returns: `(term * term) list * (hol_type * hol_type) list`	patt : `term` tm : `term` Returns: `(term * term) list * (hol_type * hol_type) list`
`term_match0 btheta (theta, tytheta) patt tm` Full Usage: `term_match0 btheta (theta, tytheta) patt tm` Parameters: btheta : `(term * term) list` theta : `(term * term) list` tytheta : `(hol_type * hol_type) list` patt : `term` tm : `term` Returns: `(term * term) list * (hol_type * hol_type) list`	btheta : `(term * term) list` theta : `(term * term) list` tytheta : `(hol_type * hol_type) list` patt : `term` tm : `term` Returns: `(term * term) list * (hol_type * hol_type) list`
`term_union tms1 tms2` Full Usage: `term_union tms1 tms2` Parameters: tms1 : `term list` tms2 : `term list` Returns: `term list`	tms1 : `term list` tms2 : `term list` Returns: `term list`
`thm_alpha_eq th1 th2` Full Usage: `thm_alpha_eq th1 th2` Parameters: th1 : `thm` th2 : `thm` Returns: `bool`	th1 : `thm` th2 : `thm` Returns: `bool`
`thm_free_vars th` Full Usage: `thm_free_vars th` Parameters: th : `thm` Returns: `term list`	th : `thm` Returns: `term list`
`var_match patt tm` Full Usage: `var_match patt tm` Parameters: patt : `term` tm : `term` Returns: `(term * term) list`	patt : `term` tm : `term` Returns: `(term * term) list`
`var_match0 btheta theta patt tm` Full Usage: `var_match0 btheta theta patt tm` Parameters: btheta : `(term * term) list` theta : `(term * term) list` patt : `term` tm : `term` Returns: `(term * term) list`	btheta : `(term * term) list` theta : `(term * term) list` patt : `term` tm : `term` Returns: `(term * term) list`