# HG changeset patch
# User nipkow
# Date 757794836 -3600
# Node ID ed6a3e2b1a33bffd1b1e9aad4fdd58145cc7f467
# Parent  42f2b8a3581fd1805a9800a90d2a6f0a2b889b00
added new parameter to the simplification tactics which indicates if
assumptions are to be simplified and/or to be used when simplifying the
conclusion. This gets rid of METAHYPS and speeds up simplification of goals
with big assumptions.

diff -r 42f2b8a3581f -r ed6a3e2b1a33 src/Pure/drule.ML
--- a/src/Pure/drule.ML	Wed Jan 05 19:29:51 1994 +0100
+++ b/src/Pure/drule.ML	Wed Jan 05 19:33:56 1994 +0100
@@ -50,8 +50,8 @@
   val read_instantiate_sg: Sign.sg -> (string*string)list -> thm -> thm
   val reflexive_thm: thm
   val revcut_rl: thm
-  val rewrite_goal_rule: (meta_simpset -> thm -> thm option) -> meta_simpset ->
-        int -> thm -> thm
+  val rewrite_goal_rule: bool*bool -> (meta_simpset -> thm -> thm option)
+        -> meta_simpset -> int -> thm -> thm
   val rewrite_goals_rule: thm list -> thm -> thm
   val rewrite_rule: thm list -> thm -> thm
   val RS: thm * thm -> thm
@@ -376,18 +376,18 @@
       val xythm = Thm.assume xy and yzthm = Thm.assume yz
   in standard(Thm.implies_intr yz (Thm.transitive xythm yzthm)) end;
 
-
 (** Below, a "conversion" has type sign->term->thm **)
 
 (*In [A1,...,An]==>B, rewrite the selected A's only -- for rewrite_goals_tac*)
+(*Do not rewrite flex-flex pairs*)
 fun goals_conv pred cv sign = 
   let val triv = reflexive o Sign.fake_cterm_of sign
       fun gconv i t =
         let val (A,B) = Logic.dest_implies t
-	    val thA = if (pred i) then (cv sign A) else (triv A)
-	in  combination (combination (triv implies) thA)
-                        (gconv (i+1) B)
-        end
+            val (thA,j) = case A of
+                  Const("=?=",_)$_$_ => (triv A,i)
+                | _ => (if pred i then cv sign A else triv A, i+1)
+	in  combination (combination (triv implies) thA) (gconv j B) end
         handle TERM _ => triv t
   in gconv 1 end;
 
@@ -397,19 +397,23 @@
   in  equal_elim (cv sign prop) th  end;
 
 (*rewriting conversion*)
-fun rew_conv prover mss sign t =
-  rewrite_cterm mss prover (Sign.fake_cterm_of sign t);
+fun rew_conv mode prover mss sign t =
+  rewrite_cterm mode mss prover (Sign.fake_cterm_of sign t);
 
 (*Rewrite a theorem*)
-fun rewrite_rule thms = fconv_rule (rew_conv (K(K None)) (Thm.mss_of thms));
+fun rewrite_rule thms =
+  fconv_rule (rew_conv (true,false) (K(K None)) (Thm.mss_of thms));
 
 (*Rewrite the subgoals of a proof state (represented by a theorem) *)
 fun rewrite_goals_rule thms =
-  fconv_rule (goals_conv (K true) (rew_conv (K(K None)) (Thm.mss_of thms)));
+  fconv_rule (goals_conv (K true) (rew_conv (true,false) (K(K None))
+             (Thm.mss_of thms)));
 
 (*Rewrite the subgoal of a proof state (represented by a theorem) *)
-fun rewrite_goal_rule prover mss i =
-      fconv_rule (goals_conv (fn j => j=i) (rew_conv prover mss));
+fun rewrite_goal_rule mode prover mss i thm =
+  if 0 < i  andalso  i <= nprems_of thm
+  then fconv_rule (goals_conv (fn j => j=i) (rew_conv mode prover mss)) thm
+  else raise THM("rewrite_goal_rule",i,[thm]);
 
 
 (** Derived rules mainly for METAHYPS **)
diff -r 42f2b8a3581f -r ed6a3e2b1a33 src/Pure/tactic.ML
--- a/src/Pure/tactic.ML	Wed Jan 05 19:29:51 1994 +0100
+++ b/src/Pure/tactic.ML	Wed Jan 05 19:33:56 1994 +0100
@@ -13,7 +13,7 @@
   in
   val ares_tac: thm list -> int -> tactic
   val asm_rewrite_goal_tac:
-        (meta_simpset -> tactic) -> meta_simpset -> int -> tactic
+        bool*bool -> (meta_simpset -> tactic) -> meta_simpset -> int -> tactic
   val assume_tac: int -> tactic
   val atac: int ->tactic
   val bimatch_from_nets_tac: (int*(bool*thm)) net * (int*(bool*thm)) net -> int -> tactic
@@ -373,8 +373,8 @@
   | Some(thm,_) => Some(thm);
 
 (*Rewrite subgoal i only *)
-fun asm_rewrite_goal_tac prover_tac mss i =
-      PRIMITIVE(rewrite_goal_rule (result1 prover_tac) mss i);
+fun asm_rewrite_goal_tac mode prover_tac mss i =
+      PRIMITIVE(rewrite_goal_rule mode (result1 prover_tac) mss i);
 
 (*Rewrite throughout proof state. *)
 fun rewrite_tac defs = PRIMITIVE(rewrite_rule defs);
diff -r 42f2b8a3581f -r ed6a3e2b1a33 src/Pure/thm.ML
--- a/src/Pure/thm.ML	Wed Jan 05 19:29:51 1994 +0100
+++ b/src/Pure/thm.ML	Wed Jan 05 19:33:56 1994 +0100
@@ -66,8 +66,9 @@
   val reflexive: Sign.cterm -> thm 
   val rename_params_rule: string list * int -> thm -> thm
   val rep_thm: thm -> {prop: term, hyps: term list, maxidx: int, sign: Sign.sg}
-  val rewrite_cterm: meta_simpset -> (meta_simpset -> thm -> thm option)
-                     -> Sign.cterm -> thm
+  val rewrite_cterm:
+         bool*bool -> meta_simpset -> (meta_simpset -> thm -> thm option)
+           -> Sign.cterm -> thm
   val set_mk_rews: meta_simpset * (thm -> thm list) -> meta_simpset
   val sign_of: theory -> Sign.sg   
   val syn_of: theory -> Sign.Syntax.syntax
@@ -954,7 +955,7 @@
   end;
 
 
-fun bottomc (prover,sign) =
+fun bottomc ((simprem,useprem),prover,sign) =
   let fun botc mss trec = let val trec1 = subc mss trec
                           in case rewritec (prover,sign) mss trec1 of
                                None => trec1
@@ -988,12 +989,11 @@
           | _ => trec)
 
       and impc(hyps,s,u,mss as Mss{mk_rews,...}) =
-        let val (hyps1,s') = botc mss (hyps,s)
-            val (rthms,mss) =
-              if maxidx_of_term s' <> ~1 then ([],mss)
+        let val (hyps1,s') = if simprem then botc mss (hyps,s) else (hyps,s)
+            val mss' =
+              if not useprem orelse maxidx_of_term s' <> ~1 then mss
               else let val thm = Thm{sign=sign,hyps=[s'],prop=s',maxidx= ~1}
-                   in (mk_rews thm, add_prems(mss,[thm])) end
-            val mss' = add_simps(mss,rthms)
+                   in add_simps(add_prems(mss,[thm]), mk_rews thm) end
             val (hyps2,u') = botc mss' (hyps1,u)
             val hyps2' = if s' mem hyps1 then hyps2 else hyps2\s'
         in (hyps2', Logic.mk_implies(s',u')) end
@@ -1003,14 +1003,15 @@
 
 (*** Meta-rewriting: rewrites t to u and returns the theorem t==u ***)
 (* Parameters:
+   mode = (simplify A, use A in simplifying B) when simplifying A ==> B 
    mss: contains equality theorems of the form [|p1,...|] ==> t==u
    prover: how to solve premises in conditional rewrites and congruences
 *)
 
 (*** FIXME: check that #primes(mss) does not "occur" in ct alread ***)
-fun rewrite_cterm mss prover ct =
+fun rewrite_cterm mode mss prover ct =
   let val {sign, t, T, maxidx} = Sign.rep_cterm ct;
-      val (hyps,u) = bottomc (prover,sign) mss ([],t);
+      val (hyps,u) = bottomc (mode,prover,sign) mss ([],t);
       val prop = Logic.mk_equals(t,u)
   in  Thm{sign= sign, hyps= hyps, maxidx= maxidx_of_term prop, prop= prop}
   end