# HG changeset patch
# User nipkow
# Date 1470392871 -7200
# Node ID f560147710fbd5c6eb67ebf92c05bf9565a842bc
# Parent  025d6e52d86f254be5423b83a45ddd240224f28e
fixed floor proofs

diff -r 025d6e52d86f -r f560147710fb src/HOL/Archimedean_Field.thy
--- 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>"
diff -r 025d6e52d86f -r f560147710fb src/HOL/Library/Float.thy
--- 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]