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