# HG changeset patch
# User paulson <lp15@cam.ac.uk>
# Date 1527369115 -3600
# Node ID 69d680e9496174d11862edf3645b514a7978a01d
# Parent  b9160ca067ae3a4e2254c0cad8257867da6b374d
tidying and reorganisation around Cauchy Integral Theorem

diff -r b9160ca067ae -r 69d680e94961 src/HOL/Analysis/Brouwer_Fixpoint.thy
--- a/src/HOL/Analysis/Brouwer_Fixpoint.thy	Sat May 26 10:11:11 2018 +0100
+++ b/src/HOL/Analysis/Brouwer_Fixpoint.thy	Sat May 26 22:11:55 2018 +0100
@@ -2036,7 +2036,8 @@
 by (simp add: continuous_on_id retraction)
 
 lemma retract_of_refl [iff]: "S retract_of S"
-  using continuous_on_id retract_of_def retraction_def by fastforce
+  unfolding retract_of_def retraction_def
+  using continuous_on_id by blast
 
 lemma retract_of_imp_subset:
    "S retract_of T \<Longrightarrow> S \<subseteq> T"
@@ -2047,8 +2048,7 @@
 by (auto simp: retract_of_def retraction_def)
 
 lemma retract_of_singleton [iff]: "({x} retract_of S) \<longleftrightarrow> x \<in> S"
-  using continuous_on_const
-  by (auto simp: retract_of_def retraction_def)
+  unfolding retract_of_def retraction_def by force
 
 lemma retraction_comp:
    "\<lbrakk>retraction S T f; retraction T U g\<rbrakk>
diff -r b9160ca067ae -r 69d680e94961 src/HOL/Analysis/Cauchy_Integral_Theorem.thy
--- a/src/HOL/Analysis/Cauchy_Integral_Theorem.thy	Sat May 26 10:11:11 2018 +0100
+++ b/src/HOL/Analysis/Cauchy_Integral_Theorem.thy	Sat May 26 22:11:55 2018 +0100
@@ -255,7 +255,7 @@
       by (simp add: \<open>finite S\<close>)
     show "g1 differentiable at x within {0..1}" if "x \<in> {0..1} - insert 1 (( * ) 2 ` S)" for x
     proof (rule_tac d="dist (x/2) (1/2)" in differentiable_transform_within)
-      have "g1 +++ g2 differentiable at (x / 2) within {0..1 / 2}"
+      have "g1 +++ g2 differentiable at (x / 2) within {0..1/2}"
         by (rule differentiable_subset [OF S [of "x/2"]] | use that in force)+
       then show "g1 +++ g2 \<circ> ( * ) (inverse 2) differentiable at x within {0..1}"
         by (auto intro: differentiable_chain_within)
@@ -288,7 +288,7 @@
         by (rule differentiable_chain_within differentiable_subset [OF S [of "(x+1)/2"]] | use x2 that in force)+
       then show "g1 +++ g2 \<circ> (\<lambda>x. (x+1) / 2) differentiable at x within {0..1}"
         by (auto intro: differentiable_chain_within)
-      show "(g1 +++ g2 \<circ> (\<lambda>x. (x + 1) / 2)) x' = g2 x'" if "x' \<in> {0..1}" "dist x' x < dist ((x + 1) / 2) (1 / 2)" for x'
+      show "(g1 +++ g2 \<circ> (\<lambda>x. (x + 1) / 2)) x' = g2 x'" if "x' \<in> {0..1}" "dist x' x < dist ((x + 1) / 2) (1/2)" for x'
       proof -
         have [simp]: "(2*x'+2)/2 = x'+1"
           by (simp add: divide_simps)
@@ -323,65 +323,78 @@
 definition C1_differentiable_on :: "(real \<Rightarrow> 'a::real_normed_vector) \<Rightarrow> real set \<Rightarrow> bool"
            (infix "C1'_differentiable'_on" 50)
   where
-  "f C1_differentiable_on s \<longleftrightarrow>
-   (\<exists>D. (\<forall>x \<in> s. (f has_vector_derivative (D x)) (at x)) \<and> continuous_on s D)"
+  "f C1_differentiable_on S \<longleftrightarrow>
+   (\<exists>D. (\<forall>x \<in> S. (f has_vector_derivative (D x)) (at x)) \<and> continuous_on S D)"
 
 lemma C1_differentiable_on_eq:
-    "f C1_differentiable_on s \<longleftrightarrow>
-     (\<forall>x \<in> s. f differentiable at x) \<and> continuous_on s (\<lambda>x. vector_derivative f (at x))"
-  unfolding C1_differentiable_on_def
-  apply safe
-  using differentiable_def has_vector_derivative_def apply blast
-  apply (erule continuous_on_eq)
-  using vector_derivative_at apply fastforce
-  using vector_derivative_works apply fastforce
-  done
+    "f C1_differentiable_on S \<longleftrightarrow>
+     (\<forall>x \<in> S. f differentiable at x) \<and> continuous_on S (\<lambda>x. vector_derivative f (at x))"
+     (is "?lhs = ?rhs")
+proof
+  assume ?lhs
+  then show ?rhs
+    unfolding C1_differentiable_on_def
+    by (metis (no_types, lifting) continuous_on_eq  differentiableI_vector vector_derivative_at)
+next
+  assume ?rhs
+  then show ?lhs
+    using C1_differentiable_on_def vector_derivative_works by fastforce
+qed
 
 lemma C1_differentiable_on_subset:
-  "f C1_differentiable_on t \<Longrightarrow> s \<subseteq> t \<Longrightarrow> f C1_differentiable_on s"
+  "f C1_differentiable_on T \<Longrightarrow> S \<subseteq> T \<Longrightarrow> f C1_differentiable_on S"
   unfolding C1_differentiable_on_def  continuous_on_eq_continuous_within
   by (blast intro:  continuous_within_subset)
 
 lemma C1_differentiable_compose:
-    "\<lbrakk>f C1_differentiable_on s; g C1_differentiable_on (f ` s);
-      \<And>x. finite (s \<inter> f-`{x})\<rbrakk>
-      \<Longrightarrow> (g o f) C1_differentiable_on s"
-  apply (simp add: C1_differentiable_on_eq, safe)
-   using differentiable_chain_at apply blast
-  apply (rule continuous_on_eq [of _ "\<lambda>x. vector_derivative f (at x) *\<^sub>R vector_derivative g (at (f x))"])
-   apply (rule Limits.continuous_on_scaleR, assumption)
-   apply (metis (mono_tags, lifting) continuous_on_eq continuous_at_imp_continuous_on continuous_on_compose differentiable_imp_continuous_within o_def)
-  by (simp add: vector_derivative_chain_at)
-
-lemma C1_diff_imp_diff: "f C1_differentiable_on s \<Longrightarrow> f differentiable_on s"
+  assumes fg: "f C1_differentiable_on S" "g C1_differentiable_on (f ` S)" and fin: "\<And>x. finite (S \<inter> f-`{x})"
+  shows "(g o f) C1_differentiable_on S"
+proof -
+  have "\<And>x. x \<in> S \<Longrightarrow> g \<circ> f differentiable at x"
+    by (meson C1_differentiable_on_eq assms differentiable_chain_at imageI)
+  moreover have "continuous_on S (\<lambda>x. vector_derivative (g \<circ> f) (at x))"
+  proof (rule continuous_on_eq [of _ "\<lambda>x. vector_derivative f (at x) *\<^sub>R vector_derivative g (at (f x))"])
+    show "continuous_on S (\<lambda>x. vector_derivative f (at x) *\<^sub>R vector_derivative g (at (f x)))"
+      using fg
+      apply (clarsimp simp add: C1_differentiable_on_eq)
+      apply (rule Limits.continuous_on_scaleR, assumption)
+      by (metis (mono_tags, lifting) continuous_at_imp_continuous_on continuous_on_compose continuous_on_cong differentiable_imp_continuous_within o_def)
+    show "\<And>x. x \<in> S \<Longrightarrow> vector_derivative f (at x) *\<^sub>R vector_derivative g (at (f x)) = vector_derivative (g \<circ> f) (at x)"
+      by (metis (mono_tags, hide_lams) C1_differentiable_on_eq fg imageI vector_derivative_chain_at)
+  qed
+  ultimately show ?thesis
+    by (simp add: C1_differentiable_on_eq)
+qed
+
+lemma C1_diff_imp_diff: "f C1_differentiable_on S \<Longrightarrow> f differentiable_on S"
   by (simp add: C1_differentiable_on_eq differentiable_at_imp_differentiable_on)
 
-lemma C1_differentiable_on_ident [simp, derivative_intros]: "(\<lambda>x. x) C1_differentiable_on s"
+lemma C1_differentiable_on_ident [simp, derivative_intros]: "(\<lambda>x. x) C1_differentiable_on S"
   by (auto simp: C1_differentiable_on_eq continuous_on_const)
 
-lemma C1_differentiable_on_const [simp, derivative_intros]: "(\<lambda>z. a) C1_differentiable_on s"
+lemma C1_differentiable_on_const [simp, derivative_intros]: "(\<lambda>z. a) C1_differentiable_on S"
   by (auto simp: C1_differentiable_on_eq continuous_on_const)
 
 lemma C1_differentiable_on_add [simp, derivative_intros]:
-  "f C1_differentiable_on s \<Longrightarrow> g C1_differentiable_on s \<Longrightarrow> (\<lambda>x. f x + g x) C1_differentiable_on s"
+  "f C1_differentiable_on S \<Longrightarrow> g C1_differentiable_on S \<Longrightarrow> (\<lambda>x. f x + g x) C1_differentiable_on S"
   unfolding C1_differentiable_on_eq  by (auto intro: continuous_intros)
 
 lemma C1_differentiable_on_minus [simp, derivative_intros]:
-  "f C1_differentiable_on s \<Longrightarrow> (\<lambda>x. - f x) C1_differentiable_on s"
+  "f C1_differentiable_on S \<Longrightarrow> (\<lambda>x. - f x) C1_differentiable_on S"
   unfolding C1_differentiable_on_eq  by (auto intro: continuous_intros)
 
 lemma C1_differentiable_on_diff [simp, derivative_intros]:
-  "f C1_differentiable_on s \<Longrightarrow> g C1_differentiable_on s \<Longrightarrow> (\<lambda>x. f x - g x) C1_differentiable_on s"
+  "f C1_differentiable_on S \<Longrightarrow> g C1_differentiable_on S \<Longrightarrow> (\<lambda>x. f x - g x) C1_differentiable_on S"
   unfolding C1_differentiable_on_eq  by (auto intro: continuous_intros)
 
 lemma C1_differentiable_on_mult [simp, derivative_intros]:
   fixes f g :: "real \<Rightarrow> 'a :: real_normed_algebra"
-  shows "f C1_differentiable_on s \<Longrightarrow> g C1_differentiable_on s \<Longrightarrow> (\<lambda>x. f x * g x) C1_differentiable_on s"
+  shows "f C1_differentiable_on S \<Longrightarrow> g C1_differentiable_on S \<Longrightarrow> (\<lambda>x. f x * g x) C1_differentiable_on S"
   unfolding C1_differentiable_on_eq
   by (auto simp: continuous_on_add continuous_on_mult continuous_at_imp_continuous_on differentiable_imp_continuous_within)
 
 lemma C1_differentiable_on_scaleR [simp, derivative_intros]:
-  "f C1_differentiable_on s \<Longrightarrow> g C1_differentiable_on s \<Longrightarrow> (\<lambda>x. f x *\<^sub>R g x) C1_differentiable_on s"
+  "f C1_differentiable_on S \<Longrightarrow> g C1_differentiable_on S \<Longrightarrow> (\<lambda>x. f x *\<^sub>R g x) C1_differentiable_on S"
   unfolding C1_differentiable_on_eq
   by (rule continuous_intros | simp add: continuous_at_imp_continuous_on differentiable_imp_continuous_within)+
 
@@ -390,10 +403,10 @@
            (infixr "piecewise'_C1'_differentiable'_on" 50)
   where "f piecewise_C1_differentiable_on i  \<equiv>
            continuous_on i f \<and>
-           (\<exists>s. finite s \<and> (f C1_differentiable_on (i - s)))"
+           (\<exists>S. finite S \<and> (f C1_differentiable_on (i - S)))"
 
 lemma C1_differentiable_imp_piecewise:
-    "f C1_differentiable_on s \<Longrightarrow> f piecewise_C1_differentiable_on s"
+    "f C1_differentiable_on S \<Longrightarrow> f piecewise_C1_differentiable_on S"
   by (auto simp: piecewise_C1_differentiable_on_def C1_differentiable_on_eq continuous_at_imp_continuous_on differentiable_imp_continuous_within)
 
 lemma piecewise_C1_imp_differentiable:
@@ -403,25 +416,38 @@
            intro: has_derivative_at_withinI)
 
 lemma piecewise_C1_differentiable_compose:
-    "\<lbrakk>f piecewise_C1_differentiable_on s; g piecewise_C1_differentiable_on (f ` s);
-      \<And>x. finite (s \<inter> f-`{x})\<rbrakk>
-      \<Longrightarrow> (g o f) piecewise_C1_differentiable_on s"
-  apply (simp add: piecewise_C1_differentiable_on_def, safe)
-  apply (blast intro: continuous_on_compose2)
-  apply (rename_tac A B)
-  apply (rule_tac x="A \<union> (\<Union>x\<in>B. s \<inter> f-`{x})" in exI)
-  apply (rule conjI, blast)
-  apply (rule C1_differentiable_compose)
-  apply (blast intro: C1_differentiable_on_subset)
-  apply (blast intro: C1_differentiable_on_subset)
-  by (simp add: Diff_Int_distrib2)
+  assumes fg: "f piecewise_C1_differentiable_on S" "g piecewise_C1_differentiable_on (f ` S)" and fin: "\<And>x. finite (S \<inter> f-`{x})"
+  shows "(g o f) piecewise_C1_differentiable_on S"
+proof -
+  have "continuous_on S (\<lambda>x. g (f x))"
+    by (metis continuous_on_compose2 fg order_refl piecewise_C1_differentiable_on_def)
+  moreover have "\<exists>T. finite T \<and> g \<circ> f C1_differentiable_on S - T"
+  proof -
+    obtain F where "finite F" and F: "f C1_differentiable_on S - F" and f: "f piecewise_C1_differentiable_on S"
+      using fg by (auto simp: piecewise_C1_differentiable_on_def)
+    obtain G where "finite G" and G: "g C1_differentiable_on f ` S - G" and g: "g piecewise_C1_differentiable_on f ` S"
+      using fg by (auto simp: piecewise_C1_differentiable_on_def)
+    show ?thesis
+    proof (intro exI conjI)
+      show "finite (F \<union> (\<Union>x\<in>G. S \<inter> f-`{x}))"
+        using fin by (auto simp only: Int_Union \<open>finite F\<close> \<open>finite G\<close> finite_UN finite_imageI)
+      show "g \<circ> f C1_differentiable_on S - (F \<union> (\<Union>x\<in>G. S \<inter> f -` {x}))"
+        apply (rule C1_differentiable_compose)
+          apply (blast intro: C1_differentiable_on_subset [OF F])
+          apply (blast intro: C1_differentiable_on_subset [OF G])
+        by (simp add:  C1_differentiable_on_subset G Diff_Int_distrib2 fin)
+    qed
+  qed
+  ultimately show ?thesis
+    by (simp add: piecewise_C1_differentiable_on_def)
+qed
 
 lemma piecewise_C1_differentiable_on_subset:
-    "f piecewise_C1_differentiable_on s \<Longrightarrow> t \<le> s \<Longrightarrow> f piecewise_C1_differentiable_on t"
+    "f piecewise_C1_differentiable_on S \<Longrightarrow> T \<le> S \<Longrightarrow> f piecewise_C1_differentiable_on T"
   by (auto simp: piecewise_C1_differentiable_on_def elim!: continuous_on_subset C1_differentiable_on_subset)
 
 lemma C1_differentiable_imp_continuous_on:
-  "f C1_differentiable_on s \<Longrightarrow> continuous_on s f"
+  "f C1_differentiable_on S \<Longrightarrow> continuous_on S f"
   unfolding C1_differentiable_on_eq continuous_on_eq_continuous_within
   using differentiable_at_withinI differentiable_imp_continuous_within by blast
 
@@ -431,19 +457,19 @@
 
 lemma piecewise_C1_differentiable_affine:
   fixes m::real
-  assumes "f piecewise_C1_differentiable_on ((\<lambda>x. m * x + c) ` s)"
-  shows "(f o (\<lambda>x. m *\<^sub>R x + c)) piecewise_C1_differentiable_on s"
+  assumes "f piecewise_C1_differentiable_on ((\<lambda>x. m * x + c) ` S)"
+  shows "(f o (\<lambda>x. m *\<^sub>R x + c)) piecewise_C1_differentiable_on S"
 proof (cases "m = 0")
   case True
   then show ?thesis
     unfolding o_def by (auto simp: piecewise_C1_differentiable_on_def continuous_on_const)
 next
   case False
+  have *: "\<And>x. finite (S \<inter> {y. m * y + c = x})"
+    using False not_finite_existsD by fastforce 
   show ?thesis
     apply (rule piecewise_C1_differentiable_compose [OF C1_differentiable_imp_piecewise])
-    apply (rule assms derivative_intros | simp add: False vimage_def)+
-    using real_vector_affinity_eq [OF False, where c=c, unfolded scaleR_conv_of_real]
-    apply simp
+    apply (rule * assms derivative_intros | simp add: False vimage_def)+
     done
 qed
 
@@ -454,13 +480,13 @@
            "a \<le> c" "c \<le> b" "f c = g c"
   shows "(\<lambda>x. if x \<le> c then f x else g x) piecewise_C1_differentiable_on {a..b}"
 proof -
-  obtain s t where st: "f C1_differentiable_on ({a..c} - s)"
-                       "g C1_differentiable_on ({c..b} - t)"
-                       "finite s" "finite t"
+  obtain S T where st: "f C1_differentiable_on ({a..c} - S)"
+                       "g C1_differentiable_on ({c..b} - T)"
+                       "finite S" "finite T"
     using assms
     by (force simp: piecewise_C1_differentiable_on_def)
-  then have f_diff: "f differentiable_on {a..<c} - s"
-        and g_diff: "g differentiable_on {c<..b} - t"
+  then have f_diff: "f differentiable_on {a..<c} - S"
+        and g_diff: "g differentiable_on {c<..b} - T"
     by (simp_all add: C1_differentiable_on_eq differentiable_at_withinI differentiable_on_def)
   have "continuous_on {a..c} f" "continuous_on {c..b} g"
     using assms piecewise_C1_differentiable_on_def by auto
@@ -470,7 +496,7 @@
                                of f g "\<lambda>x. x\<le>c"]  assms
     by (force simp: ivl_disj_un_two_touch)
   { fix x
-    assume x: "x \<in> {a..b} - insert c (s \<union> t)"
+    assume x: "x \<in> {a..b} - insert c (S \<union> T)"
     have "(\<lambda>x. if x \<le> c then f x else g x) differentiable at x" (is "?diff_fg")
     proof (cases x c rule: le_cases)
       case le show ?diff_fg
@@ -482,48 +508,61 @@
         using dist_nz x dist_real_def ge st x by (auto simp: C1_differentiable_on_eq)
     qed
   }
-  then have "(\<forall>x \<in> {a..b} - insert c (s \<union> t). (\<lambda>x. if x \<le> c then f x else g x) differentiable at x)"
+  then have "(\<forall>x \<in> {a..b} - insert c (S \<union> T). (\<lambda>x. if x \<le> c then f x else g x) differentiable at x)"
     by auto
   moreover
-  { assume fcon: "continuous_on ({a<..<c} - s) (\<lambda>x. vector_derivative f (at x))"
-       and gcon: "continuous_on ({c<..<b} - t) (\<lambda>x. vector_derivative g (at x))"
-    have "open ({a<..<c} - s)"  "open ({c<..<b} - t)"
+  { assume fcon: "continuous_on ({a<..<c} - S) (\<lambda>x. vector_derivative f (at x))"
+       and gcon: "continuous_on ({c<..<b} - T) (\<lambda>x. vector_derivative g (at x))"
+    have "open ({a<..<c} - S)"  "open ({c<..<b} - T)"
       using st by (simp_all add: open_Diff finite_imp_closed)
-    moreover have "continuous_on ({a<..<c} - s) (\<lambda>x. vector_derivative (\<lambda>x. if x \<le> c then f x else g x) (at x))"
-      apply (rule continuous_on_eq [OF fcon])
-      apply (simp add:)
-      apply (rule vector_derivative_at [symmetric])
-      apply (rule_tac f=f and d="dist x c" in has_vector_derivative_transform_within)
-      apply (simp_all add: dist_norm vector_derivative_works [symmetric])
-      apply (metis (full_types) C1_differentiable_on_eq Diff_iff Groups.add_ac(2) add_mono_thms_linordered_field(5) atLeastAtMost_iff linorder_not_le order_less_irrefl st(1))
-      apply auto
-      done
-    moreover have "continuous_on ({c<..<b} - t) (\<lambda>x. vector_derivative (\<lambda>x. if x \<le> c then f x else g x) (at x))"
-      apply (rule continuous_on_eq [OF gcon])
-      apply (simp add:)
-      apply (rule vector_derivative_at [symmetric])
-      apply (rule_tac f=g and d="dist x c" in has_vector_derivative_transform_within)
-      apply (simp_all add: dist_norm vector_derivative_works [symmetric])
-      apply (metis (full_types) C1_differentiable_on_eq Diff_iff Groups.add_ac(2) add_mono_thms_linordered_field(5) atLeastAtMost_iff less_irrefl not_le st(2))
-      apply auto
-      done
-    ultimately have "continuous_on ({a<..<b} - insert c (s \<union> t))
+    moreover have "continuous_on ({a<..<c} - S) (\<lambda>x. vector_derivative (\<lambda>x. if x \<le> c then f x else g x) (at x))"
+    proof -
+      have "((\<lambda>x. if x \<le> c then f x else g x) has_vector_derivative vector_derivative f (at x))            (at x)"
+        if "a < x" "x < c" "x \<notin> S" for x
+      proof -
+        have f: "f differentiable at x"
+          by (meson C1_differentiable_on_eq Diff_iff atLeastAtMost_iff less_eq_real_def st(1) that)
+        show ?thesis
+          using that
+          apply (rule_tac f=f and d="dist x c" in has_vector_derivative_transform_within)
+             apply (auto simp add: dist_norm vector_derivative_works [symmetric] f)
+          done
+      qed
+      then show ?thesis
+        by (metis (no_types, lifting) continuous_on_eq [OF fcon] DiffE greaterThanLessThan_iff vector_derivative_at)
+    qed
+    moreover have "continuous_on ({c<..<b} - T) (\<lambda>x. vector_derivative (\<lambda>x. if x \<le> c then f x else g x) (at x))"
+    proof -
+      have "((\<lambda>x. if x \<le> c then f x else g x) has_vector_derivative vector_derivative g (at x))            (at x)"
+        if "c < x" "x < b" "x \<notin> T" for x
+      proof -
+        have g: "g differentiable at x"
+          by (metis C1_differentiable_on_eq DiffD1 DiffI atLeastAtMost_diff_ends greaterThanLessThan_iff st(2) that)
+        show ?thesis
+          using that
+          apply (rule_tac f=g and d="dist x c" in has_vector_derivative_transform_within)
+             apply (auto simp add: dist_norm vector_derivative_works [symmetric] g)
+          done
+      qed
+      then show ?thesis
+        by (metis (no_types, lifting) continuous_on_eq [OF gcon] DiffE greaterThanLessThan_iff vector_derivative_at)
+    qed
+    ultimately have "continuous_on ({a<..<b} - insert c (S \<union> T))
         (\<lambda>x. vector_derivative (\<lambda>x. if x \<le> c then f x else g x) (at x))"
-      apply (rule continuous_on_subset [OF continuous_on_open_Un], auto)
-      done
+      by (rule continuous_on_subset [OF continuous_on_open_Un], auto)
   } note * = this
-  have "continuous_on ({a<..<b} - insert c (s \<union> t)) (\<lambda>x. vector_derivative (\<lambda>x. if x \<le> c then f x else g x) (at x))"
+  have "continuous_on ({a<..<b} - insert c (S \<union> T)) (\<lambda>x. vector_derivative (\<lambda>x. if x \<le> c then f x else g x) (at x))"
     using st
     by (auto simp: C1_differentiable_on_eq elim!: continuous_on_subset intro: *)
-  ultimately have "\<exists>s. finite s \<and> ((\<lambda>x. if x \<le> c then f x else g x) C1_differentiable_on {a..b} - s)"
-    apply (rule_tac x="{a,b,c} \<union> s \<union> t" in exI)
+  ultimately have "\<exists>S. finite S \<and> ((\<lambda>x. if x \<le> c then f x else g x) C1_differentiable_on {a..b} - S)"
+    apply (rule_tac x="{a,b,c} \<union> S \<union> T" in exI)
     using st  by (auto simp: C1_differentiable_on_eq elim!: continuous_on_subset)
   with cab show ?thesis
     by (simp add: piecewise_C1_differentiable_on_def)
 qed
 
 lemma piecewise_C1_differentiable_neg:
-    "f piecewise_C1_differentiable_on s \<Longrightarrow> (\<lambda>x. -(f x)) piecewise_C1_differentiable_on s"
+    "f piecewise_C1_differentiable_on S \<Longrightarrow> (\<lambda>x. -(f x)) piecewise_C1_differentiable_on S"
   unfolding piecewise_C1_differentiable_on_def
   by (auto intro!: continuous_on_minus C1_differentiable_on_minus)
 
@@ -532,11 +571,11 @@
           "g piecewise_C1_differentiable_on i"
     shows "(\<lambda>x. f x + g x) piecewise_C1_differentiable_on i"
 proof -
-  obtain s t where st: "finite s" "finite t"
-                       "f C1_differentiable_on (i-s)"
+  obtain S t where st: "finite S" "finite t"
+                       "f C1_differentiable_on (i-S)"
                        "g C1_differentiable_on (i-t)"
     using assms by (auto simp: piecewise_C1_differentiable_on_def)
-  then have "finite (s \<union> t) \<and> (\<lambda>x. f x + g x) C1_differentiable_on i - (s \<union> t)"
+  then have "finite (S \<union> t) \<and> (\<lambda>x. f x + g x) C1_differentiable_on i - (S \<union> t)"
     by (auto intro: C1_differentiable_on_add elim!: C1_differentiable_on_subset)
   moreover have "continuous_on i f" "continuous_on i g"
     using assms piecewise_C1_differentiable_on_def by auto
@@ -545,8 +584,8 @@
 qed
 
 lemma piecewise_C1_differentiable_diff:
-    "\<lbrakk>f piecewise_C1_differentiable_on s;  g piecewise_C1_differentiable_on s\<rbrakk>
-     \<Longrightarrow> (\<lambda>x. f x - g x) piecewise_C1_differentiable_on s"
+    "\<lbrakk>f piecewise_C1_differentiable_on S;  g piecewise_C1_differentiable_on S\<rbrakk>
+     \<Longrightarrow> (\<lambda>x. f x - g x) piecewise_C1_differentiable_on S"
   unfolding diff_conv_add_uminus
   by (metis piecewise_C1_differentiable_add piecewise_C1_differentiable_neg)
 
@@ -555,44 +594,53 @@
   assumes "(g1 +++ g2) piecewise_C1_differentiable_on {0..1}"
     shows "g1 piecewise_C1_differentiable_on {0..1}"
 proof -
-  obtain s where "finite s"
-             and co12: "continuous_on ({0..1} - s) (\<lambda>x. vector_derivative (g1 +++ g2) (at x))"
-             and g12D: "\<forall>x\<in>{0..1} - s. g1 +++ g2 differentiable at x"
+  obtain S where "finite S"
+             and co12: "continuous_on ({0..1} - S) (\<lambda>x. vector_derivative (g1 +++ g2) (at x))"
+             and g12D: "\<forall>x\<in>{0..1} - S. g1 +++ g2 differentiable at x"
     using assms  by (auto simp: piecewise_C1_differentiable_on_def C1_differentiable_on_eq)
-  then have g1D: "g1 differentiable at x" if "x \<in> {0..1} - insert 1 (( * ) 2 ` s)" for x
-    apply (rule_tac d="dist (x/2) (1/2)" and f = "(g1 +++ g2) o (( * )(inverse 2))" in differentiable_transform_within)
-    using that
-    apply (simp_all add: dist_real_def joinpaths_def)
-    apply (rule differentiable_chain_at derivative_intros | force)+
-    done
+  have g1D: "g1 differentiable at x" if "x \<in> {0..1} - insert 1 (( * ) 2 ` S)" for x
+  proof (rule differentiable_transform_within)
+    show "g1 +++ g2 \<circ> ( * ) (inverse 2) differentiable at x"
+      using that g12D 
+      apply (simp only: joinpaths_def)
+      by (rule differentiable_chain_at derivative_intros | force)+
+    show "\<And>x'. \<lbrakk>dist x' x < dist (x/2) (1/2)\<rbrakk>
+          \<Longrightarrow> (g1 +++ g2 \<circ> ( * ) (inverse 2)) x' = g1 x'"
+      using that by (auto simp add: dist_real_def joinpaths_def)
+  qed (use that in \<open>auto simp: dist_real_def\<close>)
   have [simp]: "vector_derivative (g1 \<circ> ( * ) 2) (at (x/2)) = 2 *\<^sub>R vector_derivative g1 (at x)"
-               if "x \<in> {0..1} - insert 1 (( * ) 2 ` s)" for x
+               if "x \<in> {0..1} - insert 1 (( * ) 2 ` S)" for x
     apply (subst vector_derivative_chain_at)
     using that
     apply (rule derivative_eq_intros g1D | simp)+
     done
-  have "continuous_on ({0..1/2} - insert (1/2) s) (\<lambda>x. vector_derivative (g1 +++ g2) (at x))"
+  have "continuous_on ({0..1/2} - insert (1/2) S) (\<lambda>x. vector_derivative (g1 +++ g2) (at x))"
     using co12 by (rule continuous_on_subset) force
-  then have coDhalf: "continuous_on ({0..1/2} - insert (1/2) s) (\<lambda>x. vector_derivative (g1 o ( * )2) (at x))"
-    apply (rule continuous_on_eq [OF _ vector_derivative_at])
-    apply (rule_tac f="g1 o ( * )2" and d="dist x (1/2)" in has_vector_derivative_transform_within)
-    apply (simp_all add: dist_norm joinpaths_def vector_derivative_works [symmetric])
-    apply (force intro: g1D differentiable_chain_at)
-    apply auto
-    done
-  have "continuous_on ({0..1} - insert 1 (( * ) 2 ` s))
+  then have coDhalf: "continuous_on ({0..1/2} - insert (1/2) S) (\<lambda>x. vector_derivative (g1 o ( * )2) (at x))"
+  proof (rule continuous_on_eq [OF _ vector_derivative_at])
+    show "(g1 +++ g2 has_vector_derivative vector_derivative (g1 \<circ> ( * ) 2) (at x)) (at x)"
+      if "x \<in> {0..1/2} - insert (1/2) S" for x
+    proof (rule has_vector_derivative_transform_within)
+      show "(g1 \<circ> ( * ) 2 has_vector_derivative vector_derivative (g1 \<circ> ( * ) 2) (at x)) (at x)"
+        using that
+        by (force intro: g1D differentiable_chain_at simp: vector_derivative_works [symmetric])
+      show "\<And>x'. \<lbrakk>dist x' x < dist x (1/2)\<rbrakk> \<Longrightarrow> (g1 \<circ> ( * ) 2) x' = (g1 +++ g2) x'"
+        using that by (auto simp: dist_norm joinpaths_def)
+    qed (use that in \<open>auto simp: dist_norm\<close>)
+  qed
+  have "continuous_on ({0..1} - insert 1 (( * ) 2 ` S))
                       ((\<lambda>x. 1/2 * vector_derivative (g1 o ( * )2) (at x)) o ( * )(1/2))"
     apply (rule continuous_intros)+
     using coDhalf
     apply (simp add: scaleR_conv_of_real image_set_diff image_image)
     done
-  then have con_g1: "continuous_on ({0..1} - insert 1 (( * ) 2 ` s)) (\<lambda>x. vector_derivative g1 (at x))"
+  then have con_g1: "continuous_on ({0..1} - insert 1 (( * ) 2 ` S)) (\<lambda>x. vector_derivative g1 (at x))"
     by (rule continuous_on_eq) (simp add: scaleR_conv_of_real)
   have "continuous_on {0..1} g1"
     using continuous_on_joinpaths_D1 assms piecewise_C1_differentiable_on_def by blast
-  with \<open>finite s\<close> show ?thesis
+  with \<open>finite S\<close> show ?thesis
     apply (clarsimp simp add: piecewise_C1_differentiable_on_def C1_differentiable_on_eq)
-    apply (rule_tac x="insert 1 ((( * )2)`s)" in exI)
+    apply (rule_tac x="insert 1 ((( * )2)`S)" in exI)
     apply (simp add: g1D con_g1)
   done
 qed
@@ -602,44 +650,53 @@
   assumes "(g1 +++ g2) piecewise_C1_differentiable_on {0..1}" "pathfinish g1 = pathstart g2"
     shows "g2 piecewise_C1_differentiable_on {0..1}"
 proof -
-  obtain s where "finite s"
-             and co12: "continuous_on ({0..1} - s) (\<lambda>x. vector_derivative (g1 +++ g2) (at x))"
-             and g12D: "\<forall>x\<in>{0..1} - s. g1 +++ g2 differentiable at x"
+  obtain S where "finite S"
+             and co12: "continuous_on ({0..1} - S) (\<lambda>x. vector_derivative (g1 +++ g2) (at x))"
+             and g12D: "\<forall>x\<in>{0..1} - S. g1 +++ g2 differentiable at x"
     using assms  by (auto simp: piecewise_C1_differentiable_on_def C1_differentiable_on_eq)
-  then have g2D: "g2 differentiable at x" if "x \<in> {0..1} - insert 0 ((\<lambda>x. 2*x-1) ` s)" for x
-    apply (rule_tac d="dist ((x+1)/2) (1/2)" and f = "(g1 +++ g2) o (\<lambda>x. (x+1)/2)" in differentiable_transform_within)
-    using that
-    apply (simp_all add: dist_real_def joinpaths_def)
-    apply (auto simp: dist_real_def joinpaths_def field_simps)
-    apply (rule differentiable_chain_at derivative_intros | force)+
-    apply (drule_tac x= "(x+1) / 2" in bspec, force simp: divide_simps)
-    apply assumption
-    done
+  have g2D: "g2 differentiable at x" if "x \<in> {0..1} - insert 0 ((\<lambda>x. 2*x-1) ` S)" for x
+  proof (rule differentiable_transform_within)
+    show "g1 +++ g2 \<circ> (\<lambda>x. (x + 1) / 2) differentiable at x"
+      using g12D that
+      apply (simp only: joinpaths_def)
+      apply (drule_tac x= "(x+1) / 2" in bspec, force simp: divide_simps)
+      apply (rule differentiable_chain_at derivative_intros | force)+
+      done
+    show "\<And>x'. dist x' x < dist ((x + 1) / 2) (1/2) \<Longrightarrow> (g1 +++ g2 \<circ> (\<lambda>x. (x + 1) / 2)) x' = g2 x'"
+      using that by (auto simp: dist_real_def joinpaths_def field_simps)
+    qed (use that in \<open>auto simp: dist_norm\<close>)
   have [simp]: "vector_derivative (g2 \<circ> (\<lambda>x. 2*x-1)) (at ((x+1)/2)) = 2 *\<^sub>R vector_derivative g2 (at x)"
-               if "x \<in> {0..1} - insert 0 ((\<lambda>x. 2*x-1) ` s)" for x
+               if "x \<in> {0..1} - insert 0 ((\<lambda>x. 2*x-1) ` S)" for x
     using that  by (auto simp: vector_derivative_chain_at divide_simps g2D)
-  have "continuous_on ({1/2..1} - insert (1/2) s) (\<lambda>x. vector_derivative (g1 +++ g2) (at x))"
+  have "continuous_on ({1/2..1} - insert (1/2) S) (\<lambda>x. vector_derivative (g1 +++ g2) (at x))"
     using co12 by (rule continuous_on_subset) force
-  then have coDhalf: "continuous_on ({1/2..1} - insert (1/2) s) (\<lambda>x. vector_derivative (g2 o (\<lambda>x. 2*x-1)) (at x))"
-    apply (rule continuous_on_eq [OF _ vector_derivative_at])
-    apply (rule_tac f="g2 o (\<lambda>x. 2*x-1)" and d="dist (3/4) ((x+1)/2)" in has_vector_derivative_transform_within)
-    apply (auto simp: dist_real_def field_simps joinpaths_def vector_derivative_works [symmetric]
-                intro!: g2D differentiable_chain_at)
-    done
-  have [simp]: "((\<lambda>x. (x+1) / 2) ` ({0..1} - insert 0 ((\<lambda>x. 2 * x - 1) ` s))) = ({1/2..1} - insert (1/2) s)"
+  then have coDhalf: "continuous_on ({1/2..1} - insert (1/2) S) (\<lambda>x. vector_derivative (g2 o (\<lambda>x. 2*x-1)) (at x))"
+  proof (rule continuous_on_eq [OF _ vector_derivative_at])
+    show "(g1 +++ g2 has_vector_derivative vector_derivative (g2 \<circ> (\<lambda>x. 2 * x - 1)) (at x))
+          (at x)"
+      if "x \<in> {1 / 2..1} - insert (1 / 2) S" for x
+    proof (rule_tac f="g2 o (\<lambda>x. 2*x-1)" and d="dist (3/4) ((x+1)/2)" in has_vector_derivative_transform_within)
+      show "(g2 \<circ> (\<lambda>x. 2 * x - 1) has_vector_derivative vector_derivative (g2 \<circ> (\<lambda>x. 2 * x - 1)) (at x))
+            (at x)"
+        using that by (force intro: g2D differentiable_chain_at simp: vector_derivative_works [symmetric])
+      show "\<And>x'. \<lbrakk>dist x' x < dist (3 / 4) ((x + 1) / 2)\<rbrakk> \<Longrightarrow> (g2 \<circ> (\<lambda>x. 2 * x - 1)) x' = (g1 +++ g2) x'"
+        using that by (auto simp: dist_norm joinpaths_def add_divide_distrib)
+    qed (use that in \<open>auto simp: dist_norm\<close>)
+  qed
+  have [simp]: "((\<lambda>x. (x+1) / 2) ` ({0..1} - insert 0 ((\<lambda>x. 2 * x - 1) ` S))) = ({1/2..1} - insert (1/2) S)"
     apply (simp add: image_set_diff inj_on_def image_image)
     apply (auto simp: image_affinity_atLeastAtMost_div add_divide_distrib)
     done
-  have "continuous_on ({0..1} - insert 0 ((\<lambda>x. 2*x-1) ` s))
+  have "continuous_on ({0..1} - insert 0 ((\<lambda>x. 2*x-1) ` S))
                       ((\<lambda>x. 1/2 * vector_derivative (g2 \<circ> (\<lambda>x. 2*x-1)) (at x)) o (\<lambda>x. (x+1)/2))"
     by (rule continuous_intros | simp add:  coDhalf)+
-  then have con_g2: "continuous_on ({0..1} - insert 0 ((\<lambda>x. 2*x-1) ` s)) (\<lambda>x. vector_derivative g2 (at x))"
+  then have con_g2: "continuous_on ({0..1} - insert 0 ((\<lambda>x. 2*x-1) ` S)) (\<lambda>x. vector_derivative g2 (at x))"
     by (rule continuous_on_eq) (simp add: scaleR_conv_of_real)
   have "continuous_on {0..1} g2"
     using continuous_on_joinpaths_D2 assms piecewise_C1_differentiable_on_def by blast
-  with \<open>finite s\<close> show ?thesis
+  with \<open>finite S\<close> show ?thesis
     apply (clarsimp simp add: piecewise_C1_differentiable_on_def C1_differentiable_on_eq)
-    apply (rule_tac x="insert 0 ((\<lambda>x. 2 * x - 1) ` s)" in exI)
+    apply (rule_tac x="insert 0 ((\<lambda>x. 2 * x - 1) ` S)" in exI)
     apply (simp add: g2D con_g2)
   done
 qed
@@ -675,32 +732,32 @@
       and con: "continuous_on (path_image g) (deriv f)"
     shows "valid_path (f o g)"
 proof -
-  obtain s where "finite s" and g_diff: "g C1_differentiable_on {0..1} - s"
+  obtain S where "finite S" and g_diff: "g C1_differentiable_on {0..1} - S"
     using \<open>valid_path g\<close> unfolding valid_path_def piecewise_C1_differentiable_on_def by auto
-  have "f \<circ> g differentiable at t" when "t\<in>{0..1} - s" for t
+  have "f \<circ> g differentiable at t" when "t\<in>{0..1} - S" for t
     proof (rule differentiable_chain_at)
       show "g differentiable at t" using \<open>valid_path g\<close>
-        by (meson C1_differentiable_on_eq \<open>g C1_differentiable_on {0..1} - s\<close> that)
+        by (meson C1_differentiable_on_eq \<open>g C1_differentiable_on {0..1} - S\<close> that)
     next
       have "g t\<in>path_image g" using that DiffD1 image_eqI path_image_def by metis
       then show "f differentiable at (g t)" 
         using der[THEN field_differentiable_imp_differentiable] by auto
     qed
-  moreover have "continuous_on ({0..1} - s) (\<lambda>x. vector_derivative (f \<circ> g) (at x))"
+  moreover have "continuous_on ({0..1} - S) (\<lambda>x. vector_derivative (f \<circ> g) (at x))"
     proof (rule continuous_on_eq [where f = "\<lambda>x. vector_derivative g (at x) * deriv f (g x)"],
         rule continuous_intros)
-      show "continuous_on ({0..1} - s) (\<lambda>x. vector_derivative g (at x))"
+      show "continuous_on ({0..1} - S) (\<lambda>x. vector_derivative g (at x))"
         using g_diff C1_differentiable_on_eq by auto
     next
       have "continuous_on {0..1} (\<lambda>x. deriv f (g x))"
         using continuous_on_compose[OF _ con[unfolded path_image_def],unfolded comp_def]
           \<open>valid_path g\<close> piecewise_C1_differentiable_on_def valid_path_def
         by blast
-      then show "continuous_on ({0..1} - s) (\<lambda>x. deriv f (g x))"
+      then show "continuous_on ({0..1} - S) (\<lambda>x. deriv f (g x))"
         using continuous_on_subset by blast
     next
       show "vector_derivative g (at t) * deriv f (g t) = vector_derivative (f \<circ> g) (at t)"
-          when "t \<in> {0..1} - s" for t
+          when "t \<in> {0..1} - S" for t
         proof (rule vector_derivative_chain_at_general[symmetric])
           show "g differentiable at t" by (meson C1_differentiable_on_eq g_diff that)
         next
@@ -708,14 +765,14 @@
           then show "f field_differentiable at (g t)" using der by auto
         qed
     qed
-  ultimately have "f o g C1_differentiable_on {0..1} - s"
+  ultimately have "f o g C1_differentiable_on {0..1} - S"
     using C1_differentiable_on_eq by blast
   moreover have "path (f \<circ> g)" 
     apply (rule path_continuous_image[OF valid_path_imp_path[OF \<open>valid_path g\<close>]])
     using der
     by (simp add: continuous_at_imp_continuous_on field_differentiable_imp_continuous_at)
   ultimately show ?thesis unfolding valid_path_def piecewise_C1_differentiable_on_def path_def
-    using \<open>finite s\<close> by auto
+    using \<open>finite S\<close> by auto
 qed
 
 
@@ -763,24 +820,17 @@
 lemma has_contour_integral_integrable: "(f has_contour_integral i) g \<Longrightarrow> f contour_integrable_on g"
   using contour_integrable_on_def by blast
 
-(* Show that we can forget about the localized derivative.*)
-
-lemma vector_derivative_within_interior:
-     "\<lbrakk>x \<in> interior s; NO_MATCH UNIV s\<rbrakk>
-      \<Longrightarrow> vector_derivative f (at x within s) = vector_derivative f (at x)"
-  apply (simp add: vector_derivative_def has_vector_derivative_def has_derivative_def netlimit_within_interior)
-  apply (subst lim_within_interior, auto)
-  done
+subsubsection\<open>Show that we can forget about the localized derivative.\<close>
 
 lemma has_integral_localized_vector_derivative:
     "((\<lambda>x. f (g x) * vector_derivative g (at x within {a..b})) has_integral i) {a..b} \<longleftrightarrow>
      ((\<lambda>x. f (g x) * vector_derivative g (at x)) has_integral i) {a..b}"
 proof -
-  have "{a..b} - {a,b} = interior {a..b}"
+  have *: "{a..b} - {a,b} = interior {a..b}"
     by (simp add: atLeastAtMost_diff_ends)
   show ?thesis
     apply (rule has_integral_spike_eq [of "{a,b}"])
-    apply (auto simp: vector_derivative_within_interior)
+    apply (auto simp: at_within_interior [of _ "{a..b}"])
     done
 qed
 
@@ -805,17 +855,16 @@
   assumes "valid_path g"
     shows "valid_path(reversepath g)"
 proof -
-  obtain s where "finite s" "g C1_differentiable_on ({0..1} - s)"
+  obtain S where "finite S" and S: "g C1_differentiable_on ({0..1} - S)"
     using assms by (auto simp: valid_path_def piecewise_C1_differentiable_on_def)
-  then have "finite ((-) 1 ` s)" "(reversepath g C1_differentiable_on ({0..1} - (-) 1 ` s))"
-    apply (auto simp: reversepath_def)
+  then have "finite ((-) 1 ` S)"
+    by auto
+  moreover have "(reversepath g C1_differentiable_on ({0..1} - (-) 1 ` S))"
+    unfolding reversepath_def
     apply (rule C1_differentiable_compose [of "\<lambda>x::real. 1-x" _ g, unfolded o_def])
-    apply (auto simp: C1_differentiable_on_eq)
-    apply (rule continuous_intros, force)
-    apply (force elim!: continuous_on_subset)
-    apply (simp add: finite_vimageI inj_on_def)
-    done
-  then show ?thesis using assms
+    using S
+    by (force simp: finite_vimageI inj_on_def C1_differentiable_on_eq continuous_on_const elim!: continuous_on_subset)+
+  ultimately show ?thesis using assms
     by (auto simp: valid_path_def piecewise_C1_differentiable_on_def path_def [symmetric])
 qed
 
@@ -823,38 +872,37 @@
   using valid_path_imp_reverse by force
 
 lemma has_contour_integral_reversepath:
-  assumes "valid_path g" "(f has_contour_integral i) g"
+  assumes "valid_path g" and f: "(f has_contour_integral i) g"
     shows "(f has_contour_integral (-i)) (reversepath g)"
 proof -
-  { fix s x
-    assume xs: "g C1_differentiable_on ({0..1} - s)" "x \<notin> (-) 1 ` s" "0 \<le> x" "x \<le> 1"
-      have "vector_derivative (\<lambda>x. g (1 - x)) (at x within {0..1}) =
+  { fix S x
+    assume xs: "g C1_differentiable_on ({0..1} - S)" "x \<notin> (-) 1 ` S" "0 \<le> x" "x \<le> 1"
+    have "vector_derivative (\<lambda>x. g (1 - x)) (at x within {0..1}) =
             - vector_derivative g (at (1 - x) within {0..1})"
-      proof -
-        obtain f' where f': "(g has_vector_derivative f') (at (1 - x))"
-          using xs
-          by (force simp: has_vector_derivative_def C1_differentiable_on_def)
-        have "(g o (\<lambda>x. 1 - x) has_vector_derivative -1 *\<^sub>R f') (at x)"
-          apply (rule vector_diff_chain_within)
-          apply (intro vector_diff_chain_within derivative_eq_intros | simp)+
-          apply (rule has_vector_derivative_at_within [OF f'])
-          done
-        then have mf': "((\<lambda>x. g (1 - x)) has_vector_derivative -f') (at x)"
-          by (simp add: o_def)
-        show ?thesis
-          using xs
-          by (auto simp: vector_derivative_at_within_ivl [OF mf'] vector_derivative_at_within_ivl [OF f'])
-      qed
+    proof -
+      obtain f' where f': "(g has_vector_derivative f') (at (1 - x))"
+        using xs
+        by (force simp: has_vector_derivative_def C1_differentiable_on_def)
+      have "(g o (\<lambda>x. 1 - x) has_vector_derivative -1 *\<^sub>R f') (at x)"
+        by (intro vector_diff_chain_within has_vector_derivative_at_within [OF f'] derivative_eq_intros | simp)+
+      then have mf': "((\<lambda>x. g (1 - x)) has_vector_derivative -f') (at x)"
+        by (simp add: o_def)
+      show ?thesis
+        using xs
+        by (auto simp: vector_derivative_at_within_ivl [OF mf'] vector_derivative_at_within_ivl [OF f'])
+    qed
   } note * = this
-  have 01: "{0..1::real} = cbox 0 1"
-    by simp
-  show ?thesis using assms
-    apply (auto simp: has_contour_integral_def)
-    apply (drule has_integral_affinity01 [where m= "-1" and c=1])
-    apply (auto simp: reversepath_def valid_path_def piecewise_C1_differentiable_on_def)
-    apply (drule has_integral_neg)
-    apply (rule_tac S = "(\<lambda>x. 1 - x) ` s" in has_integral_spike_finite)
-    apply (auto simp: *)
+  obtain S where S: "continuous_on {0..1} g" "finite S" "g C1_differentiable_on {0..1} - S"
+    using assms by (auto simp: valid_path_def piecewise_C1_differentiable_on_def)
+  have "((\<lambda>x. - (f (g (1 - x)) * vector_derivative g (at (1 - x) within {0..1}))) has_integral -i)
+       {0..1}"
+    using has_integral_affinity01 [where m= "-1" and c=1, OF f [unfolded has_contour_integral_def]]
+    by (simp add: has_integral_neg)
+  then show ?thesis 
+    using S
+    apply (clarsimp simp: reversepath_def has_contour_integral_def)
+    apply (rule_tac S = "(\<lambda>x. 1 - x) ` S" in has_integral_spike_finite)
+      apply (auto simp: *)
     done
 qed
 
@@ -891,7 +939,6 @@
     apply (rule piecewise_C1_differentiable_compose)
     using assms
     apply (auto simp: valid_path_def piecewise_C1_differentiable_on_def continuous_on_joinpaths)
-    apply (rule continuous_intros | simp)+
     apply (force intro: finite_vimageI [where h = "( * )2"] inj_onI)
     done
   moreover have "(g2 o (\<lambda>x. 2*x-1)) piecewise_C1_differentiable_on {1/2..1}"
@@ -1179,7 +1226,7 @@
                       [where f = "(shiftpath (1 - a) (shiftpath a g))" and S = "{0<..<1}-s"]])
       using s g assms x
       apply (auto simp: finite_imp_closed open_Diff shiftpath_shiftpath
-                        vector_derivative_within_interior vector_derivative_works [symmetric])
+                        at_within_interior [of _ "{0..1}"] vector_derivative_works [symmetric])
       apply (rule differentiable_transform_within [OF gx, of "min x (1-x)"])
       apply (auto simp: dist_real_def shiftpath_shiftpath abs_if split: if_split_asm)
       done
@@ -1268,6 +1315,9 @@
 lemma has_contour_integral_trivial [iff]: "(f has_contour_integral 0) (linepath a a)"
   by (simp add: has_contour_integral_linepath)
 
+lemma has_contour_integral_trivial_iff [simp]: "(f has_contour_integral i) (linepath a a) \<longleftrightarrow> i=0"
+  using has_contour_integral_unique by blast
+
 lemma contour_integral_trivial [simp]: "contour_integral (linepath a a) f = 0"
   using has_contour_integral_trivial contour_integral_unique by blast
 
@@ -1738,11 +1788,7 @@
 proof (cases "k = 0 \<or> k = 1")
   case True
   then show ?thesis
-    using assms
-    apply auto
-    apply (metis add.left_neutral has_contour_integral_trivial has_contour_integral_unique)
-    apply (metis add.right_neutral has_contour_integral_trivial has_contour_integral_unique)
-    done
+    using assms by auto
 next
   case False
   then have k: "0 < k" "k < 1" "complex_of_real k \<noteq> 1"
@@ -1758,12 +1804,9 @@
       apply (simp add: real_vector.scale_left_distrib [symmetric] divide_simps)
       done
     have "((\<lambda>x. f ((1 - x) *\<^sub>R a + x *\<^sub>R b) * (b - a)) has_integral i) {0..k}"
-      using * k
-      apply -
-      apply (drule has_integral_affinity [of _ _ 0 "1::real" "inverse k" "0", simplified])
-      apply (simp_all add: divide_simps mult.commute [of _ "k"] image_affinity_atLeastAtMost ** c)
-      apply (drule has_integral_cmul [where c = "inverse k"])
-      apply (simp add: has_integral_cmul)
+      using k has_integral_affinity01 [OF *, of "inverse k" "0"]
+      apply (simp add: divide_simps mult.commute [of _ "k"] image_affinity_atLeastAtMost ** c)
+      apply (auto dest: has_integral_cmul [where c = "inverse k"])
       done
   } note fi = this
   { assume *: "((\<lambda>x. f ((1 - x) *\<^sub>R c + x *\<^sub>R b) * (b - c)) has_integral j) {0..1}"
@@ -1774,12 +1817,9 @@
       apply (simp add: field_simps)
       done
     have "((\<lambda>x. f ((1 - x) *\<^sub>R a + x *\<^sub>R b) * (b - a)) has_integral j) {k..1}"
-      using * k
-      apply -
-      apply (drule has_integral_affinity [of _ _ 0 "1::real" "inverse(1 - k)" "-(k/(1 - k))", simplified])
-      apply (simp_all add: divide_simps mult.commute [of _ "1-k"] image_affinity_atLeastAtMost ** bc)
-      apply (drule has_integral_cmul [where k = "(1 - k) *\<^sub>R j" and c = "inverse (1 - k)"])
-      apply (simp add: has_integral_cmul)
+      using k has_integral_affinity01 [OF *, of "inverse(1 - k)" "-(k/(1 - k))"]
+      apply (simp add: divide_simps mult.commute [of _ "1-k"] image_affinity_atLeastAtMost ** bc)
+      apply (auto dest: has_integral_cmul [where k = "(1 - k) *\<^sub>R j" and c = "inverse (1 - k)"])
       done
   } note fj = this
   show ?thesis
@@ -1836,7 +1876,7 @@
   using c
   by (auto simp: closed_segment_def algebra_simps intro!: contour_integral_split [OF f])
 
-(* The special case of midpoints used in the main quadrisection.*)
+text\<open>The special case of midpoints used in the main quadrisection\<close>
 
 lemma has_contour_integral_midpoint:
   assumes "(f has_contour_integral i) (linepath a (midpoint a b))"
@@ -5119,7 +5159,7 @@
 
 lemma circlepath_minus: "circlepath z (-r) x = circlepath z r (x + 1/2)"
 proof -
-  have "z + of_real r * exp (2 * pi * \<i> * (x + 1 / 2)) =
+  have "z + of_real r * exp (2 * pi * \<i> * (x + 1/2)) =
         z + of_real r * exp (2 * pi * \<i> * x + pi * \<i>)"
     by (simp add: divide_simps) (simp add: algebra_simps)
   also have "... = z - r * exp (2 * pi * \<i> * x)"
diff -r b9160ca067ae -r 69d680e94961 src/HOL/Analysis/Complex_Analysis_Basics.thy
--- a/src/HOL/Analysis/Complex_Analysis_Basics.thy	Sat May 26 10:11:11 2018 +0100
+++ b/src/HOL/Analysis/Complex_Analysis_Basics.thy	Sat May 26 22:11:55 2018 +0100
@@ -47,26 +47,6 @@
 lemma lambda_one: "(\<lambda>x::'a::monoid_mult. x) = ( * ) 1"
   by auto
 
-lemma continuous_mult_left:
-  fixes c::"'a::real_normed_algebra"
-  shows "continuous F f \<Longrightarrow> continuous F (\<lambda>x. c * f x)"
-by (rule continuous_mult [OF continuous_const])
-
-lemma continuous_mult_right:
-  fixes c::"'a::real_normed_algebra"
-  shows "continuous F f \<Longrightarrow> continuous F (\<lambda>x. f x * c)"
-by (rule continuous_mult [OF _ continuous_const])
-
-lemma continuous_on_mult_left:
-  fixes c::"'a::real_normed_algebra"
-  shows "continuous_on s f \<Longrightarrow> continuous_on s (\<lambda>x. c * f x)"
-by (rule continuous_on_mult [OF continuous_on_const])
-
-lemma continuous_on_mult_right:
-  fixes c::"'a::real_normed_algebra"
-  shows "continuous_on s f \<Longrightarrow> continuous_on s (\<lambda>x. f x * c)"
-by (rule continuous_on_mult [OF _ continuous_on_const])
-
 lemma uniformly_continuous_on_cmul_right [continuous_intros]:
   fixes f :: "'a::real_normed_vector \<Rightarrow> 'b::real_normed_algebra"
   shows "uniformly_continuous_on s f \<Longrightarrow> uniformly_continuous_on s (\<lambda>x. f x * c)"
diff -r b9160ca067ae -r 69d680e94961 src/HOL/Analysis/Path_Connected.thy
--- a/src/HOL/Analysis/Path_Connected.thy	Sat May 26 10:11:11 2018 +0100
+++ b/src/HOL/Analysis/Path_Connected.thy	Sat May 26 22:11:55 2018 +0100
@@ -8371,15 +8371,12 @@
                (\<forall>x \<in> sphere a r. g x = f x))"
          (is "?lhs = ?rhs")
 proof%unimportant (cases r "0::real" rule: linorder_cases)
-  case less
-  then show ?thesis by simp
-next
   case equal
-  with continuous_on_const show ?thesis
+  then show ?thesis
     apply (auto simp: homotopic_with)
     apply (rule_tac x="\<lambda>x. h (0, a)" in exI)
-    apply (fastforce simp add:)
-    done
+     apply (fastforce simp add:)
+    using continuous_on_const by blast
 next
   case greater
   let ?P = "continuous_on {x. norm(x - a) = r} f \<and> f ` {x. norm(x - a) = r} \<subseteq> S"
@@ -8494,6 +8491,6 @@
   qed
   ultimately
   show ?thesis by meson
-qed
+qed simp
 
 end
diff -r b9160ca067ae -r 69d680e94961 src/HOL/Limits.thy
--- a/src/HOL/Limits.thy	Sat May 26 10:11:11 2018 +0100
+++ b/src/HOL/Limits.thy	Sat May 26 22:11:55 2018 +0100
@@ -842,6 +842,32 @@
 lemmas tendsto_mult_right_zero =
   bounded_bilinear.tendsto_right_zero [OF bounded_bilinear_mult]
 
+
+lemma continuous_mult_left:
+  fixes c::"'a::real_normed_algebra"
+  shows "continuous F f \<Longrightarrow> continuous F (\<lambda>x. c * f x)"
+by (rule continuous_mult [OF continuous_const])
+
+lemma continuous_mult_right:
+  fixes c::"'a::real_normed_algebra"
+  shows "continuous F f \<Longrightarrow> continuous F (\<lambda>x. f x * c)"
+by (rule continuous_mult [OF _ continuous_const])
+
+lemma continuous_on_mult_left:
+  fixes c::"'a::real_normed_algebra"
+  shows "continuous_on s f \<Longrightarrow> continuous_on s (\<lambda>x. c * f x)"
+by (rule continuous_on_mult [OF continuous_on_const])
+
+lemma continuous_on_mult_right:
+  fixes c::"'a::real_normed_algebra"
+  shows "continuous_on s f \<Longrightarrow> continuous_on s (\<lambda>x. f x * c)"
+by (rule continuous_on_mult [OF _ continuous_on_const])
+
+lemma continuous_on_mult_const [simp]:
+  fixes c::"'a::real_normed_algebra"
+  shows "continuous_on s (( * ) c)"
+  by (intro continuous_on_mult_left continuous_on_id)
+
 lemma tendsto_divide_zero:
   fixes c :: "'a::real_normed_field"
   shows "(f \<longlongrightarrow> 0) F \<Longrightarrow> ((\<lambda>x. f x / c) \<longlongrightarrow> 0) F"
diff -r b9160ca067ae -r 69d680e94961 src/HOL/Topological_Spaces.thy
--- a/src/HOL/Topological_Spaces.thy	Sat May 26 10:11:11 2018 +0100
+++ b/src/HOL/Topological_Spaces.thy	Sat May 26 22:11:55 2018 +0100
@@ -1924,13 +1924,13 @@
     continuous_on (s \<union> t) (\<lambda>x. if P x then f x else g x)"
   by (rule continuous_on_If) auto
 
-lemma continuous_on_id[continuous_intros]: "continuous_on s (\<lambda>x. x)"
+lemma continuous_on_id[continuous_intros,simp]: "continuous_on s (\<lambda>x. x)"
   unfolding continuous_on_def by fast
 
-lemma continuous_on_id'[continuous_intros]: "continuous_on s id"
+lemma continuous_on_id'[continuous_intros,simp]: "continuous_on s id"
   unfolding continuous_on_def id_def by fast
 
-lemma continuous_on_const[continuous_intros]: "continuous_on s (\<lambda>x. c)"
+lemma continuous_on_const[continuous_intros,simp]: "continuous_on s (\<lambda>x. c)"
   unfolding continuous_on_def by auto
 
 lemma continuous_on_subset: "continuous_on s f \<Longrightarrow> t \<subseteq> s \<Longrightarrow> continuous_on t f"