1(* Title: HOL/Complete_Lattices.thy 2 Author: Tobias Nipkow 3 Author: Lawrence C Paulson 4 Author: Markus Wenzel 5 Author: Florian Haftmann 6 Author: Viorel Preoteasa (Complete Distributive Lattices) 7*) 8 9section \<open>Complete lattices\<close> 10 11theory Complete_Lattices 12 imports Fun 13begin 14 15subsection \<open>Syntactic infimum and supremum operations\<close> 16 17class Inf = 18 fixes Inf :: "'a set \<Rightarrow> 'a" ("\<Sqinter>") 19 20class Sup = 21 fixes Sup :: "'a set \<Rightarrow> 'a" ("\<Squnion>") 22 23syntax 24 "_INF1" :: "pttrns \<Rightarrow> 'b \<Rightarrow> 'b" ("(3INF _./ _)" [0, 10] 10) 25 "_INF" :: "pttrn \<Rightarrow> 'a set \<Rightarrow> 'b \<Rightarrow> 'b" ("(3INF _\<in>_./ _)" [0, 0, 10] 10) 26 "_SUP1" :: "pttrns \<Rightarrow> 'b \<Rightarrow> 'b" ("(3SUP _./ _)" [0, 10] 10) 27 "_SUP" :: "pttrn \<Rightarrow> 'a set \<Rightarrow> 'b \<Rightarrow> 'b" ("(3SUP _\<in>_./ _)" [0, 0, 10] 10) 28 29syntax 30 "_INF1" :: "pttrns \<Rightarrow> 'b \<Rightarrow> 'b" ("(3\<Sqinter>_./ _)" [0, 10] 10) 31 "_INF" :: "pttrn \<Rightarrow> 'a set \<Rightarrow> 'b \<Rightarrow> 'b" ("(3\<Sqinter>_\<in>_./ _)" [0, 0, 10] 10) 32 "_SUP1" :: "pttrns \<Rightarrow> 'b \<Rightarrow> 'b" ("(3\<Squnion>_./ _)" [0, 10] 10) 33 "_SUP" :: "pttrn \<Rightarrow> 'a set \<Rightarrow> 'b \<Rightarrow> 'b" ("(3\<Squnion>_\<in>_./ _)" [0, 0, 10] 10) 34 35translations 36 "\<Sqinter>x y. f" \<rightleftharpoons> "\<Sqinter>x. \<Sqinter>y. f" 37 "\<Sqinter>x. f" \<rightleftharpoons> "\<Sqinter>(CONST range (\<lambda>x. f))" 38 "\<Sqinter>x\<in>A. f" \<rightleftharpoons> "CONST Inf ((\<lambda>x. f) ` A)" 39 "\<Squnion>x y. f" \<rightleftharpoons> "\<Squnion>x. \<Squnion>y. f" 40 "\<Squnion>x. f" \<rightleftharpoons> "\<Squnion>(CONST range (\<lambda>x. f))" 41 "\<Squnion>x\<in>A. f" \<rightleftharpoons> "CONST Sup ((\<lambda>x. f) ` A)" 42 43context Inf 44begin 45 46lemma INF_image: "\<Sqinter> (g ` f ` A) = \<Sqinter> ((g \<circ> f) ` A)" 47 by (simp add: image_comp) 48 49lemma INF_identity_eq [simp]: "(\<Sqinter>x\<in>A. x) = \<Sqinter>A" 50 by simp 51 52lemma INF_id_eq [simp]: "\<Sqinter>(id ` A) = \<Sqinter>A" 53 by simp 54 55lemma INF_cong: "A = B \<Longrightarrow> (\<And>x. x \<in> B \<Longrightarrow> C x = D x) \<Longrightarrow> \<Sqinter>(C ` A) = \<Sqinter>(D ` B)" 56 by (simp add: image_def) 57 58lemma INF_cong_simp: 59 "A = B \<Longrightarrow> (\<And>x. x \<in> B =simp=> C x = D x) \<Longrightarrow> \<Sqinter>(C ` A) = \<Sqinter>(D ` B)" 60 unfolding simp_implies_def by (fact INF_cong) 61 62end 63 64context Sup 65begin 66 67lemma SUP_image: "\<Squnion> (g ` f ` A) = \<Squnion> ((g \<circ> f) ` A)" 68by(fact Inf.INF_image) 69 70lemma SUP_identity_eq [simp]: "(\<Squnion>x\<in>A. x) = \<Squnion>A" 71by(fact Inf.INF_identity_eq) 72 73lemma SUP_id_eq [simp]: "\<Squnion>(id ` A) = \<Squnion>A" 74by(fact Inf.INF_id_eq) 75 76lemma SUP_cong: "A = B \<Longrightarrow> (\<And>x. x \<in> B \<Longrightarrow> C x = D x) \<Longrightarrow> \<Squnion>(C ` A) = \<Squnion>(D ` B)" 77by (fact Inf.INF_cong) 78 79lemma SUP_cong_simp: 80 "A = B \<Longrightarrow> (\<And>x. x \<in> B =simp=> C x = D x) \<Longrightarrow> \<Squnion>(C ` A) = \<Squnion>(D ` B)" 81by (fact Inf.INF_cong_simp) 82 83end 84 85 86subsection \<open>Abstract complete lattices\<close> 87 88text \<open>A complete lattice always has a bottom and a top, 89so we include them into the following type class, 90along with assumptions that define bottom and top 91in terms of infimum and supremum.\<close> 92 93class complete_lattice = lattice + Inf + Sup + bot + top + 94 assumes Inf_lower: "x \<in> A \<Longrightarrow> \<Sqinter>A \<le> x" 95 and Inf_greatest: "(\<And>x. x \<in> A \<Longrightarrow> z \<le> x) \<Longrightarrow> z \<le> \<Sqinter>A" 96 and Sup_upper: "x \<in> A \<Longrightarrow> x \<le> \<Squnion>A" 97 and Sup_least: "(\<And>x. x \<in> A \<Longrightarrow> x \<le> z) \<Longrightarrow> \<Squnion>A \<le> z" 98 and Inf_empty [simp]: "\<Sqinter>{} = \<top>" 99 and Sup_empty [simp]: "\<Squnion>{} = \<bottom>" 100begin 101 102subclass bounded_lattice 103proof 104 fix a 105 show "\<bottom> \<le> a" 106 by (auto intro: Sup_least simp only: Sup_empty [symmetric]) 107 show "a \<le> \<top>" 108 by (auto intro: Inf_greatest simp only: Inf_empty [symmetric]) 109qed 110 111lemma dual_complete_lattice: "class.complete_lattice Sup Inf sup (\<ge>) (>) inf \<top> \<bottom>" 112 by (auto intro!: class.complete_lattice.intro dual_lattice) 113 (unfold_locales, (fact Inf_empty Sup_empty Sup_upper Sup_least Inf_lower Inf_greatest)+) 114 115end 116 117context complete_lattice 118begin 119 120lemma Sup_eqI: 121 "(\<And>y. y \<in> A \<Longrightarrow> y \<le> x) \<Longrightarrow> (\<And>y. (\<And>z. z \<in> A \<Longrightarrow> z \<le> y) \<Longrightarrow> x \<le> y) \<Longrightarrow> \<Squnion>A = x" 122 by (blast intro: antisym Sup_least Sup_upper) 123 124lemma Inf_eqI: 125 "(\<And>i. i \<in> A \<Longrightarrow> x \<le> i) \<Longrightarrow> (\<And>y. (\<And>i. i \<in> A \<Longrightarrow> y \<le> i) \<Longrightarrow> y \<le> x) \<Longrightarrow> \<Sqinter>A = x" 126 by (blast intro: antisym Inf_greatest Inf_lower) 127 128lemma SUP_eqI: 129 "(\<And>i. i \<in> A \<Longrightarrow> f i \<le> x) \<Longrightarrow> (\<And>y. (\<And>i. i \<in> A \<Longrightarrow> f i \<le> y) \<Longrightarrow> x \<le> y) \<Longrightarrow> (\<Squnion>i\<in>A. f i) = x" 130 using Sup_eqI [of "f ` A" x] by auto 131 132lemma INF_eqI: 133 "(\<And>i. i \<in> A \<Longrightarrow> x \<le> f i) \<Longrightarrow> (\<And>y. (\<And>i. i \<in> A \<Longrightarrow> f i \<ge> y) \<Longrightarrow> x \<ge> y) \<Longrightarrow> (\<Sqinter>i\<in>A. f i) = x" 134 using Inf_eqI [of "f ` A" x] by auto 135 136lemma INF_lower: "i \<in> A \<Longrightarrow> (\<Sqinter>i\<in>A. f i) \<le> f i" 137 using Inf_lower [of _ "f ` A"] by simp 138 139lemma INF_greatest: "(\<And>i. i \<in> A \<Longrightarrow> u \<le> f i) \<Longrightarrow> u \<le> (\<Sqinter>i\<in>A. f i)" 140 using Inf_greatest [of "f ` A"] by auto 141 142lemma SUP_upper: "i \<in> A \<Longrightarrow> f i \<le> (\<Squnion>i\<in>A. f i)" 143 using Sup_upper [of _ "f ` A"] by simp 144 145lemma SUP_least: "(\<And>i. i \<in> A \<Longrightarrow> f i \<le> u) \<Longrightarrow> (\<Squnion>i\<in>A. f i) \<le> u" 146 using Sup_least [of "f ` A"] by auto 147 148lemma Inf_lower2: "u \<in> A \<Longrightarrow> u \<le> v \<Longrightarrow> \<Sqinter>A \<le> v" 149 using Inf_lower [of u A] by auto 150 151lemma INF_lower2: "i \<in> A \<Longrightarrow> f i \<le> u \<Longrightarrow> (\<Sqinter>i\<in>A. f i) \<le> u" 152 using INF_lower [of i A f] by auto 153 154lemma Sup_upper2: "u \<in> A \<Longrightarrow> v \<le> u \<Longrightarrow> v \<le> \<Squnion>A" 155 using Sup_upper [of u A] by auto 156 157lemma SUP_upper2: "i \<in> A \<Longrightarrow> u \<le> f i \<Longrightarrow> u \<le> (\<Squnion>i\<in>A. f i)" 158 using SUP_upper [of i A f] by auto 159 160lemma le_Inf_iff: "b \<le> \<Sqinter>A \<longleftrightarrow> (\<forall>a\<in>A. b \<le> a)" 161 by (auto intro: Inf_greatest dest: Inf_lower) 162 163lemma le_INF_iff: "u \<le> (\<Sqinter>i\<in>A. f i) \<longleftrightarrow> (\<forall>i\<in>A. u \<le> f i)" 164 using le_Inf_iff [of _ "f ` A"] by simp 165 166lemma Sup_le_iff: "\<Squnion>A \<le> b \<longleftrightarrow> (\<forall>a\<in>A. a \<le> b)" 167 by (auto intro: Sup_least dest: Sup_upper) 168 169lemma SUP_le_iff: "(\<Squnion>i\<in>A. f i) \<le> u \<longleftrightarrow> (\<forall>i\<in>A. f i \<le> u)" 170 using Sup_le_iff [of "f ` A"] by simp 171 172lemma Inf_insert [simp]: "\<Sqinter>(insert a A) = a \<sqinter> \<Sqinter>A" 173 by (auto intro: le_infI le_infI1 le_infI2 antisym Inf_greatest Inf_lower) 174 175lemma INF_insert: "(\<Sqinter>x\<in>insert a A. f x) = f a \<sqinter> \<Sqinter>(f ` A)" 176 by simp 177 178lemma Sup_insert [simp]: "\<Squnion>(insert a A) = a \<squnion> \<Squnion>A" 179 by (auto intro: le_supI le_supI1 le_supI2 antisym Sup_least Sup_upper) 180 181lemma SUP_insert: "(\<Squnion>x\<in>insert a A. f x) = f a \<squnion> \<Squnion>(f ` A)" 182 by simp 183 184lemma INF_empty: "(\<Sqinter>x\<in>{}. f x) = \<top>" 185 by simp 186 187lemma SUP_empty: "(\<Squnion>x\<in>{}. f x) = \<bottom>" 188 by simp 189 190lemma Inf_UNIV [simp]: "\<Sqinter>UNIV = \<bottom>" 191 by (auto intro!: antisym Inf_lower) 192 193lemma Sup_UNIV [simp]: "\<Squnion>UNIV = \<top>" 194 by (auto intro!: antisym Sup_upper) 195 196lemma Inf_eq_Sup: "\<Sqinter>A = \<Squnion>{b. \<forall>a \<in> A. b \<le> a}" 197 by (auto intro: antisym Inf_lower Inf_greatest Sup_upper Sup_least) 198 199lemma Sup_eq_Inf: "\<Squnion>A = \<Sqinter>{b. \<forall>a \<in> A. a \<le> b}" 200 by (auto intro: antisym Inf_lower Inf_greatest Sup_upper Sup_least) 201 202lemma Inf_superset_mono: "B \<subseteq> A \<Longrightarrow> \<Sqinter>A \<le> \<Sqinter>B" 203 by (auto intro: Inf_greatest Inf_lower) 204 205lemma Sup_subset_mono: "A \<subseteq> B \<Longrightarrow> \<Squnion>A \<le> \<Squnion>B" 206 by (auto intro: Sup_least Sup_upper) 207 208lemma Inf_mono: 209 assumes "\<And>b. b \<in> B \<Longrightarrow> \<exists>a\<in>A. a \<le> b" 210 shows "\<Sqinter>A \<le> \<Sqinter>B" 211proof (rule Inf_greatest) 212 fix b assume "b \<in> B" 213 with assms obtain a where "a \<in> A" and "a \<le> b" by blast 214 from \<open>a \<in> A\<close> have "\<Sqinter>A \<le> a" by (rule Inf_lower) 215 with \<open>a \<le> b\<close> show "\<Sqinter>A \<le> b" by auto 216qed 217 218lemma INF_mono: "(\<And>m. m \<in> B \<Longrightarrow> \<exists>n\<in>A. f n \<le> g m) \<Longrightarrow> (\<Sqinter>n\<in>A. f n) \<le> (\<Sqinter>n\<in>B. g n)" 219 using Inf_mono [of "g ` B" "f ` A"] by auto 220 221lemma INF_mono': "(\<And>x. f x \<le> g x) \<Longrightarrow> (\<Sqinter>x\<in>A. f x) \<le> (\<Sqinter>x\<in>A. g x)" 222 by (rule INF_mono) auto 223 224lemma Sup_mono: 225 assumes "\<And>a. a \<in> A \<Longrightarrow> \<exists>b\<in>B. a \<le> b" 226 shows "\<Squnion>A \<le> \<Squnion>B" 227proof (rule Sup_least) 228 fix a assume "a \<in> A" 229 with assms obtain b where "b \<in> B" and "a \<le> b" by blast 230 from \<open>b \<in> B\<close> have "b \<le> \<Squnion>B" by (rule Sup_upper) 231 with \<open>a \<le> b\<close> show "a \<le> \<Squnion>B" by auto 232qed 233 234lemma SUP_mono: "(\<And>n. n \<in> A \<Longrightarrow> \<exists>m\<in>B. f n \<le> g m) \<Longrightarrow> (\<Squnion>n\<in>A. f n) \<le> (\<Squnion>n\<in>B. g n)" 235 using Sup_mono [of "f ` A" "g ` B"] by auto 236 237lemma SUP_mono': "(\<And>x. f x \<le> g x) \<Longrightarrow> (\<Squnion>x\<in>A. f x) \<le> (\<Squnion>x\<in>A. g x)" 238 by (rule SUP_mono) auto 239 240lemma INF_superset_mono: "B \<subseteq> A \<Longrightarrow> (\<And>x. x \<in> B \<Longrightarrow> f x \<le> g x) \<Longrightarrow> (\<Sqinter>x\<in>A. f x) \<le> (\<Sqinter>x\<in>B. g x)" 241 \<comment> \<open>The last inclusion is POSITIVE!\<close> 242 by (blast intro: INF_mono dest: subsetD) 243 244lemma SUP_subset_mono: "A \<subseteq> B \<Longrightarrow> (\<And>x. x \<in> A \<Longrightarrow> f x \<le> g x) \<Longrightarrow> (\<Squnion>x\<in>A. f x) \<le> (\<Squnion>x\<in>B. g x)" 245 by (blast intro: SUP_mono dest: subsetD) 246 247lemma Inf_less_eq: 248 assumes "\<And>v. v \<in> A \<Longrightarrow> v \<le> u" 249 and "A \<noteq> {}" 250 shows "\<Sqinter>A \<le> u" 251proof - 252 from \<open>A \<noteq> {}\<close> obtain v where "v \<in> A" by blast 253 moreover from \<open>v \<in> A\<close> assms(1) have "v \<le> u" by blast 254 ultimately show ?thesis by (rule Inf_lower2) 255qed 256 257lemma less_eq_Sup: 258 assumes "\<And>v. v \<in> A \<Longrightarrow> u \<le> v" 259 and "A \<noteq> {}" 260 shows "u \<le> \<Squnion>A" 261proof - 262 from \<open>A \<noteq> {}\<close> obtain v where "v \<in> A" by blast 263 moreover from \<open>v \<in> A\<close> assms(1) have "u \<le> v" by blast 264 ultimately show ?thesis by (rule Sup_upper2) 265qed 266 267lemma INF_eq: 268 assumes "\<And>i. i \<in> A \<Longrightarrow> \<exists>j\<in>B. f i \<ge> g j" 269 and "\<And>j. j \<in> B \<Longrightarrow> \<exists>i\<in>A. g j \<ge> f i" 270 shows "\<Sqinter>(f ` A) = \<Sqinter>(g ` B)" 271 by (intro antisym INF_greatest) (blast intro: INF_lower2 dest: assms)+ 272 273lemma SUP_eq: 274 assumes "\<And>i. i \<in> A \<Longrightarrow> \<exists>j\<in>B. f i \<le> g j" 275 and "\<And>j. j \<in> B \<Longrightarrow> \<exists>i\<in>A. g j \<le> f i" 276 shows "\<Squnion>(f ` A) = \<Squnion>(g ` B)" 277 by (intro antisym SUP_least) (blast intro: SUP_upper2 dest: assms)+ 278 279lemma less_eq_Inf_inter: "\<Sqinter>A \<squnion> \<Sqinter>B \<le> \<Sqinter>(A \<inter> B)" 280 by (auto intro: Inf_greatest Inf_lower) 281 282lemma Sup_inter_less_eq: "\<Squnion>(A \<inter> B) \<le> \<Squnion>A \<sqinter> \<Squnion>B " 283 by (auto intro: Sup_least Sup_upper) 284 285lemma Inf_union_distrib: "\<Sqinter>(A \<union> B) = \<Sqinter>A \<sqinter> \<Sqinter>B" 286 by (rule antisym) (auto intro: Inf_greatest Inf_lower le_infI1 le_infI2) 287 288lemma INF_union: "(\<Sqinter>i \<in> A \<union> B. M i) = (\<Sqinter>i \<in> A. M i) \<sqinter> (\<Sqinter>i\<in>B. M i)" 289 by (auto intro!: antisym INF_mono intro: le_infI1 le_infI2 INF_greatest INF_lower) 290 291lemma Sup_union_distrib: "\<Squnion>(A \<union> B) = \<Squnion>A \<squnion> \<Squnion>B" 292 by (rule antisym) (auto intro: Sup_least Sup_upper le_supI1 le_supI2) 293 294lemma SUP_union: "(\<Squnion>i \<in> A \<union> B. M i) = (\<Squnion>i \<in> A. M i) \<squnion> (\<Squnion>i\<in>B. M i)" 295 by (auto intro!: antisym SUP_mono intro: le_supI1 le_supI2 SUP_least SUP_upper) 296 297lemma INF_inf_distrib: "(\<Sqinter>a\<in>A. f a) \<sqinter> (\<Sqinter>a\<in>A. g a) = (\<Sqinter>a\<in>A. f a \<sqinter> g a)" 298 by (rule antisym) (rule INF_greatest, auto intro: le_infI1 le_infI2 INF_lower INF_mono) 299 300lemma SUP_sup_distrib: "(\<Squnion>a\<in>A. f a) \<squnion> (\<Squnion>a\<in>A. g a) = (\<Squnion>a\<in>A. f a \<squnion> g a)" 301 (is "?L = ?R") 302proof (rule antisym) 303 show "?L \<le> ?R" 304 by (auto intro: le_supI1 le_supI2 SUP_upper SUP_mono) 305 show "?R \<le> ?L" 306 by (rule SUP_least) (auto intro: le_supI1 le_supI2 SUP_upper) 307qed 308 309lemma Inf_top_conv [simp]: 310 "\<Sqinter>A = \<top> \<longleftrightarrow> (\<forall>x\<in>A. x = \<top>)" 311 "\<top> = \<Sqinter>A \<longleftrightarrow> (\<forall>x\<in>A. x = \<top>)" 312proof - 313 show "\<Sqinter>A = \<top> \<longleftrightarrow> (\<forall>x\<in>A. x = \<top>)" 314 proof 315 assume "\<forall>x\<in>A. x = \<top>" 316 then have "A = {} \<or> A = {\<top>}" by auto 317 then show "\<Sqinter>A = \<top>" by auto 318 next 319 assume "\<Sqinter>A = \<top>" 320 show "\<forall>x\<in>A. x = \<top>" 321 proof (rule ccontr) 322 assume "\<not> (\<forall>x\<in>A. x = \<top>)" 323 then obtain x where "x \<in> A" and "x \<noteq> \<top>" by blast 324 then obtain B where "A = insert x B" by blast 325 with \<open>\<Sqinter>A = \<top>\<close> \<open>x \<noteq> \<top>\<close> show False by simp 326 qed 327 qed 328 then show "\<top> = \<Sqinter>A \<longleftrightarrow> (\<forall>x\<in>A. x = \<top>)" by auto 329qed 330 331lemma INF_top_conv [simp]: 332 "(\<Sqinter>x\<in>A. B x) = \<top> \<longleftrightarrow> (\<forall>x\<in>A. B x = \<top>)" 333 "\<top> = (\<Sqinter>x\<in>A. B x) \<longleftrightarrow> (\<forall>x\<in>A. B x = \<top>)" 334 using Inf_top_conv [of "B ` A"] by simp_all 335 336lemma Sup_bot_conv [simp]: 337 "\<Squnion>A = \<bottom> \<longleftrightarrow> (\<forall>x\<in>A. x = \<bottom>)" 338 "\<bottom> = \<Squnion>A \<longleftrightarrow> (\<forall>x\<in>A. x = \<bottom>)" 339 using dual_complete_lattice 340 by (rule complete_lattice.Inf_top_conv)+ 341 342lemma SUP_bot_conv [simp]: 343 "(\<Squnion>x\<in>A. B x) = \<bottom> \<longleftrightarrow> (\<forall>x\<in>A. B x = \<bottom>)" 344 "\<bottom> = (\<Squnion>x\<in>A. B x) \<longleftrightarrow> (\<forall>x\<in>A. B x = \<bottom>)" 345 using Sup_bot_conv [of "B ` A"] by simp_all 346 347lemma INF_const [simp]: "A \<noteq> {} \<Longrightarrow> (\<Sqinter>i\<in>A. f) = f" 348 by (auto intro: antisym INF_lower INF_greatest) 349 350lemma SUP_const [simp]: "A \<noteq> {} \<Longrightarrow> (\<Squnion>i\<in>A. f) = f" 351 by (auto intro: antisym SUP_upper SUP_least) 352 353lemma INF_top [simp]: "(\<Sqinter>x\<in>A. \<top>) = \<top>" 354 by (cases "A = {}") simp_all 355 356lemma SUP_bot [simp]: "(\<Squnion>x\<in>A. \<bottom>) = \<bottom>" 357 by (cases "A = {}") simp_all 358 359lemma INF_commute: "(\<Sqinter>i\<in>A. \<Sqinter>j\<in>B. f i j) = (\<Sqinter>j\<in>B. \<Sqinter>i\<in>A. f i j)" 360 by (iprover intro: INF_lower INF_greatest order_trans antisym) 361 362lemma SUP_commute: "(\<Squnion>i\<in>A. \<Squnion>j\<in>B. f i j) = (\<Squnion>j\<in>B. \<Squnion>i\<in>A. f i j)" 363 by (iprover intro: SUP_upper SUP_least order_trans antisym) 364 365lemma INF_absorb: 366 assumes "k \<in> I" 367 shows "A k \<sqinter> (\<Sqinter>i\<in>I. A i) = (\<Sqinter>i\<in>I. A i)" 368proof - 369 from assms obtain J where "I = insert k J" by blast 370 then show ?thesis by simp 371qed 372 373lemma SUP_absorb: 374 assumes "k \<in> I" 375 shows "A k \<squnion> (\<Squnion>i\<in>I. A i) = (\<Squnion>i\<in>I. A i)" 376proof - 377 from assms obtain J where "I = insert k J" by blast 378 then show ?thesis by simp 379qed 380 381lemma INF_inf_const1: "I \<noteq> {} \<Longrightarrow> (\<Sqinter>i\<in>I. inf x (f i)) = inf x (\<Sqinter>i\<in>I. f i)" 382 by (intro antisym INF_greatest inf_mono order_refl INF_lower) 383 (auto intro: INF_lower2 le_infI2 intro!: INF_mono) 384 385lemma INF_inf_const2: "I \<noteq> {} \<Longrightarrow> (\<Sqinter>i\<in>I. inf (f i) x) = inf (\<Sqinter>i\<in>I. f i) x" 386 using INF_inf_const1[of I x f] by (simp add: inf_commute) 387 388lemma INF_constant: "(\<Sqinter>y\<in>A. c) = (if A = {} then \<top> else c)" 389 by simp 390 391lemma SUP_constant: "(\<Squnion>y\<in>A. c) = (if A = {} then \<bottom> else c)" 392 by simp 393 394lemma less_INF_D: 395 assumes "y < (\<Sqinter>i\<in>A. f i)" "i \<in> A" 396 shows "y < f i" 397proof - 398 note \<open>y < (\<Sqinter>i\<in>A. f i)\<close> 399 also have "(\<Sqinter>i\<in>A. f i) \<le> f i" using \<open>i \<in> A\<close> 400 by (rule INF_lower) 401 finally show "y < f i" . 402qed 403 404lemma SUP_lessD: 405 assumes "(\<Squnion>i\<in>A. f i) < y" "i \<in> A" 406 shows "f i < y" 407proof - 408 have "f i \<le> (\<Squnion>i\<in>A. f i)" 409 using \<open>i \<in> A\<close> by (rule SUP_upper) 410 also note \<open>(\<Squnion>i\<in>A. f i) < y\<close> 411 finally show "f i < y" . 412qed 413 414lemma INF_UNIV_bool_expand: "(\<Sqinter>b. A b) = A True \<sqinter> A False" 415 by (simp add: UNIV_bool inf_commute) 416 417lemma SUP_UNIV_bool_expand: "(\<Squnion>b. A b) = A True \<squnion> A False" 418 by (simp add: UNIV_bool sup_commute) 419 420lemma Inf_le_Sup: "A \<noteq> {} \<Longrightarrow> Inf A \<le> Sup A" 421 by (blast intro: Sup_upper2 Inf_lower ex_in_conv) 422 423lemma INF_le_SUP: "A \<noteq> {} \<Longrightarrow> \<Sqinter>(f ` A) \<le> \<Squnion>(f ` A)" 424 using Inf_le_Sup [of "f ` A"] by simp 425 426lemma INF_eq_const: "I \<noteq> {} \<Longrightarrow> (\<And>i. i \<in> I \<Longrightarrow> f i = x) \<Longrightarrow> \<Sqinter>(f ` I) = x" 427 by (auto intro: INF_eqI) 428 429lemma SUP_eq_const: "I \<noteq> {} \<Longrightarrow> (\<And>i. i \<in> I \<Longrightarrow> f i = x) \<Longrightarrow> \<Squnion>(f ` I) = x" 430 by (auto intro: SUP_eqI) 431 432lemma INF_eq_iff: "I \<noteq> {} \<Longrightarrow> (\<And>i. i \<in> I \<Longrightarrow> f i \<le> c) \<Longrightarrow> \<Sqinter>(f ` I) = c \<longleftrightarrow> (\<forall>i\<in>I. f i = c)" 433 by (auto intro: INF_eq_const INF_lower antisym) 434 435lemma SUP_eq_iff: "I \<noteq> {} \<Longrightarrow> (\<And>i. i \<in> I \<Longrightarrow> c \<le> f i) \<Longrightarrow> \<Squnion>(f ` I) = c \<longleftrightarrow> (\<forall>i\<in>I. f i = c)" 436 by (auto intro: SUP_eq_const SUP_upper antisym) 437 438end 439 440context complete_lattice 441begin 442lemma Sup_Inf_le: "Sup (Inf ` {f ` A | f . (\<forall> Y \<in> A . f Y \<in> Y)}) \<le> Inf (Sup ` A)" 443 by (rule SUP_least, clarify, rule INF_greatest, simp add: INF_lower2 Sup_upper) 444end 445 446class complete_distrib_lattice = complete_lattice + 447 assumes Inf_Sup_le: "Inf (Sup ` A) \<le> Sup (Inf ` {f ` A | f . (\<forall> Y \<in> A . f Y \<in> Y)})" 448begin 449 450lemma Inf_Sup: "Inf (Sup ` A) = Sup (Inf ` {f ` A | f . (\<forall> Y \<in> A . f Y \<in> Y)})" 451 by (rule antisym, rule Inf_Sup_le, rule Sup_Inf_le) 452 453subclass distrib_lattice 454proof 455 fix a b c 456 show "a \<squnion> b \<sqinter> c = (a \<squnion> b) \<sqinter> (a \<squnion> c)" 457 proof (rule antisym, simp_all, safe) 458 show "b \<sqinter> c \<le> a \<squnion> b" 459 by (rule le_infI1, simp) 460 show "b \<sqinter> c \<le> a \<squnion> c" 461 by (rule le_infI2, simp) 462 have [simp]: "a \<sqinter> c \<le> a \<squnion> b \<sqinter> c" 463 by (rule le_infI1, simp) 464 have [simp]: "b \<sqinter> a \<le> a \<squnion> b \<sqinter> c" 465 by (rule le_infI2, simp) 466 have "\<Sqinter>(Sup ` {{a, b}, {a, c}}) = 467 \<Squnion>(Inf ` {f ` {{a, b}, {a, c}} | f. \<forall>Y\<in>{{a, b}, {a, c}}. f Y \<in> Y})" 468 by (rule Inf_Sup) 469 from this show "(a \<squnion> b) \<sqinter> (a \<squnion> c) \<le> a \<squnion> b \<sqinter> c" 470 apply simp 471 by (rule SUP_least, safe, simp_all) 472 qed 473qed 474end 475 476context complete_lattice 477begin 478context 479 fixes f :: "'a \<Rightarrow> 'b::complete_lattice" 480 assumes "mono f" 481begin 482 483lemma mono_Inf: "f (\<Sqinter>A) \<le> (\<Sqinter>x\<in>A. f x)" 484 using \<open>mono f\<close> by (auto intro: complete_lattice_class.INF_greatest Inf_lower dest: monoD) 485 486lemma mono_Sup: "(\<Squnion>x\<in>A. f x) \<le> f (\<Squnion>A)" 487 using \<open>mono f\<close> by (auto intro: complete_lattice_class.SUP_least Sup_upper dest: monoD) 488 489lemma mono_INF: "f (\<Sqinter>i\<in>I. A i) \<le> (\<Sqinter>x\<in>I. f (A x))" 490 by (intro complete_lattice_class.INF_greatest monoD[OF \<open>mono f\<close>] INF_lower) 491 492lemma mono_SUP: "(\<Squnion>x\<in>I. f (A x)) \<le> f (\<Squnion>i\<in>I. A i)" 493 by (intro complete_lattice_class.SUP_least monoD[OF \<open>mono f\<close>] SUP_upper) 494 495end 496 497end 498 499class complete_boolean_algebra = boolean_algebra + complete_distrib_lattice 500begin 501 502lemma uminus_Inf: "- (\<Sqinter>A) = \<Squnion>(uminus ` A)" 503proof (rule antisym) 504 show "- \<Sqinter>A \<le> \<Squnion>(uminus ` A)" 505 by (rule compl_le_swap2, rule Inf_greatest, rule compl_le_swap2, rule Sup_upper) simp 506 show "\<Squnion>(uminus ` A) \<le> - \<Sqinter>A" 507 by (rule Sup_least, rule compl_le_swap1, rule Inf_lower) auto 508qed 509 510lemma uminus_INF: "- (\<Sqinter>x\<in>A. B x) = (\<Squnion>x\<in>A. - B x)" 511 by (simp add: uminus_Inf image_image) 512 513lemma uminus_Sup: "- (\<Squnion>A) = \<Sqinter>(uminus ` A)" 514proof - 515 have "\<Squnion>A = - \<Sqinter>(uminus ` A)" 516 by (simp add: image_image uminus_INF) 517 then show ?thesis by simp 518qed 519 520lemma uminus_SUP: "- (\<Squnion>x\<in>A. B x) = (\<Sqinter>x\<in>A. - B x)" 521 by (simp add: uminus_Sup image_image) 522 523end 524 525class complete_linorder = linorder + complete_lattice 526begin 527 528lemma dual_complete_linorder: 529 "class.complete_linorder Sup Inf sup (\<ge>) (>) inf \<top> \<bottom>" 530 by (rule class.complete_linorder.intro, rule dual_complete_lattice, rule dual_linorder) 531 532lemma complete_linorder_inf_min: "inf = min" 533 by (auto intro: antisym simp add: min_def fun_eq_iff) 534 535lemma complete_linorder_sup_max: "sup = max" 536 by (auto intro: antisym simp add: max_def fun_eq_iff) 537 538lemma Inf_less_iff: "\<Sqinter>S < a \<longleftrightarrow> (\<exists>x\<in>S. x < a)" 539 by (simp add: not_le [symmetric] le_Inf_iff) 540 541lemma INF_less_iff: "(\<Sqinter>i\<in>A. f i) < a \<longleftrightarrow> (\<exists>x\<in>A. f x < a)" 542 by (simp add: Inf_less_iff [of "f ` A"]) 543 544lemma less_Sup_iff: "a < \<Squnion>S \<longleftrightarrow> (\<exists>x\<in>S. a < x)" 545 by (simp add: not_le [symmetric] Sup_le_iff) 546 547lemma less_SUP_iff: "a < (\<Squnion>i\<in>A. f i) \<longleftrightarrow> (\<exists>x\<in>A. a < f x)" 548 by (simp add: less_Sup_iff [of _ "f ` A"]) 549 550lemma Sup_eq_top_iff [simp]: "\<Squnion>A = \<top> \<longleftrightarrow> (\<forall>x<\<top>. \<exists>i\<in>A. x < i)" 551proof 552 assume *: "\<Squnion>A = \<top>" 553 show "(\<forall>x<\<top>. \<exists>i\<in>A. x < i)" 554 unfolding * [symmetric] 555 proof (intro allI impI) 556 fix x 557 assume "x < \<Squnion>A" 558 then show "\<exists>i\<in>A. x < i" 559 by (simp add: less_Sup_iff) 560 qed 561next 562 assume *: "\<forall>x<\<top>. \<exists>i\<in>A. x < i" 563 show "\<Squnion>A = \<top>" 564 proof (rule ccontr) 565 assume "\<Squnion>A \<noteq> \<top>" 566 with top_greatest [of "\<Squnion>A"] have "\<Squnion>A < \<top>" 567 unfolding le_less by auto 568 with * have "\<Squnion>A < \<Squnion>A" 569 unfolding less_Sup_iff by auto 570 then show False by auto 571 qed 572qed 573 574lemma SUP_eq_top_iff [simp]: "(\<Squnion>i\<in>A. f i) = \<top> \<longleftrightarrow> (\<forall>x<\<top>. \<exists>i\<in>A. x < f i)" 575 using Sup_eq_top_iff [of "f ` A"] by simp 576 577lemma Inf_eq_bot_iff [simp]: "\<Sqinter>A = \<bottom> \<longleftrightarrow> (\<forall>x>\<bottom>. \<exists>i\<in>A. i < x)" 578 using dual_complete_linorder 579 by (rule complete_linorder.Sup_eq_top_iff) 580 581lemma INF_eq_bot_iff [simp]: "(\<Sqinter>i\<in>A. f i) = \<bottom> \<longleftrightarrow> (\<forall>x>\<bottom>. \<exists>i\<in>A. f i < x)" 582 using Inf_eq_bot_iff [of "f ` A"] by simp 583 584lemma Inf_le_iff: "\<Sqinter>A \<le> x \<longleftrightarrow> (\<forall>y>x. \<exists>a\<in>A. y > a)" 585proof safe 586 fix y 587 assume "x \<ge> \<Sqinter>A" "y > x" 588 then have "y > \<Sqinter>A" by auto 589 then show "\<exists>a\<in>A. y > a" 590 unfolding Inf_less_iff . 591qed (auto elim!: allE[of _ "\<Sqinter>A"] simp add: not_le[symmetric] Inf_lower) 592 593lemma INF_le_iff: "\<Sqinter>(f ` A) \<le> x \<longleftrightarrow> (\<forall>y>x. \<exists>i\<in>A. y > f i)" 594 using Inf_le_iff [of "f ` A"] by simp 595 596lemma le_Sup_iff: "x \<le> \<Squnion>A \<longleftrightarrow> (\<forall>y<x. \<exists>a\<in>A. y < a)" 597proof safe 598 fix y 599 assume "x \<le> \<Squnion>A" "y < x" 600 then have "y < \<Squnion>A" by auto 601 then show "\<exists>a\<in>A. y < a" 602 unfolding less_Sup_iff . 603qed (auto elim!: allE[of _ "\<Squnion>A"] simp add: not_le[symmetric] Sup_upper) 604 605lemma le_SUP_iff: "x \<le> \<Squnion>(f ` A) \<longleftrightarrow> (\<forall>y<x. \<exists>i\<in>A. y < f i)" 606 using le_Sup_iff [of _ "f ` A"] by simp 607 608end 609 610subsection \<open>Complete lattice on \<^typ>\<open>bool\<close>\<close> 611 612instantiation bool :: complete_lattice 613begin 614 615definition [simp, code]: "\<Sqinter>A \<longleftrightarrow> False \<notin> A" 616 617definition [simp, code]: "\<Squnion>A \<longleftrightarrow> True \<in> A" 618 619instance 620 by standard (auto intro: bool_induct) 621 622end 623 624lemma not_False_in_image_Ball [simp]: "False \<notin> P ` A \<longleftrightarrow> Ball A P" 625 by auto 626 627lemma True_in_image_Bex [simp]: "True \<in> P ` A \<longleftrightarrow> Bex A P" 628 by auto 629 630lemma INF_bool_eq [simp]: "(\<lambda>A f. \<Sqinter>(f ` A)) = Ball" 631 by (simp add: fun_eq_iff) 632 633lemma SUP_bool_eq [simp]: "(\<lambda>A f. \<Squnion>(f ` A)) = Bex" 634 by (simp add: fun_eq_iff) 635 636instance bool :: complete_boolean_algebra 637 by (standard, fastforce) 638 639subsection \<open>Complete lattice on \<^typ>\<open>_ \<Rightarrow> _\<close>\<close> 640 641instantiation "fun" :: (type, Inf) Inf 642begin 643 644definition "\<Sqinter>A = (\<lambda>x. \<Sqinter>f\<in>A. f x)" 645 646lemma Inf_apply [simp, code]: "(\<Sqinter>A) x = (\<Sqinter>f\<in>A. f x)" 647 by (simp add: Inf_fun_def) 648 649instance .. 650 651end 652 653instantiation "fun" :: (type, Sup) Sup 654begin 655 656definition "\<Squnion>A = (\<lambda>x. \<Squnion>f\<in>A. f x)" 657 658lemma Sup_apply [simp, code]: "(\<Squnion>A) x = (\<Squnion>f\<in>A. f x)" 659 by (simp add: Sup_fun_def) 660 661instance .. 662 663end 664 665instantiation "fun" :: (type, complete_lattice) complete_lattice 666begin 667 668instance 669 by standard (auto simp add: le_fun_def intro: INF_lower INF_greatest SUP_upper SUP_least) 670 671end 672 673lemma INF_apply [simp]: "(\<Sqinter>y\<in>A. f y) x = (\<Sqinter>y\<in>A. f y x)" 674 by (simp add: image_comp) 675 676lemma SUP_apply [simp]: "(\<Squnion>y\<in>A. f y) x = (\<Squnion>y\<in>A. f y x)" 677 by (simp add: image_comp) 678 679subsection \<open>Complete lattice on unary and binary predicates\<close> 680 681lemma Inf1_I: "(\<And>P. P \<in> A \<Longrightarrow> P a) \<Longrightarrow> (\<Sqinter>A) a" 682 by auto 683 684lemma INF1_I: "(\<And>x. x \<in> A \<Longrightarrow> B x b) \<Longrightarrow> (\<Sqinter>x\<in>A. B x) b" 685 by simp 686 687lemma INF2_I: "(\<And>x. x \<in> A \<Longrightarrow> B x b c) \<Longrightarrow> (\<Sqinter>x\<in>A. B x) b c" 688 by simp 689 690lemma Inf2_I: "(\<And>r. r \<in> A \<Longrightarrow> r a b) \<Longrightarrow> (\<Sqinter>A) a b" 691 by auto 692 693lemma Inf1_D: "(\<Sqinter>A) a \<Longrightarrow> P \<in> A \<Longrightarrow> P a" 694 by auto 695 696lemma INF1_D: "(\<Sqinter>x\<in>A. B x) b \<Longrightarrow> a \<in> A \<Longrightarrow> B a b" 697 by simp 698 699lemma Inf2_D: "(\<Sqinter>A) a b \<Longrightarrow> r \<in> A \<Longrightarrow> r a b" 700 by auto 701 702lemma INF2_D: "(\<Sqinter>x\<in>A. B x) b c \<Longrightarrow> a \<in> A \<Longrightarrow> B a b c" 703 by simp 704 705lemma Inf1_E: 706 assumes "(\<Sqinter>A) a" 707 obtains "P a" | "P \<notin> A" 708 using assms by auto 709 710lemma INF1_E: 711 assumes "(\<Sqinter>x\<in>A. B x) b" 712 obtains "B a b" | "a \<notin> A" 713 using assms by auto 714 715lemma Inf2_E: 716 assumes "(\<Sqinter>A) a b" 717 obtains "r a b" | "r \<notin> A" 718 using assms by auto 719 720lemma INF2_E: 721 assumes "(\<Sqinter>x\<in>A. B x) b c" 722 obtains "B a b c" | "a \<notin> A" 723 using assms by auto 724 725lemma Sup1_I: "P \<in> A \<Longrightarrow> P a \<Longrightarrow> (\<Squnion>A) a" 726 by auto 727 728lemma SUP1_I: "a \<in> A \<Longrightarrow> B a b \<Longrightarrow> (\<Squnion>x\<in>A. B x) b" 729 by auto 730 731lemma Sup2_I: "r \<in> A \<Longrightarrow> r a b \<Longrightarrow> (\<Squnion>A) a b" 732 by auto 733 734lemma SUP2_I: "a \<in> A \<Longrightarrow> B a b c \<Longrightarrow> (\<Squnion>x\<in>A. B x) b c" 735 by auto 736 737lemma Sup1_E: 738 assumes "(\<Squnion>A) a" 739 obtains P where "P \<in> A" and "P a" 740 using assms by auto 741 742lemma SUP1_E: 743 assumes "(\<Squnion>x\<in>A. B x) b" 744 obtains x where "x \<in> A" and "B x b" 745 using assms by auto 746 747lemma Sup2_E: 748 assumes "(\<Squnion>A) a b" 749 obtains r where "r \<in> A" "r a b" 750 using assms by auto 751 752lemma SUP2_E: 753 assumes "(\<Squnion>x\<in>A. B x) b c" 754 obtains x where "x \<in> A" "B x b c" 755 using assms by auto 756 757 758subsection \<open>Complete lattice on \<^typ>\<open>_ set\<close>\<close> 759 760instantiation "set" :: (type) complete_lattice 761begin 762 763definition "\<Sqinter>A = {x. \<Sqinter>((\<lambda>B. x \<in> B) ` A)}" 764 765definition "\<Squnion>A = {x. \<Squnion>((\<lambda>B. x \<in> B) ` A)}" 766 767instance 768 by standard (auto simp add: less_eq_set_def Inf_set_def Sup_set_def le_fun_def) 769 770end 771 772subsubsection \<open>Inter\<close> 773 774abbreviation Inter :: "'a set set \<Rightarrow> 'a set" ("\<Inter>") 775 where "\<Inter>S \<equiv> \<Sqinter>S" 776 777lemma Inter_eq: "\<Inter>A = {x. \<forall>B \<in> A. x \<in> B}" 778proof (rule set_eqI) 779 fix x 780 have "(\<forall>Q\<in>{P. \<exists>B\<in>A. P \<longleftrightarrow> x \<in> B}. Q) \<longleftrightarrow> (\<forall>B\<in>A. x \<in> B)" 781 by auto 782 then show "x \<in> \<Inter>A \<longleftrightarrow> x \<in> {x. \<forall>B \<in> A. x \<in> B}" 783 by (simp add: Inf_set_def image_def) 784qed 785 786lemma Inter_iff [simp]: "A \<in> \<Inter>C \<longleftrightarrow> (\<forall>X\<in>C. A \<in> X)" 787 by (unfold Inter_eq) blast 788 789lemma InterI [intro!]: "(\<And>X. X \<in> C \<Longrightarrow> A \<in> X) \<Longrightarrow> A \<in> \<Inter>C" 790 by (simp add: Inter_eq) 791 792text \<open> 793 \<^medskip> A ``destruct'' rule -- every \<^term>\<open>X\<close> in \<^term>\<open>C\<close> 794 contains \<^term>\<open>A\<close> as an element, but \<^prop>\<open>A \<in> X\<close> can hold when 795 \<^prop>\<open>X \<in> C\<close> does not! This rule is analogous to \<open>spec\<close>. 796\<close> 797 798lemma InterD [elim, Pure.elim]: "A \<in> \<Inter>C \<Longrightarrow> X \<in> C \<Longrightarrow> A \<in> X" 799 by auto 800 801lemma InterE [elim]: "A \<in> \<Inter>C \<Longrightarrow> (X \<notin> C \<Longrightarrow> R) \<Longrightarrow> (A \<in> X \<Longrightarrow> R) \<Longrightarrow> R" 802 \<comment> \<open>``Classical'' elimination rule -- does not require proving 803 \<^prop>\<open>X \<in> C\<close>.\<close> 804 unfolding Inter_eq by blast 805 806lemma Inter_lower: "B \<in> A \<Longrightarrow> \<Inter>A \<subseteq> B" 807 by (fact Inf_lower) 808 809lemma Inter_subset: "(\<And>X. X \<in> A \<Longrightarrow> X \<subseteq> B) \<Longrightarrow> A \<noteq> {} \<Longrightarrow> \<Inter>A \<subseteq> B" 810 by (fact Inf_less_eq) 811 812lemma Inter_greatest: "(\<And>X. X \<in> A \<Longrightarrow> C \<subseteq> X) \<Longrightarrow> C \<subseteq> \<Inter>A" 813 by (fact Inf_greatest) 814 815lemma Inter_empty: "\<Inter>{} = UNIV" 816 by (fact Inf_empty) (* already simp *) 817 818lemma Inter_UNIV: "\<Inter>UNIV = {}" 819 by (fact Inf_UNIV) (* already simp *) 820 821lemma Inter_insert: "\<Inter>(insert a B) = a \<inter> \<Inter>B" 822 by (fact Inf_insert) (* already simp *) 823 824lemma Inter_Un_subset: "\<Inter>A \<union> \<Inter>B \<subseteq> \<Inter>(A \<inter> B)" 825 by (fact less_eq_Inf_inter) 826 827lemma Inter_Un_distrib: "\<Inter>(A \<union> B) = \<Inter>A \<inter> \<Inter>B" 828 by (fact Inf_union_distrib) 829 830lemma Inter_UNIV_conv [simp]: 831 "\<Inter>A = UNIV \<longleftrightarrow> (\<forall>x\<in>A. x = UNIV)" 832 "UNIV = \<Inter>A \<longleftrightarrow> (\<forall>x\<in>A. x = UNIV)" 833 by (fact Inf_top_conv)+ 834 835lemma Inter_anti_mono: "B \<subseteq> A \<Longrightarrow> \<Inter>A \<subseteq> \<Inter>B" 836 by (fact Inf_superset_mono) 837 838 839subsubsection \<open>Intersections of families\<close> 840 841syntax (ASCII) 842 "_INTER1" :: "pttrns \<Rightarrow> 'b set \<Rightarrow> 'b set" ("(3INT _./ _)" [0, 10] 10) 843 "_INTER" :: "pttrn \<Rightarrow> 'a set \<Rightarrow> 'b set \<Rightarrow> 'b set" ("(3INT _:_./ _)" [0, 0, 10] 10) 844 845syntax 846 "_INTER1" :: "pttrns \<Rightarrow> 'b set \<Rightarrow> 'b set" ("(3\<Inter>_./ _)" [0, 10] 10) 847 "_INTER" :: "pttrn \<Rightarrow> 'a set \<Rightarrow> 'b set \<Rightarrow> 'b set" ("(3\<Inter>_\<in>_./ _)" [0, 0, 10] 10) 848 849syntax (latex output) 850 "_INTER1" :: "pttrns \<Rightarrow> 'b set \<Rightarrow> 'b set" ("(3\<Inter>(\<open>unbreakable\<close>\<^bsub>_\<^esub>)/ _)" [0, 10] 10) 851 "_INTER" :: "pttrn \<Rightarrow> 'a set \<Rightarrow> 'b set \<Rightarrow> 'b set" ("(3\<Inter>(\<open>unbreakable\<close>\<^bsub>_\<in>_\<^esub>)/ _)" [0, 0, 10] 10) 852 853translations 854 "\<Inter>x y. f" \<rightleftharpoons> "\<Inter>x. \<Inter>y. f" 855 "\<Inter>x. f" \<rightleftharpoons> "\<Inter>(CONST range (\<lambda>x. f))" 856 "\<Inter>x\<in>A. f" \<rightleftharpoons> "CONST Inter ((\<lambda>x. f) ` A)" 857 858lemma INTER_eq: "(\<Inter>x\<in>A. B x) = {y. \<forall>x\<in>A. y \<in> B x}" 859 by (auto intro!: INF_eqI) 860 861lemma INT_iff [simp]: "b \<in> (\<Inter>x\<in>A. B x) \<longleftrightarrow> (\<forall>x\<in>A. b \<in> B x)" 862 using Inter_iff [of _ "B ` A"] by simp 863 864lemma INT_I [intro!]: "(\<And>x. x \<in> A \<Longrightarrow> b \<in> B x) \<Longrightarrow> b \<in> (\<Inter>x\<in>A. B x)" 865 by auto 866 867lemma INT_D [elim, Pure.elim]: "b \<in> (\<Inter>x\<in>A. B x) \<Longrightarrow> a \<in> A \<Longrightarrow> b \<in> B a" 868 by auto 869 870lemma INT_E [elim]: "b \<in> (\<Inter>x\<in>A. B x) \<Longrightarrow> (b \<in> B a \<Longrightarrow> R) \<Longrightarrow> (a \<notin> A \<Longrightarrow> R) \<Longrightarrow> R" 871 \<comment> \<open>"Classical" elimination -- by the Excluded Middle on \<^prop>\<open>a\<in>A\<close>.\<close> 872 by auto 873 874lemma Collect_ball_eq: "{x. \<forall>y\<in>A. P x y} = (\<Inter>y\<in>A. {x. P x y})" 875 by blast 876 877lemma Collect_all_eq: "{x. \<forall>y. P x y} = (\<Inter>y. {x. P x y})" 878 by blast 879 880lemma INT_lower: "a \<in> A \<Longrightarrow> (\<Inter>x\<in>A. B x) \<subseteq> B a" 881 by (fact INF_lower) 882 883lemma INT_greatest: "(\<And>x. x \<in> A \<Longrightarrow> C \<subseteq> B x) \<Longrightarrow> C \<subseteq> (\<Inter>x\<in>A. B x)" 884 by (fact INF_greatest) 885 886lemma INT_empty: "(\<Inter>x\<in>{}. B x) = UNIV" 887 by (fact INF_empty) 888 889lemma INT_absorb: "k \<in> I \<Longrightarrow> A k \<inter> (\<Inter>i\<in>I. A i) = (\<Inter>i\<in>I. A i)" 890 by (fact INF_absorb) 891 892lemma INT_subset_iff: "B \<subseteq> (\<Inter>i\<in>I. A i) \<longleftrightarrow> (\<forall>i\<in>I. B \<subseteq> A i)" 893 by (fact le_INF_iff) 894 895lemma INT_insert [simp]: "(\<Inter>x \<in> insert a A. B x) = B a \<inter> \<Inter> (B ` A)" 896 by (fact INF_insert) 897 898lemma INT_Un: "(\<Inter>i \<in> A \<union> B. M i) = (\<Inter>i \<in> A. M i) \<inter> (\<Inter>i\<in>B. M i)" 899 by (fact INF_union) 900 901lemma INT_insert_distrib: "u \<in> A \<Longrightarrow> (\<Inter>x\<in>A. insert a (B x)) = insert a (\<Inter>x\<in>A. B x)" 902 by blast 903 904lemma INT_constant [simp]: "(\<Inter>y\<in>A. c) = (if A = {} then UNIV else c)" 905 by (fact INF_constant) 906 907lemma INTER_UNIV_conv: 908 "(UNIV = (\<Inter>x\<in>A. B x)) = (\<forall>x\<in>A. B x = UNIV)" 909 "((\<Inter>x\<in>A. B x) = UNIV) = (\<forall>x\<in>A. B x = UNIV)" 910 by (fact INF_top_conv)+ (* already simp *) 911 912lemma INT_bool_eq: "(\<Inter>b. A b) = A True \<inter> A False" 913 by (fact INF_UNIV_bool_expand) 914 915lemma INT_anti_mono: "A \<subseteq> B \<Longrightarrow> (\<And>x. x \<in> A \<Longrightarrow> f x \<subseteq> g x) \<Longrightarrow> (\<Inter>x\<in>B. f x) \<subseteq> (\<Inter>x\<in>A. g x)" 916 \<comment> \<open>The last inclusion is POSITIVE!\<close> 917 by (fact INF_superset_mono) 918 919lemma Pow_INT_eq: "Pow (\<Inter>x\<in>A. B x) = (\<Inter>x\<in>A. Pow (B x))" 920 by blast 921 922lemma vimage_INT: "f -` (\<Inter>x\<in>A. B x) = (\<Inter>x\<in>A. f -` B x)" 923 by blast 924 925 926subsubsection \<open>Union\<close> 927 928abbreviation Union :: "'a set set \<Rightarrow> 'a set" ("\<Union>") 929 where "\<Union>S \<equiv> \<Squnion>S" 930 931lemma Union_eq: "\<Union>A = {x. \<exists>B \<in> A. x \<in> B}" 932proof (rule set_eqI) 933 fix x 934 have "(\<exists>Q\<in>{P. \<exists>B\<in>A. P \<longleftrightarrow> x \<in> B}. Q) \<longleftrightarrow> (\<exists>B\<in>A. x \<in> B)" 935 by auto 936 then show "x \<in> \<Union>A \<longleftrightarrow> x \<in> {x. \<exists>B\<in>A. x \<in> B}" 937 by (simp add: Sup_set_def image_def) 938qed 939 940lemma Union_iff [simp]: "A \<in> \<Union>C \<longleftrightarrow> (\<exists>X\<in>C. A\<in>X)" 941 by (unfold Union_eq) blast 942 943lemma UnionI [intro]: "X \<in> C \<Longrightarrow> A \<in> X \<Longrightarrow> A \<in> \<Union>C" 944 \<comment> \<open>The order of the premises presupposes that \<^term>\<open>C\<close> is rigid; 945 \<^term>\<open>A\<close> may be flexible.\<close> 946 by auto 947 948lemma UnionE [elim!]: "A \<in> \<Union>C \<Longrightarrow> (\<And>X. A \<in> X \<Longrightarrow> X \<in> C \<Longrightarrow> R) \<Longrightarrow> R" 949 by auto 950 951lemma Union_upper: "B \<in> A \<Longrightarrow> B \<subseteq> \<Union>A" 952 by (fact Sup_upper) 953 954lemma Union_least: "(\<And>X. X \<in> A \<Longrightarrow> X \<subseteq> C) \<Longrightarrow> \<Union>A \<subseteq> C" 955 by (fact Sup_least) 956 957lemma Union_empty: "\<Union>{} = {}" 958 by (fact Sup_empty) (* already simp *) 959 960lemma Union_UNIV: "\<Union>UNIV = UNIV" 961 by (fact Sup_UNIV) (* already simp *) 962 963lemma Union_insert: "\<Union>(insert a B) = a \<union> \<Union>B" 964 by (fact Sup_insert) (* already simp *) 965 966lemma Union_Un_distrib [simp]: "\<Union>(A \<union> B) = \<Union>A \<union> \<Union>B" 967 by (fact Sup_union_distrib) 968 969lemma Union_Int_subset: "\<Union>(A \<inter> B) \<subseteq> \<Union>A \<inter> \<Union>B" 970 by (fact Sup_inter_less_eq) 971 972lemma Union_empty_conv: "(\<Union>A = {}) \<longleftrightarrow> (\<forall>x\<in>A. x = {})" 973 by (fact Sup_bot_conv) (* already simp *) 974 975lemma empty_Union_conv: "({} = \<Union>A) \<longleftrightarrow> (\<forall>x\<in>A. x = {})" 976 by (fact Sup_bot_conv) (* already simp *) 977 978lemma subset_Pow_Union: "A \<subseteq> Pow (\<Union>A)" 979 by blast 980 981lemma Union_Pow_eq [simp]: "\<Union>(Pow A) = A" 982 by blast 983 984lemma Union_mono: "A \<subseteq> B \<Longrightarrow> \<Union>A \<subseteq> \<Union>B" 985 by (fact Sup_subset_mono) 986 987lemma Union_subsetI: "(\<And>x. x \<in> A \<Longrightarrow> \<exists>y. y \<in> B \<and> x \<subseteq> y) \<Longrightarrow> \<Union>A \<subseteq> \<Union>B" 988 by blast 989 990lemma disjnt_inj_on_iff: 991 "\<lbrakk>inj_on f (\<Union>\<A>); X \<in> \<A>; Y \<in> \<A>\<rbrakk> \<Longrightarrow> disjnt (f ` X) (f ` Y) \<longleftrightarrow> disjnt X Y" 992 apply (auto simp: disjnt_def) 993 using inj_on_eq_iff by fastforce 994 995lemma disjnt_Union1 [simp]: "disjnt (\<Union>\<A>) B \<longleftrightarrow> (\<forall>A \<in> \<A>. disjnt A B)" 996 by (auto simp: disjnt_def) 997 998lemma disjnt_Union2 [simp]: "disjnt B (\<Union>\<A>) \<longleftrightarrow> (\<forall>A \<in> \<A>. disjnt B A)" 999 by (auto simp: disjnt_def) 1000 1001 1002subsubsection \<open>Unions of families\<close> 1003 1004syntax (ASCII) 1005 "_UNION1" :: "pttrns => 'b set => 'b set" ("(3UN _./ _)" [0, 10] 10) 1006 "_UNION" :: "pttrn => 'a set => 'b set => 'b set" ("(3UN _:_./ _)" [0, 0, 10] 10) 1007 1008syntax 1009 "_UNION1" :: "pttrns => 'b set => 'b set" ("(3\<Union>_./ _)" [0, 10] 10) 1010 "_UNION" :: "pttrn => 'a set => 'b set => 'b set" ("(3\<Union>_\<in>_./ _)" [0, 0, 10] 10) 1011 1012syntax (latex output) 1013 "_UNION1" :: "pttrns => 'b set => 'b set" ("(3\<Union>(\<open>unbreakable\<close>\<^bsub>_\<^esub>)/ _)" [0, 10] 10) 1014 "_UNION" :: "pttrn => 'a set => 'b set => 'b set" ("(3\<Union>(\<open>unbreakable\<close>\<^bsub>_\<in>_\<^esub>)/ _)" [0, 0, 10] 10) 1015 1016translations 1017 "\<Union>x y. f" \<rightleftharpoons> "\<Union>x. \<Union>y. f" 1018 "\<Union>x. f" \<rightleftharpoons> "\<Union>(CONST range (\<lambda>x. f))" 1019 "\<Union>x\<in>A. f" \<rightleftharpoons> "CONST Union ((\<lambda>x. f) ` A)" 1020 1021text \<open> 1022 Note the difference between ordinary syntax of indexed 1023 unions and intersections (e.g.\ \<open>\<Union>a\<^sub>1\<in>A\<^sub>1. B\<close>) 1024 and their \LaTeX\ rendition: \<^term>\<open>\<Union>a\<^sub>1\<in>A\<^sub>1. B\<close>. 1025\<close> 1026 1027lemma disjoint_UN_iff: "disjnt A (\<Union>i\<in>I. B i) \<longleftrightarrow> (\<forall>i\<in>I. disjnt A (B i))" 1028 by (auto simp: disjnt_def) 1029 1030lemma UNION_eq: "(\<Union>x\<in>A. B x) = {y. \<exists>x\<in>A. y \<in> B x}" 1031 by (auto intro!: SUP_eqI) 1032 1033lemma bind_UNION [code]: "Set.bind A f = \<Union>(f ` A)" 1034 by (simp add: bind_def UNION_eq) 1035 1036lemma member_bind [simp]: "x \<in> Set.bind A f \<longleftrightarrow> x \<in> \<Union>(f ` A)" 1037 by (simp add: bind_UNION) 1038 1039lemma Union_SetCompr_eq: "\<Union>{f x| x. P x} = {a. \<exists>x. P x \<and> a \<in> f x}" 1040 by blast 1041 1042lemma UN_iff [simp]: "b \<in> (\<Union>x\<in>A. B x) \<longleftrightarrow> (\<exists>x\<in>A. b \<in> B x)" 1043 using Union_iff [of _ "B ` A"] by simp 1044 1045lemma UN_I [intro]: "a \<in> A \<Longrightarrow> b \<in> B a \<Longrightarrow> b \<in> (\<Union>x\<in>A. B x)" 1046 \<comment> \<open>The order of the premises presupposes that \<^term>\<open>A\<close> is rigid; 1047 \<^term>\<open>b\<close> may be flexible.\<close> 1048 by auto 1049 1050lemma UN_E [elim!]: "b \<in> (\<Union>x\<in>A. B x) \<Longrightarrow> (\<And>x. x\<in>A \<Longrightarrow> b \<in> B x \<Longrightarrow> R) \<Longrightarrow> R" 1051 by auto 1052 1053lemma UN_upper: "a \<in> A \<Longrightarrow> B a \<subseteq> (\<Union>x\<in>A. B x)" 1054 by (fact SUP_upper) 1055 1056lemma UN_least: "(\<And>x. x \<in> A \<Longrightarrow> B x \<subseteq> C) \<Longrightarrow> (\<Union>x\<in>A. B x) \<subseteq> C" 1057 by (fact SUP_least) 1058 1059lemma Collect_bex_eq: "{x. \<exists>y\<in>A. P x y} = (\<Union>y\<in>A. {x. P x y})" 1060 by blast 1061 1062lemma UN_insert_distrib: "u \<in> A \<Longrightarrow> (\<Union>x\<in>A. insert a (B x)) = insert a (\<Union>x\<in>A. B x)" 1063 by blast 1064 1065lemma UN_empty: "(\<Union>x\<in>{}. B x) = {}" 1066 by (fact SUP_empty) 1067 1068lemma UN_empty2: "(\<Union>x\<in>A. {}) = {}" 1069 by (fact SUP_bot) (* already simp *) 1070 1071lemma UN_absorb: "k \<in> I \<Longrightarrow> A k \<union> (\<Union>i\<in>I. A i) = (\<Union>i\<in>I. A i)" 1072 by (fact SUP_absorb) 1073 1074lemma UN_insert [simp]: "(\<Union>x\<in>insert a A. B x) = B a \<union> \<Union>(B ` A)" 1075 by (fact SUP_insert) 1076 1077lemma UN_Un [simp]: "(\<Union>i \<in> A \<union> B. M i) = (\<Union>i\<in>A. M i) \<union> (\<Union>i\<in>B. M i)" 1078 by (fact SUP_union) 1079 1080lemma 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)" 1081 by blast 1082 1083lemma UN_subset_iff: "((\<Union>i\<in>I. A i) \<subseteq> B) = (\<forall>i\<in>I. A i \<subseteq> B)" 1084 by (fact SUP_le_iff) 1085 1086lemma UN_constant [simp]: "(\<Union>y\<in>A. c) = (if A = {} then {} else c)" 1087 by (fact SUP_constant) 1088 1089lemma UNION_singleton_eq_range: "(\<Union>x\<in>A. {f x}) = f ` A" 1090 by blast 1091 1092lemma image_Union: "f ` \<Union>S = (\<Union>x\<in>S. f ` x)" 1093 by blast 1094 1095lemma UNION_empty_conv: 1096 "{} = (\<Union>x\<in>A. B x) \<longleftrightarrow> (\<forall>x\<in>A. B x = {})" 1097 "(\<Union>x\<in>A. B x) = {} \<longleftrightarrow> (\<forall>x\<in>A. B x = {})" 1098 by (fact SUP_bot_conv)+ (* already simp *) 1099 1100lemma Collect_ex_eq: "{x. \<exists>y. P x y} = (\<Union>y. {x. P x y})" 1101 by blast 1102 1103lemma ball_UN: "(\<forall>z \<in> \<Union>(B ` A). P z) \<longleftrightarrow> (\<forall>x\<in>A. \<forall>z \<in> B x. P z)" 1104 by blast 1105 1106lemma bex_UN: "(\<exists>z \<in> \<Union>(B ` A). P z) \<longleftrightarrow> (\<exists>x\<in>A. \<exists>z\<in>B x. P z)" 1107 by blast 1108 1109lemma Un_eq_UN: "A \<union> B = (\<Union>b. if b then A else B)" 1110 by safe (auto simp add: if_split_mem2) 1111 1112lemma UN_bool_eq: "(\<Union>b. A b) = (A True \<union> A False)" 1113 by (fact SUP_UNIV_bool_expand) 1114 1115lemma UN_Pow_subset: "(\<Union>x\<in>A. Pow (B x)) \<subseteq> Pow (\<Union>x\<in>A. B x)" 1116 by blast 1117 1118lemma UN_mono: 1119 "A \<subseteq> B \<Longrightarrow> (\<And>x. x \<in> A \<Longrightarrow> f x \<subseteq> g x) \<Longrightarrow> 1120 (\<Union>x\<in>A. f x) \<subseteq> (\<Union>x\<in>B. g x)" 1121 by (fact SUP_subset_mono) 1122 1123lemma vimage_Union: "f -` (\<Union>A) = (\<Union>X\<in>A. f -` X)" 1124 by blast 1125 1126lemma vimage_UN: "f -` (\<Union>x\<in>A. B x) = (\<Union>x\<in>A. f -` B x)" 1127 by blast 1128 1129lemma vimage_eq_UN: "f -` B = (\<Union>y\<in>B. f -` {y})" 1130 \<comment> \<open>NOT suitable for rewriting\<close> 1131 by blast 1132 1133lemma image_UN: "f ` \<Union>(B ` A) = (\<Union>x\<in>A. f ` B x)" 1134 by blast 1135 1136lemma UN_singleton [simp]: "(\<Union>x\<in>A. {x}) = A" 1137 by blast 1138 1139lemma inj_on_image: "inj_on f (\<Union>A) \<Longrightarrow> inj_on ((`) f) A" 1140 unfolding inj_on_def by blast 1141 1142 1143subsubsection \<open>Distributive laws\<close> 1144 1145lemma Int_Union: "A \<inter> \<Union>B = (\<Union>C\<in>B. A \<inter> C)" 1146 by blast 1147 1148lemma Un_Inter: "A \<union> \<Inter>B = (\<Inter>C\<in>B. A \<union> C)" 1149 by blast 1150 1151lemma Int_Union2: "\<Union>B \<inter> A = (\<Union>C\<in>B. C \<inter> A)" 1152 by blast 1153 1154lemma INT_Int_distrib: "(\<Inter>i\<in>I. A i \<inter> B i) = (\<Inter>i\<in>I. A i) \<inter> (\<Inter>i\<in>I. B i)" 1155 by (rule sym) (rule INF_inf_distrib) 1156 1157lemma UN_Un_distrib: "(\<Union>i\<in>I. A i \<union> B i) = (\<Union>i\<in>I. A i) \<union> (\<Union>i\<in>I. B i)" 1158 by (rule sym) (rule SUP_sup_distrib) 1159 1160lemma Int_Inter_image: "(\<Inter>x\<in>C. A x \<inter> B x) = \<Inter>(A ` C) \<inter> \<Inter>(B ` C)" (* FIXME drop *) 1161 by (simp add: INT_Int_distrib) 1162 1163lemma Int_Inter_eq: "A \<inter> \<Inter>\<B> = (if \<B>={} then A else (\<Inter>B\<in>\<B>. A \<inter> B))" 1164 "\<Inter>\<B> \<inter> A = (if \<B>={} then A else (\<Inter>B\<in>\<B>. B \<inter> A))" 1165 by auto 1166 1167lemma Un_Union_image: "(\<Union>x\<in>C. A x \<union> B x) = \<Union>(A ` C) \<union> \<Union>(B ` C)" (* FIXME drop *) 1168 \<comment> \<open>Devlin, Fundamentals of Contemporary Set Theory, page 12, exercise 5:\<close> 1169 \<comment> \<open>Union of a family of unions\<close> 1170 by (simp add: UN_Un_distrib) 1171 1172lemma Un_INT_distrib: "B \<union> (\<Inter>i\<in>I. A i) = (\<Inter>i\<in>I. B \<union> A i)" 1173 by blast 1174 1175lemma Int_UN_distrib: "B \<inter> (\<Union>i\<in>I. A i) = (\<Union>i\<in>I. B \<inter> A i)" 1176 \<comment> \<open>Halmos, Naive Set Theory, page 35.\<close> 1177 by blast 1178 1179lemma Int_UN_distrib2: "(\<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)" 1180 by blast 1181 1182lemma Un_INT_distrib2: "(\<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)" 1183 by blast 1184 1185lemma Union_disjoint: "(\<Union>C \<inter> A = {}) \<longleftrightarrow> (\<forall>B\<in>C. B \<inter> A = {})" 1186 by blast 1187 1188lemma SUP_UNION: "(\<Squnion>x\<in>(\<Union>y\<in>A. g y). f x) = (\<Squnion>y\<in>A. \<Squnion>x\<in>g y. f x :: _ :: complete_lattice)" 1189 by (rule order_antisym) (blast intro: SUP_least SUP_upper2)+ 1190 1191 1192subsection \<open>Injections and bijections\<close> 1193 1194lemma inj_on_Inter: "S \<noteq> {} \<Longrightarrow> (\<And>A. A \<in> S \<Longrightarrow> inj_on f A) \<Longrightarrow> inj_on f (\<Inter>S)" 1195 unfolding inj_on_def by blast 1196 1197lemma inj_on_INTER: "I \<noteq> {} \<Longrightarrow> (\<And>i. i \<in> I \<Longrightarrow> inj_on f (A i)) \<Longrightarrow> inj_on f (\<Inter>i \<in> I. A i)" 1198 unfolding inj_on_def by safe simp 1199 1200lemma inj_on_UNION_chain: 1201 assumes chain: "\<And>i j. i \<in> I \<Longrightarrow> j \<in> I \<Longrightarrow> A i \<le> A j \<or> A j \<le> A i" 1202 and inj: "\<And>i. i \<in> I \<Longrightarrow> inj_on f (A i)" 1203 shows "inj_on f (\<Union>i \<in> I. A i)" 1204proof - 1205 have "x = y" 1206 if *: "i \<in> I" "j \<in> I" 1207 and **: "x \<in> A i" "y \<in> A j" 1208 and ***: "f x = f y" 1209 for i j x y 1210 using chain [OF *] 1211 proof 1212 assume "A i \<le> A j" 1213 with ** have "x \<in> A j" by auto 1214 with inj * ** *** show ?thesis 1215 by (auto simp add: inj_on_def) 1216 next 1217 assume "A j \<le> A i" 1218 with ** have "y \<in> A i" by auto 1219 with inj * ** *** show ?thesis 1220 by (auto simp add: inj_on_def) 1221 qed 1222 then show ?thesis 1223 by (unfold inj_on_def UNION_eq) auto 1224qed 1225 1226lemma bij_betw_UNION_chain: 1227 assumes chain: "\<And>i j. i \<in> I \<Longrightarrow> j \<in> I \<Longrightarrow> A i \<le> A j \<or> A j \<le> A i" 1228 and bij: "\<And>i. i \<in> I \<Longrightarrow> bij_betw f (A i) (A' i)" 1229 shows "bij_betw f (\<Union>i \<in> I. A i) (\<Union>i \<in> I. A' i)" 1230 unfolding bij_betw_def 1231proof safe 1232 have "\<And>i. i \<in> I \<Longrightarrow> inj_on f (A i)" 1233 using bij bij_betw_def[of f] by auto 1234 then show "inj_on f (\<Union>(A ` I))" 1235 using chain inj_on_UNION_chain[of I A f] by auto 1236next 1237 fix i x 1238 assume *: "i \<in> I" "x \<in> A i" 1239 with bij have "f x \<in> A' i" 1240 by (auto simp: bij_betw_def) 1241 with * show "f x \<in> \<Union>(A' ` I)" by blast 1242next 1243 fix i x' 1244 assume *: "i \<in> I" "x' \<in> A' i" 1245 with bij have "\<exists>x \<in> A i. x' = f x" 1246 unfolding bij_betw_def by blast 1247 with * have "\<exists>j \<in> I. \<exists>x \<in> A j. x' = f x" 1248 by blast 1249 then show "x' \<in> f ` \<Union>(A ` I)" 1250 by blast 1251qed 1252 1253(*injectivity's required. Left-to-right inclusion holds even if A is empty*) 1254lemma image_INT: "inj_on f C \<Longrightarrow> \<forall>x\<in>A. B x \<subseteq> C \<Longrightarrow> j \<in> A \<Longrightarrow> f ` (\<Inter>(B ` A)) = (\<Inter>x\<in>A. f ` B x)" 1255 by (auto simp add: inj_on_def) blast 1256 1257lemma bij_image_INT: "bij f \<Longrightarrow> f ` (\<Inter>(B ` A)) = (\<Inter>x\<in>A. f ` B x)" 1258 by (auto simp: bij_def inj_def surj_def) blast 1259 1260lemma UNION_fun_upd: "\<Union>(A(i := B) ` J) = \<Union>(A ` (J - {i})) \<union> (if i \<in> J then B else {})" 1261 by (auto simp add: set_eq_iff) 1262 1263lemma bij_betw_Pow: 1264 assumes "bij_betw f A B" 1265 shows "bij_betw (image f) (Pow A) (Pow B)" 1266proof - 1267 from assms have "inj_on f A" 1268 by (rule bij_betw_imp_inj_on) 1269 then have "inj_on f (\<Union>(Pow A))" 1270 by simp 1271 then have "inj_on (image f) (Pow A)" 1272 by (rule inj_on_image) 1273 then have "bij_betw (image f) (Pow A) (image f ` Pow A)" 1274 by (rule inj_on_imp_bij_betw) 1275 moreover from assms have "f ` A = B" 1276 by (rule bij_betw_imp_surj_on) 1277 then have "image f ` Pow A = Pow B" 1278 by (rule image_Pow_surj) 1279 ultimately show ?thesis by simp 1280qed 1281 1282 1283subsubsection \<open>Complement\<close> 1284 1285lemma Compl_INT [simp]: "- (\<Inter>x\<in>A. B x) = (\<Union>x\<in>A. -B x)" 1286 by blast 1287 1288lemma Compl_UN [simp]: "- (\<Union>x\<in>A. B x) = (\<Inter>x\<in>A. -B x)" 1289 by blast 1290 1291subsubsection \<open>Miniscoping and maxiscoping\<close> 1292 1293text \<open>\<^medskip> Miniscoping: pushing in quantifiers and big Unions and Intersections.\<close> 1294 1295lemma UN_simps [simp]: 1296 "\<And>a B C. (\<Union>x\<in>C. insert a (B x)) = (if C={} then {} else insert a (\<Union>x\<in>C. B x))" 1297 "\<And>A B C. (\<Union>x\<in>C. A x \<union> B) = ((if C={} then {} else (\<Union>x\<in>C. A x) \<union> B))" 1298 "\<And>A B C. (\<Union>x\<in>C. A \<union> B x) = ((if C={} then {} else A \<union> (\<Union>x\<in>C. B x)))" 1299 "\<And>A B C. (\<Union>x\<in>C. A x \<inter> B) = ((\<Union>x\<in>C. A x) \<inter> B)" 1300 "\<And>A B C. (\<Union>x\<in>C. A \<inter> B x) = (A \<inter>(\<Union>x\<in>C. B x))" 1301 "\<And>A B C. (\<Union>x\<in>C. A x - B) = ((\<Union>x\<in>C. A x) - B)" 1302 "\<And>A B C. (\<Union>x\<in>C. A - B x) = (A - (\<Inter>x\<in>C. B x))" 1303 "\<And>A B. (\<Union>x\<in>\<Union>A. B x) = (\<Union>y\<in>A. \<Union>x\<in>y. B x)" 1304 "\<And>A B C. (\<Union>z\<in>(\<Union>(B ` A)). C z) = (\<Union>x\<in>A. \<Union>z\<in>B x. C z)" 1305 "\<And>A B f. (\<Union>x\<in>f`A. B x) = (\<Union>a\<in>A. B (f a))" 1306 by auto 1307 1308lemma INT_simps [simp]: 1309 "\<And>A B C. (\<Inter>x\<in>C. A x \<inter> B) = (if C={} then UNIV else (\<Inter>x\<in>C. A x) \<inter> B)" 1310 "\<And>A B C. (\<Inter>x\<in>C. A \<inter> B x) = (if C={} then UNIV else A \<inter>(\<Inter>x\<in>C. B x))" 1311 "\<And>A B C. (\<Inter>x\<in>C. A x - B) = (if C={} then UNIV else (\<Inter>x\<in>C. A x) - B)" 1312 "\<And>A B C. (\<Inter>x\<in>C. A - B x) = (if C={} then UNIV else A - (\<Union>x\<in>C. B x))" 1313 "\<And>a B C. (\<Inter>x\<in>C. insert a (B x)) = insert a (\<Inter>x\<in>C. B x)" 1314 "\<And>A B C. (\<Inter>x\<in>C. A x \<union> B) = ((\<Inter>x\<in>C. A x) \<union> B)" 1315 "\<And>A B C. (\<Inter>x\<in>C. A \<union> B x) = (A \<union> (\<Inter>x\<in>C. B x))" 1316 "\<And>A B. (\<Inter>x\<in>\<Union>A. B x) = (\<Inter>y\<in>A. \<Inter>x\<in>y. B x)" 1317 "\<And>A B C. (\<Inter>z\<in>(\<Union>(B ` A)). C z) = (\<Inter>x\<in>A. \<Inter>z\<in>B x. C z)" 1318 "\<And>A B f. (\<Inter>x\<in>f`A. B x) = (\<Inter>a\<in>A. B (f a))" 1319 by auto 1320 1321lemma UN_ball_bex_simps [simp]: 1322 "\<And>A P. (\<forall>x\<in>\<Union>A. P x) \<longleftrightarrow> (\<forall>y\<in>A. \<forall>x\<in>y. P x)" 1323 "\<And>A B P. (\<forall>x\<in>(\<Union>(B ` A)). P x) = (\<forall>a\<in>A. \<forall>x\<in> B a. P x)" 1324 "\<And>A P. (\<exists>x\<in>\<Union>A. P x) \<longleftrightarrow> (\<exists>y\<in>A. \<exists>x\<in>y. P x)" 1325 "\<And>A B P. (\<exists>x\<in>(\<Union>(B ` A)). P x) \<longleftrightarrow> (\<exists>a\<in>A. \<exists>x\<in>B a. P x)" 1326 by auto 1327 1328 1329text \<open>\<^medskip> Maxiscoping: pulling out big Unions and Intersections.\<close> 1330 1331lemma UN_extend_simps: 1332 "\<And>a B C. insert a (\<Union>x\<in>C. B x) = (if C={} then {a} else (\<Union>x\<in>C. insert a (B x)))" 1333 "\<And>A B C. (\<Union>x\<in>C. A x) \<union> B = (if C={} then B else (\<Union>x\<in>C. A x \<union> B))" 1334 "\<And>A B C. A \<union> (\<Union>x\<in>C. B x) = (if C={} then A else (\<Union>x\<in>C. A \<union> B x))" 1335 "\<And>A B C. ((\<Union>x\<in>C. A x) \<inter> B) = (\<Union>x\<in>C. A x \<inter> B)" 1336 "\<And>A B C. (A \<inter> (\<Union>x\<in>C. B x)) = (\<Union>x\<in>C. A \<inter> B x)" 1337 "\<And>A B C. ((\<Union>x\<in>C. A x) - B) = (\<Union>x\<in>C. A x - B)" 1338 "\<And>A B C. (A - (\<Inter>x\<in>C. B x)) = (\<Union>x\<in>C. A - B x)" 1339 "\<And>A B. (\<Union>y\<in>A. \<Union>x\<in>y. B x) = (\<Union>x\<in>\<Union>A. B x)" 1340 "\<And>A B C. (\<Union>x\<in>A. \<Union>z\<in>B x. C z) = (\<Union>z\<in>(\<Union>(B ` A)). C z)" 1341 "\<And>A B f. (\<Union>a\<in>A. B (f a)) = (\<Union>x\<in>f`A. B x)" 1342 by auto 1343 1344lemma INT_extend_simps: 1345 "\<And>A B C. (\<Inter>x\<in>C. A x) \<inter> B = (if C={} then B else (\<Inter>x\<in>C. A x \<inter> B))" 1346 "\<And>A B C. A \<inter> (\<Inter>x\<in>C. B x) = (if C={} then A else (\<Inter>x\<in>C. A \<inter> B x))" 1347 "\<And>A B C. (\<Inter>x\<in>C. A x) - B = (if C={} then UNIV - B else (\<Inter>x\<in>C. A x - B))" 1348 "\<And>A B C. A - (\<Union>x\<in>C. B x) = (if C={} then A else (\<Inter>x\<in>C. A - B x))" 1349 "\<And>a B C. insert a (\<Inter>x\<in>C. B x) = (\<Inter>x\<in>C. insert a (B x))" 1350 "\<And>A B C. ((\<Inter>x\<in>C. A x) \<union> B) = (\<Inter>x\<in>C. A x \<union> B)" 1351 "\<And>A B C. A \<union> (\<Inter>x\<in>C. B x) = (\<Inter>x\<in>C. A \<union> B x)" 1352 "\<And>A B. (\<Inter>y\<in>A. \<Inter>x\<in>y. B x) = (\<Inter>x\<in>\<Union>A. B x)" 1353 "\<And>A B C. (\<Inter>x\<in>A. \<Inter>z\<in>B x. C z) = (\<Inter>z\<in>(\<Union>(B ` A)). C z)" 1354 "\<And>A B f. (\<Inter>a\<in>A. B (f a)) = (\<Inter>x\<in>f`A. B x)" 1355 by auto 1356 1357text \<open>Finally\<close> 1358 1359lemmas mem_simps = 1360 insert_iff empty_iff Un_iff Int_iff Compl_iff Diff_iff 1361 mem_Collect_eq UN_iff Union_iff INT_iff Inter_iff 1362 \<comment> \<open>Each of these has ALREADY been added \<open>[simp]\<close> above.\<close> 1363 1364end 1365