src/Provers/hypsubst.ML
changeset 1011 5c9654e2e3de
parent 704 b71b6be59354
child 2143 093bbe6d333b
--- a/src/Provers/hypsubst.ML	Thu Apr 06 11:55:51 1995 +0200
+++ b/src/Provers/hypsubst.ML	Thu Apr 06 11:59:34 1995 +0200
@@ -1,27 +1,50 @@
 (*  Title: 	Provers/hypsubst
     ID:         $Id$
-    Author: 	Martin D Coen, Cambridge University Computer Laboratory
-    Copyright   1993  University of Cambridge
+    Authors: 	Martin D Coen, Tobias Nipkow and Lawrence C Paulson
+    Copyright   1995  University of Cambridge
+
+Tactic to substitute using the assumption x=t in the rest of the subgoal,
+and to delete that assumption.  Original version due to Martin Coen.
+
+This version uses the simplifier, and requires it to be already present.
+
+Test data:
 
-Martin Coen's tactic for substitution in the hypotheses
+goal thy "!!x.[| Q(x,y,z); y=x; a=x; z=y; P(y) |] ==> P(z)";
+goal thy "!!x.[| Q(x,y,z); z=f(x); x=z |] ==> P(z)";
+goal thy "!!y. [| ?x=y; P(?x) |] ==> y = a";
+goal thy "!!z. [| ?x=y; P(?x) |] ==> y = a";
+
+by (hyp_subst_tac 1);
+by (bound_hyp_subst_tac 1);
+
+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)))";
 *)
 
 signature HYPSUBST_DATA =
   sig
-  val dest_eq	: term -> term*term
-  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 *)
+  structure Simplifier : SIMPLIFIER
+  val dest_eq	       : 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 *)
   end;
 
+
 signature HYPSUBST =
   sig
-  val bound_hyp_subst_tac : int -> tactic
-  val hyp_subst_tac       : int -> tactic
+  val bound_hyp_subst_tac    : int -> tactic
+  val hyp_subst_tac          : int -> tactic
     (*exported purely for debugging purposes*)
-  val eq_var              : bool -> term -> int * thm
-  val inspect_pair        : bool -> term * term -> thm
+  val gen_hyp_subst_tac      : bool -> int -> tactic
+  val vars_gen_hyp_subst_tac : bool -> int -> tactic
+  val eq_var                 : bool -> bool -> term -> int * bool
+  val inspect_pair           : bool -> bool -> term * term -> bool
+  val mk_eqs                 : thm -> thm list
+  val thin_leading_eqs_tac   : bool -> int -> int -> tactic
   end;
 
 functor HypsubstFun(Data: HYPSUBST_DATA): HYPSUBST = 
@@ -33,55 +56,128 @@
 
 fun loose (i,t) = 0 mem add_loose_bnos(t,i,[]);
 
-(*It's not safe to substitute for a constant; consider 0=1.
-  It's not safe to substitute for x=t[x] since x is not eliminated.
-  It's not safe to substitute for a Var; what if it appears in other goals?
-  It's not safe to substitute for a variable free in the premises,
-    but how could we check for this?*)
-fun inspect_pair bnd (t,u) =
-  case (Pattern.eta_contract t, Pattern.eta_contract u) of
-       (Bound i, _) => if loose(i,u) then raise Match 
-		       else sym		(*eliminates t*)
-     | (_, Bound i) => if loose(i,t) then raise Match 
-		       else asm_rl	(*eliminates u*)
-     | (Free _, _) => if bnd orelse Logic.occs(t,u) then raise Match 
-		      else sym		(*eliminates t*)
-     | (_, Free _) => if bnd orelse Logic.occs(u,t) then raise Match 
-		      else asm_rl	(*eliminates u*)
+local val odot = ord"."
+in
+(*Simplifier turns Bound variables to dotted Free variables: 
+  change it back (any Bound variable will do)
+*)
+fun contract t =
+    case Pattern.eta_contract t of
+	Free(a,T) => if (ord a = odot) then Bound 0 else Free(a,T)
+      | t'        => t'
+end;
+
+fun has_vars t = maxidx_of_term t <> ~1;
+
+(*If novars then we forbid Vars in the equality.
+  If bnd then we only look for Bound (or dotted Free) variables to eliminate. 
+  When can we safely delete the equality?
+    Not if it equates two constants; consider 0=1.
+    Not if it resembles x=t[x], since substitution does not eliminate x.
+    Not if it resembles ?x=0; another goal could instantiate ?x to Suc(i)
+    Not if it involves a variable free in the premises, 
+        but we can't check for this -- hence bnd and bound_hyp_subst_tac
+  Prefer to eliminate Bound variables if possible.
+  Result:  true = use as is,  false = reorient first *)
+fun inspect_pair bnd novars (t,u) =
+  case (contract t, contract u) of
+       (Bound i, _) => if loose(i,u) orelse novars andalso has_vars u 
+		       then raise Match 
+		       else true		(*eliminates t*)
+     | (_, Bound i) => if loose(i,t) orelse novars andalso has_vars t  
+		       then raise Match 
+		       else false		(*eliminates u*)
+     | (Free _, _) =>  if bnd orelse Logic.occs(t,u) orelse  
+		          novars andalso has_vars u  
+		       then raise Match 
+		       else true		(*eliminates t*)
+     | (_, Free _) =>  if bnd orelse Logic.occs(u,t) orelse  
+		          novars andalso has_vars t 
+		       then raise Match 
+		       else false		(*eliminates u*)
      | _ => raise Match;
 
 (*Locates a substitutable variable on the left (resp. right) of an equality
-   assumption.  Returns the number of intervening assumptions, paried with
-   the rule asm_rl (resp. sym). *)
-fun eq_var bnd =
+   assumption.  Returns the number of intervening assumptions. *)
+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 (dest_eq A))
-		      (*Exception Match comes from inspect_pair or dest_eq*)
+	      ((k, inspect_pair bnd novars (dest_eq A))
+		      (*Exception comes from inspect_pair or dest_eq*)
 	       handle Match => eq_var_aux (k+1) B)
 	| eq_var_aux k _ = raise EQ_VAR
   in  eq_var_aux 0  end;
 
-(*Select a suitable equality assumption and substitute throughout the subgoal
-  Replaces only Bound variables if bnd is true*)
-fun gen_hyp_subst_tac bnd i = DETERM (STATE(fn state =>
+(*We do not try to delete ALL equality assumptions at once.  But
+  it is easy to handle several consecutive equality assumptions in a row.
+  Note that we have to inspect the proof state after doing the rewriting,
+  since e.g. z=f(x); x=z changes to z=f(x); x=f(x) and the second equality
+  must NOT be deleted.  Tactic must rotate or delete m assumptions.
+*)
+fun thin_leading_eqs_tac bnd m i = STATE(fn state =>
+    let fun count []      = 0
+	  | count (A::Bs) = ((inspect_pair bnd true (dest_eq A);  
+			      1 + count Bs)
+                             handle Match => 0)
+	val (_,_,Bi,_) = dest_state(state,i)
+        val j = min [m, count (Logic.strip_assums_hyp Bi)]
+    in  REPEAT_DETERM_N j     (etac thin_rl i)   THEN
+        REPEAT_DETERM_N (m-j) (etac revcut_rl i)
+    end);
+
+(*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)))
+      then th RS Data.eq_reflection
+      else symmetric(th RS Data.eq_reflection) (*reorient*) ] 
+    handle Match => [];  (*Exception comes from inspect_pair or dest_eq*)
+
+local open Simplifier 
+in
+
+  val hyp_subst_ss = empty_ss setmksimps mk_eqs
+
+  (*Select a suitable equality assumption and substitute throughout the subgoal
+    Replaces only Bound variables if bnd is true*)
+  fun gen_hyp_subst_tac bnd i = DETERM (STATE(fn state =>
+	let val (_,_,Bi,_) = dest_state(state,i)
+	    val n = length(Logic.strip_assums_hyp Bi) - 1
+	    val (k,_) = eq_var bnd true Bi
+	in 
+	   EVERY [REPEAT_DETERM_N k (etac revcut_rl i),
+		  asm_full_simp_tac hyp_subst_ss i,
+		  etac thin_rl i,
+		  thin_leading_eqs_tac bnd (n-k) i]
+	end
+	handle THM _ => no_tac | EQ_VAR => no_tac));
+
+end;
+
+val ssubst = standard (sym RS subst);
+
+(*Old version of the tactic above -- slower but the only way
+  to handle equalities containing Vars.*)
+fun vars_gen_hyp_subst_tac bnd i = DETERM (STATE(fn state =>
       let val (_,_,Bi,_) = dest_state(state,i)
 	  val n = length(Logic.strip_assums_hyp Bi) - 1
-	  val (k,symopt) = eq_var bnd Bi
+	  val (k,symopt) = eq_var bnd false Bi
       in 
 	 EVERY [REPEAT_DETERM_N k (etac rev_mp i),
 		etac revcut_rl i,
 		REPEAT_DETERM_N (n-k) (etac rev_mp i),
-		etac (symopt RS subst) i,
+		etac (if symopt then ssubst else subst) i,
 		REPEAT_DETERM_N n (rtac imp_intr i)]
       end
       handle THM _ => no_tac | EQ_VAR => no_tac));
 
 (*Substitutes for Free or Bound variables*)
-val hyp_subst_tac = gen_hyp_subst_tac false;
+val hyp_subst_tac = 
+    gen_hyp_subst_tac false ORELSE' 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;
+val bound_hyp_subst_tac = 
+    gen_hyp_subst_tac true ORELSE' vars_gen_hyp_subst_tac true;
 
 end
 end;