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