--- 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} \\
--- 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
--- 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 \<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 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"
--- 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