src/HOL/Set.ML
changeset 6006 d2e271b8d651
parent 5931 325300576da7
child 6171 cd237a10cbf8
equal deleted inserted replaced
6005:45186ec4d8b6 6006:d2e271b8d651
    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))  ]);