equal
deleted
inserted
replaced
61 AddEs [ballE]; |
61 AddEs [ballE]; |
62 (* gives better instantiation for bound: *) |
62 (* gives better instantiation for bound: *) |
63 claset_ref() := claset() addWrapper ("bspec", fn tac2 => |
63 claset_ref() := claset() addWrapper ("bspec", fn tac2 => |
64 (dtac bspec THEN' atac) APPEND' tac2); |
64 (dtac bspec THEN' atac) APPEND' tac2); |
65 |
65 |
|
66 (*Normally the best argument order: P(x) constrains the choice of x:A*) |
66 Goalw [Bex_def] "[| P(x); x:A |] ==> ? x:A. P(x)"; |
67 Goalw [Bex_def] "[| P(x); x:A |] ==> ? x:A. P(x)"; |
67 by (Blast_tac 1); |
68 by (Blast_tac 1); |
68 qed "bexI"; |
69 qed "bexI"; |
|
70 |
|
71 (*The best argument order when there is only one x:A*) |
|
72 Goalw [Bex_def] "[| x:A; P(x) |] ==> ? x:A. P(x)"; |
|
73 by (Blast_tac 1); |
|
74 qed "rev_bexI"; |
69 |
75 |
70 qed_goal "bexCI" Set.thy |
76 qed_goal "bexCI" Set.thy |
71 "[| ! x:A. ~P(x) ==> P(a); a:A |] ==> ? x:A. P(x)" (fn prems => |
77 "[| ! x:A. ~P(x) ==> P(a); a:A |] ==> ? x:A. P(x)" (fn prems => |
72 [ (rtac classical 1), |
78 [ (rtac classical 1), |
73 (REPEAT (ares_tac (prems@[bexI,ballI,notI,notE]) 1)) ]); |
79 (REPEAT (ares_tac (prems@[bexI,ballI,notI,notE]) 1)) ]); |