# HG changeset patch # User lcp # Date 761403380 -3600 # Node ID d506ea00c8257dbef38b3459fecd9ab7dd8be203 # Parent 237d57b956c19d4fc142c59f2c3a6a243db143b0 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 diff -r 237d57b956c1 -r d506ea00c825 src/Pure/tactic.ML --- a/src/Pure/tactic.ML Wed Feb 16 09:22:15 1994 +0100 +++ b/src/Pure/tactic.ML Wed Feb 16 13:56:20 1994 +0100 @@ -25,6 +25,7 @@ val compose_inst_tac: (string*string)list -> (bool*thm*int) -> int -> tactic val compose_tac: (bool * thm * int) -> int -> tactic 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 val dresolve_tac: thm list -> int -> tactic val dres_inst_tac: (string*string)list -> thm -> int -> tactic @@ -216,23 +217,29 @@ fun eres_inst_tac sinsts rule i = compose_inst_tac sinsts (true, rule, nprems_of rule) i; -(*For forw_inst_tac and dres_inst_tac: preserve Var indexes of rl. - Fails if rl's major premise contains !! or ==> ; it should not anyway!*) +(*For forw_inst_tac and dres_inst_tac. Preserve Var indexes of rl; + increment revcut_rl instead.*) fun make_elim_preserve rl = - let val revcut_rl' = lift_rule (rl,1) revcut_rl + let val {maxidx,...} = rep_thm rl + fun cvar ixn = cterm_of Sign.pure (Var(ixn,propT)); + val revcut_rl' = + instantiate ([], [(cvar("V",0), cvar("V",maxidx+1)), + (cvar("W",0), cvar("W",maxidx+1))]) revcut_rl val arg = (false, rl, nprems_of rl) val [th] = Sequence.list_of_s (bicompose false arg 1 revcut_rl') in th end handle Bind => raise THM("make_elim_preserve", 1, [rl]); -(*forward version*) -fun forw_inst_tac sinsts rule = - res_inst_tac sinsts (make_elim_preserve rule) THEN' assume_tac; +(*instantiate and cut -- for a FACT, anyway...*) +fun cut_inst_tac sinsts rule = res_inst_tac sinsts (make_elim_preserve rule); -(*dresolve version*) +(*forward tactic applies a RULE to an assumption without deleting it*) +fun forw_inst_tac sinsts rule = cut_inst_tac sinsts rule THEN' assume_tac; + +(*dresolve tactic applies a RULE to replace an assumption*) fun dres_inst_tac sinsts rule = eres_inst_tac sinsts (make_elim_preserve rule); -(*** Applications of cut_rl -- forward reasoning ***) +(*** Applications of cut_rl ***) (*Used by metacut_tac*) fun bires_cut_tac arg i =