# HG changeset patch
# User haftmann
# Date 1211965547 -7200
# Node ID 284c871d3acb126f54b19e9ecff391c771f15dfe
# Parent  2c4032d595862012fe93a7bf9b19b9e3b2996e13
added new code_datatype example

diff -r 2c4032d59586 -r 284c871d3acb doc-src/IsarAdvanced/Codegen/Thy/Codegen.thy
--- a/doc-src/IsarAdvanced/Codegen/Thy/Codegen.thy	Mon May 26 17:55:39 2008 +0200
+++ b/doc-src/IsarAdvanced/Codegen/Thy/Codegen.thy	Wed May 28 11:05:47 2008 +0200
@@ -147,7 +147,7 @@
   \noindent Then we generate code
 *}
 
-export_code example (*<*)in SML(*>*)in SML file "examples/tree.ML"
+export_code example (*<*)in SML (*>*)in SML file "examples/tree.ML"
 
 text {*
   \noindent which looks like:
@@ -762,22 +762,102 @@
   the @{text "\<PRINTCODESETUP>"} command.
 
   In some cases, it may be convenient to alter or
-  extend this table;  as an example FIXME
+  extend this table;  as an example, we will develope an alternative
+  representation of natural numbers as binary digits, whose
+  size does increase logarithmically with its value, not linear
+  \footnote{Indeed, the @{text "Efficient_Nat"} theory \ref{eff_nat}
+    does something similar}.  First, the digit representation:
 *}
 
-(* {* code_datatype ... *}
+definition Dig0 :: "nat \<Rightarrow> nat" where
+  "Dig0 n = 2 * n"
 
-   {* export_code "{}" insert "op \<in>" "op \<union>" "Union" (*<*)in SML(*>*) in SML file "examples/set_list.ML" *}
+definition Dig1 :: "nat \<Rightarrow> nat" where
+  "Dig1 n = Suc (2 * n)"
 
-  {* \lstsml{Thy/examples/set_list.ML} *} *)
+text {*
+  \noindent We will use these two ">digits"< to represent natural numbers
+  in binary digits, e.g.:
+*}
+
+lemma 42: "42 = Dig0 (Dig1 (Dig0 (Dig1 (Dig0 1))))"
+  by (simp add: Dig0_def Dig1_def)
+
+text {*
+  \noindent Of course we also have to provide proper code equations for
+  the operations, e.g. @{term "op + \<Colon> nat \<Rightarrow> nat \<Rightarrow> nat"}:
+*}
+
+lemma plus_Dig [code func]:
+  "0 + n = n"
+  "m + 0 = m"
+  "1 + Dig0 n = Dig1 n"
+  "Dig0 m + 1 = Dig1 m"
+  "1 + Dig1 n = Dig0 (n + 1)"
+  "Dig1 m + 1 = Dig0 (m + 1)"
+  "Dig0 m + Dig0 n = Dig0 (m + n)"
+  "Dig0 m + Dig1 n = Dig1 (m + n)"
+  "Dig1 m + Dig0 n = Dig1 (m + n)"
+  "Dig1 m + Dig1 n = Dig0 (m + n + 1)"
+  by (simp_all add: Dig0_def Dig1_def)
+
+text {*
+  \noindent We then instruct the code generator to view @{term "0\<Colon>nat"},
+  @{term "1\<Colon>nat"}, @{term Dig0} and @{term Dig1} as
+  datatype constructors:
+*}
+
+code_datatype "0\<Colon>nat" "1\<Colon>nat" Dig0 Dig1
+
+text {*
+  \noindent For the former constructor @{term Suc}, we provide a code
+  equation and remove some parts of the default code generator setup
+  which are an obstacle here:
+*}
+
+lemma Suc_Dig [code func]:
+  "Suc n = n + 1"
+  by simp
+
+declare One_nat_def [code inline del]
+declare add_Suc_shift [code func del] 
+
+text {*
+  \noindent This yields the following code:
+*}
+
+export_code "op + \<Colon> nat \<Rightarrow> nat \<Rightarrow> nat" (*<*)in SML(*>*) in SML file "examples/nat_binary.ML"
+
+text {* \lstsml{Thy/examples/nat_binary.ML} *}
 
 text {*
   \medskip
 
-  Changing the representation of existing datatypes requires
-  some care with respect to pattern matching and such.
+  From this example, it can be easily glimpsed that using own constructor sets
+  is a little delicate since it changes the set of valid patterns for values
+  of that type.  Without going into much detail, here some practical hints:
+
+  \begin{itemize}
+    \item When changing the constuctor set for datatypes, take care to
+      provide an alternative for the @{text case} combinator (e.g. by replacing
+      it using the preprocessor).
+    \item Values in the target language need not to be normalized -- different
+      values in the target language may represent the same value in the
+      logic (e.g. @{text "Dig1 0 = 1"}).
+    \item Usually, a good methodology to deal with the subleties of pattern
+      matching is to see the type as an abstract type: provide a set
+      of operations which operate on the concrete representation of the type,
+      and derive further operations by combinations of these primitive ones,
+      without relying on a particular representation.
+  \end{itemize}
 *}
 
+code_datatype %invisible "0::nat" Suc
+declare %invisible plus_Dig [code func del]
+declare %invisible One_nat_def [code inline]
+declare %invisible add_Suc_shift [code func] 
+lemma %invisible [code func]: "0 + n = (n \<Colon> nat)" by simp
+
 
 subsection {* Customizing serialization  *}
 
diff -r 2c4032d59586 -r 284c871d3acb doc-src/IsarAdvanced/Codegen/Thy/document/Codegen.tex
--- a/doc-src/IsarAdvanced/Codegen/Thy/document/Codegen.tex	Mon May 26 17:55:39 2008 +0200
+++ b/doc-src/IsarAdvanced/Codegen/Thy/document/Codegen.tex	Wed May 28 11:05:47 2008 +0200
@@ -993,18 +993,168 @@
   the \isa{{\isasymPRINTCODESETUP}} command.
 
   In some cases, it may be convenient to alter or
-  extend this table;  as an example FIXME%
+  extend this table;  as an example, we will develope an alternative
+  representation of natural numbers as binary digits, whose
+  size does increase logarithmically with its value, not linear
+  \footnote{Indeed, the \isa{Efficient{\isacharunderscore}Nat} theory \ref{eff_nat}
+    does something similar}.  First, the digit representation:%
+\end{isamarkuptext}%
+\isamarkuptrue%
+\isacommand{definition}\isamarkupfalse%
+\ Dig{\isadigit{0}}\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}nat\ {\isasymRightarrow}\ nat{\isachardoublequoteclose}\ \isakeyword{where}\isanewline
+\ \ {\isachardoublequoteopen}Dig{\isadigit{0}}\ n\ {\isacharequal}\ {\isadigit{2}}\ {\isacharasterisk}\ n{\isachardoublequoteclose}\isanewline
+\isanewline
+\isacommand{definition}\isamarkupfalse%
+\ Dig{\isadigit{1}}\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}nat\ {\isasymRightarrow}\ nat{\isachardoublequoteclose}\ \isakeyword{where}\isanewline
+\ \ {\isachardoublequoteopen}Dig{\isadigit{1}}\ n\ {\isacharequal}\ Suc\ {\isacharparenleft}{\isadigit{2}}\ {\isacharasterisk}\ n{\isacharparenright}{\isachardoublequoteclose}%
+\begin{isamarkuptext}%
+\noindent We will use these two ">digits"< to represent natural numbers
+  in binary digits, e.g.:%
+\end{isamarkuptext}%
+\isamarkuptrue%
+\isacommand{lemma}\isamarkupfalse%
+\ {\isadigit{4}}{\isadigit{2}}{\isacharcolon}\ {\isachardoublequoteopen}{\isadigit{4}}{\isadigit{2}}\ {\isacharequal}\ Dig{\isadigit{0}}\ {\isacharparenleft}Dig{\isadigit{1}}\ {\isacharparenleft}Dig{\isadigit{0}}\ {\isacharparenleft}Dig{\isadigit{1}}\ {\isacharparenleft}Dig{\isadigit{0}}\ {\isadigit{1}}{\isacharparenright}{\isacharparenright}{\isacharparenright}{\isacharparenright}{\isachardoublequoteclose}\isanewline
+%
+\isadelimproof
+\ \ %
+\endisadelimproof
+%
+\isatagproof
+\isacommand{by}\isamarkupfalse%
+\ {\isacharparenleft}simp\ add{\isacharcolon}\ Dig{\isadigit{0}}{\isacharunderscore}def\ Dig{\isadigit{1}}{\isacharunderscore}def{\isacharparenright}%
+\endisatagproof
+{\isafoldproof}%
+%
+\isadelimproof
+%
+\endisadelimproof
+%
+\begin{isamarkuptext}%
+\noindent Of course we also have to provide proper code equations for
+  the operations, e.g. \isa{op\ {\isacharplus}}:%
+\end{isamarkuptext}%
+\isamarkuptrue%
+\isacommand{lemma}\isamarkupfalse%
+\ plus{\isacharunderscore}Dig\ {\isacharbrackleft}code\ func{\isacharbrackright}{\isacharcolon}\isanewline
+\ \ {\isachardoublequoteopen}{\isadigit{0}}\ {\isacharplus}\ n\ {\isacharequal}\ n{\isachardoublequoteclose}\isanewline
+\ \ {\isachardoublequoteopen}m\ {\isacharplus}\ {\isadigit{0}}\ {\isacharequal}\ m{\isachardoublequoteclose}\isanewline
+\ \ {\isachardoublequoteopen}{\isadigit{1}}\ {\isacharplus}\ Dig{\isadigit{0}}\ n\ {\isacharequal}\ Dig{\isadigit{1}}\ n{\isachardoublequoteclose}\isanewline
+\ \ {\isachardoublequoteopen}Dig{\isadigit{0}}\ m\ {\isacharplus}\ {\isadigit{1}}\ {\isacharequal}\ Dig{\isadigit{1}}\ m{\isachardoublequoteclose}\isanewline
+\ \ {\isachardoublequoteopen}{\isadigit{1}}\ {\isacharplus}\ Dig{\isadigit{1}}\ n\ {\isacharequal}\ Dig{\isadigit{0}}\ {\isacharparenleft}n\ {\isacharplus}\ {\isadigit{1}}{\isacharparenright}{\isachardoublequoteclose}\isanewline
+\ \ {\isachardoublequoteopen}Dig{\isadigit{1}}\ m\ {\isacharplus}\ {\isadigit{1}}\ {\isacharequal}\ Dig{\isadigit{0}}\ {\isacharparenleft}m\ {\isacharplus}\ {\isadigit{1}}{\isacharparenright}{\isachardoublequoteclose}\isanewline
+\ \ {\isachardoublequoteopen}Dig{\isadigit{0}}\ m\ {\isacharplus}\ Dig{\isadigit{0}}\ n\ {\isacharequal}\ Dig{\isadigit{0}}\ {\isacharparenleft}m\ {\isacharplus}\ n{\isacharparenright}{\isachardoublequoteclose}\isanewline
+\ \ {\isachardoublequoteopen}Dig{\isadigit{0}}\ m\ {\isacharplus}\ Dig{\isadigit{1}}\ n\ {\isacharequal}\ Dig{\isadigit{1}}\ {\isacharparenleft}m\ {\isacharplus}\ n{\isacharparenright}{\isachardoublequoteclose}\isanewline
+\ \ {\isachardoublequoteopen}Dig{\isadigit{1}}\ m\ {\isacharplus}\ Dig{\isadigit{0}}\ n\ {\isacharequal}\ Dig{\isadigit{1}}\ {\isacharparenleft}m\ {\isacharplus}\ n{\isacharparenright}{\isachardoublequoteclose}\isanewline
+\ \ {\isachardoublequoteopen}Dig{\isadigit{1}}\ m\ {\isacharplus}\ Dig{\isadigit{1}}\ n\ {\isacharequal}\ Dig{\isadigit{0}}\ {\isacharparenleft}m\ {\isacharplus}\ n\ {\isacharplus}\ {\isadigit{1}}{\isacharparenright}{\isachardoublequoteclose}\isanewline
+%
+\isadelimproof
+\ \ %
+\endisadelimproof
+%
+\isatagproof
+\isacommand{by}\isamarkupfalse%
+\ {\isacharparenleft}simp{\isacharunderscore}all\ add{\isacharcolon}\ Dig{\isadigit{0}}{\isacharunderscore}def\ Dig{\isadigit{1}}{\isacharunderscore}def{\isacharparenright}%
+\endisatagproof
+{\isafoldproof}%
+%
+\isadelimproof
+%
+\endisadelimproof
+%
+\begin{isamarkuptext}%
+\noindent We then instruct the code generator to view \isa{{\isadigit{0}}},
+  \isa{{\isadigit{1}}}, \isa{Dig{\isadigit{0}}} and \isa{Dig{\isadigit{1}}} as
+  datatype constructors:%
+\end{isamarkuptext}%
+\isamarkuptrue%
+\isacommand{code{\isacharunderscore}datatype}\isamarkupfalse%
+\ {\isachardoublequoteopen}{\isadigit{0}}{\isasymColon}nat{\isachardoublequoteclose}\ {\isachardoublequoteopen}{\isadigit{1}}{\isasymColon}nat{\isachardoublequoteclose}\ Dig{\isadigit{0}}\ Dig{\isadigit{1}}%
+\begin{isamarkuptext}%
+\noindent For the former constructor \isa{Suc}, we provide a code
+  equation and remove some parts of the default code generator setup
+  which are an obstacle here:%
+\end{isamarkuptext}%
+\isamarkuptrue%
+\isacommand{lemma}\isamarkupfalse%
+\ Suc{\isacharunderscore}Dig\ {\isacharbrackleft}code\ func{\isacharbrackright}{\isacharcolon}\isanewline
+\ \ {\isachardoublequoteopen}Suc\ n\ {\isacharequal}\ n\ {\isacharplus}\ {\isadigit{1}}{\isachardoublequoteclose}\isanewline
+%
+\isadelimproof
+\ \ %
+\endisadelimproof
+%
+\isatagproof
+\isacommand{by}\isamarkupfalse%
+\ simp%
+\endisatagproof
+{\isafoldproof}%
+%
+\isadelimproof
+\isanewline
+%
+\endisadelimproof
+\isanewline
+\isacommand{declare}\isamarkupfalse%
+\ One{\isacharunderscore}nat{\isacharunderscore}def\ {\isacharbrackleft}code\ inline\ del{\isacharbrackright}\isanewline
+\isacommand{declare}\isamarkupfalse%
+\ add{\isacharunderscore}Suc{\isacharunderscore}shift\ {\isacharbrackleft}code\ func\ del{\isacharbrackright}%
+\begin{isamarkuptext}%
+\noindent This yields the following code:%
+\end{isamarkuptext}%
+\isamarkuptrue%
+\isacommand{export{\isacharunderscore}code}\isamarkupfalse%
+\ {\isachardoublequoteopen}op\ {\isacharplus}\ {\isasymColon}\ nat\ {\isasymRightarrow}\ nat\ {\isasymRightarrow}\ nat{\isachardoublequoteclose}\ \ \isakeyword{in}\ SML\ \isakeyword{file}\ {\isachardoublequoteopen}examples{\isacharslash}nat{\isacharunderscore}binary{\isachardot}ML{\isachardoublequoteclose}%
+\begin{isamarkuptext}%
+\lstsml{Thy/examples/nat_binary.ML}%
 \end{isamarkuptext}%
 \isamarkuptrue%
 %
 \begin{isamarkuptext}%
 \medskip
 
-  Changing the representation of existing datatypes requires
-  some care with respect to pattern matching and such.%
+  From this example, it can be easily glimpsed that using own constructor sets
+  is a little delicate since it changes the set of valid patterns for values
+  of that type.  Without going into much detail, here some practical hints:
+
+  \begin{itemize}
+    \item When changing the constuctor set for datatypes, take care to
+      provide an alternative for the \isa{case} combinator (e.g. by replacing
+      it using the preprocessor).
+    \item Values in the target language need not to be normalized -- different
+      values in the target language may represent the same value in the
+      logic (e.g. \isa{Dig{\isadigit{1}}\ {\isadigit{0}}\ {\isacharequal}\ {\isadigit{1}}}).
+    \item Usually, a good methodology to deal with the subleties of pattern
+      matching is to see the type as an abstract type: provide a set
+      of operations which operate on the concrete representation of the type,
+      and derive further operations by combinations of these primitive ones,
+      without relying on a particular representation.
+  \end{itemize}%
 \end{isamarkuptext}%
 \isamarkuptrue%
 %
+\isadeliminvisible
+%
+\endisadeliminvisible
+%
+\isataginvisible
+\isacommand{code{\isacharunderscore}datatype}\isamarkupfalse%
+\ {\isachardoublequoteopen}{\isadigit{0}}{\isacharcolon}{\isacharcolon}nat{\isachardoublequoteclose}\ Suc\isanewline
+\isacommand{declare}\isamarkupfalse%
+\ plus{\isacharunderscore}Dig\ {\isacharbrackleft}code\ func\ del{\isacharbrackright}\isanewline
+\isacommand{declare}\isamarkupfalse%
+\ One{\isacharunderscore}nat{\isacharunderscore}def\ {\isacharbrackleft}code\ inline{\isacharbrackright}\isanewline
+\isacommand{declare}\isamarkupfalse%
+\ add{\isacharunderscore}Suc{\isacharunderscore}shift\ {\isacharbrackleft}code\ func{\isacharbrackright}\ \isanewline
+\isacommand{lemma}\isamarkupfalse%
+\ {\isacharbrackleft}code\ func{\isacharbrackright}{\isacharcolon}\ {\isachardoublequoteopen}{\isadigit{0}}\ {\isacharplus}\ n\ {\isacharequal}\ {\isacharparenleft}n\ {\isasymColon}\ nat{\isacharparenright}{\isachardoublequoteclose}\ \isacommand{by}\isamarkupfalse%
+\ simp%
+\endisataginvisible
+{\isafoldinvisible}%
+%
+\isadeliminvisible
+%
+\endisadeliminvisible
+%
 \isamarkupsubsection{Customizing serialization%
 }
 \isamarkuptrue%
diff -r 2c4032d59586 -r 284c871d3acb doc-src/IsarAdvanced/Codegen/Thy/examples/nat_binary.ML
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/doc-src/IsarAdvanced/Codegen/Thy/examples/nat_binary.ML	Wed May 28 11:05:47 2008 +0200
@@ -0,0 +1,17 @@
+structure Nat = 
+struct
+
+datatype nat = Dig1 of nat | Dig0 of nat | One_nat | Zero_nat;
+
+fun plus_nat (Dig1 m) (Dig1 n) = Dig0 (plus_nat (plus_nat m n) One_nat)
+  | plus_nat (Dig1 m) (Dig0 n) = Dig1 (plus_nat m n)
+  | plus_nat (Dig0 m) (Dig1 n) = Dig1 (plus_nat m n)
+  | plus_nat (Dig0 m) (Dig0 n) = Dig0 (plus_nat m n)
+  | plus_nat (Dig1 m) One_nat = Dig0 (plus_nat m One_nat)
+  | plus_nat One_nat (Dig1 n) = Dig0 (plus_nat n One_nat)
+  | plus_nat (Dig0 m) One_nat = Dig1 m
+  | plus_nat One_nat (Dig0 n) = Dig1 n
+  | plus_nat m Zero_nat = m
+  | plus_nat Zero_nat n = n;
+
+end; (*struct Nat*)
diff -r 2c4032d59586 -r 284c871d3acb doc-src/IsarAdvanced/Codegen/Thy/examples/set_list.ML
--- a/doc-src/IsarAdvanced/Codegen/Thy/examples/set_list.ML	Mon May 26 17:55:39 2008 +0200
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,38 +0,0 @@
-structure HOL = 
-struct
-
-type 'a eq = {eq : 'a -> 'a -> bool};
-fun eq (A_:'a eq) = #eq A_;
-
-fun eqop A_ a = eq A_ a;
-
-end; (*struct HOL*)
-
-structure List = 
-struct
-
-fun foldr f (x :: xs) a = f x (foldr f xs a)
-  | foldr f [] a = a;
-
-fun member A_ x (y :: ys) =
-  (if HOL.eqop A_ y x then true else member A_ x ys)
-  | member A_ x [] = false;
-
-end; (*struct List*)
-
-structure Set = 
-struct
-
-datatype 'a set = Set of 'a list;
-
-val empty : 'a set = Set [];
-
-fun insert x (Set xs) = Set (x :: xs);
-
-fun uniona xs (Set ys) = List.foldr insert ys xs;
-
-fun member A_ x (Set xs) = List.member A_ x xs;
-
-fun unionaa (Set xs) = List.foldr uniona xs empty;
-
-end; (*struct Set*)