# HG changeset patch # User paulson # Date 882873543 -3600 # Node ID 305390f23734394309760017096312946aa662f9 # Parent 7ba65fe66c734f5453590aad937c6463350ac861 Better equality handling in Blast_tac, usingd a new variant of hyp_subst_tac diff -r 7ba65fe66c73 -r 305390f23734 src/FOL/ROOT.ML --- a/src/FOL/ROOT.ML Tue Dec 23 11:37:48 1997 +0100 +++ b/src/FOL/ROOT.ML Tue Dec 23 11:39:03 1997 +0100 @@ -28,9 +28,10 @@ structure Hypsubst_Data = struct structure Simplifier = Simplifier - (*Take apart an equality judgement; otherwise raise Match!*) - fun dest_eq (Const("Trueprop",_) $ (Const("op =",T) $ t $ u)) = - (t, u, domain_type T) + (*These destructors Match!*) + fun dest_eq (Const("op =",T) $ t $ u) = (t, u, domain_type T) + val dest_Trueprop = FOLogic.dest_Trueprop + val dest_imp = FOLogic.dest_imp val eq_reflection = eq_reflection val imp_intr = impI val rev_mp = rev_mp diff -r 7ba65fe66c73 -r 305390f23734 src/FOL/cladata.ML --- a/src/FOL/cladata.ML Tue Dec 23 11:37:48 1997 +0100 +++ b/src/FOL/cladata.ML Tue Dec 23 11:39:03 1997 +0100 @@ -54,7 +54,7 @@ val ccontr = ccontr val contr_tac = Cla.contr_tac val dup_intr = Cla.dup_intr - val vars_gen_hyp_subst_tac = Hypsubst.vars_gen_hyp_subst_tac + val hyp_subst_tac = Hypsubst.blast_hyp_subst_tac val claset = Cla.claset val rep_claset = Cla.rep_claset end; diff -r 7ba65fe66c73 -r 305390f23734 src/FOL/fologic.ML --- a/src/FOL/fologic.ML Tue Dec 23 11:37:48 1997 +0100 +++ b/src/FOL/fologic.ML Tue Dec 23 11:39:03 1997 +0100 @@ -10,6 +10,7 @@ val oT: typ val mk_Trueprop: term -> term val dest_Trueprop: term -> term + val dest_imp : term -> term*term val conj: term val disj: term val imp: term @@ -40,6 +41,9 @@ and disj = Const("op |", [oT,oT]--->oT) and imp = Const("op -->", [oT,oT]--->oT); +fun dest_imp (Const("op -->",_) $ A $ B) = (A, B) + | dest_imp t = raise TERM ("dest_imp", [t]); + fun eq_const T = Const ("op =", [T, T] ---> oT); fun mk_eq (t, u) = eq_const (fastype_of t) $ t $ u; diff -r 7ba65fe66c73 -r 305390f23734 src/HOL/cladata.ML --- a/src/HOL/cladata.ML Tue Dec 23 11:37:48 1997 +0100 +++ b/src/HOL/cladata.ML Tue Dec 23 11:39:03 1997 +0100 @@ -14,8 +14,9 @@ struct structure Simplifier = Simplifier (*Take apart an equality judgement; otherwise raise Match!*) - fun dest_eq (Const("Trueprop",_) $ (Const("op =",T) $ t $ u)) = - (t, u, domain_type T) + fun dest_eq (Const("op =",T) $ t $ u) = (t, u, domain_type T) + val dest_Trueprop = HOLogic.dest_Trueprop + val dest_imp = HOLogic.dest_imp val eq_reflection = eq_reflection val imp_intr = impI val rev_mp = rev_mp @@ -72,7 +73,7 @@ val ccontr = ccontr val contr_tac = Classical.contr_tac val dup_intr = Classical.dup_intr - val vars_gen_hyp_subst_tac = Hypsubst.vars_gen_hyp_subst_tac + val hyp_subst_tac = Hypsubst.blast_hyp_subst_tac val claset = Classical.claset val rep_claset = Classical.rep_claset end; diff -r 7ba65fe66c73 -r 305390f23734 src/HOL/hologic.ML --- a/src/HOL/hologic.ML Tue Dec 23 11:37:48 1997 +0100 +++ b/src/HOL/hologic.ML Tue Dec 23 11:39:03 1997 +0100 @@ -18,6 +18,7 @@ val conj: term val disj: term val imp: term + val dest_imp : term -> term*term val eq_const: typ -> term val all_const: typ -> term val exists_const: typ -> term @@ -73,6 +74,9 @@ and disj = Const ("op |", [boolT, boolT] ---> boolT) and imp = Const ("op -->", [boolT, boolT] ---> boolT); +fun dest_imp (Const("op -->",_) $ A $ B) = (A, B) + | dest_imp t = raise TERM ("dest_imp", [t]); + fun eq_const T = Const ("op =", [T, T] ---> boolT); fun mk_eq (t, u) = eq_const (fastype_of t) $ t $ u; diff -r 7ba65fe66c73 -r 305390f23734 src/Provers/blast.ML --- a/src/Provers/blast.ML Tue Dec 23 11:37:48 1997 +0100 +++ b/src/Provers/blast.ML Tue Dec 23 11:39:03 1997 +0100 @@ -58,7 +58,7 @@ val ccontr : thm val contr_tac : int -> tactic val dup_intr : thm -> thm - val vars_gen_hyp_subst_tac : bool -> int -> tactic + val hyp_subst_tac : bool ref -> int -> tactic val claset : unit -> claset val rep_claset : claset -> {safeIs: thm list, safeEs: thm list, @@ -731,26 +731,31 @@ let val (t,u) = orientGoal(dest_eq G) val subst = subst_atomic (t,u) fun subst2(G,md) = (subst G, md) - (*substitute throughout Haz list; move affected ones to Safe part*) - fun subHazs ([], Gs, nHs) = (Gs,nHs) - | subHazs ((H,md)::Hs, Gs, nHs) = - let val nH = subst H - in if nH aconv H then subHazs (Hs, Gs, (H,md)::nHs) - else subHazs (Hs, (nH,md)::Gs, nHs) + (*substitute throughout list; extract affected formulae*) + fun subForm ((G,md), (changed, pairs)) = + let val nG = subst G + in if nG aconv G then (changed, (G,md)::pairs) + else ((nG,md)::changed, pairs) end - val pairs' = map (fn(Gs,Hs) => subHazs(rev Hs, map subst2 Gs, [])) pairs - (*substitute throughout literals; move affected ones to Safe part*) - fun subLits ([], [], nlits) = (pairs', nlits, vars, lim) - | subLits ([], Gs, nlits) = ((Gs,[])::pairs', nlits, vars, lim) - | subLits (lit::lits, Gs, nlits) = + (*substitute throughout "stack frame"; extract affected formulae*) + fun subFrame ((Gs,Hs), (changed, frames)) = + let val (changed', Gs') = foldr subForm (Gs, (changed, [])) + val (changed'', Hs') = foldr subForm (Hs, (changed', [])) + in (changed'', (Gs',Hs')::frames) end + (*substitute throughout literals; extract affected ones*) + fun subLit (lit, (changed, nlits)) = let val nlit = subst lit - in if nlit aconv lit then subLits (lits, Gs, nlit::nlits) - else subLits (lits, (nlit,true)::Gs, nlits) + in if nlit aconv lit then (changed, nlit::nlits) + else ((nlit,true)::changed, nlits) end + val (changed, lits') = foldr subLit (lits, ([], [])) + val (changed', pairs') = foldr subFrame (pairs, (changed, [])) in if !trace then writeln ("Substituting " ^ traceTerm sign u ^ " for " ^ traceTerm sign t ^ " in branch" ) else (); - subLits (rev lits, [], []) + ((changed',[])::pairs', (*affected formulas, and others*) + lits', (*unaffected literals*) + vars, lim) end; @@ -1007,7 +1012,7 @@ in tracing sign brs0; if lim<0 then (traceMsg "Limit reached. "; backtrack choices) else - prv (Data.vars_gen_hyp_subst_tac false :: tacs, + prv (Data.hyp_subst_tac trace :: tacs, brs0::trs, choices, equalSubst sign (G, (br,haz)::pairs, lits, vars, lim) :: brs) handle DEST_EQ => closeF lits @@ -1015,16 +1020,18 @@ handle CLOSEF => deeper rules handle NEWBRANCHES => (case netMkRules G vars hazList of - [] => (*no plausible haz rules: move G to literals*) - prv (tacs, brs0::trs, choices, - ((br,haz)::pairs, addLit(G,lits), vars, lim) - ::brs) + [] => (*there are no plausible haz rules*) + (traceMsg "moving goal to literals"; + prv (tacs, brs0::trs, choices, + ((br,haz)::pairs, addLit(G,lits), vars, lim) + ::brs)) | _ => (*G admits some haz rules: try later*) - prv (if isGoal G then negOfGoal_tac :: tacs - else tacs, - brs0::trs, choices, - ((br, haz@[(negOfGoal G, md)])::pairs, - lits, vars, lim) :: brs)) + (traceMsg "moving goal to haz list"; + prv (if isGoal G then negOfGoal_tac :: tacs + else tacs, + brs0::trs, choices, + ((br, haz@[(negOfGoal G, md)])::pairs, + lits, vars, lim) :: brs))) end | prv (tacs, trs, choices, (([],haz)::(Gs,haz')::pairs, lits, vars, lim) :: brs) = diff -r 7ba65fe66c73 -r 305390f23734 src/Provers/hypsubst.ML --- a/src/Provers/hypsubst.ML Tue Dec 23 11:37:48 1997 +0100 +++ b/src/Provers/hypsubst.ML Tue Dec 23 11:39:03 1997 +0100 @@ -21,25 +21,32 @@ Here hyp_subst_tac goes wrong; harder still to prove P(f(f(a))) & P(f(a)) goal thy "P(a) --> (EX y. a=y --> P(f(a)))"; + +goal thy "!!x. [| Q(x,h1); P(a,h2); R(x,y,h3); R(y,z,h4); x=f(y); \ +\ P(x,h5); P(y,h6); K(x,h7) |] ==> Q(x,c)"; +by (blast_hyp_subst_tac (ref true) 1); *) signature HYPSUBST_DATA = sig structure Simplifier : SIMPLIFIER + val dest_Trueprop : term -> term val dest_eq : term -> term*term*typ + val dest_imp : term -> term*term val eq_reflection : thm (* a=b ==> a==b *) val imp_intr : thm (* (P ==> Q) ==> P-->Q *) val rev_mp : thm (* [| P; P-->Q |] ==> Q *) val subst : thm (* [| a=b; P(a) |] ==> P(b) *) val sym : thm (* a=b ==> b=a *) val thin_refl : thm (* [|x=x; PROP W|] ==> PROP W *) -end; + end; signature HYPSUBST = sig val bound_hyp_subst_tac : int -> tactic val hyp_subst_tac : int -> tactic + val blast_hyp_subst_tac : bool ref -> int -> tactic (*exported purely for debugging purposes*) val gen_hyp_subst_tac : bool -> int -> tactic val vars_gen_hyp_subst_tac : bool -> int -> tactic @@ -54,8 +61,6 @@ functor HypsubstFun(Data: HYPSUBST_DATA): HYPSUBST = struct -local open Data in - exception EQ_VAR; fun loose (i,t) = 0 mem_int add_loose_bnos(t,i,[]); @@ -109,9 +114,10 @@ fun eq_var bnd novars = let fun eq_var_aux k (Const("all",_) $ Abs(_,_,t)) = eq_var_aux k t | eq_var_aux k (Const("==>",_) $ A $ B) = - ((k, inspect_pair bnd novars (dest_eq A)) + ((k, inspect_pair bnd novars + (Data.dest_eq (Data.dest_Trueprop A))) (*Exception comes from inspect_pair or dest_eq*) - handle Match => eq_var_aux (k+1) B) + handle _ => eq_var_aux (k+1) B) | eq_var_aux k _ = raise EQ_VAR in eq_var_aux 0 end; @@ -123,9 +129,10 @@ *) fun thin_leading_eqs_tac bnd m = SUBGOAL (fn (Bi,i) => let fun count [] = 0 - | count (A::Bs) = ((inspect_pair bnd true (dest_eq A); + | count (A::Bs) = ((inspect_pair bnd true + (Data.dest_eq (Data.dest_Trueprop A)); 1 + count Bs) - handle Match => 0) + handle _ => 0) val j = Int.min(m, count (Logic.strip_assums_hyp Bi)) in REPEAT_DETERM_N j (etac thin_rl i) THEN rotate_tac (m-j) i end); @@ -133,10 +140,11 @@ (*For the simpset. Adds ALL suitable equalities, even if not first! No vars are allowed here, as simpsets are built from meta-assumptions*) fun mk_eqs th = - [ if inspect_pair false false (Data.dest_eq (#prop (rep_thm th))) + [ if inspect_pair false false (Data.dest_eq + (Data.dest_Trueprop (#prop (rep_thm th)))) then th RS Data.eq_reflection else symmetric(th RS Data.eq_reflection) (*reorient*) ] - handle Match => []; (*Exception comes from inspect_pair or dest_eq*) + handle _ => []; (*Exception comes from inspect_pair or dest_eq*) local open Simplifier in @@ -158,7 +166,9 @@ end; -val ssubst = standard (sym RS subst); +val ssubst = standard (Data.sym RS Data.subst); + +val imp_intr_tac = rtac Data.imp_intr; (*Old version of the tactic above -- slower but the only way to handle equalities containing Vars.*) @@ -167,22 +177,69 @@ val (k,symopt) = eq_var bnd false Bi in DETERM - (EVERY [REPEAT_DETERM_N k (etac rev_mp i), - etac revcut_rl i, - REPEAT_DETERM_N (n-k) (etac rev_mp i), - etac (if symopt then ssubst else subst) i, - REPEAT_DETERM_N n (rtac imp_intr i THEN rotate_tac ~1 i)]) + (EVERY [REPEAT_DETERM_N k (etac Data.rev_mp i), + rotate_tac 1 i, + REPEAT_DETERM_N (n-k) (etac Data.rev_mp i), + etac (if symopt then ssubst else Data.subst) i, + REPEAT_DETERM_N n (imp_intr_tac i THEN rotate_tac ~1 i)]) end handle THM _ => no_tac | EQ_VAR => no_tac); (*Substitutes for Free or Bound variables*) -val hyp_subst_tac = FIRST' [ematch_tac [thin_refl], +val hyp_subst_tac = FIRST' [ematch_tac [Data.thin_refl], gen_hyp_subst_tac false, vars_gen_hyp_subst_tac false]; (*Substitutes for Bound variables only -- this is always safe*) val bound_hyp_subst_tac = gen_hyp_subst_tac true ORELSE' vars_gen_hyp_subst_tac true; -end + +(** Version for Blast_tac. Hyps that are affected by the substitution are + moved to the front. Defect: even trivial changes are noticed, such as + substitutions in the arguments of a function Var. **) + +(*final re-reversal of the changed assumptions*) +fun reverse_n_tac 0 i = all_tac + | reverse_n_tac 1 i = rotate_tac ~1 i + | reverse_n_tac n i = + REPEAT_DETERM_N n (rotate_tac ~1 i THEN etac Data.rev_mp i) THEN + REPEAT_DETERM_N n (imp_intr_tac i THEN rotate_tac ~1 i); + +(*Use imp_intr, comparing the old hyps with the new ones as they come out.*) +fun all_imp_intr_tac hyps i = + let fun imptac (r, []) st = reverse_n_tac r i st + | imptac (r, hyp::hyps) st = + let val (hyp',_) = List.nth (prems_of st, i-1) |> + Logic.strip_assums_concl |> + Data.dest_Trueprop |> Data.dest_imp + val (r',tac) = if Pattern.aeconv (hyp,hyp') + then (r, imp_intr_tac i THEN rotate_tac ~1 i) + else (*leave affected hyps at end*) + (r+1, imp_intr_tac i) + in + case Seq.pull(tac st) of + None => Seq.single(st) + | Some(st',_) => imptac (r',hyps) st' + end handle _ => error "?? in blast_hyp_subst_tac" + in imptac (0, rev hyps) end; + + +fun blast_hyp_subst_tac trace = SUBGOAL(fn (Bi,i) => + let val (k,symopt) = eq_var false false Bi + val hyps0 = map Data.dest_Trueprop (Logic.strip_assums_hyp Bi) + (*omit selected equality, returning other hyps*) + val hyps = List.take(hyps0, k) @ List.drop(hyps0, k+1) + val n = length hyps + in + if !trace then writeln "Substituting an equality" else (); + DETERM + (EVERY [REPEAT_DETERM_N k (etac Data.rev_mp i), + rotate_tac 1 i, + REPEAT_DETERM_N (n-k) (etac Data.rev_mp i), + etac (if symopt then ssubst else Data.subst) i, + all_imp_intr_tac hyps i]) + end + handle THM _ => no_tac | EQ_VAR => no_tac); + end;