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