# HG changeset patch
# User berghofe
# Date 1383050898 -3600
# Node ID c0c453ce70a759b3d0b833962840a468a19b1926
# Parent  ab0595cb9fe9b2edb24fd06903e2b7c5217ab91e
inst_lift now fully instantiates context to avoid problems with loose bound variables

diff -r ab0595cb9fe9 -r c0c453ce70a7 src/Provers/splitter.ML
--- a/src/Provers/splitter.ML	Tue Oct 29 12:13:00 2013 +0100
+++ b/src/Provers/splitter.ML	Tue Oct 29 13:48:18 2013 +0100
@@ -79,6 +79,8 @@
   fold add_thm splits []
 end;
 
+val abss = fold (Term.abs o pair "");
+
 (* ------------------------------------------------------------------------- *)
 (* mk_case_split_tac                                                         *)
 (* ------------------------------------------------------------------------- *)
@@ -100,31 +102,36 @@
   (Syntax.read_prop_global Pure.thy "P(%x. Q(x)) == P(%x. R(x))")
   (fn {prems, ...} => rewrite_goals_tac prems THEN rtac reflexive_thm 1)
 
+val _ $ _ $ (_ $ (_ $ abs_lift) $ _) = prop_of lift;
+
 val trlift = lift RS transitive_thm;
-val _ $ (P $ _) $ _ = concl_of trlift;
 
 
 (************************************************************************
    Set up term for instantiation of P in the lift-theorem
 
-   Ts    : types of parameters (i.e. variables bound by meta-quantifiers)
    t     : lefthand side of meta-equality in subgoal
            the lift theorem is applied to (see select)
    pos   : "path" leading to abstraction, coded as a list
    T     : type of body of P(...)
-   maxi  : maximum index of Vars
 *************************************************************************)
 
-fun mk_cntxt Ts t pos T maxi =
-  let fun var (t,i) = Var(("X",i),type_of1(Ts,t));
-      fun down [] t i = Bound 0
-        | down (p::ps) t i =
-            let val (h,ts) = strip_comb t
-                val v1 = ListPair.map var (take p ts, i upto (i+p-1))
-                val u::us = drop p ts
-                val v2 = ListPair.map var (us, (i+p) upto (i+length(ts)-2))
-      in list_comb(h,v1@[down ps u (i+length ts)]@v2) end;
-  in Abs("", T, down (rev pos) t maxi) end;
+fun mk_cntxt t pos T =
+  let
+    fun down [] t = (Bound 0, t)
+      | down (p :: ps) t =
+          let
+            val (h, ts) = strip_comb t
+            val (ts1, u :: ts2) = chop p ts
+            val (u1, u2) = down ps u
+          in
+            (list_comb (incr_boundvars 1 h,
+               map (incr_boundvars 1) ts1 @ u1 ::
+               map (incr_boundvars 1) ts2),
+             u2)
+          end;
+    val (u1, u2) = down (rev pos) t
+  in (Abs ("", T, u1), u2) end;
 
 
 (************************************************************************
@@ -301,15 +308,18 @@
              the split theorem is applied to (see cmap)
    T,U,pos : see mk_split_pack
    state   : current proof state
-   lift    : the lift theorem
    i       : no. of subgoal
 **************************************************************)
 
 fun inst_lift Ts t (T, U, pos) state i =
   let
     val cert = cterm_of (Thm.theory_of_thm state);
-    val cntxt = mk_cntxt Ts t pos (T --> U) (Thm.maxidx_of trlift);
-  in cterm_instantiate [(cert P, cert cntxt)] trlift
+    val (cntxt, u) = mk_cntxt t pos (T --> U);
+    val trlift' = Thm.lift_rule (Thm.cprem_of state i)
+      (Thm.rename_boundvars abs_lift u trlift);
+    val (P, _) = strip_comb (fst (Logic.dest_equals
+      (Logic.strip_assums_concl (Thm.prop_of trlift'))));
+  in cterm_instantiate [(cert P, cert (abss Ts cntxt))] trlift'
   end;
 
 
@@ -333,7 +343,6 @@
       (Logic.strip_assums_concl (Thm.prop_of thm'))));
     val cert = cterm_of (Thm.theory_of_thm state);
     val cntxt = mk_cntxt_splitthm t tt TB;
-    val abss = fold (fn T => fn t => Abs ("", T, t));
   in cterm_instantiate [(cert P, cert (abss Ts cntxt))] thm'
   end;
 
@@ -348,7 +357,7 @@
 fun split_tac [] i = no_tac
   | split_tac splits i =
   let val cmap = cmap_of_split_thms splits
-      fun lift_tac Ts t p st = rtac (inst_lift Ts t p st i) i st
+      fun lift_tac Ts t p st = compose_tac (false, inst_lift Ts t p st i, 2) i st
       fun lift_split_tac state =
             let val (Ts, t, splits) = select cmap state i
             in case splits of