equal
deleted
inserted
replaced
51 "[| P-->Q; ~P ==> R; Q ==> R |] ==> R" |
51 "[| P-->Q; ~P ==> R; Q ==> R |] ==> R" |
52 (fn major::prems=> |
52 (fn major::prems=> |
53 [ (resolve_tac [excluded_middle RS disjE] 1), |
53 [ (resolve_tac [excluded_middle RS disjE] 1), |
54 (DEPTH_SOLVE (ares_tac (prems@[major RS mp]) 1)) ]); |
54 (DEPTH_SOLVE (ares_tac (prems@[major RS mp]) 1)) ]); |
55 |
55 |
|
56 (*This version of --> elimination works on Q before P. It works best for |
|
57 those cases in which P holds "almost everywhere". Can't install as |
|
58 default: would break old proofs.*) |
|
59 qed_goal "impCE'" thy |
|
60 "[| P-->Q; Q ==> R; ~P ==> R |] ==> R" |
|
61 (fn major::prems=> |
|
62 [ (resolve_tac [excluded_middle RS disjE] 1), |
|
63 (DEPTH_SOLVE (ares_tac (prems@[major RS mp]) 1)) ]); |
|
64 |
56 (*Double negation law*) |
65 (*Double negation law*) |
57 qed_goal "notnotD" FOL.thy "~~P ==> P" |
66 qed_goal "notnotD" FOL.thy "~~P ==> P" |
58 (fn [major]=> |
67 (fn [major]=> |
59 [ (rtac classical 1), (eresolve_tac [major RS notE] 1) ]); |
68 [ (rtac classical 1), (eresolve_tac [major RS notE] 1) ]); |
60 |
69 |