src/HOL/ex/Random.thy
author haftmann
Mon, 04 Feb 2008 10:52:40 +0100
changeset 26038 55a02586776d
parent 24994 c385c4eabb3b
child 26042 e7a421d1f5c1
permissions -rw-r--r--
towards quickcheck
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
26038
55a02586776d towards quickcheck
haftmann
parents: 24994
diff changeset
     5
header {* A simple term generator *}
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
26038
55a02586776d towards quickcheck
haftmann
parents: 24994
diff changeset
     8
imports State_Monad Code_Index List Eval
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
26038
55a02586776d towards quickcheck
haftmann
parents: 24994
diff changeset
    11
subsection {* The random engine *}
55a02586776d towards quickcheck
haftmann
parents: 24994
diff changeset
    12
55a02586776d towards quickcheck
haftmann
parents: 24994
diff changeset
    13
types seed = "index \<times> index"
22528
8501c4a62a3c cleaned up HOL/ex/Code*.thy
haftmann
parents:
diff changeset
    14
26038
55a02586776d towards quickcheck
haftmann
parents: 24994
diff changeset
    15
definition
55a02586776d towards quickcheck
haftmann
parents: 24994
diff changeset
    16
  "next" :: "seed \<Rightarrow> index \<times> seed"
55a02586776d towards quickcheck
haftmann
parents: 24994
diff changeset
    17
where
55a02586776d towards quickcheck
haftmann
parents: 24994
diff changeset
    18
  "next s = (let
55a02586776d towards quickcheck
haftmann
parents: 24994
diff changeset
    19
     (v, w) = s;
55a02586776d towards quickcheck
haftmann
parents: 24994
diff changeset
    20
     k = v div 53668;
55a02586776d towards quickcheck
haftmann
parents: 24994
diff changeset
    21
     v' = 40014 * (v - k * 53668) - k * 12211;
55a02586776d towards quickcheck
haftmann
parents: 24994
diff changeset
    22
     v'' = (if v' < 0 then v' + 2147483563 else v');
55a02586776d towards quickcheck
haftmann
parents: 24994
diff changeset
    23
     l = w div 52774;
55a02586776d towards quickcheck
haftmann
parents: 24994
diff changeset
    24
     w' = 40692 * (w - l * 52774) - l * 3791;
55a02586776d towards quickcheck
haftmann
parents: 24994
diff changeset
    25
     w'' = (if w' < 0 then w' + 2147483399 else w');
55a02586776d towards quickcheck
haftmann
parents: 24994
diff changeset
    26
     z = v'' - w'';
55a02586776d towards quickcheck
haftmann
parents: 24994
diff changeset
    27
     z' = (if z < 1 then z + 2147483562 else z)
55a02586776d towards quickcheck
haftmann
parents: 24994
diff changeset
    28
   in (z',  (v'', w'')))"
22528
8501c4a62a3c cleaned up HOL/ex/Code*.thy
haftmann
parents:
diff changeset
    29
8501c4a62a3c cleaned up HOL/ex/Code*.thy
haftmann
parents:
diff changeset
    30
definition
26038
55a02586776d towards quickcheck
haftmann
parents: 24994
diff changeset
    31
  split_seed :: "seed \<Rightarrow> seed \<times> seed"
55a02586776d towards quickcheck
haftmann
parents: 24994
diff changeset
    32
where
55a02586776d towards quickcheck
haftmann
parents: 24994
diff changeset
    33
  "split_seed s = (let
55a02586776d towards quickcheck
haftmann
parents: 24994
diff changeset
    34
     (v, w) = s;
55a02586776d towards quickcheck
haftmann
parents: 24994
diff changeset
    35
     (v', w') = snd (next s);
55a02586776d towards quickcheck
haftmann
parents: 24994
diff changeset
    36
     v'' = (if v = 2147483562 then 1 else v + 1);
55a02586776d towards quickcheck
haftmann
parents: 24994
diff changeset
    37
     s'' = (v'', w');
55a02586776d towards quickcheck
haftmann
parents: 24994
diff changeset
    38
     w'' = (if w = 2147483398 then 1 else w + 1);
55a02586776d towards quickcheck
haftmann
parents: 24994
diff changeset
    39
     s''' = (v', w'')
55a02586776d towards quickcheck
haftmann
parents: 24994
diff changeset
    40
   in (s'', s'''))"
55a02586776d towards quickcheck
haftmann
parents: 24994
diff changeset
    41
55a02586776d towards quickcheck
haftmann
parents: 24994
diff changeset
    42
text {* Base selectors *}
55a02586776d towards quickcheck
haftmann
parents: 24994
diff changeset
    43
55a02586776d towards quickcheck
haftmann
parents: 24994
diff changeset
    44
primrec
55a02586776d towards quickcheck
haftmann
parents: 24994
diff changeset
    45
  pick :: "(nat \<times> 'a) list \<Rightarrow> nat \<Rightarrow> 'a"
55a02586776d towards quickcheck
haftmann
parents: 24994
diff changeset
    46
where
55a02586776d towards quickcheck
haftmann
parents: 24994
diff changeset
    47
  "pick (x#xs) n = (if n < fst x then snd x else pick xs (n - fst x))"
22528
8501c4a62a3c cleaned up HOL/ex/Code*.thy
haftmann
parents:
diff changeset
    48
26038
55a02586776d towards quickcheck
haftmann
parents: 24994
diff changeset
    49
function
55a02586776d towards quickcheck
haftmann
parents: 24994
diff changeset
    50
  iLogBase :: "index \<Rightarrow> index \<Rightarrow> index"
55a02586776d towards quickcheck
haftmann
parents: 24994
diff changeset
    51
where
55a02586776d towards quickcheck
haftmann
parents: 24994
diff changeset
    52
  "iLogBase b i = (if b \<le> 1 \<or> i < b then 1 else 1 + iLogBase b (i div b))"
55a02586776d towards quickcheck
haftmann
parents: 24994
diff changeset
    53
by pat_completeness auto
55a02586776d towards quickcheck
haftmann
parents: 24994
diff changeset
    54
termination
55a02586776d towards quickcheck
haftmann
parents: 24994
diff changeset
    55
  by (relation "measure (nat_of_index o snd)")
55a02586776d towards quickcheck
haftmann
parents: 24994
diff changeset
    56
    (auto simp add: index)
22528
8501c4a62a3c cleaned up HOL/ex/Code*.thy
haftmann
parents:
diff changeset
    57
26038
55a02586776d towards quickcheck
haftmann
parents: 24994
diff changeset
    58
function
55a02586776d towards quickcheck
haftmann
parents: 24994
diff changeset
    59
  range_aux :: "index \<Rightarrow> index \<Rightarrow> seed \<Rightarrow> index \<times> seed"
55a02586776d towards quickcheck
haftmann
parents: 24994
diff changeset
    60
where
55a02586776d towards quickcheck
haftmann
parents: 24994
diff changeset
    61
  "range_aux k l s = (if k = 0 then (l, s) else
55a02586776d towards quickcheck
haftmann
parents: 24994
diff changeset
    62
    let (v, s') = next s
55a02586776d towards quickcheck
haftmann
parents: 24994
diff changeset
    63
  in range_aux (k - 1) (v + l * 2147483561) s')"
55a02586776d towards quickcheck
haftmann
parents: 24994
diff changeset
    64
by pat_completeness auto
55a02586776d towards quickcheck
haftmann
parents: 24994
diff changeset
    65
termination
55a02586776d towards quickcheck
haftmann
parents: 24994
diff changeset
    66
  by (relation "measure (nat_of_index o fst)")
55a02586776d towards quickcheck
haftmann
parents: 24994
diff changeset
    67
    (auto simp add: index)
22528
8501c4a62a3c cleaned up HOL/ex/Code*.thy
haftmann
parents:
diff changeset
    68
8501c4a62a3c cleaned up HOL/ex/Code*.thy
haftmann
parents:
diff changeset
    69
definition
26038
55a02586776d towards quickcheck
haftmann
parents: 24994
diff changeset
    70
  range :: "index \<Rightarrow> seed \<Rightarrow> index \<times> seed"
55a02586776d towards quickcheck
haftmann
parents: 24994
diff changeset
    71
where
55a02586776d towards quickcheck
haftmann
parents: 24994
diff changeset
    72
  "range k s = (let
55a02586776d towards quickcheck
haftmann
parents: 24994
diff changeset
    73
    b = 2147483561;
55a02586776d towards quickcheck
haftmann
parents: 24994
diff changeset
    74
    n = iLogBase b k;
55a02586776d towards quickcheck
haftmann
parents: 24994
diff changeset
    75
    (v, s') = range_aux n 1 s
55a02586776d towards quickcheck
haftmann
parents: 24994
diff changeset
    76
  in (v mod k, s'))"
55a02586776d towards quickcheck
haftmann
parents: 24994
diff changeset
    77
22528
8501c4a62a3c cleaned up HOL/ex/Code*.thy
haftmann
parents:
diff changeset
    78
definition
26038
55a02586776d towards quickcheck
haftmann
parents: 24994
diff changeset
    79
  select :: "'a list \<Rightarrow> seed \<Rightarrow> 'a \<times> seed"
55a02586776d towards quickcheck
haftmann
parents: 24994
diff changeset
    80
where
55a02586776d towards quickcheck
haftmann
parents: 24994
diff changeset
    81
  [simp]: "select xs s = (let
55a02586776d towards quickcheck
haftmann
parents: 24994
diff changeset
    82
    (k, s') = range (index_of_nat (length xs)) s
55a02586776d towards quickcheck
haftmann
parents: 24994
diff changeset
    83
  in (nth xs (nat_of_index k), s'))"
22528
8501c4a62a3c cleaned up HOL/ex/Code*.thy
haftmann
parents:
diff changeset
    84
26038
55a02586776d towards quickcheck
haftmann
parents: 24994
diff changeset
    85
definition
55a02586776d towards quickcheck
haftmann
parents: 24994
diff changeset
    86
  select_weight :: "(nat \<times> 'a) list \<Rightarrow> seed \<Rightarrow> 'a \<times> seed"
55a02586776d towards quickcheck
haftmann
parents: 24994
diff changeset
    87
where
55a02586776d towards quickcheck
haftmann
parents: 24994
diff changeset
    88
  [simp]: "select_weight xs s = (let
55a02586776d towards quickcheck
haftmann
parents: 24994
diff changeset
    89
    (k, s') = range (foldr (op + \<circ> index_of_nat \<circ> fst) xs 0) s
55a02586776d towards quickcheck
haftmann
parents: 24994
diff changeset
    90
  in (pick xs (nat_of_index k), s'))"
55a02586776d towards quickcheck
haftmann
parents: 24994
diff changeset
    91
55a02586776d towards quickcheck
haftmann
parents: 24994
diff changeset
    92
(*lemma
22528
8501c4a62a3c cleaned up HOL/ex/Code*.thy
haftmann
parents:
diff changeset
    93
  "select (x#xs) s = select_weight (map (Pair 1) (x#xs)) s"
8501c4a62a3c cleaned up HOL/ex/Code*.thy
haftmann
parents:
diff changeset
    94
proof (induct xs)
26038
55a02586776d towards quickcheck
haftmann
parents: 24994
diff changeset
    95
  case Nil show ?case apply (auto simp add: Let_def split_def) 
22528
8501c4a62a3c cleaned up HOL/ex/Code*.thy
haftmann
parents:
diff changeset
    96
next
8501c4a62a3c cleaned up HOL/ex/Code*.thy
haftmann
parents:
diff changeset
    97
  have map_fst_Pair: "!!xs y. map fst (map (Pair y) xs) = replicate (length xs) y"
8501c4a62a3c cleaned up HOL/ex/Code*.thy
haftmann
parents:
diff changeset
    98
  proof -
8501c4a62a3c cleaned up HOL/ex/Code*.thy
haftmann
parents:
diff changeset
    99
    fix xs
8501c4a62a3c cleaned up HOL/ex/Code*.thy
haftmann
parents:
diff changeset
   100
    fix y
8501c4a62a3c cleaned up HOL/ex/Code*.thy
haftmann
parents:
diff changeset
   101
    show "map fst (map (Pair y) xs) = replicate (length xs) y"
8501c4a62a3c cleaned up HOL/ex/Code*.thy
haftmann
parents:
diff changeset
   102
      by (induct xs) simp_all
8501c4a62a3c cleaned up HOL/ex/Code*.thy
haftmann
parents:
diff changeset
   103
  qed
8501c4a62a3c cleaned up HOL/ex/Code*.thy
haftmann
parents:
diff changeset
   104
  have pick_nth: "!!xs n. n < length xs \<Longrightarrow> pick (map (Pair 1) xs) n = nth xs n"
8501c4a62a3c cleaned up HOL/ex/Code*.thy
haftmann
parents:
diff changeset
   105
  proof -
8501c4a62a3c cleaned up HOL/ex/Code*.thy
haftmann
parents:
diff changeset
   106
    fix xs
8501c4a62a3c cleaned up HOL/ex/Code*.thy
haftmann
parents:
diff changeset
   107
    fix n
8501c4a62a3c cleaned up HOL/ex/Code*.thy
haftmann
parents:
diff changeset
   108
    assume "n < length xs"
8501c4a62a3c cleaned up HOL/ex/Code*.thy
haftmann
parents:
diff changeset
   109
    then show "pick (map (Pair 1) xs) n = nth xs n"
8501c4a62a3c cleaned up HOL/ex/Code*.thy
haftmann
parents:
diff changeset
   110
    proof (induct xs arbitrary: n)
8501c4a62a3c cleaned up HOL/ex/Code*.thy
haftmann
parents:
diff changeset
   111
      case Nil then show ?case by simp
8501c4a62a3c cleaned up HOL/ex/Code*.thy
haftmann
parents:
diff changeset
   112
    next
8501c4a62a3c cleaned up HOL/ex/Code*.thy
haftmann
parents:
diff changeset
   113
      case (Cons x xs) show ?case
8501c4a62a3c cleaned up HOL/ex/Code*.thy
haftmann
parents:
diff changeset
   114
      proof (cases n)
8501c4a62a3c cleaned up HOL/ex/Code*.thy
haftmann
parents:
diff changeset
   115
        case 0 then show ?thesis by simp
8501c4a62a3c cleaned up HOL/ex/Code*.thy
haftmann
parents:
diff changeset
   116
      next
8501c4a62a3c cleaned up HOL/ex/Code*.thy
haftmann
parents:
diff changeset
   117
        case (Suc _)
8501c4a62a3c cleaned up HOL/ex/Code*.thy
haftmann
parents:
diff changeset
   118
    from Cons have "n < length (x # xs)" by auto
8501c4a62a3c cleaned up HOL/ex/Code*.thy
haftmann
parents:
diff changeset
   119
        then have "n < Suc (length xs)" by simp
8501c4a62a3c cleaned up HOL/ex/Code*.thy
haftmann
parents:
diff changeset
   120
        with Suc have "n - 1 < Suc (length xs) - 1" by auto
8501c4a62a3c cleaned up HOL/ex/Code*.thy
haftmann
parents:
diff changeset
   121
        with Cons have "pick (map (Pair (1\<Colon>nat)) xs) (n - 1) = xs ! (n - 1)" by auto
8501c4a62a3c cleaned up HOL/ex/Code*.thy
haftmann
parents:
diff changeset
   122
        with Suc show ?thesis by auto
8501c4a62a3c cleaned up HOL/ex/Code*.thy
haftmann
parents:
diff changeset
   123
      qed
8501c4a62a3c cleaned up HOL/ex/Code*.thy
haftmann
parents:
diff changeset
   124
    qed
8501c4a62a3c cleaned up HOL/ex/Code*.thy
haftmann
parents:
diff changeset
   125
  qed
8501c4a62a3c cleaned up HOL/ex/Code*.thy
haftmann
parents:
diff changeset
   126
  have sum_length: "!!xs. foldl (op +) 0 (map fst (map (Pair 1) xs)) = length xs"
8501c4a62a3c cleaned up HOL/ex/Code*.thy
haftmann
parents:
diff changeset
   127
  proof -
8501c4a62a3c cleaned up HOL/ex/Code*.thy
haftmann
parents:
diff changeset
   128
    have replicate_append:
8501c4a62a3c cleaned up HOL/ex/Code*.thy
haftmann
parents:
diff changeset
   129
      "!!x xs y. replicate (length (x # xs)) y = replicate (length xs) y @ [y]"
8501c4a62a3c cleaned up HOL/ex/Code*.thy
haftmann
parents:
diff changeset
   130
      by (simp add: replicate_app_Cons_same)
8501c4a62a3c cleaned up HOL/ex/Code*.thy
haftmann
parents:
diff changeset
   131
    fix xs
8501c4a62a3c cleaned up HOL/ex/Code*.thy
haftmann
parents:
diff changeset
   132
    show "foldl (op +) 0 (map fst (map (Pair 1) xs)) = length xs"
8501c4a62a3c cleaned up HOL/ex/Code*.thy
haftmann
parents:
diff changeset
   133
    unfolding map_fst_Pair proof (induct xs)
8501c4a62a3c cleaned up HOL/ex/Code*.thy
haftmann
parents:
diff changeset
   134
      case Nil show ?case by simp
8501c4a62a3c cleaned up HOL/ex/Code*.thy
haftmann
parents:
diff changeset
   135
    next
8501c4a62a3c cleaned up HOL/ex/Code*.thy
haftmann
parents:
diff changeset
   136
      case (Cons x xs) then show ?case unfolding replicate_append by simp
8501c4a62a3c cleaned up HOL/ex/Code*.thy
haftmann
parents:
diff changeset
   137
    qed
8501c4a62a3c cleaned up HOL/ex/Code*.thy
haftmann
parents:
diff changeset
   138
  qed
8501c4a62a3c cleaned up HOL/ex/Code*.thy
haftmann
parents:
diff changeset
   139
  have pick_nth_random:
8501c4a62a3c cleaned up HOL/ex/Code*.thy
haftmann
parents:
diff changeset
   140
    "!!x xs s. pick (map (Pair 1) (x#xs)) (fst (random (length (x#xs)) s)) = nth (x#xs) (fst (random (length (x#xs)) s))"
8501c4a62a3c cleaned up HOL/ex/Code*.thy
haftmann
parents:
diff changeset
   141
  proof -
8501c4a62a3c cleaned up HOL/ex/Code*.thy
haftmann
parents:
diff changeset
   142
    fix s
8501c4a62a3c cleaned up HOL/ex/Code*.thy
haftmann
parents:
diff changeset
   143
    fix x
8501c4a62a3c cleaned up HOL/ex/Code*.thy
haftmann
parents:
diff changeset
   144
    fix xs
8501c4a62a3c cleaned up HOL/ex/Code*.thy
haftmann
parents:
diff changeset
   145
    have bound: "fst (random (length (x#xs)) s) < length (x#xs)" by (rule random_bound) simp
8501c4a62a3c cleaned up HOL/ex/Code*.thy
haftmann
parents:
diff changeset
   146
    from pick_nth [OF bound] show
8501c4a62a3c cleaned up HOL/ex/Code*.thy
haftmann
parents:
diff changeset
   147
      "pick (map (Pair 1) (x#xs)) (fst (random (length (x#xs)) s)) = nth (x#xs) (fst (random (length (x#xs)) s))" .
8501c4a62a3c cleaned up HOL/ex/Code*.thy
haftmann
parents:
diff changeset
   148
  qed
8501c4a62a3c cleaned up HOL/ex/Code*.thy
haftmann
parents:
diff changeset
   149
  have pick_nth_random_do:
8501c4a62a3c cleaned up HOL/ex/Code*.thy
haftmann
parents:
diff changeset
   150
    "!!x xs s. (do n \<leftarrow> random (length (x#xs)); return (pick (map (Pair 1) (x#xs)) n) done) s =
8501c4a62a3c cleaned up HOL/ex/Code*.thy
haftmann
parents:
diff changeset
   151
      (do n \<leftarrow> random (length (x#xs)); return (nth (x#xs) n) done) s"
8501c4a62a3c cleaned up HOL/ex/Code*.thy
haftmann
parents:
diff changeset
   152
  unfolding monad_collapse split_def unfolding pick_nth_random ..
8501c4a62a3c cleaned up HOL/ex/Code*.thy
haftmann
parents:
diff changeset
   153
  case (Cons x xs) then show ?case
8501c4a62a3c cleaned up HOL/ex/Code*.thy
haftmann
parents:
diff changeset
   154
    unfolding select_weight_def sum_length pick_nth_random_do
8501c4a62a3c cleaned up HOL/ex/Code*.thy
haftmann
parents:
diff changeset
   155
    by simp
26038
55a02586776d towards quickcheck
haftmann
parents: 24994
diff changeset
   156
qed*)
22528
8501c4a62a3c cleaned up HOL/ex/Code*.thy
haftmann
parents:
diff changeset
   157
26038
55a02586776d towards quickcheck
haftmann
parents: 24994
diff changeset
   158
text {* The @{text ML} interface *}
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
ML {*
26038
55a02586776d towards quickcheck
haftmann
parents: 24994
diff changeset
   161
structure Quickcheck =
22528
8501c4a62a3c cleaned up HOL/ex/Code*.thy
haftmann
parents:
diff changeset
   162
struct
8501c4a62a3c cleaned up HOL/ex/Code*.thy
haftmann
parents:
diff changeset
   163
26038
55a02586776d towards quickcheck
haftmann
parents: 24994
diff changeset
   164
type seed = int * int;
22528
8501c4a62a3c cleaned up HOL/ex/Code*.thy
haftmann
parents:
diff changeset
   165
8501c4a62a3c cleaned up HOL/ex/Code*.thy
haftmann
parents:
diff changeset
   166
local
26038
55a02586776d towards quickcheck
haftmann
parents: 24994
diff changeset
   167
55a02586776d towards quickcheck
haftmann
parents: 24994
diff changeset
   168
val seed = ref (0, 0);
55a02586776d towards quickcheck
haftmann
parents: 24994
diff changeset
   169
55a02586776d towards quickcheck
haftmann
parents: 24994
diff changeset
   170
fun init () =
55a02586776d towards quickcheck
haftmann
parents: 24994
diff changeset
   171
  let
55a02586776d towards quickcheck
haftmann
parents: 24994
diff changeset
   172
    val now = Time.toNanoseconds (Time.now ());
55a02586776d towards quickcheck
haftmann
parents: 24994
diff changeset
   173
    val (q, s1) = IntInf.divMod (now, 2147483562);
55a02586776d towards quickcheck
haftmann
parents: 24994
diff changeset
   174
    val s2 = q mod 2147483398;
55a02586776d towards quickcheck
haftmann
parents: 24994
diff changeset
   175
  in seed := (s1 + 1, s2 + 1) end;
55a02586776d towards quickcheck
haftmann
parents: 24994
diff changeset
   176
  
22528
8501c4a62a3c cleaned up HOL/ex/Code*.thy
haftmann
parents:
diff changeset
   177
in
26038
55a02586776d towards quickcheck
haftmann
parents: 24994
diff changeset
   178
55a02586776d towards quickcheck
haftmann
parents: 24994
diff changeset
   179
val seed = seed; (* FIXME *)
55a02586776d towards quickcheck
haftmann
parents: 24994
diff changeset
   180
55a02586776d towards quickcheck
haftmann
parents: 24994
diff changeset
   181
fun run f =
55a02586776d towards quickcheck
haftmann
parents: 24994
diff changeset
   182
  let
55a02586776d towards quickcheck
haftmann
parents: 24994
diff changeset
   183
    val (x, seed') = f (!seed);
55a02586776d towards quickcheck
haftmann
parents: 24994
diff changeset
   184
    val _ = seed := seed'
55a02586776d towards quickcheck
haftmann
parents: 24994
diff changeset
   185
    val _ = if fst (! seed) = 0 orelse snd (! seed) = 0 then
55a02586776d towards quickcheck
haftmann
parents: 24994
diff changeset
   186
      (warning "broken random seed"; init ())
55a02586776d towards quickcheck
haftmann
parents: 24994
diff changeset
   187
      else ()
55a02586776d towards quickcheck
haftmann
parents: 24994
diff changeset
   188
  in x end;
55a02586776d towards quickcheck
haftmann
parents: 24994
diff changeset
   189
22528
8501c4a62a3c cleaned up HOL/ex/Code*.thy
haftmann
parents:
diff changeset
   190
end;
8501c4a62a3c cleaned up HOL/ex/Code*.thy
haftmann
parents:
diff changeset
   191
8501c4a62a3c cleaned up HOL/ex/Code*.thy
haftmann
parents:
diff changeset
   192
end;
8501c4a62a3c cleaned up HOL/ex/Code*.thy
haftmann
parents:
diff changeset
   193
*}
8501c4a62a3c cleaned up HOL/ex/Code*.thy
haftmann
parents:
diff changeset
   194
26038
55a02586776d towards quickcheck
haftmann
parents: 24994
diff changeset
   195
55a02586776d towards quickcheck
haftmann
parents: 24994
diff changeset
   196
subsection {* The @{text random} class *}
55a02586776d towards quickcheck
haftmann
parents: 24994
diff changeset
   197
55a02586776d towards quickcheck
haftmann
parents: 24994
diff changeset
   198
class random = type +
55a02586776d towards quickcheck
haftmann
parents: 24994
diff changeset
   199
  fixes random :: "index \<Rightarrow> seed \<Rightarrow> 'a \<times> seed"
55a02586776d towards quickcheck
haftmann
parents: 24994
diff changeset
   200
55a02586776d towards quickcheck
haftmann
parents: 24994
diff changeset
   201
-- {* FIXME dummy implementations *}
55a02586776d towards quickcheck
haftmann
parents: 24994
diff changeset
   202
55a02586776d towards quickcheck
haftmann
parents: 24994
diff changeset
   203
instantiation nat :: random
55a02586776d towards quickcheck
haftmann
parents: 24994
diff changeset
   204
begin
55a02586776d towards quickcheck
haftmann
parents: 24994
diff changeset
   205
55a02586776d towards quickcheck
haftmann
parents: 24994
diff changeset
   206
definition
55a02586776d towards quickcheck
haftmann
parents: 24994
diff changeset
   207
  "random k = apfst nat_of_index \<circ> range k"
55a02586776d towards quickcheck
haftmann
parents: 24994
diff changeset
   208
55a02586776d towards quickcheck
haftmann
parents: 24994
diff changeset
   209
instance ..
55a02586776d towards quickcheck
haftmann
parents: 24994
diff changeset
   210
55a02586776d towards quickcheck
haftmann
parents: 24994
diff changeset
   211
end
55a02586776d towards quickcheck
haftmann
parents: 24994
diff changeset
   212
55a02586776d towards quickcheck
haftmann
parents: 24994
diff changeset
   213
instantiation bool :: random
55a02586776d towards quickcheck
haftmann
parents: 24994
diff changeset
   214
begin
55a02586776d towards quickcheck
haftmann
parents: 24994
diff changeset
   215
55a02586776d towards quickcheck
haftmann
parents: 24994
diff changeset
   216
definition
55a02586776d towards quickcheck
haftmann
parents: 24994
diff changeset
   217
  "random _ = apfst (op = 0) \<circ> range 2"
55a02586776d towards quickcheck
haftmann
parents: 24994
diff changeset
   218
55a02586776d towards quickcheck
haftmann
parents: 24994
diff changeset
   219
instance ..
55a02586776d towards quickcheck
haftmann
parents: 24994
diff changeset
   220
55a02586776d towards quickcheck
haftmann
parents: 24994
diff changeset
   221
end
24226
haftmann
parents: 24043
diff changeset
   222
26038
55a02586776d towards quickcheck
haftmann
parents: 24994
diff changeset
   223
instantiation unit :: random
55a02586776d towards quickcheck
haftmann
parents: 24994
diff changeset
   224
begin
55a02586776d towards quickcheck
haftmann
parents: 24994
diff changeset
   225
55a02586776d towards quickcheck
haftmann
parents: 24994
diff changeset
   226
definition
55a02586776d towards quickcheck
haftmann
parents: 24994
diff changeset
   227
  "random _ = Pair ()"
55a02586776d towards quickcheck
haftmann
parents: 24994
diff changeset
   228
55a02586776d towards quickcheck
haftmann
parents: 24994
diff changeset
   229
instance ..
55a02586776d towards quickcheck
haftmann
parents: 24994
diff changeset
   230
55a02586776d towards quickcheck
haftmann
parents: 24994
diff changeset
   231
end
55a02586776d towards quickcheck
haftmann
parents: 24994
diff changeset
   232
55a02586776d towards quickcheck
haftmann
parents: 24994
diff changeset
   233
instantiation "+" :: (random, random) random
55a02586776d towards quickcheck
haftmann
parents: 24994
diff changeset
   234
begin
55a02586776d towards quickcheck
haftmann
parents: 24994
diff changeset
   235
55a02586776d towards quickcheck
haftmann
parents: 24994
diff changeset
   236
definition
55a02586776d towards quickcheck
haftmann
parents: 24994
diff changeset
   237
  "random n = (do
55a02586776d towards quickcheck
haftmann
parents: 24994
diff changeset
   238
     k \<leftarrow> next;
55a02586776d towards quickcheck
haftmann
parents: 24994
diff changeset
   239
     let l = k div 2;
55a02586776d towards quickcheck
haftmann
parents: 24994
diff changeset
   240
     (if k mod 2 = 0 then do 
55a02586776d towards quickcheck
haftmann
parents: 24994
diff changeset
   241
       x \<leftarrow> random l;
55a02586776d towards quickcheck
haftmann
parents: 24994
diff changeset
   242
       return (Inl x)
55a02586776d towards quickcheck
haftmann
parents: 24994
diff changeset
   243
     done else do
55a02586776d towards quickcheck
haftmann
parents: 24994
diff changeset
   244
       x \<leftarrow> random l;
55a02586776d towards quickcheck
haftmann
parents: 24994
diff changeset
   245
       return (Inr x)
55a02586776d towards quickcheck
haftmann
parents: 24994
diff changeset
   246
     done)
55a02586776d towards quickcheck
haftmann
parents: 24994
diff changeset
   247
   done)"
55a02586776d towards quickcheck
haftmann
parents: 24994
diff changeset
   248
55a02586776d towards quickcheck
haftmann
parents: 24994
diff changeset
   249
instance ..
55a02586776d towards quickcheck
haftmann
parents: 24994
diff changeset
   250
55a02586776d towards quickcheck
haftmann
parents: 24994
diff changeset
   251
end
22528
8501c4a62a3c cleaned up HOL/ex/Code*.thy
haftmann
parents:
diff changeset
   252
26038
55a02586776d towards quickcheck
haftmann
parents: 24994
diff changeset
   253
instantiation "*" :: (random, random) random
55a02586776d towards quickcheck
haftmann
parents: 24994
diff changeset
   254
begin
55a02586776d towards quickcheck
haftmann
parents: 24994
diff changeset
   255
55a02586776d towards quickcheck
haftmann
parents: 24994
diff changeset
   256
definition
55a02586776d towards quickcheck
haftmann
parents: 24994
diff changeset
   257
  "random n = (do
55a02586776d towards quickcheck
haftmann
parents: 24994
diff changeset
   258
     x \<leftarrow> random n;
55a02586776d towards quickcheck
haftmann
parents: 24994
diff changeset
   259
     y \<leftarrow> random n;
55a02586776d towards quickcheck
haftmann
parents: 24994
diff changeset
   260
     return (x, y)
55a02586776d towards quickcheck
haftmann
parents: 24994
diff changeset
   261
   done)"
55a02586776d towards quickcheck
haftmann
parents: 24994
diff changeset
   262
55a02586776d towards quickcheck
haftmann
parents: 24994
diff changeset
   263
instance ..
55a02586776d towards quickcheck
haftmann
parents: 24994
diff changeset
   264
55a02586776d towards quickcheck
haftmann
parents: 24994
diff changeset
   265
end
55a02586776d towards quickcheck
haftmann
parents: 24994
diff changeset
   266
55a02586776d towards quickcheck
haftmann
parents: 24994
diff changeset
   267
instantiation int :: random
55a02586776d towards quickcheck
haftmann
parents: 24994
diff changeset
   268
begin
55a02586776d towards quickcheck
haftmann
parents: 24994
diff changeset
   269
55a02586776d towards quickcheck
haftmann
parents: 24994
diff changeset
   270
definition
55a02586776d towards quickcheck
haftmann
parents: 24994
diff changeset
   271
  "random n = (do
55a02586776d towards quickcheck
haftmann
parents: 24994
diff changeset
   272
     (b, m) \<leftarrow> random n;
55a02586776d towards quickcheck
haftmann
parents: 24994
diff changeset
   273
     return (if b then int m else - int m)
55a02586776d towards quickcheck
haftmann
parents: 24994
diff changeset
   274
   done)"
55a02586776d towards quickcheck
haftmann
parents: 24994
diff changeset
   275
55a02586776d towards quickcheck
haftmann
parents: 24994
diff changeset
   276
instance ..
55a02586776d towards quickcheck
haftmann
parents: 24994
diff changeset
   277
55a02586776d towards quickcheck
haftmann
parents: 24994
diff changeset
   278
end
55a02586776d towards quickcheck
haftmann
parents: 24994
diff changeset
   279
55a02586776d towards quickcheck
haftmann
parents: 24994
diff changeset
   280
instantiation list :: (random) random
55a02586776d towards quickcheck
haftmann
parents: 24994
diff changeset
   281
begin
22528
8501c4a62a3c cleaned up HOL/ex/Code*.thy
haftmann
parents:
diff changeset
   282
26038
55a02586776d towards quickcheck
haftmann
parents: 24994
diff changeset
   283
primrec
55a02586776d towards quickcheck
haftmann
parents: 24994
diff changeset
   284
  random_list_aux
55a02586776d towards quickcheck
haftmann
parents: 24994
diff changeset
   285
where
55a02586776d towards quickcheck
haftmann
parents: 24994
diff changeset
   286
  "random_list_aux 0 = Pair []"
55a02586776d towards quickcheck
haftmann
parents: 24994
diff changeset
   287
  | "random_list_aux (Suc n) = (do
55a02586776d towards quickcheck
haftmann
parents: 24994
diff changeset
   288
       x \<leftarrow> random (index_of_nat (Suc n));
55a02586776d towards quickcheck
haftmann
parents: 24994
diff changeset
   289
       xs \<leftarrow> random_list_aux n;
55a02586776d towards quickcheck
haftmann
parents: 24994
diff changeset
   290
       return (x#xs)
55a02586776d towards quickcheck
haftmann
parents: 24994
diff changeset
   291
     done)"
55a02586776d towards quickcheck
haftmann
parents: 24994
diff changeset
   292
55a02586776d towards quickcheck
haftmann
parents: 24994
diff changeset
   293
definition
55a02586776d towards quickcheck
haftmann
parents: 24994
diff changeset
   294
  [code func del]: "random n = random_list_aux (nat_of_index n)"
55a02586776d towards quickcheck
haftmann
parents: 24994
diff changeset
   295
55a02586776d towards quickcheck
haftmann
parents: 24994
diff changeset
   296
lemma [code func]:
55a02586776d towards quickcheck
haftmann
parents: 24994
diff changeset
   297
  "random n = (if n = 0 then return ([]::'a list)
55a02586776d towards quickcheck
haftmann
parents: 24994
diff changeset
   298
    else do
55a02586776d towards quickcheck
haftmann
parents: 24994
diff changeset
   299
       x \<leftarrow> random n;
55a02586776d towards quickcheck
haftmann
parents: 24994
diff changeset
   300
       xs \<leftarrow> random (n - 1);
55a02586776d towards quickcheck
haftmann
parents: 24994
diff changeset
   301
       return (x#xs)
55a02586776d towards quickcheck
haftmann
parents: 24994
diff changeset
   302
     done)"
55a02586776d towards quickcheck
haftmann
parents: 24994
diff changeset
   303
unfolding random_list_def
55a02586776d towards quickcheck
haftmann
parents: 24994
diff changeset
   304
by (cases "nat_of_index n", auto)
55a02586776d towards quickcheck
haftmann
parents: 24994
diff changeset
   305
  (cases n, auto)+
55a02586776d towards quickcheck
haftmann
parents: 24994
diff changeset
   306
55a02586776d towards quickcheck
haftmann
parents: 24994
diff changeset
   307
(*fun
55a02586776d towards quickcheck
haftmann
parents: 24994
diff changeset
   308
  random_list
55a02586776d towards quickcheck
haftmann
parents: 24994
diff changeset
   309
where
55a02586776d towards quickcheck
haftmann
parents: 24994
diff changeset
   310
  "random_list n = (if n = 0 then (\<lambda>_. ([]::'a list)) 
55a02586776d towards quickcheck
haftmann
parents: 24994
diff changeset
   311
    else random n \<guillemotright>=\<^isub>R (\<lambda>x::'a. random_list (n - 1) \<guillemotright>=\<^isub>R (\<lambda>(xs::'a list) _. x#xs)))"*)
55a02586776d towards quickcheck
haftmann
parents: 24994
diff changeset
   312
55a02586776d towards quickcheck
haftmann
parents: 24994
diff changeset
   313
instance ..
22528
8501c4a62a3c cleaned up HOL/ex/Code*.thy
haftmann
parents:
diff changeset
   314
8501c4a62a3c cleaned up HOL/ex/Code*.thy
haftmann
parents:
diff changeset
   315
end
26038
55a02586776d towards quickcheck
haftmann
parents: 24994
diff changeset
   316
55a02586776d towards quickcheck
haftmann
parents: 24994
diff changeset
   317
code_reserved SML Quickcheck
55a02586776d towards quickcheck
haftmann
parents: 24994
diff changeset
   318
55a02586776d towards quickcheck
haftmann
parents: 24994
diff changeset
   319
55a02586776d towards quickcheck
haftmann
parents: 24994
diff changeset
   320
subsection {* Quickcheck generator *}
55a02586776d towards quickcheck
haftmann
parents: 24994
diff changeset
   321
55a02586776d towards quickcheck
haftmann
parents: 24994
diff changeset
   322
ML {*
55a02586776d towards quickcheck
haftmann
parents: 24994
diff changeset
   323
structure Quickcheck =
55a02586776d towards quickcheck
haftmann
parents: 24994
diff changeset
   324
struct
55a02586776d towards quickcheck
haftmann
parents: 24994
diff changeset
   325
55a02586776d towards quickcheck
haftmann
parents: 24994
diff changeset
   326
open Quickcheck;
55a02586776d towards quickcheck
haftmann
parents: 24994
diff changeset
   327
55a02586776d towards quickcheck
haftmann
parents: 24994
diff changeset
   328
val eval_ref : (unit -> int -> int * int -> term list option * (int * int)) option ref = ref NONE;
55a02586776d towards quickcheck
haftmann
parents: 24994
diff changeset
   329
55a02586776d towards quickcheck
haftmann
parents: 24994
diff changeset
   330
fun mk_generator_expr prop tys =
55a02586776d towards quickcheck
haftmann
parents: 24994
diff changeset
   331
  let
55a02586776d towards quickcheck
haftmann
parents: 24994
diff changeset
   332
    val bounds = map_index (fn (i, ty) => (i, ty)) tys;
55a02586776d towards quickcheck
haftmann
parents: 24994
diff changeset
   333
    val result = list_comb (prop, map (fn (i, _) => Bound (length tys - i - 1)) bounds);
55a02586776d towards quickcheck
haftmann
parents: 24994
diff changeset
   334
    val terms = map (fn (i, ty) => Const (@{const_name Eval.term_of}, ty --> @{typ term}) $ Bound (length tys - i - 1)) bounds;
55a02586776d towards quickcheck
haftmann
parents: 24994
diff changeset
   335
    val check = @{term "If \<Colon> bool \<Rightarrow> term list option \<Rightarrow> term list option \<Rightarrow> term list option"}
55a02586776d towards quickcheck
haftmann
parents: 24994
diff changeset
   336
      $ result $ @{term "None \<Colon> term list option"} $ (@{term "Some \<Colon> term list \<Rightarrow> term list option "} $ HOLogic.mk_list @{typ term} terms);
55a02586776d towards quickcheck
haftmann
parents: 24994
diff changeset
   337
    val return = @{term "Pair \<Colon> term list option \<Rightarrow> seed \<Rightarrow> term list option \<times> seed"};
55a02586776d towards quickcheck
haftmann
parents: 24994
diff changeset
   338
    fun mk_bindtyp ty = @{typ seed} --> HOLogic.mk_prodT (ty, @{typ seed});
55a02586776d towards quickcheck
haftmann
parents: 24994
diff changeset
   339
    fun mk_bindclause (i, ty) t = Const (@{const_name mbind}, mk_bindtyp ty
55a02586776d towards quickcheck
haftmann
parents: 24994
diff changeset
   340
      --> (ty --> mk_bindtyp @{typ "term list option"}) --> mk_bindtyp @{typ "term list option"})
55a02586776d towards quickcheck
haftmann
parents: 24994
diff changeset
   341
      $ (Const (@{const_name random}, @{typ index} --> mk_bindtyp ty)
55a02586776d towards quickcheck
haftmann
parents: 24994
diff changeset
   342
        $ Bound i) $ Abs ("a", ty, t);
55a02586776d towards quickcheck
haftmann
parents: 24994
diff changeset
   343
    val t = fold_rev mk_bindclause bounds (return $ check);
55a02586776d towards quickcheck
haftmann
parents: 24994
diff changeset
   344
  in Abs ("n", @{typ index}, t) end;
55a02586776d towards quickcheck
haftmann
parents: 24994
diff changeset
   345
55a02586776d towards quickcheck
haftmann
parents: 24994
diff changeset
   346
fun compile_generator_expr thy prop tys =
55a02586776d towards quickcheck
haftmann
parents: 24994
diff changeset
   347
  let
55a02586776d towards quickcheck
haftmann
parents: 24994
diff changeset
   348
    val f = CodePackage.eval_term ("Quickcheck.eval_ref", eval_ref) thy
55a02586776d towards quickcheck
haftmann
parents: 24994
diff changeset
   349
      (mk_generator_expr prop tys) [];
55a02586776d towards quickcheck
haftmann
parents: 24994
diff changeset
   350
  in f #> run #> (Option.map o map) (Code.postprocess_term thy) end;
55a02586776d towards quickcheck
haftmann
parents: 24994
diff changeset
   351
55a02586776d towards quickcheck
haftmann
parents: 24994
diff changeset
   352
end
55a02586776d towards quickcheck
haftmann
parents: 24994
diff changeset
   353
*}
55a02586776d towards quickcheck
haftmann
parents: 24994
diff changeset
   354
55a02586776d towards quickcheck
haftmann
parents: 24994
diff changeset
   355
ML {* val f = Quickcheck.compile_generator_expr @{theory}
55a02586776d towards quickcheck
haftmann
parents: 24994
diff changeset
   356
  @{term "\<lambda>(n::nat) (m::nat) (q::nat). n = m + q + 1"} [@{typ nat}, @{typ nat}, @{typ nat}] *}
55a02586776d towards quickcheck
haftmann
parents: 24994
diff changeset
   357
55a02586776d towards quickcheck
haftmann
parents: 24994
diff changeset
   358
ML {* f 5 |> (Option.map o map) (Sign.string_of_term @{theory}) *}
55a02586776d towards quickcheck
haftmann
parents: 24994
diff changeset
   359
ML {* f 5 |> (Option.map o map) (Sign.string_of_term @{theory}) *}
55a02586776d towards quickcheck
haftmann
parents: 24994
diff changeset
   360
ML {* f 20 |> (Option.map o map) (Sign.string_of_term @{theory}) *}
55a02586776d towards quickcheck
haftmann
parents: 24994
diff changeset
   361
ML {* f 20 |> (Option.map o map) (Sign.string_of_term @{theory}) *}
55a02586776d towards quickcheck
haftmann
parents: 24994
diff changeset
   362
ML {* f 20 |> (Option.map o map) (Sign.string_of_term @{theory}) *}
55a02586776d towards quickcheck
haftmann
parents: 24994
diff changeset
   363
ML {* f 20 |> (Option.map o map) (Sign.string_of_term @{theory}) *}
55a02586776d towards quickcheck
haftmann
parents: 24994
diff changeset
   364
ML {* f 25 |> (Option.map o map) (Sign.string_of_term @{theory}) *}
55a02586776d towards quickcheck
haftmann
parents: 24994
diff changeset
   365
ML {* f 1 |> (Option.map o map) (Sign.string_of_term @{theory}) *}
55a02586776d towards quickcheck
haftmann
parents: 24994
diff changeset
   366
ML {* f 1 |> (Option.map o map) (Sign.string_of_term @{theory}) *}
55a02586776d towards quickcheck
haftmann
parents: 24994
diff changeset
   367
ML {* f 2 |> (Option.map o map) (Sign.string_of_term @{theory}) *}
55a02586776d towards quickcheck
haftmann
parents: 24994
diff changeset
   368
ML {* f 2 |> (Option.map o map) (Sign.string_of_term @{theory}) *}
55a02586776d towards quickcheck
haftmann
parents: 24994
diff changeset
   369
55a02586776d towards quickcheck
haftmann
parents: 24994
diff changeset
   370
ML {* val f = Quickcheck.compile_generator_expr @{theory}
55a02586776d towards quickcheck
haftmann
parents: 24994
diff changeset
   371
  @{term "\<lambda>(n::int) (m::int) (q::int). n = m + q + 1"} [@{typ int}, @{typ int}, @{typ int}] *}
55a02586776d towards quickcheck
haftmann
parents: 24994
diff changeset
   372
55a02586776d towards quickcheck
haftmann
parents: 24994
diff changeset
   373
ML {* f 5 |> (Option.map o map) (Sign.string_of_term @{theory}) *}
55a02586776d towards quickcheck
haftmann
parents: 24994
diff changeset
   374
ML {* f 5 |> (Option.map o map) (Sign.string_of_term @{theory}) *}
55a02586776d towards quickcheck
haftmann
parents: 24994
diff changeset
   375
ML {* f 20 |> (Option.map o map) (Sign.string_of_term @{theory}) *}
55a02586776d towards quickcheck
haftmann
parents: 24994
diff changeset
   376
ML {* f 20 |> (Option.map o map) (Sign.string_of_term @{theory}) *}
55a02586776d towards quickcheck
haftmann
parents: 24994
diff changeset
   377
ML {* f 20 |> (Option.map o map) (Sign.string_of_term @{theory}) *}
55a02586776d towards quickcheck
haftmann
parents: 24994
diff changeset
   378
ML {* f 20 |> (Option.map o map) (Sign.string_of_term @{theory}) *}
55a02586776d towards quickcheck
haftmann
parents: 24994
diff changeset
   379
ML {* f 25 |> (Option.map o map) (Sign.string_of_term @{theory}) *}
55a02586776d towards quickcheck
haftmann
parents: 24994
diff changeset
   380
ML {* f 1 |> (Option.map o map) (Sign.string_of_term @{theory}) *}
55a02586776d towards quickcheck
haftmann
parents: 24994
diff changeset
   381
ML {* f 1 |> (Option.map o map) (Sign.string_of_term @{theory}) *}
55a02586776d towards quickcheck
haftmann
parents: 24994
diff changeset
   382
ML {* f 2 |> (Option.map o map) (Sign.string_of_term @{theory}) *}
55a02586776d towards quickcheck
haftmann
parents: 24994
diff changeset
   383
ML {* f 2 |> (Option.map o map) (Sign.string_of_term @{theory}) *}
55a02586776d towards quickcheck
haftmann
parents: 24994
diff changeset
   384
55a02586776d towards quickcheck
haftmann
parents: 24994
diff changeset
   385
55a02586776d towards quickcheck
haftmann
parents: 24994
diff changeset
   386
subsection {* Incremental function generator *}
55a02586776d towards quickcheck
haftmann
parents: 24994
diff changeset
   387
55a02586776d towards quickcheck
haftmann
parents: 24994
diff changeset
   388
ML {*
55a02586776d towards quickcheck
haftmann
parents: 24994
diff changeset
   389
structure Quickcheck =
55a02586776d towards quickcheck
haftmann
parents: 24994
diff changeset
   390
struct
55a02586776d towards quickcheck
haftmann
parents: 24994
diff changeset
   391
55a02586776d towards quickcheck
haftmann
parents: 24994
diff changeset
   392
open Quickcheck;
55a02586776d towards quickcheck
haftmann
parents: 24994
diff changeset
   393
55a02586776d towards quickcheck
haftmann
parents: 24994
diff changeset
   394
fun random_fun (eq : 'a -> 'a -> bool)
55a02586776d towards quickcheck
haftmann
parents: 24994
diff changeset
   395
    (random : seed -> 'b * seed)
55a02586776d towards quickcheck
haftmann
parents: 24994
diff changeset
   396
    (random_split : seed -> seed * seed)
55a02586776d towards quickcheck
haftmann
parents: 24994
diff changeset
   397
    (seed : seed) =
55a02586776d towards quickcheck
haftmann
parents: 24994
diff changeset
   398
  let
55a02586776d towards quickcheck
haftmann
parents: 24994
diff changeset
   399
    val (seed', seed'') = random_split seed;
55a02586776d towards quickcheck
haftmann
parents: 24994
diff changeset
   400
    val state = ref (seed', []);
55a02586776d towards quickcheck
haftmann
parents: 24994
diff changeset
   401
    fun random_fun' x =
55a02586776d towards quickcheck
haftmann
parents: 24994
diff changeset
   402
      let
55a02586776d towards quickcheck
haftmann
parents: 24994
diff changeset
   403
        val (seed, fun_map) = ! state;
55a02586776d towards quickcheck
haftmann
parents: 24994
diff changeset
   404
      in case AList.lookup (uncurry eq) fun_map x
55a02586776d towards quickcheck
haftmann
parents: 24994
diff changeset
   405
       of SOME y => y
55a02586776d towards quickcheck
haftmann
parents: 24994
diff changeset
   406
        | NONE => let
55a02586776d towards quickcheck
haftmann
parents: 24994
diff changeset
   407
              val (y, seed') = random seed;
55a02586776d towards quickcheck
haftmann
parents: 24994
diff changeset
   408
              val _ = state := (seed', (x, y) :: fun_map);
55a02586776d towards quickcheck
haftmann
parents: 24994
diff changeset
   409
            in y end
55a02586776d towards quickcheck
haftmann
parents: 24994
diff changeset
   410
      end;
55a02586776d towards quickcheck
haftmann
parents: 24994
diff changeset
   411
  in (random_fun', seed'') end;
55a02586776d towards quickcheck
haftmann
parents: 24994
diff changeset
   412
55a02586776d towards quickcheck
haftmann
parents: 24994
diff changeset
   413
end
55a02586776d towards quickcheck
haftmann
parents: 24994
diff changeset
   414
*}
55a02586776d towards quickcheck
haftmann
parents: 24994
diff changeset
   415
55a02586776d towards quickcheck
haftmann
parents: 24994
diff changeset
   416
axiomatization
55a02586776d towards quickcheck
haftmann
parents: 24994
diff changeset
   417
  random_fun_aux :: "('a \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> (seed \<Rightarrow> 'b \<times> seed)
55a02586776d towards quickcheck
haftmann
parents: 24994
diff changeset
   418
    \<Rightarrow> (seed \<Rightarrow> seed \<times> seed) \<Rightarrow> seed \<Rightarrow> ('a \<Rightarrow> 'b) \<times> seed"
55a02586776d towards quickcheck
haftmann
parents: 24994
diff changeset
   419
55a02586776d towards quickcheck
haftmann
parents: 24994
diff changeset
   420
code_const random_fun_aux (SML "Quickcheck.random'_fun")
55a02586776d towards quickcheck
haftmann
parents: 24994
diff changeset
   421
55a02586776d towards quickcheck
haftmann
parents: 24994
diff changeset
   422
instantiation "fun" :: (term_of, term_of) term_of
55a02586776d towards quickcheck
haftmann
parents: 24994
diff changeset
   423
begin
55a02586776d towards quickcheck
haftmann
parents: 24994
diff changeset
   424
55a02586776d towards quickcheck
haftmann
parents: 24994
diff changeset
   425
instance ..
55a02586776d towards quickcheck
haftmann
parents: 24994
diff changeset
   426
55a02586776d towards quickcheck
haftmann
parents: 24994
diff changeset
   427
end
55a02586776d towards quickcheck
haftmann
parents: 24994
diff changeset
   428
55a02586776d towards quickcheck
haftmann
parents: 24994
diff changeset
   429
code_const "Eval.term_of :: ('a\<Colon>term_of \<Rightarrow> 'b\<Colon>term_of) \<Rightarrow> _"
55a02586776d towards quickcheck
haftmann
parents: 24994
diff changeset
   430
  (SML "(fn '_ => Const (\"arbitrary\", dummyT))")
55a02586776d towards quickcheck
haftmann
parents: 24994
diff changeset
   431
55a02586776d towards quickcheck
haftmann
parents: 24994
diff changeset
   432
instantiation "fun" :: (eq, random) random
55a02586776d towards quickcheck
haftmann
parents: 24994
diff changeset
   433
begin
55a02586776d towards quickcheck
haftmann
parents: 24994
diff changeset
   434
55a02586776d towards quickcheck
haftmann
parents: 24994
diff changeset
   435
definition
55a02586776d towards quickcheck
haftmann
parents: 24994
diff changeset
   436
  "random n = random_fun_aux (op =) (random n) split_seed"
55a02586776d towards quickcheck
haftmann
parents: 24994
diff changeset
   437
55a02586776d towards quickcheck
haftmann
parents: 24994
diff changeset
   438
instance ..
55a02586776d towards quickcheck
haftmann
parents: 24994
diff changeset
   439
55a02586776d towards quickcheck
haftmann
parents: 24994
diff changeset
   440
end
55a02586776d towards quickcheck
haftmann
parents: 24994
diff changeset
   441
55a02586776d towards quickcheck
haftmann
parents: 24994
diff changeset
   442
ML {* val f = Quickcheck.compile_generator_expr @{theory}
55a02586776d towards quickcheck
haftmann
parents: 24994
diff changeset
   443
  @{term "\<lambda>f k. int (f k) = k"} [@{typ "int \<Rightarrow> nat"}, @{typ int}] *}
55a02586776d towards quickcheck
haftmann
parents: 24994
diff changeset
   444
55a02586776d towards quickcheck
haftmann
parents: 24994
diff changeset
   445
ML {* f 20 |> (Option.map o map) (Sign.string_of_term @{theory}) *}
55a02586776d towards quickcheck
haftmann
parents: 24994
diff changeset
   446
ML {* f 20 |> (Option.map o map) (Sign.string_of_term @{theory}) *}
55a02586776d towards quickcheck
haftmann
parents: 24994
diff changeset
   447
ML {* f 20 |> (Option.map o map) (Sign.string_of_term @{theory}) *}
55a02586776d towards quickcheck
haftmann
parents: 24994
diff changeset
   448
ML {* f 20 |> (Option.map o map) (Sign.string_of_term @{theory}) *}
55a02586776d towards quickcheck
haftmann
parents: 24994
diff changeset
   449
ML {* f 20 |> (Option.map o map) (Sign.string_of_term @{theory}) *}
55a02586776d towards quickcheck
haftmann
parents: 24994
diff changeset
   450
ML {* f 20 |> (Option.map o map) (Sign.string_of_term @{theory}) *}
55a02586776d towards quickcheck
haftmann
parents: 24994
diff changeset
   451
55a02586776d towards quickcheck
haftmann
parents: 24994
diff changeset
   452
end