src/HOL/Library/Float.thy
changeset 45495 c55a07526dbe
parent 44766 d4d33a4d7548
child 45772 8a8f78ce0dcf
     1.1 --- a/src/HOL/Library/Float.thy	Mon Nov 14 12:28:34 2011 +0100
     1.2 +++ b/src/HOL/Library/Float.thy	Mon Nov 14 18:36:31 2011 +0100
     1.3 @@ -72,78 +72,19 @@
     1.4  lemma pow2_1[simp]: "pow2 1 = 2" by simp
     1.5  lemma pow2_neg: "pow2 x = inverse (pow2 (-x))" by simp
     1.6  
     1.7 -declare pow2_def[simp del]
     1.8 +lemma pow2_powr: "pow2 a = 2 powr a"
     1.9 +  by (simp add: powr_realpow[symmetric] powr_minus)
    1.10  
    1.11 -lemma pow2_add1: "pow2 (1 + a) = 2 * (pow2 a)"
    1.12 -proof -
    1.13 -  have h: "! n. nat (2 + int n) - Suc 0 = nat (1 + int n)" by arith
    1.14 -  have g: "! a b. a - -1 = a + (1::int)" by arith
    1.15 -  have pos: "! n. pow2 (int n + 1) = 2 * pow2 (int n)"
    1.16 -    apply (auto, induct_tac n)
    1.17 -    apply (simp_all add: pow2_def)
    1.18 -    apply (rule_tac m1="2" and n1="nat (2 + int na)" in ssubst[OF realpow_num_eq_if])
    1.19 -    by (auto simp add: h)
    1.20 -  show ?thesis
    1.21 -  proof (induct a)
    1.22 -    case (nonneg n)
    1.23 -    from pos show ?case by (simp add: algebra_simps)
    1.24 -  next
    1.25 -    case (neg n)
    1.26 -    show ?case
    1.27 -      apply (auto)
    1.28 -      apply (subst pow2_neg[of "- int n"])
    1.29 -      apply (subst pow2_neg[of "-1 - int n"])
    1.30 -      apply (auto simp add: g pos)
    1.31 -      done
    1.32 -  qed
    1.33 -qed
    1.34 +declare pow2_def[simp del]
    1.35  
    1.36  lemma pow2_add: "pow2 (a+b) = (pow2 a) * (pow2 b)"
    1.37 -proof (induct b)
    1.38 -  case (nonneg n)
    1.39 -  show ?case
    1.40 -  proof (induct n)
    1.41 -    case 0
    1.42 -    show ?case by simp
    1.43 -  next
    1.44 -    case (Suc m)
    1.45 -    then show ?case by (auto simp add: algebra_simps pow2_add1)
    1.46 -  qed
    1.47 -next
    1.48 -  case (neg n)
    1.49 -  show ?case
    1.50 -  proof (induct n)
    1.51 -    case 0
    1.52 -    show ?case
    1.53 -      apply (auto)
    1.54 -      apply (subst pow2_neg[of "a + -1"])
    1.55 -      apply (subst pow2_neg[of "-1"])
    1.56 -      apply (simp)
    1.57 -      apply (insert pow2_add1[of "-a"])
    1.58 -      apply (simp add: algebra_simps)
    1.59 -      apply (subst pow2_neg[of "-a"])
    1.60 -      apply (simp)
    1.61 -      done
    1.62 -  next
    1.63 -    case (Suc m)
    1.64 -    have a: "int m - (a + -2) =  1 + (int m - a + 1)" by arith
    1.65 -    have b: "int m - -2 = 1 + (int m + 1)" by arith
    1.66 -    show ?case
    1.67 -      apply (auto)
    1.68 -      apply (subst pow2_neg[of "a + (-2 - int m)"])
    1.69 -      apply (subst pow2_neg[of "-2 - int m"])
    1.70 -      apply (auto simp add: algebra_simps)
    1.71 -      apply (subst a)
    1.72 -      apply (subst b)
    1.73 -      apply (simp only: pow2_add1)
    1.74 -      apply (subst pow2_neg[of "int m - a + 1"])
    1.75 -      apply (subst pow2_neg[of "int m + 1"])
    1.76 -      apply auto
    1.77 -      apply (insert Suc)
    1.78 -      apply (auto simp add: algebra_simps)
    1.79 -      done
    1.80 -  qed
    1.81 -qed
    1.82 +  by (simp add: pow2_powr powr_add)
    1.83 +
    1.84 +lemma pow2_diff: "pow2 (a - b) = pow2 a / pow2 b"
    1.85 +  by (simp add: pow2_powr powr_divide2)
    1.86 +  
    1.87 +lemma pow2_add1: "pow2 (1 + a) = 2 * (pow2 a)"
    1.88 +  by (simp add: pow2_add)
    1.89  
    1.90  lemma float_components[simp]: "Float (mantissa f) (scale f) = f" by (cases f) auto
    1.91  
    1.92 @@ -185,23 +126,7 @@
    1.93  
    1.94  lemma zero_less_pow2[simp]:
    1.95    "0 < pow2 x"
    1.96 -proof -
    1.97 -  {
    1.98 -    fix y
    1.99 -    have "0 <= y \<Longrightarrow> 0 < pow2 y"
   1.100 -      apply (induct y)
   1.101 -      apply (induct_tac n)
   1.102 -      apply (simp_all add: pow2_add)
   1.103 -      done
   1.104 -  }
   1.105 -  note helper=this
   1.106 -  show ?thesis
   1.107 -    apply (case_tac "0 <= x")
   1.108 -    apply (simp add: helper)
   1.109 -    apply (subst pow2_neg)
   1.110 -    apply (simp add: helper)
   1.111 -    done
   1.112 -qed
   1.113 +  by (simp add: pow2_powr)
   1.114  
   1.115  lemma normfloat_imp_odd_or_zero: "normfloat f = Float a b \<Longrightarrow> odd a \<or> (a = 0 \<and> b = 0)"
   1.116  proof (induct f rule: normfloat.induct)
   1.117 @@ -245,46 +170,19 @@
   1.118    and floateq: "real (Float a b) = real (Float a' b')"
   1.119    shows "b \<le> b'"
   1.120  proof - 
   1.121 +  from odd have "a' \<noteq> 0" by auto
   1.122 +  with floateq have a': "real a' = real a * pow2 (b - b')"
   1.123 +    by (simp add: pow2_diff field_simps)
   1.124 +
   1.125    {
   1.126      assume bcmp: "b > b'"
   1.127 -    from floateq have eq: "real a * pow2 b = real a' * pow2 b'" by simp
   1.128 -    {
   1.129 -      fix x y z :: real
   1.130 -      assume "y \<noteq> 0"
   1.131 -      then have "(x * inverse y = z) = (x = z * y)"
   1.132 -        by auto
   1.133 -    }
   1.134 -    note inverse = this
   1.135 -    have eq': "real a * (pow2 (b - b')) = real a'"
   1.136 -      apply (subst diff_int_def)
   1.137 -      apply (subst pow2_add)
   1.138 -      apply (subst pow2_neg[where x = "-b'"])
   1.139 -      apply simp
   1.140 -      apply (subst mult_assoc[symmetric])
   1.141 -      apply (subst inverse)
   1.142 -      apply (simp_all add: eq)
   1.143 -      done
   1.144 -    have "\<exists> z > 0. pow2 (b-b') = 2^z"
   1.145 -      apply (rule exI[where x="nat (b - b')"])
   1.146 -      apply (auto)
   1.147 -      apply (insert bcmp)
   1.148 -      apply simp
   1.149 -      apply (subst pow2_int[symmetric])
   1.150 -      apply auto
   1.151 -      done
   1.152 -    then obtain z where z: "z > 0 \<and> pow2 (b-b') = 2^z" by auto
   1.153 -    with eq' have "real a * 2^z = real a'"
   1.154 -      by auto
   1.155 -    then have "real a * real ((2::int)^z) = real a'"
   1.156 -      by auto
   1.157 -    then have "real (a * 2^z) = real a'"
   1.158 -      apply (subst real_of_int_mult)
   1.159 -      apply simp
   1.160 -      done
   1.161 -    then have a'_rep: "a * 2^z = a'" by arith
   1.162 -    then have "a' = a*2^z" by simp
   1.163 -    with z have "even a'" by simp
   1.164 -    with odd have False by auto
   1.165 +    then have "\<exists>c::nat. b - b' = int c + 1"
   1.166 +      by arith
   1.167 +    then guess c ..
   1.168 +    with a' have "real a' = real (a * 2^c * 2)"
   1.169 +      by (simp add: pow2_def nat_add_distrib)
   1.170 +    with odd have False
   1.171 +      unfolding real_of_int_inject by simp
   1.172    }
   1.173    then show ?thesis by arith
   1.174  qed