src/HOL/Analysis/Ordered_Euclidean_Space.thy
 author wenzelm Mon Mar 25 17:21:26 2019 +0100 (3 months ago) changeset 69981 3dced198b9ec parent 69939 812ce526da33 child 70097 4005298550a6 permissions -rw-r--r--
more strict AFP properties;
```     1 section \<open>Ordered Euclidean Space\<close>
```
```     2
```
```     3 theory Ordered_Euclidean_Space
```
```     4 imports
```
```     5   Cartesian_Euclidean_Space
```
```     6   "HOL-Library.Product_Order"
```
```     7 begin
```
```     8
```
```     9 text \<open>An ordering on euclidean spaces that will allow us to talk about intervals\<close>
```
```    10
```
```    11 class ordered_euclidean_space = ord + inf + sup + abs + Inf + Sup + euclidean_space +
```
```    12   assumes eucl_le: "x \<le> y \<longleftrightarrow> (\<forall>i\<in>Basis. x \<bullet> i \<le> y \<bullet> i)"
```
```    13   assumes eucl_less_le_not_le: "x < y \<longleftrightarrow> x \<le> y \<and> \<not> y \<le> x"
```
```    14   assumes eucl_inf: "inf x y = (\<Sum>i\<in>Basis. inf (x \<bullet> i) (y \<bullet> i) *\<^sub>R i)"
```
```    15   assumes eucl_sup: "sup x y = (\<Sum>i\<in>Basis. sup (x \<bullet> i) (y \<bullet> i) *\<^sub>R i)"
```
```    16   assumes eucl_Inf: "Inf X = (\<Sum>i\<in>Basis. (INF x\<in>X. x \<bullet> i) *\<^sub>R i)"
```
```    17   assumes eucl_Sup: "Sup X = (\<Sum>i\<in>Basis. (SUP x\<in>X. x \<bullet> i) *\<^sub>R i)"
```
```    18   assumes eucl_abs: "\<bar>x\<bar> = (\<Sum>i\<in>Basis. \<bar>x \<bullet> i\<bar> *\<^sub>R i)"
```
```    19 begin
```
```    20
```
```    21 subclass order
```
```    22   by standard
```
```    23     (auto simp: eucl_le eucl_less_le_not_le intro!: euclidean_eqI antisym intro: order.trans)
```
```    24
```
```    25 subclass ordered_ab_group_add_abs
```
```    26   by standard (auto simp: eucl_le inner_add_left eucl_abs abs_leI)
```
```    27
```
```    28 subclass ordered_real_vector
```
```    29   by standard (auto simp: eucl_le intro!: mult_left_mono mult_right_mono)
```
```    30
```
```    31 subclass lattice
```
```    32   by standard (auto simp: eucl_inf eucl_sup eucl_le)
```
```    33
```
```    34 subclass distrib_lattice
```
```    35   by standard (auto simp: eucl_inf eucl_sup sup_inf_distrib1 intro!: euclidean_eqI)
```
```    36
```
```    37 subclass conditionally_complete_lattice
```
```    38 proof
```
```    39   fix z::'a and X::"'a set"
```
```    40   assume "X \<noteq> {}"
```
```    41   hence "\<And>i. (\<lambda>x. x \<bullet> i) ` X \<noteq> {}" by simp
```
```    42   thus "(\<And>x. x \<in> X \<Longrightarrow> z \<le> x) \<Longrightarrow> z \<le> Inf X" "(\<And>x. x \<in> X \<Longrightarrow> x \<le> z) \<Longrightarrow> Sup X \<le> z"
```
```    43     by (auto simp: eucl_Inf eucl_Sup eucl_le
```
```    44       intro!: cInf_greatest cSup_least)
```
```    45 qed (force intro!: cInf_lower cSup_upper
```
```    46       simp: bdd_below_def bdd_above_def preorder_class.bdd_below_def preorder_class.bdd_above_def
```
```    47         eucl_Inf eucl_Sup eucl_le)+
```
```    48
```
```    49 lemma inner_Basis_inf_left: "i \<in> Basis \<Longrightarrow> inf x y \<bullet> i = inf (x \<bullet> i) (y \<bullet> i)"
```
```    50   and inner_Basis_sup_left: "i \<in> Basis \<Longrightarrow> sup x y \<bullet> i = sup (x \<bullet> i) (y \<bullet> i)"
```
```    51   by (simp_all add: eucl_inf eucl_sup inner_sum_left inner_Basis if_distrib comm_monoid_add_class.sum.delta
```
```    52       cong: if_cong)
```
```    53
```
```    54 lemma inner_Basis_INF_left: "i \<in> Basis \<Longrightarrow> (INF x\<in>X. f x) \<bullet> i = (INF x\<in>X. f x \<bullet> i)"
```
```    55   and inner_Basis_SUP_left: "i \<in> Basis \<Longrightarrow> (SUP x\<in>X. f x) \<bullet> i = (SUP x\<in>X. f x \<bullet> i)"
```
```    56   using eucl_Sup [of "f ` X"] eucl_Inf [of "f ` X"] by (simp_all add: image_comp)
```
```    57
```
```    58 lemma abs_inner: "i \<in> Basis \<Longrightarrow> \<bar>x\<bar> \<bullet> i = \<bar>x \<bullet> i\<bar>"
```
```    59   by (auto simp: eucl_abs)
```
```    60
```
```    61 lemma
```
```    62   abs_scaleR: "\<bar>a *\<^sub>R b\<bar> = \<bar>a\<bar> *\<^sub>R \<bar>b\<bar>"
```
```    63   by (auto simp: eucl_abs abs_mult intro!: euclidean_eqI)
```
```    64
```
```    65 lemma interval_inner_leI:
```
```    66   assumes "x \<in> {a .. b}" "0 \<le> i"
```
```    67   shows "a\<bullet>i \<le> x\<bullet>i" "x\<bullet>i \<le> b\<bullet>i"
```
```    68   using assms
```
```    69   unfolding euclidean_inner[of a i] euclidean_inner[of x i] euclidean_inner[of b i]
```
```    70   by (auto intro!: ordered_comm_monoid_add_class.sum_mono mult_right_mono simp: eucl_le)
```
```    71
```
```    72 lemma inner_nonneg_nonneg:
```
```    73   shows "0 \<le> a \<Longrightarrow> 0 \<le> b \<Longrightarrow> 0 \<le> a \<bullet> b"
```
```    74   using interval_inner_leI[of a 0 a b]
```
```    75   by auto
```
```    76
```
```    77 lemma inner_Basis_mono:
```
```    78   shows "a \<le> b \<Longrightarrow> c \<in> Basis  \<Longrightarrow> a \<bullet> c \<le> b \<bullet> c"
```
```    79   by (simp add: eucl_le)
```
```    80
```
```    81 lemma Basis_nonneg[intro, simp]: "i \<in> Basis \<Longrightarrow> 0 \<le> i"
```
```    82   by (auto simp: eucl_le inner_Basis)
```
```    83
```
```    84 lemma Sup_eq_maximum_componentwise:
```
```    85   fixes s::"'a set"
```
```    86   assumes i: "\<And>b. b \<in> Basis \<Longrightarrow> X \<bullet> b = i b \<bullet> b"
```
```    87   assumes sup: "\<And>b x. b \<in> Basis \<Longrightarrow> x \<in> s \<Longrightarrow> x \<bullet> b \<le> X \<bullet> b"
```
```    88   assumes i_s: "\<And>b. b \<in> Basis \<Longrightarrow> (i b \<bullet> b) \<in> (\<lambda>x. x \<bullet> b) ` s"
```
```    89   shows "Sup s = X"
```
```    90   using assms
```
```    91   unfolding eucl_Sup euclidean_representation_sum
```
```    92   by (auto intro!: conditionally_complete_lattice_class.cSup_eq_maximum)
```
```    93
```
```    94 lemma Inf_eq_minimum_componentwise:
```
```    95   assumes i: "\<And>b. b \<in> Basis \<Longrightarrow> X \<bullet> b = i b \<bullet> b"
```
```    96   assumes sup: "\<And>b x. b \<in> Basis \<Longrightarrow> x \<in> s \<Longrightarrow> X \<bullet> b \<le> x \<bullet> b"
```
```    97   assumes i_s: "\<And>b. b \<in> Basis \<Longrightarrow> (i b \<bullet> b) \<in> (\<lambda>x. x \<bullet> b) ` s"
```
```    98   shows "Inf s = X"
```
```    99   using assms
```
```   100   unfolding eucl_Inf euclidean_representation_sum
```
```   101   by (auto intro!: conditionally_complete_lattice_class.cInf_eq_minimum)
```
```   102
```
```   103 end
```
```   104
```
```   105 proposition  compact_attains_Inf_componentwise:
```
```   106   fixes b::"'a::ordered_euclidean_space"
```
```   107   assumes "b \<in> Basis" assumes "X \<noteq> {}" "compact X"
```
```   108   obtains x where "x \<in> X" "x \<bullet> b = Inf X \<bullet> b" "\<And>y. y \<in> X \<Longrightarrow> x \<bullet> b \<le> y \<bullet> b"
```
```   109 proof atomize_elim
```
```   110   let ?proj = "(\<lambda>x. x \<bullet> b) ` X"
```
```   111   from assms have "compact ?proj" "?proj \<noteq> {}"
```
```   112     by (auto intro!: compact_continuous_image continuous_intros)
```
```   113   from compact_attains_inf[OF this]
```
```   114   obtain s x
```
```   115     where s: "s\<in>(\<lambda>x. x \<bullet> b) ` X" "\<And>t. t\<in>(\<lambda>x. x \<bullet> b) ` X \<Longrightarrow> s \<le> t"
```
```   116       and x: "x \<in> X" "s = x \<bullet> b" "\<And>y. y \<in> X \<Longrightarrow> x \<bullet> b \<le> y \<bullet> b"
```
```   117     by auto
```
```   118   hence "Inf ?proj = x \<bullet> b"
```
```   119     by (auto intro!: conditionally_complete_lattice_class.cInf_eq_minimum)
```
```   120   hence "x \<bullet> b = Inf X \<bullet> b"
```
```   121     by (auto simp: eucl_Inf inner_sum_left inner_Basis if_distrib \<open>b \<in> Basis\<close> sum.delta
```
```   122       cong: if_cong)
```
```   123   with x show "\<exists>x. x \<in> X \<and> x \<bullet> b = Inf X \<bullet> b \<and> (\<forall>y. y \<in> X \<longrightarrow> x \<bullet> b \<le> y \<bullet> b)" by blast
```
```   124 qed
```
```   125
```
```   126 proposition
```
```   127   compact_attains_Sup_componentwise:
```
```   128   fixes b::"'a::ordered_euclidean_space"
```
```   129   assumes "b \<in> Basis" assumes "X \<noteq> {}" "compact X"
```
```   130   obtains x where "x \<in> X" "x \<bullet> b = Sup X \<bullet> b" "\<And>y. y \<in> X \<Longrightarrow> y \<bullet> b \<le> x \<bullet> b"
```
```   131 proof atomize_elim
```
```   132   let ?proj = "(\<lambda>x. x \<bullet> b) ` X"
```
```   133   from assms have "compact ?proj" "?proj \<noteq> {}"
```
```   134     by (auto intro!: compact_continuous_image continuous_intros)
```
```   135   from compact_attains_sup[OF this]
```
```   136   obtain s x
```
```   137     where s: "s\<in>(\<lambda>x. x \<bullet> b) ` X" "\<And>t. t\<in>(\<lambda>x. x \<bullet> b) ` X \<Longrightarrow> t \<le> s"
```
```   138       and x: "x \<in> X" "s = x \<bullet> b" "\<And>y. y \<in> X \<Longrightarrow> y \<bullet> b \<le> x \<bullet> b"
```
```   139     by auto
```
```   140   hence "Sup ?proj = x \<bullet> b"
```
```   141     by (auto intro!: cSup_eq_maximum)
```
```   142   hence "x \<bullet> b = Sup X \<bullet> b"
```
```   143     by (auto simp: eucl_Sup[where 'a='a] inner_sum_left inner_Basis if_distrib \<open>b \<in> Basis\<close> sum.delta
```
```   144       cong: if_cong)
```
```   145   with x show "\<exists>x. x \<in> X \<and> x \<bullet> b = Sup X \<bullet> b \<and> (\<forall>y. y \<in> X \<longrightarrow> y \<bullet> b \<le> x \<bullet> b)" by blast
```
```   146 qed
```
```   147
```
```   148 lemma (in order) atLeastatMost_empty'[simp]:
```
```   149   "(\<not> a \<le> b) \<Longrightarrow> {a..b} = {}"
```
```   150   by (auto)
```
```   151
```
```   152 instance real :: ordered_euclidean_space
```
```   153   by standard auto
```
```   154
```
```   155 lemma in_Basis_prod_iff:
```
```   156   fixes i::"'a::euclidean_space*'b::euclidean_space"
```
```   157   shows "i \<in> Basis \<longleftrightarrow> fst i = 0 \<and> snd i \<in> Basis \<or> snd i = 0 \<and> fst i \<in> Basis"
```
```   158   by (cases i) (auto simp: Basis_prod_def)
```
```   159
```
```   160 instantiation%unimportant prod :: (abs, abs) abs
```
```   161 begin
```
```   162
```
```   163 definition "\<bar>x\<bar> = (\<bar>fst x\<bar>, \<bar>snd x\<bar>)"
```
```   164
```
```   165 instance ..
```
```   166
```
```   167 end
```
```   168
```
```   169 instance prod :: (ordered_euclidean_space, ordered_euclidean_space) ordered_euclidean_space
```
```   170   by standard
```
```   171     (auto intro!: add_mono simp add: euclidean_representation_sum'  Ball_def inner_prod_def
```
```   172       in_Basis_prod_iff inner_Basis_inf_left inner_Basis_sup_left inner_Basis_INF_left Inf_prod_def
```
```   173       inner_Basis_SUP_left Sup_prod_def less_prod_def less_eq_prod_def eucl_le[where 'a='a]
```
```   174       eucl_le[where 'a='b] abs_prod_def abs_inner)
```
```   175
```
```   176 text\<open>Instantiation for intervals on \<open>ordered_euclidean_space\<close>\<close>
```
```   177
```
```   178 proposition
```
```   179   fixes a :: "'a::ordered_euclidean_space"
```
```   180   shows cbox_interval: "cbox a b = {a..b}"
```
```   181     and interval_cbox: "{a..b} = cbox a b"
```
```   182     and eucl_le_atMost: "{x. \<forall>i\<in>Basis. x \<bullet> i <= a \<bullet> i} = {..a}"
```
```   183     and eucl_le_atLeast: "{x. \<forall>i\<in>Basis. a \<bullet> i <= x \<bullet> i} = {a..}"
```
```   184   by (auto simp: eucl_le[where 'a='a] eucl_less_def box_def cbox_def)
```
```   185
```
```   186 lemma vec_nth_real_1_iff_cbox [simp]:
```
```   187   fixes a b :: real
```
```   188   shows "(\<lambda>x::real^1. x \$ 1) ` S = {a..b} \<longleftrightarrow> S = cbox (vec a) (vec b)"
```
```   189   by (metis interval_cbox vec_nth_1_iff_cbox)
```
```   190
```
```   191 lemma closed_eucl_atLeastAtMost[simp, intro]:
```
```   192   fixes a :: "'a::ordered_euclidean_space"
```
```   193   shows "closed {a..b}"
```
```   194   by (simp add: cbox_interval[symmetric] closed_cbox)
```
```   195
```
```   196 lemma closed_eucl_atMost[simp, intro]:
```
```   197   fixes a :: "'a::ordered_euclidean_space"
```
```   198   shows "closed {..a}"
```
```   199   by (simp add: closed_interval_left eucl_le_atMost[symmetric])
```
```   200
```
```   201 lemma closed_eucl_atLeast[simp, intro]:
```
```   202   fixes a :: "'a::ordered_euclidean_space"
```
```   203   shows "closed {a..}"
```
```   204   by (simp add: closed_interval_right eucl_le_atLeast[symmetric])
```
```   205
```
```   206 lemma bounded_closed_interval [simp]:
```
```   207   fixes a :: "'a::ordered_euclidean_space"
```
```   208   shows "bounded {a .. b}"
```
```   209   using bounded_cbox[of a b]
```
```   210   by (metis interval_cbox)
```
```   211
```
```   212 lemma convex_closed_interval [simp]:
```
```   213   fixes a :: "'a::ordered_euclidean_space"
```
```   214   shows "convex {a .. b}"
```
```   215   using convex_box[of a b]
```
```   216   by (metis interval_cbox)
```
```   217
```
```   218 lemma image_smult_interval:"(\<lambda>x. m *\<^sub>R (x::_::ordered_euclidean_space)) ` {a .. b} =
```
```   219   (if {a .. b} = {} then {} else if 0 \<le> m then {m *\<^sub>R a .. m *\<^sub>R b} else {m *\<^sub>R b .. m *\<^sub>R a})"
```
```   220   using image_smult_cbox[of m a b]
```
```   221   by (simp add: cbox_interval)
```
```   222
```
```   223 lemma [simp]:
```
```   224   fixes a b::"'a::ordered_euclidean_space" and r s::real
```
```   225   shows is_interval_io: "is_interval {..<r}"
```
```   226     and is_interval_ic: "is_interval {..a}"
```
```   227     and is_interval_oi: "is_interval {r<..}"
```
```   228     and is_interval_ci: "is_interval {a..}"
```
```   229     and is_interval_oo: "is_interval {r<..<s}"
```
```   230     and is_interval_oc: "is_interval {r<..s}"
```
```   231     and is_interval_co: "is_interval {r..<s}"
```
```   232     and is_interval_cc: "is_interval {b..a}"
```
```   233   by (force simp: is_interval_def eucl_le[where 'a='a])+
```
```   234
```
```   235 lemma connected_interval [simp]:
```
```   236   fixes a b::"'a::ordered_euclidean_space"
```
```   237   shows "connected {a..b}"
```
```   238   using is_interval_cc is_interval_connected by blast
```
```   239
```
```   240 lemma path_connected_interval [simp]:
```
```   241   fixes a b::"'a::ordered_euclidean_space"
```
```   242   shows "path_connected {a..b}"
```
```   243   using is_interval_cc is_interval_path_connected by blast
```
```   244
```
```   245 lemma path_connected_Ioi[simp]: "path_connected {a<..}" for a :: real
```
```   246   by (simp add: convex_imp_path_connected)
```
```   247
```
```   248 lemma path_connected_Ici[simp]: "path_connected {a..}" for a :: real
```
```   249   by (simp add: convex_imp_path_connected)
```
```   250
```
```   251 lemma path_connected_Iio[simp]: "path_connected {..<a}" for a :: real
```
```   252   by (simp add: convex_imp_path_connected)
```
```   253
```
```   254 lemma path_connected_Iic[simp]: "path_connected {..a}" for a :: real
```
```   255   by (simp add: convex_imp_path_connected)
```
```   256
```
```   257 lemma path_connected_Ioo[simp]: "path_connected {a<..<b}" for a b :: real
```
```   258   by (simp add: convex_imp_path_connected)
```
```   259
```
```   260 lemma path_connected_Ioc[simp]: "path_connected {a<..b}" for a b :: real
```
```   261   by (simp add: convex_imp_path_connected)
```
```   262
```
```   263 lemma path_connected_Ico[simp]: "path_connected {a..<b}" for a b :: real
```
```   264   by (simp add: convex_imp_path_connected)
```
```   265
```
```   266 lemma is_interval_real_ereal_oo: "is_interval (real_of_ereal ` {N<..<M::ereal})"
```
```   267   by (auto simp: real_atLeastGreaterThan_eq)
```
```   268
```
```   269 lemma compact_interval [simp]:
```
```   270   fixes a b::"'a::ordered_euclidean_space"
```
```   271   shows "compact {a .. b}"
```
```   272   by (metis compact_cbox interval_cbox)
```
```   273
```
```   274 lemma homeomorphic_closed_intervals:
```
```   275   fixes a :: "'a::euclidean_space" and b and c :: "'a::euclidean_space" and d
```
```   276   assumes "box a b \<noteq> {}" and "box c d \<noteq> {}"
```
```   277     shows "(cbox a b) homeomorphic (cbox c d)"
```
```   278 apply (rule homeomorphic_convex_compact)
```
```   279 using assms apply auto
```
```   280 done
```
```   281
```
```   282 lemma homeomorphic_closed_intervals_real:
```
```   283   fixes a::real and b and c::real and d
```
```   284   assumes "a<b" and "c<d"
```
```   285   shows "{a..b} homeomorphic {c..d}"
```
```   286   using assms by (auto intro: homeomorphic_convex_compact)
```
```   287
```
```   288 no_notation
```
```   289   eucl_less (infix "<e" 50)
```
```   290
```
```   291 lemma One_nonneg: "0 \<le> (\<Sum>Basis::'a::ordered_euclidean_space)"
```
```   292   by (auto intro: sum_nonneg)
```
```   293
```
```   294 lemma
```
```   295   fixes a b::"'a::ordered_euclidean_space"
```
```   296   shows bdd_above_cbox[intro, simp]: "bdd_above (cbox a b)"
```
```   297     and bdd_below_cbox[intro, simp]: "bdd_below (cbox a b)"
```
```   298     and bdd_above_box[intro, simp]: "bdd_above (box a b)"
```
```   299     and bdd_below_box[intro, simp]: "bdd_below (box a b)"
```
```   300   unfolding atomize_conj
```
```   301   by (metis bdd_above_Icc bdd_above_mono bdd_below_Icc bdd_below_mono bounded_box
```
```   302             bounded_subset_cbox_symmetric interval_cbox)
```
```   303
```
```   304 instantiation vec :: (ordered_euclidean_space, finite) ordered_euclidean_space
```
```   305 begin
```
```   306
```
```   307 definition%important "inf x y = (\<chi> i. inf (x \$ i) (y \$ i))"
```
```   308 definition%important "sup x y = (\<chi> i. sup (x \$ i) (y \$ i))"
```
```   309 definition%important "Inf X = (\<chi> i. (INF x\<in>X. x \$ i))"
```
```   310 definition%important "Sup X = (\<chi> i. (SUP x\<in>X. x \$ i))"
```
```   311 definition%important "\<bar>x\<bar> = (\<chi> i. \<bar>x \$ i\<bar>)"
```
```   312
```
```   313 instance
```
```   314   apply standard
```
```   315   unfolding euclidean_representation_sum'
```
```   316   apply (auto simp: less_eq_vec_def inf_vec_def sup_vec_def Inf_vec_def Sup_vec_def inner_axis
```
```   317     Basis_vec_def inner_Basis_inf_left inner_Basis_sup_left inner_Basis_INF_left
```
```   318     inner_Basis_SUP_left eucl_le[where 'a='a] less_le_not_le abs_vec_def abs_inner)
```
```   319   done
```
```   320
```
```   321 end
```
```   322
```
```   323 lemma ANR_interval [iff]:
```
```   324     fixes a :: "'a::ordered_euclidean_space"
```
```   325     shows "ANR{a..b}"
```
```   326 by (simp add: interval_cbox)
```
```   327
```
```   328 lemma ENR_interval [iff]:
```
```   329     fixes a :: "'a::ordered_euclidean_space"
```
```   330     shows "ENR{a..b}"
```
```   331   by (auto simp: interval_cbox)
```
```   332
```
```   333 end
```
```   334
```