src/HOL/Code_Numeral.thy
changeset 55427 ff54d22fe357
parent 54489 03ff4d1e6784
child 55428 0ab52bf7b5e6
     1.1 --- a/src/HOL/Code_Numeral.thy	Wed Feb 12 08:56:38 2014 +0100
     1.2 +++ b/src/HOL/Code_Numeral.thy	Wed Feb 12 09:06:04 2014 +0100
     1.3 @@ -230,6 +230,15 @@
     1.4      semiring_numeral_div_class.div_mult2_eq
     1.5      semiring_numeral_div_class.discrete)+
     1.6  
     1.7 +lemma integer_of_nat_0: "integer_of_nat 0 = 0"
     1.8 +by transfer simp
     1.9 +
    1.10 +lemma integer_of_nat_1: "integer_of_nat 1 = 1"
    1.11 +by transfer simp
    1.12 +
    1.13 +lemma integer_of_nat_numeral:
    1.14 +  "integer_of_nat (numeral n) = numeral n"
    1.15 +by transfer simp
    1.16  
    1.17  subsection {* Code theorems for target language integers *}
    1.18