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