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.22 +lemma norm_add_rule_thm:
    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.149  lemma dist_triangle_add:
   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 @@
   1.158  lemma dist_triangle_add_half:
   1.159    fixes x x' y y' :: "'a::real_normed_vector"
   1.160    shows "dist x x' < e / 2 \<Longrightarrow> dist y y' < e / 2 \<Longrightarrow> dist(x + y) (x' + y') < e"
   1.161 -by (rule le_less_trans [OF dist_triangle_add], simp)
   1.162 +  by norm
   1.163  
   1.164  lemma setsum_component [simp]:
   1.165    fixes f:: " 'a \<Rightarrow> ('b::comm_monoid_add) ^'n"