# 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 \<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}
 *}
 
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%