--- a/doc-src/IsarRef/Thy/Proof.thy Fri Mar 13 19:18:07 2009 +0100
+++ b/doc-src/IsarRef/Thy/Proof.thy Fri Mar 13 23:56:07 2009 +0100
@@ -895,11 +895,10 @@
%FIXME proper antiquotations
{\footnotesize
\begin{verbatim}
- Method.no_args (Method.METHOD (fn facts => foobar_tac))
- Method.thms_args (fn thms => Method.METHOD (fn facts => foobar_tac))
- Method.ctxt_args (fn ctxt => Method.METHOD (fn facts => foobar_tac))
- Method.thms_ctxt_args (fn thms => fn ctxt =>
- Method.METHOD (fn facts => foobar_tac))
+ Method.no_args (METHOD (fn facts => foobar_tac))
+ Method.thms_args (fn thms => METHOD (fn facts => foobar_tac))
+ Method.ctxt_args (fn ctxt => METHOD (fn facts => foobar_tac))
+ Method.thms_ctxt_args (fn thms => fn ctxt => METHOD (fn facts => foobar_tac))
\end{verbatim}
}
--- a/doc-src/IsarRef/Thy/document/Proof.tex Fri Mar 13 19:18:07 2009 +0100
+++ b/doc-src/IsarRef/Thy/document/Proof.tex Fri Mar 13 23:56:07 2009 +0100
@@ -899,11 +899,10 @@
%FIXME proper antiquotations
{\footnotesize
\begin{verbatim}
- Method.no_args (Method.METHOD (fn facts => foobar_tac))
- Method.thms_args (fn thms => Method.METHOD (fn facts => foobar_tac))
- Method.ctxt_args (fn ctxt => Method.METHOD (fn facts => foobar_tac))
- Method.thms_ctxt_args (fn thms => fn ctxt =>
- Method.METHOD (fn facts => foobar_tac))
+ Method.no_args (METHOD (fn facts => foobar_tac))
+ Method.thms_args (fn thms => METHOD (fn facts => foobar_tac))
+ Method.ctxt_args (fn ctxt => METHOD (fn facts => foobar_tac))
+ Method.thms_ctxt_args (fn thms => fn ctxt => METHOD (fn facts => foobar_tac))
\end{verbatim}
}
--- a/doc-src/TutorialI/Protocol/Event.thy Fri Mar 13 19:18:07 2009 +0100
+++ b/doc-src/TutorialI/Protocol/Event.thy Fri Mar 13 23:56:07 2009 +0100
@@ -287,7 +287,7 @@
intro: analz_subset_parts [THEN subsetD] parts_mono [THEN [2] rev_subsetD])
method_setup analz_mono_contra = {*
- Method.no_args (Method.SIMPLE_METHOD (REPEAT_FIRST analz_mono_contra_tac)) *}
+ Method.no_args (SIMPLE_METHOD (REPEAT_FIRST analz_mono_contra_tac)) *}
"for proving theorems of the form X \<notin> analz (knows Spy evs) --> P"
subsubsection{*Useful for case analysis on whether a hash is a spoof or not*}
@@ -344,7 +344,7 @@
*}
method_setup synth_analz_mono_contra = {*
- Method.no_args (Method.SIMPLE_METHOD (REPEAT_FIRST synth_analz_mono_contra_tac)) *}
+ Method.no_args (SIMPLE_METHOD (REPEAT_FIRST synth_analz_mono_contra_tac)) *}
"for proving theorems of the form X \<notin> synth (analz (knows Spy evs)) --> P"
(*>*)
--- a/doc-src/TutorialI/Protocol/Message.thy Fri Mar 13 19:18:07 2009 +0100
+++ b/doc-src/TutorialI/Protocol/Message.thy Fri Mar 13 23:56:07 2009 +0100
@@ -919,18 +919,15 @@
lemmas Fake_parts_sing_imp_Un = Fake_parts_sing [THEN [2] rev_subsetD]
method_setup spy_analz = {*
- Method.ctxt_args (fn ctxt =>
- Method.SIMPLE_METHOD (gen_spy_analz_tac (local_clasimpset_of ctxt) 1)) *}
+ Method.ctxt_args (SIMPLE_METHOD' o gen_spy_analz_tac o local_clasimpset_of) *}
"for proving the Fake case when analz is involved"
method_setup atomic_spy_analz = {*
- Method.ctxt_args (fn ctxt =>
- Method.SIMPLE_METHOD (atomic_spy_analz_tac (local_clasimpset_of ctxt) 1)) *}
+ Method.ctxt_args (SIMPLE_METHOD' o atomic_spy_analz_tac o local_clasimpset_of) *}
"for debugging spy_analz"
method_setup Fake_insert_simp = {*
- Method.ctxt_args (fn ctxt =>
- Method.SIMPLE_METHOD (Fake_insert_simp_tac (local_simpset_of ctxt) 1)) *}
+ Method.ctxt_args (SIMPLE_METHOD' o Fake_insert_simp_tac o local_simpset_of) *}
"for debugging spy_analz"
--- a/doc-src/TutorialI/Protocol/Public.thy Fri Mar 13 19:18:07 2009 +0100
+++ b/doc-src/TutorialI/Protocol/Public.thy Fri Mar 13 23:56:07 2009 +0100
@@ -161,8 +161,7 @@
resolve_tac [refl, conjI, @{thm Nonce_supply}]));
*}
-method_setup possibility = {*
- Method.no_args (Method.METHOD (fn facts => possibility_tac)) *}
+method_setup possibility = {* Method.no_args (SIMPLE_METHOD possibility_tac) *}
"for proving possibility theorems"
end
--- a/src/CCL/Wfd.thy Fri Mar 13 19:18:07 2009 +0100
+++ b/src/CCL/Wfd.thy Fri Mar 13 23:56:07 2009 +0100
@@ -504,8 +504,9 @@
val eval_setup =
Data.setup #>
- Method.add_methods [("eval", Method.thms_ctxt_args (fn ths => fn ctxt =>
- Method.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/Cube/Example.thy Fri Mar 13 19:18:07 2009 +0100
+++ b/src/Cube/Example.thy Fri Mar 13 23:56:07 2009 +0100
@@ -15,18 +15,18 @@
*}
method_setup depth_solve = {*
- Method.thms_args (fn thms => Method.METHOD (fn facts =>
+ Method.thms_args (fn thms => METHOD (fn facts =>
(DEPTH_SOLVE (HEADGOAL (ares_tac (facts @ thms))))))
*} ""
method_setup depth_solve1 = {*
- Method.thms_args (fn thms => Method.METHOD (fn facts =>
+ Method.thms_args (fn thms => METHOD (fn facts =>
(DEPTH_SOLVE_1 (HEADGOAL (ares_tac (facts @ thms))))))
*} ""
method_setup strip_asms = {*
let val strip_b = thm "strip_b" and strip_s = thm "strip_s" in
- Method.thms_args (fn thms => Method.METHOD (fn facts =>
+ Method.thms_args (fn thms => METHOD (fn facts =>
REPEAT (resolve_tac [strip_b, strip_s] 1 THEN DEPTH_SOLVE_1 (ares_tac (facts @ thms) 1))))
end
*} ""
--- a/src/FOL/ex/Iff_Oracle.thy Fri Mar 13 19:18:07 2009 +0100
+++ b/src/FOL/ex/Iff_Oracle.thy Fri Mar 13 23:56:07 2009 +0100
@@ -53,7 +53,7 @@
method_setup iff = {*
Method.simple_args OuterParse.nat (fn n => fn ctxt =>
- Method.SIMPLE_METHOD
+ SIMPLE_METHOD
(HEADGOAL (Tactic.rtac (iff_oracle (ProofContext.theory_of ctxt, n)))
handle Fail _ => no_tac))
*} "iff oracle"
--- a/src/HOL/Algebra/abstract/Ring2.thy Fri Mar 13 19:18:07 2009 +0100
+++ b/src/HOL/Algebra/abstract/Ring2.thy Fri Mar 13 23:56:07 2009 +0100
@@ -222,7 +222,7 @@
*} (* Note: r_one is not necessary in ring_ss *)
method_setup ring =
- {* Method.no_args (Method.SIMPLE_METHOD' (full_simp_tac ring_ss)) *}
+ {* Method.no_args (SIMPLE_METHOD' (full_simp_tac ring_ss)) *}
{* computes distributive normal form in rings *}
--- a/src/HOL/Algebra/ringsimp.ML Fri Mar 13 19:18:07 2009 +0100
+++ b/src/HOL/Algebra/ringsimp.ML Fri Mar 13 23:56:07 2009 +0100
@@ -72,8 +72,8 @@
(** Setup **)
val setup =
- Method.add_methods [("algebra", Method.ctxt_args (Method.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/Auth/Event.thy Fri Mar 13 19:18:07 2009 +0100
+++ b/src/HOL/Auth/Event.thy Fri Mar 13 23:56:07 2009 +0100
@@ -289,7 +289,7 @@
*}
method_setup analz_mono_contra = {*
- Method.no_args (Method.SIMPLE_METHOD (REPEAT_FIRST analz_mono_contra_tac)) *}
+ Method.no_args (SIMPLE_METHOD (REPEAT_FIRST analz_mono_contra_tac)) *}
"for proving theorems of the form X \<notin> analz (knows Spy evs) --> P"
subsubsection{*Useful for case analysis on whether a hash is a spoof or not*}
@@ -310,7 +310,7 @@
*}
method_setup synth_analz_mono_contra = {*
- Method.no_args (Method.SIMPLE_METHOD (REPEAT_FIRST synth_analz_mono_contra_tac)) *}
+ Method.no_args (SIMPLE_METHOD (REPEAT_FIRST synth_analz_mono_contra_tac)) *}
"for proving theorems of the form X \<notin> synth (analz (knows Spy evs)) --> P"
end
--- a/src/HOL/Auth/Message.thy Fri Mar 13 19:18:07 2009 +0100
+++ b/src/HOL/Auth/Message.thy Fri Mar 13 23:56:07 2009 +0100
@@ -941,18 +941,15 @@
lemmas Fake_parts_sing_imp_Un = Fake_parts_sing [THEN [2] rev_subsetD]
method_setup spy_analz = {*
- Method.ctxt_args (fn ctxt =>
- Method.SIMPLE_METHOD (Message.gen_spy_analz_tac (local_clasimpset_of ctxt) 1)) *}
+ Method.ctxt_args (SIMPLE_METHOD' o Message.gen_spy_analz_tac o local_clasimpset_of) *}
"for proving the Fake case when analz is involved"
method_setup atomic_spy_analz = {*
- Method.ctxt_args (fn ctxt =>
- Method.SIMPLE_METHOD (Message.atomic_spy_analz_tac (local_clasimpset_of ctxt) 1)) *}
+ Method.ctxt_args (SIMPLE_METHOD' o Message.atomic_spy_analz_tac o local_clasimpset_of) *}
"for debugging spy_analz"
method_setup Fake_insert_simp = {*
- Method.ctxt_args (fn ctxt =>
- Method.SIMPLE_METHOD (Message.Fake_insert_simp_tac (local_simpset_of ctxt) 1)) *}
+ Method.ctxt_args (SIMPLE_METHOD' o Message.Fake_insert_simp_tac o local_simpset_of) *}
"for debugging spy_analz"
end
--- a/src/HOL/Auth/OtwayReesBella.thy Fri Mar 13 19:18:07 2009 +0100
+++ b/src/HOL/Auth/OtwayReesBella.thy Fri Mar 13 23:56:07 2009 +0100
@@ -137,7 +137,7 @@
*}
method_setup parts_explicit = {*
- Method.no_args (Method.SIMPLE_METHOD' parts_explicit_tac) *}
+ Method.no_args (SIMPLE_METHOD' parts_explicit_tac) *}
"to explicitly state that some message components belong to parts knows Spy"
@@ -258,7 +258,7 @@
method_setup analz_freshCryptK = {*
Method.ctxt_args (fn ctxt =>
- (Method.SIMPLE_METHOD
+ (SIMPLE_METHOD
(EVERY [REPEAT_FIRST (resolve_tac [allI, ballI, impI]),
REPEAT_FIRST (rtac @{thm analz_image_freshCryptK_lemma}),
ALLGOALS (asm_simp_tac
@@ -268,7 +268,7 @@
method_setup disentangle = {*
Method.no_args
- (Method.SIMPLE_METHOD
+ (SIMPLE_METHOD
(REPEAT_FIRST (eresolve_tac [asm_rl, conjE, disjE]
ORELSE' hyp_subst_tac))) *}
"for eliminating conjunctions, disjunctions and the like"
--- a/src/HOL/Auth/Public.thy Fri Mar 13 19:18:07 2009 +0100
+++ b/src/HOL/Auth/Public.thy Fri Mar 13 23:56:07 2009 +0100
@@ -425,7 +425,7 @@
method_setup analz_freshK = {*
Method.ctxt_args (fn ctxt =>
- (Method.SIMPLE_METHOD
+ (SIMPLE_METHOD
(EVERY [REPEAT_FIRST (resolve_tac [allI, ballI, impI]),
REPEAT_FIRST (rtac @{thm analz_image_freshK_lemma}),
ALLGOALS (asm_simp_tac (Simplifier.context ctxt Public.analz_image_freshK_ss))]))) *}
@@ -435,13 +435,11 @@
subsection{*Specialized Methods for Possibility Theorems*}
method_setup possibility = {*
- Method.ctxt_args (fn ctxt =>
- Method.SIMPLE_METHOD (Public.possibility_tac ctxt)) *}
+ Method.ctxt_args (SIMPLE_METHOD o Public.possibility_tac) *}
"for proving possibility theorems"
method_setup basic_possibility = {*
- Method.ctxt_args (fn ctxt =>
- Method.SIMPLE_METHOD (Public.basic_possibility_tac ctxt)) *}
+ Method.ctxt_args (SIMPLE_METHOD o Public.basic_possibility_tac) *}
"for proving possibility theorems"
end
--- a/src/HOL/Auth/Shared.thy Fri Mar 13 19:18:07 2009 +0100
+++ b/src/HOL/Auth/Shared.thy Fri Mar 13 23:56:07 2009 +0100
@@ -239,20 +239,18 @@
method_setup analz_freshK = {*
Method.ctxt_args (fn ctxt =>
- (Method.SIMPLE_METHOD
+ (SIMPLE_METHOD
(EVERY [REPEAT_FIRST (resolve_tac [allI, ballI, impI]),
REPEAT_FIRST (rtac @{thm analz_image_freshK_lemma}),
ALLGOALS (asm_simp_tac (Simplifier.context ctxt Shared.analz_image_freshK_ss))]))) *}
"for proving the Session Key Compromise theorem"
method_setup possibility = {*
- Method.ctxt_args (fn ctxt =>
- Method.SIMPLE_METHOD (Shared.possibility_tac ctxt)) *}
+ Method.ctxt_args (fn ctxt => SIMPLE_METHOD (Shared.possibility_tac ctxt)) *}
"for proving possibility theorems"
method_setup basic_possibility = {*
- Method.ctxt_args (fn ctxt =>
- Method.SIMPLE_METHOD (Shared.basic_possibility_tac ctxt)) *}
+ Method.ctxt_args (fn ctxt => SIMPLE_METHOD (Shared.basic_possibility_tac ctxt)) *}
"for proving possibility theorems"
lemma knows_subset_knows_Cons: "knows A evs <= knows A (e # evs)"
--- a/src/HOL/Auth/Smartcard/ShoupRubin.thy Fri Mar 13 19:18:07 2009 +0100
+++ b/src/HOL/Auth/Smartcard/ShoupRubin.thy Fri Mar 13 23:56:07 2009 +0100
@@ -769,15 +769,15 @@
*}
method_setup prepare = {*
- Method.no_args (Method.SIMPLE_METHOD ShoupRubin.prepare_tac) *}
+ Method.no_args (SIMPLE_METHOD ShoupRubin.prepare_tac) *}
"to launch a few simple facts that'll help the simplifier"
method_setup parts_prepare = {*
- Method.ctxt_args (fn ctxt => Method.SIMPLE_METHOD (ShoupRubin.parts_prepare_tac ctxt)) *}
+ Method.ctxt_args (fn ctxt => SIMPLE_METHOD (ShoupRubin.parts_prepare_tac ctxt)) *}
"additional facts to reason about parts"
method_setup analz_prepare = {*
- Method.no_args (Method.SIMPLE_METHOD ShoupRubin.analz_prepare_tac) *}
+ Method.no_args (SIMPLE_METHOD ShoupRubin.analz_prepare_tac) *}
"additional facts to reason about analz"
@@ -823,7 +823,7 @@
method_setup sc_analz_freshK = {*
Method.ctxt_args (fn ctxt =>
- (Method.SIMPLE_METHOD
+ (SIMPLE_METHOD
(EVERY [REPEAT_FIRST
(resolve_tac [allI, ballI, impI]),
REPEAT_FIRST (rtac @{thm analz_image_freshK_lemma}),
--- a/src/HOL/Auth/Smartcard/ShoupRubinBella.thy Fri Mar 13 19:18:07 2009 +0100
+++ b/src/HOL/Auth/Smartcard/ShoupRubinBella.thy Fri Mar 13 23:56:07 2009 +0100
@@ -777,15 +777,15 @@
*}
method_setup prepare = {*
- Method.ctxt_args (fn ctxt => Method.SIMPLE_METHOD (ShoupRubinBella.prepare_tac ctxt)) *}
+ Method.ctxt_args (fn ctxt => SIMPLE_METHOD (ShoupRubinBella.prepare_tac ctxt)) *}
"to launch a few simple facts that'll help the simplifier"
method_setup parts_prepare = {*
- Method.ctxt_args (fn ctxt => Method.SIMPLE_METHOD (ShoupRubinBella.parts_prepare_tac ctxt)) *}
+ Method.ctxt_args (fn ctxt => SIMPLE_METHOD (ShoupRubinBella.parts_prepare_tac ctxt)) *}
"additional facts to reason about parts"
method_setup analz_prepare = {*
- Method.ctxt_args (fn ctxt => Method.SIMPLE_METHOD (ShoupRubinBella.analz_prepare_tac ctxt)) *}
+ Method.ctxt_args (fn ctxt => SIMPLE_METHOD (ShoupRubinBella.analz_prepare_tac ctxt)) *}
"additional facts to reason about analz"
@@ -832,7 +832,7 @@
method_setup sc_analz_freshK = {*
Method.ctxt_args (fn ctxt =>
- (Method.SIMPLE_METHOD
+ (SIMPLE_METHOD
(EVERY [REPEAT_FIRST (resolve_tac [allI, ballI, impI]),
REPEAT_FIRST (rtac @{thm analz_image_freshK_lemma}),
ALLGOALS (asm_simp_tac (Simplifier.context ctxt Smartcard.analz_image_freshK_ss
--- a/src/HOL/Auth/Smartcard/Smartcard.thy Fri Mar 13 19:18:07 2009 +0100
+++ b/src/HOL/Auth/Smartcard/Smartcard.thy Fri Mar 13 23:56:07 2009 +0100
@@ -408,7 +408,7 @@
method_setup analz_freshK = {*
Method.ctxt_args (fn ctxt =>
- (Method.SIMPLE_METHOD
+ (SIMPLE_METHOD
(EVERY [REPEAT_FIRST (resolve_tac [allI, ballI, impI]),
REPEAT_FIRST (rtac @{thm analz_image_freshK_lemma}),
ALLGOALS (asm_simp_tac (Simplifier.context ctxt Smartcard.analz_image_freshK_ss))]))) *}
@@ -416,12 +416,12 @@
method_setup possibility = {*
Method.ctxt_args (fn ctxt =>
- Method.SIMPLE_METHOD (Smartcard.possibility_tac ctxt)) *}
+ SIMPLE_METHOD (Smartcard.possibility_tac ctxt)) *}
"for proving possibility theorems"
method_setup basic_possibility = {*
Method.ctxt_args (fn ctxt =>
- Method.SIMPLE_METHOD (Smartcard.basic_possibility_tac ctxt)) *}
+ SIMPLE_METHOD (Smartcard.basic_possibility_tac ctxt)) *}
"for proving possibility theorems"
lemma knows_subset_knows_Cons: "knows A evs \<subseteq> knows A (e # evs)"
--- a/src/HOL/Code_Setup.thy Fri Mar 13 19:18:07 2009 +0100
+++ b/src/HOL/Code_Setup.thy Fri Mar 13 23:56:07 2009 +0100
@@ -226,7 +226,7 @@
*}
ML {*
-fun gen_eval_method conv = Method.ctxt_args (fn ctxt => Method.SIMPLE_METHOD'
+fun gen_eval_method conv = Method.ctxt_args (fn ctxt => SIMPLE_METHOD'
(CONVERSION (Conv.params_conv (~1) (K (Conv.concl_conv (~1) conv)) ctxt)
THEN' rtac TrueI))
*}
@@ -237,7 +237,7 @@
method_setup evaluation = {* gen_eval_method Codegen.evaluation_conv *}
"solve goal by evaluation"
-method_setup normalization = {* (Method.no_args o Method.SIMPLE_METHOD')
+method_setup normalization = {* (Method.no_args o SIMPLE_METHOD')
(CONVERSION Nbe.norm_conv THEN' (fn k => TRY (rtac TrueI k)))
*} "solve goal by normalization"
--- a/src/HOL/Decision_Procs/Approximation.thy Fri Mar 13 19:18:07 2009 +0100
+++ b/src/HOL/Decision_Procs/Approximation.thy Fri Mar 13 23:56:07 2009 +0100
@@ -2499,7 +2499,7 @@
method_setup approximation = {* fn src =>
Method.syntax Args.term src #>
(fn (prec, ctxt) => let
- in Method.SIMPLE_METHOD' (fn i =>
+ in SIMPLE_METHOD' (fn i =>
(DETERM (reify_uneq ctxt i)
THEN rule_uneq ctxt prec i
THEN Simplifier.asm_full_simp_tac bounded_by_simpset i
--- a/src/HOL/Decision_Procs/Dense_Linear_Order.thy Fri Mar 13 19:18:07 2009 +0100
+++ b/src/HOL/Decision_Procs/Dense_Linear_Order.thy Fri Mar 13 23:56:07 2009 +0100
@@ -295,7 +295,7 @@
use "~~/src/HOL/Tools/Qelim/langford.ML"
method_setup dlo = {*
- Method.ctxt_args (Method.SIMPLE_METHOD' o LangfordQE.dlo_tac)
+ Method.ctxt_args (SIMPLE_METHOD' o LangfordQE.dlo_tac)
*} "Langford's algorithm for quantifier elimination in dense linear orders"
@@ -546,7 +546,7 @@
use "~~/src/HOL/Tools/Qelim/ferrante_rackoff.ML"
method_setup ferrack = {*
- Method.ctxt_args (Method.SIMPLE_METHOD' o FerranteRackoff.dlo_tac)
+ Method.ctxt_args (SIMPLE_METHOD' o FerranteRackoff.dlo_tac)
*} "Ferrante and Rackoff's algorithm for quantifier elimination in dense linear orders"
subsection {* Ferrante and Rackoff algorithm over ordered fields *}
--- a/src/HOL/Decision_Procs/cooper_tac.ML Fri Mar 13 19:18:07 2009 +0100
+++ b/src/HOL/Decision_Procs/cooper_tac.ML Fri Mar 13 23:56:07 2009 +0100
@@ -121,11 +121,10 @@
Method.simple_args
(Scan.optional (Args.$$$ "(" |-- Scan.repeat1 parse_flag --| Args.$$$ ")") [] >>
curry (Library.foldl op |>) true)
- (fn q => fn ctxt => meth ctxt q 1)
+ (fn q => fn ctxt => meth ctxt q)
end;
-fun linz_method ctxt q i = Method.METHOD (fn facts =>
- Method.insert_tac facts 1 THEN linz_tac ctxt q i);
+fun linz_method ctxt q = SIMPLE_METHOD' (linz_tac ctxt q);
val setup =
Method.add_method ("cooper",
--- a/src/HOL/Decision_Procs/ferrack_tac.ML Fri Mar 13 19:18:07 2009 +0100
+++ b/src/HOL/Decision_Procs/ferrack_tac.ML Fri Mar 13 23:56:07 2009 +0100
@@ -100,7 +100,7 @@
fun linr_meth src =
Method.syntax (Args.mode "no_quantify") src
- #> (fn (q, ctxt) => Method.SIMPLE_METHOD' (linr_tac ctxt (not q)));
+ #> (fn (q, ctxt) => SIMPLE_METHOD' (linr_tac ctxt (not q)));
val setup =
Method.add_method ("rferrack", linr_meth,
--- a/src/HOL/Decision_Procs/mir_tac.ML Fri Mar 13 19:18:07 2009 +0100
+++ b/src/HOL/Decision_Procs/mir_tac.ML Fri Mar 13 23:56:07 2009 +0100
@@ -150,11 +150,10 @@
Method.simple_args
(Scan.optional (Args.$$$ "(" |-- Scan.repeat1 parse_flag --| Args.$$$ ")") [] >>
curry (Library.foldl op |>) true)
- (fn q => fn ctxt => meth ctxt q 1)
+ (fn q => fn ctxt => meth ctxt q)
end;
-fun mir_method ctxt q i = Method.METHOD (fn facts =>
- Method.insert_tac facts 1 THEN mir_tac ctxt q i);
+fun mir_method ctxt q = SIMPLE_METHOD' (mir_tac ctxt q);
val setup =
Method.add_method ("mir",
--- a/src/HOL/Groebner_Basis.thy Fri Mar 13 19:18:07 2009 +0100
+++ b/src/HOL/Groebner_Basis.thy Fri Mar 13 23:56:07 2009 +0100
@@ -253,7 +253,7 @@
method_setup sring_norm = {*
- Method.ctxt_args (fn ctxt => Method.SIMPLE_METHOD' (Normalizer.semiring_normalize_tac ctxt))
+ Method.ctxt_args (SIMPLE_METHOD' o Normalizer.semiring_normalize_tac)
*} "semiring normalizer"
@@ -431,7 +431,7 @@
((Scan.optional (keyword addN |-- thms) []) --
(Scan.optional (keyword delN |-- thms) [])) src
#> (fn ((add_ths, del_ths), ctxt) =>
- Method.SIMPLE_METHOD' (Groebner.algebra_tac add_ths del_ths ctxt))
+ SIMPLE_METHOD' (Groebner.algebra_tac add_ths del_ths ctxt))
end
*} "solve polynomial equations over (semi)rings and ideal membership problems using Groebner bases"
declare dvd_def[algebra]
--- a/src/HOL/Hoare/Hoare.thy Fri Mar 13 19:18:07 2009 +0100
+++ b/src/HOL/Hoare/Hoare.thy Fri Mar 13 23:56:07 2009 +0100
@@ -234,12 +234,12 @@
use "hoare_tac.ML"
method_setup vcg = {*
- Method.ctxt_args (fn ctxt => Method.SIMPLE_METHOD' (hoare_tac ctxt (K all_tac))) *}
+ Method.ctxt_args (fn ctxt => SIMPLE_METHOD' (hoare_tac ctxt (K all_tac))) *}
"verification condition generator"
method_setup vcg_simp = {*
Method.ctxt_args (fn ctxt =>
- Method.SIMPLE_METHOD' (hoare_tac ctxt (asm_full_simp_tac (local_simpset_of ctxt)))) *}
+ SIMPLE_METHOD' (hoare_tac ctxt (asm_full_simp_tac (local_simpset_of ctxt)))) *}
"verification condition generator plus simplification"
end
--- a/src/HOL/Hoare/HoareAbort.thy Fri Mar 13 19:18:07 2009 +0100
+++ b/src/HOL/Hoare/HoareAbort.thy Fri Mar 13 23:56:07 2009 +0100
@@ -246,12 +246,12 @@
use "hoare_tac.ML"
method_setup vcg = {*
- Method.ctxt_args (fn ctxt => Method.SIMPLE_METHOD' (hoare_tac ctxt (K all_tac))) *}
+ Method.ctxt_args (fn ctxt => SIMPLE_METHOD' (hoare_tac ctxt (K all_tac))) *}
"verification condition generator"
method_setup vcg_simp = {*
Method.ctxt_args (fn ctxt =>
- Method.SIMPLE_METHOD' (hoare_tac ctxt (asm_full_simp_tac (local_simpset_of ctxt)))) *}
+ SIMPLE_METHOD' (hoare_tac ctxt (asm_full_simp_tac (local_simpset_of ctxt)))) *}
"verification condition generator plus simplification"
(* Special syntax for guarded statements and guarded array updates: *)
--- a/src/HOL/HoareParallel/OG_Tactics.thy Fri Mar 13 19:18:07 2009 +0100
+++ b/src/HOL/HoareParallel/OG_Tactics.thy Fri Mar 13 23:56:07 2009 +0100
@@ -465,21 +465,21 @@
Isabelle proofs. *}
method_setup oghoare = {*
- Method.no_args (Method.SIMPLE_METHOD' oghoare_tac) *}
+ Method.no_args (SIMPLE_METHOD' oghoare_tac) *}
"verification condition generator for the oghoare logic"
method_setup annhoare = {*
- Method.no_args (Method.SIMPLE_METHOD' annhoare_tac) *}
+ Method.no_args (SIMPLE_METHOD' annhoare_tac) *}
"verification condition generator for the ann_hoare logic"
method_setup interfree_aux = {*
- Method.no_args (Method.SIMPLE_METHOD' interfree_aux_tac) *}
+ Method.no_args (SIMPLE_METHOD' interfree_aux_tac) *}
"verification condition generator for interference freedom tests"
text {* Tactics useful for dealing with the generated verification conditions: *}
method_setup conjI_tac = {*
- Method.no_args (Method.SIMPLE_METHOD' (conjI_Tac (K all_tac))) *}
+ Method.no_args (SIMPLE_METHOD' (conjI_Tac (K all_tac))) *}
"verification condition generator for interference freedom tests"
ML {*
@@ -490,7 +490,7 @@
*}
method_setup disjE_tac = {*
- Method.no_args (Method.SIMPLE_METHOD' (disjE_Tac (K all_tac))) *}
+ Method.no_args (SIMPLE_METHOD' (disjE_Tac (K all_tac))) *}
"verification condition generator for interference freedom tests"
end
--- a/src/HOL/Import/import_package.ML Fri Mar 13 19:18:07 2009 +0100
+++ b/src/HOL/Import/import_package.ML Fri Mar 13 23:56:07 2009 +0100
@@ -73,7 +73,7 @@
let
val thy = ProofContext.theory_of ctxt
in
- Method.SIMPLE_METHOD (import_tac arg thy)
+ SIMPLE_METHOD (import_tac arg thy)
end)
val setup = Method.add_method("import",import_meth,"Import HOL4 theorem")
--- a/src/HOL/Import/shuffler.ML Fri Mar 13 19:18:07 2009 +0100
+++ b/src/HOL/Import/shuffler.ML Fri Mar 13 23:56:07 2009 +0100
@@ -656,7 +656,7 @@
let
val thy = ProofContext.theory_of ctxt
in
- Method.SIMPLE_METHOD' (gen_shuffle_tac thy false (map (pair "") thms))
+ SIMPLE_METHOD' (gen_shuffle_tac thy false (map (pair "") thms))
end
fun search_meth ctxt =
@@ -664,7 +664,7 @@
val thy = ProofContext.theory_of ctxt
val prems = Assumption.all_prems_of ctxt
in
- Method.SIMPLE_METHOD' (gen_shuffle_tac thy true (map (pair "premise") prems))
+ SIMPLE_METHOD' (gen_shuffle_tac thy true (map (pair "premise") prems))
end
fun add_shuffle_rule thm thy =
--- a/src/HOL/Isar_examples/Hoare.thy Fri Mar 13 19:18:07 2009 +0100
+++ b/src/HOL/Isar_examples/Hoare.thy Fri Mar 13 23:56:07 2009 +0100
@@ -455,7 +455,7 @@
method_setup hoare = {*
Method.ctxt_args (fn ctxt =>
- (Method.SIMPLE_METHOD'
+ (SIMPLE_METHOD'
(hoare_tac ctxt (simp_tac (HOL_basic_ss addsimps [@{thm "Record.K_record_comp"}] ))))) *}
"verification condition generator for Hoare logic"
--- a/src/HOL/Library/Euclidean_Space.thy Fri Mar 13 19:18:07 2009 +0100
+++ b/src/HOL/Library/Euclidean_Space.thy Fri Mar 13 23:56:07 2009 +0100
@@ -134,7 +134,7 @@
(* THEN' TRY o clarify_tac HOL_cs THEN' (TRY o rtac @{thm iffI}) *)
THEN' asm_full_simp_tac (ss2 addsimps ths)
in
- Method.thms_args (Method.SIMPLE_METHOD' o vector_arith_tac)
+ Method.thms_args (SIMPLE_METHOD' o vector_arith_tac)
end
*} "Lifts trivial vector statements to real arith statements"
@@ -948,7 +948,7 @@
use "normarith.ML"
-method_setup norm = {* Method.ctxt_args (Method.SIMPLE_METHOD' o NormArith.norm_arith_tac)
+method_setup norm = {* Method.ctxt_args (SIMPLE_METHOD' o NormArith.norm_arith_tac)
*} "Proves simple linear statements about vector norms"
--- a/src/HOL/Library/Eval_Witness.thy Fri Mar 13 19:18:07 2009 +0100
+++ b/src/HOL/Library/Eval_Witness.thy Fri Mar 13 23:56:07 2009 +0100
@@ -84,7 +84,7 @@
in
Method.simple_args (Scan.repeat Args.name) (fn ws => fn _ =>
- Method.SIMPLE_METHOD' (eval_tac ws))
+ SIMPLE_METHOD' (eval_tac ws))
end
*} "Evaluation with ML witnesses"
--- a/src/HOL/Library/Reflection.thy Fri Mar 13 19:18:07 2009 +0100
+++ b/src/HOL/Library/Reflection.thy Fri Mar 13 23:56:07 2009 +0100
@@ -19,7 +19,7 @@
method_setup reify = {* fn src =>
Method.syntax (Attrib.thms --
Scan.option (Scan.lift (Args.$$$ "(") |-- Args.term --| Scan.lift (Args.$$$ ")") )) src #>
- (fn ((eqs, to), ctxt) => Method.SIMPLE_METHOD' (Reflection.genreify_tac ctxt (eqs @ (fst (Reify_Data.get ctxt))) to))
+ (fn ((eqs, to), ctxt) => SIMPLE_METHOD' (Reflection.genreify_tac ctxt (eqs @ (fst (Reify_Data.get ctxt))) to))
*} "partial automatic reification"
method_setup reflection = {*
@@ -38,7 +38,7 @@
val (ceqs,cths) = Reify_Data.get ctxt
val corr_thms = ths@cths
val raw_eqs = eqs@ceqs
- in Method.SIMPLE_METHOD' (Reflection.reflection_tac ctxt corr_thms raw_eqs to)
+ in SIMPLE_METHOD' (Reflection.reflection_tac ctxt corr_thms raw_eqs to)
end) end
*} "reflection method"
--- a/src/HOL/Library/Topology_Euclidean_Space.thy Fri Mar 13 19:18:07 2009 +0100
+++ b/src/HOL/Library/Topology_Euclidean_Space.thy Fri Mar 13 23:56:07 2009 +0100
@@ -978,7 +978,7 @@
val ss1 = HOL_basic_ss addsimps [@{thm expand_fun_eq} RS sym]
val ss2 = HOL_basic_ss addsimps [@{thm mknet_inverse'}]
fun tac ths = ObjectLogic.full_atomize_tac THEN' Simplifier.simp_tac (ss1 addsimps ths) THEN' Simplifier.asm_full_simp_tac ss2
- in Method.thms_args (Method.SIMPLE_METHOD' o tac) end
+ in Method.thms_args (SIMPLE_METHOD' o tac) end
*} "Reduces goals about net"
--- a/src/HOL/Library/comm_ring.ML Fri Mar 13 19:18:07 2009 +0100
+++ b/src/HOL/Library/comm_ring.ML Fri Mar 13 23:56:07 2009 +0100
@@ -101,7 +101,7 @@
end);
val comm_ring_meth =
- Method.ctxt_args (Method.SIMPLE_METHOD' o comm_ring_tac);
+ Method.ctxt_args (SIMPLE_METHOD' o comm_ring_tac);
val setup =
Method.add_method ("comm_ring", comm_ring_meth,
--- a/src/HOL/NSA/transfer.ML Fri Mar 13 19:18:07 2009 +0100
+++ b/src/HOL/NSA/transfer.ML Fri Mar 13 23:56:07 2009 +0100
@@ -116,6 +116,6 @@
("transfer_refold", Attrib.add_del_args refold_add refold_del,
"declaration of transfer refolding rule")] #>
Method.add_method ("transfer", Method.thms_ctxt_args (fn ths => fn ctxt =>
- Method.SIMPLE_METHOD' (transfer_tac ctxt ths)), "transfer principle");
+ SIMPLE_METHOD' (transfer_tac ctxt ths)), "transfer principle");
end;
--- a/src/HOL/Nominal/nominal_fresh_fun.ML Fri Mar 13 19:18:07 2009 +0100
+++ b/src/HOL/Nominal/nominal_fresh_fun.ML Fri Mar 13 23:56:07 2009 +0100
@@ -204,4 +204,4 @@
val setup_fresh_fun_simp =
Method.simple_args options_syntax
- (fn b => fn _ => Method.SIMPLE_METHOD (fresh_fun_tac b 1))
+ (fn b => fn _ => SIMPLE_METHOD (fresh_fun_tac b 1))
--- a/src/HOL/Nominal/nominal_induct.ML Fri Mar 13 19:18:07 2009 +0100
+++ b/src/HOL/Nominal/nominal_induct.ML Fri Mar 13 23:56:07 2009 +0100
@@ -8,7 +8,7 @@
val nominal_induct_tac: Proof.context -> (binding option * term) option list list ->
(string * typ) list -> (string * typ) list list -> thm list ->
thm list -> int -> RuleCases.cases_tactic
- val nominal_induct_method: Method.src -> Proof.context -> Method.method
+ val nominal_induct_method: Method.src -> Proof.context -> Proof.method
end =
struct
@@ -157,7 +157,7 @@
(P.and_list' (Scan.repeat (unless_more_args def_inst)) --
avoiding -- fixing -- rule_spec) src
#> (fn ((((x, y), z), w), ctxt) =>
- Method.RAW_METHOD_CASES (fn facts =>
+ RAW_METHOD_CASES (fn facts =>
HEADGOAL (nominal_induct_tac ctxt x y z w facts)));
end;
--- a/src/HOL/Nominal/nominal_permeq.ML Fri Mar 13 19:18:07 2009 +0100
+++ b/src/HOL/Nominal/nominal_permeq.ML Fri Mar 13 23:56:07 2009 +0100
@@ -400,7 +400,7 @@
Args.parens (Args.$$$ asm_lrN) >> K (perm_asm_lr_simp_tac_i NO_DEBUG_tac) ||
Scan.succeed (perm_asm_full_simp_tac_i NO_DEBUG_tac));
-fun perm_simp_method (prems, tac) ctxt = Method.METHOD (fn facts =>
+fun perm_simp_method (prems, tac) ctxt = METHOD (fn facts =>
HEADGOAL (Method.insert_tac (prems @ facts) THEN'
((CHANGED_PROP) oo tac) (local_simpset_of ctxt)));
@@ -411,7 +411,7 @@
(* setup so that the simpset is used which is active at the moment when the tactic is called *)
fun local_simp_meth_setup tac =
Method.only_sectioned_args (Simplifier.simp_modifiers' @ Splitter.split_modifiers)
- (Method.SIMPLE_METHOD' o tac o local_simpset_of) ;
+ (SIMPLE_METHOD' o tac o local_simpset_of) ;
(* uses HOL_basic_ss only and fails if the tactic does not solve the subgoal *)
@@ -419,7 +419,7 @@
Method.sectioned_args
(fn (ctxt,l) => ((),((Simplifier.map_ss (fn _ => HOL_basic_ss) ctxt),l)))
(Simplifier.simp_modifiers' @ Splitter.split_modifiers)
- (fn _ => Method.SIMPLE_METHOD' o (fn ss => if debug then (tac ss) else SOLVEI (tac ss)) o local_simpset_of);
+ (fn _ => SIMPLE_METHOD' o (fn ss => if debug then (tac ss) else SOLVEI (tac ss)) o local_simpset_of);
val perm_simp_meth_debug = local_simp_meth_setup dperm_simp_tac;
val perm_extend_simp_meth = local_simp_meth_setup perm_extend_simp_tac;
--- a/src/HOL/Nominal/nominal_primrec.ML Fri Mar 13 19:18:07 2009 +0100
+++ b/src/HOL/Nominal/nominal_primrec.ML Fri Mar 13 23:56:07 2009 +0100
@@ -378,7 +378,7 @@
|> snd
end)
[goals] |>
- Proof.apply (Method.Basic (fn _ => Method.RAW_METHOD (fn _ =>
+ Proof.apply (Method.Basic (fn _ => RAW_METHOD (fn _ =>
rewrite_goals_tac defs_thms THEN
compose_tac (false, rule, length rule_prems) 1), Position.none)) |>
Seq.hd
--- a/src/HOL/Orderings.thy Fri Mar 13 19:18:07 2009 +0100
+++ b/src/HOL/Orderings.thy Fri Mar 13 23:56:07 2009 +0100
@@ -397,8 +397,7 @@
(** Setup **)
val setup =
- Method.add_methods
- [("order", Method.ctxt_args (Method.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/Presburger.thy Fri Mar 13 19:18:07 2009 +0100
+++ b/src/HOL/Presburger.thy Fri Mar 13 23:56:07 2009 +0100
@@ -460,7 +460,7 @@
(Scan.optional (keyword addN |-- thms) []) --
(Scan.optional (keyword delN |-- thms) [])) src
#> (fn (((elim, add_ths), del_ths),ctxt) =>
- Method.SIMPLE_METHOD' (Presburger.cooper_tac elim add_ths del_ths ctxt))
+ SIMPLE_METHOD' (Presburger.cooper_tac elim add_ths del_ths ctxt))
end
*} "Cooper's algorithm for Presburger arithmetic"
--- a/src/HOL/Prolog/HOHH.thy Fri Mar 13 19:18:07 2009 +0100
+++ b/src/HOL/Prolog/HOHH.thy Fri Mar 13 23:56:07 2009 +0100
@@ -11,11 +11,11 @@
begin
method_setup ptac =
- {* Method.thms_ctxt_args (fn thms => fn ctxt => Method.SIMPLE_METHOD' (Prolog.ptac ctxt thms)) *}
+ {* Method.thms_ctxt_args (fn thms => fn ctxt => SIMPLE_METHOD' (Prolog.ptac ctxt thms)) *}
"Basic Lambda Prolog interpreter"
method_setup prolog =
- {* Method.thms_ctxt_args (fn thms => fn ctxt => Method.SIMPLE_METHOD (Prolog.prolog_tac ctxt thms)) *}
+ {* Method.thms_ctxt_args (fn thms => fn ctxt => SIMPLE_METHOD (Prolog.prolog_tac ctxt thms)) *}
"Lambda Prolog interpreter"
consts
--- a/src/HOL/SAT.thy Fri Mar 13 19:18:07 2009 +0100
+++ b/src/HOL/SAT.thy Fri Mar 13 23:56:07 2009 +0100
@@ -28,10 +28,10 @@
ML {* structure sat = SATFunc(structure cnf = cnf); *}
-method_setup sat = {* Method.no_args (Method.SIMPLE_METHOD' sat.sat_tac) *}
+method_setup sat = {* Method.no_args (SIMPLE_METHOD' sat.sat_tac) *}
"SAT solver"
-method_setup satx = {* Method.no_args (Method.SIMPLE_METHOD' sat.satx_tac) *}
+method_setup satx = {* Method.no_args (SIMPLE_METHOD' sat.satx_tac) *}
"SAT solver (with definitional CNF)"
end
--- a/src/HOL/SET-Protocol/EventSET.thy Fri Mar 13 19:18:07 2009 +0100
+++ b/src/HOL/SET-Protocol/EventSET.thy Fri Mar 13 23:56:07 2009 +0100
@@ -189,7 +189,7 @@
*}
method_setup analz_mono_contra = {*
- Method.no_args (Method.SIMPLE_METHOD (REPEAT_FIRST analz_mono_contra_tac)) *}
+ Method.no_args (SIMPLE_METHOD (REPEAT_FIRST analz_mono_contra_tac)) *}
"for proving theorems of the form X \<notin> analz (knows Spy evs) --> P"
end
--- a/src/HOL/SET-Protocol/MessageSET.thy Fri Mar 13 19:18:07 2009 +0100
+++ b/src/HOL/SET-Protocol/MessageSET.thy Fri Mar 13 23:56:07 2009 +0100
@@ -941,17 +941,17 @@
method_setup spy_analz = {*
Method.ctxt_args (fn ctxt =>
- Method.SIMPLE_METHOD' (MessageSET.gen_spy_analz_tac (local_clasimpset_of ctxt))) *}
+ SIMPLE_METHOD' (MessageSET.gen_spy_analz_tac (local_clasimpset_of ctxt))) *}
"for proving the Fake case when analz is involved"
method_setup atomic_spy_analz = {*
Method.ctxt_args (fn ctxt =>
- Method.SIMPLE_METHOD' (MessageSET.atomic_spy_analz_tac (local_clasimpset_of ctxt))) *}
+ SIMPLE_METHOD' (MessageSET.atomic_spy_analz_tac (local_clasimpset_of ctxt))) *}
"for debugging spy_analz"
method_setup Fake_insert_simp = {*
Method.ctxt_args (fn ctxt =>
- Method.SIMPLE_METHOD' (MessageSET.Fake_insert_simp_tac (local_simpset_of ctxt))) *}
+ SIMPLE_METHOD' (MessageSET.Fake_insert_simp_tac (local_simpset_of ctxt))) *}
"for debugging spy_analz"
end
--- a/src/HOL/SET-Protocol/PublicSET.thy Fri Mar 13 19:18:07 2009 +0100
+++ b/src/HOL/SET-Protocol/PublicSET.thy Fri Mar 13 23:56:07 2009 +0100
@@ -372,7 +372,7 @@
method_setup possibility = {*
Method.ctxt_args (fn ctxt =>
- Method.SIMPLE_METHOD (PublicSET.gen_possibility_tac (local_simpset_of ctxt))) *}
+ SIMPLE_METHOD (PublicSET.gen_possibility_tac (local_simpset_of ctxt))) *}
"for proving possibility theorems"
--- a/src/HOL/Statespace/state_space.ML Fri Mar 13 19:18:07 2009 +0100
+++ b/src/HOL/Statespace/state_space.ML Fri Mar 13 23:56:07 2009 +0100
@@ -149,7 +149,7 @@
thy
|> Expression.sublocale_cmd name expr
|> Proof.global_terminal_proof
- (Method.Basic (fn ctxt => Method.SIMPLE_METHOD (ctxt_tac ctxt),Position.none), NONE)
+ (Method.Basic (fn ctxt => SIMPLE_METHOD (ctxt_tac ctxt),Position.none), NONE)
|> ProofContext.theory_of
fun add_locale name expr elems thy =
--- a/src/HOL/Tools/function_package/auto_term.ML Fri Mar 13 19:18:07 2009 +0100
+++ b/src/HOL/Tools/function_package/auto_term.ML Fri Mar 13 23:56:07 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", (Method.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_common.ML Fri Mar 13 19:18:07 2009 +0100
+++ b/src/HOL/Tools/function_package/fundef_common.ML Fri Mar 13 23:56:07 2009 +0100
@@ -155,7 +155,7 @@
structure TerminationProver = GenericDataFun
(
- type T = (Proof.context -> Method.method)
+ type T = Proof.context -> Proof.method
val empty = (fn _ => error "Termination prover not configured")
val extend = I
fun merge _ (a,b) = b (* FIXME *)
--- a/src/HOL/Tools/function_package/fundef_datatype.ML Fri Mar 13 19:18:07 2009 +0100
+++ b/src/HOL/Tools/function_package/fundef_datatype.ML Fri Mar 13 23:56:07 2009 +0100
@@ -203,7 +203,7 @@
handle COMPLETENESS => no_tac)
-fun pat_completeness ctxt = Method.SIMPLE_METHOD' (pat_completeness_tac ctxt)
+fun pat_completeness ctxt = SIMPLE_METHOD' (pat_completeness_tac ctxt)
val by_pat_completeness_auto =
Proof.global_future_terminal_proof
@@ -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 19:18:07 2009 +0100
+++ b/src/HOL/Tools/function_package/induction_scheme.ML Fri Mar 13 23:56:07 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 (Method.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/function_package/lexicographic_order.ML Fri Mar 13 19:18:07 2009 +0100
+++ b/src/HOL/Tools/function_package/lexicographic_order.ML Fri Mar 13 23:56:07 2009 +0100
@@ -218,7 +218,7 @@
TRY (FundefCommon.apply_termination_rule ctxt 1)
THEN lex_order_tac ctxt (auto_tac (local_clasimpset_of ctxt addsimps2 FundefCommon.TerminationSimps.get ctxt))
-val lexicographic_order = Method.SIMPLE_METHOD o lexicographic_order_tac
+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")]
--- a/src/HOL/Tools/function_package/scnp_reconstruct.ML Fri Mar 13 19:18:07 2009 +0100
+++ b/src/HOL/Tools/function_package/scnp_reconstruct.ML Fri Mar 13 23:56:07 2009 +0100
@@ -10,7 +10,7 @@
val sizechange_tac : Proof.context -> tactic -> tactic
- val decomp_scnp : ScnpSolve.label list -> Proof.context -> method
+ val decomp_scnp : ScnpSolve.label list -> Proof.context -> Proof.method
val setup : theory -> theory
@@ -408,7 +408,7 @@
val extra_simps = FundefCommon.TerminationSimps.get ctxt
val autom_tac = auto_tac (local_clasimpset_of ctxt addsimps2 extra_simps)
in
- Method.SIMPLE_METHOD
+ SIMPLE_METHOD
(gen_sizechange_tac orders autom_tac ctxt (print_error ctxt))
end
--- a/src/HOL/Tools/inductive_package.ML Fri Mar 13 19:18:07 2009 +0100
+++ b/src/HOL/Tools/inductive_package.ML Fri Mar 13 23:56:07 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 19:18:07 2009 +0100
+++ b/src/HOL/Tools/lin_arith.ML Fri Mar 13 23:56:07 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.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 19:18:07 2009 +0100
+++ b/src/HOL/Tools/metis_tools.ML Fri Mar 13 23:56:07 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 =>
- Method.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 (Method.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 19:18:07 2009 +0100
+++ b/src/HOL/Tools/res_axioms.ML Fri Mar 13 23:56:07 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 =>
- Method.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 (Method.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/HOL/Transitive_Closure.thy Fri Mar 13 19:18:07 2009 +0100
+++ b/src/HOL/Transitive_Closure.thy Fri Mar 13 23:56:07 2009 +0100
@@ -695,16 +695,16 @@
(* Optional methods *)
method_setup trancl =
- {* Method.no_args (Method.SIMPLE_METHOD' Trancl_Tac.trancl_tac) *}
+ {* Method.no_args (SIMPLE_METHOD' Trancl_Tac.trancl_tac) *}
{* simple transitivity reasoner *}
method_setup rtrancl =
- {* Method.no_args (Method.SIMPLE_METHOD' Trancl_Tac.rtrancl_tac) *}
+ {* Method.no_args (SIMPLE_METHOD' Trancl_Tac.rtrancl_tac) *}
{* simple transitivity reasoner *}
method_setup tranclp =
- {* Method.no_args (Method.SIMPLE_METHOD' Tranclp_Tac.trancl_tac) *}
+ {* Method.no_args (SIMPLE_METHOD' Tranclp_Tac.trancl_tac) *}
{* simple transitivity reasoner (predicate version) *}
method_setup rtranclp =
- {* Method.no_args (Method.SIMPLE_METHOD' Tranclp_Tac.rtrancl_tac) *}
+ {* Method.no_args (SIMPLE_METHOD' Tranclp_Tac.rtrancl_tac) *}
{* simple transitivity reasoner (predicate version) *}
end
--- a/src/HOL/UNITY/Comp/Alloc.thy Fri Mar 13 19:18:07 2009 +0100
+++ b/src/HOL/UNITY/Comp/Alloc.thy Fri Mar 13 23:56:07 2009 +0100
@@ -321,7 +321,7 @@
*}
method_setup record_auto = {*
- Method.ctxt_args (fn ctxt => Method.SIMPLE_METHOD (record_auto_tac (local_clasimpset_of ctxt)))
+ Method.ctxt_args (fn ctxt => SIMPLE_METHOD (record_auto_tac (local_clasimpset_of ctxt)))
*} ""
lemma inj_sysOfAlloc [iff]: "inj sysOfAlloc"
@@ -714,7 +714,7 @@
method_setup rename_client_map = {*
Method.ctxt_args (fn ctxt =>
- Method.SIMPLE_METHOD (rename_client_map_tac (local_simpset_of ctxt)))
+ SIMPLE_METHOD (rename_client_map_tac (local_simpset_of ctxt)))
*} ""
text{*Lifting @{text Client_Increasing} to @{term systemState}*}
--- a/src/HOL/UNITY/Simple/NSP_Bad.thy Fri Mar 13 19:18:07 2009 +0100
+++ b/src/HOL/UNITY/Simple/NSP_Bad.thy Fri Mar 13 23:56:07 2009 +0100
@@ -125,7 +125,7 @@
method_setup ns_induct = {*
Method.ctxt_args (fn ctxt =>
- Method.SIMPLE_METHOD' (ns_induct_tac (local_clasimpset_of ctxt))) *}
+ SIMPLE_METHOD' (ns_induct_tac (local_clasimpset_of ctxt))) *}
"for inductive reasoning about the Needham-Schroeder protocol"
text{*Converts invariants into statements about reachable states*}
--- a/src/HOL/UNITY/UNITY_Main.thy Fri Mar 13 19:18:07 2009 +0100
+++ b/src/HOL/UNITY/UNITY_Main.thy Fri Mar 13 23:56:07 2009 +0100
@@ -11,7 +11,7 @@
method_setup safety = {*
Method.ctxt_args (fn ctxt =>
- Method.SIMPLE_METHOD' (constrains_tac (local_clasimpset_of ctxt))) *}
+ SIMPLE_METHOD' (constrains_tac (local_clasimpset_of ctxt))) *}
"for proving safety properties"
method_setup ensures_tac = {*
--- a/src/HOL/Word/WordArith.thy Fri Mar 13 19:18:07 2009 +0100
+++ b/src/HOL/Word/WordArith.thy Fri Mar 13 23:56:07 2009 +0100
@@ -530,7 +530,7 @@
*}
method_setup uint_arith =
- "Method.ctxt_args (fn ctxt => Method.SIMPLE_METHOD (uint_arith_tac ctxt 1))"
+ "Method.ctxt_args (SIMPLE_METHOD' o uint_arith_tac)"
"solving word arithmetic via integers and arith"
@@ -1086,7 +1086,7 @@
*}
method_setup unat_arith =
- "Method.ctxt_args (fn ctxt => Method.SIMPLE_METHOD (unat_arith_tac ctxt 1))"
+ "Method.ctxt_args (SIMPLE_METHOD' o unat_arith_tac)"
"solving word arithmetic via natural numbers and arith"
lemma no_plus_overflow_unat_size:
--- a/src/HOL/ex/Binary.thy Fri Mar 13 19:18:07 2009 +0100
+++ b/src/HOL/ex/Binary.thy Fri Mar 13 23:56:07 2009 +0100
@@ -174,7 +174,7 @@
simproc_setup binary_nat_mod ("m mod (n::nat)") = {* K (divmod_proc @{thm binary_divmod(2)}) *}
method_setup binary_simp = {*
- Method.no_args (Method.SIMPLE_METHOD'
+ Method.no_args (SIMPLE_METHOD'
(full_simp_tac
(HOL_basic_ss
addsimps @{thms binary_simps}
--- a/src/HOL/ex/SAT_Examples.thy Fri Mar 13 19:18:07 2009 +0100
+++ b/src/HOL/ex/SAT_Examples.thy Fri Mar 13 23:56:07 2009 +0100
@@ -83,7 +83,7 @@
ML {* reset quick_and_dirty; *}
method_setup rawsat =
- {* Method.no_args (Method.SIMPLE_METHOD' sat.rawsat_tac) *}
+ {* Method.no_args (SIMPLE_METHOD' sat.rawsat_tac) *}
"SAT solver (no preprocessing)"
(* ML {* Toplevel.profiling := 1; *} *)
--- a/src/Provers/blast.ML Fri Mar 13 19:18:07 2009 +0100
+++ b/src/Provers/blast.ML Fri Mar 13 23:56:07 2009 +0100
@@ -56,7 +56,7 @@
uwrappers: (string * wrapper) list,
safe0_netpair: netpair, safep_netpair: netpair,
haz_netpair: netpair, dup_netpair: netpair, xtra_netpair: ContextRules.netpair}
- val cla_modifiers: (Args.T list -> (Method.modifier * Args.T list)) list
+ val cla_modifiers: Method.modifier parser list
val cla_meth': (claset -> int -> tactic) -> thm list -> Proof.context -> Proof.method
end;
--- a/src/Provers/clasimp.ML Fri Mar 13 19:18:07 2009 +0100
+++ b/src/Provers/clasimp.ML Fri Mar 13 23:56:07 2009 +0100
@@ -62,8 +62,8 @@
val iff_add: attribute
val iff_add': attribute
val iff_del: attribute
- val iff_modifiers: (Args.T list -> (Method.modifier * Args.T list)) list
- val clasimp_modifiers: (Args.T list -> (Method.modifier * Args.T list)) list
+ val iff_modifiers: Method.modifier parser list
+ val clasimp_modifiers: Method.modifier parser list
val clasimp_setup: theory -> theory
end;
@@ -290,10 +290,10 @@
(* methods *)
-fun clasimp_meth tac prems ctxt = Method.METHOD (fn facts =>
+fun clasimp_meth tac prems ctxt = METHOD (fn facts =>
ALLGOALS (Method.insert_tac (prems @ facts)) THEN tac (local_clasimpset_of ctxt));
-fun clasimp_meth' tac prems ctxt = Method.METHOD (fn facts =>
+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;
--- a/src/Provers/classical.ML Fri Mar 13 19:18:07 2009 +0100
+++ b/src/Provers/classical.ML Fri Mar 13 23:56:07 2009 +0100
@@ -146,7 +146,7 @@
val haz_elim: int option -> attribute
val haz_intro: int option -> attribute
val rule_del: attribute
- val cla_modifiers: (Args.T list -> (Method.modifier * Args.T list)) list
+ 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
@@ -971,11 +971,8 @@
(** proof methods **)
-fun METHOD_CLASET tac ctxt =
- Method.METHOD (tac ctxt (local_claset_of ctxt));
-
-fun METHOD_CLASET' tac ctxt =
- Method.METHOD (HEADGOAL o tac ctxt (local_claset_of ctxt));
+fun METHOD_CLASET tac ctxt = METHOD (tac ctxt (local_claset_of ctxt));
+fun METHOD_CLASET' tac ctxt = METHOD (HEADGOAL o tac ctxt (local_claset_of ctxt));
local
@@ -1021,10 +1018,10 @@
Args.$$$ introN -- Args.colon >> K (I, haz_intro NONE),
Args.del -- Args.colon >> K (I, rule_del)];
-fun cla_meth tac prems ctxt = Method.METHOD (fn facts =>
+fun cla_meth tac prems ctxt = METHOD (fn facts =>
ALLGOALS (Method.insert_tac (prems @ facts)) THEN tac (local_claset_of ctxt));
-fun cla_meth' tac prems ctxt = Method.METHOD (fn facts =>
+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;
--- a/src/Provers/hypsubst.ML Fri Mar 13 19:18:07 2009 +0100
+++ b/src/Provers/hypsubst.ML Fri Mar 13 23:56:07 2009 +0100
@@ -284,9 +284,10 @@
(* theory setup *)
val hypsubst_setup =
- Method.add_methods
- [("hypsubst", Method.no_args (Method.SIMPLE_METHOD' (CHANGED_PROP o hyp_subst_tac)),
- "substitution using an assumption (improper)"),
- ("simplesubst", Method.thm_args (Method.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 19:18:07 2009 +0100
+++ b/src/Provers/splitter.ML Fri Mar 13 23:56:07 2009 +0100
@@ -39,7 +39,7 @@
val Delsplits : thm list -> unit
val split_add: attribute
val split_del: attribute
- val split_modifiers : (Args.T list -> (Method.modifier * Args.T list)) list
+ val split_modifiers : Method.modifier parser list
val setup: theory -> theory
end;
@@ -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, _) => Method.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/args.ML Fri Mar 13 19:18:07 2009 +0100
+++ b/src/Pure/Isar/args.ML Fri Mar 13 23:56:07 2009 +0100
@@ -7,69 +7,66 @@
signature ARGS =
sig
- type T = OuterLex.token
+ type token = OuterLex.token
type src
- val src: (string * T list) * Position.T -> src
- val dest_src: src -> (string * T list) * Position.T
+ val src: (string * token list) * Position.T -> src
+ val dest_src: src -> (string * token list) * Position.T
val pretty_src: Proof.context -> src -> Pretty.T
val map_name: (string -> string) -> src -> src
val morph_values: morphism -> src -> src
val maxidx_values: src -> int -> int
val assignable: src -> src
val closure: src -> src
- val context: Context.generic * T list -> Context.proof * (Context.generic * T list)
- val theory: Context.generic * T list -> Context.theory * (Context.generic * T list)
- val $$$ : string -> T list -> string * T list
- val add: T list -> string * T list
- val del: T list -> string * T list
- val colon: T list -> string * T list
- val query: T list -> string * T list
- val bang: T list -> string * T list
- val query_colon: T list -> string * T list
- val bang_colon: T list -> string * T list
- val parens: (T list -> 'a * T list) -> T list -> 'a * T list
- val bracks: (T list -> 'a * T list) -> T list -> 'a * T list
- val mode: string -> 'a * T list -> bool * ('a * T list)
- val maybe: (T list -> 'a * T list) -> T list -> 'a option * T list
- val name_source: T list -> string * T list
- val name_source_position: T list -> (SymbolPos.text * Position.T) * T list
- val name: T list -> string * T list
- val binding: T list -> binding * T list
- val alt_name: T list -> string * T list
- val symbol: T list -> string * T list
- val liberal_name: T list -> string * T list
- val var: T list -> indexname * T list
- val internal_text: T list -> string * T list
- val internal_typ: T list -> typ * T list
- val internal_term: T list -> term * T list
- val internal_fact: T list -> thm list * T list
- val internal_attribute: T list -> (morphism -> attribute) * T list
- val named_text: (string -> string) -> T list -> string * T list
- val named_typ: (string -> typ) -> T list -> typ * T list
- val named_term: (string -> term) -> T list -> term * T list
- val named_fact: (string -> thm list) -> T list -> thm list * T list
- val named_attribute: (string -> morphism -> attribute) -> T list ->
- (morphism -> attribute) * T list
- val typ_abbrev: Context.generic * T list -> typ * (Context.generic * T list)
- val typ: Context.generic * T list -> typ * (Context.generic * T list)
- val term: Context.generic * T list -> term * (Context.generic * T list)
- val term_abbrev: Context.generic * T list -> term * (Context.generic * T list)
- val prop: Context.generic * T list -> term * (Context.generic * T list)
- val tyname: Context.generic * T list -> string * (Context.generic * T list)
- val const: Context.generic * T list -> string * (Context.generic * T list)
- val const_proper: Context.generic * T list -> string * (Context.generic * T list)
- val bang_facts: Context.generic * T list -> thm list * (Context.generic * T list)
- val goal_spec: ((int -> tactic) -> tactic) -> ('a * T list)
- -> ((int -> tactic) -> tactic) * ('a * T list)
- val parse: OuterLex.token list -> T list * OuterLex.token list
- val parse1: (string -> bool) -> OuterLex.token list -> T list * OuterLex.token list
- val attribs: (string -> string) -> T list -> src list * T list
- val opt_attribs: (string -> string) -> T list -> src list * T list
- val thm_name: (string -> string) -> string -> T list -> (binding * src list) * T list
- val opt_thm_name: (string -> string) -> string -> T list -> (binding * src list) * T list
- val syntax: string -> ('b * T list -> 'a * ('b * T list)) -> src -> 'b -> 'a * 'b
- val context_syntax: string -> (Context.generic * T list -> 'a * (Context.generic * T list)) ->
- src -> Proof.context -> 'a * Proof.context
+ val context: Proof.context context_parser
+ val theory: theory context_parser
+ val $$$ : string -> string parser
+ val add: string parser
+ val del: string parser
+ val colon: string parser
+ val query: string parser
+ val bang: string parser
+ val query_colon: string parser
+ val bang_colon: string parser
+ val parens: ('a parser) -> 'a parser
+ val bracks: ('a parser) -> 'a parser
+ val mode: string -> bool context_parser
+ val maybe: 'a parser -> 'a option parser
+ val name_source: string parser
+ val name_source_position: (SymbolPos.text * Position.T) parser
+ val name: string parser
+ val binding: binding parser
+ val alt_name: string parser
+ val symbol: string parser
+ val liberal_name: string parser
+ val var: indexname parser
+ val internal_text: string parser
+ val internal_typ: typ parser
+ val internal_term: term parser
+ val internal_fact: thm list parser
+ val internal_attribute: (morphism -> attribute) parser
+ val named_text: (string -> string) -> string parser
+ val named_typ: (string -> typ) -> typ parser
+ val named_term: (string -> term) -> term parser
+ val named_fact: (string -> thm list) -> thm list parser
+ val named_attribute: (string -> morphism -> attribute) -> (morphism -> attribute) parser
+ val typ_abbrev: typ context_parser
+ val typ: typ context_parser
+ val term: term context_parser
+ val term_abbrev: term context_parser
+ val prop: term context_parser
+ val tyname: string context_parser
+ val const: string context_parser
+ val const_proper: string context_parser
+ val bang_facts: thm list context_parser
+ val goal_spec: ((int -> tactic) -> tactic) context_parser
+ val parse: token list parser
+ val parse1: (string -> bool) -> token list parser
+ val attribs: (string -> string) -> src list parser
+ val opt_attribs: (string -> string) -> src list parser
+ val thm_name: (string -> string) -> string -> (binding * src list) parser
+ val opt_thm_name: (string -> string) -> string -> (binding * src list) parser
+ val syntax: string -> 'a context_parser -> src -> Context.generic -> 'a * Context.generic
+ val context_syntax: string -> 'a context_parser -> src -> Proof.context -> 'a * Proof.context
end;
structure Args: ARGS =
@@ -78,13 +75,13 @@
structure T = OuterLex;
structure P = OuterParse;
+type token = T.token;
+
(** datatype src **)
-type T = T.token;
-
-datatype src = Src of (string * T list) * Position.T;
+datatype src = Src of (string * token list) * Position.T;
val src = Src;
fun dest_src (Src src) = src;
@@ -236,7 +233,7 @@
$$$ "!" >> K ALLGOALS;
val goal = $$$ "[" |-- P.!!! (from_to --| $$$ "]");
-fun goal_spec def = Scan.lift (Scan.optional goal def);
+fun goal_spec x = Scan.lift (Scan.optional goal (fn tac => tac 1)) x;
(* arguments within outer syntax *)
--- a/src/Pure/Isar/attrib.ML Fri Mar 13 19:18:07 2009 +0100
+++ b/src/Pure/Isar/attrib.ML Fri Mar 13 23:56:07 2009 +0100
@@ -24,14 +24,13 @@
(('c * 'att list) * ('d * 'att list) list) list
val crude_closure: Proof.context -> src -> src
val add_attributes: (bstring * (src -> attribute) * string) list -> theory -> theory
- val syntax: (Context.generic * Args.T list ->
- attribute * (Context.generic * Args.T list)) -> src -> attribute
+ val syntax: attribute context_parser -> src -> attribute
val no_args: attribute -> src -> attribute
val add_del_args: attribute -> attribute -> src -> attribute
- val thm_sel: Args.T list -> Facts.interval list * Args.T list
- val thm: Context.generic * Args.T list -> thm * (Context.generic * Args.T list)
- val thms: Context.generic * Args.T list -> thm list * (Context.generic * Args.T list)
- val multi_thm: Context.generic * Args.T list -> thm list * (Context.generic * Args.T list)
+ val thm_sel: Facts.interval list parser
+ val thm: thm context_parser
+ val thms: thm list context_parser
+ val multi_thm: thm list context_parser
val print_configs: Proof.context -> unit
val internal: (morphism -> attribute) -> src
val register_config: Config.value Config.T -> theory -> theory
--- a/src/Pure/Isar/class_target.ML Fri Mar 13 19:18:07 2009 +0100
+++ b/src/Pure/Isar/class_target.ML Fri Mar 13 23:56:07 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.METHOD intro_classes_tac),
- "back-chain introduction rules of classes"),
- ("default", Method.thms_ctxt_args (Method.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/code.ML Fri Mar 13 19:18:07 2009 +0100
+++ b/src/Pure/Isar/code.ML Fri Mar 13 23:56:07 2009 +0100
@@ -44,7 +44,7 @@
val postprocess_conv: theory -> cterm -> thm
val postprocess_term: theory -> term -> term
- val add_attribute: string * (Args.T list -> attribute * Args.T list) -> theory -> theory
+ val add_attribute: string * attribute parser -> theory -> theory
val print_codesetup: theory -> unit
end;
@@ -83,7 +83,7 @@
(** code attributes **)
structure CodeAttr = TheoryDataFun (
- type T = (string * (Args.T list -> attribute * Args.T list)) list;
+ type T = (string * attribute parser) list;
val empty = [];
val copy = I;
val extend = I;
--- a/src/Pure/Isar/element.ML Fri Mar 13 19:18:07 2009 +0100
+++ b/src/Pure/Isar/element.ML Fri Mar 13 23:56:07 2009 +0100
@@ -268,7 +268,7 @@
local
val refine_witness =
- Proof.refine (Method.Basic (K (Method.RAW_METHOD
+ Proof.refine (Method.Basic (K (RAW_METHOD
(K (ALLGOALS
(CONJUNCTS (ALLGOALS
(CONJUNCTS (TRYALL (Tactic.rtac Drule.protectI)))))))), Position.none));
--- a/src/Pure/Isar/locale.ML Fri Mar 13 19:18:07 2009 +0100
+++ b/src/Pure/Isar/locale.ML Fri Mar 13 23:56:07 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.METHOD (intro_locales_tac false ctxt)),
- "back-chain introduction rules of locales without unfolding predicates"),
- ("unfold_locales",
- Method.ctxt_args (fn ctxt => Method.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 19:18:07 2009 +0100
+++ b/src/Pure/Isar/method.ML Fri Mar 13 23:56:07 2009 +0100
@@ -8,13 +8,13 @@
sig
val FINDGOAL: (int -> thm -> 'a Seq.seq) -> thm -> 'a Seq.seq
val HEADGOAL: (int -> thm -> 'a Seq.seq) -> thm -> 'a Seq.seq
- type method
val trace_rules: bool ref
end;
signature METHOD =
sig
include BASIC_METHOD
+ type method
val apply: Position.T -> (Proof.context -> method) -> Proof.context -> thm list -> cases_tactic
val RAW_METHOD_CASES: (thm list -> cases_tactic) -> method
val RAW_METHOD: (thm list -> tactic) -> method
@@ -78,40 +78,31 @@
-> theory -> theory
val add_method: bstring * (src -> Proof.context -> method) * string
-> theory -> theory
+ val syntax: 'a context_parser -> src -> Proof.context -> 'a * Proof.context
+ val setup: binding -> (Proof.context -> method) context_parser -> string -> theory -> theory
val method_setup: bstring -> string * Position.T -> string -> theory -> theory
- val syntax: (Context.generic * Args.T list -> 'a * (Context.generic * Args.T list))
- -> src -> Proof.context -> 'a * Proof.context
- val simple_args: (Args.T list -> 'a * Args.T list)
- -> ('a -> Proof.context -> method) -> src -> Proof.context -> method
+ val simple_args: 'a parser -> ('a -> Proof.context -> method) -> src -> Proof.context -> method
val ctxt_args: (Proof.context -> method) -> src -> Proof.context -> method
val no_args: method -> src -> Proof.context -> method
type modifier
- val sectioned_args: (Context.generic * Args.T list -> 'a * (Context.generic * Args.T list)) ->
- (Args.T list -> modifier * Args.T list) list ->
+ val sectioned_args: 'a context_parser -> modifier parser list ->
('a -> Proof.context -> 'b) -> src -> Proof.context -> 'b
- val bang_sectioned_args:
- (Args.T list -> modifier * Args.T list) list ->
+ val bang_sectioned_args: modifier parser list ->
(thm list -> Proof.context -> 'a) -> src -> Proof.context -> 'a
- val bang_sectioned_args':
- (Args.T list -> modifier * Args.T list) list ->
- (Context.generic * Args.T list -> 'a * (Context.generic * Args.T list)) ->
+ val bang_sectioned_args': modifier parser list -> 'a context_parser ->
('a -> thm list -> Proof.context -> 'b) -> src -> Proof.context -> 'b
- val only_sectioned_args:
- (Args.T list -> modifier * Args.T list) list ->
- (Proof.context -> 'a) -> src -> Proof.context -> 'a
- val thms_ctxt_args: (thm list -> Proof.context -> 'a) -> src ->
+ val only_sectioned_args: modifier parser list -> (Proof.context -> 'a) -> src ->
Proof.context -> 'a
+ val thms_ctxt_args: (thm list -> Proof.context -> 'a) -> src -> Proof.context -> 'a
val thms_args: (thm list -> 'a) -> src -> Proof.context -> 'a
val thm_args: (thm -> 'a) -> src -> Proof.context -> 'a
- val goal_args: (Args.T list -> 'a * Args.T list) -> ('a -> int -> tactic)
- -> src -> Proof.context -> method
- val goal_args': (Context.generic * Args.T list -> 'a * (Context.generic * Args.T list))
- -> ('a -> int -> tactic) -> src -> Proof.context -> method
- val goal_args_ctxt: (Args.T list -> 'a * Args.T list) ->
- (Proof.context -> 'a -> int -> tactic) -> src -> Proof.context -> method
- val goal_args_ctxt': (Context.generic * Args.T list -> 'a * (Context.generic * Args.T list)) ->
- (Proof.context -> 'a -> int -> tactic) -> src -> Proof.context -> method
- val parse: OuterLex.token list -> text * OuterLex.token list
+ val goal_args: 'a parser -> ('a -> int -> tactic) -> src -> Proof.context -> method
+ val goal_args': 'a context_parser -> ('a -> int -> tactic) -> src -> Proof.context -> method
+ val goal_args_ctxt: 'a parser -> (Proof.context -> 'a -> int -> tactic) -> src ->
+ Proof.context -> method
+ val goal_args_ctxt': 'a context_parser -> (Proof.context -> 'a -> int -> tactic) -> src ->
+ Proof.context -> method
+ val parse: text parser
end;
structure Method: METHOD =
@@ -401,7 +392,13 @@
val add_method = add_methods o Library.single;
-(* method_setup *)
+(* method setup *)
+
+fun syntax scan = Args.context_syntax "method" scan;
+
+fun setup name scan comment =
+ add_methods [(Binding.name_of name,
+ fn src => fn ctxt => let val (m, ctxt') = syntax scan src ctxt in m ctxt' end, comment)];
fun method_setup name (txt, pos) cmt =
Context.theory_map (ML_Context.expression pos
@@ -418,8 +415,6 @@
(* basic *)
-fun syntax scan = Args.context_syntax "method" scan;
-
fun simple_args scan f src ctxt : method =
fst (syntax (Scan.lift (scan >> (fn x => f x ctxt))) src ctxt);
@@ -461,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;
@@ -505,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!*)
@@ -540,3 +546,12 @@
structure BasicMethod: BASIC_METHOD = Method;
open BasicMethod;
+
+val RAW_METHOD_CASES = Method.RAW_METHOD_CASES;
+val RAW_METHOD = Method.RAW_METHOD;
+val METHOD_CASES = Method.METHOD_CASES;
+val METHOD = Method.METHOD;
+val SIMPLE_METHOD = Method.SIMPLE_METHOD;
+val SIMPLE_METHOD' = Method.SIMPLE_METHOD';
+val SIMPLE_METHOD'' = Method.SIMPLE_METHOD'';
+
--- a/src/Pure/Isar/outer_parse.ML Fri Mar 13 19:18:07 2009 +0100
+++ b/src/Pure/Isar/outer_parse.ML Fri Mar 13 23:56:07 2009 +0100
@@ -8,6 +8,7 @@
sig
type token = OuterLex.token
type 'a parser = token list -> 'a * token list
+ type 'a context_parser = Context.generic * token list -> 'a * (Context.generic * token list)
val group: string -> (token list -> 'a) -> token list -> 'a
val !!! : (token list -> 'a) -> token list -> 'a
val !!!! : (token list -> 'a) -> token list -> 'a
@@ -50,14 +51,10 @@
val enum1: string -> 'a parser -> 'a list parser
val and_list: 'a parser -> 'a list parser
val and_list1: 'a parser -> 'a list parser
- val enum': string -> ('a * token list -> 'b * ('a * token list)) ->
- 'a * token list -> 'b list * ('a * token list)
- val enum1': string -> ('a * token list -> 'b * ('a * token list)) ->
- 'a * token list -> 'b list * ('a * token list)
- val and_list': ('a * token list -> 'b * ('a * token list)) ->
- 'a * token list -> 'b list * ('a * token list)
- val and_list1': ('a * token list -> 'b * ('a * token list)) ->
- 'a * token list -> 'b list * ('a * token list)
+ val enum': string -> 'a context_parser -> 'a list context_parser
+ val enum1': string -> 'a context_parser -> 'a list context_parser
+ val and_list': 'a context_parser -> 'a list context_parser
+ val and_list1': 'a context_parser -> 'a list context_parser
val list: 'a parser -> 'a list parser
val list1: 'a parser -> 'a list parser
val name: bstring parser
@@ -106,6 +103,7 @@
type token = T.token;
type 'a parser = token list -> 'a * token list;
+type 'a context_parser = Context.generic * token list -> 'a * (Context.generic * token list);
(** error handling **)
@@ -339,3 +337,7 @@
val opt_target = Scan.option target;
end;
+
+type 'a parser = 'a OuterParse.parser;
+type 'a context_parser = 'a OuterParse.context_parser;
+
--- a/src/Pure/Isar/outer_syntax.ML Fri Mar 13 19:18:07 2009 +0100
+++ b/src/Pure/Isar/outer_syntax.ML Fri Mar 13 23:56:07 2009 +0100
@@ -9,7 +9,6 @@
signature OUTER_SYNTAX =
sig
- type 'a parser = 'a OuterParse.parser
val command: string -> string -> OuterKeyword.T ->
(Toplevel.transition -> Toplevel.transition) parser -> unit
val markup_command: ThyOutput.markup -> string -> string -> OuterKeyword.T ->
--- a/src/Pure/Isar/proof.ML Fri Mar 13 19:18:07 2009 +0100
+++ b/src/Pure/Isar/proof.ML Fri Mar 13 23:56:07 2009 +0100
@@ -780,7 +780,7 @@
in (rev vars, props') end;
fun refine_terms n =
- refine (Method.Basic (K (Method.RAW_METHOD
+ refine (Method.Basic (K (RAW_METHOD
(K (HEADGOAL (PRECISE_CONJUNCTS n
(HEADGOAL (CONJUNCTS (ALLGOALS (rtac Drule.termI)))))))), Position.none))
#> Seq.hd;
--- a/src/Pure/Isar/rule_insts.ML Fri Mar 13 19:18:07 2009 +0100
+++ b/src/Pure/Isar/rule_insts.ML Fri Mar 13 23:56:07 2009 +0100
@@ -386,61 +386,48 @@
local
-fun gen_inst _ tac _ (quant, ([], thms)) =
- Method.METHOD (fn facts => quant (Method.insert_tac facts THEN' tac thms))
- | gen_inst inst_tac _ ctxt (quant, (insts, [thm])) =
- Method.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/Pure/Isar/spec_parse.ML Fri Mar 13 19:18:07 2009 +0100
+++ b/src/Pure/Isar/spec_parse.ML Fri Mar 13 23:56:07 2009 +0100
@@ -6,8 +6,6 @@
signature SPEC_PARSE =
sig
- type token = OuterParse.token
- type 'a parser = 'a OuterParse.parser
val attrib: Attrib.src parser
val attribs: Attrib.src list parser
val opt_attribs: Attrib.src list parser
@@ -36,8 +34,6 @@
struct
structure P = OuterParse;
-type token = P.token;
-type 'a parser = 'a P.parser;
(* theorem specifications *)
--- a/src/Pure/Isar/value_parse.ML Fri Mar 13 19:18:07 2009 +0100
+++ b/src/Pure/Isar/value_parse.ML Fri Mar 13 23:56:07 2009 +0100
@@ -6,7 +6,6 @@
signature VALUE_PARSE =
sig
- type 'a parser = 'a OuterParse.parser
val comma: 'a parser -> 'a parser
val equal: 'a parser -> 'a parser
val parens: 'a parser -> 'a parser
@@ -20,7 +19,6 @@
struct
structure P = OuterParse;
-type 'a parser = 'a P.parser;
(* syntax utilities *)
--- a/src/Pure/ML/ml_antiquote.ML Fri Mar 13 19:18:07 2009 +0100
+++ b/src/Pure/ML/ml_antiquote.ML Fri Mar 13 23:56:07 2009 +0100
@@ -6,15 +6,11 @@
signature ML_ANTIQUOTE =
sig
- val macro: string ->
- (Context.generic * Args.T list -> Proof.context * (Context.generic * Args.T list)) -> unit
+ val macro: string -> Proof.context context_parser -> unit
val variant: string -> Proof.context -> string * Proof.context
- val inline: string ->
- (Context.generic * Args.T list -> string * (Context.generic * Args.T list)) -> unit
- val declaration: string -> string ->
- (Context.generic * Args.T list -> string * (Context.generic * Args.T list)) -> unit
- val value: string ->
- (Context.generic * Args.T list -> string * (Context.generic * Args.T list)) -> unit
+ val inline: string -> string context_parser -> unit
+ val declaration: string -> string -> string context_parser -> unit
+ val value: string -> string context_parser -> unit
end;
structure ML_Antiquote: ML_ANTIQUOTE =
--- a/src/Pure/ML/ml_context.ML Fri Mar 13 19:18:07 2009 +0100
+++ b/src/Pure/ML/ml_context.ML Fri Mar 13 23:56:07 2009 +0100
@@ -27,8 +27,7 @@
type antiq =
{struct_name: string, background: Proof.context} ->
(Proof.context -> string * string) * Proof.context
- val add_antiq: string ->
- (Position.T -> Context.generic * Args.T list -> antiq * (Context.generic * Args.T list)) -> unit
+ val add_antiq: string -> (Position.T -> antiq context_parser) -> unit
val trace: bool ref
val eval_wrapper: (string -> unit) * (string -> 'a) -> bool -> Position.T -> string -> unit
val eval: bool -> Position.T -> string -> unit
@@ -157,9 +156,7 @@
local
-val global_parsers = ref (Symtab.empty:
- (Position.T -> Context.generic * Args.T list -> antiq * (Context.generic * Args.T list))
- Symtab.table);
+val global_parsers = ref (Symtab.empty: (Position.T -> antiq context_parser) Symtab.table);
in
--- a/src/Pure/Thy/thy_output.ML Fri Mar 13 19:18:07 2009 +0100
+++ b/src/Pure/Thy/thy_output.ML Fri Mar 13 23:56:07 2009 +0100
@@ -18,8 +18,7 @@
val print_antiquotations: unit -> unit
val boolean: string -> bool
val integer: string -> int
- val antiquotation: string ->
- (Context.generic * Args.T list -> 'a * (Context.generic * Args.T list)) ->
+ val antiquotation: string -> 'a context_parser ->
({state: Toplevel.state, source: Args.src, context: Proof.context} -> 'a -> string) -> unit
datatype markup = Markup | MarkupEnv | Verbatim
val modes: string list ref
--- a/src/Pure/simplifier.ML Fri Mar 13 19:18:07 2009 +0100
+++ b/src/Pure/simplifier.ML Fri Mar 13 23:56:07 2009 +0100
@@ -73,11 +73,10 @@
val def_simproc_i: {name: string, lhss: term list,
proc: morphism -> simpset -> cterm -> thm option, identifier: thm list} ->
local_theory -> local_theory
- val cong_modifiers: (Args.T list -> (Method.modifier * Args.T list)) list
- val simp_modifiers': (Args.T list -> (Method.modifier * Args.T list)) list
- val simp_modifiers: (Args.T list -> (Method.modifier * Args.T list)) list
- val method_setup: (Args.T list -> (Method.modifier * Args.T list)) list
- -> theory -> theory
+ val cong_modifiers: Method.modifier parser list
+ val simp_modifiers': Method.modifier parser list
+ val simp_modifiers: Method.modifier parser list
+ val method_setup: Method.modifier parser list -> theory -> theory
val easy_setup: thm -> thm list -> theory -> theory
end;
@@ -410,11 +409,11 @@
Method.sectioned_args (Args.bang_facts -- Scan.lift simp_options)
(more_mods @ simp_modifiers');
-fun simp_method (prems, tac) ctxt = Method.METHOD (fn facts =>
+fun simp_method (prems, tac) ctxt = METHOD (fn facts =>
ALLGOALS (Method.insert_tac (prems @ facts)) THEN
(CHANGED_PROP o ALLGOALS o tac) (local_simpset_of ctxt));
-fun simp_method' (prems, tac) ctxt = Method.METHOD (fn facts =>
+fun simp_method' (prems, tac) ctxt = METHOD (fn facts =>
HEADGOAL (Method.insert_tac (prems @ facts) THEN'
((CHANGED_PROP) oo tac) (local_simpset_of ctxt)));
--- a/src/Sequents/ILL.thy Fri Mar 13 19:18:07 2009 +0100
+++ b/src/Sequents/ILL.thy Fri Mar 13 23:56:07 2009 +0100
@@ -146,7 +146,7 @@
*}
method_setup best_lazy =
- {* Method.no_args (Method.SIMPLE_METHOD' (best_tac lazy_cs)) *}
+ {* Method.no_args (SIMPLE_METHOD' (best_tac lazy_cs)) *}
"lazy classical reasoning"
lemma aux_impl: "$F, $G |- A ==> $F, !(A -o B), $G |- B"
@@ -282,10 +282,10 @@
method_setup best_safe =
- {* Method.no_args (Method.SIMPLE_METHOD' (best_tac safe_cs)) *} ""
+ {* Method.no_args (SIMPLE_METHOD' (best_tac safe_cs)) *} ""
method_setup best_power =
- {* Method.no_args (Method.SIMPLE_METHOD' (best_tac power_cs)) *} ""
+ {* Method.no_args (SIMPLE_METHOD' (best_tac power_cs)) *} ""
(* Some examples from Troelstra and van Dalen *)
--- a/src/Sequents/LK0.thy Fri Mar 13 19:18:07 2009 +0100
+++ b/src/Sequents/LK0.thy Fri Mar 13 23:56:07 2009 +0100
@@ -240,23 +240,23 @@
*}
method_setup fast_prop =
- {* Method.no_args (Method.SIMPLE_METHOD' (fast_tac prop_pack)) *}
+ {* Method.no_args (SIMPLE_METHOD' (fast_tac prop_pack)) *}
"propositional reasoning"
method_setup fast =
- {* Method.no_args (Method.SIMPLE_METHOD' (fast_tac LK_pack)) *}
+ {* Method.no_args (SIMPLE_METHOD' (fast_tac LK_pack)) *}
"classical reasoning"
method_setup fast_dup =
- {* Method.no_args (Method.SIMPLE_METHOD' (fast_tac LK_dup_pack)) *}
+ {* Method.no_args (SIMPLE_METHOD' (fast_tac LK_dup_pack)) *}
"classical reasoning"
method_setup best =
- {* Method.no_args (Method.SIMPLE_METHOD' (best_tac LK_pack)) *}
+ {* Method.no_args (SIMPLE_METHOD' (best_tac LK_pack)) *}
"classical reasoning"
method_setup best_dup =
- {* Method.no_args (Method.SIMPLE_METHOD' (best_tac LK_dup_pack)) *}
+ {* Method.no_args (SIMPLE_METHOD' (best_tac LK_dup_pack)) *}
"classical reasoning"
--- a/src/Sequents/S4.thy Fri Mar 13 19:18:07 2009 +0100
+++ b/src/Sequents/S4.thy Fri Mar 13 23:56:07 2009 +0100
@@ -45,7 +45,7 @@
*}
method_setup S4_solve =
- {* Method.no_args (Method.SIMPLE_METHOD (S4_Prover.solve_tac 2)) *} "S4 solver"
+ {* Method.no_args (SIMPLE_METHOD (S4_Prover.solve_tac 2)) *} "S4 solver"
(* Theorems of system T from Hughes and Cresswell and Hailpern, LNCS 129 *)
--- a/src/Sequents/S43.thy Fri Mar 13 19:18:07 2009 +0100
+++ b/src/Sequents/S43.thy Fri Mar 13 23:56:07 2009 +0100
@@ -92,7 +92,7 @@
method_setup S43_solve = {*
- Method.no_args (Method.SIMPLE_METHOD
+ Method.no_args (SIMPLE_METHOD
(S43_Prover.solve_tac 2 ORELSE S43_Prover.solve_tac 3))
*} "S4 solver"
--- a/src/Sequents/T.thy Fri Mar 13 19:18:07 2009 +0100
+++ b/src/Sequents/T.thy Fri Mar 13 23:56:07 2009 +0100
@@ -44,7 +44,7 @@
*}
method_setup T_solve =
- {* Method.no_args (Method.SIMPLE_METHOD (T_Prover.solve_tac 2)) *} "T solver"
+ {* Method.no_args (SIMPLE_METHOD (T_Prover.solve_tac 2)) *} "T solver"
(* Theorems of system T from Hughes and Cresswell and Hailpern, LNCS 129 *)
--- a/src/Tools/atomize_elim.ML Fri Mar 13 19:18:07 2009 +0100
+++ b/src/Tools/atomize_elim.ML Fri Mar 13 23:56:07 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 (Method.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/code/code_target.ML Fri Mar 13 19:18:07 2009 +0100
+++ b/src/Tools/code/code_target.ML Fri Mar 13 23:56:07 2009 +0100
@@ -26,7 +26,7 @@
-> (Path.T option -> 'a -> unit)
-> ('a -> string * string option list)
-> 'a -> serialization
- val serialize: theory -> string -> string option -> Args.T list
+ val serialize: theory -> string -> string option -> OuterLex.token list
-> Code_Thingol.naming -> Code_Thingol.program -> string list -> serialization
val serialize_custom: theory -> string * (serializer * literals)
-> Code_Thingol.naming -> Code_Thingol.program -> string list -> string * string option list
@@ -106,7 +106,7 @@
type serializer =
string option (*module name*)
- -> Args.T list (*arguments*)
+ -> OuterLex.token list (*arguments*)
-> (string -> string) (*labelled_name*)
-> string list (*reserved symbols*)
-> (string * Pretty.T) list (*includes*)
--- a/src/Tools/coherent.ML Fri Mar 13 19:18:07 2009 +0100
+++ b/src/Tools/coherent.ML Fri Mar 13 23:56:07 2009 +0100
@@ -225,7 +225,7 @@
end) context 1) ctxt;
fun coherent_meth rules ctxt =
- Method.METHOD (fn facts => coherent_tac (facts @ rules) ctxt 1);
+ METHOD (fn facts => coherent_tac (facts @ rules) ctxt 1);
val setup = Method.add_method
("coherent", Method.thms_ctxt_args coherent_meth, "prove coherent formula");
--- a/src/Tools/eqsubst.ML Fri Mar 13 19:18:07 2009 +0100
+++ b/src/Tools/eqsubst.ML Fri Mar 13 23:56:07 2009 +0100
@@ -109,8 +109,8 @@
searchinfo -> Term.term -> match Seq.seq Seq.seq
(* syntax tools *)
- val ith_syntax : Args.T list -> int list * Args.T list
- val options_syntax : Args.T list -> bool * Args.T list
+ val ith_syntax : int list parser
+ val options_syntax : bool parser
(* Isar level hooks *)
val eqsubst_asm_meth : Proof.context -> int list -> Thm.thm list -> Proof.method
@@ -434,7 +434,7 @@
(* inthms are the given arguments in Isar, and treated as eqstep with
the first one, then the second etc *)
fun eqsubst_meth ctxt occL inthms =
- Method.SIMPLE_METHOD' (eqsubst_tac ctxt occL inthms);
+ SIMPLE_METHOD' (eqsubst_tac ctxt occL inthms);
(* apply a substitution inside assumption j, keeps asm in the same place *)
fun apply_subst_in_asm i th rule ((cfvs, j, ngoalprems, pth),m) =
@@ -548,7 +548,7 @@
(* inthms are the given arguments in Isar, and treated as eqstep with
the first one, then the second etc *)
fun eqsubst_asm_meth ctxt occL inthms =
- Method.SIMPLE_METHOD' (eqsubst_asm_tac ctxt occL inthms);
+ SIMPLE_METHOD' (eqsubst_asm_tac ctxt occL inthms);
(* syntax for options, given "(asm)" will give back true, without
gives back false *)
--- a/src/Tools/induct.ML Fri Mar 13 19:18:07 2009 +0100
+++ b/src/Tools/induct.ML Fri Mar 13 23:56:07 2009 +0100
@@ -735,23 +735,22 @@
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.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) =>
- Method.RAW_METHOD_CASES (fn facts =>
+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) =>
- Method.RAW_METHOD_CASES (fn facts =>
+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))));
end;
@@ -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/Tools/intuitionistic.ML Fri Mar 13 19:18:07 2009 +0100
+++ b/src/Tools/intuitionistic.ML Fri Mar 13 23:56:07 2009 +0100
@@ -86,7 +86,7 @@
val method =
Method.bang_sectioned_args' modifiers (Scan.lift (Scan.option OuterParse.nat))
- (fn n => fn prems => fn ctxt => Method.METHOD (fn facts =>
+ (fn n => fn prems => fn ctxt => METHOD (fn facts =>
HEADGOAL (Method.insert_tac (prems @ facts) THEN'
ObjectLogic.atomize_prems_tac THEN' prover_tac ctxt n)));
--- a/src/ZF/Tools/ind_cases.ML Fri Mar 13 19:18:07 2009 +0100
+++ b/src/ZF/Tools/ind_cases.ML Fri Mar 13 23:56:07 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 *)
--- a/src/ZF/Tools/typechk.ML Fri Mar 13 19:18:07 2009 +0100
+++ b/src/ZF/Tools/typechk.ML Fri Mar 13 23:56:07 2009 +0100
@@ -116,7 +116,7 @@
Method.only_sectioned_args
[Args.add -- Args.colon >> K (I, TC_add),
Args.del -- Args.colon >> K (I, TC_del)]
- (fn ctxt => Method.SIMPLE_METHOD (CHANGED (typecheck_tac ctxt)));
+ (fn ctxt => SIMPLE_METHOD (CHANGED (typecheck_tac ctxt)));
val _ =
OuterSyntax.improper_command "print_tcset" "print context of ZF typecheck" OuterKeyword.diag
--- a/src/ZF/UNITY/Constrains.thy Fri Mar 13 19:18:07 2009 +0100
+++ b/src/ZF/UNITY/Constrains.thy Fri Mar 13 23:56:07 2009 +0100
@@ -496,13 +496,11 @@
setup ProgramDefs.setup
method_setup safety = {*
- Method.ctxt_args (fn ctxt =>
- Method.SIMPLE_METHOD' (constrains_tac ctxt)) *}
+ Method.ctxt_args (SIMPLE_METHOD' o constrains_tac) *}
"for proving safety properties"
method_setup always = {*
- Method.ctxt_args (fn ctxt =>
- Method.SIMPLE_METHOD' (always_tac ctxt)) *}
+ Method.ctxt_args (SIMPLE_METHOD' o always_tac) *}
"for proving invariants"
end