src/HOL/Library/Float.thy
changeset 41528 276078f01ada
parent 41024 ba961a606c67
child 42676 8724f20bf69c
     1.1 --- a/src/HOL/Library/Float.thy	Wed Jan 12 16:41:49 2011 +0100
     1.2 +++ b/src/HOL/Library/Float.thy	Wed Jan 12 17:14:27 2011 +0100
     1.3 @@ -66,7 +66,7 @@
     1.4    by (simp only:number_of_float_def Float_num[unfolded number_of_is_id])
     1.5  
     1.6  lemma float_number_of_int[simp]: "real (Float n 0) = real n"
     1.7 -  by (simp add: Float_num[unfolded number_of_is_id] real_of_float_simp pow2_def)
     1.8 +  by simp
     1.9  
    1.10  lemma pow2_0[simp]: "pow2 0 = 1" by simp
    1.11  lemma pow2_1[simp]: "pow2 1 = 2" by simp
    1.12 @@ -107,7 +107,7 @@
    1.13      show ?case by simp
    1.14    next
    1.15      case (Suc m)
    1.16 -    show ?case by (auto simp add: algebra_simps pow2_add1 prems)
    1.17 +    then show ?case by (auto simp add: algebra_simps pow2_add1)
    1.18    qed
    1.19  next
    1.20    case (2 n)
    1.21 @@ -124,6 +124,7 @@
    1.22        apply (subst pow2_neg[of "-a"])
    1.23        apply (simp)
    1.24        done
    1.25 +  next
    1.26      case (Suc m)
    1.27      have a: "int m - (a + -2) =  1 + (int m - a + 1)" by arith
    1.28      have b: "int m - -2 = 1 + (int m + 1)" by arith
    1.29 @@ -138,15 +139,15 @@
    1.30        apply (subst pow2_neg[of "int m - a + 1"])
    1.31        apply (subst pow2_neg[of "int m + 1"])
    1.32        apply auto
    1.33 -      apply (insert prems)
    1.34 +      apply (insert Suc)
    1.35        apply (auto simp add: algebra_simps)
    1.36        done
    1.37    qed
    1.38  qed
    1.39  
    1.40 -lemma float_components[simp]: "Float (mantissa f) (scale f) = f" by (cases f, auto)
    1.41 +lemma float_components[simp]: "Float (mantissa f) (scale f) = f" by (cases f) auto
    1.42  
    1.43 -lemma float_split: "\<exists> a b. x = Float a b" by (cases x, auto)
    1.44 +lemma float_split: "\<exists> a b. x = Float a b" by (cases x) auto
    1.45  
    1.46  lemma float_split2: "(\<forall> a b. x \<noteq> Float a b) = False" by (auto simp add: float_split)
    1.47  
    1.48 @@ -156,7 +157,9 @@
    1.49  by arith
    1.50  
    1.51  function normfloat :: "float \<Rightarrow> float" where
    1.52 -"normfloat (Float a b) = (if a \<noteq> 0 \<and> even a then normfloat (Float (a div 2) (b+1)) else if a=0 then Float 0 0 else Float a b)"
    1.53 +  "normfloat (Float a b) =
    1.54 +    (if a \<noteq> 0 \<and> even a then normfloat (Float (a div 2) (b+1))
    1.55 +     else if a=0 then Float 0 0 else Float a b)"
    1.56  by pat_completeness auto
    1.57  termination by (relation "measure (nat o abs o mantissa)") (auto intro: abs_div_2_less)
    1.58  declare normfloat.simps[simp del]
    1.59 @@ -168,7 +171,7 @@
    1.60      by auto
    1.61    show ?case
    1.62      apply (subst normfloat.simps)
    1.63 -    apply (auto simp add: float_zero)
    1.64 +    apply auto
    1.65      apply (subst 1[symmetric])
    1.66      apply (auto simp add: pow2_add even_def)
    1.67      done
    1.68 @@ -186,7 +189,10 @@
    1.69    {
    1.70      fix y
    1.71      have "0 <= y \<Longrightarrow> 0 < pow2 y"
    1.72 -      by (induct y, induct_tac n, simp_all add: pow2_add)
    1.73 +      apply (induct y)
    1.74 +      apply (induct_tac n)
    1.75 +      apply (simp_all add: pow2_add)
    1.76 +      done
    1.77    }
    1.78    note helper=this
    1.79    show ?thesis
    1.80 @@ -292,7 +298,7 @@
    1.81    from 
    1.82       float_eq_odd_helper[OF odd2 floateq] 
    1.83       float_eq_odd_helper[OF odd1 floateq[symmetric]]
    1.84 -  have beq: "b = b'"  by arith
    1.85 +  have beq: "b = b'" by arith
    1.86    with floateq show ?thesis by auto
    1.87  qed
    1.88  
    1.89 @@ -366,17 +372,17 @@
    1.90  end
    1.91  
    1.92  lemma real_of_float_add[simp]: "real (a + b) = real a + real (b :: float)"
    1.93 -  by (cases a, cases b, simp add: algebra_simps plus_float.simps, 
    1.94 +  by (cases a, cases b) (simp add: algebra_simps plus_float.simps, 
    1.95        auto simp add: pow2_int[symmetric] pow2_add[symmetric])
    1.96  
    1.97  lemma real_of_float_minus[simp]: "real (- a) = - real (a :: float)"
    1.98 -  by (cases a, simp add: uminus_float.simps)
    1.99 +  by (cases a) (simp add: uminus_float.simps)
   1.100  
   1.101  lemma real_of_float_sub[simp]: "real (a - b) = real a - real (b :: float)"
   1.102 -  by (cases a, cases b, simp add: minus_float_def)
   1.103 +  by (cases a, cases b) (simp add: minus_float_def)
   1.104  
   1.105  lemma real_of_float_mult[simp]: "real (a*b) = real a * real (b :: float)"
   1.106 -  by (cases a, cases b, simp add: times_float.simps pow2_add)
   1.107 +  by (cases a, cases b) (simp add: times_float.simps pow2_add)
   1.108  
   1.109  lemma real_of_float_0[simp]: "real (0 :: float) = 0"
   1.110    by (auto simp add: zero_float_def float_zero)
   1.111 @@ -419,35 +425,36 @@
   1.112  declare real_of_float_simp[simp del]
   1.113  
   1.114  lemma real_of_float_pprt[simp]: "real (float_pprt a) = pprt (real a)"
   1.115 -  by (cases a, auto simp add: float_pprt.simps zero_le_float float_le_zero float_zero)
   1.116 +  by (cases a) (auto simp add: zero_le_float float_le_zero)
   1.117  
   1.118  lemma real_of_float_nprt[simp]: "real (float_nprt a) = nprt (real a)"
   1.119 -  by (cases a,  auto simp add: float_nprt.simps zero_le_float float_le_zero float_zero)
   1.120 +  by (cases a) (auto simp add: zero_le_float float_le_zero)
   1.121  
   1.122  instance float :: ab_semigroup_add
   1.123  proof (intro_classes)
   1.124    fix a b c :: float
   1.125    show "a + b + c = a + (b + c)"
   1.126 -    by (cases a, cases b, cases c, auto simp add: algebra_simps power_add[symmetric] plus_float.simps)
   1.127 +    by (cases a, cases b, cases c)
   1.128 +      (auto simp add: algebra_simps power_add[symmetric] plus_float.simps)
   1.129  next
   1.130    fix a b :: float
   1.131    show "a + b = b + a"
   1.132 -    by (cases a, cases b, simp add: plus_float.simps)
   1.133 +    by (cases a, cases b) (simp add: plus_float.simps)
   1.134  qed
   1.135  
   1.136  instance float :: comm_monoid_mult
   1.137  proof (intro_classes)
   1.138    fix a b c :: float
   1.139    show "a * b * c = a * (b * c)"
   1.140 -    by (cases a, cases b, cases c, simp add: times_float.simps)
   1.141 +    by (cases a, cases b, cases c) (simp add: times_float.simps)
   1.142  next
   1.143    fix a b :: float
   1.144    show "a * b = b * a"
   1.145 -    by (cases a, cases b, simp add: times_float.simps)
   1.146 +    by (cases a, cases b) (simp add: times_float.simps)
   1.147  next
   1.148    fix a :: float
   1.149    show "1 * a = a"
   1.150 -    by (cases a, simp add: times_float.simps one_float_def)
   1.151 +    by (cases a) (simp add: times_float.simps one_float_def)
   1.152  qed
   1.153  
   1.154  (* Floats do NOT form a cancel_semigroup_add: *)
   1.155 @@ -458,7 +465,7 @@
   1.156  proof (intro_classes)
   1.157    fix a b c :: float
   1.158    show "(a + b) * c = a * c + b * c"
   1.159 -    by (cases a, cases b, cases c, simp, simp add: plus_float.simps times_float.simps algebra_simps)
   1.160 +    by (cases a, cases b, cases c) (simp add: plus_float.simps times_float.simps algebra_simps)
   1.161  qed
   1.162  
   1.163  (* Floats do NOT form an order, because "(x < y) = (x <= y & x <> y)" does NOT hold *)
   1.164 @@ -903,11 +910,31 @@
   1.165    and D: "\<And>x y prec. \<lbrakk>0 \<le> x; y < 0; ps = (prec, x, y)\<rbrakk> \<Longrightarrow> P"
   1.166    shows P
   1.167  proof -
   1.168 -  obtain prec x y where [simp]: "ps = (prec, x, y)" by (cases ps, auto)
   1.169 +  obtain prec x y where [simp]: "ps = (prec, x, y)" by (cases ps) auto
   1.170    from Y have "y = 0 \<Longrightarrow> P" by auto
   1.171 -  moreover { assume "0 < y" have P proof (cases "0 \<le> x") case True with A and `0 < y` show P by auto next case False with B and `0 < y` show P by auto qed } 
   1.172 -  moreover { assume "y < 0" have P proof (cases "0 \<le> x") case True with D and `y < 0` show P by auto next case False with C and `y < 0` show P by auto qed }
   1.173 -  ultimately show P by (cases "y = 0 \<or> 0 < y \<or> y < 0", auto)
   1.174 +  moreover {
   1.175 +    assume "0 < y"
   1.176 +    have P
   1.177 +    proof (cases "0 \<le> x")
   1.178 +      case True
   1.179 +      with A and `0 < y` show P by auto
   1.180 +    next
   1.181 +      case False
   1.182 +      with B and `0 < y` show P by auto
   1.183 +    qed
   1.184 +  } 
   1.185 +  moreover {
   1.186 +    assume "y < 0"
   1.187 +    have P
   1.188 +    proof (cases "0 \<le> x")
   1.189 +      case True
   1.190 +      with D and `y < 0` show P by auto
   1.191 +    next
   1.192 +      case False
   1.193 +      with C and `y < 0` show P by auto
   1.194 +    qed
   1.195 +  }
   1.196 +  ultimately show P by (cases "y = 0 \<or> 0 < y \<or> y < 0") auto
   1.197  qed
   1.198  
   1.199  function lapprox_rat :: "nat \<Rightarrow> int \<Rightarrow> int \<Rightarrow> float"
   1.200 @@ -1011,10 +1038,14 @@
   1.201  lemma rapprox_rat_nonpos_pos: assumes "x \<le> 0" and "0 < y"
   1.202    shows "real (rapprox_rat n x y) \<le> 0"
   1.203  proof (cases "x = 0") 
   1.204 -  case True hence "0 \<le> x" by auto show ?thesis unfolding rapprox_rat.simps(2)[OF `0 \<le> x` `0 < y`]
   1.205 -    unfolding True rapprox_posrat_def Let_def by auto
   1.206 +  case True
   1.207 +  hence "0 \<le> x" by auto show ?thesis
   1.208 +    unfolding rapprox_rat.simps(2)[OF `0 \<le> x` `0 < y`]
   1.209 +    unfolding True rapprox_posrat_def Let_def
   1.210 +    by auto
   1.211  next
   1.212 -  case False hence "x < 0" using assms by auto
   1.213 +  case False
   1.214 +  hence "x < 0" using assms by auto
   1.215    show ?thesis using rapprox_rat_neg[OF `x < 0` `0 < y`] .
   1.216  qed
   1.217  
   1.218 @@ -1064,19 +1095,31 @@
   1.219  proof (cases x, cases y)
   1.220    fix xm xe ym ye :: int
   1.221    assume x_eq: "x = Float xm xe" and y_eq: "y = Float ym ye"
   1.222 -  have "0 \<le> xm" using `0 \<le> x`[unfolded x_eq le_float_def real_of_float_simp real_of_float_0 zero_le_mult_iff] by auto
   1.223 -  have "0 < ym" using `0 < y`[unfolded y_eq less_float_def real_of_float_simp real_of_float_0 zero_less_mult_iff] by auto
   1.224 +  have "0 \<le> xm"
   1.225 +    using `0 \<le> x`[unfolded x_eq le_float_def real_of_float_simp real_of_float_0 zero_le_mult_iff]
   1.226 +    by auto
   1.227 +  have "0 < ym"
   1.228 +    using `0 < y`[unfolded y_eq less_float_def real_of_float_simp real_of_float_0 zero_less_mult_iff]
   1.229 +    by auto
   1.230  
   1.231 -  have "\<And>n. 0 \<le> real (Float 1 n)" unfolding real_of_float_simp using zero_le_pow2 by auto
   1.232 -  moreover have "0 \<le> real (lapprox_rat prec xm ym)" by (rule order_trans[OF _ lapprox_rat_bottom[OF `0 \<le> xm` `0 < ym`]], auto simp add: `0 \<le> xm` pos_imp_zdiv_nonneg_iff[OF `0 < ym`])
   1.233 +  have "\<And>n. 0 \<le> real (Float 1 n)"
   1.234 +    unfolding real_of_float_simp using zero_le_pow2 by auto
   1.235 +  moreover have "0 \<le> real (lapprox_rat prec xm ym)"
   1.236 +    apply (rule order_trans[OF _ lapprox_rat_bottom[OF `0 \<le> xm` `0 < ym`]])
   1.237 +    apply (auto simp add: `0 \<le> xm` pos_imp_zdiv_nonneg_iff[OF `0 < ym`])
   1.238 +    done
   1.239    ultimately show "0 \<le> float_divl prec x y"
   1.240 -    unfolding x_eq y_eq float_divl.simps Let_def le_float_def real_of_float_0 by (auto intro!: mult_nonneg_nonneg)
   1.241 +    unfolding x_eq y_eq float_divl.simps Let_def le_float_def real_of_float_0
   1.242 +    by (auto intro!: mult_nonneg_nonneg)
   1.243  qed
   1.244  
   1.245 -lemma float_divl_pos_less1_bound: assumes "0 < x" and "x < 1" and "0 < prec" shows "1 \<le> float_divl prec 1 x"
   1.246 +lemma float_divl_pos_less1_bound:
   1.247 +  assumes "0 < x" and "x < 1" and "0 < prec"
   1.248 +  shows "1 \<le> float_divl prec 1 x"
   1.249  proof (cases x)
   1.250    case (Float m e)
   1.251 -  from `0 < x` `x < 1` have "0 < m" "e < 0" using float_pos_m_pos float_pos_less1_e_neg unfolding Float by auto
   1.252 +  from `0 < x` `x < 1` have "0 < m" "e < 0"
   1.253 +    using float_pos_m_pos float_pos_less1_e_neg unfolding Float by auto
   1.254    let ?b = "nat (bitlen m)" and ?e = "nat (-e)"
   1.255    have "1 \<le> m" and "m \<noteq> 0" using `0 < m` by auto
   1.256    with bitlen_bounds[OF `0 < m`] have "m < 2^?b" and "(2::int) \<le> 2^?b" by auto
   1.257 @@ -1087,22 +1130,29 @@
   1.258  
   1.259    from float_less1_mantissa_bound `0 < x` `x < 1` Float 
   1.260    have "m < 2^?e" by auto
   1.261 -  with bitlen_bounds[OF `0 < m`, THEN conjunct1]
   1.262 -  have "(2::int)^nat (bitlen m - 1) < 2^?e" by (rule order_le_less_trans)
   1.263 +  with bitlen_bounds[OF `0 < m`, THEN conjunct1] have "(2::int)^nat (bitlen m - 1) < 2^?e"
   1.264 +    by (rule order_le_less_trans)
   1.265    from power_less_imp_less_exp[OF _ this]
   1.266    have "bitlen m \<le> - e" by auto
   1.267    hence "(2::real)^?b \<le> 2^?e" by auto
   1.268 -  hence "(2::real)^?b * inverse (2^?b) \<le> 2^?e * inverse (2^?b)" by (rule mult_right_mono, auto)
   1.269 +  hence "(2::real)^?b * inverse (2^?b) \<le> 2^?e * inverse (2^?b)"
   1.270 +    by (rule mult_right_mono) auto
   1.271    hence "(1::real) \<le> 2^?e * inverse (2^?b)" by auto
   1.272    also
   1.273    let ?d = "real (2 ^ nat (int prec + bitlen m - 1) div m) * inverse (2 ^ nat (int prec + bitlen m - 1))"
   1.274 -  { have "2^(prec - 1) * m \<le> 2^(prec - 1) * 2^?b" using `m < 2^?b`[THEN less_imp_le] by (rule mult_left_mono, auto)
   1.275 -    also have "\<dots> = 2 ^ nat (int prec + bitlen m - 1)" unfolding pow_split zpower_zadd_distrib by auto
   1.276 -    finally have "2^(prec - 1) * m div m \<le> 2 ^ nat (int prec + bitlen m - 1) div m" using `0 < m` by (rule zdiv_mono1)
   1.277 -    hence "2^(prec - 1) \<le> 2 ^ nat (int prec + bitlen m - 1) div m" unfolding div_mult_self2_is_id[OF `m \<noteq> 0`] .
   1.278 +  {
   1.279 +    have "2^(prec - 1) * m \<le> 2^(prec - 1) * 2^?b"
   1.280 +      using `m < 2^?b`[THEN less_imp_le] by (rule mult_left_mono) auto
   1.281 +    also have "\<dots> = 2 ^ nat (int prec + bitlen m - 1)"
   1.282 +      unfolding pow_split zpower_zadd_distrib by auto
   1.283 +    finally have "2^(prec - 1) * m div m \<le> 2 ^ nat (int prec + bitlen m - 1) div m"
   1.284 +      using `0 < m` by (rule zdiv_mono1)
   1.285 +    hence "2^(prec - 1) \<le> 2 ^ nat (int prec + bitlen m - 1) div m"
   1.286 +      unfolding div_mult_self2_is_id[OF `m \<noteq> 0`] .
   1.287      hence "2^(prec - 1) * inverse (2 ^ nat (int prec + bitlen m - 1)) \<le> ?d"
   1.288 -      unfolding real_of_int_le_iff[of "2^(prec - 1)", symmetric] by auto }
   1.289 -  from mult_left_mono[OF this[unfolded pow_split power_add inverse_mult_distrib mult_assoc[symmetric] right_inverse[OF pow_not0] mult_1_left], of "2^?e"]
   1.290 +      unfolding real_of_int_le_iff[of "2^(prec - 1)", symmetric] by auto
   1.291 +  }
   1.292 +  from mult_left_mono[OF this [unfolded pow_split power_add inverse_mult_distrib mult_assoc[symmetric] right_inverse[OF pow_not0] mult_1_left], of "2^?e"]
   1.293    have "2^?e * inverse (2^?b) \<le> 2^?e * ?d" unfolding pow_split power_add by auto
   1.294    finally have "1 \<le> 2^?e * ?d" .
   1.295    
   1.296 @@ -1110,8 +1160,11 @@
   1.297    have "bitlen 1 = 1" using bitlen.simps by auto
   1.298    
   1.299    show ?thesis 
   1.300 -    unfolding one_float_def Float float_divl.simps Let_def lapprox_rat.simps(2)[OF zero_le_one `0 < m`] lapprox_posrat_def `bitlen 1 = 1`
   1.301 -    unfolding le_float_def real_of_float_mult normfloat real_of_float_simp pow2_minus pow2_int e_nat
   1.302 +    unfolding one_float_def Float float_divl.simps Let_def
   1.303 +      lapprox_rat.simps(2)[OF zero_le_one `0 < m`]
   1.304 +      lapprox_posrat_def `bitlen 1 = 1`
   1.305 +    unfolding le_float_def real_of_float_mult normfloat real_of_float_simp
   1.306 +      pow2_minus pow2_int e_nat
   1.307      using `1 \<le> 2^?e * ?d` by (auto simp add: pow2_def)
   1.308  qed
   1.309