src/ZF/equalities.ML
author lcp
Fri, 03 Dec 1993 12:47:45 +0100
changeset 182 e30b55c07235
parent 0 a5a9c433f639
child 192 3dc5c8016a0e
permissions -rw-r--r--
New distributive laws for Sigma and UN
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
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    61
(** Binary Union **)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    62
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    63
goal ZF.thy "0 Un A = A";
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    64
by (fast_tac eq_cs 1);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    65
val Un_0 = result();
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    66
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    67
goal ZF.thy "cons(a,B) Un C = cons(a, B Un C)";
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    68
by (fast_tac eq_cs 1);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    69
val Un_cons = result();
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    70
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    71
goal ZF.thy "A Un A = A";
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    72
by (fast_tac eq_cs 1);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    73
val Un_absorb = result();
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    74
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    75
goal ZF.thy "A Un B = B Un 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_commute = result();
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    78
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    79
goal ZF.thy "(A Un B) Un C  =  A Un (B Un C)";
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    80
by (fast_tac eq_cs 1);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    81
val Un_assoc = result();
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    82
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    83
goal ZF.thy "(A Int B) Un C  =  (A Un C) Int (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_Int_distrib = result();
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    86
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    87
goal ZF.thy "A<=B <-> A Un B = B";
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    88
by (fast_tac (eq_cs addSEs [equalityE]) 1);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    89
val subset_Un_iff = result();
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    90
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    91
(** Simple properties of Diff -- set difference **)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    92
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    93
goal ZF.thy "A-A = 0";
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    94
by (fast_tac eq_cs 1);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    95
val Diff_cancel = result();
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    96
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    97
goal ZF.thy "0-A = 0";
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    98
by (fast_tac eq_cs 1);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    99
val empty_Diff = result();
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   100
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   101
goal ZF.thy "A-0 = A";
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   102
by (fast_tac eq_cs 1);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   103
val Diff_0 = result();
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   104
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   105
(*NOT SUITABLE FOR REWRITING since {a} == cons(a,0)*)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   106
goal ZF.thy "A - cons(a,B) = A - B - {a}";
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   107
by (fast_tac eq_cs 1);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   108
val Diff_cons = result();
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   109
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   110
(*NOT SUITABLE FOR REWRITING since {a} == cons(a,0)*)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   111
goal ZF.thy "A - cons(a,B) = A - {a} - B";
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   112
by (fast_tac eq_cs 1);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   113
val Diff_cons2 = result();
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   114
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   115
goal ZF.thy "A Int (B-A) = 0";
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   116
by (fast_tac eq_cs 1);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   117
val Diff_disjoint = result();
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   118
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   119
goal ZF.thy "!!A B. A<=B ==> A Un (B-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_partition = result();
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   122
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   123
goal ZF.thy "!!A B. [| A<=B; B<= C |] ==> (B - (C-A)) = A";
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   124
by (fast_tac eq_cs 1);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   125
val double_complement = result();
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   126
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   127
goal ZF.thy
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   128
 "(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
   129
by (fast_tac eq_cs 1);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   130
val Un_Int_crazy = result();
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   131
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   132
goal ZF.thy "A - (B Un C) = (A-B) Int (A-C)";
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   133
by (fast_tac eq_cs 1);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   134
val Diff_Un = result();
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   135
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   136
goal ZF.thy "A - (B Int C) = (A-B) Un (A-C)";
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   137
by (fast_tac eq_cs 1);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   138
val Diff_Int = result();
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   139
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   140
(*Halmos, Naive Set Theory, page 16.*)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   141
goal ZF.thy "(A Int B) Un C = A Int (B Un C)  <->  C<=A";
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   142
by (fast_tac (eq_cs addSEs [equalityE]) 1);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   143
val Un_Int_assoc_iff = result();
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   144
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   145
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   146
(** Big Union and Intersection **)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   147
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   148
goal ZF.thy "Union(0) = 0";
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   149
by (fast_tac eq_cs 1);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   150
val Union_0 = result();
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   151
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   152
goal ZF.thy "Union(cons(a,B)) = a Un Union(B)";
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   153
by (fast_tac eq_cs 1);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   154
val Union_cons = result();
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   155
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   156
goal ZF.thy "Union(A Un B) = Union(A) Un Union(B)";
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   157
by (fast_tac eq_cs 1);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   158
val Union_Un_distrib = result();
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   159
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   160
goal ZF.thy "Union(C) Int A = 0 <-> (ALL B:C. B Int A = 0)";
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   161
by (fast_tac (eq_cs addSEs [equalityE]) 1);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   162
val Union_disjoint = result();
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   163
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   164
(* A good challenge: Inter is ill-behaved on the empty set *)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   165
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
   166
by (fast_tac eq_cs 1);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   167
val Inter_Un_distrib = result();
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   168
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   169
goal ZF.thy "Union({b}) = 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_singleton = result();
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   172
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   173
goal ZF.thy "Inter({b}) = b";
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   174
by (fast_tac eq_cs 1);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   175
val Inter_singleton = result();
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   176
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   177
(** Unions and Intersections of Families **)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   178
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   179
goal ZF.thy "Union(A) = (UN x:A. x)";
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   180
by (fast_tac eq_cs 1);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   181
val Union_eq_UN = result();
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   182
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   183
goalw ZF.thy [Inter_def] "Inter(A) = (INT x:A. x)";
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   184
by (fast_tac eq_cs 1);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   185
val Inter_eq_INT = result();
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   186
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   187
(*Halmos, Naive Set Theory, page 35.*)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   188
goal ZF.thy "B Int (UN i:I. A(i)) = (UN i:I. B Int A(i))";
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   189
by (fast_tac eq_cs 1);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   190
val Int_UN_distrib = result();
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   191
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   192
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
   193
by (fast_tac eq_cs 1);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   194
val Un_INT_distrib = result();
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   195
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   196
goal ZF.thy
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   197
    "(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
   198
by (fast_tac eq_cs 1);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   199
val Int_UN_distrib2 = result();
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   200
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   201
goal ZF.thy
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   202
    "!!I J. [| i:I;  j:J |] ==> \
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   203
\    (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
   204
by (fast_tac eq_cs 1);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   205
val Un_INT_distrib2 = result();
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   206
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   207
goal ZF.thy "!!A. [| a: A;  ALL y:A. b(y)=b(a) |] ==> (UN y:A. b(y)) = b(a)";
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   208
by (fast_tac (eq_cs addSEs [equalityE]) 1);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   209
val UN_singleton_lemma = result();
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   210
val UN_singleton = ballI RSN (2,UN_singleton_lemma);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   211
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   212
goal ZF.thy "!!A. [| a: A;  ALL y:A. b(y)=b(a) |] ==> (INT y:A. b(y)) = b(a)";
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   213
by (fast_tac (eq_cs addSEs [equalityE]) 1);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   214
val INT_singleton_lemma = result();
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   215
val INT_singleton = ballI RSN (2,INT_singleton_lemma);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   216
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   217
(** Devlin, Fundamentals of Contemporary Set Theory, page 12, exercise 5: 
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   218
    Union of a family of unions **)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   219
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   220
goal ZF.thy "(UN i:I. A(x) Un B(x)) = (UN i:I. A(x))  Un  (UN i:I. B(x))";
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   221
by (fast_tac eq_cs 1);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   222
val UN_Un_distrib = result();
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   223
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   224
goal ZF.thy
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   225
    "!!A B. i:I ==> \
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   226
\           (INT i:I. A(x)  Int  B(x)) = (INT i:I. A(x)) Int (INT i:I. B(x))";
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   227
by (fast_tac eq_cs 1);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   228
val INT_Int_distrib = result();
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   229
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   230
(** Devlin, page 12, exercise 5: Complements **)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   231
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   232
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
   233
by (fast_tac eq_cs 1);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   234
val Diff_UN = result();
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   235
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   236
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
   237
by (fast_tac eq_cs 1);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   238
val Diff_INT = result();
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   239
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   240
(** Unions and Intersections with General Sum **)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   241
182
e30b55c07235 New distributive laws for Sigma and UN
lcp
parents: 0
diff changeset
   242
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
   243
by (fast_tac eq_cs 1);
e30b55c07235 New distributive laws for Sigma and UN
lcp
parents: 0
diff changeset
   244
val SUM_UN_distrib1 = result();
e30b55c07235 New distributive laws for Sigma and UN
lcp
parents: 0
diff changeset
   245
e30b55c07235 New distributive laws for Sigma and UN
lcp
parents: 0
diff changeset
   246
goal ZF.thy "(SUM x:A. UN y:B. C(x,y)) = (UN y:B. SUM x:A. C(x,y))";
e30b55c07235 New distributive laws for Sigma and UN
lcp
parents: 0
diff changeset
   247
by (fast_tac eq_cs 1);
e30b55c07235 New distributive laws for Sigma and UN
lcp
parents: 0
diff changeset
   248
val SUM_UN_distrib2 = result();
e30b55c07235 New distributive laws for Sigma and UN
lcp
parents: 0
diff changeset
   249
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   250
goal ZF.thy "(SUM x:A Un B. C(x)) = (SUM x:A. C(x)) Un (SUM x:B. C(x))";
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   251
by (fast_tac eq_cs 1);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   252
val SUM_Un_distrib1 = result();
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   253
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   254
goal ZF.thy
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   255
    "(SUM i:I. A(x) Un B(x)) = (SUM i:I. A(x)) Un (SUM i:I. B(x))";
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   256
by (fast_tac eq_cs 1);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   257
val SUM_Un_distrib2 = result();
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   258
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   259
goal ZF.thy "(SUM x:A Int B. C(x)) = (SUM x:A. C(x)) Int (SUM x:B. C(x))";
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   260
by (fast_tac eq_cs 1);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   261
val SUM_Int_distrib1 = result();
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   262
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   263
goal ZF.thy
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   264
    "(SUM i:I. A(x) Int B(x)) = (SUM i:I. A(x)) Int (SUM i:I. B(x))";
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   265
by (fast_tac eq_cs 1);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   266
val SUM_Int_distrib2 = result();
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   267
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   268
(** Domain, Range and Field **)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   269
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   270
goal ZF.thy "domain(A Un B) = domain(A) Un domain(B)";
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   271
by (fast_tac eq_cs 1);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   272
val domain_Un_eq = result();
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   273
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   274
goal ZF.thy "domain(A Int B) <= domain(A) Int domain(B)";
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   275
by (fast_tac eq_cs 1);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   276
val domain_Int_subset = result();
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   277
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   278
goal ZF.thy "domain(A) - domain(B) <= domain(A - B)";
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   279
by (fast_tac eq_cs 1);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   280
val domain_diff_subset = result();
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   281
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   282
goal ZF.thy "range(A Un B) = range(A) Un range(B)";
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   283
by (fast_tac eq_cs 1);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   284
val range_Un_eq = result();
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   285
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   286
goal ZF.thy "range(A Int B) <= range(A) Int range(B)";
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   287
by (fast_tac eq_cs 1);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   288
val range_Int_subset = result();
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   289
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   290
goal ZF.thy "range(A) - range(B) <= range(A - B)";
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   291
by (fast_tac eq_cs 1);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   292
val range_diff_subset = result();
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   293
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   294
goal ZF.thy "field(A Un B) = field(A) Un field(B)";
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   295
by (fast_tac eq_cs 1);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   296
val field_Un_eq = result();
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   297
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   298
goal ZF.thy "field(A Int B) <= field(A) Int field(B)";
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   299
by (fast_tac eq_cs 1);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   300
val field_Int_subset = result();
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   301
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   302
goal ZF.thy "field(A) - field(B) <= field(A - B)";
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   303
by (fast_tac eq_cs 1);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   304
val field_diff_subset = result();
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   305
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   306
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   307
(** Converse **)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   308
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   309
goal ZF.thy "converse(A Un B) = converse(A) Un converse(B)";
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   310
by (fast_tac eq_cs 1);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   311
val converse_Un = result();
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   312
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   313
goal ZF.thy "converse(A Int B) = converse(A) Int converse(B)";
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   314
by (fast_tac eq_cs 1);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   315
val converse_Int = result();
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   316
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   317
goal ZF.thy "converse(A) - converse(B) = converse(A - B)";
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   318
by (fast_tac eq_cs 1);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   319
val converse_diff = result();
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   320