new topological lemmas; tuned proofs
authorhuffman
Mon Oct 07 08:39:50 2013 -0700 (2013-10-07)
changeset 540701a13325269c2
parent 54069 3fd3b1683d2b
child 54071 5752a39e482e
new topological lemmas; tuned proofs
src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy
     1.1 --- a/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy	Sun Oct 06 20:54:28 2013 +0200
     1.2 +++ b/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy	Mon Oct 07 08:39:50 2013 -0700
     1.3 @@ -789,18 +789,20 @@
     1.4    "a - b \<ge> c \<longleftrightarrow> a \<ge> c + b"
     1.5    by arith+
     1.6  
     1.7 -lemma open_ball[intro, simp]: "open (ball x e)"
     1.8 -  unfolding open_dist ball_def mem_Collect_eq Ball_def
     1.9 -  unfolding dist_commute
    1.10 -  apply clarify
    1.11 -  apply (rule_tac x="e - dist xa x" in exI)
    1.12 -  using dist_triangle_alt[where z=x]
    1.13 -  apply (clarsimp simp add: diff_less_iff)
    1.14 -  apply atomize
    1.15 -  apply (erule_tac x="y" in allE)
    1.16 -  apply (erule_tac x="xa" in allE)
    1.17 -  apply arith
    1.18 -  done
    1.19 +lemma open_vimage: (* TODO: move to Topological_Spaces.thy *)
    1.20 +  assumes "open s" and "continuous_on UNIV f"
    1.21 +  shows "open (vimage f s)"
    1.22 +  using assms unfolding continuous_on_open_vimage [OF open_UNIV]
    1.23 +  by simp
    1.24 +
    1.25 +lemma open_ball [intro, simp]: "open (ball x e)"
    1.26 +proof -
    1.27 +  have "open (dist x -` {..<e})"
    1.28 +    by (intro open_vimage open_lessThan continuous_on_intros)
    1.29 +  also have "dist x -` {..<e} = ball x e"
    1.30 +    by auto
    1.31 +  finally show ?thesis .
    1.32 +qed
    1.33  
    1.34  lemma open_contains_ball: "open S \<longleftrightarrow> (\<forall>x\<in>S. \<exists>e>0. ball x e \<subseteq> S)"
    1.35    unfolding open_dist subset_eq mem_ball Ball_def dist_commute ..
    1.36 @@ -1889,7 +1891,6 @@
    1.37  lemma closed_sequential_limits:
    1.38    fixes S :: "'a::first_countable_topology set"
    1.39    shows "closed S \<longleftrightarrow> (\<forall>x l. (\<forall>n. x n \<in> S) \<and> (x ---> l) sequentially \<longrightarrow> l \<in> S)"
    1.40 -  unfolding closed_limpt
    1.41    using closure_sequential [where 'a='a] closure_closed [where 'a='a]
    1.42      closed_limpt [where 'a='a] islimpt_sequential [where 'a='a] mem_delete [where 'a='a]
    1.43    by metis
    1.44 @@ -2129,15 +2130,20 @@
    1.45  
    1.46  subsection {* More properties of closed balls *}
    1.47  
    1.48 +lemma closed_vimage: (* TODO: move to Topological_Spaces.thy *)
    1.49 +  assumes "closed s" and "continuous_on UNIV f"
    1.50 +  shows "closed (vimage f s)"
    1.51 +  using assms unfolding continuous_on_closed_vimage [OF closed_UNIV]
    1.52 +  by simp
    1.53 +
    1.54  lemma closed_cball: "closed (cball x e)"
    1.55 -  unfolding cball_def closed_def
    1.56 -  unfolding Collect_neg_eq [symmetric] not_le
    1.57 -  apply (clarsimp simp add: open_dist, rename_tac y)
    1.58 -  apply (rule_tac x="dist x y - e" in exI, clarsimp)
    1.59 -  apply (rename_tac x')
    1.60 -  apply (cut_tac x=x and y=x' and z=y in dist_triangle)
    1.61 -  apply simp
    1.62 -  done
    1.63 +proof -
    1.64 +  have "closed (dist x -` {..e})"
    1.65 +    by (intro closed_vimage closed_atMost continuous_on_intros)
    1.66 +  also have "dist x -` {..e} = cball x e"
    1.67 +    by auto
    1.68 +  finally show ?thesis .
    1.69 +qed
    1.70  
    1.71  lemma open_contains_cball: "open S \<longleftrightarrow> (\<forall>x\<in>S. \<exists>e>0.  cball x e \<subseteq> S)"
    1.72  proof -
    1.73 @@ -3298,6 +3304,50 @@
    1.74    where "seq_compact S \<longleftrightarrow>
    1.75      (\<forall>f. (\<forall>n. f n \<in> S) \<longrightarrow> (\<exists>l\<in>S. \<exists>r. subseq r \<and> ((f \<circ> r) ---> l) sequentially))"
    1.76  
    1.77 +lemma seq_compactI:
    1.78 +  assumes "\<And>f. \<forall>n. f n \<in> S \<Longrightarrow> \<exists>l\<in>S. \<exists>r. subseq r \<and> ((f \<circ> r) ---> l) sequentially"
    1.79 +  shows "seq_compact S"
    1.80 +  unfolding seq_compact_def using assms by fast
    1.81 +
    1.82 +lemma seq_compactE:
    1.83 +  assumes "seq_compact S" "\<forall>n. f n \<in> S"
    1.84 +  obtains l r where "l \<in> S" "subseq r" "((f \<circ> r) ---> l) sequentially"
    1.85 +  using assms unfolding seq_compact_def by fast
    1.86 +
    1.87 +lemma closed_sequentially: (* TODO: move upwards *)
    1.88 +  assumes "closed s" and "\<forall>n. f n \<in> s" and "f ----> l"
    1.89 +  shows "l \<in> s"
    1.90 +proof (rule ccontr)
    1.91 +  assume "l \<notin> s"
    1.92 +  with `closed s` and `f ----> l` have "eventually (\<lambda>n. f n \<in> - s) sequentially"
    1.93 +    by (fast intro: topological_tendstoD)
    1.94 +  with `\<forall>n. f n \<in> s` show "False"
    1.95 +    by simp
    1.96 +qed
    1.97 +
    1.98 +lemma seq_compact_inter_closed:
    1.99 +  assumes "seq_compact s" and "closed t"
   1.100 +  shows "seq_compact (s \<inter> t)"
   1.101 +proof (rule seq_compactI)
   1.102 +  fix f assume "\<forall>n::nat. f n \<in> s \<inter> t"
   1.103 +  hence "\<forall>n. f n \<in> s" and "\<forall>n. f n \<in> t"
   1.104 +    by simp_all
   1.105 +  from `seq_compact s` and `\<forall>n. f n \<in> s`
   1.106 +  obtain l r where "l \<in> s" and r: "subseq r" and l: "(f \<circ> r) ----> l"
   1.107 +    by (rule seq_compactE)
   1.108 +  from `\<forall>n. f n \<in> t` have "\<forall>n. (f \<circ> r) n \<in> t"
   1.109 +    by simp
   1.110 +  from `closed t` and this and l have "l \<in> t"
   1.111 +    by (rule closed_sequentially)
   1.112 +  with `l \<in> s` and r and l show "\<exists>l\<in>s \<inter> t. \<exists>r. subseq r \<and> (f \<circ> r) ----> l"
   1.113 +    by fast
   1.114 +qed
   1.115 +
   1.116 +lemma seq_compact_closed_subset:
   1.117 +  assumes "closed s" and "s \<subseteq> t" and "seq_compact t"
   1.118 +  shows "seq_compact s"
   1.119 +  using assms seq_compact_inter_closed [of t s] by (simp add: Int_absorb1)
   1.120 +
   1.121  lemma seq_compact_imp_countably_compact:
   1.122    fixes U :: "'a :: first_countable_topology set"
   1.123    assumes "seq_compact U"
   1.124 @@ -3410,16 +3460,6 @@
   1.125      using `x \<in> U` by (auto simp: convergent_def comp_def)
   1.126  qed
   1.127  
   1.128 -lemma seq_compactI:
   1.129 -  assumes "\<And>f. \<forall>n. f n \<in> S \<Longrightarrow> \<exists>l\<in>S. \<exists>r. subseq r \<and> ((f \<circ> r) ---> l) sequentially"
   1.130 -  shows "seq_compact S"
   1.131 -  unfolding seq_compact_def using assms by fast
   1.132 -
   1.133 -lemma seq_compactE:
   1.134 -  assumes "seq_compact S" "\<forall>n. f n \<in> S"
   1.135 -  obtains l r where "l \<in> S" "subseq r" "((f \<circ> r) ---> l) sequentially"
   1.136 -  using assms unfolding seq_compact_def by fast
   1.137 -
   1.138  lemma countably_compact_imp_acc_point:
   1.139    assumes "countably_compact s"
   1.140      and "countable t"
   1.141 @@ -3654,6 +3694,8 @@
   1.142    "\<forall>t. infinite t \<and> t \<subseteq> s \<longrightarrow> (\<exists>x \<in> s. x islimpt t) \<Longrightarrow> bounded s"
   1.143    using compact_imp_bounded unfolding compact_eq_bolzano_weierstrass .
   1.144  
   1.145 +subsection {* Metric spaces with the Heine-Borel property *}
   1.146 +
   1.147  text {*
   1.148    A metric space (or topological vector space) is said to have the
   1.149    Heine-Borel property if every closed and bounded subset is compact.
   1.150 @@ -3678,7 +3720,7 @@
   1.151    from f have fr: "\<forall>n. (f \<circ> r) n \<in> s"
   1.152      by simp
   1.153    have "l \<in> s" using `closed s` fr l
   1.154 -    unfolding closed_sequential_limits by blast
   1.155 +    by (rule closed_sequentially)
   1.156    show "\<exists>l\<in>s. \<exists>r. subseq r \<and> ((f \<circ> r) ---> l) sequentially"
   1.157      using `l \<in> s` r l by blast
   1.158  qed
   1.159 @@ -3859,11 +3901,21 @@
   1.160      using l r by fast
   1.161  qed
   1.162  
   1.163 -subsubsection{* Completeness *}
   1.164 +subsubsection {* Completeness *}
   1.165  
   1.166  definition complete :: "'a::metric_space set \<Rightarrow> bool"
   1.167    where "complete s \<longleftrightarrow> (\<forall>f. (\<forall>n. f n \<in> s) \<and> Cauchy f \<longrightarrow> (\<exists>l\<in>s. f ----> l))"
   1.168  
   1.169 +lemma completeI:
   1.170 +  assumes "\<And>f. \<forall>n. f n \<in> s \<Longrightarrow> Cauchy f \<Longrightarrow> \<exists>l\<in>s. f ----> l"
   1.171 +  shows "complete s"
   1.172 +  using assms unfolding complete_def by fast
   1.173 +
   1.174 +lemma completeE:
   1.175 +  assumes "complete s" and "\<forall>n. f n \<in> s" and "Cauchy f"
   1.176 +  obtains l where "l \<in> s" and "f ----> l"
   1.177 +  using assms unfolding complete_def by fast
   1.178 +
   1.179  lemma compact_imp_complete:
   1.180    assumes "compact s"
   1.181    shows "complete s"
   1.182 @@ -4085,49 +4137,57 @@
   1.183  
   1.184  instance euclidean_space \<subseteq> banach ..
   1.185  
   1.186 -lemma complete_univ: "complete (UNIV :: 'a::complete_space set)"
   1.187 -proof (simp add: complete_def, rule, rule)
   1.188 -  fix f :: "nat \<Rightarrow> 'a"
   1.189 -  assume "Cauchy f"
   1.190 +lemma complete_UNIV: "complete (UNIV :: ('a::complete_space) set)"
   1.191 +proof (rule completeI)
   1.192 +  fix f :: "nat \<Rightarrow> 'a" assume "Cauchy f"
   1.193    then have "convergent f" by (rule Cauchy_convergent)
   1.194 -  then show "\<exists>l. f ----> l" unfolding convergent_def .
   1.195 +  then show "\<exists>l\<in>UNIV. f ----> l" unfolding convergent_def by simp
   1.196  qed
   1.197  
   1.198  lemma complete_imp_closed:
   1.199    assumes "complete s"
   1.200    shows "closed s"
   1.201 -proof -
   1.202 -  {
   1.203 -    fix x
   1.204 -    assume "x islimpt s"
   1.205 -    then obtain f where f: "\<forall>n. f n \<in> s - {x}" "(f ---> x) sequentially"
   1.206 -      unfolding islimpt_sequential by auto
   1.207 -    then obtain l where l: "l\<in>s" "(f ---> l) sequentially"
   1.208 -      using `complete s`[unfolded complete_def] using LIMSEQ_imp_Cauchy[of f x] by auto
   1.209 -    then have "x \<in> s"
   1.210 -      using tendsto_unique[of sequentially f l x] trivial_limit_sequentially f(2) by auto
   1.211 -  }
   1.212 -  then show "closed s" unfolding closed_limpt by auto
   1.213 -qed
   1.214 +proof (unfold closed_sequential_limits, clarify)
   1.215 +  fix f x assume "\<forall>n. f n \<in> s" and "f ----> x"
   1.216 +  from `f ----> x` have "Cauchy f"
   1.217 +    by (rule LIMSEQ_imp_Cauchy)
   1.218 +  with `complete s` and `\<forall>n. f n \<in> s` obtain l where "l \<in> s" and "f ----> l"
   1.219 +    by (rule completeE)
   1.220 +  from `f ----> x` and `f ----> l` have "x = l"
   1.221 +    by (rule LIMSEQ_unique)
   1.222 +  with `l \<in> s` show "x \<in> s"
   1.223 +    by simp
   1.224 +qed
   1.225 +
   1.226 +lemma complete_inter_closed:
   1.227 +  assumes "complete s" and "closed t"
   1.228 +  shows "complete (s \<inter> t)"
   1.229 +proof (rule completeI)
   1.230 +  fix f assume "\<forall>n. f n \<in> s \<inter> t" and "Cauchy f"
   1.231 +  then have "\<forall>n. f n \<in> s" and "\<forall>n. f n \<in> t"
   1.232 +    by simp_all
   1.233 +  from `complete s` obtain l where "l \<in> s" and "f ----> l"
   1.234 +    using `\<forall>n. f n \<in> s` and `Cauchy f` by (rule completeE)
   1.235 +  from `closed t` and `\<forall>n. f n \<in> t` and `f ----> l` have "l \<in> t"
   1.236 +    by (rule closed_sequentially)
   1.237 +  with `l \<in> s` and `f ----> l` show "\<exists>l\<in>s \<inter> t. f ----> l"
   1.238 +    by fast
   1.239 +qed
   1.240 +
   1.241 +lemma complete_closed_subset:
   1.242 +  assumes "closed s" and "s \<subseteq> t" and "complete t"
   1.243 +  shows "complete s"
   1.244 +  using assms complete_inter_closed [of t s] by (simp add: Int_absorb1)
   1.245  
   1.246  lemma complete_eq_closed:
   1.247 -  fixes s :: "'a::complete_space set"
   1.248 -  shows "complete s \<longleftrightarrow> closed s" (is "?lhs = ?rhs")
   1.249 +  fixes s :: "('a::complete_space) set"
   1.250 +  shows "complete s \<longleftrightarrow> closed s"
   1.251  proof
   1.252 -  assume ?lhs
   1.253 -  then show ?rhs by (rule complete_imp_closed)
   1.254 +  assume "closed s" then show "complete s"
   1.255 +    using subset_UNIV complete_UNIV by (rule complete_closed_subset)
   1.256  next
   1.257 -  assume ?rhs
   1.258 -  {
   1.259 -    fix f
   1.260 -    assume as:"\<forall>n::nat. f n \<in> s" "Cauchy f"
   1.261 -    then obtain l where "(f ---> l) sequentially"
   1.262 -      using complete_univ[unfolded complete_def, THEN spec[where x=f]] by auto
   1.263 -    then have "\<exists>l\<in>s. (f ---> l) sequentially"
   1.264 -      using `?rhs`[unfolded closed_sequential_limits, THEN spec[where x=f], THEN spec[where x=l]]
   1.265 -      using as(1) by auto
   1.266 -  }
   1.267 -  then show ?lhs unfolding complete_def by auto
   1.268 +  assume "complete s" then show "closed s"
   1.269 +    by (rule complete_imp_closed)
   1.270  qed
   1.271  
   1.272  lemma convergent_eq_cauchy:
   1.273 @@ -4142,13 +4202,13 @@
   1.274  
   1.275  lemma compact_cball[simp]:
   1.276    fixes x :: "'a::heine_borel"
   1.277 -  shows "compact(cball x e)"
   1.278 +  shows "compact (cball x e)"
   1.279    using compact_eq_bounded_closed bounded_cball closed_cball
   1.280    by blast
   1.281  
   1.282  lemma compact_frontier_bounded[intro]:
   1.283    fixes s :: "'a::heine_borel set"
   1.284 -  shows "bounded s \<Longrightarrow> compact(frontier s)"
   1.285 +  shows "bounded s \<Longrightarrow> compact (frontier s)"
   1.286    unfolding frontier_def
   1.287    using compact_eq_bounded_closed
   1.288    by blast
   1.289 @@ -4168,68 +4228,51 @@
   1.290  subsection {* Bounded closed nest property (proof does not use Heine-Borel) *}
   1.291  
   1.292  lemma bounded_closed_nest:
   1.293 -  assumes "\<forall>n. closed(s n)"
   1.294 -    and "\<forall>n. (s n \<noteq> {})"
   1.295 -    and "(\<forall>m n. m \<le> n --> s n \<subseteq> s m)"
   1.296 -    and "bounded(s 0)"
   1.297 -  shows "\<exists>a::'a::heine_borel. \<forall>n::nat. a \<in> s(n)"
   1.298 +  fixes s :: "nat \<Rightarrow> ('a::heine_borel) set"
   1.299 +  assumes "\<forall>n. closed (s n)"
   1.300 +    and "\<forall>n. s n \<noteq> {}"
   1.301 +    and "\<forall>m n. m \<le> n \<longrightarrow> s n \<subseteq> s m"
   1.302 +    and "bounded (s 0)"
   1.303 +  shows "\<exists>a. \<forall>n. a \<in> s n"
   1.304  proof -
   1.305 -  from assms(2) obtain x where x:"\<forall>n::nat. x n \<in> s n"
   1.306 -    using choice[of "\<lambda>n x. x\<in> s n"] by auto
   1.307 -  from assms(4,1) have *:"seq_compact (s 0)"
   1.308 -    using bounded_closed_imp_seq_compact[of "s 0"] by auto
   1.309 -
   1.310 -  then obtain l r where lr:"l\<in>s 0" "subseq r" "((x \<circ> r) ---> l) sequentially"
   1.311 -    unfolding seq_compact_def
   1.312 -    apply (erule_tac x=x in allE)
   1.313 -    using x using assms(3)
   1.314 -    apply blast
   1.315 -    done
   1.316 -
   1.317 -  {
   1.318 +  from assms(2) obtain x where x: "\<forall>n. x n \<in> s n"
   1.319 +    using choice[of "\<lambda>n x. x \<in> s n"] by auto
   1.320 +  from assms(4,1) have "seq_compact (s 0)"
   1.321 +    by (simp add: bounded_closed_imp_seq_compact)
   1.322 +  then obtain l r where lr: "l \<in> s 0" "subseq r" "(x \<circ> r) ----> l"
   1.323 +    using x and assms(3) unfolding seq_compact_def by blast
   1.324 +  have "\<forall>n. l \<in> s n"
   1.325 +  proof
   1.326      fix n :: nat
   1.327 -    {
   1.328 -      fix e :: real
   1.329 -      assume "e>0"
   1.330 -      with lr(3) obtain N where N:"\<forall>m\<ge>N. dist ((x \<circ> r) m) l < e"
   1.331 -        unfolding LIMSEQ_def by auto
   1.332 -      then have "dist ((x \<circ> r) (max N n)) l < e" by auto
   1.333 -      moreover
   1.334 -      have "r (max N n) \<ge> n" using lr(2) using seq_suble[of r "max N n"]
   1.335 -        by auto
   1.336 -      then have "(x \<circ> r) (max N n) \<in> s n"
   1.337 -        using x
   1.338 -        apply (erule_tac x=n in allE)
   1.339 -        using x
   1.340 -        apply (erule_tac x="r (max N n)" in allE)
   1.341 -        using assms(3)
   1.342 -        apply (erule_tac x=n in allE)
   1.343 -        apply (erule_tac x="r (max N n)" in allE)
   1.344 -        apply auto
   1.345 -        done
   1.346 -      ultimately have "\<exists>y\<in>s n. dist y l < e"
   1.347 -        by auto
   1.348 -    }
   1.349 -    then have "l \<in> s n"
   1.350 -      using closed_approachable[of "s n" l] assms(1) by blast
   1.351 -  }
   1.352 -  then show ?thesis by auto
   1.353 +    have "closed (s n)"
   1.354 +      using assms(1) by simp
   1.355 +    moreover have "\<forall>i. (x \<circ> r) i \<in> s i"
   1.356 +      using x and assms(3) and lr(2) [THEN seq_suble] by auto
   1.357 +    then have "\<forall>i. (x \<circ> r) (i + n) \<in> s n"
   1.358 +      using assms(3) by (fast intro!: le_add2)
   1.359 +    moreover have "(\<lambda>i. (x \<circ> r) (i + n)) ----> l"
   1.360 +      using lr(3) by (rule LIMSEQ_ignore_initial_segment)
   1.361 +    ultimately show "l \<in> s n"
   1.362 +      by (rule closed_sequentially)
   1.363 +  qed
   1.364 +  then show ?thesis ..
   1.365  qed
   1.366  
   1.367  text {* Decreasing case does not even need compactness, just completeness. *}
   1.368  
   1.369  lemma decreasing_closed_nest:
   1.370 +  fixes s :: "nat \<Rightarrow> ('a::complete_space) set"
   1.371    assumes
   1.372 -    "\<forall>n. closed(s n)"
   1.373 -    "\<forall>n. (s n \<noteq> {})"
   1.374 -    "\<forall>m n. m \<le> n --> s n \<subseteq> s m"
   1.375 -    "\<forall>e>0. \<exists>n. \<forall>x \<in> (s n). \<forall> y \<in> (s n). dist x y < e"
   1.376 -  shows "\<exists>a::'a::complete_space. \<forall>n::nat. a \<in> s n"
   1.377 -proof-
   1.378 -  have "\<forall>n. \<exists> x. x\<in>s n"
   1.379 +    "\<forall>n. closed (s n)"
   1.380 +    "\<forall>n. s n \<noteq> {}"
   1.381 +    "\<forall>m n. m \<le> n \<longrightarrow> s n \<subseteq> s m"
   1.382 +    "\<forall>e>0. \<exists>n. \<forall>x\<in>s n. \<forall>y\<in>s n. dist x y < e"
   1.383 +  shows "\<exists>a. \<forall>n. a \<in> s n"
   1.384 +proof -
   1.385 +  have "\<forall>n. \<exists>x. x \<in> s n"
   1.386      using assms(2) by auto
   1.387    then have "\<exists>t. \<forall>n. t n \<in> s n"
   1.388 -    using choice[of "\<lambda> n x. x \<in> s n"] by auto
   1.389 +    using choice[of "\<lambda>n x. x \<in> s n"] by auto
   1.390    then obtain t where t: "\<forall>n. t n \<in> s n" by auto
   1.391    {
   1.392      fix e :: real
   1.393 @@ -4250,7 +4293,7 @@
   1.394    then have "Cauchy t"
   1.395      unfolding cauchy_def by auto
   1.396    then obtain l where l:"(t ---> l) sequentially"
   1.397 -    using complete_univ unfolding complete_def by auto
   1.398 +    using complete_UNIV unfolding complete_def by auto
   1.399    {
   1.400      fix n :: nat
   1.401      {
   1.402 @@ -4285,7 +4328,7 @@
   1.403    assumes
   1.404      "\<forall>n. closed(s n)"
   1.405      "\<forall>n. s n \<noteq> {}"
   1.406 -    "\<forall>m n. m \<le> n --> s n \<subseteq> s m"
   1.407 +    "\<forall>m n. m \<le> n \<longrightarrow> s n \<subseteq> s m"
   1.408      "\<forall>e>0. \<exists>n. \<forall>x \<in> (s n). \<forall> y\<in>(s n). dist x y < e"
   1.409    shows "\<exists>a. \<Inter>(range s) = {a}"
   1.410  proof -
   1.411 @@ -7350,14 +7393,14 @@
   1.412      fix y
   1.413      assume "a \<le> y" "y \<le> b" "m > 0"
   1.414      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"
   1.415 -      unfolding eucl_le[where 'a='a] by (auto simp: inner_simps)
   1.416 +      unfolding eucl_le[where 'a='a] by (auto simp: inner_distrib)
   1.417    }
   1.418    moreover
   1.419    {
   1.420      fix y
   1.421      assume "a \<le> y" "y \<le> b" "m < 0"
   1.422      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"
   1.423 -      unfolding eucl_le[where 'a='a] by (auto simp add: mult_left_mono_neg inner_simps)
   1.424 +      unfolding eucl_le[where 'a='a] by (auto simp add: mult_left_mono_neg inner_distrib)
   1.425    }
   1.426    moreover
   1.427    {
   1.428 @@ -7366,7 +7409,7 @@
   1.429      then have "y \<in> (\<lambda>x. m *\<^sub>R x + c) ` {a..b}"
   1.430        unfolding image_iff Bex_def mem_interval eucl_le[where 'a='a]
   1.431        apply (intro exI[where x="(1 / m) *\<^sub>R (y - c)"])
   1.432 -      apply (auto simp add: pos_le_divide_eq pos_divide_le_eq mult_commute diff_le_iff inner_simps)
   1.433 +      apply (auto simp add: pos_le_divide_eq pos_divide_le_eq mult_commute diff_le_iff inner_distrib inner_diff_left)
   1.434        done
   1.435    }
   1.436    moreover
   1.437 @@ -7376,7 +7419,7 @@
   1.438      then have "y \<in> (\<lambda>x. m *\<^sub>R x + c) ` {a..b}"
   1.439        unfolding image_iff Bex_def mem_interval eucl_le[where 'a='a]
   1.440        apply (intro exI[where x="(1 / m) *\<^sub>R (y - c)"])
   1.441 -      apply (auto simp add: neg_le_divide_eq neg_divide_le_eq mult_commute diff_le_iff inner_simps)
   1.442 +      apply (auto simp add: neg_le_divide_eq neg_divide_le_eq mult_commute diff_le_iff inner_distrib inner_diff_left)
   1.443        done
   1.444    }
   1.445    ultimately show ?thesis using False by auto