# HG changeset patch
# User paulson <lp15@cam.ac.uk>
# Date 1527320169 -3600
# Node ID 5e4e006f9552666c7b814b72d68c42052c451f9e
# Parent  e2f235b9662adec53059657904ce0d93364a8514
tidied some proofs

diff -r e2f235b9662a -r 5e4e006f9552 src/HOL/Analysis/Cauchy_Integral_Theorem.thy
--- a/src/HOL/Analysis/Cauchy_Integral_Theorem.thy	Thu May 24 23:05:28 2018 +0100
+++ b/src/HOL/Analysis/Cauchy_Integral_Theorem.thy	Sat May 26 08:36:09 2018 +0100
@@ -91,14 +91,14 @@
            (infixr "piecewise'_differentiable'_on" 50)
   where "f piecewise_differentiable_on i  \<equiv>
            continuous_on i f \<and>
-           (\<exists>s. finite s \<and> (\<forall>x \<in> i - s. f differentiable (at x within i)))"
+           (\<exists>S. finite S \<and> (\<forall>x \<in> i - S. f differentiable (at x within i)))"
 
 lemma piecewise_differentiable_on_imp_continuous_on:
-    "f piecewise_differentiable_on s \<Longrightarrow> continuous_on s f"
+    "f piecewise_differentiable_on S \<Longrightarrow> continuous_on S f"
 by (simp add: piecewise_differentiable_on_def)
 
 lemma piecewise_differentiable_on_subset:
-    "f piecewise_differentiable_on s \<Longrightarrow> t \<le> s \<Longrightarrow> f piecewise_differentiable_on t"
+    "f piecewise_differentiable_on S \<Longrightarrow> T \<le> S \<Longrightarrow> f piecewise_differentiable_on T"
   using continuous_on_subset
   unfolding piecewise_differentiable_on_def
   apply safe
@@ -113,29 +113,29 @@
   done
 
 lemma differentiable_imp_piecewise_differentiable:
-    "(\<And>x. x \<in> s \<Longrightarrow> f differentiable (at x within s))
-         \<Longrightarrow> f piecewise_differentiable_on s"
+    "(\<And>x. x \<in> S \<Longrightarrow> f differentiable (at x within S))
+         \<Longrightarrow> f piecewise_differentiable_on S"
 by (auto simp: piecewise_differentiable_on_def differentiable_imp_continuous_on differentiable_on_def
          intro: differentiable_within_subset)
 
-lemma piecewise_differentiable_const [iff]: "(\<lambda>x. z) piecewise_differentiable_on s"
+lemma piecewise_differentiable_const [iff]: "(\<lambda>x. z) piecewise_differentiable_on S"
   by (simp add: differentiable_imp_piecewise_differentiable)
 
 lemma piecewise_differentiable_compose:
-    "\<lbrakk>f piecewise_differentiable_on s; g piecewise_differentiable_on (f ` s);
-      \<And>x. finite (s \<inter> f-`{x})\<rbrakk>
-      \<Longrightarrow> (g o f) piecewise_differentiable_on s"
+    "\<lbrakk>f piecewise_differentiable_on S; g piecewise_differentiable_on (f ` S);
+      \<And>x. finite (S \<inter> f-`{x})\<rbrakk>
+      \<Longrightarrow> (g o f) piecewise_differentiable_on S"
   apply (simp add: piecewise_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_tac x="A \<union> (\<Union>x\<in>B. S \<inter> f-`{x})" in exI)
   apply (blast intro!: differentiable_chain_within)
   done
 
 lemma piecewise_differentiable_affine:
   fixes m::real
-  assumes "f piecewise_differentiable_on ((\<lambda>x. m *\<^sub>R x + c) ` s)"
-  shows "(f o (\<lambda>x. m *\<^sub>R x + c)) piecewise_differentiable_on s"
+  assumes "f piecewise_differentiable_on ((\<lambda>x. m *\<^sub>R x + c) ` S)"
+  shows "(f o (\<lambda>x. m *\<^sub>R x + c)) piecewise_differentiable_on S"
 proof (cases "m = 0")
   case True
   then show ?thesis
@@ -156,13 +156,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_differentiable_on {a..b}"
 proof -
-  obtain s t where st: "finite s" "finite t"
-                       "\<forall>x\<in>{a..c} - s. f differentiable at x within {a..c}"
-                       "\<forall>x\<in>{c..b} - t. g differentiable at x within {c..b}"
+  obtain S T where st: "finite S" "finite T"
+               and fd: "\<And>x. x \<in> {a..c} - S \<Longrightarrow> f differentiable at x within {a..c}"
+               and gd: "\<And>x. x \<in> {c..b} - T \<Longrightarrow> g differentiable at x within {c..b}"
     using assms
     by (auto simp: piecewise_differentiable_on_def)
-  have finabc: "finite ({a,b,c} \<union> (s \<union> t))"
-    by (metis \<open>finite s\<close> \<open>finite t\<close> finite_Un finite_insert finite.emptyI)
+  have finabc: "finite ({a,b,c} \<union> (S \<union> T))"
+    by (metis \<open>finite S\<close> \<open>finite T\<close> finite_Un finite_insert finite.emptyI)
   have "continuous_on {a..c} f" "continuous_on {c..b} g"
     using assms piecewise_differentiable_on_def by auto
   then have "continuous_on {a..b} (\<lambda>x. if x \<le> c then f x else g x)"
@@ -172,43 +172,35 @@
     by (force simp: ivl_disj_un_two_touch)
   moreover
   { fix x
-    assume x: "x \<in> {a..b} - ({a,b,c} \<union> (s \<union> t))"
+    assume x: "x \<in> {a..b} - ({a,b,c} \<union> (S \<union> T))"
     have "(\<lambda>x. if x \<le> c then f x else g x) differentiable at x within {a..b}" (is "?diff_fg")
     proof (cases x c rule: le_cases)
       case le show ?diff_fg
-      proof (rule differentiable_transform_within [where d = "dist x c" and f = f])
-        have "f differentiable at x within ({a<..<c} - s)"
-          apply (rule differentiable_at_withinI)
-          using x le st
-          by (metis (no_types, lifting) DiffD1 DiffD2 DiffI UnCI atLeastAtMost_diff_ends atLeastAtMost_iff at_within_interior insert_iff interior_atLeastAtMost_real le st(3) x)
-        moreover have "open ({a<..<c} - s)"
-          by (blast intro: open_greaterThanLessThan \<open>finite s\<close> finite_imp_closed)
-        ultimately show "f differentiable at x within {a..b}"
-          using x le by (auto simp add: at_within_open_NO_MATCH differentiable_at_withinI)
+      proof (rule differentiable_transform_within [where d = "dist x c"])
+        have "f differentiable at x"
+          using x le fd [of x] at_within_interior [of x "{a..c}"] by simp
+        then show "f differentiable at x within {a..b}"
+          by (simp add: differentiable_at_withinI)
       qed (use x le st dist_real_def in auto)
     next
       case ge show ?diff_fg
-      proof (rule differentiable_transform_within [where d = "dist x c" and f = g])
-        have "g differentiable at x within ({c<..<b} - t)"
-          apply (rule differentiable_at_withinI)
-          using x ge st
-          by (metis DiffD1 DiffD2 DiffI UnCI atLeastAtMost_diff_ends atLeastAtMost_iff at_within_interior insert_iff interior_atLeastAtMost_real)
-        moreover have "open ({c<..<b} - t)"
-          by (blast intro: open_greaterThanLessThan \<open>finite t\<close> finite_imp_closed)
-        ultimately show "g differentiable at x within {a..b}"
-          using x ge by (auto simp add: at_within_open_NO_MATCH differentiable_at_withinI)
+      proof (rule differentiable_transform_within [where d = "dist x c"])
+        have "g differentiable at x"
+          using x ge gd [of x] at_within_interior [of x "{c..b}"] by simp
+        then show "g differentiable at x within {a..b}"
+          by (simp add: differentiable_at_withinI)
       qed (use x ge st dist_real_def in auto)
     qed
   }
-  then have "\<exists>s. finite s \<and>
-                 (\<forall>x\<in>{a..b} - s. (\<lambda>x. if x \<le> c then f x else g x) differentiable at x within {a..b})"
+  then have "\<exists>S. finite S \<and>
+                 (\<forall>x\<in>{a..b} - S. (\<lambda>x. if x \<le> c then f x else g x) differentiable at x within {a..b})"
     by (meson finabc)
   ultimately show ?thesis
     by (simp add: piecewise_differentiable_on_def)
 qed
 
 lemma piecewise_differentiable_neg:
-    "f piecewise_differentiable_on s \<Longrightarrow> (\<lambda>x. -(f x)) piecewise_differentiable_on s"
+    "f piecewise_differentiable_on S \<Longrightarrow> (\<lambda>x. -(f x)) piecewise_differentiable_on S"
   by (auto simp: piecewise_differentiable_on_def continuous_on_minus)
 
 lemma piecewise_differentiable_add:
@@ -216,11 +208,11 @@
           "g piecewise_differentiable_on i"
     shows "(\<lambda>x. f x + g x) piecewise_differentiable_on i"
 proof -
-  obtain s t where st: "finite s" "finite t"
-                       "\<forall>x\<in>i - s. f differentiable at x within i"
-                       "\<forall>x\<in>i - t. g differentiable at x within i"
+  obtain S T where st: "finite S" "finite T"
+                       "\<forall>x\<in>i - S. f differentiable at x within i"
+                       "\<forall>x\<in>i - T. g differentiable at x within i"
     using assms by (auto simp: piecewise_differentiable_on_def)
-  then have "finite (s \<union> t) \<and> (\<forall>x\<in>i - (s \<union> t). (\<lambda>x. f x + g x) differentiable at x within i)"
+  then have "finite (S \<union> T) \<and> (\<forall>x\<in>i - (S \<union> T). (\<lambda>x. f x + g x) differentiable at x within i)"
     by auto
   moreover have "continuous_on i f" "continuous_on i g"
     using assms piecewise_differentiable_on_def by auto
@@ -229,8 +221,8 @@
 qed
 
 lemma piecewise_differentiable_diff:
-    "\<lbrakk>f piecewise_differentiable_on s;  g piecewise_differentiable_on s\<rbrakk>
-     \<Longrightarrow> (\<lambda>x. f x - g x) piecewise_differentiable_on s"
+    "\<lbrakk>f piecewise_differentiable_on S;  g piecewise_differentiable_on S\<rbrakk>
+     \<Longrightarrow> (\<lambda>x. f x - g x) piecewise_differentiable_on S"
   unfolding diff_conv_add_uminus
   by (metis piecewise_differentiable_add piecewise_differentiable_neg)
 
@@ -249,33 +241,63 @@
   done
 
 lemma piecewise_differentiable_D1:
-    "(g1 +++ g2) piecewise_differentiable_on {0..1} \<Longrightarrow> g1 piecewise_differentiable_on {0..1}"
-  apply (clarsimp simp add: piecewise_differentiable_on_def dest!: continuous_on_joinpaths_D1)
-  apply (rule_tac x="insert 1 ((( * )2)`s)" in exI)
-  apply simp
-  apply (intro ballI)
-  apply (rule_tac d="dist (x/2) (1/2)" and f = "(g1 +++ g2) o (( * )(inverse 2))"
-       in differentiable_transform_within)
-  apply (auto simp: dist_real_def joinpaths_def)
-  apply (rule differentiable_chain_within derivative_intros | simp)+
-  apply (rule differentiable_subset)
-  apply (force simp:)+
-  done
+  assumes "(g1 +++ g2) piecewise_differentiable_on {0..1}"
+  shows "g1 piecewise_differentiable_on {0..1}"
+proof -
+  obtain S where cont: "continuous_on {0..1} g1" and "finite S"
+    and S: "\<And>x. x \<in> {0..1} - S \<Longrightarrow> g1 +++ g2 differentiable at x within {0..1}"
+    using assms unfolding piecewise_differentiable_on_def
+    by (blast dest!: continuous_on_joinpaths_D1)
+  show ?thesis
+    unfolding piecewise_differentiable_on_def
+  proof (intro exI conjI ballI cont)
+    show "finite (insert 1 ((( * )2) ` S))"
+      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}"
+        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)
+    qed (use that in \<open>auto simp: joinpaths_def\<close>)
+  qed
+qed
 
 lemma piecewise_differentiable_D2:
-    "\<lbrakk>(g1 +++ g2) piecewise_differentiable_on {0..1}; pathfinish g1 = pathstart g2\<rbrakk>
-    \<Longrightarrow> g2 piecewise_differentiable_on {0..1}"
-  apply (clarsimp simp add: piecewise_differentiable_on_def dest!: continuous_on_joinpaths_D2)
-  apply (rule_tac x="insert 0 ((\<lambda>x. 2*x-1)`s)" in exI)
-  apply simp
-  apply (intro ballI)
-  apply (rule_tac d="dist ((x+1)/2) (1/2)" and f = "(g1 +++ g2) o (\<lambda>x. (x+1)/2)"
-          in differentiable_transform_within)
-  apply (auto simp: dist_real_def joinpaths_def abs_if field_simps split: if_split_asm)
-  apply (rule differentiable_chain_within derivative_intros | simp)+
-  apply (rule differentiable_subset)
-  apply (force simp: divide_simps)+
-  done
+  assumes "(g1 +++ g2) piecewise_differentiable_on {0..1}" and eq: "pathfinish g1 = pathstart g2"
+  shows "g2 piecewise_differentiable_on {0..1}"
+proof -
+  have [simp]: "g1 1 = g2 0"
+    using eq by (simp add: pathfinish_def pathstart_def)
+  obtain S where cont: "continuous_on {0..1} g2" and "finite S"
+    and S: "\<And>x. x \<in> {0..1} - S \<Longrightarrow> g1 +++ g2 differentiable at x within {0..1}"
+    using assms unfolding piecewise_differentiable_on_def
+    by (blast dest!: continuous_on_joinpaths_D2)
+  show ?thesis
+    unfolding piecewise_differentiable_on_def
+  proof (intro exI conjI ballI cont)
+    show "finite (insert 0 ((\<lambda>x. 2*x-1)`S))"
+      by (simp add: \<open>finite S\<close>)
+    show "g2 differentiable at x within {0..1}" if "x \<in> {0..1} - insert 0 ((\<lambda>x. 2*x-1)`S)" for x
+    proof (rule_tac d="dist ((x+1)/2) (1/2)" in differentiable_transform_within)
+      have x2: "(x + 1) / 2 \<notin> S"
+        using that
+        apply (clarsimp simp: image_iff)
+        by (metis add.commute add_diff_cancel_left' mult_2 real_sum_of_halves)
+      have "g1 +++ g2 \<circ> (\<lambda>x. (x+1) / 2) differentiable at x within {0..1}"
+        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'
+      proof -
+        have [simp]: "(2*x'+2)/2 = x'+1"
+          by (simp add: divide_simps)
+        show ?thesis
+          using that by (auto simp: joinpaths_def)
+      qed
+    qed (use that in \<open>auto simp: joinpaths_def\<close>)
+  qed
+qed
 
 
 subsubsection\<open>The concept of continuously differentiable\<close>
@@ -590,7 +612,7 @@
     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 (drule_tac x= "(x+1) / 2" in bspec, force simp: divide_simps)
     apply assumption
     done
   have [simp]: "vector_derivative (g2 \<circ> (\<lambda>x. 2*x-1)) (at ((x+1)/2)) = 2 *\<^sub>R vector_derivative g2 (at x)"
@@ -604,7 +626,7 @@
     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)"
+  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