--- a/src/Pure/thm.ML Thu Mar 12 12:48:49 1998 +0100
+++ b/src/Pure/thm.ML Thu Mar 12 12:49:24 1998 +0100
@@ -1682,6 +1682,9 @@
fun extract_safe_rrules(mss,thm) =
flat (map (orient_rrule mss) (extract_rews(mss,[thm])));
+fun add_safe_simp(mss,thm) =
+ foldl insert_rrule (mss, extract_safe_rrules(mss,thm))
+
(* del_simps *)
fun del_rrule(mss as Mss {rules,...},
@@ -2000,7 +2003,7 @@
| None => None
end
| t$u => (case t of
- Const("==>",_)$s => Some(snd(impc([],s,u,mss,etc)))
+ Const("==>",_)$s => Some(impc(s,u,mss,etc))
| Abs(_,_,body) =>
let val trec = (subst_bound(u,body), etc)
in case subc mss trec of
@@ -2030,28 +2033,32 @@
end)
| _ => None)
- and impc(prems, prem, conc, mss, etc) =
- let val (prem1,etc1) = if simprem then try_botc mss (prem,etc)
- else (prem,etc)
- in impc1(prems, prem1, conc, mss, etc1) end
+ and impc args =
+ if mutsimp
+ then let val (prem, conc, mss, etc) = args
+ in snd(mut_impc([], prem, conc, mss, etc)) end
+ else nonmut_impc args
- and impc1(prems, prem1, conc, mss, etc1 as (_,hyps1,_)) =
+ and mut_impc (prems, prem, conc, mss, etc) =
+ let val (prem1,etc1) = try_botc mss (prem,etc)
+ in mut_impc1(prems, prem1, conc, mss, etc1) end
+
+ and mut_impc1(prems, prem1, conc, mss, etc1 as (_,hyps1,_)) =
let
fun uncond({thm,lhs,...}:rrule) =
if nprems_of thm = 0 then Some lhs else None
- val (rrules1,lhss1,mss1) =
- if not useprem then ([],[],mss) else
+ val (lhss1,mss1) =
if maxidx_of_term prem1 <> ~1
then (trace_term true "Cannot add premise as rewrite rule because it contains (type) unknowns:"
(Sign.deref sign_ref) prem1;
- ([],[],mss))
+ ([],mss))
else let val thm = assume (Cterm{sign_ref=sign_ref, t=prem1,
T=propT, maxidx= ~1})
val rrules1 = extract_safe_rrules(mss,thm)
- val lhss1 = if mutsimp then mapfilter uncond rrules1 else []
+ val lhss1 = mapfilter uncond rrules1
val mss1 = foldl insert_rrule (add_prems(mss,[thm]),rrules1)
- in (rrules1, lhss1, mss1) end
+ in (lhss1, mss1) end
fun disch1(conc2,(shyps2,hyps2,ders2)) =
let val hyps2' = if gen_mem (op aconv) (prem1, hyps1)
@@ -2063,24 +2070,23 @@
in case rewritec (prover,sign_ref,maxidx) mss trec of
None => (None,trec)
| Some(Const("==>",_)$prem$conc,etc) =>
- impc(prems,prem,conc,mss,etc)
+ mut_impc(prems,prem,conc,mss,etc)
| Some(trec') => (None,trec')
end
fun simpconc() =
case conc of
Const("==>",_)$s$t =>
- (case impc(prems@[prem1],s,t,mss1,etc1) of
+ (case mut_impc(prems@[prem1],s,t,mss1,etc1) of
(Some(i,prem),trec2) =>
let val trec2' = disch1 trec2
- in if i=0 then impc1(prems,prem,fst trec2',mss,snd trec2')
+ in if i=0 then mut_impc1(prems,prem,fst trec2',mss,snd trec2')
else (Some(i-1,prem),trec2')
end
| (None,trec) => rebuild(trec))
| _ => rebuild(try_botc mss1 (conc,etc1))
- in if mutsimp
- then let val sg = Sign.deref sign_ref
+ in let val sg = Sign.deref sign_ref
val tsig = #tsig(Sign.rep_sg sg)
fun reducible t =
exists (fn lhs => Pattern.matches_subterm tsig (lhs,t))
@@ -2091,9 +2097,26 @@
red;
(Some(length rest,prem1),(conc,etc1)))
end
- else simpconc()
end
+ (* legacy code - only for backwards compatibility *)
+ and nonmut_impc(prem, conc, mss, etc as (_,hyps1,_)) =
+ let val (prem1,etc1) = if simprem then try_botc mss (prem,etc)
+ else (prem,etc)
+ val maxidx1 = maxidx_of_term prem1
+ val mss1 =
+ if not useprem then mss else
+ if maxidx1 <> ~1
+ then (trace_term true "Cannot add premise as rewrite rule because it contains (type) unknowns:"
+ (Sign.deref sign_ref) prem1;
+ mss)
+ else let val thm = assume (Cterm{sign_ref=sign_ref, t=prem1,
+ T=propT, maxidx= ~1})
+ in add_safe_simp(add_prems(mss,[thm]), thm) end
+ val (conc2,(shyps2,hyps2,ders2)) = try_botc mss1 (conc,etc1)
+ val hyps2' = if prem1 mem hyps1 then hyps2 else hyps2\prem1
+ in (Logic.mk_implies(prem1,conc2), (shyps2, hyps2', ders2)) end
+
in try_botc end;