author | wenzelm |
Sat, 02 Jan 2016 16:32:36 +0100 | |
changeset 62038 | 5651de00bca9 |
parent 61936 | c51ce9ed0b1c |
child 62266 | f4baefee5776 |
permissions | -rw-r--r-- |
61935 | 1 |
(* Title: HOL/Isar_Examples/Higher_Order_Logic.thy |
61759 | 2 |
Author: Makarius |
12360 | 3 |
*) |
4 |
||
59031 | 5 |
section \<open>Foundations of HOL\<close> |
12360 | 6 |
|
60769 | 7 |
theory Higher_Order_Logic |
8 |
imports Pure |
|
9 |
begin |
|
12360 | 10 |
|
59031 | 11 |
text \<open> |
61759 | 12 |
The following theory development demonstrates Higher-Order Logic itself, |
13 |
represented directly within the Pure framework of Isabelle. The ``HOL'' |
|
14 |
logic given here is essentially that of Gordon @{cite "Gordon:1985:HOL"}, |
|
15 |
although we prefer to present basic concepts in a slightly more conventional |
|
16 |
manner oriented towards plain Natural Deduction. |
|
59031 | 17 |
\<close> |
12360 | 18 |
|
19 |
||
59031 | 20 |
subsection \<open>Pure Logic\<close> |
12360 | 21 |
|
55380
4de48353034e
prefer vacuous definitional type classes over axiomatic ones;
wenzelm
parents:
41460
diff
changeset
|
22 |
class type |
36452 | 23 |
default_sort type |
12360 | 24 |
|
25 |
typedecl o |
|
55380
4de48353034e
prefer vacuous definitional type classes over axiomatic ones;
wenzelm
parents:
41460
diff
changeset
|
26 |
instance o :: type .. |
4de48353034e
prefer vacuous definitional type classes over axiomatic ones;
wenzelm
parents:
41460
diff
changeset
|
27 |
instance "fun" :: (type, type) type .. |
12360 | 28 |
|
29 |
||
59031 | 30 |
subsubsection \<open>Basic logical connectives\<close> |
12360 | 31 |
|
61759 | 32 |
judgment Trueprop :: "o \<Rightarrow> prop" ("_" 5) |
12360 | 33 |
|
61759 | 34 |
axiomatization imp :: "o \<Rightarrow> o \<Rightarrow> o" (infixr "\<longrightarrow>" 25) |
35 |
where impI [intro]: "(A \<Longrightarrow> B) \<Longrightarrow> A \<longrightarrow> B" |
|
36 |
and impE [dest, trans]: "A \<longrightarrow> B \<Longrightarrow> A \<Longrightarrow> B" |
|
37 |
||
38 |
axiomatization All :: "('a \<Rightarrow> o) \<Rightarrow> o" (binder "\<forall>" 10) |
|
39 |
where allI [intro]: "(\<And>x. P x) \<Longrightarrow> \<forall>x. P x" |
|
40 |
and allE [dest]: "\<forall>x. P x \<Longrightarrow> P a" |
|
12360 | 41 |
|
42 |
||
59031 | 43 |
subsubsection \<open>Extensional equality\<close> |
12360 | 44 |
|
61759 | 45 |
axiomatization equal :: "'a \<Rightarrow> 'a \<Rightarrow> o" (infixl "=" 50) |
46 |
where refl [intro]: "x = x" |
|
47 |
and subst: "x = y \<Longrightarrow> P x \<Longrightarrow> P y" |
|
12360 | 48 |
|
61936 | 49 |
abbreviation iff :: "o \<Rightarrow> o \<Rightarrow> o" (infixr "\<longleftrightarrow>" 25) |
50 |
where "A \<longleftrightarrow> B \<equiv> A = B" |
|
51 |
||
61759 | 52 |
axiomatization |
53 |
where ext [intro]: "(\<And>x. f x = g x) \<Longrightarrow> f = g" |
|
61936 | 54 |
and iff [intro]: "(A \<Longrightarrow> B) \<Longrightarrow> (B \<Longrightarrow> A) \<Longrightarrow> A \<longleftrightarrow> B" |
12360 | 55 |
|
61759 | 56 |
theorem sym [sym]: |
57 |
assumes "x = y" |
|
58 |
shows "y = x" |
|
59 |
using assms by (rule subst) (rule refl) |
|
12360 | 60 |
|
61 |
lemma [trans]: "x = y \<Longrightarrow> P y \<Longrightarrow> P x" |
|
62 |
by (rule subst) (rule sym) |
|
63 |
||
64 |
lemma [trans]: "P x \<Longrightarrow> x = y \<Longrightarrow> P y" |
|
65 |
by (rule subst) |
|
66 |
||
67 |
theorem trans [trans]: "x = y \<Longrightarrow> y = z \<Longrightarrow> x = z" |
|
68 |
by (rule subst) |
|
69 |
||
61936 | 70 |
theorem iff1 [elim]: "A \<longleftrightarrow> B \<Longrightarrow> A \<Longrightarrow> B" |
12360 | 71 |
by (rule subst) |
72 |
||
61936 | 73 |
theorem iff2 [elim]: "A \<longleftrightarrow> B \<Longrightarrow> B \<Longrightarrow> A" |
12360 | 74 |
by (rule subst) (rule sym) |
75 |
||
76 |
||
59031 | 77 |
subsubsection \<open>Derived connectives\<close> |
12360 | 78 |
|
59031 | 79 |
definition false :: o ("\<bottom>") where "\<bottom> \<equiv> \<forall>A. A" |
21404
eb85850d3eb7
more robust syntax for definition/abbreviation/notation;
wenzelm
parents:
20523
diff
changeset
|
80 |
|
61759 | 81 |
theorem falseE [elim]: |
82 |
assumes "\<bottom>" |
|
83 |
shows A |
|
84 |
proof - |
|
85 |
from \<open>\<bottom>\<close> have "\<forall>A. A" unfolding false_def . |
|
86 |
then show A .. |
|
87 |
qed |
|
88 |
||
89 |
||
59031 | 90 |
definition true :: o ("\<top>") where "\<top> \<equiv> \<bottom> \<longrightarrow> \<bottom>" |
21404
eb85850d3eb7
more robust syntax for definition/abbreviation/notation;
wenzelm
parents:
20523
diff
changeset
|
91 |
|
61759 | 92 |
theorem trueI [intro]: \<top> |
93 |
unfolding true_def .. |
|
94 |
||
95 |
||
59031 | 96 |
definition not :: "o \<Rightarrow> o" ("\<not> _" [40] 40) |
97 |
where "not \<equiv> \<lambda>A. A \<longrightarrow> \<bottom>" |
|
21404
eb85850d3eb7
more robust syntax for definition/abbreviation/notation;
wenzelm
parents:
20523
diff
changeset
|
98 |
|
59031 | 99 |
abbreviation not_equal :: "'a \<Rightarrow> 'a \<Rightarrow> o" (infixl "\<noteq>" 50) |
100 |
where "x \<noteq> y \<equiv> \<not> (x = y)" |
|
12360 | 101 |
|
61759 | 102 |
theorem notI [intro]: |
103 |
assumes "A \<Longrightarrow> \<bottom>" |
|
104 |
shows "\<not> A" |
|
105 |
using assms unfolding not_def .. |
|
12360 | 106 |
|
61759 | 107 |
theorem notE [elim]: |
108 |
assumes "\<not> A" and A |
|
109 |
shows B |
|
110 |
proof - |
|
111 |
from \<open>\<not> A\<close> have "A \<longrightarrow> \<bottom>" unfolding not_def . |
|
112 |
from this and \<open>A\<close> have "\<bottom>" .. |
|
23373 | 113 |
then show B .. |
12360 | 114 |
qed |
115 |
||
116 |
lemma notE': "A \<Longrightarrow> \<not> A \<Longrightarrow> B" |
|
117 |
by (rule notE) |
|
118 |
||
61759 | 119 |
lemmas contradiction = notE notE' \<comment> \<open>proof by contradiction in any order\<close> |
120 |
||
121 |
||
122 |
definition conj :: "o \<Rightarrow> o \<Rightarrow> o" (infixr "\<and>" 35) |
|
123 |
where "conj \<equiv> \<lambda>A B. \<forall>C. (A \<longrightarrow> B \<longrightarrow> C) \<longrightarrow> C" |
|
12360 | 124 |
|
61759 | 125 |
theorem conjI [intro]: |
126 |
assumes A and B |
|
127 |
shows "A \<and> B" |
|
128 |
unfolding conj_def |
|
129 |
proof |
|
130 |
fix C |
|
131 |
show "(A \<longrightarrow> B \<longrightarrow> C) \<longrightarrow> C" |
|
12360 | 132 |
proof |
61759 | 133 |
assume "A \<longrightarrow> B \<longrightarrow> C" |
134 |
also note \<open>A\<close> |
|
135 |
also note \<open>B\<close> |
|
136 |
finally show C . |
|
12360 | 137 |
qed |
138 |
qed |
|
139 |
||
61759 | 140 |
theorem conjE [elim]: |
141 |
assumes "A \<and> B" |
|
142 |
obtains A and B |
|
143 |
proof |
|
144 |
from \<open>A \<and> B\<close> have *: "(A \<longrightarrow> B \<longrightarrow> C) \<longrightarrow> C" for C |
|
145 |
unfolding conj_def .. |
|
146 |
show A |
|
147 |
proof - |
|
148 |
note * [of A] |
|
12360 | 149 |
also have "A \<longrightarrow> B \<longrightarrow> A" |
150 |
proof |
|
151 |
assume A |
|
23373 | 152 |
then show "B \<longrightarrow> A" .. |
12360 | 153 |
qed |
61759 | 154 |
finally show ?thesis . |
155 |
qed |
|
156 |
show B |
|
157 |
proof - |
|
158 |
note * [of B] |
|
12360 | 159 |
also have "A \<longrightarrow> B \<longrightarrow> B" |
160 |
proof |
|
161 |
show "B \<longrightarrow> B" .. |
|
162 |
qed |
|
61759 | 163 |
finally show ?thesis . |
12360 | 164 |
qed |
165 |
qed |
|
166 |
||
61759 | 167 |
|
168 |
definition disj :: "o \<Rightarrow> o \<Rightarrow> o" (infixr "\<or>" 30) |
|
169 |
where "disj \<equiv> \<lambda>A B. \<forall>C. (A \<longrightarrow> C) \<longrightarrow> (B \<longrightarrow> C) \<longrightarrow> C" |
|
170 |
||
171 |
theorem disjI1 [intro]: |
|
172 |
assumes A |
|
173 |
shows "A \<or> B" |
|
174 |
unfolding disj_def |
|
175 |
proof |
|
176 |
fix C |
|
177 |
show "(A \<longrightarrow> C) \<longrightarrow> (B \<longrightarrow> C) \<longrightarrow> C" |
|
12360 | 178 |
proof |
61759 | 179 |
assume "A \<longrightarrow> C" |
180 |
from this and \<open>A\<close> have C .. |
|
181 |
then show "(B \<longrightarrow> C) \<longrightarrow> C" .. |
|
182 |
qed |
|
183 |
qed |
|
184 |
||
185 |
theorem disjI2 [intro]: |
|
186 |
assumes B |
|
187 |
shows "A \<or> B" |
|
188 |
unfolding disj_def |
|
189 |
proof |
|
190 |
fix C |
|
191 |
show "(A \<longrightarrow> C) \<longrightarrow> (B \<longrightarrow> C) \<longrightarrow> C" |
|
192 |
proof |
|
193 |
show "(B \<longrightarrow> C) \<longrightarrow> C" |
|
12360 | 194 |
proof |
61759 | 195 |
assume "B \<longrightarrow> C" |
196 |
from this and \<open>B\<close> show C .. |
|
12360 | 197 |
qed |
198 |
qed |
|
199 |
qed |
|
200 |
||
61759 | 201 |
theorem disjE [elim]: |
202 |
assumes "A \<or> B" |
|
203 |
obtains (a) A | (b) B |
|
204 |
proof - |
|
205 |
from \<open>A \<or> B\<close> have "(A \<longrightarrow> thesis) \<longrightarrow> (B \<longrightarrow> thesis) \<longrightarrow> thesis" |
|
206 |
unfolding disj_def .. |
|
207 |
also have "A \<longrightarrow> thesis" |
|
12360 | 208 |
proof |
60769 | 209 |
assume A |
61759 | 210 |
then show thesis by (rule a) |
12360 | 211 |
qed |
61759 | 212 |
also have "B \<longrightarrow> thesis" |
12360 | 213 |
proof |
60769 | 214 |
assume B |
61759 | 215 |
then show thesis by (rule b) |
12360 | 216 |
qed |
61759 | 217 |
finally show thesis . |
12360 | 218 |
qed |
219 |
||
61759 | 220 |
|
221 |
definition Ex :: "('a \<Rightarrow> o) \<Rightarrow> o" (binder "\<exists>" 10) |
|
222 |
where "\<exists>x. P x \<equiv> \<forall>C. (\<forall>x. P x \<longrightarrow> C) \<longrightarrow> C" |
|
223 |
||
12360 | 224 |
theorem exI [intro]: "P a \<Longrightarrow> \<exists>x. P x" |
61759 | 225 |
unfolding Ex_def |
226 |
proof |
|
227 |
fix C |
|
12360 | 228 |
assume "P a" |
61759 | 229 |
show "(\<forall>x. P x \<longrightarrow> C) \<longrightarrow> C" |
12360 | 230 |
proof |
61759 | 231 |
assume "\<forall>x. P x \<longrightarrow> C" |
232 |
then have "P a \<longrightarrow> C" .. |
|
233 |
from this and \<open>P a\<close> show C .. |
|
12360 | 234 |
qed |
235 |
qed |
|
236 |
||
61759 | 237 |
theorem exE [elim]: |
238 |
assumes "\<exists>x. P x" |
|
239 |
obtains (that) x where "P x" |
|
240 |
proof - |
|
241 |
from \<open>\<exists>x. P x\<close> have "(\<forall>x. P x \<longrightarrow> thesis) \<longrightarrow> thesis" |
|
242 |
unfolding Ex_def .. |
|
243 |
also have "\<forall>x. P x \<longrightarrow> thesis" |
|
12360 | 244 |
proof |
61759 | 245 |
fix x |
246 |
show "P x \<longrightarrow> thesis" |
|
12360 | 247 |
proof |
248 |
assume "P x" |
|
61759 | 249 |
then show thesis by (rule that) |
12360 | 250 |
qed |
251 |
qed |
|
61759 | 252 |
finally show thesis . |
12360 | 253 |
qed |
254 |
||
255 |
||
61936 | 256 |
subsection \<open>Cantor's Theorem\<close> |
257 |
||
258 |
text \<open> |
|
259 |
Cantor's Theorem states that there is no surjection from a set to its |
|
260 |
powerset. The subsequent formulation uses elementary \<open>\<lambda>\<close>-calculus and |
|
261 |
predicate logic, with standard introduction and elimination rules. |
|
262 |
\<close> |
|
263 |
||
264 |
lemma iff_contradiction: |
|
265 |
assumes *: "\<not> A \<longleftrightarrow> A" |
|
266 |
shows C |
|
267 |
proof (rule notE) |
|
268 |
show "\<not> A" |
|
269 |
proof |
|
270 |
assume A |
|
271 |
with * have "\<not> A" .. |
|
272 |
from this and \<open>A\<close> show \<bottom> .. |
|
273 |
qed |
|
274 |
with * show A .. |
|
275 |
qed |
|
276 |
||
62038 | 277 |
theorem Cantor: "\<not> (\<exists>f :: 'a \<Rightarrow> 'a \<Rightarrow> o. \<forall>A. \<exists>x. A = f x)" |
61936 | 278 |
proof |
279 |
assume "\<exists>f :: 'a \<Rightarrow> 'a \<Rightarrow> o. \<forall>A. \<exists>x. A = f x" |
|
280 |
then obtain f :: "'a \<Rightarrow> 'a \<Rightarrow> o" where *: "\<forall>A. \<exists>x. A = f x" .. |
|
281 |
let ?D = "\<lambda>x. \<not> f x x" |
|
282 |
from * have "\<exists>x. ?D = f x" .. |
|
283 |
then obtain a where "?D = f a" .. |
|
284 |
then have "?D a \<longleftrightarrow> f a a" using refl by (rule subst) |
|
285 |
then show \<bottom> by (rule iff_contradiction) |
|
286 |
qed |
|
287 |
||
288 |
||
59031 | 289 |
subsection \<open>Classical logic\<close> |
12360 | 290 |
|
61759 | 291 |
text \<open> |
292 |
The subsequent rules of classical reasoning are all equivalent. |
|
293 |
\<close> |
|
294 |
||
12360 | 295 |
locale classical = |
296 |
assumes classical: "(\<not> A \<Longrightarrow> A) \<Longrightarrow> A" |
|
297 |
||
60769 | 298 |
theorem (in classical) Peirce's_Law: "((A \<longrightarrow> B) \<longrightarrow> A) \<longrightarrow> A" |
12360 | 299 |
proof |
300 |
assume a: "(A \<longrightarrow> B) \<longrightarrow> A" |
|
301 |
show A |
|
302 |
proof (rule classical) |
|
303 |
assume "\<not> A" |
|
304 |
have "A \<longrightarrow> B" |
|
305 |
proof |
|
306 |
assume A |
|
59031 | 307 |
with \<open>\<not> A\<close> show B by (rule contradiction) |
12360 | 308 |
qed |
309 |
with a show A .. |
|
310 |
qed |
|
311 |
qed |
|
312 |
||
61759 | 313 |
theorem (in classical) double_negation: |
314 |
assumes "\<not> \<not> A" |
|
315 |
shows A |
|
316 |
proof (rule classical) |
|
317 |
assume "\<not> A" |
|
318 |
with \<open>\<not> \<not> A\<close> show ?thesis by (rule contradiction) |
|
12360 | 319 |
qed |
320 |
||
60769 | 321 |
theorem (in classical) tertium_non_datur: "A \<or> \<not> A" |
12360 | 322 |
proof (rule double_negation) |
323 |
show "\<not> \<not> (A \<or> \<not> A)" |
|
324 |
proof |
|
325 |
assume "\<not> (A \<or> \<not> A)" |
|
326 |
have "\<not> A" |
|
327 |
proof |
|
23373 | 328 |
assume A then have "A \<or> \<not> A" .. |
59031 | 329 |
with \<open>\<not> (A \<or> \<not> A)\<close> show \<bottom> by (rule contradiction) |
12360 | 330 |
qed |
23373 | 331 |
then have "A \<or> \<not> A" .. |
59031 | 332 |
with \<open>\<not> (A \<or> \<not> A)\<close> show \<bottom> by (rule contradiction) |
12360 | 333 |
qed |
334 |
qed |
|
335 |
||
61759 | 336 |
theorem (in classical) classical_cases: |
337 |
obtains A | "\<not> A" |
|
338 |
using tertium_non_datur |
|
339 |
proof |
|
340 |
assume A |
|
341 |
then show thesis .. |
|
342 |
next |
|
343 |
assume "\<not> A" |
|
344 |
then show thesis .. |
|
345 |
qed |
|
346 |
||
347 |
lemma |
|
348 |
assumes classical_cases: "\<And>A C. (A \<Longrightarrow> C) \<Longrightarrow> (\<not> A \<Longrightarrow> C) \<Longrightarrow> C" |
|
349 |
shows "PROP classical" |
|
350 |
proof |
|
351 |
fix A |
|
352 |
assume *: "\<not> A \<Longrightarrow> A" |
|
353 |
show A |
|
354 |
proof (rule classical_cases) |
|
12360 | 355 |
assume A |
61759 | 356 |
then show A . |
12360 | 357 |
next |
358 |
assume "\<not> A" |
|
61759 | 359 |
then show A by (rule *) |
12573 | 360 |
qed |
361 |
qed |
|
362 |
||
12360 | 363 |
end |