13 where classical: "(!!x. x:~P ==> f(x):P) ==> cla(f):P" |
13 where classical: "(!!x. x:~P ==> f(x):P) ==> cla(f):P" |
14 |
14 |
15 |
15 |
16 (*** Classical introduction rules for | and EX ***) |
16 (*** Classical introduction rules for | and EX ***) |
17 |
17 |
18 schematic_lemma disjCI: |
18 schematic_goal disjCI: |
19 assumes "!!x. x:~Q ==> f(x):P" |
19 assumes "!!x. x:~Q ==> f(x):P" |
20 shows "?p : P|Q" |
20 shows "?p : P|Q" |
21 apply (rule classical) |
21 apply (rule classical) |
22 apply (assumption | rule assms disjI1 notI)+ |
22 apply (assumption | rule assms disjI1 notI)+ |
23 apply (assumption | rule disjI2 notE)+ |
23 apply (assumption | rule disjI2 notE)+ |
24 done |
24 done |
25 |
25 |
26 (*introduction rule involving only EX*) |
26 (*introduction rule involving only EX*) |
27 schematic_lemma ex_classical: |
27 schematic_goal ex_classical: |
28 assumes "!!u. u:~(EX x. P(x)) ==> f(u):P(a)" |
28 assumes "!!u. u:~(EX x. P(x)) ==> f(u):P(a)" |
29 shows "?p : EX x. P(x)" |
29 shows "?p : EX x. P(x)" |
30 apply (rule classical) |
30 apply (rule classical) |
31 apply (rule exI, rule assms, assumption) |
31 apply (rule exI, rule assms, assumption) |
32 done |
32 done |
33 |
33 |
34 (*version of above, simplifying ~EX to ALL~ *) |
34 (*version of above, simplifying ~EX to ALL~ *) |
35 schematic_lemma exCI: |
35 schematic_goal exCI: |
36 assumes "!!u. u:ALL x. ~P(x) ==> f(u):P(a)" |
36 assumes "!!u. u:ALL x. ~P(x) ==> f(u):P(a)" |
37 shows "?p : EX x. P(x)" |
37 shows "?p : EX x. P(x)" |
38 apply (rule ex_classical) |
38 apply (rule ex_classical) |
39 apply (rule notI [THEN allI, THEN assms]) |
39 apply (rule notI [THEN allI, THEN assms]) |
40 apply (erule notE) |
40 apply (erule notE) |
41 apply (erule exI) |
41 apply (erule exI) |
42 done |
42 done |
43 |
43 |
44 schematic_lemma excluded_middle: "?p : ~P | P" |
44 schematic_goal excluded_middle: "?p : ~P | P" |
45 apply (rule disjCI) |
45 apply (rule disjCI) |
46 apply assumption |
46 apply assumption |
47 done |
47 done |
48 |
48 |
49 |
49 |
50 (*** Special elimination rules *) |
50 (*** Special elimination rules *) |
51 |
51 |
52 (*Classical implies (-->) elimination. *) |
52 (*Classical implies (-->) elimination. *) |
53 schematic_lemma impCE: |
53 schematic_goal impCE: |
54 assumes major: "p:P-->Q" |
54 assumes major: "p:P-->Q" |
55 and r1: "!!x. x:~P ==> f(x):R" |
55 and r1: "!!x. x:~P ==> f(x):R" |
56 and r2: "!!y. y:Q ==> g(y):R" |
56 and r2: "!!y. y:Q ==> g(y):R" |
57 shows "?p : R" |
57 shows "?p : R" |
58 apply (rule excluded_middle [THEN disjE]) |
58 apply (rule excluded_middle [THEN disjE]) |
59 apply (tactic \<open>DEPTH_SOLVE (assume_tac @{context} 1 ORELSE |
59 apply (tactic \<open>DEPTH_SOLVE (assume_tac @{context} 1 ORELSE |
60 resolve_tac @{context} [@{thm r1}, @{thm r2}, @{thm major} RS @{thm mp}] 1)\<close>) |
60 resolve_tac @{context} [@{thm r1}, @{thm r2}, @{thm major} RS @{thm mp}] 1)\<close>) |
61 done |
61 done |
62 |
62 |
63 (*Double negation law*) |
63 (*Double negation law*) |
64 schematic_lemma notnotD: "p:~~P ==> ?p : P" |
64 schematic_goal notnotD: "p:~~P ==> ?p : P" |
65 apply (rule classical) |
65 apply (rule classical) |
66 apply (erule notE) |
66 apply (erule notE) |
67 apply assumption |
67 apply assumption |
68 done |
68 done |
69 |
69 |
70 |
70 |
71 (*** Tactics for implication and contradiction ***) |
71 (*** Tactics for implication and contradiction ***) |
72 |
72 |
73 (*Classical <-> elimination. Proof substitutes P=Q in |
73 (*Classical <-> elimination. Proof substitutes P=Q in |
74 ~P ==> ~Q and P ==> Q *) |
74 ~P ==> ~Q and P ==> Q *) |
75 schematic_lemma iffCE: |
75 schematic_goal iffCE: |
76 assumes major: "p:P<->Q" |
76 assumes major: "p:P<->Q" |
77 and r1: "!!x y.[| x:P; y:Q |] ==> f(x,y):R" |
77 and r1: "!!x y.[| x:P; y:Q |] ==> f(x,y):R" |
78 and r2: "!!x y.[| x:~P; y:~Q |] ==> g(x,y):R" |
78 and r2: "!!x y.[| x:~P; y:~Q |] ==> g(x,y):R" |
79 shows "?p : R" |
79 shows "?p : R" |
80 apply (insert major) |
80 apply (insert major) |