10 bind_thm ("ccontr", FalseE RS classical); |
10 bind_thm ("ccontr", FalseE RS classical); |
11 |
11 |
12 |
12 |
13 (*** Classical introduction rules for | and EX ***) |
13 (*** Classical introduction rules for | and EX ***) |
14 |
14 |
15 qed_goal "disjCI" (the_context ()) |
15 val prems = Goal "(~Q ==> P) ==> P|Q"; |
16 "(~Q ==> P) ==> P|Q" |
16 by (rtac classical 1); |
17 (fn prems=> |
17 by (REPEAT (ares_tac (prems@[disjI1,notI]) 1)); |
18 [ (rtac classical 1), |
18 by (REPEAT (ares_tac (prems@[disjI2,notE]) 1)) ; |
19 (REPEAT (ares_tac (prems@[disjI1,notI]) 1)), |
19 qed "disjCI"; |
20 (REPEAT (ares_tac (prems@[disjI2,notE]) 1)) ]); |
|
21 |
20 |
22 (*introduction rule involving only EX*) |
21 (*introduction rule involving only EX*) |
23 qed_goal "ex_classical" (the_context ()) |
22 val prems = Goal "( ~(EX x. P(x)) ==> P(a)) ==> EX x. P(x)"; |
24 "( ~(EX x. P(x)) ==> P(a)) ==> EX x. P(x)" |
23 by (rtac classical 1); |
25 (fn prems=> |
24 by (eresolve_tac (prems RL [exI]) 1) ; |
26 [ (rtac classical 1), |
25 qed "ex_classical"; |
27 (eresolve_tac (prems RL [exI]) 1) ]); |
|
28 |
26 |
29 (*version of above, simplifying ~EX to ALL~ *) |
27 (*version of above, simplifying ~EX to ALL~ *) |
30 qed_goal "exCI" (the_context ()) |
28 val [prem]= Goal "(ALL x. ~P(x) ==> P(a)) ==> EX x. P(x)"; |
31 "(ALL x. ~P(x) ==> P(a)) ==> EX x. P(x)" |
29 by (rtac ex_classical 1); |
32 (fn [prem]=> |
30 by (resolve_tac [notI RS allI RS prem] 1); |
33 [ (rtac ex_classical 1), |
31 by (etac notE 1); |
34 (resolve_tac [notI RS allI RS prem] 1), |
32 by (etac exI 1) ; |
35 (etac notE 1), |
33 qed "exCI"; |
36 (etac exI 1) ]); |
|
37 |
34 |
38 qed_goal "excluded_middle" (the_context ()) "~P | P" |
35 Goal"~P | P"; |
39 (fn _=> [ rtac disjCI 1, assume_tac 1 ]); |
36 by (rtac disjCI 1); |
|
37 by (assume_tac 1) ; |
|
38 qed "excluded_middle"; |
40 |
39 |
41 (*For disjunctive case analysis*) |
40 (*For disjunctive case analysis*) |
42 fun excluded_middle_tac sP = |
41 fun excluded_middle_tac sP = |
43 res_inst_tac [("Q",sP)] (excluded_middle RS disjE); |
42 res_inst_tac [("Q",sP)] (excluded_middle RS disjE); |
44 |
43 |
45 qed_goal "case_split_thm" (the_context ()) "[| P ==> Q; ~P ==> Q |] ==> Q" |
44 val [p1,p2] = Goal"[| P ==> Q; ~P ==> Q |] ==> Q"; |
46 (fn [p1,p2] => [rtac (excluded_middle RS disjE) 1, |
45 by (rtac (excluded_middle RS disjE) 1); |
47 etac p2 1, etac p1 1]); |
46 by (etac p2 1); |
|
47 by (etac p1 1); |
|
48 qed "case_split_thm"; |
48 |
49 |
49 (*HOL's more natural case analysis tactic*) |
50 (*HOL's more natural case analysis tactic*) |
50 fun case_tac a = res_inst_tac [("P",a)] case_split_thm; |
51 fun case_tac a = res_inst_tac [("P",a)] case_split_thm; |
51 |
52 |
52 |
53 |
53 (*** Special elimination rules *) |
54 (*** Special elimination rules *) |
54 |
55 |
55 |
56 |
56 (*Classical implies (-->) elimination. *) |
57 (*Classical implies (-->) elimination. *) |
57 qed_goal "impCE" (the_context ()) |
58 val major::prems = Goal "[| P-->Q; ~P ==> R; Q ==> R |] ==> R"; |
58 "[| P-->Q; ~P ==> R; Q ==> R |] ==> R" |
59 by (resolve_tac [excluded_middle RS disjE] 1); |
59 (fn major::prems=> |
60 by (DEPTH_SOLVE (ares_tac (prems@[major RS mp]) 1)) ; |
60 [ (resolve_tac [excluded_middle RS disjE] 1), |
61 qed "impCE"; |
61 (DEPTH_SOLVE (ares_tac (prems@[major RS mp]) 1)) ]); |
|
62 |
62 |
63 (*This version of --> elimination works on Q before P. It works best for |
63 (*This version of --> elimination works on Q before P. It works best for |
64 those cases in which P holds "almost everywhere". Can't install as |
64 those cases in which P holds "almost everywhere". Can't install as |
65 default: would break old proofs.*) |
65 default: would break old proofs.*) |
66 qed_goal "impCE'" (the_context ()) |
66 val major::prems = Goal "[| P-->Q; Q ==> R; ~P ==> R |] ==> R"; |
67 "[| P-->Q; Q ==> R; ~P ==> R |] ==> R" |
67 by (resolve_tac [excluded_middle RS disjE] 1); |
68 (fn major::prems=> |
68 by (DEPTH_SOLVE (ares_tac (prems@[major RS mp]) 1)) ; |
69 [ (resolve_tac [excluded_middle RS disjE] 1), |
69 qed "impCE'"; |
70 (DEPTH_SOLVE (ares_tac (prems@[major RS mp]) 1)) ]); |
|
71 |
70 |
72 (*Double negation law*) |
71 (*Double negation law*) |
73 qed_goal "notnotD" (the_context ()) "~~P ==> P" |
72 Goal"~~P ==> P"; |
74 (fn [major]=> |
73 by (rtac classical 1); |
75 [ (rtac classical 1), (eresolve_tac [major RS notE] 1) ]); |
74 by (etac notE 1); |
|
75 by (assume_tac 1); |
|
76 qed "notnotD"; |
76 |
77 |
77 qed_goal "contrapos2" (the_context ()) "[| Q; ~ P ==> ~ Q |] ==> P" (fn [p1,p2] => [ |
78 val [p1,p2] = Goal"[| Q; ~ P ==> ~ Q |] ==> P"; |
78 rtac classical 1, |
79 by (rtac classical 1); |
79 dtac p2 1, |
80 by (dtac p2 1); |
80 etac notE 1, |
81 by (etac notE 1); |
81 rtac p1 1]); |
82 by (rtac p1 1); |
|
83 qed "contrapos2"; |
82 |
84 |
83 (*** Tactics for implication and contradiction ***) |
85 (*** Tactics for implication and contradiction ***) |
84 |
86 |
85 (*Classical <-> elimination. Proof substitutes P=Q in |
87 (*Classical <-> elimination. Proof substitutes P=Q in |
86 ~P ==> ~Q and P ==> Q *) |
88 ~P ==> ~Q and P ==> Q *) |
87 qed_goalw "iffCE" (the_context ()) [iff_def] |
89 val major::prems = |
88 "[| P<->Q; [| P; Q |] ==> R; [| ~P; ~Q |] ==> R |] ==> R" |
90 Goalw [iff_def] "[| P<->Q; [| P; Q |] ==> R; [| ~P; ~Q |] ==> R |] ==> R"; |
89 (fn prems => |
91 by (rtac (major RS conjE) 1); |
90 [ (rtac conjE 1), |
92 by (REPEAT_FIRST (etac impCE)); |
91 (REPEAT (DEPTH_SOLVE_1 |
93 by (REPEAT (DEPTH_SOLVE_1 (mp_tac 1 ORELSE ares_tac prems 1))); |
92 (etac impCE 1 ORELSE mp_tac 1 ORELSE ares_tac prems 1))) ]); |
94 qed "iffCE"; |
|
95 |