--- a/src/Pure/logic.ML Fri Jan 21 13:54:09 2005 +0100
+++ b/src/Pure/logic.ML Fri Jan 21 13:55:07 2005 +0100
@@ -288,36 +288,34 @@
all T $ Abs(c, T, list_rename_params (cs, t))
| list_rename_params (cs, B) = B;
-(*Strips assumptions in goal yielding ( [HPn,...,HP1], [xm,...,x1], B ).
- Where HPi has the form (Hi,nparams_i) and x1...xm are the parameters.
- We need nparams_i only when the parameters aren't flattened; then we
- must call incr_boundvars to make up the difference. See assum_pairs.
- Without this refinement we can get the wrong answer, e.g. by
- Goal "!!f. EX B. Q(f,B) ==> (!!y. P(f,y))";
- by (etac exE 1);
- *)
-fun strip_assums_aux (HPs, params, Const("==>", _) $ H $ B) =
- strip_assums_aux ((H,length params)::HPs, params, B)
- | strip_assums_aux (HPs, params, Const("all",_)$Abs(a,T,t)) =
- strip_assums_aux (HPs, (a,T)::params, t)
- | strip_assums_aux (HPs, params, B) = (HPs, params, B);
+(*** Treatmsent of "assume", "erule", etc. ***)
-fun strip_assums A = strip_assums_aux ([],[],A);
+(*Strips assumptions in goal yielding
+ HS = [Hn,...,H1], params = [xm,...,x1], and B,
+ where x1...xm are the parameters. This version (21.1.2005) REQUIRES
+ 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);
+(*Strips OUTER parameters only, unlike similar legacy versions.*)
+fun strip_assums_all (params, Const("all",_)$Abs(a,T,t)) =
+ strip_assums_all ((a,T)::params, t)
+ | strip_assums_all (params, B) = (params, B);
(*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 =
- let val (HPs, params, B) = strip_assums A
- val nparams = length params
- val D = Unify.rlist_abs(params, B)
- fun incr_hyp(H,np) =
- Unify.rlist_abs(params, incr_boundvars (nparams-np) H)
- fun pairrev ([],pairs) = pairs
- | pairrev ((H,np)::HPs, pairs) =
- pairrev(HPs, (incr_hyp(H,np),D) :: pairs)
- in pairrev (HPs,[])
+ let val (params, A') = strip_assums_all ([],A)
+ val (Hs,B) = strip_assums_imp ([],A')
+ fun abspar t = Unify.rlist_abs(params, t)
+ val D = abspar B
+ fun pairrev ([], pairs) = pairs
+ | pairrev (H::Hs, pairs) = pairrev(Hs, (abspar H, D) :: pairs)
+ in pairrev (Hs,[])
end;
(*Converts Frees to Vars and TFrees to TVars so that axioms can be written