simplified some messy proofs
authorpaulson <lp15@cam.ac.uk>
Tue May 01 23:25:00 2018 +0100 (12 months ago)
changeset 68062ee88c0fccbae
parent 68060 3931ed905e93
child 68063 539048827fe8
simplified some messy proofs
src/HOL/Analysis/Cartesian_Euclidean_Space.thy
src/HOL/Analysis/Linear_Algebra.thy
     1.1 --- a/src/HOL/Analysis/Cartesian_Euclidean_Space.thy	Tue May 01 16:42:14 2018 +0200
     1.2 +++ b/src/HOL/Analysis/Cartesian_Euclidean_Space.thy	Tue May 01 23:25:00 2018 +0100
     1.3 @@ -1956,7 +1956,7 @@
     1.4    done
     1.5  
     1.6  lemma bounded_linear_component_cart[intro]: "bounded_linear (\<lambda>x::real^'n. x $ k)"
     1.7 -  apply (rule bounded_linearI[where K=1])
     1.8 +  apply (rule bounded_linear_intro[where K=1])
     1.9    using component_le_norm_cart[of _ k] unfolding real_norm_def by auto
    1.10  
    1.11  lemma interval_split_cart:
     2.1 --- a/src/HOL/Analysis/Linear_Algebra.thy	Tue May 01 16:42:14 2018 +0200
     2.2 +++ b/src/HOL/Analysis/Linear_Algebra.thy	Tue May 01 23:25:00 2018 +0100
     2.3 @@ -27,13 +27,6 @@
     2.4    show "f (s *\<^sub>R v) = s *\<^sub>R (f v)" by (rule f.scaleR)
     2.5  qed
     2.6  
     2.7 -lemma bounded_linearI:
     2.8 -  assumes "\<And>x y. f (x + y) = f x + f y"
     2.9 -    and "\<And>r x. f (r *\<^sub>R x) = r *\<^sub>R f x"
    2.10 -    and "\<And>x. norm (f x) \<le> norm x * K"
    2.11 -  shows "bounded_linear f"
    2.12 -  using assms by (rule bounded_linear_intro) (* FIXME: duplicate *)
    2.13 -
    2.14  subsection \<open>A generic notion of "hull" (convex, affine, conic hull and closure).\<close>
    2.15  
    2.16  definition%important hull :: "('a set \<Rightarrow> bool) \<Rightarrow> 'a set \<Rightarrow> 'a set"  (infixl "hull" 75)
    2.17 @@ -2514,35 +2507,27 @@
    2.18      and fx: "f x = 0"
    2.19    shows "x = 0"
    2.20    using fB ifB fi xsB fx
    2.21 -proof (induct arbitrary: x rule: finite_induct[OF fB])
    2.22 -  case 1
    2.23 +proof (induction B arbitrary: x rule: finite_induct)
    2.24 +  case empty
    2.25    then show ?case by auto
    2.26  next
    2.27 -  case (2 a b x)
    2.28 -  have fb: "finite b" using "2.prems" by simp
    2.29 +  case (insert a b x)
    2.30    have th0: "f ` b \<subseteq> f ` (insert a b)"
    2.31 -    apply (rule image_mono)
    2.32 -    apply blast
    2.33 -    done
    2.34 -  from independent_mono[ OF "2.prems"(2) th0]
    2.35 -  have ifb: "independent (f ` b)"  .
    2.36 +    by (simp add: subset_insertI)
    2.37 +  have ifb: "independent (f ` b)"
    2.38 +    using independent_mono insert.prems(1) th0 by blast  
    2.39    have fib: "inj_on f b"
    2.40 -    apply (rule subset_inj_on [OF "2.prems"(3)])
    2.41 -    apply blast
    2.42 -    done
    2.43 -  from span_breakdown[of a "insert a b", simplified, OF "2.prems"(4)]
    2.44 +    using insert.prems(2) by blast
    2.45 +  from span_breakdown[of a "insert a b", simplified, OF insert.prems(3)]
    2.46    obtain k where k: "x - k*\<^sub>R a \<in> span (b - {a})"
    2.47      by blast
    2.48    have "f (x - k*\<^sub>R a) \<in> span (f ` b)"
    2.49      unfolding span_linear_image[OF lf]
    2.50 -    apply (rule imageI)
    2.51 -    using k span_mono[of "b - {a}" b]
    2.52 -    apply blast
    2.53 -    done
    2.54 +    using "insert.hyps"(2) k by auto
    2.55    then have "f x - k*\<^sub>R f a \<in> span (f ` b)"
    2.56      by (simp add: linear_diff[OF lf] linear_cmul[OF lf])
    2.57    then have th: "-k *\<^sub>R f a \<in> span (f ` b)"
    2.58 -    using "2.prems"(5) by simp
    2.59 +    using insert.prems(4) by simp
    2.60    have xsb: "x \<in> span b"
    2.61    proof (cases "k = 0")
    2.62      case True
    2.63 @@ -2551,19 +2536,18 @@
    2.64        by blast
    2.65    next
    2.66      case False
    2.67 -    with span_mul[OF th, of "- 1/ k"]
    2.68 -    have th1: "f a \<in> span (f ` b)"
    2.69 -      by auto
    2.70 -    from inj_on_image_set_diff[OF "2.prems"(3), of "insert a b " "{a}", symmetric]
    2.71 -    have tha: "f ` insert a b - f ` {a} = f ` (insert a b - {a})" by blast
    2.72 -    from "2.prems"(2) [unfolded dependent_def bex_simps(8), rule_format, of "f a"]
    2.73 -    have "f a \<notin> span (f ` b)" using tha
    2.74 -      using "2.hyps"(2)
    2.75 -      "2.prems"(3) by auto
    2.76 -    with th1 have False by blast
    2.77 +    from inj_on_image_set_diff[OF insert.prems(2), of "insert a b " "{a}", symmetric]
    2.78 +    have "f ` insert a b - f ` {a} = f ` (insert a b - {a})" by blast
    2.79 +    then have "f a \<notin> span (f ` b)" 
    2.80 +      using dependent_def insert.hyps(2) insert.prems(1) by fastforce
    2.81 +    moreover have "f a \<in> span (f ` b)"
    2.82 +      using False span_mul[OF th, of "- 1/ k"] by auto
    2.83 +    ultimately have False
    2.84 +      by blast
    2.85      then show ?thesis by blast
    2.86    qed
    2.87 -  from "2.hyps"(3)[OF fb ifb fib xsb "2.prems"(5)] show "x = 0" .
    2.88 +  show "x = 0" 
    2.89 +    using ifb fib xsb insert.IH insert.prems(4) by blast
    2.90  qed
    2.91  
    2.92  text \<open>Can construct an isomorphism between spaces of same dimension.\<close>
    2.93 @@ -2644,9 +2628,8 @@
    2.94    let ?P = "{x. \<forall>y\<in> span C. f x y = g x y}"
    2.95    from bf bg have sp: "subspace ?P"
    2.96      unfolding bilinear_def linear_iff subspace_def bf bg
    2.97 -    by (auto simp add: span_0 bilinear_lzero[OF bf] bilinear_lzero[OF bg] span_add Ball_def
    2.98 +    by (auto simp add: bilinear_lzero[OF bf] bilinear_lzero[OF bg] span_add 
    2.99        intro: bilinear_ladd[OF bf])
   2.100 -
   2.101    have sfg: "\<And>x. x \<in> B \<Longrightarrow> subspace {a. f x a = g x a}"
   2.102      apply (auto simp add: subspace_def)
   2.103      using bf bg unfolding bilinear_def linear_iff
   2.104 @@ -2655,10 +2638,7 @@
   2.105      done
   2.106    have "\<forall>y\<in> span C. f x y = g x y" if "x \<in> span B" for x
   2.107      apply (rule span_induct [OF that sp])
   2.108 -    apply (rule ballI)
   2.109 -    apply (erule span_induct)
   2.110 -    apply (simp_all add: sfg fg)
   2.111 -    done
   2.112 +    using fg sfg span_induct by blast
   2.113    then show ?thesis
   2.114      using SB TC assms by auto
   2.115  qed
   2.116 @@ -2707,11 +2687,8 @@
   2.117    (is "?lhs \<longleftrightarrow> ?rhs")
   2.118  proof
   2.119    assume h: "?lhs"
   2.120 -  {
   2.121 -    fix x y
   2.122 -    assume x: "x \<in> S"
   2.123 -    assume y: "y \<in> S"
   2.124 -    assume f: "f x = f y"
   2.125 +  { fix x y
   2.126 +    assume x: "x \<in> S" and y: "y \<in> S" and f: "f x = f y"
   2.127      from x fS have S0: "card S \<noteq> 0"
   2.128        by auto
   2.129      have "x = y"
   2.130 @@ -2719,15 +2696,13 @@
   2.131        assume xy: "\<not> ?thesis"
   2.132        have th: "card S \<le> card (f ` (S - {y}))"
   2.133          unfolding c
   2.134 -        apply (rule card_mono)
   2.135 -        apply (rule finite_imageI)
   2.136 -        using fS apply simp
   2.137 -        using h xy x y f unfolding subset_eq image_iff
   2.138 -        apply auto
   2.139 -        apply (case_tac "xa = f x")
   2.140 -        apply (rule bexI[where x=x])
   2.141 -        apply auto
   2.142 -        done
   2.143 +      proof (rule card_mono)
   2.144 +        show "finite (f ` (S - {y}))"
   2.145 +          by (simp add: fS)
   2.146 +        show "T \<subseteq> f ` (S - {y})"
   2.147 +          using h xy x y f unfolding subset_eq image_iff
   2.148 +          by (metis member_remove remove_def)
   2.149 +      qed
   2.150        also have " \<dots> \<le> card (S - {y})"
   2.151          apply (rule card_image_le)
   2.152          using fS by simp
   2.153 @@ -2740,17 +2715,13 @@
   2.154  next
   2.155    assume h: ?rhs
   2.156    have "f ` S = T"
   2.157 -    apply (rule card_subset_eq[OF fT ST])
   2.158 -    unfolding card_image[OF h]
   2.159 -    apply (rule c)
   2.160 -    done
   2.161 +    by (simp add: ST c card_image card_subset_eq fT h)
   2.162    then show ?lhs by blast
   2.163  qed
   2.164  
   2.165  lemma linear_surjective_imp_injective:
   2.166    fixes f :: "'a::euclidean_space \<Rightarrow> 'a::euclidean_space"
   2.167 -  assumes lf: "linear f"
   2.168 -    and sf: "surj f"
   2.169 +  assumes lf: "linear f" and sf: "surj f"
   2.170    shows "inj f"
   2.171  proof -
   2.172    let ?U = "UNIV :: 'a set"
   2.173 @@ -2759,46 +2730,29 @@
   2.174      by blast
   2.175    {
   2.176      fix x
   2.177 -    assume x: "x \<in> span B"
   2.178 -    assume fx: "f x = 0"
   2.179 +    assume x: "x \<in> span B" and fx: "f x = 0"
   2.180      from B(2) have fB: "finite B"
   2.181        using independent_bound by auto
   2.182 +    have Uspan: "UNIV \<subseteq> span (f ` B)"
   2.183 +      by (simp add: B(3) lf sf spanning_surjective_image)
   2.184      have fBi: "independent (f ` B)"
   2.185 -      apply (rule card_le_dim_spanning[of "f ` B" ?U])
   2.186 -      apply blast
   2.187 -      using sf B(3)
   2.188 -      unfolding span_linear_image[OF lf] surj_def subset_eq image_iff
   2.189 -      apply blast
   2.190 -      using fB apply blast
   2.191 -      unfolding d[symmetric]
   2.192 -      apply (rule card_image_le)
   2.193 -      apply (rule fB)
   2.194 -      done
   2.195 +    proof (rule card_le_dim_spanning)
   2.196 +      show "card (f ` B) \<le> dim ?U"
   2.197 +        using card_image_le d fB by fastforce
   2.198 +    qed (use fB Uspan in auto)
   2.199      have th0: "dim ?U \<le> card (f ` B)"
   2.200 -      apply (rule span_card_ge_dim)
   2.201 -      apply blast
   2.202 -      unfolding span_linear_image[OF lf]
   2.203 -      apply (rule subset_trans[where B = "f ` UNIV"])
   2.204 -      using sf unfolding surj_def
   2.205 -      apply blast
   2.206 -      apply (rule image_mono)
   2.207 -      apply (rule B(3))
   2.208 -      apply (metis finite_imageI fB)
   2.209 -      done
   2.210 +      by (rule span_card_ge_dim) (use Uspan fB in auto)
   2.211      moreover have "card (f ` B) \<le> card B"
   2.212        by (rule card_image_le, rule fB)
   2.213      ultimately have th1: "card B = card (f ` B)"
   2.214        unfolding d by arith
   2.215      have fiB: "inj_on f B"
   2.216 -      unfolding surjective_iff_injective_gen[OF fB finite_imageI[OF fB] th1 subset_refl, symmetric]
   2.217 -      by blast
   2.218 +      by (simp add: eq_card_imp_inj_on fB th1)
   2.219      from linear_indep_image_lemma[OF lf fB fBi fiB x] fx
   2.220      have "x = 0" by blast
   2.221    }
   2.222    then show ?thesis
   2.223 -    unfolding linear_injective_0[OF lf]
   2.224 -    using B(3)
   2.225 -    by blast
   2.226 +    unfolding linear_injective_0[OF lf] using B(3) by blast
   2.227  qed
   2.228  
   2.229  text \<open>Hence either is enough for isomorphism.\<close>
   2.230 @@ -2854,9 +2808,7 @@
   2.231      assume lf: "linear f" "linear f'"
   2.232      assume f: "f \<circ> f' = id"
   2.233      from f have sf: "surj f"
   2.234 -      apply (auto simp add: o_def id_def surj_def)
   2.235 -      apply metis
   2.236 -      done
   2.237 +      by (auto simp add: o_def id_def surj_def) metis
   2.238      from linear_surjective_isomorphism[OF lf(1) sf] lf f
   2.239      have "f' \<circ> f = id"
   2.240        unfolding fun_eq_iff o_def id_def by metis
   2.241 @@ -2874,18 +2826,13 @@
   2.242    shows "linear g"
   2.243  proof -
   2.244    from gf have fi: "inj f"
   2.245 -    apply (auto simp add: inj_on_def o_def id_def fun_eq_iff)
   2.246 -    apply metis
   2.247 -    done
   2.248 +    by (auto simp add: inj_on_def o_def id_def fun_eq_iff) metis
   2.249    from linear_injective_isomorphism[OF lf fi]
   2.250 -  obtain h :: "'a \<Rightarrow> 'a" where h: "linear h" "\<forall>x. h (f x) = x" "\<forall>x. f (h x) = x"
   2.251 +  obtain h :: "'a \<Rightarrow> 'a" where "linear h" and h: "\<forall>x. h (f x) = x" "\<forall>x. f (h x) = x"
   2.252      by blast
   2.253    have "h = g"
   2.254 -    apply (rule ext) using gf h(2,3)
   2.255 -    apply (simp add: o_def id_def fun_eq_iff)
   2.256 -    apply metis
   2.257 -    done
   2.258 -  with h(1) show ?thesis by blast
   2.259 +    by (metis gf h isomorphism_expand left_right_inverse_eq)
   2.260 +  with \<open>linear h\<close> show ?thesis by blast
   2.261  qed
   2.262  
   2.263  lemma inj_linear_imp_inv_linear:
   2.264 @@ -2944,28 +2891,21 @@
   2.265    by (simp add: infnorm_eq_0)
   2.266  
   2.267  lemma infnorm_neg: "infnorm (- x) = infnorm x"
   2.268 -  unfolding infnorm_def
   2.269 -  apply (rule cong[of "Sup" "Sup"])
   2.270 -  apply blast
   2.271 -  apply auto
   2.272 -  done
   2.273 +  unfolding infnorm_def by simp
   2.274  
   2.275  lemma infnorm_sub: "infnorm (x - y) = infnorm (y - x)"
   2.276 -proof -
   2.277 -  have "y - x = - (x - y)" by simp
   2.278 -  then show ?thesis
   2.279 -    by (metis infnorm_neg)
   2.280 -qed
   2.281 -
   2.282 -lemma real_abs_sub_infnorm: "\<bar>infnorm x - infnorm y\<bar> \<le> infnorm (x - y)"
   2.283 +  by (metis infnorm_neg minus_diff_eq)
   2.284 +
   2.285 +lemma absdiff_infnorm: "\<bar>infnorm x - infnorm y\<bar> \<le> infnorm (x - y)"
   2.286  proof -
   2.287 -  have th: "\<And>(nx::real) n ny. nx \<le> n + ny \<Longrightarrow> ny \<le> n + nx \<Longrightarrow> \<bar>nx - ny\<bar> \<le> n"
   2.288 +  have *: "\<And>(nx::real) n ny. nx \<le> n + ny \<Longrightarrow> ny \<le> n + nx \<Longrightarrow> \<bar>nx - ny\<bar> \<le> n"
   2.289      by arith
   2.290 -  from infnorm_triangle[of "x - y" " y"] infnorm_triangle[of "x - y" "-x"]
   2.291 -  have ths: "infnorm x \<le> infnorm (x - y) + infnorm y"
   2.292 -    "infnorm y \<le> infnorm (x - y) + infnorm x"
   2.293 -    by (simp_all add: field_simps infnorm_neg)
   2.294 -  from th[OF ths] show ?thesis .
   2.295 +  show ?thesis
   2.296 +  proof (rule *)
   2.297 +    from infnorm_triangle[of "x - y" " y"] infnorm_triangle[of "x - y" "-x"]
   2.298 +    show "infnorm x \<le> infnorm (x - y) + infnorm y" "infnorm y \<le> infnorm (x - y) + infnorm x"
   2.299 +      by (simp_all add: field_simps infnorm_neg)
   2.300 +  qed
   2.301  qed
   2.302  
   2.303  lemma real_abs_infnorm: "\<bar>infnorm x\<bar> = infnorm x"
   2.304 @@ -2980,8 +2920,7 @@
   2.305    unfolding infnorm_Max
   2.306  proof (safe intro!: Max_eqI)
   2.307    let ?B = "(\<lambda>i. \<bar>x \<bullet> i\<bar>) ` Basis"
   2.308 -  {
   2.309 -    fix b :: 'a
   2.310 +  { fix b :: 'a
   2.311      assume "b \<in> Basis"
   2.312      then show "\<bar>a *\<^sub>R x \<bullet> b\<bar> \<le> \<bar>a\<bar> * Max ?B"
   2.313        by (simp add: abs_mult mult_left_mono)
   2.314 @@ -3007,27 +2946,17 @@
   2.315  lemma norm_le_infnorm:
   2.316    fixes x :: "'a::euclidean_space"
   2.317    shows "norm x \<le> sqrt DIM('a) * infnorm x"
   2.318 -proof -
   2.319 -  let ?d = "DIM('a)"
   2.320 -  have "real ?d \<ge> 0"
   2.321 -    by simp
   2.322 -  then have d2: "(sqrt (real ?d))\<^sup>2 = real ?d"
   2.323 -    by (auto intro: real_sqrt_pow2)
   2.324 -  have th: "sqrt (real ?d) * infnorm x \<ge> 0"
   2.325 +  unfolding norm_eq_sqrt_inner id_def 
   2.326 +proof (rule real_le_lsqrt[OF inner_ge_zero])
   2.327 +  show "sqrt DIM('a) * infnorm x \<ge> 0"
   2.328      by (simp add: zero_le_mult_iff infnorm_pos_le)
   2.329 -  have th1: "x \<bullet> x \<le> (sqrt (real ?d) * infnorm x)\<^sup>2"
   2.330 -    unfolding power_mult_distrib d2
   2.331 -    apply (subst euclidean_inner)
   2.332 -    apply (subst power2_abs[symmetric])
   2.333 -    apply (rule order_trans[OF sum_bounded_above[where K="\<bar>infnorm x\<bar>\<^sup>2"]])
   2.334 -    apply (auto simp add: power2_eq_square[symmetric])
   2.335 -    apply (subst power2_abs[symmetric])
   2.336 -    apply (rule power_mono)
   2.337 -    apply (auto simp: infnorm_Max)
   2.338 -    done
   2.339 -  from real_le_lsqrt[OF inner_ge_zero th th1]
   2.340 -  show ?thesis
   2.341 -    unfolding norm_eq_sqrt_inner id_def .
   2.342 +  have "x \<bullet> x \<le> (\<Sum>b\<in>Basis. x \<bullet> b * (x \<bullet> b))"
   2.343 +    by (metis euclidean_inner order_refl)
   2.344 +  also have "... \<le> DIM('a) * \<bar>infnorm x\<bar>\<^sup>2"
   2.345 +    by (rule sum_bounded_above) (metis Basis_le_infnorm abs_le_square_iff power2_eq_square real_abs_infnorm)
   2.346 +  also have "... \<le> (sqrt DIM('a) * infnorm x)\<^sup>2"
   2.347 +    by (simp add: power_mult_distrib)
   2.348 +  finally show "x \<bullet> x \<le> (sqrt DIM('a) * infnorm x)\<^sup>2" .
   2.349  qed
   2.350  
   2.351  lemma tendsto_infnorm [tendsto_intros]:
   2.352 @@ -3037,46 +2966,30 @@
   2.353    fix r :: real
   2.354    assume "r > 0"
   2.355    then show "\<exists>s>0. \<forall>x. x \<noteq> a \<and> norm (x - a) < s \<longrightarrow> norm (infnorm x - infnorm a) < r"
   2.356 -    by (metis real_norm_def le_less_trans real_abs_sub_infnorm infnorm_le_norm)
   2.357 +    by (metis real_norm_def le_less_trans absdiff_infnorm infnorm_le_norm)
   2.358  qed
   2.359  
   2.360  text \<open>Equality in Cauchy-Schwarz and triangle inequalities.\<close>
   2.361  
   2.362  lemma norm_cauchy_schwarz_eq: "x \<bullet> y = norm x * norm y \<longleftrightarrow> norm x *\<^sub>R y = norm y *\<^sub>R x"
   2.363    (is "?lhs \<longleftrightarrow> ?rhs")
   2.364 -proof -
   2.365 -  {
   2.366 -    assume h: "x = 0"
   2.367 -    then have ?thesis by simp
   2.368 -  }
   2.369 -  moreover
   2.370 -  {
   2.371 -    assume h: "y = 0"
   2.372 -    then have ?thesis by simp
   2.373 -  }
   2.374 -  moreover
   2.375 -  {
   2.376 -    assume x: "x \<noteq> 0" and y: "y \<noteq> 0"
   2.377 -    from inner_eq_zero_iff[of "norm y *\<^sub>R x - norm x *\<^sub>R y"]
   2.378 -    have "?rhs \<longleftrightarrow>
   2.379 +proof (cases "x=0")
   2.380 +  case True
   2.381 +  then show ?thesis 
   2.382 +    by auto
   2.383 +next
   2.384 +  case False
   2.385 +  from inner_eq_zero_iff[of "norm y *\<^sub>R x - norm x *\<^sub>R y"]
   2.386 +  have "?rhs \<longleftrightarrow>
   2.387        (norm y * (norm y * norm x * norm x - norm x * (x \<bullet> y)) -
   2.388          norm x * (norm y * (y \<bullet> x) - norm x * norm y * norm y) =  0)"
   2.389 -      using x y
   2.390 -      unfolding inner_simps
   2.391 -      unfolding power2_norm_eq_inner[symmetric] power2_eq_square right_minus_eq
   2.392 -      apply (simp add: inner_commute)
   2.393 -      apply (simp add: field_simps)
   2.394 -      apply metis
   2.395 -      done
   2.396 -    also have "\<dots> \<longleftrightarrow> (2 * norm x * norm y * (norm x * norm y - x \<bullet> y) = 0)" using x y
   2.397 -      by (simp add: field_simps inner_commute)
   2.398 -    also have "\<dots> \<longleftrightarrow> ?lhs" using x y
   2.399 -      apply simp
   2.400 -      apply metis
   2.401 -      done
   2.402 -    finally have ?thesis by blast
   2.403 -  }
   2.404 -  ultimately show ?thesis by blast
   2.405 +    using False unfolding inner_simps
   2.406 +    by (auto simp add: power2_norm_eq_inner[symmetric] power2_eq_square inner_commute field_simps)
   2.407 +  also have "\<dots> \<longleftrightarrow> (2 * norm x * norm y * (norm x * norm y - x \<bullet> y) = 0)" 
   2.408 +    using False  by (simp add: field_simps inner_commute)
   2.409 +  also have "\<dots> \<longleftrightarrow> ?lhs" 
   2.410 +    using False by auto
   2.411 +  finally show ?thesis by metis
   2.412  qed
   2.413  
   2.414  lemma norm_cauchy_schwarz_abs_eq:
   2.415 @@ -3088,7 +3001,7 @@
   2.416      by arith
   2.417    have "?rhs \<longleftrightarrow> norm x *\<^sub>R y = norm y *\<^sub>R x \<or> norm (- x) *\<^sub>R y = norm y *\<^sub>R (- x)"
   2.418      by simp
   2.419 -  also have "\<dots> \<longleftrightarrow>(x \<bullet> y = norm x * norm y \<or> (- x) \<bullet> y = norm x * norm y)"
   2.420 +  also have "\<dots> \<longleftrightarrow> (x \<bullet> y = norm x * norm y \<or> (- x) \<bullet> y = norm x * norm y)"
   2.421      unfolding norm_cauchy_schwarz_eq[symmetric]
   2.422      unfolding norm_minus_cancel norm_scaleR ..
   2.423    also have "\<dots> \<longleftrightarrow> ?lhs"
   2.424 @@ -3100,33 +3013,21 @@
   2.425  lemma norm_triangle_eq:
   2.426    fixes x y :: "'a::real_inner"
   2.427    shows "norm (x + y) = norm x + norm y \<longleftrightarrow> norm x *\<^sub>R y = norm y *\<^sub>R x"
   2.428 -proof -
   2.429 -  {
   2.430 -    assume x: "x = 0 \<or> y = 0"
   2.431 -    then have ?thesis
   2.432 -      by (cases "x = 0") simp_all
   2.433 -  }
   2.434 -  moreover
   2.435 -  {
   2.436 -    assume x: "x \<noteq> 0" and y: "y \<noteq> 0"
   2.437 -    then have "norm x \<noteq> 0" "norm y \<noteq> 0"
   2.438 -      by simp_all
   2.439 -    then have n: "norm x > 0" "norm y > 0"
   2.440 -      using norm_ge_zero[of x] norm_ge_zero[of y] by arith+
   2.441 -    have th: "\<And>(a::real) b c. a + b + c \<noteq> 0 \<Longrightarrow> a = b + c \<longleftrightarrow> a\<^sup>2 = (b + c)\<^sup>2"
   2.442 -      by algebra
   2.443 -    have "norm (x + y) = norm x + norm y \<longleftrightarrow> (norm (x + y))\<^sup>2 = (norm x + norm y)\<^sup>2"
   2.444 -      apply (rule th)
   2.445 -      using n norm_ge_zero[of "x + y"]
   2.446 -      apply arith
   2.447 -      done
   2.448 -    also have "\<dots> \<longleftrightarrow> norm x *\<^sub>R y = norm y *\<^sub>R x"
   2.449 -      unfolding norm_cauchy_schwarz_eq[symmetric]
   2.450 -      unfolding power2_norm_eq_inner inner_simps
   2.451 -      by (simp add: power2_norm_eq_inner[symmetric] power2_eq_square inner_commute field_simps)
   2.452 -    finally have ?thesis .
   2.453 -  }
   2.454 -  ultimately show ?thesis by blast
   2.455 +proof (cases "x = 0 \<or> y = 0")
   2.456 +  case True
   2.457 +  then show ?thesis 
   2.458 +    by force
   2.459 +next
   2.460 +  case False
   2.461 +  then have n: "norm x > 0" "norm y > 0"
   2.462 +    by auto
   2.463 +  have "norm (x + y) = norm x + norm y \<longleftrightarrow> (norm (x + y))\<^sup>2 = (norm x + norm y)\<^sup>2"
   2.464 +    by simp
   2.465 +  also have "\<dots> \<longleftrightarrow> norm x *\<^sub>R y = norm y *\<^sub>R x"
   2.466 +    unfolding norm_cauchy_schwarz_eq[symmetric]
   2.467 +    unfolding power2_norm_eq_inner inner_simps
   2.468 +    by (simp add: power2_norm_eq_inner[symmetric] power2_eq_square inner_commute field_simps)
   2.469 +  finally show ?thesis .
   2.470  qed
   2.471  
   2.472  
   2.473 @@ -3185,81 +3086,67 @@
   2.474  lemma collinear_2 [iff]: "collinear {x, y}"
   2.475    apply (simp add: collinear_def)
   2.476    apply (rule exI[where x="x - y"])
   2.477 -  apply auto
   2.478 -  apply (rule exI[where x=1], simp)
   2.479 -  apply (rule exI[where x="- 1"], simp)
   2.480 -  done
   2.481 +  by (metis minus_diff_eq scaleR_left.minus scaleR_one)
   2.482  
   2.483  lemma collinear_lemma: "collinear {0, x, y} \<longleftrightarrow> x = 0 \<or> y = 0 \<or> (\<exists>c. y = c *\<^sub>R x)"
   2.484    (is "?lhs \<longleftrightarrow> ?rhs")
   2.485 -proof -
   2.486 -  {
   2.487 -    assume "x = 0 \<or> y = 0"
   2.488 -    then have ?thesis
   2.489 -      by (cases "x = 0") (simp_all add: collinear_2 insert_commute)
   2.490 -  }
   2.491 -  moreover
   2.492 -  {
   2.493 -    assume x: "x \<noteq> 0" and y: "y \<noteq> 0"
   2.494 -    have ?thesis
   2.495 -    proof
   2.496 -      assume h: "?lhs"
   2.497 -      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"
   2.498 -        unfolding collinear_def by blast
   2.499 -      from u[rule_format, of x 0] u[rule_format, of y 0]
   2.500 -      obtain cx and cy where
   2.501 -        cx: "x = cx *\<^sub>R u" and cy: "y = cy *\<^sub>R u"
   2.502 -        by auto
   2.503 -      from cx x have cx0: "cx \<noteq> 0" by auto
   2.504 -      from cy y have cy0: "cy \<noteq> 0" by auto
   2.505 -      let ?d = "cy / cx"
   2.506 -      from cx cy cx0 have "y = ?d *\<^sub>R x"
   2.507 -        by simp
   2.508 -      then show ?rhs using x y by blast
   2.509 -    next
   2.510 -      assume h: "?rhs"
   2.511 -      then obtain c where c: "y = c *\<^sub>R x"
   2.512 -        using x y by blast
   2.513 -      show ?lhs
   2.514 -        unfolding collinear_def c
   2.515 -        apply (rule exI[where x=x])
   2.516 -        apply auto
   2.517 -        apply (rule exI[where x="- 1"], simp)
   2.518 -        apply (rule exI[where x= "-c"], simp)
   2.519 +proof (cases "x = 0 \<or> y = 0")
   2.520 +  case True
   2.521 +  then show ?thesis
   2.522 +    by (auto simp: insert_commute)
   2.523 +next
   2.524 +  case False
   2.525 +  show ?thesis 
   2.526 +  proof
   2.527 +    assume h: "?lhs"
   2.528 +    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"
   2.529 +      unfolding collinear_def by blast
   2.530 +    from u[rule_format, of x 0] u[rule_format, of y 0]
   2.531 +    obtain cx and cy where
   2.532 +      cx: "x = cx *\<^sub>R u" and cy: "y = cy *\<^sub>R u"
   2.533 +      by auto
   2.534 +    from cx cy False have cx0: "cx \<noteq> 0" and cy0: "cy \<noteq> 0" by auto
   2.535 +    let ?d = "cy / cx"
   2.536 +    from cx cy cx0 have "y = ?d *\<^sub>R x"
   2.537 +      by simp
   2.538 +    then show ?rhs using False by blast
   2.539 +  next
   2.540 +    assume h: "?rhs"
   2.541 +    then obtain c where c: "y = c *\<^sub>R x"
   2.542 +      using False by blast
   2.543 +    show ?lhs
   2.544 +      unfolding collinear_def c
   2.545 +      apply (rule exI[where x=x])
   2.546 +      apply auto
   2.547 +          apply (rule exI[where x="- 1"], simp)
   2.548 +         apply (rule exI[where x= "-c"], simp)
   2.549          apply (rule exI[where x=1], simp)
   2.550 -        apply (rule exI[where x="1 - c"], simp add: scaleR_left_diff_distrib)
   2.551 -        apply (rule exI[where x="c - 1"], simp add: scaleR_left_diff_distrib)
   2.552 -        done
   2.553 -    qed
   2.554 -  }
   2.555 -  ultimately show ?thesis by blast
   2.556 +       apply (rule exI[where x="1 - c"], simp add: scaleR_left_diff_distrib)
   2.557 +      apply (rule exI[where x="c - 1"], simp add: scaleR_left_diff_distrib)
   2.558 +      done
   2.559 +  qed
   2.560  qed
   2.561  
   2.562  lemma norm_cauchy_schwarz_equal: "\<bar>x \<bullet> y\<bar> = norm x * norm y \<longleftrightarrow> collinear {0, x, y}"
   2.563 -  unfolding norm_cauchy_schwarz_abs_eq
   2.564 -  apply (cases "x=0", simp_all)
   2.565 -  apply (cases "y=0", simp_all add: insert_commute)
   2.566 -  unfolding collinear_lemma
   2.567 -  apply simp
   2.568 -  apply (subgoal_tac "norm x \<noteq> 0")
   2.569 -  apply (subgoal_tac "norm y \<noteq> 0")
   2.570 -  apply (rule iffI)
   2.571 -  apply (cases "norm x *\<^sub>R y = norm y *\<^sub>R x")
   2.572 -  apply (rule exI[where x="(1/norm x) * norm y"])
   2.573 -  apply (drule sym)
   2.574 -  unfolding scaleR_scaleR[symmetric]
   2.575 -  apply (simp add: field_simps)
   2.576 -  apply (rule exI[where x="(1/norm x) * - norm y"])
   2.577 -  apply clarify
   2.578 -  apply (drule sym)
   2.579 -  unfolding scaleR_scaleR[symmetric]
   2.580 -  apply (simp add: field_simps)
   2.581 -  apply (erule exE)
   2.582 -  apply (erule ssubst)
   2.583 -  unfolding scaleR_scaleR
   2.584 -  unfolding norm_scaleR
   2.585 -  apply (subgoal_tac "norm x * c = \<bar>c\<bar> * norm x \<or> norm x * c = - \<bar>c\<bar> * norm x")
   2.586 -  apply (auto simp add: field_simps)
   2.587 -  done
   2.588 +proof (cases "x=0")
   2.589 +  case True
   2.590 +  then show ?thesis
   2.591 +    by (auto simp: insert_commute)
   2.592 +next
   2.593 +  case False
   2.594 +  then have nnz: "norm x \<noteq> 0"
   2.595 +    by auto
   2.596 +  show ?thesis
   2.597 +  proof
   2.598 +    assume "\<bar>x \<bullet> y\<bar> = norm x * norm y"
   2.599 +    then show "collinear {0, x, y}"
   2.600 +      unfolding norm_cauchy_schwarz_abs_eq collinear_lemma 
   2.601 +      by (meson eq_vector_fraction_iff nnz)
   2.602 +  next
   2.603 +    assume "collinear {0, x, y}"
   2.604 +    with False show "\<bar>x \<bullet> y\<bar> = norm x * norm y"
   2.605 +      unfolding norm_cauchy_schwarz_abs_eq collinear_lemma  by (auto simp: abs_if)
   2.606 +  qed
   2.607 +qed
   2.608  
   2.609  end