# HG changeset patch # User bulwahn # Date 1320744810 -3600 # Node ID 7156f63ce3c29308502a60b3b42b66f9150a6169 # Parent 1fac64bbdb4f342511cc3910a824fc5f1749d7a0 adding a minimal documentation about the code_pred command to the isar reference diff -r 1fac64bbdb4f -r 7156f63ce3c2 doc-src/IsarRef/Thy/HOL_Specific.thy --- 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 \ theory"} \\ @{command_def (HOL) "code_include"} & : & @{text "theory \ theory"} \\ @{command_def (HOL) "code_modulename"} & : & @{text "theory \ theory"} \\ - @{command_def (HOL) "code_reflect"} & : & @{text "theory \ theory"} + @{command_def (HOL) "code_reflect"} & : & @{text "theory \ theory"} \\ + @{command_def (HOL) "code_pred"} & : & @{text "theory \ 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} *} diff -r 1fac64bbdb4f -r 7156f63ce3c2 doc-src/IsarRef/Thy/document/HOL_Specific.tex --- 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%