1.1 --- a/src/HOL/Library/Nat_Infinity.thy	Sat Dec 06 20:25:31 2008 -0800
     1.2 +++ b/src/HOL/Library/Nat_Infinity.thy	Sat Dec 06 20:26:51 2008 -0800
     1.3 @@ -165,6 +165,58 @@
     1.4    unfolding iSuc_plus_1 by (simp_all add: add_ac)
     1.5  
     1.6  
     1.7 +subsection {* Multiplication *}
     1.8 +
     1.9 +instantiation inat :: comm_semiring_1
    1.10 +begin
    1.11 +
    1.12 +definition
    1.13 +  times_inat_def [code del]:
    1.14 +  "m * n = (case m of \<infinity> \<Rightarrow> if n = 0 then 0 else \<infinity> | Fin m \<Rightarrow>
    1.15 +    (case n of \<infinity> \<Rightarrow> if m = 0 then 0 else \<infinity> | Fin n \<Rightarrow> Fin (m * n)))"
    1.16 +
    1.17 +lemma times_inat_simps [simp, code]:
    1.18 +  "Fin m * Fin n = Fin (m * n)"
    1.19 +  "\<infinity> * \<infinity> = \<infinity>"
    1.20 +  "\<infinity> * Fin n = (if n = 0 then 0 else \<infinity>)"
    1.21 +  "Fin m * \<infinity> = (if m = 0 then 0 else \<infinity>)"
    1.22 +  unfolding times_inat_def zero_inat_def
    1.23 +  by (simp_all split: inat.split)
    1.24 +
    1.25 +instance proof
    1.26 +  fix a b c :: inat
    1.27 +  show "(a * b) * c = a * (b * c)"
    1.28 +    unfolding times_inat_def zero_inat_def
    1.29 +    by (simp split: inat.split)
    1.30 +  show "a * b = b * a"
    1.31 +    unfolding times_inat_def zero_inat_def
    1.32 +    by (simp split: inat.split)
    1.33 +  show "1 * a = a"
    1.34 +    unfolding times_inat_def zero_inat_def one_inat_def
    1.35 +    by (simp split: inat.split)
    1.36 +  show "(a + b) * c = a * c + b * c"
    1.37 +    unfolding times_inat_def zero_inat_def
    1.38 +    by (simp split: inat.split add: left_distrib)
    1.39 +  show "0 * a = 0"
    1.40 +    unfolding times_inat_def zero_inat_def
    1.41 +    by (simp split: inat.split)
    1.42 +  show "a * 0 = 0"
    1.43 +    unfolding times_inat_def zero_inat_def
    1.44 +    by (simp split: inat.split)
    1.45 +  show "(0::inat) \<noteq> 1"
    1.46 +    unfolding zero_inat_def one_inat_def
    1.47 +    by simp
    1.48 +qed
    1.49 +
    1.50 +end
    1.51 +
    1.52 +lemma mult_iSuc: "iSuc m * n = n + m * n"
    1.53 +  unfolding iSuc_plus_1 by (simp add: ring_simps)
    1.54 +
    1.55 +lemma mult_iSuc_right: "m * iSuc n = m + m * n"
    1.56 +  unfolding iSuc_plus_1 by (simp add: ring_simps)
    1.57 +
    1.58 +
    1.59  subsection {* Ordering *}
    1.60  
    1.61  instantiation inat :: ordered_ab_semigroup_add
    1.62 @@ -201,6 +253,15 @@
    1.63  
    1.64  end
    1.65  
    1.66 +instance inat :: pordered_comm_semiring
    1.67 +proof
    1.68 +  fix a b c :: inat
    1.69 +  assume "a \<le> b" and "0 \<le> c"
    1.70 +  thus "c * a \<le> c * b"
    1.71 +    unfolding times_inat_def less_eq_inat_def zero_inat_def
    1.72 +    by (simp split: inat.splits)
    1.73 +qed
    1.74 +
    1.75  lemma inat_ord_number [simp]:
    1.76    "(number_of m \<Colon> inat) \<le> number_of n \<longleftrightarrow> (number_of m \<Colon> nat) \<le> number_of n"
    1.77    "(number_of m \<Colon> inat) < number_of n \<longleftrightarrow> (number_of m \<Colon> nat) < number_of n"