--- 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. ***)