equal
deleted
inserted
replaced
18 definition |
18 definition |
19 minus_shift :: "index \<Rightarrow> index \<Rightarrow> index \<Rightarrow> index" |
19 minus_shift :: "index \<Rightarrow> index \<Rightarrow> index \<Rightarrow> index" |
20 where |
20 where |
21 "minus_shift r k l = (if k < l then r + k - l else k - l)" |
21 "minus_shift r k l = (if k < l then r + k - l else k - l)" |
22 |
22 |
23 function |
23 fun |
24 log :: "index \<Rightarrow> index \<Rightarrow> index" |
24 log :: "index \<Rightarrow> index \<Rightarrow> index" |
25 where |
25 where |
26 "log b i = (if b \<le> 1 \<or> i < b then 1 else 1 + log b (i div b))" |
26 "log b i = (if b \<le> 1 \<or> i < b then 1 else 1 + log b (i div b))" |
27 by pat_completeness auto |
|
28 termination |
|
29 by (relation "measure (nat_of_index o snd)") |
|
30 (auto simp add: index) |
|
31 |
|
32 |
27 |
33 subsection {* Random seeds *} |
28 subsection {* Random seeds *} |
34 |
29 |
35 types seed = "index \<times> index" |
30 types seed = "index \<times> index" |
36 |
31 |