equal
deleted
inserted
replaced
279 unfolding of_nat_mult of_nat_add by simp |
279 unfolding of_nat_mult of_nat_add by simp |
280 then show ?thesis by (auto simp add: int_of_def mult_ac) |
280 then show ?thesis by (auto simp add: int_of_def mult_ac) |
281 qed |
281 qed |
282 |
282 |
283 |
283 |
284 text {* Lazy Evaluation of an indexed function *} |
284 hide_const (open) of_nat nat_of Suc subtract int_of |
285 |
|
286 function iterate_upto :: "(code_numeral \<Rightarrow> 'a) \<Rightarrow> code_numeral \<Rightarrow> code_numeral \<Rightarrow> 'a Predicate.pred" |
|
287 where |
|
288 "iterate_upto f n m = |
|
289 Predicate.Seq (%u. if n > m then Predicate.Empty |
|
290 else Predicate.Insert (f n) (iterate_upto f (n + 1) m))" |
|
291 by pat_completeness auto |
|
292 |
|
293 termination by (relation "measure (%(f, n, m). Code_Numeral.nat_of (m + 1 - n))") auto |
|
294 |
|
295 hide_const (open) of_nat nat_of Suc subtract int_of iterate_upto |
|
296 |
285 |
297 |
286 |
298 subsection {* Code generator setup *} |
287 subsection {* Code generator setup *} |
299 |
288 |
300 text {* Implementation of code numerals by bounded integers *} |
289 text {* Implementation of code numerals by bounded integers *} |
375 |
364 |
376 code_modulename Haskell |
365 code_modulename Haskell |
377 Code_Numeral Arith |
366 Code_Numeral Arith |
378 |
367 |
379 end |
368 end |
|
369 |