--- a/doc-src/IsarAdvanced/Classes/Thy/Classes.thy Tue Mar 20 08:27:23 2007 +0100
+++ b/doc-src/IsarAdvanced/Classes/Thy/Classes.thy Tue Mar 20 10:23:31 2007 +0100
@@ -12,17 +12,17 @@
syntax
"_alpha" :: "type" ("\<alpha>")
- "_alpha_ofsort" :: "sort \<Rightarrow> type" ("\<alpha>()::_" [0] 1000)
+ "_alpha_ofsort" :: "sort \<Rightarrow> type" ("\<alpha>()\<Colon>_" [0] 1000)
"_beta" :: "type" ("\<beta>")
- "_beta_ofsort" :: "sort \<Rightarrow> type" ("\<beta>()::_" [0] 1000)
+ "_beta_ofsort" :: "sort \<Rightarrow> type" ("\<beta>()\<Colon>_" [0] 1000)
"_gamma" :: "type" ("\<gamma>")
- "_gamma_ofsort" :: "sort \<Rightarrow> type" ("\<gamma>()::_" [0] 1000)
+ "_gamma_ofsort" :: "sort \<Rightarrow> type" ("\<gamma>()\<Colon>_" [0] 1000)
"_alpha_f" :: "type" ("\<alpha>\<^sub>f")
- "_alpha_f_ofsort" :: "sort \<Rightarrow> type" ("\<alpha>\<^sub>f()::_" [0] 1000)
+ "_alpha_f_ofsort" :: "sort \<Rightarrow> type" ("\<alpha>\<^sub>f()\<Colon>_" [0] 1000)
"_beta_f" :: "type" ("\<beta>\<^sub>f")
- "_beta_f_ofsort" :: "sort \<Rightarrow> type" ("\<beta>\<^sub>f()::_" [0] 1000)
+ "_beta_f_ofsort" :: "sort \<Rightarrow> type" ("\<beta>\<^sub>f()\<Colon>_" [0] 1000)
"_gamma_f" :: "type" ("\<gamma>\<^sub>f")
- "_gamma_ofsort_f" :: "sort \<Rightarrow> type" ("\<gamma>\<^sub>f()::_" [0] 1000)
+ "_gamma_ofsort_f" :: "sort \<Rightarrow> type" ("\<gamma>\<^sub>f()\<Colon>_" [0] 1000)
parse_ast_translation {*
let
@@ -171,9 +171,9 @@
"\<FIXES>"}), the \qn{logical} part specifies properties on them
(@{text "\<ASSUMES>"}). The local @{text "\<FIXES>"} and @{text
"\<ASSUMES>"} are lifted to the theory toplevel, yielding the global
- operation @{term [source] "mult :: \<alpha>::semigroup \<Rightarrow> \<alpha> \<Rightarrow> \<alpha>"} and the
+ operation @{term [source] "mult \<Colon> \<alpha>\<Colon>semigroup \<Rightarrow> \<alpha> \<Rightarrow> \<alpha>"} and the
global theorem @{text "semigroup.assoc:"}~@{prop [source] "\<And>x y
- z::\<alpha>::semigroup. (x \<otimes> y) \<otimes> z = x \<otimes> (y \<otimes> z)"}.
+ z \<Colon> \<alpha>\<Colon>semigroup. (x \<otimes> y) \<otimes> z = x \<otimes> (y \<otimes> z)"}.
*}
@@ -186,7 +186,7 @@
*}
instance int :: semigroup
- mult_int_def: "\<And>i j :: int. i \<otimes> j \<equiv> i + j"
+ mult_int_def: "\<And>i j \<Colon> int. i \<otimes> j \<equiv> i + j"
proof
fix i j k :: int have "(i + j) + k = i + (j + k)" by simp
then show "(i \<otimes> j) \<otimes> k = i \<otimes> (j \<otimes> k)" unfolding mult_int_def .
@@ -365,7 +365,7 @@
text {*
This give you at hand the full power of the Isabelle module system;
conclusions in locale @{text idem} are implicitly propagated
- to class @{idem}.
+ to class @{text idem}.
*}
subsection {* Abstract reasoning *}
@@ -392,10 +392,10 @@
\noindent Here the \qt{@{text "\<IN> group"}} target specification
indicates that the result is recorded within that context for later
use. This local theorem is also lifted to the global one @{text
- "group.left_cancel:"} @{prop [source] "\<And>x y z::\<alpha>::group. x \<otimes> y = x \<otimes>
+ "group.left_cancel:"} @{prop [source] "\<And>x y z \<Colon> \<alpha>\<Colon>group. x \<otimes> y = x \<otimes>
z \<longleftrightarrow> y = z"}. Since type @{text "int"} has been made an instance of
@{text "group"} before, we may refer to that fact as well: @{prop
- [source] "\<And>x y z::int. x \<otimes> y = x \<otimes> z \<longleftrightarrow> y = z"}.
+ [source] "\<And>x y z \<Colon> int. x \<otimes> y = x \<otimes> z \<longleftrightarrow> y = z"}.
*}
@@ -439,7 +439,7 @@
fun
pow_nat :: "nat \<Rightarrow> \<alpha>\<Colon>monoidl \<Rightarrow> \<alpha>\<Colon>monoidl" where
"pow_nat 0 x = \<one>"
- "pow_nat (Suc n) x = x \<otimes> pow_nat n x"
+ | "pow_nat (Suc n) x = x \<otimes> pow_nat n x"
definition
pow_int :: "int \<Rightarrow> \<alpha>\<Colon>group \<Rightarrow> \<alpha>\<Colon>group" where
@@ -478,8 +478,7 @@
text {*
-(* subsection {* Syntactic classes *}
-*)
+subsection {* Syntactic classes *}
*} *)
--- a/doc-src/IsarAdvanced/Classes/Thy/code_examples/classes.ML Tue Mar 20 08:27:23 2007 +0100
+++ b/doc-src/IsarAdvanced/Classes/Thy/code_examples/classes.ML Tue Mar 20 10:23:31 2007 +0100
@@ -17,28 +17,22 @@
fun nat i = nat_aux Nat.Zero_nat i;
-fun op_eq_bit false false = true
- | op_eq_bit true true = true
- | op_eq_bit false true = false
- | op_eq_bit true false = false;
-
end; (*struct Integer*)
structure Classes =
struct
-type 'a semigroup = {Classes__mult : 'a -> 'a -> 'a};
-fun mult (A_:'a semigroup) = #Classes__mult A_;
+type 'a semigroup = {mult : 'a -> 'a -> 'a};
+fun mult (A_:'a semigroup) = #mult A_;
type 'a monoidl =
- {Classes__monoidl_semigroup : 'a semigroup, Classes__neutral : 'a};
+ {Classes__monoidl_semigroup : 'a semigroup, neutral : 'a};
fun monoidl_semigroup (A_:'a monoidl) = #Classes__monoidl_semigroup A_;
-fun neutral (A_:'a monoidl) = #Classes__neutral A_;
+fun neutral (A_:'a monoidl) = #neutral A_;
-type 'a group =
- {Classes__group_monoidl : 'a monoidl, Classes__inverse : 'a -> 'a};
+type 'a group = {Classes__group_monoidl : 'a monoidl, inverse : 'a -> 'a};
fun group_monoidl (A_:'a group) = #Classes__group_monoidl A_;
-fun inverse (A_:'a group) = #Classes__inverse A_;
+fun inverse (A_:'a group) = #inverse A_;
fun inverse_int i = IntInf.~ i;
@@ -46,15 +40,14 @@
fun mult_int i j = IntInf.+ (i, j);
-val semigroup_int = {Classes__mult = mult_int} : IntInf.int semigroup;
+val semigroup_int = {mult = mult_int} : IntInf.int semigroup;
val monoidl_int =
- {Classes__monoidl_semigroup = semigroup_int,
- Classes__neutral = neutral_int}
- : IntInf.int monoidl;
+ {Classes__monoidl_semigroup = semigroup_int, neutral = neutral_int} :
+ IntInf.int monoidl;
val group_int =
- {Classes__group_monoidl = monoidl_int, Classes__inverse = inverse_int} :
+ {Classes__group_monoidl = monoidl_int, inverse = inverse_int} :
IntInf.int group;
fun pow_nat A_ (Nat.Suc n) x =
--- a/doc-src/IsarAdvanced/Classes/Thy/document/Classes.tex Tue Mar 20 08:27:23 2007 +0100
+++ b/doc-src/IsarAdvanced/Classes/Thy/document/Classes.tex Tue Mar 20 10:23:31 2007 +0100
@@ -5,33 +5,23 @@
\isadelimtheory
\isanewline
\isanewline
-\isanewline
%
\endisadelimtheory
%
\isatagtheory
-\isacommand{theory}\isamarkupfalse%
-\ Classes\isanewline
-\isakeyword{imports}\ Main\isanewline
-\isakeyword{begin}%
+%
\endisatagtheory
{\isafoldtheory}%
%
\isadelimtheory
-\isanewline
%
\endisadelimtheory
%
\isadelimML
-\isanewline
%
\endisadelimML
%
\isatagML
-\isacommand{ML}\isamarkupfalse%
-\ {\isacharverbatimopen}\isanewline
-CodegenSerializer{\isachardot}code{\isacharunderscore}width\ {\isacharcolon}{\isacharequal}\ {\isadigit{7}}{\isadigit{4}}{\isacharsemicolon}\isanewline
-{\isacharverbatimclose}\isanewline
%
\endisatagML
{\isafoldML}%
@@ -112,7 +102,7 @@
\hspace*{4ex}\isa{trans{\isacharcolon}\ eq\ x\ y\ {\isasymand}\ eq\ y\ z\ {\isasymlongrightarrow}\ eq\ x\ z}
\medskip From a theoretic point of view, type classes are leightweight
- modules; indeed, Haskell type classes may be emulated by
+ modules; Haskell type classes may be emulated by
SML functors \cite{classes_modules}.
Isabelle/Isar offers a discipline of type classes which brings
all those aspects together:
@@ -155,15 +145,15 @@
\end{isamarkuptext}%
\isamarkuptrue%
\ \ \ \ \isacommand{class}\isamarkupfalse%
-\ semigroup\ {\isacharequal}\isanewline
+\ semigroup\ {\isacharequal}\ type\ {\isacharplus}\isanewline
\ \ \ \ \ \ \isakeyword{fixes}\ mult\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}{\isasymalpha}\ {\isasymRightarrow}\ {\isasymalpha}\ {\isasymRightarrow}\ {\isasymalpha}{\isachardoublequoteclose}\ \ \ \ {\isacharparenleft}\isakeyword{infixl}\ {\isachardoublequoteopen}\isactrlloc {\isasymotimes}{\isachardoublequoteclose}\ {\isadigit{7}}{\isadigit{0}}{\isacharparenright}\isanewline
\ \ \ \ \ \ \isakeyword{assumes}\ assoc{\isacharcolon}\ {\isachardoublequoteopen}{\isacharparenleft}x\ \isactrlloc {\isasymotimes}\ y{\isacharparenright}\ \isactrlloc {\isasymotimes}\ z\ {\isacharequal}\ x\ \isactrlloc {\isasymotimes}\ {\isacharparenleft}y\ \isactrlloc {\isasymotimes}\ z{\isacharparenright}{\isachardoublequoteclose}%
\begin{isamarkuptext}%
\noindent This \isa{{\isasymCLASS}} specification consists of two
parts: the \qn{operational} part names the class operation (\isa{{\isasymFIXES}}), the \qn{logical} part specifies properties on them
(\isa{{\isasymASSUMES}}). The local \isa{{\isasymFIXES}} and \isa{{\isasymASSUMES}} are lifted to the theory toplevel, yielding the global
- operation \isa{{\isachardoublequote}mult\ {\isacharcolon}{\isacharcolon}\ {\isasymalpha}{\isacharcolon}{\isacharcolon}semigroup\ {\isasymRightarrow}\ {\isasymalpha}\ {\isasymRightarrow}\ {\isasymalpha}{\isachardoublequote}} and the
- global theorem \isa{semigroup{\isachardot}assoc{\isacharcolon}}~\isa{{\isachardoublequote}{\isasymAnd}x\ y\ z{\isacharcolon}{\isacharcolon}{\isasymalpha}{\isacharcolon}{\isacharcolon}semigroup{\isachardot}\ {\isacharparenleft}x\ {\isasymotimes}\ y{\isacharparenright}\ {\isasymotimes}\ z\ {\isacharequal}\ x\ {\isasymotimes}\ {\isacharparenleft}y\ {\isasymotimes}\ z{\isacharparenright}{\isachardoublequote}}.%
+ operation \isa{{\isachardoublequote}mult\ {\isasymColon}\ {\isasymalpha}{\isasymColon}semigroup\ {\isasymRightarrow}\ {\isasymalpha}\ {\isasymRightarrow}\ {\isasymalpha}{\isachardoublequote}} and the
+ global theorem \isa{semigroup{\isachardot}assoc{\isacharcolon}}~\isa{{\isachardoublequote}{\isasymAnd}x\ y\ z\ {\isasymColon}\ {\isasymalpha}{\isasymColon}semigroup{\isachardot}\ {\isacharparenleft}x\ {\isasymotimes}\ y{\isacharparenright}\ {\isasymotimes}\ z\ {\isacharequal}\ x\ {\isasymotimes}\ {\isacharparenleft}y\ {\isasymotimes}\ z{\isacharparenright}{\isachardoublequote}}.%
\end{isamarkuptext}%
\isamarkuptrue%
%
@@ -179,7 +169,7 @@
\isamarkuptrue%
\ \ \ \ \isacommand{instance}\isamarkupfalse%
\ int\ {\isacharcolon}{\isacharcolon}\ semigroup\isanewline
-\ \ \ \ \ \ mult{\isacharunderscore}int{\isacharunderscore}def{\isacharcolon}\ {\isachardoublequoteopen}{\isasymAnd}i\ j\ {\isacharcolon}{\isacharcolon}\ int{\isachardot}\ i\ {\isasymotimes}\ j\ {\isasymequiv}\ i\ {\isacharplus}\ j{\isachardoublequoteclose}\isanewline
+\ \ \ \ \ \ mult{\isacharunderscore}int{\isacharunderscore}def{\isacharcolon}\ {\isachardoublequoteopen}{\isasymAnd}i\ j\ {\isasymColon}\ int{\isachardot}\ i\ {\isasymotimes}\ j\ {\isasymequiv}\ i\ {\isacharplus}\ j{\isachardoublequoteclose}\isanewline
%
\isadelimproof
\ \ \ \ %
@@ -380,7 +370,7 @@
\ {\isacharminus}\isanewline
\ \ \ \ \ \ \ \ \isacommand{from}\isamarkupfalse%
\ mult{\isacharunderscore}list{\isacharunderscore}def\ \isacommand{have}\isamarkupfalse%
-\ {\isachardoublequoteopen}{\isasymAnd}xs\ ys{\isasymColon}{\isacharprime}a\ list{\isachardot}\ xs\ {\isasymotimes}\ ys\ {\isasymequiv}\ xs\ {\isacharat}\ ys{\isachardoublequoteclose}\ \isacommand{{\isachardot}}\isamarkupfalse%
+\ {\isachardoublequoteopen}{\isasymAnd}xs\ ys{\isasymColon}{\isasymalpha}\ list{\isachardot}\ xs\ {\isasymotimes}\ ys\ {\isasymequiv}\ xs\ {\isacharat}\ ys{\isachardoublequoteclose}\ \isacommand{{\isachardot}}\isamarkupfalse%
\isanewline
\ \ \ \ \ \ \ \ \isacommand{moreover}\isamarkupfalse%
\ \isacommand{from}\isamarkupfalse%
@@ -454,7 +444,7 @@
\ \ \ \ \ \ \ \ \isacommand{moreover}\isamarkupfalse%
\ \isacommand{from}\isamarkupfalse%
\ mult{\isacharunderscore}list{\isacharunderscore}def\ neutral{\isacharunderscore}list{\isacharunderscore}def\ \isacommand{have}\isamarkupfalse%
-\ {\isachardoublequoteopen}{\isasymone}\ {\isasymequiv}\ {\isacharbrackleft}{\isacharbrackright}{\isasymColon}{\isacharprime}a\ list{\isachardoublequoteclose}\ \isacommand{by}\isamarkupfalse%
+\ {\isachardoublequoteopen}{\isasymone}\ {\isasymequiv}\ {\isacharbrackleft}{\isacharbrackright}{\isasymColon}{\isasymalpha}\ list{\isachardoublequoteclose}\ \isacommand{by}\isamarkupfalse%
\ simp\isanewline
\ \ \ \ \ \ \ \ \isacommand{ultimately}\isamarkupfalse%
\ \isacommand{show}\isamarkupfalse%
@@ -520,7 +510,88 @@
\isamarkuptrue%
%
\begin{isamarkuptext}%
+The example above gives an impression how Isar type classes work
+ in practice. As stated in the introduction, classes also provide
+ a link to Isar's locale system. Indeed, the logical core of a class
+ is nothing else than a locale:%
+\end{isamarkuptext}%
+\isamarkuptrue%
+\isacommand{class}\isamarkupfalse%
+\ idem\ {\isacharequal}\ type\ {\isacharplus}\isanewline
+\ \ \isakeyword{fixes}\ f\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}{\isasymalpha}\ {\isasymRightarrow}\ {\isasymalpha}{\isachardoublequoteclose}\isanewline
+\ \ \isakeyword{assumes}\ idem{\isacharcolon}\ {\isachardoublequoteopen}f\ {\isacharparenleft}f\ x{\isacharparenright}\ {\isacharequal}\ f\ x{\isachardoublequoteclose}%
+\begin{isamarkuptext}%
+\noindent essentially introduces the locale%
+\end{isamarkuptext}%
+\isamarkuptrue%
%
+\isadelimML
+%
+\endisadelimML
+%
+\isatagML
+%
+\endisatagML
+{\isafoldML}%
+%
+\isadelimML
+%
+\endisadelimML
+\isanewline
+\isacommand{locale}\isamarkupfalse%
+\ idem\ {\isacharequal}\isanewline
+\ \ \isakeyword{fixes}\ f\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}{\isasymalpha}\ {\isasymRightarrow}\ {\isasymalpha}{\isachardoublequoteclose}\isanewline
+\ \ \isakeyword{assumes}\ idem{\isacharcolon}\ {\isachardoublequoteopen}f\ {\isacharparenleft}f\ x{\isacharparenright}\ {\isacharequal}\ f\ x{\isachardoublequoteclose}%
+\begin{isamarkuptext}%
+\noindent together with corresponding constant(s) and axclass%
+\end{isamarkuptext}%
+\isamarkuptrue%
+\isacommand{consts}\isamarkupfalse%
+\ f\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}{\isasymalpha}\ {\isasymRightarrow}\ {\isasymalpha}{\isachardoublequoteclose}\isanewline
+\isanewline
+\isacommand{axclass}\isamarkupfalse%
+\ idem\ {\isacharless}\ type\isanewline
+\ \ idem{\isacharcolon}\ {\isachardoublequoteopen}f\ {\isacharparenleft}f\ x{\isacharparenright}\ {\isacharequal}\ f\ x{\isachardoublequoteclose}%
+\begin{isamarkuptext}%
+This axclass is coupled to the locale by means of an interpretation:%
+\end{isamarkuptext}%
+\isamarkuptrue%
+\isacommand{interpretation}\isamarkupfalse%
+\ idem{\isacharunderscore}class{\isacharcolon}\isanewline
+\ \ idem\ {\isacharbrackleft}{\isachardoublequoteopen}f\ {\isasymColon}\ {\isacharparenleft}{\isacharprime}a{\isasymColon}idem{\isacharparenright}\ {\isasymRightarrow}\ {\isasymalpha}{\isachardoublequoteclose}{\isacharbrackright}\isanewline
+%
+\isadelimproof
+%
+\endisadelimproof
+%
+\isatagproof
+\isacommand{by}\isamarkupfalse%
+\ unfold{\isacharunderscore}locales\ {\isacharparenleft}rule\ idem{\isacharparenright}\isanewline
+%
+\endisatagproof
+{\isafoldproof}%
+%
+\isadelimproof
+%
+\endisadelimproof
+%
+\isadelimML
+%
+\endisadelimML
+%
+\isatagML
+%
+\endisatagML
+{\isafoldML}%
+%
+\isadelimML
+%
+\endisadelimML
+%
+\begin{isamarkuptext}%
+This give you at hand the full power of the Isabelle module system;
+ conclusions in locale \isa{idem} are implicitly propagated
+ to class \isa{idem}.%
\end{isamarkuptext}%
\isamarkuptrue%
%
@@ -529,7 +600,7 @@
\isamarkuptrue%
%
\begin{isamarkuptext}%
-Abstract theories enable reasoning at a general level, while results
+Isabelle locales enable reasoning at a general level, while results
are implicitly transferred to all instances. For example, we can
now establish the \isa{left{\isacharunderscore}cancel} lemma for groups, which
states that the function \isa{{\isacharparenleft}x\ {\isasymcirc}{\isacharparenright}} is injective:%
@@ -547,16 +618,16 @@
\isanewline
\ \ \ \ \isacommand{assume}\isamarkupfalse%
\ {\isachardoublequoteopen}x\ \isactrlloc {\isasymotimes}\ y\ {\isacharequal}\ x\ \isactrlloc {\isasymotimes}\ z{\isachardoublequoteclose}\isanewline
-\ \ \ \ \ \ \ \ \isacommand{then}\isamarkupfalse%
+\ \ \ \ \ \ \isacommand{then}\isamarkupfalse%
\ \isacommand{have}\isamarkupfalse%
\ {\isachardoublequoteopen}x\isactrlloc {\isasymdiv}\ \isactrlloc {\isasymotimes}\ {\isacharparenleft}x\ \isactrlloc {\isasymotimes}\ y{\isacharparenright}\ {\isacharequal}\ x\isactrlloc {\isasymdiv}\ \isactrlloc {\isasymotimes}\ {\isacharparenleft}x\ \isactrlloc {\isasymotimes}\ z{\isacharparenright}{\isachardoublequoteclose}\ \isacommand{by}\isamarkupfalse%
\ simp\isanewline
-\ \ \ \ \ \ \ \ \isacommand{then}\isamarkupfalse%
+\ \ \ \ \ \ \isacommand{then}\isamarkupfalse%
\ \isacommand{have}\isamarkupfalse%
\ {\isachardoublequoteopen}{\isacharparenleft}x\isactrlloc {\isasymdiv}\ \isactrlloc {\isasymotimes}\ x{\isacharparenright}\ \isactrlloc {\isasymotimes}\ y\ {\isacharequal}\ {\isacharparenleft}x\isactrlloc {\isasymdiv}\ \isactrlloc {\isasymotimes}\ x{\isacharparenright}\ \isactrlloc {\isasymotimes}\ z{\isachardoublequoteclose}\ \isacommand{using}\isamarkupfalse%
\ assoc\ \isacommand{by}\isamarkupfalse%
\ simp\isanewline
-\ \ \ \ \ \ \ \ \isacommand{then}\isamarkupfalse%
+\ \ \ \ \ \ \isacommand{then}\isamarkupfalse%
\ \isacommand{show}\isamarkupfalse%
\ {\isachardoublequoteopen}y\ {\isacharequal}\ z{\isachardoublequoteclose}\ \isacommand{using}\isamarkupfalse%
\ neutl\ \isakeyword{and}\ invl\ \isacommand{by}\isamarkupfalse%
@@ -565,7 +636,7 @@
\isanewline
\ \ \ \ \isacommand{assume}\isamarkupfalse%
\ {\isachardoublequoteopen}y\ {\isacharequal}\ z{\isachardoublequoteclose}\isanewline
-\ \ \ \ \ \ \ \ \isacommand{then}\isamarkupfalse%
+\ \ \ \ \ \ \isacommand{then}\isamarkupfalse%
\ \isacommand{show}\isamarkupfalse%
\ {\isachardoublequoteopen}x\ \isactrlloc {\isasymotimes}\ y\ {\isacharequal}\ x\ \isactrlloc {\isasymotimes}\ z{\isachardoublequoteclose}\ \isacommand{by}\isamarkupfalse%
\ simp\isanewline
@@ -581,8 +652,8 @@
\begin{isamarkuptext}%
\noindent Here the \qt{\isa{{\isasymIN}\ group}} target specification
indicates that the result is recorded within that context for later
- use. This local theorem is also lifted to the global one \isa{group{\isachardot}left{\isacharunderscore}cancel{\isacharcolon}} \isa{{\isachardoublequote}{\isasymAnd}x\ y\ z{\isacharcolon}{\isacharcolon}{\isasymalpha}{\isacharcolon}{\isacharcolon}group{\isachardot}\ x\ {\isasymotimes}\ y\ {\isacharequal}\ x\ {\isasymotimes}\ z\ {\isasymlongleftrightarrow}\ y\ {\isacharequal}\ z{\isachardoublequote}}. Since type \isa{int} has been made an instance of
- \isa{group} before, we may refer to that fact as well: \isa{{\isachardoublequote}{\isasymAnd}x\ y\ z{\isacharcolon}{\isacharcolon}int{\isachardot}\ x\ {\isasymotimes}\ y\ {\isacharequal}\ x\ {\isasymotimes}\ z\ {\isasymlongleftrightarrow}\ y\ {\isacharequal}\ z{\isachardoublequote}}.%
+ use. This local theorem is also lifted to the global one \isa{group{\isachardot}left{\isacharunderscore}cancel{\isacharcolon}} \isa{{\isachardoublequote}{\isasymAnd}x\ y\ z\ {\isasymColon}\ {\isasymalpha}{\isasymColon}group{\isachardot}\ x\ {\isasymotimes}\ y\ {\isacharequal}\ x\ {\isasymotimes}\ z\ {\isasymlongleftrightarrow}\ y\ {\isacharequal}\ z{\isachardoublequote}}. Since type \isa{int} has been made an instance of
+ \isa{group} before, we may refer to that fact as well: \isa{{\isachardoublequote}{\isasymAnd}x\ y\ z\ {\isasymColon}\ int{\isachardot}\ x\ {\isasymotimes}\ y\ {\isacharequal}\ x\ {\isasymotimes}\ z\ {\isasymlongleftrightarrow}\ y\ {\isacharequal}\ z{\isachardoublequote}}.%
\end{isamarkuptext}%
\isamarkuptrue%
%
@@ -608,13 +679,13 @@
\isamarkuptrue%
\ \ \ \ \isacommand{fun}\isamarkupfalse%
\isanewline
-\ \ \ \ \ \ pow{\isacharunderscore}nat\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}nat\ {\isasymRightarrow}\ {\isacharprime}a{\isasymColon}monoidl\ {\isasymRightarrow}\ {\isacharprime}a{\isasymColon}monoidl{\isachardoublequoteclose}\ \isakeyword{where}\isanewline
+\ \ \ \ \ \ pow{\isacharunderscore}nat\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}nat\ {\isasymRightarrow}\ {\isasymalpha}{\isasymColon}monoidl\ {\isasymRightarrow}\ {\isasymalpha}{\isasymColon}monoidl{\isachardoublequoteclose}\ \isakeyword{where}\isanewline
\ \ \ \ \ \ {\isachardoublequoteopen}pow{\isacharunderscore}nat\ {\isadigit{0}}\ x\ {\isacharequal}\ {\isasymone}{\isachardoublequoteclose}\isanewline
-\ \ \ \ \ \ {\isachardoublequoteopen}pow{\isacharunderscore}nat\ {\isacharparenleft}Suc\ n{\isacharparenright}\ x\ {\isacharequal}\ x\ {\isasymotimes}\ pow{\isacharunderscore}nat\ n\ x{\isachardoublequoteclose}\isanewline
+\ \ \ \ \ \ {\isacharbar}\ {\isachardoublequoteopen}pow{\isacharunderscore}nat\ {\isacharparenleft}Suc\ n{\isacharparenright}\ x\ {\isacharequal}\ x\ {\isasymotimes}\ pow{\isacharunderscore}nat\ n\ x{\isachardoublequoteclose}\isanewline
\isanewline
\ \ \ \ \isacommand{definition}\isamarkupfalse%
\isanewline
-\ \ \ \ \ \ pow{\isacharunderscore}int\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}int\ {\isasymRightarrow}\ {\isacharprime}a{\isasymColon}group\ {\isasymRightarrow}\ {\isacharprime}a{\isasymColon}group{\isachardoublequoteclose}\ \isakeyword{where}\isanewline
+\ \ \ \ \ \ pow{\isacharunderscore}int\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}int\ {\isasymRightarrow}\ {\isasymalpha}{\isasymColon}group\ {\isasymRightarrow}\ {\isasymalpha}{\isasymColon}group{\isachardoublequoteclose}\ \isakeyword{where}\isanewline
\ \ \ \ \ \ {\isachardoublequoteopen}pow{\isacharunderscore}int\ k\ x\ {\isacharequal}\ {\isacharparenleft}if\ k\ {\isachargreater}{\isacharequal}\ {\isadigit{0}}\isanewline
\ \ \ \ \ \ \ \ then\ pow{\isacharunderscore}nat\ {\isacharparenleft}nat\ k{\isacharparenright}\ x\isanewline
\ \ \ \ \ \ \ \ else\ {\isacharparenleft}pow{\isacharunderscore}nat\ {\isacharparenleft}nat\ {\isacharparenleft}{\isacharminus}\ k{\isacharparenright}{\isacharparenright}\ x{\isacharparenright}{\isasymdiv}{\isacharparenright}{\isachardoublequoteclose}\isanewline
--- a/doc-src/IsarAdvanced/Codegen/Thy/Codegen.thy Tue Mar 20 08:27:23 2007 +0100
+++ b/doc-src/IsarAdvanced/Codegen/Thy/Codegen.thy Tue Mar 20 10:23:31 2007 +0100
@@ -80,6 +80,40 @@
*}
+subsection {* An exmaple: a simple theory of search trees *}
+
+datatype ('a, 'b) searchtree = Leaf "'a\<Colon>linorder" 'b
+ | Branch "('a, 'b) searchtree" "'a" "('a, 'b) searchtree"
+
+fun
+ find :: "('a\<Colon>linorder, 'b) searchtree \<Rightarrow> 'a \<Rightarrow> 'b option" where
+ "find (Leaf key val) it = (if it = key then Some val else None)"
+ | "find (Branch t1 key t2) it = (if it \<le> key then find t1 it else find t2 it)"
+
+fun
+ update :: "'a\<Colon>linorder \<times> 'b \<Rightarrow> ('a, 'b) searchtree \<Rightarrow> ('a, 'b) searchtree" where
+ "update (it, entry) (Leaf key val) = (
+ if it = key then Leaf key entry
+ else if it \<le> key
+ then Branch (Leaf it entry) it (Leaf key val)
+ else Branch (Leaf key val) it (Leaf it entry)
+ )"
+ | "update (it, entry) (Branch t1 key t2) = (
+ if it \<le> key
+ then (Branch (update (it, entry) t1) key t2)
+ else (Branch t1 key (update (it, entry) t2))
+ )"
+
+fun
+ example :: "nat \<Rightarrow> (nat, string) searchtree" where
+ "example n = update (n, ''bar'') (Leaf 0 ''foo'')"
+
+code_gen example (*<*)(SML #)(*>*)(SML "examples/tree.ML")
+
+text {*
+ \lstsml{Thy/examples/tree.ML}
+*}
+
subsection {* Code generation process *}
text {*
@@ -115,7 +149,7 @@
specifications into equivalent but executable counterparts.
The result is a structured collection of \qn{code theorems}.
- \item These \qn{code theorems} then are extracted
+ \item These \qn{code theorems} then are \qn{translated}
into an Haskell-like intermediate
language.
@@ -1175,9 +1209,8 @@
@{index_ML CodegenData.del_preproc: "string -> theory -> theory"} \\
@{index_ML CodegenData.add_datatype: "string * ((string * sort) list * (string * typ list) list)
-> theory -> theory"} \\
- @{index_ML CodegenData.del_datatype: "string -> theory -> theory"} \\
@{index_ML CodegenData.get_datatype: "theory -> string
- -> ((string * sort) list * (string * typ list) list) option"} \\
+ -> (string * sort) list * (string * typ list) list"} \\
@{index_ML CodegenData.get_datatype_of_constr: "theory -> CodegenConsts.const -> string option"}
\end{mldecls}
@@ -1225,9 +1258,6 @@
constraints and a list of constructors with name
and types of arguments.
- \item @{ML CodegenData.del_datatype}~@{text "name"}~@{text "thy"}
- remove a datatype from executable content, if present.
-
\item @{ML CodegenData.get_datatype_of_constr}~@{text "thy"}~@{text "const"}
returns type constructor corresponding to
constructor @{text const}; returns @{text NONE}
--- a/doc-src/IsarAdvanced/Codegen/Thy/document/Codegen.tex Tue Mar 20 08:27:23 2007 +0100
+++ b/doc-src/IsarAdvanced/Codegen/Thy/document/Codegen.tex Tue Mar 20 10:23:31 2007 +0100
@@ -105,6 +105,46 @@
\end{isamarkuptext}%
\isamarkuptrue%
%
+\isamarkupsubsection{An exmaple: a simple theory of search trees%
+}
+\isamarkuptrue%
+\isacommand{datatype}\isamarkupfalse%
+\ {\isacharparenleft}{\isacharprime}a{\isacharcomma}\ {\isacharprime}b{\isacharparenright}\ searchtree\ {\isacharequal}\ Leaf\ {\isachardoublequoteopen}{\isacharprime}a{\isasymColon}linorder{\isachardoublequoteclose}\ {\isacharprime}b\isanewline
+\ \ {\isacharbar}\ Branch\ {\isachardoublequoteopen}{\isacharparenleft}{\isacharprime}a{\isacharcomma}\ {\isacharprime}b{\isacharparenright}\ searchtree{\isachardoublequoteclose}\ {\isachardoublequoteopen}{\isacharprime}a{\isachardoublequoteclose}\ {\isachardoublequoteopen}{\isacharparenleft}{\isacharprime}a{\isacharcomma}\ {\isacharprime}b{\isacharparenright}\ searchtree{\isachardoublequoteclose}\isanewline
+\isanewline
+\isacommand{fun}\isamarkupfalse%
+\isanewline
+\ \ find\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}{\isacharparenleft}{\isacharprime}a{\isasymColon}linorder{\isacharcomma}\ {\isacharprime}b{\isacharparenright}\ searchtree\ {\isasymRightarrow}\ {\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}b\ option{\isachardoublequoteclose}\ \isakeyword{where}\isanewline
+\ \ {\isachardoublequoteopen}find\ {\isacharparenleft}Leaf\ key\ val{\isacharparenright}\ it\ {\isacharequal}\ {\isacharparenleft}if\ it\ {\isacharequal}\ key\ then\ Some\ val\ else\ None{\isacharparenright}{\isachardoublequoteclose}\isanewline
+\ \ {\isacharbar}\ {\isachardoublequoteopen}find\ {\isacharparenleft}Branch\ t{\isadigit{1}}\ key\ t{\isadigit{2}}{\isacharparenright}\ it\ {\isacharequal}\ {\isacharparenleft}if\ it\ {\isasymle}\ key\ then\ find\ t{\isadigit{1}}\ it\ else\ find\ t{\isadigit{2}}\ it{\isacharparenright}{\isachardoublequoteclose}\isanewline
+\isanewline
+\isacommand{fun}\isamarkupfalse%
+\isanewline
+\ \ update\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}{\isacharprime}a{\isasymColon}linorder\ {\isasymtimes}\ {\isacharprime}b\ {\isasymRightarrow}\ {\isacharparenleft}{\isacharprime}a{\isacharcomma}\ {\isacharprime}b{\isacharparenright}\ searchtree\ {\isasymRightarrow}\ {\isacharparenleft}{\isacharprime}a{\isacharcomma}\ {\isacharprime}b{\isacharparenright}\ searchtree{\isachardoublequoteclose}\ \isakeyword{where}\isanewline
+\ \ {\isachardoublequoteopen}update\ {\isacharparenleft}it{\isacharcomma}\ entry{\isacharparenright}\ {\isacharparenleft}Leaf\ key\ val{\isacharparenright}\ {\isacharequal}\ {\isacharparenleft}\isanewline
+\ \ \ \ if\ it\ {\isacharequal}\ key\ then\ Leaf\ key\ entry\isanewline
+\ \ \ \ \ \ else\ if\ it\ {\isasymle}\ key\isanewline
+\ \ \ \ \ \ then\ Branch\ {\isacharparenleft}Leaf\ it\ entry{\isacharparenright}\ it\ {\isacharparenleft}Leaf\ key\ val{\isacharparenright}\isanewline
+\ \ \ \ \ \ else\ Branch\ {\isacharparenleft}Leaf\ key\ val{\isacharparenright}\ it\ {\isacharparenleft}Leaf\ it\ entry{\isacharparenright}\isanewline
+\ \ \ {\isacharparenright}{\isachardoublequoteclose}\isanewline
+\ \ {\isacharbar}\ {\isachardoublequoteopen}update\ {\isacharparenleft}it{\isacharcomma}\ entry{\isacharparenright}\ {\isacharparenleft}Branch\ t{\isadigit{1}}\ key\ t{\isadigit{2}}{\isacharparenright}\ {\isacharequal}\ {\isacharparenleft}\isanewline
+\ \ \ \ if\ it\ {\isasymle}\ key\isanewline
+\ \ \ \ \ \ then\ {\isacharparenleft}Branch\ {\isacharparenleft}update\ {\isacharparenleft}it{\isacharcomma}\ entry{\isacharparenright}\ t{\isadigit{1}}{\isacharparenright}\ key\ t{\isadigit{2}}{\isacharparenright}\isanewline
+\ \ \ \ \ \ else\ {\isacharparenleft}Branch\ t{\isadigit{1}}\ key\ {\isacharparenleft}update\ {\isacharparenleft}it{\isacharcomma}\ entry{\isacharparenright}\ t{\isadigit{2}}{\isacharparenright}{\isacharparenright}\isanewline
+\ \ \ {\isacharparenright}{\isachardoublequoteclose}\isanewline
+\isanewline
+\isacommand{fun}\isamarkupfalse%
+\isanewline
+\ \ example\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}nat\ {\isasymRightarrow}\ {\isacharparenleft}nat{\isacharcomma}\ string{\isacharparenright}\ searchtree{\isachardoublequoteclose}\ \isakeyword{where}\isanewline
+\ \ {\isachardoublequoteopen}example\ n\ {\isacharequal}\ update\ {\isacharparenleft}n{\isacharcomma}\ {\isacharprime}{\isacharprime}bar{\isacharprime}{\isacharprime}{\isacharparenright}\ {\isacharparenleft}Leaf\ {\isadigit{0}}\ {\isacharprime}{\isacharprime}foo{\isacharprime}{\isacharprime}{\isacharparenright}{\isachardoublequoteclose}\isanewline
+\isanewline
+\isacommand{code{\isacharunderscore}gen}\isamarkupfalse%
+\ example\ {\isacharparenleft}SML\ {\isachardoublequoteopen}examples{\isacharslash}tree{\isachardot}ML{\isachardoublequoteclose}{\isacharparenright}%
+\begin{isamarkuptext}%
+\lstsml{Thy/examples/tree.ML}%
+\end{isamarkuptext}%
+\isamarkuptrue%
+%
\isamarkupsubsection{Code generation process%
}
\isamarkuptrue%
@@ -142,7 +182,7 @@
specifications into equivalent but executable counterparts.
The result is a structured collection of \qn{code theorems}.
- \item These \qn{code theorems} then are extracted
+ \item These \qn{code theorems} then are \qn{translated}
into an Haskell-like intermediate
language.
@@ -171,14 +211,11 @@
most cases code generation proceeds without further ado:%
\end{isamarkuptext}%
\isamarkuptrue%
-\isacommand{consts}\isamarkupfalse%
-\isanewline
-\ \ fac\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}nat\ {\isasymRightarrow}\ nat{\isachardoublequoteclose}\isanewline
+\isacommand{fun}\isamarkupfalse%
\isanewline
-\isacommand{primrec}\isamarkupfalse%
-\isanewline
-\ \ {\isachardoublequoteopen}fac\ {\isadigit{0}}\ {\isacharequal}\ {\isadigit{1}}{\isachardoublequoteclose}\isanewline
-\ \ {\isachardoublequoteopen}fac\ {\isacharparenleft}Suc\ n{\isacharparenright}\ {\isacharequal}\ Suc\ n\ {\isacharasterisk}\ fac\ n{\isachardoublequoteclose}%
+\ \ fac\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}nat\ {\isasymRightarrow}\ nat{\isachardoublequoteclose}\ \isakeyword{where}\isanewline
+\ \ \ \ {\isachardoublequoteopen}fac\ {\isadigit{0}}\ {\isacharequal}\ {\isadigit{1}}{\isachardoublequoteclose}\isanewline
+\ \ {\isacharbar}\ {\isachardoublequoteopen}fac\ {\isacharparenleft}Suc\ n{\isacharparenright}\ {\isacharequal}\ Suc\ n\ {\isacharasterisk}\ fac\ n{\isachardoublequoteclose}%
\begin{isamarkuptext}%
This executable specification is now turned to SML code:%
\end{isamarkuptext}%
@@ -419,7 +456,7 @@
\end{isamarkuptext}%
\isamarkuptrue%
\isacommand{class}\isamarkupfalse%
-\ null\ {\isacharequal}\isanewline
+\ null\ {\isacharequal}\ type\ {\isacharplus}\isanewline
\ \ \isakeyword{fixes}\ null\ {\isacharcolon}{\isacharcolon}\ {\isacharprime}a\isanewline
\isanewline
\isacommand{consts}\isamarkupfalse%
@@ -721,7 +758,8 @@
\isacommand{fun}\isamarkupfalse%
\isanewline
\ \ in{\isacharunderscore}interval\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}nat\ {\isasymtimes}\ nat\ {\isasymRightarrow}\ nat\ {\isasymRightarrow}\ bool{\isachardoublequoteclose}\ \isakeyword{where}\isanewline
-\ \ {\isachardoublequoteopen}in{\isacharunderscore}interval\ {\isacharparenleft}k{\isacharcomma}\ l{\isacharparenright}\ n\ {\isasymlongleftrightarrow}\ k\ {\isasymle}\ n\ {\isasymand}\ n\ {\isasymle}\ l{\isachardoublequoteclose}%
+\ \ {\isachardoublequoteopen}in{\isacharunderscore}interval\ {\isacharparenleft}k{\isacharcomma}\ l{\isacharparenright}\ n\ {\isasymlongleftrightarrow}\ k\ {\isasymle}\ n\ {\isasymand}\ n\ {\isasymle}\ l{\isachardoublequoteclose}\isanewline
+%
\isadelimtt
%
\endisadelimtt
@@ -946,12 +984,12 @@
\isacommand{fun}\isamarkupfalse%
\isanewline
\ \ collect{\isacharunderscore}duplicates\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}{\isacharprime}a\ list\ {\isasymRightarrow}\ {\isacharprime}a\ list\ {\isasymRightarrow}\ {\isacharprime}a\ list\ {\isasymRightarrow}\ {\isacharprime}a\ list{\isachardoublequoteclose}\ \isakeyword{where}\isanewline
-\ \ {\isachardoublequoteopen}collect{\isacharunderscore}duplicates\ xs\ ys\ {\isacharbrackleft}{\isacharbrackright}\ {\isacharequal}\ xs{\isachardoublequoteclose}\isanewline
-\ \ {\isachardoublequoteopen}collect{\isacharunderscore}duplicates\ xs\ ys\ {\isacharparenleft}z{\isacharhash}zs{\isacharparenright}\ {\isacharequal}\ {\isacharparenleft}if\ z\ {\isasymin}\ set\ xs\isanewline
-\ \ \ \ then\ if\ z\ {\isasymin}\ set\ ys\isanewline
-\ \ \ \ \ \ then\ collect{\isacharunderscore}duplicates\ xs\ ys\ zs\isanewline
-\ \ \ \ \ \ else\ collect{\isacharunderscore}duplicates\ xs\ {\isacharparenleft}z{\isacharhash}ys{\isacharparenright}\ zs\isanewline
-\ \ \ \ else\ collect{\isacharunderscore}duplicates\ {\isacharparenleft}z{\isacharhash}xs{\isacharparenright}\ {\isacharparenleft}z{\isacharhash}ys{\isacharparenright}\ zs{\isacharparenright}{\isachardoublequoteclose}%
+\ \ \ \ {\isachardoublequoteopen}collect{\isacharunderscore}duplicates\ xs\ ys\ {\isacharbrackleft}{\isacharbrackright}\ {\isacharequal}\ xs{\isachardoublequoteclose}\isanewline
+\ \ {\isacharbar}\ {\isachardoublequoteopen}collect{\isacharunderscore}duplicates\ xs\ ys\ {\isacharparenleft}z{\isacharhash}zs{\isacharparenright}\ {\isacharequal}\ {\isacharparenleft}if\ z\ {\isasymin}\ set\ xs\isanewline
+\ \ \ \ \ \ then\ if\ z\ {\isasymin}\ set\ ys\isanewline
+\ \ \ \ \ \ \ \ then\ collect{\isacharunderscore}duplicates\ xs\ ys\ zs\isanewline
+\ \ \ \ \ \ \ \ else\ collect{\isacharunderscore}duplicates\ xs\ {\isacharparenleft}z{\isacharhash}ys{\isacharparenright}\ zs\isanewline
+\ \ \ \ \ \ else\ collect{\isacharunderscore}duplicates\ {\isacharparenleft}z{\isacharhash}xs{\isacharparenright}\ {\isacharparenleft}z{\isacharhash}ys{\isacharparenright}\ zs{\isacharparenright}{\isachardoublequoteclose}%
\begin{isamarkuptext}%
The membership test during preprocessing is rewritten,
resulting in \isa{op\ mem}, which itself
@@ -986,7 +1024,7 @@
\endisadelimML
\isanewline
\isacommand{class}\isamarkupfalse%
-\ eq\ {\isacharparenleft}\isakeyword{attach}\ {\isachardoublequoteopen}op\ {\isacharequal}{\isachardoublequoteclose}{\isacharparenright}\ {\isacharequal}\ \isakeyword{notes}\ reflexive%
+\ eq\ {\isacharparenleft}\isakeyword{attach}\ {\isachardoublequoteopen}op\ {\isacharequal}{\isachardoublequoteclose}{\isacharparenright}\ {\isacharequal}\ type%
\begin{isamarkuptext}%
This merely introduces a class \isa{eq} with corresponding
operation \isa{op\ {\isacharequal}};
@@ -1031,10 +1069,11 @@
\isacommand{fun}\isamarkupfalse%
\isanewline
\ \ lookup\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}{\isacharparenleft}key\ {\isasymtimes}\ {\isacharprime}a{\isacharparenright}\ list\ {\isasymRightarrow}\ key\ {\isasymRightarrow}\ {\isacharprime}a\ option{\isachardoublequoteclose}\ \isakeyword{where}\isanewline
-\ \ {\isachardoublequoteopen}lookup\ {\isacharbrackleft}{\isacharbrackright}\ l\ {\isacharequal}\ None{\isachardoublequoteclose}\isanewline
-\ \ {\isachardoublequoteopen}lookup\ {\isacharparenleft}{\isacharparenleft}k{\isacharcomma}\ v{\isacharparenright}\ {\isacharhash}\ xs{\isacharparenright}\ l\ {\isacharequal}\ {\isacharparenleft}if\ k\ {\isacharequal}\ l\ then\ Some\ v\ else\ lookup\ xs\ l{\isacharparenright}{\isachardoublequoteclose}\isanewline
+\ \ \ \ {\isachardoublequoteopen}lookup\ {\isacharbrackleft}{\isacharbrackright}\ l\ {\isacharequal}\ None{\isachardoublequoteclose}\isanewline
+\ \ {\isacharbar}\ {\isachardoublequoteopen}lookup\ {\isacharparenleft}{\isacharparenleft}k{\isacharcomma}\ v{\isacharparenright}\ {\isacharhash}\ xs{\isacharparenright}\ l\ {\isacharequal}\ {\isacharparenleft}if\ k\ {\isacharequal}\ l\ then\ Some\ v\ else\ lookup\ xs\ l{\isacharparenright}{\isachardoublequoteclose}\isanewline
%
\isadelimtt
+\isanewline
%
\endisadelimtt
%
@@ -1552,8 +1591,9 @@
\isacommand{fun}\isamarkupfalse%
\isanewline
\ \ dummy{\isacharunderscore}option\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}{\isacharprime}a\ list\ {\isasymRightarrow}\ {\isacharprime}a\ option{\isachardoublequoteclose}\ \isakeyword{where}\isanewline
-\ \ {\isachardoublequoteopen}dummy{\isacharunderscore}option\ {\isacharparenleft}x{\isacharhash}xs{\isacharparenright}\ {\isacharequal}\ Some\ x{\isachardoublequoteclose}\isanewline
-\ \ {\isachardoublequoteopen}dummy{\isacharunderscore}option\ {\isacharbrackleft}{\isacharbrackright}\ {\isacharequal}\ arbitrary{\isachardoublequoteclose}\isanewline
+\ \ \ \ {\isachardoublequoteopen}dummy{\isacharunderscore}option\ {\isacharparenleft}x{\isacharhash}xs{\isacharparenright}\ {\isacharequal}\ Some\ x{\isachardoublequoteclose}\isanewline
+\ \ {\isacharbar}\ {\isachardoublequoteopen}dummy{\isacharunderscore}option\ {\isacharbrackleft}{\isacharbrackright}\ {\isacharequal}\ arbitrary{\isachardoublequoteclose}\isanewline
+\isanewline
\isacommand{code{\isacharunderscore}gen}\isamarkupfalse%
\ dummy{\isacharunderscore}option\ {\isacharparenleft}SML\ {\isachardoublequoteopen}examples{\isacharslash}arbitrary{\isachardot}ML{\isachardoublequoteclose}{\isacharparenright}%
\begin{isamarkuptext}%
@@ -1691,11 +1731,10 @@
\indexml{CodegenData.add-preproc}\verb|CodegenData.add_preproc: string * (theory -> thm list -> thm list)|\isasep\isanewline%
\verb| -> theory -> theory| \\
\indexml{CodegenData.del-preproc}\verb|CodegenData.del_preproc: string -> theory -> theory| \\
- \indexml{CodegenData.add-datatype}\verb|CodegenData.add_datatype: string * (((string * sort) list * (string * typ list) list)|\isasep\isanewline%
-\verb| * thm list Susp.T) -> theory -> theory| \\
- \indexml{CodegenData.del-datatype}\verb|CodegenData.del_datatype: string -> theory -> theory| \\
+ \indexml{CodegenData.add-datatype}\verb|CodegenData.add_datatype: string * ((string * sort) list * (string * typ list) list)|\isasep\isanewline%
+\verb| -> theory -> theory| \\
\indexml{CodegenData.get-datatype}\verb|CodegenData.get_datatype: theory -> string|\isasep\isanewline%
-\verb| -> ((string * sort) list * (string * typ list) list) option| \\
+\verb| -> (string * sort) list * (string * typ list) list| \\
\indexml{CodegenData.get-datatype-of-constr}\verb|CodegenData.get_datatype_of_constr: theory -> CodegenConsts.const -> string option|
\end{mldecls}
@@ -1736,17 +1775,12 @@
\item \verb|CodegenData.del_preproc|~\isa{name}~\isa{thy} removes
generic preprcoessor named \isa{name} from executable content.
- \item \verb|CodegenData.add_datatype|~\isa{{\isacharparenleft}name{\isacharcomma}\ {\isacharparenleft}spec{\isacharcomma}\ cert{\isacharparenright}{\isacharparenright}}~\isa{thy} adds
+ \item \verb|CodegenData.add_datatype|~\isa{{\isacharparenleft}name{\isacharcomma}\ spec{\isacharparenright}}~\isa{thy} adds
a datatype to executable content, with type constructor
\isa{name} and specification \isa{spec}; \isa{spec} is
a pair consisting of a list of type variable with sort
constraints and a list of constructors with name
- and types of arguments. The addition as datatype
- has to be justified giving a certificate of suspended
- theorems as witnesses for injectiveness and distinctness.
-
- \item \verb|CodegenData.del_datatype|~\isa{name}~\isa{thy}
- remove a datatype from executable content, if present.
+ and types of arguments.
\item \verb|CodegenData.get_datatype_of_constr|~\isa{thy}~\isa{const}
returns type constructor corresponding to
--- a/doc-src/IsarAdvanced/Codegen/Thy/examples/bool_literal.ML Tue Mar 20 08:27:23 2007 +0100
+++ b/doc-src/IsarAdvanced/Codegen/Thy/examples/bool_literal.ML Tue Mar 20 10:23:31 2007 +0100
@@ -6,10 +6,10 @@
datatype boola = True | False;
-fun op_conj y True = y
- | op_conj x False = False
- | op_conj True y = y
- | op_conj False x = False;
+fun op_and y True = y
+ | op_and x False = False
+ | op_and True y = y
+ | op_and False x = False;
end; (*struct HOL*)
@@ -29,7 +29,7 @@
struct
fun in_interval (k, l) n =
- HOL.op_conj (Nat.less_eq_nat k n) (Nat.less_eq_nat n l);
+ HOL.op_and (Nat.less_eq_nat k n) (Nat.less_eq_nat n l);
end; (*struct Codegen*)
--- a/doc-src/IsarAdvanced/Codegen/Thy/examples/lexicographic.ML Tue Mar 20 08:27:23 2007 +0100
+++ b/doc-src/IsarAdvanced/Codegen/Thy/examples/lexicographic.ML Tue Mar 20 10:23:31 2007 +0100
@@ -21,7 +21,7 @@
structure Codegen =
struct
-fun less_eq_prod (A1_, A2_) B_ (x1, y1) (x2, y2) =
+fun less_eq_times (A1_, A2_) B_ (x1, y1) (x2, y2) =
Orderings.less A2_ x1 x2 orelse
Code_Generator.op_eq A1_ x1 x2 andalso Orderings.less_eq B_ y1 y2;