1.1 --- a/src/HOL/Library/Float.thy	Tue Dec 06 14:18:24 2011 +0100
     1.2 +++ b/src/HOL/Library/Float.thy	Tue Dec 06 14:29:37 2011 +0100
     1.3 @@ -957,37 +957,10 @@
     1.4         f * l)"     
     1.5  
     1.6  lemma float_divl: "real (float_divl prec x y) \<le> real x / real y"
     1.7 -proof - 
     1.8 -  from float_split[of x] obtain mx sx where x: "x = Float mx sx" by auto
     1.9 -  from float_split[of y] obtain my sy where y: "y = Float my sy" by auto
    1.10 -  have "real mx / real my \<le> (real mx * pow2 sx / (real my * pow2 sy)) / (pow2 (sx - sy))"
    1.11 -    apply (case_tac "my = 0")
    1.12 -    apply simp
    1.13 -    apply (case_tac "my > 0")       
    1.14 -    apply (subst pos_le_divide_eq)
    1.15 -    apply simp
    1.16 -    apply (subst pos_le_divide_eq)
    1.17 -    apply (simp add: mult_pos_pos)
    1.18 -    apply simp
    1.19 -    apply (subst pow2_add[symmetric])
    1.20 -    apply simp
    1.21 -    apply (subgoal_tac "my < 0")
    1.22 -    apply auto
    1.23 -    apply (simp add: field_simps)
    1.24 -    apply (subst pow2_add[symmetric])
    1.25 -    apply (simp add: field_simps)
    1.26 -    done
    1.27 -  then have "real (lapprox_rat prec mx my) \<le> (real mx * pow2 sx / (real my * pow2 sy)) / (pow2 (sx - sy))"
    1.28 -    by (rule order_trans[OF lapprox_rat])
    1.29 -  then have "real (lapprox_rat prec mx my) * pow2 (sx - sy) \<le> real mx * pow2 sx / (real my * pow2 sy)"
    1.30 -    apply (subst pos_le_divide_eq[symmetric])
    1.31 -    apply simp_all
    1.32 -    done
    1.33 -  then have "pow2 (sx - sy) * real (lapprox_rat prec mx my) \<le> real mx * pow2 sx / (real my * pow2 sy)"
    1.34 -    by (simp add: algebra_simps)
    1.35 -  then show ?thesis
    1.36 -    by (simp add: x y Let_def real_of_float_simp)
    1.37 -qed
    1.38 +  using lapprox_rat[of prec "mantissa x" "mantissa y"]
    1.39 +  by (cases x y rule: float.exhaust[case_product float.exhaust])
    1.40 +     (simp split: split_if_asm
    1.41 +           add: real_of_float_simp pow2_diff field_simps le_divide_eq mult_less_0_iff zero_less_mult_iff)
    1.42  
    1.43  lemma float_divl_lower_bound: assumes "0 \<le> x" and "0 < y" shows "0 \<le> float_divl prec x y"
    1.44  proof (cases x, cases y)
    1.45 @@ -1076,34 +1049,10 @@
    1.46         f * r)"  
    1.47  
    1.48  lemma float_divr: "real x / real y \<le> real (float_divr prec x y)"
    1.49 -proof - 
    1.50 -  from float_split[of x] obtain mx sx where x: "x = Float mx sx" by auto
    1.51 -  from float_split[of y] obtain my sy where y: "y = Float my sy" by auto
    1.52 -  have "real mx / real my \<ge> (real mx * pow2 sx / (real my * pow2 sy)) / (pow2 (sx - sy))"
    1.53 -    apply (case_tac "my = 0")
    1.54 -    apply simp
    1.55 -    apply (case_tac "my > 0")
    1.56 -    apply auto
    1.57 -    apply (subst pos_divide_le_eq)
    1.58 -    apply (rule mult_pos_pos)+
    1.59 -    apply simp_all
    1.60 -    apply (subst pow2_add[symmetric])
    1.61 -    apply simp
    1.62 -    apply (subgoal_tac "my < 0")
    1.63 -    apply auto
    1.64 -    apply (simp add: field_simps)
    1.65 -    apply (subst pow2_add[symmetric])
    1.66 -    apply (simp add: field_simps)
    1.67 -    done
    1.68 -  then have "real (rapprox_rat prec mx my) \<ge> (real mx * pow2 sx / (real my * pow2 sy)) / (pow2 (sx - sy))"
    1.69 -    by (rule order_trans[OF _ rapprox_rat])
    1.70 -  then have "real (rapprox_rat prec mx my) * pow2 (sx - sy) \<ge> real mx * pow2 sx / (real my * pow2 sy)"
    1.71 -    apply (subst pos_divide_le_eq[symmetric])
    1.72 -    apply simp_all
    1.73 -    done
    1.74 -  then show ?thesis
    1.75 -    by (simp add: x y Let_def algebra_simps real_of_float_simp)
    1.76 -qed
    1.77 +  using rapprox_rat[of "mantissa x" "mantissa y" prec]
    1.78 +  by (cases x y rule: float.exhaust[case_product float.exhaust])
    1.79 +     (simp split: split_if_asm
    1.80 +           add: real_of_float_simp pow2_diff field_simps divide_le_eq mult_less_0_iff zero_less_mult_iff)
    1.81  
    1.82  lemma float_divr_pos_less1_lower_bound: assumes "0 < x" and "x < 1" shows "1 \<le> float_divr prec 1 x"
    1.83  proof -