src/ZF/equalities.ML
author lcp
Fri, 23 Dec 1994 16:51:10 +0100
changeset 839 1aa6b351ca34
parent 787 1affbb1c5f1f
child 1035 279a4fd3c5ce
permissions -rw-r--r--
RepFun_eq_0_iff, RepFun_0: new
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);
760
f0200e91b272 added qed and qed_goal[w]
clasohm
parents: 685
diff changeset
    15
qed "cons_eq";
520
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);
760
f0200e91b272 added qed and qed_goal[w]
clasohm
parents: 685
diff changeset
    19
qed "cons_commute";
0
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);
760
f0200e91b272 added qed and qed_goal[w]
clasohm
parents: 685
diff changeset
    23
qed "cons_absorb";
0
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);
760
f0200e91b272 added qed and qed_goal[w]
clasohm
parents: 685
diff changeset
    27
qed "cons_Diff";
0
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);
760
f0200e91b272 added qed and qed_goal[w]
clasohm
parents: 685
diff changeset
    31
qed "equal_singleton_lemma";
0
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);
760
f0200e91b272 added qed and qed_goal[w]
clasohm
parents: 685
diff changeset
    39
qed "Int_0";
0
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);
760
f0200e91b272 added qed and qed_goal[w]
clasohm
parents: 685
diff changeset
    44
qed "Int_cons";
0
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);
760
f0200e91b272 added qed and qed_goal[w]
clasohm
parents: 685
diff changeset
    48
qed "Int_absorb";
0
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);
760
f0200e91b272 added qed and qed_goal[w]
clasohm
parents: 685
diff changeset
    52
qed "Int_commute";
0
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);
760
f0200e91b272 added qed and qed_goal[w]
clasohm
parents: 685
diff changeset
    56
qed "Int_assoc";
0
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);
760
f0200e91b272 added qed and qed_goal[w]
clasohm
parents: 685
diff changeset
    60
qed "Int_Un_distrib";
0
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);
760
f0200e91b272 added qed and qed_goal[w]
clasohm
parents: 685
diff changeset
    64
qed "subset_Int_iff";
0
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);
760
f0200e91b272 added qed and qed_goal[w]
clasohm
parents: 685
diff changeset
    68
qed "subset_Int_iff2";
435
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);
760
f0200e91b272 added qed and qed_goal[w]
clasohm
parents: 685
diff changeset
    74
qed "Un_0";
0
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);
760
f0200e91b272 added qed and qed_goal[w]
clasohm
parents: 685
diff changeset
    78
qed "Un_cons";
0
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);
760
f0200e91b272 added qed and qed_goal[w]
clasohm
parents: 685
diff changeset
    82
qed "Un_absorb";
0
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);
760
f0200e91b272 added qed and qed_goal[w]
clasohm
parents: 685
diff changeset
    86
qed "Un_commute";
0
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);
760
f0200e91b272 added qed and qed_goal[w]
clasohm
parents: 685
diff changeset
    90
qed "Un_assoc";
0
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);
760
f0200e91b272 added qed and qed_goal[w]
clasohm
parents: 685
diff changeset
    94
qed "Un_Int_distrib";
0
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);
760
f0200e91b272 added qed and qed_goal[w]
clasohm
parents: 685
diff changeset
    98
qed "subset_Un_iff";
0
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);
760
f0200e91b272 added qed and qed_goal[w]
clasohm
parents: 685
diff changeset
   102
qed "subset_Un_iff2";
435
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);
760
f0200e91b272 added qed and qed_goal[w]
clasohm
parents: 685
diff changeset
   108
qed "Diff_cancel";
0
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);
760
f0200e91b272 added qed and qed_goal[w]
clasohm
parents: 685
diff changeset
   112
qed "empty_Diff";
0
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);
760
f0200e91b272 added qed and qed_goal[w]
clasohm
parents: 685
diff changeset
   116
qed "Diff_0";
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   117
787
1affbb1c5f1f converse_UN, Diff_eq_0_iff: new
lcp
parents: 760
diff changeset
   118
goal ZF.thy "A-B=0 <-> A<=B";
1affbb1c5f1f converse_UN, Diff_eq_0_iff: new
lcp
parents: 760
diff changeset
   119
by (fast_tac (eq_cs addEs [equalityE]) 1);
1affbb1c5f1f converse_UN, Diff_eq_0_iff: new
lcp
parents: 760
diff changeset
   120
qed "Diff_eq_0_iff";
1affbb1c5f1f converse_UN, Diff_eq_0_iff: new
lcp
parents: 760
diff changeset
   121
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   122
(*NOT SUITABLE FOR REWRITING since {a} == cons(a,0)*)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   123
goal ZF.thy "A - cons(a,B) = A - B - {a}";
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   124
by (fast_tac eq_cs 1);
760
f0200e91b272 added qed and qed_goal[w]
clasohm
parents: 685
diff changeset
   125
qed "Diff_cons";
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   126
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   127
(*NOT SUITABLE FOR REWRITING since {a} == cons(a,0)*)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   128
goal ZF.thy "A - cons(a,B) = A - {a} - B";
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   129
by (fast_tac eq_cs 1);
760
f0200e91b272 added qed and qed_goal[w]
clasohm
parents: 685
diff changeset
   130
qed "Diff_cons2";
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   131
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   132
goal ZF.thy "A Int (B-A) = 0";
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   133
by (fast_tac eq_cs 1);
760
f0200e91b272 added qed and qed_goal[w]
clasohm
parents: 685
diff changeset
   134
qed "Diff_disjoint";
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   135
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   136
goal ZF.thy "!!A B. A<=B ==> A Un (B-A) = B";
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   137
by (fast_tac eq_cs 1);
760
f0200e91b272 added qed and qed_goal[w]
clasohm
parents: 685
diff changeset
   138
qed "Diff_partition";
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   139
268
1a038ec6f923 double_complement_Un: new
lcp
parents: 198
diff changeset
   140
goal ZF.thy "!!A B. [| A<=B; B<=C |] ==> B-(C-A) = A";
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   141
by (fast_tac eq_cs 1);
760
f0200e91b272 added qed and qed_goal[w]
clasohm
parents: 685
diff changeset
   142
qed "double_complement";
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   143
268
1a038ec6f923 double_complement_Un: new
lcp
parents: 198
diff changeset
   144
goal ZF.thy "(A Un B) - (B-A) = A";
1a038ec6f923 double_complement_Un: new
lcp
parents: 198
diff changeset
   145
by (fast_tac eq_cs 1);
760
f0200e91b272 added qed and qed_goal[w]
clasohm
parents: 685
diff changeset
   146
qed "double_complement_Un";
268
1a038ec6f923 double_complement_Un: new
lcp
parents: 198
diff changeset
   147
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   148
goal ZF.thy
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   149
 "(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
   150
by (fast_tac eq_cs 1);
760
f0200e91b272 added qed and qed_goal[w]
clasohm
parents: 685
diff changeset
   151
qed "Un_Int_crazy";
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   152
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   153
goal ZF.thy "A - (B Un C) = (A-B) Int (A-C)";
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   154
by (fast_tac eq_cs 1);
760
f0200e91b272 added qed and qed_goal[w]
clasohm
parents: 685
diff changeset
   155
qed "Diff_Un";
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   156
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   157
goal ZF.thy "A - (B Int C) = (A-B) Un (A-C)";
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   158
by (fast_tac eq_cs 1);
760
f0200e91b272 added qed and qed_goal[w]
clasohm
parents: 685
diff changeset
   159
qed "Diff_Int";
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   160
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   161
(*Halmos, Naive Set Theory, page 16.*)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   162
goal ZF.thy "(A Int B) Un C = A Int (B Un C)  <->  C<=A";
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   163
by (fast_tac (eq_cs addSEs [equalityE]) 1);
760
f0200e91b272 added qed and qed_goal[w]
clasohm
parents: 685
diff changeset
   164
qed "Un_Int_assoc_iff";
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   165
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   166
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   167
(** Big Union and Intersection **)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   168
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   169
goal ZF.thy "Union(0) = 0";
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   170
by (fast_tac eq_cs 1);
760
f0200e91b272 added qed and qed_goal[w]
clasohm
parents: 685
diff changeset
   171
qed "Union_0";
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   172
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   173
goal ZF.thy "Union(cons(a,B)) = a Un Union(B)";
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   174
by (fast_tac eq_cs 1);
760
f0200e91b272 added qed and qed_goal[w]
clasohm
parents: 685
diff changeset
   175
qed "Union_cons";
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   176
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   177
goal ZF.thy "Union(A Un B) = Union(A) Un Union(B)";
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   178
by (fast_tac eq_cs 1);
760
f0200e91b272 added qed and qed_goal[w]
clasohm
parents: 685
diff changeset
   179
qed "Union_Un_distrib";
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   180
435
ca5356bd315a Addition of cardinals and order types, various tidying
lcp
parents: 268
diff changeset
   181
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
   182
by (fast_tac ZF_cs 1);
760
f0200e91b272 added qed and qed_goal[w]
clasohm
parents: 685
diff changeset
   183
qed "Union_Int_subset";
435
ca5356bd315a Addition of cardinals and order types, various tidying
lcp
parents: 268
diff changeset
   184
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   185
goal ZF.thy "Union(C) Int A = 0 <-> (ALL B:C. B Int A = 0)";
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   186
by (fast_tac (eq_cs addSEs [equalityE]) 1);
760
f0200e91b272 added qed and qed_goal[w]
clasohm
parents: 685
diff changeset
   187
qed "Union_disjoint";
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   188
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   189
(* A good challenge: Inter is ill-behaved on the empty set *)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   190
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
   191
by (fast_tac eq_cs 1);
760
f0200e91b272 added qed and qed_goal[w]
clasohm
parents: 685
diff changeset
   192
qed "Inter_Un_distrib";
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   193
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   194
goal ZF.thy "Union({b}) = b";
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   195
by (fast_tac eq_cs 1);
760
f0200e91b272 added qed and qed_goal[w]
clasohm
parents: 685
diff changeset
   196
qed "Union_singleton";
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   197
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   198
goal ZF.thy "Inter({b}) = b";
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   199
by (fast_tac eq_cs 1);
760
f0200e91b272 added qed and qed_goal[w]
clasohm
parents: 685
diff changeset
   200
qed "Inter_singleton";
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   201
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   202
(** Unions and Intersections of Families **)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   203
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   204
goal ZF.thy "Union(A) = (UN x:A. x)";
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   205
by (fast_tac eq_cs 1);
760
f0200e91b272 added qed and qed_goal[w]
clasohm
parents: 685
diff changeset
   206
qed "Union_eq_UN";
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   207
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   208
goalw ZF.thy [Inter_def] "Inter(A) = (INT x:A. x)";
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   209
by (fast_tac eq_cs 1);
760
f0200e91b272 added qed and qed_goal[w]
clasohm
parents: 685
diff changeset
   210
qed "Inter_eq_INT";
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   211
517
a9f93400f307 for infinite datatypes with arbitrary index sets
lcp
parents: 435
diff changeset
   212
goal ZF.thy "(UN i:0. A(i)) = 0";
a9f93400f307 for infinite datatypes with arbitrary index sets
lcp
parents: 435
diff changeset
   213
by (fast_tac eq_cs 1);
760
f0200e91b272 added qed and qed_goal[w]
clasohm
parents: 685
diff changeset
   214
qed "UN_0";
517
a9f93400f307 for infinite datatypes with arbitrary index sets
lcp
parents: 435
diff changeset
   215
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   216
(*Halmos, Naive Set Theory, page 35.*)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   217
goal ZF.thy "B Int (UN i:I. A(i)) = (UN i:I. B Int A(i))";
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   218
by (fast_tac eq_cs 1);
760
f0200e91b272 added qed and qed_goal[w]
clasohm
parents: 685
diff changeset
   219
qed "Int_UN_distrib";
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   220
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   221
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
   222
by (fast_tac eq_cs 1);
760
f0200e91b272 added qed and qed_goal[w]
clasohm
parents: 685
diff changeset
   223
qed "Un_INT_distrib";
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   224
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   225
goal ZF.thy
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   226
    "(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
   227
by (fast_tac eq_cs 1);
760
f0200e91b272 added qed and qed_goal[w]
clasohm
parents: 685
diff changeset
   228
qed "Int_UN_distrib2";
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   229
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   230
goal ZF.thy
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   231
    "!!I J. [| i:I;  j:J |] ==> \
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   232
\    (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
   233
by (fast_tac eq_cs 1);
760
f0200e91b272 added qed and qed_goal[w]
clasohm
parents: 685
diff changeset
   234
qed "Un_INT_distrib2";
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 ==> (UN 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);
760
f0200e91b272 added qed and qed_goal[w]
clasohm
parents: 685
diff changeset
   238
qed "UN_constant";
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   239
435
ca5356bd315a Addition of cardinals and order types, various tidying
lcp
parents: 268
diff changeset
   240
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
   241
by (fast_tac eq_cs 1);
760
f0200e91b272 added qed and qed_goal[w]
clasohm
parents: 685
diff changeset
   242
qed "INT_constant";
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   243
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   244
(** Devlin, Fundamentals of Contemporary Set Theory, page 12, exercise 5: 
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   245
    Union of a family of unions **)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   246
192
3dc5c8016a0e ZF/equalities/SUM_eq_UN: new
lcp
parents: 182
diff changeset
   247
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
   248
by (fast_tac eq_cs 1);
760
f0200e91b272 added qed and qed_goal[w]
clasohm
parents: 685
diff changeset
   249
qed "UN_Un_distrib";
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   250
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   251
goal ZF.thy
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   252
    "!!A B. i:I ==> \
192
3dc5c8016a0e ZF/equalities/SUM_eq_UN: new
lcp
parents: 182
diff changeset
   253
\           (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
   254
by (fast_tac eq_cs 1);
760
f0200e91b272 added qed and qed_goal[w]
clasohm
parents: 685
diff changeset
   255
qed "INT_Int_distrib";
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   256
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   257
(** Devlin, page 12, exercise 5: Complements **)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   258
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   259
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
   260
by (fast_tac eq_cs 1);
760
f0200e91b272 added qed and qed_goal[w]
clasohm
parents: 685
diff changeset
   261
qed "Diff_UN";
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   262
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   263
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
   264
by (fast_tac eq_cs 1);
760
f0200e91b272 added qed and qed_goal[w]
clasohm
parents: 685
diff changeset
   265
qed "Diff_INT";
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   266
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   267
(** Unions and Intersections with General Sum **)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   268
520
806d3f00590d ZF/equalities/Sigma_cons: new
lcp
parents: 517
diff changeset
   269
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
   270
by (fast_tac eq_cs 1);
760
f0200e91b272 added qed and qed_goal[w]
clasohm
parents: 685
diff changeset
   271
qed "Sigma_cons";
520
806d3f00590d ZF/equalities/Sigma_cons: new
lcp
parents: 517
diff changeset
   272
182
e30b55c07235 New distributive laws for Sigma and UN
lcp
parents: 0
diff changeset
   273
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
   274
by (fast_tac eq_cs 1);
760
f0200e91b272 added qed and qed_goal[w]
clasohm
parents: 685
diff changeset
   275
qed "SUM_UN_distrib1";
182
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: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
   278
by (fast_tac eq_cs 1);
760
f0200e91b272 added qed and qed_goal[w]
clasohm
parents: 685
diff changeset
   279
qed "SUM_UN_distrib2";
182
e30b55c07235 New distributive laws for Sigma and UN
lcp
parents: 0
diff changeset
   280
192
3dc5c8016a0e ZF/equalities/SUM_eq_UN: new
lcp
parents: 182
diff changeset
   281
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
   282
by (fast_tac eq_cs 1);
760
f0200e91b272 added qed and qed_goal[w]
clasohm
parents: 685
diff changeset
   283
qed "SUM_Un_distrib1";
0
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. A(i) Un B(i)) = (SUM i:I. A(i)) Un (SUM i:I. B(i))";
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   286
by (fast_tac eq_cs 1);
760
f0200e91b272 added qed and qed_goal[w]
clasohm
parents: 685
diff changeset
   287
qed "SUM_Un_distrib2";
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   288
685
0727f0c0c4f0 ZF/equalities/domain_converse,range_converse,
lcp
parents: 536
diff changeset
   289
(*First-order version of the above, for rewriting*)
0727f0c0c4f0 ZF/equalities/domain_converse,range_converse,
lcp
parents: 536
diff changeset
   290
goal ZF.thy "I * (A Un B) = I*A Un I*B";
0727f0c0c4f0 ZF/equalities/domain_converse,range_converse,
lcp
parents: 536
diff changeset
   291
by (resolve_tac [SUM_Un_distrib2] 1);
760
f0200e91b272 added qed and qed_goal[w]
clasohm
parents: 685
diff changeset
   292
qed "prod_Un_distrib2";
685
0727f0c0c4f0 ZF/equalities/domain_converse,range_converse,
lcp
parents: 536
diff changeset
   293
192
3dc5c8016a0e ZF/equalities/SUM_eq_UN: new
lcp
parents: 182
diff changeset
   294
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
   295
by (fast_tac eq_cs 1);
760
f0200e91b272 added qed and qed_goal[w]
clasohm
parents: 685
diff changeset
   296
qed "SUM_Int_distrib1";
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   297
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   298
goal ZF.thy
192
3dc5c8016a0e ZF/equalities/SUM_eq_UN: new
lcp
parents: 182
diff changeset
   299
    "(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
   300
by (fast_tac eq_cs 1);
760
f0200e91b272 added qed and qed_goal[w]
clasohm
parents: 685
diff changeset
   301
qed "SUM_Int_distrib2";
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   302
685
0727f0c0c4f0 ZF/equalities/domain_converse,range_converse,
lcp
parents: 536
diff changeset
   303
(*First-order version of the above, for rewriting*)
0727f0c0c4f0 ZF/equalities/domain_converse,range_converse,
lcp
parents: 536
diff changeset
   304
goal ZF.thy "I * (A Int B) = I*A Int I*B";
0727f0c0c4f0 ZF/equalities/domain_converse,range_converse,
lcp
parents: 536
diff changeset
   305
by (resolve_tac [SUM_Int_distrib2] 1);
760
f0200e91b272 added qed and qed_goal[w]
clasohm
parents: 685
diff changeset
   306
qed "prod_Int_distrib2";
685
0727f0c0c4f0 ZF/equalities/domain_converse,range_converse,
lcp
parents: 536
diff changeset
   307
192
3dc5c8016a0e ZF/equalities/SUM_eq_UN: new
lcp
parents: 182
diff changeset
   308
(*Cf Aczel, Non-Well-Founded Sets, page 115*)
3dc5c8016a0e ZF/equalities/SUM_eq_UN: new
lcp
parents: 182
diff changeset
   309
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
   310
by (fast_tac eq_cs 1);
760
f0200e91b272 added qed and qed_goal[w]
clasohm
parents: 685
diff changeset
   311
qed "SUM_eq_UN";
192
3dc5c8016a0e ZF/equalities/SUM_eq_UN: new
lcp
parents: 182
diff changeset
   312
536
5fbfa997f1b0 ZF/domrange/domain_of_prod, domain_empty, etc: moved to equalities.ML where
lcp
parents: 520
diff changeset
   313
(** Domain **)
5fbfa997f1b0 ZF/domrange/domain_of_prod, domain_empty, etc: moved to equalities.ML where
lcp
parents: 520
diff changeset
   314
760
f0200e91b272 added qed and qed_goal[w]
clasohm
parents: 685
diff changeset
   315
qed_goal "domain_of_prod" ZF.thy "!!A B. b:B ==> domain(A*B) = A"
536
5fbfa997f1b0 ZF/domrange/domain_of_prod, domain_empty, etc: moved to equalities.ML where
lcp
parents: 520
diff changeset
   316
 (fn _ => [ fast_tac eq_cs 1 ]);
5fbfa997f1b0 ZF/domrange/domain_of_prod, domain_empty, etc: moved to equalities.ML where
lcp
parents: 520
diff changeset
   317
760
f0200e91b272 added qed and qed_goal[w]
clasohm
parents: 685
diff changeset
   318
qed_goal "domain_0" ZF.thy "domain(0) = 0"
536
5fbfa997f1b0 ZF/domrange/domain_of_prod, domain_empty, etc: moved to equalities.ML where
lcp
parents: 520
diff changeset
   319
 (fn _ => [ fast_tac eq_cs 1 ]);
5fbfa997f1b0 ZF/domrange/domain_of_prod, domain_empty, etc: moved to equalities.ML where
lcp
parents: 520
diff changeset
   320
760
f0200e91b272 added qed and qed_goal[w]
clasohm
parents: 685
diff changeset
   321
qed_goal "domain_cons" ZF.thy
536
5fbfa997f1b0 ZF/domrange/domain_of_prod, domain_empty, etc: moved to equalities.ML where
lcp
parents: 520
diff changeset
   322
    "domain(cons(<a,b>,r)) = cons(a, domain(r))"
5fbfa997f1b0 ZF/domrange/domain_of_prod, domain_empty, etc: moved to equalities.ML where
lcp
parents: 520
diff changeset
   323
 (fn _ => [ fast_tac eq_cs 1 ]);
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   324
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   325
goal ZF.thy "domain(A Un B) = domain(A) Un domain(B)";
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   326
by (fast_tac eq_cs 1);
760
f0200e91b272 added qed and qed_goal[w]
clasohm
parents: 685
diff changeset
   327
qed "domain_Un_eq";
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   328
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   329
goal ZF.thy "domain(A Int B) <= domain(A) Int domain(B)";
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   330
by (fast_tac eq_cs 1);
760
f0200e91b272 added qed and qed_goal[w]
clasohm
parents: 685
diff changeset
   331
qed "domain_Int_subset";
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   332
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   333
goal ZF.thy "domain(A) - domain(B) <= domain(A - B)";
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   334
by (fast_tac eq_cs 1);
760
f0200e91b272 added qed and qed_goal[w]
clasohm
parents: 685
diff changeset
   335
qed "domain_diff_subset";
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   336
685
0727f0c0c4f0 ZF/equalities/domain_converse,range_converse,
lcp
parents: 536
diff changeset
   337
goal ZF.thy "domain(converse(r)) = range(r)";
0727f0c0c4f0 ZF/equalities/domain_converse,range_converse,
lcp
parents: 536
diff changeset
   338
by (fast_tac eq_cs 1);
760
f0200e91b272 added qed and qed_goal[w]
clasohm
parents: 685
diff changeset
   339
qed "domain_converse";
685
0727f0c0c4f0 ZF/equalities/domain_converse,range_converse,
lcp
parents: 536
diff changeset
   340
0727f0c0c4f0 ZF/equalities/domain_converse,range_converse,
lcp
parents: 536
diff changeset
   341
0727f0c0c4f0 ZF/equalities/domain_converse,range_converse,
lcp
parents: 536
diff changeset
   342
536
5fbfa997f1b0 ZF/domrange/domain_of_prod, domain_empty, etc: moved to equalities.ML where
lcp
parents: 520
diff changeset
   343
(** Range **)
5fbfa997f1b0 ZF/domrange/domain_of_prod, domain_empty, etc: moved to equalities.ML where
lcp
parents: 520
diff changeset
   344
760
f0200e91b272 added qed and qed_goal[w]
clasohm
parents: 685
diff changeset
   345
qed_goal "range_of_prod" ZF.thy
536
5fbfa997f1b0 ZF/domrange/domain_of_prod, domain_empty, etc: moved to equalities.ML where
lcp
parents: 520
diff changeset
   346
    "!!a A B. a:A ==> range(A*B) = B"
5fbfa997f1b0 ZF/domrange/domain_of_prod, domain_empty, etc: moved to equalities.ML where
lcp
parents: 520
diff changeset
   347
 (fn _ => [ fast_tac eq_cs 1 ]);
5fbfa997f1b0 ZF/domrange/domain_of_prod, domain_empty, etc: moved to equalities.ML where
lcp
parents: 520
diff changeset
   348
760
f0200e91b272 added qed and qed_goal[w]
clasohm
parents: 685
diff changeset
   349
qed_goal "range_0" ZF.thy "range(0) = 0"
536
5fbfa997f1b0 ZF/domrange/domain_of_prod, domain_empty, etc: moved to equalities.ML where
lcp
parents: 520
diff changeset
   350
 (fn _ => [ fast_tac eq_cs 1 ]); 
5fbfa997f1b0 ZF/domrange/domain_of_prod, domain_empty, etc: moved to equalities.ML where
lcp
parents: 520
diff changeset
   351
760
f0200e91b272 added qed and qed_goal[w]
clasohm
parents: 685
diff changeset
   352
qed_goal "range_cons" ZF.thy
536
5fbfa997f1b0 ZF/domrange/domain_of_prod, domain_empty, etc: moved to equalities.ML where
lcp
parents: 520
diff changeset
   353
    "range(cons(<a,b>,r)) = cons(b, range(r))"
5fbfa997f1b0 ZF/domrange/domain_of_prod, domain_empty, etc: moved to equalities.ML where
lcp
parents: 520
diff changeset
   354
 (fn _ => [ fast_tac eq_cs 1 ]);
5fbfa997f1b0 ZF/domrange/domain_of_prod, domain_empty, etc: moved to equalities.ML where
lcp
parents: 520
diff changeset
   355
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   356
goal ZF.thy "range(A Un B) = range(A) Un range(B)";
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   357
by (fast_tac eq_cs 1);
760
f0200e91b272 added qed and qed_goal[w]
clasohm
parents: 685
diff changeset
   358
qed "range_Un_eq";
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   359
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   360
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
   361
by (fast_tac ZF_cs 1);
760
f0200e91b272 added qed and qed_goal[w]
clasohm
parents: 685
diff changeset
   362
qed "range_Int_subset";
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   363
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   364
goal ZF.thy "range(A) - range(B) <= range(A - B)";
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   365
by (fast_tac eq_cs 1);
760
f0200e91b272 added qed and qed_goal[w]
clasohm
parents: 685
diff changeset
   366
qed "range_diff_subset";
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   367
685
0727f0c0c4f0 ZF/equalities/domain_converse,range_converse,
lcp
parents: 536
diff changeset
   368
goal ZF.thy "range(converse(r)) = domain(r)";
0727f0c0c4f0 ZF/equalities/domain_converse,range_converse,
lcp
parents: 536
diff changeset
   369
by (fast_tac eq_cs 1);
760
f0200e91b272 added qed and qed_goal[w]
clasohm
parents: 685
diff changeset
   370
qed "range_converse";
685
0727f0c0c4f0 ZF/equalities/domain_converse,range_converse,
lcp
parents: 536
diff changeset
   371
536
5fbfa997f1b0 ZF/domrange/domain_of_prod, domain_empty, etc: moved to equalities.ML where
lcp
parents: 520
diff changeset
   372
(** Field **)
5fbfa997f1b0 ZF/domrange/domain_of_prod, domain_empty, etc: moved to equalities.ML where
lcp
parents: 520
diff changeset
   373
760
f0200e91b272 added qed and qed_goal[w]
clasohm
parents: 685
diff changeset
   374
qed_goal "field_of_prod" ZF.thy "field(A*A) = A"
536
5fbfa997f1b0 ZF/domrange/domain_of_prod, domain_empty, etc: moved to equalities.ML where
lcp
parents: 520
diff changeset
   375
 (fn _ => [ fast_tac eq_cs 1 ]); 
5fbfa997f1b0 ZF/domrange/domain_of_prod, domain_empty, etc: moved to equalities.ML where
lcp
parents: 520
diff changeset
   376
760
f0200e91b272 added qed and qed_goal[w]
clasohm
parents: 685
diff changeset
   377
qed_goal "field_0" ZF.thy "field(0) = 0"
536
5fbfa997f1b0 ZF/domrange/domain_of_prod, domain_empty, etc: moved to equalities.ML where
lcp
parents: 520
diff changeset
   378
 (fn _ => [ fast_tac eq_cs 1 ]); 
5fbfa997f1b0 ZF/domrange/domain_of_prod, domain_empty, etc: moved to equalities.ML where
lcp
parents: 520
diff changeset
   379
760
f0200e91b272 added qed and qed_goal[w]
clasohm
parents: 685
diff changeset
   380
qed_goal "field_cons" ZF.thy
536
5fbfa997f1b0 ZF/domrange/domain_of_prod, domain_empty, etc: moved to equalities.ML where
lcp
parents: 520
diff changeset
   381
    "field(cons(<a,b>,r)) = cons(a, cons(b, field(r)))"
5fbfa997f1b0 ZF/domrange/domain_of_prod, domain_empty, etc: moved to equalities.ML where
lcp
parents: 520
diff changeset
   382
 (fn _ => [ rtac equalityI 1, ALLGOALS (fast_tac ZF_cs) ]);
5fbfa997f1b0 ZF/domrange/domain_of_prod, domain_empty, etc: moved to equalities.ML where
lcp
parents: 520
diff changeset
   383
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   384
goal ZF.thy "field(A Un B) = field(A) Un field(B)";
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   385
by (fast_tac eq_cs 1);
760
f0200e91b272 added qed and qed_goal[w]
clasohm
parents: 685
diff changeset
   386
qed "field_Un_eq";
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   387
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   388
goal ZF.thy "field(A Int B) <= field(A) Int field(B)";
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   389
by (fast_tac eq_cs 1);
760
f0200e91b272 added qed and qed_goal[w]
clasohm
parents: 685
diff changeset
   390
qed "field_Int_subset";
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   391
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   392
goal ZF.thy "field(A) - field(B) <= field(A - B)";
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   393
by (fast_tac eq_cs 1);
760
f0200e91b272 added qed and qed_goal[w]
clasohm
parents: 685
diff changeset
   394
qed "field_diff_subset";
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   395
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   396
435
ca5356bd315a Addition of cardinals and order types, various tidying
lcp
parents: 268
diff changeset
   397
(** Image **)
ca5356bd315a Addition of cardinals and order types, various tidying
lcp
parents: 268
diff changeset
   398
ca5356bd315a Addition of cardinals and order types, various tidying
lcp
parents: 268
diff changeset
   399
goal ZF.thy "r``0 = 0";
ca5356bd315a Addition of cardinals and order types, various tidying
lcp
parents: 268
diff changeset
   400
by (fast_tac eq_cs 1);
760
f0200e91b272 added qed and qed_goal[w]
clasohm
parents: 685
diff changeset
   401
qed "image_0";
435
ca5356bd315a Addition of cardinals and order types, various tidying
lcp
parents: 268
diff changeset
   402
ca5356bd315a Addition of cardinals and order types, various tidying
lcp
parents: 268
diff changeset
   403
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
   404
by (fast_tac eq_cs 1);
760
f0200e91b272 added qed and qed_goal[w]
clasohm
parents: 685
diff changeset
   405
qed "image_Un";
435
ca5356bd315a Addition of cardinals and order types, various tidying
lcp
parents: 268
diff changeset
   406
ca5356bd315a Addition of cardinals and order types, various tidying
lcp
parents: 268
diff changeset
   407
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
   408
by (fast_tac ZF_cs 1);
760
f0200e91b272 added qed and qed_goal[w]
clasohm
parents: 685
diff changeset
   409
qed "image_Int_subset";
435
ca5356bd315a Addition of cardinals and order types, various tidying
lcp
parents: 268
diff changeset
   410
ca5356bd315a Addition of cardinals and order types, various tidying
lcp
parents: 268
diff changeset
   411
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
   412
by (fast_tac ZF_cs 1);
760
f0200e91b272 added qed and qed_goal[w]
clasohm
parents: 685
diff changeset
   413
qed "image_Int_square_subset";
435
ca5356bd315a Addition of cardinals and order types, various tidying
lcp
parents: 268
diff changeset
   414
ca5356bd315a Addition of cardinals and order types, various tidying
lcp
parents: 268
diff changeset
   415
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
   416
by (fast_tac eq_cs 1);
760
f0200e91b272 added qed and qed_goal[w]
clasohm
parents: 685
diff changeset
   417
qed "image_Int_square";
435
ca5356bd315a Addition of cardinals and order types, various tidying
lcp
parents: 268
diff changeset
   418
ca5356bd315a Addition of cardinals and order types, various tidying
lcp
parents: 268
diff changeset
   419
ca5356bd315a Addition of cardinals and order types, various tidying
lcp
parents: 268
diff changeset
   420
(** Inverse Image **)
ca5356bd315a Addition of cardinals and order types, various tidying
lcp
parents: 268
diff changeset
   421
ca5356bd315a Addition of cardinals and order types, various tidying
lcp
parents: 268
diff changeset
   422
goal ZF.thy "r-``0 = 0";
ca5356bd315a Addition of cardinals and order types, various tidying
lcp
parents: 268
diff changeset
   423
by (fast_tac eq_cs 1);
760
f0200e91b272 added qed and qed_goal[w]
clasohm
parents: 685
diff changeset
   424
qed "vimage_0";
435
ca5356bd315a Addition of cardinals and order types, various tidying
lcp
parents: 268
diff changeset
   425
ca5356bd315a Addition of cardinals and order types, various tidying
lcp
parents: 268
diff changeset
   426
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
   427
by (fast_tac eq_cs 1);
760
f0200e91b272 added qed and qed_goal[w]
clasohm
parents: 685
diff changeset
   428
qed "vimage_Un";
435
ca5356bd315a Addition of cardinals and order types, various tidying
lcp
parents: 268
diff changeset
   429
ca5356bd315a Addition of cardinals and order types, various tidying
lcp
parents: 268
diff changeset
   430
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
   431
by (fast_tac ZF_cs 1);
760
f0200e91b272 added qed and qed_goal[w]
clasohm
parents: 685
diff changeset
   432
qed "vimage_Int_subset";
435
ca5356bd315a Addition of cardinals and order types, various tidying
lcp
parents: 268
diff changeset
   433
ca5356bd315a Addition of cardinals and order types, various tidying
lcp
parents: 268
diff changeset
   434
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
   435
by (fast_tac ZF_cs 1);
760
f0200e91b272 added qed and qed_goal[w]
clasohm
parents: 685
diff changeset
   436
qed "vimage_Int_square_subset";
435
ca5356bd315a Addition of cardinals and order types, various tidying
lcp
parents: 268
diff changeset
   437
ca5356bd315a Addition of cardinals and order types, various tidying
lcp
parents: 268
diff changeset
   438
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
   439
by (fast_tac eq_cs 1);
760
f0200e91b272 added qed and qed_goal[w]
clasohm
parents: 685
diff changeset
   440
qed "vimage_Int_square";
435
ca5356bd315a Addition of cardinals and order types, various tidying
lcp
parents: 268
diff changeset
   441
ca5356bd315a Addition of cardinals and order types, various tidying
lcp
parents: 268
diff changeset
   442
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   443
(** Converse **)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   444
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   445
goal ZF.thy "converse(A Un B) = converse(A) Un converse(B)";
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   446
by (fast_tac eq_cs 1);
760
f0200e91b272 added qed and qed_goal[w]
clasohm
parents: 685
diff changeset
   447
qed "converse_Un";
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   448
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   449
goal ZF.thy "converse(A Int B) = converse(A) Int converse(B)";
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   450
by (fast_tac eq_cs 1);
760
f0200e91b272 added qed and qed_goal[w]
clasohm
parents: 685
diff changeset
   451
qed "converse_Int";
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   452
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   453
goal ZF.thy "converse(A) - converse(B) = converse(A - B)";
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   454
by (fast_tac eq_cs 1);
760
f0200e91b272 added qed and qed_goal[w]
clasohm
parents: 685
diff changeset
   455
qed "converse_diff";
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   456
787
1affbb1c5f1f converse_UN, Diff_eq_0_iff: new
lcp
parents: 760
diff changeset
   457
(*Does the analogue hold for INT?*)
1affbb1c5f1f converse_UN, Diff_eq_0_iff: new
lcp
parents: 760
diff changeset
   458
goal ZF.thy "converse(UN x:A. B(x)) = (UN x:A. converse(B(x)))";
1affbb1c5f1f converse_UN, Diff_eq_0_iff: new
lcp
parents: 760
diff changeset
   459
by (fast_tac eq_cs 1);
1affbb1c5f1f converse_UN, Diff_eq_0_iff: new
lcp
parents: 760
diff changeset
   460
qed "converse_UN";
1affbb1c5f1f converse_UN, Diff_eq_0_iff: new
lcp
parents: 760
diff changeset
   461
198
0f0ff91b07f6 new section for equality properties
lcp
parents: 192
diff changeset
   462
(** Pow **)
0f0ff91b07f6 new section for equality properties
lcp
parents: 192
diff changeset
   463
0f0ff91b07f6 new section for equality properties
lcp
parents: 192
diff changeset
   464
goal ZF.thy "Pow(A) Un Pow(B) <= Pow(A Un B)";
0f0ff91b07f6 new section for equality properties
lcp
parents: 192
diff changeset
   465
by (fast_tac upair_cs 1);
760
f0200e91b272 added qed and qed_goal[w]
clasohm
parents: 685
diff changeset
   466
qed "Un_Pow_subset";
198
0f0ff91b07f6 new section for equality properties
lcp
parents: 192
diff changeset
   467
0f0ff91b07f6 new section for equality properties
lcp
parents: 192
diff changeset
   468
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
   469
by (fast_tac upair_cs 1);
760
f0200e91b272 added qed and qed_goal[w]
clasohm
parents: 685
diff changeset
   470
qed "UN_Pow_subset";
198
0f0ff91b07f6 new section for equality properties
lcp
parents: 192
diff changeset
   471
0f0ff91b07f6 new section for equality properties
lcp
parents: 192
diff changeset
   472
goal ZF.thy "A <= Pow(Union(A))";
0f0ff91b07f6 new section for equality properties
lcp
parents: 192
diff changeset
   473
by (fast_tac upair_cs 1);
760
f0200e91b272 added qed and qed_goal[w]
clasohm
parents: 685
diff changeset
   474
qed "subset_Pow_Union";
198
0f0ff91b07f6 new section for equality properties
lcp
parents: 192
diff changeset
   475
0f0ff91b07f6 new section for equality properties
lcp
parents: 192
diff changeset
   476
goal ZF.thy "Union(Pow(A)) = A";
0f0ff91b07f6 new section for equality properties
lcp
parents: 192
diff changeset
   477
by (fast_tac eq_cs 1);
760
f0200e91b272 added qed and qed_goal[w]
clasohm
parents: 685
diff changeset
   478
qed "Union_Pow_eq";
198
0f0ff91b07f6 new section for equality properties
lcp
parents: 192
diff changeset
   479
0f0ff91b07f6 new section for equality properties
lcp
parents: 192
diff changeset
   480
goal ZF.thy "Pow(A) Int Pow(B) = Pow(A Int B)";
0f0ff91b07f6 new section for equality properties
lcp
parents: 192
diff changeset
   481
by (fast_tac eq_cs 1);
760
f0200e91b272 added qed and qed_goal[w]
clasohm
parents: 685
diff changeset
   482
qed "Int_Pow_eq";
198
0f0ff91b07f6 new section for equality properties
lcp
parents: 192
diff changeset
   483
0f0ff91b07f6 new section for equality properties
lcp
parents: 192
diff changeset
   484
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
   485
by (fast_tac eq_cs 1);
760
f0200e91b272 added qed and qed_goal[w]
clasohm
parents: 685
diff changeset
   486
qed "INT_Pow_subset";
435
ca5356bd315a Addition of cardinals and order types, various tidying
lcp
parents: 268
diff changeset
   487
839
1aa6b351ca34 RepFun_eq_0_iff, RepFun_0: new
lcp
parents: 787
diff changeset
   488
(** RepFun **)
1aa6b351ca34 RepFun_eq_0_iff, RepFun_0: new
lcp
parents: 787
diff changeset
   489
1aa6b351ca34 RepFun_eq_0_iff, RepFun_0: new
lcp
parents: 787
diff changeset
   490
goal ZF.thy "{f(x).x:A}=0 <-> A=0";
1aa6b351ca34 RepFun_eq_0_iff, RepFun_0: new
lcp
parents: 787
diff changeset
   491
by (fast_tac (eq_cs addSEs [equalityE]) 1);
1aa6b351ca34 RepFun_eq_0_iff, RepFun_0: new
lcp
parents: 787
diff changeset
   492
qed "RepFun_eq_0_iff";
1aa6b351ca34 RepFun_eq_0_iff, RepFun_0: new
lcp
parents: 787
diff changeset
   493
1aa6b351ca34 RepFun_eq_0_iff, RepFun_0: new
lcp
parents: 787
diff changeset
   494
goal ZF.thy "{f(x).x:0} = 0";
1aa6b351ca34 RepFun_eq_0_iff, RepFun_0: new
lcp
parents: 787
diff changeset
   495
by (fast_tac eq_cs 1);
1aa6b351ca34 RepFun_eq_0_iff, RepFun_0: new
lcp
parents: 787
diff changeset
   496
qed "RepFun_0";