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