equal
deleted
inserted
replaced
710 text {* Associative law for multiplication *} |
710 text {* Associative law for multiplication *} |
711 lemma nat_mult_assoc: "(m * n) * k = m * ((n * k)::nat)" |
711 lemma nat_mult_assoc: "(m * n) * k = m * ((n * k)::nat)" |
712 by (induct m) (simp_all add: add_mult_distrib) |
712 by (induct m) (simp_all add: add_mult_distrib) |
713 |
713 |
714 |
714 |
715 text{*The Naturals Form A Semiring*} |
715 text{*The Naturals Form A comm_semiring_1_cancel*} |
716 instance nat :: semiring |
716 instance nat :: comm_semiring_1_cancel |
717 proof |
717 proof |
718 fix i j k :: nat |
718 fix i j k :: nat |
719 show "(i + j) + k = i + (j + k)" by (rule nat_add_assoc) |
719 show "(i + j) + k = i + (j + k)" by (rule nat_add_assoc) |
720 show "i + j = j + i" by (rule nat_add_commute) |
720 show "i + j = j + i" by (rule nat_add_commute) |
721 show "0 + i = i" by simp |
721 show "0 + i = i" by simp |
758 apply (induct_tac x) |
758 apply (induct_tac x) |
759 apply (simp_all add: add_less_mono) |
759 apply (simp_all add: add_less_mono) |
760 done |
760 done |
761 |
761 |
762 |
762 |
763 text{*The Naturals Form an Ordered Semiring*} |
763 text{*The Naturals Form an Ordered comm_semiring_1_cancel*} |
764 instance nat :: ordered_semiring |
764 instance nat :: ordered_semidom |
765 proof |
765 proof |
766 fix i j k :: nat |
766 fix i j k :: nat |
767 show "0 < (1::nat)" by simp |
767 show "0 < (1::nat)" by simp |
768 show "i \<le> j ==> k + i \<le> k + j" by simp |
768 show "i \<le> j ==> k + i \<le> k + j" by simp |
769 show "i < j ==> 0 < k ==> k * i < k * j" by (simp add: mult_less_mono2) |
769 show "i < j ==> 0 < k ==> k * i < k * j" by (simp add: mult_less_mono2) |