equal
deleted
inserted
replaced
57 (*Takes assumptions ! x:A.P(x) and a:A; creates assumption P(a)*) |
57 (*Takes assumptions ! x:A.P(x) and a:A; creates assumption P(a)*) |
58 fun ball_tac i = etac ballE i THEN contr_tac (i+1); |
58 fun ball_tac i = etac ballE i THEN contr_tac (i+1); |
59 |
59 |
60 AddSIs [ballI]; |
60 AddSIs [ballI]; |
61 AddEs [ballE]; |
61 AddEs [ballE]; |
|
62 (* gives better instantiation for bound: *) |
|
63 claset_ref() := claset() addWrapper ("bspec", fn tac2 => |
|
64 (dtac bspec THEN' atac) APPEND' tac2); |
62 |
65 |
63 Goalw [Bex_def] "[| P(x); x:A |] ==> ? x:A. P(x)"; |
66 Goalw [Bex_def] "[| P(x); x:A |] ==> ? x:A. P(x)"; |
64 by (Blast_tac 1); |
67 by (Blast_tac 1); |
65 qed "bexI"; |
68 qed "bexI"; |
66 |
69 |
67 qed_goal "bexCI" Set.thy |
70 qed_goal "bexCI" Set.thy |
68 "[| ! x:A. ~P(x) ==> P(a); a:A |] ==> ? x:A. P(x)" |
71 "[| ! x:A. ~P(x) ==> P(a); a:A |] ==> ? x:A. P(x)" (fn prems => |
69 (fn prems=> |
|
70 [ (rtac classical 1), |
72 [ (rtac classical 1), |
71 (REPEAT (ares_tac (prems@[bexI,ballI,notI,notE]) 1)) ]); |
73 (REPEAT (ares_tac (prems@[bexI,ballI,notI,notE]) 1)) ]); |
72 |
74 |
73 val major::prems = Goalw [Bex_def] |
75 val major::prems = Goalw [Bex_def] |
74 "[| ? x:A. P(x); !!x. [| x:A; P(x) |] ==> Q |] ==> Q"; |
76 "[| ? x:A. P(x); !!x. [| x:A; P(x) |] ==> Q |] ==> Q"; |