src/HOL/RealVector.thy
changeset 50999 3de230ed0547
parent 49962 a8cc904a6820
child 51002 496013a6eb38
     1.1 --- a/src/HOL/RealVector.thy	Thu Jan 31 11:31:22 2013 +0100
     1.2 +++ b/src/HOL/RealVector.thy	Thu Jan 31 11:31:27 2013 +0100
     1.3 @@ -508,6 +508,110 @@
     1.4  
     1.5  end
     1.6  
     1.7 +inductive generate_topology for S where
     1.8 +  UNIV: "generate_topology S UNIV"
     1.9 +| Int: "generate_topology S a \<Longrightarrow> generate_topology S b \<Longrightarrow> generate_topology S (a \<inter> b)"
    1.10 +| UN: "(\<And>k. k \<in> K \<Longrightarrow> generate_topology S k) \<Longrightarrow> generate_topology S (\<Union>K)"
    1.11 +| Basis: "s \<in> S \<Longrightarrow> generate_topology S s"
    1.12 +
    1.13 +hide_fact (open) UNIV Int UN Basis 
    1.14 +
    1.15 +lemma generate_topology_Union: 
    1.16 +  "(\<And>k. k \<in> I \<Longrightarrow> generate_topology S (K k)) \<Longrightarrow> generate_topology S (\<Union>k\<in>I. K k)"
    1.17 +  unfolding SUP_def by (intro generate_topology.UN) auto
    1.18 +
    1.19 +lemma topological_space_generate_topology:
    1.20 +  "class.topological_space (generate_topology S)"
    1.21 +  by default (auto intro: generate_topology.intros)
    1.22 +
    1.23 +class order_topology = order + "open" +
    1.24 +  assumes open_generated_order: "open = generate_topology (range (\<lambda>a. {..< a}) \<union> range (\<lambda>a. {a <..}))"
    1.25 +begin
    1.26 +
    1.27 +subclass topological_space
    1.28 +  unfolding open_generated_order
    1.29 +  by (rule topological_space_generate_topology)
    1.30 +
    1.31 +lemma open_greaterThan [simp]: "open {a <..}"
    1.32 +  unfolding open_generated_order by (auto intro: generate_topology.Basis)
    1.33 +
    1.34 +lemma open_lessThan [simp]: "open {..< a}"
    1.35 +  unfolding open_generated_order by (auto intro: generate_topology.Basis)
    1.36 +
    1.37 +lemma open_greaterThanLessThan [simp]: "open {a <..< b}"
    1.38 +   unfolding greaterThanLessThan_eq by (simp add: open_Int)
    1.39 +
    1.40 +end
    1.41 +
    1.42 +class linorder_topology = linorder + order_topology
    1.43 +
    1.44 +lemma closed_atMost [simp]: "closed {.. a::'a::linorder_topology}"
    1.45 +  by (simp add: closed_open)
    1.46 +
    1.47 +lemma closed_atLeast [simp]: "closed {a::'a::linorder_topology ..}"
    1.48 +  by (simp add: closed_open)
    1.49 +
    1.50 +lemma closed_atLeastAtMost [simp]: "closed {a::'a::linorder_topology .. b}"
    1.51 +proof -
    1.52 +  have "{a .. b} = {a ..} \<inter> {.. b}"
    1.53 +    by auto
    1.54 +  then show ?thesis
    1.55 +    by (simp add: closed_Int)
    1.56 +qed
    1.57 +
    1.58 +inductive open_interval :: "'a::order set \<Rightarrow> bool" where
    1.59 +  empty[intro]: "open_interval {}" |
    1.60 +  UNIV[intro]: "open_interval UNIV" |
    1.61 +  greaterThan[intro]: "open_interval {a <..}" |
    1.62 +  lessThan[intro]: "open_interval {..< b}" |
    1.63 +  greaterThanLessThan[intro]: "open_interval {a <..< b}"
    1.64 +hide_fact (open) empty UNIV greaterThan lessThan greaterThanLessThan
    1.65 +
    1.66 +lemma open_intervalD:
    1.67 +  "open_interval S \<Longrightarrow> x \<in> S \<Longrightarrow> y \<in> S \<Longrightarrow> x \<le> z \<Longrightarrow> z \<le> y \<Longrightarrow> z \<in> S"
    1.68 +  by (cases rule: open_interval.cases) auto
    1.69 +
    1.70 +lemma open_interval_Int[intro]:
    1.71 +  fixes S T :: "'a :: linorder set"
    1.72 +  assumes S: "open_interval S" and T: "open_interval T"
    1.73 +  shows "open_interval (S \<inter> T)"
    1.74 +proof -
    1.75 +  { fix a b :: 'a have "{..<b} \<inter> {a<..} = { a <..} \<inter> {..< b }" by auto } note this[simp]
    1.76 +  { fix a b :: 'a and A have "{a <..} \<inter> ({b <..} \<inter> A) = {max a b <..} \<inter> A" by auto } note this[simp]
    1.77 +  { fix a b :: 'a and A have "{..<b} \<inter> (A \<inter> {..<a}) = A \<inter> {..<min a b}" by auto } note this[simp]
    1.78 +  { fix a b :: 'a have "open_interval ({ a <..} \<inter> {..< b})"
    1.79 +      unfolding greaterThanLessThan_eq[symmetric] by auto } note this[simp]
    1.80 +  show ?thesis
    1.81 +    by (cases rule: open_interval.cases[OF S, case_product open_interval.cases[OF T]])
    1.82 +       (auto simp: greaterThanLessThan_eq lessThan_Int_lessThan greaterThan_Int_greaterThan Int_assoc)
    1.83 +qed
    1.84 +
    1.85 +lemma open_interval_imp_open: "open_interval S \<Longrightarrow> open (S::'a::order_topology set)"
    1.86 +  by (cases S rule: open_interval.cases) auto
    1.87 +
    1.88 +lemma open_orderD:
    1.89 +  "open (S::'a::linorder_topology set) \<Longrightarrow> x \<in> S \<Longrightarrow> \<exists>T. open_interval T \<and> T \<subseteq> S \<and> x \<in> T"
    1.90 +  unfolding open_generated_order
    1.91 +proof (induct rule: generate_topology.induct)
    1.92 +  case (UN K) then obtain k where "k \<in> K" "x \<in> k" by auto
    1.93 +  with UN(2)[of k] show ?case by auto
    1.94 +qed auto
    1.95 +
    1.96 +lemma open_order_induct[consumes 2, case_names subset UNIV lessThan greaterThan greaterThanLessThan]:
    1.97 +  fixes S :: "'a::linorder_topology set"
    1.98 +  assumes S: "open S" "x \<in> S"
    1.99 +  assumes subset: "\<And>S T. P S \<Longrightarrow> S \<subseteq> T \<Longrightarrow> P T"
   1.100 +  assumes univ: "P UNIV"
   1.101 +  assumes lt: "\<And>a. x < a \<Longrightarrow> P {..< a}"
   1.102 +  assumes gt: "\<And>a. a < x \<Longrightarrow> P {a <..}"
   1.103 +  assumes lgt: "\<And>a b. a < x \<Longrightarrow> x < b \<Longrightarrow> P {a <..< b}"
   1.104 +  shows "P S"
   1.105 +proof -
   1.106 +  from open_orderD[OF S] obtain T where "open_interval T" "T \<subseteq> S" "x \<in> T"
   1.107 +    by auto
   1.108 +  then show "P S"
   1.109 +    by induct (auto intro: univ subset lt gt lgt)
   1.110 +qed
   1.111  
   1.112  subsection {* Metric spaces *}
   1.113  
   1.114 @@ -859,46 +963,46 @@
   1.115  
   1.116  end
   1.117  
   1.118 -lemma open_real_lessThan [simp]:
   1.119 -  fixes a :: real shows "open {..<a}"
   1.120 -unfolding open_real_def dist_real_def
   1.121 -proof (clarify)
   1.122 -  fix x assume "x < a"
   1.123 -  hence "0 < a - x \<and> (\<forall>y. \<bar>y - x\<bar> < a - x \<longrightarrow> y \<in> {..<a})" by auto
   1.124 -  thus "\<exists>e>0. \<forall>y. \<bar>y - x\<bar> < e \<longrightarrow> y \<in> {..<a}" ..
   1.125 -qed
   1.126 -
   1.127 -lemma open_real_greaterThan [simp]:
   1.128 -  fixes a :: real shows "open {a<..}"
   1.129 -unfolding open_real_def dist_real_def
   1.130 -proof (clarify)
   1.131 -  fix x assume "a < x"
   1.132 -  hence "0 < x - a \<and> (\<forall>y. \<bar>y - x\<bar> < x - a \<longrightarrow> y \<in> {a<..})" by auto
   1.133 -  thus "\<exists>e>0. \<forall>y. \<bar>y - x\<bar> < e \<longrightarrow> y \<in> {a<..}" ..
   1.134 +instance real :: linorder_topology
   1.135 +proof
   1.136 +  show "(open :: real set \<Rightarrow> bool) = generate_topology (range lessThan \<union> range greaterThan)"
   1.137 +  proof (rule ext, safe)
   1.138 +    fix S :: "real set" assume "open S"
   1.139 +    then guess f unfolding open_real_def bchoice_iff ..
   1.140 +    then have *: "S = (\<Union>x\<in>S. {x - f x <..} \<inter> {..< x + f x})"
   1.141 +      by (fastforce simp: dist_real_def)
   1.142 +    show "generate_topology (range lessThan \<union> range greaterThan) S"
   1.143 +      apply (subst *)
   1.144 +      apply (intro generate_topology_Union generate_topology.Int)
   1.145 +      apply (auto intro: generate_topology.Basis)
   1.146 +      done
   1.147 +  next
   1.148 +    fix S :: "real set" assume "generate_topology (range lessThan \<union> range greaterThan) S"
   1.149 +    moreover have "\<And>a::real. open {..<a}"
   1.150 +      unfolding open_real_def dist_real_def
   1.151 +    proof clarify
   1.152 +      fix x a :: real assume "x < a"
   1.153 +      hence "0 < a - x \<and> (\<forall>y. \<bar>y - x\<bar> < a - x \<longrightarrow> y \<in> {..<a})" by auto
   1.154 +      thus "\<exists>e>0. \<forall>y. \<bar>y - x\<bar> < e \<longrightarrow> y \<in> {..<a}" ..
   1.155 +    qed
   1.156 +    moreover have "\<And>a::real. open {a <..}"
   1.157 +      unfolding open_real_def dist_real_def
   1.158 +    proof clarify
   1.159 +      fix x a :: real assume "a < x"
   1.160 +      hence "0 < x - a \<and> (\<forall>y. \<bar>y - x\<bar> < x - a \<longrightarrow> y \<in> {a<..})" by auto
   1.161 +      thus "\<exists>e>0. \<forall>y. \<bar>y - x\<bar> < e \<longrightarrow> y \<in> {a<..}" ..
   1.162 +    qed
   1.163 +    ultimately show "open S"
   1.164 +      by induct auto
   1.165 +  qed
   1.166  qed
   1.167  
   1.168 -lemma open_real_greaterThanLessThan [simp]:
   1.169 -  fixes a b :: real shows "open {a<..<b}"
   1.170 -proof -
   1.171 -  have "{a<..<b} = {a<..} \<inter> {..<b}" by auto
   1.172 -  thus "open {a<..<b}" by (simp add: open_Int)
   1.173 -qed
   1.174 -
   1.175 -lemma closed_real_atMost [simp]: 
   1.176 -  fixes a :: real shows "closed {..a}"
   1.177 -unfolding closed_open by simp
   1.178 -
   1.179 -lemma closed_real_atLeast [simp]:
   1.180 -  fixes a :: real shows "closed {a..}"
   1.181 -unfolding closed_open by simp
   1.182 -
   1.183 -lemma closed_real_atLeastAtMost [simp]:
   1.184 -  fixes a b :: real shows "closed {a..b}"
   1.185 -proof -
   1.186 -  have "{a..b} = {a..} \<inter> {..b}" by auto
   1.187 -  thus "closed {a..b}" by (simp add: closed_Int)
   1.188 -qed
   1.189 -
   1.190 +lemmas open_real_greaterThan = open_greaterThan[where 'a=real]
   1.191 +lemmas open_real_lessThan = open_lessThan[where 'a=real]
   1.192 +lemmas open_real_greaterThanLessThan = open_greaterThanLessThan[where 'a=real]
   1.193 +lemmas closed_real_atMost = closed_atMost[where 'a=real]
   1.194 +lemmas closed_real_atLeast = closed_atLeast[where 'a=real]
   1.195 +lemmas closed_real_atLeastAtMost = closed_atLeastAtMost[where 'a=real]
   1.196  
   1.197  subsection {* Extra type constraints *}
   1.198  
   1.199 @@ -1172,6 +1276,30 @@
   1.200  instance t2_space \<subseteq> t1_space
   1.201  proof qed (fast dest: hausdorff)
   1.202  
   1.203 +lemma (in linorder) less_separate:
   1.204 +  assumes "x < y"
   1.205 +  shows "\<exists>a b. x \<in> {..< a} \<and> y \<in> {b <..} \<and> {..< a} \<inter> {b <..} = {}"
   1.206 +proof cases
   1.207 +  assume "\<exists>z. x < z \<and> z < y"
   1.208 +  then guess z ..
   1.209 +  then have "x \<in> {..< z} \<and> y \<in> {z <..} \<and> {z <..} \<inter> {..< z} = {}"
   1.210 +    by auto
   1.211 +  then show ?thesis by blast
   1.212 +next
   1.213 +  assume "\<not> (\<exists>z. x < z \<and> z < y)"
   1.214 +  with `x < y` have "x \<in> {..< y} \<and> y \<in> {x <..} \<and> {x <..} \<inter> {..< y} = {}"
   1.215 +    by auto
   1.216 +  then show ?thesis by blast
   1.217 +qed
   1.218 +
   1.219 +instance linorder_topology \<subseteq> t2_space
   1.220 +proof
   1.221 +  fix x y :: 'a
   1.222 +  from less_separate[of x y] less_separate[of y x]
   1.223 +  show "x \<noteq> y \<Longrightarrow> \<exists>U V. open U \<and> open V \<and> x \<in> U \<and> y \<in> V \<and> U \<inter> V = {}"
   1.224 +    by (elim neqE) (metis open_lessThan open_greaterThan Int_commute)+
   1.225 +qed
   1.226 +
   1.227  instance metric_space \<subseteq> t2_space
   1.228  proof
   1.229    fix x y :: "'a::metric_space"