src/HOL/Library/Code_Target_Nat.thy
 author kuncar Tue Feb 25 19:07:14 2014 +0100 (2014-02-25) changeset 55736 f1ed1e9cd080 parent 54796 cdc6d8cbf770 child 57512 cc97b347b301 permissions -rw-r--r--
unregister lifting setup following the best practice of Lifting
1 (*  Title:      HOL/Library/Code_Target_Nat.thy
2     Author:     Florian Haftmann, TU Muenchen
3 *)
5 header {* Implementation of natural numbers by target-language integers *}
7 theory Code_Target_Nat
8 imports Code_Abstract_Nat
9 begin
11 subsection {* Implementation for @{typ nat} *}
13 context
14 includes natural.lifting integer.lifting
15 begin
17 lift_definition Nat :: "integer \<Rightarrow> nat"
18   is nat
19   .
21 lemma [code_post]:
22   "Nat 0 = 0"
23   "Nat 1 = 1"
24   "Nat (numeral k) = numeral k"
25   by (transfer, simp)+
27 lemma [code_abbrev]:
28   "integer_of_nat = of_nat"
29   by transfer rule
31 lemma [code_unfold]:
32   "Int.nat (int_of_integer k) = nat_of_integer k"
33   by transfer rule
35 lemma [code abstype]:
36   "Code_Target_Nat.Nat (integer_of_nat n) = n"
37   by transfer simp
39 lemma [code abstract]:
40   "integer_of_nat (nat_of_integer k) = max 0 k"
41   by transfer auto
43 lemma [code_abbrev]:
44   "nat_of_integer (numeral k) = nat_of_num k"
45   by transfer (simp add: nat_of_num_numeral)
47 lemma [code abstract]:
48   "integer_of_nat (nat_of_num n) = integer_of_num n"
49   by transfer (simp add: nat_of_num_numeral)
51 lemma [code abstract]:
52   "integer_of_nat 0 = 0"
53   by transfer simp
55 lemma [code abstract]:
56   "integer_of_nat 1 = 1"
57   by transfer simp
59 lemma [code]:
60   "Suc n = n + 1"
61   by simp
63 lemma [code abstract]:
64   "integer_of_nat (m + n) = of_nat m + of_nat n"
65   by transfer simp
67 lemma [code abstract]:
68   "integer_of_nat (m - n) = max 0 (of_nat m - of_nat n)"
69   by transfer simp
71 lemma [code abstract]:
72   "integer_of_nat (m * n) = of_nat m * of_nat n"
73   by transfer (simp add: of_nat_mult)
75 lemma [code abstract]:
76   "integer_of_nat (m div n) = of_nat m div of_nat n"
77   by transfer (simp add: zdiv_int)
79 lemma [code abstract]:
80   "integer_of_nat (m mod n) = of_nat m mod of_nat n"
81   by transfer (simp add: zmod_int)
83 lemma [code]:
84   "Divides.divmod_nat m n = (m div n, m mod n)"
85   by (fact divmod_nat_div_mod)
87 lemma [code]:
88   "HOL.equal m n = HOL.equal (of_nat m :: integer) (of_nat n)"
89   by transfer (simp add: equal)
91 lemma [code]:
92   "m \<le> n \<longleftrightarrow> (of_nat m :: integer) \<le> of_nat n"
93   by simp
95 lemma [code]:
96   "m < n \<longleftrightarrow> (of_nat m :: integer) < of_nat n"
97   by simp
99 lemma num_of_nat_code [code]:
100   "num_of_nat = num_of_integer \<circ> of_nat"
101   by transfer (simp add: fun_eq_iff)
103 end
105 lemma (in semiring_1) of_nat_code_if:
106   "of_nat n = (if n = 0 then 0
107      else let
108        (m, q) = divmod_nat n 2;
109        m' = 2 * of_nat m
110      in if q = 0 then m' else m' + 1)"
111 proof -
112   from mod_div_equality have *: "of_nat n = of_nat (n div 2 * 2 + n mod 2)" by simp
113   show ?thesis
114     by (simp add: Let_def divmod_nat_div_mod of_nat_add [symmetric])
115       (simp add: * mult_commute of_nat_mult add_commute)
116 qed
118 declare of_nat_code_if [code]
120 definition int_of_nat :: "nat \<Rightarrow> int" where
121   [code_abbrev]: "int_of_nat = of_nat"
123 lemma [code]:
124   "int_of_nat n = int_of_integer (of_nat n)"
125   by (simp add: int_of_nat_def)
127 lemma [code abstract]:
128   "integer_of_nat (nat k) = max 0 (integer_of_int k)"
129   including integer.lifting by transfer auto
131 lemma term_of_nat_code [code]:
132   -- {* Use @{term Code_Numeral.nat_of_integer} in term reconstruction
133         instead of @{term Code_Target_Nat.Nat} such that reconstructed
134         terms can be fed back to the code generator *}
135   "term_of_class.term_of n =
136    Code_Evaluation.App
137      (Code_Evaluation.Const (STR ''Code_Numeral.nat_of_integer'')
138         (typerep.Typerep (STR ''fun'')
139            [typerep.Typerep (STR ''Code_Numeral.integer'') [],
140          typerep.Typerep (STR ''Nat.nat'') []]))
141      (term_of_class.term_of (integer_of_nat n))"
142   by (simp add: term_of_anything)
144 lemma nat_of_integer_code_post [code_post]:
145   "nat_of_integer 0 = 0"
146   "nat_of_integer 1 = 1"
147   "nat_of_integer (numeral k) = numeral k"
148   including integer.lifting by (transfer, simp)+
150 code_identifier
151   code_module Code_Target_Nat \<rightharpoonup>
152     (SML) Arith and (OCaml) Arith and (Haskell) Arith
154 end