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