author | wenzelm |
Sat, 26 Dec 2015 19:27:46 +0100 | |
changeset 61935 | 6512e84cc9f5 |
parent 61759 | src/HOL/ex/Higher_Order_Logic.thy@49353865e539 |
child 61936 | c51ce9ed0b1c |
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 |
|
61759 | 49 |
axiomatization |
50 |
where ext [intro]: "(\<And>x. f x = g x) \<Longrightarrow> f = g" |
|
51 |
and iff [intro]: "(A \<Longrightarrow> B) \<Longrightarrow> (B \<Longrightarrow> A) \<Longrightarrow> A = B" |
|
12360 | 52 |
|
61759 | 53 |
theorem sym [sym]: |
54 |
assumes "x = y" |
|
55 |
shows "y = x" |
|
56 |
using assms by (rule subst) (rule refl) |
|
12360 | 57 |
|
58 |
lemma [trans]: "x = y \<Longrightarrow> P y \<Longrightarrow> P x" |
|
59 |
by (rule subst) (rule sym) |
|
60 |
||
61 |
lemma [trans]: "P x \<Longrightarrow> x = y \<Longrightarrow> P y" |
|
62 |
by (rule subst) |
|
63 |
||
64 |
theorem trans [trans]: "x = y \<Longrightarrow> y = z \<Longrightarrow> x = z" |
|
65 |
by (rule subst) |
|
66 |
||
67 |
theorem iff1 [elim]: "A = B \<Longrightarrow> A \<Longrightarrow> B" |
|
68 |
by (rule subst) |
|
69 |
||
70 |
theorem iff2 [elim]: "A = B \<Longrightarrow> B \<Longrightarrow> A" |
|
71 |
by (rule subst) (rule sym) |
|
72 |
||
73 |
||
59031 | 74 |
subsubsection \<open>Derived connectives\<close> |
12360 | 75 |
|
59031 | 76 |
definition false :: o ("\<bottom>") where "\<bottom> \<equiv> \<forall>A. A" |
21404
eb85850d3eb7
more robust syntax for definition/abbreviation/notation;
wenzelm
parents:
20523
diff
changeset
|
77 |
|
61759 | 78 |
theorem falseE [elim]: |
79 |
assumes "\<bottom>" |
|
80 |
shows A |
|
81 |
proof - |
|
82 |
from \<open>\<bottom>\<close> have "\<forall>A. A" unfolding false_def . |
|
83 |
then show A .. |
|
84 |
qed |
|
85 |
||
86 |
||
59031 | 87 |
definition true :: o ("\<top>") where "\<top> \<equiv> \<bottom> \<longrightarrow> \<bottom>" |
21404
eb85850d3eb7
more robust syntax for definition/abbreviation/notation;
wenzelm
parents:
20523
diff
changeset
|
88 |
|
61759 | 89 |
theorem trueI [intro]: \<top> |
90 |
unfolding true_def .. |
|
91 |
||
92 |
||
59031 | 93 |
definition not :: "o \<Rightarrow> o" ("\<not> _" [40] 40) |
94 |
where "not \<equiv> \<lambda>A. A \<longrightarrow> \<bottom>" |
|
21404
eb85850d3eb7
more robust syntax for definition/abbreviation/notation;
wenzelm
parents:
20523
diff
changeset
|
95 |
|
59031 | 96 |
abbreviation not_equal :: "'a \<Rightarrow> 'a \<Rightarrow> o" (infixl "\<noteq>" 50) |
97 |
where "x \<noteq> y \<equiv> \<not> (x = y)" |
|
12360 | 98 |
|
61759 | 99 |
theorem notI [intro]: |
100 |
assumes "A \<Longrightarrow> \<bottom>" |
|
101 |
shows "\<not> A" |
|
102 |
using assms unfolding not_def .. |
|
12360 | 103 |
|
61759 | 104 |
theorem notE [elim]: |
105 |
assumes "\<not> A" and A |
|
106 |
shows B |
|
107 |
proof - |
|
108 |
from \<open>\<not> A\<close> have "A \<longrightarrow> \<bottom>" unfolding not_def . |
|
109 |
from this and \<open>A\<close> have "\<bottom>" .. |
|
23373 | 110 |
then show B .. |
12360 | 111 |
qed |
112 |
||
113 |
lemma notE': "A \<Longrightarrow> \<not> A \<Longrightarrow> B" |
|
114 |
by (rule notE) |
|
115 |
||
61759 | 116 |
lemmas contradiction = notE notE' \<comment> \<open>proof by contradiction in any order\<close> |
117 |
||
118 |
||
119 |
definition conj :: "o \<Rightarrow> o \<Rightarrow> o" (infixr "\<and>" 35) |
|
120 |
where "conj \<equiv> \<lambda>A B. \<forall>C. (A \<longrightarrow> B \<longrightarrow> C) \<longrightarrow> C" |
|
12360 | 121 |
|
61759 | 122 |
theorem conjI [intro]: |
123 |
assumes A and B |
|
124 |
shows "A \<and> B" |
|
125 |
unfolding conj_def |
|
126 |
proof |
|
127 |
fix C |
|
128 |
show "(A \<longrightarrow> B \<longrightarrow> C) \<longrightarrow> C" |
|
12360 | 129 |
proof |
61759 | 130 |
assume "A \<longrightarrow> B \<longrightarrow> C" |
131 |
also note \<open>A\<close> |
|
132 |
also note \<open>B\<close> |
|
133 |
finally show C . |
|
12360 | 134 |
qed |
135 |
qed |
|
136 |
||
61759 | 137 |
theorem conjE [elim]: |
138 |
assumes "A \<and> B" |
|
139 |
obtains A and B |
|
140 |
proof |
|
141 |
from \<open>A \<and> B\<close> have *: "(A \<longrightarrow> B \<longrightarrow> C) \<longrightarrow> C" for C |
|
142 |
unfolding conj_def .. |
|
143 |
show A |
|
144 |
proof - |
|
145 |
note * [of A] |
|
12360 | 146 |
also have "A \<longrightarrow> B \<longrightarrow> A" |
147 |
proof |
|
148 |
assume A |
|
23373 | 149 |
then show "B \<longrightarrow> A" .. |
12360 | 150 |
qed |
61759 | 151 |
finally show ?thesis . |
152 |
qed |
|
153 |
show B |
|
154 |
proof - |
|
155 |
note * [of B] |
|
12360 | 156 |
also have "A \<longrightarrow> B \<longrightarrow> B" |
157 |
proof |
|
158 |
show "B \<longrightarrow> B" .. |
|
159 |
qed |
|
61759 | 160 |
finally show ?thesis . |
12360 | 161 |
qed |
162 |
qed |
|
163 |
||
61759 | 164 |
|
165 |
definition disj :: "o \<Rightarrow> o \<Rightarrow> o" (infixr "\<or>" 30) |
|
166 |
where "disj \<equiv> \<lambda>A B. \<forall>C. (A \<longrightarrow> C) \<longrightarrow> (B \<longrightarrow> C) \<longrightarrow> C" |
|
167 |
||
168 |
theorem disjI1 [intro]: |
|
169 |
assumes A |
|
170 |
shows "A \<or> B" |
|
171 |
unfolding disj_def |
|
172 |
proof |
|
173 |
fix C |
|
174 |
show "(A \<longrightarrow> C) \<longrightarrow> (B \<longrightarrow> C) \<longrightarrow> C" |
|
12360 | 175 |
proof |
61759 | 176 |
assume "A \<longrightarrow> C" |
177 |
from this and \<open>A\<close> have C .. |
|
178 |
then show "(B \<longrightarrow> C) \<longrightarrow> C" .. |
|
179 |
qed |
|
180 |
qed |
|
181 |
||
182 |
theorem disjI2 [intro]: |
|
183 |
assumes B |
|
184 |
shows "A \<or> B" |
|
185 |
unfolding disj_def |
|
186 |
proof |
|
187 |
fix C |
|
188 |
show "(A \<longrightarrow> C) \<longrightarrow> (B \<longrightarrow> C) \<longrightarrow> C" |
|
189 |
proof |
|
190 |
show "(B \<longrightarrow> C) \<longrightarrow> C" |
|
12360 | 191 |
proof |
61759 | 192 |
assume "B \<longrightarrow> C" |
193 |
from this and \<open>B\<close> show C .. |
|
12360 | 194 |
qed |
195 |
qed |
|
196 |
qed |
|
197 |
||
61759 | 198 |
theorem disjE [elim]: |
199 |
assumes "A \<or> B" |
|
200 |
obtains (a) A | (b) B |
|
201 |
proof - |
|
202 |
from \<open>A \<or> B\<close> have "(A \<longrightarrow> thesis) \<longrightarrow> (B \<longrightarrow> thesis) \<longrightarrow> thesis" |
|
203 |
unfolding disj_def .. |
|
204 |
also have "A \<longrightarrow> thesis" |
|
12360 | 205 |
proof |
60769 | 206 |
assume A |
61759 | 207 |
then show thesis by (rule a) |
12360 | 208 |
qed |
61759 | 209 |
also have "B \<longrightarrow> thesis" |
12360 | 210 |
proof |
60769 | 211 |
assume B |
61759 | 212 |
then show thesis by (rule b) |
12360 | 213 |
qed |
61759 | 214 |
finally show thesis . |
12360 | 215 |
qed |
216 |
||
61759 | 217 |
|
218 |
definition Ex :: "('a \<Rightarrow> o) \<Rightarrow> o" (binder "\<exists>" 10) |
|
219 |
where "\<exists>x. P x \<equiv> \<forall>C. (\<forall>x. P x \<longrightarrow> C) \<longrightarrow> C" |
|
220 |
||
12360 | 221 |
theorem exI [intro]: "P a \<Longrightarrow> \<exists>x. P x" |
61759 | 222 |
unfolding Ex_def |
223 |
proof |
|
224 |
fix C |
|
12360 | 225 |
assume "P a" |
61759 | 226 |
show "(\<forall>x. P x \<longrightarrow> C) \<longrightarrow> C" |
12360 | 227 |
proof |
61759 | 228 |
assume "\<forall>x. P x \<longrightarrow> C" |
229 |
then have "P a \<longrightarrow> C" .. |
|
230 |
from this and \<open>P a\<close> show C .. |
|
12360 | 231 |
qed |
232 |
qed |
|
233 |
||
61759 | 234 |
theorem exE [elim]: |
235 |
assumes "\<exists>x. P x" |
|
236 |
obtains (that) x where "P x" |
|
237 |
proof - |
|
238 |
from \<open>\<exists>x. P x\<close> have "(\<forall>x. P x \<longrightarrow> thesis) \<longrightarrow> thesis" |
|
239 |
unfolding Ex_def .. |
|
240 |
also have "\<forall>x. P x \<longrightarrow> thesis" |
|
12360 | 241 |
proof |
61759 | 242 |
fix x |
243 |
show "P x \<longrightarrow> thesis" |
|
12360 | 244 |
proof |
245 |
assume "P x" |
|
61759 | 246 |
then show thesis by (rule that) |
12360 | 247 |
qed |
248 |
qed |
|
61759 | 249 |
finally show thesis . |
12360 | 250 |
qed |
251 |
||
252 |
||
59031 | 253 |
subsection \<open>Classical logic\<close> |
12360 | 254 |
|
61759 | 255 |
text \<open> |
256 |
The subsequent rules of classical reasoning are all equivalent. |
|
257 |
\<close> |
|
258 |
||
12360 | 259 |
locale classical = |
260 |
assumes classical: "(\<not> A \<Longrightarrow> A) \<Longrightarrow> A" |
|
261 |
||
60769 | 262 |
theorem (in classical) Peirce's_Law: "((A \<longrightarrow> B) \<longrightarrow> A) \<longrightarrow> A" |
12360 | 263 |
proof |
264 |
assume a: "(A \<longrightarrow> B) \<longrightarrow> A" |
|
265 |
show A |
|
266 |
proof (rule classical) |
|
267 |
assume "\<not> A" |
|
268 |
have "A \<longrightarrow> B" |
|
269 |
proof |
|
270 |
assume A |
|
59031 | 271 |
with \<open>\<not> A\<close> show B by (rule contradiction) |
12360 | 272 |
qed |
273 |
with a show A .. |
|
274 |
qed |
|
275 |
qed |
|
276 |
||
61759 | 277 |
theorem (in classical) double_negation: |
278 |
assumes "\<not> \<not> A" |
|
279 |
shows A |
|
280 |
proof (rule classical) |
|
281 |
assume "\<not> A" |
|
282 |
with \<open>\<not> \<not> A\<close> show ?thesis by (rule contradiction) |
|
12360 | 283 |
qed |
284 |
||
60769 | 285 |
theorem (in classical) tertium_non_datur: "A \<or> \<not> A" |
12360 | 286 |
proof (rule double_negation) |
287 |
show "\<not> \<not> (A \<or> \<not> A)" |
|
288 |
proof |
|
289 |
assume "\<not> (A \<or> \<not> A)" |
|
290 |
have "\<not> A" |
|
291 |
proof |
|
23373 | 292 |
assume A then have "A \<or> \<not> A" .. |
59031 | 293 |
with \<open>\<not> (A \<or> \<not> A)\<close> show \<bottom> by (rule contradiction) |
12360 | 294 |
qed |
23373 | 295 |
then have "A \<or> \<not> A" .. |
59031 | 296 |
with \<open>\<not> (A \<or> \<not> A)\<close> show \<bottom> by (rule contradiction) |
12360 | 297 |
qed |
298 |
qed |
|
299 |
||
61759 | 300 |
theorem (in classical) classical_cases: |
301 |
obtains A | "\<not> A" |
|
302 |
using tertium_non_datur |
|
303 |
proof |
|
304 |
assume A |
|
305 |
then show thesis .. |
|
306 |
next |
|
307 |
assume "\<not> A" |
|
308 |
then show thesis .. |
|
309 |
qed |
|
310 |
||
311 |
lemma |
|
312 |
assumes classical_cases: "\<And>A C. (A \<Longrightarrow> C) \<Longrightarrow> (\<not> A \<Longrightarrow> C) \<Longrightarrow> C" |
|
313 |
shows "PROP classical" |
|
314 |
proof |
|
315 |
fix A |
|
316 |
assume *: "\<not> A \<Longrightarrow> A" |
|
317 |
show A |
|
318 |
proof (rule classical_cases) |
|
12360 | 319 |
assume A |
61759 | 320 |
then show A . |
12360 | 321 |
next |
322 |
assume "\<not> A" |
|
61759 | 323 |
then show A by (rule *) |
12573 | 324 |
qed |
325 |
qed |
|
326 |
||
12360 | 327 |
end |