# HG changeset patch
# User nipkow
# Date 842288021 -7200
# Node ID 9e626f86e3352fa5c6b073d11ef3391eeacffe6b
# Parent  789c12ea0b30366d64677f4b79c43fed2b2cde8c
added cterm_lift_inst_rule

diff -r 789c12ea0b30 -r 9e626f86e335 src/Pure/tactic.ML
--- a/src/Pure/tactic.ML	Mon Sep 09 17:44:20 1996 +0200
+++ b/src/Pure/tactic.ML	Mon Sep 09 18:53:41 1996 +0200
@@ -24,6 +24,8 @@
       (bool*thm)list -> (int*(bool*thm)) Net.net * (int*(bool*thm)) Net.net
   val compose_inst_tac: (string*string)list -> (bool*thm*int) -> int -> tactic
   val compose_tac: (bool * thm * int) -> int -> tactic 
+  val cterm_lift_inst_rule:
+      thm * int * (indexname*ctyp)list * (term*cterm)list  * thm -> thm
   val cut_facts_tac: thm list -> int -> tactic
   val cut_inst_tac: (string*string)list -> thm -> int -> tactic   
   val dmatch_tac: thm list -> int -> tactic
@@ -198,6 +200,27 @@
                (lift_rule (st,i) rule)
 end;
 
+(*Like lift_inst_rule but takes cterms, not strings.
+  The cterms must be functions of the parameters of the subgoal,
+  i.e. they are assumed to be lifted already!
+  Also: types of Vars must be fully instantiated already *)
+fun cterm_lift_inst_rule (st, i, Tinsts, insts, rule) =
+let val {maxidx,sign,...} = rep_thm st
+    val (_, _, Bi, _) = dest_state(st,i)
+    val params = Logic.strip_params Bi          (*params of subgoal i*)
+    val paramTs = map #2 params
+    and inc = maxidx+1
+    fun liftvar (Var ((a,j), T)) =
+          cterm_of sign (Var((a, j+inc), paramTs---> incr_tvar inc T))
+      | liftvar t = raise TERM("Variable expected", [t]);
+    (*lift only Var, not cterm! Must to be lifted already*)
+    fun liftpair (v,ct) = (liftvar v, ct)
+    fun lifttvar((a,i),ctyp) =
+        let val {T,sign} = rep_ctyp ctyp
+        in  ((a,i+inc), ctyp_of sign (incr_tvar inc T)) end
+in instantiate (map lifttvar Tinsts, map liftpair insts)
+               (lift_rule (st,i) rule)
+end;
 
 (*** Resolve after lifting and instantation; may refer to parameters of the
      subgoal.  Fails if "i" is out of range.  ***)