src/HOL/Library/Float.thy
changeset 60017 b785d6d06430
parent 59984 4f1eccec320c
child 60376 528a48f4ad87
     1.1 --- a/src/HOL/Library/Float.thy	Thu Apr 09 20:42:38 2015 +0200
     1.2 +++ b/src/HOL/Library/Float.thy	Sat Apr 11 11:56:40 2015 +0100
     1.3 @@ -82,16 +82,18 @@
     1.4  lemma uminus_float[simp]: "x \<in> float \<Longrightarrow> -x \<in> float"
     1.5    apply (auto simp: float_def)
     1.6    apply hypsubst_thin
     1.7 -  apply (rule_tac x="-x" in exI)
     1.8 -  apply (rule_tac x="xa" in exI)
     1.9 +  apply (rename_tac m e)
    1.10 +  apply (rule_tac x="-m" in exI)
    1.11 +  apply (rule_tac x="e" in exI)
    1.12    apply (simp add: field_simps)
    1.13    done
    1.14  
    1.15  lemma times_float[simp]: "x \<in> float \<Longrightarrow> y \<in> float \<Longrightarrow> x * y \<in> float"
    1.16    apply (auto simp: float_def)
    1.17    apply hypsubst_thin
    1.18 -  apply (rule_tac x="x * xa" in exI)
    1.19 -  apply (rule_tac x="xb + xc" in exI)
    1.20 +  apply (rename_tac mx my ex ey)
    1.21 +  apply (rule_tac x="mx * my" in exI)
    1.22 +  apply (rule_tac x="ex + ey" in exI)
    1.23    apply (simp add: powr_add)
    1.24    done
    1.25  
    1.26 @@ -107,16 +109,18 @@
    1.27  lemma div_power_2_float[simp]: "x \<in> float \<Longrightarrow> x / 2^d \<in> float"
    1.28    apply (auto simp add: float_def)
    1.29    apply hypsubst_thin
    1.30 -  apply (rule_tac x="x" in exI)
    1.31 -  apply (rule_tac x="xa - d" in exI)
    1.32 +  apply (rename_tac m e)
    1.33 +  apply (rule_tac x="m" in exI)
    1.34 +  apply (rule_tac x="e - d" in exI)
    1.35    apply (simp add: powr_realpow[symmetric] field_simps powr_add[symmetric])
    1.36    done
    1.37  
    1.38  lemma div_power_2_int_float[simp]: "x \<in> float \<Longrightarrow> x / (2::int)^d \<in> float"
    1.39    apply (auto simp add: float_def)
    1.40    apply hypsubst_thin
    1.41 -  apply (rule_tac x="x" in exI)
    1.42 -  apply (rule_tac x="xa - d" in exI)
    1.43 +  apply (rename_tac m e)
    1.44 +  apply (rule_tac x="m" in exI)
    1.45 +  apply (rule_tac x="e - d" in exI)
    1.46    apply (simp add: powr_realpow[symmetric] field_simps powr_add[symmetric])
    1.47    done
    1.48  
    1.49 @@ -687,8 +691,9 @@
    1.50  
    1.51    from neg have "2 powr real p \<le> 2 powr 0"
    1.52      by (intro powr_mono) auto
    1.53 -  also have "\<dots> \<le> \<lfloor>2 powr 0\<rfloor>" by simp
    1.54 -  also have "\<dots> \<le> \<lfloor>x * 2 powr real p\<rfloor>" unfolding real_of_int_le_iff
    1.55 +  also have "\<dots> \<le> \<lfloor>2 powr 0::real\<rfloor>" by simp
    1.56 +  also have "... \<le> \<lfloor>x * 2 powr (real p)\<rfloor>" 
    1.57 +    unfolding real_of_int_le_iff
    1.58      using x x_le by (intro floor_mono) (simp add: powr_minus_divide field_simps)
    1.59    finally show ?thesis
    1.60      using prec x
    1.61 @@ -723,7 +728,7 @@
    1.62  proof
    1.63    have "round_up e f - f \<le> round_up e f - round_down e f" using round_down by simp
    1.64    also have "\<dots> \<le> 2 powr -e" using round_up_diff_round_down by simp
    1.65 -  finally show "round_up e f - f \<le> 2 powr real (- e)"
    1.66 +  finally show "round_up e f - f \<le> 2 powr - (real e)"
    1.67      by simp
    1.68  qed (simp add: algebra_simps round_up)
    1.69  
    1.70 @@ -740,7 +745,7 @@
    1.71  proof
    1.72    have "f - round_down e f \<le> round_up e f - round_down e f" using round_up by simp
    1.73    also have "\<dots> \<le> 2 powr -e" using round_up_diff_round_down by simp
    1.74 -  finally show "f - round_down e f \<le> 2 powr real (- e)"
    1.75 +  finally show "f - round_down e f \<le> 2 powr - (real e)"
    1.76      by simp
    1.77  qed (simp add: algebra_simps round_down)
    1.78  
    1.79 @@ -923,8 +928,9 @@
    1.80    shows "0 \<le> e + (bitlen m - 1)"
    1.81  proof -
    1.82    have "0 < Float m e" using assms by auto
    1.83 -  hence "0 < m" using powr_gt_zero[of 2 e]
    1.84 -    by (auto simp: zero_less_mult_iff)
    1.85 +  hence "0 < m" using powr_gt_zero[of 2 e]  
    1.86 +    apply (auto simp: zero_less_mult_iff)
    1.87 +    using not_le powr_ge_pzero by blast
    1.88    hence "m \<noteq> 0" by auto
    1.89    show ?thesis
    1.90    proof (cases "0 \<le> e")
    1.91 @@ -2017,8 +2023,7 @@
    1.92    by (simp add: truncate_up_eq_truncate_down truncate_down_mono)
    1.93  
    1.94  lemma Float_le_zero_iff: "Float a b \<le> 0 \<longleftrightarrow> a \<le> 0"
    1.95 - apply (auto simp: zero_float_def mult_le_0_iff)
    1.96 - using powr_gt_zero[of 2 b] by simp
    1.97 + by (auto simp: zero_float_def mult_le_0_iff) (simp add: not_less [symmetric])
    1.98  
    1.99  lemma real_of_float_pprt[simp]: fixes a::float shows "real (pprt a) = pprt (real a)"
   1.100    unfolding pprt_def sup_float_def max_def sup_real_def by auto