src/HOL/Matrix/ComputeFloat.thy
changeset 41550 efa734d9b221
parent 41413 64cd30d6b0b8
child 41959 b460124855b8
     1.1 --- a/src/HOL/Matrix/ComputeFloat.thy	Fri Jan 14 15:43:04 2011 +0100
     1.2 +++ b/src/HOL/Matrix/ComputeFloat.thy	Fri Jan 14 15:44:47 2011 +0100
     1.3 @@ -57,7 +57,7 @@
     1.4      show ?case by simp
     1.5    next
     1.6      case (Suc m)
     1.7 -    show ?case by (auto simp add: algebra_simps pow2_add1 prems)
     1.8 +    show ?case by (auto simp add: algebra_simps pow2_add1 1 Suc)
     1.9    qed
    1.10  next
    1.11    case (2 n)
    1.12 @@ -88,7 +88,7 @@
    1.13        apply (subst pow2_neg[of "int m - a + 1"])
    1.14        apply (subst pow2_neg[of "int m + 1"])
    1.15        apply auto
    1.16 -      apply (insert prems)
    1.17 +      apply (insert Suc)
    1.18        apply (auto simp add: algebra_simps)
    1.19        done
    1.20    qed
    1.21 @@ -147,8 +147,8 @@
    1.22    assumes "real_is_int a" "real_is_int b"
    1.23    shows "(int_of_real (a*b)) = (int_of_real a) * (int_of_real b)"
    1.24  proof -
    1.25 -  from prems have a: "?! (a'::int). real a' = a" by (rule_tac real_is_int_rep, auto)
    1.26 -  from prems have b: "?! (b'::int). real b' = b" by (rule_tac real_is_int_rep, auto)
    1.27 +  from assms have a: "?! (a'::int). real a' = a" by (rule_tac real_is_int_rep, auto)
    1.28 +  from assms have b: "?! (b'::int). real b' = b" by (rule_tac real_is_int_rep, auto)
    1.29    from a obtain a'::int where a':"a = real a'" by auto
    1.30    from b obtain b'::int where b':"b = real b'" by auto
    1.31    have r: "real a' * real b' = real (a' * b')" by auto
    1.32 @@ -286,16 +286,16 @@
    1.33        show ?case
    1.34        proof cases
    1.35          assume u: "u \<noteq> 0 \<and> even u"
    1.36 -        with prems have ind: "float (u div 2, v + 1) = float (norm_float (u div 2) (v + 1))" by auto
    1.37 +        with 1 have ind: "float (u div 2, v + 1) = float (norm_float (u div 2) (v + 1))" by auto
    1.38          with u have "float (u,v) = float (u div 2, v+1)" by (simp add: float_transfer_even)
    1.39          then show ?thesis
    1.40            apply (subst norm_float.simps)
    1.41            apply (simp add: ind)
    1.42            done
    1.43        next
    1.44 -        assume "~(u \<noteq> 0 \<and> even u)"
    1.45 -        then show ?thesis
    1.46 -          by (simp add: prems float_def)
    1.47 +        assume nu: "~(u \<noteq> 0 \<and> even u)"
    1.48 +        show ?thesis
    1.49 +          by (simp add: nu float_def)
    1.50        qed
    1.51      qed
    1.52    }