# HG changeset patch
# User hoelzl
# Date 1454996371 -3600
# Node ID acfc4ad7b76a87c510e1d68729cdc746f5f5fb46
# Parent  106569399cd60cfa1f4f8ecd54f0d3f63884d197
instantiate topologies for nat, int and enat

diff -r 106569399cd6 -r acfc4ad7b76a src/HOL/Filter.thy
--- a/src/HOL/Filter.thy	Mon Feb 08 19:53:49 2016 +0100
+++ b/src/HOL/Filter.thy	Tue Feb 09 06:39:31 2016 +0100
@@ -479,6 +479,9 @@
     eventually P (INF b:B. F b) \<longleftrightarrow> (\<exists>b\<in>B. eventually P (F b))"
   by (subst eventually_Inf_base) auto
 
+lemma eventually_INF1: "i \<in> I \<Longrightarrow> eventually P (F i) \<Longrightarrow> eventually P (INF i:I. F i)"
+  using filter_leD[OF INF_lower] .
+
 lemma eventually_INF_mono:
   assumes *: "\<forall>\<^sub>F x in \<Sqinter>i\<in>I. F i. P x"
   assumes T1: "\<And>Q R P. (\<And>x. Q x \<and> R x \<longrightarrow> P x) \<Longrightarrow> (\<And>x. T Q x \<Longrightarrow> T R x \<Longrightarrow> T P x)"
@@ -966,6 +969,16 @@
   by (simp add: le_filter_def eventually_filtermap eventually_prod_filter)
      (auto elim: eventually_elim2)
 
+lemma eventually_prodI: "eventually P F \<Longrightarrow> eventually Q G \<Longrightarrow> eventually (\<lambda>x. P (fst x) \<and> Q (snd x)) (F \<times>\<^sub>F G)"
+  unfolding prod_filter_def
+  by (intro eventually_INF1[of "(P, Q)"]) (auto simp: eventually_principal)
+
+lemma prod_filter_INF1: "I \<noteq> {} \<Longrightarrow> (INF i:I. A i) \<times>\<^sub>F B = (INF i:I. A i \<times>\<^sub>F B)"
+  using prod_filter_INF[of I "{B}" A "\<lambda>x. x"] by simp
+
+lemma prod_filter_INF2: "J \<noteq> {} \<Longrightarrow> A \<times>\<^sub>F (INF i:J. B i) = (INF i:J. A \<times>\<^sub>F B i)"
+  using prod_filter_INF[of "{A}" J "\<lambda>x. x" B] by simp
+
 subsection \<open>Limits\<close>
 
 definition filterlim :: "('a \<Rightarrow> 'b) \<Rightarrow> 'b filter \<Rightarrow> 'a filter \<Rightarrow> bool" where
diff -r 106569399cd6 -r acfc4ad7b76a src/HOL/Library/Extended_Real.thy
--- a/src/HOL/Library/Extended_Real.thy	Mon Feb 08 19:53:49 2016 +0100
+++ b/src/HOL/Library/Extended_Real.thy	Tue Feb 09 06:39:31 2016 +0100
@@ -169,6 +169,36 @@
   qed auto
 qed
 
+lemma nhds_enat: "nhds x = (if x = \<infinity> then INF i. principal {enat i..} else principal {x})"
+proof auto
+  show "nhds \<infinity> = (INF i. principal {enat i..})"
+    unfolding nhds_def
+    apply (auto intro!: antisym INF_greatest simp add: open_enat_iff cong: rev_conj_cong)
+    apply (auto intro!: INF_lower Ioi_le_Ico) []
+    subgoal for x i
+      by (auto intro!: INF_lower2[of "Suc i"] simp: subset_eq Ball_def eSuc_enat Suc_ile_eq)
+    done
+  show "nhds (enat i) = principal {enat i}" for i
+    by (simp add: nhds_discrete_open open_enat)
+qed
+
+instance enat :: topological_comm_monoid_add
+proof
+  have [simp]: "enat i \<le> aa \<Longrightarrow> enat i \<le> aa + ba" for aa ba i
+    by (rule order_trans[OF _ add_mono[of aa aa 0 ba]]) auto
+  then have [simp]: "enat i \<le> ba \<Longrightarrow> enat i \<le> aa + ba" for aa ba i
+    by (metis add.commute)
+  fix a b :: enat show "((\<lambda>x. fst x + snd x) \<longlongrightarrow> a + b) (nhds a \<times>\<^sub>F nhds b)"
+    apply (auto simp: nhds_enat filterlim_INF prod_filter_INF1 prod_filter_INF2
+                      filterlim_principal principal_prod_principal eventually_principal)
+    subgoal for i
+      by (auto intro!: eventually_INF1[of i] simp: eventually_principal)
+    subgoal for j i
+      by (auto intro!: eventually_INF1[of i] simp: eventually_principal)
+    subgoal for j i
+      by (auto intro!: eventually_INF1[of i] simp: eventually_principal)
+    done
+qed
 
 text \<open>
 
@@ -1637,7 +1667,7 @@
   "a \<noteq> 0 \<Longrightarrow> b \<noteq> 0 \<Longrightarrow> inverse (a * (b::ereal)) = inverse a * inverse b"
   by (cases a; cases b) auto
 
-     
+
 subsection "Complete lattice"
 
 instantiation ereal :: lattice
@@ -2584,7 +2614,7 @@
     by eventually_elim (auto simp: ereal_real)
   hence "eventually (\<lambda>x. abs (real_of_ereal (f x)) < e) F" if "e > 0" for e using assms[OF that]
     by eventually_elim (simp add: real_less_ereal_iff that)
-  hence "((\<lambda>x. real_of_ereal (f x)) \<longlongrightarrow> 0) F" unfolding tendsto_iff 
+  hence "((\<lambda>x. real_of_ereal (f x)) \<longlongrightarrow> 0) F" unfolding tendsto_iff
     by (auto simp: tendsto_iff dist_real_def)
   thus "((\<lambda>x. ereal (real_of_ereal (f x))) \<longlongrightarrow> 0) F" by (simp add: zero_ereal_def)
 qed
@@ -3751,7 +3781,7 @@
   thus "x \<in> uminus ` {..a}" by simp
 qed auto
 
-lemma continuous_on_inverse_ereal [continuous_intros]: 
+lemma continuous_on_inverse_ereal [continuous_intros]:
   "continuous_on {0::ereal ..} inverse"
   unfolding continuous_on_def
 proof clarsimp
@@ -3763,9 +3793,9 @@
   ultimately show "(inverse \<longlongrightarrow> inverse x) (at x within {0..})"
     by (auto simp: le_less inverse_ereal_tendsto_at_right_0 inverse_ereal_tendsto_pos)
 qed
-  
+
 lemma continuous_inverse_ereal_nonpos: "continuous_on ({..<0} :: ereal set) inverse"
-proof (subst continuous_on_cong[OF refl]) 
+proof (subst continuous_on_cong[OF refl])
   have "continuous_on {(0::ereal)<..} inverse"
     by (rule continuous_on_subset[OF continuous_on_inverse_ereal]) auto
   thus "continuous_on {..<(0::ereal)} (uminus \<circ> inverse \<circ> uminus)"
@@ -3776,14 +3806,14 @@
   assumes "(f \<longlongrightarrow> (c :: ereal)) F"
   assumes "eventually (\<lambda>x. f x \<ge> 0) F"
   shows   "((\<lambda>x. inverse (f x)) \<longlongrightarrow> inverse c) F"
-  by (cases "F = bot") 
-     (auto intro!: tendsto_le_const[of F] assms 
+  by (cases "F = bot")
+     (auto intro!: tendsto_le_const[of F] assms
                    continuous_on_tendsto_compose[OF continuous_on_inverse_ereal])
 
 
 subsubsection \<open>liminf and limsup\<close>
 
-lemma Limsup_ereal_mult_right: 
+lemma Limsup_ereal_mult_right:
   assumes "F \<noteq> bot" "(c::real) \<ge> 0"
   shows   "Limsup F (\<lambda>n. f n * ereal c) = Limsup F f * ereal c"
 proof (rule Limsup_compose_continuous_mono)
@@ -3792,7 +3822,7 @@
     by (force simp: continuous_on_def mult_ac)
 qed (insert assms, auto simp: mono_def ereal_mult_right_mono)
 
-lemma Liminf_ereal_mult_right: 
+lemma Liminf_ereal_mult_right:
   assumes "F \<noteq> bot" "(c::real) \<ge> 0"
   shows   "Liminf F (\<lambda>n. f n * ereal c) = Liminf F f * ereal c"
 proof (rule Liminf_compose_continuous_mono)
@@ -3801,36 +3831,36 @@
     by (force simp: continuous_on_def mult_ac)
 qed (insert assms, auto simp: mono_def ereal_mult_right_mono)
 
-lemma Limsup_ereal_mult_left: 
+lemma Limsup_ereal_mult_left:
   assumes "F \<noteq> bot" "(c::real) \<ge> 0"
   shows   "Limsup F (\<lambda>n. ereal c * f n) = ereal c * Limsup F f"
   using Limsup_ereal_mult_right[OF assms] by (subst (1 2) mult.commute)
 
-lemma limsup_ereal_mult_right: 
+lemma limsup_ereal_mult_right:
   "(c::real) \<ge> 0 \<Longrightarrow> limsup (\<lambda>n. f n * ereal c) = limsup f * ereal c"
   by (rule Limsup_ereal_mult_right) simp_all
 
-lemma limsup_ereal_mult_left: 
+lemma limsup_ereal_mult_left:
   "(c::real) \<ge> 0 \<Longrightarrow> limsup (\<lambda>n. ereal c * f n) = ereal c * limsup f"
   by (subst (1 2) mult.commute, rule limsup_ereal_mult_right) simp_all
 
-lemma Limsup_add_ereal_right: 
+lemma Limsup_add_ereal_right:
   "F \<noteq> bot \<Longrightarrow> abs c \<noteq> \<infinity> \<Longrightarrow> Limsup F (\<lambda>n. g n + (c :: ereal)) = Limsup F g + c"
   by (rule Limsup_compose_continuous_mono) (auto simp: mono_def ereal_add_mono continuous_on_def)
 
-lemma Limsup_add_ereal_left: 
+lemma Limsup_add_ereal_left:
   "F \<noteq> bot \<Longrightarrow> abs c \<noteq> \<infinity> \<Longrightarrow> Limsup F (\<lambda>n. (c :: ereal) + g n) = c + Limsup F g"
   by (subst (1 2) add.commute) (rule Limsup_add_ereal_right)
 
-lemma Liminf_add_ereal_right: 
+lemma Liminf_add_ereal_right:
   "F \<noteq> bot \<Longrightarrow> abs c \<noteq> \<infinity> \<Longrightarrow> Liminf F (\<lambda>n. g n + (c :: ereal)) = Liminf F g + c"
   by (rule Liminf_compose_continuous_mono) (auto simp: mono_def ereal_add_mono continuous_on_def)
 
-lemma Liminf_add_ereal_left: 
+lemma Liminf_add_ereal_left:
   "F \<noteq> bot \<Longrightarrow> abs c \<noteq> \<infinity> \<Longrightarrow> Liminf F (\<lambda>n. (c :: ereal) + g n) = c + Liminf F g"
   by (subst (1 2) add.commute) (rule Liminf_add_ereal_right)
 
-lemma 
+lemma
   assumes "F \<noteq> bot"
   assumes nonneg: "eventually (\<lambda>x. f x \<ge> (0::ereal)) F"
   shows   Liminf_inverse_ereal: "Liminf F (\<lambda>x. inverse (f x)) = inverse (Limsup F f)"
@@ -3843,7 +3873,7 @@
   finally have cont: "continuous_on UNIV inv" .
   have antimono: "antimono inv" unfolding inv_def antimono_def
     by (auto intro!: ereal_inverse_antimono)
-  
+
   have "Liminf F (\<lambda>x. inverse (f x)) = Liminf F (\<lambda>x. inv (f x))" using nonneg
     by (auto intro!: Liminf_eq elim!: eventually_mono simp: inv_def)
   also have "... = inv (Limsup F f)"
diff -r 106569399cd6 -r acfc4ad7b76a src/HOL/Limits.thy
--- a/src/HOL/Limits.thy	Mon Feb 08 19:53:49 2016 +0100
+++ b/src/HOL/Limits.thy	Tue Feb 09 06:39:31 2016 +0100
@@ -620,6 +620,12 @@
   shows "(\<And>i. i \<in> S \<Longrightarrow> continuous_on s (f i)) \<Longrightarrow> continuous_on s (\<lambda>x. \<Sum>i\<in>S. f i x)"
   unfolding continuous_on_def by (auto intro: tendsto_setsum)
 
+instance nat :: topological_comm_monoid_add
+  proof qed (simp add: nhds_discrete principal_prod_principal filterlim_principal eventually_principal)
+
+instance int :: topological_comm_monoid_add
+  proof qed (simp add: nhds_discrete principal_prod_principal filterlim_principal eventually_principal)
+
 subsubsection \<open>Addition and subtraction\<close>
 
 instance real_normed_vector < topological_comm_monoid_add
diff -r 106569399cd6 -r acfc4ad7b76a src/HOL/Set_Interval.thy
--- a/src/HOL/Set_Interval.thy	Mon Feb 08 19:53:49 2016 +0100
+++ b/src/HOL/Set_Interval.thy	Tue Feb 09 06:39:31 2016 +0100
@@ -181,6 +181,9 @@
 lemma (in linorder) Iic_subset_Iio_iff: "{.. a} \<subseteq> {..< b} \<longleftrightarrow> a < b"
   by auto
 
+lemma (in preorder) Ioi_le_Ico: "{a <..} \<subseteq> {a ..}"
+  by (auto intro: less_imp_le)
+
 subsection \<open>Two-sided intervals\<close>
 
 context ord
@@ -409,7 +412,7 @@
   "{a .. b} \<subseteq> { c ..< d } \<longleftrightarrow> (a \<le> b \<longrightarrow> c \<le> a \<and> b < d)"
   using dense[of "max a d" "b"]
   by (force simp: subset_eq Ball_def not_less[symmetric])
-  
+
 lemma greaterThanLessThan_subseteq_greaterThanLessThan:
   "{a <..< b} \<subseteq> {c <..< d} \<longleftrightarrow> (a < b \<longrightarrow> a \<ge> c \<and> b \<le> d)"
   using dense[of "a" "min c b"] dense[of "max a d" "b"]
@@ -792,8 +795,8 @@
   by (auto intro: set_eqI)
 
 lemma atLeastLessThan_add_Un: "i \<le> j \<Longrightarrow> {i..<j+k} = {i..<j} \<union> {j..<j+k::nat}"
-  apply (induct k) 
-  apply (simp_all add: atLeastLessThanSuc)   
+  apply (induct k)
+  apply (simp_all add: atLeastLessThanSuc)
   done
 
 subsubsection \<open>Intervals and numerals\<close>
@@ -807,7 +810,7 @@
   by (simp add: numeral_eq_Suc atMost_Suc)
 
 lemma atLeastLessThan_nat_numeral:  \<comment>\<open>Evaluation for specific numerals\<close>
-  "atLeastLessThan m (numeral k :: nat) = 
+  "atLeastLessThan m (numeral k :: nat) =
      (if m \<le> (pred_numeral k) then insert (pred_numeral k) (atLeastLessThan m (pred_numeral k))
                  else {})"
   by (simp add: numeral_eq_Suc atLeastLessThanSuc)
@@ -875,7 +878,7 @@
             else {b/m + c .. a/m + c})"
   using image_affinity_atLeastAtMost [of "inverse m" c a b]
   by (simp add: field_class.field_divide_inverse algebra_simps)
-    
+
 lemma image_affinity_atLeastAtMost_div_diff:
   fixes c :: "'a::linordered_field"
   shows "((\<lambda>x. x/m - c) ` {a..b}) = (if {a..b}={} then {}
@@ -1085,15 +1088,14 @@
   qed
 qed
 
-lemma UN_UN_finite_eq:
-  "(\<Union>n::nat. \<Union>i\<in>{0..<n}. A i) = (\<Union>n. A n)"
-  by (auto simp add: atLeast0LessThan) 
+lemma UN_UN_finite_eq: "(\<Union>n::nat. \<Union>i\<in>{0..<n}. A i) = (\<Union>n. A n)"
+  by (auto simp add: atLeast0LessThan)
 
 lemma UN_finite_subset:
   "(\<And>n::nat. (\<Union>i\<in>{0..<n}. A i) \<subseteq> C) \<Longrightarrow> (\<Union>n. A n) \<subseteq> C"
   by (subst UN_UN_finite_eq [symmetric]) blast
 
-lemma UN_finite2_subset: 
+lemma UN_finite2_subset:
   assumes "\<And>n::nat. (\<Union>i\<in>{0..<n}. A i) \<subseteq> (\<Union>i\<in>{0..<n + k}. B i)"
   shows "(\<Union>n. A n) \<subseteq> (\<Union>n. B n)"
 proof (rule UN_finite_subset, rule)
@@ -1311,7 +1313,7 @@
   hence c: "{k \<in> M. k < Suc i} = insert 0 ({k \<in> M. k < Suc i} - {0})"
     by (auto simp only: insert_Diff)
   have b: "{k \<in> M. k < Suc i} - {0} = {k \<in> M - {0}. k < Suc i}"  by auto
-  from finite_M_bounded_by_nat[of "\<lambda>x. x \<in> M" "Suc i"] 
+  from finite_M_bounded_by_nat[of "\<lambda>x. x \<in> M" "Suc i"]
   have "Suc (card {k. Suc k \<in> M \<and> k < i}) = card (insert 0 ({k \<in> M. k < Suc i} - {0}))"
     apply (subst card_insert)
     apply simp_all
@@ -1520,7 +1522,7 @@
 
 lemma setsum_head:
   fixes n :: nat
-  assumes mn: "m <= n" 
+  assumes mn: "m <= n"
   shows "(\<Sum>x\<in>{m..n}. P x) = P m + (\<Sum>x\<in>{m<..n}. P x)" (is "?lhs = ?rhs")
 proof -
   from mn
diff -r 106569399cd6 -r acfc4ad7b76a src/HOL/Topological_Spaces.thy
--- a/src/HOL/Topological_Spaces.thy	Mon Feb 08 19:53:49 2016 +0100
+++ b/src/HOL/Topological_Spaces.thy	Tue Feb 09 06:39:31 2016 +0100
@@ -296,11 +296,22 @@
   case (Basis S) then show ?case by (fastforce intro: exI[of _ y] lt_ex)
 qed blast+
 
+subsection \<open>Setup some topologies\<close>
+
 subsubsection \<open>Boolean is an order topology\<close>
 
-text \<open>It also is a discrete topology, but don't have a type class for it (yet).\<close>
-
-instantiation bool :: order_topology
+text \<open>It is a discrete topology, but don't have a type class for it (yet).\<close>
+
+class discrete_topology = topological_space +
+  assumes open_discrete: "\<And>A. open A"
+
+instance discrete_topology < t2_space
+proof
+  fix x y :: 'a assume "x \<noteq> y" then show "\<exists>U V. open U \<and> open V \<and> x \<in> U \<and> y \<in> V \<and> U \<inter> V = {}"
+    by (intro exI[of _ "{_}"]) (auto intro!: open_discrete)
+qed
+
+instantiation bool :: linorder_topology
 begin
 
 definition open_bool :: "bool set \<Rightarrow> bool" where
@@ -311,8 +322,9 @@
 
 end
 
-lemma open_bool[simp, intro!]: "open (A::bool set)"
-proof -
+instance bool :: discrete_topology
+proof
+  fix A :: "bool set"
   have *: "{False <..} = {True}" "{..< True} = {False}"
     by auto
   have "A = UNIV \<or> A = {} \<or> A = {False <..} \<or> A = {..< True}"
@@ -321,6 +333,64 @@
     by auto
 qed
 
+instantiation nat :: linorder_topology
+begin
+
+definition open_nat :: "nat set \<Rightarrow> bool" where
+  "open_nat = generate_topology (range (\<lambda>a. {..< a}) \<union> range (\<lambda>a. {a <..}))"
+
+instance
+  proof qed (rule open_nat_def)
+
+end
+
+instance nat :: discrete_topology
+proof
+  fix A :: "nat set"
+  have "open {n}" for n :: nat
+  proof (cases n)
+    case 0
+    moreover have "{0} = {..<1::nat}"
+      by auto
+    ultimately show ?thesis
+       by auto
+  next
+    case (Suc n')
+    moreover then have "{n} = {..<Suc n} \<inter> {n' <..}"
+      by auto
+    ultimately show ?thesis
+      by (auto intro: open_lessThan open_greaterThan)
+  qed
+  then have "open (\<Union>a\<in>A. {a})"
+    by (intro open_UN) auto
+  then show "open A"
+    by simp
+qed
+
+instantiation int :: linorder_topology
+begin
+
+definition open_int :: "int set \<Rightarrow> bool" where
+  "open_int = generate_topology (range (\<lambda>a. {..< a}) \<union> range (\<lambda>a. {a <..}))"
+
+instance
+  proof qed (rule open_int_def)
+
+end
+
+instance int :: discrete_topology
+proof
+  fix A :: "int set"
+  have "{..<i + 1} \<inter> {i-1 <..} = {i}" for i :: int
+    by auto
+  then have "open {i}" for i :: int
+    using open_Int[OF open_lessThan[of "i + 1"] open_greaterThan[of "i - 1"]] by auto
+  then have "open (\<Union>a\<in>A. {a})"
+    by (intro open_UN) auto
+  then show "open A"
+    by simp
+qed
+
 subsubsection \<open>Topological filters\<close>
 
 definition (in topological_space) nhds :: "'a \<Rightarrow> 'a filter"
@@ -363,6 +433,15 @@
   "x \<noteq> y \<Longrightarrow> (\<forall>\<^sub>F x in nhds x. x \<noteq> y)"
   by (drule t1_space) (auto simp: eventually_nhds)
 
+lemma (in topological_space) nhds_discrete_open: "open {x} \<Longrightarrow> nhds x = principal {x}"
+  by (auto simp: nhds_def intro!: antisym INF_greatest INF_lower2[of "{x}"])
+
+lemma (in discrete_topology) nhds_discrete: "nhds x = principal {x}"
+  by (simp add: nhds_discrete_open open_discrete)
+
+lemma (in discrete_topology) at_discrete: "at x within S = bot"
+  unfolding at_within_def nhds_discrete by simp
+
 lemma at_within_eq: "at x within s = (INF S:{S. open S \<and> x \<in> S}. principal (S \<inter> s - {x}))"
   unfolding nhds_def at_within_def by (subst INF_inf_const2[symmetric]) (auto simp add: Diff_Int_distrib)
 
@@ -1996,7 +2075,7 @@
 proof safe
   fix P :: "'a \<Rightarrow> bool" assume "connected S" "continuous_on S P"
   then have "\<And>b. \<exists>A. open A \<and> A \<inter> S = P -` {b} \<inter> S"
-    unfolding continuous_on_open_invariant by simp
+    unfolding continuous_on_open_invariant by (simp add: open_discrete)
   from this[of True] this[of False]
   obtain t f where "open t" "open f" and *: "f \<inter> S = P -` {False} \<inter> S" "t \<inter> S = P -` {True} \<inter> S"
     by auto