2 Author: Florian Haftmann, TU Muenchen
5 header {* Type of indices *}
12 Indices are isomorphic to HOL @{typ nat} but
13 mapped to target-language builtin integers
16 subsection {* Datatype of indices *}
18 datatype index = index_of_nat nat
20 lemmas [code func del] = index.recs index.cases
23 nat_of_index :: "index \<Rightarrow> nat"
25 "nat_of_index (index_of_nat k) = k"
26 lemmas [code func del] = nat_of_index.simps
28 lemma index_id [simp]:
29 "index_of_nat (nat_of_index n) = n"
32 lemma nat_of_index_inject [simp]:
33 "nat_of_index n = nat_of_index m \<longleftrightarrow> n = m"
37 "(\<And>n\<Colon>index. PROP P n) \<equiv> (\<And>n\<Colon>nat. PROP P (index_of_nat n))"
40 assume "\<And>n\<Colon>index. PROP P n"
41 then show "PROP P (index_of_nat n)" .
44 assume "\<And>n\<Colon>nat. PROP P (index_of_nat n)"
45 then have "PROP P (index_of_nat (nat_of_index n))" .
46 then show "PROP P n" by simp
49 lemma [code func]: "size (n\<Colon>index) = 0"
53 subsection {* Indices as datatype of ints *}
55 instantiation index :: number
59 "number_of = index_of_nat o nat"
65 code_datatype "number_of \<Colon> int \<Rightarrow> index"
68 subsection {* Basic arithmetic *}
70 instantiation index :: "{minus, ordered_semidom, Divides.div, linorder}"
73 definition [simp, code func del]:
74 "(0\<Colon>index) = index_of_nat 0"
76 lemma zero_index_code [code inline, code func]:
77 "(0\<Colon>index) = Numeral0"
78 by (simp add: number_of_index_def Pls_def)
80 definition [simp, code func del]:
81 "(1\<Colon>index) = index_of_nat 1"
83 lemma one_index_code [code inline, code func]:
84 "(1\<Colon>index) = Numeral1"
85 by (simp add: number_of_index_def Pls_def Bit_def)
87 definition [simp, code func del]:
88 "n + m = index_of_nat (nat_of_index n + nat_of_index m)"
90 lemma plus_index_code [code func]:
91 "index_of_nat n + index_of_nat m = index_of_nat (n + m)"
94 definition [simp, code func del]:
95 "n - m = index_of_nat (nat_of_index n - nat_of_index m)"
97 definition [simp, code func del]:
98 "n * m = index_of_nat (nat_of_index n * nat_of_index m)"
100 lemma times_index_code [code func]:
101 "index_of_nat n * index_of_nat m = index_of_nat (n * m)"
104 definition [simp, code func del]:
105 "n div m = index_of_nat (nat_of_index n div nat_of_index m)"
107 definition [simp, code func del]:
108 "n mod m = index_of_nat (nat_of_index n mod nat_of_index m)"
110 lemma div_index_code [code func]:
111 "index_of_nat n div index_of_nat m = index_of_nat (n div m)"
114 lemma mod_index_code [code func]:
115 "index_of_nat n mod index_of_nat m = index_of_nat (n mod m)"
118 definition [simp, code func del]:
119 "n \<le> m \<longleftrightarrow> nat_of_index n \<le> nat_of_index m"
121 definition [simp, code func del]:
122 "n < m \<longleftrightarrow> nat_of_index n < nat_of_index m"
124 lemma less_eq_index_code [code func]:
125 "index_of_nat n \<le> index_of_nat m \<longleftrightarrow> n \<le> m"
128 lemma less_index_code [code func]:
129 "index_of_nat n < index_of_nat m \<longleftrightarrow> n < m"
132 instance by default (auto simp add: left_distrib index)
136 lemma index_of_nat_code [code func]:
137 "index_of_nat = of_nat"
140 have "of_nat n = index_of_nat n"
141 by (induct n) simp_all
142 then show "index_of_nat n = of_nat n"
146 lemma nat_of_index_code [code func]:
147 "nat_of_index n = (if n = 0 then 0 else Suc (nat_of_index (n - 1)))"
151 subsection {* ML interface *}
157 fun mk k = @{term index_of_nat} $ HOLogic.mk_number @{typ index} k;
163 subsection {* Code serialization *}
165 text {* Implementation of indices by bounded integers *}
172 code_instance index :: eq
176 fold (fn target => CodeTarget.add_pretty_numeral target false
177 @{const_name number_index_inst.number_of_index}
178 @{const_name Int.B0} @{const_name Int.B1}
179 @{const_name Int.Pls} @{const_name Int.Min}
180 @{const_name Int.Bit}
181 ) ["SML", "OCaml", "Haskell"]
184 code_reserved SML Int int
185 code_reserved OCaml Pervasives int
187 code_const "op + \<Colon> index \<Rightarrow> index \<Rightarrow> index"
188 (SML "Int.+ ((_), (_))")
189 (OCaml "Pervasives.+")
190 (Haskell infixl 6 "+")
192 code_const "op - \<Colon> index \<Rightarrow> index \<Rightarrow> index"
193 (SML "Int.max/ (_/ -/ _,/ 0 : int)")
194 (OCaml "Pervasives.max/ (_/ -/ _)/ (0 : int) ")
195 (Haskell "max/ (_/ -/ _)/ (0 :: Int)")
197 code_const "op * \<Colon> index \<Rightarrow> index \<Rightarrow> index"
198 (SML "Int.* ((_), (_))")
199 (OCaml "Pervasives.*")
200 (Haskell infixl 7 "*")
202 code_const "op = \<Colon> index \<Rightarrow> index \<Rightarrow> bool"
203 (SML "!((_ : Int.int) = _)")
204 (OCaml "!((_ : Pervasives.int) = _)")
205 (Haskell infixl 4 "==")
207 code_const "op \<le> \<Colon> index \<Rightarrow> index \<Rightarrow> bool"
208 (SML "Int.<= ((_), (_))")
209 (OCaml "!((_ : Pervasives.int) <= _)")
210 (Haskell infix 4 "<=")
212 code_const "op < \<Colon> index \<Rightarrow> index \<Rightarrow> bool"
213 (SML "Int.< ((_), (_))")
214 (OCaml "!((_ : Pervasives.int) < _)")
215 (Haskell infix 4 "<")
217 code_const "op div \<Colon> index \<Rightarrow> index \<Rightarrow> index"
218 (SML "IntInf.div ((_), (_))")
219 (OCaml "Big'_int.div'_big'_int")
222 code_const "op mod \<Colon> index \<Rightarrow> index \<Rightarrow> index"
223 (SML "IntInf.mod ((_), (_))")
224 (OCaml "Big'_int.mod'_big'_int")