1(* ========================================================================= *) 2(* HIGHER-ORDER UTILITY FUNCTIONS *) 3(* Joe Hurd, 10 June 2001 *) 4(* Updated by Chun Tian, 23 August 2018 *) 5(* ========================================================================= *) 6 7structure hurdUtils :> hurdUtils = 8struct 9 10open Susp HolKernel Parse Hol_pp boolLib metisLib bossLib BasicProvers; 11open pairTheory res_quanTools pred_setTheory; (* for RESQ_STRIP_TAC *) 12 13infixr 0 oo THENR ORELSER ## thenf orelsef; 14 15(* obsoleted: 16infix 1 >> |->; 17val op++ = op THEN; 18val op<< = op THENL; 19val op|| = op ORELSE; 20 *) 21 22structure Parse = struct 23 open Parse 24 val (Type,Term) = 25 pred_setTheory.pred_set_grammars 26 |> apsnd ParseExtras.grammar_loose_equality 27 |> parse_from_grammars 28end 29open Parse 30 31(* ------------------------------------------------------------------------- *) 32(* Basic ML datatypes/functions. *) 33(* ------------------------------------------------------------------------- *) 34 35type 'a thunk = unit -> 'a; 36type 'a susp = 'a Susp.susp 37type ('a, 'b) maplet = {redex : 'a, residue : 'b} 38type ('a, 'b) subst = ('a, 'b) Lib.subst 39 40(* Error handling *) 41 42exception BUG_EXN of 43 {origin_structure : string, origin_function : string, message : string}; 44 45val ERR = mk_HOL_ERR "hurdUtils" 46 47(* old definition: 48fun ERR f s = HOL_ERR 49 {origin_structure = "hurdUtils", origin_function = f, message = s}; 50 *) 51 52fun BUG f s = BUG_EXN 53 {origin_structure = "hurdUtils", origin_function = f, message = s}; 54 55fun BUG_to_string (BUG_EXN {origin_structure, origin_function, message}) = 56 ("\nBUG discovered by " ^ origin_structure ^ " at " ^ 57 origin_function ^ ":\n" ^ message ^ "\n") 58 | BUG_to_string _ = raise BUG "print_BUG" "not a BUG_EXN"; 59 60fun err_BUG s (h as HOL_ERR _) = 61 (print (exn_to_string h); BUG s "should never fail") 62 | err_BUG s _ = 63 raise BUG "err_BUG" ("not a HOL_ERR (called from " ^ s ^ ")"); 64 65(* Success and failure *) 66 67fun assert b e = if b then () else raise e; 68fun try f a = f a 69 handle (h as HOL_ERR _) => (print (exn_to_string h); raise h) 70 | (b as BUG_EXN _) => (print (BUG_to_string b); raise b) 71 | e => (print "\ntry: strange exception raised\n"; raise e); 72fun total f x = SOME (f x) handle HOL_ERR _ => NONE; 73fun can f = Option.isSome o total f; 74fun partial (e as HOL_ERR _) f x = (case f x of SOME y => y | NONE => raise e) 75 | partial _ _ _ = raise BUG "partial" "must take a HOL_ERR"; 76 77(* Exception combinators *) 78 79fun nof x = raise ERR "nof" "never succeeds"; 80fun allf x = x; 81fun op thenf (f, g) x = g (f x); 82fun op orelsef (f, g) x = f x handle HOL_ERR _ => g x; 83fun tryf f = f orelsef allf; 84fun repeatf f x = ((f thenf repeatf f) orelsef allf) x; 85fun repeatplusf f = f thenf repeatf f; 86fun firstf [] _ = raise ERR "firstf" "out of combinators" 87 | firstf (f :: rest) x = (f orelsef firstf rest) x; 88 89(* Combinators *) 90 91fun A f x = f x; 92fun C f x y = f y x; 93fun I x = x; 94fun K x y = x; 95fun N 0 _ x = x | N 1 f x = f x | N n f x = N (n - 1) f (f x); 96fun S f g x = f x (g x); 97fun W f x = f x x; 98fun f oo g = fn x => f o (g x); 99 100(* Pairs *) 101 102infix 3 ## 103fun (f ## g) (x, y) = (f x, g y); 104fun D x = (x, x); 105fun Df f = f ## f; 106fun fst (x,_) = x; 107fun snd (_,y) = y; 108fun add_fst x y = (x, y); 109fun add_snd x y = (y, x); 110fun curry f x y = f (x, y); 111fun uncurry f (x, y) = f x y; 112fun equal x y = (x = y); 113 114fun pair_to_string fst_to_string snd_to_string (a, b) = 115 "(" ^ fst_to_string a ^ ", " ^ snd_to_string b ^ ")"; 116 117(* Ints *) 118 119val plus = curry op+; 120val multiply = curry op*; 121val succ = plus 1; 122 123(* Strings *) 124 125val concat = curry op^; 126val int_to_string = Int.toString; 127val string_to_int = 128 partial (ERR "string_to_int" "couldn't convert string") Int.fromString; 129 130fun mk_string_fn name args = name ^ String.concat (map (concat "_") args); 131fun dest_string_fn name s = 132 (case String.tokens (fn #"_" => true | _ => false) s of [] 133 => raise ERR "pure_dest_fn" "empty string" 134 | f::args => (assert (f = name) (ERR "dest_fn" "wrong name"); args)); 135fun is_string_fn name = can (dest_string_fn name); 136 137(* --------------------------------------------------------------------- *) 138(* Tools for debugging. *) 139(* --------------------------------------------------------------------- *) 140 141(* Timing *) 142 143local 144 fun iterate f a 0 = () 145 | iterate f a n = (f a; iterate f a (n - 1)) 146in 147 fun time_n n f a = time (iterate f a) n 148end; 149 150(* Test cases *) 151 152fun tt f = (time o try) f; 153fun tt2 f = tt o f; 154fun tt3 f = tt2 o f; 155fun tt4 f = tt3 o f; 156 157fun ff f = 158 try 159 (fn x => 160 case (time o total o try) f x of NONE => () 161 | SOME _ => raise ERR "ff" "f should not have succeeded!"); 162fun ff2 f = ff o f; 163fun ff3 f = ff2 o f; 164fun ff4 f = ff3 o f; 165 166(* --------------------------------------------------------------------- *) 167(* Useful imperative features. *) 168(* --------------------------------------------------------------------- *) 169 170(* Fresh integers *) 171 172local 173 val counter = ref 0 174in 175 fun new_int () 176 = let val c = !counter 177 val _ = counter := c + 1 178 in c end 179end; 180 181(* Random numbers *) 182 183val random_generator = Random.newgen (); 184fun random_integer n = Random.range (0, n) random_generator; 185fun random_real () = Random.random random_generator; 186 187(* Lazy operations *) 188 189fun pair_susp a b = delay (fn () => (force a, force b)); 190 191fun susp_map f s = delay (fn () => f (force s)); 192 193(* --------------------------------------------------------------------- *) 194(* Options. *) 195(* --------------------------------------------------------------------- *) 196 197val is_some = Option.isSome; 198fun grab (SOME x) = x | grab NONE = raise ERR "grab" "NONE"; 199fun o_pair (SOME x, y) = SOME (x, y) | o_pair _ = NONE; 200fun pair_o (x, SOME y) = SOME (x, y) | pair_o _ = NONE; 201fun o_pair_o (SOME x, SOME y) = SOME (x, y) | o_pair_o _ = NONE; 202val app_o = Option.map; 203fun o_app f = curry (app_o (uncurry A) o o_pair) f 204fun o_app_o f = curry (app_o (uncurry A) o o_pair_o) f 205fun partial_app_o f = Option.join o app_o f; 206fun partial_o_app f = Option.join o o_app f; 207fun partial_o_app_o f = Option.join o o_app_o f; 208fun option_to_list NONE = [] | option_to_list (SOME s) = [s]; 209 210(* --------------------------------------------------------------------- *) 211(* Lists. *) 212(* --------------------------------------------------------------------- *) 213 214fun cons x = curry op:: x; 215fun append l = curry op@ l; 216fun wrap a = [a]; 217fun unwrap [a] = a | unwrap _ = raise ERR "unwrap" "not a singleton list"; 218fun fold _ b [] = b | fold f b (h::t) = f h (fold f b t); 219fun trans _ s [] = s | trans f s (h::t) = trans f (f h s) t; 220fun partial_trans _ s [] = SOME s 221 | partial_trans f s (h::t) = partial_app_o (C (partial_trans f) t) (f h s); 222fun first _ [] = raise ERR "first" "no items satisfy" 223 | first f (h::t) = if f h then h else first f t; 224fun partial_first _ [] = NONE 225 | partial_first f (h::t) = (case f h of NONE => partial_first f t | s => s); 226val forall = List.all; 227val exists = List.exists; 228val index = Lib.index; 229fun nth n l = List.nth (l, n); 230val split_after = Lib.split_after; 231fun assoc x = snd o first (equal x o fst); 232fun rev_assoc x = fst o first (equal x o snd); 233 234val map = List.map; 235val partial_map = List.mapPartial; 236 237fun zip_aux _ [] [] = [] 238 | zip_aux f (x::xs) (y::ys) = f (x, y) (zip_aux f xs ys) 239 | zip_aux _ _ _ = raise ERR "zip" "lists different lengths"; 240fun zip xs ys = zip_aux cons xs ys; 241fun zipwith f xs ys = zip_aux (cons o (uncurry f)) xs ys; 242fun partial_zipwith f xs ys = zip_aux 243 (fn (x, y) => case f x y of NONE => I | SOME s => cons s) xs ys; 244 245fun cart_aux f xs ys = 246 let 247 val xs' = rev xs 248 val ys' = rev ys 249 in 250 trans (fn x => C (trans (fn y => f (x, y))) ys') [] xs' 251 end; 252fun cart xs ys = cart_aux cons xs ys; 253fun cartwith f xs ys = cart_aux (cons o uncurry f) xs ys; 254fun partial_cartwith f xs ys = 255 cart_aux (fn (x, y) => case f x y of NONE => I | SOME s => cons s) xs ys; 256 257fun list_to_string _ [] = "[]" 258 | list_to_string elt_to_string (h :: t) = 259 trans (fn x => fn y => y ^ ", " ^ elt_to_string x) 260 ("[" ^ elt_to_string h) t ^ "]"; 261 262(* --------------------------------------------------------------------- *) 263(* Lists as sets. *) 264(* --------------------------------------------------------------------- *) 265 266fun subset s t = forall (C mem t) s; 267 268fun distinct [] = true 269 | distinct (x :: rest) = not (mem x rest) andalso distinct rest; 270 271fun union2 (a, b) (c, d) = (union a c, union b d); 272 273(* --------------------------------------------------------------------- *) 274(* Rotations, permutations and sorting. *) 275(* --------------------------------------------------------------------- *) 276 277(* Rotations of a list---surprisingly useful *) 278 279local 280 fun rot res _ [] = res 281 | rot res seen (h :: t) = rot ((h, t @ rev seen) :: res) (h :: seen) t 282in 283 fun rotations l = rev (rot [] [] l) 284end; 285 286fun rotate i = nth i o rotations; 287 288fun rotate_random l = rotate (random_integer (length l)) l; 289 290(* Permutations of a list *) 291 292fun permutations [] = [[]] 293 | permutations l = 294 (flatten o map (fn (h, t) => map (cons h) (permutations t)) o rotations) l; 295 296fun permute [] [] = [] 297 | permute (i :: is) (xs as _ :: _) = (op:: o (I ## permute is) o rotate i) xs 298 | permute _ _ = raise ERR "permute" "bad arguments (different lengths)"; 299 300fun permute_random [] = [] 301 | permute_random l = (op:: o (I ## permute_random) o rotate_random) l; 302 303(* Finding the minimal element of a list, wrt some order. *) 304 305local 306 fun min_acc _ best [] = best 307 | min_acc f best (h :: t) = min_acc f (if f best h then best else h) t 308in 309 fun min _ [] = raise ERR "min" "empty list" 310 | min f (h :: t) = min_acc f h t 311end; 312 313(* Merge (for the following merge-sort, but generally useful too). *) 314 315fun merge f [] al' = al' 316 | merge f al [] = al 317 | merge f (a::al) (a'::al') = 318 if f a a' then a::(merge f al (a'::al')) 319 else a'::(merge f (a::al) al'); 320 321(* Order function here should be <= for a stable sort... *) 322(* ...and I think < gives a reverse stable sort (but don't quote me). *) 323fun sort f l = 324 let 325 val n = length l 326 in 327 if n < 2 then l 328 else (uncurry (merge f) o Df (sort f) o split_after (n div 2)) l 329 end; 330 331local 332 fun find_min _ (_, []) = raise ERR "top_min" "no minimal element!" 333 | find_min f (a, x::b) = 334 (assert (f x x <> SOME false) (BUG "top_min" "order function says x > x!"); 335 if forall (fn y => f x y <> SOME false) (a @ b) then (x, a @ b) 336 else find_min f (x::a, b)) 337in 338 fun top_min f l = find_min f ([], l) 339end; 340 341fun top_sort f [] = [] 342 | top_sort f l = 343 let 344 val (x, rest) = top_min f l 345 in 346 x::top_sort f rest 347 end; 348 349(* --------------------------------------------------------------------- *) 350(* Sums. *) 351(* --------------------------------------------------------------------- *) 352 353datatype ('a, 'b) sum = LEFT of 'a | RIGHT of 'b; 354 355(* --------------------------------------------------------------------- *) 356(* Streams. *) 357(* --------------------------------------------------------------------- *) 358 359datatype ('a) stream = STREAM_NIL | STREAM_CONS of ('a * 'a stream thunk); 360 361fun stream_null STREAM_NIL = true 362 | stream_null (STREAM_CONS _) = false; 363 364fun dest_stream_cons STREAM_NIL = raise ERR "dest_stream_cons" "stream is nil" 365 | dest_stream_cons (STREAM_CONS c) = c; 366 367fun stream_hd s = fst (dest_stream_cons s); 368fun stream_tl s = snd (dest_stream_cons s); 369 370local 371 fun to_list res STREAM_NIL = res 372 | to_list res (STREAM_CONS (a, thk)) = to_list (a :: res) (thk ()) 373in 374 fun stream_to_list s = rev (to_list [] s) 375end; 376 377fun stream_append s1 s2 () = 378 (case s1 () of STREAM_NIL => s2 () 379 | STREAM_CONS (a, thk) => STREAM_CONS (a, stream_append thk s2)); 380 381fun stream_concat ss = trans (C stream_append) (K STREAM_NIL) ss; 382 383(* --------------------------------------------------------------------- *) 384(* A generic tree type. *) 385(* --------------------------------------------------------------------- *) 386 387datatype ('a, 'b) tree = BRANCH of 'a * ('a, 'b) tree list | LEAF of 'b; 388 389fun tree_size (LEAF _) = 1 390 | tree_size (BRANCH (_, t)) = trans (plus o tree_size) 0 t; 391 392fun tree_fold f_b f_l (LEAF l) = f_l l 393 | tree_fold f_b f_l (BRANCH (p, s)) = f_b p (map (tree_fold f_b f_l) s); 394 395fun tree_trans f_b f_l state (LEAF l) = [f_l l state] 396 | tree_trans f_b f_l state (BRANCH (p, s)) = 397 flatten (map (tree_trans f_b f_l (f_b p state)) s); 398 399fun tree_partial_trans f_b f_l state (LEAF l) = option_to_list (f_l l state) 400 | tree_partial_trans f_b f_l state (BRANCH (p, s)) = 401 (case f_b p state of NONE => [] 402 | SOME state' => flatten (map (tree_partial_trans f_b f_l state') s)); 403 404(* --------------------------------------------------------------------- *) 405(* Pretty-printing helper-functions. *) 406(* --------------------------------------------------------------------- *) 407 408fun pp_map f pp_a x = pp_a (f x); 409 410val pp_string = PP.add_string 411 412fun pp_unknown _ = pp_string "_"; 413 414fun pp_int i = pp_string (int_to_string i); 415 416open PP 417fun pp_pair pp1 pp2 = 418 fn (a, b) => block CONSISTENT 1 [ 419 add_string "(", pp1 a, add_string ",", 420 add_break (1, 0), pp2 b, add_string ")" 421 ] 422 423fun pp_list pp = 424 fn l => block INCONSISTENT 1 ( 425 add_string "[" :: 426 pr_list pp [add_string ",", add_break(1,0)] l @ 427 [add_string "]"] 428 ) 429 430(* --------------------------------------------------------------------- *) 431(* Substitution operations. *) 432(* --------------------------------------------------------------------- *) 433 434fun redex {redex, residue = _} = redex; 435fun residue {redex = _, residue} = residue; 436fun find_redex r = first (fn rr as {redex, residue} => r = redex); 437fun tfind_redex r = first (fn rr as {redex, residue} => r ~~ redex); 438fun clean_subst s = filter (fn {redex, residue} => redex <> residue) s; 439fun clean_tsubst s = filter (fn {redex, residue} => redex !~ residue) s; 440fun subst_vars sub = map redex sub; 441fun maplet_map (redf, resf) {redex, residue} = (redf redex |-> resf residue); 442fun subst_map fg = map (maplet_map fg); 443fun redex_map f = subst_map (f, I); 444fun residue_map f = subst_map (I, f); 445 446fun tdistinct tml = HOLset.numItems(listset tml) = length tml 447 448fun is_renaming_tsubst vars sub = 449 let 450 val residues = map residue sub 451 in 452 forall (C tmem vars) residues andalso tdistinct residues 453 end; 454 455fun is_renaming_subst vars sub = 456 let 457 val residues = map residue sub 458 in 459 forall (C mem vars) residues andalso distinct residues 460 end; 461 462fun invert_renaming_subst vars sub = 463 let 464 val _ = 465 assert (is_renaming_subst vars sub) 466 (ERR "invert_renaming_subst" "not a renaming subst, so not invertible") 467 fun inv {redex, residue} = residue |-> redex 468 in 469 map inv sub 470 end; 471 472(* --------------------------------------------------------------------- *) 473(* HOL-specific functions. *) 474(* --------------------------------------------------------------------- *) 475 476type hol_type = Type.hol_type 477type term = Term.term 478type thm = Thm.thm 479type goal = term list * term 480type conv = term -> thm 481type rule = thm -> thm 482type validation = thm list -> thm 483type tactic = goal -> goal list * validation 484type thm_tactic = thm -> tactic 485type vars = term list * hol_type list 486type vterm = vars * term 487type vthm = vars * thm 488type type_subst = (hol_type, hol_type) subst 489type term_subst = (term, term) subst 490type substitution = (term, term) subst * (hol_type, hol_type) subst 491type ho_substitution = substitution * thm thunk 492type raw_substitution = (term_subst * term set) * (type_subst * hol_type list) 493type ho_raw_substitution = raw_substitution * thm thunk 494 495(* --------------------------------------------------------------------- *) 496(* General *) 497(* --------------------------------------------------------------------- *) 498 499(* A profile function counting both time and primitive inferences. *) 500 501fun profile f a = 502 let 503 val m = Count.mk_meter () 504 val i = #prims(Count.read m) 505 val t = Time.now () 506 val res = f a 507 val t' = Time.now () 508 val i' = #prims(Count.read m) 509 val _ = print ("Time taken: " ^ Time.toString (Time.-(t', t)) ^ ".\n" 510 ^ "Primitive inferences: " ^ Int.toString (i' - i) ^ ".\n") 511 in 512 res 513 end; 514 515(* Parsing in the context of a goal, a la the Q library. *) 516 517fun parse_with_goal t (asms, g) = 518 let 519 val ctxt = free_varsl (g::asms) 520 in 521 Parse.parse_in_context ctxt t 522 end; 523 524val PARSE_TAC = fn tac => fn q => W (tac o parse_with_goal q); 525 526(* --------------------------------------------------------------------- *) 527(* Term/type substitutions. *) 528(* --------------------------------------------------------------------- *) 529 530val empty_subst = ([], []) : substitution; 531 532val type_inst = type_subst; 533val inst_ty = inst; 534fun pinst (tm_sub, ty_sub) = subst tm_sub o inst_ty ty_sub; 535 536fun type_subst_vars_in_set (sub : type_subst) vars = 537 subset (subst_vars sub) vars; 538 539fun subst_vars_in_set ((tm_sub, ty_sub) : substitution) (tm_vars, ty_vars) = 540 type_subst_vars_in_set ty_sub ty_vars andalso 541 HOLset.isSubset (listset (subst_vars tm_sub), 542 listset (map (inst_ty ty_sub) tm_vars)); 543 544(* Note: cyclic substitutions are right out! *) 545fun type_refine_subst ty1 ty2 : (hol_type, hol_type) subst = 546 ty2 @ (clean_subst o residue_map (type_inst ty2)) ty1; 547 548fun refine_subst (tm1, ty1) (tm2, ty2) = 549 (tm2 @ (clean_tsubst o subst_map (inst_ty ty2, pinst (tm2, ty2))) tm1, 550 type_refine_subst ty1 ty2); 551 552(* 553refine_subst 554([(``x:'b list`` |-> ``CONS (y:'b list) []``)], 555 [(``:'a`` |-> ``:'b list``)]) 556([(``y:real list`` |-> ``[0:real]``)], 557 [(``:'b`` |-> ``:real``)]); 558 559refine_subst 560([(``x:'b list`` |-> ``[y : 'b]``)], 561 [(``:'a`` |-> ``:'b``)]) 562([(``y:'a`` |-> ``z:'a``)], 563 [(``:'b`` |-> ``:'a``)]); 564*) 565 566fun type_vars_after_subst vars (sub : (hol_type, hol_type) subst) = 567 subtract vars (subst_vars sub); 568 569fun vars_after_subst (tm_vars, ty_vars) (tm_sub, ty_sub) = 570 (op_set_diff aconv (map (inst_ty ty_sub) tm_vars) (subst_vars tm_sub), 571 type_vars_after_subst ty_vars ty_sub); 572 573fun type_invert_subst vars (sub : (hol_type, hol_type) subst) = 574 invert_renaming_subst vars sub; 575 576fun invert_subst (tm_vars, ty_vars) (tm_sub, ty_sub) = 577 let 578 val _ = 579 assert (is_renaming_tsubst tm_vars tm_sub) 580 (ERR "invert_subst" "not a renaming term subst") 581 val ty_sub' = type_invert_subst ty_vars ty_sub 582 fun inv {redex, residue} = 583 inst_ty ty_sub' residue |-> inst_ty ty_sub' redex 584 in 585 (map inv tm_sub, ty_sub') 586 end; 587 588(* --------------------------------------------------------------------- *) 589(* Logic variables. *) 590(* --------------------------------------------------------------------- *) 591 592val empty_vars = ([], []) : vars; 593fun is_tyvar ((_, tyvars) : vars) ty = is_vartype ty andalso mem ty tyvars; 594fun is_tmvar ((tmvars, _) : vars) tm = is_var tm andalso tmem tm tmvars; 595 596fun type_new_vars (vars : hol_type list) = 597 let 598 val gvars = map (fn _ => gen_tyvar ()) vars 599 val old_to_new = zipwith (curry op|->) vars gvars 600 val new_to_old = zipwith (curry op|->) gvars vars 601 in 602 (gvars, (old_to_new, new_to_old)) 603 end; 604 605fun term_new_vars vars = 606 let 607 val gvars = map (genvar o type_of) vars 608 val old_to_new = zipwith (curry op|->) vars gvars 609 val new_to_old = zipwith (curry op|->) gvars vars 610 in 611 (gvars, (old_to_new, new_to_old)) 612 end; 613 614fun new_vars (tm_vars, ty_vars) = 615 let 616 val (ty_gvars, (ty_old_to_new, ty_new_to_old)) = type_new_vars ty_vars 617 val (tm_gvars, (tm_old_to_new, tm_new_to_old)) = term_new_vars tm_vars 618 val old_to_new = refine_subst (tm_old_to_new, []) ([], ty_old_to_new) 619 val new_to_old = (tm_new_to_old, ty_new_to_old) 620 in 621 ((map (inst_ty ty_old_to_new) tm_gvars, ty_gvars), (old_to_new, new_to_old)) 622 end; 623 624val vars_eq : vars eqf = pair_eq tml_eq equal 625fun vars_union (tml1, tyl1) (tml2, tyl2) = 626 (tunion tml1 tml2, union tyl1 tyl2) 627 628(* ------------------------------------------------------------------------- *) 629(* Bound variables. *) 630(* ------------------------------------------------------------------------- *) 631 632fun dest_bv bvs tm = 633 let 634 val _ = assert (is_var tm) (ERR "dest_bv" "not a var") 635 in 636 index (aconv tm) bvs 637 end; 638fun is_bv bvs = can (dest_bv bvs); 639fun mk_bv bvs n : term = nth n bvs; 640 641(* --------------------------------------------------------------------- *) 642(* Types. *) 643(* --------------------------------------------------------------------- *) 644 645(* --------------------------------------------------------------------- *) 646(* Terms. *) 647(* --------------------------------------------------------------------- *) 648 649val type_vars_in_terms = trans (union o type_vars_in_term) []; 650 651local 652 fun dest (tm, args) = 653 let 654 val (a, b) = dest_comb tm 655 in 656 (a, b::args) 657 end 658in 659 fun list_dest_comb tm = repeat dest (tm, []) 660end; 661 662fun conjuncts tm = 663 if is_conj tm then 664 let 665 val (a, b) = dest_conj tm 666 in 667 a::(conjuncts b) 668 end 669 else [tm]; 670 671fun dest_unaryop c tm = 672 let 673 val (a, b) = dest_comb tm 674 val _ = assert (fst (dest_const a) = c) 675 (ERR "dest_unaryop" "different const") 676 in 677 b 678 end; 679fun is_unaryop c = can (dest_unaryop c); 680 681fun dest_binop c tm = 682 let 683 val (a, b) = dest_comb tm 684 in 685 (dest_unaryop c a, b) 686 end; 687fun is_binop c = can (dest_binop c); 688 689val dest_imp = dest_binop "==>"; 690val is_imp = can dest_imp; 691 692local 693 fun dest (vs, tm) = (C cons vs ## I) (dest_forall tm) 694in 695 val dest_foralls = repeat dest o add_fst [] 696end; 697val mk_foralls = uncurry (C (trans (curry mk_forall))); 698 699fun spec s tm = 700 let 701 val (v, body) = dest_forall tm 702 in 703 subst [v |-> s] body 704 end; 705 706val specl = C (trans spec); 707 708fun var_match vars tm tm' = 709 let 710 val sub = match_term tm tm' 711 val _ = assert (subst_vars_in_set sub vars) 712 (ERR "var_match" "subst vars not contained in set") 713 in 714 sub 715 end; 716 717(* --------------------------------------------------------------------- *) 718(* Thms. *) 719(* --------------------------------------------------------------------- *) 720 721val FUN_EQ = prove (``!f g. (f = g) = (!x. f x = g x)``, PROVE_TAC [EQ_EXT]); 722val SET_EQ = prove (``!s t. (s = t) = (!x. x IN s = x IN t)``, 723 PROVE_TAC [SPECIFICATION, FUN_EQ]); 724 725val hyps = foldl (fn (h,t) => tunion (hyp h) t) []; 726 727val LHS = lhs o concl; 728val RHS = rhs o concl; 729 730local 731 fun fake_asm_op r th = 732 let 733 val h = rev (hyp th) 734 in 735 (N (length h) UNDISCH o r o C (foldl (uncurry DISCH)) h) th 736 end 737in 738 val INST_TY = fake_asm_op o INST_TYPE; 739 val PINST = fake_asm_op o INST_TY_TERM; 740end; 741 742(* --------------------------------------------------------------------- *) 743(* Conversions. *) 744(* --------------------------------------------------------------------- *) 745 746(* Conversionals *) 747 748fun FIRSTC [] tm = raise ERR "FIRSTC" "ran out of convs" 749 | FIRSTC (c::cs) tm = (c ORELSEC FIRSTC cs) tm; 750 751fun TRYC c = QCONV (c ORELSEC ALL_CONV); 752 753fun REPEATPLUSC c = c THENC REPEATC c; 754 755fun REPEATC_CUTOFF 0 _ _ = raise ERR "REPEATC_CUTOFF" "cut-off reached" 756 | REPEATC_CUTOFF n c tm = 757 (case (SOME (QCONV c tm) handle HOL_ERR _ => NONE) of NONE 758 => QCONV ALL_CONV tm 759 | SOME eq_th => TRANS eq_th (REPEATC_CUTOFF (n - 1) c (RHS eq_th))); 760 761(* A conversional like DEPTH_CONV, but applies the argument conversion *) 762(* at most once to each subterm *) 763 764fun DEPTH_ONCE_CONV c tm = QCONV (SUB_CONV (DEPTH_ONCE_CONV c) THENC TRYC c) tm; 765 766fun FORALLS_CONV c tm = 767 QCONV (if is_forall tm then RAND_CONV (ABS_CONV (FORALLS_CONV c)) else c) tm; 768 769fun CONJUNCT_CONV c tm = 770 QCONV 771 (if is_conj tm then RATOR_CONV (RAND_CONV c) THENC RAND_CONV (CONJUNCT_CONV c) 772 else c) tm; 773 774(* Conversions *) 775 776fun EXACT_CONV exact tm = QCONV (if tm ~~ exact then ALL_CONV else NO_CONV) tm; 777 778val NEGNEG_CONV = REWR_CONV (CONJUNCT1 NOT_CLAUSES); 779 780val FUN_EQ_CONV = REWR_CONV FUN_EQ; 781val SET_EQ_CONV = REWR_CONV SET_EQ; 782 783fun N_BETA_CONV 0 = QCONV ALL_CONV 784 | N_BETA_CONV n = RATOR_CONV (N_BETA_CONV (n - 1)) THENC TRYC BETA_CONV; 785 786local 787 val EQ_NEG_T = PROVE [] ``!a. (~a = T) = (a = F)`` 788 val EQ_NEG_F = PROVE [] ``!a. (~a = F) = (a = T)`` 789 val EQ_NEG_T_CONV = REWR_CONV EQ_NEG_T 790 val EQ_NEG_F_CONV = REWR_CONV EQ_NEG_F 791in 792 val EQ_NEG_BOOL_CONV = QCONV (EQ_NEG_T_CONV ORELSEC EQ_NEG_F_CONV); 793end; 794 795val GENVAR_ALPHA_CONV = W (ALPHA_CONV o genvar o type_of o bvar); 796val GENVAR_BVARS_CONV = DEPTH_ONCE_CONV GENVAR_ALPHA_CONV; 797 798fun ETA_EXPAND_CONV v tm = SYM (ETA_CONV (mk_abs (v, mk_comb (tm, v)))); 799val GENVAR_ETA_EXPAND_CONV = 800 W (ETA_EXPAND_CONV o genvar o fst o dom_rng o type_of); 801 802(* --------------------------------------------------------------------- *) 803(* Rules. *) 804(* --------------------------------------------------------------------- *) 805 806fun op THENR (r1, r2) (th:thm) :thm = r2 (r1 th:thm); 807fun REPEATR r (th:thm) = REPEATR r (r th) handle HOL_ERR _ => th; 808fun op ORELSER (r1, r2) (th:thm):thm = r1 th handle HOL_ERR _ => r2 th; 809fun TRYR r = r ORELSER I; 810val ALL_RULE : rule = I; 811 812fun EVERYR [] = ALL_RULE 813 | EVERYR (r::rest) = r THENR EVERYR rest; 814 815local 816 val fir = prove 817 (``(!(x:'a). P x ==> Q x) ==> ((?x. P x) ==> (?x. Q x))``, PROVE_TAC []) 818in 819 val FORALL_IMP = HO_MATCH_MP fir 820end; 821 822val EQ_BOOL_INTRO = EQT_INTRO THENR CONV_RULE (REPEATC EQ_NEG_BOOL_CONV); 823 824val GENVAR_BVARS = CONV_RULE GENVAR_BVARS_CONV; 825 826val GENVAR_SPEC = 827 CONV_RULE (RAND_CONV GENVAR_ALPHA_CONV) THENR (snd o SPEC_VAR); 828 829val GENVAR_SPEC_ALL = REPEATR GENVAR_SPEC; 830 831local 832 fun mk th [] = th 833 | mk th (c :: rest) = mk (CONJ c th) rest 834 handle HOL_ERR _ => raise BUG "REV_CONJUNCTS" "panic" 835in 836 fun REV_CONJUNCTS [] = raise ERR "REV_CONJUNCTS" "empty list" 837 | REV_CONJUNCTS (th :: rest) = mk th rest 838end; 839 840fun REORDER_ASMS asms th0 = 841 let 842 val th1 = foldr (fn (h,t) => DISCH h t) th0 asms 843 val th2 = funpow (length asms) UNDISCH th1 844 in 845 th2 846 end; 847 848local 849 fun dest_c tm = 850 if is_comb tm then 851 let 852 val (a, b) = dest_comb tm 853 in 854 (I ## cons b) (dest_c a) 855 end 856 else (tm, []) 857 858 fun comb_beta eq_th x = 859 CONV_RULE (RAND_CONV BETA_CONV) (MK_COMB (eq_th, REFL x)) 860in 861 fun NEW_CONST_RULE cvar_lvars th = 862 let 863 val (cvar, lvars) = (I ## rev) (dest_c cvar_lvars) 864 val sel_th = 865 CONV_RULE (RATOR_CONV (REWR_CONV EXISTS_DEF) THENC BETA_CONV) th 866 val pred = rator (concl sel_th) 867 val def_tm = list_mk_abs (lvars, rand (concl sel_th)) 868 val def_th = ASSUME (mk_eq (cvar, def_tm)) 869 val eq_th = MK_COMB (REFL pred, trans (C comb_beta) def_th lvars) 870 in 871 CONV_RULE BETA_CONV (EQ_MP (SYM eq_th) sel_th) 872 end 873end; 874 875val GENVAR_CONST_RULE = 876 W (NEW_CONST_RULE o genvar o type_of o bvar o rand o concl); 877 878local 879 fun zap _ _ [] = raise ERR "zap" "fresh out of asms" 880 | zap th checked (asm::rest) = 881 if is_eq asm then 882 let 883 val (v, def) = dest_eq asm 884 in 885 if is_var v andalso all (not o free_in v) (checked @ rest) then 886 MP (SPEC def (GEN v (DISCH asm th))) (REFL def) 887 else zap th (asm::checked) rest 888 end 889 else zap th (asm::checked) rest 890in 891 val ZAP_CONSTS_RULE = repeat (fn th => zap th [concl th] (hyp th)) 892end; 893 894(* ------------------------------------------------------------------------- *) 895(* vthm operations *) 896(* ------------------------------------------------------------------------- *) 897 898fun thm_to_vthm th = 899 let 900 val tm = concl th 901 902 val c_tyvars = type_vars_in_term tm 903 val h_tyvars = type_vars_in_terms (hyp th) 904 val f_tyvars = subtract c_tyvars h_tyvars 905 val (f_tmvars, _) = dest_foralls tm 906 val f_vars = (f_tmvars, f_tyvars) 907 908 val (vars, (sub, _)) = new_vars f_vars 909 in 910 (vars, PINST sub (REPEATR (snd o SPEC_VAR) th)) 911 end; 912 913fun vthm_to_thm (((vars, _), th) : vthm) = GENL vars th; 914 915fun clean_vthm ((tm_vars, ty_vars), th) = 916 let 917 val tms = concl th :: hyp th 918 val ty_vars' = intersect (type_vars_in_terms tms) ty_vars 919 val tm_vars' = op_intersect aconv (free_varsl tms) tm_vars 920 in 921 ((tm_vars', ty_vars'), ZAP_CONSTS_RULE th) 922 end; 923 924fun var_GENVAR_SPEC ((tm_vars, ty_vars), th) : vthm = 925 let 926 val v = (genvar o type_of o fst o dest_forall o concl) th 927 in 928 ((v :: tm_vars, ty_vars), SPEC v th) 929 end; 930 931fun var_CONJUNCTS (vars, th) : vthm list = 932 map (add_fst vars) (CONJUNCTS th); 933 934fun var_MATCH_MP th : vthm -> vthm = (I ## MATCH_MP th); 935 936(* --------------------------------------------------------------------- *) 937(* Discharging assumptions on to the lhs of an implication: *) 938(* DISCH_CONJ a : [a] UNION A |- P ==> Q |-> A |- a /\ P ==> Q *) 939(* UNDISCH_CONJ : A |- a /\ P ==> Q |-> [a] UNION A |- P ==> Q *) 940(* --------------------------------------------------------------------- *) 941 942val DISCH_CONJ_CONV = REWR_CONV AND_IMP_INTRO; 943fun DISCH_CONJ a th = CONV_RULE DISCH_CONJ_CONV (DISCH a th); 944fun DISCH_CONJUNCTS [] _ = raise ERR "DISCH_CONJ" "no assumptions!" 945 | DISCH_CONJUNCTS (a::al) th = foldl (uncurry DISCH_CONJ) (DISCH a th) al; 946fun DISCH_CONJUNCTS_ALL th = DISCH_CONJUNCTS (hyp th) th; 947fun DISCH_CONJUNCTS_FILTER f th = DISCH_CONJUNCTS (filter f (hyp th)) th; 948fun UNDISCH_CONJ_TAC a = UNDISCH_TAC a >> CONV_TAC DISCH_CONJ_CONV; 949val UNDISCH_CONJUNCTS_TAC = 950 POP_ASSUM MP_TAC >> REPEAT (POP_ASSUM MP_TAC >> CONV_TAC DISCH_CONJ_CONV); 951 952val UNDISCH_CONJ_CONV = REWR_CONV (GSYM AND_IMP_INTRO) 953val UNDISCH_CONJ = CONV_RULE UNDISCH_CONJ_CONV THENR UNDISCH 954val UNDISCH_CONJUNCTS = REPEATR UNDISCH_CONJ THENR UNDISCH 955val DISCH_CONJ_TAC = CONV_TAC UNDISCH_CONJ_CONV >> DISCH_TAC 956val DISCH_CONJUNCTS_TAC = REPEAT DISCH_CONJ_TAC >> DISCH_TAC 957 958(* --------------------------------------------------------------------- *) 959(* Tacticals. *) 960(* --------------------------------------------------------------------- *) 961 962fun PURE_CONV_TAC conv :tactic = fn (asms,g) => 963 let 964 val eq_th = QCONV conv g 965 in 966 ([(asms, RHS eq_th)], EQ_MP (SYM eq_th) o hd) 967 end; 968 969fun ASMLIST_CASES (t1:tactic) _ (g as ([], _)) = t1 g 970 | ASMLIST_CASES _ t2 (g as (x::_, _)) = t2 x g; 971 972fun POP_ASSUM_TAC tac = 973 ASMLIST_CASES tac 974 (K (UNDISCH_CONJUNCTS_TAC 975 >> tac 976 >> TRY (DISCH_THEN (EVERY o map ASSUME_TAC o CONJUNCTS)))); 977 978(* --------------------------------------------------------------------- *) 979(* Tactics. *) 980(* --------------------------------------------------------------------- *) 981 982val TRUTH_TAC = ACCEPT_TAC TRUTH; 983 984val S_TAC = rpt (POP_ASSUM MP_TAC) >> rpt RESQ_STRIP_TAC; 985val Strip = S_TAC; 986 987fun K_TAC _ = ALL_TAC; 988 989val KILL_TAC = POP_ASSUM_LIST K_TAC; 990 991fun CONJUNCTS_TAC g = TRY (CONJ_TAC >| [ALL_TAC, CONJUNCTS_TAC]) g; 992 993val FUN_EQ_TAC = CONV_TAC (CHANGED_CONV (ONCE_DEPTH_CONV FUN_EQ_CONV)); 994val SET_EQ_TAC = CONV_TAC (CHANGED_CONV (ONCE_DEPTH_CONV SET_EQ_CONV)); 995 996local 997 val th1 = (prove (``!t. T ==> (F ==> t)``, PROVE_TAC [])) 998in 999 val CHECK_ASMS_TAC :tactic = 1000 REPEAT (PAT_ASSUM T K_TAC) 1001 >> REPEAT (PAT_ASSUM F (fn th => MP_TAC th >> MATCH_MP_TAC th1)) 1002end; 1003 1004val Cond = 1005 MATCH_MP_TAC (PROVE [] ``!a b c. a /\ (b ==> c) ==> ((a ==> b) ==> c)``) 1006 >> CONJ_TAC; 1007 1008val Rewr = DISCH_THEN (REWRITE_TAC o wrap); 1009val Rewr' = DISCH_THEN (ONCE_REWRITE_TAC o wrap); 1010 1011(* --------------------------------------------------------------------- *) 1012(* EXACT_MP_TAC : thm -> tactic *) 1013(* *) 1014(* If the goal is (asms, g) then the supplied theorem should be of the *) 1015(* form [..] |- g' ==> g *) 1016(* *) 1017(* The tactic returns one subgoal of the form (asms, g') *) 1018(* --------------------------------------------------------------------- *) 1019 1020fun EXACT_MP_TAC mp_th :tactic = 1021 let 1022 val g' = fst (dest_imp (concl mp_th)) 1023 in 1024 fn (asms, g) => ([(asms, g')], MP mp_th o hd) 1025 end; 1026 1027(* --------------------------------------------------------------------- *) 1028(* STRONG_CONJ_TAC : tactic *) 1029(* *) 1030(* If the goal is (asms, A /\ B) then the tactic returns two subgoals of *) 1031(* the form (asms, A) and (asms, A ==> B) *) 1032(* --------------------------------------------------------------------- *) 1033 1034local 1035 val th = prove (``!a b. a /\ (a ==> b) ==> a /\ b``, PROVE_TAC []) 1036in 1037 val STRONG_CONJ_TAC :tactic = MATCH_MP_TAC th >> CONJ_TAC 1038end; 1039 1040val STRONG_DISJ_TAC = CONV_TAC (REWR_CONV (GSYM IMP_DISJ_THM)) >> STRIP_TAC; 1041 1042(* --------------------------------------------------------------------- *) 1043(* FORWARD_TAC : (thm list -> thm list) -> tactic *) 1044(* *) 1045(* Here is what happens when *) 1046(* FORWARD_TAC f *) 1047(* is applied to the goal *) 1048(* (asms, g). *) 1049(* *) 1050(* 1. It calls the supplied inference function with the assumptions *) 1051(* to obtain a list of theorems. *) 1052(* ths = f (map ASSUME asms) *) 1053(* IMPORTANT: The assumptions of the theorems in ths must be either *) 1054(* in asms, or `definitions' of the form `new_var = body`. *) 1055(* *) 1056(* 2. It returns one subgoal with the following form: *) 1057(* (map concl ths, g) *) 1058(* i.e., the same goal, and a new assumption list that logically *) 1059(* follows from asms. *) 1060(* *) 1061(* --------------------------------------------------------------------- *) 1062 1063fun forward_just ths th0 = 1064 let 1065 val th1 = foldr (fn (h,t) => DISCH (concl h) t) th0 ths 1066 val th2 = foldl (fn (h,t) => MP t h) th1 ths 1067 in 1068 th2 1069 end 1070 1071fun FORWARD_TAC f (asms, g:term) = 1072 let 1073 val ths = f (map ASSUME asms) 1074 in 1075 ([(map concl ths, g)], 1076 fn [th] => (REORDER_ASMS asms o ZAP_CONSTS_RULE o forward_just ths) th 1077 | _ => raise BUG "FORWARD_TAC" "justification function panic") 1078 end; 1079 1080val Know = Q_TAC KNOW_TAC 1081val Suff = Q_TAC SUFF_TAC 1082val POP_ORW = POP_ASSUM (fn thm => ONCE_REWRITE_TAC [thm]); 1083 1084(* --------------------------------------------------------------------- *) 1085(* A simple-minded CNF conversion. *) 1086(* --------------------------------------------------------------------- *) 1087 1088local 1089 open simpLib 1090in 1091 val EXPAND_COND_CONV = 1092 QCONV (SIMP_CONV (pureSimps.pure_ss ++ boolSimps.COND_elim_ss) []) 1093end 1094 1095local 1096 val EQ_IFF = prove 1097 (``!a b. ((a:bool) = b) = ((a ==> b) /\ (b ==> a))``, 1098 BasicProvers.PROVE_TAC []) 1099in 1100 val EQ_IFF_CONV = QCONV (PURE_REWRITE_CONV [EQ_IFF]) 1101end; 1102 1103local 1104 val IMP_DISJ = prove 1105 (``!a b. ((a:bool) ==> b) = ~a \/ b``, 1106 BasicProvers.PROVE_TAC []) 1107in 1108 val IMP_DISJ_CONV = QCONV (PURE_REWRITE_CONV [IMP_DISJ]) 1109end; 1110 1111local 1112 val NEG_NEG = CONJUNCT1 NOT_CLAUSES 1113 val DE_MORGAN1 1114 = CONJUNCT1 (CONV_RULE (DEPTH_CONV FORALL_AND_CONV) DE_MORGAN_THM) 1115 val DE_MORGAN2 1116 = CONJUNCT2 (CONV_RULE (DEPTH_CONV FORALL_AND_CONV) DE_MORGAN_THM) 1117in 1118 val NNF_CONV = (QCONV o REPEATC o CHANGED_CONV) 1119 (REWRITE_CONV [NEG_NEG, DE_MORGAN1, DE_MORGAN2] 1120 THENC DEPTH_CONV (NOT_EXISTS_CONV ORELSEC NOT_FORALL_CONV)) 1121end; 1122 1123val EXISTS_OUT_CONV = (QCONV o REPEATC o CHANGED_CONV o DEPTH_CONV) 1124 (LEFT_AND_EXISTS_CONV 1125 ORELSEC RIGHT_AND_EXISTS_CONV 1126 ORELSEC LEFT_OR_EXISTS_CONV 1127 ORELSEC RIGHT_OR_EXISTS_CONV 1128 ORELSEC CHANGED_CONV SKOLEM_CONV); 1129 1130val ANDS_OUT_CONV = (QCONV o REPEATC o CHANGED_CONV o DEPTH_CONV) 1131 (FORALL_AND_CONV 1132 ORELSEC REWR_CONV LEFT_OR_OVER_AND 1133 ORELSEC REWR_CONV RIGHT_OR_OVER_AND) 1134 1135val FORALLS_OUT_CONV = (QCONV o REPEATC o CHANGED_CONV o DEPTH_CONV) 1136 (LEFT_OR_FORALL_CONV 1137 ORELSEC RIGHT_OR_FORALL_CONV); 1138 1139val CNF_CONV = 1140 QCONV 1141 (DEPTH_CONV BETA_CONV 1142 THENC EXPAND_COND_CONV 1143 THENC EQ_IFF_CONV 1144 THENC IMP_DISJ_CONV 1145 THENC NNF_CONV 1146 THENC EXISTS_OUT_CONV 1147 THENC ANDS_OUT_CONV 1148 THENC FORALLS_OUT_CONV 1149 THENC REWRITE_CONV [GSYM DISJ_ASSOC, GSYM CONJ_ASSOC]); 1150 1151val CNF_RULE = CONV_RULE CNF_CONV; 1152 1153val CNF_EXPAND = CONJUNCTS o repeat GENVAR_CONST_RULE o CNF_RULE; 1154 1155val CNF_TAC = CCONTR_TAC THEN FORWARD_TAC (flatten o map CNF_EXPAND); 1156 1157(* --------------------------------------------------------------------- *) 1158(* ASM_MATCH_MP_TAC: adding MP-consequences to the assumption list. *) 1159(* Does less than (EVERY (map ASSUME_TAC ths) >> RES_TAC). *) 1160(* --------------------------------------------------------------------- *) 1161 1162local 1163 val is_mp = is_imp o snd o dest_foralls o concl; 1164 1165 fun initialize mp_th = 1166 let 1167 val (vars, (asm, body)) = ((rev ## dest_imp) o dest_foralls o concl) mp_th 1168 val asms = conjuncts asm 1169 in 1170 case asms of [a] => ([], [mp_th]) 1171 | _ => 1172 let 1173 val mp_th' = (SPEC_ALL THENR UNDISCH_CONJUNCTS) mp_th 1174 val rots = rotations asms 1175 fun f (asm, rest) = 1176 (DISCH_CONJUNCTS rest THENR DISCH asm THENR GENL vars) mp_th' 1177 in 1178 (map f rots, []) 1179 end 1180 end 1181 1182 fun initialize_collect (m, s) th = 1183 let 1184 val (mx, sx) = initialize th 1185 in 1186 (mx @ m, sx @ s) 1187 end 1188 1189 val initializel = trans (C initialize_collect) 1190 1191 fun match1 (multi, single) th = 1192 let 1193 val do_match = partial_map (fn x => total (MATCH_MP x) th) 1194 in 1195 (do_match multi, do_match single) 1196 end 1197 1198 fun add_thm th (concls, ths) = 1199 let 1200 val tm = concl th 1201 in 1202 if tmem tm concls then (concls, ths) else (tm :: concls, th :: ths) 1203 end 1204 1205 fun clean_add_thms ths = snd o trans add_thm (map concl ths, ths) 1206 1207 fun match 0 _ ths = ths 1208 | match n state ths = 1209 let 1210 val (m_res, s_res) = (Df flatten o unzip o map (match1 state)) ths 1211 val state' = initializel state m_res 1212 val s_res' = clean_add_thms ths s_res 1213 in 1214 match (n - 1) state' s_res' 1215 end; 1216in 1217 fun MATCH_MP_DEPTH n = 1218 match n o initializel ([], []) o filter is_mp 1219end; 1220 1221fun ASM_MATCH_MP_TAC_N depth ths = 1222 POP_ASSUM_LIST 1223 (EVERY o map ASSUME_TAC o rev o MATCH_MP_DEPTH depth ths) 1224 1225val ASM_MATCH_MP_TAC = ASM_MATCH_MP_TAC_N 10; 1226 1227val art = ASM_REWRITE_TAC; 1228 1229end; (* hurdUtils *) 1230