1(* non-interactive mode 2*) 3structure ho_proverTools :> ho_proverTools = 4struct 5open HolKernel Parse boolLib BasicProvers; 6 7structure Parse = struct 8 open Parse 9 val (Type,Term) = 10 pred_setTheory.pred_set_grammars 11 |> apsnd ParseExtras.grammar_loose_equality 12 |> parse_from_grammars 13end 14open Parse 15 16 17(* interactive mode 18val () = loadPath := union ["..", "../finished"] (!loadPath); 19val () = app load 20 ["HurdUseful", 21 "ho_basicTools", 22 "unifyTools", 23 "skiTheory"]; 24val () = show_assums := true; 25*) 26 27open Susp combinTheory hurdUtils skiTools; 28 29infixr 0 oo ## ++ << || THENC ORELSEC THENR ORELSER -->; 30infix 1 >> |->; 31infix thenf orelsef then_frule orelse_frule join_frule; 32 33val op++ = op THEN; 34val op<< = op THENL; 35val op|| = op ORELSE; 36val op>> = op THEN1; 37val !! = REPEAT; 38 39(* non-interactive mode 40*) 41fun trace _ _ = (); 42fun printVal _ = (); 43 44(* ------------------------------------------------------------------------- *) 45(* vterm operations *) 46(* ------------------------------------------------------------------------- *) 47 48local 49 fun subsumes ((vars, tm), _) ((_, tm'), _) = can (var_match vars tm) tm' 50in 51 fun cons_subsume x l = 52 if exists (C subsumes x) l then l else x :: filter (not o subsumes x) l 53end; 54 55(* ------------------------------------------------------------------------- *) 56(* vthm operations *) 57(* ------------------------------------------------------------------------- *) 58 59local 60 fun annotate vth = ((I ## concl) vth, vth) 61in 62 fun vthm_cons_subsume vth vths = 63 map snd (cons_subsume (annotate vth) (map annotate vths)) 64end; 65 66(* ========================================================================= *) 67(* Higher-order proof search. *) 68(* ========================================================================= *) 69 70(* ------------------------------------------------------------------------- *) 71(* Types. *) 72(* ------------------------------------------------------------------------- *) 73 74type literal = bool * term; 75datatype clause = CLAUSE of vars * literal list; 76 77datatype fact = FACT of clause * thm susp; 78 79type literal_rule = 80 vars * literal -> (substitution * vars * literal list * rule) list; 81 82type clause_rule = clause -> (substitution * clause * rule) list; 83 84type fact_rule = fact -> (substitution * fact) list; 85 86datatype factdb = FACTDB of {factl : fact list, normf : fact_rule}; 87 88(* ------------------------------------------------------------------------- *) 89(* Literal and clause operations. *) 90(* ------------------------------------------------------------------------- *) 91 92fun dest_clause (CLAUSE c) = c; 93val clause_vars = fst o dest_clause; 94val clause_literals = snd o dest_clause; 95 96fun literal_term (true, tm) = tm 97 | literal_term (false, tm) = mk_neg tm; 98 99fun literals_term lits = 100 (case map literal_term (rev lits) of [] => F 101 | l :: ls => trans (curry mk_disj) l ls); 102 103fun clause_term (CLAUSE ((v, _), lits)) = mk_foralls (v, literals_term lits); 104 105local 106 fun canon_ty (_, initial_vars) togo vars ty = 107 let 108 fun canon 0 vars _ = (0, vars) 109 | canon togo vars [] = (togo, vars) 110 | canon togo vars (ty :: rest) = 111 if is_vartype ty then 112 if mem ty vars orelse not (mem ty initial_vars) then 113 canon togo vars rest 114 else canon (togo - 1) (ty :: vars) rest 115 else 116 let 117 val (_, tys) = dest_type ty 118 in 119 canon togo vars (tys @ rest) 120 end 121 in 122 canon togo vars [ty] 123 end 124 125 fun canon_tm initial_vars tms = 126 let 127 fun canon _ vars [] = vars 128 | canon (0, 0) vars _ = vars 129 | canon togo vars (tm :: rest) = 130 if is_comb tm then 131 let 132 val (a, b) = dest_comb tm 133 in 134 canon togo vars (a :: b :: rest) 135 end 136 else 137 let 138 val (tmtogo, tytogo) = togo 139 val (tmvars, tyvars) = vars 140 val (tytogo', tyvars') = 141 canon_ty initial_vars tytogo tyvars (type_of tm) 142 in 143 if is_tmvar initial_vars tm andalso not (tmem tm tmvars) then 144 canon (tmtogo - 1, tytogo') (tm :: tmvars, tyvars') rest 145 else canon (tmtogo, tytogo') (tmvars, tyvars') rest 146 end 147 in 148 canon ((length ## length) initial_vars) empty_vars tms 149 end 150in 151 fun clause_canon_vars (CLAUSE (vars, lits)) = 152 CLAUSE (canon_tm vars (map snd lits), lits); 153end; 154 155(* ------------------------------------------------------------------------- *) 156(* Fact and proof operations. *) 157(* ------------------------------------------------------------------------- *) 158 159fun dest_fact (FACT f) = f; 160val fact_clause = fst o dest_fact; 161val fact_vars = clause_vars o fact_clause; 162val fact_literals = clause_literals o fact_clause; 163 164local 165 val thm1 = prove (``!a. a ==> ~a ==> F``, PROVE_TAC []) 166 val thm2 = prove (``!x. (~x ==> F) ==> x``, PROVE_TAC []) 167in 168 val norm_thm = MATCH_MP thm1 THENR UNDISCH 169 fun march_literal lit = DISCH (mk_neg (literal_term lit)) THENR MATCH_MP thm2 170end; 171 172local 173 fun mk_fact (vars, th) = 174 let 175 val c = CLAUSE (vars, [(true, concl th)]) 176 in 177 FACT (c, delay (K (norm_thm th))) 178 end; 179in 180 val vthm_to_fact = mk_fact o (I ## CONV_RULE SKI_CONV) 181 val thm_to_fact = vthm_to_fact o thm_to_vthm; 182end; 183 184fun fact_to_vthm (FACT (cl, thk)) = (clause_vars cl, force thk); 185val fact_to_thm = vthm_to_thm o fact_to_vthm; 186 187(* ------------------------------------------------------------------------- *) 188(* Fact rule operations. *) 189(* ------------------------------------------------------------------------- *) 190 191val no_frule : fact_rule = fn _ => raise ERR "no_frule" "always fails"; 192val all_frule : fact_rule = fn f => [(empty_subst, f)]; 193val empty_frule : fact_rule = K []; 194 195val trace_frule : fact_rule = 196 fn f => 197 let 198 val _ = trace "trace_frule: f" (fn () => printVal f) 199 in 200 [(empty_subst, f)] 201 end; 202 203fun op orelse_frule (r1 : fact_rule, r2 : fact_rule) : fact_rule = 204 r1 orelsef r2; 205 206fun op then_frule (r1 : fact_rule, r2 : fact_rule) : fact_rule = 207 let 208 fun process (sub, f) = map (refine_subst sub ## I) (r2 f) 209 in 210 flatten o map process o r1 211 end; 212 213fun try_frule r = r orelse_frule all_frule; 214 215fun op join_frule (r1 : fact_rule, r2 : fact_rule) : fact_rule = 216 op@ o ((r1 orelse_frule empty_frule) ## (r2 orelse_frule empty_frule)) o D; 217 218fun repeat_frule r f = try_frule (r then_frule repeat_frule r) f; 219 220fun joinl_frule [] = no_frule 221 | joinl_frule (r :: rest) = r join_frule (joinl_frule rest); 222 223fun first_frule [] = no_frule 224 | first_frule (r :: rest) = r orelse_frule (first_frule rest); 225 226local 227 fun reassem previous next (sub, vars, lits, vf) = 228 let 229 val previous' = map (I ## pinst sub) (rev previous) 230 val next' = map (I ## pinst sub) next 231 in 232 (sub, CLAUSE (vars, previous' @ lits @ next'), vf) 233 end 234 handle (h as HOL_ERR _) => raise err_BUG "lrule_to_crule" h 235 236 fun mk_crule _ _ _ [] = raise ERR "lrule_to_crule" "lrule does not apply" 237 | mk_crule r vars previous (lit :: next) = 238 (case total r (vars, lit) of NONE => mk_crule r vars (lit :: previous) next 239 | SOME cls' => map (reassem previous next) cls') 240in 241 fun lrule_to_crule (lrule : literal_rule) : clause_rule = 242 fn CLAUSE (vars, lits) => mk_crule lrule vars [] lits 243end; 244 245fun crule_to_frule (crule : clause_rule) : fact_rule = 246 fn FACT (cl, th) => 247 let 248 fun process (sub, cl', vf) = 249 let 250 val _ = trace "crule_to_frule: cl'" (fn () => printVal cl') 251 in 252 (sub, FACT (cl', susp_map vf th)) 253 end 254 handle (h as HOL_ERR _) => raise err_BUG "crule_to_frule" h 255 val cls' = crule cl 256 val _ = 257 trace "crule_to_frule: ((cl, th), cls')" 258 (fn () => printVal ((cl, th), cls')) 259 val res = map process cls' 260 in 261 res 262 end; 263 264val lrule_to_frule = crule_to_frule o lrule_to_crule; 265 266(* Replace clause variables in a fact with fresh ones. *) 267(* In order to avoid cyclic substitutions and to facilitate unification, *) 268(* we INSIST that variables present in facts are always fresh. *) 269(* Designers of tactic rules may thus wish to use this rule liberally. *) 270 271val fresh_vars_crule : clause_rule = 272 fn CLAUSE (vars, lits) => 273 let 274 val (vars', (sub, _)) = new_vars vars 275 in 276 [(sub, CLAUSE (vars', map (I ## pinst sub) lits), PINST sub)] 277 end; 278 279val fresh_vars_frule : fact_rule = crule_to_frule fresh_vars_crule; 280 281(* ------------------------------------------------------------------------- *) 282(* Fact database operations. *) 283(* ------------------------------------------------------------------------- *) 284 285val null_factdb = FACTDB {factl = [], normf = no_frule}; 286 287fun dest_factdb (FACTDB db) = db; 288val factdb_factl = #factl o dest_factdb; 289val factdb_normf = #normf o dest_factdb; 290 291val factdb_size = length o factdb_factl; 292 293fun factdb_norm_frule (FACTDB {normf, ...}) = repeat_frule normf; 294 295fun factdb_norm db f = map snd (factdb_norm_frule db f); 296 297fun factdb_add_fact f (db as FACTDB {factl, normf}) = 298 FACTDB {factl = factdb_norm db f @ factl, normf = normf}; 299 300val factdb_add_facts = C (trans factdb_add_fact); 301 302val factdb_add_vthm = factdb_add_fact o vthm_to_fact; 303val factdb_add_vthms = C (trans factdb_add_vthm); 304 305val factdb_add_thm = factdb_add_fact o thm_to_fact; 306val factdb_add_thms = C (trans factdb_add_thm); 307 308local 309 fun norm_app normf normf' = 310 (normf then_frule try_frule normf') orelse_frule normf'; 311in 312 fun factdb_add_norm normf' (FACTDB {factl, normf}) = 313 factdb_add_facts factl (FACTDB {factl = [], normf = norm_app normf normf'}); 314end; 315 316(* ------------------------------------------------------------------------- *) 317(* Pretty printing. *) 318(* ------------------------------------------------------------------------- *) 319 320val pp_literal = pp_map literal_term pp_term; 321 322val genvar_prefix = "%%genvar%%"; 323fun dest_genvar v = 324 let 325 val (name, ty) = dest_var v 326 val _ = assert (String.isPrefix genvar_prefix name) 327 (ERR "dest_genvar" "not a genvar") 328 in 329 (string_to_int (String.extract (name, size genvar_prefix, NONE)), ty) 330 end; 331val is_genvar = can dest_genvar; 332 333fun clause_pretty_term (CLAUSE ((vs, _), lits)) = 334 let 335 val tm = literals_term lits 336 val gs = (filter is_genvar o free_vars) tm 337 fun pretty_g g = 338 let 339 val name = 340 (int_to_string o fst o dest_genvar) g 341 handle HOL_ERR _ => (fst o dest_var) g 342 val stem = if tmem g vs then "v" else "c" 343 in 344 mk_var (stem ^ "_" ^ name, type_of g) 345 end 346 347 val sub = (subst o zipwith (curry op|->) gs o map pretty_g) gs 348 in 349 mk_foralls (map sub vs, sub tm) 350 end; 351 352val pp_clause = pp_map clause_pretty_term pp_term; 353 354val pp_fact = pp_map (fn FACT (c, p) => c) pp_clause; 355 356val pp_factdb = pp_map factdb_factl (pp_list pp_fact); 357 358(* ------------------------------------------------------------------------- *) 359(* Rewriting for facts. *) 360(* ------------------------------------------------------------------------- *) 361 362fun sub_conv (rw, RW) = 363 (fn tm => 364 let 365 val (a, b) = dest_comb tm 366 in 367 case Df (total rw) (a, b) of (SOME a', SOME b') => mk_comb (a', b') 368 | (SOME a', NONE) => mk_comb (a', b) 369 | (NONE, SOME b') => mk_comb (a, b') 370 | (NONE, NONE) => raise ERR "sub_conv" "unchanged" 371 end, 372 fn tm => 373 let 374 val (a, b) = dest_comb tm 375 in 376 case Df (total (QCONV RW)) (a, b) of (SOME a', SOME b') => MK_COMB (a', b') 377 | (SOME a', NONE) => MK_COMB (a', REFL b) 378 | (NONE, SOME b') => MK_COMB (REFL a, b') 379 | (NONE, NONE) => raise ERR "sub_conv" "unchanged" 380 end); 381 382fun once_depth_conv (rw, RW) = 383 (fn tm => (rw orelsef (fst (sub_conv (once_depth_conv (rw, RW))))) tm, 384 fn tm => QCONV (RW ORELSEC (snd (sub_conv (once_depth_conv (rw, RW))))) tm); 385 386fun redepth_conv (rw, RW) = 387 (fn tm => 388 ((fst (sub_conv (redepth_conv (rw, RW))) orelsef rw) 389 thenf repeatf rw 390 thenf tryf (fst (redepth_conv (rw, RW)))) tm, 391 fn tm => 392 QCONV 393 ((snd (sub_conv (redepth_conv (rw, RW))) ORELSEC RW) 394 THENC REPEATC RW 395 THENC TRYC (snd (redepth_conv (rw, RW)))) tm); 396 397fun top_depth_conv (rw, RW) = 398 (fn tm => 399 (((repeatplusf rw thenf 400 tryf (fst (sub_conv (top_depth_conv (rw, RW))))) orelsef 401 (fst (sub_conv (top_depth_conv (rw, RW))))) thenf 402 tryf (fst (top_depth_conv (rw, RW)))) tm, 403 fn tm => 404 QCONV 405 (((REPEATPLUSC RW THENC 406 TRYC (snd (sub_conv (top_depth_conv (rw, RW))))) ORELSEC 407 (snd (sub_conv (top_depth_conv (rw, RW))))) THENC 408 TRYC (snd (top_depth_conv (rw, RW)))) tm); 409 410fun rewr_conv vths = 411 let 412 val rewrs = map (fn (vars, th) => ((vars, LHS th), (RHS th, th))) vths 413 val d = mk_ski_discrim rewrs 414 val _ = trace "rewr_conv: d" (fn () => printVal (dest_ski_discrim d)) 415 fun lookup tm = 416 (case ski_discrim_match d tm of [] => raise ERR "rewrs_conv" "unchanged" 417 | a :: _ => a) 418 val rw = (fn (sub, (r, _)) => pinst sub r) o lookup 419 val RW = (fn (sub, (_, th)) => PINST sub th) o lookup 420 fun rw' tm = 421 let 422 val _ = trace "rewr_conv: rw: tm" (fn () => printVal tm) 423 val res = rw tm 424 val _ = trace "rewr_conv: rw: res" (fn () => printVal res) 425 in 426 res 427 end 428 fun RW' tm = 429 let 430 val _ = trace "rewr_conv: RW: tm" (fn () => printVal tm) 431 val res = QCONV RW tm 432 val _ = trace "rewr_conv: RW: res" (fn () => printVal res) 433 in 434 res 435 end 436 in 437 (rw', RW') 438 end; 439 440val rewrite_conv = top_depth_conv o rewr_conv; 441val once_rewrite_conv = once_depth_conv o rewr_conv; 442 443fun conv_to_lconv (rw, RW) (lit as (pos, tm)) = 444 let 445 val _ = trace "literal_conv: lit" (fn () => printVal lit) 446 val res1 = (pos, rw tm) : literal 447 val _ = trace "literal_conv: res1" (fn () => printVal res1) 448 val res2 = 449 march_literal lit THENR 450 CONV_RULE ((if pos then I else RAND_CONV) RW) THENR 451 norm_thm 452 fun res2' th = 453 let 454 val _ = trace "conv_to_lconv: th" (fn () => printVal th) 455 val th' = res2 th 456 val _ = trace "conv_to_lconv: th'" (fn () => printVal th') 457 in 458 th' 459 end 460 in 461 (res1, res2') 462 end; 463 464fun lconv_to_crule lconv : clause_rule = 465 let 466 fun advance lit (changed, lits', rules') = 467 (case total lconv lit of NONE => (changed, lit :: lits', rules') 468 | SOME (lit', rule') => (true, lit' :: lits', rules' THENR rule')) 469 in 470 fn cl as CLAUSE (vars, lits) => 471 (case trans advance (false, [], ALL_RULE) lits of (false, _, _) 472 => raise ERR "clause_conv" "unchanged" 473 | (true, lits', rule') => 474 let 475 val cl' = CLAUSE (vars, rev lits') 476 val _ = trace "lconv_to_cconv: (cl, cl')" (fn () => printVal (cl, cl')) 477 val res = [(empty_subst, cl', rule')] 478 in 479 res 480 end) 481 end; 482 483val rewrite_frule = 484 crule_to_frule o lconv_to_crule o conv_to_lconv o rewrite_conv; 485 486val once_rewrite_frule = 487 crule_to_frule o lconv_to_crule o conv_to_lconv o once_rewrite_conv; 488 489(* ------------------------------------------------------------------------- *) 490(* Normalization has two parts: basic rewrites and rules of inference. *) 491(* *) 492(* The basic rewrites define the relationship between the combinators, *) 493(* and between the constants of the logic; an example is: !x. ~~x = x. *) 494(* *) 495(* The rules of inference propagate truth from the object level to the *) 496(* meta level; an example of this is the "conjunction" rule that takes as *) 497(* input a theorem of the form a /\ b; and outputs two theorems: a and b. *) 498(* ------------------------------------------------------------------------- *) 499 500(* First, the basic rewrites *) 501 502val basic_rewrites = 503 map (prove o (I ## (fn ths => !! FUN_EQ_TAC ++ RW_TAC bool_ss ths))) 504 [(``!x y z. S x y z = (x z) (y z)``, [S_DEF]), 505 (``!x y z. combin$C x y z = x z y``, [C_DEF]), 506 (``!x y z. (x o y) z = x (y z)``, [o_DEF]), 507 (``!x y. K x y = x``, [K_DEF]), 508 (``!x. I x = x``, [I_THM]), 509 (``!x y. S (K x) (K y) = K (x y)``, [S_DEF, K_DEF]), 510 (``!x. S (K x) = $o x``, [S_DEF, K_DEF, o_DEF]), 511 (``S o K = $o``, [S_DEF, K_DEF, o_DEF]), 512 (``!x y. S x (K y) = combin$C x y``, [S_DEF, K_DEF, C_DEF]), 513 (``!x y. x o (K y) = K (x y)``, [K_DEF, o_DEF]), 514 (``!x y. combin$C (K x) y = K (x y)``, [K_DEF, C_DEF]), 515 (``!x y. K x o y = K x``, [K_DEF, o_DEF]), 516 (``!x. x o I = x``, [I_THM, o_DEF]), 517 (``$o I = I``, [I_THM, o_DEF]), 518 (``S K K = I``, [I_THM, S_DEF, K_DEF]), 519 (``!x y z. (x o y) o z = x o (y o z)``, [o_THM]), 520 (``!x. (x = T) = x``, []), 521 (``!x. (T = x) = x``, []), 522 (``!x. (x = F) = ~x``, []), 523 (``!x. (F = x) = ~x``, []), 524 (``!x:bool. ~~x = x``, []), 525 (``!x y z w. w (if x then y else z) = if x then w y else w z``, []), 526 (``!x y z w. (if x then y else z) w = if x then y w else z w``, []), 527 (``!x y. (x ==> y) = (~x \/ y)``, [IMP_DISJ_THM]), 528 (``!x. (x = x) = T``, []), 529 (``!x y. (x = y) = (!z. x z = y z)``, []), 530 (``!x y. (x = y) = (x ==> y) /\ (y ==> x)``, [EQ_IMP_THM]), 531 (``!x y z. (if x then y else z) = (x ==> y) /\ (~x ==> z)``, [])]; 532 533val basic_rewrite_frule = 534 rewrite_frule (map ((I ## CONV_RULE SKI_CONV) o thm_to_vthm) basic_rewrites); 535 536(* Second, the basic rules of inference. *) 537 538local 539 val thm1 = prove (``!x. ~~x ==> x``, PROVE_TAC []) 540in 541 val neg_lrule : literal_rule = 542 fn (vars, lit as (pos, tm)) => 543 let 544 val body = dest_neg tm 545 in 546 [(empty_subst, vars, [(not pos, body)], 547 if pos then ALL_RULE 548 else march_literal lit THENR MATCH_MP thm1 THENR norm_thm)] 549 end 550 551 val neg_frule = lrule_to_frule neg_lrule 552end; 553 554local 555 val thm1 = prove (``~T ==> F``, PROVE_TAC []) 556in 557 val true_lrule : literal_rule = 558 fn (vars, lit as (pos, tm)) => 559 let 560 val _ = assert (Teq tm) (ERR "true_lrule" "term not T") 561 in 562 if pos then [] 563 else [(empty_subst, vars, [], march_literal lit THENR MATCH_MP thm1)] 564 end 565 566 val true_frule = lrule_to_frule true_lrule 567end; 568 569val false_lrule : literal_rule = 570 fn (vars, lit as (pos, tm)) => 571 let 572 val _ = assert (Feq tm) (ERR "false_lrule" "term not F") 573 in 574 if pos then [(empty_subst, vars, [], march_literal lit)] else [] 575 end; 576 577val false_frule = lrule_to_frule false_lrule 578 579local 580 val thm1 = prove (``!a b. (a \/ b) ==> ~a ==> ~b ==> F``, PROVE_TAC []) 581 val thm2 = prove (``!a b. ~(a \/ b) ==> ~~a ==> F``, PROVE_TAC []) 582 val thm3 = prove (``!a b. ~(a \/ b) ==> ~~b ==> F``, PROVE_TAC []) 583in 584 val disj_lrule : literal_rule = 585 fn (vars, lit as (pos, tm)) => 586 let 587 val (a, b) = dest_disj tm 588 in 589 if pos then 590 [(empty_subst, vars, [(true, a), (true, b)], 591 march_literal lit THENR MATCH_MP thm1 THENR UNDISCH THENR UNDISCH)] 592 else 593 [(empty_subst, vars, [(false, a)], 594 march_literal lit THENR MATCH_MP thm2 THENR UNDISCH), 595 (empty_subst, vars, [(false, b)], 596 march_literal lit THENR MATCH_MP thm3 THENR UNDISCH)] 597 end 598 599 val disj_frule = lrule_to_frule disj_lrule 600end; 601 602local 603 val thm1 = prove (``!a b. ~(a /\ b) ==> ~~a ==> ~~b ==> F``, PROVE_TAC []) 604 val thm2 = prove (``!a b. (a /\ b) ==> ~a ==> F``, PROVE_TAC []) 605 val thm3 = prove (``!a b. (a /\ b) ==> ~b ==> F``, PROVE_TAC []) 606in 607 val conj_lrule : literal_rule = 608 fn (vars, lit as (pos, tm)) => 609 let 610 val (a, b) = dest_conj tm 611 in 612 if pos then 613 [(empty_subst, vars, [(true, a)], 614 march_literal lit THENR MATCH_MP thm2 THENR UNDISCH), 615 (empty_subst, vars, [(true, b)], 616 march_literal lit THENR MATCH_MP thm3 THENR UNDISCH)] 617 else 618 [(empty_subst, vars, [(false, a), (false, b)], 619 march_literal lit THENR MATCH_MP thm1 THENR UNDISCH THENR UNDISCH)] 620 end 621 622 val conj_frule = lrule_to_frule conj_lrule 623end; 624 625local 626 fun mk_c ty [] = genvar ty 627 | mk_c ty (v :: vs) = mk_comb (mk_c (type_of v --> ty) vs, v) 628 629 fun var_literal vars atom = 630 let 631 val lvar = (genvar o fst o dom_rng o type_of) atom 632 val atom' = mk_comb (atom, lvar) 633 in 634 (lvar, (cons lvar ## I) vars, atom') 635 end; 636 637 fun const_literal vars atom = 638 let 639 val ctype = (fst o dom_rng o type_of) atom 640 val tm_vars = op_intersect aconv (fst vars) (free_vars atom) 641 val cvar = mk_c ctype tm_vars 642 val atom' = mk_comb (atom, cvar) 643 in 644 (cvar, atom') 645 end; 646 647 fun true_forall_th lvar = 648 CONV_RULE (RAND_CONV GENVAR_ETA_EXPAND_CONV) 649 THENR SPEC lvar 650 THENR norm_thm 651 652 fun false_forall_th cvar = 653 CONV_RULE 654 (RAND_CONV (RAND_CONV GENVAR_ETA_EXPAND_CONV) THENC NOT_FORALL_CONV) 655 THENR NEW_CONST_RULE cvar 656 THENR norm_thm 657 658 fun false_exists_th lvar = 659 CONV_RULE 660 (RAND_CONV (RAND_CONV GENVAR_ETA_EXPAND_CONV) THENC NOT_EXISTS_CONV) 661 THENR SPEC lvar 662 THENR norm_thm 663 664 fun true_exists_th cvar = 665 CONV_RULE (RAND_CONV GENVAR_ETA_EXPAND_CONV) 666 THENR NEW_CONST_RULE cvar 667 THENR norm_thm 668in 669 val forall_lrule : literal_rule = 670 fn (vars, lit as (pos, atom)) => 671 let 672 val body = dest_unaryop "!" atom 673 in 674 if pos then 675 let 676 val (lvar, vars', atom') = var_literal vars body 677 in 678 [(empty_subst, vars', [(pos, atom')], 679 march_literal lit THENR true_forall_th lvar)] 680 end 681 else 682 let 683 val (cvar, atom') = const_literal vars body 684 in 685 [(empty_subst, vars, [(pos, atom')], 686 march_literal lit THENR false_forall_th cvar)] 687 end 688 end 689 690 val exists_lrule : literal_rule = 691 fn (vars, lit as (pos, atom)) => 692 let 693 val body = dest_unaryop "?" atom 694 in 695 if pos then 696 let 697 val (cvar, atom') = const_literal vars body 698 in 699 [(empty_subst, vars, [(pos, atom')], 700 march_literal lit THENR true_exists_th cvar)] 701 end 702 else 703 let 704 val (lvar, vars', atom') = var_literal vars body 705 in 706 [(empty_subst, vars', [(pos, atom')], 707 march_literal lit THENR false_exists_th lvar)] 708 end 709 end 710 711 val forall_frule = lrule_to_frule forall_lrule 712 val exists_frule = lrule_to_frule exists_lrule 713end; 714 715local 716 val thm1 = prove 717 (``(p : bool -> 'a) x = if x then p T else p F``, RW_TAC bool_ss []); 718 val (p_tm, x_tm) = dest_comb (LHS thm1) 719 val rhs_thm1 = RHS thm1 720 721 fun get_sub tm = 722 let 723 val (a, b) = dest_comb tm 724 val (dom, rng) = dom_rng (type_of a) 725 val _ = assert (dom = bool) (ERR "bool_lrule" "not a bool") 726 val _ = assert (b !~ T andalso b !~ F) (ERR "bool_rule" "already T or F") 727 val ty_sub = if rng = alpha then [alpha |-> rng] else [] 728 val (tm_sub, ty_sub) = 729 norm_subst (([p_tm |-> a, x_tm |-> b], empty_tmset), (ty_sub, [])) 730 in 731 (tm_sub, ty_sub) 732 end; 733 734 val rewr = (C pinst rhs_thm1 o get_sub, C PINST thm1 o get_sub) 735 736 val lconv = conv_to_lconv (once_depth_conv rewr); 737in 738 val bool_lrule : literal_rule = 739 fn (vars, lit) => 740 let 741 val (lit', r) = lconv lit 742 in 743 [(empty_subst, vars, [lit'], r)] 744 end 745 746 val bool_frule = lrule_to_frule bool_lrule 747end; 748 749local 750 val thm1 = prove (``!(x : 'a). ~(x = x) ==> F``, PROVE_TAC []) 751in 752 val equal_lrule : literal_rule = 753 fn (vars, lit as (pos, atom)) => 754 let 755 val _ = assert (not pos) (ERR "equal_lrule" "positive term") 756 val (l, r) = dest_eq atom 757 in 758 if is_tmvar vars l then 759 let 760 val _ = assert (not (free_in l r)) (ERR "equal_lrule" "l free in r") 761 val sub = ([l |-> r], []) 762 in 763 [(sub, vars_after_subst vars sub, [], 764 march_literal lit THENR PINST sub THENR MATCH_MP thm1)] 765 end 766 else if is_tmvar vars r then 767 let 768 val _ = assert (not (free_in r l)) (ERR "equal_lrule" "r free in l") 769 val sub = ([r |-> l], []) 770 in 771 [(sub, vars_after_subst vars sub, [], 772 march_literal lit THENR PINST sub THENR MATCH_MP thm1)] 773 end 774 else raise ERR "equal_rule" "non-var = non-var" 775 end 776 777 val equal_frule = lrule_to_frule equal_lrule 778end; 779 780local 781 fun merge _ [] = raise ERR "factor_rule" "nothing to do" 782 | merge dealt ((lit as (pos, atom)) :: rest) = 783 if op_mem xtm_eq (not pos, atom) dealt then NONE 784 else if op_mem xtm_eq lit dealt then SOME (rev dealt @ rest) 785 else merge (lit :: dealt) rest 786 787 fun process _ NONE = [] 788 | process vars (SOME lits) = [(empty_subst, CLAUSE (vars, lits), ALL_RULE)] 789in 790 val merge_crule : clause_rule = 791 fn CLAUSE (vars, lits) => process vars (merge [] lits); 792 793 val merge_frule = crule_to_frule merge_crule 794end; 795 796val basic_cnf_frule : fact_rule = 797 first_frule 798 [neg_frule, true_frule, false_frule, disj_frule, conj_frule, 799 forall_frule, exists_frule, bool_frule, equal_frule, merge_frule]; 800 801(* ------------------------------------------------------------------------- *) 802(* The fundamental factdb. *) 803(* ------------------------------------------------------------------------- *) 804 805val empty_factdb = 806 (factdb_add_norm basic_cnf_frule o 807 factdb_add_norm basic_rewrite_frule) 808 null_factdb; 809 810val mk_factdb = trans factdb_add_thm empty_factdb; 811 812(* ------------------------------------------------------------------------- *) 813(* Fact `tactic' rules for open-ended proof search. *) 814(* ------------------------------------------------------------------------- *) 815 816(* A resolution rule. *) 817 818local 819 fun extra f = 820 let 821 val (vars, lits) = dest_clause (fact_clause f) 822 fun part (true, atom) (ts, fs) = (((vars, atom), f) :: ts, fs) 823 | part (false, atom) (ts, fs) = (ts, ((vars, atom), f) :: fs) 824 val (ts, fs) = trans part ([], []) lits 825 in 826 (ts, fs) 827 end; 828 829 fun add f (td, fd) = 830 let 831 val (ts, fs) = extra f 832 in 833 (ski_discrim_addl ts td, ski_discrim_addl fs fd) 834 end; 835in 836 fun mk_atom_db db = 837 trans add (empty_ski_discrim, empty_ski_discrim) (factdb_factl db) 838end; 839 840val mk_pos_atom_db = fst o mk_atom_db; 841val mk_neg_atom_db = snd o mk_atom_db; 842 843local 844 val thm1 = prove (``!x. x /\ ~x ==> F``, PROVE_TAC []) 845in 846 fun resolution_rule sub (pos, atom) th th' = 847 let 848 val atom' = pinst sub atom 849 val (s_th, s_th') = Df (PINST sub) (th, th') 850 val _ = 851 trace "resolution rule: ((pos, atom'), s_th, s_th')" 852 (fn () => printVal ((pos, atom'), s_th, s_th')) 853 val sm_th = march_literal (pos, atom') s_th 854 val sm_th' = march_literal (not pos, atom') s_th' 855 val _ = 856 trace "resolution rule: (sm_th, sm_th')" 857 (fn () => printVal (sm_th, sm_th')) 858 in 859 MATCH_MP thm1 (if pos then CONJ sm_th sm_th' else CONJ sm_th' sm_th) 860 end 861 862 fun lazy_resolution_rule sub atom thk thk' = 863 susp_map (uncurry (resolution_rule sub atom)) (pair_susp thk thk') 864end; 865 866local 867 fun process vars lit (sub, f as FACT (CLAUSE (vars', lits'), thk')) = 868 let 869 val res_vars = 870 vars_union (vars_after_subst vars sub) (vars_after_subst vars' sub) 871 val lit' = (not ## pinst sub) lit 872 val res_lits = (filter (not o xtm_eq lit') o map (I ## pinst sub)) lits' 873 in 874 (sub, res_vars, res_lits, 875 fn th => resolution_rule sub lit th (force thk')) 876 end 877in 878 fun pos_resolution_lrule neg_db : literal_rule = 879 fn (vars, lit as (pos, atom)) => 880 let 881 val _ = assert pos (ERR "pos_resolution_rule" "not a positive literal") 882 val matches = ski_discrim_unify neg_db (vars, atom) 883 val _ = 884 trace "pos_resolution_lrule: ((vars, lit), matches)" 885 (fn () => printVal ((vars, lit), matches)) 886 val res = map (process vars lit) matches 887 val _ = trace "pos_resolution_lrule: res" (fn () => printVal res) 888 in 889 res 890 end; 891 892 fun neg_resolution_lrule pos_db : literal_rule = 893 fn (vars, lit as (pos, atom)) => 894 let 895 val _ = 896 assert (not pos) (ERR "neg_resolution_rule" "not a negative literal") 897 val matches = ski_discrim_unify pos_db (vars, atom) 898 val _ = 899 trace "neg_resolution_lrule: ((vars, lit), matches)" 900 (fn () => printVal ((vars, lit), matches)) 901 val res = map (process vars lit) matches 902 val _ = trace "neg_resolution_lrule: res" (fn () => printVal res) 903 in 904 res 905 end; 906end; 907 908fun pos_resolution_frule neg_db : fact_rule = 909 lrule_to_frule (pos_resolution_lrule neg_db); 910 911fun neg_resolution_frule pos_db : fact_rule = 912 lrule_to_frule (neg_resolution_lrule pos_db); 913 914fun biresolution_frule db : fact_rule = 915 let 916 val (pos_db, neg_db) = mk_atom_db db 917 in 918 pos_resolution_frule neg_db join_frule neg_resolution_frule pos_db 919 end; 920 921(* K rules *) 922 923fun collect_funvars vars tm = 924 let 925 fun fvars res [] = res 926 | fvars res (tm :: rest) = 927 if is_comb tm then 928 let 929 val (a, b) = dest_comb tm 930 val res' = if is_tmvar vars a then op_insert aconv a res else res 931 in 932 fvars res' (a :: b :: rest) 933 end 934 else fvars res rest 935 val res = fvars [] [tm] 936 val _ = 937 trace "collect_funvars: ((vars, tm), res)" 938 (fn () => printVal ((vars, tm), res)) 939 in 940 res 941 end; 942 943local 944 fun k_set_var vars (pos, atom) v = 945 let 946 val (dom, rng) = dom_rng (type_of v) 947 val k = 948 mk_thy_const {Name = "K", Thy = "combin", Ty = rng --> dom --> rng} 949 val g = genvar rng 950 val res = mk_comb (k, g) 951 val sub = ([v |-> res], []) 952 val vars' = (cons g ## I) (vars_after_subst vars sub) 953 in 954 (sub, vars', [(pos, pinst sub atom)], PINST sub) 955 end 956 handle (h as HOL_ERR _) => raise err_BUG "k_set_var" h 957in 958 val k1_lrule : literal_rule = 959 fn (vars, (pos, atom)) => 960 let 961 val funvars = collect_funvars vars atom 962 in 963 map (k_set_var vars (pos, atom)) funvars 964 end 965 handle (h as HOL_ERR _) => raise err_BUG "k1_lrule" h 966end; 967 968val k1_frule = lrule_to_frule k1_lrule; 969 970(* S rules *) 971 972local 973 fun s_set_var vars (lit as (pos, atom)) v = 974 let 975 val v_type = type_of v 976 val (dom, rng) = dom_rng v_type 977 val inter = gen_tyvar () 978 val g1_type = dom --> inter --> rng 979 val g1 = genvar g1_type 980 val g2_type = dom --> inter 981 val g2 = genvar g2_type 982 val s = mk_const ("S", g1_type --> g2_type --> v_type) 983 val res = mk_comb (mk_comb (s, g1), g2) 984 val sub = ([v |-> res], []) 985 val vars' = 986 ((cons g1 o cons g2) ## cons inter) (vars_after_subst vars sub) 987 val _ = 988 trace "s_set_var: (vars, sub, vars')" 989 (fn () => printVal (vars, sub, vars')) 990 val lit' = (pos, pinst sub atom) 991 val _ = trace "s_set_var: (lit, lit')" (fn () => printVal (lit, lit')) 992 in 993 (sub, vars', [lit'], PINST sub) 994 end 995 handle (h as HOL_ERR _) => raise err_BUG "s_set_var" h 996in 997 val s1_lrule : literal_rule = 998 fn (vars, (pos, atom)) => 999 let 1000 val funvars = collect_funvars vars atom 1001 val res = map (s_set_var vars (pos, atom)) funvars 1002 in 1003 res 1004 end 1005 handle (h as HOL_ERR _) => raise err_BUG "s1_lrule" h 1006end; 1007 1008val s1_frule = lrule_to_frule s1_lrule; 1009 1010(* A variable-at-top-level rule *) 1011 1012(* A variable-in-equality rule *) 1013 1014local 1015 val thm1 = prove (``!x. ~(x = x) ==> F``, PROVE_TAC []); 1016in 1017 val equality_lrule : literal_rule = 1018 fn (vars, lit as (pos, atom)) => 1019 let 1020 val _ = assert (not pos) (ERR "equality_lrule" "positive literal") 1021 val (a, b) = dest_eq atom 1022 val sub = ski_unify vars a b 1023 val _ = 1024 trace "equality_lrule: ((vars, lit), sub)" 1025 (fn () => printVal ((vars, lit), sub)) 1026 val vars' = vars_after_subst vars sub 1027 in 1028 [(sub, vars', [], march_literal lit THENR PINST sub THENR MATCH_MP thm1)] 1029 end; 1030end; 1031 1032val equality_frule : fact_rule = lrule_to_frule equality_lrule; 1033 1034(* A paramodulation rule from the equality perspective *) 1035 1036(* A paramodulation rule from the term perspective *) 1037 1038local 1039 val thm1 = prove (``!x y : bool. (x = y) ==> (~x = ~y)``, PROVE_TAC []); 1040in 1041 fun paramodulation_rule (lit as (pos, _)) sub eq_th th = 1042 let 1043 val _ = 1044 trace "paramodulation_rule: (lit, sub, eq_th, th)" 1045 (fn () => printVal (lit, sub, eq_th, th)) 1046 val res = 1047 (march_literal lit THENR PINST sub THENR 1048 EQ_MP ((if pos then ALL_RULE else MATCH_MP thm1) eq_th) THENR 1049 norm_thm) th 1050 val _ = trace "paramodulation_rule: res" (fn () => printVal res) 1051 in 1052 res 1053 end 1054 handle h as HOL_ERR _ => raise err_BUG "paramodulation_rule" h; 1055end; 1056 1057local 1058 val thm1 = prove (``!x y. (x = y) ==> (y = x)``, PROVE_TAC []); 1059 1060 fun extra1 (sub, vars', eq, lits, rule, th) = 1061 (sub, vars', rhs eq, lits, rule, th); 1062 1063 fun extra2 (sub, vars', eq, lits, rule, th) = 1064 (sub, vars', lhs eq, lits, rule THENR MATCH_MP thm1, th); 1065 1066 fun process vars eq (sub, FACT (CLAUSE (vars', lits), th)) = 1067 let 1068 val res_vars = 1069 vars_union (vars_after_subst vars sub) (vars_after_subst vars' sub) 1070 val res_eq = pinst sub eq 1071 val res_lits = 1072 filter (not o xtm_eq (true, res_eq)) (map (I ## pinst sub) lits) 1073 val _ = assert (length res_lits < length lits) 1074 (BUG "paramodulation" "literal length check failed") 1075 in 1076 (sub, res_vars, res_eq, res_lits, 1077 PINST sub THENR march_literal (true, res_eq), th) 1078 end 1079 handle h as HOL_ERR _ => raise err_BUG "paramodulation.process" h; 1080 1081 fun find_matches pos_db vars tm = 1082 let 1083 val ty = type_of tm 1084 val g = genvar ty 1085 val vars' = (cons g ## I) vars 1086 val eq1 = mk_eq (tm, g) 1087 val res1 = ski_discrim_unify pos_db (vars', eq1) 1088 val eq2 = mk_eq (g, tm) 1089 val res2 = ski_discrim_unify pos_db (vars', eq2) 1090 val all_matches = 1091 map (extra1 o process vars' eq1) res1 @ 1092 map (extra2 o process vars' eq2) res2 1093 val _ = 1094 trace "paramodulation.find_matches: ((vars, tm), all_matches)" 1095 (fn () => printVal ((vars, tm), all_matches)) 1096 in 1097 all_matches 1098 end 1099 handle h as HOL_ERR _ => raise err_BUG "paramodulation.find_matches" h; 1100 1101 fun left_lift_para b (sub, vars', a', lits, rule, thk) = 1102 let 1103 val b' = pinst sub b 1104 in 1105 (sub, vars', mk_comb (a', b'), lits, 1106 fn th => MK_COMB (rule th, REFL b'), thk) 1107 end 1108 handle h as HOL_ERR _ => raise err_BUG "paramodulation.left_lift_para" h; 1109 1110 fun right_lift_para a (sub, vars', b', lits, rule, thk) = 1111 let 1112 val a' = pinst sub a 1113 in 1114 (sub, vars', mk_comb (a', b'), lits, 1115 fn th => MK_COMB (REFL a', rule th), thk) 1116 end 1117 handle h as HOL_ERR _ => raise err_BUG "paramodulation.right_lift_para" h; 1118 1119 fun perform_para pos_db vars = 1120 let 1121 fun para tm = 1122 (let 1123 val (a, b) = dest_comb tm 1124 in 1125 map (left_lift_para b) (para a) @ 1126 map (right_lift_para a) (para b) 1127 end 1128 handle HOL_ERR _ => []) @ 1129 (find_matches pos_db vars tm) 1130 in 1131 para 1132 end 1133 handle h as HOL_ERR _ => raise err_BUG "paramodulation.perform_para" h; 1134 1135 fun finalize (lit as (pos, _)) (sub, vars', atom', lits', rule, thk) = 1136 (sub, vars', (pos, atom') :: lits', 1137 fn th => paramodulation_rule lit sub (rule (force thk)) th) 1138 handle h as HOL_ERR _ => raise err_BUG "paramodulation.finalize" h; 1139in 1140 fun paramodulation_lrule pos_db : literal_rule = 1141 fn (vars, lit as (pos, atom)) => 1142 let 1143 val res = map (finalize lit) (perform_para pos_db vars atom) 1144 val _ = 1145 trace "paramodulation_lrule: ((vars, lit), res)" 1146 (fn () => printVal ((vars, lit), res)) 1147 in 1148 res 1149 end 1150 handle h as HOL_ERR _ => raise err_BUG "paramodulation_lrule" h; 1151end; 1152 1153fun paramodulation_frule db : fact_rule = 1154 lrule_to_frule (paramodulation_lrule (mk_pos_atom_db db)) 1155 handle h as HOL_ERR _ => raise err_BUG "paramodulation_frule" h; 1156 1157(* ------------------------------------------------------------------------- *) 1158(* The core engine. *) 1159(* ------------------------------------------------------------------------- *) 1160 1161(* prune_subfacts_wrt: using only the most general results wrt some term. *) 1162 1163fun prune_subfacts_wrt tm l = 1164 let 1165 val _ = 1166 trace "prune_subfacts_wrt: (tm, length l)" 1167 (fn () => printVal ((tm, length l))) 1168 fun tag (f as (sub, FACT (CLAUSE (vars, _), _))) = ((vars, pinst sub tm), f) 1169 val res = map snd (trans cons_subsume [] (map tag l)) 1170 val _ = 1171 trace "prune_subfacts_wrt: (tm, length l, length res)" 1172 (fn () => printVal ((tm, length l, length res))) 1173 in 1174 res 1175 end; 1176 1177local 1178 type state = literal list * (substitution * fact); 1179 1180 exception CUT of string; 1181 1182 (* Ancestor resolution *) 1183 1184 fun anc_res_frule (a_pos, a_atom) : fact_rule = 1185 fn FACT (CLAUSE (vars, [(pos, atom)]), thk) => 1186 let 1187 val _ = assert (a_pos <> pos) (ERR "anc_frule" "same polarity") 1188 val sub = ski_unify vars a_atom atom 1189 val vars' = vars_after_subst vars sub 1190 val thk' = susp_map (PINST sub) thk 1191 in 1192 [(sub, FACT (CLAUSE (vars', []), thk'))] 1193 end 1194 | _ => raise BUG "anc_frule" "panic"; 1195 1196 val ancs_res_frule = joinl_frule o map anc_res_frule; 1197in 1198 fun meson_frule_reduce_depth (reduce : fact_rule) = 1199 let 1200 fun meson _ res ([] : state list) = res 1201 | meson depth res 1202 ((_, f as (sub, FACT (CLAUSE (vars, []), _))) :: others) = 1203 if can (invert_subst vars) sub then [f] 1204 else meson depth (f :: res) others 1205 | meson depth res 1206 ((state as 1207 (ancs, (sub, goal as FACT (CLAUSE (vars, lit :: lits), thk)))) :: 1208 others) = 1209 let 1210 val _ = 1211 trace "meson: (depth, state, length others)" 1212 (fn () => printVal ((depth, state, length others))) 1213 val _ = trace "meson: sub" (fn () => printVal sub) 1214 val _ = trace "meson: goal" (fn () => printVal goal) 1215 val _ = assert (depth > 0) (CUT "hit bottom") 1216 val _ = assert (not (op_mem xtm_eq lit ancs)) (CUT "duplicate goal") 1217 val goal1 = FACT (CLAUSE (vars, [lit]), thk) 1218 val subgoals = 1219 map 1220 ((fn (a, (s, f)) => (map (I ## pinst s) a, (s, f))) o 1221 add_fst (lit :: ancs)) 1222 ((ancs_res_frule ancs join_frule reduce) goal1) 1223 val _ = 1224 trace "meson: (goal1, map snd subgoals)" 1225 (fn () => printVal (goal1, map snd subgoals)) 1226 val subresults = 1227 prune_subfacts_wrt (snd lit) (meson (depth - 1) [] subgoals) 1228 fun mp (sub', FACT (CLAUSE (vars', []), thk')) = 1229 (map (I ## pinst sub') ancs, 1230 (refine_subst sub sub', 1231 FACT (CLAUSE (vars', map (I ## pinst sub') lits), 1232 lazy_resolution_rule sub' lit thk thk'))) 1233 | mp _ = raise BUG "meson mp" "panic" 1234 val newgoals = map mp subresults 1235 val _ = 1236 trace "meson: (state, subgoals, subresults, newgoals)" 1237 (fn () => printVal (state, subgoals, subresults, newgoals)) 1238 val _ = 1239 trace "meson: map (snd o snd) newgoals" 1240 (fn () => printVal (map (snd o snd) newgoals)) 1241 in 1242 meson depth res (newgoals @ others) 1243 end 1244 handle CUT _ => meson depth res others 1245 in 1246 fn depth => fn f => meson depth [] [([], (empty_subst, f))] 1247 end 1248 handle (h as HOL_ERR _) => raise err_BUG "meson_frule_depth_frule" h; 1249end; 1250 1251fun meson_refute_reduce_depth_fact reduce depth = 1252 let 1253 val frule = 1254 fresh_vars_frule then_frule 1255 meson_frule_reduce_depth reduce depth 1256 in 1257 fn f => 1258 let 1259 val _ = trace "meson_refute_fact_reduce_depth: f" (fn () => printVal f) 1260 val res = 1261 case frule f of [] 1262 => raise ERR "meson_refute_fact_reduce_depth" "too deep" 1263 | ((_, f) :: _) 1264 => ZAP_CONSTS_RULE (snd (fact_to_vthm f)) 1265 in 1266 res 1267 end 1268 end; 1269 1270fun meson_refute_reduce_depth db reduce depth = 1271 let 1272 val _ = trace "meson_refute_reduce_depth: depth" (fn () => printVal depth) 1273 val reduce' = reduce then_frule try_frule (factdb_norm_frule db) 1274 val f = meson_refute_reduce_depth_fact reduce depth 1275 val res = 1276 case partial_first (total f) (factdb_factl db) of NONE 1277 => raise ERR "meson_refute_reduce_depth" "too deep!" 1278 | SOME th => th 1279 val _ = trace "meson_refute_reduce_depth: res" (fn () => printVal res) 1280 in 1281 res 1282 end; 1283 1284fun meson_refute_reduce_deepen db reduce = 1285 let 1286 val _ = trace "meson_refute_reduce_deepen: db" (fn () => printVal db) 1287 val refute = meson_refute_reduce_depth db reduce 1288 in 1289 fn start => fn step => 1290 let 1291 fun deepen 0 depth = 1292 raise ERR "meson_refute_deepen" "no solutions up to max depth" 1293 | deepen n depth = (refute orelsef (deepen (n - 1) o plus step)) depth 1294 in 1295 C deepen start 1296 end 1297 end; 1298 1299local 1300 fun post goal (sub, f) = 1301 let 1302 val (vars, th) = fact_to_vthm f 1303 val rule = CCONTR (pinst sub goal) THENR ZAP_CONSTS_RULE 1304 in 1305 (sub, (vars, rule th)) 1306 end 1307 1308 fun post_process goal = map (post goal) o prune_subfacts_wrt goal 1309in 1310 fun meson_prove_reduce_depth db reduce depth (vars, goal) = 1311 let 1312 val _ = trace "meson_prove_reduce_depth: db" (fn () => printVal db) 1313 val _ = 1314 trace "meson_prove_reduce_depth: (vars, goal)" 1315 (fn () => printVal (vars, goal)) 1316 val neg_goal = mk_neg goal 1317 val input = vthm_to_fact (vars, ASSUME neg_goal) 1318 val frule = 1319 fresh_vars_frule then_frule 1320 try_frule (factdb_norm_frule db) then_frule 1321 meson_frule_reduce_depth reduce depth 1322 val res = (post_process goal o frule) input 1323 val _ = 1324 trace "meson_prove_reduce_depth: ((vars, goal), res)" 1325 (fn () => printVal ((vars, goal), res)) 1326 in 1327 res 1328 end 1329 handle (h as HOL_ERR _) => raise err_BUG "meson_prove_reduce_depth" h; 1330end; 1331 1332(* ------------------------------------------------------------------------ *) 1333(* The HOL tactic *) 1334(* ------------------------------------------------------------------------ *) 1335 1336(* Tuning parameters *) 1337 1338val prover_depth = ref 3; 1339val prover_start = ref 1; 1340val prover_step = ref 1; 1341val prover_steps = ref 10; 1342 1343(* The higher-order fact rule we use *) 1344 1345fun ho_meson_frule db : fact_rule = 1346 joinl_frule 1347 [biresolution_frule db then_frule fresh_vars_frule, 1348 paramodulation_frule db then_frule fresh_vars_frule, 1349 equality_frule, k1_frule, s1_frule] then_frule 1350 try_frule (factdb_norm_frule db); 1351 1352(* The calls to meson with the rule and default depths *) 1353 1354fun ho_refute db = 1355 meson_refute_reduce_deepen db (ho_meson_frule db) (!prover_start) 1356 (!prover_step) (!prover_steps); 1357 1358fun ho_prove db vgoal = 1359 meson_prove_reduce_depth db (ho_meson_frule db) (!prover_depth) vgoal; 1360 1361(* Simple strip tac to reduce the problem before beginning *) 1362 1363val ho_PROVE_INITIAL_TAC = REPEAT (EQ_TAC || STRIP_TAC); 1364 1365(* The tactic *) 1366 1367fun ho_PROVE_TAC ths = 1368 ho_PROVE_INITIAL_TAC 1369 ++ CCONTR_TAC 1370 ++ EVERY (map ASSUME_TAC ths) 1371 ++ ASSUM_LIST (ACCEPT_TAC o ho_refute o mk_factdb); 1372 1373(* A more convenient entry point to the tactic for general proving *) 1374 1375fun ho_PROVE ths goal = prove (goal, ho_PROVE_TAC ths); 1376 1377(* test goals 1378 1379allow_trace "vterm_to_ski_patterns"; 1380allow_trace "literal_conv"; 1381allow_trace "rewr_conv"; 1382allow_trace "fact_conv"; 1383allow_trace "ski_discrim_unify"; 1384allow_trace "resolution"; 1385allow_trace "collect_funvars"; 1386allow_trace "equality_lrule"; 1387allow_trace "crule_to_frule"; 1388allow_trace "conv_to_lconv"; 1389allow_trace "lconv_to_cconv"; 1390allow_trace "s_set_var"; 1391allow_trace "paramodulation"; 1392allow_trace "meson: (goal1, map (snd o snd) subgoals)"; 1393allow_trace ""; 1394reset_traces (); 1395allow_trace "meson"; 1396deny_trace "meson:"; 1397 1398tt2 ho_PROVE [] ``!a. F ==> a``; 1399tt2 ho_PROVE [] ``!a. a ==> a``; 1400tt2 ho_PROVE [] ``!x y : bool. (x \/ ~y) /\ (~x \/ y) /\ P x ==> P y``; 1401tt2 ho_PROVE [] ``?guy. drinks guy ==> (!people : 'pub. drinks people)``; 1402tt2 ho_PROVE [] ``P 3 \/ ?x. (x = 3) /\ ~P 3``; 1403tt2 ho_PROVE [] ``P c /\ (!a. P a ==> Q a) ==> Q c``; 1404tt2 ho_PROVE [] ``~?a b. (a \/ b) /\ (~a \/ b) /\ (a \/ ~b) /\ (~a \/ ~b)``; 1405tt2 ho_PROVE [] ``!a b c. ~(~(a = b) = c) = ~(a = ~(b = c))``; 1406tt2 ho_PROVE [] ``!(a : bool) b. P a /\ (a = b) ==> P b``; 1407tt2 ho_PROVE [] ``(!x. x IN s ==> x IN t /\ x IN u) = 1408 (!x. x IN s ==> x IN t) /\ !x. x IN s ==> x IN u``; 1409tt2 ho_PROVE [] ``?x. !y. x y = 1 + y``; 1410tt2 ho_PROVE [] ``?x. !y. x y = y + 1``; 1411tt2 ho_PROVE [] ``?x. x a b c = (a c) (b c)``; 1412tt2 ho_PROVE [] ``!P a b. (a = b) /\ P a ==> P b``; 1413tt2 ho_PROVE [] ``!a b. ?x : 'a. P a \/ P b ==> P x``; 1414tt2 ho_PROVE [] ``(!se : num. ?n : num. f n se se) ==> ?m : num. f m 0 0 ``; 1415tt2 ho_PROVE [] ``(!x : 'a. F0 a x \/ !y. F0 x y) ==> ?x. !y. F0 x y``; 1416tt2 ho_PROVE [] 1417 ``((a : 'a = b) \/ (c = d)) /\ ((a = c) \/ (b = d)) ==> (a = d) \/ (b = c)``; 1418tt2 ho_PROVE [] ``!a b : bool. (a = b) ==> (P a = P b)``; 1419tt2 ho_PROVE [] ``!a b. (a ==> b) /\ (b ==> a) ==> (P a = P b)``; 1420 1421(* bugs? 1422tt2 ho_PROVE [INTER_FINITE, INTER_COMM] 1423 ``!s. FINITE s ==> !t. FINITE (t INTER s)``; 1424tt2 ho_PROVE [LENGTH_NIL] ``LENGTH ([]:num list) = 0``; 1425tt2 ho_PROVE [IN_EMPTY] ``x IN {}``; 1426*) 1427 1428(* 1429tt2 ho_PROVE [] ``?x. !a. x a = a``; 1430tt2 ho_PROVE [] ``?x. !a b c. x a b c = (a c) (b c)``; 1431tt2 ho_PROVE [] 1432 ``!(f : 'a -> 'c) (g : 'a -> 'b). 1433 (!x y. (g x = g y) ==> (f x = f y)) ==> (?h. !x. h (g x) = f x)``; 1434tt2 ho_PROVE [] ``?x. !a b. a ==> b = x a b``; 1435tt2 ho_PROVE [] ``?x. !a b. b ==> a = x a b``; 1436tt2 ho_PROVE [] ``?x. !a b. (b = a) = x a b``; 1437*) 1438 1439(* Difficult bug produced by cyclic substitutions *) 1440tt2 ho_PROVE [] ``(!x. y = g (c x)) ==> (?z. y = g z)``; 1441 1442(* Eric *) 1443tt2 ho_PROVE [] 1444 ``!P Q R. !x : 'a. ?v w. !y (z : 'b). 1445 P x /\ Q y ==> (P v \/ R w) /\ (R z ==> Q v)``; 1446 1447(* I think this needs paramodulation-from-the-equality-perspective 1448val P49 = 1449 ``(?x y. !z : 'a. (z = x) \/ (z = y)) /\ 1450 P a /\ P b /\ ~(a = b) ==> !x : 'a. P x``; 1451tt2 ho_PROVE [] P49; 1452*) 1453 1454(* Los : this takes 116s, must reduce this somehow... 1455val LOS = 1456 ``(!x y z. P x y /\ P y z ==> P x z) /\ 1457 (!x y z. Q x y /\ Q y z ==> Q x z) /\ 1458 (!x y. P x y ==> P y x) /\ 1459 (!x y. P x y \/ Q x y) ==> 1460 (!x y. P x y) \/ (!x y. Q x y)``; 1461tt2 PROVE [] `^LOS`; 1462tt2 ho_PROVE [] LOS; 1463*) 1464 1465(* Equality-free Agatha *) 1466tt2 ho_PROVE [] 1467 ``lives(agatha) /\ lives(butler) /\ lives(charles) /\ 1468 (killed(agatha,agatha) \/ killed(butler,agatha) \/ 1469 killed(charles,agatha)) /\ 1470 (!x y. killed(x,y) ==> hates(x,y) /\ ~richer(x,y)) /\ 1471 (!x. hates(agatha,x) ==> ~hates(charles,x)) /\ 1472 (hates(agatha,agatha) /\ hates(agatha,charles)) /\ 1473 (!x. lives(x) /\ ~richer(x,agatha) ==> hates(butler,x)) /\ 1474 (!x. hates(agatha,x) ==> hates(butler,x)) /\ 1475 (!x. ~hates(x,agatha) \/ ~hates(x,butler) \/ ~hates(x,charles)) ==> 1476 (?x : 'person. killed(x,agatha))``; 1477 1478(* Agatha 1479tt2 ho_PROVE [] 1480 ``(?x : 'a. lives x /\ killed x agatha) /\ 1481 (lives agatha /\ lives butler /\ lives charles) /\ 1482 (!x. lives x ==> (x = agatha) \/ (x = butler) \/ (x = charles)) /\ 1483 (!y x. killed x y ==> hates x y) /\ 1484 (!x y. killed x y ==> ~richer x y) /\ 1485 (!x. hates agatha x ==> ~hates charles x) /\ 1486 (!x. ~(x = butler) ==> hates agatha x) /\ 1487 (!x. ~richer x agatha ==> hates butler x) /\ 1488 (!x. hates agatha x ==> hates butler x) /\ 1489 (!x. ?y. ~hates x y) /\ 1490 ~(agatha = butler) ==> 1491 killed agatha agatha``; 1492*) 1493 1494(* The steamroller 1495tt2 ho_PROVE [] 1496 ``((!x:'a. P1 x ==> P0 x) /\ (?x. P1 x)) /\ 1497 ((!x. P2 x ==> P0 x) /\ (?x. P2 x)) /\ 1498 ((!x. P3 x ==> P0 x) /\ (?x. P3 x)) /\ 1499 ((!x. P4 x ==> P0 x) /\ (?x. P4 x)) /\ 1500 ((!x. P5 x ==> P0 x) /\ (?x. P5 x)) /\ 1501 ((?x. Q1 x) /\ (!x. Q1 x ==> Q0 x)) /\ 1502 (!x. P0 x ==> (!y. Q0 y ==> R x y) \/ 1503 (((!y. P0 y /\ S0 y x /\ ?z. Q0 z /\ R y z) ==> R x y))) /\ 1504 (!x y. P3 y /\ (P5 x \/ P4 x) ==> S0 x y) /\ 1505 (!x y. P3 x /\ P2 y ==> S0 x y) /\ 1506 (!x y. P2 x /\ P1 y ==> S0 x y) /\ 1507 (!x y. P1 x /\ (P2 y \/ Q1 y) ==> ~(R x y)) /\ 1508 (!x y. P3 x /\ P4 y ==> R x y) /\ 1509 (!x y. P3 x /\ P5 y ==> ~(R x y)) /\ 1510 (!x. (P4 x \/ P5 x) ==> ?y. Q0 y /\ R x y) ==> 1511 ?x y. P0 x /\ P0 y /\ ?z. Q1 z /\ R y z /\ R x y``; 1512*) 1513 1514(* Unskolemized Melham *) 1515tt2 ho_PROVE [] 1516 ``(!x y. (g x = g y) ==> (f x = f y)) ==> 1517 (!y. ?h. !x. (y = g x) ==> (h = f x))``; 1518 1519(* Full Melham *) 1520val lemma = tt prove 1521 (``!(f : 'a -> 'c) (g : 'a -> 'b). 1522 (!x y. (g x = g y) ==> (f x = f y)) ==> 1523 ?h. !y x. (y = g x) ==> (h y = f x)``, 1524 !! STRIP_TAC 1525 (*the following should work, but doesn't, so we use the below instead 1526 ++ Ho_rewrite.PURE_REWRITE_TAC [GSYM Ho_boolTheory.SKOLEM_THM]*) 1527 ++ MP_TAC (Q.ISPEC `\ (y : 'b) (hy : 'c). !x. (y = g x) ==> (hy = f x)` 1528 (GSYM Ho_boolTheory.SKOLEM_THM)) 1529 ++ BETA_TAC 1530 ++ DISCH_THEN (ho_REWRITE_TAC o wrap) 1531 ++ ho_PROVE_TAC []); 1532 1533val MELHAM = tt prove 1534 (``!(f : 'a -> 'c) (g : 'a -> 'b). 1535 (!x y. (g x = g y) ==> (f x = f y)) ==> 1536 (?h. !x. h (g x) = f x)``, 1537 ho_PROVE_TAC [lemma]); 1538 1539(* A couple of token prove goals *) 1540 1541tt2 ho_prove (mk_factdb [ASSUME ``P (c : 'a) : bool``, 1542 ASSUME ``?x : 'a. P x``]) 1543(([``y : 'a``], []), ``P (y : 'a) : bool``); 1544 1545tt2 ho_prove empty_factdb 1546(([``x : ('a -> 'b -> 'c) -> ('a -> 'b) -> 'a -> 'c``], []), 1547 ``(x : ('a -> 'b -> 'c) -> ('a -> 'b) -> 'a -> 'c) a b c = (a c) (b c)``); 1548 1549end of test goals *) 1550 1551 1552(* non-interactive mode 1553*) 1554end; 1555