# HG changeset patch
# User paulson <lp15@cam.ac.uk>
# Date 1525122784 -3600
# Node ID 69715dfdc2863237e4452856ba62b629fe98fb40
# Parent  9e077a90520957bfeeacdedbff1bed13b6ba8c7d
more general tidying up

diff -r 9e077a905209 -r 69715dfdc286 src/HOL/Analysis/Convex_Euclidean_Space.thy
--- a/src/HOL/Analysis/Convex_Euclidean_Space.thy	Sun Apr 29 21:26:57 2018 +0100
+++ b/src/HOL/Analysis/Convex_Euclidean_Space.thy	Mon Apr 30 22:13:04 2018 +0100
@@ -2470,8 +2470,8 @@
 proof
   show "convex hull (s \<times> t) \<subseteq> (convex hull s) \<times> (convex hull t)"
     by (intro hull_minimal Sigma_mono hull_subset convex_Times convex_convex_hull)
-  have "\<forall>x\<in>convex hull s. \<forall>y\<in>convex hull t. (x, y) \<in> convex hull (s \<times> t)"
-  proof (intro hull_induct)
+  have "(x, y) \<in> convex hull (s \<times> t)" if x: "x \<in> convex hull s" and y: "y \<in> convex hull t" for x y
+  proof (rule hull_induct [OF x], rule hull_induct [OF y])
     fix x y assume "x \<in> s" and "y \<in> t"
     then show "(x, y) \<in> convex hull (s \<times> t)"
       by (simp add: hull_inc)
@@ -2484,8 +2484,8 @@
       by (auto simp: image_def Bex_def)
     finally show "convex {y. (x, y) \<in> convex hull (s \<times> t)}" .
   next
-    show "convex {x. \<forall>y\<in>convex hull t. (x, y) \<in> convex hull (s \<times> t)}"
-    proof (unfold Collect_ball_eq, rule convex_INT [rule_format])
+    show "convex {x. (x, y) \<in> convex hull s \<times> t}"
+    proof -
       fix y let ?S = "((\<lambda>x. (x, 0)) -` (\<lambda>p. (0, - y) + p) ` (convex hull s \<times> t))"
       have "convex ?S"
       by (intro convex_linear_vimage convex_translation convex_convex_hull,
@@ -2496,7 +2496,7 @@
     qed
   qed
   then show "(convex hull s) \<times> (convex hull t) \<subseteq> convex hull (s \<times> t)"
-    unfolding subset_eq split_paired_Ball_Sigma .
+    unfolding subset_eq split_paired_Ball_Sigma by blast
 qed
 
 
@@ -2512,16 +2512,13 @@
   fixes S :: "'a::real_vector set"
   assumes "S \<noteq> {}"
   shows "convex hull (insert a S) =
-    {x. \<exists>u\<ge>0. \<exists>v\<ge>0. \<exists>b. (u + v = 1) \<and> b \<in> (convex hull S) \<and> (x = u *\<^sub>R a + v *\<^sub>R b)}"
+         {x. \<exists>u\<ge>0. \<exists>v\<ge>0. \<exists>b. (u + v = 1) \<and> b \<in> (convex hull S) \<and> (x = u *\<^sub>R a + v *\<^sub>R b)}"
   (is "_ = ?hull")
-  apply (rule, rule hull_minimal, rule)
+proof (intro equalityI hull_minimal subsetI)
+  fix x
+  assume "x \<in> insert a S"
+  then have "\<exists>u\<ge>0. \<exists>v\<ge>0. u + v = 1 \<and> (\<exists>b. b \<in> convex hull S \<and> x = u *\<^sub>R a + v *\<^sub>R b)"
   unfolding insert_iff
-  prefer 3
-  apply rule
-proof -
-  fix x
-  assume x: "x = a \<or> x \<in> S"
-  then have "\<exists>u\<ge>0. \<exists>v\<ge>0. u + v = 1 \<and> (\<exists>b. b \<in> convex hull S \<and> x = u *\<^sub>R a + v *\<^sub>R b)"
   proof
     assume "x = a"
     then show ?thesis
@@ -2619,7 +2616,7 @@
 
 lemma convex_hull_insert_alt:
    "convex hull (insert a S) =
-      (if S = {} then {a}
+     (if S = {} then {a}
       else {(1 - u) *\<^sub>R a + u *\<^sub>R x |x u. 0 \<le> u \<and> u \<le> 1 \<and> x \<in> convex hull S})"
   apply (auto simp: convex_hull_insert)
   using diff_eq_eq apply fastforce
@@ -4371,7 +4368,7 @@
     finally have "y \<in> S"
       apply (subst *)
       apply (rule assms(1)[unfolded convex_alt,rule_format])
-      apply (rule d[unfolded subset_eq,rule_format])
+      apply (rule d[THEN subsetD])
       unfolding mem_ball
       using assms(3-5) **
       apply auto
@@ -4751,22 +4748,17 @@
 lemma affine_hull_linear_image:
   assumes "bounded_linear f"
   shows "f ` (affine hull s) = affine hull f ` s"
-  apply rule
-  unfolding subset_eq ball_simps
-  apply (rule_tac[!] hull_induct, rule hull_inc)
-  prefer 3
-  apply (erule imageE)
-  apply (rule_tac x=xa in image_eqI, assumption)
-  apply (rule hull_subset[unfolded subset_eq, rule_format], assumption)
 proof -
   interpret f: bounded_linear f by fact
-  show "affine {x. f x \<in> affine hull f ` s}"
+  have "affine {x. f x \<in> affine hull f ` s}"
     unfolding affine_def
     by (auto simp: f.scaleR f.add affine_affine_hull[unfolded affine_def, rule_format])
-  show "affine {x. x \<in> f ` (affine hull s)}"
+  moreover have "affine {x. x \<in> f ` (affine hull s)}"
     using affine_affine_hull[unfolded affine_def, of s]
     unfolding affine_def by (auto simp: f.scaleR [symmetric] f.add [symmetric])
-qed auto
+  ultimately show ?thesis
+    by (auto simp: hull_inc elim!: hull_induct)
+qed 
 
 
 lemma rel_interior_injective_on_span_linear_image:
@@ -6484,8 +6476,8 @@
   show "convex (cbox x y)"
     by (rule convex_box)
 next
-  fix s assume "{x, y} \<subseteq> s" and "convex s"
-  then show "cbox x y \<subseteq> s"
+  fix S assume "{x, y} \<subseteq> S" and "convex S"
+  then show "cbox x y \<subseteq> S"
     unfolding is_interval_convex_1 [symmetric] is_interval_def Basis_real_def
     by - (clarify, simp (no_asm_use), fast)
 qed
@@ -6516,66 +6508,53 @@
 text \<open>And this is a finite set of vertices.\<close>
 
 lemma unit_cube_convex_hull:
-  obtains s :: "'a::euclidean_space set"
-    where "finite s" and "cbox 0 (\<Sum>Basis) = convex hull s"
-  apply (rule that[of "{x::'a. \<forall>i\<in>Basis. x\<bullet>i=0 \<or> x\<bullet>i=1}"])
-  apply (rule finite_subset[of _ "(\<lambda>s. (\<Sum>i\<in>Basis. (if i\<in>s then 1 else 0) *\<^sub>R i)::'a) ` Pow Basis"])
-  prefer 3
-  apply (rule unit_interval_convex_hull, rule)
-  unfolding mem_Collect_eq
-proof -
-  fix x :: 'a
-  assume as: "\<forall>i\<in>Basis. x \<bullet> i = 0 \<or> x \<bullet> i = 1"
-  show "x \<in> (\<lambda>s. \<Sum>i\<in>Basis. (if i\<in>s then 1 else 0) *\<^sub>R i) ` Pow Basis"
-    apply (rule image_eqI[where x="{i. i\<in>Basis \<and> x\<bullet>i = 1}"])
-    using as
-    apply (subst euclidean_eq_iff, auto)
-    done
-qed auto
+  obtains S :: "'a::euclidean_space set"
+  where "finite S" and "cbox 0 (\<Sum>Basis) = convex hull S"
+proof
+  show "finite {x::'a. \<forall>i\<in>Basis. x \<bullet> i = 0 \<or> x \<bullet> i = 1}"
+  proof (rule finite_subset, clarify)
+    show "finite ((\<lambda>S. \<Sum>i\<in>Basis. (if i \<in> S then 1 else 0) *\<^sub>R i) ` Pow Basis)"
+      using finite_Basis by blast
+    fix x :: 'a
+    assume as: "\<forall>i\<in>Basis. x \<bullet> i = 0 \<or> x \<bullet> i = 1"
+    show "x \<in> (\<lambda>S. \<Sum>i\<in>Basis. (if i\<in>S then 1 else 0) *\<^sub>R i) ` Pow Basis"
+      apply (rule image_eqI[where x="{i. i\<in>Basis \<and> x\<bullet>i = 1}"])
+      using as
+       apply (subst euclidean_eq_iff, auto)
+      done
+  qed
+  show "cbox 0 One = convex hull {x. \<forall>i\<in>Basis. x \<bullet> i = 0 \<or> x \<bullet> i = 1}"
+    using unit_interval_convex_hull by blast
+qed 
 
 text \<open>Hence any cube (could do any nonempty interval).\<close>
 
 lemma cube_convex_hull:
   assumes "d > 0"
-  obtains s :: "'a::euclidean_space set" where
-    "finite s" and "cbox (x - (\<Sum>i\<in>Basis. d*\<^sub>Ri)) (x + (\<Sum>i\<in>Basis. d*\<^sub>Ri)) = convex hull s"
+  obtains S :: "'a::euclidean_space set" where
+    "finite S" and "cbox (x - (\<Sum>i\<in>Basis. d*\<^sub>Ri)) (x + (\<Sum>i\<in>Basis. d*\<^sub>Ri)) = convex hull S"
 proof -
-  let ?d = "(\<Sum>i\<in>Basis. d*\<^sub>Ri)::'a"
+  let ?d = "(\<Sum>i\<in>Basis. d *\<^sub>R i)::'a"
   have *: "cbox (x - ?d) (x + ?d) = (\<lambda>y. x - ?d + (2 * d) *\<^sub>R y) ` cbox 0 (\<Sum>Basis)"
-    apply (rule set_eqI, rule)
-    unfolding image_iff
-    defer
-    apply (erule bexE)
-  proof -
+  proof (intro set_eqI iffI)
     fix y
-    assume as: "y\<in>cbox (x - ?d) (x + ?d)"
+    assume "y \<in> cbox (x - ?d) (x + ?d)"
     then have "inverse (2 * d) *\<^sub>R (y - (x - ?d)) \<in> cbox 0 (\<Sum>Basis)"
       using assms by (simp add: mem_box field_simps inner_simps)
-    with \<open>0 < d\<close> show "\<exists>z\<in>cbox 0 (\<Sum>Basis). y = x - ?d + (2 * d) *\<^sub>R z"
-      by (intro bexI[of _ "inverse (2 * d) *\<^sub>R (y - (x - ?d))"]) auto
+    with \<open>0 < d\<close> show "y \<in> (\<lambda>y. x - sum (( *\<^sub>R) d) Basis + (2 * d) *\<^sub>R y) ` cbox 0 One"
+      by (auto intro: image_eqI[where x= "inverse (2 * d) *\<^sub>R (y - (x - ?d))"])
   next
-    fix y z
-    assume as: "z\<in>cbox 0 (\<Sum>Basis)" "y = x - ?d + (2*d) *\<^sub>R z"
-    have "\<And>i. i\<in>Basis \<Longrightarrow> 0 \<le> d * (z \<bullet> i) \<and> d * (z \<bullet> i) \<le> d"
-      using assms as(1)[unfolded mem_box]
+    fix y
+    assume "y \<in> (\<lambda>y. x - ?d + (2 * d) *\<^sub>R y) ` cbox 0 One"
+    then obtain z where z: "z \<in> cbox 0 One" "y = x - ?d + (2*d) *\<^sub>R z"
       by auto
     then show "y \<in> cbox (x - ?d) (x + ?d)"
-      unfolding as(2) mem_box
-      apply -
-      apply rule
-      using as(1)[unfolded mem_box]
-      apply (erule_tac x=i in ballE)
-      using assms
-      apply (auto simp: inner_simps)
-      done
+      using z assms by (auto simp: mem_box inner_simps)
   qed
-  obtain s where "finite s" "cbox 0 (\<Sum>Basis::'a) = convex hull s"
+  obtain S where "finite S" "cbox 0 (\<Sum>Basis::'a) = convex hull S"
     using unit_cube_convex_hull by auto
   then show ?thesis
-    apply (rule_tac that[of "(\<lambda>y. x - ?d + (2 * d) *\<^sub>R y)` s"])
-    unfolding * and convex_hull_affinity
-    apply auto
-    done
+    by (rule_tac that[of "(\<lambda>y. x - ?d + (2 * d) *\<^sub>R y)` S"]) (auto simp: convex_hull_affinity *)
 qed
 
 subsection%unimportant\<open>Representation of any interval as a finite convex hull\<close>
@@ -6635,18 +6614,18 @@
 
 lemma closed_interval_as_convex_hull:
   fixes a :: "'a::euclidean_space"
-  obtains s where "finite s" "cbox a b = convex hull s"
+  obtains S where "finite S" "cbox a b = convex hull S"
 proof (cases "cbox a b = {}")
   case True with convex_hull_empty that show ?thesis
     by blast
 next
   case False
-  obtain s::"'a set" where "finite s" and eq: "cbox 0 One = convex hull s"
+  obtain S::"'a set" where "finite S" and eq: "cbox 0 One = convex hull S"
     by (blast intro: unit_cube_convex_hull)
   have lin: "linear (\<lambda>x. \<Sum>k\<in>Basis. ((b \<bullet> k - a \<bullet> k) * (x \<bullet> k)) *\<^sub>R k)"
     by (rule linear_compose_sum) (auto simp: algebra_simps linearI)
-  have "finite ((+) a ` (\<lambda>x. \<Sum>k\<in>Basis. ((b \<bullet> k - a \<bullet> k) * (x \<bullet> k)) *\<^sub>R k) ` s)"
-    by (rule finite_imageI \<open>finite s\<close>)+
+  have "finite ((+) a ` (\<lambda>x. \<Sum>k\<in>Basis. ((b \<bullet> k - a \<bullet> k) * (x \<bullet> k)) *\<^sub>R k) ` S)"
+    by (rule finite_imageI \<open>finite S\<close>)+
   then show ?thesis
     apply (rule that)
     apply (simp add: convex_hull_translation convex_hull_linear_image [OF lin, symmetric])
@@ -6658,31 +6637,23 @@
 subsection%unimportant \<open>Bounded convex function on open set is continuous\<close>
 
 lemma convex_on_bounded_continuous:
-  fixes s :: "('a::real_normed_vector) set"
-  assumes "open s"
-    and "convex_on s f"
-    and "\<forall>x\<in>s. \<bar>f x\<bar> \<le> b"
-  shows "continuous_on s f"
+  fixes S :: "('a::real_normed_vector) set"
+  assumes "open S"
+    and "convex_on S f"
+    and "\<forall>x\<in>S. \<bar>f x\<bar> \<le> b"
+  shows "continuous_on S f"
   apply (rule continuous_at_imp_continuous_on)
   unfolding continuous_at_real_range
 proof (rule,rule,rule)
   fix x and e :: real
-  assume "x \<in> s" "e > 0"
+  assume "x \<in> S" "e > 0"
   define B where "B = \<bar>b\<bar> + 1"
-  have B: "0 < B" "\<And>x. x\<in>s \<Longrightarrow> \<bar>f x\<bar> \<le> B"
-    unfolding B_def
-    defer
-    apply (drule assms(3)[rule_format])
-    apply auto
-    done
-  obtain k where "k > 0" and k: "cball x k \<subseteq> s"
-    using assms(1)[unfolded open_contains_cball, THEN bspec[where x=x]]
-    using \<open>x\<in>s\<close> by auto
+  then have B:  "0 < B""\<And>x. x\<in>S \<Longrightarrow> \<bar>f x\<bar> \<le> B"
+    using assms(3) by auto 
+  obtain k where "k > 0" and k: "cball x k \<subseteq> S"
+    using \<open>x \<in> S\<close> assms(1) open_contains_cball_eq by blast
   show "\<exists>d>0. \<forall>x'. norm (x' - x) < d \<longrightarrow> \<bar>f x' - f x\<bar> < e"
-    apply (rule_tac x="min (k / 2) (e / (2 * B) * k)" in exI)
-    apply rule
-    defer
-  proof (rule, rule)
+  proof (intro exI conjI allI impI)
     fix y
     assume as: "norm (y - x) < min (k / 2) (e / (2 * B) * k)"
     show "\<bar>f y - f x\<bar> < e"
@@ -6692,22 +6663,16 @@
       have "2 < t" "0<t"
         unfolding t_def using as False and \<open>k>0\<close>
         by (auto simp:field_simps)
-      have "y \<in> s"
-        apply (rule k[unfolded subset_eq,rule_format])
+      have "y \<in> S"
+        apply (rule k[THEN subsetD])
         unfolding mem_cball dist_norm
         apply (rule order_trans[of _ "2 * norm (x - y)"])
         using as
         by (auto simp: field_simps norm_minus_commute)
       {
         define w where "w = x + t *\<^sub>R (y - x)"
-        have "w \<in> s"
-          unfolding w_def
-          apply (rule k[unfolded subset_eq,rule_format])
-          unfolding mem_cball dist_norm
-          unfolding t_def
-          using \<open>k>0\<close>
-          apply auto
-          done
+        have "w \<in> S"
+          using \<open>k>0\<close> by (auto simp: dist_norm t_def w_def k[THEN subsetD])
         have "(1 / t) *\<^sub>R x + - x + ((t - 1) / t) *\<^sub>R x = (1 / t - 1 + (t - 1) / t) *\<^sub>R x"
           by (auto simp: algebra_simps)
         also have "\<dots> = 0"
@@ -6720,23 +6685,17 @@
           by (auto simp:field_simps)
         have "f y - f x \<le> (f w - f x) / t"
           using assms(2)[unfolded convex_on_def,rule_format,of w x "1/t" "(t - 1)/t", unfolded w]
-          using \<open>0 < t\<close> \<open>2 < t\<close> and \<open>x \<in> s\<close> \<open>w \<in> s\<close>
+          using \<open>0 < t\<close> \<open>2 < t\<close> and \<open>x \<in> S\<close> \<open>w \<in> S\<close>
           by (auto simp:field_simps)
         also have "... < e"
-          using B(2)[OF \<open>w\<in>s\<close>] and B(2)[OF \<open>x\<in>s\<close>] 2 \<open>t > 0\<close> by (auto simp: field_simps)
+          using B(2)[OF \<open>w\<in>S\<close>] and B(2)[OF \<open>x\<in>S\<close>] 2 \<open>t > 0\<close> by (auto simp: field_simps)
         finally have th1: "f y - f x < e" .
       }
       moreover
       {
         define w where "w = x - t *\<^sub>R (y - x)"
-        have "w \<in> s"
-          unfolding w_def
-          apply (rule k[unfolded subset_eq,rule_format])
-          unfolding mem_cball dist_norm
-          unfolding t_def
-          using \<open>k > 0\<close>
-          apply auto
-          done
+        have "w \<in> S"
+          using \<open>k > 0\<close> by (auto simp: dist_norm t_def w_def k[THEN subsetD])
         have "(1 / (1 + t)) *\<^sub>R x + (t / (1 + t)) *\<^sub>R x = (1 / (1 + t) + t / (1 + t)) *\<^sub>R x"
           by (auto simp: algebra_simps)
         also have "\<dots> = x"
@@ -6749,12 +6708,12 @@
           using \<open>0 < e\<close> \<open>0 < k\<close> \<open>B > 0\<close> and as and False
           by (auto simp:field_simps)
         then have *: "(f w - f y) / t < e"
-          using B(2)[OF \<open>w\<in>s\<close>] and B(2)[OF \<open>y\<in>s\<close>]
+          using B(2)[OF \<open>w\<in>S\<close>] and B(2)[OF \<open>y\<in>S\<close>]
           using \<open>t > 0\<close>
           by (auto simp:field_simps)
         have "f x \<le> 1 / (1 + t) * f w + (t / (1 + t)) * f y"
           using assms(2)[unfolded convex_on_def,rule_format,of w y "1/(1+t)" "t / (1+t)",unfolded w]
-          using \<open>0 < t\<close> \<open>2 < t\<close> and \<open>y \<in> s\<close> \<open>w \<in> s\<close>
+          using \<open>0 < t\<close> \<open>2 < t\<close> and \<open>y \<in> S\<close> \<open>w \<in> S\<close>
           by (auto simp:field_simps)
         also have "\<dots> = (f w + t * f y) / (1 + t)"
           using \<open>t > 0\<close> by (auto simp: divide_simps)
@@ -6843,11 +6802,7 @@
       by (simp add: dist_norm abs_le_iff algebra_simps)
     show "cball x d \<subseteq> convex hull c"
       unfolding 2
-      apply clarsimp
-      apply (simp only: dist_norm)
-      apply (subst inner_diff_left [symmetric], simp)
-      apply (erule (1) order_trans [OF Basis_le_norm])
-      done
+      by (clarsimp simp: dist_norm) (metis inner_commute inner_diff_right norm_bound_Basis_le)
     have e': "e = (\<Sum>(i::'a)\<in>Basis. d)"
       by (simp add: d_def DIM_positive)
     show "convex hull c \<subseteq> cball x e"
diff -r 9e077a905209 -r 69715dfdc286 src/HOL/Analysis/Derivative.thy
--- a/src/HOL/Analysis/Derivative.thy	Sun Apr 29 21:26:57 2018 +0100
+++ b/src/HOL/Analysis/Derivative.thy	Mon Apr 30 22:13:04 2018 +0100
@@ -373,77 +373,76 @@
 
 lemma frechet_derivative_unique_within:
   fixes f :: "'a::euclidean_space \<Rightarrow> 'b::real_normed_vector"
-  assumes "(f has_derivative f') (at x within s)"
-    and "(f has_derivative f'') (at x within s)"
-    and "\<forall>i\<in>Basis. \<forall>e>0. \<exists>d. 0 < \<bar>d\<bar> \<and> \<bar>d\<bar> < e \<and> (x + d *\<^sub>R i) \<in> s"
+  assumes "(f has_derivative f') (at x within S)"
+    and "(f has_derivative f'') (at x within S)"
+    and "\<forall>i\<in>Basis. \<forall>e>0. \<exists>d. 0 < \<bar>d\<bar> \<and> \<bar>d\<bar> < e \<and> (x + d *\<^sub>R i) \<in> S"
   shows "f' = f''"
 proof -
   note as = assms(1,2)[unfolded has_derivative_def]
   then interpret f': bounded_linear f' by auto
   from as interpret f'': bounded_linear f'' by auto
-  have "x islimpt s" unfolding islimpt_approachable
+  have "x islimpt S" unfolding islimpt_approachable
   proof (rule, rule)
     fix e :: real
     assume "e > 0"
-    obtain d where "0 < \<bar>d\<bar>" and "\<bar>d\<bar> < e" and "x + d *\<^sub>R (SOME i. i \<in> Basis) \<in> s"
+    obtain d where "0 < \<bar>d\<bar>" and "\<bar>d\<bar> < e" and "x + d *\<^sub>R (SOME i. i \<in> Basis) \<in> S"
       using assms(3) SOME_Basis \<open>e>0\<close> by blast
-    then show "\<exists>x'\<in>s. x' \<noteq> x \<and> dist x' x < e"
+    then show "\<exists>x'\<in>S. x' \<noteq> x \<and> dist x' x < e"
       apply (rule_tac x="x + d *\<^sub>R (SOME i. i \<in> Basis)" in bexI)
       unfolding dist_norm
       apply (auto simp: SOME_Basis nonzero_Basis)
       done
   qed
-  then have *: "netlimit (at x within s) = x"
+  then have *: "netlimit (at x within S) = x"
     apply (auto intro!: netlimit_within)
     by (metis trivial_limit_within)
   show ?thesis
-    apply (rule linear_eq_stdbasis)
-    unfolding linear_conv_bounded_linear
-    apply (rule as(1,2)[THEN conjunct1])+
-  proof (rule, rule ccontr)
+  proof (rule linear_eq_stdbasis)
+    show "linear f'" "linear f''"
+      unfolding linear_conv_bounded_linear using as by auto
+  next
     fix i :: 'a
     assume i: "i \<in> Basis"
     define e where "e = norm (f' i - f'' i)"
-    assume "f' i \<noteq> f'' i"
-    then have "e > 0"
-      unfolding e_def by auto
-    obtain d where d:
-      "0 < d"
-      "(\<And>xa. xa\<in>s \<longrightarrow> 0 < dist xa x \<and> dist xa x < d \<longrightarrow>
-          dist ((f xa - f x - f' (xa - x)) /\<^sub>R norm (xa - x) -
-              (f xa - f x - f'' (xa - x)) /\<^sub>R norm (xa - x)) (0 - 0) < e)"
-      using tendsto_diff [OF as(1,2)[THEN conjunct2]]
-      unfolding * Lim_within
-      using \<open>e>0\<close> by blast
-    obtain c where c: "0 < \<bar>c\<bar>" "\<bar>c\<bar> < d \<and> x + c *\<^sub>R i \<in> s"
-      using assms(3) i d(1) by blast
-    have *: "norm (- ((1 / \<bar>c\<bar>) *\<^sub>R f' (c *\<^sub>R i)) + (1 / \<bar>c\<bar>) *\<^sub>R f'' (c *\<^sub>R i)) =
+    show "f' i = f'' i"
+    proof (rule ccontr)
+      assume "f' i \<noteq> f'' i"
+      then have "e > 0"
+        unfolding e_def by auto
+      obtain d where d:
+        "0 < d"
+        "(\<And>y. y\<in>S \<longrightarrow> 0 < dist y x \<and> dist y x < d \<longrightarrow>
+          dist ((f y - f x - f' (y - x)) /\<^sub>R norm (y - x) -
+              (f y - f x - f'' (y - x)) /\<^sub>R norm (y - x)) (0 - 0) < e)"
+        using tendsto_diff [OF as(1,2)[THEN conjunct2]]
+        unfolding * Lim_within
+        using \<open>e>0\<close> by blast
+      obtain c where c: "0 < \<bar>c\<bar>" "\<bar>c\<bar> < d \<and> x + c *\<^sub>R i \<in> S"
+        using assms(3) i d(1) by blast
+      have *: "norm (- ((1 / \<bar>c\<bar>) *\<^sub>R f' (c *\<^sub>R i)) + (1 / \<bar>c\<bar>) *\<^sub>R f'' (c *\<^sub>R i)) =
         norm ((1 / \<bar>c\<bar>) *\<^sub>R (- (f' (c *\<^sub>R i)) + f'' (c *\<^sub>R i)))"
-      unfolding scaleR_right_distrib by auto
-    also have "\<dots> = norm ((1 / \<bar>c\<bar>) *\<^sub>R (c *\<^sub>R (- (f' i) + f'' i)))"
-      unfolding f'.scaleR f''.scaleR
-      unfolding scaleR_right_distrib scaleR_minus_right
-      by auto
-    also have "\<dots> = e"
-      unfolding e_def
-      using c(1)
-      using norm_minus_cancel[of "f' i - f'' i"]
-      by auto
-    finally show False
-      using c
-      using d(2)[of "x + c *\<^sub>R i"]
-      unfolding dist_norm
-      unfolding f'.scaleR f''.scaleR f'.add f''.add f'.diff f''.diff
-        scaleR_scaleR scaleR_right_diff_distrib scaleR_right_distrib
-      using i
-      by (auto simp: inverse_eq_divide)
+        unfolding scaleR_right_distrib by auto
+      also have "\<dots> = norm ((1 / \<bar>c\<bar>) *\<^sub>R (c *\<^sub>R (- (f' i) + f'' i)))"
+        unfolding f'.scaleR f''.scaleR
+        unfolding scaleR_right_distrib scaleR_minus_right
+        by auto
+      also have "\<dots> = e"
+        unfolding e_def
+        using c(1)
+        using norm_minus_cancel[of "f' i - f'' i"]
+        by auto
+      finally show False
+        using c
+        using d(2)[of "x + c *\<^sub>R i"]
+        unfolding dist_norm
+        unfolding f'.scaleR f''.scaleR f'.add f''.add f'.diff f''.diff
+          scaleR_scaleR scaleR_right_diff_distrib scaleR_right_distrib
+        using i
+        by (auto simp: inverse_eq_divide)
+    qed
   qed
 qed
 
-lemma frechet_derivative_unique_at:
-  "(f has_derivative f') (at x) \<Longrightarrow> (f has_derivative f'') (at x) \<Longrightarrow> f' = f''"
-  by (rule has_derivative_unique)
-
 lemma frechet_derivative_unique_within_closed_interval:
   fixes f::"'a::euclidean_space \<Rightarrow> 'b::real_normed_vector"
   assumes "\<forall>i\<in>Basis. a\<bullet>i < b\<bullet>i"
@@ -506,12 +505,12 @@
   from assms(1) have *: "at x within box a b = at x"
     by (metis at_within_interior interior_open open_box)
   from assms(2,3) [unfolded *] show "f' = f''"
-    by (rule frechet_derivative_unique_at)
+    by (rule has_derivative_unique)
 qed
 
 lemma frechet_derivative_at:
   "(f has_derivative f') (at x) \<Longrightarrow> f' = frechet_derivative f (at x)"
-  apply (rule frechet_derivative_unique_at[of f])
+  apply (rule has_derivative_unique[of f])
   apply assumption
   unfolding frechet_derivative_works[symmetric]
   using differentiable_def
diff -r 9e077a905209 -r 69715dfdc286 src/HOL/Analysis/Linear_Algebra.thy
--- a/src/HOL/Analysis/Linear_Algebra.thy	Sun Apr 29 21:26:57 2018 +0100
+++ b/src/HOL/Analysis/Linear_Algebra.thy	Mon Apr 30 22:13:04 2018 +0100
@@ -72,7 +72,7 @@
 lemma hull_unique: "s \<subseteq> t \<Longrightarrow> S t \<Longrightarrow> (\<And>t'. s \<subseteq> t' \<Longrightarrow> S t' \<Longrightarrow> t \<subseteq> t') \<Longrightarrow> (S hull s = t)"
   unfolding hull_def by auto
 
-lemma hull_induct: "(\<And>x. x\<in> S \<Longrightarrow> P x) \<Longrightarrow> Q {x. P x} \<Longrightarrow> \<forall>x\<in> Q hull S. P x"
+lemma hull_induct: "\<lbrakk>a \<in> Q hull S; \<And>x. x\<in> S \<Longrightarrow> P x; Q {x. P x}\<rbrakk> \<Longrightarrow> P a"
   using hull_minimal[of S "{x. P x}" Q]
   by (auto simp add: subset_eq)
 
@@ -339,20 +339,12 @@
   unfolding dependent_def by auto
 
 lemma (in real_vector) independent_mono: "independent A \<Longrightarrow> B \<subseteq> A \<Longrightarrow> independent B"
-  apply (clarsimp simp add: dependent_def span_mono)
-  apply (subgoal_tac "span (B - {a}) \<le> span (A - {a})")
-  apply force
-  apply (rule span_mono)
-  apply auto
-  done
+  unfolding dependent_def span_mono
+  by (metis insert_Diff local.span_mono subsetCE subset_insert_iff) 
 
 lemma (in real_vector) span_subspace: "A \<subseteq> B \<Longrightarrow> B \<le> span A \<Longrightarrow>  subspace B \<Longrightarrow> span A = B"
   by (metis order_antisym span_def hull_minimal)
 
-lemma (in real_vector) span_induct':
-  "\<forall>x \<in> S. P x \<Longrightarrow> subspace {x. P x} \<Longrightarrow> \<forall>x \<in> span S. P x"
-  unfolding span_def by (rule hull_induct) auto
-
 inductive_set (in real_vector) span_induct_alt_help for S :: "'a set"
 where
   span_induct_alt_help_0: "0 \<in> span_induct_alt_help S"
@@ -1063,19 +1055,19 @@
   done
 
 lemma linear_eq_0_span:
-  assumes lf: "linear f" and f0: "\<forall>x\<in>B. f x = 0"
-  shows "\<forall>x \<in> span B. f x = 0"
-  using f0 subspace_kernel[OF lf]
-  by (rule span_induct')
-
-lemma linear_eq_0: "linear f \<Longrightarrow> S \<subseteq> span B \<Longrightarrow> \<forall>x\<in>B. f x = 0 \<Longrightarrow> \<forall>x\<in>S. f x = 0"
-  using linear_eq_0_span[of f B] by auto
-
-lemma linear_eq_span:  "linear f \<Longrightarrow> linear g \<Longrightarrow> \<forall>x\<in>B. f x = g x \<Longrightarrow> \<forall>x \<in> span B. f x = g x"
-  using linear_eq_0_span[of "\<lambda>x. f x - g x" B] by (auto simp: linear_compose_sub)
-
-lemma linear_eq: "linear f \<Longrightarrow> linear g \<Longrightarrow> S \<subseteq> span B \<Longrightarrow> \<forall>x\<in>B. f x = g x \<Longrightarrow> \<forall>x\<in>S. f x = g x"
-  using linear_eq_span[of f g B] by auto
+  assumes x: "x \<in> span B" and lf: "linear f" and f0: "\<And>x. x\<in>B \<Longrightarrow> f x = 0"
+  shows "f x = 0"
+  using x f0 subspace_kernel[OF lf] span_induct
+  by blast
+
+lemma linear_eq_0: "\<lbrakk>x \<in> S; linear f; S \<subseteq> span B; \<And>x. x\<in>B \<Longrightarrow> f x = 0\<rbrakk> \<Longrightarrow> f x = 0"
+  using linear_eq_0_span[of x B f] by auto
+
+lemma linear_eq_span: "\<lbrakk>x \<in> span B; linear f; linear g; \<And>x. x\<in>B \<Longrightarrow> f x = g x\<rbrakk> \<Longrightarrow> f x = g x"
+  using linear_eq_0_span[of x B "\<lambda>x. f x - g x"]  by (auto simp: linear_compose_sub)
+
+lemma linear_eq: "\<lbrakk>x \<in> S; linear f; linear g; S \<subseteq> span B; \<And>x. x\<in>B \<Longrightarrow> f x = g x\<rbrakk> \<Longrightarrow> f x = g x"
+  using linear_eq_span[of _ B f g] by auto
 
 text \<open>The degenerate case of the Exchange Lemma.\<close>
 
@@ -1174,13 +1166,13 @@
   have fB: "inj_on f B"
     using fi by (auto simp: \<open>span S = span B\<close> intro: subset_inj_on span_superset)
 
-  have "\<forall>x\<in>span B. g (f x) = x"
-  proof (intro linear_eq_span)
+  have "g (f x) = x" if "x \<in> span B" for x
+  proof (rule linear_eq_span)
     show "linear (\<lambda>x. x)" "linear (\<lambda>x. g (f x))"
       using linear_id linear_compose[OF \<open>linear f\<close> \<open>linear g\<close>] by (auto simp: id_def comp_def)
-    show "\<forall>x \<in> B. g (f x) = x"
-      using g fi \<open>span S = span B\<close> by (auto simp: fB)
-  qed
+    show "g (f x) = x" if "x \<in> B" for x
+      using g fi \<open>span S = span B\<close>   by (simp add: fB that)
+  qed (rule that)
   moreover
   have "inv_into B f ` f ` B \<subseteq> B"
     by (auto simp: fB)
@@ -1210,8 +1202,7 @@
   ultimately have "\<forall>x\<in>B. f (g x) = x"
     by auto
   then have "\<forall>x\<in>span B. f (g x) = x"
-    using linear_id linear_compose[OF \<open>linear g\<close> \<open>linear f\<close>]
-    by (intro linear_eq_span) (auto simp: id_def comp_def)
+    using linear_id linear_compose[OF \<open>linear g\<close> \<open>linear f\<close>] linear_eq_span by fastforce
   moreover have "inv_into (span S) f ` B \<subseteq> span S"
     using \<open>B \<subseteq> T\<close> \<open>span T \<subseteq> f`span S\<close> by (auto intro: inv_into_into span_superset)
   then have "range g \<subseteq> span S"
@@ -2457,8 +2448,8 @@
     done
   with a have a0:"?a  \<noteq> 0"
     by auto
-  have "\<forall>x\<in>span B. ?a \<bullet> x = 0"
-  proof (rule span_induct')
+  have "?a \<bullet> x = 0" if "x\<in>span B" for x
+  proof (rule span_induct [OF that])
     show "subspace {x. ?a \<bullet> x = 0}"
       by (auto simp add: subspace_def inner_add)
   next
@@ -2481,9 +2472,9 @@
           intro: B(5)[unfolded pairwise_def orthogonal_def, rule_format])
         done
     }
-    then show "\<forall>x \<in> B. ?a \<bullet> x = 0"
-      by blast
-  qed
+    then show "?a \<bullet> x = 0" if "x \<in> B" for x
+      using that by blast
+    qed
   with a0 show ?thesis
     unfolding sSB by (auto intro: exI[where x="?a"])
 qed
@@ -2635,9 +2626,9 @@
   fixes f :: "'a::euclidean_space \<Rightarrow> _"
   assumes lf: "linear f"
     and lg: "linear g"
-    and fg: "\<forall>b\<in>Basis. f b = g b"
+    and fg: "\<And>b. b \<in> Basis \<Longrightarrow> f b = g b"
   shows "f = g"
-  using linear_eq[OF lf lg, of _ Basis] fg by auto
+  using linear_eq[OF _ lf lg, of _ _ Basis] fg by auto
 
 text \<open>Similar results for bilinear functions.\<close>
 
@@ -2646,8 +2637,9 @@
     and bg: "bilinear g"
     and SB: "S \<subseteq> span B"
     and TC: "T \<subseteq> span C"
-    and fg: "\<forall>x\<in> B. \<forall>y\<in> C. f x y = g x y"
-  shows "\<forall>x\<in>S. \<forall>y\<in>T. f x y = g x y "
+    and "x\<in>S" "y\<in>T"
+    and fg: "\<And>x y. \<lbrakk>x \<in> B; y\<in> C\<rbrakk> \<Longrightarrow> f x y = g x y"
+  shows "f x y = g x y"
 proof -
   let ?P = "{x. \<forall>y\<in> span C. f x y = g x y}"
   from bf bg have sp: "subspace ?P"
@@ -2655,27 +2647,30 @@
     by (auto simp add: span_0 bilinear_lzero[OF bf] bilinear_lzero[OF bg] span_add Ball_def
       intro: bilinear_ladd[OF bf])
 
-  have "\<forall>x \<in> span B. \<forall>y\<in> span C. f x y = g x y"
-    apply (rule span_induct' [OF _ sp])
-    apply (rule ballI)
-    apply (rule span_induct')
-    apply (simp add: fg)
+  have sfg: "\<And>x. x \<in> B \<Longrightarrow> subspace {a. f x a = g x a}"
     apply (auto simp add: subspace_def)
     using bf bg unfolding bilinear_def linear_iff
-    apply (auto simp add: span_0 bilinear_rzero[OF bf] bilinear_rzero[OF bg] span_add Ball_def
+    apply (auto simp add: bilinear_rzero[OF bf] bilinear_rzero[OF bg] span_add 
       intro: bilinear_ladd[OF bf])
     done
+  have "\<forall>y\<in> span C. f x y = g x y" if "x \<in> span B" for x
+    apply (rule span_induct [OF that sp])
+    apply (rule ballI)
+    apply (erule span_induct)
+    apply (simp_all add: sfg fg)
+    done
   then show ?thesis
-    using SB TC by auto
+    using SB TC assms by auto
 qed
 
 lemma bilinear_eq_stdbasis:
   fixes f :: "'a::euclidean_space \<Rightarrow> 'b::euclidean_space \<Rightarrow> _"
   assumes bf: "bilinear f"
     and bg: "bilinear g"
-    and fg: "\<forall>i\<in>Basis. \<forall>j\<in>Basis. f i j = g i j"
+    and fg: "\<And>i j. i \<in> Basis \<Longrightarrow> j \<in> Basis \<Longrightarrow> f i j = g i j"
   shows "f = g"
-  using bilinear_eq[OF bf bg equalityD2[OF span_Basis] equalityD2[OF span_Basis] fg] by blast
+  using bilinear_eq[OF bf bg equalityD2[OF span_Basis] equalityD2[OF span_Basis]] fg
+  by blast
 
 text \<open>An injective map @{typ "'a::euclidean_space \<Rightarrow> 'b::euclidean_space"} is also surjective.\<close>
 
@@ -2695,13 +2690,7 @@
     apply (rule card_ge_dim_independent)
     apply blast
     apply (rule independent_injective_image[OF B(2) lf fi])
-    apply (rule order_eq_refl)
-    apply (rule sym)
-    unfolding d
-    apply (rule card_image)
-    apply (rule subset_inj_on[OF fi])
-    apply blast
-    done
+    by (metis card_image d fi inj_on_subset order_refl top_greatest)
   from th show ?thesis
     unfolding span_linear_image[OF lf] surj_def
     using B(3) by blast