Utils1 (nholz)

Utils1 Module

Namespace: HOL
Assembly: nholz.dll

This module defines various basic operations on types and terms that get used in the implementation of the primitive inference rules and primitive assertion commands in the 'Thm' module. This module is a trusted component of the system.

Types

Type	Description
Clash
destructed_term
destructed_type

Functions and values

Function or value	Description
`a_ty` Full Usage: `a_ty` Returns: `hol_type`	Returns: `hol_type`
`alpha_eq tm1 tm2` Full Usage: `alpha_eq tm1 tm2` Parameters: tm1 : `term` tm2 : `term` Returns: `bool`	Two terms are alpha-equivalent iff they are equal modulo names chosen for bound variable (i.e. ignoring the differences in the names of bound variables) tm1 : `term` tm2 : `term` Returns: `bool`
`alpha_eq0 theta0 tm1 tm2` Full Usage: `alpha_eq0 theta0 tm1 tm2` Parameters: theta0 : `(term * term) list` tm1 : `term` tm2 : `term` Returns: `bool`	theta0 : `(term * term) list` tm1 : `term` tm2 : `term` Returns: `bool`
`b_ty` Full Usage: `b_ty` Returns: `hol_type`	Returns: `hol_type`
`c_ty` Full Usage: `c_ty` Returns: `hol_type`	Returns: `hol_type`
`const_name tm` Full Usage: `const_name tm` Parameters: tm : `term` Returns: `string`	tm : `term` Returns: `string`
`const_type tm` Full Usage: `const_type tm` Parameters: tm : `term` Returns: `hol_type`	tm : `term` Returns: `hol_type`
`cvariant vs0 v` Full Usage: `cvariant vs0 v` Parameters: vs0 : `term list` v : `term` Returns: `term`	vs0 : `term list` v : `term` Returns: `term`
`cvariant_name xs0 x` Full Usage: `cvariant_name xs0 x` Parameters: xs0 : `string list` x : `string` Returns: `string`	xs0 : `string list` x : `string` Returns: `string`
`dest_bin tm` Full Usage: `dest_bin tm` Parameters: tm : `term` Returns: `term * term * term`	tm : `term` Returns: `term * term * term`
`dest_binder tm` Full Usage: `dest_binder tm` Parameters: tm : `term` Returns: `term * term * term`	tm : `term` Returns: `term * term * term`
`dest_cbin x tm` Full Usage: `dest_cbin x tm` Parameters: x : `string` tm : `term` Returns: `term * term`	x : `string` tm : `term` Returns: `term * term`
`dest_cbinder x tm` Full Usage: `dest_cbinder x tm` Parameters: x : `string` tm : `term` Returns: `term * term`	x : `string` tm : `term` Returns: `term * term`
`dest_eq tm` Full Usage: `dest_eq tm` Parameters: tm : `term` Returns: `term * term`	tm : `term` Returns: `term * term`
`dest_exists tm` Full Usage: `dest_exists tm` Parameters: tm : `term` Returns: `term * term`	tm : `term` Returns: `term * term`
`dest_imp tm` Full Usage: `dest_imp tm` Parameters: tm : `term` Returns: `term * term`	tm : `term` Returns: `term * term`
`dest_term tm` Full Usage: `dest_term tm` Parameters: tm : `term` Returns: `destructed_term`	Converts a term in a destructed term tm : `term` Returns: `destructed_term`
`dest_type ty` Full Usage: `dest_type ty` Parameters: ty : `hol_type` Returns: `destructed_type`	ty : `hol_type` Returns: `destructed_type`
`free_vars tm` Full Usage: `free_vars tm` Parameters: tm : `term` Returns: `term list`	Extracts the free variables in a term: those that occur in the term and are unbounded by any lambda abstraction tm : `term` Returns: `term list`
`is_bin tm` Full Usage: `is_bin tm` Parameters: tm : `term` Returns: `bool`	tm : `term` Returns: `bool`
`is_binder tm` Full Usage: `is_binder tm` Parameters: tm : `term` Returns: `bool`	tm : `term` Returns: `bool`
`is_bool_term tm` Full Usage: `is_bool_term tm` Parameters: tm : `term` Returns: `bool`	Boolean-valued terms tm : `term` Returns: `bool`
`is_bool_type ty` Full Usage: `is_bool_type ty` Parameters: ty : `hol_type` Returns: `bool`	A discriminator for the boolean base type ty : `hol_type` Returns: `bool`
`is_eq tm` Full Usage: `is_eq tm` Parameters: tm : `term` Returns: `bool`	tm : `term` Returns: `bool`
`is_exists tm` Full Usage: `is_exists tm` Parameters: tm : `term` Returns: `bool`	tm : `term` Returns: `bool`
`is_imp tm` Full Usage: `is_imp tm` Parameters: tm : `term` Returns: `bool`	tm : `term` Returns: `bool`
`list_mk_comb (tm, tms)` Full Usage: `list_mk_comb (tm, tms)` Parameters: tm : `term` tms : `term list` Returns: `term`	tm : `term` tms : `term list` Returns: `term`
`list_mk_exists (vs, tm0)` Full Usage: `list_mk_exists (vs, tm0)` Parameters: vs : `term list` tm0 : `term` Returns: `term`	vs : `term list` tm0 : `term` Returns: `term`
`mk_bin (f, tm1, tm2)` Full Usage: `mk_bin (f, tm1, tm2)` Parameters: f : `term` tm1 : `term` tm2 : `term` Returns: `term`	f : `term` tm1 : `term` tm2 : `term` Returns: `term`
`mk_binder (f, v, tm0)` Full Usage: `mk_binder (f, v, tm0)` Parameters: f : `term` v : `term` tm0 : `term` Returns: `term`	f : `term` v : `term` tm0 : `term` Returns: `term`
`mk_const (x, ty)` Full Usage: `mk_const (x, ty)` Parameters: x : `string` ty : `hol_type` Returns: `term`	A derived constructor for constants. It takes a constant name and a type (defined in the type constants db), where the type must be a valid match for the constant's generic type (defined in the term constants db). It returns the constant with the supplied type as its type. x : `string` ty : `hol_type` Returns: `term`
`mk_eq (tm1, tm2)` Full Usage: `mk_eq (tm1, tm2)` Parameters: tm1 : `term` tm2 : `term` Returns: `term`	tm1 : `term` tm2 : `term` Returns: `term`
`mk_exists (v, tm0)` Full Usage: `mk_exists (v, tm0)` Parameters: v : `term` tm0 : `term` Returns: `term`	v : `term` tm0 : `term` Returns: `term`
`mk_imp (tm1, tm2)` Full Usage: `mk_imp (tm1, tm2)` Parameters: tm1 : `term` tm2 : `term` Returns: `term`	tm1 : `term` tm2 : `term` Returns: `term`
`strip_exists tm` Full Usage: `strip_exists tm` Parameters: tm : `term` Returns: `term list * term`	tm : `term` Returns: `term list * term`
`term_tyvars tm` Full Usage: `term_tyvars tm` Parameters: tm : `term` Returns: `hol_type list`	tm : `term` Returns: `hol_type list`
`type_match patt ty` Full Usage: `type_match patt ty` Parameters: patt : `hol_type` ty : `hol_type` Returns: `(hol_type * hol_type) list`	Takes a type pattern and a type match, and returns an old-to-new tyvar instn list for tyvars in the type pattern to make it equal to the match. A failure is raised if the match doesn't fit the pattern. patt : `hol_type` ty : `hol_type` Returns: `(hol_type * hol_type) list`
`type_match0 theta patt ty` Full Usage: `type_match0 theta patt ty` Parameters: theta : `(hol_type * hol_type) list` patt : `hol_type` ty : `hol_type` Returns: `(hol_type * hol_type) list`	theta : `(hol_type * hol_type) list` patt : `hol_type` ty : `hol_type` Returns: `(hol_type * hol_type) list`
`type_tyvars ty` Full Usage: `type_tyvars ty` Parameters: ty : `hol_type` Returns: `hol_type list`	Lists all the type variables that occur in a type. ty : `hol_type` Returns: `hol_type list`
`tyvar_inst tytheta tm` Full Usage: `tyvar_inst tytheta tm` Parameters: tytheta : `(hol_type * hol_type) list` tm : `term` Returns: `term`	tytheta : `(hol_type * hol_type) list` tm : `term` Returns: `term`
`tyvar_inst0 theta0 tytheta tm` Full Usage: `tyvar_inst0 theta0 tytheta tm` Parameters: theta0 : `(term * term) list` tytheta : `(hol_type * hol_type) list` tm : `term` Returns: `term`	theta0 : `(term * term) list` tytheta : `(hol_type * hol_type) list` tm : `term` Returns: `term`
`var_free_in v tm` Full Usage: `var_free_in v tm` Parameters: v : `term` tm : `term` Returns: `bool`	Checks if a variable occurs free in a term v : `term` tm : `term` Returns: `bool`
`var_free_in0 v tm` Full Usage: `var_free_in0 v tm` Parameters: v : `term` tm : `term` Returns: `bool`	v : `term` tm : `term` Returns: `bool`
`var_inst theta tm` Full Usage: `var_inst theta tm` Parameters: theta : `(term * term) list` tm : `term` Returns: `term`	theta : `(term * term) list` tm : `term` Returns: `term`
`var_inst0 vs0 theta tm` Full Usage: `var_inst0 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`
`var_name tm` Full Usage: `var_name tm` Parameters: tm : `term` Returns: `string`	tm : `term` Returns: `string`
`var_type tm` Full Usage: `var_type tm` Parameters: tm : `term` Returns: `hol_type`	tm : `term` Returns: `hol_type`
`variant vs0 v` Full Usage: `variant vs0 v` Parameters: vs0 : `term list` v : `term` Returns: `term`	vs0 : `term list` v : `term` Returns: `term`