equal
deleted
inserted
replaced
58 lemma excluded_middle: "~P | P" |
58 lemma excluded_middle: "~P | P" |
59 apply (rule disjCI) |
59 apply (rule disjCI) |
60 apply assumption |
60 apply assumption |
61 done |
61 done |
62 |
62 |
63 (*For disjunctive case analysis*) |
|
64 ML {* |
|
65 fun excluded_middle_tac sP = |
|
66 res_inst_tac [("Q",sP)] (@{thm excluded_middle} RS @{thm disjE}) |
|
67 *} |
|
68 |
|
69 lemma case_split [case_names True False]: |
63 lemma case_split [case_names True False]: |
70 assumes r1: "P ==> Q" |
64 assumes r1: "P ==> Q" |
71 and r2: "~P ==> Q" |
65 and r2: "~P ==> Q" |
72 shows Q |
66 shows Q |
73 apply (rule excluded_middle [THEN disjE]) |
67 apply (rule excluded_middle [THEN disjE]) |
74 apply (erule r2) |
68 apply (erule r2) |
75 apply (erule r1) |
69 apply (erule r1) |
76 done |
70 done |
77 |
71 |
78 ML {* |
72 ML {* |
79 fun case_tac a = res_inst_tac [("P",a)] @{thm case_split} |
73 fun case_tac ctxt a = |
|
74 RuleInsts.res_inst_tac ctxt [(("P", 0), a)] @{thm case_split} |
80 *} |
75 *} |
|
76 |
|
77 method_setup case_tac = |
|
78 {* Method.goal_args_ctxt Args.name case_tac *} |
|
79 "case_tac emulation (dynamic instantiation!)" |
81 |
80 |
82 |
81 |
83 (*** Special elimination rules *) |
82 (*** Special elimination rules *) |
84 |
83 |
85 |
84 |
167 by (rule classical) iprover |
166 by (rule classical) iprover |
168 |
167 |
169 use "cladata.ML" |
168 use "cladata.ML" |
170 setup Cla.setup |
169 setup Cla.setup |
171 setup cla_setup |
170 setup cla_setup |
172 setup case_setup |
|
173 |
171 |
174 use "blastdata.ML" |
172 use "blastdata.ML" |
175 setup Blast.setup |
173 setup Blast.setup |
176 |
174 |
177 |
175 |