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