10328
|
1 |
(*<*)theory Axioms = Overloading:(*>*)
|
|
2 |
|
|
3 |
subsection{*Axioms*}
|
|
4 |
|
|
5 |
|
|
6 |
text{*Now we want to attach axioms to our classes. Then we can reason on the
|
|
7 |
level of classes and the results will be applicable to all types in a class,
|
|
8 |
just as in axiomatic mathematics. These ideas are demonstrated by means of
|
|
9 |
our above ordering relations.
|
|
10 |
*}
|
|
11 |
|
10885
|
12 |
subsubsection{*Partial Orders*}
|
10328
|
13 |
|
|
14 |
text{*
|
|
15 |
A \emph{partial order} is a subclass of @{text ordrel}
|
|
16 |
where certain axioms need to hold:
|
|
17 |
*}
|
|
18 |
|
|
19 |
axclass parord < ordrel
|
|
20 |
refl: "x <<= x"
|
|
21 |
trans: "\<lbrakk> x <<= y; y <<= z \<rbrakk> \<Longrightarrow> x <<= z"
|
|
22 |
antisym: "\<lbrakk> x <<= y; y <<= x \<rbrakk> \<Longrightarrow> x = y"
|
|
23 |
less_le: "x << y = (x <<= y \<and> x \<noteq> y)"
|
|
24 |
|
|
25 |
text{*\noindent
|
|
26 |
The first three axioms are the familiar ones, and the final one
|
|
27 |
requires that @{text"<<"} and @{text"<<="} are related as expected.
|
|
28 |
Note that behind the scenes, Isabelle has restricted the axioms to class
|
|
29 |
@{text parord}. For example, this is what @{thm[source]refl} really looks like:
|
10885
|
30 |
@{thm[show_sorts]refl}.
|
10328
|
31 |
|
10420
|
32 |
We have not made @{thm[source]less_le} a global definition because it would
|
11196
|
33 |
fix once and for all that @{text"<<"} is defined in terms of @{text"<<="} and
|
|
34 |
never the other way around. Below you will see why we want to avoid this
|
|
35 |
asymmetry. The drawback of the above class is that
|
10420
|
36 |
we need to define both @{text"<<="} and @{text"<<"} for each instance.
|
|
37 |
|
10328
|
38 |
We can now prove simple theorems in this abstract setting, for example
|
|
39 |
that @{text"<<"} is not symmetric:
|
|
40 |
*}
|
|
41 |
|
|
42 |
lemma [simp]: "(x::'a::parord) << y \<Longrightarrow> (\<not> y << x) = True";
|
|
43 |
|
|
44 |
txt{*\noindent
|
|
45 |
The conclusion is not simply @{prop"\<not> y << x"} because the preprocessor
|
10845
|
46 |
of the simplifier (see \S\ref{sec:simp-preprocessor})
|
|
47 |
would turn this into @{prop"y << x = False"}, thus yielding
|
10328
|
48 |
a nonterminating rewrite rule. In the above form it is a generally useful
|
|
49 |
rule.
|
|
50 |
The type constraint is necessary because otherwise Isabelle would only assume
|
|
51 |
@{text"'a::ordrel"} (as required in the type of @{text"<<"}), in
|
|
52 |
which case the proposition is not a theorem. The proof is easy:
|
|
53 |
*}
|
|
54 |
|
|
55 |
by(simp add:less_le antisym);
|
|
56 |
|
|
57 |
text{* We could now continue in this vein and develop a whole theory of
|
|
58 |
results about partial orders. Eventually we will want to apply these results
|
|
59 |
to concrete types, namely the instances of the class. Thus we first need to
|
|
60 |
prove that the types in question, for example @{typ bool}, are indeed
|
|
61 |
instances of @{text parord}:*}
|
|
62 |
|
|
63 |
instance bool :: parord
|
|
64 |
apply intro_classes;
|
|
65 |
|
|
66 |
txt{*\noindent
|
|
67 |
This time @{text intro_classes} leaves us with the four axioms,
|
|
68 |
specialized to type @{typ bool}, as subgoals:
|
10362
|
69 |
@{subgoals[display,show_types,indent=0]}
|
10328
|
70 |
Fortunately, the proof is easy for blast, once we have unfolded the definitions
|
|
71 |
of @{text"<<"} and @{text"<<="} at @{typ bool}:
|
|
72 |
*}
|
|
73 |
|
|
74 |
apply(simp_all (no_asm_use) only: le_bool_def less_bool_def);
|
|
75 |
by(blast, blast, blast, blast);
|
|
76 |
|
|
77 |
text{*\noindent
|
|
78 |
Can you figure out why we have to include @{text"(no_asm_use)"}?
|
|
79 |
|
|
80 |
We can now apply our single lemma above in the context of booleans:
|
|
81 |
*}
|
|
82 |
|
|
83 |
lemma "(P::bool) << Q \<Longrightarrow> \<not>(Q << P)";
|
|
84 |
by simp;
|
|
85 |
|
|
86 |
text{*\noindent
|
10885
|
87 |
The effect is not stunning, but it demonstrates the principle. It also shows
|
11196
|
88 |
that tools like the simplifier can deal with generic rules as well.
|
|
89 |
It should be clear that the main advantage of the axiomatic method is that
|
10328
|
90 |
theorems can be proved in the abstract and one does not need to repeat the
|
|
91 |
proof for each instance.
|
|
92 |
*}
|
|
93 |
|
10885
|
94 |
subsubsection{*Linear Orders*}
|
10328
|
95 |
|
|
96 |
text{* If any two elements of a partial order are comparable it is a
|
|
97 |
\emph{linear} or \emph{total} order: *}
|
|
98 |
|
|
99 |
axclass linord < parord
|
11196
|
100 |
linear: "x <<= y \<or> y <<= x"
|
10328
|
101 |
|
|
102 |
text{*\noindent
|
|
103 |
By construction, @{text linord} inherits all axioms from @{text parord}.
|
11196
|
104 |
Therefore we can show that linearity can be expressed in terms of @{text"<<"}
|
10328
|
105 |
as follows:
|
|
106 |
*}
|
|
107 |
|
11196
|
108 |
lemma "\<And>x::'a::linord. x << y \<or> x = y \<or> y << x";
|
10328
|
109 |
apply(simp add: less_le);
|
11196
|
110 |
apply(insert linear);
|
10328
|
111 |
apply blast;
|
|
112 |
done
|
|
113 |
|
|
114 |
text{*
|
|
115 |
Linear orders are an example of subclassing by construction, which is the most
|
|
116 |
common case. It is also possible to prove additional subclass relationships
|
|
117 |
later on, i.e.\ subclassing by proof. This is the topic of the following
|
10654
|
118 |
paragraph.
|
10328
|
119 |
*}
|
|
120 |
|
10885
|
121 |
subsubsection{*Strict Orders*}
|
10328
|
122 |
|
|
123 |
text{*
|
|
124 |
An alternative axiomatization of partial orders takes @{text"<<"} rather than
|
|
125 |
@{text"<<="} as the primary concept. The result is a \emph{strict} order:
|
|
126 |
*}
|
|
127 |
|
|
128 |
axclass strord < ordrel
|
|
129 |
irrefl: "\<not> x << x"
|
|
130 |
less_trans: "\<lbrakk> x << y; y << z \<rbrakk> \<Longrightarrow> x << z"
|
|
131 |
le_less: "x <<= y = (x << y \<or> x = y)"
|
|
132 |
|
|
133 |
text{*\noindent
|
|
134 |
It is well known that partial orders are the same as strict orders. Let us
|
|
135 |
prove one direction, namely that partial orders are a subclass of strict
|
11196
|
136 |
orders. *}
|
10328
|
137 |
|
|
138 |
instance parord < strord
|
|
139 |
apply intro_classes;
|
11196
|
140 |
|
|
141 |
txt{*\noindent
|
|
142 |
@{subgoals[display,show_sorts]}
|
|
143 |
Assuming @{text"'a :: parord"}, the three axioms of class @{text strord}
|
|
144 |
are easily proved:
|
|
145 |
*}
|
|
146 |
|
|
147 |
apply(simp_all (no_asm_use) add:less_le);
|
|
148 |
apply(blast intro: trans antisym);
|
|
149 |
apply(blast intro: refl);
|
10328
|
150 |
done
|
|
151 |
|
10396
|
152 |
text{*
|
|
153 |
The subclass relation must always be acyclic. Therefore Isabelle will
|
|
154 |
complain if you also prove the relationship @{text"strord < parord"}.
|
|
155 |
*}
|
10328
|
156 |
|
|
157 |
|
|
158 |
(*
|
|
159 |
instance strord < parord
|
|
160 |
apply intro_classes;
|
|
161 |
apply(simp_all (no_asm_use) add:le_less);
|
|
162 |
apply(blast intro: less_trans);
|
|
163 |
apply(erule disjE);
|
|
164 |
apply(erule disjE);
|
|
165 |
apply(rule irrefl[THEN notE]);
|
|
166 |
apply(rule less_trans, assumption, assumption);
|
|
167 |
apply blast;apply blast;
|
|
168 |
apply(blast intro: irrefl[THEN notE]);
|
|
169 |
done
|
|
170 |
*)
|
|
171 |
|
10885
|
172 |
subsubsection{*Multiple Inheritance and Sorts*}
|
10396
|
173 |
|
|
174 |
text{*
|
|
175 |
A class may inherit from more than one direct superclass. This is called
|
|
176 |
multiple inheritance and is certainly permitted. For example we could define
|
|
177 |
the classes of well-founded orderings and well-orderings:
|
|
178 |
*}
|
|
179 |
|
|
180 |
axclass wford < parord
|
|
181 |
wford: "wf {(y,x). y << x}"
|
|
182 |
|
|
183 |
axclass wellord < linord, wford
|
|
184 |
|
|
185 |
text{*\noindent
|
|
186 |
The last line expresses the usual definition: a well-ordering is a linear
|
|
187 |
well-founded ordering. The result is the subclass diagram in
|
|
188 |
Figure~\ref{fig:subclass}.
|
|
189 |
|
|
190 |
\begin{figure}[htbp]
|
|
191 |
\[
|
|
192 |
\begin{array}{r@ {}r@ {}c@ {}l@ {}l}
|
|
193 |
& & \isa{term}\\
|
|
194 |
& & |\\
|
|
195 |
& & \isa{ordrel}\\
|
|
196 |
& & |\\
|
|
197 |
& & \isa{strord}\\
|
|
198 |
& & |\\
|
|
199 |
& & \isa{parord} \\
|
|
200 |
& / & & \backslash \\
|
|
201 |
\isa{linord} & & & & \isa{wford} \\
|
|
202 |
& \backslash & & / \\
|
|
203 |
& & \isa{wellord}
|
|
204 |
\end{array}
|
|
205 |
\]
|
10885
|
206 |
\caption{Subclass Diagram}
|
10396
|
207 |
\label{fig:subclass}
|
|
208 |
\end{figure}
|
|
209 |
|
|
210 |
Since class @{text wellord} does not introduce any new axioms, it can simply
|
|
211 |
be viewed as the intersection of the two classes @{text linord} and @{text
|
|
212 |
wford}. Such intersections need not be given a new name but can be created on
|
|
213 |
the fly: the expression $\{C@1,\dots,C@n\}$, where the $C@i$ are classes,
|
|
214 |
represents the intersection of the $C@i$. Such an expression is called a
|
|
215 |
\bfindex{sort}, and sorts can appear in most places where we have only shown
|
|
216 |
classes so far, for example in type constraints: @{text"'a::{linord,wford}"}.
|
11196
|
217 |
In fact, @{text"'a::C"} is short for @{text"'a::{C}"}.
|
10396
|
218 |
However, we do not pursue this rarefied concept further.
|
|
219 |
|
|
220 |
This concludes our demonstration of type classes based on orderings. We
|
|
221 |
remind our readers that \isa{Main} contains a theory of
|
|
222 |
orderings phrased in terms of the usual @{text"\<le>"} and @{text"<"}.
|
|
223 |
It is recommended that, if possible,
|
|
224 |
you base your own ordering relations on this theory.
|
|
225 |
*}
|
|
226 |
|
10328
|
227 |
subsubsection{*Inconsistencies*}
|
|
228 |
|
|
229 |
text{* The reader may be wondering what happens if we, maybe accidentally,
|
|
230 |
attach an inconsistent set of axioms to a class. So far we have always
|
|
231 |
avoided to add new axioms to HOL for fear of inconsistencies and suddenly it
|
|
232 |
seems that we are throwing all caution to the wind. So why is there no
|
|
233 |
problem?
|
|
234 |
|
|
235 |
The point is that by construction, all type variables in the axioms of an
|
|
236 |
\isacommand{axclass} are automatically constrained with the class being
|
|
237 |
defined (as shown for axiom @{thm[source]refl} above). These constraints are
|
|
238 |
always carried around and Isabelle takes care that they are never lost,
|
|
239 |
unless the type variable is instantiated with a type that has been shown to
|
|
240 |
belong to that class. Thus you may be able to prove @{prop False}
|
|
241 |
from your axioms, but Isabelle will remind you that this
|
|
242 |
theorem has the hidden hypothesis that the class is non-empty.
|
|
243 |
*}
|
|
244 |
|
|
245 |
(*
|
|
246 |
axclass false<"term"
|
|
247 |
false: "x \<noteq> x";
|
|
248 |
|
|
249 |
lemma "False";
|
|
250 |
by(rule notE[OF false HOL.refl]);
|
|
251 |
*)
|
|
252 |
(*<*)end(*>*)
|