tidying more messy proofs
authorpaulson <lp15@cam.ac.uk>
Tue May 08 10:32:07 2018 +0100 (13 months ago)
changeset 681202f161c6910f7
parent 68097 5f3cffe16311
child 68121 6e0991ddf0ca
tidying more messy proofs
src/HOL/Analysis/Equivalence_Lebesgue_Henstock_Integration.thy
src/HOL/Analysis/Henstock_Kurzweil_Integration.thy
src/HOL/Analysis/Lebesgue_Measure.thy
src/HOL/Analysis/Ordered_Euclidean_Space.thy
src/HOL/Analysis/Path_Connected.thy
src/HOL/Analysis/Tagged_Division.thy
src/HOL/Analysis/Topology_Euclidean_Space.thy
     1.1 --- a/src/HOL/Analysis/Equivalence_Lebesgue_Henstock_Integration.thy	Sun May 06 23:59:14 2018 +0100
     1.2 +++ b/src/HOL/Analysis/Equivalence_Lebesgue_Henstock_Integration.thy	Tue May 08 10:32:07 2018 +0100
     1.3 @@ -1978,7 +1978,7 @@
     1.4    and   measure_countable_negligible_Union_bounded:    "(\<lambda>n. (measure lebesgue (S n))) sums measure lebesgue (\<Union>n. S n)" (is ?Sums)
     1.5  proof -
     1.6    obtain a b where ab: "(\<Union>n. S n) \<subseteq> cbox a b"
     1.7 -    using bo bounded_subset_cbox by blast
     1.8 +    using bo bounded_subset_cbox_symmetric by metis
     1.9    then have B: "(\<Sum>k\<le>n. measure lebesgue (S k)) \<le> measure lebesgue (cbox a b)" for n
    1.10    proof -
    1.11      have "(\<Sum>k\<le>n. measure lebesgue (S k)) = measure lebesgue (UNION {..n} S)"
    1.12 @@ -2837,7 +2837,7 @@
    1.13        if "bounded S" "S \<in> lmeasurable" for S
    1.14      proof -
    1.15        obtain a b where "S \<subseteq> cbox a b"
    1.16 -        using \<open>bounded S\<close> bounded_subset_cbox by blast
    1.17 +        using \<open>bounded S\<close> bounded_subset_cbox_symmetric by metis
    1.18        have fUD: "(f ` \<Union>\<D>) \<in> lmeasurable \<and> ?\<mu> (f ` \<Union>\<D>) = (m * ?\<mu> (\<Union>\<D>))"
    1.19          if "countable \<D>"
    1.20            and cbox: "\<And>K. K \<in> \<D> \<Longrightarrow> K \<subseteq> cbox a b \<and> K \<noteq> {} \<and> (\<exists>c d. K = cbox c d)"
    1.21 @@ -3005,7 +3005,7 @@
    1.22          "\<And>a b. ball 0 B \<subseteq> cbox a b \<Longrightarrow> \<bar>?\<mu> (S \<inter> cbox a b) - ?\<mu> S\<bar> < e / (1 + \<bar>m\<bar>)"
    1.23          using has_measure_limit [OF S] \<open>e > 0\<close> by (metis abs_add_one_gt_zero zero_less_divide_iff)
    1.24        obtain c d::'n where cd: "ball 0 B \<subseteq> cbox c d"
    1.25 -        using bounded_subset_cbox by blast
    1.26 +        by (metis bounded_subset_cbox_symmetric bounded_ball)
    1.27        with B have less: "\<bar>?\<mu> (S \<inter> cbox c d) - ?\<mu> S\<bar> < e / (1 + \<bar>m\<bar>)" .
    1.28        obtain D where "D > 0" and D: "cbox c d \<subseteq> ball 0 D"
    1.29          by (metis bounded_cbox bounded_subset_ballD)
     2.1 --- a/src/HOL/Analysis/Henstock_Kurzweil_Integration.thy	Sun May 06 23:59:14 2018 +0100
     2.2 +++ b/src/HOL/Analysis/Henstock_Kurzweil_Integration.thy	Tue May 08 10:32:07 2018 +0100
     2.3 @@ -334,7 +334,7 @@
     2.4          \<exists>z. (?F has_integral z) (cbox a b) \<and> norm (z - k2) < norm (k1 - k2)/2"
     2.5      by (rule has_integral_altD[OF assms(2) nonbox,OF e]) blast
     2.6    obtain a b :: 'n where ab: "ball 0 B1 \<subseteq> cbox a b" "ball 0 B2 \<subseteq> cbox a b"
     2.7 -    by (metis Un_subset_iff bounded_Un bounded_ball bounded_subset_cbox)
     2.8 +    by (metis Un_subset_iff bounded_Un bounded_ball bounded_subset_cbox_symmetric)
     2.9    obtain w where w: "(?F has_integral w) (cbox a b)" "norm (w - k1) < norm (k1 - k2)/2"
    2.10      using B1(2)[OF ab(1)] by blast
    2.11    obtain z where z: "(?F has_integral z) (cbox a b)" "norm (z - k2) < norm (k1 - k2)/2"
    2.12 @@ -1635,9 +1635,9 @@
    2.13          using has_integral_altD[OF _ False ij] assms by blast
    2.14        have "bounded (ball 0 B1 \<union> ball (0::'a) B2)"
    2.15          unfolding bounded_Un by(rule conjI bounded_ball)+
    2.16 -      from bounded_subset_cbox[OF this] 
    2.17 +      from bounded_subset_cbox_symmetric[OF this] 
    2.18        obtain a b::'a where ab: "ball 0 B1 \<subseteq> cbox a b" "ball 0 B2 \<subseteq> cbox a b"
    2.19 -        by blast+
    2.20 +        by (meson Un_subset_iff)
    2.21        then obtain w1 w2 where int_w1: "((\<lambda>x. if x \<in> S then f x else 0) has_integral w1) (cbox a b)"
    2.22                          and norm_w1:  "norm (w1 - i) < (i \<bullet> k - j \<bullet> k) / 3"
    2.23                          and int_w2: "((\<lambda>x. if x \<in> S then g x else 0) has_integral w2) (cbox a b)"
    2.24 @@ -6227,7 +6227,7 @@
    2.25          \<exists>z. (?g has_integral z) (cbox a b) \<and> norm (z - integral S g) < e/2"
    2.26        using integrable_integral [OF int_g,unfolded has_integral'[of g]] e that by blast
    2.27      obtain a b::'n where ab: "ball 0 Bf \<union> ball 0 Bg \<subseteq> cbox a b"
    2.28 -      using ball_max_Un bounded_subset_cbox[OF bounded_ball, of _ "max Bf Bg"] by blast
    2.29 +      using ball_max_Un  by (metis bounded_ball bounded_subset_cbox_symmetric)
    2.30      have "ball 0 Bf \<subseteq> cbox a b"
    2.31        using ab by auto
    2.32      with Bf obtain z where int_fz: "(?f has_integral z) (cbox a b)" and z: "norm (z - integral S f) < e/2"
     3.1 --- a/src/HOL/Analysis/Lebesgue_Measure.thy	Sun May 06 23:59:14 2018 +0100
     3.2 +++ b/src/HOL/Analysis/Lebesgue_Measure.thy	Tue May 08 10:32:07 2018 +0100
     3.3 @@ -908,14 +908,17 @@
     3.4  qed (simp add: borel_prod[symmetric])
     3.5  
     3.6  (* FIXME: conversion in measurable prover *)
     3.7 -lemma lborelD_Collect[measurable (raw)]: "{x\<in>space borel. P x} \<in> sets borel \<Longrightarrow> {x\<in>space lborel. P x} \<in> sets lborel" by simp
     3.8 -lemma lborelD[measurable (raw)]: "A \<in> sets borel \<Longrightarrow> A \<in> sets lborel" by simp
     3.9 +lemma lborelD_Collect[measurable (raw)]: "{x\<in>space borel. P x} \<in> sets borel \<Longrightarrow> {x\<in>space lborel. P x} \<in> sets lborel" 
    3.10 +  by simp
    3.11 +
    3.12 +lemma lborelD[measurable (raw)]: "A \<in> sets borel \<Longrightarrow> A \<in> sets lborel"
    3.13 +  by simp
    3.14  
    3.15  lemma emeasure_bounded_finite:
    3.16    assumes "bounded A" shows "emeasure lborel A < \<infinity>"
    3.17  proof -
    3.18 -  from bounded_subset_cbox[OF \<open>bounded A\<close>] obtain a b where "A \<subseteq> cbox a b"
    3.19 -    by auto
    3.20 +  obtain a b where "A \<subseteq> cbox a b"
    3.21 +    by (meson bounded_subset_cbox_symmetric \<open>bounded A\<close>)
    3.22    then have "emeasure lborel A \<le> emeasure lborel (cbox a b)"
    3.23      by (intro emeasure_mono) auto
    3.24    then show ?thesis
     4.1 --- a/src/HOL/Analysis/Ordered_Euclidean_Space.thy	Sun May 06 23:59:14 2018 +0100
     4.2 +++ b/src/HOL/Analysis/Ordered_Euclidean_Space.thy	Tue May 08 10:32:07 2018 +0100
     4.3 @@ -267,7 +267,7 @@
     4.4      and bdd_below_box[intro, simp]: "bdd_below (box a b)"
     4.5    unfolding atomize_conj
     4.6    by (metis bdd_above_Icc bdd_above_mono bdd_below_Icc bdd_below_mono bounded_box
     4.7 -    bounded_subset_cbox interval_cbox)
     4.8 +            bounded_subset_cbox_symmetric interval_cbox)
     4.9  
    4.10  instantiation vec :: (ordered_euclidean_space, finite) ordered_euclidean_space
    4.11  begin
     5.1 --- a/src/HOL/Analysis/Path_Connected.thy	Sun May 06 23:59:14 2018 +0100
     5.2 +++ b/src/HOL/Analysis/Path_Connected.thy	Tue May 08 10:32:07 2018 +0100
     5.3 @@ -6981,7 +6981,7 @@
     5.4      shows "S = {}"
     5.5  proof -
     5.6    obtain a b where "S \<subseteq> box a b"
     5.7 -    by (meson assms bounded_subset_open_interval)
     5.8 +    by (meson assms bounded_subset_box_symmetric)
     5.9    then have "a \<notin> S" "b \<notin> S"
    5.10      by auto
    5.11    then have "\<forall>x. a \<le> x \<and> x \<le> b \<longrightarrow> x \<in> - S"
     6.1 --- a/src/HOL/Analysis/Tagged_Division.thy	Sun May 06 23:59:14 2018 +0100
     6.2 +++ b/src/HOL/Analysis/Tagged_Division.thy	Tue May 08 10:32:07 2018 +0100
     6.3 @@ -685,7 +685,7 @@
     6.4  
     6.5  lemma elementary_subset_cbox:
     6.6    "p division_of S \<Longrightarrow> \<exists>a b. S \<subseteq> cbox a (b::'a::euclidean_space)"
     6.7 -  by (meson elementary_bounded bounded_subset_cbox)
     6.8 +  by (meson bounded_subset_cbox_symmetric elementary_bounded)
     6.9  
    6.10  lemma division_union_intervals_exists:
    6.11    fixes a b :: "'a::euclidean_space"
     7.1 --- a/src/HOL/Analysis/Topology_Euclidean_Space.thy	Sun May 06 23:59:14 2018 +0100
     7.2 +++ b/src/HOL/Analysis/Topology_Euclidean_Space.thy	Tue May 08 10:32:07 2018 +0100
     7.3 @@ -47,19 +47,19 @@
     7.4  lemma support_on_if_subset: "support_on A (\<lambda>x. if P x then a else 0) \<subseteq> {x \<in> A. P x}"
     7.5    by (auto simp: support_on_def)
     7.6  
     7.7 -lemma finite_support[intro]: "finite s \<Longrightarrow> finite (support_on s f)"
     7.8 +lemma finite_support[intro]: "finite S \<Longrightarrow> finite (support_on S f)"
     7.9    unfolding support_on_def by auto
    7.10  
    7.11  (* TODO: is supp_sum really needed? TODO: Generalize to Finite_Set.fold *)
    7.12  definition (in comm_monoid_add) supp_sum :: "('b \<Rightarrow> 'a) \<Rightarrow> 'b set \<Rightarrow> 'a"
    7.13 -  where "supp_sum f s = (\<Sum>x\<in>support_on s f. f x)"
    7.14 +  where "supp_sum f S = (\<Sum>x\<in>support_on S f. f x)"
    7.15  
    7.16  lemma supp_sum_empty[simp]: "supp_sum f {} = 0"
    7.17    unfolding supp_sum_def by auto
    7.18  
    7.19  lemma supp_sum_insert[simp]:
    7.20 -  "finite (support_on s f) \<Longrightarrow>
    7.21 -    supp_sum f (insert x s) = (if x \<in> s then supp_sum f s else f x + supp_sum f s)"
    7.22 +  "finite (support_on S f) \<Longrightarrow>
    7.23 +    supp_sum f (insert x S) = (if x \<in> S then supp_sum f S else f x + supp_sum f S)"
    7.24    by (simp add: supp_sum_def in_support_on insert_absorb)
    7.25  
    7.26  lemma supp_sum_divide_distrib: "supp_sum f A / (r::'a::field) = supp_sum (\<lambda>n. f n / r) A"
    7.27 @@ -70,17 +70,36 @@
    7.28  
    7.29  lemma image_affinity_interval:
    7.30    fixes c :: "'a::ordered_real_vector"
    7.31 -  shows "((\<lambda>x. m *\<^sub>R x + c) ` {a..b}) = (if {a..b}={} then {}
    7.32 -            else if 0 <= m then {m *\<^sub>R a + c .. m  *\<^sub>R b + c}
    7.33 +  shows "((\<lambda>x. m *\<^sub>R x + c) ` {a..b}) = 
    7.34 +           (if {a..b}={} then {}
    7.35 +            else if 0 \<le> m then {m *\<^sub>R a + c .. m  *\<^sub>R b + c}
    7.36              else {m *\<^sub>R b + c .. m *\<^sub>R a + c})"
    7.37 -  apply (case_tac "m=0", force)
    7.38 -  apply (auto simp: scaleR_left_mono)
    7.39 -  apply (rule_tac x="inverse m *\<^sub>R (x-c)" in rev_image_eqI, auto simp: pos_le_divideR_eq le_diff_eq scaleR_left_mono_neg)
    7.40 -  apply (metis diff_le_eq inverse_inverse_eq order.not_eq_order_implies_strict pos_le_divideR_eq positive_imp_inverse_positive)
    7.41 -  apply (rule_tac x="inverse m *\<^sub>R (x-c)" in rev_image_eqI, auto simp: not_le neg_le_divideR_eq diff_le_eq)
    7.42 -  using le_diff_eq scaleR_le_cancel_left_neg
    7.43 -  apply fastforce
    7.44 -  done
    7.45 +         (is "?lhs = ?rhs")
    7.46 +proof (cases "m=0")
    7.47 +  case True
    7.48 +  then show ?thesis
    7.49 +    by force
    7.50 +next
    7.51 +  case False
    7.52 +  show ?thesis
    7.53 +  proof
    7.54 +    show "?lhs \<subseteq> ?rhs"
    7.55 +      by (auto simp: scaleR_left_mono scaleR_left_mono_neg)
    7.56 +    show "?rhs \<subseteq> ?lhs"
    7.57 +    proof (clarsimp, intro conjI impI subsetI)
    7.58 +      show "\<lbrakk>0 \<le> m; a \<le> b; x \<in> {m *\<^sub>R a + c..m *\<^sub>R b + c}\<rbrakk>
    7.59 +            \<Longrightarrow> x \<in> (\<lambda>x. m *\<^sub>R x + c) ` {a..b}" for x
    7.60 +        apply (rule_tac x="inverse m *\<^sub>R (x-c)" in rev_image_eqI)
    7.61 +        using False apply (auto simp: le_diff_eq pos_le_divideRI)
    7.62 +        using diff_le_eq pos_le_divideR_eq by force
    7.63 +      show "\<lbrakk>\<not> 0 \<le> m; a \<le> b;  x \<in> {m *\<^sub>R b + c..m *\<^sub>R a + c}\<rbrakk>
    7.64 +            \<Longrightarrow> x \<in> (\<lambda>x. m *\<^sub>R x + c) ` {a..b}" for x
    7.65 +        apply (rule_tac x="inverse m *\<^sub>R (x-c)" in rev_image_eqI)
    7.66 +        apply (auto simp: diff_le_eq neg_le_divideR_eq)
    7.67 +        using diff_eq_diff_less_eq linordered_field_class.sign_simps(11) minus_diff_eq not_less scaleR_le_cancel_left_neg by fastforce
    7.68 +    qed
    7.69 +  qed
    7.70 +qed
    7.71  
    7.72  lemma countable_PiE:
    7.73    "finite I \<Longrightarrow> (\<And>i. i \<in> I \<Longrightarrow> countable (F i)) \<Longrightarrow> countable (Pi\<^sub>E I F)"
    7.74 @@ -286,78 +305,83 @@
    7.75  end
    7.76  
    7.77  lemma (in first_countable_topology) first_countable_basisE:
    7.78 -  obtains A where "countable A" "\<And>a. a \<in> A \<Longrightarrow> x \<in> a" "\<And>a. a \<in> A \<Longrightarrow> open a"
    7.79 -    "\<And>S. open S \<Longrightarrow> x \<in> S \<Longrightarrow> (\<exists>a\<in>A. a \<subseteq> S)"
    7.80 -  using first_countable_basis[of x]
    7.81 -  apply atomize_elim
    7.82 -  apply (elim exE)
    7.83 -  apply (rule_tac x="range A" in exI, auto)
    7.84 -  done
    7.85 +  fixes x :: 'a
    7.86 +  obtains \<A> where "countable \<A>" "\<And>A. A \<in> \<A> \<Longrightarrow> x \<in> A" "\<And>A. A \<in> \<A> \<Longrightarrow> open A"
    7.87 +    "\<And>S. open S \<Longrightarrow> x \<in> S \<Longrightarrow> (\<exists>A\<in>\<A>. A \<subseteq> S)"
    7.88 +proof -
    7.89 +  obtain \<A> where \<A>: "(\<forall>i::nat. x \<in> \<A> i \<and> open (\<A> i))" "(\<forall>S. open S \<and> x \<in> S \<longrightarrow> (\<exists>i. \<A> i \<subseteq> S))"
    7.90 +    using first_countable_basis[of x] by metis
    7.91 +  show thesis
    7.92 +  proof 
    7.93 +    show "countable (range \<A>)"
    7.94 +      by simp
    7.95 +  qed (use \<A> in auto)
    7.96 +qed
    7.97  
    7.98  lemma (in first_countable_topology) first_countable_basis_Int_stableE:
    7.99 -  obtains A where "countable A" "\<And>a. a \<in> A \<Longrightarrow> x \<in> a" "\<And>a. a \<in> A \<Longrightarrow> open a"
   7.100 -    "\<And>S. open S \<Longrightarrow> x \<in> S \<Longrightarrow> (\<exists>a\<in>A. a \<subseteq> S)"
   7.101 -    "\<And>a b. a \<in> A \<Longrightarrow> b \<in> A \<Longrightarrow> a \<inter> b \<in> A"
   7.102 +  obtains \<A> where "countable \<A>" "\<And>A. A \<in> \<A> \<Longrightarrow> x \<in> A" "\<And>A. A \<in> \<A> \<Longrightarrow> open A"
   7.103 +    "\<And>S. open S \<Longrightarrow> x \<in> S \<Longrightarrow> (\<exists>A\<in>\<A>. A \<subseteq> S)"
   7.104 +    "\<And>A B. A \<in> \<A> \<Longrightarrow> B \<in> \<A> \<Longrightarrow> A \<inter> B \<in> \<A>"
   7.105  proof atomize_elim
   7.106 -  obtain A' where A':
   7.107 -    "countable A'"
   7.108 -    "\<And>a. a \<in> A' \<Longrightarrow> x \<in> a"
   7.109 -    "\<And>a. a \<in> A' \<Longrightarrow> open a"
   7.110 -    "\<And>S. open S \<Longrightarrow> x \<in> S \<Longrightarrow> \<exists>a\<in>A'. a \<subseteq> S"
   7.111 +  obtain \<B> where \<B>:
   7.112 +    "countable \<B>"
   7.113 +    "\<And>B. B \<in> \<B> \<Longrightarrow> x \<in> B"
   7.114 +    "\<And>B. B \<in> \<B> \<Longrightarrow> open B"
   7.115 +    "\<And>S. open S \<Longrightarrow> x \<in> S \<Longrightarrow> \<exists>B\<in>\<B>. B \<subseteq> S"
   7.116      by (rule first_countable_basisE) blast
   7.117 -  define A where [abs_def]:
   7.118 -    "A = (\<lambda>N. \<Inter>((\<lambda>n. from_nat_into A' n) ` N)) ` (Collect finite::nat set set)"
   7.119 -  then show "\<exists>A. countable A \<and> (\<forall>a. a \<in> A \<longrightarrow> x \<in> a) \<and> (\<forall>a. a \<in> A \<longrightarrow> open a) \<and>
   7.120 -        (\<forall>S. open S \<longrightarrow> x \<in> S \<longrightarrow> (\<exists>a\<in>A. a \<subseteq> S)) \<and> (\<forall>a b. a \<in> A \<longrightarrow> b \<in> A \<longrightarrow> a \<inter> b \<in> A)"
   7.121 -  proof (safe intro!: exI[where x=A])
   7.122 -    show "countable A"
   7.123 -      unfolding A_def by (intro countable_image countable_Collect_finite)
   7.124 -    fix a
   7.125 -    assume "a \<in> A"
   7.126 -    then show "x \<in> a" "open a"
   7.127 -      using A'(4)[OF open_UNIV] by (auto simp: A_def intro: A' from_nat_into)
   7.128 +  define \<A> where [abs_def]:
   7.129 +    "\<A> = (\<lambda>N. \<Inter>((\<lambda>n. from_nat_into \<B> n) ` N)) ` (Collect finite::nat set set)"
   7.130 +  then show "\<exists>\<A>. countable \<A> \<and> (\<forall>A. A \<in> \<A> \<longrightarrow> x \<in> A) \<and> (\<forall>A. A \<in> \<A> \<longrightarrow> open A) \<and>
   7.131 +        (\<forall>S. open S \<longrightarrow> x \<in> S \<longrightarrow> (\<exists>A\<in>\<A>. A \<subseteq> S)) \<and> (\<forall>A B. A \<in> \<A> \<longrightarrow> B \<in> \<A> \<longrightarrow> A \<inter> B \<in> \<A>)"
   7.132 +  proof (safe intro!: exI[where x=\<A>])
   7.133 +    show "countable \<A>"
   7.134 +      unfolding \<A>_def by (intro countable_image countable_Collect_finite)
   7.135 +    fix A
   7.136 +    assume "A \<in> \<A>"
   7.137 +    then show "x \<in> A" "open A"
   7.138 +      using \<B>(4)[OF open_UNIV] by (auto simp: \<A>_def intro: \<B> from_nat_into)
   7.139    next
   7.140 -    let ?int = "\<lambda>N. \<Inter>(from_nat_into A' ` N)"
   7.141 -    fix a b
   7.142 -    assume "a \<in> A" "b \<in> A"
   7.143 -    then obtain N M where "a = ?int N" "b = ?int M" "finite (N \<union> M)"
   7.144 -      by (auto simp: A_def)
   7.145 -    then show "a \<inter> b \<in> A"
   7.146 -      by (auto simp: A_def intro!: image_eqI[where x="N \<union> M"])
   7.147 +    let ?int = "\<lambda>N. \<Inter>(from_nat_into \<B> ` N)"
   7.148 +    fix A B
   7.149 +    assume "A \<in> \<A>" "B \<in> \<A>"
   7.150 +    then obtain N M where "A = ?int N" "B = ?int M" "finite (N \<union> M)"
   7.151 +      by (auto simp: \<A>_def)
   7.152 +    then show "A \<inter> B \<in> \<A>"
   7.153 +      by (auto simp: \<A>_def intro!: image_eqI[where x="N \<union> M"])
   7.154    next
   7.155      fix S
   7.156      assume "open S" "x \<in> S"
   7.157 -    then obtain a where a: "a\<in>A'" "a \<subseteq> S" using A' by blast
   7.158 -    then show "\<exists>a\<in>A. a \<subseteq> S" using a A'
   7.159 -      by (intro bexI[where x=a]) (auto simp: A_def intro: image_eqI[where x="{to_nat_on A' a}"])
   7.160 +    then obtain a where a: "a\<in>\<B>" "a \<subseteq> S" using \<B> by blast
   7.161 +    then show "\<exists>a\<in>\<A>. a \<subseteq> S" using a \<B>
   7.162 +      by (intro bexI[where x=a]) (auto simp: \<A>_def intro: image_eqI[where x="{to_nat_on \<B> a}"])
   7.163    qed
   7.164  qed
   7.165  
   7.166  lemma (in topological_space) first_countableI:
   7.167 -  assumes "countable A"
   7.168 -    and 1: "\<And>a. a \<in> A \<Longrightarrow> x \<in> a" "\<And>a. a \<in> A \<Longrightarrow> open a"
   7.169 -    and 2: "\<And>S. open S \<Longrightarrow> x \<in> S \<Longrightarrow> \<exists>a\<in>A. a \<subseteq> S"
   7.170 -  shows "\<exists>A::nat \<Rightarrow> 'a set. (\<forall>i. x \<in> A i \<and> open (A i)) \<and> (\<forall>S. open S \<and> x \<in> S \<longrightarrow> (\<exists>i. A i \<subseteq> S))"
   7.171 -proof (safe intro!: exI[of _ "from_nat_into A"])
   7.172 +  assumes "countable \<A>"
   7.173 +    and 1: "\<And>A. A \<in> \<A> \<Longrightarrow> x \<in> A" "\<And>A. A \<in> \<A> \<Longrightarrow> open A"
   7.174 +    and 2: "\<And>S. open S \<Longrightarrow> x \<in> S \<Longrightarrow> \<exists>A\<in>\<A>. A \<subseteq> S"
   7.175 +  shows "\<exists>\<A>::nat \<Rightarrow> 'a set. (\<forall>i. x \<in> \<A> i \<and> open (\<A> i)) \<and> (\<forall>S. open S \<and> x \<in> S \<longrightarrow> (\<exists>i. \<A> i \<subseteq> S))"
   7.176 +proof (safe intro!: exI[of _ "from_nat_into \<A>"])
   7.177    fix i
   7.178 -  have "A \<noteq> {}" using 2[of UNIV] by auto
   7.179 -  show "x \<in> from_nat_into A i" "open (from_nat_into A i)"
   7.180 -    using range_from_nat_into_subset[OF \<open>A \<noteq> {}\<close>] 1 by auto
   7.181 +  have "\<A> \<noteq> {}" using 2[of UNIV] by auto
   7.182 +  show "x \<in> from_nat_into \<A> i" "open (from_nat_into \<A> i)"
   7.183 +    using range_from_nat_into_subset[OF \<open>\<A> \<noteq> {}\<close>] 1 by auto
   7.184  next
   7.185    fix S
   7.186    assume "open S" "x\<in>S" from 2[OF this]
   7.187 -  show "\<exists>i. from_nat_into A i \<subseteq> S"
   7.188 -    using subset_range_from_nat_into[OF \<open>countable A\<close>] by auto
   7.189 +  show "\<exists>i. from_nat_into \<A> i \<subseteq> S"
   7.190 +    using subset_range_from_nat_into[OF \<open>countable \<A>\<close>] by auto
   7.191  qed
   7.192  
   7.193  instance prod :: (first_countable_topology, first_countable_topology) first_countable_topology
   7.194  proof
   7.195    fix x :: "'a \<times> 'b"
   7.196 -  obtain A where A:
   7.197 -      "countable A"
   7.198 -      "\<And>a. a \<in> A \<Longrightarrow> fst x \<in> a"
   7.199 -      "\<And>a. a \<in> A \<Longrightarrow> open a"
   7.200 -      "\<And>S. open S \<Longrightarrow> fst x \<in> S \<Longrightarrow> \<exists>a\<in>A. a \<subseteq> S"
   7.201 +  obtain \<A> where \<A>:
   7.202 +      "countable \<A>"
   7.203 +      "\<And>a. a \<in> \<A> \<Longrightarrow> fst x \<in> a"
   7.204 +      "\<And>a. a \<in> \<A> \<Longrightarrow> open a"
   7.205 +      "\<And>S. open S \<Longrightarrow> fst x \<in> S \<Longrightarrow> \<exists>a\<in>\<A>. a \<subseteq> S"
   7.206      by (rule first_countable_basisE[of "fst x"]) blast
   7.207    obtain B where B:
   7.208        "countable B"
   7.209 @@ -365,27 +389,28 @@
   7.210        "\<And>a. a \<in> B \<Longrightarrow> open a"
   7.211        "\<And>S. open S \<Longrightarrow> snd x \<in> S \<Longrightarrow> \<exists>a\<in>B. a \<subseteq> S"
   7.212      by (rule first_countable_basisE[of "snd x"]) blast
   7.213 -  show "\<exists>A::nat \<Rightarrow> ('a \<times> 'b) set.
   7.214 -    (\<forall>i. x \<in> A i \<and> open (A i)) \<and> (\<forall>S. open S \<and> x \<in> S \<longrightarrow> (\<exists>i. A i \<subseteq> S))"
   7.215 -  proof (rule first_countableI[of "(\<lambda>(a, b). a \<times> b) ` (A \<times> B)"], safe)
   7.216 +  show "\<exists>\<A>::nat \<Rightarrow> ('a \<times> 'b) set.
   7.217 +    (\<forall>i. x \<in> \<A> i \<and> open (\<A> i)) \<and> (\<forall>S. open S \<and> x \<in> S \<longrightarrow> (\<exists>i. \<A> i \<subseteq> S))"
   7.218 +  proof (rule first_countableI[of "(\<lambda>(a, b). a \<times> b) ` (\<A> \<times> B)"], safe)
   7.219      fix a b
   7.220 -    assume x: "a \<in> A" "b \<in> B"
   7.221 -    with A(2, 3)[of a] B(2, 3)[of b] show "x \<in> a \<times> b" and "open (a \<times> b)"
   7.222 -      unfolding mem_Times_iff
   7.223 -      by (auto intro: open_Times)
   7.224 +    assume x: "a \<in> \<A>" "b \<in> B"
   7.225 +    show "x \<in> a \<times> b" 
   7.226 +      by (simp add: \<A>(2) B(2) mem_Times_iff x)
   7.227 +    show "open (a \<times> b)"
   7.228 +      by (simp add: \<A>(3) B(3) open_Times x)
   7.229    next
   7.230      fix S
   7.231      assume "open S" "x \<in> S"
   7.232      then obtain a' b' where a'b': "open a'" "open b'" "x \<in> a' \<times> b'" "a' \<times> b' \<subseteq> S"
   7.233        by (rule open_prod_elim)
   7.234      moreover
   7.235 -    from a'b' A(4)[of a'] B(4)[of b']
   7.236 -    obtain a b where "a \<in> A" "a \<subseteq> a'" "b \<in> B" "b \<subseteq> b'"
   7.237 +    from a'b' \<A>(4)[of a'] B(4)[of b']
   7.238 +    obtain a b where "a \<in> \<A>" "a \<subseteq> a'" "b \<in> B" "b \<subseteq> b'"
   7.239        by auto
   7.240      ultimately
   7.241 -    show "\<exists>a\<in>(\<lambda>(a, b). a \<times> b) ` (A \<times> B). a \<subseteq> S"
   7.242 +    show "\<exists>a\<in>(\<lambda>(a, b). a \<times> b) ` (\<A> \<times> B). a \<subseteq> S"
   7.243        by (auto intro!: bexI[of _ "a \<times> b"] bexI[of _ a] bexI[of _ b])
   7.244 -  qed (simp add: A B)
   7.245 +  qed (simp add: \<A> B)
   7.246  qed
   7.247  
   7.248  class second_countable_topology = topological_space +
   7.249 @@ -962,61 +987,60 @@
   7.250  qed
   7.251  
   7.252  lemma connected_openin:
   7.253 -      "connected s \<longleftrightarrow>
   7.254 -       ~(\<exists>e1 e2. openin (subtopology euclidean s) e1 \<and>
   7.255 -                 openin (subtopology euclidean s) e2 \<and>
   7.256 -                 s \<subseteq> e1 \<union> e2 \<and> e1 \<inter> e2 = {} \<and> e1 \<noteq> {} \<and> e2 \<noteq> {})"
   7.257 +      "connected S \<longleftrightarrow>
   7.258 +       ~(\<exists>E1 E2. openin (subtopology euclidean S) E1 \<and>
   7.259 +                 openin (subtopology euclidean S) E2 \<and>
   7.260 +                 S \<subseteq> E1 \<union> E2 \<and> E1 \<inter> E2 = {} \<and> E1 \<noteq> {} \<and> E2 \<noteq> {})"
   7.261    apply (simp add: connected_def openin_open disjoint_iff_not_equal, safe)
   7.262    apply (simp_all, blast+)  (* SLOW *)
   7.263    done
   7.264  
   7.265  lemma connected_openin_eq:
   7.266 -      "connected s \<longleftrightarrow>
   7.267 -       ~(\<exists>e1 e2. openin (subtopology euclidean s) e1 \<and>
   7.268 -                 openin (subtopology euclidean s) e2 \<and>
   7.269 -                 e1 \<union> e2 = s \<and> e1 \<inter> e2 = {} \<and>
   7.270 -                 e1 \<noteq> {} \<and> e2 \<noteq> {})"
   7.271 +      "connected S \<longleftrightarrow>
   7.272 +       ~(\<exists>E1 E2. openin (subtopology euclidean S) E1 \<and>
   7.273 +                 openin (subtopology euclidean S) E2 \<and>
   7.274 +                 E1 \<union> E2 = S \<and> E1 \<inter> E2 = {} \<and>
   7.275 +                 E1 \<noteq> {} \<and> E2 \<noteq> {})"
   7.276    apply (simp add: connected_openin, safe, blast)
   7.277    by (metis Int_lower1 Un_subset_iff openin_open subset_antisym)
   7.278  
   7.279  lemma connected_closedin:
   7.280 -      "connected s \<longleftrightarrow>
   7.281 -       ~(\<exists>e1 e2.
   7.282 -             closedin (subtopology euclidean s) e1 \<and>
   7.283 -             closedin (subtopology euclidean s) e2 \<and>
   7.284 -             s \<subseteq> e1 \<union> e2 \<and> e1 \<inter> e2 = {} \<and>
   7.285 -             e1 \<noteq> {} \<and> e2 \<noteq> {})"
   7.286 -proof -
   7.287 -  { fix A B x x'
   7.288 -    assume s_sub: "s \<subseteq> A \<union> B"
   7.289 -       and disj: "A \<inter> B \<inter> s = {}"
   7.290 -       and x: "x \<in> s" "x \<in> B" and x': "x' \<in> s" "x' \<in> A"
   7.291 -       and cl: "closed A" "closed B"
   7.292 -    assume "\<forall>e1. (\<forall>T. closed T \<longrightarrow> e1 \<noteq> s \<inter> T) \<or> (\<forall>e2. e1 \<inter> e2 = {} \<longrightarrow> s \<subseteq> e1 \<union> e2 \<longrightarrow> (\<forall>T. closed T \<longrightarrow> e2 \<noteq> s \<inter> T) \<or> e1 = {} \<or> e2 = {})"
   7.293 -    then have "\<And>C D. s \<inter> C = {} \<or> s \<inter> D = {} \<or> s \<inter> (C \<inter> (s \<inter> D)) \<noteq> {} \<or> \<not> s \<subseteq> s \<inter> (C \<union> D) \<or> \<not> closed C \<or> \<not> closed D"
   7.294 -      by (metis (no_types) Int_Un_distrib Int_assoc)
   7.295 -    moreover have "s \<inter> (A \<inter> B) = {}" "s \<inter> (A \<union> B) = s" "s \<inter> B \<noteq> {}"
   7.296 -      using disj s_sub x by blast+
   7.297 -    ultimately have "s \<inter> A = {}"
   7.298 -      using cl by (metis inf.left_commute inf_bot_right order_refl)
   7.299 -    then have False
   7.300 -      using x' by blast
   7.301 -  } note * = this
   7.302 -  show ?thesis
   7.303 -    apply (simp add: connected_closed closedin_closed)
   7.304 -    apply (safe; simp)
   7.305 -    apply blast
   7.306 -    apply (blast intro: *)
   7.307 -    done
   7.308 +      "connected S \<longleftrightarrow>
   7.309 +       (\<nexists>E1 E2.
   7.310 +        closedin (subtopology euclidean S) E1 \<and>
   7.311 +        closedin (subtopology euclidean S) E2 \<and>
   7.312 +        S \<subseteq> E1 \<union> E2 \<and> E1 \<inter> E2 = {} \<and> E1 \<noteq> {} \<and> E2 \<noteq> {})"
   7.313 +       (is "?lhs = ?rhs")
   7.314 +proof
   7.315 +  assume ?lhs
   7.316 +  then show ?rhs 
   7.317 +    by (auto simp add: connected_closed closedin_closed)
   7.318 +next
   7.319 +  assume R: ?rhs
   7.320 +  then show ?lhs 
   7.321 +  proof (clarsimp simp add: connected_closed closedin_closed)
   7.322 +    fix A B 
   7.323 +    assume s_sub: "S \<subseteq> A \<union> B" "B \<inter> S \<noteq> {}"
   7.324 +      and disj: "A \<inter> B \<inter> S = {}"
   7.325 +      and cl: "closed A" "closed B"
   7.326 +    have "S \<inter> (A \<union> B) = S"
   7.327 +      using s_sub(1) by auto
   7.328 +    have "S - A = B \<inter> S"
   7.329 +      using Diff_subset_conv Un_Diff_Int disj s_sub(1) by auto
   7.330 +    then have "S \<inter> A = {}"
   7.331 +      by (metis Diff_Diff_Int Diff_disjoint Un_Diff_Int R cl closedin_closed_Int inf_commute order_refl s_sub(2))
   7.332 +    then show "A \<inter> S = {}"
   7.333 +      by blast
   7.334 +  qed
   7.335  qed
   7.336  
   7.337  lemma connected_closedin_eq:
   7.338 -      "connected s \<longleftrightarrow>
   7.339 -           ~(\<exists>e1 e2.
   7.340 -                 closedin (subtopology euclidean s) e1 \<and>
   7.341 -                 closedin (subtopology euclidean s) e2 \<and>
   7.342 -                 e1 \<union> e2 = s \<and> e1 \<inter> e2 = {} \<and>
   7.343 -                 e1 \<noteq> {} \<and> e2 \<noteq> {})"
   7.344 +      "connected S \<longleftrightarrow>
   7.345 +           ~(\<exists>E1 E2.
   7.346 +                 closedin (subtopology euclidean S) E1 \<and>
   7.347 +                 closedin (subtopology euclidean S) E2 \<and>
   7.348 +                 E1 \<union> E2 = S \<and> E1 \<inter> E2 = {} \<and>
   7.349 +                 E1 \<noteq> {} \<and> E2 \<noteq> {})"
   7.350    apply (simp add: connected_closedin, safe, blast)
   7.351    by (metis Int_lower1 Un_subset_iff closedin_closed subset_antisym)
   7.352  
   7.353 @@ -1662,100 +1686,48 @@
   7.354      and "box c d \<subseteq> cbox a b \<longleftrightarrow> (\<forall>i\<in>Basis. c\<bullet>i < d\<bullet>i) \<longrightarrow> (\<forall>i\<in>Basis. a\<bullet>i \<le> c\<bullet>i \<and> d\<bullet>i \<le> b\<bullet>i)" (is ?th3)
   7.355      and "box c d \<subseteq> box a b \<longleftrightarrow> (\<forall>i\<in>Basis. c\<bullet>i < d\<bullet>i) \<longrightarrow> (\<forall>i\<in>Basis. a\<bullet>i \<le> c\<bullet>i \<and> d\<bullet>i \<le> b\<bullet>i)" (is ?th4)
   7.356  proof -
   7.357 -  show ?th1
   7.358 -    unfolding subset_eq and Ball_def and mem_box
   7.359 -    by (auto intro: order_trans)
   7.360 -  show ?th2
   7.361 -    unfolding subset_eq and Ball_def and mem_box
   7.362 -    by (auto intro: le_less_trans less_le_trans order_trans less_imp_le)
   7.363 -  {
   7.364 -    assume as: "box c d \<subseteq> cbox a b" "\<forall>i\<in>Basis. c\<bullet>i < d\<bullet>i"
   7.365 -    then have "box c d \<noteq> {}"
   7.366 -      unfolding box_eq_empty by auto
   7.367 -    fix i :: 'a
   7.368 -    assume i: "i \<in> Basis"
   7.369 -    (** TODO combine the following two parts as done in the HOL_light version. **)
   7.370 -    {
   7.371 -      let ?x = "(\<Sum>j\<in>Basis. (if j=i then ((min (a\<bullet>j) (d\<bullet>j))+c\<bullet>j)/2 else (c\<bullet>j+d\<bullet>j)/2) *\<^sub>R j)::'a"
   7.372 -      assume as2: "a\<bullet>i > c\<bullet>i"
   7.373 -      {
   7.374 -        fix j :: 'a
   7.375 -        assume j: "j \<in> Basis"
   7.376 -        then have "c \<bullet> j < ?x \<bullet> j \<and> ?x \<bullet> j < d \<bullet> j"
   7.377 -          apply (cases "j = i")
   7.378 -          using as(2)[THEN bspec[where x=j]] i
   7.379 -          apply (auto simp: as2)
   7.380 -          done
   7.381 -      }
   7.382 -      then have "?x\<in>box c d"
   7.383 -        using i unfolding mem_box by auto
   7.384 -      moreover
   7.385 -      have "?x \<notin> cbox a b"
   7.386 -        unfolding mem_box
   7.387 -        apply auto
   7.388 -        apply (rule_tac x=i in bexI)
   7.389 -        using as(2)[THEN bspec[where x=i]] and as2 i
   7.390 -        apply auto
   7.391 -        done
   7.392 -      ultimately have False using as by auto
   7.393 +  let ?lesscd = "\<forall>i\<in>Basis. c\<bullet>i < d\<bullet>i"
   7.394 +  let ?lerhs = "\<forall>i\<in>Basis. a\<bullet>i \<le> c\<bullet>i \<and> d\<bullet>i \<le> b\<bullet>i"
   7.395 +  show ?th1 ?th2
   7.396 +    by (fastforce simp: mem_box)+
   7.397 +  have acdb: "a\<bullet>i \<le> c\<bullet>i \<and> d\<bullet>i \<le> b\<bullet>i"
   7.398 +    if i: "i \<in> Basis" and box: "box c d \<subseteq> cbox a b" and cd: "\<And>i. i \<in> Basis \<Longrightarrow> c\<bullet>i < d\<bullet>i" for i
   7.399 +  proof -
   7.400 +    have "box c d \<noteq> {}"
   7.401 +      using that
   7.402 +      unfolding box_eq_empty by force
   7.403 +    { let ?x = "(\<Sum>j\<in>Basis. (if j=i then ((min (a\<bullet>j) (d\<bullet>j))+c\<bullet>j)/2 else (c\<bullet>j+d\<bullet>j)/2) *\<^sub>R j)::'a"
   7.404 +      assume *: "a\<bullet>i > c\<bullet>i"
   7.405 +      then have "c \<bullet> j < ?x \<bullet> j \<and> ?x \<bullet> j < d \<bullet> j" if "j \<in> Basis" for j
   7.406 +        using cd that by (fastforce simp add: i *)
   7.407 +      then have "?x \<in> box c d"
   7.408 +        unfolding mem_box by auto
   7.409 +      moreover have "?x \<notin> cbox a b"
   7.410 +        using i cd * by (force simp: mem_box)
   7.411 +      ultimately have False using box by auto
   7.412      }
   7.413 -    then have "a\<bullet>i \<le> c\<bullet>i" by (rule ccontr) auto
   7.414 +    then have "a\<bullet>i \<le> c\<bullet>i" by force
   7.415      moreover
   7.416 -    {
   7.417 -      let ?x = "(\<Sum>j\<in>Basis. (if j=i then ((max (b\<bullet>j) (c\<bullet>j))+d\<bullet>j)/2 else (c\<bullet>j+d\<bullet>j)/2) *\<^sub>R j)::'a"
   7.418 -      assume as2: "b\<bullet>i < d\<bullet>i"
   7.419 -      {
   7.420 -        fix j :: 'a
   7.421 -        assume "j\<in>Basis"
   7.422 -        then have "d \<bullet> j > ?x \<bullet> j \<and> ?x \<bullet> j > c \<bullet> j"
   7.423 -          apply (cases "j = i")
   7.424 -          using as(2)[THEN bspec[where x=j]]
   7.425 -          apply (auto simp: as2)
   7.426 -          done
   7.427 -      }
   7.428 -      then have "?x\<in>box c d"
   7.429 +    { let ?x = "(\<Sum>j\<in>Basis. (if j=i then ((max (b\<bullet>j) (c\<bullet>j))+d\<bullet>j)/2 else (c\<bullet>j+d\<bullet>j)/2) *\<^sub>R j)::'a"
   7.430 +      assume *: "b\<bullet>i < d\<bullet>i"
   7.431 +      then have "d \<bullet> j > ?x \<bullet> j \<and> ?x \<bullet> j > c \<bullet> j" if "j \<in> Basis" for j
   7.432 +        using cd that by (fastforce simp add: i *)
   7.433 +      then have "?x \<in> box c d"
   7.434          unfolding mem_box by auto
   7.435 -      moreover
   7.436 -      have "?x\<notin>cbox a b"
   7.437 -        unfolding mem_box
   7.438 -        apply auto
   7.439 -        apply (rule_tac x=i in bexI)
   7.440 -        using as(2)[THEN bspec[where x=i]] and as2 using i
   7.441 -        apply auto
   7.442 -        done
   7.443 -      ultimately have False using as by auto
   7.444 +      moreover have "?x \<notin> cbox a b"
   7.445 +        using i cd * by (force simp: mem_box)
   7.446 +      ultimately have False using box by auto
   7.447      }
   7.448      then have "b\<bullet>i \<ge> d\<bullet>i" by (rule ccontr) auto
   7.449 -    ultimately
   7.450 -    have "a\<bullet>i \<le> c\<bullet>i \<and> d\<bullet>i \<le> b\<bullet>i" by auto
   7.451 -  } note part1 = this
   7.452 +    ultimately show ?thesis by auto
   7.453 +  qed
   7.454    show ?th3
   7.455 -    unfolding subset_eq and Ball_def and mem_box
   7.456 -    apply (rule, rule, rule, rule)
   7.457 -    apply (rule part1)
   7.458 -    unfolding subset_eq and Ball_def and mem_box
   7.459 -    prefer 4
   7.460 -    apply auto
   7.461 -    apply (erule_tac x=xa in allE, erule_tac x=xa in allE, fastforce)+
   7.462 -    done
   7.463 -  {
   7.464 -    assume as: "box c d \<subseteq> box a b" "\<forall>i\<in>Basis. c\<bullet>i < d\<bullet>i"
   7.465 -    fix i :: 'a
   7.466 -    assume i:"i\<in>Basis"
   7.467 -    from as(1) have "box c d \<subseteq> cbox a b"
   7.468 -      using box_subset_cbox[of a b] by auto
   7.469 -    then have "a\<bullet>i \<le> c\<bullet>i \<and> d\<bullet>i \<le> b\<bullet>i"
   7.470 -      using part1 and as(2) using i by auto
   7.471 -  } note * = this
   7.472 +    using acdb by (fastforce simp add: mem_box)
   7.473 +  have acdb': "a\<bullet>i \<le> c\<bullet>i \<and> d\<bullet>i \<le> b\<bullet>i"
   7.474 +    if "i \<in> Basis" "box c d \<subseteq> box a b" "\<And>i. i \<in> Basis \<Longrightarrow> c\<bullet>i < d\<bullet>i" for i
   7.475 +      using box_subset_cbox[of a b] that acdb by auto
   7.476    show ?th4
   7.477 -    unfolding subset_eq and Ball_def and mem_box
   7.478 -    apply (rule, rule, rule, rule)
   7.479 -    apply (rule *)
   7.480 -    unfolding subset_eq and Ball_def and mem_box
   7.481 -    prefer 4
   7.482 -    apply auto
   7.483 -    apply (erule_tac x=xa in allE, simp)+
   7.484 -    done
   7.485 +    using acdb' by (fastforce simp add: mem_box)
   7.486  qed
   7.487  
   7.488  lemma eq_cbox: "cbox a b = cbox c d \<longleftrightarrow> cbox a b = {} \<and> cbox c d = {} \<or> a = c \<and> b = d"
   7.489 @@ -1775,19 +1747,14 @@
   7.490  lemma eq_cbox_box [simp]: "cbox a b = box c d \<longleftrightarrow> cbox a b = {} \<and> box c d = {}"
   7.491    (is "?lhs \<longleftrightarrow> ?rhs")
   7.492  proof
   7.493 -  assume ?lhs
   7.494 -  then have "cbox a b \<subseteq> box c d" "box c d \<subseteq>cbox a b"
   7.495 +  assume L: ?lhs
   7.496 +  then have "cbox a b \<subseteq> box c d" "box c d \<subseteq> cbox a b"
   7.497      by auto
   7.498    then show ?rhs
   7.499      apply (simp add: subset_box)
   7.500 -    using \<open>cbox a b = box c d\<close> box_ne_empty box_sing
   7.501 -    apply (fastforce simp add:)
   7.502 +    using L box_ne_empty box_sing apply (fastforce simp add:)
   7.503      done
   7.504 -next
   7.505 -  assume ?rhs
   7.506 -  then show ?lhs
   7.507 -    by force
   7.508 -qed
   7.509 +qed force
   7.510  
   7.511  lemma eq_box_cbox [simp]: "box a b = cbox c d \<longleftrightarrow> box a b = {} \<and> cbox c d = {}"
   7.512    by (metis eq_cbox_box)
   7.513 @@ -1795,20 +1762,16 @@
   7.514  lemma eq_box: "box a b = box c d \<longleftrightarrow> box a b = {} \<and> box c d = {} \<or> a = c \<and> b = d"
   7.515    (is "?lhs \<longleftrightarrow> ?rhs")
   7.516  proof
   7.517 -  assume ?lhs
   7.518 +  assume L: ?lhs
   7.519    then have "box a b \<subseteq> box c d" "box c d \<subseteq> box a b"
   7.520      by auto
   7.521    then show ?rhs
   7.522      apply (simp add: subset_box)
   7.523 -    using box_ne_empty(2) \<open>box a b = box c d\<close>
   7.524 +    using box_ne_empty(2) L
   7.525      apply auto
   7.526       apply (meson euclidean_eqI less_eq_real_def not_less)+
   7.527      done
   7.528 -next
   7.529 -  assume ?rhs
   7.530 -  then show ?lhs
   7.531 -    by force
   7.532 -qed
   7.533 +qed force
   7.534  
   7.535  lemma subset_box_complex:
   7.536     "cbox a b \<subseteq> cbox c d \<longleftrightarrow>
   7.537 @@ -2140,7 +2103,7 @@
   7.538      and d: "\<forall>x \<in> S. \<forall>y \<in> S. dist y x < e \<longrightarrow> y = x"
   7.539    shows "closed S"
   7.540  proof -
   7.541 -  have False if C: "\<forall>e>0. \<exists>x'\<in>S. x' \<noteq> x \<and> dist x' x < e" for x
   7.542 +  have False if C: "\<And>e. e>0 \<Longrightarrow> \<exists>x'\<in>S. x' \<noteq> x \<and> dist x' x < e" for x
   7.543    proof -
   7.544      from e have e2: "e/2 > 0" by arith
   7.545      from C[rule_format, OF e2] obtain y where y: "y \<in> S" "y \<noteq> x" "dist y x < e/2"
   7.546 @@ -2148,7 +2111,7 @@
   7.547      let ?m = "min (e/2) (dist x y) "
   7.548      from e2 y(2) have mp: "?m > 0"
   7.549        by simp
   7.550 -    from C[rule_format, OF mp] obtain z where z: "z \<in> S" "z \<noteq> x" "dist z x < ?m"
   7.551 +    from C[OF mp] obtain z where z: "z \<in> S" "z \<noteq> x" "dist z x < ?m"
   7.552        by blast
   7.553      from z y have "dist z y < e"
   7.554        by (intro dist_triangle_lt [where z=x]) simp
   7.555 @@ -2991,9 +2954,9 @@
   7.556          assume "m < n"
   7.557          have "dist (f(Suc n)) x = dist (y (min (inverse(2 ^ (Suc n))) (dist (f n) x))) x"
   7.558            by simp
   7.559 -        also have "... < dist (f n) x"
   7.560 +        also have "\<dots> < dist (f n) x"
   7.561            by (metis dist_pos_lt f min.strict_order_iff min_less_iff_conj y)
   7.562 -        also have "... < dist (f m) x"
   7.563 +        also have "\<dots> < dist (f m) x"
   7.564            using Suc.IH \<open>m < n\<close> by blast
   7.565          finally show ?thesis .
   7.566        next
   7.567 @@ -3127,9 +3090,9 @@
   7.568    proof -
   7.569      have "\<bar>f x\<bar> * norm (g x) \<le> \<bar>f x\<bar> * B"
   7.570        by (simp add: mult_left_mono g)
   7.571 -    also have "... \<le> \<bar>f x\<bar> * (\<bar>B\<bar> + 1)"
   7.572 +    also have "\<dots> \<le> \<bar>f x\<bar> * (\<bar>B\<bar> + 1)"
   7.573        by (simp add: mult_left_mono)
   7.574 -    also have "... < \<epsilon>"
   7.575 +    also have "\<dots> < \<epsilon>"
   7.576        by (rule f)
   7.577      finally show ?thesis .
   7.578    qed
   7.579 @@ -3290,7 +3253,7 @@
   7.580  lemma closure_approachableD:
   7.581    assumes "x \<in> closure S" "e>0"
   7.582    shows "\<exists>y\<in>S. dist x y < e"
   7.583 -  using assms unfolding closure_approachable by (auto simp add: dist_commute)
   7.584 +  using assms unfolding closure_approachable by (auto simp: dist_commute)
   7.585  
   7.586  lemma closed_approachable:
   7.587    fixes S :: "'a::metric_space set"
   7.588 @@ -5262,9 +5225,9 @@
   7.589    shows "((\<lambda>n. f (x n)) \<longlongrightarrow> f a) F"
   7.590  proof -
   7.591    have *: "filterlim x (inf (nhds a) (principal s)) F"
   7.592 -    using assms(2) assms(3) unfolding at_within_def filterlim_inf by (auto simp add: filterlim_principal eventually_mono)
   7.593 +    using assms(2) assms(3) unfolding at_within_def filterlim_inf by (auto simp: filterlim_principal eventually_mono)
   7.594    show ?thesis
   7.595 -    by (auto simp add: assms(1) continuous_within[symmetric] tendsto_at_within_iff_tendsto_nhds[symmetric] intro!: filterlim_compose[OF _ *])
   7.596 +    by (auto simp: assms(1) continuous_within[symmetric] tendsto_at_within_iff_tendsto_nhds[symmetric] intro!: filterlim_compose[OF _ *])
   7.597  qed
   7.598  
   7.599  lemma continuous_within_tendsto_compose':
   7.600 @@ -5402,7 +5365,7 @@
   7.601  
   7.602  lemma continuous_closed_imp_Cauchy_continuous:
   7.603    fixes S :: "('a::complete_space) set"
   7.604 -  shows "\<lbrakk>continuous_on S f; closed S; Cauchy \<sigma>; \<And>n. (\<sigma> n) \<in> S\<rbrakk> \<Longrightarrow> Cauchy(f o \<sigma>)"
   7.605 +  shows "\<lbrakk>continuous_on S f; closed S; Cauchy \<sigma>; \<And>n. (\<sigma> n) \<in> S\<rbrakk> \<Longrightarrow> Cauchy(f \<circ> \<sigma>)"
   7.606    apply (simp add: complete_eq_closed [symmetric] continuous_on_sequentially)
   7.607    by (meson LIMSEQ_imp_Cauchy complete_def)
   7.608  
   7.609 @@ -5876,30 +5839,20 @@
   7.610    let ?b = "\<Sum>i\<in>Basis. \<bar>a\<bullet>i\<bar> + \<bar>b\<bullet>i\<bar>"
   7.611    {
   7.612      fix x :: "'a"
   7.613 -    assume x: "\<forall>i\<in>Basis. a \<bullet> i \<le> x \<bullet> i \<and> x \<bullet> i \<le> b \<bullet> i"
   7.614 -    {
   7.615 -      fix i :: 'a
   7.616 -      assume "i \<in> Basis"
   7.617 -      then have "\<bar>x\<bullet>i\<bar> \<le> \<bar>a\<bullet>i\<bar> + \<bar>b\<bullet>i\<bar>"
   7.618 -        using x[THEN bspec[where x=i]] by auto
   7.619 -    }
   7.620 +    assume "\<And>i. i\<in>Basis \<Longrightarrow> a \<bullet> i \<le> x \<bullet> i \<and> x \<bullet> i \<le> b \<bullet> i"
   7.621      then have "(\<Sum>i\<in>Basis. \<bar>x \<bullet> i\<bar>) \<le> ?b"
   7.622 -      apply -
   7.623 -      apply (rule sum_mono, auto)
   7.624 -      done
   7.625 +      by (force simp: intro!: sum_mono)
   7.626      then have "norm x \<le> ?b"
   7.627        using norm_le_l1[of x] by auto
   7.628    }
   7.629    then show ?thesis
   7.630 -    unfolding cbox_def bounded_iff by auto
   7.631 +    unfolding cbox_def bounded_iff by force
   7.632  qed
   7.633  
   7.634  lemma bounded_box [simp]:
   7.635    fixes a :: "'a::euclidean_space"
   7.636    shows "bounded (box a b)"
   7.637 -  using bounded_cbox[of a b]
   7.638 -  using box_subset_cbox[of a b]
   7.639 -  using bounded_subset[of "cbox a b" "box a b"]
   7.640 +  using bounded_cbox[of a b] box_subset_cbox[of a b] bounded_subset[of "cbox a b" "box a b"]
   7.641    by simp
   7.642  
   7.643  lemma not_interval_UNIV [simp]:
   7.644 @@ -5923,12 +5876,8 @@
   7.645    assumes "box a b \<noteq> {}"
   7.646    shows "((1/2) *\<^sub>R (a + b)) \<in> box a b"
   7.647  proof -
   7.648 -  {
   7.649 -    fix i :: 'a
   7.650 -    assume "i \<in> Basis"
   7.651 -    then have "a \<bullet> i < ((1 / 2) *\<^sub>R (a + b)) \<bullet> i \<and> ((1 / 2) *\<^sub>R (a + b)) \<bullet> i < b \<bullet> i"
   7.652 -      using assms[unfolded box_ne_empty, THEN bspec[where x=i]] by (auto simp: inner_add_left)
   7.653 -  }
   7.654 +  have "a \<bullet> i < ((1 / 2) *\<^sub>R (a + b)) \<bullet> i \<and> ((1 / 2) *\<^sub>R (a + b)) \<bullet> i < b \<bullet> i" if "i \<in> Basis" for i
   7.655 +    using assms that by (auto simp: inner_add_left box_ne_empty)
   7.656    then show ?thesis unfolding mem_box by auto
   7.657  qed
   7.658  
   7.659 @@ -5945,14 +5894,12 @@
   7.660      have "a \<bullet> i = e * (a \<bullet> i) + (1 - e) * (a \<bullet> i)"
   7.661        unfolding left_diff_distrib by simp
   7.662      also have "\<dots> < e * (x \<bullet> i) + (1 - e) * (y \<bullet> i)"
   7.663 -      apply (rule add_less_le_mono)
   7.664 -      using e unfolding mult_less_cancel_left and mult_le_cancel_left
   7.665 -      apply simp_all
   7.666 -      using x unfolding mem_box using i
   7.667 -      apply simp
   7.668 -      using y unfolding mem_box using i
   7.669 -      apply simp
   7.670 -      done
   7.671 +    proof (rule add_less_le_mono)
   7.672 +      show "e * (a \<bullet> i) < e * (x \<bullet> i)"
   7.673 +        using \<open>0 < e\<close> i mem_box(1) x by auto
   7.674 +      show "(1 - e) * (a \<bullet> i) \<le> (1 - e) * (y \<bullet> i)"
   7.675 +        by (meson diff_ge_0_iff_ge \<open>e \<le> 1\<close> i mem_box(2) mult_left_mono y)
   7.676 +    qed
   7.677      finally have "a \<bullet> i < (e *\<^sub>R x + (1 - e) *\<^sub>R y) \<bullet> i"
   7.678        unfolding inner_simps by auto
   7.679      moreover
   7.680 @@ -5962,9 +5909,9 @@
   7.681        also have "\<dots> > e * (x \<bullet> i) + (1 - e) * (y \<bullet> i)"
   7.682        proof (rule add_less_le_mono)
   7.683          show "e * (x \<bullet> i) < e * (b \<bullet> i)"
   7.684 -          using e(1) i mem_box(1) x by auto
   7.685 +          using \<open>0 < e\<close> i mem_box(1) x by auto
   7.686          show "(1 - e) * (y \<bullet> i) \<le> (1 - e) * (b \<bullet> i)"
   7.687 -          by (meson diff_ge_0_iff_ge e(2) i mem_box(2) ordered_comm_semiring_class.comm_mult_left_mono y)
   7.688 +          by (meson diff_ge_0_iff_ge \<open>e \<le> 1\<close> i mem_box(2) mult_left_mono y)
   7.689        qed
   7.690        finally have "(e *\<^sub>R x + (1 - e) *\<^sub>R y) \<bullet> i < b \<bullet> i"
   7.691          unfolding inner_simps by auto
   7.692 @@ -6011,13 +5958,8 @@
   7.693        {
   7.694          fix e :: real
   7.695          assume "e > 0"
   7.696 -        then have "\<exists>N::nat. inverse (real (N + 1)) < e"
   7.697 -          using real_arch_inverse[of e]
   7.698 -          apply (auto simp: Suc_pred')
   7.699 -          apply (metis Suc_pred' of_nat_Suc)
   7.700 -          done
   7.701          then obtain N :: nat where N: "inverse (real (N + 1)) < e"
   7.702 -          by auto
   7.703 +          using reals_Archimedean by auto
   7.704          have "inverse (real n + 1) < e" if "N \<le> n" for n
   7.705            by (auto intro!: that le_less_trans [OF _ N])
   7.706          then have "\<exists>N::nat. \<forall>n\<ge>N. inverse (real n + 1) < e" by auto
   7.707 @@ -6031,9 +5973,8 @@
   7.708          by auto
   7.709      }
   7.710      ultimately have "x \<in> closure (box a b)"
   7.711 -      using as and box_midpoint[OF assms]
   7.712 -      unfolding closure_def
   7.713 -      unfolding islimpt_sequential
   7.714 +      using as box_midpoint[OF assms]
   7.715 +      unfolding closure_def islimpt_sequential
   7.716        by (cases "x=?c") (auto simp: in_box_eucl_less)
   7.717    }
   7.718    then show ?thesis
   7.719 @@ -6041,49 +5982,31 @@
   7.720  qed
   7.721  
   7.722  lemma bounded_subset_box_symmetric:
   7.723 -  fixes s::"('a::euclidean_space) set"
   7.724 -  assumes "bounded s"
   7.725 -  shows "\<exists>a. s \<subseteq> box (-a) a"
   7.726 +  fixes S :: "('a::euclidean_space) set"
   7.727 +  assumes "bounded S"
   7.728 +  obtains a where "S \<subseteq> box (-a) a"
   7.729  proof -
   7.730 -  obtain b where "b>0" and b: "\<forall>x\<in>s. norm x \<le> b"
   7.731 +  obtain b where "b>0" and b: "\<forall>x\<in>S. norm x \<le> b"
   7.732      using assms[unfolded bounded_pos] by auto
   7.733    define a :: 'a where "a = (\<Sum>i\<in>Basis. (b + 1) *\<^sub>R i)"
   7.734 -  {
   7.735 -    fix x
   7.736 -    assume "x \<in> s"
   7.737 -    fix i :: 'a
   7.738 -    assume i: "i \<in> Basis"
   7.739 -    then have "(-a)\<bullet>i < x\<bullet>i" and "x\<bullet>i < a\<bullet>i"
   7.740 -      using b[THEN bspec[where x=x], OF \<open>x\<in>s\<close>]
   7.741 -      using Basis_le_norm[OF i, of x]
   7.742 -      unfolding inner_simps and a_def
   7.743 -      by auto
   7.744 -  }
   7.745 -  then show ?thesis
   7.746 -    by (auto intro: exI[where x=a] simp add: box_def)
   7.747 +  have "(-a)\<bullet>i < x\<bullet>i" and "x\<bullet>i < a\<bullet>i" if "x \<in> S" and i: "i \<in> Basis" for x i
   7.748 +    using b Basis_le_norm[OF i, of x] that by (auto simp: a_def)
   7.749 +  then have "S \<subseteq> box (-a) a"
   7.750 +    by (auto simp: simp add: box_def)
   7.751 +  then show ?thesis ..
   7.752  qed
   7.753  
   7.754 -lemma bounded_subset_open_interval:
   7.755 -  fixes s :: "('a::euclidean_space) set"
   7.756 -  shows "bounded s \<Longrightarrow> (\<exists>a b. s \<subseteq> box a b)"
   7.757 -  by (auto dest!: bounded_subset_box_symmetric)
   7.758 -
   7.759  lemma bounded_subset_cbox_symmetric:
   7.760 -  fixes s :: "('a::euclidean_space) set"
   7.761 -   assumes "bounded s"
   7.762 -  shows "\<exists>a. s \<subseteq> cbox (-a) a"
   7.763 +  fixes S :: "('a::euclidean_space) set"
   7.764 +  assumes "bounded S"
   7.765 +  obtains a where "S \<subseteq> cbox (-a) a"
   7.766  proof -
   7.767 -  obtain a where "s \<subseteq> box (-a) a"
   7.768 +  obtain a where "S \<subseteq> box (-a) a"
   7.769      using bounded_subset_box_symmetric[OF assms] by auto
   7.770    then show ?thesis
   7.771 -    using box_subset_cbox[of "-a" a] by auto
   7.772 +    by (meson box_subset_cbox dual_order.trans that)
   7.773  qed
   7.774  
   7.775 -lemma bounded_subset_cbox:
   7.776 -  fixes s :: "('a::euclidean_space) set"
   7.777 -  shows "bounded s \<Longrightarrow> \<exists>a b. s \<subseteq> cbox a b"
   7.778 -  using bounded_subset_cbox_symmetric[of s] by auto
   7.779 -
   7.780  lemma frontier_cbox:
   7.781    fixes a b :: "'a::euclidean_space"
   7.782    shows "frontier (cbox a b) = cbox a b - box a b"
   7.783 @@ -6113,13 +6036,12 @@
   7.784  lemma eucl_less_eq_halfspaces:
   7.785    fixes a :: "'a::euclidean_space"
   7.786    shows "{x. x <e a} = (\<Inter>i\<in>Basis. {x. x \<bullet> i < a \<bullet> i})"
   7.787 -    "{x. a <e x} = (\<Inter>i\<in>Basis. {x. a \<bullet> i < x \<bullet> i})"
   7.788 +        "{x. a <e x} = (\<Inter>i\<in>Basis. {x. a \<bullet> i < x \<bullet> i})"
   7.789    by (auto simp: eucl_less_def)
   7.790  
   7.791  lemma open_Collect_eucl_less[simp, intro]:
   7.792    fixes a :: "'a::euclidean_space"
   7.793 -  shows "open {x. x <e a}"
   7.794 -    "open {x. a <e x}"
   7.795 +  shows "open {x. x <e a}" "open {x. a <e x}"
   7.796    by (auto simp: eucl_less_eq_halfspaces open_halfspace_component_lt open_halfspace_component_gt)
   7.797  
   7.798  no_notation