merged
authorpaulson
Sun May 06 23:59:14 2018 +0100 (14 months ago)
changeset 680975f3cffe16311
parent 68094 0b66aca9c965
parent 68096 e58c9ac761cb
child 68098 e2bb1d95cbd0
child 68101 0699a0bacc50
child 68109 cebf36c14226
child 68120 2f161c6910f7
merged
     1.1 --- a/src/HOL/Analysis/Derivative.thy	Sun May 06 23:30:34 2018 +0200
     1.2 +++ b/src/HOL/Analysis/Derivative.thy	Sun May 06 23:59:14 2018 +0100
     1.3 @@ -72,8 +72,8 @@
     1.4    by blast
     1.5  
     1.6  lemma has_derivative_within_open:
     1.7 -  "a \<in> s \<Longrightarrow> open s \<Longrightarrow>
     1.8 -    (f has_derivative f') (at a within s) \<longleftrightarrow> (f has_derivative f') (at a)"
     1.9 +  "a \<in> S \<Longrightarrow> open S \<Longrightarrow>
    1.10 +    (f has_derivative f') (at a within S) \<longleftrightarrow> (f has_derivative f') (at a)"
    1.11    by (simp only: at_within_interior interior_open)
    1.12  
    1.13  lemma has_derivative_right:
    1.14 @@ -98,8 +98,8 @@
    1.15  lemmas DERIV_within_iff = has_field_derivative_iff
    1.16  
    1.17  lemma DERIV_caratheodory_within:
    1.18 -  "(f has_field_derivative l) (at x within s) \<longleftrightarrow>
    1.19 -   (\<exists>g. (\<forall>z. f z - f x = g z * (z - x)) \<and> continuous (at x within s) g \<and> g x = l)"
    1.20 +  "(f has_field_derivative l) (at x within S) \<longleftrightarrow>
    1.21 +   (\<exists>g. (\<forall>z. f z - f x = g z * (z - x)) \<and> continuous (at x within S) g \<and> g x = l)"
    1.22        (is "?lhs = ?rhs")
    1.23  proof
    1.24    assume ?lhs
    1.25 @@ -107,14 +107,14 @@
    1.26    proof (intro exI conjI)
    1.27      let ?g = "(%z. if z = x then l else (f z - f x) / (z-x))"
    1.28      show "\<forall>z. f z - f x = ?g z * (z-x)" by simp
    1.29 -    show "continuous (at x within s) ?g" using \<open>?lhs\<close>
    1.30 +    show "continuous (at x within S) ?g" using \<open>?lhs\<close>
    1.31        by (auto simp add: continuous_within DERIV_within_iff cong: Lim_cong_within)
    1.32      show "?g x = l" by simp
    1.33    qed
    1.34  next
    1.35    assume ?rhs
    1.36    then obtain g where
    1.37 -    "(\<forall>z. f z - f x = g z * (z-x))" and "continuous (at x within s) g" and "g x = l" by blast
    1.38 +    "(\<forall>z. f z - f x = g z * (z-x))" and "continuous (at x within S) g" and "g x = l" by blast
    1.39    thus ?lhs
    1.40      by (auto simp add: continuous_within DERIV_within_iff cong: Lim_cong_within)
    1.41  qed
    1.42 @@ -330,18 +330,23 @@
    1.43    using has_derivative_compose[of f f' x UNIV g g']
    1.44    by (simp add: comp_def)
    1.45  
    1.46 +lemma has_vector_derivative_within_open:
    1.47 +  "a \<in> S \<Longrightarrow> open S \<Longrightarrow>
    1.48 +    (f has_vector_derivative f') (at a within S) \<longleftrightarrow> (f has_vector_derivative f') (at a)"
    1.49 +  by (simp only: at_within_interior interior_open)
    1.50 +
    1.51  lemma field_vector_diff_chain_within:
    1.52 - assumes Df: "(f has_vector_derivative f') (at x within s)"
    1.53 -     and Dg: "(g has_field_derivative g') (at (f x) within f`s)"
    1.54 - shows "((g \<circ> f) has_vector_derivative (f' * g')) (at x within s)"
    1.55 + assumes Df: "(f has_vector_derivative f') (at x within S)"
    1.56 +     and Dg: "(g has_field_derivative g') (at (f x) within f ` S)"
    1.57 + shows "((g \<circ> f) has_vector_derivative (f' * g')) (at x within S)"
    1.58  using diff_chain_within[OF Df[unfolded has_vector_derivative_def]
    1.59                         Dg [unfolded has_field_derivative_def]]
    1.60   by (auto simp: o_def mult.commute has_vector_derivative_def)
    1.61  
    1.62  lemma vector_derivative_diff_chain_within:
    1.63 -  assumes Df: "(f has_vector_derivative f') (at x within s)"
    1.64 -     and Dg: "(g has_derivative g') (at (f x) within f`s)"
    1.65 -  shows "((g \<circ> f) has_vector_derivative (g' f')) (at x within s)"
    1.66 +  assumes Df: "(f has_vector_derivative f') (at x within S)"
    1.67 +     and Dg: "(g has_derivative g') (at (f x) within f`S)"
    1.68 +  shows "((g \<circ> f) has_vector_derivative (g' f')) (at x within S)"
    1.69  using diff_chain_within[OF Df[unfolded has_vector_derivative_def] Dg]
    1.70    linear.scaleR[OF has_derivative_linear[OF Dg]]
    1.71    unfolding has_vector_derivative_def o_def
    1.72 @@ -357,8 +362,8 @@
    1.73    by (meson diff_chain_at)
    1.74  
    1.75  lemma differentiable_chain_within:
    1.76 -  "f differentiable (at x within s) \<Longrightarrow>
    1.77 -    g differentiable (at(f x) within (f ` s)) \<Longrightarrow> (g \<circ> f) differentiable (at x within s)"
    1.78 +  "f differentiable (at x within S) \<Longrightarrow>
    1.79 +    g differentiable (at(f x) within (f ` S)) \<Longrightarrow> (g \<circ> f) differentiable (at x within S)"
    1.80    unfolding differentiable_def
    1.81    by (meson diff_chain_within)
    1.82  
     2.1 --- a/src/HOL/Analysis/Interval_Integral.thy	Sun May 06 23:30:34 2018 +0200
     2.2 +++ b/src/HOL/Analysis/Interval_Integral.thy	Sun May 06 23:59:14 2018 +0100
     2.3 @@ -12,20 +12,6 @@
     2.4    "(\<And>x. x \<in> S \<Longrightarrow> (f has_vector_derivative f' x) (at x within S)) \<Longrightarrow> continuous_on S f"
     2.5    by (auto simp: continuous_on_eq_continuous_within intro!: has_vector_derivative_continuous)
     2.6  
     2.7 -lemma has_vector_derivative_weaken:
     2.8 -  fixes x D and f g s t
     2.9 -  assumes f: "(f has_vector_derivative D) (at x within t)"
    2.10 -    and "x \<in> s" "s \<subseteq> t"
    2.11 -    and "\<And>x. x \<in> s \<Longrightarrow> f x = g x"
    2.12 -  shows "(g has_vector_derivative D) (at x within s)"
    2.13 -proof -
    2.14 -  have "(f has_vector_derivative D) (at x within s) \<longleftrightarrow> (g has_vector_derivative D) (at x within s)"
    2.15 -    unfolding has_vector_derivative_def has_derivative_iff_norm
    2.16 -    using assms by (intro conj_cong Lim_cong_within refl) auto
    2.17 -  then show ?thesis
    2.18 -    using has_vector_derivative_within_subset[OF f \<open>s \<subseteq> t\<close>] by simp
    2.19 -qed
    2.20 -
    2.21  definition "einterval a b = {x. a < ereal x \<and> ereal x < b}"
    2.22  
    2.23  lemma einterval_eq[simp]:
    2.24 @@ -36,7 +22,7 @@
    2.25    by (auto simp: einterval_def)
    2.26  
    2.27  lemma einterval_same: "einterval a a = {}"
    2.28 -  by (auto simp add: einterval_def)
    2.29 +  by (auto simp: einterval_def)
    2.30  
    2.31  lemma einterval_iff: "x \<in> einterval a b \<longleftrightarrow> a < ereal x \<and> ereal x < b"
    2.32    by (simp add: einterval_def)
    2.33 @@ -59,21 +45,15 @@
    2.34  lemma ereal_incseq_approx:
    2.35    fixes a b :: ereal
    2.36    assumes "a < b"
    2.37 -  obtains X :: "nat \<Rightarrow> real" where
    2.38 -    "incseq X" "\<And>i. a < X i" "\<And>i. X i < b" "X \<longlonglongrightarrow> b"
    2.39 +  obtains X :: "nat \<Rightarrow> real" where "incseq X" "\<And>i. a < X i" "\<And>i. X i < b" "X \<longlonglongrightarrow> b"
    2.40  proof (cases b)
    2.41    case PInf
    2.42    with \<open>a < b\<close> have "a = -\<infinity> \<or> (\<exists>r. a = ereal r)"
    2.43      by (cases a) auto
    2.44    moreover have "(\<lambda>x. ereal (real (Suc x))) \<longlonglongrightarrow> \<infinity>"
    2.45 -      apply (subst LIMSEQ_Suc_iff)
    2.46 -      apply (simp add: Lim_PInfty)
    2.47 -      using nat_ceiling_le_eq by blast
    2.48 +    by (simp add: Lim_PInfty LIMSEQ_Suc_iff) (metis le_SucI of_nat_Suc of_nat_mono order_trans real_arch_simple)
    2.49    moreover have "\<And>r. (\<lambda>x. ereal (r + real (Suc x))) \<longlonglongrightarrow> \<infinity>"
    2.50 -    apply (subst LIMSEQ_Suc_iff)
    2.51 -    apply (subst Lim_PInfty)
    2.52 -    apply (metis add.commute diff_le_eq nat_ceiling_le_eq ereal_less_eq(3))
    2.53 -    done
    2.54 +    by (simp add: LIMSEQ_Suc_iff Lim_PInfty) (metis add.commute diff_le_eq nat_ceiling_le_eq)
    2.55    ultimately show thesis
    2.56      by (intro that[of "\<lambda>i. real_of_ereal a + Suc i"])
    2.57         (auto simp: incseq_def PInf)
    2.58 @@ -87,16 +67,15 @@
    2.59      by (intro mult_strict_left_mono) auto
    2.60    with \<open>a < b\<close> a' have "\<And>i. a < ereal (b' - d / real (Suc (Suc i)))"
    2.61      by (cases a) (auto simp: real d_def field_simps)
    2.62 -  moreover have "(\<lambda>i. b' - d / Suc (Suc i)) \<longlonglongrightarrow> b'"
    2.63 -    apply (subst filterlim_sequentially_Suc)
    2.64 -    apply (subst filterlim_sequentially_Suc)
    2.65 -    apply (rule tendsto_eq_intros)
    2.66 -    apply (auto intro!: tendsto_divide_0[OF tendsto_const] filterlim_sup1
    2.67 -                simp: at_infinity_eq_at_top_bot filterlim_real_sequentially)
    2.68 -    done
    2.69 +  moreover
    2.70 +  have "(\<lambda>i. b' - d / real i) \<longlonglongrightarrow> b'"
    2.71 +    by (force intro: tendsto_eq_intros tendsto_divide_0[OF tendsto_const] filterlim_sup1
    2.72 +              simp: at_infinity_eq_at_top_bot filterlim_real_sequentially)
    2.73 +  then have "(\<lambda>i. b' - d / Suc (Suc i)) \<longlonglongrightarrow> b'"
    2.74 +    by (blast intro: dest: filterlim_sequentially_Suc [THEN iffD2])
    2.75    ultimately show thesis
    2.76      by (intro that[of "\<lambda>i. b' - d / Suc (Suc i)"])
    2.77 -       (auto simp add: real incseq_def intro!: divide_left_mono)
    2.78 +       (auto simp: real incseq_def intro!: divide_left_mono)
    2.79  qed (insert \<open>a < b\<close>, auto)
    2.80  
    2.81  lemma ereal_decseq_approx:
    2.82 @@ -109,7 +88,7 @@
    2.83    from ereal_incseq_approx[OF this] guess X .
    2.84    then show thesis
    2.85      apply (intro that[of "\<lambda>i. - X i"])
    2.86 -    apply (auto simp add: decseq_def incseq_def reorient: uminus_ereal.simps)
    2.87 +    apply (auto simp: decseq_def incseq_def reorient: uminus_ereal.simps)
    2.88      apply (metis ereal_minus_less_minus ereal_uminus_uminus ereal_Lim_uminus)+
    2.89      done
    2.90  qed
    2.91 @@ -204,7 +183,7 @@
    2.92    shows "interval_lebesgue_integrable M a b (\<lambda>x. f x + g x)" and
    2.93      "interval_lebesgue_integral M a b (\<lambda>x. f x + g x) =
    2.94     interval_lebesgue_integral M a b f + interval_lebesgue_integral M a b g"
    2.95 -using assms by (auto simp add: interval_lebesgue_integral_def interval_lebesgue_integrable_def
    2.96 +using assms by (auto simp: interval_lebesgue_integral_def interval_lebesgue_integrable_def
    2.97      field_simps)
    2.98  
    2.99  lemma interval_lebesgue_integral_diff [intro, simp]:
   2.100 @@ -214,7 +193,7 @@
   2.101    shows "interval_lebesgue_integrable M a b (\<lambda>x. f x - g x)" and
   2.102      "interval_lebesgue_integral M a b (\<lambda>x. f x - g x) =
   2.103     interval_lebesgue_integral M a b f - interval_lebesgue_integral M a b g"
   2.104 -using assms by (auto simp add: interval_lebesgue_integral_def interval_lebesgue_integrable_def
   2.105 +using assms by (auto simp: interval_lebesgue_integral_def interval_lebesgue_integrable_def
   2.106      field_simps)
   2.107  
   2.108  lemma interval_lebesgue_integrable_mult_right [intro, simp]:
   2.109 @@ -255,31 +234,31 @@
   2.110  
   2.111  lemma interval_lebesgue_integral_uminus:
   2.112    "interval_lebesgue_integral M a b (\<lambda>x. - f x) = - interval_lebesgue_integral M a b f"
   2.113 -  by (auto simp add: interval_lebesgue_integral_def interval_lebesgue_integrable_def set_lebesgue_integral_def)
   2.114 +  by (auto simp: interval_lebesgue_integral_def interval_lebesgue_integrable_def set_lebesgue_integral_def)
   2.115  
   2.116  lemma interval_lebesgue_integral_of_real:
   2.117    "interval_lebesgue_integral M a b (\<lambda>x. complex_of_real (f x)) =
   2.118      of_real (interval_lebesgue_integral M a b f)"
   2.119    unfolding interval_lebesgue_integral_def
   2.120 -  by (auto simp add: interval_lebesgue_integral_def set_integral_complex_of_real)
   2.121 +  by (auto simp: interval_lebesgue_integral_def set_integral_complex_of_real)
   2.122  
   2.123  lemma interval_lebesgue_integral_le_eq:
   2.124    fixes a b f
   2.125    assumes "a \<le> b"
   2.126    shows "interval_lebesgue_integral M a b f = (LINT x : einterval a b | M. f x)"
   2.127 -using assms by (auto simp add: interval_lebesgue_integral_def)
   2.128 +using assms by (auto simp: interval_lebesgue_integral_def)
   2.129  
   2.130  lemma interval_lebesgue_integral_gt_eq:
   2.131    fixes a b f
   2.132    assumes "a > b"
   2.133    shows "interval_lebesgue_integral M a b f = -(LINT x : einterval b a | M. f x)"
   2.134 -using assms by (auto simp add: interval_lebesgue_integral_def less_imp_le einterval_def)
   2.135 +using assms by (auto simp: interval_lebesgue_integral_def less_imp_le einterval_def)
   2.136  
   2.137  lemma interval_lebesgue_integral_gt_eq':
   2.138    fixes a b f
   2.139    assumes "a > b"
   2.140    shows "interval_lebesgue_integral M a b f = - interval_lebesgue_integral M b a f"
   2.141 -using assms by (auto simp add: interval_lebesgue_integral_def less_imp_le einterval_def)
   2.142 +using assms by (auto simp: interval_lebesgue_integral_def less_imp_le einterval_def)
   2.143  
   2.144  lemma interval_integral_endpoints_same [simp]: "(LBINT x=a..a. f x) = 0"
   2.145    by (simp add: interval_lebesgue_integral_def set_lebesgue_integral_def einterval_same)
   2.146 @@ -296,7 +275,7 @@
   2.147    "(LBINT x=a..b. f x) = (LBINT x=-b..-a. f (-x))"
   2.148  proof (induct a b rule: linorder_wlog)
   2.149    case (sym a b) then show ?case
   2.150 -    by (auto simp add: interval_lebesgue_integral_def interval_integrable_endpoints_reverse
   2.151 +    by (auto simp: interval_lebesgue_integral_def interval_integrable_endpoints_reverse
   2.152               split: if_split_asm)
   2.153  next
   2.154    case (le a b) 
   2.155 @@ -328,7 +307,7 @@
   2.156  
   2.157  lemma interval_integral_zero [simp]:
   2.158    fixes a b :: ereal
   2.159 -  shows"LBINT x=a..b. 0 = 0"
   2.160 +  shows "LBINT x=a..b. 0 = 0"
   2.161  unfolding interval_lebesgue_integral_def set_lebesgue_integral_def einterval_eq
   2.162  by simp
   2.163  
   2.164 @@ -336,7 +315,7 @@
   2.165    fixes a b c :: real
   2.166    shows "interval_lebesgue_integrable lborel a b (\<lambda>x. c)" and "LBINT x=a..b. c = c * (b - a)"
   2.167    unfolding interval_lebesgue_integral_def interval_lebesgue_integrable_def einterval_eq
   2.168 -  by (auto simp add: less_imp_le field_simps measure_def set_integrable_def set_lebesgue_integral_def)
   2.169 +  by (auto simp: less_imp_le field_simps measure_def set_integrable_def set_lebesgue_integral_def)
   2.170  
   2.171  lemma interval_integral_cong_AE:
   2.172    assumes [measurable]: "f \<in> borel_measurable borel" "g \<in> borel_measurable borel"
   2.173 @@ -369,7 +348,7 @@
   2.174      "f \<in> borel_measurable lborel \<Longrightarrow> g \<in> borel_measurable lborel \<Longrightarrow>
   2.175      AE x \<in> einterval (min a b) (max a b) in lborel. f x = g x \<Longrightarrow>
   2.176      interval_lebesgue_integrable lborel a b f = interval_lebesgue_integrable lborel a b g"
   2.177 -  apply (simp add: interval_lebesgue_integrable_def )
   2.178 +  apply (simp add: interval_lebesgue_integrable_def)
   2.179    apply (intro conjI impI set_integrable_cong_AE)
   2.180    apply (auto simp: min_def max_def)
   2.181    done
   2.182 @@ -410,11 +389,11 @@
   2.183  
   2.184  lemma interval_integral_Ioi:
   2.185    "\<bar>a\<bar> < \<infinity> \<Longrightarrow> (LBINT x=a..\<infinity>. f x) = (LBINT x : {real_of_ereal a <..}. f x)"
   2.186 -  by (auto simp add: interval_lebesgue_integral_def einterval_iff)
   2.187 +  by (auto simp: interval_lebesgue_integral_def einterval_iff)
   2.188  
   2.189  lemma interval_integral_Ioo:
   2.190    "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)"
   2.191 -  by (auto simp add: interval_lebesgue_integral_def einterval_iff)
   2.192 +  by (auto simp: interval_lebesgue_integral_def einterval_iff)
   2.193  
   2.194  lemma interval_integral_discrete_difference:
   2.195    fixes f :: "real \<Rightarrow> 'b::{banach, second_countable_topology}" and a b :: ereal
   2.196 @@ -547,7 +526,7 @@
   2.197      using f_measurable set_borel_measurable_def by blast
   2.198    have "(LBINT x=a..b. f x) = lebesgue_integral lborel (\<lambda>x. indicator (einterval a b) x *\<^sub>R f x)"
   2.199      using assms by (simp add: interval_lebesgue_integral_def set_lebesgue_integral_def less_imp_le)
   2.200 -  also have "... = C"
   2.201 +  also have "\<dots> = C"
   2.202      by (rule integral_monotone_convergence [OF 1 2 3 4 5])
   2.203    finally show "(LBINT x=a..b. f x) = C" .
   2.204    show "set_integrable lborel (einterval a b) f"
   2.205 @@ -601,14 +580,6 @@
   2.206    TODO: make the older versions corollaries of these (using continuous_at_imp_continuous_on, etc.)
   2.207  *)
   2.208  
   2.209 -(*
   2.210 -TODO: many proofs below require inferences like
   2.211 -
   2.212 -  a < ereal x \<Longrightarrow> x < y \<Longrightarrow> a < ereal y
   2.213 -
   2.214 -where x and y are real. These should be better automated.
   2.215 -*)
   2.216 -
   2.217  lemma interval_integral_FTC_finite:
   2.218    fixes f F :: "real \<Rightarrow> 'a::euclidean_space" and a b :: real
   2.219    assumes f: "continuous_on {min a b..max a b} f"
   2.220 @@ -619,7 +590,7 @@
   2.221    case True
   2.222    have "(LBINT x=a..b. f x) = (LBINT x. indicat_real {a..b} x *\<^sub>R f x)"
   2.223      by (simp add: True interval_integral_Icc set_lebesgue_integral_def)
   2.224 -  also have "... = F b - F a"
   2.225 +  also have "\<dots> = F b - F a"
   2.226    proof (rule integral_FTC_atLeastAtMost [OF True])
   2.227      show "continuous_on {a..b} f"
   2.228        using True f by linarith
   2.229 @@ -633,7 +604,7 @@
   2.230      by simp
   2.231    have "- interval_lebesgue_integral lborel (ereal b) (ereal a) f = - (LBINT x. indicat_real {b..a} x *\<^sub>R f x)"
   2.232      by (simp add: \<open>b \<le> a\<close> interval_integral_Icc set_lebesgue_integral_def)
   2.233 -  also have "... = F b - F a"
   2.234 +  also have "\<dots> = F b - F a"
   2.235    proof (subst integral_FTC_atLeastAtMost [OF \<open>b \<le> a\<close>])
   2.236      show "continuous_on {b..a} f"
   2.237        using False f by linarith
   2.238 @@ -646,7 +617,6 @@
   2.239  qed
   2.240  
   2.241  
   2.242 -
   2.243  lemma interval_integral_FTC_nonneg:
   2.244    fixes f F :: "real \<Rightarrow> real" and a b :: ereal
   2.245    assumes "a < b"
   2.246 @@ -659,14 +629,18 @@
   2.247      "set_integrable lborel (einterval a b) f"
   2.248      "(LBINT x=a..b. f x) = B - A"
   2.249  proof -
   2.250 -  from einterval_Icc_approximation[OF \<open>a < b\<close>] guess u l . note approx = this
   2.251 +  obtain u l where approx:
   2.252 +    "einterval a b = (\<Union>i. {l i .. u i})"
   2.253 +    "incseq u" "decseq l" "\<And>i. l i < u i" "\<And>i. a < l i" "\<And>i. u i < b"
   2.254 +    "l \<longlonglongrightarrow> a" "u \<longlonglongrightarrow> b" 
   2.255 +    by (blast intro: einterval_Icc_approximation[OF \<open>a < b\<close>])
   2.256    have [simp]: "\<And>x i. l i \<le> x \<Longrightarrow> a < ereal x"
   2.257      by (rule order_less_le_trans, rule approx, force)
   2.258    have [simp]: "\<And>x i. x \<le> u i \<Longrightarrow> ereal x < b"
   2.259      by (rule order_le_less_trans, subst ereal_less_eq(3), assumption, rule approx)
   2.260    have FTCi: "\<And>i. (LBINT x=l i..u i. f x) = F (u i) - F (l i)"
   2.261      using assms approx apply (intro interval_integral_FTC_finite)
   2.262 -    apply (auto simp add: less_imp_le min_def max_def
   2.263 +    apply (auto simp: less_imp_le min_def max_def
   2.264        has_field_derivative_iff_has_vector_derivative[symmetric])
   2.265      apply (rule continuous_at_imp_continuous_on, auto intro!: f)
   2.266      by (rule DERIV_subset [OF F], auto)
   2.267 @@ -705,23 +679,30 @@
   2.268    assumes B: "((F \<circ> real_of_ereal) \<longlongrightarrow> B) (at_left b)"
   2.269    shows "(LBINT x=a..b. f x) = B - A"
   2.270  proof -
   2.271 -  from einterval_Icc_approximation[OF \<open>a < b\<close>] guess u l . note approx = this
   2.272 +  obtain u l where approx:
   2.273 +    "einterval a b = (\<Union>i. {l i .. u i})"
   2.274 +    "incseq u" "decseq l" "\<And>i. l i < u i" "\<And>i. a < l i" "\<And>i. u i < b"
   2.275 +    "l \<longlonglongrightarrow> a" "u \<longlonglongrightarrow> b" 
   2.276 +    by (blast intro: einterval_Icc_approximation[OF \<open>a < b\<close>])
   2.277    have [simp]: "\<And>x i. l i \<le> x \<Longrightarrow> a < ereal x"
   2.278      by (rule order_less_le_trans, rule approx, force)
   2.279    have [simp]: "\<And>x i. x \<le> u i \<Longrightarrow> ereal x < b"
   2.280      by (rule order_le_less_trans, subst ereal_less_eq(3), assumption, rule approx)
   2.281    have FTCi: "\<And>i. (LBINT x=l i..u i. f x) = F (u i) - F (l i)"
   2.282      using assms approx
   2.283 -    by (auto simp add: less_imp_le min_def max_def
   2.284 +    by (auto simp: less_imp_le min_def max_def
   2.285               intro!: f continuous_at_imp_continuous_on interval_integral_FTC_finite
   2.286               intro: has_vector_derivative_at_within)
   2.287    have "(\<lambda>i. LBINT x=l i..u i. f x) \<longlonglongrightarrow> B - A"
   2.288 -    apply (subst FTCi)
   2.289 -    apply (intro tendsto_intros)
   2.290 -    using B approx unfolding tendsto_at_iff_sequentially comp_def
   2.291 -    apply (elim allE[of _ "\<lambda>i. ereal (u i)"], auto)
   2.292 -    using A approx unfolding tendsto_at_iff_sequentially comp_def
   2.293 -    by (elim allE[of _ "\<lambda>i. ereal (l i)"], auto)
   2.294 +    unfolding FTCi
   2.295 +  proof (intro tendsto_intros)
   2.296 +    show "(\<lambda>x. F (l x)) \<longlonglongrightarrow> A"
   2.297 +      using A approx unfolding tendsto_at_iff_sequentially comp_def
   2.298 +      by (elim allE[of _ "\<lambda>i. ereal (l i)"], auto)
   2.299 +    show "(\<lambda>x. F (u x)) \<longlonglongrightarrow> B"
   2.300 +      using B approx unfolding tendsto_at_iff_sequentially comp_def
   2.301 +      by (elim allE[of _ "\<lambda>i. ereal (u i)"], auto)
   2.302 +  qed
   2.303    moreover have "(\<lambda>i. LBINT x=l i..u i. f x) \<longlonglongrightarrow> (LBINT x=a..b. f x)"
   2.304      by (rule interval_integral_Icc_approx_integrable [OF \<open>a < b\<close> approx f_integrable])
   2.305    ultimately show ?thesis
   2.306 @@ -745,8 +726,8 @@
   2.307    have intf: "set_integrable lborel {a..b} f"
   2.308      by (rule borel_integrable_atLeastAtMost', rule contf)
   2.309    have "((\<lambda>u. integral {a..u} f) has_vector_derivative f x) (at x within {a..b})"
   2.310 -    apply (intro integral_has_vector_derivative)
   2.311 -    using \<open>a \<le> x\<close> \<open>x \<le> b\<close> by (intro continuous_on_subset [OF contf], auto)
   2.312 +    using \<open>a \<le> x\<close> \<open>x \<le> b\<close> 
   2.313 +    by (auto intro: integral_has_vector_derivative continuous_on_subset [OF contf])
   2.314    then have "((\<lambda>u. integral {a..u} f) has_vector_derivative (f x)) (at x within {a..b})"
   2.315      by simp
   2.316    then have "(?F has_vector_derivative (f x)) (at x within {a..b})"
   2.317 @@ -760,8 +741,8 @@
   2.318      then show "(LBINT y=c..a. f y) + (LBINT y=a..u. f y) = (LBINT y=c..u. f y)"
   2.319        using assms
   2.320        apply (intro interval_integral_sum)
   2.321 -      apply (auto simp add: interval_lebesgue_integrable_def simp del: real_scaleR_def)
   2.322 -      by (rule set_integrable_subset [OF intf], auto simp add: min_def max_def)
   2.323 +      apply (auto simp: interval_lebesgue_integrable_def simp del: real_scaleR_def)
   2.324 +      by (rule set_integrable_subset [OF intf], auto simp: min_def max_def)
   2.325    qed (insert assms, auto)
   2.326  qed
   2.327  
   2.328 @@ -771,7 +752,7 @@
   2.329    shows "\<exists>F. \<forall>x :: real. a < x \<longrightarrow> x < b \<longrightarrow> (F has_vector_derivative f x) (at x)"
   2.330  proof -
   2.331    from einterval_nonempty [OF \<open>a < b\<close>] obtain c :: real where [simp]: "a < c" "c < b"
   2.332 -    by (auto simp add: einterval_def)
   2.333 +    by (auto simp: einterval_def)
   2.334    let ?F = "(\<lambda>u. LBINT y=c..u. f y)"
   2.335    show ?thesis
   2.336    proof (rule exI, clarsimp)
   2.337 @@ -779,22 +760,24 @@
   2.338      assume [simp]: "a < x" "x < b"
   2.339      have 1: "a < min c x" by simp
   2.340      from einterval_nonempty [OF 1] obtain d :: real where [simp]: "a < d" "d < c" "d < x"
   2.341 -      by (auto simp add: einterval_def)
   2.342 +      by (auto simp: einterval_def)
   2.343      have 2: "max c x < b" by simp
   2.344      from einterval_nonempty [OF 2] obtain e :: real where [simp]: "c < e" "x < e" "e < b"
   2.345 -      by (auto simp add: einterval_def)
   2.346 -    show "(?F has_vector_derivative f x) (at x)"
   2.347 -      (* TODO: factor out the next three lines to has_field_derivative_within_open *)
   2.348 -      unfolding has_vector_derivative_def
   2.349 -      apply (subst has_derivative_within_open [of _ "{d<..<e}", symmetric], auto)
   2.350 -      apply (subst has_vector_derivative_def [symmetric])
   2.351 -      apply (rule has_vector_derivative_within_subset [of _ _ _ "{d..e}"])
   2.352 -      apply (rule interval_integral_FTC2, auto simp add: less_imp_le)
   2.353 -      apply (rule continuous_at_imp_continuous_on)
   2.354 -      apply (auto intro!: contf)
   2.355 -      apply (rule order_less_le_trans, rule \<open>a < d\<close>, auto)
   2.356 -      apply (rule order_le_less_trans) prefer 2
   2.357 -      by (rule \<open>e < b\<close>, auto)
   2.358 +      by (auto simp: einterval_def)
   2.359 +    have "(?F has_vector_derivative f x) (at x within {d<..<e})"
   2.360 +    proof (rule has_vector_derivative_within_subset [of _ _ _ "{d..e}"])
   2.361 +      have "continuous_on {d..e} f"
   2.362 +      proof (intro continuous_at_imp_continuous_on ballI contf; clarsimp)
   2.363 +        show "\<And>x. \<lbrakk>d \<le> x; x \<le> e\<rbrakk> \<Longrightarrow> a < ereal x"
   2.364 +          using \<open>a < ereal d\<close> ereal_less_ereal_Ex by auto
   2.365 +        show "\<And>x. \<lbrakk>d \<le> x; x \<le> e\<rbrakk> \<Longrightarrow> ereal x < b"
   2.366 +          using \<open>ereal e < b\<close> ereal_less_eq(3) le_less_trans by blast
   2.367 +      qed
   2.368 +      then show "(?F has_vector_derivative f x) (at x within {d..e})"
   2.369 +        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>)
   2.370 +    qed auto
   2.371 +    then show "(?F has_vector_derivative f x) (at x)"
   2.372 +      by (force simp: has_vector_derivative_within_open [of _ "{d<..<e}"])
   2.373    qed
   2.374  qed
   2.375  
   2.376 @@ -815,44 +798,36 @@
   2.377      using derivg unfolding has_field_derivative_iff_has_vector_derivative .
   2.378    then have contg [simp]: "continuous_on {a..b} g"
   2.379      by (rule continuous_on_vector_derivative) auto
   2.380 -  have 1: "\<And>u. min (g a) (g b) \<le> u \<Longrightarrow> u \<le> max (g a) (g b) \<Longrightarrow>
   2.381 -      \<exists>x\<in>{a..b}. u = g x"
   2.382 -    apply (case_tac "g a \<le> g b")
   2.383 -    apply (auto simp add: min_def max_def less_imp_le)
   2.384 -    apply (frule (1) IVT' [of g], auto simp add: assms)
   2.385 -    by (frule (1) IVT2' [of g], auto simp add: assms)
   2.386 -  from contg \<open>a \<le> b\<close> have "\<exists>c d. g ` {a..b} = {c..d} \<and> c \<le> d"
   2.387 -    by (elim continuous_image_closed_interval)
   2.388 -  then obtain c d where g_im: "g ` {a..b} = {c..d}" and "c \<le> d" by auto
   2.389 -  have "\<exists>F. \<forall>x\<in>{a..b}. (F has_vector_derivative (f (g x))) (at (g x) within (g ` {a..b}))"
   2.390 -    apply (rule exI, auto, subst g_im)
   2.391 -    apply (rule interval_integral_FTC2 [of c c d])
   2.392 -    using \<open>c \<le> d\<close> apply auto
   2.393 -    apply (rule continuous_on_subset [OF contf])
   2.394 -    using g_im by auto
   2.395 -  then guess F ..
   2.396 -  then have derivF: "\<And>x. a \<le> x \<Longrightarrow> x \<le> b \<Longrightarrow>
   2.397 -    (F has_vector_derivative (f (g x))) (at (g x) within (g ` {a..b}))" by auto
   2.398 -  have contf2: "continuous_on {min (g a) (g b)..max (g a) (g b)} f"
   2.399 -    apply (rule continuous_on_subset [OF contf])
   2.400 -    apply (auto simp add: image_def)
   2.401 -    by (erule 1)
   2.402 +  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
   2.403 +    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>)
   2.404 +  obtain c d where g_im: "g ` {a..b} = {c..d}" and "c \<le> d"
   2.405 +    by (metis continuous_image_closed_interval contg \<open>a \<le> b\<close>)
   2.406 +  obtain F where derivF:
   2.407 +         "\<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}))" 
   2.408 +    using continuous_on_subset [OF contf] g_im
   2.409 +      by (metis antiderivative_continuous atLeastAtMost_iff image_subset_iff set_eq_subset)
   2.410    have contfg: "continuous_on {a..b} (\<lambda>x. f (g x))"
   2.411      by (blast intro: continuous_on_compose2 contf contg)
   2.412 -  have "LBINT x=a..b. g' x *\<^sub>R f (g x) = F (g b) - F (g a)"
   2.413 -    apply (subst interval_integral_Icc, simp add: assms)
   2.414 -    unfolding set_lebesgue_integral_def
   2.415 -    apply (rule integral_FTC_atLeastAtMost[of a b "\<lambda>x. F (g x)", OF \<open>a \<le> b\<close>])
   2.416 -    apply (rule vector_diff_chain_within[OF v_derivg derivF, unfolded comp_def])
   2.417 +  have "LBINT x. indicat_real {a..b} x *\<^sub>R g' x *\<^sub>R f (g x) = F (g b) - F (g a)"
   2.418 +    apply (rule integral_FTC_atLeastAtMost
   2.419 +                [OF \<open>a \<le> b\<close> vector_diff_chain_within[OF v_derivg derivF, unfolded comp_def]])
   2.420      apply (auto intro!: continuous_on_scaleR contg' contfg)
   2.421      done
   2.422 +  then have "LBINT x=a..b. g' x *\<^sub>R f (g x) = F (g b) - F (g a)"
   2.423 +    by (simp add: assms interval_integral_Icc set_lebesgue_integral_def)
   2.424    moreover have "LBINT y=(g a)..(g b). f y = F (g b) - F (g a)"
   2.425 -    apply (rule interval_integral_FTC_finite)
   2.426 -    apply (rule contf2)
   2.427 -    apply (frule (1) 1, auto)
   2.428 -    apply (rule has_vector_derivative_within_subset [OF derivF])
   2.429 -    apply (auto simp add: image_def)
   2.430 -    by (rule 1, auto)
   2.431 +  proof (rule interval_integral_FTC_finite)
   2.432 +    show "continuous_on {min (g a) (g b)..max (g a) (g b)} f"
   2.433 +      by (rule continuous_on_subset [OF contf]) (auto simp: image_def 1)
   2.434 +    show "(F has_vector_derivative f y) (at y within {min (g a) (g b)..max (g a) (g b)})" 
   2.435 +      if y: "min (g a) (g b) \<le> y" "y \<le> max (g a) (g b)" for y
   2.436 +    proof -
   2.437 +      obtain x where "a \<le> x" "x \<le> b" "y = g x"
   2.438 +        using 1 y by force
   2.439 +      then show ?thesis
   2.440 +        by (auto simp: image_def intro!: 1  has_vector_derivative_within_subset [OF derivF])
   2.441 +    qed
   2.442 +  qed
   2.443    ultimately show ?thesis by simp
   2.444  qed
   2.445  
   2.446 @@ -871,86 +846,85 @@
   2.447    and integrable2: "set_integrable lborel (einterval A B) (\<lambda>x. f x)"
   2.448    shows "(LBINT x=A..B. f x) = (LBINT x=a..b. g' x *\<^sub>R f (g x))"
   2.449  proof -
   2.450 -  from einterval_Icc_approximation[OF \<open>a < b\<close>] guess u l . note approx [simp] = this
   2.451 +  obtain u l where approx [simp]:
   2.452 +    "einterval a b = (\<Union>i. {l i .. u i})"
   2.453 +    "incseq u" "decseq l" "\<And>i. l i < u i" "\<And>i. a < l i" "\<And>i. u i < b"
   2.454 +    "l \<longlonglongrightarrow> a" "u \<longlonglongrightarrow> b" 
   2.455 +    by (blast intro: einterval_Icc_approximation[OF \<open>a < b\<close>])
   2.456    note less_imp_le [simp]
   2.457    have [simp]: "\<And>x i. l i \<le> x \<Longrightarrow> a < ereal x"
   2.458      by (rule order_less_le_trans, rule approx, force)
   2.459    have [simp]: "\<And>x i. x \<le> u i \<Longrightarrow> ereal x < b"
   2.460      by (rule order_le_less_trans, subst ereal_less_eq(3), assumption, rule approx)
   2.461 -  have [simp]: "\<And>i. l i < b"
   2.462 -    apply (rule order_less_trans) prefer 2
   2.463 -    by (rule approx, auto, rule approx)
   2.464 +  then have lessb[simp]: "\<And>i. l i < b"
   2.465 +    using approx(4) less_eq_real_def by blast
   2.466    have [simp]: "\<And>i. a < u i"
   2.467      by (rule order_less_trans, rule approx, auto, rule approx)
   2.468 -  have [simp]: "\<And>i j. i \<le> j \<Longrightarrow> l j \<le> l i" by (rule decseqD, rule approx)
   2.469 +  have lle[simp]: "\<And>i j. i \<le> j \<Longrightarrow> l j \<le> l i" by (rule decseqD, rule approx)
   2.470    have [simp]: "\<And>i j. i \<le> j \<Longrightarrow> u i \<le> u j" by (rule incseqD, rule approx)
   2.471 -  have g_nondec [simp]: "\<And>x y. a < x \<Longrightarrow> x \<le> y \<Longrightarrow> y < b \<Longrightarrow> g x \<le> g y"
   2.472 -    apply (erule DERIV_nonneg_imp_nondecreasing, auto)
   2.473 -    apply (rule exI, rule conjI, rule deriv_g)
   2.474 -    apply (erule order_less_le_trans, auto)
   2.475 -    apply (rule order_le_less_trans, subst ereal_less_eq(3), assumption, auto)
   2.476 -    apply (rule g'_nonneg)
   2.477 -    apply (rule less_imp_le, erule order_less_le_trans, auto)
   2.478 -    by (rule less_imp_le, rule le_less_trans, subst ereal_less_eq(3), assumption, auto)
   2.479 +  have g_nondec [simp]: "g x \<le> g y" if "a < x" "x \<le> y" "y < b" for x y
   2.480 +  proof (rule DERIV_nonneg_imp_nondecreasing [OF \<open>x \<le> y\<close>], intro exI conjI allI impI)
   2.481 +    show "\<And>u. x \<le> u \<and> u \<le> y \<Longrightarrow> (g has_real_derivative g' u) (at u)"
   2.482 +      by (meson deriv_g ereal_less_eq(3) le_less_trans less_le_trans that)
   2.483 +    show "\<And>u. x \<le> u \<and> u \<le> y \<Longrightarrow> 0 \<le> g' u"
   2.484 +      by (meson assms(5) dual_order.trans le_ereal_le less_imp_le order_refl that)
   2.485 +  qed
   2.486    have "A \<le> B" and un: "einterval A B = (\<Union>i. {g(l i)<..<g(u i)})"
   2.487    proof -
   2.488      have A2: "(\<lambda>i. g (l i)) \<longlonglongrightarrow> A"
   2.489 -      using A apply (auto simp add: einterval_def tendsto_at_iff_sequentially comp_def)
   2.490 +      using A apply (auto simp: einterval_def tendsto_at_iff_sequentially comp_def)
   2.491        by (drule_tac x = "\<lambda>i. ereal (l i)" in spec, auto)
   2.492      hence A3: "\<And>i. g (l i) \<ge> A"
   2.493 -      by (intro decseq_le, auto simp add: decseq_def)
   2.494 +      by (intro decseq_le, auto simp: decseq_def)
   2.495      have B2: "(\<lambda>i. g (u i)) \<longlonglongrightarrow> B"
   2.496 -      using B apply (auto simp add: einterval_def tendsto_at_iff_sequentially comp_def)
   2.497 +      using B apply (auto simp: einterval_def tendsto_at_iff_sequentially comp_def)
   2.498        by (drule_tac x = "\<lambda>i. ereal (u i)" in spec, auto)
   2.499      hence B3: "\<And>i. g (u i) \<le> B"
   2.500 -      by (intro incseq_le, auto simp add: incseq_def)
   2.501 -    show "A \<le> B"
   2.502 -      apply (rule order_trans [OF A3 [of 0]])
   2.503 -      apply (rule order_trans [OF _ B3 [of 0]])
   2.504 +      by (intro incseq_le, auto simp: incseq_def)
   2.505 +    have "ereal (g (l 0)) \<le> ereal (g (u 0))"
   2.506        by auto
   2.507 +    then show "A \<le> B"
   2.508 +      by (meson A3 B3 order.trans)
   2.509      { fix x :: real
   2.510        assume "A < x" and "x < B"
   2.511        then have "eventually (\<lambda>i. ereal (g (l i)) < x \<and> x < ereal (g (u i))) sequentially"
   2.512 -        apply (intro eventually_conj order_tendstoD)
   2.513 -        by (rule A2, assumption, rule B2, assumption)
   2.514 +        by (fast intro: eventually_conj order_tendstoD A2 B2)
   2.515        hence "\<exists>i. g (l i) < x \<and> x < g (u i)"
   2.516          by (simp add: eventually_sequentially, auto)
   2.517      } note AB = this
   2.518      show "einterval A B = (\<Union>i. {g(l i)<..<g(u i)})"
   2.519 -      apply (auto simp add: einterval_def)
   2.520 -      apply (erule (1) AB)
   2.521 -      apply (rule order_le_less_trans, rule A3, simp)
   2.522 -      apply (rule order_less_le_trans) prefer 2
   2.523 -      by (rule B3, simp)
   2.524 +    proof
   2.525 +      show "einterval A B \<subseteq> (\<Union>i. {g(l i)<..<g(u i)})"
   2.526 +        by (auto simp: einterval_def AB)
   2.527 +      show "(\<Union>i. {g(l i)<..<g(u i)}) \<subseteq> einterval A B"
   2.528 +      proof (clarsimp simp add: einterval_def, intro conjI)
   2.529 +        show "\<And>x i. \<lbrakk>g (l i) < x; x < g (u i)\<rbrakk> \<Longrightarrow> A < ereal x"
   2.530 +          using A3 le_ereal_less by blast
   2.531 +        show "\<And>x i. \<lbrakk>g (l i) < x; x < g (u i)\<rbrakk> \<Longrightarrow> ereal x < B"
   2.532 +          using B3 ereal_le_less by blast
   2.533 +      qed
   2.534 +    qed
   2.535    qed
   2.536    (* finally, the main argument *)
   2.537 -  {
   2.538 -     fix i
   2.539 -     have "(LBINT x=l i.. u i. g' x *\<^sub>R f (g x)) = (LBINT y=g (l i)..g (u i). f y)"
   2.540 -        apply (rule interval_integral_substitution_finite, auto)
   2.541 -        apply (rule DERIV_subset)
   2.542 -        unfolding has_field_derivative_iff_has_vector_derivative[symmetric]
   2.543 -        apply (rule deriv_g)
   2.544 -        apply (auto intro!: continuous_at_imp_continuous_on contf contg')
   2.545 -        done
   2.546 -  } note eq1 = this
   2.547 +  have eq1: "(LBINT x=l i.. u i. g' x *\<^sub>R f (g x)) = (LBINT y=g (l i)..g (u i). f y)" for i
   2.548 +    apply (rule interval_integral_substitution_finite [OF _ DERIV_subset [OF deriv_g]])
   2.549 +    unfolding has_field_derivative_iff_has_vector_derivative[symmetric]
   2.550 +         apply (auto intro!: continuous_at_imp_continuous_on contf contg')
   2.551 +    done
   2.552    have "(\<lambda>i. LBINT x=l i..u i. g' x *\<^sub>R f (g x)) \<longlonglongrightarrow> (LBINT x=a..b. g' x *\<^sub>R f (g x))"
   2.553      apply (rule interval_integral_Icc_approx_integrable [OF \<open>a < b\<close> approx])
   2.554      by (rule assms)
   2.555    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))"
   2.556      by (simp add: eq1)
   2.557    have incseq: "incseq (\<lambda>i. {g (l i)<..<g (u i)})"
   2.558 -    apply (auto simp add: incseq_def)
   2.559 -    apply (rule order_le_less_trans)
   2.560 -    prefer 2 apply (assumption, auto)
   2.561 -    by (erule order_less_le_trans, rule g_nondec, auto)
   2.562 -  have "(\<lambda>i. (LBINT y=g (l i)..g (u i). f y)) \<longlonglongrightarrow> (LBINT x = A..B. f x)"
   2.563 -    apply (subst interval_lebesgue_integral_le_eq, auto simp del: real_scaleR_def)
   2.564 -    apply (subst interval_lebesgue_integral_le_eq, rule \<open>A \<le> B\<close>)
   2.565 -    apply (subst un, rule set_integral_cont_up, auto simp del: real_scaleR_def)
   2.566 -    apply (rule incseq)
   2.567 -    apply (subst un [symmetric])
   2.568 -    by (rule integrable2)
   2.569 +    apply (auto simp: incseq_def)
   2.570 +    using lessb lle approx(5) g_nondec le_less_trans apply blast
   2.571 +    by (force intro: less_le_trans)
   2.572 +  have "(\<lambda>i. set_lebesgue_integral lborel {g (l i)<..<g (u i)} f)
   2.573 +        \<longlonglongrightarrow> set_lebesgue_integral lborel (einterval A B) f"
   2.574 +    unfolding un  by (rule set_integral_cont_up) (use incseq  integrable2 un in auto)
   2.575 +  then have "(\<lambda>i. (LBINT y=g (l i)..g (u i). f y)) \<longlonglongrightarrow> (LBINT x = A..B. f x)"
   2.576 +    by (simp add: interval_lebesgue_integral_le_eq \<open>A \<le> B\<close>)
   2.577    thus ?thesis by (intro LIMSEQ_unique [OF _ 2])
   2.578  qed
   2.579  
   2.580 @@ -975,98 +949,97 @@
   2.581  proof -
   2.582    from einterval_Icc_approximation[OF \<open>a < b\<close>] guess u l . note approx [simp] = this
   2.583    note less_imp_le [simp]
   2.584 -  have [simp]: "\<And>x i. l i \<le> x \<Longrightarrow> a < ereal x"
   2.585 +  have aless[simp]: "\<And>x i. l i \<le> x \<Longrightarrow> a < ereal x"
   2.586      by (rule order_less_le_trans, rule approx, force)
   2.587 -  have [simp]: "\<And>x i. x \<le> u i \<Longrightarrow> ereal x < b"
   2.588 +  have lessb[simp]: "\<And>x i. x \<le> u i \<Longrightarrow> ereal x < b"
   2.589      by (rule order_le_less_trans, subst ereal_less_eq(3), assumption, rule approx)
   2.590 -  have [simp]: "\<And>i. l i < b"
   2.591 -    apply (rule order_less_trans) prefer 2
   2.592 -    by (rule approx, auto, rule approx)
   2.593 -  have [simp]: "\<And>i. a < u i"
   2.594 +  have llb[simp]: "\<And>i. l i < b"
   2.595 +    using lessb approx(4) less_eq_real_def by blast
   2.596 +  have alu[simp]: "\<And>i. a < u i"
   2.597      by (rule order_less_trans, rule approx, auto, rule approx)
   2.598    have [simp]: "\<And>i j. i \<le> j \<Longrightarrow> l j \<le> l i" by (rule decseqD, rule approx)
   2.599 -  have [simp]: "\<And>i j. i \<le> j \<Longrightarrow> u i \<le> u j" by (rule incseqD, rule approx)
   2.600 -  have g_nondec [simp]: "\<And>x y. a < x \<Longrightarrow> x \<le> y \<Longrightarrow> y < b \<Longrightarrow> g x \<le> g y"
   2.601 -    apply (erule DERIV_nonneg_imp_nondecreasing, auto)
   2.602 -    apply (rule exI, rule conjI, rule deriv_g)
   2.603 -    apply (erule order_less_le_trans, auto)
   2.604 -    apply (rule order_le_less_trans, subst ereal_less_eq(3), assumption, auto)
   2.605 -    apply (rule g'_nonneg)
   2.606 -    apply (rule less_imp_le, erule order_less_le_trans, auto)
   2.607 -    by (rule less_imp_le, rule le_less_trans, subst ereal_less_eq(3), assumption, auto)
   2.608 +  have uleu[simp]: "\<And>i j. i \<le> j \<Longrightarrow> u i \<le> u j" by (rule incseqD, rule approx)
   2.609 +  have g_nondec [simp]: "g x \<le> g y" if "a < x" "x \<le> y" "y < b" for x y
   2.610 +  proof (rule DERIV_nonneg_imp_nondecreasing [OF \<open>x \<le> y\<close>], intro exI conjI allI impI)
   2.611 +    show "\<And>u. x \<le> u \<and> u \<le> y \<Longrightarrow> (g has_real_derivative g' u) (at u)"
   2.612 +      by (meson deriv_g ereal_less_eq(3) le_less_trans less_le_trans that)
   2.613 +    show "\<And>u. x \<le> u \<and> u \<le> y \<Longrightarrow> 0 \<le> g' u"
   2.614 +      by (meson g'_nonneg less_ereal.simps(1) less_trans not_less that)
   2.615 +  qed
   2.616    have "A \<le> B" and un: "einterval A B = (\<Union>i. {g(l i)<..<g(u i)})"
   2.617    proof -
   2.618      have A2: "(\<lambda>i. g (l i)) \<longlonglongrightarrow> A"
   2.619 -      using A apply (auto simp add: einterval_def tendsto_at_iff_sequentially comp_def)
   2.620 +      using A apply (auto simp: einterval_def tendsto_at_iff_sequentially comp_def)
   2.621        by (drule_tac x = "\<lambda>i. ereal (l i)" in spec, auto)
   2.622      hence A3: "\<And>i. g (l i) \<ge> A"
   2.623 -      by (intro decseq_le, auto simp add: decseq_def)
   2.624 +      by (intro decseq_le, auto simp: decseq_def)
   2.625      have B2: "(\<lambda>i. g (u i)) \<longlonglongrightarrow> B"
   2.626 -      using B apply (auto simp add: einterval_def tendsto_at_iff_sequentially comp_def)
   2.627 +      using B apply (auto simp: einterval_def tendsto_at_iff_sequentially comp_def)
   2.628        by (drule_tac x = "\<lambda>i. ereal (u i)" in spec, auto)
   2.629      hence B3: "\<And>i. g (u i) \<le> B"
   2.630 -      by (intro incseq_le, auto simp add: incseq_def)
   2.631 -    show "A \<le> B"
   2.632 -      apply (rule order_trans [OF A3 [of 0]])
   2.633 -      apply (rule order_trans [OF _ B3 [of 0]])
   2.634 +      by (intro incseq_le, auto simp: incseq_def)
   2.635 +    have "ereal (g (l 0)) \<le> ereal (g (u 0))"
   2.636        by auto
   2.637 +    then show "A \<le> B"
   2.638 +      by (meson A3 B3 order.trans)
   2.639      { fix x :: real
   2.640        assume "A < x" and "x < B"
   2.641        then have "eventually (\<lambda>i. ereal (g (l i)) < x \<and> x < ereal (g (u i))) sequentially"
   2.642 -        apply (intro eventually_conj order_tendstoD)
   2.643 -        by (rule A2, assumption, rule B2, assumption)
   2.644 +        by (fast intro: eventually_conj order_tendstoD A2 B2)
   2.645        hence "\<exists>i. g (l i) < x \<and> x < g (u i)"
   2.646          by (simp add: eventually_sequentially, auto)
   2.647      } note AB = this
   2.648      show "einterval A B = (\<Union>i. {g(l i)<..<g(u i)})"
   2.649 -      apply (auto simp add: einterval_def)
   2.650 -      apply (erule (1) AB)
   2.651 -      apply (rule order_le_less_trans, rule A3, simp)
   2.652 -      apply (rule order_less_le_trans) prefer 2
   2.653 -      by (rule B3, simp)
   2.654 +    proof
   2.655 +      show "einterval A B \<subseteq> (\<Union>i. {g (l i)<..<g (u i)})"
   2.656 +        by (auto simp: einterval_def AB)
   2.657 +      show "(\<Union>i. {g (l i)<..<g (u i)}) \<subseteq> einterval A B"
   2.658 +        apply (clarsimp simp: einterval_def, intro conjI)
   2.659 +        using A3 le_ereal_less apply blast
   2.660 +        using B3 ereal_le_less by blast
   2.661 +    qed
   2.662    qed
   2.663 -  (* finally, the main argument *)
   2.664 -  {
   2.665 -     fix i
   2.666 -     have "(LBINT x=l i.. u i. g' x *\<^sub>R f (g x)) = (LBINT y=g (l i)..g (u i). f y)"
   2.667 -        apply (rule interval_integral_substitution_finite, auto)
   2.668 -        apply (rule DERIV_subset, rule deriv_g, auto)
   2.669 -        apply (rule continuous_at_imp_continuous_on, auto, rule contf, auto)
   2.670 -        by (rule continuous_at_imp_continuous_on, auto, rule contg', auto)
   2.671 -     then have "(LBINT x=l i.. u i. (f (g x) * g' x)) = (LBINT y=g (l i)..g (u i). f y)"
   2.672 -       by (simp add: ac_simps)
   2.673 -  } note eq1 = this
   2.674 -  have "(\<lambda>i. LBINT x=l i..u i. f (g x) * g' x)
   2.675 -      \<longlonglongrightarrow> (LBINT x=a..b. f (g x) * g' x)"
   2.676 -    apply (rule interval_integral_Icc_approx_integrable [OF \<open>a < b\<close> approx])
   2.677 -    by (rule assms)
   2.678 -  hence 2: "(\<lambda>i. (LBINT y=g (l i)..g (u i). f y)) \<longlonglongrightarrow> (LBINT x=a..b. f (g x) * g' x)"
   2.679 -    by (simp add: eq1)
   2.680 +    (* finally, the main argument *)
   2.681 +  have eq1: "(LBINT x=l i.. u i. (f (g x) * g' x)) = (LBINT y=g (l i)..g (u i). f y)" for i
   2.682 +  proof -
   2.683 +    have "(LBINT x=l i.. u i. g' x *\<^sub>R f (g x)) = (LBINT y=g (l i)..g (u i). f y)"
   2.684 +      apply (rule interval_integral_substitution_finite [OF _ DERIV_subset [OF deriv_g]])
   2.685 +      unfolding has_field_derivative_iff_has_vector_derivative[symmetric]
   2.686 +           apply (auto intro!: continuous_at_imp_continuous_on contf contg')
   2.687 +      done
   2.688 +    then show ?thesis
   2.689 +      by (simp add: ac_simps)
   2.690 +  qed
   2.691    have incseq: "incseq (\<lambda>i. {g (l i)<..<g (u i)})"
   2.692 -    apply (auto simp add: incseq_def)
   2.693 -    apply (rule order_le_less_trans)
   2.694 -    prefer 2 apply assumption
   2.695 -    apply (rule g_nondec, auto)
   2.696 -    by (erule order_less_le_trans, rule g_nondec, auto)
   2.697 -  have img: "\<And>x i. g (l i) \<le> x \<Longrightarrow> x \<le> g (u i) \<Longrightarrow> \<exists>c \<ge> l i. c \<le> u i \<and> x = g c"
   2.698 -    apply (frule (1) IVT' [of g], auto)
   2.699 -    apply (rule continuous_at_imp_continuous_on, auto)
   2.700 -    by (rule DERIV_isCont, rule deriv_g, auto)
   2.701 -  have nonneg_f2: "\<And>x i. g (l i) \<le> x \<Longrightarrow> x \<le> g (u i) \<Longrightarrow> 0 \<le> f x"
   2.702 -    by (frule (1) img, auto, rule f_nonneg, auto)
   2.703 -  have contf_2: "\<And>x i. g (l i) \<le> x \<Longrightarrow> x \<le> g (u i) \<Longrightarrow> isCont f x"
   2.704 -    by (frule (1) img, auto, rule contf, auto)
   2.705 +    apply (clarsimp simp add: incseq_def, intro conjI)
   2.706 +    apply (meson llb antimono_def approx(3) approx(5) g_nondec le_less_trans)
   2.707 +    using alu uleu approx(6) g_nondec less_le_trans by blast
   2.708 +  have img: "\<exists>c \<ge> l i. c \<le> u i \<and> x = g c" if "g (l i) \<le> x" "x \<le> g (u i)" for x i
   2.709 +  proof -
   2.710 +    have "continuous_on {l i..u i} g"
   2.711 +      by (force intro!: DERIV_isCont deriv_g continuous_at_imp_continuous_on)
   2.712 +    with that show ?thesis
   2.713 +      using IVT' [of g] approx(4) dual_order.strict_implies_order by blast
   2.714 +  qed
   2.715 +  have "continuous_on {g (l i)..g (u i)} f" for i
   2.716 +    apply (intro continuous_intros continuous_at_imp_continuous_on)
   2.717 +    using contf img by force
   2.718 +  then have int_f: "\<And>i. set_integrable lborel {g (l i)<..<g (u i)} f"
   2.719 +    by (rule set_integrable_subset [OF borel_integrable_atLeastAtMost']) (auto intro: less_imp_le)
   2.720    have integrable: "set_integrable lborel (\<Union>i. {g (l i)<..<g (u i)}) f"
   2.721 -    apply (rule pos_integrable_to_top, auto simp del: real_scaleR_def)
   2.722 -    apply (rule incseq)
   2.723 -    apply (rule nonneg_f2, erule less_imp_le, erule less_imp_le)
   2.724 -    apply (rule set_integrable_subset)
   2.725 -    apply (rule borel_integrable_atLeastAtMost')
   2.726 -    apply (rule continuous_at_imp_continuous_on)
   2.727 -    apply (clarsimp, erule (1) contf_2, auto)
   2.728 -    apply (erule less_imp_le)+
   2.729 -    using 2 unfolding interval_lebesgue_integral_def
   2.730 -    by auto
   2.731 +  proof (intro pos_integrable_to_top incseq int_f)
   2.732 +    let ?l = "(LBINT x=a..b. f (g x) * g' x)"
   2.733 +    have "(\<lambda>i. LBINT x=l i..u i. f (g x) * g' x) \<longlonglongrightarrow> ?l"
   2.734 +      by (intro assms interval_integral_Icc_approx_integrable [OF \<open>a < b\<close> approx])
   2.735 +    hence "(\<lambda>i. (LBINT y=g (l i)..g (u i). f y)) \<longlonglongrightarrow> ?l"
   2.736 +      by (simp add: eq1)
   2.737 +    then show "(\<lambda>i. set_lebesgue_integral lborel {g (l i)<..<g (u i)} f) \<longlonglongrightarrow> ?l"
   2.738 +      unfolding interval_lebesgue_integral_def by auto
   2.739 +    have "\<And>x i. g (l i) \<le> x \<Longrightarrow> x \<le> g (u i) \<Longrightarrow> 0 \<le> f x"
   2.740 +      using aless f_nonneg img lessb by blast
   2.741 +    then show "\<And>x i. x \<in> {g (l i)<..<g (u i)} \<Longrightarrow> 0 \<le> f x"
   2.742 +      using less_eq_real_def by auto
   2.743 +  qed (auto simp: greaterThanLessThan_borel)
   2.744    thus "set_integrable lborel (einterval A B) f"
   2.745      by (simp add: un)
   2.746  
   2.747 @@ -1111,7 +1084,7 @@
   2.748    shows "interval_lebesgue_integrable lborel a b f \<Longrightarrow> a \<le> b \<Longrightarrow>
   2.749      norm (LBINT t=a..b. f t) \<le> LBINT t=a..b. norm (f t)"
   2.750    using integral_norm_bound[of lborel "\<lambda>x. indicator (einterval a b) x *\<^sub>R f x"]
   2.751 -  by (auto simp add: interval_lebesgue_integral_def interval_lebesgue_integrable_def set_lebesgue_integral_def)
   2.752 +  by (auto simp: interval_lebesgue_integral_def interval_lebesgue_integrable_def set_lebesgue_integral_def)
   2.753  
   2.754  lemma interval_integral_norm2:
   2.755    "interval_lebesgue_integrable lborel a b f \<Longrightarrow>
   2.756 @@ -1123,7 +1096,7 @@
   2.757    case (le a b)
   2.758    then have "\<bar>LBINT t=a..b. norm (f t)\<bar> = LBINT t=a..b. norm (f t)"
   2.759      using integrable_norm[of lborel "\<lambda>x. indicator (einterval a b) x *\<^sub>R f x"]
   2.760 -    by (auto simp add: interval_lebesgue_integral_def interval_lebesgue_integrable_def set_lebesgue_integral_def
   2.761 +    by (auto simp: interval_lebesgue_integral_def interval_lebesgue_integrable_def set_lebesgue_integral_def
   2.762               intro!: integral_nonneg_AE abs_of_nonneg)
   2.763    then show ?case
   2.764      using le by (simp add: interval_integral_norm)
   2.765 @@ -1134,5 +1107,4 @@
   2.766    apply (intro interval_integral_FTC_finite continuous_intros)
   2.767    by (auto intro!: derivative_eq_intros simp: has_field_derivative_iff_has_vector_derivative[symmetric])
   2.768  
   2.769 -
   2.770  end
     3.1 --- a/src/HOL/Analysis/Path_Connected.thy	Sun May 06 23:30:34 2018 +0200
     3.2 +++ b/src/HOL/Analysis/Path_Connected.thy	Sun May 06 23:59:14 2018 +0100
     3.3 @@ -42,15 +42,15 @@
     3.4  lemma path_eq: "path p \<Longrightarrow> (\<And>t. t \<in> {0..1} \<Longrightarrow> p t = q t) \<Longrightarrow> path q"
     3.5    using continuous_on_eq path_def by blast
     3.6  
     3.7 -lemma path_continuous_image: "path g \<Longrightarrow> continuous_on (path_image g) f \<Longrightarrow> path(f o g)"
     3.8 +lemma path_continuous_image: "path g \<Longrightarrow> continuous_on (path_image g) f \<Longrightarrow> path(f \<circ> g)"
     3.9    unfolding path_def path_image_def
    3.10    using continuous_on_compose by blast
    3.11  
    3.12  lemma path_translation_eq:
    3.13    fixes g :: "real \<Rightarrow> 'a :: real_normed_vector"
    3.14 -  shows "path((\<lambda>x. a + x) o g) = path g"
    3.15 +  shows "path((\<lambda>x. a + x) \<circ> g) = path g"
    3.16  proof -
    3.17 -  have g: "g = (\<lambda>x. -a + x) o ((\<lambda>x. a + x) o g)"
    3.18 +  have g: "g = (\<lambda>x. -a + x) \<circ> ((\<lambda>x. a + x) \<circ> g)"
    3.19      by (rule ext) simp
    3.20    show ?thesis
    3.21      unfolding path_def
    3.22 @@ -64,12 +64,12 @@
    3.23  lemma path_linear_image_eq:
    3.24    fixes f :: "'a::euclidean_space \<Rightarrow> 'b::euclidean_space"
    3.25     assumes "linear f" "inj f"
    3.26 -     shows "path(f o g) = path g"
    3.27 +     shows "path(f \<circ> g) = path g"
    3.28  proof -
    3.29    from linear_injective_left_inverse [OF assms]
    3.30    obtain h where h: "linear h" "h \<circ> f = id"
    3.31      by blast
    3.32 -  then have g: "g = h o (f o g)"
    3.33 +  then have g: "g = h \<circ> (f \<circ> g)"
    3.34      by (metis comp_assoc id_comp)
    3.35    show ?thesis
    3.36      unfolding path_def
    3.37 @@ -77,58 +77,58 @@
    3.38      by (metis g continuous_on_compose linear_continuous_on linear_conv_bounded_linear)
    3.39  qed
    3.40  
    3.41 -lemma pathstart_translation: "pathstart((\<lambda>x. a + x) o g) = a + pathstart g"
    3.42 +lemma pathstart_translation: "pathstart((\<lambda>x. a + x) \<circ> g) = a + pathstart g"
    3.43    by (simp add: pathstart_def)
    3.44  
    3.45 -lemma pathstart_linear_image_eq: "linear f \<Longrightarrow> pathstart(f o g) = f(pathstart g)"
    3.46 +lemma pathstart_linear_image_eq: "linear f \<Longrightarrow> pathstart(f \<circ> g) = f(pathstart g)"
    3.47    by (simp add: pathstart_def)
    3.48  
    3.49 -lemma pathfinish_translation: "pathfinish((\<lambda>x. a + x) o g) = a + pathfinish g"
    3.50 +lemma pathfinish_translation: "pathfinish((\<lambda>x. a + x) \<circ> g) = a + pathfinish g"
    3.51    by (simp add: pathfinish_def)
    3.52  
    3.53 -lemma pathfinish_linear_image: "linear f \<Longrightarrow> pathfinish(f o g) = f(pathfinish g)"
    3.54 +lemma pathfinish_linear_image: "linear f \<Longrightarrow> pathfinish(f \<circ> g) = f(pathfinish g)"
    3.55    by (simp add: pathfinish_def)
    3.56  
    3.57 -lemma path_image_translation: "path_image((\<lambda>x. a + x) o g) = (\<lambda>x. a + x) ` (path_image g)"
    3.58 +lemma path_image_translation: "path_image((\<lambda>x. a + x) \<circ> g) = (\<lambda>x. a + x) ` (path_image g)"
    3.59    by (simp add: image_comp path_image_def)
    3.60  
    3.61 -lemma path_image_linear_image: "linear f \<Longrightarrow> path_image(f o g) = f ` (path_image g)"
    3.62 +lemma path_image_linear_image: "linear f \<Longrightarrow> path_image(f \<circ> g) = f ` (path_image g)"
    3.63    by (simp add: image_comp path_image_def)
    3.64  
    3.65 -lemma reversepath_translation: "reversepath((\<lambda>x. a + x) o g) = (\<lambda>x. a + x) o reversepath g"
    3.66 +lemma reversepath_translation: "reversepath((\<lambda>x. a + x) \<circ> g) = (\<lambda>x. a + x) \<circ> reversepath g"
    3.67    by (rule ext) (simp add: reversepath_def)
    3.68  
    3.69 -lemma reversepath_linear_image: "linear f \<Longrightarrow> reversepath(f o g) = f o reversepath g"
    3.70 +lemma reversepath_linear_image: "linear f \<Longrightarrow> reversepath(f \<circ> g) = f \<circ> reversepath g"
    3.71    by (rule ext) (simp add: reversepath_def)
    3.72  
    3.73  lemma joinpaths_translation:
    3.74 -    "((\<lambda>x. a + x) o g1) +++ ((\<lambda>x. a + x) o g2) = (\<lambda>x. a + x) o (g1 +++ g2)"
    3.75 +    "((\<lambda>x. a + x) \<circ> g1) +++ ((\<lambda>x. a + x) \<circ> g2) = (\<lambda>x. a + x) \<circ> (g1 +++ g2)"
    3.76    by (rule ext) (simp add: joinpaths_def)
    3.77  
    3.78 -lemma joinpaths_linear_image: "linear f \<Longrightarrow> (f o g1) +++ (f o g2) = f o (g1 +++ g2)"
    3.79 +lemma joinpaths_linear_image: "linear f \<Longrightarrow> (f \<circ> g1) +++ (f \<circ> g2) = f \<circ> (g1 +++ g2)"
    3.80    by (rule ext) (simp add: joinpaths_def)
    3.81  
    3.82  lemma simple_path_translation_eq:
    3.83    fixes g :: "real \<Rightarrow> 'a::euclidean_space"
    3.84 -  shows "simple_path((\<lambda>x. a + x) o g) = simple_path g"
    3.85 +  shows "simple_path((\<lambda>x. a + x) \<circ> g) = simple_path g"
    3.86    by (simp add: simple_path_def path_translation_eq)
    3.87  
    3.88  lemma simple_path_linear_image_eq:
    3.89    fixes f :: "'a::euclidean_space \<Rightarrow> 'b::euclidean_space"
    3.90    assumes "linear f" "inj f"
    3.91 -    shows "simple_path(f o g) = simple_path g"
    3.92 +    shows "simple_path(f \<circ> g) = simple_path g"
    3.93    using assms inj_on_eq_iff [of f]
    3.94    by (auto simp: path_linear_image_eq simple_path_def path_translation_eq)
    3.95  
    3.96  lemma arc_translation_eq:
    3.97    fixes g :: "real \<Rightarrow> 'a::euclidean_space"
    3.98 -  shows "arc((\<lambda>x. a + x) o g) = arc g"
    3.99 +  shows "arc((\<lambda>x. a + x) \<circ> g) = arc g"
   3.100    by (auto simp: arc_def inj_on_def path_translation_eq)
   3.101  
   3.102  lemma arc_linear_image_eq:
   3.103    fixes f :: "'a::euclidean_space \<Rightarrow> 'b::euclidean_space"
   3.104     assumes "linear f" "inj f"
   3.105 -     shows  "arc(f o g) = arc g"
   3.106 +     shows  "arc(f \<circ> g) = arc g"
   3.107    using assms inj_on_eq_iff [of f]
   3.108    by (auto simp: arc_def inj_on_def path_linear_image_eq)
   3.109  
   3.110 @@ -151,7 +151,7 @@
   3.111  
   3.112  lemma simple_path_cases: "simple_path g \<Longrightarrow> arc g \<or> pathfinish g = pathstart g"
   3.113    unfolding simple_path_def arc_def inj_on_def pathfinish_def pathstart_def
   3.114 -  by (force)
   3.115 +  by force
   3.116  
   3.117  lemma simple_path_imp_arc: "simple_path g \<Longrightarrow> pathfinish g \<noteq> pathstart g \<Longrightarrow> arc g"
   3.118    using simple_path_cases by auto
   3.119 @@ -225,10 +225,7 @@
   3.120    have *: "\<And>g. path g \<Longrightarrow> path (reversepath g)"
   3.121      unfolding path_def reversepath_def
   3.122      apply (rule continuous_on_compose[unfolded o_def, of _ "\<lambda>x. 1 - x"])
   3.123 -    apply (intro continuous_intros)
   3.124 -    apply (rule continuous_on_subset[of "{0..1}"])
   3.125 -    apply assumption
   3.126 -    apply auto
   3.127 +    apply (auto intro: continuous_intros continuous_on_subset[of "{0..1}"])
   3.128      done
   3.129    show ?thesis
   3.130      using *[of "reversepath g"] *[of g]
   3.131 @@ -245,12 +242,7 @@
   3.132    have **: "\<And>x y::real. 1-x = 1-y \<Longrightarrow> x = y"
   3.133      by simp
   3.134    show ?thesis
   3.135 -    apply (auto simp: arc_def inj_on_def path_reversepath)
   3.136 -    apply (simp add: arc_imp_path assms)
   3.137 -    apply (rule **)
   3.138 -    apply (rule inj_onD [OF injg])
   3.139 -    apply (auto simp: reversepath_def)
   3.140 -    done
   3.141 +    using assms  by (clarsimp simp: arc_def intro!: inj_onI) (simp add: inj_onD reversepath_def **)
   3.142  qed
   3.143  
   3.144  lemma simple_path_reversepath: "simple_path g \<Longrightarrow> simple_path (reversepath g)"
   3.145 @@ -369,19 +361,19 @@
   3.146    using assms and path_image_join_subset[of g1 g2]
   3.147    by auto
   3.148  
   3.149 -lemma pathstart_compose: "pathstart(f o p) = f(pathstart p)"
   3.150 +lemma pathstart_compose: "pathstart(f \<circ> p) = f(pathstart p)"
   3.151    by (simp add: pathstart_def)
   3.152  
   3.153 -lemma pathfinish_compose: "pathfinish(f o p) = f(pathfinish p)"
   3.154 +lemma pathfinish_compose: "pathfinish(f \<circ> p) = f(pathfinish p)"
   3.155    by (simp add: pathfinish_def)
   3.156  
   3.157 -lemma path_image_compose: "path_image (f o p) = f ` (path_image p)"
   3.158 +lemma path_image_compose: "path_image (f \<circ> p) = f ` (path_image p)"
   3.159    by (simp add: image_comp path_image_def)
   3.160  
   3.161 -lemma path_compose_join: "f o (p +++ q) = (f o p) +++ (f o q)"
   3.162 +lemma path_compose_join: "f \<circ> (p +++ q) = (f \<circ> p) +++ (f \<circ> q)"
   3.163    by (rule ext) (simp add: joinpaths_def)
   3.164  
   3.165 -lemma path_compose_reversepath: "f o reversepath p = reversepath(f o p)"
   3.166 +lemma path_compose_reversepath: "f \<circ> reversepath p = reversepath(f \<circ> p)"
   3.167    by (rule ext) (simp add: reversepath_def)
   3.168  
   3.169  lemma joinpaths_eq:
   3.170 @@ -440,15 +432,15 @@
   3.171    have gg: "g2 0 = g1 1"
   3.172      by (metis assms(3) pathfinish_def pathstart_def)
   3.173    have 1: "continuous_on {0..1/2} (g1 +++ g2)"
   3.174 -    apply (rule continuous_on_eq [of _ "g1 o (\<lambda>x. 2*x)"])
   3.175 +    apply (rule continuous_on_eq [of _ "g1 \<circ> (\<lambda>x. 2*x)"])
   3.176      apply (rule continuous_intros | simp add: joinpaths_def assms)+
   3.177      done
   3.178 -  have "continuous_on {1/2..1} (g2 o (\<lambda>x. 2*x-1))"
   3.179 +  have "continuous_on {1/2..1} (g2 \<circ> (\<lambda>x. 2*x-1))"
   3.180      apply (rule continuous_on_subset [of "{1/2..1}"])
   3.181      apply (rule continuous_intros | simp add: image_affinity_atLeastAtMost_diff assms)+
   3.182      done
   3.183    then have 2: "continuous_on {1/2..1} (g1 +++ g2)"
   3.184 -    apply (rule continuous_on_eq [of "{1/2..1}" "g2 o (\<lambda>x. 2*x-1)"])
   3.185 +    apply (rule continuous_on_eq [of "{1/2..1}" "g2 \<circ> (\<lambda>x. 2*x-1)"])
   3.186      apply (rule assms continuous_intros | simp add: joinpaths_def mult.commute half_bounded_equal gg)+
   3.187      done
   3.188    show ?thesis
   3.189 @@ -793,7 +785,7 @@
   3.190    assumes "path g" "u \<in> {0..1}" "v \<in> {0..1}"
   3.191      shows "path(subpath u v g)"
   3.192  proof -
   3.193 -  have "continuous_on {0..1} (g o (\<lambda>x. ((v-u) * x+ u)))"
   3.194 +  have "continuous_on {0..1} (g \<circ> (\<lambda>x. ((v-u) * x+ u)))"
   3.195      apply (rule continuous_intros | simp)+
   3.196      apply (simp add: image_affinity_atLeastAtMost [where c=u])
   3.197      using assms
   3.198 @@ -818,10 +810,10 @@
   3.199  lemma reversepath_subpath: "reversepath(subpath u v g) = subpath v u g"
   3.200    by (simp add: reversepath_def subpath_def algebra_simps)
   3.201  
   3.202 -lemma subpath_translation: "subpath u v ((\<lambda>x. a + x) o g) = (\<lambda>x. a + x) o subpath u v g"
   3.203 +lemma subpath_translation: "subpath u v ((\<lambda>x. a + x) \<circ> g) = (\<lambda>x. a + x) \<circ> subpath u v g"
   3.204    by (rule ext) (simp add: subpath_def)
   3.205  
   3.206 -lemma subpath_linear_image: "linear f \<Longrightarrow> subpath u v (f o g) = f o subpath u v g"
   3.207 +lemma subpath_linear_image: "linear f \<Longrightarrow> subpath u v (f \<circ> g) = f \<circ> subpath u v g"
   3.208    by (rule ext) (simp add: subpath_def)
   3.209  
   3.210  lemma affine_ineq:
   3.211 @@ -891,7 +883,7 @@
   3.212      assume "x \<in> closed_segment u v" "y \<in> closed_segment u v" "g x = g y"
   3.213      then have "x = y"
   3.214      using sim [of "(x-u)/(v-u)" "(y-u)/(v-u)"] p
   3.215 -    by (force simp add: inj_on_def closed_segment_real_eq image_affinity_atLeastAtMost divide_simps
   3.216 +    by (force simp: inj_on_def closed_segment_real_eq image_affinity_atLeastAtMost divide_simps
   3.217         split: if_split_asm)
   3.218    } moreover
   3.219    have "path(subpath u v g) \<and> u\<noteq>v"
   3.220 @@ -1105,20 +1097,20 @@
   3.221      by auto
   3.222    show ?thesis
   3.223      unfolding path_def shiftpath_def *
   3.224 -    apply (rule continuous_on_closed_Un)
   3.225 -    apply (rule closed_real_atLeastAtMost)+
   3.226 -    apply (rule continuous_on_eq[of _ "g \<circ> (\<lambda>x. a + x)"])
   3.227 -    prefer 3
   3.228 -    apply (rule continuous_on_eq[of _ "g \<circ> (\<lambda>x. a - 1 + x)"])
   3.229 -    prefer 3
   3.230 -    apply (rule continuous_intros)+
   3.231 -    prefer 2
   3.232 -    apply (rule continuous_intros)+
   3.233 -    apply (rule_tac[1-2] continuous_on_subset[OF assms(1)[unfolded path_def]])
   3.234 -    using assms(3) and **
   3.235 -    apply auto
   3.236 -    apply (auto simp add: field_simps)
   3.237 -    done
   3.238 +  proof (rule continuous_on_closed_Un)
   3.239 +    have contg: "continuous_on {0..1} g"
   3.240 +      using \<open>path g\<close> path_def by blast
   3.241 +    show "continuous_on {0..1-a} (\<lambda>x. if a + x \<le> 1 then g (a + x) else g (a + x - 1))"
   3.242 +    proof (rule continuous_on_eq)
   3.243 +      show "continuous_on {0..1-a} (g \<circ> (+) a)"
   3.244 +        by (intro continuous_intros continuous_on_subset [OF contg]) (use \<open>a \<in> {0..1}\<close> in auto)
   3.245 +    qed auto
   3.246 +    show "continuous_on {1-a..1} (\<lambda>x. if a + x \<le> 1 then g (a + x) else g (a + x - 1))"
   3.247 +    proof (rule continuous_on_eq)
   3.248 +      show "continuous_on {1-a..1} (g \<circ> (+) (a - 1))"
   3.249 +        by (intro continuous_intros continuous_on_subset [OF contg]) (use \<open>a \<in> {0..1}\<close> in auto)
   3.250 +    qed (auto simp:  "**" add.commute add_diff_eq)
   3.251 +  qed auto
   3.252  qed
   3.253  
   3.254  lemma shiftpath_shiftpath:
   3.255 @@ -1131,33 +1123,30 @@
   3.256    by auto
   3.257  
   3.258  lemma path_image_shiftpath:
   3.259 -  assumes "a \<in> {0..1}"
   3.260 +  assumes a: "a \<in> {0..1}"
   3.261      and "pathfinish g = pathstart g"
   3.262    shows "path_image (shiftpath a g) = path_image g"
   3.263  proof -
   3.264    { fix x
   3.265 -    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)"
   3.266 +    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)"
   3.267      then have "\<exists>y\<in>{0..1} \<inter> {x. a + x \<le> 1}. g x = g (a + y)"
   3.268      proof (cases "a \<le> x")
   3.269        case False
   3.270        then show ?thesis
   3.271          apply (rule_tac x="1 + x - a" in bexI)
   3.272 -        using as(1,2) and as(3)[THEN bspec[where x="1 + x - a"]] and assms(1)
   3.273 -        apply (auto simp add: field_simps atomize_not)
   3.274 +        using g gne[of "1 + x - a"] a
   3.275 +        apply (force simp: field_simps)+
   3.276          done
   3.277      next
   3.278        case True
   3.279        then show ?thesis
   3.280 -        using as(1-2) and assms(1)
   3.281 -        apply (rule_tac x="x - a" in bexI)
   3.282 -        apply (auto simp add: field_simps)
   3.283 -        done
   3.284 +        using g a  by (rule_tac x="x - a" in bexI) (auto simp: field_simps)
   3.285      qed
   3.286    }
   3.287    then show ?thesis
   3.288      using assms
   3.289      unfolding shiftpath_def path_image_def pathfinish_def pathstart_def
   3.290 -    by (auto simp add: image_iff)
   3.291 +    by (auto simp: image_iff)
   3.292  qed
   3.293  
   3.294  lemma simple_path_shiftpath:
   3.295 @@ -1172,9 +1161,7 @@
   3.296    show "x = y \<or> x = 0 \<and> y = 1 \<or> x = 1 \<and> y = 0"
   3.297      if "x \<in> {0..1}" "y \<in> {0..1}" "shiftpath a g x = shiftpath a g y" for x y
   3.298      using that a unfolding shiftpath_def
   3.299 -    apply (simp add: split: if_split_asm)
   3.300 -      apply (drule *; auto)+
   3.301 -    done
   3.302 +    by (force split: if_split_asm dest!: *)
   3.303  qed
   3.304  
   3.305  subsection \<open>Special case of straight-line paths\<close>
   3.306 @@ -1226,11 +1213,11 @@
   3.307    }
   3.308    then show ?thesis
   3.309      unfolding arc_def inj_on_def
   3.310 -    by (simp add:  path_linepath) (force simp: algebra_simps linepath_def)
   3.311 +    by (fastforce simp: algebra_simps linepath_def)
   3.312  qed
   3.313  
   3.314  lemma simple_path_linepath[intro]: "a \<noteq> b \<Longrightarrow> simple_path (linepath a b)"
   3.315 -  by (simp add: arc_imp_simple_path arc_linepath)
   3.316 +  by (simp add: arc_imp_simple_path)
   3.317  
   3.318  lemma linepath_trivial [simp]: "linepath a a x = a"
   3.319    by (simp add: linepath_def real_vector.scale_left_diff_distrib)
   3.320 @@ -1275,10 +1262,7 @@
   3.321      shows "midpoint x y \<in> convex hull s"
   3.322  proof -
   3.323    have "(1 - inverse(2)) *\<^sub>R x + inverse(2) *\<^sub>R y \<in> convex hull s"
   3.324 -    apply (rule convexD_alt)
   3.325 -    using assms
   3.326 -    apply (auto simp: convex_convex_hull)
   3.327 -    done
   3.328 +    by (rule convexD_alt) (use assms in auto)
   3.329    then show ?thesis
   3.330      by (simp add: midpoint_def algebra_simps)
   3.331  qed
   3.332 @@ -1339,7 +1323,7 @@
   3.333      proof (intro exI conjI)
   3.334        have "closed_segment (x-\<delta>) (x+\<delta>) = {x-\<delta>..x+\<delta>}"
   3.335          using \<open>0 < \<delta>\<close> by (auto simp: closed_segment_eq_real_ivl)
   3.336 -      also have "... \<subseteq> S"
   3.337 +      also have "\<dots> \<subseteq> S"
   3.338          using \<delta> \<open>T \<subseteq> S\<close> by (auto simp: dist_norm subset_eq)
   3.339        finally have "f ` (open_segment (x-\<delta>) (x+\<delta>)) = open_segment (f (x-\<delta>)) (f (x+\<delta>))"
   3.340          using continuous_injective_image_open_segment_1
   3.341 @@ -1384,17 +1368,15 @@
   3.342  lemma not_on_path_ball:
   3.343    fixes g :: "real \<Rightarrow> 'a::heine_borel"
   3.344    assumes "path g"
   3.345 -    and "z \<notin> path_image g"
   3.346 +    and z: "z \<notin> path_image g"
   3.347    shows "\<exists>e > 0. ball z e \<inter> path_image g = {}"
   3.348  proof -
   3.349 -  obtain a where "a \<in> path_image g" "\<forall>y \<in> path_image g. dist z a \<le> dist z y"
   3.350 -    apply (rule distance_attains_inf[OF _ path_image_nonempty, of g z])
   3.351 -    using compact_path_image[THEN compact_imp_closed, OF assms(1)] by auto
   3.352 +  have "closed (path_image g)"
   3.353 +    by (simp add: \<open>path g\<close> closed_path_image)
   3.354 +  then obtain a where "a \<in> path_image g" "\<forall>y \<in> path_image g. dist z a \<le> dist z y"
   3.355 +    by (auto intro: distance_attains_inf[OF _ path_image_nonempty, of g z])
   3.356    then show ?thesis
   3.357 -    apply (rule_tac x="dist z a" in exI)
   3.358 -    using assms(2)
   3.359 -    apply (auto intro!: dist_pos_lt)
   3.360 -    done
   3.361 +    by (rule_tac x="dist z a" in exI) (use dist_commute z in auto)
   3.362  qed
   3.363  
   3.364  lemma not_on_path_cball:
   3.365 @@ -1408,9 +1390,7 @@
   3.366    moreover have "cball z (e/2) \<subseteq> ball z e"
   3.367      using \<open>e > 0\<close> by auto
   3.368    ultimately show ?thesis
   3.369 -    apply (rule_tac x="e/2" in exI)
   3.370 -    apply auto
   3.371 -    done
   3.372 +    by (rule_tac x="e/2" in exI) auto
   3.373  qed
   3.374  
   3.375  
   3.376 @@ -1446,8 +1426,7 @@
   3.377  lemma path_component_sym: "path_component s x y \<Longrightarrow> path_component s y x"
   3.378    unfolding path_component_def
   3.379    apply (erule exE)
   3.380 -  apply (rule_tac x="reversepath g" in exI)
   3.381 -  apply auto
   3.382 +  apply (rule_tac x="reversepath g" in exI, auto)
   3.383    done
   3.384  
   3.385  lemma path_component_trans:
   3.386 @@ -1457,7 +1436,7 @@
   3.387    unfolding path_component_def
   3.388    apply (elim exE)
   3.389    apply (rule_tac x="g +++ ga" in exI)
   3.390 -  apply (auto simp add: path_image_join)
   3.391 +  apply (auto simp: path_image_join)
   3.392    done
   3.393  
   3.394  lemma path_component_of_subset: "s \<subseteq> t \<Longrightarrow> path_component s x y \<Longrightarrow> path_component t x y"
   3.395 @@ -1466,9 +1445,8 @@
   3.396  lemma path_connected_linepath:
   3.397      fixes s :: "'a::real_normed_vector set"
   3.398      shows "closed_segment a b \<subseteq> s \<Longrightarrow> path_component s a b"
   3.399 -  apply (simp add: path_component_def)
   3.400 -  apply (rule_tac x="linepath a b" in exI, auto)
   3.401 -  done
   3.402 +  unfolding path_component_def
   3.403 +  by (rule_tac x="linepath a b" in exI, auto)
   3.404  
   3.405  
   3.406  subsubsection%unimportant \<open>Path components as sets\<close>
   3.407 @@ -1479,7 +1457,7 @@
   3.408    by (auto simp: path_component_def)
   3.409  
   3.410  lemma path_component_subset: "path_component_set s x \<subseteq> s"
   3.411 -  by (auto simp add: path_component_mem(2))
   3.412 +  by (auto simp: path_component_mem(2))
   3.413  
   3.414  lemma path_component_eq_empty: "path_component_set s x = {} \<longleftrightarrow> x \<notin> s"
   3.415    using path_component_mem path_component_refl_eq
   3.416 @@ -1578,31 +1556,23 @@
   3.417    unfolding open_contains_ball
   3.418  proof
   3.419    fix y
   3.420 -  assume as: "y \<in> S - path_component_set S x"
   3.421 +  assume y: "y \<in> S - path_component_set S x"
   3.422    then obtain e where e: "e > 0" "ball y e \<subseteq> S"
   3.423 -    using assms [unfolded open_contains_ball]
   3.424 -    by auto
   3.425 +    using assms openE by auto
   3.426    show "\<exists>e>0. ball y e \<subseteq> S - path_component_set S x"
   3.427 -    apply (rule_tac x=e in exI)
   3.428 -    apply rule
   3.429 -    apply (rule \<open>e>0\<close>)
   3.430 -    apply rule
   3.431 -    apply rule
   3.432 -    defer
   3.433 -  proof (rule ccontr)
   3.434 -    fix z
   3.435 -    assume "z \<in> ball y e" "\<not> z \<notin> path_component_set S x"
   3.436 -    then have "y \<in> path_component_set S x"
   3.437 -      unfolding not_not mem_Collect_eq using \<open>e>0\<close>
   3.438 -      apply -
   3.439 -      apply (rule path_component_trans, assumption)
   3.440 -      apply (rule path_component_of_subset[OF e(2)])
   3.441 -      apply (rule convex_imp_path_connected[OF convex_ball, unfolded path_connected_component, rule_format])
   3.442 -      apply auto
   3.443 -      done
   3.444 -    then show False
   3.445 -      using as by auto
   3.446 -  qed (insert e(2), auto)
   3.447 +  proof (intro exI conjI subsetI DiffI notI)
   3.448 +    show "\<And>x. x \<in> ball y e \<Longrightarrow> x \<in> S"
   3.449 +      using e by blast
   3.450 +    show False if "z \<in> ball y e" "z \<in> path_component_set S x" for z
   3.451 +    proof -
   3.452 +      have "y \<in> path_component_set S z"
   3.453 +        by (meson assms convex_ball convex_imp_path_connected e open_contains_ball_eq open_path_component path_component_maximal that(1))
   3.454 +      then have "y \<in> path_component_set S x"
   3.455 +        using path_component_eq that(2) by blast
   3.456 +      then show False
   3.457 +        using y by blast
   3.458 +    qed
   3.459 +  qed (use e in auto)
   3.460  qed
   3.461  
   3.462  lemma connected_open_path_connected:
   3.463 @@ -1676,7 +1646,7 @@
   3.464    by (simp add: convex_imp_path_connected)
   3.465  
   3.466  lemma homeomorphic_path_connectedness:
   3.467 -  "s homeomorphic t \<Longrightarrow> path_connected s \<longleftrightarrow> path_connected t"
   3.468 +  "S homeomorphic T \<Longrightarrow> path_connected S \<longleftrightarrow> path_connected T"
   3.469    unfolding homeomorphic_def homeomorphism_def by (metis path_connected_continuous_image)
   3.470  
   3.471  lemma path_connected_empty [simp]: "path_connected {}"
   3.472 @@ -1691,23 +1661,35 @@
   3.473    done
   3.474  
   3.475  lemma path_connected_Un:
   3.476 -  assumes "path_connected s"
   3.477 -    and "path_connected t"
   3.478 -    and "s \<inter> t \<noteq> {}"
   3.479 -  shows "path_connected (s \<union> t)"
   3.480 +  assumes "path_connected S"
   3.481 +    and "path_connected T"
   3.482 +    and "S \<inter> T \<noteq> {}"
   3.483 +  shows "path_connected (S \<union> T)"
   3.484    unfolding path_connected_component
   3.485 -proof (rule, rule)
   3.486 +proof (intro ballI)
   3.487    fix x y
   3.488 -  assume as: "x \<in> s \<union> t" "y \<in> s \<union> t"
   3.489 -  from assms(3) obtain z where "z \<in> s \<inter> t"
   3.490 +  assume x: "x \<in> S \<union> T" and y: "y \<in> S \<union> T"
   3.491 +  from assms obtain z where z: "z \<in> S" "z \<in> T"
   3.492      by auto
   3.493 -  then show "path_component (s \<union> t) x y"
   3.494 -    using as and assms(1-2)[unfolded path_connected_component]
   3.495 -    apply -
   3.496 -    apply (erule_tac[!] UnE)+
   3.497 -    apply (rule_tac[2-3] path_component_trans[of _ _ z])
   3.498 -    apply (auto simp add:path_component_of_subset [OF Un_upper1] path_component_of_subset[OF Un_upper2])
   3.499 -    done
   3.500 +  show "path_component (S \<union> T) x y"
   3.501 +    using x y
   3.502 +  proof safe
   3.503 +    assume "x \<in> S" "y \<in> S"
   3.504 +    then show "path_component (S \<union> T) x y"
   3.505 +      by (meson Un_upper1 \<open>path_connected S\<close> path_component_of_subset path_connected_component)
   3.506 +  next
   3.507 +    assume "x \<in> S" "y \<in> T"
   3.508 +    then show "path_component (S \<union> T) x y"
   3.509 +      by (metis z assms(1-2) le_sup_iff order_refl path_component_of_subset path_component_trans path_connected_component)
   3.510 +  next
   3.511 +  assume "x \<in> T" "y \<in> S"
   3.512 +    then show "path_component (S \<union> T) x y"
   3.513 +      by (metis z assms(1-2) le_sup_iff order_refl path_component_of_subset path_component_trans path_connected_component)
   3.514 +  next
   3.515 +    assume "x \<in> T" "y \<in> T"
   3.516 +    then show "path_component (S \<union> T) x y"
   3.517 +      by (metis Un_upper1 assms(2) path_component_of_subset path_connected_component sup_commute)
   3.518 +  qed
   3.519  qed
   3.520  
   3.521  lemma path_connected_UNION:
   3.522 @@ -1729,30 +1711,22 @@
   3.523  lemma path_component_path_image_pathstart:
   3.524    assumes p: "path p" and x: "x \<in> path_image p"
   3.525    shows "path_component (path_image p) (pathstart p) x"
   3.526 -using x
   3.527 -proof (clarsimp simp add: path_image_def)
   3.528 -  fix y
   3.529 -  assume "x = p y" and y: "0 \<le> y" "y \<le> 1"
   3.530 -  show "path_component (p ` {0..1}) (pathstart p) (p y)"
   3.531 -  proof (cases "y=0")
   3.532 -    case True then show ?thesis
   3.533 -      by (simp add: path_component_refl_eq pathstart_def)
   3.534 -  next
   3.535 -    case False have "continuous_on {0..1} (p o (( * ) y))"
   3.536 +proof -
   3.537 +  obtain y where x: "x = p y" and y: "0 \<le> y" "y \<le> 1"
   3.538 +    using x by (auto simp: path_image_def)
   3.539 +  show ?thesis
   3.540 +    unfolding path_component_def 
   3.541 +  proof (intro exI conjI)
   3.542 +    have "continuous_on {0..1} (p \<circ> (( *) y))"
   3.543        apply (rule continuous_intros)+
   3.544        using p [unfolded path_def] y
   3.545        apply (auto simp: mult_le_one intro: continuous_on_subset [of _ p])
   3.546        done
   3.547 -    then have "path (\<lambda>u. p (y * u))"
   3.548 +    then show "path (\<lambda>u. p (y * u))"
   3.549        by (simp add: path_def)
   3.550 -    then show ?thesis
   3.551 -      apply (simp add: path_component_def)
   3.552 -      apply (rule_tac x = "\<lambda>u. p (y * u)" in exI)
   3.553 -      apply (intro conjI)
   3.554 -      using y False
   3.555 -      apply (auto simp: mult_le_one pathstart_def pathfinish_def path_image_def)
   3.556 -      done
   3.557 -  qed
   3.558 +    show "path_image (\<lambda>u. p (y * u)) \<subseteq> path_image p"
   3.559 +      using y mult_le_one by (fastforce simp: path_image_def image_iff)
   3.560 +  qed (auto simp: pathstart_def pathfinish_def x)
   3.561  qed
   3.562  
   3.563  lemma path_connected_path_image: "path p \<Longrightarrow> path_connected(path_image p)"
   3.564 @@ -1860,7 +1834,7 @@
   3.565      by (metis hf gs path_join_imp pathstart_def pathfinish_def)
   3.566    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))"
   3.567      by (rule Path_Connected.path_image_join_subset)
   3.568 -  also have "... \<subseteq> (\<Union>x\<in>s. \<Union>x1\<in>t. {(x, x1)})"
   3.569 +  also have "\<dots> \<subseteq> (\<Union>x\<in>s. \<Union>x1\<in>t. {(x, x1)})"
   3.570      using g h \<open>x1 \<in> s\<close> \<open>y2 \<in> t\<close> by (force simp: path_image_def)
   3.571    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)})" .
   3.572    show "\<exists>g. path g \<and> path_image g \<subseteq> (\<Union>x\<in>s. \<Union>x1\<in>t. {(x, x1)}) \<and>
   3.573 @@ -2055,11 +2029,11 @@
   3.574        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)) =
   3.575              (1 + (u / (1 + C * u - u))) *\<^sub>R a + ((1 / (1 + C * u - u)) + (C * u / (1 + C * u - u))) *\<^sub>R x"
   3.576          by (simp add: algebra_simps)
   3.577 -      also have "... = (1 + (u / (1 + C * u - u))) *\<^sub>R a + (1 + (u / (1 + C * u - u))) *\<^sub>R x"
   3.578 +      also have "\<dots> = (1 + (u / (1 + C * u - u))) *\<^sub>R a + (1 + (u / (1 + C * u - u))) *\<^sub>R x"
   3.579          using CC by (simp add: field_simps)
   3.580 -      also have "... = x + (1 + (u / (1 + C * u - u))) *\<^sub>R a + (u / (1 + C * u - u)) *\<^sub>R x"
   3.581 +      also have "\<dots> = x + (1 + (u / (1 + C * u - u))) *\<^sub>R a + (u / (1 + C * u - u)) *\<^sub>R x"
   3.582          by (simp add: algebra_simps)
   3.583 -      also have "... = x + ((1 / (1 + C * u - u)) *\<^sub>R a +
   3.584 +      also have "\<dots> = x + ((1 / (1 + C * u - u)) *\<^sub>R a +
   3.585                ((u / (1 + C * u - u)) *\<^sub>R x + (C * u / (1 + C * u - u)) *\<^sub>R a))"
   3.586          using CC by (simp add: field_simps) (simp add: add_divide_distrib scaleR_add_left)
   3.587        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"
   3.588 @@ -2090,11 +2064,11 @@
   3.589        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)) =
   3.590              (1 + (u / (1 + D * u - u))) *\<^sub>R a + ((1 / (1 + D * u - u)) + (D * u / (1 + D * u - u))) *\<^sub>R y"
   3.591          by (simp add: algebra_simps)
   3.592 -      also have "... = (1 + (u / (1 + D * u - u))) *\<^sub>R a + (1 + (u / (1 + D * u - u))) *\<^sub>R y"
   3.593 +      also have "\<dots> = (1 + (u / (1 + D * u - u))) *\<^sub>R a + (1 + (u / (1 + D * u - u))) *\<^sub>R y"
   3.594          using DD by (simp add: field_simps)
   3.595 -      also have "... = y + (1 + (u / (1 + D * u - u))) *\<^sub>R a + (u / (1 + D * u - u)) *\<^sub>R y"
   3.596 +      also have "\<dots> = y + (1 + (u / (1 + D * u - u))) *\<^sub>R a + (u / (1 + D * u - u)) *\<^sub>R y"
   3.597          by (simp add: algebra_simps)
   3.598 -      also have "... = y + ((1 / (1 + D * u - u)) *\<^sub>R a +
   3.599 +      also have "\<dots> = y + ((1 / (1 + D * u - u)) *\<^sub>R a +
   3.600                ((u / (1 + D * u - u)) *\<^sub>R y + (D * u / (1 + D * u - u)) *\<^sub>R a))"
   3.601          using DD by (simp add: field_simps) (simp add: add_divide_distrib scaleR_add_left)
   3.602        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"
   3.603 @@ -2160,7 +2134,7 @@
   3.604      using \<epsilon> by (force intro: connected_diff_ball [OF \<open>connected S\<close> _ 2])
   3.605    have "x \<in> \<Union>{S - ball a r |r. 0 < r \<and> r < \<epsilon>}" if "x \<in> S - {a}" for x
   3.606      apply (rule UnionI [of "S - ball a (min \<epsilon> (dist a x) / 2)"])
   3.607 -     using that \<open>0 < \<epsilon>\<close> apply (simp_all add:)
   3.608 +     using that \<open>0 < \<epsilon>\<close> apply simp_all
   3.609      apply (rule_tac x="min \<epsilon> (dist a x) / 2" in exI)
   3.610      apply auto
   3.611      done
   3.612 @@ -2228,9 +2202,9 @@
   3.613        by (force simp: sphere_def dist_norm)
   3.614      have "dist (r *\<^sub>R b) (- r *\<^sub>R b) = norm (r *\<^sub>R b + r *\<^sub>R b)"
   3.615        by (simp add: dist_norm)
   3.616 -    also have "... = norm ((2*r) *\<^sub>R b)"
   3.617 +    also have "\<dots> = norm ((2*r) *\<^sub>R b)"
   3.618        by (metis mult_2 scaleR_add_left)
   3.619 -    also have "... = 2*r"
   3.620 +    also have "\<dots> = 2*r"
   3.621        using \<open>r > 0\<close> b norm_Basis by fastforce
   3.622      finally show "dist (r *\<^sub>R b) (- r *\<^sub>R b) = 2*r" .
   3.623    qed
   3.624 @@ -2258,7 +2232,7 @@
   3.625    obtain b where "dist a b = r" and "b \<notin> S"
   3.626      using S mem_sphere by blast
   3.627    have CS: "- S = {x. dist a x \<le> r \<and> (x \<notin> S)} \<union> {x. r \<le> dist a x \<and> (x \<notin> S)}"
   3.628 -    by (auto simp: )
   3.629 +    by auto
   3.630    have "{x. dist a x \<le> r \<and> x \<notin> S} \<inter> {x. r \<le> dist a x \<and> x \<notin> S} \<noteq> {}"
   3.631      using \<open>b \<notin> S\<close> \<open>dist a b = r\<close> by blast
   3.632    moreover have "connected {x. dist a x \<le> r \<and> x \<notin> S}"
   3.633 @@ -2451,7 +2425,7 @@
   3.634    obtain B where B: "B>0" "-s \<subseteq> ball 0 B"
   3.635      using bounded_subset_ballD [OF assms, of 0] by auto
   3.636    then have *: "\<And>x. B \<le> norm x \<Longrightarrow> x \<in> s"
   3.637 -    by (force simp add: ball_def dist_norm)
   3.638 +    by (force simp: ball_def dist_norm)
   3.639    have unbounded_inner: "~ bounded {x. inner i x \<ge> B}"
   3.640      apply (auto simp: bounded_def dist_norm)
   3.641      apply (rule_tac x="x + (max B e + 1 + \<bar>i \<bullet> x\<bar>) *\<^sub>R i" in exI)
   3.642 @@ -2486,7 +2460,7 @@
   3.643    obtain B where B: "B>0" "-s \<subseteq> ball 0 B"
   3.644      using bounded_subset_ballD [OF bs, of 0] by auto
   3.645    then have *: "\<And>x. B \<le> norm x \<Longrightarrow> x \<in> s"
   3.646 -    by (force simp add: ball_def dist_norm)
   3.647 +    by (force simp: ball_def dist_norm)
   3.648    have ccb: "connected (- ball 0 B :: 'a set)"
   3.649      using assms by (auto intro: connected_complement_bounded_convex)
   3.650    obtain x' where x': "connected_component s x x'" "norm x' > B"
   3.651 @@ -2531,47 +2505,47 @@
   3.652    The outside comprises the points in unbounded connected component of the complement.\<close>
   3.653  
   3.654  definition%important inside where
   3.655 -  "inside s \<equiv> {x. (x \<notin> s) \<and> bounded(connected_component_set ( - s) x)}"
   3.656 +  "inside S \<equiv> {x. (x \<notin> S) \<and> bounded(connected_component_set ( - S) x)}"
   3.657  
   3.658  definition%important outside where
   3.659 -  "outside s \<equiv> -s \<inter> {x. ~ bounded(connected_component_set (- s) x)}"
   3.660 -
   3.661 -lemma outside: "outside s = {x. ~ bounded(connected_component_set (- s) x)}"
   3.662 +  "outside S \<equiv> -S \<inter> {x. ~ bounded(connected_component_set (- S) x)}"
   3.663 +
   3.664 +lemma outside: "outside S = {x. ~ bounded(connected_component_set (- S) x)}"
   3.665    by (auto simp: outside_def) (metis Compl_iff bounded_empty connected_component_eq_empty)
   3.666  
   3.667 -lemma inside_no_overlap [simp]: "inside s \<inter> s = {}"
   3.668 +lemma inside_no_overlap [simp]: "inside S \<inter> S = {}"
   3.669    by (auto simp: inside_def)
   3.670  
   3.671  lemma outside_no_overlap [simp]:
   3.672 -   "outside s \<inter> s = {}"
   3.673 +   "outside S \<inter> S = {}"
   3.674    by (auto simp: outside_def)
   3.675  
   3.676 -lemma inside_Int_outside [simp]: "inside s \<inter> outside s = {}"
   3.677 +lemma inside_Int_outside [simp]: "inside S \<inter> outside S = {}"
   3.678    by (auto simp: inside_def outside_def)
   3.679  
   3.680 -lemma inside_Un_outside [simp]: "inside s \<union> outside s = (- s)"
   3.681 +lemma inside_Un_outside [simp]: "inside S \<union> outside S = (- S)"
   3.682    by (auto simp: inside_def outside_def)
   3.683  
   3.684  lemma inside_eq_outside:
   3.685 -   "inside s = outside s \<longleftrightarrow> s = UNIV"
   3.686 +   "inside S = outside S \<longleftrightarrow> S = UNIV"
   3.687    by (auto simp: inside_def outside_def)
   3.688  
   3.689 -lemma inside_outside: "inside s = (- (s \<union> outside s))"
   3.690 -  by (force simp add: inside_def outside)
   3.691 -
   3.692 -lemma outside_inside: "outside s = (- (s \<union> inside s))"
   3.693 +lemma inside_outside: "inside S = (- (S \<union> outside S))"
   3.694 +  by (force simp: inside_def outside)
   3.695 +
   3.696 +lemma outside_inside: "outside S = (- (S \<union> inside S))"
   3.697    by (auto simp: inside_outside) (metis IntI equals0D outside_no_overlap)
   3.698  
   3.699 -lemma union_with_inside: "s \<union> inside s = - outside s"
   3.700 +lemma union_with_inside: "S \<union> inside S = - outside S"
   3.701    by (auto simp: inside_outside) (simp add: outside_inside)
   3.702  
   3.703 -lemma union_with_outside: "s \<union> outside s = - inside s"
   3.704 +lemma union_with_outside: "S \<union> outside S = - inside S"
   3.705    by (simp add: inside_outside)
   3.706  
   3.707 -lemma outside_mono: "s \<subseteq> t \<Longrightarrow> outside t \<subseteq> outside s"
   3.708 +lemma outside_mono: "S \<subseteq> T \<Longrightarrow> outside T \<subseteq> outside S"
   3.709    by (auto simp: outside bounded_subset connected_component_mono)
   3.710  
   3.711 -lemma inside_mono: "s \<subseteq> t \<Longrightarrow> inside s - t \<subseteq> inside t"
   3.712 +lemma inside_mono: "S \<subseteq> T \<Longrightarrow> inside S - T \<subseteq> inside T"
   3.713    by (auto simp: inside_def bounded_subset connected_component_mono)
   3.714  
   3.715  lemma segment_bound_lemma:
   3.716 @@ -2586,80 +2560,81 @@
   3.717  qed
   3.718  
   3.719  lemma cobounded_outside:
   3.720 -  fixes s :: "'a :: real_normed_vector set"
   3.721 -  assumes "bounded s" shows "bounded (- outside s)"
   3.722 +  fixes S :: "'a :: real_normed_vector set"
   3.723 +  assumes "bounded S" shows "bounded (- outside S)"
   3.724  proof -
   3.725 -  obtain B where B: "B>0" "s \<subseteq> ball 0 B"
   3.726 +  obtain B where B: "B>0" "S \<subseteq> ball 0 B"
   3.727      using bounded_subset_ballD [OF assms, of 0] by auto
   3.728    { fix x::'a and C::real
   3.729      assume Bno: "B \<le> norm x" and C: "0 < C"
   3.730 -    have "\<exists>y. connected_component (- s) x y \<and> norm y > C"
   3.731 +    have "\<exists>y. connected_component (- S) x y \<and> norm y > C"
   3.732      proof (cases "x = 0")
   3.733        case True with B Bno show ?thesis by force
   3.734      next
   3.735 -      case False with B C show ?thesis
   3.736 -        apply (rule_tac x="((B+C)/norm x) *\<^sub>R x" in exI)
   3.737 -        apply (simp add: connected_component_def)
   3.738 -        apply (rule_tac x="closed_segment x (((B+C)/norm x) *\<^sub>R x)" in exI)
   3.739 -        apply simp
   3.740 -        apply (rule_tac y="- ball 0 B" in order_trans)
   3.741 -         prefer 2 apply force
   3.742 -        apply (simp add: closed_segment_def ball_def dist_norm, clarify)
   3.743 -        apply (simp add: real_vector_class.scaleR_add_left [symmetric] divide_simps)
   3.744 +      case False 
   3.745 +      with B C
   3.746 +      have "closed_segment x (((B + C) / norm x) *\<^sub>R x) \<subseteq> - ball 0 B"
   3.747 +        apply (clarsimp simp add: closed_segment_def ball_def dist_norm real_vector_class.scaleR_add_left [symmetric] divide_simps)
   3.748          using segment_bound_lemma [of B "norm x" "B+C" ] Bno
   3.749          by (meson le_add_same_cancel1 less_eq_real_def not_le)
   3.750 +      also have "... \<subseteq> -S"
   3.751 +        by (simp add: B)
   3.752 +      finally have "\<exists>T. connected T \<and> T \<subseteq> - S \<and> x \<in> T \<and> ((B + C) / norm x) *\<^sub>R x \<in> T"
   3.753 +        by (rule_tac x="closed_segment x (((B+C)/norm x) *\<^sub>R x)" in exI) simp
   3.754 +      with False B
   3.755 +      show ?thesis
   3.756 +        by (rule_tac x="((B+C)/norm x) *\<^sub>R x" in exI) (simp add: connected_component_def)
   3.757      qed
   3.758    }
   3.759    then show ?thesis
   3.760      apply (simp add: outside_def assms)
   3.761      apply (rule bounded_subset [OF bounded_ball [of 0 B]])
   3.762 -    apply (force simp add: dist_norm not_less bounded_pos)
   3.763 +    apply (force simp: dist_norm not_less bounded_pos)
   3.764      done
   3.765  qed
   3.766  
   3.767  lemma unbounded_outside:
   3.768 -    fixes s :: "'a::{real_normed_vector, perfect_space} set"
   3.769 -    shows "bounded s \<Longrightarrow> ~ bounded(outside s)"
   3.770 +    fixes S :: "'a::{real_normed_vector, perfect_space} set"
   3.771 +    shows "bounded S \<Longrightarrow> ~ bounded(outside S)"
   3.772    using cobounded_imp_unbounded cobounded_outside by blast
   3.773  
   3.774  lemma bounded_inside:
   3.775 -    fixes s :: "'a::{real_normed_vector, perfect_space} set"
   3.776 -    shows "bounded s \<Longrightarrow> bounded(inside s)"
   3.777 +    fixes S :: "'a::{real_normed_vector, perfect_space} set"
   3.778 +    shows "bounded S \<Longrightarrow> bounded(inside S)"
   3.779    by (simp add: bounded_Int cobounded_outside inside_outside)
   3.780  
   3.781  lemma connected_outside:
   3.782 -    fixes s :: "'a::euclidean_space set"
   3.783 -    assumes "bounded s" "2 \<le> DIM('a)"
   3.784 -      shows "connected(outside s)"
   3.785 -  apply (simp add: connected_iff_connected_component, clarify)
   3.786 -  apply (simp add: outside)
   3.787 -  apply (rule_tac s="connected_component_set (- s) x" in connected_component_of_subset)
   3.788 +    fixes S :: "'a::euclidean_space set"
   3.789 +    assumes "bounded S" "2 \<le> DIM('a)"
   3.790 +      shows "connected(outside S)"
   3.791 +  apply (clarsimp simp add: connected_iff_connected_component outside)
   3.792 +  apply (rule_tac s="connected_component_set (- S) x" in connected_component_of_subset)
   3.793    apply (metis (no_types) assms cobounded_unbounded_component cobounded_unique_unbounded_component connected_component_eq_eq connected_component_idemp double_complement mem_Collect_eq)
   3.794    apply clarify
   3.795    apply (metis connected_component_eq_eq connected_component_in)
   3.796    done
   3.797  
   3.798  lemma outside_connected_component_lt:
   3.799 -    "outside s = {x. \<forall>B. \<exists>y. B < norm(y) \<and> connected_component (- s) x y}"
   3.800 +    "outside S = {x. \<forall>B. \<exists>y. B < norm(y) \<and> connected_component (- S) x y}"
   3.801  apply (auto simp: outside bounded_def dist_norm)
   3.802  apply (metis diff_0 norm_minus_cancel not_less)
   3.803  by (metis less_diff_eq norm_minus_commute norm_triangle_ineq2 order.trans pinf(6))
   3.804  
   3.805  lemma outside_connected_component_le:
   3.806 -   "outside s =
   3.807 +   "outside S =
   3.808              {x. \<forall>B. \<exists>y. B \<le> norm(y) \<and>
   3.809 -                         connected_component (- s) x y}"
   3.810 +                         connected_component (- S) x y}"
   3.811  apply (simp add: outside_connected_component_lt)
   3.812  apply (simp add: Set.set_eq_iff)
   3.813  by (meson gt_ex leD le_less_linear less_imp_le order.trans)
   3.814  
   3.815  lemma not_outside_connected_component_lt:
   3.816 -    fixes s :: "'a::euclidean_space set"
   3.817 -    assumes s: "bounded s" and "2 \<le> DIM('a)"
   3.818 -      shows "- (outside s) = {x. \<forall>B. \<exists>y. B < norm(y) \<and> ~ (connected_component (- s) x y)}"
   3.819 +    fixes S :: "'a::euclidean_space set"
   3.820 +    assumes S: "bounded S" and "2 \<le> DIM('a)"
   3.821 +      shows "- (outside S) = {x. \<forall>B. \<exists>y. B < norm(y) \<and> ~ (connected_component (- S) x y)}"
   3.822  proof -
   3.823 -  obtain B::real where B: "0 < B" and Bno: "\<And>x. x \<in> s \<Longrightarrow> norm x \<le> B"
   3.824 -    using s [simplified bounded_pos] by auto
   3.825 +  obtain B::real where B: "0 < B" and Bno: "\<And>x. x \<in> S \<Longrightarrow> norm x \<le> B"
   3.826 +    using S [simplified bounded_pos] by auto
   3.827    { fix y::'a and z::'a
   3.828      assume yz: "B < norm z" "B < norm y"
   3.829      have "connected_component (- cball 0 B) y z"
   3.830 @@ -2667,7 +2642,7 @@
   3.831        apply (rule connected_complement_bounded_convex)
   3.832        using assms yz
   3.833        by (auto simp: dist_norm)
   3.834 -    then have "connected_component (- s) y z"
   3.835 +    then have "connected_component (- S) y z"
   3.836        apply (rule connected_component_of_subset)
   3.837        apply (metis Bno Compl_anti_mono mem_cball_0 subset_iff)
   3.838        done
   3.839 @@ -2680,29 +2655,29 @@
   3.840  qed
   3.841  
   3.842  lemma not_outside_connected_component_le:
   3.843 -    fixes s :: "'a::euclidean_space set"
   3.844 -    assumes s: "bounded s"  "2 \<le> DIM('a)"
   3.845 -      shows "- (outside s) = {x. \<forall>B. \<exists>y. B \<le> norm(y) \<and> ~ (connected_component (- s) x y)}"
   3.846 +    fixes S :: "'a::euclidean_space set"
   3.847 +    assumes S: "bounded S"  "2 \<le> DIM('a)"
   3.848 +      shows "- (outside S) = {x. \<forall>B. \<exists>y. B \<le> norm(y) \<and> ~ (connected_component (- S) x y)}"
   3.849  apply (auto intro: less_imp_le simp: not_outside_connected_component_lt [OF assms])
   3.850  by (meson gt_ex less_le_trans)
   3.851  
   3.852  lemma inside_connected_component_lt:
   3.853 -    fixes s :: "'a::euclidean_space set"
   3.854 -    assumes s: "bounded s"  "2 \<le> DIM('a)"
   3.855 -      shows "inside s = {x. (x \<notin> s) \<and> (\<forall>B. \<exists>y. B < norm(y) \<and> ~(connected_component (- s) x y))}"
   3.856 +    fixes S :: "'a::euclidean_space set"
   3.857 +    assumes S: "bounded S"  "2 \<le> DIM('a)"
   3.858 +      shows "inside S = {x. (x \<notin> S) \<and> (\<forall>B. \<exists>y. B < norm(y) \<and> ~(connected_component (- S) x y))}"
   3.859    by (auto simp: inside_outside not_outside_connected_component_lt [OF assms])
   3.860  
   3.861  lemma inside_connected_component_le:
   3.862 -    fixes s :: "'a::euclidean_space set"
   3.863 -    assumes s: "bounded s"  "2 \<le> DIM('a)"
   3.864 -      shows "inside s = {x. (x \<notin> s) \<and> (\<forall>B. \<exists>y. B \<le> norm(y) \<and> ~(connected_component (- s) x y))}"
   3.865 +    fixes S :: "'a::euclidean_space set"
   3.866 +    assumes S: "bounded S"  "2 \<le> DIM('a)"
   3.867 +      shows "inside S = {x. (x \<notin> S) \<and> (\<forall>B. \<exists>y. B \<le> norm(y) \<and> ~(connected_component (- S) x y))}"
   3.868    by (auto simp: inside_outside not_outside_connected_component_le [OF assms])
   3.869  
   3.870  lemma inside_subset:
   3.871 -  assumes "connected u" and "~bounded u" and "t \<union> u = - s"
   3.872 -  shows "inside s \<subseteq> t"
   3.873 +  assumes "connected U" and "~bounded U" and "T \<union> U = - S"
   3.874 +  shows "inside S \<subseteq> T"
   3.875  apply (auto simp: inside_def)
   3.876 -by (metis bounded_subset [of "connected_component_set (- s) _"] connected_component_maximal
   3.877 +by (metis bounded_subset [of "connected_component_set (- S) _"] connected_component_maximal
   3.878         Compl_iff Un_iff assms subsetI)
   3.879  
   3.880  lemma frontier_not_empty:
   3.881 @@ -2959,7 +2934,7 @@
   3.882    proof -
   3.883      have "Y \<subseteq> connected_component_set (- (T \<union> U)) x"
   3.884        by (simp add: connected_component_maximal that)
   3.885 -    also have "... \<subseteq> outside(T \<union> U)"
   3.886 +    also have "\<dots> \<subseteq> outside(T \<union> U)"
   3.887        by (metis (mono_tags, lifting) Collect_mono mem_Collect_eq outside outside_same_component x)
   3.888      finally have "Y \<subseteq> outside(T \<union> U)" .
   3.889      with assms show ?thesis by auto
   3.890 @@ -2996,7 +2971,7 @@
   3.891       shows "\<lbrakk>bounded s; convex s\<rbrakk> \<Longrightarrow> inside(frontier s) = interior s"
   3.892    apply (simp add: inside_outside outside_frontier_eq_complement_closure)
   3.893    using closure_subset interior_subset
   3.894 -  apply (auto simp add: frontier_def)
   3.895 +  apply (auto simp: frontier_def)
   3.896    done
   3.897  
   3.898  lemma open_inside:
   3.899 @@ -3234,8 +3209,7 @@
   3.900    using that proof
   3.901      assume "a \<in> s" then show ?thesis
   3.902        apply (rule_tac x=a in exI)
   3.903 -      apply (rule_tac x="{a}" in exI)
   3.904 -      apply (simp add:)
   3.905 +      apply (rule_tac x="{a}" in exI, simp)
   3.906        done
   3.907    next
   3.908      assume a: "a \<in> inside s"
   3.909 @@ -3273,8 +3247,7 @@
   3.910    using that proof
   3.911      assume "a \<in> s" then show ?thesis
   3.912        apply (rule_tac x=a in exI)
   3.913 -      apply (rule_tac x="{a}" in exI)
   3.914 -      apply (simp add:)
   3.915 +      apply (rule_tac x="{a}" in exI, simp)
   3.916        done
   3.917    next
   3.918      assume a: "a \<in> outside s"
   3.919 @@ -3358,7 +3331,7 @@
   3.920        done
   3.921      then have ftendsw: "((\<lambda>n. f (z n)) \<circ> K) \<longlonglongrightarrow> w"
   3.922        by (metis LIMSEQ_subseq_LIMSEQ fun.map_cong0 fz tendsw)
   3.923 -    have zKs: "\<And>n. (z o K) n \<in> S" by (simp add: zs)
   3.924 +    have zKs: "\<And>n. (z \<circ> K) n \<in> S" by (simp add: zs)
   3.925      have fz: "f \<circ> z = \<xi>"  "(\<lambda>n. f (z n)) = \<xi>"
   3.926        using fz by auto
   3.927      then have "(\<xi> \<circ> K) \<longlonglongrightarrow> f y"
   3.928 @@ -3411,7 +3384,7 @@
   3.929    unfolding homotopic_with_def
   3.930    apply (rule iffI, blast, clarify)
   3.931    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)
   3.932 -  apply (auto simp:)
   3.933 +  apply auto
   3.934    apply (force elim: continuous_on_eq)
   3.935    apply (drule_tac x=t in bspec, force)
   3.936    apply (subst assms; simp)
   3.937 @@ -3427,8 +3400,7 @@
   3.938    apply safe
   3.939    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)
   3.940    apply (simp add: f' g', safe)
   3.941 -  apply (fastforce intro: continuous_on_eq)
   3.942 -  apply fastforce
   3.943 +  apply (fastforce intro: continuous_on_eq, fastforce)
   3.944    apply (subst P; fastforce)
   3.945    done
   3.946  
   3.947 @@ -3441,7 +3413,7 @@
   3.948    apply (rule_tac x="\<lambda>(u,v). if u = 1 then g v else f v" in exI)
   3.949    using assms
   3.950    apply (intro conjI)
   3.951 -  apply (rule continuous_on_eq [where f = "f o snd"])
   3.952 +  apply (rule continuous_on_eq [where f = "f \<circ> snd"])
   3.953    apply (rule continuous_intros | force)+
   3.954    apply clarify
   3.955    apply (case_tac "t=1"; force)
   3.956 @@ -3449,7 +3421,7 @@
   3.957  
   3.958  
   3.959  lemma image_Pair_const: "(\<lambda>x. (x, c)) ` A = A \<times> {c}"
   3.960 -  by (auto simp:)
   3.961 +  by auto
   3.962  
   3.963  lemma homotopic_constant_maps:
   3.964     "homotopic_with (\<lambda>x. True) s t (\<lambda>x. a) (\<lambda>x. b) \<longleftrightarrow> s = {} \<or> path_component t a b"
   3.965 @@ -3468,19 +3440,18 @@
   3.966        by (auto simp: homotopic_with)
   3.967      have "continuous_on {0..1} (h \<circ> (\<lambda>t. (t, c)))"
   3.968        apply (rule continuous_intros conth | simp add: image_Pair_const)+
   3.969 -      apply (blast intro:  \<open>c \<in> s\<close> continuous_on_subset [OF conth] )
   3.970 +      apply (blast intro:  \<open>c \<in> s\<close> continuous_on_subset [OF conth])
   3.971        done
   3.972      with \<open>c \<in> s\<close> h show "s = {} \<or> path_component t a b"
   3.973 -      apply (simp_all add: homotopic_with path_component_def)
   3.974 -      apply (auto simp:)
   3.975 -      apply (drule_tac x="h o (\<lambda>t. (t, c))" in spec)
   3.976 +      apply (simp_all add: homotopic_with path_component_def, auto)
   3.977 +      apply (drule_tac x="h \<circ> (\<lambda>t. (t, c))" in spec)
   3.978        apply (auto simp: pathstart_def pathfinish_def path_image_def path_def)
   3.979        done
   3.980    next
   3.981      assume "s = {} \<or> path_component t a b"
   3.982      with False show "homotopic_with (\<lambda>x. True) s t (\<lambda>x. a) (\<lambda>x. b)"
   3.983        apply (clarsimp simp: homotopic_with path_component_def pathstart_def pathfinish_def path_image_def path_def)
   3.984 -      apply (rule_tac x="g o fst" in exI)
   3.985 +      apply (rule_tac x="g \<circ> fst" in exI)
   3.986        apply (rule conjI continuous_intros | force)+
   3.987        done
   3.988    qed
   3.989 @@ -3493,11 +3464,10 @@
   3.990    unfolding homotopic_with_def Ball_def
   3.991    apply clarify
   3.992    apply (frule_tac x=0 in spec)
   3.993 -  apply (drule_tac x=1 in spec)
   3.994 -  apply (auto simp:)
   3.995 +  apply (drule_tac x=1 in spec, auto)
   3.996    done
   3.997  
   3.998 -lemma continuous_on_o_Pair: "\<lbrakk>continuous_on (T \<times> X) h; t \<in> T\<rbrakk> \<Longrightarrow> continuous_on X (h o Pair t)"
   3.999 +lemma continuous_on_o_Pair: "\<lbrakk>continuous_on (T \<times> X) h; t \<in> T\<rbrakk> \<Longrightarrow> continuous_on X (h \<circ> Pair t)"
  3.1000    by (fast intro: continuous_intros elim!: continuous_on_subset)
  3.1001  
  3.1002  lemma homotopic_with_imp_continuous:
  3.1003 @@ -3508,7 +3478,7 @@
  3.1004      where conth: "continuous_on ({0..1} \<times> X) h"
  3.1005        and h: "\<forall>x. h (0, x) = f x" "\<forall>x. h (1, x) = g x"
  3.1006      using assms by (auto simp: homotopic_with_def)
  3.1007 -  have *: "t \<in> {0..1} \<Longrightarrow> continuous_on X (h o (\<lambda>x. (t,x)))" for t
  3.1008 +  have *: "t \<in> {0..1} \<Longrightarrow> continuous_on X (h \<circ> (\<lambda>x. (t,x)))" for t
  3.1009      by (rule continuous_intros continuous_on_subset [OF conth] | force)+
  3.1010    show ?thesis
  3.1011      using h *[of 0] *[of 1] by auto
  3.1012 @@ -3546,10 +3516,10 @@
  3.1013  
  3.1014  proposition homotopic_with_compose_continuous_right:
  3.1015      "\<lbrakk>homotopic_with (\<lambda>f. p (f \<circ> h)) X Y f g; continuous_on W h; h ` W \<subseteq> X\<rbrakk>
  3.1016 -     \<Longrightarrow> homotopic_with p W Y (f o h) (g o h)"
  3.1017 +     \<Longrightarrow> homotopic_with p W Y (f \<circ> h) (g \<circ> h)"
  3.1018    apply (clarsimp simp add: homotopic_with_def)
  3.1019    apply (rename_tac k)
  3.1020 -  apply (rule_tac x="k o (\<lambda>y. (fst y, h (snd y)))" in exI)
  3.1021 +  apply (rule_tac x="k \<circ> (\<lambda>y. (fst y, h (snd y)))" in exI)
  3.1022    apply (rule conjI continuous_intros continuous_on_compose [where f=snd and g=h, unfolded o_def] | simp)+
  3.1023    apply (erule continuous_on_subset)
  3.1024    apply (fastforce simp: o_def)+
  3.1025 @@ -3557,15 +3527,15 @@
  3.1026  
  3.1027  proposition homotopic_compose_continuous_right:
  3.1028       "\<lbrakk>homotopic_with (\<lambda>f. True) X Y f g; continuous_on W h; h ` W \<subseteq> X\<rbrakk>
  3.1029 -      \<Longrightarrow> homotopic_with (\<lambda>f. True) W Y (f o h) (g o h)"
  3.1030 +      \<Longrightarrow> homotopic_with (\<lambda>f. True) W Y (f \<circ> h) (g \<circ> h)"
  3.1031    using homotopic_with_compose_continuous_right by fastforce
  3.1032  
  3.1033  proposition homotopic_with_compose_continuous_left:
  3.1034       "\<lbrakk>homotopic_with (\<lambda>f. p (h \<circ> f)) X Y f g; continuous_on Y h; h ` Y \<subseteq> Z\<rbrakk>
  3.1035 -      \<Longrightarrow> homotopic_with p X Z (h o f) (h o g)"
  3.1036 +      \<Longrightarrow> homotopic_with p X Z (h \<circ> f) (h \<circ> g)"
  3.1037    apply (clarsimp simp add: homotopic_with_def)
  3.1038    apply (rename_tac k)
  3.1039 -  apply (rule_tac x="h o k" in exI)
  3.1040 +  apply (rule_tac x="h \<circ> k" in exI)
  3.1041    apply (rule conjI continuous_intros continuous_on_compose [where f=snd and g=h, unfolded o_def] | simp)+
  3.1042    apply (erule continuous_on_subset)
  3.1043    apply (fastforce simp: o_def)+
  3.1044 @@ -3574,7 +3544,7 @@
  3.1045  proposition homotopic_compose_continuous_left:
  3.1046     "\<lbrakk>homotopic_with (\<lambda>_. True) X Y f g;
  3.1047       continuous_on Y h; h ` Y \<subseteq> Z\<rbrakk>
  3.1048 -    \<Longrightarrow> homotopic_with (\<lambda>f. True) X Z (h o f) (h o g)"
  3.1049 +    \<Longrightarrow> homotopic_with (\<lambda>f. True) X Z (h \<circ> f) (h \<circ> g)"
  3.1050    using homotopic_with_compose_continuous_left by fastforce
  3.1051  
  3.1052  proposition homotopic_with_Pair:
  3.1053 @@ -3585,7 +3555,7 @@
  3.1054    using hom
  3.1055    apply (clarsimp simp add: homotopic_with_def)
  3.1056    apply (rename_tac k k')
  3.1057 -  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)
  3.1058 +  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)
  3.1059    apply (rule conjI continuous_intros | erule continuous_on_subset | clarsimp)+
  3.1060    apply (auto intro!: q [unfolded case_prod_unfold])
  3.1061    done
  3.1062 @@ -3603,7 +3573,7 @@
  3.1063    apply (rule iffI)
  3.1064    using homotopic_with_imp_continuous homotopic_with_imp_property homotopic_with_imp_subset2 apply blast
  3.1065    apply (simp add: homotopic_with_def)
  3.1066 -  apply (rule_tac x="f o snd" in exI)
  3.1067 +  apply (rule_tac x="f \<circ> snd" in exI)
  3.1068    apply (rule conjI continuous_intros | force)+
  3.1069    done
  3.1070  
  3.1071 @@ -3614,8 +3584,8 @@
  3.1072    using assms
  3.1073    apply (clarsimp simp add: homotopic_with_def)
  3.1074    apply (rename_tac h)
  3.1075 -  apply (rule_tac x="h o (\<lambda>y. (1 - fst y, snd y))" in exI)
  3.1076 -  apply (rule conjI continuous_intros | erule continuous_on_subset | force simp add: image_subset_iff)+
  3.1077 +  apply (rule_tac x="h \<circ> (\<lambda>y. (1 - fst y, snd y))" in exI)
  3.1078 +  apply (rule conjI continuous_intros | erule continuous_on_subset | force simp: image_subset_iff)+
  3.1079    done
  3.1080  
  3.1081  proposition homotopic_with_sym:
  3.1082 @@ -3637,12 +3607,12 @@
  3.1083    have clo1: "closedin (subtopology euclidean ({0..1/2} \<times> X \<union> {1/2..1} \<times> X)) ({0..1/2::real} \<times> X)"
  3.1084      apply (simp add: closedin_closed split_01_prod [symmetric])
  3.1085      apply (rule_tac x="{0..1/2} \<times> UNIV" in exI)
  3.1086 -    apply (force simp add: closed_Times)
  3.1087 +    apply (force simp: closed_Times)
  3.1088      done
  3.1089    have clo2: "closedin (subtopology euclidean ({0..1/2} \<times> X \<union> {1/2..1} \<times> X)) ({1/2..1::real} \<times> X)"
  3.1090      apply (simp add: closedin_closed split_01_prod [symmetric])
  3.1091      apply (rule_tac x="{1/2..1} \<times> UNIV" in exI)
  3.1092 -    apply (force simp add: closed_Times)
  3.1093 +    apply (force simp: closed_Times)
  3.1094      done
  3.1095    { fix k1 k2:: "real \<times> 'a \<Rightarrow> 'b"
  3.1096      assume cont: "continuous_on ({0..1} \<times> X) k1" "continuous_on ({0..1} \<times> X) k2"
  3.1097 @@ -3652,18 +3622,18 @@
  3.1098         and P:   "\<forall>t\<in>{0..1}. P (\<lambda>x. k1 (t, x))" "\<forall>t\<in>{0..1}. P (\<lambda>x. k2 (t, x))"
  3.1099      define k where "k y =
  3.1100        (if fst y \<le> 1 / 2
  3.1101 -       then (k1 o (\<lambda>x. (2 *\<^sub>R fst x, snd x))) y
  3.1102 -       else (k2 o (\<lambda>x. (2 *\<^sub>R fst x -1, snd x))) y)" for y
  3.1103 +       then (k1 \<circ> (\<lambda>x. (2 *\<^sub>R fst x, snd x))) y
  3.1104 +       else (k2 \<circ> (\<lambda>x. (2 *\<^sub>R fst x -1, snd x))) y)" for y
  3.1105      have keq: "k1 (2 * u, v) = k2 (2 * u - 1, v)" if "u = 1/2"  for u v
  3.1106        by (simp add: geq that)
  3.1107      have "continuous_on ({0..1} \<times> X) k"
  3.1108        using cont
  3.1109        apply (simp add: split_01_prod k_def)
  3.1110        apply (rule clo1 clo2 continuous_on_cases_local continuous_intros | erule continuous_on_subset | simp add: linear image_subset_iff)+
  3.1111 -      apply (force simp add: keq)
  3.1112 +      apply (force simp: keq)
  3.1113        done
  3.1114      moreover have "k ` ({0..1} \<times> X) \<subseteq> Y"
  3.1115 -      using Y by (force simp add: k_def)
  3.1116 +      using Y by (force simp: k_def)
  3.1117      moreover have "\<forall>x. k (0, x) = f x"
  3.1118        by (simp add: k_def k12)
  3.1119      moreover have "(\<forall>x. k (1, x) = h x)"
  3.1120 @@ -3671,8 +3641,7 @@
  3.1121      moreover have "\<forall>t\<in>{0..1}. P (\<lambda>x. k (t, x))"
  3.1122        using P
  3.1123        apply (clarsimp simp add: k_def)
  3.1124 -      apply (case_tac "t \<le> 1/2")
  3.1125 -      apply (auto simp:)
  3.1126 +      apply (case_tac "t \<le> 1/2", auto)
  3.1127        done
  3.1128      ultimately have *: "\<exists>k :: real \<times> 'a \<Rightarrow> 'b.
  3.1129                         continuous_on ({0..1} \<times> X) k \<and> k ` ({0..1} \<times> X) \<subseteq> Y \<and>
  3.1130 @@ -3686,8 +3655,8 @@
  3.1131  proposition homotopic_compose:
  3.1132        fixes s :: "'a::real_normed_vector set"
  3.1133        shows "\<lbrakk>homotopic_with (\<lambda>x. True) s t f f'; homotopic_with (\<lambda>x. True) t u g g'\<rbrakk>
  3.1134 -             \<Longrightarrow> homotopic_with (\<lambda>x. True) s u (g o f) (g' o f')"
  3.1135 -  apply (rule homotopic_with_trans [where g = "g o f'"])
  3.1136 +             \<Longrightarrow> homotopic_with (\<lambda>x. True) s u (g \<circ> f) (g' \<circ> f')"
  3.1137 +  apply (rule homotopic_with_trans [where g = "g \<circ> f'"])
  3.1138    apply (metis homotopic_compose_continuous_left homotopic_with_imp_continuous homotopic_with_imp_subset1)
  3.1139    by (metis homotopic_compose_continuous_right homotopic_with_imp_continuous homotopic_with_imp_subset2)
  3.1140  
  3.1141 @@ -3756,8 +3725,8 @@
  3.1142            h ` ({0..1} \<times> {0..1}) \<subseteq> s \<and>
  3.1143            (\<forall>x \<in> {0..1}. h(0,x) = p x) \<and>
  3.1144            (\<forall>x \<in> {0..1}. h(1,x) = q x) \<and>
  3.1145 -          (\<forall>t \<in> {0..1::real}. pathstart(h o Pair t) = pathstart p \<and>
  3.1146 -                        pathfinish(h o Pair t) = pathfinish p))"
  3.1147 +          (\<forall>t \<in> {0..1::real}. pathstart(h \<circ> Pair t) = pathstart p \<and>
  3.1148 +                        pathfinish(h \<circ> Pair t) = pathfinish p))"
  3.1149    by (auto simp: homotopic_paths_def homotopic_with pathstart_def pathfinish_def)
  3.1150  
  3.1151  proposition homotopic_paths_imp_pathstart:
  3.1152 @@ -3809,7 +3778,7 @@
  3.1153  proof -
  3.1154    have contp: "continuous_on {0..1} p"
  3.1155      by (metis \<open>path p\<close> path_def)
  3.1156 -  then have "continuous_on {0..1} (p o f)"
  3.1157 +  then have "continuous_on {0..1} (p \<circ> f)"
  3.1158      using contf continuous_on_compose continuous_on_subset f01 by blast
  3.1159    then have "path q"
  3.1160      by (simp add: path_def) (metis q continuous_on_cong)
  3.1161 @@ -3826,7 +3795,7 @@
  3.1162    next
  3.1163      show "homotopic_paths s (p \<circ> f) p"
  3.1164        apply (simp add: homotopic_paths_def homotopic_with_def)
  3.1165 -      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)
  3.1166 +      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)
  3.1167        apply (rule conjI contf continuous_intros continuous_on_subset [OF contp] | simp)+
  3.1168        using pips [unfolded path_image_def]
  3.1169        apply (auto simp: fb0 fb1 pathstart_def pathfinish_def)
  3.1170 @@ -3848,10 +3817,10 @@
  3.1171        and pf: "\<And>t. t \<in> {0..1} \<Longrightarrow> pathfinish(p t) = pathstart(q t)"
  3.1172      shows "continuous_on ({0..1} \<times> {0..1}) (\<lambda>y. (p(fst y) +++ q(fst y)) (snd y))"
  3.1173  proof -
  3.1174 -  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))"
  3.1175 -    by (rule ext) (simp )
  3.1176 -  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))"
  3.1177 -    by (rule ext) (simp )
  3.1178 +  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))"
  3.1179 +    by (rule ext) (simp)
  3.1180 +  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))"
  3.1181 +    by (rule ext) (simp)
  3.1182    show ?thesis
  3.1183      apply (simp add: joinpaths_def)
  3.1184      apply (rule continuous_on_cases_le)
  3.1185 @@ -3869,7 +3838,7 @@
  3.1186        shows   "homotopic_paths s (reversepath p) (reversepath q)"
  3.1187    using assms
  3.1188    apply (simp add: homotopic_paths_def homotopic_with_def, clarify)
  3.1189 -  apply (rule_tac x="h o (\<lambda>x. (fst x, 1 - snd x))" in exI)
  3.1190 +  apply (rule_tac x="h \<circ> (\<lambda>x. (fst x, 1 - snd x))" in exI)
  3.1191    apply (rule conjI continuous_intros)+
  3.1192    apply (auto simp: reversepath_def pathstart_def pathfinish_def elim!: continuous_on_subset)
  3.1193    done
  3.1194 @@ -3883,13 +3852,13 @@
  3.1195      "\<lbrakk>homotopic_paths s p p'; homotopic_paths s q q'; pathfinish p = pathstart q\<rbrakk> \<Longrightarrow> homotopic_paths s (p +++ q) (p' +++ q')"
  3.1196    apply (simp add: homotopic_paths_def homotopic_with_def, clarify)
  3.1197    apply (rename_tac k1 k2)
  3.1198 -  apply (rule_tac x="(\<lambda>y. ((k1 o Pair (fst y)) +++ (k2 o Pair (fst y))) (snd y))" in exI)
  3.1199 +  apply (rule_tac x="(\<lambda>y. ((k1 \<circ> Pair (fst y)) +++ (k2 \<circ> Pair (fst y))) (snd y))" in exI)
  3.1200    apply (rule conjI continuous_intros homotopic_join_lemma)+
  3.1201    apply (auto simp: joinpaths_def pathstart_def pathfinish_def path_image_def)
  3.1202    done
  3.1203  
  3.1204  proposition homotopic_paths_continuous_image:
  3.1205 -    "\<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)"
  3.1206 +    "\<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)"
  3.1207    unfolding homotopic_paths_def
  3.1208    apply (rule homotopic_with_compose_continuous_left [of _ _ _ s])
  3.1209    apply (auto simp: pathstart_def pathfinish_def elim!: homotopic_with_mono)
  3.1210 @@ -3970,7 +3939,7 @@
  3.1211            image h ({0..1} \<times> {0..1}) \<subseteq> s \<and>
  3.1212            (\<forall>x \<in> {0..1}. h(0,x) = p x) \<and>
  3.1213            (\<forall>x \<in> {0..1}. h(1,x) = q x) \<and>
  3.1214 -          (\<forall>t \<in> {0..1}. pathfinish(h o Pair t) = pathstart(h o Pair t)))"
  3.1215 +          (\<forall>t \<in> {0..1}. pathfinish(h \<circ> Pair t) = pathstart(h \<circ> Pair t)))"
  3.1216    by (simp add: homotopic_loops_def pathstart_def pathfinish_def homotopic_with)
  3.1217  
  3.1218  proposition homotopic_loops_imp_loop:
  3.1219 @@ -4221,7 +4190,7 @@
  3.1220    using assms
  3.1221    unfolding path_def
  3.1222    apply (simp add: closed_segment_def pathstart_def pathfinish_def homotopic_paths_def homotopic_with_def)
  3.1223 -  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)
  3.1224 +  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)
  3.1225    apply (intro conjI subsetI continuous_intros; force)
  3.1226    done
  3.1227  
  3.1228 @@ -4335,8 +4304,7 @@
  3.1229    have "homotopic_paths s (subpath u w g +++ subpath w v g) ((subpath u v g +++ subpath v w g) +++ subpath w v g)"
  3.1230      apply (rule homotopic_paths_join)
  3.1231      using hom homotopic_paths_sym_eq apply blast
  3.1232 -    apply (metis \<open>path g\<close> homotopic_paths_eq pag path_image_subpath_subset path_subpath subset_trans v w)
  3.1233 -    apply (simp add:)
  3.1234 +    apply (metis \<open>path g\<close> homotopic_paths_eq pag path_image_subpath_subset path_subpath subset_trans v w, simp)
  3.1235      done
  3.1236    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)"
  3.1237      apply (rule homotopic_paths_sym [OF homotopic_paths_assoc])
  3.1238 @@ -4346,7 +4314,7 @@
  3.1239      apply (rule homotopic_paths_join)
  3.1240      apply (metis \<open>path g\<close> homotopic_paths_eq order.trans pag path_image_subpath_subset path_subpath u v)
  3.1241      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)
  3.1242 -    apply (simp add:)
  3.1243 +    apply simp
  3.1244      done
  3.1245    also have "homotopic_paths s (subpath u v g +++ linepath (pathfinish (subpath u v g)) (pathfinish (subpath u v g))) (subpath u v g)"
  3.1246      apply (rule homotopic_paths_rid)
  3.1247 @@ -4370,7 +4338,7 @@
  3.1248      "path_component S a b \<Longrightarrow> homotopic_loops S (linepath a a) (linepath b b)"
  3.1249  apply (simp add: path_component_def homotopic_loops_def homotopic_with_def
  3.1250                   pathstart_def pathfinish_def path_image_def path_def, clarify)
  3.1251 -apply (rule_tac x="g o fst" in exI)
  3.1252 +apply (rule_tac x="g \<circ> fst" in exI)
  3.1253  apply (intro conjI continuous_intros continuous_on_compose)+
  3.1254  apply (auto elim!: continuous_on_subset)
  3.1255  done
  3.1256 @@ -4380,7 +4348,7 @@
  3.1257          \<Longrightarrow> path_component S (p t) (q t)"
  3.1258  apply (simp add: path_component_def homotopic_loops_def homotopic_with_def
  3.1259                   pathstart_def pathfinish_def path_image_def path_def, clarify)
  3.1260 -apply (rule_tac x="h o (\<lambda>u. (u, t))" in exI)
  3.1261 +apply (rule_tac x="h \<circ> (\<lambda>u. (u, t))" in exI)
  3.1262  apply (intro conjI continuous_intros continuous_on_compose)+
  3.1263  apply (auto elim!: continuous_on_subset)
  3.1264  done
  3.1265 @@ -4547,10 +4515,10 @@
  3.1266        done
  3.1267      moreover have "path_image (fst \<circ> p) \<subseteq> S"
  3.1268        using that apply (simp add: path_image_def) by force
  3.1269 -    ultimately have p1: "homotopic_loops S (fst o p) (linepath a a)"
  3.1270 +    ultimately have p1: "homotopic_loops S (fst \<circ> p) (linepath a a)"
  3.1271        using S that
  3.1272        apply (simp add: simply_connected_eq_contractible_loop_any)
  3.1273 -      apply (drule_tac x="fst o p" in spec)
  3.1274 +      apply (drule_tac x="fst \<circ> p" in spec)
  3.1275        apply (drule_tac x=a in spec)
  3.1276        apply (auto simp: pathstart_def pathfinish_def)
  3.1277        done
  3.1278 @@ -4560,10 +4528,10 @@
  3.1279        done
  3.1280      moreover have "path_image (snd \<circ> p) \<subseteq> T"
  3.1281        using that apply (simp add: path_image_def) by force
  3.1282 -    ultimately have p2: "homotopic_loops T (snd o p) (linepath b b)"
  3.1283 +    ultimately have p2: "homotopic_loops T (snd \<circ> p) (linepath b b)"
  3.1284        using T that
  3.1285        apply (simp add: simply_connected_eq_contractible_loop_any)
  3.1286 -      apply (drule_tac x="snd o p" in spec)
  3.1287 +      apply (drule_tac x="snd \<circ> p" in spec)
  3.1288        apply (drule_tac x=b in spec)
  3.1289        apply (auto simp: pathstart_def pathfinish_def)
  3.1290        done
  3.1291 @@ -4594,15 +4562,14 @@
  3.1292  next
  3.1293    case False
  3.1294    obtain a where a: "homotopic_with (\<lambda>x. True) S S id (\<lambda>x. a)"
  3.1295 -    using assms by (force simp add: contractible_def)
  3.1296 +    using assms by (force simp: contractible_def)
  3.1297    then have "a \<in> S"
  3.1298      by (metis False homotopic_constant_maps homotopic_with_symD homotopic_with_trans path_component_mem(2))
  3.1299    show ?thesis
  3.1300      apply (simp add: simply_connected_eq_contractible_loop_all False)
  3.1301      apply (rule bexI [OF _ \<open>a \<in> S\<close>])
  3.1302 -    using a apply (simp add: homotopic_loops_def homotopic_with_def path_def path_image_def pathfinish_def pathstart_def)
  3.1303 -    apply clarify
  3.1304 -    apply (rule_tac x="(h o (\<lambda>y. (fst y, (p \<circ> snd) y)))" in exI)
  3.1305 +    using a apply (simp add: homotopic_loops_def homotopic_with_def path_def path_image_def pathfinish_def pathstart_def, clarify)
  3.1306 +    apply (rule_tac x="(h \<circ> (\<lambda>y. (fst y, (p \<circ> snd) y)))" in exI)
  3.1307      apply (intro conjI continuous_on_compose continuous_intros)
  3.1308      apply (erule continuous_on_subset | force)+
  3.1309      done
  3.1310 @@ -4623,10 +4590,10 @@
  3.1311    assumes f: "continuous_on S f" "f ` S \<subseteq> T"
  3.1312        and g: "continuous_on T g" "g ` T \<subseteq> U"
  3.1313        and T: "contractible T"
  3.1314 -    obtains c where "homotopic_with (\<lambda>h. True) S U (g o f) (\<lambda>x. c)"
  3.1315 +    obtains c where "homotopic_with (\<lambda>h. True) S U (g \<circ> f) (\<lambda>x. c)"
  3.1316  proof -
  3.1317    obtain b where b: "homotopic_with (\<lambda>x. True) T T id (\<lambda>x. b)"
  3.1318 -    using assms by (force simp add: contractible_def)
  3.1319 +    using assms by (force simp: contractible_def)
  3.1320    have "homotopic_with (\<lambda>f. True) T U (g \<circ> id) (g \<circ> (\<lambda>x. b))"
  3.1321      by (rule homotopic_compose_continuous_left [OF b g])
  3.1322    then have "homotopic_with (\<lambda>f. True) S U (g \<circ> id \<circ> f) (g \<circ> (\<lambda>x. b) \<circ> f)"
  3.1323 @@ -4660,15 +4627,15 @@
  3.1324            "continuous_on S f2" "f2 ` S \<subseteq> T"
  3.1325            "continuous_on T g2" "g2 ` T \<subseteq> U"
  3.1326            "contractible T" "path_connected U"
  3.1327 -   shows "homotopic_with (\<lambda>h. True) S U (g1 o f1) (g2 o f2)"
  3.1328 +   shows "homotopic_with (\<lambda>h. True) S U (g1 \<circ> f1) (g2 \<circ> f2)"
  3.1329  proof -
  3.1330 -  obtain c1 where c1: "homotopic_with (\<lambda>h. True) S U (g1 o f1) (\<lambda>x. c1)"
  3.1331 +  obtain c1 where c1: "homotopic_with (\<lambda>h. True) S U (g1 \<circ> f1) (\<lambda>x. c1)"
  3.1332      apply (rule nullhomotopic_through_contractible [of S f1 T g1 U])
  3.1333 -    using assms apply (auto simp: )
  3.1334 +    using assms apply auto
  3.1335      done
  3.1336 -  obtain c2 where c2: "homotopic_with (\<lambda>h. True) S U (g2 o f2) (\<lambda>x. c2)"
  3.1337 +  obtain c2 where c2: "homotopic_with (\<lambda>h. True) S U (g2 \<circ> f2) (\<lambda>x. c2)"
  3.1338      apply (rule nullhomotopic_through_contractible [of S f2 T g2 U])
  3.1339 -    using assms apply (auto simp: )
  3.1340 +    using assms apply auto
  3.1341      done
  3.1342    have *: "S = {} \<or> (\<exists>t. path_connected t \<and> t \<subseteq> U \<and> c2 \<in> t \<and> c1 \<in> t)"
  3.1343    proof (cases "S = {}")
  3.1344 @@ -4712,15 +4679,14 @@
  3.1345      obtains a where "homotopic_with P S S (\<lambda>x. x) (\<lambda>x. a)"
  3.1346  proof -
  3.1347    obtain a where "a \<in> S" and a: "\<And>x. x \<in> S \<Longrightarrow> closed_segment a x \<subseteq> S"
  3.1348 -    using S by (auto simp add: starlike_def)
  3.1349 +    using S by (auto simp: starlike_def)
  3.1350    have "(\<lambda>y. (1 - fst y) *\<^sub>R snd y + fst y *\<^sub>R a) ` ({0..1} \<times> S) \<subseteq> S"
  3.1351      apply clarify
  3.1352 -    apply (erule a [unfolded closed_segment_def, THEN subsetD])
  3.1353 -    apply (simp add: )
  3.1354 +    apply (erule a [unfolded closed_segment_def, THEN subsetD], simp)
  3.1355      apply (metis add_diff_cancel_right' diff_ge_0_iff_ge le_add_diff_inverse pth_c(1))
  3.1356      done
  3.1357    then show ?thesis
  3.1358 -    apply (rule_tac a="a" in that)
  3.1359 +    apply (rule_tac a=a in that)
  3.1360      using \<open>a \<in> S\<close>
  3.1361      apply (simp add: homotopic_with_def)
  3.1362      apply (rule_tac x="\<lambda>y. (1 - (fst y)) *\<^sub>R snd y + (fst y) *\<^sub>R a" in exI)
  3.1363 @@ -4806,12 +4772,12 @@
  3.1364               and hsub: "h ` ({0..1} \<times> S) \<subseteq> S"
  3.1365               and [simp]: "\<And>x. x \<in> S \<Longrightarrow> h (0, x) = x"
  3.1366               and [simp]: "\<And>x. x \<in> S \<Longrightarrow>  h (1::real, x) = a"
  3.1367 -    using S by (auto simp add: contractible_def homotopic_with)
  3.1368 +    using S by (auto simp: contractible_def homotopic_with)
  3.1369    obtain b k where contk: "continuous_on ({0..1} \<times> T) k"
  3.1370               and ksub: "k ` ({0..1} \<times> T) \<subseteq> T"
  3.1371               and [simp]: "\<And>x. x \<in> T \<Longrightarrow> k (0, x) = x"
  3.1372               and [simp]: "\<And>x. x \<in> T \<Longrightarrow>  k (1::real, x) = b"
  3.1373 -    using T by (auto simp add: contractible_def homotopic_with)
  3.1374 +    using T by (auto simp: contractible_def homotopic_with)
  3.1375    show ?thesis
  3.1376      apply (simp add: contractible_def homotopic_with)
  3.1377      apply (rule exI [where x=a])
  3.1378 @@ -4819,7 +4785,7 @@
  3.1379      apply (rule exI [where x = "\<lambda>z. (h (fst z, fst(snd z)), k (fst z, snd(snd z)))"])
  3.1380      apply (intro conjI ballI continuous_intros continuous_on_compose2 [OF conth] continuous_on_compose2 [OF contk])
  3.1381      using hsub ksub
  3.1382 -    apply (auto simp: )
  3.1383 +    apply auto
  3.1384      done
  3.1385  qed
  3.1386  
  3.1387 @@ -4828,7 +4794,7 @@
  3.1388    assumes S: "contractible S"
  3.1389        and f: "continuous_on S f" "image f S \<subseteq> T"
  3.1390        and g: "continuous_on T g" "image g T \<subseteq> S"
  3.1391 -      and hom: "homotopic_with (\<lambda>x. True) T T (f o g) id"
  3.1392 +      and hom: "homotopic_with (\<lambda>x. True) T T (f \<circ> g) id"
  3.1393      shows "contractible T"
  3.1394  proof -
  3.1395    obtain b where "homotopic_with (\<lambda>h. True) S T f (\<lambda>x. b)"
  3.1396 @@ -4963,7 +4929,7 @@
  3.1397      using \<open>g ` t = S\<close> \<open>W \<subseteq> t\<close> apply blast
  3.1398      using g \<open>W \<subseteq> t\<close> apply auto[1]
  3.1399      by (simp add: f rev_image_eqI)
  3.1400 -  have o: "openin (subtopology euclidean S) (g ` W)"
  3.1401 +  have \<circ>: "openin (subtopology euclidean S) (g ` W)"
  3.1402    proof -
  3.1403      have "continuous_on S f"
  3.1404        using f(3) by blast
  3.1405 @@ -6138,7 +6104,7 @@
  3.1406          then show ?thesis
  3.1407            using connected_component_eq_empty by auto
  3.1408        qed
  3.1409 -      also have "... \<subseteq> (S \<inter> f -` C)"
  3.1410 +      also have "\<dots> \<subseteq> (S \<inter> f -` C)"
  3.1411          by (rule connected_component_subset)
  3.1412        finally show "connected_component_set (S \<inter> f -` U) x \<subseteq> (S \<inter> f -` C)" .
  3.1413      qed
  3.1414 @@ -6200,7 +6166,7 @@
  3.1415          by (force simp: \<open>x \<in> S\<close> \<open>f x \<in> U\<close> path_component_refl_eq)
  3.1416        ultimately have "f ` (path_component_set (S \<inter> f -` U) x) \<subseteq> path_component_set U (f x)"
  3.1417          by (meson path_component_maximal)
  3.1418 -       also have  "... \<subseteq> path_component_set U y"
  3.1419 +       also have  "\<dots> \<subseteq> path_component_set U y"
  3.1420          by (simp add: Uyfx path_component_maximal path_component_subset path_component_sym)
  3.1421        finally have fC: "f ` (path_component_set (S \<inter> f -` U) x) \<subseteq> path_component_set U y" .
  3.1422        have cUC: "path_component_set (S \<inter> f -` U) x \<subseteq> (S \<inter> f -` path_component_set U y)"
  3.1423 @@ -6212,7 +6178,7 @@
  3.1424          then show ?thesis
  3.1425            using path_component_path_component by blast
  3.1426        qed
  3.1427 -      also have "... \<subseteq> (S \<inter> f -` path_component_set U y)"
  3.1428 +      also have "\<dots> \<subseteq> (S \<inter> f -` path_component_set U y)"
  3.1429          by (rule path_component_subset)
  3.1430        finally show "path_component_set (S \<inter> f -` U) x \<subseteq> (S \<inter> f -` path_component_set U y)" .
  3.1431      qed
  3.1432 @@ -6366,11 +6332,11 @@
  3.1433      obtain a where x: "x = (\<Sum>v \<in> B. a v *\<^sub>R v)"
  3.1434        using \<open>finite B\<close> \<open>span B = S\<close> \<open>x \<in> S\<close> span_finite by fastforce
  3.1435      have "norm (f x)^2 = norm (\<Sum>v\<in>B. a v *\<^sub>R fb v)^2" by (simp add: sum scale ffb x)
  3.1436 -    also have "... = (\<Sum>v\<in>B. norm ((a v *\<^sub>R fb v))^2)"
  3.1437 +    also have "\<dots> = (\<Sum>v\<in>B. norm ((a v *\<^sub>R fb v))^2)"
  3.1438        apply (rule norm_sum_Pythagorean [OF \<open>finite B\<close>])
  3.1439        apply (rule pairwise_ortho_scaleR [OF pairwise_orth_fb])
  3.1440        done
  3.1441 -    also have "... = norm x ^2"
  3.1442 +    also have "\<dots> = norm x ^2"
  3.1443        by (simp add: x pairwise_ortho_scaleR Borth norm_sum_Pythagorean [OF \<open>finite B\<close>])
  3.1444      finally show ?thesis
  3.1445        by (simp add: norm_eq_sqrt_inner)
  3.1446 @@ -6429,29 +6395,29 @@
  3.1447        using \<open>finite B\<close> \<open>span B = S\<close> \<open>x \<in> S\<close> span_finite by fastforce
  3.1448      have "f x = (\<Sum>v \<in> B. f (a v *\<^sub>R v))"
  3.1449        using linear_sum [OF \<open>linear f\<close>] x by auto
  3.1450 -    also have "... = (\<Sum>v \<in> B. a v *\<^sub>R f v)"
  3.1451 +    also have "\<dots> = (\<Sum>v \<in> B. a v *\<^sub>R f v)"
  3.1452        by (simp add: f.sum f.scale)
  3.1453 -    also have "... = (\<Sum>v \<in> B. a v *\<^sub>R fb v)"
  3.1454 +    also have "\<dots> = (\<Sum>v \<in> B. a v *\<^sub>R fb v)"
  3.1455        by (simp add: ffb cong: sum.cong)
  3.1456      finally have *: "f x = (\<Sum>v\<in>B. a v *\<^sub>R fb v)" .
  3.1457      then have "(norm (f x))\<^sup>2 = (norm (\<Sum>v\<in>B. a v *\<^sub>R fb v))\<^sup>2" by simp
  3.1458 -    also have "... = (\<Sum>v\<in>B. norm ((a v *\<^sub>R fb v))^2)"
  3.1459 +    also have "\<dots> = (\<Sum>v\<in>B. norm ((a v *\<^sub>R fb v))^2)"
  3.1460        apply (rule norm_sum_Pythagorean [OF \<open>finite B\<close>])
  3.1461        apply (rule pairwise_ortho_scaleR [OF pairwise_orth_fb])
  3.1462        done
  3.1463 -    also have "... = (norm x)\<^sup>2"
  3.1464 +    also have "\<dots> = (norm x)\<^sup>2"
  3.1465        by (simp add: x pairwise_ortho_scaleR Borth norm_sum_Pythagorean [OF \<open>finite B\<close>])
  3.1466      finally show "norm (f x) = norm x"
  3.1467        by (simp add: norm_eq_sqrt_inner)
  3.1468      have "g (f x) = g (\<Sum>v\<in>B. a v *\<^sub>R fb v)" by (simp add: *)
  3.1469 -    also have "... = (\<Sum>v\<in>B. g (a v *\<^sub>R fb v))"
  3.1470 +    also have "\<dots> = (\<Sum>v\<in>B. g (a v *\<^sub>R fb v))"
  3.1471        by (simp add: g.sum g.scale)
  3.1472 -    also have "... = (\<Sum>v\<in>B. a v *\<^sub>R g (fb v))"
  3.1473 +    also have "\<dots> = (\<Sum>v\<in>B. a v *\<^sub>R g (fb v))"
  3.1474        by (simp add: g.scale)
  3.1475 -    also have "... = (\<Sum>v\<in>B. a v *\<^sub>R v)"
  3.1476 +    also have "\<dots> = (\<Sum>v\<in>B. a v *\<^sub>R v)"
  3.1477        apply (rule sum.cong [OF refl])
  3.1478        using \<open>bij_betw fb B C\<close> gb_def bij_betwE bij_betw_inv_into_left gb_def ggb by fastforce
  3.1479 -    also have "... = x"
  3.1480 +    also have "\<dots> = x"
  3.1481        using x by blast
  3.1482      finally show "g (f x) = x" .
  3.1483    qed
  3.1484 @@ -6463,19 +6429,19 @@
  3.1485        using \<open>finite C\<close> \<open>span C = T\<close> \<open>x \<in> T\<close> span_finite by fastforce
  3.1486      have "g x = (\<Sum>v \<in> C. g (a v *\<^sub>R v))"
  3.1487        by (simp add: x g.sum)
  3.1488 -    also have "... = (\<Sum>v \<in> C. a v *\<^sub>R g v)"
  3.1489 +    also have "\<dots> = (\<Sum>v \<in> C. a v *\<^sub>R g v)"
  3.1490        by (simp add: g.scale)
  3.1491 -    also have "... = (\<Sum>v \<in> C. a v *\<^sub>R gb v)"
  3.1492 +    also have "\<dots> = (\<Sum>v \<in> C. a v *\<^sub>R gb v)"
  3.1493        by (simp add: ggb cong: sum.cong)
  3.1494      finally have "f (g x) = f (\<Sum>v\<in>C. a v *\<^sub>R gb v)" by simp
  3.1495 -    also have "... = (\<Sum>v\<in>C. f (a v *\<^sub>R gb v))"
  3.1496 +    also have "\<dots> = (\<Sum>v\<in>C. f (a v *\<^sub>R gb v))"
  3.1497        by (simp add: f.scale f.sum)
  3.1498 -    also have "... = (\<Sum>v\<in>C. a v *\<^sub>R f (gb v))"
  3.1499 +    also have "\<dots> = (\<Sum>v\<in>C. a v *\<^sub>R f (gb v))"
  3.1500        by (simp add: f.scale f.sum)
  3.1501 -    also have "... = (\<Sum>v\<in>C. a v *\<^sub>R v)"
  3.1502 +    also have "\<dots> = (\<Sum>v\<in>C. a v *\<^sub>R v)"
  3.1503        using \<open>bij_betw fb B C\<close>
  3.1504        by (simp add: bij_betw_def gb_def bij_betw_inv_into_right ffb inv_into_into)
  3.1505 -    also have "... = x"
  3.1506 +    also have "\<dots> = x"
  3.1507        using x by blast
  3.1508      finally show "f (g x) = x" .
  3.1509    qed
  3.1510 @@ -6508,7 +6474,7 @@
  3.1511    where "linear f" "linear g"
  3.1512                      "\<And>x. norm(f x) = norm x" "\<And>y. norm(g y) = norm y"
  3.1513                      "\<And>x. g (f x) = x" "\<And>y. f(g y) = y"
  3.1514 -  using assms by (auto simp: intro: isometries_subspaces [of "UNIV::'M set" "UNIV::'N set"])
  3.1515 +  using assms by (auto intro: isometries_subspaces [of "UNIV::'M set" "UNIV::'N set"])
  3.1516  
  3.1517  lemma homeomorphic_subspaces:
  3.1518    fixes S :: "'a::euclidean_space set"
  3.1519 @@ -6544,9 +6510,9 @@
  3.1520      using assms ab  by (simp add: aff_dim_eq_dim  [OF hull_inc] image_def)
  3.1521    have "S homeomorphic ((+) (- a) ` S)"
  3.1522      by (simp add: homeomorphic_translation)
  3.1523 -  also have "... homeomorphic ((+) (- b) ` T)"
  3.1524 +  also have "\<dots> homeomorphic ((+) (- b) ` T)"
  3.1525      by (rule homeomorphic_subspaces [OF ss dd])
  3.1526 -  also have "... homeomorphic T"
  3.1527 +  also have "\<dots> homeomorphic T"
  3.1528      using homeomorphic_sym homeomorphic_translation by auto
  3.1529    finally show ?thesis .
  3.1530  qed
  3.1531 @@ -6564,8 +6530,8 @@
  3.1532  begin
  3.1533  
  3.1534  lemma homotopically_trivial_retraction_gen:
  3.1535 -  assumes P: "\<And>f. \<lbrakk>continuous_on u f; f ` u \<subseteq> t; Q f\<rbrakk> \<Longrightarrow> P(k o f)"
  3.1536 -      and Q: "\<And>f. \<lbrakk>continuous_on u f; f ` u \<subseteq> s; P f\<rbrakk> \<Longrightarrow> Q(h o f)"
  3.1537 +  assumes P: "\<And>f. \<lbrakk>continuous_on u f; f ` u \<subseteq> t; Q f\<rbrakk> \<Longrightarrow> P(k \<circ> f)"
  3.1538 +      and Q: "\<And>f. \<lbrakk>continuous_on u f; f ` u \<subseteq> s; P f\<rbrakk> \<Longrightarrow> Q(h \<circ> f)"
  3.1539        and Qeq: "\<And>h k. (\<And>x. x \<in> u \<Longrightarrow> h x = k x) \<Longrightarrow> Q h = Q k"
  3.1540        and hom: "\<And>f g. \<lbrakk>continuous_on u f; f ` u \<subseteq> s; P f;
  3.1541                         continuous_on u g; g ` u \<subseteq> s; P g\<rbrakk>
  3.1542 @@ -6602,8 +6568,8 @@
  3.1543  qed
  3.1544  
  3.1545  lemma homotopically_trivial_retraction_null_gen:
  3.1546 -  assumes P: "\<And>f. \<lbrakk>continuous_on u f; f ` u \<subseteq> t; Q f\<rbrakk> \<Longrightarrow> P(k o f)"
  3.1547 -      and Q: "\<And>f. \<lbrakk>continuous_on u f; f ` u \<subseteq> s; P f\<rbrakk> \<Longrightarrow> Q(h o f)"
  3.1548 +  assumes P: "\<And>f. \<lbrakk>continuous_on u f; f ` u \<subseteq> t; Q f\<rbrakk> \<Longrightarrow> P(k \<circ> f)"
  3.1549 +      and Q: "\<And>f. \<lbrakk>continuous_on u f; f ` u \<subseteq> s; P f\<rbrakk> \<Longrightarrow> Q(h \<circ> f)"
  3.1550        and Qeq: "\<And>h k. (\<And>x. x \<in> u \<Longrightarrow> h x = k x) \<Longrightarrow> Q h = Q k"
  3.1551        and hom: "\<And>f. \<lbrakk>continuous_on u f; f ` u \<subseteq> s; P f\<rbrakk>
  3.1552                       \<Longrightarrow> \<exists>c. homotopic_with P u s f (\<lambda>x. c)"
  3.1553 @@ -6619,7 +6585,7 @@
  3.1554      by (simp add: P Qf contf imf)
  3.1555    ultimately obtain c where "homotopic_with P u s (k \<circ> f) (\<lambda>x. c)"
  3.1556      by (metis hom)
  3.1557 -  then have "homotopic_with Q u t (h \<circ> (k \<circ> f)) (h o (\<lambda>x. c))"
  3.1558 +  then have "homotopic_with Q u t (h \<circ> (k \<circ> f)) (h \<circ> (\<lambda>x. c))"
  3.1559      apply (rule homotopic_with_compose_continuous_left [OF homotopic_with_mono])
  3.1560      using Q by (auto simp: conth imh)
  3.1561    then show ?thesis
  3.1562 @@ -6631,8 +6597,8 @@
  3.1563  qed
  3.1564  
  3.1565  lemma cohomotopically_trivial_retraction_gen:
  3.1566 -  assumes P: "\<And>f. \<lbrakk>continuous_on t f; f ` t \<subseteq> u; Q f\<rbrakk> \<Longrightarrow> P(f o h)"
  3.1567 -      and Q: "\<And>f. \<lbrakk>continuous_on s f; f ` s \<subseteq> u; P f\<rbrakk> \<Longrightarrow> Q(f o k)"
  3.1568 +  assumes P: "\<And>f. \<lbrakk>continuous_on t f; f ` t \<subseteq> u; Q f\<rbrakk> \<Longrightarrow> P(f \<circ> h)"
  3.1569 +      and Q: "\<And>f. \<lbrakk>continuous_on s f; f ` s \<subseteq> u; P f\<rbrakk> \<Longrightarrow> Q(f \<circ> k)"
  3.1570        and Qeq: "\<And>h k. (\<And>x. x \<in> t \<Longrightarrow> h x = k x) \<Longrightarrow> Q h = Q k"
  3.1571        and hom: "\<And>f g. \<lbrakk>continuous_on s f; f ` s \<subseteq> u; P f;
  3.1572                         continuous_on s g; g ` s \<subseteq> u; P g\<rbrakk>
  3.1573 @@ -6649,15 +6615,15 @@
  3.1574      using imf imh by fastforce
  3.1575    moreover have "P (f \<circ> h)"
  3.1576      by (simp add: P Qf contf imf)
  3.1577 -  moreover have "continuous_on s (g o h)"
  3.1578 +  moreover have "continuous_on s (g \<circ> h)"
  3.1579      using contg continuous_on_compose continuous_on_subset conth imh by blast
  3.1580    moreover have "(g \<circ> h) ` s \<subseteq> u"
  3.1581      using img imh by fastforce
  3.1582    moreover have "P (g \<circ> h)"
  3.1583      by (simp add: P Qg contg img)
  3.1584 -  ultimately have "homotopic_with P s u (f o h) (g \<circ> h)"
  3.1585 +  ultimately have "homotopic_with P s u (f \<circ> h) (g \<circ> h)"
  3.1586      by (rule hom)
  3.1587 -  then have "homotopic_with Q t u (f o h o k) (g \<circ> h o k)"
  3.1588 +  then have "homotopic_with Q t u (f \<circ> h \<circ> k) (g \<circ> h \<circ> k)"
  3.1589      apply (rule homotopic_with_compose_continuous_right [OF homotopic_with_mono])
  3.1590      using Q by (auto simp: contk imk)
  3.1591    then show ?thesis
  3.1592 @@ -6669,8 +6635,8 @@
  3.1593  qed
  3.1594  
  3.1595  lemma cohomotopically_trivial_retraction_null_gen:
  3.1596 -  assumes P: "\<And>f. \<lbrakk>continuous_on t f; f ` t \<subseteq> u; Q f\<rbrakk> \<Longrightarrow> P(f o h)"
  3.1597 -      and Q: "\<And>f. \<lbrakk>continuous_on s f; f ` s \<subseteq> u; P f\<rbrakk> \<Longrightarrow> Q(f o k)"
  3.1598 +  assumes P: "\<And>f. \<lbrakk>continuous_on t f; f ` t \<subseteq> u; Q f\<rbrakk> \<Longrightarrow> P(f \<circ> h)"
  3.1599 +      and Q: "\<And>f. \<lbrakk>continuous_on s f; f ` s \<subseteq> u; P f\<rbrakk> \<Longrightarrow> Q(f \<circ> k)"
  3.1600        and Qeq: "\<And>h k. (\<And>x. x \<in> t \<Longrightarrow> h x = k x) \<Longrightarrow> Q h = Q k"
  3.1601        and hom: "\<And>f g. \<lbrakk>continuous_on s f; f ` s \<subseteq> u; P f\<rbrakk>
  3.1602                         \<Longrightarrow> \<exists>c. homotopic_with P s u f (\<lambda>x. c)"
  3.1603 @@ -6684,9 +6650,9 @@
  3.1604      using imf imh by fastforce
  3.1605    moreover have "P (f \<circ> h)"
  3.1606      by (simp add: P Qf contf imf)
  3.1607 -  ultimately obtain c where "homotopic_with P s u (f o h) (\<lambda>x. c)"
  3.1608 +  ultimately obtain c where "homotopic_with P s u (f \<circ> h) (\<lambda>x. c)"
  3.1609      by (metis hom)
  3.1610 -  then have "homotopic_with Q t u (f o h o k) ((\<lambda>x. c) o k)"
  3.1611 +  then have "homotopic_with Q t u (f \<circ> h \<circ> k) ((\<lambda>x. c) \<circ> k)"
  3.1612      apply (rule homotopic_with_compose_continuous_right [OF homotopic_with_mono])
  3.1613      using Q by (auto simp: contk imk)
  3.1614    then show ?thesis
  3.1615 @@ -6724,8 +6690,8 @@
  3.1616    where "S homotopy_eqv T \<equiv>
  3.1617          \<exists>f g. continuous_on S f \<and> f ` S \<subseteq> T \<and>
  3.1618                continuous_on T g \<and> g ` T \<subseteq> S \<and>
  3.1619 -              homotopic_with (\<lambda>x. True) S S (g o f) id \<and>
  3.1620 -              homotopic_with (\<lambda>x. True) T T (f o g) id"
  3.1621 +              homotopic_with (\<lambda>x. True) S S (g \<circ> f) id \<and>
  3.1622 +              homotopic_with (\<lambda>x. True) T T (f \<circ> g) id"
  3.1623  
  3.1624  lemma homeomorphic_imp_homotopy_eqv: "S homeomorphic T \<Longrightarrow> S homotopy_eqv T"
  3.1625    unfolding homeomorphic_def homotopy_eqv_def homeomorphism_def
  3.1626 @@ -6744,22 +6710,22 @@
  3.1627  proof -
  3.1628    obtain f1 g1 where f1: "continuous_on S f1" "f1 ` S \<subseteq> T"
  3.1629                   and g1: "continuous_on T g1" "g1 ` T \<subseteq> S"
  3.1630 -                 and hom1: "homotopic_with (\<lambda>x. True) S S (g1 o f1) id"
  3.1631 -                           "homotopic_with (\<lambda>x. True) T T (f1 o g1) id"
  3.1632 +                 and hom1: "homotopic_with (\<lambda>x. True) S S (g1 \<circ> f1) id"
  3.1633 +                           "homotopic_with (\<lambda>x. True) T T (f1 \<circ> g1) id"
  3.1634      using ST by (auto simp: homotopy_eqv_def)
  3.1635    obtain f2 g2 where f2: "continuous_on T f2" "f2 ` T \<subseteq> U"
  3.1636                   and g2: "continuous_on U g2" "g2 ` U \<subseteq> T"
  3.1637 -                 and hom2: "homotopic_with (\<lambda>x. True) T T (g2 o f2) id"
  3.1638 -                           "homotopic_with (\<lambda>x. True) U U (f2 o g2) id"
  3.1639 +                 and hom2: "homotopic_with (\<lambda>x. True) T T (g2 \<circ> f2) id"
  3.1640 +                           "homotopic_with (\<lambda>x. True) U U (f2 \<circ> g2) id"
  3.1641      using TU by (auto simp: homotopy_eqv_def)
  3.1642    have "homotopic_with (\<lambda>f. True) S T (g2 \<circ> f2 \<circ> f1) (id \<circ> f1)"
  3.1643      by (rule homotopic_with_compose_continuous_right hom2 f1)+
  3.1644    then have "homotopic_with (\<lambda>f. True) S T (g2 \<circ> (f2 \<circ> f1)) (id \<circ> f1)"
  3.1645      by (simp add: o_assoc)
  3.1646    then have "homotopic_with (\<lambda>x. True) S S
  3.1647 -         (g1 \<circ> (g2 \<circ> (f2 \<circ> f1))) (g1 o (id o f1))"
  3.1648 +         (g1 \<circ> (g2 \<circ> (f2 \<circ> f1))) (g1 \<circ> (id \<circ> f1))"
  3.1649      by (simp add: g1 homotopic_with_compose_continuous_left)
  3.1650 -  moreover have "homotopic_with (\<lambda>x. True) S S (g1 o id o f1) id"
  3.1651 +  moreover have "homotopic_with (\<lambda>x. True) S S (g1 \<circ> id \<circ> f1) id"
  3.1652      using hom1 by simp
  3.1653    ultimately have SS: "homotopic_with (\<lambda>x. True) S S (g1 \<circ> g2 \<circ> (f2 \<circ> f1)) id"
  3.1654      apply (simp add: o_assoc)
  3.1655 @@ -6770,9 +6736,9 @@
  3.1656    then have "homotopic_with (\<lambda>f. True) U T (f1 \<circ> (g1 \<circ> g2)) (id \<circ> g2)"
  3.1657      by (simp add: o_assoc)
  3.1658    then have "homotopic_with (\<lambda>x. True) U U
  3.1659 -         (f2 \<circ> (f1 \<circ> (g1 \<circ> g2))) (f2 o (id o g2))"
  3.1660 +         (f2 \<circ> (f1 \<circ> (g1 \<circ> g2))) (f2 \<circ> (id \<circ> g2))"
  3.1661      by (simp add: f2 homotopic_with_compose_continuous_left)
  3.1662 -  moreover have "homotopic_with (\<lambda>x. True) U U (f2 o id o g2) id"
  3.1663 +  moreover have "homotopic_with (\<lambda>x. True) U U (f2 \<circ> id \<circ> g2) id"
  3.1664      using hom2 by simp
  3.1665    ultimately have UU: "homotopic_with (\<lambda>x. True) U U (f2 \<circ> f1 \<circ> (g1 \<circ> g2)) id"
  3.1666      apply (simp add: o_assoc)
  3.1667 @@ -6814,8 +6780,8 @@
  3.1668  proof -
  3.1669    obtain h k where h: "continuous_on S h" "h ` S \<subseteq> T"
  3.1670                 and k: "continuous_on T k" "k ` T \<subseteq> S"
  3.1671 -               and hom: "homotopic_with (\<lambda>x. True) S S (k o h) id"
  3.1672 -                        "homotopic_with (\<lambda>x. True) T T (h o k) id"
  3.1673 +               and hom: "homotopic_with (\<lambda>x. True) S S (k \<circ> h) id"
  3.1674 +                        "homotopic_with (\<lambda>x. True) T T (h \<circ> k) id"
  3.1675      using assms by (auto simp: homotopy_eqv_def)
  3.1676    have "homotopic_with (\<lambda>f. True) U S (k \<circ> f) (k \<circ> g)"
  3.1677      apply (rule homUS)
  3.1678 @@ -6823,15 +6789,15 @@
  3.1679      apply (safe intro!: continuous_on_compose h k f elim!: continuous_on_subset)
  3.1680      apply (force simp: o_def)+
  3.1681      done
  3.1682 -  then have "homotopic_with (\<lambda>x. True) U T (h o (k o f)) (h o (k o g))"
  3.1683 +  then have "homotopic_with (\<lambda>x. True) U T (h \<circ> (k \<circ> f)) (h \<circ> (k \<circ> g))"
  3.1684      apply (rule homotopic_with_compose_continuous_left)
  3.1685      apply (simp_all add: h)
  3.1686      done
  3.1687 -  moreover have "homotopic_with (\<lambda>x. True) U T (h o k o f) (id o f)"
  3.1688 +  moreover have "homotopic_with (\<lambda>x. True) U T (h \<circ> k \<circ> f) (id \<circ> f)"
  3.1689      apply (rule homotopic_with_compose_continuous_right [where X=T and Y=T])
  3.1690      apply (auto simp: hom f)
  3.1691      done
  3.1692 -  moreover have "homotopic_with (\<lambda>x. True) U T (h o k o g) (id o g)"
  3.1693 +  moreover have "homotopic_with (\<lambda>x. True) U T (h \<circ> k \<circ> g) (id \<circ> g)"
  3.1694      apply (rule homotopic_with_compose_continuous_right [where X=T and Y=T])
  3.1695      apply (auto simp: hom g)
  3.1696      done
  3.1697 @@ -6867,15 +6833,15 @@
  3.1698  proof -
  3.1699    obtain h k where h: "continuous_on S h" "h ` S \<subseteq> T"
  3.1700                 and k: "continuous_on T k" "k ` T \<subseteq> S"
  3.1701 -               and hom: "homotopic_with (\<lambda>x. True) S S (k o h) id"
  3.1702 -                        "homotopic_with (\<lambda>x. True) T T (h o k) id"
  3.1703 +               and hom: "homotopic_with (\<lambda>x. True) S S (k \<circ> h) id"
  3.1704 +                        "homotopic_with (\<lambda>x. True) T T (h \<circ> k) id"
  3.1705      using assms by (auto simp: homotopy_eqv_def)
  3.1706    obtain c where "homotopic_with (\<lambda>x. True) S U (f \<circ> h) (\<lambda>x. c)"
  3.1707      apply (rule exE [OF homSU [of "f \<circ> h"]])
  3.1708      apply (intro continuous_on_compose h)
  3.1709      using h f  apply (force elim!: continuous_on_subset)+
  3.1710      done
  3.1711 -  then have "homotopic_with (\<lambda>x. True) T U ((f o h) o k) ((\<lambda>x. c) o k)"
  3.1712 +  then have "homotopic_with (\<lambda>x. True) T U ((f \<circ> h) \<circ> k) ((\<lambda>x. c) \<circ> k)"
  3.1713      apply (rule homotopic_with_compose_continuous_right [where X=S])
  3.1714      using k by auto
  3.1715    moreover have "homotopic_with (\<lambda>x. True) T U (f \<circ> id) (f \<circ> (h \<circ> k))"
  3.1716 @@ -7477,18 +7443,18 @@
  3.1717        using eq by (simp add: algebra_simps)
  3.1718      then have "norm x = norm (y + ((norm x - norm y) / r) *\<^sub>R u)"
  3.1719        by (metis diff_divide_distrib)
  3.1720 -    also have "... \<le> norm y + norm(((norm x - norm y) / r) *\<^sub>R u)"
  3.1721 +    also have "\<dots> \<le> norm y + norm(((norm x - norm y) / r) *\<^sub>R u)"
  3.1722        using norm_triangle_ineq by blast
  3.1723 -    also have "... = norm y + (norm x - norm y) * (norm u / r)"
  3.1724 +    also have "\<dots> = norm y + (norm x - norm y) * (norm u / r)"
  3.1725        using yx \<open>r > 0\<close>
  3.1726        by (simp add: divide_simps)
  3.1727 -    also have "... < norm y + (norm x - norm y) * 1"
  3.1728 +    also have "\<dots> < norm y + (norm x - norm y) * 1"
  3.1729        apply (subst add_less_cancel_left)
  3.1730        apply (rule mult_strict_left_mono)
  3.1731        using nou \<open>0 < r\<close> yx
  3.1732         apply (simp_all add: field_simps)
  3.1733        done
  3.1734 -    also have "... = norm x"
  3.1735 +    also have "\<dots> = norm x"
  3.1736        by simp
  3.1737      finally show False by simp
  3.1738    qed
  3.1739 @@ -7530,9 +7496,9 @@
  3.1740      proof -
  3.1741        have "norm (y + (1 - norm y / r) *\<^sub>R u) \<le> norm y + norm((1 - norm y / r) *\<^sub>R u)"
  3.1742          using norm_triangle_ineq by blast
  3.1743 -      also have "... = norm y + abs(1 - norm y / r) * norm u"
  3.1744 +      also have "\<dots> = norm y + abs(1 - norm y / r) * norm u"
  3.1745          by simp
  3.1746 -      also have "... \<le> r"
  3.1747 +      also have "\<dots> \<le> r"
  3.1748        proof -
  3.1749          have "(r - norm u) * (r - norm y) \<ge> 0"
  3.1750            using that by auto
  3.1751 @@ -7868,9 +7834,9 @@
  3.1752    then have ope: "openin (subtopology euclidean (affine hull S)) S"
  3.1753      using \<open>open S\<close> open_openin by auto
  3.1754    have "2 \<le> DIM('a)" by (rule 2)
  3.1755 -  also have "... = aff_dim (UNIV :: 'a set)"
  3.1756 +  also have "\<dots> = aff_dim (UNIV :: 'a set)"
  3.1757      by simp
  3.1758 -  also have "... \<le> aff_dim S"
  3.1759 +  also have "\<dots> \<le> aff_dim S"
  3.1760      by (metis aff_dim_UNIV aff_dim_affine_hull aff_dim_le_DIM affS)
  3.1761    finally have "2 \<le> aff_dim S"
  3.1762      by linarith
  3.1763 @@ -8167,16 +8133,11 @@
  3.1764    proof
  3.1765      show "homeomorphism T T (j \<circ> f \<circ> h) (j \<circ> g \<circ> h)"
  3.1766      proof
  3.1767 -      show "continuous_on T (j \<circ> f \<circ> h)"
  3.1768 -        apply (intro continuous_on_compose cont_hj)
  3.1769 -        using hom homeomorphism_def by blast
  3.1770 -      show "continuous_on T (j \<circ> g \<circ> h)"
  3.1771 -        apply (intro continuous_on_compose cont_hj)
  3.1772 -        using hom homeomorphism_def by blast
  3.1773 -      show "(j \<circ> f \<circ> h) ` T \<subseteq> T"
  3.1774 -        by clarsimp (metis (mono_tags, hide_lams) hj(1) hom homeomorphism_def imageE imageI)
  3.1775 -      show "(j \<circ> g \<circ> h) ` T \<subseteq> T"
  3.1776 -        by clarsimp (metis (mono_tags, hide_lams) hj(1) hom homeomorphism_def imageE imageI)
  3.1777 +      show "continuous_on T (j \<circ> f \<circ> h)" "continuous_on T (j \<circ> g \<circ> h)"
  3.1778 +        using hom homeomorphism_def
  3.1779 +        by (blast intro: continuous_on_compose cont_hj)+
  3.1780 +      show "(j \<circ> f \<circ> h) ` T \<subseteq> T" "(j \<circ> g \<circ> h) ` T \<subseteq> T"
  3.1781 +        by auto (metis (mono_tags, hide_lams) hj(1) hom homeomorphism_def imageE imageI)+
  3.1782        show "\<And>x. x \<in> T \<Longrightarrow> (j \<circ> g \<circ> h) ((j \<circ> f \<circ> h) x) = x"
  3.1783          using hj hom homeomorphism_apply1 by fastforce
  3.1784        show "\<And>y. y \<in> T \<Longrightarrow> (j \<circ> f \<circ> h) ((j \<circ> g \<circ> h) y) = y"
  3.1785 @@ -8188,12 +8149,10 @@
  3.1786        apply (drule_tac c="h x" in subsetD, force)
  3.1787        by (metis imageE)
  3.1788      have "bounded (j ` {x. (~ (f x = x \<and> g x = x))})"
  3.1789 -      apply (rule bounded_linear_image [OF bou])
  3.1790 -      using \<open>linear j\<close> linear_conv_bounded_linear by auto
  3.1791 +      by (rule bounded_linear_image [OF bou]) (use \<open>linear j\<close> linear_conv_bounded_linear in auto)
  3.1792      moreover
  3.1793      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))}"
  3.1794 -      using hj apply (auto simp: jf jg image_iff, metis+)
  3.1795 -      done
  3.1796 +      using hj by (auto simp: jf jg image_iff, metis+)
  3.1797      ultimately show "bounded {x. \<not> ((j \<circ> f \<circ> h) x = x \<and> (j \<circ> g \<circ> h) x = x)}"
  3.1798        by metis
  3.1799      show "\<And>x. x \<in> K \<Longrightarrow> (j \<circ> f \<circ> h) x \<in> U"
  3.1800 @@ -8329,10 +8288,10 @@
  3.1801          apply (rule imageE [OF subsetD [OF sub]], force)
  3.1802          by (metis h hull_inc)
  3.1803      next
  3.1804 -      have "bounded (j ` {x. (~ (f x = x \<and> g x = x))})"
  3.1805 -        apply (rule bounded_closure_image)
  3.1806 -        apply (rule compact_imp_bounded)
  3.1807 +      have "compact (j ` closure {x. \<not> (f x = x \<and> g x = x)})"
  3.1808          using bou by (auto simp: compact_continuous_image cont_hj)
  3.1809 +      then have "bounded (j ` {x. (~ (f x = x \<and> g x = x))})"
  3.1810 +        by (rule bounded_closure_image [OF compact_imp_bounded])
  3.1811        moreover
  3.1812        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))}"
  3.1813          using h j by (auto simp: image_iff; metis)
  3.1814 @@ -8487,7 +8446,7 @@
  3.1815              have "norm (h (norm (x - a) / r, a + (r / norm (x - a)) *\<^sub>R (x - a)) - h (0, a + r *\<^sub>R b1)) =
  3.1816                    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)))"
  3.1817                by (simp add: h)
  3.1818 -            also have "... < e"
  3.1819 +            also have "\<dots> < e"
  3.1820                apply (rule d [unfolded dist_norm])
  3.1821                using greater \<open>0 < d\<close> \<open>b1 \<in> Basis\<close> that
  3.1822                  by (auto simp: dist_norm divide_simps)
     4.1 --- a/src/HOL/Library/Extended_Real.thy	Sun May 06 23:30:34 2018 +0200
     4.2 +++ b/src/HOL/Library/Extended_Real.thy	Sun May 06 23:59:14 2018 +0100
     4.3 @@ -627,6 +627,28 @@
     4.4    "real_of_ereal y < x \<longleftrightarrow> (\<bar>y\<bar> \<noteq> \<infinity> \<longrightarrow> y < ereal x) \<and> (\<bar>y\<bar> = \<infinity> \<longrightarrow> 0 < x)"
     4.5    by (cases y) auto
     4.6  
     4.7 +(*To help with inferences like  a < ereal x \<Longrightarrow> x < y \<Longrightarrow> a < ereal y,
     4.8 +  where x and y are real.
     4.9 +*)
    4.10 +
    4.11 +lemma le_ereal_le: "a \<le> ereal x \<Longrightarrow> x \<le> y \<Longrightarrow> a \<le> ereal y"
    4.12 +  using ereal_less_eq(3) order.trans by blast
    4.13 +
    4.14 +lemma le_ereal_less: "a \<le> ereal x \<Longrightarrow> x < y \<Longrightarrow> a < ereal y"
    4.15 +  by (simp add: le_less_trans)
    4.16 +
    4.17 +lemma less_ereal_le: "a < ereal x \<Longrightarrow> x \<le> y \<Longrightarrow> a < ereal y"
    4.18 +  using ereal_less_ereal_Ex by auto
    4.19 +
    4.20 +lemma ereal_le_le: "ereal y \<le> a \<Longrightarrow> x \<le> y \<Longrightarrow> ereal x \<le> a"
    4.21 +  by (simp add: order_subst2)
    4.22 +
    4.23 +lemma ereal_le_less: "ereal y \<le> a \<Longrightarrow> x < y \<Longrightarrow> ereal x < a"
    4.24 +  by (simp add: dual_order.strict_trans1)
    4.25 +
    4.26 +lemma ereal_less_le: "ereal y < a \<Longrightarrow> x \<le> y \<Longrightarrow> ereal x < a"
    4.27 +  using ereal_less_eq(3) le_less_trans by blast
    4.28 +
    4.29  lemma real_of_ereal_pos:
    4.30    fixes x :: ereal
    4.31    shows "0 \<le> x \<Longrightarrow> 0 \<le> real_of_ereal x" by (cases x) auto