# 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 \<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"