src/HOL/Library/Euclidean_Space.thy
 changeset 31344 fc09ec06b89b parent 31340 5cddd98abe14 child 31389 3affcbc60c6d
```     1.1 --- a/src/HOL/Library/Euclidean_Space.thy	Fri May 29 14:09:58 2009 -0700
1.2 +++ b/src/HOL/Library/Euclidean_Space.thy	Fri May 29 15:32:33 2009 -0700
1.3 @@ -498,6 +498,30 @@
1.4    apply simp
1.5    done
1.6
1.7 +subsection {* Metric *}
1.8 +
1.9 +instantiation "^" :: (metric_space, finite) metric_space
1.10 +begin
1.11 +
1.12 +definition dist_vector_def:
1.13 +  "dist (x::'a^'b) (y::'a^'b) = setL2 (\<lambda>i. dist (x\$i) (y\$i)) UNIV"
1.14 +
1.15 +instance proof
1.16 +  fix x y :: "'a ^ 'b"
1.17 +  show "dist x y = 0 \<longleftrightarrow> x = y"
1.18 +    unfolding dist_vector_def
1.19 +    by (simp add: setL2_eq_0_iff Cart_eq)
1.20 +next
1.21 +  fix x y z :: "'a ^ 'b"
1.22 +  show "dist x y \<le> dist x z + dist y z"
1.23 +    unfolding dist_vector_def
1.24 +    apply (rule order_trans [OF _ setL2_triangle_ineq])
1.25 +    apply (simp add: setL2_mono dist_triangle2)
1.26 +    done
1.27 +qed
1.28 +
1.29 +end
1.30 +
1.31  subsection {* Norms *}
1.32
1.33  instantiation "^" :: (real_normed_vector, finite) real_normed_vector
1.34 @@ -509,9 +533,6 @@
1.35  definition vector_sgn_def:
1.36    "sgn (x::'a^'b) = scaleR (inverse (norm x)) x"
1.37
1.38 -definition dist_vector_def:
1.39 -  "dist (x::'a^'b) y = norm (x - y)"
1.40 -
1.41  instance proof
1.42    fix a :: real and x y :: "'a ^ 'b"
1.43    show "0 \<le> norm x"
1.44 @@ -531,7 +552,8 @@
1.45    show "sgn x = scaleR (inverse (norm x)) x"
1.46      by (rule vector_sgn_def)
1.47    show "dist x y = norm (x - y)"
1.48 -    by (rule dist_vector_def)
1.49 +    unfolding dist_vector_def vector_norm_def
1.50 +    by (simp add: dist_norm)
1.51  qed
1.52
1.53  end
1.54 @@ -949,6 +971,11 @@
1.55    "x \<noteq> y \<longleftrightarrow> \<not> (norm (x - y) \<le> 0)"
1.56    using norm_ge_zero[of "x - y"] by auto
1.57
1.58 +lemma vector_dist_norm:
1.59 +  fixes x y :: "real ^ _"
1.60 +  shows "dist x y = norm (x - y)"
1.61 +  by (rule dist_norm)
1.62 +
1.63  use "normarith.ML"
1.64
1.65  method_setup norm = {* Scan.succeed (SIMPLE_METHOD' o NormArith.norm_arith_tac)
1.66 @@ -2566,7 +2593,7 @@
1.67  qed
1.68
1.69  lemma dist_fstcart: "dist(fstcart (x::real^_)) (fstcart y) <= dist x y"
1.70 -  by (metis dist_vector_def fstcart_sub[symmetric] norm_fstcart)
1.71 +  unfolding dist_norm by (metis fstcart_sub[symmetric] norm_fstcart)
1.72
1.73  lemma norm_sndcart: "norm(sndcart x) <= norm (x::real ^('n::finite + 'm::finite))"
1.74  proof-
1.75 @@ -2581,7 +2608,7 @@
1.76  qed
1.77
1.78  lemma dist_sndcart: "dist(sndcart (x::real^_)) (sndcart y) <= dist x y"
1.79 -  by (metis dist_vector_def sndcart_sub[symmetric] norm_sndcart)
1.80 +  unfolding dist_norm by (metis sndcart_sub[symmetric] norm_sndcart)
1.81
1.82  lemma dot_pastecart: "(pastecart (x1::'a::{times,comm_monoid_add}^'n::finite) (x2::'a::{times,comm_monoid_add}^'m::finite)) \<bullet> (pastecart y1 y2) =  x1 \<bullet> y1 + x2 \<bullet> y2"
1.83    by (simp add: dot_def setsum_UNIV_sum pastecart_def)
```