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.5    by (simp add: less_ceiling_iff)
     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.16    apply (simp add: frac_def)
    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?)+)[2])+
    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