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.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.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.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.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.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.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
```