src/HOL/RComplete.thy
author wenzelm
Fri Jan 14 15:44:47 2011 +0100 (2011-01-14)
changeset 41550 efa734d9b221
parent 37887 2ae085b07f2f
child 44667 ee5772ca7d16
permissions -rw-r--r--
eliminated global prems;
tuned proofs;
wenzelm@30122
     1
(*  Title:      HOL/RComplete.thy
wenzelm@30122
     2
    Author:     Jacques D. Fleuriot, University of Edinburgh
wenzelm@30122
     3
    Author:     Larry Paulson, University of Cambridge
wenzelm@30122
     4
    Author:     Jeremy Avigad, Carnegie Mellon University
wenzelm@30122
     5
    Author:     Florian Zuleger, Johannes Hoelzl, and Simon Funke, TU Muenchen
wenzelm@16893
     6
*)
paulson@5078
     7
wenzelm@16893
     8
header {* Completeness of the Reals; Floor and Ceiling Functions *}
paulson@14365
     9
nipkow@15131
    10
theory RComplete
nipkow@15140
    11
imports Lubs RealDef
nipkow@15131
    12
begin
paulson@14365
    13
paulson@14365
    14
lemma real_sum_of_halves: "x/2 + x/2 = (x::real)"
wenzelm@16893
    15
  by simp
paulson@14365
    16
paulson@32707
    17
lemma abs_diff_less_iff:
haftmann@35028
    18
  "(\<bar>x - a\<bar> < (r::'a::linordered_idom)) = (a - r < x \<and> x < a + r)"
paulson@32707
    19
  by auto
paulson@14365
    20
wenzelm@16893
    21
subsection {* Completeness of Positive Reals *}
wenzelm@16893
    22
wenzelm@16893
    23
text {*
wenzelm@16893
    24
  Supremum property for the set of positive reals
wenzelm@16893
    25
wenzelm@16893
    26
  Let @{text "P"} be a non-empty set of positive reals, with an upper
wenzelm@16893
    27
  bound @{text "y"}.  Then @{text "P"} has a least upper bound
wenzelm@16893
    28
  (written @{text "S"}).
paulson@14365
    29
wenzelm@16893
    30
  FIXME: Can the premise be weakened to @{text "\<forall>x \<in> P. x\<le> y"}?
wenzelm@16893
    31
*}
wenzelm@16893
    32
huffman@36795
    33
text {* Only used in HOL/Import/HOL4Compat.thy; delete? *}
huffman@36795
    34
wenzelm@16893
    35
lemma posreal_complete:
wenzelm@16893
    36
  assumes positive_P: "\<forall>x \<in> P. (0::real) < x"
wenzelm@16893
    37
    and not_empty_P: "\<exists>x. x \<in> P"
wenzelm@16893
    38
    and upper_bound_Ex: "\<exists>y. \<forall>x \<in> P. x<y"
wenzelm@16893
    39
  shows "\<exists>S. \<forall>y. (\<exists>x \<in> P. y < x) = (y < S)"
huffman@36795
    40
proof -
huffman@36795
    41
  from upper_bound_Ex have "\<exists>z. \<forall>x\<in>P. x \<le> z"
huffman@36795
    42
    by (auto intro: less_imp_le)
huffman@36795
    43
  from complete_real [OF not_empty_P this] obtain S
huffman@36795
    44
  where S1: "\<And>x. x \<in> P \<Longrightarrow> x \<le> S" and S2: "\<And>z. \<forall>x\<in>P. x \<le> z \<Longrightarrow> S \<le> z" by fast
huffman@36795
    45
  have "\<forall>y. (\<exists>x \<in> P. y < x) = (y < S)"
huffman@36795
    46
  proof
huffman@36795
    47
    fix y show "(\<exists>x\<in>P. y < x) = (y < S)"
huffman@36795
    48
      apply (cases "\<exists>x\<in>P. y < x", simp_all)
huffman@36795
    49
      apply (clarify, drule S1, simp)
huffman@36795
    50
      apply (simp add: not_less S2)
huffman@36795
    51
      done
wenzelm@16893
    52
  qed
huffman@36795
    53
  thus ?thesis ..
wenzelm@16893
    54
qed
wenzelm@16893
    55
wenzelm@16893
    56
text {*
wenzelm@16893
    57
  \medskip Completeness properties using @{text "isUb"}, @{text "isLub"} etc.
wenzelm@16893
    58
*}
paulson@14365
    59
paulson@14365
    60
lemma real_isLub_unique: "[| isLub R S x; isLub R S y |] ==> x = (y::real)"
wenzelm@16893
    61
  apply (frule isLub_isUb)
wenzelm@16893
    62
  apply (frule_tac x = y in isLub_isUb)
wenzelm@16893
    63
  apply (blast intro!: order_antisym dest!: isLub_le_isUb)
wenzelm@16893
    64
  done
paulson@14365
    65
paulson@5078
    66
wenzelm@16893
    67
text {*
wenzelm@16893
    68
  \medskip reals Completeness (again!)
wenzelm@16893
    69
*}
paulson@14365
    70
wenzelm@16893
    71
lemma reals_complete:
wenzelm@16893
    72
  assumes notempty_S: "\<exists>X. X \<in> S"
wenzelm@16893
    73
    and exists_Ub: "\<exists>Y. isUb (UNIV::real set) S Y"
wenzelm@16893
    74
  shows "\<exists>t. isLub (UNIV :: real set) S t"
wenzelm@16893
    75
proof -
huffman@36795
    76
  from assms have "\<exists>X. X \<in> S" and "\<exists>Y. \<forall>x\<in>S. x \<le> Y"
huffman@36795
    77
    unfolding isUb_def setle_def by simp_all
huffman@36795
    78
  from complete_real [OF this] show ?thesis
huffman@36795
    79
    unfolding isLub_def leastP_def setle_def setge_def Ball_def
huffman@36795
    80
      Collect_def mem_def isUb_def UNIV_def by simp
wenzelm@16893
    81
qed
paulson@14365
    82
paulson@32707
    83
text{*A version of the same theorem without all those predicates!*}
paulson@32707
    84
lemma reals_complete2:
paulson@32707
    85
  fixes S :: "(real set)"
paulson@32707
    86
  assumes "\<exists>y. y\<in>S" and "\<exists>(x::real). \<forall>y\<in>S. y \<le> x"
paulson@32707
    87
  shows "\<exists>x. (\<forall>y\<in>S. y \<le> x) & 
paulson@32707
    88
               (\<forall>z. ((\<forall>y\<in>S. y \<le> z) --> x \<le> z))"
huffman@36795
    89
using assms by (rule complete_real)
paulson@32707
    90
paulson@14365
    91
wenzelm@16893
    92
subsection {* The Archimedean Property of the Reals *}
wenzelm@16893
    93
wenzelm@16893
    94
theorem reals_Archimedean:
wenzelm@16893
    95
  assumes x_pos: "0 < x"
wenzelm@16893
    96
  shows "\<exists>n. inverse (real (Suc n)) < x"
huffman@36795
    97
  unfolding real_of_nat_def using x_pos
huffman@36795
    98
  by (rule ex_inverse_of_nat_Suc_less)
paulson@14365
    99
paulson@14365
   100
lemma reals_Archimedean2: "\<exists>n. (x::real) < real (n::nat)"
huffman@36795
   101
  unfolding real_of_nat_def by (rule ex_less_of_nat)
huffman@30097
   102
wenzelm@16893
   103
lemma reals_Archimedean3:
wenzelm@16893
   104
  assumes x_greater_zero: "0 < x"
wenzelm@16893
   105
  shows "\<forall>(y::real). \<exists>(n::nat). y < real n * x"
huffman@30097
   106
  unfolding real_of_nat_def using `0 < x`
huffman@30097
   107
  by (auto intro: ex_less_of_nat_mult)
paulson@14365
   108
avigad@16819
   109
lemma reals_Archimedean6:
avigad@16819
   110
     "0 \<le> r ==> \<exists>(n::nat). real (n - 1) \<le> r & r < real (n)"
huffman@30097
   111
unfolding real_of_nat_def
huffman@30097
   112
apply (rule exI [where x="nat (floor r + 1)"])
huffman@30097
   113
apply (insert floor_correct [of r])
huffman@30097
   114
apply (simp add: nat_add_distrib of_nat_nat)
avigad@16819
   115
done
avigad@16819
   116
avigad@16819
   117
lemma reals_Archimedean6a: "0 \<le> r ==> \<exists>n. real (n) \<le> r & r < real (Suc n)"
wenzelm@16893
   118
  by (drule reals_Archimedean6) auto
avigad@16819
   119
huffman@36979
   120
text {* TODO: delete *}
avigad@16819
   121
lemma reals_Archimedean_6b_int:
avigad@16819
   122
     "0 \<le> r ==> \<exists>n::int. real n \<le> r & r < real (n+1)"
huffman@30097
   123
  unfolding real_of_int_def by (rule floor_exists)
avigad@16819
   124
huffman@36979
   125
text {* TODO: delete *}
avigad@16819
   126
lemma reals_Archimedean_6c_int:
avigad@16819
   127
     "r < 0 ==> \<exists>n::int. real n \<le> r & r < real (n+1)"
huffman@30097
   128
  unfolding real_of_int_def by (rule floor_exists)
avigad@16819
   129
avigad@16819
   130
nipkow@28091
   131
subsection{*Density of the Rational Reals in the Reals*}
nipkow@28091
   132
nipkow@28091
   133
text{* This density proof is due to Stefan Richter and was ported by TN.  The
nipkow@28091
   134
original source is \emph{Real Analysis} by H.L. Royden.
nipkow@28091
   135
It employs the Archimedean property of the reals. *}
nipkow@28091
   136
nipkow@28091
   137
lemma Rats_dense_in_nn_real: fixes x::real
nipkow@28091
   138
assumes "0\<le>x" and "x<y" shows "\<exists>r \<in> \<rat>.  x<r \<and> r<y"
nipkow@28091
   139
proof -
nipkow@28091
   140
  from `x<y` have "0 < y-x" by simp
nipkow@28091
   141
  with reals_Archimedean obtain q::nat 
nipkow@28091
   142
    where q: "inverse (real q) < y-x" and "0 < real q" by auto  
nipkow@28091
   143
  def p \<equiv> "LEAST n.  y \<le> real (Suc n)/real q"  
nipkow@28091
   144
  from reals_Archimedean2 obtain n::nat where "y * real q < real n" by auto
nipkow@28091
   145
  with `0 < real q` have ex: "y \<le> real n/real q" (is "?P n")
nipkow@28091
   146
    by (simp add: pos_less_divide_eq[THEN sym])
nipkow@28091
   147
  also from assms have "\<not> y \<le> real (0::nat) / real q" by simp
nipkow@28091
   148
  ultimately have main: "(LEAST n. y \<le> real n/real q) = Suc p"
nipkow@28091
   149
    by (unfold p_def) (rule Least_Suc)
nipkow@28091
   150
  also from ex have "?P (LEAST x. ?P x)" by (rule LeastI)
nipkow@28091
   151
  ultimately have suc: "y \<le> real (Suc p) / real q" by simp
nipkow@28091
   152
  def r \<equiv> "real p/real q"
nipkow@28091
   153
  have "x = y-(y-x)" by simp
nipkow@28091
   154
  also from suc q have "\<dots> < real (Suc p)/real q - inverse (real q)" by arith
nipkow@28091
   155
  also have "\<dots> = real p / real q"
haftmann@37887
   156
    by (simp only: inverse_eq_divide diff_minus real_of_nat_Suc 
nipkow@28091
   157
    minus_divide_left add_divide_distrib[THEN sym]) simp
nipkow@28091
   158
  finally have "x<r" by (unfold r_def)
nipkow@28091
   159
  have "p<Suc p" .. also note main[THEN sym]
nipkow@28091
   160
  finally have "\<not> ?P p"  by (rule not_less_Least)
nipkow@28091
   161
  hence "r<y" by (simp add: r_def)
nipkow@28091
   162
  from r_def have "r \<in> \<rat>" by simp
nipkow@28091
   163
  with `x<r` `r<y` show ?thesis by fast
nipkow@28091
   164
qed
nipkow@28091
   165
nipkow@28091
   166
theorem Rats_dense_in_real: fixes x y :: real
nipkow@28091
   167
assumes "x<y" shows "\<exists>r \<in> \<rat>.  x<r \<and> r<y"
nipkow@28091
   168
proof -
nipkow@28091
   169
  from reals_Archimedean2 obtain n::nat where "-x < real n" by auto
nipkow@28091
   170
  hence "0 \<le> x + real n" by arith
nipkow@28091
   171
  also from `x<y` have "x + real n < y + real n" by arith
nipkow@28091
   172
  ultimately have "\<exists>r \<in> \<rat>. x + real n < r \<and> r < y + real n"
nipkow@28091
   173
    by(rule Rats_dense_in_nn_real)
nipkow@28091
   174
  then obtain r where "r \<in> \<rat>" and r2: "x + real n < r" 
nipkow@28091
   175
    and r3: "r < y + real n"
nipkow@28091
   176
    by blast
nipkow@28091
   177
  have "r - real n = r + real (int n)/real (-1::int)" by simp
nipkow@28091
   178
  also from `r\<in>\<rat>` have "r + real (int n)/real (-1::int) \<in> \<rat>" by simp
nipkow@28091
   179
  also from r2 have "x < r - real n" by arith
nipkow@28091
   180
  moreover from r3 have "r - real n < y" by arith
nipkow@28091
   181
  ultimately show ?thesis by fast
nipkow@28091
   182
qed
nipkow@28091
   183
nipkow@28091
   184
paulson@14641
   185
subsection{*Floor and Ceiling Functions from the Reals to the Integers*}
paulson@14641
   186
paulson@14641
   187
lemma number_of_less_real_of_int_iff [simp]:
paulson@14641
   188
     "((number_of n) < real (m::int)) = (number_of n < m)"
paulson@14641
   189
apply auto
paulson@14641
   190
apply (rule real_of_int_less_iff [THEN iffD1])
paulson@14641
   191
apply (drule_tac [2] real_of_int_less_iff [THEN iffD2], auto)
paulson@14641
   192
done
paulson@14641
   193
paulson@14641
   194
lemma number_of_less_real_of_int_iff2 [simp]:
paulson@14641
   195
     "(real (m::int) < (number_of n)) = (m < number_of n)"
paulson@14641
   196
apply auto
paulson@14641
   197
apply (rule real_of_int_less_iff [THEN iffD1])
paulson@14641
   198
apply (drule_tac [2] real_of_int_less_iff [THEN iffD2], auto)
paulson@14641
   199
done
paulson@14641
   200
paulson@14641
   201
lemma number_of_le_real_of_int_iff [simp]:
paulson@14641
   202
     "((number_of n) \<le> real (m::int)) = (number_of n \<le> m)"
paulson@14641
   203
by (simp add: linorder_not_less [symmetric])
paulson@14641
   204
paulson@14641
   205
lemma number_of_le_real_of_int_iff2 [simp]:
paulson@14641
   206
     "(real (m::int) \<le> (number_of n)) = (m \<le> number_of n)"
paulson@14641
   207
by (simp add: linorder_not_less [symmetric])
paulson@14641
   208
huffman@24355
   209
lemma floor_real_of_nat [simp]: "floor (real (n::nat)) = int n"
huffman@30097
   210
unfolding real_of_nat_def by simp
paulson@14641
   211
huffman@24355
   212
lemma floor_minus_real_of_nat [simp]: "floor (- real (n::nat)) = - int n"
huffman@30102
   213
unfolding real_of_nat_def by (simp add: floor_minus)
paulson@14641
   214
paulson@14641
   215
lemma floor_real_of_int [simp]: "floor (real (n::int)) = n"
huffman@30097
   216
unfolding real_of_int_def by simp
paulson@14641
   217
paulson@14641
   218
lemma floor_minus_real_of_int [simp]: "floor (- real (n::int)) = - n"
huffman@30102
   219
unfolding real_of_int_def by (simp add: floor_minus)
paulson@14641
   220
paulson@14641
   221
lemma real_lb_ub_int: " \<exists>n::int. real n \<le> r & r < real (n+1)"
huffman@30097
   222
unfolding real_of_int_def by (rule floor_exists)
paulson@14641
   223
paulson@14641
   224
lemma lemma_floor:
paulson@14641
   225
  assumes a1: "real m \<le> r" and a2: "r < real n + 1"
paulson@14641
   226
  shows "m \<le> (n::int)"
paulson@14641
   227
proof -
wenzelm@23389
   228
  have "real m < real n + 1" using a1 a2 by (rule order_le_less_trans)
wenzelm@23389
   229
  also have "... = real (n + 1)" by simp
wenzelm@23389
   230
  finally have "m < n + 1" by (simp only: real_of_int_less_iff)
paulson@14641
   231
  thus ?thesis by arith
paulson@14641
   232
qed
paulson@14641
   233
paulson@14641
   234
lemma real_of_int_floor_le [simp]: "real (floor r) \<le> r"
huffman@30097
   235
unfolding real_of_int_def by (rule of_int_floor_le)
paulson@14641
   236
paulson@14641
   237
lemma lemma_floor2: "real n < real (x::int) + 1 ==> n \<le> x"
paulson@14641
   238
by (auto intro: lemma_floor)
paulson@14641
   239
paulson@14641
   240
lemma real_of_int_floor_cancel [simp]:
paulson@14641
   241
    "(real (floor x) = x) = (\<exists>n::int. x = real n)"
huffman@30097
   242
  using floor_real_of_int by metis
paulson@14641
   243
paulson@14641
   244
lemma floor_eq: "[| real n < x; x < real n + 1 |] ==> floor x = n"
huffman@30097
   245
  unfolding real_of_int_def using floor_unique [of n x] by simp
paulson@14641
   246
paulson@14641
   247
lemma floor_eq2: "[| real n \<le> x; x < real n + 1 |] ==> floor x = n"
huffman@30097
   248
  unfolding real_of_int_def by (rule floor_unique)
paulson@14641
   249
paulson@14641
   250
lemma floor_eq3: "[| real n < x; x < real (Suc n) |] ==> nat(floor x) = n"
paulson@14641
   251
apply (rule inj_int [THEN injD])
paulson@14641
   252
apply (simp add: real_of_nat_Suc)
nipkow@15539
   253
apply (simp add: real_of_nat_Suc floor_eq floor_eq [where n = "int n"])
paulson@14641
   254
done
paulson@14641
   255
paulson@14641
   256
lemma floor_eq4: "[| real n \<le> x; x < real (Suc n) |] ==> nat(floor x) = n"
paulson@14641
   257
apply (drule order_le_imp_less_or_eq)
paulson@14641
   258
apply (auto intro: floor_eq3)
paulson@14641
   259
done
paulson@14641
   260
paulson@14641
   261
lemma real_of_int_floor_ge_diff_one [simp]: "r - 1 \<le> real(floor r)"
huffman@30097
   262
  unfolding real_of_int_def using floor_correct [of r] by simp
avigad@16819
   263
avigad@16819
   264
lemma real_of_int_floor_gt_diff_one [simp]: "r - 1 < real(floor r)"
huffman@30097
   265
  unfolding real_of_int_def using floor_correct [of r] by simp
paulson@14641
   266
paulson@14641
   267
lemma real_of_int_floor_add_one_ge [simp]: "r \<le> real(floor r) + 1"
huffman@30097
   268
  unfolding real_of_int_def using floor_correct [of r] by simp
paulson@14641
   269
avigad@16819
   270
lemma real_of_int_floor_add_one_gt [simp]: "r < real(floor r) + 1"
huffman@30097
   271
  unfolding real_of_int_def using floor_correct [of r] by simp
paulson@14641
   272
avigad@16819
   273
lemma le_floor: "real a <= x ==> a <= floor x"
huffman@30097
   274
  unfolding real_of_int_def by (simp add: le_floor_iff)
avigad@16819
   275
avigad@16819
   276
lemma real_le_floor: "a <= floor x ==> real a <= x"
huffman@30097
   277
  unfolding real_of_int_def by (simp add: le_floor_iff)
avigad@16819
   278
avigad@16819
   279
lemma le_floor_eq: "(a <= floor x) = (real a <= x)"
huffman@30097
   280
  unfolding real_of_int_def by (rule le_floor_iff)
avigad@16819
   281
avigad@16819
   282
lemma floor_less_eq: "(floor x < a) = (x < real a)"
huffman@30097
   283
  unfolding real_of_int_def by (rule floor_less_iff)
avigad@16819
   284
avigad@16819
   285
lemma less_floor_eq: "(a < floor x) = (real a + 1 <= x)"
huffman@30097
   286
  unfolding real_of_int_def by (rule less_floor_iff)
avigad@16819
   287
avigad@16819
   288
lemma floor_le_eq: "(floor x <= a) = (x < real a + 1)"
huffman@30097
   289
  unfolding real_of_int_def by (rule floor_le_iff)
avigad@16819
   290
avigad@16819
   291
lemma floor_add [simp]: "floor (x + real a) = floor x + a"
huffman@30097
   292
  unfolding real_of_int_def by (rule floor_add_of_int)
avigad@16819
   293
avigad@16819
   294
lemma floor_subtract [simp]: "floor (x - real a) = floor x - a"
huffman@30097
   295
  unfolding real_of_int_def by (rule floor_diff_of_int)
avigad@16819
   296
hoelzl@35578
   297
lemma le_mult_floor:
hoelzl@35578
   298
  assumes "0 \<le> (a :: real)" and "0 \<le> b"
hoelzl@35578
   299
  shows "floor a * floor b \<le> floor (a * b)"
hoelzl@35578
   300
proof -
hoelzl@35578
   301
  have "real (floor a) \<le> a"
hoelzl@35578
   302
    and "real (floor b) \<le> b" by auto
hoelzl@35578
   303
  hence "real (floor a * floor b) \<le> a * b"
hoelzl@35578
   304
    using assms by (auto intro!: mult_mono)
hoelzl@35578
   305
  also have "a * b < real (floor (a * b) + 1)" by auto
hoelzl@35578
   306
  finally show ?thesis unfolding real_of_int_less_iff by simp
hoelzl@35578
   307
qed
hoelzl@35578
   308
huffman@24355
   309
lemma ceiling_real_of_nat [simp]: "ceiling (real (n::nat)) = int n"
huffman@30097
   310
  unfolding real_of_nat_def by simp
paulson@14641
   311
paulson@14641
   312
lemma ceiling_floor [simp]: "ceiling (real (floor r)) = floor r"
huffman@30097
   313
  unfolding real_of_int_def by simp
paulson@14641
   314
paulson@14641
   315
lemma floor_ceiling [simp]: "floor (real (ceiling r)) = ceiling r"
huffman@30097
   316
  unfolding real_of_int_def by simp
paulson@14641
   317
paulson@14641
   318
lemma real_of_int_ceiling_ge [simp]: "r \<le> real (ceiling r)"
huffman@30097
   319
  unfolding real_of_int_def by (rule le_of_int_ceiling)
paulson@14641
   320
huffman@30097
   321
lemma ceiling_real_of_int [simp]: "ceiling (real (n::int)) = n"
huffman@30097
   322
  unfolding real_of_int_def by simp
paulson@14641
   323
paulson@14641
   324
lemma real_of_int_ceiling_cancel [simp]:
paulson@14641
   325
     "(real (ceiling x) = x) = (\<exists>n::int. x = real n)"
huffman@30097
   326
  using ceiling_real_of_int by metis
paulson@14641
   327
paulson@14641
   328
lemma ceiling_eq: "[| real n < x; x < real n + 1 |] ==> ceiling x = n + 1"
huffman@30097
   329
  unfolding real_of_int_def using ceiling_unique [of "n + 1" x] by simp
paulson@14641
   330
paulson@14641
   331
lemma ceiling_eq2: "[| real n < x; x \<le> real n + 1 |] ==> ceiling x = n + 1"
huffman@30097
   332
  unfolding real_of_int_def using ceiling_unique [of "n + 1" x] by simp
paulson@14641
   333
paulson@14641
   334
lemma ceiling_eq3: "[| real n - 1 < x; x \<le> real n  |] ==> ceiling x = n"
huffman@30097
   335
  unfolding real_of_int_def using ceiling_unique [of n x] by simp
paulson@14641
   336
paulson@14641
   337
lemma real_of_int_ceiling_diff_one_le [simp]: "real (ceiling r) - 1 \<le> r"
huffman@30097
   338
  unfolding real_of_int_def using ceiling_correct [of r] by simp
paulson@14641
   339
paulson@14641
   340
lemma real_of_int_ceiling_le_add_one [simp]: "real (ceiling r) \<le> r + 1"
huffman@30097
   341
  unfolding real_of_int_def using ceiling_correct [of r] by simp
paulson@14641
   342
avigad@16819
   343
lemma ceiling_le: "x <= real a ==> ceiling x <= a"
huffman@30097
   344
  unfolding real_of_int_def by (simp add: ceiling_le_iff)
avigad@16819
   345
avigad@16819
   346
lemma ceiling_le_real: "ceiling x <= a ==> x <= real a"
huffman@30097
   347
  unfolding real_of_int_def by (simp add: ceiling_le_iff)
avigad@16819
   348
avigad@16819
   349
lemma ceiling_le_eq: "(ceiling x <= a) = (x <= real a)"
huffman@30097
   350
  unfolding real_of_int_def by (rule ceiling_le_iff)
avigad@16819
   351
avigad@16819
   352
lemma less_ceiling_eq: "(a < ceiling x) = (real a < x)"
huffman@30097
   353
  unfolding real_of_int_def by (rule less_ceiling_iff)
avigad@16819
   354
avigad@16819
   355
lemma ceiling_less_eq: "(ceiling x < a) = (x <= real a - 1)"
huffman@30097
   356
  unfolding real_of_int_def by (rule ceiling_less_iff)
avigad@16819
   357
avigad@16819
   358
lemma le_ceiling_eq: "(a <= ceiling x) = (real a - 1 < x)"
huffman@30097
   359
  unfolding real_of_int_def by (rule le_ceiling_iff)
avigad@16819
   360
avigad@16819
   361
lemma ceiling_add [simp]: "ceiling (x + real a) = ceiling x + a"
huffman@30097
   362
  unfolding real_of_int_def by (rule ceiling_add_of_int)
avigad@16819
   363
avigad@16819
   364
lemma ceiling_subtract [simp]: "ceiling (x - real a) = ceiling x - a"
huffman@30097
   365
  unfolding real_of_int_def by (rule ceiling_diff_of_int)
avigad@16819
   366
avigad@16819
   367
avigad@16819
   368
subsection {* Versions for the natural numbers *}
avigad@16819
   369
wenzelm@19765
   370
definition
wenzelm@21404
   371
  natfloor :: "real => nat" where
wenzelm@19765
   372
  "natfloor x = nat(floor x)"
wenzelm@21404
   373
wenzelm@21404
   374
definition
wenzelm@21404
   375
  natceiling :: "real => nat" where
wenzelm@19765
   376
  "natceiling x = nat(ceiling x)"
avigad@16819
   377
avigad@16819
   378
lemma natfloor_zero [simp]: "natfloor 0 = 0"
avigad@16819
   379
  by (unfold natfloor_def, simp)
avigad@16819
   380
avigad@16819
   381
lemma natfloor_one [simp]: "natfloor 1 = 1"
avigad@16819
   382
  by (unfold natfloor_def, simp)
avigad@16819
   383
avigad@16819
   384
lemma zero_le_natfloor [simp]: "0 <= natfloor x"
avigad@16819
   385
  by (unfold natfloor_def, simp)
avigad@16819
   386
avigad@16819
   387
lemma natfloor_number_of_eq [simp]: "natfloor (number_of n) = number_of n"
avigad@16819
   388
  by (unfold natfloor_def, simp)
avigad@16819
   389
avigad@16819
   390
lemma natfloor_real_of_nat [simp]: "natfloor(real n) = n"
avigad@16819
   391
  by (unfold natfloor_def, simp)
avigad@16819
   392
avigad@16819
   393
lemma real_natfloor_le: "0 <= x ==> real(natfloor x) <= x"
avigad@16819
   394
  by (unfold natfloor_def, simp)
avigad@16819
   395
avigad@16819
   396
lemma natfloor_neg: "x <= 0 ==> natfloor x = 0"
avigad@16819
   397
  apply (unfold natfloor_def)
avigad@16819
   398
  apply (subgoal_tac "floor x <= floor 0")
avigad@16819
   399
  apply simp
huffman@30097
   400
  apply (erule floor_mono)
avigad@16819
   401
done
avigad@16819
   402
avigad@16819
   403
lemma natfloor_mono: "x <= y ==> natfloor x <= natfloor y"
avigad@16819
   404
  apply (case_tac "0 <= x")
avigad@16819
   405
  apply (subst natfloor_def)+
avigad@16819
   406
  apply (subst nat_le_eq_zle)
avigad@16819
   407
  apply force
huffman@30097
   408
  apply (erule floor_mono)
avigad@16819
   409
  apply (subst natfloor_neg)
avigad@16819
   410
  apply simp
avigad@16819
   411
  apply simp
avigad@16819
   412
done
avigad@16819
   413
avigad@16819
   414
lemma le_natfloor: "real x <= a ==> x <= natfloor a"
avigad@16819
   415
  apply (unfold natfloor_def)
avigad@16819
   416
  apply (subst nat_int [THEN sym])
avigad@16819
   417
  apply (subst nat_le_eq_zle)
avigad@16819
   418
  apply simp
avigad@16819
   419
  apply (rule le_floor)
avigad@16819
   420
  apply simp
avigad@16819
   421
done
avigad@16819
   422
hoelzl@35578
   423
lemma less_natfloor:
hoelzl@35578
   424
  assumes "0 \<le> x" and "x < real (n :: nat)"
hoelzl@35578
   425
  shows "natfloor x < n"
hoelzl@35578
   426
proof (rule ccontr)
hoelzl@35578
   427
  assume "\<not> ?thesis" hence *: "n \<le> natfloor x" by simp
hoelzl@35578
   428
  note assms(2)
hoelzl@35578
   429
  also have "real n \<le> real (natfloor x)"
hoelzl@35578
   430
    using * unfolding real_of_nat_le_iff .
hoelzl@35578
   431
  finally have "x < real (natfloor x)" .
hoelzl@35578
   432
  with real_natfloor_le[OF assms(1)]
hoelzl@35578
   433
  show False by auto
hoelzl@35578
   434
qed
hoelzl@35578
   435
avigad@16819
   436
lemma le_natfloor_eq: "0 <= x ==> (a <= natfloor x) = (real a <= x)"
avigad@16819
   437
  apply (rule iffI)
avigad@16819
   438
  apply (rule order_trans)
avigad@16819
   439
  prefer 2
avigad@16819
   440
  apply (erule real_natfloor_le)
avigad@16819
   441
  apply (subst real_of_nat_le_iff)
avigad@16819
   442
  apply assumption
avigad@16819
   443
  apply (erule le_natfloor)
avigad@16819
   444
done
avigad@16819
   445
wenzelm@16893
   446
lemma le_natfloor_eq_number_of [simp]:
avigad@16819
   447
    "~ neg((number_of n)::int) ==> 0 <= x ==>
avigad@16819
   448
      (number_of n <= natfloor x) = (number_of n <= x)"
avigad@16819
   449
  apply (subst le_natfloor_eq, assumption)
avigad@16819
   450
  apply simp
avigad@16819
   451
done
avigad@16819
   452
avigad@16820
   453
lemma le_natfloor_eq_one [simp]: "(1 <= natfloor x) = (1 <= x)"
avigad@16819
   454
  apply (case_tac "0 <= x")
avigad@16819
   455
  apply (subst le_natfloor_eq, assumption, simp)
avigad@16819
   456
  apply (rule iffI)
wenzelm@16893
   457
  apply (subgoal_tac "natfloor x <= natfloor 0")
avigad@16819
   458
  apply simp
avigad@16819
   459
  apply (rule natfloor_mono)
avigad@16819
   460
  apply simp
avigad@16819
   461
  apply simp
avigad@16819
   462
done
avigad@16819
   463
avigad@16819
   464
lemma natfloor_eq: "real n <= x ==> x < real n + 1 ==> natfloor x = n"
avigad@16819
   465
  apply (unfold natfloor_def)
hoelzl@35578
   466
  apply (subst (2) nat_int [THEN sym])
avigad@16819
   467
  apply (subst eq_nat_nat_iff)
avigad@16819
   468
  apply simp
avigad@16819
   469
  apply simp
avigad@16819
   470
  apply (rule floor_eq2)
avigad@16819
   471
  apply auto
avigad@16819
   472
done
avigad@16819
   473
avigad@16819
   474
lemma real_natfloor_add_one_gt: "x < real(natfloor x) + 1"
avigad@16819
   475
  apply (case_tac "0 <= x")
avigad@16819
   476
  apply (unfold natfloor_def)
avigad@16819
   477
  apply simp
avigad@16819
   478
  apply simp_all
avigad@16819
   479
done
avigad@16819
   480
avigad@16819
   481
lemma real_natfloor_gt_diff_one: "x - 1 < real(natfloor x)"
nipkow@29667
   482
using real_natfloor_add_one_gt by (simp add: algebra_simps)
avigad@16819
   483
avigad@16819
   484
lemma ge_natfloor_plus_one_imp_gt: "natfloor z + 1 <= n ==> z < real n"
avigad@16819
   485
  apply (subgoal_tac "z < real(natfloor z) + 1")
avigad@16819
   486
  apply arith
avigad@16819
   487
  apply (rule real_natfloor_add_one_gt)
avigad@16819
   488
done
avigad@16819
   489
avigad@16819
   490
lemma natfloor_add [simp]: "0 <= x ==> natfloor (x + real a) = natfloor x + a"
avigad@16819
   491
  apply (unfold natfloor_def)
huffman@24355
   492
  apply (subgoal_tac "real a = real (int a)")
avigad@16819
   493
  apply (erule ssubst)
huffman@23309
   494
  apply (simp add: nat_add_distrib del: real_of_int_of_nat_eq)
avigad@16819
   495
  apply simp
avigad@16819
   496
done
avigad@16819
   497
wenzelm@16893
   498
lemma natfloor_add_number_of [simp]:
wenzelm@16893
   499
    "~neg ((number_of n)::int) ==> 0 <= x ==>
avigad@16819
   500
      natfloor (x + number_of n) = natfloor x + number_of n"
avigad@16819
   501
  apply (subst natfloor_add [THEN sym])
avigad@16819
   502
  apply simp_all
avigad@16819
   503
done
avigad@16819
   504
avigad@16819
   505
lemma natfloor_add_one: "0 <= x ==> natfloor(x + 1) = natfloor x + 1"
avigad@16819
   506
  apply (subst natfloor_add [THEN sym])
avigad@16819
   507
  apply assumption
avigad@16819
   508
  apply simp
avigad@16819
   509
done
avigad@16819
   510
wenzelm@16893
   511
lemma natfloor_subtract [simp]: "real a <= x ==>
avigad@16819
   512
    natfloor(x - real a) = natfloor x - a"
avigad@16819
   513
  apply (unfold natfloor_def)
huffman@24355
   514
  apply (subgoal_tac "real a = real (int a)")
avigad@16819
   515
  apply (erule ssubst)
huffman@23309
   516
  apply (simp del: real_of_int_of_nat_eq)
avigad@16819
   517
  apply simp
avigad@16819
   518
done
avigad@16819
   519
wenzelm@41550
   520
lemma natfloor_div_nat:
wenzelm@41550
   521
  assumes "1 <= x" and "y > 0"
wenzelm@41550
   522
  shows "natfloor (x / real y) = natfloor x div y"
hoelzl@35578
   523
proof -
hoelzl@35578
   524
  have "natfloor x = (natfloor x) div y * y + (natfloor x) mod y"
hoelzl@35578
   525
    by simp
hoelzl@35578
   526
  then have a: "real(natfloor x) = real ((natfloor x) div y) * real y +
hoelzl@35578
   527
    real((natfloor x) mod y)"
hoelzl@35578
   528
    by (simp only: real_of_nat_add [THEN sym] real_of_nat_mult [THEN sym])
hoelzl@35578
   529
  have "x = real(natfloor x) + (x - real(natfloor x))"
hoelzl@35578
   530
    by simp
hoelzl@35578
   531
  then have "x = real ((natfloor x) div y) * real y +
hoelzl@35578
   532
      real((natfloor x) mod y) + (x - real(natfloor x))"
hoelzl@35578
   533
    by (simp add: a)
hoelzl@35578
   534
  then have "x / real y = ... / real y"
hoelzl@35578
   535
    by simp
hoelzl@35578
   536
  also have "... = real((natfloor x) div y) + real((natfloor x) mod y) /
hoelzl@35578
   537
    real y + (x - real(natfloor x)) / real y"
wenzelm@41550
   538
    by (auto simp add: algebra_simps add_divide_distrib diff_divide_distrib)
hoelzl@35578
   539
  finally have "natfloor (x / real y) = natfloor(...)" by simp
hoelzl@35578
   540
  also have "... = natfloor(real((natfloor x) mod y) /
hoelzl@35578
   541
    real y + (x - real(natfloor x)) / real y + real((natfloor x) div y))"
hoelzl@35578
   542
    by (simp add: add_ac)
hoelzl@35578
   543
  also have "... = natfloor(real((natfloor x) mod y) /
hoelzl@35578
   544
    real y + (x - real(natfloor x)) / real y) + (natfloor x) div y"
hoelzl@35578
   545
    apply (rule natfloor_add)
hoelzl@35578
   546
    apply (rule add_nonneg_nonneg)
hoelzl@35578
   547
    apply (rule divide_nonneg_pos)
hoelzl@35578
   548
    apply simp
wenzelm@41550
   549
    apply (simp add: assms)
hoelzl@35578
   550
    apply (rule divide_nonneg_pos)
hoelzl@35578
   551
    apply (simp add: algebra_simps)
hoelzl@35578
   552
    apply (rule real_natfloor_le)
wenzelm@41550
   553
    using assms apply auto
hoelzl@35578
   554
    done
hoelzl@35578
   555
  also have "natfloor(real((natfloor x) mod y) /
hoelzl@35578
   556
    real y + (x - real(natfloor x)) / real y) = 0"
hoelzl@35578
   557
    apply (rule natfloor_eq)
hoelzl@35578
   558
    apply simp
hoelzl@35578
   559
    apply (rule add_nonneg_nonneg)
hoelzl@35578
   560
    apply (rule divide_nonneg_pos)
hoelzl@35578
   561
    apply force
wenzelm@41550
   562
    apply (force simp add: assms)
hoelzl@35578
   563
    apply (rule divide_nonneg_pos)
hoelzl@35578
   564
    apply (simp add: algebra_simps)
hoelzl@35578
   565
    apply (rule real_natfloor_le)
wenzelm@41550
   566
    apply (auto simp add: assms)
wenzelm@41550
   567
    using assms apply arith
wenzelm@41550
   568
    using assms apply (simp add: add_divide_distrib [THEN sym])
hoelzl@35578
   569
    apply (subgoal_tac "real y = real y - 1 + 1")
hoelzl@35578
   570
    apply (erule ssubst)
hoelzl@35578
   571
    apply (rule add_le_less_mono)
hoelzl@35578
   572
    apply (simp add: algebra_simps)
hoelzl@35578
   573
    apply (subgoal_tac "1 + real(natfloor x mod y) =
hoelzl@35578
   574
      real(natfloor x mod y + 1)")
hoelzl@35578
   575
    apply (erule ssubst)
hoelzl@35578
   576
    apply (subst real_of_nat_le_iff)
hoelzl@35578
   577
    apply (subgoal_tac "natfloor x mod y < y")
hoelzl@35578
   578
    apply arith
hoelzl@35578
   579
    apply (rule mod_less_divisor)
hoelzl@35578
   580
    apply auto
hoelzl@35578
   581
    using real_natfloor_add_one_gt
hoelzl@35578
   582
    apply (simp add: algebra_simps)
hoelzl@35578
   583
    done
hoelzl@35578
   584
  finally show ?thesis by simp
hoelzl@35578
   585
qed
hoelzl@35578
   586
hoelzl@35578
   587
lemma le_mult_natfloor:
hoelzl@35578
   588
  assumes "0 \<le> (a :: real)" and "0 \<le> b"
hoelzl@35578
   589
  shows "natfloor a * natfloor b \<le> natfloor (a * b)"
hoelzl@35578
   590
  unfolding natfloor_def
hoelzl@35578
   591
  apply (subst nat_mult_distrib[symmetric])
hoelzl@35578
   592
  using assms apply simp
hoelzl@35578
   593
  apply (subst nat_le_eq_zle)
hoelzl@35578
   594
  using assms le_mult_floor by (auto intro!: mult_nonneg_nonneg)
hoelzl@35578
   595
avigad@16819
   596
lemma natceiling_zero [simp]: "natceiling 0 = 0"
avigad@16819
   597
  by (unfold natceiling_def, simp)
avigad@16819
   598
avigad@16819
   599
lemma natceiling_one [simp]: "natceiling 1 = 1"
avigad@16819
   600
  by (unfold natceiling_def, simp)
avigad@16819
   601
avigad@16819
   602
lemma zero_le_natceiling [simp]: "0 <= natceiling x"
avigad@16819
   603
  by (unfold natceiling_def, simp)
avigad@16819
   604
avigad@16819
   605
lemma natceiling_number_of_eq [simp]: "natceiling (number_of n) = number_of n"
avigad@16819
   606
  by (unfold natceiling_def, simp)
avigad@16819
   607
avigad@16819
   608
lemma natceiling_real_of_nat [simp]: "natceiling(real n) = n"
avigad@16819
   609
  by (unfold natceiling_def, simp)
avigad@16819
   610
avigad@16819
   611
lemma real_natceiling_ge: "x <= real(natceiling x)"
avigad@16819
   612
  apply (unfold natceiling_def)
avigad@16819
   613
  apply (case_tac "x < 0")
avigad@16819
   614
  apply simp
avigad@16819
   615
  apply (subst real_nat_eq_real)
avigad@16819
   616
  apply (subgoal_tac "ceiling 0 <= ceiling x")
avigad@16819
   617
  apply simp
huffman@30097
   618
  apply (rule ceiling_mono)
avigad@16819
   619
  apply simp
avigad@16819
   620
  apply simp
avigad@16819
   621
done
avigad@16819
   622
avigad@16819
   623
lemma natceiling_neg: "x <= 0 ==> natceiling x = 0"
avigad@16819
   624
  apply (unfold natceiling_def)
avigad@16819
   625
  apply simp
avigad@16819
   626
done
avigad@16819
   627
avigad@16819
   628
lemma natceiling_mono: "x <= y ==> natceiling x <= natceiling y"
avigad@16819
   629
  apply (case_tac "0 <= x")
avigad@16819
   630
  apply (subst natceiling_def)+
avigad@16819
   631
  apply (subst nat_le_eq_zle)
avigad@16819
   632
  apply (rule disjI2)
avigad@16819
   633
  apply (subgoal_tac "real (0::int) <= real(ceiling y)")
avigad@16819
   634
  apply simp
avigad@16819
   635
  apply (rule order_trans)
avigad@16819
   636
  apply simp
avigad@16819
   637
  apply (erule order_trans)
avigad@16819
   638
  apply simp
huffman@30097
   639
  apply (erule ceiling_mono)
avigad@16819
   640
  apply (subst natceiling_neg)
avigad@16819
   641
  apply simp_all
avigad@16819
   642
done
avigad@16819
   643
avigad@16819
   644
lemma natceiling_le: "x <= real a ==> natceiling x <= a"
avigad@16819
   645
  apply (unfold natceiling_def)
avigad@16819
   646
  apply (case_tac "x < 0")
avigad@16819
   647
  apply simp
hoelzl@35578
   648
  apply (subst (2) nat_int [THEN sym])
avigad@16819
   649
  apply (subst nat_le_eq_zle)
avigad@16819
   650
  apply simp
avigad@16819
   651
  apply (rule ceiling_le)
avigad@16819
   652
  apply simp
avigad@16819
   653
done
avigad@16819
   654
avigad@16819
   655
lemma natceiling_le_eq: "0 <= x ==> (natceiling x <= a) = (x <= real a)"
avigad@16819
   656
  apply (rule iffI)
avigad@16819
   657
  apply (rule order_trans)
avigad@16819
   658
  apply (rule real_natceiling_ge)
avigad@16819
   659
  apply (subst real_of_nat_le_iff)
avigad@16819
   660
  apply assumption
avigad@16819
   661
  apply (erule natceiling_le)
avigad@16819
   662
done
avigad@16819
   663
wenzelm@16893
   664
lemma natceiling_le_eq_number_of [simp]:
avigad@16820
   665
    "~ neg((number_of n)::int) ==> 0 <= x ==>
avigad@16820
   666
      (natceiling x <= number_of n) = (x <= number_of n)"
avigad@16819
   667
  apply (subst natceiling_le_eq, assumption)
avigad@16819
   668
  apply simp
avigad@16819
   669
done
avigad@16819
   670
avigad@16820
   671
lemma natceiling_le_eq_one: "(natceiling x <= 1) = (x <= 1)"
avigad@16819
   672
  apply (case_tac "0 <= x")
avigad@16819
   673
  apply (subst natceiling_le_eq)
avigad@16819
   674
  apply assumption
avigad@16819
   675
  apply simp
avigad@16819
   676
  apply (subst natceiling_neg)
avigad@16819
   677
  apply simp
avigad@16819
   678
  apply simp
avigad@16819
   679
done
avigad@16819
   680
avigad@16819
   681
lemma natceiling_eq: "real n < x ==> x <= real n + 1 ==> natceiling x = n + 1"
avigad@16819
   682
  apply (unfold natceiling_def)
wenzelm@19850
   683
  apply (simplesubst nat_int [THEN sym]) back back
avigad@16819
   684
  apply (subgoal_tac "nat(int n) + 1 = nat(int n + 1)")
avigad@16819
   685
  apply (erule ssubst)
avigad@16819
   686
  apply (subst eq_nat_nat_iff)
avigad@16819
   687
  apply (subgoal_tac "ceiling 0 <= ceiling x")
avigad@16819
   688
  apply simp
huffman@30097
   689
  apply (rule ceiling_mono)
avigad@16819
   690
  apply force
avigad@16819
   691
  apply force
avigad@16819
   692
  apply (rule ceiling_eq2)
avigad@16819
   693
  apply (simp, simp)
avigad@16819
   694
  apply (subst nat_add_distrib)
avigad@16819
   695
  apply auto
avigad@16819
   696
done
avigad@16819
   697
wenzelm@16893
   698
lemma natceiling_add [simp]: "0 <= x ==>
avigad@16819
   699
    natceiling (x + real a) = natceiling x + a"
avigad@16819
   700
  apply (unfold natceiling_def)
huffman@24355
   701
  apply (subgoal_tac "real a = real (int a)")
avigad@16819
   702
  apply (erule ssubst)
huffman@23309
   703
  apply (simp del: real_of_int_of_nat_eq)
avigad@16819
   704
  apply (subst nat_add_distrib)
avigad@16819
   705
  apply (subgoal_tac "0 = ceiling 0")
avigad@16819
   706
  apply (erule ssubst)
huffman@30097
   707
  apply (erule ceiling_mono)
avigad@16819
   708
  apply simp_all
avigad@16819
   709
done
avigad@16819
   710
wenzelm@16893
   711
lemma natceiling_add_number_of [simp]:
wenzelm@16893
   712
    "~ neg ((number_of n)::int) ==> 0 <= x ==>
avigad@16820
   713
      natceiling (x + number_of n) = natceiling x + number_of n"
avigad@16819
   714
  apply (subst natceiling_add [THEN sym])
avigad@16819
   715
  apply simp_all
avigad@16819
   716
done
avigad@16819
   717
avigad@16819
   718
lemma natceiling_add_one: "0 <= x ==> natceiling(x + 1) = natceiling x + 1"
avigad@16819
   719
  apply (subst natceiling_add [THEN sym])
avigad@16819
   720
  apply assumption
avigad@16819
   721
  apply simp
avigad@16819
   722
done
avigad@16819
   723
wenzelm@16893
   724
lemma natceiling_subtract [simp]: "real a <= x ==>
avigad@16819
   725
    natceiling(x - real a) = natceiling x - a"
avigad@16819
   726
  apply (unfold natceiling_def)
huffman@24355
   727
  apply (subgoal_tac "real a = real (int a)")
avigad@16819
   728
  apply (erule ssubst)
huffman@23309
   729
  apply (simp del: real_of_int_of_nat_eq)
avigad@16819
   730
  apply simp
avigad@16819
   731
done
avigad@16819
   732
huffman@36826
   733
subsection {* Exponentiation with floor *}
huffman@36826
   734
huffman@36826
   735
lemma floor_power:
huffman@36826
   736
  assumes "x = real (floor x)"
huffman@36826
   737
  shows "floor (x ^ n) = floor x ^ n"
huffman@36826
   738
proof -
huffman@36826
   739
  have *: "x ^ n = real (floor x ^ n)"
huffman@36826
   740
    using assms by (induct n arbitrary: x) simp_all
huffman@36826
   741
  show ?thesis unfolding real_of_int_inject[symmetric]
huffman@36826
   742
    unfolding * floor_real_of_int ..
huffman@36826
   743
qed
huffman@36826
   744
huffman@36826
   745
lemma natfloor_power:
huffman@36826
   746
  assumes "x = real (natfloor x)"
huffman@36826
   747
  shows "natfloor (x ^ n) = natfloor x ^ n"
huffman@36826
   748
proof -
huffman@36826
   749
  from assms have "0 \<le> floor x" by auto
huffman@36826
   750
  note assms[unfolded natfloor_def real_nat_eq_real[OF `0 \<le> floor x`]]
huffman@36826
   751
  from floor_power[OF this]
huffman@36826
   752
  show ?thesis unfolding natfloor_def nat_power_eq[OF `0 \<le> floor x`, symmetric]
huffman@36826
   753
    by simp
huffman@36826
   754
qed
avigad@16819
   755
paulson@14365
   756
end