--- a/src/HOL/Library/Float.thy Sun Jan 18 13:58:17 2009 +0100
+++ b/src/HOL/Library/Float.thy Wed Jan 28 16:29:16 2009 +0100
@@ -38,7 +38,7 @@
show ?thesis
proof (induct a)
case (1 n)
- from pos show ?case by (simp add: ring_simps)
+ from pos show ?case by (simp add: algebra_simps)
next
case (2 n)
show ?case
@@ -59,7 +59,7 @@
show ?case by simp
next
case (Suc m)
- show ?case by (auto simp add: ring_simps pow2_add1 prems)
+ show ?case by (auto simp add: algebra_simps pow2_add1 prems)
qed
next
case (2 n)
@@ -72,7 +72,7 @@
apply (subst pow2_neg[of "-1"])
apply (simp)
apply (insert pow2_add1[of "-a"])
- apply (simp add: ring_simps)
+ apply (simp add: algebra_simps)
apply (subst pow2_neg[of "-a"])
apply (simp)
done
@@ -83,7 +83,7 @@
apply (auto)
apply (subst pow2_neg[of "a + (-2 - int m)"])
apply (subst pow2_neg[of "-2 - int m"])
- apply (auto simp add: ring_simps)
+ apply (auto simp add: algebra_simps)
apply (subst a)
apply (subst b)
apply (simp only: pow2_add1)
@@ -91,13 +91,13 @@
apply (subst pow2_neg[of "int m + 1"])
apply auto
apply (insert prems)
- apply (auto simp add: ring_simps)
+ apply (auto simp add: algebra_simps)
done
qed
qed
lemma "float (a, e) + float (b, e) = float (a + b, e)"
-by (simp add: float_def ring_simps)
+by (simp add: float_def algebra_simps)
definition
int_of_real :: "real \<Rightarrow> int" where
@@ -254,7 +254,7 @@
lemma float_transfer_even: "even a \<Longrightarrow> float (a, b) = float (a div 2, b+1)"
apply (subst float_transfer[where a="a" and b="b" and c="-1", simplified])
- apply (simp_all add: pow2_def even_def real_is_int_def ring_simps)
+ apply (simp_all add: pow2_def even_def real_is_int_def algebra_simps)
apply (auto)
proof -
fix q::int
@@ -319,7 +319,7 @@
"float (a1, e1) + float (a2, e2) =
(if e1<=e2 then float (a1+a2*2^(nat(e2-e1)), e1)
else float (a1*2^(nat (e1-e2))+a2, e2))"
- apply (simp add: float_def ring_simps)
+ apply (simp add: float_def algebra_simps)
apply (auto simp add: pow2_int[symmetric] pow2_add[symmetric])
done