--- a/doc-src/IsarRef/Thy/HOL_Specific.thy Tue Nov 08 08:56:24 2011 +0100
+++ b/doc-src/IsarRef/Thy/HOL_Specific.thy Tue Nov 08 10:33:30 2011 +0100
@@ -1758,7 +1758,8 @@
@{command_def (HOL) "code_monad"} & : & @{text "theory \<rightarrow> theory"} \\
@{command_def (HOL) "code_include"} & : & @{text "theory \<rightarrow> theory"} \\
@{command_def (HOL) "code_modulename"} & : & @{text "theory \<rightarrow> theory"} \\
- @{command_def (HOL) "code_reflect"} & : & @{text "theory \<rightarrow> theory"}
+ @{command_def (HOL) "code_reflect"} & : & @{text "theory \<rightarrow> theory"} \\
+ @{command_def (HOL) "code_pred"} & : & @{text "theory \<rightarrow> proof(prove)"}
\end{matharray}
@{rail "
@@ -1839,7 +1840,17 @@
( @'functions' ( @{syntax string} + ) ) ? ( @'file' @{syntax string} ) ?
;
+ @@{command (HOL) code_pred} \\( '(' @'modes' ':' modedecl ')')? \\ const
+ ;
+
syntax: @{syntax string} | ( @'infix' | @'infixl' | @'infixr' ) @{syntax nat} @{syntax string}
+ ;
+
+ modedecl: (modes | ((const ':' modes) \\
+ (@'and' ((const ':' modes @'and') +))?))
+ ;
+
+ modes: mode @'as' const
"}
\begin{description}
@@ -1955,6 +1966,12 @@
is generated into that specified file without modifying the code
generator setup.
+ \item @{command (HOL) "code_pred"} creates code equations for a predicate
+ given a set of introduction rules. Optional mode annotations determine
+ which arguments are supposed to be input or output. If alternative
+ introduction rules are declared, one must prove a corresponding elimination
+ rule.
+
\end{description}
*}
--- a/doc-src/IsarRef/Thy/document/HOL_Specific.tex Tue Nov 08 08:56:24 2011 +0100
+++ b/doc-src/IsarRef/Thy/document/HOL_Specific.tex Tue Nov 08 10:33:30 2011 +0100
@@ -2557,7 +2557,8 @@
\indexdef{HOL}{command}{code\_monad}\hypertarget{command.HOL.code-monad}{\hyperlink{command.HOL.code-monad}{\mbox{\isa{\isacommand{code{\isaliteral{5F}{\isacharunderscore}}monad}}}}} & : & \isa{{\isaliteral{22}{\isachardoublequote}}theory\ {\isaliteral{5C3C72696768746172726F773E}{\isasymrightarrow}}\ theory{\isaliteral{22}{\isachardoublequote}}} \\
\indexdef{HOL}{command}{code\_include}\hypertarget{command.HOL.code-include}{\hyperlink{command.HOL.code-include}{\mbox{\isa{\isacommand{code{\isaliteral{5F}{\isacharunderscore}}include}}}}} & : & \isa{{\isaliteral{22}{\isachardoublequote}}theory\ {\isaliteral{5C3C72696768746172726F773E}{\isasymrightarrow}}\ theory{\isaliteral{22}{\isachardoublequote}}} \\
\indexdef{HOL}{command}{code\_modulename}\hypertarget{command.HOL.code-modulename}{\hyperlink{command.HOL.code-modulename}{\mbox{\isa{\isacommand{code{\isaliteral{5F}{\isacharunderscore}}modulename}}}}} & : & \isa{{\isaliteral{22}{\isachardoublequote}}theory\ {\isaliteral{5C3C72696768746172726F773E}{\isasymrightarrow}}\ theory{\isaliteral{22}{\isachardoublequote}}} \\
- \indexdef{HOL}{command}{code\_reflect}\hypertarget{command.HOL.code-reflect}{\hyperlink{command.HOL.code-reflect}{\mbox{\isa{\isacommand{code{\isaliteral{5F}{\isacharunderscore}}reflect}}}}} & : & \isa{{\isaliteral{22}{\isachardoublequote}}theory\ {\isaliteral{5C3C72696768746172726F773E}{\isasymrightarrow}}\ theory{\isaliteral{22}{\isachardoublequote}}}
+ \indexdef{HOL}{command}{code\_reflect}\hypertarget{command.HOL.code-reflect}{\hyperlink{command.HOL.code-reflect}{\mbox{\isa{\isacommand{code{\isaliteral{5F}{\isacharunderscore}}reflect}}}}} & : & \isa{{\isaliteral{22}{\isachardoublequote}}theory\ {\isaliteral{5C3C72696768746172726F773E}{\isasymrightarrow}}\ theory{\isaliteral{22}{\isachardoublequote}}} \\
+ \indexdef{HOL}{command}{code\_pred}\hypertarget{command.HOL.code-pred}{\hyperlink{command.HOL.code-pred}{\mbox{\isa{\isacommand{code{\isaliteral{5F}{\isacharunderscore}}pred}}}}} & : & \isa{{\isaliteral{22}{\isachardoublequote}}theory\ {\isaliteral{5C3C72696768746172726F773E}{\isasymrightarrow}}\ proof{\isaliteral{28}{\isacharparenleft}}prove{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequote}}}
\end{matharray}
\begin{railoutput}
@@ -2857,6 +2858,20 @@
\rail@nont{\hyperlink{syntax.string}{\mbox{\isa{string}}}}[]
\rail@endbar
\rail@end
+\rail@begin{6}{}
+\rail@term{\hyperlink{command.HOL.code-pred}{\mbox{\isa{\isacommand{code{\isaliteral{5F}{\isacharunderscore}}pred}}}}}[]
+\rail@cr{2}
+\rail@bar
+\rail@nextbar{3}
+\rail@term{\isa{{\isaliteral{28}{\isacharparenleft}}}}[]
+\rail@term{\isa{\isakeyword{modes}}}[]
+\rail@term{\isa{{\isaliteral{3A}{\isacharcolon}}}}[]
+\rail@nont{\isa{modedecl}}[]
+\rail@term{\isa{{\isaliteral{29}{\isacharparenright}}}}[]
+\rail@endbar
+\rail@cr{5}
+\rail@nont{\isa{const}}[]
+\rail@end
\rail@begin{4}{\isa{syntax}}
\rail@bar
\rail@nont{\hyperlink{syntax.string}{\mbox{\isa{string}}}}[]
@@ -2872,6 +2887,32 @@
\rail@nont{\hyperlink{syntax.string}{\mbox{\isa{string}}}}[]
\rail@endbar
\rail@end
+\rail@begin{6}{\isa{modedecl}}
+\rail@bar
+\rail@nont{\isa{modes}}[]
+\rail@nextbar{1}
+\rail@nont{\isa{const}}[]
+\rail@term{\isa{{\isaliteral{3A}{\isacharcolon}}}}[]
+\rail@nont{\isa{modes}}[]
+\rail@cr{3}
+\rail@bar
+\rail@nextbar{4}
+\rail@term{\isa{\isakeyword{and}}}[]
+\rail@plus
+\rail@nont{\isa{const}}[]
+\rail@term{\isa{{\isaliteral{3A}{\isacharcolon}}}}[]
+\rail@nont{\isa{modes}}[]
+\rail@term{\isa{\isakeyword{and}}}[]
+\rail@nextplus{5}
+\rail@endplus
+\rail@endbar
+\rail@endbar
+\rail@end
+\rail@begin{1}{\isa{modes}}
+\rail@nont{\isa{mode}}[]
+\rail@term{\isa{\isakeyword{as}}}[]
+\rail@nont{\isa{const}}[]
+\rail@end
\end{railoutput}
@@ -2985,6 +3026,12 @@
is generated into that specified file without modifying the code
generator setup.
+ \item \hyperlink{command.HOL.code-pred}{\mbox{\isa{\isacommand{code{\isaliteral{5F}{\isacharunderscore}}pred}}}} creates code equations for a predicate
+ given a set of introduction rules. Optional mode annotations determine
+ which arguments are supposed to be input or output. If alternative
+ introduction rules are declared, one must prove a corresponding elimination
+ rule.
+
\end{description}%
\end{isamarkuptext}%
\isamarkuptrue%