equal
deleted
inserted
replaced
254 |
254 |
255 lemma [code]: |
255 lemma [code]: |
256 "n mod m = snd (div_mod_index n m)" |
256 "n mod m = snd (div_mod_index n m)" |
257 unfolding div_mod_index_def by simp |
257 unfolding div_mod_index_def by simp |
258 |
258 |
259 hide (open) const of_nat nat_of |
259 definition int_of :: "index \<Rightarrow> int" where |
260 |
260 "int_of = Nat.of_nat o nat_of" |
261 subsection {* ML interface *} |
261 |
262 |
262 lemma int_of_code [code]: |
263 ML {* |
263 "int_of k = (if k = 0 then 0 |
264 structure Index = |
264 else (if k mod 2 = 0 then 2 * int_of (k div 2) else 2 * int_of (k div 2) + 1))" |
265 struct |
265 by (auto simp add: int_of_def mod_div_equality') |
266 |
266 |
267 fun mk k = HOLogic.mk_number @{typ index} k; |
267 lemma (in term_syntax) term_of_index_code [code]: |
268 |
268 "Code_Eval.term_of k = |
269 end; |
269 Code_Eval.termify (number_of :: int \<Rightarrow> int) <\<cdot>> Code_Eval.term_of_num (2::index) k" |
270 *} |
270 by (simp only: term_of_anything) |
|
271 |
|
272 hide (open) const of_nat nat_of int_of |
271 |
273 |
272 |
274 |
273 subsection {* Code generator setup *} |
275 subsection {* Code generator setup *} |
274 |
276 |
275 text {* Implementation of indices by bounded integers *} |
277 text {* Implementation of indices by bounded integers *} |
323 code_const "op < \<Colon> index \<Rightarrow> index \<Rightarrow> bool" |
325 code_const "op < \<Colon> index \<Rightarrow> index \<Rightarrow> bool" |
324 (SML "Int.</ ((_),/ (_))") |
326 (SML "Int.</ ((_),/ (_))") |
325 (OCaml "!((_ : int) < _)") |
327 (OCaml "!((_ : int) < _)") |
326 (Haskell infix 4 "<") |
328 (Haskell infix 4 "<") |
327 |
329 |
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 |
330 end |