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