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