Psyntax

The following shows how to open the Psyntax structure and the functions that subsequently become available in the top level environment. Documentation for each of these functions is available online.

   - open Psyntax;

This command results in the following functions entering the top-level name-space. Term creation functions:

   val mk_var = fn : string * hol_type -> term
   val mk_const = fn : string * hol_type -> term
   val mk_comb = fn : term * term -> term
   val mk_abs = fn : term * term -> term
   val mk_primed_var = fn : string * hol_type -> term
   val mk_eq = fn : term * term -> term
   val mk_imp = fn : term * term -> term
   val mk_select = fn : term * term -> term
   val mk_forall = fn : term * term -> term
   val mk_exists = fn : term * term -> term
   val mk_conj = fn : term * term -> term
   val mk_disj = fn : term * term -> term
   val mk_cond = fn : term * term * term -> term
   val mk_let = fn : term * term -> term

Term “destructor” functions (i.e., those functions that pull a term apart, and reveal some of its internal structure):

   val dest_var = fn : term -> string * hol_type
   val dest_const = fn : term -> string * hol_type
   val dest_comb = fn : term -> term * term
   val dest_abs = fn : term -> term * term
   val dest_eq = fn : term -> term * term
   val dest_imp = fn : term -> term * term
   val dest_select = fn : term -> term * term
   val dest_forall = fn : term -> term * term
   val dest_exists = fn : term -> term * term
   val dest_conj = fn : term -> term * term
   val dest_disj = fn : term -> term * term
   val dest_cond = fn : term -> term * term * term
   val dest_let = fn : term -> term * term

The lambda datatype for taking terms apart, which is the range of the dest_term function.

   datatype lambda =
      VAR of string * hol_type
    | CONST of {Name : string, Thy : string, Ty : hol_type}
    | COMB of term * term
    | LAMB of term * term
   val dest_term : term -> lambda