--- 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
--- 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)"
--- 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
--- 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
--- 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