src/HOL/Multivariate_Analysis/Ordered_Euclidean_Space.thy
 author haftmann Sun Mar 16 18:09:04 2014 +0100 (2014-03-16) changeset 56166 9a241bc276cd parent 55413 a8e96847523c child 56188 0268784f60da permissions -rw-r--r--
normalising simp rules for compound operators
 immler@54780 ` 1` ```theory Ordered_Euclidean_Space ``` immler@54780 ` 2` ```imports ``` immler@54780 ` 3` ``` Topology_Euclidean_Space ``` immler@54780 ` 4` ``` "~~/src/HOL/Library/Product_Order" ``` immler@54780 ` 5` ```begin ``` immler@54780 ` 6` immler@54780 ` 7` ```subsection {* An ordering on euclidean spaces that will allow us to talk about intervals *} ``` immler@54780 ` 8` immler@54780 ` 9` ```class ordered_euclidean_space = ord + inf + sup + abs + Inf + Sup + euclidean_space + ``` immler@54780 ` 10` ``` assumes eucl_le: "x \ y \ (\i\Basis. x \ i \ y \ i)" ``` immler@54780 ` 11` ``` assumes eucl_less_le_not_le: "x < y \ x \ y \ \ y \ x" ``` immler@54780 ` 12` ``` assumes eucl_inf: "inf x y = (\i\Basis. inf (x \ i) (y \ i) *\<^sub>R i)" ``` immler@54780 ` 13` ``` assumes eucl_sup: "sup x y = (\i\Basis. sup (x \ i) (y \ i) *\<^sub>R i)" ``` immler@54780 ` 14` ``` assumes eucl_Inf: "Inf X = (\i\Basis. (INF x:X. x \ i) *\<^sub>R i)" ``` immler@54780 ` 15` ``` assumes eucl_Sup: "Sup X = (\i\Basis. (SUP x:X. x \ i) *\<^sub>R i)" ``` immler@54780 ` 16` ``` assumes eucl_abs: "abs x = (\i\Basis. abs (x \ i) *\<^sub>R i)" ``` immler@54780 ` 17` ```begin ``` immler@54780 ` 18` immler@54780 ` 19` ```subclass order ``` immler@54780 ` 20` ``` by default ``` immler@54780 ` 21` ``` (auto simp: eucl_le eucl_less_le_not_le intro!: euclidean_eqI antisym intro: order.trans) ``` immler@54780 ` 22` immler@54780 ` 23` ```subclass ordered_ab_group_add_abs ``` immler@54780 ` 24` ``` by default (auto simp: eucl_le inner_add_left eucl_abs abs_leI) ``` immler@54780 ` 25` immler@54780 ` 26` ```subclass ordered_real_vector ``` immler@54780 ` 27` ``` by default (auto simp: eucl_le intro!: mult_left_mono mult_right_mono) ``` immler@54780 ` 28` immler@54780 ` 29` ```subclass lattice ``` immler@54780 ` 30` ``` by default (auto simp: eucl_inf eucl_sup eucl_le) ``` immler@54780 ` 31` immler@54780 ` 32` ```subclass distrib_lattice ``` immler@54780 ` 33` ``` by default (auto simp: eucl_inf eucl_sup sup_inf_distrib1 intro!: euclidean_eqI) ``` immler@54780 ` 34` immler@54780 ` 35` ```subclass conditionally_complete_lattice ``` immler@54780 ` 36` ```proof ``` immler@54780 ` 37` ``` fix z::'a and X::"'a set" ``` immler@54780 ` 38` ``` assume "X \ {}" ``` immler@54780 ` 39` ``` hence "\i. (\x. x \ i) ` X \ {}" by simp ``` immler@54780 ` 40` ``` thus "(\x. x \ X \ z \ x) \ z \ Inf X" "(\x. x \ X \ x \ z) \ Sup X \ z" ``` immler@54780 ` 41` ``` by (auto simp: eucl_Inf eucl_Sup eucl_le Inf_class.INF_def Sup_class.SUP_def ``` haftmann@56166 ` 42` ``` simp del: Inf_class.Inf_image_eq Sup_class.Sup_image_eq ``` immler@54780 ` 43` ``` intro!: cInf_greatest cSup_least) ``` immler@54780 ` 44` ```qed (force intro!: cInf_lower cSup_upper ``` immler@54780 ` 45` ``` simp: bdd_below_def bdd_above_def preorder_class.bdd_below_def preorder_class.bdd_above_def ``` haftmann@56166 ` 46` ``` eucl_Inf eucl_Sup eucl_le Inf_class.INF_def Sup_class.SUP_def ``` haftmann@56166 ` 47` ``` simp del: Inf_class.Inf_image_eq Sup_class.Sup_image_eq)+ ``` immler@54780 ` 48` immler@54780 ` 49` ```lemma inner_Basis_inf_left: "i \ Basis \ inf x y \ i = inf (x \ i) (y \ i)" ``` immler@54780 ` 50` ``` and inner_Basis_sup_left: "i \ Basis \ sup x y \ i = sup (x \ i) (y \ i)" ``` immler@54780 ` 51` ``` by (simp_all add: eucl_inf eucl_sup inner_setsum_left inner_Basis if_distrib setsum_delta ``` immler@54780 ` 52` ``` cong: if_cong) ``` immler@54780 ` 53` immler@54780 ` 54` ```lemma inner_Basis_INF_left: "i \ Basis \ (INF x:X. f x) \ i = (INF x:X. f x \ i)" ``` immler@54780 ` 55` ``` and inner_Basis_SUP_left: "i \ Basis \ (SUP x:X. f x) \ i = (SUP x:X. f x \ i)" ``` haftmann@56166 ` 56` ``` using eucl_Sup [of "f ` X"] eucl_Inf [of "f ` X"] by (simp_all add: comp_def) ``` immler@54780 ` 57` immler@54780 ` 58` ```lemma abs_inner: "i \ Basis \ abs x \ i = abs (x \ i)" ``` immler@54780 ` 59` ``` by (auto simp: eucl_abs) ``` immler@54780 ` 60` immler@54780 ` 61` ```lemma ``` immler@54780 ` 62` ``` abs_scaleR: "\a *\<^sub>R b\ = \a\ *\<^sub>R \b\" ``` immler@54780 ` 63` ``` by (auto simp: eucl_abs abs_mult intro!: euclidean_eqI) ``` immler@54780 ` 64` immler@54780 ` 65` ```lemma interval_inner_leI: ``` immler@54780 ` 66` ``` assumes "x \ {a .. b}" "0 \ i" ``` immler@54780 ` 67` ``` shows "a\i \ x\i" "x\i \ b\i" ``` immler@54780 ` 68` ``` using assms ``` immler@54780 ` 69` ``` unfolding euclidean_inner[of a i] euclidean_inner[of x i] euclidean_inner[of b i] ``` immler@54780 ` 70` ``` by (auto intro!: setsum_mono mult_right_mono simp: eucl_le) ``` immler@54780 ` 71` immler@54780 ` 72` ```lemma inner_nonneg_nonneg: ``` immler@54780 ` 73` ``` shows "0 \ a \ 0 \ b \ 0 \ a \ b" ``` immler@54780 ` 74` ``` using interval_inner_leI[of a 0 a b] ``` immler@54780 ` 75` ``` by auto ``` immler@54780 ` 76` immler@54780 ` 77` ```lemma inner_Basis_mono: ``` immler@54780 ` 78` ``` shows "a \ b \ c \ Basis \ a \ c \ b \ c" ``` immler@54780 ` 79` ``` by (simp add: eucl_le) ``` immler@54780 ` 80` immler@54780 ` 81` ```lemma Basis_nonneg[intro, simp]: "i \ Basis \ 0 \ i" ``` immler@54780 ` 82` ``` by (auto simp: eucl_le inner_Basis) ``` immler@54780 ` 83` immler@54781 ` 84` ```lemma Sup_eq_maximum_componentwise: ``` immler@54781 ` 85` ``` fixes s::"'a set" ``` immler@54781 ` 86` ``` assumes i: "\b. b \ Basis \ X \ b = i b \ b" ``` immler@54781 ` 87` ``` assumes sup: "\b x. b \ Basis \ x \ s \ x \ b \ X \ b" ``` immler@54781 ` 88` ``` assumes i_s: "\b. b \ Basis \ (i b \ b) \ (\x. x \ b) ` s" ``` immler@54781 ` 89` ``` shows "Sup s = X" ``` immler@54781 ` 90` ``` using assms ``` immler@54781 ` 91` ``` unfolding eucl_Sup euclidean_representation_setsum ``` haftmann@56166 ` 92` ``` by (auto simp: Sup_class.SUP_def simp del: Sup_class.Sup_image_eq intro!: conditionally_complete_lattice_class.cSup_eq_maximum) ``` immler@54781 ` 93` immler@54781 ` 94` ```lemma Inf_eq_minimum_componentwise: ``` immler@54781 ` 95` ``` assumes i: "\b. b \ Basis \ X \ b = i b \ b" ``` immler@54781 ` 96` ``` assumes sup: "\b x. b \ Basis \ x \ s \ X \ b \ x \ b" ``` immler@54781 ` 97` ``` assumes i_s: "\b. b \ Basis \ (i b \ b) \ (\x. x \ b) ` s" ``` immler@54781 ` 98` ``` shows "Inf s = X" ``` immler@54781 ` 99` ``` using assms ``` immler@54781 ` 100` ``` unfolding eucl_Inf euclidean_representation_setsum ``` haftmann@56166 ` 101` ``` by (auto simp: Inf_class.INF_def simp del: Inf_class.Inf_image_eq intro!: conditionally_complete_lattice_class.cInf_eq_minimum) ``` immler@54781 ` 102` immler@54780 ` 103` ```end ``` immler@54780 ` 104` immler@54781 ` 105` ```lemma ``` immler@54781 ` 106` ``` compact_attains_Inf_componentwise: ``` immler@54781 ` 107` ``` fixes b::"'a::ordered_euclidean_space" ``` immler@54781 ` 108` ``` assumes "b \ Basis" assumes "X \ {}" "compact X" ``` immler@54781 ` 109` ``` obtains x where "x \ X" "x \ b = Inf X \ b" "\y. y \ X \ x \ b \ y \ b" ``` immler@54781 ` 110` ```proof atomize_elim ``` immler@54781 ` 111` ``` let ?proj = "(\x. x \ b) ` X" ``` immler@54781 ` 112` ``` from assms have "compact ?proj" "?proj \ {}" ``` immler@54781 ` 113` ``` by (auto intro!: compact_continuous_image continuous_on_intros) ``` immler@54781 ` 114` ``` from compact_attains_inf[OF this] ``` immler@54781 ` 115` ``` obtain s x ``` immler@54781 ` 116` ``` where s: "s\(\x. x \ b) ` X" "\t. t\(\x. x \ b) ` X \ s \ t" ``` immler@54781 ` 117` ``` and x: "x \ X" "s = x \ b" "\y. y \ X \ x \ b \ y \ b" ``` immler@54781 ` 118` ``` by auto ``` immler@54781 ` 119` ``` hence "Inf ?proj = x \ b" ``` haftmann@56166 ` 120` ``` by (auto intro!: conditionally_complete_lattice_class.cInf_eq_minimum simp del: Inf_class.Inf_image_eq) ``` immler@54781 ` 121` ``` hence "x \ b = Inf X \ b" ``` haftmann@56166 ` 122` ``` by (auto simp: eucl_Inf Inf_class.INF_def inner_setsum_left inner_Basis if_distrib `b \ Basis` setsum_delta ``` haftmann@56166 ` 123` ``` simp del: Inf_class.Inf_image_eq ``` haftmann@56166 ` 124` ``` cong: if_cong) ``` immler@54781 ` 125` ``` with x show "\x. x \ X \ x \ b = Inf X \ b \ (\y. y \ X \ x \ b \ y \ b)" by blast ``` immler@54781 ` 126` ```qed ``` immler@54781 ` 127` immler@54781 ` 128` ```lemma ``` immler@54781 ` 129` ``` compact_attains_Sup_componentwise: ``` immler@54781 ` 130` ``` fixes b::"'a::ordered_euclidean_space" ``` immler@54781 ` 131` ``` assumes "b \ Basis" assumes "X \ {}" "compact X" ``` immler@54781 ` 132` ``` obtains x where "x \ X" "x \ b = Sup X \ b" "\y. y \ X \ y \ b \ x \ b" ``` immler@54781 ` 133` ```proof atomize_elim ``` immler@54781 ` 134` ``` let ?proj = "(\x. x \ b) ` X" ``` immler@54781 ` 135` ``` from assms have "compact ?proj" "?proj \ {}" ``` immler@54781 ` 136` ``` by (auto intro!: compact_continuous_image continuous_on_intros) ``` immler@54781 ` 137` ``` from compact_attains_sup[OF this] ``` immler@54781 ` 138` ``` obtain s x ``` immler@54781 ` 139` ``` where s: "s\(\x. x \ b) ` X" "\t. t\(\x. x \ b) ` X \ t \ s" ``` immler@54781 ` 140` ``` and x: "x \ X" "s = x \ b" "\y. y \ X \ y \ b \ x \ b" ``` immler@54781 ` 141` ``` by auto ``` immler@54781 ` 142` ``` hence "Sup ?proj = x \ b" ``` haftmann@56166 ` 143` ``` by (auto intro!: cSup_eq_maximum simp del: Sup_image_eq) ``` immler@54781 ` 144` ``` hence "x \ b = Sup X \ b" ``` haftmann@56166 ` 145` ``` by (auto simp: eucl_Sup[where 'a='a] SUP_def inner_setsum_left inner_Basis if_distrib `b \ Basis` setsum_delta ``` haftmann@56166 ` 146` ``` simp del: Sup_image_eq cong: if_cong) ``` immler@54781 ` 147` ``` with x show "\x. x \ X \ x \ b = Sup X \ b \ (\y. y \ X \ y \ b \ x \ b)" by blast ``` immler@54781 ` 148` ```qed ``` immler@54781 ` 149` immler@54780 ` 150` ```lemma (in order) atLeastatMost_empty'[simp]: ``` immler@54780 ` 151` ``` "(~ a <= b) \ {a..b} = {}" ``` immler@54780 ` 152` ``` by (auto) ``` immler@54780 ` 153` immler@54780 ` 154` ```instance real :: ordered_euclidean_space ``` immler@54780 ` 155` ``` by default (auto simp: INF_def SUP_def) ``` immler@54780 ` 156` immler@54780 ` 157` ```lemma in_Basis_prod_iff: ``` immler@54780 ` 158` ``` fixes i::"'a::euclidean_space*'b::euclidean_space" ``` immler@54780 ` 159` ``` shows "i \ Basis \ fst i = 0 \ snd i \ Basis \ snd i = 0 \ fst i \ Basis" ``` immler@54780 ` 160` ``` by (cases i) (auto simp: Basis_prod_def) ``` immler@54780 ` 161` immler@54780 ` 162` ```instantiation prod::(abs, abs) abs ``` immler@54780 ` 163` ```begin ``` immler@54780 ` 164` immler@54780 ` 165` ```definition "abs x = (abs (fst x), abs (snd x))" ``` immler@54780 ` 166` immler@54780 ` 167` ```instance proof qed ``` immler@54780 ` 168` ```end ``` immler@54780 ` 169` immler@54780 ` 170` ```instance prod :: (ordered_euclidean_space, ordered_euclidean_space) ordered_euclidean_space ``` immler@54780 ` 171` ``` by default ``` immler@54780 ` 172` ``` (auto intro!: add_mono simp add: euclidean_representation_setsum' Ball_def inner_prod_def ``` immler@54780 ` 173` ``` in_Basis_prod_iff inner_Basis_inf_left inner_Basis_sup_left inner_Basis_INF_left Inf_prod_def ``` immler@54780 ` 174` ``` inner_Basis_SUP_left Sup_prod_def less_prod_def less_eq_prod_def eucl_le[where 'a='a] ``` immler@54780 ` 175` ``` eucl_le[where 'a='b] abs_prod_def abs_inner) ``` immler@54780 ` 176` immler@54780 ` 177` immler@54780 ` 178` ```subsection {* Intervals *} ``` immler@54780 ` 179` immler@54780 ` 180` ```lemma interval: ``` immler@54780 ` 181` ``` fixes a :: "'a::ordered_euclidean_space" ``` immler@54780 ` 182` ``` shows "box a b = {x::'a. \i\Basis. a\i < x\i \ x\i < b\i}" ``` immler@54780 ` 183` ``` and "{a .. b} = {x::'a. \i\Basis. a\i \ x\i \ x\i \ b\i}" ``` immler@54780 ` 184` ``` by (auto simp add:set_eq_iff eucl_le[where 'a='a] box_def) ``` immler@54780 ` 185` immler@54780 ` 186` ```lemma mem_interval: ``` immler@54780 ` 187` ``` fixes a :: "'a::ordered_euclidean_space" ``` immler@54780 ` 188` ``` shows "x \ box a b \ (\i\Basis. a\i < x\i \ x\i < b\i)" ``` immler@54780 ` 189` ``` and "x \ {a .. b} \ (\i\Basis. a\i \ x\i \ x\i \ b\i)" ``` immler@54780 ` 190` ``` using interval[of a b] ``` immler@54780 ` 191` ``` by auto ``` immler@54780 ` 192` immler@54780 ` 193` ```lemma interval_eq_empty: ``` immler@54780 ` 194` ``` fixes a :: "'a::ordered_euclidean_space" ``` immler@54780 ` 195` ``` shows "(box a b = {} \ (\i\Basis. b\i \ a\i))" (is ?th1) ``` immler@54780 ` 196` ``` and "({a .. b} = {} \ (\i\Basis. b\i < a\i))" (is ?th2) ``` immler@54780 ` 197` ```proof - ``` immler@54780 ` 198` ``` { ``` immler@54780 ` 199` ``` fix i x ``` immler@54780 ` 200` ``` assume i: "i\Basis" and as:"b\i \ a\i" and x:"x\box a b" ``` immler@54780 ` 201` ``` then have "a \ i < x \ i \ x \ i < b \ i" ``` immler@54780 ` 202` ``` unfolding mem_interval by auto ``` immler@54780 ` 203` ``` then have "a\i < b\i" by auto ``` immler@54780 ` 204` ``` then have False using as by auto ``` immler@54780 ` 205` ``` } ``` immler@54780 ` 206` ``` moreover ``` immler@54780 ` 207` ``` { ``` immler@54780 ` 208` ``` assume as: "\i\Basis. \ (b\i \ a\i)" ``` immler@54780 ` 209` ``` let ?x = "(1/2) *\<^sub>R (a + b)" ``` immler@54780 ` 210` ``` { ``` immler@54780 ` 211` ``` fix i :: 'a ``` immler@54780 ` 212` ``` assume i: "i \ Basis" ``` immler@54780 ` 213` ``` have "a\i < b\i" ``` immler@54780 ` 214` ``` using as[THEN bspec[where x=i]] i by auto ``` immler@54780 ` 215` ``` then have "a\i < ((1/2) *\<^sub>R (a+b)) \ i" "((1/2) *\<^sub>R (a+b)) \ i < b\i" ``` immler@54780 ` 216` ``` by (auto simp: inner_add_left) ``` immler@54780 ` 217` ``` } ``` immler@54780 ` 218` ``` then have "box a b \ {}" ``` immler@54780 ` 219` ``` using mem_interval(1)[of "?x" a b] by auto ``` immler@54780 ` 220` ``` } ``` immler@54780 ` 221` ``` ultimately show ?th1 by blast ``` immler@54780 ` 222` immler@54780 ` 223` ``` { ``` immler@54780 ` 224` ``` fix i x ``` immler@54780 ` 225` ``` assume i: "i \ Basis" and as:"b\i < a\i" and x:"x\{a .. b}" ``` immler@54780 ` 226` ``` then have "a \ i \ x \ i \ x \ i \ b \ i" ``` immler@54780 ` 227` ``` unfolding mem_interval by auto ``` immler@54780 ` 228` ``` then have "a\i \ b\i" by auto ``` immler@54780 ` 229` ``` then have False using as by auto ``` immler@54780 ` 230` ``` } ``` immler@54780 ` 231` ``` moreover ``` immler@54780 ` 232` ``` { ``` immler@54780 ` 233` ``` assume as:"\i\Basis. \ (b\i < a\i)" ``` immler@54780 ` 234` ``` let ?x = "(1/2) *\<^sub>R (a + b)" ``` immler@54780 ` 235` ``` { ``` immler@54780 ` 236` ``` fix i :: 'a ``` immler@54780 ` 237` ``` assume i:"i \ Basis" ``` immler@54780 ` 238` ``` have "a\i \ b\i" ``` immler@54780 ` 239` ``` using as[THEN bspec[where x=i]] i by auto ``` immler@54780 ` 240` ``` then have "a\i \ ((1/2) *\<^sub>R (a+b)) \ i" "((1/2) *\<^sub>R (a+b)) \ i \ b\i" ``` immler@54780 ` 241` ``` by (auto simp: inner_add_left) ``` immler@54780 ` 242` ``` } ``` immler@54780 ` 243` ``` then have "{a .. b} \ {}" ``` immler@54780 ` 244` ``` using mem_interval(2)[of "?x" a b] by auto ``` immler@54780 ` 245` ``` } ``` immler@54780 ` 246` ``` ultimately show ?th2 by blast ``` immler@54780 ` 247` ```qed ``` immler@54780 ` 248` immler@54780 ` 249` ```lemma interval_ne_empty: ``` immler@54780 ` 250` ``` fixes a :: "'a::ordered_euclidean_space" ``` immler@54780 ` 251` ``` shows "{a .. b} \ {} \ (\i\Basis. a\i \ b\i)" ``` immler@54780 ` 252` ``` and "box a b \ {} \ (\i\Basis. a\i < b\i)" ``` immler@54780 ` 253` ``` unfolding interval_eq_empty[of a b] by fastforce+ ``` immler@54780 ` 254` immler@54780 ` 255` ```lemma interval_sing: ``` immler@54780 ` 256` ``` fixes a :: "'a::ordered_euclidean_space" ``` immler@54780 ` 257` ``` shows "{a .. a} = {a}" ``` immler@54780 ` 258` ``` and "box a a = {}" ``` immler@54780 ` 259` ``` unfolding set_eq_iff mem_interval eq_iff [symmetric] ``` immler@54780 ` 260` ``` by (auto intro: euclidean_eqI simp: ex_in_conv) ``` immler@54780 ` 261` immler@54780 ` 262` ```lemma subset_interval_imp: ``` immler@54780 ` 263` ``` fixes a :: "'a::ordered_euclidean_space" ``` immler@54780 ` 264` ``` shows "(\i\Basis. a\i \ c\i \ d\i \ b\i) \ {c .. d} \ {a .. b}" ``` immler@54780 ` 265` ``` and "(\i\Basis. a\i < c\i \ d\i < b\i) \ {c .. d} \ box a b" ``` immler@54780 ` 266` ``` and "(\i\Basis. a\i \ c\i \ d\i \ b\i) \ box c d \ {a .. b}" ``` immler@54780 ` 267` ``` and "(\i\Basis. a\i \ c\i \ d\i \ b\i) \ box c d \ box a b" ``` immler@54780 ` 268` ``` unfolding subset_eq[unfolded Ball_def] unfolding mem_interval ``` immler@54780 ` 269` ``` by (best intro: order_trans less_le_trans le_less_trans less_imp_le)+ ``` immler@54780 ` 270` immler@54780 ` 271` ```lemma interval_open_subset_closed: ``` immler@54780 ` 272` ``` fixes a :: "'a::ordered_euclidean_space" ``` immler@54780 ` 273` ``` shows "box a b \ {a .. b}" ``` immler@54780 ` 274` ``` unfolding subset_eq [unfolded Ball_def] mem_interval ``` immler@54780 ` 275` ``` by (fast intro: less_imp_le) ``` immler@54780 ` 276` immler@54780 ` 277` ```lemma subset_interval: ``` immler@54780 ` 278` ``` fixes a :: "'a::ordered_euclidean_space" ``` immler@54780 ` 279` ``` shows "{c .. d} \ {a .. b} \ (\i\Basis. c\i \ d\i) --> (\i\Basis. a\i \ c\i \ d\i \ b\i)" (is ?th1) ``` immler@54780 ` 280` ``` and "{c .. d} \ box a b \ (\i\Basis. c\i \ d\i) --> (\i\Basis. a\i < c\i \ d\i < b\i)" (is ?th2) ``` immler@54780 ` 281` ``` and "box c d \ {a .. b} \ (\i\Basis. c\i < d\i) --> (\i\Basis. a\i \ c\i \ d\i \ b\i)" (is ?th3) ``` immler@54780 ` 282` ``` and "box c d \ box a b \ (\i\Basis. c\i < d\i) --> (\i\Basis. a\i \ c\i \ d\i \ b\i)" (is ?th4) ``` immler@54780 ` 283` ```proof - ``` immler@54780 ` 284` ``` show ?th1 ``` immler@54780 ` 285` ``` unfolding subset_eq and Ball_def and mem_interval ``` immler@54780 ` 286` ``` by (auto intro: order_trans) ``` immler@54780 ` 287` ``` show ?th2 ``` immler@54780 ` 288` ``` unfolding subset_eq and Ball_def and mem_interval ``` immler@54780 ` 289` ``` by (auto intro: le_less_trans less_le_trans order_trans less_imp_le) ``` immler@54780 ` 290` ``` { ``` immler@54780 ` 291` ``` assume as: "box c d \ {a .. b}" "\i\Basis. c\i < d\i" ``` immler@54780 ` 292` ``` then have "box c d \ {}" ``` immler@54780 ` 293` ``` unfolding interval_eq_empty by auto ``` immler@54780 ` 294` ``` fix i :: 'a ``` immler@54780 ` 295` ``` assume i: "i \ Basis" ``` immler@54780 ` 296` ``` (** TODO combine the following two parts as done in the HOL_light version. **) ``` immler@54780 ` 297` ``` { ``` immler@54780 ` 298` ``` let ?x = "(\j\Basis. (if j=i then ((min (a\j) (d\j))+c\j)/2 else (c\j+d\j)/2) *\<^sub>R j)::'a" ``` immler@54780 ` 299` ``` assume as2: "a\i > c\i" ``` immler@54780 ` 300` ``` { ``` immler@54780 ` 301` ``` fix j :: 'a ``` immler@54780 ` 302` ``` assume j: "j \ Basis" ``` immler@54780 ` 303` ``` then have "c \ j < ?x \ j \ ?x \ j < d \ j" ``` immler@54780 ` 304` ``` apply (cases "j = i") ``` immler@54780 ` 305` ``` using as(2)[THEN bspec[where x=j]] i ``` immler@54780 ` 306` ``` apply (auto simp add: as2) ``` immler@54780 ` 307` ``` done ``` immler@54780 ` 308` ``` } ``` immler@54780 ` 309` ``` then have "?x\box c d" ``` immler@54780 ` 310` ``` using i unfolding mem_interval by auto ``` immler@54780 ` 311` ``` moreover ``` immler@54780 ` 312` ``` have "?x \ {a .. b}" ``` immler@54780 ` 313` ``` unfolding mem_interval ``` immler@54780 ` 314` ``` apply auto ``` immler@54780 ` 315` ``` apply (rule_tac x=i in bexI) ``` immler@54780 ` 316` ``` using as(2)[THEN bspec[where x=i]] and as2 i ``` immler@54780 ` 317` ``` apply auto ``` immler@54780 ` 318` ``` done ``` immler@54780 ` 319` ``` ultimately have False using as by auto ``` immler@54780 ` 320` ``` } ``` immler@54780 ` 321` ``` then have "a\i \ c\i" by (rule ccontr) auto ``` immler@54780 ` 322` ``` moreover ``` immler@54780 ` 323` ``` { ``` immler@54780 ` 324` ``` let ?x = "(\j\Basis. (if j=i then ((max (b\j) (c\j))+d\j)/2 else (c\j+d\j)/2) *\<^sub>R j)::'a" ``` immler@54780 ` 325` ``` assume as2: "b\i < d\i" ``` immler@54780 ` 326` ``` { ``` immler@54780 ` 327` ``` fix j :: 'a ``` immler@54780 ` 328` ``` assume "j\Basis" ``` immler@54780 ` 329` ``` then have "d \ j > ?x \ j \ ?x \ j > c \ j" ``` immler@54780 ` 330` ``` apply (cases "j = i") ``` immler@54780 ` 331` ``` using as(2)[THEN bspec[where x=j]] ``` immler@54780 ` 332` ``` apply (auto simp add: as2) ``` immler@54780 ` 333` ``` done ``` immler@54780 ` 334` ``` } ``` immler@54780 ` 335` ``` then have "?x\box c d" ``` immler@54780 ` 336` ``` unfolding mem_interval by auto ``` immler@54780 ` 337` ``` moreover ``` immler@54780 ` 338` ``` have "?x\{a .. b}" ``` immler@54780 ` 339` ``` unfolding mem_interval ``` immler@54780 ` 340` ``` apply auto ``` immler@54780 ` 341` ``` apply (rule_tac x=i in bexI) ``` immler@54780 ` 342` ``` using as(2)[THEN bspec[where x=i]] and as2 using i ``` immler@54780 ` 343` ``` apply auto ``` immler@54780 ` 344` ``` done ``` immler@54780 ` 345` ``` ultimately have False using as by auto ``` immler@54780 ` 346` ``` } ``` immler@54780 ` 347` ``` then have "b\i \ d\i" by (rule ccontr) auto ``` immler@54780 ` 348` ``` ultimately ``` immler@54780 ` 349` ``` have "a\i \ c\i \ d\i \ b\i" by auto ``` immler@54780 ` 350` ``` } note part1 = this ``` immler@54780 ` 351` ``` show ?th3 ``` immler@54780 ` 352` ``` unfolding subset_eq and Ball_def and mem_interval ``` immler@54780 ` 353` ``` apply (rule, rule, rule, rule) ``` immler@54780 ` 354` ``` apply (rule part1) ``` immler@54780 ` 355` ``` unfolding subset_eq and Ball_def and mem_interval ``` immler@54780 ` 356` ``` prefer 4 ``` immler@54780 ` 357` ``` apply auto ``` immler@54780 ` 358` ``` apply (erule_tac x=xa in allE, erule_tac x=xa in allE, fastforce)+ ``` immler@54780 ` 359` ``` done ``` immler@54780 ` 360` ``` { ``` immler@54780 ` 361` ``` assume as: "box c d \ box a b" "\i\Basis. c\i < d\i" ``` immler@54780 ` 362` ``` fix i :: 'a ``` immler@54780 ` 363` ``` assume i:"i\Basis" ``` immler@54780 ` 364` ``` from as(1) have "box c d \ {a..b}" ``` immler@54780 ` 365` ``` using interval_open_subset_closed[of a b] by auto ``` immler@54780 ` 366` ``` then have "a\i \ c\i \ d\i \ b\i" ``` immler@54780 ` 367` ``` using part1 and as(2) using i by auto ``` immler@54780 ` 368` ``` } note * = this ``` immler@54780 ` 369` ``` show ?th4 ``` immler@54780 ` 370` ``` unfolding subset_eq and Ball_def and mem_interval ``` immler@54780 ` 371` ``` apply (rule, rule, rule, rule) ``` immler@54780 ` 372` ``` apply (rule *) ``` immler@54780 ` 373` ``` unfolding subset_eq and Ball_def and mem_interval ``` immler@54780 ` 374` ``` prefer 4 ``` immler@54780 ` 375` ``` apply auto ``` immler@54780 ` 376` ``` apply (erule_tac x=xa in allE, simp)+ ``` immler@54780 ` 377` ``` done ``` immler@54780 ` 378` ```qed ``` immler@54780 ` 379` immler@54780 ` 380` ```lemma inter_interval: ``` immler@54780 ` 381` ``` fixes a :: "'a::ordered_euclidean_space" ``` immler@54780 ` 382` ``` shows "{a .. b} \ {c .. d} = ``` immler@54780 ` 383` ``` {(\i\Basis. max (a\i) (c\i) *\<^sub>R i) .. (\i\Basis. min (b\i) (d\i) *\<^sub>R i)}" ``` immler@54780 ` 384` ``` unfolding set_eq_iff and Int_iff and mem_interval ``` immler@54780 ` 385` ``` by auto ``` immler@54780 ` 386` immler@54780 ` 387` ```lemma disjoint_interval: ``` immler@54780 ` 388` ``` fixes a::"'a::ordered_euclidean_space" ``` immler@54780 ` 389` ``` shows "{a .. b} \ {c .. d} = {} \ (\i\Basis. (b\i < a\i \ d\i < c\i \ b\i < c\i \ d\i < a\i))" (is ?th1) ``` immler@54780 ` 390` ``` and "{a .. b} \ box c d = {} \ (\i\Basis. (b\i < a\i \ d\i \ c\i \ b\i \ c\i \ d\i \ a\i))" (is ?th2) ``` immler@54780 ` 391` ``` and "box a b \ {c .. d} = {} \ (\i\Basis. (b\i \ a\i \ d\i < c\i \ b\i \ c\i \ d\i \ a\i))" (is ?th3) ``` immler@54780 ` 392` ``` and "box a b \ box c d = {} \ (\i\Basis. (b\i \ a\i \ d\i \ c\i \ b\i \ c\i \ d\i \ a\i))" (is ?th4) ``` immler@54780 ` 393` ```proof - ``` immler@54780 ` 394` ``` let ?z = "(\i\Basis. (((max (a\i) (c\i)) + (min (b\i) (d\i))) / 2) *\<^sub>R i)::'a" ``` immler@54780 ` 395` ``` have **: "\P Q. (\i :: 'a. i \ Basis \ Q ?z i \ P i) \ ``` immler@54780 ` 396` ``` (\i x :: 'a. i \ Basis \ P i \ Q x i) \ (\x. \i\Basis. Q x i) \ (\i\Basis. P i)" ``` immler@54780 ` 397` ``` by blast ``` immler@54780 ` 398` ``` note * = set_eq_iff Int_iff empty_iff mem_interval ball_conj_distrib[symmetric] eq_False ball_simps(10) ``` immler@54780 ` 399` ``` show ?th1 unfolding * by (intro **) auto ``` immler@54780 ` 400` ``` show ?th2 unfolding * by (intro **) auto ``` immler@54780 ` 401` ``` show ?th3 unfolding * by (intro **) auto ``` immler@54780 ` 402` ``` show ?th4 unfolding * by (intro **) auto ``` immler@54780 ` 403` ```qed ``` immler@54780 ` 404` immler@54780 ` 405` ```(* Moved interval_open_subset_closed a bit upwards *) ``` immler@54780 ` 406` immler@54780 ` 407` ```lemma open_interval[intro]: ``` immler@54780 ` 408` ``` fixes a b :: "'a::ordered_euclidean_space" ``` immler@54780 ` 409` ``` shows "open (box a b)" ``` immler@54780 ` 410` ```proof - ``` immler@54780 ` 411` ``` have "open (\i\Basis. (\x. x\i) -` {a\i<..i})" ``` immler@54780 ` 412` ``` by (intro open_INT finite_lessThan ballI continuous_open_vimage allI ``` immler@54780 ` 413` ``` linear_continuous_at open_real_greaterThanLessThan finite_Basis bounded_linear_inner_left) ``` immler@54780 ` 414` ``` also have "(\i\Basis. (\x. x\i) -` {a\i<..i}) = box a b" ``` immler@54780 ` 415` ``` by (auto simp add: interval) ``` immler@54780 ` 416` ``` finally show "open (box a b)" . ``` immler@54780 ` 417` ```qed ``` immler@54780 ` 418` immler@54780 ` 419` ```lemma closed_interval[intro]: ``` immler@54780 ` 420` ``` fixes a b :: "'a::ordered_euclidean_space" ``` immler@54780 ` 421` ``` shows "closed {a .. b}" ``` immler@54780 ` 422` ```proof - ``` immler@54780 ` 423` ``` have "closed (\i\Basis. (\x. x\i) -` {a\i .. b\i})" ``` immler@54780 ` 424` ``` by (intro closed_INT ballI continuous_closed_vimage allI ``` immler@54780 ` 425` ``` linear_continuous_at closed_real_atLeastAtMost finite_Basis bounded_linear_inner_left) ``` immler@54780 ` 426` ``` also have "(\i\Basis. (\x. x\i) -` {a\i .. b\i}) = {a .. b}" ``` immler@54780 ` 427` ``` by (auto simp add: eucl_le [where 'a='a]) ``` immler@54780 ` 428` ``` finally show "closed {a .. b}" . ``` immler@54780 ` 429` ```qed ``` immler@54780 ` 430` immler@54780 ` 431` ```lemma interior_closed_interval [intro]: ``` immler@54780 ` 432` ``` fixes a b :: "'a::ordered_euclidean_space" ``` immler@54780 ` 433` ``` shows "interior {a..b} = box a b" (is "?L = ?R") ``` immler@54780 ` 434` ```proof(rule subset_antisym) ``` immler@54780 ` 435` ``` show "?R \ ?L" ``` immler@54780 ` 436` ``` using interval_open_subset_closed open_interval ``` immler@54780 ` 437` ``` by (rule interior_maximal) ``` immler@54780 ` 438` ``` { ``` immler@54780 ` 439` ``` fix x ``` immler@54780 ` 440` ``` assume "x \ interior {a..b}" ``` immler@54780 ` 441` ``` then obtain s where s: "open s" "x \ s" "s \ {a..b}" .. ``` immler@54780 ` 442` ``` then obtain e where "e>0" and e:"\x'. dist x' x < e \ x' \ {a..b}" ``` immler@54780 ` 443` ``` unfolding open_dist and subset_eq by auto ``` immler@54780 ` 444` ``` { ``` immler@54780 ` 445` ``` fix i :: 'a ``` immler@54780 ` 446` ``` assume i: "i \ Basis" ``` immler@54780 ` 447` ``` have "dist (x - (e / 2) *\<^sub>R i) x < e" ``` immler@54780 ` 448` ``` and "dist (x + (e / 2) *\<^sub>R i) x < e" ``` immler@54780 ` 449` ``` unfolding dist_norm ``` immler@54780 ` 450` ``` apply auto ``` immler@54780 ` 451` ``` unfolding norm_minus_cancel ``` immler@54780 ` 452` ``` using norm_Basis[OF i] `e>0` ``` immler@54780 ` 453` ``` apply auto ``` immler@54780 ` 454` ``` done ``` immler@54780 ` 455` ``` then have "a \ i \ (x - (e / 2) *\<^sub>R i) \ i" and "(x + (e / 2) *\<^sub>R i) \ i \ b \ i" ``` immler@54780 ` 456` ``` using e[THEN spec[where x="x - (e/2) *\<^sub>R i"]] ``` immler@54780 ` 457` ``` and e[THEN spec[where x="x + (e/2) *\<^sub>R i"]] ``` immler@54780 ` 458` ``` unfolding mem_interval ``` immler@54780 ` 459` ``` using i ``` immler@54780 ` 460` ``` by blast+ ``` immler@54780 ` 461` ``` then have "a \ i < x \ i" and "x \ i < b \ i" ``` immler@54780 ` 462` ``` using `e>0` i ``` immler@54780 ` 463` ``` by (auto simp: inner_diff_left inner_Basis inner_add_left) ``` immler@54780 ` 464` ``` } ``` immler@54780 ` 465` ``` then have "x \ box a b" ``` immler@54780 ` 466` ``` unfolding mem_interval by auto ``` immler@54780 ` 467` ``` } ``` immler@54780 ` 468` ``` then show "?L \ ?R" .. ``` immler@54780 ` 469` ```qed ``` immler@54780 ` 470` immler@54780 ` 471` ```lemma bounded_closed_interval: ``` immler@54780 ` 472` ``` fixes a :: "'a::ordered_euclidean_space" ``` immler@54780 ` 473` ``` shows "bounded {a .. b}" ``` immler@54780 ` 474` ```proof - ``` immler@54780 ` 475` ``` let ?b = "\i\Basis. \a\i\ + \b\i\" ``` immler@54780 ` 476` ``` { ``` immler@54780 ` 477` ``` fix x :: "'a" ``` immler@54780 ` 478` ``` assume x: "\i\Basis. a \ i \ x \ i \ x \ i \ b \ i" ``` immler@54780 ` 479` ``` { ``` immler@54780 ` 480` ``` fix i :: 'a ``` immler@54780 ` 481` ``` assume "i \ Basis" ``` immler@54780 ` 482` ``` then have "\x\i\ \ \a\i\ + \b\i\" ``` immler@54780 ` 483` ``` using x[THEN bspec[where x=i]] by auto ``` immler@54780 ` 484` ``` } ``` immler@54780 ` 485` ``` then have "(\i\Basis. \x \ i\) \ ?b" ``` immler@54780 ` 486` ``` apply - ``` immler@54780 ` 487` ``` apply (rule setsum_mono) ``` immler@54780 ` 488` ``` apply auto ``` immler@54780 ` 489` ``` done ``` immler@54780 ` 490` ``` then have "norm x \ ?b" ``` immler@54780 ` 491` ``` using norm_le_l1[of x] by auto ``` immler@54780 ` 492` ``` } ``` immler@54780 ` 493` ``` then show ?thesis ``` immler@54780 ` 494` ``` unfolding interval and bounded_iff by auto ``` immler@54780 ` 495` ```qed ``` immler@54780 ` 496` immler@54780 ` 497` ```lemma bounded_interval: ``` immler@54780 ` 498` ``` fixes a :: "'a::ordered_euclidean_space" ``` immler@54780 ` 499` ``` shows "bounded {a .. b} \ bounded (box a b)" ``` immler@54780 ` 500` ``` using bounded_closed_interval[of a b] ``` immler@54780 ` 501` ``` using interval_open_subset_closed[of a b] ``` immler@54780 ` 502` ``` using bounded_subset[of "{a..b}" "box a b"] ``` immler@54780 ` 503` ``` by simp ``` immler@54780 ` 504` immler@54780 ` 505` ```lemma not_interval_univ: ``` immler@54780 ` 506` ``` fixes a :: "'a::ordered_euclidean_space" ``` immler@54780 ` 507` ``` shows "{a .. b} \ UNIV \ box a b \ UNIV" ``` immler@54780 ` 508` ``` using bounded_interval[of a b] by auto ``` immler@54780 ` 509` immler@54780 ` 510` ```lemma compact_interval: ``` immler@54780 ` 511` ``` fixes a :: "'a::ordered_euclidean_space" ``` immler@54780 ` 512` ``` shows "compact {a .. b}" ``` immler@54780 ` 513` ``` using bounded_closed_imp_seq_compact[of "{a..b}"] using bounded_interval[of a b] ``` immler@54780 ` 514` ``` by (auto simp: compact_eq_seq_compact_metric) ``` immler@54780 ` 515` immler@54780 ` 516` ```lemma open_interval_midpoint: ``` immler@54780 ` 517` ``` fixes a :: "'a::ordered_euclidean_space" ``` immler@54780 ` 518` ``` assumes "box a b \ {}" ``` immler@54780 ` 519` ``` shows "((1/2) *\<^sub>R (a + b)) \ box a b" ``` immler@54780 ` 520` ```proof - ``` immler@54780 ` 521` ``` { ``` immler@54780 ` 522` ``` fix i :: 'a ``` immler@54780 ` 523` ``` assume "i \ Basis" ``` immler@54780 ` 524` ``` then have "a \ i < ((1 / 2) *\<^sub>R (a + b)) \ i \ ((1 / 2) *\<^sub>R (a + b)) \ i < b \ i" ``` immler@54780 ` 525` ``` using assms[unfolded interval_ne_empty, THEN bspec[where x=i]] by (auto simp: inner_add_left) ``` immler@54780 ` 526` ``` } ``` immler@54780 ` 527` ``` then show ?thesis unfolding mem_interval by auto ``` immler@54780 ` 528` ```qed ``` immler@54780 ` 529` immler@54780 ` 530` ```lemma open_closed_interval_convex: ``` immler@54780 ` 531` ``` fixes x :: "'a::ordered_euclidean_space" ``` immler@54780 ` 532` ``` assumes x: "x \ box a b" ``` immler@54780 ` 533` ``` and y: "y \ {a .. b}" ``` immler@54780 ` 534` ``` and e: "0 < e" "e \ 1" ``` immler@54780 ` 535` ``` shows "(e *\<^sub>R x + (1 - e) *\<^sub>R y) \ box a b" ``` immler@54780 ` 536` ```proof - ``` immler@54780 ` 537` ``` { ``` immler@54780 ` 538` ``` fix i :: 'a ``` immler@54780 ` 539` ``` assume i: "i \ Basis" ``` immler@54780 ` 540` ``` have "a \ i = e * (a \ i) + (1 - e) * (a \ i)" ``` immler@54780 ` 541` ``` unfolding left_diff_distrib by simp ``` immler@54780 ` 542` ``` also have "\ < e * (x \ i) + (1 - e) * (y \ i)" ``` immler@54780 ` 543` ``` apply (rule add_less_le_mono) ``` immler@54780 ` 544` ``` using e unfolding mult_less_cancel_left and mult_le_cancel_left ``` immler@54780 ` 545` ``` apply simp_all ``` immler@54780 ` 546` ``` using x unfolding mem_interval using i ``` immler@54780 ` 547` ``` apply simp ``` immler@54780 ` 548` ``` using y unfolding mem_interval using i ``` immler@54780 ` 549` ``` apply simp ``` immler@54780 ` 550` ``` done ``` immler@54780 ` 551` ``` finally have "a \ i < (e *\<^sub>R x + (1 - e) *\<^sub>R y) \ i" ``` immler@54780 ` 552` ``` unfolding inner_simps by auto ``` immler@54780 ` 553` ``` moreover ``` immler@54780 ` 554` ``` { ``` immler@54780 ` 555` ``` have "b \ i = e * (b\i) + (1 - e) * (b\i)" ``` immler@54780 ` 556` ``` unfolding left_diff_distrib by simp ``` immler@54780 ` 557` ``` also have "\ > e * (x \ i) + (1 - e) * (y \ i)" ``` immler@54780 ` 558` ``` apply (rule add_less_le_mono) ``` immler@54780 ` 559` ``` using e unfolding mult_less_cancel_left and mult_le_cancel_left ``` immler@54780 ` 560` ``` apply simp_all ``` immler@54780 ` 561` ``` using x ``` immler@54780 ` 562` ``` unfolding mem_interval ``` immler@54780 ` 563` ``` using i ``` immler@54780 ` 564` ``` apply simp ``` immler@54780 ` 565` ``` using y ``` immler@54780 ` 566` ``` unfolding mem_interval ``` immler@54780 ` 567` ``` using i ``` immler@54780 ` 568` ``` apply simp ``` immler@54780 ` 569` ``` done ``` immler@54780 ` 570` ``` finally have "(e *\<^sub>R x + (1 - e) *\<^sub>R y) \ i < b \ i" ``` immler@54780 ` 571` ``` unfolding inner_simps by auto ``` immler@54780 ` 572` ``` } ``` immler@54780 ` 573` ``` ultimately have "a \ i < (e *\<^sub>R x + (1 - e) *\<^sub>R y) \ i \ (e *\<^sub>R x + (1 - e) *\<^sub>R y) \ i < b \ i" ``` immler@54780 ` 574` ``` by auto ``` immler@54780 ` 575` ``` } ``` immler@54780 ` 576` ``` then show ?thesis ``` immler@54780 ` 577` ``` unfolding mem_interval by auto ``` immler@54780 ` 578` ```qed ``` immler@54780 ` 579` immler@54780 ` 580` ```notation ``` immler@54780 ` 581` ``` eucl_less (infix " {}" ``` immler@54780 ` 586` ``` shows "closure (box a b) = {a .. b}" ``` immler@54780 ` 587` ```proof - ``` immler@54780 ` 588` ``` have ab: "a {a .. b}" ``` immler@54780 ` 594` ``` def f \ "\n::nat. x + (inverse (real n + 1)) *\<^sub>R (?c - x)" ``` immler@54780 ` 595` ``` { ``` immler@54780 ` 596` ``` fix n ``` immler@54780 ` 597` ``` assume fn: "f n a f n = x" and xc: "x \ ?c" ``` immler@54780 ` 598` ``` have *: "0 < inverse (real n + 1)" "inverse (real n + 1) \ 1" ``` immler@54780 ` 599` ``` unfolding inverse_le_1_iff by auto ``` immler@54780 ` 600` ``` have "(inverse (real n + 1)) *\<^sub>R ((1 / 2) *\<^sub>R (a + b)) + (1 - inverse (real n + 1)) *\<^sub>R x = ``` immler@54780 ` 601` ``` x + (inverse (real n + 1)) *\<^sub>R (((1 / 2) *\<^sub>R (a + b)) - x)" ``` immler@54780 ` 602` ``` by (auto simp add: algebra_simps) ``` immler@54780 ` 603` ``` then have "f n (f ---> x) sequentially" ``` immler@54780 ` 612` ``` { ``` immler@54780 ` 613` ``` fix e :: real ``` immler@54780 ` 614` ``` assume "e > 0" ``` immler@54780 ` 615` ``` then have "\N::nat. inverse (real (N + 1)) < e" ``` immler@54780 ` 616` ``` using real_arch_inv[of e] ``` immler@54780 ` 617` ``` apply (auto simp add: Suc_pred') ``` immler@54780 ` 618` ``` apply (rule_tac x="n - 1" in exI) ``` immler@54780 ` 619` ``` apply auto ``` immler@54780 ` 620` ``` done ``` immler@54780 ` 621` ``` then obtain N :: nat where "inverse (real (N + 1)) < e" ``` immler@54780 ` 622` ``` by auto ``` immler@54780 ` 623` ``` then have "\n\N. inverse (real n + 1) < e" ``` immler@54780 ` 624` ``` apply auto ``` immler@54780 ` 625` ``` apply (metis Suc_le_mono le_SucE less_imp_inverse_less nat_le_real_less order_less_trans ``` immler@54780 ` 626` ``` real_of_nat_Suc real_of_nat_Suc_gt_zero) ``` immler@54780 ` 627` ``` done ``` immler@54780 ` 628` ``` then have "\N::nat. \n\N. inverse (real n + 1) < e" by auto ``` immler@54780 ` 629` ``` } ``` immler@54780 ` 630` ``` then have "((\n. inverse (real n + 1)) ---> 0) sequentially" ``` immler@54780 ` 631` ``` unfolding LIMSEQ_def by(auto simp add: dist_norm) ``` immler@54780 ` 632` ``` then have "(f ---> x) sequentially" ``` immler@54780 ` 633` ``` unfolding f_def ``` immler@54780 ` 634` ``` using tendsto_add[OF tendsto_const, of "\n::nat. (inverse (real n + 1)) *\<^sub>R ((1 / 2) *\<^sub>R (a + b) - x)" 0 sequentially x] ``` immler@54780 ` 635` ``` using tendsto_scaleR [OF _ tendsto_const, of "\n::nat. inverse (real n + 1)" 0 sequentially "((1 / 2) *\<^sub>R (a + b) - x)"] ``` immler@54780 ` 636` ``` by auto ``` immler@54780 ` 637` ``` } ``` immler@54780 ` 638` ``` ultimately have "x \ closure (box a b)" ``` immler@54780 ` 639` ``` using as and open_interval_midpoint[OF assms] ``` immler@54780 ` 640` ``` unfolding closure_def ``` immler@54780 ` 641` ``` unfolding islimpt_sequential ``` immler@54780 ` 642` ``` by (cases "x=?c") (auto simp: in_box_eucl_less) ``` immler@54780 ` 643` ``` } ``` immler@54780 ` 644` ``` then show ?thesis ``` immler@54780 ` 645` ``` using closure_minimal[OF interval_open_subset_closed closed_interval, of a b] by blast ``` immler@54780 ` 646` ```qed ``` immler@54780 ` 647` immler@54780 ` 648` ```lemma bounded_subset_open_interval_symmetric: ``` immler@54780 ` 649` ``` fixes s::"('a::ordered_euclidean_space) set" ``` immler@54780 ` 650` ``` assumes "bounded s" ``` immler@54780 ` 651` ``` shows "\a. s \ box (-a) a" ``` immler@54780 ` 652` ```proof - ``` immler@54780 ` 653` ``` obtain b where "b>0" and b: "\x\s. norm x \ b" ``` immler@54780 ` 654` ``` using assms[unfolded bounded_pos] by auto ``` immler@54780 ` 655` ``` def a \ "(\i\Basis. (b + 1) *\<^sub>R i)::'a" ``` immler@54780 ` 656` ``` { ``` immler@54780 ` 657` ``` fix x ``` immler@54780 ` 658` ``` assume "x \ s" ``` immler@54780 ` 659` ``` fix i :: 'a ``` immler@54780 ` 660` ``` assume i: "i \ Basis" ``` immler@54780 ` 661` ``` then have "(-a)\i < x\i" and "x\i < a\i" ``` immler@54780 ` 662` ``` using b[THEN bspec[where x=x], OF `x\s`] ``` immler@54780 ` 663` ``` using Basis_le_norm[OF i, of x] ``` immler@54780 ` 664` ``` unfolding inner_simps and a_def ``` immler@54780 ` 665` ``` by auto ``` immler@54780 ` 666` ``` } ``` immler@54780 ` 667` ``` then show ?thesis ``` immler@54780 ` 668` ``` by (auto intro: exI[where x=a] simp add: interval) ``` immler@54780 ` 669` ```qed ``` immler@54780 ` 670` immler@54780 ` 671` ```lemma bounded_subset_open_interval: ``` immler@54780 ` 672` ``` fixes s :: "('a::ordered_euclidean_space) set" ``` immler@54780 ` 673` ``` shows "bounded s \ (\a b. s \ box a b)" ``` immler@54780 ` 674` ``` by (auto dest!: bounded_subset_open_interval_symmetric) ``` immler@54780 ` 675` immler@54780 ` 676` ```lemma bounded_subset_closed_interval_symmetric: ``` immler@54780 ` 677` ``` fixes s :: "('a::ordered_euclidean_space) set" ``` immler@54780 ` 678` ``` assumes "bounded s" ``` immler@54780 ` 679` ``` shows "\a. s \ {-a .. a}" ``` immler@54780 ` 680` ```proof - ``` immler@54780 ` 681` ``` obtain a where "s \ box (-a) a" ``` immler@54780 ` 682` ``` using bounded_subset_open_interval_symmetric[OF assms] by auto ``` immler@54780 ` 683` ``` then show ?thesis ``` immler@54780 ` 684` ``` using interval_open_subset_closed[of "-a" a] by auto ``` immler@54780 ` 685` ```qed ``` immler@54780 ` 686` immler@54780 ` 687` ```lemma bounded_subset_closed_interval: ``` immler@54780 ` 688` ``` fixes s :: "('a::ordered_euclidean_space) set" ``` immler@54780 ` 689` ``` shows "bounded s \ \a b. s \ {a .. b}" ``` immler@54780 ` 690` ``` using bounded_subset_closed_interval_symmetric[of s] by auto ``` immler@54780 ` 691` immler@54780 ` 692` ```lemma frontier_closed_interval: ``` immler@54780 ` 693` ``` fixes a b :: "'a::ordered_euclidean_space" ``` immler@54780 ` 694` ``` shows "frontier {a .. b} = {a .. b} - box a b" ``` immler@54780 ` 695` ``` unfolding frontier_def unfolding interior_closed_interval and closure_closed[OF closed_interval] .. ``` immler@54780 ` 696` immler@54780 ` 697` ```lemma frontier_open_interval: ``` immler@54780 ` 698` ``` fixes a b :: "'a::ordered_euclidean_space" ``` immler@54780 ` 699` ``` shows "frontier (box a b) = (if box a b = {} then {} else {a .. b} - box a b)" ``` immler@54780 ` 700` ```proof (cases "box a b = {}") ``` immler@54780 ` 701` ``` case True ``` immler@54780 ` 702` ``` then show ?thesis ``` immler@54780 ` 703` ``` using frontier_empty by auto ``` immler@54780 ` 704` ```next ``` immler@54780 ` 705` ``` case False ``` immler@54780 ` 706` ``` then show ?thesis ``` immler@54780 ` 707` ``` unfolding frontier_def and closure_open_interval[OF False] and interior_open[OF open_interval] ``` immler@54780 ` 708` ``` by auto ``` immler@54780 ` 709` ```qed ``` immler@54780 ` 710` immler@54780 ` 711` ```lemma inter_interval_mixed_eq_empty: ``` immler@54780 ` 712` ``` fixes a :: "'a::ordered_euclidean_space" ``` immler@54780 ` 713` ``` assumes "box c d \ {}" ``` immler@54780 ` 714` ``` shows "box a b \ {c .. d} = {} \ box a b \ box c d = {}" ``` immler@54780 ` 715` ``` unfolding closure_open_interval[OF assms, symmetric] ``` immler@54780 ` 716` ``` unfolding open_inter_closure_eq_empty[OF open_interval] .. ``` immler@54780 ` 717` immler@54781 ` 718` ```lemma diameter_closed_interval: ``` immler@54781 ` 719` ``` fixes a b::"'a::ordered_euclidean_space" ``` immler@54781 ` 720` ``` shows "a \ b \ diameter {a..b} = dist a b" ``` haftmann@56166 ` 721` ``` by (force simp add: diameter_def SUP_def simp del: Sup_image_eq intro!: cSup_eq_maximum setL2_mono ``` immler@54781 ` 722` ``` simp: euclidean_dist_l2[where 'a='a] eucl_le[where 'a='a] dist_norm) ``` immler@54781 ` 723` immler@54780 ` 724` ```text {* Intervals in general, including infinite and mixtures of open and closed. *} ``` immler@54780 ` 725` immler@54780 ` 726` ```definition "is_interval (s::('a::euclidean_space) set) \ ``` immler@54780 ` 727` ``` (\a\s. \b\s. \x. (\i\Basis. ((a\i \ x\i \ x\i \ b\i) \ (b\i \ x\i \ x\i \ a\i))) \ x \ s)" ``` immler@54780 ` 728` immler@54780 ` 729` ```lemma is_interval_interval: "is_interval {a .. b::'a::ordered_euclidean_space}" (is ?th1) ``` immler@54780 ` 730` ``` "is_interval (box a b)" (is ?th2) proof - ``` immler@54780 ` 731` ``` show ?th1 ?th2 unfolding is_interval_def mem_interval Ball_def atLeastAtMost_iff ``` immler@54780 ` 732` ``` by(meson order_trans le_less_trans less_le_trans less_trans)+ qed ``` immler@54780 ` 733` immler@54780 ` 734` ```lemma is_interval_empty: ``` immler@54780 ` 735` ``` "is_interval {}" ``` immler@54780 ` 736` ``` unfolding is_interval_def ``` immler@54780 ` 737` ``` by simp ``` immler@54780 ` 738` immler@54780 ` 739` ```lemma is_interval_univ: ``` immler@54780 ` 740` ``` "is_interval UNIV" ``` immler@54780 ` 741` ``` unfolding is_interval_def ``` immler@54780 ` 742` ``` by simp ``` immler@54780 ` 743` immler@54781 ` 744` ```lemma mem_is_intervalI: ``` immler@54781 ` 745` ``` assumes "is_interval s" ``` immler@54781 ` 746` ``` assumes "a \ s" "b \ s" ``` immler@54781 ` 747` ``` assumes "\i. i \ Basis \ a \ i \ x \ i \ x \ i \ b \ i \ b \ i \ x \ i \ x \ i \ a \ i" ``` immler@54781 ` 748` ``` shows "x \ s" ``` immler@54781 ` 749` ``` by (rule assms(1)[simplified is_interval_def, rule_format, OF assms(2,3,4)]) ``` immler@54781 ` 750` immler@54781 ` 751` ```lemma interval_subst: ``` immler@54781 ` 752` ``` fixes S::"'a::ordered_euclidean_space set" ``` immler@54781 ` 753` ``` assumes "is_interval S" ``` immler@54781 ` 754` ``` assumes "x \ S" "y j \ S" ``` immler@54781 ` 755` ``` assumes "j \ Basis" ``` immler@54781 ` 756` ``` shows "(\i\Basis. (if i = j then y i \ i else x \ i) *\<^sub>R i) \ S" ``` immler@54781 ` 757` ``` by (rule mem_is_intervalI[OF assms(1,2)]) (auto simp: assms) ``` immler@54781 ` 758` immler@54781 ` 759` ```lemma mem_interval_componentwiseI: ``` immler@54781 ` 760` ``` fixes S::"'a::ordered_euclidean_space set" ``` immler@54781 ` 761` ``` assumes "is_interval S" ``` immler@54781 ` 762` ``` assumes "\i. i \ Basis \ x \ i \ ((\x. x \ i) ` S)" ``` immler@54781 ` 763` ``` shows "x \ S" ``` immler@54781 ` 764` ```proof - ``` immler@54781 ` 765` ``` from assms have "\i \ Basis. \s \ S. x \ i = s \ i" ``` immler@54781 ` 766` ``` by auto ``` immler@54781 ` 767` ``` with finite_Basis obtain s and bs::"'a list" where ``` immler@54781 ` 768` ``` s: "\i. i \ Basis \ x \ i = s i \ i" "\i. i \ Basis \ s i \ S" and ``` immler@54781 ` 769` ``` bs: "set bs = Basis" "distinct bs" ``` immler@54781 ` 770` ``` by (metis finite_distinct_list) ``` immler@54781 ` 771` ``` from nonempty_Basis s obtain j where j: "j \ Basis" "s j \ S" by blast ``` blanchet@55413 ` 772` ``` def y \ "rec_list ``` immler@54781 ` 773` ``` (s j) ``` immler@54781 ` 774` ``` (\j _ Y. (\i\Basis. (if i = j then s i \ i else Y \ i) *\<^sub>R i))" ``` immler@54781 ` 775` ``` have "x = (\i\Basis. (if i \ set bs then s i \ i else s j \ i) *\<^sub>R i)" ``` immler@54781 ` 776` ``` using bs by (auto simp add: s(1)[symmetric] euclidean_representation) ``` immler@54781 ` 777` ``` also have [symmetric]: "y bs = \" ``` immler@54781 ` 778` ``` using bs(2) bs(1)[THEN equalityD1] ``` immler@54781 ` 779` ``` by (induct bs) (auto simp: y_def euclidean_representation intro!: euclidean_eqI[where 'a='a]) ``` immler@54781 ` 780` ``` also have "y bs \ S" ``` immler@54781 ` 781` ``` using bs(1)[THEN equalityD1] ``` immler@54781 ` 782` ``` apply (induct bs) ``` immler@54781 ` 783` ``` apply (auto simp: y_def j) ``` immler@54781 ` 784` ``` apply (rule interval_subst[OF assms(1)]) ``` immler@54781 ` 785` ``` apply (auto simp: s) ``` immler@54781 ` 786` ``` done ``` immler@54781 ` 787` ``` finally show ?thesis . ``` immler@54781 ` 788` ```qed ``` immler@54781 ` 789` immler@54780 ` 790` ```text{* Instantiation for intervals on @{text ordered_euclidean_space} *} ``` immler@54780 ` 791` immler@54780 ` 792` ```lemma eucl_lessThan_eq_halfspaces: ``` immler@54780 ` 793` ``` fixes a :: "'a\ordered_euclidean_space" ``` immler@54780 ` 794` ``` shows "{x. x i\Basis. {x. x \ i < a \ i})" ``` immler@54780 ` 795` ``` by (auto simp: eucl_less_def) ``` immler@54780 ` 796` immler@54780 ` 797` ```lemma eucl_greaterThan_eq_halfspaces: ``` immler@54780 ` 798` ``` fixes a :: "'a\ordered_euclidean_space" ``` immler@54780 ` 799` ``` shows "{x. a i\Basis. {x. a \ i < x \ i})" ``` immler@54780 ` 800` ``` by (auto simp: eucl_less_def) ``` immler@54780 ` 801` immler@54780 ` 802` ```lemma eucl_atMost_eq_halfspaces: ``` immler@54780 ` 803` ``` fixes a :: "'a\ordered_euclidean_space" ``` immler@54780 ` 804` ``` shows "{.. a} = (\i\Basis. {x. x \ i \ a \ i})" ``` immler@54780 ` 805` ``` by (auto simp: eucl_le[where 'a='a]) ``` immler@54780 ` 806` immler@54780 ` 807` ```lemma eucl_atLeast_eq_halfspaces: ``` immler@54780 ` 808` ``` fixes a :: "'a\ordered_euclidean_space" ``` immler@54780 ` 809` ``` shows "{a ..} = (\i\Basis. {x. a \ i \ x \ i})" ``` immler@54780 ` 810` ``` by (auto simp: eucl_le[where 'a='a]) ``` immler@54780 ` 811` immler@54780 ` 812` ```lemma open_eucl_lessThan[simp, intro]: ``` immler@54780 ` 813` ``` fixes a :: "'a\ordered_euclidean_space" ``` immler@54780 ` 814` ``` shows "open {x. x ordered_euclidean_space" ``` immler@54780 ` 819` ``` shows "open {x. a ordered_euclidean_space" ``` immler@54780 ` 824` ``` shows "closed {.. a}" ``` immler@54780 ` 825` ``` unfolding eucl_atMost_eq_halfspaces ``` immler@54780 ` 826` ``` by (simp add: closed_INT closed_Collect_le) ``` immler@54780 ` 827` immler@54780 ` 828` ```lemma closed_eucl_atLeast[simp, intro]: ``` immler@54780 ` 829` ``` fixes a :: "'a\ordered_euclidean_space" ``` immler@54780 ` 830` ``` shows "closed {a ..}" ``` immler@54780 ` 831` ``` unfolding eucl_atLeast_eq_halfspaces ``` immler@54780 ` 832` ``` by (simp add: closed_INT closed_Collect_le) ``` immler@54780 ` 833` immler@54780 ` 834` immler@54780 ` 835` ```lemma image_affinity_interval: fixes m::real ``` immler@54780 ` 836` ``` fixes a b c :: "'a::ordered_euclidean_space" ``` immler@54780 ` 837` ``` shows "(\x. m *\<^sub>R x + c) ` {a .. b} = ``` immler@54780 ` 838` ``` (if {a .. b} = {} then {} ``` immler@54780 ` 839` ``` else (if 0 \ m then {m *\<^sub>R a + c .. m *\<^sub>R b + c} ``` immler@54780 ` 840` ``` else {m *\<^sub>R b + c .. m *\<^sub>R a + c}))" ``` immler@54780 ` 841` ```proof (cases "m = 0") ``` immler@54780 ` 842` ``` case True ``` immler@54780 ` 843` ``` { ``` immler@54780 ` 844` ``` fix x ``` immler@54780 ` 845` ``` assume "x \ c" "c \ x" ``` immler@54780 ` 846` ``` then have "x = c" ``` immler@54780 ` 847` ``` unfolding eucl_le[where 'a='a] ``` immler@54780 ` 848` ``` apply - ``` immler@54780 ` 849` ``` apply (subst euclidean_eq_iff) ``` immler@54780 ` 850` ``` apply (auto intro: order_antisym) ``` immler@54780 ` 851` ``` done ``` immler@54780 ` 852` ``` } ``` immler@54780 ` 853` ``` moreover have "c \ {m *\<^sub>R a + c..m *\<^sub>R b + c}" ``` immler@54780 ` 854` ``` unfolding True by (auto simp add: eucl_le[where 'a='a]) ``` immler@54780 ` 855` ``` ultimately show ?thesis using True by auto ``` immler@54780 ` 856` ```next ``` immler@54780 ` 857` ``` case False ``` immler@54780 ` 858` ``` { ``` immler@54780 ` 859` ``` fix y ``` immler@54780 ` 860` ``` assume "a \ y" "y \ b" "m > 0" ``` immler@54780 ` 861` ``` then have "m *\<^sub>R a + c \ m *\<^sub>R y + c" and "m *\<^sub>R y + c \ m *\<^sub>R b + c" ``` immler@54780 ` 862` ``` unfolding eucl_le[where 'a='a] by (auto simp: inner_distrib) ``` immler@54780 ` 863` ``` } ``` immler@54780 ` 864` ``` moreover ``` immler@54780 ` 865` ``` { ``` immler@54780 ` 866` ``` fix y ``` immler@54780 ` 867` ``` assume "a \ y" "y \ b" "m < 0" ``` immler@54780 ` 868` ``` then have "m *\<^sub>R b + c \ m *\<^sub>R y + c" and "m *\<^sub>R y + c \ m *\<^sub>R a + c" ``` immler@54780 ` 869` ``` unfolding eucl_le[where 'a='a] by (auto simp add: mult_left_mono_neg inner_distrib) ``` immler@54780 ` 870` ``` } ``` immler@54780 ` 871` ``` moreover ``` immler@54780 ` 872` ``` { ``` immler@54780 ` 873` ``` fix y ``` immler@54780 ` 874` ``` assume "m > 0" and "m *\<^sub>R a + c \ y" and "y \ m *\<^sub>R b + c" ``` immler@54780 ` 875` ``` then have "y \ (\x. m *\<^sub>R x + c) ` {a..b}" ``` immler@54780 ` 876` ``` unfolding image_iff Bex_def mem_interval eucl_le[where 'a='a] ``` immler@54780 ` 877` ``` apply (intro exI[where x="(1 / m) *\<^sub>R (y - c)"]) ``` immler@54780 ` 878` ``` apply (auto simp add: pos_le_divide_eq pos_divide_le_eq mult_commute diff_le_iff inner_distrib inner_diff_left) ``` immler@54780 ` 879` ``` done ``` immler@54780 ` 880` ``` } ``` immler@54780 ` 881` ``` moreover ``` immler@54780 ` 882` ``` { ``` immler@54780 ` 883` ``` fix y ``` immler@54780 ` 884` ``` assume "m *\<^sub>R b + c \ y" "y \ m *\<^sub>R a + c" "m < 0" ``` immler@54780 ` 885` ``` then have "y \ (\x. m *\<^sub>R x + c) ` {a..b}" ``` immler@54780 ` 886` ``` unfolding image_iff Bex_def mem_interval eucl_le[where 'a='a] ``` immler@54780 ` 887` ``` apply (intro exI[where x="(1 / m) *\<^sub>R (y - c)"]) ``` immler@54780 ` 888` ``` apply (auto simp add: neg_le_divide_eq neg_divide_le_eq mult_commute diff_le_iff inner_distrib inner_diff_left) ``` immler@54780 ` 889` ``` done ``` immler@54780 ` 890` ``` } ``` immler@54780 ` 891` ``` ultimately show ?thesis using False by auto ``` immler@54780 ` 892` ```qed ``` immler@54780 ` 893` immler@54780 ` 894` ```lemma image_smult_interval:"(\x. m *\<^sub>R (x::_::ordered_euclidean_space)) ` {a..b} = ``` immler@54780 ` 895` ``` (if {a..b} = {} then {} else if 0 \ m then {m *\<^sub>R a..m *\<^sub>R b} else {m *\<^sub>R b..m *\<^sub>R a})" ``` immler@54780 ` 896` ``` using image_affinity_interval[of m 0 a b] by auto ``` immler@54780 ` 897` immler@54780 ` 898` ```no_notation ``` immler@54780 ` 899` ``` eucl_less (infix "