src/HOL/Nat_Numeral.thy
changeset 44766 d4d33a4d7548
parent 44345 881c324470a2
child 44857 73d5b722c4b4
equal deleted inserted replaced
44765:d96550db3d77 44766:d4d33a4d7548
   362 
   362 
   363 subsubsection{*Successor *}
   363 subsubsection{*Successor *}
   364 
   364 
   365 lemma Suc_nat_eq_nat_zadd1: "(0::int) <= z ==> Suc (nat z) = nat (1 + z)"
   365 lemma Suc_nat_eq_nat_zadd1: "(0::int) <= z ==> Suc (nat z) = nat (1 + z)"
   366 apply (rule sym)
   366 apply (rule sym)
   367 apply (simp add: nat_eq_iff int_Suc)
   367 apply (simp add: nat_eq_iff)
   368 done
   368 done
   369 
   369 
   370 lemma Suc_nat_number_of_add:
   370 lemma Suc_nat_number_of_add:
   371      "Suc (number_of v + n) =  
   371      "Suc (number_of v + n) =  
   372         (if neg (number_of v :: int) then 1+n else number_of (Int.succ v) + n)"
   372         (if neg (number_of v :: int) then 1+n else number_of (Int.succ v) + n)"