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.
--- 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 **)
--- 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);
--- 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