src/HOL/ex/Random.thy
author haftmann
Sat, 06 Sep 2008 14:02:36 +0200
changeset 28145 af3923ed4786
parent 28042 1471f2974eb1
child 28562 4e74209f113e
permissions -rw-r--r--
dropped "run" marker in monad syntax
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
22528
8501c4a62a3c cleaned up HOL/ex/Code*.thy
haftmann
parents:
diff changeset
     1
(*  ID:         $Id$
8501c4a62a3c cleaned up HOL/ex/Code*.thy
haftmann
parents:
diff changeset
     2
    Author:     Florian Haftmann, TU Muenchen
8501c4a62a3c cleaned up HOL/ex/Code*.thy
haftmann
parents:
diff changeset
     3
*)
8501c4a62a3c cleaned up HOL/ex/Code*.thy
haftmann
parents:
diff changeset
     4
26265
4b63b9e9b10d separated Random.thy from Quickcheck.thy
haftmann
parents: 26261
diff changeset
     5
header {* A HOL random engine *}
22528
8501c4a62a3c cleaned up HOL/ex/Code*.thy
haftmann
parents:
diff changeset
     6
8501c4a62a3c cleaned up HOL/ex/Code*.thy
haftmann
parents:
diff changeset
     7
theory Random
26265
4b63b9e9b10d separated Random.thy from Quickcheck.thy
haftmann
parents: 26261
diff changeset
     8
imports State_Monad Code_Index
22528
8501c4a62a3c cleaned up HOL/ex/Code*.thy
haftmann
parents:
diff changeset
     9
begin
8501c4a62a3c cleaned up HOL/ex/Code*.thy
haftmann
parents:
diff changeset
    10
26265
4b63b9e9b10d separated Random.thy from Quickcheck.thy
haftmann
parents: 26261
diff changeset
    11
subsection {* Auxiliary functions *}
4b63b9e9b10d separated Random.thy from Quickcheck.thy
haftmann
parents: 26261
diff changeset
    12
4b63b9e9b10d separated Random.thy from Quickcheck.thy
haftmann
parents: 26261
diff changeset
    13
definition
4b63b9e9b10d separated Random.thy from Quickcheck.thy
haftmann
parents: 26261
diff changeset
    14
  inc_shift :: "index \<Rightarrow> index \<Rightarrow> index"
4b63b9e9b10d separated Random.thy from Quickcheck.thy
haftmann
parents: 26261
diff changeset
    15
where
4b63b9e9b10d separated Random.thy from Quickcheck.thy
haftmann
parents: 26261
diff changeset
    16
  "inc_shift v k = (if v = k then 1 else k + 1)"
4b63b9e9b10d separated Random.thy from Quickcheck.thy
haftmann
parents: 26261
diff changeset
    17
4b63b9e9b10d separated Random.thy from Quickcheck.thy
haftmann
parents: 26261
diff changeset
    18
definition
4b63b9e9b10d separated Random.thy from Quickcheck.thy
haftmann
parents: 26261
diff changeset
    19
  minus_shift :: "index \<Rightarrow> index \<Rightarrow> index \<Rightarrow> index"
4b63b9e9b10d separated Random.thy from Quickcheck.thy
haftmann
parents: 26261
diff changeset
    20
where
4b63b9e9b10d separated Random.thy from Quickcheck.thy
haftmann
parents: 26261
diff changeset
    21
  "minus_shift r k l = (if k < l then r + k - l else k - l)"
4b63b9e9b10d separated Random.thy from Quickcheck.thy
haftmann
parents: 26261
diff changeset
    22
28042
1471f2974eb1 more function -> fun
krauss
parents: 26589
diff changeset
    23
fun
26265
4b63b9e9b10d separated Random.thy from Quickcheck.thy
haftmann
parents: 26261
diff changeset
    24
  log :: "index \<Rightarrow> index \<Rightarrow> index"
4b63b9e9b10d separated Random.thy from Quickcheck.thy
haftmann
parents: 26261
diff changeset
    25
where
4b63b9e9b10d separated Random.thy from Quickcheck.thy
haftmann
parents: 26261
diff changeset
    26
  "log b i = (if b \<le> 1 \<or> i < b then 1 else 1 + log b (i div b))"
4b63b9e9b10d separated Random.thy from Quickcheck.thy
haftmann
parents: 26261
diff changeset
    27
4b63b9e9b10d separated Random.thy from Quickcheck.thy
haftmann
parents: 26261
diff changeset
    28
subsection {* Random seeds *}
26038
55a02586776d towards quickcheck
haftmann
parents: 24994
diff changeset
    29
55a02586776d towards quickcheck
haftmann
parents: 24994
diff changeset
    30
types seed = "index \<times> index"
22528
8501c4a62a3c cleaned up HOL/ex/Code*.thy
haftmann
parents:
diff changeset
    31
26265
4b63b9e9b10d separated Random.thy from Quickcheck.thy
haftmann
parents: 26261
diff changeset
    32
primrec
26038
55a02586776d towards quickcheck
haftmann
parents: 24994
diff changeset
    33
  "next" :: "seed \<Rightarrow> index \<times> seed"
55a02586776d towards quickcheck
haftmann
parents: 24994
diff changeset
    34
where
26265
4b63b9e9b10d separated Random.thy from Quickcheck.thy
haftmann
parents: 26261
diff changeset
    35
  "next (v, w) = (let
4b63b9e9b10d separated Random.thy from Quickcheck.thy
haftmann
parents: 26261
diff changeset
    36
     k =  v div 53668;
4b63b9e9b10d separated Random.thy from Quickcheck.thy
haftmann
parents: 26261
diff changeset
    37
     v' = minus_shift 2147483563 (40014 * (v mod 53668)) (k * 12211);
4b63b9e9b10d separated Random.thy from Quickcheck.thy
haftmann
parents: 26261
diff changeset
    38
     l =  w div 52774;
4b63b9e9b10d separated Random.thy from Quickcheck.thy
haftmann
parents: 26261
diff changeset
    39
     w' = minus_shift 2147483399 (40692 * (w mod 52774)) (l * 3791);
4b63b9e9b10d separated Random.thy from Quickcheck.thy
haftmann
parents: 26261
diff changeset
    40
     z =  minus_shift 2147483562 v' (w' + 1) + 1
4b63b9e9b10d separated Random.thy from Quickcheck.thy
haftmann
parents: 26261
diff changeset
    41
   in (z, (v', w')))"
4b63b9e9b10d separated Random.thy from Quickcheck.thy
haftmann
parents: 26261
diff changeset
    42
4b63b9e9b10d separated Random.thy from Quickcheck.thy
haftmann
parents: 26261
diff changeset
    43
lemma next_not_0:
4b63b9e9b10d separated Random.thy from Quickcheck.thy
haftmann
parents: 26261
diff changeset
    44
  "fst (next s) \<noteq> 0"
4b63b9e9b10d separated Random.thy from Quickcheck.thy
haftmann
parents: 26261
diff changeset
    45
apply (cases s)
4b63b9e9b10d separated Random.thy from Quickcheck.thy
haftmann
parents: 26261
diff changeset
    46
apply (auto simp add: minus_shift_def Let_def)
4b63b9e9b10d separated Random.thy from Quickcheck.thy
haftmann
parents: 26261
diff changeset
    47
done
4b63b9e9b10d separated Random.thy from Quickcheck.thy
haftmann
parents: 26261
diff changeset
    48
4b63b9e9b10d separated Random.thy from Quickcheck.thy
haftmann
parents: 26261
diff changeset
    49
primrec
4b63b9e9b10d separated Random.thy from Quickcheck.thy
haftmann
parents: 26261
diff changeset
    50
  seed_invariant :: "seed \<Rightarrow> bool"
4b63b9e9b10d separated Random.thy from Quickcheck.thy
haftmann
parents: 26261
diff changeset
    51
where
4b63b9e9b10d separated Random.thy from Quickcheck.thy
haftmann
parents: 26261
diff changeset
    52
  "seed_invariant (v, w) \<longleftrightarrow> 0 < v \<and> v < 9438322952 \<and> 0 < w \<and> True"
4b63b9e9b10d separated Random.thy from Quickcheck.thy
haftmann
parents: 26261
diff changeset
    53
4b63b9e9b10d separated Random.thy from Quickcheck.thy
haftmann
parents: 26261
diff changeset
    54
lemma if_same:
4b63b9e9b10d separated Random.thy from Quickcheck.thy
haftmann
parents: 26261
diff changeset
    55
  "(if b then f x else f y) = f (if b then x else y)"
4b63b9e9b10d separated Random.thy from Quickcheck.thy
haftmann
parents: 26261
diff changeset
    56
  by (cases b) simp_all
4b63b9e9b10d separated Random.thy from Quickcheck.thy
haftmann
parents: 26261
diff changeset
    57
22528
8501c4a62a3c cleaned up HOL/ex/Code*.thy
haftmann
parents:
diff changeset
    58
definition
26038
55a02586776d towards quickcheck
haftmann
parents: 24994
diff changeset
    59
  split_seed :: "seed \<Rightarrow> seed \<times> seed"
55a02586776d towards quickcheck
haftmann
parents: 24994
diff changeset
    60
where
55a02586776d towards quickcheck
haftmann
parents: 24994
diff changeset
    61
  "split_seed s = (let
55a02586776d towards quickcheck
haftmann
parents: 24994
diff changeset
    62
     (v, w) = s;
55a02586776d towards quickcheck
haftmann
parents: 24994
diff changeset
    63
     (v', w') = snd (next s);
26265
4b63b9e9b10d separated Random.thy from Quickcheck.thy
haftmann
parents: 26261
diff changeset
    64
     v'' = inc_shift 2147483562 v;
26038
55a02586776d towards quickcheck
haftmann
parents: 24994
diff changeset
    65
     s'' = (v'', w');
26265
4b63b9e9b10d separated Random.thy from Quickcheck.thy
haftmann
parents: 26261
diff changeset
    66
     w'' = inc_shift 2147483398 w;
26038
55a02586776d towards quickcheck
haftmann
parents: 24994
diff changeset
    67
     s''' = (v', w'')
55a02586776d towards quickcheck
haftmann
parents: 24994
diff changeset
    68
   in (s'', s'''))"
55a02586776d towards quickcheck
haftmann
parents: 24994
diff changeset
    69
55a02586776d towards quickcheck
haftmann
parents: 24994
diff changeset
    70
26265
4b63b9e9b10d separated Random.thy from Quickcheck.thy
haftmann
parents: 26261
diff changeset
    71
subsection {* Base selectors *}
22528
8501c4a62a3c cleaned up HOL/ex/Code*.thy
haftmann
parents:
diff changeset
    72
26038
55a02586776d towards quickcheck
haftmann
parents: 24994
diff changeset
    73
function
55a02586776d towards quickcheck
haftmann
parents: 24994
diff changeset
    74
  range_aux :: "index \<Rightarrow> index \<Rightarrow> seed \<Rightarrow> index \<times> seed"
55a02586776d towards quickcheck
haftmann
parents: 24994
diff changeset
    75
where
55a02586776d towards quickcheck
haftmann
parents: 24994
diff changeset
    76
  "range_aux k l s = (if k = 0 then (l, s) else
55a02586776d towards quickcheck
haftmann
parents: 24994
diff changeset
    77
    let (v, s') = next s
55a02586776d towards quickcheck
haftmann
parents: 24994
diff changeset
    78
  in range_aux (k - 1) (v + l * 2147483561) s')"
55a02586776d towards quickcheck
haftmann
parents: 24994
diff changeset
    79
by pat_completeness auto
55a02586776d towards quickcheck
haftmann
parents: 24994
diff changeset
    80
termination
55a02586776d towards quickcheck
haftmann
parents: 24994
diff changeset
    81
  by (relation "measure (nat_of_index o fst)")
55a02586776d towards quickcheck
haftmann
parents: 24994
diff changeset
    82
    (auto simp add: index)
22528
8501c4a62a3c cleaned up HOL/ex/Code*.thy
haftmann
parents:
diff changeset
    83
8501c4a62a3c cleaned up HOL/ex/Code*.thy
haftmann
parents:
diff changeset
    84
definition
26038
55a02586776d towards quickcheck
haftmann
parents: 24994
diff changeset
    85
  range :: "index \<Rightarrow> seed \<Rightarrow> index \<times> seed"
55a02586776d towards quickcheck
haftmann
parents: 24994
diff changeset
    86
where
26265
4b63b9e9b10d separated Random.thy from Quickcheck.thy
haftmann
parents: 26261
diff changeset
    87
  "range k = (do
4b63b9e9b10d separated Random.thy from Quickcheck.thy
haftmann
parents: 26261
diff changeset
    88
     v \<leftarrow> range_aux (log 2147483561 k) 1;
4b63b9e9b10d separated Random.thy from Quickcheck.thy
haftmann
parents: 26261
diff changeset
    89
     return (v mod k)
4b63b9e9b10d separated Random.thy from Quickcheck.thy
haftmann
parents: 26261
diff changeset
    90
   done)"
4b63b9e9b10d separated Random.thy from Quickcheck.thy
haftmann
parents: 26261
diff changeset
    91
4b63b9e9b10d separated Random.thy from Quickcheck.thy
haftmann
parents: 26261
diff changeset
    92
lemma range:
4b63b9e9b10d separated Random.thy from Quickcheck.thy
haftmann
parents: 26261
diff changeset
    93
  assumes "k > 0"
4b63b9e9b10d separated Random.thy from Quickcheck.thy
haftmann
parents: 26261
diff changeset
    94
  shows "fst (range k s) < k"
4b63b9e9b10d separated Random.thy from Quickcheck.thy
haftmann
parents: 26261
diff changeset
    95
proof -
4b63b9e9b10d separated Random.thy from Quickcheck.thy
haftmann
parents: 26261
diff changeset
    96
  obtain v w where range_aux:
4b63b9e9b10d separated Random.thy from Quickcheck.thy
haftmann
parents: 26261
diff changeset
    97
    "range_aux (log 2147483561 k) 1 s = (v, w)"
4b63b9e9b10d separated Random.thy from Quickcheck.thy
haftmann
parents: 26261
diff changeset
    98
    by (cases "range_aux (log 2147483561 k) 1 s")
4b63b9e9b10d separated Random.thy from Quickcheck.thy
haftmann
parents: 26261
diff changeset
    99
  with assms show ?thesis
28145
af3923ed4786 dropped "run" marker in monad syntax
haftmann
parents: 28042
diff changeset
   100
    by (simp add: monad_collapse range_def del: range_aux.simps log.simps)
26265
4b63b9e9b10d separated Random.thy from Quickcheck.thy
haftmann
parents: 26261
diff changeset
   101
qed
26038
55a02586776d towards quickcheck
haftmann
parents: 24994
diff changeset
   102
22528
8501c4a62a3c cleaned up HOL/ex/Code*.thy
haftmann
parents:
diff changeset
   103
definition
26038
55a02586776d towards quickcheck
haftmann
parents: 24994
diff changeset
   104
  select :: "'a list \<Rightarrow> seed \<Rightarrow> 'a \<times> seed"
55a02586776d towards quickcheck
haftmann
parents: 24994
diff changeset
   105
where
26265
4b63b9e9b10d separated Random.thy from Quickcheck.thy
haftmann
parents: 26261
diff changeset
   106
  "select xs = (do
4b63b9e9b10d separated Random.thy from Quickcheck.thy
haftmann
parents: 26261
diff changeset
   107
     k \<leftarrow> range (index_of_nat (length xs));
4b63b9e9b10d separated Random.thy from Quickcheck.thy
haftmann
parents: 26261
diff changeset
   108
     return (nth xs (nat_of_index k))
4b63b9e9b10d separated Random.thy from Quickcheck.thy
haftmann
parents: 26261
diff changeset
   109
   done)"
4b63b9e9b10d separated Random.thy from Quickcheck.thy
haftmann
parents: 26261
diff changeset
   110
4b63b9e9b10d separated Random.thy from Quickcheck.thy
haftmann
parents: 26261
diff changeset
   111
lemma select:
4b63b9e9b10d separated Random.thy from Quickcheck.thy
haftmann
parents: 26261
diff changeset
   112
  assumes "xs \<noteq> []"
4b63b9e9b10d separated Random.thy from Quickcheck.thy
haftmann
parents: 26261
diff changeset
   113
  shows "fst (select xs s) \<in> set xs"
4b63b9e9b10d separated Random.thy from Quickcheck.thy
haftmann
parents: 26261
diff changeset
   114
proof -
4b63b9e9b10d separated Random.thy from Quickcheck.thy
haftmann
parents: 26261
diff changeset
   115
  from assms have "index_of_nat (length xs) > 0" by simp
4b63b9e9b10d separated Random.thy from Quickcheck.thy
haftmann
parents: 26261
diff changeset
   116
  with range have
4b63b9e9b10d separated Random.thy from Quickcheck.thy
haftmann
parents: 26261
diff changeset
   117
    "fst (range (index_of_nat (length xs)) s) < index_of_nat (length xs)" by best
4b63b9e9b10d separated Random.thy from Quickcheck.thy
haftmann
parents: 26261
diff changeset
   118
  then have
4b63b9e9b10d separated Random.thy from Quickcheck.thy
haftmann
parents: 26261
diff changeset
   119
    "nat_of_index (fst (range (index_of_nat (length xs)) s)) < length xs" by simp
4b63b9e9b10d separated Random.thy from Quickcheck.thy
haftmann
parents: 26261
diff changeset
   120
  then show ?thesis
28145
af3923ed4786 dropped "run" marker in monad syntax
haftmann
parents: 28042
diff changeset
   121
    by (auto simp add: monad_collapse select_def)
26265
4b63b9e9b10d separated Random.thy from Quickcheck.thy
haftmann
parents: 26261
diff changeset
   122
qed
22528
8501c4a62a3c cleaned up HOL/ex/Code*.thy
haftmann
parents:
diff changeset
   123
26038
55a02586776d towards quickcheck
haftmann
parents: 24994
diff changeset
   124
definition
26265
4b63b9e9b10d separated Random.thy from Quickcheck.thy
haftmann
parents: 26261
diff changeset
   125
  select_default :: "index \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> seed \<Rightarrow> 'a \<times> seed"
26038
55a02586776d towards quickcheck
haftmann
parents: 24994
diff changeset
   126
where
26265
4b63b9e9b10d separated Random.thy from Quickcheck.thy
haftmann
parents: 26261
diff changeset
   127
  [code func del]: "select_default k x y = (do
4b63b9e9b10d separated Random.thy from Quickcheck.thy
haftmann
parents: 26261
diff changeset
   128
     l \<leftarrow> range k;
4b63b9e9b10d separated Random.thy from Quickcheck.thy
haftmann
parents: 26261
diff changeset
   129
     return (if l + 1 < k then x else y)
4b63b9e9b10d separated Random.thy from Quickcheck.thy
haftmann
parents: 26261
diff changeset
   130
   done)"
4b63b9e9b10d separated Random.thy from Quickcheck.thy
haftmann
parents: 26261
diff changeset
   131
4b63b9e9b10d separated Random.thy from Quickcheck.thy
haftmann
parents: 26261
diff changeset
   132
lemma select_default_zero:
4b63b9e9b10d separated Random.thy from Quickcheck.thy
haftmann
parents: 26261
diff changeset
   133
  "fst (select_default 0 x y s) = y"
28145
af3923ed4786 dropped "run" marker in monad syntax
haftmann
parents: 28042
diff changeset
   134
  by (simp add: monad_collapse select_default_def)
26038
55a02586776d towards quickcheck
haftmann
parents: 24994
diff changeset
   135
26265
4b63b9e9b10d separated Random.thy from Quickcheck.thy
haftmann
parents: 26261
diff changeset
   136
lemma select_default_code [code]:
4b63b9e9b10d separated Random.thy from Quickcheck.thy
haftmann
parents: 26261
diff changeset
   137
  "select_default k x y = (if k = 0 then do
4b63b9e9b10d separated Random.thy from Quickcheck.thy
haftmann
parents: 26261
diff changeset
   138
     _ \<leftarrow> range 1;
4b63b9e9b10d separated Random.thy from Quickcheck.thy
haftmann
parents: 26261
diff changeset
   139
     return y
4b63b9e9b10d separated Random.thy from Quickcheck.thy
haftmann
parents: 26261
diff changeset
   140
   done else do
4b63b9e9b10d separated Random.thy from Quickcheck.thy
haftmann
parents: 26261
diff changeset
   141
     l \<leftarrow> range k;
4b63b9e9b10d separated Random.thy from Quickcheck.thy
haftmann
parents: 26261
diff changeset
   142
     return (if l + 1 < k then x else y)
4b63b9e9b10d separated Random.thy from Quickcheck.thy
haftmann
parents: 26261
diff changeset
   143
   done)"
4b63b9e9b10d separated Random.thy from Quickcheck.thy
haftmann
parents: 26261
diff changeset
   144
proof (cases "k = 0")
4b63b9e9b10d separated Random.thy from Quickcheck.thy
haftmann
parents: 26261
diff changeset
   145
  case False then show ?thesis by (simp add: select_default_def)
22528
8501c4a62a3c cleaned up HOL/ex/Code*.thy
haftmann
parents:
diff changeset
   146
next
26265
4b63b9e9b10d separated Random.thy from Quickcheck.thy
haftmann
parents: 26261
diff changeset
   147
  case True then show ?thesis
28145
af3923ed4786 dropped "run" marker in monad syntax
haftmann
parents: 28042
diff changeset
   148
    by (simp add: monad_collapse select_default_def range_def)
26265
4b63b9e9b10d separated Random.thy from Quickcheck.thy
haftmann
parents: 26261
diff changeset
   149
qed
22528
8501c4a62a3c cleaned up HOL/ex/Code*.thy
haftmann
parents:
diff changeset
   150
26265
4b63b9e9b10d separated Random.thy from Quickcheck.thy
haftmann
parents: 26261
diff changeset
   151
4b63b9e9b10d separated Random.thy from Quickcheck.thy
haftmann
parents: 26261
diff changeset
   152
subsection {* @{text ML} interface *}
22528
8501c4a62a3c cleaned up HOL/ex/Code*.thy
haftmann
parents:
diff changeset
   153
8501c4a62a3c cleaned up HOL/ex/Code*.thy
haftmann
parents:
diff changeset
   154
ML {*
26265
4b63b9e9b10d separated Random.thy from Quickcheck.thy
haftmann
parents: 26261
diff changeset
   155
structure Random_Engine =
22528
8501c4a62a3c cleaned up HOL/ex/Code*.thy
haftmann
parents:
diff changeset
   156
struct
8501c4a62a3c cleaned up HOL/ex/Code*.thy
haftmann
parents:
diff changeset
   157
26038
55a02586776d towards quickcheck
haftmann
parents: 24994
diff changeset
   158
type seed = int * int;
22528
8501c4a62a3c cleaned up HOL/ex/Code*.thy
haftmann
parents:
diff changeset
   159
8501c4a62a3c cleaned up HOL/ex/Code*.thy
haftmann
parents:
diff changeset
   160
local
26038
55a02586776d towards quickcheck
haftmann
parents: 24994
diff changeset
   161
26265
4b63b9e9b10d separated Random.thy from Quickcheck.thy
haftmann
parents: 26261
diff changeset
   162
val seed = ref 
4b63b9e9b10d separated Random.thy from Quickcheck.thy
haftmann
parents: 26261
diff changeset
   163
  (let
4b63b9e9b10d separated Random.thy from Quickcheck.thy
haftmann
parents: 26261
diff changeset
   164
    val now = Time.toMilliseconds (Time.now ());
26038
55a02586776d towards quickcheck
haftmann
parents: 24994
diff changeset
   165
    val (q, s1) = IntInf.divMod (now, 2147483562);
55a02586776d towards quickcheck
haftmann
parents: 24994
diff changeset
   166
    val s2 = q mod 2147483398;
26265
4b63b9e9b10d separated Random.thy from Quickcheck.thy
haftmann
parents: 26261
diff changeset
   167
  in (s1 + 1, s2 + 1) end);
4b63b9e9b10d separated Random.thy from Quickcheck.thy
haftmann
parents: 26261
diff changeset
   168
22528
8501c4a62a3c cleaned up HOL/ex/Code*.thy
haftmann
parents:
diff changeset
   169
in
26038
55a02586776d towards quickcheck
haftmann
parents: 24994
diff changeset
   170
55a02586776d towards quickcheck
haftmann
parents: 24994
diff changeset
   171
fun run f =
55a02586776d towards quickcheck
haftmann
parents: 24994
diff changeset
   172
  let
26265
4b63b9e9b10d separated Random.thy from Quickcheck.thy
haftmann
parents: 26261
diff changeset
   173
    val (x, seed') = f (! seed);
26038
55a02586776d towards quickcheck
haftmann
parents: 24994
diff changeset
   174
    val _ = seed := seed'
55a02586776d towards quickcheck
haftmann
parents: 24994
diff changeset
   175
  in x end;
55a02586776d towards quickcheck
haftmann
parents: 24994
diff changeset
   176
22528
8501c4a62a3c cleaned up HOL/ex/Code*.thy
haftmann
parents:
diff changeset
   177
end;
8501c4a62a3c cleaned up HOL/ex/Code*.thy
haftmann
parents:
diff changeset
   178
8501c4a62a3c cleaned up HOL/ex/Code*.thy
haftmann
parents:
diff changeset
   179
end;
8501c4a62a3c cleaned up HOL/ex/Code*.thy
haftmann
parents:
diff changeset
   180
*}
8501c4a62a3c cleaned up HOL/ex/Code*.thy
haftmann
parents:
diff changeset
   181
26038
55a02586776d towards quickcheck
haftmann
parents: 24994
diff changeset
   182
end
28145
af3923ed4786 dropped "run" marker in monad syntax
haftmann
parents: 28042
diff changeset
   183