src/HOL/Library/Code_Target_Nat.thy
changeset 51095 7ae79f2e3cc7
parent 50023 28f3263d4d1b
child 51113 222fb6cb2c3e
     1.1 --- a/src/HOL/Library/Code_Target_Nat.thy	Wed Feb 13 13:38:52 2013 +0100
     1.2 +++ b/src/HOL/Library/Code_Target_Nat.thy	Wed Feb 13 13:38:52 2013 +0100
     1.3 @@ -14,13 +14,15 @@
     1.4  where
     1.5    "Nat = nat_of_integer"
     1.6  
     1.7 -definition integer_of_nat :: "nat \<Rightarrow> integer"
     1.8 -where
     1.9 -  [code_abbrev]: "integer_of_nat = of_nat"
    1.10 +lemma [code_post]:
    1.11 +  "Nat 0 = 0"
    1.12 +  "Nat 1 = 1"
    1.13 +  "Nat (numeral k) = numeral k"
    1.14 +  by (simp_all add: Nat_def nat_of_integer_def)
    1.15  
    1.16 -lemma int_of_integer_integer_of_nat [simp]:
    1.17 -  "int_of_integer (integer_of_nat n) = of_nat n"
    1.18 -  by (simp add: integer_of_nat_def)
    1.19 +lemma [code_abbrev]:
    1.20 +  "integer_of_nat = of_nat"
    1.21 +  by (fact integer_of_nat_def)
    1.22  
    1.23  lemma [code_unfold]:
    1.24    "Int.nat (int_of_integer k) = nat_of_integer k"
    1.25 @@ -35,7 +37,7 @@
    1.26    by (simp add: integer_of_nat_def)
    1.27  
    1.28  lemma [code_abbrev]:
    1.29 -  "nat_of_integer (Code_Numeral_Types.Pos k) = nat_of_num k"
    1.30 +  "nat_of_integer (numeral k) = nat_of_num k"
    1.31    by (simp add: nat_of_integer_def nat_of_num_numeral)
    1.32  
    1.33  lemma [code abstract]: