src/HOL/Analysis/Ordered_Euclidean_Space.thy
 changeset 68833 fde093888c16 parent 68239 0764ee22a4d1 child 69000 7cb3ddd60fd6
```     1.1 --- a/src/HOL/Analysis/Ordered_Euclidean_Space.thy	Mon Aug 27 22:58:36 2018 +0200
1.2 +++ b/src/HOL/Analysis/Ordered_Euclidean_Space.thy	Tue Aug 28 13:28:39 2018 +0100
1.3 @@ -4,7 +4,7 @@
1.4    "HOL-Library.Product_Order"
1.5  begin
1.6
1.7 -subsection \<open>An ordering on euclidean spaces that will allow us to talk about intervals\<close>
1.8 +subsection%important \<open>An ordering on euclidean spaces that will allow us to talk about intervals\<close>
1.9
1.10  class ordered_euclidean_space = ord + inf + sup + abs + Inf + Sup + euclidean_space +
1.11    assumes eucl_le: "x \<le> y \<longleftrightarrow> (\<forall>i\<in>Basis. x \<bullet> i \<le> y \<bullet> i)"
1.12 @@ -33,7 +33,7 @@
1.13    by standard (auto simp: eucl_inf eucl_sup sup_inf_distrib1 intro!: euclidean_eqI)
1.14
1.15  subclass conditionally_complete_lattice
1.16 -proof
1.17 +proof%unimportant
1.18    fix z::'a and X::"'a set"
1.19    assume "X \<noteq> {}"
1.20    hence "\<And>i. (\<lambda>x. x \<bullet> i) ` X \<noteq> {}" by simp
1.21 @@ -44,42 +44,42 @@
1.22        simp: bdd_below_def bdd_above_def preorder_class.bdd_below_def preorder_class.bdd_above_def
1.23          eucl_Inf eucl_Sup eucl_le)+
1.24
1.25 -lemma inner_Basis_inf_left: "i \<in> Basis \<Longrightarrow> inf x y \<bullet> i = inf (x \<bullet> i) (y \<bullet> i)"
1.26 +lemma%unimportant inner_Basis_inf_left: "i \<in> Basis \<Longrightarrow> inf x y \<bullet> i = inf (x \<bullet> i) (y \<bullet> i)"
1.27    and inner_Basis_sup_left: "i \<in> Basis \<Longrightarrow> sup x y \<bullet> i = sup (x \<bullet> i) (y \<bullet> i)"
1.29        cong: if_cong)
1.30
1.31 -lemma inner_Basis_INF_left: "i \<in> Basis \<Longrightarrow> (INF x:X. f x) \<bullet> i = (INF x:X. f x \<bullet> i)"
1.32 +lemma%unimportant inner_Basis_INF_left: "i \<in> Basis \<Longrightarrow> (INF x:X. f x) \<bullet> i = (INF x:X. f x \<bullet> i)"
1.33    and inner_Basis_SUP_left: "i \<in> Basis \<Longrightarrow> (SUP x:X. f x) \<bullet> i = (SUP x:X. f x \<bullet> i)"
1.34    using eucl_Sup [of "f ` X"] eucl_Inf [of "f ` X"] by (simp_all add: comp_def)
1.35
1.36 -lemma abs_inner: "i \<in> Basis \<Longrightarrow> \<bar>x\<bar> \<bullet> i = \<bar>x \<bullet> i\<bar>"
1.37 +lemma%unimportant abs_inner: "i \<in> Basis \<Longrightarrow> \<bar>x\<bar> \<bullet> i = \<bar>x \<bullet> i\<bar>"
1.38    by (auto simp: eucl_abs)
1.39
1.40 -lemma
1.41 +lemma%unimportant
1.42    abs_scaleR: "\<bar>a *\<^sub>R b\<bar> = \<bar>a\<bar> *\<^sub>R \<bar>b\<bar>"
1.43    by (auto simp: eucl_abs abs_mult intro!: euclidean_eqI)
1.44
1.45 -lemma interval_inner_leI:
1.46 +lemma%unimportant interval_inner_leI:
1.47    assumes "x \<in> {a .. b}" "0 \<le> i"
1.48    shows "a\<bullet>i \<le> x\<bullet>i" "x\<bullet>i \<le> b\<bullet>i"
1.49    using assms
1.50    unfolding euclidean_inner[of a i] euclidean_inner[of x i] euclidean_inner[of b i]
1.51    by (auto intro!: ordered_comm_monoid_add_class.sum_mono mult_right_mono simp: eucl_le)
1.52
1.53 -lemma inner_nonneg_nonneg:
1.54 +lemma%unimportant inner_nonneg_nonneg:
1.55    shows "0 \<le> a \<Longrightarrow> 0 \<le> b \<Longrightarrow> 0 \<le> a \<bullet> b"
1.56    using interval_inner_leI[of a 0 a b]
1.57    by auto
1.58
1.59 -lemma inner_Basis_mono:
1.60 +lemma%unimportant inner_Basis_mono:
1.61    shows "a \<le> b \<Longrightarrow> c \<in> Basis  \<Longrightarrow> a \<bullet> c \<le> b \<bullet> c"
1.63
1.64 -lemma Basis_nonneg[intro, simp]: "i \<in> Basis \<Longrightarrow> 0 \<le> i"
1.65 +lemma%unimportant Basis_nonneg[intro, simp]: "i \<in> Basis \<Longrightarrow> 0 \<le> i"
1.66    by (auto simp: eucl_le inner_Basis)
1.67
1.68 -lemma Sup_eq_maximum_componentwise:
1.69 +lemma%unimportant Sup_eq_maximum_componentwise:
1.70    fixes s::"'a set"
1.71    assumes i: "\<And>b. b \<in> Basis \<Longrightarrow> X \<bullet> b = i b \<bullet> b"
1.72    assumes sup: "\<And>b x. b \<in> Basis \<Longrightarrow> x \<in> s \<Longrightarrow> x \<bullet> b \<le> X \<bullet> b"
1.73 @@ -89,7 +89,7 @@
1.74    unfolding eucl_Sup euclidean_representation_sum
1.75    by (auto intro!: conditionally_complete_lattice_class.cSup_eq_maximum)
1.76
1.77 -lemma Inf_eq_minimum_componentwise:
1.78 +lemma%unimportant Inf_eq_minimum_componentwise:
1.79    assumes i: "\<And>b. b \<in> Basis \<Longrightarrow> X \<bullet> b = i b \<bullet> b"
1.80    assumes sup: "\<And>b x. b \<in> Basis \<Longrightarrow> x \<in> s \<Longrightarrow> X \<bullet> b \<le> x \<bullet> b"
1.81    assumes i_s: "\<And>b. b \<in> Basis \<Longrightarrow> (i b \<bullet> b) \<in> (\<lambda>x. x \<bullet> b) ` s"
1.82 @@ -100,12 +100,12 @@
1.83
1.84  end
1.85
1.86 -lemma
1.87 +lemma%important
1.88    compact_attains_Inf_componentwise:
1.89    fixes b::"'a::ordered_euclidean_space"
1.90    assumes "b \<in> Basis" assumes "X \<noteq> {}" "compact X"
1.91    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"
1.92 -proof atomize_elim
1.93 +proof%unimportant atomize_elim
1.94    let ?proj = "(\<lambda>x. x \<bullet> b) ` X"
1.95    from assms have "compact ?proj" "?proj \<noteq> {}"
1.96      by (auto intro!: compact_continuous_image continuous_intros)
1.97 @@ -122,12 +122,12 @@
1.98    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
1.99  qed
1.100
1.101 -lemma
1.102 +lemma%important
1.103    compact_attains_Sup_componentwise:
1.104    fixes b::"'a::ordered_euclidean_space"
1.105    assumes "b \<in> Basis" assumes "X \<noteq> {}" "compact X"
1.106    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"
1.107 -proof atomize_elim
1.108 +proof%unimportant atomize_elim
1.109    let ?proj = "(\<lambda>x. x \<bullet> b) ` X"
1.110    from assms have "compact ?proj" "?proj \<noteq> {}"
1.111      by (auto intro!: compact_continuous_image continuous_intros)
1.112 @@ -144,14 +144,14 @@
1.113    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
1.114  qed
1.115
1.116 -lemma (in order) atLeastatMost_empty'[simp]:
1.117 +lemma%unimportant (in order) atLeastatMost_empty'[simp]:
1.118    "(~ a <= b) \<Longrightarrow> {a..b} = {}"
1.119    by (auto)
1.120
1.121  instance real :: ordered_euclidean_space
1.122    by standard auto
1.123
1.124 -lemma in_Basis_prod_iff:
1.125 +lemma%unimportant in_Basis_prod_iff:
1.126    fixes i::"'a::euclidean_space*'b::euclidean_space"
1.127    shows "i \<in> Basis \<longleftrightarrow> fst i = 0 \<and> snd i \<in> Basis \<or> snd i = 0 \<and> fst i \<in> Basis"
1.128    by (cases i) (auto simp: Basis_prod_def)
1.129 @@ -174,52 +174,52 @@
1.130
1.131  text\<open>Instantiation for intervals on \<open>ordered_euclidean_space\<close>\<close>
1.132
1.133 -lemma
1.134 +lemma%important
1.135    fixes a :: "'a::ordered_euclidean_space"
1.136    shows cbox_interval: "cbox a b = {a..b}"
1.137      and interval_cbox: "{a..b} = cbox a b"
1.138      and eucl_le_atMost: "{x. \<forall>i\<in>Basis. x \<bullet> i <= a \<bullet> i} = {..a}"
1.139      and eucl_le_atLeast: "{x. \<forall>i\<in>Basis. a \<bullet> i <= x \<bullet> i} = {a..}"
1.140 -    by (auto simp: eucl_le[where 'a='a] eucl_less_def box_def cbox_def)
1.141 +    by%unimportant (auto simp: eucl_le[where 'a='a] eucl_less_def box_def cbox_def)
1.142
1.143 -lemma vec_nth_real_1_iff_cbox [simp]:
1.144 +lemma%unimportant vec_nth_real_1_iff_cbox [simp]:
1.145    fixes a b :: real
1.146    shows "(\<lambda>x::real^1. x \$ 1) ` S = {a..b} \<longleftrightarrow> S = cbox (vec a) (vec b)"
1.147    by (metis interval_cbox vec_nth_1_iff_cbox)
1.148
1.149 -lemma closed_eucl_atLeastAtMost[simp, intro]:
1.150 +lemma%unimportant closed_eucl_atLeastAtMost[simp, intro]:
1.151    fixes a :: "'a::ordered_euclidean_space"
1.152    shows "closed {a..b}"
1.153    by (simp add: cbox_interval[symmetric] closed_cbox)
1.154
1.155 -lemma closed_eucl_atMost[simp, intro]:
1.156 +lemma%unimportant closed_eucl_atMost[simp, intro]:
1.157    fixes a :: "'a::ordered_euclidean_space"
1.158    shows "closed {..a}"
1.159    by (simp add: closed_interval_left eucl_le_atMost[symmetric])
1.160
1.161 -lemma closed_eucl_atLeast[simp, intro]:
1.162 +lemma%unimportant closed_eucl_atLeast[simp, intro]:
1.163    fixes a :: "'a::ordered_euclidean_space"
1.164    shows "closed {a..}"
1.165    by (simp add: closed_interval_right eucl_le_atLeast[symmetric])
1.166
1.167 -lemma bounded_closed_interval [simp]:
1.168 +lemma%unimportant bounded_closed_interval [simp]:
1.169    fixes a :: "'a::ordered_euclidean_space"
1.170    shows "bounded {a .. b}"
1.171    using bounded_cbox[of a b]
1.172    by (metis interval_cbox)
1.173
1.174 -lemma convex_closed_interval [simp]:
1.175 +lemma%unimportant convex_closed_interval [simp]:
1.176    fixes a :: "'a::ordered_euclidean_space"
1.177    shows "convex {a .. b}"
1.178    using convex_box[of a b]
1.179    by (metis interval_cbox)
1.180
1.181 -lemma image_smult_interval:"(\<lambda>x. m *\<^sub>R (x::_::ordered_euclidean_space)) ` {a .. b} =
1.182 +lemma%unimportant image_smult_interval:"(\<lambda>x. m *\<^sub>R (x::_::ordered_euclidean_space)) ` {a .. b} =
1.183    (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})"
1.184    using image_smult_cbox[of m a b]
1.186
1.187 -lemma [simp]:
1.188 +lemma%unimportant [simp]:
1.189    fixes a b::"'a::ordered_euclidean_space" and r s::real
1.190    shows is_interval_io: "is_interval {..<r}"
1.191      and is_interval_ic: "is_interval {..a}"
1.192 @@ -231,15 +231,15 @@
1.193      and is_interval_cc: "is_interval {b..a}"
1.194    by (force simp: is_interval_def eucl_le[where 'a='a])+
1.195
1.196 -lemma is_interval_real_ereal_oo: "is_interval (real_of_ereal ` {N<..<M::ereal})"
1.197 +lemma%unimportant is_interval_real_ereal_oo: "is_interval (real_of_ereal ` {N<..<M::ereal})"
1.198    by (auto simp: real_atLeastGreaterThan_eq)
1.199
1.200 -lemma compact_interval [simp]:
1.201 +lemma%unimportant compact_interval [simp]:
1.202    fixes a b::"'a::ordered_euclidean_space"
1.203    shows "compact {a .. b}"
1.204    by (metis compact_cbox interval_cbox)
1.205
1.206 -lemma homeomorphic_closed_intervals:
1.207 +lemma%unimportant homeomorphic_closed_intervals:
1.208    fixes a :: "'a::euclidean_space" and b and c :: "'a::euclidean_space" and d
1.209    assumes "box a b \<noteq> {}" and "box c d \<noteq> {}"
1.210      shows "(cbox a b) homeomorphic (cbox c d)"
1.211 @@ -247,7 +247,7 @@
1.212  using assms apply auto
1.213  done
1.214
1.215 -lemma homeomorphic_closed_intervals_real:
1.216 +lemma%unimportant homeomorphic_closed_intervals_real:
1.217    fixes a::real and b and c::real and d
1.218    assumes "a<b" and "c<d"
1.219    shows "{a..b} homeomorphic {c..d}"
1.220 @@ -256,10 +256,10 @@
1.221  no_notation
1.222    eucl_less (infix "<e" 50)
1.223
1.224 -lemma One_nonneg: "0 \<le> (\<Sum>Basis::'a::ordered_euclidean_space)"
1.225 +lemma%unimportant One_nonneg: "0 \<le> (\<Sum>Basis::'a::ordered_euclidean_space)"
1.226    by (auto intro: sum_nonneg)
1.227
1.228 -lemma
1.229 +lemma%unimportant
1.230    fixes a b::"'a::ordered_euclidean_space"
1.231    shows bdd_above_cbox[intro, simp]: "bdd_above (cbox a b)"
1.232      and bdd_below_cbox[intro, simp]: "bdd_below (cbox a b)"
1.233 @@ -272,11 +272,11 @@
1.234  instantiation vec :: (ordered_euclidean_space, finite) ordered_euclidean_space
1.235  begin
1.236
1.237 -definition "inf x y = (\<chi> i. inf (x \$ i) (y \$ i))"
1.238 -definition "sup x y = (\<chi> i. sup (x \$ i) (y \$ i))"
1.239 -definition "Inf X = (\<chi> i. (INF x:X. x \$ i))"
1.240 -definition "Sup X = (\<chi> i. (SUP x:X. x \$ i))"
1.241 -definition "\<bar>x\<bar> = (\<chi> i. \<bar>x \$ i\<bar>)"
1.242 +definition%important "inf x y = (\<chi> i. inf (x \$ i) (y \$ i))"
1.243 +definition%important "sup x y = (\<chi> i. sup (x \$ i) (y \$ i))"
1.244 +definition%important "Inf X = (\<chi> i. (INF x:X. x \$ i))"
1.245 +definition%important "Sup X = (\<chi> i. (SUP x:X. x \$ i))"
1.246 +definition%important "\<bar>x\<bar> = (\<chi> i. \<bar>x \$ i\<bar>)"
1.247
1.248  instance
1.249    apply standard
1.250 @@ -288,12 +288,12 @@
1.251
1.252  end
1.253
1.254 -lemma ANR_interval [iff]:
1.255 +lemma%unimportant ANR_interval [iff]:
1.256      fixes a :: "'a::ordered_euclidean_space"
1.257      shows "ANR{a..b}"