src/HOL/Analysis/Linear_Algebra.thy
changeset 66486 ffaaa83543b2
parent 66453 cc19f7ca2ed6
child 66503 7685861f337d
     1.1 --- a/src/HOL/Analysis/Linear_Algebra.thy	Tue Aug 22 14:34:26 2017 +0200
     1.2 +++ b/src/HOL/Analysis/Linear_Algebra.thy	Tue Aug 22 21:36:48 2017 +0200
     1.3 @@ -1397,43 +1397,6 @@
     1.4  lemma norm_eq_1: "norm x = 1 \<longleftrightarrow> x \<bullet> x = 1"
     1.5    by (simp add: norm_eq_sqrt_inner)
     1.6  
     1.7 -text\<open>Squaring equations and inequalities involving norms.\<close>
     1.8 -
     1.9 -lemma dot_square_norm: "x \<bullet> x = (norm x)\<^sup>2"
    1.10 -  by (simp only: power2_norm_eq_inner) (* TODO: move? *)
    1.11 -
    1.12 -lemma norm_eq_square: "norm x = a \<longleftrightarrow> 0 \<le> a \<and> x \<bullet> x = a\<^sup>2"
    1.13 -  by (auto simp add: norm_eq_sqrt_inner)
    1.14 -
    1.15 -lemma norm_le_square: "norm x \<le> a \<longleftrightarrow> 0 \<le> a \<and> x \<bullet> x \<le> a\<^sup>2"
    1.16 -  apply (simp add: dot_square_norm abs_le_square_iff[symmetric])
    1.17 -  using norm_ge_zero[of x]
    1.18 -  apply arith
    1.19 -  done
    1.20 -
    1.21 -lemma norm_ge_square: "norm x \<ge> a \<longleftrightarrow> a \<le> 0 \<or> x \<bullet> x \<ge> a\<^sup>2"
    1.22 -  apply (simp add: dot_square_norm abs_le_square_iff[symmetric])
    1.23 -  using norm_ge_zero[of x]
    1.24 -  apply arith
    1.25 -  done
    1.26 -
    1.27 -lemma norm_lt_square: "norm x < a \<longleftrightarrow> 0 < a \<and> x \<bullet> x < a\<^sup>2"
    1.28 -  by (metis not_le norm_ge_square)
    1.29 -
    1.30 -lemma norm_gt_square: "norm x > a \<longleftrightarrow> a < 0 \<or> x \<bullet> x > a\<^sup>2"
    1.31 -  by (metis norm_le_square not_less)
    1.32 -
    1.33 -text\<open>Dot product in terms of the norm rather than conversely.\<close>
    1.34 -
    1.35 -lemmas inner_simps = inner_add_left inner_add_right inner_diff_right inner_diff_left
    1.36 -  inner_scaleR_left inner_scaleR_right
    1.37 -
    1.38 -lemma dot_norm: "x \<bullet> y = ((norm (x + y))\<^sup>2 - (norm x)\<^sup>2 - (norm y)\<^sup>2) / 2"
    1.39 -  by (simp only: power2_norm_eq_inner inner_simps inner_commute) auto
    1.40 -
    1.41 -lemma dot_norm_neg: "x \<bullet> y = (((norm x)\<^sup>2 + (norm y)\<^sup>2) - (norm (x - y))\<^sup>2) / 2"
    1.42 -  by (simp only: power2_norm_eq_inner inner_simps inner_commute)
    1.43 -    (auto simp add: algebra_simps)
    1.44  
    1.45  text\<open>Equality of vectors in terms of @{term "op \<bullet>"} products.\<close>
    1.46