--- a/src/HOL/Analysis/Linear_Algebra.thy Tue May 01 20:40:27 2018 +0200
+++ b/src/HOL/Analysis/Linear_Algebra.thy Wed May 02 09:57:37 2018 +0100
@@ -27,13 +27,6 @@
show "f (s *\<^sub>R v) = s *\<^sub>R (f v)" by (rule f.scaleR)
qed
-lemma bounded_linearI:
- assumes "\<And>x y. f (x + y) = f x + f y"
- and "\<And>r x. f (r *\<^sub>R x) = r *\<^sub>R f x"
- and "\<And>x. norm (f x) \<le> norm x * K"
- shows "bounded_linear f"
- using assms by (rule bounded_linear_intro) (* FIXME: duplicate *)
-
subsection \<open>A generic notion of "hull" (convex, affine, conic hull and closure).\<close>
definition%important hull :: "('a set \<Rightarrow> bool) \<Rightarrow> 'a set \<Rightarrow> 'a set" (infixl "hull" 75)
@@ -2514,35 +2507,27 @@
and fx: "f x = 0"
shows "x = 0"
using fB ifB fi xsB fx
-proof (induct arbitrary: x rule: finite_induct[OF fB])
- case 1
+proof (induction B arbitrary: x rule: finite_induct)
+ case empty
then show ?case by auto
next
- case (2 a b x)
- have fb: "finite b" using "2.prems" by simp
+ case (insert a b x)
have th0: "f ` b \<subseteq> f ` (insert a b)"
- apply (rule image_mono)
- apply blast
- done
- from independent_mono[ OF "2.prems"(2) th0]
- have ifb: "independent (f ` b)" .
+ by (simp add: subset_insertI)
+ have ifb: "independent (f ` b)"
+ using independent_mono insert.prems(1) th0 by blast
have fib: "inj_on f b"
- apply (rule subset_inj_on [OF "2.prems"(3)])
- apply blast
- done
- from span_breakdown[of a "insert a b", simplified, OF "2.prems"(4)]
+ using insert.prems(2) by blast
+ from span_breakdown[of a "insert a b", simplified, OF insert.prems(3)]
obtain k where k: "x - k*\<^sub>R a \<in> span (b - {a})"
by blast
have "f (x - k*\<^sub>R a) \<in> span (f ` b)"
unfolding span_linear_image[OF lf]
- apply (rule imageI)
- using k span_mono[of "b - {a}" b]
- apply blast
- done
+ using "insert.hyps"(2) k by auto
then have "f x - k*\<^sub>R f a \<in> span (f ` b)"
by (simp add: linear_diff[OF lf] linear_cmul[OF lf])
then have th: "-k *\<^sub>R f a \<in> span (f ` b)"
- using "2.prems"(5) by simp
+ using insert.prems(4) by simp
have xsb: "x \<in> span b"
proof (cases "k = 0")
case True
@@ -2551,19 +2536,18 @@
by blast
next
case False
- with span_mul[OF th, of "- 1/ k"]
- have th1: "f a \<in> span (f ` b)"
- by auto
- from inj_on_image_set_diff[OF "2.prems"(3), of "insert a b " "{a}", symmetric]
- have tha: "f ` insert a b - f ` {a} = f ` (insert a b - {a})" by blast
- from "2.prems"(2) [unfolded dependent_def bex_simps(8), rule_format, of "f a"]
- have "f a \<notin> span (f ` b)" using tha
- using "2.hyps"(2)
- "2.prems"(3) by auto
- with th1 have False by blast
+ from inj_on_image_set_diff[OF insert.prems(2), of "insert a b " "{a}", symmetric]
+ have "f ` insert a b - f ` {a} = f ` (insert a b - {a})" by blast
+ then have "f a \<notin> span (f ` b)"
+ using dependent_def insert.hyps(2) insert.prems(1) by fastforce
+ moreover have "f a \<in> span (f ` b)"
+ using False span_mul[OF th, of "- 1/ k"] by auto
+ ultimately have False
+ by blast
then show ?thesis by blast
qed
- from "2.hyps"(3)[OF fb ifb fib xsb "2.prems"(5)] show "x = 0" .
+ show "x = 0"
+ using ifb fib xsb insert.IH insert.prems(4) by blast
qed
text \<open>Can construct an isomorphism between spaces of same dimension.\<close>
@@ -2644,9 +2628,8 @@
let ?P = "{x. \<forall>y\<in> span C. f x y = g x y}"
from bf bg have sp: "subspace ?P"
unfolding bilinear_def linear_iff subspace_def bf bg
- by (auto simp add: span_0 bilinear_lzero[OF bf] bilinear_lzero[OF bg] span_add Ball_def
+ by (auto simp add: bilinear_lzero[OF bf] bilinear_lzero[OF bg] span_add
intro: bilinear_ladd[OF bf])
-
have sfg: "\<And>x. x \<in> B \<Longrightarrow> subspace {a. f x a = g x a}"
apply (auto simp add: subspace_def)
using bf bg unfolding bilinear_def linear_iff
@@ -2655,10 +2638,7 @@
done
have "\<forall>y\<in> span C. f x y = g x y" if "x \<in> span B" for x
apply (rule span_induct [OF that sp])
- apply (rule ballI)
- apply (erule span_induct)
- apply (simp_all add: sfg fg)
- done
+ using fg sfg span_induct by blast
then show ?thesis
using SB TC assms by auto
qed
@@ -2707,11 +2687,8 @@
(is "?lhs \<longleftrightarrow> ?rhs")
proof
assume h: "?lhs"
- {
- fix x y
- assume x: "x \<in> S"
- assume y: "y \<in> S"
- assume f: "f x = f y"
+ { fix x y
+ assume x: "x \<in> S" and y: "y \<in> S" and f: "f x = f y"
from x fS have S0: "card S \<noteq> 0"
by auto
have "x = y"
@@ -2719,15 +2696,13 @@
assume xy: "\<not> ?thesis"
have th: "card S \<le> card (f ` (S - {y}))"
unfolding c
- apply (rule card_mono)
- apply (rule finite_imageI)
- using fS apply simp
- using h xy x y f unfolding subset_eq image_iff
- apply auto
- apply (case_tac "xa = f x")
- apply (rule bexI[where x=x])
- apply auto
- done
+ proof (rule card_mono)
+ show "finite (f ` (S - {y}))"
+ by (simp add: fS)
+ show "T \<subseteq> f ` (S - {y})"
+ using h xy x y f unfolding subset_eq image_iff
+ by (metis member_remove remove_def)
+ qed
also have " \<dots> \<le> card (S - {y})"
apply (rule card_image_le)
using fS by simp
@@ -2740,17 +2715,13 @@
next
assume h: ?rhs
have "f ` S = T"
- apply (rule card_subset_eq[OF fT ST])
- unfolding card_image[OF h]
- apply (rule c)
- done
+ by (simp add: ST c card_image card_subset_eq fT h)
then show ?lhs by blast
qed
lemma linear_surjective_imp_injective:
fixes f :: "'a::euclidean_space \<Rightarrow> 'a::euclidean_space"
- assumes lf: "linear f"
- and sf: "surj f"
+ assumes lf: "linear f" and sf: "surj f"
shows "inj f"
proof -
let ?U = "UNIV :: 'a set"
@@ -2759,46 +2730,29 @@
by blast
{
fix x
- assume x: "x \<in> span B"
- assume fx: "f x = 0"
+ assume x: "x \<in> span B" and fx: "f x = 0"
from B(2) have fB: "finite B"
using independent_bound by auto
+ have Uspan: "UNIV \<subseteq> span (f ` B)"
+ by (simp add: B(3) lf sf spanning_surjective_image)
have fBi: "independent (f ` B)"
- apply (rule card_le_dim_spanning[of "f ` B" ?U])
- apply blast
- using sf B(3)
- unfolding span_linear_image[OF lf] surj_def subset_eq image_iff
- apply blast
- using fB apply blast
- unfolding d[symmetric]
- apply (rule card_image_le)
- apply (rule fB)
- done
+ proof (rule card_le_dim_spanning)
+ show "card (f ` B) \<le> dim ?U"
+ using card_image_le d fB by fastforce
+ qed (use fB Uspan in auto)
have th0: "dim ?U \<le> card (f ` B)"
- apply (rule span_card_ge_dim)
- apply blast
- unfolding span_linear_image[OF lf]
- apply (rule subset_trans[where B = "f ` UNIV"])
- using sf unfolding surj_def
- apply blast
- apply (rule image_mono)
- apply (rule B(3))
- apply (metis finite_imageI fB)
- done
+ by (rule span_card_ge_dim) (use Uspan fB in auto)
moreover have "card (f ` B) \<le> card B"
by (rule card_image_le, rule fB)
ultimately have th1: "card B = card (f ` B)"
unfolding d by arith
have fiB: "inj_on f B"
- unfolding surjective_iff_injective_gen[OF fB finite_imageI[OF fB] th1 subset_refl, symmetric]
- by blast
+ by (simp add: eq_card_imp_inj_on fB th1)
from linear_indep_image_lemma[OF lf fB fBi fiB x] fx
have "x = 0" by blast
}
then show ?thesis
- unfolding linear_injective_0[OF lf]
- using B(3)
- by blast
+ unfolding linear_injective_0[OF lf] using B(3) by blast
qed
text \<open>Hence either is enough for isomorphism.\<close>
@@ -2854,9 +2808,7 @@
assume lf: "linear f" "linear f'"
assume f: "f \<circ> f' = id"
from f have sf: "surj f"
- apply (auto simp add: o_def id_def surj_def)
- apply metis
- done
+ by (auto simp add: o_def id_def surj_def) metis
from linear_surjective_isomorphism[OF lf(1) sf] lf f
have "f' \<circ> f = id"
unfolding fun_eq_iff o_def id_def by metis
@@ -2874,18 +2826,13 @@
shows "linear g"
proof -
from gf have fi: "inj f"
- apply (auto simp add: inj_on_def o_def id_def fun_eq_iff)
- apply metis
- done
+ by (auto simp add: inj_on_def o_def id_def fun_eq_iff) metis
from linear_injective_isomorphism[OF lf fi]
- obtain h :: "'a \<Rightarrow> 'a" where h: "linear h" "\<forall>x. h (f x) = x" "\<forall>x. f (h x) = x"
+ obtain h :: "'a \<Rightarrow> 'a" where "linear h" and h: "\<forall>x. h (f x) = x" "\<forall>x. f (h x) = x"
by blast
have "h = g"
- apply (rule ext) using gf h(2,3)
- apply (simp add: o_def id_def fun_eq_iff)
- apply metis
- done
- with h(1) show ?thesis by blast
+ by (metis gf h isomorphism_expand left_right_inverse_eq)
+ with \<open>linear h\<close> show ?thesis by blast
qed
lemma inj_linear_imp_inv_linear:
@@ -2944,28 +2891,21 @@
by (simp add: infnorm_eq_0)
lemma infnorm_neg: "infnorm (- x) = infnorm x"
- unfolding infnorm_def
- apply (rule cong[of "Sup" "Sup"])
- apply blast
- apply auto
- done
+ unfolding infnorm_def by simp
lemma infnorm_sub: "infnorm (x - y) = infnorm (y - x)"
-proof -
- have "y - x = - (x - y)" by simp
- then show ?thesis
- by (metis infnorm_neg)
-qed
-
-lemma real_abs_sub_infnorm: "\<bar>infnorm x - infnorm y\<bar> \<le> infnorm (x - y)"
+ by (metis infnorm_neg minus_diff_eq)
+
+lemma absdiff_infnorm: "\<bar>infnorm x - infnorm y\<bar> \<le> infnorm (x - y)"
proof -
- have th: "\<And>(nx::real) n ny. nx \<le> n + ny \<Longrightarrow> ny \<le> n + nx \<Longrightarrow> \<bar>nx - ny\<bar> \<le> n"
+ have *: "\<And>(nx::real) n ny. nx \<le> n + ny \<Longrightarrow> ny \<le> n + nx \<Longrightarrow> \<bar>nx - ny\<bar> \<le> n"
by arith
- from infnorm_triangle[of "x - y" " y"] infnorm_triangle[of "x - y" "-x"]
- have ths: "infnorm x \<le> infnorm (x - y) + infnorm y"
- "infnorm y \<le> infnorm (x - y) + infnorm x"
- by (simp_all add: field_simps infnorm_neg)
- from th[OF ths] show ?thesis .
+ show ?thesis
+ proof (rule *)
+ from infnorm_triangle[of "x - y" " y"] infnorm_triangle[of "x - y" "-x"]
+ show "infnorm x \<le> infnorm (x - y) + infnorm y" "infnorm y \<le> infnorm (x - y) + infnorm x"
+ by (simp_all add: field_simps infnorm_neg)
+ qed
qed
lemma real_abs_infnorm: "\<bar>infnorm x\<bar> = infnorm x"
@@ -2980,8 +2920,7 @@
unfolding infnorm_Max
proof (safe intro!: Max_eqI)
let ?B = "(\<lambda>i. \<bar>x \<bullet> i\<bar>) ` Basis"
- {
- fix b :: 'a
+ { fix b :: 'a
assume "b \<in> Basis"
then show "\<bar>a *\<^sub>R x \<bullet> b\<bar> \<le> \<bar>a\<bar> * Max ?B"
by (simp add: abs_mult mult_left_mono)
@@ -3007,27 +2946,17 @@
lemma norm_le_infnorm:
fixes x :: "'a::euclidean_space"
shows "norm x \<le> sqrt DIM('a) * infnorm x"
-proof -
- let ?d = "DIM('a)"
- have "real ?d \<ge> 0"
- by simp
- then have d2: "(sqrt (real ?d))\<^sup>2 = real ?d"
- by (auto intro: real_sqrt_pow2)
- have th: "sqrt (real ?d) * infnorm x \<ge> 0"
+ unfolding norm_eq_sqrt_inner id_def
+proof (rule real_le_lsqrt[OF inner_ge_zero])
+ show "sqrt DIM('a) * infnorm x \<ge> 0"
by (simp add: zero_le_mult_iff infnorm_pos_le)
- have th1: "x \<bullet> x \<le> (sqrt (real ?d) * infnorm x)\<^sup>2"
- unfolding power_mult_distrib d2
- apply (subst euclidean_inner)
- apply (subst power2_abs[symmetric])
- apply (rule order_trans[OF sum_bounded_above[where K="\<bar>infnorm x\<bar>\<^sup>2"]])
- apply (auto simp add: power2_eq_square[symmetric])
- apply (subst power2_abs[symmetric])
- apply (rule power_mono)
- apply (auto simp: infnorm_Max)
- done
- from real_le_lsqrt[OF inner_ge_zero th th1]
- show ?thesis
- unfolding norm_eq_sqrt_inner id_def .
+ have "x \<bullet> x \<le> (\<Sum>b\<in>Basis. x \<bullet> b * (x \<bullet> b))"
+ by (metis euclidean_inner order_refl)
+ also have "... \<le> DIM('a) * \<bar>infnorm x\<bar>\<^sup>2"
+ by (rule sum_bounded_above) (metis Basis_le_infnorm abs_le_square_iff power2_eq_square real_abs_infnorm)
+ also have "... \<le> (sqrt DIM('a) * infnorm x)\<^sup>2"
+ by (simp add: power_mult_distrib)
+ finally show "x \<bullet> x \<le> (sqrt DIM('a) * infnorm x)\<^sup>2" .
qed
lemma tendsto_infnorm [tendsto_intros]:
@@ -3037,46 +2966,30 @@
fix r :: real
assume "r > 0"
then show "\<exists>s>0. \<forall>x. x \<noteq> a \<and> norm (x - a) < s \<longrightarrow> norm (infnorm x - infnorm a) < r"
- by (metis real_norm_def le_less_trans real_abs_sub_infnorm infnorm_le_norm)
+ by (metis real_norm_def le_less_trans absdiff_infnorm infnorm_le_norm)
qed
text \<open>Equality in Cauchy-Schwarz and triangle inequalities.\<close>
lemma norm_cauchy_schwarz_eq: "x \<bullet> y = norm x * norm y \<longleftrightarrow> norm x *\<^sub>R y = norm y *\<^sub>R x"
(is "?lhs \<longleftrightarrow> ?rhs")
-proof -
- {
- assume h: "x = 0"
- then have ?thesis by simp
- }
- moreover
- {
- assume h: "y = 0"
- then have ?thesis by simp
- }
- moreover
- {
- assume x: "x \<noteq> 0" and y: "y \<noteq> 0"
- from inner_eq_zero_iff[of "norm y *\<^sub>R x - norm x *\<^sub>R y"]
- have "?rhs \<longleftrightarrow>
+proof (cases "x=0")
+ case True
+ then show ?thesis
+ by auto
+next
+ case False
+ from inner_eq_zero_iff[of "norm y *\<^sub>R x - norm x *\<^sub>R y"]
+ have "?rhs \<longleftrightarrow>
(norm y * (norm y * norm x * norm x - norm x * (x \<bullet> y)) -
norm x * (norm y * (y \<bullet> x) - norm x * norm y * norm y) = 0)"
- using x y
- unfolding inner_simps
- unfolding power2_norm_eq_inner[symmetric] power2_eq_square right_minus_eq
- apply (simp add: inner_commute)
- apply (simp add: field_simps)
- apply metis
- done
- also have "\<dots> \<longleftrightarrow> (2 * norm x * norm y * (norm x * norm y - x \<bullet> y) = 0)" using x y
- by (simp add: field_simps inner_commute)
- also have "\<dots> \<longleftrightarrow> ?lhs" using x y
- apply simp
- apply metis
- done
- finally have ?thesis by blast
- }
- ultimately show ?thesis by blast
+ using False unfolding inner_simps
+ by (auto simp add: power2_norm_eq_inner[symmetric] power2_eq_square inner_commute field_simps)
+ also have "\<dots> \<longleftrightarrow> (2 * norm x * norm y * (norm x * norm y - x \<bullet> y) = 0)"
+ using False by (simp add: field_simps inner_commute)
+ also have "\<dots> \<longleftrightarrow> ?lhs"
+ using False by auto
+ finally show ?thesis by metis
qed
lemma norm_cauchy_schwarz_abs_eq:
@@ -3088,7 +3001,7 @@
by arith
have "?rhs \<longleftrightarrow> norm x *\<^sub>R y = norm y *\<^sub>R x \<or> norm (- x) *\<^sub>R y = norm y *\<^sub>R (- x)"
by simp
- also have "\<dots> \<longleftrightarrow>(x \<bullet> y = norm x * norm y \<or> (- x) \<bullet> y = norm x * norm y)"
+ also have "\<dots> \<longleftrightarrow> (x \<bullet> y = norm x * norm y \<or> (- x) \<bullet> y = norm x * norm y)"
unfolding norm_cauchy_schwarz_eq[symmetric]
unfolding norm_minus_cancel norm_scaleR ..
also have "\<dots> \<longleftrightarrow> ?lhs"
@@ -3100,33 +3013,21 @@
lemma norm_triangle_eq:
fixes x y :: "'a::real_inner"
shows "norm (x + y) = norm x + norm y \<longleftrightarrow> norm x *\<^sub>R y = norm y *\<^sub>R x"
-proof -
- {
- assume x: "x = 0 \<or> y = 0"
- then have ?thesis
- by (cases "x = 0") simp_all
- }
- moreover
- {
- assume x: "x \<noteq> 0" and y: "y \<noteq> 0"
- then have "norm x \<noteq> 0" "norm y \<noteq> 0"
- by simp_all
- then have n: "norm x > 0" "norm y > 0"
- using norm_ge_zero[of x] norm_ge_zero[of y] by arith+
- have th: "\<And>(a::real) b c. a + b + c \<noteq> 0 \<Longrightarrow> a = b + c \<longleftrightarrow> a\<^sup>2 = (b + c)\<^sup>2"
- by algebra
- have "norm (x + y) = norm x + norm y \<longleftrightarrow> (norm (x + y))\<^sup>2 = (norm x + norm y)\<^sup>2"
- apply (rule th)
- using n norm_ge_zero[of "x + y"]
- apply arith
- done
- also have "\<dots> \<longleftrightarrow> norm x *\<^sub>R y = norm y *\<^sub>R x"
- unfolding norm_cauchy_schwarz_eq[symmetric]
- unfolding power2_norm_eq_inner inner_simps
- by (simp add: power2_norm_eq_inner[symmetric] power2_eq_square inner_commute field_simps)
- finally have ?thesis .
- }
- ultimately show ?thesis by blast
+proof (cases "x = 0 \<or> y = 0")
+ case True
+ then show ?thesis
+ by force
+next
+ case False
+ then have n: "norm x > 0" "norm y > 0"
+ by auto
+ have "norm (x + y) = norm x + norm y \<longleftrightarrow> (norm (x + y))\<^sup>2 = (norm x + norm y)\<^sup>2"
+ by simp
+ also have "\<dots> \<longleftrightarrow> norm x *\<^sub>R y = norm y *\<^sub>R x"
+ unfolding norm_cauchy_schwarz_eq[symmetric]
+ unfolding power2_norm_eq_inner inner_simps
+ by (simp add: power2_norm_eq_inner[symmetric] power2_eq_square inner_commute field_simps)
+ finally show ?thesis .
qed
@@ -3185,81 +3086,67 @@
lemma collinear_2 [iff]: "collinear {x, y}"
apply (simp add: collinear_def)
apply (rule exI[where x="x - y"])
- apply auto
- apply (rule exI[where x=1], simp)
- apply (rule exI[where x="- 1"], simp)
- done
+ by (metis minus_diff_eq scaleR_left.minus scaleR_one)
lemma collinear_lemma: "collinear {0, x, y} \<longleftrightarrow> x = 0 \<or> y = 0 \<or> (\<exists>c. y = c *\<^sub>R x)"
(is "?lhs \<longleftrightarrow> ?rhs")
-proof -
- {
- assume "x = 0 \<or> y = 0"
- then have ?thesis
- by (cases "x = 0") (simp_all add: collinear_2 insert_commute)
- }
- moreover
- {
- assume x: "x \<noteq> 0" and y: "y \<noteq> 0"
- have ?thesis
- proof
- assume h: "?lhs"
- 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"
- unfolding collinear_def by blast
- from u[rule_format, of x 0] u[rule_format, of y 0]
- obtain cx and cy where
- cx: "x = cx *\<^sub>R u" and cy: "y = cy *\<^sub>R u"
- by auto
- from cx x have cx0: "cx \<noteq> 0" by auto
- from cy y have cy0: "cy \<noteq> 0" by auto
- let ?d = "cy / cx"
- from cx cy cx0 have "y = ?d *\<^sub>R x"
- by simp
- then show ?rhs using x y by blast
- next
- assume h: "?rhs"
- then obtain c where c: "y = c *\<^sub>R x"
- using x y by blast
- show ?lhs
- unfolding collinear_def c
- apply (rule exI[where x=x])
- apply auto
- apply (rule exI[where x="- 1"], simp)
- apply (rule exI[where x= "-c"], simp)
+proof (cases "x = 0 \<or> y = 0")
+ case True
+ then show ?thesis
+ by (auto simp: insert_commute)
+next
+ case False
+ show ?thesis
+ proof
+ assume h: "?lhs"
+ 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"
+ unfolding collinear_def by blast
+ from u[rule_format, of x 0] u[rule_format, of y 0]
+ obtain cx and cy where
+ cx: "x = cx *\<^sub>R u" and cy: "y = cy *\<^sub>R u"
+ by auto
+ from cx cy False have cx0: "cx \<noteq> 0" and cy0: "cy \<noteq> 0" by auto
+ let ?d = "cy / cx"
+ from cx cy cx0 have "y = ?d *\<^sub>R x"
+ by simp
+ then show ?rhs using False by blast
+ next
+ assume h: "?rhs"
+ then obtain c where c: "y = c *\<^sub>R x"
+ using False by blast
+ show ?lhs
+ unfolding collinear_def c
+ apply (rule exI[where x=x])
+ apply auto
+ apply (rule exI[where x="- 1"], simp)
+ apply (rule exI[where x= "-c"], simp)
apply (rule exI[where x=1], simp)
- apply (rule exI[where x="1 - c"], simp add: scaleR_left_diff_distrib)
- apply (rule exI[where x="c - 1"], simp add: scaleR_left_diff_distrib)
- done
- qed
- }
- ultimately show ?thesis by blast
+ apply (rule exI[where x="1 - c"], simp add: scaleR_left_diff_distrib)
+ apply (rule exI[where x="c - 1"], simp add: scaleR_left_diff_distrib)
+ done
+ qed
qed
lemma norm_cauchy_schwarz_equal: "\<bar>x \<bullet> y\<bar> = norm x * norm y \<longleftrightarrow> collinear {0, x, y}"
- unfolding norm_cauchy_schwarz_abs_eq
- apply (cases "x=0", simp_all)
- apply (cases "y=0", simp_all add: insert_commute)
- unfolding collinear_lemma
- apply simp
- apply (subgoal_tac "norm x \<noteq> 0")
- apply (subgoal_tac "norm y \<noteq> 0")
- apply (rule iffI)
- apply (cases "norm x *\<^sub>R y = norm y *\<^sub>R x")
- apply (rule exI[where x="(1/norm x) * norm y"])
- apply (drule sym)
- unfolding scaleR_scaleR[symmetric]
- apply (simp add: field_simps)
- apply (rule exI[where x="(1/norm x) * - norm y"])
- apply clarify
- apply (drule sym)
- unfolding scaleR_scaleR[symmetric]
- apply (simp add: field_simps)
- apply (erule exE)
- apply (erule ssubst)
- unfolding scaleR_scaleR
- unfolding norm_scaleR
- apply (subgoal_tac "norm x * c = \<bar>c\<bar> * norm x \<or> norm x * c = - \<bar>c\<bar> * norm x")
- apply (auto simp add: field_simps)
- done
+proof (cases "x=0")
+ case True
+ then show ?thesis
+ by (auto simp: insert_commute)
+next
+ case False
+ then have nnz: "norm x \<noteq> 0"
+ by auto
+ show ?thesis
+ proof
+ assume "\<bar>x \<bullet> y\<bar> = norm x * norm y"
+ then show "collinear {0, x, y}"
+ unfolding norm_cauchy_schwarz_abs_eq collinear_lemma
+ by (meson eq_vector_fraction_iff nnz)
+ next
+ assume "collinear {0, x, y}"
+ with False show "\<bar>x \<bullet> y\<bar> = norm x * norm y"
+ unfolding norm_cauchy_schwarz_abs_eq collinear_lemma by (auto simp: abs_if)
+ qed
+qed
end