1signature formalizeUseful = 2sig 3 4 (* GENERAL *) 5 6 type 'a thunk = unit -> 'a 7 type 'a susp = 'a Susp.susp 8 type ppstream = Portable.ppstream 9 type ('a, 'b) maplet = {redex : 'a, residue : 'b} 10 type ('a, 'b) subst = ('a, 'b) Lib.subst 11 12 (* Error handling *) 13 val ERR : string -> string -> exn 14 val BUG : string -> string -> exn 15 val BUG_to_string : exn -> string 16 val err_BUG : string -> exn -> exn 17 18 (* Success and failure *) 19 val assert : bool -> exn -> unit 20 val try : ('a -> 'b) -> 'a -> 'b 21 val total : ('a -> 'b) -> 'a -> 'b option 22 val can : ('a -> 'b) -> 'a -> bool 23 val partial : exn -> ('a -> 'b option) -> 'a -> 'b 24 25 (* Exception combinators *) 26 val nof : 'a -> 'b 27 val allf : 'a -> 'a 28 val thenf : ('a -> 'b) * ('b -> 'c) -> 'a -> 'c 29 val orelsef : ('a -> 'b) * ('a -> 'b) -> 'a -> 'b 30 val tryf : ('a -> 'a) -> 'a -> 'a 31 val repeatf : ('a -> 'a) -> 'a -> 'a 32 val repeatplusf : ('a -> 'a) -> 'a -> 'a 33 val firstf : ('a -> 'b) list -> 'a -> 'b 34 35 (* Combinators *) 36 val A : ('a -> 'b) -> 'a -> 'b 37 val C : ('a -> 'b -> 'c) -> 'b -> 'a -> 'c 38 val I : 'a -> 'a 39 val K : 'a -> 'b -> 'a 40 val N : int -> ('a -> 'a) -> 'a -> 'a 41 val S : ('a -> 'b -> 'c) -> ('a -> 'b) -> 'a -> 'c 42 val W : ('a -> 'a -> 'b) -> 'a -> 'b 43 val oo : ('a -> 'b) * ('c -> 'd -> 'a) -> 'c -> 'd -> 'b 44 45 (* Pairs *) 46 val ## : ('a -> 'b) * ('c -> 'd) -> 'a * 'c -> 'b * 'd 47 val D : 'a -> 'a * 'a 48 val Df : ('a -> 'b) -> ('a * 'a -> 'b * 'b) 49 val fst : 'a * 'b -> 'a 50 val snd : 'a * 'b -> 'b 51 val add_fst : 'a -> 'b -> 'a * 'b 52 val add_snd : 'a -> 'b -> 'b * 'a 53 val curry : ('a * 'b -> 'c) -> 'a -> 'b -> 'c 54 val uncurry : ('a -> 'b -> 'c) -> 'a * 'b -> 'c 55 val equal : ''a -> ''a -> bool 56 val pair_to_string : ('a -> string) -> ('b -> string) -> 'a * 'b -> string 57 58 (* Integers *) 59 val plus : int -> int -> int 60 val multiply : int -> int -> int 61 val succ : int -> int 62 63 (* Strings *) 64 val concat : string -> string -> string 65 val int_to_string : int -> string 66 val string_to_int : string -> int 67 val mk_string_fn : string -> string list -> string 68 val dest_string_fn : string -> string -> string list 69 val is_string_fn : string -> string -> bool 70 71 (* Debugging *) 72 val time_n : int -> ('a -> 'b) -> 'a -> unit 73 val tt : ('a -> 'b) -> 'a -> 'b 74 val tt2 : ('a -> 'b -> 'c) -> 'a -> 'b -> 'c 75 val tt3 : ('a -> 'b -> 'c -> 'd) -> 'a -> 'b -> 'c -> 'd 76 val tt4 : ('a -> 'b -> 'c -> 'd -> 'e) -> 'a -> 'b -> 'c -> 'd -> 'e 77 val ff : ('a -> 'b) -> 'a -> unit 78 val ff2 : ('a -> 'b -> 'c) -> 'a -> 'b -> unit 79 val ff3 : ('a -> 'b -> 'c -> 'd) -> 'a -> 'b -> 'c -> unit 80 val ff4 : ('a -> 'b -> 'c -> 'd -> 'e) -> 'a -> 'b -> 'c -> 'd -> unit 81 82 (* Useful imperative features *) 83 val new_int : unit -> int 84 val random_generator : Random.generator 85 val random_integer : int -> int 86 val random_real : unit -> real 87 val pair_susp : 'a susp -> 'b susp -> ('a * 'b) susp 88 val susp_map : ('a -> 'b) -> 'a susp -> 'b susp 89 90 (* Options *) 91 val is_some : 'a option -> bool 92 val grab : 'a option -> 'a 93 val o_pair : 'a option * 'b -> ('a * 'b) option 94 val pair_o : 'a * 'b option -> ('a * 'b) option 95 val o_pair_o : 'a option * 'b option -> ('a * 'b) option 96 val app_o : ('a -> 'b) -> 'a option -> 'b option 97 val o_app : ('a -> 'b) option -> 'a -> 'b option 98 val o_app_o : ('a -> 'b) option -> 'a option -> 'b option 99 val partial_app_o : ('a -> 'b option) -> 'a option -> 'b option 100 val partial_o_app : ('a -> 'b option) option -> 'a -> 'b option 101 val partial_o_app_o : ('a -> 'b option) option -> 'a option -> 'b option 102 val option_to_list : 'a option -> 'a list 103 104 (* Lists *) 105 val cons : 'a -> 'a list -> 'a list 106 val append : 'a list -> 'a list -> 'a list 107 val wrap : 'a -> 'a list 108 val unwrap : 'a list -> 'a 109 val fold : ('a -> 'b -> 'b) -> 'b -> 'a list -> 'b 110 val trans : ('a -> 'b -> 'b) -> 'b -> 'a list -> 'b 111 val partial_trans : ('a -> 'b -> 'b option) -> 'b -> 'a list -> 'b option 112 val first : ('a -> bool) -> 'a list -> 'a 113 val partial_first : ('a -> 'b option) -> 'a list -> 'b option 114 val forall : ('a -> bool) -> 'a list -> bool 115 val exists : ('a -> bool) -> 'a list -> bool 116 val index : ('a -> bool) -> 'a list -> int 117 val nth : int -> 'a list -> 'a 118 val split_after : int -> 'a list -> 'a list * 'a list 119 val assoc : ''a -> (''a * 'b) list -> 'b 120 val rev_assoc : ''a -> ('b * ''a) list -> 'b 121 val map : ('a -> 'b) -> 'a list -> 'b list 122 val partial_map : ('a -> 'b option) -> 'a list -> 'b list 123 val zip : 'a list -> 'b list -> ('a * 'b) list 124 val zipwith : ('a -> 'b -> 'c) -> 'a list -> 'b list -> 'c list 125 val partial_zipwith : ('a -> 'b -> 'c option) -> 'a list -> 'b list -> 'c list 126 val cart : 'a list -> 'b list -> ('a * 'b) list 127 val cartwith : ('a -> 'b -> 'c) -> 'a list -> 'b list -> 'c list 128 val partial_cartwith : 129 ('a -> 'b -> 'c option) -> 'a list -> 'b list -> 'c list 130 val list_to_string : ('a -> string) -> 'a list -> string 131 132 (* Lists as sets *) 133 val subset : ''a list -> ''a list -> bool 134 val distinct : ''a list -> bool 135 val union2 : ''a list * ''b list -> ''a list * ''b list -> ''a list * ''b list 136 137 (* Permutations and sorting (order functions should always be <=) *) 138 val rotations : 'a list -> ('a * 'a list) list 139 val rotate : int -> ('a list -> 'a * 'a list) 140 val rotate_random : 'a list -> 'a * 'a list 141 val permutations : 'a list -> 'a list list 142 val permute : int list -> 'a list -> 'a list 143 val permute_random : 'a list -> 'a list 144 val min : ('a -> 'a -> bool) -> 'a list -> 'a 145 val merge : ('a -> 'a -> bool) -> 'a list -> 'a list -> 'a list 146 val sort : ('a -> 'a -> bool) -> 'a list -> 'a list 147 val top_min : ('a -> 'a -> bool option) -> 'a list -> 'a * 'a list 148 val top_sort : ('a -> 'a -> bool option) -> 'a list -> 'a list 149 150 (* Sums *) 151 datatype ('a, 'b) sum = LEFT of 'a | RIGHT of 'b 152 153 (* Streams *) 154 datatype ('a) stream = STREAM_NIL | STREAM_CONS of ('a * 'a stream thunk) 155 val stream_null : 'a stream -> bool 156 val dest_stream_cons : 'a stream -> 'a * 'a stream thunk 157 val stream_hd : 'a stream -> 'a 158 val stream_tl : 'a stream -> 'a stream thunk 159 val stream_to_list : 'a stream -> 'a list 160 val stream_append : 'a stream thunk -> 'a stream thunk -> 'a stream thunk 161 val stream_concat : 'a stream thunk list -> 'a stream thunk 162 163 (* Trees *) 164 datatype ('a, 'b) tree = BRANCH of 'a * ('a, 'b) tree list | LEAF of 'b 165 val tree_size : ('a, 'b) tree -> int 166 val tree_fold : ('a -> 'b list -> 'b) -> ('c -> 'b) -> ('a, 'c) tree -> 'b 167 val tree_trans : 168 ('a -> 'b -> 'b) -> ('c -> 'b -> 'd) -> 'b -> ('a, 'c) tree -> 'd list 169 val tree_partial_trans : 170 ('a -> 'b -> 'b option) -> ('c -> 'b -> 'd option) -> 'b -> 171 ('a, 'c) tree -> 'd list 172 173 (* Pretty-printing *) 174 val pp_map : 175 ('a -> 'b) -> (ppstream -> 'b -> unit) -> ppstream -> 'a -> unit 176 val pp_string : ppstream -> string -> unit 177 val pp_unknown : ppstream -> 'a -> unit 178 val pp_int : ppstream -> int -> unit 179 val pp_pair : 180 (ppstream -> 'a -> unit) -> (ppstream -> 'b -> unit) -> 181 (ppstream -> 'a * 'b -> unit) 182 val pp_list : (ppstream -> 'a -> unit) -> (ppstream -> 'a list -> unit) 183 184 (* Substitutions *) 185 val redex : ('a, 'b) maplet -> 'a 186 val residue : ('a, 'b) maplet -> 'b 187 val maplet_map : ('a -> 'c) * ('b -> 'd) -> ('a, 'b) maplet -> ('c, 'd) maplet 188 val find_redex : ''a -> (''a, 'b) subst -> (''a, 'b) maplet 189 val clean_subst : (''a, ''a) subst -> (''a, ''a) subst 190 val subst_vars : ('a, 'b) subst -> 'a list 191 val subst_map : ('a -> 'c) * ('b -> 'd) -> ('a, 'b) subst -> ('c, 'd) subst 192 val redex_map : ('a -> 'c) -> ('a, 'b) subst -> ('c, 'b) subst 193 val residue_map : ('b -> 'c) -> ('a, 'b) subst -> ('a, 'c) subst 194 val is_renaming_subst : ''b list -> ('a, ''b) subst -> bool 195 val invert_renaming_subst : ''b list -> ('a, ''b) subst -> (''b, 'a) subst 196 197 (* HOL *) 198 199 type hol_type = Type.hol_type 200 type term = Term.term 201 type thm = Thm.thm 202 type goal = term list * term 203 type conv = term -> thm 204 type rule = thm -> thm 205 type validation = thm list -> thm 206 type tactic = goal -> goal list * validation 207 type thm_tactic = thm -> tactic 208 type thm_tactical = thm_tactic -> thm_tactic 209 type vars = term list * hol_type list 210 type vterm = vars * term 211 type vthm = vars * thm 212 type type_subst = (hol_type, hol_type) subst 213 type term_subst = (term, term) subst 214 type substitution = term_subst * type_subst 215 type ho_substitution = substitution * thm thunk 216 type raw_substitution = term_subst * (type_subst * hol_type list) 217 type ho_raw_substitution = raw_substitution * thm thunk 218 219 (* General *) 220 val profile : ('a -> 'b) -> 'a -> 'b 221 val parse_with_goal : term frag list -> goal -> term 222 val PARSE_TAC : (term -> tactic) -> term frag list -> tactic 223 224 (* Term/type substitutions *) 225 val empty_subst : substitution 226 val type_inst : type_subst -> hol_type -> hol_type 227 val inst_ty : type_subst -> term -> term 228 val pinst : substitution -> term -> term 229 val type_subst_vars_in_set : type_subst -> hol_type list -> bool 230 val subst_vars_in_set : substitution -> vars -> bool 231 val type_refine_subst : type_subst -> type_subst -> type_subst 232 val refine_subst : substitution -> substitution -> substitution 233 val type_vars_after_subst : hol_type list -> type_subst -> hol_type list 234 val vars_after_subst : vars -> substitution -> vars 235 val type_invert_subst : hol_type list -> type_subst -> type_subst 236 val invert_subst : vars -> substitution -> substitution 237 238 (* Logic variables *) 239 val empty_vars : vars 240 val is_tyvar : vars -> hol_type -> bool 241 val is_tmvar : vars -> term -> bool 242 val type_new_vars : hol_type list -> hol_type list * (type_subst * type_subst) 243 val term_new_vars : term list -> term list * (term_subst * term_subst) 244 val new_vars : vars -> vars * (substitution * substitution) 245 246 (* Bound variables *) 247 val dest_bv : term list -> term -> int 248 val is_bv : term list -> term -> bool 249 val mk_bv : term list -> int -> term 250 251 (* Types *) 252 253 (* Terms *) 254 val type_vars_in_terms : term list -> hol_type list 255 val list_dest_comb : term -> term * term list 256 val conjuncts : term -> term list 257 val dest_unaryop : string -> term -> term 258 val is_unaryop : string -> (term -> bool) 259 val dest_binop : string -> term -> term * term 260 val is_binop : string -> (term -> bool) 261 val dest_imp : term -> term * term 262 val is_imp : term -> bool 263 val dest_foralls : term -> term list * term 264 val mk_foralls : term list * term -> term 265 val spec : term -> term -> term 266 val specl : term list -> term -> term 267 val var_match : vars -> term -> term -> substitution 268 269 (* Theorems *) 270 val FUN_EQ : thm 271 val SET_EQ : thm 272 val hyps : thm list -> term list 273 val LHS : thm -> term 274 val RHS : thm -> term 275 val INST_TY : type_subst -> thm -> thm 276 val PINST : substitution -> thm -> thm 277 278 (* Conversions *) 279 val FIRSTC : conv list -> conv 280 val TRYC : conv -> conv 281 val REPEATPLUSC : conv -> conv 282 val REPEATC_CUTOFF : int -> conv -> conv 283 val DEPTH_ONCE_CONV : conv -> conv 284 val FORALLS_CONV : conv -> conv 285 val CONJUNCT_CONV : conv -> conv 286 val EXACT_CONV : term -> conv 287 val NEGNEG_CONV : conv 288 val FUN_EQ_CONV : conv 289 val SET_EQ_CONV : conv 290 val N_BETA_CONV : int -> conv 291 val EQ_NEG_BOOL_CONV : conv 292 val GENVAR_ALPHA_CONV : conv 293 val GENVAR_BVARS_CONV : conv 294 val ETA_EXPAND_CONV : term -> conv 295 val GENVAR_ETA_EXPAND_CONV : conv 296 297 (* Rules *) 298 val THENR : rule * rule -> rule 299 val REPEATR : rule -> rule 300 val ORELSER : rule * rule -> rule 301 val TRYR : rule -> rule 302 val ALL_RULE : rule 303 val EVERYR : rule list -> rule 304 val FORALL_IMP : rule 305 val EQ_BOOL_INTRO : rule 306 val GENVAR_BVARS : rule 307 val GENVAR_SPEC : rule 308 val GENVAR_SPEC_ALL : rule 309 val REV_CONJUNCTS : thm list -> thm 310 val REORDER_ASMS : term list -> rule 311 val NEW_CONST_RULE : term -> rule 312 val GENVAR_CONST_RULE : rule 313 val ZAP_CONSTS_RULE : rule 314 315 (* Variable theorem (vthm) operations *) 316 val thm_to_vthm : thm -> vthm 317 val vthm_to_thm : vthm -> thm 318 val clean_vthm : vthm -> vthm 319 val var_GENVAR_SPEC : vthm -> vthm 320 val var_CONJUNCTS : vthm -> vthm list 321 val var_MATCH_MP : thm -> vthm -> vthm 322 323 (* Discharging assumptions onto the lhs of an implication *) 324 val DISCH_CONJ_CONV : conv 325 val DISCH_CONJ : term -> rule 326 val DISCH_CONJUNCTS : term list -> rule 327 val DISCH_CONJUNCTS_ALL : rule 328 val DISCH_CONJUNCTS_FILTER : (term -> bool) -> rule 329 val DISCH_CONJ_TAC : tactic 330 val DISCH_CONJUNCTS_TAC : tactic 331 val UNDISCH_CONJ_CONV : conv 332 val UNDISCH_CONJ : rule 333 val UNDISCH_CONJUNCTS : rule 334 val UNDISCH_CONJ_TAC : term -> tactic 335 val UNDISCH_CONJUNCTS_TAC : tactic 336 337 (* Tactics *) 338 val PURE_CONV_TAC : conv -> tactic 339 val ASMLIST_CASES : tactic -> (term -> tactic) -> tactic 340 val POP_ASSUM_TAC : tactic -> tactic 341 val THEN1 : tactic * tactic -> tactic 342 val REVERSE : tactic -> tactic 343 val TRUTH_TAC : tactic 344 val K_TAC : 'a -> tactic 345 val KILL_TAC : tactic 346 val CONJUNCTS_TAC : tactic 347 val FUN_EQ_TAC : tactic 348 val SET_EQ_TAC : tactic 349 val SUFF_TAC : term -> tactic 350 val KNOW_TAC : term -> tactic 351 val CHECK_ASMS_TAC : tactic 352 val EXACT_MP_TAC : thm_tactic 353 val STRONG_CONJ_TAC : tactic 354 val FORWARD_TAC : (thm list -> thm list) -> tactic 355 356 (* Simple CNF conversion *) 357 val CNF_CONV : conv 358 val CNF_RULE : rule 359 val CNF_EXPAND : thm -> thm list 360 val CNF_TAC : tactic 361 362 (* ASM_MATCH_MP_TAC *) 363 val MATCH_MP_DEPTH : int -> thm list -> thm list -> thm list 364 val ASM_MATCH_MP_TAC_N : int -> thm list -> tactic 365 val ASM_MATCH_MP_TAC : thm list -> tactic 366 367end 368