--- a/src/HOL/Word/Word.thy Sat May 12 17:53:12 2018 +0200
+++ b/src/HOL/Word/Word.thy Sat May 12 22:20:46 2018 +0200
@@ -1750,13 +1750,8 @@
lemma of_nat_eq: "of_nat n = w \<longleftrightarrow> (\<exists>q. n = unat w + q * 2 ^ len_of TYPE('a))"
for w :: "'a::len word"
- apply (rule trans)
- apply (rule word_unat.inverse_norm)
- apply (rule iffI)
- apply (rule mod_eqD)
- apply simp
- apply clarsimp
- done
+ using mod_div_mult_eq [of n "2 ^ LENGTH('a)", symmetric]
+ by (auto simp add: word_unat.inverse_norm)
lemma of_nat_eq_size: "of_nat n = w \<longleftrightarrow> (\<exists>q. n = unat w + q * 2 ^ size w)"
unfolding word_size by (rule of_nat_eq)