author wenzelm Fri, 27 May 2016 23:35:13 +0200 changeset 63171 a0088f1c049d parent 63170 eae6549dbea2 child 63172 d4f459eb7ed0
tuned proofs;
 src/HOL/Conditionally_Complete_Lattices.thy file | annotate | diff | comparison | revisions src/HOL/Set.thy file | annotate | diff | comparison | revisions src/HOL/Set_Interval.thy file | annotate | diff | comparison | revisions src/HOL/Topological_Spaces.thy file | annotate | diff | comparison | revisions
```--- a/src/HOL/Conditionally_Complete_Lattices.thy	Fri May 27 20:23:55 2016 +0200
+++ b/src/HOL/Conditionally_Complete_Lattices.thy	Fri May 27 23:35:13 2016 +0200
@@ -631,7 +631,7 @@
qed
ultimately show ?thesis
unfolding greaterThanAtMost_def greaterThanLessThan_def atLeastAtMost_def atLeastLessThan_def
-    by (elim exE disjE) auto
+    by (metis inf_bot_left inf_bot_right inf_top.left_neutral inf_top.right_neutral)
qed

lemma cSUP_eq_cINF_D:```
```--- a/src/HOL/Set.thy	Fri May 27 20:23:55 2016 +0200
+++ b/src/HOL/Set.thy	Fri May 27 23:35:13 2016 +0200
@@ -1596,7 +1596,7 @@
by (auto simp add: Pow_def)

lemma Pow_singleton_iff [simp]: "Pow X = {Y} \<longleftrightarrow> X = {} \<and> Y = {}"
-by blast
+  by blast

lemma Pow_insert: "Pow (insert a A) = Pow A \<union> (insert a ` Pow A)"
by (blast intro: image_eqI [where ?x = "u - {a}" for u])```
```--- a/src/HOL/Set_Interval.thy	Fri May 27 20:23:55 2016 +0200
+++ b/src/HOL/Set_Interval.thy	Fri May 27 23:35:13 2016 +0200
@@ -1071,7 +1071,7 @@
qed
qed
next
-  show "?B <= ?A" by auto
+  show "?B <= ?A" by fastforce
qed

```--- a/src/HOL/Topological_Spaces.thy	Fri May 27 20:23:55 2016 +0200
+++ b/src/HOL/Topological_Spaces.thy	Fri May 27 23:35:13 2016 +0200
@@ -331,7 +331,7 @@
have *: "{False <..} = {True}" "{..< True} = {False}"
by auto
have "A = UNIV \<or> A = {} \<or> A = {False <..} \<or> A = {..< True}"
-    using subset_UNIV[of A] unfolding UNIV_bool * by auto
+    using subset_UNIV[of A] unfolding UNIV_bool * by blast
then show "open A"
by auto
qed
@@ -1194,7 +1194,7 @@
fix S assume "open S" "x \<in> S"
from incl[OF this] obtain i where "F i \<subseteq> S" unfolding F_def by auto
moreover have "\<And>j. i \<le> j \<Longrightarrow> F j \<subseteq> F i"
-      by (auto simp: F_def)
+      by (simp add: Inf_superset_mono F_def image_mono)
ultimately show "eventually (\<lambda>i. F i \<subseteq> S) sequentially"
by (auto simp: eventually_sequentially)
qed
@@ -1210,7 +1210,7 @@
show thesis
proof
show "decseq (\<lambda>n. \<Inter>i\<le>n. A i)"
-      by (auto simp: decseq_def)
+      by (simp add: antimono_iff_le_Suc atMost_Suc)
show "\<And>n. x \<in> (\<Inter>i\<le>n. A i)" "\<And>n. open (\<Inter>i\<le>n. A i)"
using A by auto
show "nhds x = (INF n. principal (\<Inter>i\<le>n. A i))"
@@ -1735,7 +1735,7 @@

lemma continuous_within_compose3:
"isCont g (f x) \<Longrightarrow> continuous (at x within s) f \<Longrightarrow> continuous (at x within s) (\<lambda>x. g (f x))"
-  using continuous_within_compose2[of x s f g] by (simp add: continuous_at_imp_continuous_at_within)
+  using continuous_at_imp_continuous_at_within continuous_within_compose2 by blast

lemma filtermap_nhds_open_map:
assumes cont: "isCont f a" and open_map: "\<And>S. open S \<Longrightarrow> open (f`S)"
@@ -2091,7 +2091,7 @@
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
+    by meson
then have "t \<inter> S = {} \<or> f \<inter> S = {}"
by (intro connectedD[OF \<open>connected S\<close>])  auto
then show "\<exists>c. \<forall>s\<in>S. P s = c"
@@ -2253,7 +2253,7 @@
using open_right[OF \<open>open A\<close> \<open>?z \<in> A\<close> \<open>?z < y\<close>] by auto
moreover obtain b where "b \<in> B" "x < b" "b < min a y"
using cInf_less_iff[of "B \<inter> {x <..}" "min a y"] \<open>?z < a\<close> \<open>?z < y\<close> \<open>x < y\<close> \<open>y \<in> B\<close>
-        by (auto intro: less_imp_le)
+        by auto
moreover have "?z \<le> b"
using \<open>b \<in> B\<close> \<open>x < b\<close>
by (intro cInf_lower) auto
@@ -2593,7 +2593,7 @@
by (auto simp add: totally_bounded_def)

lemma totally_bounded_subset: "totally_bounded S \<Longrightarrow> T \<subseteq> S \<Longrightarrow> totally_bounded T"
-  by (force simp add: totally_bounded_def)
+  by (fastforce simp add: totally_bounded_def)

lemma totally_bounded_Union[intro]:
assumes M: "finite M" "\<And>S. S \<in> M \<Longrightarrow> totally_bounded S" shows "totally_bounded (\<Union>M)"```