equal
deleted
inserted
replaced
56 (*Double negation law*) |
56 (*Double negation law*) |
57 qed_goal "notnotD" FOL.thy "~~P ==> P" |
57 qed_goal "notnotD" FOL.thy "~~P ==> P" |
58 (fn [major]=> |
58 (fn [major]=> |
59 [ (rtac classical 1), (eresolve_tac [major RS notE] 1) ]); |
59 [ (rtac classical 1), (eresolve_tac [major RS notE] 1) ]); |
60 |
60 |
|
61 qed_goal "contrapos2" FOL.thy "[| Q; ~ P ==> ~ Q |] ==> P" (fn [p1,p2] => [ |
|
62 rtac classical 1, |
|
63 dtac p2 1, |
|
64 etac notE 1, |
|
65 rtac p1 1]); |
61 |
66 |
62 (*** Tactics for implication and contradiction ***) |
67 (*** Tactics for implication and contradiction ***) |
63 |
68 |
64 (*Classical <-> elimination. Proof substitutes P=Q in |
69 (*Classical <-> elimination. Proof substitutes P=Q in |
65 ~P ==> ~Q and P ==> Q *) |
70 ~P ==> ~Q and P ==> Q *) |