author | haftmann |
Thu, 29 Nov 2007 17:08:26 +0100 | |
changeset 25502 | 9200b36280c0 |
parent 25488 | c945521fa0d9 |
child 25615 | b337edd55a07 |
permissions | -rw-r--r-- |
23854 | 1 |
(* Title: HOL/Library/Efficient_Nat.thy |
2 |
ID: $Id$ |
|
3 |
Author: Stefan Berghofer, TU Muenchen |
|
4 |
*) |
|
5 |
||
6 |
header {* Implementation of natural numbers by integers *} |
|
7 |
||
8 |
theory Efficient_Nat |
|
24994
c385c4eabb3b
consolidated naming conventions for code generator theories
haftmann
parents:
24715
diff
changeset
|
9 |
imports Main Code_Integer |
23854 | 10 |
begin |
11 |
||
12 |
text {* |
|
13 |
When generating code for functions on natural numbers, the canonical |
|
14 |
representation using @{term "0::nat"} and @{term "Suc"} is unsuitable for |
|
15 |
computations involving large numbers. The efficiency of the generated |
|
16 |
code can be improved drastically by implementing natural numbers by |
|
17 |
integers. To do this, just include this theory. |
|
18 |
*} |
|
19 |
||
20 |
subsection {* Logical rewrites *} |
|
21 |
||
22 |
text {* |
|
23 |
An int-to-nat conversion |
|
24 |
restricted to non-negative ints (in contrast to @{const nat}). |
|
25 |
Note that this restriction has no logical relevance and |
|
26 |
is just a kind of proof hint -- nothing prevents you from |
|
27 |
writing nonsense like @{term "nat_of_int (-4)"} |
|
28 |
*} |
|
29 |
||
30 |
definition |
|
31 |
nat_of_int :: "int \<Rightarrow> nat" where |
|
32 |
"k \<ge> 0 \<Longrightarrow> nat_of_int k = nat k" |
|
33 |
||
34 |
definition |
|
24715
f96d86cdbe5a
Efficient_Nat and Pretty_Int integrated with ML_Int
haftmann
parents:
24630
diff
changeset
|
35 |
int_of_nat :: "nat \<Rightarrow> int" where |
25488 | 36 |
[code func del]: "int_of_nat n = of_nat n" |
23854 | 37 |
|
24715
f96d86cdbe5a
Efficient_Nat and Pretty_Int integrated with ML_Int
haftmann
parents:
24630
diff
changeset
|
38 |
lemma int_of_nat_Suc [simp]: |
f96d86cdbe5a
Efficient_Nat and Pretty_Int integrated with ML_Int
haftmann
parents:
24630
diff
changeset
|
39 |
"int_of_nat (Suc n) = 1 + int_of_nat n" |
f96d86cdbe5a
Efficient_Nat and Pretty_Int integrated with ML_Int
haftmann
parents:
24630
diff
changeset
|
40 |
unfolding int_of_nat_def by simp |
23854 | 41 |
|
24715
f96d86cdbe5a
Efficient_Nat and Pretty_Int integrated with ML_Int
haftmann
parents:
24630
diff
changeset
|
42 |
lemma int_of_nat_add: |
f96d86cdbe5a
Efficient_Nat and Pretty_Int integrated with ML_Int
haftmann
parents:
24630
diff
changeset
|
43 |
"int_of_nat (m + n) = int_of_nat m + int_of_nat n" |
f96d86cdbe5a
Efficient_Nat and Pretty_Int integrated with ML_Int
haftmann
parents:
24630
diff
changeset
|
44 |
unfolding int_of_nat_def by (rule of_nat_add) |
23854 | 45 |
|
24715
f96d86cdbe5a
Efficient_Nat and Pretty_Int integrated with ML_Int
haftmann
parents:
24630
diff
changeset
|
46 |
lemma int_of_nat_mult: |
f96d86cdbe5a
Efficient_Nat and Pretty_Int integrated with ML_Int
haftmann
parents:
24630
diff
changeset
|
47 |
"int_of_nat (m * n) = int_of_nat m * int_of_nat n" |
f96d86cdbe5a
Efficient_Nat and Pretty_Int integrated with ML_Int
haftmann
parents:
24630
diff
changeset
|
48 |
unfolding int_of_nat_def by (rule of_nat_mult) |
23854 | 49 |
|
50 |
lemma nat_of_int_of_number_of: |
|
51 |
fixes k |
|
52 |
assumes "k \<ge> 0" |
|
53 |
shows "number_of k = nat_of_int (number_of k)" |
|
54 |
unfolding nat_of_int_def [OF assms] nat_number_of_def number_of_is_id .. |
|
55 |
||
56 |
lemma nat_of_int_of_number_of_aux: |
|
57 |
fixes k |
|
58 |
assumes "Numeral.Pls \<le> k \<equiv> True" |
|
59 |
shows "k \<ge> 0" |
|
60 |
using assms unfolding Pls_def by simp |
|
61 |
||
62 |
lemma nat_of_int_int: |
|
24715
f96d86cdbe5a
Efficient_Nat and Pretty_Int integrated with ML_Int
haftmann
parents:
24630
diff
changeset
|
63 |
"nat_of_int (int_of_nat n) = n" |
f96d86cdbe5a
Efficient_Nat and Pretty_Int integrated with ML_Int
haftmann
parents:
24630
diff
changeset
|
64 |
using nat_of_int_def int_of_nat_def by simp |
23854 | 65 |
|
24715
f96d86cdbe5a
Efficient_Nat and Pretty_Int integrated with ML_Int
haftmann
parents:
24630
diff
changeset
|
66 |
lemma eq_nat_of_int: "int_of_nat n = x \<Longrightarrow> n = nat_of_int x" |
23854 | 67 |
by (erule subst, simp only: nat_of_int_int) |
68 |
||
24423
ae9cd0e92423
overloaded definitions accompanied by explicit constants
haftmann
parents:
24222
diff
changeset
|
69 |
code_datatype nat_of_int |
ae9cd0e92423
overloaded definitions accompanied by explicit constants
haftmann
parents:
24222
diff
changeset
|
70 |
|
23854 | 71 |
text {* |
72 |
Case analysis on natural numbers is rephrased using a conditional |
|
73 |
expression: |
|
74 |
*} |
|
75 |
||
76 |
lemma [code unfold, code inline del]: |
|
77 |
"nat_case \<equiv> (\<lambda>f g n. if n = 0 then f else g (n - 1))" |
|
78 |
proof - |
|
79 |
have rewrite: "\<And>f g n. nat_case f g n = (if n = 0 then f else g (n - 1))" |
|
80 |
proof - |
|
81 |
fix f g n |
|
82 |
show "nat_case f g n = (if n = 0 then f else g (n - 1))" |
|
83 |
by (cases n) simp_all |
|
84 |
qed |
|
85 |
show "nat_case \<equiv> (\<lambda>f g n. if n = 0 then f else g (n - 1))" |
|
86 |
by (rule eq_reflection ext rewrite)+ |
|
87 |
qed |
|
88 |
||
89 |
lemma [code inline]: |
|
24715
f96d86cdbe5a
Efficient_Nat and Pretty_Int integrated with ML_Int
haftmann
parents:
24630
diff
changeset
|
90 |
"nat_case = (\<lambda>f g n. if n = 0 then f else g (nat_of_int (int_of_nat n - 1)))" |
23854 | 91 |
proof (rule ext)+ |
92 |
fix f g n |
|
24715
f96d86cdbe5a
Efficient_Nat and Pretty_Int integrated with ML_Int
haftmann
parents:
24630
diff
changeset
|
93 |
show "nat_case f g n = (if n = 0 then f else g (nat_of_int (int_of_nat n - 1)))" |
23854 | 94 |
by (cases n) (simp_all add: nat_of_int_int) |
95 |
qed |
|
96 |
||
97 |
text {* |
|
98 |
Most standard arithmetic functions on natural numbers are implemented |
|
99 |
using their counterparts on the integers: |
|
100 |
*} |
|
101 |
||
102 |
lemma [code func]: "0 = nat_of_int 0" |
|
103 |
by (simp add: nat_of_int_def) |
|
24715
f96d86cdbe5a
Efficient_Nat and Pretty_Int integrated with ML_Int
haftmann
parents:
24630
diff
changeset
|
104 |
|
23854 | 105 |
lemma [code func, code inline]: "1 = nat_of_int 1" |
106 |
by (simp add: nat_of_int_def) |
|
24715
f96d86cdbe5a
Efficient_Nat and Pretty_Int integrated with ML_Int
haftmann
parents:
24630
diff
changeset
|
107 |
|
f96d86cdbe5a
Efficient_Nat and Pretty_Int integrated with ML_Int
haftmann
parents:
24630
diff
changeset
|
108 |
lemma [code func]: "Suc n = nat_of_int (int_of_nat n + 1)" |
23854 | 109 |
by (simp add: eq_nat_of_int) |
24715
f96d86cdbe5a
Efficient_Nat and Pretty_Int integrated with ML_Int
haftmann
parents:
24630
diff
changeset
|
110 |
|
f96d86cdbe5a
Efficient_Nat and Pretty_Int integrated with ML_Int
haftmann
parents:
24630
diff
changeset
|
111 |
lemma [code]: "m + n = nat (int_of_nat m + int_of_nat n)" |
f96d86cdbe5a
Efficient_Nat and Pretty_Int integrated with ML_Int
haftmann
parents:
24630
diff
changeset
|
112 |
by (simp add: int_of_nat_def nat_eq_iff2) |
f96d86cdbe5a
Efficient_Nat and Pretty_Int integrated with ML_Int
haftmann
parents:
24630
diff
changeset
|
113 |
|
f96d86cdbe5a
Efficient_Nat and Pretty_Int integrated with ML_Int
haftmann
parents:
24630
diff
changeset
|
114 |
lemma [code func, code inline]: "m + n = nat_of_int (int_of_nat m + int_of_nat n)" |
f96d86cdbe5a
Efficient_Nat and Pretty_Int integrated with ML_Int
haftmann
parents:
24630
diff
changeset
|
115 |
by (simp add: eq_nat_of_int int_of_nat_add) |
f96d86cdbe5a
Efficient_Nat and Pretty_Int integrated with ML_Int
haftmann
parents:
24630
diff
changeset
|
116 |
|
f96d86cdbe5a
Efficient_Nat and Pretty_Int integrated with ML_Int
haftmann
parents:
24630
diff
changeset
|
117 |
lemma [code, code inline]: "m - n = nat (int_of_nat m - int_of_nat n)" |
f96d86cdbe5a
Efficient_Nat and Pretty_Int integrated with ML_Int
haftmann
parents:
24630
diff
changeset
|
118 |
by (simp add: int_of_nat_def nat_eq_iff2 of_nat_diff) |
f96d86cdbe5a
Efficient_Nat and Pretty_Int integrated with ML_Int
haftmann
parents:
24630
diff
changeset
|
119 |
|
f96d86cdbe5a
Efficient_Nat and Pretty_Int integrated with ML_Int
haftmann
parents:
24630
diff
changeset
|
120 |
lemma [code]: "m * n = nat (int_of_nat m * int_of_nat n)" |
f96d86cdbe5a
Efficient_Nat and Pretty_Int integrated with ML_Int
haftmann
parents:
24630
diff
changeset
|
121 |
unfolding int_of_nat_def |
23854 | 122 |
by (simp add: of_nat_mult [symmetric] del: of_nat_mult) |
24715
f96d86cdbe5a
Efficient_Nat and Pretty_Int integrated with ML_Int
haftmann
parents:
24630
diff
changeset
|
123 |
|
f96d86cdbe5a
Efficient_Nat and Pretty_Int integrated with ML_Int
haftmann
parents:
24630
diff
changeset
|
124 |
lemma [code func, code inline]: "m * n = nat_of_int (int_of_nat m * int_of_nat n)" |
f96d86cdbe5a
Efficient_Nat and Pretty_Int integrated with ML_Int
haftmann
parents:
24630
diff
changeset
|
125 |
by (simp add: eq_nat_of_int int_of_nat_mult) |
f96d86cdbe5a
Efficient_Nat and Pretty_Int integrated with ML_Int
haftmann
parents:
24630
diff
changeset
|
126 |
|
f96d86cdbe5a
Efficient_Nat and Pretty_Int integrated with ML_Int
haftmann
parents:
24630
diff
changeset
|
127 |
lemma [code]: "m div n = nat (int_of_nat m div int_of_nat n)" |
f96d86cdbe5a
Efficient_Nat and Pretty_Int integrated with ML_Int
haftmann
parents:
24630
diff
changeset
|
128 |
unfolding int_of_nat_def zdiv_int [symmetric] by simp |
f96d86cdbe5a
Efficient_Nat and Pretty_Int integrated with ML_Int
haftmann
parents:
24630
diff
changeset
|
129 |
|
f96d86cdbe5a
Efficient_Nat and Pretty_Int integrated with ML_Int
haftmann
parents:
24630
diff
changeset
|
130 |
lemma div_nat_code [code func]: |
f96d86cdbe5a
Efficient_Nat and Pretty_Int integrated with ML_Int
haftmann
parents:
24630
diff
changeset
|
131 |
"m div k = nat_of_int (fst (divAlg (int_of_nat m, int_of_nat k)))" |
f96d86cdbe5a
Efficient_Nat and Pretty_Int integrated with ML_Int
haftmann
parents:
24630
diff
changeset
|
132 |
unfolding div_def [symmetric] int_of_nat_def zdiv_int [symmetric] |
f96d86cdbe5a
Efficient_Nat and Pretty_Int integrated with ML_Int
haftmann
parents:
24630
diff
changeset
|
133 |
unfolding int_of_nat_def [symmetric] nat_of_int_int .. |
f96d86cdbe5a
Efficient_Nat and Pretty_Int integrated with ML_Int
haftmann
parents:
24630
diff
changeset
|
134 |
|
f96d86cdbe5a
Efficient_Nat and Pretty_Int integrated with ML_Int
haftmann
parents:
24630
diff
changeset
|
135 |
lemma [code]: "m mod n = nat (int_of_nat m mod int_of_nat n)" |
f96d86cdbe5a
Efficient_Nat and Pretty_Int integrated with ML_Int
haftmann
parents:
24630
diff
changeset
|
136 |
unfolding int_of_nat_def zmod_int [symmetric] by simp |
f96d86cdbe5a
Efficient_Nat and Pretty_Int integrated with ML_Int
haftmann
parents:
24630
diff
changeset
|
137 |
|
f96d86cdbe5a
Efficient_Nat and Pretty_Int integrated with ML_Int
haftmann
parents:
24630
diff
changeset
|
138 |
lemma mod_nat_code [code func]: |
f96d86cdbe5a
Efficient_Nat and Pretty_Int integrated with ML_Int
haftmann
parents:
24630
diff
changeset
|
139 |
"m mod k = nat_of_int (snd (divAlg (int_of_nat m, int_of_nat k)))" |
f96d86cdbe5a
Efficient_Nat and Pretty_Int integrated with ML_Int
haftmann
parents:
24630
diff
changeset
|
140 |
unfolding mod_def [symmetric] int_of_nat_def zmod_int [symmetric] |
f96d86cdbe5a
Efficient_Nat and Pretty_Int integrated with ML_Int
haftmann
parents:
24630
diff
changeset
|
141 |
unfolding int_of_nat_def [symmetric] nat_of_int_int .. |
f96d86cdbe5a
Efficient_Nat and Pretty_Int integrated with ML_Int
haftmann
parents:
24630
diff
changeset
|
142 |
|
f96d86cdbe5a
Efficient_Nat and Pretty_Int integrated with ML_Int
haftmann
parents:
24630
diff
changeset
|
143 |
lemma [code, code inline]: "(m < n) \<longleftrightarrow> (int_of_nat m < int_of_nat n)" |
f96d86cdbe5a
Efficient_Nat and Pretty_Int integrated with ML_Int
haftmann
parents:
24630
diff
changeset
|
144 |
unfolding int_of_nat_def by simp |
f96d86cdbe5a
Efficient_Nat and Pretty_Int integrated with ML_Int
haftmann
parents:
24630
diff
changeset
|
145 |
|
f96d86cdbe5a
Efficient_Nat and Pretty_Int integrated with ML_Int
haftmann
parents:
24630
diff
changeset
|
146 |
lemma [code func, code inline]: "(m \<le> n) \<longleftrightarrow> (int_of_nat m \<le> int_of_nat n)" |
f96d86cdbe5a
Efficient_Nat and Pretty_Int integrated with ML_Int
haftmann
parents:
24630
diff
changeset
|
147 |
unfolding int_of_nat_def by simp |
f96d86cdbe5a
Efficient_Nat and Pretty_Int integrated with ML_Int
haftmann
parents:
24630
diff
changeset
|
148 |
|
f96d86cdbe5a
Efficient_Nat and Pretty_Int integrated with ML_Int
haftmann
parents:
24630
diff
changeset
|
149 |
lemma [code func, code inline]: "m = n \<longleftrightarrow> int_of_nat m = int_of_nat n" |
f96d86cdbe5a
Efficient_Nat and Pretty_Int integrated with ML_Int
haftmann
parents:
24630
diff
changeset
|
150 |
unfolding int_of_nat_def by simp |
f96d86cdbe5a
Efficient_Nat and Pretty_Int integrated with ML_Int
haftmann
parents:
24630
diff
changeset
|
151 |
|
23854 | 152 |
lemma [code func]: "nat k = (if k < 0 then 0 else nat_of_int k)" |
24715
f96d86cdbe5a
Efficient_Nat and Pretty_Int integrated with ML_Int
haftmann
parents:
24630
diff
changeset
|
153 |
by (cases "k < 0") (simp, simp add: nat_of_int_def) |
f96d86cdbe5a
Efficient_Nat and Pretty_Int integrated with ML_Int
haftmann
parents:
24630
diff
changeset
|
154 |
|
23854 | 155 |
lemma [code func]: |
24715
f96d86cdbe5a
Efficient_Nat and Pretty_Int integrated with ML_Int
haftmann
parents:
24630
diff
changeset
|
156 |
"int_aux n i = (if int_of_nat n = 0 then i else int_aux (nat_of_int (int_of_nat n - 1)) (i + 1))" |
23854 | 157 |
proof - |
24715
f96d86cdbe5a
Efficient_Nat and Pretty_Int integrated with ML_Int
haftmann
parents:
24630
diff
changeset
|
158 |
have "0 < n \<Longrightarrow> int_of_nat n = 1 + int_of_nat (nat_of_int (int_of_nat n - 1))" |
23854 | 159 |
proof - |
160 |
assume prem: "n > 0" |
|
24715
f96d86cdbe5a
Efficient_Nat and Pretty_Int integrated with ML_Int
haftmann
parents:
24630
diff
changeset
|
161 |
then have "int_of_nat n - 1 \<ge> 0" unfolding int_of_nat_def by auto |
f96d86cdbe5a
Efficient_Nat and Pretty_Int integrated with ML_Int
haftmann
parents:
24630
diff
changeset
|
162 |
then have "nat_of_int (int_of_nat n - 1) = nat (int_of_nat n - 1)" by (simp add: nat_of_int_def) |
f96d86cdbe5a
Efficient_Nat and Pretty_Int integrated with ML_Int
haftmann
parents:
24630
diff
changeset
|
163 |
with prem show "int_of_nat n = 1 + int_of_nat (nat_of_int (int_of_nat n - 1))" unfolding int_of_nat_def by simp |
23854 | 164 |
qed |
24715
f96d86cdbe5a
Efficient_Nat and Pretty_Int integrated with ML_Int
haftmann
parents:
24630
diff
changeset
|
165 |
then show ?thesis unfolding int_aux_def int_of_nat_def by auto |
23854 | 166 |
qed |
167 |
||
24994
c385c4eabb3b
consolidated naming conventions for code generator theories
haftmann
parents:
24715
diff
changeset
|
168 |
lemma index_of_nat_code [code func, code inline]: |
c385c4eabb3b
consolidated naming conventions for code generator theories
haftmann
parents:
24715
diff
changeset
|
169 |
"index_of_nat n = index_of_int (int_of_nat n)" |
c385c4eabb3b
consolidated naming conventions for code generator theories
haftmann
parents:
24715
diff
changeset
|
170 |
unfolding index_of_nat_def int_of_nat_def by simp |
23854 | 171 |
|
24994
c385c4eabb3b
consolidated naming conventions for code generator theories
haftmann
parents:
24715
diff
changeset
|
172 |
lemma nat_of_index_code [code func, code inline]: |
c385c4eabb3b
consolidated naming conventions for code generator theories
haftmann
parents:
24715
diff
changeset
|
173 |
"nat_of_index k = nat (int_of_index k)" |
c385c4eabb3b
consolidated naming conventions for code generator theories
haftmann
parents:
24715
diff
changeset
|
174 |
unfolding nat_of_index_def by simp |
23854 | 175 |
|
176 |
||
177 |
subsection {* Code generator setup for basic functions *} |
|
178 |
||
179 |
text {* |
|
180 |
@{typ nat} is no longer a datatype but embedded into the integers. |
|
181 |
*} |
|
182 |
||
183 |
code_type nat |
|
24630
351a308ab58d
simplified type int (eliminated IntInf.int, integer);
wenzelm
parents:
24423
diff
changeset
|
184 |
(SML "int") |
23854 | 185 |
(OCaml "Big'_int.big'_int") |
186 |
(Haskell "Integer") |
|
187 |
||
188 |
types_code |
|
189 |
nat ("int") |
|
190 |
attach (term_of) {* |
|
24630
351a308ab58d
simplified type int (eliminated IntInf.int, integer);
wenzelm
parents:
24423
diff
changeset
|
191 |
val term_of_nat = HOLogic.mk_number HOLogic.natT; |
23854 | 192 |
*} |
193 |
attach (test) {* |
|
194 |
fun gen_nat i = random_range 0 i; |
|
195 |
*} |
|
196 |
||
197 |
consts_code |
|
198 |
"0 \<Colon> nat" ("0") |
|
199 |
Suc ("(_ + 1)") |
|
200 |
||
201 |
text {* |
|
202 |
Since natural numbers are implemented |
|
203 |
using integers, the coercion function @{const "int"} of type |
|
204 |
@{typ "nat \<Rightarrow> int"} is simply implemented by the identity function, |
|
205 |
likewise @{const nat_of_int} of type @{typ "int \<Rightarrow> nat"}. |
|
206 |
For the @{const "nat"} function for converting an integer to a natural |
|
207 |
number, we give a specific implementation using an ML function that |
|
208 |
returns its input value, provided that it is non-negative, and otherwise |
|
209 |
returns @{text "0"}. |
|
210 |
*} |
|
211 |
||
212 |
consts_code |
|
24715
f96d86cdbe5a
Efficient_Nat and Pretty_Int integrated with ML_Int
haftmann
parents:
24630
diff
changeset
|
213 |
int_of_nat ("(_)") |
23854 | 214 |
nat ("\<module>nat") |
215 |
attach {* |
|
216 |
fun nat i = if i < 0 then 0 else i; |
|
217 |
*} |
|
218 |
||
24715
f96d86cdbe5a
Efficient_Nat and Pretty_Int integrated with ML_Int
haftmann
parents:
24630
diff
changeset
|
219 |
code_const int_of_nat |
23854 | 220 |
(SML "_") |
221 |
(OCaml "_") |
|
222 |
(Haskell "_") |
|
223 |
||
224 |
code_const nat_of_int |
|
225 |
(SML "_") |
|
226 |
(OCaml "_") |
|
227 |
(Haskell "_") |
|
228 |
||
229 |
||
230 |
subsection {* Preprocessors *} |
|
231 |
||
232 |
text {* |
|
233 |
Natural numerals should be expressed using @{const nat_of_int}. |
|
234 |
*} |
|
235 |
||
236 |
lemmas [code inline del] = nat_number_of_def |
|
237 |
||
238 |
ML {* |
|
239 |
fun nat_of_int_of_number_of thy cts = |
|
240 |
let |
|
241 |
val simplify_less = Simplifier.rewrite |
|
242 |
(HOL_basic_ss addsimps (@{thms less_numeral_code} @ @{thms less_eq_numeral_code})); |
|
243 |
fun mk_rew (t, ty) = |
|
24630
351a308ab58d
simplified type int (eliminated IntInf.int, integer);
wenzelm
parents:
24423
diff
changeset
|
244 |
if ty = HOLogic.natT andalso 0 <= HOLogic.dest_numeral t then |
23854 | 245 |
Thm.capply @{cterm "(op \<le>) Numeral.Pls"} (Thm.cterm_of thy t) |
246 |
|> simplify_less |
|
247 |
|> (fn thm => @{thm nat_of_int_of_number_of_aux} OF [thm]) |
|
248 |
|> (fn thm => @{thm nat_of_int_of_number_of} OF [thm]) |
|
249 |
|> (fn thm => @{thm eq_reflection} OF [thm]) |
|
250 |
|> SOME |
|
251 |
else NONE |
|
252 |
in |
|
253 |
fold (HOLogic.add_numerals o Thm.term_of) cts [] |
|
254 |
|> map_filter mk_rew |
|
255 |
end; |
|
256 |
*} |
|
257 |
||
258 |
setup {* |
|
24222 | 259 |
Code.add_inline_proc ("nat_of_int_of_number_of", nat_of_int_of_number_of) |
23854 | 260 |
*} |
261 |
||
262 |
text {* |
|
263 |
In contrast to @{term "Suc n"}, the term @{term "n + (1::nat)"} is no longer |
|
264 |
a constructor term. Therefore, all occurrences of this term in a position |
|
265 |
where a pattern is expected (i.e.\ on the left-hand side of a recursion |
|
266 |
equation or in the arguments of an inductive relation in an introduction |
|
267 |
rule) must be eliminated. |
|
268 |
This can be accomplished by applying the following transformation rules: |
|
269 |
*} |
|
270 |
||
271 |
theorem Suc_if_eq: "(\<And>n. f (Suc n) = h n) \<Longrightarrow> f 0 = g \<Longrightarrow> |
|
272 |
f n = (if n = 0 then g else h (n - 1))" |
|
273 |
by (case_tac n) simp_all |
|
274 |
||
275 |
theorem Suc_clause: "(\<And>n. P n (Suc n)) \<Longrightarrow> n \<noteq> 0 \<Longrightarrow> P (n - 1) n" |
|
276 |
by (case_tac n) simp_all |
|
277 |
||
278 |
text {* |
|
279 |
The rules above are built into a preprocessor that is plugged into |
|
280 |
the code generator. Since the preprocessor for introduction rules |
|
281 |
does not know anything about modes, some of the modes that worked |
|
282 |
for the canonical representation of natural numbers may no longer work. |
|
283 |
*} |
|
284 |
||
285 |
(*<*) |
|
286 |
||
287 |
ML {* |
|
288 |
fun remove_suc thy thms = |
|
289 |
let |
|
290 |
val vname = Name.variant (map fst |
|
291 |
(fold (Term.add_varnames o Thm.full_prop_of) thms [])) "x"; |
|
292 |
val cv = cterm_of thy (Var ((vname, 0), HOLogic.natT)); |
|
293 |
fun lhs_of th = snd (Thm.dest_comb |
|
294 |
(fst (Thm.dest_comb (snd (Thm.dest_comb (cprop_of th)))))); |
|
295 |
fun rhs_of th = snd (Thm.dest_comb (snd (Thm.dest_comb (cprop_of th)))); |
|
296 |
fun find_vars ct = (case term_of ct of |
|
297 |
(Const ("Suc", _) $ Var _) => [(cv, snd (Thm.dest_comb ct))] |
|
298 |
| _ $ _ => |
|
299 |
let val (ct1, ct2) = Thm.dest_comb ct |
|
300 |
in |
|
301 |
map (apfst (fn ct => Thm.capply ct ct2)) (find_vars ct1) @ |
|
302 |
map (apfst (Thm.capply ct1)) (find_vars ct2) |
|
303 |
end |
|
304 |
| _ => []); |
|
305 |
val eqs = maps |
|
306 |
(fn th => map (pair th) (find_vars (lhs_of th))) thms; |
|
307 |
fun mk_thms (th, (ct, cv')) = |
|
308 |
let |
|
309 |
val th' = |
|
310 |
Thm.implies_elim |
|
311 |
(Conv.fconv_rule (Thm.beta_conversion true) |
|
312 |
(Drule.instantiate' |
|
313 |
[SOME (ctyp_of_term ct)] [SOME (Thm.cabs cv ct), |
|
314 |
SOME (Thm.cabs cv' (rhs_of th)), NONE, SOME cv'] |
|
24222 | 315 |
@{thm Suc_if_eq})) (Thm.forall_intr cv' th) |
23854 | 316 |
in |
317 |
case map_filter (fn th'' => |
|
318 |
SOME (th'', singleton |
|
319 |
(Variable.trade (K (fn [th'''] => [th''' RS th'])) (Variable.thm_context th'')) th'') |
|
320 |
handle THM _ => NONE) thms of |
|
321 |
[] => NONE |
|
322 |
| thps => |
|
323 |
let val (ths1, ths2) = split_list thps |
|
324 |
in SOME (subtract Thm.eq_thm (th :: ths1) thms @ ths2) end |
|
325 |
end |
|
326 |
in |
|
327 |
case get_first mk_thms eqs of |
|
328 |
NONE => thms |
|
329 |
| SOME x => remove_suc thy x |
|
330 |
end; |
|
331 |
||
332 |
fun eqn_suc_preproc thy ths = |
|
333 |
let |
|
24222 | 334 |
val dest = fst o HOLogic.dest_eq o HOLogic.dest_Trueprop o prop_of; |
335 |
fun contains_suc t = member (op =) (term_consts t) @{const_name Suc}; |
|
23854 | 336 |
in |
337 |
if forall (can dest) ths andalso |
|
338 |
exists (contains_suc o dest) ths |
|
339 |
then remove_suc thy ths else ths |
|
340 |
end; |
|
341 |
||
342 |
fun remove_suc_clause thy thms = |
|
343 |
let |
|
344 |
val vname = Name.variant (map fst |
|
345 |
(fold (Term.add_varnames o Thm.full_prop_of) thms [])) "x"; |
|
24222 | 346 |
fun find_var (t as Const (@{const_name Suc}, _) $ (v as Var _)) = SOME (t, v) |
23854 | 347 |
| find_var (t $ u) = (case find_var t of NONE => find_var u | x => x) |
348 |
| find_var _ = NONE; |
|
349 |
fun find_thm th = |
|
350 |
let val th' = Conv.fconv_rule ObjectLogic.atomize th |
|
351 |
in Option.map (pair (th, th')) (find_var (prop_of th')) end |
|
352 |
in |
|
353 |
case get_first find_thm thms of |
|
354 |
NONE => thms |
|
355 |
| SOME ((th, th'), (Sucv, v)) => |
|
356 |
let |
|
357 |
val cert = cterm_of (Thm.theory_of_thm th); |
|
358 |
val th'' = ObjectLogic.rulify (Thm.implies_elim |
|
359 |
(Conv.fconv_rule (Thm.beta_conversion true) |
|
360 |
(Drule.instantiate' [] |
|
361 |
[SOME (cert (lambda v (Abs ("x", HOLogic.natT, |
|
362 |
abstract_over (Sucv, |
|
363 |
HOLogic.dest_Trueprop (prop_of th')))))), |
|
24222 | 364 |
SOME (cert v)] @{thm Suc_clause})) |
23854 | 365 |
(Thm.forall_intr (cert v) th')) |
366 |
in |
|
367 |
remove_suc_clause thy (map (fn th''' => |
|
368 |
if (op = o pairself prop_of) (th''', th) then th'' else th''') thms) |
|
369 |
end |
|
370 |
end; |
|
371 |
||
372 |
fun clause_suc_preproc thy ths = |
|
373 |
let |
|
374 |
val dest = fst o HOLogic.dest_mem o HOLogic.dest_Trueprop |
|
375 |
in |
|
376 |
if forall (can (dest o concl_of)) ths andalso |
|
377 |
exists (fn th => member (op =) (foldr add_term_consts |
|
378 |
[] (map_filter (try dest) (concl_of th :: prems_of th))) "Suc") ths |
|
379 |
then remove_suc_clause thy ths else ths |
|
380 |
end; |
|
381 |
||
382 |
fun lift_obj_eq f thy = |
|
383 |
map (fn thm => thm RS @{thm meta_eq_to_obj_eq}) |
|
384 |
#> f thy |
|
385 |
#> map (fn thm => thm RS @{thm eq_reflection}) |
|
386 |
#> map (Conv.fconv_rule Drule.beta_eta_conversion) |
|
387 |
*} |
|
388 |
||
389 |
setup {* |
|
390 |
Codegen.add_preprocessor eqn_suc_preproc |
|
391 |
#> Codegen.add_preprocessor clause_suc_preproc |
|
24222 | 392 |
#> Code.add_preproc ("eqn_Suc", lift_obj_eq eqn_suc_preproc) |
393 |
#> Code.add_preproc ("clause_Suc", lift_obj_eq clause_suc_preproc) |
|
23854 | 394 |
*} |
395 |
(*>*) |
|
396 |
||
397 |
||
398 |
subsection {* Module names *} |
|
399 |
||
400 |
code_modulename SML |
|
401 |
Nat Integer |
|
402 |
Divides Integer |
|
403 |
Efficient_Nat Integer |
|
404 |
||
405 |
code_modulename OCaml |
|
406 |
Nat Integer |
|
407 |
Divides Integer |
|
408 |
Efficient_Nat Integer |
|
409 |
||
410 |
code_modulename Haskell |
|
411 |
Nat Integer |
|
24195 | 412 |
Divides Integer |
23854 | 413 |
Efficient_Nat Integer |
414 |
||
24715
f96d86cdbe5a
Efficient_Nat and Pretty_Int integrated with ML_Int
haftmann
parents:
24630
diff
changeset
|
415 |
hide const nat_of_int int_of_nat |
23854 | 416 |
|
417 |
end |