src/HOL/Random.thy
changeset 33236 ea75c6ea643e
parent 32740 9dd0a2f83429
child 35266 07a56610c00b
     1.1 --- a/src/HOL/Random.thy	Tue Oct 27 15:32:20 2009 +0100
     1.2 +++ b/src/HOL/Random.thy	Tue Oct 27 15:32:21 2009 +0100
     1.3 @@ -12,15 +12,15 @@
     1.4  
     1.5  subsection {* Auxiliary functions *}
     1.6  
     1.7 +fun log :: "code_numeral \<Rightarrow> code_numeral \<Rightarrow> code_numeral" where
     1.8 +  "log b i = (if b \<le> 1 \<or> i < b then 1 else 1 + log b (i div b))"
     1.9 +
    1.10  definition inc_shift :: "code_numeral \<Rightarrow> code_numeral \<Rightarrow> code_numeral" where
    1.11    "inc_shift v k = (if v = k then 1 else k + 1)"
    1.12  
    1.13  definition minus_shift :: "code_numeral \<Rightarrow> code_numeral \<Rightarrow> code_numeral \<Rightarrow> code_numeral" where
    1.14    "minus_shift r k l = (if k < l then r + k - l else k - l)"
    1.15  
    1.16 -fun log :: "code_numeral \<Rightarrow> code_numeral \<Rightarrow> code_numeral" where
    1.17 -  "log b i = (if b \<le> 1 \<or> i < b then 1 else 1 + log b (i div b))"
    1.18 -
    1.19  
    1.20  subsection {* Random seeds *}
    1.21  
    1.22 @@ -29,28 +29,19 @@
    1.23  primrec "next" :: "seed \<Rightarrow> code_numeral \<times> seed" where
    1.24    "next (v, w) = (let
    1.25       k =  v div 53668;
    1.26 -     v' = minus_shift 2147483563 (40014 * (v mod 53668)) (k * 12211);
    1.27 +     v' = minus_shift 2147483563 ((v mod 53668) * 40014) (k * 12211);
    1.28       l =  w div 52774;
    1.29 -     w' = minus_shift 2147483399 (40692 * (w mod 52774)) (l * 3791);
    1.30 +     w' = minus_shift 2147483399 ((w mod 52774) * 40692) (l * 3791);
    1.31       z =  minus_shift 2147483562 v' (w' + 1) + 1
    1.32     in (z, (v', w')))"
    1.33  
    1.34 -lemma next_not_0:
    1.35 -  "fst (next s) \<noteq> 0"
    1.36 -  by (cases s) (auto simp add: minus_shift_def Let_def)
    1.37 -
    1.38 -primrec seed_invariant :: "seed \<Rightarrow> bool" where
    1.39 -  "seed_invariant (v, w) \<longleftrightarrow> 0 < v \<and> v < 9438322952 \<and> 0 < w \<and> True"
    1.40 -
    1.41  definition split_seed :: "seed \<Rightarrow> seed \<times> seed" where
    1.42    "split_seed s = (let
    1.43       (v, w) = s;
    1.44       (v', w') = snd (next s);
    1.45       v'' = inc_shift 2147483562 v;
    1.46 -     s'' = (v'', w');
    1.47 -     w'' = inc_shift 2147483398 w;
    1.48 -     s''' = (v', w'')
    1.49 -   in (s'', s'''))"
    1.50 +     w'' = inc_shift 2147483398 w
    1.51 +   in ((v'', w'), (v', w'')))"
    1.52  
    1.53  
    1.54  subsection {* Base selectors *}
    1.55 @@ -175,7 +166,7 @@
    1.56  *}
    1.57  
    1.58  hide (open) type seed
    1.59 -hide (open) const inc_shift minus_shift log "next" seed_invariant split_seed
    1.60 +hide (open) const inc_shift minus_shift log "next" split_seed
    1.61    iterate range select pick select_weight
    1.62  
    1.63  no_notation fcomp (infixl "o>" 60)