1.1 --- a/src/HOL/Real/Float.thy	Fri Aug 17 00:03:50 2007 +0200
     1.2 +++ b/src/HOL/Real/Float.thy	Fri Aug 17 09:19:53 2007 +0200
     1.3 @@ -320,6 +320,12 @@
     1.4  lemma pow2_int: "pow2 (int n) = 2^n"
     1.5    by (simp add: pow2_def)
     1.6  
     1.7 +lemma float_add_l0: "float (0, e) + x = x"
     1.8 +  by (simp add: float_def)
     1.9 +
    1.10 +lemma float_add_r0: "x + float (0, e) = x"
    1.11 +  by (simp add: float_def)
    1.12 +
    1.13  lemma float_add:
    1.14    "float (a1, e1) + float (a2, e2) =
    1.15    (if e1<=e2 then float (a1+a2*2^(nat(e2-e1)), e1)
    1.16 @@ -328,6 +334,44 @@
    1.17    apply (auto simp add: pow2_int[symmetric] pow2_add[symmetric])
    1.18    done
    1.19  
    1.20 +lemma float_add_assoc1:
    1.21 +  "(x + float (y1, e1)) + float (y2, e2) = (float (y1, e1) + float (y2, e2)) + x"
    1.22 +  by simp
    1.23 +
    1.24 +lemma float_add_assoc2:
    1.25 +  "(float (y1, e1) + x) + float (y2, e2) = (float (y1, e1) + float (y2, e2)) + x"
    1.26 +  by simp
    1.27 +
    1.28 +lemma float_add_assoc3:
    1.29 +  "float (y1, e1) + (x + float (y2, e2)) = (float (y1, e1) + float (y2, e2)) + x"
    1.30 +  by simp
    1.31 +
    1.32 +lemma float_add_assoc4:
    1.33 +  "float (y1, e1) + (float (y2, e2) + x) = (float (y1, e1) + float (y2, e2)) + x"
    1.34 +  by simp
    1.35 +
    1.36 +lemma float_mult_l0: "float (0, e) * x = float (0, 0)"
    1.37 +  by (simp add: float_def)
    1.38 +
    1.39 +lemma float_mult_r0: "x * float (0, e) = float (0, 0)"
    1.40 +  by (simp add: float_def)
    1.41 +
    1.42 +definition 
    1.43 +  lbound :: "real \<Rightarrow> real"
    1.44 +where
    1.45 +  "lbound x = min 0 x"
    1.46 +
    1.47 +definition
    1.48 +  ubound :: "real \<Rightarrow> real"
    1.49 +where
    1.50 +  "ubound x = max 0 x"
    1.51 +
    1.52 +lemma lbound: "lbound x \<le> x"   
    1.53 +  by (simp add: lbound_def)
    1.54 +
    1.55 +lemma ubound: "x \<le> ubound x"
    1.56 +  by (simp add: ubound_def)
    1.57 +
    1.58  lemma float_mult:
    1.59    "float (a1, e1) * float (a2, e2) =
    1.60    (float (a1 * a2, e1 + e2))"
    1.61 @@ -384,6 +428,18 @@
    1.62    "pprt (float (a, b)) = (if 0 <= a then (float (a,b)) else (float (0, b)))"
    1.63    by (auto simp add: zero_le_float float_le_zero float_zero)
    1.64  
    1.65 +lemma pprt_lbound: "pprt (lbound x) = float (0, 0)"
    1.66 +  apply (simp add: float_def)
    1.67 +  apply (rule pprt_eq_0)
    1.68 +  apply (simp add: lbound_def)
    1.69 +  done
    1.70 +
    1.71 +lemma nprt_ubound: "nprt (ubound x) = float (0, 0)"
    1.72 +  apply (simp add: float_def)
    1.73 +  apply (rule nprt_eq_0)
    1.74 +  apply (simp add: ubound_def)
    1.75 +  done
    1.76 +
    1.77  lemma float_nprt:
    1.78    "nprt (float (a, b)) = (if 0 <= a then (float (0,b)) else (float (a, b)))"
    1.79    by (auto simp add: zero_le_float float_le_zero float_zero)
    1.80 @@ -513,7 +569,8 @@
    1.81    zpower_number_of_odd[simplified zero_eq_Numeral0_nring one_eq_Numeral1_nring]
    1.82    zpower_Pls zpower_Min
    1.83  
    1.84 -lemmas floatarith[simplified norm_0_1] = float_add float_mult float_minus float_abs zero_le_float float_pprt float_nprt
    1.85 +lemmas floatarith[simplified norm_0_1] = float_add float_add_l0 float_add_r0 float_mult float_mult_l0 float_mult_r0 
    1.86 +          float_minus float_abs zero_le_float float_pprt float_nprt pprt_lbound nprt_ubound float_add_assoc1 float_add_assoc2
    1.87  
    1.88  (* for use with the compute oracle *)
    1.89  lemmas arith = binarith intarith intarithrel natarith powerarith floatarith not_false_eq_true not_true_eq_false