src/HOL/Analysis/Linear_Algebra.thy
 changeset 68073 fad29d2a17a5 parent 68072 493b818e8e10 parent 68069 36209dfb981e child 68074 8d50467f7555
```     1.1 --- a/src/HOL/Analysis/Linear_Algebra.thy	Wed May 02 13:49:38 2018 +0200
1.2 +++ b/src/HOL/Analysis/Linear_Algebra.thy	Thu May 03 15:07:14 2018 +0200
1.3 @@ -27,22 +27,8 @@
1.4    show "f (s *\<^sub>R v) = s *\<^sub>R (f v)" by (rule f.scale)
1.5  qed
1.6
1.7 -lemma bounded_linearI:
1.8 -  assumes "\<And>x y. f (x + y) = f x + f y"
1.9 -    and "\<And>r x. f (r *\<^sub>R x) = r *\<^sub>R f x"
1.10 -    and "\<And>x. norm (f x) \<le> norm x * K"
1.11 -  shows "bounded_linear f"
1.12 -  using assms by (rule bounded_linear_intro) (* FIXME: duplicate *)
1.13 -
1.14 -lemma finite_Atleast_Atmost_nat[simp]: "finite {f x |x. x\<in> (UNIV::'a::finite set)}"
1.15 -proof -
1.16 -  have eq: "{f x |x. x\<in> UNIV} = f ` UNIV"
1.17 -    by auto
1.18 -  show ?thesis unfolding eq
1.19 -    apply (rule finite_imageI)
1.20 -    apply (rule finite)
1.21 -    done
1.22 -qed
1.23 +lemma finite_Atleast_Atmost_nat[simp]: "finite {f x |x. x \<in> (UNIV::'a::finite set)}"
1.24 +  using finite finite_image_set by blast
1.25
1.26
1.27  subsection%unimportant \<open>More interesting properties of the norm.\<close>
1.28 @@ -123,10 +109,8 @@
1.29  lemma sum_group:
1.30    assumes fS: "finite S" and fT: "finite T" and fST: "f ` S \<subseteq> T"
1.31    shows "sum (\<lambda>y. sum g {x. x \<in> S \<and> f x = y}) T = sum g S"
1.32 -  apply (subst sum_image_gen[OF fS, of g f])
1.33 -  apply (rule sum.mono_neutral_right[OF fT fST])
1.34 -  apply (auto intro: sum.neutral)
1.35 -  done
1.36 +  unfolding sum_image_gen[OF fS, of g f]
1.37 +  by (auto intro: sum.neutral sum.mono_neutral_right[OF fT fST])
1.38
1.39  lemma vector_eq_ldot: "(\<forall>x. x \<bullet> y = x \<bullet> z) \<longleftrightarrow> y = z"
1.40  proof
1.41 @@ -351,12 +335,7 @@
1.42    assumes "\<forall>(n::nat) \<ge> m. (d n :: real) < e n"
1.43      and "\<forall>n \<ge> m. e n \<le> e m"
1.44    shows "\<forall>n \<ge> m. d n < e m"
1.45 -  using assms
1.46 -  apply auto
1.47 -  apply (erule_tac x="n" in allE)
1.48 -  apply (erule_tac x="n" in allE)
1.49 -  apply auto
1.50 -  done
1.51 +  using assms by force
1.52
1.53  lemma infinite_enumerate:
1.54    assumes fS: "infinite S"
1.55 @@ -468,10 +447,7 @@
1.56  next
1.57    case False
1.58    with y x1 show ?thesis
1.59 -    apply auto
1.60 -    apply (rule exI[where x=1])
1.61 -    apply auto
1.62 -    done
1.63 +    by (metis less_le_trans not_less power_one_right)
1.64  qed
1.65
1.66  lemma forall_pos_mono:
1.67 @@ -522,11 +498,7 @@
1.68      proof -
1.69        from Basis_le_norm[OF that, of x]
1.70        show "norm (?g i) \<le> norm (f i) * norm x"
1.71 -        unfolding norm_scaleR
1.72 -        apply (subst mult.commute)
1.73 -        apply (rule mult_mono)
1.74 -        apply (auto simp add: field_simps)
1.75 -        done
1.76 +        unfolding norm_scaleR  by (metis mult.commute mult_left_mono norm_ge_zero)
1.77      qed
1.78      from sum_norm_le[of _ ?g, OF th]
1.79      show "norm (f x) \<le> ?B * norm x"
1.80 @@ -611,23 +583,17 @@
1.81    fix x :: 'm
1.82    fix y :: 'n
1.83    have "norm (h x y) = norm (h (sum (\<lambda>i. (x \<bullet> i) *\<^sub>R i) Basis) (sum (\<lambda>i. (y \<bullet> i) *\<^sub>R i) Basis))"
1.84 -    apply (subst euclidean_representation[where 'a='m])
1.85 -    apply (subst euclidean_representation[where 'a='n])
1.86 -    apply rule
1.87 -    done
1.88 +    by (simp add: euclidean_representation)
1.89    also have "\<dots> = norm (sum (\<lambda> (i,j). h ((x \<bullet> i) *\<^sub>R i) ((y \<bullet> j) *\<^sub>R j)) (Basis \<times> Basis))"
1.90      unfolding bilinear_sum[OF bh] ..
1.91    finally have th: "norm (h x y) = \<dots>" .
1.92 -  show "norm (h x y) \<le> (\<Sum>i\<in>Basis. \<Sum>j\<in>Basis. norm (h i j)) * norm x * norm y"
1.93 -    apply (auto simp add: sum_distrib_right th sum.cartesian_product)
1.94 -    apply (rule sum_norm_le)
1.95 -    apply (auto simp add: bilinear_rmul[OF bh] bilinear_lmul[OF bh]
1.96 -      field_simps simp del: scaleR_scaleR)
1.97 -    apply (rule mult_mono)
1.98 -    apply (auto simp add: zero_le_mult_iff Basis_le_norm)
1.99 -    apply (rule mult_mono)
1.100 -    apply (auto simp add: zero_le_mult_iff Basis_le_norm)
1.101 -    done
1.102 +  have "\<And>i j. \<lbrakk>i \<in> Basis; j \<in> Basis\<rbrakk>
1.103 +           \<Longrightarrow> \<bar>x \<bullet> i\<bar> * (\<bar>y \<bullet> j\<bar> * norm (h i j)) \<le> norm x * (norm y * norm (h i j))"
1.104 +    by (auto simp add: zero_le_mult_iff Basis_le_norm mult_mono)
1.105 +  then show "norm (h x y) \<le> (\<Sum>i\<in>Basis. \<Sum>j\<in>Basis. norm (h i j)) * norm x * norm y"
1.106 +    unfolding sum_distrib_right th sum.cartesian_product
1.107 +    by (clarsimp simp add: bilinear_rmul[OF bh] bilinear_lmul[OF bh]
1.108 +      field_simps simp del: scaleR_scaleR intro!: sum_norm_le)
1.109  qed
1.110
1.111  lemma bilinear_conv_bounded_bilinear:
1.112 @@ -645,15 +611,9 @@
1.113      show "h x (y + z) = h x y + h x z"
1.114        using \<open>bilinear h\<close> unfolding bilinear_def linear_iff by simp
1.115    next
1.116 -    fix r x y
1.117 -    show "h (scaleR r x) y = scaleR r (h x y)"
1.118 +    show "h (scaleR r x) y = scaleR r (h x y)" "h x (scaleR r y) = scaleR r (h x y)" for r x y
1.119        using \<open>bilinear h\<close> unfolding bilinear_def linear_iff
1.120 -      by simp
1.121 -  next
1.122 -    fix r x y
1.123 -    show "h x (scaleR r y) = scaleR r (h x y)"
1.124 -      using \<open>bilinear h\<close> unfolding bilinear_def linear_iff
1.125 -      by simp
1.126 +      by simp_all
1.127    next
1.128      have "\<exists>B. \<forall>x y. norm (h x y) \<le> B * norm x * norm y"
1.129        using \<open>bilinear h\<close> by (rule bilinear_bounded)
1.130 @@ -803,7 +763,7 @@
1.131  proof -
1.132    from basis_exists[of V] obtain B where
1.133      B: "B \<subseteq> V" "independent B" "V \<subseteq> span B" "card B = dim V"
1.134 -    by blast
1.135 +    by force
1.136    from B have fB: "finite B" "card B = dim V"
1.137      using independent_bound by auto
1.138    from basis_orthogonal[OF fB(1)] obtain C where
1.139 @@ -855,8 +815,8 @@
1.140      done
1.141    with a have a0:"?a  \<noteq> 0"
1.142      by auto
1.143 -  have "\<forall>x\<in>span B. ?a \<bullet> x = 0"
1.144 -  proof (rule span_induct')
1.145 +  have "?a \<bullet> x = 0" if "x\<in>span B" for x
1.146 +  proof (rule span_induct [OF that])
1.147      show "subspace {x. ?a \<bullet> x = 0}"
1.148        by (auto simp add: subspace_def inner_add)
1.149    next
1.150 @@ -879,9 +839,9 @@
1.151            intro: B(5)[unfolded pairwise_def orthogonal_def, rule_format])
1.152          done
1.153      }
1.154 -    then show "\<forall>x \<in> B. ?a \<bullet> x = 0"
1.155 -      by blast
1.156 -  qed
1.157 +    then show "?a \<bullet> x = 0" if "x \<in> B" for x
1.158 +      using that by blast
1.159 +    qed
1.160    with a0 show ?thesis
1.161      unfolding sSB by (auto intro: exI[where x="?a"])
1.162  qed
1.163 @@ -927,8 +887,9 @@
1.164      and bg: "bilinear g"
1.165      and SB: "S \<subseteq> span B"
1.166      and TC: "T \<subseteq> span C"
1.167 -    and fg: "\<forall>x\<in> B. \<forall>y\<in> C. f x y = g x y"
1.168 -  shows "\<forall>x\<in>S. \<forall>y\<in>T. f x y = g x y "
1.169 +    and "x\<in>S" "y\<in>T"
1.170 +    and fg: "\<And>x y. \<lbrakk>x \<in> B; y\<in> C\<rbrakk> \<Longrightarrow> f x y = g x y"
1.171 +  shows "f x y = g x y"
1.172  proof -
1.173    let ?P = "{x. \<forall>y\<in> span C. f x y = g x y}"
1.174    from bf bg have sp: "subspace ?P"
1.175 @@ -936,27 +897,25 @@
1.176      by (auto simp add: span_zero bilinear_lzero[OF bf] bilinear_lzero[OF bg]
1.177          span_add Ball_def
1.178        intro: bilinear_ladd[OF bf])
1.179 -
1.180 -  have "\<forall>x \<in> span B. \<forall>y\<in> span C. f x y = g x y"
1.181 -    apply (rule span_induct' [OF _ sp])
1.182 -    apply (rule ballI)
1.183 -    apply (rule span_induct')
1.184 -    apply (simp add: fg)
1.185 +  have sfg: "\<And>x. x \<in> B \<Longrightarrow> subspace {a. f x a = g x a}"
1.186      apply (auto simp add: subspace_def)
1.187      using bf bg unfolding bilinear_def linear_iff
1.188        apply (auto simp add: span_zero bilinear_rzero[OF bf] bilinear_rzero[OF bg]
1.189          span_add Ball_def
1.190        intro: bilinear_ladd[OF bf])
1.191      done
1.192 +  have "\<forall>y\<in> span C. f x y = g x y" if "x \<in> span B" for x
1.193 +    apply (rule span_induct [OF that sp])
1.194 +    using fg sfg span_induct by blast
1.195    then show ?thesis
1.196 -    using SB TC by auto
1.197 +    using SB TC assms by auto
1.198  qed
1.199
1.200  lemma bilinear_eq_stdbasis:
1.201    fixes f :: "'a::euclidean_space \<Rightarrow> 'b::euclidean_space \<Rightarrow> _"
1.202    assumes bf: "bilinear f"
1.203      and bg: "bilinear g"
1.204 -    and fg: "\<forall>i\<in>Basis. \<forall>j\<in>Basis. f i j = g i j"
1.205 +    and fg: "\<And>i j. i \<in> Basis \<Longrightarrow> j \<in> Basis \<Longrightarrow> f i j = g i j"
1.206    shows "f = g"
1.207    using bilinear_eq[OF bf bg equalityD2[OF span_Basis] equalityD2[OF span_Basis] fg] by blast
1.208
1.209 @@ -1010,28 +969,21 @@
1.210    by (simp add: infnorm_eq_0)
1.211
1.212  lemma infnorm_neg: "infnorm (- x) = infnorm x"
1.213 -  unfolding infnorm_def
1.214 -  apply (rule cong[of "Sup" "Sup"])
1.215 -  apply blast
1.216 -  apply auto
1.217 -  done
1.218 +  unfolding infnorm_def by simp
1.219
1.220  lemma infnorm_sub: "infnorm (x - y) = infnorm (y - x)"
1.221 -proof -
1.222 -  have "y - x = - (x - y)" by simp
1.223 -  then show ?thesis
1.224 -    by (metis infnorm_neg)
1.225 -qed
1.226 +  by (metis infnorm_neg minus_diff_eq)
1.227
1.228 -lemma real_abs_sub_infnorm: "\<bar>infnorm x - infnorm y\<bar> \<le> infnorm (x - y)"
1.229 +lemma absdiff_infnorm: "\<bar>infnorm x - infnorm y\<bar> \<le> infnorm (x - y)"
1.230  proof -
1.231 -  have th: "\<And>(nx::real) n ny. nx \<le> n + ny \<Longrightarrow> ny \<le> n + nx \<Longrightarrow> \<bar>nx - ny\<bar> \<le> n"
1.232 +  have *: "\<And>(nx::real) n ny. nx \<le> n + ny \<Longrightarrow> ny \<le> n + nx \<Longrightarrow> \<bar>nx - ny\<bar> \<le> n"
1.233      by arith
1.234 -  from infnorm_triangle[of "x - y" " y"] infnorm_triangle[of "x - y" "-x"]
1.235 -  have ths: "infnorm x \<le> infnorm (x - y) + infnorm y"
1.236 -    "infnorm y \<le> infnorm (x - y) + infnorm x"
1.237 -    by (simp_all add: field_simps infnorm_neg)
1.238 -  from th[OF ths] show ?thesis .
1.239 +  show ?thesis
1.240 +  proof (rule *)
1.241 +    from infnorm_triangle[of "x - y" " y"] infnorm_triangle[of "x - y" "-x"]
1.242 +    show "infnorm x \<le> infnorm (x - y) + infnorm y" "infnorm y \<le> infnorm (x - y) + infnorm x"
1.243 +      by (simp_all add: field_simps infnorm_neg)
1.244 +  qed
1.245  qed
1.246
1.247  lemma real_abs_infnorm: "\<bar>infnorm x\<bar> = infnorm x"
1.248 @@ -1046,8 +998,7 @@
1.249    unfolding infnorm_Max
1.250  proof (safe intro!: Max_eqI)
1.251    let ?B = "(\<lambda>i. \<bar>x \<bullet> i\<bar>) ` Basis"
1.252 -  {
1.253 -    fix b :: 'a
1.254 +  { fix b :: 'a
1.255      assume "b \<in> Basis"
1.256      then show "\<bar>a *\<^sub>R x \<bullet> b\<bar> \<le> \<bar>a\<bar> * Max ?B"
1.257        by (simp add: abs_mult mult_left_mono)
1.258 @@ -1073,27 +1024,17 @@
1.259  lemma norm_le_infnorm:
1.260    fixes x :: "'a::euclidean_space"
1.261    shows "norm x \<le> sqrt DIM('a) * infnorm x"
1.262 -proof -
1.263 -  let ?d = "DIM('a)"
1.264 -  have "real ?d \<ge> 0"
1.265 -    by simp
1.266 -  then have d2: "(sqrt (real ?d))\<^sup>2 = real ?d"
1.267 -    by (auto intro: real_sqrt_pow2)
1.268 -  have th: "sqrt (real ?d) * infnorm x \<ge> 0"
1.269 +  unfolding norm_eq_sqrt_inner id_def
1.270 +proof (rule real_le_lsqrt[OF inner_ge_zero])
1.271 +  show "sqrt DIM('a) * infnorm x \<ge> 0"
1.272      by (simp add: zero_le_mult_iff infnorm_pos_le)
1.273 -  have th1: "x \<bullet> x \<le> (sqrt (real ?d) * infnorm x)\<^sup>2"
1.274 -    unfolding power_mult_distrib d2
1.275 -    apply (subst euclidean_inner)
1.276 -    apply (subst power2_abs[symmetric])
1.277 -    apply (rule order_trans[OF sum_bounded_above[where K="\<bar>infnorm x\<bar>\<^sup>2"]])
1.278 -    apply (auto simp add: power2_eq_square[symmetric])
1.279 -    apply (subst power2_abs[symmetric])
1.280 -    apply (rule power_mono)
1.281 -    apply (auto simp: infnorm_Max)
1.282 -    done
1.283 -  from real_le_lsqrt[OF inner_ge_zero th th1]
1.284 -  show ?thesis
1.285 -    unfolding norm_eq_sqrt_inner id_def .
1.286 +  have "x \<bullet> x \<le> (\<Sum>b\<in>Basis. x \<bullet> b * (x \<bullet> b))"
1.287 +    by (metis euclidean_inner order_refl)
1.288 +  also have "... \<le> DIM('a) * \<bar>infnorm x\<bar>\<^sup>2"
1.289 +    by (rule sum_bounded_above) (metis Basis_le_infnorm abs_le_square_iff power2_eq_square real_abs_infnorm)
1.290 +  also have "... \<le> (sqrt DIM('a) * infnorm x)\<^sup>2"
1.291 +    by (simp add: power_mult_distrib)
1.292 +  finally show "x \<bullet> x \<le> (sqrt DIM('a) * infnorm x)\<^sup>2" .
1.293  qed
1.294
1.295  lemma tendsto_infnorm [tendsto_intros]:
1.296 @@ -1103,46 +1044,30 @@
1.297    fix r :: real
1.298    assume "r > 0"
1.299    then show "\<exists>s>0. \<forall>x. x \<noteq> a \<and> norm (x - a) < s \<longrightarrow> norm (infnorm x - infnorm a) < r"
1.300 -    by (metis real_norm_def le_less_trans real_abs_sub_infnorm infnorm_le_norm)
1.301 +    by (metis real_norm_def le_less_trans absdiff_infnorm infnorm_le_norm)
1.302  qed
1.303
1.304  text \<open>Equality in Cauchy-Schwarz and triangle inequalities.\<close>
1.305
1.306  lemma norm_cauchy_schwarz_eq: "x \<bullet> y = norm x * norm y \<longleftrightarrow> norm x *\<^sub>R y = norm y *\<^sub>R x"
1.307    (is "?lhs \<longleftrightarrow> ?rhs")
1.308 -proof -
1.309 -  {
1.310 -    assume h: "x = 0"
1.311 -    then have ?thesis by simp
1.312 -  }
1.313 -  moreover
1.314 -  {
1.315 -    assume h: "y = 0"
1.316 -    then have ?thesis by simp
1.317 -  }
1.318 -  moreover
1.319 -  {
1.320 -    assume x: "x \<noteq> 0" and y: "y \<noteq> 0"
1.321 -    from inner_eq_zero_iff[of "norm y *\<^sub>R x - norm x *\<^sub>R y"]
1.322 -    have "?rhs \<longleftrightarrow>
1.323 +proof (cases "x=0")
1.324 +  case True
1.325 +  then show ?thesis
1.326 +    by auto
1.327 +next
1.328 +  case False
1.329 +  from inner_eq_zero_iff[of "norm y *\<^sub>R x - norm x *\<^sub>R y"]
1.330 +  have "?rhs \<longleftrightarrow>
1.331        (norm y * (norm y * norm x * norm x - norm x * (x \<bullet> y)) -
1.332          norm x * (norm y * (y \<bullet> x) - norm x * norm y * norm y) =  0)"
1.333 -      using x y
1.334 -      unfolding inner_simps
1.335 -      unfolding power2_norm_eq_inner[symmetric] power2_eq_square right_minus_eq
1.336 -      apply (simp add: inner_commute)
1.337 -      apply (simp add: field_simps)
1.338 -      apply metis
1.339 -      done
1.340 -    also have "\<dots> \<longleftrightarrow> (2 * norm x * norm y * (norm x * norm y - x \<bullet> y) = 0)" using x y
1.341 -      by (simp add: field_simps inner_commute)
1.342 -    also have "\<dots> \<longleftrightarrow> ?lhs" using x y
1.343 -      apply simp
1.344 -      apply metis
1.345 -      done
1.346 -    finally have ?thesis by blast
1.347 -  }
1.348 -  ultimately show ?thesis by blast
1.349 +    using False unfolding inner_simps
1.350 +    by (auto simp add: power2_norm_eq_inner[symmetric] power2_eq_square inner_commute field_simps)
1.351 +  also have "\<dots> \<longleftrightarrow> (2 * norm x * norm y * (norm x * norm y - x \<bullet> y) = 0)"
1.352 +    using False  by (simp add: field_simps inner_commute)
1.353 +  also have "\<dots> \<longleftrightarrow> ?lhs"
1.354 +    using False by auto
1.355 +  finally show ?thesis by metis
1.356  qed
1.357
1.358  lemma norm_cauchy_schwarz_abs_eq:
1.359 @@ -1154,7 +1079,7 @@
1.360      by arith
1.361    have "?rhs \<longleftrightarrow> norm x *\<^sub>R y = norm y *\<^sub>R x \<or> norm (- x) *\<^sub>R y = norm y *\<^sub>R (- x)"
1.362      by simp
1.363 -  also have "\<dots> \<longleftrightarrow>(x \<bullet> y = norm x * norm y \<or> (- x) \<bullet> y = norm x * norm y)"
1.364 +  also have "\<dots> \<longleftrightarrow> (x \<bullet> y = norm x * norm y \<or> (- x) \<bullet> y = norm x * norm y)"
1.365      unfolding norm_cauchy_schwarz_eq[symmetric]
1.366      unfolding norm_minus_cancel norm_scaleR ..
1.367    also have "\<dots> \<longleftrightarrow> ?lhs"
1.368 @@ -1166,33 +1091,21 @@
1.369  lemma norm_triangle_eq:
1.370    fixes x y :: "'a::real_inner"
1.371    shows "norm (x + y) = norm x + norm y \<longleftrightarrow> norm x *\<^sub>R y = norm y *\<^sub>R x"
1.372 -proof -
1.373 -  {
1.374 -    assume x: "x = 0 \<or> y = 0"
1.375 -    then have ?thesis
1.376 -      by (cases "x = 0") simp_all
1.377 -  }
1.378 -  moreover
1.379 -  {
1.380 -    assume x: "x \<noteq> 0" and y: "y \<noteq> 0"
1.381 -    then have "norm x \<noteq> 0" "norm y \<noteq> 0"
1.382 -      by simp_all
1.383 -    then have n: "norm x > 0" "norm y > 0"
1.384 -      using norm_ge_zero[of x] norm_ge_zero[of y] by arith+
1.385 -    have th: "\<And>(a::real) b c. a + b + c \<noteq> 0 \<Longrightarrow> a = b + c \<longleftrightarrow> a\<^sup>2 = (b + c)\<^sup>2"
1.386 -      by algebra
1.387 -    have "norm (x + y) = norm x + norm y \<longleftrightarrow> (norm (x + y))\<^sup>2 = (norm x + norm y)\<^sup>2"
1.388 -      apply (rule th)
1.389 -      using n norm_ge_zero[of "x + y"]
1.390 -      apply arith
1.391 -      done
1.392 -    also have "\<dots> \<longleftrightarrow> norm x *\<^sub>R y = norm y *\<^sub>R x"
1.393 -      unfolding norm_cauchy_schwarz_eq[symmetric]
1.394 -      unfolding power2_norm_eq_inner inner_simps
1.395 -      by (simp add: power2_norm_eq_inner[symmetric] power2_eq_square inner_commute field_simps)
1.396 -    finally have ?thesis .
1.397 -  }
1.398 -  ultimately show ?thesis by blast
1.399 +proof (cases "x = 0 \<or> y = 0")
1.400 +  case True
1.401 +  then show ?thesis
1.402 +    by force
1.403 +next
1.404 +  case False
1.405 +  then have n: "norm x > 0" "norm y > 0"
1.406 +    by auto
1.407 +  have "norm (x + y) = norm x + norm y \<longleftrightarrow> (norm (x + y))\<^sup>2 = (norm x + norm y)\<^sup>2"
1.408 +    by simp
1.409 +  also have "\<dots> \<longleftrightarrow> norm x *\<^sub>R y = norm y *\<^sub>R x"
1.410 +    unfolding norm_cauchy_schwarz_eq[symmetric]
1.411 +    unfolding power2_norm_eq_inner inner_simps
1.412 +    by (simp add: power2_norm_eq_inner[symmetric] power2_eq_square inner_commute field_simps)
1.413 +  finally show ?thesis .
1.414  qed
1.415
1.416
1.417 @@ -1251,81 +1164,67 @@
1.418  lemma collinear_2 [iff]: "collinear {x, y}"
1.419    apply (simp add: collinear_def)
1.420    apply (rule exI[where x="x - y"])
1.421 -  apply auto
1.422 -  apply (rule exI[where x=1], simp)
1.423 -  apply (rule exI[where x="- 1"], simp)
1.424 -  done
1.425 +  by (metis minus_diff_eq scaleR_left.minus scaleR_one)
1.426
1.427  lemma collinear_lemma: "collinear {0, x, y} \<longleftrightarrow> x = 0 \<or> y = 0 \<or> (\<exists>c. y = c *\<^sub>R x)"
1.428    (is "?lhs \<longleftrightarrow> ?rhs")
1.429 -proof -
1.430 -  {
1.431 -    assume "x = 0 \<or> y = 0"
1.432 -    then have ?thesis
1.433 -      by (cases "x = 0") (simp_all add: collinear_2 insert_commute)
1.434 -  }
1.435 -  moreover
1.436 -  {
1.437 -    assume x: "x \<noteq> 0" and y: "y \<noteq> 0"
1.438 -    have ?thesis
1.439 -    proof
1.440 -      assume h: "?lhs"
1.441 -      then obtain u where u: "\<forall> x\<in> {0,x,y}. \<forall>y\<in> {0,x,y}. \<exists>c. x - y = c *\<^sub>R u"
1.442 -        unfolding collinear_def by blast
1.443 -      from u[rule_format, of x 0] u[rule_format, of y 0]
1.444 -      obtain cx and cy where
1.445 -        cx: "x = cx *\<^sub>R u" and cy: "y = cy *\<^sub>R u"
1.446 -        by auto
1.447 -      from cx x have cx0: "cx \<noteq> 0" by auto
1.448 -      from cy y have cy0: "cy \<noteq> 0" by auto
1.449 -      let ?d = "cy / cx"
1.450 -      from cx cy cx0 have "y = ?d *\<^sub>R x"
1.451 -        by simp
1.452 -      then show ?rhs using x y by blast
1.453 -    next
1.454 -      assume h: "?rhs"
1.455 -      then obtain c where c: "y = c *\<^sub>R x"
1.456 -        using x y by blast
1.457 -      show ?lhs
1.458 -        unfolding collinear_def c
1.459 -        apply (rule exI[where x=x])
1.460 -        apply auto
1.461 -        apply (rule exI[where x="- 1"], simp)
1.462 -        apply (rule exI[where x= "-c"], simp)
1.463 +proof (cases "x = 0 \<or> y = 0")
1.464 +  case True
1.465 +  then show ?thesis
1.466 +    by (auto simp: insert_commute)
1.467 +next
1.468 +  case False
1.469 +  show ?thesis
1.470 +  proof
1.471 +    assume h: "?lhs"
1.472 +    then obtain u where u: "\<forall> x\<in> {0,x,y}. \<forall>y\<in> {0,x,y}. \<exists>c. x - y = c *\<^sub>R u"
1.473 +      unfolding collinear_def by blast
1.474 +    from u[rule_format, of x 0] u[rule_format, of y 0]
1.475 +    obtain cx and cy where
1.476 +      cx: "x = cx *\<^sub>R u" and cy: "y = cy *\<^sub>R u"
1.477 +      by auto
1.478 +    from cx cy False have cx0: "cx \<noteq> 0" and cy0: "cy \<noteq> 0" by auto
1.479 +    let ?d = "cy / cx"
1.480 +    from cx cy cx0 have "y = ?d *\<^sub>R x"
1.481 +      by simp
1.482 +    then show ?rhs using False by blast
1.483 +  next
1.484 +    assume h: "?rhs"
1.485 +    then obtain c where c: "y = c *\<^sub>R x"
1.486 +      using False by blast
1.487 +    show ?lhs
1.488 +      unfolding collinear_def c
1.489 +      apply (rule exI[where x=x])
1.490 +      apply auto
1.491 +          apply (rule exI[where x="- 1"], simp)
1.492 +         apply (rule exI[where x= "-c"], simp)
1.493          apply (rule exI[where x=1], simp)
1.494 -        apply (rule exI[where x="1 - c"], simp add: scaleR_left_diff_distrib)
1.495 -        apply (rule exI[where x="c - 1"], simp add: scaleR_left_diff_distrib)
1.496 -        done
1.497 -    qed
1.498 -  }
1.499 -  ultimately show ?thesis by blast
1.500 +       apply (rule exI[where x="1 - c"], simp add: scaleR_left_diff_distrib)
1.501 +      apply (rule exI[where x="c - 1"], simp add: scaleR_left_diff_distrib)
1.502 +      done
1.503 +  qed
1.504  qed
1.505
1.506  lemma norm_cauchy_schwarz_equal: "\<bar>x \<bullet> y\<bar> = norm x * norm y \<longleftrightarrow> collinear {0, x, y}"
1.507 -  unfolding norm_cauchy_schwarz_abs_eq
1.508 -  apply (cases "x=0", simp_all)
1.509 -  apply (cases "y=0", simp_all add: insert_commute)
1.510 -  unfolding collinear_lemma
1.511 -  apply simp
1.512 -  apply (subgoal_tac "norm x \<noteq> 0")
1.513 -  apply (subgoal_tac "norm y \<noteq> 0")
1.514 -  apply (rule iffI)
1.515 -  apply (cases "norm x *\<^sub>R y = norm y *\<^sub>R x")
1.516 -  apply (rule exI[where x="(1/norm x) * norm y"])
1.517 -  apply (drule sym)
1.518 -  unfolding scaleR_scaleR[symmetric]
1.519 -  apply (simp add: field_simps)
1.520 -  apply (rule exI[where x="(1/norm x) * - norm y"])
1.521 -  apply clarify
1.522 -  apply (drule sym)
1.523 -  unfolding scaleR_scaleR[symmetric]
1.524 -  apply (simp add: field_simps)
1.525 -  apply (erule exE)
1.526 -  apply (erule ssubst)
1.527 -  unfolding scaleR_scaleR
1.528 -  unfolding norm_scaleR
1.529 -  apply (subgoal_tac "norm x * c = \<bar>c\<bar> * norm x \<or> norm x * c = - \<bar>c\<bar> * norm x")
1.530 -  apply (auto simp add: field_simps)
1.531 -  done
1.532 +proof (cases "x=0")
1.533 +  case True
1.534 +  then show ?thesis
1.535 +    by (auto simp: insert_commute)
1.536 +next
1.537 +  case False
1.538 +  then have nnz: "norm x \<noteq> 0"
1.539 +    by auto
1.540 +  show ?thesis
1.541 +  proof
1.542 +    assume "\<bar>x \<bullet> y\<bar> = norm x * norm y"
1.543 +    then show "collinear {0, x, y}"
1.544 +      unfolding norm_cauchy_schwarz_abs_eq collinear_lemma
1.545 +      by (meson eq_vector_fraction_iff nnz)
1.546 +  next
1.547 +    assume "collinear {0, x, y}"
1.548 +    with False show "\<bar>x \<bullet> y\<bar> = norm x * norm y"
1.549 +      unfolding norm_cauchy_schwarz_abs_eq collinear_lemma  by (auto simp: abs_if)
1.550 +  qed
1.551 +qed
1.552
1.553  end
```