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