src/HOL/Set.ML
changeset 3420 02dc9c5b035f
parent 3222 726a9b069947
child 3469 61d927bd57ec
     1.1 --- a/src/HOL/Set.ML	Fri Jun 06 10:19:53 1997 +0200
     1.2 +++ b/src/HOL/Set.ML	Fri Jun 06 10:20:38 1997 +0200
     1.3 @@ -80,17 +80,17 @@
     1.4  AddIs  [bexI];
     1.5  AddSEs [bexE];
     1.6  
     1.7 -(*Trival rewrite rule;   (! x:A.P)=P holds only if A is nonempty!*)
     1.8 -goalw Set.thy [Ball_def] "(! x:A. True) = True";
     1.9 -by (Simp_tac 1);
    1.10 -qed "ball_True";
    1.11 +(*Trival rewrite rule*)
    1.12 +goal Set.thy "(! x:A.P) = ((? x. x:A) --> P)";
    1.13 +by (simp_tac (!simpset addsimps [Ball_def]) 1);
    1.14 +qed "ball_triv";
    1.15  
    1.16  (*Dual form for existentials*)
    1.17 -goalw Set.thy [Bex_def] "(? x:A. False) = False";
    1.18 -by (Simp_tac 1);
    1.19 -qed "bex_False";
    1.20 +goal Set.thy "(? x:A.P) = ((? x. x:A) & P)";
    1.21 +by (simp_tac (!simpset addsimps [Bex_def]) 1);
    1.22 +qed "bex_triv";
    1.23  
    1.24 -Addsimps [ball_True, bex_False];
    1.25 +Addsimps [ball_triv, bex_triv];
    1.26  
    1.27  (** Congruence rules **)
    1.28  
    1.29 @@ -234,18 +234,6 @@
    1.30  qed "bex_empty";
    1.31  Addsimps [ball_empty, bex_empty];
    1.32  
    1.33 -goalw Set.thy [Ball_def] "(!x:A.False) = (A = {})";
    1.34 -by(Blast_tac 1);
    1.35 -qed "ball_False";
    1.36 -Addsimps [ball_False];
    1.37 -
    1.38 -(* The dual is probably not helpful:
    1.39 -goal Set.thy "(? x:A.True) = (A ~= {})";
    1.40 -by(Blast_tac 1);
    1.41 -qed "bex_True";
    1.42 -Addsimps [bex_True];
    1.43 -*)
    1.44 -
    1.45  
    1.46  section "The Powerset operator -- Pow";
    1.47