author  wenzelm 
Thu, 07 Sep 2000 21:12:49 +0200  
changeset 9907  473a6604da94 
parent 9303  f1ad1ed0d110 
child 11695  8c66866fb0ff 
permissions  rwrr 
1461  1 
(* Title: ZF/equalities 
0  2 
ID: $Id$ 
1461  3 
Author: Lawrence C Paulson, Cambridge University Computer Laboratory 
0  4 
Copyright 1992 University of Cambridge 
5 

6 
Set Theory examples: Union, Intersection, Inclusion, etc. 

7 
(Thanks also to Philippe de Groote.) 

8 
*) 

9 

10 
(** Finite Sets **) 

11 

520  12 
(* cons_def refers to Upair; reversing the equality LOOPS in rewriting!*) 
5321  13 
Goal "{a} Un B = cons(a,B)"; 
2877  14 
by (Blast_tac 1); 
760  15 
qed "cons_eq"; 
520  16 

5321  17 
Goal "cons(a, cons(b, C)) = cons(b, cons(a, C))"; 
2877  18 
by (Blast_tac 1); 
760  19 
qed "cons_commute"; 
0  20 

5321  21 
Goal "a: B ==> cons(a,B) = B"; 
2877  22 
by (Blast_tac 1); 
760  23 
qed "cons_absorb"; 
0  24 

5321  25 
Goal "a: B ==> cons(a, B{a}) = B"; 
2877  26 
by (Blast_tac 1); 
760  27 
qed "cons_Diff"; 
0  28 

5321  29 
Goal "[ a: C; ALL y:C. y=b ] ==> C = {b}"; 
2877  30 
by (Blast_tac 1); 
760  31 
qed "equal_singleton_lemma"; 
9907  32 
bind_thm ("equal_singleton", ballI RSN (2,equal_singleton_lemma)); 
0  33 

34 

35 
(** Binary Intersection **) 

36 

37 
(*NOT an equality, but it seems to belong here...*) 

5321  38 
Goal "cons(a,B) Int C <= cons(a, B Int C)"; 
2877  39 
by (Blast_tac 1); 
760  40 
qed "Int_cons"; 
0  41 

5321  42 
Goal "A Int A = A"; 
2877  43 
by (Blast_tac 1); 
760  44 
qed "Int_absorb"; 
0  45 

5321  46 
Goal "A Int B = B Int A"; 
2877  47 
by (Blast_tac 1); 
760  48 
qed "Int_commute"; 
0  49 

5321  50 
Goal "(A Int B) Int C = A Int (B Int C)"; 
2877  51 
by (Blast_tac 1); 
760  52 
qed "Int_assoc"; 
0  53 

5321  54 
Goal "(A Un B) Int C = (A Int C) Un (B Int C)"; 
2877  55 
by (Blast_tac 1); 
760  56 
qed "Int_Un_distrib"; 
0  57 

5321  58 
Goal "A<=B <> A Int B = A"; 
4091  59 
by (blast_tac (claset() addSEs [equalityE]) 1); 
760  60 
qed "subset_Int_iff"; 
0  61 

5321  62 
Goal "A<=B <> B Int A = A"; 
4091  63 
by (blast_tac (claset() addSEs [equalityE]) 1); 
760  64 
qed "subset_Int_iff2"; 
435  65 

5321  66 
Goal "C<=A ==> (AB) Int C = CB"; 
2877  67 
by (Blast_tac 1); 
1035  68 
qed "Int_Diff_eq"; 
69 

0  70 
(** Binary Union **) 
71 

5321  72 
Goal "cons(a,B) Un C = cons(a, B Un C)"; 
2877  73 
by (Blast_tac 1); 
760  74 
qed "Un_cons"; 
0  75 

5321  76 
Goal "A Un A = A"; 
2877  77 
by (Blast_tac 1); 
760  78 
qed "Un_absorb"; 
0  79 

5321  80 
Goal "A Un B = B Un A"; 
2877  81 
by (Blast_tac 1); 
760  82 
qed "Un_commute"; 
0  83 

5321  84 
Goal "(A Un B) Un C = A Un (B Un C)"; 
2877  85 
by (Blast_tac 1); 
760  86 
qed "Un_assoc"; 
0  87 

5321  88 
Goal "(A Int B) Un C = (A Un C) Int (B Un C)"; 
2877  89 
by (Blast_tac 1); 
760  90 
qed "Un_Int_distrib"; 
0  91 

5321  92 
Goal "A<=B <> A Un B = B"; 
4091  93 
by (blast_tac (claset() addSEs [equalityE]) 1); 
760  94 
qed "subset_Un_iff"; 
0  95 

5321  96 
Goal "A<=B <> B Un A = B"; 
4091  97 
by (blast_tac (claset() addSEs [equalityE]) 1); 
760  98 
qed "subset_Un_iff2"; 
435  99 

0  100 
(** Simple properties of Diff  set difference **) 
101 

5321  102 
Goal "AA = 0"; 
2877  103 
by (Blast_tac 1); 
760  104 
qed "Diff_cancel"; 
0  105 

5321  106 
Goal "0A = 0"; 
2877  107 
by (Blast_tac 1); 
760  108 
qed "empty_Diff"; 
0  109 

5321  110 
Goal "A0 = A"; 
2877  111 
by (Blast_tac 1); 
760  112 
qed "Diff_0"; 
0  113 

5321  114 
Goal "AB=0 <> A<=B"; 
4091  115 
by (blast_tac (claset() addEs [equalityE]) 1); 
787  116 
qed "Diff_eq_0_iff"; 
117 

0  118 
(*NOT SUITABLE FOR REWRITING since {a} == cons(a,0)*) 
5321  119 
Goal "A  cons(a,B) = A  B  {a}"; 
2877  120 
by (Blast_tac 1); 
760  121 
qed "Diff_cons"; 
0  122 

123 
(*NOT SUITABLE FOR REWRITING since {a} == cons(a,0)*) 

5321  124 
Goal "A  cons(a,B) = A  {a}  B"; 
2877  125 
by (Blast_tac 1); 
760  126 
qed "Diff_cons2"; 
0  127 

5321  128 
Goal "A Int (BA) = 0"; 
2877  129 
by (Blast_tac 1); 
760  130 
qed "Diff_disjoint"; 
0  131 

5321  132 
Goal "A<=B ==> A Un (BA) = B"; 
2877  133 
by (Blast_tac 1); 
760  134 
qed "Diff_partition"; 
0  135 

5321  136 
Goal "A <= B Un (A  B)"; 
2877  137 
by (Blast_tac 1); 
1611  138 
qed "subset_Un_Diff"; 
139 

5321  140 
Goal "[ A<=B; B<=C ] ==> B(CA) = A"; 
2877  141 
by (Blast_tac 1); 
760  142 
qed "double_complement"; 
0  143 

5321  144 
Goal "(A Un B)  (BA) = A"; 
2877  145 
by (Blast_tac 1); 
760  146 
qed "double_complement_Un"; 
268  147 

5321  148 
Goal 
0  149 
"(A Int B) Un (B Int C) Un (C Int A) = (A Un B) Int (B Un C) Int (C Un A)"; 
2877  150 
by (Blast_tac 1); 
760  151 
qed "Un_Int_crazy"; 
0  152 

5321  153 
Goal "A  (B Un C) = (AB) Int (AC)"; 
2877  154 
by (Blast_tac 1); 
760  155 
qed "Diff_Un"; 
0  156 

5321  157 
Goal "A  (B Int C) = (AB) Un (AC)"; 
2877  158 
by (Blast_tac 1); 
760  159 
qed "Diff_Int"; 
0  160 

161 
(*Halmos, Naive Set Theory, page 16.*) 

5321  162 
Goal "(A Int B) Un C = A Int (B Un C) <> C<=A"; 
4091  163 
by (blast_tac (claset() addSEs [equalityE]) 1); 
760  164 
qed "Un_Int_assoc_iff"; 
0  165 

166 

167 
(** Big Union and Intersection **) 

168 

5321  169 
Goal "Union(cons(a,B)) = a Un Union(B)"; 
2877  170 
by (Blast_tac 1); 
760  171 
qed "Union_cons"; 
0  172 

5321  173 
Goal "Union(A Un B) = Union(A) Un Union(B)"; 
2877  174 
by (Blast_tac 1); 
760  175 
qed "Union_Un_distrib"; 
0  176 

5321  177 
Goal "Union(A Int B) <= Union(A) Int Union(B)"; 
2877  178 
by (Blast_tac 1); 
760  179 
qed "Union_Int_subset"; 
435  180 

5321  181 
Goal "Union(C) Int A = 0 <> (ALL B:C. B Int A = 0)"; 
4091  182 
by (blast_tac (claset() addSEs [equalityE]) 1); 
760  183 
qed "Union_disjoint"; 
0  184 

5325
f7a5e06adea1
Yet more removal of "goal" commands, especially "goal ZF.thy", so ZF.thy
paulson
parents:
5321
diff
changeset

185 
Goal "Union(A) = 0 <> (ALL B:A. B=0)"; 
f7a5e06adea1
Yet more removal of "goal" commands, especially "goal ZF.thy", so ZF.thy
paulson
parents:
5321
diff
changeset

186 
by (Blast_tac 1); 
f7a5e06adea1
Yet more removal of "goal" commands, especially "goal ZF.thy", so ZF.thy
paulson
parents:
5321
diff
changeset

187 
qed "Union_empty_iff"; 
f7a5e06adea1
Yet more removal of "goal" commands, especially "goal ZF.thy", so ZF.thy
paulson
parents:
5321
diff
changeset

188 

f7a5e06adea1
Yet more removal of "goal" commands, especially "goal ZF.thy", so ZF.thy
paulson
parents:
5321
diff
changeset

189 
Goalw [Inter_def] "Inter(0) = 0"; 
2877  190 
by (Blast_tac 1); 
1652  191 
qed "Inter_0"; 
192 

5321  193 
Goal "[ z:A; z:B ] ==> Inter(A) Un Inter(B) <= Inter(A Int B)"; 
2877  194 
by (Blast_tac 1); 
1568  195 
qed "Inter_Un_subset"; 
196 

0  197 
(* A good challenge: Inter is illbehaved on the empty set *) 
5321  198 
Goal "[ a:A; b:B ] ==> Inter(A Un B) = Inter(A) Int Inter(B)"; 
2877  199 
by (Blast_tac 1); 
760  200 
qed "Inter_Un_distrib"; 
0  201 

5321  202 
Goal "Union({b}) = b"; 
2877  203 
by (Blast_tac 1); 
760  204 
qed "Union_singleton"; 
0  205 

5321  206 
Goal "Inter({b}) = b"; 
2877  207 
by (Blast_tac 1); 
760  208 
qed "Inter_singleton"; 
0  209 

210 
(** Unions and Intersections of Families **) 

211 

5321  212 
Goal "Union(A) = (UN x:A. x)"; 
2877  213 
by (Blast_tac 1); 
760  214 
qed "Union_eq_UN"; 
0  215 

5325
f7a5e06adea1
Yet more removal of "goal" commands, especially "goal ZF.thy", so ZF.thy
paulson
parents:
5321
diff
changeset

216 
Goalw [Inter_def] "Inter(A) = (INT x:A. x)"; 
2877  217 
by (Blast_tac 1); 
760  218 
qed "Inter_eq_INT"; 
0  219 

5321  220 
Goal "(UN i:0. A(i)) = 0"; 
2877  221 
by (Blast_tac 1); 
760  222 
qed "UN_0"; 
517  223 

0  224 
(*Halmos, Naive Set Theory, page 35.*) 
5321  225 
Goal "B Int (UN i:I. A(i)) = (UN i:I. B Int A(i))"; 
2877  226 
by (Blast_tac 1); 
760  227 
qed "Int_UN_distrib"; 
0  228 

5321  229 
Goal "i:I ==> B Un (INT i:I. A(i)) = (INT i:I. B Un A(i))"; 
2877  230 
by (Blast_tac 1); 
760  231 
qed "Un_INT_distrib"; 
0  232 

5321  233 
Goal "(UN i:I. A(i)) Int (UN j:J. B(j)) = (UN i:I. UN j:J. A(i) Int B(j))"; 
2877  234 
by (Blast_tac 1); 
760  235 
qed "Int_UN_distrib2"; 
0  236 

5321  237 
Goal "[ i:I; j:J ] ==> \ 
238 
\ (INT i:I. A(i)) Un (INT j:J. B(j)) = (INT i:I. INT j:J. A(i) Un B(j))"; 

2877  239 
by (Blast_tac 1); 
760  240 
qed "Un_INT_distrib2"; 
0  241 

5321  242 
Goal "a: A ==> (UN y:A. c) = c"; 
2877  243 
by (Blast_tac 1); 
760  244 
qed "UN_constant"; 
0  245 

5321  246 
Goal "a: A ==> (INT y:A. c) = c"; 
2877  247 
by (Blast_tac 1); 
760  248 
qed "INT_constant"; 
0  249 

5321  250 
Goal "(UN y: RepFun(A,f). B(y)) = (UN x:A. B(f(x)))"; 
4242  251 
by (Blast_tac 1); 
252 
qed "UN_RepFun"; 

253 

5321  254 
Goal "x:A ==> (INT y: RepFun(A,f). B(y)) = (INT x:A. B(f(x)))"; 
4242  255 
by (Blast_tac 1); 
256 
qed "INT_RepFun"; 

257 

258 
Addsimps [UN_RepFun, INT_RepFun]; 

259 

260 

0  261 
(** Devlin, Fundamentals of Contemporary Set Theory, page 12, exercise 5: 
262 
Union of a family of unions **) 

263 

5321  264 
Goal "(UN i:I. A(i) Un B(i)) = (UN i:I. A(i)) Un (UN i:I. B(i))"; 
2877  265 
by (Blast_tac 1); 
760  266 
qed "UN_Un_distrib"; 
0  267 

5321  268 
Goal "i:I ==> (INT i:I. A(i) Int B(i)) = (INT i:I. A(i)) Int (INT i:I. B(i))"; 
2877  269 
by (Blast_tac 1); 
760  270 
qed "INT_Int_distrib"; 
0  271 

5321  272 
Goal "(UN z:I Int J. A(z)) <= (UN z:I. A(z)) Int (UN z:J. A(z))"; 
2877  273 
by (Blast_tac 1); 
1784  274 
qed "UN_Int_subset"; 
275 

0  276 
(** Devlin, page 12, exercise 5: Complements **) 
277 

5321  278 
Goal "i:I ==> B  (UN i:I. A(i)) = (INT i:I. B  A(i))"; 
2877  279 
by (Blast_tac 1); 
760  280 
qed "Diff_UN"; 
0  281 

5321  282 
Goal "i:I ==> B  (INT i:I. A(i)) = (UN i:I. B  A(i))"; 
2877  283 
by (Blast_tac 1); 
760  284 
qed "Diff_INT"; 
0  285 

286 
(** Unions and Intersections with General Sum **) 

287 

1611  288 
(*Not suitable for rewriting: LOOPS!*) 
5321  289 
Goal "Sigma(cons(a,B), C) = ({a}*C(a)) Un Sigma(B,C)"; 
2877  290 
by (Blast_tac 1); 
1611  291 
qed "Sigma_cons1"; 
292 

293 
(*Not suitable for rewriting: LOOPS!*) 

5321  294 
Goal "A * cons(b,B) = A*{b} Un A*B"; 
2877  295 
by (Blast_tac 1); 
1611  296 
qed "Sigma_cons2"; 
297 

5321  298 
Goal "Sigma(succ(A), B) = ({A}*B(A)) Un Sigma(A,B)"; 
2877  299 
by (Blast_tac 1); 
1611  300 
qed "Sigma_succ1"; 
301 

5321  302 
Goal "A * succ(B) = A*{B} Un A*B"; 
2877  303 
by (Blast_tac 1); 
1611  304 
qed "Sigma_succ2"; 
520  305 

5321  306 
Goal "(SUM x:(UN y:A. C(y)). B(x)) = (UN y:A. SUM x:C(y). B(x))"; 
2877  307 
by (Blast_tac 1); 
760  308 
qed "SUM_UN_distrib1"; 
182  309 

5321  310 
Goal "(SUM i:I. UN j:J. C(i,j)) = (UN j:J. SUM i:I. C(i,j))"; 
2877  311 
by (Blast_tac 1); 
760  312 
qed "SUM_UN_distrib2"; 
182  313 

5321  314 
Goal "(SUM i:I Un J. C(i)) = (SUM i:I. C(i)) Un (SUM j:J. C(j))"; 
2877  315 
by (Blast_tac 1); 
760  316 
qed "SUM_Un_distrib1"; 
0  317 

5321  318 
Goal "(SUM i:I. A(i) Un B(i)) = (SUM i:I. A(i)) Un (SUM i:I. B(i))"; 
2877  319 
by (Blast_tac 1); 
760  320 
qed "SUM_Un_distrib2"; 
0  321 

685  322 
(*Firstorder version of the above, for rewriting*) 
5321  323 
Goal "I * (A Un B) = I*A Un I*B"; 
1461  324 
by (rtac SUM_Un_distrib2 1); 
760  325 
qed "prod_Un_distrib2"; 
685  326 

5321  327 
Goal "(SUM i:I Int J. C(i)) = (SUM i:I. C(i)) Int (SUM j:J. C(j))"; 
2877  328 
by (Blast_tac 1); 
760  329 
qed "SUM_Int_distrib1"; 
0  330 

5321  331 
Goal "(SUM i:I. A(i) Int B(i)) = (SUM i:I. A(i)) Int (SUM i:I. B(i))"; 
2877  332 
by (Blast_tac 1); 
760  333 
qed "SUM_Int_distrib2"; 
0  334 

685  335 
(*Firstorder version of the above, for rewriting*) 
5321  336 
Goal "I * (A Int B) = I*A Int I*B"; 
1461  337 
by (rtac SUM_Int_distrib2 1); 
760  338 
qed "prod_Int_distrib2"; 
685  339 

192  340 
(*Cf Aczel, NonWellFounded Sets, page 115*) 
5321  341 
Goal "(SUM i:I. A(i)) = (UN i:I. {i} * A(i))"; 
2877  342 
by (Blast_tac 1); 
760  343 
qed "SUM_eq_UN"; 
192  344 

536
5fbfa997f1b0
ZF/domrange/domain_of_prod, domain_empty, etc: moved to equalities.ML where
lcp
parents:
520
diff
changeset

345 
(** Domain **) 
5fbfa997f1b0
ZF/domrange/domain_of_prod, domain_empty, etc: moved to equalities.ML where
lcp
parents:
520
diff
changeset

346 

5321  347 
Goal "b:B ==> domain(A*B) = A"; 
348 
by (Blast_tac 1); 

349 
qed "domain_of_prod"; 

536
5fbfa997f1b0
ZF/domrange/domain_of_prod, domain_empty, etc: moved to equalities.ML where
lcp
parents:
520
diff
changeset

350 

9180  351 
Goal "domain(0) = 0"; 
352 
by (Blast_tac 1); 

353 
qed "domain_0"; 

536
5fbfa997f1b0
ZF/domrange/domain_of_prod, domain_empty, etc: moved to equalities.ML where
lcp
parents:
520
diff
changeset

354 

9180  355 
Goal "domain(cons(<a,b>,r)) = cons(a, domain(r))"; 
356 
by (Blast_tac 1); 

357 
qed "domain_cons"; 

0  358 

5321  359 
Goal "domain(A Un B) = domain(A) Un domain(B)"; 
2877  360 
by (Blast_tac 1); 
760  361 
qed "domain_Un_eq"; 
0  362 

5321  363 
Goal "domain(A Int B) <= domain(A) Int domain(B)"; 
2877  364 
by (Blast_tac 1); 
760  365 
qed "domain_Int_subset"; 
0  366 

5321  367 
Goal "domain(A)  domain(B) <= domain(A  B)"; 
2877  368 
by (Blast_tac 1); 
1056  369 
qed "domain_Diff_subset"; 
0  370 

5321  371 
Goal "domain(converse(r)) = range(r)"; 
2877  372 
by (Blast_tac 1); 
760  373 
qed "domain_converse"; 
685  374 

2469  375 
Addsimps [domain_0, domain_cons, domain_Un_eq, domain_converse]; 
685  376 

377 

536
5fbfa997f1b0
ZF/domrange/domain_of_prod, domain_empty, etc: moved to equalities.ML where
lcp
parents:
520
diff
changeset

378 
(** Range **) 
5fbfa997f1b0
ZF/domrange/domain_of_prod, domain_empty, etc: moved to equalities.ML where
lcp
parents:
520
diff
changeset

379 

5321  380 
Goal "a:A ==> range(A*B) = B"; 
381 
by (Blast_tac 1); 

382 
qed "range_of_prod"; 

536
5fbfa997f1b0
ZF/domrange/domain_of_prod, domain_empty, etc: moved to equalities.ML where
lcp
parents:
520
diff
changeset

383 

9180  384 
Goal "range(0) = 0"; 
385 
by (Blast_tac 1); 

386 
qed "range_0"; 

536
5fbfa997f1b0
ZF/domrange/domain_of_prod, domain_empty, etc: moved to equalities.ML where
lcp
parents:
520
diff
changeset

387 

9180  388 
Goal "range(cons(<a,b>,r)) = cons(b, range(r))"; 
389 
by (Blast_tac 1); 

390 
qed "range_cons"; 

536
5fbfa997f1b0
ZF/domrange/domain_of_prod, domain_empty, etc: moved to equalities.ML where
lcp
parents:
520
diff
changeset

391 

5321  392 
Goal "range(A Un B) = range(A) Un range(B)"; 
2877  393 
by (Blast_tac 1); 
760  394 
qed "range_Un_eq"; 
0  395 

5321  396 
Goal "range(A Int B) <= range(A) Int range(B)"; 
2877  397 
by (Blast_tac 1); 
760  398 
qed "range_Int_subset"; 
0  399 

5321  400 
Goal "range(A)  range(B) <= range(A  B)"; 
2877  401 
by (Blast_tac 1); 
1056  402 
qed "range_Diff_subset"; 
0  403 

5321  404 
Goal "range(converse(r)) = domain(r)"; 
2877  405 
by (Blast_tac 1); 
760  406 
qed "range_converse"; 
685  407 

2469  408 
Addsimps [range_0, range_cons, range_Un_eq, range_converse]; 
409 

410 

536
5fbfa997f1b0
ZF/domrange/domain_of_prod, domain_empty, etc: moved to equalities.ML where
lcp
parents:
520
diff
changeset

411 
(** Field **) 
5fbfa997f1b0
ZF/domrange/domain_of_prod, domain_empty, etc: moved to equalities.ML where
lcp
parents:
520
diff
changeset

412 

9180  413 
Goal "field(A*A) = A"; 
414 
by (Blast_tac 1); 

415 
qed "field_of_prod"; 

536
5fbfa997f1b0
ZF/domrange/domain_of_prod, domain_empty, etc: moved to equalities.ML where
lcp
parents:
520
diff
changeset

416 

9180  417 
Goal "field(0) = 0"; 
418 
by (Blast_tac 1); 

419 
qed "field_0"; 

536
5fbfa997f1b0
ZF/domrange/domain_of_prod, domain_empty, etc: moved to equalities.ML where
lcp
parents:
520
diff
changeset

420 

9180  421 
Goal "field(cons(<a,b>,r)) = cons(a, cons(b, field(r)))"; 
422 
by (rtac equalityI 1); 

423 
by (ALLGOALS Blast_tac) ; 

424 
qed "field_cons"; 

536
5fbfa997f1b0
ZF/domrange/domain_of_prod, domain_empty, etc: moved to equalities.ML where
lcp
parents:
520
diff
changeset

425 

5321  426 
Goal "field(A Un B) = field(A) Un field(B)"; 
2877  427 
by (Blast_tac 1); 
760  428 
qed "field_Un_eq"; 
0  429 

5321  430 
Goal "field(A Int B) <= field(A) Int field(B)"; 
2877  431 
by (Blast_tac 1); 
760  432 
qed "field_Int_subset"; 
0  433 

5321  434 
Goal "field(A)  field(B) <= field(A  B)"; 
2877  435 
by (Blast_tac 1); 
1056  436 
qed "field_Diff_subset"; 
0  437 

5321  438 
Goal "field(converse(r)) = field(r)"; 
2877  439 
by (Blast_tac 1); 
2469  440 
qed "field_converse"; 
441 

442 
Addsimps [field_0, field_cons, field_Un_eq, field_converse]; 

443 

0  444 

435  445 
(** Image **) 
446 

5321  447 
Goal "r``0 = 0"; 
2877  448 
by (Blast_tac 1); 
760  449 
qed "image_0"; 
435  450 

5321  451 
Goal "r``(A Un B) = (r``A) Un (r``B)"; 
2877  452 
by (Blast_tac 1); 
760  453 
qed "image_Un"; 
435  454 

5321  455 
Goal "r``(A Int B) <= (r``A) Int (r``B)"; 
2877  456 
by (Blast_tac 1); 
760  457 
qed "image_Int_subset"; 
435  458 

5321  459 
Goal "(r Int A*A)``B <= (r``B) Int A"; 
2877  460 
by (Blast_tac 1); 
760  461 
qed "image_Int_square_subset"; 
435  462 

5321  463 
Goal "B<=A ==> (r Int A*A)``B = (r``B) Int A"; 
2877  464 
by (Blast_tac 1); 
760  465 
qed "image_Int_square"; 
435  466 

2469  467 
Addsimps [image_0, image_Un]; 
468 

4840  469 
(*Image laws for special relations*) 
5321  470 
Goal "0``A = 0"; 
4840  471 
by (Blast_tac 1); 
472 
qed "image_0_left"; 

473 
Addsimps [image_0_left]; 

474 

5321  475 
Goal "(r Un s)``A = (r``A) Un (s``A)"; 
4840  476 
by (Blast_tac 1); 
477 
qed "image_Un_left"; 

478 

5321  479 
Goal "(r Int s)``A <= (r``A) Int (s``A)"; 
4840  480 
by (Blast_tac 1); 
481 
qed "image_Int_subset_left"; 

482 

435  483 

484 
(** Inverse Image **) 

485 

5321  486 
Goal "r``0 = 0"; 
2877  487 
by (Blast_tac 1); 
760  488 
qed "vimage_0"; 
435  489 

5321  490 
Goal "r``(A Un B) = (r``A) Un (r``B)"; 
2877  491 
by (Blast_tac 1); 
760  492 
qed "vimage_Un"; 
435  493 

5321  494 
Goal "r``(A Int B) <= (r``A) Int (r``B)"; 
2877  495 
by (Blast_tac 1); 
760  496 
qed "vimage_Int_subset"; 
435  497 

5321  498 
Goalw [function_def] "function(f) ==> f``(A Int B) = (f``A) Int (f``B)"; 
4660  499 
by (Blast_tac 1); 
500 
qed "function_vimage_Int"; 

501 

5321  502 
Goalw [function_def] "function(f) ==> f``(AB) = (f``A)  (f``B)"; 
4660  503 
by (Blast_tac 1); 
504 
qed "function_vimage_Diff"; 

505 

5321  506 
Goalw [function_def] "function(f) ==> f `` (f`` A) <= A"; 
507 
by (Blast_tac 1); 

508 
qed "function_image_vimage"; 

509 

510 
Goal "(r Int A*A)``B <= (r``B) Int A"; 

2877  511 
by (Blast_tac 1); 
760  512 
qed "vimage_Int_square_subset"; 
435  513 

5321  514 
Goal "B<=A ==> (r Int A*A)``B = (r``B) Int A"; 
2877  515 
by (Blast_tac 1); 
760  516 
qed "vimage_Int_square"; 
435  517 

2469  518 
Addsimps [vimage_0, vimage_Un]; 
519 

435  520 

4840  521 
(*Invese image laws for special relations*) 
5321  522 
Goal "0``A = 0"; 
4840  523 
by (Blast_tac 1); 
524 
qed "vimage_0_left"; 

525 
Addsimps [vimage_0_left]; 

526 

5321  527 
Goal "(r Un s)``A = (r``A) Un (s``A)"; 
4840  528 
by (Blast_tac 1); 
529 
qed "vimage_Un_left"; 

530 

5321  531 
Goal "(r Int s)``A <= (r``A) Int (s``A)"; 
4840  532 
by (Blast_tac 1); 
533 
qed "vimage_Int_subset_left"; 

534 

535 

0  536 
(** Converse **) 
537 

5321  538 
Goal "converse(A Un B) = converse(A) Un converse(B)"; 
2877  539 
by (Blast_tac 1); 
760  540 
qed "converse_Un"; 
0  541 

5321  542 
Goal "converse(A Int B) = converse(A) Int converse(B)"; 
2877  543 
by (Blast_tac 1); 
760  544 
qed "converse_Int"; 
0  545 

5321  546 
Goal "converse(A  B) = converse(A)  converse(B)"; 
2877  547 
by (Blast_tac 1); 
1056  548 
qed "converse_Diff"; 
0  549 

5321  550 
Goal "converse(UN x:A. B(x)) = (UN x:A. converse(B(x)))"; 
2877  551 
by (Blast_tac 1); 
787  552 
qed "converse_UN"; 
553 

1652  554 
(*Unfolding Inter avoids using excluded middle on A=0*) 
5325
f7a5e06adea1
Yet more removal of "goal" commands, especially "goal ZF.thy", so ZF.thy
paulson
parents:
5321
diff
changeset

555 
Goalw [Inter_def] "converse(INT x:A. B(x)) = (INT x:A. converse(B(x)))"; 
2877  556 
by (Blast_tac 1); 
1652  557 
qed "converse_INT"; 
558 

2469  559 
Addsimps [converse_Un, converse_Int, converse_Diff, converse_UN, converse_INT]; 
560 

198  561 
(** Pow **) 
562 

6288
694c9c1910e8
new theorems Pow_0 and Pow_insert; renamed other Pow theorems
paulson
parents:
6068
diff
changeset

563 
Goal "Pow(0) = {0}"; 
694c9c1910e8
new theorems Pow_0 and Pow_insert; renamed other Pow theorems
paulson
parents:
6068
diff
changeset

564 
by (Blast_tac 1); 
694c9c1910e8
new theorems Pow_0 and Pow_insert; renamed other Pow theorems
paulson
parents:
6068
diff
changeset

565 
qed "Pow_0"; 
694c9c1910e8
new theorems Pow_0 and Pow_insert; renamed other Pow theorems
paulson
parents:
6068
diff
changeset

566 

694c9c1910e8
new theorems Pow_0 and Pow_insert; renamed other Pow theorems
paulson
parents:
6068
diff
changeset

567 
Goal "Pow (cons(a,A)) = Pow(A) Un {cons(a,X) . X: Pow(A)}"; 
6298  568 
by (rtac equalityI 1); 
6288
694c9c1910e8
new theorems Pow_0 and Pow_insert; renamed other Pow theorems
paulson
parents:
6068
diff
changeset

569 
by Safe_tac; 
694c9c1910e8
new theorems Pow_0 and Pow_insert; renamed other Pow theorems
paulson
parents:
6068
diff
changeset

570 
by (etac swap 1); 
694c9c1910e8
new theorems Pow_0 and Pow_insert; renamed other Pow theorems
paulson
parents:
6068
diff
changeset

571 
by (res_inst_tac [("a", "x{a}")] RepFun_eqI 1); 
694c9c1910e8
new theorems Pow_0 and Pow_insert; renamed other Pow theorems
paulson
parents:
6068
diff
changeset

572 
by (ALLGOALS Blast_tac); 
694c9c1910e8
new theorems Pow_0 and Pow_insert; renamed other Pow theorems
paulson
parents:
6068
diff
changeset

573 
qed "Pow_insert"; 
694c9c1910e8
new theorems Pow_0 and Pow_insert; renamed other Pow theorems
paulson
parents:
6068
diff
changeset

574 

5321  575 
Goal "Pow(A) Un Pow(B) <= Pow(A Un B)"; 
2877  576 
by (Blast_tac 1); 
760  577 
qed "Un_Pow_subset"; 
198  578 

5321  579 
Goal "(UN x:A. Pow(B(x))) <= Pow(UN x:A. B(x))"; 
2877  580 
by (Blast_tac 1); 
760  581 
qed "UN_Pow_subset"; 
198  582 

5321  583 
Goal "A <= Pow(Union(A))"; 
2877  584 
by (Blast_tac 1); 
760  585 
qed "subset_Pow_Union"; 
198  586 

5321  587 
Goal "Union(Pow(A)) = A"; 
2877  588 
by (Blast_tac 1); 
760  589 
qed "Union_Pow_eq"; 
198  590 

5321  591 
Goal "Pow(A Int B) = Pow(A) Int Pow(B)"; 
2877  592 
by (Blast_tac 1); 
6288
694c9c1910e8
new theorems Pow_0 and Pow_insert; renamed other Pow theorems
paulson
parents:
6068
diff
changeset

593 
qed "Pow_Int_eq"; 
198  594 

6288
694c9c1910e8
new theorems Pow_0 and Pow_insert; renamed other Pow theorems
paulson
parents:
6068
diff
changeset

595 
Goal "x:A ==> Pow(INT x:A. B(x)) = (INT x:A. Pow(B(x)))"; 
2877  596 
by (Blast_tac 1); 
6288
694c9c1910e8
new theorems Pow_0 and Pow_insert; renamed other Pow theorems
paulson
parents:
6068
diff
changeset

597 
qed "Pow_INT_eq"; 
435  598 

6288
694c9c1910e8
new theorems Pow_0 and Pow_insert; renamed other Pow theorems
paulson
parents:
6068
diff
changeset

599 
Addsimps [Pow_0, Union_Pow_eq, Pow_Int_eq]; 
2469  600 

839  601 
(** RepFun **) 
602 

5321  603 
Goal "{f(x).x:A}=0 <> A=0"; 
9303  604 
by (Blast_tac 1); 
839  605 
qed "RepFun_eq_0_iff"; 
606 

1611  607 
(** Collect **) 
608 

5321  609 
Goal "Collect(A Un B, P) = Collect(A,P) Un Collect(B,P)"; 
2877  610 
by (Blast_tac 1); 
1611  611 
qed "Collect_Un"; 
612 

5321  613 
Goal "Collect(A Int B, P) = Collect(A,P) Int Collect(B,P)"; 
2877  614 
by (Blast_tac 1); 
1611  615 
qed "Collect_Int"; 
616 

5321  617 
Goal "Collect(A  B, P) = Collect(A,P)  Collect(B,P)"; 
2877  618 
by (Blast_tac 1); 
1611  619 
qed "Collect_Diff"; 
620 

6068  621 
Goal "{x:cons(a,B). P(x)} = \ 
622 
\ (if P(a) then cons(a, {x:B. P(x)}) else {x:B. P(x)})"; 

5116
8eb343ab5748
Renamed expand_if to split_if and setloop split_tac to addsplits,
paulson
parents:
5067
diff
changeset

623 
by (simp_tac (simpset() addsplits [split_if]) 1); 
2877  624 
by (Blast_tac 1); 
1611  625 
qed "Collect_cons"; 
626 