1signature boolSyntax = 2sig 3 type thm = Thm.thm 4 type term = Term.term 5 type hol_type = Type.hol_type 6 type goal = term list * term 7 8 9 (* Constants *) 10 11 val equality : term 12 val implication : term 13 val select : term 14 val T : term 15 val F : term 16 val universal : term 17 val existential : term 18 val exists1 : term 19 val conjunction : term 20 val disjunction : term 21 val negation : term 22 val conditional : term 23 val bool_case : term 24 val literal_case : term 25 val let_tm : term 26 val arb : term 27 val the_value : term 28 val bounded_tm : term 29 val IN_tm : term 30 val res_forall_tm : term 31 val res_exists_tm : term 32 val res_exists1_tm : term 33 val res_select_tm : term 34 val res_abstract_tm: term 35 36 (* Construction routines *) 37 38 val mk_eq : term * term -> term 39 val mk_imp : term * term -> term 40 val mk_select : term * term -> term 41 val mk_forall : term * term -> term 42 val mk_exists : term * term -> term 43 val mk_exists1 : term * term -> term 44 val mk_conj : term * term -> term 45 val mk_disj : term * term -> term 46 val mk_neg : term -> term 47 val mk_let : term * term -> term 48 val mk_cond : term * term * term -> term 49 val mk_bool_case : term * term * term -> term 50 val mk_literal_case : term * term -> term 51 val mk_arb : hol_type -> term 52 val mk_itself : hol_type -> term 53 val mk_res_forall : term * term * term -> term 54 val mk_res_exists : term * term * term -> term 55 val mk_res_exists_unique : term * term * term -> term 56 val mk_res_select : term * term * term -> term 57 val mk_res_abstract : term * term * term -> term 58 val mk_icomb : term * term -> term 59 val mk_IN : term * term -> term 60 val mk_ucomb : term * term -> term 61 62 (* Destruction routines *) 63 64 val dest_eq : term -> term * term 65 val dest_eq_ty : term -> term * term * hol_type 66 val lhs : term -> term 67 val rhs : term -> term 68 val lhand : term -> term 69 val rand : term -> term 70 val rator : term -> term 71 val dest_imp : term -> term * term 72 val dest_imp_only : term -> term * term 73 val dest_select : term -> term * term 74 val dest_forall : term -> term * term 75 val dest_exists : term -> term * term 76 val dest_exists1 : term -> term * term 77 val dest_conj : term -> term * term 78 val dest_disj : term -> term * term 79 val dest_neg : term -> term 80 val dest_let : term -> term * term 81 val dest_cond : term -> term * term * term 82 val dest_bool_case : term -> term * term * term 83 val dest_literal_case : term -> term * term 84 val dest_arb : term -> hol_type 85 val dest_itself : term -> hol_type 86 val dest_res_forall : term -> term * term * term 87 val dest_res_exists : term -> term * term * term 88 val dest_res_exists_unique : term -> term * term * term 89 val dest_res_select : term -> term * term * term 90 val dest_res_abstract : term -> term * term * term 91 val dest_IN : term -> term * term 92 93 94 (* Query routines *) 95 96 val is_eq : term -> bool 97 val is_imp : term -> bool 98 val is_imp_only : term -> bool 99 val is_select : term -> bool 100 val is_forall : term -> bool 101 val is_exists : term -> bool 102 val is_exists1 : term -> bool 103 val is_conj : term -> bool 104 val is_disj : term -> bool 105 val is_neg : term -> bool 106 val is_cond : term -> bool 107 val is_bool_case : term -> bool 108 val is_literal_case : term -> bool 109 val is_let : term -> bool 110 val is_arb : term -> bool 111 val is_the_value : term -> bool 112 val is_res_forall : term -> bool 113 val is_res_exists : term -> bool 114 val is_res_exists_unique : term -> bool 115 val is_res_select : term -> bool 116 val is_res_abstract : term -> bool 117 val is_IN : term -> bool 118 val is_bool_atom : term -> bool 119 120 (* Construction of a term from a list of terms *) 121 122 val list_mk_abs : term list * term -> term 123 val list_mk_forall : term list * term -> term 124 val list_mk_exists : term list * term -> term 125 val list_mk_imp : term list * term -> term 126 val list_mk_conj : term list -> term 127 val list_mk_disj : term list -> term 128 val list_mk_fun : hol_type list * hol_type -> hol_type 129 val list_mk_res_forall : (term * term) list * term -> term 130 val list_mk_res_exists : (term * term) list * term -> term 131 val list_mk_icomb : term * term list -> term 132 val list_mk_ucomb : term * term list -> term 133 val gen_all : term -> term 134 135 (* Destructing a term to a list of terms *) 136 137 val strip_comb : term -> term * term list 138 val strip_abs : term -> term list * term 139 val strip_imp : term -> term list * term 140 val strip_imp_only : term -> term list * term 141 val strip_forall : term -> term list * term 142 val strip_exists : term -> term list * term 143 val strip_conj : term -> term list 144 val strip_disj : term -> term list 145 val strip_neg : term -> term * int 146 val strip_res_forall : term -> (term * term) list * term 147 val strip_res_exists : term -> (term * term) list * term 148 val strip_fun : hol_type -> hol_type list * hol_type 149 150 val dest_strip_comb : term -> string * term list 151 152 (* Connecting signature operations with grammar operations. *) 153 154 val new_type : string * int -> unit 155 val new_infix_type : {Name:string, Arity:int, 156 ParseName:string option, Prec:int, 157 Assoc:Parse.associativity} -> unit 158 159 val new_constant : string * hol_type -> unit 160 val new_infix : string * hol_type * int -> unit 161 val new_binder : string * hol_type -> unit 162 val delete_const : string -> unit 163 val new_type_definition : string * thm -> thm 164 val new_infixl_definition : string * term * int -> thm 165 val new_infixr_definition : string * term * int -> thm 166 val new_binder_definition : string * term -> thm 167 168 169 (* Lifter from ML bool to HOL bool *) 170 171 val lift_bool : hol_type -> bool -> term 172 173 (* Algebraic properties *) 174 175 val comm_tm : term 176 val assoc_tm : term 177 val idem_tm : term 178 val ldistrib_tm : term 179 val rdistrib_tm : term 180 181 (* sets and aconv *) 182 val ~~ : term * term -> bool 183 val !~ : term * term -> bool 184 val singt : term -> term HOLset.set 185 val listset : term list -> term HOLset.set 186 val FVs : term -> term HOLset.set 187 val FVLset : term list -> term HOLset.set 188 val ES : term HOLset.set 189 val Teq : term -> bool (* equals the T constant *) 190 val Feq : term -> bool (* equals the F constant *) 191 val tml_eq : term list -> term list -> bool 192 val tmp_eq : term * term -> term * term -> bool 193 val goal_eq : goal -> goal -> bool 194 val goals_eq : goal list -> goal list -> bool 195 val tmem : term -> term list -> bool 196 val memt : term list -> term -> bool (* flip of above *) 197 val tunion : term list -> term list -> term list 198 val tassoc : term -> (term * 'a) list -> 'a 199 val tmx_eq : term * ''a -> term * ''a -> bool 200 val xtm_eq : ''a * term -> ''a * term -> bool 201 202 (* (Type) unification *) 203 val gen_tyvar_sigma : hol_type list -> (hol_type,hol_type) Lib.subst 204 val gen_tyvarify : term -> term 205 val type_unify : hol_type -> hol_type -> (hol_type, hol_type) Lib.subst 206 val sep_type_unify : hol_type -> hol_type -> 207 (hol_type, hol_type) Lib.subst * (hol_type, hol_type) Lib.subst 208 209 210 211end 212