--- a/src/HOL/Tools/function_package/lexicographic_order.ML Sun Mar 15 20:19:14 2009 +0100
+++ b/src/HOL/Tools/function_package/lexicographic_order.ML Sun Mar 15 20:25:58 2009 +0100
@@ -220,9 +220,11 @@
val lexicographic_order = SIMPLE_METHOD o lexicographic_order_tac
-val setup = Method.add_methods [("lexicographic_order", Method.only_sectioned_args clasimp_modifiers lexicographic_order,
- "termination prover for lexicographic orderings")]
- #> Context.theory_map (FundefCommon.set_termination_prover lexicographic_order)
+val setup =
+ Method.setup @{binding lexicographic_order}
+ (Method.sections clasimp_modifiers >> (K lexicographic_order))
+ "termination prover for lexicographic orderings"
+ #> Context.theory_map (FundefCommon.set_termination_prover lexicographic_order)
end;
--- a/src/Provers/blast.ML Sun Mar 15 20:19:14 2009 +0100
+++ b/src/Provers/blast.ML Sun Mar 15 20:25:58 2009 +0100
@@ -1306,12 +1306,13 @@
(** method setup **)
val blast_method =
- Method.bang_sectioned_args' Data.cla_modifiers (Scan.lift (Scan.option OuterParse.nat))
- (fn NONE => Data.cla_meth' blast_tac
- | SOME lim => Data.cla_meth' (fn cs => depth_tac cs lim));
+ Args.bang_facts -- Scan.lift (Scan.option OuterParse.nat) --|
+ Method.sections Data.cla_modifiers >>
+ (fn (prems, NONE) => Data.cla_meth' blast_tac prems
+ | (prems, SOME lim) => Data.cla_meth' (fn cs => depth_tac cs lim) prems);
val setup =
setup_depth_limit #>
- Method.add_methods [("blast", blast_method, "tableau prover")];
+ Method.setup @{binding blast} blast_method "tableau prover";
end;
--- a/src/Provers/clasimp.ML Sun Mar 15 20:19:14 2009 +0100
+++ b/src/Provers/clasimp.ML Sun Mar 15 20:25:58 2009 +0100
@@ -296,28 +296,30 @@
fun clasimp_meth' tac prems ctxt = METHOD (fn facts =>
HEADGOAL (Method.insert_tac (prems @ facts) THEN' tac (local_clasimpset_of ctxt)));
-val clasimp_method = Method.bang_sectioned_args clasimp_modifiers o clasimp_meth;
-val clasimp_method' = Method.bang_sectioned_args clasimp_modifiers o clasimp_meth';
+fun clasimp_method tac =
+ Args.bang_facts --| Method.sections clasimp_modifiers >> (clasimp_meth tac);
-fun auto_args m =
- Method.bang_sectioned_args' clasimp_modifiers
- (Scan.lift (Scan.option (OuterParse.nat -- OuterParse.nat))) m;
+fun clasimp_method' tac =
+ Args.bang_facts --| Method.sections clasimp_modifiers >> (clasimp_meth' tac);
-fun auto_meth NONE = clasimp_meth (CHANGED_PROP o auto_tac)
- | auto_meth (SOME (m, n)) = clasimp_meth (CHANGED_PROP o (fn css => mk_auto_tac css m n));
+val auto_method =
+ Args.bang_facts -- Scan.lift (Scan.option (OuterParse.nat -- OuterParse.nat)) --|
+ Method.sections clasimp_modifiers >>
+ (fn (prems, NONE) => clasimp_meth (CHANGED_PROP o auto_tac) prems
+ | (prems, SOME (m, n)) => clasimp_meth (CHANGED_PROP o (fn css => mk_auto_tac css m n)) prems);
(* theory setup *)
val clasimp_setup =
- (Attrib.setup @{binding iff} iff_att "declaration of Simplifier / Classical rules" #>
- Method.add_methods
- [("fastsimp", clasimp_method' fast_simp_tac, "combined fast and simp"),
- ("slowsimp", clasimp_method' slow_simp_tac, "combined slow and simp"),
- ("bestsimp", clasimp_method' best_simp_tac, "combined best and simp"),
- ("force", clasimp_method' force_tac, "force"),
- ("auto", auto_args auto_meth, "auto"),
- ("clarsimp", clasimp_method' (CHANGED_PROP oo clarsimp_tac), "clarify simplified goal")]);
+ Attrib.setup @{binding iff} iff_att "declaration of Simplifier / Classical rules" #>
+ Method.setup @{binding fastsimp} (clasimp_method' fast_simp_tac) "combined fast and simp" #>
+ Method.setup @{binding slowsimp} (clasimp_method' slow_simp_tac) "combined slow and simp" #>
+ Method.setup @{binding bestsimp} (clasimp_method' best_simp_tac) "combined best and simp" #>
+ Method.setup @{binding force} (clasimp_method' force_tac) "force" #>
+ Method.setup @{binding auto} auto_method "auto" #>
+ Method.setup @{binding clarsimp} (clasimp_method' (CHANGED_PROP oo clarsimp_tac))
+ "clarify simplified goal";
end;
--- a/src/Provers/classical.ML Sun Mar 15 20:19:14 2009 +0100
+++ b/src/Provers/classical.ML Sun Mar 15 20:25:58 2009 +0100
@@ -149,8 +149,8 @@
val cla_modifiers: Method.modifier parser list
val cla_meth: (claset -> tactic) -> thm list -> Proof.context -> Proof.method
val cla_meth': (claset -> int -> tactic) -> thm list -> Proof.context -> Proof.method
- val cla_method: (claset -> tactic) -> Method.src -> Proof.context -> Proof.method
- val cla_method': (claset -> int -> tactic) -> Method.src -> Proof.context -> Proof.method
+ val cla_method: (claset -> tactic) -> (Proof.context -> Proof.method) context_parser
+ val cla_method': (claset -> int -> tactic) -> (Proof.context -> Proof.method) context_parser
val setup: theory -> theory
end;
@@ -1025,23 +1025,29 @@
fun cla_meth' tac prems ctxt = METHOD (fn facts =>
HEADGOAL (Method.insert_tac (prems @ facts) THEN' tac (local_claset_of ctxt)));
-val cla_method = Method.bang_sectioned_args cla_modifiers o cla_meth;
-val cla_method' = Method.bang_sectioned_args cla_modifiers o cla_meth';
+fun cla_method tac = Args.bang_facts --| Method.sections cla_modifiers >> (cla_meth tac);
+fun cla_method' tac = Args.bang_facts --| Method.sections cla_modifiers >> (cla_meth' tac);
(** setup_methods **)
-val setup_methods = Method.add_methods
- [("default", Method.thms_ctxt_args default, "apply some intro/elim rule (potentially classical)"),
- ("rule", Method.thms_ctxt_args rule, "apply some intro/elim rule (potentially classical)"),
- ("contradiction", Method.no_args contradiction, "proof by contradiction"),
- ("clarify", cla_method' (CHANGED_PROP oo clarify_tac), "repeatedly apply safe steps"),
- ("fast", cla_method' fast_tac, "classical prover (depth-first)"),
- ("slow", cla_method' slow_tac, "classical prover (slow depth-first)"),
- ("best", cla_method' best_tac, "classical prover (best-first)"),
- ("deepen", cla_method' (fn cs => deepen_tac cs 4), "classical prover (iterative deepening)"),
- ("safe", cla_method (CHANGED_PROP o safe_tac), "classical prover (apply safe rules)")];
+val setup_methods =
+ Method.setup @{binding default} (Attrib.thms >> default)
+ "apply some intro/elim rule (potentially classical)" #>
+ Method.setup @{binding rule} (Attrib.thms >> rule)
+ "apply some intro/elim rule (potentially classical)" #>
+ Method.setup @{binding contradiction} (Scan.succeed (K contradiction))
+ "proof by contradiction" #>
+ Method.setup @{binding clarify} (cla_method' (CHANGED_PROP oo clarify_tac))
+ "repeatedly apply safe steps" #>
+ Method.setup @{binding fast} (cla_method' fast_tac) "classical prover (depth-first)" #>
+ Method.setup @{binding slow} (cla_method' slow_tac) "classical prover (slow depth-first)" #>
+ Method.setup @{binding best} (cla_method' best_tac) "classical prover (best-first)" #>
+ Method.setup @{binding deepen} (cla_method' (fn cs => deepen_tac cs 4))
+ "classical prover (iterative deepening)" #>
+ Method.setup @{binding safe} (cla_method (CHANGED_PROP o safe_tac))
+ "classical prover (apply safe rules)";
--- a/src/Tools/induct_tacs.ML Sun Mar 15 20:19:14 2009 +0100
+++ b/src/Tools/induct_tacs.ML Sun Mar 15 20:25:58 2009 +0100
@@ -26,7 +26,7 @@
error ("Cannot determine type of " ^ Syntax.string_of_term ctxt u);
in (u, U) end;
-fun gen_case_tac ctxt0 (s, opt_rule) i st =
+fun gen_case_tac ctxt0 s opt_rule i st =
let
val ((_, goal), ctxt) = Variable.focus_subgoal i st ctxt0;
val rule =
@@ -46,8 +46,8 @@
in res_inst_tac ctxt [(xi, s)] rule i st end
handle THM _ => Seq.empty;
-fun case_tac ctxt s = gen_case_tac ctxt (s, NONE);
-fun case_rule_tac ctxt s rule = gen_case_tac ctxt (s, SOME rule);
+fun case_tac ctxt s = gen_case_tac ctxt s NONE;
+fun case_rule_tac ctxt s rule = gen_case_tac ctxt s (SOME rule);
(* induction *)
@@ -63,7 +63,7 @@
in
-fun gen_induct_tac ctxt0 (varss, opt_rules) i st =
+fun gen_induct_tac ctxt0 varss opt_rules i st =
let
val ((_, goal), ctxt) = Variable.focus_subgoal i st ctxt0;
val (prems, concl) = Logic.strip_horn (Thm.term_of goal);
@@ -103,8 +103,8 @@
end;
-fun induct_tac ctxt args = gen_induct_tac ctxt (args, NONE);
-fun induct_rules_tac ctxt args rules = gen_induct_tac ctxt (args, SOME rules);
+fun induct_tac ctxt args = gen_induct_tac ctxt args NONE;
+fun induct_rules_tac ctxt args rules = gen_induct_tac ctxt args (SOME rules);
(* method syntax *)
@@ -122,11 +122,14 @@
in
val setup =
- Method.add_methods
- [("case_tac", Method.goal_args_ctxt' (Scan.lift Args.name_source -- opt_rule) gen_case_tac,
- "unstructured case analysis on types"),
- ("induct_tac", Method.goal_args_ctxt' (varss -- opt_rules) gen_induct_tac,
- "unstructured induction on types")];
+ Method.setup @{binding case_tac}
+ (Args.goal_spec -- Scan.lift Args.name_source -- opt_rule >>
+ (fn ((quant, s), r) => fn ctxt => SIMPLE_METHOD'' quant (gen_case_tac ctxt s r)))
+ "unstructured case analysis on types" #>
+ Method.setup @{binding induct_tac}
+ (Args.goal_spec -- varss -- opt_rules >>
+ (fn ((quant, vs), rs) => fn ctxt => SIMPLE_METHOD'' quant (gen_induct_tac ctxt vs rs)))
+ "unstructured induction on types";
end;
--- a/src/ZF/Tools/induct_tacs.ML Sun Mar 15 20:19:14 2009 +0100
+++ b/src/ZF/Tools/induct_tacs.ML Sun Mar 15 20:25:58 2009 +0100
@@ -1,5 +1,4 @@
(* Title: ZF/Tools/induct_tacs.ML
- ID: $Id$
Author: Lawrence C Paulson, Cambridge University Computer Laboratory
Copyright 1994 University of Cambridge
@@ -177,11 +176,14 @@
(* theory setup *)
val setup =
- Method.add_methods
- [("induct_tac", Method.goal_args_ctxt Args.name induct_tac,
- "induct_tac emulation (dynamic instantiation!)"),
- ("case_tac", Method.goal_args_ctxt Args.name exhaust_tac,
- "datatype case_tac emulation (dynamic instantiation!)")];
+ Method.setup @{binding induct_tac}
+ (Args.goal_spec -- Scan.lift Args.name >>
+ (fn (quant, s) => fn ctxt => SIMPLE_METHOD'' quant (induct_tac ctxt s)))
+ "induct_tac emulation (dynamic instantiation!)" #>
+ Method.setup @{binding case_tac}
+ (Args.goal_spec -- Scan.lift Args.name >>
+ (fn (quant, s) => fn ctxt => SIMPLE_METHOD'' quant (exhaust_tac ctxt s)))
+ "datatype case_tac emulation (dynamic instantiation!)";
(* outer syntax *)
--- a/src/ZF/Tools/typechk.ML Sun Mar 15 20:19:14 2009 +0100
+++ b/src/ZF/Tools/typechk.ML Sun Mar 15 20:25:58 2009 +0100
@@ -1,5 +1,4 @@
(* Title: ZF/Tools/typechk.ML
- ID: $Id$
Author: Lawrence C Paulson, Cambridge University Computer Laboratory
Copyright 1999 University of Cambridge
@@ -111,10 +110,10 @@
(* concrete syntax *)
val typecheck_meth =
- Method.only_sectioned_args
+ Method.sections
[Args.add -- Args.colon >> K (I, TC_add),
Args.del -- Args.colon >> K (I, TC_del)]
- (fn ctxt => SIMPLE_METHOD (CHANGED (typecheck_tac ctxt)));
+ >> (K (fn ctxt => SIMPLE_METHOD (CHANGED (typecheck_tac ctxt))));
val _ =
OuterSyntax.improper_command "print_tcset" "print context of ZF typecheck" OuterKeyword.diag
@@ -126,7 +125,7 @@
val setup =
Attrib.setup @{binding TC} (Attrib.add_del TC_add TC_del) "declaration of type-checking rule" #>
- Method.add_methods [("typecheck", typecheck_meth, "ZF type-checking")] #>
+ Method.setup @{binding typecheck} typecheck_meth "ZF type-checking" #>
Simplifier.map_simpset (fn ss => ss setSolver type_solver);
end;