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