fixed strip_assums and assum_pairs, restoring them (essentially) to their
authorpaulson
Thu Aug 24 11:14:21 2000 +0200 (2000-08-24)
changeset 96846b7d7635a062
parent 9683 f87c8c449018
child 9685 6d123a7e30bd
fixed strip_assums and assum_pairs, restoring them (essentially) to their
1989 versions. They had been "optimized" for flattened parameters, but
failed when given an initial, non-flattened proof state. A manifestation
of the bug is

Goal "of the bug isf. EX B. Q(f,B) ==> (of the bug isy. P(f,y))";
be exE 1;
src/Pure/logic.ML
     1.1 --- a/src/Pure/logic.ML	Thu Aug 24 11:05:20 2000 +0200
     1.2 +++ b/src/Pure/logic.ML	Thu Aug 24 11:14:21 2000 +0200
     1.3 @@ -314,13 +314,19 @@
     1.4        all T $ Abs(c, T, list_rename_params (cs, t))
     1.5    | list_rename_params (cs, B) = B;
     1.6  
     1.7 -(*Strips assumptions in goal yielding  ( [Hn,...,H1], [xm,...,x1], B )
     1.8 -  where H1,...,Hn are the hypotheses and x1...xm are the parameters.   *)
     1.9 -fun strip_assums_aux (Hs, params, Const("==>", _) $ H $ B) =
    1.10 -        strip_assums_aux (H::Hs, params, B)
    1.11 -  | strip_assums_aux (Hs, params, Const("all",_)$Abs(a,T,t)) =
    1.12 -        strip_assums_aux (Hs, (a,T)::params, t)
    1.13 -  | strip_assums_aux (Hs, params, B) = (Hs, params, B);
    1.14 +(*Strips assumptions in goal yielding  ( [HPn,...,HP1], [xm,...,x1], B ).
    1.15 +  Where HPi has the form (Hi,nparams_i) and x1...xm are the parameters.
    1.16 +  We need nparams_i only when the parameters aren't flattened; then we
    1.17 +    must call incr_boundvars to make up the difference.  See assum_pairs.
    1.18 +  Without this refinement we can get the wrong answer, e.g. by
    1.19 +	Goal "!!f. EX B. Q(f,B) ==> (!!y. P(f,y))";
    1.20 +	by (etac exE 1);
    1.21 + *)
    1.22 +fun strip_assums_aux (HPs, params, Const("==>", _) $ H $ B) =
    1.23 +        strip_assums_aux ((H,length params)::HPs, params, B)
    1.24 +  | strip_assums_aux (HPs, params, Const("all",_)$Abs(a,T,t)) =
    1.25 +        strip_assums_aux (HPs, (a,T)::params, t)
    1.26 +  | strip_assums_aux (HPs, params, B) = (HPs, params, B);
    1.27  
    1.28  fun strip_assums A = strip_assums_aux ([],[],A);
    1.29  
    1.30 @@ -329,15 +335,17 @@
    1.31    A is the first premise of the lifted rule, and thus has the form
    1.32      H1 ==> ... Hk ==> B   and the pairs are (H1,B),...,(Hk,B) *)
    1.33  fun assum_pairs A =
    1.34 -  let val (Hs, params, B) = strip_assums A
    1.35 +  let val (HPs, params, B) = strip_assums A
    1.36 +      val nparams = length params
    1.37        val D = Unify.rlist_abs(params, B)
    1.38 +      fun incr_hyp(H,np) = 
    1.39 +	  Unify.rlist_abs(params, incr_boundvars (nparams-np) H)
    1.40        fun pairrev ([],pairs) = pairs
    1.41 -        | pairrev (H::Hs,pairs) =
    1.42 -            pairrev(Hs, (Unify.rlist_abs(params,H), D) :: pairs)
    1.43 -  in  pairrev (Hs,[])   (*WAS:  map pair (rev Hs)  *)
    1.44 +        | pairrev ((H,np)::HPs, pairs) =
    1.45 +            pairrev(HPs,  (incr_hyp(H,np),D) :: pairs)
    1.46 +  in  pairrev (HPs,[]) 
    1.47    end;
    1.48  
    1.49 -
    1.50  (*Converts Frees to Vars and TFrees to TVars so that axioms can be written
    1.51    without (?) everywhere*)
    1.52  fun varify (Const(a,T)) = Const(a, Type.varifyT T)