src/HOL/Library/Product_Vector.thy
changeset 36332 3ddb2bc07784
parent 34110 4c113c744b86
child 36660 1cc4ab4b7ff7
     1.1 --- a/src/HOL/Library/Product_Vector.thy	Sat Apr 24 09:34:36 2010 -0700
     1.2 +++ b/src/HOL/Library/Product_Vector.thy	Sat Apr 24 09:37:24 2010 -0700
     1.3 @@ -49,21 +49,37 @@
     1.4    "open (S :: ('a \<times> 'b) set) \<longleftrightarrow>
     1.5      (\<forall>x\<in>S. \<exists>A B. open A \<and> open B \<and> x \<in> A \<times> B \<and> A \<times> B \<subseteq> S)"
     1.6  
     1.7 +lemma open_prod_elim:
     1.8 +  assumes "open S" and "x \<in> S"
     1.9 +  obtains A B where "open A" and "open B" and "x \<in> A \<times> B" and "A \<times> B \<subseteq> S"
    1.10 +using assms unfolding open_prod_def by fast
    1.11 +
    1.12 +lemma open_prod_intro:
    1.13 +  assumes "\<And>x. x \<in> S \<Longrightarrow> \<exists>A B. open A \<and> open B \<and> x \<in> A \<times> B \<and> A \<times> B \<subseteq> S"
    1.14 +  shows "open S"
    1.15 +using assms unfolding open_prod_def by fast
    1.16 +
    1.17  instance proof
    1.18    show "open (UNIV :: ('a \<times> 'b) set)"
    1.19      unfolding open_prod_def by auto
    1.20  next
    1.21    fix S T :: "('a \<times> 'b) set"
    1.22 -  assume "open S" "open T" thus "open (S \<inter> T)"
    1.23 -    unfolding open_prod_def
    1.24 -    apply clarify
    1.25 -    apply (drule (1) bspec)+
    1.26 -    apply (clarify, rename_tac Sa Ta Sb Tb)
    1.27 -    apply (rule_tac x="Sa \<inter> Ta" in exI)
    1.28 -    apply (rule_tac x="Sb \<inter> Tb" in exI)
    1.29 -    apply (simp add: open_Int)
    1.30 -    apply fast
    1.31 -    done
    1.32 +  assume "open S" "open T"
    1.33 +  show "open (S \<inter> T)"
    1.34 +  proof (rule open_prod_intro)
    1.35 +    fix x assume x: "x \<in> S \<inter> T"
    1.36 +    from x have "x \<in> S" by simp
    1.37 +    obtain Sa Sb where A: "open Sa" "open Sb" "x \<in> Sa \<times> Sb" "Sa \<times> Sb \<subseteq> S"
    1.38 +      using `open S` and `x \<in> S` by (rule open_prod_elim)
    1.39 +    from x have "x \<in> T" by simp
    1.40 +    obtain Ta Tb where B: "open Ta" "open Tb" "x \<in> Ta \<times> Tb" "Ta \<times> Tb \<subseteq> T"
    1.41 +      using `open T` and `x \<in> T` by (rule open_prod_elim)
    1.42 +    let ?A = "Sa \<inter> Ta" and ?B = "Sb \<inter> Tb"
    1.43 +    have "open ?A \<and> open ?B \<and> x \<in> ?A \<times> ?B \<and> ?A \<times> ?B \<subseteq> S \<inter> T"
    1.44 +      using A B by (auto simp add: open_Int)
    1.45 +    thus "\<exists>A B. open A \<and> open B \<and> x \<in> A \<times> B \<and> A \<times> B \<subseteq> S \<inter> T"
    1.46 +      by fast
    1.47 +  qed
    1.48  next
    1.49    fix K :: "('a \<times> 'b) set set"
    1.50    assume "\<forall>S\<in>K. open S" thus "open (\<Union>K)"
    1.51 @@ -151,6 +167,12 @@
    1.52  lemma dist_Pair_Pair: "dist (a, b) (c, d) = sqrt ((dist a c)\<twosuperior> + (dist b d)\<twosuperior>)"
    1.53    unfolding dist_prod_def by simp
    1.54  
    1.55 +lemma dist_fst_le: "dist (fst x) (fst y) \<le> dist x y"
    1.56 +unfolding dist_prod_def by (rule real_sqrt_sum_squares_ge1)
    1.57 +
    1.58 +lemma dist_snd_le: "dist (snd x) (snd y) \<le> dist x y"
    1.59 +unfolding dist_prod_def by (rule real_sqrt_sum_squares_ge2)
    1.60 +
    1.61  instance proof
    1.62    fix x y :: "'a \<times> 'b"
    1.63    show "dist x y = 0 \<longleftrightarrow> x = y"
    1.64 @@ -168,23 +190,32 @@
    1.65    fix S :: "('a \<times> 'b) set"
    1.66    show "open S \<longleftrightarrow> (\<forall>x\<in>S. \<exists>e>0. \<forall>y. dist y x < e \<longrightarrow> y \<in> S)"
    1.67    proof
    1.68 -    assume "open S" thus "\<forall>x\<in>S. \<exists>e>0. \<forall>y. dist y x < e \<longrightarrow> y \<in> S"
    1.69 -    unfolding open_prod_def open_dist
    1.70 -    apply safe
    1.71 -    apply (drule (1) bspec)
    1.72 -    apply clarify
    1.73 -    apply (drule (1) bspec)+
    1.74 -    apply (clarify, rename_tac r s)
    1.75 -    apply (rule_tac x="min r s" in exI, simp)
    1.76 -    apply (clarify, rename_tac c d)
    1.77 -    apply (erule subsetD)
    1.78 -    apply (simp add: dist_Pair_Pair)
    1.79 -    apply (rule conjI)
    1.80 -    apply (drule spec, erule mp)
    1.81 -    apply (erule le_less_trans [OF real_sqrt_sum_squares_ge1])
    1.82 -    apply (drule spec, erule mp)
    1.83 -    apply (erule le_less_trans [OF real_sqrt_sum_squares_ge2])
    1.84 -    done
    1.85 +    assume "open S" show "\<forall>x\<in>S. \<exists>e>0. \<forall>y. dist y x < e \<longrightarrow> y \<in> S"
    1.86 +    proof
    1.87 +      fix x assume "x \<in> S"
    1.88 +      obtain A B where "open A" "open B" "x \<in> A \<times> B" "A \<times> B \<subseteq> S"
    1.89 +        using `open S` and `x \<in> S` by (rule open_prod_elim)
    1.90 +      obtain r where r: "0 < r" "\<forall>y. dist y (fst x) < r \<longrightarrow> y \<in> A"
    1.91 +        using `open A` and `x \<in> A \<times> B` unfolding open_dist by auto
    1.92 +      obtain s where s: "0 < s" "\<forall>y. dist y (snd x) < s \<longrightarrow> y \<in> B"
    1.93 +        using `open B` and `x \<in> A \<times> B` unfolding open_dist by auto
    1.94 +      let ?e = "min r s"
    1.95 +      have "0 < ?e \<and> (\<forall>y. dist y x < ?e \<longrightarrow> y \<in> S)"
    1.96 +      proof (intro allI impI conjI)
    1.97 +        show "0 < min r s" by (simp add: r(1) s(1))
    1.98 +      next
    1.99 +        fix y assume "dist y x < min r s"
   1.100 +        hence "dist y x < r" and "dist y x < s"
   1.101 +          by simp_all
   1.102 +        hence "dist (fst y) (fst x) < r" and "dist (snd y) (snd x) < s"
   1.103 +          by (auto intro: le_less_trans dist_fst_le dist_snd_le)
   1.104 +        hence "fst y \<in> A" and "snd y \<in> B"
   1.105 +          by (simp_all add: r(2) s(2))
   1.106 +        hence "y \<in> A \<times> B" by (induct y, simp)
   1.107 +        with `A \<times> B \<subseteq> S` show "y \<in> S" ..
   1.108 +      qed
   1.109 +      thus "\<exists>e>0. \<forall>y. dist y x < e \<longrightarrow> y \<in> S" ..
   1.110 +    qed
   1.111    next
   1.112      assume "\<forall>x\<in>S. \<exists>e>0. \<forall>y. dist y x < e \<longrightarrow> y \<in> S" thus "open S"
   1.113      unfolding open_prod_def open_dist
   1.114 @@ -223,12 +254,6 @@
   1.115  
   1.116  subsection {* Continuity of operations *}
   1.117  
   1.118 -lemma dist_fst_le: "dist (fst x) (fst y) \<le> dist x y"
   1.119 -unfolding dist_prod_def by simp
   1.120 -
   1.121 -lemma dist_snd_le: "dist (snd x) (snd y) \<le> dist x y"
   1.122 -unfolding dist_prod_def by simp
   1.123 -
   1.124  lemma tendsto_fst [tendsto_intros]:
   1.125    assumes "(f ---> a) net"
   1.126    shows "((\<lambda>x. fst (f x)) ---> fst a) net"