# HG changeset patch # User wenzelm # Date 1237222284 -3600 # Node ID 2eef5e71edd6bfebb3fbce2e67c4c5dbc4a6dc7f # Parent 4c25146258732176ebdd15dc28ffd1a17010da12 updated generated file; diff -r 4c2514625873 -r 2eef5e71edd6 doc-src/IsarRef/Thy/document/Proof.tex --- a/doc-src/IsarRef/Thy/document/Proof.tex Mon Mar 16 17:51:07 2009 +0100 +++ b/doc-src/IsarRef/Thy/document/Proof.tex Mon Mar 16 17:51:24 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 4c2514625873 -r 2eef5e71edd6 doc-src/IsarRef/Thy/document/Spec.tex --- a/doc-src/IsarRef/Thy/document/Spec.tex Mon Mar 16 17:51:07 2009 +0100 +++ b/doc-src/IsarRef/Thy/document/Spec.tex Mon Mar 16 17:51:24 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 4c2514625873 -r 2eef5e71edd6 doc-src/TutorialI/Protocol/Event.thy --- a/doc-src/TutorialI/Protocol/Event.thy Mon Mar 16 17:51:07 2009 +0100 +++ b/doc-src/TutorialI/Protocol/Event.thy Mon Mar 16 17:51:24 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 4c2514625873 -r 2eef5e71edd6 doc-src/TutorialI/Protocol/Message.thy --- a/doc-src/TutorialI/Protocol/Message.thy Mon Mar 16 17:51:07 2009 +0100 +++ b/doc-src/TutorialI/Protocol/Message.thy Mon Mar 16 17:51:24 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 4c2514625873 -r 2eef5e71edd6 doc-src/TutorialI/Protocol/Public.thy --- a/doc-src/TutorialI/Protocol/Public.thy Mon Mar 16 17:51:07 2009 +0100 +++ b/doc-src/TutorialI/Protocol/Public.thy Mon Mar 16 17:51:24 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