equal
deleted
inserted
replaced
271 "word_of_int (2^len_of TYPE('a) - i) = (word_of_int (-i)::'a::len word)" |
271 "word_of_int (2^len_of TYPE('a) - i) = (word_of_int (-i)::'a::len word)" |
272 proof - |
272 proof - |
273 have x: "2^len_of TYPE('a) - i = -i + 2^len_of TYPE('a)" by simp |
273 have x: "2^len_of TYPE('a) - i = -i + 2^len_of TYPE('a)" by simp |
274 show ?thesis |
274 show ?thesis |
275 apply (subst x) |
275 apply (subst x) |
276 apply (subst word_uint.Abs_norm [symmetric], subst zmod_zadd_self2) |
276 apply (subst word_uint.Abs_norm [symmetric], subst mod_add_self2) |
277 apply simp |
277 apply simp |
278 done |
278 done |
279 qed |
279 qed |
280 |
280 |
281 lemmas word_of_int_inj = |
281 lemmas word_of_int_inj = |