1(* ========================================================================= *) 2(* Version of the MESON procedure a la PTTP. Various search options. *) 3(* ========================================================================= *) 4 5structure mesonLib :> mesonLib = 6struct 7 8open HolKernel boolLib liteLib Ho_Rewrite Canon_Port tautLib; 9 10infix THEN THENC ORELSE ORELSE_TCL; 11 12(* Fix the grammar used by this file *) 13val ambient_grammars = Parse.current_grammars(); 14val _ = Parse.temp_set_grammars boolTheory.bool_grammars 15 16(*---------------------------------------------------------------------------* 17 * Miscellaneous bits. * 18 *---------------------------------------------------------------------------*) 19 20exception NOT_FOUND; 21exception Cut; 22 23fun assoc1 item = 24 let fun assc ((key,ob)::rst) = if (item=key) then SOME ob else assc rst 25 | assc [] = NONE 26 in assc 27 end; 28fun assoc1_eq cmp item = let 29 fun assc ((k,ob)::rst) = if cmp(item,k) = EQUAL then SOME ob else assc rst 30 | assc [] = NONE 31in 32 assc 33end 34fun assoc2 item = 35 let fun assc ((ob,key)::rst) = if (item=key) then SOME ob else assc rst 36 | assc [] = NONE 37 in assc 38 end; 39 40fun allpairs f l1 l2 = itlist (union o C map l2 o f) l1 [];; 41 42fun thm_eq th1 th2 = let 43 val (h1, c1) = dest_thm th1 44 val (h2, c2) = dest_thm th2 45 fun all_aconv [] [] = true 46 | all_aconv [] _ = false 47 | all_aconv _ [] = false 48 | all_aconv (h1::t1) (h2::t2) = aconv h1 h2 andalso all_aconv t1 t2 49in 50 all_aconv h1 h2 andalso aconv c1 c2 51end 52 53val the_true = T 54val the_false = F 55 56fun type_match vty cty sofar = 57 if is_vartype vty 58 then if ((vty = cty) orelse 59 (case subst_assoc (equal vty) sofar 60 of SOME ty => (ty = cty) 61 | NONE => false)) 62 then sofar 63 else {redex=vty, residue=cty}::sofar 64 else let val (vop,vargs) = dest_type vty 65 and (cop,cargs) = dest_type cty 66 in 67 if vop = cop 68 then itlist2 type_match vargs cargs sofar 69 else failwith "type_match" 70 end; 71 72 73fun is_beq tm = (type_of (lhs tm) = bool) handle HOL_ERR _ => false; 74 75(*---------------------------------------------------------------------------* 76 * Global constant. * 77 *---------------------------------------------------------------------------*) 78 79val offinc = 10000;; (* NB: should be bigger than all variable codes. *) 80 81 82(* ------------------------------------------------------------------------- *) 83(* Some "flags". *) 84(* ------------------------------------------------------------------------- *) 85 86val depth = ref false;; (* Use depth not inference bound. *) 87 88val prefine = ref true;; (* Plaisted's "positive refinement". *) 89 90val precheck = ref false;; (* Precheck ancestors for repetitions. *) 91 92val dcutin = ref 1;; (* Min size for d-and-c optimization cut-in. *) 93 94val skew = ref 3;; (* Skew proof bias (one side is <= n / skew) *) 95 96val cache = ref true;; (* Cache continuations *) 97 98val chatting = ref (if !Globals.interactive then 1 else 0); 99 (* Gives intermediate info as proof runs. 100 When the number is 1, then minimal output 101 is given. When the number is 0, no output 102 is given. Otherwise, jrh's original output 103 is given. *) 104val _ = register_trace("meson", chatting, 2); 105 106 107 108(* ------------------------------------------------------------------------- *) 109(* Shadow syntax for FOL terms in NNF. Functions and predicates have *) 110(* numeric codes, and negation is done by negating the predicate code. *) 111(* ------------------------------------------------------------------------- *) 112 113 114datatype fol_term = Var of int 115 | Fnapp of int * fol_term list;; 116 117type fol_atom = int * fol_term list;; 118 119datatype fol_form = Atom of fol_atom 120 | Conj of fol_form * fol_form 121 | Disj of fol_form * fol_form 122 | Forall of int * fol_form;; 123 124(* ------------------------------------------------------------------------- *) 125(* Translate a term (in NNF) into the shadow syntax. *) 126(* ------------------------------------------------------------------------- *) 127 128local 129 fun inc_vcounter vcounter = 130 let 131 val n = !vcounter 132 val m = n + 1 133 in 134 if (m >= offinc) then 135 raise failwith "inc_vcounter: too many variables" 136 else 137 (vcounter := m; n) 138 end 139 fun hol_of_var (vstore,gstore,_) v = 140 case assoc2 v (!vstore) 141 of NONE => assoc2 v (!gstore) 142 | x => x 143 fun hol_of_bumped_var (vdb as (_, gstore, _)) v = 144 case hol_of_var vdb v of 145 SOME x => x 146 | NONE => 147 let val v' = v mod offinc 148 val hv' = case hol_of_var vdb v' of 149 SOME y => y 150 | NONE => failwith "hol_of_bumped_var" 151 val gv = genvar (type_of hv') 152 in 153 gstore := (gv, v)::(!gstore); 154 gv 155 end 156in 157 type vardb = (term * int) list ref * (term * int) list ref * int ref 158 fun new_vardb () : vardb = (ref [], ref [], ref 0) 159 fun fol_of_var ((vstore,_,vcounter):vardb) (v:term) = 160 let val currentvars = !vstore 161 in case assoc1 v currentvars 162 of SOME x => x 163 | NONE => 164 let val n = inc_vcounter vcounter 165 in vstore := (v,n)::currentvars; n 166 end 167 end 168 val hol_of_var = hol_of_bumped_var 169end; 170 171type cdb = ((term * int) list ref * int ref) 172fun new_cdb () : cdb = (ref [(the_false, 1)], ref 2) 173fun fol_of_const ((cstore,ccounter) : cdb) c = 174 let 175 val currentconsts = !cstore 176 in 177 case assoc1_eq Term.compare c currentconsts of 178 SOME x => x 179 | NONE => 180 let val n = !ccounter 181 in 182 ccounter := n + 1; 183 cstore := (c,n)::currentconsts; 184 n 185 end 186 end 187fun hol_of_const ((cstore,_):cdb) c = 188 case assoc2 c (!cstore) 189 of SOME x => x 190 | NONE => failwith "hol_of_const" 191 192fun fol_of_term env consts (cvdb as (cdb,vdb)) tm = 193 if is_var tm andalso not (mem tm consts) then Var(fol_of_var vdb tm) 194 else 195 let val (f,args) = strip_comb tm 196 in if mem f env then failwith "fol_of_term: higher order" 197 else let val ff = fol_of_const cdb f 198 in Fnapp(ff, map (fol_of_term env consts cvdb) args) 199 end 200 end 201 202fun fol_of_atom env consts (cvdb as (cdb,_)) tm = 203 let val (f,args) = strip_comb tm 204 in if mem f env then failwith "fol_of_atom: higher order" 205 else (fol_of_const cdb f, map (fol_of_term env consts cvdb) args) 206 end 207 208fun fol_of_literal env consts cvdb tm = 209 let val tm' = dest_neg tm 210 val (p,a) = fol_of_atom env consts cvdb tm' 211 in 212 (~p,a) 213 end 214 handle HOL_ERR _ => fol_of_atom env consts cvdb tm 215 216(* ------------------------------------------------------------------------- *) 217(* Further translation functions for HOL formulas. *) 218(* ------------------------------------------------------------------------- *) 219 220fun hol_of_term (cvdb as (cdb,vdb)) tm = 221 case tm of 222 Var v => hol_of_var vdb v 223 | Fnapp(f,args) => 224 list_mk_comb(hol_of_const cdb f,map (hol_of_term cvdb) args) 225 226fun hol_of_atom (cvdb as (cdb,vdb)) (p,args) = 227 list_mk_comb(hol_of_const cdb p,map (hol_of_term cvdb) args);; 228 229fun hol_of_literal cvdb (p,args) = 230 if p < 0 then mk_neg(hol_of_atom cvdb (~p,args)) 231 else hol_of_atom cvdb (p,args) 232 233(* ------------------------------------------------------------------------- *) 234(* Versions of shadow syntax operations with variable bumping. *) 235(* ------------------------------------------------------------------------- *) 236 237fun fol_free_in v = 238 let fun freein (Var x) = (x=v) 239 | freein (Fnapp(_,lis)) = exists freein lis 240 in freein end; 241 242val fol_frees = 243 let fun fol_frees (Var x) acc = insert x acc 244 | fol_frees (Fnapp(_,lis)) acc = itlist fol_frees lis acc 245 in 246 fn tm => fol_frees tm [] 247 end; 248 249 250(*---------------------------------------------------------------------------* 251 * Short-cutting function applications of various sorts. * 252 *---------------------------------------------------------------------------*) 253 254local exception Unchanged 255 fun qmap f = 256 let fun app [] = raise Unchanged 257 | app (h::t) = 258 let val t' = app t 259 val h' = f h handle Unchanged => h 260 in h'::t' 261 end 262 handle Unchanged => f h::t 263 in app end 264 265 fun qtry f arg = f arg handle Unchanged => arg 266in 267fun raw_fol_subst theta (Var v) = 268 (case assoc2 v theta 269 of SOME x => x 270 | NONE => raise Unchanged) 271 | raw_fol_subst theta (Fnapp(f,args)) = 272 Fnapp(f,qmap (raw_fol_subst theta) args);; 273 274fun fol_subst theta tm = raw_fol_subst theta tm handle Unchanged => tm; 275 276fun fol_substl theta tms = 277 qmap (raw_fol_subst theta) tms handle Unchanged => tms;; 278 279fun fol_inst theta (at as (p,args)) = 280 (p,qmap (raw_fol_subst theta) args) handle Unchanged => at;; 281 282fun raw_fol_subst_bump offset theta tm = 283 case tm 284 of Var v => 285 if v < offinc 286 then let val v' = v + offset 287 in case (assoc2 v' theta) of SOME x => x | NONE => Var(v') 288 end 289 else (case assoc2 v theta of SOME x => x | NONE => raise Unchanged) 290 | Fnapp(f,args) => 291 Fnapp(f,qmap (raw_fol_subst_bump offset theta) args);; 292 293fun fol_subst_bump offset theta tm = 294 raw_fol_subst_bump offset theta tm handle Unchanged => tm;; 295 296fun fol_inst_bump offset theta (at as (p,args)) = 297 (p,qmap (raw_fol_subst_bump offset theta) args) handle Unchanged => at;; 298 299(* ------------------------------------------------------------------------- *) 300(* Versions of "augment_insts" and "fol_unify" with variable offsets. *) 301(* ------------------------------------------------------------------------- *) 302 303val raw_augment_insts = 304 let fun augment1 theta (s,x) = 305 let val s' = raw_fol_subst theta s 306 in if fol_free_in x s andalso not(s = Var(x)) 307 then failwith "augment1: Occurs check" 308 else (s',x) 309 end 310 in 311 fn p => fn insts => p :: qtry (qmap (augment1 [p])) insts 312 end; 313 314fun qpartition p m = 315 let fun qpart l = 316 if l=m then raise Unchanged else 317 case l 318 of [] => raise Unchanged 319 | h::t => if p h 320 then let val (yes,no) = qpart t in (h::yes,no) end 321 handle Unchanged => ([h],t) 322 else let val (yes,no) = qpart t in (yes,h::no) end 323 in 324 fn l => qpart l handle Unchanged => ([], l) 325 end 326end; 327 328fun augment_insts offset (t,v) insts = 329 let val t' = fol_subst_bump offset insts t 330 val p = (t',v) 331 in 332 case t' of 333 Var(w) => 334 if w <= v then 335 if w = v then insts else raw_augment_insts p insts 336 else raw_augment_insts (Var(v),w) insts 337 | _ => 338 if fol_free_in v t' then failwith "augment_insts: Occurs check" 339 else raw_augment_insts p insts 340 end; 341 342fun fol_unify offset tm1 tm2 sofar = 343 if tm1 = tm2 then sofar else 344 case tm1 of 345 Var(x) => 346 let val x' = if x < offinc then x + offset else x 347 in case assoc2 x' sofar 348 of SOME tm1' => fol_unify offset tm1' tm2 sofar 349 | NONE => augment_insts offset (tm2,x') sofar 350 end 351 | Fnapp(f1,args1) => 352 (case tm2 of 353 Var(y) => 354 let val y' = if y < offinc then y + offset else y 355 in case assoc2 y' sofar 356 of SOME tm2' => fol_unify offset tm1 tm2' sofar 357 | NONE => augment_insts offset (tm1,y') sofar 358 end 359 | Fnapp(f2,args2) => 360 if f1 = f2 361 then rev_itlist2 (fol_unify offset) args1 args2 sofar 362 else failwith "fol_unify: No match"); 363 364(* ------------------------------------------------------------------------- *) 365(* Test for equality under the pending instantiations. *) 366(* ------------------------------------------------------------------------- *) 367 368fun fol_eq insts tm1 tm2 = 369 tm1 = tm2 orelse 370 case tm1 371 of Var(x) => 372 (case assoc2 x insts 373 of SOME tm1' => fol_eq insts tm1' tm2 374 | NONE => 375 (case tm2 376 of Var(y) => (if x = y then true 377 else case (assoc2 y insts) 378 of SOME tm2' => (tm1 = tm2') 379 | NONE => (tm1 = tm2)) 380 | _ => false)) 381 | Fnapp(f1,args1) => 382 case tm2 383 of Var(y) => 384 (case assoc2 y insts 385 of SOME tm2' => fol_eq insts tm1 tm2' 386 | NONE => false) 387 | Fnapp(f2,args2) => 388 if f1 = f2 then Lib.all2 (fol_eq insts) args1 args2 389 else false; 390 391 392fun fol_atom_eq insts (p1,args1) (p2,args2) = 393 (p1 = p2) andalso Lib.all2 (fol_eq insts) args1 args2;; 394 395(* ------------------------------------------------------------------------- *) 396(* Cacheing continuations. Very crude, but it works remarkably well. *) 397(* ------------------------------------------------------------------------- *) 398 399fun cacheconts f = 400 if !cache 401 then let val memory = ref [] 402 in fn input as (gg, (insts,offset,(size:int))) => 403 if exists (fn (_,(insts',_,size')) => 404 insts=insts' andalso (size <= size' orelse !depth)) 405 (!memory) 406 then failwith "cachecont" 407 else (memory := input::(!memory); f input) 408 end 409 else f;; 410 411(* ------------------------------------------------------------------------- *) 412(* Check ancestor list for repetition. *) 413(* ------------------------------------------------------------------------- *) 414 415fun checkan insts (p:int,a) ancestors = 416 if !precheck 417 then let val p' = ~p 418 val t' = (p',a) 419 in case assoc1 p' ancestors 420 of NONE => ancestors 421 | SOME ours => 422 if exists (fn u => fol_atom_eq insts t' (snd(fst u))) ours 423 then failwith "checkan" 424 else ancestors 425 end 426 else ancestors;; 427 428(* ------------------------------------------------------------------------- *) 429(* Insert new goal's negation in ancestor clause, given refinement. *) 430(* ------------------------------------------------------------------------- *) 431 432fun insertan insts (p,a) ancestors = 433 let val p':int = ~p 434 val t' = (p',a) 435 val (ourancp,otheranc) = Lib.pluck (fn (pr,_) => pr = p') ancestors 436 handle HOL_ERR _ => ((p',[]),ancestors) 437 val ouranc = snd ourancp 438 in 439 if exists (fn u => fol_atom_eq insts t' (snd(fst u))) ouranc 440 then failwith "insertan: loop" 441 else (p',(([],t'),(0,TRUTH))::ouranc)::otheranc 442 end 443 444(* ------------------------------------------------------------------------- *) 445(* Recording MESON proof tree. *) 446(* ------------------------------------------------------------------------- *) 447 448datatype fol_goal = Subgoal of fol_atom 449 * fol_goal list 450 * (int * thm) 451 * int 452 * (fol_term * int)list;; 453 454(* ------------------------------------------------------------------------- *) 455(* Perform basic MESON expansion. *) 456(* ------------------------------------------------------------------------- *) 457 458fun meson_single_expand infs rule ((g,ancestors),(insts,offset,size)) = 459 let val ((hyps,conc),tag) = rule 460 val allins = rev_itlist2 (fol_unify offset) (snd g) (snd conc) insts 461 val (locin,globin) = qpartition (fn (_,v) => offset <= v) insts allins 462 fun mk_ihyp h = 463 let val h' = fol_inst_bump offset locin h 464 in (h', checkan insts h' ancestors) 465 end 466 val newhyps = map mk_ihyp hyps 467 in 468 infs := !infs + 1; 469 (newhyps, (globin, offset+offinc, size - length hyps)) 470 end; 471 472 473(* ------------------------------------------------------------------------- *) 474(* Perform first basic expansion which allows continuation call. *) 475(* ------------------------------------------------------------------------- *) 476 477fun meson_expand_cont infs rules state cont = 478 tryfind (fn r => cont (snd r) (meson_single_expand infs r state)) rules;; 479 480(* ------------------------------------------------------------------------- *) 481(* Try expansion and continuation call with either ancestor or initial rule. *) 482(* ------------------------------------------------------------------------- *) 483 484fun meson_expand infs rules ((g,ancestors),(tup as (insts,offset,size))) cont = 485 let val pr = fst g 486 val newancestors = insertan insts g ancestors 487 val newstate = ((g,newancestors),tup) 488 in 489 (if !prefine andalso pr > 0 then failwith "meson_expand" 490 else case (assoc1 pr ancestors) 491 of SOME arules => meson_expand_cont infs arules newstate cont 492 | NONE => failwith "not found") 493 handle Cut => failwith "meson_expand" 494 | HOL_ERR _ => 495 (case (assoc1 pr rules) 496 of SOME x => 497 let val crules = filter (fn ((h,_),_) => length h <= size) x 498 in meson_expand_cont infs crules newstate cont 499 end 500 | NONE => failwith "not found") 501 handle Cut => failwith "meson_expand" 502 end 503 504(* ------------------------------------------------------------------------- *) 505(* Simple Prolog engine which organizes search and backtracking. *) 506(* ------------------------------------------------------------------------- *) 507 508fun expand_goal infs rules = 509 let 510 fun exp_goal depth (state as ((g,_),(insts,offset,size))) cont = 511 if depth < 0 then failwith "expand_goal: too deep" 512 else 513 meson_expand infs rules state 514 (fn apprule => fn (newstate as (_,(pinsts,_,_))) => 515 exp_goals (depth-1) newstate 516 (cacheconts 517 (fn (gs,(newinsts,newoffset,newsize)) => 518 let val (locin,globin) = 519 qpartition (fn (_,v) => offset <= v) pinsts newinsts 520 val g' = Subgoal(g,gs,apprule,offset,locin) 521 in 522 if (globin = insts) andalso null(gs) then 523 cont(g',(globin,newoffset,size)) handle HOL_ERR _ => raise Cut 524 else 525 cont(g',(globin,newoffset,newsize)) 526 handle Cut => failwith "expand_goal" 527 end))) 528 and 529 exp_goals depth (gl, tup as (insts,offset,size)) cont = 530 case gl of 531 [] => cont ([],tup) 532 | [g] => exp_goal depth (g,tup) (fn (g',stup) => cont([g'],stup)) 533 | g::gs => 534 if size >= !dcutin 535 then let val lsize = size div (!skew) 536 val rsize = size - lsize 537 val (lgoals,rgoals) = chop_list (length gl div 2) gl 538 in 539 exp_goals depth (lgoals,(insts,offset,lsize)) 540 (cacheconts(fn (lg',(i,off,n)) => 541 exp_goals depth (rgoals,(i,off,n + rsize)) 542 (cacheconts(fn (rg',ztup) => cont (lg'@rg',ztup))))) 543 handle HOL_ERR _ => 544 exp_goals depth (rgoals,(insts,offset,lsize)) 545 (cacheconts(fn (rg',(i,off,n)) => 546 exp_goals depth (lgoals,(i,off,n + rsize)) 547 (cacheconts (fn (lg',ztup as (_,_,fsize)) => 548 if n + rsize <= lsize + fsize 549 then failwith "repetition of demigoal pair" 550 else cont (lg'@rg',ztup))))) 551 end 552 else 553 exp_goal depth (g,tup) 554 (cacheconts (fn (g',stup) => 555 exp_goals depth (gs,stup) 556 (cacheconts (fn (gs',ftup) => cont(g'::gs',ftup))))) 557 in 558 fn g => 559 fn maxdep => 560 fn maxinf => 561 fn cont => exp_goal maxdep (g,([],2 * offinc,maxinf)) cont 562 end 563 564(* 565val state = (g,([],2 * offinc,maxinf)) 566 : ((int * fol_term list) 567 * (int * (((int * fol_term list) list * (int * fol_term list)) * (int * thm)) list) list) 568 * ((fol_term * int) list * int * int);; 569 570*) 571(* ------------------------------------------------------------------------- *) 572(* With iterative deepening of inferences or depth. *) 573(* *) 574(* NB: If multiple solutions are required, simply give a continuation which *) 575(* stores putative solutions then fails; that will initiate backtracking! *) 576(* ------------------------------------------------------------------------- *) 577 578fun chat infs n = 579 case !chatting 580 of 0 => () 581 | 1 => say "." 582 | _ => say (String.concat[Int.toString infs, " inferences so far. ", 583 "Searching with maximum size ", 584 int_to_string n, ".\n"]); 585 586fun say_solved infs n = 587 if (n <> 0 andalso n <> 1) 588 then say (String.concat["Internal goal solved with ", 589 Int.toString infs, 590 " MESON inferences.\n"]) 591 else (); 592 593fun solve_goal infs rules incdepth min max incsize = 594 let fun solve n g = 595 if n > max then failwith "solve_goal: Too deep" 596 else let val _ = chat (!infs) n 597 val gi = if incdepth then expand_goal infs rules g n 100000 I 598 else expand_goal infs rules g 100000 n I 599 val _ = say_solved (!infs) (!chatting) 600 in 601 gi 602 end 603 handle HOL_ERR _ => solve (n + incsize) g 604 in 605 fn g => solve min (g,[]) 606 end; 607 608(* ------------------------------------------------------------------------- *) 609(* Creation of tagged contrapositives from a HOL clause. *) 610(* This includes any possible support clauses (1 = falsity). *) 611(* The rules are partitioned into association lists. *) 612(* ------------------------------------------------------------------------- *) 613 614val fol_of_hol_clauses = 615 let 616 fun mk_negated (p:int,a) = (~p,a) 617 fun mk_contraposes n th used unused sofar = 618 case unused 619 of [] => sofar 620 | h::t => 621 let val new = ((map mk_negated (used @ t),h),(n,th)) 622 in mk_contraposes (n + 1) th (used@[h]) t (new::sofar) 623 end 624 fun fol_of_hol_clause cvdb th = 625 let 626 val lconsts = freesl (hyp th) 627 val tm = concl th 628 val hlits = strip_disj tm 629 val flits = map (fol_of_literal [] lconsts cvdb) hlits 630 val basics = mk_contraposes 0 th [] flits [] 631 in 632 if Lib.all (fn (p,_) => p < 0) flits then 633 ((map mk_negated flits,(1,[])),(~1,th))::basics 634 else basics 635 end 636 fun eek (x1,(i1,th1)) (x2,(i2,th2)) = 637 (x1=x2) andalso (i1=i2) andalso thm_eq th1 th2 638 in 639 fn cvdb => fn thms => 640 let 641 val rawrules = itlist (Lib.op_union eek o fol_of_hol_clause cvdb) thms [] 642 val prs = mk_set (map (fst o snd o fst) rawrules) 643 val prules = 644 map (fn t => (t,filter (curry op = t o fst o snd o fst) rawrules)) prs 645 val srules = sort (fn (p:int,_) => fn (q,_) => abs(p) <= abs(q)) prules 646 in 647 srules 648 end 649 end 650 651(* ------------------------------------------------------------------------- *) 652(* Optimize a set of clauses (changing literal order complicates HOL stuff). *) 653(* ------------------------------------------------------------------------- *) 654 655fun optimize_rules l = 656 let 657 fun fol_atom_frees (p,a) = fol_frees(Fnapp(p,a)) 658 fun optimize_clause_order cls = 659 sort (fn ((l1,_),_) => fn ((l2,_),_) => length l1 <= length l2) cls 660 in 661 map (fn (a,b) => (a,optimize_clause_order b)) l 662 end 663 664 665(* ------------------------------------------------------------------------- *) 666(* Create a HOL contrapositive on demand, with a cache. *) 667(* ------------------------------------------------------------------------- *) 668 669local 670 open boolTheory 671 val DISJ_ASSOC' = SPEC_ALL DISJ_ASSOC 672 val DISJ_SYM' = SPEC_ALL DISJ_SYM 673 val DEMORG = SPEC_ALL DE_MORGAN_THM 674 val DEMORG_DISJ = CONJUNCT2 DEMORG 675 val DEMORG_AND = SYM (CONJUNCT1 DEMORG) 676 val NOT2 = CONJUNCT1(SPEC_ALL NOT_CLAUSES) 677 val NOT_IMP = IMP_ANTISYM_RULE (SPEC_ALL boolTheory.F_IMP) 678 (SPEC_ALL boolTheory.IMP_F); 679 680 val DISJ_AC = EQT_ELIM o AC_CONV (DISJ_ASSOC', DISJ_SYM') 681 val imp_CONV = REWR_CONV(TAUT `a \/ b = ~b ==> a`) 682 val push_CONV = GEN_REWRITE_CONV TOP_SWEEP_CONV [DEMORG_DISJ, NOT2] 683 and pull_CONV = GEN_REWRITE_CONV DEPTH_CONV [DEMORG_AND] 684 and imf_CONV = REWR_CONV NOT_IMP 685in 686 fun new_contrapos_cache() = ref ([] : ((int * term) * thm) list) 687 fun make_hol_contrapos memory (n,th) = 688 let val tm = concl th 689 val key = (n,tm) 690 in 691 case (assoc1 key (!memory)) 692 of SOME x => x 693 | NONE => 694 if n < 0 then CONV_RULE (pull_CONV THENC imf_CONV) th 695 else let val djs = strip_disj tm 696 val acth = 697 if n = 0 then th else 698 let val (ldjs,rdjs) = chop_list n djs 699 val ndjs = hd rdjs::(ldjs@(tl rdjs)) 700 in 701 EQ_MP (DISJ_AC(mk_eq(tm,list_mk_disj ndjs))) th 702 end 703 val fth = if length djs = 1 then acth 704 else CONV_RULE (imp_CONV THENC push_CONV) acth 705 in 706 memory := (key,fth)::(!memory); 707 fth 708 end 709 end 710end 711 712(* ------------------------------------------------------------------------- *) 713(* Translate back the saved proof into HOL. *) 714(* ------------------------------------------------------------------------- *) 715 716local 717 fun hol_negate tm = dest_neg tm handle HOL_ERR _ => mk_neg tm 718 fun merge_inst (t,x) current = (fol_subst current t,x)::current 719 val finish_RULE = Rewrite.GEN_REWRITE_RULE I Rewrite.empty_rewrites 720 [TAUT `(~p ==> p) = p`, TAUT `(p ==> ~p) = ~p`] 721in 722 fun meson_to_hol insts cpos_cache cvdb (Subgoal(g,gs,(n,th),offset,locin)) = 723 let val newins = itlist merge_inst locin insts 724 val g' = fol_inst newins g 725 val hol_g = hol_of_literal cvdb g' 726 val (cdv, vdb) = cvdb 727 val ths = map (meson_to_hol newins cpos_cache cvdb) gs 728 val hth = 729 if concl th = the_true then ASSUME hol_g 730 else let val cth = make_hol_contrapos cpos_cache (n,th) 731 in if null ths then cth 732 else Drule.MATCH_MP cth (Lib.end_itlist Thm.CONJ ths) 733 handle e as HOL_ERR _ => 734 (say ("Attempting to match\n "^ 735 (term_to_string (concl cth))^"\n\nand\n\n "^ 736 (term_to_string (concl (end_itlist CONJ ths)))^ 737 "\n\nwith n = "^ (int_to_string n)^ 738 " and th = "^(term_to_string (concl th))^"\n"); 739 raise e) 740 end 741 val ith = HO_PART_MATCH I hth hol_g 742 in 743 finish_RULE (DISCH (hol_negate(concl ith)) ith) 744 end 745end 746 747fun ASM_FOL_TAC (asl,w) = 748 let val headsp = itlist Canon_Port.get_thm_heads asl ([],[]) 749 in jrhTactics.RULE_ASSUM_TAC 750 (CONV_RULE(Canon_Port.GEN_FOL_CONV headsp)) (asl,w) 751 end 752 753 754(* ------------------------------------------------------------------------- *) 755(* Initial canonicalizer. *) 756(* ------------------------------------------------------------------------- *) 757 758val PREMESON_CANON_TAC = 759 let fun GSPEC th = SPEC (genvar(type_of(fst(dest_forall(concl th))))) th 760 open jrhTactics 761 in 762 RULE_ASSUM_TAC 763 (CONV_RULE 764 (PRESIMP_CONV THENC DELAMB_CONV THENC NNFC_CONV THENC SKOLEM_CONV)) THEN 765 REPEAT (FIRST_X_ASSUM CHOOSE_TAC) THEN 766 ASM_FOL_TAC THEN 767 REPEAT(FIRST_X_ASSUM 768 ((DISJ_CASES_THEN ORELSE_TCL CONJUNCTS_THEN) ASSUME_TAC)) THEN 769 RULE_ASSUM_TAC(CONV_RULE(PRENEX_CONV THENC PROP_CNF_CONV)) THEN 770 RULE_ASSUM_TAC(liteLib.repeat GSPEC) THEN 771 REPEAT (FIRST_X_ASSUM (CONJUNCTS_THEN ASSUME_TAC)) 772 end 773 774 775(* ------------------------------------------------------------------------- *) 776(* Create equality axioms for all the function and predicate symbols in *) 777(* a HOL term. Not very efficient (but then neither is throwing them into *) 778(* automated proof search!) *) 779(* ------------------------------------------------------------------------- *) 780 781val create_equality_axioms = 782 let 783 (* open Resolve *) 784 val eq_thms = (CONJUNCTS o prove) 785 (``(x:'a = x) /\ 786 (~(x:'a = y) \/ ~(x = z) \/ (y = z))``, 787 REWRITE_TAC[] THEN ASM_CASES_TAC ``x:'a = y`` THEN 788 ASM_REWRITE_TAC[ONCE_REWRITE_RULE[boolTheory.DISJ_SYM] 789 (REWRITE_RULE[] boolTheory.BOOL_CASES_AX)]) 790 val imp_elim_CONV = REWR_CONV (TAUT `(a ==> b) = ~a \/ b`) 791 val eq_elim_RULE = MATCH_MP(TAUT `(a = b) ==> b \/ ~a`) 792 val veq_tm = rator(rator(concl(hd eq_thms))) 793 fun create_equivalence_axioms (eq,_) = 794 let val tyins = type_match (type_of veq_tm) (type_of eq) [] 795 in map (INST_TYPE tyins) eq_thms 796 end 797 fun tm_consts tm acc = 798 let val (fnc,args) = strip_comb tm 799 in if args = [] then acc 800 else itlist tm_consts args (insert (fnc,length args) acc) 801 end 802 fun fm_consts tm (acc as (preds,funs)) = 803 fm_consts(snd(dest_forall tm)) acc 804 handle HOL_ERR _ => fm_consts(snd(dest_exists tm)) acc 805 handle HOL_ERR _ => 806 let val (l,r) = dest_conj tm in fm_consts l (fm_consts r acc) end 807 handle HOL_ERR _ => 808 let val (l,r) = dest_disj tm in fm_consts l (fm_consts r acc) end 809 handle HOL_ERR _ => 810 let val (l,r) = dest_imp tm in fm_consts l (fm_consts r acc) end 811 handle HOL_ERR _ => fm_consts (dest_neg tm) acc 812 handle HOL_ERR _ => 813 let val (l,r) = dest_eq tm 814 in if type_of l = Type.bool 815 then fm_consts r (fm_consts l acc) 816 else failwith "atomic equality" 817 end 818 handle HOL_ERR _ => 819 let val (pred,args) = strip_comb tm 820 in if args = [] then acc 821 else (insert (pred,length args) preds, 822 itlist tm_consts args funs) 823 end; 824 825 fun create_congruence_axiom pflag (tm,len) = 826 let val (atys,rty) = splitlist (fn ty => 827 let val (opn,l) = dest_type ty 828 in if opn = "fun" then (hd l,hd(tl l)) else fail() 829 end) (type_of tm) 830 val ctys = fst(chop_list len atys) 831 val largs = map genvar ctys 832 and rargs = map genvar ctys 833 val th1 = rev_itlist (C (curry MK_COMB)) 834 (map (ASSUME o mk_eq) (zip largs rargs)) (REFL tm) 835 val th2 = if pflag then eq_elim_RULE th1 else th1 836 in 837 itlist (fn e => fn th => 838 CONV_RULE imp_elim_CONV (DISCH e th)) (hyp th2) th2 839 end 840 in 841 fn tms => 842 let val (preds,funs) = itlist fm_consts tms ([],[]) 843 val (eqs0,noneqs) = partition (is_eqc o fst) preds 844 in if eqs0 = [] then [] 845 else let val pcongs = map (create_congruence_axiom true) noneqs 846 and fcongs = map (create_congruence_axiom false) funs 847 val (preds1,_) = 848 itlist fm_consts (map concl (pcongs @ fcongs)) ([],[]) 849 val eqs1 = filter (is_eqc o fst) preds1 850 val eqs = union eqs0 eqs1 851 val equivs = itlist 852 (Lib.op_union thm_eq o create_equivalence_axioms) eqs [] 853 in 854 equivs@pcongs@fcongs 855 end 856 end 857 end 858 859(* ------------------------------------------------------------------------- *) 860(* Push duplicated copies of poly theorems to match existing assumptions. *) 861(* ------------------------------------------------------------------------- *) 862 863val (POLY_ASSUME_TAC:thm list -> jrhTactics.Tactic) = 864 let 865 open jrhTactics 866 fun grab_constants tm acc = 867 if is_forall tm orelse is_exists tm then 868 grab_constants (body(rand tm)) acc 869 else 870 if is_beq tm orelse is_imp tm orelse is_conj tm orelse is_disj tm then 871 grab_constants (rand tm) (grab_constants (lhand tm) acc) 872 else 873 if is_neg tm then 874 grab_constants (rand tm) acc 875 else union (find_terms is_const tm) acc 876 fun match_consts (tm1,tm2) = 877 let val {Name=s1,Thy=thy1,Ty=ty1} = dest_thy_const tm1 878 and {Name=s2,Thy=thy2,Ty=ty2} = dest_thy_const tm2 879 in 880 if (s1=s2) andalso (thy1=thy2) 881 then type_match ty1 ty2 [] 882 else failwith "match_consts" 883 end 884 fun polymorph mconsts th = 885 let val tvs = subtract (type_vars_in_term (concl th)) 886 (Lib.U (map type_vars_in_term (hyp th))) 887 in 888 if tvs = [] then [th] else 889 let 890 val pconsts = grab_constants (concl th) [] 891 val tyins = mapfilter match_consts 892 (allpairs (fn x => fn y => (x,y)) pconsts mconsts) 893 val ths' = Lib.op_mk_set thm_eq (mapfilter (C INST_TYPE th) tyins) 894 in 895 if null ths' then 896 (if not (!Globals.interactive) then () 897 else say "No useful-looking instantiations of lemma\n"; 898 [th]) 899 else ths' 900 end 901 end 902 903 fun polymorph_all mconsts ths acc = 904 if null(ths) then acc else 905 let 906 val ths' = polymorph mconsts (hd ths) 907 val mconsts' = itlist grab_constants (map concl ths') mconsts 908 in 909 polymorph_all mconsts' (tl ths) (Lib.op_union thm_eq ths' acc) 910 end 911 in 912 fn ths => fn (gl as (asl,w)) => 913 let 914 val mconsts = itlist (grab_constants o concl) asl [] 915 val ths' = polymorph_all mconsts ths [] 916 in 917 MAP_EVERY ASSUME_TAC ths' gl 918 end 919 end 920 921(* ------------------------------------------------------------------------- *) 922(* HOL MESON procedure. *) 923(* *) 924(* NB! We try all the support clauses in each iterative deepening run. *) 925(* *) 926(* This makes sure we get the shortest proof, but it can increase the run *) 927(* time if there is a proof based on the first support clause with similar *) 928(* size. It would be easy to separate out the support-clause trying (and *) 929(* it would save a little time in the assocs to take it out of the main *) 930(* rules too). *) 931(* ------------------------------------------------------------------------- *) 932 933fun SIMPLE_MESON_REFUTE infs min max inc ths = 934 (let val old_dcutin = !dcutin 935 in 936 if !depth then dcutin := 100001 else (); 937 let 938 val ths' = ths @ create_equality_axioms (map concl ths) 939 val cvdb = (new_cdb(), new_vardb()) 940 val rules = optimize_rules(fol_of_hol_clauses cvdb ths') 941 val (proof,(insts,_,_)) = 942 solve_goal infs rules (!depth) min max inc (1,[]) 943 in 944 dcutin := old_dcutin; 945 meson_to_hol insts (new_contrapos_cache()) cvdb proof 946 end 947 end) 948 949 950fun PURE_MESON_TAC infs min max inc gl = 951 let open jrhTactics 952 in 953 (FIRST_ASSUM CONTR_TAC ORELSE 954 W(ACCEPT_TAC o SIMPLE_MESON_REFUTE infs min max inc o fst)) gl 955 end 956 957 958fun inform tac g = 959 let val _ = if (!chatting = 1) then say "Meson search level: " else () 960 val infs = ref 0 961 val res = tac infs g 962 val _ = if (!chatting = 0) then () 963 else if (!chatting = 1) then say"\n" 964 else say (" solved with " ^ Int.toString (!infs) ^ 965 " MESON inferences.\n") 966 in res end; 967 968fun GEN_MESON_TAC min max step ths g = 969 inform 970 (fn infs => 971 REFUTE_THEN ASSUME_TAC THEN 972 let 973 open jrhTactics 974 in 975 convert (POLY_ASSUME_TAC (map GEN_ALL ths) THEN PREMESON_CANON_TAC THEN 976 PURE_MESON_TAC infs min max step) 977 end) g; 978 979 980val max_depth = ref 30; 981fun ASM_MESON_TAC e = GEN_MESON_TAC 0 (!max_depth) 1 e; 982 983fun MESON_TAC ths = POP_ASSUM_LIST (K ALL_TAC) THEN ASM_MESON_TAC ths; 984 985val _ = Parse.temp_set_grammars ambient_grammars; 986 987end; 988