equal
deleted
inserted
replaced
395 unfolding of_num_plus_one [symmetric] add_commute .. |
395 unfolding of_num_plus_one [symmetric] add_commute .. |
396 |
396 |
397 lemma of_num_plus [numeral]: |
397 lemma of_num_plus [numeral]: |
398 "of_num m + of_num n = of_num (m + n)" |
398 "of_num m + of_num n = of_num (m + n)" |
399 by (induct n rule: num_induct) |
399 by (induct n rule: num_induct) |
400 (simp_all add: Dig_plus of_num_one semigroup_add_class.plus.add_assoc [symmetric, of m] |
400 (simp_all add: Dig_plus of_num_one semigroup_add_class.add_assoc [symmetric, of m] |
401 add_ac of_num_plus_one [symmetric]) |
401 add_ac of_num_plus_one [symmetric]) |
402 |
402 |
403 lemma of_num_times_one [numeral]: |
403 lemma of_num_times_one [numeral]: |
404 "of_num n * 1 = of_num n" |
404 "of_num n * 1 = of_num n" |
405 by simp |
405 by simp |
410 |
410 |
411 lemma of_num_times [numeral]: |
411 lemma of_num_times [numeral]: |
412 "of_num m * of_num n = of_num (m * n)" |
412 "of_num m * of_num n = of_num (m * n)" |
413 by (induct n rule: num_induct) |
413 by (induct n rule: num_induct) |
414 (simp_all add: of_num_plus [symmetric] |
414 (simp_all add: of_num_plus [symmetric] |
415 semiring_class.plus_times.right_distrib right_distrib of_num_one) |
415 semiring_class.right_distrib right_distrib of_num_one) |
416 |
416 |
417 end |
417 end |
418 |
418 |
419 text {* |
419 text {* |
420 Structures with a @{term 0}. |
420 Structures with a @{term 0}. |