--- a/src/HOL/Enum.thy Mon Mar 26 19:13:45 2018 +0200
+++ b/src/HOL/Enum.thy Mon Mar 26 23:58:43 2018 +0200
@@ -795,18 +795,29 @@
proof
fix x A
show "x \<in> A \<Longrightarrow> \<Sqinter>A \<le> x"
- by (cut_tac A = A and a = x in Inf_finite_insert, simp add: insert_absorb inf.absorb_iff2)
+ by (metis Set.set_insert abel_semigroup.commute local.Inf_finite_insert local.inf.abel_semigroup_axioms local.inf.left_idem local.inf.orderI)
show "x \<in> A \<Longrightarrow> x \<le> \<Squnion>A"
- by (cut_tac A = A and a = x in Sup_finite_insert, simp add: insert_absorb sup.absorb_iff2)
+ by (metis Set.set_insert insert_absorb2 local.Sup_finite_insert local.sup.absorb_iff2)
next
fix A z
- show "(\<And>x. x \<in> A \<Longrightarrow> z \<le> x) \<Longrightarrow> z \<le> \<Sqinter>A"
- apply (cut_tac F = A and P = "\<lambda> A . (\<forall> x. x \<in> A \<longrightarrow> z \<le> x) \<longrightarrow> z \<le> \<Sqinter>A" in finite_induct, simp_all add: Inf_finite_empty Inf_finite_insert)
- by(cut_tac A = UNIV and a = z in Sup_finite_insert, simp add: insert_UNIV local.sup.absorb_iff2)
+ have "\<Squnion> UNIV = z \<squnion> \<Squnion>UNIV"
+ by (subst Sup_finite_insert [symmetric], simp add: insert_UNIV)
+ from this have [simp]: "z \<le> \<Squnion>UNIV"
+ using local.le_iff_sup by auto
+ have "(\<forall> x. x \<in> A \<longrightarrow> z \<le> x) \<longrightarrow> z \<le> \<Sqinter>A"
+ apply (rule finite_induct [of A "\<lambda> A . (\<forall> x. x \<in> A \<longrightarrow> z \<le> x) \<longrightarrow> z \<le> \<Sqinter>A"])
+ by (simp_all add: Inf_finite_empty Inf_finite_insert)
+ from this show "(\<And>x. x \<in> A \<Longrightarrow> z \<le> x) \<Longrightarrow> z \<le> \<Sqinter>A"
+ by simp
- show " (\<And>x. x \<in> A \<Longrightarrow> x \<le> z) \<Longrightarrow> \<Squnion>A \<le> z"
- apply (cut_tac F = A and P = "\<lambda> A . (\<forall> x. x \<in> A \<longrightarrow> x \<le> z) \<longrightarrow> \<Squnion>A \<le> z" in finite_induct, simp_all add: Sup_finite_empty Sup_finite_insert)
- by(cut_tac A = UNIV and a = z in Inf_finite_insert, simp add: insert_UNIV local.inf.absorb_iff2)
+ have "\<Sqinter> UNIV = z \<sqinter> \<Sqinter>UNIV"
+ by (subst Inf_finite_insert [symmetric], simp add: insert_UNIV)
+ from this have [simp]: "\<Sqinter>UNIV \<le> z"
+ by (simp add: local.inf.absorb_iff2)
+ have "(\<forall> x. x \<in> A \<longrightarrow> x \<le> z) \<longrightarrow> \<Squnion>A \<le> z"
+ by (rule finite_induct [of A "\<lambda> A . (\<forall> x. x \<in> A \<longrightarrow> x \<le> z) \<longrightarrow> \<Squnion>A \<le> z" ], simp_all add: Sup_finite_empty Sup_finite_insert)
+ from this show " (\<And>x. x \<in> A \<Longrightarrow> x \<le> z) \<Longrightarrow> \<Squnion>A \<le> z"
+ by blast
next
show "\<Sqinter>{} = \<top>"
by (simp add: Inf_finite_empty top_finite_def)
@@ -818,40 +829,38 @@
class finite_distrib_lattice = finite_lattice + distrib_lattice
begin
lemma finite_inf_Sup: "a \<sqinter> (Sup A) = Sup {a \<sqinter> b | b . b \<in> A}"
-proof (cut_tac F = A and P = "\<lambda> A . a \<sqinter> (Sup A) = Sup {a \<sqinter> b | b . b \<in> A}" in finite_induct, simp_all)
+proof (rule finite_induct [of A "\<lambda> A . a \<sqinter> (Sup A) = Sup {a \<sqinter> b | b . b \<in> A}"], simp_all)
fix x::"'a"
fix F
assume "x \<notin> F"
- assume A: "a \<sqinter> \<Squnion>F = \<Squnion>{a \<sqinter> b |b. b \<in> F}"
-
+ assume [simp]: "a \<sqinter> \<Squnion>F = \<Squnion>{a \<sqinter> b |b. b \<in> F}"
have [simp]: " insert (a \<sqinter> x) {a \<sqinter> b |b. b \<in> F} = {a \<sqinter> b |b. b = x \<or> b \<in> F}"
- by auto
-
+ by blast
have "a \<sqinter> (x \<squnion> \<Squnion>F) = a \<sqinter> x \<squnion> a \<sqinter> \<Squnion>F"
by (simp add: inf_sup_distrib1)
also have "... = a \<sqinter> x \<squnion> \<Squnion>{a \<sqinter> b |b. b \<in> F}"
- by (simp add: A)
+ by simp
also have "... = \<Squnion>{a \<sqinter> b |b. b = x \<or> b \<in> F}"
by (unfold Sup_insert[THEN sym], simp)
-
finally show "a \<sqinter> (x \<squnion> \<Squnion>F) = \<Squnion>{a \<sqinter> b |b. b = x \<or> b \<in> F}"
by simp
qed
lemma finite_Inf_Sup: "INFIMUM A Sup \<le> SUPREMUM {f ` A |f. \<forall>Y\<in>A. f Y \<in> Y} Inf"
-proof (cut_tac F = A and P = "\<lambda> A .INFIMUM A Sup \<le> SUPREMUM {f ` A |f. \<forall>Y\<in>A. f Y \<in> Y} Inf" in finite_induct, simp_all add: finite_UnionD)
+proof (rule finite_induct [of A "\<lambda> A .INFIMUM A Sup \<le> SUPREMUM {f ` A |f. \<forall>Y\<in>A. f Y \<in> Y} Inf"], simp_all add: finite_UnionD)
fix x::"'a set"
fix F
assume "x \<notin> F"
- have [simp]: "{\<Squnion>x \<sqinter> b |b . b \<in> Inf ` {f ` F |f. \<forall>Y\<in>F. f Y \<in> Y} } = {\<Squnion>x \<sqinter> (Inf (f ` F)) |f . (\<forall>Y\<in>F. f Y \<in> Y)}"
- by auto
- have [simp]:" \<And>f b. \<forall>Y\<in>F. f Y \<in> Y \<Longrightarrow> b \<in> x \<Longrightarrow> \<exists>fa. insert b (f ` (F \<inter> {Y. Y \<noteq> x})) = insert (fa x) (fa ` F) \<and> fa x \<in> x \<and> (\<forall>Y\<in>F. fa Y \<in> Y)"
- apply (rule_tac x = "(\<lambda> Y . (if Y = x then b else f Y))" in exI)
+ have [simp]: "{\<Squnion>x \<sqinter> b |b . b \<in> Inf ` {f ` F |f. \<forall>Y\<in>F. f Y \<in> Y} } = {\<Squnion>x \<sqinter> (Inf (f ` F)) |f . (\<forall>Y\<in>F. f Y \<in> Y)}"
by auto
- have [simp]: "\<And>f b. \<forall>Y\<in>F. f Y \<in> Y \<Longrightarrow> b \<in> x \<Longrightarrow> (\<Sqinter>x\<in>F. f x) \<sqinter> b \<le> SUPREMUM {insert (f x) (f ` F) |f. f x \<in> x \<and> (\<forall>Y\<in>F. f Y \<in> Y)} Inf"
- apply (rule_tac i = "(\<lambda> Y . (if Y = x then b else f Y)) ` ({x} \<union> F)" in SUP_upper2, simp)
- apply (subst inf_commute)
- by (simp add: INF_greatest Inf_lower inf.coboundedI2)
+ define fa where "fa = (\<lambda> (b::'a) f Y . (if Y = x then b else f Y))"
+ have "\<And>f b. \<forall>Y\<in>F. f Y \<in> Y \<Longrightarrow> b \<in> x \<Longrightarrow> insert b (f ` (F \<inter> {Y. Y \<noteq> x})) = insert (fa b f x) (fa b f ` F) \<and> fa b f x \<in> x \<and> (\<forall>Y\<in>F. fa b f Y \<in> Y)"
+ by (auto simp add: fa_def)
+ from this have B: "\<And>f b. \<forall>Y\<in>F. f Y \<in> Y \<Longrightarrow> b \<in> x \<Longrightarrow> fa b f ` ({x} \<union> F) \<in> {insert (f x) (f ` F) |f. f x \<in> x \<and> (\<forall>Y\<in>F. f Y \<in> Y)}"
+ by blast
+ have [simp]: "\<And>f b. \<forall>Y\<in>F. f Y \<in> Y \<Longrightarrow> b \<in> x \<Longrightarrow> b \<sqinter> (\<Sqinter>x\<in>F. f x) \<le> SUPREMUM {insert (f x) (f ` F) |f. f x \<in> x \<and> (\<forall>Y\<in>F. f Y \<in> Y)} Inf"
+ using B apply (rule SUP_upper2, simp_all)
+ by (simp_all add: INF_greatest Inf_lower inf.coboundedI2 fa_def)
assume "INFIMUM F Sup \<le> SUPREMUM {f ` F |f. \<forall>Y\<in>F. f Y \<in> Y} Inf"
@@ -866,7 +875,8 @@
by (simp add: finite_inf_Sup)
also have "... \<le> SUPREMUM {insert (f x) (f ` F) |f. f x \<in> x \<and> (\<forall>Y\<in>F. f Y \<in> Y)} Inf"
- by (rule Sup_least, clarsimp, rule Sup_least, clarsimp)
+ apply (rule Sup_least, clarsimp)+
+ by (subst inf_commute, simp)
finally show "\<Squnion>x \<sqinter> INFIMUM F Sup \<le> SUPREMUM {insert (f x) (f ` F) |f. f x \<in> x \<and> (\<forall>Y\<in>F. f Y \<in> Y)} Inf"
by simp
--- a/src/HOL/Filter.thy Mon Mar 26 19:13:45 2018 +0200
+++ b/src/HOL/Filter.thy Mon Mar 26 23:58:43 2018 +0200
@@ -1210,6 +1210,11 @@
apply auto
done
+lemma eventually_compose_filterlim:
+ assumes "eventually P F" "filterlim f F G"
+ shows "eventually (\<lambda>x. P (f x)) G"
+ using assms by (simp add: filterlim_iff)
+
lemma filtermap_eq_strong: "inj f \<Longrightarrow> filtermap f F = filtermap f G \<longleftrightarrow> F = G"
by (simp add: filtermap_mono_strong eq_iff)
--- a/src/HOL/Hilbert_Choice.thy Mon Mar 26 19:13:45 2018 +0200
+++ b/src/HOL/Hilbert_Choice.thy Mon Mar 26 23:58:43 2018 +0200
@@ -815,7 +815,7 @@
using Inf_lower2 Sup_upper by auto
next
show "INFIMUM {f ` A |f. \<forall>Y\<in>A. f Y \<in> Y} Sup \<le> SUPREMUM A Inf"
- proof (simp add: Inf_Sup, rule_tac SUP_least, simp, safe)
+ proof (simp add: Inf_Sup, rule SUP_least, simp, safe)
fix f
assume "\<forall>Y. (\<exists>f. Y = f ` A \<and> (\<forall>Y\<in>A. f Y \<in> Y)) \<longrightarrow> f Y \<in> Y"
from this have B: "\<And> F . (\<forall> Y \<in> A . F Y \<in> Y) \<Longrightarrow> \<exists> Z \<in> A . f (F ` A) = F Z"
@@ -828,7 +828,7 @@
have B: "... \<le> SUPREMUM A Inf"
by (simp add: SUP_upper)
from A and B show ?thesis
- by (drule_tac order_trans, simp_all)
+ by simp
next
case False
from this have X: "\<And> Z . Z \<in> A \<Longrightarrow> \<exists> x . x \<in> Z \<and> \<not> INFIMUM {f ` A |f. \<forall>Y\<in>A. f Y \<in> Y} f \<le> x"
@@ -842,8 +842,9 @@
by blast
from E and D have W: "\<not> INFIMUM {f ` A |f. \<forall>Y\<in>A. f Y \<in> Y} f \<le> F Z"
by simp
- from C have "INFIMUM {f ` A |f. \<forall>Y\<in>A. f Y \<in> Y} f \<le> f (F ` A)"
- by (rule_tac INF_lower, blast)
+ have "INFIMUM {f ` A |f. \<forall>Y\<in>A. f Y \<in> Y} f \<le> f (F ` A)"
+ apply (rule INF_lower)
+ using C by blast
from this and W and Y show ?thesis
by simp
qed
@@ -859,12 +860,13 @@
lemma sup_Inf: "a \<squnion> Inf B = (INF b:B. a \<squnion> b)"
proof (rule antisym)
show "a \<squnion> Inf B \<le> (INF b:B. a \<squnion> b)"
- using Inf_lower sup.mono by (rule_tac INF_greatest, fastforce)
+ apply (rule INF_greatest)
+ using Inf_lower sup.mono by fastforce
next
have "(INF b:B. a \<squnion> b) \<le> INFIMUM {{f {a}, f B} |f. f {a} = a \<and> f B \<in> B} Sup"
by (rule INF_greatest, auto simp add: INF_lower)
- also have "... = a \<squnion> Inf B"
- by (cut_tac A = "{{a}, B}" in Sup_Inf, simp)
+ also have "... = SUPREMUM {{a}, B} Inf"
+ by (unfold Sup_Inf, simp)
finally show "(INF b:B. a \<squnion> b) \<le> a \<squnion> Inf B"
by simp
qed
@@ -879,7 +881,7 @@
by (rule SUP_least, rule INF_greatest, rule SUP_upper2, simp_all, rule INF_lower2, simp, blast)
next
have "(INF y. SUP x. ((P x y))) \<le> Inf (Sup ` {{P x y | x . True} | y . True })" (is "?A \<le> ?B")
- proof (rule_tac INF_greatest, clarsimp)
+ proof (rule INF_greatest, clarsimp)
fix y
have "?A \<le> (SUP x. P x y)"
by (rule INF_lower, simp)
@@ -889,7 +891,7 @@
by simp
qed
also have "... \<le> (SUP x. INF y. P (x y) y)"
- proof (subst Inf_Sup, rule_tac SUP_least, clarsimp)
+ proof (subst Inf_Sup, rule SUP_least, clarsimp)
fix f
assume A: "\<forall>Y. (\<exists>y. Y = {uu. \<exists>x. uu = P x y}) \<longrightarrow> f Y \<in> Y"
@@ -897,9 +899,10 @@
proof (rule INF_greatest, clarsimp)
fix y
have "(INF x:{uu. \<exists>y. uu = {uu. \<exists>x. uu = P x y}}. f x) \<le> f {uu. \<exists>x. uu = P x y}"
- by (rule_tac INF_lower, blast)
+ by (rule INF_lower, blast)
also have "... \<le> P (SOME x. f {uu . \<exists>x. uu = P x y} = P x y) y"
- using A by (rule_tac someI2_ex, auto)
+ apply (rule someI2_ex)
+ using A by auto
finally show "(INF x:{uu. \<exists>y. uu = {uu. \<exists>x. uu = P x y}}. f x) \<le> P (SOME x. f {uu . \<exists>x. uu = P x y} = P x y) y"
by simp
qed
@@ -914,8 +917,12 @@
lemma INF_SUP_set: "(INF x:A. SUP a:x. (g a)) = (SUP x:{f ` A |f. \<forall>Y\<in>A. f Y \<in> Y}. INF a:x. g a)"
proof (rule antisym)
+ have [simp]: "\<And>f xa. \<forall>Y\<in>A. f Y \<in> Y \<Longrightarrow> xa \<in> A \<Longrightarrow> (\<Sqinter>x\<in>A. g (f x)) \<le> g (f xa)"
+ by (rule INF_lower2, blast+)
+ have B: "\<And>f xa. \<forall>Y\<in>A. f Y \<in> Y \<Longrightarrow> xa \<in> A \<Longrightarrow> f xa \<in> xa"
+ by blast
have A: "\<And>f xa. \<forall>Y\<in>A. f Y \<in> Y \<Longrightarrow> xa \<in> A \<Longrightarrow> (\<Sqinter>x\<in>A. g (f x)) \<le> SUPREMUM xa g"
- by (rule_tac i = "(f xa)" in SUP_upper2, simp, rule_tac i = "xa" in INF_lower2, simp_all)
+ by (rule SUP_upper2, rule B, simp_all, simp)
show "(\<Squnion>x\<in>{f ` A |f. \<forall>Y\<in>A. f Y \<in> Y}. \<Sqinter>a\<in>x. g a) \<le> (\<Sqinter>x\<in>A. \<Squnion>a\<in>x. g a)"
apply (rule SUP_least, simp, safe, rule INF_greatest, simp)
by (rule A)
@@ -924,22 +931,38 @@
proof (cases "{} \<in> A")
case True
then show ?thesis
- by (rule_tac i = "{}" in INF_lower2, simp_all)
+ by (rule INF_lower2, simp_all)
next
case False
have [simp]: "\<And>x xa xb. xb \<in> A \<Longrightarrow> x xb \<in> xb \<Longrightarrow> (\<Sqinter>xa. if xa \<in> A then if x xa \<in> xa then g (x xa) else \<bottom> else \<top>) \<le> g (x xb)"
- by (rule_tac i = xb in INF_lower2, simp_all)
+ by (rule INF_lower2, auto)
have [simp]: " \<And>x xa y. y \<in> A \<Longrightarrow> x y \<notin> y \<Longrightarrow> (\<Sqinter>xa. if xa \<in> A then if x xa \<in> xa then g (x xa) else \<bottom> else \<top>) \<le> g (SOME x. x \<in> y)"
- by (rule_tac i = y in INF_lower2, simp_all)
+ by (rule INF_lower2, auto)
have [simp]: "\<And>x. (\<Sqinter>xa. if xa \<in> A then if x xa \<in> xa then g (x xa) else \<bottom> else \<top>) \<le> (\<Squnion>x\<in>{f ` A |f. \<forall>Y\<in>A. f Y \<in> Y}. \<Sqinter>x\<in>x. g x)"
- apply (rule_tac i = "(\<lambda> y . if x y \<in> y then x y else (SOME x . x \<in>y)) ` A" in SUP_upper2, simp)
- apply (rule_tac x = "(\<lambda> y . if x y \<in> y then x y else (SOME x . x \<in>y))" in exI, simp)
- using False some_in_eq apply auto[1]
- by (rule INF_greatest, auto)
- have "\<And>x. (\<Sqinter>x\<in>A. \<Squnion>x\<in>x. g x) \<le> (\<Squnion>xa. if x \<in> A then if xa \<in> x then g xa else \<bottom> else \<top>)"
- apply (case_tac "x \<in> A")
- apply (rule INF_lower2, simp)
- by (rule SUP_least, rule SUP_upper2, auto)
+ proof -
+ fix x
+ define F where "F = (\<lambda> (y::'b set) . if x y \<in> y then x y else (SOME x . x \<in>y))"
+ have B: "(\<forall>Y\<in>A. F Y \<in> Y)"
+ using False some_in_eq F_def by auto
+ have A: "F ` A \<in> {f ` A |f. \<forall>Y\<in>A. f Y \<in> Y}"
+ using B by blast
+ show "(\<Sqinter>xa. if xa \<in> A then if x xa \<in> xa then g (x xa) else \<bottom> else \<top>) \<le> (\<Squnion>x\<in>{f ` A |f. \<forall>Y\<in>A. f Y \<in> Y}. \<Sqinter>x\<in>x. g x)"
+ using A apply (rule SUP_upper2)
+ by (simp add: F_def, rule INF_greatest, auto)
+ qed
+
+ {fix x
+ have "(\<Sqinter>x\<in>A. \<Squnion>x\<in>x. g x) \<le> (\<Squnion>xa. if x \<in> A then if xa \<in> x then g xa else \<bottom> else \<top>)"
+ proof (cases "x \<in> A")
+ case True
+ then show ?thesis
+ apply (rule INF_lower2, simp_all)
+ by (rule SUP_least, rule SUP_upper2, auto)
+ next
+ case False
+ then show ?thesis by simp
+ qed
+ }
from this have "(\<Sqinter>x\<in>A. \<Squnion>a\<in>x. g a) \<le> (\<Sqinter>x. \<Squnion>xa. if x \<in> A then if xa \<in> x then g xa else \<bottom> else \<top>)"
by (rule INF_greatest)
also have "... = (\<Squnion>x. \<Sqinter>xa. if xa \<in> A then if x xa \<in> xa then g (x xa) else \<bottom> else \<top>)"
@@ -1020,10 +1043,14 @@
from this have B: " (\<forall>xa \<in> F ` A. x \<in> xa)"
apply (safe, simp add: F_def)
by (rule someI2_ex, auto)
-
+
+ have C: "(\<forall>Y\<in>A. F Y \<in> Y)"
+ apply (simp add: F_def, safe)
+ apply (rule someI2_ex)
+ using A by auto
+
have "(\<exists>f. F ` A = f ` A \<and> (\<forall>Y\<in>A. f Y \<in> Y))"
- apply (rule_tac x = "F" in exI, simp add: F_def, safe)
- using A by (rule_tac someI2_ex, auto)
+ using C by blast
from B and this show "\<exists>X. (\<exists>f. X = f ` A \<and> (\<forall>Y\<in>A. f Y \<in> Y)) \<and> (\<forall>xa\<in>X. x \<in> xa)"
by auto
@@ -1063,10 +1090,13 @@
define F where "F = (\<lambda> Y . SOME k . k \<in> Y \<and> z < k)"
have D: "\<And> Y . Y \<in> A \<Longrightarrow> z < F Y"
- using B by (simp add: F_def, rule_tac someI2_ex, auto)
+ using B apply (simp add: F_def)
+ by (rule someI2_ex, auto)
+
have E: "\<And> Y . Y \<in> A \<Longrightarrow> F Y \<in> Y"
- using B by (simp add: F_def, rule_tac someI2_ex, auto)
+ using B apply (simp add: F_def)
+ by (rule someI2_ex, auto)
have "z \<le> Inf (F ` A)"
by (simp add: D local.INF_greatest local.order.strict_implies_order)
@@ -1093,10 +1123,12 @@
define F where "F = (\<lambda> Y . SOME k . k \<in> Y \<and> SUPREMUM {f ` A |f. \<forall>Y\<in>A. f Y \<in> Y} Inf < k)"
have D: "\<And> Y . Y \<in> A \<Longrightarrow> SUPREMUM {f ` A |f. \<forall>Y\<in>A. f Y \<in> Y} Inf < F Y"
- using B by (simp add: F_def, rule_tac someI2_ex, auto)
+ using B apply (simp add: F_def)
+ by (rule someI2_ex, auto)
have E: "\<And> Y . Y \<in> A \<Longrightarrow> F Y \<in> Y"
- using B by (simp add: F_def, rule_tac someI2_ex, auto)
+ using B apply (simp add: F_def)
+ by (rule someI2_ex, auto)
have "\<And> Y . Y \<in> A \<Longrightarrow> INFIMUM A Sup \<le> F Y"
using D False local.leI by blast
@@ -1112,7 +1144,7 @@
by simp
from C and this show ?thesis
- using local.not_less by blast
+ using not_less by blast
qed
qed
end
--- a/src/HOL/Library/Option_ord.thy Mon Mar 26 19:13:45 2018 +0200
+++ b/src/HOL/Library/Option_ord.thy Mon Mar 26 23:58:43 2018 +0200
@@ -287,7 +287,7 @@
proof (cases "{} \<in> A")
case True
then show ?thesis
- by (rule_tac i = "{}" in INF_lower2, simp_all)
+ by (rule INF_lower2, simp_all)
next
case False
from this have X: "{} \<notin> A"
@@ -296,37 +296,41 @@
proof (cases "{None} \<in> A")
case True
then show ?thesis
- by (rule_tac i = "{None}" in INF_lower2, simp_all)
+ by (rule INF_lower2, simp_all)
next
case False
- have "\<And> y . y\<in>A \<Longrightarrow> Sup (y - {None}) = Sup y"
- by (metis (no_types, lifting) Sup_option_def insert_Diff_single these_insert_None these_not_empty_eq)
-
+
+ {fix y
+ assume A: "y \<in> A"
+ have "Sup (y - {None}) = Sup y"
+ by (metis (no_types, lifting) Sup_option_def insert_Diff_single these_insert_None these_not_empty_eq)
+ from A and this have "(\<exists>z. y - {None} = z - {None} \<and> z \<in> A) \<and> \<Squnion>y = \<Squnion>(y - {None})"
+ by auto
+ }
from this have A: "Sup ` A = (Sup ` {y - {None} | y. y\<in>A})"
- apply (simp add: image_def, simp, safe)
- apply (rule_tac x = "xa - {None}" in exI, simp, blast)
- by blast
+ by (auto simp add: image_def)
have [simp]: "\<And>y. y \<in> A \<Longrightarrow> \<exists>ya. {ya. \<exists>x. x \<in> y \<and> (\<exists>y. x = Some y) \<and> ya = the x}
= {y. \<exists>x\<in>ya - {None}. y = the x} \<and> ya \<in> A"
- by (rule_tac x = "y" in exI, auto)
+ by (rule exI, auto)
have [simp]: "\<And>y. y \<in> A \<Longrightarrow>
(\<exists>ya. y - {None} = ya - {None} \<and> ya \<in> A) \<and> \<Squnion>{ya. \<exists>x\<in>y - {None}. ya = the x}
= \<Squnion>{ya. \<exists>x. x \<in> y \<and> (\<exists>y. x = Some y) \<and> ya = the x}"
- apply safe
- apply blast
- apply (rule_tac f = Sup in arg_cong)
- by auto
-
- have C: "(\<lambda>x. (\<Squnion>Option.these x)) ` {y - {None} |y. y \<in> A} = (Sup ` {the ` (y - {None}) |y. y \<in> A})"
- apply (simp add: image_def Option.these_def, safe)
- apply (rule_tac x = "{ya. \<exists>x. x \<in> y - {None} \<and> (\<exists>y. x = Some y) \<and> ya = the x}" in exI, simp)
- by (rule_tac x = "y -{None}" in exI, simp)
+ apply (safe, blast)
+ by (rule arg_cong [of _ _ Sup], auto)
+ {fix y
+ assume [simp]: "y \<in> A"
+ have "\<exists>x. (\<exists>y. x = {ya. \<exists>x\<in>y - {None}. ya = the x} \<and> y \<in> A) \<and> \<Squnion>{ya. \<exists>x. x \<in> y \<and> (\<exists>y. x = Some y) \<and> ya = the x} = \<Squnion>x"
+ and "\<exists>x. (\<exists>y. x = y - {None} \<and> y \<in> A) \<and> \<Squnion>{ya. \<exists>x\<in>y - {None}. ya = the x} = \<Squnion>{y. \<exists>xa. xa \<in> x \<and> (\<exists>y. xa = Some y) \<and> y = the xa}"
+ apply (rule exI [of _ "{ya. \<exists>x. x \<in> y \<and> (\<exists>y. x = Some y) \<and> ya = the x}"], simp)
+ by (rule exI [of _ "y - {None}"], simp)
+ }
+ from this have C: "(\<lambda>x. (\<Squnion>Option.these x)) ` {y - {None} |y. y \<in> A} = (Sup ` {the ` (y - {None}) |y. y \<in> A})"
+ by (simp add: image_def Option.these_def, safe, simp_all)
have D: "\<forall> f . \<exists>Y\<in>A. f Y \<notin> Y \<Longrightarrow> False"
- apply (drule_tac x = "\<lambda> Y . SOME x . x \<in> Y" in spec, safe)
- by (simp add: X some_in_eq)
+ by (drule spec [of _ "\<lambda> Y . SOME x . x \<in> Y"], simp add: X some_in_eq)
define F where "F = (\<lambda> Y . SOME x::'a option . x \<in> (Y - {None}))"
@@ -341,12 +345,13 @@
less_eq_option_Some singletonI)
from this have "Inf (F ` A) \<noteq> None"
- by (case_tac "\<Sqinter>x\<in>A. F x", simp_all)
-
+ by (cases "\<Sqinter>x\<in>A. F x", simp_all)
+
+ from this have "Inf (F ` A) \<noteq> None \<and> Inf (F ` A) \<in> Inf ` {f ` A |f. \<forall>Y\<in>A. f Y \<in> Y}"
+ using F by auto
+
from this have "\<exists> x . x \<noteq> None \<and> x \<in> Inf ` {f ` A |f. \<forall>Y\<in>A. f Y \<in> Y}"
- apply (rule_tac x = "Inf (F ` A)" in exI, simp add: image_def, safe)
- apply (rule_tac x = "F ` A" in exI, safe)
- using F by auto
+ by blast
from this have E:" Inf ` {f ` A |f. \<forall>Y\<in>A. f Y \<in> Y} = {None} \<Longrightarrow> False"
by blast
@@ -358,36 +363,59 @@
have B: "Option.these ((\<lambda>x. Some (\<Squnion>Option.these x)) ` {y - {None} |y. y \<in> A})
= ((\<lambda>x. (\<Squnion> Option.these x)) ` {y - {None} |y. y \<in> A})"
by (metis image_image these_image_Some_eq)
+ {
+ fix f
+ assume A: "\<And> Y . (\<exists>y. Y = the ` (y - {None}) \<and> y \<in> A) \<Longrightarrow> f Y \<in> Y"
- have [simp]: "\<And>f. \<forall>Y. (\<exists>y. Y = {ya. \<exists>x\<in>y - {None}. ya = the x} \<and> y \<in> A) \<longrightarrow> f Y \<in> Y \<Longrightarrow>
- \<exists>x. (\<exists>f. x = {y. \<exists>x\<in>A. y = f x} \<and> (\<forall>Y\<in>A. f Y \<in> Y)) \<and> (\<Sqinter>x\<in>A. Some (f {y. \<exists>x\<in>x - {None}. y = the x})) = \<Sqinter>x"
- apply (rule_tac x = "{Some (f {y. \<exists>a\<in>x - {None}. y = the a}) | x . x\<in> A}" in exI, safe)
- apply (rule_tac x = "(\<lambda> Y . Some (f (the ` (Y - {None})))) " in exI, safe)
- apply (rule_tac x = xa in bexI, simp add: image_def, simp)
- apply (rule_tac x = xa in exI, simp add: image_def)
- apply(drule_tac x = "(the ` (Y - {None}))" in spec)
- apply (simp add: image_def,safe, simp)
- using option.collapse apply fastforce
- by (simp add: Setcompr_eq_image)
+ have "\<And>xa. xa \<in> A \<Longrightarrow> f {y. \<exists>a\<in>xa - {None}. y = the a} = f (the ` (xa - {None}))"
+ by (simp add: image_def)
+ from this have [simp]: "\<And>xa. xa \<in> A \<Longrightarrow> \<exists>x\<in>A. f {y. \<exists>a\<in>xa - {None}. y = the a} = f (the ` (x - {None}))"
+ by blast
+ have "\<And>xa. xa \<in> A \<Longrightarrow> f (the ` (xa - {None})) = f {y. \<exists>a \<in> xa - {None}. y = the a} \<and> xa \<in> A"
+ by (simp add: image_def)
+ from this have [simp]: "\<And>xa. xa \<in> A \<Longrightarrow> \<exists>x. f (the ` (xa - {None})) = f {y. \<exists>a\<in>x - {None}. y = the a} \<and> x \<in> A"
+ by blast
- have [simp]: "\<And>f. \<forall>Y. (\<exists>y. Y = {ya. \<exists>x\<in>y - {None}. ya = the x} \<and> y \<in> A) \<longrightarrow> f Y \<in> Y
- \<Longrightarrow> \<exists>y. (\<Sqinter>x\<in>A. Some (f {y. \<exists>x\<in>x - {None}. y = the x})) = Some y"
- by (metis (no_types) Some_INF)
+ {
+ fix Y
+ have "Y \<in> A \<Longrightarrow> Some (f (the ` (Y - {None}))) \<in> Y"
+ using A [of "the ` (Y - {None})"] apply (simp add: image_def)
+ using option.collapse by fastforce
+ }
+ from this have [simp]: "\<And> Y . Y \<in> A \<Longrightarrow> Some (f (the ` (Y - {None}))) \<in> Y"
+ by blast
+ have [simp]: "(\<Sqinter>x\<in>A. Some (f {y. \<exists>x\<in>x - {None}. y = the x})) = \<Sqinter>{Some (f {y. \<exists>a\<in>x - {None}. y = the a}) |x. x \<in> A}"
+ by (simp add: Setcompr_eq_image)
+
+ have [simp]: "\<exists>x. (\<exists>f. x = {y. \<exists>x\<in>A. y = f x} \<and> (\<forall>Y\<in>A. f Y \<in> Y)) \<and> \<Sqinter>{Some (f {y. \<exists>a\<in>x - {None}. y = the a}) |x. x \<in> A} = \<Sqinter>x"
+ apply (rule exI [of _ "{Some (f {y. \<exists>a\<in>x - {None}. y = the a}) | x . x\<in> A}"], safe)
+ by (rule exI [of _ "(\<lambda> Y . Some (f (the ` (Y - {None})))) "], safe, simp_all)
- have [simp]: "\<And> f.
- (\<Sqinter>x\<in>{the ` (y - {None}) |y. y \<in> A}. f x) \<le> the (\<Sqinter>Y\<in>A. Some (f (the ` (Y - {None}))))"
- apply (simp add: Inf_option_def, safe)
- apply (rule Inf_greatest, simp add: image_def Option.these_def, safe)
- apply (rule_tac i = " {y. \<exists>x\<in>xb - {None}. y = the x}" in INF_lower2)
- apply simp_all
+ {
+ fix xb
+ have "xb \<in> A \<Longrightarrow> (\<Sqinter>x\<in>{{ya. \<exists>x\<in>y - {None}. ya = the x} |y. y \<in> A}. f x) \<le> f {y. \<exists>x\<in>xb - {None}. y = the x}"
+ apply (rule INF_lower2 [of "{y. \<exists>x\<in>xb - {None}. y = the x}"])
+ by blast+
+ }
+ from this have [simp]: "(\<Sqinter>x\<in>{the ` (y - {None}) |y. y \<in> A}. f x) \<le> the (\<Sqinter>Y\<in>A. Some (f (the ` (Y - {None}))))"
+ apply (simp add: Inf_option_def image_def Option.these_def)
+ by (rule Inf_greatest, clarsimp)
+
+ have [simp]: "the (\<Sqinter>Y\<in>A. Some (f (the ` (Y - {None})))) \<in> Option.these (Inf ` {f ` A |f. \<forall>Y\<in>A. f Y \<in> Y})"
+ apply (simp add: Option.these_def image_def)
+ apply (rule exI [of _ "(\<Sqinter>x\<in>A. Some (f {y. \<exists>x\<in>x - {None}. y = the x}))"], simp)
+ by (simp add: Inf_option_def)
+
+ have "(\<Sqinter>x\<in>{the ` (y - {None}) |y. y \<in> A}. f x) \<le> \<Squnion>Option.these (Inf ` {f ` A |f. \<forall>Y\<in>A. f Y \<in> Y})"
+ by (rule Sup_upper2 [of "the (Inf ((\<lambda> Y . Some (f (the ` (Y - {None})) )) ` A))"], simp_all)
+ }
+ from this have X: "\<And> f . \<forall>Y. (\<exists>y. Y = the ` (y - {None}) \<and> y \<in> A) \<longrightarrow> f Y \<in> Y \<Longrightarrow>
+ (\<Sqinter>x\<in>{the ` (y - {None}) |y. y \<in> A}. f x) \<le> \<Squnion>Option.these (Inf ` {f ` A |f. \<forall>Y\<in>A. f Y \<in> Y})"
by blast
+
- have X: "\<And> f . \<forall>Y. (\<exists>y. Y = the ` (y - {None}) \<and> y \<in> A) \<longrightarrow> f Y \<in> Y
- \<Longrightarrow> (\<Sqinter>x\<in>{the ` (y - {None}) |y. y \<in> A}. f x) \<le> \<Squnion>Option.these (Inf ` {f ` A |f. \<forall>Y\<in>A. f Y \<in> Y})"
- apply (rule_tac u = "the (Inf ((\<lambda> Y . Some (f (the ` (Y - {None})) )) ` A))" in Sup_upper2)
- apply (simp add: Option.these_def image_def)
- apply (rule_tac x = "(\<Sqinter>x\<in>A. Some (f {y. \<exists>x\<in>x - {None}. y = the x}))" in exI, simp)
- by simp
+ have [simp]: "\<And> x . x\<in>{y - {None} |y. y \<in> A} \<Longrightarrow> x \<noteq> {} \<and> x \<noteq> {None}"
+ using F by fastforce
have "(Inf (Sup `A)) = (Inf (Sup ` {y - {None} | y. y\<in>A}))"
by (subst A, simp)
@@ -396,7 +424,6 @@
by (simp add: Sup_option_def)
also have "... = (\<Sqinter>x\<in>{y - {None} |y. y \<in> A}. Some (\<Squnion>Option.these x))"
- apply (subgoal_tac "\<And> x . x\<in>{y - {None} |y. y \<in> A} \<Longrightarrow> x \<noteq> {} \<and> x \<noteq> {None}", simp)
using G by fastforce
also have "... = Some (\<Sqinter>Option.these ((\<lambda>x. Some (\<Squnion>Option.these x)) ` {y - {None} |y. y \<in> A}))"
@@ -412,12 +439,18 @@
by (simp add: Inf_Sup)
also have "... \<le> SUPREMUM {f ` A |f. \<forall>Y\<in>A. f Y \<in> Y} Inf"
- apply (simp add: less_eq_option_def)
- apply (case_tac "\<Squnion>x\<in>{f ` A |f. \<forall>Y\<in>A. f Y \<in> Y}. \<Sqinter>x", simp_all)
- apply (rule Sup_least, safe)
- apply (simp add: Sup_option_def)
- apply (case_tac "(\<forall>f. \<exists>Y\<in>A. f Y \<notin> Y) \<or> Inf ` {f ` A |f. \<forall>Y\<in>A. f Y \<in> Y} = {None}", simp_all)
- by (drule X, simp)
+ proof (cases "SUPREMUM {f ` A |f. \<forall>Y\<in>A. f Y \<in> Y} Inf")
+ case None
+ then show ?thesis by (simp add: less_eq_option_def)
+ next
+ case (Some a)
+ then show ?thesis
+ apply simp
+ apply (rule Sup_least, safe)
+ apply (simp add: Sup_option_def)
+ apply (cases "(\<forall>f. \<exists>Y\<in>A. f Y \<notin> Y) \<or> Inf ` {f ` A |f. \<forall>Y\<in>A. f Y \<in> Y} = {None}", simp_all)
+ by (drule X, simp)
+ qed
finally show ?thesis by simp
qed
qed
--- a/src/HOL/Limits.thy Mon Mar 26 19:13:45 2018 +0200
+++ b/src/HOL/Limits.thy Mon Mar 26 23:58:43 2018 +0200
@@ -1113,6 +1113,10 @@
lemma filterlim_norm_at_top: "filterlim norm at_top at_infinity"
by (rule filterlim_at_infinity_imp_norm_at_top) (rule filterlim_ident)
+lemma filterlim_at_infinity_conv_norm_at_top:
+ "filterlim f at_infinity G \<longleftrightarrow> filterlim (\<lambda>x. norm (f x)) at_top G"
+ by (auto simp: filterlim_at_infinity[OF order.refl] filterlim_at_top_gt[of _ _ 0])
+
lemma eventually_not_equal_at_infinity:
"eventually (\<lambda>x. x \<noteq> (a :: 'a :: {real_normed_vector})) at_infinity"
proof -
@@ -1322,6 +1326,28 @@
and filterlim_compose[OF filterlim_uminus_at_top_at_bot, of "\<lambda>x. - f x" F]
by auto
+lemma filterlim_at_infinity_imp_filterlim_at_top:
+ assumes "filterlim (f :: 'a \<Rightarrow> real) at_infinity F"
+ assumes "eventually (\<lambda>x. f x > 0) F"
+ shows "filterlim f at_top F"
+proof -
+ from assms(2) have *: "eventually (\<lambda>x. norm (f x) = f x) F" by eventually_elim simp
+ from assms(1) show ?thesis unfolding filterlim_at_infinity_conv_norm_at_top
+ by (subst (asm) filterlim_cong[OF refl refl *])
+qed
+
+lemma filterlim_at_infinity_imp_filterlim_at_bot:
+ assumes "filterlim (f :: 'a \<Rightarrow> real) at_infinity F"
+ assumes "eventually (\<lambda>x. f x < 0) F"
+ shows "filterlim f at_bot F"
+proof -
+ from assms(2) have *: "eventually (\<lambda>x. norm (f x) = -f x) F" by eventually_elim simp
+ from assms(1) have "filterlim (\<lambda>x. - f x) at_top F"
+ unfolding filterlim_at_infinity_conv_norm_at_top
+ by (subst (asm) filterlim_cong[OF refl refl *])
+ thus ?thesis by (simp add: filterlim_uminus_at_top)
+qed
+
lemma filterlim_uminus_at_bot: "(LIM x F. f x :> at_bot) \<longleftrightarrow> (LIM x F. - (f x) :: real :> at_top)"
unfolding filterlim_uminus_at_top by simp
--- a/src/HOL/Predicate.thy Mon Mar 26 19:13:45 2018 +0200
+++ b/src/HOL/Predicate.thy Mon Mar 26 23:58:43 2018 +0200
@@ -110,9 +110,10 @@
define F where "F = (\<lambda> x . SOME f . f \<in> x \<and> eval f w)"
have [simp]: "(\<forall>f\<in> (F ` A). eval f w)"
by (metis (no_types, lifting) A F_def image_iff some_eq_ex)
- show "\<exists>x. (\<exists>f. x = f ` A \<and> (\<forall>Y\<in>A. f Y \<in> Y)) \<and> (\<forall>f\<in>x. eval f w)"
- apply (rule_tac x = "F ` A" in exI, simp)
- using A by (metis (no_types, lifting) F_def someI)+
+ have "(\<exists>f. F ` A = f ` A \<and> (\<forall>Y\<in>A. f Y \<in> Y)) \<and> (\<forall>f\<in>(F ` A). eval f w)"
+ using A by (simp, metis (no_types, lifting) F_def someI)+
+ from this show "\<exists>x. (\<exists>f. x = f ` A \<and> (\<forall>Y\<in>A. f Y \<in> Y)) \<and> (\<forall>f\<in>x. eval f w)"
+ by (rule exI [of _ "F ` A"])
qed
qed (auto intro!: pred_eqI)
--- a/src/HOL/Topological_Spaces.thy Mon Mar 26 19:13:45 2018 +0200
+++ b/src/HOL/Topological_Spaces.thy Mon Mar 26 23:58:43 2018 +0200
@@ -743,10 +743,18 @@
lemma tendsto_const [tendsto_intros, simp, intro]: "((\<lambda>x. k) \<longlongrightarrow> k) F"
by (simp add: tendsto_def)
-lemma filterlim_at:
+lemma filterlim_at:
"(LIM x F. f x :> at b within s) \<longleftrightarrow> eventually (\<lambda>x. f x \<in> s \<and> f x \<noteq> b) F \<and> (f \<longlongrightarrow> b) F"
by (simp add: at_within_def filterlim_inf filterlim_principal conj_commute)
+lemma (in -)
+ assumes "filterlim f (nhds L) F"
+ shows tendsto_imp_filterlim_at_right:
+ "eventually (\<lambda>x. f x > L) F \<Longrightarrow> filterlim f (at_right L) F"
+ and tendsto_imp_filterlim_at_left:
+ "eventually (\<lambda>x. f x < L) F \<Longrightarrow> filterlim f (at_left L) F"
+ using assms by (auto simp: filterlim_at elim: eventually_mono)
+
lemma filterlim_at_withinI:
assumes "filterlim f (nhds c) F"
assumes "eventually (\<lambda>x. f x \<in> A - {c}) F"