# HG changeset patch
# User immler
# Date 1387210102 -3600
# Node ID cd8f55c358c5245fbf6c26bfa84d90f88f080bf4
# Parent  fe462aa28c3d2f95d228371ed89fcc0a5f1c76d1
additional definitions and lemmas for Float

diff -r fe462aa28c3d -r cd8f55c358c5 src/HOL/Decision_Procs/Approximation.thy
--- a/src/HOL/Decision_Procs/Approximation.thy	Mon Dec 16 17:08:22 2013 +0100
+++ b/src/HOL/Decision_Procs/Approximation.thy	Mon Dec 16 17:08:22 2013 +0100
@@ -534,7 +534,7 @@
       moreover have "?DIV \<le> real x / ?fR" by (rule float_divl)
       ultimately have "real ?DIV \<le> 1" unfolding divide_le_eq_1_pos[OF `0 < real ?fR`, symmetric] by auto
 
-      have "0 \<le> real ?DIV" using float_divl_lower_bound[OF `0 \<le> x` `0 < ?fR`] unfolding less_eq_float_def by auto
+      have "0 \<le> real ?DIV" using float_divl_lower_bound[OF `0 \<le> x`] `0 < ?fR` unfolding less_eq_float_def by auto
 
       have "(Float 1 1 * ?lb_horner ?DIV) \<le> 2 * arctan (float_divl prec x ?fR)"
         using arctan_0_1_bounds[OF `0 \<le> real ?DIV` `real ?DIV \<le> 1`] by auto
diff -r fe462aa28c3d -r cd8f55c358c5 src/HOL/Library/Float.thy
--- a/src/HOL/Library/Float.thy	Mon Dec 16 17:08:22 2013 +0100
+++ b/src/HOL/Library/Float.thy	Mon Dec 16 17:08:22 2013 +0100
@@ -555,29 +555,37 @@
 lift_definition float_up :: "int \<Rightarrow> float \<Rightarrow> float" is round_up by simp
 declare float_up.rep_eq[simp]
 
-lemma float_up_correct:
-  shows "real (float_up e f) - real f \<in> {0..2 powr -e}"
+lemma round_up_correct:
+  shows "round_up e f - f \<in> {0..2 powr -e}"
 unfolding atLeastAtMost_iff
 proof
   have "round_up e f - f \<le> round_up e f - round_down e f" using round_down by simp
   also have "\<dots> \<le> 2 powr -e" using round_up_diff_round_down by simp
-  finally show "real (float_up e f) - real f \<le> 2 powr real (- e)"
+  finally show "round_up e f - f \<le> 2 powr real (- e)"
     by simp
 qed (simp add: algebra_simps round_up)
 
+lemma float_up_correct:
+  shows "real (float_up e f) - real f \<in> {0..2 powr -e}"
+  by transfer (rule round_up_correct)
+
 lift_definition float_down :: "int \<Rightarrow> float \<Rightarrow> float" is round_down by simp
 declare float_down.rep_eq[simp]
 
-lemma float_down_correct:
-  shows "real f - real (float_down e f) \<in> {0..2 powr -e}"
+lemma round_down_correct:
+  shows "f - (round_down e f) \<in> {0..2 powr -e}"
 unfolding atLeastAtMost_iff
 proof
   have "f - round_down e f \<le> round_up e f - round_down e f" using round_up by simp
   also have "\<dots> \<le> 2 powr -e" using round_up_diff_round_down by simp
-  finally show "real f - real (float_down e f) \<le> 2 powr real (- e)"
+  finally show "f - round_down e f \<le> 2 powr real (- e)"
     by simp
 qed (simp add: algebra_simps round_down)
 
+lemma float_down_correct:
+  shows "real f - real (float_down e f) \<in> {0..2 powr -e}"
+  by transfer (rule round_down_correct)
+
 lemma compute_float_down[code]:
   "float_down p (Float m e) =
     (if p + e < 0 then Float (m div 2^nat (-(p + e))) (-p) else Float m e)"
@@ -602,6 +610,15 @@
 qed
 hide_fact (open) compute_float_down
 
+lemma abs_round_down_le: "\<bar>f - (round_down e f)\<bar> \<le> 2 powr -e"
+  using round_down_correct[of f e] by simp
+
+lemma abs_round_up_le: "\<bar>f - (round_up e f)\<bar> \<le> 2 powr -e"
+  using round_up_correct[of e f] by simp
+
+lemma round_down_nonneg: "0 \<le> s \<Longrightarrow> 0 \<le> round_down p s"
+  by (auto simp: round_down_def intro!: mult_nonneg_nonneg)
+
 lemma ceil_divide_floor_conv:
 assumes "b \<noteq> 0"
 shows "\<lceil>real a / real b\<rceil> = (if b dvd a then a div b else \<lfloor>real a / real b\<rfloor> + 1)"
@@ -1006,8 +1023,12 @@
 
 subsection {* Division *}
 
-lift_definition float_divl :: "nat \<Rightarrow> float \<Rightarrow> float \<Rightarrow> float" is
-  "\<lambda>(prec::nat) a b. round_down (prec + \<lfloor> log 2 \<bar>b\<bar> \<rfloor> - \<lfloor> log 2 \<bar>a\<bar> \<rfloor>) (a / b)" by simp
+definition "real_divl prec a b = round_down (int prec + \<lfloor> log 2 \<bar>b\<bar> \<rfloor> - \<lfloor> log 2 \<bar>a\<bar> \<rfloor>) (a / b)"
+
+definition "real_divr prec a b = round_up (int prec + \<lfloor> log 2 \<bar>b\<bar> \<rfloor> - \<lfloor> log 2 \<bar>a\<bar> \<rfloor>) (a / b)"
+
+lift_definition float_divl :: "nat \<Rightarrow> float \<Rightarrow> float \<Rightarrow> float" is real_divl
+  by (simp add: real_divl_def)
 
 lemma compute_float_divl[code]:
   "float_divl prec (Float m1 s1) (Float m2 s2) = lapprox_rat prec m1 m2 * Float 1 (s1 - s2)"
@@ -1022,12 +1043,13 @@
 
   show ?thesis
     using not_0
-    by (transfer fixing: m1 s1 m2 s2 prec) (unfold eq1 eq2 round_down_shift, simp add: field_simps)
-qed (transfer, auto)
+    by (transfer fixing: m1 s1 m2 s2 prec) (unfold eq1 eq2 round_down_shift real_divl_def,
+      simp add: field_simps)
+qed (transfer, auto simp: real_divl_def)
 hide_fact (open) compute_float_divl
 
-lift_definition float_divr :: "nat \<Rightarrow> float \<Rightarrow> float \<Rightarrow> float" is
-  "\<lambda>(prec::nat) a b. round_up (prec + \<lfloor> log 2 \<bar>b\<bar> \<rfloor> - \<lfloor> log 2 \<bar>a\<bar> \<rfloor>) (a / b)" by simp
+lift_definition float_divr :: "nat \<Rightarrow> float \<Rightarrow> float \<Rightarrow> float" is real_divr
+  by (simp add: real_divr_def)
 
 lemma compute_float_divr[code]:
   "float_divr prec (Float m1 s1) (Float m2 s2) = rapprox_rat prec m1 m2 * Float 1 (s1 - s2)"
@@ -1042,8 +1064,9 @@
 
   show ?thesis
     using not_0
-    by (transfer fixing: m1 s1 m2 s2 prec) (unfold eq1 eq2 round_up_shift, simp add: field_simps)
-qed (transfer, auto)
+    by (transfer fixing: m1 s1 m2 s2 prec) (unfold eq1 eq2 round_up_shift real_divr_def,
+      simp add: field_simps)
+qed (transfer, auto simp: real_divr_def)
 hide_fact (open) compute_float_divr
 
 subsection {* Lemmas needed by Approximate *}
@@ -1123,12 +1146,22 @@
   unfolding rapprox_rat_def round_up_def
   by (auto simp: field_simps mult_le_0_iff)
 
+lemma real_divl: "real_divl prec x y \<le> x / y"
+  by (simp add: real_divl_def round_down)
+
+lemma real_divr: "x / y \<le> real_divr prec x y"
+  using round_up by (simp add: real_divr_def)
+
 lemma float_divl: "real (float_divl prec x y) \<le> real x / real y"
-  by transfer (simp add: round_down)
+  by transfer (rule real_divl)
+
+lemma real_divl_lower_bound:
+  "0 \<le> x \<Longrightarrow> 0 \<le> y \<Longrightarrow> 0 \<le> real_divl prec x y"
+  by (simp add: real_divl_def round_down_def zero_le_mult_iff zero_le_divide_iff)
 
 lemma float_divl_lower_bound:
-  "0 \<le> x \<Longrightarrow> 0 < y \<Longrightarrow> 0 \<le> real (float_divl prec x y)"
-  by transfer (simp add: round_down_def zero_le_mult_iff zero_le_divide_iff)
+  "0 \<le> x \<Longrightarrow> 0 \<le> y \<Longrightarrow> 0 \<le> real (float_divl prec x y)"
+  by transfer (rule real_divl_lower_bound)
 
 lemma exponent_1: "exponent 1 = 0"
   using exponent_float[of 1 0] by (simp add: one_float_def)
@@ -1157,10 +1190,10 @@
   finally show ?thesis by (simp add: powr_add)
 qed
 
-lemma float_divl_pos_less1_bound:
-  "0 < real x \<Longrightarrow> real x < 1 \<Longrightarrow> prec \<ge> 1 \<Longrightarrow> 1 \<le> real (float_divl prec 1 x)"
-proof transfer
-  fix prec :: nat and x :: real assume x: "0 < x" "x < 1" "x \<in> float" and prec: "1 \<le> prec"
+lemma real_divl_pos_less1_bound:
+  "0 < x \<Longrightarrow> x < 1 \<Longrightarrow> prec \<ge> 1 \<Longrightarrow> 1 \<le> real_divl prec 1 x"
+proof (unfold real_divl_def)
+  fix prec :: nat and x :: real assume x: "0 < x" "x < 1" and prec: "1 \<le> prec"
   def p \<equiv> "int prec + \<lfloor>log 2 \<bar>x\<bar>\<rfloor>"
   show "1 \<le> round_down (int prec + \<lfloor>log 2 \<bar>x\<bar>\<rfloor> - \<lfloor>log 2 \<bar>1\<bar>\<rfloor>) (1 / x) "
   proof cases
@@ -1203,35 +1236,71 @@
   qed
 qed
 
-lemma float_divr: "real x / real y \<le> real (float_divr prec x y)"
-  using round_up by transfer simp
+lemma float_divl_pos_less1_bound:
+  "0 < real x \<Longrightarrow> real x < 1 \<Longrightarrow> prec \<ge> 1 \<Longrightarrow> 1 \<le> real (float_divl prec 1 x)"
+  by (transfer, rule real_divl_pos_less1_bound)
 
-lemma float_divr_pos_less1_lower_bound: assumes "0 < x" and "x < 1" shows "1 \<le> float_divr prec 1 x"
+lemma float_divr: "real x / real y \<le> real (float_divr prec x y)"
+  by transfer (rule real_divr)
+
+lemma real_divr_pos_less1_lower_bound: assumes "0 < x" and "x < 1" shows "1 \<le> real_divr prec 1 x"
 proof -
-  have "1 \<le> 1 / real x" using `0 < x` and `x < 1` by auto
-  also have "\<dots> \<le> real (float_divr prec 1 x)" using float_divr[where x=1 and y=x] by auto
+  have "1 \<le> 1 / x" using `0 < x` and `x < 1` by auto
+  also have "\<dots> \<le> real_divr prec 1 x" using real_divr[where x=1 and y=x] by auto
   finally show ?thesis by auto
 qed
 
+lemma float_divr_pos_less1_lower_bound: "0 < x \<Longrightarrow> x < 1 \<Longrightarrow> 1 \<le> float_divr prec 1 x"
+  by transfer (rule real_divr_pos_less1_lower_bound)
+
+lemma real_divr_nonpos_pos_upper_bound:
+  "x \<le> 0 \<Longrightarrow> 0 < y \<Longrightarrow> real_divr prec x y \<le> 0"
+  by (auto simp: field_simps mult_le_0_iff divide_le_0_iff round_up_def real_divr_def)
+
 lemma float_divr_nonpos_pos_upper_bound:
   "real x \<le> 0 \<Longrightarrow> 0 < real y \<Longrightarrow> real (float_divr prec x y) \<le> 0"
-  by transfer (auto simp: field_simps mult_le_0_iff divide_le_0_iff round_up_def)
+  by transfer (rule real_divr_nonpos_pos_upper_bound)
+
+lemma real_divr_nonneg_neg_upper_bound:
+  "0 \<le> x \<Longrightarrow> y < 0 \<Longrightarrow> real_divr prec x y \<le> 0"
+  by (auto simp: field_simps mult_le_0_iff zero_le_mult_iff divide_le_0_iff round_up_def real_divr_def)
 
 lemma float_divr_nonneg_neg_upper_bound:
   "0 \<le> real x \<Longrightarrow> real y < 0 \<Longrightarrow> real (float_divr prec x y) \<le> 0"
-  by transfer (auto simp: field_simps mult_le_0_iff zero_le_mult_iff divide_le_0_iff round_up_def)
+  by transfer (rule real_divr_nonneg_neg_upper_bound)
+
+definition truncate_down::"nat \<Rightarrow> real \<Rightarrow> real" where
+  "truncate_down prec x = round_down (prec - \<lfloor>log 2 \<bar>x\<bar>\<rfloor> - 1) x"
+
+lemma truncate_down: "truncate_down prec x \<le> x"
+  using round_down by (simp add: truncate_down_def)
+
+lemma truncate_down_le: "x \<le> y \<Longrightarrow> truncate_down prec x \<le> y"
+  by (rule order_trans[OF truncate_down])
 
-lift_definition float_round_up :: "nat \<Rightarrow> float \<Rightarrow> float" is
-  "\<lambda>(prec::nat) x. round_up (prec - \<lfloor>log 2 \<bar>x\<bar>\<rfloor> - 1) x" by simp
+definition truncate_up::"nat \<Rightarrow> real \<Rightarrow> real" where
+  "truncate_up prec x = round_up (prec - \<lfloor>log 2 \<bar>x\<bar>\<rfloor> - 1) x"
+
+lemma truncate_up: "x \<le> truncate_up prec x"
+  using round_up by (simp add: truncate_up_def)
+
+lemma truncate_up_le: "x \<le> y \<Longrightarrow> x \<le> truncate_up prec y"
+  by (rule order_trans[OF _ truncate_up])
+
+lemma truncate_up_zero[simp]: "truncate_up prec 0 = 0"
+  by (simp add: truncate_up_def)
+
+lift_definition float_round_up :: "nat \<Rightarrow> float \<Rightarrow> float" is truncate_up
+  by (simp add: truncate_up_def)
 
 lemma float_round_up: "real x \<le> real (float_round_up prec x)"
-  using round_up by transfer simp
+  using truncate_up by transfer simp
 
-lift_definition float_round_down :: "nat \<Rightarrow> float \<Rightarrow> float" is
-  "\<lambda>(prec::nat) x. round_down (prec - \<lfloor>log 2 \<bar>x\<bar>\<rfloor> - 1) x" by simp
+lift_definition float_round_down :: "nat \<Rightarrow> float \<Rightarrow> float" is truncate_down
+  by (simp add: truncate_down_def)
 
 lemma float_round_down: "real (float_round_down prec x) \<le> real x"
-  using round_down by transfer simp
+  using truncate_down by transfer simp
 
 lemma floor_add2[simp]: "\<lfloor> real i + x \<rfloor> = i + \<lfloor> x \<rfloor>"
   using floor_add[of x i] by (simp del: floor_add add: ac_simps)
@@ -1241,7 +1310,8 @@
     if 0 < d then let P = 2^nat d ; n = m div P in Float n (e + d)
              else Float m e)"
   using Float.compute_float_down[of "prec - bitlen \<bar>m\<bar> - e" m e, symmetric]
-  by transfer (simp add: field_simps abs_mult log_mult bitlen_def cong del: if_weak_cong)
+  by transfer (simp add: field_simps abs_mult log_mult bitlen_def truncate_down_def
+    cong del: if_weak_cong)
 hide_fact (open) compute_float_round_down
 
 lemma compute_float_round_up[code]:
@@ -1251,7 +1321,8 @@
               else Float m e)"
   using Float.compute_float_up[of "prec - bitlen \<bar>m\<bar> - e" m e, symmetric]
   unfolding Let_def
-  by transfer (simp add: field_simps abs_mult log_mult bitlen_def cong del: if_weak_cong)
+  by transfer (simp add: field_simps abs_mult log_mult bitlen_def truncate_up_def
+    cong del: if_weak_cong)
 hide_fact (open) compute_float_round_up
 
 lemma Float_le_zero_iff: "Float a b \<le> 0 \<longleftrightarrow> a \<le> 0"