src/Doc/Classes/Classes.thy
author wenzelm
Wed, 27 Mar 2013 16:38:25 +0100
changeset 51553 63327f679cff
parent 51143 0a2371e7ced3
child 53015 a1119cf551e8
permissions -rw-r--r--
more ambitious Goal.skip_proofs: covers Goal.prove forms as well, and do not insist in quick_and_dirty (for the sake of Isabelle/jEdit);
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
20946
75b56e51fade initial draft
haftmann
parents:
diff changeset
     1
theory Classes
28565
haftmann
parents: 28540
diff changeset
     2
imports Main Setup
20946
75b56e51fade initial draft
haftmann
parents:
diff changeset
     3
begin
75b56e51fade initial draft
haftmann
parents:
diff changeset
     4
75b56e51fade initial draft
haftmann
parents:
diff changeset
     5
section {* Introduction *}
75b56e51fade initial draft
haftmann
parents:
diff changeset
     6
75b56e51fade initial draft
haftmann
parents:
diff changeset
     7
text {*
31691
7d50527dc008 Polishing the English
paulson
parents: 31675
diff changeset
     8
  Type classes were introduced by Wadler and Blott \cite{wadler89how}
7d50527dc008 Polishing the English
paulson
parents: 31675
diff changeset
     9
  into the Haskell language to allow for a reasonable implementation
22317
b550d2c6ca90 continued class tutorial
haftmann
parents: 20946
diff changeset
    10
  of overloading\footnote{throughout this tutorial, we are referring
38812
e527a34bf69d tuned whitespace
haftmann
parents: 38322
diff changeset
    11
  to classical Haskell 1.0 type classes, not considering later
e527a34bf69d tuned whitespace
haftmann
parents: 38322
diff changeset
    12
  additions in expressiveness}.  As a canonical example, a polymorphic
e527a34bf69d tuned whitespace
haftmann
parents: 38322
diff changeset
    13
  equality function @{text "eq \<Colon> \<alpha> \<Rightarrow> \<alpha> \<Rightarrow> bool"} which is overloaded on
e527a34bf69d tuned whitespace
haftmann
parents: 38322
diff changeset
    14
  different types for @{text "\<alpha>"}, which is achieved by splitting
e527a34bf69d tuned whitespace
haftmann
parents: 38322
diff changeset
    15
  introduction of the @{text eq} function from its overloaded
e527a34bf69d tuned whitespace
haftmann
parents: 38322
diff changeset
    16
  definitions by means of @{text class} and @{text instance}
e527a34bf69d tuned whitespace
haftmann
parents: 38322
diff changeset
    17
  declarations: \footnote{syntax here is a kind of isabellized
e527a34bf69d tuned whitespace
haftmann
parents: 38322
diff changeset
    18
  Haskell}
22317
b550d2c6ca90 continued class tutorial
haftmann
parents: 20946
diff changeset
    19
28565
haftmann
parents: 28540
diff changeset
    20
  \begin{quote}
haftmann
parents: 28540
diff changeset
    21
30227
853abb4853cc tuned manuals
haftmann
parents: 30226
diff changeset
    22
  \noindent@{text "class eq where"} \\
28565
haftmann
parents: 28540
diff changeset
    23
  \hspace*{2ex}@{text "eq \<Colon> \<alpha> \<Rightarrow> \<alpha> \<Rightarrow> bool"}
20946
75b56e51fade initial draft
haftmann
parents:
diff changeset
    24
28565
haftmann
parents: 28540
diff changeset
    25
  \medskip\noindent@{text "instance nat \<Colon> eq where"} \\
haftmann
parents: 28540
diff changeset
    26
  \hspace*{2ex}@{text "eq 0 0 = True"} \\
haftmann
parents: 28540
diff changeset
    27
  \hspace*{2ex}@{text "eq 0 _ = False"} \\
haftmann
parents: 28540
diff changeset
    28
  \hspace*{2ex}@{text "eq _ 0 = False"} \\
haftmann
parents: 28540
diff changeset
    29
  \hspace*{2ex}@{text "eq (Suc n) (Suc m) = eq n m"}
22317
b550d2c6ca90 continued class tutorial
haftmann
parents: 20946
diff changeset
    30
28948
1860f016886d fixed typo
haftmann
parents: 28947
diff changeset
    31
  \medskip\noindent@{text "instance (\<alpha>\<Colon>eq, \<beta>\<Colon>eq) pair \<Colon> eq where"} \\
28565
haftmann
parents: 28540
diff changeset
    32
  \hspace*{2ex}@{text "eq (x1, y1) (x2, y2) = eq x1 x2 \<and> eq y1 y2"}
20946
75b56e51fade initial draft
haftmann
parents:
diff changeset
    33
28565
haftmann
parents: 28540
diff changeset
    34
  \medskip\noindent@{text "class ord extends eq where"} \\
haftmann
parents: 28540
diff changeset
    35
  \hspace*{2ex}@{text "less_eq \<Colon> \<alpha> \<Rightarrow> \<alpha> \<Rightarrow> bool"} \\
haftmann
parents: 28540
diff changeset
    36
  \hspace*{2ex}@{text "less \<Colon> \<alpha> \<Rightarrow> \<alpha> \<Rightarrow> bool"}
22317
b550d2c6ca90 continued class tutorial
haftmann
parents: 20946
diff changeset
    37
28565
haftmann
parents: 28540
diff changeset
    38
  \end{quote}
haftmann
parents: 28540
diff changeset
    39
haftmann
parents: 28540
diff changeset
    40
  \noindent Type variables are annotated with (finitely many) classes;
22317
b550d2c6ca90 continued class tutorial
haftmann
parents: 20946
diff changeset
    41
  these annotations are assertions that a particular polymorphic type
b550d2c6ca90 continued class tutorial
haftmann
parents: 20946
diff changeset
    42
  provides definitions for overloaded functions.
b550d2c6ca90 continued class tutorial
haftmann
parents: 20946
diff changeset
    43
38812
e527a34bf69d tuned whitespace
haftmann
parents: 38322
diff changeset
    44
  Indeed, type classes not only allow for simple overloading but form
e527a34bf69d tuned whitespace
haftmann
parents: 38322
diff changeset
    45
  a generic calculus, an instance of order-sorted algebra
e527a34bf69d tuned whitespace
haftmann
parents: 38322
diff changeset
    46
  \cite{nipkow-sorts93,Nipkow-Prehofer:1993,Wenzel:1997:TPHOL}.
20946
75b56e51fade initial draft
haftmann
parents:
diff changeset
    47
38812
e527a34bf69d tuned whitespace
haftmann
parents: 38322
diff changeset
    48
  From a software engineering point of view, type classes roughly
e527a34bf69d tuned whitespace
haftmann
parents: 38322
diff changeset
    49
  correspond to interfaces in object-oriented languages like Java; so,
e527a34bf69d tuned whitespace
haftmann
parents: 38322
diff changeset
    50
  it is naturally desirable that type classes do not only provide
e527a34bf69d tuned whitespace
haftmann
parents: 38322
diff changeset
    51
  functions (class parameters) but also state specifications
22317
b550d2c6ca90 continued class tutorial
haftmann
parents: 20946
diff changeset
    52
  implementations must obey.  For example, the @{text "class eq"}
22550
c5039bee2602 updated
haftmann
parents: 22479
diff changeset
    53
  above could be given the following specification, demanding that
c5039bee2602 updated
haftmann
parents: 22479
diff changeset
    54
  @{text "class eq"} is an equivalence relation obeying reflexivity,
c5039bee2602 updated
haftmann
parents: 22479
diff changeset
    55
  symmetry and transitivity:
22317
b550d2c6ca90 continued class tutorial
haftmann
parents: 20946
diff changeset
    56
28565
haftmann
parents: 28540
diff changeset
    57
  \begin{quote}
22317
b550d2c6ca90 continued class tutorial
haftmann
parents: 20946
diff changeset
    58
28565
haftmann
parents: 28540
diff changeset
    59
  \noindent@{text "class eq where"} \\
haftmann
parents: 28540
diff changeset
    60
  \hspace*{2ex}@{text "eq \<Colon> \<alpha> \<Rightarrow> \<alpha> \<Rightarrow> bool"} \\
haftmann
parents: 28540
diff changeset
    61
  @{text "satisfying"} \\
haftmann
parents: 28540
diff changeset
    62
  \hspace*{2ex}@{text "refl: eq x x"} \\
haftmann
parents: 28540
diff changeset
    63
  \hspace*{2ex}@{text "sym: eq x y \<longleftrightarrow> eq x y"} \\
haftmann
parents: 28540
diff changeset
    64
  \hspace*{2ex}@{text "trans: eq x y \<and> eq y z \<longrightarrow> eq x z"}
haftmann
parents: 28540
diff changeset
    65
haftmann
parents: 28540
diff changeset
    66
  \end{quote}
haftmann
parents: 28540
diff changeset
    67
38812
e527a34bf69d tuned whitespace
haftmann
parents: 38322
diff changeset
    68
  \noindent From a theoretical point of view, type classes are
e527a34bf69d tuned whitespace
haftmann
parents: 38322
diff changeset
    69
  lightweight modules; Haskell type classes may be emulated by SML
e527a34bf69d tuned whitespace
haftmann
parents: 38322
diff changeset
    70
  functors \cite{classes_modules}.  Isabelle/Isar offers a discipline
e527a34bf69d tuned whitespace
haftmann
parents: 38322
diff changeset
    71
  of type classes which brings all those aspects together:
22317
b550d2c6ca90 continued class tutorial
haftmann
parents: 20946
diff changeset
    72
b550d2c6ca90 continued class tutorial
haftmann
parents: 20946
diff changeset
    73
  \begin{enumerate}
24991
c6f5cc939c29 added subclass command
haftmann
parents: 24628
diff changeset
    74
    \item specifying abstract parameters together with
22317
b550d2c6ca90 continued class tutorial
haftmann
parents: 20946
diff changeset
    75
       corresponding specifications,
28540
haftmann
parents: 27505
diff changeset
    76
    \item instantiating those abstract parameters by a particular
22317
b550d2c6ca90 continued class tutorial
haftmann
parents: 20946
diff changeset
    77
       type
b550d2c6ca90 continued class tutorial
haftmann
parents: 20946
diff changeset
    78
    \item in connection with a ``less ad-hoc'' approach to overloading,
31691
7d50527dc008 Polishing the English
paulson
parents: 31675
diff changeset
    79
    \item with a direct link to the Isabelle module system:
7d50527dc008 Polishing the English
paulson
parents: 31675
diff changeset
    80
      locales \cite{kammueller-locales}.
22317
b550d2c6ca90 continued class tutorial
haftmann
parents: 20946
diff changeset
    81
  \end{enumerate}
b550d2c6ca90 continued class tutorial
haftmann
parents: 20946
diff changeset
    82
38812
e527a34bf69d tuned whitespace
haftmann
parents: 38322
diff changeset
    83
  \noindent Isar type classes also directly support code generation in
e527a34bf69d tuned whitespace
haftmann
parents: 38322
diff changeset
    84
  a Haskell like fashion. Internally, they are mapped to more
e527a34bf69d tuned whitespace
haftmann
parents: 38322
diff changeset
    85
  primitive Isabelle concepts \cite{Haftmann-Wenzel:2006:classes}.
22317
b550d2c6ca90 continued class tutorial
haftmann
parents: 20946
diff changeset
    86
38812
e527a34bf69d tuned whitespace
haftmann
parents: 38322
diff changeset
    87
  This tutorial demonstrates common elements of structured
e527a34bf69d tuned whitespace
haftmann
parents: 38322
diff changeset
    88
  specifications and abstract reasoning with type classes by the
e527a34bf69d tuned whitespace
haftmann
parents: 38322
diff changeset
    89
  algebraic hierarchy of semigroups, monoids and groups.  Our
e527a34bf69d tuned whitespace
haftmann
parents: 38322
diff changeset
    90
  background theory is that of Isabelle/HOL \cite{isa-tutorial}, for
e527a34bf69d tuned whitespace
haftmann
parents: 38322
diff changeset
    91
  which some familiarity is assumed.
20946
75b56e51fade initial draft
haftmann
parents:
diff changeset
    92
*}
75b56e51fade initial draft
haftmann
parents:
diff changeset
    93
22317
b550d2c6ca90 continued class tutorial
haftmann
parents: 20946
diff changeset
    94
section {* A simple algebra example \label{sec:example} *}
20946
75b56e51fade initial draft
haftmann
parents:
diff changeset
    95
75b56e51fade initial draft
haftmann
parents:
diff changeset
    96
subsection {* Class definition *}
75b56e51fade initial draft
haftmann
parents:
diff changeset
    97
75b56e51fade initial draft
haftmann
parents:
diff changeset
    98
text {*
75b56e51fade initial draft
haftmann
parents:
diff changeset
    99
  Depending on an arbitrary type @{text "\<alpha>"}, class @{text
28565
haftmann
parents: 28540
diff changeset
   100
  "semigroup"} introduces a binary operator @{text "(\<otimes>)"} that is
20946
75b56e51fade initial draft
haftmann
parents:
diff changeset
   101
  assumed to be associative:
75b56e51fade initial draft
haftmann
parents:
diff changeset
   102
*}
75b56e51fade initial draft
haftmann
parents:
diff changeset
   103
29705
a1ecdd8cf81c updated class documentation
haftmann
parents: 29513
diff changeset
   104
class %quote semigroup =
28565
haftmann
parents: 28540
diff changeset
   105
  fixes mult :: "\<alpha> \<Rightarrow> \<alpha> \<Rightarrow> \<alpha>"    (infixl "\<otimes>" 70)
haftmann
parents: 28540
diff changeset
   106
  assumes assoc: "(x \<otimes> y) \<otimes> z = x \<otimes> (y \<otimes> z)"
20946
75b56e51fade initial draft
haftmann
parents:
diff changeset
   107
75b56e51fade initial draft
haftmann
parents:
diff changeset
   108
text {*
38812
e527a34bf69d tuned whitespace
haftmann
parents: 38322
diff changeset
   109
  \noindent This @{command class} specification consists of two parts:
e527a34bf69d tuned whitespace
haftmann
parents: 38322
diff changeset
   110
  the \qn{operational} part names the class parameter (@{element
e527a34bf69d tuned whitespace
haftmann
parents: 38322
diff changeset
   111
  "fixes"}), the \qn{logical} part specifies properties on them
e527a34bf69d tuned whitespace
haftmann
parents: 38322
diff changeset
   112
  (@{element "assumes"}).  The local @{element "fixes"} and @{element
e527a34bf69d tuned whitespace
haftmann
parents: 38322
diff changeset
   113
  "assumes"} are lifted to the theory toplevel, yielding the global
24991
c6f5cc939c29 added subclass command
haftmann
parents: 24628
diff changeset
   114
  parameter @{term [source] "mult \<Colon> \<alpha>\<Colon>semigroup \<Rightarrow> \<alpha> \<Rightarrow> \<alpha>"} and the
38812
e527a34bf69d tuned whitespace
haftmann
parents: 38322
diff changeset
   115
  global theorem @{fact "semigroup.assoc:"}~@{prop [source] "\<And>x y z \<Colon>
e527a34bf69d tuned whitespace
haftmann
parents: 38322
diff changeset
   116
  \<alpha>\<Colon>semigroup. (x \<otimes> y) \<otimes> z = x \<otimes> (y \<otimes> z)"}.
20946
75b56e51fade initial draft
haftmann
parents:
diff changeset
   117
*}
75b56e51fade initial draft
haftmann
parents:
diff changeset
   118
75b56e51fade initial draft
haftmann
parents:
diff changeset
   119
75b56e51fade initial draft
haftmann
parents:
diff changeset
   120
subsection {* Class instantiation \label{sec:class_inst} *}
75b56e51fade initial draft
haftmann
parents:
diff changeset
   121
75b56e51fade initial draft
haftmann
parents:
diff changeset
   122
text {*
38812
e527a34bf69d tuned whitespace
haftmann
parents: 38322
diff changeset
   123
  The concrete type @{typ int} is made a @{class semigroup} instance
e527a34bf69d tuned whitespace
haftmann
parents: 38322
diff changeset
   124
  by providing a suitable definition for the class parameter @{text
e527a34bf69d tuned whitespace
haftmann
parents: 38322
diff changeset
   125
  "(\<otimes>)"} and a proof for the specification of @{fact assoc}.  This is
e527a34bf69d tuned whitespace
haftmann
parents: 38322
diff changeset
   126
  accomplished by the @{command instantiation} target:
20946
75b56e51fade initial draft
haftmann
parents:
diff changeset
   127
*}
75b56e51fade initial draft
haftmann
parents:
diff changeset
   128
28565
haftmann
parents: 28540
diff changeset
   129
instantiation %quote int :: semigroup
haftmann
parents: 28540
diff changeset
   130
begin
25533
0140cc7b26ad added something about instantiation target
haftmann
parents: 25369
diff changeset
   131
28565
haftmann
parents: 28540
diff changeset
   132
definition %quote
haftmann
parents: 28540
diff changeset
   133
  mult_int_def: "i \<otimes> j = i + (j\<Colon>int)"
25533
0140cc7b26ad added something about instantiation target
haftmann
parents: 25369
diff changeset
   134
28565
haftmann
parents: 28540
diff changeset
   135
instance %quote proof
haftmann
parents: 28540
diff changeset
   136
  fix i j k :: int have "(i + j) + k = i + (j + k)" by simp
haftmann
parents: 28540
diff changeset
   137
  then show "(i \<otimes> j) \<otimes> k = i \<otimes> (j \<otimes> k)"
28566
haftmann
parents: 28565
diff changeset
   138
    unfolding mult_int_def .
28565
haftmann
parents: 28540
diff changeset
   139
qed
20946
75b56e51fade initial draft
haftmann
parents:
diff changeset
   140
28565
haftmann
parents: 28540
diff changeset
   141
end %quote
25533
0140cc7b26ad added something about instantiation target
haftmann
parents: 25369
diff changeset
   142
20946
75b56e51fade initial draft
haftmann
parents:
diff changeset
   143
text {*
38812
e527a34bf69d tuned whitespace
haftmann
parents: 38322
diff changeset
   144
  \noindent @{command instantiation} defines class parameters at a
e527a34bf69d tuned whitespace
haftmann
parents: 38322
diff changeset
   145
  particular instance using common specification tools (here,
e527a34bf69d tuned whitespace
haftmann
parents: 38322
diff changeset
   146
  @{command definition}).  The concluding @{command instance} opens a
e527a34bf69d tuned whitespace
haftmann
parents: 38322
diff changeset
   147
  proof that the given parameters actually conform to the class
e527a34bf69d tuned whitespace
haftmann
parents: 38322
diff changeset
   148
  specification.  Note that the first proof step is the @{method
e527a34bf69d tuned whitespace
haftmann
parents: 38322
diff changeset
   149
  default} method, which for such instance proofs maps to the @{method
e527a34bf69d tuned whitespace
haftmann
parents: 38322
diff changeset
   150
  intro_classes} method.  This reduces an instance judgement to the
e527a34bf69d tuned whitespace
haftmann
parents: 38322
diff changeset
   151
  relevant primitive proof goals; typically it is the first method
e527a34bf69d tuned whitespace
haftmann
parents: 38322
diff changeset
   152
  applied in an instantiation proof.
22317
b550d2c6ca90 continued class tutorial
haftmann
parents: 20946
diff changeset
   153
38812
e527a34bf69d tuned whitespace
haftmann
parents: 38322
diff changeset
   154
  From now on, the type-checker will consider @{typ int} as a @{class
e527a34bf69d tuned whitespace
haftmann
parents: 38322
diff changeset
   155
  semigroup} automatically, i.e.\ any general results are immediately
e527a34bf69d tuned whitespace
haftmann
parents: 38322
diff changeset
   156
  available on concrete instances.
28565
haftmann
parents: 28540
diff changeset
   157
38812
e527a34bf69d tuned whitespace
haftmann
parents: 38322
diff changeset
   158
  \medskip Another instance of @{class semigroup} yields the natural
e527a34bf69d tuned whitespace
haftmann
parents: 38322
diff changeset
   159
  numbers:
20946
75b56e51fade initial draft
haftmann
parents:
diff changeset
   160
*}
75b56e51fade initial draft
haftmann
parents:
diff changeset
   161
28565
haftmann
parents: 28540
diff changeset
   162
instantiation %quote nat :: semigroup
haftmann
parents: 28540
diff changeset
   163
begin
25533
0140cc7b26ad added something about instantiation target
haftmann
parents: 25369
diff changeset
   164
28565
haftmann
parents: 28540
diff changeset
   165
primrec %quote mult_nat where
haftmann
parents: 28540
diff changeset
   166
  "(0\<Colon>nat) \<otimes> n = n"
haftmann
parents: 28540
diff changeset
   167
  | "Suc m \<otimes> n = Suc (m \<otimes> n)"
25533
0140cc7b26ad added something about instantiation target
haftmann
parents: 25369
diff changeset
   168
28565
haftmann
parents: 28540
diff changeset
   169
instance %quote proof
haftmann
parents: 28540
diff changeset
   170
  fix m n q :: nat 
haftmann
parents: 28540
diff changeset
   171
  show "m \<otimes> n \<otimes> q = m \<otimes> (n \<otimes> q)"
haftmann
parents: 28540
diff changeset
   172
    by (induct m) auto
haftmann
parents: 28540
diff changeset
   173
qed
20946
75b56e51fade initial draft
haftmann
parents:
diff changeset
   174
28565
haftmann
parents: 28540
diff changeset
   175
end %quote
20946
75b56e51fade initial draft
haftmann
parents:
diff changeset
   176
25871
45753d56d935 some more primrec
haftmann
parents: 25868
diff changeset
   177
text {*
38812
e527a34bf69d tuned whitespace
haftmann
parents: 38322
diff changeset
   178
  \noindent Note the occurence of the name @{text mult_nat} in the
e527a34bf69d tuned whitespace
haftmann
parents: 38322
diff changeset
   179
  primrec declaration; by default, the local name of a class operation
e527a34bf69d tuned whitespace
haftmann
parents: 38322
diff changeset
   180
  @{text f} to be instantiated on type constructor @{text \<kappa>} is
e527a34bf69d tuned whitespace
haftmann
parents: 38322
diff changeset
   181
  mangled as @{text f_\<kappa>}.  In case of uncertainty, these names may be
e527a34bf69d tuned whitespace
haftmann
parents: 38322
diff changeset
   182
  inspected using the @{command "print_context"} command or the
e527a34bf69d tuned whitespace
haftmann
parents: 38322
diff changeset
   183
  corresponding ProofGeneral button.
25871
45753d56d935 some more primrec
haftmann
parents: 25868
diff changeset
   184
*}
45753d56d935 some more primrec
haftmann
parents: 25868
diff changeset
   185
25247
haftmann
parents: 25200
diff changeset
   186
subsection {* Lifting and parametric types *}
haftmann
parents: 25200
diff changeset
   187
haftmann
parents: 25200
diff changeset
   188
text {*
38812
e527a34bf69d tuned whitespace
haftmann
parents: 38322
diff changeset
   189
  Overloaded definitions given at a class instantiation may include
e527a34bf69d tuned whitespace
haftmann
parents: 38322
diff changeset
   190
  recursion over the syntactic structure of types.  As a canonical
e527a34bf69d tuned whitespace
haftmann
parents: 38322
diff changeset
   191
  example, we model product semigroups using our simple algebra:
25247
haftmann
parents: 25200
diff changeset
   192
*}
haftmann
parents: 25200
diff changeset
   193
37706
c63649d8d75b updated document
haftmann
parents: 35282
diff changeset
   194
instantiation %quote prod :: (semigroup, semigroup) semigroup
28565
haftmann
parents: 28540
diff changeset
   195
begin
25533
0140cc7b26ad added something about instantiation target
haftmann
parents: 25369
diff changeset
   196
28565
haftmann
parents: 28540
diff changeset
   197
definition %quote
31931
0b1d807b1c2d restored subscripts
haftmann
parents: 31691
diff changeset
   198
  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)"
25533
0140cc7b26ad added something about instantiation target
haftmann
parents: 25369
diff changeset
   199
28565
haftmann
parents: 28540
diff changeset
   200
instance %quote proof
31931
0b1d807b1c2d restored subscripts
haftmann
parents: 31691
diff changeset
   201
  fix p\<^isub>1 p\<^isub>2 p\<^isub>3 :: "\<alpha>\<Colon>semigroup \<times> \<beta>\<Colon>semigroup"
0b1d807b1c2d restored subscripts
haftmann
parents: 31691
diff changeset
   202
  show "p\<^isub>1 \<otimes> p\<^isub>2 \<otimes> p\<^isub>3 = p\<^isub>1 \<otimes> (p\<^isub>2 \<otimes> p\<^isub>3)"
28566
haftmann
parents: 28565
diff changeset
   203
    unfolding mult_prod_def by (simp add: assoc)
28565
haftmann
parents: 28540
diff changeset
   204
qed      
25247
haftmann
parents: 25200
diff changeset
   205
28565
haftmann
parents: 28540
diff changeset
   206
end %quote
25533
0140cc7b26ad added something about instantiation target
haftmann
parents: 25369
diff changeset
   207
25247
haftmann
parents: 25200
diff changeset
   208
text {*
31675
6c95ec0394f1 fixed grammar
haftmann
parents: 31255
diff changeset
   209
  \noindent Associativity of product semigroups is established using
28565
haftmann
parents: 28540
diff changeset
   210
  the definition of @{text "(\<otimes>)"} on products and the hypothetical
38812
e527a34bf69d tuned whitespace
haftmann
parents: 38322
diff changeset
   211
  associativity of the type components; these hypotheses are
e527a34bf69d tuned whitespace
haftmann
parents: 38322
diff changeset
   212
  legitimate due to the @{class semigroup} constraints imposed on the
e527a34bf69d tuned whitespace
haftmann
parents: 38322
diff changeset
   213
  type components by the @{command instance} proposition.  Indeed,
e527a34bf69d tuned whitespace
haftmann
parents: 38322
diff changeset
   214
  this pattern often occurs with parametric types and type classes.
25247
haftmann
parents: 25200
diff changeset
   215
*}
haftmann
parents: 25200
diff changeset
   216
haftmann
parents: 25200
diff changeset
   217
haftmann
parents: 25200
diff changeset
   218
subsection {* Subclassing *}
20946
75b56e51fade initial draft
haftmann
parents:
diff changeset
   219
75b56e51fade initial draft
haftmann
parents:
diff changeset
   220
text {*
38812
e527a34bf69d tuned whitespace
haftmann
parents: 38322
diff changeset
   221
  We define a subclass @{text monoidl} (a semigroup with a left-hand
e527a34bf69d tuned whitespace
haftmann
parents: 38322
diff changeset
   222
  neutral) by extending @{class semigroup} with one additional
e527a34bf69d tuned whitespace
haftmann
parents: 38322
diff changeset
   223
  parameter @{text neutral} together with its characteristic property:
20946
75b56e51fade initial draft
haftmann
parents:
diff changeset
   224
*}
75b56e51fade initial draft
haftmann
parents:
diff changeset
   225
28565
haftmann
parents: 28540
diff changeset
   226
class %quote monoidl = semigroup +
haftmann
parents: 28540
diff changeset
   227
  fixes neutral :: "\<alpha>" ("\<one>")
haftmann
parents: 28540
diff changeset
   228
  assumes neutl: "\<one> \<otimes> x = x"
20946
75b56e51fade initial draft
haftmann
parents:
diff changeset
   229
75b56e51fade initial draft
haftmann
parents:
diff changeset
   230
text {*
38812
e527a34bf69d tuned whitespace
haftmann
parents: 38322
diff changeset
   231
  \noindent Again, we prove some instances, by providing suitable
e527a34bf69d tuned whitespace
haftmann
parents: 38322
diff changeset
   232
  parameter definitions and proofs for the additional specifications.
e527a34bf69d tuned whitespace
haftmann
parents: 38322
diff changeset
   233
  Observe that instantiations for types with the same arity may be
e527a34bf69d tuned whitespace
haftmann
parents: 38322
diff changeset
   234
  simultaneous:
20946
75b56e51fade initial draft
haftmann
parents:
diff changeset
   235
*}
75b56e51fade initial draft
haftmann
parents:
diff changeset
   236
28566
haftmann
parents: 28565
diff changeset
   237
instantiation %quote nat and int :: monoidl
haftmann
parents: 28565
diff changeset
   238
begin
25533
0140cc7b26ad added something about instantiation target
haftmann
parents: 25369
diff changeset
   239
28566
haftmann
parents: 28565
diff changeset
   240
definition %quote
haftmann
parents: 28565
diff changeset
   241
  neutral_nat_def: "\<one> = (0\<Colon>nat)"
25533
0140cc7b26ad added something about instantiation target
haftmann
parents: 25369
diff changeset
   242
28566
haftmann
parents: 28565
diff changeset
   243
definition %quote
haftmann
parents: 28565
diff changeset
   244
  neutral_int_def: "\<one> = (0\<Colon>int)"
25533
0140cc7b26ad added something about instantiation target
haftmann
parents: 25369
diff changeset
   245
28566
haftmann
parents: 28565
diff changeset
   246
instance %quote proof
haftmann
parents: 28565
diff changeset
   247
  fix n :: nat
haftmann
parents: 28565
diff changeset
   248
  show "\<one> \<otimes> n = n"
haftmann
parents: 28565
diff changeset
   249
    unfolding neutral_nat_def by simp
haftmann
parents: 28565
diff changeset
   250
next
haftmann
parents: 28565
diff changeset
   251
  fix k :: int
haftmann
parents: 28565
diff changeset
   252
  show "\<one> \<otimes> k = k"
haftmann
parents: 28565
diff changeset
   253
    unfolding neutral_int_def mult_int_def by simp
haftmann
parents: 28565
diff changeset
   254
qed
20946
75b56e51fade initial draft
haftmann
parents:
diff changeset
   255
28566
haftmann
parents: 28565
diff changeset
   256
end %quote
25533
0140cc7b26ad added something about instantiation target
haftmann
parents: 25369
diff changeset
   257
37706
c63649d8d75b updated document
haftmann
parents: 35282
diff changeset
   258
instantiation %quote prod :: (monoidl, monoidl) monoidl
28566
haftmann
parents: 28565
diff changeset
   259
begin
25533
0140cc7b26ad added something about instantiation target
haftmann
parents: 25369
diff changeset
   260
28566
haftmann
parents: 28565
diff changeset
   261
definition %quote
haftmann
parents: 28565
diff changeset
   262
  neutral_prod_def: "\<one> = (\<one>, \<one>)"
25533
0140cc7b26ad added something about instantiation target
haftmann
parents: 25369
diff changeset
   263
28566
haftmann
parents: 28565
diff changeset
   264
instance %quote proof
haftmann
parents: 28565
diff changeset
   265
  fix p :: "\<alpha>\<Colon>monoidl \<times> \<beta>\<Colon>monoidl"
haftmann
parents: 28565
diff changeset
   266
  show "\<one> \<otimes> p = p"
haftmann
parents: 28565
diff changeset
   267
    unfolding neutral_prod_def mult_prod_def by (simp add: neutl)
haftmann
parents: 28565
diff changeset
   268
qed
20946
75b56e51fade initial draft
haftmann
parents:
diff changeset
   269
28566
haftmann
parents: 28565
diff changeset
   270
end %quote
25533
0140cc7b26ad added something about instantiation target
haftmann
parents: 25369
diff changeset
   271
20946
75b56e51fade initial draft
haftmann
parents:
diff changeset
   272
text {*
31691
7d50527dc008 Polishing the English
paulson
parents: 31675
diff changeset
   273
  \noindent Fully-fledged monoids are modelled by another subclass,
24991
c6f5cc939c29 added subclass command
haftmann
parents: 24628
diff changeset
   274
  which does not add new parameters but tightens the specification:
20946
75b56e51fade initial draft
haftmann
parents:
diff changeset
   275
*}
75b56e51fade initial draft
haftmann
parents:
diff changeset
   276
28566
haftmann
parents: 28565
diff changeset
   277
class %quote monoid = monoidl +
haftmann
parents: 28565
diff changeset
   278
  assumes neutr: "x \<otimes> \<one> = x"
20946
75b56e51fade initial draft
haftmann
parents:
diff changeset
   279
28566
haftmann
parents: 28565
diff changeset
   280
instantiation %quote nat and int :: monoid 
haftmann
parents: 28565
diff changeset
   281
begin
25533
0140cc7b26ad added something about instantiation target
haftmann
parents: 25369
diff changeset
   282
28566
haftmann
parents: 28565
diff changeset
   283
instance %quote proof
haftmann
parents: 28565
diff changeset
   284
  fix n :: nat
haftmann
parents: 28565
diff changeset
   285
  show "n \<otimes> \<one> = n"
haftmann
parents: 28565
diff changeset
   286
    unfolding neutral_nat_def by (induct n) simp_all
haftmann
parents: 28565
diff changeset
   287
next
haftmann
parents: 28565
diff changeset
   288
  fix k :: int
haftmann
parents: 28565
diff changeset
   289
  show "k \<otimes> \<one> = k"
haftmann
parents: 28565
diff changeset
   290
    unfolding neutral_int_def mult_int_def by simp
haftmann
parents: 28565
diff changeset
   291
qed
25247
haftmann
parents: 25200
diff changeset
   292
28566
haftmann
parents: 28565
diff changeset
   293
end %quote
25533
0140cc7b26ad added something about instantiation target
haftmann
parents: 25369
diff changeset
   294
37706
c63649d8d75b updated document
haftmann
parents: 35282
diff changeset
   295
instantiation %quote prod :: (monoid, monoid) monoid
28566
haftmann
parents: 28565
diff changeset
   296
begin
25533
0140cc7b26ad added something about instantiation target
haftmann
parents: 25369
diff changeset
   297
28566
haftmann
parents: 28565
diff changeset
   298
instance %quote proof 
haftmann
parents: 28565
diff changeset
   299
  fix p :: "\<alpha>\<Colon>monoid \<times> \<beta>\<Colon>monoid"
haftmann
parents: 28565
diff changeset
   300
  show "p \<otimes> \<one> = p"
haftmann
parents: 28565
diff changeset
   301
    unfolding neutral_prod_def mult_prod_def by (simp add: neutr)
haftmann
parents: 28565
diff changeset
   302
qed
22317
b550d2c6ca90 continued class tutorial
haftmann
parents: 20946
diff changeset
   303
28566
haftmann
parents: 28565
diff changeset
   304
end %quote
25533
0140cc7b26ad added something about instantiation target
haftmann
parents: 25369
diff changeset
   305
22317
b550d2c6ca90 continued class tutorial
haftmann
parents: 20946
diff changeset
   306
text {*
38812
e527a34bf69d tuned whitespace
haftmann
parents: 38322
diff changeset
   307
  \noindent To finish our small algebra example, we add a @{text
e527a34bf69d tuned whitespace
haftmann
parents: 38322
diff changeset
   308
  group} class with a corresponding instance:
22317
b550d2c6ca90 continued class tutorial
haftmann
parents: 20946
diff changeset
   309
*}
20946
75b56e51fade initial draft
haftmann
parents:
diff changeset
   310
28566
haftmann
parents: 28565
diff changeset
   311
class %quote group = monoidl +
haftmann
parents: 28565
diff changeset
   312
  fixes inverse :: "\<alpha> \<Rightarrow> \<alpha>"    ("(_\<div>)" [1000] 999)
haftmann
parents: 28565
diff changeset
   313
  assumes invl: "x\<div> \<otimes> x = \<one>"
20946
75b56e51fade initial draft
haftmann
parents:
diff changeset
   314
28566
haftmann
parents: 28565
diff changeset
   315
instantiation %quote int :: group
haftmann
parents: 28565
diff changeset
   316
begin
haftmann
parents: 28565
diff changeset
   317
haftmann
parents: 28565
diff changeset
   318
definition %quote
haftmann
parents: 28565
diff changeset
   319
  inverse_int_def: "i\<div> = - (i\<Colon>int)"
25533
0140cc7b26ad added something about instantiation target
haftmann
parents: 25369
diff changeset
   320
28566
haftmann
parents: 28565
diff changeset
   321
instance %quote proof
haftmann
parents: 28565
diff changeset
   322
  fix i :: int
haftmann
parents: 28565
diff changeset
   323
  have "-i + i = 0" by simp
haftmann
parents: 28565
diff changeset
   324
  then show "i\<div> \<otimes> i = \<one>"
haftmann
parents: 28565
diff changeset
   325
    unfolding mult_int_def neutral_int_def inverse_int_def .
haftmann
parents: 28565
diff changeset
   326
qed
25533
0140cc7b26ad added something about instantiation target
haftmann
parents: 25369
diff changeset
   327
28566
haftmann
parents: 28565
diff changeset
   328
end %quote
20946
75b56e51fade initial draft
haftmann
parents:
diff changeset
   329
25533
0140cc7b26ad added something about instantiation target
haftmann
parents: 25369
diff changeset
   330
22317
b550d2c6ca90 continued class tutorial
haftmann
parents: 20946
diff changeset
   331
section {* Type classes as locales *}
b550d2c6ca90 continued class tutorial
haftmann
parents: 20946
diff changeset
   332
31691
7d50527dc008 Polishing the English
paulson
parents: 31675
diff changeset
   333
subsection {* A look behind the scenes *}
22317
b550d2c6ca90 continued class tutorial
haftmann
parents: 20946
diff changeset
   334
22347
ddbf185a3be0 continued
haftmann
parents: 22317
diff changeset
   335
text {*
38812
e527a34bf69d tuned whitespace
haftmann
parents: 38322
diff changeset
   336
  The example above gives an impression how Isar type classes work in
e527a34bf69d tuned whitespace
haftmann
parents: 38322
diff changeset
   337
  practice.  As stated in the introduction, classes also provide a
e527a34bf69d tuned whitespace
haftmann
parents: 38322
diff changeset
   338
  link to Isar's locale system.  Indeed, the logical core of a class
31691
7d50527dc008 Polishing the English
paulson
parents: 31675
diff changeset
   339
  is nothing other than a locale:
22347
ddbf185a3be0 continued
haftmann
parents: 22317
diff changeset
   340
*}
ddbf185a3be0 continued
haftmann
parents: 22317
diff changeset
   341
29705
a1ecdd8cf81c updated class documentation
haftmann
parents: 29513
diff changeset
   342
class %quote idem =
22347
ddbf185a3be0 continued
haftmann
parents: 22317
diff changeset
   343
  fixes f :: "\<alpha> \<Rightarrow> \<alpha>"
ddbf185a3be0 continued
haftmann
parents: 22317
diff changeset
   344
  assumes idem: "f (f x) = f x"
22317
b550d2c6ca90 continued class tutorial
haftmann
parents: 20946
diff changeset
   345
b550d2c6ca90 continued class tutorial
haftmann
parents: 20946
diff changeset
   346
text {*
22347
ddbf185a3be0 continued
haftmann
parents: 22317
diff changeset
   347
  \noindent essentially introduces the locale
30227
853abb4853cc tuned manuals
haftmann
parents: 30226
diff changeset
   348
*} (*<*)setup %invisible {* Sign.add_path "foo" *}
853abb4853cc tuned manuals
haftmann
parents: 30226
diff changeset
   349
(*>*)
28566
haftmann
parents: 28565
diff changeset
   350
locale %quote idem =
22347
ddbf185a3be0 continued
haftmann
parents: 22317
diff changeset
   351
  fixes f :: "\<alpha> \<Rightarrow> \<alpha>"
ddbf185a3be0 continued
haftmann
parents: 22317
diff changeset
   352
  assumes idem: "f (f x) = f x"
ddbf185a3be0 continued
haftmann
parents: 22317
diff changeset
   353
22550
c5039bee2602 updated
haftmann
parents: 22479
diff changeset
   354
text {* \noindent together with corresponding constant(s): *}
22347
ddbf185a3be0 continued
haftmann
parents: 22317
diff changeset
   355
28566
haftmann
parents: 28565
diff changeset
   356
consts %quote f :: "\<alpha> \<Rightarrow> \<alpha>"
22347
ddbf185a3be0 continued
haftmann
parents: 22317
diff changeset
   357
22550
c5039bee2602 updated
haftmann
parents: 22479
diff changeset
   358
text {*
c5039bee2602 updated
haftmann
parents: 22479
diff changeset
   359
  \noindent The connection to the type system is done by means
35282
8fd9d555d04d dropped references to old axclass from documentation
haftmann
parents: 31931
diff changeset
   360
  of a primitive type class
30227
853abb4853cc tuned manuals
haftmann
parents: 30226
diff changeset
   361
*} (*<*)setup %invisible {* Sign.add_path "foo" *}
853abb4853cc tuned manuals
haftmann
parents: 30226
diff changeset
   362
(*>*)
35282
8fd9d555d04d dropped references to old axclass from documentation
haftmann
parents: 31931
diff changeset
   363
classes %quote idem < type
8fd9d555d04d dropped references to old axclass from documentation
haftmann
parents: 31931
diff changeset
   364
(*<*)axiomatization where idem: "f (f (x::\<alpha>\<Colon>idem)) = f x"
8fd9d555d04d dropped references to old axclass from documentation
haftmann
parents: 31931
diff changeset
   365
setup %invisible {* Sign.parent_path *}(*>*)
22347
ddbf185a3be0 continued
haftmann
parents: 22317
diff changeset
   366
22550
c5039bee2602 updated
haftmann
parents: 22479
diff changeset
   367
text {* \noindent together with a corresponding interpretation: *}
22347
ddbf185a3be0 continued
haftmann
parents: 22317
diff changeset
   368
29513
363f17dee9ca adapted to changes in class package
haftmann
parents: 29294
diff changeset
   369
interpretation %quote idem_class:
29294
6cd3ac4708d2 crude adaption to intermediate class/locale version;
wenzelm
parents: 28948
diff changeset
   370
  idem "f \<Colon> (\<alpha>\<Colon>idem) \<Rightarrow> \<alpha>"
35282
8fd9d555d04d dropped references to old axclass from documentation
haftmann
parents: 31931
diff changeset
   371
(*<*)proof qed (rule idem)(*>*)
28565
haftmann
parents: 28540
diff changeset
   372
22347
ddbf185a3be0 continued
haftmann
parents: 22317
diff changeset
   373
text {*
31691
7d50527dc008 Polishing the English
paulson
parents: 31675
diff changeset
   374
  \noindent This gives you the full power of the Isabelle module system;
22347
ddbf185a3be0 continued
haftmann
parents: 22317
diff changeset
   375
  conclusions in locale @{text idem} are implicitly propagated
22479
de15ea8fb348 updated code generation sections
haftmann
parents: 22473
diff changeset
   376
  to class @{text idem}.
30227
853abb4853cc tuned manuals
haftmann
parents: 30226
diff changeset
   377
*} (*<*)setup %invisible {* Sign.parent_path *}
853abb4853cc tuned manuals
haftmann
parents: 30226
diff changeset
   378
(*>*)
20946
75b56e51fade initial draft
haftmann
parents:
diff changeset
   379
subsection {* Abstract reasoning *}
75b56e51fade initial draft
haftmann
parents:
diff changeset
   380
75b56e51fade initial draft
haftmann
parents:
diff changeset
   381
text {*
22347
ddbf185a3be0 continued
haftmann
parents: 22317
diff changeset
   382
  Isabelle locales enable reasoning at a general level, while results
20946
75b56e51fade initial draft
haftmann
parents:
diff changeset
   383
  are implicitly transferred to all instances.  For example, we can
75b56e51fade initial draft
haftmann
parents:
diff changeset
   384
  now establish the @{text "left_cancel"} lemma for groups, which
25247
haftmann
parents: 25200
diff changeset
   385
  states that the function @{text "(x \<otimes>)"} is injective:
20946
75b56e51fade initial draft
haftmann
parents:
diff changeset
   386
*}
75b56e51fade initial draft
haftmann
parents:
diff changeset
   387
28566
haftmann
parents: 28565
diff changeset
   388
lemma %quote (in group) left_cancel: "x \<otimes> y = x \<otimes> z \<longleftrightarrow> y = z"
haftmann
parents: 28565
diff changeset
   389
proof
haftmann
parents: 28565
diff changeset
   390
  assume "x \<otimes> y = x \<otimes> z"
haftmann
parents: 28565
diff changeset
   391
  then have "x\<div> \<otimes> (x \<otimes> y) = x\<div> \<otimes> (x \<otimes> z)" by simp
haftmann
parents: 28565
diff changeset
   392
  then have "(x\<div> \<otimes> x) \<otimes> y = (x\<div> \<otimes> x) \<otimes> z" using assoc by simp
haftmann
parents: 28565
diff changeset
   393
  then show "y = z" using neutl and invl by simp
haftmann
parents: 28565
diff changeset
   394
next
haftmann
parents: 28565
diff changeset
   395
  assume "y = z"
haftmann
parents: 28565
diff changeset
   396
  then show "x \<otimes> y = x \<otimes> z" by simp
haftmann
parents: 28565
diff changeset
   397
qed
20946
75b56e51fade initial draft
haftmann
parents:
diff changeset
   398
75b56e51fade initial draft
haftmann
parents:
diff changeset
   399
text {*
38812
e527a34bf69d tuned whitespace
haftmann
parents: 38322
diff changeset
   400
  \noindent Here the \qt{@{keyword "in"} @{class group}} target
e527a34bf69d tuned whitespace
haftmann
parents: 38322
diff changeset
   401
  specification indicates that the result is recorded within that
e527a34bf69d tuned whitespace
haftmann
parents: 38322
diff changeset
   402
  context for later use.  This local theorem is also lifted to the
e527a34bf69d tuned whitespace
haftmann
parents: 38322
diff changeset
   403
  global one @{fact "group.left_cancel:"} @{prop [source] "\<And>x y z \<Colon>
e527a34bf69d tuned whitespace
haftmann
parents: 38322
diff changeset
   404
  \<alpha>\<Colon>group. x \<otimes> y = x \<otimes> z \<longleftrightarrow> y = z"}.  Since type @{text "int"} has been
e527a34bf69d tuned whitespace
haftmann
parents: 38322
diff changeset
   405
  made an instance of @{text "group"} before, we may refer to that
e527a34bf69d tuned whitespace
haftmann
parents: 38322
diff changeset
   406
  fact as well: @{prop [source] "\<And>x y z \<Colon> int. x \<otimes> y = x \<otimes> z \<longleftrightarrow> y =
e527a34bf69d tuned whitespace
haftmann
parents: 38322
diff changeset
   407
  z"}.
20946
75b56e51fade initial draft
haftmann
parents:
diff changeset
   408
*}
75b56e51fade initial draft
haftmann
parents:
diff changeset
   409
75b56e51fade initial draft
haftmann
parents:
diff changeset
   410
23956
48494ccfabaf updated
haftmann
parents: 22845
diff changeset
   411
subsection {* Derived definitions *}
48494ccfabaf updated
haftmann
parents: 22845
diff changeset
   412
48494ccfabaf updated
haftmann
parents: 22845
diff changeset
   413
text {*
35282
8fd9d555d04d dropped references to old axclass from documentation
haftmann
parents: 31931
diff changeset
   414
  Isabelle locales are targets which support local definitions:
23956
48494ccfabaf updated
haftmann
parents: 22845
diff changeset
   415
*}
48494ccfabaf updated
haftmann
parents: 22845
diff changeset
   416
28566
haftmann
parents: 28565
diff changeset
   417
primrec %quote (in monoid) pow_nat :: "nat \<Rightarrow> \<alpha> \<Rightarrow> \<alpha>" where
haftmann
parents: 28565
diff changeset
   418
  "pow_nat 0 x = \<one>"
haftmann
parents: 28565
diff changeset
   419
  | "pow_nat (Suc n) x = x \<otimes> pow_nat n x"
20946
75b56e51fade initial draft
haftmann
parents:
diff changeset
   420
75b56e51fade initial draft
haftmann
parents:
diff changeset
   421
text {*
23956
48494ccfabaf updated
haftmann
parents: 22845
diff changeset
   422
  \noindent If the locale @{text group} is also a class, this local
38812
e527a34bf69d tuned whitespace
haftmann
parents: 38322
diff changeset
   423
  definition is propagated onto a global definition of @{term [source]
e527a34bf69d tuned whitespace
haftmann
parents: 38322
diff changeset
   424
  "pow_nat \<Colon> nat \<Rightarrow> \<alpha>\<Colon>monoid \<Rightarrow> \<alpha>\<Colon>monoid"} with corresponding theorems
23956
48494ccfabaf updated
haftmann
parents: 22845
diff changeset
   425
48494ccfabaf updated
haftmann
parents: 22845
diff changeset
   426
  @{thm pow_nat.simps [no_vars]}.
20946
75b56e51fade initial draft
haftmann
parents:
diff changeset
   427
38812
e527a34bf69d tuned whitespace
haftmann
parents: 38322
diff changeset
   428
  \noindent As you can see from this example, for local definitions
e527a34bf69d tuned whitespace
haftmann
parents: 38322
diff changeset
   429
  you may use any specification tool which works together with
e527a34bf69d tuned whitespace
haftmann
parents: 38322
diff changeset
   430
  locales, such as Krauss's recursive function package
31691
7d50527dc008 Polishing the English
paulson
parents: 31675
diff changeset
   431
  \cite{krauss2006}.
23956
48494ccfabaf updated
haftmann
parents: 22845
diff changeset
   432
*}
48494ccfabaf updated
haftmann
parents: 22845
diff changeset
   433
48494ccfabaf updated
haftmann
parents: 22845
diff changeset
   434
25247
haftmann
parents: 25200
diff changeset
   435
subsection {* A functor analogy *}
haftmann
parents: 25200
diff changeset
   436
haftmann
parents: 25200
diff changeset
   437
text {*
38812
e527a34bf69d tuned whitespace
haftmann
parents: 38322
diff changeset
   438
  We introduced Isar classes by analogy to type classes in functional
e527a34bf69d tuned whitespace
haftmann
parents: 38322
diff changeset
   439
  programming; if we reconsider this in the context of what has been
e527a34bf69d tuned whitespace
haftmann
parents: 38322
diff changeset
   440
  said about type classes and locales, we can drive this analogy
e527a34bf69d tuned whitespace
haftmann
parents: 38322
diff changeset
   441
  further by stating that type classes essentially correspond to
e527a34bf69d tuned whitespace
haftmann
parents: 38322
diff changeset
   442
  functors that have a canonical interpretation as type classes.
e527a34bf69d tuned whitespace
haftmann
parents: 38322
diff changeset
   443
  There is also the possibility of other interpretations.  For
e527a34bf69d tuned whitespace
haftmann
parents: 38322
diff changeset
   444
  example, @{text list}s also form a monoid with @{text append} and
e527a34bf69d tuned whitespace
haftmann
parents: 38322
diff changeset
   445
  @{term "[]"} as operations, but it seems inappropriate to apply to
e527a34bf69d tuned whitespace
haftmann
parents: 38322
diff changeset
   446
  lists the same operations as for genuinely algebraic types.  In such
e527a34bf69d tuned whitespace
haftmann
parents: 38322
diff changeset
   447
  a case, we can simply make a particular interpretation of monoids
e527a34bf69d tuned whitespace
haftmann
parents: 38322
diff changeset
   448
  for lists:
25247
haftmann
parents: 25200
diff changeset
   449
*}
haftmann
parents: 25200
diff changeset
   450
30729
461ee3e49ad3 interpretation/interpret: prefixes are mandatory by default;
wenzelm
parents: 30227
diff changeset
   451
interpretation %quote list_monoid: monoid append "[]"
28947
ac1a14b5a085 unfold_locales is default method - no need for explicit references
haftmann
parents: 28566
diff changeset
   452
  proof qed auto
25247
haftmann
parents: 25200
diff changeset
   453
haftmann
parents: 25200
diff changeset
   454
text {*
haftmann
parents: 25200
diff changeset
   455
  \noindent This enables us to apply facts on monoids
haftmann
parents: 25200
diff changeset
   456
  to lists, e.g. @{thm list_monoid.neutl [no_vars]}.
haftmann
parents: 25200
diff changeset
   457
haftmann
parents: 25200
diff changeset
   458
  When using this interpretation pattern, it may also
haftmann
parents: 25200
diff changeset
   459
  be appropriate to map derived definitions accordingly:
haftmann
parents: 25200
diff changeset
   460
*}
haftmann
parents: 25200
diff changeset
   461
28566
haftmann
parents: 28565
diff changeset
   462
primrec %quote replicate :: "nat \<Rightarrow> \<alpha> list \<Rightarrow> \<alpha> list" where
haftmann
parents: 28565
diff changeset
   463
  "replicate 0 _ = []"
haftmann
parents: 28565
diff changeset
   464
  | "replicate (Suc n) xs = xs @ replicate n xs"
25247
haftmann
parents: 25200
diff changeset
   465
30729
461ee3e49ad3 interpretation/interpret: prefixes are mandatory by default;
wenzelm
parents: 30227
diff changeset
   466
interpretation %quote list_monoid: monoid append "[]" where
28566
haftmann
parents: 28565
diff changeset
   467
  "monoid.pow_nat append [] = replicate"
haftmann
parents: 28565
diff changeset
   468
proof -
29513
363f17dee9ca adapted to changes in class package
haftmann
parents: 29294
diff changeset
   469
  interpret monoid append "[]" ..
28566
haftmann
parents: 28565
diff changeset
   470
  show "monoid.pow_nat append [] = replicate"
haftmann
parents: 28565
diff changeset
   471
  proof
haftmann
parents: 28565
diff changeset
   472
    fix n
haftmann
parents: 28565
diff changeset
   473
    show "monoid.pow_nat append [] n = replicate n"
haftmann
parents: 28565
diff changeset
   474
      by (induct n) auto
haftmann
parents: 28565
diff changeset
   475
  qed
haftmann
parents: 28565
diff changeset
   476
qed intro_locales
25247
haftmann
parents: 25200
diff changeset
   477
31255
0f8cb37bcafd clarified benefit of interpretation
haftmann
parents: 30729
diff changeset
   478
text {*
0f8cb37bcafd clarified benefit of interpretation
haftmann
parents: 30729
diff changeset
   479
  \noindent This pattern is also helpful to reuse abstract
0f8cb37bcafd clarified benefit of interpretation
haftmann
parents: 30729
diff changeset
   480
  specifications on the \emph{same} type.  For example, think of a
0f8cb37bcafd clarified benefit of interpretation
haftmann
parents: 30729
diff changeset
   481
  class @{text preorder}; for type @{typ nat}, there are at least two
0f8cb37bcafd clarified benefit of interpretation
haftmann
parents: 30729
diff changeset
   482
  possible instances: the natural order or the order induced by the
0f8cb37bcafd clarified benefit of interpretation
haftmann
parents: 30729
diff changeset
   483
  divides relation.  But only one of these instances can be used for
0f8cb37bcafd clarified benefit of interpretation
haftmann
parents: 30729
diff changeset
   484
  @{command instantiation}; using the locale behind the class @{text
0f8cb37bcafd clarified benefit of interpretation
haftmann
parents: 30729
diff changeset
   485
  preorder}, it is still possible to utilise the same abstract
0f8cb37bcafd clarified benefit of interpretation
haftmann
parents: 30729
diff changeset
   486
  specification again using @{command interpretation}.
0f8cb37bcafd clarified benefit of interpretation
haftmann
parents: 30729
diff changeset
   487
*}
25247
haftmann
parents: 25200
diff changeset
   488
24991
c6f5cc939c29 added subclass command
haftmann
parents: 24628
diff changeset
   489
subsection {* Additional subclass relations *}
22347
ddbf185a3be0 continued
haftmann
parents: 22317
diff changeset
   490
ddbf185a3be0 continued
haftmann
parents: 22317
diff changeset
   491
text {*
31255
0f8cb37bcafd clarified benefit of interpretation
haftmann
parents: 30729
diff changeset
   492
  Any @{text "group"} is also a @{text "monoid"}; this can be made
0f8cb37bcafd clarified benefit of interpretation
haftmann
parents: 30729
diff changeset
   493
  explicit by claiming an additional subclass relation, together with
0f8cb37bcafd clarified benefit of interpretation
haftmann
parents: 30729
diff changeset
   494
  a proof of the logical difference:
22347
ddbf185a3be0 continued
haftmann
parents: 22317
diff changeset
   495
*}
ddbf185a3be0 continued
haftmann
parents: 22317
diff changeset
   496
28566
haftmann
parents: 28565
diff changeset
   497
subclass %quote (in group) monoid
28947
ac1a14b5a085 unfold_locales is default method - no need for explicit references
haftmann
parents: 28566
diff changeset
   498
proof
28566
haftmann
parents: 28565
diff changeset
   499
  fix x
haftmann
parents: 28565
diff changeset
   500
  from invl have "x\<div> \<otimes> x = \<one>" by simp
haftmann
parents: 28565
diff changeset
   501
  with assoc [symmetric] neutl invl have "x\<div> \<otimes> (x \<otimes> \<one>) = x\<div> \<otimes> x" by simp
haftmann
parents: 28565
diff changeset
   502
  with left_cancel show "x \<otimes> \<one> = x" by simp
haftmann
parents: 28565
diff changeset
   503
qed
23956
48494ccfabaf updated
haftmann
parents: 22845
diff changeset
   504
48494ccfabaf updated
haftmann
parents: 22845
diff changeset
   505
text {*
38812
e527a34bf69d tuned whitespace
haftmann
parents: 38322
diff changeset
   506
  The logical proof is carried out on the locale level.  Afterwards it
e527a34bf69d tuned whitespace
haftmann
parents: 38322
diff changeset
   507
  is propagated to the type system, making @{text group} an instance
e527a34bf69d tuned whitespace
haftmann
parents: 38322
diff changeset
   508
  of @{text monoid} by adding an additional edge to the graph of
e527a34bf69d tuned whitespace
haftmann
parents: 38322
diff changeset
   509
  subclass relations (\figref{fig:subclass}).
25247
haftmann
parents: 25200
diff changeset
   510
haftmann
parents: 25200
diff changeset
   511
  \begin{figure}[htbp]
haftmann
parents: 25200
diff changeset
   512
   \begin{center}
haftmann
parents: 25200
diff changeset
   513
     \small
haftmann
parents: 25200
diff changeset
   514
     \unitlength 0.6mm
haftmann
parents: 25200
diff changeset
   515
     \begin{picture}(40,60)(0,0)
haftmann
parents: 25200
diff changeset
   516
       \put(20,60){\makebox(0,0){@{text semigroup}}}
haftmann
parents: 25200
diff changeset
   517
       \put(20,40){\makebox(0,0){@{text monoidl}}}
haftmann
parents: 25200
diff changeset
   518
       \put(00,20){\makebox(0,0){@{text monoid}}}
haftmann
parents: 25200
diff changeset
   519
       \put(40,00){\makebox(0,0){@{text group}}}
haftmann
parents: 25200
diff changeset
   520
       \put(20,55){\vector(0,-1){10}}
haftmann
parents: 25200
diff changeset
   521
       \put(15,35){\vector(-1,-1){10}}
haftmann
parents: 25200
diff changeset
   522
       \put(25,35){\vector(1,-3){10}}
haftmann
parents: 25200
diff changeset
   523
     \end{picture}
haftmann
parents: 25200
diff changeset
   524
     \hspace{8em}
haftmann
parents: 25200
diff changeset
   525
     \begin{picture}(40,60)(0,0)
haftmann
parents: 25200
diff changeset
   526
       \put(20,60){\makebox(0,0){@{text semigroup}}}
haftmann
parents: 25200
diff changeset
   527
       \put(20,40){\makebox(0,0){@{text monoidl}}}
haftmann
parents: 25200
diff changeset
   528
       \put(00,20){\makebox(0,0){@{text monoid}}}
haftmann
parents: 25200
diff changeset
   529
       \put(40,00){\makebox(0,0){@{text group}}}
haftmann
parents: 25200
diff changeset
   530
       \put(20,55){\vector(0,-1){10}}
haftmann
parents: 25200
diff changeset
   531
       \put(15,35){\vector(-1,-1){10}}
haftmann
parents: 25200
diff changeset
   532
       \put(05,15){\vector(3,-1){30}}
haftmann
parents: 25200
diff changeset
   533
     \end{picture}
haftmann
parents: 25200
diff changeset
   534
     \caption{Subclass relationship of monoids and groups:
haftmann
parents: 25200
diff changeset
   535
        before and after establishing the relationship
30134
c2640140b951 fixed typo
haftmann
parents: 29705
diff changeset
   536
        @{text "group \<subseteq> monoid"};  transitive edges are left out.}
25247
haftmann
parents: 25200
diff changeset
   537
     \label{fig:subclass}
haftmann
parents: 25200
diff changeset
   538
   \end{center}
haftmann
parents: 25200
diff changeset
   539
  \end{figure}
30227
853abb4853cc tuned manuals
haftmann
parents: 30226
diff changeset
   540
38812
e527a34bf69d tuned whitespace
haftmann
parents: 38322
diff changeset
   541
  For illustration, a derived definition in @{text group} using @{text
e527a34bf69d tuned whitespace
haftmann
parents: 38322
diff changeset
   542
  pow_nat}
23956
48494ccfabaf updated
haftmann
parents: 22845
diff changeset
   543
*}
48494ccfabaf updated
haftmann
parents: 22845
diff changeset
   544
28565
haftmann
parents: 28540
diff changeset
   545
definition %quote (in group) pow_int :: "int \<Rightarrow> \<alpha> \<Rightarrow> \<alpha>" where
haftmann
parents: 28540
diff changeset
   546
  "pow_int k x = (if k >= 0
haftmann
parents: 28540
diff changeset
   547
    then pow_nat (nat k) x
haftmann
parents: 28540
diff changeset
   548
    else (pow_nat (nat (- k)) x)\<div>)"
23956
48494ccfabaf updated
haftmann
parents: 22845
diff changeset
   549
48494ccfabaf updated
haftmann
parents: 22845
diff changeset
   550
text {*
38812
e527a34bf69d tuned whitespace
haftmann
parents: 38322
diff changeset
   551
  \noindent yields the global definition of @{term [source] "pow_int \<Colon>
e527a34bf69d tuned whitespace
haftmann
parents: 38322
diff changeset
   552
  int \<Rightarrow> \<alpha>\<Colon>group \<Rightarrow> \<alpha>\<Colon>group"} with the corresponding theorem @{thm
e527a34bf69d tuned whitespace
haftmann
parents: 38322
diff changeset
   553
  pow_int_def [no_vars]}.
24991
c6f5cc939c29 added subclass command
haftmann
parents: 24628
diff changeset
   554
*}
23956
48494ccfabaf updated
haftmann
parents: 22845
diff changeset
   555
25868
97c6787099bc a note on syntax
haftmann
parents: 25533
diff changeset
   556
subsection {* A note on syntax *}
97c6787099bc a note on syntax
haftmann
parents: 25533
diff changeset
   557
97c6787099bc a note on syntax
haftmann
parents: 25533
diff changeset
   558
text {*
38812
e527a34bf69d tuned whitespace
haftmann
parents: 38322
diff changeset
   559
  As a convenience, class context syntax allows references to local
e527a34bf69d tuned whitespace
haftmann
parents: 38322
diff changeset
   560
  class operations and their global counterparts uniformly; type
e527a34bf69d tuned whitespace
haftmann
parents: 38322
diff changeset
   561
  inference resolves ambiguities.  For example:
25868
97c6787099bc a note on syntax
haftmann
parents: 25533
diff changeset
   562
*}
97c6787099bc a note on syntax
haftmann
parents: 25533
diff changeset
   563
28565
haftmann
parents: 28540
diff changeset
   564
context %quote semigroup
25868
97c6787099bc a note on syntax
haftmann
parents: 25533
diff changeset
   565
begin
97c6787099bc a note on syntax
haftmann
parents: 25533
diff changeset
   566
28565
haftmann
parents: 28540
diff changeset
   567
term %quote "x \<otimes> y" -- {* example 1 *}
haftmann
parents: 28540
diff changeset
   568
term %quote "(x\<Colon>nat) \<otimes> y" -- {* example 2 *}
25868
97c6787099bc a note on syntax
haftmann
parents: 25533
diff changeset
   569
28566
haftmann
parents: 28565
diff changeset
   570
end  %quote
25868
97c6787099bc a note on syntax
haftmann
parents: 25533
diff changeset
   571
28565
haftmann
parents: 28540
diff changeset
   572
term %quote "x \<otimes> y" -- {* example 3 *}
25868
97c6787099bc a note on syntax
haftmann
parents: 25533
diff changeset
   573
97c6787099bc a note on syntax
haftmann
parents: 25533
diff changeset
   574
text {*
38812
e527a34bf69d tuned whitespace
haftmann
parents: 38322
diff changeset
   575
  \noindent Here in example 1, the term refers to the local class
e527a34bf69d tuned whitespace
haftmann
parents: 38322
diff changeset
   576
  operation @{text "mult [\<alpha>]"}, whereas in example 2 the type
e527a34bf69d tuned whitespace
haftmann
parents: 38322
diff changeset
   577
  constraint enforces the global class operation @{text "mult [nat]"}.
e527a34bf69d tuned whitespace
haftmann
parents: 38322
diff changeset
   578
  In the global context in example 3, the reference is to the
e527a34bf69d tuned whitespace
haftmann
parents: 38322
diff changeset
   579
  polymorphic global class operation @{text "mult [?\<alpha> \<Colon> semigroup]"}.
25868
97c6787099bc a note on syntax
haftmann
parents: 25533
diff changeset
   580
*}
22347
ddbf185a3be0 continued
haftmann
parents: 22317
diff changeset
   581
29705
a1ecdd8cf81c updated class documentation
haftmann
parents: 29513
diff changeset
   582
section {* Further issues *}
a1ecdd8cf81c updated class documentation
haftmann
parents: 29513
diff changeset
   583
a1ecdd8cf81c updated class documentation
haftmann
parents: 29513
diff changeset
   584
subsection {* Type classes and code generation *}
22317
b550d2c6ca90 continued class tutorial
haftmann
parents: 20946
diff changeset
   585
b550d2c6ca90 continued class tutorial
haftmann
parents: 20946
diff changeset
   586
text {*
38812
e527a34bf69d tuned whitespace
haftmann
parents: 38322
diff changeset
   587
  Turning back to the first motivation for type classes, namely
e527a34bf69d tuned whitespace
haftmann
parents: 38322
diff changeset
   588
  overloading, it is obvious that overloading stemming from @{command
e527a34bf69d tuned whitespace
haftmann
parents: 38322
diff changeset
   589
  class} statements and @{command instantiation} targets naturally
e527a34bf69d tuned whitespace
haftmann
parents: 38322
diff changeset
   590
  maps to Haskell type classes.  The code generator framework
e527a34bf69d tuned whitespace
haftmann
parents: 38322
diff changeset
   591
  \cite{isabelle-codegen} takes this into account.  If the target
e527a34bf69d tuned whitespace
haftmann
parents: 38322
diff changeset
   592
  language (e.g.~SML) lacks type classes, then they are implemented by
e527a34bf69d tuned whitespace
haftmann
parents: 38322
diff changeset
   593
  an explicit dictionary construction.  As example, let's go back to
e527a34bf69d tuned whitespace
haftmann
parents: 38322
diff changeset
   594
  the power function:
22317
b550d2c6ca90 continued class tutorial
haftmann
parents: 20946
diff changeset
   595
*}
b550d2c6ca90 continued class tutorial
haftmann
parents: 20946
diff changeset
   596
28565
haftmann
parents: 28540
diff changeset
   597
definition %quote example :: int where
haftmann
parents: 28540
diff changeset
   598
  "example = pow_int 10 (-2)"
22317
b550d2c6ca90 continued class tutorial
haftmann
parents: 20946
diff changeset
   599
b550d2c6ca90 continued class tutorial
haftmann
parents: 20946
diff changeset
   600
text {*
31691
7d50527dc008 Polishing the English
paulson
parents: 31675
diff changeset
   601
  \noindent This maps to Haskell as follows:
22317
b550d2c6ca90 continued class tutorial
haftmann
parents: 20946
diff changeset
   602
*}
39743
7aef0e4a3aac combine quote and typewriter tag
haftmann
parents: 39680
diff changeset
   603
text %quotetypewriter {*
39680
a0d49ed5a23a use typewriter tag instead of bare environment
haftmann
parents: 39664
diff changeset
   604
  @{code_stmts example (Haskell)}
39664
0afaf89ab591 more canonical type setting of type writer code examples
haftmann
parents: 38812
diff changeset
   605
*}
22317
b550d2c6ca90 continued class tutorial
haftmann
parents: 20946
diff changeset
   606
b550d2c6ca90 continued class tutorial
haftmann
parents: 20946
diff changeset
   607
text {*
31691
7d50527dc008 Polishing the English
paulson
parents: 31675
diff changeset
   608
  \noindent The code in SML has explicit dictionary passing:
22317
b550d2c6ca90 continued class tutorial
haftmann
parents: 20946
diff changeset
   609
*}
39743
7aef0e4a3aac combine quote and typewriter tag
haftmann
parents: 39680
diff changeset
   610
text %quotetypewriter {*
39680
a0d49ed5a23a use typewriter tag instead of bare environment
haftmann
parents: 39664
diff changeset
   611
  @{code_stmts example (SML)}
39664
0afaf89ab591 more canonical type setting of type writer code examples
haftmann
parents: 38812
diff changeset
   612
*}
0afaf89ab591 more canonical type setting of type writer code examples
haftmann
parents: 38812
diff changeset
   613
20946
75b56e51fade initial draft
haftmann
parents:
diff changeset
   614
38812
e527a34bf69d tuned whitespace
haftmann
parents: 38322
diff changeset
   615
text {*
e527a34bf69d tuned whitespace
haftmann
parents: 38322
diff changeset
   616
  \noindent In Scala, implicts are used as dictionaries:
e527a34bf69d tuned whitespace
haftmann
parents: 38322
diff changeset
   617
*}
39743
7aef0e4a3aac combine quote and typewriter tag
haftmann
parents: 39680
diff changeset
   618
text %quotetypewriter {*
39680
a0d49ed5a23a use typewriter tag instead of bare environment
haftmann
parents: 39664
diff changeset
   619
  @{code_stmts example (Scala)}
39664
0afaf89ab591 more canonical type setting of type writer code examples
haftmann
parents: 38812
diff changeset
   620
*}
38812
e527a34bf69d tuned whitespace
haftmann
parents: 38322
diff changeset
   621
e527a34bf69d tuned whitespace
haftmann
parents: 38322
diff changeset
   622
29705
a1ecdd8cf81c updated class documentation
haftmann
parents: 29513
diff changeset
   623
subsection {* Inspecting the type class universe *}
a1ecdd8cf81c updated class documentation
haftmann
parents: 29513
diff changeset
   624
a1ecdd8cf81c updated class documentation
haftmann
parents: 29513
diff changeset
   625
text {*
38812
e527a34bf69d tuned whitespace
haftmann
parents: 38322
diff changeset
   626
  To facilitate orientation in complex subclass structures, two
e527a34bf69d tuned whitespace
haftmann
parents: 38322
diff changeset
   627
  diagnostics commands are provided:
29705
a1ecdd8cf81c updated class documentation
haftmann
parents: 29513
diff changeset
   628
a1ecdd8cf81c updated class documentation
haftmann
parents: 29513
diff changeset
   629
  \begin{description}
a1ecdd8cf81c updated class documentation
haftmann
parents: 29513
diff changeset
   630
a1ecdd8cf81c updated class documentation
haftmann
parents: 29513
diff changeset
   631
    \item[@{command "print_classes"}] print a list of all classes
a1ecdd8cf81c updated class documentation
haftmann
parents: 29513
diff changeset
   632
      together with associated operations etc.
a1ecdd8cf81c updated class documentation
haftmann
parents: 29513
diff changeset
   633
a1ecdd8cf81c updated class documentation
haftmann
parents: 29513
diff changeset
   634
    \item[@{command "class_deps"}] visualizes the subclass relation
a1ecdd8cf81c updated class documentation
haftmann
parents: 29513
diff changeset
   635
      between all classes as a Hasse diagram.
a1ecdd8cf81c updated class documentation
haftmann
parents: 29513
diff changeset
   636
a1ecdd8cf81c updated class documentation
haftmann
parents: 29513
diff changeset
   637
  \end{description}
a1ecdd8cf81c updated class documentation
haftmann
parents: 29513
diff changeset
   638
*}
a1ecdd8cf81c updated class documentation
haftmann
parents: 29513
diff changeset
   639
20946
75b56e51fade initial draft
haftmann
parents:
diff changeset
   640
end
51143
0a2371e7ced3 two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents: 48985
diff changeset
   641