--- a/NEWS Mon Mar 16 14:26:30 2009 +0100
+++ b/NEWS Mon Mar 16 18:24:39 2009 +0100
@@ -603,7 +603,10 @@
or later]
* Simplified ML attribute and method setup, cf. functions Attrib.setup
-and Method.setup, as well as commands 'attribute_setup'.
+and Method.setup, as well as commands 'attribute_setup' and
+'method_setup'. INCOMPATIBILITY for 'method_setup', need to simplify
+existing code accordingly, or use plain 'setup' together with old
+Method.add_method.
* Simplified ML oracle interface Thm.add_oracle promotes 'a -> cterm
to 'a -> thm, while results are always tagged with an authentic oracle
--- a/doc-src/IsarRef/Thy/Proof.thy Mon Mar 16 14:26:30 2009 +0100
+++ b/doc-src/IsarRef/Thy/Proof.thy Mon Mar 16 18:24:39 2009 +0100
@@ -886,32 +886,33 @@
\item @{command "method_setup"}~@{text "name = text description"}
defines a proof method in the current theory. The given @{text
- "text"} has to be an ML expression of type @{ML_type "Args.src ->
- Proof.context -> Proof.method"}. Parsing concrete method syntax
- from @{ML_type Args.src} input can be quite tedious in general. The
- following simple examples are for methods without any explicit
- arguments, or a list of theorems, respectively.
+ "text"} has to be an ML expression of type
+ @{ML_type "(Proof.context -> Proof.method) context_parser"}, cf.\
+ basic parsers defined in structure @{ML_struct Args} and @{ML_struct
+ Attrib}. There are also combinators like @{ML METHOD} and @{ML
+ SIMPLE_METHOD} to turn certain tactic forms into official proof
+ methods; the primed versions refer to tactics with explicit goal
+ addressing.
-%FIXME proper antiquotations
-{\footnotesize
-\begin{verbatim}
- 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}
-}
-
- Note that mere tactic emulations may ignore the @{text facts}
- parameter above. Proper proof methods would do something
- appropriate with the list of current facts, though. Single-rule
- methods usually do strict forward-chaining (e.g.\ by using @{ML
- Drule.multi_resolves}), while automatic ones just insert the facts
- using @{ML Method.insert_tac} before applying the main tactic.
+ Here are some example method definitions:
\end{description}
*}
+ method_setup my_method1 = {*
+ Scan.succeed (K (SIMPLE_METHOD' (fn i: int => no_tac)))
+ *} "my first method (without any arguments)"
+
+ method_setup my_method2 = {*
+ Scan.succeed (fn ctxt: Proof.context =>
+ SIMPLE_METHOD' (fn i: int => no_tac))
+ *} "my second method (with context)"
+
+ method_setup my_method3 = {*
+ Attrib.thms >> (fn thms: thm list => fn ctxt: Proof.context =>
+ SIMPLE_METHOD' (fn i: int => no_tac))
+ *} "my third method (with theorem arguments and context)"
+
section {* Generalized elimination \label{sec:obtain} *}
@@ -1041,7 +1042,7 @@
\begin{matharray}{rcl}
@{command "also"}@{text "\<^sub>0"} & \equiv & @{command "note"}~@{text "calculation = this"} \\
- @{command "also"}@{text "\<^sub>n\<^sub>+\<^sub>1"} & \equiv & @{command "note"}~@{text "calculation = trans [OF calculation this]"} \\[0.5ex]
+ @{command "also"}@{text "\<^sub>n+1"} & \equiv & @{command "note"}~@{text "calculation = trans [OF calculation this]"} \\[0.5ex]
@{command "finally"} & \equiv & @{command "also"}~@{command "from"}~@{text calculation} \\[0.5ex]
@{command "moreover"} & \equiv & @{command "note"}~@{text "calculation = calculation this"} \\
@{command "ultimately"} & \equiv & @{command "moreover"}~@{command "from"}~@{text calculation} \\
--- a/doc-src/IsarRef/Thy/Spec.thy Mon Mar 16 14:26:30 2009 +0100
+++ b/doc-src/IsarRef/Thy/Spec.thy Mon Mar 16 18:24:39 2009 +0100
@@ -878,7 +878,7 @@
let val th' = th OF ths
in th' end)) *} "my rule"
- attribute_setup my_declatation = {*
+ attribute_setup my_declaration = {*
Attrib.thms >> (fn ths =>
Thm.declaration_attribute (fn th: thm => fn context: Context.generic =>
let val context' = context
--- a/doc-src/IsarRef/Thy/document/Proof.tex Mon Mar 16 14:26:30 2009 +0100
+++ b/doc-src/IsarRef/Thy/document/Proof.tex Mon Mar 16 18:24:39 2009 +0100
@@ -890,32 +890,46 @@
\begin{description}
\item \hyperlink{command.method-setup}{\mbox{\isa{\isacommand{method{\isacharunderscore}setup}}}}~\isa{{\isachardoublequote}name\ {\isacharequal}\ text\ description{\isachardoublequote}}
- defines a proof method in the current theory. The given \isa{{\isachardoublequote}text{\isachardoublequote}} has to be an ML expression of type \verb|Args.src ->|\isasep\isanewline%
-\verb| Proof.context -> Proof.method|. Parsing concrete method syntax
- from \verb|Args.src| input can be quite tedious in general. The
- following simple examples are for methods without any explicit
- arguments, or a list of theorems, respectively.
+ defines a proof method in the current theory. The given \isa{{\isachardoublequote}text{\isachardoublequote}} has to be an ML expression of type
+ \verb|(Proof.context -> Proof.method) context_parser|, cf.\
+ basic parsers defined in structure \verb|Args| and \verb|Attrib|. There are also combinators like \verb|METHOD| and \verb|SIMPLE_METHOD| to turn certain tactic forms into official proof
+ methods; the primed versions refer to tactics with explicit goal
+ addressing.
-%FIXME proper antiquotations
-{\footnotesize
-\begin{verbatim}
- 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}
-}
-
- Note that mere tactic emulations may ignore the \isa{facts}
- parameter above. Proper proof methods would do something
- appropriate with the list of current facts, though. Single-rule
- methods usually do strict forward-chaining (e.g.\ by using \verb|Drule.multi_resolves|), while automatic ones just insert the facts
- using \verb|Method.insert_tac| before applying the main tactic.
+ Here are some example method definitions:
\end{description}%
\end{isamarkuptext}%
\isamarkuptrue%
%
+\isadelimML
+\ \ \ \ %
+\endisadelimML
+%
+\isatagML
+\isacommand{method{\isacharunderscore}setup}\isamarkupfalse%
+\ my{\isacharunderscore}method{\isadigit{1}}\ {\isacharequal}\ {\isacharverbatimopen}\isanewline
+\ \ \ \ \ \ Scan{\isachardot}succeed\ {\isacharparenleft}K\ {\isacharparenleft}SIMPLE{\isacharunderscore}METHOD{\isacharprime}\ {\isacharparenleft}fn\ i{\isacharcolon}\ int\ {\isacharequal}{\isachargreater}\ no{\isacharunderscore}tac{\isacharparenright}{\isacharparenright}{\isacharparenright}\isanewline
+\ \ \ \ {\isacharverbatimclose}\ \ {\isachardoublequoteopen}my\ first\ method\ {\isacharparenleft}without\ any\ arguments{\isacharparenright}{\isachardoublequoteclose}\isanewline
+\isanewline
+\ \ \ \ \isacommand{method{\isacharunderscore}setup}\isamarkupfalse%
+\ my{\isacharunderscore}method{\isadigit{2}}\ {\isacharequal}\ {\isacharverbatimopen}\isanewline
+\ \ \ \ \ \ Scan{\isachardot}succeed\ {\isacharparenleft}fn\ ctxt{\isacharcolon}\ Proof{\isachardot}context\ {\isacharequal}{\isachargreater}\isanewline
+\ \ \ \ \ \ \ \ SIMPLE{\isacharunderscore}METHOD{\isacharprime}\ {\isacharparenleft}fn\ i{\isacharcolon}\ int\ {\isacharequal}{\isachargreater}\ no{\isacharunderscore}tac{\isacharparenright}{\isacharparenright}\isanewline
+\ \ \ \ {\isacharverbatimclose}\ \ {\isachardoublequoteopen}my\ second\ method\ {\isacharparenleft}with\ context{\isacharparenright}{\isachardoublequoteclose}\isanewline
+\isanewline
+\ \ \ \ \isacommand{method{\isacharunderscore}setup}\isamarkupfalse%
+\ my{\isacharunderscore}method{\isadigit{3}}\ {\isacharequal}\ {\isacharverbatimopen}\isanewline
+\ \ \ \ \ \ Attrib{\isachardot}thms\ {\isachargreater}{\isachargreater}\ {\isacharparenleft}fn\ thms{\isacharcolon}\ thm\ list\ {\isacharequal}{\isachargreater}\ fn\ ctxt{\isacharcolon}\ Proof{\isachardot}context\ {\isacharequal}{\isachargreater}\isanewline
+\ \ \ \ \ \ \ \ SIMPLE{\isacharunderscore}METHOD{\isacharprime}\ {\isacharparenleft}fn\ i{\isacharcolon}\ int\ {\isacharequal}{\isachargreater}\ no{\isacharunderscore}tac{\isacharparenright}{\isacharparenright}\isanewline
+\ \ \ \ {\isacharverbatimclose}\ \ {\isachardoublequoteopen}my\ third\ method\ {\isacharparenleft}with\ theorem\ arguments\ and\ context{\isacharparenright}{\isachardoublequoteclose}%
+\endisatagML
+{\isafoldML}%
+%
+\isadelimML
+%
+\endisadelimML
+%
\isamarkupsection{Generalized elimination \label{sec:obtain}%
}
\isamarkuptrue%
@@ -1040,7 +1054,7 @@
\begin{matharray}{rcl}
\hyperlink{command.also}{\mbox{\isa{\isacommand{also}}}}\isa{{\isachardoublequote}\isactrlsub {\isadigit{0}}{\isachardoublequote}} & \equiv & \hyperlink{command.note}{\mbox{\isa{\isacommand{note}}}}~\isa{{\isachardoublequote}calculation\ {\isacharequal}\ this{\isachardoublequote}} \\
- \hyperlink{command.also}{\mbox{\isa{\isacommand{also}}}}\isa{{\isachardoublequote}\isactrlsub n\isactrlsub {\isacharplus}\isactrlsub {\isadigit{1}}{\isachardoublequote}} & \equiv & \hyperlink{command.note}{\mbox{\isa{\isacommand{note}}}}~\isa{{\isachardoublequote}calculation\ {\isacharequal}\ trans\ {\isacharbrackleft}OF\ calculation\ this{\isacharbrackright}{\isachardoublequote}} \\[0.5ex]
+ \hyperlink{command.also}{\mbox{\isa{\isacommand{also}}}}\isa{{\isachardoublequote}\isactrlsub n{\isacharplus}{\isadigit{1}}{\isachardoublequote}} & \equiv & \hyperlink{command.note}{\mbox{\isa{\isacommand{note}}}}~\isa{{\isachardoublequote}calculation\ {\isacharequal}\ trans\ {\isacharbrackleft}OF\ calculation\ this{\isacharbrackright}{\isachardoublequote}} \\[0.5ex]
\hyperlink{command.finally}{\mbox{\isa{\isacommand{finally}}}} & \equiv & \hyperlink{command.also}{\mbox{\isa{\isacommand{also}}}}~\hyperlink{command.from}{\mbox{\isa{\isacommand{from}}}}~\isa{calculation} \\[0.5ex]
\hyperlink{command.moreover}{\mbox{\isa{\isacommand{moreover}}}} & \equiv & \hyperlink{command.note}{\mbox{\isa{\isacommand{note}}}}~\isa{{\isachardoublequote}calculation\ {\isacharequal}\ calculation\ this{\isachardoublequote}} \\
\hyperlink{command.ultimately}{\mbox{\isa{\isacommand{ultimately}}}} & \equiv & \hyperlink{command.moreover}{\mbox{\isa{\isacommand{moreover}}}}~\hyperlink{command.from}{\mbox{\isa{\isacommand{from}}}}~\isa{calculation} \\
--- a/doc-src/IsarRef/Thy/document/Spec.tex Mon Mar 16 14:26:30 2009 +0100
+++ b/doc-src/IsarRef/Thy/document/Spec.tex Mon Mar 16 18:24:39 2009 +0100
@@ -891,7 +891,7 @@
\ \ \ \ \ \ \ \ \ \ in\ th{\isacharprime}\ end{\isacharparenright}{\isacharparenright}\ {\isacharverbatimclose}\ \ {\isachardoublequoteopen}my\ rule{\isachardoublequoteclose}\isanewline
\isanewline
\ \ \ \ \isacommand{attribute{\isacharunderscore}setup}\isamarkupfalse%
-\ my{\isacharunderscore}declatation\ {\isacharequal}\ {\isacharverbatimopen}\isanewline
+\ my{\isacharunderscore}declaration\ {\isacharequal}\ {\isacharverbatimopen}\isanewline
\ \ \ \ \ \ Attrib{\isachardot}thms\ {\isachargreater}{\isachargreater}\ {\isacharparenleft}fn\ ths\ {\isacharequal}{\isachargreater}\isanewline
\ \ \ \ \ \ \ \ Thm{\isachardot}declaration{\isacharunderscore}attribute\ {\isacharparenleft}fn\ th{\isacharcolon}\ thm\ {\isacharequal}{\isachargreater}\ fn\ context{\isacharcolon}\ Context{\isachardot}generic\ {\isacharequal}{\isachargreater}\isanewline
\ \ \ \ \ \ \ \ \ \ let\ val\ context{\isacharprime}\ {\isacharequal}\ context\isanewline
--- a/doc-src/TutorialI/Protocol/Event.thy Mon Mar 16 14:26:30 2009 +0100
+++ b/doc-src/TutorialI/Protocol/Event.thy Mon Mar 16 18:24:39 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 (SIMPLE_METHOD (REPEAT_FIRST analz_mono_contra_tac)) *}
+ Scan.succeed (K (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 (SIMPLE_METHOD (REPEAT_FIRST synth_analz_mono_contra_tac)) *}
+ Scan.succeed (K (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 Mon Mar 16 14:26:30 2009 +0100
+++ b/doc-src/TutorialI/Protocol/Message.thy Mon Mar 16 18:24:39 2009 +0100
@@ -919,15 +919,15 @@
lemmas Fake_parts_sing_imp_Un = Fake_parts_sing [THEN [2] rev_subsetD]
method_setup spy_analz = {*
- Method.ctxt_args (SIMPLE_METHOD' o gen_spy_analz_tac o local_clasimpset_of) *}
+ Scan.succeed (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 (SIMPLE_METHOD' o atomic_spy_analz_tac o local_clasimpset_of) *}
+ Scan.succeed (SIMPLE_METHOD' o atomic_spy_analz_tac o local_clasimpset_of) *}
"for debugging spy_analz"
method_setup Fake_insert_simp = {*
- Method.ctxt_args (SIMPLE_METHOD' o Fake_insert_simp_tac o local_simpset_of) *}
+ Scan.succeed (SIMPLE_METHOD' o Fake_insert_simp_tac o local_simpset_of) *}
"for debugging spy_analz"
--- a/doc-src/TutorialI/Protocol/Public.thy Mon Mar 16 14:26:30 2009 +0100
+++ b/doc-src/TutorialI/Protocol/Public.thy Mon Mar 16 18:24:39 2009 +0100
@@ -161,7 +161,7 @@
resolve_tac [refl, conjI, @{thm Nonce_supply}]));
*}
-method_setup possibility = {* Method.no_args (SIMPLE_METHOD possibility_tac) *}
+method_setup possibility = {* Scan.succeed (K (SIMPLE_METHOD possibility_tac)) *}
"for proving possibility theorems"
end
--- a/src/Cube/Example.thy Mon Mar 16 14:26:30 2009 +0100
+++ b/src/Cube/Example.thy Mon Mar 16 18:24:39 2009 +0100
@@ -15,20 +15,19 @@
*}
method_setup depth_solve = {*
- Method.thms_args (fn thms => METHOD (fn facts =>
- (DEPTH_SOLVE (HEADGOAL (ares_tac (facts @ thms))))))
+ Attrib.thms >> (fn thms => K (METHOD (fn facts =>
+ (DEPTH_SOLVE (HEADGOAL (ares_tac (facts @ thms)))))))
*} ""
method_setup depth_solve1 = {*
- Method.thms_args (fn thms => METHOD (fn facts =>
- (DEPTH_SOLVE_1 (HEADGOAL (ares_tac (facts @ thms))))))
+ Attrib.thms >> (fn thms => K (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 (fn facts =>
- REPEAT (resolve_tac [strip_b, strip_s] 1 THEN DEPTH_SOLVE_1 (ares_tac (facts @ thms) 1))))
- end
+ Attrib.thms >> (fn thms => K (METHOD (fn facts =>
+ REPEAT (resolve_tac [@{thm strip_b}, @{thm strip_s}] 1 THEN
+ DEPTH_SOLVE_1 (ares_tac (facts @ thms) 1)))))
*} ""
--- a/src/FOL/FOL.thy Mon Mar 16 14:26:30 2009 +0100
+++ b/src/FOL/FOL.thy Mon Mar 16 18:24:39 2009 +0100
@@ -73,9 +73,10 @@
fun case_tac ctxt a = res_inst_tac ctxt [(("P", 0), a)] @{thm case_split}
*}
-method_setup case_tac =
- {* Method.goal_args_ctxt Args.name_source case_tac *}
- "case_tac emulation (dynamic instantiation!)"
+method_setup case_tac = {*
+ Args.goal_spec -- Scan.lift Args.name_source >>
+ (fn (quant, s) => fn ctxt => SIMPLE_METHOD'' quant (case_tac ctxt s))
+*} "case_tac emulation (dynamic instantiation!)"
(*** Special elimination rules *)
--- a/src/FOL/ex/Iff_Oracle.thy Mon Mar 16 14:26:30 2009 +0100
+++ b/src/FOL/ex/Iff_Oracle.thy Mon Mar 16 18:24:39 2009 +0100
@@ -52,7 +52,7 @@
subsection {* Oracle as proof method *}
method_setup iff = {*
- Method.simple_args OuterParse.nat (fn n => fn ctxt =>
+ Scan.lift OuterParse.nat >> (fn n => fn ctxt =>
SIMPLE_METHOD
(HEADGOAL (Tactic.rtac (iff_oracle (ProofContext.theory_of ctxt, n)))
handle Fail _ => no_tac))
--- a/src/HOL/Algebra/abstract/Ring2.thy Mon Mar 16 14:26:30 2009 +0100
+++ b/src/HOL/Algebra/abstract/Ring2.thy Mon Mar 16 18:24:39 2009 +0100
@@ -222,7 +222,7 @@
*} (* Note: r_one is not necessary in ring_ss *)
method_setup ring =
- {* Method.no_args (SIMPLE_METHOD' (full_simp_tac ring_ss)) *}
+ {* Scan.succeed (K (SIMPLE_METHOD' (full_simp_tac ring_ss))) *}
{* computes distributive normal form in rings *}
--- a/src/HOL/Auth/Event.thy Mon Mar 16 14:26:30 2009 +0100
+++ b/src/HOL/Auth/Event.thy Mon Mar 16 18:24:39 2009 +0100
@@ -289,7 +289,7 @@
*}
method_setup analz_mono_contra = {*
- Method.no_args (SIMPLE_METHOD (REPEAT_FIRST analz_mono_contra_tac)) *}
+ Scan.succeed (K (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 (SIMPLE_METHOD (REPEAT_FIRST synth_analz_mono_contra_tac)) *}
+ Scan.succeed (K (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 Mon Mar 16 14:26:30 2009 +0100
+++ b/src/HOL/Auth/Message.thy Mon Mar 16 18:24:39 2009 +0100
@@ -941,15 +941,15 @@
lemmas Fake_parts_sing_imp_Un = Fake_parts_sing [THEN [2] rev_subsetD]
method_setup spy_analz = {*
- Method.ctxt_args (SIMPLE_METHOD' o Message.gen_spy_analz_tac o local_clasimpset_of) *}
+ Scan.succeed (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 (SIMPLE_METHOD' o Message.atomic_spy_analz_tac o local_clasimpset_of) *}
+ Scan.succeed (SIMPLE_METHOD' o Message.atomic_spy_analz_tac o local_clasimpset_of) *}
"for debugging spy_analz"
method_setup Fake_insert_simp = {*
- Method.ctxt_args (SIMPLE_METHOD' o Message.Fake_insert_simp_tac o local_simpset_of) *}
+ Scan.succeed (SIMPLE_METHOD' o Message.Fake_insert_simp_tac o local_simpset_of) *}
"for debugging spy_analz"
end
--- a/src/HOL/Auth/OtwayReesBella.thy Mon Mar 16 14:26:30 2009 +0100
+++ b/src/HOL/Auth/OtwayReesBella.thy Mon Mar 16 18:24:39 2009 +0100
@@ -137,7 +137,7 @@
*}
method_setup parts_explicit = {*
- Method.no_args (SIMPLE_METHOD' parts_explicit_tac) *}
+ Scan.succeed (K (SIMPLE_METHOD' parts_explicit_tac)) *}
"to explicitly state that some message components belong to parts knows Spy"
@@ -257,7 +257,7 @@
*}
method_setup analz_freshCryptK = {*
- Method.ctxt_args (fn ctxt =>
+ Scan.succeed (fn ctxt =>
(SIMPLE_METHOD
(EVERY [REPEAT_FIRST (resolve_tac [allI, ballI, impI]),
REPEAT_FIRST (rtac @{thm analz_image_freshCryptK_lemma}),
@@ -267,10 +267,10 @@
method_setup disentangle = {*
- Method.no_args
- (SIMPLE_METHOD
+ Scan.succeed
+ (K (SIMPLE_METHOD
(REPEAT_FIRST (eresolve_tac [asm_rl, conjE, disjE]
- ORELSE' hyp_subst_tac))) *}
+ ORELSE' hyp_subst_tac)))) *}
"for eliminating conjunctions, disjunctions and the like"
--- a/src/HOL/Auth/Public.thy Mon Mar 16 14:26:30 2009 +0100
+++ b/src/HOL/Auth/Public.thy Mon Mar 16 18:24:39 2009 +0100
@@ -424,7 +424,7 @@
*}
method_setup analz_freshK = {*
- Method.ctxt_args (fn ctxt =>
+ Scan.succeed (fn ctxt =>
(SIMPLE_METHOD
(EVERY [REPEAT_FIRST (resolve_tac [allI, ballI, impI]),
REPEAT_FIRST (rtac @{thm analz_image_freshK_lemma}),
@@ -435,11 +435,11 @@
subsection{*Specialized Methods for Possibility Theorems*}
method_setup possibility = {*
- Method.ctxt_args (SIMPLE_METHOD o Public.possibility_tac) *}
+ Scan.succeed (SIMPLE_METHOD o Public.possibility_tac) *}
"for proving possibility theorems"
method_setup basic_possibility = {*
- Method.ctxt_args (SIMPLE_METHOD o Public.basic_possibility_tac) *}
+ Scan.succeed (SIMPLE_METHOD o Public.basic_possibility_tac) *}
"for proving possibility theorems"
end
--- a/src/HOL/Auth/Shared.thy Mon Mar 16 14:26:30 2009 +0100
+++ b/src/HOL/Auth/Shared.thy Mon Mar 16 18:24:39 2009 +0100
@@ -238,7 +238,7 @@
(*Specialized methods*)
method_setup analz_freshK = {*
- Method.ctxt_args (fn ctxt =>
+ Scan.succeed (fn ctxt =>
(SIMPLE_METHOD
(EVERY [REPEAT_FIRST (resolve_tac [allI, ballI, impI]),
REPEAT_FIRST (rtac @{thm analz_image_freshK_lemma}),
@@ -246,11 +246,11 @@
"for proving the Session Key Compromise theorem"
method_setup possibility = {*
- Method.ctxt_args (fn ctxt => SIMPLE_METHOD (Shared.possibility_tac ctxt)) *}
+ Scan.succeed (fn ctxt => SIMPLE_METHOD (Shared.possibility_tac ctxt)) *}
"for proving possibility theorems"
method_setup basic_possibility = {*
- Method.ctxt_args (fn ctxt => SIMPLE_METHOD (Shared.basic_possibility_tac ctxt)) *}
+ Scan.succeed (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 Mon Mar 16 14:26:30 2009 +0100
+++ b/src/HOL/Auth/Smartcard/ShoupRubin.thy Mon Mar 16 18:24:39 2009 +0100
@@ -769,15 +769,15 @@
*}
method_setup prepare = {*
- Method.no_args (SIMPLE_METHOD ShoupRubin.prepare_tac) *}
+ Scan.succeed (K (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 => SIMPLE_METHOD (ShoupRubin.parts_prepare_tac ctxt)) *}
+ Scan.succeed (fn ctxt => SIMPLE_METHOD (ShoupRubin.parts_prepare_tac ctxt)) *}
"additional facts to reason about parts"
method_setup analz_prepare = {*
- Method.no_args (SIMPLE_METHOD ShoupRubin.analz_prepare_tac) *}
+ Scan.succeed (K (SIMPLE_METHOD ShoupRubin.analz_prepare_tac)) *}
"additional facts to reason about analz"
@@ -822,7 +822,7 @@
done
method_setup sc_analz_freshK = {*
- Method.ctxt_args (fn ctxt =>
+ Scan.succeed (fn ctxt =>
(SIMPLE_METHOD
(EVERY [REPEAT_FIRST
(resolve_tac [allI, ballI, impI]),
--- a/src/HOL/Auth/Smartcard/ShoupRubinBella.thy Mon Mar 16 14:26:30 2009 +0100
+++ b/src/HOL/Auth/Smartcard/ShoupRubinBella.thy Mon Mar 16 18:24:39 2009 +0100
@@ -777,15 +777,15 @@
*}
method_setup prepare = {*
- Method.ctxt_args (fn ctxt => SIMPLE_METHOD (ShoupRubinBella.prepare_tac ctxt)) *}
+ Scan.succeed (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 => SIMPLE_METHOD (ShoupRubinBella.parts_prepare_tac ctxt)) *}
+ Scan.succeed (fn ctxt => SIMPLE_METHOD (ShoupRubinBella.parts_prepare_tac ctxt)) *}
"additional facts to reason about parts"
method_setup analz_prepare = {*
- Method.ctxt_args (fn ctxt => SIMPLE_METHOD (ShoupRubinBella.analz_prepare_tac ctxt)) *}
+ Scan.succeed (fn ctxt => SIMPLE_METHOD (ShoupRubinBella.analz_prepare_tac ctxt)) *}
"additional facts to reason about analz"
@@ -831,7 +831,7 @@
done
method_setup sc_analz_freshK = {*
- Method.ctxt_args (fn ctxt =>
+ Scan.succeed (fn ctxt =>
(SIMPLE_METHOD
(EVERY [REPEAT_FIRST (resolve_tac [allI, ballI, impI]),
REPEAT_FIRST (rtac @{thm analz_image_freshK_lemma}),
--- a/src/HOL/Auth/Smartcard/Smartcard.thy Mon Mar 16 14:26:30 2009 +0100
+++ b/src/HOL/Auth/Smartcard/Smartcard.thy Mon Mar 16 18:24:39 2009 +0100
@@ -407,7 +407,7 @@
(*Specialized methods*)
method_setup analz_freshK = {*
- Method.ctxt_args (fn ctxt =>
+ Scan.succeed (fn ctxt =>
(SIMPLE_METHOD
(EVERY [REPEAT_FIRST (resolve_tac [allI, ballI, impI]),
REPEAT_FIRST (rtac @{thm analz_image_freshK_lemma}),
@@ -415,12 +415,12 @@
"for proving the Session Key Compromise theorem"
method_setup possibility = {*
- Method.ctxt_args (fn ctxt =>
+ Scan.succeed (fn ctxt =>
SIMPLE_METHOD (Smartcard.possibility_tac ctxt)) *}
"for proving possibility theorems"
method_setup basic_possibility = {*
- Method.ctxt_args (fn ctxt =>
+ Scan.succeed (fn ctxt =>
SIMPLE_METHOD (Smartcard.basic_possibility_tac ctxt)) *}
"for proving possibility theorems"
--- a/src/HOL/Code_Setup.thy Mon Mar 16 14:26:30 2009 +0100
+++ b/src/HOL/Code_Setup.thy Mon Mar 16 18:24:39 2009 +0100
@@ -226,19 +226,19 @@
*}
ML {*
-fun gen_eval_method conv = Method.ctxt_args (fn ctxt => SIMPLE_METHOD'
+fun gen_eval_method conv ctxt = SIMPLE_METHOD'
(CONVERSION (Conv.params_conv (~1) (K (Conv.concl_conv (~1) conv)) ctxt)
- THEN' rtac TrueI))
+ THEN' rtac TrueI)
*}
-method_setup eval = {* gen_eval_method eval_oracle *}
+method_setup eval = {* Scan.succeed (gen_eval_method eval_oracle) *}
"solve goal by evaluation"
-method_setup evaluation = {* gen_eval_method Codegen.evaluation_conv *}
+method_setup evaluation = {* Scan.succeed (gen_eval_method Codegen.evaluation_conv) *}
"solve goal by evaluation"
-method_setup normalization = {* (Method.no_args o SIMPLE_METHOD')
- (CONVERSION Nbe.norm_conv THEN' (fn k => TRY (rtac TrueI k)))
+method_setup normalization = {*
+ Scan.succeed (K (SIMPLE_METHOD' (CONVERSION Nbe.norm_conv THEN' (fn k => TRY (rtac TrueI k)))))
*} "solve goal by normalization"
--- a/src/HOL/Decision_Procs/Approximation.thy Mon Mar 16 14:26:30 2009 +0100
+++ b/src/HOL/Decision_Procs/Approximation.thy Mon Mar 16 18:24:39 2009 +0100
@@ -2496,16 +2496,15 @@
*}
-method_setup approximation = {* fn src =>
- Method.syntax Args.term src #>
- (fn (prec, ctxt) => let
- in SIMPLE_METHOD' (fn i =>
+method_setup approximation = {*
+ Args.term >>
+ (fn prec => fn ctxt =>
+ 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
THEN (TRY (filter_prems_tac (fn t => false) i))
- THEN (gen_eval_tac eval_oracle ctxt) i))
- end)
+ THEN (gen_eval_tac eval_oracle ctxt) i)))
*} "real number approximation"
end
--- a/src/HOL/Decision_Procs/Dense_Linear_Order.thy Mon Mar 16 14:26:30 2009 +0100
+++ b/src/HOL/Decision_Procs/Dense_Linear_Order.thy Mon Mar 16 18:24:39 2009 +0100
@@ -295,7 +295,7 @@
use "~~/src/HOL/Tools/Qelim/langford.ML"
method_setup dlo = {*
- Method.ctxt_args (SIMPLE_METHOD' o LangfordQE.dlo_tac)
+ Scan.succeed (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 (SIMPLE_METHOD' o FerranteRackoff.dlo_tac)
+ Scan.succeed (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/Groebner_Basis.thy Mon Mar 16 14:26:30 2009 +0100
+++ b/src/HOL/Groebner_Basis.thy Mon Mar 16 18:24:39 2009 +0100
@@ -253,7 +253,7 @@
method_setup sring_norm = {*
- Method.ctxt_args (SIMPLE_METHOD' o Normalizer.semiring_normalize_tac)
+ Scan.succeed (SIMPLE_METHOD' o Normalizer.semiring_normalize_tac)
*} "semiring normalizer"
@@ -427,10 +427,9 @@
val any_keyword = keyword addN || keyword delN
val thms = Scan.repeat (Scan.unless any_keyword Attrib.multi_thm) >> flat;
in
-fn src => Method.syntax
- ((Scan.optional (keyword addN |-- thms) []) --
- (Scan.optional (keyword delN |-- thms) [])) src
- #> (fn ((add_ths, del_ths), ctxt) =>
+ ((Scan.optional (keyword addN |-- thms) []) --
+ (Scan.optional (keyword delN |-- thms) [])) >>
+ (fn (add_ths, del_ths) => fn 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"
--- a/src/HOL/Hoare/Hoare.thy Mon Mar 16 14:26:30 2009 +0100
+++ b/src/HOL/Hoare/Hoare.thy Mon Mar 16 18:24:39 2009 +0100
@@ -234,11 +234,11 @@
use "hoare_tac.ML"
method_setup vcg = {*
- Method.ctxt_args (fn ctxt => SIMPLE_METHOD' (hoare_tac ctxt (K all_tac))) *}
+ Scan.succeed (fn ctxt => SIMPLE_METHOD' (hoare_tac ctxt (K all_tac))) *}
"verification condition generator"
method_setup vcg_simp = {*
- Method.ctxt_args (fn ctxt =>
+ Scan.succeed (fn ctxt =>
SIMPLE_METHOD' (hoare_tac ctxt (asm_full_simp_tac (local_simpset_of ctxt)))) *}
"verification condition generator plus simplification"
--- a/src/HOL/Hoare/HoareAbort.thy Mon Mar 16 14:26:30 2009 +0100
+++ b/src/HOL/Hoare/HoareAbort.thy Mon Mar 16 18:24:39 2009 +0100
@@ -246,11 +246,11 @@
use "hoare_tac.ML"
method_setup vcg = {*
- Method.ctxt_args (fn ctxt => SIMPLE_METHOD' (hoare_tac ctxt (K all_tac))) *}
+ Scan.succeed (fn ctxt => SIMPLE_METHOD' (hoare_tac ctxt (K all_tac))) *}
"verification condition generator"
method_setup vcg_simp = {*
- Method.ctxt_args (fn ctxt =>
+ Scan.succeed (fn ctxt =>
SIMPLE_METHOD' (hoare_tac ctxt (asm_full_simp_tac (local_simpset_of ctxt)))) *}
"verification condition generator plus simplification"
--- a/src/HOL/HoareParallel/OG_Tactics.thy Mon Mar 16 14:26:30 2009 +0100
+++ b/src/HOL/HoareParallel/OG_Tactics.thy Mon Mar 16 18:24:39 2009 +0100
@@ -465,21 +465,21 @@
Isabelle proofs. *}
method_setup oghoare = {*
- Method.no_args (SIMPLE_METHOD' oghoare_tac) *}
+ Scan.succeed (K (SIMPLE_METHOD' oghoare_tac)) *}
"verification condition generator for the oghoare logic"
method_setup annhoare = {*
- Method.no_args (SIMPLE_METHOD' annhoare_tac) *}
+ Scan.succeed (K (SIMPLE_METHOD' annhoare_tac)) *}
"verification condition generator for the ann_hoare logic"
method_setup interfree_aux = {*
- Method.no_args (SIMPLE_METHOD' interfree_aux_tac) *}
+ Scan.succeed (K (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 (SIMPLE_METHOD' (conjI_Tac (K all_tac))) *}
+ Scan.succeed (K (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 (SIMPLE_METHOD' (disjE_Tac (K all_tac))) *}
+ Scan.succeed (K (SIMPLE_METHOD' (disjE_Tac (K all_tac)))) *}
"verification condition generator for interference freedom tests"
end
--- a/src/HOL/Isar_examples/Hoare.thy Mon Mar 16 14:26:30 2009 +0100
+++ b/src/HOL/Isar_examples/Hoare.thy Mon Mar 16 18:24:39 2009 +0100
@@ -454,7 +454,7 @@
use "~~/src/HOL/Hoare/hoare_tac.ML"
method_setup hoare = {*
- Method.ctxt_args (fn ctxt =>
+ Scan.succeed (fn ctxt =>
(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 Mon Mar 16 14:26:30 2009 +0100
+++ b/src/HOL/Library/Euclidean_Space.thy Mon Mar 16 18:24:39 2009 +0100
@@ -134,8 +134,8 @@
(* 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 (SIMPLE_METHOD' o vector_arith_tac)
-end
+ Attrib.thms >> (fn ths => K (SIMPLE_METHOD' (vector_arith_tac ths)))
+ end
*} "Lifts trivial vector statements to real arith statements"
lemma vec_0[simp]: "vec 0 = 0" by (vector vector_zero_def)
@@ -948,7 +948,7 @@
use "normarith.ML"
-method_setup norm = {* Method.ctxt_args (SIMPLE_METHOD' o NormArith.norm_arith_tac)
+method_setup norm = {* Scan.succeed (SIMPLE_METHOD' o NormArith.norm_arith_tac)
*} "Proves simple linear statements about vector norms"
--- a/src/HOL/Library/Eval_Witness.thy Mon Mar 16 14:26:30 2009 +0100
+++ b/src/HOL/Library/Eval_Witness.thy Mon Mar 16 18:24:39 2009 +0100
@@ -1,7 +1,5 @@
(* Title: HOL/Library/Eval_Witness.thy
- ID: $Id$
Author: Alexander Krauss, TU Muenchen
-
*)
header {* Evaluation Oracle with ML witnesses *}
@@ -78,15 +76,10 @@
method_setup eval_witness = {*
-let
-
-fun eval_tac ws = CSUBGOAL (fn (ct, i) => rtac (eval_witness_oracle (ct, ws)) i)
-
-in
- Method.simple_args (Scan.repeat Args.name) (fn ws => fn _ =>
- SIMPLE_METHOD' (eval_tac ws))
-end
-*} "Evaluation with ML witnesses"
+ Scan.lift (Scan.repeat Args.name) >>
+ (fn ws => K (SIMPLE_METHOD'
+ (CSUBGOAL (fn (ct, i) => rtac (eval_witness_oracle (ct, ws)) i))))
+*} "evaluation with ML witnesses"
subsection {* Toy Examples *}
--- a/src/HOL/Library/Reflection.thy Mon Mar 16 14:26:30 2009 +0100
+++ b/src/HOL/Library/Reflection.thy Mon Mar 16 18:24:39 2009 +0100
@@ -16,10 +16,10 @@
use "reflection.ML"
-method_setup reify = {* fn src =>
- Method.syntax (Attrib.thms --
- Scan.option (Scan.lift (Args.$$$ "(") |-- Args.term --| Scan.lift (Args.$$$ ")") )) src #>
- (fn ((eqs, to), ctxt) => SIMPLE_METHOD' (Reflection.genreify_tac ctxt (eqs @ (fst (Reify_Data.get ctxt))) to))
+method_setup reify = {*
+ Attrib.thms --
+ Scan.option (Scan.lift (Args.$$$ "(") |-- Args.term --| Scan.lift (Args.$$$ ")")) >>
+ (fn (eqs, to) => fn ctxt => SIMPLE_METHOD' (Reflection.genreify_tac ctxt (eqs @ (fst (Reify_Data.get ctxt))) to))
*} "partial automatic reification"
method_setup reflection = {*
@@ -30,16 +30,17 @@
val any_keyword = keyword onlyN || keyword rulesN;
val thms = Scan.repeat (Scan.unless any_keyword Attrib.multi_thm) >> flat;
val terms = thms >> map (term_of o Drule.dest_term);
- fun optional scan = Scan.optional scan [];
-in fn src =>
- Method.syntax (thms -- optional (keyword rulesN |-- thms) -- Scan.option (keyword onlyN |-- Args.term)) src #>
- (fn (((eqs,ths),to), ctxt) =>
- let
- val (ceqs,cths) = Reify_Data.get ctxt
- val corr_thms = ths@cths
- val raw_eqs = eqs@ceqs
- in SIMPLE_METHOD' (Reflection.reflection_tac ctxt corr_thms raw_eqs to)
- end) end
-*} "reflection method"
+in
+ thms --
+ Scan.optional (keyword rulesN |-- thms) [] --
+ Scan.option (keyword onlyN |-- Args.term) >>
+ (fn ((eqs,ths),to) => fn ctxt =>
+ let
+ val (ceqs,cths) = Reify_Data.get ctxt
+ val corr_thms = ths@cths
+ val raw_eqs = eqs@ceqs
+ in SIMPLE_METHOD' (Reflection.reflection_tac ctxt corr_thms raw_eqs to) end)
+end
+*} "reflection"
end
--- a/src/HOL/Library/Topology_Euclidean_Space.thy Mon Mar 16 14:26:30 2009 +0100
+++ b/src/HOL/Library/Topology_Euclidean_Space.thy Mon Mar 16 18:24:39 2009 +0100
@@ -978,9 +978,8 @@
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 (SIMPLE_METHOD' o tac) end
-
-*} "Reduces goals about net"
+ in Attrib.thms >> (fn ths => K (SIMPLE_METHOD' (tac ths))) end
+*} "reduces goals about net"
lemma at: "\<And>x y. netord (at a) x y \<longleftrightarrow> 0 < dist x a \<and> dist x a <= dist y a"
apply (net at_def)
--- a/src/HOL/Nominal/nominal_fresh_fun.ML Mon Mar 16 14:26:30 2009 +0100
+++ b/src/HOL/Nominal/nominal_fresh_fun.ML Mon Mar 16 18:24:39 2009 +0100
@@ -199,9 +199,10 @@
(Args.parens (Args.$$$ "no_asm") >> (K true)) ||
(Scan.succeed false);
-val setup_generate_fresh =
- Method.goal_args_ctxt' Args.tyname (fn ctxt => generate_fresh_tac)
+fun setup_generate_fresh x =
+ (Args.goal_spec -- Args.tyname >>
+ (fn (quant, s) => K (SIMPLE_METHOD'' quant (generate_fresh_tac s)))) x;
-val setup_fresh_fun_simp =
- Method.simple_args options_syntax
- (fn b => fn _ => SIMPLE_METHOD (fresh_fun_tac b 1))
+fun setup_fresh_fun_simp x =
+ (Scan.lift options_syntax >> (fn b => K (SIMPLE_METHOD' (fresh_fun_tac b)))) x;
+
--- a/src/HOL/Nominal/nominal_induct.ML Mon Mar 16 14:26:30 2009 +0100
+++ b/src/HOL/Nominal/nominal_induct.ML Mon Mar 16 18:24:39 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 -> Proof.method
+ val nominal_induct_method: (Proof.context -> Proof.method) context_parser
end =
struct
@@ -152,11 +152,10 @@
in
-fun nominal_induct_method src =
- Method.syntax
- (P.and_list' (Scan.repeat (unless_more_args def_inst)) --
- avoiding -- fixing -- rule_spec) src
- #> (fn ((((x, y), z), w), ctxt) =>
+val nominal_induct_method =
+ P.and_list' (Scan.repeat (unless_more_args def_inst)) --
+ avoiding -- fixing -- rule_spec >>
+ (fn (((x, y), z), w) => fn ctxt =>
RAW_METHOD_CASES (fn facts =>
HEADGOAL (nominal_induct_tac ctxt x y z w facts)));
--- a/src/HOL/Nominal/nominal_permeq.ML Mon Mar 16 14:26:30 2009 +0100
+++ b/src/HOL/Nominal/nominal_permeq.ML Mon Mar 16 18:24:39 2009 +0100
@@ -1,5 +1,4 @@
(* Title: HOL/Nominal/nominal_permeq.ML
- ID: $Id$
Authors: Christian Urban, Julien Narboux, TU Muenchen
Methods for simplifying permutations and
@@ -36,16 +35,16 @@
val finite_guess_tac : simpset -> int -> tactic
val fresh_guess_tac : simpset -> int -> tactic
- val perm_simp_meth : Method.src -> Proof.context -> Proof.method
- val perm_simp_meth_debug : Method.src -> Proof.context -> Proof.method
- val perm_extend_simp_meth : Method.src -> Proof.context -> Proof.method
- val perm_extend_simp_meth_debug : Method.src -> Proof.context -> Proof.method
- val supports_meth : Method.src -> Proof.context -> Proof.method
- val supports_meth_debug : Method.src -> Proof.context -> Proof.method
- val finite_guess_meth : Method.src -> Proof.context -> Proof.method
- val finite_guess_meth_debug : Method.src -> Proof.context -> Proof.method
- val fresh_guess_meth : Method.src -> Proof.context -> Proof.method
- val fresh_guess_meth_debug : Method.src -> Proof.context -> Proof.method
+ val perm_simp_meth : (Proof.context -> Proof.method) context_parser
+ val perm_simp_meth_debug : (Proof.context -> Proof.method) context_parser
+ val perm_extend_simp_meth : (Proof.context -> Proof.method) context_parser
+ val perm_extend_simp_meth_debug : (Proof.context -> Proof.method) context_parser
+ val supports_meth : (Proof.context -> Proof.method) context_parser
+ val supports_meth_debug : (Proof.context -> Proof.method) context_parser
+ val finite_guess_meth : (Proof.context -> Proof.method) context_parser
+ val finite_guess_meth_debug : (Proof.context -> Proof.method) context_parser
+ val fresh_guess_meth : (Proof.context -> Proof.method) context_parser
+ val fresh_guess_meth_debug : (Proof.context -> Proof.method) context_parser
end
structure NominalPermeq : NOMINAL_PERMEQ =
@@ -400,26 +399,24 @@
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 (fn facts =>
- HEADGOAL (Method.insert_tac (prems @ facts) THEN'
- ((CHANGED_PROP) oo tac) (local_simpset_of ctxt)));
-
-val perm_simp_meth = Method.sectioned_args
- (Args.bang_facts -- Scan.lift perm_simp_options)
- (Simplifier.simp_modifiers') perm_simp_method
+val perm_simp_meth =
+ Args.bang_facts -- Scan.lift perm_simp_options --|
+ Method.sections (Simplifier.simp_modifiers') >>
+ (fn (prems, tac) => fn ctxt => METHOD (fn facts =>
+ HEADGOAL (Method.insert_tac (prems @ facts) THEN'
+ (CHANGED_PROP oo tac) (local_simpset_of ctxt))));
(* 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)
- (SIMPLE_METHOD' o tac o local_simpset_of) ;
+ Method.sections (Simplifier.simp_modifiers' @ Splitter.split_modifiers) >>
+ (K (SIMPLE_METHOD' o tac o local_simpset_of));
(* uses HOL_basic_ss only and fails if the tactic does not solve the subgoal *)
fun basic_simp_meth_setup debug tac =
- Method.sectioned_args
- (fn (ctxt,l) => ((),((Simplifier.map_ss (fn _ => HOL_basic_ss) ctxt),l)))
- (Simplifier.simp_modifiers' @ Splitter.split_modifiers)
- (fn _ => SIMPLE_METHOD' o (fn ss => if debug then (tac ss) else SOLVEI (tac ss)) o local_simpset_of);
+ Scan.depend (fn ctxt => Scan.succeed (Simplifier.map_ss (fn _ => HOL_basic_ss) ctxt, ())) --
+ Method.sections (Simplifier.simp_modifiers' @ Splitter.split_modifiers) >>
+ (K (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/Presburger.thy Mon Mar 16 14:26:30 2009 +0100
+++ b/src/HOL/Presburger.thy Mon Mar 16 18:24:39 2009 +0100
@@ -455,12 +455,11 @@
val any_keyword = keyword addN || keyword delN || simple_keyword elimN
val thms = Scan.repeat (Scan.unless any_keyword Attrib.multi_thm) >> flat;
in
- fn src => Method.syntax
- ((Scan.optional (simple_keyword elimN >> K false) true) --
- (Scan.optional (keyword addN |-- thms) []) --
- (Scan.optional (keyword delN |-- thms) [])) src
- #> (fn (((elim, add_ths), del_ths),ctxt) =>
- SIMPLE_METHOD' (Presburger.cooper_tac elim add_ths del_ths ctxt))
+ Scan.optional (simple_keyword elimN >> K false) true --
+ Scan.optional (keyword addN |-- thms) [] --
+ Scan.optional (keyword delN |-- thms) [] >>
+ (fn ((elim, add_ths), del_ths) => fn 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 Mon Mar 16 14:26:30 2009 +0100
+++ b/src/HOL/Prolog/HOHH.thy Mon Mar 16 18:24:39 2009 +0100
@@ -11,11 +11,11 @@
begin
method_setup ptac =
- {* Method.thms_ctxt_args (fn thms => fn ctxt => SIMPLE_METHOD' (Prolog.ptac ctxt thms)) *}
+ {* Attrib.thms >> (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 => SIMPLE_METHOD (Prolog.prolog_tac ctxt thms)) *}
+ {* Attrib.thms >> (fn thms => fn ctxt => SIMPLE_METHOD (Prolog.prolog_tac ctxt thms)) *}
"Lambda Prolog interpreter"
consts
--- a/src/HOL/SAT.thy Mon Mar 16 14:26:30 2009 +0100
+++ b/src/HOL/SAT.thy Mon Mar 16 18:24:39 2009 +0100
@@ -1,5 +1,4 @@
(* Title: HOL/SAT.thy
- ID: $Id$
Author: Alwen Tiu, Tjark Weber
Copyright 2005
@@ -28,10 +27,10 @@
ML {* structure sat = SATFunc(structure cnf = cnf); *}
-method_setup sat = {* Method.no_args (SIMPLE_METHOD' sat.sat_tac) *}
+method_setup sat = {* Scan.succeed (K (SIMPLE_METHOD' sat.sat_tac)) *}
"SAT solver"
-method_setup satx = {* Method.no_args (SIMPLE_METHOD' sat.satx_tac) *}
+method_setup satx = {* Scan.succeed (K (SIMPLE_METHOD' sat.satx_tac)) *}
"SAT solver (with definitional CNF)"
end
--- a/src/HOL/SET-Protocol/Cardholder_Registration.thy Mon Mar 16 14:26:30 2009 +0100
+++ b/src/HOL/SET-Protocol/Cardholder_Registration.thy Mon Mar 16 18:24:39 2009 +0100
@@ -541,10 +541,11 @@
by (blast intro: analz_mono [THEN [2] rev_subsetD])
method_setup valid_certificate_tac = {*
- Method.goal_args (Scan.succeed ()) (fn () => fn i =>
- EVERY [ftac @{thm Gets_certificate_valid} i,
- assume_tac i,
- etac conjE i, REPEAT (hyp_subst_tac i)])
+ Args.goal_spec >> (fn quant => K (SIMPLE_METHOD'' quant
+ (fn i =>
+ EVERY [ftac @{thm Gets_certificate_valid} i,
+ assume_tac i,
+ etac conjE i, REPEAT (hyp_subst_tac i)])))
*} ""
text{*The @{text "(no_asm)"} attribute is essential, since it retains
--- a/src/HOL/SET-Protocol/EventSET.thy Mon Mar 16 14:26:30 2009 +0100
+++ b/src/HOL/SET-Protocol/EventSET.thy Mon Mar 16 18:24:39 2009 +0100
@@ -189,7 +189,7 @@
*}
method_setup analz_mono_contra = {*
- Method.no_args (SIMPLE_METHOD (REPEAT_FIRST analz_mono_contra_tac)) *}
+ Scan.succeed (K (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 Mon Mar 16 14:26:30 2009 +0100
+++ b/src/HOL/SET-Protocol/MessageSET.thy Mon Mar 16 18:24:39 2009 +0100
@@ -940,17 +940,17 @@
lemmas Fake_parts_sing_imp_Un = Fake_parts_sing [THEN [2] rev_subsetD]
method_setup spy_analz = {*
- Method.ctxt_args (fn ctxt =>
+ Scan.succeed (fn 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 =>
+ Scan.succeed (fn 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 =>
+ Scan.succeed (fn ctxt =>
SIMPLE_METHOD' (MessageSET.Fake_insert_simp_tac (local_simpset_of ctxt))) *}
"for debugging spy_analz"
--- a/src/HOL/SET-Protocol/PublicSET.thy Mon Mar 16 14:26:30 2009 +0100
+++ b/src/HOL/SET-Protocol/PublicSET.thy Mon Mar 16 18:24:39 2009 +0100
@@ -371,7 +371,7 @@
*}
method_setup possibility = {*
- Method.ctxt_args (fn ctxt =>
+ Scan.succeed (fn ctxt =>
SIMPLE_METHOD (PublicSET.gen_possibility_tac (local_simpset_of ctxt))) *}
"for proving possibility theorems"
--- a/src/HOL/SET-Protocol/Purchase.thy Mon Mar 16 14:26:30 2009 +0100
+++ b/src/HOL/SET-Protocol/Purchase.thy Mon Mar 16 18:24:39 2009 +0100
@@ -477,9 +477,10 @@
by (frule Gets_imp_Says, auto)
method_setup valid_certificate_tac = {*
- Method.goal_args (Scan.succeed ()) (fn () => fn i =>
- EVERY [ftac @{thm Gets_certificate_valid} i,
- assume_tac i, REPEAT (hyp_subst_tac i)])
+ Args.goal_spec >> (fn quant =>
+ K (SIMPLE_METHOD'' quant (fn i =>
+ EVERY [ftac @{thm Gets_certificate_valid} i,
+ assume_tac i, REPEAT (hyp_subst_tac i)])))
*} ""
--- a/src/HOL/Transitive_Closure.thy Mon Mar 16 14:26:30 2009 +0100
+++ b/src/HOL/Transitive_Closure.thy Mon Mar 16 18:24:39 2009 +0100
@@ -695,16 +695,16 @@
(* Optional methods *)
method_setup trancl =
- {* Method.no_args (SIMPLE_METHOD' Trancl_Tac.trancl_tac) *}
+ {* Scan.succeed (K (SIMPLE_METHOD' Trancl_Tac.trancl_tac)) *}
{* simple transitivity reasoner *}
method_setup rtrancl =
- {* Method.no_args (SIMPLE_METHOD' Trancl_Tac.rtrancl_tac) *}
+ {* Scan.succeed (K (SIMPLE_METHOD' Trancl_Tac.rtrancl_tac)) *}
{* simple transitivity reasoner *}
method_setup tranclp =
- {* Method.no_args (SIMPLE_METHOD' Tranclp_Tac.trancl_tac) *}
+ {* Scan.succeed (K (SIMPLE_METHOD' Tranclp_Tac.trancl_tac)) *}
{* simple transitivity reasoner (predicate version) *}
method_setup rtranclp =
- {* Method.no_args (SIMPLE_METHOD' Tranclp_Tac.rtrancl_tac) *}
+ {* Scan.succeed (K (SIMPLE_METHOD' Tranclp_Tac.rtrancl_tac)) *}
{* simple transitivity reasoner (predicate version) *}
end
--- a/src/HOL/UNITY/Comp/Alloc.thy Mon Mar 16 14:26:30 2009 +0100
+++ b/src/HOL/UNITY/Comp/Alloc.thy Mon Mar 16 18:24:39 2009 +0100
@@ -321,7 +321,7 @@
*}
method_setup record_auto = {*
- Method.ctxt_args (fn ctxt => SIMPLE_METHOD (record_auto_tac (local_clasimpset_of ctxt)))
+ Scan.succeed (fn ctxt => SIMPLE_METHOD (record_auto_tac (local_clasimpset_of ctxt)))
*} ""
lemma inj_sysOfAlloc [iff]: "inj sysOfAlloc"
@@ -713,7 +713,7 @@
*}
method_setup rename_client_map = {*
- Method.ctxt_args (fn ctxt =>
+ Scan.succeed (fn ctxt =>
SIMPLE_METHOD (rename_client_map_tac (local_simpset_of ctxt)))
*} ""
--- a/src/HOL/UNITY/Simple/NSP_Bad.thy Mon Mar 16 14:26:30 2009 +0100
+++ b/src/HOL/UNITY/Simple/NSP_Bad.thy Mon Mar 16 18:24:39 2009 +0100
@@ -124,7 +124,7 @@
*}
method_setup ns_induct = {*
- Method.ctxt_args (fn ctxt =>
+ Scan.succeed (fn ctxt =>
SIMPLE_METHOD' (ns_induct_tac (local_clasimpset_of ctxt))) *}
"for inductive reasoning about the Needham-Schroeder protocol"
--- a/src/HOL/UNITY/UNITY_Main.thy Mon Mar 16 14:26:30 2009 +0100
+++ b/src/HOL/UNITY/UNITY_Main.thy Mon Mar 16 18:24:39 2009 +0100
@@ -10,15 +10,13 @@
uses "UNITY_tactics.ML" begin
method_setup safety = {*
- Method.ctxt_args (fn ctxt =>
+ Scan.succeed (fn ctxt =>
SIMPLE_METHOD' (constrains_tac (local_clasimpset_of ctxt))) *}
"for proving safety properties"
method_setup ensures_tac = {*
- fn args => fn ctxt =>
- Method.goal_args' (Scan.lift Args.name_source)
- (ensures_tac (local_clasimpset_of ctxt))
- args ctxt *}
- "for proving progress properties"
+ Args.goal_spec -- Scan.lift Args.name_source >>
+ (fn (quant, s) => fn ctxt => SIMPLE_METHOD'' quant (ensures_tac (local_clasimpset_of ctxt) s))
+*} "for proving progress properties"
end
--- a/src/HOL/Word/WordArith.thy Mon Mar 16 14:26:30 2009 +0100
+++ b/src/HOL/Word/WordArith.thy Mon Mar 16 18:24:39 2009 +0100
@@ -530,7 +530,7 @@
*}
method_setup uint_arith =
- "Method.ctxt_args (SIMPLE_METHOD' o uint_arith_tac)"
+ {* Scan.succeed (SIMPLE_METHOD' o uint_arith_tac) *}
"solving word arithmetic via integers and arith"
@@ -1086,7 +1086,7 @@
*}
method_setup unat_arith =
- "Method.ctxt_args (SIMPLE_METHOD' o unat_arith_tac)"
+ {* Scan.succeed (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 Mon Mar 16 14:26:30 2009 +0100
+++ b/src/HOL/ex/Binary.thy Mon Mar 16 18:24:39 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 (SIMPLE_METHOD'
+ Scan.succeed (K (SIMPLE_METHOD'
(full_simp_tac
(HOL_basic_ss
addsimps @{thms binary_simps}
@@ -183,7 +183,7 @@
@{simproc binary_nat_less},
@{simproc binary_nat_diff},
@{simproc binary_nat_div},
- @{simproc binary_nat_mod}])))
+ @{simproc binary_nat_mod}]))))
*} "binary simplification"
--- a/src/HOL/ex/SAT_Examples.thy Mon Mar 16 14:26:30 2009 +0100
+++ b/src/HOL/ex/SAT_Examples.thy Mon Mar 16 18:24:39 2009 +0100
@@ -83,7 +83,7 @@
ML {* reset quick_and_dirty; *}
method_setup rawsat =
- {* Method.no_args (SIMPLE_METHOD' sat.rawsat_tac) *}
+ {* Scan.succeed (K (SIMPLE_METHOD' sat.rawsat_tac)) *}
"SAT solver (no preprocessing)"
(* ML {* Toplevel.profiling := 1; *} *)
--- a/src/Pure/Isar/attrib.ML Mon Mar 16 14:26:30 2009 +0100
+++ b/src/Pure/Isar/attrib.ML Mon Mar 16 18:24:39 2009 +0100
@@ -26,7 +26,7 @@
val add_attributes: (bstring * (src -> attribute) * string) list -> theory -> theory
val syntax: attribute context_parser -> src -> attribute
val setup: Binding.binding -> attribute context_parser -> string -> theory -> theory
- val attribute_setup: string * Position.T -> string * Position.T -> string -> theory -> theory
+ val attribute_setup: bstring * Position.T -> string * Position.T -> string -> theory -> theory
val no_args: attribute -> src -> attribute
val add_del: attribute -> attribute -> attribute context_parser
val add_del_args: attribute -> attribute -> src -> attribute
--- a/src/Pure/Isar/isar_syn.ML Mon Mar 16 14:26:30 2009 +0100
+++ b/src/Pure/Isar/isar_syn.ML Mon Mar 16 18:24:39 2009 +0100
@@ -334,7 +334,7 @@
val _ =
OuterSyntax.command "method_setup" "define proof method in ML" (K.tag_ml K.thy_decl)
- (P.name -- P.!!! (P.$$$ "=" |-- P.ML_source -- P.text)
+ (P.position P.name -- P.!!! (P.$$$ "=" |-- P.ML_source -- P.text)
>> (fn (name, (txt, cmt)) => Toplevel.theory (Method.method_setup name txt cmt)));
val _ =
--- a/src/Pure/Isar/method.ML Mon Mar 16 14:26:30 2009 +0100
+++ b/src/Pure/Isar/method.ML Mon Mar 16 18:24:39 2009 +0100
@@ -80,7 +80,7 @@
-> 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 method_setup: bstring * Position.T -> string * Position.T -> string -> theory -> theory
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
@@ -404,9 +404,9 @@
fun method_setup name (txt, pos) cmt =
Context.theory_map (ML_Context.expression pos
- "val method: bstring * (Method.src -> Proof.context -> Proof.method) * string"
- "Context.map_theory (Method.add_method method)"
- ("(" ^ quote name ^ ", " ^ txt ^ ", " ^ quote cmt ^ ")"));
+ "val (name, scan, comment): binding * (Proof.context -> Proof.method) context_parser * string"
+ "Context.map_theory (Method.setup name scan comment)"
+ ("(" ^ ML_Syntax.make_binding name ^ ", " ^ txt ^ ", " ^ ML_Syntax.print_string cmt ^ ")"));
--- a/src/Pure/Isar/rule_insts.ML Mon Mar 16 14:26:30 2009 +0100
+++ b/src/Pure/Isar/rule_insts.ML Mon Mar 16 18:24:39 2009 +0100
@@ -16,6 +16,8 @@
val thin_tac: Proof.context -> string -> int -> tactic
val subgoal_tac: Proof.context -> string -> int -> tactic
val subgoals_tac: Proof.context -> string list -> int -> tactic
+ val method: (Proof.context -> (indexname * string) list -> thm -> int -> tactic) ->
+ (thm list -> int -> tactic) -> (Proof.context -> Proof.method) context_parser
end;
signature RULE_INSTS =
@@ -383,9 +385,7 @@
(* rule_tac etc. -- refer to dynamic goal state! *)
-local
-
-fun inst_meth inst_tac tac =
+fun method inst_tac tac =
Args.goal_spec --
Scan.optional (Scan.lift
(P.and_list1 (Args.var -- (Args.$$$ "=" |-- P.!!! Args.name_source)) --| Args.$$$ "in")) [] --
@@ -397,15 +397,11 @@
[thm] => quant (Method.insert_tac facts THEN' inst_tac ctxt insts thm)
| _ => error "Cannot have instantiations with multiple rules")));
-in
-
-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;
+val res_inst_meth = method res_inst_tac Tactic.resolve_tac;
+val eres_inst_meth = method eres_inst_tac Tactic.eresolve_tac;
+val cut_inst_meth = method cut_inst_tac Tactic.cut_rules_tac;
+val dres_inst_meth = method dres_inst_tac Tactic.dresolve_tac;
+val forw_inst_meth = method forw_inst_tac Tactic.forward_tac;
(* setup *)
--- a/src/Sequents/ILL.thy Mon Mar 16 14:26:30 2009 +0100
+++ b/src/Sequents/ILL.thy Mon Mar 16 18:24:39 2009 +0100
@@ -146,7 +146,7 @@
*}
method_setup best_lazy =
- {* Method.no_args (SIMPLE_METHOD' (best_tac lazy_cs)) *}
+ {* Scan.succeed (K (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 (SIMPLE_METHOD' (best_tac safe_cs)) *} ""
+ {* Scan.succeed (K (SIMPLE_METHOD' (best_tac safe_cs))) *} ""
method_setup best_power =
- {* Method.no_args (SIMPLE_METHOD' (best_tac power_cs)) *} ""
+ {* Scan.succeed (K (SIMPLE_METHOD' (best_tac power_cs))) *} ""
(* Some examples from Troelstra and van Dalen *)
--- a/src/Sequents/LK0.thy Mon Mar 16 14:26:30 2009 +0100
+++ b/src/Sequents/LK0.thy Mon Mar 16 18:24:39 2009 +0100
@@ -240,23 +240,23 @@
*}
method_setup fast_prop =
- {* Method.no_args (SIMPLE_METHOD' (fast_tac prop_pack)) *}
+ {* Scan.succeed (K (SIMPLE_METHOD' (fast_tac prop_pack))) *}
"propositional reasoning"
method_setup fast =
- {* Method.no_args (SIMPLE_METHOD' (fast_tac LK_pack)) *}
+ {* Scan.succeed (K (SIMPLE_METHOD' (fast_tac LK_pack))) *}
"classical reasoning"
method_setup fast_dup =
- {* Method.no_args (SIMPLE_METHOD' (fast_tac LK_dup_pack)) *}
+ {* Scan.succeed (K (SIMPLE_METHOD' (fast_tac LK_dup_pack))) *}
"classical reasoning"
method_setup best =
- {* Method.no_args (SIMPLE_METHOD' (best_tac LK_pack)) *}
+ {* Scan.succeed (K (SIMPLE_METHOD' (best_tac LK_pack))) *}
"classical reasoning"
method_setup best_dup =
- {* Method.no_args (SIMPLE_METHOD' (best_tac LK_dup_pack)) *}
+ {* Scan.succeed (K (SIMPLE_METHOD' (best_tac LK_dup_pack))) *}
"classical reasoning"
--- a/src/Sequents/S4.thy Mon Mar 16 14:26:30 2009 +0100
+++ b/src/Sequents/S4.thy Mon Mar 16 18:24:39 2009 +0100
@@ -45,7 +45,7 @@
*}
method_setup S4_solve =
- {* Method.no_args (SIMPLE_METHOD (S4_Prover.solve_tac 2)) *} "S4 solver"
+ {* Scan.succeed (K (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 Mon Mar 16 14:26:30 2009 +0100
+++ b/src/Sequents/S43.thy Mon Mar 16 18:24:39 2009 +0100
@@ -92,8 +92,8 @@
method_setup S43_solve = {*
- Method.no_args (SIMPLE_METHOD
- (S43_Prover.solve_tac 2 ORELSE S43_Prover.solve_tac 3))
+ Scan.succeed (K (SIMPLE_METHOD
+ (S43_Prover.solve_tac 2 ORELSE S43_Prover.solve_tac 3)))
*} "S4 solver"
--- a/src/Sequents/T.thy Mon Mar 16 14:26:30 2009 +0100
+++ b/src/Sequents/T.thy Mon Mar 16 18:24:39 2009 +0100
@@ -44,7 +44,7 @@
*}
method_setup T_solve =
- {* Method.no_args (SIMPLE_METHOD (T_Prover.solve_tac 2)) *} "T solver"
+ {* Scan.succeed (K (SIMPLE_METHOD (T_Prover.solve_tac 2))) *} "T solver"
(* Theorems of system T from Hughes and Cresswell and Hailpern, LNCS 129 *)
--- a/src/ZF/UNITY/Constrains.thy Mon Mar 16 14:26:30 2009 +0100
+++ b/src/ZF/UNITY/Constrains.thy Mon Mar 16 18:24:39 2009 +0100
@@ -496,11 +496,11 @@
setup ProgramDefs.setup
method_setup safety = {*
- Method.ctxt_args (SIMPLE_METHOD' o constrains_tac) *}
+ Scan.succeed (SIMPLE_METHOD' o constrains_tac) *}
"for proving safety properties"
method_setup always = {*
- Method.ctxt_args (SIMPLE_METHOD' o always_tac) *}
+ Scan.succeed (SIMPLE_METHOD' o always_tac) *}
"for proving invariants"
end
--- a/src/ZF/UNITY/SubstAx.thy Mon Mar 16 14:26:30 2009 +0100
+++ b/src/ZF/UNITY/SubstAx.thy Mon Mar 16 18:24:39 2009 +0100
@@ -377,9 +377,8 @@
*}
method_setup ensures_tac = {*
- fn args => fn ctxt =>
- Method.goal_args' (Scan.lift Args.name_source) (ensures_tac ctxt)
- args ctxt *}
- "for proving progress properties"
+ Args.goal_spec -- Scan.lift Args.name_source >>
+ (fn (quant, s) => fn ctxt => SIMPLE_METHOD'' quant (ensures_tac ctxt s))
+*} "for proving progress properties"
end