--- a/src/HOL/Archimedean_Field.thy Fri Aug 05 10:05:50 2016 +0200
+++ b/src/HOL/Archimedean_Field.thy Fri Aug 05 12:27:51 2016 +0200
@@ -342,17 +342,17 @@
text \<open>Addition and subtraction of integers.\<close>
-lemma floor_add_of_int [simp]: "\<lfloor>x + of_int z\<rfloor> = \<lfloor>x\<rfloor> + z"
- using floor_correct [of x] by (simp add: floor_unique)
+lemma floor_add_int: "\<lfloor>x\<rfloor> + z = \<lfloor>x + of_int z\<rfloor>"
+ using floor_correct [of x] by (simp add: floor_unique[symmetric])
-lemma floor_add_numeral [simp]: "\<lfloor>x + numeral v\<rfloor> = \<lfloor>x\<rfloor> + numeral v"
- using floor_add_of_int [of x "numeral v"] by simp
+lemma int_add_floor: "z + \<lfloor>x\<rfloor> = \<lfloor>of_int z + x\<rfloor>"
+ using floor_correct [of x] by (simp add: floor_unique[symmetric])
-lemma floor_add_one [simp]: "\<lfloor>x + 1\<rfloor> = \<lfloor>x\<rfloor> + 1"
- using floor_add_of_int [of x 1] by simp
+lemma one_add_floor: "\<lfloor>x\<rfloor> + 1 = \<lfloor>x + 1\<rfloor>"
+ using floor_add_int [of x 1] by simp
lemma floor_diff_of_int [simp]: "\<lfloor>x - of_int z\<rfloor> = \<lfloor>x\<rfloor> - z"
- using floor_add_of_int [of x "- z"] by (simp add: algebra_simps)
+ using floor_add_int [of x "- z"] by (simp add: algebra_simps)
lemma floor_uminus_of_int [simp]: "\<lfloor>- (of_int z)\<rfloor> = - z"
by (metis floor_diff_of_int [of 0] diff_0 floor_zero)
@@ -414,7 +414,7 @@
then have "\<lfloor>of_int k / of_int l :: 'a\<rfloor> = \<lfloor>of_int (k mod l) / of_int l + of_int (k div l) :: 'a\<rfloor>"
by (simp add: ac_simps)
then have "\<lfloor>of_int k / of_int l :: 'a\<rfloor> = \<lfloor>of_int (k mod l) / of_int l :: 'a\<rfloor> + k div l"
- by simp
+ by (simp add: floor_add_int)
with * show ?thesis
by simp
qed
@@ -444,7 +444,7 @@
by simp
ultimately have "\<lfloor>of_nat m / of_nat n :: 'a\<rfloor> =
\<lfloor>of_nat (m mod n) / of_nat n :: 'a\<rfloor> + of_nat (m div n)"
- by (simp only: floor_add_of_int)
+ by (simp only: floor_add_int)
with * show ?thesis
by simp
qed
@@ -629,17 +629,15 @@
lemma floor_add: "\<lfloor>x + y\<rfloor> = (if frac x + frac y < 1 then \<lfloor>x\<rfloor> + \<lfloor>y\<rfloor> else (\<lfloor>x\<rfloor> + \<lfloor>y\<rfloor>) + 1)"
proof -
- have "\<lfloor>x + y\<rfloor> = \<lfloor>x\<rfloor> + \<lfloor>y\<rfloor>" if "x + y < 1 + (of_int \<lfloor>x\<rfloor> + of_int \<lfloor>y\<rfloor>)"
- using that by (metis add.commute floor_unique le_floor_add le_floor_iff of_int_add)
+ have "x + y < 1 + (of_int \<lfloor>x\<rfloor> + of_int \<lfloor>y\<rfloor>) \<Longrightarrow> \<lfloor>x + y\<rfloor> = \<lfloor>x\<rfloor> + \<lfloor>y\<rfloor>"
+ by (metis add.commute floor_unique le_floor_add le_floor_iff of_int_add)
moreover
- have "\<lfloor>x + y\<rfloor> = 1 + (\<lfloor>x\<rfloor> + \<lfloor>y\<rfloor>)" if "\<not> x + y < 1 + (of_int \<lfloor>x\<rfloor> + of_int \<lfloor>y\<rfloor>)"
- using that
+ have "\<not> x + y < 1 + (of_int \<lfloor>x\<rfloor> + of_int \<lfloor>y\<rfloor>) \<Longrightarrow> \<lfloor>x + y\<rfloor> = 1 + (\<lfloor>x\<rfloor> + \<lfloor>y\<rfloor>)"
apply (simp add: floor_unique_iff)
apply (auto simp add: algebra_simps)
apply linarith
done
- ultimately show ?thesis
- by (auto simp add: frac_def algebra_simps)
+ ultimately show ?thesis by (auto simp add: frac_def algebra_simps)
qed
lemma floor_add2[simp]: "frac x = 0 \<or> frac y = 0 \<Longrightarrow> \<lfloor>x + y\<rfloor> = \<lfloor>x\<rfloor> + \<lfloor>y\<rfloor>"
--- a/src/HOL/Library/Float.thy Fri Aug 05 10:05:50 2016 +0200
+++ b/src/HOL/Library/Float.thy Fri Aug 05 12:27:51 2016 +0200
@@ -1425,8 +1425,8 @@
by (simp add: log_mult)
then have "bitlen (int x) < bitlen (int y)"
using assms
- by (simp add: bitlen_alt_def del: floor_add_one)
- (auto intro!: floor_mono simp add: floor_add_one[symmetric] simp del: floor_add floor_add_one)
+ by (simp add: bitlen_alt_def)
+ (auto intro!: floor_mono simp add: one_add_floor)
then show ?thesis
using assms
by (auto intro!: pos_add_strict simp add: field_simps rat_precision_def)
@@ -1812,9 +1812,9 @@
have "\<dots> = \<lfloor>log 2 (1 + (r + sgn (sgn ai * b) / 2) / 2 powr k)\<rfloor>"
by (subst floor_eq) (auto simp: sgn_if)
also have "k + \<dots> = \<lfloor>log 2 (2 powr k * (1 + (r + sgn (sgn ai * b) / 2) / 2 powr k))\<rfloor>"
- unfolding floor_add2[symmetric]
+ unfolding int_add_floor
using pos[OF less'] \<open>\<bar>b\<bar> \<le> _\<close>
- by (simp add: field_simps add_log_eq_powr)
+ by (simp add: field_simps add_log_eq_powr del: floor_add2)
also have "2 powr k * (1 + (r + sgn (sgn ai * b) / 2) / 2 powr k) =
2 powr k + r + sgn (sgn ai * b) / 2"
by (simp add: sgn_if field_simps)
@@ -1899,8 +1899,8 @@
by (auto simp: field_simps powr_minus[symmetric] powr_divide2[symmetric] powr_mult_base)
then have "\<lfloor>log 2 \<bar>?m1 + ?m2'\<bar>\<rfloor> + ?e = \<lfloor>log 2 \<bar>real_of_float (Float (?m1 * 2 + sgn m2) (?e - 1))\<bar>\<rfloor>"
using \<open>?m1 + ?m2' \<noteq> 0\<close>
- unfolding floor_add_of_int[symmetric]
- by (simp add: log_add_eq_powr abs_mult_pos)
+ unfolding floor_add_int
+ by (simp add: log_add_eq_powr abs_mult_pos del: floor_add2)
finally
have "\<lfloor>log 2 \<bar>?sum\<bar>\<rfloor> = \<lfloor>log 2 \<bar>real_of_float (Float (?m1*2 + sgn m2) (?e - 1))\<bar>\<rfloor>" .
then have "plus_down p (Float m1 e1) (Float m2 e2) =
@@ -1919,7 +1919,7 @@
next
have "e1 + \<lfloor>log 2 \<bar>real_of_int m1\<bar>\<rfloor> - 1 = \<lfloor>log 2 \<bar>?a\<bar>\<rfloor> - 1"
using \<open>m1 \<noteq> 0\<close>
- by (simp add: floor_add2[symmetric] algebra_simps log_mult abs_mult del: floor_add2)
+ by (simp add: int_add_floor algebra_simps log_mult abs_mult del: floor_add2)
also have "\<dots> \<le> \<lfloor>log 2 \<bar>?a + ?b\<bar>\<rfloor>"
using a_half_less_sum \<open>m1 \<noteq> 0\<close> \<open>?sum \<noteq> 0\<close>
unfolding floor_diff_of_int[symmetric]