--- a/src/HOL/Library/Code_Target_Nat.thy Tue Feb 25 17:06:17 2014 +0000
+++ b/src/HOL/Library/Code_Target_Nat.thy Tue Feb 25 19:07:14 2014 +0100
@@ -10,6 +10,10 @@
subsection {* Implementation for @{typ nat} *}
+context
+includes natural.lifting integer.lifting
+begin
+
lift_definition Nat :: "integer \<Rightarrow> nat"
is nat
.
@@ -96,6 +100,8 @@
"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
@@ -120,7 +126,7 @@
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
@@ -139,7 +145,7 @@
"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>