author paulson Sun May 06 23:59:14 2018 +0100 (14 months ago) changeset 68097 5f3cffe16311 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.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.13  lemma has_derivative_right:
1.14 @@ -98,8 +98,8 @@
1.15  lemmas DERIV_within_iff = has_field_derivative_iff
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.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.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.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)
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.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.23  lemma einterval_eq[simp]:
2.24 @@ -36,7 +22,7 @@
2.25    by (auto simp: einterval_def)
2.27  lemma einterval_same: "einterval a a = {}"
2.28 -  by (auto simp add: einterval_def)
2.29 +  by (auto simp: einterval_def)
2.31  lemma einterval_iff: "x \<in> einterval a b \<longleftrightarrow> a < ereal x \<and> ereal x < b"
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.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.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.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.108  lemma interval_lebesgue_integrable_mult_right [intro, simp]:
2.109 @@ -255,31 +234,31 @@
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.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.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.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.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.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.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.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.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.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.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.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.209 -(*
2.210 -TODO: many proofs below require inferences like
2.212 -  a < ereal x \<Longrightarrow> x < y \<Longrightarrow> a < ereal y
2.214 -where x and y are real. These should be better automated.
2.215 -*)
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.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.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.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.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.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.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.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.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.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.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.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.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.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.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.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.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.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.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.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.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.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.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.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.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.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.110 @@ -151,7 +151,7 @@
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.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.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.149 -lemma pathstart_compose: "pathstart(f o p) = f(pathstart p)"
3.150 +lemma pathstart_compose: "pathstart(f \<circ> p) = f(pathstart p)"
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.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.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.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.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.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.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.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.251 +  qed auto
3.252  qed
3.254  lemma shiftpath_shiftpath:
3.255 @@ -1131,33 +1123,30 @@
3.256    by auto
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.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.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.305  subsection \<open>Special case of straight-line paths\<close>
3.306 @@ -1226,11 +1213,11 @@
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.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.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.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.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.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.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.406  subsubsection%unimportant \<open>Path components as sets\<close>
3.407 @@ -1479,7 +1457,7 @@
3.408    by (auto simp: path_component_def)
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.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.462  lemma connected_open_path_connected:
3.463 @@ -1676,7 +1646,7 @@
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.471  lemma path_connected_empty [simp]: "path_connected {}"
3.472 @@ -1691,23 +1661,35 @@
3.473    done
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.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.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.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.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.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.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.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.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.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.616 -    also have "... = norm ((2*r) *\<^sub>R b)"
3.617 +    also have "\<dots> = norm ((2*r) *\<^sub>R b)"
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.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.658  definition%important outside where
3.659 -  "outside s \<equiv> -s \<inter> {x. ~ bounded(connected_component_set (- s) x)}"
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.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.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.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.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.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.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.689 -lemma inside_outside: "inside s = (- (s \<union> outside s))"
3.690 -  by (force simp add: inside_def outside)
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.696 +lemma outside_inside: "outside S = (- (S \<union> inside S))"
3.697    by (auto simp: inside_outside) (metis IntI equals0D outside_no_overlap)
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.703 -lemma union_with_outside: "s \<union> outside s = - inside s"
3.704 +lemma union_with_outside: "S \<union> outside S = - inside S"
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.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.715  lemma segment_bound_lemma:
3.716 @@ -2586,80 +2560,81 @@
3.717  qed
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.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.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.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.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.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.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.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.813  by (meson gt_ex leD le_less_linear less_imp_le order.trans)
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.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.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.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.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.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.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.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.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.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.959  lemma image_Pair_const: "(\<lambda>x. (x, c)) ` A = A \<times> {c}"
3.960 -  by (auto simp:)
3.961 +  by auto
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.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.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.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.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.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.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.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.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.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.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.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.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.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.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.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.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.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.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.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.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.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.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.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.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.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.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.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.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.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.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.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.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.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.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.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.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.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.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.1727 -    also have "... < norm y + (norm x - norm y) * 1"
3.1728 +    also have "\<dots> < norm y + (norm x - norm y) * 1"
3.1730        apply (rule mult_strict_left_mono)
3.1731        using nou \<open>0 < r\<close> yx
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.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.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