141 subsection {* Basic arithmetic *} |
144 subsection {* Basic arithmetic *} |
142 |
145 |
143 instantiation index :: "{minus, ordered_semidom, Divides.div, linorder}" |
146 instantiation index :: "{minus, ordered_semidom, Divides.div, linorder}" |
144 begin |
147 begin |
145 |
148 |
|
149 definition [simp, code del]: |
|
150 "(1\<Colon>index) = index_of_nat 1" |
|
151 |
|
152 definition [simp, code del]: |
|
153 "n + m = index_of_nat (nat_of_index n + nat_of_index m)" |
|
154 |
|
155 definition [simp, code del]: |
|
156 "n - m = index_of_nat (nat_of_index n - nat_of_index m)" |
|
157 |
|
158 definition [simp, code del]: |
|
159 "n * m = index_of_nat (nat_of_index n * nat_of_index m)" |
|
160 |
|
161 definition [simp, code del]: |
|
162 "n div m = index_of_nat (nat_of_index n div nat_of_index m)" |
|
163 |
|
164 definition [simp, code del]: |
|
165 "n mod m = index_of_nat (nat_of_index n mod nat_of_index m)" |
|
166 |
|
167 definition [simp, code del]: |
|
168 "n \<le> m \<longleftrightarrow> nat_of_index n \<le> nat_of_index m" |
|
169 |
|
170 definition [simp, code del]: |
|
171 "n < m \<longleftrightarrow> nat_of_index n < nat_of_index m" |
|
172 |
|
173 instance by default (auto simp add: left_distrib index) |
|
174 |
|
175 end |
|
176 |
146 lemma zero_index_code [code inline, code]: |
177 lemma zero_index_code [code inline, code]: |
147 "(0\<Colon>index) = Numeral0" |
178 "(0\<Colon>index) = Numeral0" |
148 by (simp add: number_of_index_def Pls_def) |
179 by (simp add: number_of_index_def Pls_def) |
149 lemma [code post]: "Numeral0 = (0\<Colon>index)" |
180 lemma [code post]: "Numeral0 = (0\<Colon>index)" |
150 using zero_index_code .. |
181 using zero_index_code .. |
151 |
182 |
152 definition [simp, code del]: |
|
153 "(1\<Colon>index) = index_of_nat 1" |
|
154 |
|
155 lemma one_index_code [code inline, code]: |
183 lemma one_index_code [code inline, code]: |
156 "(1\<Colon>index) = Numeral1" |
184 "(1\<Colon>index) = Numeral1" |
157 by (simp add: number_of_index_def Pls_def Bit1_def) |
185 by (simp add: number_of_index_def Pls_def Bit1_def) |
158 lemma [code post]: "Numeral1 = (1\<Colon>index)" |
186 lemma [code post]: "Numeral1 = (1\<Colon>index)" |
159 using one_index_code .. |
187 using one_index_code .. |
160 |
188 |
161 definition [simp, code del]: |
189 lemma plus_index_code [code nbe]: |
162 "n + m = index_of_nat (nat_of_index n + nat_of_index m)" |
|
163 |
|
164 lemma plus_index_code [code]: |
|
165 "index_of_nat n + index_of_nat m = index_of_nat (n + m)" |
190 "index_of_nat n + index_of_nat m = index_of_nat (n + m)" |
166 by simp |
191 by simp |
167 |
192 |
168 definition [simp, code del]: |
193 definition subtract_index :: "index \<Rightarrow> index \<Rightarrow> index" where |
169 "n - m = index_of_nat (nat_of_index n - nat_of_index m)" |
194 [simp, code del]: "subtract_index = op -" |
170 |
195 |
171 definition [simp, code del]: |
196 lemma subtract_index_code [code nbe]: |
172 "n * m = index_of_nat (nat_of_index n * nat_of_index m)" |
197 "subtract_index (index_of_nat n) (index_of_nat m) = index_of_nat (n - m)" |
173 |
198 by simp |
174 lemma times_index_code [code]: |
199 |
|
200 lemma minus_index_code [code]: |
|
201 "n - m = subtract_index n m" |
|
202 by simp |
|
203 |
|
204 lemma times_index_code [code nbe]: |
175 "index_of_nat n * index_of_nat m = index_of_nat (n * m)" |
205 "index_of_nat n * index_of_nat m = index_of_nat (n * m)" |
176 by simp |
206 by simp |
177 |
207 |
178 definition [simp, code del]: |
208 lemma less_eq_index_code [code nbe]: |
179 "n div m = index_of_nat (nat_of_index n div nat_of_index m)" |
|
180 |
|
181 definition [simp, code del]: |
|
182 "n mod m = index_of_nat (nat_of_index n mod nat_of_index m)" |
|
183 |
|
184 lemma div_index_code [code]: |
|
185 "index_of_nat n div index_of_nat m = index_of_nat (n div m)" |
|
186 by simp |
|
187 |
|
188 lemma mod_index_code [code]: |
|
189 "index_of_nat n mod index_of_nat m = index_of_nat (n mod m)" |
|
190 by simp |
|
191 |
|
192 definition [simp, code del]: |
|
193 "n \<le> m \<longleftrightarrow> nat_of_index n \<le> nat_of_index m" |
|
194 |
|
195 definition [simp, code del]: |
|
196 "n < m \<longleftrightarrow> nat_of_index n < nat_of_index m" |
|
197 |
|
198 lemma less_eq_index_code [code]: |
|
199 "index_of_nat n \<le> index_of_nat m \<longleftrightarrow> n \<le> m" |
209 "index_of_nat n \<le> index_of_nat m \<longleftrightarrow> n \<le> m" |
200 by simp |
210 by simp |
201 |
211 |
202 lemma less_index_code [code]: |
212 lemma less_index_code [code nbe]: |
203 "index_of_nat n < index_of_nat m \<longleftrightarrow> n < m" |
213 "index_of_nat n < index_of_nat m \<longleftrightarrow> n < m" |
204 by simp |
214 by simp |
205 |
|
206 instance by default (auto simp add: left_distrib index) |
|
207 |
|
208 end |
|
209 |
215 |
210 lemma Suc_index_minus_one: "Suc_index n - 1 = n" by simp |
216 lemma Suc_index_minus_one: "Suc_index n - 1 = n" by simp |
211 |
217 |
212 lemma index_of_nat_code [code]: |
218 lemma index_of_nat_code [code]: |
213 "index_of_nat = of_nat" |
219 "index_of_nat = of_nat" |
220 qed |
226 qed |
221 |
227 |
222 lemma index_not_eq_zero: "i \<noteq> index_of_nat 0 \<longleftrightarrow> i \<ge> 1" |
228 lemma index_not_eq_zero: "i \<noteq> index_of_nat 0 \<longleftrightarrow> i \<ge> 1" |
223 by (cases i) auto |
229 by (cases i) auto |
224 |
230 |
225 definition |
231 definition nat_of_index_aux :: "index \<Rightarrow> nat \<Rightarrow> nat" where |
226 nat_of_index_aux :: "index \<Rightarrow> nat \<Rightarrow> nat" |
|
227 where |
|
228 "nat_of_index_aux i n = nat_of_index i + n" |
232 "nat_of_index_aux i n = nat_of_index i + n" |
229 |
233 |
230 lemma nat_of_index_aux_code [code]: |
234 lemma nat_of_index_aux_code [code]: |
231 "nat_of_index_aux i n = (if i = 0 then n else nat_of_index_aux (i - 1) (Suc n))" |
235 "nat_of_index_aux i n = (if i = 0 then n else nat_of_index_aux (i - 1) (Suc n))" |
232 by (auto simp add: nat_of_index_aux_def index_not_eq_zero) |
236 by (auto simp add: nat_of_index_aux_def index_not_eq_zero) |
233 |
237 |
234 lemma nat_of_index_code [code]: |
238 lemma nat_of_index_code [code]: |
235 "nat_of_index i = nat_of_index_aux i 0" |
239 "nat_of_index i = nat_of_index_aux i 0" |
236 by (simp add: nat_of_index_aux_def) |
240 by (simp add: nat_of_index_aux_def) |
237 |
241 |
238 |
242 definition div_mod_index :: "index \<Rightarrow> index \<Rightarrow> index \<times> index" where |
239 text {* Measure function (for termination proofs) *} |
243 [code del]: "div_mod_index n m = (n div m, n mod m)" |
240 |
244 |
241 lemma [measure_function]: |
245 lemma [code]: |
242 "is_measure nat_of_index" by (rule is_measure_trivial) |
246 "div_mod_index n m = (if m = 0 then (0, n) else (n div m, n mod m))" |
|
247 unfolding div_mod_index_def by auto |
|
248 |
|
249 lemma [code]: |
|
250 "n div m = fst (div_mod_index n m)" |
|
251 unfolding div_mod_index_def by simp |
|
252 |
|
253 lemma [code]: |
|
254 "n mod m = snd (div_mod_index n m)" |
|
255 unfolding div_mod_index_def by simp |
|
256 |
243 |
257 |
244 subsection {* ML interface *} |
258 subsection {* ML interface *} |
245 |
259 |
246 ML {* |
260 ML {* |
247 structure Index = |
261 structure Index = |
249 |
263 |
250 fun mk k = HOLogic.mk_number @{typ index} k; |
264 fun mk k = HOLogic.mk_number @{typ index} k; |
251 |
265 |
252 end; |
266 end; |
253 *} |
267 *} |
254 |
|
255 |
|
256 subsection {* Specialized @{term "op - \<Colon> index \<Rightarrow> index \<Rightarrow> index"}, |
|
257 @{term "op div \<Colon> index \<Rightarrow> index \<Rightarrow> index"} and @{term "op mod \<Colon> index \<Rightarrow> index \<Rightarrow> index"} |
|
258 operations *} |
|
259 |
|
260 definition |
|
261 minus_index_aux :: "index \<Rightarrow> index \<Rightarrow> index" |
|
262 where |
|
263 [code del]: "minus_index_aux = op -" |
|
264 |
|
265 lemma [code]: "op - = minus_index_aux" |
|
266 using minus_index_aux_def .. |
|
267 |
|
268 definition |
|
269 div_mod_index :: "index \<Rightarrow> index \<Rightarrow> index \<times> index" |
|
270 where |
|
271 [code del]: "div_mod_index n m = (n div m, n mod m)" |
|
272 |
|
273 lemma [code]: |
|
274 "div_mod_index n m = (if m = 0 then (0, n) else (n div m, n mod m))" |
|
275 unfolding div_mod_index_def by auto |
|
276 |
|
277 lemma [code]: |
|
278 "n div m = fst (div_mod_index n m)" |
|
279 unfolding div_mod_index_def by simp |
|
280 |
|
281 lemma [code]: |
|
282 "n mod m = snd (div_mod_index n m)" |
|
283 unfolding div_mod_index_def by simp |
|
284 |
268 |
285 |
269 |
286 subsection {* Code generator setup *} |
270 subsection {* Code generator setup *} |
287 |
271 |
288 text {* Implementation of indices by bounded integers *} |
272 text {* Implementation of indices by bounded integers *} |
306 code_const "op + \<Colon> index \<Rightarrow> index \<Rightarrow> index" |
290 code_const "op + \<Colon> index \<Rightarrow> index \<Rightarrow> index" |
307 (SML "Int.+/ ((_),/ (_))") |
291 (SML "Int.+/ ((_),/ (_))") |
308 (OCaml "Pervasives.( + )") |
292 (OCaml "Pervasives.( + )") |
309 (Haskell infixl 6 "+") |
293 (Haskell infixl 6 "+") |
310 |
294 |
311 code_const "minus_index_aux \<Colon> index \<Rightarrow> index \<Rightarrow> index" |
295 code_const "subtract_index \<Colon> index \<Rightarrow> index \<Rightarrow> index" |
312 (SML "Int.max/ (_/ -/ _,/ 0 : int)") |
296 (SML "Int.max/ (_/ -/ _,/ 0 : int)") |
313 (OCaml "Pervasives.max/ (_/ -/ _)/ (0 : int) ") |
297 (OCaml "Pervasives.max/ (_/ -/ _)/ (0 : int) ") |
314 (Haskell "max/ (_/ -/ _)/ (0 :: Int)") |
298 (Haskell "max/ (_/ -/ _)/ (0 :: Int)") |
315 |
299 |
316 code_const "op * \<Colon> index \<Rightarrow> index \<Rightarrow> index" |
300 code_const "op * \<Colon> index \<Rightarrow> index \<Rightarrow> index" |