removed unused term_lift_inst_rule (superceded by Subgoal.FOCUS etc.);
authorwenzelm
Sat Mar 06 14:35:06 2010 +0100 (2010-03-06)
changeset 3561107a8904f8fcd
parent 35610 a5b7a0903441
child 35612 0a9fb49a086d
removed unused term_lift_inst_rule (superceded by Subgoal.FOCUS etc.);
src/Pure/tactic.ML
     1.1 --- a/src/Pure/tactic.ML	Sat Mar 06 14:28:31 2010 +0100
     1.2 +++ b/src/Pure/tactic.ML	Sat Mar 06 14:35:06 2010 +0100
     1.3 @@ -63,8 +63,6 @@
     1.4  sig
     1.5    include BASIC_TACTIC
     1.6    val innermost_params: int -> thm -> (string * typ) list
     1.7 -  val term_lift_inst_rule:
     1.8 -    thm * int * ((indexname * sort) * typ) list * ((indexname * typ) * term) list * thm -> thm
     1.9    val insert_tagged_brl: 'a * (bool * thm) ->
    1.10      ('a * (bool * thm)) Net.net * ('a * (bool * thm)) Net.net ->
    1.11        ('a * (bool * thm)) Net.net * ('a * (bool * thm)) Net.net
    1.12 @@ -193,40 +191,6 @@
    1.13  (*params of subgoal i as they are printed*)
    1.14  fun params_of_state i st = rev (innermost_params i st);
    1.15  
    1.16 -(*
    1.17 -Like lift_inst_rule but takes terms, not strings, where the terms may contain
    1.18 -Bounds referring to parameters of the subgoal.
    1.19 -
    1.20 -insts: [...,(vj,tj),...]
    1.21 -
    1.22 -The tj may contain references to parameters of subgoal i of the state st
    1.23 -in the form of Bound k, i.e. the tj may be subterms of the subgoal.
    1.24 -To saturate the lose bound vars, the tj are enclosed in abstractions
    1.25 -corresponding to the parameters of subgoal i, thus turning them into
    1.26 -functions. At the same time, the types of the vj are lifted.
    1.27 -
    1.28 -NB: the types in insts must be correctly instantiated already,
    1.29 -    i.e. Tinsts is not applied to insts.
    1.30 -*)
    1.31 -fun term_lift_inst_rule (st, i, Tinsts, insts, rule) =
    1.32 -let
    1.33 -    val thy = Thm.theory_of_thm st
    1.34 -    val cert = Thm.cterm_of thy
    1.35 -    val certT = Thm.ctyp_of thy
    1.36 -    val maxidx = Thm.maxidx_of st
    1.37 -    val paramTs = map #2 (params_of_state i st)
    1.38 -    val inc = maxidx+1
    1.39 -    fun liftvar ((a,j), T) = Var((a, j+inc), paramTs---> Logic.incr_tvar inc T)
    1.40 -    (*lift only Var, not term, which must be lifted already*)
    1.41 -    fun liftpair (v,t) = (cert (liftvar v), cert t)
    1.42 -    fun liftTpair (((a, i), S), T) =
    1.43 -      (certT (TVar ((a, i + inc), S)),
    1.44 -       certT (Logic.incr_tvar inc T))
    1.45 -in Drule.instantiate (map liftTpair Tinsts, map liftpair insts)
    1.46 -                     (Thm.lift_rule (Thm.cprem_of st i) rule)
    1.47 -end;
    1.48 -
    1.49 -
    1.50  
    1.51  (*** Applications of cut_rl ***)
    1.52