src/HOL/RComplete.thy
author huffman
Mon May 10 12:12:58 2010 -0700 (2010-05-10)
changeset 36795 e05e1283c550
parent 35578 384ad08a1d1b
child 36826 4d4462d644ae
permissions -rw-r--r--
new construction of real numbers using Cauchy sequences
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
avigad@16819
   120
lemma reals_Archimedean_6b_int:
avigad@16819
   121
     "0 \<le> r ==> \<exists>n::int. real n \<le> r & r < real (n+1)"
huffman@30097
   122
  unfolding real_of_int_def by (rule floor_exists)
avigad@16819
   123
avigad@16819
   124
lemma reals_Archimedean_6c_int:
avigad@16819
   125
     "r < 0 ==> \<exists>n::int. real n \<le> r & r < real (n+1)"
huffman@30097
   126
  unfolding real_of_int_def by (rule floor_exists)
avigad@16819
   127
avigad@16819
   128
nipkow@28091
   129
subsection{*Density of the Rational Reals in the Reals*}
nipkow@28091
   130
nipkow@28091
   131
text{* This density proof is due to Stefan Richter and was ported by TN.  The
nipkow@28091
   132
original source is \emph{Real Analysis} by H.L. Royden.
nipkow@28091
   133
It employs the Archimedean property of the reals. *}
nipkow@28091
   134
nipkow@28091
   135
lemma Rats_dense_in_nn_real: fixes x::real
nipkow@28091
   136
assumes "0\<le>x" and "x<y" shows "\<exists>r \<in> \<rat>.  x<r \<and> r<y"
nipkow@28091
   137
proof -
nipkow@28091
   138
  from `x<y` have "0 < y-x" by simp
nipkow@28091
   139
  with reals_Archimedean obtain q::nat 
nipkow@28091
   140
    where q: "inverse (real q) < y-x" and "0 < real q" by auto  
nipkow@28091
   141
  def p \<equiv> "LEAST n.  y \<le> real (Suc n)/real q"  
nipkow@28091
   142
  from reals_Archimedean2 obtain n::nat where "y * real q < real n" by auto
nipkow@28091
   143
  with `0 < real q` have ex: "y \<le> real n/real q" (is "?P n")
nipkow@28091
   144
    by (simp add: pos_less_divide_eq[THEN sym])
nipkow@28091
   145
  also from assms have "\<not> y \<le> real (0::nat) / real q" by simp
nipkow@28091
   146
  ultimately have main: "(LEAST n. y \<le> real n/real q) = Suc p"
nipkow@28091
   147
    by (unfold p_def) (rule Least_Suc)
nipkow@28091
   148
  also from ex have "?P (LEAST x. ?P x)" by (rule LeastI)
nipkow@28091
   149
  ultimately have suc: "y \<le> real (Suc p) / real q" by simp
nipkow@28091
   150
  def r \<equiv> "real p/real q"
nipkow@28091
   151
  have "x = y-(y-x)" by simp
nipkow@28091
   152
  also from suc q have "\<dots> < real (Suc p)/real q - inverse (real q)" by arith
nipkow@28091
   153
  also have "\<dots> = real p / real q"
huffman@36795
   154
    by (simp only: inverse_eq_divide diff_def real_of_nat_Suc 
nipkow@28091
   155
    minus_divide_left add_divide_distrib[THEN sym]) simp
nipkow@28091
   156
  finally have "x<r" by (unfold r_def)
nipkow@28091
   157
  have "p<Suc p" .. also note main[THEN sym]
nipkow@28091
   158
  finally have "\<not> ?P p"  by (rule not_less_Least)
nipkow@28091
   159
  hence "r<y" by (simp add: r_def)
nipkow@28091
   160
  from r_def have "r \<in> \<rat>" by simp
nipkow@28091
   161
  with `x<r` `r<y` show ?thesis by fast
nipkow@28091
   162
qed
nipkow@28091
   163
nipkow@28091
   164
theorem Rats_dense_in_real: fixes x y :: real
nipkow@28091
   165
assumes "x<y" shows "\<exists>r \<in> \<rat>.  x<r \<and> r<y"
nipkow@28091
   166
proof -
nipkow@28091
   167
  from reals_Archimedean2 obtain n::nat where "-x < real n" by auto
nipkow@28091
   168
  hence "0 \<le> x + real n" by arith
nipkow@28091
   169
  also from `x<y` have "x + real n < y + real n" by arith
nipkow@28091
   170
  ultimately have "\<exists>r \<in> \<rat>. x + real n < r \<and> r < y + real n"
nipkow@28091
   171
    by(rule Rats_dense_in_nn_real)
nipkow@28091
   172
  then obtain r where "r \<in> \<rat>" and r2: "x + real n < r" 
nipkow@28091
   173
    and r3: "r < y + real n"
nipkow@28091
   174
    by blast
nipkow@28091
   175
  have "r - real n = r + real (int n)/real (-1::int)" by simp
nipkow@28091
   176
  also from `r\<in>\<rat>` have "r + real (int n)/real (-1::int) \<in> \<rat>" by simp
nipkow@28091
   177
  also from r2 have "x < r - real n" by arith
nipkow@28091
   178
  moreover from r3 have "r - real n < y" by arith
nipkow@28091
   179
  ultimately show ?thesis by fast
nipkow@28091
   180
qed
nipkow@28091
   181
nipkow@28091
   182
paulson@14641
   183
subsection{*Floor and Ceiling Functions from the Reals to the Integers*}
paulson@14641
   184
paulson@14641
   185
lemma number_of_less_real_of_int_iff [simp]:
paulson@14641
   186
     "((number_of n) < real (m::int)) = (number_of n < m)"
paulson@14641
   187
apply auto
paulson@14641
   188
apply (rule real_of_int_less_iff [THEN iffD1])
paulson@14641
   189
apply (drule_tac [2] real_of_int_less_iff [THEN iffD2], auto)
paulson@14641
   190
done
paulson@14641
   191
paulson@14641
   192
lemma number_of_less_real_of_int_iff2 [simp]:
paulson@14641
   193
     "(real (m::int) < (number_of n)) = (m < number_of n)"
paulson@14641
   194
apply auto
paulson@14641
   195
apply (rule real_of_int_less_iff [THEN iffD1])
paulson@14641
   196
apply (drule_tac [2] real_of_int_less_iff [THEN iffD2], auto)
paulson@14641
   197
done
paulson@14641
   198
paulson@14641
   199
lemma number_of_le_real_of_int_iff [simp]:
paulson@14641
   200
     "((number_of n) \<le> real (m::int)) = (number_of n \<le> m)"
paulson@14641
   201
by (simp add: linorder_not_less [symmetric])
paulson@14641
   202
paulson@14641
   203
lemma number_of_le_real_of_int_iff2 [simp]:
paulson@14641
   204
     "(real (m::int) \<le> (number_of n)) = (m \<le> number_of n)"
paulson@14641
   205
by (simp add: linorder_not_less [symmetric])
paulson@14641
   206
huffman@30097
   207
lemma floor_real_of_nat_zero: "floor (real (0::nat)) = 0"
huffman@30097
   208
by auto (* delete? *)
paulson@14641
   209
huffman@24355
   210
lemma floor_real_of_nat [simp]: "floor (real (n::nat)) = int n"
huffman@30097
   211
unfolding real_of_nat_def by simp
paulson@14641
   212
huffman@24355
   213
lemma floor_minus_real_of_nat [simp]: "floor (- real (n::nat)) = - int n"
huffman@30102
   214
unfolding real_of_nat_def by (simp add: floor_minus)
paulson@14641
   215
paulson@14641
   216
lemma floor_real_of_int [simp]: "floor (real (n::int)) = n"
huffman@30097
   217
unfolding real_of_int_def by simp
paulson@14641
   218
paulson@14641
   219
lemma floor_minus_real_of_int [simp]: "floor (- real (n::int)) = - n"
huffman@30102
   220
unfolding real_of_int_def by (simp add: floor_minus)
paulson@14641
   221
paulson@14641
   222
lemma real_lb_ub_int: " \<exists>n::int. real n \<le> r & r < real (n+1)"
huffman@30097
   223
unfolding real_of_int_def by (rule floor_exists)
paulson@14641
   224
paulson@14641
   225
lemma lemma_floor:
paulson@14641
   226
  assumes a1: "real m \<le> r" and a2: "r < real n + 1"
paulson@14641
   227
  shows "m \<le> (n::int)"
paulson@14641
   228
proof -
wenzelm@23389
   229
  have "real m < real n + 1" using a1 a2 by (rule order_le_less_trans)
wenzelm@23389
   230
  also have "... = real (n + 1)" by simp
wenzelm@23389
   231
  finally have "m < n + 1" by (simp only: real_of_int_less_iff)
paulson@14641
   232
  thus ?thesis by arith
paulson@14641
   233
qed
paulson@14641
   234
paulson@14641
   235
lemma real_of_int_floor_le [simp]: "real (floor r) \<le> r"
huffman@30097
   236
unfolding real_of_int_def by (rule of_int_floor_le)
paulson@14641
   237
paulson@14641
   238
lemma lemma_floor2: "real n < real (x::int) + 1 ==> n \<le> x"
paulson@14641
   239
by (auto intro: lemma_floor)
paulson@14641
   240
paulson@14641
   241
lemma real_of_int_floor_cancel [simp]:
paulson@14641
   242
    "(real (floor x) = x) = (\<exists>n::int. x = real n)"
huffman@30097
   243
  using floor_real_of_int by metis
paulson@14641
   244
paulson@14641
   245
lemma floor_eq: "[| real n < x; x < real n + 1 |] ==> floor x = n"
huffman@30097
   246
  unfolding real_of_int_def using floor_unique [of n x] by simp
paulson@14641
   247
paulson@14641
   248
lemma floor_eq2: "[| real n \<le> x; x < real n + 1 |] ==> floor x = n"
huffman@30097
   249
  unfolding real_of_int_def by (rule floor_unique)
paulson@14641
   250
paulson@14641
   251
lemma floor_eq3: "[| real n < x; x < real (Suc n) |] ==> nat(floor x) = n"
paulson@14641
   252
apply (rule inj_int [THEN injD])
paulson@14641
   253
apply (simp add: real_of_nat_Suc)
nipkow@15539
   254
apply (simp add: real_of_nat_Suc floor_eq floor_eq [where n = "int n"])
paulson@14641
   255
done
paulson@14641
   256
paulson@14641
   257
lemma floor_eq4: "[| real n \<le> x; x < real (Suc n) |] ==> nat(floor x) = n"
paulson@14641
   258
apply (drule order_le_imp_less_or_eq)
paulson@14641
   259
apply (auto intro: floor_eq3)
paulson@14641
   260
done
paulson@14641
   261
huffman@30097
   262
lemma floor_number_of_eq:
paulson@14641
   263
     "floor(number_of n :: real) = (number_of n :: int)"
huffman@30097
   264
  by (rule floor_number_of) (* already declared [simp] *)
avigad@16819
   265
paulson@14641
   266
lemma real_of_int_floor_ge_diff_one [simp]: "r - 1 \<le> real(floor r)"
huffman@30097
   267
  unfolding real_of_int_def using floor_correct [of r] by simp
avigad@16819
   268
avigad@16819
   269
lemma real_of_int_floor_gt_diff_one [simp]: "r - 1 < real(floor r)"
huffman@30097
   270
  unfolding real_of_int_def using floor_correct [of r] by simp
paulson@14641
   271
paulson@14641
   272
lemma real_of_int_floor_add_one_ge [simp]: "r \<le> real(floor r) + 1"
huffman@30097
   273
  unfolding real_of_int_def using floor_correct [of r] by simp
paulson@14641
   274
avigad@16819
   275
lemma real_of_int_floor_add_one_gt [simp]: "r < real(floor r) + 1"
huffman@30097
   276
  unfolding real_of_int_def using floor_correct [of r] by simp
paulson@14641
   277
avigad@16819
   278
lemma le_floor: "real a <= x ==> a <= floor x"
huffman@30097
   279
  unfolding real_of_int_def by (simp add: le_floor_iff)
avigad@16819
   280
avigad@16819
   281
lemma real_le_floor: "a <= floor x ==> real a <= x"
huffman@30097
   282
  unfolding real_of_int_def by (simp add: le_floor_iff)
avigad@16819
   283
avigad@16819
   284
lemma le_floor_eq: "(a <= floor x) = (real a <= x)"
huffman@30097
   285
  unfolding real_of_int_def by (rule le_floor_iff)
avigad@16819
   286
huffman@30097
   287
lemma le_floor_eq_number_of:
avigad@16819
   288
    "(number_of n <= floor x) = (number_of n <= x)"
huffman@30097
   289
  by (rule number_of_le_floor) (* already declared [simp] *)
avigad@16819
   290
huffman@30097
   291
lemma le_floor_eq_zero: "(0 <= floor x) = (0 <= x)"
huffman@30097
   292
  by (rule zero_le_floor) (* already declared [simp] *)
avigad@16819
   293
huffman@30097
   294
lemma le_floor_eq_one: "(1 <= floor x) = (1 <= x)"
huffman@30097
   295
  by (rule one_le_floor) (* already declared [simp] *)
avigad@16819
   296
avigad@16819
   297
lemma floor_less_eq: "(floor x < a) = (x < real a)"
huffman@30097
   298
  unfolding real_of_int_def by (rule floor_less_iff)
avigad@16819
   299
huffman@30097
   300
lemma floor_less_eq_number_of:
avigad@16819
   301
    "(floor x < number_of n) = (x < number_of n)"
huffman@30097
   302
  by (rule floor_less_number_of) (* already declared [simp] *)
avigad@16819
   303
huffman@30097
   304
lemma floor_less_eq_zero: "(floor x < 0) = (x < 0)"
huffman@30097
   305
  by (rule floor_less_zero) (* already declared [simp] *)
avigad@16819
   306
huffman@30097
   307
lemma floor_less_eq_one: "(floor x < 1) = (x < 1)"
huffman@30097
   308
  by (rule floor_less_one) (* already declared [simp] *)
avigad@16819
   309
avigad@16819
   310
lemma less_floor_eq: "(a < floor x) = (real a + 1 <= x)"
huffman@30097
   311
  unfolding real_of_int_def by (rule less_floor_iff)
avigad@16819
   312
huffman@30097
   313
lemma less_floor_eq_number_of:
avigad@16819
   314
    "(number_of n < floor x) = (number_of n + 1 <= x)"
huffman@30097
   315
  by (rule number_of_less_floor) (* already declared [simp] *)
avigad@16819
   316
huffman@30097
   317
lemma less_floor_eq_zero: "(0 < floor x) = (1 <= x)"
huffman@30097
   318
  by (rule zero_less_floor) (* already declared [simp] *)
avigad@16819
   319
huffman@30097
   320
lemma less_floor_eq_one: "(1 < floor x) = (2 <= x)"
huffman@30097
   321
  by (rule one_less_floor) (* already declared [simp] *)
avigad@16819
   322
avigad@16819
   323
lemma floor_le_eq: "(floor x <= a) = (x < real a + 1)"
huffman@30097
   324
  unfolding real_of_int_def by (rule floor_le_iff)
avigad@16819
   325
huffman@30097
   326
lemma floor_le_eq_number_of:
avigad@16819
   327
    "(floor x <= number_of n) = (x < number_of n + 1)"
huffman@30097
   328
  by (rule floor_le_number_of) (* already declared [simp] *)
avigad@16819
   329
huffman@30097
   330
lemma floor_le_eq_zero: "(floor x <= 0) = (x < 1)"
huffman@30097
   331
  by (rule floor_le_zero) (* already declared [simp] *)
avigad@16819
   332
huffman@30097
   333
lemma floor_le_eq_one: "(floor x <= 1) = (x < 2)"
huffman@30097
   334
  by (rule floor_le_one) (* already declared [simp] *)
avigad@16819
   335
avigad@16819
   336
lemma floor_add [simp]: "floor (x + real a) = floor x + a"
huffman@30097
   337
  unfolding real_of_int_def by (rule floor_add_of_int)
avigad@16819
   338
avigad@16819
   339
lemma floor_subtract [simp]: "floor (x - real a) = floor x - a"
huffman@30097
   340
  unfolding real_of_int_def by (rule floor_diff_of_int)
avigad@16819
   341
huffman@30097
   342
lemma floor_subtract_number_of: "floor (x - number_of n) =
avigad@16819
   343
    floor x - number_of n"
huffman@30097
   344
  by (rule floor_diff_number_of) (* already declared [simp] *)
avigad@16819
   345
huffman@30097
   346
lemma floor_subtract_one: "floor (x - 1) = floor x - 1"
huffman@30097
   347
  by (rule floor_diff_one) (* already declared [simp] *)
paulson@14641
   348
hoelzl@35578
   349
lemma le_mult_floor:
hoelzl@35578
   350
  assumes "0 \<le> (a :: real)" and "0 \<le> b"
hoelzl@35578
   351
  shows "floor a * floor b \<le> floor (a * b)"
hoelzl@35578
   352
proof -
hoelzl@35578
   353
  have "real (floor a) \<le> a"
hoelzl@35578
   354
    and "real (floor b) \<le> b" by auto
hoelzl@35578
   355
  hence "real (floor a * floor b) \<le> a * b"
hoelzl@35578
   356
    using assms by (auto intro!: mult_mono)
hoelzl@35578
   357
  also have "a * b < real (floor (a * b) + 1)" by auto
hoelzl@35578
   358
  finally show ?thesis unfolding real_of_int_less_iff by simp
hoelzl@35578
   359
qed
hoelzl@35578
   360
huffman@24355
   361
lemma ceiling_real_of_nat [simp]: "ceiling (real (n::nat)) = int n"
huffman@30097
   362
  unfolding real_of_nat_def by simp
paulson@14641
   363
huffman@30097
   364
lemma ceiling_real_of_nat_zero: "ceiling (real (0::nat)) = 0"
huffman@30097
   365
by auto (* delete? *)
paulson@14641
   366
paulson@14641
   367
lemma ceiling_floor [simp]: "ceiling (real (floor r)) = floor r"
huffman@30097
   368
  unfolding real_of_int_def by simp
paulson@14641
   369
paulson@14641
   370
lemma floor_ceiling [simp]: "floor (real (ceiling r)) = ceiling r"
huffman@30097
   371
  unfolding real_of_int_def by simp
paulson@14641
   372
paulson@14641
   373
lemma real_of_int_ceiling_ge [simp]: "r \<le> real (ceiling r)"
huffman@30097
   374
  unfolding real_of_int_def by (rule le_of_int_ceiling)
paulson@14641
   375
huffman@30097
   376
lemma ceiling_real_of_int [simp]: "ceiling (real (n::int)) = n"
huffman@30097
   377
  unfolding real_of_int_def by simp
paulson@14641
   378
paulson@14641
   379
lemma real_of_int_ceiling_cancel [simp]:
paulson@14641
   380
     "(real (ceiling x) = x) = (\<exists>n::int. x = real n)"
huffman@30097
   381
  using ceiling_real_of_int by metis
paulson@14641
   382
paulson@14641
   383
lemma ceiling_eq: "[| real n < x; x < real n + 1 |] ==> ceiling x = n + 1"
huffman@30097
   384
  unfolding real_of_int_def using ceiling_unique [of "n + 1" x] by simp
paulson@14641
   385
paulson@14641
   386
lemma ceiling_eq2: "[| real n < x; x \<le> real n + 1 |] ==> ceiling x = n + 1"
huffman@30097
   387
  unfolding real_of_int_def using ceiling_unique [of "n + 1" x] by simp
paulson@14641
   388
paulson@14641
   389
lemma ceiling_eq3: "[| real n - 1 < x; x \<le> real n  |] ==> ceiling x = n"
huffman@30097
   390
  unfolding real_of_int_def using ceiling_unique [of n x] by simp
paulson@14641
   391
huffman@30097
   392
lemma ceiling_number_of_eq:
paulson@14641
   393
     "ceiling (number_of n :: real) = (number_of n)"
huffman@30097
   394
  by (rule ceiling_number_of) (* already declared [simp] *)
avigad@16819
   395
paulson@14641
   396
lemma real_of_int_ceiling_diff_one_le [simp]: "real (ceiling r) - 1 \<le> r"
huffman@30097
   397
  unfolding real_of_int_def using ceiling_correct [of r] by simp
paulson@14641
   398
paulson@14641
   399
lemma real_of_int_ceiling_le_add_one [simp]: "real (ceiling r) \<le> r + 1"
huffman@30097
   400
  unfolding real_of_int_def using ceiling_correct [of r] by simp
paulson@14641
   401
avigad@16819
   402
lemma ceiling_le: "x <= real a ==> ceiling x <= a"
huffman@30097
   403
  unfolding real_of_int_def by (simp add: ceiling_le_iff)
avigad@16819
   404
avigad@16819
   405
lemma ceiling_le_real: "ceiling x <= a ==> x <= real a"
huffman@30097
   406
  unfolding real_of_int_def by (simp add: ceiling_le_iff)
avigad@16819
   407
avigad@16819
   408
lemma ceiling_le_eq: "(ceiling x <= a) = (x <= real a)"
huffman@30097
   409
  unfolding real_of_int_def by (rule ceiling_le_iff)
avigad@16819
   410
huffman@30097
   411
lemma ceiling_le_eq_number_of:
avigad@16819
   412
    "(ceiling x <= number_of n) = (x <= number_of n)"
huffman@30097
   413
  by (rule ceiling_le_number_of) (* already declared [simp] *)
avigad@16819
   414
huffman@30097
   415
lemma ceiling_le_zero_eq: "(ceiling x <= 0) = (x <= 0)"
huffman@30097
   416
  by (rule ceiling_le_zero) (* already declared [simp] *)
avigad@16819
   417
huffman@30097
   418
lemma ceiling_le_eq_one: "(ceiling x <= 1) = (x <= 1)"
huffman@30097
   419
  by (rule ceiling_le_one) (* already declared [simp] *)
avigad@16819
   420
avigad@16819
   421
lemma less_ceiling_eq: "(a < ceiling x) = (real a < x)"
huffman@30097
   422
  unfolding real_of_int_def by (rule less_ceiling_iff)
avigad@16819
   423
huffman@30097
   424
lemma less_ceiling_eq_number_of:
avigad@16819
   425
    "(number_of n < ceiling x) = (number_of n < x)"
huffman@30097
   426
  by (rule number_of_less_ceiling) (* already declared [simp] *)
avigad@16819
   427
huffman@30097
   428
lemma less_ceiling_eq_zero: "(0 < ceiling x) = (0 < x)"
huffman@30097
   429
  by (rule zero_less_ceiling) (* already declared [simp] *)
avigad@16819
   430
huffman@30097
   431
lemma less_ceiling_eq_one: "(1 < ceiling x) = (1 < x)"
huffman@30097
   432
  by (rule one_less_ceiling) (* already declared [simp] *)
avigad@16819
   433
avigad@16819
   434
lemma ceiling_less_eq: "(ceiling x < a) = (x <= real a - 1)"
huffman@30097
   435
  unfolding real_of_int_def by (rule ceiling_less_iff)
avigad@16819
   436
huffman@30097
   437
lemma ceiling_less_eq_number_of:
avigad@16819
   438
    "(ceiling x < number_of n) = (x <= number_of n - 1)"
huffman@30097
   439
  by (rule ceiling_less_number_of) (* already declared [simp] *)
avigad@16819
   440
huffman@30097
   441
lemma ceiling_less_eq_zero: "(ceiling x < 0) = (x <= -1)"
huffman@30097
   442
  by (rule ceiling_less_zero) (* already declared [simp] *)
avigad@16819
   443
huffman@30097
   444
lemma ceiling_less_eq_one: "(ceiling x < 1) = (x <= 0)"
huffman@30097
   445
  by (rule ceiling_less_one) (* already declared [simp] *)
avigad@16819
   446
avigad@16819
   447
lemma le_ceiling_eq: "(a <= ceiling x) = (real a - 1 < x)"
huffman@30097
   448
  unfolding real_of_int_def by (rule le_ceiling_iff)
avigad@16819
   449
huffman@30097
   450
lemma le_ceiling_eq_number_of:
avigad@16819
   451
    "(number_of n <= ceiling x) = (number_of n - 1 < x)"
huffman@30097
   452
  by (rule number_of_le_ceiling) (* already declared [simp] *)
avigad@16819
   453
huffman@30097
   454
lemma le_ceiling_eq_zero: "(0 <= ceiling x) = (-1 < x)"
huffman@30097
   455
  by (rule zero_le_ceiling) (* already declared [simp] *)
avigad@16819
   456
huffman@30097
   457
lemma le_ceiling_eq_one: "(1 <= ceiling x) = (0 < x)"
huffman@30097
   458
  by (rule one_le_ceiling) (* already declared [simp] *)
avigad@16819
   459
avigad@16819
   460
lemma ceiling_add [simp]: "ceiling (x + real a) = ceiling x + a"
huffman@30097
   461
  unfolding real_of_int_def by (rule ceiling_add_of_int)
avigad@16819
   462
avigad@16819
   463
lemma ceiling_subtract [simp]: "ceiling (x - real a) = ceiling x - a"
huffman@30097
   464
  unfolding real_of_int_def by (rule ceiling_diff_of_int)
avigad@16819
   465
huffman@30097
   466
lemma ceiling_subtract_number_of: "ceiling (x - number_of n) =
avigad@16819
   467
    ceiling x - number_of n"
huffman@30097
   468
  by (rule ceiling_diff_number_of) (* already declared [simp] *)
avigad@16819
   469
huffman@30097
   470
lemma ceiling_subtract_one: "ceiling (x - 1) = ceiling x - 1"
huffman@30097
   471
  by (rule ceiling_diff_one) (* already declared [simp] *)
huffman@30097
   472
avigad@16819
   473
avigad@16819
   474
subsection {* Versions for the natural numbers *}
avigad@16819
   475
wenzelm@19765
   476
definition
wenzelm@21404
   477
  natfloor :: "real => nat" where
wenzelm@19765
   478
  "natfloor x = nat(floor x)"
wenzelm@21404
   479
wenzelm@21404
   480
definition
wenzelm@21404
   481
  natceiling :: "real => nat" where
wenzelm@19765
   482
  "natceiling x = nat(ceiling x)"
avigad@16819
   483
avigad@16819
   484
lemma natfloor_zero [simp]: "natfloor 0 = 0"
avigad@16819
   485
  by (unfold natfloor_def, simp)
avigad@16819
   486
avigad@16819
   487
lemma natfloor_one [simp]: "natfloor 1 = 1"
avigad@16819
   488
  by (unfold natfloor_def, simp)
avigad@16819
   489
avigad@16819
   490
lemma zero_le_natfloor [simp]: "0 <= natfloor x"
avigad@16819
   491
  by (unfold natfloor_def, simp)
avigad@16819
   492
avigad@16819
   493
lemma natfloor_number_of_eq [simp]: "natfloor (number_of n) = number_of n"
avigad@16819
   494
  by (unfold natfloor_def, simp)
avigad@16819
   495
avigad@16819
   496
lemma natfloor_real_of_nat [simp]: "natfloor(real n) = n"
avigad@16819
   497
  by (unfold natfloor_def, simp)
avigad@16819
   498
avigad@16819
   499
lemma real_natfloor_le: "0 <= x ==> real(natfloor x) <= x"
avigad@16819
   500
  by (unfold natfloor_def, simp)
avigad@16819
   501
avigad@16819
   502
lemma natfloor_neg: "x <= 0 ==> natfloor x = 0"
avigad@16819
   503
  apply (unfold natfloor_def)
avigad@16819
   504
  apply (subgoal_tac "floor x <= floor 0")
avigad@16819
   505
  apply simp
huffman@30097
   506
  apply (erule floor_mono)
avigad@16819
   507
done
avigad@16819
   508
avigad@16819
   509
lemma natfloor_mono: "x <= y ==> natfloor x <= natfloor y"
avigad@16819
   510
  apply (case_tac "0 <= x")
avigad@16819
   511
  apply (subst natfloor_def)+
avigad@16819
   512
  apply (subst nat_le_eq_zle)
avigad@16819
   513
  apply force
huffman@30097
   514
  apply (erule floor_mono)
avigad@16819
   515
  apply (subst natfloor_neg)
avigad@16819
   516
  apply simp
avigad@16819
   517
  apply simp
avigad@16819
   518
done
avigad@16819
   519
avigad@16819
   520
lemma le_natfloor: "real x <= a ==> x <= natfloor a"
avigad@16819
   521
  apply (unfold natfloor_def)
avigad@16819
   522
  apply (subst nat_int [THEN sym])
avigad@16819
   523
  apply (subst nat_le_eq_zle)
avigad@16819
   524
  apply simp
avigad@16819
   525
  apply (rule le_floor)
avigad@16819
   526
  apply simp
avigad@16819
   527
done
avigad@16819
   528
hoelzl@35578
   529
lemma less_natfloor:
hoelzl@35578
   530
  assumes "0 \<le> x" and "x < real (n :: nat)"
hoelzl@35578
   531
  shows "natfloor x < n"
hoelzl@35578
   532
proof (rule ccontr)
hoelzl@35578
   533
  assume "\<not> ?thesis" hence *: "n \<le> natfloor x" by simp
hoelzl@35578
   534
  note assms(2)
hoelzl@35578
   535
  also have "real n \<le> real (natfloor x)"
hoelzl@35578
   536
    using * unfolding real_of_nat_le_iff .
hoelzl@35578
   537
  finally have "x < real (natfloor x)" .
hoelzl@35578
   538
  with real_natfloor_le[OF assms(1)]
hoelzl@35578
   539
  show False by auto
hoelzl@35578
   540
qed
hoelzl@35578
   541
avigad@16819
   542
lemma le_natfloor_eq: "0 <= x ==> (a <= natfloor x) = (real a <= x)"
avigad@16819
   543
  apply (rule iffI)
avigad@16819
   544
  apply (rule order_trans)
avigad@16819
   545
  prefer 2
avigad@16819
   546
  apply (erule real_natfloor_le)
avigad@16819
   547
  apply (subst real_of_nat_le_iff)
avigad@16819
   548
  apply assumption
avigad@16819
   549
  apply (erule le_natfloor)
avigad@16819
   550
done
avigad@16819
   551
wenzelm@16893
   552
lemma le_natfloor_eq_number_of [simp]:
avigad@16819
   553
    "~ neg((number_of n)::int) ==> 0 <= x ==>
avigad@16819
   554
      (number_of n <= natfloor x) = (number_of n <= x)"
avigad@16819
   555
  apply (subst le_natfloor_eq, assumption)
avigad@16819
   556
  apply simp
avigad@16819
   557
done
avigad@16819
   558
avigad@16820
   559
lemma le_natfloor_eq_one [simp]: "(1 <= natfloor x) = (1 <= x)"
avigad@16819
   560
  apply (case_tac "0 <= x")
avigad@16819
   561
  apply (subst le_natfloor_eq, assumption, simp)
avigad@16819
   562
  apply (rule iffI)
wenzelm@16893
   563
  apply (subgoal_tac "natfloor x <= natfloor 0")
avigad@16819
   564
  apply simp
avigad@16819
   565
  apply (rule natfloor_mono)
avigad@16819
   566
  apply simp
avigad@16819
   567
  apply simp
avigad@16819
   568
done
avigad@16819
   569
avigad@16819
   570
lemma natfloor_eq: "real n <= x ==> x < real n + 1 ==> natfloor x = n"
avigad@16819
   571
  apply (unfold natfloor_def)
hoelzl@35578
   572
  apply (subst (2) nat_int [THEN sym])
avigad@16819
   573
  apply (subst eq_nat_nat_iff)
avigad@16819
   574
  apply simp
avigad@16819
   575
  apply simp
avigad@16819
   576
  apply (rule floor_eq2)
avigad@16819
   577
  apply auto
avigad@16819
   578
done
avigad@16819
   579
avigad@16819
   580
lemma real_natfloor_add_one_gt: "x < real(natfloor x) + 1"
avigad@16819
   581
  apply (case_tac "0 <= x")
avigad@16819
   582
  apply (unfold natfloor_def)
avigad@16819
   583
  apply simp
avigad@16819
   584
  apply simp_all
avigad@16819
   585
done
avigad@16819
   586
avigad@16819
   587
lemma real_natfloor_gt_diff_one: "x - 1 < real(natfloor x)"
nipkow@29667
   588
using real_natfloor_add_one_gt by (simp add: algebra_simps)
avigad@16819
   589
avigad@16819
   590
lemma ge_natfloor_plus_one_imp_gt: "natfloor z + 1 <= n ==> z < real n"
avigad@16819
   591
  apply (subgoal_tac "z < real(natfloor z) + 1")
avigad@16819
   592
  apply arith
avigad@16819
   593
  apply (rule real_natfloor_add_one_gt)
avigad@16819
   594
done
avigad@16819
   595
avigad@16819
   596
lemma natfloor_add [simp]: "0 <= x ==> natfloor (x + real a) = natfloor x + a"
avigad@16819
   597
  apply (unfold natfloor_def)
huffman@24355
   598
  apply (subgoal_tac "real a = real (int a)")
avigad@16819
   599
  apply (erule ssubst)
huffman@23309
   600
  apply (simp add: nat_add_distrib del: real_of_int_of_nat_eq)
avigad@16819
   601
  apply simp
avigad@16819
   602
done
avigad@16819
   603
wenzelm@16893
   604
lemma natfloor_add_number_of [simp]:
wenzelm@16893
   605
    "~neg ((number_of n)::int) ==> 0 <= x ==>
avigad@16819
   606
      natfloor (x + number_of n) = natfloor x + number_of n"
avigad@16819
   607
  apply (subst natfloor_add [THEN sym])
avigad@16819
   608
  apply simp_all
avigad@16819
   609
done
avigad@16819
   610
avigad@16819
   611
lemma natfloor_add_one: "0 <= x ==> natfloor(x + 1) = natfloor x + 1"
avigad@16819
   612
  apply (subst natfloor_add [THEN sym])
avigad@16819
   613
  apply assumption
avigad@16819
   614
  apply simp
avigad@16819
   615
done
avigad@16819
   616
wenzelm@16893
   617
lemma natfloor_subtract [simp]: "real a <= x ==>
avigad@16819
   618
    natfloor(x - real a) = natfloor x - a"
avigad@16819
   619
  apply (unfold natfloor_def)
huffman@24355
   620
  apply (subgoal_tac "real a = real (int a)")
avigad@16819
   621
  apply (erule ssubst)
huffman@23309
   622
  apply (simp del: real_of_int_of_nat_eq)
avigad@16819
   623
  apply simp
avigad@16819
   624
done
avigad@16819
   625
hoelzl@35578
   626
lemma natfloor_div_nat: "1 <= x ==> y > 0 ==>
hoelzl@35578
   627
  natfloor (x / real y) = natfloor x div y"
hoelzl@35578
   628
proof -
hoelzl@35578
   629
  assume "1 <= (x::real)" and "(y::nat) > 0"
hoelzl@35578
   630
  have "natfloor x = (natfloor x) div y * y + (natfloor x) mod y"
hoelzl@35578
   631
    by simp
hoelzl@35578
   632
  then have a: "real(natfloor x) = real ((natfloor x) div y) * real y +
hoelzl@35578
   633
    real((natfloor x) mod y)"
hoelzl@35578
   634
    by (simp only: real_of_nat_add [THEN sym] real_of_nat_mult [THEN sym])
hoelzl@35578
   635
  have "x = real(natfloor x) + (x - real(natfloor x))"
hoelzl@35578
   636
    by simp
hoelzl@35578
   637
  then have "x = real ((natfloor x) div y) * real y +
hoelzl@35578
   638
      real((natfloor x) mod y) + (x - real(natfloor x))"
hoelzl@35578
   639
    by (simp add: a)
hoelzl@35578
   640
  then have "x / real y = ... / real y"
hoelzl@35578
   641
    by simp
hoelzl@35578
   642
  also have "... = real((natfloor x) div y) + real((natfloor x) mod y) /
hoelzl@35578
   643
    real y + (x - real(natfloor x)) / real y"
hoelzl@35578
   644
    by (auto simp add: algebra_simps add_divide_distrib
hoelzl@35578
   645
      diff_divide_distrib prems)
hoelzl@35578
   646
  finally have "natfloor (x / real y) = natfloor(...)" by simp
hoelzl@35578
   647
  also have "... = natfloor(real((natfloor x) mod y) /
hoelzl@35578
   648
    real y + (x - real(natfloor x)) / real y + real((natfloor x) div y))"
hoelzl@35578
   649
    by (simp add: add_ac)
hoelzl@35578
   650
  also have "... = natfloor(real((natfloor x) mod y) /
hoelzl@35578
   651
    real y + (x - real(natfloor x)) / real y) + (natfloor x) div y"
hoelzl@35578
   652
    apply (rule natfloor_add)
hoelzl@35578
   653
    apply (rule add_nonneg_nonneg)
hoelzl@35578
   654
    apply (rule divide_nonneg_pos)
hoelzl@35578
   655
    apply simp
hoelzl@35578
   656
    apply (simp add: prems)
hoelzl@35578
   657
    apply (rule divide_nonneg_pos)
hoelzl@35578
   658
    apply (simp add: algebra_simps)
hoelzl@35578
   659
    apply (rule real_natfloor_le)
hoelzl@35578
   660
    apply (insert prems, auto)
hoelzl@35578
   661
    done
hoelzl@35578
   662
  also have "natfloor(real((natfloor x) mod y) /
hoelzl@35578
   663
    real y + (x - real(natfloor x)) / real y) = 0"
hoelzl@35578
   664
    apply (rule natfloor_eq)
hoelzl@35578
   665
    apply simp
hoelzl@35578
   666
    apply (rule add_nonneg_nonneg)
hoelzl@35578
   667
    apply (rule divide_nonneg_pos)
hoelzl@35578
   668
    apply force
hoelzl@35578
   669
    apply (force simp add: prems)
hoelzl@35578
   670
    apply (rule divide_nonneg_pos)
hoelzl@35578
   671
    apply (simp add: algebra_simps)
hoelzl@35578
   672
    apply (rule real_natfloor_le)
hoelzl@35578
   673
    apply (auto simp add: prems)
hoelzl@35578
   674
    apply (insert prems, arith)
hoelzl@35578
   675
    apply (simp add: add_divide_distrib [THEN sym])
hoelzl@35578
   676
    apply (subgoal_tac "real y = real y - 1 + 1")
hoelzl@35578
   677
    apply (erule ssubst)
hoelzl@35578
   678
    apply (rule add_le_less_mono)
hoelzl@35578
   679
    apply (simp add: algebra_simps)
hoelzl@35578
   680
    apply (subgoal_tac "1 + real(natfloor x mod y) =
hoelzl@35578
   681
      real(natfloor x mod y + 1)")
hoelzl@35578
   682
    apply (erule ssubst)
hoelzl@35578
   683
    apply (subst real_of_nat_le_iff)
hoelzl@35578
   684
    apply (subgoal_tac "natfloor x mod y < y")
hoelzl@35578
   685
    apply arith
hoelzl@35578
   686
    apply (rule mod_less_divisor)
hoelzl@35578
   687
    apply auto
hoelzl@35578
   688
    using real_natfloor_add_one_gt
hoelzl@35578
   689
    apply (simp add: algebra_simps)
hoelzl@35578
   690
    done
hoelzl@35578
   691
  finally show ?thesis by simp
hoelzl@35578
   692
qed
hoelzl@35578
   693
hoelzl@35578
   694
lemma le_mult_natfloor:
hoelzl@35578
   695
  assumes "0 \<le> (a :: real)" and "0 \<le> b"
hoelzl@35578
   696
  shows "natfloor a * natfloor b \<le> natfloor (a * b)"
hoelzl@35578
   697
  unfolding natfloor_def
hoelzl@35578
   698
  apply (subst nat_mult_distrib[symmetric])
hoelzl@35578
   699
  using assms apply simp
hoelzl@35578
   700
  apply (subst nat_le_eq_zle)
hoelzl@35578
   701
  using assms le_mult_floor by (auto intro!: mult_nonneg_nonneg)
hoelzl@35578
   702
avigad@16819
   703
lemma natceiling_zero [simp]: "natceiling 0 = 0"
avigad@16819
   704
  by (unfold natceiling_def, simp)
avigad@16819
   705
avigad@16819
   706
lemma natceiling_one [simp]: "natceiling 1 = 1"
avigad@16819
   707
  by (unfold natceiling_def, simp)
avigad@16819
   708
avigad@16819
   709
lemma zero_le_natceiling [simp]: "0 <= natceiling x"
avigad@16819
   710
  by (unfold natceiling_def, simp)
avigad@16819
   711
avigad@16819
   712
lemma natceiling_number_of_eq [simp]: "natceiling (number_of n) = number_of n"
avigad@16819
   713
  by (unfold natceiling_def, simp)
avigad@16819
   714
avigad@16819
   715
lemma natceiling_real_of_nat [simp]: "natceiling(real n) = n"
avigad@16819
   716
  by (unfold natceiling_def, simp)
avigad@16819
   717
avigad@16819
   718
lemma real_natceiling_ge: "x <= real(natceiling x)"
avigad@16819
   719
  apply (unfold natceiling_def)
avigad@16819
   720
  apply (case_tac "x < 0")
avigad@16819
   721
  apply simp
avigad@16819
   722
  apply (subst real_nat_eq_real)
avigad@16819
   723
  apply (subgoal_tac "ceiling 0 <= ceiling x")
avigad@16819
   724
  apply simp
huffman@30097
   725
  apply (rule ceiling_mono)
avigad@16819
   726
  apply simp
avigad@16819
   727
  apply simp
avigad@16819
   728
done
avigad@16819
   729
avigad@16819
   730
lemma natceiling_neg: "x <= 0 ==> natceiling x = 0"
avigad@16819
   731
  apply (unfold natceiling_def)
avigad@16819
   732
  apply simp
avigad@16819
   733
done
avigad@16819
   734
avigad@16819
   735
lemma natceiling_mono: "x <= y ==> natceiling x <= natceiling y"
avigad@16819
   736
  apply (case_tac "0 <= x")
avigad@16819
   737
  apply (subst natceiling_def)+
avigad@16819
   738
  apply (subst nat_le_eq_zle)
avigad@16819
   739
  apply (rule disjI2)
avigad@16819
   740
  apply (subgoal_tac "real (0::int) <= real(ceiling y)")
avigad@16819
   741
  apply simp
avigad@16819
   742
  apply (rule order_trans)
avigad@16819
   743
  apply simp
avigad@16819
   744
  apply (erule order_trans)
avigad@16819
   745
  apply simp
huffman@30097
   746
  apply (erule ceiling_mono)
avigad@16819
   747
  apply (subst natceiling_neg)
avigad@16819
   748
  apply simp_all
avigad@16819
   749
done
avigad@16819
   750
avigad@16819
   751
lemma natceiling_le: "x <= real a ==> natceiling x <= a"
avigad@16819
   752
  apply (unfold natceiling_def)
avigad@16819
   753
  apply (case_tac "x < 0")
avigad@16819
   754
  apply simp
hoelzl@35578
   755
  apply (subst (2) nat_int [THEN sym])
avigad@16819
   756
  apply (subst nat_le_eq_zle)
avigad@16819
   757
  apply simp
avigad@16819
   758
  apply (rule ceiling_le)
avigad@16819
   759
  apply simp
avigad@16819
   760
done
avigad@16819
   761
avigad@16819
   762
lemma natceiling_le_eq: "0 <= x ==> (natceiling x <= a) = (x <= real a)"
avigad@16819
   763
  apply (rule iffI)
avigad@16819
   764
  apply (rule order_trans)
avigad@16819
   765
  apply (rule real_natceiling_ge)
avigad@16819
   766
  apply (subst real_of_nat_le_iff)
avigad@16819
   767
  apply assumption
avigad@16819
   768
  apply (erule natceiling_le)
avigad@16819
   769
done
avigad@16819
   770
wenzelm@16893
   771
lemma natceiling_le_eq_number_of [simp]:
avigad@16820
   772
    "~ neg((number_of n)::int) ==> 0 <= x ==>
avigad@16820
   773
      (natceiling x <= number_of n) = (x <= number_of n)"
avigad@16819
   774
  apply (subst natceiling_le_eq, assumption)
avigad@16819
   775
  apply simp
avigad@16819
   776
done
avigad@16819
   777
avigad@16820
   778
lemma natceiling_le_eq_one: "(natceiling x <= 1) = (x <= 1)"
avigad@16819
   779
  apply (case_tac "0 <= x")
avigad@16819
   780
  apply (subst natceiling_le_eq)
avigad@16819
   781
  apply assumption
avigad@16819
   782
  apply simp
avigad@16819
   783
  apply (subst natceiling_neg)
avigad@16819
   784
  apply simp
avigad@16819
   785
  apply simp
avigad@16819
   786
done
avigad@16819
   787
avigad@16819
   788
lemma natceiling_eq: "real n < x ==> x <= real n + 1 ==> natceiling x = n + 1"
avigad@16819
   789
  apply (unfold natceiling_def)
wenzelm@19850
   790
  apply (simplesubst nat_int [THEN sym]) back back
avigad@16819
   791
  apply (subgoal_tac "nat(int n) + 1 = nat(int n + 1)")
avigad@16819
   792
  apply (erule ssubst)
avigad@16819
   793
  apply (subst eq_nat_nat_iff)
avigad@16819
   794
  apply (subgoal_tac "ceiling 0 <= ceiling x")
avigad@16819
   795
  apply simp
huffman@30097
   796
  apply (rule ceiling_mono)
avigad@16819
   797
  apply force
avigad@16819
   798
  apply force
avigad@16819
   799
  apply (rule ceiling_eq2)
avigad@16819
   800
  apply (simp, simp)
avigad@16819
   801
  apply (subst nat_add_distrib)
avigad@16819
   802
  apply auto
avigad@16819
   803
done
avigad@16819
   804
wenzelm@16893
   805
lemma natceiling_add [simp]: "0 <= x ==>
avigad@16819
   806
    natceiling (x + real a) = natceiling x + a"
avigad@16819
   807
  apply (unfold natceiling_def)
huffman@24355
   808
  apply (subgoal_tac "real a = real (int a)")
avigad@16819
   809
  apply (erule ssubst)
huffman@23309
   810
  apply (simp del: real_of_int_of_nat_eq)
avigad@16819
   811
  apply (subst nat_add_distrib)
avigad@16819
   812
  apply (subgoal_tac "0 = ceiling 0")
avigad@16819
   813
  apply (erule ssubst)
huffman@30097
   814
  apply (erule ceiling_mono)
avigad@16819
   815
  apply simp_all
avigad@16819
   816
done
avigad@16819
   817
wenzelm@16893
   818
lemma natceiling_add_number_of [simp]:
wenzelm@16893
   819
    "~ neg ((number_of n)::int) ==> 0 <= x ==>
avigad@16820
   820
      natceiling (x + number_of n) = natceiling x + number_of n"
avigad@16819
   821
  apply (subst natceiling_add [THEN sym])
avigad@16819
   822
  apply simp_all
avigad@16819
   823
done
avigad@16819
   824
avigad@16819
   825
lemma natceiling_add_one: "0 <= x ==> natceiling(x + 1) = natceiling x + 1"
avigad@16819
   826
  apply (subst natceiling_add [THEN sym])
avigad@16819
   827
  apply assumption
avigad@16819
   828
  apply simp
avigad@16819
   829
done
avigad@16819
   830
wenzelm@16893
   831
lemma natceiling_subtract [simp]: "real a <= x ==>
avigad@16819
   832
    natceiling(x - real a) = natceiling x - a"
avigad@16819
   833
  apply (unfold natceiling_def)
huffman@24355
   834
  apply (subgoal_tac "real a = real (int a)")
avigad@16819
   835
  apply (erule ssubst)
huffman@23309
   836
  apply (simp del: real_of_int_of_nat_eq)
avigad@16819
   837
  apply simp
avigad@16819
   838
done
avigad@16819
   839
avigad@16819
   840
paulson@14365
   841
end