1.1 --- a/src/HOL/Library/Determinants.thy Sat Feb 21 10:58:25 2009 -0800
1.2 +++ b/src/HOL/Library/Determinants.thy Sat Feb 21 11:18:50 2009 -0800
1.3 @@ -1048,7 +1048,7 @@
1.4 note th0 = this
1.5 let ?g = "\<lambda>x. if x = 0 then 0 else norm x *s f (inverse (norm x) *s x)"
1.6 {fix x:: "real ^'n" assume nx: "norm x = 1"
1.7 - have "?g x = f x" using nx by (simp add: norm_eq_0[symmetric])}
1.8 + have "?g x = f x" using nx by auto}
1.9 hence thfg: "\<forall>x. norm x = 1 \<longrightarrow> ?g x = f x" by blast
1.10 have g0: "?g 0 = 0" by simp
1.11 {fix x y :: "real ^'n"
1.12 @@ -1057,15 +1057,15 @@
1.13 moreover
1.14 {assume "x = 0" "y \<noteq> 0"
1.15 then have "dist (?g x) (?g y) = dist x y"
1.16 - apply (simp add: dist_def norm_neg norm_mul norm_eq_0)
1.17 + apply (simp add: dist_def norm_mul)
1.18 apply (rule f1[rule_format])
1.19 - by(simp add: norm_mul norm_eq_0 field_simps)}
1.20 + by(simp add: norm_mul field_simps)}
1.21 moreover
1.22 {assume "x \<noteq> 0" "y = 0"
1.23 then have "dist (?g x) (?g y) = dist x y"
1.24 - apply (simp add: dist_def norm_neg norm_mul norm_eq_0)
1.25 + apply (simp add: dist_def norm_mul)
1.26 apply (rule f1[rule_format])
1.27 - by(simp add: norm_mul norm_eq_0 field_simps)}
1.28 + by(simp add: norm_mul field_simps)}
1.29 moreover
1.30 {assume z: "x \<noteq> 0" "y \<noteq> 0"
1.31 have th00: "x = norm x *s inverse (norm x) *s x" "y = norm y *s inverse (norm y) *s y" "norm x *s f (inverse (norm x) *s x) = norm x *s f (inverse (norm x) *s x)"
1.32 @@ -1077,7 +1077,7 @@
1.33 "norm (f (inverse (norm x) *s x) - f (inverse (norm y) *s y)) =
1.34 norm (inverse (norm x) *s x - inverse (norm y) *s y)"
1.35 using z
1.36 - by (auto simp add: norm_eq_0 vector_smult_assoc field_simps norm_mul intro: f1[rule_format] fd1[rule_format, unfolded dist_def])
1.37 + by (auto simp add: vector_smult_assoc field_simps norm_mul intro: f1[rule_format] fd1[rule_format, unfolded dist_def])
1.38 from z th0[OF th00] have "dist (?g x) (?g y) = dist x y"
1.39 by (simp add: dist_def)}
1.40 ultimately have "dist (?g x) (?g y) = dist x y" by blast}
1.41 @@ -1148,4 +1148,4 @@
1.42 by (simp add: ring_simps)
1.43 qed
1.44
1.45 -end
1.46 \ No newline at end of file
1.47 +end
2.1 --- a/src/HOL/Library/Euclidean_Space.thy Sat Feb 21 10:58:25 2009 -0800
2.2 +++ b/src/HOL/Library/Euclidean_Space.thy Sat Feb 21 11:18:50 2009 -0800
2.3 @@ -729,28 +729,16 @@
2.4 lemma norm_0: "norm (0::real ^ 'n) = 0"
2.5 by (rule norm_zero)
2.6
2.7 -lemma norm_pos_le: "0 <= norm (x::real^'n)"
2.8 - by (rule norm_ge_zero)
2.9 -lemma norm_neg: " norm(-x) = norm (x:: real ^ 'n)"
2.10 - by (rule norm_minus_cancel)
2.11 -lemma norm_sub: "norm(x - y) = norm(y - (x::real ^ 'n))"
2.12 - by (rule norm_minus_commute)
2.13 lemma norm_mul: "norm(a *s x) = abs(a) * norm x"
2.14 by (simp add: vector_norm_def vector_component setL2_right_distrib
2.15 abs_mult cong: strong_setL2_cong)
2.16 lemma norm_eq_0_dot: "(norm x = 0) \<longleftrightarrow> (x \<bullet> x = (0::real))"
2.17 by (simp add: vector_norm_def dot_def setL2_def power2_eq_square)
2.18 -lemma norm_eq_0: "norm x = 0 \<longleftrightarrow> x = (0::real ^ 'n)"
2.19 - by (rule norm_eq_zero)
2.20 -lemma norm_pos_lt: "0 < norm x \<longleftrightarrow> x \<noteq> (0::real ^ 'n)"
2.21 - by (rule zero_less_norm_iff)
2.22 lemma real_vector_norm_def: "norm x = sqrt (x \<bullet> x)"
2.23 by (simp add: vector_norm_def setL2_def dot_def power2_eq_square)
2.24 lemma norm_pow_2: "norm x ^ 2 = x \<bullet> x"
2.25 by (simp add: real_vector_norm_def)
2.26 -lemma norm_eq_0_imp: "norm x = 0 ==> x = (0::real ^'n)" by (metis norm_eq_0)
2.27 -lemma norm_le_0: "norm x <= 0 \<longleftrightarrow> x = (0::real ^'n)"
2.28 - by (rule norm_le_zero_iff)
2.29 +lemma norm_eq_0_imp: "norm x = 0 ==> x = (0::real ^'n)" by (metis norm_eq_zero)
2.30 lemma vector_mul_eq_0: "(a *s x = 0) \<longleftrightarrow> a = (0::'a::idom) \<or> x = 0"
2.31 by vector
2.32 lemma vector_mul_lcancel: "a *s x = a *s y \<longleftrightarrow> a = (0::real) \<or> x = y"
2.33 @@ -764,14 +752,14 @@
2.34 lemma norm_cauchy_schwarz: "x \<bullet> y <= norm x * norm y"
2.35 proof-
2.36 {assume "norm x = 0"
2.37 - hence ?thesis by (simp add: norm_eq_0 dot_lzero dot_rzero norm_0)}
2.38 + hence ?thesis by (simp add: dot_lzero dot_rzero)}
2.39 moreover
2.40 {assume "norm y = 0"
2.41 - hence ?thesis by (simp add: norm_eq_0 dot_lzero dot_rzero norm_0)}
2.42 + hence ?thesis by (simp add: dot_lzero dot_rzero)}
2.43 moreover
2.44 {assume h: "norm x \<noteq> 0" "norm y \<noteq> 0"
2.45 let ?z = "norm y *s x - norm x *s y"
2.46 - from h have p: "norm x * norm y > 0" by (metis norm_pos_le le_less zero_compare_simps)
2.47 + from h have p: "norm x * norm y > 0" by (metis norm_ge_zero le_less zero_compare_simps)
2.48 from dot_pos_le[of ?z]
2.49 have "(norm x * norm y) * (x \<bullet> y) \<le> norm x ^2 * norm y ^2"
2.50 apply (simp add: dot_rsub dot_lsub dot_lmult dot_rmult ring_simps)
2.51 @@ -782,21 +770,16 @@
2.52 ultimately show ?thesis by metis
2.53 qed
2.54
2.55 -lemma norm_abs: "abs (norm x) = norm (x::real ^'n)"
2.56 - by (rule abs_norm_cancel) (* already declared [simp] *)
2.57 -
2.58 lemma norm_cauchy_schwarz_abs: "\<bar>x \<bullet> y\<bar> \<le> norm x * norm y"
2.59 using norm_cauchy_schwarz[of x y] norm_cauchy_schwarz[of x "-y"]
2.60 - by (simp add: real_abs_def dot_rneg norm_neg)
2.61 -lemma norm_triangle: "norm(x + y) <= norm x + norm (y::real ^'n)"
2.62 - by (rule norm_triangle_ineq)
2.63 + by (simp add: real_abs_def dot_rneg)
2.64
2.65 lemma norm_triangle_sub: "norm (x::real ^'n) <= norm(y) + norm(x - y)"
2.66 - using norm_triangle[of "y" "x - y"] by (simp add: ring_simps)
2.67 + using norm_triangle_ineq[of "y" "x - y"] by (simp add: ring_simps)
2.68 lemma norm_triangle_le: "norm(x::real ^'n) + norm y <= e ==> norm(x + y) <= e"
2.69 - by (metis order_trans norm_triangle)
2.70 + by (metis order_trans norm_triangle_ineq)
2.71 lemma norm_triangle_lt: "norm(x::real ^'n) + norm(y) < e ==> norm(x + y) < e"
2.72 - by (metis basic_trans_rules(21) norm_triangle)
2.73 + by (metis basic_trans_rules(21) norm_triangle_ineq)
2.74
2.75 lemma setsum_delta:
2.76 assumes fS: "finite S"
2.77 @@ -866,13 +849,13 @@
2.78
2.79 lemma norm_le_square: "norm(x) <= a \<longleftrightarrow> 0 <= a \<and> x \<bullet> x <= a^2"
2.80 apply (simp add: dot_square_norm real_abs_le_square_iff[symmetric])
2.81 - using norm_pos_le[of x]
2.82 + using norm_ge_zero[of x]
2.83 apply arith
2.84 done
2.85
2.86 lemma norm_ge_square: "norm(x) >= a \<longleftrightarrow> a <= 0 \<or> x \<bullet> x >= a ^ 2"
2.87 apply (simp add: dot_square_norm real_abs_le_square_iff[symmetric])
2.88 - using norm_pos_le[of x]
2.89 + using norm_ge_zero[of x]
2.90 apply arith
2.91 done
2.92
2.93 @@ -943,14 +926,14 @@
2.94 lemma pth_d: "x + (0::real ^'n) == x" by (atomize (full)) vector
2.95
2.96 lemma norm_imp_pos_and_ge: "norm (x::real ^ 'n) == n \<Longrightarrow> norm x \<ge> 0 \<and> n \<ge> norm x"
2.97 - by (atomize) (auto simp add: norm_pos_le)
2.98 + by (atomize) (auto simp add: norm_ge_zero)
2.99
2.100 lemma real_eq_0_iff_le_ge_0: "(x::real) = 0 == x \<ge> 0 \<and> -x \<ge> 0" by arith
2.101
2.102 lemma norm_pths:
2.103 "(x::real ^'n) = y \<longleftrightarrow> norm (x - y) \<le> 0"
2.104 "x \<noteq> y \<longleftrightarrow> \<not> (norm (x - y) \<le> 0)"
2.105 - using norm_pos_le[of "x - y"] by (auto simp add: norm_0 norm_eq_0)
2.106 + using norm_ge_zero[of "x - y"] by auto
2.107
2.108 use "normarith.ML"
2.109
2.110 @@ -1070,7 +1053,7 @@
2.111 assumes fS: "finite S"
2.112 shows "norm (setsum f S) <= setsum (\<lambda>x. norm(f x)) S"
2.113 proof(induct rule: finite_induct[OF fS])
2.114 - case 1 thus ?case by (simp add: norm_zero)
2.115 + case 1 thus ?case by simp
2.116 next
2.117 case (2 x S)
2.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)
2.119 @@ -1369,7 +1352,7 @@
2.120 by (auto simp add: setsum_component intro: abs_le_D1)
2.121 have Pne: "setsum (\<lambda>x. \<bar>f x $ i\<bar>) ?Pn \<le> e"
2.122 using i component_le_norm[OF i, of "setsum (\<lambda>x. - f x) ?Pn"] fPs[OF PnP]
2.123 - by (auto simp add: setsum_negf norm_neg setsum_component vector_component intro: abs_le_D1)
2.124 + by (auto simp add: setsum_negf setsum_component vector_component intro: abs_le_D1)
2.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"
2.126 apply (subst thp)
2.127 apply (rule setsum_Un_nonzero)
2.128 @@ -1693,7 +1676,7 @@
2.129 unfolding norm_mul
2.130 apply (simp only: mult_commute)
2.131 apply (rule mult_mono)
2.132 - by (auto simp add: ring_simps norm_pos_le) }
2.133 + by (auto simp add: ring_simps norm_ge_zero) }
2.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
2.135 from real_setsum_norm_le[OF fS, of "\<lambda>i. (x$i) *s (f (basis i))", OF th]
2.136 have "norm (f x) \<le> ?B * norm x" unfolding th0 setsum_left_distrib by metis}
2.137 @@ -1710,15 +1693,15 @@
2.138 let ?K = "\<bar>B\<bar> + 1"
2.139 have Kp: "?K > 0" by arith
2.140 {assume C: "B < 0"
2.141 - have "norm (1::real ^ 'n) > 0" by (simp add: norm_pos_lt)
2.142 + have "norm (1::real ^ 'n) > 0" by (simp add: zero_less_norm_iff)
2.143 with C have "B * norm (1:: real ^ 'n) < 0"
2.144 by (simp add: zero_compare_simps)
2.145 - with B[rule_format, of 1] norm_pos_le[of "f 1"] have False by simp
2.146 + with B[rule_format, of 1] norm_ge_zero[of "f 1"] have False by simp
2.147 }
2.148 then have Bp: "B \<ge> 0" by ferrack
2.149 {fix x::"real ^ 'n"
2.150 have "norm (f x) \<le> ?K * norm x"
2.151 - using B[rule_format, of x] norm_pos_le[of x] norm_pos_le[of "f x"] Bp
2.152 + using B[rule_format, of x] norm_ge_zero[of x] norm_ge_zero[of "f x"] Bp
2.153 apply (auto simp add: ring_simps split add: abs_split)
2.154 apply (erule order_trans, simp)
2.155 done
2.156 @@ -1801,9 +1784,9 @@
2.157 apply simp
2.158 apply (auto simp add: bilinear_rmul[OF bh] bilinear_lmul[OF bh] norm_mul ring_simps)
2.159 apply (rule mult_mono)
2.160 - apply (auto simp add: norm_pos_le zero_le_mult_iff component_le_norm)
2.161 + apply (auto simp add: norm_ge_zero zero_le_mult_iff component_le_norm)
2.162 apply (rule mult_mono)
2.163 - apply (auto simp add: norm_pos_le zero_le_mult_iff component_le_norm)
2.164 + apply (auto simp add: norm_ge_zero zero_le_mult_iff component_le_norm)
2.165 done}
2.166 then show ?thesis by metis
2.167 qed
2.168 @@ -1823,7 +1806,7 @@
2.169 have "B * norm x * norm y \<le> ?K * norm x * norm y"
2.170 apply -
2.171 apply (rule mult_right_mono, rule mult_right_mono)
2.172 - by (auto simp add: norm_pos_le)
2.173 + by (auto simp add: norm_ge_zero)
2.174 then have "norm (h x y) \<le> ?K * norm x * norm y"
2.175 using B[rule_format, of x y] by simp}
2.176 with Kp show ?thesis by blast
2.177 @@ -2436,21 +2419,21 @@
2.178 moreover
2.179 {assume H: ?lhs
2.180 from H[rule_format, of "basis 1"]
2.181 - have bp: "b \<ge> 0" using norm_pos_le[of "f (basis 1)"] dimindex_ge_1[of "UNIV:: 'n set"]
2.182 + have bp: "b \<ge> 0" using norm_ge_zero[of "f (basis 1)"] dimindex_ge_1[of "UNIV:: 'n set"]
2.183 by (auto simp add: norm_basis elim: order_trans [OF norm_ge_zero])
2.184 {fix x :: "real ^'n"
2.185 {assume "x = 0"
2.186 - then have "norm (f x) \<le> b * norm x" by (simp add: linear_0[OF lf] norm_0 bp)}
2.187 + then have "norm (f x) \<le> b * norm x" by (simp add: linear_0[OF lf] bp)}
2.188 moreover
2.189 {assume x0: "x \<noteq> 0"
2.190 - hence n0: "norm x \<noteq> 0" by (metis norm_eq_0)
2.191 + hence n0: "norm x \<noteq> 0" by (metis norm_eq_zero)
2.192 let ?c = "1/ norm x"
2.193 have "norm (?c*s x) = 1" using x0 by (simp add: n0 norm_mul)
2.194 with H have "norm (f(?c*s x)) \<le> b" by blast
2.195 hence "?c * norm (f x) \<le> b"
2.196 by (simp add: linear_cmul[OF lf] norm_mul)
2.197 hence "norm (f x) \<le> b * norm x"
2.198 - using n0 norm_pos_le[of x] by (auto simp add: field_simps)}
2.199 + using n0 norm_ge_zero[of x] by (auto simp add: field_simps)}
2.200 ultimately have "norm (f x) \<le> b * norm x" by blast}
2.201 then have ?rhs by blast}
2.202 ultimately show ?thesis by blast
2.203 @@ -2482,12 +2465,12 @@
2.204 qed
2.205
2.206 lemma onorm_pos_le: assumes lf: "linear (f::real ^'n \<Rightarrow> real ^'m)" shows "0 <= onorm f"
2.207 - using order_trans[OF norm_pos_le onorm(1)[OF lf, of "basis 1"], unfolded norm_basis_1] by simp
2.208 + using order_trans[OF norm_ge_zero onorm(1)[OF lf, of "basis 1"], unfolded norm_basis_1] by simp
2.209
2.210 lemma onorm_eq_0: assumes lf: "linear (f::real ^'n \<Rightarrow> real ^'m)"
2.211 shows "onorm f = 0 \<longleftrightarrow> (\<forall>x. f x = 0)"
2.212 using onorm[OF lf]
2.213 - apply (auto simp add: norm_0 onorm_pos_le norm_le_0)
2.214 + apply (auto simp add: onorm_pos_le)
2.215 apply atomize
2.216 apply (erule allE[where x="0::real"])
2.217 using onorm_pos_le[OF lf]
2.218 @@ -2525,7 +2508,7 @@
2.219 lemma onorm_neg_lemma: assumes lf: "linear (f::real ^'n \<Rightarrow> real^'m)"
2.220 shows "onorm (\<lambda>x. - f x) \<le> onorm f"
2.221 using onorm[OF linear_compose_neg[OF lf]] onorm[OF lf]
2.222 - unfolding norm_neg by metis
2.223 + unfolding norm_minus_cancel by metis
2.224
2.225 lemma onorm_neg: assumes lf: "linear (f::real ^'n \<Rightarrow> real^'m)"
2.226 shows "onorm (\<lambda>x. - f x) = onorm f"
2.227 @@ -2537,7 +2520,7 @@
2.228 shows "onorm (\<lambda>x. f x + g x) <= onorm f + onorm g"
2.229 apply(rule onorm(2)[OF linear_compose_add[OF lf lg], rule_format])
2.230 apply (rule order_trans)
2.231 - apply (rule norm_triangle)
2.232 + apply (rule norm_triangle_ineq)
2.233 apply (simp add: distrib)
2.234 apply (rule add_mono)
2.235 apply (rule onorm(1)[OF lf])
2.236 @@ -5175,10 +5158,10 @@
2.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")
2.238 proof-
2.239 {assume h: "x = 0"
2.240 - hence ?thesis by (simp add: norm_0)}
2.241 + hence ?thesis by simp}
2.242 moreover
2.243 {assume h: "y = 0"
2.244 - hence ?thesis by (simp add: norm_0)}
2.245 + hence ?thesis by simp}
2.246 moreover
2.247 {assume x: "x \<noteq> 0" and y: "y \<noteq> 0"
2.248 from dot_eq_0[of "norm y *s x - norm x *s y"]
2.249 @@ -5192,7 +5175,7 @@
2.250 also have "\<dots> \<longleftrightarrow> (2 * norm x * norm y * (norm x * norm y - x \<bullet> y) = 0)" using x y
2.251 by (simp add: ring_simps dot_sym)
2.252 also have "\<dots> \<longleftrightarrow> ?lhs" using x y
2.253 - apply (simp add: norm_eq_0)
2.254 + apply simp
2.255 by metis
2.256 finally have ?thesis by blast}
2.257 ultimately show ?thesis by blast
2.258 @@ -5203,14 +5186,14 @@
2.259 proof-
2.260 have th: "\<And>(x::real) a. a \<ge> 0 \<Longrightarrow> abs x = a \<longleftrightarrow> x = a \<or> x = - a" by arith
2.261 have "?rhs \<longleftrightarrow> norm x *s y = norm y *s x \<or> norm (- x) *s y = norm y *s (- x)"
2.262 - apply (simp add: norm_neg) by vector
2.263 + apply simp by vector
2.264 also have "\<dots> \<longleftrightarrow>(x \<bullet> y = norm x * norm y \<or>
2.265 (-x) \<bullet> y = norm x * norm y)"
2.266 unfolding norm_cauchy_schwarz_eq[symmetric]
2.267 - unfolding norm_neg
2.268 + unfolding norm_minus_cancel
2.269 norm_mul by blast
2.270 also have "\<dots> \<longleftrightarrow> ?lhs"
2.271 - unfolding th[OF mult_nonneg_nonneg, OF norm_pos_le[of x] norm_pos_le[of y]] dot_lneg
2.272 + unfolding th[OF mult_nonneg_nonneg, OF norm_ge_zero[of x] norm_ge_zero[of y]] dot_lneg
2.273 by arith
2.274 finally show ?thesis ..
2.275 qed
2.276 @@ -5218,17 +5201,17 @@
2.277 lemma norm_triangle_eq: "norm(x + y) = norm x + norm y \<longleftrightarrow> norm x *s y = norm y *s x"
2.278 proof-
2.279 {assume x: "x =0 \<or> y =0"
2.280 - hence ?thesis by (cases "x=0", simp_all add: norm_0)}
2.281 + hence ?thesis by (cases "x=0", simp_all)}
2.282 moreover
2.283 {assume x: "x \<noteq> 0" and y: "y \<noteq> 0"
2.284 hence "norm x \<noteq> 0" "norm y \<noteq> 0"
2.285 - by (simp_all add: norm_eq_0)
2.286 + by simp_all
2.287 hence n: "norm x > 0" "norm y > 0"
2.288 - using norm_pos_le[of x] norm_pos_le[of y]
2.289 + using norm_ge_zero[of x] norm_ge_zero[of y]
2.290 by arith+
2.291 have th: "\<And>(a::real) b c. a + b + c \<noteq> 0 ==> (a = b + c \<longleftrightarrow> a^2 = (b + c)^2)" by algebra
2.292 have "norm(x + y) = norm x + norm y \<longleftrightarrow> norm(x + y)^ 2 = (norm x + norm y) ^2"
2.293 - apply (rule th) using n norm_pos_le[of "x + y"]
2.294 + apply (rule th) using n norm_ge_zero[of "x + y"]
2.295 by arith
2.296 also have "\<dots> \<longleftrightarrow> norm x *s y = norm y *s x"
2.297 unfolding norm_cauchy_schwarz_eq[symmetric]
2.298 @@ -5298,8 +5281,8 @@
2.299
2.300 lemma norm_cauchy_schwarz_equal: "abs(x \<bullet> y) = norm x * norm y \<longleftrightarrow> collinear {(0::real^'n),x,y}"
2.301 unfolding norm_cauchy_schwarz_abs_eq
2.302 -apply (cases "x=0", simp_all add: collinear_2 norm_0)
2.303 -apply (cases "y=0", simp_all add: collinear_2 norm_0 insert_commute)
2.304 +apply (cases "x=0", simp_all add: collinear_2)
2.305 +apply (cases "y=0", simp_all add: collinear_2 insert_commute)
2.306 unfolding collinear_lemma
2.307 apply simp
2.308 apply (subgoal_tac "norm x \<noteq> 0")
2.309 @@ -5324,8 +5307,8 @@
2.310 apply (simp add: ring_simps)
2.311 apply (case_tac "c <= 0", simp add: ring_simps)
2.312 apply (simp add: ring_simps)
2.313 -apply (simp add: norm_eq_0)
2.314 -apply (simp add: norm_eq_0)
2.315 +apply simp
2.316 +apply simp
2.317 done
2.318
2.319 end