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