src/HOL/Library/Random.thy
changeset 30495 a5f1e4f46d14
parent 29823 0ab754d13ccd
child 30500 072daf3914c0
equal deleted 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