author  paulson 
Wed, 08 Sep 1999 15:39:52 +0200  
changeset 7516  a1d476251238 
parent 7127  48e235179ffb 
child 7648  8258b93cdd32 
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 

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

19 

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

24 

5069  25 
Goalw [psubset_def] "~ (A < {})"; 
3222
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 

5069  30 
Goal "{x. P x  Q x} = {x. P x} Un {x. Q x}"; 
4748  31 
by (Blast_tac 1); 
32 
qed "Collect_disj_eq"; 

33 

5069  34 
Goal "{x. P x & Q x} = {x. P x} Int {x. Q x}"; 
4748  35 
by (Blast_tac 1); 
36 
qed "Collect_conj_eq"; 

37 

38 

1548  39 
section "insert"; 
923  40 

1531  41 
(*NOT SUITABLE FOR REWRITING since {a} == insert a {}*) 
5069  42 
Goal "insert a A = {a} Un A"; 
2891  43 
by (Blast_tac 1); 
1531  44 
qed "insert_is_Un"; 
45 

5069  46 
Goal "insert a A ~= {}"; 
4089  47 
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

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

50 

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

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

53 

5143
b94cd208f073
Removal of leading "\!\!..." from most Goal commands
paulson
parents:
5069
diff
changeset

54 
Goal "a:A ==> insert a A = A"; 
2891  55 
by (Blast_tac 1); 
923  56 
qed "insert_absorb"; 
6832  57 
(* Addsimps [insert_absorb] causes recursive calls 
58 
when there are nested inserts, with QUADRATIC running time 

4605  59 
*) 
923  60 

5069  61 
Goal "insert x (insert x A) = insert x A"; 
2891  62 
by (Blast_tac 1); 
1531  63 
qed "insert_absorb2"; 
64 
Addsimps [insert_absorb2]; 

65 

5069  66 
Goal "insert x (insert y A) = insert y (insert x A)"; 
2891  67 
by (Blast_tac 1); 
1879  68 
qed "insert_commute"; 
69 

5069  70 
Goal "(insert x A <= B) = (x:B & A <= B)"; 
2891  71 
by (Blast_tac 1); 
923  72 
qed "insert_subset"; 
1531  73 
Addsimps[insert_subset]; 
74 

5143
b94cd208f073
Removal of leading "\!\!..." from most Goal commands
paulson
parents:
5069
diff
changeset

75 
Goal "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

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

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

78 

1531  79 
(* use new B rather than (A{a}) to avoid infinite unfolding *) 
5143
b94cd208f073
Removal of leading "\!\!..." from most Goal commands
paulson
parents:
5069
diff
changeset

80 
Goal "a:A ==> ? B. A = insert a B & a ~: B"; 
1553  81 
by (res_inst_tac [("x","A{a}")] exI 1); 
2891  82 
by (Blast_tac 1); 
1531  83 
qed "mk_disjoint_insert"; 
923  84 

4882  85 
bind_thm ("insert_Collect", prove_goal thy 
5590  86 
"insert a (Collect P) = {u. u ~= a > P u}" (K [Auto_tac])); 
4882  87 

5941
1db9fad40a4f
better miniscoping rules: the premise C~={} is not good
paulson
parents:
5931
diff
changeset

88 
Goal "u: A ==> (UN x:A. insert a (B x)) = insert a (UN x:A. B x)"; 
2891  89 
by (Blast_tac 1); 
1843
a6d7aef48c2f
Removed the unused eq_cs, and added some distributive laws
paulson
parents:
1786
diff
changeset

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

91 

1660  92 
section "``"; 
923  93 

5069  94 
Goal "f``{} = {}"; 
2891  95 
by (Blast_tac 1); 
923  96 
qed "image_empty"; 
1531  97 
Addsimps[image_empty]; 
923  98 

5069  99 
Goal "f``insert a B = insert (f a) (f``B)"; 
2891  100 
by (Blast_tac 1); 
923  101 
qed "image_insert"; 
1531  102 
Addsimps[image_insert]; 
923  103 

6292
e50e1142dd06
new results e.g. about Pow; new simprules Union_image_eq, Inter_image_eq
paulson
parents:
6283
diff
changeset

104 
Goal "x:A ==> (%x. c) `` A = {c}"; 
e50e1142dd06
new results e.g. about Pow; new simprules Union_image_eq, Inter_image_eq
paulson
parents:
6283
diff
changeset

105 
by (Blast_tac 1); 
e50e1142dd06
new results e.g. about Pow; new simprules Union_image_eq, Inter_image_eq
paulson
parents:
6283
diff
changeset

106 
qed "image_constant"; 
e50e1142dd06
new results e.g. about Pow; new simprules Union_image_eq, Inter_image_eq
paulson
parents:
6283
diff
changeset

107 

5069  108 
Goal "f``(g``A) = (%x. f (g x)) `` A"; 
3457  109 
by (Blast_tac 1); 
4059  110 
qed "image_image"; 
3222
726a9b069947
Distributed Psubset stuff to basic set theory files, incl Finite.
nipkow
parents:
2922
diff
changeset

111 

5143
b94cd208f073
Removal of leading "\!\!..." from most Goal commands
paulson
parents:
5069
diff
changeset

112 
Goal "x:A ==> insert (f x) (f``A) = f``A"; 
2891  113 
by (Blast_tac 1); 
1884  114 
qed "insert_image"; 
115 
Addsimps [insert_image]; 

116 

5069  117 
Goal "(f``A = {}) = (A = {})"; 
4306
ddbe1a9722ab
Tidying and using equalityCE instead of the slower equalityE
paulson
parents:
4231
diff
changeset

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

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

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

121 

5281  122 
Goal "f `` {x. P x} = {f x  x. P x}"; 
5319
7356d0c88b1b
Moved Un_subset_iff and Int_subset_iff from UNITY to equalities.ML
paulson
parents:
5316
diff
changeset

123 
by (Blast_tac 1); 
5281  124 
qed "image_Collect"; 
125 
Addsimps [image_Collect]; 

126 

5590  127 
Goalw [image_def] "(%x. if P x then f x else g x) `` S \ 
128 
\ = (f `` (S Int {x. P x})) Un (g `` (S Int {x. ~(P x)}))"; 

4686  129 
by (Simp_tac 1); 
2891  130 
by (Blast_tac 1); 
1748  131 
qed "if_image_distrib"; 
132 
Addsimps[if_image_distrib]; 

133 

5590  134 
val prems = Goal "[M = N; !!x. x:N ==> f x = g x] ==> f``M = g``N"; 
4136  135 
by (simp_tac (simpset() addsimps image_def::prems) 1); 
136 
qed "image_cong"; 

137 

1748  138 

1548  139 
section "Int"; 
923  140 

5069  141 
Goal "A Int A = A"; 
2891  142 
by (Blast_tac 1); 
923  143 
qed "Int_absorb"; 
1531  144 
Addsimps[Int_absorb]; 
923  145 

5590  146 
Goal "A Int (A Int B) = A Int B"; 
4609  147 
by (Blast_tac 1); 
148 
qed "Int_left_absorb"; 

149 

5590  150 
Goal "A Int B = B Int A"; 
2891  151 
by (Blast_tac 1); 
923  152 
qed "Int_commute"; 
153 

5069  154 
Goal "A Int (B Int C) = B Int (A Int C)"; 
4609  155 
by (Blast_tac 1); 
156 
qed "Int_left_commute"; 

157 

5590  158 
Goal "(A Int B) Int C = A Int (B Int C)"; 
2891  159 
by (Blast_tac 1); 
923  160 
qed "Int_assoc"; 
161 

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

164 

5143
b94cd208f073
Removal of leading "\!\!..." from most Goal commands
paulson
parents:
5069
diff
changeset

165 
Goal "B<=A ==> A Int B = B"; 
4662  166 
by (Blast_tac 1); 
167 
qed "Int_absorb1"; 

168 

5143
b94cd208f073
Removal of leading "\!\!..." from most Goal commands
paulson
parents:
5069
diff
changeset

169 
Goal "A<=B ==> A Int B = A"; 
4662  170 
by (Blast_tac 1); 
171 
qed "Int_absorb2"; 

172 

5069  173 
Goal "{} Int B = {}"; 
2891  174 
by (Blast_tac 1); 
923  175 
qed "Int_empty_left"; 
1531  176 
Addsimps[Int_empty_left]; 
923  177 

5069  178 
Goal "A Int {} = {}"; 
2891  179 
by (Blast_tac 1); 
923  180 
qed "Int_empty_right"; 
1531  181 
Addsimps[Int_empty_right]; 
182 

5490  183 
Goal "(A Int B = {}) = (A <= B)"; 
4306
ddbe1a9722ab
Tidying and using equalityCE instead of the slower equalityE
paulson
parents:
4231
diff
changeset

184 
by (blast_tac (claset() addSEs [equalityCE]) 1); 
3356  185 
qed "disjoint_eq_subset_Compl"; 
186 

5069  187 
Goal "UNIV Int B = B"; 
2891  188 
by (Blast_tac 1); 
1531  189 
qed "Int_UNIV_left"; 
190 
Addsimps[Int_UNIV_left]; 

191 

5069  192 
Goal "A Int UNIV = A"; 
2891  193 
by (Blast_tac 1); 
1531  194 
qed "Int_UNIV_right"; 
195 
Addsimps[Int_UNIV_right]; 

923  196 

5069  197 
Goal "A Int B = Inter{A,B}"; 
4634  198 
by (Blast_tac 1); 
199 
qed "Int_eq_Inter"; 

200 

5590  201 
Goal "A Int (B Un C) = (A Int B) Un (A Int C)"; 
2891  202 
by (Blast_tac 1); 
923  203 
qed "Int_Un_distrib"; 
204 

5590  205 
Goal "(B Un C) Int A = (B Int A) Un (C Int A)"; 
2891  206 
by (Blast_tac 1); 
1618  207 
qed "Int_Un_distrib2"; 
208 

5069  209 
Goal "(A Int B = UNIV) = (A = UNIV & B = UNIV)"; 
4089  210 
by (blast_tac (claset() addEs [equalityCE]) 1); 
1531  211 
qed "Int_UNIV"; 
212 
Addsimps[Int_UNIV]; 

213 

5319
7356d0c88b1b
Moved Un_subset_iff and Int_subset_iff from UNITY to equalities.ML
paulson
parents:
5316
diff
changeset

214 
Goal "(C <= A Int B) = (C <= A & C <= B)"; 
7356d0c88b1b
Moved Un_subset_iff and Int_subset_iff from UNITY to equalities.ML
paulson
parents:
5316
diff
changeset

215 
by (Blast_tac 1); 
7356d0c88b1b
Moved Un_subset_iff and Int_subset_iff from UNITY to equalities.ML
paulson
parents:
5316
diff
changeset

216 
qed "Int_subset_iff"; 
7356d0c88b1b
Moved Un_subset_iff and Int_subset_iff from UNITY to equalities.ML
paulson
parents:
5316
diff
changeset

217 

7356d0c88b1b
Moved Un_subset_iff and Int_subset_iff from UNITY to equalities.ML
paulson
parents:
5316
diff
changeset

218 

1548  219 
section "Un"; 
923  220 

5069  221 
Goal "A Un A = A"; 
2891  222 
by (Blast_tac 1); 
923  223 
qed "Un_absorb"; 
1531  224 
Addsimps[Un_absorb]; 
923  225 

5069  226 
Goal " 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

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

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

229 

5590  230 
Goal "A Un B = B Un A"; 
2891  231 
by (Blast_tac 1); 
923  232 
qed "Un_commute"; 
233 

5069  234 
Goal "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

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

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

237 

5590  238 
Goal "(A Un B) Un C = A Un (B Un C)"; 
2891  239 
by (Blast_tac 1); 
923  240 
qed "Un_assoc"; 
241 

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

244 

5143
b94cd208f073
Removal of leading "\!\!..." from most Goal commands
paulson
parents:
5069
diff
changeset

245 
Goal "A<=B ==> A Un B = B"; 
4662  246 
by (Blast_tac 1); 
247 
qed "Un_absorb1"; 

248 

5143
b94cd208f073
Removal of leading "\!\!..." from most Goal commands
paulson
parents:
5069
diff
changeset

249 
Goal "B<=A ==> A Un B = A"; 
4662  250 
by (Blast_tac 1); 
251 
qed "Un_absorb2"; 

252 

5069  253 
Goal "{} Un B = B"; 
2891  254 
by (Blast_tac 1); 
923  255 
qed "Un_empty_left"; 
1531  256 
Addsimps[Un_empty_left]; 
923  257 

5069  258 
Goal "A Un {} = A"; 
2891  259 
by (Blast_tac 1); 
923  260 
qed "Un_empty_right"; 
1531  261 
Addsimps[Un_empty_right]; 
262 

5069  263 
Goal "UNIV Un B = UNIV"; 
2891  264 
by (Blast_tac 1); 
1531  265 
qed "Un_UNIV_left"; 
266 
Addsimps[Un_UNIV_left]; 

267 

5069  268 
Goal "A Un UNIV = UNIV"; 
2891  269 
by (Blast_tac 1); 
1531  270 
qed "Un_UNIV_right"; 
271 
Addsimps[Un_UNIV_right]; 

923  272 

5069  273 
Goal "A Un B = Union{A,B}"; 
4634  274 
by (Blast_tac 1); 
275 
qed "Un_eq_Union"; 

276 

5069  277 
Goal "(insert a B) Un C = insert a (B Un C)"; 
2891  278 
by (Blast_tac 1); 
923  279 
qed "Un_insert_left"; 
3384
5ef99c94e1fb
Now Un_insert_left, Un_insert_right are default rewrite rules
paulson
parents:
3356
diff
changeset

280 
Addsimps[Un_insert_left]; 
923  281 

5069  282 
Goal "A Un (insert a B) = insert a (A Un B)"; 
2891  283 
by (Blast_tac 1); 
1917  284 
qed "Un_insert_right"; 
3384
5ef99c94e1fb
Now Un_insert_left, Un_insert_right are default rewrite rules
paulson
parents:
3356
diff
changeset

285 
Addsimps[Un_insert_right]; 
1917  286 

5069  287 
Goal "(insert a B) Int C = (if a:C then insert a (B Int C) \ 
5590  288 
\ else B Int C)"; 
4686  289 
by (Simp_tac 1); 
3356  290 
by (Blast_tac 1); 
291 
qed "Int_insert_left"; 

292 

5069  293 
Goal "A Int (insert a B) = (if a:A then insert a (A Int B) \ 
5590  294 
\ else A Int B)"; 
4686  295 
by (Simp_tac 1); 
3356  296 
by (Blast_tac 1); 
297 
qed "Int_insert_right"; 

298 

5590  299 
Goal "A Un (B Int C) = (A Un B) Int (A Un C)"; 
2891  300 
by (Blast_tac 1); 
923  301 
qed "Un_Int_distrib"; 
302 

5590  303 
Goal "(B Int C) Un A = (B Un A) Int (C Un A)"; 
4609  304 
by (Blast_tac 1); 
305 
qed "Un_Int_distrib2"; 

306 

5590  307 
Goal "(A Int B) Un (B Int C) Un (C Int A) = \ 
308 
\ (A Un B) Int (B Un C) Int (C Un A)"; 

2891  309 
by (Blast_tac 1); 
923  310 
qed "Un_Int_crazy"; 
311 

5069  312 
Goal "(A<=B) = (A Un B = B)"; 
4306
ddbe1a9722ab
Tidying and using equalityCE instead of the slower equalityE
paulson
parents:
4231
diff
changeset

313 
by (blast_tac (claset() addSEs [equalityCE]) 1); 
923  314 
qed "subset_Un_eq"; 
315 

5069  316 
Goal "(A <= insert b C) = (A <= C  b:A & A{b} <= C)"; 
2891  317 
by (Blast_tac 1); 
923  318 
qed "subset_insert_iff"; 
319 

5069  320 
Goal "(A Un B = {}) = (A = {} & B = {})"; 
4089  321 
by (blast_tac (claset() addEs [equalityCE]) 1); 
923  322 
qed "Un_empty"; 
1531  323 
Addsimps[Un_empty]; 
923  324 

5319
7356d0c88b1b
Moved Un_subset_iff and Int_subset_iff from UNITY to equalities.ML
paulson
parents:
5316
diff
changeset

325 
Goal "(A Un B <= C) = (A <= C & B <= C)"; 
7356d0c88b1b
Moved Un_subset_iff and Int_subset_iff from UNITY to equalities.ML
paulson
parents:
5316
diff
changeset

326 
by (Blast_tac 1); 
7356d0c88b1b
Moved Un_subset_iff and Int_subset_iff from UNITY to equalities.ML
paulson
parents:
5316
diff
changeset

327 
qed "Un_subset_iff"; 
7356d0c88b1b
Moved Un_subset_iff and Int_subset_iff from UNITY to equalities.ML
paulson
parents:
5316
diff
changeset

328 

5331  329 
Goal "(A  B) Un (A Int B) = A"; 
330 
by (Blast_tac 1); 

331 
qed "Un_Diff_Int"; 

332 

5319
7356d0c88b1b
Moved Un_subset_iff and Int_subset_iff from UNITY to equalities.ML
paulson
parents:
5316
diff
changeset

333 

5931  334 
section "Set complement"; 
923  335 

7127
48e235179ffb
added parentheses to cope with a possible reduction of the precedence of unary
paulson
parents:
6832
diff
changeset

336 
Goal "A Int (A) = {}"; 
2891  337 
by (Blast_tac 1); 
923  338 
qed "Compl_disjoint"; 
1531  339 
Addsimps[Compl_disjoint]; 
923  340 

7127
48e235179ffb
added parentheses to cope with a possible reduction of the precedence of unary
paulson
parents:
6832
diff
changeset

341 
Goal "A Un (A) = UNIV"; 
2891  342 
by (Blast_tac 1); 
923  343 
qed "Compl_partition"; 
344 

7127
48e235179ffb
added parentheses to cope with a possible reduction of the precedence of unary
paulson
parents:
6832
diff
changeset

345 
Goal " (A) = (A:: 'a set)"; 
2891  346 
by (Blast_tac 1); 
923  347 
qed "double_complement"; 
1531  348 
Addsimps[double_complement]; 
923  349 

7127
48e235179ffb
added parentheses to cope with a possible reduction of the precedence of unary
paulson
parents:
6832
diff
changeset

350 
Goal "(A Un B) = (A) Int (B)"; 
2891  351 
by (Blast_tac 1); 
923  352 
qed "Compl_Un"; 
353 

7127
48e235179ffb
added parentheses to cope with a possible reduction of the precedence of unary
paulson
parents:
6832
diff
changeset

354 
Goal "(A Int B) = (A) Un (B)"; 
2891  355 
by (Blast_tac 1); 
923  356 
qed "Compl_Int"; 
357 

5490  358 
Goal "(UN x:A. B(x)) = (INT x:A. B(x))"; 
2891  359 
by (Blast_tac 1); 
923  360 
qed "Compl_UN"; 
361 

5490  362 
Goal "(INT x:A. B(x)) = (UN x:A. B(x))"; 
2891  363 
by (Blast_tac 1); 
923  364 
qed "Compl_INT"; 
365 

4615  366 
Addsimps [Compl_Un, Compl_Int, Compl_UN, Compl_INT]; 
367 

923  368 
(*Halmos, Naive Set Theory, page 16.*) 
369 

5069  370 
Goal "((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

371 
by (blast_tac (claset() addSEs [equalityCE]) 1); 
923  372 
qed "Un_Int_assoc_eq"; 
373 

374 

1548  375 
section "Union"; 
923  376 

5069  377 
Goal "Union({}) = {}"; 
2891  378 
by (Blast_tac 1); 
923  379 
qed "Union_empty"; 
1531  380 
Addsimps[Union_empty]; 
381 

5069  382 
Goal "Union(UNIV) = UNIV"; 
2891  383 
by (Blast_tac 1); 
1531  384 
qed "Union_UNIV"; 
385 
Addsimps[Union_UNIV]; 

923  386 

5069  387 
Goal "Union(insert a B) = a Un Union(B)"; 
2891  388 
by (Blast_tac 1); 
923  389 
qed "Union_insert"; 
1531  390 
Addsimps[Union_insert]; 
923  391 

5069  392 
Goal "Union(A Un B) = Union(A) Un Union(B)"; 
2891  393 
by (Blast_tac 1); 
923  394 
qed "Union_Un_distrib"; 
1531  395 
Addsimps[Union_Un_distrib]; 
923  396 

5069  397 
Goal "Union(A Int B) <= Union(A) Int Union(B)"; 
2891  398 
by (Blast_tac 1); 
923  399 
qed "Union_Int_subset"; 
400 

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

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

403 
qed "Union_empty_conv"; 
4003  404 
AddIffs [Union_empty_conv]; 
405 

5069  406 
Goal "(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

407 
by (blast_tac (claset() addSEs [equalityCE]) 1); 
923  408 
qed "Union_disjoint"; 
409 

1548  410 
section "Inter"; 
411 

5069  412 
Goal "Inter({}) = UNIV"; 
2891  413 
by (Blast_tac 1); 
1531  414 
qed "Inter_empty"; 
415 
Addsimps[Inter_empty]; 

416 

5069  417 
Goal "Inter(UNIV) = {}"; 
2891  418 
by (Blast_tac 1); 
1531  419 
qed "Inter_UNIV"; 
420 
Addsimps[Inter_UNIV]; 

421 

5069  422 
Goal "Inter(insert a B) = a Int Inter(B)"; 
2891  423 
by (Blast_tac 1); 
1531  424 
qed "Inter_insert"; 
425 
Addsimps[Inter_insert]; 

426 

5069  427 
Goal "Inter(A) Un Inter(B) <= Inter(A Int B)"; 
2891  428 
by (Blast_tac 1); 
1564
822575c737bd
Deleted faulty comment; proved new rule Inter_Un_subset
paulson
parents:
1553
diff
changeset

429 
qed "Inter_Un_subset"; 
1531  430 

5069  431 
Goal "Inter(A Un B) = Inter(A) Int Inter(B)"; 
2891  432 
by (Blast_tac 1); 
923  433 
qed "Inter_Un_distrib"; 
434 

1548  435 
section "UN and INT"; 
923  436 

437 
(*Basic identities*) 

438 

4200  439 
val not_empty = prove_goal Set.thy "(A ~= {}) = (? x. x:A)" (K [Blast_tac 1]); 
4136  440 

5069  441 
Goal "(UN x:{}. B x) = {}"; 
2891  442 
by (Blast_tac 1); 
1179
7678408f9751
Added insert_not_empty, UN_empty and UN_insert (to set_ss).
nipkow
parents:
923
diff
changeset

443 
qed "UN_empty"; 
1531  444 
Addsimps[UN_empty]; 
445 

5069  446 
Goal "(UN x:A. {}) = {}"; 
3457  447 
by (Blast_tac 1); 
3222
726a9b069947
Distributed Psubset stuff to basic set theory files, incl Finite.
nipkow
parents:
2922
diff
changeset

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

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

450 

5069  451 
Goal "(UN x:A. {x}) = A"; 
4645  452 
by (Blast_tac 1); 
453 
qed "UN_singleton"; 

454 
Addsimps [UN_singleton]; 

455 

5143
b94cd208f073
Removal of leading "\!\!..." from most Goal commands
paulson
parents:
5069
diff
changeset

456 
Goal "k:I ==> A k Un (UN i:I. A i) = (UN i:I. A i)"; 
4634  457 
by (Blast_tac 1); 
458 
qed "UN_absorb"; 

459 

5069  460 
Goal "(INT x:{}. B x) = UNIV"; 
2891  461 
by (Blast_tac 1); 
1531  462 
qed "INT_empty"; 
463 
Addsimps[INT_empty]; 

464 

5143
b94cd208f073
Removal of leading "\!\!..." from most Goal commands
paulson
parents:
5069
diff
changeset

465 
Goal "k:I ==> A k Int (INT i:I. A i) = (INT i:I. A i)"; 
4634  466 
by (Blast_tac 1); 
467 
qed "INT_absorb"; 

468 

5069  469 
Goal "(UN x:insert a A. B x) = B a Un UNION A B"; 
2891  470 
by (Blast_tac 1); 
1179
7678408f9751
Added insert_not_empty, UN_empty and UN_insert (to set_ss).
nipkow
parents:
923
diff
changeset

471 
qed "UN_insert"; 
1531  472 
Addsimps[UN_insert]; 
473 

5999  474 
Goal "(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

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

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

477 

5069  478 
Goal "(UN x : (UN y:A. B y). C x) = (UN y:A. UN x: B y. C x)"; 
4771  479 
by (Blast_tac 1); 
480 
qed "UN_UN_flatten"; 

481 

6292
e50e1142dd06
new results e.g. about Pow; new simprules Union_image_eq, Inter_image_eq
paulson
parents:
6283
diff
changeset

482 
Goal "((UN i:I. A i) <= B) = (ALL i:I. A i <= B)"; 
e50e1142dd06
new results e.g. about Pow; new simprules Union_image_eq, Inter_image_eq
paulson
parents:
6283
diff
changeset

483 
by (Blast_tac 1); 
e50e1142dd06
new results e.g. about Pow; new simprules Union_image_eq, Inter_image_eq
paulson
parents:
6283
diff
changeset

484 
qed "UN_subset_iff"; 
e50e1142dd06
new results e.g. about Pow; new simprules Union_image_eq, Inter_image_eq
paulson
parents:
6283
diff
changeset

485 

e50e1142dd06
new results e.g. about Pow; new simprules Union_image_eq, Inter_image_eq
paulson
parents:
6283
diff
changeset

486 
Goal "(B <= (INT i:I. A i)) = (ALL i:I. B <= A i)"; 
e50e1142dd06
new results e.g. about Pow; new simprules Union_image_eq, Inter_image_eq
paulson
parents:
6283
diff
changeset

487 
by (Blast_tac 1); 
e50e1142dd06
new results e.g. about Pow; new simprules Union_image_eq, Inter_image_eq
paulson
parents:
6283
diff
changeset

488 
qed "INT_subset_iff"; 
e50e1142dd06
new results e.g. about Pow; new simprules Union_image_eq, Inter_image_eq
paulson
parents:
6283
diff
changeset

489 

5069  490 
Goal "(INT x:insert a A. B x) = B a Int INTER A B"; 
2891  491 
by (Blast_tac 1); 
1531  492 
qed "INT_insert"; 
493 
Addsimps[INT_insert]; 

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

494 

5999  495 
Goal "(INT i: A Un B. M i) = (INT i: A. M i) Int (INT i:B. M i)"; 
496 
by (Blast_tac 1); 

497 
qed "INT_Un"; 

498 

5941
1db9fad40a4f
better miniscoping rules: the premise C~={} is not good
paulson
parents:
5931
diff
changeset

499 
Goal "u: A ==> (INT x:A. insert a (B x)) = insert a (INT x:A. B x)"; 
2891  500 
by (Blast_tac 1); 
2021  501 
qed "INT_insert_distrib"; 
502 

5069  503 
Goal "Union(B``A) = (UN x:A. B(x))"; 
2891  504 
by (Blast_tac 1); 
923  505 
qed "Union_image_eq"; 
6292
e50e1142dd06
new results e.g. about Pow; new simprules Union_image_eq, Inter_image_eq
paulson
parents:
6283
diff
changeset

506 
Addsimps [Union_image_eq]; 
923  507 

6283  508 
Goal "f `` Union S = (UN x:S. f `` x)"; 
509 
by (Blast_tac 1); 

510 
qed "image_Union_eq"; 

511 

5069  512 
Goal "Inter(B``A) = (INT x:A. B(x))"; 
2891  513 
by (Blast_tac 1); 
923  514 
qed "Inter_image_eq"; 
6292
e50e1142dd06
new results e.g. about Pow; new simprules Union_image_eq, Inter_image_eq
paulson
parents:
6283
diff
changeset

515 
Addsimps [Inter_image_eq]; 
923  516 

5941
1db9fad40a4f
better miniscoping rules: the premise C~={} is not good
paulson
parents:
5931
diff
changeset

517 
Goal "u: A ==> (UN y:A. c) = c"; 
2891  518 
by (Blast_tac 1); 
923  519 
qed "UN_constant"; 
4159
4aff9b7e5597
UNIV now a constant; UNION1, INTER1 now translations and no longer have
paulson
parents:
4136
diff
changeset

520 
Addsimps[UN_constant]; 
923  521 

5941
1db9fad40a4f
better miniscoping rules: the premise C~={} is not good
paulson
parents:
5931
diff
changeset

522 
Goal "u: A ==> (INT y:A. c) = c"; 
2891  523 
by (Blast_tac 1); 
923  524 
qed "INT_constant"; 
4159
4aff9b7e5597
UNIV now a constant; UNION1, INTER1 now translations and no longer have
paulson
parents:
4136
diff
changeset

525 
Addsimps[INT_constant]; 
923  526 

5069  527 
Goal "(UN x:A. B(x)) = Union({Y. ? x:A. Y=B(x)})"; 
2891  528 
by (Blast_tac 1); 
923  529 
qed "UN_eq"; 
530 

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

5069  532 
Goal "(INT x:A. B(x)) = Inter({Y. ? x:A. Y=B(x)})"; 
2891  533 
by (Blast_tac 1); 
923  534 
qed "INT_eq"; 
535 

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

536 

923  537 
(*Distributive laws...*) 
538 

5069  539 
Goal "A Int Union(B) = (UN C:B. A Int C)"; 
2891  540 
by (Blast_tac 1); 
923  541 
qed "Int_Union"; 
542 

5069  543 
Goal "Union(B) Int A = (UN C:B. C Int A)"; 
4674  544 
by (Blast_tac 1); 
545 
qed "Int_Union2"; 

546 

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

547 
(* Devlin, Fundamentals of Contemporary Set Theory, page 12, exercise 5: 
923  548 
Union of a family of unions **) 
5069  549 
Goal "(UN x:C. A(x) Un B(x)) = Union(A``C) Un Union(B``C)"; 
2891  550 
by (Blast_tac 1); 
923  551 
qed "Un_Union_image"; 
552 

553 
(*Equivalent version*) 

5069  554 
Goal "(UN i:I. A(i) Un B(i)) = (UN i:I. A(i)) Un (UN i:I. B(i))"; 
2891  555 
by (Blast_tac 1); 
923  556 
qed "UN_Un_distrib"; 
557 

5069  558 
Goal "A Un Inter(B) = (INT C:B. A Un C)"; 
2891  559 
by (Blast_tac 1); 
923  560 
qed "Un_Inter"; 
561 

5069  562 
Goal "(INT x:C. A(x) Int B(x)) = Inter(A``C) Int Inter(B``C)"; 
2891  563 
by (Blast_tac 1); 
923  564 
qed "Int_Inter_image"; 
565 

566 
(*Equivalent version*) 

5069  567 
Goal "(INT i:I. A(i) Int B(i)) = (INT i:I. A(i)) Int (INT i:I. B(i))"; 
2891  568 
by (Blast_tac 1); 
923  569 
qed "INT_Int_distrib"; 
570 

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

5069  572 
Goal "B Int (UN i:I. A(i)) = (UN i:I. B Int A(i))"; 
2891  573 
by (Blast_tac 1); 
923  574 
qed "Int_UN_distrib"; 
575 

5069  576 
Goal "B Un (INT i:I. A(i)) = (INT i:I. B Un A(i))"; 
2891  577 
by (Blast_tac 1); 
923  578 
qed "Un_INT_distrib"; 
579 

5278  580 
Goal "(UN i:I. A(i)) Int (UN j:J. B(j)) = (UN i:I. UN j:J. A(i) Int B(j))"; 
2891  581 
by (Blast_tac 1); 
923  582 
qed "Int_UN_distrib2"; 
583 

5278  584 
Goal "(INT i:I. A(i)) Un (INT j:J. B(j)) = (INT i:I. INT j:J. A(i) Un B(j))"; 
2891  585 
by (Blast_tac 1); 
923  586 
qed "Un_INT_distrib2"; 
587 

2512  588 

589 
section"Bounded quantifiers"; 

590 

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

2512  593 

5069  594 
Goal "(ALL x:A Un B. P x) = ((ALL x:A. P x) & (ALL x:B. P x))"; 
2891  595 
by (Blast_tac 1); 
2519  596 
qed "ball_Un"; 
597 

5069  598 
Goal "(EX x:A Un B. P x) = ((EX x:A. P x)  (EX x:B. P x))"; 
2891  599 
by (Blast_tac 1); 
2519  600 
qed "bex_Un"; 
2512  601 

5069  602 
Goal "(ALL z: UNION A B. P z) = (ALL x:A. ALL z:B x. P z)"; 
4771  603 
by (Blast_tac 1); 
604 
qed "ball_UN"; 

605 

5069  606 
Goal "(EX z: UNION A B. P z) = (EX x:A. EX z:B x. P z)"; 
4771  607 
by (Blast_tac 1); 
608 
qed "bex_UN"; 

609 

2512  610 

1548  611 
section ""; 
923  612 

7127
48e235179ffb
added parentheses to cope with a possible reduction of the precedence of unary
paulson
parents:
6832
diff
changeset

613 
Goal "AB = A Int (B)"; 
4609  614 
by (Blast_tac 1); 
4662  615 
qed "Diff_eq"; 
4609  616 

7516  617 
Goal "(AB = {}) = (A<=B)"; 
618 
by (Blast_tac 1); 

619 
qed "Diff_eq_empty_iff"; 

620 
Addsimps[Diff_eq_empty_iff]; 

621 

5069  622 
Goal "AA = {}"; 
2891  623 
by (Blast_tac 1); 
923  624 
qed "Diff_cancel"; 
1531  625 
Addsimps[Diff_cancel]; 
923  626 

5143
b94cd208f073
Removal of leading "\!\!..." from most Goal commands
paulson
parents:
5069
diff
changeset

627 
Goal "A Int B = {} ==> AB = A"; 
4674  628 
by (blast_tac (claset() addEs [equalityE]) 1); 
629 
qed "Diff_triv"; 

630 

5069  631 
Goal "{}A = {}"; 
2891  632 
by (Blast_tac 1); 
923  633 
qed "empty_Diff"; 
1531  634 
Addsimps[empty_Diff]; 
923  635 

5069  636 
Goal "A{} = A"; 
2891  637 
by (Blast_tac 1); 
923  638 
qed "Diff_empty"; 
1531  639 
Addsimps[Diff_empty]; 
640 

5069  641 
Goal "AUNIV = {}"; 
2891  642 
by (Blast_tac 1); 
1531  643 
qed "Diff_UNIV"; 
644 
Addsimps[Diff_UNIV]; 

645 

5143
b94cd208f073
Removal of leading "\!\!..." from most Goal commands
paulson
parents:
5069
diff
changeset

646 
Goal "x~:A ==> A  insert x B = AB"; 
2891  647 
by (Blast_tac 1); 
1531  648 
qed "Diff_insert0"; 
649 
Addsimps [Diff_insert0]; 

923  650 

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

5069  652 
Goal "A  insert a B = A  B  {a}"; 
2891  653 
by (Blast_tac 1); 
923  654 
qed "Diff_insert"; 
655 

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

5069  657 
Goal "A  insert a B = A  {a}  B"; 
2891  658 
by (Blast_tac 1); 
923  659 
qed "Diff_insert2"; 
660 

5069  661 
Goal "insert x A  B = (if x:B then AB else insert x (AB))"; 
4686  662 
by (Simp_tac 1); 
2891  663 
by (Blast_tac 1); 
1531  664 
qed "insert_Diff_if"; 
665 

5143
b94cd208f073
Removal of leading "\!\!..." from most Goal commands
paulson
parents:
5069
diff
changeset

666 
Goal "x:B ==> insert x A  B = AB"; 
2891  667 
by (Blast_tac 1); 
1531  668 
qed "insert_Diff1"; 
669 
Addsimps [insert_Diff1]; 

670 

5143
b94cd208f073
Removal of leading "\!\!..." from most Goal commands
paulson
parents:
5069
diff
changeset

671 
Goal "a:A ==> insert a (A{a}) = A"; 
2922  672 
by (Blast_tac 1); 
923  673 
qed "insert_Diff"; 
674 

5069  675 
Goal "A Int (BA) = {}"; 
2891  676 
by (Blast_tac 1); 
923  677 
qed "Diff_disjoint"; 
1531  678 
Addsimps[Diff_disjoint]; 
923  679 

5143
b94cd208f073
Removal of leading "\!\!..." from most Goal commands
paulson
parents:
5069
diff
changeset

680 
Goal "A<=B ==> A Un (BA) = B"; 
2891  681 
by (Blast_tac 1); 
923  682 
qed "Diff_partition"; 
683 

5143
b94cd208f073
Removal of leading "\!\!..." from most Goal commands
paulson
parents:
5069
diff
changeset

684 
Goal "[ A<=B; B<= C ] ==> (B  (C  A)) = (A :: 'a set)"; 
2891  685 
by (Blast_tac 1); 
923  686 
qed "double_diff"; 
687 

5069  688 
Goal "A Un (BA) = A Un B"; 
4645  689 
by (Blast_tac 1); 
690 
qed "Un_Diff_cancel"; 

691 

5069  692 
Goal "(BA) Un A = B Un A"; 
4645  693 
by (Blast_tac 1); 
694 
qed "Un_Diff_cancel2"; 

695 

696 
Addsimps [Un_Diff_cancel, Un_Diff_cancel2]; 

697 

5069  698 
Goal "A  (B Un C) = (AB) Int (AC)"; 
2891  699 
by (Blast_tac 1); 
923  700 
qed "Diff_Un"; 
701 

5069  702 
Goal "A  (B Int C) = (AB) Un (AC)"; 
2891  703 
by (Blast_tac 1); 
923  704 
qed "Diff_Int"; 
705 

5069  706 
Goal "(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

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

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

709 

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

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

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

713 

5069  714 
Goal "C Int (AB) = (C Int A)  (C Int B)"; 
4748  715 
by (Blast_tac 1); 
716 
qed "Diff_Int_distrib"; 

717 

5069  718 
Goal "(AB) Int C = (A Int C)  (B Int C)"; 
4645  719 
by (Blast_tac 1); 
4748  720 
qed "Diff_Int_distrib2"; 
4645  721 

7127
48e235179ffb
added parentheses to cope with a possible reduction of the precedence of unary
paulson
parents:
6832
diff
changeset

722 
Goal "A  ( B) = A Int B"; 
5632  723 
by Auto_tac; 
724 
qed "Diff_Compl"; 

725 
Addsimps [Diff_Compl]; 

726 

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

727 

5238  728 
section "Quantification over type \"bool\""; 
729 

730 
Goal "(ALL b::bool. P b) = (P True & P False)"; 

731 
by Auto_tac; 

732 
by (case_tac "b" 1); 

733 
by Auto_tac; 

734 
qed "all_bool_eq"; 

735 

5762  736 
bind_thm ("bool_induct", conjI RS (all_bool_eq RS iffD2) RS spec); 
737 

5238  738 
Goal "(EX b::bool. P b) = (P True  P False)"; 
739 
by Auto_tac; 

740 
by (case_tac "b" 1); 

741 
by Auto_tac; 

742 
qed "ex_bool_eq"; 

743 

744 
Goal "A Un B = (UN b. if b then A else B)"; 

6301  745 
by (auto_tac(claset()delWrapper"bspec",simpset()addsimps [split_if_mem2])); 
5238  746 
qed "Un_eq_UN"; 
747 

748 
Goal "(UN b::bool. A b) = (A True Un A False)"; 

749 
by Auto_tac; 

750 
by (case_tac "b" 1); 

751 
by Auto_tac; 

752 
qed "UN_bool_eq"; 

753 

754 
Goal "(INT b::bool. A b) = (A True Int A False)"; 

755 
by Auto_tac; 

756 
by (case_tac "b" 1); 

757 
by Auto_tac; 

758 
qed "INT_bool_eq"; 

759 

760 

6292
e50e1142dd06
new results e.g. about Pow; new simprules Union_image_eq, Inter_image_eq
paulson
parents:
6283
diff
changeset

761 
section "Pow"; 
e50e1142dd06
new results e.g. about Pow; new simprules Union_image_eq, Inter_image_eq
paulson
parents:
6283
diff
changeset

762 

e50e1142dd06
new results e.g. about Pow; new simprules Union_image_eq, Inter_image_eq
paulson
parents:
6283
diff
changeset

763 
Goalw [Pow_def] "Pow {} = {{}}"; 
e50e1142dd06
new results e.g. about Pow; new simprules Union_image_eq, Inter_image_eq
paulson
parents:
6283
diff
changeset

764 
by Auto_tac; 
e50e1142dd06
new results e.g. about Pow; new simprules Union_image_eq, Inter_image_eq
paulson
parents:
6283
diff
changeset

765 
qed "Pow_empty"; 
e50e1142dd06
new results e.g. about Pow; new simprules Union_image_eq, Inter_image_eq
paulson
parents:
6283
diff
changeset

766 
Addsimps [Pow_empty]; 
e50e1142dd06
new results e.g. about Pow; new simprules Union_image_eq, Inter_image_eq
paulson
parents:
6283
diff
changeset

767 

e50e1142dd06
new results e.g. about Pow; new simprules Union_image_eq, Inter_image_eq
paulson
parents:
6283
diff
changeset

768 
Goal "Pow (insert a A) = Pow A Un (insert a `` Pow A)"; 
e50e1142dd06
new results e.g. about Pow; new simprules Union_image_eq, Inter_image_eq
paulson
parents:
6283
diff
changeset

769 
by Safe_tac; 
e50e1142dd06
new results e.g. about Pow; new simprules Union_image_eq, Inter_image_eq
paulson
parents:
6283
diff
changeset

770 
by (etac swap 1); 
e50e1142dd06
new results e.g. about Pow; new simprules Union_image_eq, Inter_image_eq
paulson
parents:
6283
diff
changeset

771 
by (res_inst_tac [("x", "x{a}")] image_eqI 1); 
e50e1142dd06
new results e.g. about Pow; new simprules Union_image_eq, Inter_image_eq
paulson
parents:
6283
diff
changeset

772 
by (ALLGOALS Blast_tac); 
e50e1142dd06
new results e.g. about Pow; new simprules Union_image_eq, Inter_image_eq
paulson
parents:
6283
diff
changeset

773 
qed "Pow_insert"; 
e50e1142dd06
new results e.g. about Pow; new simprules Union_image_eq, Inter_image_eq
paulson
parents:
6283
diff
changeset

774 

e50e1142dd06
new results e.g. about Pow; new simprules Union_image_eq, Inter_image_eq
paulson
parents:
6283
diff
changeset

775 
Goal "Pow ( A) = {B B. A: Pow B}"; 
e50e1142dd06
new results e.g. about Pow; new simprules Union_image_eq, Inter_image_eq
paulson
parents:
6283
diff
changeset

776 
by Safe_tac; 
e50e1142dd06
new results e.g. about Pow; new simprules Union_image_eq, Inter_image_eq
paulson
parents:
6283
diff
changeset

777 
by (Blast_tac 2); 
e50e1142dd06
new results e.g. about Pow; new simprules Union_image_eq, Inter_image_eq
paulson
parents:
6283
diff
changeset

778 
by (res_inst_tac [("x", "x")] exI 1); 
e50e1142dd06
new results e.g. about Pow; new simprules Union_image_eq, Inter_image_eq
paulson
parents:
6283
diff
changeset

779 
by (ALLGOALS Blast_tac); 
e50e1142dd06
new results e.g. about Pow; new simprules Union_image_eq, Inter_image_eq
paulson
parents:
6283
diff
changeset

780 
qed "Pow_Compl"; 
e50e1142dd06
new results e.g. about Pow; new simprules Union_image_eq, Inter_image_eq
paulson
parents:
6283
diff
changeset

781 

e50e1142dd06
new results e.g. about Pow; new simprules Union_image_eq, Inter_image_eq
paulson
parents:
6283
diff
changeset

782 
Goal "Pow UNIV = UNIV"; 
e50e1142dd06
new results e.g. about Pow; new simprules Union_image_eq, Inter_image_eq
paulson
parents:
6283
diff
changeset

783 
by (Blast_tac 1); 
e50e1142dd06
new results e.g. about Pow; new simprules Union_image_eq, Inter_image_eq
paulson
parents:
6283
diff
changeset

784 
qed "Pow_UNIV"; 
e50e1142dd06
new results e.g. about Pow; new simprules Union_image_eq, Inter_image_eq
paulson
parents:
6283
diff
changeset

785 
Addsimps [Pow_UNIV]; 
e50e1142dd06
new results e.g. about Pow; new simprules Union_image_eq, Inter_image_eq
paulson
parents:
6283
diff
changeset

786 

e50e1142dd06
new results e.g. about Pow; new simprules Union_image_eq, Inter_image_eq
paulson
parents:
6283
diff
changeset

787 
Goal "Pow(A) Un Pow(B) <= Pow(A Un B)"; 
e50e1142dd06
new results e.g. about Pow; new simprules Union_image_eq, Inter_image_eq
paulson
parents:
6283
diff
changeset

788 
by (Blast_tac 1); 
e50e1142dd06
new results e.g. about Pow; new simprules Union_image_eq, Inter_image_eq
paulson
parents:
6283
diff
changeset

789 
qed "Un_Pow_subset"; 
e50e1142dd06
new results e.g. about Pow; new simprules Union_image_eq, Inter_image_eq
paulson
parents:
6283
diff
changeset

790 

e50e1142dd06
new results e.g. about Pow; new simprules Union_image_eq, Inter_image_eq
paulson
parents:
6283
diff
changeset

791 
Goal "(UN x:A. Pow(B(x))) <= Pow(UN x:A. B(x))"; 
e50e1142dd06
new results e.g. about Pow; new simprules Union_image_eq, Inter_image_eq
paulson
parents:
6283
diff
changeset

792 
by (Blast_tac 1); 
e50e1142dd06
new results e.g. about Pow; new simprules Union_image_eq, Inter_image_eq
paulson
parents:
6283
diff
changeset

793 
qed "UN_Pow_subset"; 
e50e1142dd06
new results e.g. about Pow; new simprules Union_image_eq, Inter_image_eq
paulson
parents:
6283
diff
changeset

794 

e50e1142dd06
new results e.g. about Pow; new simprules Union_image_eq, Inter_image_eq
paulson
parents:
6283
diff
changeset

795 
Goal "A <= Pow(Union(A))"; 
e50e1142dd06
new results e.g. about Pow; new simprules Union_image_eq, Inter_image_eq
paulson
parents:
6283
diff
changeset

796 
by (Blast_tac 1); 
e50e1142dd06
new results e.g. about Pow; new simprules Union_image_eq, Inter_image_eq
paulson
parents:
6283
diff
changeset

797 
qed "subset_Pow_Union"; 
e50e1142dd06
new results e.g. about Pow; new simprules Union_image_eq, Inter_image_eq
paulson
parents:
6283
diff
changeset

798 

e50e1142dd06
new results e.g. about Pow; new simprules Union_image_eq, Inter_image_eq
paulson
parents:
6283
diff
changeset

799 
Goal "Union(Pow(A)) = A"; 
e50e1142dd06
new results e.g. about Pow; new simprules Union_image_eq, Inter_image_eq
paulson
parents:
6283
diff
changeset

800 
by (Blast_tac 1); 
e50e1142dd06
new results e.g. about Pow; new simprules Union_image_eq, Inter_image_eq
paulson
parents:
6283
diff
changeset

801 
qed "Union_Pow_eq"; 
e50e1142dd06
new results e.g. about Pow; new simprules Union_image_eq, Inter_image_eq
paulson
parents:
6283
diff
changeset

802 

e50e1142dd06
new results e.g. about Pow; new simprules Union_image_eq, Inter_image_eq
paulson
parents:
6283
diff
changeset

803 
Goal "Pow(A Int B) = Pow(A) Int Pow(B)"; 
e50e1142dd06
new results e.g. about Pow; new simprules Union_image_eq, Inter_image_eq
paulson
parents:
6283
diff
changeset

804 
by (Blast_tac 1); 
e50e1142dd06
new results e.g. about Pow; new simprules Union_image_eq, Inter_image_eq
paulson
parents:
6283
diff
changeset

805 
qed "Pow_Int_eq"; 
e50e1142dd06
new results e.g. about Pow; new simprules Union_image_eq, Inter_image_eq
paulson
parents:
6283
diff
changeset

806 

e50e1142dd06
new results e.g. about Pow; new simprules Union_image_eq, Inter_image_eq
paulson
parents:
6283
diff
changeset

807 
Goal "Pow(INT x:A. B(x)) = (INT x:A. Pow(B(x)))"; 
e50e1142dd06
new results e.g. about Pow; new simprules Union_image_eq, Inter_image_eq
paulson
parents:
6283
diff
changeset

808 
by (Blast_tac 1); 
e50e1142dd06
new results e.g. about Pow; new simprules Union_image_eq, Inter_image_eq
paulson
parents:
6283
diff
changeset

809 
qed "Pow_INT_eq"; 
e50e1142dd06
new results e.g. about Pow; new simprules Union_image_eq, Inter_image_eq
paulson
parents:
6283
diff
changeset

810 

e50e1142dd06
new results e.g. about Pow; new simprules Union_image_eq, Inter_image_eq
paulson
parents:
6283
diff
changeset

811 
Addsimps [Union_Pow_eq, Pow_Int_eq]; 
e50e1142dd06
new results e.g. about Pow; new simprules Union_image_eq, Inter_image_eq
paulson
parents:
6283
diff
changeset

812 

e50e1142dd06
new results e.g. about Pow; new simprules Union_image_eq, Inter_image_eq
paulson
parents:
6283
diff
changeset

813 

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

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

815 

5069  816 
Goal "(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

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

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

819 

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

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

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

823 

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

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

826 
qed "subset_iff_psubset_eq"; 
2021  827 

5069  828 
Goal "(!x. x ~: A) = (A={})"; 
4423  829 
by (Blast_tac 1); 
3896
ee8ebb74ec00
Various new lemmas. Improved conversion of equations to rewrite rules:
nipkow
parents:
3860
diff
changeset

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

832 

6007  833 

5189
362e4d6213c5
Added theorem distinct_lemma (needed for datatypes).
berghofe
parents:
5148
diff
changeset

834 
(** for datatypes **) 
362e4d6213c5
Added theorem distinct_lemma (needed for datatypes).
berghofe
parents:
5148
diff
changeset

835 
Goal "f x ~= f y ==> x ~= y"; 
362e4d6213c5
Added theorem distinct_lemma (needed for datatypes).
berghofe
parents:
5148
diff
changeset

836 
by (Fast_tac 1); 
362e4d6213c5
Added theorem distinct_lemma (needed for datatypes).
berghofe
parents:
5148
diff
changeset

837 
qed "distinct_lemma"; 
362e4d6213c5
Added theorem distinct_lemma (needed for datatypes).
berghofe
parents:
5148
diff
changeset

838 

2021  839 

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

841 
local 

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

844 
val UN_simps = map prover 
5941
1db9fad40a4f
better miniscoping rules: the premise C~={} is not good
paulson
parents:
5931
diff
changeset

845 
["!!C. c: C ==> (UN x:C. insert a (B x)) = insert a (UN x:C. B x)", 
1db9fad40a4f
better miniscoping rules: the premise C~={} is not good
paulson
parents:
5931
diff
changeset

846 
"!!C. c: C ==> (UN x:C. A x Un B) = ((UN x:C. A x) Un B)", 
1db9fad40a4f
better miniscoping rules: the premise C~={} is not good
paulson
parents:
5931
diff
changeset

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

848 
"(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

849 
"(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

850 
"(UN x:C. A x  B) = ((UN x:C. A x)  B)", 
4231  851 
"(UN x:C. A  B x) = (A  (INT x:C. B x))", 
852 
"(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

853 

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

854 
val INT_simps = map prover 
5941
1db9fad40a4f
better miniscoping rules: the premise C~={} is not good
paulson
parents:
5931
diff
changeset

855 
["!!C. c: C ==> (INT x:C. A x Int B) = ((INT x:C. A x) Int B)", 
1db9fad40a4f
better miniscoping rules: the premise C~={} is not good
paulson
parents:
5931
diff
changeset

856 
"!!C. c: C ==> (INT x:C. A Int B x) = (A Int (INT x:C. B x))", 
1db9fad40a4f
better miniscoping rules: the premise C~={} is not good
paulson
parents:
5931
diff
changeset

857 
"!!C. c: C ==> (INT x:C. A x  B) = ((INT x:C. A x)  B)", 
1db9fad40a4f
better miniscoping rules: the premise C~={} is not good
paulson
parents:
5931
diff
changeset

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

859 
"(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

860 
"(INT x:C. A x Un B) = ((INT x:C. A x) Un B)", 
4231  861 
"(INT x:C. A Un B x) = (A Un (INT x:C. B x))", 
862 
"(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

863 

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

864 

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

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

866 
["(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

867 
"(ALL x:A. P  Q x) = (P  (ALL x:A. Q x))", 
3422  868 
"(ALL x:A. P > Q x) = (P > (ALL x:A. Q x))", 
869 
"(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

870 
"(ALL x:{}. P x) = True", 
4136  871 
"(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

872 
"(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

873 
"(ALL x:Union(A). P x) = (ALL y:A. ALL x:y. P x)", 
5233
3571ff68ceda
New rewrite rules for quantification over bounded UNIONs
paulson
parents:
5189
diff
changeset

874 
"(ALL x: UNION A B. P x) = (ALL a:A. ALL x: B a. P x)", 
3860  875 
"(ALL x:Collect Q. P x) = (ALL x. Q x > P x)", 
876 
"(ALL x:f``A. P x) = (ALL x:A. P(f x))", 

877 
"(~(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

878 

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

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

880 
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

881 

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

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

883 
["(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

884 
"(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

885 
"(EX x:{}. P x) = False", 
4136  886 
"(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

887 
"(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

888 
"(EX x:Union(A). P x) = (EX y:A. EX x:y. P x)", 
5233
3571ff68ceda
New rewrite rules for quantification over bounded UNIONs
paulson
parents:
5189
diff
changeset

889 
"(EX x: UNION A B. P x) = (EX a:A. EX x: B a. P x)", 
3860  890 
"(EX x:Collect Q. P x) = (EX x. Q x & P x)", 
891 
"(EX x:f``A. P x) = (EX x:A. P(f x))", 

892 
"(~(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

893 

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

895 
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

896 

2021  897 
end; 
898 

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

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