author Manuel Eberl Mon, 26 Mar 2018 23:58:43 +0200 changeset 67952 120c96286336 parent 67949 4bb49ed64933 (current diff) parent 67951 655aa11359dc (diff) child 67953 f646d1c826a1
Merged
```--- 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"
+  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>"
@@ -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"
also have "... = a \<sqinter> x \<squnion> \<Squnion>{a \<sqinter> b |b. b \<in> F}"
+    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 @@

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"
```
```--- 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"
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)"
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
+      have "\<And>xa. xa \<in> A \<Longrightarrow> f {y. \<exists>a\<in>xa - {None}. y = the a} = f (the ` (xa - {None}))"
+      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"
+      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}"
+
+      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)
+
+      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 @@

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 @@

also have "... \<le> SUPREMUM {f ` A |f. \<forall>Y\<in>A. f Y \<in> Y} Inf"
-      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 (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 (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"

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