author  wenzelm 
Wed, 27 Mar 2013 16:38:25 +0100  
changeset 51553  63327f679cff 
parent 46821  ff6b0c1087f2 
child 58860  fee7cfa69c50 
permissions  rwrr 
35762  1 
(* Title: ZF/equalities.thy 
13165  2 
Author: Lawrence C Paulson, Cambridge University Computer Laboratory 
3 
Copyright 1992 University of Cambridge 

4 
*) 

5 

13356  6 
header{*Basic Equalities and Inclusions*} 
7 

16417  8 
theory equalities imports pair begin 
13168
afcbca3498b0
converted domrange to Isar and merged with equalities
paulson
parents:
13165
diff
changeset

9 

13356  10 
text{*These cover union, intersection, converse, domain, range, etc. Philippe 
11 
de Groote proved many of the inclusions.*} 

12 

46820  13 
lemma in_mono: "A\<subseteq>B ==> x\<in>A \<longrightarrow> x\<in>B" 
13259  14 
by blast 
15 

13174  16 
lemma the_eq_0 [simp]: "(THE x. False) = 0" 
17 
by (blast intro: the_0) 

13168
afcbca3498b0
converted domrange to Isar and merged with equalities
paulson
parents:
13165
diff
changeset

18 

13356  19 
subsection{*Bounded Quantifiers*} 
46820  20 
text {* \medskip 
13178  21 

22 
The following are not added to the default simpset because 

13356  23 
(a) they duplicate the body and (b) there are no similar rules for @{text Int}.*} 
13178  24 

46821
ff6b0c1087f2
Using mathematical notation for <> and cardinal arithmetic
paulson
parents:
46820
diff
changeset

25 
lemma ball_Un: "(\<forall>x \<in> A\<union>B. P(x)) \<longleftrightarrow> (\<forall>x \<in> A. P(x)) & (\<forall>x \<in> B. P(x))"; 
13178  26 
by blast 
27 

46821
ff6b0c1087f2
Using mathematical notation for <> and cardinal arithmetic
paulson
parents:
46820
diff
changeset

28 
lemma bex_Un: "(\<exists>x \<in> A\<union>B. P(x)) \<longleftrightarrow> (\<exists>x \<in> A. P(x))  (\<exists>x \<in> B. P(x))"; 
13178  29 
by blast 
30 

46821
ff6b0c1087f2
Using mathematical notation for <> and cardinal arithmetic
paulson
parents:
46820
diff
changeset

31 
lemma ball_UN: "(\<forall>z \<in> (\<Union>x\<in>A. B(x)). P(z)) \<longleftrightarrow> (\<forall>x\<in>A. \<forall>z \<in> B(x). P(z))" 
13178  32 
by blast 
33 

46821
ff6b0c1087f2
Using mathematical notation for <> and cardinal arithmetic
paulson
parents:
46820
diff
changeset

34 
lemma bex_UN: "(\<exists>z \<in> (\<Union>x\<in>A. B(x)). P(z)) \<longleftrightarrow> (\<exists>x\<in>A. \<exists>z\<in>B(x). P(z))" 
13178  35 
by blast 
36 

13356  37 
subsection{*Converse of a Relation*} 
13168
afcbca3498b0
converted domrange to Isar and merged with equalities
paulson
parents:
13165
diff
changeset

38 

46821
ff6b0c1087f2
Using mathematical notation for <> and cardinal arithmetic
paulson
parents:
46820
diff
changeset

39 
lemma converse_iff [simp]: "<a,b>\<in> converse(r) \<longleftrightarrow> <b,a>\<in>r" 
13169  40 
by (unfold converse_def, blast) 
13168
afcbca3498b0
converted domrange to Isar and merged with equalities
paulson
parents:
13165
diff
changeset

41 

14095
a1ba833d6b61
Changed many Intersection rules from i:I to I~=0 to avoid introducing a new
paulson
parents:
14084
diff
changeset

42 
lemma converseI [intro!]: "<a,b>\<in>r ==> <b,a>\<in>converse(r)" 
13169  43 
by (unfold converse_def, blast) 
13168
afcbca3498b0
converted domrange to Isar and merged with equalities
paulson
parents:
13165
diff
changeset

44 

14095
a1ba833d6b61
Changed many Intersection rules from i:I to I~=0 to avoid introducing a new
paulson
parents:
14084
diff
changeset

45 
lemma converseD: "<a,b> \<in> converse(r) ==> <b,a> \<in> r" 
13169  46 
by (unfold converse_def, blast) 
13168
afcbca3498b0
converted domrange to Isar and merged with equalities
paulson
parents:
13165
diff
changeset

47 

afcbca3498b0
converted domrange to Isar and merged with equalities
paulson
parents:
13165
diff
changeset

48 
lemma converseE [elim!]: 
46820  49 
"[ yx \<in> converse(r); 
14095
a1ba833d6b61
Changed many Intersection rules from i:I to I~=0 to avoid introducing a new
paulson
parents:
14084
diff
changeset

50 
!!x y. [ yx=<y,x>; <x,y>\<in>r ] ==> P ] 
13168
afcbca3498b0
converted domrange to Isar and merged with equalities
paulson
parents:
13165
diff
changeset

51 
==> P" 
46820  52 
by (unfold converse_def, blast) 
13168
afcbca3498b0
converted domrange to Isar and merged with equalities
paulson
parents:
13165
diff
changeset

53 

14095
a1ba833d6b61
Changed many Intersection rules from i:I to I~=0 to avoid introducing a new
paulson
parents:
14084
diff
changeset

54 
lemma converse_converse: "r\<subseteq>Sigma(A,B) ==> converse(converse(r)) = r" 
13169  55 
by blast 
13168
afcbca3498b0
converted domrange to Isar and merged with equalities
paulson
parents:
13165
diff
changeset

56 

14095
a1ba833d6b61
Changed many Intersection rules from i:I to I~=0 to avoid introducing a new
paulson
parents:
14084
diff
changeset

57 
lemma converse_type: "r\<subseteq>A*B ==> converse(r)\<subseteq>B*A" 
13169  58 
by blast 
13168
afcbca3498b0
converted domrange to Isar and merged with equalities
paulson
parents:
13165
diff
changeset

59 

afcbca3498b0
converted domrange to Isar and merged with equalities
paulson
parents:
13165
diff
changeset

60 
lemma converse_prod [simp]: "converse(A*B) = B*A" 
13169  61 
by blast 
13168
afcbca3498b0
converted domrange to Isar and merged with equalities
paulson
parents:
13165
diff
changeset

62 

afcbca3498b0
converted domrange to Isar and merged with equalities
paulson
parents:
13165
diff
changeset

63 
lemma converse_empty [simp]: "converse(0) = 0" 
13169  64 
by blast 
13168
afcbca3498b0
converted domrange to Isar and merged with equalities
paulson
parents:
13165
diff
changeset

65 

13174  66 
lemma converse_subset_iff: 
46821
ff6b0c1087f2
Using mathematical notation for <> and cardinal arithmetic
paulson
parents:
46820
diff
changeset

67 
"A \<subseteq> Sigma(X,Y) ==> converse(A) \<subseteq> converse(B) \<longleftrightarrow> A \<subseteq> B" 
13169  68 
by blast 
13168
afcbca3498b0
converted domrange to Isar and merged with equalities
paulson
parents:
13165
diff
changeset

69 

afcbca3498b0
converted domrange to Isar and merged with equalities
paulson
parents:
13165
diff
changeset

70 

13356  71 
subsection{*Finite Set Constructions Using @{term cons}*} 
13168
afcbca3498b0
converted domrange to Isar and merged with equalities
paulson
parents:
13165
diff
changeset

72 

14095
a1ba833d6b61
Changed many Intersection rules from i:I to I~=0 to avoid introducing a new
paulson
parents:
14084
diff
changeset

73 
lemma cons_subsetI: "[ a\<in>C; B\<subseteq>C ] ==> cons(a,B) \<subseteq> C" 
13169  74 
by blast 
13168
afcbca3498b0
converted domrange to Isar and merged with equalities
paulson
parents:
13165
diff
changeset

75 

14095
a1ba833d6b61
Changed many Intersection rules from i:I to I~=0 to avoid introducing a new
paulson
parents:
14084
diff
changeset

76 
lemma subset_consI: "B \<subseteq> cons(a,B)" 
13169  77 
by blast 
13168
afcbca3498b0
converted domrange to Isar and merged with equalities
paulson
parents:
13165
diff
changeset

78 

46821
ff6b0c1087f2
Using mathematical notation for <> and cardinal arithmetic
paulson
parents:
46820
diff
changeset

79 
lemma cons_subset_iff [iff]: "cons(a,B)\<subseteq>C \<longleftrightarrow> a\<in>C & B\<subseteq>C" 
13169  80 
by blast 
13168
afcbca3498b0
converted domrange to Isar and merged with equalities
paulson
parents:
13165
diff
changeset

81 

46820  82 
(*A safe special case of subset elimination, adding no new variables 
14095
a1ba833d6b61
Changed many Intersection rules from i:I to I~=0 to avoid introducing a new
paulson
parents:
14084
diff
changeset

83 
[ cons(a,B) \<subseteq> C; [ a \<in> C; B \<subseteq> C ] ==> R ] ==> R *) 
45602  84 
lemmas cons_subsetE = cons_subset_iff [THEN iffD1, THEN conjE] 
13168
afcbca3498b0
converted domrange to Isar and merged with equalities
paulson
parents:
13165
diff
changeset

85 

46821
ff6b0c1087f2
Using mathematical notation for <> and cardinal arithmetic
paulson
parents:
46820
diff
changeset

86 
lemma subset_empty_iff: "A\<subseteq>0 \<longleftrightarrow> A=0" 
13168
afcbca3498b0
converted domrange to Isar and merged with equalities
paulson
parents:
13165
diff
changeset

87 
by blast 
afcbca3498b0
converted domrange to Isar and merged with equalities
paulson
parents:
13165
diff
changeset

88 

46821
ff6b0c1087f2
Using mathematical notation for <> and cardinal arithmetic
paulson
parents:
46820
diff
changeset

89 
lemma subset_cons_iff: "C\<subseteq>cons(a,B) \<longleftrightarrow> C\<subseteq>B  (a\<in>C & C{a} \<subseteq> B)" 
13169  90 
by blast 
13168
afcbca3498b0
converted domrange to Isar and merged with equalities
paulson
parents:
13165
diff
changeset

91 

13165  92 
(* cons_def refers to Upair; reversing the equality LOOPS in rewriting!*) 
46820  93 
lemma cons_eq: "{a} \<union> B = cons(a,B)" 
13165  94 
by blast 
95 

96 
lemma cons_commute: "cons(a, cons(b, C)) = cons(b, cons(a, C))" 

97 
by blast 

98 

99 
lemma cons_absorb: "a: B ==> cons(a,B) = B" 

100 
by blast 

101 

102 
lemma cons_Diff: "a: B ==> cons(a, B{a}) = B" 

103 
by blast 

104 

46820  105 
lemma Diff_cons_eq: "cons(a,B)  C = (if a\<in>C then BC else cons(a,BC))" 
14071  106 
by auto 
107 

13615
449a70d88b38
Numerous cosmetic changes, prompted by the new simplifier
paulson
parents:
13611
diff
changeset

108 
lemma equal_singleton [rule_format]: "[ a: C; \<forall>y\<in>C. y=b ] ==> C = {b}" 
13165  109 
by blast 
110 

13172  111 
lemma [simp]: "cons(a,cons(a,B)) = cons(a,B)" 
112 
by blast 

13165  113 

13259  114 
(** singletons **) 
115 

14095
a1ba833d6b61
Changed many Intersection rules from i:I to I~=0 to avoid introducing a new
paulson
parents:
14084
diff
changeset

116 
lemma singleton_subsetI: "a\<in>C ==> {a} \<subseteq> C" 
13259  117 
by blast 
118 

14095
a1ba833d6b61
Changed many Intersection rules from i:I to I~=0 to avoid introducing a new
paulson
parents:
14084
diff
changeset

119 
lemma singleton_subsetD: "{a} \<subseteq> C ==> a\<in>C" 
13259  120 
by blast 
121 

122 

13356  123 
(** succ **) 
13259  124 

14095
a1ba833d6b61
Changed many Intersection rules from i:I to I~=0 to avoid introducing a new
paulson
parents:
14084
diff
changeset

125 
lemma subset_succI: "i \<subseteq> succ(i)" 
13259  126 
by blast 
127 

46820  128 
(*But if j is an ordinal or is transitive, then @{term"i\<in>j"} implies @{term"i\<subseteq>j"}! 
129 
See @{text"Ord_succ_subsetI}*) 

14095
a1ba833d6b61
Changed many Intersection rules from i:I to I~=0 to avoid introducing a new
paulson
parents:
14084
diff
changeset

130 
lemma succ_subsetI: "[ i\<in>j; i\<subseteq>j ] ==> succ(i)\<subseteq>j" 
13259  131 
by (unfold succ_def, blast) 
13165  132 

13259  133 
lemma succ_subsetE: 
14095
a1ba833d6b61
Changed many Intersection rules from i:I to I~=0 to avoid introducing a new
paulson
parents:
14084
diff
changeset

134 
"[ succ(i) \<subseteq> j; [ i\<in>j; i\<subseteq>j ] ==> P ] ==> P" 
46820  135 
by (unfold succ_def, blast) 
13259  136 

46821
ff6b0c1087f2
Using mathematical notation for <> and cardinal arithmetic
paulson
parents:
46820
diff
changeset

137 
lemma succ_subset_iff: "succ(a) \<subseteq> B \<longleftrightarrow> (a \<subseteq> B & a \<in> B)" 
13259  138 
by (unfold succ_def, blast) 
139 

140 

13356  141 
subsection{*Binary Intersection*} 
13259  142 

143 
(** Intersection is the greatest lower bound of two sets **) 

144 

46821
ff6b0c1087f2
Using mathematical notation for <> and cardinal arithmetic
paulson
parents:
46820
diff
changeset

145 
lemma Int_subset_iff: "C \<subseteq> A \<inter> B \<longleftrightarrow> C \<subseteq> A & C \<subseteq> B" 
13259  146 
by blast 
147 

46820  148 
lemma Int_lower1: "A \<inter> B \<subseteq> A" 
13259  149 
by blast 
150 

46820  151 
lemma Int_lower2: "A \<inter> B \<subseteq> B" 
13259  152 
by blast 
153 

46820  154 
lemma Int_greatest: "[ C\<subseteq>A; C\<subseteq>B ] ==> C \<subseteq> A \<inter> B" 
13259  155 
by blast 
156 

46820  157 
lemma Int_cons: "cons(a,B) \<inter> C \<subseteq> cons(a, B \<inter> C)" 
13165  158 
by blast 
159 

46820  160 
lemma Int_absorb [simp]: "A \<inter> A = A" 
13165  161 
by blast 
162 

46820  163 
lemma Int_left_absorb: "A \<inter> (A \<inter> B) = A \<inter> B" 
13165  164 
by blast 
165 

46820  166 
lemma Int_commute: "A \<inter> B = B \<inter> A" 
13165  167 
by blast 
168 

46820  169 
lemma Int_left_commute: "A \<inter> (B \<inter> C) = B \<inter> (A \<inter> C)" 
13165  170 
by blast 
171 

46820  172 
lemma Int_assoc: "(A \<inter> B) \<inter> C = A \<inter> (B \<inter> C)" 
13165  173 
by blast 
174 

175 
(*Intersection is an ACoperator*) 

176 
lemmas Int_ac= Int_assoc Int_left_absorb Int_commute Int_left_commute 

177 

14046  178 
lemma Int_absorb1: "B \<subseteq> A ==> A \<inter> B = B" 
179 
by blast 

180 

181 
lemma Int_absorb2: "A \<subseteq> B ==> A \<inter> B = A" 

182 
by blast 

183 

46820  184 
lemma Int_Un_distrib: "A \<inter> (B \<union> C) = (A \<inter> B) \<union> (A \<inter> C)" 
13165  185 
by blast 
186 

46820  187 
lemma Int_Un_distrib2: "(B \<union> C) \<inter> A = (B \<inter> A) \<union> (C \<inter> A)" 
13165  188 
by blast 
189 

46821
ff6b0c1087f2
Using mathematical notation for <> and cardinal arithmetic
paulson
parents:
46820
diff
changeset

190 
lemma subset_Int_iff: "A\<subseteq>B \<longleftrightarrow> A \<inter> B = A" 
13165  191 
by (blast elim!: equalityE) 
192 

46821
ff6b0c1087f2
Using mathematical notation for <> and cardinal arithmetic
paulson
parents:
46820
diff
changeset

193 
lemma subset_Int_iff2: "A\<subseteq>B \<longleftrightarrow> B \<inter> A = A" 
13165  194 
by (blast elim!: equalityE) 
195 

46820  196 
lemma Int_Diff_eq: "C\<subseteq>A ==> (AB) \<inter> C = CB" 
13165  197 
by blast 
198 

14071  199 
lemma Int_cons_left: 
46820  200 
"cons(a,A) \<inter> B = (if a \<in> B then cons(a, A \<inter> B) else A \<inter> B)" 
14071  201 
by auto 
202 

203 
lemma Int_cons_right: 

46820  204 
"A \<inter> cons(a, B) = (if a \<in> A then cons(a, A \<inter> B) else A \<inter> B)" 
14071  205 
by auto 
206 

14076  207 
lemma cons_Int_distrib: "cons(x, A \<inter> B) = cons(x, A) \<inter> cons(x, B)" 
208 
by auto 

209 

13356  210 
subsection{*Binary Union*} 
13259  211 

212 
(** Union is the least upper bound of two sets *) 

213 

46821
ff6b0c1087f2
Using mathematical notation for <> and cardinal arithmetic
paulson
parents:
46820
diff
changeset

214 
lemma Un_subset_iff: "A \<union> B \<subseteq> C \<longleftrightarrow> A \<subseteq> C & B \<subseteq> C" 
13259  215 
by blast 
216 

46820  217 
lemma Un_upper1: "A \<subseteq> A \<union> B" 
13259  218 
by blast 
219 

46820  220 
lemma Un_upper2: "B \<subseteq> A \<union> B" 
13259  221 
by blast 
222 

46820  223 
lemma Un_least: "[ A\<subseteq>C; B\<subseteq>C ] ==> A \<union> B \<subseteq> C" 
13259  224 
by blast 
13165  225 

46820  226 
lemma Un_cons: "cons(a,B) \<union> C = cons(a, B \<union> C)" 
13165  227 
by blast 
228 

46820  229 
lemma Un_absorb [simp]: "A \<union> A = A" 
13165  230 
by blast 
231 

46820  232 
lemma Un_left_absorb: "A \<union> (A \<union> B) = A \<union> B" 
13165  233 
by blast 
234 

46820  235 
lemma Un_commute: "A \<union> B = B \<union> A" 
13165  236 
by blast 
237 

46820  238 
lemma Un_left_commute: "A \<union> (B \<union> C) = B \<union> (A \<union> C)" 
13165  239 
by blast 
240 

46820  241 
lemma Un_assoc: "(A \<union> B) \<union> C = A \<union> (B \<union> C)" 
13165  242 
by blast 
243 

244 
(*Union is an ACoperator*) 

245 
lemmas Un_ac = Un_assoc Un_left_absorb Un_commute Un_left_commute 

246 

14046  247 
lemma Un_absorb1: "A \<subseteq> B ==> A \<union> B = B" 
248 
by blast 

249 

250 
lemma Un_absorb2: "B \<subseteq> A ==> A \<union> B = A" 

251 
by blast 

252 

46820  253 
lemma Un_Int_distrib: "(A \<inter> B) \<union> C = (A \<union> C) \<inter> (B \<union> C)" 
13165  254 
by blast 
255 

46821
ff6b0c1087f2
Using mathematical notation for <> and cardinal arithmetic
paulson
parents:
46820
diff
changeset

256 
lemma subset_Un_iff: "A\<subseteq>B \<longleftrightarrow> A \<union> B = B" 
13165  257 
by (blast elim!: equalityE) 
258 

46821
ff6b0c1087f2
Using mathematical notation for <> and cardinal arithmetic
paulson
parents:
46820
diff
changeset

259 
lemma subset_Un_iff2: "A\<subseteq>B \<longleftrightarrow> B \<union> A = B" 
13165  260 
by (blast elim!: equalityE) 
261 

46821
ff6b0c1087f2
Using mathematical notation for <> and cardinal arithmetic
paulson
parents:
46820
diff
changeset

262 
lemma Un_empty [iff]: "(A \<union> B = 0) \<longleftrightarrow> (A = 0 & B = 0)" 
13165  263 
by blast 
264 

46820  265 
lemma Un_eq_Union: "A \<union> B = \<Union>({A, B})" 
13165  266 
by blast 
267 

13356  268 
subsection{*Set Difference*} 
13259  269 

14095
a1ba833d6b61
Changed many Intersection rules from i:I to I~=0 to avoid introducing a new
paulson
parents:
14084
diff
changeset

270 
lemma Diff_subset: "AB \<subseteq> A" 
13259  271 
by blast 
272 

46820  273 
lemma Diff_contains: "[ C\<subseteq>A; C \<inter> B = 0 ] ==> C \<subseteq> AB" 
13259  274 
by blast 
275 

46821
ff6b0c1087f2
Using mathematical notation for <> and cardinal arithmetic
paulson
parents:
46820
diff
changeset

276 
lemma subset_Diff_cons_iff: "B \<subseteq> A  cons(c,C) \<longleftrightarrow> B\<subseteq>AC & c \<notin> B" 
13259  277 
by blast 
13165  278 

279 
lemma Diff_cancel: "A  A = 0" 

280 
by blast 

281 

46820  282 
lemma Diff_triv: "A \<inter> B = 0 ==> A  B = A" 
13165  283 
by blast 
284 

285 
lemma empty_Diff [simp]: "0  A = 0" 

286 
by blast 

287 

288 
lemma Diff_0 [simp]: "A  0 = A" 

289 
by blast 

290 

46821
ff6b0c1087f2
Using mathematical notation for <> and cardinal arithmetic
paulson
parents:
46820
diff
changeset

291 
lemma Diff_eq_0_iff: "A  B = 0 \<longleftrightarrow> A \<subseteq> B" 
13165  292 
by (blast elim: equalityE) 
293 

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

295 
lemma Diff_cons: "A  cons(a,B) = A  B  {a}" 

296 
by blast 

297 

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

299 
lemma Diff_cons2: "A  cons(a,B) = A  {a}  B" 

300 
by blast 

301 

46820  302 
lemma Diff_disjoint: "A \<inter> (BA) = 0" 
13165  303 
by blast 
304 

46820  305 
lemma Diff_partition: "A\<subseteq>B ==> A \<union> (BA) = B" 
13165  306 
by blast 
307 

46820  308 
lemma subset_Un_Diff: "A \<subseteq> B \<union> (A  B)" 
13165  309 
by blast 
310 

14095
a1ba833d6b61
Changed many Intersection rules from i:I to I~=0 to avoid introducing a new
paulson
parents:
14084
diff
changeset

311 
lemma double_complement: "[ A\<subseteq>B; B\<subseteq>C ] ==> B(CA) = A" 
13165  312 
by blast 
313 

46820  314 
lemma double_complement_Un: "(A \<union> B)  (BA) = A" 
13165  315 
by blast 
316 

46820  317 
lemma Un_Int_crazy: 
318 
"(A \<inter> B) \<union> (B \<inter> C) \<union> (C \<inter> A) = (A \<union> B) \<inter> (B \<union> C) \<inter> (C \<union> A)" 

13165  319 
apply blast 
320 
done 

321 

46820  322 
lemma Diff_Un: "A  (B \<union> C) = (AB) \<inter> (AC)" 
13165  323 
by blast 
324 

46820  325 
lemma Diff_Int: "A  (B \<inter> C) = (AB) \<union> (AC)" 
13165  326 
by blast 
327 

46820  328 
lemma Un_Diff: "(A \<union> B)  C = (A  C) \<union> (B  C)" 
13165  329 
by blast 
330 

46820  331 
lemma Int_Diff: "(A \<inter> B)  C = A \<inter> (B  C)" 
13165  332 
by blast 
333 

46820  334 
lemma Diff_Int_distrib: "C \<inter> (AB) = (C \<inter> A)  (C \<inter> B)" 
13165  335 
by blast 
336 

46820  337 
lemma Diff_Int_distrib2: "(AB) \<inter> C = (A \<inter> C)  (B \<inter> C)" 
13165  338 
by blast 
339 

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

46821
ff6b0c1087f2
Using mathematical notation for <> and cardinal arithmetic
paulson
parents:
46820
diff
changeset

341 
lemma Un_Int_assoc_iff: "(A \<inter> B) \<union> C = A \<inter> (B \<union> C) \<longleftrightarrow> C\<subseteq>A" 
13165  342 
by (blast elim!: equalityE) 
343 

344 

13356  345 
subsection{*Big Union and Intersection*} 
13259  346 

347 
(** Big Union is the least upper bound of a set **) 

348 

46821
ff6b0c1087f2
Using mathematical notation for <> and cardinal arithmetic
paulson
parents:
46820
diff
changeset

349 
lemma Union_subset_iff: "\<Union>(A) \<subseteq> C \<longleftrightarrow> (\<forall>x\<in>A. x \<subseteq> C)" 
13259  350 
by blast 
351 

46820  352 
lemma Union_upper: "B\<in>A ==> B \<subseteq> \<Union>(A)" 
13259  353 
by blast 
354 

46820  355 
lemma Union_least: "[ !!x. x\<in>A ==> x\<subseteq>C ] ==> \<Union>(A) \<subseteq> C" 
13259  356 
by blast 
13165  357 

46820  358 
lemma Union_cons [simp]: "\<Union>(cons(a,B)) = a \<union> \<Union>(B)" 
13165  359 
by blast 
360 

46820  361 
lemma Union_Un_distrib: "\<Union>(A \<union> B) = \<Union>(A) \<union> \<Union>(B)" 
13165  362 
by blast 
363 

46820  364 
lemma Union_Int_subset: "\<Union>(A \<inter> B) \<subseteq> \<Union>(A) \<inter> \<Union>(B)" 
13165  365 
by blast 
366 

46821
ff6b0c1087f2
Using mathematical notation for <> and cardinal arithmetic
paulson
parents:
46820
diff
changeset

367 
lemma Union_disjoint: "\<Union>(C) \<inter> A = 0 \<longleftrightarrow> (\<forall>B\<in>C. B \<inter> A = 0)" 
13165  368 
by (blast elim!: equalityE) 
369 

46821
ff6b0c1087f2
Using mathematical notation for <> and cardinal arithmetic
paulson
parents:
46820
diff
changeset

370 
lemma Union_empty_iff: "\<Union>(A) = 0 \<longleftrightarrow> (\<forall>B\<in>A. B=0)" 
13165  371 
by blast 
372 

46820  373 
lemma Int_Union2: "\<Union>(B) \<inter> A = (\<Union>C\<in>B. C \<inter> A)" 
14084
ccb48f3239f7
Removal of UNITY/UNITYMisc, moving its theorems elsewhere.
paulson
parents:
14077
diff
changeset

374 
by blast 
ccb48f3239f7
Removal of UNITY/UNITYMisc, moving its theorems elsewhere.
paulson
parents:
14077
diff
changeset

375 

13259  376 
(** Big Intersection is the greatest lower bound of a nonempty set **) 
377 

46821
ff6b0c1087f2
Using mathematical notation for <> and cardinal arithmetic
paulson
parents:
46820
diff
changeset

378 
lemma Inter_subset_iff: "A\<noteq>0 ==> C \<subseteq> \<Inter>(A) \<longleftrightarrow> (\<forall>x\<in>A. C \<subseteq> x)" 
13259  379 
by blast 
380 

46820  381 
lemma Inter_lower: "B\<in>A ==> \<Inter>(A) \<subseteq> B" 
13259  382 
by blast 
383 

46820  384 
lemma Inter_greatest: "[ A\<noteq>0; !!x. x\<in>A ==> C\<subseteq>x ] ==> C \<subseteq> \<Inter>(A)" 
13259  385 
by blast 
386 

387 
(** Intersection of a family of sets **) 

388 

14095
a1ba833d6b61
Changed many Intersection rules from i:I to I~=0 to avoid introducing a new
paulson
parents:
14084
diff
changeset

389 
lemma INT_lower: "x\<in>A ==> (\<Inter>x\<in>A. B(x)) \<subseteq> B(x)" 
13259  390 
by blast 
391 

14095
a1ba833d6b61
Changed many Intersection rules from i:I to I~=0 to avoid introducing a new
paulson
parents:
14084
diff
changeset

392 
lemma INT_greatest: "[ A\<noteq>0; !!x. x\<in>A ==> C\<subseteq>B(x) ] ==> C \<subseteq> (\<Inter>x\<in>A. B(x))" 
a1ba833d6b61
Changed many Intersection rules from i:I to I~=0 to avoid introducing a new
paulson
parents:
14084
diff
changeset

393 
by force 
13259  394 

46820  395 
lemma Inter_0 [simp]: "\<Inter>(0) = 0" 
13165  396 
by (unfold Inter_def, blast) 
397 

13259  398 
lemma Inter_Un_subset: 
46820  399 
"[ z\<in>A; z\<in>B ] ==> \<Inter>(A) \<union> \<Inter>(B) \<subseteq> \<Inter>(A \<inter> B)" 
13165  400 
by blast 
401 

402 
(* A good challenge: Inter is illbehaved on the empty set *) 

403 
lemma Inter_Un_distrib: 

46820  404 
"[ A\<noteq>0; B\<noteq>0 ] ==> \<Inter>(A \<union> B) = \<Inter>(A) \<inter> \<Inter>(B)" 
13165  405 
by blast 
406 

46820  407 
lemma Union_singleton: "\<Union>({b}) = b" 
13165  408 
by blast 
409 

46820  410 
lemma Inter_singleton: "\<Inter>({b}) = b" 
13165  411 
by blast 
412 

413 
lemma Inter_cons [simp]: 

46820  414 
"\<Inter>(cons(a,B)) = (if B=0 then a else a \<inter> \<Inter>(B))" 
13165  415 
by force 
416 

13356  417 
subsection{*Unions and Intersections of Families*} 
13259  418 

46821
ff6b0c1087f2
Using mathematical notation for <> and cardinal arithmetic
paulson
parents:
46820
diff
changeset

419 
lemma subset_UN_iff_eq: "A \<subseteq> (\<Union>i\<in>I. B(i)) \<longleftrightarrow> A = (\<Union>i\<in>I. A \<inter> B(i))" 
13259  420 
by (blast elim!: equalityE) 
421 

46821
ff6b0c1087f2
Using mathematical notation for <> and cardinal arithmetic
paulson
parents:
46820
diff
changeset

422 
lemma UN_subset_iff: "(\<Union>x\<in>A. B(x)) \<subseteq> C \<longleftrightarrow> (\<forall>x\<in>A. B(x) \<subseteq> C)" 
13259  423 
by blast 
424 

14095
a1ba833d6b61
Changed many Intersection rules from i:I to I~=0 to avoid introducing a new
paulson
parents:
14084
diff
changeset

425 
lemma UN_upper: "x\<in>A ==> B(x) \<subseteq> (\<Union>x\<in>A. B(x))" 
13259  426 
by (erule RepFunI [THEN Union_upper]) 
427 

14095
a1ba833d6b61
Changed many Intersection rules from i:I to I~=0 to avoid introducing a new
paulson
parents:
14084
diff
changeset

428 
lemma UN_least: "[ !!x. x\<in>A ==> B(x)\<subseteq>C ] ==> (\<Union>x\<in>A. B(x)) \<subseteq> C" 
13259  429 
by blast 
13165  430 

46820  431 
lemma Union_eq_UN: "\<Union>(A) = (\<Union>x\<in>A. x)" 
13165  432 
by blast 
433 

46820  434 
lemma Inter_eq_INT: "\<Inter>(A) = (\<Inter>x\<in>A. x)" 
13165  435 
by (unfold Inter_def, blast) 
436 

13615
449a70d88b38
Numerous cosmetic changes, prompted by the new simplifier
paulson
parents:
13611
diff
changeset

437 
lemma UN_0 [simp]: "(\<Union>i\<in>0. A(i)) = 0" 
13165  438 
by blast 
439 

13615
449a70d88b38
Numerous cosmetic changes, prompted by the new simplifier
paulson
parents:
13611
diff
changeset

440 
lemma UN_singleton: "(\<Union>x\<in>A. {x}) = A" 
13165  441 
by blast 
442 

46820  443 
lemma UN_Un: "(\<Union>i\<in> A \<union> B. C(i)) = (\<Union>i\<in> A. C(i)) \<union> (\<Union>i\<in>B. C(i))" 
13165  444 
by blast 
445 

46820  446 
lemma INT_Un: "(\<Inter>i\<in>I \<union> J. A(i)) = 
447 
(if I=0 then \<Inter>j\<in>J. A(j) 

448 
else if J=0 then \<Inter>i\<in>I. A(i) 

449 
else ((\<Inter>i\<in>I. A(i)) \<inter> (\<Inter>j\<in>J. A(j))))" 

14095
a1ba833d6b61
Changed many Intersection rules from i:I to I~=0 to avoid introducing a new
paulson
parents:
14084
diff
changeset

450 
by (simp, blast intro!: equalityI) 
13165  451 

13615
449a70d88b38
Numerous cosmetic changes, prompted by the new simplifier
paulson
parents:
13611
diff
changeset

452 
lemma UN_UN_flatten: "(\<Union>x \<in> (\<Union>y\<in>A. B(y)). C(x)) = (\<Union>y\<in>A. \<Union>x\<in> B(y). C(x))" 
13165  453 
by blast 
454 

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

46820  456 
lemma Int_UN_distrib: "B \<inter> (\<Union>i\<in>I. A(i)) = (\<Union>i\<in>I. B \<inter> A(i))" 
13165  457 
by blast 
458 

46820  459 
lemma Un_INT_distrib: "I\<noteq>0 ==> B \<union> (\<Inter>i\<in>I. A(i)) = (\<Inter>i\<in>I. B \<union> A(i))" 
14095
a1ba833d6b61
Changed many Intersection rules from i:I to I~=0 to avoid introducing a new
paulson
parents:
14084
diff
changeset

460 
by auto 
13165  461 

462 
lemma Int_UN_distrib2: 

46820  463 
"(\<Union>i\<in>I. A(i)) \<inter> (\<Union>j\<in>J. B(j)) = (\<Union>i\<in>I. \<Union>j\<in>J. A(i) \<inter> B(j))" 
13165  464 
by blast 
465 

46820  466 
lemma Un_INT_distrib2: "[ I\<noteq>0; J\<noteq>0 ] ==> 
467 
(\<Inter>i\<in>I. A(i)) \<union> (\<Inter>j\<in>J. B(j)) = (\<Inter>i\<in>I. \<Inter>j\<in>J. A(i) \<union> B(j))" 

14095
a1ba833d6b61
Changed many Intersection rules from i:I to I~=0 to avoid introducing a new
paulson
parents:
14084
diff
changeset

468 
by auto 
13165  469 

14095
a1ba833d6b61
Changed many Intersection rules from i:I to I~=0 to avoid introducing a new
paulson
parents:
14084
diff
changeset

470 
lemma UN_constant [simp]: "(\<Union>y\<in>A. c) = (if A=0 then 0 else c)" 
a1ba833d6b61
Changed many Intersection rules from i:I to I~=0 to avoid introducing a new
paulson
parents:
14084
diff
changeset

471 
by force 
13165  472 

14095
a1ba833d6b61
Changed many Intersection rules from i:I to I~=0 to avoid introducing a new
paulson
parents:
14084
diff
changeset

473 
lemma INT_constant [simp]: "(\<Inter>y\<in>A. c) = (if A=0 then 0 else c)" 
a1ba833d6b61
Changed many Intersection rules from i:I to I~=0 to avoid introducing a new
paulson
parents:
14084
diff
changeset

474 
by force 
13165  475 

13615
449a70d88b38
Numerous cosmetic changes, prompted by the new simplifier
paulson
parents:
13611
diff
changeset

476 
lemma UN_RepFun [simp]: "(\<Union>y\<in> RepFun(A,f). B(y)) = (\<Union>x\<in>A. B(f(x)))" 
13165  477 
by blast 
478 

13615
449a70d88b38
Numerous cosmetic changes, prompted by the new simplifier
paulson
parents:
13611
diff
changeset

479 
lemma INT_RepFun [simp]: "(\<Inter>x\<in>RepFun(A,f). B(x)) = (\<Inter>a\<in>A. B(f(a)))" 
13165  480 
by (auto simp add: Inter_def) 
481 

482 
lemma INT_Union_eq: 

46820  483 
"0 \<notin> A ==> (\<Inter>x\<in> \<Union>(A). B(x)) = (\<Inter>y\<in>A. \<Inter>x\<in>y. B(x))" 
484 
apply (subgoal_tac "\<forall>x\<in>A. x\<noteq>0") 

13615
449a70d88b38
Numerous cosmetic changes, prompted by the new simplifier
paulson
parents:
13611
diff
changeset

485 
prefer 2 apply blast 
46820  486 
apply (force simp add: Inter_def ball_conj_distrib) 
13165  487 
done 
488 

13615
449a70d88b38
Numerous cosmetic changes, prompted by the new simplifier
paulson
parents:
13611
diff
changeset

489 
lemma INT_UN_eq: 
46820  490 
"(\<forall>x\<in>A. B(x) \<noteq> 0) 
13615
449a70d88b38
Numerous cosmetic changes, prompted by the new simplifier
paulson
parents:
13611
diff
changeset

491 
==> (\<Inter>z\<in> (\<Union>x\<in>A. B(x)). C(z)) = (\<Inter>x\<in>A. \<Inter>z\<in> B(x). C(z))" 
13165  492 
apply (subst INT_Union_eq, blast) 
493 
apply (simp add: Inter_def) 

494 
done 

495 

496 

46820  497 
(** Devlin, Fundamentals of Contemporary Set Theory, page 12, exercise 5: 
13165  498 
Union of a family of unions **) 
499 

500 
lemma UN_Un_distrib: 

46820  501 
"(\<Union>i\<in>I. A(i) \<union> B(i)) = (\<Union>i\<in>I. A(i)) \<union> (\<Union>i\<in>I. B(i))" 
13165  502 
by blast 
503 

504 
lemma INT_Int_distrib: 

46820  505 
"I\<noteq>0 ==> (\<Inter>i\<in>I. A(i) \<inter> B(i)) = (\<Inter>i\<in>I. A(i)) \<inter> (\<Inter>i\<in>I. B(i))" 
14095
a1ba833d6b61
Changed many Intersection rules from i:I to I~=0 to avoid introducing a new
paulson
parents:
14084
diff
changeset

506 
by (blast elim!: not_emptyE) 
13165  507 

508 
lemma UN_Int_subset: 

46820  509 
"(\<Union>z\<in>I \<inter> J. A(z)) \<subseteq> (\<Union>z\<in>I. A(z)) \<inter> (\<Union>z\<in>J. A(z))" 
13165  510 
by blast 
511 

512 
(** Devlin, page 12, exercise 5: Complements **) 

513 

14095
a1ba833d6b61
Changed many Intersection rules from i:I to I~=0 to avoid introducing a new
paulson
parents:
14084
diff
changeset

514 
lemma Diff_UN: "I\<noteq>0 ==> B  (\<Union>i\<in>I. A(i)) = (\<Inter>i\<in>I. B  A(i))" 
a1ba833d6b61
Changed many Intersection rules from i:I to I~=0 to avoid introducing a new
paulson
parents:
14084
diff
changeset

515 
by (blast elim!: not_emptyE) 
13165  516 

14095
a1ba833d6b61
Changed many Intersection rules from i:I to I~=0 to avoid introducing a new
paulson
parents:
14084
diff
changeset

517 
lemma Diff_INT: "I\<noteq>0 ==> B  (\<Inter>i\<in>I. A(i)) = (\<Union>i\<in>I. B  A(i))" 
a1ba833d6b61
Changed many Intersection rules from i:I to I~=0 to avoid introducing a new
paulson
parents:
14084
diff
changeset

518 
by (blast elim!: not_emptyE) 
a1ba833d6b61
Changed many Intersection rules from i:I to I~=0 to avoid introducing a new
paulson
parents:
14084
diff
changeset

519 

13165  520 

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

522 

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

46820  524 
lemma Sigma_cons1: "Sigma(cons(a,B), C) = ({a}*C(a)) \<union> Sigma(B,C)" 
13165  525 
by blast 
526 

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

46820  528 
lemma Sigma_cons2: "A * cons(b,B) = A*{b} \<union> A*B" 
13165  529 
by blast 
530 

46820  531 
lemma Sigma_succ1: "Sigma(succ(A), B) = ({A}*B(A)) \<union> Sigma(A,B)" 
13165  532 
by blast 
533 

46820  534 
lemma Sigma_succ2: "A * succ(B) = A*{B} \<union> A*B" 
13165  535 
by blast 
536 

537 
lemma SUM_UN_distrib1: 

14171
0cab06e3bbd0
Extended the notion of letter and digit, such that now one may use greek,
skalberg
parents:
14095
diff
changeset

538 
"(\<Sigma> x \<in> (\<Union>y\<in>A. C(y)). B(x)) = (\<Union>y\<in>A. \<Sigma> x\<in>C(y). B(x))" 
13165  539 
by blast 
540 

541 
lemma SUM_UN_distrib2: 

14171
0cab06e3bbd0
Extended the notion of letter and digit, such that now one may use greek,
skalberg
parents:
14095
diff
changeset

542 
"(\<Sigma> i\<in>I. \<Union>j\<in>J. C(i,j)) = (\<Union>j\<in>J. \<Sigma> i\<in>I. C(i,j))" 
13165  543 
by blast 
544 

545 
lemma SUM_Un_distrib1: 

46820  546 
"(\<Sigma> i\<in>I \<union> J. C(i)) = (\<Sigma> i\<in>I. C(i)) \<union> (\<Sigma> j\<in>J. C(j))" 
13165  547 
by blast 
548 

549 
lemma SUM_Un_distrib2: 

46820  550 
"(\<Sigma> i\<in>I. A(i) \<union> B(i)) = (\<Sigma> i\<in>I. A(i)) \<union> (\<Sigma> i\<in>I. B(i))" 
13165  551 
by blast 
552 

553 
(*Firstorder version of the above, for rewriting*) 

46820  554 
lemma prod_Un_distrib2: "I * (A \<union> B) = I*A \<union> I*B" 
13165  555 
by (rule SUM_Un_distrib2) 
556 

557 
lemma SUM_Int_distrib1: 

46820  558 
"(\<Sigma> i\<in>I \<inter> J. C(i)) = (\<Sigma> i\<in>I. C(i)) \<inter> (\<Sigma> j\<in>J. C(j))" 
13165  559 
by blast 
560 

561 
lemma SUM_Int_distrib2: 

46820  562 
"(\<Sigma> i\<in>I. A(i) \<inter> B(i)) = (\<Sigma> i\<in>I. A(i)) \<inter> (\<Sigma> i\<in>I. B(i))" 
13165  563 
by blast 
564 

565 
(*Firstorder version of the above, for rewriting*) 

46820  566 
lemma prod_Int_distrib2: "I * (A \<inter> B) = I*A \<inter> I*B" 
13165  567 
by (rule SUM_Int_distrib2) 
568 

569 
(*Cf Aczel, NonWellFounded Sets, page 115*) 

14171
0cab06e3bbd0
Extended the notion of letter and digit, such that now one may use greek,
skalberg
parents:
14095
diff
changeset

570 
lemma SUM_eq_UN: "(\<Sigma> i\<in>I. A(i)) = (\<Union>i\<in>I. {i} * A(i))" 
13165  571 
by blast 
572 

13544  573 
lemma times_subset_iff: 
46821
ff6b0c1087f2
Using mathematical notation for <> and cardinal arithmetic
paulson
parents:
46820
diff
changeset

574 
"(A'*B' \<subseteq> A*B) \<longleftrightarrow> (A' = 0  B' = 0  (A'\<subseteq>A) & (B'\<subseteq>B))" 
13544  575 
by blast 
576 

577 
lemma Int_Sigma_eq: 

46820  578 
"(\<Sigma> x \<in> A'. B'(x)) \<inter> (\<Sigma> x \<in> A. B(x)) = (\<Sigma> x \<in> A' \<inter> A. B'(x) \<inter> B(x))" 
13544  579 
by blast 
580 

13165  581 
(** Domain **) 
582 

46821
ff6b0c1087f2
Using mathematical notation for <> and cardinal arithmetic
paulson
parents:
46820
diff
changeset

583 
lemma domain_iff: "a: domain(r) \<longleftrightarrow> (\<exists>y. <a,y>\<in> r)" 
13259  584 
by (unfold domain_def, blast) 
585 

14095
a1ba833d6b61
Changed many Intersection rules from i:I to I~=0 to avoid introducing a new
paulson
parents:
14084
diff
changeset

586 
lemma domainI [intro]: "<a,b>\<in> r ==> a: domain(r)" 
13259  587 
by (unfold domain_def, blast) 
588 

589 
lemma domainE [elim!]: 

14095
a1ba833d6b61
Changed many Intersection rules from i:I to I~=0 to avoid introducing a new
paulson
parents:
14084
diff
changeset

590 
"[ a \<in> domain(r); !!y. <a,y>\<in> r ==> P ] ==> P" 
13259  591 
by (unfold domain_def, blast) 
592 

14095
a1ba833d6b61
Changed many Intersection rules from i:I to I~=0 to avoid introducing a new
paulson
parents:
14084
diff
changeset

593 
lemma domain_subset: "domain(Sigma(A,B)) \<subseteq> A" 
13259  594 
by blast 
595 

14095
a1ba833d6b61
Changed many Intersection rules from i:I to I~=0 to avoid introducing a new
paulson
parents:
14084
diff
changeset

596 
lemma domain_of_prod: "b\<in>B ==> domain(A*B) = A" 
13165  597 
by blast 
598 

599 
lemma domain_0 [simp]: "domain(0) = 0" 

600 
by blast 

601 

602 
lemma domain_cons [simp]: "domain(cons(<a,b>,r)) = cons(a, domain(r))" 

603 
by blast 

604 

46820  605 
lemma domain_Un_eq [simp]: "domain(A \<union> B) = domain(A) \<union> domain(B)" 
13165  606 
by blast 
607 

46820  608 
lemma domain_Int_subset: "domain(A \<inter> B) \<subseteq> domain(A) \<inter> domain(B)" 
13165  609 
by blast 
610 

14095
a1ba833d6b61
Changed many Intersection rules from i:I to I~=0 to avoid introducing a new
paulson
parents:
14084
diff
changeset

611 
lemma domain_Diff_subset: "domain(A)  domain(B) \<subseteq> domain(A  B)" 
13165  612 
by blast 
613 

13615
449a70d88b38
Numerous cosmetic changes, prompted by the new simplifier
paulson
parents:
13611
diff
changeset

614 
lemma domain_UN: "domain(\<Union>x\<in>A. B(x)) = (\<Union>x\<in>A. domain(B(x)))" 
13165  615 
by blast 
616 

46820  617 
lemma domain_Union: "domain(\<Union>(A)) = (\<Union>x\<in>A. domain(x))" 
13165  618 
by blast 
619 

620 

621 
(** Range **) 

622 

14095
a1ba833d6b61
Changed many Intersection rules from i:I to I~=0 to avoid introducing a new
paulson
parents:
14084
diff
changeset

623 
lemma rangeI [intro]: "<a,b>\<in> r ==> b \<in> range(r)" 
13259  624 
apply (unfold range_def) 
625 
apply (erule converseI [THEN domainI]) 

626 
done 

627 

14095
a1ba833d6b61
Changed many Intersection rules from i:I to I~=0 to avoid introducing a new
paulson
parents:
14084
diff
changeset

628 
lemma rangeE [elim!]: "[ b \<in> range(r); !!x. <x,b>\<in> r ==> P ] ==> P" 
13259  629 
by (unfold range_def, blast) 
630 

14095
a1ba833d6b61
Changed many Intersection rules from i:I to I~=0 to avoid introducing a new
paulson
parents:
14084
diff
changeset

631 
lemma range_subset: "range(A*B) \<subseteq> B" 
13259  632 
apply (unfold range_def) 
633 
apply (subst converse_prod) 

634 
apply (rule domain_subset) 

635 
done 

636 

14095
a1ba833d6b61
Changed many Intersection rules from i:I to I~=0 to avoid introducing a new
paulson
parents:
14084
diff
changeset

637 
lemma range_of_prod: "a\<in>A ==> range(A*B) = B" 
13165  638 
by blast 
639 

640 
lemma range_0 [simp]: "range(0) = 0" 

641 
by blast 

642 

643 
lemma range_cons [simp]: "range(cons(<a,b>,r)) = cons(b, range(r))" 

644 
by blast 

645 

46820  646 
lemma range_Un_eq [simp]: "range(A \<union> B) = range(A) \<union> range(B)" 
13165  647 
by blast 
648 

46820  649 
lemma range_Int_subset: "range(A \<inter> B) \<subseteq> range(A) \<inter> range(B)" 
13165  650 
by blast 
651 

14095
a1ba833d6b61
Changed many Intersection rules from i:I to I~=0 to avoid introducing a new
paulson
parents:
14084
diff
changeset

652 
lemma range_Diff_subset: "range(A)  range(B) \<subseteq> range(A  B)" 
13165  653 
by blast 
654 

13259  655 
lemma domain_converse [simp]: "domain(converse(r)) = range(r)" 
656 
by blast 

657 

13165  658 
lemma range_converse [simp]: "range(converse(r)) = domain(r)" 
659 
by blast 

660 

661 

662 
(** Field **) 

663 

14095
a1ba833d6b61
Changed many Intersection rules from i:I to I~=0 to avoid introducing a new
paulson
parents:
14084
diff
changeset

664 
lemma fieldI1: "<a,b>\<in> r ==> a \<in> field(r)" 
13259  665 
by (unfold field_def, blast) 
666 

14095
a1ba833d6b61
Changed many Intersection rules from i:I to I~=0 to avoid introducing a new
paulson
parents:
14084
diff
changeset

667 
lemma fieldI2: "<a,b>\<in> r ==> b \<in> field(r)" 
13259  668 
by (unfold field_def, blast) 
669 

46820  670 
lemma fieldCI [intro]: 
14095
a1ba833d6b61
Changed many Intersection rules from i:I to I~=0 to avoid introducing a new
paulson
parents:
14084
diff
changeset

671 
"(~ <c,a>\<in>r ==> <a,b>\<in> r) ==> a \<in> field(r)" 
13259  672 
apply (unfold field_def, blast) 
673 
done 

674 

46820  675 
lemma fieldE [elim!]: 
676 
"[ a \<in> field(r); 

677 
!!x. <a,x>\<in> r ==> P; 

14095
a1ba833d6b61
Changed many Intersection rules from i:I to I~=0 to avoid introducing a new
paulson
parents:
14084
diff
changeset

678 
!!x. <x,a>\<in> r ==> P ] ==> P" 
13259  679 
by (unfold field_def, blast) 
680 

46820  681 
lemma field_subset: "field(A*B) \<subseteq> A \<union> B" 
13259  682 
by blast 
683 

14095
a1ba833d6b61
Changed many Intersection rules from i:I to I~=0 to avoid introducing a new
paulson
parents:
14084
diff
changeset

684 
lemma domain_subset_field: "domain(r) \<subseteq> field(r)" 
13259  685 
apply (unfold field_def) 
686 
apply (rule Un_upper1) 

687 
done 

688 

14095
a1ba833d6b61
Changed many Intersection rules from i:I to I~=0 to avoid introducing a new
paulson
parents:
14084
diff
changeset

689 
lemma range_subset_field: "range(r) \<subseteq> field(r)" 
13259  690 
apply (unfold field_def) 
691 
apply (rule Un_upper2) 

692 
done 

693 

14095
a1ba833d6b61
Changed many Intersection rules from i:I to I~=0 to avoid introducing a new
paulson
parents:
14084
diff
changeset

694 
lemma domain_times_range: "r \<subseteq> Sigma(A,B) ==> r \<subseteq> domain(r)*range(r)" 
13259  695 
by blast 
696 

14095
a1ba833d6b61
Changed many Intersection rules from i:I to I~=0 to avoid introducing a new
paulson
parents:
14084
diff
changeset

697 
lemma field_times_field: "r \<subseteq> Sigma(A,B) ==> r \<subseteq> field(r)*field(r)" 
13259  698 
by blast 
699 

14095
a1ba833d6b61
Changed many Intersection rules from i:I to I~=0 to avoid introducing a new
paulson
parents:
14084
diff
changeset

700 
lemma relation_field_times_field: "relation(r) ==> r \<subseteq> field(r)*field(r)" 
46820  701 
by (simp add: relation_def, blast) 
13259  702 

13165  703 
lemma field_of_prod: "field(A*A) = A" 
704 
by blast 

705 

706 
lemma field_0 [simp]: "field(0) = 0" 

707 
by blast 

708 

709 
lemma field_cons [simp]: "field(cons(<a,b>,r)) = cons(a, cons(b, field(r)))" 

710 
by blast 

711 

46820  712 
lemma field_Un_eq [simp]: "field(A \<union> B) = field(A) \<union> field(B)" 
13165  713 
by blast 
714 

46820  715 
lemma field_Int_subset: "field(A \<inter> B) \<subseteq> field(A) \<inter> field(B)" 
13165  716 
by blast 
717 

14095
a1ba833d6b61
Changed many Intersection rules from i:I to I~=0 to avoid introducing a new
paulson
parents:
14084
diff
changeset

718 
lemma field_Diff_subset: "field(A)  field(B) \<subseteq> field(A  B)" 
13165  719 
by blast 
720 

721 
lemma field_converse [simp]: "field(converse(r)) = field(r)" 

722 
by blast 

723 

13259  724 
(** The Union of a set of relations is a relation  Lemma for fun_Union **) 
46820  725 
lemma rel_Union: "(\<forall>x\<in>S. \<exists>A B. x \<subseteq> A*B) ==> 
726 
\<Union>(S) \<subseteq> domain(\<Union>(S)) * range(\<Union>(S))" 

13259  727 
by blast 
13165  728 

13259  729 
(** The Union of 2 relations is a relation (Lemma for fun_Un) **) 
46820  730 
lemma rel_Un: "[ r \<subseteq> A*B; s \<subseteq> C*D ] ==> (r \<union> s) \<subseteq> (A \<union> C) * (B \<union> D)" 
13259  731 
by blast 
732 

46820  733 
lemma domain_Diff_eq: "[ <a,c> \<in> r; c\<noteq>b ] ==> domain(r{<a,b>}) = domain(r)" 
13259  734 
by blast 
735 

46820  736 
lemma range_Diff_eq: "[ <c,b> \<in> r; c\<noteq>a ] ==> range(r{<a,b>}) = range(r)" 
13259  737 
by blast 
738 

739 

13356  740 
subsection{*Image of a Set under a Function or Relation*} 
13259  741 

46821
ff6b0c1087f2
Using mathematical notation for <> and cardinal arithmetic
paulson
parents:
46820
diff
changeset

742 
lemma image_iff: "b \<in> r``A \<longleftrightarrow> (\<exists>x\<in>A. <x,b>\<in>r)" 
13259  743 
by (unfold image_def, blast) 
744 

46821
ff6b0c1087f2
Using mathematical notation for <> and cardinal arithmetic
paulson
parents:
46820
diff
changeset

745 
lemma image_singleton_iff: "b \<in> r``{a} \<longleftrightarrow> <a,b>\<in>r" 
13259  746 
by (rule image_iff [THEN iff_trans], blast) 
747 

14095
a1ba833d6b61
Changed many Intersection rules from i:I to I~=0 to avoid introducing a new
paulson
parents:
14084
diff
changeset

748 
lemma imageI [intro]: "[ <a,b>\<in> r; a\<in>A ] ==> b \<in> r``A" 
13259  749 
by (unfold image_def, blast) 
750 

46820  751 
lemma imageE [elim!]: 
14095
a1ba833d6b61
Changed many Intersection rules from i:I to I~=0 to avoid introducing a new
paulson
parents:
14084
diff
changeset

752 
"[ b: r``A; !!x.[ <x,b>\<in> r; x\<in>A ] ==> P ] ==> P" 
13259  753 
by (unfold image_def, blast) 
754 

14095
a1ba833d6b61
Changed many Intersection rules from i:I to I~=0 to avoid introducing a new
paulson
parents:
14084
diff
changeset

755 
lemma image_subset: "r \<subseteq> A*B ==> r``C \<subseteq> B" 
13259  756 
by blast 
13165  757 

758 
lemma image_0 [simp]: "r``0 = 0" 

759 
by blast 

760 

46820  761 
lemma image_Un [simp]: "r``(A \<union> B) = (r``A) \<union> (r``B)" 
13165  762 
by blast 
763 

14883  764 
lemma image_UN: "r `` (\<Union>x\<in>A. B(x)) = (\<Union>x\<in>A. r `` B(x))" 
765 
by blast 

766 

767 
lemma Collect_image_eq: 

768 
"{z \<in> Sigma(A,B). P(z)} `` C = (\<Union>x \<in> A. {y \<in> B(x). x \<in> C & P(<x,y>)})" 

769 
by blast 

770 

46820  771 
lemma image_Int_subset: "r``(A \<inter> B) \<subseteq> (r``A) \<inter> (r``B)" 
13165  772 
by blast 
773 

46820  774 
lemma image_Int_square_subset: "(r \<inter> A*A)``B \<subseteq> (r``B) \<inter> A" 
13165  775 
by blast 
776 

46820  777 
lemma image_Int_square: "B\<subseteq>A ==> (r \<inter> A*A)``B = (r``B) \<inter> A" 
13165  778 
by blast 
779 

780 

781 
(*Image laws for special relations*) 

782 
lemma image_0_left [simp]: "0``A = 0" 

783 
by blast 

784 

46820  785 
lemma image_Un_left: "(r \<union> s)``A = (r``A) \<union> (s``A)" 
13165  786 
by blast 
787 

46820  788 
lemma image_Int_subset_left: "(r \<inter> s)``A \<subseteq> (r``A) \<inter> (s``A)" 
13165  789 
by blast 
790 

791 

13356  792 
subsection{*Inverse Image of a Set under a Function or Relation*} 
13259  793 

46820  794 
lemma vimage_iff: 
46821
ff6b0c1087f2
Using mathematical notation for <> and cardinal arithmetic
paulson
parents:
46820
diff
changeset

795 
"a \<in> r``B \<longleftrightarrow> (\<exists>y\<in>B. <a,y>\<in>r)" 
13259  796 
by (unfold vimage_def image_def converse_def, blast) 
797 

46821
ff6b0c1087f2
Using mathematical notation for <> and cardinal arithmetic
paulson
parents:
46820
diff
changeset

798 
lemma vimage_singleton_iff: "a \<in> r``{b} \<longleftrightarrow> <a,b>\<in>r" 
13259  799 
by (rule vimage_iff [THEN iff_trans], blast) 
800 

14095
a1ba833d6b61
Changed many Intersection rules from i:I to I~=0 to avoid introducing a new
paulson
parents:
14084
diff
changeset

801 
lemma vimageI [intro]: "[ <a,b>\<in> r; b\<in>B ] ==> a \<in> r``B" 
13259  802 
by (unfold vimage_def, blast) 
803 

46820  804 
lemma vimageE [elim!]: 
14095
a1ba833d6b61
Changed many Intersection rules from i:I to I~=0 to avoid introducing a new
paulson
parents:
14084
diff
changeset

805 
"[ a: r``B; !!x.[ <a,x>\<in> r; x\<in>B ] ==> P ] ==> P" 
13259  806 
apply (unfold vimage_def, blast) 
807 
done 

808 

14095
a1ba833d6b61
Changed many Intersection rules from i:I to I~=0 to avoid introducing a new
paulson
parents:
14084
diff
changeset

809 
lemma vimage_subset: "r \<subseteq> A*B ==> r``C \<subseteq> A" 
13259  810 
apply (unfold vimage_def) 
811 
apply (erule converse_type [THEN image_subset]) 

812 
done 

13165  813 

814 
lemma vimage_0 [simp]: "r``0 = 0" 

815 
by blast 

816 

46820  817 
lemma vimage_Un [simp]: "r``(A \<union> B) = (r``A) \<union> (r``B)" 
13165  818 
by blast 
819 

46820  820 
lemma vimage_Int_subset: "r``(A \<inter> B) \<subseteq> (r``A) \<inter> (r``B)" 
13165  821 
by blast 
822 

823 
(*NOT suitable for rewriting*) 

13615
449a70d88b38
Numerous cosmetic changes, prompted by the new simplifier
paulson
parents:
13611
diff
changeset

824 
lemma vimage_eq_UN: "f ``B = (\<Union>y\<in>B. f``{y})" 
13165  825 
by blast 
826 

827 
lemma function_vimage_Int: 

46820  828 
"function(f) ==> f``(A \<inter> B) = (f``A) \<inter> (f``B)" 
13165  829 
by (unfold function_def, blast) 
830 

831 
lemma function_vimage_Diff: "function(f) ==> f``(AB) = (f``A)  (f``B)" 

832 
by (unfold function_def, blast) 

833 

14095
a1ba833d6b61
Changed many Intersection rules from i:I to I~=0 to avoid introducing a new
paulson
parents:
14084
diff
changeset

834 
lemma function_image_vimage: "function(f) ==> f `` (f`` A) \<subseteq> A" 
13165  835 
by (unfold function_def, blast) 
836 

46820  837 
lemma vimage_Int_square_subset: "(r \<inter> A*A)``B \<subseteq> (r``B) \<inter> A" 
13165  838 
by blast 
839 

46820  840 
lemma vimage_Int_square: "B\<subseteq>A ==> (r \<inter> A*A)``B = (r``B) \<inter> A" 
13165  841 
by blast 
842 

843 

844 

845 
(*Invese image laws for special relations*) 

846 
lemma vimage_0_left [simp]: "0``A = 0" 

847 
by blast 

848 

46820  849 
lemma vimage_Un_left: "(r \<union> s)``A = (r``A) \<union> (s``A)" 
13165  850 
by blast 
851 

46820  852 
lemma vimage_Int_subset_left: "(r \<inter> s)``A \<subseteq> (r``A) \<inter> (s``A)" 
13165  853 
by blast 
854 

855 

856 
(** Converse **) 

857 

46820  858 
lemma converse_Un [simp]: "converse(A \<union> B) = converse(A) \<union> converse(B)" 
13165  859 
by blast 
860 

46820  861 
lemma converse_Int [simp]: "converse(A \<inter> B) = converse(A) \<inter> converse(B)" 
13165  862 
by blast 
863 

864 
lemma converse_Diff [simp]: "converse(A  B) = converse(A)  converse(B)" 

865 
by blast 

866 

13615
449a70d88b38
Numerous cosmetic changes, prompted by the new simplifier
paulson
parents:
13611
diff
changeset

867 
lemma converse_UN [simp]: "converse(\<Union>x\<in>A. B(x)) = (\<Union>x\<in>A. converse(B(x)))" 
13165  868 
by blast 
869 

870 
(*Unfolding Inter avoids using excluded middle on A=0*) 

871 
lemma converse_INT [simp]: 

13615
449a70d88b38
Numerous cosmetic changes, prompted by the new simplifier
paulson
parents:
13611
diff
changeset

872 
"converse(\<Inter>x\<in>A. B(x)) = (\<Inter>x\<in>A. converse(B(x)))" 
13165  873 
apply (unfold Inter_def, blast) 
874 
done 

875 

13356  876 

877 
subsection{*Powerset Operator*} 

13165  878 

879 
lemma Pow_0 [simp]: "Pow(0) = {0}" 

880 
by blast 

881 

46820  882 
lemma Pow_insert: "Pow (cons(a,A)) = Pow(A) \<union> {cons(a,X) . X: Pow(A)}" 
13165  883 
apply (rule equalityI, safe) 
884 
apply (erule swap) 

46820  885 
apply (rule_tac a = "x{a}" in RepFun_eqI, auto) 
13165  886 
done 
887 

46820  888 
lemma Un_Pow_subset: "Pow(A) \<union> Pow(B) \<subseteq> Pow(A \<union> B)" 
13165  889 
by blast 
890 

14095
a1ba833d6b61
Changed many Intersection rules from i:I to I~=0 to avoid introducing a new
paulson
parents:
14084
diff
changeset

891 
lemma UN_Pow_subset: "(\<Union>x\<in>A. Pow(B(x))) \<subseteq> Pow(\<Union>x\<in>A. B(x))" 
13165  892 
by blast 
893 

46820  894 
lemma subset_Pow_Union: "A \<subseteq> Pow(\<Union>(A))" 
13165  895 
by blast 
896 

46820  897 
lemma Union_Pow_eq [simp]: "\<Union>(Pow(A)) = A" 
13165  898 
by blast 
899 

46821
ff6b0c1087f2
Using mathematical notation for <> and cardinal arithmetic
paulson
parents:
46820
diff
changeset

900 
lemma Union_Pow_iff: "\<Union>(A) \<in> Pow(B) \<longleftrightarrow> A \<in> Pow(Pow(B))" 
14077  901 
by blast 
902 

46820  903 
lemma Pow_Int_eq [simp]: "Pow(A \<inter> B) = Pow(A) \<inter> Pow(B)" 
13165  904 
by blast 
905 

14095
a1ba833d6b61
Changed many Intersection rules from i:I to I~=0 to avoid introducing a new
paulson
parents:
14084
diff
changeset

906 
lemma Pow_INT_eq: "A\<noteq>0 ==> Pow(\<Inter>x\<in>A. B(x)) = (\<Inter>x\<in>A. Pow(B(x)))" 
a1ba833d6b61
Changed many Intersection rules from i:I to I~=0 to avoid introducing a new
paulson
parents:
14084
diff
changeset

907 
by (blast elim!: not_emptyE) 
13165  908 

13356  909 

910 
subsection{*RepFun*} 

13259  911 

14095
a1ba833d6b61
Changed many Intersection rules from i:I to I~=0 to avoid introducing a new
paulson
parents:
14084
diff
changeset

912 
lemma RepFun_subset: "[ !!x. x\<in>A ==> f(x) \<in> B ] ==> {f(x). x\<in>A} \<subseteq> B" 
13259  913 
by blast 
13165  914 

46821
ff6b0c1087f2
Using mathematical notation for <> and cardinal arithmetic
paulson
parents:
46820
diff
changeset

915 
lemma RepFun_eq_0_iff [simp]: "{f(x).x\<in>A}=0 \<longleftrightarrow> A=0" 
13165  916 
by blast 
917 

14095
a1ba833d6b61
Changed many Intersection rules from i:I to I~=0 to avoid introducing a new
paulson
parents:
14084
diff
changeset

918 
lemma RepFun_constant [simp]: "{c. x\<in>A} = (if A=0 then 0 else {c})" 
a1ba833d6b61
Changed many Intersection rules from i:I to I~=0 to avoid introducing a new
paulson
parents:
14084
diff
changeset

919 
by force 
a1ba833d6b61
Changed many Intersection rules from i:I to I~=0 to avoid introducing a new
paulson
parents:
14084
diff
changeset

920 

13165  921 

13356  922 
subsection{*Collect*} 
13259  923 

14095
a1ba833d6b61
Changed many Intersection rules from i:I to I~=0 to avoid introducing a new
paulson
parents:
14084
diff
changeset

924 
lemma Collect_subset: "Collect(A,P) \<subseteq> A" 
13259  925 
by blast 
2469  926 

46820  927 
lemma Collect_Un: "Collect(A \<union> B, P) = Collect(A,P) \<union> Collect(B,P)" 
13165  928 
by blast 
929 

46820  930 
lemma Collect_Int: "Collect(A \<inter> B, P) = Collect(A,P) \<inter> Collect(B,P)" 
13165  931 
by blast 
932 

933 
lemma Collect_Diff: "Collect(A  B, P) = Collect(A,P)  Collect(B,P)" 

934 
by blast 

935 

46820  936 
lemma Collect_cons: "{x\<in>cons(a,B). P(x)} = 
14095
a1ba833d6b61
Changed many Intersection rules from i:I to I~=0 to avoid introducing a new
paulson
parents:
14084
diff
changeset

937 
(if P(a) then cons(a, {x\<in>B. P(x)}) else {x\<in>B. P(x)})" 
13165  938 
by (simp, blast) 
939 

46820  940 
lemma Int_Collect_self_eq: "A \<inter> Collect(A,P) = Collect(A,P)" 
13165  941 
by blast 
942 

943 
lemma Collect_Collect_eq [simp]: 

944 
"Collect(Collect(A,P), Q) = Collect(A, %x. P(x) & Q(x))" 

945 
by blast 

946 

947 
lemma Collect_Int_Collect_eq: 

46820  948 
"Collect(A,P) \<inter> Collect(A,Q) = Collect(A, %x. P(x) & Q(x))" 
13165  949 
by blast 
950 

13203
fac77a839aa2
Tidying up. Mainly moving proofs from Main.thy to other (Isar) theory files.
paulson
parents:
13178
diff
changeset

951 
lemma Collect_Union_eq [simp]: 
fac77a839aa2
Tidying up. Mainly moving proofs from Main.thy to other (Isar) theory files.
paulson
parents:
13178
diff
changeset

952 
"Collect(\<Union>x\<in>A. B(x), P) = (\<Union>x\<in>A. Collect(B(x), P))" 
fac77a839aa2
Tidying up. Mainly moving proofs from Main.thy to other (Isar) theory files.
paulson
parents:
13178
diff
changeset

953 
by blast 
fac77a839aa2
Tidying up. Mainly moving proofs from Main.thy to other (Isar) theory files.
paulson
parents:
13178
diff
changeset

954 

46820  955 
lemma Collect_Int_left: "{x\<in>A. P(x)} \<inter> B = {x \<in> A \<inter> B. P(x)}" 
14084
ccb48f3239f7
Removal of UNITY/UNITYMisc, moving its theorems elsewhere.
paulson
parents:
14077
diff
changeset

956 
by blast 
ccb48f3239f7
Removal of UNITY/UNITYMisc, moving its theorems elsewhere.
paulson
parents:
14077
diff
changeset

957 

46820  958 
lemma Collect_Int_right: "A \<inter> {x\<in>B. P(x)} = {x \<in> A \<inter> B. P(x)}" 
14084
ccb48f3239f7
Removal of UNITY/UNITYMisc, moving its theorems elsewhere.
paulson
parents:
14077
diff
changeset

959 
by blast 
ccb48f3239f7
Removal of UNITY/UNITYMisc, moving its theorems elsewhere.
paulson
parents:
14077
diff
changeset

960 

46820  961 
lemma Collect_disj_eq: "{x\<in>A. P(x)  Q(x)} = Collect(A, P) \<union> Collect(A, Q)" 
14084
ccb48f3239f7
Removal of UNITY/UNITYMisc, moving its theorems elsewhere.
paulson
parents:
14077
diff
changeset

962 
by blast 
ccb48f3239f7
Removal of UNITY/UNITYMisc, moving its theorems elsewhere.
paulson
parents:
14077
diff
changeset

963 

46820  964 
lemma Collect_conj_eq: "{x\<in>A. P(x) & Q(x)} = Collect(A, P) \<inter> Collect(A, Q)" 
14084
ccb48f3239f7
Removal of UNITY/UNITYMisc, moving its theorems elsewhere.
paulson
parents:
14077
diff
changeset

965 
by blast 
ccb48f3239f7
Removal of UNITY/UNITYMisc, moving its theorems elsewhere.
paulson
parents:
14077
diff
changeset

966 

46820  967 
lemmas subset_SIs = subset_refl cons_subsetI subset_consI 
968 
Union_least UN_least Un_least 

13259  969 
Inter_greatest Int_greatest RepFun_subset 
970 
Un_upper1 Un_upper2 Int_lower1 Int_lower2 

971 

24893  972 
ML {* 
42793  973 
val subset_cs = 
974 
claset_of (@{context} 

24893  975 
delrules [@{thm subsetI}, @{thm subsetCE}] 
976 
addSIs @{thms subset_SIs} 

977 
addIs [@{thm Union_upper}, @{thm Inter_lower}] 

42793  978 
addSEs [@{thm cons_subsetE}]); 
13259  979 

42793  980 
val ZF_cs = claset_of (@{context} delrules [@{thm equalityI}]); 
13165  981 
*} 
46820  982 

13165  983 
end 
984 