27 \begin{isamarkuptext}% |
27 \begin{isamarkuptext}% |
28 \noindent |
28 \noindent |
29 The first three axioms are the familiar ones, and the final one |
29 The first three axioms are the familiar ones, and the final one |
30 requires that \isa{{\isacharless}{\isacharless}} and \isa{{\isacharless}{\isacharless}{\isacharequal}} are related as expected. |
30 requires that \isa{{\isacharless}{\isacharless}} and \isa{{\isacharless}{\isacharless}{\isacharequal}} are related as expected. |
31 Note that behind the scenes, Isabelle has restricted the axioms to class |
31 Note that behind the scenes, Isabelle has restricted the axioms to class |
32 \isa{parord}. For example, this is what \isa{refl} really looks like: |
32 \isa{parord}. For example, the axiom \isa{refl} really is |
33 \isa{{\isacharparenleft}{\isacharquery}x{\isasymColon}{\isacharquery}{\isacharprime}a{\isasymColon}parord{\isacharparenright}\ {\isacharless}{\isacharless}{\isacharequal}\ {\isacharquery}x}. |
33 \isa{{\isacharparenleft}{\isacharquery}x{\isasymColon}{\isacharquery}{\isacharprime}a{\isasymColon}parord{\isacharparenright}\ {\isacharless}{\isacharless}{\isacharequal}\ {\isacharquery}x}. |
34 |
34 |
35 We have not made \isa{less{\isacharunderscore}le} a global definition because it would |
35 We have not made \isa{less{\isacharunderscore}le} a global definition because it would |
36 fix once and for all that \isa{{\isacharless}{\isacharless}} is defined in terms of \isa{{\isacharless}{\isacharless}{\isacharequal}} and |
36 fix once and for all that \isa{{\isacharless}{\isacharless}} is defined in terms of \isa{{\isacharless}{\isacharless}{\isacharequal}} and |
37 never the other way around. Below you will see why we want to avoid this |
37 never the other way around. Below you will see why we want to avoid this |
38 asymmetry. The drawback of the above class is that |
38 asymmetry. The drawback of our choice is that |
39 we need to define both \isa{{\isacharless}{\isacharless}{\isacharequal}} and \isa{{\isacharless}{\isacharless}} for each instance. |
39 we need to define both \isa{{\isacharless}{\isacharless}{\isacharequal}} and \isa{{\isacharless}{\isacharless}} for each instance. |
40 |
40 |
41 We can now prove simple theorems in this abstract setting, for example |
41 We can now prove simple theorems in this abstract setting, for example |
42 that \isa{{\isacharless}{\isacharless}} is not symmetric:% |
42 that \isa{{\isacharless}{\isacharless}} is not symmetric:% |
43 \end{isamarkuptext}% |
43 \end{isamarkuptext}% |
44 \isacommand{lemma}\ {\isacharbrackleft}simp{\isacharbrackright}{\isacharcolon}\ {\isachardoublequote}{\isacharparenleft}x{\isacharcolon}{\isacharcolon}{\isacharprime}a{\isacharcolon}{\isacharcolon}parord{\isacharparenright}\ {\isacharless}{\isacharless}\ y\ {\isasymLongrightarrow}\ {\isacharparenleft}{\isasymnot}\ y\ {\isacharless}{\isacharless}\ x{\isacharparenright}\ {\isacharequal}\ True{\isachardoublequote}% |
44 \isacommand{lemma}\ {\isacharbrackleft}simp{\isacharbrackright}{\isacharcolon}\ {\isachardoublequote}{\isacharparenleft}x{\isacharcolon}{\isacharcolon}{\isacharprime}a{\isacharcolon}{\isacharcolon}parord{\isacharparenright}\ {\isacharless}{\isacharless}\ y\ {\isasymLongrightarrow}\ {\isacharparenleft}{\isasymnot}\ y\ {\isacharless}{\isacharless}\ x{\isacharparenright}\ {\isacharequal}\ True{\isachardoublequote}% |
45 \begin{isamarkuptxt}% |
45 \begin{isamarkuptxt}% |
46 \noindent |
46 \noindent |
47 The conclusion is not simply \isa{{\isasymnot}\ y\ {\isacharless}{\isacharless}\ x} because the preprocessor |
47 The conclusion is not just \isa{{\isasymnot}\ y\ {\isacharless}{\isacharless}\ x} because the |
48 of the simplifier (see \S\ref{sec:simp-preprocessor}) |
48 simplifier's preprocessor (see \S\ref{sec:simp-preprocessor}) |
49 would turn this into \isa{{\isacharparenleft}y\ {\isacharless}{\isacharless}\ x{\isacharparenright}\ {\isacharequal}\ False}, thus yielding |
49 would turn it into \isa{{\isacharparenleft}y\ {\isacharless}{\isacharless}\ x{\isacharparenright}\ {\isacharequal}\ False}, yielding |
50 a nonterminating rewrite rule. In the above form it is a generally useful |
50 a nonterminating rewrite rule. |
51 rule. |
51 (It would be used to try to prove its own precondition \emph{ad |
|
52 infinitum}.) |
|
53 In the form above, the rule is useful. |
52 The type constraint is necessary because otherwise Isabelle would only assume |
54 The type constraint is necessary because otherwise Isabelle would only assume |
53 \isa{{\isacharprime}a{\isacharcolon}{\isacharcolon}ordrel} (as required in the type of \isa{{\isacharless}{\isacharless}}), in |
55 \isa{{\isacharprime}a{\isacharcolon}{\isacharcolon}ordrel} (as required in the type of \isa{{\isacharless}{\isacharless}}), |
54 which case the proposition is not a theorem. The proof is easy:% |
56 when the proposition is not a theorem. The proof is easy:% |
55 \end{isamarkuptxt}% |
57 \end{isamarkuptxt}% |
56 \isacommand{by}{\isacharparenleft}simp\ add{\isacharcolon}less{\isacharunderscore}le\ antisym{\isacharparenright}% |
58 \isacommand{by}{\isacharparenleft}simp\ add{\isacharcolon}less{\isacharunderscore}le\ antisym{\isacharparenright}% |
57 \begin{isamarkuptext}% |
59 \begin{isamarkuptext}% |
58 We could now continue in this vein and develop a whole theory of |
60 We could now continue in this vein and develop a whole theory of |
59 results about partial orders. Eventually we will want to apply these results |
61 results about partial orders. Eventually we will want to apply these results |
71 \ {\isadigit{1}}{\isachardot}\ {\isasymAnd}x{\isasymColon}bool{\isachardot}\ x\ {\isacharless}{\isacharless}{\isacharequal}\ x\isanewline |
73 \ {\isadigit{1}}{\isachardot}\ {\isasymAnd}x{\isasymColon}bool{\isachardot}\ x\ {\isacharless}{\isacharless}{\isacharequal}\ x\isanewline |
72 \ {\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 |
74 \ {\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 |
73 \ {\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 |
75 \ {\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 |
74 \ {\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}% |
76 \ {\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}% |
75 \end{isabelle} |
77 \end{isabelle} |
76 Fortunately, the proof is easy for blast, once we have unfolded the definitions |
78 Fortunately, the proof is easy for \isa{blast} |
77 of \isa{{\isacharless}{\isacharless}} and \isa{{\isacharless}{\isacharless}{\isacharequal}} at \isa{bool}:% |
79 once we have unfolded the definitions |
|
80 of \isa{{\isacharless}{\isacharless}} and \isa{{\isacharless}{\isacharless}{\isacharequal}} at type \isa{bool}:% |
78 \end{isamarkuptxt}% |
81 \end{isamarkuptxt}% |
79 \isacommand{apply}{\isacharparenleft}simp{\isacharunderscore}all\ {\isacharparenleft}no{\isacharunderscore}asm{\isacharunderscore}use{\isacharparenright}\ only{\isacharcolon}\ le{\isacharunderscore}bool{\isacharunderscore}def\ less{\isacharunderscore}bool{\isacharunderscore}def{\isacharparenright}\isanewline |
82 \isacommand{apply}{\isacharparenleft}simp{\isacharunderscore}all\ {\isacharparenleft}no{\isacharunderscore}asm{\isacharunderscore}use{\isacharparenright}\ only{\isacharcolon}\ le{\isacharunderscore}bool{\isacharunderscore}def\ less{\isacharunderscore}bool{\isacharunderscore}def{\isacharparenright}\isanewline |
80 \isacommand{by}{\isacharparenleft}blast{\isacharcomma}\ blast{\isacharcomma}\ blast{\isacharcomma}\ blast{\isacharparenright}% |
83 \isacommand{by}{\isacharparenleft}blast{\isacharcomma}\ blast{\isacharcomma}\ blast{\isacharcomma}\ blast{\isacharparenright}% |
81 \begin{isamarkuptext}% |
84 \begin{isamarkuptext}% |
82 \noindent |
85 \noindent |
87 \isacommand{lemma}\ {\isachardoublequote}{\isacharparenleft}P{\isacharcolon}{\isacharcolon}bool{\isacharparenright}\ {\isacharless}{\isacharless}\ Q\ {\isasymLongrightarrow}\ {\isasymnot}{\isacharparenleft}Q\ {\isacharless}{\isacharless}\ P{\isacharparenright}{\isachardoublequote}\isanewline |
90 \isacommand{lemma}\ {\isachardoublequote}{\isacharparenleft}P{\isacharcolon}{\isacharcolon}bool{\isacharparenright}\ {\isacharless}{\isacharless}\ Q\ {\isasymLongrightarrow}\ {\isasymnot}{\isacharparenleft}Q\ {\isacharless}{\isacharless}\ P{\isacharparenright}{\isachardoublequote}\isanewline |
88 \isacommand{by}\ simp% |
91 \isacommand{by}\ simp% |
89 \begin{isamarkuptext}% |
92 \begin{isamarkuptext}% |
90 \noindent |
93 \noindent |
91 The effect is not stunning, but it demonstrates the principle. It also shows |
94 The effect is not stunning, but it demonstrates the principle. It also shows |
92 that tools like the simplifier can deal with generic rules as well. |
95 that tools like the simplifier can deal with generic rules. |
93 It should be clear that the main advantage of the axiomatic method is that |
96 The main advantage of the axiomatic method is that |
94 theorems can be proved in the abstract and one does not need to repeat the |
97 theorems can be proved in the abstract and freely reused for each instance.% |
95 proof for each instance.% |
|
96 \end{isamarkuptext}% |
98 \end{isamarkuptext}% |
97 % |
99 % |
98 \isamarkupsubsubsection{Linear Orders% |
100 \isamarkupsubsubsection{Linear Orders% |
99 } |
101 } |
100 % |
102 % |
101 \begin{isamarkuptext}% |
103 \begin{isamarkuptext}% |
102 If any two elements of a partial order are comparable it is a |
104 If any two elements of a partial order are comparable it is a |
103 \emph{linear} or \emph{total} order:% |
105 \textbf{linear} or \textbf{total} order:% |
104 \end{isamarkuptext}% |
106 \end{isamarkuptext}% |
105 \isacommand{axclass}\ linord\ {\isacharless}\ parord\isanewline |
107 \isacommand{axclass}\ linord\ {\isacharless}\ parord\isanewline |
106 linear{\isacharcolon}\ {\isachardoublequote}x\ {\isacharless}{\isacharless}{\isacharequal}\ y\ {\isasymor}\ y\ {\isacharless}{\isacharless}{\isacharequal}\ x{\isachardoublequote}% |
108 linear{\isacharcolon}\ {\isachardoublequote}x\ {\isacharless}{\isacharless}{\isacharequal}\ y\ {\isasymor}\ y\ {\isacharless}{\isacharless}{\isacharequal}\ x{\isachardoublequote}% |
107 \begin{isamarkuptext}% |
109 \begin{isamarkuptext}% |
108 \noindent |
110 \noindent |
114 \isacommand{apply}{\isacharparenleft}simp\ add{\isacharcolon}\ less{\isacharunderscore}le{\isacharparenright}\isanewline |
116 \isacommand{apply}{\isacharparenleft}simp\ add{\isacharcolon}\ less{\isacharunderscore}le{\isacharparenright}\isanewline |
115 \isacommand{apply}{\isacharparenleft}insert\ linear{\isacharparenright}\isanewline |
117 \isacommand{apply}{\isacharparenleft}insert\ linear{\isacharparenright}\isanewline |
116 \isacommand{apply}\ blast\isanewline |
118 \isacommand{apply}\ blast\isanewline |
117 \isacommand{done}% |
119 \isacommand{done}% |
118 \begin{isamarkuptext}% |
120 \begin{isamarkuptext}% |
119 Linear orders are an example of subclassing by construction, which is the most |
121 Linear orders are an example of subclassing\index{subclasses} |
120 common case. It is also possible to prove additional subclass relationships |
122 by construction, which is the most |
121 later on, i.e.\ subclassing by proof. This is the topic of the following |
123 common case. Subclass relationships can also be proved. |
|
124 This is the topic of the following |
122 paragraph.% |
125 paragraph.% |
123 \end{isamarkuptext}% |
126 \end{isamarkuptext}% |
124 % |
127 % |
125 \isamarkupsubsubsection{Strict Orders% |
128 \isamarkupsubsubsection{Strict Orders% |
126 } |
129 } |
127 % |
130 % |
128 \begin{isamarkuptext}% |
131 \begin{isamarkuptext}% |
129 An alternative axiomatization of partial orders takes \isa{{\isacharless}{\isacharless}} rather than |
132 An alternative axiomatization of partial orders takes \isa{{\isacharless}{\isacharless}} rather than |
130 \isa{{\isacharless}{\isacharless}{\isacharequal}} as the primary concept. The result is a \emph{strict} order:% |
133 \isa{{\isacharless}{\isacharless}{\isacharequal}} as the primary concept. The result is a \textbf{strict} order:% |
131 \end{isamarkuptext}% |
134 \end{isamarkuptext}% |
132 \isacommand{axclass}\ strord\ {\isacharless}\ ordrel\isanewline |
135 \isacommand{axclass}\ strord\ {\isacharless}\ ordrel\isanewline |
133 irrefl{\isacharcolon}\ \ \ \ \ {\isachardoublequote}{\isasymnot}\ x\ {\isacharless}{\isacharless}\ x{\isachardoublequote}\isanewline |
136 irrefl{\isacharcolon}\ \ \ \ \ {\isachardoublequote}{\isasymnot}\ x\ {\isacharless}{\isacharless}\ x{\isachardoublequote}\isanewline |
134 less{\isacharunderscore}trans{\isacharcolon}\ {\isachardoublequote}{\isasymlbrakk}\ x\ {\isacharless}{\isacharless}\ y{\isacharsemicolon}\ y\ {\isacharless}{\isacharless}\ z\ {\isasymrbrakk}\ {\isasymLongrightarrow}\ x\ {\isacharless}{\isacharless}\ z{\isachardoublequote}\isanewline |
137 less{\isacharunderscore}trans{\isacharcolon}\ {\isachardoublequote}{\isasymlbrakk}\ x\ {\isacharless}{\isacharless}\ y{\isacharsemicolon}\ y\ {\isacharless}{\isacharless}\ z\ {\isasymrbrakk}\ {\isasymLongrightarrow}\ x\ {\isacharless}{\isacharless}\ z{\isachardoublequote}\isanewline |
135 le{\isacharunderscore}less{\isacharcolon}\ \ \ \ {\isachardoublequote}x\ {\isacharless}{\isacharless}{\isacharequal}\ y\ {\isacharequal}\ {\isacharparenleft}x\ {\isacharless}{\isacharless}\ y\ {\isasymor}\ x\ {\isacharequal}\ y{\isacharparenright}{\isachardoublequote}% |
138 le{\isacharunderscore}less{\isacharcolon}\ \ \ \ {\isachardoublequote}x\ {\isacharless}{\isacharless}{\isacharequal}\ y\ {\isacharequal}\ {\isacharparenleft}x\ {\isacharless}{\isacharless}\ y\ {\isasymor}\ x\ {\isacharequal}\ y{\isacharparenright}{\isachardoublequote}% |
165 \isamarkupsubsubsection{Multiple Inheritance and Sorts% |
168 \isamarkupsubsubsection{Multiple Inheritance and Sorts% |
166 } |
169 } |
167 % |
170 % |
168 \begin{isamarkuptext}% |
171 \begin{isamarkuptext}% |
169 A class may inherit from more than one direct superclass. This is called |
172 A class may inherit from more than one direct superclass. This is called |
170 multiple inheritance and is certainly permitted. For example we could define |
173 \bfindex{multiple inheritance}. For example, we could define |
171 the classes of well-founded orderings and well-orderings:% |
174 the classes of well-founded orderings and well-orderings:% |
172 \end{isamarkuptext}% |
175 \end{isamarkuptext}% |
173 \isacommand{axclass}\ wford\ {\isacharless}\ parord\isanewline |
176 \isacommand{axclass}\ wford\ {\isacharless}\ parord\isanewline |
174 wford{\isacharcolon}\ {\isachardoublequote}wf\ {\isacharbraceleft}{\isacharparenleft}y{\isacharcomma}x{\isacharparenright}{\isachardot}\ y\ {\isacharless}{\isacharless}\ x{\isacharbraceright}{\isachardoublequote}\isanewline |
177 wford{\isacharcolon}\ {\isachardoublequote}wf\ {\isacharbraceleft}{\isacharparenleft}y{\isacharcomma}x{\isacharparenright}{\isachardot}\ y\ {\isacharless}{\isacharless}\ x{\isacharbraceright}{\isachardoublequote}\isanewline |
175 \isanewline |
178 \isanewline |
210 However, we do not pursue this rarefied concept further. |
213 However, we do not pursue this rarefied concept further. |
211 |
214 |
212 This concludes our demonstration of type classes based on orderings. We |
215 This concludes our demonstration of type classes based on orderings. We |
213 remind our readers that \isa{Main} contains a theory of |
216 remind our readers that \isa{Main} contains a theory of |
214 orderings phrased in terms of the usual \isa{{\isasymle}} and \isa{{\isacharless}}. |
217 orderings phrased in terms of the usual \isa{{\isasymle}} and \isa{{\isacharless}}. |
215 It is recommended that, if possible, |
218 If possible, base your own ordering relations on this theory.% |
216 you base your own ordering relations on this theory.% |
|
217 \end{isamarkuptext}% |
219 \end{isamarkuptext}% |
218 % |
220 % |
219 \isamarkupsubsubsection{Inconsistencies% |
221 \isamarkupsubsubsection{Inconsistencies% |
220 } |
222 } |
221 % |
223 % |
222 \begin{isamarkuptext}% |
224 \begin{isamarkuptext}% |
223 The reader may be wondering what happens if we, maybe accidentally, |
225 The reader may be wondering what happens if we |
224 attach an inconsistent set of axioms to a class. So far we have always |
226 attach an inconsistent set of axioms to a class. So far we have always |
225 avoided to add new axioms to HOL for fear of inconsistencies and suddenly it |
227 avoided to add new axioms to HOL for fear of inconsistencies and suddenly it |
226 seems that we are throwing all caution to the wind. So why is there no |
228 seems that we are throwing all caution to the wind. So why is there no |
227 problem? |
229 problem? |
228 |
230 |