# HG changeset patch # User huffman # Date 1228624011 28800 # Node ID e515f42d1db7db702a0325a3b04b918ee9962641 # Parent 62a6ddcbb53b3abef6c98294a043713696b53a14 multiplication for type inat diff -r 62a6ddcbb53b -r e515f42d1db7 src/HOL/Library/Nat_Infinity.thy --- a/src/HOL/Library/Nat_Infinity.thy Sat Dec 06 20:25:31 2008 -0800 +++ b/src/HOL/Library/Nat_Infinity.thy Sat Dec 06 20:26:51 2008 -0800 @@ -165,6 +165,58 @@ unfolding iSuc_plus_1 by (simp_all add: add_ac) +subsection {* Multiplication *} + +instantiation inat :: comm_semiring_1 +begin + +definition + times_inat_def [code del]: + "m * n = (case m of \ \ if n = 0 then 0 else \ | Fin m \ + (case n of \ \ if m = 0 then 0 else \ | Fin n \ Fin (m * n)))" + +lemma times_inat_simps [simp, code]: + "Fin m * Fin n = Fin (m * n)" + "\ * \ = \" + "\ * Fin n = (if n = 0 then 0 else \)" + "Fin m * \ = (if m = 0 then 0 else \)" + unfolding times_inat_def zero_inat_def + by (simp_all split: inat.split) + +instance proof + fix a b c :: inat + show "(a * b) * c = a * (b * c)" + unfolding times_inat_def zero_inat_def + by (simp split: inat.split) + show "a * b = b * a" + unfolding times_inat_def zero_inat_def + by (simp split: inat.split) + show "1 * a = a" + unfolding times_inat_def zero_inat_def one_inat_def + by (simp split: inat.split) + show "(a + b) * c = a * c + b * c" + unfolding times_inat_def zero_inat_def + by (simp split: inat.split add: left_distrib) + show "0 * a = 0" + unfolding times_inat_def zero_inat_def + by (simp split: inat.split) + show "a * 0 = 0" + unfolding times_inat_def zero_inat_def + by (simp split: inat.split) + show "(0::inat) \ 1" + unfolding zero_inat_def one_inat_def + by simp +qed + +end + +lemma mult_iSuc: "iSuc m * n = n + m * n" + unfolding iSuc_plus_1 by (simp add: ring_simps) + +lemma mult_iSuc_right: "m * iSuc n = m + m * n" + unfolding iSuc_plus_1 by (simp add: ring_simps) + + subsection {* Ordering *} instantiation inat :: ordered_ab_semigroup_add @@ -201,6 +253,15 @@ end +instance inat :: pordered_comm_semiring +proof + fix a b c :: inat + assume "a \ b" and "0 \ c" + thus "c * a \ c * b" + unfolding times_inat_def less_eq_inat_def zero_inat_def + by (simp split: inat.splits) +qed + lemma inat_ord_number [simp]: "(number_of m \ inat) \ number_of n \ (number_of m \ nat) \ number_of n" "(number_of m \ inat) < number_of n \ (number_of m \ nat) < number_of n"