|
1 % |
|
2 \begin{isabellebody}% |
|
3 \def\isabellecontext{First{\isacharunderscore}Order{\isacharunderscore}Logic}% |
|
4 % |
|
5 \isamarkupheader{Example: First-Order Logic% |
|
6 } |
|
7 \isamarkuptrue% |
|
8 % |
|
9 \isadelimvisible |
|
10 % |
|
11 \endisadelimvisible |
|
12 % |
|
13 \isatagvisible |
|
14 \isacommand{theory}\isamarkupfalse% |
|
15 \ First{\isacharunderscore}Order{\isacharunderscore}Logic\isanewline |
|
16 \isakeyword{imports}\ Pure\isanewline |
|
17 \isakeyword{begin}% |
|
18 \endisatagvisible |
|
19 {\isafoldvisible}% |
|
20 % |
|
21 \isadelimvisible |
|
22 % |
|
23 \endisadelimvisible |
|
24 % |
|
25 \begin{isamarkuptext}% |
|
26 In order to commence a new object-logic within Isabelle/Pure we |
|
27 introduce abstract syntactic categories \isa{{\isachardoublequote}i{\isachardoublequote}} for individuals |
|
28 and \isa{{\isachardoublequote}o{\isachardoublequote}} for object-propositions. The latter is embedded |
|
29 into the language of Pure propositions by means of a separate |
|
30 judgment.% |
|
31 \end{isamarkuptext}% |
|
32 \isamarkuptrue% |
|
33 \isacommand{typedecl}\isamarkupfalse% |
|
34 \ i\isanewline |
|
35 \isacommand{typedecl}\isamarkupfalse% |
|
36 \ o\isanewline |
|
37 \isanewline |
|
38 \isacommand{judgment}\isamarkupfalse% |
|
39 \isanewline |
|
40 \ \ Trueprop\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}o\ {\isasymRightarrow}\ prop{\isachardoublequoteclose}\ \ \ \ {\isacharparenleft}{\isachardoublequoteopen}{\isacharunderscore}{\isachardoublequoteclose}\ {\isadigit{5}}{\isacharparenright}% |
|
41 \begin{isamarkuptext}% |
|
42 \noindent Note that the object-logic judgement is implicit in the |
|
43 syntax: writing \isa{A} produces \isa{{\isachardoublequote}Trueprop\ A{\isachardoublequote}} internally. |
|
44 From the Pure perspective this means ``\isa{A} is derivable in the |
|
45 object-logic''.% |
|
46 \end{isamarkuptext}% |
|
47 \isamarkuptrue% |
|
48 % |
|
49 \isamarkupsubsection{Equational reasoning \label{sec:framework-ex-equal}% |
|
50 } |
|
51 \isamarkuptrue% |
|
52 % |
|
53 \begin{isamarkuptext}% |
|
54 Equality is axiomatized as a binary predicate on individuals, with |
|
55 reflexivity as introduction, and substitution as elimination |
|
56 principle. Note that the latter is particularly convenient in a |
|
57 framework like Isabelle, because syntactic congruences are |
|
58 implicitly produced by unification of \isa{{\isachardoublequote}B\ x{\isachardoublequote}} against |
|
59 expressions containing occurrences of \isa{x}.% |
|
60 \end{isamarkuptext}% |
|
61 \isamarkuptrue% |
|
62 \isacommand{axiomatization}\isamarkupfalse% |
|
63 \isanewline |
|
64 \ \ equal\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}i\ {\isasymRightarrow}\ i\ {\isasymRightarrow}\ o{\isachardoublequoteclose}\ \ {\isacharparenleft}\isakeyword{infix}\ {\isachardoublequoteopen}{\isacharequal}{\isachardoublequoteclose}\ {\isadigit{5}}{\isadigit{0}}{\isacharparenright}\isanewline |
|
65 \isakeyword{where}\isanewline |
|
66 \ \ refl\ {\isacharbrackleft}intro{\isacharbrackright}{\isacharcolon}\ {\isachardoublequoteopen}x\ {\isacharequal}\ x{\isachardoublequoteclose}\ \isakeyword{and}\isanewline |
|
67 \ \ subst\ {\isacharbrackleft}elim{\isacharbrackright}{\isacharcolon}\ {\isachardoublequoteopen}x\ {\isacharequal}\ y\ {\isasymLongrightarrow}\ B\ x\ {\isasymLongrightarrow}\ B\ y{\isachardoublequoteclose}% |
|
68 \begin{isamarkuptext}% |
|
69 \noindent Substitution is very powerful, but also hard to control in |
|
70 full generality. We derive some common symmetry~/ transitivity |
|
71 schemes of as particular consequences.% |
|
72 \end{isamarkuptext}% |
|
73 \isamarkuptrue% |
|
74 \isacommand{theorem}\isamarkupfalse% |
|
75 \ sym\ {\isacharbrackleft}sym{\isacharbrackright}{\isacharcolon}\isanewline |
|
76 \ \ \isakeyword{assumes}\ {\isachardoublequoteopen}x\ {\isacharequal}\ y{\isachardoublequoteclose}\isanewline |
|
77 \ \ \isakeyword{shows}\ {\isachardoublequoteopen}y\ {\isacharequal}\ x{\isachardoublequoteclose}\isanewline |
|
78 % |
|
79 \isadelimproof |
|
80 % |
|
81 \endisadelimproof |
|
82 % |
|
83 \isatagproof |
|
84 \isacommand{proof}\isamarkupfalse% |
|
85 \ {\isacharminus}\isanewline |
|
86 \ \ \isacommand{have}\isamarkupfalse% |
|
87 \ {\isachardoublequoteopen}x\ {\isacharequal}\ x{\isachardoublequoteclose}\ \isacommand{{\isachardot}{\isachardot}}\isamarkupfalse% |
|
88 \isanewline |
|
89 \ \ \isacommand{with}\isamarkupfalse% |
|
90 \ {\isacharbackquoteopen}x\ {\isacharequal}\ y{\isacharbackquoteclose}\ \isacommand{show}\isamarkupfalse% |
|
91 \ {\isachardoublequoteopen}y\ {\isacharequal}\ x{\isachardoublequoteclose}\ \isacommand{{\isachardot}{\isachardot}}\isamarkupfalse% |
|
92 \isanewline |
|
93 \isacommand{qed}\isamarkupfalse% |
|
94 % |
|
95 \endisatagproof |
|
96 {\isafoldproof}% |
|
97 % |
|
98 \isadelimproof |
|
99 \isanewline |
|
100 % |
|
101 \endisadelimproof |
|
102 \isanewline |
|
103 \isacommand{theorem}\isamarkupfalse% |
|
104 \ forw{\isacharunderscore}subst\ {\isacharbrackleft}trans{\isacharbrackright}{\isacharcolon}\isanewline |
|
105 \ \ \isakeyword{assumes}\ {\isachardoublequoteopen}y\ {\isacharequal}\ x{\isachardoublequoteclose}\ \isakeyword{and}\ {\isachardoublequoteopen}B\ x{\isachardoublequoteclose}\isanewline |
|
106 \ \ \isakeyword{shows}\ {\isachardoublequoteopen}B\ y{\isachardoublequoteclose}\isanewline |
|
107 % |
|
108 \isadelimproof |
|
109 % |
|
110 \endisadelimproof |
|
111 % |
|
112 \isatagproof |
|
113 \isacommand{proof}\isamarkupfalse% |
|
114 \ {\isacharminus}\isanewline |
|
115 \ \ \isacommand{from}\isamarkupfalse% |
|
116 \ {\isacharbackquoteopen}y\ {\isacharequal}\ x{\isacharbackquoteclose}\ \isacommand{have}\isamarkupfalse% |
|
117 \ {\isachardoublequoteopen}x\ {\isacharequal}\ y{\isachardoublequoteclose}\ \isacommand{{\isachardot}{\isachardot}}\isamarkupfalse% |
|
118 \isanewline |
|
119 \ \ \isacommand{from}\isamarkupfalse% |
|
120 \ this\ \isakeyword{and}\ {\isacharbackquoteopen}B\ x{\isacharbackquoteclose}\ \isacommand{show}\isamarkupfalse% |
|
121 \ {\isachardoublequoteopen}B\ y{\isachardoublequoteclose}\ \isacommand{{\isachardot}{\isachardot}}\isamarkupfalse% |
|
122 \isanewline |
|
123 \isacommand{qed}\isamarkupfalse% |
|
124 % |
|
125 \endisatagproof |
|
126 {\isafoldproof}% |
|
127 % |
|
128 \isadelimproof |
|
129 \isanewline |
|
130 % |
|
131 \endisadelimproof |
|
132 \isanewline |
|
133 \isacommand{theorem}\isamarkupfalse% |
|
134 \ back{\isacharunderscore}subst\ {\isacharbrackleft}trans{\isacharbrackright}{\isacharcolon}\isanewline |
|
135 \ \ \isakeyword{assumes}\ {\isachardoublequoteopen}B\ x{\isachardoublequoteclose}\ \isakeyword{and}\ {\isachardoublequoteopen}x\ {\isacharequal}\ y{\isachardoublequoteclose}\isanewline |
|
136 \ \ \isakeyword{shows}\ {\isachardoublequoteopen}B\ y{\isachardoublequoteclose}\isanewline |
|
137 % |
|
138 \isadelimproof |
|
139 % |
|
140 \endisadelimproof |
|
141 % |
|
142 \isatagproof |
|
143 \isacommand{proof}\isamarkupfalse% |
|
144 \ {\isacharminus}\isanewline |
|
145 \ \ \isacommand{from}\isamarkupfalse% |
|
146 \ {\isacharbackquoteopen}x\ {\isacharequal}\ y{\isacharbackquoteclose}\ \isakeyword{and}\ {\isacharbackquoteopen}B\ x{\isacharbackquoteclose}\isanewline |
|
147 \ \ \isacommand{show}\isamarkupfalse% |
|
148 \ {\isachardoublequoteopen}B\ y{\isachardoublequoteclose}\ \isacommand{{\isachardot}{\isachardot}}\isamarkupfalse% |
|
149 \isanewline |
|
150 \isacommand{qed}\isamarkupfalse% |
|
151 % |
|
152 \endisatagproof |
|
153 {\isafoldproof}% |
|
154 % |
|
155 \isadelimproof |
|
156 \isanewline |
|
157 % |
|
158 \endisadelimproof |
|
159 \isanewline |
|
160 \isacommand{theorem}\isamarkupfalse% |
|
161 \ trans\ {\isacharbrackleft}trans{\isacharbrackright}{\isacharcolon}\isanewline |
|
162 \ \ \isakeyword{assumes}\ {\isachardoublequoteopen}x\ {\isacharequal}\ y{\isachardoublequoteclose}\ \isakeyword{and}\ {\isachardoublequoteopen}y\ {\isacharequal}\ z{\isachardoublequoteclose}\isanewline |
|
163 \ \ \isakeyword{shows}\ {\isachardoublequoteopen}x\ {\isacharequal}\ z{\isachardoublequoteclose}\isanewline |
|
164 % |
|
165 \isadelimproof |
|
166 % |
|
167 \endisadelimproof |
|
168 % |
|
169 \isatagproof |
|
170 \isacommand{proof}\isamarkupfalse% |
|
171 \ {\isacharminus}\isanewline |
|
172 \ \ \isacommand{from}\isamarkupfalse% |
|
173 \ {\isacharbackquoteopen}y\ {\isacharequal}\ z{\isacharbackquoteclose}\ \isakeyword{and}\ {\isacharbackquoteopen}x\ {\isacharequal}\ y{\isacharbackquoteclose}\isanewline |
|
174 \ \ \isacommand{show}\isamarkupfalse% |
|
175 \ {\isachardoublequoteopen}x\ {\isacharequal}\ z{\isachardoublequoteclose}\ \isacommand{{\isachardot}{\isachardot}}\isamarkupfalse% |
|
176 \isanewline |
|
177 \isacommand{qed}\isamarkupfalse% |
|
178 % |
|
179 \endisatagproof |
|
180 {\isafoldproof}% |
|
181 % |
|
182 \isadelimproof |
|
183 % |
|
184 \endisadelimproof |
|
185 % |
|
186 \isamarkupsubsection{Basic group theory% |
|
187 } |
|
188 \isamarkuptrue% |
|
189 % |
|
190 \begin{isamarkuptext}% |
|
191 As an example for equational reasoning we consider some bits of |
|
192 group theory. The subsequent locale definition postulates group |
|
193 operations and axioms; we also derive some consequences of this |
|
194 specification.% |
|
195 \end{isamarkuptext}% |
|
196 \isamarkuptrue% |
|
197 \isacommand{locale}\isamarkupfalse% |
|
198 \ group\ {\isacharequal}\isanewline |
|
199 \ \ \isakeyword{fixes}\ prod\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}i\ {\isasymRightarrow}\ i\ {\isasymRightarrow}\ i{\isachardoublequoteclose}\ \ {\isacharparenleft}\isakeyword{infix}\ {\isachardoublequoteopen}{\isasymcirc}{\isachardoublequoteclose}\ {\isadigit{7}}{\isadigit{0}}{\isacharparenright}\isanewline |
|
200 \ \ \ \ \isakeyword{and}\ inv\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}i\ {\isasymRightarrow}\ i{\isachardoublequoteclose}\ \ {\isacharparenleft}{\isachardoublequoteopen}{\isacharparenleft}{\isacharunderscore}{\isasyminverse}{\isacharparenright}{\isachardoublequoteclose}\ {\isacharbrackleft}{\isadigit{1}}{\isadigit{0}}{\isadigit{0}}{\isadigit{0}}{\isacharbrackright}\ {\isadigit{9}}{\isadigit{9}}{\isadigit{9}}{\isacharparenright}\isanewline |
|
201 \ \ \ \ \isakeyword{and}\ unit\ {\isacharcolon}{\isacharcolon}\ i\ \ {\isacharparenleft}{\isachardoublequoteopen}{\isadigit{1}}{\isachardoublequoteclose}{\isacharparenright}\isanewline |
|
202 \ \ \isakeyword{assumes}\ assoc{\isacharcolon}\ {\isachardoublequoteopen}{\isacharparenleft}x\ {\isasymcirc}\ y{\isacharparenright}\ {\isasymcirc}\ z\ {\isacharequal}\ x\ {\isasymcirc}\ {\isacharparenleft}y\ {\isasymcirc}\ z{\isacharparenright}{\isachardoublequoteclose}\isanewline |
|
203 \ \ \ \ \isakeyword{and}\ left{\isacharunderscore}unit{\isacharcolon}\ \ {\isachardoublequoteopen}{\isadigit{1}}\ {\isasymcirc}\ x\ {\isacharequal}\ x{\isachardoublequoteclose}\isanewline |
|
204 \ \ \ \ \isakeyword{and}\ left{\isacharunderscore}inv{\isacharcolon}\ {\isachardoublequoteopen}x{\isasyminverse}\ {\isasymcirc}\ x\ {\isacharequal}\ {\isadigit{1}}{\isachardoublequoteclose}\isanewline |
|
205 \isakeyword{begin}\isanewline |
|
206 \isanewline |
|
207 \isacommand{theorem}\isamarkupfalse% |
|
208 \ right{\isacharunderscore}inv{\isacharcolon}\ {\isachardoublequoteopen}x\ {\isasymcirc}\ x{\isasyminverse}\ {\isacharequal}\ {\isadigit{1}}{\isachardoublequoteclose}\isanewline |
|
209 % |
|
210 \isadelimproof |
|
211 % |
|
212 \endisadelimproof |
|
213 % |
|
214 \isatagproof |
|
215 \isacommand{proof}\isamarkupfalse% |
|
216 \ {\isacharminus}\isanewline |
|
217 \ \ \isacommand{have}\isamarkupfalse% |
|
218 \ {\isachardoublequoteopen}x\ {\isasymcirc}\ x{\isasyminverse}\ {\isacharequal}\ {\isadigit{1}}\ {\isasymcirc}\ {\isacharparenleft}x\ {\isasymcirc}\ x{\isasyminverse}{\isacharparenright}{\isachardoublequoteclose}\ \isacommand{by}\isamarkupfalse% |
|
219 \ {\isacharparenleft}rule\ left{\isacharunderscore}unit\ {\isacharbrackleft}symmetric{\isacharbrackright}{\isacharparenright}\isanewline |
|
220 \ \ \isacommand{also}\isamarkupfalse% |
|
221 \ \isacommand{have}\isamarkupfalse% |
|
222 \ {\isachardoublequoteopen}{\isasymdots}\ {\isacharequal}\ {\isacharparenleft}{\isadigit{1}}\ {\isasymcirc}\ x{\isacharparenright}\ {\isasymcirc}\ x{\isasyminverse}{\isachardoublequoteclose}\ \isacommand{by}\isamarkupfalse% |
|
223 \ {\isacharparenleft}rule\ assoc\ {\isacharbrackleft}symmetric{\isacharbrackright}{\isacharparenright}\isanewline |
|
224 \ \ \isacommand{also}\isamarkupfalse% |
|
225 \ \isacommand{have}\isamarkupfalse% |
|
226 \ {\isachardoublequoteopen}{\isadigit{1}}\ {\isacharequal}\ {\isacharparenleft}x{\isasyminverse}{\isacharparenright}{\isasyminverse}\ {\isasymcirc}\ x{\isasyminverse}{\isachardoublequoteclose}\ \isacommand{by}\isamarkupfalse% |
|
227 \ {\isacharparenleft}rule\ left{\isacharunderscore}inv\ {\isacharbrackleft}symmetric{\isacharbrackright}{\isacharparenright}\isanewline |
|
228 \ \ \isacommand{also}\isamarkupfalse% |
|
229 \ \isacommand{have}\isamarkupfalse% |
|
230 \ {\isachardoublequoteopen}{\isasymdots}\ {\isasymcirc}\ x\ {\isacharequal}\ {\isacharparenleft}x{\isasyminverse}{\isacharparenright}{\isasyminverse}\ {\isasymcirc}\ {\isacharparenleft}x{\isasyminverse}\ {\isasymcirc}\ x{\isacharparenright}{\isachardoublequoteclose}\ \isacommand{by}\isamarkupfalse% |
|
231 \ {\isacharparenleft}rule\ assoc{\isacharparenright}\isanewline |
|
232 \ \ \isacommand{also}\isamarkupfalse% |
|
233 \ \isacommand{have}\isamarkupfalse% |
|
234 \ {\isachardoublequoteopen}x{\isasyminverse}\ {\isasymcirc}\ x\ {\isacharequal}\ {\isadigit{1}}{\isachardoublequoteclose}\ \isacommand{by}\isamarkupfalse% |
|
235 \ {\isacharparenleft}rule\ left{\isacharunderscore}inv{\isacharparenright}\isanewline |
|
236 \ \ \isacommand{also}\isamarkupfalse% |
|
237 \ \isacommand{have}\isamarkupfalse% |
|
238 \ {\isachardoublequoteopen}{\isacharparenleft}{\isacharparenleft}x{\isasyminverse}{\isacharparenright}{\isasyminverse}\ {\isasymcirc}\ {\isasymdots}{\isacharparenright}\ {\isasymcirc}\ x{\isasyminverse}\ {\isacharequal}\ {\isacharparenleft}x{\isasyminverse}{\isacharparenright}{\isasyminverse}\ {\isasymcirc}\ {\isacharparenleft}{\isadigit{1}}\ {\isasymcirc}\ x{\isasyminverse}{\isacharparenright}{\isachardoublequoteclose}\ \isacommand{by}\isamarkupfalse% |
|
239 \ {\isacharparenleft}rule\ assoc{\isacharparenright}\isanewline |
|
240 \ \ \isacommand{also}\isamarkupfalse% |
|
241 \ \isacommand{have}\isamarkupfalse% |
|
242 \ {\isachardoublequoteopen}{\isadigit{1}}\ {\isasymcirc}\ x{\isasyminverse}\ {\isacharequal}\ x{\isasyminverse}{\isachardoublequoteclose}\ \isacommand{by}\isamarkupfalse% |
|
243 \ {\isacharparenleft}rule\ left{\isacharunderscore}unit{\isacharparenright}\isanewline |
|
244 \ \ \isacommand{also}\isamarkupfalse% |
|
245 \ \isacommand{have}\isamarkupfalse% |
|
246 \ {\isachardoublequoteopen}{\isacharparenleft}x{\isasyminverse}{\isacharparenright}{\isasyminverse}\ {\isasymcirc}\ {\isasymdots}\ {\isacharequal}\ {\isadigit{1}}{\isachardoublequoteclose}\ \isacommand{by}\isamarkupfalse% |
|
247 \ {\isacharparenleft}rule\ left{\isacharunderscore}inv{\isacharparenright}\isanewline |
|
248 \ \ \isacommand{finally}\isamarkupfalse% |
|
249 \ \isacommand{show}\isamarkupfalse% |
|
250 \ {\isachardoublequoteopen}x\ {\isasymcirc}\ x{\isasyminverse}\ {\isacharequal}\ {\isadigit{1}}{\isachardoublequoteclose}\ \isacommand{{\isachardot}}\isamarkupfalse% |
|
251 \isanewline |
|
252 \isacommand{qed}\isamarkupfalse% |
|
253 % |
|
254 \endisatagproof |
|
255 {\isafoldproof}% |
|
256 % |
|
257 \isadelimproof |
|
258 \isanewline |
|
259 % |
|
260 \endisadelimproof |
|
261 \isanewline |
|
262 \isacommand{theorem}\isamarkupfalse% |
|
263 \ right{\isacharunderscore}unit{\isacharcolon}\ {\isachardoublequoteopen}x\ {\isasymcirc}\ {\isadigit{1}}\ {\isacharequal}\ x{\isachardoublequoteclose}\isanewline |
|
264 % |
|
265 \isadelimproof |
|
266 % |
|
267 \endisadelimproof |
|
268 % |
|
269 \isatagproof |
|
270 \isacommand{proof}\isamarkupfalse% |
|
271 \ {\isacharminus}\isanewline |
|
272 \ \ \isacommand{have}\isamarkupfalse% |
|
273 \ {\isachardoublequoteopen}{\isadigit{1}}\ {\isacharequal}\ x{\isasyminverse}\ {\isasymcirc}\ x{\isachardoublequoteclose}\ \isacommand{by}\isamarkupfalse% |
|
274 \ {\isacharparenleft}rule\ left{\isacharunderscore}inv\ {\isacharbrackleft}symmetric{\isacharbrackright}{\isacharparenright}\isanewline |
|
275 \ \ \isacommand{also}\isamarkupfalse% |
|
276 \ \isacommand{have}\isamarkupfalse% |
|
277 \ {\isachardoublequoteopen}x\ {\isasymcirc}\ {\isasymdots}\ {\isacharequal}\ {\isacharparenleft}x\ {\isasymcirc}\ x{\isasyminverse}{\isacharparenright}\ {\isasymcirc}\ x{\isachardoublequoteclose}\ \isacommand{by}\isamarkupfalse% |
|
278 \ {\isacharparenleft}rule\ assoc\ {\isacharbrackleft}symmetric{\isacharbrackright}{\isacharparenright}\isanewline |
|
279 \ \ \isacommand{also}\isamarkupfalse% |
|
280 \ \isacommand{have}\isamarkupfalse% |
|
281 \ {\isachardoublequoteopen}x\ {\isasymcirc}\ x{\isasyminverse}\ {\isacharequal}\ {\isadigit{1}}{\isachardoublequoteclose}\ \isacommand{by}\isamarkupfalse% |
|
282 \ {\isacharparenleft}rule\ right{\isacharunderscore}inv{\isacharparenright}\isanewline |
|
283 \ \ \isacommand{also}\isamarkupfalse% |
|
284 \ \isacommand{have}\isamarkupfalse% |
|
285 \ {\isachardoublequoteopen}{\isasymdots}\ {\isasymcirc}\ x\ {\isacharequal}\ x{\isachardoublequoteclose}\ \isacommand{by}\isamarkupfalse% |
|
286 \ {\isacharparenleft}rule\ left{\isacharunderscore}unit{\isacharparenright}\isanewline |
|
287 \ \ \isacommand{finally}\isamarkupfalse% |
|
288 \ \isacommand{show}\isamarkupfalse% |
|
289 \ {\isachardoublequoteopen}x\ {\isasymcirc}\ {\isadigit{1}}\ {\isacharequal}\ x{\isachardoublequoteclose}\ \isacommand{{\isachardot}}\isamarkupfalse% |
|
290 \isanewline |
|
291 \isacommand{qed}\isamarkupfalse% |
|
292 % |
|
293 \endisatagproof |
|
294 {\isafoldproof}% |
|
295 % |
|
296 \isadelimproof |
|
297 % |
|
298 \endisadelimproof |
|
299 % |
|
300 \begin{isamarkuptext}% |
|
301 Reasoning from basic axioms is often tedious. Our proofs work by |
|
302 producing various instances of the given rules (potentially the |
|
303 symmetric form) using the pattern ``\hyperlink{command.have}{\mbox{\isa{\isacommand{have}}}}~\isa{eq}~\hyperlink{command.by}{\mbox{\isa{\isacommand{by}}}}~\isa{{\isachardoublequote}{\isacharparenleft}rule\ r{\isacharparenright}{\isachardoublequote}}'' and composing the chain of |
|
304 results via \hyperlink{command.also}{\mbox{\isa{\isacommand{also}}}}/\hyperlink{command.finally}{\mbox{\isa{\isacommand{finally}}}}. These steps may |
|
305 involve any of the transitivity rules declared in |
|
306 \secref{sec:framework-ex-equal}, namely \isa{trans} in combining |
|
307 the first two results in \isa{right{\isacharunderscore}inv} and in the final steps of |
|
308 both proofs, \isa{forw{\isacharunderscore}subst} in the first combination of \isa{right{\isacharunderscore}unit}, and \isa{back{\isacharunderscore}subst} in all other calculational steps. |
|
309 |
|
310 Occasional substitutions in calculations are adequate, but should |
|
311 not be over-emphasized. The other extreme is to compose a chain by |
|
312 plain transitivity only, with replacements occurring always in |
|
313 topmost position. For example:% |
|
314 \end{isamarkuptext}% |
|
315 \isamarkuptrue% |
|
316 % |
|
317 \isadelimproof |
|
318 % |
|
319 \endisadelimproof |
|
320 % |
|
321 \isatagproof |
|
322 \ \ \isacommand{have}\isamarkupfalse% |
|
323 \ {\isachardoublequoteopen}x\ {\isasymcirc}\ {\isadigit{1}}\ {\isacharequal}\ x\ {\isasymcirc}\ {\isacharparenleft}x{\isasyminverse}\ {\isasymcirc}\ x{\isacharparenright}{\isachardoublequoteclose}\ \isacommand{unfolding}\isamarkupfalse% |
|
324 \ left{\isacharunderscore}inv\ \isacommand{{\isachardot}{\isachardot}}\isamarkupfalse% |
|
325 \isanewline |
|
326 \ \ \isacommand{also}\isamarkupfalse% |
|
327 \ \isacommand{have}\isamarkupfalse% |
|
328 \ {\isachardoublequoteopen}{\isasymdots}\ {\isacharequal}\ {\isacharparenleft}x\ {\isasymcirc}\ x{\isasyminverse}{\isacharparenright}\ {\isasymcirc}\ x{\isachardoublequoteclose}\ \isacommand{unfolding}\isamarkupfalse% |
|
329 \ assoc\ \isacommand{{\isachardot}{\isachardot}}\isamarkupfalse% |
|
330 \isanewline |
|
331 \ \ \isacommand{also}\isamarkupfalse% |
|
332 \ \isacommand{have}\isamarkupfalse% |
|
333 \ {\isachardoublequoteopen}{\isasymdots}\ {\isacharequal}\ {\isadigit{1}}\ {\isasymcirc}\ x{\isachardoublequoteclose}\ \isacommand{unfolding}\isamarkupfalse% |
|
334 \ right{\isacharunderscore}inv\ \isacommand{{\isachardot}{\isachardot}}\isamarkupfalse% |
|
335 \isanewline |
|
336 \ \ \isacommand{also}\isamarkupfalse% |
|
337 \ \isacommand{have}\isamarkupfalse% |
|
338 \ {\isachardoublequoteopen}{\isasymdots}\ {\isacharequal}\ x{\isachardoublequoteclose}\ \isacommand{unfolding}\isamarkupfalse% |
|
339 \ left{\isacharunderscore}unit\ \isacommand{{\isachardot}{\isachardot}}\isamarkupfalse% |
|
340 \isanewline |
|
341 \ \ \isacommand{finally}\isamarkupfalse% |
|
342 \ \isacommand{have}\isamarkupfalse% |
|
343 \ {\isachardoublequoteopen}x\ {\isasymcirc}\ {\isadigit{1}}\ {\isacharequal}\ x{\isachardoublequoteclose}\ \isacommand{{\isachardot}}\isamarkupfalse% |
|
344 % |
|
345 \endisatagproof |
|
346 {\isafoldproof}% |
|
347 % |
|
348 \isadelimproof |
|
349 % |
|
350 \endisadelimproof |
|
351 % |
|
352 \begin{isamarkuptext}% |
|
353 \noindent Here we have re-used the built-in mechanism for unfolding |
|
354 definitions in order to normalize each equational problem. A more |
|
355 realistic object-logic would include proper setup for the Simplifier |
|
356 (\secref{sec:simplifier}), the main automated tool for equational |
|
357 reasoning in Isabelle. Then ``\hyperlink{command.unfolding}{\mbox{\isa{\isacommand{unfolding}}}}~\isa{left{\isacharunderscore}inv}~\hyperlink{command.ddot}{\mbox{\isa{\isacommand{{\isachardot}{\isachardot}}}}}'' would become ``\hyperlink{command.by}{\mbox{\isa{\isacommand{by}}}}~\isa{{\isachardoublequote}{\isacharparenleft}simp\ add{\isacharcolon}\ left{\isacharunderscore}inv{\isacharparenright}{\isachardoublequote}}'' etc.% |
|
358 \end{isamarkuptext}% |
|
359 \isamarkuptrue% |
|
360 \isacommand{end}\isamarkupfalse% |
|
361 % |
|
362 \isamarkupsubsection{Propositional logic% |
|
363 } |
|
364 \isamarkuptrue% |
|
365 % |
|
366 \begin{isamarkuptext}% |
|
367 We axiomatize basic connectives of propositional logic: implication, |
|
368 disjunction, and conjunction. The associated rules are modeled |
|
369 after Gentzen's natural deduction \cite{Gentzen:1935}.% |
|
370 \end{isamarkuptext}% |
|
371 \isamarkuptrue% |
|
372 \isacommand{axiomatization}\isamarkupfalse% |
|
373 \isanewline |
|
374 \ \ imp\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}o\ {\isasymRightarrow}\ o\ {\isasymRightarrow}\ o{\isachardoublequoteclose}\ \ {\isacharparenleft}\isakeyword{infixr}\ {\isachardoublequoteopen}{\isasymlongrightarrow}{\isachardoublequoteclose}\ {\isadigit{2}}{\isadigit{5}}{\isacharparenright}\ \isakeyword{where}\isanewline |
|
375 \ \ impI\ {\isacharbrackleft}intro{\isacharbrackright}{\isacharcolon}\ {\isachardoublequoteopen}{\isacharparenleft}A\ {\isasymLongrightarrow}\ B{\isacharparenright}\ {\isasymLongrightarrow}\ A\ {\isasymlongrightarrow}\ B{\isachardoublequoteclose}\ \isakeyword{and}\isanewline |
|
376 \ \ impD\ {\isacharbrackleft}dest{\isacharbrackright}{\isacharcolon}\ {\isachardoublequoteopen}{\isacharparenleft}A\ {\isasymlongrightarrow}\ B{\isacharparenright}\ {\isasymLongrightarrow}\ A\ {\isasymLongrightarrow}\ B{\isachardoublequoteclose}\isanewline |
|
377 \isanewline |
|
378 \isacommand{axiomatization}\isamarkupfalse% |
|
379 \isanewline |
|
380 \ \ disj\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}o\ {\isasymRightarrow}\ o\ {\isasymRightarrow}\ o{\isachardoublequoteclose}\ \ {\isacharparenleft}\isakeyword{infixr}\ {\isachardoublequoteopen}{\isasymor}{\isachardoublequoteclose}\ {\isadigit{3}}{\isadigit{0}}{\isacharparenright}\ \isakeyword{where}\isanewline |
|
381 \ \ disjE\ {\isacharbrackleft}elim{\isacharbrackright}{\isacharcolon}\ {\isachardoublequoteopen}A\ {\isasymor}\ B\ {\isasymLongrightarrow}\ {\isacharparenleft}A\ {\isasymLongrightarrow}\ C{\isacharparenright}\ {\isasymLongrightarrow}\ {\isacharparenleft}B\ {\isasymLongrightarrow}\ C{\isacharparenright}\ {\isasymLongrightarrow}\ C{\isachardoublequoteclose}\ \isakeyword{and}\isanewline |
|
382 \ \ disjI\isactrlisub {\isadigit{1}}\ {\isacharbrackleft}intro{\isacharbrackright}{\isacharcolon}\ {\isachardoublequoteopen}A\ {\isasymLongrightarrow}\ A\ {\isasymor}\ B{\isachardoublequoteclose}\ \isakeyword{and}\isanewline |
|
383 \ \ disjI\isactrlisub {\isadigit{2}}\ {\isacharbrackleft}intro{\isacharbrackright}{\isacharcolon}\ {\isachardoublequoteopen}B\ {\isasymLongrightarrow}\ A\ {\isasymor}\ B{\isachardoublequoteclose}\isanewline |
|
384 \isanewline |
|
385 \isacommand{axiomatization}\isamarkupfalse% |
|
386 \isanewline |
|
387 \ \ conj\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}o\ {\isasymRightarrow}\ o\ {\isasymRightarrow}\ o{\isachardoublequoteclose}\ \ {\isacharparenleft}\isakeyword{infixr}\ {\isachardoublequoteopen}{\isasymand}{\isachardoublequoteclose}\ {\isadigit{3}}{\isadigit{5}}{\isacharparenright}\ \isakeyword{where}\isanewline |
|
388 \ \ conjI\ {\isacharbrackleft}intro{\isacharbrackright}{\isacharcolon}\ {\isachardoublequoteopen}A\ {\isasymLongrightarrow}\ B\ {\isasymLongrightarrow}\ A\ {\isasymand}\ B{\isachardoublequoteclose}\ \isakeyword{and}\isanewline |
|
389 \ \ conjD\isactrlisub {\isadigit{1}}\ {\isacharbrackleft}dest{\isacharbrackright}{\isacharcolon}\ {\isachardoublequoteopen}A\ {\isasymand}\ B\ {\isasymLongrightarrow}\ A{\isachardoublequoteclose}\ \isakeyword{and}\isanewline |
|
390 \ \ conjD\isactrlisub {\isadigit{2}}\ {\isacharbrackleft}dest{\isacharbrackright}{\isacharcolon}\ {\isachardoublequoteopen}A\ {\isasymand}\ B\ {\isasymLongrightarrow}\ B{\isachardoublequoteclose}% |
|
391 \begin{isamarkuptext}% |
|
392 \noindent The conjunctive destructions have the disadvantage that |
|
393 decomposing \isa{{\isachardoublequote}A\ {\isasymand}\ B{\isachardoublequote}} involves an immediate decision which |
|
394 component should be projected. The more convenient simultaneous |
|
395 elimination \isa{{\isachardoublequote}A\ {\isasymand}\ B\ {\isasymLongrightarrow}\ {\isacharparenleft}A\ {\isasymLongrightarrow}\ B\ {\isasymLongrightarrow}\ C{\isacharparenright}\ {\isasymLongrightarrow}\ C{\isachardoublequote}} can be derived as |
|
396 follows:% |
|
397 \end{isamarkuptext}% |
|
398 \isamarkuptrue% |
|
399 \isacommand{theorem}\isamarkupfalse% |
|
400 \ conjE\ {\isacharbrackleft}elim{\isacharbrackright}{\isacharcolon}\isanewline |
|
401 \ \ \isakeyword{assumes}\ {\isachardoublequoteopen}A\ {\isasymand}\ B{\isachardoublequoteclose}\isanewline |
|
402 \ \ \isakeyword{obtains}\ A\ \isakeyword{and}\ B\isanewline |
|
403 % |
|
404 \isadelimproof |
|
405 % |
|
406 \endisadelimproof |
|
407 % |
|
408 \isatagproof |
|
409 \isacommand{proof}\isamarkupfalse% |
|
410 \isanewline |
|
411 \ \ \isacommand{from}\isamarkupfalse% |
|
412 \ {\isacharbackquoteopen}A\ {\isasymand}\ B{\isacharbackquoteclose}\ \isacommand{show}\isamarkupfalse% |
|
413 \ A\ \isacommand{{\isachardot}{\isachardot}}\isamarkupfalse% |
|
414 \isanewline |
|
415 \ \ \isacommand{from}\isamarkupfalse% |
|
416 \ {\isacharbackquoteopen}A\ {\isasymand}\ B{\isacharbackquoteclose}\ \isacommand{show}\isamarkupfalse% |
|
417 \ B\ \isacommand{{\isachardot}{\isachardot}}\isamarkupfalse% |
|
418 \isanewline |
|
419 \isacommand{qed}\isamarkupfalse% |
|
420 % |
|
421 \endisatagproof |
|
422 {\isafoldproof}% |
|
423 % |
|
424 \isadelimproof |
|
425 % |
|
426 \endisadelimproof |
|
427 % |
|
428 \begin{isamarkuptext}% |
|
429 \noindent Here is an example of swapping conjuncts with a single |
|
430 intermediate elimination step:% |
|
431 \end{isamarkuptext}% |
|
432 \isamarkuptrue% |
|
433 % |
|
434 \isadelimproof |
|
435 % |
|
436 \endisadelimproof |
|
437 % |
|
438 \isatagproof |
|
439 \ \ \isacommand{assume}\isamarkupfalse% |
|
440 \ {\isachardoublequoteopen}A\ {\isasymand}\ B{\isachardoublequoteclose}\isanewline |
|
441 \ \ \isacommand{then}\isamarkupfalse% |
|
442 \ \isacommand{obtain}\isamarkupfalse% |
|
443 \ B\ \isakeyword{and}\ A\ \isacommand{{\isachardot}{\isachardot}}\isamarkupfalse% |
|
444 \isanewline |
|
445 \ \ \isacommand{then}\isamarkupfalse% |
|
446 \ \isacommand{have}\isamarkupfalse% |
|
447 \ {\isachardoublequoteopen}B\ {\isasymand}\ A{\isachardoublequoteclose}\ \isacommand{{\isachardot}{\isachardot}}\isamarkupfalse% |
|
448 % |
|
449 \endisatagproof |
|
450 {\isafoldproof}% |
|
451 % |
|
452 \isadelimproof |
|
453 % |
|
454 \endisadelimproof |
|
455 % |
|
456 \begin{isamarkuptext}% |
|
457 Note that the analogous elimination for disjunction ``\isa{{\isachardoublequote}{\isasymASSUMES}\ A\ {\isasymor}\ B\ {\isasymOBTAINS}\ A\ {\isasymBBAR}\ B{\isachardoublequote}}'' coincides with the |
|
458 original axiomatization of \isa{{\isachardoublequote}disjE{\isachardoublequote}}. |
|
459 |
|
460 \medskip We continue propositional logic by introducing absurdity |
|
461 with its characteristic elimination. Plain truth may then be |
|
462 defined as a proposition that is trivially true.% |
|
463 \end{isamarkuptext}% |
|
464 \isamarkuptrue% |
|
465 \isacommand{axiomatization}\isamarkupfalse% |
|
466 \isanewline |
|
467 \ \ false\ {\isacharcolon}{\isacharcolon}\ o\ \ {\isacharparenleft}{\isachardoublequoteopen}{\isasymbottom}{\isachardoublequoteclose}{\isacharparenright}\ \isakeyword{where}\isanewline |
|
468 \ \ falseE\ {\isacharbrackleft}elim{\isacharbrackright}{\isacharcolon}\ {\isachardoublequoteopen}{\isasymbottom}\ {\isasymLongrightarrow}\ A{\isachardoublequoteclose}\isanewline |
|
469 \isanewline |
|
470 \isacommand{definition}\isamarkupfalse% |
|
471 \isanewline |
|
472 \ \ true\ {\isacharcolon}{\isacharcolon}\ o\ \ {\isacharparenleft}{\isachardoublequoteopen}{\isasymtop}{\isachardoublequoteclose}{\isacharparenright}\ \isakeyword{where}\isanewline |
|
473 \ \ {\isachardoublequoteopen}{\isasymtop}\ {\isasymequiv}\ {\isasymbottom}\ {\isasymlongrightarrow}\ {\isasymbottom}{\isachardoublequoteclose}\isanewline |
|
474 \isanewline |
|
475 \isacommand{theorem}\isamarkupfalse% |
|
476 \ trueI\ {\isacharbrackleft}intro{\isacharbrackright}{\isacharcolon}\ {\isasymtop}\isanewline |
|
477 % |
|
478 \isadelimproof |
|
479 \ \ % |
|
480 \endisadelimproof |
|
481 % |
|
482 \isatagproof |
|
483 \isacommand{unfolding}\isamarkupfalse% |
|
484 \ true{\isacharunderscore}def\ \isacommand{{\isachardot}{\isachardot}}\isamarkupfalse% |
|
485 % |
|
486 \endisatagproof |
|
487 {\isafoldproof}% |
|
488 % |
|
489 \isadelimproof |
|
490 % |
|
491 \endisadelimproof |
|
492 % |
|
493 \begin{isamarkuptext}% |
|
494 \medskip Now negation represents an implication towards absurdity:% |
|
495 \end{isamarkuptext}% |
|
496 \isamarkuptrue% |
|
497 \isacommand{definition}\isamarkupfalse% |
|
498 \isanewline |
|
499 \ \ not\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}o\ {\isasymRightarrow}\ o{\isachardoublequoteclose}\ \ {\isacharparenleft}{\isachardoublequoteopen}{\isasymnot}\ {\isacharunderscore}{\isachardoublequoteclose}\ {\isacharbrackleft}{\isadigit{4}}{\isadigit{0}}{\isacharbrackright}\ {\isadigit{4}}{\isadigit{0}}{\isacharparenright}\ \isakeyword{where}\isanewline |
|
500 \ \ {\isachardoublequoteopen}{\isasymnot}\ A\ {\isasymequiv}\ A\ {\isasymlongrightarrow}\ {\isasymbottom}{\isachardoublequoteclose}\isanewline |
|
501 \isanewline |
|
502 \isacommand{theorem}\isamarkupfalse% |
|
503 \ notI\ {\isacharbrackleft}intro{\isacharbrackright}{\isacharcolon}\isanewline |
|
504 \ \ \isakeyword{assumes}\ {\isachardoublequoteopen}A\ {\isasymLongrightarrow}\ {\isasymbottom}{\isachardoublequoteclose}\isanewline |
|
505 \ \ \isakeyword{shows}\ {\isachardoublequoteopen}{\isasymnot}\ A{\isachardoublequoteclose}\isanewline |
|
506 % |
|
507 \isadelimproof |
|
508 % |
|
509 \endisadelimproof |
|
510 % |
|
511 \isatagproof |
|
512 \isacommand{unfolding}\isamarkupfalse% |
|
513 \ not{\isacharunderscore}def\isanewline |
|
514 \isacommand{proof}\isamarkupfalse% |
|
515 \isanewline |
|
516 \ \ \isacommand{assume}\isamarkupfalse% |
|
517 \ A\isanewline |
|
518 \ \ \isacommand{then}\isamarkupfalse% |
|
519 \ \isacommand{show}\isamarkupfalse% |
|
520 \ {\isasymbottom}\ \isacommand{by}\isamarkupfalse% |
|
521 \ {\isacharparenleft}rule\ {\isacharbackquoteopen}A\ {\isasymLongrightarrow}\ {\isasymbottom}{\isacharbackquoteclose}{\isacharparenright}\isanewline |
|
522 \isacommand{qed}\isamarkupfalse% |
|
523 % |
|
524 \endisatagproof |
|
525 {\isafoldproof}% |
|
526 % |
|
527 \isadelimproof |
|
528 \isanewline |
|
529 % |
|
530 \endisadelimproof |
|
531 \isanewline |
|
532 \isacommand{theorem}\isamarkupfalse% |
|
533 \ notE\ {\isacharbrackleft}elim{\isacharbrackright}{\isacharcolon}\isanewline |
|
534 \ \ \isakeyword{assumes}\ {\isachardoublequoteopen}{\isasymnot}\ A{\isachardoublequoteclose}\ \isakeyword{and}\ A\isanewline |
|
535 \ \ \isakeyword{shows}\ B\isanewline |
|
536 % |
|
537 \isadelimproof |
|
538 % |
|
539 \endisadelimproof |
|
540 % |
|
541 \isatagproof |
|
542 \isacommand{proof}\isamarkupfalse% |
|
543 \ {\isacharminus}\isanewline |
|
544 \ \ \isacommand{from}\isamarkupfalse% |
|
545 \ {\isacharbackquoteopen}{\isasymnot}\ A{\isacharbackquoteclose}\ \isacommand{have}\isamarkupfalse% |
|
546 \ {\isachardoublequoteopen}A\ {\isasymlongrightarrow}\ {\isasymbottom}{\isachardoublequoteclose}\ \isacommand{unfolding}\isamarkupfalse% |
|
547 \ not{\isacharunderscore}def\ \isacommand{{\isachardot}}\isamarkupfalse% |
|
548 \isanewline |
|
549 \ \ \isacommand{from}\isamarkupfalse% |
|
550 \ {\isacharbackquoteopen}A\ {\isasymlongrightarrow}\ {\isasymbottom}{\isacharbackquoteclose}\ \isakeyword{and}\ {\isacharbackquoteopen}A{\isacharbackquoteclose}\ \isacommand{have}\isamarkupfalse% |
|
551 \ {\isasymbottom}\ \isacommand{{\isachardot}{\isachardot}}\isamarkupfalse% |
|
552 \isanewline |
|
553 \ \ \isacommand{then}\isamarkupfalse% |
|
554 \ \isacommand{show}\isamarkupfalse% |
|
555 \ B\ \isacommand{{\isachardot}{\isachardot}}\isamarkupfalse% |
|
556 \isanewline |
|
557 \isacommand{qed}\isamarkupfalse% |
|
558 % |
|
559 \endisatagproof |
|
560 {\isafoldproof}% |
|
561 % |
|
562 \isadelimproof |
|
563 % |
|
564 \endisadelimproof |
|
565 % |
|
566 \isamarkupsubsection{Classical logic% |
|
567 } |
|
568 \isamarkuptrue% |
|
569 % |
|
570 \begin{isamarkuptext}% |
|
571 Subsequently we state the principle of classical contradiction as a |
|
572 local assumption. Thus we refrain from forcing the object-logic |
|
573 into the classical perspective. Within that context, we may derive |
|
574 well-known consequences of the classical principle.% |
|
575 \end{isamarkuptext}% |
|
576 \isamarkuptrue% |
|
577 \isacommand{locale}\isamarkupfalse% |
|
578 \ classical\ {\isacharequal}\isanewline |
|
579 \ \ \isakeyword{assumes}\ classical{\isacharcolon}\ {\isachardoublequoteopen}{\isacharparenleft}{\isasymnot}\ C\ {\isasymLongrightarrow}\ C{\isacharparenright}\ {\isasymLongrightarrow}\ C{\isachardoublequoteclose}\isanewline |
|
580 \isakeyword{begin}\isanewline |
|
581 \isanewline |
|
582 \isacommand{theorem}\isamarkupfalse% |
|
583 \ double{\isacharunderscore}negation{\isacharcolon}\isanewline |
|
584 \ \ \isakeyword{assumes}\ {\isachardoublequoteopen}{\isasymnot}\ {\isasymnot}\ C{\isachardoublequoteclose}\isanewline |
|
585 \ \ \isakeyword{shows}\ C\isanewline |
|
586 % |
|
587 \isadelimproof |
|
588 % |
|
589 \endisadelimproof |
|
590 % |
|
591 \isatagproof |
|
592 \isacommand{proof}\isamarkupfalse% |
|
593 \ {\isacharparenleft}rule\ classical{\isacharparenright}\isanewline |
|
594 \ \ \isacommand{assume}\isamarkupfalse% |
|
595 \ {\isachardoublequoteopen}{\isasymnot}\ C{\isachardoublequoteclose}\isanewline |
|
596 \ \ \isacommand{with}\isamarkupfalse% |
|
597 \ {\isacharbackquoteopen}{\isasymnot}\ {\isasymnot}\ C{\isacharbackquoteclose}\ \isacommand{show}\isamarkupfalse% |
|
598 \ C\ \isacommand{{\isachardot}{\isachardot}}\isamarkupfalse% |
|
599 \isanewline |
|
600 \isacommand{qed}\isamarkupfalse% |
|
601 % |
|
602 \endisatagproof |
|
603 {\isafoldproof}% |
|
604 % |
|
605 \isadelimproof |
|
606 \isanewline |
|
607 % |
|
608 \endisadelimproof |
|
609 \isanewline |
|
610 \isacommand{theorem}\isamarkupfalse% |
|
611 \ tertium{\isacharunderscore}non{\isacharunderscore}datur{\isacharcolon}\ {\isachardoublequoteopen}C\ {\isasymor}\ {\isasymnot}\ C{\isachardoublequoteclose}\isanewline |
|
612 % |
|
613 \isadelimproof |
|
614 % |
|
615 \endisadelimproof |
|
616 % |
|
617 \isatagproof |
|
618 \isacommand{proof}\isamarkupfalse% |
|
619 \ {\isacharparenleft}rule\ double{\isacharunderscore}negation{\isacharparenright}\isanewline |
|
620 \ \ \isacommand{show}\isamarkupfalse% |
|
621 \ {\isachardoublequoteopen}{\isasymnot}\ {\isasymnot}\ {\isacharparenleft}C\ {\isasymor}\ {\isasymnot}\ C{\isacharparenright}{\isachardoublequoteclose}\isanewline |
|
622 \ \ \isacommand{proof}\isamarkupfalse% |
|
623 \isanewline |
|
624 \ \ \ \ \isacommand{assume}\isamarkupfalse% |
|
625 \ {\isachardoublequoteopen}{\isasymnot}\ {\isacharparenleft}C\ {\isasymor}\ {\isasymnot}\ C{\isacharparenright}{\isachardoublequoteclose}\isanewline |
|
626 \ \ \ \ \isacommand{have}\isamarkupfalse% |
|
627 \ {\isachardoublequoteopen}{\isasymnot}\ C{\isachardoublequoteclose}\isanewline |
|
628 \ \ \ \ \isacommand{proof}\isamarkupfalse% |
|
629 \isanewline |
|
630 \ \ \ \ \ \ \isacommand{assume}\isamarkupfalse% |
|
631 \ C\ \isacommand{then}\isamarkupfalse% |
|
632 \ \isacommand{have}\isamarkupfalse% |
|
633 \ {\isachardoublequoteopen}C\ {\isasymor}\ {\isasymnot}\ C{\isachardoublequoteclose}\ \isacommand{{\isachardot}{\isachardot}}\isamarkupfalse% |
|
634 \isanewline |
|
635 \ \ \ \ \ \ \isacommand{with}\isamarkupfalse% |
|
636 \ {\isacharbackquoteopen}{\isasymnot}\ {\isacharparenleft}C\ {\isasymor}\ {\isasymnot}\ C{\isacharparenright}{\isacharbackquoteclose}\ \isacommand{show}\isamarkupfalse% |
|
637 \ {\isasymbottom}\ \isacommand{{\isachardot}{\isachardot}}\isamarkupfalse% |
|
638 \isanewline |
|
639 \ \ \ \ \isacommand{qed}\isamarkupfalse% |
|
640 \isanewline |
|
641 \ \ \ \ \isacommand{then}\isamarkupfalse% |
|
642 \ \isacommand{have}\isamarkupfalse% |
|
643 \ {\isachardoublequoteopen}C\ {\isasymor}\ {\isasymnot}\ C{\isachardoublequoteclose}\ \isacommand{{\isachardot}{\isachardot}}\isamarkupfalse% |
|
644 \isanewline |
|
645 \ \ \ \ \isacommand{with}\isamarkupfalse% |
|
646 \ {\isacharbackquoteopen}{\isasymnot}\ {\isacharparenleft}C\ {\isasymor}\ {\isasymnot}\ C{\isacharparenright}{\isacharbackquoteclose}\ \isacommand{show}\isamarkupfalse% |
|
647 \ {\isasymbottom}\ \isacommand{{\isachardot}{\isachardot}}\isamarkupfalse% |
|
648 \isanewline |
|
649 \ \ \isacommand{qed}\isamarkupfalse% |
|
650 \isanewline |
|
651 \isacommand{qed}\isamarkupfalse% |
|
652 % |
|
653 \endisatagproof |
|
654 {\isafoldproof}% |
|
655 % |
|
656 \isadelimproof |
|
657 % |
|
658 \endisadelimproof |
|
659 % |
|
660 \begin{isamarkuptext}% |
|
661 These examples illustrate both classical reasoning and non-trivial |
|
662 propositional proofs in general. All three rules characterize |
|
663 classical logic independently, but the original rule is already the |
|
664 most convenient to use, because it leaves the conclusion unchanged. |
|
665 Note that \isa{{\isachardoublequote}{\isacharparenleft}{\isasymnot}\ C\ {\isasymLongrightarrow}\ C{\isacharparenright}\ {\isasymLongrightarrow}\ C{\isachardoublequote}} fits again into our format for |
|
666 eliminations, despite the additional twist that the context refers |
|
667 to the main conclusion. So we may write \isa{{\isachardoublequote}classical{\isachardoublequote}} as the |
|
668 Isar statement ``\isa{{\isachardoublequote}{\isasymOBTAINS}\ {\isasymnot}\ thesis{\isachardoublequote}}''. This also |
|
669 explains nicely how classical reasoning really works: whatever the |
|
670 main \isa{thesis} might be, we may always assume its negation!% |
|
671 \end{isamarkuptext}% |
|
672 \isamarkuptrue% |
|
673 \isacommand{end}\isamarkupfalse% |
|
674 % |
|
675 \isamarkupsubsection{Quantifiers% |
|
676 } |
|
677 \isamarkuptrue% |
|
678 % |
|
679 \begin{isamarkuptext}% |
|
680 Representing quantifiers is easy, thanks to the higher-order nature |
|
681 of the underlying framework. According to the well-known technique |
|
682 introduced by Church \cite{church40}, quantifiers are operators on |
|
683 predicates, which are syntactically represented as \isa{{\isachardoublequote}{\isasymlambda}{\isachardoublequote}}-terms |
|
684 of type \isa{{\isachardoublequote}i\ {\isasymRightarrow}\ o{\isachardoublequote}}. Specific binder notation relates \isa{{\isachardoublequote}All\ {\isacharparenleft}{\isasymlambda}x{\isachardot}\ B\ x{\isacharparenright}{\isachardoublequote}} to \isa{{\isachardoublequote}{\isasymforall}x{\isachardot}\ B\ x{\isachardoublequote}} etc.% |
|
685 \end{isamarkuptext}% |
|
686 \isamarkuptrue% |
|
687 \isacommand{axiomatization}\isamarkupfalse% |
|
688 \isanewline |
|
689 \ \ All\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}{\isacharparenleft}i\ {\isasymRightarrow}\ o{\isacharparenright}\ {\isasymRightarrow}\ o{\isachardoublequoteclose}\ \ {\isacharparenleft}\isakeyword{binder}\ {\isachardoublequoteopen}{\isasymforall}{\isachardoublequoteclose}\ {\isadigit{1}}{\isadigit{0}}{\isacharparenright}\ \isakeyword{where}\isanewline |
|
690 \ \ allI\ {\isacharbrackleft}intro{\isacharbrackright}{\isacharcolon}\ {\isachardoublequoteopen}{\isacharparenleft}{\isasymAnd}x{\isachardot}\ B\ x{\isacharparenright}\ {\isasymLongrightarrow}\ {\isasymforall}x{\isachardot}\ B\ x{\isachardoublequoteclose}\ \isakeyword{and}\isanewline |
|
691 \ \ allD\ {\isacharbrackleft}dest{\isacharbrackright}{\isacharcolon}\ {\isachardoublequoteopen}{\isacharparenleft}{\isasymforall}x{\isachardot}\ B\ x{\isacharparenright}\ {\isasymLongrightarrow}\ B\ a{\isachardoublequoteclose}\isanewline |
|
692 \isanewline |
|
693 \isacommand{axiomatization}\isamarkupfalse% |
|
694 \isanewline |
|
695 \ \ Ex\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}{\isacharparenleft}i\ {\isasymRightarrow}\ o{\isacharparenright}\ {\isasymRightarrow}\ o{\isachardoublequoteclose}\ \ {\isacharparenleft}\isakeyword{binder}\ {\isachardoublequoteopen}{\isasymexists}{\isachardoublequoteclose}\ {\isadigit{1}}{\isadigit{0}}{\isacharparenright}\ \isakeyword{where}\isanewline |
|
696 \ \ exI\ {\isacharbrackleft}intro{\isacharbrackright}{\isacharcolon}\ {\isachardoublequoteopen}B\ a\ {\isasymLongrightarrow}\ {\isacharparenleft}{\isasymexists}x{\isachardot}\ B\ x{\isacharparenright}{\isachardoublequoteclose}\ \isakeyword{and}\isanewline |
|
697 \ \ exE\ {\isacharbrackleft}elim{\isacharbrackright}{\isacharcolon}\ {\isachardoublequoteopen}{\isacharparenleft}{\isasymexists}x{\isachardot}\ B\ x{\isacharparenright}\ {\isasymLongrightarrow}\ {\isacharparenleft}{\isasymAnd}x{\isachardot}\ B\ x\ {\isasymLongrightarrow}\ C{\isacharparenright}\ {\isasymLongrightarrow}\ C{\isachardoublequoteclose}% |
|
698 \begin{isamarkuptext}% |
|
699 \noindent The \isa{exE} rule corresponds to an Isar statement |
|
700 ``\isa{{\isachardoublequote}{\isasymASSUMES}\ {\isasymexists}x{\isachardot}\ B\ x\ {\isasymOBTAINS}\ x\ {\isasymWHERE}\ B\ x{\isachardoublequote}}''. In the |
|
701 following example we illustrate quantifier reasoning with all four |
|
702 rules:% |
|
703 \end{isamarkuptext}% |
|
704 \isamarkuptrue% |
|
705 \isacommand{theorem}\isamarkupfalse% |
|
706 \isanewline |
|
707 \ \ \isakeyword{assumes}\ {\isachardoublequoteopen}{\isasymexists}x{\isachardot}\ {\isasymforall}y{\isachardot}\ R\ x\ y{\isachardoublequoteclose}\isanewline |
|
708 \ \ \isakeyword{shows}\ {\isachardoublequoteopen}{\isasymforall}y{\isachardot}\ {\isasymexists}x{\isachardot}\ R\ x\ y{\isachardoublequoteclose}\isanewline |
|
709 % |
|
710 \isadelimproof |
|
711 % |
|
712 \endisadelimproof |
|
713 % |
|
714 \isatagproof |
|
715 \isacommand{proof}\isamarkupfalse% |
|
716 \ \ \ \ % |
|
717 \isamarkupcmt{\isa{{\isachardoublequote}{\isasymforall}{\isachardoublequote}} introduction% |
|
718 } |
|
719 \isanewline |
|
720 \ \ \isacommand{obtain}\isamarkupfalse% |
|
721 \ x\ \isakeyword{where}\ {\isachardoublequoteopen}{\isasymforall}y{\isachardot}\ R\ x\ y{\isachardoublequoteclose}\ \isacommand{using}\isamarkupfalse% |
|
722 \ {\isacharbackquoteopen}{\isasymexists}x{\isachardot}\ {\isasymforall}y{\isachardot}\ R\ x\ y{\isacharbackquoteclose}\ \isacommand{{\isachardot}{\isachardot}}\isamarkupfalse% |
|
723 \ \ \ \ % |
|
724 \isamarkupcmt{\isa{{\isachardoublequote}{\isasymexists}{\isachardoublequote}} elimination% |
|
725 } |
|
726 \isanewline |
|
727 \ \ \isacommand{fix}\isamarkupfalse% |
|
728 \ y\ \isacommand{have}\isamarkupfalse% |
|
729 \ {\isachardoublequoteopen}R\ x\ y{\isachardoublequoteclose}\ \isacommand{using}\isamarkupfalse% |
|
730 \ {\isacharbackquoteopen}{\isasymforall}y{\isachardot}\ R\ x\ y{\isacharbackquoteclose}\ \isacommand{{\isachardot}{\isachardot}}\isamarkupfalse% |
|
731 \ \ \ \ % |
|
732 \isamarkupcmt{\isa{{\isachardoublequote}{\isasymforall}{\isachardoublequote}} destruction% |
|
733 } |
|
734 \isanewline |
|
735 \ \ \isacommand{then}\isamarkupfalse% |
|
736 \ \isacommand{show}\isamarkupfalse% |
|
737 \ {\isachardoublequoteopen}{\isasymexists}x{\isachardot}\ R\ x\ y{\isachardoublequoteclose}\ \isacommand{{\isachardot}{\isachardot}}\isamarkupfalse% |
|
738 \ \ \ \ % |
|
739 \isamarkupcmt{\isa{{\isachardoublequote}{\isasymexists}{\isachardoublequote}} introduction% |
|
740 } |
|
741 \isanewline |
|
742 \isacommand{qed}\isamarkupfalse% |
|
743 % |
|
744 \endisatagproof |
|
745 {\isafoldproof}% |
|
746 % |
|
747 \isadelimproof |
|
748 \isanewline |
|
749 % |
|
750 \endisadelimproof |
|
751 % |
|
752 \isadelimvisible |
|
753 \isanewline |
|
754 % |
|
755 \endisadelimvisible |
|
756 % |
|
757 \isatagvisible |
|
758 \isacommand{end}\isamarkupfalse% |
|
759 % |
|
760 \endisatagvisible |
|
761 {\isafoldvisible}% |
|
762 % |
|
763 \isadelimvisible |
|
764 \isanewline |
|
765 % |
|
766 \endisadelimvisible |
|
767 \end{isabellebody}% |
|
768 %%% Local Variables: |
|
769 %%% mode: latex |
|
770 %%% TeX-master: "root" |
|
771 %%% End: |