removed redundant ball_image
authoroheimb
Tue Nov 04 20:52:20 1997 +0100 (1997-11-04)
changeset 4136ba267836dd7a
parent 4135 4830f1f5f6ea
child 4137 2ce2e659c2b1
removed redundant ball_image
added image_cong and not_empty
added ball and bex of UNIV
src/HOL/equalities.ML
     1.1 --- a/src/HOL/equalities.ML	Tue Nov 04 20:50:35 1997 +0100
     1.2 +++ b/src/HOL/equalities.ML	Tue Nov 04 20:52:20 1997 +0100
     1.3 @@ -103,9 +103,6 @@
     1.4  by (Blast_tac 1);
     1.5  qed "image_image";
     1.6  
     1.7 -qed_goal "ball_image" Set.thy "(!y:F``S. P y) = (!x:S. P (F x))"
     1.8 - (fn _ => [Blast_tac 1]);
     1.9 -
    1.10  goal thy "!!x. x:A ==> insert (f x) (f``A) = f``A";
    1.11  by (Blast_tac 1);
    1.12  qed "insert_image";
    1.13 @@ -124,6 +121,11 @@
    1.14  qed "if_image_distrib";
    1.15  Addsimps[if_image_distrib];
    1.16  
    1.17 +val prems= goal thy "[|M = N; !!x. x:N ==> f x = g x|] ==> f``M = g``N";
    1.18 +by (rtac set_ext 1);
    1.19 +by (simp_tac (simpset() addsimps image_def::prems) 1);
    1.20 +qed "image_cong";
    1.21 +
    1.22  
    1.23  section "Int";
    1.24  
    1.25 @@ -372,6 +374,9 @@
    1.26  
    1.27  (*Basic identities*)
    1.28  
    1.29 +val not_empty = prove_goal Set.thy "A  {} = (x. xA)" (K [Blast_tac 1]);
    1.30 +(*Addsimps[not_empty];*)
    1.31 +
    1.32  goal thy "(UN x:{}. B x) = {}";
    1.33  by (Blast_tac 1);
    1.34  qed "UN_empty";
    1.35 @@ -680,6 +685,7 @@
    1.36       "(ALL x:A. P --> Q x) = (P --> (ALL x:A. Q x))",
    1.37       "(ALL x:A. P x --> Q) = ((EX x:A. P x) --> Q)",
    1.38       "(ALL x:{}. P x) = True",
    1.39 +     "(ALL x:UNIV. P x) = (ALL x. P x)",
    1.40       "(ALL x:insert a B. P x) = (P(a) & (ALL x:B. P x))",
    1.41       "(ALL x:Union(A). P x) = (ALL y:A. ALL x:y. P x)",
    1.42       "(ALL x:Collect Q. P x) = (ALL x. Q x --> P x)",
    1.43 @@ -693,6 +699,7 @@
    1.44      ["(EX x:A. P x & Q) = ((EX x:A. P x) & Q)",
    1.45       "(EX x:A. P & Q x) = (P & (EX x:A. Q x))",
    1.46       "(EX x:{}. P x) = False",
    1.47 +     "(EX x:UNIV. P x) = (EX x. P x)",
    1.48       "(EX x:insert a B. P x) = (P(a) | (EX x:B. P x))",
    1.49       "(EX x:Union(A). P x) = (EX y:A. EX x:y.  P x)",
    1.50       "(EX x:Collect Q. P x) = (EX x. Q x & P x)",