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.28    by (simp_all add: eucl_inf eucl_sup inner_sum_left inner_Basis if_distrib comm_monoid_add_class.sum.delta
    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.62    by (simp add: eucl_le)
    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.185    by (simp add: cbox_interval)
   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}"
   1.258  by (simp add: interval_cbox)
   1.259  
   1.260 -lemma ENR_interval [iff]:
   1.261 +lemma%unimportant ENR_interval [iff]:
   1.262      fixes a :: "'a::ordered_euclidean_space"
   1.263      shows "ENR{a..b}"
   1.264    by (auto simp: interval_cbox)