src/HOL/Archimedean_Field.thy
 changeset 61531 ab2e862263e7 parent 61378 3e04c9ca001a child 61649 268d88ec9087
```     1.1 --- a/src/HOL/Archimedean_Field.thy	Thu Oct 29 15:40:52 2015 +0100
1.2 +++ b/src/HOL/Archimedean_Field.thy	Mon Nov 02 11:56:28 2015 +0100
1.3 @@ -486,6 +486,11 @@
1.4    "- numeral v < ceiling x \<longleftrightarrow> - numeral v < x"
1.6
1.7 +lemma ceiling_altdef: "ceiling x = (if x = of_int (floor x) then floor x else floor x + 1)"
1.8 +  by (intro ceiling_unique, (simp, linarith?)+)
1.9 +
1.10 +lemma floor_le_ceiling [simp]: "floor x \<le> ceiling x" by (simp add: ceiling_altdef)
1.11 +
1.12  text \<open>Addition and subtraction of integers\<close>
1.13
1.14  lemma ceiling_add_of_int [simp]: "ceiling (x + of_int z) = ceiling x + z"
1.15 @@ -592,4 +597,79 @@
1.17    by (meson frac_lt_1 less_iff_diff_less_0 not_le not_less_iff_gr_or_eq)
1.18
1.19 +
1.20 +subsection \<open>Rounding to the nearest integer\<close>
1.21 +
1.22 +definition round where "round x = \<lfloor>x + 1/2\<rfloor>"
1.23 +
1.24 +lemma of_int_round_ge:     "of_int (round x) \<ge> x - 1/2"
1.25 +  and of_int_round_le:     "of_int (round x) \<le> x + 1/2"
1.26 +  and of_int_round_abs_le: "\<bar>of_int (round x) - x\<bar> \<le> 1/2"
1.27 +  and of_int_round_gt:     "of_int (round x) > x - 1/2"
1.28 +proof -
1.29 +  from floor_correct[of "x + 1/2"] have "x + 1/2 < of_int (round x) + 1" by (simp add: round_def)
1.30 +  from add_strict_right_mono[OF this, of "-1"] show A: "of_int (round x) > x - 1/2" by simp
1.31 +  thus "of_int (round x) \<ge> x - 1/2" by simp
1.32 +  from floor_correct[of "x + 1/2"] show "of_int (round x) \<le> x + 1/2" by (simp add: round_def)
1.33 +  with A show "\<bar>of_int (round x) - x\<bar> \<le> 1/2" by linarith
1.34 +qed
1.35 +
1.36 +lemma round_of_int [simp]: "round (of_int n) = n"
1.37 +  unfolding round_def by (subst floor_unique_iff) force
1.38 +
1.39 +lemma round_0 [simp]: "round 0 = 0"
1.40 +  using round_of_int[of 0] by simp
1.41 +
1.42 +lemma round_1 [simp]: "round 1 = 1"
1.43 +  using round_of_int[of 1] by simp
1.44 +
1.45 +lemma round_numeral [simp]: "round (numeral n) = numeral n"
1.46 +  using round_of_int[of "numeral n"] by simp
1.47 +
1.48 +lemma round_neg_numeral [simp]: "round (-numeral n) = -numeral n"
1.49 +  using round_of_int[of "-numeral n"] by simp
1.50 +
1.51 +lemma round_of_nat [simp]: "round (of_nat n) = of_nat n"
1.52 +  using round_of_int[of "int n"] by simp
1.53 +
1.54 +lemma round_mono: "x \<le> y \<Longrightarrow> round x \<le> round y"
1.55 +  unfolding round_def by (intro floor_mono) simp
1.56 +
1.57 +lemma round_unique: "of_int y > x - 1/2 \<Longrightarrow> of_int y \<le> x + 1/2 \<Longrightarrow> round x = y"
1.58 +unfolding round_def
1.59 +proof (rule floor_unique)
1.60 +  assume "x - 1 / 2 < of_int y"
1.61 +  from add_strict_left_mono[OF this, of 1] show "x + 1 / 2 < of_int y + 1" by simp
1.62 +qed
1.63 +
1.64 +lemma round_altdef: "round x = (if frac x \<ge> 1/2 then ceiling x else floor x)"
1.65 +  by (cases "frac x \<ge> 1/2")
1.66 +     (rule round_unique, ((simp add: frac_def field_simps ceiling_altdef, linarith?)+))+
1.67 +
1.68 +lemma floor_le_round: "\<lfloor>x\<rfloor> \<le> round x"
1.69 +  unfolding round_def by (intro floor_mono) simp
1.70 +
1.71 +lemma ceiling_ge_round: "\<lceil>x\<rceil> \<ge> round x" unfolding round_altdef by simp
1.72 +
1.73 +lemma round_diff_minimal:
1.74 +  fixes z :: "'a :: floor_ceiling"
1.75 +  shows "abs (z - of_int (round z)) \<le> abs (z - of_int m)"
1.76 +proof (cases "of_int m \<ge> z")
1.77 +  case True
1.78 +  hence "\<bar>z - of_int (round z)\<bar> \<le> \<bar>of_int (ceiling z) - z\<bar>"
1.79 +    unfolding round_altdef by (simp add: ceiling_altdef frac_def) linarith?
1.80 +  also have "of_int \<lceil>z\<rceil> - z \<ge> 0" by linarith
1.81 +  with True have "\<bar>of_int (ceiling z) - z\<bar> \<le> \<bar>z - of_int m\<bar>"
1.82 +    by (simp add: ceiling_le_iff)
1.83 +  finally show ?thesis .
1.84 +next
1.85 +  case False
1.86 +  hence "\<bar>z - of_int (round z)\<bar> \<le> \<bar>of_int (floor z) - z\<bar>"
1.87 +    unfolding round_altdef by (simp add: ceiling_altdef frac_def) linarith?
1.88 +  also have "z - of_int \<lfloor>z\<rfloor> \<ge> 0" by linarith
1.89 +  with False have "\<bar>of_int (floor z) - z\<bar> \<le> \<bar>z - of_int m\<bar>"
1.90 +    by (simp add: le_floor_iff)
1.91 +  finally show ?thesis .
1.92 +qed
1.93 +
1.94  end
```