21 % |
34 % |
22 \begin{isamarkuptext}% |
35 \begin{isamarkuptext}% |
23 A \emph{partial order} is a subclass of \isa{ordrel} |
36 A \emph{partial order} is a subclass of \isa{ordrel} |
24 where certain axioms need to hold:% |
37 where certain axioms need to hold:% |
25 \end{isamarkuptext}% |
38 \end{isamarkuptext}% |
26 \isamarkuptrue% |
39 \isamarkupfalse% |
27 \isacommand{axclass}\ parord\ {\isacharless}\ ordrel\isanewline |
40 \isacommand{axclass}\ parord\ {\isacharless}\ ordrel\isanewline |
28 refl{\isacharcolon}\ \ \ \ {\isachardoublequote}x\ {\isacharless}{\isacharless}{\isacharequal}\ x{\isachardoublequote}\isanewline |
41 refl{\isacharcolon}\ \ \ \ {\isachardoublequote}x\ {\isacharless}{\isacharless}{\isacharequal}\ x{\isachardoublequote}\isanewline |
29 trans{\isacharcolon}\ \ \ {\isachardoublequote}{\isasymlbrakk}\ x\ {\isacharless}{\isacharless}{\isacharequal}\ y{\isacharsemicolon}\ y\ {\isacharless}{\isacharless}{\isacharequal}\ z\ {\isasymrbrakk}\ {\isasymLongrightarrow}\ x\ {\isacharless}{\isacharless}{\isacharequal}\ z{\isachardoublequote}\isanewline |
42 trans{\isacharcolon}\ \ \ {\isachardoublequote}{\isasymlbrakk}\ x\ {\isacharless}{\isacharless}{\isacharequal}\ y{\isacharsemicolon}\ y\ {\isacharless}{\isacharless}{\isacharequal}\ z\ {\isasymrbrakk}\ {\isasymLongrightarrow}\ x\ {\isacharless}{\isacharless}{\isacharequal}\ z{\isachardoublequote}\isanewline |
30 antisym{\isacharcolon}\ {\isachardoublequote}{\isasymlbrakk}\ x\ {\isacharless}{\isacharless}{\isacharequal}\ y{\isacharsemicolon}\ y\ {\isacharless}{\isacharless}{\isacharequal}\ x\ {\isasymrbrakk}\ {\isasymLongrightarrow}\ x\ {\isacharequal}\ y{\isachardoublequote}\isanewline |
43 antisym{\isacharcolon}\ {\isachardoublequote}{\isasymlbrakk}\ x\ {\isacharless}{\isacharless}{\isacharequal}\ y{\isacharsemicolon}\ y\ {\isacharless}{\isacharless}{\isacharequal}\ x\ {\isasymrbrakk}\ {\isasymLongrightarrow}\ x\ {\isacharequal}\ y{\isachardoublequote}\isanewline |
31 less{\isacharunderscore}le{\isacharcolon}\ {\isachardoublequote}x\ {\isacharless}{\isacharless}\ y\ {\isacharequal}\ {\isacharparenleft}x\ {\isacharless}{\isacharless}{\isacharequal}\ y\ {\isasymand}\ x\ {\isasymnoteq}\ y{\isacharparenright}{\isachardoublequote}\isamarkupfalse% |
44 less{\isacharunderscore}le{\isacharcolon}\ {\isachardoublequote}x\ {\isacharless}{\isacharless}\ y\ {\isacharequal}\ {\isacharparenleft}x\ {\isacharless}{\isacharless}{\isacharequal}\ y\ {\isasymand}\ x\ {\isasymnoteq}\ y{\isacharparenright}{\isachardoublequote}\isamarkuptrue% |
32 % |
45 % |
33 \begin{isamarkuptext}% |
46 \begin{isamarkuptext}% |
34 \noindent |
47 \noindent |
35 The first three axioms are the familiar ones, and the final one |
48 The first three axioms are the familiar ones, and the final one |
36 requires that \isa{{\isacharless}{\isacharless}} and \isa{{\isacharless}{\isacharless}{\isacharequal}} are related as expected. |
49 requires that \isa{{\isacharless}{\isacharless}} and \isa{{\isacharless}{\isacharless}{\isacharequal}} are related as expected. |
45 we need to define both \isa{{\isacharless}{\isacharless}{\isacharequal}} and \isa{{\isacharless}{\isacharless}} for each instance. |
58 we need to define both \isa{{\isacharless}{\isacharless}{\isacharequal}} and \isa{{\isacharless}{\isacharless}} for each instance. |
46 |
59 |
47 We can now prove simple theorems in this abstract setting, for example |
60 We can now prove simple theorems in this abstract setting, for example |
48 that \isa{{\isacharless}{\isacharless}} is not symmetric:% |
61 that \isa{{\isacharless}{\isacharless}} is not symmetric:% |
49 \end{isamarkuptext}% |
62 \end{isamarkuptext}% |
50 \isamarkuptrue% |
63 \isamarkupfalse% |
51 \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}\isamarkupfalse% |
64 \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}% |
|
65 \isadelimproof |
|
66 % |
|
67 \endisadelimproof |
|
68 % |
|
69 \isatagproof |
|
70 \isamarkuptrue% |
52 % |
71 % |
53 \begin{isamarkuptxt}% |
72 \begin{isamarkuptxt}% |
54 \noindent |
73 \noindent |
55 The conclusion is not just \isa{{\isasymnot}\ y\ {\isacharless}{\isacharless}\ x} because the |
74 The conclusion is not just \isa{{\isasymnot}\ y\ {\isacharless}{\isacharless}\ x} because the |
56 simplifier's preprocessor (see \S\ref{sec:simp-preprocessor}) |
75 simplifier's preprocessor (see \S\ref{sec:simp-preprocessor}) |
61 In the form above, the rule is useful. |
80 In the form above, the rule is useful. |
62 The type constraint is necessary because otherwise Isabelle would only assume |
81 The type constraint is necessary because otherwise Isabelle would only assume |
63 \isa{{\isacharprime}a{\isacharcolon}{\isacharcolon}ordrel} (as required in the type of \isa{{\isacharless}{\isacharless}}), |
82 \isa{{\isacharprime}a{\isacharcolon}{\isacharcolon}ordrel} (as required in the type of \isa{{\isacharless}{\isacharless}}), |
64 when the proposition is not a theorem. The proof is easy:% |
83 when the proposition is not a theorem. The proof is easy:% |
65 \end{isamarkuptxt}% |
84 \end{isamarkuptxt}% |
66 \isamarkuptrue% |
85 \isamarkupfalse% |
67 \isacommand{by}{\isacharparenleft}simp\ add{\isacharcolon}\ less{\isacharunderscore}le\ antisym{\isacharparenright}\isamarkupfalse% |
86 \isacommand{by}{\isacharparenleft}simp\ add{\isacharcolon}\ less{\isacharunderscore}le\ antisym{\isacharparenright}% |
|
87 \endisatagproof |
|
88 {\isafoldproof}% |
|
89 % |
|
90 \isadelimproof |
|
91 % |
|
92 \endisadelimproof |
|
93 \isamarkuptrue% |
68 % |
94 % |
69 \begin{isamarkuptext}% |
95 \begin{isamarkuptext}% |
70 We could now continue in this vein and develop a whole theory of |
96 We could now continue in this vein and develop a whole theory of |
71 results about partial orders. Eventually we will want to apply these results |
97 results about partial orders. Eventually we will want to apply these results |
72 to concrete types, namely the instances of the class. Thus we first need to |
98 to concrete types, namely the instances of the class. Thus we first need to |
73 prove that the types in question, for example \isa{bool}, are indeed |
99 prove that the types in question, for example \isa{bool}, are indeed |
74 instances of \isa{parord}:% |
100 instances of \isa{parord}:% |
75 \end{isamarkuptext}% |
101 \end{isamarkuptext}% |
76 \isamarkuptrue% |
102 \isamarkupfalse% |
77 \isacommand{instance}\ bool\ {\isacharcolon}{\isacharcolon}\ parord\isanewline |
103 \isacommand{instance}\ bool\ {\isacharcolon}{\isacharcolon}\ parord\isanewline |
78 \isamarkupfalse% |
104 % |
79 \isacommand{apply}\ intro{\isacharunderscore}classes\isamarkupfalse% |
105 \isadelimproof |
|
106 % |
|
107 \endisadelimproof |
|
108 % |
|
109 \isatagproof |
|
110 \isamarkupfalse% |
|
111 \isacommand{apply}\ intro{\isacharunderscore}classes\isamarkuptrue% |
80 % |
112 % |
81 \begin{isamarkuptxt}% |
113 \begin{isamarkuptxt}% |
82 \noindent |
114 \noindent |
83 This time \isa{intro{\isacharunderscore}classes} leaves us with the four axioms, |
115 This time \isa{intro{\isacharunderscore}classes} leaves us with the four axioms, |
84 specialized to type \isa{bool}, as subgoals: |
116 specialized to type \isa{bool}, as subgoals: |
90 \end{isabelle} |
122 \end{isabelle} |
91 Fortunately, the proof is easy for \isa{blast} |
123 Fortunately, the proof is easy for \isa{blast} |
92 once we have unfolded the definitions |
124 once we have unfolded the definitions |
93 of \isa{{\isacharless}{\isacharless}} and \isa{{\isacharless}{\isacharless}{\isacharequal}} at type \isa{bool}:% |
125 of \isa{{\isacharless}{\isacharless}} and \isa{{\isacharless}{\isacharless}{\isacharequal}} at type \isa{bool}:% |
94 \end{isamarkuptxt}% |
126 \end{isamarkuptxt}% |
95 \isamarkuptrue% |
127 \isamarkupfalse% |
96 \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 |
128 \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 |
97 \isamarkupfalse% |
129 \isamarkupfalse% |
98 \isacommand{by}{\isacharparenleft}blast{\isacharcomma}\ blast{\isacharcomma}\ blast{\isacharcomma}\ blast{\isacharparenright}\isamarkupfalse% |
130 \isacommand{by}{\isacharparenleft}blast{\isacharcomma}\ blast{\isacharcomma}\ blast{\isacharcomma}\ blast{\isacharparenright}% |
|
131 \endisatagproof |
|
132 {\isafoldproof}% |
|
133 % |
|
134 \isadelimproof |
|
135 % |
|
136 \endisadelimproof |
|
137 \isamarkuptrue% |
99 % |
138 % |
100 \begin{isamarkuptext}% |
139 \begin{isamarkuptext}% |
101 \noindent |
140 \noindent |
102 Can you figure out why we have to include \isa{{\isacharparenleft}no{\isacharunderscore}asm{\isacharunderscore}use{\isacharparenright}}? |
141 Can you figure out why we have to include \isa{{\isacharparenleft}no{\isacharunderscore}asm{\isacharunderscore}use{\isacharparenright}}? |
103 |
142 |
104 We can now apply our single lemma above in the context of booleans:% |
143 We can now apply our single lemma above in the context of booleans:% |
105 \end{isamarkuptext}% |
144 \end{isamarkuptext}% |
106 \isamarkuptrue% |
145 \isamarkupfalse% |
107 \isacommand{lemma}\ {\isachardoublequote}{\isacharparenleft}P{\isacharcolon}{\isacharcolon}bool{\isacharparenright}\ {\isacharless}{\isacharless}\ Q\ {\isasymLongrightarrow}\ {\isasymnot}{\isacharparenleft}Q\ {\isacharless}{\isacharless}\ P{\isacharparenright}{\isachardoublequote}\isanewline |
146 \isacommand{lemma}\ {\isachardoublequote}{\isacharparenleft}P{\isacharcolon}{\isacharcolon}bool{\isacharparenright}\ {\isacharless}{\isacharless}\ Q\ {\isasymLongrightarrow}\ {\isasymnot}{\isacharparenleft}Q\ {\isacharless}{\isacharless}\ P{\isacharparenright}{\isachardoublequote}\isanewline |
108 \isamarkupfalse% |
147 % |
109 \isacommand{by}\ simp\isamarkupfalse% |
148 \isadelimproof |
|
149 % |
|
150 \endisadelimproof |
|
151 % |
|
152 \isatagproof |
|
153 \isamarkupfalse% |
|
154 \isacommand{by}\ simp% |
|
155 \endisatagproof |
|
156 {\isafoldproof}% |
|
157 % |
|
158 \isadelimproof |
|
159 % |
|
160 \endisadelimproof |
|
161 \isamarkuptrue% |
110 % |
162 % |
111 \begin{isamarkuptext}% |
163 \begin{isamarkuptext}% |
112 \noindent |
164 \noindent |
113 The effect is not stunning, but it demonstrates the principle. It also shows |
165 The effect is not stunning, but it demonstrates the principle. It also shows |
114 that tools like the simplifier can deal with generic rules. |
166 that tools like the simplifier can deal with generic rules. |
123 % |
175 % |
124 \begin{isamarkuptext}% |
176 \begin{isamarkuptext}% |
125 If any two elements of a partial order are comparable it is a |
177 If any two elements of a partial order are comparable it is a |
126 \textbf{linear} or \textbf{total} order:% |
178 \textbf{linear} or \textbf{total} order:% |
127 \end{isamarkuptext}% |
179 \end{isamarkuptext}% |
128 \isamarkuptrue% |
180 \isamarkupfalse% |
129 \isacommand{axclass}\ linord\ {\isacharless}\ parord\isanewline |
181 \isacommand{axclass}\ linord\ {\isacharless}\ parord\isanewline |
130 linear{\isacharcolon}\ {\isachardoublequote}x\ {\isacharless}{\isacharless}{\isacharequal}\ y\ {\isasymor}\ y\ {\isacharless}{\isacharless}{\isacharequal}\ x{\isachardoublequote}\isamarkupfalse% |
182 linear{\isacharcolon}\ {\isachardoublequote}x\ {\isacharless}{\isacharless}{\isacharequal}\ y\ {\isasymor}\ y\ {\isacharless}{\isacharless}{\isacharequal}\ x{\isachardoublequote}\isamarkuptrue% |
131 % |
183 % |
132 \begin{isamarkuptext}% |
184 \begin{isamarkuptext}% |
133 \noindent |
185 \noindent |
134 By construction, \isa{linord} inherits all axioms from \isa{parord}. |
186 By construction, \isa{linord} inherits all axioms from \isa{parord}. |
135 Therefore we can show that linearity can be expressed in terms of \isa{{\isacharless}{\isacharless}} |
187 Therefore we can show that linearity can be expressed in terms of \isa{{\isacharless}{\isacharless}} |
136 as follows:% |
188 as follows:% |
137 \end{isamarkuptext}% |
189 \end{isamarkuptext}% |
138 \isamarkuptrue% |
190 \isamarkupfalse% |
139 \isacommand{lemma}\ {\isachardoublequote}{\isasymAnd}x{\isacharcolon}{\isacharcolon}{\isacharprime}a{\isacharcolon}{\isacharcolon}linord{\isachardot}\ x\ {\isacharless}{\isacharless}\ y\ {\isasymor}\ x\ {\isacharequal}\ y\ {\isasymor}\ y\ {\isacharless}{\isacharless}\ x{\isachardoublequote}\isanewline |
191 \isacommand{lemma}\ {\isachardoublequote}{\isasymAnd}x{\isacharcolon}{\isacharcolon}{\isacharprime}a{\isacharcolon}{\isacharcolon}linord{\isachardot}\ x\ {\isacharless}{\isacharless}\ y\ {\isasymor}\ x\ {\isacharequal}\ y\ {\isasymor}\ y\ {\isacharless}{\isacharless}\ x{\isachardoublequote}\isanewline |
|
192 % |
|
193 \isadelimproof |
|
194 % |
|
195 \endisadelimproof |
|
196 % |
|
197 \isatagproof |
140 \isamarkupfalse% |
198 \isamarkupfalse% |
141 \isacommand{apply}{\isacharparenleft}simp\ add{\isacharcolon}\ less{\isacharunderscore}le{\isacharparenright}\isanewline |
199 \isacommand{apply}{\isacharparenleft}simp\ add{\isacharcolon}\ less{\isacharunderscore}le{\isacharparenright}\isanewline |
142 \isamarkupfalse% |
200 \isamarkupfalse% |
143 \isacommand{apply}{\isacharparenleft}insert\ linear{\isacharparenright}\isanewline |
201 \isacommand{apply}{\isacharparenleft}insert\ linear{\isacharparenright}\isanewline |
144 \isamarkupfalse% |
202 \isamarkupfalse% |
145 \isacommand{apply}\ blast\isanewline |
203 \isacommand{apply}\ blast\isanewline |
146 \isamarkupfalse% |
204 \isamarkupfalse% |
147 \isacommand{done}\isamarkupfalse% |
205 \isacommand{done}% |
|
206 \endisatagproof |
|
207 {\isafoldproof}% |
|
208 % |
|
209 \isadelimproof |
|
210 % |
|
211 \endisadelimproof |
|
212 \isamarkuptrue% |
148 % |
213 % |
149 \begin{isamarkuptext}% |
214 \begin{isamarkuptext}% |
150 Linear orders are an example of subclassing\index{subclasses} |
215 Linear orders are an example of subclassing\index{subclasses} |
151 by construction, which is the most |
216 by construction, which is the most |
152 common case. Subclass relationships can also be proved. |
217 common case. Subclass relationships can also be proved. |
161 % |
226 % |
162 \begin{isamarkuptext}% |
227 \begin{isamarkuptext}% |
163 An alternative axiomatization of partial orders takes \isa{{\isacharless}{\isacharless}} rather than |
228 An alternative axiomatization of partial orders takes \isa{{\isacharless}{\isacharless}} rather than |
164 \isa{{\isacharless}{\isacharless}{\isacharequal}} as the primary concept. The result is a \textbf{strict} order:% |
229 \isa{{\isacharless}{\isacharless}{\isacharequal}} as the primary concept. The result is a \textbf{strict} order:% |
165 \end{isamarkuptext}% |
230 \end{isamarkuptext}% |
166 \isamarkuptrue% |
231 \isamarkupfalse% |
167 \isacommand{axclass}\ strord\ {\isacharless}\ ordrel\isanewline |
232 \isacommand{axclass}\ strord\ {\isacharless}\ ordrel\isanewline |
168 irrefl{\isacharcolon}\ \ \ \ \ {\isachardoublequote}{\isasymnot}\ x\ {\isacharless}{\isacharless}\ x{\isachardoublequote}\isanewline |
233 irrefl{\isacharcolon}\ \ \ \ \ {\isachardoublequote}{\isasymnot}\ x\ {\isacharless}{\isacharless}\ x{\isachardoublequote}\isanewline |
169 less{\isacharunderscore}trans{\isacharcolon}\ {\isachardoublequote}{\isasymlbrakk}\ x\ {\isacharless}{\isacharless}\ y{\isacharsemicolon}\ y\ {\isacharless}{\isacharless}\ z\ {\isasymrbrakk}\ {\isasymLongrightarrow}\ x\ {\isacharless}{\isacharless}\ z{\isachardoublequote}\isanewline |
234 less{\isacharunderscore}trans{\isacharcolon}\ {\isachardoublequote}{\isasymlbrakk}\ x\ {\isacharless}{\isacharless}\ y{\isacharsemicolon}\ y\ {\isacharless}{\isacharless}\ z\ {\isasymrbrakk}\ {\isasymLongrightarrow}\ x\ {\isacharless}{\isacharless}\ z{\isachardoublequote}\isanewline |
170 le{\isacharunderscore}less{\isacharcolon}\ \ \ \ {\isachardoublequote}x\ {\isacharless}{\isacharless}{\isacharequal}\ y\ {\isacharequal}\ {\isacharparenleft}x\ {\isacharless}{\isacharless}\ y\ {\isasymor}\ x\ {\isacharequal}\ y{\isacharparenright}{\isachardoublequote}\isamarkupfalse% |
235 le{\isacharunderscore}less{\isacharcolon}\ \ \ \ {\isachardoublequote}x\ {\isacharless}{\isacharless}{\isacharequal}\ y\ {\isacharequal}\ {\isacharparenleft}x\ {\isacharless}{\isacharless}\ y\ {\isasymor}\ x\ {\isacharequal}\ y{\isacharparenright}{\isachardoublequote}\isamarkuptrue% |
171 % |
236 % |
172 \begin{isamarkuptext}% |
237 \begin{isamarkuptext}% |
173 \noindent |
238 \noindent |
174 It is well known that partial orders are the same as strict orders. Let us |
239 It is well known that partial orders are the same as strict orders. Let us |
175 prove one direction, namely that partial orders are a subclass of strict |
240 prove one direction, namely that partial orders are a subclass of strict |
176 orders.% |
241 orders.% |
177 \end{isamarkuptext}% |
242 \end{isamarkuptext}% |
178 \isamarkuptrue% |
243 \isamarkupfalse% |
179 \isacommand{instance}\ parord\ {\isacharless}\ strord\isanewline |
244 \isacommand{instance}\ parord\ {\isacharless}\ strord\isanewline |
180 \isamarkupfalse% |
245 % |
181 \isacommand{apply}\ intro{\isacharunderscore}classes\isamarkupfalse% |
246 \isadelimproof |
|
247 % |
|
248 \endisadelimproof |
|
249 % |
|
250 \isatagproof |
|
251 \isamarkupfalse% |
|
252 \isacommand{apply}\ intro{\isacharunderscore}classes\isamarkuptrue% |
182 % |
253 % |
183 \begin{isamarkuptxt}% |
254 \begin{isamarkuptxt}% |
184 \noindent |
255 \noindent |
185 \begin{isabelle}% |
256 \begin{isabelle}% |
186 \ {\isadigit{1}}{\isachardot}\ {\isasymAnd}x{\isasymColon}{\isacharprime}a{\isachardot}\ {\isasymnot}\ x\ {\isacharless}{\isacharless}\ x\isanewline |
257 \ {\isadigit{1}}{\isachardot}\ {\isasymAnd}x{\isasymColon}{\isacharprime}a{\isachardot}\ {\isasymnot}\ x\ {\isacharless}{\isacharless}\ x\isanewline |
190 \isaindent{\ \ }{\isacharprime}a\ {\isacharcolon}{\isacharcolon}\ parord% |
261 \isaindent{\ \ }{\isacharprime}a\ {\isacharcolon}{\isacharcolon}\ parord% |
191 \end{isabelle} |
262 \end{isabelle} |
192 Assuming \isa{{\isacharprime}a\ {\isacharcolon}{\isacharcolon}\ parord}, the three axioms of class \isa{strord} |
263 Assuming \isa{{\isacharprime}a\ {\isacharcolon}{\isacharcolon}\ parord}, the three axioms of class \isa{strord} |
193 are easily proved:% |
264 are easily proved:% |
194 \end{isamarkuptxt}% |
265 \end{isamarkuptxt}% |
195 \ \ \isamarkuptrue% |
266 \ \ \isamarkupfalse% |
196 \isacommand{apply}{\isacharparenleft}simp{\isacharunderscore}all\ {\isacharparenleft}no{\isacharunderscore}asm{\isacharunderscore}use{\isacharparenright}\ add{\isacharcolon}\ less{\isacharunderscore}le{\isacharparenright}\isanewline |
267 \isacommand{apply}{\isacharparenleft}simp{\isacharunderscore}all\ {\isacharparenleft}no{\isacharunderscore}asm{\isacharunderscore}use{\isacharparenright}\ add{\isacharcolon}\ less{\isacharunderscore}le{\isacharparenright}\isanewline |
197 \ \isamarkupfalse% |
268 \ \isamarkupfalse% |
198 \isacommand{apply}{\isacharparenleft}blast\ intro{\isacharcolon}\ trans\ antisym{\isacharparenright}\isanewline |
269 \isacommand{apply}{\isacharparenleft}blast\ intro{\isacharcolon}\ trans\ antisym{\isacharparenright}\isanewline |
199 \isamarkupfalse% |
270 \isamarkupfalse% |
200 \isacommand{apply}{\isacharparenleft}blast\ intro{\isacharcolon}\ refl{\isacharparenright}\isanewline |
271 \isacommand{apply}{\isacharparenleft}blast\ intro{\isacharcolon}\ refl{\isacharparenright}\isanewline |
201 \isamarkupfalse% |
272 \isamarkupfalse% |
202 \isacommand{done}\isamarkupfalse% |
273 \isacommand{done}% |
|
274 \endisatagproof |
|
275 {\isafoldproof}% |
|
276 % |
|
277 \isadelimproof |
|
278 % |
|
279 \endisadelimproof |
|
280 \isamarkuptrue% |
203 % |
281 % |
204 \begin{isamarkuptext}% |
282 \begin{isamarkuptext}% |
205 The subclass relation must always be acyclic. Therefore Isabelle will |
283 The subclass relation must always be acyclic. Therefore Isabelle will |
206 complain if you also prove the relationship \isa{strord\ {\isacharless}\ parord}.% |
284 complain if you also prove the relationship \isa{strord\ {\isacharless}\ parord}.% |
207 \end{isamarkuptext}% |
285 \end{isamarkuptext}% |
214 \begin{isamarkuptext}% |
292 \begin{isamarkuptext}% |
215 A class may inherit from more than one direct superclass. This is called |
293 A class may inherit from more than one direct superclass. This is called |
216 \bfindex{multiple inheritance}. For example, we could define |
294 \bfindex{multiple inheritance}. For example, we could define |
217 the classes of well-founded orderings and well-orderings:% |
295 the classes of well-founded orderings and well-orderings:% |
218 \end{isamarkuptext}% |
296 \end{isamarkuptext}% |
219 \isamarkuptrue% |
297 \isamarkupfalse% |
220 \isacommand{axclass}\ wford\ {\isacharless}\ parord\isanewline |
298 \isacommand{axclass}\ wford\ {\isacharless}\ parord\isanewline |
221 wford{\isacharcolon}\ {\isachardoublequote}wf\ {\isacharbraceleft}{\isacharparenleft}y{\isacharcomma}x{\isacharparenright}{\isachardot}\ y\ {\isacharless}{\isacharless}\ x{\isacharbraceright}{\isachardoublequote}\isanewline |
299 wford{\isacharcolon}\ {\isachardoublequote}wf\ {\isacharbraceleft}{\isacharparenleft}y{\isacharcomma}x{\isacharparenright}{\isachardot}\ y\ {\isacharless}{\isacharless}\ x{\isacharbraceright}{\isachardoublequote}\isanewline |
222 \isanewline |
300 \isanewline |
223 \isamarkupfalse% |
301 \isamarkupfalse% |
224 \isacommand{axclass}\ wellord\ {\isacharless}\ linord{\isacharcomma}\ wford\isamarkupfalse% |
302 \isacommand{axclass}\ wellord\ {\isacharless}\ linord{\isacharcomma}\ wford\isamarkuptrue% |
225 % |
303 % |
226 \begin{isamarkuptext}% |
304 \begin{isamarkuptext}% |
227 \noindent |
305 \noindent |
228 The last line expresses the usual definition: a well-ordering is a linear |
306 The last line expresses the usual definition: a well-ordering is a linear |
229 well-founded ordering. The result is the subclass diagram in |
307 well-founded ordering. The result is the subclass diagram in |