|
1 (* Title: HOL/Isar_Examples/Higher_Order_Logic.thy |
|
2 Author: Makarius |
|
3 *) |
|
4 |
|
5 section \<open>Foundations of HOL\<close> |
|
6 |
|
7 theory Higher_Order_Logic |
|
8 imports Pure |
|
9 begin |
|
10 |
|
11 text \<open> |
|
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. |
|
17 \<close> |
|
18 |
|
19 |
|
20 subsection \<open>Pure Logic\<close> |
|
21 |
|
22 class type |
|
23 default_sort type |
|
24 |
|
25 typedecl o |
|
26 instance o :: type .. |
|
27 instance "fun" :: (type, type) type .. |
|
28 |
|
29 |
|
30 subsubsection \<open>Basic logical connectives\<close> |
|
31 |
|
32 judgment Trueprop :: "o \<Rightarrow> prop" ("_" 5) |
|
33 |
|
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" |
|
41 |
|
42 |
|
43 subsubsection \<open>Extensional equality\<close> |
|
44 |
|
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" |
|
48 |
|
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" |
|
52 |
|
53 theorem sym [sym]: |
|
54 assumes "x = y" |
|
55 shows "y = x" |
|
56 using assms by (rule subst) (rule refl) |
|
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 |
|
74 subsubsection \<open>Derived connectives\<close> |
|
75 |
|
76 definition false :: o ("\<bottom>") where "\<bottom> \<equiv> \<forall>A. A" |
|
77 |
|
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 |
|
87 definition true :: o ("\<top>") where "\<top> \<equiv> \<bottom> \<longrightarrow> \<bottom>" |
|
88 |
|
89 theorem trueI [intro]: \<top> |
|
90 unfolding true_def .. |
|
91 |
|
92 |
|
93 definition not :: "o \<Rightarrow> o" ("\<not> _" [40] 40) |
|
94 where "not \<equiv> \<lambda>A. A \<longrightarrow> \<bottom>" |
|
95 |
|
96 abbreviation not_equal :: "'a \<Rightarrow> 'a \<Rightarrow> o" (infixl "\<noteq>" 50) |
|
97 where "x \<noteq> y \<equiv> \<not> (x = y)" |
|
98 |
|
99 theorem notI [intro]: |
|
100 assumes "A \<Longrightarrow> \<bottom>" |
|
101 shows "\<not> A" |
|
102 using assms unfolding not_def .. |
|
103 |
|
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>" .. |
|
110 then show B .. |
|
111 qed |
|
112 |
|
113 lemma notE': "A \<Longrightarrow> \<not> A \<Longrightarrow> B" |
|
114 by (rule notE) |
|
115 |
|
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" |
|
121 |
|
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" |
|
129 proof |
|
130 assume "A \<longrightarrow> B \<longrightarrow> C" |
|
131 also note \<open>A\<close> |
|
132 also note \<open>B\<close> |
|
133 finally show C . |
|
134 qed |
|
135 qed |
|
136 |
|
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] |
|
146 also have "A \<longrightarrow> B \<longrightarrow> A" |
|
147 proof |
|
148 assume A |
|
149 then show "B \<longrightarrow> A" .. |
|
150 qed |
|
151 finally show ?thesis . |
|
152 qed |
|
153 show B |
|
154 proof - |
|
155 note * [of B] |
|
156 also have "A \<longrightarrow> B \<longrightarrow> B" |
|
157 proof |
|
158 show "B \<longrightarrow> B" .. |
|
159 qed |
|
160 finally show ?thesis . |
|
161 qed |
|
162 qed |
|
163 |
|
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" |
|
175 proof |
|
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" |
|
191 proof |
|
192 assume "B \<longrightarrow> C" |
|
193 from this and \<open>B\<close> show C .. |
|
194 qed |
|
195 qed |
|
196 qed |
|
197 |
|
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" |
|
205 proof |
|
206 assume A |
|
207 then show thesis by (rule a) |
|
208 qed |
|
209 also have "B \<longrightarrow> thesis" |
|
210 proof |
|
211 assume B |
|
212 then show thesis by (rule b) |
|
213 qed |
|
214 finally show thesis . |
|
215 qed |
|
216 |
|
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 |
|
221 theorem exI [intro]: "P a \<Longrightarrow> \<exists>x. P x" |
|
222 unfolding Ex_def |
|
223 proof |
|
224 fix C |
|
225 assume "P a" |
|
226 show "(\<forall>x. P x \<longrightarrow> C) \<longrightarrow> C" |
|
227 proof |
|
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 .. |
|
231 qed |
|
232 qed |
|
233 |
|
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" |
|
241 proof |
|
242 fix x |
|
243 show "P x \<longrightarrow> thesis" |
|
244 proof |
|
245 assume "P x" |
|
246 then show thesis by (rule that) |
|
247 qed |
|
248 qed |
|
249 finally show thesis . |
|
250 qed |
|
251 |
|
252 |
|
253 subsection \<open>Classical logic\<close> |
|
254 |
|
255 text \<open> |
|
256 The subsequent rules of classical reasoning are all equivalent. |
|
257 \<close> |
|
258 |
|
259 locale classical = |
|
260 assumes classical: "(\<not> A \<Longrightarrow> A) \<Longrightarrow> A" |
|
261 |
|
262 theorem (in classical) Peirce's_Law: "((A \<longrightarrow> B) \<longrightarrow> A) \<longrightarrow> A" |
|
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 |
|
271 with \<open>\<not> A\<close> show B by (rule contradiction) |
|
272 qed |
|
273 with a show A .. |
|
274 qed |
|
275 qed |
|
276 |
|
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) |
|
283 qed |
|
284 |
|
285 theorem (in classical) tertium_non_datur: "A \<or> \<not> A" |
|
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 |
|
292 assume A then have "A \<or> \<not> A" .. |
|
293 with \<open>\<not> (A \<or> \<not> A)\<close> show \<bottom> by (rule contradiction) |
|
294 qed |
|
295 then have "A \<or> \<not> A" .. |
|
296 with \<open>\<not> (A \<or> \<not> A)\<close> show \<bottom> by (rule contradiction) |
|
297 qed |
|
298 qed |
|
299 |
|
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) |
|
319 assume A |
|
320 then show A . |
|
321 next |
|
322 assume "\<not> A" |
|
323 then show A by (rule *) |
|
324 qed |
|
325 qed |
|
326 |
|
327 end |