src/HOL/Library/Product_Vector.thy
 changeset 31339 b4660351e8e7 parent 31290 f41c023d90bc child 31388 e0c05b595d1f
```     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.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.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.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]:
```