author paulson Tue Sep 27 16:24:53 2016 +0100 (2016-09-27) changeset 63945 444eafb6e864 parent 63944 21eaff8c8fc9 child 63946 d05da6b707dd
a few new theorems and a renaming
```     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"
```