--- 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 \<infinity> \<Rightarrow> if n = 0 then 0 else \<infinity> | Fin m \<Rightarrow>
+ (case n of \<infinity> \<Rightarrow> if m = 0 then 0 else \<infinity> | Fin n \<Rightarrow> Fin (m * n)))"
+
+lemma times_inat_simps [simp, code]:
+ "Fin m * Fin n = Fin (m * n)"
+ "\<infinity> * \<infinity> = \<infinity>"
+ "\<infinity> * Fin n = (if n = 0 then 0 else \<infinity>)"
+ "Fin m * \<infinity> = (if m = 0 then 0 else \<infinity>)"
+ 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) \<noteq> 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 \<le> b" and "0 \<le> c"
+ thus "c * a \<le> 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 \<Colon> inat) \<le> number_of n \<longleftrightarrow> (number_of m \<Colon> nat) \<le> number_of n"
"(number_of m \<Colon> inat) < number_of n \<longleftrightarrow> (number_of m \<Colon> nat) < number_of n"