a few new theorems and a renaming
authorpaulson <lp15@cam.ac.uk>
Tue Sep 27 16:24:53 2016 +0100 (2016-09-27)
changeset 63945444eafb6e864
parent 63944 21eaff8c8fc9
child 63946 d05da6b707dd
a few new theorems and a renaming
src/HOL/Analysis/Cartesian_Euclidean_Space.thy
src/HOL/Analysis/Convex_Euclidean_Space.thy
src/HOL/Analysis/Equivalence_Lebesgue_Henstock_Integration.thy
src/HOL/Analysis/Henstock_Kurzweil_Integration.thy
src/HOL/Analysis/Homeomorphism.thy
src/HOL/Analysis/Topology_Euclidean_Space.thy
src/HOL/Archimedean_Field.thy
     1.1 --- a/src/HOL/Analysis/Cartesian_Euclidean_Space.thy	Mon Sep 26 16:57:05 2016 +0200
     1.2 +++ b/src/HOL/Analysis/Cartesian_Euclidean_Space.thy	Tue Sep 27 16:24:53 2016 +0100
     1.3 @@ -1085,7 +1085,7 @@
     1.4  lemma inter_interval_cart:
     1.5    fixes a :: "real^'n"
     1.6    shows "cbox a b \<inter> cbox c d =  {(\<chi> i. max (a$i) (c$i)) .. (\<chi> i. min (b$i) (d$i))}"
     1.7 -  unfolding inter_interval
     1.8 +  unfolding Int_interval
     1.9    by (auto simp: mem_box less_eq_vec_def)
    1.10      (auto simp: Basis_vec_def inner_axis)
    1.11  
     2.1 --- a/src/HOL/Analysis/Convex_Euclidean_Space.thy	Mon Sep 26 16:57:05 2016 +0200
     2.2 +++ b/src/HOL/Analysis/Convex_Euclidean_Space.thy	Tue Sep 27 16:24:53 2016 +0100
     2.3 @@ -7748,6 +7748,22 @@
     2.4      using rel_interior_empty by auto
     2.5  qed
     2.6  
     2.7 +lemma interior_simplex_nonempty:
     2.8 +  fixes S :: "'N :: euclidean_space set"
     2.9 +  assumes "independent S" "finite S" "card S = DIM('N)"
    2.10 +  obtains a where "a \<in> interior (convex hull (insert 0 S))"
    2.11 +proof -
    2.12 +  have "affine hull (insert 0 S) = UNIV"
    2.13 +    apply (simp add: hull_inc affine_hull_span_0)
    2.14 +    using assms dim_eq_full indep_card_eq_dim_span by fastforce
    2.15 +  moreover have "rel_interior (convex hull insert 0 S) \<noteq> {}"
    2.16 +    using rel_interior_eq_empty [of "convex hull (insert 0 S)"] by auto
    2.17 +  ultimately have "interior (convex hull insert 0 S) \<noteq> {}"
    2.18 +    by (simp add: rel_interior_interior)
    2.19 +  with that show ?thesis
    2.20 +    by auto
    2.21 +qed
    2.22 +
    2.23  lemma convex_rel_interior:
    2.24    fixes S :: "'n::euclidean_space set"
    2.25    assumes "convex S"
     3.1 --- a/src/HOL/Analysis/Equivalence_Lebesgue_Henstock_Integration.thy	Mon Sep 26 16:57:05 2016 +0200
     3.2 +++ b/src/HOL/Analysis/Equivalence_Lebesgue_Henstock_Integration.thy	Tue Sep 27 16:24:53 2016 +0100
     3.3 @@ -1108,7 +1108,7 @@
     3.4          show "\<exists>a b. k = cbox a b"
     3.5            unfolding il using p'(4)[OF il(3)] d'(4)[OF il(2)]
     3.6            apply safe
     3.7 -          unfolding inter_interval
     3.8 +          unfolding Int_interval
     3.9            apply auto
    3.10            done
    3.11        next
    3.12 @@ -1288,7 +1288,7 @@
    3.13              from d'(4)[OF k] snd_p(4)[OF prems(1)] guess u1 v1 u2 v2 by (elim exE) note uv=this
    3.14              show ?case
    3.15                using *
    3.16 -              unfolding uv inter_interval content_eq_0_interior[symmetric]
    3.17 +              unfolding uv Int_interval content_eq_0_interior[symmetric]
    3.18                by auto
    3.19            qed
    3.20            finally show ?case .
    3.21 @@ -1338,7 +1338,7 @@
    3.22            ultimately have "interior(l1 \<inter> k1) = {}"
    3.23              by auto
    3.24            then show "norm (integral (l1 \<inter> k1) f) = 0"
    3.25 -            unfolding uv inter_interval
    3.26 +            unfolding uv Int_interval
    3.27              unfolding content_eq_0_interior[symmetric]
    3.28              by auto
    3.29          qed
    3.30 @@ -1429,7 +1429,7 @@
    3.31            ultimately have "interior (l1 \<inter> k1) = {}"
    3.32              by auto
    3.33            then show "\<bar>content (l1 \<inter> k1)\<bar> * norm (f x1) = 0"
    3.34 -            unfolding uv inter_interval
    3.35 +            unfolding uv Int_interval
    3.36              unfolding content_eq_0_interior[symmetric]
    3.37              by auto
    3.38          qed safe
    3.39 @@ -1453,7 +1453,7 @@
    3.40              apply (drule d'(4))
    3.41              apply safe
    3.42              apply (subst Int_commute)
    3.43 -            unfolding inter_interval uv
    3.44 +            unfolding Int_interval uv
    3.45              apply (subst abs_of_nonneg)
    3.46              apply auto
    3.47              done
    3.48 @@ -1475,7 +1475,7 @@
    3.49              also have "\<dots> = interior (k \<inter> cbox u v)"
    3.50                unfolding prems(4) by auto
    3.51              finally show ?case
    3.52 -              unfolding uv inter_interval content_eq_0_interior ..
    3.53 +              unfolding uv Int_interval content_eq_0_interior ..
    3.54            qed
    3.55            also have "\<dots> = setsum content {cbox u v \<inter> k |k. k \<in> d \<and> cbox u v \<inter> k \<noteq> {}}"
    3.56              apply (rule setsum.mono_neutral_right)
    3.57 @@ -1490,7 +1490,7 @@
    3.58              from d'(4)[OF this(1)] guess a b by (elim exE) note ab=this
    3.59              have "interior (k \<inter> cbox u v) \<noteq> {}"
    3.60                using prems(2)
    3.61 -              unfolding ab inter_interval content_eq_0_interior
    3.62 +              unfolding ab Int_interval content_eq_0_interior
    3.63                by auto
    3.64              then show ?case
    3.65                using prems(1)
     4.1 --- a/src/HOL/Analysis/Henstock_Kurzweil_Integration.thy	Mon Sep 26 16:57:05 2016 +0200
     4.2 +++ b/src/HOL/Analysis/Henstock_Kurzweil_Integration.thy	Tue Sep 27 16:24:53 2016 +0100
     4.3 @@ -503,7 +503,7 @@
     4.4        obtain a2 b2 where k2: "k2 = cbox a2 b2"
     4.5          using division_ofD(4)[OF assms(2) k(3)] by blast
     4.6        show "\<exists>a b. k = cbox a b"
     4.7 -        unfolding k k1 k2 unfolding inter_interval by auto
     4.8 +        unfolding k k1 k2 unfolding Int_interval by auto
     4.9      }
    4.10      fix k1 k2
    4.11      assume "k1 \<in> ?A"
    4.12 @@ -826,7 +826,7 @@
    4.13    next
    4.14      case False
    4.15      obtain u v where uv: "cbox a b \<inter> cbox c d = cbox u v"
    4.16 -      unfolding inter_interval by auto
    4.17 +      unfolding Int_interval by auto
    4.18      have uv_sub: "cbox u v \<subseteq> cbox c d" using uv by auto
    4.19      obtain p where "p division_of cbox c d" "cbox u v \<in> p"
    4.20        by (rule partial_division_extend_1[OF uv_sub False[unfolded uv]])
    4.21 @@ -4733,34 +4733,21 @@
    4.22  
    4.23  subsection \<open>Some other trivialities about negligible sets.\<close>
    4.24  
    4.25 -lemma negligible_subset[intro]:
    4.26 -  assumes "negligible s"
    4.27 -    and "t \<subseteq> s"
    4.28 +lemma negligible_subset:
    4.29 +  assumes "negligible s" "t \<subseteq> s"
    4.30    shows "negligible t"
    4.31    unfolding negligible_def
    4.32 -proof (safe, goal_cases)
    4.33 -  case (1 a b)
    4.34 -  show ?case
    4.35 -    using assms(1)[unfolded negligible_def,rule_format,of a b]
    4.36 -    apply -
    4.37 -    apply (rule has_integral_spike[OF assms(1)])
    4.38 -    defer
    4.39 -    apply assumption
    4.40 -    using assms(2)
    4.41 -    unfolding indicator_def
    4.42 -    apply auto
    4.43 -    done
    4.44 -qed
    4.45 +    by (metis (no_types) Diff_iff assms contra_subsetD has_integral_negligible indicator_simps(2))
    4.46  
    4.47  lemma negligible_diff[intro?]:
    4.48    assumes "negligible s"
    4.49    shows "negligible (s - t)"
    4.50 -  using assms by auto
    4.51 +  using assms by (meson Diff_subset negligible_subset)
    4.52  
    4.53  lemma negligible_Int:
    4.54    assumes "negligible s \<or> negligible t"
    4.55    shows "negligible (s \<inter> t)"
    4.56 -  using assms by auto
    4.57 +  using assms negligible_subset by force
    4.58  
    4.59  lemma negligible_Un:
    4.60    assumes "negligible s"
    4.61 @@ -4780,10 +4767,10 @@
    4.62  qed
    4.63  
    4.64  lemma negligible_Un_eq[simp]: "negligible (s \<union> t) \<longleftrightarrow> negligible s \<and> negligible t"
    4.65 -  using negligible_Un by auto
    4.66 +  using negligible_Un negligible_subset by blast 
    4.67  
    4.68  lemma negligible_sing[intro]: "negligible {a::'a::euclidean_space}"
    4.69 -  using negligible_standard_hyperplane[OF SOME_Basis, of "a \<bullet> (SOME i. i \<in> Basis)"] by auto
    4.70 +  using negligible_standard_hyperplane[OF SOME_Basis, of "a \<bullet> (SOME i. i \<in> Basis)"] negligible_subset by blast
    4.71  
    4.72  lemma negligible_insert[simp]: "negligible (insert a s) \<longleftrightarrow> negligible s"
    4.73    apply (subst insert_is_Un)
    4.74 @@ -4792,7 +4779,7 @@
    4.75    done
    4.76  
    4.77  lemma negligible_empty[iff]: "negligible {}"
    4.78 -  by auto
    4.79 +  using negligible_insert by blast
    4.80  
    4.81  lemma negligible_finite[intro]:
    4.82    assumes "finite s"
    4.83 @@ -7652,7 +7639,7 @@
    4.84        apply auto
    4.85        done
    4.86    qed
    4.87 -qed auto
    4.88 +qed (simp add: negligible_Int)
    4.89  
    4.90  lemma negligible_translation:
    4.91    assumes "negligible S"
    4.92 @@ -7689,32 +7676,24 @@
    4.93    apply (rule has_integral_spike_eq[OF assms])
    4.94    by (auto split: if_split_asm)
    4.95  
    4.96 -lemma has_integral_spike_set[dest]:
    4.97 +lemma has_integral_spike_set:
    4.98    fixes f :: "'n::euclidean_space \<Rightarrow> 'a::banach"
    4.99 -  assumes "negligible ((s - t) \<union> (t - s))"
   4.100 -    and "(f has_integral y) s"
   4.101 +  assumes "(f has_integral y) s" "negligible ((s - t) \<union> (t - s))"
   4.102    shows "(f has_integral y) t"
   4.103    using assms has_integral_spike_set_eq
   4.104    by auto
   4.105  
   4.106 -lemma integrable_spike_set[dest]:
   4.107 +lemma integrable_spike_set:
   4.108    fixes f :: "'n::euclidean_space \<Rightarrow> 'a::banach"
   4.109 -  assumes "negligible ((s - t) \<union> (t - s))"
   4.110 -    and "f integrable_on s"
   4.111 -  shows "f integrable_on t"
   4.112 -  using assms(2)
   4.113 -  unfolding integrable_on_def
   4.114 -  unfolding has_integral_spike_set_eq[OF assms(1)] .
   4.115 +  assumes "f integrable_on s" and "negligible ((s - t) \<union> (t - s))"
   4.116 +    shows "f integrable_on t"
   4.117 +  using assms by (simp add: integrable_on_def has_integral_spike_set_eq)
   4.118  
   4.119  lemma integrable_spike_set_eq:
   4.120    fixes f :: "'n::euclidean_space \<Rightarrow> 'a::banach"
   4.121    assumes "negligible ((s - t) \<union> (t - s))"
   4.122    shows "f integrable_on s \<longleftrightarrow> f integrable_on t"
   4.123 -  apply rule
   4.124 -  apply (rule_tac[!] integrable_spike_set)
   4.125 -  using assms
   4.126 -  apply auto
   4.127 -  done
   4.128 +by (blast intro: integrable_spike_set assms negligible_subset)
   4.129  
   4.130  (*lemma integral_spike_set:
   4.131   "\<forall>f:real^M->real^N g s t.
     5.1 --- a/src/HOL/Analysis/Homeomorphism.thy	Mon Sep 26 16:57:05 2016 +0200
     5.2 +++ b/src/HOL/Analysis/Homeomorphism.thy	Tue Sep 27 16:24:53 2016 +0100
     5.3 @@ -973,6 +973,52 @@
     5.4  by (metis closed_closure closed_imp_locally_compact inf_commute locally_compact_Int locally_compact_open_Int_closure open_imp_locally_compact)
     5.5  
     5.6  
     5.7 +lemma lowerdim_embeddings:
     5.8 +  assumes  "DIM('a) < DIM('b)"
     5.9 +  obtains f :: "'a::euclidean_space*real \<Rightarrow> 'b::euclidean_space" 
    5.10 +      and g :: "'b \<Rightarrow> 'a*real"
    5.11 +      and j :: 'b
    5.12 +  where "linear f" "linear g" "\<And>z. g (f z) = z" "j \<in> Basis" "\<And>x. f(x,0) \<bullet> j = 0"
    5.13 +proof -
    5.14 +  let ?B = "Basis :: ('a*real) set"
    5.15 +  have b01: "(0,1) \<in> ?B"
    5.16 +    by (simp add: Basis_prod_def)
    5.17 +  have "DIM('a * real) \<le> DIM('b)"
    5.18 +    by (simp add: Suc_leI assms)
    5.19 +  then obtain basf :: "'a*real \<Rightarrow> 'b" where sbf: "basf ` ?B \<subseteq> Basis" and injbf: "inj_on basf Basis"
    5.20 +    by (metis finite_Basis card_le_inj)
    5.21 +  define basg:: "'b \<Rightarrow> 'a * real" where
    5.22 +    "basg \<equiv> \<lambda>i. if i \<in> basf ` Basis then inv_into Basis basf i else (0,1)"
    5.23 +  have bgf[simp]: "basg (basf i) = i" if "i \<in> Basis" for i
    5.24 +    using inv_into_f_f injbf that by (force simp: basg_def)
    5.25 +  have sbg: "basg ` Basis \<subseteq> ?B" 
    5.26 +    by (force simp: basg_def injbf b01)
    5.27 +  define f :: "'a*real \<Rightarrow> 'b" where "f \<equiv> \<lambda>u. \<Sum>j\<in>Basis. (u \<bullet> basg j) *\<^sub>R j"
    5.28 +  define g :: "'b \<Rightarrow> 'a*real" where "g \<equiv> \<lambda>z. (\<Sum>i\<in>Basis. (z \<bullet> basf i) *\<^sub>R i)" 
    5.29 +  show ?thesis
    5.30 +  proof
    5.31 +    show "linear f"
    5.32 +      unfolding f_def
    5.33 +      by (intro linear_compose_setsum linearI ballI) (auto simp: algebra_simps)
    5.34 +    show "linear g"
    5.35 +      unfolding g_def
    5.36 +      by (intro linear_compose_setsum linearI ballI) (auto simp: algebra_simps)
    5.37 +    have *: "(\<Sum>a \<in> Basis. a \<bullet> basf b * (x \<bullet> basg a)) = x \<bullet> b" if "b \<in> Basis" for x b
    5.38 +      using sbf that by auto
    5.39 +    show gf: "g (f x) = x" for x
    5.40 +      apply (rule euclidean_eqI)
    5.41 +      apply (simp add: f_def g_def inner_setsum_left scaleR_setsum_left algebra_simps)
    5.42 +      apply (simp add: Groups_Big.setsum_distrib_left [symmetric] *)
    5.43 +      done
    5.44 +    show "basf(0,1) \<in> Basis"
    5.45 +      using b01 sbf by auto
    5.46 +    then show "f(x,0) \<bullet> basf(0,1) = 0" for x
    5.47 +      apply (simp add: f_def inner_setsum_left)
    5.48 +      apply (rule comm_monoid_add_class.setsum.neutral)
    5.49 +      using b01 inner_not_same_Basis by fastforce
    5.50 +  qed
    5.51 +qed
    5.52 +
    5.53  proposition locally_compact_homeomorphic_closed:
    5.54    fixes S :: "'a::euclidean_space set"
    5.55    assumes "locally compact S" and dimlt: "DIM('a) < DIM('b)"
    5.56 @@ -981,45 +1027,21 @@
    5.57    obtain U:: "('a*real)set" and h
    5.58      where "closed U" and homU: "homeomorphism S U h fst"
    5.59      using locally_compact_homeomorphism_projection_closed assms by metis
    5.60 -  let ?BP = "Basis :: ('a*real) set"
    5.61 -  have "DIM('a * real) \<le> DIM('b)"
    5.62 -    by (simp add: Suc_leI dimlt)
    5.63 -  then obtain basf :: "'a*real \<Rightarrow> 'b" where surbf: "basf ` ?BP \<subseteq> Basis" and injbf: "inj_on basf Basis"
    5.64 -    by (metis finite_Basis card_le_inj)
    5.65 -  define basg:: "'b \<Rightarrow> 'a * real" where
    5.66 -    "basg \<equiv> \<lambda>i. inv_into Basis basf i"
    5.67 -  have bgf[simp]: "basg (basf i) = i" if "i \<in> Basis" for i
    5.68 -    using inv_into_f_f injbf that by (force simp: basg_def)
    5.69 -  define f :: "'a*real \<Rightarrow> 'b" where "f \<equiv> \<lambda>u. \<Sum>j\<in>Basis. (u \<bullet> basg j) *\<^sub>R j"
    5.70 -  have "linear f"
    5.71 -    unfolding f_def
    5.72 -    apply (intro linear_compose_setsum linearI ballI)
    5.73 -    apply (auto simp: algebra_simps)
    5.74 -    done
    5.75 -  define g :: "'b \<Rightarrow> 'a*real" where "g \<equiv> \<lambda>z. (\<Sum>i\<in>Basis. (z \<bullet> basf i) *\<^sub>R i)"
    5.76 -  have "linear g"
    5.77 -    unfolding g_def
    5.78 -    apply (intro linear_compose_setsum linearI ballI)
    5.79 -    apply (auto simp: algebra_simps)
    5.80 -    done
    5.81 -  have *: "(\<Sum>a \<in> Basis. a \<bullet> basf b * (x \<bullet> basg a)) = x \<bullet> b" if "b \<in> Basis" for x b
    5.82 -    using surbf that by auto
    5.83 -  have gf[simp]: "g (f x) = x" for x
    5.84 -    apply (rule euclidean_eqI)
    5.85 -    apply (simp add: f_def g_def inner_setsum_left scaleR_setsum_left algebra_simps)
    5.86 -    apply (simp add: Groups_Big.setsum_distrib_left [symmetric] *)
    5.87 -    done
    5.88 -  then have "inj f" by (metis injI)
    5.89 +  obtain f :: "'a*real \<Rightarrow> 'b" and g :: "'b \<Rightarrow> 'a*real"
    5.90 +    where "linear f" "linear g" and gf [simp]: "\<And>z. g (f z) = z"
    5.91 +    using lowerdim_embeddings [OF dimlt] by metis 
    5.92 +  then have "inj f"
    5.93 +    by (metis injI)
    5.94    have gfU: "g ` f ` U = U"
    5.95 -    by (rule set_eqI) (auto simp: image_def)
    5.96 +    by (simp add: image_comp o_def)
    5.97    have "S homeomorphic U"
    5.98      using homU homeomorphic_def by blast
    5.99    also have "... homeomorphic f ` U"
   5.100      apply (rule homeomorphicI [OF refl gfU])
   5.101         apply (meson \<open>inj f\<close> \<open>linear f\<close> homeomorphism_cont2 linear_homeomorphism_image)
   5.102 -      using \<open>linear g\<close> linear_continuous_on linear_conv_bounded_linear apply blast
   5.103 -     apply auto
   5.104 -     done
   5.105 +    using \<open>linear g\<close> linear_continuous_on linear_conv_bounded_linear apply blast
   5.106 +    apply (auto simp: o_def)
   5.107 +    done
   5.108    finally show ?thesis
   5.109      apply (rule_tac T = "f ` U" in that)
   5.110      apply (rule closed_injective_linear_image [OF \<open>closed U\<close> \<open>linear f\<close> \<open>inj f\<close>], assumption)
     6.1 --- a/src/HOL/Analysis/Topology_Euclidean_Space.thy	Mon Sep 26 16:57:05 2016 +0200
     6.2 +++ b/src/HOL/Analysis/Topology_Euclidean_Space.thy	Tue Sep 27 16:24:53 2016 +0100
     6.3 @@ -1388,7 +1388,59 @@
     6.4      done
     6.5  qed
     6.6  
     6.7 -lemma inter_interval:
     6.8 +lemma eq_cbox: "cbox a b = cbox c d \<longleftrightarrow> cbox a b = {} \<and> cbox c d = {} \<or> a = c \<and> b = d"
     6.9 +      (is "?lhs = ?rhs")
    6.10 +proof
    6.11 +  assume ?lhs
    6.12 +  then have "cbox a b \<subseteq> cbox c d" "cbox c d \<subseteq> cbox a b"
    6.13 +    by auto
    6.14 +  then show ?rhs
    6.15 +    by (force simp add: subset_box box_eq_empty intro: antisym euclidean_eqI)
    6.16 +next
    6.17 +  assume ?rhs
    6.18 +  then show ?lhs
    6.19 +    by force
    6.20 +qed
    6.21 +
    6.22 +lemma eq_cbox_box [simp]: "cbox a b = box c d \<longleftrightarrow> cbox a b = {} \<and> box c d = {}"
    6.23 +      (is "?lhs = ?rhs")
    6.24 +proof
    6.25 +  assume ?lhs
    6.26 +  then have "cbox a b \<subseteq> box c d" "box c d \<subseteq>cbox a b"
    6.27 +    by auto
    6.28 +  then show ?rhs
    6.29 +    apply (simp add: subset_box) 
    6.30 +    using \<open>cbox a b = box c d\<close> box_ne_empty box_sing
    6.31 +    apply (fastforce simp add:)
    6.32 +    done
    6.33 +next
    6.34 +  assume ?rhs
    6.35 +  then show ?lhs
    6.36 +    by force
    6.37 +qed
    6.38 +
    6.39 +lemma eq_box_cbox [simp]: "box a b = cbox c d \<longleftrightarrow> box a b = {} \<and> cbox c d = {}"
    6.40 +  by (metis eq_cbox_box)
    6.41 +
    6.42 +lemma eq_box: "box a b = box c d \<longleftrightarrow> box a b = {} \<and> box c d = {} \<or> a = c \<and> b = d"
    6.43 +      (is "?lhs = ?rhs")
    6.44 +proof
    6.45 +  assume ?lhs
    6.46 +  then have "box a b \<subseteq> box c d" "box c d \<subseteq> box a b"
    6.47 +    by auto
    6.48 +  then show ?rhs
    6.49 +    apply (simp add: subset_box)
    6.50 +    using box_ne_empty(2) \<open>box a b = box c d\<close> 
    6.51 +    apply auto
    6.52 +     apply (meson euclidean_eqI less_eq_real_def not_less)+
    6.53 +    done
    6.54 +next
    6.55 +  assume ?rhs
    6.56 +  then show ?lhs
    6.57 +    by force
    6.58 +qed
    6.59 +
    6.60 +lemma Int_interval:
    6.61    fixes a :: "'a::euclidean_space"
    6.62    shows "cbox a b \<inter> cbox c d =
    6.63      cbox (\<Sum>i\<in>Basis. max (a\<bullet>i) (c\<bullet>i) *\<^sub>R i) (\<Sum>i\<in>Basis. min (b\<bullet>i) (d\<bullet>i) *\<^sub>R i)"
    6.64 @@ -8077,6 +8129,11 @@
    6.65    shows "cbox a b \<noteq> UNIV" "box a b \<noteq> UNIV"
    6.66    using bounded_box[of a b] bounded_cbox[of a b] by force+
    6.67  
    6.68 +lemma not_interval_UNIV2 [simp]:
    6.69 +  fixes a :: "'a::euclidean_space"
    6.70 +  shows "UNIV \<noteq> cbox a b" "UNIV \<noteq> box a b"
    6.71 +  using bounded_box[of a b] bounded_cbox[of a b] by force+
    6.72 +
    6.73  lemma compact_cbox [simp]:
    6.74    fixes a :: "'a::euclidean_space"
    6.75    shows "compact (cbox a b)"
    6.76 @@ -9057,7 +9114,7 @@
    6.77    shows "closed (span s)"
    6.78  by (simp add: closed_subspace subspace_span)
    6.79  
    6.80 -lemma dim_closure:
    6.81 +lemma dim_closure [simp]:
    6.82    fixes s :: "('a::euclidean_space) set"
    6.83    shows "dim(closure s) = dim s" (is "?dc = ?d")
    6.84  proof -
     7.1 --- a/src/HOL/Archimedean_Field.thy	Mon Sep 26 16:57:05 2016 +0200
     7.2 +++ b/src/HOL/Archimedean_Field.thy	Tue Sep 27 16:24:53 2016 +0100
     7.3 @@ -619,6 +619,15 @@
     7.4    unfolding ceiling_def by simp
     7.5  
     7.6  
     7.7 +subsection \<open>Natural numbers\<close>
     7.8 +
     7.9 +lemma of_nat_floor: "r\<ge>0 \<Longrightarrow> of_nat (nat \<lfloor>r\<rfloor>) \<le> r"
    7.10 +  by simp
    7.11 +
    7.12 +lemma of_nat_ceiling: "of_nat (nat \<lceil>r\<rceil>) \<ge> r"
    7.13 +  by (cases "r\<ge>0") auto
    7.14 +
    7.15 +
    7.16  subsection \<open>Frac Function\<close>
    7.17  
    7.18  definition frac :: "'a \<Rightarrow> 'a::floor_ceiling"