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