--- 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
--- 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;
--- 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;
--- 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;
--- 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;
--- 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) =
--- 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;