Better equality handling in Blast_tac, usingd a new variant of hyp_subst_tac
authorpaulson
Tue, 23 Dec 1997 11:39:03 +0100
changeset 4466 305390f23734
parent 4465 7ba65fe66c73
child 4467 bd05e2a28602
Better equality handling in Blast_tac, usingd a new variant of hyp_subst_tac
src/FOL/ROOT.ML
src/FOL/cladata.ML
src/FOL/fologic.ML
src/HOL/cladata.ML
src/HOL/hologic.ML
src/Provers/blast.ML
src/Provers/hypsubst.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
--- 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;