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