equal
deleted
inserted
replaced
226 lemma nat_of_num_sqr: "nat_of_num (sqr x) = nat_of_num x * nat_of_num x" |
226 lemma nat_of_num_sqr: "nat_of_num (sqr x) = nat_of_num x * nat_of_num x" |
227 by (induct x) (simp_all add: algebra_simps nat_of_num_add) |
227 by (induct x) (simp_all add: algebra_simps nat_of_num_add) |
228 |
228 |
229 lemma sqr_conv_mult: "sqr x = x * x" |
229 lemma sqr_conv_mult: "sqr x = x * x" |
230 by (simp add: num_eq_iff nat_of_num_sqr nat_of_num_mult) |
230 by (simp add: num_eq_iff nat_of_num_sqr nat_of_num_mult) |
|
231 |
|
232 lemma num_double [simp]: |
|
233 "num.Bit0 num.One * n = num.Bit0 n" |
|
234 by (simp add: num_eq_iff nat_of_num_mult) |
231 |
235 |
232 |
236 |
233 subsection \<open>Binary numerals\<close> |
237 subsection \<open>Binary numerals\<close> |
234 |
238 |
235 text \<open> |
239 text \<open> |