# HG changeset patch
# User immler
# Date 1508863701 -7200
# Node ID a99a7cbf0fb5391d4da127fe05ac69c4a999800c
# Parent  d122c24a93d67861e391e1d4f0d806985550696f
generalized lemmas cancelling real_of_int/real in (in)equalities with power; completed set of related simp rules; lemmas about floorlog/bitlen

diff -r d122c24a93d6 -r a99a7cbf0fb5 src/HOL/Analysis/Arcwise_Connected.thy
--- a/src/HOL/Analysis/Arcwise_Connected.thy	Tue Oct 24 10:59:15 2017 +0200
+++ b/src/HOL/Analysis/Arcwise_Connected.thy	Tue Oct 24 18:48:21 2017 +0200
@@ -1093,7 +1093,8 @@
             proof
               have "real j < 2 ^ n"
                 using j_le i k
-                apply (auto simp: le_max_iff_disj simp del: real_of_nat_less_numeral_power_cancel_iff elim!: le_less_trans)
+                apply (auto simp: le_max_iff_disj simp del: of_nat_less_numeral_power_cancel_iff
+                    elim!: le_less_trans)
                  apply (auto simp: field_simps)
                 done
               then show "j < 2 ^ n"
diff -r d122c24a93d6 -r a99a7cbf0fb5 src/HOL/Data_Structures/Sorting.thy
--- a/src/HOL/Data_Structures/Sorting.thy	Tue Oct 24 10:59:15 2017 +0200
+++ b/src/HOL/Data_Structures/Sorting.thy	Tue Oct 24 18:48:21 2017 +0200
@@ -202,6 +202,6 @@
 (* Beware of conversions: *)
 lemma "length xs = 2^k \<Longrightarrow> c_msort xs \<le> length xs * log 2 (length xs)"
 using c_msort_le[of xs k] apply (simp add: log_nat_power algebra_simps)
-by (metis (mono_tags) numeral_power_eq_real_of_nat_cancel_iff of_nat_le_iff of_nat_mult)
+by (metis (mono_tags) numeral_power_eq_of_nat_cancel_iff of_nat_le_iff of_nat_mult)
 
 end
diff -r d122c24a93d6 -r a99a7cbf0fb5 src/HOL/Int.thy
--- a/src/HOL/Int.thy	Tue Oct 24 10:59:15 2017 +0200
+++ b/src/HOL/Int.thy	Tue Oct 24 18:48:21 2017 +0200
@@ -277,6 +277,29 @@
 lemma of_int_eq_1_iff [iff]: "of_int z = 1 \<longleftrightarrow> z = 1"
   using of_int_eq_iff [of z 1] by simp
 
+lemma numeral_power_eq_of_int_cancel_iff [simp]:
+  "numeral x ^ n = of_int y \<longleftrightarrow> numeral x ^ n = y"
+  using of_int_eq_iff[of "numeral x ^ n" y, unfolded of_int_numeral of_int_power] .
+
+lemma of_int_eq_numeral_power_cancel_iff [simp]:
+  "of_int y = numeral x ^ n \<longleftrightarrow> y = numeral x ^ n"
+  using numeral_power_eq_of_int_cancel_iff [of x n y] by (metis (mono_tags))
+
+lemma neg_numeral_power_eq_of_int_cancel_iff [simp]:
+  "(- numeral x) ^ n = of_int y \<longleftrightarrow> (- numeral x) ^ n = y"
+  using of_int_eq_iff[of "(- numeral x) ^ n" y]
+  by simp
+
+lemma of_int_eq_neg_numeral_power_cancel_iff [simp]:
+  "of_int y = (- numeral x) ^ n \<longleftrightarrow> y = (- numeral x) ^ n"
+  using neg_numeral_power_eq_of_int_cancel_iff[of x n y] by (metis (mono_tags))
+
+lemma of_int_eq_of_int_power_cancel_iff[simp]: "(of_int b) ^ w = of_int x \<longleftrightarrow> b ^ w = x"
+  by (metis of_int_power of_int_eq_iff)
+
+lemma of_int_power_eq_of_int_cancel_iff[simp]: "of_int x = (of_int b) ^ w \<longleftrightarrow> x = b ^ w"
+  by (metis of_int_eq_of_int_power_cancel_iff)
+
 end
 
 context linordered_idom
@@ -361,6 +384,52 @@
   then show ?thesis ..
 qed
 
+lemma numeral_power_le_of_int_cancel_iff [simp]:
+  "numeral x ^ n \<le> of_int a \<longleftrightarrow> numeral x ^ n \<le> a"
+  by (metis (mono_tags) local.of_int_eq_numeral_power_cancel_iff of_int_le_iff)
+
+lemma of_int_le_numeral_power_cancel_iff [simp]:
+  "of_int a \<le> numeral x ^ n \<longleftrightarrow> a \<le> numeral x ^ n"
+  by (metis (mono_tags) local.numeral_power_eq_of_int_cancel_iff of_int_le_iff)
+
+lemma numeral_power_less_of_int_cancel_iff [simp]:
+  "numeral x ^ n < of_int a \<longleftrightarrow> numeral x ^ n < a"
+  by (metis (mono_tags) local.of_int_eq_numeral_power_cancel_iff of_int_less_iff)
+
+lemma of_int_less_numeral_power_cancel_iff [simp]:
+  "of_int a < numeral x ^ n \<longleftrightarrow> a < numeral x ^ n"
+  by (metis (mono_tags) local.of_int_eq_numeral_power_cancel_iff of_int_less_iff)
+
+lemma neg_numeral_power_le_of_int_cancel_iff [simp]:
+  "(- numeral x) ^ n \<le> of_int a \<longleftrightarrow> (- numeral x) ^ n \<le> a"
+  by (metis (mono_tags) of_int_le_iff of_int_neg_numeral of_int_power)
+
+lemma of_int_le_neg_numeral_power_cancel_iff [simp]:
+  "of_int a \<le> (- numeral x) ^ n \<longleftrightarrow> a \<le> (- numeral x) ^ n"
+  by (metis (mono_tags) of_int_le_iff of_int_neg_numeral of_int_power)
+
+lemma neg_numeral_power_less_of_int_cancel_iff [simp]:
+  "(- numeral x) ^ n < of_int a \<longleftrightarrow> (- numeral x) ^ n < a"
+  using of_int_less_iff[of "(- numeral x) ^ n" a]
+  by simp
+
+lemma of_int_less_neg_numeral_power_cancel_iff [simp]:
+  "of_int a < (- numeral x) ^ n \<longleftrightarrow> a < (- numeral x::int) ^ n"
+  using of_int_less_iff[of a "(- numeral x) ^ n"]
+  by simp
+
+lemma of_int_le_of_int_power_cancel_iff[simp]: "(of_int b) ^ w \<le> of_int x \<longleftrightarrow> b ^ w \<le> x"
+  by (metis (mono_tags) of_int_le_iff of_int_power)
+
+lemma of_int_power_le_of_int_cancel_iff[simp]: "of_int x \<le> (of_int b) ^ w\<longleftrightarrow> x \<le> b ^ w"
+  by (metis (mono_tags) of_int_le_iff of_int_power)
+
+lemma of_int_less_of_int_power_cancel_iff[simp]: "(of_int b) ^ w < of_int x \<longleftrightarrow> b ^ w < x"
+  by (metis (mono_tags) of_int_less_iff of_int_power)
+
+lemma of_int_power_less_of_int_cancel_iff[simp]: "of_int x < (of_int b) ^ w\<longleftrightarrow> x < b ^ w"
+  by (metis (mono_tags) of_int_less_iff of_int_power)
+
 end
 
 text \<open>Comparisons involving @{term of_int}.\<close>
@@ -1670,6 +1739,34 @@
 lemma nat_power_eq: "0 \<le> z \<Longrightarrow> nat (z ^ n) = nat z ^ n"
   by (induct n) (simp_all add: nat_mult_distrib)
 
+lemma numeral_power_eq_nat_cancel_iff [simp]:
+  "numeral x ^ n = nat y \<longleftrightarrow> numeral x ^ n = y"
+  using nat_eq_iff2 by auto
+
+lemma nat_eq_numeral_power_cancel_iff [simp]:
+  "nat y = numeral x ^ n \<longleftrightarrow> y = numeral x ^ n"
+  using numeral_power_eq_nat_cancel_iff[of x n y]
+  by (metis (mono_tags))
+
+lemma numeral_power_le_nat_cancel_iff [simp]:
+  "numeral x ^ n \<le> nat a \<longleftrightarrow> numeral x ^ n \<le> a"
+  using nat_le_eq_zle[of "numeral x ^ n" a]
+  by (auto simp: nat_power_eq)
+
+lemma nat_le_numeral_power_cancel_iff [simp]:
+  "nat a \<le> numeral x ^ n \<longleftrightarrow> a \<le> numeral x ^ n"
+  by (simp add: nat_le_iff)
+
+lemma numeral_power_less_nat_cancel_iff [simp]:
+  "numeral x ^ n < nat a \<longleftrightarrow> numeral x ^ n < a"
+  using nat_less_eq_zless[of "numeral x ^ n" a]
+  by (auto simp: nat_power_eq)
+
+lemma nat_less_numeral_power_cancel_iff [simp]:
+  "nat a < numeral x ^ n \<longleftrightarrow> a < numeral x ^ n"
+  using nat_less_eq_zless[of a "numeral x ^ n"]
+  by (cases "a < 0") (auto simp: nat_power_eq less_le_trans[where y=0])
+
 lemma zdvd_imp_le: "z dvd n \<Longrightarrow> 0 < n \<Longrightarrow> z \<le> n"
   for n z :: int
   apply (cases n)
diff -r d122c24a93d6 -r a99a7cbf0fb5 src/HOL/Library/Float.thy
--- a/src/HOL/Library/Float.thy	Tue Oct 24 10:59:15 2017 +0200
+++ b/src/HOL/Library/Float.thy	Tue Oct 24 18:48:21 2017 +0200
@@ -1467,8 +1467,8 @@
     using bitlen_bounds[of "\<bar>m2\<bar>"]
     by (auto simp: powr_add bitlen_nonneg)
   then show ?thesis
-    by (metis bitlen_nonneg powr_int of_int_abs real_of_int_less_numeral_power_cancel_iff
-      zero_less_numeral)
+    by (metis bitlen_nonneg powr_int of_int_abs of_int_less_numeral_power_cancel_iff
+        zero_less_numeral)
 qed
 
 lemma floor_sum_times_2_powr_sgn_eq:
@@ -1570,7 +1570,7 @@
   from this[simplified of_int_le_iff[symmetric]] \<open>0 \<le> k\<close>
   have r_le: "r \<le> 2 powr k - 1"
     by (auto simp: algebra_simps powr_int)
-      (metis of_int_1 of_int_add real_of_int_le_numeral_power_cancel_iff)
+      (metis of_int_1 of_int_add of_int_le_numeral_power_cancel_iff)
 
   have "\<bar>ai\<bar> = 2 powr k + r"
     using \<open>k \<ge> 0\<close> by (auto simp: k_def r_def powr_realpow[symmetric])
@@ -1981,7 +1981,7 @@
     qed
     then have "real_of_int \<lceil>x * 2 powr real_of_int (int prec - \<lfloor>log 2 x\<rfloor>)\<rceil> \<le> 2 powr int (Suc prec)"
       by (auto simp: powr_realpow powr_add)
-        (metis power_Suc real_of_int_le_numeral_power_cancel_iff)
+        (metis power_Suc of_int_le_numeral_power_cancel_iff)
     also
     have "2 powr - real_of_int (int prec - \<lfloor>log 2 x\<rfloor>) \<le> 2 powr - real_of_int (int prec - \<lfloor>log 2 y\<rfloor> + 1)"
       using logless flogless by (auto intro!: floor_mono)
diff -r d122c24a93d6 -r a99a7cbf0fb5 src/HOL/Library/Log_Nat.thy
--- a/src/HOL/Library/Log_Nat.thy	Tue Oct 24 10:59:15 2017 +0200
+++ b/src/HOL/Library/Log_Nat.thy	Tue Oct 24 18:48:21 2017 +0200
@@ -131,6 +131,70 @@
 qed
 
 
+lemma powr_eq_one_iff[simp]: "a powr x = 1 \<longleftrightarrow> (x = 0)"
+  if "a > 1"
+  for a x::real
+  using that
+  by (auto simp: powr_def split: if_splits)
+
+lemma floorlog_leD: "floorlog b x \<le> w \<Longrightarrow> b > 1 \<Longrightarrow> x < b ^ w"
+  by (metis floorlog_bounds leD linorder_neqE_nat order.strict_trans power_strict_increasing_iff
+      zero_less_one zero_less_power)
+
+lemma floorlog_leI: "x < b ^ w \<Longrightarrow> 0 \<le> w \<Longrightarrow> b > 1 \<Longrightarrow> floorlog b x \<le> w"
+  by (drule less_imp_of_nat_less[where 'a=real])
+    (auto simp: floorlog_def Suc_le_eq nat_less_iff floor_less_iff log_of_power_less)
+
+lemma floorlog_eq_zero_iff:
+  "floorlog b x = 0 \<longleftrightarrow> (b \<le> 1 \<or> x \<le> 0)"
+  by (auto simp: floorlog_def)
+
+lemma floorlog_le_iff: "floorlog b x \<le> w \<longleftrightarrow> b \<le> 1 \<or> b > 1 \<and> 0 \<le> w \<and> x < b ^ w"
+  using floorlog_leD[of b x w] floorlog_leI[of x b w]
+  by (auto simp: floorlog_eq_zero_iff[THEN iffD2])
+
+lemma floorlog_ge_SucI: "Suc w \<le> floorlog b x" if "b ^ w \<le> x" "b > 1"
+  using that le_log_of_power[of b w x] power_not_zero
+  by (force simp: floorlog_def Suc_le_eq powr_realpow not_less Suc_nat_eq_nat_zadd1
+      zless_nat_eq_int_zless int_add_floor less_floor_iff
+      simp del: floor_add2)
+
+lemma floorlog_geI: "w \<le> floorlog b x" if "b ^ (w - 1) \<le> x" "b > 1"
+  using floorlog_ge_SucI[of b "w - 1" x] that
+  by auto
+
+lemma floorlog_geD: "b ^ (w - 1) \<le> x" if "w \<le> floorlog b x" "w > 0"
+proof -
+  have "b > 1" "0 < x"
+    using that by (auto simp: floorlog_def split: if_splits)
+  have "b ^ (w - 1) \<le> x" if "b ^ w \<le> x"
+  proof -
+    have "b ^ (w - 1) \<le> b ^ w"
+      using \<open>b > 1\<close>
+      by (auto intro!: power_increasing)
+    also note that
+    finally show ?thesis .
+  qed
+  moreover have "b ^ nat \<lfloor>log (real b) (real x)\<rfloor> \<le> x" (is "?l \<le> _")
+  proof -
+    have "0 \<le> log (real b) (real x)"
+      using \<open>b > 1\<close> \<open>0 < x\<close>
+      by (auto simp: )
+    then have "?l \<le> b powr log (real b) (real x)"
+      using \<open>b > 1\<close>
+      by (auto simp add: powr_realpow[symmetric] intro!: powr_mono of_nat_floor)
+    also have "\<dots> = x" using \<open>b > 1\<close> \<open>0 < x\<close>
+      by auto
+    finally show ?thesis
+      unfolding of_nat_le_iff .
+  qed
+  ultimately show ?thesis
+    using that
+    by (auto simp: floorlog_def le_nat_iff le_floor_iff le_log_iff powr_realpow
+        split: if_splits elim!: le_SucE)
+qed
+
+
 definition bitlen :: "int \<Rightarrow> int" where "bitlen a = floorlog 2 (nat a)"
 
 lemma bitlen_alt_def: "bitlen a = (if a > 0 then \<lfloor>log 2 a\<rfloor> + 1 else 0)"
@@ -184,10 +248,27 @@
   also have "\<dots> = ?B * 2"
     unfolding nat_add_distrib[OF \<open>0 \<le> bitlen m - 1\<close> zero_le_one] by auto
   finally have "real_of_int m < 2 * ?B"
-    by (metis (full_types) mult.commute power.simps(2) real_of_int_less_numeral_power_cancel_iff)
+    by (metis (full_types) mult.commute power.simps(2) of_int_less_numeral_power_cancel_iff)
   then have "real_of_int m / ?B < 2 * ?B / ?B"
     by (rule divide_strict_right_mono) auto
   then show "real_of_int m / ?B < 2" by auto
 qed
 
+lemma bitlen_le_iff_floorlog: "bitlen x \<le> w \<longleftrightarrow> w \<ge> 0 \<and> floorlog 2 (nat x) \<le> nat w"
+  by (auto simp: bitlen_def)
+
+lemma bitlen_le_iff_power: "bitlen x \<le> w \<longleftrightarrow> w \<ge> 0 \<and> x < 2 ^ nat w"
+  by (auto simp: bitlen_le_iff_floorlog floorlog_le_iff)
+
+lemma less_power_nat_iff_bitlen: "x < 2 ^ w \<longleftrightarrow> bitlen (int x) \<le> w"
+  using bitlen_le_iff_power[of x w]
+  by auto
+
+lemma bitlen_ge_iff_power: "w \<le> bitlen x \<longleftrightarrow> w \<le> 0 \<or> 2 ^ (nat w - 1) \<le> x"
+  unfolding bitlen_def
+  by (auto simp: nat_le_iff[symmetric] intro: floorlog_geI dest: floorlog_geD)
+
+lemma bitlen_twopow_add_eq: "bitlen (2 ^ w + b) = w + 1" if "0 \<le> b" "b < 2 ^ w"
+  by (auto simp: that nat_add_distrib bitlen_le_iff_power bitlen_ge_iff_power intro!: antisym)
+
 end
diff -r d122c24a93d6 -r a99a7cbf0fb5 src/HOL/Power.thy
--- a/src/HOL/Power.thy	Tue Oct 24 10:59:15 2017 +0200
+++ b/src/HOL/Power.thy	Tue Oct 24 18:48:21 2017 +0200
@@ -174,6 +174,24 @@
 
 end
 
+context semiring_char_0 begin
+
+lemma numeral_power_eq_of_nat_cancel_iff [simp]:
+  "numeral x ^ n = of_nat y \<longleftrightarrow> numeral x ^ n = y"
+  using of_nat_eq_iff by fastforce
+
+lemma real_of_nat_eq_numeral_power_cancel_iff [simp]:
+  "of_nat y = numeral x ^ n \<longleftrightarrow> y = numeral x ^ n"
+  using numeral_power_eq_of_nat_cancel_iff [of x n y] by (metis (mono_tags))
+
+lemma of_nat_eq_of_nat_power_cancel_iff[simp]: "(of_nat b) ^ w = of_nat x \<longleftrightarrow> b ^ w = x"
+  by (metis of_nat_power of_nat_eq_iff)
+
+lemma of_nat_power_eq_of_nat_cancel_iff[simp]: "of_nat x = (of_nat b) ^ w \<longleftrightarrow> x = b ^ w"
+  by (metis of_nat_eq_of_nat_power_cancel_iff)
+
+end
+
 context comm_semiring_1
 begin
 
@@ -568,6 +586,34 @@
   shows "(x ^ 2 = y ^ 2) \<longleftrightarrow> x = y"
 using assms power2_eq_imp_eq by blast
 
+lemma of_nat_less_numeral_power_cancel_iff[simp]:
+  "of_nat x < numeral i ^ n \<longleftrightarrow> x < numeral i ^ n"
+  using of_nat_less_iff[of x "numeral i ^ n", unfolded of_nat_numeral of_nat_power] .
+
+lemma of_nat_le_numeral_power_cancel_iff[simp]:
+  "of_nat x \<le> numeral i ^ n \<longleftrightarrow> x \<le> numeral i ^ n"
+  using of_nat_le_iff[of x "numeral i ^ n", unfolded of_nat_numeral of_nat_power] .
+
+lemma numeral_power_less_of_nat_cancel_iff[simp]:
+  "numeral i ^ n < of_nat x \<longleftrightarrow> numeral i ^ n < x"
+  using of_nat_less_iff[of "numeral i ^ n" x, unfolded of_nat_numeral of_nat_power] .
+
+lemma numeral_power_le_of_nat_cancel_iff[simp]:
+  "numeral i ^ n \<le> of_nat x \<longleftrightarrow> numeral i ^ n \<le> x"
+  using of_nat_le_iff[of "numeral i ^ n" x, unfolded of_nat_numeral of_nat_power] .
+
+lemma of_nat_le_of_nat_power_cancel_iff[simp]: "(of_nat b) ^ w \<le> of_nat x \<longleftrightarrow> b ^ w \<le> x"
+  by (metis of_nat_le_iff of_nat_power)
+
+lemma of_nat_power_le_of_nat_cancel_iff[simp]: "of_nat x \<le> (of_nat b) ^ w \<longleftrightarrow> x \<le> b ^ w"
+  by (metis of_nat_le_iff of_nat_power)
+
+lemma of_nat_less_of_nat_power_cancel_iff[simp]: "(of_nat b) ^ w < of_nat x \<longleftrightarrow> b ^ w < x"
+  by (metis of_nat_less_iff of_nat_power)
+
+lemma of_nat_power_less_of_nat_cancel_iff[simp]: "of_nat x < (of_nat b) ^ w \<longleftrightarrow> x < b ^ w"
+  by (metis of_nat_less_iff of_nat_power)
+
 end
 
 context linordered_ring_strict
diff -r d122c24a93d6 -r a99a7cbf0fb5 src/HOL/Real.thy
--- a/src/HOL/Real.thy	Tue Oct 24 10:59:15 2017 +0200
+++ b/src/HOL/Real.thy	Tue Oct 24 18:48:21 2017 +0200
@@ -1378,62 +1378,6 @@
   for u x :: real
   by (auto simp add: power2_eq_square)
 
-lemma numeral_power_eq_real_of_int_cancel_iff [simp]:
-  "numeral x ^ n = real_of_int y \<longleftrightarrow> numeral x ^ n = y"
-  by (metis of_int_eq_iff of_int_numeral of_int_power)
-
-lemma real_of_int_eq_numeral_power_cancel_iff [simp]:
-  "real_of_int y = numeral x ^ n \<longleftrightarrow> y = numeral x ^ n"
-  using numeral_power_eq_real_of_int_cancel_iff [of x n y] by metis
-
-lemma numeral_power_eq_real_of_nat_cancel_iff [simp]:
-  "numeral x ^ n = real y \<longleftrightarrow> numeral x ^ n = y"
-  using of_nat_eq_iff by fastforce
-
-lemma real_of_nat_eq_numeral_power_cancel_iff [simp]:
-  "real y = numeral x ^ n \<longleftrightarrow> y = numeral x ^ n"
-  using numeral_power_eq_real_of_nat_cancel_iff [of x n y] by metis
-
-lemma numeral_power_le_real_of_nat_cancel_iff [simp]:
-  "(numeral x :: real) ^ n \<le> real a \<longleftrightarrow> (numeral x::nat) ^ n \<le> a"
-  by (metis of_nat_le_iff of_nat_numeral of_nat_power)
-
-lemma real_of_nat_le_numeral_power_cancel_iff [simp]:
-  "real a \<le> (numeral x::real) ^ n \<longleftrightarrow> a \<le> (numeral x::nat) ^ n"
-  by (metis of_nat_le_iff of_nat_numeral of_nat_power)
-
-lemma numeral_power_le_real_of_int_cancel_iff [simp]:
-  "(numeral x::real) ^ n \<le> real_of_int a \<longleftrightarrow> (numeral x::int) ^ n \<le> a"
-  by (metis ceiling_le_iff ceiling_of_int of_int_numeral of_int_power)
-
-lemma real_of_int_le_numeral_power_cancel_iff [simp]:
-  "real_of_int a \<le> (numeral x::real) ^ n \<longleftrightarrow> a \<le> (numeral x::int) ^ n"
-  by (metis floor_of_int le_floor_iff of_int_numeral of_int_power)
-
-lemma numeral_power_less_real_of_nat_cancel_iff [simp]:
-  "(numeral x::real) ^ n < real a \<longleftrightarrow> (numeral x::nat) ^ n < a"
-  by (metis of_nat_less_iff of_nat_numeral of_nat_power)
-
-lemma real_of_nat_less_numeral_power_cancel_iff [simp]:
-  "real a < (numeral x::real) ^ n \<longleftrightarrow> a < (numeral x::nat) ^ n"
-  by (metis of_nat_less_iff of_nat_numeral of_nat_power)
-
-lemma numeral_power_less_real_of_int_cancel_iff [simp]:
-  "(numeral x::real) ^ n < real_of_int a \<longleftrightarrow> (numeral x::int) ^ n < a"
-  by (meson not_less real_of_int_le_numeral_power_cancel_iff)
-
-lemma real_of_int_less_numeral_power_cancel_iff [simp]:
-  "real_of_int a < (numeral x::real) ^ n \<longleftrightarrow> a < (numeral x::int) ^ n"
-  by (meson not_less numeral_power_le_real_of_int_cancel_iff)
-
-lemma neg_numeral_power_le_real_of_int_cancel_iff [simp]:
-  "(- numeral x::real) ^ n \<le> real_of_int a \<longleftrightarrow> (- numeral x::int) ^ n \<le> a"
-  by (metis of_int_le_iff of_int_neg_numeral of_int_power)
-
-lemma real_of_int_le_neg_numeral_power_cancel_iff [simp]:
-  "real_of_int a \<le> (- numeral x::real) ^ n \<longleftrightarrow> a \<le> (- numeral x::int) ^ n"
-  by (metis of_int_le_iff of_int_neg_numeral of_int_power)
-
 
 subsection \<open>Density of the Reals\<close>
 
diff -r d122c24a93d6 -r a99a7cbf0fb5 src/HOL/Word/Word.thy
--- a/src/HOL/Word/Word.thy	Tue Oct 24 10:59:15 2017 +0200
+++ b/src/HOL/Word/Word.thy	Tue Oct 24 18:48:21 2017 +0200
@@ -868,11 +868,7 @@
   apply safe
     apply (rule_tac image_eqI)
      apply (erule_tac nat_0_le [symmetric])
-    apply auto
-   apply (erule_tac nat_less_iff [THEN iffD2])
-   apply (rule_tac [2] zless_nat_eq_int_zless [THEN iffD1])
-   apply (auto simp: nat_power_eq)
-  done
+  by auto
 
 lemma unats_uints: "unats n = nat ` uints n"
   by (auto simp: uints_unats image_iff)