updated

--- a/doc-src/IsarAdvanced/Codegen/Thy/Codegen.thy	Mon Nov 12 11:18:51 2007 +0100
+++ b/doc-src/IsarAdvanced/Codegen/Thy/Codegen.thy	Mon Nov 12 14:20:21 2007 +0100
@@ -751,6 +751,48 @@
 *}
 
 
+subsection {* Constructor sets for datatypes *}
+
+text {*
+  Conceptually, any datatype is spanned by a set of
+  \emph{constructors} of type @{text "\<tau> = \<dots> \<Rightarrow> \<kappa> \<alpha>\<^isub>1 \<dots> \<alpha>\<^isub>n"}
+  where @{text "{\<alpha>\<^isub>1, \<dots>, \<alpha>\<^isub>n}"} is excactly the set of \emph{all}
+  type variables in @{text "\<tau>"}.  The HOL datatype package
+  by default registers any new datatype in the table
+  of datatypes, which may be inspected using
+  the @{text "\<PRINTCODESETUP>"} command.
+
+  In some cases, it may be convenient to alter or
+  extend this table;  as an example, we show
+  how to implement finite sets by lists
+  using the conversion @{term [source] "set \<Colon> 'a list \<Rightarrow> 'a set"}
+  as constructor:
+*} (*<*)ML {* nonfix union *} lemmas [code func del] = in_code union_empty1 union_empty2 union_insert Union_code(*>*)
+
+code_datatype set
+
+lemma [code func]: "{} = set []" by simp
+
+lemma [code func]: "insert x (set xs) = set (x#xs)" by simp
+
+lemma [code func]: "x \<in> set xs \<longleftrightarrow> x mem xs" by (induct xs) simp_all
+
+lemma [code func]: "xs \<union> set ys = foldr insert ys xs" by (induct ys) simp_all
+
+lemma [code func]: "\<Union>set xs = foldr (op \<union>) xs {}" by (induct xs) simp_all
+
+export_code "{}" insert "op \<in>" "op \<union>" "Union" (*<*)in SML(*>*) in SML file "examples/set_list.ML"
+
+text {*
+  \lstsml{Thy/examples/set_list.ML}
+
+  \medskip
+
+  Changing the representation of existing datatypes requires
+  some care with respect to pattern matching and such.
+*}
+
+
 subsection {* Customizing serialization  *}
 
 subsubsection {* Basics *}
@@ -862,8 +904,7 @@
   second ``@{verbatim "_"}'' is a placeholder.
 
   The HOL theories provide further
-  examples for custom serializations and form
-  a recommended tutorial on how to use them properly.
+  examples for custom serializations.
 *}
 
 
@@ -917,46 +958,6 @@
   theories introduces in \secref{sec:library}.
 *}
 
-subsection {* Constructor sets for datatypes *}
-
-text {*
-  Conceptually, any datatype is spanned by a set of
-  \emph{constructors} of type @{text "\<tau> = \<dots> \<Rightarrow> \<kappa> \<alpha>\<^isub>1 \<dots> \<alpha>\<^isub>n"}
-  where @{text "{\<alpha>\<^isub>1, \<dots>, \<alpha>\<^isub>n}"} is excactly the set of \emph{all}
-  type variables in @{text "\<tau>"}.  The HOL datatype package
-  by default registers any new datatype in the table
-  of datatypes, which may be inspected using
-  the @{text "\<PRINTCODESETUP>"} command.
-
-  In some cases, it may be convenient to alter or
-  extend this table;  as an example, we show
-  how to implement finite sets by lists
-  using the conversion @{term [source] "set \<Colon> 'a list \<Rightarrow> 'a set"}
-  as constructor:
-*} (*<*)ML {* nonfix union *} lemmas [code func del] = in_code union_empty1 union_empty2 union_insert Union_code(*>*)
-
-code_datatype set
-
-lemma [code func]: "{} = set []" by simp
-
-lemma [code func]: "insert x (set xs) = set (x#xs)" by simp
-
-lemma [code func]: "x \<in> set xs \<longleftrightarrow> x mem xs" by (induct xs) simp_all
-
-lemma [code func]: "xs \<union> set ys = foldr insert ys xs" by (induct ys) simp_all
-
-lemma [code func]: "\<Union>set xs = foldr (op \<union>) xs {}" by (induct xs) simp_all
-
-export_code "{}" insert "op \<in>" "op \<union>" "Union" (*<*)in SML(*>*) in SML file "examples/set_list.ML"
-
-text {*
-  \lstsml{Thy/examples/set_list.ML}
-
-  \medskip
-
-  Changing the representation of existing datatypes requires
-  some care with respect to pattern matching and such.
-*}
 
 subsection {* Cyclic module dependencies *}
 
@@ -1000,11 +1001,11 @@
   in the current cache are referred to.
 *}
 
-subsection {* Code generation and proof extraction *}
+(*subsection {* Code generation and proof extraction *}
 
 text {*
   \fixme
-*}
+*}*)
 
 
 section {* ML interfaces \label{sec:ml} *}

--- a/doc-src/IsarAdvanced/Codegen/Thy/document/Codegen.tex	Mon Nov 12 11:18:51 2007 +0100
+++ b/doc-src/IsarAdvanced/Codegen/Thy/document/Codegen.tex	Mon Nov 12 14:20:21 2007 +0100
@@ -1008,6 +1008,140 @@
 \end{isamarkuptext}%
 \isamarkuptrue%
 %
+\isamarkupsubsection{Constructor sets for datatypes%
+}
+\isamarkuptrue%
+%
+\begin{isamarkuptext}%
+Conceptually, any datatype is spanned by a set of
+  \emph{constructors} of type \isa{{\isasymtau}\ {\isacharequal}\ {\isasymdots}\ {\isasymRightarrow}\ {\isasymkappa}\ {\isasymalpha}\isactrlisub {\isadigit{1}}\ {\isasymdots}\ {\isasymalpha}\isactrlisub n}
+  where \isa{{\isacharbraceleft}{\isasymalpha}\isactrlisub {\isadigit{1}}{\isacharcomma}\ {\isasymdots}{\isacharcomma}\ {\isasymalpha}\isactrlisub n{\isacharbraceright}} is excactly the set of \emph{all}
+  type variables in \isa{{\isasymtau}}.  The HOL datatype package
+  by default registers any new datatype in the table
+  of datatypes, which may be inspected using
+  the \isa{{\isasymPRINTCODESETUP}} command.
+
+  In some cases, it may be convenient to alter or
+  extend this table;  as an example, we show
+  how to implement finite sets by lists
+  using the conversion \isa{{\isachardoublequote}set\ {\isasymColon}\ {\isacharprime}a\ list\ {\isasymRightarrow}\ {\isacharprime}a\ set{\isachardoublequote}}
+  as constructor:%
+\end{isamarkuptext}%
+\isamarkuptrue%
+\ %
+\isadelimML
+%
+\endisadelimML
+%
+\isatagML
+%
+\endisatagML
+{\isafoldML}%
+%
+\isadelimML
+%
+\endisadelimML
+\isanewline
+\isacommand{code{\isacharunderscore}datatype}\isamarkupfalse%
+\ set\isanewline
+\isanewline
+\isacommand{lemma}\isamarkupfalse%
+\ {\isacharbrackleft}code\ func{\isacharbrackright}{\isacharcolon}\ {\isachardoublequoteopen}{\isacharbraceleft}{\isacharbraceright}\ {\isacharequal}\ set\ {\isacharbrackleft}{\isacharbrackright}{\isachardoublequoteclose}%
+\isadelimproof
+\ %
+\endisadelimproof
+%
+\isatagproof
+\isacommand{by}\isamarkupfalse%
+\ simp%
+\endisatagproof
+{\isafoldproof}%
+%
+\isadelimproof
+%
+\endisadelimproof
+\isanewline
+\isanewline
+\isacommand{lemma}\isamarkupfalse%
+\ {\isacharbrackleft}code\ func{\isacharbrackright}{\isacharcolon}\ {\isachardoublequoteopen}insert\ x\ {\isacharparenleft}set\ xs{\isacharparenright}\ {\isacharequal}\ set\ {\isacharparenleft}x{\isacharhash}xs{\isacharparenright}{\isachardoublequoteclose}%
+\isadelimproof
+\ %
+\endisadelimproof
+%
+\isatagproof
+\isacommand{by}\isamarkupfalse%
+\ simp%
+\endisatagproof
+{\isafoldproof}%
+%
+\isadelimproof
+%
+\endisadelimproof
+\isanewline
+\isanewline
+\isacommand{lemma}\isamarkupfalse%
+\ {\isacharbrackleft}code\ func{\isacharbrackright}{\isacharcolon}\ {\isachardoublequoteopen}x\ {\isasymin}\ set\ xs\ {\isasymlongleftrightarrow}\ x\ mem\ xs{\isachardoublequoteclose}%
+\isadelimproof
+\ %
+\endisadelimproof
+%
+\isatagproof
+\isacommand{by}\isamarkupfalse%
+\ {\isacharparenleft}induct\ xs{\isacharparenright}\ simp{\isacharunderscore}all%
+\endisatagproof
+{\isafoldproof}%
+%
+\isadelimproof
+%
+\endisadelimproof
+\isanewline
+\isanewline
+\isacommand{lemma}\isamarkupfalse%
+\ {\isacharbrackleft}code\ func{\isacharbrackright}{\isacharcolon}\ {\isachardoublequoteopen}xs\ {\isasymunion}\ set\ ys\ {\isacharequal}\ foldr\ insert\ ys\ xs{\isachardoublequoteclose}%
+\isadelimproof
+\ %
+\endisadelimproof
+%
+\isatagproof
+\isacommand{by}\isamarkupfalse%
+\ {\isacharparenleft}induct\ ys{\isacharparenright}\ simp{\isacharunderscore}all%
+\endisatagproof
+{\isafoldproof}%
+%
+\isadelimproof
+%
+\endisadelimproof
+\isanewline
+\isanewline
+\isacommand{lemma}\isamarkupfalse%
+\ {\isacharbrackleft}code\ func{\isacharbrackright}{\isacharcolon}\ {\isachardoublequoteopen}{\isasymUnion}set\ xs\ {\isacharequal}\ foldr\ {\isacharparenleft}op\ {\isasymunion}{\isacharparenright}\ xs\ {\isacharbraceleft}{\isacharbraceright}{\isachardoublequoteclose}%
+\isadelimproof
+\ %
+\endisadelimproof
+%
+\isatagproof
+\isacommand{by}\isamarkupfalse%
+\ {\isacharparenleft}induct\ xs{\isacharparenright}\ simp{\isacharunderscore}all%
+\endisatagproof
+{\isafoldproof}%
+%
+\isadelimproof
+%
+\endisadelimproof
+\isanewline
+\isanewline
+\isacommand{export{\isacharunderscore}code}\isamarkupfalse%
+\ {\isachardoublequoteopen}{\isacharbraceleft}{\isacharbraceright}{\isachardoublequoteclose}\ insert\ {\isachardoublequoteopen}op\ {\isasymin}{\isachardoublequoteclose}\ {\isachardoublequoteopen}op\ {\isasymunion}{\isachardoublequoteclose}\ {\isachardoublequoteopen}Union{\isachardoublequoteclose}\ \ \isakeyword{in}\ SML\ \isakeyword{file}\ {\isachardoublequoteopen}examples{\isacharslash}set{\isacharunderscore}list{\isachardot}ML{\isachardoublequoteclose}%
+\begin{isamarkuptext}%
+\lstsml{Thy/examples/set_list.ML}
+
+  \medskip
+
+  Changing the representation of existing datatypes requires
+  some care with respect to pattern matching and such.%
+\end{isamarkuptext}%
+\isamarkuptrue%
+%
 \isamarkupsubsection{Customizing serialization%
 }
 \isamarkuptrue%
@@ -1167,8 +1301,7 @@
   second ``\verb|_|'' is a placeholder.
 
   The HOL theories provide further
-  examples for custom serializations and form
-  a recommended tutorial on how to use them properly.%
+  examples for custom serializations.%
 \end{isamarkuptext}%
 \isamarkuptrue%
 %
@@ -1282,140 +1415,6 @@
 \end{isamarkuptext}%
 \isamarkuptrue%
 %
-\isamarkupsubsection{Constructor sets for datatypes%
-}
-\isamarkuptrue%
-%
-\begin{isamarkuptext}%
-Conceptually, any datatype is spanned by a set of
-  \emph{constructors} of type \isa{{\isasymtau}\ {\isacharequal}\ {\isasymdots}\ {\isasymRightarrow}\ {\isasymkappa}\ {\isasymalpha}\isactrlisub {\isadigit{1}}\ {\isasymdots}\ {\isasymalpha}\isactrlisub n}
-  where \isa{{\isacharbraceleft}{\isasymalpha}\isactrlisub {\isadigit{1}}{\isacharcomma}\ {\isasymdots}{\isacharcomma}\ {\isasymalpha}\isactrlisub n{\isacharbraceright}} is excactly the set of \emph{all}
-  type variables in \isa{{\isasymtau}}.  The HOL datatype package
-  by default registers any new datatype in the table
-  of datatypes, which may be inspected using
-  the \isa{{\isasymPRINTCODESETUP}} command.
-
-  In some cases, it may be convenient to alter or
-  extend this table;  as an example, we show
-  how to implement finite sets by lists
-  using the conversion \isa{{\isachardoublequote}set\ {\isasymColon}\ {\isacharprime}a\ list\ {\isasymRightarrow}\ {\isacharprime}a\ set{\isachardoublequote}}
-  as constructor:%
-\end{isamarkuptext}%
-\isamarkuptrue%
-\ %
-\isadelimML
-%
-\endisadelimML
-%
-\isatagML
-%
-\endisatagML
-{\isafoldML}%
-%
-\isadelimML
-%
-\endisadelimML
-\isanewline
-\isacommand{code{\isacharunderscore}datatype}\isamarkupfalse%
-\ set\isanewline
-\isanewline
-\isacommand{lemma}\isamarkupfalse%
-\ {\isacharbrackleft}code\ func{\isacharbrackright}{\isacharcolon}\ {\isachardoublequoteopen}{\isacharbraceleft}{\isacharbraceright}\ {\isacharequal}\ set\ {\isacharbrackleft}{\isacharbrackright}{\isachardoublequoteclose}%
-\isadelimproof
-\ %
-\endisadelimproof
-%
-\isatagproof
-\isacommand{by}\isamarkupfalse%
-\ simp%
-\endisatagproof
-{\isafoldproof}%
-%
-\isadelimproof
-%
-\endisadelimproof
-\isanewline
-\isanewline
-\isacommand{lemma}\isamarkupfalse%
-\ {\isacharbrackleft}code\ func{\isacharbrackright}{\isacharcolon}\ {\isachardoublequoteopen}insert\ x\ {\isacharparenleft}set\ xs{\isacharparenright}\ {\isacharequal}\ set\ {\isacharparenleft}x{\isacharhash}xs{\isacharparenright}{\isachardoublequoteclose}%
-\isadelimproof
-\ %
-\endisadelimproof
-%
-\isatagproof
-\isacommand{by}\isamarkupfalse%
-\ simp%
-\endisatagproof
-{\isafoldproof}%
-%
-\isadelimproof
-%
-\endisadelimproof
-\isanewline
-\isanewline
-\isacommand{lemma}\isamarkupfalse%
-\ {\isacharbrackleft}code\ func{\isacharbrackright}{\isacharcolon}\ {\isachardoublequoteopen}x\ {\isasymin}\ set\ xs\ {\isasymlongleftrightarrow}\ x\ mem\ xs{\isachardoublequoteclose}%
-\isadelimproof
-\ %
-\endisadelimproof
-%
-\isatagproof
-\isacommand{by}\isamarkupfalse%
-\ {\isacharparenleft}induct\ xs{\isacharparenright}\ simp{\isacharunderscore}all%
-\endisatagproof
-{\isafoldproof}%
-%
-\isadelimproof
-%
-\endisadelimproof
-\isanewline
-\isanewline
-\isacommand{lemma}\isamarkupfalse%
-\ {\isacharbrackleft}code\ func{\isacharbrackright}{\isacharcolon}\ {\isachardoublequoteopen}xs\ {\isasymunion}\ set\ ys\ {\isacharequal}\ foldr\ insert\ ys\ xs{\isachardoublequoteclose}%
-\isadelimproof
-\ %
-\endisadelimproof
-%
-\isatagproof
-\isacommand{by}\isamarkupfalse%
-\ {\isacharparenleft}induct\ ys{\isacharparenright}\ simp{\isacharunderscore}all%
-\endisatagproof
-{\isafoldproof}%
-%
-\isadelimproof
-%
-\endisadelimproof
-\isanewline
-\isanewline
-\isacommand{lemma}\isamarkupfalse%
-\ {\isacharbrackleft}code\ func{\isacharbrackright}{\isacharcolon}\ {\isachardoublequoteopen}{\isasymUnion}set\ xs\ {\isacharequal}\ foldr\ {\isacharparenleft}op\ {\isasymunion}{\isacharparenright}\ xs\ {\isacharbraceleft}{\isacharbraceright}{\isachardoublequoteclose}%
-\isadelimproof
-\ %
-\endisadelimproof
-%
-\isatagproof
-\isacommand{by}\isamarkupfalse%
-\ {\isacharparenleft}induct\ xs{\isacharparenright}\ simp{\isacharunderscore}all%
-\endisatagproof
-{\isafoldproof}%
-%
-\isadelimproof
-%
-\endisadelimproof
-\isanewline
-\isanewline
-\isacommand{export{\isacharunderscore}code}\isamarkupfalse%
-\ {\isachardoublequoteopen}{\isacharbraceleft}{\isacharbraceright}{\isachardoublequoteclose}\ insert\ {\isachardoublequoteopen}op\ {\isasymin}{\isachardoublequoteclose}\ {\isachardoublequoteopen}op\ {\isasymunion}{\isachardoublequoteclose}\ {\isachardoublequoteopen}Union{\isachardoublequoteclose}\ \ \isakeyword{in}\ SML\ \isakeyword{file}\ {\isachardoublequoteopen}examples{\isacharslash}set{\isacharunderscore}list{\isachardot}ML{\isachardoublequoteclose}%
-\begin{isamarkuptext}%
-\lstsml{Thy/examples/set_list.ML}
-
-  \medskip
-
-  Changing the representation of existing datatypes requires
-  some care with respect to pattern matching and such.%
-\end{isamarkuptext}%
-\isamarkuptrue%
-%
 \isamarkupsubsection{Cyclic module dependencies%
 }
 \isamarkuptrue%
@@ -1464,15 +1463,6 @@
 \end{isamarkuptext}%
 \isamarkuptrue%
 %
-\isamarkupsubsection{Code generation and proof extraction%
-}
-\isamarkuptrue%
-%
-\begin{isamarkuptext}%
-\fixme%
-\end{isamarkuptext}%
-\isamarkuptrue%
-%
 \isamarkupsection{ML interfaces \label{sec:ml}%
 }
 \isamarkuptrue%