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