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