author  paulson 
Tue, 10 Feb 1998 10:27:30 +0100  
changeset 4615  67457d16cdbc 
parent 4609  b435c5a320b0 
child 4634  83d364462ce1 
permissions  rwrr 
1465  1 
(* Title: HOL/equalities 
923  2 
ID: $Id$ 
1465  3 
Author: Lawrence C Paulson, Cambridge University Computer Laboratory 
923  4 
Copyright 1994 University of Cambridge 
5 

6 
Equalities involving union, intersection, inclusion, etc. 

7 
*) 

8 

9 
writeln"File HOL/equalities"; 

10 

1754
852093aeb0ab
Replaced fast_tac by Fast_tac (which uses default claset)
berghofe
parents:
1748
diff
changeset

11 
AddSIs [equalityI]; 
852093aeb0ab
Replaced fast_tac by Fast_tac (which uses default claset)
berghofe
parents:
1748
diff
changeset

12 

1548  13 
section "{}"; 
14 

4059  15 
goal thy "{x. False} = {}"; 
2891  16 
by (Blast_tac 1); 
1531  17 
qed "Collect_False_empty"; 
18 
Addsimps [Collect_False_empty]; 

19 

4059  20 
goal thy "(A <= {}) = (A = {})"; 
2891  21 
by (Blast_tac 1); 
1531  22 
qed "subset_empty"; 
23 
Addsimps [subset_empty]; 

24 

3222
726a9b069947
Distributed Psubset stuff to basic set theory files, incl Finite.
nipkow
parents:
2922
diff
changeset

25 
goalw thy [psubset_def] "~ (A < {})"; 
726a9b069947
Distributed Psubset stuff to basic set theory files, incl Finite.
nipkow
parents:
2922
diff
changeset

26 
by (Blast_tac 1); 
726a9b069947
Distributed Psubset stuff to basic set theory files, incl Finite.
nipkow
parents:
2922
diff
changeset

27 
qed "not_psubset_empty"; 
726a9b069947
Distributed Psubset stuff to basic set theory files, incl Finite.
nipkow
parents:
2922
diff
changeset

28 
AddIffs [not_psubset_empty]; 
726a9b069947
Distributed Psubset stuff to basic set theory files, incl Finite.
nipkow
parents:
2922
diff
changeset

29 

1548  30 
section "insert"; 
923  31 

1531  32 
(*NOT SUITABLE FOR REWRITING since {a} == insert a {}*) 
4059  33 
goal thy "insert a A = {a} Un A"; 
2891  34 
by (Blast_tac 1); 
1531  35 
qed "insert_is_Un"; 
36 

4059  37 
goal thy "insert a A ~= {}"; 
4089  38 
by (blast_tac (claset() addEs [equalityCE]) 1); 
1179
7678408f9751
Added insert_not_empty, UN_empty and UN_insert (to set_ss).
nipkow
parents:
923
diff
changeset

39 
qed"insert_not_empty"; 
1531  40 
Addsimps[insert_not_empty]; 
1179
7678408f9751
Added insert_not_empty, UN_empty and UN_insert (to set_ss).
nipkow
parents:
923
diff
changeset

41 

7678408f9751
Added insert_not_empty, UN_empty and UN_insert (to set_ss).
nipkow
parents:
923
diff
changeset

42 
bind_thm("empty_not_insert",insert_not_empty RS not_sym); 
1531  43 
Addsimps[empty_not_insert]; 
1179
7678408f9751
Added insert_not_empty, UN_empty and UN_insert (to set_ss).
nipkow
parents:
923
diff
changeset

44 

4059  45 
goal thy "!!a. a:A ==> insert a A = A"; 
2891  46 
by (Blast_tac 1); 
923  47 
qed "insert_absorb"; 
4605  48 
(* Addsimps [insert_absorb] causes recursive (ie quadtratic) calls 
49 
in case of nested inserts! 

50 
*) 

923  51 

4059  52 
goal thy "insert x (insert x A) = insert x A"; 
2891  53 
by (Blast_tac 1); 
1531  54 
qed "insert_absorb2"; 
55 
Addsimps [insert_absorb2]; 

56 

4059  57 
goal thy "insert x (insert y A) = insert y (insert x A)"; 
2891  58 
by (Blast_tac 1); 
1879  59 
qed "insert_commute"; 
60 

4059  61 
goal thy "(insert x A <= B) = (x:B & A <= B)"; 
2891  62 
by (Blast_tac 1); 
923  63 
qed "insert_subset"; 
1531  64 
Addsimps[insert_subset]; 
65 

4059  66 
goal thy "!!a. insert a A ~= insert a B ==> A ~= B"; 
3222
726a9b069947
Distributed Psubset stuff to basic set theory files, incl Finite.
nipkow
parents:
2922
diff
changeset

67 
by (Blast_tac 1); 
726a9b069947
Distributed Psubset stuff to basic set theory files, incl Finite.
nipkow
parents:
2922
diff
changeset

68 
qed "insert_lim"; 
726a9b069947
Distributed Psubset stuff to basic set theory files, incl Finite.
nipkow
parents:
2922
diff
changeset

69 

1531  70 
(* use new B rather than (A{a}) to avoid infinite unfolding *) 
4059  71 
goal thy "!!a. a:A ==> ? B. A = insert a B & a ~: B"; 
1553  72 
by (res_inst_tac [("x","A{a}")] exI 1); 
2891  73 
by (Blast_tac 1); 
1531  74 
qed "mk_disjoint_insert"; 
923  75 

4059  76 
goal thy 
1843
a6d7aef48c2f
Removed the unused eq_cs, and added some distributive laws
paulson
parents:
1786
diff
changeset

77 
"!!A. A~={} ==> (UN x:A. insert a (B x)) = insert a (UN x:A. B x)"; 
2891  78 
by (Blast_tac 1); 
1843
a6d7aef48c2f
Removed the unused eq_cs, and added some distributive laws
paulson
parents:
1786
diff
changeset

79 
qed "UN_insert_distrib"; 
a6d7aef48c2f
Removed the unused eq_cs, and added some distributive laws
paulson
parents:
1786
diff
changeset

80 

1660  81 
section "``"; 
923  82 

4059  83 
goal thy "f``{} = {}"; 
2891  84 
by (Blast_tac 1); 
923  85 
qed "image_empty"; 
1531  86 
Addsimps[image_empty]; 
923  87 

4059  88 
goal thy "f``insert a B = insert (f a) (f``B)"; 
2891  89 
by (Blast_tac 1); 
923  90 
qed "image_insert"; 
1531  91 
Addsimps[image_insert]; 
923  92 

4059  93 
goal thy "(f `` (UNION A B)) = (UN x:A.(f `` (B x)))"; 
3222
726a9b069947
Distributed Psubset stuff to basic set theory files, incl Finite.
nipkow
parents:
2922
diff
changeset

94 
by (Blast_tac 1); 
726a9b069947
Distributed Psubset stuff to basic set theory files, incl Finite.
nipkow
parents:
2922
diff
changeset

95 
qed "image_UNION"; 
726a9b069947
Distributed Psubset stuff to basic set theory files, incl Finite.
nipkow
parents:
2922
diff
changeset

96 

4059  97 
goal thy "(%x. x) `` Y = Y"; 
3222
726a9b069947
Distributed Psubset stuff to basic set theory files, incl Finite.
nipkow
parents:
2922
diff
changeset

98 
by (Blast_tac 1); 
726a9b069947
Distributed Psubset stuff to basic set theory files, incl Finite.
nipkow
parents:
2922
diff
changeset

99 
qed "image_id"; 
726a9b069947
Distributed Psubset stuff to basic set theory files, incl Finite.
nipkow
parents:
2922
diff
changeset

100 

4059  101 
goal thy "f``(g``A) = (%x. f (g x)) `` A"; 
3457  102 
by (Blast_tac 1); 
4059  103 
qed "image_image"; 
3222
726a9b069947
Distributed Psubset stuff to basic set theory files, incl Finite.
nipkow
parents:
2922
diff
changeset

104 

4059  105 
goal thy "!!x. x:A ==> insert (f x) (f``A) = f``A"; 
2891  106 
by (Blast_tac 1); 
1884  107 
qed "insert_image"; 
108 
Addsimps [insert_image]; 

109 

4059  110 
goal thy "(f``A = {}) = (A = {})"; 
4306
ddbe1a9722ab
Tidying and using equalityCE instead of the slower equalityE
paulson
parents:
4231
diff
changeset

111 
by (blast_tac (claset() addSEs [equalityCE]) 1); 
3415
c068bd2f0bbd
Moved image_is_empty from Finite.ML to equalities.ML
nipkow
parents:
3384
diff
changeset

112 
qed "image_is_empty"; 
c068bd2f0bbd
Moved image_is_empty from Finite.ML to equalities.ML
nipkow
parents:
3384
diff
changeset

113 
AddIffs [image_is_empty]; 
c068bd2f0bbd
Moved image_is_empty from Finite.ML to equalities.ML
nipkow
parents:
3384
diff
changeset

114 

4059  115 
goalw thy [image_def] 
1763  116 
"(%x. if P x then f x else g x) `` S \ 
4200  117 
\ = (f `` (S Int {x. P x})) Un (g `` (S Int {x. ~(P x)}))"; 
2031  118 
by (split_tac [expand_if] 1); 
2891  119 
by (Blast_tac 1); 
1748  120 
qed "if_image_distrib"; 
121 
Addsimps[if_image_distrib]; 

122 

4136  123 
val prems= goal thy "[M = N; !!x. x:N ==> f x = g x] ==> f``M = g``N"; 
124 
by (rtac set_ext 1); 

125 
by (simp_tac (simpset() addsimps image_def::prems) 1); 

126 
qed "image_cong"; 

127 

1748  128 

1548  129 
section "Int"; 
923  130 

4059  131 
goal thy "A Int A = A"; 
2891  132 
by (Blast_tac 1); 
923  133 
qed "Int_absorb"; 
1531  134 
Addsimps[Int_absorb]; 
923  135 

4609  136 
goal thy " A Int (A Int B) = A Int B"; 
137 
by (Blast_tac 1); 

138 
qed "Int_left_absorb"; 

139 

4059  140 
goal thy "A Int B = B Int A"; 
2891  141 
by (Blast_tac 1); 
923  142 
qed "Int_commute"; 
143 

4609  144 
goal thy "A Int (B Int C) = B Int (A Int C)"; 
145 
by (Blast_tac 1); 

146 
qed "Int_left_commute"; 

147 

4059  148 
goal thy "(A Int B) Int C = A Int (B Int C)"; 
2891  149 
by (Blast_tac 1); 
923  150 
qed "Int_assoc"; 
151 

4609  152 
(*Intersection is an ACoperator*) 
153 
val Int_ac = [Int_assoc, Int_left_absorb, Int_commute, Int_left_commute]; 

154 

4059  155 
goal thy "{} Int B = {}"; 
2891  156 
by (Blast_tac 1); 
923  157 
qed "Int_empty_left"; 
1531  158 
Addsimps[Int_empty_left]; 
923  159 

4059  160 
goal thy "A Int {} = {}"; 
2891  161 
by (Blast_tac 1); 
923  162 
qed "Int_empty_right"; 
1531  163 
Addsimps[Int_empty_right]; 
164 

4059  165 
goal thy "(A Int B = {}) = (A <= Compl B)"; 
4306
ddbe1a9722ab
Tidying and using equalityCE instead of the slower equalityE
paulson
parents:
4231
diff
changeset

166 
by (blast_tac (claset() addSEs [equalityCE]) 1); 
3356  167 
qed "disjoint_eq_subset_Compl"; 
168 

4059  169 
goal thy "UNIV Int B = B"; 
2891  170 
by (Blast_tac 1); 
1531  171 
qed "Int_UNIV_left"; 
172 
Addsimps[Int_UNIV_left]; 

173 

4059  174 
goal thy "A Int UNIV = A"; 
2891  175 
by (Blast_tac 1); 
1531  176 
qed "Int_UNIV_right"; 
177 
Addsimps[Int_UNIV_right]; 

923  178 

4059  179 
goal thy "A Int (B Un C) = (A Int B) Un (A Int C)"; 
2891  180 
by (Blast_tac 1); 
923  181 
qed "Int_Un_distrib"; 
182 

4059  183 
goal thy "(B Un C) Int A = (B Int A) Un (C Int A)"; 
2891  184 
by (Blast_tac 1); 
1618  185 
qed "Int_Un_distrib2"; 
186 

4059  187 
goal thy "(A<=B) = (A Int B = A)"; 
4306
ddbe1a9722ab
Tidying and using equalityCE instead of the slower equalityE
paulson
parents:
4231
diff
changeset

188 
by (blast_tac (claset() addSEs [equalityCE]) 1); 
923  189 
qed "subset_Int_eq"; 
190 

4059  191 
goal thy "(A Int B = UNIV) = (A = UNIV & B = UNIV)"; 
4089  192 
by (blast_tac (claset() addEs [equalityCE]) 1); 
1531  193 
qed "Int_UNIV"; 
194 
Addsimps[Int_UNIV]; 

195 

1548  196 
section "Un"; 
923  197 

4059  198 
goal thy "A Un A = A"; 
2891  199 
by (Blast_tac 1); 
923  200 
qed "Un_absorb"; 
1531  201 
Addsimps[Un_absorb]; 
923  202 

4059  203 
goal thy " A Un (A Un B) = A Un B"; 
3222
726a9b069947
Distributed Psubset stuff to basic set theory files, incl Finite.
nipkow
parents:
2922
diff
changeset

204 
by (Blast_tac 1); 
726a9b069947
Distributed Psubset stuff to basic set theory files, incl Finite.
nipkow
parents:
2922
diff
changeset

205 
qed "Un_left_absorb"; 
726a9b069947
Distributed Psubset stuff to basic set theory files, incl Finite.
nipkow
parents:
2922
diff
changeset

206 

4059  207 
goal thy "A Un B = B Un A"; 
2891  208 
by (Blast_tac 1); 
923  209 
qed "Un_commute"; 
210 

4609  211 
goal thy "A Un (B Un C) = B Un (A Un C)"; 
3222
726a9b069947
Distributed Psubset stuff to basic set theory files, incl Finite.
nipkow
parents:
2922
diff
changeset

212 
by (Blast_tac 1); 
726a9b069947
Distributed Psubset stuff to basic set theory files, incl Finite.
nipkow
parents:
2922
diff
changeset

213 
qed "Un_left_commute"; 
726a9b069947
Distributed Psubset stuff to basic set theory files, incl Finite.
nipkow
parents:
2922
diff
changeset

214 

4059  215 
goal thy "(A Un B) Un C = A Un (B Un C)"; 
2891  216 
by (Blast_tac 1); 
923  217 
qed "Un_assoc"; 
218 

4609  219 
(*Union is an ACoperator*) 
220 
val Un_ac = [Un_assoc, Un_left_absorb, Un_commute, Un_left_commute]; 

221 

4059  222 
goal thy "{} Un B = B"; 
2891  223 
by (Blast_tac 1); 
923  224 
qed "Un_empty_left"; 
1531  225 
Addsimps[Un_empty_left]; 
923  226 

4059  227 
goal thy "A Un {} = A"; 
2891  228 
by (Blast_tac 1); 
923  229 
qed "Un_empty_right"; 
1531  230 
Addsimps[Un_empty_right]; 
231 

4059  232 
goal thy "UNIV Un B = UNIV"; 
2891  233 
by (Blast_tac 1); 
1531  234 
qed "Un_UNIV_left"; 
235 
Addsimps[Un_UNIV_left]; 

236 

4059  237 
goal thy "A Un UNIV = UNIV"; 
2891  238 
by (Blast_tac 1); 
1531  239 
qed "Un_UNIV_right"; 
240 
Addsimps[Un_UNIV_right]; 

923  241 

4059  242 
goal thy "(insert a B) Un C = insert a (B Un C)"; 
2891  243 
by (Blast_tac 1); 
923  244 
qed "Un_insert_left"; 
3384
5ef99c94e1fb
Now Un_insert_left, Un_insert_right are default rewrite rules
paulson
parents:
3356
diff
changeset

245 
Addsimps[Un_insert_left]; 
923  246 

4059  247 
goal thy "A Un (insert a B) = insert a (A Un B)"; 
2891  248 
by (Blast_tac 1); 
1917  249 
qed "Un_insert_right"; 
3384
5ef99c94e1fb
Now Un_insert_left, Un_insert_right are default rewrite rules
paulson
parents:
3356
diff
changeset

250 
Addsimps[Un_insert_right]; 
1917  251 

4059  252 
goal thy "(insert a B) Int C = (if a:C then insert a (B Int C) \ 
4306
ddbe1a9722ab
Tidying and using equalityCE instead of the slower equalityE
paulson
parents:
4231
diff
changeset

253 
\ else B Int C)"; 
4089  254 
by (simp_tac (simpset() addsplits [expand_if]) 1); 
3356  255 
by (Blast_tac 1); 
256 
qed "Int_insert_left"; 

257 

4059  258 
goal thy "A Int (insert a B) = (if a:A then insert a (A Int B) \ 
4306
ddbe1a9722ab
Tidying and using equalityCE instead of the slower equalityE
paulson
parents:
4231
diff
changeset

259 
\ else A Int B)"; 
4089  260 
by (simp_tac (simpset() addsplits [expand_if]) 1); 
3356  261 
by (Blast_tac 1); 
262 
qed "Int_insert_right"; 

263 

4609  264 
goal thy "A Un (B Int C) = (A Un B) Int (A Un C)"; 
2891  265 
by (Blast_tac 1); 
923  266 
qed "Un_Int_distrib"; 
267 

4609  268 
goal thy "(B Int C) Un A = (B Un A) Int (C Un A)"; 
269 
by (Blast_tac 1); 

270 
qed "Un_Int_distrib2"; 

271 

4059  272 
goal thy 
923  273 
"(A Int B) Un (B Int C) Un (C Int A) = (A Un B) Int (B Un C) Int (C Un A)"; 
2891  274 
by (Blast_tac 1); 
923  275 
qed "Un_Int_crazy"; 
276 

4059  277 
goal thy "(A<=B) = (A Un B = B)"; 
4306
ddbe1a9722ab
Tidying and using equalityCE instead of the slower equalityE
paulson
parents:
4231
diff
changeset

278 
by (blast_tac (claset() addSEs [equalityCE]) 1); 
923  279 
qed "subset_Un_eq"; 
280 

4059  281 
goal thy "(A <= insert b C) = (A <= C  b:A & A{b} <= C)"; 
2891  282 
by (Blast_tac 1); 
923  283 
qed "subset_insert_iff"; 
284 

4059  285 
goal thy "(A Un B = {}) = (A = {} & B = {})"; 
4089  286 
by (blast_tac (claset() addEs [equalityCE]) 1); 
923  287 
qed "Un_empty"; 
1531  288 
Addsimps[Un_empty]; 
923  289 

1548  290 
section "Compl"; 
923  291 

4059  292 
goal thy "A Int Compl(A) = {}"; 
2891  293 
by (Blast_tac 1); 
923  294 
qed "Compl_disjoint"; 
1531  295 
Addsimps[Compl_disjoint]; 
923  296 

4059  297 
goal thy "A Un Compl(A) = UNIV"; 
2891  298 
by (Blast_tac 1); 
923  299 
qed "Compl_partition"; 
300 

4059  301 
goal thy "Compl(Compl(A)) = A"; 
2891  302 
by (Blast_tac 1); 
923  303 
qed "double_complement"; 
1531  304 
Addsimps[double_complement]; 
923  305 

4059  306 
goal thy "Compl(A Un B) = Compl(A) Int Compl(B)"; 
2891  307 
by (Blast_tac 1); 
923  308 
qed "Compl_Un"; 
309 

4059  310 
goal thy "Compl(A Int B) = Compl(A) Un Compl(B)"; 
2891  311 
by (Blast_tac 1); 
923  312 
qed "Compl_Int"; 
313 

4059  314 
goal thy "Compl(UN x:A. B(x)) = (INT x:A. Compl(B(x)))"; 
2891  315 
by (Blast_tac 1); 
923  316 
qed "Compl_UN"; 
317 

4059  318 
goal thy "Compl(INT x:A. B(x)) = (UN x:A. Compl(B(x)))"; 
2891  319 
by (Blast_tac 1); 
923  320 
qed "Compl_INT"; 
321 

4615  322 
Addsimps [Compl_Un, Compl_Int, Compl_UN, Compl_INT]; 
323 

923  324 
(*Halmos, Naive Set Theory, page 16.*) 
325 

4059  326 
goal thy "((A Int B) Un C = A Int (B Un C)) = (C<=A)"; 
4306
ddbe1a9722ab
Tidying and using equalityCE instead of the slower equalityE
paulson
parents:
4231
diff
changeset

327 
by (blast_tac (claset() addSEs [equalityCE]) 1); 
923  328 
qed "Un_Int_assoc_eq"; 
329 

330 

1548  331 
section "Union"; 
923  332 

4059  333 
goal thy "Union({}) = {}"; 
2891  334 
by (Blast_tac 1); 
923  335 
qed "Union_empty"; 
1531  336 
Addsimps[Union_empty]; 
337 

4059  338 
goal thy "Union(UNIV) = UNIV"; 
2891  339 
by (Blast_tac 1); 
1531  340 
qed "Union_UNIV"; 
341 
Addsimps[Union_UNIV]; 

923  342 

4059  343 
goal thy "Union(insert a B) = a Un Union(B)"; 
2891  344 
by (Blast_tac 1); 
923  345 
qed "Union_insert"; 
1531  346 
Addsimps[Union_insert]; 
923  347 

4059  348 
goal thy "Union(A Un B) = Union(A) Un Union(B)"; 
2891  349 
by (Blast_tac 1); 
923  350 
qed "Union_Un_distrib"; 
1531  351 
Addsimps[Union_Un_distrib]; 
923  352 

4059  353 
goal thy "Union(A Int B) <= Union(A) Int Union(B)"; 
2891  354 
by (Blast_tac 1); 
923  355 
qed "Union_Int_subset"; 
356 

4059  357 
goal thy "(Union M = {}) = (! A : M. A = {})"; 
4306
ddbe1a9722ab
Tidying and using equalityCE instead of the slower equalityE
paulson
parents:
4231
diff
changeset

358 
by (blast_tac (claset() addEs [equalityCE]) 1); 
ddbe1a9722ab
Tidying and using equalityCE instead of the slower equalityE
paulson
parents:
4231
diff
changeset

359 
qed "Union_empty_conv"; 
4003  360 
AddIffs [Union_empty_conv]; 
361 

4159
4aff9b7e5597
UNIV now a constant; UNION1, INTER1 now translations and no longer have
paulson
parents:
4136
diff
changeset

362 
goal thy "(Union(C) Int A = {}) = (! B:C. B Int A = {})"; 
4306
ddbe1a9722ab
Tidying and using equalityCE instead of the slower equalityE
paulson
parents:
4231
diff
changeset

363 
by (blast_tac (claset() addSEs [equalityCE]) 1); 
923  364 
qed "Union_disjoint"; 
365 

1548  366 
section "Inter"; 
367 

4059  368 
goal thy "Inter({}) = UNIV"; 
2891  369 
by (Blast_tac 1); 
1531  370 
qed "Inter_empty"; 
371 
Addsimps[Inter_empty]; 

372 

4059  373 
goal thy "Inter(UNIV) = {}"; 
2891  374 
by (Blast_tac 1); 
1531  375 
qed "Inter_UNIV"; 
376 
Addsimps[Inter_UNIV]; 

377 

4059  378 
goal thy "Inter(insert a B) = a Int Inter(B)"; 
2891  379 
by (Blast_tac 1); 
1531  380 
qed "Inter_insert"; 
381 
Addsimps[Inter_insert]; 

382 

4059  383 
goal thy "Inter(A) Un Inter(B) <= Inter(A Int B)"; 
2891  384 
by (Blast_tac 1); 
1564
822575c737bd
Deleted faulty comment; proved new rule Inter_Un_subset
paulson
parents:
1553
diff
changeset

385 
qed "Inter_Un_subset"; 
1531  386 

4059  387 
goal thy "Inter(A Un B) = Inter(A) Int Inter(B)"; 
2891  388 
by (Blast_tac 1); 
923  389 
qed "Inter_Un_distrib"; 
390 

1548  391 
section "UN and INT"; 
923  392 

393 
(*Basic identities*) 

394 

4200  395 
val not_empty = prove_goal Set.thy "(A ~= {}) = (? x. x:A)" (K [Blast_tac 1]); 
4136  396 
(*Addsimps[not_empty];*) 
397 

4059  398 
goal thy "(UN x:{}. B x) = {}"; 
2891  399 
by (Blast_tac 1); 
1179
7678408f9751
Added insert_not_empty, UN_empty and UN_insert (to set_ss).
nipkow
parents:
923
diff
changeset

400 
qed "UN_empty"; 
1531  401 
Addsimps[UN_empty]; 
402 

4059  403 
goal thy "(UN x:A. {}) = {}"; 
3457  404 
by (Blast_tac 1); 
3222
726a9b069947
Distributed Psubset stuff to basic set theory files, incl Finite.
nipkow
parents:
2922
diff
changeset

405 
qed "UN_empty2"; 
726a9b069947
Distributed Psubset stuff to basic set theory files, incl Finite.
nipkow
parents:
2922
diff
changeset

406 
Addsimps[UN_empty2]; 
726a9b069947
Distributed Psubset stuff to basic set theory files, incl Finite.
nipkow
parents:
2922
diff
changeset

407 

4059  408 
goal thy "(INT x:{}. B x) = UNIV"; 
2891  409 
by (Blast_tac 1); 
1531  410 
qed "INT_empty"; 
411 
Addsimps[INT_empty]; 

412 

4059  413 
goal thy "(UN x:insert a A. B x) = B a Un UNION A B"; 
2891  414 
by (Blast_tac 1); 
1179
7678408f9751
Added insert_not_empty, UN_empty and UN_insert (to set_ss).
nipkow
parents:
923
diff
changeset

415 
qed "UN_insert"; 
1531  416 
Addsimps[UN_insert]; 
417 

4059  418 
goal thy "(UN i: A Un B. M i) = ((UN i: A. M i) Un (UN i:B. M i))"; 
3222
726a9b069947
Distributed Psubset stuff to basic set theory files, incl Finite.
nipkow
parents:
2922
diff
changeset

419 
by (Blast_tac 1); 
726a9b069947
Distributed Psubset stuff to basic set theory files, incl Finite.
nipkow
parents:
2922
diff
changeset

420 
qed "UN_Un"; 
726a9b069947
Distributed Psubset stuff to basic set theory files, incl Finite.
nipkow
parents:
2922
diff
changeset

421 

4059  422 
goal thy "(INT x:insert a A. B x) = B a Int INTER A B"; 
2891  423 
by (Blast_tac 1); 
1531  424 
qed "INT_insert"; 
425 
Addsimps[INT_insert]; 

1179
7678408f9751
Added insert_not_empty, UN_empty and UN_insert (to set_ss).
nipkow
parents:
923
diff
changeset

426 

4059  427 
goal thy 
2021  428 
"!!A. A~={} ==> (INT x:A. insert a (B x)) = insert a (INT x:A. B x)"; 
2891  429 
by (Blast_tac 1); 
2021  430 
qed "INT_insert_distrib"; 
431 

4059  432 
goal thy "Union(B``A) = (UN x:A. B(x))"; 
2891  433 
by (Blast_tac 1); 
923  434 
qed "Union_image_eq"; 
435 

4059  436 
goal thy "Inter(B``A) = (INT x:A. B(x))"; 
2891  437 
by (Blast_tac 1); 
923  438 
qed "Inter_image_eq"; 
439 

4159
4aff9b7e5597
UNIV now a constant; UNION1, INTER1 now translations and no longer have
paulson
parents:
4136
diff
changeset

440 
goal thy "!!A. A~={} ==> (UN y:A. c) = c"; 
2891  441 
by (Blast_tac 1); 
923  442 
qed "UN_constant"; 
4159
4aff9b7e5597
UNIV now a constant; UNION1, INTER1 now translations and no longer have
paulson
parents:
4136
diff
changeset

443 
Addsimps[UN_constant]; 
923  444 

4159
4aff9b7e5597
UNIV now a constant; UNION1, INTER1 now translations and no longer have
paulson
parents:
4136
diff
changeset

445 
goal thy "!!A. A~={} ==> (INT y:A. c) = c"; 
2891  446 
by (Blast_tac 1); 
923  447 
qed "INT_constant"; 
4159
4aff9b7e5597
UNIV now a constant; UNION1, INTER1 now translations and no longer have
paulson
parents:
4136
diff
changeset

448 
Addsimps[INT_constant]; 
923  449 

4059  450 
goal thy "(UN x:A. B(x)) = Union({Y. ? x:A. Y=B(x)})"; 
2891  451 
by (Blast_tac 1); 
923  452 
qed "UN_eq"; 
453 

454 
(*Look: it has an EXISTENTIAL quantifier*) 

4059  455 
goal thy "(INT x:A. B(x)) = Inter({Y. ? x:A. Y=B(x)})"; 
2891  456 
by (Blast_tac 1); 
923  457 
qed "INT_eq"; 
458 

4059  459 
goalw thy [o_def] "UNION A (g o f) = UNION (f``A) g"; 
3222
726a9b069947
Distributed Psubset stuff to basic set theory files, incl Finite.
nipkow
parents:
2922
diff
changeset

460 
by (Blast_tac 1); 
726a9b069947
Distributed Psubset stuff to basic set theory files, incl Finite.
nipkow
parents:
2922
diff
changeset

461 
qed "UNION_o"; 
726a9b069947
Distributed Psubset stuff to basic set theory files, incl Finite.
nipkow
parents:
2922
diff
changeset

462 

726a9b069947
Distributed Psubset stuff to basic set theory files, incl Finite.
nipkow
parents:
2922
diff
changeset

463 

923  464 
(*Distributive laws...*) 
465 

4059  466 
goal thy "A Int Union(B) = (UN C:B. A Int C)"; 
2891  467 
by (Blast_tac 1); 
923  468 
qed "Int_Union"; 
469 

4306
ddbe1a9722ab
Tidying and using equalityCE instead of the slower equalityE
paulson
parents:
4231
diff
changeset

470 
(* Devlin, Fundamentals of Contemporary Set Theory, page 12, exercise 5: 
923  471 
Union of a family of unions **) 
4059  472 
goal thy "(UN x:C. A(x) Un B(x)) = Union(A``C) Un Union(B``C)"; 
2891  473 
by (Blast_tac 1); 
923  474 
qed "Un_Union_image"; 
475 

476 
(*Equivalent version*) 

4059  477 
goal thy "(UN i:I. A(i) Un B(i)) = (UN i:I. A(i)) Un (UN i:I. B(i))"; 
2891  478 
by (Blast_tac 1); 
923  479 
qed "UN_Un_distrib"; 
480 

4059  481 
goal thy "A Un Inter(B) = (INT C:B. A Un C)"; 
2891  482 
by (Blast_tac 1); 
923  483 
qed "Un_Inter"; 
484 

4059  485 
goal thy "(INT x:C. A(x) Int B(x)) = Inter(A``C) Int Inter(B``C)"; 
2891  486 
by (Blast_tac 1); 
923  487 
qed "Int_Inter_image"; 
488 

489 
(*Equivalent version*) 

4059  490 
goal thy "(INT i:I. A(i) Int B(i)) = (INT i:I. A(i)) Int (INT i:I. B(i))"; 
2891  491 
by (Blast_tac 1); 
923  492 
qed "INT_Int_distrib"; 
493 

494 
(*Halmos, Naive Set Theory, page 35.*) 

4059  495 
goal thy "B Int (UN i:I. A(i)) = (UN i:I. B Int A(i))"; 
2891  496 
by (Blast_tac 1); 
923  497 
qed "Int_UN_distrib"; 
498 

4059  499 
goal thy "B Un (INT i:I. A(i)) = (INT i:I. B Un A(i))"; 
2891  500 
by (Blast_tac 1); 
923  501 
qed "Un_INT_distrib"; 
502 

4059  503 
goal thy 
923  504 
"(UN i:I. A(i)) Int (UN j:J. B(j)) = (UN i:I. UN j:J. A(i) Int B(j))"; 
2891  505 
by (Blast_tac 1); 
923  506 
qed "Int_UN_distrib2"; 
507 

4059  508 
goal thy 
923  509 
"(INT i:I. A(i)) Un (INT j:J. B(j)) = (INT i:I. INT j:J. A(i) Un B(j))"; 
2891  510 
by (Blast_tac 1); 
923  511 
qed "Un_INT_distrib2"; 
512 

2512  513 

514 
section"Bounded quantifiers"; 

515 

3860  516 
(** The following are not added to the default simpset because 
517 
(a) they duplicate the body and (b) there are no similar rules for Int. **) 

2512  518 

4059  519 
goal thy "(ALL x:A Un B. P x) = ((ALL x:A. P x) & (ALL x:B. P x))"; 
2891  520 
by (Blast_tac 1); 
2519  521 
qed "ball_Un"; 
522 

4059  523 
goal thy "(EX x:A Un B. P x) = ((EX x:A. P x)  (EX x:B. P x))"; 
2891  524 
by (Blast_tac 1); 
2519  525 
qed "bex_Un"; 
2512  526 

527 

1548  528 
section ""; 
923  529 

4609  530 
goal thy "AB = A Int Compl B"; 
531 
by (Blast_tac 1); 

532 
qed "Diff_eq_Int_Compl"; 

533 

4059  534 
goal thy "AA = {}"; 
2891  535 
by (Blast_tac 1); 
923  536 
qed "Diff_cancel"; 
1531  537 
Addsimps[Diff_cancel]; 
923  538 

4059  539 
goal thy "{}A = {}"; 
2891  540 
by (Blast_tac 1); 
923  541 
qed "empty_Diff"; 
1531  542 
Addsimps[empty_Diff]; 
923  543 

4059  544 
goal thy "A{} = A"; 
2891  545 
by (Blast_tac 1); 
923  546 
qed "Diff_empty"; 
1531  547 
Addsimps[Diff_empty]; 
548 

4059  549 
goal thy "AUNIV = {}"; 
2891  550 
by (Blast_tac 1); 
1531  551 
qed "Diff_UNIV"; 
552 
Addsimps[Diff_UNIV]; 

553 

4059  554 
goal thy "!!x. x~:A ==> A  insert x B = AB"; 
2891  555 
by (Blast_tac 1); 
1531  556 
qed "Diff_insert0"; 
557 
Addsimps [Diff_insert0]; 

923  558 

559 
(*NOT SUITABLE FOR REWRITING since {a} == insert a 0*) 

4059  560 
goal thy "A  insert a B = A  B  {a}"; 
2891  561 
by (Blast_tac 1); 
923  562 
qed "Diff_insert"; 
563 

564 
(*NOT SUITABLE FOR REWRITING since {a} == insert a 0*) 

4059  565 
goal thy "A  insert a B = A  {a}  B"; 
2891  566 
by (Blast_tac 1); 
923  567 
qed "Diff_insert2"; 
568 

4059  569 
goal thy "insert x A  B = (if x:B then AB else insert x (AB))"; 
4089  570 
by (simp_tac (simpset() addsplits [expand_if]) 1); 
2891  571 
by (Blast_tac 1); 
1531  572 
qed "insert_Diff_if"; 
573 

4059  574 
goal thy "!!x. x:B ==> insert x A  B = AB"; 
2891  575 
by (Blast_tac 1); 
1531  576 
qed "insert_Diff1"; 
577 
Addsimps [insert_Diff1]; 

578 

4059  579 
goal thy "!!a. a:A ==> insert a (A{a}) = A"; 
2922  580 
by (Blast_tac 1); 
923  581 
qed "insert_Diff"; 
582 

4059  583 
goal thy "A Int (BA) = {}"; 
2891  584 
by (Blast_tac 1); 
923  585 
qed "Diff_disjoint"; 
1531  586 
Addsimps[Diff_disjoint]; 
923  587 

4059  588 
goal thy "!!A. A<=B ==> A Un (BA) = B"; 
2891  589 
by (Blast_tac 1); 
923  590 
qed "Diff_partition"; 
591 

4059  592 
goal thy "!!A. [ A<=B; B<= C ] ==> (B  (C  A)) = (A :: 'a set)"; 
2891  593 
by (Blast_tac 1); 
923  594 
qed "double_diff"; 
595 

4059  596 
goal thy "A  (B Un C) = (AB) Int (AC)"; 
2891  597 
by (Blast_tac 1); 
923  598 
qed "Diff_Un"; 
599 

4059  600 
goal thy "A  (B Int C) = (AB) Un (AC)"; 
2891  601 
by (Blast_tac 1); 
923  602 
qed "Diff_Int"; 
603 

4059  604 
goal thy "(A Un B)  C = (A  C) Un (B  C)"; 
3222
726a9b069947
Distributed Psubset stuff to basic set theory files, incl Finite.
nipkow
parents:
2922
diff
changeset

605 
by (Blast_tac 1); 
726a9b069947
Distributed Psubset stuff to basic set theory files, incl Finite.
nipkow
parents:
2922
diff
changeset

606 
qed "Un_Diff"; 
726a9b069947
Distributed Psubset stuff to basic set theory files, incl Finite.
nipkow
parents:
2922
diff
changeset

607 

4059  608 
goal thy "(A Int B)  C = (A  C) Int (B  C)"; 
3222
726a9b069947
Distributed Psubset stuff to basic set theory files, incl Finite.
nipkow
parents:
2922
diff
changeset

609 
by (Blast_tac 1); 
726a9b069947
Distributed Psubset stuff to basic set theory files, incl Finite.
nipkow
parents:
2922
diff
changeset

610 
qed "Int_Diff"; 
726a9b069947
Distributed Psubset stuff to basic set theory files, incl Finite.
nipkow
parents:
2922
diff
changeset

611 

726a9b069947
Distributed Psubset stuff to basic set theory files, incl Finite.
nipkow
parents:
2922
diff
changeset

612 

726a9b069947
Distributed Psubset stuff to basic set theory files, incl Finite.
nipkow
parents:
2922
diff
changeset

613 
section "Miscellany"; 
726a9b069947
Distributed Psubset stuff to basic set theory files, incl Finite.
nipkow
parents:
2922
diff
changeset

614 

4059  615 
goal thy "(A = B) = ((A <= (B::'a set)) & (B<=A))"; 
3222
726a9b069947
Distributed Psubset stuff to basic set theory files, incl Finite.
nipkow
parents:
2922
diff
changeset

616 
by (Blast_tac 1); 
726a9b069947
Distributed Psubset stuff to basic set theory files, incl Finite.
nipkow
parents:
2922
diff
changeset

617 
qed "set_eq_subset"; 
726a9b069947
Distributed Psubset stuff to basic set theory files, incl Finite.
nipkow
parents:
2922
diff
changeset

618 

4059  619 
goal thy "A <= B = (! t. t:A > t:B)"; 
3222
726a9b069947
Distributed Psubset stuff to basic set theory files, incl Finite.
nipkow
parents:
2922
diff
changeset

620 
by (Blast_tac 1); 
726a9b069947
Distributed Psubset stuff to basic set theory files, incl Finite.
nipkow
parents:
2922
diff
changeset

621 
qed "subset_iff"; 
726a9b069947
Distributed Psubset stuff to basic set theory files, incl Finite.
nipkow
parents:
2922
diff
changeset

622 

726a9b069947
Distributed Psubset stuff to basic set theory files, incl Finite.
nipkow
parents:
2922
diff
changeset

623 
goalw thy [psubset_def] "((A::'a set) <= B) = ((A < B)  (A=B))"; 
726a9b069947
Distributed Psubset stuff to basic set theory files, incl Finite.
nipkow
parents:
2922
diff
changeset

624 
by (Blast_tac 1); 
726a9b069947
Distributed Psubset stuff to basic set theory files, incl Finite.
nipkow
parents:
2922
diff
changeset

625 
qed "subset_iff_psubset_eq"; 
2021  626 

4059  627 
goal thy "(!x. x ~: A) = (A={})"; 
4423  628 
by (Blast_tac 1); 
3896
ee8ebb74ec00
Various new lemmas. Improved conversion of equations to rewrite rules:
nipkow
parents:
3860
diff
changeset

629 
qed "all_not_in_conv"; 
3907  630 
AddIffs [all_not_in_conv]; 
3896
ee8ebb74ec00
Various new lemmas. Improved conversion of equations to rewrite rules:
nipkow
parents:
3860
diff
changeset

631 

4059  632 
goalw thy [Pow_def] "Pow {} = {{}}"; 
4477
b3e5857d8d99
New Auto_tac (by Oheimb), and new syntax (without parens), and expandshort
paulson
parents:
4423
diff
changeset

633 
by Auto_tac; 
3348
3f9a806f061e
Two useful facts about Powersets suggested by Florian Kammueller
paulson
parents:
3222
diff
changeset

634 
qed "Pow_empty"; 
3f9a806f061e
Two useful facts about Powersets suggested by Florian Kammueller
paulson
parents:
3222
diff
changeset

635 
Addsimps [Pow_empty]; 
3f9a806f061e
Two useful facts about Powersets suggested by Florian Kammueller
paulson
parents:
3222
diff
changeset

636 

4059  637 
goal thy "Pow (insert a A) = Pow A Un (insert a `` Pow A)"; 
3724  638 
by Safe_tac; 
3457  639 
by (etac swap 1); 
3348
3f9a806f061e
Two useful facts about Powersets suggested by Florian Kammueller
paulson
parents:
3222
diff
changeset

640 
by (res_inst_tac [("x", "x{a}")] image_eqI 1); 
3f9a806f061e
Two useful facts about Powersets suggested by Florian Kammueller
paulson
parents:
3222
diff
changeset

641 
by (ALLGOALS Blast_tac); 
3f9a806f061e
Two useful facts about Powersets suggested by Florian Kammueller
paulson
parents:
3222
diff
changeset

642 
qed "Pow_insert"; 
3f9a806f061e
Two useful facts about Powersets suggested by Florian Kammueller
paulson
parents:
3222
diff
changeset

643 

2021  644 

645 
(** Miniscoping: pushing in big Unions and Intersections **) 

646 
local 

4059  647 
fun prover s = prove_goal thy s (fn _ => [Blast_tac 1]) 
2021  648 
in 
2513
d708d8cdc8e8
New miniscoping rules for the bounded quantifiers and UN/INT operators
paulson
parents:
2512
diff
changeset

649 
val UN_simps = map prover 
4159
4aff9b7e5597
UNIV now a constant; UNION1, INTER1 now translations and no longer have
paulson
parents:
4136
diff
changeset

650 
["!!C. C ~= {} ==> (UN x:C. insert a (B x)) = insert a (UN x:C. B x)", 
4aff9b7e5597
UNIV now a constant; UNION1, INTER1 now translations and no longer have
paulson
parents:
4136
diff
changeset

651 
"!!C. C ~= {} ==> (UN x:C. A x Un B) = ((UN x:C. A x) Un B)", 
4aff9b7e5597
UNIV now a constant; UNION1, INTER1 now translations and no longer have
paulson
parents:
4136
diff
changeset

652 
"!!C. C ~= {} ==> (UN x:C. A Un B x) = (A Un (UN x:C. B x))", 
4aff9b7e5597
UNIV now a constant; UNION1, INTER1 now translations and no longer have
paulson
parents:
4136
diff
changeset

653 
"(UN x:C. A x Int B) = ((UN x:C. A x) Int B)", 
4aff9b7e5597
UNIV now a constant; UNION1, INTER1 now translations and no longer have
paulson
parents:
4136
diff
changeset

654 
"(UN x:C. A Int B x) = (A Int (UN x:C. B x))", 
4aff9b7e5597
UNIV now a constant; UNION1, INTER1 now translations and no longer have
paulson
parents:
4136
diff
changeset

655 
"(UN x:C. A x  B) = ((UN x:C. A x)  B)", 
4231  656 
"(UN x:C. A  B x) = (A  (INT x:C. B x))", 
657 
"(UN x:f``A. B x) = (UN a:A. B(f a))"]; 

2513
d708d8cdc8e8
New miniscoping rules for the bounded quantifiers and UN/INT operators
paulson
parents:
2512
diff
changeset

658 

d708d8cdc8e8
New miniscoping rules for the bounded quantifiers and UN/INT operators
paulson
parents:
2512
diff
changeset

659 
val INT_simps = map prover 
4159
4aff9b7e5597
UNIV now a constant; UNION1, INTER1 now translations and no longer have
paulson
parents:
4136
diff
changeset

660 
["!!C. C ~= {} ==> (INT x:C. A x Int B) = ((INT x:C. A x) Int B)", 
4aff9b7e5597
UNIV now a constant; UNION1, INTER1 now translations and no longer have
paulson
parents:
4136
diff
changeset

661 
"!!C. C ~= {} ==> (INT x:C. A Int B x) = (A Int (INT x:C. B x))", 
4aff9b7e5597
UNIV now a constant; UNION1, INTER1 now translations and no longer have
paulson
parents:
4136
diff
changeset

662 
"!!C. C ~= {} ==> (INT x:C. A x  B) = ((INT x:C. A x)  B)", 
4aff9b7e5597
UNIV now a constant; UNION1, INTER1 now translations and no longer have
paulson
parents:
4136
diff
changeset

663 
"!!C. C ~= {} ==> (INT x:C. A  B x) = (A  (UN x:C. B x))", 
4aff9b7e5597
UNIV now a constant; UNION1, INTER1 now translations and no longer have
paulson
parents:
4136
diff
changeset

664 
"(INT x:C. insert a (B x)) = insert a (INT x:C. B x)", 
4aff9b7e5597
UNIV now a constant; UNION1, INTER1 now translations and no longer have
paulson
parents:
4136
diff
changeset

665 
"(INT x:C. A x Un B) = ((INT x:C. A x) Un B)", 
4231  666 
"(INT x:C. A Un B x) = (A Un (INT x:C. B x))", 
667 
"(INT x:f``A. B x) = (INT a:A. B(f a))"]; 

2513
d708d8cdc8e8
New miniscoping rules for the bounded quantifiers and UN/INT operators
paulson
parents:
2512
diff
changeset

668 

d708d8cdc8e8
New miniscoping rules for the bounded quantifiers and UN/INT operators
paulson
parents:
2512
diff
changeset

669 

d708d8cdc8e8
New miniscoping rules for the bounded quantifiers and UN/INT operators
paulson
parents:
2512
diff
changeset

670 
val ball_simps = map prover 
d708d8cdc8e8
New miniscoping rules for the bounded quantifiers and UN/INT operators
paulson
parents:
2512
diff
changeset

671 
["(ALL x:A. P x  Q) = ((ALL x:A. P x)  Q)", 
d708d8cdc8e8
New miniscoping rules for the bounded quantifiers and UN/INT operators
paulson
parents:
2512
diff
changeset

672 
"(ALL x:A. P  Q x) = (P  (ALL x:A. Q x))", 
3422  673 
"(ALL x:A. P > Q x) = (P > (ALL x:A. Q x))", 
674 
"(ALL x:A. P x > Q) = ((EX x:A. P x) > Q)", 

2513
d708d8cdc8e8
New miniscoping rules for the bounded quantifiers and UN/INT operators
paulson
parents:
2512
diff
changeset

675 
"(ALL x:{}. P x) = True", 
4136  676 
"(ALL x:UNIV. P x) = (ALL x. P x)", 
2513
d708d8cdc8e8
New miniscoping rules for the bounded quantifiers and UN/INT operators
paulson
parents:
2512
diff
changeset

677 
"(ALL x:insert a B. P x) = (P(a) & (ALL x:B. P x))", 
d708d8cdc8e8
New miniscoping rules for the bounded quantifiers and UN/INT operators
paulson
parents:
2512
diff
changeset

678 
"(ALL x:Union(A). P x) = (ALL y:A. ALL x:y. P x)", 
3860  679 
"(ALL x:Collect Q. P x) = (ALL x. Q x > P x)", 
680 
"(ALL x:f``A. P x) = (ALL x:A. P(f x))", 

681 
"(~(ALL x:A. P x)) = (EX x:A. ~P x)"]; 

2513
d708d8cdc8e8
New miniscoping rules for the bounded quantifiers and UN/INT operators
paulson
parents:
2512
diff
changeset

682 

d708d8cdc8e8
New miniscoping rules for the bounded quantifiers and UN/INT operators
paulson
parents:
2512
diff
changeset

683 
val ball_conj_distrib = 
d708d8cdc8e8
New miniscoping rules for the bounded quantifiers and UN/INT operators
paulson
parents:
2512
diff
changeset

684 
prover "(ALL x:A. P x & Q x) = ((ALL x:A. P x) & (ALL x:A. Q x))"; 
d708d8cdc8e8
New miniscoping rules for the bounded quantifiers and UN/INT operators
paulson
parents:
2512
diff
changeset

685 

d708d8cdc8e8
New miniscoping rules for the bounded quantifiers and UN/INT operators
paulson
parents:
2512
diff
changeset

686 
val bex_simps = map prover 
d708d8cdc8e8
New miniscoping rules for the bounded quantifiers and UN/INT operators
paulson
parents:
2512
diff
changeset

687 
["(EX x:A. P x & Q) = ((EX x:A. P x) & Q)", 
d708d8cdc8e8
New miniscoping rules for the bounded quantifiers and UN/INT operators
paulson
parents:
2512
diff
changeset

688 
"(EX x:A. P & Q x) = (P & (EX x:A. Q x))", 
d708d8cdc8e8
New miniscoping rules for the bounded quantifiers and UN/INT operators
paulson
parents:
2512
diff
changeset

689 
"(EX x:{}. P x) = False", 
4136  690 
"(EX x:UNIV. P x) = (EX x. P x)", 
2513
d708d8cdc8e8
New miniscoping rules for the bounded quantifiers and UN/INT operators
paulson
parents:
2512
diff
changeset

691 
"(EX x:insert a B. P x) = (P(a)  (EX x:B. P x))", 
d708d8cdc8e8
New miniscoping rules for the bounded quantifiers and UN/INT operators
paulson
parents:
2512
diff
changeset

692 
"(EX x:Union(A). P x) = (EX y:A. EX x:y. P x)", 
3860  693 
"(EX x:Collect Q. P x) = (EX x. Q x & P x)", 
694 
"(EX x:f``A. P x) = (EX x:A. P(f x))", 

695 
"(~(EX x:A. P x)) = (ALL x:A. ~P x)"]; 

2513
d708d8cdc8e8
New miniscoping rules for the bounded quantifiers and UN/INT operators
paulson
parents:
2512
diff
changeset

696 

3426  697 
val bex_disj_distrib = 
2513
d708d8cdc8e8
New miniscoping rules for the bounded quantifiers and UN/INT operators
paulson
parents:
2512
diff
changeset

698 
prover "(EX x:A. P x  Q x) = ((EX x:A. P x)  (EX x:A. Q x))"; 
d708d8cdc8e8
New miniscoping rules for the bounded quantifiers and UN/INT operators
paulson
parents:
2512
diff
changeset

699 

2021  700 
end; 
701 

4159
4aff9b7e5597
UNIV now a constant; UNION1, INTER1 now translations and no longer have
paulson
parents:
4136
diff
changeset

702 
Addsimps (UN_simps @ INT_simps @ ball_simps @ bex_simps); 