instance * :: (metric_space, metric_space) metric_space; generalize lemmas to class metric_space
authorhuffman
Fri May 29 09:58:14 2009 -0700 (2009-05-29)
changeset 31339b4660351e8e7
parent 31338 d41a8ba25b67
child 31340 5cddd98abe14
instance * :: (metric_space, metric_space) metric_space; generalize lemmas to class metric_space
src/HOL/Library/Product_Vector.thy
     1.1 --- a/src/HOL/Library/Product_Vector.thy	Fri May 29 09:22:56 2009 -0700
     1.2 +++ b/src/HOL/Library/Product_Vector.thy	Fri May 29 09:58:14 2009 -0700
     1.3 @@ -39,6 +39,38 @@
     1.4  
     1.5  end
     1.6  
     1.7 +subsection {* Product is a metric space *}
     1.8 +
     1.9 +instantiation
    1.10 +  "*" :: (metric_space, metric_space) metric_space
    1.11 +begin
    1.12 +
    1.13 +definition dist_prod_def:
    1.14 +  "dist (x::'a \<times> 'b) y = sqrt ((dist (fst x) (fst y))\<twosuperior> + (dist (snd x) (snd y))\<twosuperior>)"
    1.15 +
    1.16 +lemma dist_Pair_Pair: "dist (a, b) (c, d) = sqrt ((dist a c)\<twosuperior> + (dist b d)\<twosuperior>)"
    1.17 +  unfolding dist_prod_def by simp
    1.18 +
    1.19 +instance proof
    1.20 +  fix x y :: "'a \<times> 'b"
    1.21 +  show "dist x y = 0 \<longleftrightarrow> x = y"
    1.22 +    unfolding dist_prod_def
    1.23 +    by (simp add: expand_prod_eq)
    1.24 +next
    1.25 +  fix x y z :: "'a \<times> 'b"
    1.26 +  show "dist x y \<le> dist x z + dist y z"
    1.27 +    unfolding dist_prod_def
    1.28 +    apply (rule order_trans [OF _ real_sqrt_sum_squares_triangle_ineq])
    1.29 +    apply (rule real_sqrt_le_mono)
    1.30 +    apply (rule order_trans [OF add_mono])
    1.31 +    apply (rule power_mono [OF dist_triangle2 [of _ _ "fst z"] zero_le_dist])
    1.32 +    apply (rule power_mono [OF dist_triangle2 [of _ _ "snd z"] zero_le_dist])
    1.33 +    apply (simp only: real_sum_squared_expand)
    1.34 +    done
    1.35 +qed
    1.36 +
    1.37 +end
    1.38 +
    1.39  subsection {* Product is a normed vector space *}
    1.40  
    1.41  instantiation
    1.42 @@ -51,9 +83,6 @@
    1.43  definition sgn_prod_def:
    1.44    "sgn (x::'a \<times> 'b) = scaleR (inverse (norm x)) x"
    1.45  
    1.46 -definition dist_prod_def:
    1.47 -  "dist (x::'a \<times> 'b) y = norm (x - y)"
    1.48 -
    1.49  lemma norm_Pair: "norm (a, b) = sqrt ((norm a)\<twosuperior> + (norm b)\<twosuperior>)"
    1.50    unfolding norm_prod_def by simp
    1.51  
    1.52 @@ -78,7 +107,8 @@
    1.53    show "sgn x = scaleR (inverse (norm x)) x"
    1.54      by (rule sgn_prod_def)
    1.55    show "dist x y = norm (x - y)"
    1.56 -    by (rule dist_prod_def)
    1.57 +    unfolding dist_prod_def norm_prod_def
    1.58 +    by (simp add: dist_norm)
    1.59  qed
    1.60  
    1.61  end
    1.62 @@ -179,53 +209,53 @@
    1.63  lemma LIMSEQ_Pair:
    1.64    assumes "X ----> a" and "Y ----> b"
    1.65    shows "(\<lambda>n. (X n, Y n)) ----> (a, b)"
    1.66 -proof (rule LIMSEQ_I)
    1.67 +proof (rule metric_LIMSEQ_I)
    1.68    fix r :: real assume "0 < r"
    1.69    then have "0 < r / sqrt 2" (is "0 < ?s")
    1.70      by (simp add: divide_pos_pos)
    1.71 -  obtain M where M: "\<forall>n\<ge>M. norm (X n - a) < ?s"
    1.72 -    using LIMSEQ_D [OF `X ----> a` `0 < ?s`] ..
    1.73 -  obtain N where N: "\<forall>n\<ge>N. norm (Y n - b) < ?s"
    1.74 -    using LIMSEQ_D [OF `Y ----> b` `0 < ?s`] ..
    1.75 -  have "\<forall>n\<ge>max M N. norm ((X n, Y n) - (a, b)) < r"
    1.76 -    using M N by (simp add: real_sqrt_sum_squares_less norm_Pair)
    1.77 -  then show "\<exists>n0. \<forall>n\<ge>n0. norm ((X n, Y n) - (a, b)) < r" ..
    1.78 +  obtain M where M: "\<forall>n\<ge>M. dist (X n) a < ?s"
    1.79 +    using metric_LIMSEQ_D [OF `X ----> a` `0 < ?s`] ..
    1.80 +  obtain N where N: "\<forall>n\<ge>N. dist (Y n) b < ?s"
    1.81 +    using metric_LIMSEQ_D [OF `Y ----> b` `0 < ?s`] ..
    1.82 +  have "\<forall>n\<ge>max M N. dist (X n, Y n) (a, b) < r"
    1.83 +    using M N by (simp add: real_sqrt_sum_squares_less dist_Pair_Pair)
    1.84 +  then show "\<exists>n0. \<forall>n\<ge>n0. dist (X n, Y n) (a, b) < r" ..
    1.85  qed
    1.86  
    1.87  lemma Cauchy_Pair:
    1.88    assumes "Cauchy X" and "Cauchy Y"
    1.89    shows "Cauchy (\<lambda>n. (X n, Y n))"
    1.90 -proof (rule CauchyI)
    1.91 +proof (rule metric_CauchyI)
    1.92    fix r :: real assume "0 < r"
    1.93    then have "0 < r / sqrt 2" (is "0 < ?s")
    1.94      by (simp add: divide_pos_pos)
    1.95 -  obtain M where M: "\<forall>m\<ge>M. \<forall>n\<ge>M. norm (X m - X n) < ?s"
    1.96 -    using CauchyD [OF `Cauchy X` `0 < ?s`] ..
    1.97 -  obtain N where N: "\<forall>m\<ge>N. \<forall>n\<ge>N. norm (Y m - Y n) < ?s"
    1.98 -    using CauchyD [OF `Cauchy Y` `0 < ?s`] ..
    1.99 -  have "\<forall>m\<ge>max M N. \<forall>n\<ge>max M N. norm ((X m, Y m) - (X n, Y n)) < r"
   1.100 -    using M N by (simp add: real_sqrt_sum_squares_less norm_Pair)
   1.101 -  then show "\<exists>n0. \<forall>m\<ge>n0. \<forall>n\<ge>n0. norm ((X m, Y m) - (X n, Y n)) < r" ..
   1.102 +  obtain M where M: "\<forall>m\<ge>M. \<forall>n\<ge>M. dist (X m) (X n) < ?s"
   1.103 +    using metric_CauchyD [OF `Cauchy X` `0 < ?s`] ..
   1.104 +  obtain N where N: "\<forall>m\<ge>N. \<forall>n\<ge>N. dist (Y m) (Y n) < ?s"
   1.105 +    using metric_CauchyD [OF `Cauchy Y` `0 < ?s`] ..
   1.106 +  have "\<forall>m\<ge>max M N. \<forall>n\<ge>max M N. dist (X m, Y m) (X n, Y n) < r"
   1.107 +    using M N by (simp add: real_sqrt_sum_squares_less dist_Pair_Pair)
   1.108 +  then show "\<exists>n0. \<forall>m\<ge>n0. \<forall>n\<ge>n0. dist (X m, Y m) (X n, Y n) < r" ..
   1.109  qed
   1.110  
   1.111  lemma LIM_Pair:
   1.112    assumes "f -- x --> a" and "g -- x --> b"
   1.113    shows "(\<lambda>x. (f x, g x)) -- x --> (a, b)"
   1.114 -proof (rule LIM_I)
   1.115 +proof (rule metric_LIM_I)
   1.116    fix r :: real assume "0 < r"
   1.117    then have "0 < r / sqrt 2" (is "0 < ?e")
   1.118      by (simp add: divide_pos_pos)
   1.119    obtain s where s: "0 < s"
   1.120 -    "\<forall>z. z \<noteq> x \<and> norm (z - x) < s \<longrightarrow> norm (f z - a) < ?e"
   1.121 -    using LIM_D [OF `f -- x --> a` `0 < ?e`] by fast
   1.122 +    "\<forall>z. z \<noteq> x \<and> dist z x < s \<longrightarrow> dist (f z) a < ?e"
   1.123 +    using metric_LIM_D [OF `f -- x --> a` `0 < ?e`] by fast
   1.124    obtain t where t: "0 < t"
   1.125 -    "\<forall>z. z \<noteq> x \<and> norm (z - x) < t \<longrightarrow> norm (g z - b) < ?e"
   1.126 -    using LIM_D [OF `g -- x --> b` `0 < ?e`] by fast
   1.127 +    "\<forall>z. z \<noteq> x \<and> dist z x < t \<longrightarrow> dist (g z) b < ?e"
   1.128 +    using metric_LIM_D [OF `g -- x --> b` `0 < ?e`] by fast
   1.129    have "0 < min s t \<and>
   1.130 -    (\<forall>z. z \<noteq> x \<and> norm (z - x) < min s t \<longrightarrow> norm ((f z, g z) - (a, b)) < r)"
   1.131 -    using s t by (simp add: real_sqrt_sum_squares_less norm_Pair)
   1.132 +    (\<forall>z. z \<noteq> x \<and> dist z x < min s t \<longrightarrow> dist (f z, g z) (a, b) < r)"
   1.133 +    using s t by (simp add: real_sqrt_sum_squares_less dist_Pair_Pair)
   1.134    then show
   1.135 -    "\<exists>s>0. \<forall>z. z \<noteq> x \<and> norm (z - x) < s \<longrightarrow> norm ((f z, g z) - (a, b)) < r" ..
   1.136 +    "\<exists>s>0. \<forall>z. z \<noteq> x \<and> dist z x < s \<longrightarrow> dist (f z, g z) (a, b) < r" ..
   1.137  qed
   1.138  
   1.139  lemma isCont_Pair [simp]: