--- a/doc-src/IsarAdvanced/Classes/Thy/Classes.thy Wed Dec 05 04:34:15 2007 +0100
+++ b/doc-src/IsarAdvanced/Classes/Thy/Classes.thy Wed Dec 05 14:15:39 2007 +0100
@@ -12,6 +12,8 @@
syntax
"_alpha" :: "type" ("\<alpha>")
"_alpha_ofsort" :: "sort \<Rightarrow> type" ("\<alpha>()\<Colon>_" [0] 1000)
+ "_beta" :: "type" ("\<beta>")
+ "_beta_ofsort" :: "sort \<Rightarrow> type" ("\<beta>()\<Colon>_" [0] 1000)
parse_ast_translation {*
let
@@ -20,8 +22,14 @@
fun alpha_ofsort_ast_tr [ast] =
Syntax.Appl [Syntax.Constant "_ofsort", Syntax.Variable "'a", ast]
| alpha_ofsort_ast_tr asts = raise Syntax.AST ("alpha_ast_tr", asts);
+ fun beta_ast_tr [] = Syntax.Variable "'b"
+ | beta_ast_tr asts = raise Syntax.AST ("beta_ast_tr", asts);
+ fun beta_ofsort_ast_tr [ast] =
+ Syntax.Appl [Syntax.Constant "_ofsort", Syntax.Variable "'b", ast]
+ | beta_ofsort_ast_tr asts = raise Syntax.AST ("beta_ast_tr", asts);
in [
- ("_alpha", alpha_ast_tr), ("_alpha_ofsort", alpha_ofsort_ast_tr)
+ ("_alpha", alpha_ast_tr), ("_alpha_ofsort", alpha_ofsort_ast_tr),
+ ("_beta", beta_ast_tr), ("_beta_ofsort", beta_ofsort_ast_tr)
] end
*}
(*>*)
@@ -145,38 +153,54 @@
The concrete type @{text "int"} is made a @{text "semigroup"}
instance by providing a suitable definition for the class parameter
@{text "mult"} and a proof for the specification of @{text "assoc"}.
+ This is accomplished by the @{text "\<INSTANTIATION>"} target:
*}
- instance int :: semigroup
- mult_int_def: "i \<otimes> j \<equiv> i + j"
- proof
+ instantiation int :: semigroup
+ begin
+
+ definition
+ mult_int_def: "i \<otimes> j = i + (j\<Colon>int)"
+
+ instance 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 .
qed
+ end
+
text {*
- \noindent From now on, the type-checker will consider @{text "int"}
- as a @{text "semigroup"} automatically, i.e.\ any general results
- are immediately available on concrete instances.
-
- Note that the first proof step is the @{text default} method,
- which for instantiation proofs maps to the @{text intro_classes} method.
- This boils down an instantiation judgement to the relevant primitive
+ \noindent @{text "\<INSTANTIATION>"} allows to define class parameters
+ at a particular instance using common specification tools (here,
+ @{text "\<DEFINITION>"}). The concluding @{text "\<INSTANCE>"}
+ opens a proof that the given parameters actually conform
+ to the class specification. Note that the first proof step
+ is the @{text default} method,
+ which for such instance proofs maps to the @{text intro_classes} method.
+ This boils down an instance judgement to the relevant primitive
proof goals and should conveniently always be the first method applied
in an instantiation proof.
+ From now on, the type-checker will consider @{text "int"}
+ as a @{text "semigroup"} automatically, i.e.\ any general results
+ are immediately available on concrete instances.
\medskip Another instance of @{text "semigroup"} are the natural numbers:
*}
- instance nat :: semigroup
- mult_nat_def: "m \<otimes> n \<equiv> m + n"
- proof
+ instantiation nat :: semigroup
+ begin
+
+ definition
+ mult_nat_def: "m \<otimes> n = m + (n\<Colon>nat)"
+
+ instance proof
fix m n q :: nat
show "m \<otimes> n \<otimes> q = m \<otimes> (n \<otimes> q)"
unfolding mult_nat_def by simp
qed
+ end
subsection {* Lifting and parametric types *}
@@ -187,14 +211,20 @@
using our simple algebra:
*}
- instance * :: (semigroup, semigroup) semigroup
- mult_prod_def: "p\<^isub>1 \<otimes> p\<^isub>2 \<equiv> (fst p\<^isub>1 \<otimes> fst p\<^isub>2, snd p\<^isub>1 \<otimes> snd p\<^isub>2)"
- proof
- fix p\<^isub>1 p\<^isub>2 p\<^isub>3 :: "'a\<Colon>semigroup \<times> 'b\<Colon>semigroup"
+ instantiation * :: (semigroup, semigroup) semigroup
+ begin
+
+ definition
+ mult_prod_def: "p\<^isub>1 \<otimes> p\<^isub>2 = (fst p\<^isub>1 \<otimes> fst p\<^isub>2, snd p\<^isub>1 \<otimes> snd p\<^isub>2)"
+
+ instance proof
+ fix p\<^isub>1 p\<^isub>2 p\<^isub>3 :: "\<alpha>\<Colon>semigroup \<times> \<beta>\<Colon>semigroup"
show "p\<^isub>1 \<otimes> p\<^isub>2 \<otimes> p\<^isub>3 = p\<^isub>1 \<otimes> (p\<^isub>2 \<otimes> p\<^isub>3)"
unfolding mult_prod_def by (simp add: assoc)
qed
+ end
+
text {*
\noindent Associativity from product semigroups is
established using
@@ -223,33 +253,45 @@
text {*
\noindent Again, we prove some instances, by
providing suitable parameter definitions and proofs for the
- additional specifications:
+ additional specifications. Obverve that instantiations
+ for types with the same arity may be simultaneous:
*}
- instance nat :: monoidl
- neutral_nat_def: "\<one> \<equiv> 0"
- proof
+ instantiation nat and int :: monoidl
+ begin
+
+ definition
+ neutral_nat_def: "\<one> = (0\<Colon>nat)"
+
+ definition
+ neutral_int_def: "\<one> = (0\<Colon>int)"
+
+ instance proof
fix n :: nat
show "\<one> \<otimes> n = n"
unfolding neutral_nat_def mult_nat_def by simp
- qed
-
- instance int :: monoidl
- neutral_int_def: "\<one> \<equiv> 0"
- proof
+ next
fix k :: int
show "\<one> \<otimes> k = k"
unfolding neutral_int_def mult_int_def by simp
qed
- instance * :: (monoidl, monoidl) monoidl
- neutral_prod_def: "\<one> \<equiv> (\<one>, \<one>)"
- proof
- fix p :: "'a\<Colon>monoidl \<times> 'b\<Colon>monoidl"
+ end
+
+ instantiation * :: (monoidl, monoidl) monoidl
+ begin
+
+ definition
+ neutral_prod_def: "\<one> = (\<one>, \<one>)"
+
+ instance proof
+ fix p :: "\<alpha>\<Colon>monoidl \<times> \<beta>\<Colon>monoidl"
show "\<one> \<otimes> p = p"
unfolding neutral_prod_def mult_prod_def by (simp add: neutl)
qed
+ end
+
text {*
\noindent Fully-fledged monoids are modelled by another subclass
which does not add new parameters but tightens the specification:
@@ -258,27 +300,32 @@
class monoid = monoidl +
assumes neutr: "x \<otimes> \<one> = x"
- instance nat :: monoid
- proof
+ instantiation nat and int :: monoid
+ begin
+
+ instance proof
fix n :: nat
show "n \<otimes> \<one> = n"
unfolding neutral_nat_def mult_nat_def by simp
- qed
-
- instance int :: monoid
- proof
+ next
fix k :: int
show "k \<otimes> \<one> = k"
unfolding neutral_int_def mult_int_def by simp
qed
- instance * :: (monoid, monoid) monoid
- proof
- fix p :: "'a\<Colon>monoid \<times> 'b\<Colon>monoid"
+ end
+
+ instantiation * :: (monoid, monoid) monoid
+ begin
+
+ instance proof
+ fix p :: "\<alpha>\<Colon>monoid \<times> \<beta>\<Colon>monoid"
show "p \<otimes> \<one> = p"
unfolding neutral_prod_def mult_prod_def by (simp add: neutr)
qed
+ end
+
text {*
\noindent To finish our small algebra example, we add a @{text "group"} class
with a corresponding instance:
@@ -288,15 +335,21 @@
fixes inverse :: "\<alpha> \<Rightarrow> \<alpha>" ("(_\<div>)" [1000] 999)
assumes invl: "x\<div> \<otimes> x = \<one>"
- instance int :: group
- inverse_int_def: "i\<div> \<equiv> - i"
- proof
+ instantiation int :: group
+ begin
+
+ definition
+ inverse_int_def: "i\<div> = - (i\<Colon>int)"
+
+ instance proof
fix i :: int
have "-i + i = 0" by simp
then show "i\<div> \<otimes> i = \<one>"
unfolding mult_int_def neutral_int_def inverse_int_def .
qed
+ end
+
section {* Type classes as locales *}
subsection {* A look behind the scene *}
@@ -335,7 +388,7 @@
text {* \noindent together with a corresponding interpretation: *}
interpretation idem_class:
- idem ["f \<Colon> ('a\<Colon>idem) \<Rightarrow> \<alpha>"]
+ idem ["f \<Colon> (\<alpha>\<Colon>idem) \<Rightarrow> \<alpha>"]
by unfold_locales (rule idem)
(*<*) setup {* Sign.parent_path *} (*>*)
text {*
@@ -431,7 +484,7 @@
*}
fun
- replicate :: "nat \<Rightarrow> 'a list \<Rightarrow> 'a list"
+ replicate :: "nat \<Rightarrow> \<alpha> list \<Rightarrow> \<alpha> list"
where
"replicate 0 _ = []"
| "replicate (Suc n) xs = xs @ replicate n xs"
@@ -524,8 +577,9 @@
text {*
Turning back to the first motivation for type classes,
namely overloading, it is obvious that overloading
- stemming from @{text "\<CLASS>"} and @{text "\<INSTANCE>"}
- statements naturally maps to Haskell type classes.
+ stemming from @{text "\<CLASS>"} statements and
+ @{text "\<INSTANTIATION>"}
+ targets naturally maps to Haskell type classes.
The code generator framework \cite{isabelle-codegen}
takes this into account. Concerning target languages
lacking type classes (e.g.~SML), type classes
@@ -533,17 +587,6 @@
For example, lets go back to the power function:
*}
-(* fun
- pow_nat :: "nat \<Rightarrow> \<alpha>\<Colon>group \<Rightarrow> \<alpha>\<Colon>group" where
- "pow_nat 0 x = \<one>"
- | "pow_nat (Suc n) x = x \<otimes> pow_nat n x"
-
- definition
- pow_int :: "int \<Rightarrow> \<alpha>\<Colon>group \<Rightarrow> \<alpha>\<Colon>group" where
- "pow_int k x = (if k >= 0
- then pow_nat (nat k) x
- else (pow_nat (nat (- k)) x)\<div>)"*)
-
definition
example :: int where
"example = pow_int 10 (-2)"
--- a/doc-src/IsarAdvanced/Classes/Thy/document/Classes.tex Wed Dec 05 04:34:15 2007 +0100
+++ b/doc-src/IsarAdvanced/Classes/Thy/document/Classes.tex Wed Dec 05 14:15:39 2007 +0100
@@ -166,15 +166,22 @@
\begin{isamarkuptext}%
The concrete type \isa{int} is made a \isa{semigroup}
instance by providing a suitable definition for the class parameter
- \isa{mult} and a proof for the specification of \isa{assoc}.%
+ \isa{mult} and a proof for the specification of \isa{assoc}.
+ This is accomplished by the \isa{{\isasymINSTANTIATION}} target:%
\end{isamarkuptext}%
\isamarkuptrue%
-\ \ \ \ \isacommand{instance}\isamarkupfalse%
+\ \ \ \ \isacommand{instantiation}\isamarkupfalse%
\ int\ {\isacharcolon}{\isacharcolon}\ semigroup\isanewline
-\ \ \ \ \ \ mult{\isacharunderscore}int{\isacharunderscore}def{\isacharcolon}\ {\isachardoublequoteopen}i\ {\isasymotimes}\ j\ {\isasymequiv}\ i\ {\isacharplus}\ j{\isachardoublequoteclose}\isanewline
+\ \ \ \ \isakeyword{begin}\isanewline
+\isanewline
+\ \ \ \ \isacommand{definition}\isamarkupfalse%
+\isanewline
+\ \ \ \ \ \ mult{\isacharunderscore}int{\isacharunderscore}def{\isacharcolon}\ {\isachardoublequoteopen}i\ {\isasymotimes}\ j\ {\isacharequal}\ i\ {\isacharplus}\ {\isacharparenleft}j{\isasymColon}int{\isacharparenright}{\isachardoublequoteclose}\isanewline
+\isanewline
+\ \ \ \ \isacommand{instance}\isamarkupfalse%
%
\isadelimproof
-\ \ \ \ %
+\ %
\endisadelimproof
%
\isatagproof
@@ -198,27 +205,40 @@
\isadelimproof
%
\endisadelimproof
+\isanewline
+\isanewline
+\ \ \ \ \isacommand{end}\isamarkupfalse%
%
\begin{isamarkuptext}%
-\noindent From now on, the type-checker will consider \isa{int}
- as a \isa{semigroup} automatically, i.e.\ any general results
- are immediately available on concrete instances.
-
- Note that the first proof step is the \isa{default} method,
- which for instantiation proofs maps to the \isa{intro{\isacharunderscore}classes} method.
- This boils down an instantiation judgement to the relevant primitive
+\noindent \isa{{\isasymINSTANTIATION}} allows to define class parameters
+ at a particular instance using common specification tools (here,
+ \isa{{\isasymDEFINITION}}). The concluding \isa{{\isasymINSTANCE}}
+ opens a proof that the given parameters actually conform
+ to the class specification. Note that the first proof step
+ is the \isa{default} method,
+ which for such instance proofs maps to the \isa{intro{\isacharunderscore}classes} method.
+ This boils down an instance judgement to the relevant primitive
proof goals and should conveniently always be the first method applied
in an instantiation proof.
+ From now on, the type-checker will consider \isa{int}
+ as a \isa{semigroup} automatically, i.e.\ any general results
+ are immediately available on concrete instances.
\medskip Another instance of \isa{semigroup} are the natural numbers:%
\end{isamarkuptext}%
\isamarkuptrue%
-\ \ \ \ \isacommand{instance}\isamarkupfalse%
+\ \ \ \ \isacommand{instantiation}\isamarkupfalse%
\ nat\ {\isacharcolon}{\isacharcolon}\ semigroup\isanewline
-\ \ \ \ \ \ mult{\isacharunderscore}nat{\isacharunderscore}def{\isacharcolon}\ {\isachardoublequoteopen}m\ {\isasymotimes}\ n\ {\isasymequiv}\ m\ {\isacharplus}\ n{\isachardoublequoteclose}\isanewline
+\ \ \ \ \isakeyword{begin}\isanewline
+\isanewline
+\ \ \ \ \isacommand{definition}\isamarkupfalse%
+\isanewline
+\ \ \ \ \ \ mult{\isacharunderscore}nat{\isacharunderscore}def{\isacharcolon}\ {\isachardoublequoteopen}m\ {\isasymotimes}\ n\ {\isacharequal}\ m\ {\isacharplus}\ {\isacharparenleft}n{\isasymColon}nat{\isacharparenright}{\isachardoublequoteclose}\isanewline
+\isanewline
+\ \ \ \ \isacommand{instance}\isamarkupfalse%
%
\isadelimproof
-\ \ \ \ %
+\ %
\endisadelimproof
%
\isatagproof
@@ -239,6 +259,9 @@
\isadelimproof
%
\endisadelimproof
+\isanewline
+\isanewline
+\ \ \ \ \isacommand{end}\isamarkupfalse%
%
\isamarkupsubsection{Lifting and parametric types%
}
@@ -251,19 +274,25 @@
using our simple algebra:%
\end{isamarkuptext}%
\isamarkuptrue%
-\ \ \ \ \isacommand{instance}\isamarkupfalse%
+\ \ \ \ \isacommand{instantiation}\isamarkupfalse%
\ {\isacharasterisk}\ {\isacharcolon}{\isacharcolon}\ {\isacharparenleft}semigroup{\isacharcomma}\ semigroup{\isacharparenright}\ semigroup\isanewline
-\ \ \ \ \ \ mult{\isacharunderscore}prod{\isacharunderscore}def{\isacharcolon}\ {\isachardoublequoteopen}p\isactrlisub {\isadigit{1}}\ {\isasymotimes}\ p\isactrlisub {\isadigit{2}}\ {\isasymequiv}\ {\isacharparenleft}fst\ p\isactrlisub {\isadigit{1}}\ {\isasymotimes}\ fst\ p\isactrlisub {\isadigit{2}}{\isacharcomma}\ snd\ p\isactrlisub {\isadigit{1}}\ {\isasymotimes}\ snd\ p\isactrlisub {\isadigit{2}}{\isacharparenright}{\isachardoublequoteclose}\isanewline
+\ \ \ \ \isakeyword{begin}\isanewline
+\isanewline
+\ \ \ \ \isacommand{definition}\isamarkupfalse%
+\isanewline
+\ \ \ \ \ \ mult{\isacharunderscore}prod{\isacharunderscore}def{\isacharcolon}\ {\isachardoublequoteopen}p\isactrlisub {\isadigit{1}}\ {\isasymotimes}\ p\isactrlisub {\isadigit{2}}\ {\isacharequal}\ {\isacharparenleft}fst\ p\isactrlisub {\isadigit{1}}\ {\isasymotimes}\ fst\ p\isactrlisub {\isadigit{2}}{\isacharcomma}\ snd\ p\isactrlisub {\isadigit{1}}\ {\isasymotimes}\ snd\ p\isactrlisub {\isadigit{2}}{\isacharparenright}{\isachardoublequoteclose}\isanewline
+\isanewline
+\ \ \ \ \isacommand{instance}\isamarkupfalse%
%
\isadelimproof
-\ \ \ \ %
+\ %
\endisadelimproof
%
\isatagproof
\isacommand{proof}\isamarkupfalse%
\isanewline
\ \ \ \ \ \ \isacommand{fix}\isamarkupfalse%
-\ p\isactrlisub {\isadigit{1}}\ p\isactrlisub {\isadigit{2}}\ p\isactrlisub {\isadigit{3}}\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}{\isacharprime}a{\isasymColon}semigroup\ {\isasymtimes}\ {\isacharprime}b{\isasymColon}semigroup{\isachardoublequoteclose}\isanewline
+\ p\isactrlisub {\isadigit{1}}\ p\isactrlisub {\isadigit{2}}\ p\isactrlisub {\isadigit{3}}\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}{\isasymalpha}{\isasymColon}semigroup\ {\isasymtimes}\ {\isasymbeta}{\isasymColon}semigroup{\isachardoublequoteclose}\isanewline
\ \ \ \ \ \ \isacommand{show}\isamarkupfalse%
\ {\isachardoublequoteopen}p\isactrlisub {\isadigit{1}}\ {\isasymotimes}\ p\isactrlisub {\isadigit{2}}\ {\isasymotimes}\ p\isactrlisub {\isadigit{3}}\ {\isacharequal}\ p\isactrlisub {\isadigit{1}}\ {\isasymotimes}\ {\isacharparenleft}p\isactrlisub {\isadigit{2}}\ {\isasymotimes}\ p\isactrlisub {\isadigit{3}}{\isacharparenright}{\isachardoublequoteclose}\isanewline
\ \ \ \ \ \ \ \ \isacommand{unfolding}\isamarkupfalse%
@@ -277,6 +306,9 @@
\isadelimproof
%
\endisadelimproof
+\ \ \ \ \ \ \isanewline
+\isanewline
+\ \ \ \ \isacommand{end}\isamarkupfalse%
%
\begin{isamarkuptext}%
\noindent Associativity from product semigroups is
@@ -308,15 +340,26 @@
\begin{isamarkuptext}%
\noindent Again, we prove some instances, by
providing suitable parameter definitions and proofs for the
- additional specifications:%
+ additional specifications. Obverve that instantiations
+ for types with the same arity may be simultaneous:%
\end{isamarkuptext}%
\isamarkuptrue%
+\ \ \ \ \isacommand{instantiation}\isamarkupfalse%
+\ nat\ \isakeyword{and}\ int\ {\isacharcolon}{\isacharcolon}\ monoidl\isanewline
+\ \ \ \ \isakeyword{begin}\isanewline
+\isanewline
+\ \ \ \ \isacommand{definition}\isamarkupfalse%
+\isanewline
+\ \ \ \ \ \ neutral{\isacharunderscore}nat{\isacharunderscore}def{\isacharcolon}\ {\isachardoublequoteopen}{\isasymone}\ {\isacharequal}\ {\isacharparenleft}{\isadigit{0}}{\isasymColon}nat{\isacharparenright}{\isachardoublequoteclose}\isanewline
+\isanewline
+\ \ \ \ \isacommand{definition}\isamarkupfalse%
+\isanewline
+\ \ \ \ \ \ neutral{\isacharunderscore}int{\isacharunderscore}def{\isacharcolon}\ {\isachardoublequoteopen}{\isasymone}\ {\isacharequal}\ {\isacharparenleft}{\isadigit{0}}{\isasymColon}int{\isacharparenright}{\isachardoublequoteclose}\isanewline
+\isanewline
\ \ \ \ \isacommand{instance}\isamarkupfalse%
-\ nat\ {\isacharcolon}{\isacharcolon}\ monoidl\isanewline
-\ \ \ \ \ \ neutral{\isacharunderscore}nat{\isacharunderscore}def{\isacharcolon}\ {\isachardoublequoteopen}{\isasymone}\ {\isasymequiv}\ {\isadigit{0}}{\isachardoublequoteclose}\isanewline
%
\isadelimproof
-\ \ \ \ %
+\ %
\endisadelimproof
%
\isatagproof
@@ -329,26 +372,7 @@
\ \ \ \ \ \ \ \ \isacommand{unfolding}\isamarkupfalse%
\ neutral{\isacharunderscore}nat{\isacharunderscore}def\ mult{\isacharunderscore}nat{\isacharunderscore}def\ \isacommand{by}\isamarkupfalse%
\ simp\isanewline
-\ \ \ \ \isacommand{qed}\isamarkupfalse%
-%
-\endisatagproof
-{\isafoldproof}%
-%
-\isadelimproof
-\isanewline
-%
-\endisadelimproof
-\isanewline
-\ \ \ \ \isacommand{instance}\isamarkupfalse%
-\ int\ {\isacharcolon}{\isacharcolon}\ monoidl\isanewline
-\ \ \ \ \ \ neutral{\isacharunderscore}int{\isacharunderscore}def{\isacharcolon}\ {\isachardoublequoteopen}{\isasymone}\ {\isasymequiv}\ {\isadigit{0}}{\isachardoublequoteclose}\isanewline
-%
-\isadelimproof
-\ \ \ \ %
-\endisadelimproof
-%
-\isatagproof
-\isacommand{proof}\isamarkupfalse%
+\ \ \ \ \isacommand{next}\isamarkupfalse%
\isanewline
\ \ \ \ \ \ \isacommand{fix}\isamarkupfalse%
\ k\ {\isacharcolon}{\isacharcolon}\ int\isanewline
@@ -363,23 +387,32 @@
{\isafoldproof}%
%
\isadelimproof
-\isanewline
%
\endisadelimproof
\isanewline
-\ \ \ \ \isacommand{instance}\isamarkupfalse%
+\isanewline
+\ \ \ \ \isacommand{end}\isamarkupfalse%
+\isanewline
+\isanewline
+\ \ \ \ \isacommand{instantiation}\isamarkupfalse%
\ {\isacharasterisk}\ {\isacharcolon}{\isacharcolon}\ {\isacharparenleft}monoidl{\isacharcomma}\ monoidl{\isacharparenright}\ monoidl\isanewline
-\ \ \ \ \ \ neutral{\isacharunderscore}prod{\isacharunderscore}def{\isacharcolon}\ {\isachardoublequoteopen}{\isasymone}\ {\isasymequiv}\ {\isacharparenleft}{\isasymone}{\isacharcomma}\ {\isasymone}{\isacharparenright}{\isachardoublequoteclose}\isanewline
+\ \ \ \ \isakeyword{begin}\isanewline
+\isanewline
+\ \ \ \ \isacommand{definition}\isamarkupfalse%
+\isanewline
+\ \ \ \ \ \ neutral{\isacharunderscore}prod{\isacharunderscore}def{\isacharcolon}\ {\isachardoublequoteopen}{\isasymone}\ {\isacharequal}\ {\isacharparenleft}{\isasymone}{\isacharcomma}\ {\isasymone}{\isacharparenright}{\isachardoublequoteclose}\isanewline
+\isanewline
+\ \ \ \ \isacommand{instance}\isamarkupfalse%
%
\isadelimproof
-\ \ \ \ %
+\ %
\endisadelimproof
%
\isatagproof
\isacommand{proof}\isamarkupfalse%
\isanewline
\ \ \ \ \ \ \isacommand{fix}\isamarkupfalse%
-\ p\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}{\isacharprime}a{\isasymColon}monoidl\ {\isasymtimes}\ {\isacharprime}b{\isasymColon}monoidl{\isachardoublequoteclose}\isanewline
+\ p\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}{\isasymalpha}{\isasymColon}monoidl\ {\isasymtimes}\ {\isasymbeta}{\isasymColon}monoidl{\isachardoublequoteclose}\isanewline
\ \ \ \ \ \ \isacommand{show}\isamarkupfalse%
\ {\isachardoublequoteopen}{\isasymone}\ {\isasymotimes}\ p\ {\isacharequal}\ p{\isachardoublequoteclose}\isanewline
\ \ \ \ \ \ \ \ \isacommand{unfolding}\isamarkupfalse%
@@ -393,6 +426,9 @@
\isadelimproof
%
\endisadelimproof
+\isanewline
+\isanewline
+\ \ \ \isacommand{end}\isamarkupfalse%
%
\begin{isamarkuptext}%
\noindent Fully-fledged monoids are modelled by another subclass
@@ -403,11 +439,14 @@
\ monoid\ {\isacharequal}\ monoidl\ {\isacharplus}\isanewline
\ \ \ \ \ \ \isakeyword{assumes}\ neutr{\isacharcolon}\ {\isachardoublequoteopen}x\ {\isasymotimes}\ {\isasymone}\ {\isacharequal}\ x{\isachardoublequoteclose}\isanewline
\isanewline
+\ \ \ \ \isacommand{instantiation}\isamarkupfalse%
+\ nat\ \isakeyword{and}\ int\ {\isacharcolon}{\isacharcolon}\ monoid\ \isanewline
+\ \ \ \ \isakeyword{begin}\isanewline
+\isanewline
\ \ \ \ \isacommand{instance}\isamarkupfalse%
-\ nat\ {\isacharcolon}{\isacharcolon}\ monoid\ \isanewline
%
\isadelimproof
-\ \ \ \ %
+\ %
\endisadelimproof
%
\isatagproof
@@ -420,25 +459,7 @@
\ \ \ \ \ \ \ \ \isacommand{unfolding}\isamarkupfalse%
\ neutral{\isacharunderscore}nat{\isacharunderscore}def\ mult{\isacharunderscore}nat{\isacharunderscore}def\ \isacommand{by}\isamarkupfalse%
\ simp\isanewline
-\ \ \ \ \isacommand{qed}\isamarkupfalse%
-%
-\endisatagproof
-{\isafoldproof}%
-%
-\isadelimproof
-\isanewline
-%
-\endisadelimproof
-\isanewline
-\ \ \ \ \isacommand{instance}\isamarkupfalse%
-\ int\ {\isacharcolon}{\isacharcolon}\ monoid\isanewline
-%
-\isadelimproof
-\ \ \ \ %
-\endisadelimproof
-%
-\isatagproof
-\isacommand{proof}\isamarkupfalse%
+\ \ \ \ \isacommand{next}\isamarkupfalse%
\isanewline
\ \ \ \ \ \ \isacommand{fix}\isamarkupfalse%
\ k\ {\isacharcolon}{\isacharcolon}\ int\isanewline
@@ -453,22 +474,28 @@
{\isafoldproof}%
%
\isadelimproof
-\isanewline
%
\endisadelimproof
\isanewline
+\isanewline
+\ \ \ \ \isacommand{end}\isamarkupfalse%
+\isanewline
+\isanewline
+\ \ \ \ \isacommand{instantiation}\isamarkupfalse%
+\ {\isacharasterisk}\ {\isacharcolon}{\isacharcolon}\ {\isacharparenleft}monoid{\isacharcomma}\ monoid{\isacharparenright}\ monoid\isanewline
+\ \ \ \ \isakeyword{begin}\isanewline
+\isanewline
\ \ \ \ \isacommand{instance}\isamarkupfalse%
-\ {\isacharasterisk}\ {\isacharcolon}{\isacharcolon}\ {\isacharparenleft}monoid{\isacharcomma}\ monoid{\isacharparenright}\ monoid\isanewline
%
\isadelimproof
-\ \ \ \ %
+\ %
\endisadelimproof
%
\isatagproof
\isacommand{proof}\isamarkupfalse%
\ \isanewline
\ \ \ \ \ \ \isacommand{fix}\isamarkupfalse%
-\ p\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}{\isacharprime}a{\isasymColon}monoid\ {\isasymtimes}\ {\isacharprime}b{\isasymColon}monoid{\isachardoublequoteclose}\isanewline
+\ p\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}{\isasymalpha}{\isasymColon}monoid\ {\isasymtimes}\ {\isasymbeta}{\isasymColon}monoid{\isachardoublequoteclose}\isanewline
\ \ \ \ \ \ \isacommand{show}\isamarkupfalse%
\ {\isachardoublequoteopen}p\ {\isasymotimes}\ {\isasymone}\ {\isacharequal}\ p{\isachardoublequoteclose}\isanewline
\ \ \ \ \ \ \ \ \isacommand{unfolding}\isamarkupfalse%
@@ -482,6 +509,9 @@
\isadelimproof
%
\endisadelimproof
+\isanewline
+\isanewline
+\ \ \ \ \isacommand{end}\isamarkupfalse%
%
\begin{isamarkuptext}%
\noindent To finish our small algebra example, we add a \isa{group} class
@@ -493,12 +523,18 @@
\ \ \ \ \ \ \isakeyword{fixes}\ inverse\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}{\isasymalpha}\ {\isasymRightarrow}\ {\isasymalpha}{\isachardoublequoteclose}\ \ \ \ {\isacharparenleft}{\isachardoublequoteopen}{\isacharparenleft}{\isacharunderscore}{\isasymdiv}{\isacharparenright}{\isachardoublequoteclose}\ {\isacharbrackleft}{\isadigit{1}}{\isadigit{0}}{\isadigit{0}}{\isadigit{0}}{\isacharbrackright}\ {\isadigit{9}}{\isadigit{9}}{\isadigit{9}}{\isacharparenright}\isanewline
\ \ \ \ \ \ \isakeyword{assumes}\ invl{\isacharcolon}\ {\isachardoublequoteopen}x{\isasymdiv}\ {\isasymotimes}\ x\ {\isacharequal}\ {\isasymone}{\isachardoublequoteclose}\isanewline
\isanewline
-\ \ \ \ \isacommand{instance}\isamarkupfalse%
+\ \ \ \ \isacommand{instantiation}\isamarkupfalse%
\ int\ {\isacharcolon}{\isacharcolon}\ group\isanewline
-\ \ \ \ \ \ inverse{\isacharunderscore}int{\isacharunderscore}def{\isacharcolon}\ {\isachardoublequoteopen}i{\isasymdiv}\ {\isasymequiv}\ {\isacharminus}\ i{\isachardoublequoteclose}\isanewline
+\ \ \ \ \isakeyword{begin}\isanewline
+\isanewline
+\ \ \ \ \isacommand{definition}\isamarkupfalse%
+\isanewline
+\ \ \ \ \ \ inverse{\isacharunderscore}int{\isacharunderscore}def{\isacharcolon}\ {\isachardoublequoteopen}i{\isasymdiv}\ {\isacharequal}\ {\isacharminus}\ {\isacharparenleft}i{\isasymColon}int{\isacharparenright}{\isachardoublequoteclose}\isanewline
+\isanewline
+\ \ \ \ \isacommand{instance}\isamarkupfalse%
%
\isadelimproof
-\ \ \ \ %
+\ %
\endisadelimproof
%
\isatagproof
@@ -523,6 +559,9 @@
\isadelimproof
%
\endisadelimproof
+\isanewline
+\isanewline
+\ \ \ \ \isacommand{end}\isamarkupfalse%
%
\isamarkupsection{Type classes as locales%
}
@@ -584,7 +623,7 @@
\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
+\ \ idem\ {\isacharbrackleft}{\isachardoublequoteopen}f\ {\isasymColon}\ {\isacharparenleft}{\isasymalpha}{\isasymColon}idem{\isacharparenright}\ {\isasymRightarrow}\ {\isasymalpha}{\isachardoublequoteclose}{\isacharbrackright}\isanewline
%
\isadelimproof
%
@@ -758,7 +797,7 @@
\isamarkuptrue%
\ \ \ \ \isacommand{fun}\isamarkupfalse%
\isanewline
-\ \ \ \ \ \ replicate\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}nat\ {\isasymRightarrow}\ {\isacharprime}a\ list\ {\isasymRightarrow}\ {\isacharprime}a\ list{\isachardoublequoteclose}\isanewline
+\ \ \ \ \ \ replicate\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}nat\ {\isasymRightarrow}\ {\isasymalpha}\ list\ {\isasymRightarrow}\ {\isasymalpha}\ list{\isachardoublequoteclose}\isanewline
\ \ \ \ \isakeyword{where}\isanewline
\ \ \ \ \ \ {\isachardoublequoteopen}replicate\ {\isadigit{0}}\ {\isacharunderscore}\ {\isacharequal}\ {\isacharbrackleft}{\isacharbrackright}{\isachardoublequoteclose}\isanewline
\ \ \ \ \ \ {\isacharbar}\ {\isachardoublequoteopen}replicate\ {\isacharparenleft}Suc\ n{\isacharparenright}\ xs\ {\isacharequal}\ xs\ {\isacharat}\ replicate\ n\ xs{\isachardoublequoteclose}\isanewline
@@ -897,8 +936,9 @@
\begin{isamarkuptext}%
Turning back to the first motivation for type classes,
namely overloading, it is obvious that overloading
- stemming from \isa{{\isasymCLASS}} and \isa{{\isasymINSTANCE}}
- statements naturally maps to Haskell type classes.
+ stemming from \isa{{\isasymCLASS}} statements and
+ \isa{{\isasymINSTANTIATION}}
+ targets naturally maps to Haskell type classes.
The code generator framework \cite{isabelle-codegen}
takes this into account. Concerning target languages
lacking type classes (e.g.~SML), type classes
--- a/doc-src/IsarAdvanced/Classes/classes.tex Wed Dec 05 04:34:15 2007 +0100
+++ b/doc-src/IsarAdvanced/Classes/classes.tex Wed Dec 05 14:15:39 2007 +0100
@@ -28,6 +28,7 @@
\newcommand{\isasymSHOWS}{\cmd{shows}}
\newcommand{\isasymCLASS}{\cmd{class}}
\newcommand{\isasymINSTANCE}{\cmd{instance}}
+\newcommand{\isasymINSTANTIATION}{\cmd{instantiation}}
\newcommand{\isasymLEMMA}{\cmd{lemma}}
\newcommand{\isasymPROOF}{\cmd{proof}}
\newcommand{\isasymQED}{\cmd{qed}}
--- a/doc-src/IsarAdvanced/Codegen/Thy/Codegen.thy Wed Dec 05 04:34:15 2007 +0100
+++ b/doc-src/IsarAdvanced/Codegen/Thy/Codegen.thy Wed Dec 05 14:15:39 2007 +0100
@@ -372,17 +372,24 @@
| "head (x#xs) = x"
text {*
- We provide some instances for our @{text null}:
+ \noindent We provide some instances for our @{text null}:
*}
-instance option :: (type) null
- "null \<equiv> None" ..
+instantiation option and list :: (type) null
+begin
+
+definition
+ "null = None"
-instance list :: (type) null
- "null \<equiv> []" ..
+definition
+ "null = []"
+
+instance ..
+
+end
text {*
- Constructing a dummy example:
+ \noindent Constructing a dummy example:
*}
definition
--- a/doc-src/IsarAdvanced/Codegen/Thy/document/Codegen.tex Wed Dec 05 04:34:15 2007 +0100
+++ b/doc-src/IsarAdvanced/Codegen/Thy/document/Codegen.tex Wed Dec 05 14:15:39 2007 +0100
@@ -464,9 +464,20 @@
We provide some instances for our \isa{null}:%
\end{isamarkuptext}%
\isamarkuptrue%
+\isacommand{instantiation}\isamarkupfalse%
+\ option\ \isakeyword{and}\ list\ {\isacharcolon}{\isacharcolon}\ {\isacharparenleft}type{\isacharparenright}\ null\isanewline
+\isakeyword{begin}\isanewline
+\isanewline
+\isacommand{definition}\isamarkupfalse%
+\isanewline
+\ \ {\isachardoublequoteopen}null\ {\isacharequal}\ None{\isachardoublequoteclose}\isanewline
+\isanewline
+\isacommand{definition}\isamarkupfalse%
+\isanewline
+\ \ {\isachardoublequoteopen}null\ {\isasymequiv}\ {\isacharbrackleft}{\isacharbrackright}{\isachardoublequoteclose}\isanewline
+\isanewline
\isacommand{instance}\isamarkupfalse%
-\ option\ {\isacharcolon}{\isacharcolon}\ {\isacharparenleft}type{\isacharparenright}\ null\isanewline
-\ \ {\isachardoublequoteopen}null\ {\isasymequiv}\ None{\isachardoublequoteclose}%
+%
\isadelimproof
\ %
\endisadelimproof
@@ -482,22 +493,7 @@
\endisadelimproof
\isanewline
\isanewline
-\isacommand{instance}\isamarkupfalse%
-\ list\ {\isacharcolon}{\isacharcolon}\ {\isacharparenleft}type{\isacharparenright}\ null\isanewline
-\ \ {\isachardoublequoteopen}null\ {\isasymequiv}\ {\isacharbrackleft}{\isacharbrackright}{\isachardoublequoteclose}%
-\isadelimproof
-\ %
-\endisadelimproof
-%
-\isatagproof
-\isacommand{{\isachardot}{\isachardot}}\isamarkupfalse%
-%
-\endisatagproof
-{\isafoldproof}%
-%
-\isadelimproof
-%
-\endisadelimproof
+\isacommand{end}\isamarkupfalse%
%
\begin{isamarkuptext}%
Constructing a dummy example:%
--- a/doc-src/isar.sty Wed Dec 05 04:34:15 2007 +0100
+++ b/doc-src/isar.sty Wed Dec 05 14:15:39 2007 +0100
@@ -78,6 +78,7 @@
\newcommand{\DEFS}{\isarkeyword{defs}}
\newcommand{\AXCLASS}{\isarkeyword{axclass}}
\newcommand{\INSTANCE}{\isarkeyword{instance}}
+\newcommand{\INSTANTIATION}{\isarkeyword{instantiation}}
\newcommand{\DECLARE}{\isarkeyword{declare}}
\newcommand{\LEMMAS}{\isarkeyword{lemmas}}
\newcommand{\THEOREMS}{\isarkeyword{theorems}}