equal
deleted
inserted
replaced
49 (*This is useful with the special implication rules for each kind of P. *) |
49 (*This is useful with the special implication rules for each kind of P. *) |
50 qed_goal "not_to_imp" IFOL.thy |
50 qed_goal "not_to_imp" IFOL.thy |
51 "[| ~P; (P-->False) ==> Q |] ==> Q" |
51 "[| ~P; (P-->False) ==> Q |] ==> Q" |
52 (fn prems=> [ (REPEAT (ares_tac (prems@[impI,notE]) 1)) ]); |
52 (fn prems=> [ (REPEAT (ares_tac (prems@[impI,notE]) 1)) ]); |
53 |
53 |
54 |
54 (* For substitution into an assumption P, reduce Q to P-->Q, substitute into |
55 (* For substitution int an assumption P, reduce Q to P-->Q, substitute into |
|
56 this implication, then apply impI to move P back into the assumptions. |
55 this implication, then apply impI to move P back into the assumptions. |
57 To specify P use something like |
56 To specify P use something like |
58 eres_inst_tac [ ("P","ALL y. ?S(x,y)") ] rev_mp 1 *) |
57 eres_inst_tac [ ("P","ALL y. ?S(x,y)") ] rev_mp 1 *) |
59 qed_goal "rev_mp" IFOL.thy "[| P; P --> Q |] ==> Q" |
58 qed_goal "rev_mp" IFOL.thy "[| P; P --> Q |] ==> Q" |
60 (fn prems=> [ (REPEAT (resolve_tac (prems@[mp]) 1)) ]); |
59 (fn prems=> [ (REPEAT (resolve_tac (prems@[mp]) 1)) ]); |