src/HOL/Analysis/Ordered_Euclidean_Space.thy
 author wenzelm Mon Mar 25 17:21:26 2019 +0100 (2 months ago) changeset 69981 3dced198b9ec parent 69939 812ce526da33 child 70097 4005298550a6 permissions -rw-r--r--
more strict AFP properties;
 lp15@69939 ` 1` ```section \Ordered Euclidean Space\ ``` nipkow@69631 ` 2` immler@54780 ` 3` ```theory Ordered_Euclidean_Space ``` immler@54780 ` 4` ```imports ``` immler@56189 ` 5` ``` Cartesian_Euclidean_Space ``` wenzelm@66453 ` 6` ``` "HOL-Library.Product_Order" ``` immler@54780 ` 7` ```begin ``` immler@54780 ` 8` ak2110@69730 ` 9` ```text \An ordering on euclidean spaces that will allow us to talk about intervals\ ``` immler@54780 ` 10` immler@54780 ` 11` ```class ordered_euclidean_space = ord + inf + sup + abs + Inf + Sup + euclidean_space + ``` immler@54780 ` 12` ``` assumes eucl_le: "x \ y \ (\i\Basis. x \ i \ y \ i)" ``` immler@54780 ` 13` ``` assumes eucl_less_le_not_le: "x < y \ x \ y \ \ y \ x" ``` immler@54780 ` 14` ``` assumes eucl_inf: "inf x y = (\i\Basis. inf (x \ i) (y \ i) *\<^sub>R i)" ``` immler@54780 ` 15` ``` assumes eucl_sup: "sup x y = (\i\Basis. sup (x \ i) (y \ i) *\<^sub>R i)" ``` haftmann@69260 ` 16` ``` assumes eucl_Inf: "Inf X = (\i\Basis. (INF x\X. x \ i) *\<^sub>R i)" ``` haftmann@69260 ` 17` ``` assumes eucl_Sup: "Sup X = (\i\Basis. (SUP x\X. x \ i) *\<^sub>R i)" ``` wenzelm@61945 ` 18` ``` assumes eucl_abs: "\x\ = (\i\Basis. \x \ i\ *\<^sub>R i)" ``` immler@54780 ` 19` ```begin ``` immler@54780 ` 20` immler@54780 ` 21` ```subclass order ``` wenzelm@61169 ` 22` ``` by standard ``` immler@54780 ` 23` ``` (auto simp: eucl_le eucl_less_le_not_le intro!: euclidean_eqI antisym intro: order.trans) ``` immler@54780 ` 24` immler@54780 ` 25` ```subclass ordered_ab_group_add_abs ``` wenzelm@61169 ` 26` ``` by standard (auto simp: eucl_le inner_add_left eucl_abs abs_leI) ``` immler@54780 ` 27` immler@54780 ` 28` ```subclass ordered_real_vector ``` wenzelm@61169 ` 29` ``` by standard (auto simp: eucl_le intro!: mult_left_mono mult_right_mono) ``` immler@54780 ` 30` immler@54780 ` 31` ```subclass lattice ``` wenzelm@61169 ` 32` ``` by standard (auto simp: eucl_inf eucl_sup eucl_le) ``` immler@54780 ` 33` immler@54780 ` 34` ```subclass distrib_lattice ``` wenzelm@61169 ` 35` ``` by standard (auto simp: eucl_inf eucl_sup sup_inf_distrib1 intro!: euclidean_eqI) ``` immler@54780 ` 36` immler@54780 ` 37` ```subclass conditionally_complete_lattice ``` ak2110@69730 ` 38` ```proof ``` immler@54780 ` 39` ``` fix z::'a and X::"'a set" ``` immler@54780 ` 40` ``` assume "X \ {}" ``` immler@54780 ` 41` ``` hence "\i. (\x. x \ i) ` X \ {}" by simp ``` immler@54780 ` 42` ``` thus "(\x. x \ X \ z \ x) \ z \ Inf X" "(\x. x \ X \ x \ z) \ Sup X \ z" ``` haftmann@62343 ` 43` ``` by (auto simp: eucl_Inf eucl_Sup eucl_le ``` immler@54780 ` 44` ``` intro!: cInf_greatest cSup_least) ``` immler@54780 ` 45` ```qed (force intro!: cInf_lower cSup_upper ``` immler@54780 ` 46` ``` simp: bdd_below_def bdd_above_def preorder_class.bdd_below_def preorder_class.bdd_above_def ``` haftmann@62343 ` 47` ``` eucl_Inf eucl_Sup eucl_le)+ ``` immler@54780 ` 48` ak2110@69730 ` 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)" ``` nipkow@64267 ` 51` ``` by (simp_all add: eucl_inf eucl_sup inner_sum_left inner_Basis if_distrib comm_monoid_add_class.sum.delta ``` immler@54780 ` 52` ``` cong: if_cong) ``` immler@54780 ` 53` ak2110@69730 ` 54` ```lemma inner_Basis_INF_left: "i \ Basis \ (INF x\X. f x) \ i = (INF x\X. f x \ i)" ``` haftmann@69260 ` 55` ``` and inner_Basis_SUP_left: "i \ Basis \ (SUP x\X. f x) \ i = (SUP x\X. f x \ i)" ``` haftmann@69861 ` 56` ``` using eucl_Sup [of "f ` X"] eucl_Inf [of "f ` X"] by (simp_all add: image_comp) ``` immler@54780 ` 57` ak2110@69730 ` 58` ```lemma abs_inner: "i \ Basis \ \x\ \ i = \x \ i\" ``` immler@54780 ` 59` ``` by (auto simp: eucl_abs) ``` immler@54780 ` 60` ak2110@69730 ` 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` ak2110@69730 ` 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] ``` nipkow@64267 ` 70` ``` by (auto intro!: ordered_comm_monoid_add_class.sum_mono mult_right_mono simp: eucl_le) ``` immler@54780 ` 71` ak2110@69730 ` 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` ak2110@69730 ` 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` ak2110@69730 ` 81` ```lemma Basis_nonneg[intro, simp]: "i \ Basis \ 0 \ i" ``` immler@54780 ` 82` ``` by (auto simp: eucl_le inner_Basis) ``` immler@54780 ` 83` ak2110@69730 ` 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 ``` nipkow@64267 ` 91` ``` unfolding eucl_Sup euclidean_representation_sum ``` haftmann@62343 ` 92` ``` by (auto intro!: conditionally_complete_lattice_class.cSup_eq_maximum) ``` immler@54781 ` 93` ak2110@69730 ` 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 ``` nipkow@64267 ` 100` ``` unfolding eucl_Inf euclidean_representation_sum ``` haftmann@62343 ` 101` ``` by (auto intro!: conditionally_complete_lattice_class.cInf_eq_minimum) ``` immler@54781 ` 102` immler@54780 ` 103` ```end ``` immler@54780 ` 104` ak2110@69730 ` 105` ```proposition compact_attains_Inf_componentwise: ``` immler@54781 ` 106` ``` fixes b::"'a::ordered_euclidean_space" ``` immler@54781 ` 107` ``` assumes "b \ Basis" assumes "X \ {}" "compact X" ``` immler@54781 ` 108` ``` obtains x where "x \ X" "x \ b = Inf X \ b" "\y. y \ X \ x \ b \ y \ b" ``` ak2110@69730 ` 109` ```proof atomize_elim ``` immler@54781 ` 110` ``` let ?proj = "(\x. x \ b) ` X" ``` immler@54781 ` 111` ``` from assms have "compact ?proj" "?proj \ {}" ``` hoelzl@56371 ` 112` ``` by (auto intro!: compact_continuous_image continuous_intros) ``` immler@54781 ` 113` ``` from compact_attains_inf[OF this] ``` immler@54781 ` 114` ``` obtain s x ``` immler@54781 ` 115` ``` where s: "s\(\x. x \ b) ` X" "\t. t\(\x. x \ b) ` X \ s \ t" ``` immler@54781 ` 116` ``` and x: "x \ X" "s = x \ b" "\y. y \ X \ x \ b \ y \ b" ``` immler@54781 ` 117` ``` by auto ``` immler@54781 ` 118` ``` hence "Inf ?proj = x \ b" ``` haftmann@62343 ` 119` ``` by (auto intro!: conditionally_complete_lattice_class.cInf_eq_minimum) ``` immler@54781 ` 120` ``` hence "x \ b = Inf X \ b" ``` nipkow@64267 ` 121` ``` by (auto simp: eucl_Inf inner_sum_left inner_Basis if_distrib \b \ Basis\ sum.delta ``` haftmann@56166 ` 122` ``` cong: if_cong) ``` immler@54781 ` 123` ``` with x show "\x. x \ X \ x \ b = Inf X \ b \ (\y. y \ X \ x \ b \ y \ b)" by blast ``` immler@54781 ` 124` ```qed ``` immler@54781 ` 125` ak2110@69730 ` 126` ```proposition ``` immler@54781 ` 127` ``` compact_attains_Sup_componentwise: ``` immler@54781 ` 128` ``` fixes b::"'a::ordered_euclidean_space" ``` immler@54781 ` 129` ``` assumes "b \ Basis" assumes "X \ {}" "compact X" ``` immler@54781 ` 130` ``` obtains x where "x \ X" "x \ b = Sup X \ b" "\y. y \ X \ y \ b \ x \ b" ``` ak2110@69730 ` 131` ```proof atomize_elim ``` immler@54781 ` 132` ``` let ?proj = "(\x. x \ b) ` X" ``` immler@54781 ` 133` ``` from assms have "compact ?proj" "?proj \ {}" ``` hoelzl@56371 ` 134` ``` by (auto intro!: compact_continuous_image continuous_intros) ``` immler@54781 ` 135` ``` from compact_attains_sup[OF this] ``` immler@54781 ` 136` ``` obtain s x ``` immler@54781 ` 137` ``` where s: "s\(\x. x \ b) ` X" "\t. t\(\x. x \ b) ` X \ t \ s" ``` immler@54781 ` 138` ``` and x: "x \ X" "s = x \ b" "\y. y \ X \ y \ b \ x \ b" ``` immler@54781 ` 139` ``` by auto ``` immler@54781 ` 140` ``` hence "Sup ?proj = x \ b" ``` haftmann@62343 ` 141` ``` by (auto intro!: cSup_eq_maximum) ``` immler@54781 ` 142` ``` hence "x \ b = Sup X \ b" ``` nipkow@64267 ` 143` ``` by (auto simp: eucl_Sup[where 'a='a] inner_sum_left inner_Basis if_distrib \b \ Basis\ sum.delta ``` haftmann@62343 ` 144` ``` cong: if_cong) ``` immler@54781 ` 145` ``` with x show "\x. x \ X \ x \ b = Sup X \ b \ (\y. y \ X \ y \ b \ x \ b)" by blast ``` immler@54781 ` 146` ```qed ``` immler@54781 ` 147` ak2110@69730 ` 148` ```lemma (in order) atLeastatMost_empty'[simp]: ``` nipkow@69508 ` 149` ``` "(\ a \ b) \ {a..b} = {}" ``` immler@54780 ` 150` ``` by (auto) ``` immler@54780 ` 151` immler@54780 ` 152` ```instance real :: ordered_euclidean_space ``` haftmann@62343 ` 153` ``` by standard auto ``` immler@54780 ` 154` ak2110@69730 ` 155` ```lemma in_Basis_prod_iff: ``` immler@54780 ` 156` ``` fixes i::"'a::euclidean_space*'b::euclidean_space" ``` immler@54780 ` 157` ``` shows "i \ Basis \ fst i = 0 \ snd i \ Basis \ snd i = 0 \ fst i \ Basis" ``` immler@54780 ` 158` ``` by (cases i) (auto simp: Basis_prod_def) ``` immler@54780 ` 159` ak2110@69730 ` 160` ```instantiation%unimportant prod :: (abs, abs) abs ``` immler@54780 ` 161` ```begin ``` immler@54780 ` 162` wenzelm@61945 ` 163` ```definition "\x\ = (\fst x\, \snd x\)" ``` immler@54780 ` 164` wenzelm@61945 ` 165` ```instance .. ``` wenzelm@61945 ` 166` immler@54780 ` 167` ```end ``` immler@54780 ` 168` immler@54780 ` 169` ```instance prod :: (ordered_euclidean_space, ordered_euclidean_space) ordered_euclidean_space ``` wenzelm@61169 ` 170` ``` by standard ``` nipkow@64267 ` 171` ``` (auto intro!: add_mono simp add: euclidean_representation_sum' Ball_def inner_prod_def ``` immler@54780 ` 172` ``` in_Basis_prod_iff inner_Basis_inf_left inner_Basis_sup_left inner_Basis_INF_left Inf_prod_def ``` immler@54780 ` 173` ``` inner_Basis_SUP_left Sup_prod_def less_prod_def less_eq_prod_def eucl_le[where 'a='a] ``` immler@54780 ` 174` ``` eucl_le[where 'a='b] abs_prod_def abs_inner) ``` immler@54780 ` 175` wenzelm@61808 ` 176` ```text\Instantiation for intervals on \ordered_euclidean_space\\ ``` immler@56188 ` 177` ak2110@69730 ` 178` ```proposition ``` wenzelm@61076 ` 179` ``` fixes a :: "'a::ordered_euclidean_space" ``` immler@56188 ` 180` ``` shows cbox_interval: "cbox a b = {a..b}" ``` immler@56188 ` 181` ``` and interval_cbox: "{a..b} = cbox a b" ``` immler@56188 ` 182` ``` and eucl_le_atMost: "{x. \i\Basis. x \ i <= a \ i} = {..a}" ``` immler@56188 ` 183` ``` and eucl_le_atLeast: "{x. \i\Basis. a \ i <= x \ i} = {a..}" ``` ak2110@69730 ` 184` ``` by (auto simp: eucl_le[where 'a='a] eucl_less_def box_def cbox_def) ``` immler@56188 ` 185` ak2110@69730 ` 186` ```lemma vec_nth_real_1_iff_cbox [simp]: ``` lp15@67981 ` 187` ``` fixes a b :: real ``` lp15@67981 ` 188` ``` shows "(\x::real^1. x \$ 1) ` S = {a..b} \ S = cbox (vec a) (vec b)" ``` lp15@67981 ` 189` ``` by (metis interval_cbox vec_nth_1_iff_cbox) ``` lp15@67981 ` 190` ak2110@69730 ` 191` ```lemma closed_eucl_atLeastAtMost[simp, intro]: ``` wenzelm@61076 ` 192` ``` fixes a :: "'a::ordered_euclidean_space" ``` immler@56188 ` 193` ``` shows "closed {a..b}" ``` immler@56188 ` 194` ``` by (simp add: cbox_interval[symmetric] closed_cbox) ``` immler@56188 ` 195` ak2110@69730 ` 196` ```lemma closed_eucl_atMost[simp, intro]: ``` wenzelm@61076 ` 197` ``` fixes a :: "'a::ordered_euclidean_space" ``` immler@56188 ` 198` ``` shows "closed {..a}" ``` lp15@66827 ` 199` ``` by (simp add: closed_interval_left eucl_le_atMost[symmetric]) ``` immler@56188 ` 200` ak2110@69730 ` 201` ```lemma closed_eucl_atLeast[simp, intro]: ``` wenzelm@61076 ` 202` ``` fixes a :: "'a::ordered_euclidean_space" ``` immler@56188 ` 203` ``` shows "closed {a..}" ``` lp15@66827 ` 204` ``` by (simp add: closed_interval_right eucl_le_atLeast[symmetric]) ``` immler@56188 ` 205` ak2110@69730 ` 206` ```lemma bounded_closed_interval [simp]: ``` immler@56189 ` 207` ``` fixes a :: "'a::ordered_euclidean_space" ``` immler@56189 ` 208` ``` shows "bounded {a .. b}" ``` immler@56189 ` 209` ``` using bounded_cbox[of a b] ``` immler@56189 ` 210` ``` by (metis interval_cbox) ``` immler@56189 ` 211` ak2110@69730 ` 212` ```lemma convex_closed_interval [simp]: ``` immler@56190 ` 213` ``` fixes a :: "'a::ordered_euclidean_space" ``` immler@56190 ` 214` ``` shows "convex {a .. b}" ``` immler@56190 ` 215` ``` using convex_box[of a b] ``` immler@56190 ` 216` ``` by (metis interval_cbox) ``` immler@56190 ` 217` ak2110@69730 ` 218` ```lemma image_smult_interval:"(\x. m *\<^sub>R (x::_::ordered_euclidean_space)) ` {a .. b} = ``` immler@56188 ` 219` ``` (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@56188 ` 220` ``` using image_smult_cbox[of m a b] ``` immler@56188 ` 221` ``` by (simp add: cbox_interval) ``` immler@54780 ` 222` ak2110@69730 ` 223` ```lemma [simp]: ``` immler@67685 ` 224` ``` fixes a b::"'a::ordered_euclidean_space" and r s::real ``` immler@67685 ` 225` ``` shows is_interval_io: "is_interval {.. {}" and "box c d \ {}" ``` lp15@62620 ` 277` ``` shows "(cbox a b) homeomorphic (cbox c d)" ``` lp15@62620 ` 278` ```apply (rule homeomorphic_convex_compact) ``` lp15@62620 ` 279` ```using assms apply auto ``` lp15@62620 ` 280` ```done ``` lp15@62620 ` 281` ak2110@69730 ` 282` ```lemma homeomorphic_closed_intervals_real: ``` lp15@62620 ` 283` ``` fixes a::real and b and c::real and d ``` lp15@62620 ` 284` ``` assumes "a (\Basis::'a::ordered_euclidean_space)" ``` nipkow@64267 ` 292` ``` by (auto intro: sum_nonneg) ``` immler@56189 ` 293` ak2110@69730 ` 294` ```lemma ``` immler@56190 ` 295` ``` fixes a b::"'a::ordered_euclidean_space" ``` immler@56190 ` 296` ``` shows bdd_above_cbox[intro, simp]: "bdd_above (cbox a b)" ``` immler@56190 ` 297` ``` and bdd_below_cbox[intro, simp]: "bdd_below (cbox a b)" ``` immler@56190 ` 298` ``` and bdd_above_box[intro, simp]: "bdd_above (box a b)" ``` immler@56190 ` 299` ``` and bdd_below_box[intro, simp]: "bdd_below (box a b)" ``` immler@56190 ` 300` ``` unfolding atomize_conj ``` immler@56190 ` 301` ``` by (metis bdd_above_Icc bdd_above_mono bdd_below_Icc bdd_below_mono bounded_box ``` lp15@68120 ` 302` ``` bounded_subset_cbox_symmetric interval_cbox) ``` immler@56190 ` 303` immler@56189 ` 304` ```instantiation vec :: (ordered_euclidean_space, finite) ordered_euclidean_space ``` immler@56189 ` 305` ```begin ``` immler@56189 ` 306` ak2110@68833 ` 307` ```definition%important "inf x y = (\ i. inf (x \$ i) (y \$ i))" ``` ak2110@68833 ` 308` ```definition%important "sup x y = (\ i. sup (x \$ i) (y \$ i))" ``` haftmann@69260 ` 309` ```definition%important "Inf X = (\ i. (INF x\X. x \$ i))" ``` haftmann@69260 ` 310` ```definition%important "Sup X = (\ i. (SUP x\X. x \$ i))" ``` ak2110@68833 ` 311` ```definition%important "\x\ = (\ i. \x \$ i\)" ``` immler@56189 ` 312` immler@56189 ` 313` ```instance ``` wenzelm@61169 ` 314` ``` apply standard ``` nipkow@64267 ` 315` ``` unfolding euclidean_representation_sum' ``` immler@56189 ` 316` ``` apply (auto simp: less_eq_vec_def inf_vec_def sup_vec_def Inf_vec_def Sup_vec_def inner_axis ``` immler@56189 ` 317` ``` Basis_vec_def inner_Basis_inf_left inner_Basis_sup_left inner_Basis_INF_left ``` immler@56189 ` 318` ``` inner_Basis_SUP_left eucl_le[where 'a='a] less_le_not_le abs_vec_def abs_inner) ``` immler@56189 ` 319` ``` done ``` immler@56189 ` 320` immler@54780 ` 321` ```end ``` immler@56189 ` 322` ak2110@69730 ` 323` ```lemma ANR_interval [iff]: ``` lp15@63469 ` 324` ``` fixes a :: "'a::ordered_euclidean_space" ``` lp15@63469 ` 325` ``` shows "ANR{a..b}" ``` lp15@63469 ` 326` ```by (simp add: interval_cbox) ``` lp15@63469 ` 327` ak2110@69730 ` 328` ```lemma ENR_interval [iff]: ``` lp15@63469 ` 329` ``` fixes a :: "'a::ordered_euclidean_space" ``` lp15@63469 ` 330` ``` shows "ENR{a..b}" ``` lp15@63469 ` 331` ``` by (auto simp: interval_cbox) ``` lp15@63469 ` 332` immler@56189 ` 333` ```end ``` immler@56189 ` 334`