src/HOL/Library/Nat_Infinity.thy
changeset 29014 e515f42d1db7
parent 29012 9140227dc8c5
child 29023 ef3adebc6d98
equal deleted inserted replaced
29013:62a6ddcbb53b 29014:e515f42d1db7
   163   "1 + q = iSuc q"
   163   "1 + q = iSuc q"
   164   "q + 1 = iSuc q"
   164   "q + 1 = iSuc q"
   165   unfolding iSuc_plus_1 by (simp_all add: add_ac)
   165   unfolding iSuc_plus_1 by (simp_all add: add_ac)
   166 
   166 
   167 
   167 
       
   168 subsection {* Multiplication *}
       
   169 
       
   170 instantiation inat :: comm_semiring_1
       
   171 begin
       
   172 
       
   173 definition
       
   174   times_inat_def [code del]:
       
   175   "m * n = (case m of \<infinity> \<Rightarrow> if n = 0 then 0 else \<infinity> | Fin m \<Rightarrow>
       
   176     (case n of \<infinity> \<Rightarrow> if m = 0 then 0 else \<infinity> | Fin n \<Rightarrow> Fin (m * n)))"
       
   177 
       
   178 lemma times_inat_simps [simp, code]:
       
   179   "Fin m * Fin n = Fin (m * n)"
       
   180   "\<infinity> * \<infinity> = \<infinity>"
       
   181   "\<infinity> * Fin n = (if n = 0 then 0 else \<infinity>)"
       
   182   "Fin m * \<infinity> = (if m = 0 then 0 else \<infinity>)"
       
   183   unfolding times_inat_def zero_inat_def
       
   184   by (simp_all split: inat.split)
       
   185 
       
   186 instance proof
       
   187   fix a b c :: inat
       
   188   show "(a * b) * c = a * (b * c)"
       
   189     unfolding times_inat_def zero_inat_def
       
   190     by (simp split: inat.split)
       
   191   show "a * b = b * a"
       
   192     unfolding times_inat_def zero_inat_def
       
   193     by (simp split: inat.split)
       
   194   show "1 * a = a"
       
   195     unfolding times_inat_def zero_inat_def one_inat_def
       
   196     by (simp split: inat.split)
       
   197   show "(a + b) * c = a * c + b * c"
       
   198     unfolding times_inat_def zero_inat_def
       
   199     by (simp split: inat.split add: left_distrib)
       
   200   show "0 * a = 0"
       
   201     unfolding times_inat_def zero_inat_def
       
   202     by (simp split: inat.split)
       
   203   show "a * 0 = 0"
       
   204     unfolding times_inat_def zero_inat_def
       
   205     by (simp split: inat.split)
       
   206   show "(0::inat) \<noteq> 1"
       
   207     unfolding zero_inat_def one_inat_def
       
   208     by simp
       
   209 qed
       
   210 
       
   211 end
       
   212 
       
   213 lemma mult_iSuc: "iSuc m * n = n + m * n"
       
   214   unfolding iSuc_plus_1 by (simp add: ring_simps)
       
   215 
       
   216 lemma mult_iSuc_right: "m * iSuc n = m + m * n"
       
   217   unfolding iSuc_plus_1 by (simp add: ring_simps)
       
   218 
       
   219 
   168 subsection {* Ordering *}
   220 subsection {* Ordering *}
   169 
   221 
   170 instantiation inat :: ordered_ab_semigroup_add
   222 instantiation inat :: ordered_ab_semigroup_add
   171 begin
   223 begin
   172 
   224 
   198 
   250 
   199 instance by default
   251 instance by default
   200   (auto simp add: less_eq_inat_def less_inat_def plus_inat_def split: inat.splits)
   252   (auto simp add: less_eq_inat_def less_inat_def plus_inat_def split: inat.splits)
   201 
   253 
   202 end
   254 end
       
   255 
       
   256 instance inat :: pordered_comm_semiring
       
   257 proof
       
   258   fix a b c :: inat
       
   259   assume "a \<le> b" and "0 \<le> c"
       
   260   thus "c * a \<le> c * b"
       
   261     unfolding times_inat_def less_eq_inat_def zero_inat_def
       
   262     by (simp split: inat.splits)
       
   263 qed
   203 
   264 
   204 lemma inat_ord_number [simp]:
   265 lemma inat_ord_number [simp]:
   205   "(number_of m \<Colon> inat) \<le> number_of n \<longleftrightarrow> (number_of m \<Colon> nat) \<le> number_of n"
   266   "(number_of m \<Colon> inat) \<le> number_of n \<longleftrightarrow> (number_of m \<Colon> nat) \<le> number_of n"
   206   "(number_of m \<Colon> inat) < number_of n \<longleftrightarrow> (number_of m \<Colon> nat) < number_of n"
   267   "(number_of m \<Colon> inat) < number_of n \<longleftrightarrow> (number_of m \<Colon> nat) < number_of n"
   207   by (simp_all add: number_of_inat_def)
   268   by (simp_all add: number_of_inat_def)