src/HOL/Code_Numeral.thy
changeset 63174 57c0d60e491c
parent 61857 542f2c6da692
child 63950 cdc1e59aa513
     1.1 --- a/src/HOL/Code_Numeral.thy	Sun May 29 14:10:48 2016 +0200
     1.2 +++ b/src/HOL/Code_Numeral.thy	Sun May 29 14:43:17 2016 +0200
     1.3 @@ -893,9 +893,9 @@
     1.4    "Nat (integer_of_natural n) = n"
     1.5    by transfer simp
     1.6  
     1.7 -lemma [code abstract]:
     1.8 -  "integer_of_natural (natural_of_nat n) = of_nat n"
     1.9 -  by simp
    1.10 +lemma [code]:
    1.11 +  "natural_of_nat n = natural_of_integer (integer_of_nat n)"
    1.12 +  by transfer simp
    1.13  
    1.14  lemma [code abstract]:
    1.15    "integer_of_natural (natural_of_integer k) = max 0 k"
    1.16 @@ -969,7 +969,11 @@
    1.17  lifting_forget natural.lifting
    1.18  
    1.19  code_reflect Code_Numeral
    1.20 -  datatypes natural = _
    1.21 -  functions integer_of_natural natural_of_integer
    1.22 +  datatypes natural
    1.23 +  functions "Code_Numeral.Suc" "0 :: natural" "1 :: natural"
    1.24 +    "plus :: natural \<Rightarrow> _" "minus :: natural \<Rightarrow> _"
    1.25 +    "times :: natural \<Rightarrow> _" "divide :: natural \<Rightarrow> _"
    1.26 +    "Divides.mod :: natural \<Rightarrow> _"
    1.27 +    integer_of_natural natural_of_integer
    1.28  
    1.29  end