src/HOL/Library/Code_Target_Nat.thy

 theory Code_Target_Nat
 imports Code_Abstract_Nat
 begin
 
 subsection {* Implementation for @{typ nat} *}
+
+context
+includes natural.lifting integer.lifting
+begin
 
 lift_definition Nat :: "integer \<Rightarrow> nat"
   is nat
   .
 

 
 lemma num_of_nat_code [code]:
   "num_of_nat = num_of_integer \<circ> of_nat"
   by transfer (simp add: fun_eq_iff)
 
+end
+
 lemma (in semiring_1) of_nat_code_if:
   "of_nat n = (if n = 0 then 0
      else let
        (m, q) = divmod_nat n 2;
        m' = 2 * of_nat m

   "int_of_nat n = int_of_integer (of_nat n)"
   by (simp add: int_of_nat_def)
 
 lemma [code abstract]:
   "integer_of_nat (nat k) = max 0 (integer_of_int k)"
-  by transfer auto
+  including integer.lifting by transfer auto
 
 lemma term_of_nat_code [code]:
   -- {* Use @{term Code_Numeral.nat_of_integer} in term reconstruction
         instead of @{term Code_Target_Nat.Nat} such that reconstructed
         terms can be fed back to the code generator *}

 
 lemma nat_of_integer_code_post [code_post]:
   "nat_of_integer 0 = 0"
   "nat_of_integer 1 = 1"
   "nat_of_integer (numeral k) = numeral k"
-  by (transfer, simp)+
+  including integer.lifting by (transfer, simp)+
 
 code_identifier
   code_module Code_Target_Nat \<rightharpoonup>
     (SML) Arith and (OCaml) Arith and (Haskell) Arith