author paulson Sun, 06 May 2018 23:59:14 +0100 changeset 68097 5f3cffe16311 parent 68094 0b66aca9c965 (current diff) parent 68096 e58c9ac761cb (diff) child 68098 e2bb1d95cbd0 child 68101 0699a0bacc50 child 68109 cebf36c14226 child 68120 2f161c6910f7
merged
```--- a/src/HOL/Analysis/Derivative.thy	Sun May 06 23:30:34 2018 +0200
+++ b/src/HOL/Analysis/Derivative.thy	Sun May 06 23:59:14 2018 +0100
@@ -72,8 +72,8 @@
by blast

lemma has_derivative_within_open:
-  "a \<in> s \<Longrightarrow> open s \<Longrightarrow>
-    (f has_derivative f') (at a within s) \<longleftrightarrow> (f has_derivative f') (at a)"
+  "a \<in> S \<Longrightarrow> open S \<Longrightarrow>
+    (f has_derivative f') (at a within S) \<longleftrightarrow> (f has_derivative f') (at a)"
by (simp only: at_within_interior interior_open)

lemma has_derivative_right:
@@ -98,8 +98,8 @@
lemmas DERIV_within_iff = has_field_derivative_iff

lemma DERIV_caratheodory_within:
-  "(f has_field_derivative l) (at x within s) \<longleftrightarrow>
-   (\<exists>g. (\<forall>z. f z - f x = g z * (z - x)) \<and> continuous (at x within s) g \<and> g x = l)"
+  "(f has_field_derivative l) (at x within S) \<longleftrightarrow>
+   (\<exists>g. (\<forall>z. f z - f x = g z * (z - x)) \<and> continuous (at x within S) g \<and> g x = l)"
(is "?lhs = ?rhs")
proof
assume ?lhs
@@ -107,14 +107,14 @@
proof (intro exI conjI)
let ?g = "(%z. if z = x then l else (f z - f x) / (z-x))"
show "\<forall>z. f z - f x = ?g z * (z-x)" by simp
-    show "continuous (at x within s) ?g" using \<open>?lhs\<close>
+    show "continuous (at x within S) ?g" using \<open>?lhs\<close>
by (auto simp add: continuous_within DERIV_within_iff cong: Lim_cong_within)
show "?g x = l" by simp
qed
next
assume ?rhs
then obtain g where
-    "(\<forall>z. f z - f x = g z * (z-x))" and "continuous (at x within s) g" and "g x = l" by blast
+    "(\<forall>z. f z - f x = g z * (z-x))" and "continuous (at x within S) g" and "g x = l" by blast
thus ?lhs
by (auto simp add: continuous_within DERIV_within_iff cong: Lim_cong_within)
qed
@@ -330,18 +330,23 @@
using has_derivative_compose[of f f' x UNIV g g']

+lemma has_vector_derivative_within_open:
+  "a \<in> S \<Longrightarrow> open S \<Longrightarrow>
+    (f has_vector_derivative f') (at a within S) \<longleftrightarrow> (f has_vector_derivative f') (at a)"
+  by (simp only: at_within_interior interior_open)
+
lemma field_vector_diff_chain_within:
- assumes Df: "(f has_vector_derivative f') (at x within s)"
-     and Dg: "(g has_field_derivative g') (at (f x) within f`s)"
- shows "((g \<circ> f) has_vector_derivative (f' * g')) (at x within s)"
+ assumes Df: "(f has_vector_derivative f') (at x within S)"
+     and Dg: "(g has_field_derivative g') (at (f x) within f ` S)"
+ shows "((g \<circ> f) has_vector_derivative (f' * g')) (at x within S)"
using diff_chain_within[OF Df[unfolded has_vector_derivative_def]
Dg [unfolded has_field_derivative_def]]
by (auto simp: o_def mult.commute has_vector_derivative_def)

lemma vector_derivative_diff_chain_within:
-  assumes Df: "(f has_vector_derivative f') (at x within s)"
-     and Dg: "(g has_derivative g') (at (f x) within f`s)"
-  shows "((g \<circ> f) has_vector_derivative (g' f')) (at x within s)"
+  assumes Df: "(f has_vector_derivative f') (at x within S)"
+     and Dg: "(g has_derivative g') (at (f x) within f`S)"
+  shows "((g \<circ> f) has_vector_derivative (g' f')) (at x within S)"
using diff_chain_within[OF Df[unfolded has_vector_derivative_def] Dg]
linear.scaleR[OF has_derivative_linear[OF Dg]]
unfolding has_vector_derivative_def o_def
@@ -357,8 +362,8 @@
by (meson diff_chain_at)

lemma differentiable_chain_within:
-  "f differentiable (at x within s) \<Longrightarrow>
-    g differentiable (at(f x) within (f ` s)) \<Longrightarrow> (g \<circ> f) differentiable (at x within s)"
+  "f differentiable (at x within S) \<Longrightarrow>
+    g differentiable (at(f x) within (f ` S)) \<Longrightarrow> (g \<circ> f) differentiable (at x within S)"
unfolding differentiable_def
by (meson diff_chain_within)
```
```--- a/src/HOL/Analysis/Interval_Integral.thy	Sun May 06 23:30:34 2018 +0200
+++ b/src/HOL/Analysis/Interval_Integral.thy	Sun May 06 23:59:14 2018 +0100
@@ -12,20 +12,6 @@
"(\<And>x. x \<in> S \<Longrightarrow> (f has_vector_derivative f' x) (at x within S)) \<Longrightarrow> continuous_on S f"
by (auto simp: continuous_on_eq_continuous_within intro!: has_vector_derivative_continuous)

-lemma has_vector_derivative_weaken:
-  fixes x D and f g s t
-  assumes f: "(f has_vector_derivative D) (at x within t)"
-    and "x \<in> s" "s \<subseteq> t"
-    and "\<And>x. x \<in> s \<Longrightarrow> f x = g x"
-  shows "(g has_vector_derivative D) (at x within s)"
-proof -
-  have "(f has_vector_derivative D) (at x within s) \<longleftrightarrow> (g has_vector_derivative D) (at x within s)"
-    unfolding has_vector_derivative_def has_derivative_iff_norm
-    using assms by (intro conj_cong Lim_cong_within refl) auto
-  then show ?thesis
-    using has_vector_derivative_within_subset[OF f \<open>s \<subseteq> t\<close>] by simp
-qed
-
definition "einterval a b = {x. a < ereal x \<and> ereal x < b}"

lemma einterval_eq[simp]:
@@ -36,7 +22,7 @@
by (auto simp: einterval_def)

lemma einterval_same: "einterval a a = {}"
-  by (auto simp add: einterval_def)
+  by (auto simp: einterval_def)

lemma einterval_iff: "x \<in> einterval a b \<longleftrightarrow> a < ereal x \<and> ereal x < b"
@@ -59,21 +45,15 @@
lemma ereal_incseq_approx:
fixes a b :: ereal
assumes "a < b"
-  obtains X :: "nat \<Rightarrow> real" where
-    "incseq X" "\<And>i. a < X i" "\<And>i. X i < b" "X \<longlonglongrightarrow> b"
+  obtains X :: "nat \<Rightarrow> real" where "incseq X" "\<And>i. a < X i" "\<And>i. X i < b" "X \<longlonglongrightarrow> b"
proof (cases b)
case PInf
with \<open>a < b\<close> have "a = -\<infinity> \<or> (\<exists>r. a = ereal r)"
by (cases a) auto
moreover have "(\<lambda>x. ereal (real (Suc x))) \<longlonglongrightarrow> \<infinity>"
-      apply (subst LIMSEQ_Suc_iff)
-      using nat_ceiling_le_eq by blast
+    by (simp add: Lim_PInfty LIMSEQ_Suc_iff) (metis le_SucI of_nat_Suc of_nat_mono order_trans real_arch_simple)
moreover have "\<And>r. (\<lambda>x. ereal (r + real (Suc x))) \<longlonglongrightarrow> \<infinity>"
-    apply (subst LIMSEQ_Suc_iff)
-    apply (subst Lim_PInfty)
-    apply (metis add.commute diff_le_eq nat_ceiling_le_eq ereal_less_eq(3))
-    done
ultimately show thesis
by (intro that[of "\<lambda>i. real_of_ereal a + Suc i"])
(auto simp: incseq_def PInf)
@@ -87,16 +67,15 @@
by (intro mult_strict_left_mono) auto
with \<open>a < b\<close> a' have "\<And>i. a < ereal (b' - d / real (Suc (Suc i)))"
by (cases a) (auto simp: real d_def field_simps)
-  moreover have "(\<lambda>i. b' - d / Suc (Suc i)) \<longlonglongrightarrow> b'"
-    apply (subst filterlim_sequentially_Suc)
-    apply (subst filterlim_sequentially_Suc)
-    apply (rule tendsto_eq_intros)
-    apply (auto intro!: tendsto_divide_0[OF tendsto_const] filterlim_sup1
-                simp: at_infinity_eq_at_top_bot filterlim_real_sequentially)
-    done
+  moreover
+  have "(\<lambda>i. b' - d / real i) \<longlonglongrightarrow> b'"
+    by (force intro: tendsto_eq_intros tendsto_divide_0[OF tendsto_const] filterlim_sup1
+              simp: at_infinity_eq_at_top_bot filterlim_real_sequentially)
+  then have "(\<lambda>i. b' - d / Suc (Suc i)) \<longlonglongrightarrow> b'"
+    by (blast intro: dest: filterlim_sequentially_Suc [THEN iffD2])
ultimately show thesis
by (intro that[of "\<lambda>i. b' - d / Suc (Suc i)"])
-       (auto simp add: real incseq_def intro!: divide_left_mono)
+       (auto simp: real incseq_def intro!: divide_left_mono)
qed (insert \<open>a < b\<close>, auto)

lemma ereal_decseq_approx:
@@ -109,7 +88,7 @@
from ereal_incseq_approx[OF this] guess X .
then show thesis
apply (intro that[of "\<lambda>i. - X i"])
-    apply (auto simp add: decseq_def incseq_def reorient: uminus_ereal.simps)
+    apply (auto simp: decseq_def incseq_def reorient: uminus_ereal.simps)
apply (metis ereal_minus_less_minus ereal_uminus_uminus ereal_Lim_uminus)+
done
qed
@@ -204,7 +183,7 @@
shows "interval_lebesgue_integrable M a b (\<lambda>x. f x + g x)" and
"interval_lebesgue_integral M a b (\<lambda>x. f x + g x) =
interval_lebesgue_integral M a b f + interval_lebesgue_integral M a b g"
-using assms by (auto simp add: interval_lebesgue_integral_def interval_lebesgue_integrable_def
+using assms by (auto simp: interval_lebesgue_integral_def interval_lebesgue_integrable_def
field_simps)

lemma interval_lebesgue_integral_diff [intro, simp]:
@@ -214,7 +193,7 @@
shows "interval_lebesgue_integrable M a b (\<lambda>x. f x - g x)" and
"interval_lebesgue_integral M a b (\<lambda>x. f x - g x) =
interval_lebesgue_integral M a b f - interval_lebesgue_integral M a b g"
-using assms by (auto simp add: interval_lebesgue_integral_def interval_lebesgue_integrable_def
+using assms by (auto simp: interval_lebesgue_integral_def interval_lebesgue_integrable_def
field_simps)

lemma interval_lebesgue_integrable_mult_right [intro, simp]:
@@ -255,31 +234,31 @@

lemma interval_lebesgue_integral_uminus:
"interval_lebesgue_integral M a b (\<lambda>x. - f x) = - interval_lebesgue_integral M a b f"
-  by (auto simp add: interval_lebesgue_integral_def interval_lebesgue_integrable_def set_lebesgue_integral_def)
+  by (auto simp: interval_lebesgue_integral_def interval_lebesgue_integrable_def set_lebesgue_integral_def)

lemma interval_lebesgue_integral_of_real:
"interval_lebesgue_integral M a b (\<lambda>x. complex_of_real (f x)) =
of_real (interval_lebesgue_integral M a b f)"
unfolding interval_lebesgue_integral_def
-  by (auto simp add: interval_lebesgue_integral_def set_integral_complex_of_real)
+  by (auto simp: interval_lebesgue_integral_def set_integral_complex_of_real)

lemma interval_lebesgue_integral_le_eq:
fixes a b f
assumes "a \<le> b"
shows "interval_lebesgue_integral M a b f = (LINT x : einterval a b | M. f x)"
-using assms by (auto simp add: interval_lebesgue_integral_def)
+using assms by (auto simp: interval_lebesgue_integral_def)

lemma interval_lebesgue_integral_gt_eq:
fixes a b f
assumes "a > b"
shows "interval_lebesgue_integral M a b f = -(LINT x : einterval b a | M. f x)"
-using assms by (auto simp add: interval_lebesgue_integral_def less_imp_le einterval_def)
+using assms by (auto simp: interval_lebesgue_integral_def less_imp_le einterval_def)

lemma interval_lebesgue_integral_gt_eq':
fixes a b f
assumes "a > b"
shows "interval_lebesgue_integral M a b f = - interval_lebesgue_integral M b a f"
-using assms by (auto simp add: interval_lebesgue_integral_def less_imp_le einterval_def)
+using assms by (auto simp: interval_lebesgue_integral_def less_imp_le einterval_def)

lemma interval_integral_endpoints_same [simp]: "(LBINT x=a..a. f x) = 0"
by (simp add: interval_lebesgue_integral_def set_lebesgue_integral_def einterval_same)
@@ -296,7 +275,7 @@
"(LBINT x=a..b. f x) = (LBINT x=-b..-a. f (-x))"
proof (induct a b rule: linorder_wlog)
case (sym a b) then show ?case
-    by (auto simp add: interval_lebesgue_integral_def interval_integrable_endpoints_reverse
+    by (auto simp: interval_lebesgue_integral_def interval_integrable_endpoints_reverse
split: if_split_asm)
next
case (le a b)
@@ -328,7 +307,7 @@

lemma interval_integral_zero [simp]:
fixes a b :: ereal
-  shows"LBINT x=a..b. 0 = 0"
+  shows "LBINT x=a..b. 0 = 0"
unfolding interval_lebesgue_integral_def set_lebesgue_integral_def einterval_eq
by simp

@@ -336,7 +315,7 @@
fixes a b c :: real
shows "interval_lebesgue_integrable lborel a b (\<lambda>x. c)" and "LBINT x=a..b. c = c * (b - a)"
unfolding interval_lebesgue_integral_def interval_lebesgue_integrable_def einterval_eq
-  by (auto simp add: less_imp_le field_simps measure_def set_integrable_def set_lebesgue_integral_def)
+  by (auto simp: less_imp_le field_simps measure_def set_integrable_def set_lebesgue_integral_def)

lemma interval_integral_cong_AE:
assumes [measurable]: "f \<in> borel_measurable borel" "g \<in> borel_measurable borel"
@@ -369,7 +348,7 @@
"f \<in> borel_measurable lborel \<Longrightarrow> g \<in> borel_measurable lborel \<Longrightarrow>
AE x \<in> einterval (min a b) (max a b) in lborel. f x = g x \<Longrightarrow>
interval_lebesgue_integrable lborel a b f = interval_lebesgue_integrable lborel a b g"
-  apply (simp add: interval_lebesgue_integrable_def )
apply (intro conjI impI set_integrable_cong_AE)
apply (auto simp: min_def max_def)
done
@@ -410,11 +389,11 @@

lemma interval_integral_Ioi:
"\<bar>a\<bar> < \<infinity> \<Longrightarrow> (LBINT x=a..\<infinity>. f x) = (LBINT x : {real_of_ereal a <..}. f x)"
-  by (auto simp add: interval_lebesgue_integral_def einterval_iff)
+  by (auto simp: interval_lebesgue_integral_def einterval_iff)

lemma interval_integral_Ioo:
"a \<le> b \<Longrightarrow> \<bar>a\<bar> < \<infinity> ==> \<bar>b\<bar> < \<infinity> \<Longrightarrow> (LBINT x=a..b. f x) = (LBINT x : {real_of_ereal a <..< real_of_ereal b}. f x)"
-  by (auto simp add: interval_lebesgue_integral_def einterval_iff)
+  by (auto simp: interval_lebesgue_integral_def einterval_iff)

lemma interval_integral_discrete_difference:
fixes f :: "real \<Rightarrow> 'b::{banach, second_countable_topology}" and a b :: ereal
@@ -547,7 +526,7 @@
using f_measurable set_borel_measurable_def by blast
have "(LBINT x=a..b. f x) = lebesgue_integral lborel (\<lambda>x. indicator (einterval a b) x *\<^sub>R f x)"
using assms by (simp add: interval_lebesgue_integral_def set_lebesgue_integral_def less_imp_le)
-  also have "... = C"
+  also have "\<dots> = C"
by (rule integral_monotone_convergence [OF 1 2 3 4 5])
finally show "(LBINT x=a..b. f x) = C" .
show "set_integrable lborel (einterval a b) f"
@@ -601,14 +580,6 @@
TODO: make the older versions corollaries of these (using continuous_at_imp_continuous_on, etc.)
*)

-(*
-TODO: many proofs below require inferences like
-
-  a < ereal x \<Longrightarrow> x < y \<Longrightarrow> a < ereal y
-
-where x and y are real. These should be better automated.
-*)
-
lemma interval_integral_FTC_finite:
fixes f F :: "real \<Rightarrow> 'a::euclidean_space" and a b :: real
assumes f: "continuous_on {min a b..max a b} f"
@@ -619,7 +590,7 @@
case True
have "(LBINT x=a..b. f x) = (LBINT x. indicat_real {a..b} x *\<^sub>R f x)"
by (simp add: True interval_integral_Icc set_lebesgue_integral_def)
-  also have "... = F b - F a"
+  also have "\<dots> = F b - F a"
proof (rule integral_FTC_atLeastAtMost [OF True])
show "continuous_on {a..b} f"
using True f by linarith
@@ -633,7 +604,7 @@
by simp
have "- interval_lebesgue_integral lborel (ereal b) (ereal a) f = - (LBINT x. indicat_real {b..a} x *\<^sub>R f x)"
by (simp add: \<open>b \<le> a\<close> interval_integral_Icc set_lebesgue_integral_def)
-  also have "... = F b - F a"
+  also have "\<dots> = F b - F a"
proof (subst integral_FTC_atLeastAtMost [OF \<open>b \<le> a\<close>])
show "continuous_on {b..a} f"
using False f by linarith
@@ -646,7 +617,6 @@
qed

-
lemma interval_integral_FTC_nonneg:
fixes f F :: "real \<Rightarrow> real" and a b :: ereal
assumes "a < b"
@@ -659,14 +629,18 @@
"set_integrable lborel (einterval a b) f"
"(LBINT x=a..b. f x) = B - A"
proof -
-  from einterval_Icc_approximation[OF \<open>a < b\<close>] guess u l . note approx = this
+  obtain u l where approx:
+    "einterval a b = (\<Union>i. {l i .. u i})"
+    "incseq u" "decseq l" "\<And>i. l i < u i" "\<And>i. a < l i" "\<And>i. u i < b"
+    "l \<longlonglongrightarrow> a" "u \<longlonglongrightarrow> b"
+    by (blast intro: einterval_Icc_approximation[OF \<open>a < b\<close>])
have [simp]: "\<And>x i. l i \<le> x \<Longrightarrow> a < ereal x"
by (rule order_less_le_trans, rule approx, force)
have [simp]: "\<And>x i. x \<le> u i \<Longrightarrow> ereal x < b"
by (rule order_le_less_trans, subst ereal_less_eq(3), assumption, rule approx)
have FTCi: "\<And>i. (LBINT x=l i..u i. f x) = F (u i) - F (l i)"
using assms approx apply (intro interval_integral_FTC_finite)
-    apply (auto simp add: less_imp_le min_def max_def
+    apply (auto simp: less_imp_le min_def max_def
has_field_derivative_iff_has_vector_derivative[symmetric])
apply (rule continuous_at_imp_continuous_on, auto intro!: f)
by (rule DERIV_subset [OF F], auto)
@@ -705,23 +679,30 @@
assumes B: "((F \<circ> real_of_ereal) \<longlongrightarrow> B) (at_left b)"
shows "(LBINT x=a..b. f x) = B - A"
proof -
-  from einterval_Icc_approximation[OF \<open>a < b\<close>] guess u l . note approx = this
+  obtain u l where approx:
+    "einterval a b = (\<Union>i. {l i .. u i})"
+    "incseq u" "decseq l" "\<And>i. l i < u i" "\<And>i. a < l i" "\<And>i. u i < b"
+    "l \<longlonglongrightarrow> a" "u \<longlonglongrightarrow> b"
+    by (blast intro: einterval_Icc_approximation[OF \<open>a < b\<close>])
have [simp]: "\<And>x i. l i \<le> x \<Longrightarrow> a < ereal x"
by (rule order_less_le_trans, rule approx, force)
have [simp]: "\<And>x i. x \<le> u i \<Longrightarrow> ereal x < b"
by (rule order_le_less_trans, subst ereal_less_eq(3), assumption, rule approx)
have FTCi: "\<And>i. (LBINT x=l i..u i. f x) = F (u i) - F (l i)"
using assms approx
-    by (auto simp add: less_imp_le min_def max_def
+    by (auto simp: less_imp_le min_def max_def
intro!: f continuous_at_imp_continuous_on interval_integral_FTC_finite
intro: has_vector_derivative_at_within)
have "(\<lambda>i. LBINT x=l i..u i. f x) \<longlonglongrightarrow> B - A"
-    apply (subst FTCi)
-    apply (intro tendsto_intros)
-    using B approx unfolding tendsto_at_iff_sequentially comp_def
-    apply (elim allE[of _ "\<lambda>i. ereal (u i)"], auto)
-    using A approx unfolding tendsto_at_iff_sequentially comp_def
-    by (elim allE[of _ "\<lambda>i. ereal (l i)"], auto)
+    unfolding FTCi
+  proof (intro tendsto_intros)
+    show "(\<lambda>x. F (l x)) \<longlonglongrightarrow> A"
+      using A approx unfolding tendsto_at_iff_sequentially comp_def
+      by (elim allE[of _ "\<lambda>i. ereal (l i)"], auto)
+    show "(\<lambda>x. F (u x)) \<longlonglongrightarrow> B"
+      using B approx unfolding tendsto_at_iff_sequentially comp_def
+      by (elim allE[of _ "\<lambda>i. ereal (u i)"], auto)
+  qed
moreover have "(\<lambda>i. LBINT x=l i..u i. f x) \<longlonglongrightarrow> (LBINT x=a..b. f x)"
by (rule interval_integral_Icc_approx_integrable [OF \<open>a < b\<close> approx f_integrable])
ultimately show ?thesis
@@ -745,8 +726,8 @@
have intf: "set_integrable lborel {a..b} f"
by (rule borel_integrable_atLeastAtMost', rule contf)
have "((\<lambda>u. integral {a..u} f) has_vector_derivative f x) (at x within {a..b})"
-    apply (intro integral_has_vector_derivative)
-    using \<open>a \<le> x\<close> \<open>x \<le> b\<close> by (intro continuous_on_subset [OF contf], auto)
+    using \<open>a \<le> x\<close> \<open>x \<le> b\<close>
+    by (auto intro: integral_has_vector_derivative continuous_on_subset [OF contf])
then have "((\<lambda>u. integral {a..u} f) has_vector_derivative (f x)) (at x within {a..b})"
by simp
then have "(?F has_vector_derivative (f x)) (at x within {a..b})"
@@ -760,8 +741,8 @@
then show "(LBINT y=c..a. f y) + (LBINT y=a..u. f y) = (LBINT y=c..u. f y)"
using assms
apply (intro interval_integral_sum)
-      apply (auto simp add: interval_lebesgue_integrable_def simp del: real_scaleR_def)
-      by (rule set_integrable_subset [OF intf], auto simp add: min_def max_def)
+      apply (auto simp: interval_lebesgue_integrable_def simp del: real_scaleR_def)
+      by (rule set_integrable_subset [OF intf], auto simp: min_def max_def)
qed (insert assms, auto)
qed

@@ -771,7 +752,7 @@
shows "\<exists>F. \<forall>x :: real. a < x \<longrightarrow> x < b \<longrightarrow> (F has_vector_derivative f x) (at x)"
proof -
from einterval_nonempty [OF \<open>a < b\<close>] obtain c :: real where [simp]: "a < c" "c < b"
-    by (auto simp add: einterval_def)
+    by (auto simp: einterval_def)
let ?F = "(\<lambda>u. LBINT y=c..u. f y)"
show ?thesis
proof (rule exI, clarsimp)
@@ -779,22 +760,24 @@
assume [simp]: "a < x" "x < b"
have 1: "a < min c x" by simp
from einterval_nonempty [OF 1] obtain d :: real where [simp]: "a < d" "d < c" "d < x"
-      by (auto simp add: einterval_def)
+      by (auto simp: einterval_def)
have 2: "max c x < b" by simp
from einterval_nonempty [OF 2] obtain e :: real where [simp]: "c < e" "x < e" "e < b"
-      by (auto simp add: einterval_def)
-    show "(?F has_vector_derivative f x) (at x)"
-      (* TODO: factor out the next three lines to has_field_derivative_within_open *)
-      unfolding has_vector_derivative_def
-      apply (subst has_derivative_within_open [of _ "{d<..<e}", symmetric], auto)
-      apply (subst has_vector_derivative_def [symmetric])
-      apply (rule has_vector_derivative_within_subset [of _ _ _ "{d..e}"])
-      apply (rule interval_integral_FTC2, auto simp add: less_imp_le)
-      apply (rule continuous_at_imp_continuous_on)
-      apply (auto intro!: contf)
-      apply (rule order_less_le_trans, rule \<open>a < d\<close>, auto)
-      apply (rule order_le_less_trans) prefer 2
-      by (rule \<open>e < b\<close>, auto)
+      by (auto simp: einterval_def)
+    have "(?F has_vector_derivative f x) (at x within {d<..<e})"
+    proof (rule has_vector_derivative_within_subset [of _ _ _ "{d..e}"])
+      have "continuous_on {d..e} f"
+      proof (intro continuous_at_imp_continuous_on ballI contf; clarsimp)
+        show "\<And>x. \<lbrakk>d \<le> x; x \<le> e\<rbrakk> \<Longrightarrow> a < ereal x"
+          using \<open>a < ereal d\<close> ereal_less_ereal_Ex by auto
+        show "\<And>x. \<lbrakk>d \<le> x; x \<le> e\<rbrakk> \<Longrightarrow> ereal x < b"
+          using \<open>ereal e < b\<close> ereal_less_eq(3) le_less_trans by blast
+      qed
+      then show "(?F has_vector_derivative f x) (at x within {d..e})"
+        by (intro interval_integral_FTC2) (use \<open>d < c\<close> \<open>c < e\<close> \<open>d < x\<close> \<open>x < e\<close> in \<open>linarith+\<close>)
+    qed auto
+    then show "(?F has_vector_derivative f x) (at x)"
+      by (force simp: has_vector_derivative_within_open [of _ "{d<..<e}"])
qed
qed

@@ -815,44 +798,36 @@
using derivg unfolding has_field_derivative_iff_has_vector_derivative .
then have contg [simp]: "continuous_on {a..b} g"
by (rule continuous_on_vector_derivative) auto
-  have 1: "\<And>u. min (g a) (g b) \<le> u \<Longrightarrow> u \<le> max (g a) (g b) \<Longrightarrow>
-      \<exists>x\<in>{a..b}. u = g x"
-    apply (case_tac "g a \<le> g b")
-    apply (auto simp add: min_def max_def less_imp_le)
-    apply (frule (1) IVT' [of g], auto simp add: assms)
-    by (frule (1) IVT2' [of g], auto simp add: assms)
-  from contg \<open>a \<le> b\<close> have "\<exists>c d. g ` {a..b} = {c..d} \<and> c \<le> d"
-    by (elim continuous_image_closed_interval)
-  then obtain c d where g_im: "g ` {a..b} = {c..d}" and "c \<le> d" by auto
-  have "\<exists>F. \<forall>x\<in>{a..b}. (F has_vector_derivative (f (g x))) (at (g x) within (g ` {a..b}))"
-    apply (rule exI, auto, subst g_im)
-    apply (rule interval_integral_FTC2 [of c c d])
-    using \<open>c \<le> d\<close> apply auto
-    apply (rule continuous_on_subset [OF contf])
-    using g_im by auto
-  then guess F ..
-  then have derivF: "\<And>x. a \<le> x \<Longrightarrow> x \<le> b \<Longrightarrow>
-    (F has_vector_derivative (f (g x))) (at (g x) within (g ` {a..b}))" by auto
-  have contf2: "continuous_on {min (g a) (g b)..max (g a) (g b)} f"
-    apply (rule continuous_on_subset [OF contf])
-    apply (auto simp add: image_def)
-    by (erule 1)
+  have 1: "\<exists>x\<in>{a..b}. u = g x" if "min (g a) (g b) \<le> u" "u \<le> max (g a) (g b)" for u
+    by (cases "g a \<le> g b") (use that assms IVT' [of g a u b]  IVT2' [of g b u a]  in \<open>auto simp: min_def max_def\<close>)
+  obtain c d where g_im: "g ` {a..b} = {c..d}" and "c \<le> d"
+    by (metis continuous_image_closed_interval contg \<open>a \<le> b\<close>)
+  obtain F where derivF:
+         "\<And>x. \<lbrakk>a \<le> x; x \<le> b\<rbrakk> \<Longrightarrow> (F has_vector_derivative (f (g x))) (at (g x) within (g ` {a..b}))"
+    using continuous_on_subset [OF contf] g_im
+      by (metis antiderivative_continuous atLeastAtMost_iff image_subset_iff set_eq_subset)
have contfg: "continuous_on {a..b} (\<lambda>x. f (g x))"
by (blast intro: continuous_on_compose2 contf contg)
-  have "LBINT x=a..b. g' x *\<^sub>R f (g x) = F (g b) - F (g a)"
-    apply (subst interval_integral_Icc, simp add: assms)
-    unfolding set_lebesgue_integral_def
-    apply (rule integral_FTC_atLeastAtMost[of a b "\<lambda>x. F (g x)", OF \<open>a \<le> b\<close>])
-    apply (rule vector_diff_chain_within[OF v_derivg derivF, unfolded comp_def])
+  have "LBINT x. indicat_real {a..b} x *\<^sub>R g' x *\<^sub>R f (g x) = F (g b) - F (g a)"
+    apply (rule integral_FTC_atLeastAtMost
+                [OF \<open>a \<le> b\<close> vector_diff_chain_within[OF v_derivg derivF, unfolded comp_def]])
apply (auto intro!: continuous_on_scaleR contg' contfg)
done
+  then have "LBINT x=a..b. g' x *\<^sub>R f (g x) = F (g b) - F (g a)"
+    by (simp add: assms interval_integral_Icc set_lebesgue_integral_def)
moreover have "LBINT y=(g a)..(g b). f y = F (g b) - F (g a)"
-    apply (rule interval_integral_FTC_finite)
-    apply (rule contf2)
-    apply (frule (1) 1, auto)
-    apply (rule has_vector_derivative_within_subset [OF derivF])
-    apply (auto simp add: image_def)
-    by (rule 1, auto)
+  proof (rule interval_integral_FTC_finite)
+    show "continuous_on {min (g a) (g b)..max (g a) (g b)} f"
+      by (rule continuous_on_subset [OF contf]) (auto simp: image_def 1)
+    show "(F has_vector_derivative f y) (at y within {min (g a) (g b)..max (g a) (g b)})"
+      if y: "min (g a) (g b) \<le> y" "y \<le> max (g a) (g b)" for y
+    proof -
+      obtain x where "a \<le> x" "x \<le> b" "y = g x"
+        using 1 y by force
+      then show ?thesis
+        by (auto simp: image_def intro!: 1  has_vector_derivative_within_subset [OF derivF])
+    qed
+  qed
ultimately show ?thesis by simp
qed

@@ -871,86 +846,85 @@
and integrable2: "set_integrable lborel (einterval A B) (\<lambda>x. f x)"
shows "(LBINT x=A..B. f x) = (LBINT x=a..b. g' x *\<^sub>R f (g x))"
proof -
-  from einterval_Icc_approximation[OF \<open>a < b\<close>] guess u l . note approx [simp] = this
+  obtain u l where approx [simp]:
+    "einterval a b = (\<Union>i. {l i .. u i})"
+    "incseq u" "decseq l" "\<And>i. l i < u i" "\<And>i. a < l i" "\<And>i. u i < b"
+    "l \<longlonglongrightarrow> a" "u \<longlonglongrightarrow> b"
+    by (blast intro: einterval_Icc_approximation[OF \<open>a < b\<close>])
note less_imp_le [simp]
have [simp]: "\<And>x i. l i \<le> x \<Longrightarrow> a < ereal x"
by (rule order_less_le_trans, rule approx, force)
have [simp]: "\<And>x i. x \<le> u i \<Longrightarrow> ereal x < b"
by (rule order_le_less_trans, subst ereal_less_eq(3), assumption, rule approx)
-  have [simp]: "\<And>i. l i < b"
-    apply (rule order_less_trans) prefer 2
-    by (rule approx, auto, rule approx)
+  then have lessb[simp]: "\<And>i. l i < b"
+    using approx(4) less_eq_real_def by blast
have [simp]: "\<And>i. a < u i"
by (rule order_less_trans, rule approx, auto, rule approx)
-  have [simp]: "\<And>i j. i \<le> j \<Longrightarrow> l j \<le> l i" by (rule decseqD, rule approx)
+  have lle[simp]: "\<And>i j. i \<le> j \<Longrightarrow> l j \<le> l i" by (rule decseqD, rule approx)
have [simp]: "\<And>i j. i \<le> j \<Longrightarrow> u i \<le> u j" by (rule incseqD, rule approx)
-  have g_nondec [simp]: "\<And>x y. a < x \<Longrightarrow> x \<le> y \<Longrightarrow> y < b \<Longrightarrow> g x \<le> g y"
-    apply (erule DERIV_nonneg_imp_nondecreasing, auto)
-    apply (rule exI, rule conjI, rule deriv_g)
-    apply (erule order_less_le_trans, auto)
-    apply (rule order_le_less_trans, subst ereal_less_eq(3), assumption, auto)
-    apply (rule g'_nonneg)
-    apply (rule less_imp_le, erule order_less_le_trans, auto)
-    by (rule less_imp_le, rule le_less_trans, subst ereal_less_eq(3), assumption, auto)
+  have g_nondec [simp]: "g x \<le> g y" if "a < x" "x \<le> y" "y < b" for x y
+  proof (rule DERIV_nonneg_imp_nondecreasing [OF \<open>x \<le> y\<close>], intro exI conjI allI impI)
+    show "\<And>u. x \<le> u \<and> u \<le> y \<Longrightarrow> (g has_real_derivative g' u) (at u)"
+      by (meson deriv_g ereal_less_eq(3) le_less_trans less_le_trans that)
+    show "\<And>u. x \<le> u \<and> u \<le> y \<Longrightarrow> 0 \<le> g' u"
+      by (meson assms(5) dual_order.trans le_ereal_le less_imp_le order_refl that)
+  qed
have "A \<le> B" and un: "einterval A B = (\<Union>i. {g(l i)<..<g(u i)})"
proof -
have A2: "(\<lambda>i. g (l i)) \<longlonglongrightarrow> A"
-      using A apply (auto simp add: einterval_def tendsto_at_iff_sequentially comp_def)
+      using A apply (auto simp: einterval_def tendsto_at_iff_sequentially comp_def)
by (drule_tac x = "\<lambda>i. ereal (l i)" in spec, auto)
hence A3: "\<And>i. g (l i) \<ge> A"
-      by (intro decseq_le, auto simp add: decseq_def)
+      by (intro decseq_le, auto simp: decseq_def)
have B2: "(\<lambda>i. g (u i)) \<longlonglongrightarrow> B"
-      using B apply (auto simp add: einterval_def tendsto_at_iff_sequentially comp_def)
+      using B apply (auto simp: einterval_def tendsto_at_iff_sequentially comp_def)
by (drule_tac x = "\<lambda>i. ereal (u i)" in spec, auto)
hence B3: "\<And>i. g (u i) \<le> B"
-      by (intro incseq_le, auto simp add: incseq_def)
-    show "A \<le> B"
-      apply (rule order_trans [OF A3 [of 0]])
-      apply (rule order_trans [OF _ B3 [of 0]])
+      by (intro incseq_le, auto simp: incseq_def)
+    have "ereal (g (l 0)) \<le> ereal (g (u 0))"
by auto
+    then show "A \<le> B"
+      by (meson A3 B3 order.trans)
{ fix x :: real
assume "A < x" and "x < B"
then have "eventually (\<lambda>i. ereal (g (l i)) < x \<and> x < ereal (g (u i))) sequentially"
-        apply (intro eventually_conj order_tendstoD)
-        by (rule A2, assumption, rule B2, assumption)
+        by (fast intro: eventually_conj order_tendstoD A2 B2)
hence "\<exists>i. g (l i) < x \<and> x < g (u i)"
} note AB = this
show "einterval A B = (\<Union>i. {g(l i)<..<g(u i)})"
-      apply (auto simp add: einterval_def)
-      apply (erule (1) AB)
-      apply (rule order_le_less_trans, rule A3, simp)
-      apply (rule order_less_le_trans) prefer 2
-      by (rule B3, simp)
+    proof
+      show "einterval A B \<subseteq> (\<Union>i. {g(l i)<..<g(u i)})"
+        by (auto simp: einterval_def AB)
+      show "(\<Union>i. {g(l i)<..<g(u i)}) \<subseteq> einterval A B"
+      proof (clarsimp simp add: einterval_def, intro conjI)
+        show "\<And>x i. \<lbrakk>g (l i) < x; x < g (u i)\<rbrakk> \<Longrightarrow> A < ereal x"
+          using A3 le_ereal_less by blast
+        show "\<And>x i. \<lbrakk>g (l i) < x; x < g (u i)\<rbrakk> \<Longrightarrow> ereal x < B"
+          using B3 ereal_le_less by blast
+      qed
+    qed
qed
(* finally, the main argument *)
-  {
-     fix i
-     have "(LBINT x=l i.. u i. g' x *\<^sub>R f (g x)) = (LBINT y=g (l i)..g (u i). f y)"
-        apply (rule interval_integral_substitution_finite, auto)
-        apply (rule DERIV_subset)
-        unfolding has_field_derivative_iff_has_vector_derivative[symmetric]
-        apply (rule deriv_g)
-        apply (auto intro!: continuous_at_imp_continuous_on contf contg')
-        done
-  } note eq1 = this
+  have eq1: "(LBINT x=l i.. u i. g' x *\<^sub>R f (g x)) = (LBINT y=g (l i)..g (u i). f y)" for i
+    apply (rule interval_integral_substitution_finite [OF _ DERIV_subset [OF deriv_g]])
+    unfolding has_field_derivative_iff_has_vector_derivative[symmetric]
+         apply (auto intro!: continuous_at_imp_continuous_on contf contg')
+    done
have "(\<lambda>i. LBINT x=l i..u i. g' x *\<^sub>R f (g x)) \<longlonglongrightarrow> (LBINT x=a..b. g' x *\<^sub>R f (g x))"
apply (rule interval_integral_Icc_approx_integrable [OF \<open>a < b\<close> approx])
by (rule assms)
hence 2: "(\<lambda>i. (LBINT y=g (l i)..g (u i). f y)) \<longlonglongrightarrow> (LBINT x=a..b. g' x *\<^sub>R f (g x))"
have incseq: "incseq (\<lambda>i. {g (l i)<..<g (u i)})"
-    apply (auto simp add: incseq_def)
-    apply (rule order_le_less_trans)
-    prefer 2 apply (assumption, auto)
-    by (erule order_less_le_trans, rule g_nondec, auto)
-  have "(\<lambda>i. (LBINT y=g (l i)..g (u i). f y)) \<longlonglongrightarrow> (LBINT x = A..B. f x)"
-    apply (subst interval_lebesgue_integral_le_eq, auto simp del: real_scaleR_def)
-    apply (subst interval_lebesgue_integral_le_eq, rule \<open>A \<le> B\<close>)
-    apply (subst un, rule set_integral_cont_up, auto simp del: real_scaleR_def)
-    apply (rule incseq)
-    apply (subst un [symmetric])
-    by (rule integrable2)
+    apply (auto simp: incseq_def)
+    using lessb lle approx(5) g_nondec le_less_trans apply blast
+    by (force intro: less_le_trans)
+  have "(\<lambda>i. set_lebesgue_integral lborel {g (l i)<..<g (u i)} f)
+        \<longlonglongrightarrow> set_lebesgue_integral lborel (einterval A B) f"
+    unfolding un  by (rule set_integral_cont_up) (use incseq  integrable2 un in auto)
+  then have "(\<lambda>i. (LBINT y=g (l i)..g (u i). f y)) \<longlonglongrightarrow> (LBINT x = A..B. f x)"
+    by (simp add: interval_lebesgue_integral_le_eq \<open>A \<le> B\<close>)
thus ?thesis by (intro LIMSEQ_unique [OF _ 2])
qed

@@ -975,98 +949,97 @@
proof -
from einterval_Icc_approximation[OF \<open>a < b\<close>] guess u l . note approx [simp] = this
note less_imp_le [simp]
-  have [simp]: "\<And>x i. l i \<le> x \<Longrightarrow> a < ereal x"
+  have aless[simp]: "\<And>x i. l i \<le> x \<Longrightarrow> a < ereal x"
by (rule order_less_le_trans, rule approx, force)
-  have [simp]: "\<And>x i. x \<le> u i \<Longrightarrow> ereal x < b"
+  have lessb[simp]: "\<And>x i. x \<le> u i \<Longrightarrow> ereal x < b"
by (rule order_le_less_trans, subst ereal_less_eq(3), assumption, rule approx)
-  have [simp]: "\<And>i. l i < b"
-    apply (rule order_less_trans) prefer 2
-    by (rule approx, auto, rule approx)
-  have [simp]: "\<And>i. a < u i"
+  have llb[simp]: "\<And>i. l i < b"
+    using lessb approx(4) less_eq_real_def by blast
+  have alu[simp]: "\<And>i. a < u i"
by (rule order_less_trans, rule approx, auto, rule approx)
have [simp]: "\<And>i j. i \<le> j \<Longrightarrow> l j \<le> l i" by (rule decseqD, rule approx)
-  have [simp]: "\<And>i j. i \<le> j \<Longrightarrow> u i \<le> u j" by (rule incseqD, rule approx)
-  have g_nondec [simp]: "\<And>x y. a < x \<Longrightarrow> x \<le> y \<Longrightarrow> y < b \<Longrightarrow> g x \<le> g y"
-    apply (erule DERIV_nonneg_imp_nondecreasing, auto)
-    apply (rule exI, rule conjI, rule deriv_g)
-    apply (erule order_less_le_trans, auto)
-    apply (rule order_le_less_trans, subst ereal_less_eq(3), assumption, auto)
-    apply (rule g'_nonneg)
-    apply (rule less_imp_le, erule order_less_le_trans, auto)
-    by (rule less_imp_le, rule le_less_trans, subst ereal_less_eq(3), assumption, auto)
+  have uleu[simp]: "\<And>i j. i \<le> j \<Longrightarrow> u i \<le> u j" by (rule incseqD, rule approx)
+  have g_nondec [simp]: "g x \<le> g y" if "a < x" "x \<le> y" "y < b" for x y
+  proof (rule DERIV_nonneg_imp_nondecreasing [OF \<open>x \<le> y\<close>], intro exI conjI allI impI)
+    show "\<And>u. x \<le> u \<and> u \<le> y \<Longrightarrow> (g has_real_derivative g' u) (at u)"
+      by (meson deriv_g ereal_less_eq(3) le_less_trans less_le_trans that)
+    show "\<And>u. x \<le> u \<and> u \<le> y \<Longrightarrow> 0 \<le> g' u"
+      by (meson g'_nonneg less_ereal.simps(1) less_trans not_less that)
+  qed
have "A \<le> B" and un: "einterval A B = (\<Union>i. {g(l i)<..<g(u i)})"
proof -
have A2: "(\<lambda>i. g (l i)) \<longlonglongrightarrow> A"
-      using A apply (auto simp add: einterval_def tendsto_at_iff_sequentially comp_def)
+      using A apply (auto simp: einterval_def tendsto_at_iff_sequentially comp_def)
by (drule_tac x = "\<lambda>i. ereal (l i)" in spec, auto)
hence A3: "\<And>i. g (l i) \<ge> A"
-      by (intro decseq_le, auto simp add: decseq_def)
+      by (intro decseq_le, auto simp: decseq_def)
have B2: "(\<lambda>i. g (u i)) \<longlonglongrightarrow> B"
-      using B apply (auto simp add: einterval_def tendsto_at_iff_sequentially comp_def)
+      using B apply (auto simp: einterval_def tendsto_at_iff_sequentially comp_def)
by (drule_tac x = "\<lambda>i. ereal (u i)" in spec, auto)
hence B3: "\<And>i. g (u i) \<le> B"
-      by (intro incseq_le, auto simp add: incseq_def)
-    show "A \<le> B"
-      apply (rule order_trans [OF A3 [of 0]])
-      apply (rule order_trans [OF _ B3 [of 0]])
+      by (intro incseq_le, auto simp: incseq_def)
+    have "ereal (g (l 0)) \<le> ereal (g (u 0))"
by auto
+    then show "A \<le> B"
+      by (meson A3 B3 order.trans)
{ fix x :: real
assume "A < x" and "x < B"
then have "eventually (\<lambda>i. ereal (g (l i)) < x \<and> x < ereal (g (u i))) sequentially"
-        apply (intro eventually_conj order_tendstoD)
-        by (rule A2, assumption, rule B2, assumption)
+        by (fast intro: eventually_conj order_tendstoD A2 B2)
hence "\<exists>i. g (l i) < x \<and> x < g (u i)"
} note AB = this
show "einterval A B = (\<Union>i. {g(l i)<..<g(u i)})"
-      apply (auto simp add: einterval_def)
-      apply (erule (1) AB)
-      apply (rule order_le_less_trans, rule A3, simp)
-      apply (rule order_less_le_trans) prefer 2
-      by (rule B3, simp)
+    proof
+      show "einterval A B \<subseteq> (\<Union>i. {g (l i)<..<g (u i)})"
+        by (auto simp: einterval_def AB)
+      show "(\<Union>i. {g (l i)<..<g (u i)}) \<subseteq> einterval A B"
+        apply (clarsimp simp: einterval_def, intro conjI)
+        using A3 le_ereal_less apply blast
+        using B3 ereal_le_less by blast
+    qed
qed
-  (* finally, the main argument *)
-  {
-     fix i
-     have "(LBINT x=l i.. u i. g' x *\<^sub>R f (g x)) = (LBINT y=g (l i)..g (u i). f y)"
-        apply (rule interval_integral_substitution_finite, auto)
-        apply (rule DERIV_subset, rule deriv_g, auto)
-        apply (rule continuous_at_imp_continuous_on, auto, rule contf, auto)
-        by (rule continuous_at_imp_continuous_on, auto, rule contg', auto)
-     then have "(LBINT x=l i.. u i. (f (g x) * g' x)) = (LBINT y=g (l i)..g (u i). f y)"
-  } note eq1 = this
-  have "(\<lambda>i. LBINT x=l i..u i. f (g x) * g' x)
-      \<longlonglongrightarrow> (LBINT x=a..b. f (g x) * g' x)"
-    apply (rule interval_integral_Icc_approx_integrable [OF \<open>a < b\<close> approx])
-    by (rule assms)
-  hence 2: "(\<lambda>i. (LBINT y=g (l i)..g (u i). f y)) \<longlonglongrightarrow> (LBINT x=a..b. f (g x) * g' x)"
+    (* finally, the main argument *)
+  have eq1: "(LBINT x=l i.. u i. (f (g x) * g' x)) = (LBINT y=g (l i)..g (u i). f y)" for i
+  proof -
+    have "(LBINT x=l i.. u i. g' x *\<^sub>R f (g x)) = (LBINT y=g (l i)..g (u i). f y)"
+      apply (rule interval_integral_substitution_finite [OF _ DERIV_subset [OF deriv_g]])
+      unfolding has_field_derivative_iff_has_vector_derivative[symmetric]
+           apply (auto intro!: continuous_at_imp_continuous_on contf contg')
+      done
+    then show ?thesis
+  qed
have incseq: "incseq (\<lambda>i. {g (l i)<..<g (u i)})"
-    apply (auto simp add: incseq_def)
-    apply (rule order_le_less_trans)
-    prefer 2 apply assumption
-    apply (rule g_nondec, auto)
-    by (erule order_less_le_trans, rule g_nondec, auto)
-  have img: "\<And>x i. g (l i) \<le> x \<Longrightarrow> x \<le> g (u i) \<Longrightarrow> \<exists>c \<ge> l i. c \<le> u i \<and> x = g c"
-    apply (frule (1) IVT' [of g], auto)
-    apply (rule continuous_at_imp_continuous_on, auto)
-    by (rule DERIV_isCont, rule deriv_g, auto)
-  have nonneg_f2: "\<And>x i. g (l i) \<le> x \<Longrightarrow> x \<le> g (u i) \<Longrightarrow> 0 \<le> f x"
-    by (frule (1) img, auto, rule f_nonneg, auto)
-  have contf_2: "\<And>x i. g (l i) \<le> x \<Longrightarrow> x \<le> g (u i) \<Longrightarrow> isCont f x"
-    by (frule (1) img, auto, rule contf, auto)
+    apply (clarsimp simp add: incseq_def, intro conjI)
+    apply (meson llb antimono_def approx(3) approx(5) g_nondec le_less_trans)
+    using alu uleu approx(6) g_nondec less_le_trans by blast
+  have img: "\<exists>c \<ge> l i. c \<le> u i \<and> x = g c" if "g (l i) \<le> x" "x \<le> g (u i)" for x i
+  proof -
+    have "continuous_on {l i..u i} g"
+      by (force intro!: DERIV_isCont deriv_g continuous_at_imp_continuous_on)
+    with that show ?thesis
+      using IVT' [of g] approx(4) dual_order.strict_implies_order by blast
+  qed
+  have "continuous_on {g (l i)..g (u i)} f" for i
+    apply (intro continuous_intros continuous_at_imp_continuous_on)
+    using contf img by force
+  then have int_f: "\<And>i. set_integrable lborel {g (l i)<..<g (u i)} f"
+    by (rule set_integrable_subset [OF borel_integrable_atLeastAtMost']) (auto intro: less_imp_le)
have integrable: "set_integrable lborel (\<Union>i. {g (l i)<..<g (u i)}) f"
-    apply (rule pos_integrable_to_top, auto simp del: real_scaleR_def)
-    apply (rule incseq)
-    apply (rule nonneg_f2, erule less_imp_le, erule less_imp_le)
-    apply (rule set_integrable_subset)
-    apply (rule borel_integrable_atLeastAtMost')
-    apply (rule continuous_at_imp_continuous_on)
-    apply (clarsimp, erule (1) contf_2, auto)
-    apply (erule less_imp_le)+
-    using 2 unfolding interval_lebesgue_integral_def
-    by auto
+  proof (intro pos_integrable_to_top incseq int_f)
+    let ?l = "(LBINT x=a..b. f (g x) * g' x)"
+    have "(\<lambda>i. LBINT x=l i..u i. f (g x) * g' x) \<longlonglongrightarrow> ?l"
+      by (intro assms interval_integral_Icc_approx_integrable [OF \<open>a < b\<close> approx])
+    hence "(\<lambda>i. (LBINT y=g (l i)..g (u i). f y)) \<longlonglongrightarrow> ?l"
+    then show "(\<lambda>i. set_lebesgue_integral lborel {g (l i)<..<g (u i)} f) \<longlonglongrightarrow> ?l"
+      unfolding interval_lebesgue_integral_def by auto
+    have "\<And>x i. g (l i) \<le> x \<Longrightarrow> x \<le> g (u i) \<Longrightarrow> 0 \<le> f x"
+      using aless f_nonneg img lessb by blast
+    then show "\<And>x i. x \<in> {g (l i)<..<g (u i)} \<Longrightarrow> 0 \<le> f x"
+      using less_eq_real_def by auto
+  qed (auto simp: greaterThanLessThan_borel)
thus "set_integrable lborel (einterval A B) f"

@@ -1111,7 +1084,7 @@
shows "interval_lebesgue_integrable lborel a b f \<Longrightarrow> a \<le> b \<Longrightarrow>
norm (LBINT t=a..b. f t) \<le> LBINT t=a..b. norm (f t)"
using integral_norm_bound[of lborel "\<lambda>x. indicator (einterval a b) x *\<^sub>R f x"]
-  by (auto simp add: interval_lebesgue_integral_def interval_lebesgue_integrable_def set_lebesgue_integral_def)
+  by (auto simp: interval_lebesgue_integral_def interval_lebesgue_integrable_def set_lebesgue_integral_def)

lemma interval_integral_norm2:
"interval_lebesgue_integrable lborel a b f \<Longrightarrow>
@@ -1123,7 +1096,7 @@
case (le a b)
then have "\<bar>LBINT t=a..b. norm (f t)\<bar> = LBINT t=a..b. norm (f t)"
using integrable_norm[of lborel "\<lambda>x. indicator (einterval a b) x *\<^sub>R f x"]
-    by (auto simp add: interval_lebesgue_integral_def interval_lebesgue_integrable_def set_lebesgue_integral_def
+    by (auto simp: interval_lebesgue_integral_def interval_lebesgue_integrable_def set_lebesgue_integral_def
intro!: integral_nonneg_AE abs_of_nonneg)
then show ?case
using le by (simp add: interval_integral_norm)
@@ -1134,5 +1107,4 @@
apply (intro interval_integral_FTC_finite continuous_intros)
by (auto intro!: derivative_eq_intros simp: has_field_derivative_iff_has_vector_derivative[symmetric])

-
end```
```--- a/src/HOL/Analysis/Path_Connected.thy	Sun May 06 23:30:34 2018 +0200
+++ b/src/HOL/Analysis/Path_Connected.thy	Sun May 06 23:59:14 2018 +0100
@@ -42,15 +42,15 @@
lemma path_eq: "path p \<Longrightarrow> (\<And>t. t \<in> {0..1} \<Longrightarrow> p t = q t) \<Longrightarrow> path q"
using continuous_on_eq path_def by blast

-lemma path_continuous_image: "path g \<Longrightarrow> continuous_on (path_image g) f \<Longrightarrow> path(f o g)"
+lemma path_continuous_image: "path g \<Longrightarrow> continuous_on (path_image g) f \<Longrightarrow> path(f \<circ> g)"
unfolding path_def path_image_def
using continuous_on_compose by blast

lemma path_translation_eq:
fixes g :: "real \<Rightarrow> 'a :: real_normed_vector"
-  shows "path((\<lambda>x. a + x) o g) = path g"
+  shows "path((\<lambda>x. a + x) \<circ> g) = path g"
proof -
-  have g: "g = (\<lambda>x. -a + x) o ((\<lambda>x. a + x) o g)"
+  have g: "g = (\<lambda>x. -a + x) \<circ> ((\<lambda>x. a + x) \<circ> g)"
by (rule ext) simp
show ?thesis
unfolding path_def
@@ -64,12 +64,12 @@
lemma path_linear_image_eq:
fixes f :: "'a::euclidean_space \<Rightarrow> 'b::euclidean_space"
assumes "linear f" "inj f"
-     shows "path(f o g) = path g"
+     shows "path(f \<circ> g) = path g"
proof -
from linear_injective_left_inverse [OF assms]
obtain h where h: "linear h" "h \<circ> f = id"
by blast
-  then have g: "g = h o (f o g)"
+  then have g: "g = h \<circ> (f \<circ> g)"
by (metis comp_assoc id_comp)
show ?thesis
unfolding path_def
@@ -77,58 +77,58 @@
by (metis g continuous_on_compose linear_continuous_on linear_conv_bounded_linear)
qed

-lemma pathstart_translation: "pathstart((\<lambda>x. a + x) o g) = a + pathstart g"
+lemma pathstart_translation: "pathstart((\<lambda>x. a + x) \<circ> g) = a + pathstart g"

-lemma pathstart_linear_image_eq: "linear f \<Longrightarrow> pathstart(f o g) = f(pathstart g)"
+lemma pathstart_linear_image_eq: "linear f \<Longrightarrow> pathstart(f \<circ> g) = f(pathstart g)"

-lemma pathfinish_translation: "pathfinish((\<lambda>x. a + x) o g) = a + pathfinish g"
+lemma pathfinish_translation: "pathfinish((\<lambda>x. a + x) \<circ> g) = a + pathfinish g"

-lemma pathfinish_linear_image: "linear f \<Longrightarrow> pathfinish(f o g) = f(pathfinish g)"
+lemma pathfinish_linear_image: "linear f \<Longrightarrow> pathfinish(f \<circ> g) = f(pathfinish g)"

-lemma path_image_translation: "path_image((\<lambda>x. a + x) o g) = (\<lambda>x. a + x) ` (path_image g)"
+lemma path_image_translation: "path_image((\<lambda>x. a + x) \<circ> g) = (\<lambda>x. a + x) ` (path_image g)"

-lemma path_image_linear_image: "linear f \<Longrightarrow> path_image(f o g) = f ` (path_image g)"
+lemma path_image_linear_image: "linear f \<Longrightarrow> path_image(f \<circ> g) = f ` (path_image g)"

-lemma reversepath_translation: "reversepath((\<lambda>x. a + x) o g) = (\<lambda>x. a + x) o reversepath g"
+lemma reversepath_translation: "reversepath((\<lambda>x. a + x) \<circ> g) = (\<lambda>x. a + x) \<circ> reversepath g"
by (rule ext) (simp add: reversepath_def)

-lemma reversepath_linear_image: "linear f \<Longrightarrow> reversepath(f o g) = f o reversepath g"
+lemma reversepath_linear_image: "linear f \<Longrightarrow> reversepath(f \<circ> g) = f \<circ> reversepath g"
by (rule ext) (simp add: reversepath_def)

lemma joinpaths_translation:
-    "((\<lambda>x. a + x) o g1) +++ ((\<lambda>x. a + x) o g2) = (\<lambda>x. a + x) o (g1 +++ g2)"
+    "((\<lambda>x. a + x) \<circ> g1) +++ ((\<lambda>x. a + x) \<circ> g2) = (\<lambda>x. a + x) \<circ> (g1 +++ g2)"
by (rule ext) (simp add: joinpaths_def)

-lemma joinpaths_linear_image: "linear f \<Longrightarrow> (f o g1) +++ (f o g2) = f o (g1 +++ g2)"
+lemma joinpaths_linear_image: "linear f \<Longrightarrow> (f \<circ> g1) +++ (f \<circ> g2) = f \<circ> (g1 +++ g2)"
by (rule ext) (simp add: joinpaths_def)

lemma simple_path_translation_eq:
fixes g :: "real \<Rightarrow> 'a::euclidean_space"
-  shows "simple_path((\<lambda>x. a + x) o g) = simple_path g"
+  shows "simple_path((\<lambda>x. a + x) \<circ> g) = simple_path g"

lemma simple_path_linear_image_eq:
fixes f :: "'a::euclidean_space \<Rightarrow> 'b::euclidean_space"
assumes "linear f" "inj f"
-    shows "simple_path(f o g) = simple_path g"
+    shows "simple_path(f \<circ> g) = simple_path g"
using assms inj_on_eq_iff [of f]
by (auto simp: path_linear_image_eq simple_path_def path_translation_eq)

lemma arc_translation_eq:
fixes g :: "real \<Rightarrow> 'a::euclidean_space"
-  shows "arc((\<lambda>x. a + x) o g) = arc g"
+  shows "arc((\<lambda>x. a + x) \<circ> g) = arc g"
by (auto simp: arc_def inj_on_def path_translation_eq)

lemma arc_linear_image_eq:
fixes f :: "'a::euclidean_space \<Rightarrow> 'b::euclidean_space"
assumes "linear f" "inj f"
-     shows  "arc(f o g) = arc g"
+     shows  "arc(f \<circ> g) = arc g"
using assms inj_on_eq_iff [of f]
by (auto simp: arc_def inj_on_def path_linear_image_eq)

@@ -151,7 +151,7 @@

lemma simple_path_cases: "simple_path g \<Longrightarrow> arc g \<or> pathfinish g = pathstart g"
unfolding simple_path_def arc_def inj_on_def pathfinish_def pathstart_def
-  by (force)
+  by force

lemma simple_path_imp_arc: "simple_path g \<Longrightarrow> pathfinish g \<noteq> pathstart g \<Longrightarrow> arc g"
using simple_path_cases by auto
@@ -225,10 +225,7 @@
have *: "\<And>g. path g \<Longrightarrow> path (reversepath g)"
unfolding path_def reversepath_def
apply (rule continuous_on_compose[unfolded o_def, of _ "\<lambda>x. 1 - x"])
-    apply (intro continuous_intros)
-    apply (rule continuous_on_subset[of "{0..1}"])
-    apply assumption
-    apply auto
+    apply (auto intro: continuous_intros continuous_on_subset[of "{0..1}"])
done
show ?thesis
using *[of "reversepath g"] *[of g]
@@ -245,12 +242,7 @@
have **: "\<And>x y::real. 1-x = 1-y \<Longrightarrow> x = y"
by simp
show ?thesis
-    apply (auto simp: arc_def inj_on_def path_reversepath)
-    apply (simp add: arc_imp_path assms)
-    apply (rule **)
-    apply (rule inj_onD [OF injg])
-    apply (auto simp: reversepath_def)
-    done
+    using assms  by (clarsimp simp: arc_def intro!: inj_onI) (simp add: inj_onD reversepath_def **)
qed

lemma simple_path_reversepath: "simple_path g \<Longrightarrow> simple_path (reversepath g)"
@@ -369,19 +361,19 @@
using assms and path_image_join_subset[of g1 g2]
by auto

-lemma pathstart_compose: "pathstart(f o p) = f(pathstart p)"
+lemma pathstart_compose: "pathstart(f \<circ> p) = f(pathstart p)"

-lemma pathfinish_compose: "pathfinish(f o p) = f(pathfinish p)"
+lemma pathfinish_compose: "pathfinish(f \<circ> p) = f(pathfinish p)"

-lemma path_image_compose: "path_image (f o p) = f ` (path_image p)"
+lemma path_image_compose: "path_image (f \<circ> p) = f ` (path_image p)"

-lemma path_compose_join: "f o (p +++ q) = (f o p) +++ (f o q)"
+lemma path_compose_join: "f \<circ> (p +++ q) = (f \<circ> p) +++ (f \<circ> q)"
by (rule ext) (simp add: joinpaths_def)

-lemma path_compose_reversepath: "f o reversepath p = reversepath(f o p)"
+lemma path_compose_reversepath: "f \<circ> reversepath p = reversepath(f \<circ> p)"
by (rule ext) (simp add: reversepath_def)

lemma joinpaths_eq:
@@ -440,15 +432,15 @@
have gg: "g2 0 = g1 1"
by (metis assms(3) pathfinish_def pathstart_def)
have 1: "continuous_on {0..1/2} (g1 +++ g2)"
-    apply (rule continuous_on_eq [of _ "g1 o (\<lambda>x. 2*x)"])
+    apply (rule continuous_on_eq [of _ "g1 \<circ> (\<lambda>x. 2*x)"])
apply (rule continuous_intros | simp add: joinpaths_def assms)+
done
-  have "continuous_on {1/2..1} (g2 o (\<lambda>x. 2*x-1))"
+  have "continuous_on {1/2..1} (g2 \<circ> (\<lambda>x. 2*x-1))"
apply (rule continuous_on_subset [of "{1/2..1}"])
apply (rule continuous_intros | simp add: image_affinity_atLeastAtMost_diff assms)+
done
then have 2: "continuous_on {1/2..1} (g1 +++ g2)"
-    apply (rule continuous_on_eq [of "{1/2..1}" "g2 o (\<lambda>x. 2*x-1)"])
+    apply (rule continuous_on_eq [of "{1/2..1}" "g2 \<circ> (\<lambda>x. 2*x-1)"])
apply (rule assms continuous_intros | simp add: joinpaths_def mult.commute half_bounded_equal gg)+
done
show ?thesis
@@ -793,7 +785,7 @@
assumes "path g" "u \<in> {0..1}" "v \<in> {0..1}"
shows "path(subpath u v g)"
proof -
-  have "continuous_on {0..1} (g o (\<lambda>x. ((v-u) * x+ u)))"
+  have "continuous_on {0..1} (g \<circ> (\<lambda>x. ((v-u) * x+ u)))"
apply (rule continuous_intros | simp)+
apply (simp add: image_affinity_atLeastAtMost [where c=u])
using assms
@@ -818,10 +810,10 @@
lemma reversepath_subpath: "reversepath(subpath u v g) = subpath v u g"
by (simp add: reversepath_def subpath_def algebra_simps)

-lemma subpath_translation: "subpath u v ((\<lambda>x. a + x) o g) = (\<lambda>x. a + x) o subpath u v g"
+lemma subpath_translation: "subpath u v ((\<lambda>x. a + x) \<circ> g) = (\<lambda>x. a + x) \<circ> subpath u v g"
by (rule ext) (simp add: subpath_def)

-lemma subpath_linear_image: "linear f \<Longrightarrow> subpath u v (f o g) = f o subpath u v g"
+lemma subpath_linear_image: "linear f \<Longrightarrow> subpath u v (f \<circ> g) = f \<circ> subpath u v g"
by (rule ext) (simp add: subpath_def)

lemma affine_ineq:
@@ -891,7 +883,7 @@
assume "x \<in> closed_segment u v" "y \<in> closed_segment u v" "g x = g y"
then have "x = y"
using sim [of "(x-u)/(v-u)" "(y-u)/(v-u)"] p
-    by (force simp add: inj_on_def closed_segment_real_eq image_affinity_atLeastAtMost divide_simps
+    by (force simp: inj_on_def closed_segment_real_eq image_affinity_atLeastAtMost divide_simps
split: if_split_asm)
} moreover
have "path(subpath u v g) \<and> u\<noteq>v"
@@ -1105,20 +1097,20 @@
by auto
show ?thesis
unfolding path_def shiftpath_def *
-    apply (rule continuous_on_closed_Un)
-    apply (rule closed_real_atLeastAtMost)+
-    apply (rule continuous_on_eq[of _ "g \<circ> (\<lambda>x. a + x)"])
-    prefer 3
-    apply (rule continuous_on_eq[of _ "g \<circ> (\<lambda>x. a - 1 + x)"])
-    prefer 3
-    apply (rule continuous_intros)+
-    prefer 2
-    apply (rule continuous_intros)+
-    apply (rule_tac[1-2] continuous_on_subset[OF assms(1)[unfolded path_def]])
-    using assms(3) and **
-    apply auto
-    apply (auto simp add: field_simps)
-    done
+  proof (rule continuous_on_closed_Un)
+    have contg: "continuous_on {0..1} g"
+      using \<open>path g\<close> path_def by blast
+    show "continuous_on {0..1-a} (\<lambda>x. if a + x \<le> 1 then g (a + x) else g (a + x - 1))"
+    proof (rule continuous_on_eq)
+      show "continuous_on {0..1-a} (g \<circ> (+) a)"
+        by (intro continuous_intros continuous_on_subset [OF contg]) (use \<open>a \<in> {0..1}\<close> in auto)
+    qed auto
+    show "continuous_on {1-a..1} (\<lambda>x. if a + x \<le> 1 then g (a + x) else g (a + x - 1))"
+    proof (rule continuous_on_eq)
+      show "continuous_on {1-a..1} (g \<circ> (+) (a - 1))"
+        by (intro continuous_intros continuous_on_subset [OF contg]) (use \<open>a \<in> {0..1}\<close> in auto)
+  qed auto
qed

lemma shiftpath_shiftpath:
@@ -1131,33 +1123,30 @@
by auto

lemma path_image_shiftpath:
-  assumes "a \<in> {0..1}"
+  assumes a: "a \<in> {0..1}"
and "pathfinish g = pathstart g"
shows "path_image (shiftpath a g) = path_image g"
proof -
{ fix x
-    assume as: "g 1 = g 0" "x \<in> {0..1::real}" " \<forall>y\<in>{0..1} \<inter> {x. \<not> a + x \<le> 1}. g x \<noteq> g (a + y - 1)"
+    assume g: "g 1 = g 0" "x \<in> {0..1::real}" and gne: "\<And>y. y\<in>{0..1} \<inter> {x. \<not> a + x \<le> 1} \<Longrightarrow> g x \<noteq> g (a + y - 1)"
then have "\<exists>y\<in>{0..1} \<inter> {x. a + x \<le> 1}. g x = g (a + y)"
proof (cases "a \<le> x")
case False
then show ?thesis
apply (rule_tac x="1 + x - a" in bexI)
-        using as(1,2) and as(3)[THEN bspec[where x="1 + x - a"]] and assms(1)
-        apply (auto simp add: field_simps atomize_not)
+        using g gne[of "1 + x - a"] a
+        apply (force simp: field_simps)+
done
next
case True
then show ?thesis
-        using as(1-2) and assms(1)
-        apply (rule_tac x="x - a" in bexI)
-        apply (auto simp add: field_simps)
-        done
+        using g a  by (rule_tac x="x - a" in bexI) (auto simp: field_simps)
qed
}
then show ?thesis
using assms
unfolding shiftpath_def path_image_def pathfinish_def pathstart_def
-    by (auto simp add: image_iff)
+    by (auto simp: image_iff)
qed

lemma simple_path_shiftpath:
@@ -1172,9 +1161,7 @@
show "x = y \<or> x = 0 \<and> y = 1 \<or> x = 1 \<and> y = 0"
if "x \<in> {0..1}" "y \<in> {0..1}" "shiftpath a g x = shiftpath a g y" for x y
using that a unfolding shiftpath_def
-    apply (simp add: split: if_split_asm)
-      apply (drule *; auto)+
-    done
+    by (force split: if_split_asm dest!: *)
qed

subsection \<open>Special case of straight-line paths\<close>
@@ -1226,11 +1213,11 @@
}
then show ?thesis
unfolding arc_def inj_on_def
-    by (simp add:  path_linepath) (force simp: algebra_simps linepath_def)
+    by (fastforce simp: algebra_simps linepath_def)
qed

lemma simple_path_linepath[intro]: "a \<noteq> b \<Longrightarrow> simple_path (linepath a b)"
-  by (simp add: arc_imp_simple_path arc_linepath)

lemma linepath_trivial [simp]: "linepath a a x = a"
@@ -1275,10 +1262,7 @@
shows "midpoint x y \<in> convex hull s"
proof -
have "(1 - inverse(2)) *\<^sub>R x + inverse(2) *\<^sub>R y \<in> convex hull s"
-    apply (rule convexD_alt)
-    using assms
-    apply (auto simp: convex_convex_hull)
-    done
+    by (rule convexD_alt) (use assms in auto)
then show ?thesis
qed
@@ -1339,7 +1323,7 @@
proof (intro exI conjI)
have "closed_segment (x-\<delta>) (x+\<delta>) = {x-\<delta>..x+\<delta>}"
using \<open>0 < \<delta>\<close> by (auto simp: closed_segment_eq_real_ivl)
-      also have "... \<subseteq> S"
+      also have "\<dots> \<subseteq> S"
using \<delta> \<open>T \<subseteq> S\<close> by (auto simp: dist_norm subset_eq)
finally have "f ` (open_segment (x-\<delta>) (x+\<delta>)) = open_segment (f (x-\<delta>)) (f (x+\<delta>))"
using continuous_injective_image_open_segment_1
@@ -1384,17 +1368,15 @@
lemma not_on_path_ball:
fixes g :: "real \<Rightarrow> 'a::heine_borel"
assumes "path g"
-    and "z \<notin> path_image g"
+    and z: "z \<notin> path_image g"
shows "\<exists>e > 0. ball z e \<inter> path_image g = {}"
proof -
-  obtain a where "a \<in> path_image g" "\<forall>y \<in> path_image g. dist z a \<le> dist z y"
-    apply (rule distance_attains_inf[OF _ path_image_nonempty, of g z])
-    using compact_path_image[THEN compact_imp_closed, OF assms(1)] by auto
+  have "closed (path_image g)"
+    by (simp add: \<open>path g\<close> closed_path_image)
+  then obtain a where "a \<in> path_image g" "\<forall>y \<in> path_image g. dist z a \<le> dist z y"
+    by (auto intro: distance_attains_inf[OF _ path_image_nonempty, of g z])
then show ?thesis
-    apply (rule_tac x="dist z a" in exI)
-    using assms(2)
-    apply (auto intro!: dist_pos_lt)
-    done
+    by (rule_tac x="dist z a" in exI) (use dist_commute z in auto)
qed

lemma not_on_path_cball:
@@ -1408,9 +1390,7 @@
moreover have "cball z (e/2) \<subseteq> ball z e"
using \<open>e > 0\<close> by auto
ultimately show ?thesis
-    apply (rule_tac x="e/2" in exI)
-    apply auto
-    done
+    by (rule_tac x="e/2" in exI) auto
qed

@@ -1446,8 +1426,7 @@
lemma path_component_sym: "path_component s x y \<Longrightarrow> path_component s y x"
unfolding path_component_def
apply (erule exE)
-  apply (rule_tac x="reversepath g" in exI)
-  apply auto
+  apply (rule_tac x="reversepath g" in exI, auto)
done

lemma path_component_trans:
@@ -1457,7 +1436,7 @@
unfolding path_component_def
apply (elim exE)
apply (rule_tac x="g +++ ga" in exI)
-  apply (auto simp add: path_image_join)
+  apply (auto simp: path_image_join)
done

lemma path_component_of_subset: "s \<subseteq> t \<Longrightarrow> path_component s x y \<Longrightarrow> path_component t x y"
@@ -1466,9 +1445,8 @@
lemma path_connected_linepath:
fixes s :: "'a::real_normed_vector set"
shows "closed_segment a b \<subseteq> s \<Longrightarrow> path_component s a b"
-  apply (rule_tac x="linepath a b" in exI, auto)
-  done
+  unfolding path_component_def
+  by (rule_tac x="linepath a b" in exI, auto)

subsubsection%unimportant \<open>Path components as sets\<close>
@@ -1479,7 +1457,7 @@
by (auto simp: path_component_def)

lemma path_component_subset: "path_component_set s x \<subseteq> s"
-  by (auto simp add: path_component_mem(2))
+  by (auto simp: path_component_mem(2))

lemma path_component_eq_empty: "path_component_set s x = {} \<longleftrightarrow> x \<notin> s"
using path_component_mem path_component_refl_eq
@@ -1578,31 +1556,23 @@
unfolding open_contains_ball
proof
fix y
-  assume as: "y \<in> S - path_component_set S x"
+  assume y: "y \<in> S - path_component_set S x"
then obtain e where e: "e > 0" "ball y e \<subseteq> S"
-    using assms [unfolded open_contains_ball]
-    by auto
+    using assms openE by auto
show "\<exists>e>0. ball y e \<subseteq> S - path_component_set S x"
-    apply (rule_tac x=e in exI)
-    apply rule
-    apply (rule \<open>e>0\<close>)
-    apply rule
-    apply rule
-    defer
-  proof (rule ccontr)
-    fix z
-    assume "z \<in> ball y e" "\<not> z \<notin> path_component_set S x"
-    then have "y \<in> path_component_set S x"
-      unfolding not_not mem_Collect_eq using \<open>e>0\<close>
-      apply -
-      apply (rule path_component_trans, assumption)
-      apply (rule path_component_of_subset[OF e(2)])
-      apply (rule convex_imp_path_connected[OF convex_ball, unfolded path_connected_component, rule_format])
-      apply auto
-      done
-    then show False
-      using as by auto
-  qed (insert e(2), auto)
+  proof (intro exI conjI subsetI DiffI notI)
+    show "\<And>x. x \<in> ball y e \<Longrightarrow> x \<in> S"
+      using e by blast
+    show False if "z \<in> ball y e" "z \<in> path_component_set S x" for z
+    proof -
+      have "y \<in> path_component_set S z"
+        by (meson assms convex_ball convex_imp_path_connected e open_contains_ball_eq open_path_component path_component_maximal that(1))
+      then have "y \<in> path_component_set S x"
+        using path_component_eq that(2) by blast
+      then show False
+        using y by blast
+    qed
+  qed (use e in auto)
qed

lemma connected_open_path_connected:
@@ -1676,7 +1646,7 @@

lemma homeomorphic_path_connectedness:
-  "s homeomorphic t \<Longrightarrow> path_connected s \<longleftrightarrow> path_connected t"
+  "S homeomorphic T \<Longrightarrow> path_connected S \<longleftrightarrow> path_connected T"
unfolding homeomorphic_def homeomorphism_def by (metis path_connected_continuous_image)

lemma path_connected_empty [simp]: "path_connected {}"
@@ -1691,23 +1661,35 @@
done

lemma path_connected_Un:
-  assumes "path_connected s"
-    and "path_connected t"
-    and "s \<inter> t \<noteq> {}"
-  shows "path_connected (s \<union> t)"
+  assumes "path_connected S"
+    and "path_connected T"
+    and "S \<inter> T \<noteq> {}"
+  shows "path_connected (S \<union> T)"
unfolding path_connected_component
-proof (rule, rule)
+proof (intro ballI)
fix x y
-  assume as: "x \<in> s \<union> t" "y \<in> s \<union> t"
-  from assms(3) obtain z where "z \<in> s \<inter> t"
+  assume x: "x \<in> S \<union> T" and y: "y \<in> S \<union> T"
+  from assms obtain z where z: "z \<in> S" "z \<in> T"
by auto
-  then show "path_component (s \<union> t) x y"
-    using as and assms(1-2)[unfolded path_connected_component]
-    apply -
-    apply (erule_tac[!] UnE)+
-    apply (rule_tac[2-3] path_component_trans[of _ _ z])
-    apply (auto simp add:path_component_of_subset [OF Un_upper1] path_component_of_subset[OF Un_upper2])
-    done
+  show "path_component (S \<union> T) x y"
+    using x y
+  proof safe
+    assume "x \<in> S" "y \<in> S"
+    then show "path_component (S \<union> T) x y"
+      by (meson Un_upper1 \<open>path_connected S\<close> path_component_of_subset path_connected_component)
+  next
+    assume "x \<in> S" "y \<in> T"
+    then show "path_component (S \<union> T) x y"
+      by (metis z assms(1-2) le_sup_iff order_refl path_component_of_subset path_component_trans path_connected_component)
+  next
+  assume "x \<in> T" "y \<in> S"
+    then show "path_component (S \<union> T) x y"
+      by (metis z assms(1-2) le_sup_iff order_refl path_component_of_subset path_component_trans path_connected_component)
+  next
+    assume "x \<in> T" "y \<in> T"
+    then show "path_component (S \<union> T) x y"
+      by (metis Un_upper1 assms(2) path_component_of_subset path_connected_component sup_commute)
+  qed
qed

lemma path_connected_UNION:
@@ -1729,30 +1711,22 @@
lemma path_component_path_image_pathstart:
assumes p: "path p" and x: "x \<in> path_image p"
shows "path_component (path_image p) (pathstart p) x"
-using x
-  fix y
-  assume "x = p y" and y: "0 \<le> y" "y \<le> 1"
-  show "path_component (p ` {0..1}) (pathstart p) (p y)"
-  proof (cases "y=0")
-    case True then show ?thesis
-      by (simp add: path_component_refl_eq pathstart_def)
-  next
-    case False have "continuous_on {0..1} (p o (( * ) y))"
+proof -
+  obtain y where x: "x = p y" and y: "0 \<le> y" "y \<le> 1"
+    using x by (auto simp: path_image_def)
+  show ?thesis
+    unfolding path_component_def
+  proof (intro exI conjI)
+    have "continuous_on {0..1} (p \<circ> (( *) y))"
apply (rule continuous_intros)+
using p [unfolded path_def] y
apply (auto simp: mult_le_one intro: continuous_on_subset [of _ p])
done
-    then have "path (\<lambda>u. p (y * u))"
+    then show "path (\<lambda>u. p (y * u))"
-    then show ?thesis
-      apply (rule_tac x = "\<lambda>u. p (y * u)" in exI)
-      apply (intro conjI)
-      using y False
-      apply (auto simp: mult_le_one pathstart_def pathfinish_def path_image_def)
-      done
-  qed
+    show "path_image (\<lambda>u. p (y * u)) \<subseteq> path_image p"
+      using y mult_le_one by (fastforce simp: path_image_def image_iff)
+  qed (auto simp: pathstart_def pathfinish_def x)
qed

lemma path_connected_path_image: "path p \<Longrightarrow> path_connected(path_image p)"
@@ -1860,7 +1834,7 @@
by (metis hf gs path_join_imp pathstart_def pathfinish_def)
have "path_image ((\<lambda>z. (x1, h z)) +++ (\<lambda>z. (g z, y2))) \<subseteq> path_image (\<lambda>z. (x1, h z)) \<union> path_image (\<lambda>z. (g z, y2))"
by (rule Path_Connected.path_image_join_subset)
-  also have "... \<subseteq> (\<Union>x\<in>s. \<Union>x1\<in>t. {(x, x1)})"
+  also have "\<dots> \<subseteq> (\<Union>x\<in>s. \<Union>x1\<in>t. {(x, x1)})"
using g h \<open>x1 \<in> s\<close> \<open>y2 \<in> t\<close> by (force simp: path_image_def)
finally have 2: "path_image ((\<lambda>z. (x1, h z)) +++ (\<lambda>z. (g z, y2))) \<subseteq> (\<Union>x\<in>s. \<Union>x1\<in>t. {(x, x1)})" .
show "\<exists>g. path g \<and> path_image g \<subseteq> (\<Union>x\<in>s. \<Union>x1\<in>t. {(x, x1)}) \<and>
@@ -2055,11 +2029,11 @@
have "a + ((1 / (1 + C * u - u)) *\<^sub>R x + ((u / (1 + C * u - u)) *\<^sub>R a + (C * u / (1 + C * u - u)) *\<^sub>R x)) =
(1 + (u / (1 + C * u - u))) *\<^sub>R a + ((1 / (1 + C * u - u)) + (C * u / (1 + C * u - u))) *\<^sub>R x"
-      also have "... = (1 + (u / (1 + C * u - u))) *\<^sub>R a + (1 + (u / (1 + C * u - u))) *\<^sub>R x"
+      also have "\<dots> = (1 + (u / (1 + C * u - u))) *\<^sub>R a + (1 + (u / (1 + C * u - u))) *\<^sub>R x"
using CC by (simp add: field_simps)
-      also have "... = x + (1 + (u / (1 + C * u - u))) *\<^sub>R a + (u / (1 + C * u - u)) *\<^sub>R x"
+      also have "\<dots> = x + (1 + (u / (1 + C * u - u))) *\<^sub>R a + (u / (1 + C * u - u)) *\<^sub>R x"
-      also have "... = x + ((1 / (1 + C * u - u)) *\<^sub>R a +
+      also have "\<dots> = x + ((1 / (1 + C * u - u)) *\<^sub>R a +
((u / (1 + C * u - u)) *\<^sub>R x + (C * u / (1 + C * u - u)) *\<^sub>R a))"
finally have xeq: "(1 - 1 / (1 + (C - 1) * u)) *\<^sub>R a + (1 / (1 + (C - 1) * u)) *\<^sub>R (a + (1 + (C - 1) * u) *\<^sub>R (x - a)) = x"
@@ -2090,11 +2064,11 @@
have "a + ((1 / (1 + D * u - u)) *\<^sub>R y + ((u / (1 + D * u - u)) *\<^sub>R a + (D * u / (1 + D * u - u)) *\<^sub>R y)) =
(1 + (u / (1 + D * u - u))) *\<^sub>R a + ((1 / (1 + D * u - u)) + (D * u / (1 + D * u - u))) *\<^sub>R y"
-      also have "... = (1 + (u / (1 + D * u - u))) *\<^sub>R a + (1 + (u / (1 + D * u - u))) *\<^sub>R y"
+      also have "\<dots> = (1 + (u / (1 + D * u - u))) *\<^sub>R a + (1 + (u / (1 + D * u - u))) *\<^sub>R y"
using DD by (simp add: field_simps)
-      also have "... = y + (1 + (u / (1 + D * u - u))) *\<^sub>R a + (u / (1 + D * u - u)) *\<^sub>R y"
+      also have "\<dots> = y + (1 + (u / (1 + D * u - u))) *\<^sub>R a + (u / (1 + D * u - u)) *\<^sub>R y"
-      also have "... = y + ((1 / (1 + D * u - u)) *\<^sub>R a +
+      also have "\<dots> = y + ((1 / (1 + D * u - u)) *\<^sub>R a +
((u / (1 + D * u - u)) *\<^sub>R y + (D * u / (1 + D * u - u)) *\<^sub>R a))"
finally have xeq: "(1 - 1 / (1 + (D - 1) * u)) *\<^sub>R a + (1 / (1 + (D - 1) * u)) *\<^sub>R (a + (1 + (D - 1) * u) *\<^sub>R (y - a)) = y"
@@ -2160,7 +2134,7 @@
using \<epsilon> by (force intro: connected_diff_ball [OF \<open>connected S\<close> _ 2])
have "x \<in> \<Union>{S - ball a r |r. 0 < r \<and> r < \<epsilon>}" if "x \<in> S - {a}" for x
apply (rule UnionI [of "S - ball a (min \<epsilon> (dist a x) / 2)"])
-     using that \<open>0 < \<epsilon>\<close> apply (simp_all add:)
+     using that \<open>0 < \<epsilon>\<close> apply simp_all
apply (rule_tac x="min \<epsilon> (dist a x) / 2" in exI)
apply auto
done
@@ -2228,9 +2202,9 @@
by (force simp: sphere_def dist_norm)
have "dist (r *\<^sub>R b) (- r *\<^sub>R b) = norm (r *\<^sub>R b + r *\<^sub>R b)"
-    also have "... = norm ((2*r) *\<^sub>R b)"
+    also have "\<dots> = norm ((2*r) *\<^sub>R b)"
-    also have "... = 2*r"
+    also have "\<dots> = 2*r"
using \<open>r > 0\<close> b norm_Basis by fastforce
finally show "dist (r *\<^sub>R b) (- r *\<^sub>R b) = 2*r" .
qed
@@ -2258,7 +2232,7 @@
obtain b where "dist a b = r" and "b \<notin> S"
using S mem_sphere by blast
have CS: "- S = {x. dist a x \<le> r \<and> (x \<notin> S)} \<union> {x. r \<le> dist a x \<and> (x \<notin> S)}"
-    by (auto simp: )
+    by auto
have "{x. dist a x \<le> r \<and> x \<notin> S} \<inter> {x. r \<le> dist a x \<and> x \<notin> S} \<noteq> {}"
using \<open>b \<notin> S\<close> \<open>dist a b = r\<close> by blast
moreover have "connected {x. dist a x \<le> r \<and> x \<notin> S}"
@@ -2451,7 +2425,7 @@
obtain B where B: "B>0" "-s \<subseteq> ball 0 B"
using bounded_subset_ballD [OF assms, of 0] by auto
then have *: "\<And>x. B \<le> norm x \<Longrightarrow> x \<in> s"
-    by (force simp add: ball_def dist_norm)
+    by (force simp: ball_def dist_norm)
have unbounded_inner: "~ bounded {x. inner i x \<ge> B}"
apply (auto simp: bounded_def dist_norm)
apply (rule_tac x="x + (max B e + 1 + \<bar>i \<bullet> x\<bar>) *\<^sub>R i" in exI)
@@ -2486,7 +2460,7 @@
obtain B where B: "B>0" "-s \<subseteq> ball 0 B"
using bounded_subset_ballD [OF bs, of 0] by auto
then have *: "\<And>x. B \<le> norm x \<Longrightarrow> x \<in> s"
-    by (force simp add: ball_def dist_norm)
+    by (force simp: ball_def dist_norm)
have ccb: "connected (- ball 0 B :: 'a set)"
using assms by (auto intro: connected_complement_bounded_convex)
obtain x' where x': "connected_component s x x'" "norm x' > B"
@@ -2531,47 +2505,47 @@
The outside comprises the points in unbounded connected component of the complement.\<close>

definition%important inside where
-  "inside s \<equiv> {x. (x \<notin> s) \<and> bounded(connected_component_set ( - s) x)}"
+  "inside S \<equiv> {x. (x \<notin> S) \<and> bounded(connected_component_set ( - S) x)}"

definition%important outside where
-  "outside s \<equiv> -s \<inter> {x. ~ bounded(connected_component_set (- s) x)}"
-
-lemma outside: "outside s = {x. ~ bounded(connected_component_set (- s) x)}"
+  "outside S \<equiv> -S \<inter> {x. ~ bounded(connected_component_set (- S) x)}"
+
+lemma outside: "outside S = {x. ~ bounded(connected_component_set (- S) x)}"
by (auto simp: outside_def) (metis Compl_iff bounded_empty connected_component_eq_empty)

-lemma inside_no_overlap [simp]: "inside s \<inter> s = {}"
+lemma inside_no_overlap [simp]: "inside S \<inter> S = {}"
by (auto simp: inside_def)

lemma outside_no_overlap [simp]:
-   "outside s \<inter> s = {}"
+   "outside S \<inter> S = {}"
by (auto simp: outside_def)

-lemma inside_Int_outside [simp]: "inside s \<inter> outside s = {}"
+lemma inside_Int_outside [simp]: "inside S \<inter> outside S = {}"
by (auto simp: inside_def outside_def)

-lemma inside_Un_outside [simp]: "inside s \<union> outside s = (- s)"
+lemma inside_Un_outside [simp]: "inside S \<union> outside S = (- S)"
by (auto simp: inside_def outside_def)

lemma inside_eq_outside:
-   "inside s = outside s \<longleftrightarrow> s = UNIV"
+   "inside S = outside S \<longleftrightarrow> S = UNIV"
by (auto simp: inside_def outside_def)

-lemma inside_outside: "inside s = (- (s \<union> outside s))"
-  by (force simp add: inside_def outside)
-
-lemma outside_inside: "outside s = (- (s \<union> inside s))"
+lemma inside_outside: "inside S = (- (S \<union> outside S))"
+  by (force simp: inside_def outside)
+
+lemma outside_inside: "outside S = (- (S \<union> inside S))"
by (auto simp: inside_outside) (metis IntI equals0D outside_no_overlap)

-lemma union_with_inside: "s \<union> inside s = - outside s"
+lemma union_with_inside: "S \<union> inside S = - outside S"
by (auto simp: inside_outside) (simp add: outside_inside)

-lemma union_with_outside: "s \<union> outside s = - inside s"
+lemma union_with_outside: "S \<union> outside S = - inside S"

-lemma outside_mono: "s \<subseteq> t \<Longrightarrow> outside t \<subseteq> outside s"
+lemma outside_mono: "S \<subseteq> T \<Longrightarrow> outside T \<subseteq> outside S"
by (auto simp: outside bounded_subset connected_component_mono)

-lemma inside_mono: "s \<subseteq> t \<Longrightarrow> inside s - t \<subseteq> inside t"
+lemma inside_mono: "S \<subseteq> T \<Longrightarrow> inside S - T \<subseteq> inside T"
by (auto simp: inside_def bounded_subset connected_component_mono)

lemma segment_bound_lemma:
@@ -2586,80 +2560,81 @@
qed

lemma cobounded_outside:
-  fixes s :: "'a :: real_normed_vector set"
-  assumes "bounded s" shows "bounded (- outside s)"
+  fixes S :: "'a :: real_normed_vector set"
+  assumes "bounded S" shows "bounded (- outside S)"
proof -
-  obtain B where B: "B>0" "s \<subseteq> ball 0 B"
+  obtain B where B: "B>0" "S \<subseteq> ball 0 B"
using bounded_subset_ballD [OF assms, of 0] by auto
{ fix x::'a and C::real
assume Bno: "B \<le> norm x" and C: "0 < C"
-    have "\<exists>y. connected_component (- s) x y \<and> norm y > C"
+    have "\<exists>y. connected_component (- S) x y \<and> norm y > C"
proof (cases "x = 0")
case True with B Bno show ?thesis by force
next
-      case False with B C show ?thesis
-        apply (rule_tac x="((B+C)/norm x) *\<^sub>R x" in exI)
-        apply (rule_tac x="closed_segment x (((B+C)/norm x) *\<^sub>R x)" in exI)
-        apply simp
-        apply (rule_tac y="- ball 0 B" in order_trans)
-         prefer 2 apply force
-        apply (simp add: closed_segment_def ball_def dist_norm, clarify)
+      case False
+      with B C
+      have "closed_segment x (((B + C) / norm x) *\<^sub>R x) \<subseteq> - ball 0 B"
using segment_bound_lemma [of B "norm x" "B+C" ] Bno
+      also have "... \<subseteq> -S"
+      finally have "\<exists>T. connected T \<and> T \<subseteq> - S \<and> x \<in> T \<and> ((B + C) / norm x) *\<^sub>R x \<in> T"
+        by (rule_tac x="closed_segment x (((B+C)/norm x) *\<^sub>R x)" in exI) simp
+      with False B
+      show ?thesis
+        by (rule_tac x="((B+C)/norm x) *\<^sub>R x" in exI) (simp add: connected_component_def)
qed
}
then show ?thesis
apply (rule bounded_subset [OF bounded_ball [of 0 B]])
-    apply (force simp add: dist_norm not_less bounded_pos)
+    apply (force simp: dist_norm not_less bounded_pos)
done
qed

lemma unbounded_outside:
-    fixes s :: "'a::{real_normed_vector, perfect_space} set"
-    shows "bounded s \<Longrightarrow> ~ bounded(outside s)"
+    fixes S :: "'a::{real_normed_vector, perfect_space} set"
+    shows "bounded S \<Longrightarrow> ~ bounded(outside S)"
using cobounded_imp_unbounded cobounded_outside by blast

lemma bounded_inside:
-    fixes s :: "'a::{real_normed_vector, perfect_space} set"
-    shows "bounded s \<Longrightarrow> bounded(inside s)"
+    fixes S :: "'a::{real_normed_vector, perfect_space} set"
+    shows "bounded S \<Longrightarrow> bounded(inside S)"
by (simp add: bounded_Int cobounded_outside inside_outside)

lemma connected_outside:
-    fixes s :: "'a::euclidean_space set"
-    assumes "bounded s" "2 \<le> DIM('a)"
-      shows "connected(outside s)"
-  apply (simp add: connected_iff_connected_component, clarify)
-  apply (rule_tac s="connected_component_set (- s) x" in connected_component_of_subset)
+    fixes S :: "'a::euclidean_space set"
+    assumes "bounded S" "2 \<le> DIM('a)"
+      shows "connected(outside S)"
+  apply (clarsimp simp add: connected_iff_connected_component outside)
+  apply (rule_tac s="connected_component_set (- S) x" in connected_component_of_subset)
apply (metis (no_types) assms cobounded_unbounded_component cobounded_unique_unbounded_component connected_component_eq_eq connected_component_idemp double_complement mem_Collect_eq)
apply clarify
apply (metis connected_component_eq_eq connected_component_in)
done

lemma outside_connected_component_lt:
-    "outside s = {x. \<forall>B. \<exists>y. B < norm(y) \<and> connected_component (- s) x y}"
+    "outside S = {x. \<forall>B. \<exists>y. B < norm(y) \<and> connected_component (- S) x y}"
apply (auto simp: outside bounded_def dist_norm)
apply (metis diff_0 norm_minus_cancel not_less)
by (metis less_diff_eq norm_minus_commute norm_triangle_ineq2 order.trans pinf(6))

lemma outside_connected_component_le:
-   "outside s =
+   "outside S =
{x. \<forall>B. \<exists>y. B \<le> norm(y) \<and>
-                         connected_component (- s) x y}"
+                         connected_component (- S) x y}"
by (meson gt_ex leD le_less_linear less_imp_le order.trans)

lemma not_outside_connected_component_lt:
-    fixes s :: "'a::euclidean_space set"
-    assumes s: "bounded s" and "2 \<le> DIM('a)"
-      shows "- (outside s) = {x. \<forall>B. \<exists>y. B < norm(y) \<and> ~ (connected_component (- s) x y)}"
+    fixes S :: "'a::euclidean_space set"
+    assumes S: "bounded S" and "2 \<le> DIM('a)"
+      shows "- (outside S) = {x. \<forall>B. \<exists>y. B < norm(y) \<and> ~ (connected_component (- S) x y)}"
proof -
-  obtain B::real where B: "0 < B" and Bno: "\<And>x. x \<in> s \<Longrightarrow> norm x \<le> B"
-    using s [simplified bounded_pos] by auto
+  obtain B::real where B: "0 < B" and Bno: "\<And>x. x \<in> S \<Longrightarrow> norm x \<le> B"
+    using S [simplified bounded_pos] by auto
{ fix y::'a and z::'a
assume yz: "B < norm z" "B < norm y"
have "connected_component (- cball 0 B) y z"
@@ -2667,7 +2642,7 @@
apply (rule connected_complement_bounded_convex)
using assms yz
by (auto simp: dist_norm)
-    then have "connected_component (- s) y z"
+    then have "connected_component (- S) y z"
apply (rule connected_component_of_subset)
apply (metis Bno Compl_anti_mono mem_cball_0 subset_iff)
done
@@ -2680,29 +2655,29 @@
qed

lemma not_outside_connected_component_le:
-    fixes s :: "'a::euclidean_space set"
-    assumes s: "bounded s"  "2 \<le> DIM('a)"
-      shows "- (outside s) = {x. \<forall>B. \<exists>y. B \<le> norm(y) \<and> ~ (connected_component (- s) x y)}"
+    fixes S :: "'a::euclidean_space set"
+    assumes S: "bounded S"  "2 \<le> DIM('a)"
+      shows "- (outside S) = {x. \<forall>B. \<exists>y. B \<le> norm(y) \<and> ~ (connected_component (- S) x y)}"
apply (auto intro: less_imp_le simp: not_outside_connected_component_lt [OF assms])
by (meson gt_ex less_le_trans)

lemma inside_connected_component_lt:
-    fixes s :: "'a::euclidean_space set"
-    assumes s: "bounded s"  "2 \<le> DIM('a)"
-      shows "inside s = {x. (x \<notin> s) \<and> (\<forall>B. \<exists>y. B < norm(y) \<and> ~(connected_component (- s) x y))}"
+    fixes S :: "'a::euclidean_space set"
+    assumes S: "bounded S"  "2 \<le> DIM('a)"
+      shows "inside S = {x. (x \<notin> S) \<and> (\<forall>B. \<exists>y. B < norm(y) \<and> ~(connected_component (- S) x y))}"
by (auto simp: inside_outside not_outside_connected_component_lt [OF assms])

lemma inside_connected_component_le:
-    fixes s :: "'a::euclidean_space set"
-    assumes s: "bounded s"  "2 \<le> DIM('a)"
-      shows "inside s = {x. (x \<notin> s) \<and> (\<forall>B. \<exists>y. B \<le> norm(y) \<and> ~(connected_component (- s) x y))}"
+    fixes S :: "'a::euclidean_space set"
+    assumes S: "bounded S"  "2 \<le> DIM('a)"
+      shows "inside S = {x. (x \<notin> S) \<and> (\<forall>B. \<exists>y. B \<le> norm(y) \<and> ~(connected_component (- S) x y))}"
by (auto simp: inside_outside not_outside_connected_component_le [OF assms])

lemma inside_subset:
-  assumes "connected u" and "~bounded u" and "t \<union> u = - s"
-  shows "inside s \<subseteq> t"
+  assumes "connected U" and "~bounded U" and "T \<union> U = - S"
+  shows "inside S \<subseteq> T"
apply (auto simp: inside_def)
-by (metis bounded_subset [of "connected_component_set (- s) _"] connected_component_maximal
+by (metis bounded_subset [of "connected_component_set (- S) _"] connected_component_maximal
Compl_iff Un_iff assms subsetI)

lemma frontier_not_empty:
@@ -2959,7 +2934,7 @@
proof -
have "Y \<subseteq> connected_component_set (- (T \<union> U)) x"
-    also have "... \<subseteq> outside(T \<union> U)"
+    also have "\<dots> \<subseteq> outside(T \<union> U)"
by (metis (mono_tags, lifting) Collect_mono mem_Collect_eq outside outside_same_component x)
finally have "Y \<subseteq> outside(T \<union> U)" .
with assms show ?thesis by auto
@@ -2996,7 +2971,7 @@
shows "\<lbrakk>bounded s; convex s\<rbrakk> \<Longrightarrow> inside(frontier s) = interior s"
using closure_subset interior_subset
-  apply (auto simp add: frontier_def)
+  apply (auto simp: frontier_def)
done

lemma open_inside:
@@ -3234,8 +3209,7 @@
using that proof
assume "a \<in> s" then show ?thesis
apply (rule_tac x=a in exI)
-      apply (rule_tac x="{a}" in exI)
+      apply (rule_tac x="{a}" in exI, simp)
done
next
assume a: "a \<in> inside s"
@@ -3273,8 +3247,7 @@
using that proof
assume "a \<in> s" then show ?thesis
apply (rule_tac x=a in exI)
-      apply (rule_tac x="{a}" in exI)
+      apply (rule_tac x="{a}" in exI, simp)
done
next
assume a: "a \<in> outside s"
@@ -3358,7 +3331,7 @@
done
then have ftendsw: "((\<lambda>n. f (z n)) \<circ> K) \<longlonglongrightarrow> w"
by (metis LIMSEQ_subseq_LIMSEQ fun.map_cong0 fz tendsw)
-    have zKs: "\<And>n. (z o K) n \<in> S" by (simp add: zs)
+    have zKs: "\<And>n. (z \<circ> K) n \<in> S" by (simp add: zs)
have fz: "f \<circ> z = \<xi>"  "(\<lambda>n. f (z n)) = \<xi>"
using fz by auto
then have "(\<xi> \<circ> K) \<longlonglongrightarrow> f y"
@@ -3411,7 +3384,7 @@
unfolding homotopic_with_def
apply (rule iffI, blast, clarify)
apply (rule_tac x="\<lambda>(u,v). if v \<in> X then h(u,v) else if u = 0 then p v else q v" in exI)
-  apply (auto simp:)
+  apply auto
apply (force elim: continuous_on_eq)
apply (drule_tac x=t in bspec, force)
apply (subst assms; simp)
@@ -3427,8 +3400,7 @@
apply safe
apply (rule_tac x="\<lambda>(u,v). if v \<in> X then h(u,v) else if u = 0 then f' v else g' v" in exI)
apply (simp add: f' g', safe)
-  apply (fastforce intro: continuous_on_eq)
-  apply fastforce
+  apply (fastforce intro: continuous_on_eq, fastforce)
apply (subst P; fastforce)
done

@@ -3441,7 +3413,7 @@
apply (rule_tac x="\<lambda>(u,v). if u = 1 then g v else f v" in exI)
using assms
apply (intro conjI)
-  apply (rule continuous_on_eq [where f = "f o snd"])
+  apply (rule continuous_on_eq [where f = "f \<circ> snd"])
apply (rule continuous_intros | force)+
apply clarify
apply (case_tac "t=1"; force)
@@ -3449,7 +3421,7 @@

lemma image_Pair_const: "(\<lambda>x. (x, c)) ` A = A \<times> {c}"
-  by (auto simp:)
+  by auto

lemma homotopic_constant_maps:
"homotopic_with (\<lambda>x. True) s t (\<lambda>x. a) (\<lambda>x. b) \<longleftrightarrow> s = {} \<or> path_component t a b"
@@ -3468,19 +3440,18 @@
by (auto simp: homotopic_with)
have "continuous_on {0..1} (h \<circ> (\<lambda>t. (t, c)))"
apply (rule continuous_intros conth | simp add: image_Pair_const)+
-      apply (blast intro:  \<open>c \<in> s\<close> continuous_on_subset [OF conth] )
+      apply (blast intro:  \<open>c \<in> s\<close> continuous_on_subset [OF conth])
done
with \<open>c \<in> s\<close> h show "s = {} \<or> path_component t a b"
-      apply (simp_all add: homotopic_with path_component_def)
-      apply (auto simp:)
-      apply (drule_tac x="h o (\<lambda>t. (t, c))" in spec)
+      apply (simp_all add: homotopic_with path_component_def, auto)
+      apply (drule_tac x="h \<circ> (\<lambda>t. (t, c))" in spec)
apply (auto simp: pathstart_def pathfinish_def path_image_def path_def)
done
next
assume "s = {} \<or> path_component t a b"
with False show "homotopic_with (\<lambda>x. True) s t (\<lambda>x. a) (\<lambda>x. b)"
apply (clarsimp simp: homotopic_with path_component_def pathstart_def pathfinish_def path_image_def path_def)
-      apply (rule_tac x="g o fst" in exI)
+      apply (rule_tac x="g \<circ> fst" in exI)
apply (rule conjI continuous_intros | force)+
done
qed
@@ -3493,11 +3464,10 @@
unfolding homotopic_with_def Ball_def
apply clarify
apply (frule_tac x=0 in spec)
-  apply (drule_tac x=1 in spec)
-  apply (auto simp:)
+  apply (drule_tac x=1 in spec, auto)
done

-lemma continuous_on_o_Pair: "\<lbrakk>continuous_on (T \<times> X) h; t \<in> T\<rbrakk> \<Longrightarrow> continuous_on X (h o Pair t)"
+lemma continuous_on_o_Pair: "\<lbrakk>continuous_on (T \<times> X) h; t \<in> T\<rbrakk> \<Longrightarrow> continuous_on X (h \<circ> Pair t)"
by (fast intro: continuous_intros elim!: continuous_on_subset)

lemma homotopic_with_imp_continuous:
@@ -3508,7 +3478,7 @@
where conth: "continuous_on ({0..1} \<times> X) h"
and h: "\<forall>x. h (0, x) = f x" "\<forall>x. h (1, x) = g x"
using assms by (auto simp: homotopic_with_def)
-  have *: "t \<in> {0..1} \<Longrightarrow> continuous_on X (h o (\<lambda>x. (t,x)))" for t
+  have *: "t \<in> {0..1} \<Longrightarrow> continuous_on X (h \<circ> (\<lambda>x. (t,x)))" for t
by (rule continuous_intros continuous_on_subset [OF conth] | force)+
show ?thesis
using h *[of 0] *[of 1] by auto
@@ -3546,10 +3516,10 @@

proposition homotopic_with_compose_continuous_right:
"\<lbrakk>homotopic_with (\<lambda>f. p (f \<circ> h)) X Y f g; continuous_on W h; h ` W \<subseteq> X\<rbrakk>
-     \<Longrightarrow> homotopic_with p W Y (f o h) (g o h)"
+     \<Longrightarrow> homotopic_with p W Y (f \<circ> h) (g \<circ> h)"
apply (rename_tac k)
-  apply (rule_tac x="k o (\<lambda>y. (fst y, h (snd y)))" in exI)
+  apply (rule_tac x="k \<circ> (\<lambda>y. (fst y, h (snd y)))" in exI)
apply (rule conjI continuous_intros continuous_on_compose [where f=snd and g=h, unfolded o_def] | simp)+
apply (erule continuous_on_subset)
apply (fastforce simp: o_def)+
@@ -3557,15 +3527,15 @@

proposition homotopic_compose_continuous_right:
"\<lbrakk>homotopic_with (\<lambda>f. True) X Y f g; continuous_on W h; h ` W \<subseteq> X\<rbrakk>
-      \<Longrightarrow> homotopic_with (\<lambda>f. True) W Y (f o h) (g o h)"
+      \<Longrightarrow> homotopic_with (\<lambda>f. True) W Y (f \<circ> h) (g \<circ> h)"
using homotopic_with_compose_continuous_right by fastforce

proposition homotopic_with_compose_continuous_left:
"\<lbrakk>homotopic_with (\<lambda>f. p (h \<circ> f)) X Y f g; continuous_on Y h; h ` Y \<subseteq> Z\<rbrakk>
-      \<Longrightarrow> homotopic_with p X Z (h o f) (h o g)"
+      \<Longrightarrow> homotopic_with p X Z (h \<circ> f) (h \<circ> g)"
apply (rename_tac k)
-  apply (rule_tac x="h o k" in exI)
+  apply (rule_tac x="h \<circ> k" in exI)
apply (rule conjI continuous_intros continuous_on_compose [where f=snd and g=h, unfolded o_def] | simp)+
apply (erule continuous_on_subset)
apply (fastforce simp: o_def)+
@@ -3574,7 +3544,7 @@
proposition homotopic_compose_continuous_left:
"\<lbrakk>homotopic_with (\<lambda>_. True) X Y f g;
continuous_on Y h; h ` Y \<subseteq> Z\<rbrakk>
-    \<Longrightarrow> homotopic_with (\<lambda>f. True) X Z (h o f) (h o g)"
+    \<Longrightarrow> homotopic_with (\<lambda>f. True) X Z (h \<circ> f) (h \<circ> g)"
using homotopic_with_compose_continuous_left by fastforce

proposition homotopic_with_Pair:
@@ -3585,7 +3555,7 @@
using hom
apply (rename_tac k k')
-  apply (rule_tac x="\<lambda>z. ((k o (\<lambda>x. (fst x, fst (snd x)))) z, (k' o (\<lambda>x. (fst x, snd (snd x)))) z)" in exI)
+  apply (rule_tac x="\<lambda>z. ((k \<circ> (\<lambda>x. (fst x, fst (snd x)))) z, (k' \<circ> (\<lambda>x. (fst x, snd (snd x)))) z)" in exI)
apply (rule conjI continuous_intros | erule continuous_on_subset | clarsimp)+
apply (auto intro!: q [unfolded case_prod_unfold])
done
@@ -3603,7 +3573,7 @@
apply (rule iffI)
using homotopic_with_imp_continuous homotopic_with_imp_property homotopic_with_imp_subset2 apply blast
-  apply (rule_tac x="f o snd" in exI)
+  apply (rule_tac x="f \<circ> snd" in exI)
apply (rule conjI continuous_intros | force)+
done

@@ -3614,8 +3584,8 @@
using assms
apply (rename_tac h)
-  apply (rule_tac x="h o (\<lambda>y. (1 - fst y, snd y))" in exI)
-  apply (rule conjI continuous_intros | erule continuous_on_subset | force simp add: image_subset_iff)+
+  apply (rule_tac x="h \<circ> (\<lambda>y. (1 - fst y, snd y))" in exI)
+  apply (rule conjI continuous_intros | erule continuous_on_subset | force simp: image_subset_iff)+
done

proposition homotopic_with_sym:
@@ -3637,12 +3607,12 @@
have clo1: "closedin (subtopology euclidean ({0..1/2} \<times> X \<union> {1/2..1} \<times> X)) ({0..1/2::real} \<times> X)"
apply (simp add: closedin_closed split_01_prod [symmetric])
apply (rule_tac x="{0..1/2} \<times> UNIV" in exI)
-    apply (force simp add: closed_Times)
+    apply (force simp: closed_Times)
done
have clo2: "closedin (subtopology euclidean ({0..1/2} \<times> X \<union> {1/2..1} \<times> X)) ({1/2..1::real} \<times> X)"
apply (simp add: closedin_closed split_01_prod [symmetric])
apply (rule_tac x="{1/2..1} \<times> UNIV" in exI)
-    apply (force simp add: closed_Times)
+    apply (force simp: closed_Times)
done
{ fix k1 k2:: "real \<times> 'a \<Rightarrow> 'b"
assume cont: "continuous_on ({0..1} \<times> X) k1" "continuous_on ({0..1} \<times> X) k2"
@@ -3652,18 +3622,18 @@
and P:   "\<forall>t\<in>{0..1}. P (\<lambda>x. k1 (t, x))" "\<forall>t\<in>{0..1}. P (\<lambda>x. k2 (t, x))"
define k where "k y =
(if fst y \<le> 1 / 2
-       then (k1 o (\<lambda>x. (2 *\<^sub>R fst x, snd x))) y
-       else (k2 o (\<lambda>x. (2 *\<^sub>R fst x -1, snd x))) y)" for y
+       then (k1 \<circ> (\<lambda>x. (2 *\<^sub>R fst x, snd x))) y
+       else (k2 \<circ> (\<lambda>x. (2 *\<^sub>R fst x -1, snd x))) y)" for y
have keq: "k1 (2 * u, v) = k2 (2 * u - 1, v)" if "u = 1/2"  for u v
have "continuous_on ({0..1} \<times> X) k"
using cont
apply (rule clo1 clo2 continuous_on_cases_local continuous_intros | erule continuous_on_subset | simp add: linear image_subset_iff)+
-      apply (force simp add: keq)
+      apply (force simp: keq)
done
moreover have "k ` ({0..1} \<times> X) \<subseteq> Y"
-      using Y by (force simp add: k_def)
+      using Y by (force simp: k_def)
moreover have "\<forall>x. k (0, x) = f x"
moreover have "(\<forall>x. k (1, x) = h x)"
@@ -3671,8 +3641,7 @@
moreover have "\<forall>t\<in>{0..1}. P (\<lambda>x. k (t, x))"
using P
-      apply (case_tac "t \<le> 1/2")
-      apply (auto simp:)
+      apply (case_tac "t \<le> 1/2", auto)
done
ultimately have *: "\<exists>k :: real \<times> 'a \<Rightarrow> 'b.
continuous_on ({0..1} \<times> X) k \<and> k ` ({0..1} \<times> X) \<subseteq> Y \<and>
@@ -3686,8 +3655,8 @@
proposition homotopic_compose:
fixes s :: "'a::real_normed_vector set"
shows "\<lbrakk>homotopic_with (\<lambda>x. True) s t f f'; homotopic_with (\<lambda>x. True) t u g g'\<rbrakk>
-             \<Longrightarrow> homotopic_with (\<lambda>x. True) s u (g o f) (g' o f')"
-  apply (rule homotopic_with_trans [where g = "g o f'"])
+             \<Longrightarrow> homotopic_with (\<lambda>x. True) s u (g \<circ> f) (g' \<circ> f')"
+  apply (rule homotopic_with_trans [where g = "g \<circ> f'"])
apply (metis homotopic_compose_continuous_left homotopic_with_imp_continuous homotopic_with_imp_subset1)
by (metis homotopic_compose_continuous_right homotopic_with_imp_continuous homotopic_with_imp_subset2)

@@ -3756,8 +3725,8 @@
h ` ({0..1} \<times> {0..1}) \<subseteq> s \<and>
(\<forall>x \<in> {0..1}. h(0,x) = p x) \<and>
(\<forall>x \<in> {0..1}. h(1,x) = q x) \<and>
-          (\<forall>t \<in> {0..1::real}. pathstart(h o Pair t) = pathstart p \<and>
-                        pathfinish(h o Pair t) = pathfinish p))"
+          (\<forall>t \<in> {0..1::real}. pathstart(h \<circ> Pair t) = pathstart p \<and>
+                        pathfinish(h \<circ> Pair t) = pathfinish p))"
by (auto simp: homotopic_paths_def homotopic_with pathstart_def pathfinish_def)

proposition homotopic_paths_imp_pathstart:
@@ -3809,7 +3778,7 @@
proof -
have contp: "continuous_on {0..1} p"
by (metis \<open>path p\<close> path_def)
-  then have "continuous_on {0..1} (p o f)"
+  then have "continuous_on {0..1} (p \<circ> f)"
using contf continuous_on_compose continuous_on_subset f01 by blast
then have "path q"
by (simp add: path_def) (metis q continuous_on_cong)
@@ -3826,7 +3795,7 @@
next
show "homotopic_paths s (p \<circ> f) p"
-      apply (rule_tac x="p o (\<lambda>y. (1 - (fst y)) *\<^sub>R ((f o snd) y) + (fst y) *\<^sub>R snd y)"  in exI)
+      apply (rule_tac x="p \<circ> (\<lambda>y. (1 - (fst y)) *\<^sub>R ((f \<circ> snd) y) + (fst y) *\<^sub>R snd y)"  in exI)
apply (rule conjI contf continuous_intros continuous_on_subset [OF contp] | simp)+
using pips [unfolded path_image_def]
apply (auto simp: fb0 fb1 pathstart_def pathfinish_def)
@@ -3848,10 +3817,10 @@
and pf: "\<And>t. t \<in> {0..1} \<Longrightarrow> pathfinish(p t) = pathstart(q t)"
shows "continuous_on ({0..1} \<times> {0..1}) (\<lambda>y. (p(fst y) +++ q(fst y)) (snd y))"
proof -
-  have 1: "(\<lambda>y. p (fst y) (2 * snd y)) = (\<lambda>y. p (fst y) (snd y)) o (\<lambda>y. (fst y, 2 * snd y))"
-    by (rule ext) (simp )
-  have 2: "(\<lambda>y. q (fst y) (2 * snd y - 1)) = (\<lambda>y. q (fst y) (snd y)) o (\<lambda>y. (fst y, 2 * snd y - 1))"
-    by (rule ext) (simp )
+  have 1: "(\<lambda>y. p (fst y) (2 * snd y)) = (\<lambda>y. p (fst y) (snd y)) \<circ> (\<lambda>y. (fst y, 2 * snd y))"
+    by (rule ext) (simp)
+  have 2: "(\<lambda>y. q (fst y) (2 * snd y - 1)) = (\<lambda>y. q (fst y) (snd y)) \<circ> (\<lambda>y. (fst y, 2 * snd y - 1))"
+    by (rule ext) (simp)
show ?thesis
apply (rule continuous_on_cases_le)
@@ -3869,7 +3838,7 @@
shows   "homotopic_paths s (reversepath p) (reversepath q)"
using assms
apply (simp add: homotopic_paths_def homotopic_with_def, clarify)
-  apply (rule_tac x="h o (\<lambda>x. (fst x, 1 - snd x))" in exI)
+  apply (rule_tac x="h \<circ> (\<lambda>x. (fst x, 1 - snd x))" in exI)
apply (rule conjI continuous_intros)+
apply (auto simp: reversepath_def pathstart_def pathfinish_def elim!: continuous_on_subset)
done
@@ -3883,13 +3852,13 @@
"\<lbrakk>homotopic_paths s p p'; homotopic_paths s q q'; pathfinish p = pathstart q\<rbrakk> \<Longrightarrow> homotopic_paths s (p +++ q) (p' +++ q')"
apply (simp add: homotopic_paths_def homotopic_with_def, clarify)
apply (rename_tac k1 k2)
-  apply (rule_tac x="(\<lambda>y. ((k1 o Pair (fst y)) +++ (k2 o Pair (fst y))) (snd y))" in exI)
+  apply (rule_tac x="(\<lambda>y. ((k1 \<circ> Pair (fst y)) +++ (k2 \<circ> Pair (fst y))) (snd y))" in exI)
apply (rule conjI continuous_intros homotopic_join_lemma)+
apply (auto simp: joinpaths_def pathstart_def pathfinish_def path_image_def)
done

proposition homotopic_paths_continuous_image:
-    "\<lbrakk>homotopic_paths s f g; continuous_on s h; h ` s \<subseteq> t\<rbrakk> \<Longrightarrow> homotopic_paths t (h o f) (h o g)"
+    "\<lbrakk>homotopic_paths s f g; continuous_on s h; h ` s \<subseteq> t\<rbrakk> \<Longrightarrow> homotopic_paths t (h \<circ> f) (h \<circ> g)"
unfolding homotopic_paths_def
apply (rule homotopic_with_compose_continuous_left [of _ _ _ s])
apply (auto simp: pathstart_def pathfinish_def elim!: homotopic_with_mono)
@@ -3970,7 +3939,7 @@
image h ({0..1} \<times> {0..1}) \<subseteq> s \<and>
(\<forall>x \<in> {0..1}. h(0,x) = p x) \<and>
(\<forall>x \<in> {0..1}. h(1,x) = q x) \<and>
-          (\<forall>t \<in> {0..1}. pathfinish(h o Pair t) = pathstart(h o Pair t)))"
+          (\<forall>t \<in> {0..1}. pathfinish(h \<circ> Pair t) = pathstart(h \<circ> Pair t)))"
by (simp add: homotopic_loops_def pathstart_def pathfinish_def homotopic_with)

proposition homotopic_loops_imp_loop:
@@ -4221,7 +4190,7 @@
using assms
unfolding path_def
apply (simp add: closed_segment_def pathstart_def pathfinish_def homotopic_paths_def homotopic_with_def)
-  apply (rule_tac x="\<lambda>y. ((1 - (fst y)) *\<^sub>R (g o snd) y + (fst y) *\<^sub>R (h o snd) y)" in exI)
+  apply (rule_tac x="\<lambda>y. ((1 - (fst y)) *\<^sub>R (g \<circ> snd) y + (fst y) *\<^sub>R (h \<circ> snd) y)" in exI)
apply (intro conjI subsetI continuous_intros; force)
done

@@ -4335,8 +4304,7 @@
have "homotopic_paths s (subpath u w g +++ subpath w v g) ((subpath u v g +++ subpath v w g) +++ subpath w v g)"
apply (rule homotopic_paths_join)
using hom homotopic_paths_sym_eq apply blast
-    apply (metis \<open>path g\<close> homotopic_paths_eq pag path_image_subpath_subset path_subpath subset_trans v w)
+    apply (metis \<open>path g\<close> homotopic_paths_eq pag path_image_subpath_subset path_subpath subset_trans v w, simp)
done
also have "homotopic_paths s ((subpath u v g +++ subpath v w g) +++ subpath w v g) (subpath u v g +++ subpath v w g +++ subpath w v g)"
apply (rule homotopic_paths_sym [OF homotopic_paths_assoc])
@@ -4346,7 +4314,7 @@
apply (rule homotopic_paths_join)
apply (metis \<open>path g\<close> homotopic_paths_eq order.trans pag path_image_subpath_subset path_subpath u v)
apply (metis (no_types, lifting) \<open>path g\<close> homotopic_paths_linv order_trans pag path_image_subpath_subset path_subpath pathfinish_subpath reversepath_subpath v w)
+    apply simp
done
also have "homotopic_paths s (subpath u v g +++ linepath (pathfinish (subpath u v g)) (pathfinish (subpath u v g))) (subpath u v g)"
apply (rule homotopic_paths_rid)
@@ -4370,7 +4338,7 @@
"path_component S a b \<Longrightarrow> homotopic_loops S (linepath a a) (linepath b b)"
apply (simp add: path_component_def homotopic_loops_def homotopic_with_def
pathstart_def pathfinish_def path_image_def path_def, clarify)
-apply (rule_tac x="g o fst" in exI)
+apply (rule_tac x="g \<circ> fst" in exI)
apply (intro conjI continuous_intros continuous_on_compose)+
apply (auto elim!: continuous_on_subset)
done
@@ -4380,7 +4348,7 @@
\<Longrightarrow> path_component S (p t) (q t)"
apply (simp add: path_component_def homotopic_loops_def homotopic_with_def
pathstart_def pathfinish_def path_image_def path_def, clarify)
-apply (rule_tac x="h o (\<lambda>u. (u, t))" in exI)
+apply (rule_tac x="h \<circ> (\<lambda>u. (u, t))" in exI)
apply (intro conjI continuous_intros continuous_on_compose)+
apply (auto elim!: continuous_on_subset)
done
@@ -4547,10 +4515,10 @@
done
moreover have "path_image (fst \<circ> p) \<subseteq> S"
using that apply (simp add: path_image_def) by force
-    ultimately have p1: "homotopic_loops S (fst o p) (linepath a a)"
+    ultimately have p1: "homotopic_loops S (fst \<circ> p) (linepath a a)"
using S that
-      apply (drule_tac x="fst o p" in spec)
+      apply (drule_tac x="fst \<circ> p" in spec)
apply (drule_tac x=a in spec)
apply (auto simp: pathstart_def pathfinish_def)
done
@@ -4560,10 +4528,10 @@
done
moreover have "path_image (snd \<circ> p) \<subseteq> T"
using that apply (simp add: path_image_def) by force
-    ultimately have p2: "homotopic_loops T (snd o p) (linepath b b)"
+    ultimately have p2: "homotopic_loops T (snd \<circ> p) (linepath b b)"
using T that
-      apply (drule_tac x="snd o p" in spec)
+      apply (drule_tac x="snd \<circ> p" in spec)
apply (drule_tac x=b in spec)
apply (auto simp: pathstart_def pathfinish_def)
done
@@ -4594,15 +4562,14 @@
next
case False
obtain a where a: "homotopic_with (\<lambda>x. True) S S id (\<lambda>x. a)"
-    using assms by (force simp add: contractible_def)
+    using assms by (force simp: contractible_def)
then have "a \<in> S"
by (metis False homotopic_constant_maps homotopic_with_symD homotopic_with_trans path_component_mem(2))
show ?thesis
apply (rule bexI [OF _ \<open>a \<in> S\<close>])
-    using a apply (simp add: homotopic_loops_def homotopic_with_def path_def path_image_def pathfinish_def pathstart_def)
-    apply clarify
-    apply (rule_tac x="(h o (\<lambda>y. (fst y, (p \<circ> snd) y)))" in exI)
+    using a apply (simp add: homotopic_loops_def homotopic_with_def path_def path_image_def pathfinish_def pathstart_def, clarify)
+    apply (rule_tac x="(h \<circ> (\<lambda>y. (fst y, (p \<circ> snd) y)))" in exI)
apply (intro conjI continuous_on_compose continuous_intros)
apply (erule continuous_on_subset | force)+
done
@@ -4623,10 +4590,10 @@
assumes f: "continuous_on S f" "f ` S \<subseteq> T"
and g: "continuous_on T g" "g ` T \<subseteq> U"
and T: "contractible T"
-    obtains c where "homotopic_with (\<lambda>h. True) S U (g o f) (\<lambda>x. c)"
+    obtains c where "homotopic_with (\<lambda>h. True) S U (g \<circ> f) (\<lambda>x. c)"
proof -
obtain b where b: "homotopic_with (\<lambda>x. True) T T id (\<lambda>x. b)"
-    using assms by (force simp add: contractible_def)
+    using assms by (force simp: contractible_def)
have "homotopic_with (\<lambda>f. True) T U (g \<circ> id) (g \<circ> (\<lambda>x. b))"
by (rule homotopic_compose_continuous_left [OF b g])
then have "homotopic_with (\<lambda>f. True) S U (g \<circ> id \<circ> f) (g \<circ> (\<lambda>x. b) \<circ> f)"
@@ -4660,15 +4627,15 @@
"continuous_on S f2" "f2 ` S \<subseteq> T"
"continuous_on T g2" "g2 ` T \<subseteq> U"
"contractible T" "path_connected U"
-   shows "homotopic_with (\<lambda>h. True) S U (g1 o f1) (g2 o f2)"
+   shows "homotopic_with (\<lambda>h. True) S U (g1 \<circ> f1) (g2 \<circ> f2)"
proof -
-  obtain c1 where c1: "homotopic_with (\<lambda>h. True) S U (g1 o f1) (\<lambda>x. c1)"
+  obtain c1 where c1: "homotopic_with (\<lambda>h. True) S U (g1 \<circ> f1) (\<lambda>x. c1)"
apply (rule nullhomotopic_through_contractible [of S f1 T g1 U])
-    using assms apply (auto simp: )
+    using assms apply auto
done
-  obtain c2 where c2: "homotopic_with (\<lambda>h. True) S U (g2 o f2) (\<lambda>x. c2)"
+  obtain c2 where c2: "homotopic_with (\<lambda>h. True) S U (g2 \<circ> f2) (\<lambda>x. c2)"
apply (rule nullhomotopic_through_contractible [of S f2 T g2 U])
-    using assms apply (auto simp: )
+    using assms apply auto
done
have *: "S = {} \<or> (\<exists>t. path_connected t \<and> t \<subseteq> U \<and> c2 \<in> t \<and> c1 \<in> t)"
proof (cases "S = {}")
@@ -4712,15 +4679,14 @@
obtains a where "homotopic_with P S S (\<lambda>x. x) (\<lambda>x. a)"
proof -
obtain a where "a \<in> S" and a: "\<And>x. x \<in> S \<Longrightarrow> closed_segment a x \<subseteq> S"
-    using S by (auto simp add: starlike_def)
+    using S by (auto simp: starlike_def)
have "(\<lambda>y. (1 - fst y) *\<^sub>R snd y + fst y *\<^sub>R a) ` ({0..1} \<times> S) \<subseteq> S"
apply clarify
-    apply (erule a [unfolded closed_segment_def, THEN subsetD])
+    apply (erule a [unfolded closed_segment_def, THEN subsetD], simp)
done
then show ?thesis
-    apply (rule_tac a="a" in that)
+    apply (rule_tac a=a in that)
using \<open>a \<in> S\<close>
apply (rule_tac x="\<lambda>y. (1 - (fst y)) *\<^sub>R snd y + (fst y) *\<^sub>R a" in exI)
@@ -4806,12 +4772,12 @@
and hsub: "h ` ({0..1} \<times> S) \<subseteq> S"
and [simp]: "\<And>x. x \<in> S \<Longrightarrow> h (0, x) = x"
and [simp]: "\<And>x. x \<in> S \<Longrightarrow>  h (1::real, x) = a"
-    using S by (auto simp add: contractible_def homotopic_with)
+    using S by (auto simp: contractible_def homotopic_with)
obtain b k where contk: "continuous_on ({0..1} \<times> T) k"
and ksub: "k ` ({0..1} \<times> T) \<subseteq> T"
and [simp]: "\<And>x. x \<in> T \<Longrightarrow> k (0, x) = x"
and [simp]: "\<And>x. x \<in> T \<Longrightarrow>  k (1::real, x) = b"
-    using T by (auto simp add: contractible_def homotopic_with)
+    using T by (auto simp: contractible_def homotopic_with)
show ?thesis
apply (rule exI [where x=a])
@@ -4819,7 +4785,7 @@
apply (rule exI [where x = "\<lambda>z. (h (fst z, fst(snd z)), k (fst z, snd(snd z)))"])
apply (intro conjI ballI continuous_intros continuous_on_compose2 [OF conth] continuous_on_compose2 [OF contk])
using hsub ksub
-    apply (auto simp: )
+    apply auto
done
qed

@@ -4828,7 +4794,7 @@
assumes S: "contractible S"
and f: "continuous_on S f" "image f S \<subseteq> T"
and g: "continuous_on T g" "image g T \<subseteq> S"
-      and hom: "homotopic_with (\<lambda>x. True) T T (f o g) id"
+      and hom: "homotopic_with (\<lambda>x. True) T T (f \<circ> g) id"
shows "contractible T"
proof -
obtain b where "homotopic_with (\<lambda>h. True) S T f (\<lambda>x. b)"
@@ -4963,7 +4929,7 @@
using \<open>g ` t = S\<close> \<open>W \<subseteq> t\<close> apply blast
using g \<open>W \<subseteq> t\<close> apply auto[1]
-  have o: "openin (subtopology euclidean S) (g ` W)"
+  have \<circ>: "openin (subtopology euclidean S) (g ` W)"
proof -
have "continuous_on S f"
using f(3) by blast
@@ -6138,7 +6104,7 @@
then show ?thesis
using connected_component_eq_empty by auto
qed
-      also have "... \<subseteq> (S \<inter> f -` C)"
+      also have "\<dots> \<subseteq> (S \<inter> f -` C)"
by (rule connected_component_subset)
finally show "connected_component_set (S \<inter> f -` U) x \<subseteq> (S \<inter> f -` C)" .
qed
@@ -6200,7 +6166,7 @@
by (force simp: \<open>x \<in> S\<close> \<open>f x \<in> U\<close> path_component_refl_eq)
ultimately have "f ` (path_component_set (S \<inter> f -` U) x) \<subseteq> path_component_set U (f x)"
by (meson path_component_maximal)
-       also have  "... \<subseteq> path_component_set U y"
+       also have  "\<dots> \<subseteq> path_component_set U y"
by (simp add: Uyfx path_component_maximal path_component_subset path_component_sym)
finally have fC: "f ` (path_component_set (S \<inter> f -` U) x) \<subseteq> path_component_set U y" .
have cUC: "path_component_set (S \<inter> f -` U) x \<subseteq> (S \<inter> f -` path_component_set U y)"
@@ -6212,7 +6178,7 @@
then show ?thesis
using path_component_path_component by blast
qed
-      also have "... \<subseteq> (S \<inter> f -` path_component_set U y)"
+      also have "\<dots> \<subseteq> (S \<inter> f -` path_component_set U y)"
by (rule path_component_subset)
finally show "path_component_set (S \<inter> f -` U) x \<subseteq> (S \<inter> f -` path_component_set U y)" .
qed
@@ -6366,11 +6332,11 @@
obtain a where x: "x = (\<Sum>v \<in> B. a v *\<^sub>R v)"
using \<open>finite B\<close> \<open>span B = S\<close> \<open>x \<in> S\<close> span_finite by fastforce
have "norm (f x)^2 = norm (\<Sum>v\<in>B. a v *\<^sub>R fb v)^2" by (simp add: sum scale ffb x)
-    also have "... = (\<Sum>v\<in>B. norm ((a v *\<^sub>R fb v))^2)"
+    also have "\<dots> = (\<Sum>v\<in>B. norm ((a v *\<^sub>R fb v))^2)"
apply (rule norm_sum_Pythagorean [OF \<open>finite B\<close>])
apply (rule pairwise_ortho_scaleR [OF pairwise_orth_fb])
done
-    also have "... = norm x ^2"
+    also have "\<dots> = norm x ^2"
by (simp add: x pairwise_ortho_scaleR Borth norm_sum_Pythagorean [OF \<open>finite B\<close>])
finally show ?thesis
@@ -6429,29 +6395,29 @@
using \<open>finite B\<close> \<open>span B = S\<close> \<open>x \<in> S\<close> span_finite by fastforce
have "f x = (\<Sum>v \<in> B. f (a v *\<^sub>R v))"
using linear_sum [OF \<open>linear f\<close>] x by auto
-    also have "... = (\<Sum>v \<in> B. a v *\<^sub>R f v)"
+    also have "\<dots> = (\<Sum>v \<in> B. a v *\<^sub>R f v)"
-    also have "... = (\<Sum>v \<in> B. a v *\<^sub>R fb v)"
+    also have "\<dots> = (\<Sum>v \<in> B. a v *\<^sub>R fb v)"
by (simp add: ffb cong: sum.cong)
finally have *: "f x = (\<Sum>v\<in>B. a v *\<^sub>R fb v)" .
then have "(norm (f x))\<^sup>2 = (norm (\<Sum>v\<in>B. a v *\<^sub>R fb v))\<^sup>2" by simp
-    also have "... = (\<Sum>v\<in>B. norm ((a v *\<^sub>R fb v))^2)"
+    also have "\<dots> = (\<Sum>v\<in>B. norm ((a v *\<^sub>R fb v))^2)"
apply (rule norm_sum_Pythagorean [OF \<open>finite B\<close>])
apply (rule pairwise_ortho_scaleR [OF pairwise_orth_fb])
done
-    also have "... = (norm x)\<^sup>2"
+    also have "\<dots> = (norm x)\<^sup>2"
by (simp add: x pairwise_ortho_scaleR Borth norm_sum_Pythagorean [OF \<open>finite B\<close>])
finally show "norm (f x) = norm x"
have "g (f x) = g (\<Sum>v\<in>B. a v *\<^sub>R fb v)" by (simp add: *)
-    also have "... = (\<Sum>v\<in>B. g (a v *\<^sub>R fb v))"
+    also have "\<dots> = (\<Sum>v\<in>B. g (a v *\<^sub>R fb v))"
-    also have "... = (\<Sum>v\<in>B. a v *\<^sub>R g (fb v))"
+    also have "\<dots> = (\<Sum>v\<in>B. a v *\<^sub>R g (fb v))"
-    also have "... = (\<Sum>v\<in>B. a v *\<^sub>R v)"
+    also have "\<dots> = (\<Sum>v\<in>B. a v *\<^sub>R v)"
apply (rule sum.cong [OF refl])
using \<open>bij_betw fb B C\<close> gb_def bij_betwE bij_betw_inv_into_left gb_def ggb by fastforce
-    also have "... = x"
+    also have "\<dots> = x"
using x by blast
finally show "g (f x) = x" .
qed
@@ -6463,19 +6429,19 @@
using \<open>finite C\<close> \<open>span C = T\<close> \<open>x \<in> T\<close> span_finite by fastforce
have "g x = (\<Sum>v \<in> C. g (a v *\<^sub>R v))"
-    also have "... = (\<Sum>v \<in> C. a v *\<^sub>R g v)"
+    also have "\<dots> = (\<Sum>v \<in> C. a v *\<^sub>R g v)"
-    also have "... = (\<Sum>v \<in> C. a v *\<^sub>R gb v)"
+    also have "\<dots> = (\<Sum>v \<in> C. a v *\<^sub>R gb v)"
by (simp add: ggb cong: sum.cong)
finally have "f (g x) = f (\<Sum>v\<in>C. a v *\<^sub>R gb v)" by simp
-    also have "... = (\<Sum>v\<in>C. f (a v *\<^sub>R gb v))"
+    also have "\<dots> = (\<Sum>v\<in>C. f (a v *\<^sub>R gb v))"
-    also have "... = (\<Sum>v\<in>C. a v *\<^sub>R f (gb v))"
+    also have "\<dots> = (\<Sum>v\<in>C. a v *\<^sub>R f (gb v))"
-    also have "... = (\<Sum>v\<in>C. a v *\<^sub>R v)"
+    also have "\<dots> = (\<Sum>v\<in>C. a v *\<^sub>R v)"
using \<open>bij_betw fb B C\<close>
by (simp add: bij_betw_def gb_def bij_betw_inv_into_right ffb inv_into_into)
-    also have "... = x"
+    also have "\<dots> = x"
using x by blast
finally show "f (g x) = x" .
qed
@@ -6508,7 +6474,7 @@
where "linear f" "linear g"
"\<And>x. norm(f x) = norm x" "\<And>y. norm(g y) = norm y"
"\<And>x. g (f x) = x" "\<And>y. f(g y) = y"
-  using assms by (auto simp: intro: isometries_subspaces [of "UNIV::'M set" "UNIV::'N set"])
+  using assms by (auto intro: isometries_subspaces [of "UNIV::'M set" "UNIV::'N set"])

lemma homeomorphic_subspaces:
fixes S :: "'a::euclidean_space set"
@@ -6544,9 +6510,9 @@
using assms ab  by (simp add: aff_dim_eq_dim  [OF hull_inc] image_def)
have "S homeomorphic ((+) (- a) ` S)"
-  also have "... homeomorphic ((+) (- b) ` T)"
+  also have "\<dots> homeomorphic ((+) (- b) ` T)"
by (rule homeomorphic_subspaces [OF ss dd])
-  also have "... homeomorphic T"
+  also have "\<dots> homeomorphic T"
using homeomorphic_sym homeomorphic_translation by auto
finally show ?thesis .
qed
@@ -6564,8 +6530,8 @@
begin

lemma homotopically_trivial_retraction_gen:
-  assumes P: "\<And>f. \<lbrakk>continuous_on u f; f ` u \<subseteq> t; Q f\<rbrakk> \<Longrightarrow> P(k o f)"
-      and Q: "\<And>f. \<lbrakk>continuous_on u f; f ` u \<subseteq> s; P f\<rbrakk> \<Longrightarrow> Q(h o f)"
+  assumes P: "\<And>f. \<lbrakk>continuous_on u f; f ` u \<subseteq> t; Q f\<rbrakk> \<Longrightarrow> P(k \<circ> f)"
+      and Q: "\<And>f. \<lbrakk>continuous_on u f; f ` u \<subseteq> s; P f\<rbrakk> \<Longrightarrow> Q(h \<circ> f)"
and Qeq: "\<And>h k. (\<And>x. x \<in> u \<Longrightarrow> h x = k x) \<Longrightarrow> Q h = Q k"
and hom: "\<And>f g. \<lbrakk>continuous_on u f; f ` u \<subseteq> s; P f;
continuous_on u g; g ` u \<subseteq> s; P g\<rbrakk>
@@ -6602,8 +6568,8 @@
qed

lemma homotopically_trivial_retraction_null_gen:
-  assumes P: "\<And>f. \<lbrakk>continuous_on u f; f ` u \<subseteq> t; Q f\<rbrakk> \<Longrightarrow> P(k o f)"
-      and Q: "\<And>f. \<lbrakk>continuous_on u f; f ` u \<subseteq> s; P f\<rbrakk> \<Longrightarrow> Q(h o f)"
+  assumes P: "\<And>f. \<lbrakk>continuous_on u f; f ` u \<subseteq> t; Q f\<rbrakk> \<Longrightarrow> P(k \<circ> f)"
+      and Q: "\<And>f. \<lbrakk>continuous_on u f; f ` u \<subseteq> s; P f\<rbrakk> \<Longrightarrow> Q(h \<circ> f)"
and Qeq: "\<And>h k. (\<And>x. x \<in> u \<Longrightarrow> h x = k x) \<Longrightarrow> Q h = Q k"
and hom: "\<And>f. \<lbrakk>continuous_on u f; f ` u \<subseteq> s; P f\<rbrakk>
\<Longrightarrow> \<exists>c. homotopic_with P u s f (\<lambda>x. c)"
@@ -6619,7 +6585,7 @@
by (simp add: P Qf contf imf)
ultimately obtain c where "homotopic_with P u s (k \<circ> f) (\<lambda>x. c)"
by (metis hom)
-  then have "homotopic_with Q u t (h \<circ> (k \<circ> f)) (h o (\<lambda>x. c))"
+  then have "homotopic_with Q u t (h \<circ> (k \<circ> f)) (h \<circ> (\<lambda>x. c))"
apply (rule homotopic_with_compose_continuous_left [OF homotopic_with_mono])
using Q by (auto simp: conth imh)
then show ?thesis
@@ -6631,8 +6597,8 @@
qed

lemma cohomotopically_trivial_retraction_gen:
-  assumes P: "\<And>f. \<lbrakk>continuous_on t f; f ` t \<subseteq> u; Q f\<rbrakk> \<Longrightarrow> P(f o h)"
-      and Q: "\<And>f. \<lbrakk>continuous_on s f; f ` s \<subseteq> u; P f\<rbrakk> \<Longrightarrow> Q(f o k)"
+  assumes P: "\<And>f. \<lbrakk>continuous_on t f; f ` t \<subseteq> u; Q f\<rbrakk> \<Longrightarrow> P(f \<circ> h)"
+      and Q: "\<And>f. \<lbrakk>continuous_on s f; f ` s \<subseteq> u; P f\<rbrakk> \<Longrightarrow> Q(f \<circ> k)"
and Qeq: "\<And>h k. (\<And>x. x \<in> t \<Longrightarrow> h x = k x) \<Longrightarrow> Q h = Q k"
and hom: "\<And>f g. \<lbrakk>continuous_on s f; f ` s \<subseteq> u; P f;
continuous_on s g; g ` s \<subseteq> u; P g\<rbrakk>
@@ -6649,15 +6615,15 @@
using imf imh by fastforce
moreover have "P (f \<circ> h)"
by (simp add: P Qf contf imf)
-  moreover have "continuous_on s (g o h)"
+  moreover have "continuous_on s (g \<circ> h)"
using contg continuous_on_compose continuous_on_subset conth imh by blast
moreover have "(g \<circ> h) ` s \<subseteq> u"
using img imh by fastforce
moreover have "P (g \<circ> h)"
by (simp add: P Qg contg img)
-  ultimately have "homotopic_with P s u (f o h) (g \<circ> h)"
+  ultimately have "homotopic_with P s u (f \<circ> h) (g \<circ> h)"
by (rule hom)
-  then have "homotopic_with Q t u (f o h o k) (g \<circ> h o k)"
+  then have "homotopic_with Q t u (f \<circ> h \<circ> k) (g \<circ> h \<circ> k)"
apply (rule homotopic_with_compose_continuous_right [OF homotopic_with_mono])
using Q by (auto simp: contk imk)
then show ?thesis
@@ -6669,8 +6635,8 @@
qed

lemma cohomotopically_trivial_retraction_null_gen:
-  assumes P: "\<And>f. \<lbrakk>continuous_on t f; f ` t \<subseteq> u; Q f\<rbrakk> \<Longrightarrow> P(f o h)"
-      and Q: "\<And>f. \<lbrakk>continuous_on s f; f ` s \<subseteq> u; P f\<rbrakk> \<Longrightarrow> Q(f o k)"
+  assumes P: "\<And>f. \<lbrakk>continuous_on t f; f ` t \<subseteq> u; Q f\<rbrakk> \<Longrightarrow> P(f \<circ> h)"
+      and Q: "\<And>f. \<lbrakk>continuous_on s f; f ` s \<subseteq> u; P f\<rbrakk> \<Longrightarrow> Q(f \<circ> k)"
and Qeq: "\<And>h k. (\<And>x. x \<in> t \<Longrightarrow> h x = k x) \<Longrightarrow> Q h = Q k"
and hom: "\<And>f g. \<lbrakk>continuous_on s f; f ` s \<subseteq> u; P f\<rbrakk>
\<Longrightarrow> \<exists>c. homotopic_with P s u f (\<lambda>x. c)"
@@ -6684,9 +6650,9 @@
using imf imh by fastforce
moreover have "P (f \<circ> h)"
by (simp add: P Qf contf imf)
-  ultimately obtain c where "homotopic_with P s u (f o h) (\<lambda>x. c)"
+  ultimately obtain c where "homotopic_with P s u (f \<circ> h) (\<lambda>x. c)"
by (metis hom)
-  then have "homotopic_with Q t u (f o h o k) ((\<lambda>x. c) o k)"
+  then have "homotopic_with Q t u (f \<circ> h \<circ> k) ((\<lambda>x. c) \<circ> k)"
apply (rule homotopic_with_compose_continuous_right [OF homotopic_with_mono])
using Q by (auto simp: contk imk)
then show ?thesis
@@ -6724,8 +6690,8 @@
where "S homotopy_eqv T \<equiv>
\<exists>f g. continuous_on S f \<and> f ` S \<subseteq> T \<and>
continuous_on T g \<and> g ` T \<subseteq> S \<and>
-              homotopic_with (\<lambda>x. True) S S (g o f) id \<and>
-              homotopic_with (\<lambda>x. True) T T (f o g) id"
+              homotopic_with (\<lambda>x. True) S S (g \<circ> f) id \<and>
+              homotopic_with (\<lambda>x. True) T T (f \<circ> g) id"

lemma homeomorphic_imp_homotopy_eqv: "S homeomorphic T \<Longrightarrow> S homotopy_eqv T"
unfolding homeomorphic_def homotopy_eqv_def homeomorphism_def
@@ -6744,22 +6710,22 @@
proof -
obtain f1 g1 where f1: "continuous_on S f1" "f1 ` S \<subseteq> T"
and g1: "continuous_on T g1" "g1 ` T \<subseteq> S"
-                 and hom1: "homotopic_with (\<lambda>x. True) S S (g1 o f1) id"
-                           "homotopic_with (\<lambda>x. True) T T (f1 o g1) id"
+                 and hom1: "homotopic_with (\<lambda>x. True) S S (g1 \<circ> f1) id"
+                           "homotopic_with (\<lambda>x. True) T T (f1 \<circ> g1) id"
using ST by (auto simp: homotopy_eqv_def)
obtain f2 g2 where f2: "continuous_on T f2" "f2 ` T \<subseteq> U"
and g2: "continuous_on U g2" "g2 ` U \<subseteq> T"
-                 and hom2: "homotopic_with (\<lambda>x. True) T T (g2 o f2) id"
-                           "homotopic_with (\<lambda>x. True) U U (f2 o g2) id"
+                 and hom2: "homotopic_with (\<lambda>x. True) T T (g2 \<circ> f2) id"
+                           "homotopic_with (\<lambda>x. True) U U (f2 \<circ> g2) id"
using TU by (auto simp: homotopy_eqv_def)
have "homotopic_with (\<lambda>f. True) S T (g2 \<circ> f2 \<circ> f1) (id \<circ> f1)"
by (rule homotopic_with_compose_continuous_right hom2 f1)+
then have "homotopic_with (\<lambda>f. True) S T (g2 \<circ> (f2 \<circ> f1)) (id \<circ> f1)"
then have "homotopic_with (\<lambda>x. True) S S
-         (g1 \<circ> (g2 \<circ> (f2 \<circ> f1))) (g1 o (id o f1))"
+         (g1 \<circ> (g2 \<circ> (f2 \<circ> f1))) (g1 \<circ> (id \<circ> f1))"
-  moreover have "homotopic_with (\<lambda>x. True) S S (g1 o id o f1) id"
+  moreover have "homotopic_with (\<lambda>x. True) S S (g1 \<circ> id \<circ> f1) id"
using hom1 by simp
ultimately have SS: "homotopic_with (\<lambda>x. True) S S (g1 \<circ> g2 \<circ> (f2 \<circ> f1)) id"
@@ -6770,9 +6736,9 @@
then have "homotopic_with (\<lambda>f. True) U T (f1 \<circ> (g1 \<circ> g2)) (id \<circ> g2)"
then have "homotopic_with (\<lambda>x. True) U U
-         (f2 \<circ> (f1 \<circ> (g1 \<circ> g2))) (f2 o (id o g2))"
+         (f2 \<circ> (f1 \<circ> (g1 \<circ> g2))) (f2 \<circ> (id \<circ> g2))"
-  moreover have "homotopic_with (\<lambda>x. True) U U (f2 o id o g2) id"
+  moreover have "homotopic_with (\<lambda>x. True) U U (f2 \<circ> id \<circ> g2) id"
using hom2 by simp
ultimately have UU: "homotopic_with (\<lambda>x. True) U U (f2 \<circ> f1 \<circ> (g1 \<circ> g2)) id"
@@ -6814,8 +6780,8 @@
proof -
obtain h k where h: "continuous_on S h" "h ` S \<subseteq> T"
and k: "continuous_on T k" "k ` T \<subseteq> S"
-               and hom: "homotopic_with (\<lambda>x. True) S S (k o h) id"
-                        "homotopic_with (\<lambda>x. True) T T (h o k) id"
+               and hom: "homotopic_with (\<lambda>x. True) S S (k \<circ> h) id"
+                        "homotopic_with (\<lambda>x. True) T T (h \<circ> k) id"
using assms by (auto simp: homotopy_eqv_def)
have "homotopic_with (\<lambda>f. True) U S (k \<circ> f) (k \<circ> g)"
apply (rule homUS)
@@ -6823,15 +6789,15 @@
apply (safe intro!: continuous_on_compose h k f elim!: continuous_on_subset)
apply (force simp: o_def)+
done
-  then have "homotopic_with (\<lambda>x. True) U T (h o (k o f)) (h o (k o g))"
+  then have "homotopic_with (\<lambda>x. True) U T (h \<circ> (k \<circ> f)) (h \<circ> (k \<circ> g))"
apply (rule homotopic_with_compose_continuous_left)
done
-  moreover have "homotopic_with (\<lambda>x. True) U T (h o k o f) (id o f)"
+  moreover have "homotopic_with (\<lambda>x. True) U T (h \<circ> k \<circ> f) (id \<circ> f)"
apply (rule homotopic_with_compose_continuous_right [where X=T and Y=T])
apply (auto simp: hom f)
done
-  moreover have "homotopic_with (\<lambda>x. True) U T (h o k o g) (id o g)"
+  moreover have "homotopic_with (\<lambda>x. True) U T (h \<circ> k \<circ> g) (id \<circ> g)"
apply (rule homotopic_with_compose_continuous_right [where X=T and Y=T])
apply (auto simp: hom g)
done
@@ -6867,15 +6833,15 @@
proof -
obtain h k where h: "continuous_on S h" "h ` S \<subseteq> T"
and k: "continuous_on T k" "k ` T \<subseteq> S"
-               and hom: "homotopic_with (\<lambda>x. True) S S (k o h) id"
-                        "homotopic_with (\<lambda>x. True) T T (h o k) id"
+               and hom: "homotopic_with (\<lambda>x. True) S S (k \<circ> h) id"
+                        "homotopic_with (\<lambda>x. True) T T (h \<circ> k) id"
using assms by (auto simp: homotopy_eqv_def)
obtain c where "homotopic_with (\<lambda>x. True) S U (f \<circ> h) (\<lambda>x. c)"
apply (rule exE [OF homSU [of "f \<circ> h"]])
apply (intro continuous_on_compose h)
using h f  apply (force elim!: continuous_on_subset)+
done
-  then have "homotopic_with (\<lambda>x. True) T U ((f o h) o k) ((\<lambda>x. c) o k)"
+  then have "homotopic_with (\<lambda>x. True) T U ((f \<circ> h) \<circ> k) ((\<lambda>x. c) \<circ> k)"
apply (rule homotopic_with_compose_continuous_right [where X=S])
using k by auto
moreover have "homotopic_with (\<lambda>x. True) T U (f \<circ> id) (f \<circ> (h \<circ> k))"
@@ -7477,18 +7443,18 @@
using eq by (simp add: algebra_simps)
then have "norm x = norm (y + ((norm x - norm y) / r) *\<^sub>R u)"
by (metis diff_divide_distrib)
-    also have "... \<le> norm y + norm(((norm x - norm y) / r) *\<^sub>R u)"
+    also have "\<dots> \<le> norm y + norm(((norm x - norm y) / r) *\<^sub>R u)"
using norm_triangle_ineq by blast
-    also have "... = norm y + (norm x - norm y) * (norm u / r)"
+    also have "\<dots> = norm y + (norm x - norm y) * (norm u / r)"
using yx \<open>r > 0\<close>
-    also have "... < norm y + (norm x - norm y) * 1"
+    also have "\<dots> < norm y + (norm x - norm y) * 1"
apply (rule mult_strict_left_mono)
using nou \<open>0 < r\<close> yx
done
-    also have "... = norm x"
+    also have "\<dots> = norm x"
by simp
finally show False by simp
qed
@@ -7530,9 +7496,9 @@
proof -
have "norm (y + (1 - norm y / r) *\<^sub>R u) \<le> norm y + norm((1 - norm y / r) *\<^sub>R u)"
using norm_triangle_ineq by blast
-      also have "... = norm y + abs(1 - norm y / r) * norm u"
+      also have "\<dots> = norm y + abs(1 - norm y / r) * norm u"
by simp
-      also have "... \<le> r"
+      also have "\<dots> \<le> r"
proof -
have "(r - norm u) * (r - norm y) \<ge> 0"
using that by auto
@@ -7868,9 +7834,9 @@
then have ope: "openin (subtopology euclidean (affine hull S)) S"
using \<open>open S\<close> open_openin by auto
have "2 \<le> DIM('a)" by (rule 2)
-  also have "... = aff_dim (UNIV :: 'a set)"
+  also have "\<dots> = aff_dim (UNIV :: 'a set)"
by simp
-  also have "... \<le> aff_dim S"
+  also have "\<dots> \<le> aff_dim S"
by (metis aff_dim_UNIV aff_dim_affine_hull aff_dim_le_DIM affS)
finally have "2 \<le> aff_dim S"
by linarith
@@ -8167,16 +8133,11 @@
proof
show "homeomorphism T T (j \<circ> f \<circ> h) (j \<circ> g \<circ> h)"
proof
-      show "continuous_on T (j \<circ> f \<circ> h)"
-        apply (intro continuous_on_compose cont_hj)
-        using hom homeomorphism_def by blast
-      show "continuous_on T (j \<circ> g \<circ> h)"
-        apply (intro continuous_on_compose cont_hj)
-        using hom homeomorphism_def by blast
-      show "(j \<circ> f \<circ> h) ` T \<subseteq> T"
-        by clarsimp (metis (mono_tags, hide_lams) hj(1) hom homeomorphism_def imageE imageI)
-      show "(j \<circ> g \<circ> h) ` T \<subseteq> T"
-        by clarsimp (metis (mono_tags, hide_lams) hj(1) hom homeomorphism_def imageE imageI)
+      show "continuous_on T (j \<circ> f \<circ> h)" "continuous_on T (j \<circ> g \<circ> h)"
+        using hom homeomorphism_def
+        by (blast intro: continuous_on_compose cont_hj)+
+      show "(j \<circ> f \<circ> h) ` T \<subseteq> T" "(j \<circ> g \<circ> h) ` T \<subseteq> T"
+        by auto (metis (mono_tags, hide_lams) hj(1) hom homeomorphism_def imageE imageI)+
show "\<And>x. x \<in> T \<Longrightarrow> (j \<circ> g \<circ> h) ((j \<circ> f \<circ> h) x) = x"
using hj hom homeomorphism_apply1 by fastforce
show "\<And>y. y \<in> T \<Longrightarrow> (j \<circ> f \<circ> h) ((j \<circ> g \<circ> h) y) = y"
@@ -8188,12 +8149,10 @@
apply (drule_tac c="h x" in subsetD, force)
by (metis imageE)
have "bounded (j ` {x. (~ (f x = x \<and> g x = x))})"
-      apply (rule bounded_linear_image [OF bou])
-      using \<open>linear j\<close> linear_conv_bounded_linear by auto
+      by (rule bounded_linear_image [OF bou]) (use \<open>linear j\<close> linear_conv_bounded_linear in auto)
moreover
have *: "{x. ~((j \<circ> f \<circ> h) x = x \<and> (j \<circ> g \<circ> h) x = x)} = j ` {x. (~ (f x = x \<and> g x = x))}"
-      using hj apply (auto simp: jf jg image_iff, metis+)
-      done
+      using hj by (auto simp: jf jg image_iff, metis+)
ultimately show "bounded {x. \<not> ((j \<circ> f \<circ> h) x = x \<and> (j \<circ> g \<circ> h) x = x)}"
by metis
show "\<And>x. x \<in> K \<Longrightarrow> (j \<circ> f \<circ> h) x \<in> U"
@@ -8329,10 +8288,10 @@
apply (rule imageE [OF subsetD [OF sub]], force)
by (metis h hull_inc)
next
-      have "bounded (j ` {x. (~ (f x = x \<and> g x = x))})"
-        apply (rule bounded_closure_image)
-        apply (rule compact_imp_bounded)
+      have "compact (j ` closure {x. \<not> (f x = x \<and> g x = x)})"
using bou by (auto simp: compact_continuous_image cont_hj)
+      then have "bounded (j ` {x. (~ (f x = x \<and> g x = x))})"
+        by (rule bounded_closure_image [OF compact_imp_bounded])
moreover
have *: "{x \<in> affine hull S. j (f (h x)) \<noteq> x \<or> j (g (h x)) \<noteq> x} = j ` {x. (~ (f x = x \<and> g x = x))}"
using h j by (auto simp: image_iff; metis)
@@ -8487,7 +8446,7 @@
have "norm (h (norm (x - a) / r, a + (r / norm (x - a)) *\<^sub>R (x - a)) - h (0, a + r *\<^sub>R b1)) =
norm (h (norm (x - a) / r, a + (r / norm (x - a)) *\<^sub>R (x - a)) - h (0, a + (r / norm (x - a)) *\<^sub>R (x - a)))"
-            also have "... < e"
+            also have "\<dots> < e"
apply (rule d [unfolded dist_norm])
using greater \<open>0 < d\<close> \<open>b1 \<in> Basis\<close> that
by (auto simp: dist_norm divide_simps)```
```--- a/src/HOL/Library/Extended_Real.thy	Sun May 06 23:30:34 2018 +0200
+++ b/src/HOL/Library/Extended_Real.thy	Sun May 06 23:59:14 2018 +0100
@@ -627,6 +627,28 @@
"real_of_ereal y < x \<longleftrightarrow> (\<bar>y\<bar> \<noteq> \<infinity> \<longrightarrow> y < ereal x) \<and> (\<bar>y\<bar> = \<infinity> \<longrightarrow> 0 < x)"
by (cases y) auto

+(*To help with inferences like  a < ereal x \<Longrightarrow> x < y \<Longrightarrow> a < ereal y,
+  where x and y are real.
+*)
+
+lemma le_ereal_le: "a \<le> ereal x \<Longrightarrow> x \<le> y \<Longrightarrow> a \<le> ereal y"
+  using ereal_less_eq(3) order.trans by blast
+
+lemma le_ereal_less: "a \<le> ereal x \<Longrightarrow> x < y \<Longrightarrow> a < ereal y"
+
+lemma less_ereal_le: "a < ereal x \<Longrightarrow> x \<le> y \<Longrightarrow> a < ereal y"
+  using ereal_less_ereal_Ex by auto
+
+lemma ereal_le_le: "ereal y \<le> a \<Longrightarrow> x \<le> y \<Longrightarrow> ereal x \<le> a"