src/HOL/Library/Random.thy
 changeset 30495 a5f1e4f46d14 parent 29823 0ab754d13ccd child 30500 072daf3914c0
equal inserted replaced
30494:c150e6fa4e0d 30495:a5f1e4f46d14
`    18 definition minus_shift :: "index \<Rightarrow> index \<Rightarrow> index \<Rightarrow> index" where`
`    18 definition minus_shift :: "index \<Rightarrow> index \<Rightarrow> index \<Rightarrow> index" where`
`    19   "minus_shift r k l = (if k < l then r + k - l else k - l)"`
`    19   "minus_shift r k l = (if k < l then r + k - l else k - l)"`
`    20 `
`    20 `
`    21 fun log :: "index \<Rightarrow> index \<Rightarrow> index" where`
`    21 fun log :: "index \<Rightarrow> index \<Rightarrow> index" where`
`    22   "log b i = (if b \<le> 1 \<or> i < b then 1 else 1 + log b (i div b))"`
`    22   "log b i = (if b \<le> 1 \<or> i < b then 1 else 1 + log b (i div b))"`
`       `
`    23 `
`    23 `
`    24 `
`    24 subsection {* Random seeds *}`
`    25 subsection {* Random seeds *}`
`    25 `
`    26 `
`    26 types seed = "index \<times> index"`
`    27 types seed = "index \<times> index"`
`    27 `
`    28 `
`    55    in (s'', s'''))"`
`    56    in (s'', s'''))"`
`    56 `
`    57 `
`    57 `
`    58 `
`    58 subsection {* Base selectors *}`
`    59 subsection {* Base selectors *}`
`    59 `
`    60 `
`    60 function range_aux :: "index \<Rightarrow> index \<Rightarrow> seed \<Rightarrow> index \<times> seed" where`
`    61 fun %quote iterate :: "index \<Rightarrow> ('b \<Rightarrow> 'a \<Rightarrow> 'b \<times> 'a) \<Rightarrow> 'b \<Rightarrow> 'a \<Rightarrow> 'b \<times> 'a" where`
`    61   "range_aux k l s = (if k = 0 then (l, s) else`
`    62   "iterate k f x = (if k = 0 then Pair x else f x o\<rightarrow> iterate (k - 1) f)"`
`    62     let (v, s') = next s`
`       `
`    63   in range_aux (k - 1) (v + l * 2147483561) s')"`
`       `
`    64 by pat_completeness auto`
`       `
`    65 termination`
`       `
`    66   by (relation "measure (Code_Index.nat_of o fst)")`
`       `
`    67     (auto simp add: index)`
`       `
`    68 `
`    63 `
`    69 definition range :: "index \<Rightarrow> seed \<Rightarrow> index \<times> seed" where`
`    64 definition %quote range :: "index \<Rightarrow> seed \<Rightarrow> index \<times> seed" where`
`    70   "range k = range_aux (log 2147483561 k) 1`
`    65   "range k = iterate (log 2147483561 k)`
`       `
`    66       (\<lambda>l. next o\<rightarrow> (\<lambda>v. Pair (v + l * 2147483561))) 1`
`    71     o\<rightarrow> (\<lambda>v. Pair (v mod k))"`
`    67     o\<rightarrow> (\<lambda>v. Pair (v mod k))"`
`    72 `
`    68 `
`    73 lemma range:`
`    69 lemma range:`
`    74   assumes "k > 0"`
`    70   "k > 0 \<Longrightarrow> fst (range k s) < k"`
`    75   shows "fst (range k s) < k"`
`    71   by (simp add: range_def scomp_apply split_def del: log.simps iterate.simps)`
`    76 proof -`
`       `
`    77   obtain v w where range_aux:`
`       `
`    78     "range_aux (log 2147483561 k) 1 s = (v, w)"`
`       `
`    79     by (cases "range_aux (log 2147483561 k) 1 s")`
`       `
`    80   with assms show ?thesis`
`       `
`    81     by (simp add: scomp_apply range_def del: range_aux.simps log.simps)`
`       `
`    82 qed`
`       `
`    83 `
`    72 `
`    84 definition select :: "'a list \<Rightarrow> seed \<Rightarrow> 'a \<times> seed" where`
`    73 definition select :: "'a list \<Rightarrow> seed \<Rightarrow> 'a \<times> seed" where`
`    85   "select xs = range (Code_Index.of_nat (length xs))`
`    74   "select xs = range (Code_Index.of_nat (length xs))`
`    86     o\<rightarrow> (\<lambda>k. Pair (nth xs (Code_Index.nat_of k)))"`
`    75     o\<rightarrow> (\<lambda>k. Pair (nth xs (Code_Index.nat_of k)))"`
`    87      `
`    76      `