src/HOL/Library/Code_Target_Nat.thy
 author haftmann Mon Jun 05 15:59:41 2017 +0200 (2017-06-05) changeset 66010 2f7d39285a1a parent 64997 067a6cca39f0 child 66190 a41435469559 permissions -rw-r--r--
executable domain membership checks
1 (*  Title:      HOL/Library/Code_Target_Nat.thy
2     Author:     Florian Haftmann, TU Muenchen
3 *)
5 section \<open>Implementation of natural numbers by target-language integers\<close>
7 theory Code_Target_Nat
8 imports Code_Abstract_Nat
9 begin
11 subsection \<open>Implementation for @{typ nat}\<close>
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 context
48 begin
50 qualified definition natural :: "num \<Rightarrow> nat"
51   where [simp]: "natural = nat_of_num"
53 lemma [code_computation_unfold]:
54   "numeral = natural"
55   "nat_of_num = natural"
58 end
60 lemma [code abstract]:
61   "integer_of_nat (nat_of_num n) = integer_of_num n"
62   by transfer (simp add: nat_of_num_numeral)
64 lemma [code abstract]:
65   "integer_of_nat 0 = 0"
66   by transfer simp
68 lemma [code abstract]:
69   "integer_of_nat 1 = 1"
70   by transfer simp
72 lemma [code]:
73   "Suc n = n + 1"
74   by simp
76 lemma [code abstract]:
77   "integer_of_nat (m + n) = of_nat m + of_nat n"
78   by transfer simp
80 lemma [code abstract]:
81   "integer_of_nat (m - n) = max 0 (of_nat m - of_nat n)"
82   by transfer simp
84 lemma [code abstract]:
85   "integer_of_nat (m * n) = of_nat m * of_nat n"
86   by transfer (simp add: of_nat_mult)
88 lemma [code abstract]:
89   "integer_of_nat (m div n) = of_nat m div of_nat n"
90   by transfer (simp add: zdiv_int)
92 lemma [code abstract]:
93   "integer_of_nat (m mod n) = of_nat m mod of_nat n"
94   by transfer (simp add: zmod_int)
96 lemma [code]:
97   "Divides.divmod_nat m n = (m div n, m mod n)"
98   by (fact divmod_nat_div_mod)
100 lemma [code]:
101   "divmod m n = map_prod nat_of_integer nat_of_integer (divmod m n)"
102   by (simp only: prod_eq_iff divmod_def map_prod_def case_prod_beta fst_conv snd_conv)
103     (transfer, simp_all only: nat_div_distrib nat_mod_distrib
104         zero_le_numeral nat_numeral)
106 lemma [code]:
107   "HOL.equal m n = HOL.equal (of_nat m :: integer) (of_nat n)"
108   by transfer (simp add: equal)
110 lemma [code]:
111   "m \<le> n \<longleftrightarrow> (of_nat m :: integer) \<le> of_nat n"
112   by simp
114 lemma [code]:
115   "m < n \<longleftrightarrow> (of_nat m :: integer) < of_nat n"
116   by simp
118 lemma num_of_nat_code [code]:
119   "num_of_nat = num_of_integer \<circ> of_nat"
120   by transfer (simp add: fun_eq_iff)
122 end
124 lemma (in semiring_1) of_nat_code_if:
125   "of_nat n = (if n = 0 then 0
126      else let
127        (m, q) = Divides.divmod_nat n 2;
128        m' = 2 * of_nat m
129      in if q = 0 then m' else m' + 1)"
130 proof -
131   from div_mult_mod_eq have *: "of_nat n = of_nat (n div 2 * 2 + n mod 2)" by simp
132   show ?thesis
135 qed
137 declare of_nat_code_if [code]
139 definition int_of_nat :: "nat \<Rightarrow> int" where
140   [code_abbrev]: "int_of_nat = of_nat"
142 lemma [code]:
143   "int_of_nat n = int_of_integer (of_nat n)"
146 lemma [code abstract]:
147   "integer_of_nat (nat k) = max 0 (integer_of_int k)"
148   including integer.lifting by transfer auto
150 lemma term_of_nat_code [code]:
151   \<comment> \<open>Use @{term Code_Numeral.nat_of_integer} in term reconstruction
152         instead of @{term Code_Target_Nat.Nat} such that reconstructed
153         terms can be fed back to the code generator\<close>
154   "term_of_class.term_of n =
155    Code_Evaluation.App
156      (Code_Evaluation.Const (STR ''Code_Numeral.nat_of_integer'')
157         (typerep.Typerep (STR ''fun'')
158            [typerep.Typerep (STR ''Code_Numeral.integer'') [],
159          typerep.Typerep (STR ''Nat.nat'') []]))
160      (term_of_class.term_of (integer_of_nat n))"