tuned proofs;
authorwenzelm
Fri May 27 23:35:13 2016 +0200 (2016-05-27)
changeset 63171a0088f1c049d
parent 63170 eae6549dbea2
child 63172 d4f459eb7ed0
tuned proofs;
src/HOL/Conditionally_Complete_Lattices.thy
src/HOL/Set.thy
src/HOL/Set_Interval.thy
src/HOL/Topological_Spaces.thy
     1.1 --- a/src/HOL/Conditionally_Complete_Lattices.thy	Fri May 27 20:23:55 2016 +0200
     1.2 +++ b/src/HOL/Conditionally_Complete_Lattices.thy	Fri May 27 23:35:13 2016 +0200
     1.3 @@ -631,7 +631,7 @@
     1.4    qed
     1.5    ultimately show ?thesis
     1.6      unfolding greaterThanAtMost_def greaterThanLessThan_def atLeastAtMost_def atLeastLessThan_def
     1.7 -    by (elim exE disjE) auto
     1.8 +    by (metis inf_bot_left inf_bot_right inf_top.left_neutral inf_top.right_neutral)
     1.9  qed
    1.10  
    1.11  lemma cSUP_eq_cINF_D:
     2.1 --- a/src/HOL/Set.thy	Fri May 27 20:23:55 2016 +0200
     2.2 +++ b/src/HOL/Set.thy	Fri May 27 23:35:13 2016 +0200
     2.3 @@ -1596,7 +1596,7 @@
     2.4    by (auto simp add: Pow_def)
     2.5  
     2.6  lemma Pow_singleton_iff [simp]: "Pow X = {Y} \<longleftrightarrow> X = {} \<and> Y = {}"
     2.7 -by blast
     2.8 +  by blast
     2.9  
    2.10  lemma Pow_insert: "Pow (insert a A) = Pow A \<union> (insert a ` Pow A)"
    2.11    by (blast intro: image_eqI [where ?x = "u - {a}" for u])
     3.1 --- a/src/HOL/Set_Interval.thy	Fri May 27 20:23:55 2016 +0200
     3.2 +++ b/src/HOL/Set_Interval.thy	Fri May 27 23:35:13 2016 +0200
     3.3 @@ -1071,7 +1071,7 @@
     3.4      qed
     3.5    qed
     3.6  next
     3.7 -  show "?B <= ?A" by auto
     3.8 +  show "?B <= ?A" by fastforce
     3.9  qed
    3.10  
    3.11  lemma UN_le_add_shift:
     4.1 --- a/src/HOL/Topological_Spaces.thy	Fri May 27 20:23:55 2016 +0200
     4.2 +++ b/src/HOL/Topological_Spaces.thy	Fri May 27 23:35:13 2016 +0200
     4.3 @@ -331,7 +331,7 @@
     4.4    have *: "{False <..} = {True}" "{..< True} = {False}"
     4.5      by auto
     4.6    have "A = UNIV \<or> A = {} \<or> A = {False <..} \<or> A = {..< True}"
     4.7 -    using subset_UNIV[of A] unfolding UNIV_bool * by auto
     4.8 +    using subset_UNIV[of A] unfolding UNIV_bool * by blast
     4.9    then show "open A"
    4.10      by auto
    4.11  qed
    4.12 @@ -1194,7 +1194,7 @@
    4.13      fix S assume "open S" "x \<in> S"
    4.14      from incl[OF this] obtain i where "F i \<subseteq> S" unfolding F_def by auto
    4.15      moreover have "\<And>j. i \<le> j \<Longrightarrow> F j \<subseteq> F i"
    4.16 -      by (auto simp: F_def)
    4.17 +      by (simp add: Inf_superset_mono F_def image_mono)
    4.18      ultimately show "eventually (\<lambda>i. F i \<subseteq> S) sequentially"
    4.19        by (auto simp: eventually_sequentially)
    4.20    qed
    4.21 @@ -1210,7 +1210,7 @@
    4.22    show thesis
    4.23    proof
    4.24      show "decseq (\<lambda>n. \<Inter>i\<le>n. A i)"
    4.25 -      by (auto simp: decseq_def)
    4.26 +      by (simp add: antimono_iff_le_Suc atMost_Suc)
    4.27      show "\<And>n. x \<in> (\<Inter>i\<le>n. A i)" "\<And>n. open (\<Inter>i\<le>n. A i)"
    4.28        using A by auto
    4.29      show "nhds x = (INF n. principal (\<Inter>i\<le>n. A i))"
    4.30 @@ -1735,7 +1735,7 @@
    4.31  
    4.32  lemma continuous_within_compose3:
    4.33    "isCont g (f x) \<Longrightarrow> continuous (at x within s) f \<Longrightarrow> continuous (at x within s) (\<lambda>x. g (f x))"
    4.34 -  using continuous_within_compose2[of x s f g] by (simp add: continuous_at_imp_continuous_at_within)
    4.35 +  using continuous_at_imp_continuous_at_within continuous_within_compose2 by blast
    4.36  
    4.37  lemma filtermap_nhds_open_map:
    4.38    assumes cont: "isCont f a" and open_map: "\<And>S. open S \<Longrightarrow> open (f`S)"
    4.39 @@ -2091,7 +2091,7 @@
    4.40      unfolding continuous_on_open_invariant by (simp add: open_discrete)
    4.41    from this[of True] this[of False]
    4.42    obtain t f where "open t" "open f" and *: "f \<inter> S = P -` {False} \<inter> S" "t \<inter> S = P -` {True} \<inter> S"
    4.43 -    by auto
    4.44 +    by meson
    4.45    then have "t \<inter> S = {} \<or> f \<inter> S = {}"
    4.46      by (intro connectedD[OF \<open>connected S\<close>])  auto
    4.47    then show "\<exists>c. \<forall>s\<in>S. P s = c"
    4.48 @@ -2253,7 +2253,7 @@
    4.49          using open_right[OF \<open>open A\<close> \<open>?z \<in> A\<close> \<open>?z < y\<close>] by auto
    4.50        moreover obtain b where "b \<in> B" "x < b" "b < min a y"
    4.51          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>
    4.52 -        by (auto intro: less_imp_le)
    4.53 +        by auto
    4.54        moreover have "?z \<le> b"
    4.55          using \<open>b \<in> B\<close> \<open>x < b\<close>
    4.56          by (intro cInf_lower) auto
    4.57 @@ -2593,7 +2593,7 @@
    4.58    by (auto simp add: totally_bounded_def)
    4.59  
    4.60  lemma totally_bounded_subset: "totally_bounded S \<Longrightarrow> T \<subseteq> S \<Longrightarrow> totally_bounded T"
    4.61 -  by (force simp add: totally_bounded_def)
    4.62 +  by (fastforce simp add: totally_bounded_def)
    4.63  
    4.64  lemma totally_bounded_Union[intro]:
    4.65    assumes M: "finite M" "\<And>S. S \<in> M \<Longrightarrow> totally_bounded S" shows "totally_bounded (\<Union>M)"