src/HOL/Library/Product_Vector.thy
changeset 31417 c12b25b7f015
parent 31415 80686a815b59
child 31491 f7310185481d
     1.1 --- a/src/HOL/Library/Product_Vector.thy	Wed Jun 03 08:46:13 2009 -0700
     1.2 +++ b/src/HOL/Library/Product_Vector.thy	Wed Jun 03 09:58:11 2009 -0700
     1.3 @@ -45,28 +45,29 @@
     1.4    "*" :: (topological_space, topological_space) topological_space
     1.5  begin
     1.6  
     1.7 -definition open_prod_def:
     1.8 -  "open S = (\<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.9 +definition topo_prod_def:
    1.10 +  "topo = {S. \<forall>x\<in>S. \<exists>A\<in>topo. \<exists>B\<in>topo. x \<in> A \<times> B \<and> A \<times> B \<subseteq> S}"
    1.11  
    1.12  instance proof
    1.13 -  show "open (UNIV :: ('a \<times> 'b) set)"
    1.14 -    unfolding open_prod_def by (fast intro: open_UNIV)
    1.15 +  show "(UNIV :: ('a \<times> 'b) set) \<in> topo"
    1.16 +    unfolding topo_prod_def by (auto intro: topo_UNIV)
    1.17  next
    1.18    fix S T :: "('a \<times> 'b) set"
    1.19 -  assume "open S" "open T" thus "open (S \<inter> T)"
    1.20 -    unfolding open_prod_def
    1.21 +  assume "S \<in> topo" "T \<in> topo" thus "S \<inter> T \<in> topo"
    1.22 +    unfolding topo_prod_def
    1.23      apply clarify
    1.24      apply (drule (1) bspec)+
    1.25      apply (clarify, rename_tac Sa Ta Sb Tb)
    1.26 -    apply (rule_tac x="Sa \<inter> Ta" in exI)
    1.27 -    apply (rule_tac x="Sb \<inter> Tb" in exI)
    1.28 -    apply (simp add: open_Int)
    1.29 +    apply (rule_tac x="Sa \<inter> Ta" in rev_bexI)
    1.30 +    apply (simp add: topo_Int)
    1.31 +    apply (rule_tac x="Sb \<inter> Tb" in rev_bexI)
    1.32 +    apply (simp add: topo_Int)
    1.33      apply fast
    1.34      done
    1.35  next
    1.36    fix T :: "('a \<times> 'b) set set"
    1.37 -  assume "\<forall>A\<in>T. open A" thus "open (\<Union>T)"
    1.38 -    unfolding open_prod_def by fast
    1.39 +  assume "T \<subseteq> topo" thus "\<Union>T \<in> topo"
    1.40 +    unfolding topo_prod_def Bex_def by fast
    1.41  qed
    1.42  
    1.43  end
    1.44 @@ -103,10 +104,9 @@
    1.45    (* FIXME: long proof! *)
    1.46    (* Maybe it would be easier to define topological spaces *)
    1.47    (* in terms of neighborhoods instead of open sets? *)
    1.48 -  fix S :: "('a \<times> 'b) set"
    1.49 -  show "open S = (\<forall>x\<in>S. \<exists>e>0. \<forall>y. dist y x < e \<longrightarrow> y \<in> S)"
    1.50 -    unfolding open_prod_def open_dist
    1.51 -    apply safe
    1.52 +  show "topo = {S::('a \<times> 'b) set. \<forall>x\<in>S. \<exists>e>0. \<forall>y. dist y x < e \<longrightarrow> y \<in> S}"
    1.53 +    unfolding topo_prod_def topo_dist
    1.54 +    apply (safe, rename_tac S a b)
    1.55      apply (drule (1) bspec)
    1.56      apply clarify
    1.57      apply (drule (1) bspec)+
    1.58 @@ -121,19 +121,18 @@
    1.59      apply (drule spec, erule mp)
    1.60      apply (erule le_less_trans [OF real_sqrt_sum_squares_ge2])
    1.61  
    1.62 +    apply (rename_tac S a b)
    1.63      apply (drule (1) bspec)
    1.64      apply clarify
    1.65      apply (subgoal_tac "\<exists>r>0. \<exists>s>0. e = sqrt (r\<twosuperior> + s\<twosuperior>)")
    1.66      apply clarify
    1.67 -    apply (rule_tac x="{y. dist y a < r}" in exI)
    1.68 -    apply (rule_tac x="{y. dist y b < s}" in exI)
    1.69 -    apply (rule conjI)
    1.70 +    apply (rule_tac x="{y. dist y a < r}" in rev_bexI)
    1.71      apply clarify
    1.72      apply (rule_tac x="r - dist x a" in exI, rule conjI, simp)
    1.73      apply clarify
    1.74      apply (rule le_less_trans [OF dist_triangle])
    1.75      apply (erule less_le_trans [OF add_strict_right_mono], simp)
    1.76 -    apply (rule conjI)
    1.77 +    apply (rule_tac x="{y. dist y b < s}" in rev_bexI)
    1.78      apply clarify
    1.79      apply (rule_tac x="s - dist x b" in exI, rule conjI, simp)
    1.80      apply clarify