tactic/make_elim_preserve: recoded to avoid using lift_inst_rule. Instead
authorlcp
Wed Feb 16 13:56:20 1994 +0100 (1994-02-16)
changeset 270d506ea00c825
parent 269 237d57b956c1
child 271 d773733dfc74
tactic/make_elim_preserve: recoded to avoid using lift_inst_rule. Instead
instantiate changes the indices of V and W.

tactic/cut_inst_tac: new
src/Pure/tactic.ML
     1.1 --- a/src/Pure/tactic.ML	Wed Feb 16 09:22:15 1994 +0100
     1.2 +++ b/src/Pure/tactic.ML	Wed Feb 16 13:56:20 1994 +0100
     1.3 @@ -25,6 +25,7 @@
     1.4    val compose_inst_tac: (string*string)list -> (bool*thm*int) -> int -> tactic
     1.5    val compose_tac: (bool * thm * int) -> int -> tactic 
     1.6    val cut_facts_tac: thm list -> int -> tactic
     1.7 +  val cut_inst_tac: (string*string)list -> thm -> int -> tactic   
     1.8    val dmatch_tac: thm list -> int -> tactic
     1.9    val dresolve_tac: thm list -> int -> tactic
    1.10    val dres_inst_tac: (string*string)list -> thm -> int -> tactic   
    1.11 @@ -216,23 +217,29 @@
    1.12  fun eres_inst_tac sinsts rule i =
    1.13      compose_inst_tac sinsts (true, rule, nprems_of rule) i;
    1.14  
    1.15 -(*For forw_inst_tac and dres_inst_tac: preserve Var indexes of rl.
    1.16 -  Fails if rl's major premise contains !! or ==> ; it should not anyway!*)
    1.17 +(*For forw_inst_tac and dres_inst_tac.  Preserve Var indexes of rl;
    1.18 +  increment revcut_rl instead.*)
    1.19  fun make_elim_preserve rl = 
    1.20 -  let val revcut_rl' = lift_rule (rl,1) revcut_rl
    1.21 +  let val {maxidx,...} = rep_thm rl
    1.22 +      fun cvar ixn = cterm_of Sign.pure (Var(ixn,propT));
    1.23 +      val revcut_rl' = 
    1.24 +	  instantiate ([],  [(cvar("V",0), cvar("V",maxidx+1)),
    1.25 +			     (cvar("W",0), cvar("W",maxidx+1))]) revcut_rl
    1.26        val arg = (false, rl, nprems_of rl)
    1.27        val [th] = Sequence.list_of_s (bicompose false arg 1 revcut_rl')
    1.28    in  th  end
    1.29    handle Bind => raise THM("make_elim_preserve", 1, [rl]);
    1.30  
    1.31 -(*forward version*)
    1.32 -fun forw_inst_tac sinsts rule =
    1.33 -    res_inst_tac sinsts (make_elim_preserve rule) THEN' assume_tac;
    1.34 +(*instantiate and cut -- for a FACT, anyway...*)
    1.35 +fun cut_inst_tac sinsts rule = res_inst_tac sinsts (make_elim_preserve rule);
    1.36  
    1.37 -(*dresolve version*)
    1.38 +(*forward tactic applies a RULE to an assumption without deleting it*)
    1.39 +fun forw_inst_tac sinsts rule = cut_inst_tac sinsts rule THEN' assume_tac;
    1.40 +
    1.41 +(*dresolve tactic applies a RULE to replace an assumption*)
    1.42  fun dres_inst_tac sinsts rule = eres_inst_tac sinsts (make_elim_preserve rule);
    1.43  
    1.44 -(*** Applications of cut_rl -- forward reasoning ***)
    1.45 +(*** Applications of cut_rl ***)
    1.46  
    1.47  (*Used by metacut_tac*)
    1.48  fun bires_cut_tac arg i =