src/ZF/equalities.ML
author lcp
Fri, 12 Aug 1994 18:45:33 +0200
changeset 517 a9f93400f307
parent 435 ca5356bd315a
child 520 806d3f00590d
permissions -rw-r--r--
for infinite datatypes with arbitrary index sets
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
     1
(*  Title: 	ZF/equalities
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
     2
    ID:         $Id$
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
     3
    Author: 	Lawrence C Paulson, Cambridge University Computer Laboratory
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
     4
    Copyright   1992  University of Cambridge
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
     5
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
     6
Set Theory examples: Union, Intersection, Inclusion, etc.
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
     7
    (Thanks also to Philippe de Groote.)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
     8
*)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
     9
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    10
(** Finite Sets **)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    11
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    12
goal ZF.thy "cons(a, cons(b, C)) = cons(b, cons(a, C))";
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    13
by (fast_tac eq_cs 1);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    14
val cons_commute = result();
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    15
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    16
goal ZF.thy "!!B. a: B ==> cons(a,B) = B";
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    17
by (fast_tac eq_cs 1);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    18
val cons_absorb = result();
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    19
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    20
goal ZF.thy "!!B. a: B ==> cons(a, B-{a}) = B";
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    21
by (fast_tac eq_cs 1);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    22
val cons_Diff = result();
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    23
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    24
goal ZF.thy "!!C. [| a: C;  ALL y:C. y=b |] ==> C = {b}";
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    25
by (fast_tac eq_cs 1);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    26
val equal_singleton_lemma = result();
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    27
val equal_singleton = ballI RSN (2,equal_singleton_lemma);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    28
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    29
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    30
(** Binary Intersection **)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    31
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    32
goal ZF.thy "0 Int A = 0";
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    33
by (fast_tac eq_cs 1);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    34
val Int_0 = result();
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    35
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    36
(*NOT an equality, but it seems to belong here...*)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    37
goal ZF.thy "cons(a,B) Int C <= cons(a, B Int C)";
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    38
by (fast_tac eq_cs 1);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    39
val Int_cons = result();
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    40
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    41
goal ZF.thy "A Int A = A";
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    42
by (fast_tac eq_cs 1);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    43
val Int_absorb = result();
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    44
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    45
goal ZF.thy "A Int B = B Int A";
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    46
by (fast_tac eq_cs 1);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    47
val Int_commute = result();
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    48
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    49
goal ZF.thy "(A Int B) Int C  =  A Int (B Int C)";
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    50
by (fast_tac eq_cs 1);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    51
val Int_assoc = result();
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    52
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    53
goal ZF.thy "(A Un B) Int C  =  (A Int C) Un (B Int C)";
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    54
by (fast_tac eq_cs 1);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    55
val Int_Un_distrib = result();
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    56
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    57
goal ZF.thy "A<=B <-> A Int B = A";
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    58
by (fast_tac (eq_cs addSEs [equalityE]) 1);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    59
val subset_Int_iff = result();
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    60
435
ca5356bd315a Addition of cardinals and order types, various tidying
lcp
parents: 268
diff changeset
    61
goal ZF.thy "A<=B <-> B Int A = A";
ca5356bd315a Addition of cardinals and order types, various tidying
lcp
parents: 268
diff changeset
    62
by (fast_tac (eq_cs addSEs [equalityE]) 1);
ca5356bd315a Addition of cardinals and order types, various tidying
lcp
parents: 268
diff changeset
    63
val subset_Int_iff2 = result();
ca5356bd315a Addition of cardinals and order types, various tidying
lcp
parents: 268
diff changeset
    64
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    65
(** Binary Union **)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    66
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    67
goal ZF.thy "0 Un A = A";
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    68
by (fast_tac eq_cs 1);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    69
val Un_0 = result();
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    70
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    71
goal ZF.thy "cons(a,B) Un C = cons(a, B Un C)";
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    72
by (fast_tac eq_cs 1);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    73
val Un_cons = result();
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    74
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    75
goal ZF.thy "A Un A = A";
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    76
by (fast_tac eq_cs 1);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    77
val Un_absorb = result();
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    78
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    79
goal ZF.thy "A Un B = B Un A";
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    80
by (fast_tac eq_cs 1);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    81
val Un_commute = result();
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    82
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    83
goal ZF.thy "(A Un B) Un C  =  A Un (B Un C)";
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    84
by (fast_tac eq_cs 1);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    85
val Un_assoc = result();
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    86
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    87
goal ZF.thy "(A Int B) Un C  =  (A Un C) Int (B Un C)";
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    88
by (fast_tac eq_cs 1);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    89
val Un_Int_distrib = result();
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    90
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    91
goal ZF.thy "A<=B <-> A Un B = B";
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    92
by (fast_tac (eq_cs addSEs [equalityE]) 1);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    93
val subset_Un_iff = result();
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    94
435
ca5356bd315a Addition of cardinals and order types, various tidying
lcp
parents: 268
diff changeset
    95
goal ZF.thy "A<=B <-> B Un A = B";
ca5356bd315a Addition of cardinals and order types, various tidying
lcp
parents: 268
diff changeset
    96
by (fast_tac (eq_cs addSEs [equalityE]) 1);
ca5356bd315a Addition of cardinals and order types, various tidying
lcp
parents: 268
diff changeset
    97
val subset_Un_iff2 = result();
ca5356bd315a Addition of cardinals and order types, various tidying
lcp
parents: 268
diff changeset
    98
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    99
(** Simple properties of Diff -- set difference **)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   100
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   101
goal ZF.thy "A-A = 0";
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   102
by (fast_tac eq_cs 1);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   103
val Diff_cancel = result();
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   104
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   105
goal ZF.thy "0-A = 0";
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   106
by (fast_tac eq_cs 1);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   107
val empty_Diff = result();
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   108
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   109
goal ZF.thy "A-0 = A";
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   110
by (fast_tac eq_cs 1);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   111
val Diff_0 = result();
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   112
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   113
(*NOT SUITABLE FOR REWRITING since {a} == cons(a,0)*)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   114
goal ZF.thy "A - cons(a,B) = A - B - {a}";
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   115
by (fast_tac eq_cs 1);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   116
val Diff_cons = result();
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   117
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   118
(*NOT SUITABLE FOR REWRITING since {a} == cons(a,0)*)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   119
goal ZF.thy "A - cons(a,B) = A - {a} - B";
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   120
by (fast_tac eq_cs 1);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   121
val Diff_cons2 = result();
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   122
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   123
goal ZF.thy "A Int (B-A) = 0";
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   124
by (fast_tac eq_cs 1);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   125
val Diff_disjoint = result();
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   126
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   127
goal ZF.thy "!!A B. A<=B ==> A Un (B-A) = B";
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   128
by (fast_tac eq_cs 1);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   129
val Diff_partition = result();
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   130
268
1a038ec6f923 double_complement_Un: new
lcp
parents: 198
diff changeset
   131
goal ZF.thy "!!A B. [| A<=B; B<=C |] ==> B-(C-A) = A";
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   132
by (fast_tac eq_cs 1);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   133
val double_complement = result();
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   134
268
1a038ec6f923 double_complement_Un: new
lcp
parents: 198
diff changeset
   135
goal ZF.thy "(A Un B) - (B-A) = A";
1a038ec6f923 double_complement_Un: new
lcp
parents: 198
diff changeset
   136
by (fast_tac eq_cs 1);
1a038ec6f923 double_complement_Un: new
lcp
parents: 198
diff changeset
   137
val double_complement_Un = result();
1a038ec6f923 double_complement_Un: new
lcp
parents: 198
diff changeset
   138
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   139
goal ZF.thy
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   140
 "(A Int B) Un (B Int C) Un (C Int A) = (A Un B) Int (B Un C) Int (C Un A)";
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   141
by (fast_tac eq_cs 1);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   142
val Un_Int_crazy = result();
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   143
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   144
goal ZF.thy "A - (B Un C) = (A-B) Int (A-C)";
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   145
by (fast_tac eq_cs 1);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   146
val Diff_Un = result();
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   147
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   148
goal ZF.thy "A - (B Int C) = (A-B) Un (A-C)";
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   149
by (fast_tac eq_cs 1);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   150
val Diff_Int = result();
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   151
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   152
(*Halmos, Naive Set Theory, page 16.*)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   153
goal ZF.thy "(A Int B) Un C = A Int (B Un C)  <->  C<=A";
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   154
by (fast_tac (eq_cs addSEs [equalityE]) 1);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   155
val Un_Int_assoc_iff = result();
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   156
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   157
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   158
(** Big Union and Intersection **)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   159
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   160
goal ZF.thy "Union(0) = 0";
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   161
by (fast_tac eq_cs 1);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   162
val Union_0 = result();
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   163
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   164
goal ZF.thy "Union(cons(a,B)) = a Un Union(B)";
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   165
by (fast_tac eq_cs 1);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   166
val Union_cons = result();
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   167
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   168
goal ZF.thy "Union(A Un B) = Union(A) Un Union(B)";
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   169
by (fast_tac eq_cs 1);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   170
val Union_Un_distrib = result();
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   171
435
ca5356bd315a Addition of cardinals and order types, various tidying
lcp
parents: 268
diff changeset
   172
goal ZF.thy "Union(A Int B) <= Union(A) Int Union(B)";
ca5356bd315a Addition of cardinals and order types, various tidying
lcp
parents: 268
diff changeset
   173
by (fast_tac ZF_cs 1);
ca5356bd315a Addition of cardinals and order types, various tidying
lcp
parents: 268
diff changeset
   174
val Union_Int_subset = result();
ca5356bd315a Addition of cardinals and order types, various tidying
lcp
parents: 268
diff changeset
   175
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   176
goal ZF.thy "Union(C) Int A = 0 <-> (ALL B:C. B Int A = 0)";
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   177
by (fast_tac (eq_cs addSEs [equalityE]) 1);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   178
val Union_disjoint = result();
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   179
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   180
(* A good challenge: Inter is ill-behaved on the empty set *)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   181
goal ZF.thy "!!A B. [| a:A;  b:B |] ==> Inter(A Un B) = Inter(A) Int Inter(B)";
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   182
by (fast_tac eq_cs 1);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   183
val Inter_Un_distrib = result();
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   184
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   185
goal ZF.thy "Union({b}) = b";
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   186
by (fast_tac eq_cs 1);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   187
val Union_singleton = result();
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   188
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   189
goal ZF.thy "Inter({b}) = b";
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   190
by (fast_tac eq_cs 1);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   191
val Inter_singleton = result();
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   192
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   193
(** Unions and Intersections of Families **)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   194
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   195
goal ZF.thy "Union(A) = (UN x:A. x)";
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   196
by (fast_tac eq_cs 1);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   197
val Union_eq_UN = result();
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   198
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   199
goalw ZF.thy [Inter_def] "Inter(A) = (INT x:A. x)";
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   200
by (fast_tac eq_cs 1);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   201
val Inter_eq_INT = result();
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   202
517
a9f93400f307 for infinite datatypes with arbitrary index sets
lcp
parents: 435
diff changeset
   203
goal ZF.thy "(UN i:0. A(i)) = 0";
a9f93400f307 for infinite datatypes with arbitrary index sets
lcp
parents: 435
diff changeset
   204
by (fast_tac eq_cs 1);
a9f93400f307 for infinite datatypes with arbitrary index sets
lcp
parents: 435
diff changeset
   205
val UN_0 = result();
a9f93400f307 for infinite datatypes with arbitrary index sets
lcp
parents: 435
diff changeset
   206
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   207
(*Halmos, Naive Set Theory, page 35.*)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   208
goal ZF.thy "B Int (UN i:I. A(i)) = (UN i:I. B Int A(i))";
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   209
by (fast_tac eq_cs 1);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   210
val Int_UN_distrib = result();
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   211
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   212
goal ZF.thy "!!A B. i:I ==> B Un (INT i:I. A(i)) = (INT i:I. B Un A(i))";
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   213
by (fast_tac eq_cs 1);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   214
val Un_INT_distrib = result();
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   215
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   216
goal ZF.thy
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   217
    "(UN i:I. A(i)) Int (UN j:J. B(j)) = (UN i:I. UN j:J. A(i) Int B(j))";
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   218
by (fast_tac eq_cs 1);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   219
val Int_UN_distrib2 = result();
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   220
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   221
goal ZF.thy
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   222
    "!!I J. [| i:I;  j:J |] ==> \
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   223
\    (INT i:I. A(i)) Un (INT j:J. B(j)) = (INT i:I. INT j:J. A(i) Un B(j))";
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   224
by (fast_tac eq_cs 1);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   225
val Un_INT_distrib2 = result();
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   226
435
ca5356bd315a Addition of cardinals and order types, various tidying
lcp
parents: 268
diff changeset
   227
goal ZF.thy "!!A. a: A ==> (UN y:A. c) = c";
ca5356bd315a Addition of cardinals and order types, various tidying
lcp
parents: 268
diff changeset
   228
by (fast_tac eq_cs 1);
ca5356bd315a Addition of cardinals and order types, various tidying
lcp
parents: 268
diff changeset
   229
val UN_constant = result();
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   230
435
ca5356bd315a Addition of cardinals and order types, various tidying
lcp
parents: 268
diff changeset
   231
goal ZF.thy "!!A. a: A ==> (INT y:A. c) = c";
ca5356bd315a Addition of cardinals and order types, various tidying
lcp
parents: 268
diff changeset
   232
by (fast_tac eq_cs 1);
ca5356bd315a Addition of cardinals and order types, various tidying
lcp
parents: 268
diff changeset
   233
val INT_constant = result();
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   234
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   235
(** Devlin, Fundamentals of Contemporary Set Theory, page 12, exercise 5: 
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   236
    Union of a family of unions **)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   237
192
3dc5c8016a0e ZF/equalities/SUM_eq_UN: new
lcp
parents: 182
diff changeset
   238
goal ZF.thy "(UN i:I. A(i) Un B(i)) = (UN i:I. A(i))  Un  (UN i:I. B(i))";
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   239
by (fast_tac eq_cs 1);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   240
val UN_Un_distrib = result();
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   241
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   242
goal ZF.thy
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   243
    "!!A B. i:I ==> \
192
3dc5c8016a0e ZF/equalities/SUM_eq_UN: new
lcp
parents: 182
diff changeset
   244
\           (INT i:I. A(i)  Int  B(i)) = (INT i:I. A(i)) Int (INT i:I. B(i))";
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   245
by (fast_tac eq_cs 1);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   246
val INT_Int_distrib = result();
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   247
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   248
(** Devlin, page 12, exercise 5: Complements **)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   249
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   250
goal ZF.thy "!!A B. i:I ==> B - (UN i:I. A(i)) = (INT i:I. B - A(i))";
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   251
by (fast_tac eq_cs 1);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   252
val Diff_UN = result();
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   253
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   254
goal ZF.thy "!!A B. i:I ==> B - (INT i:I. A(i)) = (UN i:I. B - A(i))";
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   255
by (fast_tac eq_cs 1);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   256
val Diff_INT = result();
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   257
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   258
(** Unions and Intersections with General Sum **)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   259
182
e30b55c07235 New distributive laws for Sigma and UN
lcp
parents: 0
diff changeset
   260
goal ZF.thy "(SUM x:(UN y:A. C(y)). B(x)) = (UN y:A. SUM x:C(y). B(x))";
e30b55c07235 New distributive laws for Sigma and UN
lcp
parents: 0
diff changeset
   261
by (fast_tac eq_cs 1);
e30b55c07235 New distributive laws for Sigma and UN
lcp
parents: 0
diff changeset
   262
val SUM_UN_distrib1 = result();
e30b55c07235 New distributive laws for Sigma and UN
lcp
parents: 0
diff changeset
   263
192
3dc5c8016a0e ZF/equalities/SUM_eq_UN: new
lcp
parents: 182
diff changeset
   264
goal ZF.thy "(SUM i:I. UN j:J. C(i,j)) = (UN j:J. SUM i:I. C(i,j))";
182
e30b55c07235 New distributive laws for Sigma and UN
lcp
parents: 0
diff changeset
   265
by (fast_tac eq_cs 1);
e30b55c07235 New distributive laws for Sigma and UN
lcp
parents: 0
diff changeset
   266
val SUM_UN_distrib2 = result();
e30b55c07235 New distributive laws for Sigma and UN
lcp
parents: 0
diff changeset
   267
192
3dc5c8016a0e ZF/equalities/SUM_eq_UN: new
lcp
parents: 182
diff changeset
   268
goal ZF.thy "(SUM i:I Un J. C(i)) = (SUM i:I. C(i)) Un (SUM j:J. C(j))";
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   269
by (fast_tac eq_cs 1);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   270
val SUM_Un_distrib1 = result();
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   271
192
3dc5c8016a0e ZF/equalities/SUM_eq_UN: new
lcp
parents: 182
diff changeset
   272
goal ZF.thy "(SUM i:I. A(i) Un B(i)) = (SUM i:I. A(i)) Un (SUM i:I. B(i))";
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   273
by (fast_tac eq_cs 1);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   274
val SUM_Un_distrib2 = result();
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   275
192
3dc5c8016a0e ZF/equalities/SUM_eq_UN: new
lcp
parents: 182
diff changeset
   276
goal ZF.thy "(SUM i:I Int J. C(i)) = (SUM i:I. C(i)) Int (SUM j:J. C(j))";
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   277
by (fast_tac eq_cs 1);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   278
val SUM_Int_distrib1 = result();
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   279
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   280
goal ZF.thy
192
3dc5c8016a0e ZF/equalities/SUM_eq_UN: new
lcp
parents: 182
diff changeset
   281
    "(SUM i:I. A(i) Int B(i)) = (SUM i:I. A(i)) Int (SUM i:I. B(i))";
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   282
by (fast_tac eq_cs 1);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   283
val SUM_Int_distrib2 = result();
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   284
192
3dc5c8016a0e ZF/equalities/SUM_eq_UN: new
lcp
parents: 182
diff changeset
   285
(*Cf Aczel, Non-Well-Founded Sets, page 115*)
3dc5c8016a0e ZF/equalities/SUM_eq_UN: new
lcp
parents: 182
diff changeset
   286
goal ZF.thy "(SUM i:I. A(i)) = (UN i:I. {i} * A(i))";
3dc5c8016a0e ZF/equalities/SUM_eq_UN: new
lcp
parents: 182
diff changeset
   287
by (fast_tac eq_cs 1);
3dc5c8016a0e ZF/equalities/SUM_eq_UN: new
lcp
parents: 182
diff changeset
   288
val SUM_eq_UN = result();
3dc5c8016a0e ZF/equalities/SUM_eq_UN: new
lcp
parents: 182
diff changeset
   289
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   290
(** Domain, Range and Field **)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   291
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   292
goal ZF.thy "domain(A Un B) = domain(A) Un domain(B)";
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   293
by (fast_tac eq_cs 1);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   294
val domain_Un_eq = result();
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   295
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   296
goal ZF.thy "domain(A Int B) <= domain(A) Int domain(B)";
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   297
by (fast_tac eq_cs 1);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   298
val domain_Int_subset = result();
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   299
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   300
goal ZF.thy "domain(A) - domain(B) <= domain(A - B)";
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   301
by (fast_tac eq_cs 1);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   302
val domain_diff_subset = result();
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   303
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   304
goal ZF.thy "range(A Un B) = range(A) Un range(B)";
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   305
by (fast_tac eq_cs 1);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   306
val range_Un_eq = result();
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   307
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   308
goal ZF.thy "range(A Int B) <= range(A) Int range(B)";
435
ca5356bd315a Addition of cardinals and order types, various tidying
lcp
parents: 268
diff changeset
   309
by (fast_tac ZF_cs 1);
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   310
val range_Int_subset = result();
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   311
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   312
goal ZF.thy "range(A) - range(B) <= range(A - B)";
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   313
by (fast_tac eq_cs 1);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   314
val range_diff_subset = result();
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   315
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   316
goal ZF.thy "field(A Un B) = field(A) Un field(B)";
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   317
by (fast_tac eq_cs 1);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   318
val field_Un_eq = result();
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   319
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   320
goal ZF.thy "field(A Int B) <= field(A) Int field(B)";
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   321
by (fast_tac eq_cs 1);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   322
val field_Int_subset = result();
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   323
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   324
goal ZF.thy "field(A) - field(B) <= field(A - B)";
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   325
by (fast_tac eq_cs 1);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   326
val field_diff_subset = result();
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   327
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   328
435
ca5356bd315a Addition of cardinals and order types, various tidying
lcp
parents: 268
diff changeset
   329
(** Image **)
ca5356bd315a Addition of cardinals and order types, various tidying
lcp
parents: 268
diff changeset
   330
ca5356bd315a Addition of cardinals and order types, various tidying
lcp
parents: 268
diff changeset
   331
goal ZF.thy "r``0 = 0";
ca5356bd315a Addition of cardinals and order types, various tidying
lcp
parents: 268
diff changeset
   332
by (fast_tac eq_cs 1);
ca5356bd315a Addition of cardinals and order types, various tidying
lcp
parents: 268
diff changeset
   333
val image_empty = result();
ca5356bd315a Addition of cardinals and order types, various tidying
lcp
parents: 268
diff changeset
   334
ca5356bd315a Addition of cardinals and order types, various tidying
lcp
parents: 268
diff changeset
   335
goal ZF.thy "r``(A Un B) = (r``A) Un (r``B)";
ca5356bd315a Addition of cardinals and order types, various tidying
lcp
parents: 268
diff changeset
   336
by (fast_tac eq_cs 1);
ca5356bd315a Addition of cardinals and order types, various tidying
lcp
parents: 268
diff changeset
   337
val image_Un = result();
ca5356bd315a Addition of cardinals and order types, various tidying
lcp
parents: 268
diff changeset
   338
ca5356bd315a Addition of cardinals and order types, various tidying
lcp
parents: 268
diff changeset
   339
goal ZF.thy "r``(A Int B) <= (r``A) Int (r``B)";
ca5356bd315a Addition of cardinals and order types, various tidying
lcp
parents: 268
diff changeset
   340
by (fast_tac ZF_cs 1);
ca5356bd315a Addition of cardinals and order types, various tidying
lcp
parents: 268
diff changeset
   341
val image_Int_subset = result();
ca5356bd315a Addition of cardinals and order types, various tidying
lcp
parents: 268
diff changeset
   342
ca5356bd315a Addition of cardinals and order types, various tidying
lcp
parents: 268
diff changeset
   343
goal ZF.thy "(r Int A*A)``B <= (r``B) Int A";
ca5356bd315a Addition of cardinals and order types, various tidying
lcp
parents: 268
diff changeset
   344
by (fast_tac ZF_cs 1);
ca5356bd315a Addition of cardinals and order types, various tidying
lcp
parents: 268
diff changeset
   345
val image_Int_square_subset = result();
ca5356bd315a Addition of cardinals and order types, various tidying
lcp
parents: 268
diff changeset
   346
ca5356bd315a Addition of cardinals and order types, various tidying
lcp
parents: 268
diff changeset
   347
goal ZF.thy "!!r. B<=A ==> (r Int A*A)``B = (r``B) Int A";
ca5356bd315a Addition of cardinals and order types, various tidying
lcp
parents: 268
diff changeset
   348
by (fast_tac eq_cs 1);
ca5356bd315a Addition of cardinals and order types, various tidying
lcp
parents: 268
diff changeset
   349
val image_Int_square = result();
ca5356bd315a Addition of cardinals and order types, various tidying
lcp
parents: 268
diff changeset
   350
ca5356bd315a Addition of cardinals and order types, various tidying
lcp
parents: 268
diff changeset
   351
ca5356bd315a Addition of cardinals and order types, various tidying
lcp
parents: 268
diff changeset
   352
(** Inverse Image **)
ca5356bd315a Addition of cardinals and order types, various tidying
lcp
parents: 268
diff changeset
   353
ca5356bd315a Addition of cardinals and order types, various tidying
lcp
parents: 268
diff changeset
   354
goal ZF.thy "r-``0 = 0";
ca5356bd315a Addition of cardinals and order types, various tidying
lcp
parents: 268
diff changeset
   355
by (fast_tac eq_cs 1);
ca5356bd315a Addition of cardinals and order types, various tidying
lcp
parents: 268
diff changeset
   356
val vimage_empty = result();
ca5356bd315a Addition of cardinals and order types, various tidying
lcp
parents: 268
diff changeset
   357
ca5356bd315a Addition of cardinals and order types, various tidying
lcp
parents: 268
diff changeset
   358
goal ZF.thy "r-``(A Un B) = (r-``A) Un (r-``B)";
ca5356bd315a Addition of cardinals and order types, various tidying
lcp
parents: 268
diff changeset
   359
by (fast_tac eq_cs 1);
ca5356bd315a Addition of cardinals and order types, various tidying
lcp
parents: 268
diff changeset
   360
val vimage_Un = result();
ca5356bd315a Addition of cardinals and order types, various tidying
lcp
parents: 268
diff changeset
   361
ca5356bd315a Addition of cardinals and order types, various tidying
lcp
parents: 268
diff changeset
   362
goal ZF.thy "r-``(A Int B) <= (r-``A) Int (r-``B)";
ca5356bd315a Addition of cardinals and order types, various tidying
lcp
parents: 268
diff changeset
   363
by (fast_tac ZF_cs 1);
ca5356bd315a Addition of cardinals and order types, various tidying
lcp
parents: 268
diff changeset
   364
val vimage_Int_subset = result();
ca5356bd315a Addition of cardinals and order types, various tidying
lcp
parents: 268
diff changeset
   365
ca5356bd315a Addition of cardinals and order types, various tidying
lcp
parents: 268
diff changeset
   366
goal ZF.thy "(r Int A*A)-``B <= (r-``B) Int A";
ca5356bd315a Addition of cardinals and order types, various tidying
lcp
parents: 268
diff changeset
   367
by (fast_tac ZF_cs 1);
ca5356bd315a Addition of cardinals and order types, various tidying
lcp
parents: 268
diff changeset
   368
val vimage_Int_square_subset = result();
ca5356bd315a Addition of cardinals and order types, various tidying
lcp
parents: 268
diff changeset
   369
ca5356bd315a Addition of cardinals and order types, various tidying
lcp
parents: 268
diff changeset
   370
goal ZF.thy "!!r. B<=A ==> (r Int A*A)-``B = (r-``B) Int A";
ca5356bd315a Addition of cardinals and order types, various tidying
lcp
parents: 268
diff changeset
   371
by (fast_tac eq_cs 1);
ca5356bd315a Addition of cardinals and order types, various tidying
lcp
parents: 268
diff changeset
   372
val vimage_Int_square = result();
ca5356bd315a Addition of cardinals and order types, various tidying
lcp
parents: 268
diff changeset
   373
ca5356bd315a Addition of cardinals and order types, various tidying
lcp
parents: 268
diff changeset
   374
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   375
(** Converse **)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   376
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   377
goal ZF.thy "converse(A Un B) = converse(A) Un converse(B)";
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   378
by (fast_tac eq_cs 1);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   379
val converse_Un = result();
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   380
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   381
goal ZF.thy "converse(A Int B) = converse(A) Int converse(B)";
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   382
by (fast_tac eq_cs 1);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   383
val converse_Int = result();
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   384
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   385
goal ZF.thy "converse(A) - converse(B) = converse(A - B)";
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   386
by (fast_tac eq_cs 1);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   387
val converse_diff = result();
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   388
198
0f0ff91b07f6 new section for equality properties
lcp
parents: 192
diff changeset
   389
(** Pow **)
0f0ff91b07f6 new section for equality properties
lcp
parents: 192
diff changeset
   390
0f0ff91b07f6 new section for equality properties
lcp
parents: 192
diff changeset
   391
goal ZF.thy "Pow(A) Un Pow(B) <= Pow(A Un B)";
0f0ff91b07f6 new section for equality properties
lcp
parents: 192
diff changeset
   392
by (fast_tac upair_cs 1);
0f0ff91b07f6 new section for equality properties
lcp
parents: 192
diff changeset
   393
val Un_Pow_subset = result();
0f0ff91b07f6 new section for equality properties
lcp
parents: 192
diff changeset
   394
0f0ff91b07f6 new section for equality properties
lcp
parents: 192
diff changeset
   395
goal ZF.thy "(UN x:A. Pow(B(x))) <= Pow(UN x:A. B(x))";
0f0ff91b07f6 new section for equality properties
lcp
parents: 192
diff changeset
   396
by (fast_tac upair_cs 1);
0f0ff91b07f6 new section for equality properties
lcp
parents: 192
diff changeset
   397
val UN_Pow_subset = result();
0f0ff91b07f6 new section for equality properties
lcp
parents: 192
diff changeset
   398
0f0ff91b07f6 new section for equality properties
lcp
parents: 192
diff changeset
   399
goal ZF.thy "A <= Pow(Union(A))";
0f0ff91b07f6 new section for equality properties
lcp
parents: 192
diff changeset
   400
by (fast_tac upair_cs 1);
0f0ff91b07f6 new section for equality properties
lcp
parents: 192
diff changeset
   401
val subset_Pow_Union = result();
0f0ff91b07f6 new section for equality properties
lcp
parents: 192
diff changeset
   402
0f0ff91b07f6 new section for equality properties
lcp
parents: 192
diff changeset
   403
goal ZF.thy "Union(Pow(A)) = A";
0f0ff91b07f6 new section for equality properties
lcp
parents: 192
diff changeset
   404
by (fast_tac eq_cs 1);
0f0ff91b07f6 new section for equality properties
lcp
parents: 192
diff changeset
   405
val Union_Pow_eq = result();
0f0ff91b07f6 new section for equality properties
lcp
parents: 192
diff changeset
   406
0f0ff91b07f6 new section for equality properties
lcp
parents: 192
diff changeset
   407
goal ZF.thy "Pow(A) Int Pow(B) = Pow(A Int B)";
0f0ff91b07f6 new section for equality properties
lcp
parents: 192
diff changeset
   408
by (fast_tac eq_cs 1);
0f0ff91b07f6 new section for equality properties
lcp
parents: 192
diff changeset
   409
val Int_Pow_eq = result();
0f0ff91b07f6 new section for equality properties
lcp
parents: 192
diff changeset
   410
0f0ff91b07f6 new section for equality properties
lcp
parents: 192
diff changeset
   411
goal ZF.thy "!!x A. x:A ==> (INT x:A. Pow(B(x))) = Pow(INT x:A. B(x))";
0f0ff91b07f6 new section for equality properties
lcp
parents: 192
diff changeset
   412
by (fast_tac eq_cs 1);
0f0ff91b07f6 new section for equality properties
lcp
parents: 192
diff changeset
   413
val INT_Pow_subset = result();
435
ca5356bd315a Addition of cardinals and order types, various tidying
lcp
parents: 268
diff changeset
   414