src/Pure/Isar/method.ML

   val rule: thm list -> method
   val erule: int -> thm list -> method
   val drule: int -> thm list -> method
   val frule: int -> thm list -> method
   val iprover_tac: Proof.context -> int option -> int -> tactic
-  val bires_inst_tac: bool -> Proof.context -> (indexname * string) list ->
-    thm -> int -> tactic
   val set_tactic: (Proof.context -> thm list -> tactic) -> unit
   val tactic: string -> Proof.context -> method
   type src
   datatype text =
     Basic of (Proof.context -> method) |

   SELECT_GOAL (DEEPEN (2, the_default 20 opt_lim) (intprover_tac ctxt [] 0) 4 1);
 
 end;
 
 
-(* rule_tac etc. -- refer to dynamic goal state!! *)   (* FIXME cleanup!! *)
-
-fun bires_inst_tac bires_flag ctxt insts thm =
-  let
-    val thy = ProofContext.theory_of ctxt;
-    (* Separate type and term insts *)
-    fun has_type_var ((x, _), _) = (case Symbol.explode x of
-          "'"::cs => true | cs => false);
-    val Tinsts = List.filter has_type_var insts;
-    val tinsts = filter_out has_type_var insts;
-    (* Tactic *)
-    fun tac i st =
-      let
-        (* Preprocess state: extract environment information:
-           - variables and their types
-           - type variables and their sorts
-           - parameters and their types *)
-        val (types, sorts) = types_sorts st;
-    (* Process type insts: Tinsts_env *)
-    fun absent xi = error
-          ("No such variable in theorem: " ^ Syntax.string_of_vname xi);
-    val (rtypes, rsorts) = types_sorts thm;
-    fun readT (xi, s) =
-        let val S = case rsorts xi of SOME S => S | NONE => absent xi;
-            val T = Sign.read_typ (thy, sorts) s;
-            val U = TVar (xi, S);
-        in if Sign.typ_instance thy (T, U) then (U, T)
-           else error
-             ("Instantiation of " ^ Syntax.string_of_vname xi ^ " fails")
-        end;
-    val Tinsts_env = map readT Tinsts;
-    (* Preprocess rule: extract vars and their types, apply Tinsts *)
-    fun get_typ xi =
-      (case rtypes xi of
-           SOME T => typ_subst_atomic Tinsts_env T
-         | NONE => absent xi);
-    val (xis, ss) = Library.split_list tinsts;
-    val Ts = map get_typ xis;
-        val (_, _, Bi, _) = dest_state(st,i)
-        val params = Logic.strip_params Bi
-                             (* params of subgoal i as string typ pairs *)
-        val params = rev(Term.rename_wrt_term Bi params)
-                           (* as they are printed: bound variables with *)
-                           (* the same name are renamed during printing *)
-        fun types' (a, ~1) = (case AList.lookup (op =) params a of
-                NONE => types (a, ~1)
-              | some => some)
-          | types' xi = types xi;
-        fun internal x = is_some (types' (x, ~1));
-        val used = Drule.add_used thm (Drule.add_used st []);
-        val (ts, envT) =
-          ProofContext.read_termTs_schematic ctxt internal types' sorts used (ss ~~ Ts);
-        val envT' = map (fn (ixn, T) =>
-          (TVar (ixn, the (rsorts ixn)), T)) envT @ Tinsts_env;
-        val cenv =
-          map
-            (fn (xi, t) =>
-              pairself (Thm.cterm_of thy) (Var (xi, fastype_of t), t))
-            (distinct
-              (fn ((x1, t1), (x2, t2)) => x1 = x2 andalso t1 aconv t2)
-              (xis ~~ ts));
-        (* Lift and instantiate rule *)
-        val {maxidx, ...} = rep_thm st;
-        val paramTs = map #2 params
-        and inc = maxidx+1
-        fun liftvar (Var ((a,j), T)) =
-              Var((a, j+inc), paramTs ---> Logic.incr_tvar inc T)
-          | liftvar t = raise TERM("Variable expected", [t]);
-        fun liftterm t = list_abs_free
-              (params, Logic.incr_indexes(paramTs,inc) t)
-        fun liftpair (cv,ct) =
-              (cterm_fun liftvar cv, cterm_fun liftterm ct)
-        val lifttvar = pairself (ctyp_of thy o Logic.incr_tvar inc);
-        val rule = Drule.instantiate
-              (map lifttvar envT', map liftpair cenv)
-              (Thm.lift_rule (Thm.cprem_of st i) thm)
-      in
-        if i > nprems_of st then no_tac st
-        else st |>
-          compose_tac (bires_flag, rule, nprems_of thm) i
-      end
-           handle TERM (msg,_)   => (warning msg; no_tac st)
-                | THM  (msg,_,_) => (warning msg; no_tac st);
-  in tac end;
-
-local
-
-fun gen_inst _ tac _ (quant, ([], thms)) =
-      METHOD (fn facts => quant (insert_tac facts THEN' tac thms))
-  | gen_inst inst_tac _ ctxt (quant, (insts, [thm])) =
-      METHOD (fn facts =>
-        quant (insert_tac facts THEN' inst_tac ctxt insts thm))
-  | gen_inst _ _ _ _ = error "Cannot have instantiations with multiple rules";
-
-in
-
-val res_inst_meth = gen_inst (bires_inst_tac false) Tactic.resolve_tac;
-
-val eres_inst_meth = gen_inst (bires_inst_tac true) Tactic.eresolve_tac;
-
-val cut_inst_meth =
-  gen_inst
-    (fn ctxt => fn insts => bires_inst_tac false ctxt insts o Tactic.make_elim_preserve)
-    Tactic.cut_rules_tac;
-
-val dres_inst_meth =
-  gen_inst
-    (fn ctxt => fn insts => bires_inst_tac true ctxt insts o Tactic.make_elim_preserve)
-    Tactic.dresolve_tac;
-
-val forw_inst_meth =
-  gen_inst
-    (fn ctxt => fn insts => fn rule =>
-       bires_inst_tac false ctxt insts (Tactic.make_elim_preserve rule) THEN'
-       assume_tac)
-    Tactic.forward_tac;
-
-fun subgoal_tac ctxt sprop =
-  DETERM o bires_inst_tac false ctxt [(("psi", 0), sprop)] cut_rl;
-
-fun subgoals_tac ctxt sprops = EVERY' (map (subgoal_tac ctxt) sprops);
-
-fun thin_tac ctxt s =
-  bires_inst_tac true ctxt [(("V", 0), s)] thin_rl;
-
-end;
-
-
 (* ML tactics *)
 
 val tactic_ref = ref ((fn _ => raise Match): Proof.context -> thm list -> tactic);
 fun set_tactic f = tactic_ref := f;
 

 (* tactic syntax *)
 
 fun nat_thms_args f = uncurry f oo
   (#2 oo syntax (Scan.lift (Scan.optional (Args.parens Args.nat) 0) -- Attrib.thms));
 
-val insts =
-  Scan.optional
-    (Args.enum1 "and" (Scan.lift (Args.name -- (Args.$$$ "=" |-- Args.!!! Args.name))) --|
-      Scan.lift (Args.$$$ "in")) [] -- Attrib.thms;
-
-fun inst_args f src ctxt = f ctxt (#2 (syntax (Args.goal_spec HEADGOAL -- insts) src ctxt));
-
-val insts_var =
-  Scan.optional
-    (Args.enum1 "and" (Scan.lift (Args.var -- (Args.$$$ "=" |-- Args.!!! Args.name))) --|
-      Scan.lift (Args.$$$ "in")) [] -- Attrib.thms;
-
-fun inst_args_var f src ctxt =
-  f ctxt (#2 (syntax (Args.goal_spec HEADGOAL -- insts_var) src ctxt));
-
 fun goal_args' args tac src ctxt = #2 (syntax (Args.goal_spec HEADGOAL -- args >>
   (fn (quant, s) => SIMPLE_METHOD' quant (tac s))) src ctxt);
 
 fun goal_args args tac = goal_args' (Scan.lift args) tac;
 
 fun goal_args_ctxt' args tac src ctxt =
   #2 (syntax (Args.goal_spec HEADGOAL -- args >>
   (fn (quant, s) => SIMPLE_METHOD' quant (tac ctxt s))) src ctxt);
 
 fun goal_args_ctxt args tac = goal_args_ctxt' (Scan.lift args) tac;
-
-
-(* misc tactic emulations *)
-
-val subgoal_meth = goal_args_ctxt (Scan.repeat1 Args.name) subgoals_tac;
-val thin_meth = goal_args_ctxt Args.name thin_tac;
-val rename_meth = goal_args (Scan.repeat1 Args.name) Tactic.rename_params_tac;
-val rotate_meth = goal_args (Scan.optional Args.int 1) Tactic.rotate_tac;
 
 
 (* theory setup *)
 
 val _ = Context.add_setup (add_methods

   ("drule", nat_thms_args drule, "apply rule in destruct manner (improper)"),
   ("frule", nat_thms_args frule, "apply rule in forward manner (improper)"),
   ("this", no_args this, "apply current facts as rules"),
   ("fact", thms_ctxt_args fact, "composition by facts from context"),
   ("assumption", ctxt_args assumption, "proof by assumption, preferring facts"),
-  ("rule_tac", inst_args_var res_inst_meth, "apply rule (dynamic instantiation)"),
-  ("erule_tac", inst_args_var eres_inst_meth, "apply rule in elimination manner (dynamic instantiation)"),
-  ("drule_tac", inst_args_var dres_inst_meth, "apply rule in destruct manner (dynamic instantiation)"),
-  ("frule_tac", inst_args_var forw_inst_meth, "apply rule in forward manner (dynamic instantiation)"),
-  ("cut_tac", inst_args_var cut_inst_meth, "cut rule (dynamic instantiation)"),
-  ("subgoal_tac", subgoal_meth, "insert subgoal (dynamic instantiation)"),
-  ("thin_tac", thin_meth, "remove premise (dynamic instantiation)"),
-  ("rename_tac", rename_meth, "rename parameters of goal (dynamic instantiation)"),
-  ("rotate_tac", rotate_meth, "rotate assumptions of goal"),
+  ("rename_tac", goal_args (Scan.repeat1 Args.name) Tactic.rename_params_tac,
+    "rename parameters of goal (dynamic instantiation)"),
+  ("rotate_tac", goal_args (Scan.optional Args.int 1) Tactic.rotate_tac,
+    "rotate assumptions of goal"),
   ("tactic", simple_args Args.name tactic, "ML tactic as proof method")]);
 
 
 (*final declarations of this structure!*)
 val unfold = unfold_meth;