monotonicity of rounding and truncating float
authorimmler
Mon Dec 16 17:08:22 2013 +0100 (2013-12-16)
changeset 5478454f1ce13c140
parent 54783 25860d89a044
child 54785 4876fb408c0d
monotonicity of rounding and truncating float
src/HOL/Library/Float.thy
     1.1 --- a/src/HOL/Library/Float.thy	Mon Dec 16 17:08:22 2013 +0100
     1.2 +++ b/src/HOL/Library/Float.thy	Mon Dec 16 17:08:22 2013 +0100
     1.3 @@ -1326,6 +1326,203 @@
     1.4      cong del: if_weak_cong)
     1.5  hide_fact (open) compute_float_round_up
     1.6  
     1.7 +lemma round_up_mono: "x \<le> y \<Longrightarrow> round_up p x \<le> round_up p y"
     1.8 +  by (auto intro!: ceiling_mono simp: round_up_def)
     1.9 +
    1.10 +lemma truncate_up_nonneg_mono:
    1.11 +  assumes "0 \<le> x" "x \<le> y"
    1.12 +  shows "truncate_up prec x \<le> truncate_up prec y"
    1.13 +proof -
    1.14 +  {
    1.15 +    assume "\<lfloor>log 2 x\<rfloor> = \<lfloor>log 2 y\<rfloor>"
    1.16 +    hence ?thesis
    1.17 +      using assms
    1.18 +      by (auto simp: truncate_up_def round_up_def intro!: ceiling_mono)
    1.19 +  } moreover {
    1.20 +    assume "0 < x"
    1.21 +    hence "log 2 x \<le> log 2 y" using assms by auto
    1.22 +    moreover
    1.23 +    assume "\<lfloor>log 2 x\<rfloor> \<noteq> \<lfloor>log 2 y\<rfloor>"
    1.24 +    ultimately have logless: "log 2 x < log 2 y" and flogless: "\<lfloor>log 2 x\<rfloor> < \<lfloor>log 2 y\<rfloor>"
    1.25 +      unfolding atomize_conj
    1.26 +      by (metis floor_less_cancel linorder_cases not_le)
    1.27 +    have "truncate_up prec x =
    1.28 +      real \<lceil>x * 2 powr real (int prec - \<lfloor>log 2 x\<rfloor> - 1)\<rceil> * 2 powr - real (int prec - \<lfloor>log 2 x\<rfloor> - 1)"
    1.29 +      using assms by (simp add: truncate_up_def round_up_def)
    1.30 +    also have "\<lceil>x * 2 powr real (int prec - \<lfloor>log 2 x\<rfloor> - 1)\<rceil> \<le> (2 ^ prec)"
    1.31 +    proof (unfold ceiling_le_eq)
    1.32 +      have "x * 2 powr real (int prec - \<lfloor>log 2 x\<rfloor> - 1) \<le> x * (2 powr real prec / (2 powr log 2 x))"
    1.33 +        using real_of_int_floor_add_one_ge[of "log 2 x"] assms
    1.34 +        by (auto simp add: algebra_simps powr_divide2 intro!: mult_left_mono)
    1.35 +      thus "x * 2 powr real (int prec - \<lfloor>log 2 x\<rfloor> - 1) \<le> real ((2::int) ^ prec)"
    1.36 +        using `0 < x` by (simp add: powr_realpow)
    1.37 +    qed
    1.38 +    hence "real \<lceil>x * 2 powr real (int prec - \<lfloor>log 2 x\<rfloor> - 1)\<rceil> \<le> 2 powr int prec"
    1.39 +      by (auto simp: powr_realpow)
    1.40 +    also
    1.41 +    have "2 powr - real (int prec - \<lfloor>log 2 x\<rfloor> - 1) \<le> 2 powr - real (int prec - \<lfloor>log 2 y\<rfloor>)"
    1.42 +      using logless flogless by (auto intro!: floor_mono)
    1.43 +    also have "2 powr real (int prec) \<le> 2 powr (log 2 y + real (int prec - \<lfloor>log 2 y\<rfloor>))"
    1.44 +      using assms `0 < x`
    1.45 +      by (auto simp: algebra_simps)
    1.46 +    finally have "truncate_up prec x \<le> 2 powr (log 2 y + real (int prec - \<lfloor>log 2 y\<rfloor>)) * 2 powr - real (int prec - \<lfloor>log 2 y\<rfloor>)"
    1.47 +      by simp
    1.48 +    also have "\<dots> = 2 powr (log 2 y + real (int prec - \<lfloor>log 2 y\<rfloor>) - real (int prec - \<lfloor>log 2 y\<rfloor>))"
    1.49 +      by (subst powr_add[symmetric]) simp
    1.50 +    also have "\<dots> = y"
    1.51 +      using `0 < x` assms
    1.52 +      by (simp add: powr_add)
    1.53 +    also have "\<dots> \<le> truncate_up prec y"
    1.54 +      by (rule truncate_up)
    1.55 +    finally have ?thesis .
    1.56 +  } moreover {
    1.57 +    assume "~ 0 < x"
    1.58 +    hence ?thesis
    1.59 +      using assms
    1.60 +      by (auto intro!: truncate_up_le)
    1.61 +  } ultimately show ?thesis
    1.62 +    by blast
    1.63 +qed
    1.64 +
    1.65 +lemma truncate_up_nonpos: "x \<le> 0 \<Longrightarrow> truncate_up prec x \<le> 0"
    1.66 +  by (auto simp: truncate_up_def round_up_def intro!: mult_nonpos_nonneg)
    1.67 +
    1.68 +lemma truncate_down_nonpos: "x \<le> 0 \<Longrightarrow> truncate_down prec x \<le> 0"
    1.69 +  by (auto simp: truncate_down_def round_down_def intro!: mult_nonpos_nonneg
    1.70 +    order_le_less_trans[of _ 0, OF mult_nonpos_nonneg])
    1.71 +
    1.72 +lemma truncate_up_switch_sign_mono:
    1.73 +  assumes "x \<le> 0" "0 \<le> y"
    1.74 +  shows "truncate_up prec x \<le> truncate_up prec y"
    1.75 +proof -
    1.76 +  note truncate_up_nonpos[OF `x \<le> 0`]
    1.77 +  also note truncate_up_le[OF `0 \<le> y`]
    1.78 +  finally show ?thesis .
    1.79 +qed
    1.80 +
    1.81 +lemma truncate_down_zeroprec_mono:
    1.82 +  assumes "0 < x" "x \<le> y"
    1.83 +  shows "truncate_down 0 x \<le> truncate_down 0 y"
    1.84 +proof -
    1.85 +  have "x * 2 powr (- real \<lfloor>log 2 x\<rfloor> - 1) = x * inverse (2 powr ((real \<lfloor>log 2 x\<rfloor> + 1)))"
    1.86 +    by (simp add: powr_divide2[symmetric] powr_add powr_minus inverse_eq_divide)
    1.87 +  also have "\<dots> = 2 powr (log 2 x - (real \<lfloor>log 2 x\<rfloor>) - 1)"
    1.88 +    using `0 < x`
    1.89 +    by (auto simp: inverse_eq_divide field_simps powr_add powr_divide2[symmetric])
    1.90 +  also have "\<dots> < 2 powr 0"
    1.91 +    using real_of_int_floor_add_one_gt
    1.92 +    unfolding neg_less_iff_less
    1.93 +    by (intro powr_less_mono) (auto simp: algebra_simps)
    1.94 +  finally have "\<lfloor>x * 2 powr (- real \<lfloor>log 2 x\<rfloor> - 1)\<rfloor> < 1"
    1.95 +    unfolding less_ceiling_eq real_of_int_minus real_of_one
    1.96 +    by simp
    1.97 +  moreover
    1.98 +  have "0 \<le> \<lfloor>x * 2 powr (- real \<lfloor>log 2 x\<rfloor> - 1)\<rfloor>"
    1.99 +    using `x > 0` by (auto intro: mult_nonneg_nonneg)
   1.100 +  ultimately have "\<lfloor>x * 2 powr (- real \<lfloor>log 2 x\<rfloor> - 1)\<rfloor> \<in> {0 ..< 1}"
   1.101 +    by simp
   1.102 +  also have "\<dots> \<subseteq> {0}" by auto
   1.103 +  finally have "\<lfloor>x * 2 powr (- real \<lfloor>log 2 x\<rfloor> - 1)\<rfloor> = 0" by simp
   1.104 +  with assms show ?thesis
   1.105 +    by (auto simp: truncate_down_def round_down_def intro!: mult_nonneg_nonneg)
   1.106 +qed
   1.107 +
   1.108 +lemma truncate_down_nonneg: "0 \<le> y \<Longrightarrow> 0 \<le> truncate_down prec y"
   1.109 +  by (auto simp: truncate_down_def round_down_def intro!: mult_nonneg_nonneg)
   1.110 +
   1.111 +lemma truncate_down_zero: "truncate_down prec 0 = 0"
   1.112 +  by (auto simp: truncate_down_def round_down_def intro!: mult_nonneg_nonneg)
   1.113 +
   1.114 +lemma truncate_down_switch_sign_mono:
   1.115 +  assumes "x \<le> 0" "0 \<le> y"
   1.116 +  assumes "x \<le> y"
   1.117 +  shows "truncate_down prec x \<le> truncate_down prec y"
   1.118 +proof -
   1.119 +  note truncate_down_nonpos[OF `x \<le> 0`]
   1.120 +  also note truncate_down_nonneg[OF `0 \<le> y`]
   1.121 +  finally show ?thesis .
   1.122 +qed
   1.123 +
   1.124 +lemma truncate_up_uminus_truncate_down:
   1.125 +  "truncate_up prec x = - truncate_down prec (- x)"
   1.126 +  "truncate_up prec (-x) = - truncate_down prec x"
   1.127 +  by (auto simp: truncate_up_def round_up_def truncate_down_def round_down_def ceiling_def)
   1.128 +
   1.129 +lemma truncate_down_uminus_truncate_up:
   1.130 +  "truncate_down prec x = - truncate_up prec (- x)"
   1.131 +  "truncate_down prec (-x) = - truncate_up prec x"
   1.132 +  by (auto simp: truncate_up_def round_up_def truncate_down_def round_down_def ceiling_def)
   1.133 +
   1.134 +lemma truncate_down_nonneg_mono:
   1.135 +  assumes "0 \<le> x" "x \<le> y"
   1.136 +  shows "truncate_down prec x \<le> truncate_down prec y"
   1.137 +proof -
   1.138 +  {
   1.139 +    assume "0 < x" "prec = 0"
   1.140 +    with assms have ?thesis
   1.141 +      by (simp add: truncate_down_zeroprec_mono)
   1.142 +  } moreover {
   1.143 +    assume "~ 0 < x"
   1.144 +    with assms have "x = 0" "0 \<le> y" by simp_all
   1.145 +    hence ?thesis
   1.146 +      by (auto simp add: truncate_down_zero intro!: truncate_down_nonneg)
   1.147 +  } moreover {
   1.148 +    assume "\<lfloor>log 2 \<bar>x\<bar>\<rfloor> = \<lfloor>log 2 \<bar>y\<bar>\<rfloor>"
   1.149 +    hence ?thesis
   1.150 +      using assms
   1.151 +      by (auto simp: truncate_down_def round_down_def intro!: floor_mono)
   1.152 +  } moreover {
   1.153 +    assume "0 < x"
   1.154 +    hence "log 2 x \<le> log 2 y" "0 < y" "0 \<le> y" using assms by auto
   1.155 +    moreover
   1.156 +    assume "\<lfloor>log 2 \<bar>x\<bar>\<rfloor> \<noteq> \<lfloor>log 2 \<bar>y\<bar>\<rfloor>"
   1.157 +    ultimately have logless: "log 2 x < log 2 y" and flogless: "\<lfloor>log 2 x\<rfloor> < \<lfloor>log 2 y\<rfloor>"
   1.158 +      unfolding atomize_conj abs_of_pos[OF `0 < x`] abs_of_pos[OF `0 < y`]
   1.159 +      by (metis floor_less_cancel linorder_cases not_le)
   1.160 +    assume "prec \<noteq> 0" hence [simp]: "prec \<ge> Suc 0" by auto
   1.161 +    have "2 powr (prec - 1) \<le> y * 2 powr real (prec - 1) / (2 powr log 2 y)"
   1.162 +      using `0 < y`
   1.163 +      by simp
   1.164 +    also have "\<dots> \<le> y * 2 powr real prec / (2 powr (real \<lfloor>log 2 y\<rfloor> + 1))"
   1.165 +      using `0 \<le> y` `0 \<le> x` assms(2)
   1.166 +      by (auto intro!: powr_mono mult_nonneg_nonneg mult_pos_pos divide_left_mono
   1.167 +        simp: real_of_nat_diff powr_add
   1.168 +        powr_divide2[symmetric])
   1.169 +    also have "\<dots> = y * 2 powr real prec / (2 powr real \<lfloor>log 2 y\<rfloor> * 2)"
   1.170 +      by (auto simp: powr_add)
   1.171 +    finally have "(2 ^ (prec - 1)) \<le> \<lfloor>y * 2 powr real (int prec - \<lfloor>log 2 \<bar>y\<bar>\<rfloor> - 1)\<rfloor>"
   1.172 +      using `0 \<le> y`
   1.173 +      by (auto simp: powr_divide2[symmetric] le_floor_eq powr_realpow)
   1.174 +    hence "(2 ^ (prec - 1)) * 2 powr - real (int prec - \<lfloor>log 2 \<bar>y\<bar>\<rfloor> - 1) \<le> truncate_down prec y"
   1.175 +      by (auto simp: truncate_down_def round_down_def)
   1.176 +    moreover
   1.177 +    {
   1.178 +      have "x = 2 powr (log 2 \<bar>x\<bar>)" using `0 < x` by simp
   1.179 +      also have "\<dots> \<le> (2 ^ (prec )) * 2 powr - real (int prec - \<lfloor>log 2 \<bar>x\<bar>\<rfloor> - 1)"
   1.180 +        using real_of_int_floor_add_one_ge[of "log 2 \<bar>x\<bar>"]
   1.181 +        by (auto simp: powr_realpow[symmetric] powr_add[symmetric] algebra_simps)
   1.182 +      also
   1.183 +      have "2 powr - real (int prec - \<lfloor>log 2 \<bar>x\<bar>\<rfloor> - 1) \<le> 2 powr - real (int prec - \<lfloor>log 2 \<bar>y\<bar>\<rfloor>)"
   1.184 +        using logless flogless `x > 0` `y > 0`
   1.185 +        by (auto intro!: floor_mono)
   1.186 +      finally have "x \<le> (2 ^ (prec - 1)) * 2 powr - real (int prec - \<lfloor>log 2 \<bar>y\<bar>\<rfloor> - 1)"
   1.187 +        by (auto simp: powr_realpow[symmetric] powr_divide2[symmetric] assms real_of_nat_diff)
   1.188 +    } ultimately have ?thesis
   1.189 +      by (metis dual_order.trans truncate_down)
   1.190 +  } ultimately show ?thesis by blast
   1.191 +qed
   1.192 +
   1.193 +lemma truncate_down_mono: "x \<le> y \<Longrightarrow> truncate_down p x \<le> truncate_down p y"
   1.194 +  apply (cases "0 \<le> x")
   1.195 +  apply (rule truncate_down_nonneg_mono, assumption+)
   1.196 +  apply (simp add: truncate_down_uminus_truncate_up)
   1.197 +  apply (cases "0 \<le> y")
   1.198 +  apply (auto intro: truncate_up_nonneg_mono truncate_up_switch_sign_mono)
   1.199 +  done
   1.200 +
   1.201 +lemma truncate_up_mono: "x \<le> y \<Longrightarrow> truncate_up p x \<le> truncate_up p y"
   1.202 +  by (simp add: truncate_up_uminus_truncate_down truncate_down_mono)
   1.203 +
   1.204  lemma Float_le_zero_iff: "Float a b \<le> 0 \<longleftrightarrow> a \<le> 0"
   1.205   apply (auto simp: zero_float_def mult_le_0_iff)
   1.206   using powr_gt_zero[of 2 b] by simp