equal
deleted
inserted
replaced
1 (* Author: Florian Haftmann, TU Muenchen *) |
1 (* Author: Florian Haftmann, TU Muenchen *) |
2 |
2 |
3 header {* Type of indices *} |
3 header {* Type of indices *} |
4 |
4 |
5 theory Code_Index |
5 theory Code_Index |
6 imports Main |
6 imports Nat_Numeral |
7 begin |
7 begin |
8 |
8 |
9 text {* |
9 text {* |
10 Indices are isomorphic to HOL @{typ nat} but |
10 Indices are isomorphic to HOL @{typ nat} but |
11 mapped to target-language builtin integers. |
11 mapped to target-language builtin integers. |
262 lemma int_of_code [code]: |
262 lemma int_of_code [code]: |
263 "int_of k = (if k = 0 then 0 |
263 "int_of k = (if k = 0 then 0 |
264 else (if k mod 2 = 0 then 2 * int_of (k div 2) else 2 * int_of (k div 2) + 1))" |
264 else (if k mod 2 = 0 then 2 * int_of (k div 2) else 2 * int_of (k div 2) + 1))" |
265 by (auto simp add: int_of_def mod_div_equality') |
265 by (auto simp add: int_of_def mod_div_equality') |
266 |
266 |
267 lemma (in term_syntax) term_of_index_code [code]: |
|
268 "Code_Eval.term_of k = |
|
269 Code_Eval.termify (number_of :: int \<Rightarrow> int) <\<cdot>> Code_Eval.term_of_num (2::index) k" |
|
270 by (simp only: term_of_anything) |
|
271 |
|
272 hide (open) const of_nat nat_of int_of |
267 hide (open) const of_nat nat_of int_of |
273 |
268 |
274 |
269 |
275 subsection {* Code generator setup *} |
270 subsection {* Code generator setup *} |
276 |
271 |