author  nipkow 
Fri, 24 Nov 2000 16:49:27 +0100  
changeset 10519  ade64af4c57c 
parent 10234  c8726d4ee89a 
child 10832  e33b47e4246d 
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 

7824
1a85ba81d019
new default simprule Collect_const and new them Diff_insert_absorb
paulson
parents:
7713
diff
changeset

15 
(*supersedes Collect_False_empty*) 
1a85ba81d019
new default simprule Collect_const and new them Diff_insert_absorb
paulson
parents:
7713
diff
changeset

16 
Goal "{s. P} = (if P then UNIV else {})"; 
1a85ba81d019
new default simprule Collect_const and new them Diff_insert_absorb
paulson
parents:
7713
diff
changeset

17 
by (Force_tac 1); 
1a85ba81d019
new default simprule Collect_const and new them Diff_insert_absorb
paulson
parents:
7713
diff
changeset

18 
qed "Collect_const"; 
1a85ba81d019
new default simprule Collect_const and new them Diff_insert_absorb
paulson
parents:
7713
diff
changeset

19 
Addsimps [Collect_const]; 
1531  20 

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

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

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

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

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

30 

9206  31 
Goal "(Collect P = {}) = (ALL x. ~ P x)"; 
7958  32 
by Auto_tac; 
33 
qed "Collect_empty_eq"; 

34 
Addsimps[Collect_empty_eq]; 

35 

8993  36 
Goal "{x. ~ (P x)} =  {x. P x}"; 
37 
by (Blast_tac 1); 

38 
qed "Collect_neg_eq"; 

39 

5069  40 
Goal "{x. P x  Q x} = {x. P x} Un {x. Q x}"; 
4748  41 
by (Blast_tac 1); 
42 
qed "Collect_disj_eq"; 

43 

5069  44 
Goal "{x. P x & Q x} = {x. P x} Int {x. Q x}"; 
4748  45 
by (Blast_tac 1); 
46 
qed "Collect_conj_eq"; 

47 

7845  48 
Goal "{x. ALL y. P x y} = (INT y. {x. P x y})"; 
49 
by (Blast_tac 1); 

50 
qed "Collect_all_eq"; 

51 

52 
Goal "{x. ALL y: A. P x y} = (INT y: A. {x. P x y})"; 

53 
by (Blast_tac 1); 

54 
qed "Collect_ball_eq"; 

55 

56 
Goal "{x. EX y. P x y} = (UN y. {x. P x y})"; 

57 
by (Blast_tac 1); 

58 
qed "Collect_ex_eq"; 

59 

60 
Goal "{x. EX y: A. P x y} = (UN y: A. {x. P x y})"; 

61 
by (Blast_tac 1); 

62 
qed "Collect_bex_eq"; 

63 

4748  64 

1548  65 
section "insert"; 
923  66 

1531  67 
(*NOT SUITABLE FOR REWRITING since {a} == insert a {}*) 
5069  68 
Goal "insert a A = {a} Un A"; 
2891  69 
by (Blast_tac 1); 
1531  70 
qed "insert_is_Un"; 
71 

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

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

76 

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

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

79 

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

80 
Goal "a:A ==> insert a A = A"; 
2891  81 
by (Blast_tac 1); 
923  82 
qed "insert_absorb"; 
6832  83 
(* Addsimps [insert_absorb] causes recursive calls 
84 
when there are nested inserts, with QUADRATIC running time 

4605  85 
*) 
923  86 

5069  87 
Goal "insert x (insert x A) = insert x A"; 
2891  88 
by (Blast_tac 1); 
1531  89 
qed "insert_absorb2"; 
90 
Addsimps [insert_absorb2]; 

91 

5069  92 
Goal "insert x (insert y A) = insert y (insert x A)"; 
2891  93 
by (Blast_tac 1); 
1879  94 
qed "insert_commute"; 
95 

5069  96 
Goal "(insert x A <= B) = (x:B & A <= B)"; 
2891  97 
by (Blast_tac 1); 
923  98 
qed "insert_subset"; 
1531  99 
Addsimps[insert_subset]; 
100 

101 
(* use new B rather than (A{a}) to avoid infinite unfolding *) 

9206  102 
Goal "a:A ==> EX B. A = insert a B & a ~: B"; 
1553  103 
by (res_inst_tac [("x","A{a}")] exI 1); 
2891  104 
by (Blast_tac 1); 
1531  105 
qed "mk_disjoint_insert"; 
923  106 

9969  107 
Goal "insert a (Collect P) = {u. u ~= a > P u}"; 
108 
by Auto_tac; 

109 
qed "insert_Collect"; 

4882  110 

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

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

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

114 

1660  115 
section "``"; 
923  116 

5069  117 
Goal "f``{} = {}"; 
2891  118 
by (Blast_tac 1); 
923  119 
qed "image_empty"; 
1531  120 
Addsimps[image_empty]; 
923  121 

5069  122 
Goal "f``insert a B = insert (f a) (f``B)"; 
2891  123 
by (Blast_tac 1); 
923  124 
qed "image_insert"; 
1531  125 
Addsimps[image_insert]; 
923  126 

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

127 
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

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

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

130 

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

134 

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

135 
Goal "x:A ==> insert (f x) (f``A) = f``A"; 
2891  136 
by (Blast_tac 1); 
1884  137 
qed "insert_image"; 
138 
Addsimps [insert_image]; 

139 

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

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

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

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

144 

5281  145 
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

146 
by (Blast_tac 1); 
5281  147 
qed "image_Collect"; 
148 
Addsimps [image_Collect]; 

149 

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

4686  152 
by (Simp_tac 1); 
2891  153 
by (Blast_tac 1); 
1748  154 
qed "if_image_distrib"; 
155 
Addsimps[if_image_distrib]; 

156 

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

160 

1748  161 

7958  162 
section "range"; 
163 

9206  164 
Goal "{u. EX x. u = f x} = range f"; 
7958  165 
by Auto_tac; 
166 
qed "full_SetCompr_eq"; 

167 

8161  168 
Goal "range (%x. f (g x)) = f``range g"; 
169 
by (stac image_image 1); 

170 
by (Simp_tac 1); 

171 
qed "range_composition"; 

172 
Addsimps[range_composition]; 

7958  173 

1548  174 
section "Int"; 
923  175 

5069  176 
Goal "A Int A = A"; 
2891  177 
by (Blast_tac 1); 
923  178 
qed "Int_absorb"; 
1531  179 
Addsimps[Int_absorb]; 
923  180 

5590  181 
Goal "A Int (A Int B) = A Int B"; 
4609  182 
by (Blast_tac 1); 
183 
qed "Int_left_absorb"; 

184 

5590  185 
Goal "A Int B = B Int A"; 
2891  186 
by (Blast_tac 1); 
923  187 
qed "Int_commute"; 
188 

5069  189 
Goal "A Int (B Int C) = B Int (A Int C)"; 
4609  190 
by (Blast_tac 1); 
191 
qed "Int_left_commute"; 

192 

5590  193 
Goal "(A Int B) Int C = A Int (B Int C)"; 
2891  194 
by (Blast_tac 1); 
923  195 
qed "Int_assoc"; 
196 

4609  197 
(*Intersection is an ACoperator*) 
7648  198 
bind_thms ("Int_ac", [Int_assoc, Int_left_absorb, Int_commute, Int_left_commute]); 
4609  199 

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

200 
Goal "B<=A ==> A Int B = B"; 
4662  201 
by (Blast_tac 1); 
202 
qed "Int_absorb1"; 

203 

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

204 
Goal "A<=B ==> A Int B = A"; 
4662  205 
by (Blast_tac 1); 
206 
qed "Int_absorb2"; 

207 

5069  208 
Goal "{} Int B = {}"; 
2891  209 
by (Blast_tac 1); 
923  210 
qed "Int_empty_left"; 
1531  211 
Addsimps[Int_empty_left]; 
923  212 

5069  213 
Goal "A Int {} = {}"; 
2891  214 
by (Blast_tac 1); 
923  215 
qed "Int_empty_right"; 
1531  216 
Addsimps[Int_empty_right]; 
217 

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

219 
by (blast_tac (claset() addSEs [equalityCE]) 1); 
3356  220 
qed "disjoint_eq_subset_Compl"; 
221 

7877  222 
Goal "(A Int B = {}) = (ALL x:A. ALL y:B. x ~= y)"; 
223 
by (Blast_tac 1); 

224 
qed "disjoint_iff_not_equal"; 

225 

5069  226 
Goal "UNIV Int B = B"; 
2891  227 
by (Blast_tac 1); 
1531  228 
qed "Int_UNIV_left"; 
229 
Addsimps[Int_UNIV_left]; 

230 

5069  231 
Goal "A Int UNIV = A"; 
2891  232 
by (Blast_tac 1); 
1531  233 
qed "Int_UNIV_right"; 
234 
Addsimps[Int_UNIV_right]; 

923  235 

5069  236 
Goal "A Int B = Inter{A,B}"; 
4634  237 
by (Blast_tac 1); 
238 
qed "Int_eq_Inter"; 

239 

5590  240 
Goal "A Int (B Un C) = (A Int B) Un (A Int C)"; 
2891  241 
by (Blast_tac 1); 
923  242 
qed "Int_Un_distrib"; 
243 

5590  244 
Goal "(B Un C) Int A = (B Int A) Un (C Int A)"; 
2891  245 
by (Blast_tac 1); 
1618  246 
qed "Int_Un_distrib2"; 
247 

5069  248 
Goal "(A Int B = UNIV) = (A = UNIV & B = UNIV)"; 
4089  249 
by (blast_tac (claset() addEs [equalityCE]) 1); 
1531  250 
qed "Int_UNIV"; 
251 
Addsimps[Int_UNIV]; 

252 

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

253 
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

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

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

256 

7713  257 
Goal "(x : A Int {x. P x}) = (x : A & P x)"; 
258 
by (Blast_tac 1); 

259 
qed "Int_Collect"; 

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

260 

1548  261 
section "Un"; 
923  262 

5069  263 
Goal "A Un A = A"; 
2891  264 
by (Blast_tac 1); 
923  265 
qed "Un_absorb"; 
1531  266 
Addsimps[Un_absorb]; 
923  267 

5069  268 
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

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

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

271 

5590  272 
Goal "A Un B = B Un A"; 
2891  273 
by (Blast_tac 1); 
923  274 
qed "Un_commute"; 
275 

5069  276 
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

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

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

279 

5590  280 
Goal "(A Un B) Un C = A Un (B Un C)"; 
2891  281 
by (Blast_tac 1); 
923  282 
qed "Un_assoc"; 
283 

4609  284 
(*Union is an ACoperator*) 
7648  285 
bind_thms ("Un_ac", [Un_assoc, Un_left_absorb, Un_commute, Un_left_commute]); 
4609  286 

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

287 
Goal "A<=B ==> A Un B = B"; 
4662  288 
by (Blast_tac 1); 
289 
qed "Un_absorb1"; 

290 

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

291 
Goal "B<=A ==> A Un B = A"; 
4662  292 
by (Blast_tac 1); 
293 
qed "Un_absorb2"; 

294 

5069  295 
Goal "{} Un B = B"; 
2891  296 
by (Blast_tac 1); 
923  297 
qed "Un_empty_left"; 
1531  298 
Addsimps[Un_empty_left]; 
923  299 

5069  300 
Goal "A Un {} = A"; 
2891  301 
by (Blast_tac 1); 
923  302 
qed "Un_empty_right"; 
1531  303 
Addsimps[Un_empty_right]; 
304 

5069  305 
Goal "UNIV Un B = UNIV"; 
2891  306 
by (Blast_tac 1); 
1531  307 
qed "Un_UNIV_left"; 
308 
Addsimps[Un_UNIV_left]; 

309 

5069  310 
Goal "A Un UNIV = UNIV"; 
2891  311 
by (Blast_tac 1); 
1531  312 
qed "Un_UNIV_right"; 
313 
Addsimps[Un_UNIV_right]; 

923  314 

5069  315 
Goal "A Un B = Union{A,B}"; 
4634  316 
by (Blast_tac 1); 
317 
qed "Un_eq_Union"; 

318 

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

322 
Addsimps[Un_insert_left]; 
923  323 

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

327 
Addsimps[Un_insert_right]; 
1917  328 

5069  329 
Goal "(insert a B) Int C = (if a:C then insert a (B Int C) \ 
5590  330 
\ else B Int C)"; 
4686  331 
by (Simp_tac 1); 
3356  332 
by (Blast_tac 1); 
333 
qed "Int_insert_left"; 

334 

5069  335 
Goal "A Int (insert a B) = (if a:A then insert a (A Int B) \ 
5590  336 
\ else A Int B)"; 
4686  337 
by (Simp_tac 1); 
3356  338 
by (Blast_tac 1); 
339 
qed "Int_insert_right"; 

340 

5590  341 
Goal "A Un (B Int C) = (A Un B) Int (A Un C)"; 
2891  342 
by (Blast_tac 1); 
923  343 
qed "Un_Int_distrib"; 
344 

5590  345 
Goal "(B Int C) Un A = (B Un A) Int (C Un A)"; 
4609  346 
by (Blast_tac 1); 
347 
qed "Un_Int_distrib2"; 

348 

5590  349 
Goal "(A Int B) Un (B Int C) Un (C Int A) = \ 
350 
\ (A Un B) Int (B Un C) Int (C Un A)"; 

2891  351 
by (Blast_tac 1); 
923  352 
qed "Un_Int_crazy"; 
353 

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

355 
by (blast_tac (claset() addSEs [equalityCE]) 1); 
923  356 
qed "subset_Un_eq"; 
357 

5069  358 
Goal "(A Un B = {}) = (A = {} & B = {})"; 
4089  359 
by (blast_tac (claset() addEs [equalityCE]) 1); 
923  360 
qed "Un_empty"; 
9098
3a0912a127ec
new theorem UN_empty; it and Un_empty inserted by AddIffs
paulson
parents:
9077
diff
changeset

361 
AddIffs[Un_empty]; 
923  362 

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

363 
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

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

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

366 

5331  367 
Goal "(A  B) Un (A Int B) = A"; 
368 
by (Blast_tac 1); 

369 
qed "Un_Diff_Int"; 

370 

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

371 

5931  372 
section "Set complement"; 
923  373 

8333  374 
Goal "A Int A = {}"; 
2891  375 
by (Blast_tac 1); 
923  376 
qed "Compl_disjoint"; 
8333  377 

378 
Goal "A Int A = {}"; 

379 
by (Blast_tac 1); 

380 
qed "Compl_disjoint2"; 

381 
Addsimps[Compl_disjoint, Compl_disjoint2]; 

923  382 

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

383 
Goal "A Un (A) = UNIV"; 
2891  384 
by (Blast_tac 1); 
923  385 
qed "Compl_partition"; 
386 

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

387 
Goal " (A) = (A:: 'a set)"; 
2891  388 
by (Blast_tac 1); 
923  389 
qed "double_complement"; 
1531  390 
Addsimps[double_complement]; 
923  391 

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

392 
Goal "(A Un B) = (A) Int (B)"; 
2891  393 
by (Blast_tac 1); 
923  394 
qed "Compl_Un"; 
395 

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

396 
Goal "(A Int B) = (A) Un (B)"; 
2891  397 
by (Blast_tac 1); 
923  398 
qed "Compl_Int"; 
399 

5490  400 
Goal "(UN x:A. B(x)) = (INT x:A. B(x))"; 
2891  401 
by (Blast_tac 1); 
923  402 
qed "Compl_UN"; 
403 

5490  404 
Goal "(INT x:A. B(x)) = (UN x:A. B(x))"; 
2891  405 
by (Blast_tac 1); 
923  406 
qed "Compl_INT"; 
407 

4615  408 
Addsimps [Compl_Un, Compl_Int, Compl_UN, Compl_INT]; 
409 

8121  410 
Goal "(A <= A) = (A = {})"; 
411 
by (Blast_tac 1); 

412 
qed "subset_Compl_self_eq"; 

413 

923  414 
(*Halmos, Naive Set Theory, page 16.*) 
5069  415 
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

416 
by (blast_tac (claset() addSEs [equalityCE]) 1); 
923  417 
qed "Un_Int_assoc_eq"; 
418 

8333  419 
Goal "UNIV = {}"; 
420 
by (Blast_tac 1); 

421 
qed "Compl_UNIV_eq"; 

422 

423 
Goal "{} = UNIV"; 

424 
by (Blast_tac 1); 

425 
qed "Compl_empty_eq"; 

426 

427 
Addsimps [Compl_UNIV_eq, Compl_empty_eq]; 

428 

9447  429 
Goal "(A <= B) = (B <= (A::'a set))"; 
430 
by(Blast_tac 1); 

431 
qed "Compl_subset_Compl_iff"; 

432 
AddIffs [Compl_subset_Compl_iff]; 

433 

434 
Goal "(A = B) = (A = (B::'a set))"; 

435 
by(Blast_tac 1); 

436 
qed "Compl_eq_Compl_iff"; 

437 
AddIffs [Compl_eq_Compl_iff]; 

438 

923  439 

1548  440 
section "Union"; 
923  441 

5069  442 
Goal "Union({}) = {}"; 
2891  443 
by (Blast_tac 1); 
923  444 
qed "Union_empty"; 
1531  445 
Addsimps[Union_empty]; 
446 

5069  447 
Goal "Union(UNIV) = UNIV"; 
2891  448 
by (Blast_tac 1); 
1531  449 
qed "Union_UNIV"; 
450 
Addsimps[Union_UNIV]; 

923  451 

5069  452 
Goal "Union(insert a B) = a Un Union(B)"; 
2891  453 
by (Blast_tac 1); 
923  454 
qed "Union_insert"; 
1531  455 
Addsimps[Union_insert]; 
923  456 

5069  457 
Goal "Union(A Un B) = Union(A) Un Union(B)"; 
2891  458 
by (Blast_tac 1); 
923  459 
qed "Union_Un_distrib"; 
1531  460 
Addsimps[Union_Un_distrib]; 
923  461 

5069  462 
Goal "Union(A Int B) <= Union(A) Int Union(B)"; 
2891  463 
by (Blast_tac 1); 
923  464 
qed "Union_Int_subset"; 
465 

9098
3a0912a127ec
new theorem UN_empty; it and Un_empty inserted by AddIffs
paulson
parents:
9077
diff
changeset

466 
Goal "(Union A = {}) = (ALL x:A. x={})"; 
3a0912a127ec
new theorem UN_empty; it and Un_empty inserted by AddIffs
paulson
parents:
9077
diff
changeset

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

468 
qed "Union_empty_conv"; 
4003  469 
AddIffs [Union_empty_conv]; 
470 

9206  471 
Goal "(Union(C) Int A = {}) = (ALL B:C. B Int A = {})"; 
4306
ddbe1a9722ab
Tidying and using equalityCE instead of the slower equalityE
paulson
parents:
4231
diff
changeset

472 
by (blast_tac (claset() addSEs [equalityCE]) 1); 
923  473 
qed "Union_disjoint"; 
474 

1548  475 
section "Inter"; 
476 

5069  477 
Goal "Inter({}) = UNIV"; 
2891  478 
by (Blast_tac 1); 
1531  479 
qed "Inter_empty"; 
480 
Addsimps[Inter_empty]; 

481 

5069  482 
Goal "Inter(UNIV) = {}"; 
2891  483 
by (Blast_tac 1); 
1531  484 
qed "Inter_UNIV"; 
485 
Addsimps[Inter_UNIV]; 

486 

5069  487 
Goal "Inter(insert a B) = a Int Inter(B)"; 
2891  488 
by (Blast_tac 1); 
1531  489 
qed "Inter_insert"; 
490 
Addsimps[Inter_insert]; 

491 

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

494 
qed "Inter_Un_subset"; 
1531  495 

5069  496 
Goal "Inter(A Un B) = Inter(A) Int Inter(B)"; 
2891  497 
by (Blast_tac 1); 
923  498 
qed "Inter_Un_distrib"; 
499 

1548  500 
section "UN and INT"; 
923  501 

502 
(*Basic identities*) 

503 

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

506 
qed "UN_empty"; 
1531  507 
Addsimps[UN_empty]; 
508 

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

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

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

513 

5069  514 
Goal "(UN x:A. {x}) = A"; 
4645  515 
by (Blast_tac 1); 
516 
qed "UN_singleton"; 

517 
Addsimps [UN_singleton]; 

518 

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

519 
Goal "k:I ==> A k Un (UN i:I. A i) = (UN i:I. A i)"; 
4634  520 
by (Blast_tac 1); 
521 
qed "UN_absorb"; 

522 

5069  523 
Goal "(INT x:{}. B x) = UNIV"; 
2891  524 
by (Blast_tac 1); 
1531  525 
qed "INT_empty"; 
526 
Addsimps[INT_empty]; 

527 

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

528 
Goal "k:I ==> A k Int (INT i:I. A i) = (INT i:I. A i)"; 
4634  529 
by (Blast_tac 1); 
530 
qed "INT_absorb"; 

531 

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

534 
qed "UN_insert"; 
1531  535 
Addsimps[UN_insert]; 
536 

5999  537 
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

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

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

540 

5069  541 
Goal "(UN x : (UN y:A. B y). C x) = (UN y:A. UN x: B y. C x)"; 
4771  542 
by (Blast_tac 1); 
543 
qed "UN_UN_flatten"; 

544 

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

545 
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

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

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

548 

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

549 
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

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

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

552 

5069  553 
Goal "(INT x:insert a A. B x) = B a Int INTER A B"; 
2891  554 
by (Blast_tac 1); 
1531  555 
qed "INT_insert"; 
556 
Addsimps[INT_insert]; 

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

557 

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

560 
qed "INT_Un"; 

561 

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

562 
Goal "u: A ==> (INT x:A. insert a (B x)) = insert a (INT x:A. B x)"; 
2891  563 
by (Blast_tac 1); 
2021  564 
qed "INT_insert_distrib"; 
565 

5069  566 
Goal "Union(B``A) = (UN x:A. B(x))"; 
2891  567 
by (Blast_tac 1); 
923  568 
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

569 
Addsimps [Union_image_eq]; 
923  570 

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

8176  573 
qed "image_Union"; 
6283  574 

5069  575 
Goal "Inter(B``A) = (INT x:A. B(x))"; 
2891  576 
by (Blast_tac 1); 
923  577 
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

578 
Addsimps [Inter_image_eq]; 
923  579 

8313
c7a87e79e9b1
replaced UN_constant, INT_constant by unconditional versions that rewrite
paulson
parents:
8176
diff
changeset

580 
Goal "(UN y:A. c) = (if A={} then {} else c)"; 
c7a87e79e9b1
replaced UN_constant, INT_constant by unconditional versions that rewrite
paulson
parents:
8176
diff
changeset

581 
by Auto_tac; 
923  582 
qed "UN_constant"; 
4159
4aff9b7e5597
UNIV now a constant; UNION1, INTER1 now translations and no longer have
paulson
parents:
4136
diff
changeset

583 
Addsimps[UN_constant]; 
923  584 

8313
c7a87e79e9b1
replaced UN_constant, INT_constant by unconditional versions that rewrite
paulson
parents:
8176
diff
changeset

585 
Goal "(INT y:A. c) = (if A={} then UNIV else c)"; 
c7a87e79e9b1
replaced UN_constant, INT_constant by unconditional versions that rewrite
paulson
parents:
8176
diff
changeset

586 
by Auto_tac; 
923  587 
qed "INT_constant"; 
4159
4aff9b7e5597
UNIV now a constant; UNION1, INTER1 now translations and no longer have
paulson
parents:
4136
diff
changeset

588 
Addsimps[INT_constant]; 
923  589 

9206  590 
Goal "(UN x:A. B(x)) = Union({Y. EX x:A. Y=B(x)})"; 
2891  591 
by (Blast_tac 1); 
923  592 
qed "UN_eq"; 
593 

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

9206  595 
Goal "(INT x:A. B(x)) = Inter({Y. EX x:A. Y=B(x)})"; 
2891  596 
by (Blast_tac 1); 
923  597 
qed "INT_eq"; 
598 

9098
3a0912a127ec
new theorem UN_empty; it and Un_empty inserted by AddIffs
paulson
parents:
9077
diff
changeset

599 
Goal "(UNION A B = {}) = (ALL x:A. B x = {})"; 
3a0912a127ec
new theorem UN_empty; it and Un_empty inserted by AddIffs
paulson
parents:
9077
diff
changeset

600 
by Auto_tac; 
9312  601 
qed "UN_empty3"; 
602 
AddIffs [UN_empty3]; 

9098
3a0912a127ec
new theorem UN_empty; it and Un_empty inserted by AddIffs
paulson
parents:
9077
diff
changeset

603 

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

604 

923  605 
(*Distributive laws...*) 
606 

5069  607 
Goal "A Int Union(B) = (UN C:B. A Int C)"; 
2891  608 
by (Blast_tac 1); 
923  609 
qed "Int_Union"; 
610 

5069  611 
Goal "Union(B) Int A = (UN C:B. C Int A)"; 
4674  612 
by (Blast_tac 1); 
613 
qed "Int_Union2"; 

614 

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

615 
(* Devlin, Fundamentals of Contemporary Set Theory, page 12, exercise 5: 
923  616 
Union of a family of unions **) 
5069  617 
Goal "(UN x:C. A(x) Un B(x)) = Union(A``C) Un Union(B``C)"; 
2891  618 
by (Blast_tac 1); 
923  619 
qed "Un_Union_image"; 
620 

621 
(*Equivalent version*) 

5069  622 
Goal "(UN i:I. A(i) Un B(i)) = (UN i:I. A(i)) Un (UN i:I. B(i))"; 
2891  623 
by (Blast_tac 1); 
923  624 
qed "UN_Un_distrib"; 
625 

5069  626 
Goal "A Un Inter(B) = (INT C:B. A Un C)"; 
2891  627 
by (Blast_tac 1); 
923  628 
qed "Un_Inter"; 
629 

5069  630 
Goal "(INT x:C. A(x) Int B(x)) = Inter(A``C) Int Inter(B``C)"; 
2891  631 
by (Blast_tac 1); 
923  632 
qed "Int_Inter_image"; 
633 

634 
(*Equivalent version*) 

5069  635 
Goal "(INT i:I. A(i) Int B(i)) = (INT i:I. A(i)) Int (INT i:I. B(i))"; 
2891  636 
by (Blast_tac 1); 
923  637 
qed "INT_Int_distrib"; 
638 

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

5069  640 
Goal "B Int (UN i:I. A(i)) = (UN i:I. B Int A(i))"; 
2891  641 
by (Blast_tac 1); 
923  642 
qed "Int_UN_distrib"; 
643 

5069  644 
Goal "B Un (INT i:I. A(i)) = (INT i:I. B Un A(i))"; 
2891  645 
by (Blast_tac 1); 
923  646 
qed "Un_INT_distrib"; 
647 

5278  648 
Goal "(UN i:I. A(i)) Int (UN j:J. B(j)) = (UN i:I. UN j:J. A(i) Int B(j))"; 
2891  649 
by (Blast_tac 1); 
923  650 
qed "Int_UN_distrib2"; 
651 

5278  652 
Goal "(INT i:I. A(i)) Un (INT j:J. B(j)) = (INT i:I. INT j:J. A(i) Un B(j))"; 
2891  653 
by (Blast_tac 1); 
923  654 
qed "Un_INT_distrib2"; 
655 

2512  656 

657 
section"Bounded quantifiers"; 

658 

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

2512  661 

5069  662 
Goal "(ALL x:A Un B. P x) = ((ALL x:A. P x) & (ALL x:B. P x))"; 
2891  663 
by (Blast_tac 1); 
2519  664 
qed "ball_Un"; 
665 

5069  666 
Goal "(EX x:A Un B. P x) = ((EX x:A. P x)  (EX x:B. P x))"; 
2891  667 
by (Blast_tac 1); 
2519  668 
qed "bex_Un"; 
2512  669 

5069  670 
Goal "(ALL z: UNION A B. P z) = (ALL x:A. ALL z:B x. P z)"; 
4771  671 
by (Blast_tac 1); 
672 
qed "ball_UN"; 

673 

5069  674 
Goal "(EX z: UNION A B. P z) = (EX x:A. EX z:B x. P z)"; 
4771  675 
by (Blast_tac 1); 
676 
qed "bex_UN"; 

677 

2512  678 

1548  679 
section ""; 
923  680 

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

681 
Goal "AB = A Int (B)"; 
4609  682 
by (Blast_tac 1); 
4662  683 
qed "Diff_eq"; 
4609  684 

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

687 
qed "Diff_eq_empty_iff"; 

688 
Addsimps[Diff_eq_empty_iff]; 

689 

5069  690 
Goal "AA = {}"; 
2891  691 
by (Blast_tac 1); 
923  692 
qed "Diff_cancel"; 
1531  693 
Addsimps[Diff_cancel]; 
923  694 

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

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

698 

5069  699 
Goal "{}A = {}"; 
2891  700 
by (Blast_tac 1); 
923  701 
qed "empty_Diff"; 
1531  702 
Addsimps[empty_Diff]; 
923  703 

5069  704 
Goal "A{} = A"; 
2891  705 
by (Blast_tac 1); 
923  706 
qed "Diff_empty"; 
1531  707 
Addsimps[Diff_empty]; 
708 

5069  709 
Goal "AUNIV = {}"; 
2891  710 
by (Blast_tac 1); 
1531  711 
qed "Diff_UNIV"; 
712 
Addsimps[Diff_UNIV]; 

713 

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

714 
Goal "x~:A ==> A  insert x B = AB"; 
2891  715 
by (Blast_tac 1); 
1531  716 
qed "Diff_insert0"; 
717 
Addsimps [Diff_insert0]; 

923  718 

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

5069  720 
Goal "A  insert a B = A  B  {a}"; 
2891  721 
by (Blast_tac 1); 
923  722 
qed "Diff_insert"; 
723 

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

5069  725 
Goal "A  insert a B = A  {a}  B"; 
2891  726 
by (Blast_tac 1); 
923  727 
qed "Diff_insert2"; 
728 

5069  729 
Goal "insert x A  B = (if x:B then AB else insert x (AB))"; 
4686  730 
by (Simp_tac 1); 
2891  731 
by (Blast_tac 1); 
1531  732 
qed "insert_Diff_if"; 
733 

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

734 
Goal "x:B ==> insert x A  B = AB"; 
2891  735 
by (Blast_tac 1); 
1531  736 
qed "insert_Diff1"; 
737 
Addsimps [insert_Diff1]; 

738 

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

739 
Goal "a:A ==> insert a (A{a}) = A"; 
2922  740 
by (Blast_tac 1); 
923  741 
qed "insert_Diff"; 
742 

7824
1a85ba81d019
new default simprule Collect_const and new them Diff_insert_absorb
paulson
parents:
7713
diff
changeset

743 
Goal "x ~: A ==> (insert x A)  {x} = A"; 
1a85ba81d019
new default simprule Collect_const and new them Diff_insert_absorb
paulson
parents:
7713
diff
changeset

744 
by Auto_tac; 
1a85ba81d019
new default simprule Collect_const and new them Diff_insert_absorb
paulson
parents:
7713
diff
changeset

745 
qed "Diff_insert_absorb"; 
1a85ba81d019
new default simprule Collect_const and new them Diff_insert_absorb
paulson
parents:
7713
diff
changeset

746 

5069  747 
Goal "A Int (BA) = {}"; 
2891  748 
by (Blast_tac 1); 
923  749 
qed "Diff_disjoint"; 
1531  750 
Addsimps[Diff_disjoint]; 
923  751 

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

752 
Goal "A<=B ==> A Un (BA) = B"; 
2891  753 
by (Blast_tac 1); 
923  754 
qed "Diff_partition"; 
755 

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

756 
Goal "[ A<=B; B<= C ] ==> (B  (C  A)) = (A :: 'a set)"; 
2891  757 
by (Blast_tac 1); 
923  758 
qed "double_diff"; 
759 

5069  760 
Goal "A Un (BA) = A Un B"; 
4645  761 
by (Blast_tac 1); 
762 
qed "Un_Diff_cancel"; 

763 

5069  764 
Goal "(BA) Un A = B Un A"; 
4645  765 
by (Blast_tac 1); 
766 
qed "Un_Diff_cancel2"; 

767 

768 
Addsimps [Un_Diff_cancel, Un_Diff_cancel2]; 

769 

5069  770 
Goal "A  (B Un C) = (AB) Int (AC)"; 
2891  771 
by (Blast_tac 1); 
923  772 
qed "Diff_Un"; 
773 

5069  774 
Goal "A  (B Int C) = (AB) Un (AC)"; 
2891  775 
by (Blast_tac 1); 
923  776 
qed "Diff_Int"; 
777 

5069  778 
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

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

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

781 

5069  782 
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

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

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

785 

5069  786 
Goal "C Int (AB) = (C Int A)  (C Int B)"; 
4748  787 
by (Blast_tac 1); 
788 
qed "Diff_Int_distrib"; 

789 

5069  790 
Goal "(AB) Int C = (A Int C)  (B Int C)"; 
4645  791 
by (Blast_tac 1); 
4748  792 
qed "Diff_Int_distrib2"; 
4645  793 

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

794 
Goal "A  ( B) = A Int B"; 
5632  795 
by Auto_tac; 
796 
qed "Diff_Compl"; 

797 
Addsimps [Diff_Compl]; 

798 

9608  799 
Goal " (AB) = A Un B"; 
800 
by (blast_tac (claset() addIs []) 1); 

801 
qed "Compl_Diff_eq"; 

802 
Addsimps [Compl_Diff_eq]; 

803 

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

804 

5238  805 
section "Quantification over type \"bool\""; 
806 

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

808 
by Auto_tac; 

809 
by (case_tac "b" 1); 

810 
by Auto_tac; 

811 
qed "all_bool_eq"; 

812 

5762  813 
bind_thm ("bool_induct", conjI RS (all_bool_eq RS iffD2) RS spec); 
814 

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

817 
by (case_tac "b" 1); 

818 
by Auto_tac; 

819 
qed "ex_bool_eq"; 

820 

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

8026  822 
by (auto_tac(claset(), simpset() addsimps [split_if_mem2])); 
5238  823 
qed "Un_eq_UN"; 
824 

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

826 
by Auto_tac; 

827 
by (case_tac "b" 1); 

828 
by Auto_tac; 

829 
qed "UN_bool_eq"; 

830 

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

832 
by Auto_tac; 

833 
by (case_tac "b" 1); 

834 
by Auto_tac; 

835 
qed "INT_bool_eq"; 

836 

837 

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

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

839 

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

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

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

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

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

844 

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

845 
Goal "Pow (insert a A) = Pow A Un (insert a `` Pow A)"; 
10234  846 
by (blast_tac (claset() addIs [inst "x" "?u{a}" image_eqI]) 1); 
6292
e50e1142dd06
new results e.g. about Pow; new simprules Union_image_eq, Inter_image_eq
paulson
parents:
6283
diff
changeset

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

848 

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

849 
Goal "Pow ( A) = {B B. A: Pow B}"; 
10234  850 
by (blast_tac (claset() addIs [inst "x" " ?u" exI]) 1); 
6292
e50e1142dd06
new results e.g. about Pow; new simprules Union_image_eq, Inter_image_eq
paulson
parents:
6283
diff
changeset

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

852 

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

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

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

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

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

857 

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

858 
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

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

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

861 

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

862 
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

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

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

865 

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

866 
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

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

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

869 

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

870 
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

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

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

873 

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

874 
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

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

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

877 

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

878 
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

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

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

881 

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

882 
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

883 

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

884 

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

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

886 

5069  887 
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

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

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

890 

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

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

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

894 

5069  895 
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

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

897 
qed "subset_iff_psubset_eq"; 
2021  898 

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

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

903 

6007  904 

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

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

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

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

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

909 

2021  910 

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

912 
local 

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

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

916 
["!!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

917 
"!!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

918 
"!!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

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

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

921 
"(UN x:C. A x  B) = ((UN x:C. A x)  B)", 
4231  922 
"(UN x:C. A  B x) = (A  (INT x:C. B x))", 
7914  923 
"(UN x: Union A. B x) = (UN y:A. UN x:y. B x)", 
924 
"(UN z: UNION A B. C z) = (UN x:A. UN z: B(x). C z)", 

4231  925 
"(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

926 

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

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

928 
["!!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

929 
"!!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

930 
"!!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

931 
"!!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

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

933 
"(INT x:C. A x Un B) = ((INT x:C. A x) Un B)", 
4231  934 
"(INT x:C. A Un B x) = (A Un (INT x:C. B x))", 
7914  935 
"(INT x: Union A. B x) = (INT y:A. INT x:y. B x)", 
936 
"(INT z: UNION A B. C z) = (INT x:A. INT z: B(x). C z)", 

4231  937 
"(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

938 

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

939 

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

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

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

942 
"(ALL x:A. P  Q x) = (P  (ALL x:A. Q x))", 
3422  943 
"(ALL x:A. P > Q x) = (P > (ALL x:A. Q x))", 
944 
"(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

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

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

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

949 
"(ALL x: UNION A B. P x) = (ALL a:A. ALL x: B a. P x)", 
3860  950 
"(ALL x:Collect Q. P x) = (ALL x. Q x > P x)", 
951 
"(ALL x:f``A. P x) = (ALL x:A. P(f x))", 

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

953 

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

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

955 
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

956 

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

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

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

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

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

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

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

964 
"(EX x: UNION A B. P x) = (EX a:A. EX x: B a. P x)", 
3860  965 
"(EX x:Collect Q. P x) = (EX x. Q x & P x)", 
966 
"(EX x:f``A. P x) = (EX x:A. P(f x))", 

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

968 

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

970 
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

971 

2021  972 
end; 
973 

7648  974 
bind_thms ("UN_simps", UN_simps); 
975 
bind_thms ("INT_simps", INT_simps); 

976 
bind_thms ("ball_simps", ball_simps); 

977 
bind_thms ("bex_simps", bex_simps); 

978 
bind_thm ("ball_conj_distrib", ball_conj_distrib); 

979 
bind_thm ("bex_disj_distrib", bex_disj_distrib); 

980 

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

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