--- a/src/CCL/Wfd.thy Fri Mar 13 23:32:40 2009 +0100
+++ b/src/CCL/Wfd.thy Fri Mar 13 23:50:05 2009 +0100
@@ -504,8 +504,9 @@
val eval_setup =
Data.setup #>
- Method.add_methods [("eval", Method.thms_ctxt_args (fn ths => fn ctxt =>
- SIMPLE_METHOD (CHANGED (eval_tac ctxt ths))), "evaluation")];
+ Method.setup @{binding eval}
+ (Attrib.thms >> (fn ths => fn ctxt => SIMPLE_METHOD (CHANGED (eval_tac ctxt ths))))
+ "evaluation";
end;
--- a/src/HOL/Algebra/ringsimp.ML Fri Mar 13 23:32:40 2009 +0100
+++ b/src/HOL/Algebra/ringsimp.ML Fri Mar 13 23:50:05 2009 +0100
@@ -72,8 +72,8 @@
(** Setup **)
val setup =
- Method.add_methods [("algebra", Method.ctxt_args (SIMPLE_METHOD' o algebra_tac),
- "normalisation of algebraic structure")] #>
+ Method.setup @{binding algebra} (Scan.succeed (SIMPLE_METHOD' o algebra_tac))
+ "normalisation of algebraic structure" #>
Attrib.add_attributes [("algebra", attribute, "theorems controlling algebra method")];
end;
--- a/src/HOL/Orderings.thy Fri Mar 13 23:32:40 2009 +0100
+++ b/src/HOL/Orderings.thy Fri Mar 13 23:50:05 2009 +0100
@@ -397,8 +397,7 @@
(** Setup **)
val setup =
- Method.add_methods
- [("order", Method.ctxt_args (SIMPLE_METHOD' o order_tac []), "transitivity reasoner")] #>
+ Method.setup @{binding order} (Scan.succeed (SIMPLE_METHOD' o order_tac [])) "transitivity reasoner" #>
Attrib.add_attributes [("order", attribute, "theorems controlling transitivity reasoner")];
end;
--- a/src/HOL/Tools/function_package/auto_term.ML Fri Mar 13 23:32:40 2009 +0100
+++ b/src/HOL/Tools/function_package/auto_term.ML Fri Mar 13 23:50:05 2009 +0100
@@ -29,8 +29,9 @@
TRY (FundefCommon.apply_termination_rule ctxt i)
THEN PRIMITIVE (inst_thm ctxt rel)
-val setup = Method.add_methods
- [("relation", (SIMPLE_METHOD' o (fn (rel, ctxt) => relation_tac ctxt rel)) oo (Method.syntax Args.term),
- "proves termination using a user-specified wellfounded relation")]
+val setup =
+ Method.setup @{binding relation}
+ (Args.term >> (fn rel => fn ctxt => SIMPLE_METHOD' (relation_tac ctxt rel)))
+ "proves termination using a user-specified wellfounded relation"
end
--- a/src/HOL/Tools/function_package/fundef_datatype.ML Fri Mar 13 23:32:40 2009 +0100
+++ b/src/HOL/Tools/function_package/fundef_datatype.ML Fri Mar 13 23:50:05 2009 +0100
@@ -300,8 +300,8 @@
end
val setup =
- Method.add_methods [("pat_completeness", Method.ctxt_args pat_completeness,
- "Completeness prover for datatype patterns")]
+ Method.setup @{binding pat_completeness} (Scan.succeed pat_completeness)
+ "Completeness prover for datatype patterns"
#> Context.theory_map (FundefCommon.set_preproc sequential_preproc)
--- a/src/HOL/Tools/function_package/induction_scheme.ML Fri Mar 13 23:32:40 2009 +0100
+++ b/src/HOL/Tools/function_package/induction_scheme.ML Fri Mar 13 23:50:05 2009 +0100
@@ -398,8 +398,8 @@
fun induct_scheme_tac ctxt =
mk_ind_tac (K all_tac) (assume_tac APPEND' Goal.assume_rule_tac ctxt) (K all_tac) ctxt;
-val setup = Method.add_methods
- [("induct_scheme", Method.ctxt_args (RAW_METHOD o induct_scheme_tac),
- "proves an induction principle")]
+val setup =
+ Method.setup @{binding induct_scheme} (Scan.succeed (RAW_METHOD o induct_scheme_tac))
+ "proves an induction principle"
end
--- a/src/HOL/Tools/inductive_package.ML Fri Mar 13 23:32:40 2009 +0100
+++ b/src/HOL/Tools/inductive_package.ML Fri Mar 13 23:50:05 2009 +0100
@@ -460,9 +460,10 @@
val inductive_cases_i = gen_inductive_cases (K I) Syntax.check_prop;
-fun ind_cases src = Method.syntax (Scan.lift (Scan.repeat1 Args.name_source --
- Scan.optional (Args.$$$ "for" |-- Scan.repeat1 Args.name) [])) src
- #> (fn ((raw_props, fixes), ctxt) =>
+val ind_cases =
+ Scan.lift (Scan.repeat1 Args.name_source --
+ Scan.optional (Args.$$$ "for" |-- Scan.repeat1 Args.name) []) >>
+ (fn (raw_props, fixes) => fn ctxt =>
let
val (_, ctxt') = Variable.add_fixes fixes ctxt;
val props = Syntax.read_props ctxt' raw_props;
@@ -933,8 +934,7 @@
(* setup theory *)
val setup =
- Method.add_methods [("ind_cases", ind_cases,
- "dynamic case analysis on predicates")] #>
+ Method.setup @{binding ind_cases} ind_cases "dynamic case analysis on predicates" #>
Attrib.add_attributes [("mono", Attrib.add_del_args mono_add mono_del,
"declaration of monotonicity rule")];
--- a/src/HOL/Tools/lin_arith.ML Fri Mar 13 23:32:40 2009 +0100
+++ b/src/HOL/Tools/lin_arith.ML Fri Mar 13 23:50:05 2009 +0100
@@ -912,9 +912,8 @@
ObjectLogic.full_atomize_tac THEN' (REPEAT_DETERM o rtac impI) THEN' raw_arith_tac ctxt false,
more_arith_tacs ctxt];
-fun arith_method src =
- Method.syntax Args.bang_facts src
- #> (fn (prems, ctxt) => METHOD (fn facts =>
+val arith_method = Args.bang_facts >>
+ (fn prems => fn ctxt => METHOD (fn facts =>
HEADGOAL (Method.insert_tac (prems @ ArithFacts.get ctxt @ facts)
THEN' arith_tac ctxt)));
@@ -930,8 +929,7 @@
(add_arith_facts #> Fast_Arith.cut_lin_arith_tac))) #>
Context.mapping
(setup_options #>
- Method.add_methods
- [("arith", arith_method, "decide linear arithmetic")] #>
+ Method.setup @{binding arith} arith_method "decide linear arithmetic" #>
Attrib.add_attributes [("arith_split", Attrib.no_args arith_split_add,
"declaration of split rules for arithmetic procedure")]) I;
--- a/src/HOL/Tools/metis_tools.ML Fri Mar 13 23:32:40 2009 +0100
+++ b/src/HOL/Tools/metis_tools.ML Fri Mar 13 23:50:05 2009 +0100
@@ -637,17 +637,16 @@
val metisF_tac = metis_general_tac ResAtp.Fol;
val metisH_tac = metis_general_tac ResAtp.Hol;
- fun method mode = Method.thms_ctxt_args (fn ths => fn ctxt =>
- SIMPLE_METHOD' (CHANGED_PROP o metis_general_tac mode ctxt ths));
+ fun method name mode comment = Method.setup name (Attrib.thms >> (fn ths => fn ctxt =>
+ SIMPLE_METHOD' (CHANGED_PROP o metis_general_tac mode ctxt ths))) comment;
val setup =
type_lits_setup #>
- Method.add_methods
- [("metis", method ResAtp.Auto, "METIS for FOL & HOL problems"),
- ("metisF", method ResAtp.Fol, "METIS for FOL problems"),
- ("metisH", method ResAtp.Hol, "METIS for HOL problems"),
- ("finish_clausify",
- Method.no_args (SIMPLE_METHOD' (K (ResAxioms.expand_defs_tac refl))),
- "cleanup after conversion to clauses")];
+ method @{binding metis} ResAtp.Auto "METIS for FOL & HOL problems" #>
+ method @{binding metisF} ResAtp.Fol "METIS for FOL problems" #>
+ method @{binding metisH} ResAtp.Hol "METIS for HOL problems" #>
+ Method.setup @{binding finish_clausify}
+ (Scan.succeed (K (SIMPLE_METHOD (ResAxioms.expand_defs_tac refl))))
+ "cleanup after conversion to clauses";
end;
--- a/src/HOL/Tools/res_axioms.ML Fri Mar 13 23:32:40 2009 +0100
+++ b/src/HOL/Tools/res_axioms.ML Fri Mar 13 23:50:05 2009 +0100
@@ -487,10 +487,10 @@
val thy = Thm.theory_of_thm st0
in (Meson.meson_claset_tac (maps (cnf_axiom thy) ths) HOL_cs i THEN expand_defs_tac st0) st0 end;
-val meson_method_setup = Method.add_methods
- [("meson", Method.thms_args (fn ths =>
- SIMPLE_METHOD' (CHANGED_PROP o meson_general_tac ths)),
- "MESON resolution proof procedure")];
+val meson_method_setup =
+ Method.setup @{binding meson} (Attrib.thms >> (fn ths => fn _ =>
+ SIMPLE_METHOD' (CHANGED_PROP o meson_general_tac ths)))
+ "MESON resolution proof procedure";
(*** Converting a subgoal into negated conjecture clauses. ***)
@@ -521,9 +521,9 @@
REPEAT_DETERM_N (length ts) o (etac thin_rl)]
end);
-val setup_methods = Method.add_methods
- [("neg_clausify", Method.no_args (SIMPLE_METHOD' neg_clausify_tac),
- "conversion of goal to conjecture clauses")];
+val setup_methods =
+ Method.setup @{binding neg_clausify} (Scan.succeed (K (SIMPLE_METHOD' neg_clausify_tac)))
+ "conversion of goal to conjecture clauses";
(** Attribute for converting a theorem into clauses **)
--- a/src/Provers/hypsubst.ML Fri Mar 13 23:32:40 2009 +0100
+++ b/src/Provers/hypsubst.ML Fri Mar 13 23:50:05 2009 +0100
@@ -284,9 +284,10 @@
(* theory setup *)
val hypsubst_setup =
- Method.add_methods
- [("hypsubst", Method.no_args (SIMPLE_METHOD' (CHANGED_PROP o hyp_subst_tac)),
- "substitution using an assumption (improper)"),
- ("simplesubst", Method.thm_args (SIMPLE_METHOD' o stac), "simple substitution")];
+ Method.setup @{binding hypsubst}
+ (Scan.succeed (K (SIMPLE_METHOD' (CHANGED_PROP o hyp_subst_tac))))
+ "substitution using an assumption (improper)" #>
+ Method.setup @{binding simplesubst} (Attrib.thm >> (fn th => K (SIMPLE_METHOD' (stac th))))
+ "simple substitution";
end;
--- a/src/Provers/splitter.ML Fri Mar 13 23:32:40 2009 +0100
+++ b/src/Provers/splitter.ML Fri Mar 13 23:50:05 2009 +0100
@@ -472,16 +472,15 @@
Args.$$$ splitN -- Args.add -- Args.colon >> K (I, split_add),
Args.$$$ splitN -- Args.del -- Args.colon >> K (I, split_del)];
-fun split_meth src =
- Method.syntax Attrib.thms src
- #> (fn (ths, _) => SIMPLE_METHOD' (CHANGED_PROP o gen_split_tac ths));
+val split_meth = Attrib.thms >>
+ (fn ths => K (SIMPLE_METHOD' (CHANGED_PROP o gen_split_tac ths)));
(* theory setup *)
val setup =
- (Attrib.add_attributes
- [(splitN, Attrib.add_del_args split_add split_del, "declaration of case split rule")] #>
- Method.add_methods [(splitN, split_meth, "apply case split rule")]);
+ Attrib.add_attributes
+ [(splitN, Attrib.add_del_args split_add split_del, "declaration of case split rule")] #>
+ Method.setup @{binding split} split_meth "apply case split rule";
end;
--- a/src/Pure/Isar/class_target.ML Fri Mar 13 23:32:40 2009 +0100
+++ b/src/Pure/Isar/class_target.ML Fri Mar 13 23:50:05 2009 +0100
@@ -615,11 +615,10 @@
default_intro_tac ctxt facts;
val _ = Context.>> (Context.map_theory
- (Method.add_methods
- [("intro_classes", Method.no_args (METHOD intro_classes_tac),
- "back-chain introduction rules of classes"),
- ("default", Method.thms_ctxt_args (METHOD oo default_tac),
- "apply some intro/elim rule")]));
+ (Method.setup (Binding.name "intro_classes") (Scan.succeed (K (METHOD intro_classes_tac)))
+ "back-chain introduction rules of classes" #>
+ Method.setup (Binding.name "default") (Attrib.thms >> (METHOD oo default_tac))
+ "apply some intro/elim rule"));
end;
--- a/src/Pure/Isar/locale.ML Fri Mar 13 23:32:40 2009 +0100
+++ b/src/Pure/Isar/locale.ML Fri Mar 13 23:50:05 2009 +0100
@@ -487,13 +487,10 @@
(Witnesses.get ctxt @ Intros.get ctxt @ (if eager then Unfolds.get ctxt else [])) facts st;
val _ = Context.>> (Context.map_theory
- (Method.add_methods
- [("intro_locales",
- Method.ctxt_args (fn ctxt => METHOD (intro_locales_tac false ctxt)),
- "back-chain introduction rules of locales without unfolding predicates"),
- ("unfold_locales",
- Method.ctxt_args (fn ctxt => METHOD (intro_locales_tac true ctxt)),
- "back-chain all introduction rules of locales")]));
+ (Method.setup (Binding.name "intro_locales") (Scan.succeed (METHOD o intro_locales_tac false))
+ "back-chain introduction rules of locales without unfolding predicates" #>
+ Method.setup (Binding.name "unfold_locales") (Scan.succeed (METHOD o intro_locales_tac true))
+ "back-chain all introduction rules of locales"));
end;
--- a/src/Pure/Isar/method.ML Fri Mar 13 23:32:40 2009 +0100
+++ b/src/Pure/Isar/method.ML Fri Mar 13 23:50:05 2009 +0100
@@ -456,18 +456,22 @@
end;
+(* extra rule methods *)
+
+fun xrule_meth m =
+ Scan.lift (Scan.optional (Args.parens OuterParse.nat) 0) -- Attrib.thms >>
+ (fn (n, ths) => K (m n ths));
+
+
(* tactic syntax *)
-fun nat_thms_args f = uncurry f oo
- (fst oo syntax (Scan.lift (Scan.optional (Args.parens P.nat) 0) -- Attrib.thms));
-
-fun goal_args' args tac src ctxt = fst (syntax (Args.goal_spec HEADGOAL -- args >>
+fun goal_args' args tac src ctxt = fst (syntax (Args.goal_spec -- 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 =
- fst (syntax (Args.goal_spec HEADGOAL -- args >>
+ fst (syntax (Args.goal_spec -- 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;
@@ -500,31 +504,38 @@
(* theory setup *)
val _ = Context.>> (Context.map_theory
- (add_methods
- [("fail", no_args fail, "force failure"),
- ("succeed", no_args succeed, "succeed"),
- ("-", no_args insert_facts, "do nothing (insert current facts only)"),
- ("insert", thms_args insert, "insert theorems, ignoring facts (improper)"),
- ("intro", thms_args intro, "repeatedly apply introduction rules"),
- ("elim", thms_args elim, "repeatedly apply elimination rules"),
- ("unfold", thms_ctxt_args unfold_meth, "unfold definitions"),
- ("fold", thms_ctxt_args fold_meth, "fold definitions"),
- ("atomize", (atomize o fst) oo syntax (Args.mode "full"),
- "present local premises as object-level statements"),
- ("rule", thms_ctxt_args some_rule, "apply some intro/elim rule"),
- ("erule", nat_thms_args erule, "apply rule in elimination manner (improper)"),
- ("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"),
- ("rename_tac", goal_args (Scan.repeat1 Args.name) Tactic.rename_tac,
- "rename parameters of goal"),
- ("rotate_tac", goal_args (Scan.optional P.int 1) Tactic.rotate_tac,
- "rotate assumptions of goal"),
- ("tactic", simple_args (P.position Args.name) tactic, "ML tactic as proof method"),
- ("raw_tactic", simple_args (P.position Args.name) raw_tactic,
- "ML tactic as raw proof method")]));
+ (setup (Binding.name "fail") (Scan.succeed (K fail)) "force failure" #>
+ setup (Binding.name "succeed") (Scan.succeed (K succeed)) "succeed" #>
+ setup (Binding.name "-") (Scan.succeed (K insert_facts))
+ "do nothing (insert current facts only)" #>
+ setup (Binding.name "insert") (Attrib.thms >> (K o insert))
+ "insert theorems, ignoring facts (improper)" #>
+ setup (Binding.name "intro") (Attrib.thms >> (K o intro))
+ "repeatedly apply introduction rules" #>
+ setup (Binding.name "elim") (Attrib.thms >> (K o elim))
+ "repeatedly apply elimination rules" #>
+ setup (Binding.name "unfold") (Attrib.thms >> unfold_meth) "unfold definitions" #>
+ setup (Binding.name "fold") (Attrib.thms >> fold_meth) "fold definitions" #>
+ setup (Binding.name "atomize") (Args.mode "full" >> (K o atomize))
+ "present local premises as object-level statements" #>
+ setup (Binding.name "rule") (Attrib.thms >> some_rule) "apply some intro/elim rule" #>
+ setup (Binding.name "erule") (xrule_meth erule) "apply rule in elimination manner (improper)" #>
+ setup (Binding.name "drule") (xrule_meth drule) "apply rule in destruct manner (improper)" #>
+ setup (Binding.name "frule") (xrule_meth frule) "apply rule in forward manner (improper)" #>
+ setup (Binding.name "this") (Scan.succeed (K this)) "apply current facts as rules" #>
+ setup (Binding.name "fact") (Attrib.thms >> fact) "composition by facts from context" #>
+ setup (Binding.name "assumption") (Scan.succeed assumption)
+ "proof by assumption, preferring facts" #>
+ setup (Binding.name "rename_tac") (Args.goal_spec -- Scan.lift (Scan.repeat1 Args.name) >>
+ (fn (quant, xs) => K (SIMPLE_METHOD'' quant (Tactic.rename_tac xs))))
+ "rename parameters of goal" #>
+ setup (Binding.name "rotate_tac") (Args.goal_spec -- Scan.lift (Scan.optional P.int 1) >>
+ (fn (quant, i) => K (SIMPLE_METHOD'' quant (Tactic.rotate_tac i))))
+ "rotate assumptions of goal" #>
+ setup (Binding.name "tactic") (Scan.lift (P.position Args.name) >> tactic)
+ "ML tactic as proof method" #>
+ setup (Binding.name "raw_tactic") (Scan.lift (P.position Args.name) >> raw_tactic)
+ "ML tactic as raw proof method"));
(*final declarations of this structure!*)
--- a/src/Pure/Isar/rule_insts.ML Fri Mar 13 23:32:40 2009 +0100
+++ b/src/Pure/Isar/rule_insts.ML Fri Mar 13 23:50:05 2009 +0100
@@ -386,61 +386,48 @@
local
-fun gen_inst _ tac _ (quant, ([], thms)) =
- METHOD (fn facts => quant (Method.insert_tac facts THEN' tac thms))
- | gen_inst inst_tac _ ctxt (quant, (insts, [thm])) =
- METHOD (fn facts =>
- quant (Method.insert_tac facts THEN' inst_tac ctxt insts thm))
- | gen_inst _ _ _ _ = error "Cannot have instantiations with multiple rules";
+fun inst_meth inst_tac tac =
+ Args.goal_spec --
+ Scan.optional (Scan.lift
+ (P.and_list1 (Args.var -- (Args.$$$ "=" |-- P.!!! Args.name_source)) --| Args.$$$ "in")) [] --
+ Attrib.thms >>
+ (fn ((quant, insts), thms) => fn ctxt => METHOD (fn facts =>
+ if null insts then quant (Method.insert_tac facts THEN' tac thms)
+ else
+ (case thms of
+ [thm] => quant (Method.insert_tac facts THEN' inst_tac ctxt insts thm)
+ | _ => error "Cannot have instantiations with multiple rules")));
in
-val res_inst_meth = gen_inst res_inst_tac Tactic.resolve_tac;
-val eres_inst_meth = gen_inst eres_inst_tac Tactic.eresolve_tac;
-val cut_inst_meth = gen_inst cut_inst_tac Tactic.cut_rules_tac;
-val dres_inst_meth = gen_inst dres_inst_tac Tactic.dresolve_tac;
-val forw_inst_meth = gen_inst forw_inst_tac Tactic.forward_tac;
+val res_inst_meth = inst_meth res_inst_tac Tactic.resolve_tac;
+val eres_inst_meth = inst_meth eres_inst_tac Tactic.eresolve_tac;
+val cut_inst_meth = inst_meth cut_inst_tac Tactic.cut_rules_tac;
+val dres_inst_meth = inst_meth dres_inst_tac Tactic.dresolve_tac;
+val forw_inst_meth = inst_meth forw_inst_tac Tactic.forward_tac;
end;
-(* method syntax *)
-
-val insts =
- Scan.optional (Scan.lift
- (P.and_list1 (Args.name -- (Args.$$$ "=" |-- P.!!! Args.name_source)) --| Args.$$$ "in")) []
- -- Attrib.thms;
-
-fun inst_args f src ctxt =
- f ctxt (fst (Method.syntax (Args.goal_spec HEADGOAL -- insts) src ctxt));
-
-val insts_var =
- Scan.optional (Scan.lift
- (P.and_list1 (Args.var -- (Args.$$$ "=" |-- P.!!! Args.name_source)) --| Args.$$$ "in")) []
- -- Attrib.thms;
-
-fun inst_args_var f src ctxt =
- f ctxt (fst (Method.syntax (Args.goal_spec HEADGOAL -- insts_var) src ctxt));
-
-
(* setup *)
val _ = Context.>> (Context.map_theory
- (Method.add_methods
- [("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", Method.goal_args_ctxt (Scan.repeat1 Args.name_source) subgoals_tac,
- "insert subgoal (dynamic instantiation)"),
- ("thin_tac", Method.goal_args_ctxt Args.name_source thin_tac,
- "remove premise (dynamic instantiation)")]));
+ (Method.setup (Binding.name "rule_tac") res_inst_meth "apply rule (dynamic instantiation)" #>
+ Method.setup (Binding.name "erule_tac") eres_inst_meth
+ "apply rule in elimination manner (dynamic instantiation)" #>
+ Method.setup (Binding.name "drule_tac") dres_inst_meth
+ "apply rule in destruct manner (dynamic instantiation)" #>
+ Method.setup (Binding.name "frule_tac") forw_inst_meth
+ "apply rule in forward manner (dynamic instantiation)" #>
+ Method.setup (Binding.name "cut_tac") cut_inst_meth "cut rule (dynamic instantiation)" #>
+ Method.setup (Binding.name "subgoal_tac")
+ (Args.goal_spec -- Scan.lift (Scan.repeat1 Args.name_source) >>
+ (fn (quant, props) => fn ctxt => SIMPLE_METHOD'' quant (subgoals_tac ctxt props)))
+ "insert subgoal (dynamic instantiation)" #>
+ Method.setup (Binding.name "thin_tac")
+ (Args.goal_spec -- Scan.lift Args.name_source >>
+ (fn (quant, prop) => fn ctxt => SIMPLE_METHOD'' quant (thin_tac ctxt prop)))
+ "remove premise (dynamic instantiation)"));
end;
--- a/src/Tools/atomize_elim.ML Fri Mar 13 23:32:40 2009 +0100
+++ b/src/Tools/atomize_elim.ML Fri Mar 13 23:50:05 2009 +0100
@@ -131,9 +131,9 @@
THEN (CONVERSION (full_atomize_elim_conv ctxt) i)
end)
-val setup = Method.add_methods
- [("atomize_elim", Method.ctxt_args (SIMPLE_METHOD' o atomize_elim_tac),
- "convert obtains statement to atomic object logic goal")]
+val setup =
+ Method.setup @{binding atomize_elim} (Scan.succeed (SIMPLE_METHOD' o atomize_elim_tac))
+ "convert obtains statement to atomic object logic goal"
#> AtomizeElimData.setup
end
--- a/src/Tools/induct.ML Fri Mar 13 23:32:40 2009 +0100
+++ b/src/Tools/induct.ML Fri Mar 13 23:50:05 2009 +0100
@@ -735,22 +735,21 @@
in
-fun cases_meth src =
- Method.syntax (P.and_list' (Scan.repeat (unless_more_args inst)) -- Scan.option cases_rule) src
- #> (fn ((insts, opt_rule), ctxt) =>
- METHOD_CASES (fn facts =>
- Seq.DETERM (HEADGOAL (cases_tac ctxt insts opt_rule facts))));
+val cases_meth =
+ P.and_list' (Scan.repeat (unless_more_args inst)) -- Scan.option cases_rule >>
+ (fn (insts, opt_rule) => fn ctxt =>
+ METHOD_CASES (fn facts => Seq.DETERM (HEADGOAL (cases_tac ctxt insts opt_rule facts))));
-fun induct_meth src =
- Method.syntax (P.and_list' (Scan.repeat (unless_more_args def_inst)) --
- (arbitrary -- taking -- Scan.option induct_rule)) src
- #> (fn ((insts, ((arbitrary, taking), opt_rule)), ctxt) =>
+val induct_meth =
+ P.and_list' (Scan.repeat (unless_more_args def_inst)) --
+ (arbitrary -- taking -- Scan.option induct_rule) >>
+ (fn (insts, ((arbitrary, taking), opt_rule)) => fn ctxt =>
RAW_METHOD_CASES (fn facts =>
Seq.DETERM (HEADGOAL (induct_tac ctxt insts arbitrary taking opt_rule facts))));
-fun coinduct_meth src =
- Method.syntax (Scan.repeat (unless_more_args inst) -- taking -- Scan.option coinduct_rule) src
- #> (fn (((insts, taking), opt_rule), ctxt) =>
+val coinduct_meth =
+ Scan.repeat (unless_more_args inst) -- taking -- Scan.option coinduct_rule >>
+ (fn ((insts, taking), opt_rule) => fn ctxt =>
RAW_METHOD_CASES (fn facts =>
Seq.DETERM (HEADGOAL (coinduct_tac ctxt insts taking opt_rule facts))));
@@ -762,9 +761,8 @@
val setup =
attrib_setup #>
- Method.add_methods
- [(casesN, cases_meth, "case analysis on types or predicates/sets"),
- (inductN, induct_meth, "induction on types or predicates/sets"),
- (coinductN, coinduct_meth, "coinduction on types or predicates/sets")];
+ Method.setup @{binding cases} cases_meth "case analysis on types or predicates/sets" #>
+ Method.setup @{binding induct} induct_meth "induction on types or predicates/sets" #>
+ Method.setup @{binding coinduct} coinduct_meth "coinduction on types or predicates/sets";
end;
--- a/src/ZF/Tools/ind_cases.ML Fri Mar 13 23:32:40 2009 +0100
+++ b/src/ZF/Tools/ind_cases.ML Fri Mar 13 23:50:05 2009 +0100
@@ -57,19 +57,14 @@
(* ind_cases method *)
-fun mk_cases_meth (props, ctxt) =
- props
- |> map (smart_cases (ProofContext.theory_of ctxt) (local_simpset_of ctxt) (Syntax.read_prop ctxt))
- |> Method.erule 0;
-
-val mk_cases_args = Method.syntax (Scan.lift (Scan.repeat1 Args.name_source));
-
-
-(* package setup *)
+val mk_cases_meth = Scan.lift (Scan.repeat1 Args.name_source) >>
+ (fn props => fn ctxt =>
+ props
+ |> map (smart_cases (ProofContext.theory_of ctxt) (local_simpset_of ctxt) (Syntax.read_prop ctxt))
+ |> Method.erule 0);
val setup =
- Method.add_methods
- [("ind_cases", mk_cases_meth oo mk_cases_args, "dynamic case analysis on sets")];
+ Method.setup @{binding "ind_cases"} mk_cases_meth "dynamic case analysis on sets";
(* outer syntax *)