# HG changeset patch
# User paulson <lp15@cam.ac.uk>
# Date 1525647541 -3600
# Node ID e58c9ac761cb0b29ddea25eb5272ddbfde5df254
# Parent  4fa3e63ecc7e22776b5f4450f7d23e3e9fe3cb3b
more tidying

diff -r 4fa3e63ecc7e -r e58c9ac761cb src/HOL/Analysis/Interval_Integral.thy
--- a/src/HOL/Analysis/Interval_Integral.thy	Sun May 06 11:33:40 2018 +0100
+++ b/src/HOL/Analysis/Interval_Integral.thy	Sun May 06 23:59:01 2018 +0100
@@ -22,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"
   by (simp add: einterval_def)
@@ -51,14 +51,9 @@
   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)
-      apply (simp add: Lim_PInfty)
-      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
+    by (simp add: LIMSEQ_Suc_iff Lim_PInfty) (metis add.commute diff_le_eq nat_ceiling_le_eq)
   ultimately show thesis
     by (intro that[of "\<lambda>i. real_of_ereal a + Suc i"])
        (auto simp: incseq_def PInf)
@@ -80,7 +75,7 @@
     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:
@@ -93,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
@@ -188,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]:
@@ -198,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]:
@@ -239,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)
@@ -280,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) 
@@ -312,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
 
@@ -320,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"
@@ -353,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 (simp add: interval_lebesgue_integrable_def)
   apply (intro conjI impI set_integrable_cong_AE)
   apply (auto simp: min_def max_def)
   done
@@ -394,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
@@ -531,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"
@@ -595,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
@@ -609,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
@@ -645,7 +640,7 @@
     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)
@@ -695,16 +690,19 @@
     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
@@ -728,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})"
@@ -743,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
 
@@ -754,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)
@@ -762,10 +760,10 @@
     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)
+      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"
@@ -779,7 +777,7 @@
         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 add: has_vector_derivative_within_open [of _ "{d<..<e}"])
+      by (force simp: has_vector_derivative_within_open [of _ "{d<..<e}"])
   qed
 qed
 
@@ -800,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
 
@@ -882,15 +872,15 @@
   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)
+      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"
@@ -905,7 +895,7 @@
     show "einterval A B = (\<Union>i. {g(l i)<..<g(u i)})"
     proof
       show "einterval A B \<subseteq> (\<Union>i. {g(l i)<..<g(u i)})"
-        by (auto simp add: einterval_def AB)
+        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"
@@ -927,16 +917,14 @@
   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))"
     by (simp add: eq1)
   have incseq: "incseq (\<lambda>i. {g (l i)<..<g (u i)})"
-    apply (auto simp add: incseq_def)
+    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. (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)
+  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
 
@@ -961,7 +949,7 @@
 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 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)
@@ -981,15 +969,15 @@
   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)
+      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"
@@ -997,15 +985,14 @@
     { 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)"
         by (simp add: eventually_sequentially, auto)
     } note AB = this
     show "einterval A B = (\<Union>i. {g(l i)<..<g(u i)})"
     proof
       show "einterval A B \<subseteq> (\<Union>i. {g (l i)<..<g (u i)})"
-        by (auto simp add: einterval_def AB)
+        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
@@ -1023,12 +1010,6 @@
     then show ?thesis
       by (simp add: ac_simps)
   qed
-  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)"
-    by (simp add: eq1)
   have incseq: "incseq (\<lambda>i. {g (l i)<..<g (u i)})"
     apply (clarsimp simp add: incseq_def, intro conjI)
     apply (meson llb antimono_def approx(3) approx(5) g_nondec le_less_trans)
@@ -1040,21 +1021,25 @@
     with that show ?thesis
       using IVT' [of g] approx(4) dual_order.strict_implies_order by blast
   qed
-  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)
+  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"
+      by (simp add: eq1)
+    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"
     by (simp add: un)
 
@@ -1099,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>
@@ -1111,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)
@@ -1122,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
diff -r 4fa3e63ecc7e -r e58c9ac761cb src/HOL/Analysis/Path_Connected.thy
--- a/src/HOL/Analysis/Path_Connected.thy	Sun May 06 11:33:40 2018 +0100
+++ b/src/HOL/Analysis/Path_Connected.thy	Sun May 06 23:59:01 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"
   by (simp add: pathstart_def)
 
-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)"
   by (simp add: pathstart_def)
 
-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"
   by (simp add: pathfinish_def)
 
-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)"
   by (simp add: pathfinish_def)
 
-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)"
   by (simp add: image_comp path_image_def)
 
-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)"
   by (simp add: image_comp path_image_def)
 
-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"
   by (simp add: simple_path_def path_translation_eq)
 
 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)"
   by (simp add: pathstart_def)
 
-lemma pathfinish_compose: "pathfinish(f o p) = f(pathfinish p)"
+lemma pathfinish_compose: "pathfinish(f \<circ> p) = f(pathfinish p)"
   by (simp add: pathfinish_def)
 
-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)"
   by (simp add: image_comp path_image_def)
 
-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 simp:  "**" add.commute add_diff_eq)
+  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)
+  by (simp add: arc_imp_simple_path)
 
 lemma linepath_trivial [simp]: "linepath a a x = a"
   by (simp add: linepath_def real_vector.scale_left_diff_distrib)
@@ -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
     by (simp add: midpoint_def algebra_simps)
 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 (simp add: path_component_def)
-  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 @@
   by (simp add: convex_imp_path_connected)
 
 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
-proof (clarsimp simp add: path_image_def)
-  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))"
       by (simp add: path_def)
-    then show ?thesis
-      apply (simp add: path_component_def)
-      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"
         by (simp add: algebra_simps)
-      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"
         by (simp add: algebra_simps)
-      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))"
         using CC by (simp add: field_simps) (simp add: add_divide_distrib scaleR_add_left)
       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"
         by (simp add: algebra_simps)
-      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"
         by (simp add: algebra_simps)
-      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))"
         using DD by (simp add: field_simps) (simp add: add_divide_distrib scaleR_add_left)
       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)"
       by (simp add: dist_norm)
-    also have "... = norm ((2*r) *\<^sub>R b)"
+    also have "\<dots> = norm ((2*r) *\<^sub>R b)"
       by (metis mult_2 scaleR_add_left)
-    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"
   by (simp add: inside_outside)
 
-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 (simp add: connected_component_def)
-        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)
-        apply (simp add: real_vector_class.scaleR_add_left [symmetric] divide_simps)
+      case False 
+      with B C
+      have "closed_segment x (((B + C) / norm x) *\<^sub>R x) \<subseteq> - ball 0 B"
+        apply (clarsimp simp add: closed_segment_def ball_def dist_norm real_vector_class.scaleR_add_left [symmetric] divide_simps)
         using segment_bound_lemma [of B "norm x" "B+C" ] Bno
         by (meson le_add_same_cancel1 less_eq_real_def not_le)
+      also have "... \<subseteq> -S"
+        by (simp add: B)
+      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 (simp add: outside_def assms)
     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 (simp add: outside)
-  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}"
 apply (simp add: outside_connected_component_lt)
 apply (simp add: Set.set_eq_iff)
 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"
       by (simp add: connected_component_maximal that)
-    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"
   apply (simp add: inside_outside outside_frontier_eq_complement_closure)
   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 (simp add:)
+      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 (simp add:)
+      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 (clarsimp simp add: homotopic_with_def)
   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 (clarsimp simp add: homotopic_with_def)
   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 (clarsimp simp add: homotopic_with_def)
   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 (simp add: homotopic_with_def)
-  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 (clarsimp simp add: homotopic_with_def)
   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
       by (simp add: geq that)
     have "continuous_on ({0..1} \<times> X) k"
       using cont
       apply (simp add: split_01_prod k_def)
       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"
       by (simp add: k_def k12)
     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 (clarsimp simp add: k_def)
-      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 (simp add: homotopic_paths_def homotopic_with_def)
-      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 (simp add: joinpaths_def)
     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 (simp add:)
+    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 add:)
+    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 (simp add: simply_connected_eq_contractible_loop_any)
-      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 (simp add: simply_connected_eq_contractible_loop_any)
-      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 (simp add: simply_connected_eq_contractible_loop_all False)
     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 (simp add: )
+    apply (erule a [unfolded closed_segment_def, THEN subsetD], simp)
     apply (metis add_diff_cancel_right' diff_ge_0_iff_ge le_add_diff_inverse pth_c(1))
     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 (simp add: homotopic_with_def)
     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 (simp add: contractible_def homotopic_with)
     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]
     by (simp add: f rev_image_eqI)
-  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
       by (simp add: norm_eq_sqrt_inner)
@@ -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)"
       by (simp add: f.sum f.scale)
-    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"
       by (simp add: norm_eq_sqrt_inner)
     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))"
       by (simp add: g.sum g.scale)
-    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))"
       by (simp add: g.scale)
-    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))"
       by (simp add: x g.sum)
-    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)"
       by (simp add: g.scale)
-    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))"
       by (simp add: f.scale f.sum)
-    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))"
       by (simp add: f.scale f.sum)
-    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)"
     by (simp add: homeomorphic_translation)
-  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)"
     by (simp add: o_assoc)
   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))"
     by (simp add: g1 homotopic_with_compose_continuous_left)
-  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"
     apply (simp add: o_assoc)
@@ -6770,9 +6736,9 @@
   then have "homotopic_with (\<lambda>f. True) U T (f1 \<circ> (g1 \<circ> g2)) (id \<circ> g2)"
     by (simp add: o_assoc)
   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))"
     by (simp add: f2 homotopic_with_compose_continuous_left)
-  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"
     apply (simp add: o_assoc)
@@ -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)
     apply (simp_all add: h)
     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>
       by (simp add: divide_simps)
-    also have "... < norm y + (norm x - norm y) * 1"
+    also have "\<dots> < norm y + (norm x - norm y) * 1"
       apply (subst add_less_cancel_left)
       apply (rule mult_strict_left_mono)
       using nou \<open>0 < r\<close> yx
        apply (simp_all add: field_simps)
       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)))"
               by (simp add: h)
-            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)