1 (* Author: Florian Haftmann, TU Muenchen *) |
|
2 |
|
3 header {* Type of indices *} |
|
4 |
|
5 theory Code_Index |
|
6 imports Main |
|
7 begin |
|
8 |
|
9 text {* |
|
10 Indices are isomorphic to HOL @{typ nat} but |
|
11 mapped to target-language builtin integers. |
|
12 *} |
|
13 |
|
14 subsection {* Datatype of indices *} |
|
15 |
|
16 typedef (open) index = "UNIV \<Colon> nat set" |
|
17 morphisms nat_of of_nat by rule |
|
18 |
|
19 lemma of_nat_nat_of [simp]: |
|
20 "of_nat (nat_of k) = k" |
|
21 by (rule nat_of_inverse) |
|
22 |
|
23 lemma nat_of_of_nat [simp]: |
|
24 "nat_of (of_nat n) = n" |
|
25 by (rule of_nat_inverse) (rule UNIV_I) |
|
26 |
|
27 lemma [measure_function]: |
|
28 "is_measure nat_of" by (rule is_measure_trivial) |
|
29 |
|
30 lemma index: |
|
31 "(\<And>n\<Colon>index. PROP P n) \<equiv> (\<And>n\<Colon>nat. PROP P (of_nat n))" |
|
32 proof |
|
33 fix n :: nat |
|
34 assume "\<And>n\<Colon>index. PROP P n" |
|
35 then show "PROP P (of_nat n)" . |
|
36 next |
|
37 fix n :: index |
|
38 assume "\<And>n\<Colon>nat. PROP P (of_nat n)" |
|
39 then have "PROP P (of_nat (nat_of n))" . |
|
40 then show "PROP P n" by simp |
|
41 qed |
|
42 |
|
43 lemma index_case: |
|
44 assumes "\<And>n. k = of_nat n \<Longrightarrow> P" |
|
45 shows P |
|
46 by (rule assms [of "nat_of k"]) simp |
|
47 |
|
48 lemma index_induct_raw: |
|
49 assumes "\<And>n. P (of_nat n)" |
|
50 shows "P k" |
|
51 proof - |
|
52 from assms have "P (of_nat (nat_of k))" . |
|
53 then show ?thesis by simp |
|
54 qed |
|
55 |
|
56 lemma nat_of_inject [simp]: |
|
57 "nat_of k = nat_of l \<longleftrightarrow> k = l" |
|
58 by (rule nat_of_inject) |
|
59 |
|
60 lemma of_nat_inject [simp]: |
|
61 "of_nat n = of_nat m \<longleftrightarrow> n = m" |
|
62 by (rule of_nat_inject) (rule UNIV_I)+ |
|
63 |
|
64 instantiation index :: zero |
|
65 begin |
|
66 |
|
67 definition [simp, code del]: |
|
68 "0 = of_nat 0" |
|
69 |
|
70 instance .. |
|
71 |
|
72 end |
|
73 |
|
74 definition [simp]: |
|
75 "Suc_index k = of_nat (Suc (nat_of k))" |
|
76 |
|
77 rep_datatype "0 \<Colon> index" Suc_index |
|
78 proof - |
|
79 fix P :: "index \<Rightarrow> bool" |
|
80 fix k :: index |
|
81 assume "P 0" then have init: "P (of_nat 0)" by simp |
|
82 assume "\<And>k. P k \<Longrightarrow> P (Suc_index k)" |
|
83 then have "\<And>n. P (of_nat n) \<Longrightarrow> P (Suc_index (of_nat n))" . |
|
84 then have step: "\<And>n. P (of_nat n) \<Longrightarrow> P (of_nat (Suc n))" by simp |
|
85 from init step have "P (of_nat (nat_of k))" |
|
86 by (induct "nat_of k") simp_all |
|
87 then show "P k" by simp |
|
88 qed simp_all |
|
89 |
|
90 declare index_case [case_names nat, cases type: index] |
|
91 declare index.induct [case_names nat, induct type: index] |
|
92 |
|
93 lemma index_decr [termination_simp]: |
|
94 "k \<noteq> Code_Index.of_nat 0 \<Longrightarrow> Code_Index.nat_of k - Suc 0 < Code_Index.nat_of k" |
|
95 by (cases k) simp |
|
96 |
|
97 lemma [simp, code]: |
|
98 "index_size = nat_of" |
|
99 proof (rule ext) |
|
100 fix k |
|
101 have "index_size k = nat_size (nat_of k)" |
|
102 by (induct k rule: index.induct) (simp_all del: zero_index_def Suc_index_def, simp_all) |
|
103 also have "nat_size (nat_of k) = nat_of k" by (induct "nat_of k") simp_all |
|
104 finally show "index_size k = nat_of k" . |
|
105 qed |
|
106 |
|
107 lemma [simp, code]: |
|
108 "size = nat_of" |
|
109 proof (rule ext) |
|
110 fix k |
|
111 show "size k = nat_of k" |
|
112 by (induct k) (simp_all del: zero_index_def Suc_index_def, simp_all) |
|
113 qed |
|
114 |
|
115 lemmas [code del] = index.recs index.cases |
|
116 |
|
117 lemma [code]: |
|
118 "eq_class.eq k l \<longleftrightarrow> eq_class.eq (nat_of k) (nat_of l)" |
|
119 by (cases k, cases l) (simp add: eq) |
|
120 |
|
121 lemma [code nbe]: |
|
122 "eq_class.eq (k::index) k \<longleftrightarrow> True" |
|
123 by (rule HOL.eq_refl) |
|
124 |
|
125 |
|
126 subsection {* Indices as datatype of ints *} |
|
127 |
|
128 instantiation index :: number |
|
129 begin |
|
130 |
|
131 definition |
|
132 "number_of = of_nat o nat" |
|
133 |
|
134 instance .. |
|
135 |
|
136 end |
|
137 |
|
138 lemma nat_of_number [simp]: |
|
139 "nat_of (number_of k) = number_of k" |
|
140 by (simp add: number_of_index_def nat_number_of_def number_of_is_id) |
|
141 |
|
142 code_datatype "number_of \<Colon> int \<Rightarrow> index" |
|
143 |
|
144 |
|
145 subsection {* Basic arithmetic *} |
|
146 |
|
147 instantiation index :: "{minus, ordered_semidom, semiring_div, linorder}" |
|
148 begin |
|
149 |
|
150 definition [simp, code del]: |
|
151 "(1\<Colon>index) = of_nat 1" |
|
152 |
|
153 definition [simp, code del]: |
|
154 "n + m = of_nat (nat_of n + nat_of m)" |
|
155 |
|
156 definition [simp, code del]: |
|
157 "n - m = of_nat (nat_of n - nat_of m)" |
|
158 |
|
159 definition [simp, code del]: |
|
160 "n * m = of_nat (nat_of n * nat_of m)" |
|
161 |
|
162 definition [simp, code del]: |
|
163 "n div m = of_nat (nat_of n div nat_of m)" |
|
164 |
|
165 definition [simp, code del]: |
|
166 "n mod m = of_nat (nat_of n mod nat_of m)" |
|
167 |
|
168 definition [simp, code del]: |
|
169 "n \<le> m \<longleftrightarrow> nat_of n \<le> nat_of m" |
|
170 |
|
171 definition [simp, code del]: |
|
172 "n < m \<longleftrightarrow> nat_of n < nat_of m" |
|
173 |
|
174 instance proof |
|
175 qed (auto simp add: index left_distrib div_mult_self1) |
|
176 |
|
177 end |
|
178 |
|
179 lemma zero_index_code [code inline, code]: |
|
180 "(0\<Colon>index) = Numeral0" |
|
181 by (simp add: number_of_index_def Pls_def) |
|
182 lemma [code post]: "Numeral0 = (0\<Colon>index)" |
|
183 using zero_index_code .. |
|
184 |
|
185 lemma one_index_code [code inline, code]: |
|
186 "(1\<Colon>index) = Numeral1" |
|
187 by (simp add: number_of_index_def Pls_def Bit1_def) |
|
188 lemma [code post]: "Numeral1 = (1\<Colon>index)" |
|
189 using one_index_code .. |
|
190 |
|
191 lemma plus_index_code [code nbe]: |
|
192 "of_nat n + of_nat m = of_nat (n + m)" |
|
193 by simp |
|
194 |
|
195 definition subtract_index :: "index \<Rightarrow> index \<Rightarrow> index" where |
|
196 [simp, code del]: "subtract_index = op -" |
|
197 |
|
198 lemma subtract_index_code [code nbe]: |
|
199 "subtract_index (of_nat n) (of_nat m) = of_nat (n - m)" |
|
200 by simp |
|
201 |
|
202 lemma minus_index_code [code]: |
|
203 "n - m = subtract_index n m" |
|
204 by simp |
|
205 |
|
206 lemma times_index_code [code nbe]: |
|
207 "of_nat n * of_nat m = of_nat (n * m)" |
|
208 by simp |
|
209 |
|
210 lemma less_eq_index_code [code nbe]: |
|
211 "of_nat n \<le> of_nat m \<longleftrightarrow> n \<le> m" |
|
212 by simp |
|
213 |
|
214 lemma less_index_code [code nbe]: |
|
215 "of_nat n < of_nat m \<longleftrightarrow> n < m" |
|
216 by simp |
|
217 |
|
218 lemma Suc_index_minus_one: "Suc_index n - 1 = n" by simp |
|
219 |
|
220 lemma of_nat_code [code]: |
|
221 "of_nat = Nat.of_nat" |
|
222 proof |
|
223 fix n :: nat |
|
224 have "Nat.of_nat n = of_nat n" |
|
225 by (induct n) simp_all |
|
226 then show "of_nat n = Nat.of_nat n" |
|
227 by (rule sym) |
|
228 qed |
|
229 |
|
230 lemma index_not_eq_zero: "i \<noteq> of_nat 0 \<longleftrightarrow> i \<ge> 1" |
|
231 by (cases i) auto |
|
232 |
|
233 definition nat_of_aux :: "index \<Rightarrow> nat \<Rightarrow> nat" where |
|
234 "nat_of_aux i n = nat_of i + n" |
|
235 |
|
236 lemma nat_of_aux_code [code]: |
|
237 "nat_of_aux i n = (if i = 0 then n else nat_of_aux (i - 1) (Suc n))" |
|
238 by (auto simp add: nat_of_aux_def index_not_eq_zero) |
|
239 |
|
240 lemma nat_of_code [code]: |
|
241 "nat_of i = nat_of_aux i 0" |
|
242 by (simp add: nat_of_aux_def) |
|
243 |
|
244 definition div_mod_index :: "index \<Rightarrow> index \<Rightarrow> index \<times> index" where |
|
245 [code del]: "div_mod_index n m = (n div m, n mod m)" |
|
246 |
|
247 lemma [code]: |
|
248 "div_mod_index n m = (if m = 0 then (0, n) else (n div m, n mod m))" |
|
249 unfolding div_mod_index_def by auto |
|
250 |
|
251 lemma [code]: |
|
252 "n div m = fst (div_mod_index n m)" |
|
253 unfolding div_mod_index_def by simp |
|
254 |
|
255 lemma [code]: |
|
256 "n mod m = snd (div_mod_index n m)" |
|
257 unfolding div_mod_index_def by simp |
|
258 |
|
259 hide (open) const of_nat nat_of |
|
260 |
|
261 subsection {* ML interface *} |
|
262 |
|
263 ML {* |
|
264 structure Index = |
|
265 struct |
|
266 |
|
267 fun mk k = HOLogic.mk_number @{typ index} k; |
|
268 |
|
269 end; |
|
270 *} |
|
271 |
|
272 |
|
273 subsection {* Code generator setup *} |
|
274 |
|
275 text {* Implementation of indices by bounded integers *} |
|
276 |
|
277 code_type index |
|
278 (SML "int") |
|
279 (OCaml "int") |
|
280 (Haskell "Int") |
|
281 |
|
282 code_instance index :: eq |
|
283 (Haskell -) |
|
284 |
|
285 setup {* |
|
286 fold (Numeral.add_code @{const_name number_index_inst.number_of_index} |
|
287 false false) ["SML", "OCaml", "Haskell"] |
|
288 *} |
|
289 |
|
290 code_reserved SML Int int |
|
291 code_reserved OCaml Pervasives int |
|
292 |
|
293 code_const "op + \<Colon> index \<Rightarrow> index \<Rightarrow> index" |
|
294 (SML "Int.+/ ((_),/ (_))") |
|
295 (OCaml "Pervasives.( + )") |
|
296 (Haskell infixl 6 "+") |
|
297 |
|
298 code_const "subtract_index \<Colon> index \<Rightarrow> index \<Rightarrow> index" |
|
299 (SML "Int.max/ (_/ -/ _,/ 0 : int)") |
|
300 (OCaml "Pervasives.max/ (_/ -/ _)/ (0 : int) ") |
|
301 (Haskell "max/ (_/ -/ _)/ (0 :: Int)") |
|
302 |
|
303 code_const "op * \<Colon> index \<Rightarrow> index \<Rightarrow> index" |
|
304 (SML "Int.*/ ((_),/ (_))") |
|
305 (OCaml "Pervasives.( * )") |
|
306 (Haskell infixl 7 "*") |
|
307 |
|
308 code_const div_mod_index |
|
309 (SML "(fn n => fn m =>/ if m = 0/ then (0, n) else/ (n div m, n mod m))") |
|
310 (OCaml "(fun n -> fun m ->/ if m = 0/ then (0, n) else/ (n '/ m, n mod m))") |
|
311 (Haskell "divMod") |
|
312 |
|
313 code_const "eq_class.eq \<Colon> index \<Rightarrow> index \<Rightarrow> bool" |
|
314 (SML "!((_ : Int.int) = _)") |
|
315 (OCaml "!((_ : int) = _)") |
|
316 (Haskell infixl 4 "==") |
|
317 |
|
318 code_const "op \<le> \<Colon> index \<Rightarrow> index \<Rightarrow> bool" |
|
319 (SML "Int.<=/ ((_),/ (_))") |
|
320 (OCaml "!((_ : int) <= _)") |
|
321 (Haskell infix 4 "<=") |
|
322 |
|
323 code_const "op < \<Colon> index \<Rightarrow> index \<Rightarrow> bool" |
|
324 (SML "Int.</ ((_),/ (_))") |
|
325 (OCaml "!((_ : int) < _)") |
|
326 (Haskell infix 4 "<") |
|
327 |
|
328 text {* Evaluation *} |
|
329 |
|
330 lemma [code, code del]: |
|
331 "(Code_Eval.term_of \<Colon> index \<Rightarrow> term) = Code_Eval.term_of" .. |
|
332 |
|
333 code_const "Code_Eval.term_of \<Colon> index \<Rightarrow> term" |
|
334 (SML "HOLogic.mk'_number/ HOLogic.indexT/ (IntInf.fromInt/ _)") |
|
335 |
|
336 end |
|