src/HOL/SupInf.thy
 author haftmann Fri Nov 27 08:41:10 2009 +0100 (2009-11-27) changeset 33963 977b94b64905 parent 33657 a4179bf442d1 child 35028 108662d50512 permissions -rw-r--r--
renamed former datatype.ML to datatype_data.ML; datatype.ML provides uniform view on datatype.ML and datatype_rep_proofs.ML
 paulson@33269 ` 1` ```(* Author: Amine Chaieb and L C Paulson, University of Cambridge *) ``` paulson@33269 ` 2` paulson@33269 ` 3` ```header {*Sup and Inf Operators on Sets of Reals.*} ``` paulson@33269 ` 4` paulson@33269 ` 5` ```theory SupInf ``` paulson@33269 ` 6` ```imports RComplete ``` paulson@33269 ` 7` ```begin ``` paulson@33269 ` 8` paulson@33269 ` 9` ```lemma minus_max_eq_min: ``` paulson@33269 ` 10` ``` fixes x :: "'a::{lordered_ab_group_add, linorder}" ``` paulson@33269 ` 11` ``` shows "- (max x y) = min (-x) (-y)" ``` paulson@33269 ` 12` ```by (metis le_imp_neg_le linorder_linear min_max.inf_absorb2 min_max.le_iff_inf min_max.le_iff_sup min_max.sup_absorb1) ``` paulson@33269 ` 13` paulson@33269 ` 14` ```lemma minus_min_eq_max: ``` paulson@33269 ` 15` ``` fixes x :: "'a::{lordered_ab_group_add, linorder}" ``` paulson@33269 ` 16` ``` shows "- (min x y) = max (-x) (-y)" ``` paulson@33269 ` 17` ```by (metis minus_max_eq_min minus_minus) ``` paulson@33269 ` 18` paulson@33269 ` 19` ```lemma minus_Max_eq_Min [simp]: ``` paulson@33269 ` 20` ``` fixes S :: "'a::{lordered_ab_group_add, linorder} set" ``` paulson@33269 ` 21` ``` shows "finite S \ S \ {} \ - (Max S) = Min (uminus ` S)" ``` paulson@33269 ` 22` ```proof (induct S rule: finite_ne_induct) ``` paulson@33269 ` 23` ``` case (singleton x) ``` paulson@33269 ` 24` ``` thus ?case by simp ``` paulson@33269 ` 25` ```next ``` paulson@33269 ` 26` ``` case (insert x S) ``` paulson@33269 ` 27` ``` thus ?case by (simp add: minus_max_eq_min) ``` paulson@33269 ` 28` ```qed ``` paulson@33269 ` 29` paulson@33269 ` 30` ```lemma minus_Min_eq_Max [simp]: ``` paulson@33269 ` 31` ``` fixes S :: "'a::{lordered_ab_group_add, linorder} set" ``` paulson@33269 ` 32` ``` shows "finite S \ S \ {} \ - (Min S) = Max (uminus ` S)" ``` paulson@33269 ` 33` ```proof (induct S rule: finite_ne_induct) ``` paulson@33269 ` 34` ``` case (singleton x) ``` paulson@33269 ` 35` ``` thus ?case by simp ``` paulson@33269 ` 36` ```next ``` paulson@33269 ` 37` ``` case (insert x S) ``` paulson@33269 ` 38` ``` thus ?case by (simp add: minus_min_eq_max) ``` paulson@33269 ` 39` ```qed ``` paulson@33269 ` 40` paulson@33269 ` 41` ```instantiation real :: Sup ``` paulson@33269 ` 42` ```begin ``` paulson@33269 ` 43` ```definition ``` paulson@33269 ` 44` ``` Sup_real_def [code del]: "Sup X == (LEAST z::real. \x\X. x\z)" ``` paulson@33269 ` 45` paulson@33269 ` 46` ```instance .. ``` paulson@33269 ` 47` ```end ``` paulson@33269 ` 48` paulson@33269 ` 49` ```instantiation real :: Inf ``` paulson@33269 ` 50` ```begin ``` paulson@33269 ` 51` ```definition ``` paulson@33269 ` 52` ``` Inf_real_def [code del]: "Inf (X::real set) == - (Sup (uminus ` X))" ``` paulson@33269 ` 53` paulson@33269 ` 54` ```instance .. ``` paulson@33269 ` 55` ```end ``` paulson@33269 ` 56` paulson@33269 ` 57` ```subsection{*Supremum of a set of reals*} ``` paulson@33269 ` 58` paulson@33269 ` 59` ```lemma Sup_upper [intro]: (*REAL_SUP_UBOUND in HOL4*) ``` paulson@33269 ` 60` ``` fixes x :: real ``` paulson@33269 ` 61` ``` assumes x: "x \ X" ``` paulson@33269 ` 62` ``` and z: "!!x. x \ X \ x \ z" ``` paulson@33269 ` 63` ``` shows "x \ Sup X" ``` paulson@33269 ` 64` ```proof (auto simp add: Sup_real_def) ``` paulson@33269 ` 65` ``` from reals_complete2 ``` paulson@33269 ` 66` ``` obtain s where s: "(\y\X. y \ s) & (\z. ((\y\X. y \ z) --> s \ z))" ``` paulson@33269 ` 67` ``` by (blast intro: x z) ``` paulson@33269 ` 68` ``` hence "x \ s" ``` paulson@33269 ` 69` ``` by (blast intro: x z) ``` paulson@33269 ` 70` ``` also with s have "... = (LEAST z. \x\X. x \ z)" ``` paulson@33269 ` 71` ``` by (fast intro: Least_equality [symmetric]) ``` paulson@33269 ` 72` ``` finally show "x \ (LEAST z. \x\X. x \ z)" . ``` paulson@33269 ` 73` ```qed ``` paulson@33269 ` 74` paulson@33269 ` 75` ```lemma Sup_least [intro]: (*REAL_IMP_SUP_LE in HOL4*) ``` paulson@33269 ` 76` ``` fixes z :: real ``` paulson@33269 ` 77` ``` assumes x: "X \ {}" ``` paulson@33269 ` 78` ``` and z: "\x. x \ X \ x \ z" ``` paulson@33269 ` 79` ``` shows "Sup X \ z" ``` paulson@33269 ` 80` ```proof (auto simp add: Sup_real_def) ``` paulson@33269 ` 81` ``` from reals_complete2 x ``` paulson@33269 ` 82` ``` obtain s where s: "(\y\X. y \ s) & (\z. ((\y\X. y \ z) --> s \ z))" ``` paulson@33269 ` 83` ``` by (blast intro: z) ``` paulson@33269 ` 84` ``` hence "(LEAST z. \x\X. x \ z) = s" ``` paulson@33269 ` 85` ``` by (best intro: Least_equality) ``` paulson@33269 ` 86` ``` also with s z have "... \ z" ``` paulson@33269 ` 87` ``` by blast ``` paulson@33269 ` 88` ``` finally show "(LEAST z. \x\X. x \ z) \ z" . ``` paulson@33269 ` 89` ```qed ``` paulson@33269 ` 90` paulson@33609 ` 91` ```lemma less_SupE: ``` paulson@33609 ` 92` ``` fixes y :: real ``` paulson@33609 ` 93` ``` assumes "y < Sup X" "X \ {}" ``` paulson@33609 ` 94` ``` obtains x where "x\X" "y < x" ``` paulson@33609 ` 95` ```by (metis SupInf.Sup_least assms linorder_not_less that) ``` paulson@33609 ` 96` paulson@33269 ` 97` ```lemma Sup_singleton [simp]: "Sup {x::real} = x" ``` paulson@33269 ` 98` ``` by (force intro: Least_equality simp add: Sup_real_def) ``` paulson@33269 ` 99` ``` ``` paulson@33269 ` 100` ```lemma Sup_eq_maximum: (*REAL_SUP_MAX in HOL4*) ``` paulson@33269 ` 101` ``` fixes z :: real ``` paulson@33269 ` 102` ``` assumes X: "z \ X" and z: "!!x. x \ X \ x \ z" ``` paulson@33269 ` 103` ``` shows "Sup X = z" ``` paulson@33269 ` 104` ``` by (force intro: Least_equality X z simp add: Sup_real_def) ``` paulson@33269 ` 105` ``` ``` paulson@33269 ` 106` ```lemma Sup_upper2: (*REAL_IMP_LE_SUP in HOL4*) ``` paulson@33269 ` 107` ``` fixes x :: real ``` paulson@33269 ` 108` ``` shows "x \ X \ y \ x \ (!!x. x \ X \ x \ z) \ y \ Sup X" ``` paulson@33269 ` 109` ``` by (metis Sup_upper real_le_trans) ``` paulson@33269 ` 110` paulson@33269 ` 111` ```lemma Sup_real_iff : (*REAL_SUP_LE in HOL4*) ``` paulson@33269 ` 112` ``` fixes z :: real ``` paulson@33269 ` 113` ``` shows "X ~= {} ==> (!!x. x \ X ==> x \ z) ==> (\x\X. y y < Sup X" ``` paulson@33269 ` 114` ``` by (metis Sup_least Sup_upper linorder_not_le le_less_trans) ``` paulson@33269 ` 115` paulson@33269 ` 116` ```lemma Sup_eq: ``` paulson@33269 ` 117` ``` fixes a :: real ``` paulson@33269 ` 118` ``` shows "(!!x. x \ X \ x \ a) ``` paulson@33269 ` 119` ``` \ (!!y. (!!x. x \ X \ x \ y) \ a \ y) \ Sup X = a" ``` paulson@33269 ` 120` ``` by (metis Sup_least Sup_upper add_le_cancel_left diff_add_cancel insert_absorb ``` nipkow@33657 ` 121` ``` insert_not_empty real_le_antisym) ``` paulson@33269 ` 122` paulson@33269 ` 123` ```lemma Sup_le: ``` paulson@33269 ` 124` ``` fixes S :: "real set" ``` paulson@33269 ` 125` ``` shows "S \ {} \ S *<= b \ Sup S \ b" ``` paulson@33269 ` 126` ```by (metis SupInf.Sup_least setle_def) ``` paulson@33269 ` 127` paulson@33269 ` 128` ```lemma Sup_upper_EX: ``` paulson@33269 ` 129` ``` fixes x :: real ``` paulson@33269 ` 130` ``` shows "x \ X \ \z. \x. x \ X \ x \ z \ x \ Sup X" ``` paulson@33269 ` 131` ``` by blast ``` paulson@33269 ` 132` paulson@33269 ` 133` ```lemma Sup_insert_nonempty: ``` paulson@33269 ` 134` ``` fixes x :: real ``` paulson@33269 ` 135` ``` assumes x: "x \ X" ``` paulson@33269 ` 136` ``` and z: "!!x. x \ X \ x \ z" ``` paulson@33269 ` 137` ``` shows "Sup (insert a X) = max a (Sup X)" ``` paulson@33269 ` 138` ```proof (cases "Sup X \ a") ``` paulson@33269 ` 139` ``` case True ``` paulson@33269 ` 140` ``` thus ?thesis ``` paulson@33269 ` 141` ``` apply (simp add: max_def) ``` paulson@33269 ` 142` ``` apply (rule Sup_eq_maximum) ``` paulson@33269 ` 143` ``` apply (metis insertCI) ``` paulson@33269 ` 144` ``` apply (metis Sup_upper insertE le_iff_sup real_le_linear real_le_trans sup_absorb1 z) ``` paulson@33269 ` 145` ``` done ``` paulson@33269 ` 146` ```next ``` paulson@33269 ` 147` ``` case False ``` paulson@33269 ` 148` ``` hence 1:"a < Sup X" by simp ``` paulson@33269 ` 149` ``` have "Sup X \ Sup (insert a X)" ``` paulson@33269 ` 150` ``` apply (rule Sup_least) ``` paulson@33269 ` 151` ``` apply (metis empty_psubset_nonempty psubset_eq x) ``` paulson@33269 ` 152` ``` apply (rule Sup_upper_EX) ``` paulson@33269 ` 153` ``` apply blast ``` paulson@33269 ` 154` ``` apply (metis insert_iff real_le_linear real_le_refl real_le_trans z) ``` paulson@33269 ` 155` ``` done ``` paulson@33269 ` 156` ``` moreover ``` paulson@33269 ` 157` ``` have "Sup (insert a X) \ Sup X" ``` paulson@33269 ` 158` ``` apply (rule Sup_least) ``` paulson@33269 ` 159` ``` apply blast ``` paulson@33269 ` 160` ``` apply (metis False Sup_upper insertE real_le_linear z) ``` paulson@33269 ` 161` ``` done ``` paulson@33269 ` 162` ``` ultimately have "Sup (insert a X) = Sup X" ``` paulson@33269 ` 163` ``` by (blast intro: antisym ) ``` paulson@33269 ` 164` ``` thus ?thesis ``` paulson@33269 ` 165` ``` by (metis 1 min_max.le_iff_sup real_less_def) ``` paulson@33269 ` 166` ```qed ``` paulson@33269 ` 167` paulson@33269 ` 168` ```lemma Sup_insert_if: ``` paulson@33269 ` 169` ``` fixes X :: "real set" ``` paulson@33269 ` 170` ``` assumes z: "!!x. x \ X \ x \ z" ``` paulson@33269 ` 171` ``` shows "Sup (insert a X) = (if X={} then a else max a (Sup X))" ``` paulson@33269 ` 172` ```by auto (metis Sup_insert_nonempty z) ``` paulson@33269 ` 173` paulson@33269 ` 174` ```lemma Sup: ``` paulson@33269 ` 175` ``` fixes S :: "real set" ``` paulson@33269 ` 176` ``` shows "S \ {} \ (\b. S *<= b) \ isLub UNIV S (Sup S)" ``` paulson@33269 ` 177` ```by (auto simp add: isLub_def setle_def leastP_def isUb_def intro!: setgeI) ``` paulson@33269 ` 178` paulson@33269 ` 179` ```lemma Sup_finite_Max: ``` paulson@33269 ` 180` ``` fixes S :: "real set" ``` paulson@33269 ` 181` ``` assumes fS: "finite S" and Se: "S \ {}" ``` paulson@33269 ` 182` ``` shows "Sup S = Max S" ``` paulson@33269 ` 183` ```using fS Se ``` paulson@33269 ` 184` ```proof- ``` paulson@33269 ` 185` ``` let ?m = "Max S" ``` paulson@33269 ` 186` ``` from Max_ge[OF fS] have Sm: "\ x\ S. x \ ?m" by metis ``` paulson@33269 ` 187` ``` with Sup[OF Se] have lub: "isLub UNIV S (Sup S)" by (metis setle_def) ``` paulson@33269 ` 188` ``` from Max_in[OF fS Se] lub have mrS: "?m \ Sup S" ``` paulson@33269 ` 189` ``` by (auto simp add: isLub_def leastP_def setle_def setge_def isUb_def) ``` paulson@33269 ` 190` ``` moreover ``` paulson@33269 ` 191` ``` have "Sup S \ ?m" using Sm lub ``` paulson@33269 ` 192` ``` by (auto simp add: isLub_def leastP_def isUb_def setle_def setge_def) ``` paulson@33269 ` 193` ``` ultimately show ?thesis by arith ``` paulson@33269 ` 194` ```qed ``` paulson@33269 ` 195` paulson@33269 ` 196` ```lemma Sup_finite_in: ``` paulson@33269 ` 197` ``` fixes S :: "real set" ``` paulson@33269 ` 198` ``` assumes fS: "finite S" and Se: "S \ {}" ``` paulson@33269 ` 199` ``` shows "Sup S \ S" ``` paulson@33269 ` 200` ``` using Sup_finite_Max[OF fS Se] Max_in[OF fS Se] by metis ``` paulson@33269 ` 201` paulson@33269 ` 202` ```lemma Sup_finite_ge_iff: ``` paulson@33269 ` 203` ``` fixes S :: "real set" ``` paulson@33269 ` 204` ``` assumes fS: "finite S" and Se: "S \ {}" ``` paulson@33269 ` 205` ``` shows "a \ Sup S \ (\ x \ S. a \ x)" ``` paulson@33269 ` 206` ```by (metis Max_ge Se Sup_finite_Max Sup_finite_in fS linorder_not_le less_le_trans) ``` paulson@33269 ` 207` paulson@33269 ` 208` ```lemma Sup_finite_le_iff: ``` paulson@33269 ` 209` ``` fixes S :: "real set" ``` paulson@33269 ` 210` ``` assumes fS: "finite S" and Se: "S \ {}" ``` paulson@33269 ` 211` ``` shows "a \ Sup S \ (\ x \ S. a \ x)" ``` paulson@33269 ` 212` ```by (metis Max_ge Se Sup_finite_Max Sup_finite_in fS le_iff_sup real_le_trans) ``` paulson@33269 ` 213` paulson@33269 ` 214` ```lemma Sup_finite_gt_iff: ``` paulson@33269 ` 215` ``` fixes S :: "real set" ``` paulson@33269 ` 216` ``` assumes fS: "finite S" and Se: "S \ {}" ``` paulson@33269 ` 217` ``` shows "a < Sup S \ (\ x \ S. a < x)" ``` paulson@33269 ` 218` ```by (metis Se Sup_finite_le_iff fS linorder_not_less) ``` paulson@33269 ` 219` paulson@33269 ` 220` ```lemma Sup_finite_lt_iff: ``` paulson@33269 ` 221` ``` fixes S :: "real set" ``` paulson@33269 ` 222` ``` assumes fS: "finite S" and Se: "S \ {}" ``` paulson@33269 ` 223` ``` shows "a > Sup S \ (\ x \ S. a > x)" ``` paulson@33269 ` 224` ```by (metis Se Sup_finite_ge_iff fS linorder_not_less) ``` paulson@33269 ` 225` paulson@33269 ` 226` ```lemma Sup_unique: ``` paulson@33269 ` 227` ``` fixes S :: "real set" ``` paulson@33269 ` 228` ``` shows "S *<= b \ (\b' < b. \x \ S. b' < x) \ Sup S = b" ``` paulson@33269 ` 229` ```unfolding setle_def ``` paulson@33269 ` 230` ```apply (rule Sup_eq, auto) ``` paulson@33269 ` 231` ```apply (metis linorder_not_less) ``` paulson@33269 ` 232` ```done ``` paulson@33269 ` 233` paulson@33269 ` 234` ```lemma Sup_abs_le: ``` paulson@33269 ` 235` ``` fixes S :: "real set" ``` paulson@33269 ` 236` ``` shows "S \ {} \ (\x\S. \x\ \ a) \ \Sup S\ \ a" ``` paulson@33269 ` 237` ```by (auto simp add: abs_le_interval_iff) (metis Sup_upper2) ``` paulson@33269 ` 238` paulson@33269 ` 239` ```lemma Sup_bounds: ``` paulson@33269 ` 240` ``` fixes S :: "real set" ``` paulson@33269 ` 241` ``` assumes Se: "S \ {}" and l: "a <=* S" and u: "S *<= b" ``` paulson@33269 ` 242` ``` shows "a \ Sup S \ Sup S \ b" ``` paulson@33269 ` 243` ```proof- ``` paulson@33269 ` 244` ``` from Sup[OF Se] u have lub: "isLub UNIV S (Sup S)" by blast ``` paulson@33269 ` 245` ``` hence b: "Sup S \ b" using u ``` paulson@33269 ` 246` ``` by (auto simp add: isLub_def leastP_def setle_def setge_def isUb_def) ``` paulson@33269 ` 247` ``` from Se obtain y where y: "y \ S" by blast ``` paulson@33269 ` 248` ``` from lub l have "a \ Sup S" ``` paulson@33269 ` 249` ``` by (auto simp add: isLub_def leastP_def setle_def setge_def isUb_def) ``` paulson@33269 ` 250` ``` (metis le_iff_sup le_sup_iff y) ``` paulson@33269 ` 251` ``` with b show ?thesis by blast ``` paulson@33269 ` 252` ```qed ``` paulson@33269 ` 253` paulson@33269 ` 254` ```lemma Sup_asclose: ``` paulson@33269 ` 255` ``` fixes S :: "real set" ``` paulson@33269 ` 256` ``` assumes S:"S \ {}" and b: "\x\S. \x - l\ \ e" shows "\Sup S - l\ \ e" ``` paulson@33269 ` 257` ```proof- ``` paulson@33269 ` 258` ``` have th: "\(x::real) l e. \x - l\ \ e \ l - e \ x \ x \ l + e" by arith ``` paulson@33269 ` 259` ``` thus ?thesis using S b Sup_bounds[of S "l - e" "l+e"] unfolding th ``` paulson@33269 ` 260` ``` by (auto simp add: setge_def setle_def) ``` paulson@33269 ` 261` ```qed ``` paulson@33269 ` 262` paulson@33269 ` 263` paulson@33269 ` 264` ```subsection{*Infimum of a set of reals*} ``` paulson@33269 ` 265` paulson@33269 ` 266` ```lemma Inf_lower [intro]: ``` paulson@33269 ` 267` ``` fixes z :: real ``` paulson@33269 ` 268` ``` assumes x: "x \ X" ``` paulson@33269 ` 269` ``` and z: "!!x. x \ X \ z \ x" ``` paulson@33269 ` 270` ``` shows "Inf X \ x" ``` paulson@33269 ` 271` ```proof - ``` paulson@33269 ` 272` ``` have "-x \ Sup (uminus ` X)" ``` paulson@33269 ` 273` ``` by (rule Sup_upper [where z = "-z"]) (auto simp add: image_iff x z) ``` paulson@33269 ` 274` ``` thus ?thesis ``` paulson@33269 ` 275` ``` by (auto simp add: Inf_real_def) ``` paulson@33269 ` 276` ```qed ``` paulson@33269 ` 277` paulson@33269 ` 278` ```lemma Inf_greatest [intro]: ``` paulson@33269 ` 279` ``` fixes z :: real ``` paulson@33269 ` 280` ``` assumes x: "X \ {}" ``` paulson@33269 ` 281` ``` and z: "\x. x \ X \ z \ x" ``` paulson@33269 ` 282` ``` shows "z \ Inf X" ``` paulson@33269 ` 283` ```proof - ``` paulson@33269 ` 284` ``` have "Sup (uminus ` X) \ -z" using x z by (force intro: Sup_least) ``` paulson@33269 ` 285` ``` hence "z \ - Sup (uminus ` X)" ``` paulson@33269 ` 286` ``` by simp ``` paulson@33269 ` 287` ``` thus ?thesis ``` paulson@33269 ` 288` ``` by (auto simp add: Inf_real_def) ``` paulson@33269 ` 289` ```qed ``` paulson@33269 ` 290` paulson@33269 ` 291` ```lemma Inf_singleton [simp]: "Inf {x::real} = x" ``` paulson@33269 ` 292` ``` by (simp add: Inf_real_def) ``` paulson@33269 ` 293` ``` ``` paulson@33269 ` 294` ```lemma Inf_eq_minimum: (*REAL_INF_MIN in HOL4*) ``` paulson@33269 ` 295` ``` fixes z :: real ``` paulson@33269 ` 296` ``` assumes x: "z \ X" and z: "!!x. x \ X \ z \ x" ``` paulson@33269 ` 297` ``` shows "Inf X = z" ``` paulson@33269 ` 298` ```proof - ``` paulson@33269 ` 299` ``` have "Sup (uminus ` X) = -z" using x z ``` paulson@33269 ` 300` ``` by (force intro: Sup_eq_maximum x z) ``` paulson@33269 ` 301` ``` thus ?thesis ``` paulson@33269 ` 302` ``` by (simp add: Inf_real_def) ``` paulson@33269 ` 303` ```qed ``` paulson@33269 ` 304` ``` ``` paulson@33269 ` 305` ```lemma Inf_lower2: ``` paulson@33269 ` 306` ``` fixes x :: real ``` paulson@33269 ` 307` ``` shows "x \ X \ x \ y \ (!!x. x \ X \ z \ x) \ Inf X \ y" ``` paulson@33269 ` 308` ``` by (metis Inf_lower real_le_trans) ``` paulson@33269 ` 309` paulson@33269 ` 310` ```lemma Inf_real_iff: ``` paulson@33269 ` 311` ``` fixes z :: real ``` paulson@33269 ` 312` ``` shows "X \ {} \ (!!x. x \ X \ z \ x) \ (\x\X. x Inf X < y" ``` paulson@33269 ` 313` ``` by (metis Inf_greatest Inf_lower less_le_not_le real_le_linear ``` paulson@33269 ` 314` ``` order_less_le_trans) ``` paulson@33269 ` 315` paulson@33269 ` 316` ```lemma Inf_eq: ``` paulson@33269 ` 317` ``` fixes a :: real ``` paulson@33269 ` 318` ``` shows "(!!x. x \ X \ a \ x) \ (!!y. (!!x. x \ X \ y \ x) \ y \ a) \ Inf X = a" ``` paulson@33269 ` 319` ``` by (metis Inf_greatest Inf_lower add_le_cancel_left diff_add_cancel ``` nipkow@33657 ` 320` ``` insert_absorb insert_not_empty real_le_antisym) ``` paulson@33269 ` 321` paulson@33269 ` 322` ```lemma Inf_ge: ``` paulson@33269 ` 323` ``` fixes S :: "real set" ``` paulson@33269 ` 324` ``` shows "S \ {} \ b <=* S \ Inf S \ b" ``` paulson@33269 ` 325` ```by (metis SupInf.Inf_greatest setge_def) ``` paulson@33269 ` 326` paulson@33269 ` 327` ```lemma Inf_lower_EX: ``` paulson@33269 ` 328` ``` fixes x :: real ``` paulson@33269 ` 329` ``` shows "x \ X \ \z. \x. x \ X \ z \ x \ Inf X \ x" ``` paulson@33269 ` 330` ``` by blast ``` paulson@33269 ` 331` paulson@33269 ` 332` ```lemma Inf_insert_nonempty: ``` paulson@33269 ` 333` ``` fixes x :: real ``` paulson@33269 ` 334` ``` assumes x: "x \ X" ``` paulson@33269 ` 335` ``` and z: "!!x. x \ X \ z \ x" ``` paulson@33269 ` 336` ``` shows "Inf (insert a X) = min a (Inf X)" ``` paulson@33269 ` 337` ```proof (cases "a \ Inf X") ``` paulson@33269 ` 338` ``` case True ``` paulson@33269 ` 339` ``` thus ?thesis ``` paulson@33269 ` 340` ``` by (simp add: min_def) ``` paulson@33269 ` 341` ``` (blast intro: Inf_eq_minimum Inf_lower real_le_refl real_le_trans z) ``` paulson@33269 ` 342` ```next ``` paulson@33269 ` 343` ``` case False ``` paulson@33269 ` 344` ``` hence 1:"Inf X < a" by simp ``` paulson@33269 ` 345` ``` have "Inf (insert a X) \ Inf X" ``` paulson@33269 ` 346` ``` apply (rule Inf_greatest) ``` paulson@33269 ` 347` ``` apply (metis empty_psubset_nonempty psubset_eq x) ``` paulson@33269 ` 348` ``` apply (rule Inf_lower_EX) ``` paulson@33269 ` 349` ``` apply (blast intro: elim:) ``` paulson@33269 ` 350` ``` apply (metis insert_iff real_le_linear real_le_refl real_le_trans z) ``` paulson@33269 ` 351` ``` done ``` paulson@33269 ` 352` ``` moreover ``` paulson@33269 ` 353` ``` have "Inf X \ Inf (insert a X)" ``` paulson@33269 ` 354` ``` apply (rule Inf_greatest) ``` paulson@33269 ` 355` ``` apply blast ``` paulson@33269 ` 356` ``` apply (metis False Inf_lower insertE real_le_linear z) ``` paulson@33269 ` 357` ``` done ``` paulson@33269 ` 358` ``` ultimately have "Inf (insert a X) = Inf X" ``` paulson@33269 ` 359` ``` by (blast intro: antisym ) ``` paulson@33269 ` 360` ``` thus ?thesis ``` paulson@33269 ` 361` ``` by (metis False min_max.inf_absorb2 real_le_linear) ``` paulson@33269 ` 362` ```qed ``` paulson@33269 ` 363` paulson@33269 ` 364` ```lemma Inf_insert_if: ``` paulson@33269 ` 365` ``` fixes X :: "real set" ``` paulson@33269 ` 366` ``` assumes z: "!!x. x \ X \ z \ x" ``` paulson@33269 ` 367` ``` shows "Inf (insert a X) = (if X={} then a else min a (Inf X))" ``` paulson@33269 ` 368` ```by auto (metis Inf_insert_nonempty z) ``` paulson@33269 ` 369` paulson@33269 ` 370` ```lemma Inf_greater: ``` paulson@33269 ` 371` ``` fixes z :: real ``` paulson@33269 ` 372` ``` shows "X \ {} \ Inf X < z \ \x \ X. x < z" ``` paulson@33269 ` 373` ``` by (metis Inf_real_iff mem_def not_leE) ``` paulson@33269 ` 374` paulson@33269 ` 375` ```lemma Inf_close: ``` paulson@33269 ` 376` ``` fixes e :: real ``` paulson@33269 ` 377` ``` shows "X \ {} \ 0 < e \ \x \ X. x < Inf X + e" ``` paulson@33269 ` 378` ``` by (metis add_strict_increasing comm_monoid_add.mult_commute Inf_greater linorder_not_le pos_add_strict) ``` paulson@33269 ` 379` paulson@33269 ` 380` ```lemma Inf_finite_Min: ``` paulson@33269 ` 381` ``` fixes S :: "real set" ``` paulson@33269 ` 382` ``` shows "finite S \ S \ {} \ Inf S = Min S" ``` paulson@33269 ` 383` ```by (simp add: Inf_real_def Sup_finite_Max image_image) ``` paulson@33269 ` 384` paulson@33269 ` 385` ```lemma Inf_finite_in: ``` paulson@33269 ` 386` ``` fixes S :: "real set" ``` paulson@33269 ` 387` ``` assumes fS: "finite S" and Se: "S \ {}" ``` paulson@33269 ` 388` ``` shows "Inf S \ S" ``` paulson@33269 ` 389` ``` using Inf_finite_Min[OF fS Se] Min_in[OF fS Se] by metis ``` paulson@33269 ` 390` paulson@33269 ` 391` ```lemma Inf_finite_ge_iff: ``` paulson@33269 ` 392` ``` fixes S :: "real set" ``` paulson@33269 ` 393` ``` shows "finite S \ S \ {} \ a \ Inf S \ (\ x \ S. a \ x)" ``` paulson@33269 ` 394` ```by (metis Inf_finite_Min Inf_finite_in Min_le real_le_trans) ``` paulson@33269 ` 395` paulson@33269 ` 396` ```lemma Inf_finite_le_iff: ``` paulson@33269 ` 397` ``` fixes S :: "real set" ``` paulson@33269 ` 398` ``` shows "finite S \ S \ {} \ a \ Inf S \ (\ x \ S. a \ x)" ``` paulson@33269 ` 399` ```by (metis Inf_finite_Min Inf_finite_ge_iff Inf_finite_in Min_le ``` nipkow@33657 ` 400` ``` real_le_antisym real_le_linear) ``` paulson@33269 ` 401` paulson@33269 ` 402` ```lemma Inf_finite_gt_iff: ``` paulson@33269 ` 403` ``` fixes S :: "real set" ``` paulson@33269 ` 404` ``` shows "finite S \ S \ {} \ a < Inf S \ (\ x \ S. a < x)" ``` paulson@33269 ` 405` ```by (metis Inf_finite_le_iff linorder_not_less) ``` paulson@33269 ` 406` paulson@33269 ` 407` ```lemma Inf_finite_lt_iff: ``` paulson@33269 ` 408` ``` fixes S :: "real set" ``` paulson@33269 ` 409` ``` shows "finite S \ S \ {} \ a > Inf S \ (\ x \ S. a > x)" ``` paulson@33269 ` 410` ```by (metis Inf_finite_ge_iff linorder_not_less) ``` paulson@33269 ` 411` paulson@33269 ` 412` ```lemma Inf_unique: ``` paulson@33269 ` 413` ``` fixes S :: "real set" ``` paulson@33269 ` 414` ``` shows "b <=* S \ (\b' > b. \x \ S. b' > x) \ Inf S = b" ``` paulson@33269 ` 415` ```unfolding setge_def ``` paulson@33269 ` 416` ```apply (rule Inf_eq, auto) ``` paulson@33269 ` 417` ```apply (metis less_le_not_le linorder_not_less) ``` paulson@33269 ` 418` ```done ``` paulson@33269 ` 419` paulson@33269 ` 420` ```lemma Inf_abs_ge: ``` paulson@33269 ` 421` ``` fixes S :: "real set" ``` paulson@33269 ` 422` ``` shows "S \ {} \ (\x\S. \x\ \ a) \ \Inf S\ \ a" ``` paulson@33269 ` 423` ```by (simp add: Inf_real_def) (rule Sup_abs_le, auto) ``` paulson@33269 ` 424` paulson@33269 ` 425` ```lemma Inf_asclose: ``` paulson@33269 ` 426` ``` fixes S :: "real set" ``` paulson@33269 ` 427` ``` assumes S:"S \ {}" and b: "\x\S. \x - l\ \ e" shows "\Inf S - l\ \ e" ``` paulson@33269 ` 428` ```proof - ``` paulson@33269 ` 429` ``` have "\- Sup (uminus ` S) - l\ = \Sup (uminus ` S) - (-l)\" ``` paulson@33269 ` 430` ``` by auto ``` paulson@33269 ` 431` ``` also have "... \ e" ``` paulson@33269 ` 432` ``` apply (rule Sup_asclose) ``` paulson@33269 ` 433` ``` apply (auto simp add: S) ``` paulson@33269 ` 434` ``` apply (metis abs_minus_add_cancel b comm_monoid_add.mult_commute real_diff_def) ``` paulson@33269 ` 435` ``` done ``` paulson@33269 ` 436` ``` finally have "\- Sup (uminus ` S) - l\ \ e" . ``` paulson@33269 ` 437` ``` thus ?thesis ``` paulson@33269 ` 438` ``` by (simp add: Inf_real_def) ``` paulson@33269 ` 439` ```qed ``` paulson@33269 ` 440` paulson@33271 ` 441` ```subsection{*Relate max and min to Sup and Inf.*} ``` paulson@33269 ` 442` paulson@33269 ` 443` ```lemma real_max_Sup: ``` paulson@33269 ` 444` ``` fixes x :: real ``` paulson@33269 ` 445` ``` shows "max x y = Sup {x,y}" ``` paulson@33269 ` 446` ```proof- ``` paulson@33269 ` 447` ``` have f: "finite {x, y}" "{x,y} \ {}" by simp_all ``` paulson@33269 ` 448` ``` from Sup_finite_le_iff[OF f, of "max x y"] have "Sup {x,y} \ max x y" by simp ``` paulson@33269 ` 449` ``` moreover ``` paulson@33269 ` 450` ``` have "max x y \ Sup {x,y}" using Sup_finite_ge_iff[OF f, of "max x y"] ``` paulson@33269 ` 451` ``` by (simp add: linorder_linear) ``` paulson@33269 ` 452` ``` ultimately show ?thesis by arith ``` paulson@33269 ` 453` ```qed ``` paulson@33269 ` 454` paulson@33269 ` 455` ```lemma real_min_Inf: ``` paulson@33269 ` 456` ``` fixes x :: real ``` paulson@33269 ` 457` ``` shows "min x y = Inf {x,y}" ``` paulson@33269 ` 458` ```proof- ``` paulson@33269 ` 459` ``` have f: "finite {x, y}" "{x,y} \ {}" by simp_all ``` paulson@33269 ` 460` ``` from Inf_finite_le_iff[OF f, of "min x y"] have "Inf {x,y} \ min x y" ``` paulson@33269 ` 461` ``` by (simp add: linorder_linear) ``` paulson@33269 ` 462` ``` moreover ``` paulson@33269 ` 463` ``` have "min x y \ Inf {x,y}" using Inf_finite_ge_iff[OF f, of "min x y"] ``` paulson@33269 ` 464` ``` by simp ``` paulson@33269 ` 465` ``` ultimately show ?thesis by arith ``` paulson@33269 ` 466` ```qed ``` paulson@33269 ` 467` paulson@33609 ` 468` ```lemma reals_complete_interval: ``` paulson@33609 ` 469` ``` fixes a::real and b::real ``` paulson@33609 ` 470` ``` assumes "a < b" and "P a" and "~P b" ``` paulson@33609 ` 471` ``` shows "\c. a \ c & c \ b & (\x. a \ x & x < c --> P x) & ``` paulson@33609 ` 472` ``` (\d. (\x. a \ x & x < d --> P x) --> d \ c)" ``` paulson@33609 ` 473` ```proof (rule exI [where x = "Sup {d. \x. a \ x & x < d --> P x}"], auto) ``` paulson@33609 ` 474` ``` show "a \ Sup {d. \c. a \ c \ c < d \ P c}" ``` paulson@33609 ` 475` ``` by (rule SupInf.Sup_upper [where z=b], auto) ``` paulson@33609 ` 476` ``` (metis prems real_le_linear real_less_def) ``` paulson@33609 ` 477` ```next ``` paulson@33609 ` 478` ``` show "Sup {d. \c. a \ c \ c < d \ P c} \ b" ``` paulson@33609 ` 479` ``` apply (rule SupInf.Sup_least) ``` paulson@33609 ` 480` ``` apply (auto simp add: ) ``` paulson@33609 ` 481` ``` apply (metis less_le_not_le) ``` paulson@33609 ` 482` ``` apply (metis `a x" and lt: "x < Sup {d. \c. a \ c \ c < d \ P c}" ``` paulson@33609 ` 487` ``` show "P x" ``` paulson@33609 ` 488` ``` apply (rule less_SupE [OF lt], auto) ``` paulson@33609 ` 489` ``` apply (metis less_le_not_le) ``` paulson@33609 ` 490` ``` apply (metis x) ``` paulson@33609 ` 491` ``` done ``` paulson@33609 ` 492` ```next ``` paulson@33609 ` 493` ``` fix d ``` paulson@33609 ` 494` ``` assume 0: "\x. a \ x \ x < d \ P x" ``` paulson@33609 ` 495` ``` thus "d \ Sup {d. \c. a \ c \ c < d \ P c}" ``` paulson@33609 ` 496` ``` by (rule_tac z="b" in SupInf.Sup_upper, auto) ``` paulson@33609 ` 497` ``` (metis `a