src/HOL/Conditionally_Complete_Lattices.thy
 author wenzelm Fri Jul 22 11:00:43 2016 +0200 (2016-07-22) changeset 63540 f8652d0534fa parent 63331 247eac9758dd child 65466 b0f89998c2a1 permissions -rw-r--r--
tuned proofs -- avoid unstructured calculation;
 wenzelm@52265 ` 1` ```(* Title: HOL/Conditionally_Complete_Lattices.thy ``` hoelzl@51518 ` 2` ``` Author: Amine Chaieb and L C Paulson, University of Cambridge ``` hoelzl@51643 ` 3` ``` Author: Johannes Hölzl, TU München ``` hoelzl@54258 ` 4` ``` Author: Luke S. Serafin, Carnegie Mellon University ``` hoelzl@51518 ` 5` ```*) ``` paulson@33269 ` 6` wenzelm@60758 ` 7` ```section \Conditionally-complete Lattices\ ``` paulson@33269 ` 8` hoelzl@51773 ` 9` ```theory Conditionally_Complete_Lattices ``` hoelzl@63331 ` 10` ```imports Finite_Set Lattices_Big Set_Interval ``` paulson@33269 ` 11` ```begin ``` paulson@33269 ` 12` hoelzl@54259 ` 13` ```lemma (in linorder) Sup_fin_eq_Max: "finite X \ X \ {} \ Sup_fin X = Max X" ``` hoelzl@51475 ` 14` ``` by (induct X rule: finite_ne_induct) (simp_all add: sup_max) ``` hoelzl@51475 ` 15` hoelzl@54259 ` 16` ```lemma (in linorder) Inf_fin_eq_Min: "finite X \ X \ {} \ Inf_fin X = Min X" ``` hoelzl@51475 ` 17` ``` by (induct X rule: finite_ne_induct) (simp_all add: inf_min) ``` hoelzl@51475 ` 18` hoelzl@54258 ` 19` ```context preorder ``` hoelzl@54258 ` 20` ```begin ``` hoelzl@54258 ` 21` hoelzl@54258 ` 22` ```definition "bdd_above A \ (\M. \x \ A. x \ M)" ``` hoelzl@54258 ` 23` ```definition "bdd_below A \ (\m. \x \ A. m \ x)" ``` hoelzl@54258 ` 24` hoelzl@54258 ` 25` ```lemma bdd_aboveI[intro]: "(\x. x \ A \ x \ M) \ bdd_above A" ``` hoelzl@54258 ` 26` ``` by (auto simp: bdd_above_def) ``` hoelzl@54258 ` 27` hoelzl@54258 ` 28` ```lemma bdd_belowI[intro]: "(\x. x \ A \ m \ x) \ bdd_below A" ``` hoelzl@54258 ` 29` ``` by (auto simp: bdd_below_def) ``` hoelzl@54258 ` 30` hoelzl@54263 ` 31` ```lemma bdd_aboveI2: "(\x. x \ A \ f x \ M) \ bdd_above (f`A)" ``` hoelzl@54263 ` 32` ``` by force ``` hoelzl@54263 ` 33` hoelzl@54263 ` 34` ```lemma bdd_belowI2: "(\x. x \ A \ m \ f x) \ bdd_below (f`A)" ``` hoelzl@54263 ` 35` ``` by force ``` hoelzl@54263 ` 36` hoelzl@54258 ` 37` ```lemma bdd_above_empty [simp, intro]: "bdd_above {}" ``` hoelzl@54258 ` 38` ``` unfolding bdd_above_def by auto ``` hoelzl@54258 ` 39` hoelzl@54258 ` 40` ```lemma bdd_below_empty [simp, intro]: "bdd_below {}" ``` hoelzl@54258 ` 41` ``` unfolding bdd_below_def by auto ``` hoelzl@54258 ` 42` hoelzl@54258 ` 43` ```lemma bdd_above_mono: "bdd_above B \ A \ B \ bdd_above A" ``` hoelzl@54258 ` 44` ``` by (metis (full_types) bdd_above_def order_class.le_neq_trans psubsetD) ``` hoelzl@54258 ` 45` hoelzl@54258 ` 46` ```lemma bdd_below_mono: "bdd_below B \ A \ B \ bdd_below A" ``` hoelzl@54258 ` 47` ``` by (metis bdd_below_def order_class.le_neq_trans psubsetD) ``` hoelzl@54258 ` 48` hoelzl@54258 ` 49` ```lemma bdd_above_Int1 [simp]: "bdd_above A \ bdd_above (A \ B)" ``` hoelzl@54258 ` 50` ``` using bdd_above_mono by auto ``` hoelzl@54258 ` 51` hoelzl@54258 ` 52` ```lemma bdd_above_Int2 [simp]: "bdd_above B \ bdd_above (A \ B)" ``` hoelzl@54258 ` 53` ``` using bdd_above_mono by auto ``` hoelzl@54258 ` 54` hoelzl@54258 ` 55` ```lemma bdd_below_Int1 [simp]: "bdd_below A \ bdd_below (A \ B)" ``` hoelzl@54258 ` 56` ``` using bdd_below_mono by auto ``` hoelzl@54258 ` 57` hoelzl@54258 ` 58` ```lemma bdd_below_Int2 [simp]: "bdd_below B \ bdd_below (A \ B)" ``` hoelzl@54258 ` 59` ``` using bdd_below_mono by auto ``` hoelzl@54258 ` 60` hoelzl@54258 ` 61` ```lemma bdd_above_Ioo [simp, intro]: "bdd_above {a <..< b}" ``` hoelzl@54258 ` 62` ``` by (auto simp add: bdd_above_def intro!: exI[of _ b] less_imp_le) ``` hoelzl@54258 ` 63` hoelzl@54258 ` 64` ```lemma bdd_above_Ico [simp, intro]: "bdd_above {a ..< b}" ``` hoelzl@54258 ` 65` ``` by (auto simp add: bdd_above_def intro!: exI[of _ b] less_imp_le) ``` hoelzl@54258 ` 66` hoelzl@54258 ` 67` ```lemma bdd_above_Iio [simp, intro]: "bdd_above {..< b}" ``` hoelzl@54258 ` 68` ``` by (auto simp add: bdd_above_def intro: exI[of _ b] less_imp_le) ``` hoelzl@54258 ` 69` hoelzl@54258 ` 70` ```lemma bdd_above_Ioc [simp, intro]: "bdd_above {a <.. b}" ``` hoelzl@54258 ` 71` ``` by (auto simp add: bdd_above_def intro: exI[of _ b] less_imp_le) ``` hoelzl@54258 ` 72` hoelzl@54258 ` 73` ```lemma bdd_above_Icc [simp, intro]: "bdd_above {a .. b}" ``` hoelzl@54258 ` 74` ``` by (auto simp add: bdd_above_def intro: exI[of _ b] less_imp_le) ``` hoelzl@54258 ` 75` hoelzl@54258 ` 76` ```lemma bdd_above_Iic [simp, intro]: "bdd_above {.. b}" ``` hoelzl@54258 ` 77` ``` by (auto simp add: bdd_above_def intro: exI[of _ b] less_imp_le) ``` hoelzl@54258 ` 78` hoelzl@54258 ` 79` ```lemma bdd_below_Ioo [simp, intro]: "bdd_below {a <..< b}" ``` hoelzl@54258 ` 80` ``` by (auto simp add: bdd_below_def intro!: exI[of _ a] less_imp_le) ``` hoelzl@54258 ` 81` hoelzl@54258 ` 82` ```lemma bdd_below_Ioc [simp, intro]: "bdd_below {a <.. b}" ``` hoelzl@54258 ` 83` ``` by (auto simp add: bdd_below_def intro!: exI[of _ a] less_imp_le) ``` hoelzl@54258 ` 84` hoelzl@54258 ` 85` ```lemma bdd_below_Ioi [simp, intro]: "bdd_below {a <..}" ``` hoelzl@54258 ` 86` ``` by (auto simp add: bdd_below_def intro: exI[of _ a] less_imp_le) ``` hoelzl@54258 ` 87` hoelzl@54258 ` 88` ```lemma bdd_below_Ico [simp, intro]: "bdd_below {a ..< b}" ``` hoelzl@54258 ` 89` ``` by (auto simp add: bdd_below_def intro: exI[of _ a] less_imp_le) ``` hoelzl@54258 ` 90` hoelzl@54258 ` 91` ```lemma bdd_below_Icc [simp, intro]: "bdd_below {a .. b}" ``` hoelzl@54258 ` 92` ``` by (auto simp add: bdd_below_def intro: exI[of _ a] less_imp_le) ``` hoelzl@54258 ` 93` hoelzl@54258 ` 94` ```lemma bdd_below_Ici [simp, intro]: "bdd_below {a ..}" ``` hoelzl@54258 ` 95` ``` by (auto simp add: bdd_below_def intro: exI[of _ a] less_imp_le) ``` hoelzl@54258 ` 96` hoelzl@54258 ` 97` ```end ``` hoelzl@54258 ` 98` hoelzl@54261 ` 99` ```lemma (in order_top) bdd_above_top[simp, intro!]: "bdd_above A" ``` hoelzl@54261 ` 100` ``` by (rule bdd_aboveI[of _ top]) simp ``` hoelzl@54261 ` 101` hoelzl@54261 ` 102` ```lemma (in order_bot) bdd_above_bot[simp, intro!]: "bdd_below A" ``` hoelzl@54261 ` 103` ``` by (rule bdd_belowI[of _ bot]) simp ``` hoelzl@54261 ` 104` hoelzl@59452 ` 105` ```lemma bdd_above_image_mono: "mono f \ bdd_above A \ bdd_above (f`A)" ``` hoelzl@59452 ` 106` ``` by (auto simp: bdd_above_def mono_def) ``` hoelzl@59452 ` 107` hoelzl@59452 ` 108` ```lemma bdd_below_image_mono: "mono f \ bdd_below A \ bdd_below (f`A)" ``` hoelzl@59452 ` 109` ``` by (auto simp: bdd_below_def mono_def) ``` hoelzl@63331 ` 110` hoelzl@59452 ` 111` ```lemma bdd_above_image_antimono: "antimono f \ bdd_below A \ bdd_above (f`A)" ``` hoelzl@59452 ` 112` ``` by (auto simp: bdd_above_def bdd_below_def antimono_def) ``` hoelzl@54262 ` 113` hoelzl@59452 ` 114` ```lemma bdd_below_image_antimono: "antimono f \ bdd_above A \ bdd_below (f`A)" ``` hoelzl@59452 ` 115` ``` by (auto simp: bdd_above_def bdd_below_def antimono_def) ``` hoelzl@59452 ` 116` hoelzl@59452 ` 117` ```lemma ``` hoelzl@54262 ` 118` ``` fixes X :: "'a::ordered_ab_group_add set" ``` hoelzl@59452 ` 119` ``` shows bdd_above_uminus[simp]: "bdd_above (uminus ` X) \ bdd_below X" ``` hoelzl@59452 ` 120` ``` and bdd_below_uminus[simp]: "bdd_below (uminus ` X) \ bdd_above X" ``` hoelzl@59452 ` 121` ``` using bdd_above_image_antimono[of uminus X] bdd_below_image_antimono[of uminus "uminus`X"] ``` hoelzl@59452 ` 122` ``` using bdd_below_image_antimono[of uminus X] bdd_above_image_antimono[of uminus "uminus`X"] ``` hoelzl@59452 ` 123` ``` by (auto simp: antimono_def image_image) ``` hoelzl@54262 ` 124` hoelzl@54258 ` 125` ```context lattice ``` hoelzl@54258 ` 126` ```begin ``` hoelzl@54258 ` 127` hoelzl@54258 ` 128` ```lemma bdd_above_insert [simp]: "bdd_above (insert a A) = bdd_above A" ``` hoelzl@54258 ` 129` ``` by (auto simp: bdd_above_def intro: le_supI2 sup_ge1) ``` hoelzl@54258 ` 130` hoelzl@54258 ` 131` ```lemma bdd_below_insert [simp]: "bdd_below (insert a A) = bdd_below A" ``` hoelzl@54258 ` 132` ``` by (auto simp: bdd_below_def intro: le_infI2 inf_le1) ``` hoelzl@54258 ` 133` hoelzl@54258 ` 134` ```lemma bdd_finite [simp]: ``` hoelzl@54258 ` 135` ``` assumes "finite A" shows bdd_above_finite: "bdd_above A" and bdd_below_finite: "bdd_below A" ``` hoelzl@54258 ` 136` ``` using assms by (induct rule: finite_induct, auto) ``` hoelzl@54258 ` 137` hoelzl@54258 ` 138` ```lemma bdd_above_Un [simp]: "bdd_above (A \ B) = (bdd_above A \ bdd_above B)" ``` hoelzl@54258 ` 139` ```proof ``` hoelzl@54258 ` 140` ``` assume "bdd_above (A \ B)" ``` hoelzl@54258 ` 141` ``` thus "bdd_above A \ bdd_above B" unfolding bdd_above_def by auto ``` hoelzl@54258 ` 142` ```next ``` hoelzl@54258 ` 143` ``` assume "bdd_above A \ bdd_above B" ``` hoelzl@54258 ` 144` ``` then obtain a b where "\x\A. x \ a" "\x\B. x \ b" unfolding bdd_above_def by auto ``` hoelzl@54258 ` 145` ``` hence "\x \ A \ B. x \ sup a b" by (auto intro: Un_iff le_supI1 le_supI2) ``` hoelzl@54258 ` 146` ``` thus "bdd_above (A \ B)" unfolding bdd_above_def .. ``` hoelzl@54258 ` 147` ```qed ``` hoelzl@54258 ` 148` hoelzl@54258 ` 149` ```lemma bdd_below_Un [simp]: "bdd_below (A \ B) = (bdd_below A \ bdd_below B)" ``` hoelzl@54258 ` 150` ```proof ``` hoelzl@54258 ` 151` ``` assume "bdd_below (A \ B)" ``` hoelzl@54258 ` 152` ``` thus "bdd_below A \ bdd_below B" unfolding bdd_below_def by auto ``` hoelzl@54258 ` 153` ```next ``` hoelzl@54258 ` 154` ``` assume "bdd_below A \ bdd_below B" ``` hoelzl@54258 ` 155` ``` then obtain a b where "\x\A. a \ x" "\x\B. b \ x" unfolding bdd_below_def by auto ``` hoelzl@54258 ` 156` ``` hence "\x \ A \ B. inf a b \ x" by (auto intro: Un_iff le_infI1 le_infI2) ``` hoelzl@54258 ` 157` ``` thus "bdd_below (A \ B)" unfolding bdd_below_def .. ``` hoelzl@54258 ` 158` ```qed ``` hoelzl@54258 ` 159` hoelzl@54259 ` 160` ```lemma bdd_above_sup[simp]: "bdd_above ((\x. sup (f x) (g x)) ` A) \ bdd_above (f`A) \ bdd_above (g`A)" ``` hoelzl@54259 ` 161` ``` by (auto simp: bdd_above_def intro: le_supI1 le_supI2) ``` hoelzl@54259 ` 162` hoelzl@54259 ` 163` ```lemma bdd_below_inf[simp]: "bdd_below ((\x. inf (f x) (g x)) ` A) \ bdd_below (f`A) \ bdd_below (g`A)" ``` hoelzl@54259 ` 164` ``` by (auto simp: bdd_below_def intro: le_infI1 le_infI2) ``` hoelzl@54259 ` 165` hoelzl@54258 ` 166` ```end ``` hoelzl@54258 ` 167` hoelzl@54258 ` 168` wenzelm@60758 ` 169` ```text \ ``` hoelzl@51475 ` 170` hoelzl@51475 ` 171` ```To avoid name classes with the @{class complete_lattice}-class we prefix @{const Sup} and ``` hoelzl@51475 ` 172` ```@{const Inf} in theorem names with c. ``` hoelzl@51475 ` 173` wenzelm@60758 ` 174` ```\ ``` hoelzl@51475 ` 175` hoelzl@51773 ` 176` ```class conditionally_complete_lattice = lattice + Sup + Inf + ``` hoelzl@54258 ` 177` ``` assumes cInf_lower: "x \ X \ bdd_below X \ Inf X \ x" ``` hoelzl@51475 ` 178` ``` and cInf_greatest: "X \ {} \ (\x. x \ X \ z \ x) \ z \ Inf X" ``` hoelzl@54258 ` 179` ``` assumes cSup_upper: "x \ X \ bdd_above X \ x \ Sup X" ``` hoelzl@51475 ` 180` ``` and cSup_least: "X \ {} \ (\x. x \ X \ x \ z) \ Sup X \ z" ``` paulson@33269 ` 181` ```begin ``` hoelzl@51475 ` 182` hoelzl@54259 ` 183` ```lemma cSup_upper2: "x \ X \ y \ x \ bdd_above X \ y \ Sup X" ``` hoelzl@54259 ` 184` ``` by (metis cSup_upper order_trans) ``` hoelzl@54259 ` 185` hoelzl@54259 ` 186` ```lemma cInf_lower2: "x \ X \ x \ y \ bdd_below X \ Inf X \ y" ``` hoelzl@54259 ` 187` ``` by (metis cInf_lower order_trans) ``` hoelzl@54259 ` 188` hoelzl@54259 ` 189` ```lemma cSup_mono: "B \ {} \ bdd_above A \ (\b. b \ B \ \a\A. b \ a) \ Sup B \ Sup A" ``` hoelzl@54259 ` 190` ``` by (metis cSup_least cSup_upper2) ``` hoelzl@54259 ` 191` hoelzl@54259 ` 192` ```lemma cInf_mono: "B \ {} \ bdd_below A \ (\b. b \ B \ \a\A. a \ b) \ Inf A \ Inf B" ``` hoelzl@54259 ` 193` ``` by (metis cInf_greatest cInf_lower2) ``` hoelzl@54259 ` 194` hoelzl@54259 ` 195` ```lemma cSup_subset_mono: "A \ {} \ bdd_above B \ A \ B \ Sup A \ Sup B" ``` hoelzl@54259 ` 196` ``` by (metis cSup_least cSup_upper subsetD) ``` hoelzl@54259 ` 197` hoelzl@54259 ` 198` ```lemma cInf_superset_mono: "A \ {} \ bdd_below B \ A \ B \ Inf B \ Inf A" ``` hoelzl@54259 ` 199` ``` by (metis cInf_greatest cInf_lower subsetD) ``` hoelzl@54259 ` 200` hoelzl@54258 ` 201` ```lemma cSup_eq_maximum: "z \ X \ (\x. x \ X \ x \ z) \ Sup X = z" ``` hoelzl@54258 ` 202` ``` by (intro antisym cSup_upper[of z X] cSup_least[of X z]) auto ``` hoelzl@51475 ` 203` hoelzl@54258 ` 204` ```lemma cInf_eq_minimum: "z \ X \ (\x. x \ X \ z \ x) \ Inf X = z" ``` hoelzl@54258 ` 205` ``` by (intro antisym cInf_lower[of z X] cInf_greatest[of X z]) auto ``` hoelzl@51475 ` 206` hoelzl@54258 ` 207` ```lemma cSup_le_iff: "S \ {} \ bdd_above S \ Sup S \ a \ (\x\S. x \ a)" ``` hoelzl@51475 ` 208` ``` by (metis order_trans cSup_upper cSup_least) ``` hoelzl@51475 ` 209` hoelzl@54258 ` 210` ```lemma le_cInf_iff: "S \ {} \ bdd_below S \ a \ Inf S \ (\x\S. a \ x)" ``` hoelzl@51475 ` 211` ``` by (metis order_trans cInf_lower cInf_greatest) ``` hoelzl@51475 ` 212` hoelzl@51475 ` 213` ```lemma cSup_eq_non_empty: ``` hoelzl@51475 ` 214` ``` assumes 1: "X \ {}" ``` hoelzl@51475 ` 215` ``` assumes 2: "\x. x \ X \ x \ a" ``` hoelzl@51475 ` 216` ``` assumes 3: "\y. (\x. x \ X \ x \ y) \ a \ y" ``` hoelzl@51475 ` 217` ``` shows "Sup X = a" ``` hoelzl@51475 ` 218` ``` by (intro 3 1 antisym cSup_least) (auto intro: 2 1 cSup_upper) ``` hoelzl@51475 ` 219` hoelzl@51475 ` 220` ```lemma cInf_eq_non_empty: ``` hoelzl@51475 ` 221` ``` assumes 1: "X \ {}" ``` hoelzl@51475 ` 222` ``` assumes 2: "\x. x \ X \ a \ x" ``` hoelzl@51475 ` 223` ``` assumes 3: "\y. (\x. x \ X \ y \ x) \ y \ a" ``` hoelzl@51475 ` 224` ``` shows "Inf X = a" ``` hoelzl@51475 ` 225` ``` by (intro 3 1 antisym cInf_greatest) (auto intro: 2 1 cInf_lower) ``` hoelzl@51475 ` 226` hoelzl@54258 ` 227` ```lemma cInf_cSup: "S \ {} \ bdd_below S \ Inf S = Sup {x. \s\S. x \ s}" ``` hoelzl@54258 ` 228` ``` by (rule cInf_eq_non_empty) (auto intro!: cSup_upper cSup_least simp: bdd_below_def) ``` hoelzl@51518 ` 229` hoelzl@54258 ` 230` ```lemma cSup_cInf: "S \ {} \ bdd_above S \ Sup S = Inf {x. \s\S. s \ x}" ``` hoelzl@54258 ` 231` ``` by (rule cSup_eq_non_empty) (auto intro!: cInf_lower cInf_greatest simp: bdd_above_def) ``` hoelzl@54258 ` 232` hoelzl@54258 ` 233` ```lemma cSup_insert: "X \ {} \ bdd_above X \ Sup (insert a X) = sup a (Sup X)" ``` hoelzl@54258 ` 234` ``` by (intro cSup_eq_non_empty) (auto intro: le_supI2 cSup_upper cSup_least) ``` paulson@33269 ` 235` hoelzl@54258 ` 236` ```lemma cInf_insert: "X \ {} \ bdd_below X \ Inf (insert a X) = inf a (Inf X)" ``` hoelzl@54258 ` 237` ``` by (intro cInf_eq_non_empty) (auto intro: le_infI2 cInf_lower cInf_greatest) ``` hoelzl@51475 ` 238` hoelzl@54259 ` 239` ```lemma cSup_singleton [simp]: "Sup {x} = x" ``` hoelzl@54259 ` 240` ``` by (intro cSup_eq_maximum) auto ``` hoelzl@54259 ` 241` hoelzl@54259 ` 242` ```lemma cInf_singleton [simp]: "Inf {x} = x" ``` hoelzl@54259 ` 243` ``` by (intro cInf_eq_minimum) auto ``` hoelzl@54259 ` 244` hoelzl@54258 ` 245` ```lemma cSup_insert_If: "bdd_above X \ Sup (insert a X) = (if X = {} then a else sup a (Sup X))" ``` hoelzl@54258 ` 246` ``` using cSup_insert[of X] by simp ``` hoelzl@51475 ` 247` hoelzl@54259 ` 248` ```lemma cInf_insert_If: "bdd_below X \ Inf (insert a X) = (if X = {} then a else inf a (Inf X))" ``` hoelzl@54258 ` 249` ``` using cInf_insert[of X] by simp ``` hoelzl@51475 ` 250` hoelzl@51475 ` 251` ```lemma le_cSup_finite: "finite X \ x \ X \ x \ Sup X" ``` hoelzl@51475 ` 252` ```proof (induct X arbitrary: x rule: finite_induct) ``` hoelzl@51475 ` 253` ``` case (insert x X y) then show ?case ``` hoelzl@54258 ` 254` ``` by (cases "X = {}") (auto simp: cSup_insert intro: le_supI2) ``` hoelzl@51475 ` 255` ```qed simp ``` hoelzl@51475 ` 256` hoelzl@51475 ` 257` ```lemma cInf_le_finite: "finite X \ x \ X \ Inf X \ x" ``` hoelzl@51475 ` 258` ```proof (induct X arbitrary: x rule: finite_induct) ``` hoelzl@51475 ` 259` ``` case (insert x X y) then show ?case ``` hoelzl@54258 ` 260` ``` by (cases "X = {}") (auto simp: cInf_insert intro: le_infI2) ``` hoelzl@51475 ` 261` ```qed simp ``` hoelzl@51475 ` 262` hoelzl@51475 ` 263` ```lemma cSup_eq_Sup_fin: "finite X \ X \ {} \ Sup X = Sup_fin X" ``` hoelzl@54258 ` 264` ``` by (induct X rule: finite_ne_induct) (simp_all add: cSup_insert) ``` hoelzl@51475 ` 265` hoelzl@51475 ` 266` ```lemma cInf_eq_Inf_fin: "finite X \ X \ {} \ Inf X = Inf_fin X" ``` hoelzl@54258 ` 267` ``` by (induct X rule: finite_ne_induct) (simp_all add: cInf_insert) ``` hoelzl@51475 ` 268` hoelzl@51475 ` 269` ```lemma cSup_atMost[simp]: "Sup {..x} = x" ``` hoelzl@51475 ` 270` ``` by (auto intro!: cSup_eq_maximum) ``` hoelzl@51475 ` 271` hoelzl@51475 ` 272` ```lemma cSup_greaterThanAtMost[simp]: "y < x \ Sup {y<..x} = x" ``` hoelzl@51475 ` 273` ``` by (auto intro!: cSup_eq_maximum) ``` hoelzl@51475 ` 274` hoelzl@51475 ` 275` ```lemma cSup_atLeastAtMost[simp]: "y \ x \ Sup {y..x} = x" ``` hoelzl@51475 ` 276` ``` by (auto intro!: cSup_eq_maximum) ``` hoelzl@51475 ` 277` hoelzl@51475 ` 278` ```lemma cInf_atLeast[simp]: "Inf {x..} = x" ``` hoelzl@51475 ` 279` ``` by (auto intro!: cInf_eq_minimum) ``` hoelzl@51475 ` 280` hoelzl@51475 ` 281` ```lemma cInf_atLeastLessThan[simp]: "y < x \ Inf {y.. x \ Inf {y..x} = y" ``` hoelzl@51475 ` 285` ``` by (auto intro!: cInf_eq_minimum) ``` hoelzl@51475 ` 286` haftmann@56218 ` 287` ```lemma cINF_lower: "bdd_below (f ` A) \ x \ A \ INFIMUM A f \ f x" ``` haftmann@56166 ` 288` ``` using cInf_lower [of _ "f ` A"] by simp ``` hoelzl@54259 ` 289` haftmann@56218 ` 290` ```lemma cINF_greatest: "A \ {} \ (\x. x \ A \ m \ f x) \ m \ INFIMUM A f" ``` haftmann@56166 ` 291` ``` using cInf_greatest [of "f ` A"] by auto ``` hoelzl@54259 ` 292` haftmann@56218 ` 293` ```lemma cSUP_upper: "x \ A \ bdd_above (f ` A) \ f x \ SUPREMUM A f" ``` haftmann@56166 ` 294` ``` using cSup_upper [of _ "f ` A"] by simp ``` hoelzl@54259 ` 295` haftmann@56218 ` 296` ```lemma cSUP_least: "A \ {} \ (\x. x \ A \ f x \ M) \ SUPREMUM A f \ M" ``` haftmann@56166 ` 297` ``` using cSup_least [of "f ` A"] by auto ``` hoelzl@54259 ` 298` haftmann@56218 ` 299` ```lemma cINF_lower2: "bdd_below (f ` A) \ x \ A \ f x \ u \ INFIMUM A f \ u" ``` wenzelm@63092 ` 300` ``` by (auto intro: cINF_lower order_trans) ``` hoelzl@54259 ` 301` haftmann@56218 ` 302` ```lemma cSUP_upper2: "bdd_above (f ` A) \ x \ A \ u \ f x \ u \ SUPREMUM A f" ``` wenzelm@63092 ` 303` ``` by (auto intro: cSUP_upper order_trans) ``` hoelzl@54259 ` 304` lp15@60615 ` 305` ```lemma cSUP_const [simp]: "A \ {} \ (SUP x:A. c) = c" ``` hoelzl@54261 ` 306` ``` by (intro antisym cSUP_least) (auto intro: cSUP_upper) ``` hoelzl@54261 ` 307` lp15@60615 ` 308` ```lemma cINF_const [simp]: "A \ {} \ (INF x:A. c) = c" ``` hoelzl@54261 ` 309` ``` by (intro antisym cINF_greatest) (auto intro: cINF_lower) ``` hoelzl@54261 ` 310` haftmann@56218 ` 311` ```lemma le_cINF_iff: "A \ {} \ bdd_below (f ` A) \ u \ INFIMUM A f \ (\x\A. u \ f x)" ``` wenzelm@63092 ` 312` ``` by (metis cINF_greatest cINF_lower order_trans) ``` hoelzl@54259 ` 313` haftmann@56218 ` 314` ```lemma cSUP_le_iff: "A \ {} \ bdd_above (f ` A) \ SUPREMUM A f \ u \ (\x\A. f x \ u)" ``` wenzelm@63092 ` 315` ``` by (metis cSUP_least cSUP_upper order_trans) ``` hoelzl@54259 ` 316` hoelzl@54263 ` 317` ```lemma less_cINF_D: "bdd_below (f`A) \ y < (INF i:A. f i) \ i \ A \ y < f i" ``` hoelzl@54263 ` 318` ``` by (metis cINF_lower less_le_trans) ``` hoelzl@54263 ` 319` hoelzl@54263 ` 320` ```lemma cSUP_lessD: "bdd_above (f`A) \ (SUP i:A. f i) < y \ i \ A \ f i < y" ``` hoelzl@54263 ` 321` ``` by (metis cSUP_upper le_less_trans) ``` hoelzl@54263 ` 322` haftmann@56218 ` 323` ```lemma cINF_insert: "A \ {} \ bdd_below (f ` A) \ INFIMUM (insert a A) f = inf (f a) (INFIMUM A f)" ``` haftmann@62343 ` 324` ``` by (metis cInf_insert image_insert image_is_empty) ``` hoelzl@54259 ` 325` haftmann@56218 ` 326` ```lemma cSUP_insert: "A \ {} \ bdd_above (f ` A) \ SUPREMUM (insert a A) f = sup (f a) (SUPREMUM A f)" ``` haftmann@62343 ` 327` ``` by (metis cSup_insert image_insert image_is_empty) ``` hoelzl@54259 ` 328` haftmann@56218 ` 329` ```lemma cINF_mono: "B \ {} \ bdd_below (f ` A) \ (\m. m \ B \ \n\A. f n \ g m) \ INFIMUM A f \ INFIMUM B g" ``` haftmann@56166 ` 330` ``` using cInf_mono [of "g ` B" "f ` A"] by auto ``` hoelzl@54259 ` 331` haftmann@56218 ` 332` ```lemma cSUP_mono: "A \ {} \ bdd_above (g ` B) \ (\n. n \ A \ \m\B. f n \ g m) \ SUPREMUM A f \ SUPREMUM B g" ``` haftmann@56166 ` 333` ``` using cSup_mono [of "f ` A" "g ` B"] by auto ``` hoelzl@54259 ` 334` haftmann@56218 ` 335` ```lemma cINF_superset_mono: "A \ {} \ bdd_below (g ` B) \ A \ B \ (\x. x \ B \ g x \ f x) \ INFIMUM B g \ INFIMUM A f" ``` hoelzl@54259 ` 336` ``` by (rule cINF_mono) auto ``` hoelzl@54259 ` 337` haftmann@56218 ` 338` ```lemma cSUP_subset_mono: "A \ {} \ bdd_above (g ` B) \ A \ B \ (\x. x \ B \ f x \ g x) \ SUPREMUM A f \ SUPREMUM B g" ``` hoelzl@54259 ` 339` ``` by (rule cSUP_mono) auto ``` hoelzl@54259 ` 340` hoelzl@54259 ` 341` ```lemma less_eq_cInf_inter: "bdd_below A \ bdd_below B \ A \ B \ {} \ inf (Inf A) (Inf B) \ Inf (A \ B)" ``` hoelzl@54259 ` 342` ``` by (metis cInf_superset_mono lattice_class.inf_sup_ord(1) le_infI1) ``` hoelzl@54259 ` 343` hoelzl@54259 ` 344` ```lemma cSup_inter_less_eq: "bdd_above A \ bdd_above B \ A \ B \ {} \ Sup (A \ B) \ sup (Sup A) (Sup B) " ``` hoelzl@54259 ` 345` ``` by (metis cSup_subset_mono lattice_class.inf_sup_ord(1) le_supI1) ``` hoelzl@54259 ` 346` hoelzl@54259 ` 347` ```lemma cInf_union_distrib: "A \ {} \ bdd_below A \ B \ {} \ bdd_below B \ Inf (A \ B) = inf (Inf A) (Inf B)" ``` hoelzl@54259 ` 348` ``` by (intro antisym le_infI cInf_greatest cInf_lower) (auto intro: le_infI1 le_infI2 cInf_lower) ``` hoelzl@54259 ` 349` haftmann@56218 ` 350` ```lemma cINF_union: "A \ {} \ bdd_below (f`A) \ B \ {} \ bdd_below (f`B) \ INFIMUM (A \ B) f = inf (INFIMUM A f) (INFIMUM B f)" ``` haftmann@56166 ` 351` ``` using cInf_union_distrib [of "f ` A" "f ` B"] by (simp add: image_Un [symmetric]) ``` hoelzl@54259 ` 352` hoelzl@54259 ` 353` ```lemma cSup_union_distrib: "A \ {} \ bdd_above A \ B \ {} \ bdd_above B \ Sup (A \ B) = sup (Sup A) (Sup B)" ``` hoelzl@54259 ` 354` ``` by (intro antisym le_supI cSup_least cSup_upper) (auto intro: le_supI1 le_supI2 cSup_upper) ``` hoelzl@54259 ` 355` haftmann@56218 ` 356` ```lemma cSUP_union: "A \ {} \ bdd_above (f`A) \ B \ {} \ bdd_above (f`B) \ SUPREMUM (A \ B) f = sup (SUPREMUM A f) (SUPREMUM B f)" ``` haftmann@56166 ` 357` ``` using cSup_union_distrib [of "f ` A" "f ` B"] by (simp add: image_Un [symmetric]) ``` hoelzl@54259 ` 358` haftmann@56218 ` 359` ```lemma cINF_inf_distrib: "A \ {} \ bdd_below (f`A) \ bdd_below (g`A) \ inf (INFIMUM A f) (INFIMUM A g) = (INF a:A. inf (f a) (g a))" ``` hoelzl@54259 ` 360` ``` by (intro antisym le_infI cINF_greatest cINF_lower2) ``` hoelzl@54259 ` 361` ``` (auto intro: le_infI1 le_infI2 cINF_greatest cINF_lower le_infI) ``` hoelzl@54259 ` 362` haftmann@56218 ` 363` ```lemma SUP_sup_distrib: "A \ {} \ bdd_above (f`A) \ bdd_above (g`A) \ sup (SUPREMUM A f) (SUPREMUM A g) = (SUP a:A. sup (f a) (g a))" ``` hoelzl@54259 ` 364` ``` by (intro antisym le_supI cSUP_least cSUP_upper2) ``` hoelzl@54259 ` 365` ``` (auto intro: le_supI1 le_supI2 cSUP_least cSUP_upper le_supI) ``` hoelzl@54259 ` 366` hoelzl@57447 ` 367` ```lemma cInf_le_cSup: ``` hoelzl@57447 ` 368` ``` "A \ {} \ bdd_above A \ bdd_below A \ Inf A \ Sup A" ``` hoelzl@57447 ` 369` ``` by (auto intro!: cSup_upper2[of "SOME a. a \ A"] intro: someI cInf_lower) ``` hoelzl@57447 ` 370` paulson@33269 ` 371` ```end ``` paulson@33269 ` 372` hoelzl@51773 ` 373` ```instance complete_lattice \ conditionally_complete_lattice ``` wenzelm@61169 ` 374` ``` by standard (auto intro: Sup_upper Sup_least Inf_lower Inf_greatest) ``` hoelzl@51475 ` 375` hoelzl@51475 ` 376` ```lemma cSup_eq: ``` hoelzl@51773 ` 377` ``` fixes a :: "'a :: {conditionally_complete_lattice, no_bot}" ``` hoelzl@51475 ` 378` ``` assumes upper: "\x. x \ X \ x \ a" ``` hoelzl@51475 ` 379` ``` assumes least: "\y. (\x. x \ X \ x \ y) \ a \ y" ``` hoelzl@51475 ` 380` ``` shows "Sup X = a" ``` hoelzl@51475 ` 381` ```proof cases ``` hoelzl@51475 ` 382` ``` assume "X = {}" with lt_ex[of a] least show ?thesis by (auto simp: less_le_not_le) ``` hoelzl@51475 ` 383` ```qed (intro cSup_eq_non_empty assms) ``` hoelzl@51475 ` 384` hoelzl@51475 ` 385` ```lemma cInf_eq: ``` hoelzl@51773 ` 386` ``` fixes a :: "'a :: {conditionally_complete_lattice, no_top}" ``` hoelzl@51475 ` 387` ``` assumes upper: "\x. x \ X \ a \ x" ``` hoelzl@51475 ` 388` ``` assumes least: "\y. (\x. x \ X \ y \ x) \ y \ a" ``` hoelzl@51475 ` 389` ``` shows "Inf X = a" ``` hoelzl@51475 ` 390` ```proof cases ``` hoelzl@51475 ` 391` ``` assume "X = {}" with gt_ex[of a] least show ?thesis by (auto simp: less_le_not_le) ``` hoelzl@51475 ` 392` ```qed (intro cInf_eq_non_empty assms) ``` hoelzl@51475 ` 393` hoelzl@51773 ` 394` ```class conditionally_complete_linorder = conditionally_complete_lattice + linorder ``` paulson@33269 ` 395` ```begin ``` hoelzl@51475 ` 396` hoelzl@63331 ` 397` ```lemma less_cSup_iff: ``` hoelzl@54258 ` 398` ``` "X \ {} \ bdd_above X \ y < Sup X \ (\x\X. y < x)" ``` hoelzl@51475 ` 399` ``` by (rule iffI) (metis cSup_least not_less, metis cSup_upper less_le_trans) ``` hoelzl@51475 ` 400` hoelzl@54258 ` 401` ```lemma cInf_less_iff: "X \ {} \ bdd_below X \ Inf X < y \ (\x\X. x < y)" ``` hoelzl@51475 ` 402` ``` by (rule iffI) (metis cInf_greatest not_less, metis cInf_lower le_less_trans) ``` hoelzl@51475 ` 403` hoelzl@54263 ` 404` ```lemma cINF_less_iff: "A \ {} \ bdd_below (f`A) \ (INF i:A. f i) < a \ (\x\A. f x < a)" ``` haftmann@56166 ` 405` ``` using cInf_less_iff[of "f`A"] by auto ``` hoelzl@54263 ` 406` hoelzl@54263 ` 407` ```lemma less_cSUP_iff: "A \ {} \ bdd_above (f`A) \ a < (SUP i:A. f i) \ (\x\A. a < f x)" ``` haftmann@56166 ` 408` ``` using less_cSup_iff[of "f`A"] by auto ``` hoelzl@54263 ` 409` hoelzl@51475 ` 410` ```lemma less_cSupE: ``` hoelzl@51475 ` 411` ``` assumes "y < Sup X" "X \ {}" obtains x where "x \ X" "y < x" ``` hoelzl@51475 ` 412` ``` by (metis cSup_least assms not_le that) ``` hoelzl@51475 ` 413` hoelzl@51518 ` 414` ```lemma less_cSupD: ``` hoelzl@51518 ` 415` ``` "X \ {} \ z < Sup X \ \x\X. z < x" ``` lp15@61824 ` 416` ``` by (metis less_cSup_iff not_le_imp_less bdd_above_def) ``` hoelzl@51518 ` 417` hoelzl@51518 ` 418` ```lemma cInf_lessD: ``` hoelzl@51518 ` 419` ``` "X \ {} \ Inf X < z \ \x\X. x < z" ``` lp15@61824 ` 420` ``` by (metis cInf_less_iff not_le_imp_less bdd_below_def) ``` hoelzl@51518 ` 421` hoelzl@51475 ` 422` ```lemma complete_interval: ``` hoelzl@51475 ` 423` ``` assumes "a < b" and "P a" and "\ P b" ``` hoelzl@51475 ` 424` ``` shows "\c. a \ c \ c \ b \ (\x. a \ x \ x < c \ P x) \ ``` hoelzl@51475 ` 425` ``` (\d. (\x. a \ x \ x < d \ P x) \ d \ c)" ``` hoelzl@51475 ` 426` ```proof (rule exI [where x = "Sup {d. \x. a \ x & x < d --> P x}"], auto) ``` hoelzl@51475 ` 427` ``` show "a \ Sup {d. \c. a \ c \ c < d \ P c}" ``` hoelzl@54258 ` 428` ``` by (rule cSup_upper, auto simp: bdd_above_def) ``` wenzelm@60758 ` 429` ``` (metis \a < b\ \\ P b\ linear less_le) ``` hoelzl@51475 ` 430` ```next ``` hoelzl@51475 ` 431` ``` show "Sup {d. \c. a \ c \ c < d \ P c} \ b" ``` hoelzl@63331 ` 432` ``` apply (rule cSup_least) ``` hoelzl@51475 ` 433` ``` apply auto ``` hoelzl@51475 ` 434` ``` apply (metis less_le_not_le) ``` wenzelm@60758 ` 435` ``` apply (metis \a \~ P b\ linear less_le) ``` hoelzl@51475 ` 436` ``` done ``` hoelzl@51475 ` 437` ```next ``` hoelzl@51475 ` 438` ``` fix x ``` hoelzl@51475 ` 439` ``` assume x: "a \ x" and lt: "x < Sup {d. \c. a \ c \ c < d \ P c}" ``` hoelzl@51475 ` 440` ``` show "P x" ``` hoelzl@51475 ` 441` ``` apply (rule less_cSupE [OF lt], auto) ``` hoelzl@51475 ` 442` ``` apply (metis less_le_not_le) ``` hoelzl@63331 ` 443` ``` apply (metis x) ``` hoelzl@51475 ` 444` ``` done ``` hoelzl@51475 ` 445` ```next ``` hoelzl@51475 ` 446` ``` fix d ``` hoelzl@51475 ` 447` ``` assume 0: "\x. a \ x \ x < d \ P x" ``` hoelzl@51475 ` 448` ``` thus "d \ Sup {d. \c. a \ c \ c < d \ P c}" ``` hoelzl@54258 ` 449` ``` by (rule_tac cSup_upper, auto simp: bdd_above_def) ``` wenzelm@60758 ` 450` ``` (metis \a \~ P b\ linear less_le) ``` hoelzl@51475 ` 451` ```qed ``` hoelzl@51475 ` 452` hoelzl@51475 ` 453` ```end ``` hoelzl@51475 ` 454` hoelzl@60172 ` 455` ```instance complete_linorder < conditionally_complete_linorder ``` hoelzl@60172 ` 456` ``` .. ``` hoelzl@60172 ` 457` hoelzl@54259 ` 458` ```lemma cSup_eq_Max: "finite (X::'a::conditionally_complete_linorder set) \ X \ {} \ Sup X = Max X" ``` hoelzl@54259 ` 459` ``` using cSup_eq_Sup_fin[of X] Sup_fin_eq_Max[of X] by simp ``` hoelzl@51775 ` 460` hoelzl@54259 ` 461` ```lemma cInf_eq_Min: "finite (X::'a::conditionally_complete_linorder set) \ X \ {} \ Inf X = Min X" ``` hoelzl@54259 ` 462` ``` using cInf_eq_Inf_fin[of X] Inf_fin_eq_Min[of X] by simp ``` hoelzl@51775 ` 463` hoelzl@54257 ` 464` ```lemma cSup_lessThan[simp]: "Sup {.. Sup {y<.. Sup {y.. Inf {y<..x::'a::{conditionally_complete_linorder, dense_linorder}} = y" ``` hoelzl@57447 ` 477` ``` by (auto intro!: cInf_eq_non_empty intro: dense_ge_bounded) ``` hoelzl@51475 ` 478` hoelzl@57447 ` 479` ```lemma cInf_greaterThanLessThan[simp]: "y < x \ Inf {y<..a b::'a. a \ b" ``` hoelzl@54259 ` 484` ```begin ``` hoelzl@54259 ` 485` hoelzl@54259 ` 486` ```lemma ex_gt_or_lt: "\b. a < b \ b < a" ``` hoelzl@54259 ` 487` ``` by (metis UNIV_not_singleton neq_iff) ``` hoelzl@54259 ` 488` paulson@33269 ` 489` ```end ``` hoelzl@54259 ` 490` hoelzl@54281 ` 491` ```instantiation nat :: conditionally_complete_linorder ``` hoelzl@54281 ` 492` ```begin ``` hoelzl@54281 ` 493` hoelzl@54281 ` 494` ```definition "Sup (X::nat set) = Max X" ``` hoelzl@54281 ` 495` ```definition "Inf (X::nat set) = (LEAST n. n \ X)" ``` hoelzl@54281 ` 496` hoelzl@54281 ` 497` ```lemma bdd_above_nat: "bdd_above X \ finite (X::nat set)" ``` hoelzl@54281 ` 498` ```proof ``` hoelzl@54281 ` 499` ``` assume "bdd_above X" ``` hoelzl@54281 ` 500` ``` then obtain z where "X \ {.. z}" ``` hoelzl@54281 ` 501` ``` by (auto simp: bdd_above_def) ``` hoelzl@54281 ` 502` ``` then show "finite X" ``` hoelzl@54281 ` 503` ``` by (rule finite_subset) simp ``` hoelzl@54281 ` 504` ```qed simp ``` hoelzl@54281 ` 505` hoelzl@54281 ` 506` ```instance ``` hoelzl@54281 ` 507` ```proof ``` wenzelm@63540 ` 508` ``` fix x :: nat ``` wenzelm@63540 ` 509` ``` fix X :: "nat set" ``` wenzelm@63540 ` 510` ``` show "Inf X \ x" if "x \ X" "bdd_below X" ``` wenzelm@63540 ` 511` ``` using that by (simp add: Inf_nat_def Least_le) ``` wenzelm@63540 ` 512` ``` show "x \ Inf X" if "X \ {}" "\y. y \ X \ x \ y" ``` wenzelm@63540 ` 513` ``` using that unfolding Inf_nat_def ex_in_conv[symmetric] by (rule LeastI2_ex) ``` wenzelm@63540 ` 514` ``` show "x \ Sup X" if "x \ X" "bdd_above X" ``` wenzelm@63540 ` 515` ``` using that by (simp add: Sup_nat_def bdd_above_nat) ``` wenzelm@63540 ` 516` ``` show "Sup X \ x" if "X \ {}" "\y. y \ X \ y \ x" ``` wenzelm@63540 ` 517` ``` proof - ``` wenzelm@63540 ` 518` ``` from that have "bdd_above X" ``` hoelzl@54281 ` 519` ``` by (auto simp: bdd_above_def) ``` wenzelm@63540 ` 520` ``` with that show ?thesis ``` wenzelm@63540 ` 521` ``` by (simp add: Sup_nat_def bdd_above_nat) ``` wenzelm@63540 ` 522` ``` qed ``` hoelzl@54281 ` 523` ```qed ``` wenzelm@63540 ` 524` hoelzl@54259 ` 525` ```end ``` hoelzl@54281 ` 526` hoelzl@54281 ` 527` ```instantiation int :: conditionally_complete_linorder ``` hoelzl@54281 ` 528` ```begin ``` hoelzl@54281 ` 529` hoelzl@54281 ` 530` ```definition "Sup (X::int set) = (THE x. x \ X \ (\y\X. y \ x))" ``` hoelzl@54281 ` 531` ```definition "Inf (X::int set) = - (Sup (uminus ` X))" ``` hoelzl@54281 ` 532` hoelzl@54281 ` 533` ```instance ``` hoelzl@54281 ` 534` ```proof ``` hoelzl@54281 ` 535` ``` { fix x :: int and X :: "int set" assume "X \ {}" "bdd_above X" ``` hoelzl@54281 ` 536` ``` then obtain x y where "X \ {..y}" "x \ X" ``` hoelzl@54281 ` 537` ``` by (auto simp: bdd_above_def) ``` hoelzl@54281 ` 538` ``` then have *: "finite (X \ {x..y})" "X \ {x..y} \ {}" and "x \ y" ``` hoelzl@54281 ` 539` ``` by (auto simp: subset_eq) ``` hoelzl@54281 ` 540` ``` have "\!x\X. (\y\X. y \ x)" ``` hoelzl@54281 ` 541` ``` proof ``` hoelzl@54281 ` 542` ``` { fix z assume "z \ X" ``` hoelzl@54281 ` 543` ``` have "z \ Max (X \ {x..y})" ``` hoelzl@54281 ` 544` ``` proof cases ``` wenzelm@60758 ` 545` ``` assume "x \ z" with \z \ X\ \X \ {..y}\ *(1) show ?thesis ``` hoelzl@54281 ` 546` ``` by (auto intro!: Max_ge) ``` hoelzl@54281 ` 547` ``` next ``` hoelzl@54281 ` 548` ``` assume "\ x \ z" ``` hoelzl@54281 ` 549` ``` then have "z < x" by simp ``` hoelzl@54281 ` 550` ``` also have "x \ Max (X \ {x..y})" ``` wenzelm@60758 ` 551` ``` using \x \ X\ *(1) \x \ y\ by (intro Max_ge) auto ``` hoelzl@54281 ` 552` ``` finally show ?thesis by simp ``` hoelzl@54281 ` 553` ``` qed } ``` hoelzl@54281 ` 554` ``` note le = this ``` hoelzl@54281 ` 555` ``` with Max_in[OF *] show ex: "Max (X \ {x..y}) \ X \ (\z\X. z \ Max (X \ {x..y}))" by auto ``` hoelzl@54281 ` 556` hoelzl@54281 ` 557` ``` fix z assume *: "z \ X \ (\y\X. y \ z)" ``` hoelzl@54281 ` 558` ``` with le have "z \ Max (X \ {x..y})" ``` hoelzl@54281 ` 559` ``` by auto ``` hoelzl@54281 ` 560` ``` moreover have "Max (X \ {x..y}) \ z" ``` hoelzl@54281 ` 561` ``` using * ex by auto ``` hoelzl@54281 ` 562` ``` ultimately show "z = Max (X \ {x..y})" ``` hoelzl@54281 ` 563` ``` by auto ``` hoelzl@54281 ` 564` ``` qed ``` hoelzl@54281 ` 565` ``` then have "Sup X \ X \ (\y\X. y \ Sup X)" ``` hoelzl@54281 ` 566` ``` unfolding Sup_int_def by (rule theI') } ``` hoelzl@54281 ` 567` ``` note Sup_int = this ``` hoelzl@54281 ` 568` hoelzl@54281 ` 569` ``` { fix x :: int and X :: "int set" assume "x \ X" "bdd_above X" then show "x \ Sup X" ``` hoelzl@54281 ` 570` ``` using Sup_int[of X] by auto } ``` hoelzl@54281 ` 571` ``` note le_Sup = this ``` hoelzl@54281 ` 572` ``` { fix x :: int and X :: "int set" assume "X \ {}" "\y. y \ X \ y \ x" then show "Sup X \ x" ``` hoelzl@54281 ` 573` ``` using Sup_int[of X] by (auto simp: bdd_above_def) } ``` hoelzl@54281 ` 574` ``` note Sup_le = this ``` hoelzl@54281 ` 575` hoelzl@54281 ` 576` ``` { fix x :: int and X :: "int set" assume "x \ X" "bdd_below X" then show "Inf X \ x" ``` hoelzl@54281 ` 577` ``` using le_Sup[of "-x" "uminus ` X"] by (auto simp: Inf_int_def) } ``` hoelzl@54281 ` 578` ``` { fix x :: int and X :: "int set" assume "X \ {}" "\y. y \ X \ x \ y" then show "x \ Inf X" ``` hoelzl@54281 ` 579` ``` using Sup_le[of "uminus ` X" "-x"] by (force simp: Inf_int_def) } ``` hoelzl@54281 ` 580` ```qed ``` hoelzl@54281 ` 581` ```end ``` hoelzl@54281 ` 582` hoelzl@57275 ` 583` ```lemma interval_cases: ``` hoelzl@57275 ` 584` ``` fixes S :: "'a :: conditionally_complete_linorder set" ``` hoelzl@57275 ` 585` ``` assumes ivl: "\a b x. a \ S \ b \ S \ a \ x \ x \ b \ x \ S" ``` hoelzl@57275 ` 586` ``` shows "\a b. S = {} \ ``` hoelzl@57275 ` 587` ``` S = UNIV \ ``` hoelzl@57275 ` 588` ``` S = {.. ``` hoelzl@57275 ` 589` ``` S = {..b} \ ``` hoelzl@57275 ` 590` ``` S = {a<..} \ ``` hoelzl@57275 ` 591` ``` S = {a..} \ ``` hoelzl@57275 ` 592` ``` S = {a<.. ``` hoelzl@57275 ` 593` ``` S = {a<..b} \ ``` hoelzl@57275 ` 594` ``` S = {a.. ``` hoelzl@57275 ` 595` ``` S = {a..b}" ``` hoelzl@57275 ` 596` ```proof - ``` wenzelm@63040 ` 597` ``` define lower upper where "lower = {x. \s\S. s \ x}" and "upper = {x. \s\S. x \ s}" ``` hoelzl@57275 ` 598` ``` with ivl have "S = lower \ upper" ``` hoelzl@57275 ` 599` ``` by auto ``` hoelzl@63331 ` 600` ``` moreover ``` hoelzl@57275 ` 601` ``` have "\a. upper = UNIV \ upper = {} \ upper = {.. a} \ upper = {..< a}" ``` hoelzl@57275 ` 602` ``` proof cases ``` hoelzl@57275 ` 603` ``` assume *: "bdd_above S \ S \ {}" ``` hoelzl@57275 ` 604` ``` from * have "upper \ {.. Sup S}" ``` hoelzl@57275 ` 605` ``` by (auto simp: upper_def intro: cSup_upper2) ``` hoelzl@57275 ` 606` ``` moreover from * have "{..< Sup S} \ upper" ``` hoelzl@57275 ` 607` ``` by (force simp add: less_cSup_iff upper_def subset_eq Ball_def) ``` hoelzl@57275 ` 608` ``` ultimately have "upper = {.. Sup S} \ upper = {..< Sup S}" ``` hoelzl@57275 ` 609` ``` unfolding ivl_disj_un(2)[symmetric] by auto ``` hoelzl@57275 ` 610` ``` then show ?thesis by auto ``` hoelzl@57275 ` 611` ``` next ``` hoelzl@57275 ` 612` ``` assume "\ (bdd_above S \ S \ {})" ``` hoelzl@57275 ` 613` ``` then have "upper = UNIV \ upper = {}" ``` hoelzl@57275 ` 614` ``` by (auto simp: upper_def bdd_above_def not_le dest: less_imp_le) ``` hoelzl@57275 ` 615` ``` then show ?thesis ``` hoelzl@57275 ` 616` ``` by auto ``` hoelzl@57275 ` 617` ``` qed ``` hoelzl@57275 ` 618` ``` moreover ``` hoelzl@57275 ` 619` ``` have "\b. lower = UNIV \ lower = {} \ lower = {b ..} \ lower = {b <..}" ``` hoelzl@57275 ` 620` ``` proof cases ``` hoelzl@57275 ` 621` ``` assume *: "bdd_below S \ S \ {}" ``` hoelzl@57275 ` 622` ``` from * have "lower \ {Inf S ..}" ``` hoelzl@57275 ` 623` ``` by (auto simp: lower_def intro: cInf_lower2) ``` hoelzl@57275 ` 624` ``` moreover from * have "{Inf S <..} \ lower" ``` hoelzl@57275 ` 625` ``` by (force simp add: cInf_less_iff lower_def subset_eq Ball_def) ``` hoelzl@57275 ` 626` ``` ultimately have "lower = {Inf S ..} \ lower = {Inf S <..}" ``` hoelzl@57275 ` 627` ``` unfolding ivl_disj_un(1)[symmetric] by auto ``` hoelzl@57275 ` 628` ``` then show ?thesis by auto ``` hoelzl@57275 ` 629` ``` next ``` hoelzl@57275 ` 630` ``` assume "\ (bdd_below S \ S \ {})" ``` hoelzl@57275 ` 631` ``` then have "lower = UNIV \ lower = {}" ``` hoelzl@57275 ` 632` ``` by (auto simp: lower_def bdd_below_def not_le dest: less_imp_le) ``` hoelzl@57275 ` 633` ``` then show ?thesis ``` hoelzl@57275 ` 634` ``` by auto ``` hoelzl@57275 ` 635` ``` qed ``` hoelzl@57275 ` 636` ``` ultimately show ?thesis ``` hoelzl@57275 ` 637` ``` unfolding greaterThanAtMost_def greaterThanLessThan_def atLeastAtMost_def atLeastLessThan_def ``` wenzelm@63171 ` 638` ``` by (metis inf_bot_left inf_bot_right inf_top.left_neutral inf_top.right_neutral) ``` hoelzl@57275 ` 639` ```qed ``` hoelzl@57275 ` 640` lp15@60615 ` 641` ```lemma cSUP_eq_cINF_D: ``` lp15@60615 ` 642` ``` fixes f :: "_ \ 'b::conditionally_complete_lattice" ``` lp15@60615 ` 643` ``` assumes eq: "(SUP x:A. f x) = (INF x:A. f x)" ``` lp15@60615 ` 644` ``` and bdd: "bdd_above (f ` A)" "bdd_below (f ` A)" ``` lp15@60615 ` 645` ``` and a: "a \ A" ``` lp15@60615 ` 646` ``` shows "f a = (INF x:A. f x)" ``` lp15@60615 ` 647` ```apply (rule antisym) ``` lp15@60615 ` 648` ```using a bdd ``` lp15@60615 ` 649` ```apply (auto simp: cINF_lower) ``` lp15@60615 ` 650` ```apply (metis eq cSUP_upper) ``` hoelzl@63331 ` 651` ```done ``` lp15@60615 ` 652` lp15@62379 ` 653` ```lemma cSUP_UNION: ``` lp15@62379 ` 654` ``` fixes f :: "_ \ 'b::conditionally_complete_lattice" ``` lp15@62379 ` 655` ``` assumes ne: "A \ {}" "\x. x \ A \ B(x) \ {}" ``` lp15@62379 ` 656` ``` and bdd_UN: "bdd_above (\x\A. f ` B x)" ``` lp15@62379 ` 657` ``` shows "(SUP z : \x\A. B x. f z) = (SUP x:A. SUP z:B x. f z)" ``` lp15@62379 ` 658` ```proof - ``` lp15@62379 ` 659` ``` have bdd: "\x. x \ A \ bdd_above (f ` B x)" ``` lp15@62379 ` 660` ``` using bdd_UN by (meson UN_upper bdd_above_mono) ``` lp15@62379 ` 661` ``` obtain M where "\x y. x \ A \ y \ B(x) \ f y \ M" ``` lp15@62379 ` 662` ``` using bdd_UN by (auto simp: bdd_above_def) ``` lp15@62379 ` 663` ``` then have bdd2: "bdd_above ((\x. SUP z:B x. f z) ` A)" ``` lp15@62379 ` 664` ``` unfolding bdd_above_def by (force simp: bdd cSUP_le_iff ne(2)) ``` lp15@62379 ` 665` ``` have "(SUP z:\x\A. B x. f z) \ (SUP x:A. SUP z:B x. f z)" ``` lp15@62379 ` 666` ``` using assms by (fastforce simp add: intro!: cSUP_least intro: cSUP_upper2 simp: bdd2 bdd) ``` lp15@62379 ` 667` ``` moreover have "(SUP x:A. SUP z:B x. f z) \ (SUP z:\x\A. B x. f z)" ``` lp15@62379 ` 668` ``` using assms by (fastforce simp add: intro!: cSUP_least intro: cSUP_upper simp: image_UN bdd_UN) ``` lp15@62379 ` 669` ``` ultimately show ?thesis ``` lp15@62379 ` 670` ``` by (rule order_antisym) ``` lp15@62379 ` 671` ```qed ``` lp15@62379 ` 672` lp15@62379 ` 673` ```lemma cINF_UNION: ``` lp15@62379 ` 674` ``` fixes f :: "_ \ 'b::conditionally_complete_lattice" ``` lp15@62379 ` 675` ``` assumes ne: "A \ {}" "\x. x \ A \ B(x) \ {}" ``` lp15@62379 ` 676` ``` and bdd_UN: "bdd_below (\x\A. f ` B x)" ``` lp15@62379 ` 677` ``` shows "(INF z : \x\A. B x. f z) = (INF x:A. INF z:B x. f z)" ``` lp15@62379 ` 678` ```proof - ``` lp15@62379 ` 679` ``` have bdd: "\x. x \ A \ bdd_below (f ` B x)" ``` lp15@62379 ` 680` ``` using bdd_UN by (meson UN_upper bdd_below_mono) ``` lp15@62379 ` 681` ``` obtain M where "\x y. x \ A \ y \ B(x) \ f y \ M" ``` lp15@62379 ` 682` ``` using bdd_UN by (auto simp: bdd_below_def) ``` lp15@62379 ` 683` ``` then have bdd2: "bdd_below ((\x. INF z:B x. f z) ` A)" ``` lp15@62379 ` 684` ``` unfolding bdd_below_def by (force simp: bdd le_cINF_iff ne(2)) ``` lp15@62379 ` 685` ``` have "(INF z:\x\A. B x. f z) \ (INF x:A. INF z:B x. f z)" ``` lp15@62379 ` 686` ``` using assms by (fastforce simp add: intro!: cINF_greatest intro: cINF_lower simp: bdd2 bdd) ``` lp15@62379 ` 687` ``` moreover have "(INF x:A. INF z:B x. f z) \ (INF z:\x\A. B x. f z)" ``` lp15@62379 ` 688` ``` using assms by (fastforce simp add: intro!: cINF_greatest intro: cINF_lower2 simp: bdd bdd_UN bdd2) ``` lp15@62379 ` 689` ``` ultimately show ?thesis ``` lp15@62379 ` 690` ``` by (rule order_antisym) ``` lp15@62379 ` 691` ```qed ``` lp15@62379 ` 692` hoelzl@63331 ` 693` ```lemma cSup_abs_le: ``` lp15@62626 ` 694` ``` fixes S :: "('a::{linordered_idom,conditionally_complete_linorder}) set" ``` lp15@62626 ` 695` ``` shows "S \ {} \ (\x. x\S \ \x\ \ a) \ \Sup S\ \ a" ``` lp15@62626 ` 696` ``` apply (auto simp add: abs_le_iff intro: cSup_least) ``` lp15@62626 ` 697` ``` by (metis bdd_aboveI cSup_upper neg_le_iff_le order_trans) ``` lp15@62626 ` 698` hoelzl@54281 ` 699` ```end ```