src/Doc/Tutorial/Types/Axioms.thy
author wenzelm
Sat, 05 Apr 2014 15:03:40 +0200
changeset 56421 1ffd7eaa778b
parent 53015 a1119cf551e8
child 58620 7435b6a3f72e
permissions -rw-r--r--
updated to jedit_build-20140405: Code2HTML.jar, CommonControls.jar, Console.jar, kappalayout.jar, Navigator.jar, SideKick.jar, doc with jEdit manuals (ant dist-manuals);
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
31678
752f23a37240 reworked section on type classes
haftmann
parents: 27027
diff changeset
     1
(*<*)theory Axioms imports Overloading Setup begin(*>*)
752f23a37240 reworked section on type classes
haftmann
parents: 27027
diff changeset
     2
752f23a37240 reworked section on type classes
haftmann
parents: 27027
diff changeset
     3
subsection {* Axioms *}
752f23a37240 reworked section on type classes
haftmann
parents: 27027
diff changeset
     4
752f23a37240 reworked section on type classes
haftmann
parents: 27027
diff changeset
     5
text {* Attaching axioms to our classes lets us reason on the level of
752f23a37240 reworked section on type classes
haftmann
parents: 27027
diff changeset
     6
classes.  The results will be applicable to all types in a class, just
752f23a37240 reworked section on type classes
haftmann
parents: 27027
diff changeset
     7
as in axiomatic mathematics.
752f23a37240 reworked section on type classes
haftmann
parents: 27027
diff changeset
     8
752f23a37240 reworked section on type classes
haftmann
parents: 27027
diff changeset
     9
\begin{warn}
752f23a37240 reworked section on type classes
haftmann
parents: 27027
diff changeset
    10
Proofs in this section use structured \emph{Isar} proofs, which are not
752f23a37240 reworked section on type classes
haftmann
parents: 27027
diff changeset
    11
covered in this tutorial; but see \cite{Nipkow-TYPES02}.%
752f23a37240 reworked section on type classes
haftmann
parents: 27027
diff changeset
    12
\end{warn} *}
752f23a37240 reworked section on type classes
haftmann
parents: 27027
diff changeset
    13
752f23a37240 reworked section on type classes
haftmann
parents: 27027
diff changeset
    14
subsubsection {* Semigroups *}
752f23a37240 reworked section on type classes
haftmann
parents: 27027
diff changeset
    15
31682
358cdcdf56d2 corrected some issues
haftmann
parents: 31678
diff changeset
    16
text{* We specify \emph{semigroups} as subclass of @{class plus}: *}
31678
752f23a37240 reworked section on type classes
haftmann
parents: 27027
diff changeset
    17
752f23a37240 reworked section on type classes
haftmann
parents: 27027
diff changeset
    18
class semigroup = plus +
752f23a37240 reworked section on type classes
haftmann
parents: 27027
diff changeset
    19
  assumes assoc: "(x \<oplus> y) \<oplus> z = x \<oplus> (y \<oplus> z)"
752f23a37240 reworked section on type classes
haftmann
parents: 27027
diff changeset
    20
752f23a37240 reworked section on type classes
haftmann
parents: 27027
diff changeset
    21
text {* \noindent This @{command class} specification requires that
752f23a37240 reworked section on type classes
haftmann
parents: 27027
diff changeset
    22
all instances of @{class semigroup} obey @{fact "assoc:"}~@{prop
752f23a37240 reworked section on type classes
haftmann
parents: 27027
diff changeset
    23
[source] "\<And>x y z \<Colon> 'a\<Colon>semigroup. (x \<oplus> y) \<oplus> z = x \<oplus> (y \<oplus> z)"}.
10328
bf33cbd76c05 *** empty log message ***
nipkow
parents:
diff changeset
    24
31678
752f23a37240 reworked section on type classes
haftmann
parents: 27027
diff changeset
    25
We can use this class axiom to derive further abstract theorems
752f23a37240 reworked section on type classes
haftmann
parents: 27027
diff changeset
    26
relative to class @{class semigroup}: *}
752f23a37240 reworked section on type classes
haftmann
parents: 27027
diff changeset
    27
752f23a37240 reworked section on type classes
haftmann
parents: 27027
diff changeset
    28
lemma assoc_left:
752f23a37240 reworked section on type classes
haftmann
parents: 27027
diff changeset
    29
  fixes x y z :: "'a\<Colon>semigroup"
752f23a37240 reworked section on type classes
haftmann
parents: 27027
diff changeset
    30
  shows "x \<oplus> (y \<oplus> z) = (x \<oplus> y) \<oplus> z"
752f23a37240 reworked section on type classes
haftmann
parents: 27027
diff changeset
    31
  using assoc by (rule sym)
752f23a37240 reworked section on type classes
haftmann
parents: 27027
diff changeset
    32
752f23a37240 reworked section on type classes
haftmann
parents: 27027
diff changeset
    33
text {* \noindent The @{class semigroup} constraint on type @{typ
752f23a37240 reworked section on type classes
haftmann
parents: 27027
diff changeset
    34
"'a"} restricts instantiations of @{typ "'a"} to types of class
752f23a37240 reworked section on type classes
haftmann
parents: 27027
diff changeset
    35
@{class semigroup} and during the proof enables us to use the fact
752f23a37240 reworked section on type classes
haftmann
parents: 27027
diff changeset
    36
@{fact assoc} whose type parameter is itself constrained to class
31682
358cdcdf56d2 corrected some issues
haftmann
parents: 31678
diff changeset
    37
@{class semigroup}.  The main advantage of classes is that theorems
358cdcdf56d2 corrected some issues
haftmann
parents: 31678
diff changeset
    38
can be proved in the abstract and freely reused for each instance.
31678
752f23a37240 reworked section on type classes
haftmann
parents: 27027
diff changeset
    39
752f23a37240 reworked section on type classes
haftmann
parents: 27027
diff changeset
    40
On instantiation, we have to give a proof that the given operations
752f23a37240 reworked section on type classes
haftmann
parents: 27027
diff changeset
    41
obey the class axioms: *}
752f23a37240 reworked section on type classes
haftmann
parents: 27027
diff changeset
    42
752f23a37240 reworked section on type classes
haftmann
parents: 27027
diff changeset
    43
instantiation nat :: semigroup
752f23a37240 reworked section on type classes
haftmann
parents: 27027
diff changeset
    44
begin
752f23a37240 reworked section on type classes
haftmann
parents: 27027
diff changeset
    45
752f23a37240 reworked section on type classes
haftmann
parents: 27027
diff changeset
    46
instance proof
752f23a37240 reworked section on type classes
haftmann
parents: 27027
diff changeset
    47
752f23a37240 reworked section on type classes
haftmann
parents: 27027
diff changeset
    48
txt {* \noindent The proof opens with a default proof step, which for
752f23a37240 reworked section on type classes
haftmann
parents: 27027
diff changeset
    49
instance judgements invokes method @{method intro_classes}. *}
10328
bf33cbd76c05 *** empty log message ***
nipkow
parents:
diff changeset
    50
bf33cbd76c05 *** empty log message ***
nipkow
parents:
diff changeset
    51
31678
752f23a37240 reworked section on type classes
haftmann
parents: 27027
diff changeset
    52
  fix m n q :: nat
752f23a37240 reworked section on type classes
haftmann
parents: 27027
diff changeset
    53
  show "(m \<oplus> n) \<oplus> q = m \<oplus> (n \<oplus> q)"
752f23a37240 reworked section on type classes
haftmann
parents: 27027
diff changeset
    54
    by (induct m) simp_all
752f23a37240 reworked section on type classes
haftmann
parents: 27027
diff changeset
    55
qed
10328
bf33cbd76c05 *** empty log message ***
nipkow
parents:
diff changeset
    56
31678
752f23a37240 reworked section on type classes
haftmann
parents: 27027
diff changeset
    57
end
10328
bf33cbd76c05 *** empty log message ***
nipkow
parents:
diff changeset
    58
31678
752f23a37240 reworked section on type classes
haftmann
parents: 27027
diff changeset
    59
text {* \noindent Again, the interesting things enter the stage with
752f23a37240 reworked section on type classes
haftmann
parents: 27027
diff changeset
    60
parametric types: *}
752f23a37240 reworked section on type classes
haftmann
parents: 27027
diff changeset
    61
38325
6daf896bca5e * -> prod
haftmann
parents: 31682
diff changeset
    62
instantiation prod :: (semigroup, semigroup) semigroup
31678
752f23a37240 reworked section on type classes
haftmann
parents: 27027
diff changeset
    63
begin
10328
bf33cbd76c05 *** empty log message ***
nipkow
parents:
diff changeset
    64
31678
752f23a37240 reworked section on type classes
haftmann
parents: 27027
diff changeset
    65
instance proof
53015
a1119cf551e8 standardized symbols via "isabelle update_sub_sup", excluding src/Pure and src/Tools/WWW_Find;
wenzelm
parents: 48985
diff changeset
    66
  fix p\<^sub>1 p\<^sub>2 p\<^sub>3 :: "'a\<Colon>semigroup \<times> 'b\<Colon>semigroup"
a1119cf551e8 standardized symbols via "isabelle update_sub_sup", excluding src/Pure and src/Tools/WWW_Find;
wenzelm
parents: 48985
diff changeset
    67
  show "p\<^sub>1 \<oplus> p\<^sub>2 \<oplus> p\<^sub>3 = p\<^sub>1 \<oplus> (p\<^sub>2 \<oplus> p\<^sub>3)"
a1119cf551e8 standardized symbols via "isabelle update_sub_sup", excluding src/Pure and src/Tools/WWW_Find;
wenzelm
parents: 48985
diff changeset
    68
    by (cases p\<^sub>1, cases p\<^sub>2, cases p\<^sub>3) (simp add: assoc)
10328
bf33cbd76c05 *** empty log message ***
nipkow
parents:
diff changeset
    69
31678
752f23a37240 reworked section on type classes
haftmann
parents: 27027
diff changeset
    70
txt {* \noindent Associativity of product semigroups is established
752f23a37240 reworked section on type classes
haftmann
parents: 27027
diff changeset
    71
using the hypothetical associativity @{fact assoc} of the type
752f23a37240 reworked section on type classes
haftmann
parents: 27027
diff changeset
    72
components, which holds due to the @{class semigroup} constraints
752f23a37240 reworked section on type classes
haftmann
parents: 27027
diff changeset
    73
imposed on the type components by the @{command instance} proposition.
752f23a37240 reworked section on type classes
haftmann
parents: 27027
diff changeset
    74
Indeed, this pattern often occurs with parametric types and type
752f23a37240 reworked section on type classes
haftmann
parents: 27027
diff changeset
    75
classes. *}
10420
ef006735bee8 *** empty log message ***
nipkow
parents: 10396
diff changeset
    76
31678
752f23a37240 reworked section on type classes
haftmann
parents: 27027
diff changeset
    77
qed
10328
bf33cbd76c05 *** empty log message ***
nipkow
parents:
diff changeset
    78
31678
752f23a37240 reworked section on type classes
haftmann
parents: 27027
diff changeset
    79
end
752f23a37240 reworked section on type classes
haftmann
parents: 27027
diff changeset
    80
752f23a37240 reworked section on type classes
haftmann
parents: 27027
diff changeset
    81
subsubsection {* Monoids *}
10328
bf33cbd76c05 *** empty log message ***
nipkow
parents:
diff changeset
    82
31678
752f23a37240 reworked section on type classes
haftmann
parents: 27027
diff changeset
    83
text {* We define a subclass @{text monoidl} (a semigroup with a
752f23a37240 reworked section on type classes
haftmann
parents: 27027
diff changeset
    84
left-hand neutral) by extending @{class semigroup} with one additional
752f23a37240 reworked section on type classes
haftmann
parents: 27027
diff changeset
    85
parameter @{text neutral} together with its property: *}
10328
bf33cbd76c05 *** empty log message ***
nipkow
parents:
diff changeset
    86
31678
752f23a37240 reworked section on type classes
haftmann
parents: 27027
diff changeset
    87
class monoidl = semigroup +
752f23a37240 reworked section on type classes
haftmann
parents: 27027
diff changeset
    88
  fixes neutral :: "'a" ("\<zero>")
752f23a37240 reworked section on type classes
haftmann
parents: 27027
diff changeset
    89
  assumes neutl: "\<zero> \<oplus> x = x"
10328
bf33cbd76c05 *** empty log message ***
nipkow
parents:
diff changeset
    90
31678
752f23a37240 reworked section on type classes
haftmann
parents: 27027
diff changeset
    91
text {* \noindent Again, we prove some instances, by providing
752f23a37240 reworked section on type classes
haftmann
parents: 27027
diff changeset
    92
suitable parameter definitions and proofs for the additional
752f23a37240 reworked section on type classes
haftmann
parents: 27027
diff changeset
    93
specifications. *}
10328
bf33cbd76c05 *** empty log message ***
nipkow
parents:
diff changeset
    94
31678
752f23a37240 reworked section on type classes
haftmann
parents: 27027
diff changeset
    95
instantiation nat :: monoidl
752f23a37240 reworked section on type classes
haftmann
parents: 27027
diff changeset
    96
begin
10328
bf33cbd76c05 *** empty log message ***
nipkow
parents:
diff changeset
    97
31678
752f23a37240 reworked section on type classes
haftmann
parents: 27027
diff changeset
    98
definition
752f23a37240 reworked section on type classes
haftmann
parents: 27027
diff changeset
    99
  neutral_nat_def: "\<zero> = (0\<Colon>nat)"
10328
bf33cbd76c05 *** empty log message ***
nipkow
parents:
diff changeset
   100
31678
752f23a37240 reworked section on type classes
haftmann
parents: 27027
diff changeset
   101
instance proof
752f23a37240 reworked section on type classes
haftmann
parents: 27027
diff changeset
   102
  fix n :: nat
752f23a37240 reworked section on type classes
haftmann
parents: 27027
diff changeset
   103
  show "\<zero> \<oplus> n = n"
752f23a37240 reworked section on type classes
haftmann
parents: 27027
diff changeset
   104
    unfolding neutral_nat_def by simp
752f23a37240 reworked section on type classes
haftmann
parents: 27027
diff changeset
   105
qed
10328
bf33cbd76c05 *** empty log message ***
nipkow
parents:
diff changeset
   106
31678
752f23a37240 reworked section on type classes
haftmann
parents: 27027
diff changeset
   107
end
10328
bf33cbd76c05 *** empty log message ***
nipkow
parents:
diff changeset
   108
31682
358cdcdf56d2 corrected some issues
haftmann
parents: 31678
diff changeset
   109
text {* \noindent In contrast to the examples above, we here have both
31678
752f23a37240 reworked section on type classes
haftmann
parents: 27027
diff changeset
   110
specification of class operations and a non-trivial instance proof.
752f23a37240 reworked section on type classes
haftmann
parents: 27027
diff changeset
   111
752f23a37240 reworked section on type classes
haftmann
parents: 27027
diff changeset
   112
This covers products as well:
10328
bf33cbd76c05 *** empty log message ***
nipkow
parents:
diff changeset
   113
*}
bf33cbd76c05 *** empty log message ***
nipkow
parents:
diff changeset
   114
38325
6daf896bca5e * -> prod
haftmann
parents: 31682
diff changeset
   115
instantiation prod :: (monoidl, monoidl) monoidl
31678
752f23a37240 reworked section on type classes
haftmann
parents: 27027
diff changeset
   116
begin
10328
bf33cbd76c05 *** empty log message ***
nipkow
parents:
diff changeset
   117
31678
752f23a37240 reworked section on type classes
haftmann
parents: 27027
diff changeset
   118
definition
752f23a37240 reworked section on type classes
haftmann
parents: 27027
diff changeset
   119
  neutral_prod_def: "\<zero> = (\<zero>, \<zero>)"
10328
bf33cbd76c05 *** empty log message ***
nipkow
parents:
diff changeset
   120
31678
752f23a37240 reworked section on type classes
haftmann
parents: 27027
diff changeset
   121
instance proof
752f23a37240 reworked section on type classes
haftmann
parents: 27027
diff changeset
   122
  fix p :: "'a\<Colon>monoidl \<times> 'b\<Colon>monoidl"
752f23a37240 reworked section on type classes
haftmann
parents: 27027
diff changeset
   123
  show "\<zero> \<oplus> p = p"
752f23a37240 reworked section on type classes
haftmann
parents: 27027
diff changeset
   124
    by (cases p) (simp add: neutral_prod_def neutl)
752f23a37240 reworked section on type classes
haftmann
parents: 27027
diff changeset
   125
qed
10328
bf33cbd76c05 *** empty log message ***
nipkow
parents:
diff changeset
   126
31678
752f23a37240 reworked section on type classes
haftmann
parents: 27027
diff changeset
   127
end
10328
bf33cbd76c05 *** empty log message ***
nipkow
parents:
diff changeset
   128
31678
752f23a37240 reworked section on type classes
haftmann
parents: 27027
diff changeset
   129
text {* \noindent Fully-fledged monoids are modelled by another
752f23a37240 reworked section on type classes
haftmann
parents: 27027
diff changeset
   130
subclass which does not add new parameters but tightens the
752f23a37240 reworked section on type classes
haftmann
parents: 27027
diff changeset
   131
specification: *}
10328
bf33cbd76c05 *** empty log message ***
nipkow
parents:
diff changeset
   132
31678
752f23a37240 reworked section on type classes
haftmann
parents: 27027
diff changeset
   133
class monoid = monoidl +
752f23a37240 reworked section on type classes
haftmann
parents: 27027
diff changeset
   134
  assumes neutr: "x \<oplus> \<zero> = x"
10328
bf33cbd76c05 *** empty log message ***
nipkow
parents:
diff changeset
   135
31678
752f23a37240 reworked section on type classes
haftmann
parents: 27027
diff changeset
   136
text {* \noindent Corresponding instances for @{typ nat} and products
752f23a37240 reworked section on type classes
haftmann
parents: 27027
diff changeset
   137
are left as an exercise to the reader. *}
752f23a37240 reworked section on type classes
haftmann
parents: 27027
diff changeset
   138
752f23a37240 reworked section on type classes
haftmann
parents: 27027
diff changeset
   139
subsubsection {* Groups *}
10328
bf33cbd76c05 *** empty log message ***
nipkow
parents:
diff changeset
   140
31678
752f23a37240 reworked section on type classes
haftmann
parents: 27027
diff changeset
   141
text {* \noindent To finish our small algebra example, we add a @{text
752f23a37240 reworked section on type classes
haftmann
parents: 27027
diff changeset
   142
group} class: *}
10328
bf33cbd76c05 *** empty log message ***
nipkow
parents:
diff changeset
   143
31678
752f23a37240 reworked section on type classes
haftmann
parents: 27027
diff changeset
   144
class group = monoidl +
752f23a37240 reworked section on type classes
haftmann
parents: 27027
diff changeset
   145
  fixes inv :: "'a \<Rightarrow> 'a" ("\<div> _" [81] 80)
752f23a37240 reworked section on type classes
haftmann
parents: 27027
diff changeset
   146
  assumes invl: "\<div> x \<oplus> x = \<zero>"
11196
bb4ede27fcb7 *** empty log message ***
nipkow
parents: 10885
diff changeset
   147
31678
752f23a37240 reworked section on type classes
haftmann
parents: 27027
diff changeset
   148
text {* \noindent We continue with a further example for abstract
752f23a37240 reworked section on type classes
haftmann
parents: 27027
diff changeset
   149
proofs relative to type classes: *}
11196
bb4ede27fcb7 *** empty log message ***
nipkow
parents: 10885
diff changeset
   150
31678
752f23a37240 reworked section on type classes
haftmann
parents: 27027
diff changeset
   151
lemma left_cancel:
752f23a37240 reworked section on type classes
haftmann
parents: 27027
diff changeset
   152
  fixes x y z :: "'a\<Colon>group"
752f23a37240 reworked section on type classes
haftmann
parents: 27027
diff changeset
   153
  shows "x \<oplus> y = x \<oplus> z \<longleftrightarrow> y = z"
752f23a37240 reworked section on type classes
haftmann
parents: 27027
diff changeset
   154
proof
752f23a37240 reworked section on type classes
haftmann
parents: 27027
diff changeset
   155
  assume "x \<oplus> y = x \<oplus> z"
752f23a37240 reworked section on type classes
haftmann
parents: 27027
diff changeset
   156
  then have "\<div> x \<oplus> (x \<oplus> y) = \<div> x \<oplus> (x \<oplus> z)" by simp
752f23a37240 reworked section on type classes
haftmann
parents: 27027
diff changeset
   157
  then have "(\<div> x \<oplus> x) \<oplus> y = (\<div> x \<oplus> x) \<oplus> z" by (simp add: assoc)
752f23a37240 reworked section on type classes
haftmann
parents: 27027
diff changeset
   158
  then show "y = z" by (simp add: invl neutl)
752f23a37240 reworked section on type classes
haftmann
parents: 27027
diff changeset
   159
next
752f23a37240 reworked section on type classes
haftmann
parents: 27027
diff changeset
   160
  assume "y = z"
752f23a37240 reworked section on type classes
haftmann
parents: 27027
diff changeset
   161
  then show "x \<oplus> y = x \<oplus> z" by simp
752f23a37240 reworked section on type classes
haftmann
parents: 27027
diff changeset
   162
qed
10328
bf33cbd76c05 *** empty log message ***
nipkow
parents:
diff changeset
   163
31678
752f23a37240 reworked section on type classes
haftmann
parents: 27027
diff changeset
   164
text {* \noindent Any @{text "group"} is also a @{text "monoid"}; this
752f23a37240 reworked section on type classes
haftmann
parents: 27027
diff changeset
   165
can be made explicit by claiming an additional subclass relation,
752f23a37240 reworked section on type classes
haftmann
parents: 27027
diff changeset
   166
together with a proof of the logical difference: *}
10328
bf33cbd76c05 *** empty log message ***
nipkow
parents:
diff changeset
   167
31678
752f23a37240 reworked section on type classes
haftmann
parents: 27027
diff changeset
   168
instance group \<subseteq> monoid
752f23a37240 reworked section on type classes
haftmann
parents: 27027
diff changeset
   169
proof
752f23a37240 reworked section on type classes
haftmann
parents: 27027
diff changeset
   170
  fix x
752f23a37240 reworked section on type classes
haftmann
parents: 27027
diff changeset
   171
  from invl have "\<div> x \<oplus> x = \<zero>" .
752f23a37240 reworked section on type classes
haftmann
parents: 27027
diff changeset
   172
  then have "\<div> x \<oplus> (x \<oplus> \<zero>) = \<div> x \<oplus> x"
752f23a37240 reworked section on type classes
haftmann
parents: 27027
diff changeset
   173
    by (simp add: neutl invl assoc [symmetric])
752f23a37240 reworked section on type classes
haftmann
parents: 27027
diff changeset
   174
  then show "x \<oplus> \<zero> = x" by (simp add: left_cancel)
752f23a37240 reworked section on type classes
haftmann
parents: 27027
diff changeset
   175
qed
10396
5ab08609e6c8 *** empty log message ***
nipkow
parents: 10362
diff changeset
   176
31678
752f23a37240 reworked section on type classes
haftmann
parents: 27027
diff changeset
   177
text {* \noindent The proof result is propagated to the type system,
752f23a37240 reworked section on type classes
haftmann
parents: 27027
diff changeset
   178
making @{text group} an instance of @{text monoid} by adding an
752f23a37240 reworked section on type classes
haftmann
parents: 27027
diff changeset
   179
additional edge to the graph of subclass relation; see also
10396
5ab08609e6c8 *** empty log message ***
nipkow
parents: 10362
diff changeset
   180
Figure~\ref{fig:subclass}.
5ab08609e6c8 *** empty log message ***
nipkow
parents: 10362
diff changeset
   181
5ab08609e6c8 *** empty log message ***
nipkow
parents: 10362
diff changeset
   182
\begin{figure}[htbp]
31678
752f23a37240 reworked section on type classes
haftmann
parents: 27027
diff changeset
   183
 \begin{center}
752f23a37240 reworked section on type classes
haftmann
parents: 27027
diff changeset
   184
   \small
752f23a37240 reworked section on type classes
haftmann
parents: 27027
diff changeset
   185
   \unitlength 0.6mm
752f23a37240 reworked section on type classes
haftmann
parents: 27027
diff changeset
   186
   \begin{picture}(40,60)(0,0)
752f23a37240 reworked section on type classes
haftmann
parents: 27027
diff changeset
   187
     \put(20,60){\makebox(0,0){@{text semigroup}}}
752f23a37240 reworked section on type classes
haftmann
parents: 27027
diff changeset
   188
     \put(20,40){\makebox(0,0){@{text monoidl}}}
752f23a37240 reworked section on type classes
haftmann
parents: 27027
diff changeset
   189
     \put(00,20){\makebox(0,0){@{text monoid}}}
752f23a37240 reworked section on type classes
haftmann
parents: 27027
diff changeset
   190
     \put(40,00){\makebox(0,0){@{text group}}}
752f23a37240 reworked section on type classes
haftmann
parents: 27027
diff changeset
   191
     \put(20,55){\vector(0,-1){10}}
752f23a37240 reworked section on type classes
haftmann
parents: 27027
diff changeset
   192
     \put(15,35){\vector(-1,-1){10}}
752f23a37240 reworked section on type classes
haftmann
parents: 27027
diff changeset
   193
     \put(25,35){\vector(1,-3){10}}
752f23a37240 reworked section on type classes
haftmann
parents: 27027
diff changeset
   194
   \end{picture}
752f23a37240 reworked section on type classes
haftmann
parents: 27027
diff changeset
   195
   \hspace{8em}
752f23a37240 reworked section on type classes
haftmann
parents: 27027
diff changeset
   196
   \begin{picture}(40,60)(0,0)
752f23a37240 reworked section on type classes
haftmann
parents: 27027
diff changeset
   197
     \put(20,60){\makebox(0,0){@{text semigroup}}}
752f23a37240 reworked section on type classes
haftmann
parents: 27027
diff changeset
   198
     \put(20,40){\makebox(0,0){@{text monoidl}}}
752f23a37240 reworked section on type classes
haftmann
parents: 27027
diff changeset
   199
     \put(00,20){\makebox(0,0){@{text monoid}}}
752f23a37240 reworked section on type classes
haftmann
parents: 27027
diff changeset
   200
     \put(40,00){\makebox(0,0){@{text group}}}
752f23a37240 reworked section on type classes
haftmann
parents: 27027
diff changeset
   201
     \put(20,55){\vector(0,-1){10}}
752f23a37240 reworked section on type classes
haftmann
parents: 27027
diff changeset
   202
     \put(15,35){\vector(-1,-1){10}}
752f23a37240 reworked section on type classes
haftmann
parents: 27027
diff changeset
   203
     \put(05,15){\vector(3,-1){30}}
752f23a37240 reworked section on type classes
haftmann
parents: 27027
diff changeset
   204
   \end{picture}
752f23a37240 reworked section on type classes
haftmann
parents: 27027
diff changeset
   205
   \caption{Subclass relationship of monoids and groups:
752f23a37240 reworked section on type classes
haftmann
parents: 27027
diff changeset
   206
      before and after establishing the relationship
752f23a37240 reworked section on type classes
haftmann
parents: 27027
diff changeset
   207
      @{text "group \<subseteq> monoid"};  transitive edges are left out.}
752f23a37240 reworked section on type classes
haftmann
parents: 27027
diff changeset
   208
   \label{fig:subclass}
752f23a37240 reworked section on type classes
haftmann
parents: 27027
diff changeset
   209
 \end{center}
10396
5ab08609e6c8 *** empty log message ***
nipkow
parents: 10362
diff changeset
   210
\end{figure}
5ab08609e6c8 *** empty log message ***
nipkow
parents: 10362
diff changeset
   211
*}
5ab08609e6c8 *** empty log message ***
nipkow
parents: 10362
diff changeset
   212
31678
752f23a37240 reworked section on type classes
haftmann
parents: 27027
diff changeset
   213
subsubsection {* Inconsistencies *}
10328
bf33cbd76c05 *** empty log message ***
nipkow
parents:
diff changeset
   214
31678
752f23a37240 reworked section on type classes
haftmann
parents: 27027
diff changeset
   215
text {* The reader may be wondering what happens if we attach an
752f23a37240 reworked section on type classes
haftmann
parents: 27027
diff changeset
   216
inconsistent set of axioms to a class. So far we have always avoided
752f23a37240 reworked section on type classes
haftmann
parents: 27027
diff changeset
   217
to add new axioms to HOL for fear of inconsistencies and suddenly it
10328
bf33cbd76c05 *** empty log message ***
nipkow
parents:
diff changeset
   218
seems that we are throwing all caution to the wind. So why is there no
bf33cbd76c05 *** empty log message ***
nipkow
parents:
diff changeset
   219
problem?
bf33cbd76c05 *** empty log message ***
nipkow
parents:
diff changeset
   220
31678
752f23a37240 reworked section on type classes
haftmann
parents: 27027
diff changeset
   221
The point is that by construction, all type variables in the axioms of
752f23a37240 reworked section on type classes
haftmann
parents: 27027
diff changeset
   222
a \isacommand{class} are automatically constrained with the class
752f23a37240 reworked section on type classes
haftmann
parents: 27027
diff changeset
   223
being defined (as shown for axiom @{thm[source]refl} above). These
752f23a37240 reworked section on type classes
haftmann
parents: 27027
diff changeset
   224
constraints are always carried around and Isabelle takes care that
752f23a37240 reworked section on type classes
haftmann
parents: 27027
diff changeset
   225
they are never lost, unless the type variable is instantiated with a
752f23a37240 reworked section on type classes
haftmann
parents: 27027
diff changeset
   226
type that has been shown to belong to that class. Thus you may be able
752f23a37240 reworked section on type classes
haftmann
parents: 27027
diff changeset
   227
to prove @{prop False} from your axioms, but Isabelle will remind you
752f23a37240 reworked section on type classes
haftmann
parents: 27027
diff changeset
   228
that this theorem has the hidden hypothesis that the class is
752f23a37240 reworked section on type classes
haftmann
parents: 27027
diff changeset
   229
non-empty.
752f23a37240 reworked section on type classes
haftmann
parents: 27027
diff changeset
   230
752f23a37240 reworked section on type classes
haftmann
parents: 27027
diff changeset
   231
Even if each individual class is consistent, intersections of
752f23a37240 reworked section on type classes
haftmann
parents: 27027
diff changeset
   232
(unrelated) classes readily become inconsistent in practice. Now we
752f23a37240 reworked section on type classes
haftmann
parents: 27027
diff changeset
   233
know this need not worry us. *}
752f23a37240 reworked section on type classes
haftmann
parents: 27027
diff changeset
   234
752f23a37240 reworked section on type classes
haftmann
parents: 27027
diff changeset
   235
752f23a37240 reworked section on type classes
haftmann
parents: 27027
diff changeset
   236
subsubsection{* Syntactic Classes and Predefined Overloading *}
12332
aea72a834c85 *** empty log message ***
nipkow
parents: 11494
diff changeset
   237
31678
752f23a37240 reworked section on type classes
haftmann
parents: 27027
diff changeset
   238
text {* In our algebra example, we have started with a \emph{syntactic
752f23a37240 reworked section on type classes
haftmann
parents: 27027
diff changeset
   239
class} @{class plus} which only specifies operations but no axioms; it
752f23a37240 reworked section on type classes
haftmann
parents: 27027
diff changeset
   240
would have been also possible to start immediately with class @{class
752f23a37240 reworked section on type classes
haftmann
parents: 27027
diff changeset
   241
semigroup}, specifying the @{text "\<oplus>"} operation and associativity at
752f23a37240 reworked section on type classes
haftmann
parents: 27027
diff changeset
   242
the same time.
10328
bf33cbd76c05 *** empty log message ***
nipkow
parents:
diff changeset
   243
31678
752f23a37240 reworked section on type classes
haftmann
parents: 27027
diff changeset
   244
Which approach is more appropriate depends.  Usually it is more
752f23a37240 reworked section on type classes
haftmann
parents: 27027
diff changeset
   245
convenient to introduce operations and axioms in the same class: then
752f23a37240 reworked section on type classes
haftmann
parents: 27027
diff changeset
   246
the type checker will automatically insert the corresponding class
752f23a37240 reworked section on type classes
haftmann
parents: 27027
diff changeset
   247
constraints whenever the operations occur, reducing the need of manual
752f23a37240 reworked section on type classes
haftmann
parents: 27027
diff changeset
   248
annotations.  However, when operations are decorated with popular
752f23a37240 reworked section on type classes
haftmann
parents: 27027
diff changeset
   249
syntax, syntactic classes can be an option to re-use the syntax in
752f23a37240 reworked section on type classes
haftmann
parents: 27027
diff changeset
   250
different contexts; this is indeed the way most overloaded constants
752f23a37240 reworked section on type classes
haftmann
parents: 27027
diff changeset
   251
in HOL are introduced, of which the most important are listed in
752f23a37240 reworked section on type classes
haftmann
parents: 27027
diff changeset
   252
Table~\ref{tab:overloading} in the appendix.  Section
752f23a37240 reworked section on type classes
haftmann
parents: 27027
diff changeset
   253
\ref{sec:numeric-classes} covers a range of corresponding classes
752f23a37240 reworked section on type classes
haftmann
parents: 27027
diff changeset
   254
\emph{with} axioms.
10328
bf33cbd76c05 *** empty log message ***
nipkow
parents:
diff changeset
   255
31678
752f23a37240 reworked section on type classes
haftmann
parents: 27027
diff changeset
   256
Further note that classes may contain axioms but \emph{no} operations.
752f23a37240 reworked section on type classes
haftmann
parents: 27027
diff changeset
   257
An example is class @{class finite} from theory @{theory Finite_Set}
752f23a37240 reworked section on type classes
haftmann
parents: 27027
diff changeset
   258
which specifies a type to be finite: @{lemma [source] "finite (UNIV \<Colon> 'a\<Colon>finite
752f23a37240 reworked section on type classes
haftmann
parents: 27027
diff changeset
   259
set)" by (fact finite_UNIV)}. *}
752f23a37240 reworked section on type classes
haftmann
parents: 27027
diff changeset
   260
10328
bf33cbd76c05 *** empty log message ***
nipkow
parents:
diff changeset
   261
(*<*)end(*>*)