author haftmann Wed, 31 Oct 2007 10:10:50 +0100 changeset 25247 7bacd1798fc4 parent 25246 584d8f2e1fc9 child 25248 cc5cf5f1178b
tuned
--- a/doc-src/IsarAdvanced/Classes/Thy/Classes.thy	Tue Oct 30 17:58:03 2007 +0100
+++ b/doc-src/IsarAdvanced/Classes/Thy/Classes.thy	Wed Oct 31 10:10:50 2007 +0100
@@ -151,7 +151,8 @@
mult_int_def: "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 .
+      then show "(i \<otimes> j) \<otimes> k = i \<otimes> (j \<otimes> k)"
+	unfolding mult_int_def .
qed

text {*
@@ -172,27 +173,41 @@
mult_nat_def: "m \<otimes> n \<equiv> m + n"
proof
fix m n q :: nat
-      show "m \<otimes> n \<otimes> q = m \<otimes> (n \<otimes> q)" unfolding mult_nat_def by simp
-    qed
-
-text {*
-  \noindent Also @{text "list"}s form a semigroup with @{const "op @"} as
-  parameter:
-*}
-
-    instance list :: (type) semigroup
-      mult_list_def: "xs \<otimes> ys \<equiv> xs @ ys"
-    proof
-      fix xs ys zs :: "\<alpha> list"
-      show "xs \<otimes> ys \<otimes> zs = xs \<otimes> (ys \<otimes> zs)"
-      proof -
-        from mult_list_def have "\<And>xs ys\<Colon>\<alpha> list. xs \<otimes> ys \<equiv> xs @ ys" .
-        thus ?thesis by simp
-      qed
+      show "m \<otimes> n \<otimes> q = m \<otimes> (n \<otimes> q)"
+	unfolding mult_nat_def by simp
qed

-subsection {* Subclasses *}
+subsection {* Lifting and parametric types *}
+
+text {*
+  Overloaded definitions giving on class instantiation
+  may include recursion over the syntactic structure of types.
+  As a canonical example, we model product semigroups
+  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"
+      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
+
+text {*
+  \noindent Associativity from product semigroups is
+  established using
+  the definition of @{text \<otimes>} on products and the hypothetical
+  associativety of the type components;  these hypothesis
+  are facts due to the @{text semigroup} constraints imposed
+  on the type components by the @{text instance} proposition.
+  Indeed, this pattern often occurs with parametric types
+  and type classes.
+*}
+
+
+subsection {* Subclassing *}

text {*
We define a subclass @{text "monoidl"} (a semigroup with a left-hand neutral)
@@ -206,36 +221,34 @@
assumes neutl: "\<one> \<otimes> x = x"

text {*
-  \noindent Again, we make some instances, by
+  \noindent Again, we prove some instances, by
providing suitable parameter definitions and proofs for the
*}

instance nat :: monoidl
neutral_nat_def: "\<one> \<equiv> 0"
proof
fix n :: nat
-      show "\<one> \<otimes> n = n" unfolding neutral_nat_def mult_nat_def by simp
+      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
fix k :: int
-      show "\<one> \<otimes> k = k" unfolding neutral_int_def mult_int_def by simp
+      show "\<one> \<otimes> k = k"
+	unfolding neutral_int_def mult_int_def by simp
qed

-    instance list :: (type) monoidl
-      neutral_list_def: "\<one> \<equiv> []"
+    instance * :: (monoidl, monoidl) monoidl
+      neutral_prod_def: "\<one> \<equiv> (\<one>, \<one>)"
proof
-      fix xs :: "\<alpha> list"
-      show "\<one> \<otimes> xs = xs"
-      proof -
-	from mult_list_def have "\<And>xs ys\<Colon>\<alpha> list. xs \<otimes> ys \<equiv> xs @ ys" .
-	moreover from mult_list_def neutral_list_def have "\<one> \<equiv> []\<Colon>\<alpha> list" by simp
-	ultimately show ?thesis by simp
-      qed
-    qed
+      fix p :: "'a\<Colon>monoidl \<times> 'b\<Colon>monoidl"
+      show "\<one> \<otimes> p = p"
+	unfolding neutral_prod_def mult_prod_def by (simp add: neutl)
+    qed

text {*
\noindent Fully-fledged monoids are modelled by another subclass
@@ -245,26 +258,25 @@
class monoid = monoidl +
assumes neutr: "x \<otimes> \<one> = x"

-text {*
-  \noindent Instantiations may also be given simultaneously for different
-  type constructors:
-*}
-
-    instance nat :: monoid and int :: monoid and list :: (type) monoid
+    instance nat :: monoid
proof
fix n :: nat
-      show "n \<otimes> \<one> = n" unfolding neutral_nat_def mult_nat_def by simp
-    next
+      show "n \<otimes> \<one> = n"
+	unfolding neutral_nat_def mult_nat_def by simp
+    qed
+
+    instance int :: monoid
+    proof
fix k :: int
-      show "k \<otimes> \<one> = k" unfolding neutral_int_def mult_int_def by simp
-    next
-      fix xs :: "\<alpha> list"
-      show "xs \<otimes> \<one> = xs"
-      proof -
-	from mult_list_def have "\<And>xs ys\<Colon>\<alpha> list. xs \<otimes> ys \<equiv> xs @ ys" .
-	moreover from mult_list_def neutral_list_def have "\<one> \<equiv> []\<Colon>\<alpha> list" by simp
-	ultimately show ?thesis by simp
-      qed
+      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"
+      show "p \<otimes> \<one> = p"
+	unfolding neutral_prod_def mult_prod_def by (simp add: neutr)
qed

text {*
@@ -282,7 +294,7 @@
fix i :: int
have "-i + i = 0" by simp
then show "i\<div> \<otimes> i = \<one>"
-      unfolding mult_int_def and neutral_int_def and inverse_int_def .
+	unfolding mult_int_def neutral_int_def inverse_int_def .
qed

section {* Type classes as locales *}
@@ -338,17 +350,17 @@
Isabelle locales enable reasoning at a general level, while results
are implicitly transferred to all instances.  For example, we can
now establish the @{text "left_cancel"} lemma for groups, which
-  states that the function @{text "(x \<circ>)"} is injective:
+  states that the function @{text "(x \<otimes>)"} is injective:
*}

lemma (in group) left_cancel: "x \<otimes> y = x \<otimes> z \<longleftrightarrow> y = z"
proof
-    assume "x \<otimes> y = x \<otimes> z"
+      assume "x \<otimes> y = x \<otimes> z"
then have "x\<div> \<otimes> (x \<otimes> y) = x\<div> \<otimes> (x \<otimes> z)" by simp
then have "(x\<div> \<otimes> x) \<otimes> y = (x\<div> \<otimes> x) \<otimes> z" using assoc by simp
then show "y = z" using neutl and invl by simp
next
-    assume "y = z"
+      assume "y = z"
then show "x \<otimes> y = x \<otimes> z" by simp
qed

@@ -389,11 +401,56 @@
*}

+subsection {* A functor analogy *}
+
+text {*
+  We introduced Isar classes by analogy to type classes
+  functional programming;  if we reconsider this in the
+  context of what has been said about type classes and locales,
+  we can drive this analogy further by stating that type
+  classes essentially correspond to functors which have
+  a canonical interpretation as type classes.
+  Anyway, there is also the possibility of other interpretations.
+  For example, also @{text "list"}s form a monoid with
+  @{const "op @"} and @{const "[]"} as operations, but it
+  seems inappropriate to apply to lists
+  the same operations as for genuinly algebraic types.
+  In such a case, we simply can do a particular interpretation
+  of monoids for lists:
+*}
+
+    interpretation list_monoid: monoid ["op @" "[]"]
+      by unfold_locales auto
+
+text {*
+  \noindent This enables us to apply facts on monoids
+  to lists, e.g. @{thm list_monoid.neutl [no_vars]}.
+
+  When using this interpretation pattern, it may also
+  be appropriate to map derived definitions accordingly:
+*}
+
+    fun
+      replicate :: "nat \<Rightarrow> 'a list \<Rightarrow> 'a list"
+    where
+      "replicate 0 _ = []"
+      | "replicate (Suc n) xs = xs @ replicate n xs"
+
+    interpretation list_monoid: monoid ["op @" "[]"] where
+      "monoid.pow_nat (op @) [] = replicate"
+    proof
+      fix n :: nat
+      show "monoid.pow_nat (op @) [] n = replicate n"
+	by (induct n) auto
+    qed
+
+
subsection {* Additional subclass relations *}

text {*
Any @{text "group"} is also a @{text "monoid"};  this
+  subclass relation,
together with a proof of the logical difference:
*}

@@ -411,7 +468,41 @@
method which only leaves the logical differences still
open to proof to the user.  Afterwards it is propagated
to the type system, making @{text group} an instance of
-  @{text monoid}.  For illustration, a derived definition
+  to the graph of subclass relations
+  (cf.\ \figref{fig:subclass}).
+
+  \begin{figure}[htbp]
+   \begin{center}
+     \small
+     \unitlength 0.6mm
+     \begin{picture}(40,60)(0,0)
+       \put(20,60){\makebox(0,0){@{text semigroup}}}
+       \put(20,40){\makebox(0,0){@{text monoidl}}}
+       \put(00,20){\makebox(0,0){@{text monoid}}}
+       \put(40,00){\makebox(0,0){@{text group}}}
+       \put(20,55){\vector(0,-1){10}}
+       \put(15,35){\vector(-1,-1){10}}
+       \put(25,35){\vector(1,-3){10}}
+     \end{picture}
+     \hspace{8em}
+     \begin{picture}(40,60)(0,0)
+       \put(20,60){\makebox(0,0){@{text semigroup}}}
+       \put(20,40){\makebox(0,0){@{text monoidl}}}
+       \put(00,20){\makebox(0,0){@{text monoid}}}
+       \put(40,00){\makebox(0,0){@{text group}}}
+       \put(20,55){\vector(0,-1){10}}
+       \put(15,35){\vector(-1,-1){10}}
+       \put(05,15){\vector(3,-1){30}}
+     \end{picture}
+     \caption{Subclass relationship of monoids and groups:
+        before and after establishing the relationship
+        @{text "group \<subseteq> monoid"};  transitive edges left out.}
+     \label{fig:subclass}
+   \end{center}
+  \end{figure}
+
+  For illustration, a derived definition
in @{text group} which uses @{text pow_nat}:
*}

@@ -422,15 +513,13 @@
else (pow_nat (nat (- k)) x)\<div>)"

text {*
-  \noindent   yields the global definition of
+  \noindent yields the global definition of
@{term [source] "pow_int \<Colon> int \<Rightarrow> \<alpha>\<Colon>group \<Rightarrow> \<alpha>\<Colon>group"}
with the corresponding theorem @{thm pow_int_def [no_vars]}.
*}

-section {* Further issues *}
-
-subsection {* Code generation *}
+section {* Type classes and code generation *}

text {*
Turning back to the first motivation for type classes,
--- a/doc-src/IsarAdvanced/Classes/Thy/document/Classes.tex	Tue Oct 30 17:58:03 2007 +0100
+++ b/doc-src/IsarAdvanced/Classes/Thy/document/Classes.tex	Wed Oct 31 10:10:50 2007 +0100
@@ -186,7 +186,8 @@
\ simp\isanewline
\ \ \ \ \ \ \isacommand{then}\isamarkupfalse%
\ \isacommand{show}\isamarkupfalse%
-\ {\isachardoublequoteopen}{\isacharparenleft}i\ {\isasymotimes}\ j{\isacharparenright}\ {\isasymotimes}\ k\ {\isacharequal}\ i\ {\isasymotimes}\ {\isacharparenleft}j\ {\isasymotimes}\ k{\isacharparenright}{\isachardoublequoteclose}\ \isacommand{unfolding}\isamarkupfalse%
+\ {\isachardoublequoteopen}{\isacharparenleft}i\ {\isasymotimes}\ j{\isacharparenright}\ {\isasymotimes}\ k\ {\isacharequal}\ i\ {\isasymotimes}\ {\isacharparenleft}j\ {\isasymotimes}\ k{\isacharparenright}{\isachardoublequoteclose}\isanewline
+\ \ \ \ \ \ \ \ \isacommand{unfolding}\isamarkupfalse%
\ mult{\isacharunderscore}int{\isacharunderscore}def\ \isacommand{{\isachardot}}\isamarkupfalse%
\isanewline
\ \ \ \ \isacommand{qed}\isamarkupfalse%
@@ -226,7 +227,8 @@
\ \ \ \ \ \ \isacommand{fix}\isamarkupfalse%
\ m\ n\ q\ {\isacharcolon}{\isacharcolon}\ nat\ \isanewline
\ \ \ \ \ \ \isacommand{show}\isamarkupfalse%
-\ {\isachardoublequoteopen}m\ {\isasymotimes}\ n\ {\isasymotimes}\ q\ {\isacharequal}\ m\ {\isasymotimes}\ {\isacharparenleft}n\ {\isasymotimes}\ q{\isacharparenright}{\isachardoublequoteclose}\ \isacommand{unfolding}\isamarkupfalse%
+\ {\isachardoublequoteopen}m\ {\isasymotimes}\ n\ {\isasymotimes}\ q\ {\isacharequal}\ m\ {\isasymotimes}\ {\isacharparenleft}n\ {\isasymotimes}\ q{\isacharparenright}{\isachardoublequoteclose}\isanewline
+\ \ \ \ \ \ \ \ \isacommand{unfolding}\isamarkupfalse%
\ mult{\isacharunderscore}nat{\isacharunderscore}def\ \isacommand{by}\isamarkupfalse%
\ simp\isanewline
\ \ \ \ \isacommand{qed}\isamarkupfalse%
@@ -238,14 +240,20 @@
%
%
+\isamarkupsubsection{Lifting and parametric types%
+}
+\isamarkuptrue%
+%
\begin{isamarkuptext}%
-\noindent Also \isa{list}s form a semigroup with \isa{op\ {\isacharat}} as
-  parameter:%
+Overloaded definitions giving on class instantiation
+  may include recursion over the syntactic structure of types.
+  As a canonical example, we model product semigroups
+  using our simple algebra:%
\end{isamarkuptext}%
\isamarkuptrue%
\ \ \ \ \isacommand{instance}\isamarkupfalse%
-\ list\ {\isacharcolon}{\isacharcolon}\ {\isacharparenleft}type{\isacharparenright}\ semigroup\isanewline
-\ \ \ \ \ \ mult{\isacharunderscore}list{\isacharunderscore}def{\isacharcolon}\ {\isachardoublequoteopen}xs\ {\isasymotimes}\ ys\ {\isasymequiv}\ xs\ {\isacharat}\ ys{\isachardoublequoteclose}\isanewline
+\ {\isacharasterisk}\ {\isacharcolon}{\isacharcolon}\ {\isacharparenleft}semigroup{\isacharcomma}\ semigroup{\isacharparenright}\ semigroup\isanewline
%
\ \ \ \ %
@@ -255,20 +263,12 @@
\isacommand{proof}\isamarkupfalse%
\isanewline
\ \ \ \ \ \ \isacommand{fix}\isamarkupfalse%
-\ xs\ ys\ zs\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}{\isasymalpha}\ list{\isachardoublequoteclose}\isanewline
\ \ \ \ \ \ \isacommand{show}\isamarkupfalse%
-\ {\isachardoublequoteopen}xs\ {\isasymotimes}\ ys\ {\isasymotimes}\ zs\ {\isacharequal}\ xs\ {\isasymotimes}\ {\isacharparenleft}ys\ {\isasymotimes}\ zs{\isacharparenright}{\isachardoublequoteclose}\isanewline
-\ \ \ \ \ \ \isacommand{proof}\isamarkupfalse%
-\ {\isacharminus}\isanewline
-\ \ \ \ \ \ \ \ \isacommand{from}\isamarkupfalse%
-\ mult{\isacharunderscore}list{\isacharunderscore}def\ \isacommand{have}\isamarkupfalse%
-\ {\isachardoublequoteopen}{\isasymAnd}xs\ ys{\isasymColon}{\isasymalpha}\ list{\isachardot}\ xs\ {\isasymotimes}\ ys\ {\isasymequiv}\ xs\ {\isacharat}\ ys{\isachardoublequoteclose}\ \isacommand{{\isachardot}}\isamarkupfalse%
-\isanewline
-\ \ \ \ \ \ \ \ \isacommand{thus}\isamarkupfalse%
-\ {\isacharquery}thesis\ \isacommand{by}\isamarkupfalse%
-\ simp\isanewline
-\ \ \ \ \ \ \isacommand{qed}\isamarkupfalse%
-\isanewline
+\ \ \ \ \ \ \ \ \isacommand{unfolding}\isamarkupfalse%
+\ mult{\isacharunderscore}prod{\isacharunderscore}def\ \isacommand{by}\isamarkupfalse%
\ \ \ \ \isacommand{qed}\isamarkupfalse%
%
\endisatagproof
@@ -278,7 +278,19 @@
%
%
-\isamarkupsubsection{Subclasses%
+\begin{isamarkuptext}%
+\noindent Associativity from product semigroups is
+  established using
+  the definition of \isa{{\isasymotimes}} on products and the hypothetical
+  associativety of the type components;  these hypothesis
+  are facts due to the \isa{semigroup} constraints imposed
+  on the type components by the \isa{instance} proposition.
+  Indeed, this pattern often occurs with parametric types
+  and type classes.%
+\end{isamarkuptext}%
+\isamarkuptrue%
+%
+\isamarkupsubsection{Subclassing%
}
\isamarkuptrue%
%
@@ -294,9 +306,9 @@
\ \ \ \ \ \ \isakeyword{fixes}\ neutral\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}{\isasymalpha}{\isachardoublequoteclose}\ {\isacharparenleft}{\isachardoublequoteopen}{\isasymone}{\isachardoublequoteclose}{\isacharparenright}\isanewline
\ \ \ \ \ \ \isakeyword{assumes}\ neutl{\isacharcolon}\ {\isachardoublequoteopen}{\isasymone}\ {\isasymotimes}\ x\ {\isacharequal}\ x{\isachardoublequoteclose}%
\begin{isamarkuptext}%
-\noindent Again, we make some instances, by
+\noindent Again, we prove some instances, by
providing suitable parameter definitions and proofs for the
\end{isamarkuptext}%
\isamarkuptrue%
\ \ \ \ \isacommand{instance}\isamarkupfalse%
@@ -313,7 +325,8 @@
\ \ \ \ \ \ \isacommand{fix}\isamarkupfalse%
\ n\ {\isacharcolon}{\isacharcolon}\ nat\isanewline
\ \ \ \ \ \ \isacommand{show}\isamarkupfalse%
-\ {\isachardoublequoteopen}{\isasymone}\ {\isasymotimes}\ n\ {\isacharequal}\ n{\isachardoublequoteclose}\ \isacommand{unfolding}\isamarkupfalse%
+\ {\isachardoublequoteopen}{\isasymone}\ {\isasymotimes}\ n\ {\isacharequal}\ n{\isachardoublequoteclose}\isanewline
+\ \ \ \ \ \ \ \ \isacommand{unfolding}\isamarkupfalse%
\ neutral{\isacharunderscore}nat{\isacharunderscore}def\ mult{\isacharunderscore}nat{\isacharunderscore}def\ \isacommand{by}\isamarkupfalse%
\ simp\isanewline
\ \ \ \ \isacommand{qed}\isamarkupfalse%
@@ -340,7 +353,8 @@
\ \ \ \ \ \ \isacommand{fix}\isamarkupfalse%
\ k\ {\isacharcolon}{\isacharcolon}\ int\isanewline
\ \ \ \ \ \ \isacommand{show}\isamarkupfalse%
-\ {\isachardoublequoteopen}{\isasymone}\ {\isasymotimes}\ k\ {\isacharequal}\ k{\isachardoublequoteclose}\ \isacommand{unfolding}\isamarkupfalse%
+\ {\isachardoublequoteopen}{\isasymone}\ {\isasymotimes}\ k\ {\isacharequal}\ k{\isachardoublequoteclose}\isanewline
+\ \ \ \ \ \ \ \ \isacommand{unfolding}\isamarkupfalse%
\ neutral{\isacharunderscore}int{\isacharunderscore}def\ mult{\isacharunderscore}int{\isacharunderscore}def\ \isacommand{by}\isamarkupfalse%
\ simp\isanewline
\ \ \ \ \isacommand{qed}\isamarkupfalse%
@@ -354,8 +368,8 @@
\isanewline
\ \ \ \ \isacommand{instance}\isamarkupfalse%
-\ list\ {\isacharcolon}{\isacharcolon}\ {\isacharparenleft}type{\isacharparenright}\ monoidl\isanewline
-\ \ \ \ \ \ neutral{\isacharunderscore}list{\isacharunderscore}def{\isacharcolon}\ {\isachardoublequoteopen}{\isasymone}\ {\isasymequiv}\ {\isacharbrackleft}{\isacharbrackright}{\isachardoublequoteclose}\isanewline
+\ {\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
%
\ \ \ \ %
@@ -365,26 +379,12 @@
\isacommand{proof}\isamarkupfalse%
\isanewline
\ \ \ \ \ \ \isacommand{fix}\isamarkupfalse%
-\ xs\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}{\isasymalpha}\ list{\isachardoublequoteclose}\isanewline
+\ p\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}{\isacharprime}a{\isasymColon}monoidl\ {\isasymtimes}\ {\isacharprime}b{\isasymColon}monoidl{\isachardoublequoteclose}\isanewline
\ \ \ \ \ \ \isacommand{show}\isamarkupfalse%
-\ {\isachardoublequoteopen}{\isasymone}\ {\isasymotimes}\ xs\ {\isacharequal}\ xs{\isachardoublequoteclose}\isanewline
-\ \ \ \ \ \ \isacommand{proof}\isamarkupfalse%
-\ {\isacharminus}\isanewline
-\ \ \ \ \ \ \ \ \isacommand{from}\isamarkupfalse%
-\ mult{\isacharunderscore}list{\isacharunderscore}def\ \isacommand{have}\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%
-\ mult{\isacharunderscore}list{\isacharunderscore}def\ neutral{\isacharunderscore}list{\isacharunderscore}def\ \isacommand{have}\isamarkupfalse%
-\ {\isachardoublequoteopen}{\isasymone}\ {\isasymequiv}\ {\isacharbrackleft}{\isacharbrackright}{\isasymColon}{\isasymalpha}\ list{\isachardoublequoteclose}\ \isacommand{by}\isamarkupfalse%
-\ simp\isanewline
-\ \ \ \ \ \ \ \ \isacommand{ultimately}\isamarkupfalse%
-\ \isacommand{show}\isamarkupfalse%
-\ {\isacharquery}thesis\ \isacommand{by}\isamarkupfalse%
-\ simp\isanewline
-\ \ \ \ \ \ \isacommand{qed}\isamarkupfalse%
-\isanewline
+\ {\isachardoublequoteopen}{\isasymone}\ {\isasymotimes}\ p\ {\isacharequal}\ p{\isachardoublequoteclose}\isanewline
+\ \ \ \ \ \ \ \ \isacommand{unfolding}\isamarkupfalse%
+\ neutral{\isacharunderscore}prod{\isacharunderscore}def\ mult{\isacharunderscore}prod{\isacharunderscore}def\ \isacommand{by}\isamarkupfalse%
\ \ \ \ \isacommand{qed}\isamarkupfalse%
%
\endisatagproof
@@ -401,14 +401,10 @@
\isamarkuptrue%
\ \ \ \ \isacommand{class}\isamarkupfalse%
\ monoid\ {\isacharequal}\ monoidl\ {\isacharplus}\isanewline
-\ \ \ \ \ \ \isakeyword{assumes}\ neutr{\isacharcolon}\ {\isachardoublequoteopen}x\ {\isasymotimes}\ {\isasymone}\ {\isacharequal}\ x{\isachardoublequoteclose}%
-\begin{isamarkuptext}%
-\noindent Instantiations may also be given simultaneously for different
-  type constructors:%
-\end{isamarkuptext}%
-\isamarkuptrue%
+\ \ \ \ \ \ \isakeyword{assumes}\ neutr{\isacharcolon}\ {\isachardoublequoteopen}x\ {\isasymotimes}\ {\isasymone}\ {\isacharequal}\ x{\isachardoublequoteclose}\isanewline
+\isanewline
\ \ \ \ \isacommand{instance}\isamarkupfalse%
-\ nat\ {\isacharcolon}{\isacharcolon}\ monoid\ \isakeyword{and}\ int\ {\isacharcolon}{\isacharcolon}\ monoid\ \isakeyword{and}\ list\ {\isacharcolon}{\isacharcolon}\ {\isacharparenleft}type{\isacharparenright}\ monoid\isanewline
+\ nat\ {\isacharcolon}{\isacharcolon}\ monoid\ \isanewline
%
\ \ \ \ %
@@ -420,40 +416,64 @@
\ \ \ \ \ \ \isacommand{fix}\isamarkupfalse%
\ n\ {\isacharcolon}{\isacharcolon}\ nat\isanewline
\ \ \ \ \ \ \isacommand{show}\isamarkupfalse%
-\ {\isachardoublequoteopen}n\ {\isasymotimes}\ {\isasymone}\ {\isacharequal}\ n{\isachardoublequoteclose}\ \isacommand{unfolding}\isamarkupfalse%
+\ {\isachardoublequoteopen}n\ {\isasymotimes}\ {\isasymone}\ {\isacharequal}\ n{\isachardoublequoteclose}\isanewline
+\ \ \ \ \ \ \ \ \isacommand{unfolding}\isamarkupfalse%
\ neutral{\isacharunderscore}nat{\isacharunderscore}def\ mult{\isacharunderscore}nat{\isacharunderscore}def\ \isacommand{by}\isamarkupfalse%
\ simp\isanewline
-\ \ \ \ \isacommand{next}\isamarkupfalse%
+\ \ \ \ \isacommand{qed}\isamarkupfalse%
+%
+\endisatagproof
+{\isafoldproof}%
+%
+\isanewline
+%
+\isanewline
+\ \ \ \ \isacommand{instance}\isamarkupfalse%
+\ int\ {\isacharcolon}{\isacharcolon}\ monoid\isanewline
+%
+\ \ \ \ %
+%
+\isatagproof
+\isacommand{proof}\isamarkupfalse%
\isanewline
\ \ \ \ \ \ \isacommand{fix}\isamarkupfalse%
\ k\ {\isacharcolon}{\isacharcolon}\ int\isanewline
\ \ \ \ \ \ \isacommand{show}\isamarkupfalse%
-\ {\isachardoublequoteopen}k\ {\isasymotimes}\ {\isasymone}\ {\isacharequal}\ k{\isachardoublequoteclose}\ \isacommand{unfolding}\isamarkupfalse%
+\ {\isachardoublequoteopen}k\ {\isasymotimes}\ {\isasymone}\ {\isacharequal}\ k{\isachardoublequoteclose}\isanewline
+\ \ \ \ \ \ \ \ \isacommand{unfolding}\isamarkupfalse%
\ neutral{\isacharunderscore}int{\isacharunderscore}def\ mult{\isacharunderscore}int{\isacharunderscore}def\ \isacommand{by}\isamarkupfalse%
\ simp\isanewline
-\ \ \ \ \isacommand{next}\isamarkupfalse%
+\ \ \ \ \isacommand{qed}\isamarkupfalse%
+%
+\endisatagproof
+{\isafoldproof}%
+%
\isanewline
-\ \ \ \ \ \ \isacommand{fix}\isamarkupfalse%
-\ xs\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}{\isasymalpha}\ list{\isachardoublequoteclose}\isanewline
-\ \ \ \ \ \ \isacommand{show}\isamarkupfalse%
-\ {\isachardoublequoteopen}xs\ {\isasymotimes}\ {\isasymone}\ {\isacharequal}\ xs{\isachardoublequoteclose}\isanewline
-\ \ \ \ \ \ \isacommand{proof}\isamarkupfalse%
-\ {\isacharminus}\isanewline
-\ \ \ \ \ \ \ \ \isacommand{from}\isamarkupfalse%
-\ mult{\isacharunderscore}list{\isacharunderscore}def\ \isacommand{have}\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%
-\ mult{\isacharunderscore}list{\isacharunderscore}def\ neutral{\isacharunderscore}list{\isacharunderscore}def\ \isacommand{have}\isamarkupfalse%
-\ {\isachardoublequoteopen}{\isasymone}\ {\isasymequiv}\ {\isacharbrackleft}{\isacharbrackright}{\isasymColon}{\isasymalpha}\ list{\isachardoublequoteclose}\ \isacommand{by}\isamarkupfalse%
-\ simp\isanewline
-\ \ \ \ \ \ \ \ \isacommand{ultimately}\isamarkupfalse%
-\ \isacommand{show}\isamarkupfalse%
-\ {\isacharquery}thesis\ \isacommand{by}\isamarkupfalse%
-\ simp\isanewline
-\ \ \ \ \ \ \isacommand{qed}\isamarkupfalse%
-\isanewline
+\ \ \ \ \isacommand{instance}\isamarkupfalse%
+\ {\isacharasterisk}\ {\isacharcolon}{\isacharcolon}\ {\isacharparenleft}monoid{\isacharcomma}\ monoid{\isacharparenright}\ monoid\isanewline
+%
+\ \ \ \ %
+%
+\isatagproof
+\isacommand{proof}\isamarkupfalse%
+\ \isanewline
+\ \ \ \ \ \ \isacommand{fix}\isamarkupfalse%
+\ p\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}{\isacharprime}a{\isasymColon}monoid\ {\isasymtimes}\ {\isacharprime}b{\isasymColon}monoid{\isachardoublequoteclose}\isanewline
+\ \ \ \ \ \ \isacommand{show}\isamarkupfalse%
+\ {\isachardoublequoteopen}p\ {\isasymotimes}\ {\isasymone}\ {\isacharequal}\ p{\isachardoublequoteclose}\isanewline
+\ \ \ \ \ \ \ \ \isacommand{unfolding}\isamarkupfalse%
+\ neutral{\isacharunderscore}prod{\isacharunderscore}def\ mult{\isacharunderscore}prod{\isacharunderscore}def\ \isacommand{by}\isamarkupfalse%
\ \ \ \ \isacommand{qed}\isamarkupfalse%
%
\endisatagproof
@@ -492,8 +512,8 @@
\ \ \ \ \ \ \isacommand{then}\isamarkupfalse%
\ \isacommand{show}\isamarkupfalse%
\ {\isachardoublequoteopen}i{\isasymdiv}\ {\isasymotimes}\ i\ {\isacharequal}\ {\isasymone}{\isachardoublequoteclose}\isanewline
-\ \ \ \ \ \ \isacommand{unfolding}\isamarkupfalse%
-\ mult{\isacharunderscore}int{\isacharunderscore}def\ \isakeyword{and}\ neutral{\isacharunderscore}int{\isacharunderscore}def\ \isakeyword{and}\ inverse{\isacharunderscore}int{\isacharunderscore}def\ \isacommand{{\isachardot}}\isamarkupfalse%
+\ \ \ \ \ \ \ \ \isacommand{unfolding}\isamarkupfalse%
+\ mult{\isacharunderscore}int{\isacharunderscore}def\ neutral{\isacharunderscore}int{\isacharunderscore}def\ inverse{\isacharunderscore}int{\isacharunderscore}def\ \isacommand{{\isachardot}}\isamarkupfalse%
\isanewline
\ \ \ \ \isacommand{qed}\isamarkupfalse%
%
@@ -608,7 +628,7 @@
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:%
+  states that the function \isa{{\isacharparenleft}x\ {\isasymotimes}{\isacharparenright}} is injective:%
\end{isamarkuptext}%
\isamarkuptrue%
\ \ \ \ \isacommand{lemma}\isamarkupfalse%
@@ -621,7 +641,7 @@
\isatagproof
\isacommand{proof}\isamarkupfalse%
\isanewline
-\ \ \ \ \isacommand{assume}\isamarkupfalse%
+\ \ \ \ \ \ \isacommand{assume}\isamarkupfalse%
\ {\isachardoublequoteopen}x\ {\isasymotimes}\ y\ {\isacharequal}\ x\ {\isasymotimes}\ z{\isachardoublequoteclose}\isanewline
\ \ \ \ \ \ \isacommand{then}\isamarkupfalse%
\ \isacommand{have}\isamarkupfalse%
@@ -639,7 +659,7 @@
\ simp\isanewline
\ \ \ \ \isacommand{next}\isamarkupfalse%
\isanewline
-\ \ \ \ \isacommand{assume}\isamarkupfalse%
+\ \ \ \ \ \ \isacommand{assume}\isamarkupfalse%
\ {\isachardoublequoteopen}y\ {\isacharequal}\ z{\isachardoublequoteclose}\isanewline
\ \ \ \ \ \ \isacommand{then}\isamarkupfalse%
\ \isacommand{show}\isamarkupfalse%
@@ -691,13 +711,92 @@
\end{isamarkuptext}%
\isamarkuptrue%
%
+\isamarkupsubsection{A functor analogy%
+}
+\isamarkuptrue%
+%
+\begin{isamarkuptext}%
+We introduced Isar classes by analogy to type classes
+  functional programming;  if we reconsider this in the
+  context of what has been said about type classes and locales,
+  we can drive this analogy further by stating that type
+  classes essentially correspond to functors which have
+  a canonical interpretation as type classes.
+  Anyway, there is also the possibility of other interpretations.
+  For example, also \isa{list}s form a monoid with
+  \isa{op\ {\isacharat}} and \isa{{\isacharbrackleft}{\isacharbrackright}} as operations, but it
+  seems inappropriate to apply to lists
+  the same operations as for genuinly algebraic types.
+  In such a case, we simply can do a particular interpretation
+  of monoids for lists:%
+\end{isamarkuptext}%
+\isamarkuptrue%
+\ \ \ \ \isacommand{interpretation}\isamarkupfalse%
+\ list{\isacharunderscore}monoid{\isacharcolon}\ monoid\ {\isacharbrackleft}{\isachardoublequoteopen}op\ {\isacharat}{\isachardoublequoteclose}\ {\isachardoublequoteopen}{\isacharbrackleft}{\isacharbrackright}{\isachardoublequoteclose}{\isacharbrackright}\isanewline
+%
+\ \ \ \ \ \ %
+%
+\isatagproof
+\isacommand{by}\isamarkupfalse%
+\ unfold{\isacharunderscore}locales\ auto%
+\endisatagproof
+{\isafoldproof}%
+%
+%
+%
+\begin{isamarkuptext}%
+\noindent This enables us to apply facts on monoids
+  to lists, e.g. \isa{{\isacharbrackleft}{\isacharbrackright}\ {\isacharat}\ x\ {\isacharequal}\ x}.
+
+  When using this interpretation pattern, it may also
+  be appropriate to map derived definitions accordingly:%
+\end{isamarkuptext}%
+\isamarkuptrue%
+\ \ \ \ \isacommand{fun}\isamarkupfalse%
+\isanewline
+\ \ \ \ \ \ replicate\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}nat\ {\isasymRightarrow}\ {\isacharprime}a\ list\ {\isasymRightarrow}\ {\isacharprime}a\ 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
+\isanewline
+\ \ \ \ \isacommand{interpretation}\isamarkupfalse%
+\ list{\isacharunderscore}monoid{\isacharcolon}\ monoid\ {\isacharbrackleft}{\isachardoublequoteopen}op\ {\isacharat}{\isachardoublequoteclose}\ {\isachardoublequoteopen}{\isacharbrackleft}{\isacharbrackright}{\isachardoublequoteclose}{\isacharbrackright}\ \isakeyword{where}\isanewline
+\ \ \ \ \ \ {\isachardoublequoteopen}monoid{\isachardot}pow{\isacharunderscore}nat\ {\isacharparenleft}op\ {\isacharat}{\isacharparenright}\ {\isacharbrackleft}{\isacharbrackright}\ {\isacharequal}\ replicate{\isachardoublequoteclose}\isanewline
+%
+\ \ \ \ %
+%
+\isatagproof
+\isacommand{proof}\isamarkupfalse%
+\isanewline
+\ \ \ \ \ \ \isacommand{fix}\isamarkupfalse%
+\ n\ {\isacharcolon}{\isacharcolon}\ nat\isanewline
+\ \ \ \ \ \ \isacommand{show}\isamarkupfalse%
+\ {\isachardoublequoteopen}monoid{\isachardot}pow{\isacharunderscore}nat\ {\isacharparenleft}op\ {\isacharat}{\isacharparenright}\ {\isacharbrackleft}{\isacharbrackright}\ n\ {\isacharequal}\ replicate\ n{\isachardoublequoteclose}\isanewline
+\ \ \ \ \ \ \ \ \isacommand{by}\isamarkupfalse%
+\ {\isacharparenleft}induct\ n{\isacharparenright}\ auto\isanewline
+\ \ \ \ \isacommand{qed}\isamarkupfalse%
+%
+\endisatagproof
+{\isafoldproof}%
+%
+%
+%
}
\isamarkuptrue%
%
\begin{isamarkuptext}%
Any \isa{group} is also a \isa{monoid};  this
+  subclass relation,
together with a proof of the logical difference:%
\end{isamarkuptext}%
\isamarkuptrue%
@@ -740,7 +839,41 @@
method which only leaves the logical differences still
open to proof to the user.  Afterwards it is propagated
to the type system, making \isa{group} an instance of
-  \isa{monoid}.  For illustration, a derived definition
+  to the graph of subclass relations
+  (cf.\ \figref{fig:subclass}).
+
+  \begin{figure}[htbp]
+   \begin{center}
+     \small
+     \unitlength 0.6mm
+     \begin{picture}(40,60)(0,0)
+       \put(20,60){\makebox(0,0){\isa{semigroup}}}
+       \put(20,40){\makebox(0,0){\isa{monoidl}}}
+       \put(00,20){\makebox(0,0){\isa{monoid}}}
+       \put(40,00){\makebox(0,0){\isa{group}}}
+       \put(20,55){\vector(0,-1){10}}
+       \put(15,35){\vector(-1,-1){10}}
+       \put(25,35){\vector(1,-3){10}}
+     \end{picture}
+     \hspace{8em}
+     \begin{picture}(40,60)(0,0)
+       \put(20,60){\makebox(0,0){\isa{semigroup}}}
+       \put(20,40){\makebox(0,0){\isa{monoidl}}}
+       \put(00,20){\makebox(0,0){\isa{monoid}}}
+       \put(40,00){\makebox(0,0){\isa{group}}}
+       \put(20,55){\vector(0,-1){10}}
+       \put(15,35){\vector(-1,-1){10}}
+       \put(05,15){\vector(3,-1){30}}
+     \end{picture}
+     \caption{Subclass relationship of monoids and groups:
+        before and after establishing the relationship
+        \isa{group\ {\isasymsubseteq}\ monoid};  transitive edges left out.}
+     \label{fig:subclass}
+   \end{center}
+  \end{figure}
+
+  For illustration, a derived definition
in \isa{group} which uses \isa{pow{\isacharunderscore}nat}:%
\end{isamarkuptext}%
\isamarkuptrue%
@@ -751,17 +884,13 @@
\ \ \ \ \ \ \ \ 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}%
\begin{isamarkuptext}%
-\noindent   yields the global definition of
+\noindent yields the global definition of
\isa{{\isachardoublequote}pow{\isacharunderscore}int\ {\isasymColon}\ int\ {\isasymRightarrow}\ {\isasymalpha}{\isasymColon}group\ {\isasymRightarrow}\ {\isasymalpha}{\isasymColon}group{\isachardoublequote}}
with the corresponding theorem \isa{pow{\isacharunderscore}int\ k\ x\ {\isacharequal}\ {\isacharparenleft}if\ {\isadigit{0}}\ {\isasymle}\ k\ then\ pow{\isacharunderscore}nat\ {\isacharparenleft}nat\ k{\isacharparenright}\ x\ else\ {\isacharparenleft}pow{\isacharunderscore}nat\ {\isacharparenleft}nat\ {\isacharparenleft}{\isacharminus}\ k{\isacharparenright}{\isacharparenright}\ x{\isacharparenright}{\isasymdiv}{\isacharparenright}}.%
\end{isamarkuptext}%
\isamarkuptrue%
%
-\isamarkupsection{Further issues%
-}
-\isamarkuptrue%
-%
-\isamarkupsubsection{Code generation%
+\isamarkupsection{Type classes and code generation%
}
\isamarkuptrue%
%