src/HOL/RComplete.thy
 author huffman Tue May 11 09:10:31 2010 -0700 (2010-05-11) changeset 36826 4d4462d644ae parent 36795 e05e1283c550 child 36979 da7c06ab3169 permissions -rw-r--r--
move floor lemmas from RealPow.thy to RComplete.thy
     1 (*  Title:      HOL/RComplete.thy

     2     Author:     Jacques D. Fleuriot, University of Edinburgh

     3     Author:     Larry Paulson, University of Cambridge

     4     Author:     Jeremy Avigad, Carnegie Mellon University

     5     Author:     Florian Zuleger, Johannes Hoelzl, and Simon Funke, TU Muenchen

     6 *)

     7

     8 header {* Completeness of the Reals; Floor and Ceiling Functions *}

     9

    10 theory RComplete

    11 imports Lubs RealDef

    12 begin

    13

    14 lemma real_sum_of_halves: "x/2 + x/2 = (x::real)"

    15   by simp

    16

    17 lemma abs_diff_less_iff:

    18   "(\<bar>x - a\<bar> < (r::'a::linordered_idom)) = (a - r < x \<and> x < a + r)"

    19   by auto

    20

    21 subsection {* Completeness of Positive Reals *}

    22

    23 text {*

    24   Supremum property for the set of positive reals

    25

    26   Let @{text "P"} be a non-empty set of positive reals, with an upper

    27   bound @{text "y"}.  Then @{text "P"} has a least upper bound

    28   (written @{text "S"}).

    29

    30   FIXME: Can the premise be weakened to @{text "\<forall>x \<in> P. x\<le> y"}?

    31 *}

    32

    33 text {* Only used in HOL/Import/HOL4Compat.thy; delete? *}

    34

    35 lemma posreal_complete:

    36   assumes positive_P: "\<forall>x \<in> P. (0::real) < x"

    37     and not_empty_P: "\<exists>x. x \<in> P"

    38     and upper_bound_Ex: "\<exists>y. \<forall>x \<in> P. x<y"

    39   shows "\<exists>S. \<forall>y. (\<exists>x \<in> P. y < x) = (y < S)"

    40 proof -

    41   from upper_bound_Ex have "\<exists>z. \<forall>x\<in>P. x \<le> z"

    42     by (auto intro: less_imp_le)

    43   from complete_real [OF not_empty_P this] obtain S

    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

    45   have "\<forall>y. (\<exists>x \<in> P. y < x) = (y < S)"

    46   proof

    47     fix y show "(\<exists>x\<in>P. y < x) = (y < S)"

    48       apply (cases "\<exists>x\<in>P. y < x", simp_all)

    49       apply (clarify, drule S1, simp)

    50       apply (simp add: not_less S2)

    51       done

    52   qed

    53   thus ?thesis ..

    54 qed

    55

    56 text {*

    57   \medskip Completeness properties using @{text "isUb"}, @{text "isLub"} etc.

    58 *}

    59

    60 lemma real_isLub_unique: "[| isLub R S x; isLub R S y |] ==> x = (y::real)"

    61   apply (frule isLub_isUb)

    62   apply (frule_tac x = y in isLub_isUb)

    63   apply (blast intro!: order_antisym dest!: isLub_le_isUb)

    64   done

    65

    66

    67 text {*

    68   \medskip reals Completeness (again!)

    69 *}

    70

    71 lemma reals_complete:

    72   assumes notempty_S: "\<exists>X. X \<in> S"

    73     and exists_Ub: "\<exists>Y. isUb (UNIV::real set) S Y"

    74   shows "\<exists>t. isLub (UNIV :: real set) S t"

    75 proof -

    76   from assms have "\<exists>X. X \<in> S" and "\<exists>Y. \<forall>x\<in>S. x \<le> Y"

    77     unfolding isUb_def setle_def by simp_all

    78   from complete_real [OF this] show ?thesis

    79     unfolding isLub_def leastP_def setle_def setge_def Ball_def

    80       Collect_def mem_def isUb_def UNIV_def by simp

    81 qed

    82

    83 text{*A version of the same theorem without all those predicates!*}

    84 lemma reals_complete2:

    85   fixes S :: "(real set)"

    86   assumes "\<exists>y. y\<in>S" and "\<exists>(x::real). \<forall>y\<in>S. y \<le> x"

    87   shows "\<exists>x. (\<forall>y\<in>S. y \<le> x) &

    88                (\<forall>z. ((\<forall>y\<in>S. y \<le> z) --> x \<le> z))"

    89 using assms by (rule complete_real)

    90

    91

    92 subsection {* The Archimedean Property of the Reals *}

    93

    94 theorem reals_Archimedean:

    95   assumes x_pos: "0 < x"

    96   shows "\<exists>n. inverse (real (Suc n)) < x"

    97   unfolding real_of_nat_def using x_pos

    98   by (rule ex_inverse_of_nat_Suc_less)

    99

   100 lemma reals_Archimedean2: "\<exists>n. (x::real) < real (n::nat)"

   101   unfolding real_of_nat_def by (rule ex_less_of_nat)

   102

   103 lemma reals_Archimedean3:

   104   assumes x_greater_zero: "0 < x"

   105   shows "\<forall>(y::real). \<exists>(n::nat). y < real n * x"

   106   unfolding real_of_nat_def using 0 < x

   107   by (auto intro: ex_less_of_nat_mult)

   108

   109 lemma reals_Archimedean6:

   110      "0 \<le> r ==> \<exists>(n::nat). real (n - 1) \<le> r & r < real (n)"

   111 unfolding real_of_nat_def

   112 apply (rule exI [where x="nat (floor r + 1)"])

   113 apply (insert floor_correct [of r])

   114 apply (simp add: nat_add_distrib of_nat_nat)

   115 done

   116

   117 lemma reals_Archimedean6a: "0 \<le> r ==> \<exists>n. real (n) \<le> r & r < real (Suc n)"

   118   by (drule reals_Archimedean6) auto

   119

   120 lemma reals_Archimedean_6b_int:

   121      "0 \<le> r ==> \<exists>n::int. real n \<le> r & r < real (n+1)"

   122   unfolding real_of_int_def by (rule floor_exists)

   123

   124 lemma reals_Archimedean_6c_int:

   125      "r < 0 ==> \<exists>n::int. real n \<le> r & r < real (n+1)"

   126   unfolding real_of_int_def by (rule floor_exists)

   127

   128

   129 subsection{*Density of the Rational Reals in the Reals*}

   130

   131 text{* This density proof is due to Stefan Richter and was ported by TN.  The

   132 original source is \emph{Real Analysis} by H.L. Royden.

   133 It employs the Archimedean property of the reals. *}

   134

   135 lemma Rats_dense_in_nn_real: fixes x::real

   136 assumes "0\<le>x" and "x<y" shows "\<exists>r \<in> \<rat>.  x<r \<and> r<y"

   137 proof -

   138   from x<y have "0 < y-x" by simp

   139   with reals_Archimedean obtain q::nat

   140     where q: "inverse (real q) < y-x" and "0 < real q" by auto

   141   def p \<equiv> "LEAST n.  y \<le> real (Suc n)/real q"

   142   from reals_Archimedean2 obtain n::nat where "y * real q < real n" by auto

   143   with 0 < real q have ex: "y \<le> real n/real q" (is "?P n")

   144     by (simp add: pos_less_divide_eq[THEN sym])

   145   also from assms have "\<not> y \<le> real (0::nat) / real q" by simp

   146   ultimately have main: "(LEAST n. y \<le> real n/real q) = Suc p"

   147     by (unfold p_def) (rule Least_Suc)

   148   also from ex have "?P (LEAST x. ?P x)" by (rule LeastI)

   149   ultimately have suc: "y \<le> real (Suc p) / real q" by simp

   150   def r \<equiv> "real p/real q"

   151   have "x = y-(y-x)" by simp

   152   also from suc q have "\<dots> < real (Suc p)/real q - inverse (real q)" by arith

   153   also have "\<dots> = real p / real q"

   154     by (simp only: inverse_eq_divide diff_def real_of_nat_Suc

   155     minus_divide_left add_divide_distrib[THEN sym]) simp

   156   finally have "x<r" by (unfold r_def)

   157   have "p<Suc p" .. also note main[THEN sym]

   158   finally have "\<not> ?P p"  by (rule not_less_Least)

   159   hence "r<y" by (simp add: r_def)

   160   from r_def have "r \<in> \<rat>" by simp

   161   with x<r r<y show ?thesis by fast

   162 qed

   163

   164 theorem Rats_dense_in_real: fixes x y :: real

   165 assumes "x<y" shows "\<exists>r \<in> \<rat>.  x<r \<and> r<y"

   166 proof -

   167   from reals_Archimedean2 obtain n::nat where "-x < real n" by auto

   168   hence "0 \<le> x + real n" by arith

   169   also from x<y have "x + real n < y + real n" by arith

   170   ultimately have "\<exists>r \<in> \<rat>. x + real n < r \<and> r < y + real n"

   171     by(rule Rats_dense_in_nn_real)

   172   then obtain r where "r \<in> \<rat>" and r2: "x + real n < r"

   173     and r3: "r < y + real n"

   174     by blast

   175   have "r - real n = r + real (int n)/real (-1::int)" by simp

   176   also from r\<in>\<rat> have "r + real (int n)/real (-1::int) \<in> \<rat>" by simp

   177   also from r2 have "x < r - real n" by arith

   178   moreover from r3 have "r - real n < y" by arith

   179   ultimately show ?thesis by fast

   180 qed

   181

   182

   183 subsection{*Floor and Ceiling Functions from the Reals to the Integers*}

   184

   185 lemma number_of_less_real_of_int_iff [simp]:

   186      "((number_of n) < real (m::int)) = (number_of n < m)"

   187 apply auto

   188 apply (rule real_of_int_less_iff [THEN iffD1])

   189 apply (drule_tac  real_of_int_less_iff [THEN iffD2], auto)

   190 done

   191

   192 lemma number_of_less_real_of_int_iff2 [simp]:

   193      "(real (m::int) < (number_of n)) = (m < number_of n)"

   194 apply auto

   195 apply (rule real_of_int_less_iff [THEN iffD1])

   196 apply (drule_tac  real_of_int_less_iff [THEN iffD2], auto)

   197 done

   198

   199 lemma number_of_le_real_of_int_iff [simp]:

   200      "((number_of n) \<le> real (m::int)) = (number_of n \<le> m)"

   201 by (simp add: linorder_not_less [symmetric])

   202

   203 lemma number_of_le_real_of_int_iff2 [simp]:

   204      "(real (m::int) \<le> (number_of n)) = (m \<le> number_of n)"

   205 by (simp add: linorder_not_less [symmetric])

   206

   207 lemma floor_real_of_nat_zero: "floor (real (0::nat)) = 0"

   208 by auto (* delete? *)

   209

   210 lemma floor_real_of_nat [simp]: "floor (real (n::nat)) = int n"

   211 unfolding real_of_nat_def by simp

   212

   213 lemma floor_minus_real_of_nat [simp]: "floor (- real (n::nat)) = - int n"

   214 unfolding real_of_nat_def by (simp add: floor_minus)

   215

   216 lemma floor_real_of_int [simp]: "floor (real (n::int)) = n"

   217 unfolding real_of_int_def by simp

   218

   219 lemma floor_minus_real_of_int [simp]: "floor (- real (n::int)) = - n"

   220 unfolding real_of_int_def by (simp add: floor_minus)

   221

   222 lemma real_lb_ub_int: " \<exists>n::int. real n \<le> r & r < real (n+1)"

   223 unfolding real_of_int_def by (rule floor_exists)

   224

   225 lemma lemma_floor:

   226   assumes a1: "real m \<le> r" and a2: "r < real n + 1"

   227   shows "m \<le> (n::int)"

   228 proof -

   229   have "real m < real n + 1" using a1 a2 by (rule order_le_less_trans)

   230   also have "... = real (n + 1)" by simp

   231   finally have "m < n + 1" by (simp only: real_of_int_less_iff)

   232   thus ?thesis by arith

   233 qed

   234

   235 lemma real_of_int_floor_le [simp]: "real (floor r) \<le> r"

   236 unfolding real_of_int_def by (rule of_int_floor_le)

   237

   238 lemma lemma_floor2: "real n < real (x::int) + 1 ==> n \<le> x"

   239 by (auto intro: lemma_floor)

   240

   241 lemma real_of_int_floor_cancel [simp]:

   242     "(real (floor x) = x) = (\<exists>n::int. x = real n)"

   243   using floor_real_of_int by metis

   244

   245 lemma floor_eq: "[| real n < x; x < real n + 1 |] ==> floor x = n"

   246   unfolding real_of_int_def using floor_unique [of n x] by simp

   247

   248 lemma floor_eq2: "[| real n \<le> x; x < real n + 1 |] ==> floor x = n"

   249   unfolding real_of_int_def by (rule floor_unique)

   250

   251 lemma floor_eq3: "[| real n < x; x < real (Suc n) |] ==> nat(floor x) = n"

   252 apply (rule inj_int [THEN injD])

   253 apply (simp add: real_of_nat_Suc)

   254 apply (simp add: real_of_nat_Suc floor_eq floor_eq [where n = "int n"])

   255 done

   256

   257 lemma floor_eq4: "[| real n \<le> x; x < real (Suc n) |] ==> nat(floor x) = n"

   258 apply (drule order_le_imp_less_or_eq)

   259 apply (auto intro: floor_eq3)

   260 done

   261

   262 lemma floor_number_of_eq:

   263      "floor(number_of n :: real) = (number_of n :: int)"

   264   by (rule floor_number_of) (* already declared [simp] *)

   265

   266 lemma real_of_int_floor_ge_diff_one [simp]: "r - 1 \<le> real(floor r)"

   267   unfolding real_of_int_def using floor_correct [of r] by simp

   268

   269 lemma real_of_int_floor_gt_diff_one [simp]: "r - 1 < real(floor r)"

   270   unfolding real_of_int_def using floor_correct [of r] by simp

   271

   272 lemma real_of_int_floor_add_one_ge [simp]: "r \<le> real(floor r) + 1"

   273   unfolding real_of_int_def using floor_correct [of r] by simp

   274

   275 lemma real_of_int_floor_add_one_gt [simp]: "r < real(floor r) + 1"

   276   unfolding real_of_int_def using floor_correct [of r] by simp

   277

   278 lemma le_floor: "real a <= x ==> a <= floor x"

   279   unfolding real_of_int_def by (simp add: le_floor_iff)

   280

   281 lemma real_le_floor: "a <= floor x ==> real a <= x"

   282   unfolding real_of_int_def by (simp add: le_floor_iff)

   283

   284 lemma le_floor_eq: "(a <= floor x) = (real a <= x)"

   285   unfolding real_of_int_def by (rule le_floor_iff)

   286

   287 lemma le_floor_eq_number_of:

   288     "(number_of n <= floor x) = (number_of n <= x)"

   289   by (rule number_of_le_floor) (* already declared [simp] *)

   290

   291 lemma le_floor_eq_zero: "(0 <= floor x) = (0 <= x)"

   292   by (rule zero_le_floor) (* already declared [simp] *)

   293

   294 lemma le_floor_eq_one: "(1 <= floor x) = (1 <= x)"

   295   by (rule one_le_floor) (* already declared [simp] *)

   296

   297 lemma floor_less_eq: "(floor x < a) = (x < real a)"

   298   unfolding real_of_int_def by (rule floor_less_iff)

   299

   300 lemma floor_less_eq_number_of:

   301     "(floor x < number_of n) = (x < number_of n)"

   302   by (rule floor_less_number_of) (* already declared [simp] *)

   303

   304 lemma floor_less_eq_zero: "(floor x < 0) = (x < 0)"

   305   by (rule floor_less_zero) (* already declared [simp] *)

   306

   307 lemma floor_less_eq_one: "(floor x < 1) = (x < 1)"

   308   by (rule floor_less_one) (* already declared [simp] *)

   309

   310 lemma less_floor_eq: "(a < floor x) = (real a + 1 <= x)"

   311   unfolding real_of_int_def by (rule less_floor_iff)

   312

   313 lemma less_floor_eq_number_of:

   314     "(number_of n < floor x) = (number_of n + 1 <= x)"

   315   by (rule number_of_less_floor) (* already declared [simp] *)

   316

   317 lemma less_floor_eq_zero: "(0 < floor x) = (1 <= x)"

   318   by (rule zero_less_floor) (* already declared [simp] *)

   319

   320 lemma less_floor_eq_one: "(1 < floor x) = (2 <= x)"

   321   by (rule one_less_floor) (* already declared [simp] *)

   322

   323 lemma floor_le_eq: "(floor x <= a) = (x < real a + 1)"

   324   unfolding real_of_int_def by (rule floor_le_iff)

   325

   326 lemma floor_le_eq_number_of:

   327     "(floor x <= number_of n) = (x < number_of n + 1)"

   328   by (rule floor_le_number_of) (* already declared [simp] *)

   329

   330 lemma floor_le_eq_zero: "(floor x <= 0) = (x < 1)"

   331   by (rule floor_le_zero) (* already declared [simp] *)

   332

   333 lemma floor_le_eq_one: "(floor x <= 1) = (x < 2)"

   334   by (rule floor_le_one) (* already declared [simp] *)

   335

   336 lemma floor_add [simp]: "floor (x + real a) = floor x + a"

   337   unfolding real_of_int_def by (rule floor_add_of_int)

   338

   339 lemma floor_subtract [simp]: "floor (x - real a) = floor x - a"

   340   unfolding real_of_int_def by (rule floor_diff_of_int)

   341

   342 lemma floor_subtract_number_of: "floor (x - number_of n) =

   343     floor x - number_of n"

   344   by (rule floor_diff_number_of) (* already declared [simp] *)

   345

   346 lemma floor_subtract_one: "floor (x - 1) = floor x - 1"

   347   by (rule floor_diff_one) (* already declared [simp] *)

   348

   349 lemma le_mult_floor:

   350   assumes "0 \<le> (a :: real)" and "0 \<le> b"

   351   shows "floor a * floor b \<le> floor (a * b)"

   352 proof -

   353   have "real (floor a) \<le> a"

   354     and "real (floor b) \<le> b" by auto

   355   hence "real (floor a * floor b) \<le> a * b"

   356     using assms by (auto intro!: mult_mono)

   357   also have "a * b < real (floor (a * b) + 1)" by auto

   358   finally show ?thesis unfolding real_of_int_less_iff by simp

   359 qed

   360

   361 lemma ceiling_real_of_nat [simp]: "ceiling (real (n::nat)) = int n"

   362   unfolding real_of_nat_def by simp

   363

   364 lemma ceiling_real_of_nat_zero: "ceiling (real (0::nat)) = 0"

   365 by auto (* delete? *)

   366

   367 lemma ceiling_floor [simp]: "ceiling (real (floor r)) = floor r"

   368   unfolding real_of_int_def by simp

   369

   370 lemma floor_ceiling [simp]: "floor (real (ceiling r)) = ceiling r"

   371   unfolding real_of_int_def by simp

   372

   373 lemma real_of_int_ceiling_ge [simp]: "r \<le> real (ceiling r)"

   374   unfolding real_of_int_def by (rule le_of_int_ceiling)

   375

   376 lemma ceiling_real_of_int [simp]: "ceiling (real (n::int)) = n"

   377   unfolding real_of_int_def by simp

   378

   379 lemma real_of_int_ceiling_cancel [simp]:

   380      "(real (ceiling x) = x) = (\<exists>n::int. x = real n)"

   381   using ceiling_real_of_int by metis

   382

   383 lemma ceiling_eq: "[| real n < x; x < real n + 1 |] ==> ceiling x = n + 1"

   384   unfolding real_of_int_def using ceiling_unique [of "n + 1" x] by simp

   385

   386 lemma ceiling_eq2: "[| real n < x; x \<le> real n + 1 |] ==> ceiling x = n + 1"

   387   unfolding real_of_int_def using ceiling_unique [of "n + 1" x] by simp

   388

   389 lemma ceiling_eq3: "[| real n - 1 < x; x \<le> real n  |] ==> ceiling x = n"

   390   unfolding real_of_int_def using ceiling_unique [of n x] by simp

   391

   392 lemma ceiling_number_of_eq:

   393      "ceiling (number_of n :: real) = (number_of n)"

   394   by (rule ceiling_number_of) (* already declared [simp] *)

   395

   396 lemma real_of_int_ceiling_diff_one_le [simp]: "real (ceiling r) - 1 \<le> r"

   397   unfolding real_of_int_def using ceiling_correct [of r] by simp

   398

   399 lemma real_of_int_ceiling_le_add_one [simp]: "real (ceiling r) \<le> r + 1"

   400   unfolding real_of_int_def using ceiling_correct [of r] by simp

   401

   402 lemma ceiling_le: "x <= real a ==> ceiling x <= a"

   403   unfolding real_of_int_def by (simp add: ceiling_le_iff)

   404

   405 lemma ceiling_le_real: "ceiling x <= a ==> x <= real a"

   406   unfolding real_of_int_def by (simp add: ceiling_le_iff)

   407

   408 lemma ceiling_le_eq: "(ceiling x <= a) = (x <= real a)"

   409   unfolding real_of_int_def by (rule ceiling_le_iff)

   410

   411 lemma ceiling_le_eq_number_of:

   412     "(ceiling x <= number_of n) = (x <= number_of n)"

   413   by (rule ceiling_le_number_of) (* already declared [simp] *)

   414

   415 lemma ceiling_le_zero_eq: "(ceiling x <= 0) = (x <= 0)"

   416   by (rule ceiling_le_zero) (* already declared [simp] *)

   417

   418 lemma ceiling_le_eq_one: "(ceiling x <= 1) = (x <= 1)"

   419   by (rule ceiling_le_one) (* already declared [simp] *)

   420

   421 lemma less_ceiling_eq: "(a < ceiling x) = (real a < x)"

   422   unfolding real_of_int_def by (rule less_ceiling_iff)

   423

   424 lemma less_ceiling_eq_number_of:

   425     "(number_of n < ceiling x) = (number_of n < x)"

   426   by (rule number_of_less_ceiling) (* already declared [simp] *)

   427

   428 lemma less_ceiling_eq_zero: "(0 < ceiling x) = (0 < x)"

   429   by (rule zero_less_ceiling) (* already declared [simp] *)

   430

   431 lemma less_ceiling_eq_one: "(1 < ceiling x) = (1 < x)"

   432   by (rule one_less_ceiling) (* already declared [simp] *)

   433

   434 lemma ceiling_less_eq: "(ceiling x < a) = (x <= real a - 1)"

   435   unfolding real_of_int_def by (rule ceiling_less_iff)

   436

   437 lemma ceiling_less_eq_number_of:

   438     "(ceiling x < number_of n) = (x <= number_of n - 1)"

   439   by (rule ceiling_less_number_of) (* already declared [simp] *)

   440

   441 lemma ceiling_less_eq_zero: "(ceiling x < 0) = (x <= -1)"

   442   by (rule ceiling_less_zero) (* already declared [simp] *)

   443

   444 lemma ceiling_less_eq_one: "(ceiling x < 1) = (x <= 0)"

   445   by (rule ceiling_less_one) (* already declared [simp] *)

   446

   447 lemma le_ceiling_eq: "(a <= ceiling x) = (real a - 1 < x)"

   448   unfolding real_of_int_def by (rule le_ceiling_iff)

   449

   450 lemma le_ceiling_eq_number_of:

   451     "(number_of n <= ceiling x) = (number_of n - 1 < x)"

   452   by (rule number_of_le_ceiling) (* already declared [simp] *)

   453

   454 lemma le_ceiling_eq_zero: "(0 <= ceiling x) = (-1 < x)"

   455   by (rule zero_le_ceiling) (* already declared [simp] *)

   456

   457 lemma le_ceiling_eq_one: "(1 <= ceiling x) = (0 < x)"

   458   by (rule one_le_ceiling) (* already declared [simp] *)

   459

   460 lemma ceiling_add [simp]: "ceiling (x + real a) = ceiling x + a"

   461   unfolding real_of_int_def by (rule ceiling_add_of_int)

   462

   463 lemma ceiling_subtract [simp]: "ceiling (x - real a) = ceiling x - a"

   464   unfolding real_of_int_def by (rule ceiling_diff_of_int)

   465

   466 lemma ceiling_subtract_number_of: "ceiling (x - number_of n) =

   467     ceiling x - number_of n"

   468   by (rule ceiling_diff_number_of) (* already declared [simp] *)

   469

   470 lemma ceiling_subtract_one: "ceiling (x - 1) = ceiling x - 1"

   471   by (rule ceiling_diff_one) (* already declared [simp] *)

   472

   473

   474 subsection {* Versions for the natural numbers *}

   475

   476 definition

   477   natfloor :: "real => nat" where

   478   "natfloor x = nat(floor x)"

   479

   480 definition

   481   natceiling :: "real => nat" where

   482   "natceiling x = nat(ceiling x)"

   483

   484 lemma natfloor_zero [simp]: "natfloor 0 = 0"

   485   by (unfold natfloor_def, simp)

   486

   487 lemma natfloor_one [simp]: "natfloor 1 = 1"

   488   by (unfold natfloor_def, simp)

   489

   490 lemma zero_le_natfloor [simp]: "0 <= natfloor x"

   491   by (unfold natfloor_def, simp)

   492

   493 lemma natfloor_number_of_eq [simp]: "natfloor (number_of n) = number_of n"

   494   by (unfold natfloor_def, simp)

   495

   496 lemma natfloor_real_of_nat [simp]: "natfloor(real n) = n"

   497   by (unfold natfloor_def, simp)

   498

   499 lemma real_natfloor_le: "0 <= x ==> real(natfloor x) <= x"

   500   by (unfold natfloor_def, simp)

   501

   502 lemma natfloor_neg: "x <= 0 ==> natfloor x = 0"

   503   apply (unfold natfloor_def)

   504   apply (subgoal_tac "floor x <= floor 0")

   505   apply simp

   506   apply (erule floor_mono)

   507 done

   508

   509 lemma natfloor_mono: "x <= y ==> natfloor x <= natfloor y"

   510   apply (case_tac "0 <= x")

   511   apply (subst natfloor_def)+

   512   apply (subst nat_le_eq_zle)

   513   apply force

   514   apply (erule floor_mono)

   515   apply (subst natfloor_neg)

   516   apply simp

   517   apply simp

   518 done

   519

   520 lemma le_natfloor: "real x <= a ==> x <= natfloor a"

   521   apply (unfold natfloor_def)

   522   apply (subst nat_int [THEN sym])

   523   apply (subst nat_le_eq_zle)

   524   apply simp

   525   apply (rule le_floor)

   526   apply simp

   527 done

   528

   529 lemma less_natfloor:

   530   assumes "0 \<le> x" and "x < real (n :: nat)"

   531   shows "natfloor x < n"

   532 proof (rule ccontr)

   533   assume "\<not> ?thesis" hence *: "n \<le> natfloor x" by simp

   534   note assms(2)

   535   also have "real n \<le> real (natfloor x)"

   536     using * unfolding real_of_nat_le_iff .

   537   finally have "x < real (natfloor x)" .

   538   with real_natfloor_le[OF assms(1)]

   539   show False by auto

   540 qed

   541

   542 lemma le_natfloor_eq: "0 <= x ==> (a <= natfloor x) = (real a <= x)"

   543   apply (rule iffI)

   544   apply (rule order_trans)

   545   prefer 2

   546   apply (erule real_natfloor_le)

   547   apply (subst real_of_nat_le_iff)

   548   apply assumption

   549   apply (erule le_natfloor)

   550 done

   551

   552 lemma le_natfloor_eq_number_of [simp]:

   553     "~ neg((number_of n)::int) ==> 0 <= x ==>

   554       (number_of n <= natfloor x) = (number_of n <= x)"

   555   apply (subst le_natfloor_eq, assumption)

   556   apply simp

   557 done

   558

   559 lemma le_natfloor_eq_one [simp]: "(1 <= natfloor x) = (1 <= x)"

   560   apply (case_tac "0 <= x")

   561   apply (subst le_natfloor_eq, assumption, simp)

   562   apply (rule iffI)

   563   apply (subgoal_tac "natfloor x <= natfloor 0")

   564   apply simp

   565   apply (rule natfloor_mono)

   566   apply simp

   567   apply simp

   568 done

   569

   570 lemma natfloor_eq: "real n <= x ==> x < real n + 1 ==> natfloor x = n"

   571   apply (unfold natfloor_def)

   572   apply (subst (2) nat_int [THEN sym])

   573   apply (subst eq_nat_nat_iff)

   574   apply simp

   575   apply simp

   576   apply (rule floor_eq2)

   577   apply auto

   578 done

   579

   580 lemma real_natfloor_add_one_gt: "x < real(natfloor x) + 1"

   581   apply (case_tac "0 <= x")

   582   apply (unfold natfloor_def)

   583   apply simp

   584   apply simp_all

   585 done

   586

   587 lemma real_natfloor_gt_diff_one: "x - 1 < real(natfloor x)"

   588 using real_natfloor_add_one_gt by (simp add: algebra_simps)

   589

   590 lemma ge_natfloor_plus_one_imp_gt: "natfloor z + 1 <= n ==> z < real n"

   591   apply (subgoal_tac "z < real(natfloor z) + 1")

   592   apply arith

   593   apply (rule real_natfloor_add_one_gt)

   594 done

   595

   596 lemma natfloor_add [simp]: "0 <= x ==> natfloor (x + real a) = natfloor x + a"

   597   apply (unfold natfloor_def)

   598   apply (subgoal_tac "real a = real (int a)")

   599   apply (erule ssubst)

   600   apply (simp add: nat_add_distrib del: real_of_int_of_nat_eq)

   601   apply simp

   602 done

   603

   604 lemma natfloor_add_number_of [simp]:

   605     "~neg ((number_of n)::int) ==> 0 <= x ==>

   606       natfloor (x + number_of n) = natfloor x + number_of n"

   607   apply (subst natfloor_add [THEN sym])

   608   apply simp_all

   609 done

   610

   611 lemma natfloor_add_one: "0 <= x ==> natfloor(x + 1) = natfloor x + 1"

   612   apply (subst natfloor_add [THEN sym])

   613   apply assumption

   614   apply simp

   615 done

   616

   617 lemma natfloor_subtract [simp]: "real a <= x ==>

   618     natfloor(x - real a) = natfloor x - a"

   619   apply (unfold natfloor_def)

   620   apply (subgoal_tac "real a = real (int a)")

   621   apply (erule ssubst)

   622   apply (simp del: real_of_int_of_nat_eq)

   623   apply simp

   624 done

   625

   626 lemma natfloor_div_nat: "1 <= x ==> y > 0 ==>

   627   natfloor (x / real y) = natfloor x div y"

   628 proof -

   629   assume "1 <= (x::real)" and "(y::nat) > 0"

   630   have "natfloor x = (natfloor x) div y * y + (natfloor x) mod y"

   631     by simp

   632   then have a: "real(natfloor x) = real ((natfloor x) div y) * real y +

   633     real((natfloor x) mod y)"

   634     by (simp only: real_of_nat_add [THEN sym] real_of_nat_mult [THEN sym])

   635   have "x = real(natfloor x) + (x - real(natfloor x))"

   636     by simp

   637   then have "x = real ((natfloor x) div y) * real y +

   638       real((natfloor x) mod y) + (x - real(natfloor x))"

   639     by (simp add: a)

   640   then have "x / real y = ... / real y"

   641     by simp

   642   also have "... = real((natfloor x) div y) + real((natfloor x) mod y) /

   643     real y + (x - real(natfloor x)) / real y"

   644     by (auto simp add: algebra_simps add_divide_distrib

   645       diff_divide_distrib prems)

   646   finally have "natfloor (x / real y) = natfloor(...)" by simp

   647   also have "... = natfloor(real((natfloor x) mod y) /

   648     real y + (x - real(natfloor x)) / real y + real((natfloor x) div y))"

   649     by (simp add: add_ac)

   650   also have "... = natfloor(real((natfloor x) mod y) /

   651     real y + (x - real(natfloor x)) / real y) + (natfloor x) div y"

   652     apply (rule natfloor_add)

   653     apply (rule add_nonneg_nonneg)

   654     apply (rule divide_nonneg_pos)

   655     apply simp

   656     apply (simp add: prems)

   657     apply (rule divide_nonneg_pos)

   658     apply (simp add: algebra_simps)

   659     apply (rule real_natfloor_le)

   660     apply (insert prems, auto)

   661     done

   662   also have "natfloor(real((natfloor x) mod y) /

   663     real y + (x - real(natfloor x)) / real y) = 0"

   664     apply (rule natfloor_eq)

   665     apply simp

   666     apply (rule add_nonneg_nonneg)

   667     apply (rule divide_nonneg_pos)

   668     apply force

   669     apply (force simp add: prems)

   670     apply (rule divide_nonneg_pos)

   671     apply (simp add: algebra_simps)

   672     apply (rule real_natfloor_le)

   673     apply (auto simp add: prems)

   674     apply (insert prems, arith)

   675     apply (simp add: add_divide_distrib [THEN sym])

   676     apply (subgoal_tac "real y = real y - 1 + 1")

   677     apply (erule ssubst)

   678     apply (rule add_le_less_mono)

   679     apply (simp add: algebra_simps)

   680     apply (subgoal_tac "1 + real(natfloor x mod y) =

   681       real(natfloor x mod y + 1)")

   682     apply (erule ssubst)

   683     apply (subst real_of_nat_le_iff)

   684     apply (subgoal_tac "natfloor x mod y < y")

   685     apply arith

   686     apply (rule mod_less_divisor)

   687     apply auto

   688     using real_natfloor_add_one_gt

   689     apply (simp add: algebra_simps)

   690     done

   691   finally show ?thesis by simp

   692 qed

   693

   694 lemma le_mult_natfloor:

   695   assumes "0 \<le> (a :: real)" and "0 \<le> b"

   696   shows "natfloor a * natfloor b \<le> natfloor (a * b)"

   697   unfolding natfloor_def

   698   apply (subst nat_mult_distrib[symmetric])

   699   using assms apply simp

   700   apply (subst nat_le_eq_zle)

   701   using assms le_mult_floor by (auto intro!: mult_nonneg_nonneg)

   702

   703 lemma natceiling_zero [simp]: "natceiling 0 = 0"

   704   by (unfold natceiling_def, simp)

   705

   706 lemma natceiling_one [simp]: "natceiling 1 = 1"

   707   by (unfold natceiling_def, simp)

   708

   709 lemma zero_le_natceiling [simp]: "0 <= natceiling x"

   710   by (unfold natceiling_def, simp)

   711

   712 lemma natceiling_number_of_eq [simp]: "natceiling (number_of n) = number_of n"

   713   by (unfold natceiling_def, simp)

   714

   715 lemma natceiling_real_of_nat [simp]: "natceiling(real n) = n"

   716   by (unfold natceiling_def, simp)

   717

   718 lemma real_natceiling_ge: "x <= real(natceiling x)"

   719   apply (unfold natceiling_def)

   720   apply (case_tac "x < 0")

   721   apply simp

   722   apply (subst real_nat_eq_real)

   723   apply (subgoal_tac "ceiling 0 <= ceiling x")

   724   apply simp

   725   apply (rule ceiling_mono)

   726   apply simp

   727   apply simp

   728 done

   729

   730 lemma natceiling_neg: "x <= 0 ==> natceiling x = 0"

   731   apply (unfold natceiling_def)

   732   apply simp

   733 done

   734

   735 lemma natceiling_mono: "x <= y ==> natceiling x <= natceiling y"

   736   apply (case_tac "0 <= x")

   737   apply (subst natceiling_def)+

   738   apply (subst nat_le_eq_zle)

   739   apply (rule disjI2)

   740   apply (subgoal_tac "real (0::int) <= real(ceiling y)")

   741   apply simp

   742   apply (rule order_trans)

   743   apply simp

   744   apply (erule order_trans)

   745   apply simp

   746   apply (erule ceiling_mono)

   747   apply (subst natceiling_neg)

   748   apply simp_all

   749 done

   750

   751 lemma natceiling_le: "x <= real a ==> natceiling x <= a"

   752   apply (unfold natceiling_def)

   753   apply (case_tac "x < 0")

   754   apply simp

   755   apply (subst (2) nat_int [THEN sym])

   756   apply (subst nat_le_eq_zle)

   757   apply simp

   758   apply (rule ceiling_le)

   759   apply simp

   760 done

   761

   762 lemma natceiling_le_eq: "0 <= x ==> (natceiling x <= a) = (x <= real a)"

   763   apply (rule iffI)

   764   apply (rule order_trans)

   765   apply (rule real_natceiling_ge)

   766   apply (subst real_of_nat_le_iff)

   767   apply assumption

   768   apply (erule natceiling_le)

   769 done

   770

   771 lemma natceiling_le_eq_number_of [simp]:

   772     "~ neg((number_of n)::int) ==> 0 <= x ==>

   773       (natceiling x <= number_of n) = (x <= number_of n)"

   774   apply (subst natceiling_le_eq, assumption)

   775   apply simp

   776 done

   777

   778 lemma natceiling_le_eq_one: "(natceiling x <= 1) = (x <= 1)"

   779   apply (case_tac "0 <= x")

   780   apply (subst natceiling_le_eq)

   781   apply assumption

   782   apply simp

   783   apply (subst natceiling_neg)

   784   apply simp

   785   apply simp

   786 done

   787

   788 lemma natceiling_eq: "real n < x ==> x <= real n + 1 ==> natceiling x = n + 1"

   789   apply (unfold natceiling_def)

   790   apply (simplesubst nat_int [THEN sym]) back back

   791   apply (subgoal_tac "nat(int n) + 1 = nat(int n + 1)")

   792   apply (erule ssubst)

   793   apply (subst eq_nat_nat_iff)

   794   apply (subgoal_tac "ceiling 0 <= ceiling x")

   795   apply simp

   796   apply (rule ceiling_mono)

   797   apply force

   798   apply force

   799   apply (rule ceiling_eq2)

   800   apply (simp, simp)

   801   apply (subst nat_add_distrib)

   802   apply auto

   803 done

   804

   805 lemma natceiling_add [simp]: "0 <= x ==>

   806     natceiling (x + real a) = natceiling x + a"

   807   apply (unfold natceiling_def)

   808   apply (subgoal_tac "real a = real (int a)")

   809   apply (erule ssubst)

   810   apply (simp del: real_of_int_of_nat_eq)

   811   apply (subst nat_add_distrib)

   812   apply (subgoal_tac "0 = ceiling 0")

   813   apply (erule ssubst)

   814   apply (erule ceiling_mono)

   815   apply simp_all

   816 done

   817

   818 lemma natceiling_add_number_of [simp]:

   819     "~ neg ((number_of n)::int) ==> 0 <= x ==>

   820       natceiling (x + number_of n) = natceiling x + number_of n"

   821   apply (subst natceiling_add [THEN sym])

   822   apply simp_all

   823 done

   824

   825 lemma natceiling_add_one: "0 <= x ==> natceiling(x + 1) = natceiling x + 1"

   826   apply (subst natceiling_add [THEN sym])

   827   apply assumption

   828   apply simp

   829 done

   830

   831 lemma natceiling_subtract [simp]: "real a <= x ==>

   832     natceiling(x - real a) = natceiling x - a"

   833   apply (unfold natceiling_def)

   834   apply (subgoal_tac "real a = real (int a)")

   835   apply (erule ssubst)

   836   apply (simp del: real_of_int_of_nat_eq)

   837   apply simp

   838 done

   839

   840 subsection {* Exponentiation with floor *}

   841

   842 lemma floor_power:

   843   assumes "x = real (floor x)"

   844   shows "floor (x ^ n) = floor x ^ n"

   845 proof -

   846   have *: "x ^ n = real (floor x ^ n)"

   847     using assms by (induct n arbitrary: x) simp_all

   848   show ?thesis unfolding real_of_int_inject[symmetric]

   849     unfolding * floor_real_of_int ..

   850 qed

   851

   852 lemma natfloor_power:

   853   assumes "x = real (natfloor x)"

   854   shows "natfloor (x ^ n) = natfloor x ^ n"

   855 proof -

   856   from assms have "0 \<le> floor x" by auto

   857   note assms[unfolded natfloor_def real_nat_eq_real[OF 0 \<le> floor x]]

   858   from floor_power[OF this]

   859   show ?thesis unfolding natfloor_def nat_power_eq[OF 0 \<le> floor x, symmetric]

   860     by simp

   861 qed

   862

   863 end