10328
|
1 |
%
|
|
2 |
\begin{isabellebody}%
|
|
3 |
\def\isabellecontext{Axioms}%
|
17056
|
4 |
%
|
|
5 |
\isadelimtheory
|
|
6 |
%
|
|
7 |
\endisadelimtheory
|
|
8 |
%
|
|
9 |
\isatagtheory
|
|
10 |
%
|
|
11 |
\endisatagtheory
|
|
12 |
{\isafoldtheory}%
|
|
13 |
%
|
|
14 |
\isadelimtheory
|
|
15 |
%
|
|
16 |
\endisadelimtheory
|
10328
|
17 |
%
|
10397
|
18 |
\isamarkupsubsection{Axioms%
|
|
19 |
}
|
11866
|
20 |
\isamarkuptrue%
|
10328
|
21 |
%
|
|
22 |
\begin{isamarkuptext}%
|
11494
|
23 |
Attaching axioms to our classes lets us reason on the
|
|
24 |
level of classes. The results will be applicable to all types in a class,
|
|
25 |
just as in axiomatic mathematics. These ideas are demonstrated by means of
|
|
26 |
our ordering relations.%
|
10328
|
27 |
\end{isamarkuptext}%
|
11866
|
28 |
\isamarkuptrue%
|
10328
|
29 |
%
|
10878
|
30 |
\isamarkupsubsubsection{Partial Orders%
|
10397
|
31 |
}
|
11866
|
32 |
\isamarkuptrue%
|
10328
|
33 |
%
|
|
34 |
\begin{isamarkuptext}%
|
|
35 |
A \emph{partial order} is a subclass of \isa{ordrel}
|
|
36 |
where certain axioms need to hold:%
|
|
37 |
\end{isamarkuptext}%
|
17175
|
38 |
\isamarkuptrue%
|
|
39 |
\isacommand{axclass}\isamarkupfalse%
|
|
40 |
\ parord\ {\isacharless}\ ordrel\isanewline
|
|
41 |
refl{\isacharcolon}\ \ \ \ {\isachardoublequoteopen}x\ {\isacharless}{\isacharless}{\isacharequal}\ x{\isachardoublequoteclose}\isanewline
|
|
42 |
trans{\isacharcolon}\ \ \ {\isachardoublequoteopen}{\isasymlbrakk}\ x\ {\isacharless}{\isacharless}{\isacharequal}\ y{\isacharsemicolon}\ y\ {\isacharless}{\isacharless}{\isacharequal}\ z\ {\isasymrbrakk}\ {\isasymLongrightarrow}\ x\ {\isacharless}{\isacharless}{\isacharequal}\ z{\isachardoublequoteclose}\isanewline
|
|
43 |
antisym{\isacharcolon}\ {\isachardoublequoteopen}{\isasymlbrakk}\ x\ {\isacharless}{\isacharless}{\isacharequal}\ y{\isacharsemicolon}\ y\ {\isacharless}{\isacharless}{\isacharequal}\ x\ {\isasymrbrakk}\ {\isasymLongrightarrow}\ x\ {\isacharequal}\ y{\isachardoublequoteclose}\isanewline
|
19288
|
44 |
lt{\isacharunderscore}le{\isacharcolon}\ \ \ {\isachardoublequoteopen}x\ {\isacharless}{\isacharless}\ y\ {\isacharequal}\ {\isacharparenleft}x\ {\isacharless}{\isacharless}{\isacharequal}\ y\ {\isasymand}\ x\ {\isasymnoteq}\ y{\isacharparenright}{\isachardoublequoteclose}%
|
10328
|
45 |
\begin{isamarkuptext}%
|
|
46 |
\noindent
|
|
47 |
The first three axioms are the familiar ones, and the final one
|
|
48 |
requires that \isa{{\isacharless}{\isacharless}} and \isa{{\isacharless}{\isacharless}{\isacharequal}} are related as expected.
|
|
49 |
Note that behind the scenes, Isabelle has restricted the axioms to class
|
11494
|
50 |
\isa{parord}. For example, the axiom \isa{refl} really is
|
10878
|
51 |
\isa{{\isacharparenleft}{\isacharquery}x{\isasymColon}{\isacharquery}{\isacharprime}a{\isasymColon}parord{\isacharparenright}\ {\isacharless}{\isacharless}{\isacharequal}\ {\isacharquery}x}.
|
10328
|
52 |
|
19288
|
53 |
We have not made \isa{lt{\isacharunderscore}le} a global definition because it would
|
11196
|
54 |
fix once and for all that \isa{{\isacharless}{\isacharless}} is defined in terms of \isa{{\isacharless}{\isacharless}{\isacharequal}} and
|
|
55 |
never the other way around. Below you will see why we want to avoid this
|
11494
|
56 |
asymmetry. The drawback of our choice is that
|
10420
|
57 |
we need to define both \isa{{\isacharless}{\isacharless}{\isacharequal}} and \isa{{\isacharless}{\isacharless}} for each instance.
|
|
58 |
|
10328
|
59 |
We can now prove simple theorems in this abstract setting, for example
|
|
60 |
that \isa{{\isacharless}{\isacharless}} is not symmetric:%
|
|
61 |
\end{isamarkuptext}%
|
17175
|
62 |
\isamarkuptrue%
|
|
63 |
\isacommand{lemma}\isamarkupfalse%
|
|
64 |
\ {\isacharbrackleft}simp{\isacharbrackright}{\isacharcolon}\ {\isachardoublequoteopen}{\isacharparenleft}x{\isacharcolon}{\isacharcolon}{\isacharprime}a{\isacharcolon}{\isacharcolon}parord{\isacharparenright}\ {\isacharless}{\isacharless}\ y\ {\isasymLongrightarrow}\ {\isacharparenleft}{\isasymnot}\ y\ {\isacharless}{\isacharless}\ x{\isacharparenright}\ {\isacharequal}\ True{\isachardoublequoteclose}%
|
17056
|
65 |
\isadelimproof
|
|
66 |
%
|
|
67 |
\endisadelimproof
|
|
68 |
%
|
|
69 |
\isatagproof
|
16353
|
70 |
%
|
|
71 |
\begin{isamarkuptxt}%
|
|
72 |
\noindent
|
|
73 |
The conclusion is not just \isa{{\isasymnot}\ y\ {\isacharless}{\isacharless}\ x} because the
|
|
74 |
simplifier's preprocessor (see \S\ref{sec:simp-preprocessor})
|
|
75 |
would turn it into \isa{{\isacharparenleft}y\ {\isacharless}{\isacharless}\ x{\isacharparenright}\ {\isacharequal}\ False}, yielding
|
|
76 |
a nonterminating rewrite rule.
|
|
77 |
(It would be used to try to prove its own precondition \emph{ad
|
|
78 |
infinitum}.)
|
|
79 |
In the form above, the rule is useful.
|
|
80 |
The type constraint is necessary because otherwise Isabelle would only assume
|
|
81 |
\isa{{\isacharprime}a{\isacharcolon}{\isacharcolon}ordrel} (as required in the type of \isa{{\isacharless}{\isacharless}}),
|
|
82 |
when the proposition is not a theorem. The proof is easy:%
|
|
83 |
\end{isamarkuptxt}%
|
17175
|
84 |
\isamarkuptrue%
|
|
85 |
\isacommand{by}\isamarkupfalse%
|
19288
|
86 |
{\isacharparenleft}simp\ add{\isacharcolon}\ lt{\isacharunderscore}le\ antisym{\isacharparenright}%
|
17056
|
87 |
\endisatagproof
|
|
88 |
{\isafoldproof}%
|
|
89 |
%
|
|
90 |
\isadelimproof
|
|
91 |
%
|
|
92 |
\endisadelimproof
|
11866
|
93 |
%
|
10328
|
94 |
\begin{isamarkuptext}%
|
|
95 |
We could now continue in this vein and develop a whole theory of
|
|
96 |
results about partial orders. Eventually we will want to apply these results
|
|
97 |
to concrete types, namely the instances of the class. Thus we first need to
|
|
98 |
prove that the types in question, for example \isa{bool}, are indeed
|
|
99 |
instances of \isa{parord}:%
|
|
100 |
\end{isamarkuptext}%
|
17175
|
101 |
\isamarkuptrue%
|
|
102 |
\isacommand{instance}\isamarkupfalse%
|
|
103 |
\ bool\ {\isacharcolon}{\isacharcolon}\ parord\isanewline
|
17056
|
104 |
%
|
|
105 |
\isadelimproof
|
|
106 |
%
|
|
107 |
\endisadelimproof
|
|
108 |
%
|
|
109 |
\isatagproof
|
17175
|
110 |
\isacommand{apply}\isamarkupfalse%
|
|
111 |
\ intro{\isacharunderscore}classes%
|
16353
|
112 |
\begin{isamarkuptxt}%
|
|
113 |
\noindent
|
|
114 |
This time \isa{intro{\isacharunderscore}classes} leaves us with the four axioms,
|
|
115 |
specialized to type \isa{bool}, as subgoals:
|
|
116 |
\begin{isabelle}%
|
|
117 |
\ {\isadigit{1}}{\isachardot}\ {\isasymAnd}x{\isasymColon}bool{\isachardot}\ x\ {\isacharless}{\isacharless}{\isacharequal}\ x\isanewline
|
|
118 |
\ {\isadigit{2}}{\isachardot}\ {\isasymAnd}{\isacharparenleft}x{\isasymColon}bool{\isacharparenright}\ {\isacharparenleft}y{\isasymColon}bool{\isacharparenright}\ z{\isasymColon}bool{\isachardot}\ {\isasymlbrakk}x\ {\isacharless}{\isacharless}{\isacharequal}\ y{\isacharsemicolon}\ y\ {\isacharless}{\isacharless}{\isacharequal}\ z{\isasymrbrakk}\ {\isasymLongrightarrow}\ x\ {\isacharless}{\isacharless}{\isacharequal}\ z\isanewline
|
|
119 |
\ {\isadigit{3}}{\isachardot}\ {\isasymAnd}{\isacharparenleft}x{\isasymColon}bool{\isacharparenright}\ y{\isasymColon}bool{\isachardot}\ {\isasymlbrakk}x\ {\isacharless}{\isacharless}{\isacharequal}\ y{\isacharsemicolon}\ y\ {\isacharless}{\isacharless}{\isacharequal}\ x{\isasymrbrakk}\ {\isasymLongrightarrow}\ x\ {\isacharequal}\ y\isanewline
|
|
120 |
\ {\isadigit{4}}{\isachardot}\ {\isasymAnd}{\isacharparenleft}x{\isasymColon}bool{\isacharparenright}\ y{\isasymColon}bool{\isachardot}\ {\isacharparenleft}x\ {\isacharless}{\isacharless}\ y{\isacharparenright}\ {\isacharequal}\ {\isacharparenleft}x\ {\isacharless}{\isacharless}{\isacharequal}\ y\ {\isasymand}\ x\ {\isasymnoteq}\ y{\isacharparenright}%
|
|
121 |
\end{isabelle}
|
|
122 |
Fortunately, the proof is easy for \isa{blast}
|
|
123 |
once we have unfolded the definitions
|
|
124 |
of \isa{{\isacharless}{\isacharless}} and \isa{{\isacharless}{\isacharless}{\isacharequal}} at type \isa{bool}:%
|
|
125 |
\end{isamarkuptxt}%
|
17175
|
126 |
\isamarkuptrue%
|
|
127 |
\isacommand{apply}\isamarkupfalse%
|
19288
|
128 |
{\isacharparenleft}simp{\isacharunderscore}all\ {\isacharparenleft}no{\isacharunderscore}asm{\isacharunderscore}use{\isacharparenright}\ only{\isacharcolon}\ le{\isacharunderscore}bool{\isacharunderscore}def\ lt{\isacharunderscore}bool{\isacharunderscore}def{\isacharparenright}\isanewline
|
17175
|
129 |
\isacommand{by}\isamarkupfalse%
|
|
130 |
{\isacharparenleft}blast{\isacharcomma}\ blast{\isacharcomma}\ blast{\isacharcomma}\ blast{\isacharparenright}%
|
17056
|
131 |
\endisatagproof
|
|
132 |
{\isafoldproof}%
|
|
133 |
%
|
|
134 |
\isadelimproof
|
|
135 |
%
|
|
136 |
\endisadelimproof
|
11866
|
137 |
%
|
10328
|
138 |
\begin{isamarkuptext}%
|
|
139 |
\noindent
|
|
140 |
Can you figure out why we have to include \isa{{\isacharparenleft}no{\isacharunderscore}asm{\isacharunderscore}use{\isacharparenright}}?
|
|
141 |
|
|
142 |
We can now apply our single lemma above in the context of booleans:%
|
|
143 |
\end{isamarkuptext}%
|
17175
|
144 |
\isamarkuptrue%
|
|
145 |
\isacommand{lemma}\isamarkupfalse%
|
|
146 |
\ {\isachardoublequoteopen}{\isacharparenleft}P{\isacharcolon}{\isacharcolon}bool{\isacharparenright}\ {\isacharless}{\isacharless}\ Q\ {\isasymLongrightarrow}\ {\isasymnot}{\isacharparenleft}Q\ {\isacharless}{\isacharless}\ P{\isacharparenright}{\isachardoublequoteclose}\isanewline
|
17056
|
147 |
%
|
|
148 |
\isadelimproof
|
|
149 |
%
|
|
150 |
\endisadelimproof
|
|
151 |
%
|
|
152 |
\isatagproof
|
17175
|
153 |
\isacommand{by}\isamarkupfalse%
|
|
154 |
\ simp%
|
17056
|
155 |
\endisatagproof
|
|
156 |
{\isafoldproof}%
|
|
157 |
%
|
|
158 |
\isadelimproof
|
|
159 |
%
|
|
160 |
\endisadelimproof
|
11866
|
161 |
%
|
10328
|
162 |
\begin{isamarkuptext}%
|
|
163 |
\noindent
|
10878
|
164 |
The effect is not stunning, but it demonstrates the principle. It also shows
|
11494
|
165 |
that tools like the simplifier can deal with generic rules.
|
|
166 |
The main advantage of the axiomatic method is that
|
|
167 |
theorems can be proved in the abstract and freely reused for each instance.%
|
10328
|
168 |
\end{isamarkuptext}%
|
11866
|
169 |
\isamarkuptrue%
|
10328
|
170 |
%
|
10878
|
171 |
\isamarkupsubsubsection{Linear Orders%
|
10397
|
172 |
}
|
11866
|
173 |
\isamarkuptrue%
|
10328
|
174 |
%
|
|
175 |
\begin{isamarkuptext}%
|
|
176 |
If any two elements of a partial order are comparable it is a
|
11494
|
177 |
\textbf{linear} or \textbf{total} order:%
|
10328
|
178 |
\end{isamarkuptext}%
|
17175
|
179 |
\isamarkuptrue%
|
|
180 |
\isacommand{axclass}\isamarkupfalse%
|
|
181 |
\ linord\ {\isacharless}\ parord\isanewline
|
|
182 |
linear{\isacharcolon}\ {\isachardoublequoteopen}x\ {\isacharless}{\isacharless}{\isacharequal}\ y\ {\isasymor}\ y\ {\isacharless}{\isacharless}{\isacharequal}\ x{\isachardoublequoteclose}%
|
10328
|
183 |
\begin{isamarkuptext}%
|
|
184 |
\noindent
|
|
185 |
By construction, \isa{linord} inherits all axioms from \isa{parord}.
|
11196
|
186 |
Therefore we can show that linearity can be expressed in terms of \isa{{\isacharless}{\isacharless}}
|
10328
|
187 |
as follows:%
|
|
188 |
\end{isamarkuptext}%
|
17175
|
189 |
\isamarkuptrue%
|
|
190 |
\isacommand{lemma}\isamarkupfalse%
|
|
191 |
\ {\isachardoublequoteopen}{\isasymAnd}x{\isacharcolon}{\isacharcolon}{\isacharprime}a{\isacharcolon}{\isacharcolon}linord{\isachardot}\ x\ {\isacharless}{\isacharless}\ y\ {\isasymor}\ x\ {\isacharequal}\ y\ {\isasymor}\ y\ {\isacharless}{\isacharless}\ x{\isachardoublequoteclose}\isanewline
|
17056
|
192 |
%
|
|
193 |
\isadelimproof
|
|
194 |
%
|
|
195 |
\endisadelimproof
|
|
196 |
%
|
|
197 |
\isatagproof
|
17175
|
198 |
\isacommand{apply}\isamarkupfalse%
|
19288
|
199 |
{\isacharparenleft}simp\ add{\isacharcolon}\ lt{\isacharunderscore}le{\isacharparenright}\isanewline
|
17175
|
200 |
\isacommand{apply}\isamarkupfalse%
|
|
201 |
{\isacharparenleft}insert\ linear{\isacharparenright}\isanewline
|
|
202 |
\isacommand{apply}\isamarkupfalse%
|
|
203 |
\ blast\isanewline
|
|
204 |
\isacommand{done}\isamarkupfalse%
|
|
205 |
%
|
17056
|
206 |
\endisatagproof
|
|
207 |
{\isafoldproof}%
|
|
208 |
%
|
|
209 |
\isadelimproof
|
|
210 |
%
|
|
211 |
\endisadelimproof
|
11866
|
212 |
%
|
10328
|
213 |
\begin{isamarkuptext}%
|
11494
|
214 |
Linear orders are an example of subclassing\index{subclasses}
|
|
215 |
by construction, which is the most
|
|
216 |
common case. Subclass relationships can also be proved.
|
|
217 |
This is the topic of the following
|
10654
|
218 |
paragraph.%
|
10328
|
219 |
\end{isamarkuptext}%
|
11866
|
220 |
\isamarkuptrue%
|
10328
|
221 |
%
|
10878
|
222 |
\isamarkupsubsubsection{Strict Orders%
|
10397
|
223 |
}
|
11866
|
224 |
\isamarkuptrue%
|
10328
|
225 |
%
|
|
226 |
\begin{isamarkuptext}%
|
|
227 |
An alternative axiomatization of partial orders takes \isa{{\isacharless}{\isacharless}} rather than
|
11494
|
228 |
\isa{{\isacharless}{\isacharless}{\isacharequal}} as the primary concept. The result is a \textbf{strict} order:%
|
10328
|
229 |
\end{isamarkuptext}%
|
17175
|
230 |
\isamarkuptrue%
|
|
231 |
\isacommand{axclass}\isamarkupfalse%
|
|
232 |
\ strord\ {\isacharless}\ ordrel\isanewline
|
|
233 |
irrefl{\isacharcolon}\ \ \ \ \ {\isachardoublequoteopen}{\isasymnot}\ x\ {\isacharless}{\isacharless}\ x{\isachardoublequoteclose}\isanewline
|
19288
|
234 |
lt{\isacharunderscore}trans{\isacharcolon}\ \ \ {\isachardoublequoteopen}{\isasymlbrakk}\ x\ {\isacharless}{\isacharless}\ y{\isacharsemicolon}\ y\ {\isacharless}{\isacharless}\ z\ {\isasymrbrakk}\ {\isasymLongrightarrow}\ x\ {\isacharless}{\isacharless}\ z{\isachardoublequoteclose}\isanewline
|
17175
|
235 |
le{\isacharunderscore}less{\isacharcolon}\ \ \ \ {\isachardoublequoteopen}x\ {\isacharless}{\isacharless}{\isacharequal}\ y\ {\isacharequal}\ {\isacharparenleft}x\ {\isacharless}{\isacharless}\ y\ {\isasymor}\ x\ {\isacharequal}\ y{\isacharparenright}{\isachardoublequoteclose}%
|
10328
|
236 |
\begin{isamarkuptext}%
|
|
237 |
\noindent
|
|
238 |
It is well known that partial orders are the same as strict orders. Let us
|
|
239 |
prove one direction, namely that partial orders are a subclass of strict
|
11196
|
240 |
orders.%
|
10328
|
241 |
\end{isamarkuptext}%
|
17175
|
242 |
\isamarkuptrue%
|
|
243 |
\isacommand{instance}\isamarkupfalse%
|
|
244 |
\ parord\ {\isacharless}\ strord\isanewline
|
17056
|
245 |
%
|
|
246 |
\isadelimproof
|
|
247 |
%
|
|
248 |
\endisadelimproof
|
|
249 |
%
|
|
250 |
\isatagproof
|
17175
|
251 |
\isacommand{apply}\isamarkupfalse%
|
|
252 |
\ intro{\isacharunderscore}classes%
|
16353
|
253 |
\begin{isamarkuptxt}%
|
|
254 |
\noindent
|
|
255 |
\begin{isabelle}%
|
|
256 |
\ {\isadigit{1}}{\isachardot}\ {\isasymAnd}x{\isasymColon}{\isacharprime}a{\isachardot}\ {\isasymnot}\ x\ {\isacharless}{\isacharless}\ x\isanewline
|
|
257 |
\ {\isadigit{2}}{\isachardot}\ {\isasymAnd}{\isacharparenleft}x{\isasymColon}{\isacharprime}a{\isacharparenright}\ {\isacharparenleft}y{\isasymColon}{\isacharprime}a{\isacharparenright}\ z{\isasymColon}{\isacharprime}a{\isachardot}\ {\isasymlbrakk}x\ {\isacharless}{\isacharless}\ y{\isacharsemicolon}\ y\ {\isacharless}{\isacharless}\ z{\isasymrbrakk}\ {\isasymLongrightarrow}\ x\ {\isacharless}{\isacharless}\ z\isanewline
|
|
258 |
\ {\isadigit{3}}{\isachardot}\ {\isasymAnd}{\isacharparenleft}x{\isasymColon}{\isacharprime}a{\isacharparenright}\ y{\isasymColon}{\isacharprime}a{\isachardot}\ {\isacharparenleft}x\ {\isacharless}{\isacharless}{\isacharequal}\ y{\isacharparenright}\ {\isacharequal}\ {\isacharparenleft}x\ {\isacharless}{\isacharless}\ y\ {\isasymor}\ x\ {\isacharequal}\ y{\isacharparenright}\isanewline
|
|
259 |
type\ variables{\isacharcolon}\isanewline
|
|
260 |
\isaindent{\ \ }{\isacharprime}a\ {\isacharcolon}{\isacharcolon}\ parord%
|
|
261 |
\end{isabelle}
|
27027
|
262 |
Because of \isa{{\isacharprime}a\ {\isacharcolon}{\isacharcolon}\ parord}, the three axioms of class \isa{strord}
|
16353
|
263 |
are easily proved:%
|
|
264 |
\end{isamarkuptxt}%
|
17175
|
265 |
\isamarkuptrue%
|
|
266 |
\ \ \isacommand{apply}\isamarkupfalse%
|
19288
|
267 |
{\isacharparenleft}simp{\isacharunderscore}all\ {\isacharparenleft}no{\isacharunderscore}asm{\isacharunderscore}use{\isacharparenright}\ add{\isacharcolon}\ lt{\isacharunderscore}le{\isacharparenright}\isanewline
|
17175
|
268 |
\ \isacommand{apply}\isamarkupfalse%
|
|
269 |
{\isacharparenleft}blast\ intro{\isacharcolon}\ trans\ antisym{\isacharparenright}\isanewline
|
|
270 |
\isacommand{apply}\isamarkupfalse%
|
|
271 |
{\isacharparenleft}blast\ intro{\isacharcolon}\ refl{\isacharparenright}\isanewline
|
|
272 |
\isacommand{done}\isamarkupfalse%
|
|
273 |
%
|
17056
|
274 |
\endisatagproof
|
|
275 |
{\isafoldproof}%
|
|
276 |
%
|
|
277 |
\isadelimproof
|
|
278 |
%
|
|
279 |
\endisadelimproof
|
11866
|
280 |
%
|
10328
|
281 |
\begin{isamarkuptext}%
|
10396
|
282 |
The subclass relation must always be acyclic. Therefore Isabelle will
|
|
283 |
complain if you also prove the relationship \isa{strord\ {\isacharless}\ parord}.%
|
|
284 |
\end{isamarkuptext}%
|
11866
|
285 |
\isamarkuptrue%
|
10396
|
286 |
%
|
10878
|
287 |
\isamarkupsubsubsection{Multiple Inheritance and Sorts%
|
10397
|
288 |
}
|
11866
|
289 |
\isamarkuptrue%
|
10396
|
290 |
%
|
|
291 |
\begin{isamarkuptext}%
|
|
292 |
A class may inherit from more than one direct superclass. This is called
|
11494
|
293 |
\bfindex{multiple inheritance}. For example, we could define
|
10396
|
294 |
the classes of well-founded orderings and well-orderings:%
|
|
295 |
\end{isamarkuptext}%
|
17175
|
296 |
\isamarkuptrue%
|
|
297 |
\isacommand{axclass}\isamarkupfalse%
|
|
298 |
\ wford\ {\isacharless}\ parord\isanewline
|
|
299 |
wford{\isacharcolon}\ {\isachardoublequoteopen}wf\ {\isacharbraceleft}{\isacharparenleft}y{\isacharcomma}x{\isacharparenright}{\isachardot}\ y\ {\isacharless}{\isacharless}\ x{\isacharbraceright}{\isachardoublequoteclose}\isanewline
|
10396
|
300 |
\isanewline
|
17175
|
301 |
\isacommand{axclass}\isamarkupfalse%
|
|
302 |
\ wellord\ {\isacharless}\ linord{\isacharcomma}\ wford%
|
10396
|
303 |
\begin{isamarkuptext}%
|
10328
|
304 |
\noindent
|
10396
|
305 |
The last line expresses the usual definition: a well-ordering is a linear
|
|
306 |
well-founded ordering. The result is the subclass diagram in
|
|
307 |
Figure~\ref{fig:subclass}.
|
|
308 |
|
|
309 |
\begin{figure}[htbp]
|
10328
|
310 |
\[
|
10396
|
311 |
\begin{array}{r@ {}r@ {}c@ {}l@ {}l}
|
12815
|
312 |
& & \isa{type}\\
|
10396
|
313 |
& & |\\
|
|
314 |
& & \isa{ordrel}\\
|
|
315 |
& & |\\
|
|
316 |
& & \isa{strord}\\
|
|
317 |
& & |\\
|
|
318 |
& & \isa{parord} \\
|
|
319 |
& / & & \backslash \\
|
|
320 |
\isa{linord} & & & & \isa{wford} \\
|
|
321 |
& \backslash & & / \\
|
|
322 |
& & \isa{wellord}
|
10328
|
323 |
\end{array}
|
|
324 |
\]
|
10878
|
325 |
\caption{Subclass Diagram}
|
10396
|
326 |
\label{fig:subclass}
|
|
327 |
\end{figure}
|
10328
|
328 |
|
10396
|
329 |
Since class \isa{wellord} does not introduce any new axioms, it can simply
|
|
330 |
be viewed as the intersection of the two classes \isa{linord} and \isa{wford}. Such intersections need not be given a new name but can be created on
|
|
331 |
the fly: the expression $\{C@1,\dots,C@n\}$, where the $C@i$ are classes,
|
|
332 |
represents the intersection of the $C@i$. Such an expression is called a
|
11428
|
333 |
\textbf{sort},\index{sorts} and sorts can appear in most places where we have only shown
|
10396
|
334 |
classes so far, for example in type constraints: \isa{{\isacharprime}a{\isacharcolon}{\isacharcolon}{\isacharbraceleft}linord{\isacharcomma}wford{\isacharbraceright}}.
|
11196
|
335 |
In fact, \isa{{\isacharprime}a{\isacharcolon}{\isacharcolon}C} is short for \isa{{\isacharprime}a{\isacharcolon}{\isacharcolon}{\isacharbraceleft}C{\isacharbraceright}}.
|
10396
|
336 |
However, we do not pursue this rarefied concept further.
|
10328
|
337 |
|
10396
|
338 |
This concludes our demonstration of type classes based on orderings. We
|
|
339 |
remind our readers that \isa{Main} contains a theory of
|
10328
|
340 |
orderings phrased in terms of the usual \isa{{\isasymle}} and \isa{{\isacharless}}.
|
11494
|
341 |
If possible, base your own ordering relations on this theory.%
|
10328
|
342 |
\end{isamarkuptext}%
|
11866
|
343 |
\isamarkuptrue%
|
10328
|
344 |
%
|
10397
|
345 |
\isamarkupsubsubsection{Inconsistencies%
|
|
346 |
}
|
11866
|
347 |
\isamarkuptrue%
|
10328
|
348 |
%
|
|
349 |
\begin{isamarkuptext}%
|
11494
|
350 |
The reader may be wondering what happens if we
|
10328
|
351 |
attach an inconsistent set of axioms to a class. So far we have always
|
|
352 |
avoided to add new axioms to HOL for fear of inconsistencies and suddenly it
|
|
353 |
seems that we are throwing all caution to the wind. So why is there no
|
|
354 |
problem?
|
|
355 |
|
|
356 |
The point is that by construction, all type variables in the axioms of an
|
|
357 |
\isacommand{axclass} are automatically constrained with the class being
|
|
358 |
defined (as shown for axiom \isa{refl} above). These constraints are
|
|
359 |
always carried around and Isabelle takes care that they are never lost,
|
|
360 |
unless the type variable is instantiated with a type that has been shown to
|
|
361 |
belong to that class. Thus you may be able to prove \isa{False}
|
|
362 |
from your axioms, but Isabelle will remind you that this
|
12332
|
363 |
theorem has the hidden hypothesis that the class is non-empty.
|
|
364 |
|
|
365 |
Even if each individual class is consistent, intersections of (unrelated)
|
|
366 |
classes readily become inconsistent in practice. Now we know this need not
|
|
367 |
worry us.%
|
10328
|
368 |
\end{isamarkuptext}%
|
17175
|
369 |
\isamarkuptrue%
|
17056
|
370 |
%
|
|
371 |
\isadelimtheory
|
|
372 |
%
|
|
373 |
\endisadelimtheory
|
|
374 |
%
|
|
375 |
\isatagtheory
|
|
376 |
%
|
|
377 |
\endisatagtheory
|
|
378 |
{\isafoldtheory}%
|
|
379 |
%
|
|
380 |
\isadelimtheory
|
|
381 |
%
|
|
382 |
\endisadelimtheory
|
10328
|
383 |
\end{isabellebody}%
|
|
384 |
%%% Local Variables:
|
|
385 |
%%% mode: latex
|
|
386 |
%%% TeX-master: "root"
|
|
387 |
%%% End:
|