1(* Title: Provers/blast.ML 2 Author: Lawrence C Paulson, Cambridge University Computer Laboratory 3 Copyright 1997 University of Cambridge 4 5Generic tableau prover with proof reconstruction 6 7 SKOLEMIZES ReplaceI WRONGLY: allow new vars in prems, or forbid such rules?? 8 Needs explicit instantiation of assumptions? 9 10Given the typeargs system, constructor Const could be eliminated, with 11TConst replaced by a constructor that takes the typargs list as an argument. 12However, Const is heavily used for logical connectives. 13 14Blast_tac is often more powerful than fast_tac, but has some limitations. 15Blast_tac... 16 * ignores wrappers (addss, addbefore, addafter, addWrapper, ...); 17 this restriction is intrinsic 18 * ignores elimination rules that don't have the correct format 19 (conclusion must be a formula variable) 20 * rules must not require higher-order unification, e.g. apply_type in ZF 21 + message "Function unknown's argument not a bound variable" relates to this 22 * its proof strategy is more general but can actually be slower 23 24Known problems: 25 "Recursive" chains of rules can sometimes exclude other unsafe formulae 26 from expansion. This happens because newly-created formulae always 27 have priority over existing ones. But obviously recursive rules 28 such as transitivity are treated specially to prevent this. Sometimes 29 the formulae get into the wrong order (see WRONG below). 30 31 With substition for equalities (hyp_subst_tac): 32 When substitution affects an unsafe formula or literal, it is moved 33 back to the list of safe formulae. 34 But there's no way of putting it in the right place. A "moved" or 35 "no DETERM" flag would prevent proofs failing here. 36*) 37 38signature BLAST_DATA = 39sig 40 structure Classical: CLASSICAL 41 val Trueprop_const: string * typ 42 val equality_name: string 43 val not_name: string 44 val notE: thm (* [| ~P; P |] ==> R *) 45 val ccontr: thm 46 val hyp_subst_tac: Proof.context -> bool -> int -> tactic 47end; 48 49signature BLAST = 50sig 51 exception TRANS of string (*reports translation errors*) 52 datatype term = 53 Const of string * term list 54 | Skolem of string * term option Unsynchronized.ref list 55 | Free of string 56 | Var of term option Unsynchronized.ref 57 | Bound of int 58 | Abs of string*term 59 | $ of term*term; 60 val depth_tac: Proof.context -> int -> int -> tactic 61 val depth_limit: int Config.T 62 val trace: bool Config.T 63 val stats: bool Config.T 64 val blast_tac: Proof.context -> int -> tactic 65 (*debugging tools*) 66 type branch 67 val tryIt: Proof.context -> int -> string -> 68 {fullTrace: branch list list, 69 result: ((int -> tactic) list * branch list list * (int * int * exn) list)} 70end; 71 72functor Blast(Data: BLAST_DATA): BLAST = 73struct 74 75structure Classical = Data.Classical; 76 77(* options *) 78 79val depth_limit = Attrib.setup_config_int @{binding blast_depth_limit} (K 20); 80val (trace, _) = Attrib.config_bool @{binding blast_trace} (K false); 81val (stats, _) = Attrib.config_bool @{binding blast_stats} (K false); 82 83 84datatype term = 85 Const of string * term list (*typargs constant--as a term!*) 86 | Skolem of string * term option Unsynchronized.ref list 87 | Free of string 88 | Var of term option Unsynchronized.ref 89 | Bound of int 90 | Abs of string*term 91 | op $ of term*term; 92 93(*Pending formulae carry md (may duplicate) flags*) 94type branch = 95 {pairs: ((term*bool) list * (*safe formulae on this level*) 96 (term*bool) list) list, (*unsafe formulae on this level*) 97 lits: term list, (*literals: irreducible formulae*) 98 vars: term option Unsynchronized.ref list, (*variables occurring in branch*) 99 lim: int}; (*resource limit*) 100 101 102(* global state information *) 103 104datatype state = State of 105 {ctxt: Proof.context, 106 names: Name.context Unsynchronized.ref, 107 fullTrace: branch list list Unsynchronized.ref, 108 trail: term option Unsynchronized.ref list Unsynchronized.ref, 109 ntrail: int Unsynchronized.ref, 110 nclosed: int Unsynchronized.ref, 111 ntried: int Unsynchronized.ref} 112 113fun reserved_const thy c = 114 is_some (Sign.const_type thy c) andalso 115 error ("blast: theory contains reserved constant " ^ quote c); 116 117fun initialize ctxt = 118 let 119 val thy = Proof_Context.theory_of ctxt; 120 val _ = reserved_const thy "*Goal*"; 121 val _ = reserved_const thy "*False*"; 122 in 123 State 124 {ctxt = ctxt, 125 names = Unsynchronized.ref (Variable.names_of ctxt), 126 fullTrace = Unsynchronized.ref [], 127 trail = Unsynchronized.ref [], 128 ntrail = Unsynchronized.ref 0, 129 nclosed = Unsynchronized.ref 0, (*number of branches closed during the search*) 130 ntried = Unsynchronized.ref 1} (*number of branches created by splitting (counting from 1)*) 131 end; 132 133fun gensym (State {names, ...}) x = 134 Unsynchronized.change_result names (Name.variant x); 135 136 137(** Basic syntactic operations **) 138 139fun is_Var (Var _) = true 140 | is_Var _ = false; 141 142fun dest_Var (Var x) = x; 143 144fun rand (f$x) = x; 145 146(* maps (f, [t1,...,tn]) to f(t1,...,tn) *) 147val list_comb : term * term list -> term = Library.foldl (op $); 148 149(* maps f(t1,...,tn) to (f, [t1,...,tn]) ; naturally tail-recursive*) 150fun strip_comb u : term * term list = 151 let fun stripc (f$t, ts) = stripc (f, t::ts) 152 | stripc x = x 153 in stripc(u,[]) end; 154 155(* maps f(t1,...,tn) to f , which is never a combination *) 156fun head_of (f$t) = head_of f 157 | head_of u = u; 158 159 160(** Particular constants **) 161 162fun negate P = Const (Data.not_name, []) $ P; 163 164fun isNot (Const (c, _) $ _) = c = Data.not_name 165 | isNot _ = false; 166 167fun mkGoal P = Const ("*Goal*", []) $ P; 168 169fun isGoal (Const ("*Goal*", _) $ _) = true 170 | isGoal _ = false; 171 172val (TruepropC, TruepropT) = Data.Trueprop_const; 173 174fun mk_Trueprop t = Term.$ (Term.Const (TruepropC, TruepropT), t); 175 176fun strip_Trueprop (tm as Const (c, _) $ t) = if c = TruepropC then t else tm 177 | strip_Trueprop tm = tm; 178 179 180 181(*** Dealing with overloaded constants ***) 182 183(*alist is a map from TVar names to Vars. We need to unify the TVars 184 faithfully in order to track overloading*) 185fun fromType alist (Term.Type(a,Ts)) = list_comb (Const (a, []), map (fromType alist) Ts) 186 | fromType alist (Term.TFree(a,_)) = Free a 187 | fromType alist (Term.TVar (ixn,_)) = 188 (case (AList.lookup (op =) (!alist) ixn) of 189 NONE => let val t' = Var (Unsynchronized.ref NONE) 190 in alist := (ixn, t') :: !alist; t' 191 end 192 | SOME v => v) 193 194fun fromConst thy alist (a, T) = 195 Const (a, map (fromType alist) (Sign.const_typargs thy (a, T))); 196 197 198(*Tests whether 2 terms are alpha-convertible; chases instantiations*) 199fun (Const (a, ts)) aconv (Const (b, us)) = a = b andalso aconvs (ts, us) 200 | (Skolem (a,_)) aconv (Skolem (b,_)) = a = b (*arglists must then be equal*) 201 | (Free a) aconv (Free b) = a = b 202 | (Var (Unsynchronized.ref(SOME t))) aconv u = t aconv u 203 | t aconv (Var (Unsynchronized.ref (SOME u))) = t aconv u 204 | (Var v) aconv (Var w) = v=w (*both Vars are un-assigned*) 205 | (Bound i) aconv (Bound j) = i=j 206 | (Abs(_,t)) aconv (Abs(_,u)) = t aconv u 207 | (f$t) aconv (g$u) = (f aconv g) andalso (t aconv u) 208 | _ aconv _ = false 209and aconvs ([], []) = true 210 | aconvs (t :: ts, u :: us) = t aconv u andalso aconvs (ts, us) 211 | aconvs _ = false; 212 213 214fun mem_term (_, []) = false 215 | mem_term (t, t'::ts) = t aconv t' orelse mem_term(t,ts); 216 217fun ins_term(t,ts) = if mem_term(t,ts) then ts else t :: ts; 218 219fun mem_var (v: term option Unsynchronized.ref, []) = false 220 | mem_var (v, v'::vs) = v=v' orelse mem_var(v,vs); 221 222fun ins_var(v,vs) = if mem_var(v,vs) then vs else v :: vs; 223 224 225(** Vars **) 226 227(*Accumulates the Vars in the term, suppressing duplicates*) 228fun add_term_vars (Skolem(a,args), vars) = add_vars_vars(args,vars) 229 | add_term_vars (Var (v as Unsynchronized.ref NONE), vars) = ins_var (v, vars) 230 | add_term_vars (Var (Unsynchronized.ref (SOME u)), vars) = add_term_vars (u, vars) 231 | add_term_vars (Const (_, ts), vars) = add_terms_vars (ts, vars) 232 | add_term_vars (Abs (_, body), vars) = add_term_vars (body, vars) 233 | add_term_vars (f $ t, vars) = add_term_vars (f, add_term_vars (t, vars)) 234 | add_term_vars (_, vars) = vars 235(*Term list version. [The fold functionals are slow]*) 236and add_terms_vars ([], vars) = vars 237 | add_terms_vars (t::ts, vars) = add_terms_vars (ts, add_term_vars(t,vars)) 238(*Var list version.*) 239and add_vars_vars ([], vars) = vars 240 | add_vars_vars (Unsynchronized.ref (SOME u) :: vs, vars) = 241 add_vars_vars (vs, add_term_vars(u,vars)) 242 | add_vars_vars (v::vs, vars) = (*v must be a ref NONE*) 243 add_vars_vars (vs, ins_var (v, vars)); 244 245 246(*Chase assignments in "vars"; return a list of unassigned variables*) 247fun vars_in_vars vars = add_vars_vars(vars,[]); 248 249 250 251(*increment a term's non-local bound variables 252 inc is increment for bound variables 253 lev is level at which a bound variable is considered 'loose'*) 254fun incr_bv (inc, lev, u as Bound i) = if i>=lev then Bound(i+inc) else u 255 | incr_bv (inc, lev, Abs(a,body)) = Abs(a, incr_bv(inc,lev+1,body)) 256 | incr_bv (inc, lev, f$t) = incr_bv(inc,lev,f) $ incr_bv(inc,lev,t) 257 | incr_bv (inc, lev, u) = u; 258 259fun incr_boundvars 0 t = t 260 | incr_boundvars inc t = incr_bv(inc,0,t); 261 262 263(*Accumulate all 'loose' bound vars referring to level 'lev' or beyond. 264 (Bound 0) is loose at level 0 *) 265fun add_loose_bnos (Bound i, lev, js) = if i<lev then js 266 else insert (op =) (i - lev) js 267 | add_loose_bnos (Abs (_,t), lev, js) = add_loose_bnos (t, lev+1, js) 268 | add_loose_bnos (f$t, lev, js) = 269 add_loose_bnos (f, lev, add_loose_bnos (t, lev, js)) 270 | add_loose_bnos (_, _, js) = js; 271 272fun loose_bnos t = add_loose_bnos (t, 0, []); 273 274fun subst_bound (arg, t) : term = 275 let fun subst (t as Bound i, lev) = 276 if i<lev then t (*var is locally bound*) 277 else if i=lev then incr_boundvars lev arg 278 else Bound(i-1) (*loose: change it*) 279 | subst (Abs(a,body), lev) = Abs(a, subst(body,lev+1)) 280 | subst (f$t, lev) = subst(f,lev) $ subst(t,lev) 281 | subst (t,lev) = t 282 in subst (t,0) end; 283 284 285(*Normalize...but not the bodies of ABSTRACTIONS*) 286fun norm t = case t of 287 Skolem (a, args) => Skolem (a, vars_in_vars args) 288 | Const (a, ts) => Const (a, map norm ts) 289 | (Var (Unsynchronized.ref NONE)) => t 290 | (Var (Unsynchronized.ref (SOME u))) => norm u 291 | (f $ u) => (case norm f of 292 Abs(_,body) => norm (subst_bound (u, body)) 293 | nf => nf $ norm u) 294 | _ => t; 295 296 297(*Weak (one-level) normalize for use in unification*) 298fun wkNormAux t = case t of 299 (Var v) => (case !v of 300 SOME u => wkNorm u 301 | NONE => t) 302 | (f $ u) => (case wkNormAux f of 303 Abs(_,body) => wkNorm (subst_bound (u, body)) 304 | nf => nf $ u) 305 | Abs (a,body) => (*eta-contract if possible*) 306 (case wkNormAux body of 307 nb as (f $ t) => 308 if member (op =) (loose_bnos f) 0 orelse wkNorm t <> Bound 0 309 then Abs(a,nb) 310 else wkNorm (incr_boundvars ~1 f) 311 | nb => Abs (a,nb)) 312 | _ => t 313and wkNorm t = case head_of t of 314 Const _ => t 315 | Skolem(a,args) => t 316 | Free _ => t 317 | _ => wkNormAux t; 318 319 320(*Does variable v occur in u? For unification. 321 Dangling bound vars are also forbidden.*) 322fun varOccur v = 323 let fun occL lev [] = false (*same as (exists occ), but faster*) 324 | occL lev (u::us) = occ lev u orelse occL lev us 325 and occ lev (Var w) = 326 v=w orelse 327 (case !w of NONE => false 328 | SOME u => occ lev u) 329 | occ lev (Skolem(_,args)) = occL lev (map Var args) 330 (*ignore Const, since term variables can't occur in types (?) *) 331 | occ lev (Bound i) = lev <= i 332 | occ lev (Abs(_,u)) = occ (lev+1) u 333 | occ lev (f$u) = occ lev u orelse occ lev f 334 | occ lev _ = false; 335 in occ 0 end; 336 337exception UNIFY; 338 339 340(*Restore the trail to some previous state: for backtracking*) 341fun clearTo (State {ntrail, trail, ...}) n = 342 while !ntrail<>n do 343 (hd(!trail) := NONE; 344 trail := tl (!trail); 345 ntrail := !ntrail - 1); 346 347 348(*First-order unification with bound variables. 349 "vars" is a list of variables local to the rule and NOT to be put 350 on the trail (no point in doing so) 351*) 352fun unify state (vars,t,u) = 353 let val State {ntrail, trail, ...} = state 354 val n = !ntrail 355 fun update (t as Var v, u) = 356 if t aconv u then () 357 else if varOccur v u then raise UNIFY 358 else if mem_var(v, vars) then v := SOME u 359 else (*avoid updating Vars in the branch if possible!*) 360 if is_Var u andalso mem_var(dest_Var u, vars) 361 then dest_Var u := SOME t 362 else (v := SOME u; 363 trail := v :: !trail; ntrail := !ntrail + 1) 364 fun unifyAux (t,u) = 365 case (wkNorm t, wkNorm u) of 366 (nt as Var v, nu) => update(nt,nu) 367 | (nu, nt as Var v) => update(nt,nu) 368 | (Const(a,ats), Const(b,bts)) => if a=b then unifysAux(ats,bts) 369 else raise UNIFY 370 | (Abs(_,t'), Abs(_,u')) => unifyAux(t',u') 371 (*NB: can yield unifiers having dangling Bound vars!*) 372 | (f$t', g$u') => (unifyAux(f,g); unifyAux(t',u')) 373 | (nt, nu) => if nt aconv nu then () else raise UNIFY 374 and unifysAux ([], []) = () 375 | unifysAux (t :: ts, u :: us) = (unifyAux (t, u); unifysAux (ts, us)) 376 | unifysAux _ = raise UNIFY; 377 in (unifyAux(t,u); true) handle UNIFY => (clearTo state n; false) 378 end; 379 380 381(*Convert from "real" terms to prototerms; eta-contract. 382 Code is similar to fromSubgoal.*) 383fun fromTerm thy t = 384 let val alistVar = Unsynchronized.ref [] 385 and alistTVar = Unsynchronized.ref [] 386 fun from (Term.Const aT) = fromConst thy alistTVar aT 387 | from (Term.Free (a,_)) = Free a 388 | from (Term.Bound i) = Bound i 389 | from (Term.Var (ixn,T)) = 390 (case (AList.lookup (op =) (!alistVar) ixn) of 391 NONE => let val t' = Var (Unsynchronized.ref NONE) 392 in alistVar := (ixn, t') :: !alistVar; t' 393 end 394 | SOME v => v) 395 | from (Term.Abs (a,_,u)) = 396 (case from u of 397 u' as (f $ Bound 0) => 398 if member (op =) (loose_bnos f) 0 then Abs(a,u') 399 else incr_boundvars ~1 f 400 | u' => Abs(a,u')) 401 | from (Term.$ (f,u)) = from f $ from u 402 in from t end; 403 404(*A debugging function: replaces all Vars by dummy Frees for visual inspection 405 of whether they are distinct. Function revert undoes the assignments.*) 406fun instVars t = 407 let val name = Unsynchronized.ref "a" 408 val updated = Unsynchronized.ref [] 409 fun inst (Const(a,ts)) = List.app inst ts 410 | inst (Var(v as Unsynchronized.ref NONE)) = (updated := v :: (!updated); 411 v := SOME (Free ("?" ^ !name)); 412 name := Symbol.bump_string (!name)) 413 | inst (Abs(a,t)) = inst t 414 | inst (f $ u) = (inst f; inst u) 415 | inst _ = () 416 fun revert() = List.app (fn v => v:=NONE) (!updated) 417 in inst t; revert end; 418 419 420(* A1==>...An==>B goes to [A1,...,An], where B is not an implication *) 421fun strip_imp_prems (Const (@{const_name Pure.imp}, _) $ A $ B) = 422 strip_Trueprop A :: strip_imp_prems B 423 | strip_imp_prems _ = []; 424 425(* A1==>...An==>B goes to B, where B is not an implication *) 426fun strip_imp_concl (Const (@{const_name Pure.imp}, _) $ A $ B) = strip_imp_concl B 427 | strip_imp_concl A = strip_Trueprop A; 428 429 430 431(*** Conversion of Elimination Rules to Tableau Operations ***) 432 433exception ElimBadConcl and ElimBadPrem; 434 435(*The conclusion becomes the goal/negated assumption *False*: delete it! 436 If we don't find it then the premise is ill-formed and could cause 437 PROOF FAILED*) 438fun delete_concl [] = raise ElimBadPrem 439 | delete_concl (P :: Ps) = 440 (case P of 441 Const (c, _) $ Var (Unsynchronized.ref (SOME (Const ("*False*", _)))) => 442 if c = "*Goal*" orelse c = Data.not_name then Ps 443 else P :: delete_concl Ps 444 | _ => P :: delete_concl Ps); 445 446fun skoPrem state vars (Const (@{const_name Pure.all}, _) $ Abs (_, P)) = 447 skoPrem state vars (subst_bound (Skolem (gensym state "S", vars), P)) 448 | skoPrem _ _ P = P; 449 450fun convertPrem t = 451 delete_concl (mkGoal (strip_imp_concl t) :: strip_imp_prems t); 452 453(*Expects elimination rules to have a formula variable as conclusion*) 454fun convertRule state vars t = 455 let val (P::Ps) = strip_imp_prems t 456 val Var v = strip_imp_concl t 457 in v := SOME (Const ("*False*", [])); 458 (P, map (convertPrem o skoPrem state vars) Ps) 459 end 460 handle Bind => raise ElimBadConcl; 461 462 463(*Like dup_elim, but puts the duplicated major premise FIRST*) 464fun rev_dup_elim ctxt th = (th RSN (2, revcut_rl)) |> Thm.assumption (SOME ctxt) 2 |> Seq.hd; 465 466 467(*Rotate the assumptions in all new subgoals for the LIFO discipline*) 468local 469 (*Count new hyps so that they can be rotated*) 470 fun nNewHyps [] = 0 471 | nNewHyps (Const ("*Goal*", _) $ _ :: Ps) = nNewHyps Ps 472 | nNewHyps (P::Ps) = 1 + nNewHyps Ps; 473 474 fun rot_tac [] i st = Seq.single st 475 | rot_tac (0::ks) i st = rot_tac ks (i+1) st 476 | rot_tac (k::ks) i st = rot_tac ks (i+1) (Thm.rotate_rule (~k) i st); 477in 478fun rot_subgoals_tac (rot, rl) = 479 rot_tac (if rot then map nNewHyps rl else []) 480end; 481 482 483fun cond_tracing true msg = tracing (msg ()) 484 | cond_tracing false _ = (); 485 486fun TRACE ctxt rl tac i st = 487 (cond_tracing (Config.get ctxt trace) (fn () => Thm.string_of_thm ctxt rl); tac i st); 488 489(*Resolution/matching tactics: if upd then the proof state may be updated. 490 Matching makes the tactics more deterministic in the presence of Vars.*) 491fun emtac ctxt upd rl = 492 TRACE ctxt rl (if upd then eresolve_tac ctxt [rl] else ematch_tac ctxt [rl]); 493 494fun rmtac ctxt upd rl = 495 TRACE ctxt rl (if upd then resolve_tac ctxt [rl] else match_tac ctxt [rl]); 496 497(*Tableau rule from elimination rule. 498 Flag "upd" says that the inference updated the branch. 499 Flag "dup" requests duplication of the affected formula.*) 500fun fromRule (state as State {ctxt, ...}) vars rl0 = 501 let 502 val thy = Proof_Context.theory_of ctxt 503 val rl = Thm.transfer thy rl0 504 val trl = rl |> Thm.prop_of |> fromTerm thy |> convertRule state vars 505 fun tac (upd, dup,rot) i = 506 emtac ctxt upd (if dup then rev_dup_elim ctxt rl else rl) i THEN 507 rot_subgoals_tac (rot, #2 trl) i 508 in SOME (trl, tac) end 509 handle 510 ElimBadPrem => (*reject: prems don't preserve conclusion*) 511 (if Context_Position.is_visible ctxt then 512 warning ("Ignoring weak elimination rule\n" ^ Thm.string_of_thm ctxt rl0) 513 else (); 514 Option.NONE) 515 | ElimBadConcl => (*ignore: conclusion is not just a variable*) 516 (cond_tracing (Config.get ctxt trace) 517 (fn () => "Ignoring ill-formed elimination rule:\n" ^ 518 "conclusion should be a variable\n" ^ Thm.string_of_thm ctxt rl0); 519 Option.NONE); 520 521 522(*** Conversion of Introduction Rules ***) 523 524fun convertIntrPrem t = mkGoal (strip_imp_concl t) :: strip_imp_prems t; 525 526fun convertIntrRule state vars t = 527 let val Ps = strip_imp_prems t 528 val P = strip_imp_concl t 529 in (mkGoal P, map (convertIntrPrem o skoPrem state vars) Ps) 530 end; 531 532(*Tableau rule from introduction rule. 533 Flag "upd" says that the inference updated the branch. 534 Flag "dup" requests duplication of the affected formula. 535 Since unsafe rules are now delayed, "dup" is always FALSE for 536 introduction rules.*) 537fun fromIntrRule (state as State {ctxt, ...}) vars rl0 = 538 let 539 val thy = Proof_Context.theory_of ctxt 540 val rl = Thm.transfer thy rl0 541 val trl = rl |> Thm.prop_of |> fromTerm thy |> convertIntrRule state vars 542 fun tac (upd,dup,rot) i = 543 rmtac ctxt upd (if dup then Classical.dup_intr rl else rl) i THEN 544 rot_subgoals_tac (rot, #2 trl) i 545 in (trl, tac) end; 546 547 548val dummyVar = Term.Var (("etc",0), dummyT); 549 550(*Convert from prototerms to ordinary terms with dummy types 551 Ignore abstractions; identify all Vars; STOP at given depth*) 552fun toTerm 0 _ = dummyVar 553 | toTerm d (Const(a,_)) = Term.Const (a,dummyT) (*no need to convert typargs*) 554 | toTerm d (Skolem(a,_)) = Term.Const (a,dummyT) 555 | toTerm d (Free a) = Term.Free (a,dummyT) 556 | toTerm d (Bound i) = Term.Bound i 557 | toTerm d (Var _) = dummyVar 558 | toTerm d (Abs(a,_)) = dummyVar 559 | toTerm d (f $ u) = Term.$ (toTerm d f, toTerm (d-1) u); 560 561(*Too flexible assertions or goals. Motivated by examples such as "(\<And>P. ~P) \<Longrightarrow> 0==1"*) 562fun isVarForm (Var _) = true 563 | isVarForm (Const (c, _) $ Var _) = (c = Data.not_name) 564 | isVarForm _ = false; 565 566fun netMkRules state P vars (nps: Classical.netpair list) = 567 case P of 568 (Const ("*Goal*", _) $ G) => 569 let val pG = mk_Trueprop (toTerm 2 G) 570 val intrs = maps (fn (inet,_) => Net.unify_term inet pG) nps 571 in map (fromIntrRule state vars o #2) (order_list intrs) end 572 | _ => 573 if isVarForm P then [] (*The formula is too flexible, reject*) 574 else 575 let val pP = mk_Trueprop (toTerm 3 P) 576 val elims = maps (fn (_,enet) => Net.unify_term enet pP) nps 577 in map_filter (fromRule state vars o #2) (order_list elims) end; 578 579 580(*Normalize a branch--for tracing*) 581fun norm2 (G,md) = (norm G, md); 582 583fun normLev (Gs,Hs) = (map norm2 Gs, map norm2 Hs); 584 585fun normBr {pairs, lits, vars, lim} = 586 {pairs = map normLev pairs, 587 lits = map norm lits, 588 vars = vars, 589 lim = lim}; 590 591 592val dummyTVar = Term.TVar(("a",0), []); 593val dummyVar2 = Term.Var(("var",0), dummyT); 594 595(*convert blast_tac's type representation to real types for tracing*) 596fun showType (Free a) = Term.TFree (a,[]) 597 | showType (Var _) = dummyTVar 598 | showType t = 599 (case strip_comb t of 600 (Const (a, _), us) => Term.Type(a, map showType us) 601 | _ => dummyT); 602 603(*Display top-level overloading if any*) 604fun topType thy (Const (c, ts)) = SOME (Sign.const_instance thy (c, map showType ts)) 605 | topType thy (Abs(a,t)) = topType thy t 606 | topType thy (f $ u) = (case topType thy f of NONE => topType thy u | some => some) 607 | topType _ _ = NONE; 608 609 610(*Convert from prototerms to ordinary terms with dummy types for tracing*) 611fun showTerm d (Const (a,_)) = Term.Const (a,dummyT) 612 | showTerm d (Skolem(a,_)) = Term.Const (a,dummyT) 613 | showTerm d (Free a) = Term.Free (a,dummyT) 614 | showTerm d (Bound i) = Term.Bound i 615 | showTerm d (Var (Unsynchronized.ref(SOME u))) = showTerm d u 616 | showTerm d (Var (Unsynchronized.ref NONE)) = dummyVar2 617 | showTerm d (Abs(a,t)) = if d=0 then dummyVar 618 else Term.Abs(a, dummyT, showTerm (d-1) t) 619 | showTerm d (f $ u) = if d=0 then dummyVar 620 else Term.$ (showTerm d f, showTerm (d-1) u); 621 622fun string_of ctxt d t = Syntax.string_of_term ctxt (showTerm d t); 623 624(*Convert a Goal to an ordinary Not. Used also in dup_intr, where a goal like 625 Ex(P) is duplicated as the assumption ~Ex(P). *) 626fun negOfGoal (Const ("*Goal*", _) $ G) = negate G 627 | negOfGoal G = G; 628 629fun negOfGoal2 (G,md) = (negOfGoal G, md); 630 631(*Converts all Goals to Nots in the safe parts of a branch. They could 632 have been moved there from the literals list after substitution (equalSubst). 633 There can be at most one--this function could be made more efficient.*) 634fun negOfGoals pairs = map (fn (Gs, unsafe) => (map negOfGoal2 Gs, unsafe)) pairs; 635 636(*Tactic. Convert *Goal* to negated assumption in FIRST position*) 637fun negOfGoal_tac ctxt i = 638 TRACE ctxt Data.ccontr (resolve_tac ctxt [Data.ccontr]) i THEN rotate_tac ~1 i; 639 640fun traceTerm ctxt t = 641 let val thy = Proof_Context.theory_of ctxt 642 val t' = norm (negOfGoal t) 643 val stm = string_of ctxt 8 t' 644 in 645 case topType thy t' of 646 NONE => stm (*no type to attach*) 647 | SOME T => stm ^ " :: " ^ Syntax.string_of_typ ctxt T 648 end; 649 650 651(*Print tracing information at each iteration of prover*) 652fun trace_prover (State {ctxt, fullTrace, ...}) brs = 653 let fun printPairs (((G,_)::_,_)::_) = tracing (traceTerm ctxt G) 654 | printPairs (([],(H,_)::_)::_) = tracing (traceTerm ctxt H ^ " (Unsafe)") 655 | printPairs _ = () 656 fun printBrs (brs0 as {pairs, lits, lim, ...} :: brs) = 657 (fullTrace := brs0 :: !fullTrace; 658 List.app (fn _ => tracing "+") brs; 659 tracing (" [" ^ string_of_int lim ^ "] "); 660 printPairs pairs; 661 tracing "") 662 in if Config.get ctxt trace then printBrs (map normBr brs) else () end; 663 664(*Tracing: variables updated in the last branch operation?*) 665fun traceVars (State {ctxt, ntrail, trail, ...}) ntrl = 666 if Config.get ctxt trace then 667 (case !ntrail-ntrl of 668 0 => () 669 | 1 => tracing " 1 variable UPDATED:" 670 | n => tracing (" " ^ string_of_int n ^ " variables UPDATED:"); 671 (*display the instantiations themselves, though no variable names*) 672 List.app (fn v => tracing (" " ^ string_of ctxt 4 (the (!v)))) 673 (List.take(!trail, !ntrail-ntrl)); 674 tracing "") 675 else (); 676 677(*Tracing: how many new branches are created?*) 678fun traceNew true prems = 679 (case length prems of 680 0 => tracing "branch closed by rule" 681 | 1 => tracing "branch extended (1 new subgoal)" 682 | n => tracing ("branch split: "^ string_of_int n ^ " new subgoals")) 683 | traceNew _ _ = (); 684 685 686 687(*** Code for handling equality: naive substitution, like hyp_subst_tac ***) 688 689(*Replace the ATOMIC term "old" by "new" in t*) 690fun subst_atomic (old,new) t = 691 let fun subst (Var(Unsynchronized.ref(SOME u))) = subst u 692 | subst (Abs(a,body)) = Abs(a, subst body) 693 | subst (f$t) = subst f $ subst t 694 | subst t = if t aconv old then new else t 695 in subst t end; 696 697(*Eta-contract a term from outside: just enough to reduce it to an atom*) 698fun eta_contract_atom (t0 as Abs(a, body)) = 699 (case eta_contract2 body of 700 f $ Bound 0 => if member (op =) (loose_bnos f) 0 then t0 701 else eta_contract_atom (incr_boundvars ~1 f) 702 | _ => t0) 703 | eta_contract_atom t = t 704and eta_contract2 (f$t) = f $ eta_contract_atom t 705 | eta_contract2 t = eta_contract_atom t; 706 707 708(*When can we safely delete the equality? 709 Not if it equates two constants; consider 0=1. 710 Not if it resembles x=t[x], since substitution does not eliminate x. 711 Not if it resembles ?x=0; another goal could instantiate ?x to Suc(i) 712 Prefer to eliminate Bound variables if possible. 713 Result: true = use as is, false = reorient first *) 714 715(*Can t occur in u? For substitution. 716 Does NOT examine the args of Skolem terms: substitution does not affect them. 717 REFLEXIVE because hyp_subst_tac fails on x=x.*) 718fun substOccur t = 719 let (*NO vars are permitted in u except the arguments of t, if it is 720 a Skolem term. This ensures that no equations are deleted that could 721 be instantiated to a cycle. For example, x=?a is rejected because ?a 722 could be instantiated to Suc(x).*) 723 val vars = case t of 724 Skolem(_,vars) => vars 725 | _ => [] 726 fun occEq u = (t aconv u) orelse occ u 727 and occ (Var(Unsynchronized.ref(SOME u))) = occEq u 728 | occ (Var v) = not (mem_var (v, vars)) 729 | occ (Abs(_,u)) = occEq u 730 | occ (f$u) = occEq u orelse occEq f 731 | occ _ = false; 732 in occEq end; 733 734exception DEST_EQ; 735 736(*Take apart an equality. NO constant Trueprop*) 737fun dest_eq (Const (c, _) $ t $ u) = 738 if c = Data.equality_name then (eta_contract_atom t, eta_contract_atom u) 739 else raise DEST_EQ 740 | dest_eq _ = raise DEST_EQ; 741 742(*Reject the equality if u occurs in (or equals!) t*) 743fun check (t,u,v) = if substOccur t u then raise DEST_EQ else v; 744 745(*IF the goal is an equality with a substitutable variable 746 THEN orient that equality ELSE raise exception DEST_EQ*) 747fun orientGoal (t,u) = case (t,u) of 748 (Skolem _, _) => check(t,u,(t,u)) (*eliminates t*) 749 | (_, Skolem _) => check(u,t,(u,t)) (*eliminates u*) 750 | (Free _, _) => check(t,u,(t,u)) (*eliminates t*) 751 | (_, Free _) => check(u,t,(u,t)) (*eliminates u*) 752 | _ => raise DEST_EQ; 753 754(*Substitute through the branch if an equality goal (else raise DEST_EQ). 755 Moves affected literals back into the branch, but it is not clear where 756 they should go: this could make proofs fail.*) 757fun equalSubst ctxt (G, {pairs, lits, vars, lim}) = 758 let val (t,u) = orientGoal(dest_eq G) 759 val subst = subst_atomic (t,u) 760 fun subst2(G,md) = (subst G, md) 761 (*substitute throughout list; extract affected formulae*) 762 fun subForm ((G,md), (changed, pairs)) = 763 let val nG = subst G 764 in if nG aconv G then (changed, (G,md)::pairs) 765 else ((nG,md)::changed, pairs) 766 end 767 (*substitute throughout "stack frame"; extract affected formulae*) 768 fun subFrame ((Gs,Hs), (changed, frames)) = 769 let val (changed', Gs') = List.foldr subForm (changed, []) Gs 770 val (changed'', Hs') = List.foldr subForm (changed', []) Hs 771 in (changed'', (Gs',Hs')::frames) end 772 (*substitute throughout literals; extract affected ones*) 773 fun subLit (lit, (changed, nlits)) = 774 let val nlit = subst lit 775 in if nlit aconv lit then (changed, nlit::nlits) 776 else ((nlit,true)::changed, nlits) 777 end 778 val (changed, lits') = List.foldr subLit ([], []) lits 779 val (changed', pairs') = List.foldr subFrame (changed, []) pairs 780 in if Config.get ctxt trace then tracing ("Substituting " ^ traceTerm ctxt u ^ 781 " for " ^ traceTerm ctxt t ^ " in branch" ) 782 else (); 783 {pairs = (changed',[])::pairs', (*affected formulas, and others*) 784 lits = lits', (*unaffected literals*) 785 vars = vars, 786 lim = lim} 787 end; 788 789 790exception NEWBRANCHES and CLOSEF; 791 792exception PROVE; 793 794(*Trying eq_contr_tac first INCREASES the effort, slowing reconstruction*) 795fun contr_tac ctxt = 796 ematch_tac ctxt [Data.notE] THEN' (eq_assume_tac ORELSE' assume_tac ctxt); 797 798(*Try to unify complementary literals and return the corresponding tactic. *) 799fun tryClose state (G, L) = 800 let 801 val State {ctxt, ...} = state; 802 val eContr_tac = TRACE ctxt Data.notE contr_tac; 803 val eAssume_tac = TRACE ctxt asm_rl (eq_assume_tac ORELSE' assume_tac ctxt); 804 fun close t u tac = if unify state ([], t, u) then SOME tac else NONE; 805 fun arg (_ $ t) = t; 806 in 807 if isGoal G then close (arg G) L eAssume_tac 808 else if isGoal L then close G (arg L) eAssume_tac 809 else if isNot G then close (arg G) L (eContr_tac ctxt) 810 else if isNot L then close G (arg L) (eContr_tac ctxt) 811 else NONE 812 end; 813 814(*Were there Skolem terms in the premise? Must NOT chase Vars*) 815fun hasSkolem (Skolem _) = true 816 | hasSkolem (Abs (_,body)) = hasSkolem body 817 | hasSkolem (f$t) = hasSkolem f orelse hasSkolem t 818 | hasSkolem _ = false; 819 820(*Attach the right "may duplicate" flag to new formulae: if they contain 821 Skolem terms then allow duplication.*) 822fun joinMd md [] = [] 823 | joinMd md (G::Gs) = (G, hasSkolem G orelse md) :: joinMd md Gs; 824 825 826(** Backtracking and Pruning **) 827 828(*clashVar vars (n,trail) determines whether any of the last n elements 829 of "trail" occur in "vars" OR in their instantiations*) 830fun clashVar [] = (fn _ => false) 831 | clashVar vars = 832 let fun clash (0, _) = false 833 | clash (_, []) = false 834 | clash (n, v::vs) = exists (varOccur v) vars orelse clash(n-1,vs) 835 in clash end; 836 837 838(*nbrs = # of branches just prior to closing this one. Delete choice points 839 for goals proved by the latest inference, provided NO variables in the 840 next branch have been updated.*) 841fun prune _ (1, nxtVars, choices) = choices (*DON'T prune at very end: allow 842 backtracking over bad proofs*) 843 | prune (State {ctxt, ntrail, trail, ...}) (nbrs: int, nxtVars, choices) = 844 let fun traceIt last = 845 let val ll = length last 846 and lc = length choices 847 in if Config.get ctxt trace andalso ll<lc then 848 (tracing ("Pruning " ^ string_of_int(lc-ll) ^ " levels"); 849 last) 850 else last 851 end 852 fun pruneAux (last, _, _, []) = last 853 | pruneAux (last, ntrl, trl, (ntrl',nbrs',exn) :: choices) = 854 if nbrs' < nbrs 855 then last (*don't backtrack beyond first solution of goal*) 856 else if nbrs' > nbrs then pruneAux (last, ntrl, trl, choices) 857 else (* nbrs'=nbrs *) 858 if clashVar nxtVars (ntrl-ntrl', trl) then last 859 else (*no clashes: can go back at least this far!*) 860 pruneAux(choices, ntrl', List.drop(trl, ntrl-ntrl'), 861 choices) 862 in traceIt (pruneAux (choices, !ntrail, !trail, choices)) end; 863 864fun nextVars ({pairs, lits, vars, lim} :: _) = map Var vars 865 | nextVars [] = []; 866 867fun backtrack trace (choices as (ntrl, nbrs, exn)::_) = 868 (cond_tracing trace 869 (fn () => "Backtracking; now there are " ^ string_of_int nbrs ^ " branches"); 870 raise exn) 871 | backtrack _ _ = raise PROVE; 872 873(*Add the literal G, handling *Goal* and detecting duplicates.*) 874fun addLit (Const ("*Goal*", _) $ G, lits) = 875 (*New literal is a *Goal*, so change all other Goals to Nots*) 876 let fun bad (Const ("*Goal*", _) $ _) = true 877 | bad (Const (c, _) $ G') = c = Data.not_name andalso G aconv G' 878 | bad _ = false; 879 fun change [] = [] 880 | change (lit :: lits) = 881 (case lit of 882 Const (c, _) $ G' => 883 if c = "*Goal*" orelse c = Data.not_name then 884 if G aconv G' then change lits 885 else negate G' :: change lits 886 else lit :: change lits 887 | _ => lit :: change lits) 888 in 889 Const ("*Goal*", []) $ G :: (if exists bad lits then change lits else lits) 890 end 891 | addLit (G,lits) = ins_term(G, lits) 892 893 894(*For calculating the "penalty" to assess on a branching factor of n 895 log2 seems a little too severe*) 896fun log n = if n<4 then 0 else 1 + log(n div 4); 897 898 899(*match(t,u) says whether the term u might be an instance of the pattern t 900 Used to detect "recursive" rules such as transitivity*) 901fun match (Var _) u = true 902 | match (Const (a,tas)) (Const (b,tbs)) = 903 a = "*Goal*" andalso b = Data.not_name orelse 904 a = Data.not_name andalso b = "*Goal*" orelse 905 a = b andalso matchs tas tbs 906 | match (Free a) (Free b) = (a=b) 907 | match (Bound i) (Bound j) = (i=j) 908 | match (Abs(_,t)) (Abs(_,u)) = match t u 909 | match (f$t) (g$u) = match f g andalso match t u 910 | match t u = false 911and matchs [] [] = true 912 | matchs (t :: ts) (u :: us) = match t u andalso matchs ts us; 913 914 915fun printStats (State {ntried, nclosed, ...}) (b, start, tacs) = 916 if b then 917 tracing (Timing.message (Timing.result start) ^ " for search. Closed: " 918 ^ string_of_int (!nclosed) ^ 919 " tried: " ^ string_of_int (!ntried) ^ 920 " tactics: " ^ string_of_int (length tacs)) 921 else (); 922 923 924(*Tableau prover based on leanTaP. Argument is a list of branches. Each 925 branch contains a list of unexpanded formulae, a list of literals, and a 926 bound on unsafe expansions. 927 "start" is CPU time at start, for printing search time 928*) 929fun prove (state, start, brs, cont) = 930 let val State {ctxt, ntrail, nclosed, ntried, ...} = state; 931 val trace = Config.get ctxt trace; 932 val stats = Config.get ctxt stats; 933 val {safe0_netpair, safep_netpair, unsafe_netpair, ...} = 934 Classical.rep_cs (Classical.claset_of ctxt); 935 val safeList = [safe0_netpair, safep_netpair]; 936 val unsafeList = [unsafe_netpair]; 937 fun prv (tacs, trs, choices, []) = 938 (printStats state (trace orelse stats, start, tacs); 939 cont (tacs, trs, choices)) (*all branches closed!*) 940 | prv (tacs, trs, choices, 941 brs0 as {pairs = ((G,md)::br, unsafe)::pairs, 942 lits, vars, lim} :: brs) = 943 (*apply a safe rule only (possibly allowing instantiation); 944 defer any unsafe formulae*) 945 let exception PRV (*backtrack to precisely this recursion!*) 946 val ntrl = !ntrail 947 val nbrs = length brs0 948 val nxtVars = nextVars brs 949 val G = norm G 950 val rules = netMkRules state G vars safeList 951 (*Make a new branch, decrementing "lim" if instantiations occur*) 952 fun newBr (vars',lim') prems = 953 map (fn prem => 954 if (exists isGoal prem) 955 then {pairs = ((joinMd md prem, []) :: 956 negOfGoals ((br, unsafe)::pairs)), 957 lits = map negOfGoal lits, 958 vars = vars', 959 lim = lim'} 960 else {pairs = ((joinMd md prem, []) :: 961 (br, unsafe) :: pairs), 962 lits = lits, 963 vars = vars', 964 lim = lim'}) 965 prems @ 966 brs 967 (*Seek a matching rule. If unifiable then add new premises 968 to branch.*) 969 fun deeper [] = raise NEWBRANCHES 970 | deeper (((P,prems),tac)::grls) = 971 if unify state (add_term_vars(P,[]), P, G) 972 then (*P comes from the rule; G comes from the branch.*) 973 let val updated = ntrl < !ntrail (*branch updated*) 974 val lim' = if updated 975 then lim - (1+log(length rules)) 976 else lim (*discourage branching updates*) 977 val vars = vars_in_vars vars 978 val vars' = List.foldr add_terms_vars vars prems 979 val choices' = (ntrl, nbrs, PRV) :: choices 980 val tacs' = (tac(updated,false,true)) 981 :: tacs (*no duplication; rotate*) 982 in 983 traceNew trace prems; traceVars state ntrl; 984 (if null prems then (*closed the branch: prune!*) 985 (nclosed := !nclosed + 1; 986 prv(tacs', brs0::trs, 987 prune state (nbrs, nxtVars, choices'), 988 brs)) 989 else (*prems non-null*) 990 if lim'<0 (*faster to kill ALL the alternatives*) 991 then (cond_tracing trace (fn () => "Excessive branching: KILLED"); 992 clearTo state ntrl; raise NEWBRANCHES) 993 else 994 (ntried := !ntried + length prems - 1; 995 prv(tacs', brs0::trs, choices', 996 newBr (vars',lim') prems))) 997 handle PRV => 998 if updated then 999 (*Backtrack at this level. 1000 Reset Vars and try another rule*) 1001 (clearTo state ntrl; deeper grls) 1002 else (*backtrack to previous level*) 1003 backtrack trace choices 1004 end 1005 else deeper grls 1006 (*Try to close branch by unifying with head goal*) 1007 fun closeF [] = raise CLOSEF 1008 | closeF (L::Ls) = 1009 case tryClose state (G,L) of 1010 NONE => closeF Ls 1011 | SOME tac => 1012 let val choices' = 1013 (if trace then (tracing "branch closed"; 1014 traceVars state ntrl) 1015 else (); 1016 prune state (nbrs, nxtVars, 1017 (ntrl, nbrs, PRV) :: choices)) 1018 in nclosed := !nclosed + 1; 1019 prv (tac::tacs, brs0::trs, choices', brs) 1020 handle PRV => 1021 (*reset Vars and try another literal 1022 [this handler is pruned if possible!]*) 1023 (clearTo state ntrl; closeF Ls) 1024 end 1025 (*Try to unify a queued formula (safe or unsafe) with head goal*) 1026 fun closeFl [] = raise CLOSEF 1027 | closeFl ((br, unsafe)::pairs) = 1028 closeF (map fst br) 1029 handle CLOSEF => closeF (map fst unsafe) 1030 handle CLOSEF => closeFl pairs 1031 in 1032 trace_prover state brs0; 1033 if lim<0 then (cond_tracing trace (fn () => "Limit reached."); backtrack trace choices) 1034 else 1035 prv (Data.hyp_subst_tac ctxt trace :: tacs, 1036 brs0::trs, choices, 1037 equalSubst ctxt 1038 (G, {pairs = (br,unsafe)::pairs, 1039 lits = lits, vars = vars, lim = lim}) 1040 :: brs) 1041 handle DEST_EQ => closeF lits 1042 handle CLOSEF => closeFl ((br,unsafe)::pairs) 1043 handle CLOSEF => deeper rules 1044 handle NEWBRANCHES => 1045 (case netMkRules state G vars unsafeList of 1046 [] => (*there are no plausible unsafe rules*) 1047 (cond_tracing trace (fn () => "moving formula to literals"); 1048 prv (tacs, brs0::trs, choices, 1049 {pairs = (br,unsafe)::pairs, 1050 lits = addLit(G,lits), 1051 vars = vars, 1052 lim = lim} :: brs)) 1053 | _ => (*G admits some unsafe rules: try later*) 1054 (cond_tracing trace (fn () => "moving formula to unsafe list"); 1055 prv (if isGoal G then negOfGoal_tac ctxt :: tacs 1056 else tacs, 1057 brs0::trs, 1058 choices, 1059 {pairs = (br, unsafe@[(negOfGoal G, md)])::pairs, 1060 lits = lits, 1061 vars = vars, 1062 lim = lim} :: brs))) 1063 end 1064 | prv (tacs, trs, choices, 1065 {pairs = ([],unsafe)::(Gs,unsafe')::pairs, lits, vars, lim} :: brs) = 1066 (*no more "safe" formulae: transfer unsafe down a level*) 1067 prv (tacs, trs, choices, 1068 {pairs = (Gs,unsafe@unsafe')::pairs, 1069 lits = lits, 1070 vars = vars, 1071 lim = lim} :: brs) 1072 | prv (tacs, trs, choices, 1073 brs0 as {pairs = [([], (H,md)::Hs)], 1074 lits, vars, lim} :: brs) = 1075 (*no safe steps possible at any level: apply a unsafe rule*) 1076 let exception PRV (*backtrack to precisely this recursion!*) 1077 val H = norm H 1078 val ntrl = !ntrail 1079 val rules = netMkRules state H vars unsafeList 1080 (*new premises of unsafe rules may NOT be duplicated*) 1081 fun newPrem (vars,P,dup,lim') prem = 1082 let val Gs' = map (fn Q => (Q,false)) prem 1083 and Hs' = if dup then Hs @ [(negOfGoal H, md)] else Hs 1084 and lits' = if (exists isGoal prem) 1085 then map negOfGoal lits 1086 else lits 1087 in {pairs = if exists (match P) prem then [(Gs',Hs')] 1088 (*Recursive in this premise. Don't make new 1089 "stack frame". New unsafe premises will end up 1090 at the BACK of the queue, preventing 1091 exclusion of others*) 1092 else [(Gs',[]), ([],Hs')], 1093 lits = lits', 1094 vars = vars, 1095 lim = lim'} 1096 end 1097 fun newBr x prems = map (newPrem x) prems @ brs 1098 (*Seek a matching rule. If unifiable then add new premises 1099 to branch.*) 1100 fun deeper [] = raise NEWBRANCHES 1101 | deeper (((P,prems),tac)::grls) = 1102 if unify state (add_term_vars(P,[]), P, H) 1103 then 1104 let val updated = ntrl < !ntrail (*branch updated*) 1105 val vars = vars_in_vars vars 1106 val vars' = List.foldr add_terms_vars vars prems 1107 (*duplicate H if md permits*) 1108 val dup = md (*earlier had "andalso vars' <> vars": 1109 duplicate only if the subgoal has new vars*) 1110 (*any instances of P in the subgoals? 1111 NB: boolean "recur" affects tracing only!*) 1112 and recur = exists (exists (match P)) prems 1113 val lim' = (*Decrement "lim" extra if updates occur*) 1114 if updated then lim - (1+log(length rules)) 1115 else lim-1 1116 (*It is tempting to leave "lim" UNCHANGED if 1117 both dup and recur are false. Proofs are 1118 found at shallower depths, but looping 1119 occurs too often...*) 1120 val mayUndo = 1121 (*Allowing backtracking from a rule application 1122 if other matching rules exist, if the rule 1123 updated variables, or if the rule did not 1124 introduce new variables. This latter condition 1125 means it is not a standard "gamma-rule" but 1126 some other form of unsafe rule. Aim is to 1127 emulate Fast_tac, which allows all unsafe steps 1128 to be undone.*) 1129 not(null grls) (*other rules to try?*) 1130 orelse updated 1131 orelse vars=vars' (*no new Vars?*) 1132 val tac' = tac(updated, dup, true) 1133 (*if recur then perhaps shouldn't call rotate_tac: new 1134 formulae should be last, but that's WRONG if the new 1135 formulae are Goals, since they remain in the first 1136 position*) 1137 1138 in 1139 if lim'<0 andalso not (null prems) 1140 then (*it's faster to kill ALL the alternatives*) 1141 (cond_tracing trace (fn () => "Excessive branching: KILLED"); 1142 clearTo state ntrl; raise NEWBRANCHES) 1143 else 1144 traceNew trace prems; 1145 cond_tracing (trace andalso dup) (fn () => " (duplicating)"); 1146 cond_tracing (trace andalso recur) (fn () => " (recursive)"); 1147 traceVars state ntrl; 1148 if null prems then nclosed := !nclosed + 1 1149 else ntried := !ntried + length prems - 1; 1150 prv(tac' :: tacs, 1151 brs0::trs, 1152 (ntrl, length brs0, PRV) :: choices, 1153 newBr (vars', P, dup, lim') prems) 1154 handle PRV => 1155 if mayUndo 1156 then (*reset Vars and try another rule*) 1157 (clearTo state ntrl; deeper grls) 1158 else (*backtrack to previous level*) 1159 backtrack trace choices 1160 end 1161 else deeper grls 1162 in 1163 trace_prover state brs0; 1164 if lim<1 then (cond_tracing trace (fn () => "Limit reached."); backtrack trace choices) 1165 else deeper rules 1166 handle NEWBRANCHES => 1167 (*cannot close branch: move H to literals*) 1168 prv (tacs, brs0::trs, choices, 1169 {pairs = [([], Hs)], 1170 lits = H::lits, 1171 vars = vars, 1172 lim = lim} :: brs) 1173 end 1174 | prv (tacs, trs, choices, _ :: brs) = backtrack trace choices 1175 in prv ([], [], [(!ntrail, length brs, PROVE)], brs) end; 1176 1177 1178(*Construct an initial branch.*) 1179fun initBranch (ts,lim) = 1180 {pairs = [(map (fn t => (t,true)) ts, [])], 1181 lits = [], 1182 vars = add_terms_vars (ts,[]), 1183 lim = lim}; 1184 1185 1186(*** Conversion & Skolemization of the Isabelle proof state ***) 1187 1188(*Make a list of all the parameters in a subgoal, even if nested*) 1189local open Term 1190in 1191fun discard_foralls (Const(@{const_name Pure.all},_)$Abs(a,T,t)) = discard_foralls t 1192 | discard_foralls t = t; 1193end; 1194 1195(*List of variables not appearing as arguments to the given parameter*) 1196fun getVars [] i = [] 1197 | getVars ((_,(v,is))::alist) (i: int) = 1198 if member (op =) is i then getVars alist i 1199 else v :: getVars alist i; 1200 1201exception TRANS of string; 1202 1203(*Translation of a subgoal: Skolemize all parameters*) 1204fun fromSubgoal (state as State {ctxt, ...}) t = 1205 let val thy = Proof_Context.theory_of ctxt 1206 val alistVar = Unsynchronized.ref [] 1207 and alistTVar = Unsynchronized.ref [] 1208 fun hdvar ((ix,(v,is))::_) = v 1209 fun from lev t = 1210 let val (ht,ts) = Term.strip_comb t 1211 fun apply u = list_comb (u, map (from lev) ts) 1212 fun bounds [] = [] 1213 | bounds (Term.Bound i::ts) = 1214 if i<lev then raise TRANS 1215 "Function unknown's argument not a parameter" 1216 else i-lev :: bounds ts 1217 | bounds ts = raise TRANS 1218 "Function unknown's argument not a bound variable" 1219 in 1220 case ht of 1221 Term.Const aT => apply (fromConst thy alistTVar aT) 1222 | Term.Free (a,_) => apply (Free a) 1223 | Term.Bound i => apply (Bound i) 1224 | Term.Var (ix,_) => 1225 (case (AList.lookup (op =) (!alistVar) ix) of 1226 NONE => (alistVar := (ix, (Unsynchronized.ref NONE, bounds ts)) 1227 :: !alistVar; 1228 Var (hdvar(!alistVar))) 1229 | SOME(v,is) => if is=bounds ts then Var v 1230 else raise TRANS 1231 ("Discrepancy among occurrences of " 1232 ^ Term.string_of_vname ix)) 1233 | Term.Abs (a,_,body) => 1234 if null ts then Abs(a, from (lev+1) body) 1235 else raise TRANS "argument not in normal form" 1236 end 1237 1238 val npars = length (Logic.strip_params t) 1239 1240 (*Skolemize a subgoal from a proof state*) 1241 fun skoSubgoal i t = 1242 if i<npars then 1243 skoSubgoal (i+1) 1244 (subst_bound (Skolem (gensym state "T", getVars (!alistVar) i), t)) 1245 else t 1246 1247 in skoSubgoal 0 (from 0 (discard_foralls t)) end; 1248 1249 1250(*Tableau engine and proof reconstruction operating on subgoal 1. 1251 "start" is CPU time at start, for printing SEARCH time (also prints reconstruction time) 1252 "lim" is depth limit.*) 1253fun raw_blast start ctxt lim st = 1254 let val state = initialize ctxt 1255 val trace = Config.get ctxt trace; 1256 val stats = Config.get ctxt stats; 1257 val skoprem = fromSubgoal state (#1 (Logic.dest_implies (Thm.prop_of st))) 1258 val hyps = strip_imp_prems skoprem 1259 and concl = strip_imp_concl skoprem 1260 fun cont (tacs,_,choices) = 1261 let val start = Timing.start () 1262 in 1263 case Seq.pull(EVERY' (rev tacs) 1 st) of 1264 NONE => (cond_tracing trace (fn () => "PROOF FAILED for depth " ^ string_of_int lim); 1265 backtrack trace choices) 1266 | cell => (cond_tracing (trace orelse stats) 1267 (fn () => Timing.message (Timing.result start) ^ " for reconstruction"); 1268 Seq.make(fn()=> cell)) 1269 end handle TERM _ => 1270 (cond_tracing trace (fn () => "PROOF RAISED EXN TERM for depth " ^ string_of_int lim); 1271 backtrack trace choices) 1272 in 1273 prove (state, start, [initBranch (mkGoal concl :: hyps, lim)], cont) 1274 end 1275 handle PROVE => Seq.empty 1276 | TRANS s => (cond_tracing (Config.get ctxt trace) (fn () => "Blast: " ^ s); Seq.empty); 1277 1278fun depth_tac ctxt lim i st = 1279 SELECT_GOAL 1280 (Object_Logic.atomize_prems_tac ctxt 1 THEN 1281 raw_blast (Timing.start ()) ctxt lim) i st; 1282 1283fun blast_tac ctxt i st = 1284 let 1285 val start = Timing.start (); 1286 val lim = Config.get ctxt depth_limit; 1287 in 1288 SELECT_GOAL 1289 (Object_Logic.atomize_prems_tac ctxt 1 THEN 1290 DEEPEN (1, lim) (fn m => fn _ => raw_blast start ctxt m) 0 1) i st 1291 end; 1292 1293 1294 1295(*** For debugging: these apply the prover to a subgoal and return 1296 the resulting tactics, trace, etc. ***) 1297 1298(*Read a string to make an initial, singleton branch*) 1299fun readGoal ctxt s = 1300 Syntax.read_prop ctxt s |> fromTerm (Proof_Context.theory_of ctxt) |> rand |> mkGoal; 1301 1302fun tryIt ctxt lim s = 1303 let 1304 val state as State {fullTrace, ...} = initialize ctxt; 1305 val res = timeap prove (state, Timing.start (), [initBranch ([readGoal ctxt s], lim)], I); 1306 in {fullTrace = !fullTrace, result = res} end; 1307 1308 1309 1310(** method setup **) 1311 1312val _ = 1313 Theory.setup 1314 (Method.setup @{binding blast} 1315 (Scan.lift (Scan.option Parse.nat) --| Method.sections Classical.cla_modifiers >> 1316 (fn NONE => SIMPLE_METHOD' o blast_tac 1317 | SOME lim => (fn ctxt => SIMPLE_METHOD' (depth_tac ctxt lim)))) 1318 "classical tableau prover"); 1319 1320end; 1321