src/HOL/Real/RComplete.thy
author avigad
Wed Jul 13 19:49:07 2005 +0200 (2005-07-13)
changeset 16819 00d8f9300d13
parent 15539 333a88244569
child 16820 5c9d597e4cb9
permissions -rw-r--r--
Additions to the Real (and Hyperreal) libraries:
RealDef.thy: lemmas relating nats, ints, and reals
reversed direction of real_of_int_mult, etc. (now they agree with nat versions)
SEQ.thy and Series.thy: various additions
RComplete.thy: lemmas involving floor and ceiling
introduced natfloor and natceiling
Log.thy: various additions
paulson@5078
     1
(*  Title       : RComplete.thy
paulson@7219
     2
    ID          : $Id$
paulson@5078
     3
    Author      : Jacques D. Fleuriot
avigad@16819
     4
                  Converted to Isar and polished by lcp
avigad@16819
     5
                  Most floor and ceiling lemmas by Jeremy Avigad
paulson@5078
     6
    Copyright   : 1998  University of Cambridge
paulson@14641
     7
    Copyright   : 2001,2002  University of Edinburgh
paulson@5078
     8
*) 
paulson@5078
     9
paulson@14641
    10
header{*Completeness of the Reals; Floor and Ceiling Functions*}
paulson@14365
    11
nipkow@15131
    12
theory RComplete
nipkow@15140
    13
imports Lubs RealDef
nipkow@15131
    14
begin
paulson@14365
    15
paulson@14365
    16
lemma real_sum_of_halves: "x/2 + x/2 = (x::real)"
paulson@14387
    17
by simp
paulson@14365
    18
paulson@14365
    19
paulson@14365
    20
subsection{*Completeness of Reals by Supremum Property of type @{typ preal}*} 
paulson@14365
    21
paulson@14365
    22
 (*a few lemmas*)
paulson@14365
    23
lemma real_sup_lemma1:
paulson@14365
    24
     "\<forall>x \<in> P. 0 < x ==>   
paulson@14365
    25
      ((\<exists>x \<in> P. y < x) = (\<exists>X. real_of_preal X \<in> P & y < real_of_preal X))"
paulson@14365
    26
by (blast dest!: bspec real_gt_zero_preal_Ex [THEN iffD1])
paulson@14365
    27
paulson@14365
    28
lemma real_sup_lemma2:
paulson@14365
    29
     "[| \<forall>x \<in> P. 0 < x;  a \<in> P;   \<forall>x \<in> P. x < y |]  
paulson@14365
    30
      ==> (\<exists>X. X\<in> {w. real_of_preal w \<in> P}) &  
paulson@14365
    31
          (\<exists>Y. \<forall>X\<in> {w. real_of_preal w \<in> P}. X < Y)"
paulson@14365
    32
apply (rule conjI)
paulson@14365
    33
apply (blast dest: bspec real_gt_zero_preal_Ex [THEN iffD1], auto)
paulson@14365
    34
apply (drule bspec, assumption)
paulson@14365
    35
apply (frule bspec, assumption)
paulson@14365
    36
apply (drule order_less_trans, assumption)
paulson@14387
    37
apply (drule real_gt_zero_preal_Ex [THEN iffD1], force) 
paulson@14365
    38
done
paulson@14365
    39
paulson@14365
    40
(*-------------------------------------------------------------
paulson@14365
    41
            Completeness of Positive Reals
paulson@14365
    42
 -------------------------------------------------------------*)
paulson@14365
    43
paulson@14365
    44
(**
paulson@14365
    45
 Supremum property for the set of positive reals
paulson@14365
    46
 FIXME: long proof - should be improved
paulson@14365
    47
**)
paulson@14365
    48
paulson@14365
    49
(*Let P be a non-empty set of positive reals, with an upper bound y.
paulson@14365
    50
  Then P has a least upper bound (written S).  
paulson@14365
    51
FIXME: Can the premise be weakened to \<forall>x \<in> P. x\<le> y ??*)
paulson@14365
    52
lemma posreal_complete: "[| \<forall>x \<in> P. (0::real) < x;  \<exists>x. x \<in> P;  \<exists>y. \<forall>x \<in> P. x<y |]  
paulson@14365
    53
      ==> (\<exists>S. \<forall>y. (\<exists>x \<in> P. y < x) = (y < S))"
paulson@14365
    54
apply (rule_tac x = "real_of_preal (psup ({w. real_of_preal w \<in> P}))" in exI)
paulson@14365
    55
apply clarify
paulson@14365
    56
apply (case_tac "0 < ya", auto)
paulson@14365
    57
apply (frule real_sup_lemma2, assumption+)
paulson@14365
    58
apply (drule real_gt_zero_preal_Ex [THEN iffD1])
paulson@14387
    59
apply (drule_tac [3] real_less_all_real2, auto)
paulson@14365
    60
apply (rule preal_complete [THEN iffD1])
paulson@14365
    61
apply (auto intro: order_less_imp_le)
paulson@14387
    62
apply (frule real_gt_preal_preal_Ex, force)
paulson@14365
    63
(* second part *)
paulson@14365
    64
apply (rule real_sup_lemma1 [THEN iffD2], assumption)
paulson@14365
    65
apply (auto dest!: real_less_all_real2 real_gt_zero_preal_Ex [THEN iffD1])
paulson@14365
    66
apply (frule_tac [2] real_sup_lemma2)
paulson@14365
    67
apply (frule real_sup_lemma2, assumption+, clarify) 
paulson@14365
    68
apply (rule preal_complete [THEN iffD2, THEN bexE])
paulson@14365
    69
prefer 3 apply blast
paulson@14365
    70
apply (blast intro!: order_less_imp_le)+
paulson@14365
    71
done
paulson@14365
    72
paulson@14365
    73
(*--------------------------------------------------------
paulson@14365
    74
   Completeness properties using isUb, isLub etc.
paulson@14365
    75
 -------------------------------------------------------*)
paulson@14365
    76
paulson@14365
    77
lemma real_isLub_unique: "[| isLub R S x; isLub R S y |] ==> x = (y::real)"
paulson@14365
    78
apply (frule isLub_isUb)
paulson@14365
    79
apply (frule_tac x = y in isLub_isUb)
paulson@14476
    80
apply (blast intro!: order_antisym dest!: isLub_le_isUb)
paulson@14365
    81
done
paulson@14365
    82
paulson@14365
    83
lemma real_order_restrict: "[| (x::real) <=* S'; S <= S' |] ==> x <=* S"
paulson@14365
    84
by (unfold setle_def setge_def, blast)
paulson@14365
    85
paulson@14365
    86
(*----------------------------------------------------------------
paulson@14365
    87
           Completeness theorem for the positive reals(again)
paulson@14365
    88
 ----------------------------------------------------------------*)
paulson@14365
    89
paulson@14365
    90
lemma posreals_complete:
paulson@14365
    91
     "[| \<forall>x \<in>S. 0 < x;  
paulson@14365
    92
         \<exists>x. x \<in>S;  
paulson@14365
    93
         \<exists>u. isUb (UNIV::real set) S u  
paulson@14365
    94
      |] ==> \<exists>t. isLub (UNIV::real set) S t"
paulson@14365
    95
apply (rule_tac x = "real_of_preal (psup ({w. real_of_preal w \<in> S}))" in exI)
paulson@14365
    96
apply (auto simp add: isLub_def leastP_def isUb_def)
paulson@14365
    97
apply (auto intro!: setleI setgeI dest!: real_gt_zero_preal_Ex [THEN iffD1])
paulson@14365
    98
apply (frule_tac x = y in bspec, assumption)
paulson@14365
    99
apply (drule real_gt_zero_preal_Ex [THEN iffD1])
paulson@14365
   100
apply (auto simp add: real_of_preal_le_iff)
paulson@14365
   101
apply (frule_tac y = "real_of_preal ya" in setleD, assumption)
paulson@14365
   102
apply (frule real_ge_preal_preal_Ex, safe)
paulson@14365
   103
apply (blast intro!: preal_psup_le dest!: setleD intro: real_of_preal_le_iff [THEN iffD1])
paulson@14365
   104
apply (frule_tac x = x in bspec, assumption)
paulson@14365
   105
apply (frule isUbD2)
paulson@14365
   106
apply (drule real_gt_zero_preal_Ex [THEN iffD1])
paulson@14365
   107
apply (auto dest!: isUbD real_ge_preal_preal_Ex simp add: real_of_preal_le_iff)
paulson@14365
   108
apply (blast dest!: setleD intro!: psup_le_ub intro: real_of_preal_le_iff [THEN iffD1])
paulson@14365
   109
done
paulson@14365
   110
paulson@5078
   111
paulson@14365
   112
(*-------------------------------
paulson@14365
   113
    Lemmas
paulson@14365
   114
 -------------------------------*)
paulson@14365
   115
lemma real_sup_lemma3: "\<forall>y \<in> {z. \<exists>x \<in> P. z = x + (-xa) + 1} Int {x. 0 < x}. 0 < y"
paulson@14365
   116
by auto
paulson@14365
   117
 
paulson@14365
   118
lemma lemma_le_swap2: "(xa <= S + X + (-Z)) = (xa + (-X) + Z <= (S::real))"
paulson@14365
   119
by auto
paulson@14365
   120
paulson@14365
   121
lemma lemma_real_complete2b: "[| (x::real) + (-X) + 1 <= S; xa <= x |] ==> xa <= S + X + (- 1)"
paulson@14365
   122
by arith
paulson@14365
   123
paulson@14365
   124
(*----------------------------------------------------------
paulson@14365
   125
      reals Completeness (again!)
paulson@14365
   126
 ----------------------------------------------------------*)
paulson@14365
   127
lemma reals_complete: "[| \<exists>X. X \<in>S;  \<exists>Y. isUb (UNIV::real set) S Y |]   
paulson@14365
   128
      ==> \<exists>t. isLub (UNIV :: real set) S t"
paulson@14365
   129
apply safe
paulson@14365
   130
apply (subgoal_tac "\<exists>u. u\<in> {z. \<exists>x \<in>S. z = x + (-X) + 1} Int {x. 0 < x}")
paulson@14365
   131
apply (subgoal_tac "isUb (UNIV::real set) ({z. \<exists>x \<in>S. z = x + (-X) + 1} Int {x. 0 < x}) (Y + (-X) + 1) ")
paulson@14365
   132
apply (cut_tac P = S and xa = X in real_sup_lemma3)
paulson@14387
   133
apply (frule posreals_complete [OF _ _ exI], blast, blast, safe)
paulson@14365
   134
apply (rule_tac x = "t + X + (- 1) " in exI)
paulson@14365
   135
apply (rule isLubI2)
paulson@14365
   136
apply (rule_tac [2] setgeI, safe)
paulson@14365
   137
apply (subgoal_tac [2] "isUb (UNIV:: real set) ({z. \<exists>x \<in>S. z = x + (-X) + 1} Int {x. 0 < x}) (y + (-X) + 1) ")
paulson@14365
   138
apply (drule_tac [2] y = " (y + (- X) + 1) " in isLub_le_isUb)
paulson@14365
   139
 prefer 2 apply assumption
paulson@14365
   140
 prefer 2
paulson@14365
   141
apply arith
paulson@14365
   142
apply (rule setleI [THEN isUbI], safe)
paulson@14365
   143
apply (rule_tac x = x and y = y in linorder_cases)
paulson@14365
   144
apply (subst lemma_le_swap2)
paulson@14365
   145
apply (frule isLubD2)
paulson@14365
   146
 prefer 2 apply assumption
paulson@14365
   147
apply safe
paulson@14365
   148
apply blast
paulson@14365
   149
apply arith
paulson@14365
   150
apply (subst lemma_le_swap2)
paulson@14365
   151
apply (frule isLubD2)
paulson@14365
   152
 prefer 2 apply assumption
paulson@14365
   153
apply blast
paulson@14365
   154
apply (rule lemma_real_complete2b)
paulson@14365
   155
apply (erule_tac [2] order_less_imp_le)
paulson@14365
   156
apply (blast intro!: isLubD2, blast) 
paulson@15234
   157
apply (simp (no_asm_use) add: add_assoc)
paulson@14365
   158
apply (blast dest: isUbD intro!: setleI [THEN isUbI] intro: add_right_mono)
paulson@14365
   159
apply (blast dest: isUbD intro!: setleI [THEN isUbI] intro: add_right_mono, auto)
paulson@14365
   160
done
paulson@14365
   161
paulson@14365
   162
paulson@14365
   163
subsection{*Corollary: the Archimedean Property of the Reals*}
paulson@14365
   164
paulson@14365
   165
lemma reals_Archimedean: "0 < x ==> \<exists>n. inverse (real(Suc n)) < x"
paulson@14365
   166
apply (rule ccontr)
paulson@14365
   167
apply (subgoal_tac "\<forall>n. x * real (Suc n) <= 1")
paulson@14365
   168
 prefer 2
paulson@14365
   169
apply (simp add: linorder_not_less inverse_eq_divide, clarify) 
paulson@14365
   170
apply (drule_tac x = n in spec)
paulson@14365
   171
apply (drule_tac c = "real (Suc n)"  in mult_right_mono)
paulson@14365
   172
apply (rule real_of_nat_ge_zero)
paulson@15234
   173
apply (simp add: times_divide_eq_right real_of_nat_Suc_gt_zero [THEN real_not_refl2, THEN not_sym] mult_commute)
paulson@14365
   174
apply (subgoal_tac "isUb (UNIV::real set) {z. \<exists>n. z = x* (real (Suc n))} 1")
paulson@14365
   175
apply (subgoal_tac "\<exists>X. X \<in> {z. \<exists>n. z = x* (real (Suc n))}")
paulson@14365
   176
apply (drule reals_complete)
paulson@14365
   177
apply (auto intro: isUbI setleI)
paulson@14365
   178
apply (subgoal_tac "\<forall>m. x* (real (Suc m)) <= t")
paulson@14365
   179
apply (simp add: real_of_nat_Suc right_distrib)
paulson@14365
   180
prefer 2 apply (blast intro: isLubD2)
paulson@14365
   181
apply (simp add: le_diff_eq [symmetric] real_diff_def)
paulson@14365
   182
apply (subgoal_tac "isUb (UNIV::real set) {z. \<exists>n. z = x* (real (Suc n))} (t + (-x))")
paulson@14365
   183
prefer 2 apply (blast intro!: isUbI setleI)
paulson@14365
   184
apply (drule_tac y = "t+ (-x) " in isLub_le_isUb)
paulson@14365
   185
apply (auto simp add: real_of_nat_Suc right_distrib)
paulson@14365
   186
done
paulson@14365
   187
paulson@14365
   188
(*There must be other proofs, e.g. Suc of the largest integer in the
paulson@14365
   189
  cut representing x*)
paulson@14365
   190
lemma reals_Archimedean2: "\<exists>n. (x::real) < real (n::nat)"
paulson@14365
   191
apply (rule_tac x = x and y = 0 in linorder_cases)
paulson@14365
   192
apply (rule_tac x = 0 in exI)
paulson@14365
   193
apply (rule_tac [2] x = 1 in exI)
paulson@14365
   194
apply (auto elim: order_less_trans simp add: real_of_nat_one)
paulson@14365
   195
apply (frule positive_imp_inverse_positive [THEN reals_Archimedean], safe)
paulson@14365
   196
apply (rule_tac x = "Suc n" in exI)
paulson@14365
   197
apply (frule_tac b = "inverse x" in mult_strict_right_mono, auto)
paulson@14365
   198
done
paulson@14365
   199
paulson@14365
   200
lemma reals_Archimedean3: "0 < x ==> \<forall>y. \<exists>(n::nat). y < real n * x"
paulson@14365
   201
apply safe
paulson@14365
   202
apply (cut_tac x = "y*inverse (x) " in reals_Archimedean2)
paulson@14365
   203
apply safe
paulson@14365
   204
apply (frule_tac a = "y * inverse x" in mult_strict_right_mono)
paulson@14365
   205
apply (auto simp add: mult_assoc real_of_nat_def)
paulson@14365
   206
done
paulson@14365
   207
avigad@16819
   208
lemma reals_Archimedean6:
avigad@16819
   209
     "0 \<le> r ==> \<exists>(n::nat). real (n - 1) \<le> r & r < real (n)"
avigad@16819
   210
apply (insert reals_Archimedean2 [of r], safe)
avigad@16819
   211
apply (frule_tac P = "%k. r < real k" and k = n and m = "%x. x"
avigad@16819
   212
       in ex_has_least_nat, auto)
avigad@16819
   213
apply (rule_tac x = x in exI)
avigad@16819
   214
apply (case_tac x, simp)
avigad@16819
   215
apply (rename_tac x')
avigad@16819
   216
apply (drule_tac x = x' in spec, simp)
avigad@16819
   217
done
avigad@16819
   218
avigad@16819
   219
lemma reals_Archimedean6a: "0 \<le> r ==> \<exists>n. real (n) \<le> r & r < real (Suc n)"
avigad@16819
   220
by (drule reals_Archimedean6, auto)
avigad@16819
   221
avigad@16819
   222
lemma reals_Archimedean_6b_int:
avigad@16819
   223
     "0 \<le> r ==> \<exists>n::int. real n \<le> r & r < real (n+1)"
avigad@16819
   224
apply (drule reals_Archimedean6a, auto)
avigad@16819
   225
apply (rule_tac x = "int n" in exI)
avigad@16819
   226
apply (simp add: real_of_int_real_of_nat real_of_nat_Suc)
avigad@16819
   227
done
avigad@16819
   228
avigad@16819
   229
lemma reals_Archimedean_6c_int:
avigad@16819
   230
     "r < 0 ==> \<exists>n::int. real n \<le> r & r < real (n+1)"
avigad@16819
   231
apply (rule reals_Archimedean_6b_int [of "-r", THEN exE], simp, auto)
avigad@16819
   232
apply (rename_tac n)
avigad@16819
   233
apply (drule real_le_imp_less_or_eq, auto)
avigad@16819
   234
apply (rule_tac x = "- n - 1" in exI)
avigad@16819
   235
apply (rule_tac [2] x = "- n" in exI, auto)
avigad@16819
   236
done
avigad@16819
   237
avigad@16819
   238
paulson@14365
   239
ML
paulson@14365
   240
{*
paulson@14365
   241
val real_sum_of_halves = thm "real_sum_of_halves";
paulson@14365
   242
val posreal_complete = thm "posreal_complete";
paulson@14365
   243
val real_isLub_unique = thm "real_isLub_unique";
paulson@14365
   244
val real_order_restrict = thm "real_order_restrict";
paulson@14365
   245
val posreals_complete = thm "posreals_complete";
paulson@14365
   246
val reals_complete = thm "reals_complete";
paulson@14365
   247
val reals_Archimedean = thm "reals_Archimedean";
paulson@14365
   248
val reals_Archimedean2 = thm "reals_Archimedean2";
paulson@14365
   249
val reals_Archimedean3 = thm "reals_Archimedean3";
paulson@14365
   250
*}
paulson@14365
   251
paulson@14641
   252
paulson@14641
   253
subsection{*Floor and Ceiling Functions from the Reals to the Integers*}
paulson@14641
   254
paulson@14641
   255
constdefs
paulson@14641
   256
paulson@14641
   257
  floor :: "real => int"
paulson@14641
   258
   "floor r == (LEAST n::int. r < real (n+1))"
paulson@14641
   259
paulson@14641
   260
  ceiling :: "real => int"
paulson@14641
   261
    "ceiling r == - floor (- r)"
paulson@14641
   262
paulson@14641
   263
syntax (xsymbols)
paulson@14641
   264
  floor :: "real => int"     ("\<lfloor>_\<rfloor>")
paulson@14641
   265
  ceiling :: "real => int"   ("\<lceil>_\<rceil>")
paulson@14641
   266
paulson@14641
   267
syntax (HTML output)
paulson@14641
   268
  floor :: "real => int"     ("\<lfloor>_\<rfloor>")
paulson@14641
   269
  ceiling :: "real => int"   ("\<lceil>_\<rceil>")
paulson@14641
   270
paulson@14641
   271
paulson@14641
   272
lemma number_of_less_real_of_int_iff [simp]:
paulson@14641
   273
     "((number_of n) < real (m::int)) = (number_of n < m)"
paulson@14641
   274
apply auto
paulson@14641
   275
apply (rule real_of_int_less_iff [THEN iffD1])
paulson@14641
   276
apply (drule_tac [2] real_of_int_less_iff [THEN iffD2], auto)
paulson@14641
   277
done
paulson@14641
   278
paulson@14641
   279
lemma number_of_less_real_of_int_iff2 [simp]:
paulson@14641
   280
     "(real (m::int) < (number_of n)) = (m < number_of n)"
paulson@14641
   281
apply auto
paulson@14641
   282
apply (rule real_of_int_less_iff [THEN iffD1])
paulson@14641
   283
apply (drule_tac [2] real_of_int_less_iff [THEN iffD2], auto)
paulson@14641
   284
done
paulson@14641
   285
paulson@14641
   286
lemma number_of_le_real_of_int_iff [simp]:
paulson@14641
   287
     "((number_of n) \<le> real (m::int)) = (number_of n \<le> m)"
paulson@14641
   288
by (simp add: linorder_not_less [symmetric])
paulson@14641
   289
paulson@14641
   290
lemma number_of_le_real_of_int_iff2 [simp]:
paulson@14641
   291
     "(real (m::int) \<le> (number_of n)) = (m \<le> number_of n)"
paulson@14641
   292
by (simp add: linorder_not_less [symmetric])
paulson@14641
   293
paulson@14641
   294
lemma floor_zero [simp]: "floor 0 = 0"
avigad@16819
   295
apply (simp add: floor_def del: real_of_int_add)
avigad@16819
   296
apply (rule Least_equality)
avigad@16819
   297
apply simp_all
paulson@14641
   298
done
paulson@14641
   299
paulson@14641
   300
lemma floor_real_of_nat_zero [simp]: "floor (real (0::nat)) = 0"
paulson@14641
   301
by auto
paulson@14641
   302
paulson@14641
   303
lemma floor_real_of_nat [simp]: "floor (real (n::nat)) = int n"
paulson@14641
   304
apply (simp only: floor_def)
paulson@14641
   305
apply (rule Least_equality)
paulson@14641
   306
apply (drule_tac [2] real_of_int_real_of_nat [THEN ssubst])
paulson@14641
   307
apply (drule_tac [2] real_of_int_less_iff [THEN iffD1])
paulson@14641
   308
apply (simp_all add: real_of_int_real_of_nat)
paulson@14641
   309
done
paulson@14641
   310
paulson@14641
   311
lemma floor_minus_real_of_nat [simp]: "floor (- real (n::nat)) = - int n"
paulson@14641
   312
apply (simp only: floor_def)
paulson@14641
   313
apply (rule Least_equality)
paulson@14641
   314
apply (drule_tac [2] real_of_int_real_of_nat [THEN ssubst])
avigad@16819
   315
apply (drule_tac [2] real_of_int_minus [THEN sym, THEN subst])
paulson@14641
   316
apply (drule_tac [2] real_of_int_less_iff [THEN iffD1])
paulson@14641
   317
apply (simp_all add: real_of_int_real_of_nat)
paulson@14641
   318
done
paulson@14641
   319
paulson@14641
   320
lemma floor_real_of_int [simp]: "floor (real (n::int)) = n"
paulson@14641
   321
apply (simp only: floor_def)
paulson@14641
   322
apply (rule Least_equality)
paulson@14641
   323
apply (drule_tac [2] real_of_int_real_of_nat [THEN ssubst])
paulson@14641
   324
apply (drule_tac [2] real_of_int_less_iff [THEN iffD1], auto)
paulson@14641
   325
done
paulson@14641
   326
paulson@14641
   327
lemma floor_minus_real_of_int [simp]: "floor (- real (n::int)) = - n"
paulson@14641
   328
apply (simp only: floor_def)
paulson@14641
   329
apply (rule Least_equality)
avigad@16819
   330
apply (drule_tac [2] real_of_int_minus [THEN sym, THEN subst])
paulson@14641
   331
apply (drule_tac [2] real_of_int_real_of_nat [THEN ssubst])
paulson@14641
   332
apply (drule_tac [2] real_of_int_less_iff [THEN iffD1], auto)
paulson@14641
   333
done
paulson@14641
   334
paulson@14641
   335
lemma real_lb_ub_int: " \<exists>n::int. real n \<le> r & r < real (n+1)"
paulson@14641
   336
apply (case_tac "r < 0")
paulson@14641
   337
apply (blast intro: reals_Archimedean_6c_int)
paulson@14641
   338
apply (simp only: linorder_not_less)
paulson@14641
   339
apply (blast intro: reals_Archimedean_6b_int reals_Archimedean_6c_int)
paulson@14641
   340
done
paulson@14641
   341
paulson@14641
   342
lemma lemma_floor:
paulson@14641
   343
  assumes a1: "real m \<le> r" and a2: "r < real n + 1"
paulson@14641
   344
  shows "m \<le> (n::int)"
paulson@14641
   345
proof -
paulson@14641
   346
  have "real m < real n + 1" by (rule order_le_less_trans)
paulson@14641
   347
  also have "... = real(n+1)" by simp
paulson@14641
   348
  finally have "m < n+1" by (simp only: real_of_int_less_iff)
paulson@14641
   349
  thus ?thesis by arith
paulson@14641
   350
qed
paulson@14641
   351
paulson@14641
   352
lemma real_of_int_floor_le [simp]: "real (floor r) \<le> r"
paulson@14641
   353
apply (simp add: floor_def Least_def)
paulson@14641
   354
apply (insert real_lb_ub_int [of r], safe)
avigad@16819
   355
apply (rule theI2)
avigad@16819
   356
apply auto
avigad@16819
   357
apply (subst int_le_real_less, simp)
avigad@16819
   358
apply (drule_tac x = n in spec)
avigad@16819
   359
apply auto
avigad@16819
   360
apply (subgoal_tac "n <= x")
avigad@16819
   361
apply simp
avigad@16819
   362
apply (subst int_le_real_less, simp)
paulson@14641
   363
done
paulson@14641
   364
avigad@16819
   365
lemma floor_mono: "x < y ==> floor x \<le> floor y"
paulson@14641
   366
apply (simp add: floor_def Least_def)
paulson@14641
   367
apply (insert real_lb_ub_int [of x])
paulson@14641
   368
apply (insert real_lb_ub_int [of y], safe)
paulson@14641
   369
apply (rule theI2)
avigad@16819
   370
apply (rule_tac [3] theI2)
avigad@16819
   371
apply simp
avigad@16819
   372
apply (erule conjI)
avigad@16819
   373
apply (auto simp add: order_eq_iff int_le_real_less)
paulson@14641
   374
done
paulson@14641
   375
avigad@16819
   376
lemma floor_mono2: "x \<le> y ==> floor x \<le> floor y"
avigad@16819
   377
by (auto dest: real_le_imp_less_or_eq simp add: floor_mono)
paulson@14641
   378
paulson@14641
   379
lemma lemma_floor2: "real n < real (x::int) + 1 ==> n \<le> x"
paulson@14641
   380
by (auto intro: lemma_floor)
paulson@14641
   381
paulson@14641
   382
lemma real_of_int_floor_cancel [simp]:
paulson@14641
   383
    "(real (floor x) = x) = (\<exists>n::int. x = real n)"
paulson@14641
   384
apply (simp add: floor_def Least_def)
paulson@14641
   385
apply (insert real_lb_ub_int [of x], erule exE)
paulson@14641
   386
apply (rule theI2)
avigad@16819
   387
apply (auto intro: lemma_floor) 
avigad@16819
   388
apply (auto simp add: order_eq_iff int_le_real_less)
paulson@14641
   389
done
paulson@14641
   390
paulson@14641
   391
lemma floor_eq: "[| real n < x; x < real n + 1 |] ==> floor x = n"
paulson@14641
   392
apply (simp add: floor_def)
paulson@14641
   393
apply (rule Least_equality)
paulson@14641
   394
apply (auto intro: lemma_floor)
paulson@14641
   395
done
paulson@14641
   396
paulson@14641
   397
lemma floor_eq2: "[| real n \<le> x; x < real n + 1 |] ==> floor x = n"
paulson@14641
   398
apply (simp add: floor_def)
paulson@14641
   399
apply (rule Least_equality)
paulson@14641
   400
apply (auto intro: lemma_floor)
paulson@14641
   401
done
paulson@14641
   402
paulson@14641
   403
lemma floor_eq3: "[| real n < x; x < real (Suc n) |] ==> nat(floor x) = n"
paulson@14641
   404
apply (rule inj_int [THEN injD])
paulson@14641
   405
apply (simp add: real_of_nat_Suc)
nipkow@15539
   406
apply (simp add: real_of_nat_Suc floor_eq floor_eq [where n = "int n"])
paulson@14641
   407
done
paulson@14641
   408
paulson@14641
   409
lemma floor_eq4: "[| real n \<le> x; x < real (Suc n) |] ==> nat(floor x) = n"
paulson@14641
   410
apply (drule order_le_imp_less_or_eq)
paulson@14641
   411
apply (auto intro: floor_eq3)
paulson@14641
   412
done
paulson@14641
   413
paulson@14641
   414
lemma floor_number_of_eq [simp]:
paulson@14641
   415
     "floor(number_of n :: real) = (number_of n :: int)"
paulson@14641
   416
apply (subst real_number_of [symmetric])
paulson@14641
   417
apply (rule floor_real_of_int)
paulson@14641
   418
done
paulson@14641
   419
avigad@16819
   420
lemma floor_one [simp]: "floor 1 = 1"
avigad@16819
   421
  apply (rule trans)
avigad@16819
   422
  prefer 2
avigad@16819
   423
  apply (rule floor_real_of_int)
avigad@16819
   424
  apply simp
avigad@16819
   425
done
avigad@16819
   426
paulson@14641
   427
lemma real_of_int_floor_ge_diff_one [simp]: "r - 1 \<le> real(floor r)"
paulson@14641
   428
apply (simp add: floor_def Least_def)
paulson@14641
   429
apply (insert real_lb_ub_int [of r], safe)
paulson@14641
   430
apply (rule theI2)
paulson@14641
   431
apply (auto intro: lemma_floor)
avigad@16819
   432
apply (auto simp add: order_eq_iff int_le_real_less)
avigad@16819
   433
done
avigad@16819
   434
avigad@16819
   435
lemma real_of_int_floor_gt_diff_one [simp]: "r - 1 < real(floor r)"
avigad@16819
   436
apply (simp add: floor_def Least_def)
avigad@16819
   437
apply (insert real_lb_ub_int [of r], safe)
avigad@16819
   438
apply (rule theI2)
avigad@16819
   439
apply (auto intro: lemma_floor)
avigad@16819
   440
apply (auto simp add: order_eq_iff int_le_real_less)
paulson@14641
   441
done
paulson@14641
   442
paulson@14641
   443
lemma real_of_int_floor_add_one_ge [simp]: "r \<le> real(floor r) + 1"
paulson@14641
   444
apply (insert real_of_int_floor_ge_diff_one [of r])
paulson@14641
   445
apply (auto simp del: real_of_int_floor_ge_diff_one)
paulson@14641
   446
done
paulson@14641
   447
avigad@16819
   448
lemma real_of_int_floor_add_one_gt [simp]: "r < real(floor r) + 1"
avigad@16819
   449
apply (insert real_of_int_floor_gt_diff_one [of r])
avigad@16819
   450
apply (auto simp del: real_of_int_floor_gt_diff_one)
avigad@16819
   451
done
paulson@14641
   452
avigad@16819
   453
lemma le_floor: "real a <= x ==> a <= floor x"
avigad@16819
   454
  apply (subgoal_tac "a < floor x + 1")
avigad@16819
   455
  apply arith
avigad@16819
   456
  apply (subst real_of_int_less_iff [THEN sym])
avigad@16819
   457
  apply simp
avigad@16819
   458
  apply (insert real_of_int_floor_add_one_gt [of x]) 
avigad@16819
   459
  apply arith
avigad@16819
   460
done
avigad@16819
   461
avigad@16819
   462
lemma real_le_floor: "a <= floor x ==> real a <= x"
avigad@16819
   463
  apply (rule order_trans)
avigad@16819
   464
  prefer 2
avigad@16819
   465
  apply (rule real_of_int_floor_le)
avigad@16819
   466
  apply (subst real_of_int_le_iff)
avigad@16819
   467
  apply assumption
avigad@16819
   468
done
avigad@16819
   469
avigad@16819
   470
lemma le_floor_eq: "(a <= floor x) = (real a <= x)"
avigad@16819
   471
  apply (rule iffI)
avigad@16819
   472
  apply (erule real_le_floor)
avigad@16819
   473
  apply (erule le_floor)
avigad@16819
   474
done
avigad@16819
   475
avigad@16819
   476
lemma le_floor_eq_number_of [simp]: 
avigad@16819
   477
    "(number_of n <= floor x) = (number_of n <= x)"
avigad@16819
   478
by (simp add: le_floor_eq)
avigad@16819
   479
avigad@16819
   480
lemma le_floor_eq_zero [simp]: "(0 <= floor x) = (0 <= x)"
avigad@16819
   481
by (simp add: le_floor_eq)
avigad@16819
   482
avigad@16819
   483
lemma le_floor_eq_one [simp]: "(1 <= floor x) = (1 <= x)"
avigad@16819
   484
by (simp add: le_floor_eq)
avigad@16819
   485
avigad@16819
   486
lemma floor_less_eq: "(floor x < a) = (x < real a)"
avigad@16819
   487
  apply (subst linorder_not_le [THEN sym])+
avigad@16819
   488
  apply simp
avigad@16819
   489
  apply (rule le_floor_eq)
avigad@16819
   490
done
avigad@16819
   491
avigad@16819
   492
lemma floor_less_eq_number_of [simp]: 
avigad@16819
   493
    "(floor x < number_of n) = (x < number_of n)"
avigad@16819
   494
by (simp add: floor_less_eq)
avigad@16819
   495
avigad@16819
   496
lemma floor_less_eq_zero [simp]: "(floor x < 0) = (x < 0)"
avigad@16819
   497
by (simp add: floor_less_eq)
avigad@16819
   498
avigad@16819
   499
lemma floor_less_eq_one [simp]: "(floor x < 1) = (x < 1)"
avigad@16819
   500
by (simp add: floor_less_eq)
avigad@16819
   501
avigad@16819
   502
lemma less_floor_eq: "(a < floor x) = (real a + 1 <= x)"
avigad@16819
   503
  apply (insert le_floor_eq [of "a + 1" x])
avigad@16819
   504
  apply auto
avigad@16819
   505
done
avigad@16819
   506
avigad@16819
   507
lemma less_floor_eq_number_of [simp]: 
avigad@16819
   508
    "(number_of n < floor x) = (number_of n + 1 <= x)"
avigad@16819
   509
by (simp add: less_floor_eq)
avigad@16819
   510
avigad@16819
   511
lemma less_floor_eq_zero [simp]: "(0 < floor x) = (1 <= x)"
avigad@16819
   512
by (simp add: less_floor_eq)
avigad@16819
   513
avigad@16819
   514
lemma less_floor_eq_one [simp]: "(1 < floor x) = (2 <= x)"
avigad@16819
   515
by (simp add: less_floor_eq)
avigad@16819
   516
avigad@16819
   517
lemma floor_le_eq: "(floor x <= a) = (x < real a + 1)"
avigad@16819
   518
  apply (insert floor_less_eq [of x "a + 1"])
avigad@16819
   519
  apply auto
avigad@16819
   520
done
avigad@16819
   521
avigad@16819
   522
lemma floor_le_eq_number_of [simp]: 
avigad@16819
   523
    "(floor x <= number_of n) = (x < number_of n + 1)"
avigad@16819
   524
by (simp add: floor_le_eq)
avigad@16819
   525
avigad@16819
   526
lemma floor_le_eq_zero [simp]: "(floor x <= 0) = (x < 1)"
avigad@16819
   527
by (simp add: floor_le_eq)
avigad@16819
   528
avigad@16819
   529
lemma floor_le_eq_one [simp]: "(floor x <= 1) = (x < 2)"
avigad@16819
   530
by (simp add: floor_le_eq)
avigad@16819
   531
avigad@16819
   532
lemma floor_add [simp]: "floor (x + real a) = floor x + a"
avigad@16819
   533
  apply (subst order_eq_iff)
avigad@16819
   534
  apply (rule conjI)
avigad@16819
   535
  prefer 2
avigad@16819
   536
  apply (subgoal_tac "floor x + a < floor (x + real a) + 1")
avigad@16819
   537
  apply arith
avigad@16819
   538
  apply (subst real_of_int_less_iff [THEN sym])
avigad@16819
   539
  apply simp
avigad@16819
   540
  apply (subgoal_tac "x + real a < real(floor(x + real a)) + 1")
avigad@16819
   541
  apply (subgoal_tac "real (floor x) <= x")
avigad@16819
   542
  apply arith
avigad@16819
   543
  apply (rule real_of_int_floor_le)
avigad@16819
   544
  apply (rule real_of_int_floor_add_one_gt)
avigad@16819
   545
  apply (subgoal_tac "floor (x + real a) < floor x + a + 1")
avigad@16819
   546
  apply arith
avigad@16819
   547
  apply (subst real_of_int_less_iff [THEN sym])  
avigad@16819
   548
  apply simp
avigad@16819
   549
  apply (subgoal_tac "real(floor(x + real a)) <= x + real a") 
avigad@16819
   550
  apply (subgoal_tac "x < real(floor x) + 1")
avigad@16819
   551
  apply arith
avigad@16819
   552
  apply (rule real_of_int_floor_add_one_gt)
avigad@16819
   553
  apply (rule real_of_int_floor_le)
avigad@16819
   554
done
avigad@16819
   555
avigad@16819
   556
lemma floor_add_number_of [simp]: 
avigad@16819
   557
    "floor (x + number_of n) = floor x + number_of n"
avigad@16819
   558
  apply (subst floor_add [THEN sym])
avigad@16819
   559
  apply simp
avigad@16819
   560
done
avigad@16819
   561
avigad@16819
   562
lemma floor_add_one [simp]: "floor (x + 1) = floor x + 1"
avigad@16819
   563
  apply (subst floor_add [THEN sym])
avigad@16819
   564
  apply simp
avigad@16819
   565
done
avigad@16819
   566
avigad@16819
   567
lemma floor_subtract [simp]: "floor (x - real a) = floor x - a"
avigad@16819
   568
  apply (subst diff_minus)+
avigad@16819
   569
  apply (subst real_of_int_minus [THEN sym])
avigad@16819
   570
  apply (rule floor_add)
avigad@16819
   571
done
avigad@16819
   572
avigad@16819
   573
lemma floor_subtract_number_of [simp]: "floor (x - number_of n) = 
avigad@16819
   574
    floor x - number_of n"
avigad@16819
   575
  apply (subst floor_subtract [THEN sym])
avigad@16819
   576
  apply simp
avigad@16819
   577
done
avigad@16819
   578
avigad@16819
   579
lemma floor_subtract_one [simp]: "floor (x - 1) = floor x - 1"
avigad@16819
   580
  apply (subst floor_subtract [THEN sym])
avigad@16819
   581
  apply simp
avigad@16819
   582
done
paulson@14641
   583
paulson@14641
   584
lemma ceiling_zero [simp]: "ceiling 0 = 0"
paulson@14641
   585
by (simp add: ceiling_def)
paulson@14641
   586
paulson@14641
   587
lemma ceiling_real_of_nat [simp]: "ceiling (real (n::nat)) = int n"
paulson@14641
   588
by (simp add: ceiling_def)
paulson@14641
   589
paulson@14641
   590
lemma ceiling_real_of_nat_zero [simp]: "ceiling (real (0::nat)) = 0"
paulson@14641
   591
by auto
paulson@14641
   592
paulson@14641
   593
lemma ceiling_floor [simp]: "ceiling (real (floor r)) = floor r"
paulson@14641
   594
by (simp add: ceiling_def)
paulson@14641
   595
paulson@14641
   596
lemma floor_ceiling [simp]: "floor (real (ceiling r)) = ceiling r"
paulson@14641
   597
by (simp add: ceiling_def)
paulson@14641
   598
paulson@14641
   599
lemma real_of_int_ceiling_ge [simp]: "r \<le> real (ceiling r)"
paulson@14641
   600
apply (simp add: ceiling_def)
paulson@14641
   601
apply (subst le_minus_iff, simp)
paulson@14641
   602
done
paulson@14641
   603
avigad@16819
   604
lemma ceiling_mono: "x < y ==> ceiling x \<le> ceiling y"
avigad@16819
   605
by (simp add: floor_mono ceiling_def)
paulson@14641
   606
avigad@16819
   607
lemma ceiling_mono2: "x \<le> y ==> ceiling x \<le> ceiling y"
avigad@16819
   608
by (simp add: floor_mono2 ceiling_def)
paulson@14641
   609
paulson@14641
   610
lemma real_of_int_ceiling_cancel [simp]:
paulson@14641
   611
     "(real (ceiling x) = x) = (\<exists>n::int. x = real n)"
paulson@14641
   612
apply (auto simp add: ceiling_def)
paulson@14641
   613
apply (drule arg_cong [where f = uminus], auto)
paulson@14641
   614
apply (rule_tac x = "-n" in exI, auto)
paulson@14641
   615
done
paulson@14641
   616
paulson@14641
   617
lemma ceiling_eq: "[| real n < x; x < real n + 1 |] ==> ceiling x = n + 1"
paulson@14641
   618
apply (simp add: ceiling_def)
paulson@14641
   619
apply (rule minus_equation_iff [THEN iffD1])
paulson@14641
   620
apply (simp add: floor_eq [where n = "-(n+1)"])
paulson@14641
   621
done
paulson@14641
   622
paulson@14641
   623
lemma ceiling_eq2: "[| real n < x; x \<le> real n + 1 |] ==> ceiling x = n + 1"
paulson@14641
   624
by (simp add: ceiling_def floor_eq2 [where n = "-(n+1)"])
paulson@14641
   625
paulson@14641
   626
lemma ceiling_eq3: "[| real n - 1 < x; x \<le> real n  |] ==> ceiling x = n"
paulson@14641
   627
by (simp add: ceiling_def floor_eq2 [where n = "-n"])
paulson@14641
   628
paulson@14641
   629
lemma ceiling_real_of_int [simp]: "ceiling (real (n::int)) = n"
paulson@14641
   630
by (simp add: ceiling_def)
paulson@14641
   631
paulson@14641
   632
lemma ceiling_number_of_eq [simp]:
paulson@14641
   633
     "ceiling (number_of n :: real) = (number_of n)"
paulson@14641
   634
apply (subst real_number_of [symmetric])
paulson@14641
   635
apply (rule ceiling_real_of_int)
paulson@14641
   636
done
paulson@14641
   637
avigad@16819
   638
lemma ceiling_one [simp]: "ceiling 1 = 1"
avigad@16819
   639
  by (unfold ceiling_def, simp)
avigad@16819
   640
paulson@14641
   641
lemma real_of_int_ceiling_diff_one_le [simp]: "real (ceiling r) - 1 \<le> r"
paulson@14641
   642
apply (rule neg_le_iff_le [THEN iffD1])
paulson@14641
   643
apply (simp add: ceiling_def diff_minus)
paulson@14641
   644
done
paulson@14641
   645
paulson@14641
   646
lemma real_of_int_ceiling_le_add_one [simp]: "real (ceiling r) \<le> r + 1"
paulson@14641
   647
apply (insert real_of_int_ceiling_diff_one_le [of r])
paulson@14641
   648
apply (simp del: real_of_int_ceiling_diff_one_le)
paulson@14641
   649
done
paulson@14641
   650
avigad@16819
   651
lemma ceiling_le: "x <= real a ==> ceiling x <= a"
avigad@16819
   652
  apply (unfold ceiling_def)
avigad@16819
   653
  apply (subgoal_tac "-a <= floor(- x)")
avigad@16819
   654
  apply simp
avigad@16819
   655
  apply (rule le_floor)
avigad@16819
   656
  apply simp
avigad@16819
   657
done
avigad@16819
   658
avigad@16819
   659
lemma ceiling_le_real: "ceiling x <= a ==> x <= real a"
avigad@16819
   660
  apply (unfold ceiling_def)
avigad@16819
   661
  apply (subgoal_tac "real(- a) <= - x")
avigad@16819
   662
  apply simp
avigad@16819
   663
  apply (rule real_le_floor)
avigad@16819
   664
  apply simp
avigad@16819
   665
done
avigad@16819
   666
avigad@16819
   667
lemma ceiling_le_eq: "(ceiling x <= a) = (x <= real a)"
avigad@16819
   668
  apply (rule iffI)
avigad@16819
   669
  apply (erule ceiling_le_real)
avigad@16819
   670
  apply (erule ceiling_le)
avigad@16819
   671
done
avigad@16819
   672
avigad@16819
   673
lemma ceiling_le_eq_number_of [simp]: 
avigad@16819
   674
    "(ceiling x <= number_of n) = (x <= number_of n)"
avigad@16819
   675
by (simp add: ceiling_le_eq)
avigad@16819
   676
avigad@16819
   677
lemma ceiling_le_zero_eq [simp]: "(ceiling x <= 0) = (x <= 0)" 
avigad@16819
   678
by (simp add: ceiling_le_eq)
avigad@16819
   679
avigad@16819
   680
lemma ceiling_le_eq_one [simp]: "(ceiling x <= 1) = (x <= 1)" 
avigad@16819
   681
by (simp add: ceiling_le_eq)
avigad@16819
   682
avigad@16819
   683
lemma less_ceiling_eq: "(a < ceiling x) = (real a < x)"
avigad@16819
   684
  apply (subst linorder_not_le [THEN sym])+
avigad@16819
   685
  apply simp
avigad@16819
   686
  apply (rule ceiling_le_eq)
avigad@16819
   687
done
avigad@16819
   688
avigad@16819
   689
lemma less_ceiling_eq_number_of [simp]: 
avigad@16819
   690
    "(number_of n < ceiling x) = (number_of n < x)"
avigad@16819
   691
by (simp add: less_ceiling_eq)
avigad@16819
   692
avigad@16819
   693
lemma less_ceiling_eq_zero [simp]: "(0 < ceiling x) = (0 < x)"
avigad@16819
   694
by (simp add: less_ceiling_eq)
avigad@16819
   695
avigad@16819
   696
lemma less_ceiling_eq_one [simp]: "(1 < ceiling x) = (1 < x)"
avigad@16819
   697
by (simp add: less_ceiling_eq)
avigad@16819
   698
avigad@16819
   699
lemma ceiling_less_eq: "(ceiling x < a) = (x <= real a - 1)"
avigad@16819
   700
  apply (insert ceiling_le_eq [of x "a - 1"])
avigad@16819
   701
  apply auto
avigad@16819
   702
done
avigad@16819
   703
avigad@16819
   704
lemma ceiling_less_eq_number_of [simp]: 
avigad@16819
   705
    "(ceiling x < number_of n) = (x <= number_of n - 1)"
avigad@16819
   706
by (simp add: ceiling_less_eq)
avigad@16819
   707
avigad@16819
   708
lemma ceiling_less_eq_zero [simp]: "(ceiling x < 0) = (x <= -1)"
avigad@16819
   709
by (simp add: ceiling_less_eq)
avigad@16819
   710
avigad@16819
   711
lemma ceiling_less_eq_one [simp]: "(ceiling x < 1) = (x <= 0)"
avigad@16819
   712
by (simp add: ceiling_less_eq)
avigad@16819
   713
avigad@16819
   714
lemma le_ceiling_eq: "(a <= ceiling x) = (real a - 1 < x)"
avigad@16819
   715
  apply (insert less_ceiling_eq [of "a - 1" x])
avigad@16819
   716
  apply auto
avigad@16819
   717
done
avigad@16819
   718
avigad@16819
   719
lemma le_ceiling_eq_number_of [simp]: 
avigad@16819
   720
    "(number_of n <= ceiling x) = (number_of n - 1 < x)"
avigad@16819
   721
by (simp add: le_ceiling_eq)
avigad@16819
   722
avigad@16819
   723
lemma le_ceiling_eq_zero [simp]: "(0 <= ceiling x) = (-1 < x)"
avigad@16819
   724
by (simp add: le_ceiling_eq)
avigad@16819
   725
avigad@16819
   726
lemma le_ceiling_eq_one [simp]: "(1 <= ceiling x) = (0 < x)"
avigad@16819
   727
by (simp add: le_ceiling_eq)
avigad@16819
   728
avigad@16819
   729
lemma ceiling_add [simp]: "ceiling (x + real a) = ceiling x + a"
avigad@16819
   730
  apply (unfold ceiling_def, simp)
avigad@16819
   731
  apply (subst real_of_int_minus [THEN sym])
avigad@16819
   732
  apply (subst floor_add)
avigad@16819
   733
  apply simp
avigad@16819
   734
done
avigad@16819
   735
avigad@16819
   736
lemma ceiling_add_number_of [simp]: "ceiling (x + number_of n) = 
avigad@16819
   737
    ceiling x + number_of n"
avigad@16819
   738
  apply (subst ceiling_add [THEN sym])
avigad@16819
   739
  apply simp
avigad@16819
   740
done
avigad@16819
   741
avigad@16819
   742
lemma ceiling_add_one [simp]: "ceiling (x + 1) = ceiling x + 1"
avigad@16819
   743
  apply (subst ceiling_add [THEN sym])
avigad@16819
   744
  apply simp
avigad@16819
   745
done
avigad@16819
   746
avigad@16819
   747
lemma ceiling_subtract [simp]: "ceiling (x - real a) = ceiling x - a"
avigad@16819
   748
  apply (subst diff_minus)+
avigad@16819
   749
  apply (subst real_of_int_minus [THEN sym])
avigad@16819
   750
  apply (rule ceiling_add)
avigad@16819
   751
done
avigad@16819
   752
avigad@16819
   753
lemma ceiling_subtract_number_of [simp]: "ceiling (x - number_of n) = 
avigad@16819
   754
    ceiling x - number_of n"
avigad@16819
   755
  apply (subst ceiling_subtract [THEN sym])
avigad@16819
   756
  apply simp
avigad@16819
   757
done
avigad@16819
   758
avigad@16819
   759
lemma ceiling_subtract_one [simp]: "ceiling (x - 1) = ceiling x - 1"
avigad@16819
   760
  apply (subst ceiling_subtract [THEN sym])
avigad@16819
   761
  apply simp
avigad@16819
   762
done
avigad@16819
   763
avigad@16819
   764
subsection {* Versions for the natural numbers *}
avigad@16819
   765
avigad@16819
   766
constdefs
avigad@16819
   767
  natfloor :: "real => nat"
avigad@16819
   768
  "natfloor x == nat(floor x)"
avigad@16819
   769
  natceiling :: "real => nat"
avigad@16819
   770
  "natceiling x == nat(ceiling x)"
avigad@16819
   771
avigad@16819
   772
lemma natfloor_zero [simp]: "natfloor 0 = 0"
avigad@16819
   773
  by (unfold natfloor_def, simp)
avigad@16819
   774
avigad@16819
   775
lemma natfloor_one [simp]: "natfloor 1 = 1"
avigad@16819
   776
  by (unfold natfloor_def, simp)
avigad@16819
   777
avigad@16819
   778
lemma zero_le_natfloor [simp]: "0 <= natfloor x"
avigad@16819
   779
  by (unfold natfloor_def, simp)
avigad@16819
   780
avigad@16819
   781
lemma natfloor_number_of_eq [simp]: "natfloor (number_of n) = number_of n"
avigad@16819
   782
  by (unfold natfloor_def, simp)
avigad@16819
   783
avigad@16819
   784
lemma natfloor_real_of_nat [simp]: "natfloor(real n) = n"
avigad@16819
   785
  by (unfold natfloor_def, simp)
avigad@16819
   786
avigad@16819
   787
lemma real_natfloor_le: "0 <= x ==> real(natfloor x) <= x"
avigad@16819
   788
  by (unfold natfloor_def, simp)
avigad@16819
   789
avigad@16819
   790
lemma natfloor_neg: "x <= 0 ==> natfloor x = 0"
avigad@16819
   791
  apply (unfold natfloor_def)
avigad@16819
   792
  apply (subgoal_tac "floor x <= floor 0")
avigad@16819
   793
  apply simp
avigad@16819
   794
  apply (erule floor_mono2)
avigad@16819
   795
done
avigad@16819
   796
avigad@16819
   797
lemma natfloor_mono: "x <= y ==> natfloor x <= natfloor y"
avigad@16819
   798
  apply (case_tac "0 <= x")
avigad@16819
   799
  apply (subst natfloor_def)+
avigad@16819
   800
  apply (subst nat_le_eq_zle)
avigad@16819
   801
  apply force
avigad@16819
   802
  apply (erule floor_mono2) 
avigad@16819
   803
  apply (subst natfloor_neg)
avigad@16819
   804
  apply simp
avigad@16819
   805
  apply simp
avigad@16819
   806
done
avigad@16819
   807
avigad@16819
   808
lemma le_natfloor: "real x <= a ==> x <= natfloor a"
avigad@16819
   809
  apply (unfold natfloor_def)
avigad@16819
   810
  apply (subst nat_int [THEN sym])
avigad@16819
   811
  apply (subst nat_le_eq_zle)
avigad@16819
   812
  apply simp
avigad@16819
   813
  apply (rule le_floor)
avigad@16819
   814
  apply simp
avigad@16819
   815
done
avigad@16819
   816
avigad@16819
   817
lemma le_natfloor_eq: "0 <= x ==> (a <= natfloor x) = (real a <= x)"
avigad@16819
   818
  apply (rule iffI)
avigad@16819
   819
  apply (rule order_trans)
avigad@16819
   820
  prefer 2
avigad@16819
   821
  apply (erule real_natfloor_le)
avigad@16819
   822
  apply (subst real_of_nat_le_iff)
avigad@16819
   823
  apply assumption
avigad@16819
   824
  apply (erule le_natfloor)
avigad@16819
   825
done
avigad@16819
   826
avigad@16819
   827
lemma le_natfloor_eq_number_of [simp]: 
avigad@16819
   828
    "~ neg((number_of n)::int) ==> 0 <= x ==>
avigad@16819
   829
      (number_of n <= natfloor x) = (number_of n <= x)"
avigad@16819
   830
  apply (subst le_natfloor_eq, assumption)
avigad@16819
   831
  apply simp
avigad@16819
   832
done
avigad@16819
   833
avigad@16819
   834
lemma le_natfloor_one_eq [simp]: "(1 <= natfloor x) = (1 <= x)"
avigad@16819
   835
  apply (case_tac "0 <= x")
avigad@16819
   836
  apply (subst le_natfloor_eq, assumption, simp)
avigad@16819
   837
  apply (rule iffI)
avigad@16819
   838
  apply (subgoal_tac "natfloor x <= natfloor 0") 
avigad@16819
   839
  apply simp
avigad@16819
   840
  apply (rule natfloor_mono)
avigad@16819
   841
  apply simp
avigad@16819
   842
  apply simp
avigad@16819
   843
done
avigad@16819
   844
avigad@16819
   845
lemma natfloor_eq: "real n <= x ==> x < real n + 1 ==> natfloor x = n"
avigad@16819
   846
  apply (unfold natfloor_def)
avigad@16819
   847
  apply (subst nat_int [THEN sym]);back;
avigad@16819
   848
  apply (subst eq_nat_nat_iff)
avigad@16819
   849
  apply simp
avigad@16819
   850
  apply simp
avigad@16819
   851
  apply (rule floor_eq2)
avigad@16819
   852
  apply auto
avigad@16819
   853
done
avigad@16819
   854
avigad@16819
   855
lemma real_natfloor_add_one_gt: "x < real(natfloor x) + 1"
avigad@16819
   856
  apply (case_tac "0 <= x")
avigad@16819
   857
  apply (unfold natfloor_def)
avigad@16819
   858
  apply simp
avigad@16819
   859
  apply simp_all
avigad@16819
   860
done
avigad@16819
   861
avigad@16819
   862
lemma real_natfloor_gt_diff_one: "x - 1 < real(natfloor x)"
avigad@16819
   863
  apply (simp add: compare_rls)
avigad@16819
   864
  apply (rule real_natfloor_add_one_gt)
avigad@16819
   865
done
avigad@16819
   866
avigad@16819
   867
lemma ge_natfloor_plus_one_imp_gt: "natfloor z + 1 <= n ==> z < real n"
avigad@16819
   868
  apply (subgoal_tac "z < real(natfloor z) + 1")
avigad@16819
   869
  apply arith
avigad@16819
   870
  apply (rule real_natfloor_add_one_gt)
avigad@16819
   871
done
avigad@16819
   872
avigad@16819
   873
lemma natfloor_add [simp]: "0 <= x ==> natfloor (x + real a) = natfloor x + a"
avigad@16819
   874
  apply (unfold natfloor_def)
avigad@16819
   875
  apply (subgoal_tac "real a = real (int a)")
avigad@16819
   876
  apply (erule ssubst)
avigad@16819
   877
  apply (simp add: nat_add_distrib)
avigad@16819
   878
  apply simp
avigad@16819
   879
done
avigad@16819
   880
avigad@16819
   881
lemma natfloor_add_number_of [simp]: 
avigad@16819
   882
    "~neg ((number_of n)::int) ==> 0 <= x ==> 
avigad@16819
   883
      natfloor (x + number_of n) = natfloor x + number_of n"
avigad@16819
   884
  apply (subst natfloor_add [THEN sym])
avigad@16819
   885
  apply simp_all
avigad@16819
   886
done
avigad@16819
   887
avigad@16819
   888
lemma natfloor_add_one: "0 <= x ==> natfloor(x + 1) = natfloor x + 1"
avigad@16819
   889
  apply (subst natfloor_add [THEN sym])
avigad@16819
   890
  apply assumption
avigad@16819
   891
  apply simp
avigad@16819
   892
done
avigad@16819
   893
avigad@16819
   894
lemma natfloor_subtract [simp]: "real a <= x ==> 
avigad@16819
   895
    natfloor(x - real a) = natfloor x - a"
avigad@16819
   896
  apply (unfold natfloor_def)
avigad@16819
   897
  apply (subgoal_tac "real a = real (int a)")
avigad@16819
   898
  apply (erule ssubst)
avigad@16819
   899
  apply simp
avigad@16819
   900
  apply (subst nat_diff_distrib)
avigad@16819
   901
  apply simp
avigad@16819
   902
  apply (rule le_floor)
avigad@16819
   903
  apply simp_all
avigad@16819
   904
done
avigad@16819
   905
avigad@16819
   906
lemma natceiling_zero [simp]: "natceiling 0 = 0"
avigad@16819
   907
  by (unfold natceiling_def, simp)
avigad@16819
   908
avigad@16819
   909
lemma natceiling_one [simp]: "natceiling 1 = 1"
avigad@16819
   910
  by (unfold natceiling_def, simp)
avigad@16819
   911
avigad@16819
   912
lemma zero_le_natceiling [simp]: "0 <= natceiling x"
avigad@16819
   913
  by (unfold natceiling_def, simp)
avigad@16819
   914
avigad@16819
   915
lemma natceiling_number_of_eq [simp]: "natceiling (number_of n) = number_of n"
avigad@16819
   916
  by (unfold natceiling_def, simp)
avigad@16819
   917
avigad@16819
   918
lemma natceiling_real_of_nat [simp]: "natceiling(real n) = n"
avigad@16819
   919
  by (unfold natceiling_def, simp)
avigad@16819
   920
avigad@16819
   921
lemma real_natceiling_ge: "x <= real(natceiling x)"
avigad@16819
   922
  apply (unfold natceiling_def)
avigad@16819
   923
  apply (case_tac "x < 0")
avigad@16819
   924
  apply simp
avigad@16819
   925
  apply (subst real_nat_eq_real)
avigad@16819
   926
  apply (subgoal_tac "ceiling 0 <= ceiling x")
avigad@16819
   927
  apply simp
avigad@16819
   928
  apply (rule ceiling_mono2)
avigad@16819
   929
  apply simp
avigad@16819
   930
  apply simp
avigad@16819
   931
done
avigad@16819
   932
avigad@16819
   933
lemma natceiling_neg: "x <= 0 ==> natceiling x = 0"
avigad@16819
   934
  apply (unfold natceiling_def)
avigad@16819
   935
  apply simp
avigad@16819
   936
done
avigad@16819
   937
avigad@16819
   938
lemma natceiling_mono: "x <= y ==> natceiling x <= natceiling y"
avigad@16819
   939
  apply (case_tac "0 <= x")
avigad@16819
   940
  apply (subst natceiling_def)+
avigad@16819
   941
  apply (subst nat_le_eq_zle)
avigad@16819
   942
  apply (rule disjI2)
avigad@16819
   943
  apply (subgoal_tac "real (0::int) <= real(ceiling y)")
avigad@16819
   944
  apply simp
avigad@16819
   945
  apply (rule order_trans)
avigad@16819
   946
  apply simp
avigad@16819
   947
  apply (erule order_trans)
avigad@16819
   948
  apply simp
avigad@16819
   949
  apply (erule ceiling_mono2)
avigad@16819
   950
  apply (subst natceiling_neg)
avigad@16819
   951
  apply simp_all
avigad@16819
   952
done
avigad@16819
   953
avigad@16819
   954
lemma natceiling_le: "x <= real a ==> natceiling x <= a"
avigad@16819
   955
  apply (unfold natceiling_def)
avigad@16819
   956
  apply (case_tac "x < 0")
avigad@16819
   957
  apply simp
avigad@16819
   958
  apply (subst nat_int [THEN sym]);back;
avigad@16819
   959
  apply (subst nat_le_eq_zle)
avigad@16819
   960
  apply simp
avigad@16819
   961
  apply (rule ceiling_le)
avigad@16819
   962
  apply simp
avigad@16819
   963
done
avigad@16819
   964
avigad@16819
   965
lemma natceiling_le_eq: "0 <= x ==> (natceiling x <= a) = (x <= real a)"
avigad@16819
   966
  apply (rule iffI)
avigad@16819
   967
  apply (rule order_trans)
avigad@16819
   968
  apply (rule real_natceiling_ge)
avigad@16819
   969
  apply (subst real_of_nat_le_iff)
avigad@16819
   970
  apply assumption
avigad@16819
   971
  apply (erule natceiling_le)
avigad@16819
   972
done
avigad@16819
   973
avigad@16819
   974
lemma natceiling_le_eq2 [simp]: "~ neg((number_of n)::int) ==> 0 <= x ==>
avigad@16819
   975
    (natceiling x <= number_of n) = (x <= number_of n)"
avigad@16819
   976
  apply (subst natceiling_le_eq, assumption)
avigad@16819
   977
  apply simp
avigad@16819
   978
done
avigad@16819
   979
avigad@16819
   980
lemma natceiling_one_le_eq: "(natceiling x <= 1) = (x <= 1)"
avigad@16819
   981
  apply (case_tac "0 <= x")
avigad@16819
   982
  apply (subst natceiling_le_eq)
avigad@16819
   983
  apply assumption
avigad@16819
   984
  apply simp
avigad@16819
   985
  apply (subst natceiling_neg)
avigad@16819
   986
  apply simp
avigad@16819
   987
  apply simp
avigad@16819
   988
done
avigad@16819
   989
avigad@16819
   990
lemma natceiling_eq: "real n < x ==> x <= real n + 1 ==> natceiling x = n + 1"
avigad@16819
   991
  apply (unfold natceiling_def)
avigad@16819
   992
  apply (subst nat_int [THEN sym]);back;
avigad@16819
   993
  apply (subgoal_tac "nat(int n) + 1 = nat(int n + 1)")
avigad@16819
   994
  apply (erule ssubst)
avigad@16819
   995
  apply (subst eq_nat_nat_iff)
avigad@16819
   996
  apply (subgoal_tac "ceiling 0 <= ceiling x")
avigad@16819
   997
  apply simp
avigad@16819
   998
  apply (rule ceiling_mono2)
avigad@16819
   999
  apply force
avigad@16819
  1000
  apply force
avigad@16819
  1001
  apply (rule ceiling_eq2)
avigad@16819
  1002
  apply (simp, simp)
avigad@16819
  1003
  apply (subst nat_add_distrib)
avigad@16819
  1004
  apply auto
avigad@16819
  1005
done
avigad@16819
  1006
avigad@16819
  1007
lemma natceiling_add [simp]: "0 <= x ==> 
avigad@16819
  1008
    natceiling (x + real a) = natceiling x + a"
avigad@16819
  1009
  apply (unfold natceiling_def)
avigad@16819
  1010
  apply (subgoal_tac "real a = real (int a)")
avigad@16819
  1011
  apply (erule ssubst)
avigad@16819
  1012
  apply simp
avigad@16819
  1013
  apply (subst nat_add_distrib)
avigad@16819
  1014
  apply (subgoal_tac "0 = ceiling 0")
avigad@16819
  1015
  apply (erule ssubst)
avigad@16819
  1016
  apply (erule ceiling_mono2)
avigad@16819
  1017
  apply simp_all
avigad@16819
  1018
done
avigad@16819
  1019
avigad@16819
  1020
lemma natceiling_add2 [simp]: "~ neg ((number_of n)::int) ==> 0 <= x ==> 
avigad@16819
  1021
    natceiling (x + number_of n) = natceiling x + number_of n"
avigad@16819
  1022
  apply (subst natceiling_add [THEN sym])
avigad@16819
  1023
  apply simp_all
avigad@16819
  1024
done
avigad@16819
  1025
avigad@16819
  1026
lemma natceiling_add_one: "0 <= x ==> natceiling(x + 1) = natceiling x + 1"
avigad@16819
  1027
  apply (subst natceiling_add [THEN sym])
avigad@16819
  1028
  apply assumption
avigad@16819
  1029
  apply simp
avigad@16819
  1030
done
avigad@16819
  1031
avigad@16819
  1032
lemma natceiling_subtract [simp]: "real a <= x ==> 
avigad@16819
  1033
    natceiling(x - real a) = natceiling x - a"
avigad@16819
  1034
  apply (unfold natceiling_def)
avigad@16819
  1035
  apply (subgoal_tac "real a = real (int a)")
avigad@16819
  1036
  apply (erule ssubst)
avigad@16819
  1037
  apply simp
avigad@16819
  1038
  apply (subst nat_diff_distrib)
avigad@16819
  1039
  apply simp
avigad@16819
  1040
  apply (rule order_trans)
avigad@16819
  1041
  prefer 2
avigad@16819
  1042
  apply (rule ceiling_mono2)
avigad@16819
  1043
  apply assumption
avigad@16819
  1044
  apply simp_all
avigad@16819
  1045
done
avigad@16819
  1046
avigad@16819
  1047
lemma natfloor_div_nat: "1 <= x ==> 0 < y ==> 
avigad@16819
  1048
  natfloor (x / real y) = natfloor x div y"
avigad@16819
  1049
proof -
avigad@16819
  1050
  assume "1 <= (x::real)" and "0 < (y::nat)"
avigad@16819
  1051
  have "natfloor x = (natfloor x) div y * y + (natfloor x) mod y"
avigad@16819
  1052
    by simp
avigad@16819
  1053
  then have a: "real(natfloor x) = real ((natfloor x) div y) * real y + 
avigad@16819
  1054
    real((natfloor x) mod y)"
avigad@16819
  1055
    by (simp only: real_of_nat_add [THEN sym] real_of_nat_mult [THEN sym])
avigad@16819
  1056
  have "x = real(natfloor x) + (x - real(natfloor x))"
avigad@16819
  1057
    by simp
avigad@16819
  1058
  then have "x = real ((natfloor x) div y) * real y + 
avigad@16819
  1059
      real((natfloor x) mod y) + (x - real(natfloor x))"
avigad@16819
  1060
    by (simp add: a)
avigad@16819
  1061
  then have "x / real y = ... / real y"
avigad@16819
  1062
    by simp
avigad@16819
  1063
  also have "... = real((natfloor x) div y) + real((natfloor x) mod y) / 
avigad@16819
  1064
    real y + (x - real(natfloor x)) / real y"
avigad@16819
  1065
    by (auto simp add: ring_distrib ring_eq_simps add_divide_distrib
avigad@16819
  1066
      diff_divide_distrib prems)
avigad@16819
  1067
  finally have "natfloor (x / real y) = natfloor(...)" by simp
avigad@16819
  1068
  also have "... = natfloor(real((natfloor x) mod y) / 
avigad@16819
  1069
    real y + (x - real(natfloor x)) / real y + real((natfloor x) div y))"
avigad@16819
  1070
    by (simp add: add_ac)
avigad@16819
  1071
  also have "... = natfloor(real((natfloor x) mod y) / 
avigad@16819
  1072
    real y + (x - real(natfloor x)) / real y) + (natfloor x) div y"
avigad@16819
  1073
    apply (rule natfloor_add)
avigad@16819
  1074
    apply (rule add_nonneg_nonneg)
avigad@16819
  1075
    apply (rule divide_nonneg_pos)
avigad@16819
  1076
    apply simp
avigad@16819
  1077
    apply (simp add: prems)
avigad@16819
  1078
    apply (rule divide_nonneg_pos)
avigad@16819
  1079
    apply (simp add: compare_rls)
avigad@16819
  1080
    apply (rule real_natfloor_le)
avigad@16819
  1081
    apply (insert prems, auto)
avigad@16819
  1082
    done
avigad@16819
  1083
  also have "natfloor(real((natfloor x) mod y) / 
avigad@16819
  1084
    real y + (x - real(natfloor x)) / real y) = 0"
avigad@16819
  1085
    apply (rule natfloor_eq)
avigad@16819
  1086
    apply simp
avigad@16819
  1087
    apply (rule add_nonneg_nonneg)
avigad@16819
  1088
    apply (rule divide_nonneg_pos)
avigad@16819
  1089
    apply force
avigad@16819
  1090
    apply (force simp add: prems)
avigad@16819
  1091
    apply (rule divide_nonneg_pos)
avigad@16819
  1092
    apply (simp add: compare_rls)
avigad@16819
  1093
    apply (rule real_natfloor_le)
avigad@16819
  1094
    apply (auto simp add: prems)
avigad@16819
  1095
    apply (insert prems, arith)
avigad@16819
  1096
    apply (simp add: add_divide_distrib [THEN sym])
avigad@16819
  1097
    apply (subgoal_tac "real y = real y - 1 + 1")
avigad@16819
  1098
    apply (erule ssubst)
avigad@16819
  1099
    apply (rule add_le_less_mono)
avigad@16819
  1100
    apply (simp add: compare_rls)
avigad@16819
  1101
    apply (subgoal_tac "real(natfloor x mod y) + 1 = 
avigad@16819
  1102
      real(natfloor x mod y + 1)")
avigad@16819
  1103
    apply (erule ssubst)
avigad@16819
  1104
    apply (subst real_of_nat_le_iff)
avigad@16819
  1105
    apply (subgoal_tac "natfloor x mod y < y")
avigad@16819
  1106
    apply arith
avigad@16819
  1107
    apply (rule mod_less_divisor)
avigad@16819
  1108
    apply assumption
avigad@16819
  1109
    apply auto
avigad@16819
  1110
    apply (simp add: compare_rls)
avigad@16819
  1111
    apply (subst add_commute)
avigad@16819
  1112
    apply (rule real_natfloor_add_one_gt)
avigad@16819
  1113
    done
avigad@16819
  1114
  finally show ?thesis
avigad@16819
  1115
    by simp
avigad@16819
  1116
qed
avigad@16819
  1117
paulson@14641
  1118
ML
paulson@14641
  1119
{*
paulson@14641
  1120
val number_of_less_real_of_int_iff = thm "number_of_less_real_of_int_iff";
paulson@14641
  1121
val number_of_less_real_of_int_iff2 = thm "number_of_less_real_of_int_iff2";
paulson@14641
  1122
val number_of_le_real_of_int_iff = thm "number_of_le_real_of_int_iff";
paulson@14641
  1123
val number_of_le_real_of_int_iff2 = thm "number_of_le_real_of_int_iff2";
paulson@14641
  1124
val floor_zero = thm "floor_zero";
paulson@14641
  1125
val floor_real_of_nat_zero = thm "floor_real_of_nat_zero";
paulson@14641
  1126
val floor_real_of_nat = thm "floor_real_of_nat";
paulson@14641
  1127
val floor_minus_real_of_nat = thm "floor_minus_real_of_nat";
paulson@14641
  1128
val floor_real_of_int = thm "floor_real_of_int";
paulson@14641
  1129
val floor_minus_real_of_int = thm "floor_minus_real_of_int";
paulson@14641
  1130
val reals_Archimedean6 = thm "reals_Archimedean6";
paulson@14641
  1131
val reals_Archimedean6a = thm "reals_Archimedean6a";
paulson@14641
  1132
val reals_Archimedean_6b_int = thm "reals_Archimedean_6b_int";
paulson@14641
  1133
val reals_Archimedean_6c_int = thm "reals_Archimedean_6c_int";
paulson@14641
  1134
val real_lb_ub_int = thm "real_lb_ub_int";
paulson@14641
  1135
val lemma_floor = thm "lemma_floor";
paulson@14641
  1136
val real_of_int_floor_le = thm "real_of_int_floor_le";
avigad@16819
  1137
(*val floor_le = thm "floor_le";
paulson@14641
  1138
val floor_le2 = thm "floor_le2";
avigad@16819
  1139
*)
paulson@14641
  1140
val lemma_floor2 = thm "lemma_floor2";
paulson@14641
  1141
val real_of_int_floor_cancel = thm "real_of_int_floor_cancel";
paulson@14641
  1142
val floor_eq = thm "floor_eq";
paulson@14641
  1143
val floor_eq2 = thm "floor_eq2";
paulson@14641
  1144
val floor_eq3 = thm "floor_eq3";
paulson@14641
  1145
val floor_eq4 = thm "floor_eq4";
paulson@14641
  1146
val floor_number_of_eq = thm "floor_number_of_eq";
paulson@14641
  1147
val real_of_int_floor_ge_diff_one = thm "real_of_int_floor_ge_diff_one";
paulson@14641
  1148
val real_of_int_floor_add_one_ge = thm "real_of_int_floor_add_one_ge";
paulson@14641
  1149
val ceiling_zero = thm "ceiling_zero";
paulson@14641
  1150
val ceiling_real_of_nat = thm "ceiling_real_of_nat";
paulson@14641
  1151
val ceiling_real_of_nat_zero = thm "ceiling_real_of_nat_zero";
paulson@14641
  1152
val ceiling_floor = thm "ceiling_floor";
paulson@14641
  1153
val floor_ceiling = thm "floor_ceiling";
paulson@14641
  1154
val real_of_int_ceiling_ge = thm "real_of_int_ceiling_ge";
avigad@16819
  1155
(*
paulson@14641
  1156
val ceiling_le = thm "ceiling_le";
paulson@14641
  1157
val ceiling_le2 = thm "ceiling_le2";
avigad@16819
  1158
*)
paulson@14641
  1159
val real_of_int_ceiling_cancel = thm "real_of_int_ceiling_cancel";
paulson@14641
  1160
val ceiling_eq = thm "ceiling_eq";
paulson@14641
  1161
val ceiling_eq2 = thm "ceiling_eq2";
paulson@14641
  1162
val ceiling_eq3 = thm "ceiling_eq3";
paulson@14641
  1163
val ceiling_real_of_int = thm "ceiling_real_of_int";
paulson@14641
  1164
val ceiling_number_of_eq = thm "ceiling_number_of_eq";
paulson@14641
  1165
val real_of_int_ceiling_diff_one_le = thm "real_of_int_ceiling_diff_one_le";
paulson@14641
  1166
val real_of_int_ceiling_le_add_one = thm "real_of_int_ceiling_le_add_one";
paulson@14641
  1167
*}
paulson@14641
  1168
paulson@14641
  1169
paulson@14365
  1170
end