author | haftmann |
Tue, 10 Jul 2007 17:30:50 +0200 | |
changeset 23709 | fd31da8f752a |
parent 23393 | 31781b2de73d |
child 24097 | 86734ba03ca2 |
permissions | -rw-r--r-- |
1268 | 1 |
(* Title: FOL/IFOL.thy |
35 | 2 |
ID: $Id$ |
11677 | 3 |
Author: Lawrence C Paulson and Markus Wenzel |
4 |
*) |
|
35 | 5 |
|
11677 | 6 |
header {* Intuitionistic first-order logic *} |
35 | 7 |
|
15481 | 8 |
theory IFOL |
9 |
imports Pure |
|
23155 | 10 |
uses |
11 |
"~~/src/Provers/splitter.ML" |
|
12 |
"~~/src/Provers/hypsubst.ML" |
|
23171 | 13 |
"~~/src/Tools/IsaPlanner/zipper.ML" |
14 |
"~~/src/Tools/IsaPlanner/isand.ML" |
|
15 |
"~~/src/Tools/IsaPlanner/rw_tools.ML" |
|
16 |
"~~/src/Tools/IsaPlanner/rw_inst.ML" |
|
23155 | 17 |
"~~/src/Provers/eqsubst.ML" |
18 |
"~~/src/Provers/induct_method.ML" |
|
19 |
"~~/src/Provers/classical.ML" |
|
20 |
"~~/src/Provers/blast.ML" |
|
21 |
"~~/src/Provers/clasimp.ML" |
|
22 |
"~~/src/Provers/quantifier1.ML" |
|
23 |
"~~/src/Provers/project_rule.ML" |
|
24 |
("fologic.ML") |
|
25 |
("hypsubstdata.ML") |
|
26 |
("intprover.ML") |
|
15481 | 27 |
begin |
7355
4c43090659ca
proper bootstrap of IFOL/FOL theories and packages;
wenzelm
parents:
6340
diff
changeset
|
28 |
|
0 | 29 |
|
11677 | 30 |
subsection {* Syntax and axiomatic basis *} |
31 |
||
3906 | 32 |
global |
33 |
||
14854 | 34 |
classes "term" |
7355
4c43090659ca
proper bootstrap of IFOL/FOL theories and packages;
wenzelm
parents:
6340
diff
changeset
|
35 |
defaultsort "term" |
0 | 36 |
|
7355
4c43090659ca
proper bootstrap of IFOL/FOL theories and packages;
wenzelm
parents:
6340
diff
changeset
|
37 |
typedecl o |
79 | 38 |
|
11747 | 39 |
judgment |
40 |
Trueprop :: "o => prop" ("(_)" 5) |
|
0 | 41 |
|
11747 | 42 |
consts |
7355
4c43090659ca
proper bootstrap of IFOL/FOL theories and packages;
wenzelm
parents:
6340
diff
changeset
|
43 |
True :: o |
4c43090659ca
proper bootstrap of IFOL/FOL theories and packages;
wenzelm
parents:
6340
diff
changeset
|
44 |
False :: o |
79 | 45 |
|
46 |
(* Connectives *) |
|
47 |
||
17276 | 48 |
"op =" :: "['a, 'a] => o" (infixl "=" 50) |
35 | 49 |
|
7355
4c43090659ca
proper bootstrap of IFOL/FOL theories and packages;
wenzelm
parents:
6340
diff
changeset
|
50 |
Not :: "o => o" ("~ _" [40] 40) |
17276 | 51 |
"op &" :: "[o, o] => o" (infixr "&" 35) |
52 |
"op |" :: "[o, o] => o" (infixr "|" 30) |
|
53 |
"op -->" :: "[o, o] => o" (infixr "-->" 25) |
|
54 |
"op <->" :: "[o, o] => o" (infixr "<->" 25) |
|
79 | 55 |
|
56 |
(* Quantifiers *) |
|
57 |
||
7355
4c43090659ca
proper bootstrap of IFOL/FOL theories and packages;
wenzelm
parents:
6340
diff
changeset
|
58 |
All :: "('a => o) => o" (binder "ALL " 10) |
4c43090659ca
proper bootstrap of IFOL/FOL theories and packages;
wenzelm
parents:
6340
diff
changeset
|
59 |
Ex :: "('a => o) => o" (binder "EX " 10) |
4c43090659ca
proper bootstrap of IFOL/FOL theories and packages;
wenzelm
parents:
6340
diff
changeset
|
60 |
Ex1 :: "('a => o) => o" (binder "EX! " 10) |
79 | 61 |
|
0 | 62 |
|
19363 | 63 |
abbreviation |
21404
eb85850d3eb7
more robust syntax for definition/abbreviation/notation;
wenzelm
parents:
21210
diff
changeset
|
64 |
not_equal :: "['a, 'a] => o" (infixl "~=" 50) where |
19120
353d349740de
not_equal: replaced syntax translation by abbreviation;
wenzelm
parents:
18861
diff
changeset
|
65 |
"x ~= y == ~ (x = y)" |
79 | 66 |
|
21210 | 67 |
notation (xsymbols) |
19656
09be06943252
tuned concrete syntax -- abbreviation/const_syntax;
wenzelm
parents:
19380
diff
changeset
|
68 |
not_equal (infixl "\<noteq>" 50) |
19363 | 69 |
|
21210 | 70 |
notation (HTML output) |
19656
09be06943252
tuned concrete syntax -- abbreviation/const_syntax;
wenzelm
parents:
19380
diff
changeset
|
71 |
not_equal (infixl "\<noteq>" 50) |
19363 | 72 |
|
21524 | 73 |
notation (xsymbols) |
21539 | 74 |
Not ("\<not> _" [40] 40) and |
75 |
"op &" (infixr "\<and>" 35) and |
|
76 |
"op |" (infixr "\<or>" 30) and |
|
77 |
All (binder "\<forall>" 10) and |
|
78 |
Ex (binder "\<exists>" 10) and |
|
79 |
Ex1 (binder "\<exists>!" 10) and |
|
21524 | 80 |
"op -->" (infixr "\<longrightarrow>" 25) and |
81 |
"op <->" (infixr "\<longleftrightarrow>" 25) |
|
35 | 82 |
|
21524 | 83 |
notation (HTML output) |
21539 | 84 |
Not ("\<not> _" [40] 40) and |
85 |
"op &" (infixr "\<and>" 35) and |
|
86 |
"op |" (infixr "\<or>" 30) and |
|
87 |
All (binder "\<forall>" 10) and |
|
88 |
Ex (binder "\<exists>" 10) and |
|
89 |
Ex1 (binder "\<exists>!" 10) |
|
6340 | 90 |
|
3932 | 91 |
local |
3906 | 92 |
|
14236 | 93 |
finalconsts |
94 |
False All Ex |
|
95 |
"op =" |
|
96 |
"op &" |
|
97 |
"op |" |
|
98 |
"op -->" |
|
99 |
||
7355
4c43090659ca
proper bootstrap of IFOL/FOL theories and packages;
wenzelm
parents:
6340
diff
changeset
|
100 |
axioms |
0 | 101 |
|
79 | 102 |
(* Equality *) |
0 | 103 |
|
7355
4c43090659ca
proper bootstrap of IFOL/FOL theories and packages;
wenzelm
parents:
6340
diff
changeset
|
104 |
refl: "a=a" |
0 | 105 |
|
79 | 106 |
(* Propositional logic *) |
0 | 107 |
|
7355
4c43090659ca
proper bootstrap of IFOL/FOL theories and packages;
wenzelm
parents:
6340
diff
changeset
|
108 |
conjI: "[| P; Q |] ==> P&Q" |
4c43090659ca
proper bootstrap of IFOL/FOL theories and packages;
wenzelm
parents:
6340
diff
changeset
|
109 |
conjunct1: "P&Q ==> P" |
4c43090659ca
proper bootstrap of IFOL/FOL theories and packages;
wenzelm
parents:
6340
diff
changeset
|
110 |
conjunct2: "P&Q ==> Q" |
0 | 111 |
|
7355
4c43090659ca
proper bootstrap of IFOL/FOL theories and packages;
wenzelm
parents:
6340
diff
changeset
|
112 |
disjI1: "P ==> P|Q" |
4c43090659ca
proper bootstrap of IFOL/FOL theories and packages;
wenzelm
parents:
6340
diff
changeset
|
113 |
disjI2: "Q ==> P|Q" |
4c43090659ca
proper bootstrap of IFOL/FOL theories and packages;
wenzelm
parents:
6340
diff
changeset
|
114 |
disjE: "[| P|Q; P ==> R; Q ==> R |] ==> R" |
0 | 115 |
|
7355
4c43090659ca
proper bootstrap of IFOL/FOL theories and packages;
wenzelm
parents:
6340
diff
changeset
|
116 |
impI: "(P ==> Q) ==> P-->Q" |
4c43090659ca
proper bootstrap of IFOL/FOL theories and packages;
wenzelm
parents:
6340
diff
changeset
|
117 |
mp: "[| P-->Q; P |] ==> Q" |
0 | 118 |
|
7355
4c43090659ca
proper bootstrap of IFOL/FOL theories and packages;
wenzelm
parents:
6340
diff
changeset
|
119 |
FalseE: "False ==> P" |
4c43090659ca
proper bootstrap of IFOL/FOL theories and packages;
wenzelm
parents:
6340
diff
changeset
|
120 |
|
79 | 121 |
(* Quantifiers *) |
0 | 122 |
|
7355
4c43090659ca
proper bootstrap of IFOL/FOL theories and packages;
wenzelm
parents:
6340
diff
changeset
|
123 |
allI: "(!!x. P(x)) ==> (ALL x. P(x))" |
4c43090659ca
proper bootstrap of IFOL/FOL theories and packages;
wenzelm
parents:
6340
diff
changeset
|
124 |
spec: "(ALL x. P(x)) ==> P(x)" |
0 | 125 |
|
7355
4c43090659ca
proper bootstrap of IFOL/FOL theories and packages;
wenzelm
parents:
6340
diff
changeset
|
126 |
exI: "P(x) ==> (EX x. P(x))" |
4c43090659ca
proper bootstrap of IFOL/FOL theories and packages;
wenzelm
parents:
6340
diff
changeset
|
127 |
exE: "[| EX x. P(x); !!x. P(x) ==> R |] ==> R" |
0 | 128 |
|
129 |
(* Reflection *) |
|
130 |
||
7355
4c43090659ca
proper bootstrap of IFOL/FOL theories and packages;
wenzelm
parents:
6340
diff
changeset
|
131 |
eq_reflection: "(x=y) ==> (x==y)" |
4c43090659ca
proper bootstrap of IFOL/FOL theories and packages;
wenzelm
parents:
6340
diff
changeset
|
132 |
iff_reflection: "(P<->Q) ==> (P==Q)" |
0 | 133 |
|
4092 | 134 |
|
19756 | 135 |
lemmas strip = impI allI |
136 |
||
137 |
||
15377 | 138 |
text{*Thanks to Stephan Merz*} |
139 |
theorem subst: |
|
140 |
assumes eq: "a = b" and p: "P(a)" |
|
141 |
shows "P(b)" |
|
142 |
proof - |
|
143 |
from eq have meta: "a \<equiv> b" |
|
144 |
by (rule eq_reflection) |
|
145 |
from p show ?thesis |
|
146 |
by (unfold meta) |
|
147 |
qed |
|
148 |
||
149 |
||
14236 | 150 |
defs |
151 |
(* Definitions *) |
|
152 |
||
153 |
True_def: "True == False-->False" |
|
154 |
not_def: "~P == P-->False" |
|
155 |
iff_def: "P<->Q == (P-->Q) & (Q-->P)" |
|
156 |
||
157 |
(* Unique existence *) |
|
158 |
||
159 |
ex1_def: "Ex1(P) == EX x. P(x) & (ALL y. P(y) --> y=x)" |
|
160 |
||
13779 | 161 |
|
11677 | 162 |
subsection {* Lemmas and proof tools *} |
163 |
||
21539 | 164 |
lemma TrueI: True |
165 |
unfolding True_def by (rule impI) |
|
166 |
||
167 |
||
168 |
(*** Sequent-style elimination rules for & --> and ALL ***) |
|
169 |
||
170 |
lemma conjE: |
|
171 |
assumes major: "P & Q" |
|
172 |
and r: "[| P; Q |] ==> R" |
|
173 |
shows R |
|
174 |
apply (rule r) |
|
175 |
apply (rule major [THEN conjunct1]) |
|
176 |
apply (rule major [THEN conjunct2]) |
|
177 |
done |
|
178 |
||
179 |
lemma impE: |
|
180 |
assumes major: "P --> Q" |
|
181 |
and P |
|
182 |
and r: "Q ==> R" |
|
183 |
shows R |
|
184 |
apply (rule r) |
|
185 |
apply (rule major [THEN mp]) |
|
186 |
apply (rule `P`) |
|
187 |
done |
|
188 |
||
189 |
lemma allE: |
|
190 |
assumes major: "ALL x. P(x)" |
|
191 |
and r: "P(x) ==> R" |
|
192 |
shows R |
|
193 |
apply (rule r) |
|
194 |
apply (rule major [THEN spec]) |
|
195 |
done |
|
196 |
||
197 |
(*Duplicates the quantifier; for use with eresolve_tac*) |
|
198 |
lemma all_dupE: |
|
199 |
assumes major: "ALL x. P(x)" |
|
200 |
and r: "[| P(x); ALL x. P(x) |] ==> R" |
|
201 |
shows R |
|
202 |
apply (rule r) |
|
203 |
apply (rule major [THEN spec]) |
|
204 |
apply (rule major) |
|
205 |
done |
|
206 |
||
207 |
||
208 |
(*** Negation rules, which translate between ~P and P-->False ***) |
|
209 |
||
210 |
lemma notI: "(P ==> False) ==> ~P" |
|
211 |
unfolding not_def by (erule impI) |
|
212 |
||
213 |
lemma notE: "[| ~P; P |] ==> R" |
|
214 |
unfolding not_def by (erule mp [THEN FalseE]) |
|
215 |
||
216 |
lemma rev_notE: "[| P; ~P |] ==> R" |
|
217 |
by (erule notE) |
|
218 |
||
219 |
(*This is useful with the special implication rules for each kind of P. *) |
|
220 |
lemma not_to_imp: |
|
221 |
assumes "~P" |
|
222 |
and r: "P --> False ==> Q" |
|
223 |
shows Q |
|
224 |
apply (rule r) |
|
225 |
apply (rule impI) |
|
226 |
apply (erule notE [OF `~P`]) |
|
227 |
done |
|
228 |
||
229 |
(* For substitution into an assumption P, reduce Q to P-->Q, substitute into |
|
230 |
this implication, then apply impI to move P back into the assumptions. |
|
231 |
To specify P use something like |
|
232 |
eres_inst_tac [ ("P","ALL y. ?S(x,y)") ] rev_mp 1 *) |
|
233 |
lemma rev_mp: "[| P; P --> Q |] ==> Q" |
|
234 |
by (erule mp) |
|
235 |
||
236 |
(*Contrapositive of an inference rule*) |
|
237 |
lemma contrapos: |
|
238 |
assumes major: "~Q" |
|
239 |
and minor: "P ==> Q" |
|
240 |
shows "~P" |
|
241 |
apply (rule major [THEN notE, THEN notI]) |
|
242 |
apply (erule minor) |
|
243 |
done |
|
244 |
||
245 |
||
246 |
(*** Modus Ponens Tactics ***) |
|
247 |
||
248 |
(*Finds P-->Q and P in the assumptions, replaces implication by Q *) |
|
249 |
ML {* |
|
22139 | 250 |
fun mp_tac i = eresolve_tac [@{thm notE}, @{thm impE}] i THEN assume_tac i |
251 |
fun eq_mp_tac i = eresolve_tac [@{thm notE}, @{thm impE}] i THEN eq_assume_tac i |
|
21539 | 252 |
*} |
253 |
||
254 |
||
255 |
(*** If-and-only-if ***) |
|
256 |
||
257 |
lemma iffI: "[| P ==> Q; Q ==> P |] ==> P<->Q" |
|
258 |
apply (unfold iff_def) |
|
259 |
apply (rule conjI) |
|
260 |
apply (erule impI) |
|
261 |
apply (erule impI) |
|
262 |
done |
|
263 |
||
264 |
||
265 |
(*Observe use of rewrite_rule to unfold "<->" in meta-assumptions (prems) *) |
|
266 |
lemma iffE: |
|
267 |
assumes major: "P <-> Q" |
|
268 |
and r: "P-->Q ==> Q-->P ==> R" |
|
269 |
shows R |
|
270 |
apply (insert major, unfold iff_def) |
|
271 |
apply (erule conjE) |
|
272 |
apply (erule r) |
|
273 |
apply assumption |
|
274 |
done |
|
275 |
||
276 |
(* Destruct rules for <-> similar to Modus Ponens *) |
|
277 |
||
278 |
lemma iffD1: "[| P <-> Q; P |] ==> Q" |
|
279 |
apply (unfold iff_def) |
|
280 |
apply (erule conjunct1 [THEN mp]) |
|
281 |
apply assumption |
|
282 |
done |
|
283 |
||
284 |
lemma iffD2: "[| P <-> Q; Q |] ==> P" |
|
285 |
apply (unfold iff_def) |
|
286 |
apply (erule conjunct2 [THEN mp]) |
|
287 |
apply assumption |
|
288 |
done |
|
289 |
||
290 |
lemma rev_iffD1: "[| P; P <-> Q |] ==> Q" |
|
291 |
apply (erule iffD1) |
|
292 |
apply assumption |
|
293 |
done |
|
294 |
||
295 |
lemma rev_iffD2: "[| Q; P <-> Q |] ==> P" |
|
296 |
apply (erule iffD2) |
|
297 |
apply assumption |
|
298 |
done |
|
299 |
||
300 |
lemma iff_refl: "P <-> P" |
|
301 |
by (rule iffI) |
|
302 |
||
303 |
lemma iff_sym: "Q <-> P ==> P <-> Q" |
|
304 |
apply (erule iffE) |
|
305 |
apply (rule iffI) |
|
306 |
apply (assumption | erule mp)+ |
|
307 |
done |
|
308 |
||
309 |
lemma iff_trans: "[| P <-> Q; Q<-> R |] ==> P <-> R" |
|
310 |
apply (rule iffI) |
|
311 |
apply (assumption | erule iffE | erule (1) notE impE)+ |
|
312 |
done |
|
313 |
||
314 |
||
315 |
(*** Unique existence. NOTE THAT the following 2 quantifications |
|
316 |
EX!x such that [EX!y such that P(x,y)] (sequential) |
|
317 |
EX!x,y such that P(x,y) (simultaneous) |
|
318 |
do NOT mean the same thing. The parser treats EX!x y.P(x,y) as sequential. |
|
319 |
***) |
|
320 |
||
321 |
lemma ex1I: |
|
23393 | 322 |
"P(a) \<Longrightarrow> (!!x. P(x) ==> x=a) \<Longrightarrow> EX! x. P(x)" |
21539 | 323 |
apply (unfold ex1_def) |
23393 | 324 |
apply (assumption | rule exI conjI allI impI)+ |
21539 | 325 |
done |
326 |
||
327 |
(*Sometimes easier to use: the premises have no shared variables. Safe!*) |
|
328 |
lemma ex_ex1I: |
|
23393 | 329 |
"EX x. P(x) \<Longrightarrow> (!!x y. [| P(x); P(y) |] ==> x=y) \<Longrightarrow> EX! x. P(x)" |
330 |
apply (erule exE) |
|
331 |
apply (rule ex1I) |
|
332 |
apply assumption |
|
333 |
apply assumption |
|
21539 | 334 |
done |
335 |
||
336 |
lemma ex1E: |
|
23393 | 337 |
"EX! x. P(x) \<Longrightarrow> (!!x. [| P(x); ALL y. P(y) --> y=x |] ==> R) \<Longrightarrow> R" |
338 |
apply (unfold ex1_def) |
|
21539 | 339 |
apply (assumption | erule exE conjE)+ |
340 |
done |
|
341 |
||
342 |
||
343 |
(*** <-> congruence rules for simplification ***) |
|
344 |
||
345 |
(*Use iffE on a premise. For conj_cong, imp_cong, all_cong, ex_cong*) |
|
346 |
ML {* |
|
22139 | 347 |
fun iff_tac prems i = |
348 |
resolve_tac (prems RL @{thms iffE}) i THEN |
|
349 |
REPEAT1 (eresolve_tac [@{thm asm_rl}, @{thm mp}] i) |
|
21539 | 350 |
*} |
351 |
||
352 |
lemma conj_cong: |
|
353 |
assumes "P <-> P'" |
|
354 |
and "P' ==> Q <-> Q'" |
|
355 |
shows "(P&Q) <-> (P'&Q')" |
|
356 |
apply (insert assms) |
|
357 |
apply (assumption | rule iffI conjI | erule iffE conjE mp | |
|
358 |
tactic {* iff_tac (thms "assms") 1 *})+ |
|
359 |
done |
|
360 |
||
361 |
(*Reversed congruence rule! Used in ZF/Order*) |
|
362 |
lemma conj_cong2: |
|
363 |
assumes "P <-> P'" |
|
364 |
and "P' ==> Q <-> Q'" |
|
365 |
shows "(Q&P) <-> (Q'&P')" |
|
366 |
apply (insert assms) |
|
367 |
apply (assumption | rule iffI conjI | erule iffE conjE mp | |
|
368 |
tactic {* iff_tac (thms "assms") 1 *})+ |
|
369 |
done |
|
370 |
||
371 |
lemma disj_cong: |
|
372 |
assumes "P <-> P'" and "Q <-> Q'" |
|
373 |
shows "(P|Q) <-> (P'|Q')" |
|
374 |
apply (insert assms) |
|
375 |
apply (erule iffE disjE disjI1 disjI2 | assumption | rule iffI | erule (1) notE impE)+ |
|
376 |
done |
|
377 |
||
378 |
lemma imp_cong: |
|
379 |
assumes "P <-> P'" |
|
380 |
and "P' ==> Q <-> Q'" |
|
381 |
shows "(P-->Q) <-> (P'-->Q')" |
|
382 |
apply (insert assms) |
|
383 |
apply (assumption | rule iffI impI | erule iffE | erule (1) notE impE | |
|
384 |
tactic {* iff_tac (thms "assms") 1 *})+ |
|
385 |
done |
|
386 |
||
387 |
lemma iff_cong: "[| P <-> P'; Q <-> Q' |] ==> (P<->Q) <-> (P'<->Q')" |
|
388 |
apply (erule iffE | assumption | rule iffI | erule (1) notE impE)+ |
|
389 |
done |
|
390 |
||
391 |
lemma not_cong: "P <-> P' ==> ~P <-> ~P'" |
|
392 |
apply (assumption | rule iffI notI | erule (1) notE impE | erule iffE notE)+ |
|
393 |
done |
|
394 |
||
395 |
lemma all_cong: |
|
396 |
assumes "!!x. P(x) <-> Q(x)" |
|
397 |
shows "(ALL x. P(x)) <-> (ALL x. Q(x))" |
|
398 |
apply (assumption | rule iffI allI | erule (1) notE impE | erule allE | |
|
399 |
tactic {* iff_tac (thms "assms") 1 *})+ |
|
400 |
done |
|
401 |
||
402 |
lemma ex_cong: |
|
403 |
assumes "!!x. P(x) <-> Q(x)" |
|
404 |
shows "(EX x. P(x)) <-> (EX x. Q(x))" |
|
405 |
apply (erule exE | assumption | rule iffI exI | erule (1) notE impE | |
|
406 |
tactic {* iff_tac (thms "assms") 1 *})+ |
|
407 |
done |
|
408 |
||
409 |
lemma ex1_cong: |
|
410 |
assumes "!!x. P(x) <-> Q(x)" |
|
411 |
shows "(EX! x. P(x)) <-> (EX! x. Q(x))" |
|
412 |
apply (erule ex1E spec [THEN mp] | assumption | rule iffI ex1I | erule (1) notE impE | |
|
413 |
tactic {* iff_tac (thms "assms") 1 *})+ |
|
414 |
done |
|
415 |
||
416 |
(*** Equality rules ***) |
|
417 |
||
418 |
lemma sym: "a=b ==> b=a" |
|
419 |
apply (erule subst) |
|
420 |
apply (rule refl) |
|
421 |
done |
|
422 |
||
423 |
lemma trans: "[| a=b; b=c |] ==> a=c" |
|
424 |
apply (erule subst, assumption) |
|
425 |
done |
|
426 |
||
427 |
(** **) |
|
428 |
lemma not_sym: "b ~= a ==> a ~= b" |
|
429 |
apply (erule contrapos) |
|
430 |
apply (erule sym) |
|
431 |
done |
|
432 |
||
433 |
(* Two theorms for rewriting only one instance of a definition: |
|
434 |
the first for definitions of formulae and the second for terms *) |
|
435 |
||
436 |
lemma def_imp_iff: "(A == B) ==> A <-> B" |
|
437 |
apply unfold |
|
438 |
apply (rule iff_refl) |
|
439 |
done |
|
440 |
||
441 |
lemma meta_eq_to_obj_eq: "(A == B) ==> A = B" |
|
442 |
apply unfold |
|
443 |
apply (rule refl) |
|
444 |
done |
|
445 |
||
446 |
lemma meta_eq_to_iff: "x==y ==> x<->y" |
|
447 |
by unfold (rule iff_refl) |
|
448 |
||
449 |
(*substitution*) |
|
450 |
lemma ssubst: "[| b = a; P(a) |] ==> P(b)" |
|
451 |
apply (drule sym) |
|
452 |
apply (erule (1) subst) |
|
453 |
done |
|
454 |
||
455 |
(*A special case of ex1E that would otherwise need quantifier expansion*) |
|
456 |
lemma ex1_equalsE: |
|
457 |
"[| EX! x. P(x); P(a); P(b) |] ==> a=b" |
|
458 |
apply (erule ex1E) |
|
459 |
apply (rule trans) |
|
460 |
apply (rule_tac [2] sym) |
|
461 |
apply (assumption | erule spec [THEN mp])+ |
|
462 |
done |
|
463 |
||
464 |
(** Polymorphic congruence rules **) |
|
465 |
||
466 |
lemma subst_context: "[| a=b |] ==> t(a)=t(b)" |
|
467 |
apply (erule ssubst) |
|
468 |
apply (rule refl) |
|
469 |
done |
|
470 |
||
471 |
lemma subst_context2: "[| a=b; c=d |] ==> t(a,c)=t(b,d)" |
|
472 |
apply (erule ssubst)+ |
|
473 |
apply (rule refl) |
|
474 |
done |
|
475 |
||
476 |
lemma subst_context3: "[| a=b; c=d; e=f |] ==> t(a,c,e)=t(b,d,f)" |
|
477 |
apply (erule ssubst)+ |
|
478 |
apply (rule refl) |
|
479 |
done |
|
480 |
||
481 |
(*Useful with eresolve_tac for proving equalties from known equalities. |
|
482 |
a = b |
|
483 |
| | |
|
484 |
c = d *) |
|
485 |
lemma box_equals: "[| a=b; a=c; b=d |] ==> c=d" |
|
486 |
apply (rule trans) |
|
487 |
apply (rule trans) |
|
488 |
apply (rule sym) |
|
489 |
apply assumption+ |
|
490 |
done |
|
491 |
||
492 |
(*Dual of box_equals: for proving equalities backwards*) |
|
493 |
lemma simp_equals: "[| a=c; b=d; c=d |] ==> a=b" |
|
494 |
apply (rule trans) |
|
495 |
apply (rule trans) |
|
496 |
apply assumption+ |
|
497 |
apply (erule sym) |
|
498 |
done |
|
499 |
||
500 |
(** Congruence rules for predicate letters **) |
|
501 |
||
502 |
lemma pred1_cong: "a=a' ==> P(a) <-> P(a')" |
|
503 |
apply (rule iffI) |
|
504 |
apply (erule (1) subst) |
|
505 |
apply (erule (1) ssubst) |
|
506 |
done |
|
507 |
||
508 |
lemma pred2_cong: "[| a=a'; b=b' |] ==> P(a,b) <-> P(a',b')" |
|
509 |
apply (rule iffI) |
|
510 |
apply (erule subst)+ |
|
511 |
apply assumption |
|
512 |
apply (erule ssubst)+ |
|
513 |
apply assumption |
|
514 |
done |
|
515 |
||
516 |
lemma pred3_cong: "[| a=a'; b=b'; c=c' |] ==> P(a,b,c) <-> P(a',b',c')" |
|
517 |
apply (rule iffI) |
|
518 |
apply (erule subst)+ |
|
519 |
apply assumption |
|
520 |
apply (erule ssubst)+ |
|
521 |
apply assumption |
|
522 |
done |
|
523 |
||
524 |
(*special cases for free variables P, Q, R, S -- up to 3 arguments*) |
|
525 |
||
526 |
ML {* |
|
527 |
bind_thms ("pred_congs", |
|
528 |
List.concat (map (fn c => |
|
529 |
map (fn th => read_instantiate [("P",c)] th) |
|
22139 | 530 |
[@{thm pred1_cong}, @{thm pred2_cong}, @{thm pred3_cong}]) |
21539 | 531 |
(explode"PQRS"))) |
532 |
*} |
|
533 |
||
534 |
(*special case for the equality predicate!*) |
|
535 |
lemma eq_cong: "[| a = a'; b = b' |] ==> a = b <-> a' = b'" |
|
536 |
apply (erule (1) pred2_cong) |
|
537 |
done |
|
538 |
||
539 |
||
540 |
(*** Simplifications of assumed implications. |
|
541 |
Roy Dyckhoff has proved that conj_impE, disj_impE, and imp_impE |
|
542 |
used with mp_tac (restricted to atomic formulae) is COMPLETE for |
|
543 |
intuitionistic propositional logic. See |
|
544 |
R. Dyckhoff, Contraction-free sequent calculi for intuitionistic logic |
|
545 |
(preprint, University of St Andrews, 1991) ***) |
|
546 |
||
547 |
lemma conj_impE: |
|
548 |
assumes major: "(P&Q)-->S" |
|
549 |
and r: "P-->(Q-->S) ==> R" |
|
550 |
shows R |
|
551 |
by (assumption | rule conjI impI major [THEN mp] r)+ |
|
552 |
||
553 |
lemma disj_impE: |
|
554 |
assumes major: "(P|Q)-->S" |
|
555 |
and r: "[| P-->S; Q-->S |] ==> R" |
|
556 |
shows R |
|
557 |
by (assumption | rule disjI1 disjI2 impI major [THEN mp] r)+ |
|
558 |
||
559 |
(*Simplifies the implication. Classical version is stronger. |
|
560 |
Still UNSAFE since Q must be provable -- backtracking needed. *) |
|
561 |
lemma imp_impE: |
|
562 |
assumes major: "(P-->Q)-->S" |
|
563 |
and r1: "[| P; Q-->S |] ==> Q" |
|
564 |
and r2: "S ==> R" |
|
565 |
shows R |
|
566 |
by (assumption | rule impI major [THEN mp] r1 r2)+ |
|
567 |
||
568 |
(*Simplifies the implication. Classical version is stronger. |
|
569 |
Still UNSAFE since ~P must be provable -- backtracking needed. *) |
|
570 |
lemma not_impE: |
|
23393 | 571 |
"~P --> S \<Longrightarrow> (P ==> False) \<Longrightarrow> (S ==> R) \<Longrightarrow> R" |
572 |
apply (drule mp) |
|
573 |
apply (rule notI) |
|
574 |
apply assumption |
|
575 |
apply assumption |
|
21539 | 576 |
done |
577 |
||
578 |
(*Simplifies the implication. UNSAFE. *) |
|
579 |
lemma iff_impE: |
|
580 |
assumes major: "(P<->Q)-->S" |
|
581 |
and r1: "[| P; Q-->S |] ==> Q" |
|
582 |
and r2: "[| Q; P-->S |] ==> P" |
|
583 |
and r3: "S ==> R" |
|
584 |
shows R |
|
585 |
apply (assumption | rule iffI impI major [THEN mp] r1 r2 r3)+ |
|
586 |
done |
|
587 |
||
588 |
(*What if (ALL x.~~P(x)) --> ~~(ALL x.P(x)) is an assumption? UNSAFE*) |
|
589 |
lemma all_impE: |
|
590 |
assumes major: "(ALL x. P(x))-->S" |
|
591 |
and r1: "!!x. P(x)" |
|
592 |
and r2: "S ==> R" |
|
593 |
shows R |
|
23393 | 594 |
apply (rule allI impI major [THEN mp] r1 r2)+ |
21539 | 595 |
done |
596 |
||
597 |
(*Unsafe: (EX x.P(x))-->S is equivalent to ALL x.P(x)-->S. *) |
|
598 |
lemma ex_impE: |
|
599 |
assumes major: "(EX x. P(x))-->S" |
|
600 |
and r: "P(x)-->S ==> R" |
|
601 |
shows R |
|
602 |
apply (assumption | rule exI impI major [THEN mp] r)+ |
|
603 |
done |
|
604 |
||
605 |
(*** Courtesy of Krzysztof Grabczewski ***) |
|
606 |
||
607 |
lemma disj_imp_disj: |
|
23393 | 608 |
"P|Q \<Longrightarrow> (P==>R) \<Longrightarrow> (Q==>S) \<Longrightarrow> R|S" |
609 |
apply (erule disjE) |
|
21539 | 610 |
apply (rule disjI1) apply assumption |
611 |
apply (rule disjI2) apply assumption |
|
612 |
done |
|
11734 | 613 |
|
18481 | 614 |
ML {* |
615 |
structure ProjectRule = ProjectRuleFun |
|
616 |
(struct |
|
22139 | 617 |
val conjunct1 = @{thm conjunct1} |
618 |
val conjunct2 = @{thm conjunct2} |
|
619 |
val mp = @{thm mp} |
|
18481 | 620 |
end) |
621 |
*} |
|
622 |
||
7355
4c43090659ca
proper bootstrap of IFOL/FOL theories and packages;
wenzelm
parents:
6340
diff
changeset
|
623 |
use "fologic.ML" |
21539 | 624 |
|
625 |
lemma thin_refl: "!!X. [|x=x; PROP W|] ==> PROP W" . |
|
626 |
||
9886 | 627 |
use "hypsubstdata.ML" |
628 |
setup hypsubst_setup |
|
7355
4c43090659ca
proper bootstrap of IFOL/FOL theories and packages;
wenzelm
parents:
6340
diff
changeset
|
629 |
use "intprover.ML" |
4c43090659ca
proper bootstrap of IFOL/FOL theories and packages;
wenzelm
parents:
6340
diff
changeset
|
630 |
|
4092 | 631 |
|
12875 | 632 |
subsection {* Intuitionistic Reasoning *} |
12368 | 633 |
|
12349 | 634 |
lemma impE': |
12937
0c4fd7529467
clarified syntax of ``long'' statements: fixes/assumes/shows;
wenzelm
parents:
12875
diff
changeset
|
635 |
assumes 1: "P --> Q" |
0c4fd7529467
clarified syntax of ``long'' statements: fixes/assumes/shows;
wenzelm
parents:
12875
diff
changeset
|
636 |
and 2: "Q ==> R" |
0c4fd7529467
clarified syntax of ``long'' statements: fixes/assumes/shows;
wenzelm
parents:
12875
diff
changeset
|
637 |
and 3: "P --> Q ==> P" |
0c4fd7529467
clarified syntax of ``long'' statements: fixes/assumes/shows;
wenzelm
parents:
12875
diff
changeset
|
638 |
shows R |
12349 | 639 |
proof - |
640 |
from 3 and 1 have P . |
|
12368 | 641 |
with 1 have Q by (rule impE) |
12349 | 642 |
with 2 show R . |
643 |
qed |
|
644 |
||
645 |
lemma allE': |
|
12937
0c4fd7529467
clarified syntax of ``long'' statements: fixes/assumes/shows;
wenzelm
parents:
12875
diff
changeset
|
646 |
assumes 1: "ALL x. P(x)" |
0c4fd7529467
clarified syntax of ``long'' statements: fixes/assumes/shows;
wenzelm
parents:
12875
diff
changeset
|
647 |
and 2: "P(x) ==> ALL x. P(x) ==> Q" |
0c4fd7529467
clarified syntax of ``long'' statements: fixes/assumes/shows;
wenzelm
parents:
12875
diff
changeset
|
648 |
shows Q |
12349 | 649 |
proof - |
650 |
from 1 have "P(x)" by (rule spec) |
|
651 |
from this and 1 show Q by (rule 2) |
|
652 |
qed |
|
653 |
||
12937
0c4fd7529467
clarified syntax of ``long'' statements: fixes/assumes/shows;
wenzelm
parents:
12875
diff
changeset
|
654 |
lemma notE': |
0c4fd7529467
clarified syntax of ``long'' statements: fixes/assumes/shows;
wenzelm
parents:
12875
diff
changeset
|
655 |
assumes 1: "~ P" |
0c4fd7529467
clarified syntax of ``long'' statements: fixes/assumes/shows;
wenzelm
parents:
12875
diff
changeset
|
656 |
and 2: "~ P ==> P" |
0c4fd7529467
clarified syntax of ``long'' statements: fixes/assumes/shows;
wenzelm
parents:
12875
diff
changeset
|
657 |
shows R |
12349 | 658 |
proof - |
659 |
from 2 and 1 have P . |
|
660 |
with 1 show R by (rule notE) |
|
661 |
qed |
|
662 |
||
663 |
lemmas [Pure.elim!] = disjE iffE FalseE conjE exE |
|
664 |
and [Pure.intro!] = iffI conjI impI TrueI notI allI refl |
|
665 |
and [Pure.elim 2] = allE notE' impE' |
|
666 |
and [Pure.intro] = exI disjI2 disjI1 |
|
667 |
||
18708 | 668 |
setup {* ContextRules.addSWrapper (fn tac => hyp_subst_tac ORELSE' tac) *} |
12349 | 669 |
|
670 |
||
12368 | 671 |
lemma iff_not_sym: "~ (Q <-> P) ==> ~ (P <-> Q)" |
17591 | 672 |
by iprover |
12368 | 673 |
|
674 |
lemmas [sym] = sym iff_sym not_sym iff_not_sym |
|
675 |
and [Pure.elim?] = iffD1 iffD2 impE |
|
676 |
||
677 |
||
13435 | 678 |
lemma eq_commute: "a=b <-> b=a" |
679 |
apply (rule iffI) |
|
680 |
apply (erule sym)+ |
|
681 |
done |
|
682 |
||
683 |
||
11677 | 684 |
subsection {* Atomizing meta-level rules *} |
685 |
||
11747 | 686 |
lemma atomize_all [atomize]: "(!!x. P(x)) == Trueprop (ALL x. P(x))" |
11976 | 687 |
proof |
11677 | 688 |
assume "!!x. P(x)" |
22931 | 689 |
then show "ALL x. P(x)" .. |
11677 | 690 |
next |
691 |
assume "ALL x. P(x)" |
|
22931 | 692 |
then show "!!x. P(x)" .. |
11677 | 693 |
qed |
694 |
||
11747 | 695 |
lemma atomize_imp [atomize]: "(A ==> B) == Trueprop (A --> B)" |
11976 | 696 |
proof |
12368 | 697 |
assume "A ==> B" |
22931 | 698 |
then show "A --> B" .. |
11677 | 699 |
next |
700 |
assume "A --> B" and A |
|
22931 | 701 |
then show B by (rule mp) |
11677 | 702 |
qed |
703 |
||
11747 | 704 |
lemma atomize_eq [atomize]: "(x == y) == Trueprop (x = y)" |
11976 | 705 |
proof |
11677 | 706 |
assume "x == y" |
22931 | 707 |
show "x = y" unfolding `x == y` by (rule refl) |
11677 | 708 |
next |
709 |
assume "x = y" |
|
22931 | 710 |
then show "x == y" by (rule eq_reflection) |
11677 | 711 |
qed |
712 |
||
18813 | 713 |
lemma atomize_iff [atomize]: "(A == B) == Trueprop (A <-> B)" |
714 |
proof |
|
715 |
assume "A == B" |
|
22931 | 716 |
show "A <-> B" unfolding `A == B` by (rule iff_refl) |
18813 | 717 |
next |
718 |
assume "A <-> B" |
|
22931 | 719 |
then show "A == B" by (rule iff_reflection) |
18813 | 720 |
qed |
721 |
||
12875 | 722 |
lemma atomize_conj [atomize]: |
19120
353d349740de
not_equal: replaced syntax translation by abbreviation;
wenzelm
parents:
18861
diff
changeset
|
723 |
includes meta_conjunction_syntax |
353d349740de
not_equal: replaced syntax translation by abbreviation;
wenzelm
parents:
18861
diff
changeset
|
724 |
shows "(A && B) == Trueprop (A & B)" |
11976 | 725 |
proof |
19120
353d349740de
not_equal: replaced syntax translation by abbreviation;
wenzelm
parents:
18861
diff
changeset
|
726 |
assume conj: "A && B" |
353d349740de
not_equal: replaced syntax translation by abbreviation;
wenzelm
parents:
18861
diff
changeset
|
727 |
show "A & B" |
353d349740de
not_equal: replaced syntax translation by abbreviation;
wenzelm
parents:
18861
diff
changeset
|
728 |
proof (rule conjI) |
353d349740de
not_equal: replaced syntax translation by abbreviation;
wenzelm
parents:
18861
diff
changeset
|
729 |
from conj show A by (rule conjunctionD1) |
353d349740de
not_equal: replaced syntax translation by abbreviation;
wenzelm
parents:
18861
diff
changeset
|
730 |
from conj show B by (rule conjunctionD2) |
353d349740de
not_equal: replaced syntax translation by abbreviation;
wenzelm
parents:
18861
diff
changeset
|
731 |
qed |
11953 | 732 |
next |
19120
353d349740de
not_equal: replaced syntax translation by abbreviation;
wenzelm
parents:
18861
diff
changeset
|
733 |
assume conj: "A & B" |
353d349740de
not_equal: replaced syntax translation by abbreviation;
wenzelm
parents:
18861
diff
changeset
|
734 |
show "A && B" |
353d349740de
not_equal: replaced syntax translation by abbreviation;
wenzelm
parents:
18861
diff
changeset
|
735 |
proof - |
353d349740de
not_equal: replaced syntax translation by abbreviation;
wenzelm
parents:
18861
diff
changeset
|
736 |
from conj show A .. |
353d349740de
not_equal: replaced syntax translation by abbreviation;
wenzelm
parents:
18861
diff
changeset
|
737 |
from conj show B .. |
11953 | 738 |
qed |
739 |
qed |
|
740 |
||
12368 | 741 |
lemmas [symmetric, rulify] = atomize_all atomize_imp |
18861 | 742 |
and [symmetric, defn] = atomize_all atomize_imp atomize_eq atomize_iff |
11771 | 743 |
|
11848 | 744 |
|
745 |
subsection {* Calculational rules *} |
|
746 |
||
747 |
lemma forw_subst: "a = b ==> P(b) ==> P(a)" |
|
748 |
by (rule ssubst) |
|
749 |
||
750 |
lemma back_subst: "P(a) ==> a = b ==> P(b)" |
|
751 |
by (rule subst) |
|
752 |
||
753 |
text {* |
|
754 |
Note that this list of rules is in reverse order of priorities. |
|
755 |
*} |
|
756 |
||
12019 | 757 |
lemmas basic_trans_rules [trans] = |
11848 | 758 |
forw_subst |
759 |
back_subst |
|
760 |
rev_mp |
|
761 |
mp |
|
762 |
trans |
|
763 |
||
13779 | 764 |
subsection {* ``Let'' declarations *} |
765 |
||
766 |
nonterminals letbinds letbind |
|
767 |
||
768 |
constdefs |
|
14854 | 769 |
Let :: "['a::{}, 'a => 'b] => ('b::{})" |
13779 | 770 |
"Let(s, f) == f(s)" |
771 |
||
772 |
syntax |
|
773 |
"_bind" :: "[pttrn, 'a] => letbind" ("(2_ =/ _)" 10) |
|
774 |
"" :: "letbind => letbinds" ("_") |
|
775 |
"_binds" :: "[letbind, letbinds] => letbinds" ("_;/ _") |
|
776 |
"_Let" :: "[letbinds, 'a] => 'a" ("(let (_)/ in (_))" 10) |
|
777 |
||
778 |
translations |
|
779 |
"_Let(_binds(b, bs), e)" == "_Let(b, _Let(bs, e))" |
|
780 |
"let x = a in e" == "Let(a, %x. e)" |
|
781 |
||
782 |
||
783 |
lemma LetI: |
|
21539 | 784 |
assumes "!!x. x=t ==> P(u(x))" |
785 |
shows "P(let x=t in u(x))" |
|
786 |
apply (unfold Let_def) |
|
787 |
apply (rule refl [THEN assms]) |
|
788 |
done |
|
789 |
||
790 |
||
791 |
subsection {* ML bindings *} |
|
13779 | 792 |
|
21539 | 793 |
ML {* |
22139 | 794 |
val refl = @{thm refl} |
795 |
val trans = @{thm trans} |
|
796 |
val sym = @{thm sym} |
|
797 |
val subst = @{thm subst} |
|
798 |
val ssubst = @{thm ssubst} |
|
799 |
val conjI = @{thm conjI} |
|
800 |
val conjE = @{thm conjE} |
|
801 |
val conjunct1 = @{thm conjunct1} |
|
802 |
val conjunct2 = @{thm conjunct2} |
|
803 |
val disjI1 = @{thm disjI1} |
|
804 |
val disjI2 = @{thm disjI2} |
|
805 |
val disjE = @{thm disjE} |
|
806 |
val impI = @{thm impI} |
|
807 |
val impE = @{thm impE} |
|
808 |
val mp = @{thm mp} |
|
809 |
val rev_mp = @{thm rev_mp} |
|
810 |
val TrueI = @{thm TrueI} |
|
811 |
val FalseE = @{thm FalseE} |
|
812 |
val iff_refl = @{thm iff_refl} |
|
813 |
val iff_trans = @{thm iff_trans} |
|
814 |
val iffI = @{thm iffI} |
|
815 |
val iffE = @{thm iffE} |
|
816 |
val iffD1 = @{thm iffD1} |
|
817 |
val iffD2 = @{thm iffD2} |
|
818 |
val notI = @{thm notI} |
|
819 |
val notE = @{thm notE} |
|
820 |
val allI = @{thm allI} |
|
821 |
val allE = @{thm allE} |
|
822 |
val spec = @{thm spec} |
|
823 |
val exI = @{thm exI} |
|
824 |
val exE = @{thm exE} |
|
825 |
val eq_reflection = @{thm eq_reflection} |
|
826 |
val iff_reflection = @{thm iff_reflection} |
|
827 |
val meta_eq_to_obj_eq = @{thm meta_eq_to_obj_eq} |
|
828 |
val meta_eq_to_iff = @{thm meta_eq_to_iff} |
|
13779 | 829 |
*} |
830 |
||
4854 | 831 |
end |