--- a/CONTRIBUTORS Fri Jan 19 20:09:04 2018 +0100
+++ b/CONTRIBUTORS Fri Jan 19 20:11:14 2018 +0100
@@ -6,6 +6,9 @@
Contributions to this Isabelle version
--------------------------------------
+* January 2018: Sebastien Gouezel
+ Various small additions to HOL-Analysis
+
* December 2017: Jan Gilcher, Andreas Lochbihler, Dmitriy Traytel
A new conditional parametricity prover.
--- a/src/HOL/Analysis/Connected.thy Fri Jan 19 20:09:04 2018 +0100
+++ b/src/HOL/Analysis/Connected.thy Fri Jan 19 20:11:14 2018 +0100
@@ -1292,7 +1292,7 @@
definition "infdist x A = (if A = {} then 0 else INF a:A. dist x a)"
-lemma bdd_below_infdist[intro, simp]: "bdd_below (dist x`A)"
+lemma bdd_below_image_dist[intro, simp]: "bdd_below (dist x ` A)"
by (auto intro!: zero_le_dist)
lemma infdist_notempty: "A \<noteq> {} \<Longrightarrow> infdist x A = (INF a:A. dist x a)"
@@ -1396,6 +1396,58 @@
with assms show ?thesis by simp
qed
+lemma infdist_pos_not_in_closed:
+ assumes "closed S" "S \<noteq> {}" "x \<notin> S"
+ shows "infdist x S > 0"
+using in_closed_iff_infdist_zero[OF assms(1) assms(2), of x] assms(3) infdist_nonneg le_less by fastforce
+
+text \<open>Every metric space is a T4 space:\<close>
+
+instance metric_space \<subseteq> t4_space
+proof
+ fix S T::"'a set" assume H: "closed S" "closed T" "S \<inter> T = {}"
+ consider "S = {}" | "T = {}" | "S \<noteq> {} \<and> T \<noteq> {}" by auto
+ then show "\<exists>U V. open U \<and> open V \<and> S \<subseteq> U \<and> T \<subseteq> V \<and> U \<inter> V = {}"
+ proof (cases)
+ case 1
+ show ?thesis
+ apply (rule exI[of _ "{}"], rule exI[of _ UNIV]) using 1 by auto
+ next
+ case 2
+ show ?thesis
+ apply (rule exI[of _ UNIV], rule exI[of _ "{}"]) using 2 by auto
+ next
+ case 3
+ define U where "U = (\<Union>x\<in>S. ball x ((infdist x T)/2))"
+ have A: "open U" unfolding U_def by auto
+ have "infdist x T > 0" if "x \<in> S" for x
+ using H that 3 by (auto intro!: infdist_pos_not_in_closed)
+ then have B: "S \<subseteq> U" unfolding U_def by auto
+ define V where "V = (\<Union>x\<in>T. ball x ((infdist x S)/2))"
+ have C: "open V" unfolding V_def by auto
+ have "infdist x S > 0" if "x \<in> T" for x
+ using H that 3 by (auto intro!: infdist_pos_not_in_closed)
+ then have D: "T \<subseteq> V" unfolding V_def by auto
+
+ have "(ball x ((infdist x T)/2)) \<inter> (ball y ((infdist y S)/2)) = {}" if "x \<in> S" "y \<in> T" for x y
+ proof (auto)
+ fix z assume H: "dist x z * 2 < infdist x T" "dist y z * 2 < infdist y S"
+ have "2 * dist x y \<le> 2 * dist x z + 2 * dist y z"
+ using dist_triangle[of x y z] by (auto simp add: dist_commute)
+ also have "... < infdist x T + infdist y S"
+ using H by auto
+ finally have "dist x y < infdist x T \<or> dist x y < infdist y S"
+ by auto
+ then show False
+ using infdist_le[OF \<open>x \<in> S\<close>, of y] infdist_le[OF \<open>y \<in> T\<close>, of x] by (auto simp add: dist_commute)
+ qed
+ then have E: "U \<inter> V = {}"
+ unfolding U_def V_def by auto
+ show ?thesis
+ apply (rule exI[of _ U], rule exI[of _ V]) using A B C D E by auto
+ qed
+qed
+
lemma tendsto_infdist [tendsto_intros]:
assumes f: "(f \<longlongrightarrow> l) F"
shows "((\<lambda>x. infdist (f x) A) \<longlongrightarrow> infdist l A) F"
--- a/src/HOL/Conditionally_Complete_Lattices.thy Fri Jan 19 20:09:04 2018 +0100
+++ b/src/HOL/Conditionally_Complete_Lattices.thy Fri Jan 19 20:11:14 2018 +0100
@@ -164,11 +164,19 @@
thus "bdd_below (A \<union> B)" unfolding bdd_below_def ..
qed
-lemma bdd_above_sup[simp]: "bdd_above ((\<lambda>x. sup (f x) (g x)) ` A) \<longleftrightarrow> bdd_above (f`A) \<and> bdd_above (g`A)"
- by (auto simp: bdd_above_def intro: le_supI1 le_supI2)
+lemma bdd_above_image_sup[simp]:
+ "bdd_above ((\<lambda>x. sup (f x) (g x)) ` A) \<longleftrightarrow> bdd_above (f`A) \<and> bdd_above (g`A)"
+by (auto simp: bdd_above_def intro: le_supI1 le_supI2)
-lemma bdd_below_inf[simp]: "bdd_below ((\<lambda>x. inf (f x) (g x)) ` A) \<longleftrightarrow> bdd_below (f`A) \<and> bdd_below (g`A)"
- by (auto simp: bdd_below_def intro: le_infI1 le_infI2)
+lemma bdd_below_image_inf[simp]:
+ "bdd_below ((\<lambda>x. inf (f x) (g x)) ` A) \<longleftrightarrow> bdd_below (f`A) \<and> bdd_below (g`A)"
+by (auto simp: bdd_below_def intro: le_infI1 le_infI2)
+
+lemma bdd_below_UN[simp]: "finite I \<Longrightarrow> bdd_below (\<Union>i\<in>I. A i) = (\<forall>i \<in> I. bdd_below (A i))"
+by (induction I rule: finite.induct) auto
+
+lemma bdd_above_UN[simp]: "finite I \<Longrightarrow> bdd_above (\<Union>i\<in>I. A i) = (\<forall>i \<in> I. bdd_above (A i))"
+by (induction I rule: finite.induct) auto
end
--- a/src/HOL/Finite_Set.thy Fri Jan 19 20:09:04 2018 +0100
+++ b/src/HOL/Finite_Set.thy Fri Jan 19 20:11:14 2018 +0100
@@ -1743,6 +1743,24 @@
then show "\<exists>B. finite B \<and> card B = Suc n \<and> B \<subseteq> A" ..
qed
+text \<open>Sometimes, to prove that a set is finite, it is convenient to work with finite subsets
+and to show that their cardinalities are uniformly bounded. This possibility is formalized in
+the next criterion.\<close>
+
+lemma finite_if_finite_subsets_card_bdd:
+ assumes "\<And>G. G \<subseteq> F \<Longrightarrow> finite G \<Longrightarrow> card G \<le> C"
+ shows "finite F \<and> card F \<le> C"
+proof (cases "finite F")
+ case False
+ obtain n::nat where n: "n > max C 0" by auto
+ obtain G where G: "G \<subseteq> F" "card G = n" using infinite_arbitrarily_large[OF False] by auto
+ hence "finite G" using \<open>n > max C 0\<close> using card_infinite gr_implies_not0 by blast
+ hence False using assms G n not_less by auto
+ thus ?thesis ..
+next
+ case True thus ?thesis using assms[of F] by auto
+qed
+
subsubsection \<open>Cardinality of image\<close>
--- a/src/HOL/Library/Extended_Nonnegative_Real.thy Fri Jan 19 20:09:04 2018 +0100
+++ b/src/HOL/Library/Extended_Nonnegative_Real.thy Fri Jan 19 20:11:14 2018 +0100
@@ -570,10 +570,10 @@
lemma enn2ereal_eq_top_iff[simp]: "enn2ereal x = \<infinity> \<longleftrightarrow> x = top"
by transfer (simp add: top_ereal_def)
-lemma enn2ereal_top: "enn2ereal top = \<infinity>"
+lemma enn2ereal_top[simp]: "enn2ereal top = \<infinity>"
by transfer (simp add: top_ereal_def)
-lemma e2ennreal_infty: "e2ennreal \<infinity> = top"
+lemma e2ennreal_infty[simp]: "e2ennreal \<infinity> = top"
by (simp add: top_ennreal.abs_eq top_ereal_def)
lemma ennreal_top_minus[simp]: "top - x = (top::ennreal)"
@@ -659,9 +659,6 @@
subgoal for a b c
apply (cases a b c rule: ereal3_cases)
apply (auto simp: ereal_max[symmetric] simp del: ereal_max)
- apply (auto simp: top_ereal_def[symmetric] sup_ereal_def[symmetric]
- simp del: sup_ereal_def)
- apply (auto simp add: top_ereal_def)
done
done
@@ -926,6 +923,12 @@
lemma e2ennreal_enn2ereal[simp]: "e2ennreal (enn2ereal x) = x"
by (simp add: e2ennreal_def max_absorb2 ennreal.enn2ereal_inverse)
+lemma enn2ereal_e2ennreal: "x \<ge> 0 \<Longrightarrow> enn2ereal (e2ennreal x) = x"
+by (metis e2ennreal_enn2ereal ereal_ennreal_cases not_le)
+
+lemma e2ennreal_ereal [simp]: "e2ennreal (ereal x) = ennreal x"
+by (metis e2ennreal_def enn2ereal_inverse ennreal.rep_eq sup_ereal_def)
+
lemma ennreal_0[simp]: "ennreal 0 = 0"
by (simp add: ennreal_def max.absorb1 zero_ennreal.abs_eq)
@@ -1001,6 +1004,10 @@
lemma ennreal_minus_top[simp]: "ennreal a - top = 0"
by (simp add: minus_top_ennreal)
+lemma e2eenreal_enn2ereal_diff [simp]:
+ "e2ennreal(enn2ereal x - enn2ereal y) = x - y" for x y
+by (cases x, cases y, auto simp add: ennreal_minus e2ennreal_neg)
+
lemma ennreal_mult: "0 \<le> a \<Longrightarrow> 0 \<le> b \<Longrightarrow> ennreal (a * b) = ennreal a * ennreal b"
by transfer (simp add: max_absorb2)
@@ -1465,8 +1472,7 @@
by (cases y rule: ennreal_cases) auto
then show "\<exists>i\<in>UNIV. y < of_nat i"
using reals_Archimedean2[of "max 1 r"] zero_less_one
- by (auto simp: ennreal_of_nat_eq_real_of_nat ennreal_def less_ennreal.abs_eq eq_onp_def max.absorb2
- dest!: one_less_of_natD intro: less_trans)
+ by (simp add: ennreal_Ex_less_of_nat)
qed
lemma ennreal_SUP_eq_top:
--- a/src/HOL/Library/Extended_Real.thy Fri Jan 19 20:09:04 2018 +0100
+++ b/src/HOL/Library/Extended_Real.thy Fri Jan 19 20:11:14 2018 +0100
@@ -1776,6 +1776,31 @@
using zero_neq_one by blast
qed
+lemma min_PInf [simp]: "min (\<infinity>::ereal) x = x"
+by (metis min_top top_ereal_def)
+
+lemma min_PInf2 [simp]: "min x (\<infinity>::ereal) = x"
+by (metis min_top2 top_ereal_def)
+
+lemma max_PInf [simp]: "max (\<infinity>::ereal) x = \<infinity>"
+by (metis max_top top_ereal_def)
+
+lemma max_PInf2 [simp]: "max x (\<infinity>::ereal) = \<infinity>"
+by (metis max_top2 top_ereal_def)
+
+lemma min_MInf [simp]: "min (-\<infinity>::ereal) x = -\<infinity>"
+by (metis min_bot bot_ereal_def)
+
+lemma min_MInf2 [simp]: "min x (-\<infinity>::ereal) = -\<infinity>"
+by (metis min_bot2 bot_ereal_def)
+
+lemma max_MInf [simp]: "max (-\<infinity>::ereal) x = x"
+by (metis max_bot bot_ereal_def)
+
+lemma max_MInf2 [simp]: "max x (-\<infinity>::ereal) = x"
+by (metis max_bot2 bot_ereal_def)
+
+
subsubsection "Topological space"
instantiation ereal :: linear_continuum_topology
--- a/src/HOL/Orderings.thy Fri Jan 19 20:09:04 2018 +0100
+++ b/src/HOL/Orderings.thy Fri Jan 19 20:11:14 2018 +0100
@@ -1287,6 +1287,18 @@
"a \<noteq> \<bottom> \<longleftrightarrow> \<bottom> < a"
by (fact bot.not_eq_extremum)
+lemma max_bot[simp]: "max bot x = x"
+by(simp add: max_def bot_unique)
+
+lemma max_bot2[simp]: "max x bot = x"
+by(simp add: max_def bot_unique)
+
+lemma min_bot[simp]: "min bot x = bot"
+by(simp add: min_def bot_unique)
+
+lemma min_bot2[simp]: "min x bot = bot"
+by(simp add: min_def bot_unique)
+
end
class top =
@@ -1315,6 +1327,18 @@
"a \<noteq> \<top> \<longleftrightarrow> a < \<top>"
by (fact top.not_eq_extremum)
+lemma max_top[simp]: "max top x = top"
+by(simp add: max_def top_unique)
+
+lemma max_top2[simp]: "max x top = top"
+by(simp add: max_def top_unique)
+
+lemma min_top[simp]: "min top x = x"
+by(simp add: min_def top_unique)
+
+lemma min_top2[simp]: "min x top = x"
+by(simp add: min_def top_unique)
+
end
--- a/src/HOL/Topological_Spaces.thy Fri Jan 19 20:09:04 2018 +0100
+++ b/src/HOL/Topological_Spaces.thy Fri Jan 19 20:11:14 2018 +0100
@@ -196,6 +196,27 @@
using t0_space [of x y] by blast
+text \<open>A classical separation axiom for topological space, the T3 axiom -- also called regularity:
+if a point is not in a closed set, then there are open sets separating them.\<close>
+
+class t3_space = t2_space +
+ assumes t3_space: "closed S \<Longrightarrow> y \<notin> S \<Longrightarrow> \<exists>U V. open U \<and> open V \<and> y \<in> U \<and> S \<subseteq> V \<and> U \<inter> V = {}"
+
+text \<open>A classical separation axiom for topological space, the T4 axiom -- also called normality:
+if two closed sets are disjoint, then there are open sets separating them.\<close>
+
+class t4_space = t2_space +
+ assumes t4_space: "closed S \<Longrightarrow> closed T \<Longrightarrow> S \<inter> T = {} \<Longrightarrow> \<exists>U V. open U \<and> open V \<and> S \<subseteq> U \<and> T \<subseteq> V \<and> U \<inter> V = {}"
+
+text \<open>T4 is stronger than T3, and weaker than metric.\<close>
+
+instance t4_space \<subseteq> t3_space
+proof
+ fix S and y::'a assume "closed S" "y \<notin> S"
+ then show "\<exists>U V. open U \<and> open V \<and> y \<in> U \<and> S \<subseteq> V \<and> U \<inter> V = {}"
+ using t4_space[of "{y}" S] by auto
+qed
+
text \<open>A perfect space is a topological space with no isolated points.\<close>
class perfect_space = topological_space +
@@ -760,7 +781,7 @@
and "y < a \<Longrightarrow> eventually (\<lambda>x. f x < a) F"
using assms by (auto simp: order_tendsto_iff)
-lemma (in linorder_topology) tendsto_max:
+lemma (in linorder_topology) tendsto_max[tendsto_intros]:
assumes X: "(X \<longlongrightarrow> x) net"
and Y: "(Y \<longlongrightarrow> y) net"
shows "((\<lambda>x. max (X x) (Y x)) \<longlongrightarrow> max x y) net"
@@ -778,7 +799,7 @@
by (auto simp: eventually_conj_iff)
qed
-lemma (in linorder_topology) tendsto_min:
+lemma (in linorder_topology) tendsto_min[tendsto_intros]:
assumes X: "(X \<longlongrightarrow> x) net"
and Y: "(Y \<longlongrightarrow> y) net"
shows "((\<lambda>x. min (X x) (Y x)) \<longlongrightarrow> min x y) net"