src/HOL/Library/Code_Target_Nat.thy
changeset 55736 f1ed1e9cd080
parent 54796 cdc6d8cbf770
child 57512 cc97b347b301
     1.1 --- a/src/HOL/Library/Code_Target_Nat.thy	Tue Feb 25 17:06:17 2014 +0000
     1.2 +++ b/src/HOL/Library/Code_Target_Nat.thy	Tue Feb 25 19:07:14 2014 +0100
     1.3 @@ -10,6 +10,10 @@
     1.4  
     1.5  subsection {* Implementation for @{typ nat} *}
     1.6  
     1.7 +context
     1.8 +includes natural.lifting integer.lifting
     1.9 +begin
    1.10 +
    1.11  lift_definition Nat :: "integer \<Rightarrow> nat"
    1.12    is nat
    1.13    .
    1.14 @@ -96,6 +100,8 @@
    1.15    "num_of_nat = num_of_integer \<circ> of_nat"
    1.16    by transfer (simp add: fun_eq_iff)
    1.17  
    1.18 +end
    1.19 +
    1.20  lemma (in semiring_1) of_nat_code_if:
    1.21    "of_nat n = (if n = 0 then 0
    1.22       else let
    1.23 @@ -120,7 +126,7 @@
    1.24  
    1.25  lemma [code abstract]:
    1.26    "integer_of_nat (nat k) = max 0 (integer_of_int k)"
    1.27 -  by transfer auto
    1.28 +  including integer.lifting by transfer auto
    1.29  
    1.30  lemma term_of_nat_code [code]:
    1.31    -- {* Use @{term Code_Numeral.nat_of_integer} in term reconstruction
    1.32 @@ -139,7 +145,7 @@
    1.33    "nat_of_integer 0 = 0"
    1.34    "nat_of_integer 1 = 1"
    1.35    "nat_of_integer (numeral k) = numeral k"
    1.36 -  by (transfer, simp)+
    1.37 +  including integer.lifting by (transfer, simp)+
    1.38  
    1.39  code_identifier
    1.40    code_module Code_Target_Nat \<rightharpoonup>