--- a/NEWS Mon Jan 24 12:40:52 2005 +0100
+++ b/NEWS Mon Jan 24 12:41:06 2005 +0100
@@ -34,6 +34,10 @@
* Provers/blast.ML: new reference depth_limit to make blast's depth
limit (previously hard-coded with a value of 20) user-definable.
+* Pure: thin_tac now works even if the assumption being deleted contains !! or ==>.
+ More generally, erule now works even if the major premise of the elimination rule
+ contains !! or ==>.
+
* Pure: considerably improved version of 'constdefs' command. Now
performs automatic type-inference of declared constants; additional
support for local structure declarations (cf. locales and HOL
--- a/src/Pure/logic.ML Mon Jan 24 12:40:52 2005 +0100
+++ b/src/Pure/logic.ML Mon Jan 24 12:41:06 2005 +0100
@@ -46,7 +46,7 @@
val auto_rename : bool ref
val set_rename_prefix : string -> unit
val list_rename_params: string list * term -> term
- val assum_pairs : term -> (term*term)list
+ val assum_pairs : int * term -> (term*term)list
val varify : term -> term
val unvarify : term -> term
val get_goal : term -> int -> term
@@ -296,9 +296,14 @@
the the parameters to be flattened, but it allows erule to work on
assumptions of the form !!x. phi. Any !! after the outermost string
will be regarded as belonging to the conclusion, and left untouched.
- Used ONLY by assum_pairs. *)
-fun strip_assums_imp (Hs, Const("==>", _) $ H $ B) = strip_assums_imp (H::Hs, B)
- | strip_assums_imp (Hs, B) = (Hs, B);
+ Used ONLY by assum_pairs.
+ Unless nasms<0, it can terminate the recursion early; that allows
+ erule to work on assumptions of the form P==>Q.*)
+fun strip_assums_imp (0, Hs, B) = (Hs, B) (*recursion terminated by nasms*)
+ | strip_assums_imp (nasms, Hs, Const("==>", _) $ H $ B) =
+ strip_assums_imp (nasms-1, H::Hs, B)
+ | strip_assums_imp (_, Hs, B) = (Hs, B); (*recursion terminated by B*)
+
(*Strips OUTER parameters only, unlike similar legacy versions.*)
fun strip_assums_all (params, Const("all",_)$Abs(a,T,t)) =
@@ -307,10 +312,12 @@
(*Produces disagreement pairs, one for each assumption proof, in order.
A is the first premise of the lifted rule, and thus has the form
- H1 ==> ... Hk ==> B and the pairs are (H1,B),...,(Hk,B) *)
-fun assum_pairs A =
+ H1 ==> ... Hk ==> B and the pairs are (H1,B),...,(Hk,B).
+ nasms is the number of assumptions in the original subgoal, needed when B
+ has the form B1 ==> B2: it stops B1 from being taken as an assumption. *)
+fun assum_pairs(nasms,A) =
let val (params, A') = strip_assums_all ([],A)
- val (Hs,B) = strip_assums_imp ([],A')
+ val (Hs,B) = strip_assums_imp (nasms,[],A')
fun abspar t = Unify.rlist_abs(params, t)
val D = abspar B
fun pairrev ([], pairs) = pairs
--- a/src/Pure/thm.ML Mon Jan 24 12:40:52 2005 +0100
+++ b/src/Pure/thm.ML Mon Jan 24 12:41:06 2005 +0100
@@ -1143,14 +1143,14 @@
(Seq.mapp (newth n)
(Unify.unifiers(Sign.deref sign_ref,Envir.empty maxidx, (t,u)::tpairs))
(addprfs apairs (n+1))))
- in addprfs (Logic.assum_pairs Bi) 1 end;
+ in addprfs (Logic.assum_pairs (~1,Bi)) 1 end;
(*Solve subgoal Bi of proof state B1...Bn/C by assumption.
Checks if Bi's conclusion is alpha-convertible to one of its assumptions*)
fun eq_assumption i state =
let val Thm{sign_ref,der,maxidx,hyps,prop,...} = state;
val (tpairs, Bs, Bi, C) = dest_state(state,i)
- in (case find_index (op aconv) (Logic.assum_pairs Bi) of
+ in (case find_index (op aconv) (Logic.assum_pairs (~1,Bi)) of
(~1) => raise THM("eq_assumption", 0, [state])
| n => fix_shyps [state] []
(Thm{sign_ref = sign_ref,
@@ -1403,13 +1403,13 @@
fun tryasms (_, _, _, []) = Seq.empty
| tryasms (A, As, n, (t,u)::apairs) =
(case Seq.pull(Unify.unifiers(sign, env, (t,u)::dpairs)) of
- None => tryasms (A, As, n+1, apairs)
- | cell as Some((_,tpairs),_) =>
- Seq.it_right (addth A (newAs(As, n, [BBi,(u,t)], tpairs)))
- (Seq.make (fn()=> cell),
- Seq.make (fn()=> Seq.pull (tryasms (A, As, n+1, apairs)))));
+ None => tryasms (A, As, n+1, apairs)
+ | cell as Some((_,tpairs),_) =>
+ Seq.it_right (addth A (newAs(As, n, [BBi,(u,t)], tpairs)))
+ (Seq.make(fn()=> cell),
+ Seq.make(fn()=> Seq.pull (tryasms(A, As, n+1, apairs)))))
fun eres [] = raise THM("bicompose: no premises", 0, [orule,state])
- | eres (A1::As) = tryasms (Some A1, As, 1, Logic.assum_pairs A1);
+ | eres (A1::As) = tryasms(Some A1, As, 1, Logic.assum_pairs(nlift+1,A1))
(*ordinary resolution*)
fun res(None) = Seq.empty
| res(cell as Some((_,tpairs),_)) =