src/HOL/Archimedean_Field.thy
author haftmann
Thu Apr 09 09:12:47 2015 +0200 (2015-04-09)
changeset 59984 4f1eccec320c
parent 59613 7103019278f0
child 60128 3d696ccb7fa6
permissions -rw-r--r--
conversion between division on nat/int and division in archmedean fields
     1 (*  Title:      HOL/Archimedean_Field.thy
     2     Author:     Brian Huffman
     3 *)
     4 
     5 section {* Archimedean Fields, Floor and Ceiling Functions *}
     6 
     7 theory Archimedean_Field
     8 imports Main
     9 begin
    10 
    11 subsection {* Class of Archimedean fields *}
    12 
    13 text {* Archimedean fields have no infinite elements. *}
    14 
    15 class archimedean_field = linordered_field +
    16   assumes ex_le_of_int: "\<exists>z. x \<le> of_int z"
    17 
    18 lemma ex_less_of_int:
    19   fixes x :: "'a::archimedean_field" shows "\<exists>z. x < of_int z"
    20 proof -
    21   from ex_le_of_int obtain z where "x \<le> of_int z" ..
    22   then have "x < of_int (z + 1)" by simp
    23   then show ?thesis ..
    24 qed
    25 
    26 lemma ex_of_int_less:
    27   fixes x :: "'a::archimedean_field" shows "\<exists>z. of_int z < x"
    28 proof -
    29   from ex_less_of_int obtain z where "- x < of_int z" ..
    30   then have "of_int (- z) < x" by simp
    31   then show ?thesis ..
    32 qed
    33 
    34 lemma ex_less_of_nat:
    35   fixes x :: "'a::archimedean_field" shows "\<exists>n. x < of_nat n"
    36 proof -
    37   obtain z where "x < of_int z" using ex_less_of_int ..
    38   also have "\<dots> \<le> of_int (int (nat z))" by simp
    39   also have "\<dots> = of_nat (nat z)" by (simp only: of_int_of_nat_eq)
    40   finally show ?thesis ..
    41 qed
    42 
    43 lemma ex_le_of_nat:
    44   fixes x :: "'a::archimedean_field" shows "\<exists>n. x \<le> of_nat n"
    45 proof -
    46   obtain n where "x < of_nat n" using ex_less_of_nat ..
    47   then have "x \<le> of_nat n" by simp
    48   then show ?thesis ..
    49 qed
    50 
    51 text {* Archimedean fields have no infinitesimal elements. *}
    52 
    53 lemma ex_inverse_of_nat_Suc_less:
    54   fixes x :: "'a::archimedean_field"
    55   assumes "0 < x" shows "\<exists>n. inverse (of_nat (Suc n)) < x"
    56 proof -
    57   from `0 < x` have "0 < inverse x"
    58     by (rule positive_imp_inverse_positive)
    59   obtain n where "inverse x < of_nat n"
    60     using ex_less_of_nat ..
    61   then obtain m where "inverse x < of_nat (Suc m)"
    62     using `0 < inverse x` by (cases n) (simp_all del: of_nat_Suc)
    63   then have "inverse (of_nat (Suc m)) < inverse (inverse x)"
    64     using `0 < inverse x` by (rule less_imp_inverse_less)
    65   then have "inverse (of_nat (Suc m)) < x"
    66     using `0 < x` by (simp add: nonzero_inverse_inverse_eq)
    67   then show ?thesis ..
    68 qed
    69 
    70 lemma ex_inverse_of_nat_less:
    71   fixes x :: "'a::archimedean_field"
    72   assumes "0 < x" shows "\<exists>n>0. inverse (of_nat n) < x"
    73   using ex_inverse_of_nat_Suc_less [OF `0 < x`] by auto
    74 
    75 lemma ex_less_of_nat_mult:
    76   fixes x :: "'a::archimedean_field"
    77   assumes "0 < x" shows "\<exists>n. y < of_nat n * x"
    78 proof -
    79   obtain n where "y / x < of_nat n" using ex_less_of_nat ..
    80   with `0 < x` have "y < of_nat n * x" by (simp add: pos_divide_less_eq)
    81   then show ?thesis ..
    82 qed
    83 
    84 
    85 subsection {* Existence and uniqueness of floor function *}
    86 
    87 lemma exists_least_lemma:
    88   assumes "\<not> P 0" and "\<exists>n. P n"
    89   shows "\<exists>n. \<not> P n \<and> P (Suc n)"
    90 proof -
    91   from `\<exists>n. P n` have "P (Least P)" by (rule LeastI_ex)
    92   with `\<not> P 0` obtain n where "Least P = Suc n"
    93     by (cases "Least P") auto
    94   then have "n < Least P" by simp
    95   then have "\<not> P n" by (rule not_less_Least)
    96   then have "\<not> P n \<and> P (Suc n)"
    97     using `P (Least P)` `Least P = Suc n` by simp
    98   then show ?thesis ..
    99 qed
   100 
   101 lemma floor_exists:
   102   fixes x :: "'a::archimedean_field"
   103   shows "\<exists>z. of_int z \<le> x \<and> x < of_int (z + 1)"
   104 proof (cases)
   105   assume "0 \<le> x"
   106   then have "\<not> x < of_nat 0" by simp
   107   then have "\<exists>n. \<not> x < of_nat n \<and> x < of_nat (Suc n)"
   108     using ex_less_of_nat by (rule exists_least_lemma)
   109   then obtain n where "\<not> x < of_nat n \<and> x < of_nat (Suc n)" ..
   110   then have "of_int (int n) \<le> x \<and> x < of_int (int n + 1)" by simp
   111   then show ?thesis ..
   112 next
   113   assume "\<not> 0 \<le> x"
   114   then have "\<not> - x \<le> of_nat 0" by simp
   115   then have "\<exists>n. \<not> - x \<le> of_nat n \<and> - x \<le> of_nat (Suc n)"
   116     using ex_le_of_nat by (rule exists_least_lemma)
   117   then obtain n where "\<not> - x \<le> of_nat n \<and> - x \<le> of_nat (Suc n)" ..
   118   then have "of_int (- int n - 1) \<le> x \<and> x < of_int (- int n - 1 + 1)" by simp
   119   then show ?thesis ..
   120 qed
   121 
   122 lemma floor_exists1:
   123   fixes x :: "'a::archimedean_field"
   124   shows "\<exists>!z. of_int z \<le> x \<and> x < of_int (z + 1)"
   125 proof (rule ex_ex1I)
   126   show "\<exists>z. of_int z \<le> x \<and> x < of_int (z + 1)"
   127     by (rule floor_exists)
   128 next
   129   fix y z assume
   130     "of_int y \<le> x \<and> x < of_int (y + 1)"
   131     "of_int z \<le> x \<and> x < of_int (z + 1)"
   132   with le_less_trans [of "of_int y" "x" "of_int (z + 1)"]
   133        le_less_trans [of "of_int z" "x" "of_int (y + 1)"]
   134   show "y = z" by (simp del: of_int_add)
   135 qed
   136 
   137 
   138 subsection {* Floor function *}
   139 
   140 class floor_ceiling = archimedean_field +
   141   fixes floor :: "'a \<Rightarrow> int"
   142   assumes floor_correct: "of_int (floor x) \<le> x \<and> x < of_int (floor x + 1)"
   143 
   144 notation (xsymbols)
   145   floor  ("\<lfloor>_\<rfloor>")
   146 
   147 notation (HTML output)
   148   floor  ("\<lfloor>_\<rfloor>")
   149 
   150 lemma floor_unique: "\<lbrakk>of_int z \<le> x; x < of_int z + 1\<rbrakk> \<Longrightarrow> floor x = z"
   151   using floor_correct [of x] floor_exists1 [of x] by auto
   152 
   153 lemma floor_unique_iff:
   154   fixes x :: "'a::floor_ceiling"
   155   shows  "\<lfloor>x\<rfloor> = a \<longleftrightarrow> of_int a \<le> x \<and> x < of_int a + 1"
   156 using floor_correct floor_unique by auto
   157 
   158 lemma of_int_floor_le: "of_int (floor x) \<le> x"
   159   using floor_correct ..
   160 
   161 lemma le_floor_iff: "z \<le> floor x \<longleftrightarrow> of_int z \<le> x"
   162 proof
   163   assume "z \<le> floor x"
   164   then have "(of_int z :: 'a) \<le> of_int (floor x)" by simp
   165   also have "of_int (floor x) \<le> x" by (rule of_int_floor_le)
   166   finally show "of_int z \<le> x" .
   167 next
   168   assume "of_int z \<le> x"
   169   also have "x < of_int (floor x + 1)" using floor_correct ..
   170   finally show "z \<le> floor x" by (simp del: of_int_add)
   171 qed
   172 
   173 lemma floor_less_iff: "floor x < z \<longleftrightarrow> x < of_int z"
   174   by (simp add: not_le [symmetric] le_floor_iff)
   175 
   176 lemma less_floor_iff: "z < floor x \<longleftrightarrow> of_int z + 1 \<le> x"
   177   using le_floor_iff [of "z + 1" x] by auto
   178 
   179 lemma floor_le_iff: "floor x \<le> z \<longleftrightarrow> x < of_int z + 1"
   180   by (simp add: not_less [symmetric] less_floor_iff)
   181 
   182 lemma floor_split[arith_split]: "P (floor t) \<longleftrightarrow> (\<forall>i. of_int i \<le> t \<and> t < of_int i + 1 \<longrightarrow> P i)"
   183   by (metis floor_correct floor_unique less_floor_iff not_le order_refl)
   184 
   185 lemma floor_mono: assumes "x \<le> y" shows "floor x \<le> floor y"
   186 proof -
   187   have "of_int (floor x) \<le> x" by (rule of_int_floor_le)
   188   also note `x \<le> y`
   189   finally show ?thesis by (simp add: le_floor_iff)
   190 qed
   191 
   192 lemma floor_less_cancel: "floor x < floor y \<Longrightarrow> x < y"
   193   by (auto simp add: not_le [symmetric] floor_mono)
   194 
   195 lemma floor_of_int [simp]: "floor (of_int z) = z"
   196   by (rule floor_unique) simp_all
   197 
   198 lemma floor_of_nat [simp]: "floor (of_nat n) = int n"
   199   using floor_of_int [of "of_nat n"] by simp
   200 
   201 lemma le_floor_add: "floor x + floor y \<le> floor (x + y)"
   202   by (simp only: le_floor_iff of_int_add add_mono of_int_floor_le)
   203 
   204 text {* Floor with numerals *}
   205 
   206 lemma floor_zero [simp]: "floor 0 = 0"
   207   using floor_of_int [of 0] by simp
   208 
   209 lemma floor_one [simp]: "floor 1 = 1"
   210   using floor_of_int [of 1] by simp
   211 
   212 lemma floor_numeral [simp]: "floor (numeral v) = numeral v"
   213   using floor_of_int [of "numeral v"] by simp
   214 
   215 lemma floor_neg_numeral [simp]: "floor (- numeral v) = - numeral v"
   216   using floor_of_int [of "- numeral v"] by simp
   217 
   218 lemma zero_le_floor [simp]: "0 \<le> floor x \<longleftrightarrow> 0 \<le> x"
   219   by (simp add: le_floor_iff)
   220 
   221 lemma one_le_floor [simp]: "1 \<le> floor x \<longleftrightarrow> 1 \<le> x"
   222   by (simp add: le_floor_iff)
   223 
   224 lemma numeral_le_floor [simp]:
   225   "numeral v \<le> floor x \<longleftrightarrow> numeral v \<le> x"
   226   by (simp add: le_floor_iff)
   227 
   228 lemma neg_numeral_le_floor [simp]:
   229   "- numeral v \<le> floor x \<longleftrightarrow> - numeral v \<le> x"
   230   by (simp add: le_floor_iff)
   231 
   232 lemma zero_less_floor [simp]: "0 < floor x \<longleftrightarrow> 1 \<le> x"
   233   by (simp add: less_floor_iff)
   234 
   235 lemma one_less_floor [simp]: "1 < floor x \<longleftrightarrow> 2 \<le> x"
   236   by (simp add: less_floor_iff)
   237 
   238 lemma numeral_less_floor [simp]:
   239   "numeral v < floor x \<longleftrightarrow> numeral v + 1 \<le> x"
   240   by (simp add: less_floor_iff)
   241 
   242 lemma neg_numeral_less_floor [simp]:
   243   "- numeral v < floor x \<longleftrightarrow> - numeral v + 1 \<le> x"
   244   by (simp add: less_floor_iff)
   245 
   246 lemma floor_le_zero [simp]: "floor x \<le> 0 \<longleftrightarrow> x < 1"
   247   by (simp add: floor_le_iff)
   248 
   249 lemma floor_le_one [simp]: "floor x \<le> 1 \<longleftrightarrow> x < 2"
   250   by (simp add: floor_le_iff)
   251 
   252 lemma floor_le_numeral [simp]:
   253   "floor x \<le> numeral v \<longleftrightarrow> x < numeral v + 1"
   254   by (simp add: floor_le_iff)
   255 
   256 lemma floor_le_neg_numeral [simp]:
   257   "floor x \<le> - numeral v \<longleftrightarrow> x < - numeral v + 1"
   258   by (simp add: floor_le_iff)
   259 
   260 lemma floor_less_zero [simp]: "floor x < 0 \<longleftrightarrow> x < 0"
   261   by (simp add: floor_less_iff)
   262 
   263 lemma floor_less_one [simp]: "floor x < 1 \<longleftrightarrow> x < 1"
   264   by (simp add: floor_less_iff)
   265 
   266 lemma floor_less_numeral [simp]:
   267   "floor x < numeral v \<longleftrightarrow> x < numeral v"
   268   by (simp add: floor_less_iff)
   269 
   270 lemma floor_less_neg_numeral [simp]:
   271   "floor x < - numeral v \<longleftrightarrow> x < - numeral v"
   272   by (simp add: floor_less_iff)
   273 
   274 text {* Addition and subtraction of integers *}
   275 
   276 lemma floor_add_of_int [simp]: "floor (x + of_int z) = floor x + z"
   277   using floor_correct [of x] by (simp add: floor_unique)
   278 
   279 lemma floor_add_numeral [simp]:
   280     "floor (x + numeral v) = floor x + numeral v"
   281   using floor_add_of_int [of x "numeral v"] by simp
   282 
   283 lemma floor_add_one [simp]: "floor (x + 1) = floor x + 1"
   284   using floor_add_of_int [of x 1] by simp
   285 
   286 lemma floor_diff_of_int [simp]: "floor (x - of_int z) = floor x - z"
   287   using floor_add_of_int [of x "- z"] by (simp add: algebra_simps)
   288 
   289 lemma floor_uminus_of_int [simp]: "floor (- (of_int z)) = - z"
   290   by (metis floor_diff_of_int [of 0] diff_0 floor_zero)
   291 
   292 lemma floor_diff_numeral [simp]:
   293   "floor (x - numeral v) = floor x - numeral v"
   294   using floor_diff_of_int [of x "numeral v"] by simp
   295 
   296 lemma floor_diff_one [simp]: "floor (x - 1) = floor x - 1"
   297   using floor_diff_of_int [of x 1] by simp
   298 
   299 lemma le_mult_floor:
   300   assumes "0 \<le> a" and "0 \<le> b"
   301   shows "floor a * floor b \<le> floor (a * b)"
   302 proof -
   303   have "of_int (floor a) \<le> a"
   304     and "of_int (floor b) \<le> b" by (auto intro: of_int_floor_le)
   305   hence "of_int (floor a * floor b) \<le> a * b"
   306     using assms by (auto intro!: mult_mono)
   307   also have "a * b < of_int (floor (a * b) + 1)"  
   308     using floor_correct[of "a * b"] by auto
   309   finally show ?thesis unfolding of_int_less_iff by simp
   310 qed
   311 
   312 lemma floor_divide_of_int_eq:
   313   fixes k l :: int
   314   shows "\<lfloor>of_int k / of_int l\<rfloor> = of_int (k div l)"
   315 proof (cases "l = 0")
   316   case True then show ?thesis by simp
   317 next
   318   case False
   319   have *: "\<lfloor>of_int (k mod l) / of_int l :: 'a\<rfloor> = 0"
   320   proof (cases "l > 0")
   321     case True then show ?thesis
   322       by (auto intro: floor_unique)
   323   next
   324     case False
   325     obtain r where "r = - l" by blast
   326     then have l: "l = - r" by simp
   327     moreover with `l \<noteq> 0` False have "r > 0" by simp
   328     ultimately show ?thesis using pos_mod_bound [of r]
   329       by (auto simp add: zmod_zminus2_eq_if less_le field_simps intro: floor_unique)
   330   qed
   331   have "(of_int k :: 'a) = of_int (k div l * l + k mod l)"
   332     by simp
   333   also have "\<dots> = (of_int (k div l) + of_int (k mod l) / of_int l) * of_int l"
   334     using False by (simp only: of_int_add) (simp add: field_simps)
   335   finally have "(of_int k / of_int l :: 'a) = \<dots> / of_int l"
   336     by simp 
   337   then have "(of_int k / of_int l :: 'a) = of_int (k div l) + of_int (k mod l) / of_int l"
   338     using False by (simp only:) (simp add: field_simps)
   339   then have "\<lfloor>of_int k / of_int l :: 'a\<rfloor> = \<lfloor>of_int (k div l) + of_int (k mod l) / of_int l :: 'a\<rfloor>" 
   340     by simp
   341   then have "\<lfloor>of_int k / of_int l :: 'a\<rfloor> = \<lfloor>of_int (k mod l) / of_int l + of_int (k div l) :: 'a\<rfloor>"
   342     by (simp add: ac_simps)
   343   then have "\<lfloor>of_int k / of_int l :: 'a\<rfloor> = \<lfloor>of_int (k mod l) / of_int l :: 'a\<rfloor> + of_int (k div l)"
   344     by simp
   345   with * show ?thesis by simp
   346 qed
   347 
   348 lemma floor_divide_of_nat_eq:
   349   fixes m n :: nat
   350   shows "\<lfloor>of_nat m / of_nat n\<rfloor> = of_nat (m div n)"
   351 proof (cases "n = 0")
   352   case True then show ?thesis by simp
   353 next
   354   case False
   355   then have *: "\<lfloor>of_nat (m mod n) / of_nat n :: 'a\<rfloor> = 0"
   356     by (auto intro: floor_unique)
   357   have "(of_nat m :: 'a) = of_nat (m div n * n + m mod n)"
   358     by simp
   359   also have "\<dots> = (of_nat (m div n) + of_nat (m mod n) / of_nat n) * of_nat n"
   360     using False by (simp only: of_nat_add) (simp add: field_simps of_nat_mult)
   361   finally have "(of_nat m / of_nat n :: 'a) = \<dots> / of_nat n"
   362     by simp 
   363   then have "(of_nat m / of_nat n :: 'a) = of_nat (m div n) + of_nat (m mod n) / of_nat n"
   364     using False by (simp only:) simp
   365   then have "\<lfloor>of_nat m / of_nat n :: 'a\<rfloor> = \<lfloor>of_nat (m div n) + of_nat (m mod n) / of_nat n :: 'a\<rfloor>" 
   366     by simp
   367   then have "\<lfloor>of_nat m / of_nat n :: 'a\<rfloor> = \<lfloor>of_nat (m mod n) / of_nat n + of_nat (m div n) :: 'a\<rfloor>"
   368     by (simp add: ac_simps)
   369   moreover have "(of_nat (m div n) :: 'a) = of_int (of_nat (m div n))"
   370     by simp
   371   ultimately have "\<lfloor>of_nat m / of_nat n :: 'a\<rfloor> = \<lfloor>of_nat (m mod n) / of_nat n :: 'a\<rfloor> + of_nat (m div n)"
   372     by (simp only: floor_add_of_int)
   373   with * show ?thesis by simp
   374 qed
   375 
   376 
   377 subsection {* Ceiling function *}
   378 
   379 definition
   380   ceiling :: "'a::floor_ceiling \<Rightarrow> int" where
   381   "ceiling x = - floor (- x)"
   382 
   383 notation (xsymbols)
   384   ceiling  ("\<lceil>_\<rceil>")
   385 
   386 notation (HTML output)
   387   ceiling  ("\<lceil>_\<rceil>")
   388 
   389 lemma ceiling_correct: "of_int (ceiling x) - 1 < x \<and> x \<le> of_int (ceiling x)"
   390   unfolding ceiling_def using floor_correct [of "- x"] by simp
   391 
   392 lemma ceiling_unique: "\<lbrakk>of_int z - 1 < x; x \<le> of_int z\<rbrakk> \<Longrightarrow> ceiling x = z"
   393   unfolding ceiling_def using floor_unique [of "- z" "- x"] by simp
   394 
   395 lemma le_of_int_ceiling: "x \<le> of_int (ceiling x)"
   396   using ceiling_correct ..
   397 
   398 lemma ceiling_le_iff: "ceiling x \<le> z \<longleftrightarrow> x \<le> of_int z"
   399   unfolding ceiling_def using le_floor_iff [of "- z" "- x"] by auto
   400 
   401 lemma less_ceiling_iff: "z < ceiling x \<longleftrightarrow> of_int z < x"
   402   by (simp add: not_le [symmetric] ceiling_le_iff)
   403 
   404 lemma ceiling_less_iff: "ceiling x < z \<longleftrightarrow> x \<le> of_int z - 1"
   405   using ceiling_le_iff [of x "z - 1"] by simp
   406 
   407 lemma le_ceiling_iff: "z \<le> ceiling x \<longleftrightarrow> of_int z - 1 < x"
   408   by (simp add: not_less [symmetric] ceiling_less_iff)
   409 
   410 lemma ceiling_mono: "x \<ge> y \<Longrightarrow> ceiling x \<ge> ceiling y"
   411   unfolding ceiling_def by (simp add: floor_mono)
   412 
   413 lemma ceiling_less_cancel: "ceiling x < ceiling y \<Longrightarrow> x < y"
   414   by (auto simp add: not_le [symmetric] ceiling_mono)
   415 
   416 lemma ceiling_of_int [simp]: "ceiling (of_int z) = z"
   417   by (rule ceiling_unique) simp_all
   418 
   419 lemma ceiling_of_nat [simp]: "ceiling (of_nat n) = int n"
   420   using ceiling_of_int [of "of_nat n"] by simp
   421 
   422 lemma ceiling_add_le: "ceiling (x + y) \<le> ceiling x + ceiling y"
   423   by (simp only: ceiling_le_iff of_int_add add_mono le_of_int_ceiling)
   424 
   425 text {* Ceiling with numerals *}
   426 
   427 lemma ceiling_zero [simp]: "ceiling 0 = 0"
   428   using ceiling_of_int [of 0] by simp
   429 
   430 lemma ceiling_one [simp]: "ceiling 1 = 1"
   431   using ceiling_of_int [of 1] by simp
   432 
   433 lemma ceiling_numeral [simp]: "ceiling (numeral v) = numeral v"
   434   using ceiling_of_int [of "numeral v"] by simp
   435 
   436 lemma ceiling_neg_numeral [simp]: "ceiling (- numeral v) = - numeral v"
   437   using ceiling_of_int [of "- numeral v"] by simp
   438 
   439 lemma ceiling_le_zero [simp]: "ceiling x \<le> 0 \<longleftrightarrow> x \<le> 0"
   440   by (simp add: ceiling_le_iff)
   441 
   442 lemma ceiling_le_one [simp]: "ceiling x \<le> 1 \<longleftrightarrow> x \<le> 1"
   443   by (simp add: ceiling_le_iff)
   444 
   445 lemma ceiling_le_numeral [simp]:
   446   "ceiling x \<le> numeral v \<longleftrightarrow> x \<le> numeral v"
   447   by (simp add: ceiling_le_iff)
   448 
   449 lemma ceiling_le_neg_numeral [simp]:
   450   "ceiling x \<le> - numeral v \<longleftrightarrow> x \<le> - numeral v"
   451   by (simp add: ceiling_le_iff)
   452 
   453 lemma ceiling_less_zero [simp]: "ceiling x < 0 \<longleftrightarrow> x \<le> -1"
   454   by (simp add: ceiling_less_iff)
   455 
   456 lemma ceiling_less_one [simp]: "ceiling x < 1 \<longleftrightarrow> x \<le> 0"
   457   by (simp add: ceiling_less_iff)
   458 
   459 lemma ceiling_less_numeral [simp]:
   460   "ceiling x < numeral v \<longleftrightarrow> x \<le> numeral v - 1"
   461   by (simp add: ceiling_less_iff)
   462 
   463 lemma ceiling_less_neg_numeral [simp]:
   464   "ceiling x < - numeral v \<longleftrightarrow> x \<le> - numeral v - 1"
   465   by (simp add: ceiling_less_iff)
   466 
   467 lemma zero_le_ceiling [simp]: "0 \<le> ceiling x \<longleftrightarrow> -1 < x"
   468   by (simp add: le_ceiling_iff)
   469 
   470 lemma one_le_ceiling [simp]: "1 \<le> ceiling x \<longleftrightarrow> 0 < x"
   471   by (simp add: le_ceiling_iff)
   472 
   473 lemma numeral_le_ceiling [simp]:
   474   "numeral v \<le> ceiling x \<longleftrightarrow> numeral v - 1 < x"
   475   by (simp add: le_ceiling_iff)
   476 
   477 lemma neg_numeral_le_ceiling [simp]:
   478   "- numeral v \<le> ceiling x \<longleftrightarrow> - numeral v - 1 < x"
   479   by (simp add: le_ceiling_iff)
   480 
   481 lemma zero_less_ceiling [simp]: "0 < ceiling x \<longleftrightarrow> 0 < x"
   482   by (simp add: less_ceiling_iff)
   483 
   484 lemma one_less_ceiling [simp]: "1 < ceiling x \<longleftrightarrow> 1 < x"
   485   by (simp add: less_ceiling_iff)
   486 
   487 lemma numeral_less_ceiling [simp]:
   488   "numeral v < ceiling x \<longleftrightarrow> numeral v < x"
   489   by (simp add: less_ceiling_iff)
   490 
   491 lemma neg_numeral_less_ceiling [simp]:
   492   "- numeral v < ceiling x \<longleftrightarrow> - numeral v < x"
   493   by (simp add: less_ceiling_iff)
   494 
   495 text {* Addition and subtraction of integers *}
   496 
   497 lemma ceiling_add_of_int [simp]: "ceiling (x + of_int z) = ceiling x + z"
   498   using ceiling_correct [of x] by (simp add: ceiling_unique)
   499 
   500 lemma ceiling_add_numeral [simp]:
   501     "ceiling (x + numeral v) = ceiling x + numeral v"
   502   using ceiling_add_of_int [of x "numeral v"] by simp
   503 
   504 lemma ceiling_add_one [simp]: "ceiling (x + 1) = ceiling x + 1"
   505   using ceiling_add_of_int [of x 1] by simp
   506 
   507 lemma ceiling_diff_of_int [simp]: "ceiling (x - of_int z) = ceiling x - z"
   508   using ceiling_add_of_int [of x "- z"] by (simp add: algebra_simps)
   509 
   510 lemma ceiling_diff_numeral [simp]:
   511   "ceiling (x - numeral v) = ceiling x - numeral v"
   512   using ceiling_diff_of_int [of x "numeral v"] by simp
   513 
   514 lemma ceiling_diff_one [simp]: "ceiling (x - 1) = ceiling x - 1"
   515   using ceiling_diff_of_int [of x 1] by simp
   516 
   517 lemma ceiling_split[arith_split]: "P (ceiling t) \<longleftrightarrow> (\<forall>i. of_int i - 1 < t \<and> t \<le> of_int i \<longrightarrow> P i)"
   518   by (auto simp add: ceiling_unique ceiling_correct)
   519 
   520 lemma ceiling_diff_floor_le_1: "ceiling x - floor x \<le> 1"
   521 proof -
   522   have "of_int \<lceil>x\<rceil> - 1 < x" 
   523     using ceiling_correct[of x] by simp
   524   also have "x < of_int \<lfloor>x\<rfloor> + 1"
   525     using floor_correct[of x] by simp_all
   526   finally have "of_int (\<lceil>x\<rceil> - \<lfloor>x\<rfloor>) < (of_int 2::'a)"
   527     by simp
   528   then show ?thesis
   529     unfolding of_int_less_iff by simp
   530 qed
   531 
   532 subsection {* Negation *}
   533 
   534 lemma floor_minus: "floor (- x) = - ceiling x"
   535   unfolding ceiling_def by simp
   536 
   537 lemma ceiling_minus: "ceiling (- x) = - floor x"
   538   unfolding ceiling_def by simp
   539 
   540 subsection {* Frac Function *}
   541 
   542 
   543 definition frac :: "'a \<Rightarrow> 'a::floor_ceiling" where
   544   "frac x \<equiv> x - of_int \<lfloor>x\<rfloor>"
   545 
   546 lemma frac_lt_1: "frac x < 1"
   547   by  (simp add: frac_def) linarith
   548 
   549 lemma frac_eq_0_iff [simp]: "frac x = 0 \<longleftrightarrow> x \<in> Ints"
   550   by (simp add: frac_def) (metis Ints_cases Ints_of_int floor_of_int )
   551 
   552 lemma frac_ge_0 [simp]: "frac x \<ge> 0"
   553   unfolding frac_def
   554   by linarith
   555 
   556 lemma frac_gt_0_iff [simp]: "frac x > 0 \<longleftrightarrow> x \<notin> Ints"
   557   by (metis frac_eq_0_iff frac_ge_0 le_less less_irrefl)
   558 
   559 lemma frac_of_int [simp]: "frac (of_int z) = 0"
   560   by (simp add: frac_def)
   561 
   562 lemma floor_add: "\<lfloor>x + y\<rfloor> = (if frac x + frac y < 1 then \<lfloor>x\<rfloor> + \<lfloor>y\<rfloor> else (\<lfloor>x\<rfloor> + \<lfloor>y\<rfloor>) + 1)"  
   563 proof -
   564   {assume "x + y < 1 + (of_int \<lfloor>x\<rfloor> + of_int \<lfloor>y\<rfloor>)"
   565    then have "\<lfloor>x + y\<rfloor> = \<lfloor>x\<rfloor> + \<lfloor>y\<rfloor>"
   566      by (metis add.commute floor_unique le_floor_add le_floor_iff of_int_add)
   567    }
   568   moreover
   569   { assume "\<not> x + y < 1 + (of_int \<lfloor>x\<rfloor> + of_int \<lfloor>y\<rfloor>)"
   570     then have "\<lfloor>x + y\<rfloor> = 1 + (\<lfloor>x\<rfloor> + \<lfloor>y\<rfloor>)"
   571       apply (simp add: floor_unique_iff)
   572       apply (auto simp add: algebra_simps)
   573       by linarith    
   574   }
   575   ultimately show ?thesis
   576     by (auto simp add: frac_def algebra_simps)
   577 qed
   578 
   579 lemma frac_add: "frac (x + y) = (if frac x + frac y < 1 then frac x + frac y
   580                                  else (frac x + frac y) - 1)"  
   581   by (simp add: frac_def floor_add)
   582 
   583 lemma frac_unique_iff:
   584   fixes x :: "'a::floor_ceiling"
   585   shows  "(frac x) = a \<longleftrightarrow> x - a \<in> Ints \<and> 0 \<le> a \<and> a < 1"
   586   apply (auto simp: Ints_def frac_def)
   587   apply linarith
   588   apply linarith
   589   by (metis (no_types) add.commute add.left_neutral eq_diff_eq floor_add_of_int floor_unique of_int_0)
   590 
   591 lemma frac_eq: "(frac x) = x \<longleftrightarrow> 0 \<le> x \<and> x < 1"
   592   by (simp add: frac_unique_iff)
   593   
   594 lemma frac_neg:
   595   fixes x :: "'a::floor_ceiling"
   596   shows  "frac (-x) = (if x \<in> Ints then 0 else 1 - frac x)"
   597   apply (auto simp add: frac_unique_iff)
   598   apply (simp add: frac_def)
   599   by (meson frac_lt_1 less_iff_diff_less_0 not_le not_less_iff_gr_or_eq)
   600 
   601 end