equal
deleted
inserted
replaced
442 Addsimps [empty_subsetI]; |
442 Addsimps [empty_subsetI]; |
443 |
443 |
444 qed_goal "equals0I" ZF.thy "[| !!y. y:A ==> False |] ==> A=0" |
444 qed_goal "equals0I" ZF.thy "[| !!y. y:A ==> False |] ==> A=0" |
445 (fn prems=> [ blast_tac (claset() addDs prems) 1 ]); |
445 (fn prems=> [ blast_tac (claset() addDs prems) 1 ]); |
446 |
446 |
447 qed_goal "equals0E" ZF.thy "!!P. [| A=0; a:A |] ==> P" |
447 qed_goal "equals0D" ZF.thy "!!P. A=0 ==> a ~: A" |
448 (fn _=> [ Full_simp_tac 1, Blast_tac 1 ]); |
448 (fn _=> [ Blast_tac 1 ]); |
449 |
449 |
450 AddEs [equals0E, sym RS equals0E]; |
450 AddDs [equals0D, sym RS equals0D]; |
451 |
451 |
452 qed_goal "not_emptyI" ZF.thy "!!A a. a:A ==> A ~= 0" |
452 qed_goal "not_emptyI" ZF.thy "!!A a. a:A ==> A ~= 0" |
453 (fn _=> [ Blast_tac 1 ]); |
453 (fn _=> [ Blast_tac 1 ]); |
454 |
454 |
455 qed_goal "not_emptyE" ZF.thy "[| A ~= 0; !!x. x:A ==> R |] ==> R" |
455 qed_goal "not_emptyE" ZF.thy "[| A ~= 0; !!x. x:A ==> R |] ==> R" |