--- a/src/Pure/Isar/method.ML Thu Aug 03 17:30:42 2006 +0200
+++ b/src/Pure/Isar/method.ML Thu Aug 03 17:30:43 2006 +0200
@@ -50,8 +50,6 @@
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
@@ -337,134 +335,6 @@
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);
@@ -670,21 +540,6 @@
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);
@@ -697,14 +552,6 @@
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
@@ -726,15 +573,10 @@
("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")]);