Structure boolSyntax

signature boolSyntax =
sig
  type thm      = Thm.thm
  type term     = Term.term
  type hol_type = Type.hol_type
  type goal     = term list * term


  (* Constants *)

  val equality       : term
  val implication    : term
  val select         : term
  val T              : term
  val F              : term
  val universal      : term
  val existential    : term
  val exists1        : term
  val conjunction    : term
  val disjunction    : term
  val negation       : term
  val conditional    : term
  val bool_case      : term
  val literal_case   : term
  val let_tm         : term
  val arb            : term
  val the_value      : term
  val bounded_tm     : term
  val IN_tm          : term
  val res_forall_tm  : term
  val res_exists_tm  : term
  val res_exists1_tm : term
  val res_select_tm  : term
  val res_abstract_tm: term

  (* Construction routines *)

  val mk_eq                  : term * term -> term
  val mk_imp                 : term * term -> term
  val mk_select              : term * term -> term
  val mk_forall              : term * term -> term
  val mk_exists              : term * term -> term
  val mk_exists1             : term * term -> term
  val mk_conj                : term * term -> term
  val mk_disj                : term * term -> term
  val mk_neg                 : term -> term
  val mk_let                 : term * term -> term
  val mk_cond                : term * term * term -> term
  val mk_bool_case           : term * term * term -> term
  val mk_literal_case        : term * term -> term
  val mk_arb                 : hol_type -> term
  val mk_itself              : hol_type -> term
  val mk_res_forall          : term * term * term -> term
  val mk_res_exists          : term * term * term -> term
  val mk_res_exists_unique   : term * term * term -> term
  val mk_res_select          : term * term * term -> term
  val mk_res_abstract        : term * term * term -> term
  val mk_icomb               : term * term -> term
  val mk_IN                  : term * term -> term
  val mk_ucomb               : term * term -> term

  (* Destruction routines *)

  val dest_eq                : term -> term * term
  val dest_eq_ty             : term -> term * term * hol_type
  val lhs                    : term -> term
  val rhs                    : term -> term
  val lhand                  : term -> term
  val rand                   : term -> term
  val rator                  : term -> term
  val dest_imp               : term -> term * term
  val dest_imp_only          : term -> term * term
  val dest_select            : term -> term * term
  val dest_forall            : term -> term * term
  val dest_exists            : term -> term * term
  val dest_exists1           : term -> term * term
  val dest_conj              : term -> term * term
  val dest_disj              : term -> term * term
  val dest_neg               : term -> term
  val dest_let               : term -> term * term
  val dest_cond              : term -> term * term * term
  val dest_bool_case         : term -> term * term * term
  val dest_literal_case      : term -> term * term
  val dest_arb               : term -> hol_type
  val dest_itself            : term -> hol_type
  val dest_res_forall        : term -> term * term * term
  val dest_res_exists        : term -> term * term * term
  val dest_res_exists_unique : term -> term * term * term
  val dest_res_select        : term -> term * term * term
  val dest_res_abstract      : term -> term * term * term
  val dest_IN                : term -> term * term


  (* Query routines *)

  val is_eq                  : term -> bool
  val is_imp                 : term -> bool
  val is_imp_only            : term -> bool
  val is_select              : term -> bool
  val is_forall              : term -> bool
  val is_exists              : term -> bool
  val is_exists1             : term -> bool
  val is_conj                : term -> bool
  val is_disj                : term -> bool
  val is_neg                 : term -> bool
  val is_cond                : term -> bool
  val is_bool_case           : term -> bool
  val is_literal_case        : term -> bool
  val is_let                 : term -> bool
  val is_arb                 : term -> bool
  val is_the_value           : term -> bool
  val is_res_forall          : term -> bool
  val is_res_exists          : term -> bool
  val is_res_exists_unique   : term -> bool
  val is_res_select          : term -> bool
  val is_res_abstract        : term -> bool
  val is_IN                  : term -> bool
  val is_bool_atom           : term -> bool

  (* Construction of a term from a list of terms *)

  val list_mk_abs            : term list * term -> term
  val list_mk_forall         : term list * term -> term
  val list_mk_exists         : term list * term -> term
  val list_mk_imp            : term list * term -> term
  val list_mk_conj           : term list -> term
  val list_mk_disj           : term list -> term
  val list_mk_fun            : hol_type list * hol_type -> hol_type
  val list_mk_res_forall     : (term * term) list * term -> term
  val list_mk_res_exists     : (term * term) list * term -> term
  val list_mk_icomb          : term * term list -> term
  val list_mk_ucomb          : term * term list -> term
  val gen_all                : term -> term

  (* Destructing a term to a list of terms *)

  val strip_comb             : term -> term * term list
  val strip_abs              : term -> term list * term
  val strip_imp              : term -> term list * term
  val strip_imp_only         : term -> term list * term
  val strip_forall           : term -> term list * term
  val strip_exists           : term -> term list * term
  val strip_conj             : term -> term list
  val strip_disj             : term -> term list
  val strip_neg              : term -> term * int
  val strip_res_forall       : term -> (term * term) list * term
  val strip_res_exists       : term -> (term * term) list * term
  val strip_fun              : hol_type -> hol_type list * hol_type

  val dest_strip_comb        : term -> string * term list

  (* Connecting signature operations with grammar operations. *)

  val new_type              : string * int -> unit
  val new_infix_type        : {Name:string, Arity:int,
                               ParseName:string option, Prec:int,
                               Assoc:Parse.associativity} -> unit

  val new_constant          : string * hol_type -> unit
  val new_infix             : string * hol_type * int -> unit
  val new_binder            : string * hol_type -> unit
  val delete_const          : string -> unit
  val new_type_definition   : string * thm -> thm
  val new_infixl_definition : string * term * int -> thm
  val new_infixr_definition : string * term * int -> thm
  val new_binder_definition : string * term -> thm


  (* Lifter from ML bool to HOL bool *)

  val lift_bool : hol_type -> bool -> term

  (* Algebraic properties *)

  val comm_tm     : term
  val assoc_tm    : term
  val idem_tm     : term
  val ldistrib_tm : term
  val rdistrib_tm : term

  (* sets and aconv *)
  val ~~ : term * term -> bool
  val !~ : term * term -> bool
  val singt : term -> term HOLset.set
  val listset : term list -> term HOLset.set
  val FVs : term -> term HOLset.set
  val FVLset : term list -> term HOLset.set
  val ES : term HOLset.set
  val Teq : term -> bool  (* equals the T constant *)
  val Feq : term -> bool  (* equals the F constant *)
  val tml_eq : term list -> term list -> bool
  val tmp_eq : term * term -> term * term -> bool
  val goal_eq : goal -> goal -> bool
  val goals_eq : goal list -> goal list -> bool
  val tmem : term -> term list -> bool
  val memt : term list -> term -> bool  (* flip of above *)
  val tunion : term list -> term list -> term list
  val tassoc : term -> (term * 'a) list -> 'a
  val tmx_eq : term * ''a -> term * ''a -> bool
  val xtm_eq : ''a * term -> ''a * term -> bool

  (* (Type) unification *)
  val gen_tyvar_sigma : hol_type list -> (hol_type,hol_type) Lib.subst
  val gen_tyvarify : term -> term
  val type_unify : hol_type -> hol_type -> (hol_type, hol_type) Lib.subst
  val sep_type_unify : hol_type -> hol_type ->
              (hol_type, hol_type) Lib.subst * (hol_type, hol_type) Lib.subst



end

HOL 4, Kananaskis-14