equal
deleted
inserted
replaced
59 To specify P use something like |
59 To specify P use something like |
60 eres_inst_tac [ ("P","ALL y. ?S(x,y)") ] rev_mp 1 *) |
60 eres_inst_tac [ ("P","ALL y. ?S(x,y)") ] rev_mp 1 *) |
61 qed_goal "rev_mp" IFOL.thy "[| P; P --> Q |] ==> Q" |
61 qed_goal "rev_mp" IFOL.thy "[| P; P --> Q |] ==> Q" |
62 (fn prems=> [ (REPEAT (resolve_tac (prems@[mp]) 1)) ]); |
62 (fn prems=> [ (REPEAT (resolve_tac (prems@[mp]) 1)) ]); |
63 |
63 |
|
64 qed_goal "contrapos" IFOL.thy "[| ~Q; P==>Q |] ==> ~P" |
|
65 (fn [major,minor]=> |
|
66 [ (rtac (major RS notE RS notI) 1), |
|
67 (etac minor 1) ]); |
|
68 |
64 |
69 |
65 (*Contrapositive of an inference rule*) |
70 (*Contrapositive of an inference rule*) |
66 qed_goal "contrapos" IFOL.thy "[| ~Q; P==>Q |] ==> ~P" |
71 qed_goal "contrapos" IFOL.thy "[| ~Q; P==>Q |] ==> ~P" |
67 (fn [major,minor]=> |
72 (fn [major,minor]=> |
68 [ (rtac (major RS notE RS notI) 1), |
73 [ (rtac (major RS notE RS notI) 1), |