src/HOL/Library/Euclidean_Space.thy
 changeset 31445 c8a474a919a7 parent 31417 c12b25b7f015 child 31492 5400beeddb55
```     1.1 --- a/src/HOL/Library/Euclidean_Space.thy	Thu Jun 04 15:00:44 2009 +0200
1.2 +++ b/src/HOL/Library/Euclidean_Space.thy	Thu Jun 04 14:32:00 2009 -0700
1.3 @@ -1060,54 +1060,103 @@
1.4
1.5  subsection{* General linear decision procedure for normed spaces. *}
1.6
1.7 -lemma norm_cmul_rule_thm: "b >= norm(x) ==> \<bar>c\<bar> * b >= norm(c *s x)"
1.8 -  apply (clarsimp simp add: norm_mul)
1.9 -  apply (rule mult_mono1)
1.10 -  apply simp_all
1.11 +lemma norm_cmul_rule_thm:
1.12 +  fixes x :: "'a::real_normed_vector"
1.13 +  shows "b >= norm(x) ==> \<bar>c\<bar> * b >= norm(scaleR c x)"
1.14 +  unfolding norm_scaleR
1.15 +  apply (erule mult_mono1)
1.16 +  apply simp
1.17    done
1.18
1.19    (* FIXME: Move all these theorems into the ML code using lemma antiquotation *)
1.20 -lemma norm_add_rule_thm: "b1 >= norm(x1 :: real ^'n::finite) \<Longrightarrow> b2 >= norm(x2) ==> b1 + b2 >= norm(x1 + x2)"
1.21 -  apply (rule norm_triangle_le) by simp
1.23 +  fixes x1 x2 :: "'a::real_normed_vector"
1.24 +  shows "norm x1 \<le> b1 \<Longrightarrow> norm x2 \<le> b2 \<Longrightarrow> norm (x1 + x2) \<le> b1 + b2"
1.25 +  by (rule order_trans [OF norm_triangle_ineq add_mono])
1.26
1.27  lemma ge_iff_diff_ge_0: "(a::'a::ordered_ring) \<ge> b == a - b \<ge> 0"
1.28    by (simp add: ring_simps)
1.29
1.30 -lemma pth_1: "(x::real^'n) == 1 *s x" by (simp only: vector_smult_lid)
1.31 -lemma pth_2: "x - (y::real^'n) == x + -y" by (atomize (full)) simp
1.32 -lemma pth_3: "(-x::real^'n) == -1 *s x" by vector
1.33 -lemma pth_4: "0 *s (x::real^'n) == 0" "c *s 0 = (0::real ^ 'n)" by vector+
1.34 -lemma pth_5: "c *s (d *s x) == (c * d) *s (x::real ^ 'n)" by (atomize (full)) vector
1.35 -lemma pth_6: "(c::real) *s (x + y) == c *s x + c *s y" by (atomize (full)) (vector ring_simps)
1.36 -lemma pth_7: "0 + x == (x::real^'n)" "x + 0 == x" by simp_all
1.37 -lemma pth_8: "(c::real) *s x + d *s x == (c + d) *s x" by (atomize (full)) (vector ring_simps)
1.38 -lemma pth_9: "((c::real) *s x + z) + d *s x == (c + d) *s x + z"
1.39 -  "c *s x + (d *s x + z) == (c + d) *s x + z"
1.40 -  "(c *s x + w) + (d *s x + z) == (c + d) *s x + (w + z)" by ((atomize (full)), vector ring_simps)+
1.41 -lemma pth_a: "(0::real) *s x + y == y" by (atomize (full)) vector
1.42 -lemma pth_b: "(c::real) *s x + d *s y == c *s x + d *s y"
1.43 -  "(c *s x + z) + d *s y == c *s x + (z + d *s y)"
1.44 -  "c *s x + (d *s y + z) == c *s x + (d *s y + z)"
1.45 -  "(c *s x + w) + (d *s y + z) == c *s x + (w + (d *s y + z))"
1.46 -  by ((atomize (full)), vector)+
1.47 -lemma pth_c: "(c::real) *s x + d *s y == d *s y + c *s x"
1.48 -  "(c *s x + z) + d *s y == d *s y + (c *s x + z)"
1.49 -  "c *s x + (d *s y + z) == d *s y + (c *s x + z)"
1.50 -  "(c *s x + w) + (d *s y + z) == d *s y + ((c *s x + w) + z)" by ((atomize (full)), vector)+
1.51 -lemma pth_d: "x + (0::real ^'n) == x" by (atomize (full)) vector
1.52 -
1.53 -lemma norm_imp_pos_and_ge: "norm (x::real ^ _) == n \<Longrightarrow> norm x \<ge> 0 \<and> n \<ge> norm x"
1.54 -  by (atomize) (auto simp add: norm_ge_zero)
1.55 +lemma pth_1:
1.56 +  fixes x :: "'a::real_normed_vector"
1.57 +  shows "x == scaleR 1 x" by simp
1.58 +
1.59 +lemma pth_2:
1.60 +  fixes x :: "'a::real_normed_vector"
1.61 +  shows "x - y == x + -y" by (atomize (full)) simp
1.62 +
1.63 +lemma pth_3:
1.64 +  fixes x :: "'a::real_normed_vector"
1.65 +  shows "- x == scaleR (-1) x" by simp
1.66 +
1.67 +lemma pth_4:
1.68 +  fixes x :: "'a::real_normed_vector"
1.69 +  shows "scaleR 0 x == 0" and "scaleR c 0 = (0::'a)" by simp_all
1.70 +
1.71 +lemma pth_5:
1.72 +  fixes x :: "'a::real_normed_vector"
1.73 +  shows "scaleR c (scaleR d x) == scaleR (c * d) x" by simp
1.74 +
1.75 +lemma pth_6:
1.76 +  fixes x :: "'a::real_normed_vector"
1.77 +  shows "scaleR c (x + y) == scaleR c x + scaleR c y"
1.78 +  by (simp add: scaleR_right_distrib)
1.79 +
1.80 +lemma pth_7:
1.81 +  fixes x :: "'a::real_normed_vector"
1.82 +  shows "0 + x == x" and "x + 0 == x" by simp_all
1.83 +
1.84 +lemma pth_8:
1.85 +  fixes x :: "'a::real_normed_vector"
1.86 +  shows "scaleR c x + scaleR d x == scaleR (c + d) x"
1.87 +  by (simp add: scaleR_left_distrib)
1.88 +
1.89 +lemma pth_9:
1.90 +  fixes x :: "'a::real_normed_vector" shows
1.91 +  "(scaleR c x + z) + scaleR d x == scaleR (c + d) x + z"
1.92 +  "scaleR c x + (scaleR d x + z) == scaleR (c + d) x + z"
1.93 +  "(scaleR c x + w) + (scaleR d x + z) == scaleR (c + d) x + (w + z)"
1.94 +  by (simp_all add: algebra_simps)
1.95 +
1.96 +lemma pth_a:
1.97 +  fixes x :: "'a::real_normed_vector"
1.98 +  shows "scaleR 0 x + y == y" by simp
1.99 +
1.100 +lemma pth_b:
1.101 +  fixes x :: "'a::real_normed_vector" shows
1.102 +  "scaleR c x + scaleR d y == scaleR c x + scaleR d y"
1.103 +  "(scaleR c x + z) + scaleR d y == scaleR c x + (z + scaleR d y)"
1.104 +  "scaleR c x + (scaleR d y + z) == scaleR c x + (scaleR d y + z)"
1.105 +  "(scaleR c x + w) + (scaleR d y + z) == scaleR c x + (w + (scaleR d y + z))"
1.106 +  by (simp_all add: algebra_simps)
1.107 +
1.108 +lemma pth_c:
1.109 +  fixes x :: "'a::real_normed_vector" shows
1.110 +  "scaleR c x + scaleR d y == scaleR d y + scaleR c x"
1.111 +  "(scaleR c x + z) + scaleR d y == scaleR d y + (scaleR c x + z)"
1.112 +  "scaleR c x + (scaleR d y + z) == scaleR d y + (scaleR c x + z)"
1.113 +  "(scaleR c x + w) + (scaleR d y + z) == scaleR d y + ((scaleR c x + w) + z)"
1.114 +  by (simp_all add: algebra_simps)
1.115 +
1.116 +lemma pth_d:
1.117 +  fixes x :: "'a::real_normed_vector"
1.118 +  shows "x + 0 == x" by simp
1.119 +
1.120 +lemma norm_imp_pos_and_ge:
1.121 +  fixes x :: "'a::real_normed_vector"
1.122 +  shows "norm x == n \<Longrightarrow> norm x \<ge> 0 \<and> n \<ge> norm x"
1.123 +  by atomize auto
1.124
1.125  lemma real_eq_0_iff_le_ge_0: "(x::real) = 0 == x \<ge> 0 \<and> -x \<ge> 0" by arith
1.126
1.127  lemma norm_pths:
1.128 -  "(x::real ^'n::finite) = y \<longleftrightarrow> norm (x - y) \<le> 0"
1.129 +  fixes x :: "'a::real_normed_vector" shows
1.130 +  "x = y \<longleftrightarrow> norm (x - y) \<le> 0"
1.131    "x \<noteq> y \<longleftrightarrow> \<not> (norm (x - y) \<le> 0)"
1.132    using norm_ge_zero[of "x - y"] by auto
1.133
1.134  lemma vector_dist_norm:
1.135 -  fixes x y :: "real ^ _"
1.136 +  fixes x :: "'a::real_normed_vector"
1.137    shows "dist x y = norm (x - y)"
1.138    by (rule dist_norm)
1.139
1.140 @@ -1117,7 +1166,6 @@
1.141  *} "Proves simple linear statements about vector norms"
1.142
1.143
1.144 -
1.145  text{* Hence more metric properties. *}
1.146
1.147  lemma dist_triangle_alt:
1.148 @@ -1158,7 +1206,7 @@
1.150    fixes x y x' y' :: "'a::real_normed_vector"
1.151    shows "dist (x + y) (x' + y') <= dist x x' + dist y y'"
1.152 -unfolding dist_norm by (rule norm_diff_triangle_ineq)
1.153 +  by norm
1.154
1.155  lemma dist_mul[simp]: "dist (c *s x) (c *s y) = \<bar>c\<bar> * dist x y"
1.156    unfolding dist_norm vector_ssub_ldistrib[symmetric] norm_mul ..
1.157 @@ -1166,7 +1214,7 @@