author | wenzelm |
Tue, 02 Aug 2016 18:46:24 +0200 | |
changeset 63585 | f4a308fdf664 |
parent 63532 | b01154b74314 |
child 64475 | d751bef76e5c |
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 |
63585 | 8 |
imports Pure |
60769 | 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 |
|
63585 | 79 |
definition false :: o ("\<bottom>") |
80 |
where "\<bottom> \<equiv> \<forall>A. A" |
|
21404
eb85850d3eb7
more robust syntax for definition/abbreviation/notation;
wenzelm
parents:
20523
diff
changeset
|
81 |
|
61759 | 82 |
theorem falseE [elim]: |
83 |
assumes "\<bottom>" |
|
84 |
shows A |
|
85 |
proof - |
|
63532
b01154b74314
provide Pure.simp/simp_all, which only know about meta-equality;
wenzelm
parents:
62266
diff
changeset
|
86 |
from \<open>\<bottom>\<close> have "\<forall>A. A" by (simp only: false_def) |
61759 | 87 |
then show A .. |
88 |
qed |
|
89 |
||
90 |
||
63585 | 91 |
definition true :: o ("\<top>") |
92 |
where "\<top> \<equiv> \<bottom> \<longrightarrow> \<bottom>" |
|
21404
eb85850d3eb7
more robust syntax for definition/abbreviation/notation;
wenzelm
parents:
20523
diff
changeset
|
93 |
|
61759 | 94 |
theorem trueI [intro]: \<top> |
95 |
unfolding true_def .. |
|
96 |
||
97 |
||
59031 | 98 |
definition not :: "o \<Rightarrow> o" ("\<not> _" [40] 40) |
99 |
where "not \<equiv> \<lambda>A. A \<longrightarrow> \<bottom>" |
|
21404
eb85850d3eb7
more robust syntax for definition/abbreviation/notation;
wenzelm
parents:
20523
diff
changeset
|
100 |
|
59031 | 101 |
abbreviation not_equal :: "'a \<Rightarrow> 'a \<Rightarrow> o" (infixl "\<noteq>" 50) |
102 |
where "x \<noteq> y \<equiv> \<not> (x = y)" |
|
12360 | 103 |
|
61759 | 104 |
theorem notI [intro]: |
105 |
assumes "A \<Longrightarrow> \<bottom>" |
|
106 |
shows "\<not> A" |
|
107 |
using assms unfolding not_def .. |
|
12360 | 108 |
|
61759 | 109 |
theorem notE [elim]: |
110 |
assumes "\<not> A" and A |
|
111 |
shows B |
|
112 |
proof - |
|
63532
b01154b74314
provide Pure.simp/simp_all, which only know about meta-equality;
wenzelm
parents:
62266
diff
changeset
|
113 |
from \<open>\<not> A\<close> have "A \<longrightarrow> \<bottom>" by (simp only: not_def) |
61759 | 114 |
from this and \<open>A\<close> have "\<bottom>" .. |
23373 | 115 |
then show B .. |
12360 | 116 |
qed |
117 |
||
118 |
lemma notE': "A \<Longrightarrow> \<not> A \<Longrightarrow> B" |
|
119 |
by (rule notE) |
|
120 |
||
61759 | 121 |
lemmas contradiction = notE notE' \<comment> \<open>proof by contradiction in any order\<close> |
122 |
||
123 |
||
124 |
definition conj :: "o \<Rightarrow> o \<Rightarrow> o" (infixr "\<and>" 35) |
|
125 |
where "conj \<equiv> \<lambda>A B. \<forall>C. (A \<longrightarrow> B \<longrightarrow> C) \<longrightarrow> C" |
|
12360 | 126 |
|
61759 | 127 |
theorem conjI [intro]: |
128 |
assumes A and B |
|
129 |
shows "A \<and> B" |
|
130 |
unfolding conj_def |
|
131 |
proof |
|
132 |
fix C |
|
133 |
show "(A \<longrightarrow> B \<longrightarrow> C) \<longrightarrow> C" |
|
12360 | 134 |
proof |
61759 | 135 |
assume "A \<longrightarrow> B \<longrightarrow> C" |
136 |
also note \<open>A\<close> |
|
137 |
also note \<open>B\<close> |
|
138 |
finally show C . |
|
12360 | 139 |
qed |
140 |
qed |
|
141 |
||
61759 | 142 |
theorem conjE [elim]: |
143 |
assumes "A \<and> B" |
|
144 |
obtains A and B |
|
145 |
proof |
|
146 |
from \<open>A \<and> B\<close> have *: "(A \<longrightarrow> B \<longrightarrow> C) \<longrightarrow> C" for C |
|
147 |
unfolding conj_def .. |
|
148 |
show A |
|
149 |
proof - |
|
150 |
note * [of A] |
|
12360 | 151 |
also have "A \<longrightarrow> B \<longrightarrow> A" |
152 |
proof |
|
153 |
assume A |
|
23373 | 154 |
then show "B \<longrightarrow> A" .. |
12360 | 155 |
qed |
61759 | 156 |
finally show ?thesis . |
157 |
qed |
|
158 |
show B |
|
159 |
proof - |
|
160 |
note * [of B] |
|
12360 | 161 |
also have "A \<longrightarrow> B \<longrightarrow> B" |
162 |
proof |
|
163 |
show "B \<longrightarrow> B" .. |
|
164 |
qed |
|
61759 | 165 |
finally show ?thesis . |
12360 | 166 |
qed |
167 |
qed |
|
168 |
||
61759 | 169 |
|
170 |
definition disj :: "o \<Rightarrow> o \<Rightarrow> o" (infixr "\<or>" 30) |
|
171 |
where "disj \<equiv> \<lambda>A B. \<forall>C. (A \<longrightarrow> C) \<longrightarrow> (B \<longrightarrow> C) \<longrightarrow> C" |
|
172 |
||
173 |
theorem disjI1 [intro]: |
|
174 |
assumes A |
|
175 |
shows "A \<or> B" |
|
176 |
unfolding disj_def |
|
177 |
proof |
|
178 |
fix C |
|
179 |
show "(A \<longrightarrow> C) \<longrightarrow> (B \<longrightarrow> C) \<longrightarrow> C" |
|
12360 | 180 |
proof |
61759 | 181 |
assume "A \<longrightarrow> C" |
182 |
from this and \<open>A\<close> have C .. |
|
183 |
then show "(B \<longrightarrow> C) \<longrightarrow> C" .. |
|
184 |
qed |
|
185 |
qed |
|
186 |
||
187 |
theorem disjI2 [intro]: |
|
188 |
assumes B |
|
189 |
shows "A \<or> B" |
|
190 |
unfolding disj_def |
|
191 |
proof |
|
192 |
fix C |
|
193 |
show "(A \<longrightarrow> C) \<longrightarrow> (B \<longrightarrow> C) \<longrightarrow> C" |
|
194 |
proof |
|
195 |
show "(B \<longrightarrow> C) \<longrightarrow> C" |
|
12360 | 196 |
proof |
61759 | 197 |
assume "B \<longrightarrow> C" |
198 |
from this and \<open>B\<close> show C .. |
|
12360 | 199 |
qed |
200 |
qed |
|
201 |
qed |
|
202 |
||
61759 | 203 |
theorem disjE [elim]: |
204 |
assumes "A \<or> B" |
|
205 |
obtains (a) A | (b) B |
|
206 |
proof - |
|
207 |
from \<open>A \<or> B\<close> have "(A \<longrightarrow> thesis) \<longrightarrow> (B \<longrightarrow> thesis) \<longrightarrow> thesis" |
|
208 |
unfolding disj_def .. |
|
209 |
also have "A \<longrightarrow> thesis" |
|
12360 | 210 |
proof |
60769 | 211 |
assume A |
61759 | 212 |
then show thesis by (rule a) |
12360 | 213 |
qed |
61759 | 214 |
also have "B \<longrightarrow> thesis" |
12360 | 215 |
proof |
60769 | 216 |
assume B |
61759 | 217 |
then show thesis by (rule b) |
12360 | 218 |
qed |
61759 | 219 |
finally show thesis . |
12360 | 220 |
qed |
221 |
||
61759 | 222 |
|
223 |
definition Ex :: "('a \<Rightarrow> o) \<Rightarrow> o" (binder "\<exists>" 10) |
|
224 |
where "\<exists>x. P x \<equiv> \<forall>C. (\<forall>x. P x \<longrightarrow> C) \<longrightarrow> C" |
|
225 |
||
12360 | 226 |
theorem exI [intro]: "P a \<Longrightarrow> \<exists>x. P x" |
61759 | 227 |
unfolding Ex_def |
228 |
proof |
|
229 |
fix C |
|
12360 | 230 |
assume "P a" |
61759 | 231 |
show "(\<forall>x. P x \<longrightarrow> C) \<longrightarrow> C" |
12360 | 232 |
proof |
61759 | 233 |
assume "\<forall>x. P x \<longrightarrow> C" |
234 |
then have "P a \<longrightarrow> C" .. |
|
235 |
from this and \<open>P a\<close> show C .. |
|
12360 | 236 |
qed |
237 |
qed |
|
238 |
||
61759 | 239 |
theorem exE [elim]: |
240 |
assumes "\<exists>x. P x" |
|
241 |
obtains (that) x where "P x" |
|
242 |
proof - |
|
243 |
from \<open>\<exists>x. P x\<close> have "(\<forall>x. P x \<longrightarrow> thesis) \<longrightarrow> thesis" |
|
244 |
unfolding Ex_def .. |
|
245 |
also have "\<forall>x. P x \<longrightarrow> thesis" |
|
12360 | 246 |
proof |
61759 | 247 |
fix x |
248 |
show "P x \<longrightarrow> thesis" |
|
12360 | 249 |
proof |
250 |
assume "P x" |
|
61759 | 251 |
then show thesis by (rule that) |
12360 | 252 |
qed |
253 |
qed |
|
61759 | 254 |
finally show thesis . |
12360 | 255 |
qed |
256 |
||
257 |
||
61936 | 258 |
subsection \<open>Cantor's Theorem\<close> |
259 |
||
260 |
text \<open> |
|
261 |
Cantor's Theorem states that there is no surjection from a set to its |
|
262 |
powerset. The subsequent formulation uses elementary \<open>\<lambda>\<close>-calculus and |
|
263 |
predicate logic, with standard introduction and elimination rules. |
|
264 |
\<close> |
|
265 |
||
266 |
lemma iff_contradiction: |
|
267 |
assumes *: "\<not> A \<longleftrightarrow> A" |
|
268 |
shows C |
|
269 |
proof (rule notE) |
|
270 |
show "\<not> A" |
|
271 |
proof |
|
272 |
assume A |
|
273 |
with * have "\<not> A" .. |
|
274 |
from this and \<open>A\<close> show \<bottom> .. |
|
275 |
qed |
|
276 |
with * show A .. |
|
277 |
qed |
|
278 |
||
62038 | 279 |
theorem Cantor: "\<not> (\<exists>f :: 'a \<Rightarrow> 'a \<Rightarrow> o. \<forall>A. \<exists>x. A = f x)" |
61936 | 280 |
proof |
281 |
assume "\<exists>f :: 'a \<Rightarrow> 'a \<Rightarrow> o. \<forall>A. \<exists>x. A = f x" |
|
282 |
then obtain f :: "'a \<Rightarrow> 'a \<Rightarrow> o" where *: "\<forall>A. \<exists>x. A = f x" .. |
|
283 |
let ?D = "\<lambda>x. \<not> f x x" |
|
284 |
from * have "\<exists>x. ?D = f x" .. |
|
285 |
then obtain a where "?D = f a" .. |
|
286 |
then have "?D a \<longleftrightarrow> f a a" using refl by (rule subst) |
|
62266 | 287 |
then have "\<not> f a a \<longleftrightarrow> f a a" . |
61936 | 288 |
then show \<bottom> by (rule iff_contradiction) |
289 |
qed |
|
290 |
||
291 |
||
59031 | 292 |
subsection \<open>Classical logic\<close> |
12360 | 293 |
|
61759 | 294 |
text \<open> |
295 |
The subsequent rules of classical reasoning are all equivalent. |
|
296 |
\<close> |
|
297 |
||
12360 | 298 |
locale classical = |
299 |
assumes classical: "(\<not> A \<Longrightarrow> A) \<Longrightarrow> A" |
|
300 |
||
60769 | 301 |
theorem (in classical) Peirce's_Law: "((A \<longrightarrow> B) \<longrightarrow> A) \<longrightarrow> A" |
12360 | 302 |
proof |
303 |
assume a: "(A \<longrightarrow> B) \<longrightarrow> A" |
|
304 |
show A |
|
305 |
proof (rule classical) |
|
306 |
assume "\<not> A" |
|
307 |
have "A \<longrightarrow> B" |
|
308 |
proof |
|
309 |
assume A |
|
59031 | 310 |
with \<open>\<not> A\<close> show B by (rule contradiction) |
12360 | 311 |
qed |
312 |
with a show A .. |
|
313 |
qed |
|
314 |
qed |
|
315 |
||
61759 | 316 |
theorem (in classical) double_negation: |
317 |
assumes "\<not> \<not> A" |
|
318 |
shows A |
|
319 |
proof (rule classical) |
|
320 |
assume "\<not> A" |
|
321 |
with \<open>\<not> \<not> A\<close> show ?thesis by (rule contradiction) |
|
12360 | 322 |
qed |
323 |
||
60769 | 324 |
theorem (in classical) tertium_non_datur: "A \<or> \<not> A" |
12360 | 325 |
proof (rule double_negation) |
326 |
show "\<not> \<not> (A \<or> \<not> A)" |
|
327 |
proof |
|
328 |
assume "\<not> (A \<or> \<not> A)" |
|
329 |
have "\<not> A" |
|
330 |
proof |
|
23373 | 331 |
assume A then have "A \<or> \<not> A" .. |
59031 | 332 |
with \<open>\<not> (A \<or> \<not> A)\<close> show \<bottom> by (rule contradiction) |
12360 | 333 |
qed |
23373 | 334 |
then have "A \<or> \<not> A" .. |
59031 | 335 |
with \<open>\<not> (A \<or> \<not> A)\<close> show \<bottom> by (rule contradiction) |
12360 | 336 |
qed |
337 |
qed |
|
338 |
||
61759 | 339 |
theorem (in classical) classical_cases: |
340 |
obtains A | "\<not> A" |
|
341 |
using tertium_non_datur |
|
342 |
proof |
|
343 |
assume A |
|
344 |
then show thesis .. |
|
345 |
next |
|
346 |
assume "\<not> A" |
|
347 |
then show thesis .. |
|
348 |
qed |
|
349 |
||
350 |
lemma |
|
351 |
assumes classical_cases: "\<And>A C. (A \<Longrightarrow> C) \<Longrightarrow> (\<not> A \<Longrightarrow> C) \<Longrightarrow> C" |
|
352 |
shows "PROP classical" |
|
353 |
proof |
|
354 |
fix A |
|
355 |
assume *: "\<not> A \<Longrightarrow> A" |
|
356 |
show A |
|
357 |
proof (rule classical_cases) |
|
12360 | 358 |
assume A |
61759 | 359 |
then show A . |
12360 | 360 |
next |
361 |
assume "\<not> A" |
|
61759 | 362 |
then show A by (rule *) |
12573 | 363 |
qed |
364 |
qed |
|
365 |
||
12360 | 366 |
end |