instance ^ :: (metric_space, finite) metric_space
authorhuffman
Fri May 29 15:32:33 2009 -0700 (2009-05-29)
changeset 31344fc09ec06b89b
parent 31343 9983f648f9bb
child 31345 80667d5bee32
instance ^ :: (metric_space, finite) metric_space
src/HOL/Library/Euclidean_Space.thy
src/HOL/Library/Topology_Euclidean_Space.thy
src/HOL/Library/normarith.ML
     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)
     2.1 --- a/src/HOL/Library/Topology_Euclidean_Space.thy	Fri May 29 14:09:58 2009 -0700
     2.2 +++ b/src/HOL/Library/Topology_Euclidean_Space.thy	Fri May 29 15:32:33 2009 -0700
     2.3 @@ -1314,7 +1314,7 @@
     2.4      { fix x
     2.5        have "netord net x y \<longrightarrow> dist (h (f x)) (h l) < e"
     2.6  	using y(2) b unfolding dist_norm using linear_sub[of h "f x" l] `linear h`
     2.7 -	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! *)
     2.8 +	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! *)
     2.9      }
    2.10      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
    2.11        by(rule_tac x="y" in exI) auto
    2.12 @@ -2353,7 +2353,7 @@
    2.13    hence N:"\<forall>n. N \<le> n \<longrightarrow> dist (s N) (s n) < 1" by auto
    2.14    { fix n::nat assume "n\<ge>N"
    2.15      hence "norm (s n) \<le> norm (s N) + 1" using N apply(erule_tac x=n in allE) unfolding dist_norm
    2.16 -      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)
    2.17 +      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)
    2.18    }
    2.19    hence "\<forall>n\<ge>N. norm (s n) \<le> norm (s N) + 1" by auto
    2.20    moreover
     3.1 --- a/src/HOL/Library/normarith.ML	Fri May 29 14:09:58 2009 -0700
     3.2 +++ b/src/HOL/Library/normarith.ML	Fri May 29 15:32:33 2009 -0700
     3.3 @@ -391,7 +391,7 @@
     3.4  
     3.5    fun init_conv ctxt = 
     3.6     Simplifier.rewrite (Simplifier.context ctxt 
     3.7 -     (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})))
     3.8 +     (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})))
     3.9     then_conv field_comp_conv 
    3.10     then_conv nnf_conv
    3.11