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