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>
```