src/HOL/Library/Euclidean_Space.thy
changeset 30041 9becd197a40e
parent 30040 e2cd1acda1ab
child 30045 b8ddd7667eed
     1.1 --- a/src/HOL/Library/Euclidean_Space.thy	Sat Feb 21 10:58:25 2009 -0800
     1.2 +++ b/src/HOL/Library/Euclidean_Space.thy	Sat Feb 21 11:18:50 2009 -0800
     1.3 @@ -729,28 +729,16 @@
     1.4  lemma norm_0: "norm (0::real ^ 'n) = 0"
     1.5    by (rule norm_zero)
     1.6  
     1.7 -lemma norm_pos_le: "0 <= norm (x::real^'n)"
     1.8 -  by (rule norm_ge_zero)
     1.9 -lemma norm_neg: " norm(-x) = norm (x:: real ^ 'n)" 
    1.10 -  by (rule norm_minus_cancel)
    1.11 -lemma norm_sub: "norm(x - y) = norm(y - (x::real ^ 'n))" 
    1.12 -  by (rule norm_minus_commute)
    1.13  lemma norm_mul: "norm(a *s x) = abs(a) * norm x"
    1.14    by (simp add: vector_norm_def vector_component setL2_right_distrib
    1.15             abs_mult cong: strong_setL2_cong)
    1.16  lemma norm_eq_0_dot: "(norm x = 0) \<longleftrightarrow> (x \<bullet> x = (0::real))"
    1.17    by (simp add: vector_norm_def dot_def setL2_def power2_eq_square)
    1.18 -lemma norm_eq_0: "norm x = 0 \<longleftrightarrow> x = (0::real ^ 'n)"
    1.19 -  by (rule norm_eq_zero)
    1.20 -lemma norm_pos_lt: "0 < norm x \<longleftrightarrow> x \<noteq> (0::real ^ 'n)"
    1.21 -  by (rule zero_less_norm_iff)
    1.22  lemma real_vector_norm_def: "norm x = sqrt (x \<bullet> x)"
    1.23    by (simp add: vector_norm_def setL2_def dot_def power2_eq_square)
    1.24  lemma norm_pow_2: "norm x ^ 2 = x \<bullet> x"
    1.25    by (simp add: real_vector_norm_def)
    1.26 -lemma norm_eq_0_imp: "norm x = 0 ==> x = (0::real ^'n)" by (metis norm_eq_0)
    1.27 -lemma norm_le_0: "norm x <= 0 \<longleftrightarrow> x = (0::real ^'n)"
    1.28 -  by (rule norm_le_zero_iff)
    1.29 +lemma norm_eq_0_imp: "norm x = 0 ==> x = (0::real ^'n)" by (metis norm_eq_zero)
    1.30  lemma vector_mul_eq_0: "(a *s x = 0) \<longleftrightarrow> a = (0::'a::idom) \<or> x = 0"
    1.31    by vector
    1.32  lemma vector_mul_lcancel: "a *s x = a *s y \<longleftrightarrow> a = (0::real) \<or> x = y"
    1.33 @@ -764,14 +752,14 @@
    1.34  lemma norm_cauchy_schwarz: "x \<bullet> y <= norm x * norm y"
    1.35  proof-
    1.36    {assume "norm x = 0"
    1.37 -    hence ?thesis by (simp add: norm_eq_0 dot_lzero dot_rzero norm_0)}
    1.38 +    hence ?thesis by (simp add: dot_lzero dot_rzero)}
    1.39    moreover
    1.40    {assume "norm y = 0" 
    1.41 -    hence ?thesis by (simp add: norm_eq_0 dot_lzero dot_rzero norm_0)}
    1.42 +    hence ?thesis by (simp add: dot_lzero dot_rzero)}
    1.43    moreover
    1.44    {assume h: "norm x \<noteq> 0" "norm y \<noteq> 0"
    1.45      let ?z = "norm y *s x - norm x *s y"
    1.46 -    from h have p: "norm x * norm y > 0" by (metis norm_pos_le le_less zero_compare_simps)
    1.47 +    from h have p: "norm x * norm y > 0" by (metis norm_ge_zero le_less zero_compare_simps)
    1.48      from dot_pos_le[of ?z]
    1.49      have "(norm x * norm y) * (x \<bullet> y) \<le> norm x ^2 * norm y ^2"
    1.50        apply (simp add: dot_rsub dot_lsub dot_lmult dot_rmult ring_simps)
    1.51 @@ -782,21 +770,16 @@
    1.52    ultimately show ?thesis by metis
    1.53  qed
    1.54  
    1.55 -lemma norm_abs: "abs (norm x) = norm (x::real ^'n)"
    1.56 -  by (rule abs_norm_cancel) (* already declared [simp] *)
    1.57 -
    1.58  lemma norm_cauchy_schwarz_abs: "\<bar>x \<bullet> y\<bar> \<le> norm x * norm y"
    1.59    using norm_cauchy_schwarz[of x y] norm_cauchy_schwarz[of x "-y"]
    1.60 -  by (simp add: real_abs_def dot_rneg norm_neg)
    1.61 -lemma norm_triangle: "norm(x + y) <= norm x + norm (y::real ^'n)"
    1.62 -  by (rule norm_triangle_ineq)
    1.63 +  by (simp add: real_abs_def dot_rneg)
    1.64  
    1.65  lemma norm_triangle_sub: "norm (x::real ^'n) <= norm(y) + norm(x - y)"
    1.66 -  using norm_triangle[of "y" "x - y"] by (simp add: ring_simps)
    1.67 +  using norm_triangle_ineq[of "y" "x - y"] by (simp add: ring_simps)
    1.68  lemma norm_triangle_le: "norm(x::real ^'n) + norm y <= e ==> norm(x + y) <= e"
    1.69 -  by (metis order_trans norm_triangle)
    1.70 +  by (metis order_trans norm_triangle_ineq)
    1.71  lemma norm_triangle_lt: "norm(x::real ^'n) + norm(y) < e ==> norm(x + y) < e"
    1.72 -  by (metis basic_trans_rules(21) norm_triangle)
    1.73 +  by (metis basic_trans_rules(21) norm_triangle_ineq)
    1.74  
    1.75  lemma setsum_delta: 
    1.76    assumes fS: "finite S"
    1.77 @@ -866,13 +849,13 @@
    1.78  
    1.79  lemma norm_le_square: "norm(x) <= a \<longleftrightarrow> 0 <= a \<and> x \<bullet> x <= a^2"
    1.80    apply (simp add: dot_square_norm real_abs_le_square_iff[symmetric])
    1.81 -  using norm_pos_le[of x]
    1.82 +  using norm_ge_zero[of x]
    1.83    apply arith
    1.84    done
    1.85  
    1.86  lemma norm_ge_square: "norm(x) >= a \<longleftrightarrow> a <= 0 \<or> x \<bullet> x >= a ^ 2" 
    1.87    apply (simp add: dot_square_norm real_abs_le_square_iff[symmetric])
    1.88 -  using norm_pos_le[of x]
    1.89 +  using norm_ge_zero[of x]
    1.90    apply arith
    1.91    done
    1.92  
    1.93 @@ -943,14 +926,14 @@
    1.94  lemma pth_d: "x + (0::real ^'n) == x" by (atomize (full)) vector
    1.95  
    1.96  lemma norm_imp_pos_and_ge: "norm (x::real ^ 'n) == n \<Longrightarrow> norm x \<ge> 0 \<and> n \<ge> norm x"
    1.97 -  by (atomize) (auto simp add: norm_pos_le)
    1.98 +  by (atomize) (auto simp add: norm_ge_zero)
    1.99  
   1.100  lemma real_eq_0_iff_le_ge_0: "(x::real) = 0 == x \<ge> 0 \<and> -x \<ge> 0" by arith
   1.101  
   1.102  lemma norm_pths: 
   1.103    "(x::real ^'n) = y \<longleftrightarrow> norm (x - y) \<le> 0"
   1.104    "x \<noteq> y \<longleftrightarrow> \<not> (norm (x - y) \<le> 0)"
   1.105 -  using norm_pos_le[of "x - y"] by (auto simp add: norm_0 norm_eq_0)
   1.106 +  using norm_ge_zero[of "x - y"] by auto
   1.107  
   1.108  use "normarith.ML"
   1.109  
   1.110 @@ -1070,7 +1053,7 @@
   1.111    assumes fS: "finite S"
   1.112    shows "norm (setsum f S) <= setsum (\<lambda>x. norm(f x)) S"
   1.113  proof(induct rule: finite_induct[OF fS])
   1.114 -  case 1 thus ?case by (simp add: norm_zero)
   1.115 +  case 1 thus ?case by simp
   1.116  next
   1.117    case (2 x S)
   1.118    from "2.hyps" have "norm (setsum f (insert x S)) \<le> norm (f x) + norm (setsum f S)" by (simp add: norm_triangle_ineq)
   1.119 @@ -1369,7 +1352,7 @@
   1.120        by (auto simp add: setsum_component intro: abs_le_D1)
   1.121      have Pne: "setsum (\<lambda>x. \<bar>f x $ i\<bar>) ?Pn \<le> e"
   1.122        using i component_le_norm[OF i, of "setsum (\<lambda>x. - f x) ?Pn"]  fPs[OF PnP]
   1.123 -      by (auto simp add: setsum_negf norm_neg setsum_component vector_component intro: abs_le_D1)
   1.124 +      by (auto simp add: setsum_negf setsum_component vector_component intro: abs_le_D1)
   1.125      have "setsum (\<lambda>x. \<bar>f x $ i\<bar>) P = setsum (\<lambda>x. \<bar>f x $ i\<bar>) ?Pp + setsum (\<lambda>x. \<bar>f x $ i\<bar>) ?Pn" 
   1.126        apply (subst thp)
   1.127        apply (rule setsum_Un_nonzero) 
   1.128 @@ -1693,7 +1676,7 @@
   1.129        unfolding norm_mul
   1.130        apply (simp only: mult_commute)
   1.131        apply (rule mult_mono)
   1.132 -      by (auto simp add: ring_simps norm_pos_le) }
   1.133 +      by (auto simp add: ring_simps norm_ge_zero) }
   1.134      then have th: "\<forall>i\<in> ?S. norm ((x$i) *s f (basis i :: real ^'m)) \<le> norm (f (basis i)) * norm x" by metis
   1.135      from real_setsum_norm_le[OF fS, of "\<lambda>i. (x$i) *s (f (basis i))", OF th]
   1.136      have "norm (f x) \<le> ?B * norm x" unfolding th0 setsum_left_distrib by metis}
   1.137 @@ -1710,15 +1693,15 @@
   1.138    let ?K = "\<bar>B\<bar> + 1"
   1.139    have Kp: "?K > 0" by arith
   1.140      {assume C: "B < 0"
   1.141 -      have "norm (1::real ^ 'n) > 0" by (simp add: norm_pos_lt)
   1.142 +      have "norm (1::real ^ 'n) > 0" by (simp add: zero_less_norm_iff)
   1.143        with C have "B * norm (1:: real ^ 'n) < 0"
   1.144  	by (simp add: zero_compare_simps)
   1.145 -      with B[rule_format, of 1] norm_pos_le[of "f 1"] have False by simp
   1.146 +      with B[rule_format, of 1] norm_ge_zero[of "f 1"] have False by simp
   1.147      }
   1.148      then have Bp: "B \<ge> 0" by ferrack
   1.149      {fix x::"real ^ 'n"
   1.150        have "norm (f x) \<le> ?K *  norm x"
   1.151 -      using B[rule_format, of x] norm_pos_le[of x] norm_pos_le[of "f x"] Bp
   1.152 +      using B[rule_format, of x] norm_ge_zero[of x] norm_ge_zero[of "f x"] Bp
   1.153        apply (auto simp add: ring_simps split add: abs_split)
   1.154        apply (erule order_trans, simp)
   1.155        done
   1.156 @@ -1801,9 +1784,9 @@
   1.157        apply simp
   1.158        apply (auto simp add: bilinear_rmul[OF bh] bilinear_lmul[OF bh] norm_mul ring_simps)
   1.159        apply (rule mult_mono)
   1.160 -      apply (auto simp add: norm_pos_le zero_le_mult_iff component_le_norm)
   1.161 +      apply (auto simp add: norm_ge_zero zero_le_mult_iff component_le_norm)
   1.162        apply (rule mult_mono)
   1.163 -      apply (auto simp add: norm_pos_le zero_le_mult_iff component_le_norm)
   1.164 +      apply (auto simp add: norm_ge_zero zero_le_mult_iff component_le_norm)
   1.165        done}
   1.166    then show ?thesis by metis
   1.167  qed
   1.168 @@ -1823,7 +1806,7 @@
   1.169      have "B * norm x * norm y \<le> ?K * norm x * norm y"
   1.170        apply - 
   1.171        apply (rule mult_right_mono, rule mult_right_mono)
   1.172 -      by (auto simp add: norm_pos_le)
   1.173 +      by (auto simp add: norm_ge_zero)
   1.174      then have "norm (h x y) \<le> ?K * norm x * norm y"
   1.175        using B[rule_format, of x y] by simp} 
   1.176    with Kp show ?thesis by blast
   1.177 @@ -2436,21 +2419,21 @@
   1.178    moreover
   1.179    {assume H: ?lhs
   1.180      from H[rule_format, of "basis 1"] 
   1.181 -    have bp: "b \<ge> 0" using norm_pos_le[of "f (basis 1)"] dimindex_ge_1[of "UNIV:: 'n set"]
   1.182 +    have bp: "b \<ge> 0" using norm_ge_zero[of "f (basis 1)"] dimindex_ge_1[of "UNIV:: 'n set"]
   1.183        by (auto simp add: norm_basis elim: order_trans [OF norm_ge_zero])
   1.184      {fix x :: "real ^'n"
   1.185        {assume "x = 0"
   1.186 -	then have "norm (f x) \<le> b * norm x" by (simp add: linear_0[OF lf] norm_0 bp)}
   1.187 +	then have "norm (f x) \<le> b * norm x" by (simp add: linear_0[OF lf] bp)}
   1.188        moreover
   1.189        {assume x0: "x \<noteq> 0"
   1.190 -	hence n0: "norm x \<noteq> 0" by (metis norm_eq_0)
   1.191 +	hence n0: "norm x \<noteq> 0" by (metis norm_eq_zero)
   1.192  	let ?c = "1/ norm x"
   1.193  	have "norm (?c*s x) = 1" using x0 by (simp add: n0 norm_mul)
   1.194  	with H have "norm (f(?c*s x)) \<le> b" by blast
   1.195  	hence "?c * norm (f x) \<le> b" 
   1.196  	  by (simp add: linear_cmul[OF lf] norm_mul)
   1.197  	hence "norm (f x) \<le> b * norm x" 
   1.198 -	  using n0 norm_pos_le[of x] by (auto simp add: field_simps)}
   1.199 +	  using n0 norm_ge_zero[of x] by (auto simp add: field_simps)}
   1.200        ultimately have "norm (f x) \<le> b * norm x" by blast}
   1.201      then have ?rhs by blast}
   1.202    ultimately show ?thesis by blast
   1.203 @@ -2482,12 +2465,12 @@
   1.204  qed
   1.205  
   1.206  lemma onorm_pos_le: assumes lf: "linear (f::real ^'n \<Rightarrow> real ^'m)" shows "0 <= onorm f"
   1.207 -  using order_trans[OF norm_pos_le onorm(1)[OF lf, of "basis 1"], unfolded norm_basis_1] by simp
   1.208 +  using order_trans[OF norm_ge_zero onorm(1)[OF lf, of "basis 1"], unfolded norm_basis_1] by simp
   1.209  
   1.210  lemma onorm_eq_0: assumes lf: "linear (f::real ^'n \<Rightarrow> real ^'m)" 
   1.211    shows "onorm f = 0 \<longleftrightarrow> (\<forall>x. f x = 0)"
   1.212    using onorm[OF lf]
   1.213 -  apply (auto simp add: norm_0 onorm_pos_le norm_le_0)
   1.214 +  apply (auto simp add: onorm_pos_le)
   1.215    apply atomize
   1.216    apply (erule allE[where x="0::real"])
   1.217    using onorm_pos_le[OF lf]
   1.218 @@ -2525,7 +2508,7 @@
   1.219  lemma onorm_neg_lemma: assumes lf: "linear (f::real ^'n \<Rightarrow> real^'m)"
   1.220    shows "onorm (\<lambda>x. - f x) \<le> onorm f"
   1.221    using onorm[OF linear_compose_neg[OF lf]] onorm[OF lf]
   1.222 -  unfolding norm_neg by metis
   1.223 +  unfolding norm_minus_cancel by metis
   1.224  
   1.225  lemma onorm_neg: assumes lf: "linear (f::real ^'n \<Rightarrow> real^'m)"
   1.226    shows "onorm (\<lambda>x. - f x) = onorm f"
   1.227 @@ -2537,7 +2520,7 @@
   1.228    shows "onorm (\<lambda>x. f x + g x) <= onorm f + onorm g"
   1.229    apply(rule onorm(2)[OF linear_compose_add[OF lf lg], rule_format])
   1.230    apply (rule order_trans)
   1.231 -  apply (rule norm_triangle)
   1.232 +  apply (rule norm_triangle_ineq)
   1.233    apply (simp add: distrib)
   1.234    apply (rule add_mono)
   1.235    apply (rule onorm(1)[OF lf])
   1.236 @@ -5175,10 +5158,10 @@
   1.237  lemma norm_cauchy_schwarz_eq: "(x::real ^'n) \<bullet> y = norm x * norm y \<longleftrightarrow> norm x *s y = norm y *s x" (is "?lhs \<longleftrightarrow> ?rhs")
   1.238  proof-
   1.239    {assume h: "x = 0"
   1.240 -    hence ?thesis by (simp add: norm_0)}
   1.241 +    hence ?thesis by simp}
   1.242    moreover
   1.243    {assume h: "y = 0"
   1.244 -    hence ?thesis by (simp add: norm_0)}
   1.245 +    hence ?thesis by simp}
   1.246    moreover
   1.247    {assume x: "x \<noteq> 0" and y: "y \<noteq> 0"
   1.248      from dot_eq_0[of "norm y *s x - norm x *s y"]
   1.249 @@ -5192,7 +5175,7 @@
   1.250      also have "\<dots> \<longleftrightarrow> (2 * norm x * norm y * (norm x * norm y - x \<bullet> y) = 0)" using x y
   1.251        by (simp add: ring_simps dot_sym)
   1.252      also have "\<dots> \<longleftrightarrow> ?lhs" using x y
   1.253 -      apply (simp add: norm_eq_0)
   1.254 +      apply simp
   1.255        by metis
   1.256      finally have ?thesis by blast}
   1.257    ultimately show ?thesis by blast
   1.258 @@ -5203,14 +5186,14 @@
   1.259  proof-
   1.260    have th: "\<And>(x::real) a. a \<ge> 0 \<Longrightarrow> abs x = a \<longleftrightarrow> x = a \<or> x = - a" by arith
   1.261    have "?rhs \<longleftrightarrow> norm x *s y = norm y *s x \<or> norm (- x) *s y = norm y *s (- x)"
   1.262 -    apply (simp add: norm_neg) by vector
   1.263 +    apply simp by vector
   1.264    also have "\<dots> \<longleftrightarrow>(x \<bullet> y = norm x * norm y \<or>
   1.265       (-x) \<bullet> y = norm x * norm y)"
   1.266      unfolding norm_cauchy_schwarz_eq[symmetric]
   1.267 -    unfolding norm_neg
   1.268 +    unfolding norm_minus_cancel
   1.269        norm_mul by blast
   1.270    also have "\<dots> \<longleftrightarrow> ?lhs"
   1.271 -    unfolding th[OF mult_nonneg_nonneg, OF norm_pos_le[of x] norm_pos_le[of y]] dot_lneg
   1.272 +    unfolding th[OF mult_nonneg_nonneg, OF norm_ge_zero[of x] norm_ge_zero[of y]] dot_lneg
   1.273      by arith
   1.274    finally show ?thesis ..
   1.275  qed
   1.276 @@ -5218,17 +5201,17 @@
   1.277  lemma norm_triangle_eq: "norm(x + y) = norm x + norm y \<longleftrightarrow> norm x *s y = norm y *s x"
   1.278  proof-
   1.279    {assume x: "x =0 \<or> y =0"
   1.280 -    hence ?thesis by (cases "x=0", simp_all add: norm_0)}
   1.281 +    hence ?thesis by (cases "x=0", simp_all)}
   1.282    moreover
   1.283    {assume x: "x \<noteq> 0" and y: "y \<noteq> 0"
   1.284      hence "norm x \<noteq> 0" "norm y \<noteq> 0"
   1.285 -      by (simp_all add: norm_eq_0)
   1.286 +      by simp_all
   1.287      hence n: "norm x > 0" "norm y > 0" 
   1.288 -      using norm_pos_le[of x] norm_pos_le[of y]
   1.289 +      using norm_ge_zero[of x] norm_ge_zero[of y]
   1.290        by arith+
   1.291      have th: "\<And>(a::real) b c. a + b + c \<noteq> 0 ==> (a = b + c \<longleftrightarrow> a^2 = (b + c)^2)" by algebra
   1.292      have "norm(x + y) = norm x + norm y \<longleftrightarrow> norm(x + y)^ 2 = (norm x + norm y) ^2"
   1.293 -      apply (rule th) using n norm_pos_le[of "x + y"]
   1.294 +      apply (rule th) using n norm_ge_zero[of "x + y"]
   1.295        by arith
   1.296      also have "\<dots> \<longleftrightarrow> norm x *s y = norm y *s x"
   1.297        unfolding norm_cauchy_schwarz_eq[symmetric]
   1.298 @@ -5298,8 +5281,8 @@
   1.299  
   1.300  lemma norm_cauchy_schwarz_equal: "abs(x \<bullet> y) = norm x * norm y \<longleftrightarrow> collinear {(0::real^'n),x,y}"
   1.301  unfolding norm_cauchy_schwarz_abs_eq
   1.302 -apply (cases "x=0", simp_all add: collinear_2 norm_0)
   1.303 -apply (cases "y=0", simp_all add: collinear_2 norm_0 insert_commute)
   1.304 +apply (cases "x=0", simp_all add: collinear_2)
   1.305 +apply (cases "y=0", simp_all add: collinear_2 insert_commute)
   1.306  unfolding collinear_lemma
   1.307  apply simp
   1.308  apply (subgoal_tac "norm x \<noteq> 0")
   1.309 @@ -5324,8 +5307,8 @@
   1.310  apply (simp add: ring_simps)
   1.311  apply (case_tac "c <= 0", simp add: ring_simps)
   1.312  apply (simp add: ring_simps)
   1.313 -apply (simp add: norm_eq_0)
   1.314 -apply (simp add: norm_eq_0)
   1.315 +apply simp
   1.316 +apply simp
   1.317  done
   1.318  
   1.319  end