--- a/src/HOL/Library/Euclidean_Space.thy Fri May 29 14:09:58 2009 -0700
+++ b/src/HOL/Library/Euclidean_Space.thy Fri May 29 15:32:33 2009 -0700
@@ -498,6 +498,30 @@
apply simp
done
+subsection {* Metric *}
+
+instantiation "^" :: (metric_space, finite) metric_space
+begin
+
+definition dist_vector_def:
+ "dist (x::'a^'b) (y::'a^'b) = setL2 (\<lambda>i. dist (x$i) (y$i)) UNIV"
+
+instance proof
+ fix x y :: "'a ^ 'b"
+ show "dist x y = 0 \<longleftrightarrow> x = y"
+ unfolding dist_vector_def
+ by (simp add: setL2_eq_0_iff Cart_eq)
+next
+ fix x y z :: "'a ^ 'b"
+ show "dist x y \<le> dist x z + dist y z"
+ unfolding dist_vector_def
+ apply (rule order_trans [OF _ setL2_triangle_ineq])
+ apply (simp add: setL2_mono dist_triangle2)
+ done
+qed
+
+end
+
subsection {* Norms *}
instantiation "^" :: (real_normed_vector, finite) real_normed_vector
@@ -509,9 +533,6 @@
definition vector_sgn_def:
"sgn (x::'a^'b) = scaleR (inverse (norm x)) x"
-definition dist_vector_def:
- "dist (x::'a^'b) y = norm (x - y)"
-
instance proof
fix a :: real and x y :: "'a ^ 'b"
show "0 \<le> norm x"
@@ -531,7 +552,8 @@
show "sgn x = scaleR (inverse (norm x)) x"
by (rule vector_sgn_def)
show "dist x y = norm (x - y)"
- by (rule dist_vector_def)
+ unfolding dist_vector_def vector_norm_def
+ by (simp add: dist_norm)
qed
end
@@ -949,6 +971,11 @@
"x \<noteq> y \<longleftrightarrow> \<not> (norm (x - y) \<le> 0)"
using norm_ge_zero[of "x - y"] by auto
+lemma vector_dist_norm:
+ fixes x y :: "real ^ _"
+ shows "dist x y = norm (x - y)"
+ by (rule dist_norm)
+
use "normarith.ML"
method_setup norm = {* Scan.succeed (SIMPLE_METHOD' o NormArith.norm_arith_tac)
@@ -2566,7 +2593,7 @@
qed
lemma dist_fstcart: "dist(fstcart (x::real^_)) (fstcart y) <= dist x y"
- by (metis dist_vector_def fstcart_sub[symmetric] norm_fstcart)
+ unfolding dist_norm by (metis fstcart_sub[symmetric] norm_fstcart)
lemma norm_sndcart: "norm(sndcart x) <= norm (x::real ^('n::finite + 'm::finite))"
proof-
@@ -2581,7 +2608,7 @@
qed
lemma dist_sndcart: "dist(sndcart (x::real^_)) (sndcart y) <= dist x y"
- by (metis dist_vector_def sndcart_sub[symmetric] norm_sndcart)
+ unfolding dist_norm by (metis sndcart_sub[symmetric] norm_sndcart)
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"
by (simp add: dot_def setsum_UNIV_sum pastecart_def)
--- a/src/HOL/Library/Topology_Euclidean_Space.thy Fri May 29 14:09:58 2009 -0700
+++ b/src/HOL/Library/Topology_Euclidean_Space.thy Fri May 29 15:32:33 2009 -0700
@@ -1314,7 +1314,7 @@
{ fix x
have "netord net x y \<longrightarrow> dist (h (f x)) (h l) < e"
using y(2) b unfolding dist_norm using linear_sub[of h "f x" l] `linear h`
- apply auto by (metis b(1) b(2) dist_vector_def dist_commute less_le_not_le linorder_not_le mult_imp_div_pos_le real_mult_commute xt1(7)) (* FIXME: VERY slow! *)
+ apply auto by (metis b(1) b(2) less_le_not_le linorder_not_le mult_imp_div_pos_le real_mult_commute xt1(7)) (* FIXME: VERY slow! *)
}
hence " (\<exists>y. (\<exists>x. netord net x y) \<and> (\<forall>x. netord net x y \<longrightarrow> dist (h (f x)) (h l) < e))" using y
by(rule_tac x="y" in exI) auto
@@ -2353,7 +2353,7 @@
hence N:"\<forall>n. N \<le> n \<longrightarrow> dist (s N) (s n) < 1" by auto
{ fix n::nat assume "n\<ge>N"
hence "norm (s n) \<le> norm (s N) + 1" using N apply(erule_tac x=n in allE) unfolding dist_norm
- using norm_triangle_sub[of "s N" "s n"] by (auto, metis dist_vector_def dist_commute le_add_right_mono norm_triangle_sub real_less_def)
+ using norm_triangle_sub[of "s N" "s n"] by (auto, metis norm_minus_commute le_add_right_mono norm_triangle_sub real_less_def)
}
hence "\<forall>n\<ge>N. norm (s n) \<le> norm (s N) + 1" by auto
moreover
--- a/src/HOL/Library/normarith.ML Fri May 29 14:09:58 2009 -0700
+++ b/src/HOL/Library/normarith.ML Fri May 29 15:32:33 2009 -0700
@@ -391,7 +391,7 @@
fun init_conv ctxt =
Simplifier.rewrite (Simplifier.context ctxt
- (HOL_basic_ss addsimps ([@{thm vec_0}, @{thm vec_1}, @{thm dist_vector_def}, @{thm diff_0_right}, @{thm right_minus}, @{thm diff_self}, @{thm norm_0}] @ @{thms arithmetic_simps} @ @{thms norm_pths})))
+ (HOL_basic_ss addsimps ([@{thm vec_0}, @{thm vec_1}, @{thm vector_dist_norm}, @{thm diff_0_right}, @{thm right_minus}, @{thm diff_self}, @{thm norm_0}] @ @{thms arithmetic_simps} @ @{thms norm_pths})))
then_conv field_comp_conv
then_conv nnf_conv