src/HOL/Multivariate_Analysis/Ordered_Euclidean_Space.thy
author haftmann
Sat, 28 Jun 2014 09:16:42 +0200
changeset 57418 6ab1c7cb0b8d
parent 56371 fb9ae0727548
child 60420 884f54e01427
permissions -rw-r--r--
fact consolidation
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
54780
6fae499e0827 summarized notions related to ordered_euclidean_space and intervals in separate theory
immler
parents:
diff changeset
     1
theory Ordered_Euclidean_Space
6fae499e0827 summarized notions related to ordered_euclidean_space and intervals in separate theory
immler
parents:
diff changeset
     2
imports
56189
c4daa97ac57a removed dependencies on theory Ordered_Euclidean_Space
immler
parents: 56188
diff changeset
     3
  Cartesian_Euclidean_Space
54780
6fae499e0827 summarized notions related to ordered_euclidean_space and intervals in separate theory
immler
parents:
diff changeset
     4
  "~~/src/HOL/Library/Product_Order"
6fae499e0827 summarized notions related to ordered_euclidean_space and intervals in separate theory
immler
parents:
diff changeset
     5
begin
6fae499e0827 summarized notions related to ordered_euclidean_space and intervals in separate theory
immler
parents:
diff changeset
     6
6fae499e0827 summarized notions related to ordered_euclidean_space and intervals in separate theory
immler
parents:
diff changeset
     7
subsection {* An ordering on euclidean spaces that will allow us to talk about intervals *}
6fae499e0827 summarized notions related to ordered_euclidean_space and intervals in separate theory
immler
parents:
diff changeset
     8
6fae499e0827 summarized notions related to ordered_euclidean_space and intervals in separate theory
immler
parents:
diff changeset
     9
class ordered_euclidean_space = ord + inf + sup + abs + Inf + Sup + euclidean_space +
6fae499e0827 summarized notions related to ordered_euclidean_space and intervals in separate theory
immler
parents:
diff changeset
    10
  assumes eucl_le: "x \<le> y \<longleftrightarrow> (\<forall>i\<in>Basis. x \<bullet> i \<le> y \<bullet> i)"
6fae499e0827 summarized notions related to ordered_euclidean_space and intervals in separate theory
immler
parents:
diff changeset
    11
  assumes eucl_less_le_not_le: "x < y \<longleftrightarrow> x \<le> y \<and> \<not> y \<le> x"
6fae499e0827 summarized notions related to ordered_euclidean_space and intervals in separate theory
immler
parents:
diff changeset
    12
  assumes eucl_inf: "inf x y = (\<Sum>i\<in>Basis. inf (x \<bullet> i) (y \<bullet> i) *\<^sub>R i)"
6fae499e0827 summarized notions related to ordered_euclidean_space and intervals in separate theory
immler
parents:
diff changeset
    13
  assumes eucl_sup: "sup x y = (\<Sum>i\<in>Basis. sup (x \<bullet> i) (y \<bullet> i) *\<^sub>R i)"
6fae499e0827 summarized notions related to ordered_euclidean_space and intervals in separate theory
immler
parents:
diff changeset
    14
  assumes eucl_Inf: "Inf X = (\<Sum>i\<in>Basis. (INF x:X. x \<bullet> i) *\<^sub>R i)"
6fae499e0827 summarized notions related to ordered_euclidean_space and intervals in separate theory
immler
parents:
diff changeset
    15
  assumes eucl_Sup: "Sup X = (\<Sum>i\<in>Basis. (SUP x:X. x \<bullet> i) *\<^sub>R i)"
6fae499e0827 summarized notions related to ordered_euclidean_space and intervals in separate theory
immler
parents:
diff changeset
    16
  assumes eucl_abs: "abs x = (\<Sum>i\<in>Basis. abs (x \<bullet> i) *\<^sub>R i)"
6fae499e0827 summarized notions related to ordered_euclidean_space and intervals in separate theory
immler
parents:
diff changeset
    17
begin
6fae499e0827 summarized notions related to ordered_euclidean_space and intervals in separate theory
immler
parents:
diff changeset
    18
6fae499e0827 summarized notions related to ordered_euclidean_space and intervals in separate theory
immler
parents:
diff changeset
    19
subclass order
6fae499e0827 summarized notions related to ordered_euclidean_space and intervals in separate theory
immler
parents:
diff changeset
    20
  by default
6fae499e0827 summarized notions related to ordered_euclidean_space and intervals in separate theory
immler
parents:
diff changeset
    21
    (auto simp: eucl_le eucl_less_le_not_le intro!: euclidean_eqI antisym intro: order.trans)
6fae499e0827 summarized notions related to ordered_euclidean_space and intervals in separate theory
immler
parents:
diff changeset
    22
6fae499e0827 summarized notions related to ordered_euclidean_space and intervals in separate theory
immler
parents:
diff changeset
    23
subclass ordered_ab_group_add_abs
6fae499e0827 summarized notions related to ordered_euclidean_space and intervals in separate theory
immler
parents:
diff changeset
    24
  by default (auto simp: eucl_le inner_add_left eucl_abs abs_leI)
6fae499e0827 summarized notions related to ordered_euclidean_space and intervals in separate theory
immler
parents:
diff changeset
    25
6fae499e0827 summarized notions related to ordered_euclidean_space and intervals in separate theory
immler
parents:
diff changeset
    26
subclass ordered_real_vector
6fae499e0827 summarized notions related to ordered_euclidean_space and intervals in separate theory
immler
parents:
diff changeset
    27
  by default (auto simp: eucl_le intro!: mult_left_mono mult_right_mono)
6fae499e0827 summarized notions related to ordered_euclidean_space and intervals in separate theory
immler
parents:
diff changeset
    28
6fae499e0827 summarized notions related to ordered_euclidean_space and intervals in separate theory
immler
parents:
diff changeset
    29
subclass lattice
6fae499e0827 summarized notions related to ordered_euclidean_space and intervals in separate theory
immler
parents:
diff changeset
    30
  by default (auto simp: eucl_inf eucl_sup eucl_le)
6fae499e0827 summarized notions related to ordered_euclidean_space and intervals in separate theory
immler
parents:
diff changeset
    31
6fae499e0827 summarized notions related to ordered_euclidean_space and intervals in separate theory
immler
parents:
diff changeset
    32
subclass distrib_lattice
6fae499e0827 summarized notions related to ordered_euclidean_space and intervals in separate theory
immler
parents:
diff changeset
    33
  by default (auto simp: eucl_inf eucl_sup sup_inf_distrib1 intro!: euclidean_eqI)
6fae499e0827 summarized notions related to ordered_euclidean_space and intervals in separate theory
immler
parents:
diff changeset
    34
6fae499e0827 summarized notions related to ordered_euclidean_space and intervals in separate theory
immler
parents:
diff changeset
    35
subclass conditionally_complete_lattice
6fae499e0827 summarized notions related to ordered_euclidean_space and intervals in separate theory
immler
parents:
diff changeset
    36
proof
6fae499e0827 summarized notions related to ordered_euclidean_space and intervals in separate theory
immler
parents:
diff changeset
    37
  fix z::'a and X::"'a set"
6fae499e0827 summarized notions related to ordered_euclidean_space and intervals in separate theory
immler
parents:
diff changeset
    38
  assume "X \<noteq> {}"
6fae499e0827 summarized notions related to ordered_euclidean_space and intervals in separate theory
immler
parents:
diff changeset
    39
  hence "\<And>i. (\<lambda>x. x \<bullet> i) ` X \<noteq> {}" by simp
6fae499e0827 summarized notions related to ordered_euclidean_space and intervals in separate theory
immler
parents:
diff changeset
    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"
6fae499e0827 summarized notions related to ordered_euclidean_space and intervals in separate theory
immler
parents:
diff changeset
    41
    by (auto simp: eucl_Inf eucl_Sup eucl_le Inf_class.INF_def Sup_class.SUP_def
56166
9a241bc276cd normalising simp rules for compound operators
haftmann
parents: 55413
diff changeset
    42
      simp del: Inf_class.Inf_image_eq Sup_class.Sup_image_eq
54780
6fae499e0827 summarized notions related to ordered_euclidean_space and intervals in separate theory
immler
parents:
diff changeset
    43
      intro!: cInf_greatest cSup_least)
6fae499e0827 summarized notions related to ordered_euclidean_space and intervals in separate theory
immler
parents:
diff changeset
    44
qed (force intro!: cInf_lower cSup_upper
6fae499e0827 summarized notions related to ordered_euclidean_space and intervals in separate theory
immler
parents:
diff changeset
    45
      simp: bdd_below_def bdd_above_def preorder_class.bdd_below_def preorder_class.bdd_above_def
56166
9a241bc276cd normalising simp rules for compound operators
haftmann
parents: 55413
diff changeset
    46
        eucl_Inf eucl_Sup eucl_le Inf_class.INF_def Sup_class.SUP_def
9a241bc276cd normalising simp rules for compound operators
haftmann
parents: 55413
diff changeset
    47
      simp del: Inf_class.Inf_image_eq Sup_class.Sup_image_eq)+
54780
6fae499e0827 summarized notions related to ordered_euclidean_space and intervals in separate theory
immler
parents:
diff changeset
    48
6fae499e0827 summarized notions related to ordered_euclidean_space and intervals in separate theory
immler
parents:
diff changeset
    49
lemma inner_Basis_inf_left: "i \<in> Basis \<Longrightarrow> inf x y \<bullet> i = inf (x \<bullet> i) (y \<bullet> i)"
6fae499e0827 summarized notions related to ordered_euclidean_space and intervals in separate theory
immler
parents:
diff changeset
    50
  and inner_Basis_sup_left: "i \<in> Basis \<Longrightarrow> sup x y \<bullet> i = sup (x \<bullet> i) (y \<bullet> i)"
57418
6ab1c7cb0b8d fact consolidation
haftmann
parents: 56371
diff changeset
    51
  by (simp_all add: eucl_inf eucl_sup inner_setsum_left inner_Basis if_distrib comm_monoid_add_class.setsum.delta
54780
6fae499e0827 summarized notions related to ordered_euclidean_space and intervals in separate theory
immler
parents:
diff changeset
    52
      cong: if_cong)
6fae499e0827 summarized notions related to ordered_euclidean_space and intervals in separate theory
immler
parents:
diff changeset
    53
6fae499e0827 summarized notions related to ordered_euclidean_space and intervals in separate theory
immler
parents:
diff changeset
    54
lemma inner_Basis_INF_left: "i \<in> Basis \<Longrightarrow> (INF x:X. f x) \<bullet> i = (INF x:X. f x \<bullet> i)"
6fae499e0827 summarized notions related to ordered_euclidean_space and intervals in separate theory
immler
parents:
diff changeset
    55
  and inner_Basis_SUP_left: "i \<in> Basis \<Longrightarrow> (SUP x:X. f x) \<bullet> i = (SUP x:X. f x \<bullet> i)"
56166
9a241bc276cd normalising simp rules for compound operators
haftmann
parents: 55413
diff changeset
    56
  using eucl_Sup [of "f ` X"] eucl_Inf [of "f ` X"] by (simp_all add: comp_def)
54780
6fae499e0827 summarized notions related to ordered_euclidean_space and intervals in separate theory
immler
parents:
diff changeset
    57
6fae499e0827 summarized notions related to ordered_euclidean_space and intervals in separate theory
immler
parents:
diff changeset
    58
lemma abs_inner: "i \<in> Basis \<Longrightarrow> abs x \<bullet> i = abs (x \<bullet> i)"
6fae499e0827 summarized notions related to ordered_euclidean_space and intervals in separate theory
immler
parents:
diff changeset
    59
  by (auto simp: eucl_abs)
6fae499e0827 summarized notions related to ordered_euclidean_space and intervals in separate theory
immler
parents:
diff changeset
    60
6fae499e0827 summarized notions related to ordered_euclidean_space and intervals in separate theory
immler
parents:
diff changeset
    61
lemma
6fae499e0827 summarized notions related to ordered_euclidean_space and intervals in separate theory
immler
parents:
diff changeset
    62
  abs_scaleR: "\<bar>a *\<^sub>R b\<bar> = \<bar>a\<bar> *\<^sub>R \<bar>b\<bar>"
6fae499e0827 summarized notions related to ordered_euclidean_space and intervals in separate theory
immler
parents:
diff changeset
    63
  by (auto simp: eucl_abs abs_mult intro!: euclidean_eqI)
6fae499e0827 summarized notions related to ordered_euclidean_space and intervals in separate theory
immler
parents:
diff changeset
    64
6fae499e0827 summarized notions related to ordered_euclidean_space and intervals in separate theory
immler
parents:
diff changeset
    65
lemma interval_inner_leI:
6fae499e0827 summarized notions related to ordered_euclidean_space and intervals in separate theory
immler
parents:
diff changeset
    66
  assumes "x \<in> {a .. b}" "0 \<le> i"
6fae499e0827 summarized notions related to ordered_euclidean_space and intervals in separate theory
immler
parents:
diff changeset
    67
  shows "a\<bullet>i \<le> x\<bullet>i" "x\<bullet>i \<le> b\<bullet>i"
6fae499e0827 summarized notions related to ordered_euclidean_space and intervals in separate theory
immler
parents:
diff changeset
    68
  using assms
6fae499e0827 summarized notions related to ordered_euclidean_space and intervals in separate theory
immler
parents:
diff changeset
    69
  unfolding euclidean_inner[of a i] euclidean_inner[of x i] euclidean_inner[of b i]
6fae499e0827 summarized notions related to ordered_euclidean_space and intervals in separate theory
immler
parents:
diff changeset
    70
  by (auto intro!: setsum_mono mult_right_mono simp: eucl_le)
6fae499e0827 summarized notions related to ordered_euclidean_space and intervals in separate theory
immler
parents:
diff changeset
    71
6fae499e0827 summarized notions related to ordered_euclidean_space and intervals in separate theory
immler
parents:
diff changeset
    72
lemma inner_nonneg_nonneg:
6fae499e0827 summarized notions related to ordered_euclidean_space and intervals in separate theory
immler
parents:
diff changeset
    73
  shows "0 \<le> a \<Longrightarrow> 0 \<le> b \<Longrightarrow> 0 \<le> a \<bullet> b"
6fae499e0827 summarized notions related to ordered_euclidean_space and intervals in separate theory
immler
parents:
diff changeset
    74
  using interval_inner_leI[of a 0 a b]
6fae499e0827 summarized notions related to ordered_euclidean_space and intervals in separate theory
immler
parents:
diff changeset
    75
  by auto
6fae499e0827 summarized notions related to ordered_euclidean_space and intervals in separate theory
immler
parents:
diff changeset
    76
6fae499e0827 summarized notions related to ordered_euclidean_space and intervals in separate theory
immler
parents:
diff changeset
    77
lemma inner_Basis_mono:
6fae499e0827 summarized notions related to ordered_euclidean_space and intervals in separate theory
immler
parents:
diff changeset
    78
  shows "a \<le> b \<Longrightarrow> c \<in> Basis  \<Longrightarrow> a \<bullet> c \<le> b \<bullet> c"
6fae499e0827 summarized notions related to ordered_euclidean_space and intervals in separate theory
immler
parents:
diff changeset
    79
  by (simp add: eucl_le)
6fae499e0827 summarized notions related to ordered_euclidean_space and intervals in separate theory
immler
parents:
diff changeset
    80
6fae499e0827 summarized notions related to ordered_euclidean_space and intervals in separate theory
immler
parents:
diff changeset
    81
lemma Basis_nonneg[intro, simp]: "i \<in> Basis \<Longrightarrow> 0 \<le> i"
6fae499e0827 summarized notions related to ordered_euclidean_space and intervals in separate theory
immler
parents:
diff changeset
    82
  by (auto simp: eucl_le inner_Basis)
6fae499e0827 summarized notions related to ordered_euclidean_space and intervals in separate theory
immler
parents:
diff changeset
    83
54781
fe462aa28c3d additional lemmas
immler
parents: 54780
diff changeset
    84
lemma Sup_eq_maximum_componentwise:
fe462aa28c3d additional lemmas
immler
parents: 54780
diff changeset
    85
  fixes s::"'a set"
fe462aa28c3d additional lemmas
immler
parents: 54780
diff changeset
    86
  assumes i: "\<And>b. b \<in> Basis \<Longrightarrow> X \<bullet> b = i b \<bullet> b"
fe462aa28c3d additional lemmas
immler
parents: 54780
diff changeset
    87
  assumes sup: "\<And>b x. b \<in> Basis \<Longrightarrow> x \<in> s \<Longrightarrow> x \<bullet> b \<le> X \<bullet> b"
fe462aa28c3d additional lemmas
immler
parents: 54780
diff changeset
    88
  assumes i_s: "\<And>b. b \<in> Basis \<Longrightarrow> (i b \<bullet> b) \<in> (\<lambda>x. x \<bullet> b) ` s"
fe462aa28c3d additional lemmas
immler
parents: 54780
diff changeset
    89
  shows "Sup s = X"
fe462aa28c3d additional lemmas
immler
parents: 54780
diff changeset
    90
  using assms
fe462aa28c3d additional lemmas
immler
parents: 54780
diff changeset
    91
  unfolding eucl_Sup euclidean_representation_setsum
56166
9a241bc276cd normalising simp rules for compound operators
haftmann
parents: 55413
diff changeset
    92
  by (auto simp: Sup_class.SUP_def simp del: Sup_class.Sup_image_eq intro!: conditionally_complete_lattice_class.cSup_eq_maximum)
54781
fe462aa28c3d additional lemmas
immler
parents: 54780
diff changeset
    93
fe462aa28c3d additional lemmas
immler
parents: 54780
diff changeset
    94
lemma Inf_eq_minimum_componentwise:
fe462aa28c3d additional lemmas
immler
parents: 54780
diff changeset
    95
  assumes i: "\<And>b. b \<in> Basis \<Longrightarrow> X \<bullet> b = i b \<bullet> b"
fe462aa28c3d additional lemmas
immler
parents: 54780
diff changeset
    96
  assumes sup: "\<And>b x. b \<in> Basis \<Longrightarrow> x \<in> s \<Longrightarrow> X \<bullet> b \<le> x \<bullet> b"
fe462aa28c3d additional lemmas
immler
parents: 54780
diff changeset
    97
  assumes i_s: "\<And>b. b \<in> Basis \<Longrightarrow> (i b \<bullet> b) \<in> (\<lambda>x. x \<bullet> b) ` s"
fe462aa28c3d additional lemmas
immler
parents: 54780
diff changeset
    98
  shows "Inf s = X"
fe462aa28c3d additional lemmas
immler
parents: 54780
diff changeset
    99
  using assms
fe462aa28c3d additional lemmas
immler
parents: 54780
diff changeset
   100
  unfolding eucl_Inf euclidean_representation_setsum
56166
9a241bc276cd normalising simp rules for compound operators
haftmann
parents: 55413
diff changeset
   101
  by (auto simp: Inf_class.INF_def simp del: Inf_class.Inf_image_eq intro!: conditionally_complete_lattice_class.cInf_eq_minimum)
54781
fe462aa28c3d additional lemmas
immler
parents: 54780
diff changeset
   102
54780
6fae499e0827 summarized notions related to ordered_euclidean_space and intervals in separate theory
immler
parents:
diff changeset
   103
end
6fae499e0827 summarized notions related to ordered_euclidean_space and intervals in separate theory
immler
parents:
diff changeset
   104
54781
fe462aa28c3d additional lemmas
immler
parents: 54780
diff changeset
   105
lemma
fe462aa28c3d additional lemmas
immler
parents: 54780
diff changeset
   106
  compact_attains_Inf_componentwise:
fe462aa28c3d additional lemmas
immler
parents: 54780
diff changeset
   107
  fixes b::"'a::ordered_euclidean_space"
fe462aa28c3d additional lemmas
immler
parents: 54780
diff changeset
   108
  assumes "b \<in> Basis" assumes "X \<noteq> {}" "compact X"
fe462aa28c3d additional lemmas
immler
parents: 54780
diff changeset
   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"
fe462aa28c3d additional lemmas
immler
parents: 54780
diff changeset
   110
proof atomize_elim
fe462aa28c3d additional lemmas
immler
parents: 54780
diff changeset
   111
  let ?proj = "(\<lambda>x. x \<bullet> b) ` X"
fe462aa28c3d additional lemmas
immler
parents: 54780
diff changeset
   112
  from assms have "compact ?proj" "?proj \<noteq> {}"
56371
fb9ae0727548 extend continuous_intros; remove continuous_on_intros and isCont_intros
hoelzl
parents: 56190
diff changeset
   113
    by (auto intro!: compact_continuous_image continuous_intros)
54781
fe462aa28c3d additional lemmas
immler
parents: 54780
diff changeset
   114
  from compact_attains_inf[OF this]
fe462aa28c3d additional lemmas
immler
parents: 54780
diff changeset
   115
  obtain s x
fe462aa28c3d additional lemmas
immler
parents: 54780
diff changeset
   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"
fe462aa28c3d additional lemmas
immler
parents: 54780
diff changeset
   117
      and x: "x \<in> X" "s = x \<bullet> b" "\<And>y. y \<in> X \<Longrightarrow> x \<bullet> b \<le> y \<bullet> b"
fe462aa28c3d additional lemmas
immler
parents: 54780
diff changeset
   118
    by auto
fe462aa28c3d additional lemmas
immler
parents: 54780
diff changeset
   119
  hence "Inf ?proj = x \<bullet> b"
56166
9a241bc276cd normalising simp rules for compound operators
haftmann
parents: 55413
diff changeset
   120
    by (auto intro!: conditionally_complete_lattice_class.cInf_eq_minimum simp del: Inf_class.Inf_image_eq)
54781
fe462aa28c3d additional lemmas
immler
parents: 54780
diff changeset
   121
  hence "x \<bullet> b = Inf X \<bullet> b"
57418
6ab1c7cb0b8d fact consolidation
haftmann
parents: 56371
diff changeset
   122
    by (auto simp: eucl_Inf Inf_class.INF_def inner_setsum_left inner_Basis if_distrib `b \<in> Basis` setsum.delta
56166
9a241bc276cd normalising simp rules for compound operators
haftmann
parents: 55413
diff changeset
   123
      simp del: Inf_class.Inf_image_eq
9a241bc276cd normalising simp rules for compound operators
haftmann
parents: 55413
diff changeset
   124
      cong: if_cong)
54781
fe462aa28c3d additional lemmas
immler
parents: 54780
diff changeset
   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
fe462aa28c3d additional lemmas
immler
parents: 54780
diff changeset
   126
qed
fe462aa28c3d additional lemmas
immler
parents: 54780
diff changeset
   127
fe462aa28c3d additional lemmas
immler
parents: 54780
diff changeset
   128
lemma
fe462aa28c3d additional lemmas
immler
parents: 54780
diff changeset
   129
  compact_attains_Sup_componentwise:
fe462aa28c3d additional lemmas
immler
parents: 54780
diff changeset
   130
  fixes b::"'a::ordered_euclidean_space"
fe462aa28c3d additional lemmas
immler
parents: 54780
diff changeset
   131
  assumes "b \<in> Basis" assumes "X \<noteq> {}" "compact X"
fe462aa28c3d additional lemmas
immler
parents: 54780
diff changeset
   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"
fe462aa28c3d additional lemmas
immler
parents: 54780
diff changeset
   133
proof atomize_elim
fe462aa28c3d additional lemmas
immler
parents: 54780
diff changeset
   134
  let ?proj = "(\<lambda>x. x \<bullet> b) ` X"
fe462aa28c3d additional lemmas
immler
parents: 54780
diff changeset
   135
  from assms have "compact ?proj" "?proj \<noteq> {}"
56371
fb9ae0727548 extend continuous_intros; remove continuous_on_intros and isCont_intros
hoelzl
parents: 56190
diff changeset
   136
    by (auto intro!: compact_continuous_image continuous_intros)
54781
fe462aa28c3d additional lemmas
immler
parents: 54780
diff changeset
   137
  from compact_attains_sup[OF this]
fe462aa28c3d additional lemmas
immler
parents: 54780
diff changeset
   138
  obtain s x
fe462aa28c3d additional lemmas
immler
parents: 54780
diff changeset
   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"
fe462aa28c3d additional lemmas
immler
parents: 54780
diff changeset
   140
      and x: "x \<in> X" "s = x \<bullet> b" "\<And>y. y \<in> X \<Longrightarrow> y \<bullet> b \<le> x \<bullet> b"
fe462aa28c3d additional lemmas
immler
parents: 54780
diff changeset
   141
    by auto
fe462aa28c3d additional lemmas
immler
parents: 54780
diff changeset
   142
  hence "Sup ?proj = x \<bullet> b"
56166
9a241bc276cd normalising simp rules for compound operators
haftmann
parents: 55413
diff changeset
   143
    by (auto intro!: cSup_eq_maximum simp del: Sup_image_eq)
54781
fe462aa28c3d additional lemmas
immler
parents: 54780
diff changeset
   144
  hence "x \<bullet> b = Sup X \<bullet> b"
57418
6ab1c7cb0b8d fact consolidation
haftmann
parents: 56371
diff changeset
   145
    by (auto simp: eucl_Sup[where 'a='a] SUP_def inner_setsum_left inner_Basis if_distrib `b \<in> Basis` setsum.delta
56166
9a241bc276cd normalising simp rules for compound operators
haftmann
parents: 55413
diff changeset
   146
      simp del: Sup_image_eq cong: if_cong)
54781
fe462aa28c3d additional lemmas
immler
parents: 54780
diff changeset
   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
fe462aa28c3d additional lemmas
immler
parents: 54780
diff changeset
   148
qed
fe462aa28c3d additional lemmas
immler
parents: 54780
diff changeset
   149
54780
6fae499e0827 summarized notions related to ordered_euclidean_space and intervals in separate theory
immler
parents:
diff changeset
   150
lemma (in order) atLeastatMost_empty'[simp]:
6fae499e0827 summarized notions related to ordered_euclidean_space and intervals in separate theory
immler
parents:
diff changeset
   151
  "(~ a <= b) \<Longrightarrow> {a..b} = {}"
6fae499e0827 summarized notions related to ordered_euclidean_space and intervals in separate theory
immler
parents:
diff changeset
   152
  by (auto)
6fae499e0827 summarized notions related to ordered_euclidean_space and intervals in separate theory
immler
parents:
diff changeset
   153
6fae499e0827 summarized notions related to ordered_euclidean_space and intervals in separate theory
immler
parents:
diff changeset
   154
instance real :: ordered_euclidean_space
6fae499e0827 summarized notions related to ordered_euclidean_space and intervals in separate theory
immler
parents:
diff changeset
   155
  by default (auto simp: INF_def SUP_def)
6fae499e0827 summarized notions related to ordered_euclidean_space and intervals in separate theory
immler
parents:
diff changeset
   156
6fae499e0827 summarized notions related to ordered_euclidean_space and intervals in separate theory
immler
parents:
diff changeset
   157
lemma in_Basis_prod_iff:
6fae499e0827 summarized notions related to ordered_euclidean_space and intervals in separate theory
immler
parents:
diff changeset
   158
  fixes i::"'a::euclidean_space*'b::euclidean_space"
6fae499e0827 summarized notions related to ordered_euclidean_space and intervals in separate theory
immler
parents:
diff changeset
   159
  shows "i \<in> Basis \<longleftrightarrow> fst i = 0 \<and> snd i \<in> Basis \<or> snd i = 0 \<and> fst i \<in> Basis"
6fae499e0827 summarized notions related to ordered_euclidean_space and intervals in separate theory
immler
parents:
diff changeset
   160
  by (cases i) (auto simp: Basis_prod_def)
6fae499e0827 summarized notions related to ordered_euclidean_space and intervals in separate theory
immler
parents:
diff changeset
   161
6fae499e0827 summarized notions related to ordered_euclidean_space and intervals in separate theory
immler
parents:
diff changeset
   162
instantiation prod::(abs, abs) abs
6fae499e0827 summarized notions related to ordered_euclidean_space and intervals in separate theory
immler
parents:
diff changeset
   163
begin
6fae499e0827 summarized notions related to ordered_euclidean_space and intervals in separate theory
immler
parents:
diff changeset
   164
6fae499e0827 summarized notions related to ordered_euclidean_space and intervals in separate theory
immler
parents:
diff changeset
   165
definition "abs x = (abs (fst x), abs (snd x))"
6fae499e0827 summarized notions related to ordered_euclidean_space and intervals in separate theory
immler
parents:
diff changeset
   166
6fae499e0827 summarized notions related to ordered_euclidean_space and intervals in separate theory
immler
parents:
diff changeset
   167
instance proof qed
6fae499e0827 summarized notions related to ordered_euclidean_space and intervals in separate theory
immler
parents:
diff changeset
   168
end
6fae499e0827 summarized notions related to ordered_euclidean_space and intervals in separate theory
immler
parents:
diff changeset
   169
6fae499e0827 summarized notions related to ordered_euclidean_space and intervals in separate theory
immler
parents:
diff changeset
   170
instance prod :: (ordered_euclidean_space, ordered_euclidean_space) ordered_euclidean_space
6fae499e0827 summarized notions related to ordered_euclidean_space and intervals in separate theory
immler
parents:
diff changeset
   171
  by default
6fae499e0827 summarized notions related to ordered_euclidean_space and intervals in separate theory
immler
parents:
diff changeset
   172
    (auto intro!: add_mono simp add: euclidean_representation_setsum'  Ball_def inner_prod_def
6fae499e0827 summarized notions related to ordered_euclidean_space and intervals in separate theory
immler
parents:
diff changeset
   173
      in_Basis_prod_iff inner_Basis_inf_left inner_Basis_sup_left inner_Basis_INF_left Inf_prod_def
6fae499e0827 summarized notions related to ordered_euclidean_space and intervals in separate theory
immler
parents:
diff changeset
   174
      inner_Basis_SUP_left Sup_prod_def less_prod_def less_eq_prod_def eucl_le[where 'a='a]
6fae499e0827 summarized notions related to ordered_euclidean_space and intervals in separate theory
immler
parents:
diff changeset
   175
      eucl_le[where 'a='b] abs_prod_def abs_inner)
6fae499e0827 summarized notions related to ordered_euclidean_space and intervals in separate theory
immler
parents:
diff changeset
   176
56188
0268784f60da use cbox to relax class constraints
immler
parents: 56166
diff changeset
   177
text{* Instantiation for intervals on @{text ordered_euclidean_space} *}
0268784f60da use cbox to relax class constraints
immler
parents: 56166
diff changeset
   178
0268784f60da use cbox to relax class constraints
immler
parents: 56166
diff changeset
   179
lemma
0268784f60da use cbox to relax class constraints
immler
parents: 56166
diff changeset
   180
  fixes a :: "'a\<Colon>ordered_euclidean_space"
0268784f60da use cbox to relax class constraints
immler
parents: 56166
diff changeset
   181
  shows cbox_interval: "cbox a b = {a..b}"
0268784f60da use cbox to relax class constraints
immler
parents: 56166
diff changeset
   182
    and interval_cbox: "{a..b} = cbox a b"
0268784f60da use cbox to relax class constraints
immler
parents: 56166
diff changeset
   183
    and eucl_le_atMost: "{x. \<forall>i\<in>Basis. x \<bullet> i <= a \<bullet> i} = {..a}"
0268784f60da use cbox to relax class constraints
immler
parents: 56166
diff changeset
   184
    and eucl_le_atLeast: "{x. \<forall>i\<in>Basis. a \<bullet> i <= x \<bullet> i} = {a..}"
0268784f60da use cbox to relax class constraints
immler
parents: 56166
diff changeset
   185
    by (auto simp: eucl_le[where 'a='a] eucl_less_def box_def cbox_def)
0268784f60da use cbox to relax class constraints
immler
parents: 56166
diff changeset
   186
0268784f60da use cbox to relax class constraints
immler
parents: 56166
diff changeset
   187
lemma closed_eucl_atLeastAtMost[simp, intro]:
0268784f60da use cbox to relax class constraints
immler
parents: 56166
diff changeset
   188
  fixes a :: "'a\<Colon>ordered_euclidean_space"
0268784f60da use cbox to relax class constraints
immler
parents: 56166
diff changeset
   189
  shows "closed {a..b}"
0268784f60da use cbox to relax class constraints
immler
parents: 56166
diff changeset
   190
  by (simp add: cbox_interval[symmetric] closed_cbox)
0268784f60da use cbox to relax class constraints
immler
parents: 56166
diff changeset
   191
0268784f60da use cbox to relax class constraints
immler
parents: 56166
diff changeset
   192
lemma closed_eucl_atMost[simp, intro]:
0268784f60da use cbox to relax class constraints
immler
parents: 56166
diff changeset
   193
  fixes a :: "'a\<Colon>ordered_euclidean_space"
0268784f60da use cbox to relax class constraints
immler
parents: 56166
diff changeset
   194
  shows "closed {..a}"
0268784f60da use cbox to relax class constraints
immler
parents: 56166
diff changeset
   195
  by (simp add: eucl_le_atMost[symmetric])
0268784f60da use cbox to relax class constraints
immler
parents: 56166
diff changeset
   196
0268784f60da use cbox to relax class constraints
immler
parents: 56166
diff changeset
   197
lemma closed_eucl_atLeast[simp, intro]:
0268784f60da use cbox to relax class constraints
immler
parents: 56166
diff changeset
   198
  fixes a :: "'a\<Colon>ordered_euclidean_space"
0268784f60da use cbox to relax class constraints
immler
parents: 56166
diff changeset
   199
  shows "closed {a..}"
0268784f60da use cbox to relax class constraints
immler
parents: 56166
diff changeset
   200
  by (simp add: eucl_le_atLeast[symmetric])
0268784f60da use cbox to relax class constraints
immler
parents: 56166
diff changeset
   201
56189
c4daa97ac57a removed dependencies on theory Ordered_Euclidean_Space
immler
parents: 56188
diff changeset
   202
lemma bounded_closed_interval:
c4daa97ac57a removed dependencies on theory Ordered_Euclidean_Space
immler
parents: 56188
diff changeset
   203
  fixes a :: "'a::ordered_euclidean_space"
c4daa97ac57a removed dependencies on theory Ordered_Euclidean_Space
immler
parents: 56188
diff changeset
   204
  shows "bounded {a .. b}"
c4daa97ac57a removed dependencies on theory Ordered_Euclidean_Space
immler
parents: 56188
diff changeset
   205
  using bounded_cbox[of a b]
c4daa97ac57a removed dependencies on theory Ordered_Euclidean_Space
immler
parents: 56188
diff changeset
   206
  by (metis interval_cbox)
c4daa97ac57a removed dependencies on theory Ordered_Euclidean_Space
immler
parents: 56188
diff changeset
   207
56190
f0d2609c4cdc additional lemmas
immler
parents: 56189
diff changeset
   208
lemma convex_closed_interval:
f0d2609c4cdc additional lemmas
immler
parents: 56189
diff changeset
   209
  fixes a :: "'a::ordered_euclidean_space"
f0d2609c4cdc additional lemmas
immler
parents: 56189
diff changeset
   210
  shows "convex {a .. b}"
f0d2609c4cdc additional lemmas
immler
parents: 56189
diff changeset
   211
  using convex_box[of a b]
f0d2609c4cdc additional lemmas
immler
parents: 56189
diff changeset
   212
  by (metis interval_cbox)
f0d2609c4cdc additional lemmas
immler
parents: 56189
diff changeset
   213
56188
0268784f60da use cbox to relax class constraints
immler
parents: 56166
diff changeset
   214
lemma image_affinity_interval: fixes m::real
0268784f60da use cbox to relax class constraints
immler
parents: 56166
diff changeset
   215
  fixes a b c :: "'a::ordered_euclidean_space"
0268784f60da use cbox to relax class constraints
immler
parents: 56166
diff changeset
   216
  shows "(\<lambda>x. m *\<^sub>R x + c) ` {a..b} =
0268784f60da use cbox to relax class constraints
immler
parents: 56166
diff changeset
   217
    (if {a..b} = {} then {}
0268784f60da use cbox to relax class constraints
immler
parents: 56166
diff changeset
   218
     else (if 0 \<le> m then {m *\<^sub>R a + c .. m *\<^sub>R b + c}
0268784f60da use cbox to relax class constraints
immler
parents: 56166
diff changeset
   219
     else {m *\<^sub>R b + c .. m *\<^sub>R a + c}))"
0268784f60da use cbox to relax class constraints
immler
parents: 56166
diff changeset
   220
  using image_affinity_cbox[of m c a b]
0268784f60da use cbox to relax class constraints
immler
parents: 56166
diff changeset
   221
  by (simp add: cbox_interval)
0268784f60da use cbox to relax class constraints
immler
parents: 56166
diff changeset
   222
0268784f60da use cbox to relax class constraints
immler
parents: 56166
diff changeset
   223
lemma image_smult_interval:"(\<lambda>x. m *\<^sub>R (x::_::ordered_euclidean_space)) ` {a .. b} =
0268784f60da use cbox to relax class constraints
immler
parents: 56166
diff changeset
   224
  (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})"
0268784f60da use cbox to relax class constraints
immler
parents: 56166
diff changeset
   225
  using image_smult_cbox[of m a b]
0268784f60da use cbox to relax class constraints
immler
parents: 56166
diff changeset
   226
  by (simp add: cbox_interval)
54780
6fae499e0827 summarized notions related to ordered_euclidean_space and intervals in separate theory
immler
parents:
diff changeset
   227
56189
c4daa97ac57a removed dependencies on theory Ordered_Euclidean_Space
immler
parents: 56188
diff changeset
   228
lemma is_interval_closed_interval:
c4daa97ac57a removed dependencies on theory Ordered_Euclidean_Space
immler
parents: 56188
diff changeset
   229
  "is_interval {a .. (b::'a::ordered_euclidean_space)}"
c4daa97ac57a removed dependencies on theory Ordered_Euclidean_Space
immler
parents: 56188
diff changeset
   230
  by (metis cbox_interval is_interval_cbox)
c4daa97ac57a removed dependencies on theory Ordered_Euclidean_Space
immler
parents: 56188
diff changeset
   231
56190
f0d2609c4cdc additional lemmas
immler
parents: 56189
diff changeset
   232
lemma compact_interval:
f0d2609c4cdc additional lemmas
immler
parents: 56189
diff changeset
   233
  fixes a b::"'a::ordered_euclidean_space"
f0d2609c4cdc additional lemmas
immler
parents: 56189
diff changeset
   234
  shows "compact {a .. b}"
f0d2609c4cdc additional lemmas
immler
parents: 56189
diff changeset
   235
  by (metis compact_cbox interval_cbox)
f0d2609c4cdc additional lemmas
immler
parents: 56189
diff changeset
   236
54780
6fae499e0827 summarized notions related to ordered_euclidean_space and intervals in separate theory
immler
parents:
diff changeset
   237
no_notation
6fae499e0827 summarized notions related to ordered_euclidean_space and intervals in separate theory
immler
parents:
diff changeset
   238
  eucl_less (infix "<e" 50)
6fae499e0827 summarized notions related to ordered_euclidean_space and intervals in separate theory
immler
parents:
diff changeset
   239
56189
c4daa97ac57a removed dependencies on theory Ordered_Euclidean_Space
immler
parents: 56188
diff changeset
   240
lemma One_nonneg: "0 \<le> (\<Sum>Basis::'a::ordered_euclidean_space)"
c4daa97ac57a removed dependencies on theory Ordered_Euclidean_Space
immler
parents: 56188
diff changeset
   241
  by (auto intro: setsum_nonneg)
c4daa97ac57a removed dependencies on theory Ordered_Euclidean_Space
immler
parents: 56188
diff changeset
   242
c4daa97ac57a removed dependencies on theory Ordered_Euclidean_Space
immler
parents: 56188
diff changeset
   243
lemma content_closed_interval:
c4daa97ac57a removed dependencies on theory Ordered_Euclidean_Space
immler
parents: 56188
diff changeset
   244
  fixes a :: "'a::ordered_euclidean_space"
c4daa97ac57a removed dependencies on theory Ordered_Euclidean_Space
immler
parents: 56188
diff changeset
   245
  assumes "a \<le> b"
c4daa97ac57a removed dependencies on theory Ordered_Euclidean_Space
immler
parents: 56188
diff changeset
   246
  shows "content {a .. b} = (\<Prod>i\<in>Basis. b\<bullet>i - a\<bullet>i)"
c4daa97ac57a removed dependencies on theory Ordered_Euclidean_Space
immler
parents: 56188
diff changeset
   247
  using content_cbox[of a b] assms
c4daa97ac57a removed dependencies on theory Ordered_Euclidean_Space
immler
parents: 56188
diff changeset
   248
  by (simp add: cbox_interval eucl_le[where 'a='a])
c4daa97ac57a removed dependencies on theory Ordered_Euclidean_Space
immler
parents: 56188
diff changeset
   249
c4daa97ac57a removed dependencies on theory Ordered_Euclidean_Space
immler
parents: 56188
diff changeset
   250
lemma integrable_const_ivl[intro]:
c4daa97ac57a removed dependencies on theory Ordered_Euclidean_Space
immler
parents: 56188
diff changeset
   251
  fixes a::"'a::ordered_euclidean_space"
c4daa97ac57a removed dependencies on theory Ordered_Euclidean_Space
immler
parents: 56188
diff changeset
   252
  shows "(\<lambda>x. c) integrable_on {a .. b}"
c4daa97ac57a removed dependencies on theory Ordered_Euclidean_Space
immler
parents: 56188
diff changeset
   253
  unfolding cbox_interval[symmetric]
c4daa97ac57a removed dependencies on theory Ordered_Euclidean_Space
immler
parents: 56188
diff changeset
   254
  by (rule integrable_const)
c4daa97ac57a removed dependencies on theory Ordered_Euclidean_Space
immler
parents: 56188
diff changeset
   255
c4daa97ac57a removed dependencies on theory Ordered_Euclidean_Space
immler
parents: 56188
diff changeset
   256
lemma integrable_on_subinterval:
c4daa97ac57a removed dependencies on theory Ordered_Euclidean_Space
immler
parents: 56188
diff changeset
   257
  fixes f :: "'n::ordered_euclidean_space \<Rightarrow> 'a::banach"
c4daa97ac57a removed dependencies on theory Ordered_Euclidean_Space
immler
parents: 56188
diff changeset
   258
  assumes "f integrable_on s"
c4daa97ac57a removed dependencies on theory Ordered_Euclidean_Space
immler
parents: 56188
diff changeset
   259
    and "{a .. b} \<subseteq> s"
c4daa97ac57a removed dependencies on theory Ordered_Euclidean_Space
immler
parents: 56188
diff changeset
   260
  shows "f integrable_on {a .. b}"
c4daa97ac57a removed dependencies on theory Ordered_Euclidean_Space
immler
parents: 56188
diff changeset
   261
  using integrable_on_subcbox[of f s a b] assms
c4daa97ac57a removed dependencies on theory Ordered_Euclidean_Space
immler
parents: 56188
diff changeset
   262
  by (simp add: cbox_interval)
c4daa97ac57a removed dependencies on theory Ordered_Euclidean_Space
immler
parents: 56188
diff changeset
   263
56190
f0d2609c4cdc additional lemmas
immler
parents: 56189
diff changeset
   264
lemma
f0d2609c4cdc additional lemmas
immler
parents: 56189
diff changeset
   265
  fixes a b::"'a::ordered_euclidean_space"
f0d2609c4cdc additional lemmas
immler
parents: 56189
diff changeset
   266
  shows bdd_above_cbox[intro, simp]: "bdd_above (cbox a b)"
f0d2609c4cdc additional lemmas
immler
parents: 56189
diff changeset
   267
    and bdd_below_cbox[intro, simp]: "bdd_below (cbox a b)"
f0d2609c4cdc additional lemmas
immler
parents: 56189
diff changeset
   268
    and bdd_above_box[intro, simp]: "bdd_above (box a b)"
f0d2609c4cdc additional lemmas
immler
parents: 56189
diff changeset
   269
    and bdd_below_box[intro, simp]: "bdd_below (box a b)"
f0d2609c4cdc additional lemmas
immler
parents: 56189
diff changeset
   270
  unfolding atomize_conj
f0d2609c4cdc additional lemmas
immler
parents: 56189
diff changeset
   271
  by (metis bdd_above_Icc bdd_above_mono bdd_below_Icc bdd_below_mono bounded_box
f0d2609c4cdc additional lemmas
immler
parents: 56189
diff changeset
   272
    bounded_subset_cbox interval_cbox)
f0d2609c4cdc additional lemmas
immler
parents: 56189
diff changeset
   273
56189
c4daa97ac57a removed dependencies on theory Ordered_Euclidean_Space
immler
parents: 56188
diff changeset
   274
instantiation vec :: (ordered_euclidean_space, finite) ordered_euclidean_space
c4daa97ac57a removed dependencies on theory Ordered_Euclidean_Space
immler
parents: 56188
diff changeset
   275
begin
c4daa97ac57a removed dependencies on theory Ordered_Euclidean_Space
immler
parents: 56188
diff changeset
   276
c4daa97ac57a removed dependencies on theory Ordered_Euclidean_Space
immler
parents: 56188
diff changeset
   277
definition "inf x y = (\<chi> i. inf (x $ i) (y $ i))"
c4daa97ac57a removed dependencies on theory Ordered_Euclidean_Space
immler
parents: 56188
diff changeset
   278
definition "sup x y = (\<chi> i. sup (x $ i) (y $ i))"
c4daa97ac57a removed dependencies on theory Ordered_Euclidean_Space
immler
parents: 56188
diff changeset
   279
definition "Inf X = (\<chi> i. (INF x:X. x $ i))"
c4daa97ac57a removed dependencies on theory Ordered_Euclidean_Space
immler
parents: 56188
diff changeset
   280
definition "Sup X = (\<chi> i. (SUP x:X. x $ i))"
c4daa97ac57a removed dependencies on theory Ordered_Euclidean_Space
immler
parents: 56188
diff changeset
   281
definition "abs x = (\<chi> i. abs (x $ i))"
c4daa97ac57a removed dependencies on theory Ordered_Euclidean_Space
immler
parents: 56188
diff changeset
   282
c4daa97ac57a removed dependencies on theory Ordered_Euclidean_Space
immler
parents: 56188
diff changeset
   283
instance
c4daa97ac57a removed dependencies on theory Ordered_Euclidean_Space
immler
parents: 56188
diff changeset
   284
  apply default
c4daa97ac57a removed dependencies on theory Ordered_Euclidean_Space
immler
parents: 56188
diff changeset
   285
  unfolding euclidean_representation_setsum'
c4daa97ac57a removed dependencies on theory Ordered_Euclidean_Space
immler
parents: 56188
diff changeset
   286
  apply (auto simp: less_eq_vec_def inf_vec_def sup_vec_def Inf_vec_def Sup_vec_def inner_axis
c4daa97ac57a removed dependencies on theory Ordered_Euclidean_Space
immler
parents: 56188
diff changeset
   287
    Basis_vec_def inner_Basis_inf_left inner_Basis_sup_left inner_Basis_INF_left
c4daa97ac57a removed dependencies on theory Ordered_Euclidean_Space
immler
parents: 56188
diff changeset
   288
    inner_Basis_SUP_left eucl_le[where 'a='a] less_le_not_le abs_vec_def abs_inner)
c4daa97ac57a removed dependencies on theory Ordered_Euclidean_Space
immler
parents: 56188
diff changeset
   289
  done
c4daa97ac57a removed dependencies on theory Ordered_Euclidean_Space
immler
parents: 56188
diff changeset
   290
54780
6fae499e0827 summarized notions related to ordered_euclidean_space and intervals in separate theory
immler
parents:
diff changeset
   291
end
56189
c4daa97ac57a removed dependencies on theory Ordered_Euclidean_Space
immler
parents: 56188
diff changeset
   292
c4daa97ac57a removed dependencies on theory Ordered_Euclidean_Space
immler
parents: 56188
diff changeset
   293
end
c4daa97ac57a removed dependencies on theory Ordered_Euclidean_Space
immler
parents: 56188
diff changeset
   294