introduce order topology
authorhoelzl
Thu Jan 31 11:31:27 2013 +0100 (2013-01-31)
changeset 509993de230ed0547
parent 50998 501200635659
child 51000 c9adb50f74ad
introduce order topology
src/HOL/Limits.thy
src/HOL/RealVector.thy
src/HOL/SEQ.thy
src/HOL/Series.thy
src/HOL/Set_Interval.thy
     1.1 --- a/src/HOL/Limits.thy	Thu Jan 31 11:31:22 2013 +0100
     1.2 +++ b/src/HOL/Limits.thy	Thu Jan 31 11:31:27 2013 +0100
     1.3 @@ -469,6 +469,12 @@
     1.4  apply (erule le_less_trans [OF dist_triangle])
     1.5  done
     1.6  
     1.7 +lemma eventually_nhds_order:
     1.8 +  "eventually P (nhds (a::'a::linorder_topology)) \<longleftrightarrow>
     1.9 +    (\<exists>S. open_interval S \<and> a \<in> S \<and> (\<forall>z\<in>S. P z))"
    1.10 +  (is "_ \<longleftrightarrow> ?rhs")
    1.11 +  unfolding eventually_nhds by (auto dest!: open_orderD dest: open_interval_imp_open)
    1.12 +
    1.13  lemma nhds_neq_bot [simp]: "nhds a \<noteq> bot"
    1.14    unfolding trivial_limit_def eventually_nhds by simp
    1.15  
    1.16 @@ -901,6 +907,36 @@
    1.17      using le_less_trans by (rule eventually_elim2)
    1.18  qed
    1.19  
    1.20 +lemma increasing_tendsto:
    1.21 +  fixes f :: "_ \<Rightarrow> 'a::linorder_topology"
    1.22 +  assumes bdd: "eventually (\<lambda>n. f n \<le> l) F"
    1.23 +      and en: "\<And>x. x < l \<Longrightarrow> eventually (\<lambda>n. x < f n) F"
    1.24 +  shows "(f ---> l) F"
    1.25 +proof (rule topological_tendstoI)
    1.26 +  fix S assume "open S" "l \<in> S"
    1.27 +  then show "eventually (\<lambda>x. f x \<in> S) F"
    1.28 +  proof (induct rule: open_order_induct)
    1.29 +    case (greaterThanLessThan a b) with en bdd show ?case
    1.30 +      by (auto elim!: eventually_elim2)
    1.31 +  qed (insert en bdd, auto elim!: eventually_elim1)
    1.32 +qed
    1.33 +
    1.34 +lemma decreasing_tendsto:
    1.35 +  fixes f :: "_ \<Rightarrow> 'a::linorder_topology"
    1.36 +  assumes bdd: "eventually (\<lambda>n. l \<le> f n) F"
    1.37 +      and en: "\<And>x. l < x \<Longrightarrow> eventually (\<lambda>n. f n < x) F"
    1.38 +  shows "(f ---> l) F"
    1.39 +proof (rule topological_tendstoI)
    1.40 +  fix S assume "open S" "l \<in> S"
    1.41 +  then show "eventually (\<lambda>x. f x \<in> S) F"
    1.42 +  proof (induct rule: open_order_induct)
    1.43 +    case (greaterThanLessThan a b)
    1.44 +    with en have "eventually (\<lambda>n. f n < b) F" by auto
    1.45 +    with bdd show ?case
    1.46 +      by eventually_elim (insert greaterThanLessThan, auto)
    1.47 +  qed (insert en bdd, auto elim!: eventually_elim1)
    1.48 +qed
    1.49 +
    1.50  subsubsection {* Distance and norms *}
    1.51  
    1.52  lemma tendsto_dist [tendsto_intros]:
    1.53 @@ -1002,22 +1038,25 @@
    1.54      by (simp add: tendsto_const)
    1.55  qed
    1.56  
    1.57 -lemma real_tendsto_sandwich:
    1.58 -  fixes f g h :: "'a \<Rightarrow> real"
    1.59 +lemma tendsto_sandwich:
    1.60 +  fixes f g h :: "'a \<Rightarrow> 'b::linorder_topology"
    1.61    assumes ev: "eventually (\<lambda>n. f n \<le> g n) net" "eventually (\<lambda>n. g n \<le> h n) net"
    1.62    assumes lim: "(f ---> c) net" "(h ---> c) net"
    1.63    shows "(g ---> c) net"
    1.64 -proof -
    1.65 -  have "((\<lambda>n. g n - f n) ---> 0) net"
    1.66 -  proof (rule metric_tendsto_imp_tendsto)
    1.67 -    show "eventually (\<lambda>n. dist (g n - f n) 0 \<le> dist (h n - f n) 0) net"
    1.68 -      using ev by (rule eventually_elim2) (simp add: dist_real_def)
    1.69 -    show "((\<lambda>n. h n - f n) ---> 0) net"
    1.70 -      using tendsto_diff[OF lim(2,1)] by simp
    1.71 -  qed
    1.72 -  from tendsto_add[OF this lim(1)] show ?thesis by simp
    1.73 +proof (rule topological_tendstoI)
    1.74 +  fix S assume "open S" "c \<in> S"
    1.75 +  from open_orderD[OF this] obtain T where "open_interval T" "c \<in> T" "T \<subseteq> S" by auto
    1.76 +  with lim[THEN topological_tendstoD, of T]
    1.77 +  have "eventually (\<lambda>x. f x \<in> T) net" "eventually (\<lambda>x. h x \<in> T) net"
    1.78 +    by (auto dest: open_interval_imp_open)
    1.79 +  with ev have "eventually (\<lambda>x. g x \<in> T) net"
    1.80 +    by eventually_elim (insert `open_interval T`, auto dest: open_intervalD)
    1.81 +  with `T \<subseteq> S` show "eventually (\<lambda>x. g x \<in> S) net"
    1.82 +    by (auto elim: eventually_elim1)
    1.83  qed
    1.84  
    1.85 +lemmas real_tendsto_sandwich = tendsto_sandwich[where 'b=real]
    1.86 +
    1.87  subsubsection {* Linear operators and multiplication *}
    1.88  
    1.89  lemma (in bounded_linear) tendsto:
    1.90 @@ -1082,29 +1121,33 @@
    1.91      by (simp add: tendsto_const)
    1.92  qed
    1.93  
    1.94 -lemma tendsto_le_const:
    1.95 -  fixes f :: "_ \<Rightarrow> real" 
    1.96 +lemma tendsto_le:
    1.97 +  fixes f g :: "'a \<Rightarrow> 'b::linorder_topology"
    1.98    assumes F: "\<not> trivial_limit F"
    1.99 -  assumes x: "(f ---> x) F" and a: "eventually (\<lambda>x. a \<le> f x) F"
   1.100 -  shows "a \<le> x"
   1.101 +  assumes x: "(f ---> x) F" and y: "(g ---> y) F"
   1.102 +  assumes ev: "eventually (\<lambda>x. g x \<le> f x) F"
   1.103 +  shows "y \<le> x"
   1.104  proof (rule ccontr)
   1.105 -  assume "\<not> a \<le> x"
   1.106 -  with x have "eventually (\<lambda>x. f x < a) F"
   1.107 -    by (auto simp add: tendsto_def elim!: allE[of _ "{..< a}"])
   1.108 -  with a have "eventually (\<lambda>x. False) F"
   1.109 -    by eventually_elim auto
   1.110 +  assume "\<not> y \<le> x"
   1.111 +  then have "x < y" by simp
   1.112 +  from less_separate[OF this] obtain a b where xy: "x \<in> {..<a}" "y \<in> {b <..}" "{..<a} \<inter> {b<..} = {}"
   1.113 +    by auto
   1.114 +  then have less: "\<And>x y. x < a \<Longrightarrow> b < y \<Longrightarrow> x < y"
   1.115 +    by auto
   1.116 +  from x[THEN topological_tendstoD, of "{..<a}"] y[THEN topological_tendstoD, of "{b <..}"] xy
   1.117 +  have "eventually (\<lambda>x. f x \<in> {..<a}) F" "eventually (\<lambda>x. g x \<in> {b <..}) F" by auto
   1.118 +  with ev have "eventually (\<lambda>x. False) F"
   1.119 +    by eventually_elim (auto dest!: less)
   1.120    with F show False
   1.121      by (simp add: eventually_False)
   1.122  qed
   1.123  
   1.124 -lemma tendsto_le:
   1.125 -  fixes f g :: "_ \<Rightarrow> real" 
   1.126 +lemma tendsto_le_const:
   1.127 +  fixes f :: "'a \<Rightarrow> 'b::linorder_topology"
   1.128    assumes F: "\<not> trivial_limit F"
   1.129 -  assumes x: "(f ---> x) F" and y: "(g ---> y) F"
   1.130 -  assumes ev: "eventually (\<lambda>x. g x \<le> f x) F"
   1.131 -  shows "y \<le> x"
   1.132 -  using tendsto_le_const[OF F tendsto_diff[OF x y], of 0] ev
   1.133 -  by (simp add: sign_simps)
   1.134 +  assumes x: "(f ---> x) F" and a: "eventually (\<lambda>x. a \<le> f x) F"
   1.135 +  shows "a \<le> x"
   1.136 +  using F x tendsto_const a by (rule tendsto_le)
   1.137  
   1.138  subsubsection {* Inverse and division *}
   1.139  
     2.1 --- a/src/HOL/RealVector.thy	Thu Jan 31 11:31:22 2013 +0100
     2.2 +++ b/src/HOL/RealVector.thy	Thu Jan 31 11:31:27 2013 +0100
     2.3 @@ -508,6 +508,110 @@
     2.4  
     2.5  end
     2.6  
     2.7 +inductive generate_topology for S where
     2.8 +  UNIV: "generate_topology S UNIV"
     2.9 +| Int: "generate_topology S a \<Longrightarrow> generate_topology S b \<Longrightarrow> generate_topology S (a \<inter> b)"
    2.10 +| UN: "(\<And>k. k \<in> K \<Longrightarrow> generate_topology S k) \<Longrightarrow> generate_topology S (\<Union>K)"
    2.11 +| Basis: "s \<in> S \<Longrightarrow> generate_topology S s"
    2.12 +
    2.13 +hide_fact (open) UNIV Int UN Basis 
    2.14 +
    2.15 +lemma generate_topology_Union: 
    2.16 +  "(\<And>k. k \<in> I \<Longrightarrow> generate_topology S (K k)) \<Longrightarrow> generate_topology S (\<Union>k\<in>I. K k)"
    2.17 +  unfolding SUP_def by (intro generate_topology.UN) auto
    2.18 +
    2.19 +lemma topological_space_generate_topology:
    2.20 +  "class.topological_space (generate_topology S)"
    2.21 +  by default (auto intro: generate_topology.intros)
    2.22 +
    2.23 +class order_topology = order + "open" +
    2.24 +  assumes open_generated_order: "open = generate_topology (range (\<lambda>a. {..< a}) \<union> range (\<lambda>a. {a <..}))"
    2.25 +begin
    2.26 +
    2.27 +subclass topological_space
    2.28 +  unfolding open_generated_order
    2.29 +  by (rule topological_space_generate_topology)
    2.30 +
    2.31 +lemma open_greaterThan [simp]: "open {a <..}"
    2.32 +  unfolding open_generated_order by (auto intro: generate_topology.Basis)
    2.33 +
    2.34 +lemma open_lessThan [simp]: "open {..< a}"
    2.35 +  unfolding open_generated_order by (auto intro: generate_topology.Basis)
    2.36 +
    2.37 +lemma open_greaterThanLessThan [simp]: "open {a <..< b}"
    2.38 +   unfolding greaterThanLessThan_eq by (simp add: open_Int)
    2.39 +
    2.40 +end
    2.41 +
    2.42 +class linorder_topology = linorder + order_topology
    2.43 +
    2.44 +lemma closed_atMost [simp]: "closed {.. a::'a::linorder_topology}"
    2.45 +  by (simp add: closed_open)
    2.46 +
    2.47 +lemma closed_atLeast [simp]: "closed {a::'a::linorder_topology ..}"
    2.48 +  by (simp add: closed_open)
    2.49 +
    2.50 +lemma closed_atLeastAtMost [simp]: "closed {a::'a::linorder_topology .. b}"
    2.51 +proof -
    2.52 +  have "{a .. b} = {a ..} \<inter> {.. b}"
    2.53 +    by auto
    2.54 +  then show ?thesis
    2.55 +    by (simp add: closed_Int)
    2.56 +qed
    2.57 +
    2.58 +inductive open_interval :: "'a::order set \<Rightarrow> bool" where
    2.59 +  empty[intro]: "open_interval {}" |
    2.60 +  UNIV[intro]: "open_interval UNIV" |
    2.61 +  greaterThan[intro]: "open_interval {a <..}" |
    2.62 +  lessThan[intro]: "open_interval {..< b}" |
    2.63 +  greaterThanLessThan[intro]: "open_interval {a <..< b}"
    2.64 +hide_fact (open) empty UNIV greaterThan lessThan greaterThanLessThan
    2.65 +
    2.66 +lemma open_intervalD:
    2.67 +  "open_interval S \<Longrightarrow> x \<in> S \<Longrightarrow> y \<in> S \<Longrightarrow> x \<le> z \<Longrightarrow> z \<le> y \<Longrightarrow> z \<in> S"
    2.68 +  by (cases rule: open_interval.cases) auto
    2.69 +
    2.70 +lemma open_interval_Int[intro]:
    2.71 +  fixes S T :: "'a :: linorder set"
    2.72 +  assumes S: "open_interval S" and T: "open_interval T"
    2.73 +  shows "open_interval (S \<inter> T)"
    2.74 +proof -
    2.75 +  { fix a b :: 'a have "{..<b} \<inter> {a<..} = { a <..} \<inter> {..< b }" by auto } note this[simp]
    2.76 +  { fix a b :: 'a and A have "{a <..} \<inter> ({b <..} \<inter> A) = {max a b <..} \<inter> A" by auto } note this[simp]
    2.77 +  { fix a b :: 'a and A have "{..<b} \<inter> (A \<inter> {..<a}) = A \<inter> {..<min a b}" by auto } note this[simp]
    2.78 +  { fix a b :: 'a have "open_interval ({ a <..} \<inter> {..< b})"
    2.79 +      unfolding greaterThanLessThan_eq[symmetric] by auto } note this[simp]
    2.80 +  show ?thesis
    2.81 +    by (cases rule: open_interval.cases[OF S, case_product open_interval.cases[OF T]])
    2.82 +       (auto simp: greaterThanLessThan_eq lessThan_Int_lessThan greaterThan_Int_greaterThan Int_assoc)
    2.83 +qed
    2.84 +
    2.85 +lemma open_interval_imp_open: "open_interval S \<Longrightarrow> open (S::'a::order_topology set)"
    2.86 +  by (cases S rule: open_interval.cases) auto
    2.87 +
    2.88 +lemma open_orderD:
    2.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"
    2.90 +  unfolding open_generated_order
    2.91 +proof (induct rule: generate_topology.induct)
    2.92 +  case (UN K) then obtain k where "k \<in> K" "x \<in> k" by auto
    2.93 +  with UN(2)[of k] show ?case by auto
    2.94 +qed auto
    2.95 +
    2.96 +lemma open_order_induct[consumes 2, case_names subset UNIV lessThan greaterThan greaterThanLessThan]:
    2.97 +  fixes S :: "'a::linorder_topology set"
    2.98 +  assumes S: "open S" "x \<in> S"
    2.99 +  assumes subset: "\<And>S T. P S \<Longrightarrow> S \<subseteq> T \<Longrightarrow> P T"
   2.100 +  assumes univ: "P UNIV"
   2.101 +  assumes lt: "\<And>a. x < a \<Longrightarrow> P {..< a}"
   2.102 +  assumes gt: "\<And>a. a < x \<Longrightarrow> P {a <..}"
   2.103 +  assumes lgt: "\<And>a b. a < x \<Longrightarrow> x < b \<Longrightarrow> P {a <..< b}"
   2.104 +  shows "P S"
   2.105 +proof -
   2.106 +  from open_orderD[OF S] obtain T where "open_interval T" "T \<subseteq> S" "x \<in> T"
   2.107 +    by auto
   2.108 +  then show "P S"
   2.109 +    by induct (auto intro: univ subset lt gt lgt)
   2.110 +qed
   2.111  
   2.112  subsection {* Metric spaces *}
   2.113  
   2.114 @@ -859,46 +963,46 @@
   2.115  
   2.116  end
   2.117  
   2.118 -lemma open_real_lessThan [simp]:
   2.119 -  fixes a :: real shows "open {..<a}"
   2.120 -unfolding open_real_def dist_real_def
   2.121 -proof (clarify)
   2.122 -  fix x assume "x < a"
   2.123 -  hence "0 < a - x \<and> (\<forall>y. \<bar>y - x\<bar> < a - x \<longrightarrow> y \<in> {..<a})" by auto
   2.124 -  thus "\<exists>e>0. \<forall>y. \<bar>y - x\<bar> < e \<longrightarrow> y \<in> {..<a}" ..
   2.125 -qed
   2.126 -
   2.127 -lemma open_real_greaterThan [simp]:
   2.128 -  fixes a :: real shows "open {a<..}"
   2.129 -unfolding open_real_def dist_real_def
   2.130 -proof (clarify)
   2.131 -  fix x assume "a < x"
   2.132 -  hence "0 < x - a \<and> (\<forall>y. \<bar>y - x\<bar> < x - a \<longrightarrow> y \<in> {a<..})" by auto
   2.133 -  thus "\<exists>e>0. \<forall>y. \<bar>y - x\<bar> < e \<longrightarrow> y \<in> {a<..}" ..
   2.134 +instance real :: linorder_topology
   2.135 +proof
   2.136 +  show "(open :: real set \<Rightarrow> bool) = generate_topology (range lessThan \<union> range greaterThan)"
   2.137 +  proof (rule ext, safe)
   2.138 +    fix S :: "real set" assume "open S"
   2.139 +    then guess f unfolding open_real_def bchoice_iff ..
   2.140 +    then have *: "S = (\<Union>x\<in>S. {x - f x <..} \<inter> {..< x + f x})"
   2.141 +      by (fastforce simp: dist_real_def)
   2.142 +    show "generate_topology (range lessThan \<union> range greaterThan) S"
   2.143 +      apply (subst *)
   2.144 +      apply (intro generate_topology_Union generate_topology.Int)
   2.145 +      apply (auto intro: generate_topology.Basis)
   2.146 +      done
   2.147 +  next
   2.148 +    fix S :: "real set" assume "generate_topology (range lessThan \<union> range greaterThan) S"
   2.149 +    moreover have "\<And>a::real. open {..<a}"
   2.150 +      unfolding open_real_def dist_real_def
   2.151 +    proof clarify
   2.152 +      fix x a :: real assume "x < a"
   2.153 +      hence "0 < a - x \<and> (\<forall>y. \<bar>y - x\<bar> < a - x \<longrightarrow> y \<in> {..<a})" by auto
   2.154 +      thus "\<exists>e>0. \<forall>y. \<bar>y - x\<bar> < e \<longrightarrow> y \<in> {..<a}" ..
   2.155 +    qed
   2.156 +    moreover have "\<And>a::real. open {a <..}"
   2.157 +      unfolding open_real_def dist_real_def
   2.158 +    proof clarify
   2.159 +      fix x a :: real assume "a < x"
   2.160 +      hence "0 < x - a \<and> (\<forall>y. \<bar>y - x\<bar> < x - a \<longrightarrow> y \<in> {a<..})" by auto
   2.161 +      thus "\<exists>e>0. \<forall>y. \<bar>y - x\<bar> < e \<longrightarrow> y \<in> {a<..}" ..
   2.162 +    qed
   2.163 +    ultimately show "open S"
   2.164 +      by induct auto
   2.165 +  qed
   2.166  qed
   2.167  
   2.168 -lemma open_real_greaterThanLessThan [simp]:
   2.169 -  fixes a b :: real shows "open {a<..<b}"
   2.170 -proof -
   2.171 -  have "{a<..<b} = {a<..} \<inter> {..<b}" by auto
   2.172 -  thus "open {a<..<b}" by (simp add: open_Int)
   2.173 -qed
   2.174 -
   2.175 -lemma closed_real_atMost [simp]: 
   2.176 -  fixes a :: real shows "closed {..a}"
   2.177 -unfolding closed_open by simp
   2.178 -
   2.179 -lemma closed_real_atLeast [simp]:
   2.180 -  fixes a :: real shows "closed {a..}"
   2.181 -unfolding closed_open by simp
   2.182 -
   2.183 -lemma closed_real_atLeastAtMost [simp]:
   2.184 -  fixes a b :: real shows "closed {a..b}"
   2.185 -proof -
   2.186 -  have "{a..b} = {a..} \<inter> {..b}" by auto
   2.187 -  thus "closed {a..b}" by (simp add: closed_Int)
   2.188 -qed
   2.189 -
   2.190 +lemmas open_real_greaterThan = open_greaterThan[where 'a=real]
   2.191 +lemmas open_real_lessThan = open_lessThan[where 'a=real]
   2.192 +lemmas open_real_greaterThanLessThan = open_greaterThanLessThan[where 'a=real]
   2.193 +lemmas closed_real_atMost = closed_atMost[where 'a=real]
   2.194 +lemmas closed_real_atLeast = closed_atLeast[where 'a=real]
   2.195 +lemmas closed_real_atLeastAtMost = closed_atLeastAtMost[where 'a=real]
   2.196  
   2.197  subsection {* Extra type constraints *}
   2.198  
   2.199 @@ -1172,6 +1276,30 @@
   2.200  instance t2_space \<subseteq> t1_space
   2.201  proof qed (fast dest: hausdorff)
   2.202  
   2.203 +lemma (in linorder) less_separate:
   2.204 +  assumes "x < y"
   2.205 +  shows "\<exists>a b. x \<in> {..< a} \<and> y \<in> {b <..} \<and> {..< a} \<inter> {b <..} = {}"
   2.206 +proof cases
   2.207 +  assume "\<exists>z. x < z \<and> z < y"
   2.208 +  then guess z ..
   2.209 +  then have "x \<in> {..< z} \<and> y \<in> {z <..} \<and> {z <..} \<inter> {..< z} = {}"
   2.210 +    by auto
   2.211 +  then show ?thesis by blast
   2.212 +next
   2.213 +  assume "\<not> (\<exists>z. x < z \<and> z < y)"
   2.214 +  with `x < y` have "x \<in> {..< y} \<and> y \<in> {x <..} \<and> {x <..} \<inter> {..< y} = {}"
   2.215 +    by auto
   2.216 +  then show ?thesis by blast
   2.217 +qed
   2.218 +
   2.219 +instance linorder_topology \<subseteq> t2_space
   2.220 +proof
   2.221 +  fix x y :: 'a
   2.222 +  from less_separate[of x y] less_separate[of y x]
   2.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 = {}"
   2.224 +    by (elim neqE) (metis open_lessThan open_greaterThan Int_commute)+
   2.225 +qed
   2.226 +
   2.227  instance metric_space \<subseteq> t2_space
   2.228  proof
   2.229    fix x y :: "'a::metric_space"
     3.1 --- a/src/HOL/SEQ.thy	Thu Jan 31 11:31:22 2013 +0100
     3.2 +++ b/src/HOL/SEQ.thy	Thu Jan 31 11:31:27 2013 +0100
     3.3 @@ -368,19 +368,16 @@
     3.4        and bdd: "\<And>n. f n \<le> l"
     3.5        and en: "\<And>e. 0 < e \<Longrightarrow> \<exists>n. l \<le> f n + e"
     3.6    shows "f ----> l"
     3.7 -  unfolding LIMSEQ_def
     3.8 -proof safe
     3.9 -  fix r :: real assume "0 < r"
    3.10 -  with bdd en[of "r / 2"] obtain n where n: "dist (f n) l \<le> r / 2"
    3.11 -    by (auto simp add: field_simps dist_real_def)
    3.12 -  { fix N assume "n \<le> N"
    3.13 -    then have "dist (f N) l \<le> dist (f n) l"
    3.14 -      using incseq_SucI[of f] inc bdd by (auto dest!: incseqD simp: dist_real_def)
    3.15 -    then have "dist (f N) l < r"
    3.16 -      using `0 < r` n by simp }
    3.17 -  with `0 < r` show "\<exists>no. \<forall>n\<ge>no. dist (f n) l < r"
    3.18 -    by (auto simp add: LIMSEQ_def field_simps intro!: exI[of _ n])
    3.19 -qed
    3.20 +proof (rule increasing_tendsto)
    3.21 +  fix x assume "x < l"
    3.22 +  with dense[of 0 "l - x"] obtain e where "0 < e" "e < l - x"
    3.23 +    by auto
    3.24 +  from en[OF `0 < e`] obtain n where "l - e \<le> f n"
    3.25 +    by (auto simp: field_simps)
    3.26 +  with `e < l - x` `0 < e` have "x < f n" by simp
    3.27 +  with incseq_SucI[of f, OF inc] show "eventually (\<lambda>n. x < f n) sequentially"
    3.28 +    by (auto simp: eventually_sequentially incseq_def intro: less_le_trans)
    3.29 +qed (insert bdd, auto)
    3.30  
    3.31  lemma Bseq_inverse_lemma:
    3.32    fixes x :: "'a::real_normed_div_algebra"
    3.33 @@ -437,15 +434,15 @@
    3.34    by auto
    3.35  
    3.36  lemma LIMSEQ_le_const:
    3.37 -  "\<lbrakk>X ----> (x::real); \<exists>N. \<forall>n\<ge>N. a \<le> X n\<rbrakk> \<Longrightarrow> a \<le> x"
    3.38 +  "\<lbrakk>X ----> (x::'a::linorder_topology); \<exists>N. \<forall>n\<ge>N. a \<le> X n\<rbrakk> \<Longrightarrow> a \<le> x"
    3.39    using tendsto_le_const[of sequentially X x a] by (simp add: eventually_sequentially)
    3.40  
    3.41  lemma LIMSEQ_le:
    3.42 -  "\<lbrakk>X ----> x; Y ----> y; \<exists>N. \<forall>n\<ge>N. X n \<le> Y n\<rbrakk> \<Longrightarrow> x \<le> (y::real)"
    3.43 +  "\<lbrakk>X ----> x; Y ----> y; \<exists>N. \<forall>n\<ge>N. X n \<le> Y n\<rbrakk> \<Longrightarrow> x \<le> (y::'a::linorder_topology)"
    3.44    using tendsto_le[of sequentially Y y X x] by (simp add: eventually_sequentially)
    3.45  
    3.46  lemma LIMSEQ_le_const2:
    3.47 -  "\<lbrakk>X ----> (x::real); \<exists>N. \<forall>n\<ge>N. X n \<le> a\<rbrakk> \<Longrightarrow> x \<le> a"
    3.48 +  "\<lbrakk>X ----> (x::'a::linorder_topology); \<exists>N. \<forall>n\<ge>N. X n \<le> a\<rbrakk> \<Longrightarrow> x \<le> a"
    3.49    by (rule LIMSEQ_le[of X x "\<lambda>n. a"]) (auto simp: tendsto_const)
    3.50  
    3.51  subsection {* Convergence *}
     4.1 --- a/src/HOL/Series.thy	Thu Jan 31 11:31:22 2013 +0100
     4.2 +++ b/src/HOL/Series.thy	Thu Jan 31 11:31:27 2013 +0100
     4.3 @@ -367,7 +367,7 @@
     4.4  
     4.5  lemma pos_summable:
     4.6    fixes f:: "nat \<Rightarrow> real"
     4.7 -  assumes pos: "!!n. 0 \<le> f n" and le: "!!n. setsum f {0..<n} \<le> x"
     4.8 +  assumes pos: "\<And>n. 0 \<le> f n" and le: "\<And>n. setsum f {0..<n} \<le> x"
     4.9    shows "summable f"
    4.10  proof -
    4.11    have "convergent (\<lambda>n. setsum f {0..<n})"
    4.12 @@ -386,35 +386,65 @@
    4.13  qed
    4.14  
    4.15  lemma series_pos_le:
    4.16 -  fixes f :: "nat \<Rightarrow> real"
    4.17 +  fixes f :: "nat \<Rightarrow> 'a::{ordered_comm_monoid_add, linorder_topology}"
    4.18    shows "\<lbrakk>summable f; \<forall>m\<ge>n. 0 \<le> f m\<rbrakk> \<Longrightarrow> setsum f {0..<n} \<le> suminf f"
    4.19 -apply (drule summable_sums)
    4.20 -apply (simp add: sums_def)
    4.21 -apply (cut_tac k = "setsum f {0..<n}" in tendsto_const)
    4.22 -apply (erule LIMSEQ_le, blast)
    4.23 -apply (rule_tac x="n" in exI, clarify)
    4.24 -apply (rule setsum_mono2)
    4.25 -apply auto
    4.26 -done
    4.27 +  apply (drule summable_sums)
    4.28 +  apply (simp add: sums_def)
    4.29 +  apply (rule LIMSEQ_le_const)
    4.30 +  apply assumption
    4.31 +  apply (intro exI[of _ n])
    4.32 +  apply (auto intro!: setsum_mono2)
    4.33 +  done
    4.34  
    4.35  lemma series_pos_less:
    4.36 -  fixes f :: "nat \<Rightarrow> real"
    4.37 +  fixes f :: "nat \<Rightarrow> 'a::{ordered_ab_semigroup_add_imp_le, ordered_comm_monoid_add, linorder_topology}"
    4.38    shows "\<lbrakk>summable f; \<forall>m\<ge>n. 0 < f m\<rbrakk> \<Longrightarrow> setsum f {0..<n} < suminf f"
    4.39 -apply (rule_tac y="setsum f {0..<Suc n}" in order_less_le_trans)
    4.40 -apply simp
    4.41 -apply (erule series_pos_le)
    4.42 -apply (simp add: order_less_imp_le)
    4.43 -done
    4.44 +  apply (rule_tac y="setsum f {0..<Suc n}" in order_less_le_trans)
    4.45 +  using add_less_cancel_left [of "setsum f {0..<n}" 0 "f n"]
    4.46 +  apply simp
    4.47 +  apply (erule series_pos_le)
    4.48 +  apply (simp add: order_less_imp_le)
    4.49 +  done
    4.50 +
    4.51 +lemma suminf_eq_zero_iff:
    4.52 +  fixes f :: "nat \<Rightarrow> 'a::{ordered_comm_monoid_add, linorder_topology}"
    4.53 +  shows "\<lbrakk>summable f; \<forall>n. 0 \<le> f n\<rbrakk> \<Longrightarrow> suminf f = 0 \<longleftrightarrow> (\<forall>n. f n = 0)"
    4.54 +proof
    4.55 +  assume "summable f" "suminf f = 0" and pos: "\<forall>n. 0 \<le> f n"
    4.56 +  then have "f sums 0"
    4.57 +    by (simp add: sums_iff)
    4.58 +  then have f: "(\<lambda>n. \<Sum>i<n. f i) ----> 0"
    4.59 +    by (simp add: sums_def atLeast0LessThan)
    4.60 +  have "\<And>i. (\<Sum>n\<in>{i}. f n) \<le> 0"
    4.61 +  proof (rule LIMSEQ_le_const[OF f])
    4.62 +    fix i show "\<exists>N. \<forall>n\<ge>N. (\<Sum>n\<in>{i}. f n) \<le> setsum f {..<n}"
    4.63 +      using pos by (intro exI[of _ "Suc i"] allI impI setsum_mono2) auto
    4.64 +  qed
    4.65 +  with pos show "\<forall>n. f n = 0"
    4.66 +    by (auto intro!: antisym)
    4.67 +next
    4.68 +  assume "\<forall>n. f n = 0"
    4.69 +  then have "f = (\<lambda>n. 0)"
    4.70 +    by auto
    4.71 +  then show "suminf f = 0"
    4.72 +    by simp
    4.73 +qed
    4.74 +
    4.75 +lemma suminf_gt_zero_iff:
    4.76 +  fixes f :: "nat \<Rightarrow> 'a::{ordered_comm_monoid_add, linorder_topology}"
    4.77 +  shows "\<lbrakk>summable f; \<forall>n. 0 \<le> f n\<rbrakk> \<Longrightarrow> 0 < suminf f \<longleftrightarrow> (\<exists>i. 0 < f i)"
    4.78 +  using series_pos_le[of f 0] suminf_eq_zero_iff[of f]
    4.79 +  by (simp add: less_le)
    4.80  
    4.81  lemma suminf_gt_zero:
    4.82 -  fixes f :: "nat \<Rightarrow> real"
    4.83 +  fixes f :: "nat \<Rightarrow> 'a::{ordered_comm_monoid_add, linorder_topology}"
    4.84    shows "\<lbrakk>summable f; \<forall>n. 0 < f n\<rbrakk> \<Longrightarrow> 0 < suminf f"
    4.85 -by (drule_tac n="0" in series_pos_less, simp_all)
    4.86 +  using suminf_gt_zero_iff[of f] by (simp add: less_imp_le)
    4.87  
    4.88  lemma suminf_ge_zero:
    4.89 -  fixes f :: "nat \<Rightarrow> real"
    4.90 +  fixes f :: "nat \<Rightarrow> 'a::{ordered_comm_monoid_add, linorder_topology}"
    4.91    shows "\<lbrakk>summable f; \<forall>n. 0 \<le> f n\<rbrakk> \<Longrightarrow> 0 \<le> suminf f"
    4.92 -by (drule_tac n="0" in series_pos_le, simp_all)
    4.93 +  by (drule_tac n="0" in series_pos_le, simp_all)
    4.94  
    4.95  lemma sumr_pos_lt_pair:
    4.96    fixes f :: "nat \<Rightarrow> real"
    4.97 @@ -493,9 +523,14 @@
    4.98  done
    4.99  
   4.100  lemma suminf_le:
   4.101 -  fixes x :: real
   4.102 +  fixes x :: "'a :: {ordered_comm_monoid_add, linorder_topology}"
   4.103    shows "summable f \<Longrightarrow> (!!n. setsum f {0..<n} \<le> x) \<Longrightarrow> suminf f \<le> x"
   4.104 -  by (simp add: summable_convergent_sumr_iff suminf_eq_lim lim_le)
   4.105 +  apply (drule summable_sums)
   4.106 +  apply (simp add: sums_def)
   4.107 +  apply (rule LIMSEQ_le_const2)
   4.108 +  apply assumption
   4.109 +  apply auto
   4.110 +  done
   4.111  
   4.112  lemma summable_Cauchy:
   4.113       "summable (f::nat \<Rightarrow> 'a::banach) =
   4.114 @@ -575,7 +610,7 @@
   4.115  text{*Limit comparison property for series (c.f. jrh)*}
   4.116  
   4.117  lemma summable_le:
   4.118 -  fixes f g :: "nat \<Rightarrow> real"
   4.119 +  fixes f g :: "nat \<Rightarrow> 'a::{ordered_comm_monoid_add, linorder_topology}"
   4.120    shows "\<lbrakk>\<forall>n. f n \<le> g n; summable f; summable g\<rbrakk> \<Longrightarrow> suminf f \<le> suminf g"
   4.121  apply (drule summable_sums)+
   4.122  apply (simp only: sums_def, erule (1) LIMSEQ_le)
   4.123 @@ -597,15 +632,7 @@
   4.124    fixes f::"nat\<Rightarrow>real"
   4.125    assumes gt0: "\<forall>n. 0 \<le> f n" and sm: "summable f"
   4.126    shows "0 \<le> suminf f"
   4.127 -proof -
   4.128 -  let ?g = "(\<lambda>n. (0::real))"
   4.129 -  from gt0 have "\<forall>n. ?g n \<le> f n" by simp
   4.130 -  moreover have "summable ?g" by (rule summable_zero)
   4.131 -  moreover from sm have "summable f" .
   4.132 -  ultimately have "suminf ?g \<le> suminf f" by (rule summable_le)
   4.133 -  then show "0 \<le> suminf f" by simp
   4.134 -qed
   4.135 -
   4.136 +  using suminf_ge_zero[OF sm gt0] by simp
   4.137  
   4.138  text{*Absolute convergence imples normal convergence*}
   4.139  lemma summable_norm_cancel:
     5.1 --- a/src/HOL/Set_Interval.thy	Thu Jan 31 11:31:22 2013 +0100
     5.2 +++ b/src/HOL/Set_Interval.thy	Thu Jan 31 11:31:27 2013 +0100
     5.3 @@ -117,6 +117,11 @@
     5.4  lemma atMost_Int_atLeast: "!!n:: 'a::order. atMost n Int atLeast n = {n}"
     5.5  by (blast intro: order_antisym)
     5.6  
     5.7 +lemma (in linorder) lessThan_Int_lessThan: "{ a <..} \<inter> { b <..} = { max a b <..}"
     5.8 +  by auto
     5.9 +
    5.10 +lemma (in linorder) greaterThan_Int_greaterThan: "{..< a} \<inter> {..< b} = {..< min a b}"
    5.11 +  by auto
    5.12  
    5.13  subsection {* Logical Equivalences for Set Inclusion and Equality *}
    5.14  
    5.15 @@ -190,6 +195,9 @@
    5.16  breaks many proofs. Since it only helps blast, it is better to leave well
    5.17  alone *}
    5.18  
    5.19 +lemma greaterThanLessThan_eq: "{ a <..< b} = { a <..} \<inter> {..< b }"
    5.20 +  by auto
    5.21 +
    5.22  end
    5.23  
    5.24  subsubsection{* Emptyness, singletons, subset *}