more general tidying up
authorpaulson <lp15@cam.ac.uk>
Mon Apr 30 22:13:04 2018 +0100 (13 months ago)
changeset 6805869715dfdc286
parent 68056 9e077a905209
child 68059 6f7829c14f5a
more general tidying up
src/HOL/Analysis/Convex_Euclidean_Space.thy
src/HOL/Analysis/Derivative.thy
src/HOL/Analysis/Linear_Algebra.thy
     1.1 --- a/src/HOL/Analysis/Convex_Euclidean_Space.thy	Sun Apr 29 21:26:57 2018 +0100
     1.2 +++ b/src/HOL/Analysis/Convex_Euclidean_Space.thy	Mon Apr 30 22:13:04 2018 +0100
     1.3 @@ -2470,8 +2470,8 @@
     1.4  proof
     1.5    show "convex hull (s \<times> t) \<subseteq> (convex hull s) \<times> (convex hull t)"
     1.6      by (intro hull_minimal Sigma_mono hull_subset convex_Times convex_convex_hull)
     1.7 -  have "\<forall>x\<in>convex hull s. \<forall>y\<in>convex hull t. (x, y) \<in> convex hull (s \<times> t)"
     1.8 -  proof (intro hull_induct)
     1.9 +  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
    1.10 +  proof (rule hull_induct [OF x], rule hull_induct [OF y])
    1.11      fix x y assume "x \<in> s" and "y \<in> t"
    1.12      then show "(x, y) \<in> convex hull (s \<times> t)"
    1.13        by (simp add: hull_inc)
    1.14 @@ -2484,8 +2484,8 @@
    1.15        by (auto simp: image_def Bex_def)
    1.16      finally show "convex {y. (x, y) \<in> convex hull (s \<times> t)}" .
    1.17    next
    1.18 -    show "convex {x. \<forall>y\<in>convex hull t. (x, y) \<in> convex hull (s \<times> t)}"
    1.19 -    proof (unfold Collect_ball_eq, rule convex_INT [rule_format])
    1.20 +    show "convex {x. (x, y) \<in> convex hull s \<times> t}"
    1.21 +    proof -
    1.22        fix y let ?S = "((\<lambda>x. (x, 0)) -` (\<lambda>p. (0, - y) + p) ` (convex hull s \<times> t))"
    1.23        have "convex ?S"
    1.24        by (intro convex_linear_vimage convex_translation convex_convex_hull,
    1.25 @@ -2496,7 +2496,7 @@
    1.26      qed
    1.27    qed
    1.28    then show "(convex hull s) \<times> (convex hull t) \<subseteq> convex hull (s \<times> t)"
    1.29 -    unfolding subset_eq split_paired_Ball_Sigma .
    1.30 +    unfolding subset_eq split_paired_Ball_Sigma by blast
    1.31  qed
    1.32  
    1.33  
    1.34 @@ -2512,16 +2512,13 @@
    1.35    fixes S :: "'a::real_vector set"
    1.36    assumes "S \<noteq> {}"
    1.37    shows "convex hull (insert a S) =
    1.38 -    {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)}"
    1.39 +         {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)}"
    1.40    (is "_ = ?hull")
    1.41 -  apply (rule, rule hull_minimal, rule)
    1.42 +proof (intro equalityI hull_minimal subsetI)
    1.43 +  fix x
    1.44 +  assume "x \<in> insert a S"
    1.45 +  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)"
    1.46    unfolding insert_iff
    1.47 -  prefer 3
    1.48 -  apply rule
    1.49 -proof -
    1.50 -  fix x
    1.51 -  assume x: "x = a \<or> x \<in> S"
    1.52 -  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)"
    1.53    proof
    1.54      assume "x = a"
    1.55      then show ?thesis
    1.56 @@ -2619,7 +2616,7 @@
    1.57  
    1.58  lemma convex_hull_insert_alt:
    1.59     "convex hull (insert a S) =
    1.60 -      (if S = {} then {a}
    1.61 +     (if S = {} then {a}
    1.62        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})"
    1.63    apply (auto simp: convex_hull_insert)
    1.64    using diff_eq_eq apply fastforce
    1.65 @@ -4371,7 +4368,7 @@
    1.66      finally have "y \<in> S"
    1.67        apply (subst *)
    1.68        apply (rule assms(1)[unfolded convex_alt,rule_format])
    1.69 -      apply (rule d[unfolded subset_eq,rule_format])
    1.70 +      apply (rule d[THEN subsetD])
    1.71        unfolding mem_ball
    1.72        using assms(3-5) **
    1.73        apply auto
    1.74 @@ -4751,22 +4748,17 @@
    1.75  lemma affine_hull_linear_image:
    1.76    assumes "bounded_linear f"
    1.77    shows "f ` (affine hull s) = affine hull f ` s"
    1.78 -  apply rule
    1.79 -  unfolding subset_eq ball_simps
    1.80 -  apply (rule_tac[!] hull_induct, rule hull_inc)
    1.81 -  prefer 3
    1.82 -  apply (erule imageE)
    1.83 -  apply (rule_tac x=xa in image_eqI, assumption)
    1.84 -  apply (rule hull_subset[unfolded subset_eq, rule_format], assumption)
    1.85  proof -
    1.86    interpret f: bounded_linear f by fact
    1.87 -  show "affine {x. f x \<in> affine hull f ` s}"
    1.88 +  have "affine {x. f x \<in> affine hull f ` s}"
    1.89      unfolding affine_def
    1.90      by (auto simp: f.scaleR f.add affine_affine_hull[unfolded affine_def, rule_format])
    1.91 -  show "affine {x. x \<in> f ` (affine hull s)}"
    1.92 +  moreover have "affine {x. x \<in> f ` (affine hull s)}"
    1.93      using affine_affine_hull[unfolded affine_def, of s]
    1.94      unfolding affine_def by (auto simp: f.scaleR [symmetric] f.add [symmetric])
    1.95 -qed auto
    1.96 +  ultimately show ?thesis
    1.97 +    by (auto simp: hull_inc elim!: hull_induct)
    1.98 +qed 
    1.99  
   1.100  
   1.101  lemma rel_interior_injective_on_span_linear_image:
   1.102 @@ -6484,8 +6476,8 @@
   1.103    show "convex (cbox x y)"
   1.104      by (rule convex_box)
   1.105  next
   1.106 -  fix s assume "{x, y} \<subseteq> s" and "convex s"
   1.107 -  then show "cbox x y \<subseteq> s"
   1.108 +  fix S assume "{x, y} \<subseteq> S" and "convex S"
   1.109 +  then show "cbox x y \<subseteq> S"
   1.110      unfolding is_interval_convex_1 [symmetric] is_interval_def Basis_real_def
   1.111      by - (clarify, simp (no_asm_use), fast)
   1.112  qed
   1.113 @@ -6516,66 +6508,53 @@
   1.114  text \<open>And this is a finite set of vertices.\<close>
   1.115  
   1.116  lemma unit_cube_convex_hull:
   1.117 -  obtains s :: "'a::euclidean_space set"
   1.118 -    where "finite s" and "cbox 0 (\<Sum>Basis) = convex hull s"
   1.119 -  apply (rule that[of "{x::'a. \<forall>i\<in>Basis. x\<bullet>i=0 \<or> x\<bullet>i=1}"])
   1.120 -  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"])
   1.121 -  prefer 3
   1.122 -  apply (rule unit_interval_convex_hull, rule)
   1.123 -  unfolding mem_Collect_eq
   1.124 -proof -
   1.125 -  fix x :: 'a
   1.126 -  assume as: "\<forall>i\<in>Basis. x \<bullet> i = 0 \<or> x \<bullet> i = 1"
   1.127 -  show "x \<in> (\<lambda>s. \<Sum>i\<in>Basis. (if i\<in>s then 1 else 0) *\<^sub>R i) ` Pow Basis"
   1.128 -    apply (rule image_eqI[where x="{i. i\<in>Basis \<and> x\<bullet>i = 1}"])
   1.129 -    using as
   1.130 -    apply (subst euclidean_eq_iff, auto)
   1.131 -    done
   1.132 -qed auto
   1.133 +  obtains S :: "'a::euclidean_space set"
   1.134 +  where "finite S" and "cbox 0 (\<Sum>Basis) = convex hull S"
   1.135 +proof
   1.136 +  show "finite {x::'a. \<forall>i\<in>Basis. x \<bullet> i = 0 \<or> x \<bullet> i = 1}"
   1.137 +  proof (rule finite_subset, clarify)
   1.138 +    show "finite ((\<lambda>S. \<Sum>i\<in>Basis. (if i \<in> S then 1 else 0) *\<^sub>R i) ` Pow Basis)"
   1.139 +      using finite_Basis by blast
   1.140 +    fix x :: 'a
   1.141 +    assume as: "\<forall>i\<in>Basis. x \<bullet> i = 0 \<or> x \<bullet> i = 1"
   1.142 +    show "x \<in> (\<lambda>S. \<Sum>i\<in>Basis. (if i\<in>S then 1 else 0) *\<^sub>R i) ` Pow Basis"
   1.143 +      apply (rule image_eqI[where x="{i. i\<in>Basis \<and> x\<bullet>i = 1}"])
   1.144 +      using as
   1.145 +       apply (subst euclidean_eq_iff, auto)
   1.146 +      done
   1.147 +  qed
   1.148 +  show "cbox 0 One = convex hull {x. \<forall>i\<in>Basis. x \<bullet> i = 0 \<or> x \<bullet> i = 1}"
   1.149 +    using unit_interval_convex_hull by blast
   1.150 +qed 
   1.151  
   1.152  text \<open>Hence any cube (could do any nonempty interval).\<close>
   1.153  
   1.154  lemma cube_convex_hull:
   1.155    assumes "d > 0"
   1.156 -  obtains s :: "'a::euclidean_space set" where
   1.157 -    "finite s" and "cbox (x - (\<Sum>i\<in>Basis. d*\<^sub>Ri)) (x + (\<Sum>i\<in>Basis. d*\<^sub>Ri)) = convex hull s"
   1.158 +  obtains S :: "'a::euclidean_space set" where
   1.159 +    "finite S" and "cbox (x - (\<Sum>i\<in>Basis. d*\<^sub>Ri)) (x + (\<Sum>i\<in>Basis. d*\<^sub>Ri)) = convex hull S"
   1.160  proof -
   1.161 -  let ?d = "(\<Sum>i\<in>Basis. d*\<^sub>Ri)::'a"
   1.162 +  let ?d = "(\<Sum>i\<in>Basis. d *\<^sub>R i)::'a"
   1.163    have *: "cbox (x - ?d) (x + ?d) = (\<lambda>y. x - ?d + (2 * d) *\<^sub>R y) ` cbox 0 (\<Sum>Basis)"
   1.164 -    apply (rule set_eqI, rule)
   1.165 -    unfolding image_iff
   1.166 -    defer
   1.167 -    apply (erule bexE)
   1.168 -  proof -
   1.169 +  proof (intro set_eqI iffI)
   1.170      fix y
   1.171 -    assume as: "y\<in>cbox (x - ?d) (x + ?d)"
   1.172 +    assume "y \<in> cbox (x - ?d) (x + ?d)"
   1.173      then have "inverse (2 * d) *\<^sub>R (y - (x - ?d)) \<in> cbox 0 (\<Sum>Basis)"
   1.174        using assms by (simp add: mem_box field_simps inner_simps)
   1.175 -    with \<open>0 < d\<close> show "\<exists>z\<in>cbox 0 (\<Sum>Basis). y = x - ?d + (2 * d) *\<^sub>R z"
   1.176 -      by (intro bexI[of _ "inverse (2 * d) *\<^sub>R (y - (x - ?d))"]) auto
   1.177 +    with \<open>0 < d\<close> show "y \<in> (\<lambda>y. x - sum (( *\<^sub>R) d) Basis + (2 * d) *\<^sub>R y) ` cbox 0 One"
   1.178 +      by (auto intro: image_eqI[where x= "inverse (2 * d) *\<^sub>R (y - (x - ?d))"])
   1.179    next
   1.180 -    fix y z
   1.181 -    assume as: "z\<in>cbox 0 (\<Sum>Basis)" "y = x - ?d + (2*d) *\<^sub>R z"
   1.182 -    have "\<And>i. i\<in>Basis \<Longrightarrow> 0 \<le> d * (z \<bullet> i) \<and> d * (z \<bullet> i) \<le> d"
   1.183 -      using assms as(1)[unfolded mem_box]
   1.184 +    fix y
   1.185 +    assume "y \<in> (\<lambda>y. x - ?d + (2 * d) *\<^sub>R y) ` cbox 0 One"
   1.186 +    then obtain z where z: "z \<in> cbox 0 One" "y = x - ?d + (2*d) *\<^sub>R z"
   1.187        by auto
   1.188      then show "y \<in> cbox (x - ?d) (x + ?d)"
   1.189 -      unfolding as(2) mem_box
   1.190 -      apply -
   1.191 -      apply rule
   1.192 -      using as(1)[unfolded mem_box]
   1.193 -      apply (erule_tac x=i in ballE)
   1.194 -      using assms
   1.195 -      apply (auto simp: inner_simps)
   1.196 -      done
   1.197 +      using z assms by (auto simp: mem_box inner_simps)
   1.198    qed
   1.199 -  obtain s where "finite s" "cbox 0 (\<Sum>Basis::'a) = convex hull s"
   1.200 +  obtain S where "finite S" "cbox 0 (\<Sum>Basis::'a) = convex hull S"
   1.201      using unit_cube_convex_hull by auto
   1.202    then show ?thesis
   1.203 -    apply (rule_tac that[of "(\<lambda>y. x - ?d + (2 * d) *\<^sub>R y)` s"])
   1.204 -    unfolding * and convex_hull_affinity
   1.205 -    apply auto
   1.206 -    done
   1.207 +    by (rule_tac that[of "(\<lambda>y. x - ?d + (2 * d) *\<^sub>R y)` S"]) (auto simp: convex_hull_affinity *)
   1.208  qed
   1.209  
   1.210  subsection%unimportant\<open>Representation of any interval as a finite convex hull\<close>
   1.211 @@ -6635,18 +6614,18 @@
   1.212  
   1.213  lemma closed_interval_as_convex_hull:
   1.214    fixes a :: "'a::euclidean_space"
   1.215 -  obtains s where "finite s" "cbox a b = convex hull s"
   1.216 +  obtains S where "finite S" "cbox a b = convex hull S"
   1.217  proof (cases "cbox a b = {}")
   1.218    case True with convex_hull_empty that show ?thesis
   1.219      by blast
   1.220  next
   1.221    case False
   1.222 -  obtain s::"'a set" where "finite s" and eq: "cbox 0 One = convex hull s"
   1.223 +  obtain S::"'a set" where "finite S" and eq: "cbox 0 One = convex hull S"
   1.224      by (blast intro: unit_cube_convex_hull)
   1.225    have lin: "linear (\<lambda>x. \<Sum>k\<in>Basis. ((b \<bullet> k - a \<bullet> k) * (x \<bullet> k)) *\<^sub>R k)"
   1.226      by (rule linear_compose_sum) (auto simp: algebra_simps linearI)
   1.227 -  have "finite ((+) a ` (\<lambda>x. \<Sum>k\<in>Basis. ((b \<bullet> k - a \<bullet> k) * (x \<bullet> k)) *\<^sub>R k) ` s)"
   1.228 -    by (rule finite_imageI \<open>finite s\<close>)+
   1.229 +  have "finite ((+) a ` (\<lambda>x. \<Sum>k\<in>Basis. ((b \<bullet> k - a \<bullet> k) * (x \<bullet> k)) *\<^sub>R k) ` S)"
   1.230 +    by (rule finite_imageI \<open>finite S\<close>)+
   1.231    then show ?thesis
   1.232      apply (rule that)
   1.233      apply (simp add: convex_hull_translation convex_hull_linear_image [OF lin, symmetric])
   1.234 @@ -6658,31 +6637,23 @@
   1.235  subsection%unimportant \<open>Bounded convex function on open set is continuous\<close>
   1.236  
   1.237  lemma convex_on_bounded_continuous:
   1.238 -  fixes s :: "('a::real_normed_vector) set"
   1.239 -  assumes "open s"
   1.240 -    and "convex_on s f"
   1.241 -    and "\<forall>x\<in>s. \<bar>f x\<bar> \<le> b"
   1.242 -  shows "continuous_on s f"
   1.243 +  fixes S :: "('a::real_normed_vector) set"
   1.244 +  assumes "open S"
   1.245 +    and "convex_on S f"
   1.246 +    and "\<forall>x\<in>S. \<bar>f x\<bar> \<le> b"
   1.247 +  shows "continuous_on S f"
   1.248    apply (rule continuous_at_imp_continuous_on)
   1.249    unfolding continuous_at_real_range
   1.250  proof (rule,rule,rule)
   1.251    fix x and e :: real
   1.252 -  assume "x \<in> s" "e > 0"
   1.253 +  assume "x \<in> S" "e > 0"
   1.254    define B where "B = \<bar>b\<bar> + 1"
   1.255 -  have B: "0 < B" "\<And>x. x\<in>s \<Longrightarrow> \<bar>f x\<bar> \<le> B"
   1.256 -    unfolding B_def
   1.257 -    defer
   1.258 -    apply (drule assms(3)[rule_format])
   1.259 -    apply auto
   1.260 -    done
   1.261 -  obtain k where "k > 0" and k: "cball x k \<subseteq> s"
   1.262 -    using assms(1)[unfolded open_contains_cball, THEN bspec[where x=x]]
   1.263 -    using \<open>x\<in>s\<close> by auto
   1.264 +  then have B:  "0 < B""\<And>x. x\<in>S \<Longrightarrow> \<bar>f x\<bar> \<le> B"
   1.265 +    using assms(3) by auto 
   1.266 +  obtain k where "k > 0" and k: "cball x k \<subseteq> S"
   1.267 +    using \<open>x \<in> S\<close> assms(1) open_contains_cball_eq by blast
   1.268    show "\<exists>d>0. \<forall>x'. norm (x' - x) < d \<longrightarrow> \<bar>f x' - f x\<bar> < e"
   1.269 -    apply (rule_tac x="min (k / 2) (e / (2 * B) * k)" in exI)
   1.270 -    apply rule
   1.271 -    defer
   1.272 -  proof (rule, rule)
   1.273 +  proof (intro exI conjI allI impI)
   1.274      fix y
   1.275      assume as: "norm (y - x) < min (k / 2) (e / (2 * B) * k)"
   1.276      show "\<bar>f y - f x\<bar> < e"
   1.277 @@ -6692,22 +6663,16 @@
   1.278        have "2 < t" "0<t"
   1.279          unfolding t_def using as False and \<open>k>0\<close>
   1.280          by (auto simp:field_simps)
   1.281 -      have "y \<in> s"
   1.282 -        apply (rule k[unfolded subset_eq,rule_format])
   1.283 +      have "y \<in> S"
   1.284 +        apply (rule k[THEN subsetD])
   1.285          unfolding mem_cball dist_norm
   1.286          apply (rule order_trans[of _ "2 * norm (x - y)"])
   1.287          using as
   1.288          by (auto simp: field_simps norm_minus_commute)
   1.289        {
   1.290          define w where "w = x + t *\<^sub>R (y - x)"
   1.291 -        have "w \<in> s"
   1.292 -          unfolding w_def
   1.293 -          apply (rule k[unfolded subset_eq,rule_format])
   1.294 -          unfolding mem_cball dist_norm
   1.295 -          unfolding t_def
   1.296 -          using \<open>k>0\<close>
   1.297 -          apply auto
   1.298 -          done
   1.299 +        have "w \<in> S"
   1.300 +          using \<open>k>0\<close> by (auto simp: dist_norm t_def w_def k[THEN subsetD])
   1.301          have "(1 / t) *\<^sub>R x + - x + ((t - 1) / t) *\<^sub>R x = (1 / t - 1 + (t - 1) / t) *\<^sub>R x"
   1.302            by (auto simp: algebra_simps)
   1.303          also have "\<dots> = 0"
   1.304 @@ -6720,23 +6685,17 @@
   1.305            by (auto simp:field_simps)
   1.306          have "f y - f x \<le> (f w - f x) / t"
   1.307            using assms(2)[unfolded convex_on_def,rule_format,of w x "1/t" "(t - 1)/t", unfolded w]
   1.308 -          using \<open>0 < t\<close> \<open>2 < t\<close> and \<open>x \<in> s\<close> \<open>w \<in> s\<close>
   1.309 +          using \<open>0 < t\<close> \<open>2 < t\<close> and \<open>x \<in> S\<close> \<open>w \<in> S\<close>
   1.310            by (auto simp:field_simps)
   1.311          also have "... < e"
   1.312 -          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)
   1.313 +          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)
   1.314          finally have th1: "f y - f x < e" .
   1.315        }
   1.316        moreover
   1.317        {
   1.318          define w where "w = x - t *\<^sub>R (y - x)"
   1.319 -        have "w \<in> s"
   1.320 -          unfolding w_def
   1.321 -          apply (rule k[unfolded subset_eq,rule_format])
   1.322 -          unfolding mem_cball dist_norm
   1.323 -          unfolding t_def
   1.324 -          using \<open>k > 0\<close>
   1.325 -          apply auto
   1.326 -          done
   1.327 +        have "w \<in> S"
   1.328 +          using \<open>k > 0\<close> by (auto simp: dist_norm t_def w_def k[THEN subsetD])
   1.329          have "(1 / (1 + t)) *\<^sub>R x + (t / (1 + t)) *\<^sub>R x = (1 / (1 + t) + t / (1 + t)) *\<^sub>R x"
   1.330            by (auto simp: algebra_simps)
   1.331          also have "\<dots> = x"
   1.332 @@ -6749,12 +6708,12 @@
   1.333            using \<open>0 < e\<close> \<open>0 < k\<close> \<open>B > 0\<close> and as and False
   1.334            by (auto simp:field_simps)
   1.335          then have *: "(f w - f y) / t < e"
   1.336 -          using B(2)[OF \<open>w\<in>s\<close>] and B(2)[OF \<open>y\<in>s\<close>]
   1.337 +          using B(2)[OF \<open>w\<in>S\<close>] and B(2)[OF \<open>y\<in>S\<close>]
   1.338            using \<open>t > 0\<close>
   1.339            by (auto simp:field_simps)
   1.340          have "f x \<le> 1 / (1 + t) * f w + (t / (1 + t)) * f y"
   1.341            using assms(2)[unfolded convex_on_def,rule_format,of w y "1/(1+t)" "t / (1+t)",unfolded w]
   1.342 -          using \<open>0 < t\<close> \<open>2 < t\<close> and \<open>y \<in> s\<close> \<open>w \<in> s\<close>
   1.343 +          using \<open>0 < t\<close> \<open>2 < t\<close> and \<open>y \<in> S\<close> \<open>w \<in> S\<close>
   1.344            by (auto simp:field_simps)
   1.345          also have "\<dots> = (f w + t * f y) / (1 + t)"
   1.346            using \<open>t > 0\<close> by (auto simp: divide_simps)
   1.347 @@ -6843,11 +6802,7 @@
   1.348        by (simp add: dist_norm abs_le_iff algebra_simps)
   1.349      show "cball x d \<subseteq> convex hull c"
   1.350        unfolding 2
   1.351 -      apply clarsimp
   1.352 -      apply (simp only: dist_norm)
   1.353 -      apply (subst inner_diff_left [symmetric], simp)
   1.354 -      apply (erule (1) order_trans [OF Basis_le_norm])
   1.355 -      done
   1.356 +      by (clarsimp simp: dist_norm) (metis inner_commute inner_diff_right norm_bound_Basis_le)
   1.357      have e': "e = (\<Sum>(i::'a)\<in>Basis. d)"
   1.358        by (simp add: d_def DIM_positive)
   1.359      show "convex hull c \<subseteq> cball x e"
     2.1 --- a/src/HOL/Analysis/Derivative.thy	Sun Apr 29 21:26:57 2018 +0100
     2.2 +++ b/src/HOL/Analysis/Derivative.thy	Mon Apr 30 22:13:04 2018 +0100
     2.3 @@ -373,77 +373,76 @@
     2.4  
     2.5  lemma frechet_derivative_unique_within:
     2.6    fixes f :: "'a::euclidean_space \<Rightarrow> 'b::real_normed_vector"
     2.7 -  assumes "(f has_derivative f') (at x within s)"
     2.8 -    and "(f has_derivative f'') (at x within s)"
     2.9 -    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"
    2.10 +  assumes "(f has_derivative f') (at x within S)"
    2.11 +    and "(f has_derivative f'') (at x within S)"
    2.12 +    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"
    2.13    shows "f' = f''"
    2.14  proof -
    2.15    note as = assms(1,2)[unfolded has_derivative_def]
    2.16    then interpret f': bounded_linear f' by auto
    2.17    from as interpret f'': bounded_linear f'' by auto
    2.18 -  have "x islimpt s" unfolding islimpt_approachable
    2.19 +  have "x islimpt S" unfolding islimpt_approachable
    2.20    proof (rule, rule)
    2.21      fix e :: real
    2.22      assume "e > 0"
    2.23 -    obtain d where "0 < \<bar>d\<bar>" and "\<bar>d\<bar> < e" and "x + d *\<^sub>R (SOME i. i \<in> Basis) \<in> s"
    2.24 +    obtain d where "0 < \<bar>d\<bar>" and "\<bar>d\<bar> < e" and "x + d *\<^sub>R (SOME i. i \<in> Basis) \<in> S"
    2.25        using assms(3) SOME_Basis \<open>e>0\<close> by blast
    2.26 -    then show "\<exists>x'\<in>s. x' \<noteq> x \<and> dist x' x < e"
    2.27 +    then show "\<exists>x'\<in>S. x' \<noteq> x \<and> dist x' x < e"
    2.28        apply (rule_tac x="x + d *\<^sub>R (SOME i. i \<in> Basis)" in bexI)
    2.29        unfolding dist_norm
    2.30        apply (auto simp: SOME_Basis nonzero_Basis)
    2.31        done
    2.32    qed
    2.33 -  then have *: "netlimit (at x within s) = x"
    2.34 +  then have *: "netlimit (at x within S) = x"
    2.35      apply (auto intro!: netlimit_within)
    2.36      by (metis trivial_limit_within)
    2.37    show ?thesis
    2.38 -    apply (rule linear_eq_stdbasis)
    2.39 -    unfolding linear_conv_bounded_linear
    2.40 -    apply (rule as(1,2)[THEN conjunct1])+
    2.41 -  proof (rule, rule ccontr)
    2.42 +  proof (rule linear_eq_stdbasis)
    2.43 +    show "linear f'" "linear f''"
    2.44 +      unfolding linear_conv_bounded_linear using as by auto
    2.45 +  next
    2.46      fix i :: 'a
    2.47      assume i: "i \<in> Basis"
    2.48      define e where "e = norm (f' i - f'' i)"
    2.49 -    assume "f' i \<noteq> f'' i"
    2.50 -    then have "e > 0"
    2.51 -      unfolding e_def by auto
    2.52 -    obtain d where d:
    2.53 -      "0 < d"
    2.54 -      "(\<And>xa. xa\<in>s \<longrightarrow> 0 < dist xa x \<and> dist xa x < d \<longrightarrow>
    2.55 -          dist ((f xa - f x - f' (xa - x)) /\<^sub>R norm (xa - x) -
    2.56 -              (f xa - f x - f'' (xa - x)) /\<^sub>R norm (xa - x)) (0 - 0) < e)"
    2.57 -      using tendsto_diff [OF as(1,2)[THEN conjunct2]]
    2.58 -      unfolding * Lim_within
    2.59 -      using \<open>e>0\<close> by blast
    2.60 -    obtain c where c: "0 < \<bar>c\<bar>" "\<bar>c\<bar> < d \<and> x + c *\<^sub>R i \<in> s"
    2.61 -      using assms(3) i d(1) by blast
    2.62 -    have *: "norm (- ((1 / \<bar>c\<bar>) *\<^sub>R f' (c *\<^sub>R i)) + (1 / \<bar>c\<bar>) *\<^sub>R f'' (c *\<^sub>R i)) =
    2.63 +    show "f' i = f'' i"
    2.64 +    proof (rule ccontr)
    2.65 +      assume "f' i \<noteq> f'' i"
    2.66 +      then have "e > 0"
    2.67 +        unfolding e_def by auto
    2.68 +      obtain d where d:
    2.69 +        "0 < d"
    2.70 +        "(\<And>y. y\<in>S \<longrightarrow> 0 < dist y x \<and> dist y x < d \<longrightarrow>
    2.71 +          dist ((f y - f x - f' (y - x)) /\<^sub>R norm (y - x) -
    2.72 +              (f y - f x - f'' (y - x)) /\<^sub>R norm (y - x)) (0 - 0) < e)"
    2.73 +        using tendsto_diff [OF as(1,2)[THEN conjunct2]]
    2.74 +        unfolding * Lim_within
    2.75 +        using \<open>e>0\<close> by blast
    2.76 +      obtain c where c: "0 < \<bar>c\<bar>" "\<bar>c\<bar> < d \<and> x + c *\<^sub>R i \<in> S"
    2.77 +        using assms(3) i d(1) by blast
    2.78 +      have *: "norm (- ((1 / \<bar>c\<bar>) *\<^sub>R f' (c *\<^sub>R i)) + (1 / \<bar>c\<bar>) *\<^sub>R f'' (c *\<^sub>R i)) =
    2.79          norm ((1 / \<bar>c\<bar>) *\<^sub>R (- (f' (c *\<^sub>R i)) + f'' (c *\<^sub>R i)))"
    2.80 -      unfolding scaleR_right_distrib by auto
    2.81 -    also have "\<dots> = norm ((1 / \<bar>c\<bar>) *\<^sub>R (c *\<^sub>R (- (f' i) + f'' i)))"
    2.82 -      unfolding f'.scaleR f''.scaleR
    2.83 -      unfolding scaleR_right_distrib scaleR_minus_right
    2.84 -      by auto
    2.85 -    also have "\<dots> = e"
    2.86 -      unfolding e_def
    2.87 -      using c(1)
    2.88 -      using norm_minus_cancel[of "f' i - f'' i"]
    2.89 -      by auto
    2.90 -    finally show False
    2.91 -      using c
    2.92 -      using d(2)[of "x + c *\<^sub>R i"]
    2.93 -      unfolding dist_norm
    2.94 -      unfolding f'.scaleR f''.scaleR f'.add f''.add f'.diff f''.diff
    2.95 -        scaleR_scaleR scaleR_right_diff_distrib scaleR_right_distrib
    2.96 -      using i
    2.97 -      by (auto simp: inverse_eq_divide)
    2.98 +        unfolding scaleR_right_distrib by auto
    2.99 +      also have "\<dots> = norm ((1 / \<bar>c\<bar>) *\<^sub>R (c *\<^sub>R (- (f' i) + f'' i)))"
   2.100 +        unfolding f'.scaleR f''.scaleR
   2.101 +        unfolding scaleR_right_distrib scaleR_minus_right
   2.102 +        by auto
   2.103 +      also have "\<dots> = e"
   2.104 +        unfolding e_def
   2.105 +        using c(1)
   2.106 +        using norm_minus_cancel[of "f' i - f'' i"]
   2.107 +        by auto
   2.108 +      finally show False
   2.109 +        using c
   2.110 +        using d(2)[of "x + c *\<^sub>R i"]
   2.111 +        unfolding dist_norm
   2.112 +        unfolding f'.scaleR f''.scaleR f'.add f''.add f'.diff f''.diff
   2.113 +          scaleR_scaleR scaleR_right_diff_distrib scaleR_right_distrib
   2.114 +        using i
   2.115 +        by (auto simp: inverse_eq_divide)
   2.116 +    qed
   2.117    qed
   2.118  qed
   2.119  
   2.120 -lemma frechet_derivative_unique_at:
   2.121 -  "(f has_derivative f') (at x) \<Longrightarrow> (f has_derivative f'') (at x) \<Longrightarrow> f' = f''"
   2.122 -  by (rule has_derivative_unique)
   2.123 -
   2.124  lemma frechet_derivative_unique_within_closed_interval:
   2.125    fixes f::"'a::euclidean_space \<Rightarrow> 'b::real_normed_vector"
   2.126    assumes "\<forall>i\<in>Basis. a\<bullet>i < b\<bullet>i"
   2.127 @@ -506,12 +505,12 @@
   2.128    from assms(1) have *: "at x within box a b = at x"
   2.129      by (metis at_within_interior interior_open open_box)
   2.130    from assms(2,3) [unfolded *] show "f' = f''"
   2.131 -    by (rule frechet_derivative_unique_at)
   2.132 +    by (rule has_derivative_unique)
   2.133  qed
   2.134  
   2.135  lemma frechet_derivative_at:
   2.136    "(f has_derivative f') (at x) \<Longrightarrow> f' = frechet_derivative f (at x)"
   2.137 -  apply (rule frechet_derivative_unique_at[of f])
   2.138 +  apply (rule has_derivative_unique[of f])
   2.139    apply assumption
   2.140    unfolding frechet_derivative_works[symmetric]
   2.141    using differentiable_def
     3.1 --- a/src/HOL/Analysis/Linear_Algebra.thy	Sun Apr 29 21:26:57 2018 +0100
     3.2 +++ b/src/HOL/Analysis/Linear_Algebra.thy	Mon Apr 30 22:13:04 2018 +0100
     3.3 @@ -72,7 +72,7 @@
     3.4  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)"
     3.5    unfolding hull_def by auto
     3.6  
     3.7 -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"
     3.8 +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"
     3.9    using hull_minimal[of S "{x. P x}" Q]
    3.10    by (auto simp add: subset_eq)
    3.11  
    3.12 @@ -339,20 +339,12 @@
    3.13    unfolding dependent_def by auto
    3.14  
    3.15  lemma (in real_vector) independent_mono: "independent A \<Longrightarrow> B \<subseteq> A \<Longrightarrow> independent B"
    3.16 -  apply (clarsimp simp add: dependent_def span_mono)
    3.17 -  apply (subgoal_tac "span (B - {a}) \<le> span (A - {a})")
    3.18 -  apply force
    3.19 -  apply (rule span_mono)
    3.20 -  apply auto
    3.21 -  done
    3.22 +  unfolding dependent_def span_mono
    3.23 +  by (metis insert_Diff local.span_mono subsetCE subset_insert_iff) 
    3.24  
    3.25  lemma (in real_vector) span_subspace: "A \<subseteq> B \<Longrightarrow> B \<le> span A \<Longrightarrow>  subspace B \<Longrightarrow> span A = B"
    3.26    by (metis order_antisym span_def hull_minimal)
    3.27  
    3.28 -lemma (in real_vector) span_induct':
    3.29 -  "\<forall>x \<in> S. P x \<Longrightarrow> subspace {x. P x} \<Longrightarrow> \<forall>x \<in> span S. P x"
    3.30 -  unfolding span_def by (rule hull_induct) auto
    3.31 -
    3.32  inductive_set (in real_vector) span_induct_alt_help for S :: "'a set"
    3.33  where
    3.34    span_induct_alt_help_0: "0 \<in> span_induct_alt_help S"
    3.35 @@ -1063,19 +1055,19 @@
    3.36    done
    3.37  
    3.38  lemma linear_eq_0_span:
    3.39 -  assumes lf: "linear f" and f0: "\<forall>x\<in>B. f x = 0"
    3.40 -  shows "\<forall>x \<in> span B. f x = 0"
    3.41 -  using f0 subspace_kernel[OF lf]
    3.42 -  by (rule span_induct')
    3.43 -
    3.44 -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"
    3.45 -  using linear_eq_0_span[of f B] by auto
    3.46 -
    3.47 -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"
    3.48 -  using linear_eq_0_span[of "\<lambda>x. f x - g x" B] by (auto simp: linear_compose_sub)
    3.49 -
    3.50 -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"
    3.51 -  using linear_eq_span[of f g B] by auto
    3.52 +  assumes x: "x \<in> span B" and lf: "linear f" and f0: "\<And>x. x\<in>B \<Longrightarrow> f x = 0"
    3.53 +  shows "f x = 0"
    3.54 +  using x f0 subspace_kernel[OF lf] span_induct
    3.55 +  by blast
    3.56 +
    3.57 +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"
    3.58 +  using linear_eq_0_span[of x B f] by auto
    3.59 +
    3.60 +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"
    3.61 +  using linear_eq_0_span[of x B "\<lambda>x. f x - g x"]  by (auto simp: linear_compose_sub)
    3.62 +
    3.63 +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"
    3.64 +  using linear_eq_span[of _ B f g] by auto
    3.65  
    3.66  text \<open>The degenerate case of the Exchange Lemma.\<close>
    3.67  
    3.68 @@ -1174,13 +1166,13 @@
    3.69    have fB: "inj_on f B"
    3.70      using fi by (auto simp: \<open>span S = span B\<close> intro: subset_inj_on span_superset)
    3.71  
    3.72 -  have "\<forall>x\<in>span B. g (f x) = x"
    3.73 -  proof (intro linear_eq_span)
    3.74 +  have "g (f x) = x" if "x \<in> span B" for x
    3.75 +  proof (rule linear_eq_span)
    3.76      show "linear (\<lambda>x. x)" "linear (\<lambda>x. g (f x))"
    3.77        using linear_id linear_compose[OF \<open>linear f\<close> \<open>linear g\<close>] by (auto simp: id_def comp_def)
    3.78 -    show "\<forall>x \<in> B. g (f x) = x"
    3.79 -      using g fi \<open>span S = span B\<close> by (auto simp: fB)
    3.80 -  qed
    3.81 +    show "g (f x) = x" if "x \<in> B" for x
    3.82 +      using g fi \<open>span S = span B\<close>   by (simp add: fB that)
    3.83 +  qed (rule that)
    3.84    moreover
    3.85    have "inv_into B f ` f ` B \<subseteq> B"
    3.86      by (auto simp: fB)
    3.87 @@ -1210,8 +1202,7 @@
    3.88    ultimately have "\<forall>x\<in>B. f (g x) = x"
    3.89      by auto
    3.90    then have "\<forall>x\<in>span B. f (g x) = x"
    3.91 -    using linear_id linear_compose[OF \<open>linear g\<close> \<open>linear f\<close>]
    3.92 -    by (intro linear_eq_span) (auto simp: id_def comp_def)
    3.93 +    using linear_id linear_compose[OF \<open>linear g\<close> \<open>linear f\<close>] linear_eq_span by fastforce
    3.94    moreover have "inv_into (span S) f ` B \<subseteq> span S"
    3.95      using \<open>B \<subseteq> T\<close> \<open>span T \<subseteq> f`span S\<close> by (auto intro: inv_into_into span_superset)
    3.96    then have "range g \<subseteq> span S"
    3.97 @@ -2457,8 +2448,8 @@
    3.98      done
    3.99    with a have a0:"?a  \<noteq> 0"
   3.100      by auto
   3.101 -  have "\<forall>x\<in>span B. ?a \<bullet> x = 0"
   3.102 -  proof (rule span_induct')
   3.103 +  have "?a \<bullet> x = 0" if "x\<in>span B" for x
   3.104 +  proof (rule span_induct [OF that])
   3.105      show "subspace {x. ?a \<bullet> x = 0}"
   3.106        by (auto simp add: subspace_def inner_add)
   3.107    next
   3.108 @@ -2481,9 +2472,9 @@
   3.109            intro: B(5)[unfolded pairwise_def orthogonal_def, rule_format])
   3.110          done
   3.111      }
   3.112 -    then show "\<forall>x \<in> B. ?a \<bullet> x = 0"
   3.113 -      by blast
   3.114 -  qed
   3.115 +    then show "?a \<bullet> x = 0" if "x \<in> B" for x
   3.116 +      using that by blast
   3.117 +    qed
   3.118    with a0 show ?thesis
   3.119      unfolding sSB by (auto intro: exI[where x="?a"])
   3.120  qed
   3.121 @@ -2635,9 +2626,9 @@
   3.122    fixes f :: "'a::euclidean_space \<Rightarrow> _"
   3.123    assumes lf: "linear f"
   3.124      and lg: "linear g"
   3.125 -    and fg: "\<forall>b\<in>Basis. f b = g b"
   3.126 +    and fg: "\<And>b. b \<in> Basis \<Longrightarrow> f b = g b"
   3.127    shows "f = g"
   3.128 -  using linear_eq[OF lf lg, of _ Basis] fg by auto
   3.129 +  using linear_eq[OF _ lf lg, of _ _ Basis] fg by auto
   3.130  
   3.131  text \<open>Similar results for bilinear functions.\<close>
   3.132  
   3.133 @@ -2646,8 +2637,9 @@
   3.134      and bg: "bilinear g"
   3.135      and SB: "S \<subseteq> span B"
   3.136      and TC: "T \<subseteq> span C"
   3.137 -    and fg: "\<forall>x\<in> B. \<forall>y\<in> C. f x y = g x y"
   3.138 -  shows "\<forall>x\<in>S. \<forall>y\<in>T. f x y = g x y "
   3.139 +    and "x\<in>S" "y\<in>T"
   3.140 +    and fg: "\<And>x y. \<lbrakk>x \<in> B; y\<in> C\<rbrakk> \<Longrightarrow> f x y = g x y"
   3.141 +  shows "f x y = g x y"
   3.142  proof -
   3.143    let ?P = "{x. \<forall>y\<in> span C. f x y = g x y}"
   3.144    from bf bg have sp: "subspace ?P"
   3.145 @@ -2655,27 +2647,30 @@
   3.146      by (auto simp add: span_0 bilinear_lzero[OF bf] bilinear_lzero[OF bg] span_add Ball_def
   3.147        intro: bilinear_ladd[OF bf])
   3.148  
   3.149 -  have "\<forall>x \<in> span B. \<forall>y\<in> span C. f x y = g x y"
   3.150 -    apply (rule span_induct' [OF _ sp])
   3.151 -    apply (rule ballI)
   3.152 -    apply (rule span_induct')
   3.153 -    apply (simp add: fg)
   3.154 +  have sfg: "\<And>x. x \<in> B \<Longrightarrow> subspace {a. f x a = g x a}"
   3.155      apply (auto simp add: subspace_def)
   3.156      using bf bg unfolding bilinear_def linear_iff
   3.157 -    apply (auto simp add: span_0 bilinear_rzero[OF bf] bilinear_rzero[OF bg] span_add Ball_def
   3.158 +    apply (auto simp add: bilinear_rzero[OF bf] bilinear_rzero[OF bg] span_add 
   3.159        intro: bilinear_ladd[OF bf])
   3.160      done
   3.161 +  have "\<forall>y\<in> span C. f x y = g x y" if "x \<in> span B" for x
   3.162 +    apply (rule span_induct [OF that sp])
   3.163 +    apply (rule ballI)
   3.164 +    apply (erule span_induct)
   3.165 +    apply (simp_all add: sfg fg)
   3.166 +    done
   3.167    then show ?thesis
   3.168 -    using SB TC by auto
   3.169 +    using SB TC assms by auto
   3.170  qed
   3.171  
   3.172  lemma bilinear_eq_stdbasis:
   3.173    fixes f :: "'a::euclidean_space \<Rightarrow> 'b::euclidean_space \<Rightarrow> _"
   3.174    assumes bf: "bilinear f"
   3.175      and bg: "bilinear g"
   3.176 -    and fg: "\<forall>i\<in>Basis. \<forall>j\<in>Basis. f i j = g i j"
   3.177 +    and fg: "\<And>i j. i \<in> Basis \<Longrightarrow> j \<in> Basis \<Longrightarrow> f i j = g i j"
   3.178    shows "f = g"
   3.179 -  using bilinear_eq[OF bf bg equalityD2[OF span_Basis] equalityD2[OF span_Basis] fg] by blast
   3.180 +  using bilinear_eq[OF bf bg equalityD2[OF span_Basis] equalityD2[OF span_Basis]] fg
   3.181 +  by blast
   3.182  
   3.183  text \<open>An injective map @{typ "'a::euclidean_space \<Rightarrow> 'b::euclidean_space"} is also surjective.\<close>
   3.184  
   3.185 @@ -2695,13 +2690,7 @@
   3.186      apply (rule card_ge_dim_independent)
   3.187      apply blast
   3.188      apply (rule independent_injective_image[OF B(2) lf fi])
   3.189 -    apply (rule order_eq_refl)
   3.190 -    apply (rule sym)
   3.191 -    unfolding d
   3.192 -    apply (rule card_image)
   3.193 -    apply (rule subset_inj_on[OF fi])
   3.194 -    apply blast
   3.195 -    done
   3.196 +    by (metis card_image d fi inj_on_subset order_refl top_greatest)
   3.197    from th show ?thesis
   3.198      unfolding span_linear_image[OF lf] surj_def
   3.199      using B(3) by blast