# HG changeset patch # User wenzelm # Date 1237224279 -3600 # Node ID c601204b055c3a3f21742bc26fd2fe8fdec0bba9 # Parent eb720644facd3aa90eba921a26ef234bf4645ebf# Parent d2d7874648bda047741356da04c9ead1290ff72c merged diff -r eb720644facd -r c601204b055c NEWS --- 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 diff -r eb720644facd -r c601204b055c doc-src/IsarRef/Thy/Proof.thy --- 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} \\ diff -r eb720644facd -r c601204b055c doc-src/IsarRef/Thy/Spec.thy --- 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 diff -r eb720644facd -r c601204b055c doc-src/IsarRef/Thy/document/Proof.tex --- 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} \\ diff -r eb720644facd -r c601204b055c doc-src/IsarRef/Thy/document/Spec.tex --- 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 diff -r eb720644facd -r c601204b055c doc-src/TutorialI/Protocol/Event.thy --- 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 \ 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 \ synth (analz (knows Spy evs)) --> P" (*>*) diff -r eb720644facd -r c601204b055c doc-src/TutorialI/Protocol/Message.thy --- 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" diff -r eb720644facd -r c601204b055c doc-src/TutorialI/Protocol/Public.thy --- 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 diff -r eb720644facd -r c601204b055c src/Cube/Example.thy --- 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))))) *} "" diff -r eb720644facd -r c601204b055c src/FOL/FOL.thy --- 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 *) diff -r eb720644facd -r c601204b055c src/FOL/ex/Iff_Oracle.thy --- 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)) diff -r eb720644facd -r c601204b055c src/HOL/Algebra/abstract/Ring2.thy --- 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 *} diff -r eb720644facd -r c601204b055c src/HOL/Auth/Event.thy --- 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 \ 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 \ synth (analz (knows Spy evs)) --> P" end diff -r eb720644facd -r c601204b055c src/HOL/Auth/Message.thy --- 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 diff -r eb720644facd -r c601204b055c src/HOL/Auth/OtwayReesBella.thy --- 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" diff -r eb720644facd -r c601204b055c src/HOL/Auth/Public.thy --- 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 diff -r eb720644facd -r c601204b055c src/HOL/Auth/Shared.thy --- 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)" diff -r eb720644facd -r c601204b055c src/HOL/Auth/Smartcard/ShoupRubin.thy --- 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]), diff -r eb720644facd -r c601204b055c src/HOL/Auth/Smartcard/ShoupRubinBella.thy --- 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}), diff -r eb720644facd -r c601204b055c src/HOL/Auth/Smartcard/Smartcard.thy --- 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" diff -r eb720644facd -r c601204b055c src/HOL/Code_Setup.thy --- 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" diff -r eb720644facd -r c601204b055c src/HOL/Decision_Procs/Approximation.thy --- 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 diff -r eb720644facd -r c601204b055c src/HOL/Decision_Procs/Dense_Linear_Order.thy --- 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 *} diff -r eb720644facd -r c601204b055c src/HOL/Groebner_Basis.thy --- 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" diff -r eb720644facd -r c601204b055c src/HOL/Hoare/Hoare.thy --- 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" diff -r eb720644facd -r c601204b055c src/HOL/Hoare/HoareAbort.thy --- 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" diff -r eb720644facd -r c601204b055c src/HOL/HoareParallel/OG_Tactics.thy --- 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 diff -r eb720644facd -r c601204b055c src/HOL/Isar_examples/Hoare.thy --- 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" diff -r eb720644facd -r c601204b055c src/HOL/Library/Euclidean_Space.thy --- 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" diff -r eb720644facd -r c601204b055c src/HOL/Library/Eval_Witness.thy --- 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 *} diff -r eb720644facd -r c601204b055c src/HOL/Library/Reflection.thy --- 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 diff -r eb720644facd -r c601204b055c src/HOL/Library/Topology_Euclidean_Space.thy --- 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: "\x y. netord (at a) x y \ 0 < dist x a \ dist x a <= dist y a" apply (net at_def) diff -r eb720644facd -r c601204b055c src/HOL/Nominal/nominal_fresh_fun.ML --- 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; + diff -r eb720644facd -r c601204b055c src/HOL/Nominal/nominal_induct.ML --- 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))); diff -r eb720644facd -r c601204b055c src/HOL/Nominal/nominal_permeq.ML --- 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; diff -r eb720644facd -r c601204b055c src/HOL/Presburger.thy --- 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" diff -r eb720644facd -r c601204b055c src/HOL/Prolog/HOHH.thy --- 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 diff -r eb720644facd -r c601204b055c src/HOL/SAT.thy --- 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 diff -r eb720644facd -r c601204b055c src/HOL/SET-Protocol/Cardholder_Registration.thy --- 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 diff -r eb720644facd -r c601204b055c src/HOL/SET-Protocol/EventSET.thy --- 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 \ analz (knows Spy evs) --> P" end diff -r eb720644facd -r c601204b055c src/HOL/SET-Protocol/MessageSET.thy --- 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" diff -r eb720644facd -r c601204b055c src/HOL/SET-Protocol/PublicSET.thy --- 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" diff -r eb720644facd -r c601204b055c src/HOL/SET-Protocol/Purchase.thy --- 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)]))) *} "" diff -r eb720644facd -r c601204b055c src/HOL/Transitive_Closure.thy --- 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 diff -r eb720644facd -r c601204b055c src/HOL/UNITY/Comp/Alloc.thy --- 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))) *} "" diff -r eb720644facd -r c601204b055c src/HOL/UNITY/Simple/NSP_Bad.thy --- 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" diff -r eb720644facd -r c601204b055c src/HOL/UNITY/UNITY_Main.thy --- 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 diff -r eb720644facd -r c601204b055c src/HOL/Word/WordArith.thy --- 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: diff -r eb720644facd -r c601204b055c src/HOL/ex/Binary.thy --- 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" diff -r eb720644facd -r c601204b055c src/HOL/ex/SAT_Examples.thy --- 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; *} *) diff -r eb720644facd -r c601204b055c src/Pure/Isar/attrib.ML --- 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 diff -r eb720644facd -r c601204b055c src/Pure/Isar/isar_syn.ML --- 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 _ = diff -r eb720644facd -r c601204b055c src/Pure/Isar/method.ML --- 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 ^ ")")); diff -r eb720644facd -r c601204b055c src/Pure/Isar/rule_insts.ML --- 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 *) diff -r eb720644facd -r c601204b055c src/Sequents/ILL.thy --- 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 *) diff -r eb720644facd -r c601204b055c src/Sequents/LK0.thy --- 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" diff -r eb720644facd -r c601204b055c src/Sequents/S4.thy --- 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 *) diff -r eb720644facd -r c601204b055c src/Sequents/S43.thy --- 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" diff -r eb720644facd -r c601204b055c src/Sequents/T.thy --- 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 *) diff -r eb720644facd -r c601204b055c src/ZF/UNITY/Constrains.thy --- 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 diff -r eb720644facd -r c601204b055c src/ZF/UNITY/SubstAx.thy --- 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