src/HOL/ex/Random.thy
author haftmann
Wed, 12 Mar 2008 08:47:37 +0100
changeset 26261 b6a103ace4db
parent 26142 3d5df9a56537
child 26265 4b63b9e9b10d
permissions -rw-r--r--
continued
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
26142
3d5df9a56537 some steps towards automated generators
haftmann
parents: 26042
diff changeset
    45
  pick :: "(index \<times> 'a) list \<Rightarrow> index \<Rightarrow> 'a"
26038
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
26142
3d5df9a56537 some steps towards automated generators
haftmann
parents: 26042
diff changeset
    86
  select_weight :: "(index \<times> 'a) list \<Rightarrow> seed \<Rightarrow> 'a \<times> seed"
26038
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
26142
3d5df9a56537 some steps towards automated generators
haftmann
parents: 26042
diff changeset
    89
    (k, s') = range (foldr (op + \<circ> fst) xs 0) s
3d5df9a56537 some steps towards automated generators
haftmann
parents: 26042
diff changeset
    90
  in (pick xs k, s'))"
26038
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
26042
e7a421d1f5c1 continued
haftmann
parents: 26038
diff changeset
   198
class random =
e7a421d1f5c1 continued
haftmann
parents: 26038
diff changeset
   199
  fixes random :: "index \<Rightarrow> seed \<Rightarrow> 'a\<Colon>{} \<times> seed"
26038
55a02586776d towards quickcheck
haftmann
parents: 24994
diff changeset
   200
26261
b6a103ace4db continued
haftmann
parents: 26142
diff changeset
   201
instantiation itself :: (type) random
26038
55a02586776d towards quickcheck
haftmann
parents: 24994
diff changeset
   202
begin
55a02586776d towards quickcheck
haftmann
parents: 24994
diff changeset
   203
55a02586776d towards quickcheck
haftmann
parents: 24994
diff changeset
   204
definition
26261
b6a103ace4db continued
haftmann
parents: 26142
diff changeset
   205
  "random _ = return TYPE('a)"
26038
55a02586776d towards quickcheck
haftmann
parents: 24994
diff changeset
   206
55a02586776d towards quickcheck
haftmann
parents: 24994
diff changeset
   207
instance ..
55a02586776d towards quickcheck
haftmann
parents: 24994
diff changeset
   208
55a02586776d towards quickcheck
haftmann
parents: 24994
diff changeset
   209
end
55a02586776d towards quickcheck
haftmann
parents: 24994
diff changeset
   210
26261
b6a103ace4db continued
haftmann
parents: 26142
diff changeset
   211
lemma random_aux_if:
b6a103ace4db continued
haftmann
parents: 26142
diff changeset
   212
  fixes random' :: "index \<Rightarrow> index \<Rightarrow> seed \<Rightarrow> 'a \<times> seed"
b6a103ace4db continued
haftmann
parents: 26142
diff changeset
   213
  assumes "random' 0 j = undefined"
b6a103ace4db continued
haftmann
parents: 26142
diff changeset
   214
    and "\<And>i. random' (Suc_index i) j = rhs2 i"
b6a103ace4db continued
haftmann
parents: 26142
diff changeset
   215
  shows "random' i j s = (if i = 0 then undefined else rhs2 (i - 1) s)"
b6a103ace4db continued
haftmann
parents: 26142
diff changeset
   216
  by (cases i rule: index.exhaust) (insert assms, simp_all add: undefined_fun)
26038
55a02586776d towards quickcheck
haftmann
parents: 24994
diff changeset
   217
26261
b6a103ace4db continued
haftmann
parents: 26142
diff changeset
   218
setup {*
b6a103ace4db continued
haftmann
parents: 26142
diff changeset
   219
let
b6a103ace4db continued
haftmann
parents: 26142
diff changeset
   220
  fun random_inst tyco thy =
b6a103ace4db continued
haftmann
parents: 26142
diff changeset
   221
    let
b6a103ace4db continued
haftmann
parents: 26142
diff changeset
   222
      val { descr, index, ... } = DatatypePackage.the_datatype thy tyco;
b6a103ace4db continued
haftmann
parents: 26142
diff changeset
   223
      val (raw_vs, _) = DatatypePackage.the_datatype_spec thy tyco;
b6a103ace4db continued
haftmann
parents: 26142
diff changeset
   224
      val vs = (map o apsnd)
b6a103ace4db continued
haftmann
parents: 26142
diff changeset
   225
        (curry (Sorts.inter_sort (Sign.classes_of thy)) @{sort random}) raw_vs;
b6a103ace4db continued
haftmann
parents: 26142
diff changeset
   226
      val ty = Type (tyco, map TFree vs);
b6a103ace4db continued
haftmann
parents: 26142
diff changeset
   227
      val typ_of = DatatypeAux.typ_of_dtyp descr vs;
b6a103ace4db continued
haftmann
parents: 26142
diff changeset
   228
      val SOME (_, _, constrs) = AList.lookup (op =) descr index;
b6a103ace4db continued
haftmann
parents: 26142
diff changeset
   229
      val randomN = NameSpace.base @{const_name random};
b6a103ace4db continued
haftmann
parents: 26142
diff changeset
   230
      val random_aux_name = randomN ^ "_" ^ Class.type_name tyco ^ "'";
b6a103ace4db continued
haftmann
parents: 26142
diff changeset
   231
      fun lift_ty ty = StateMonad.liftT ty @{typ seed};
b6a103ace4db continued
haftmann
parents: 26142
diff changeset
   232
      val ty_aux = @{typ index} --> @{typ index} --> lift_ty ty;
b6a103ace4db continued
haftmann
parents: 26142
diff changeset
   233
      fun random ty =
b6a103ace4db continued
haftmann
parents: 26142
diff changeset
   234
        Const (@{const_name random}, @{typ index} --> lift_ty ty);
b6a103ace4db continued
haftmann
parents: 26142
diff changeset
   235
      val random_aux = Free (random_aux_name, ty_aux);
b6a103ace4db continued
haftmann
parents: 26142
diff changeset
   236
      fun add_cons_arg dty (is_rec, t) =
b6a103ace4db continued
haftmann
parents: 26142
diff changeset
   237
        let
b6a103ace4db continued
haftmann
parents: 26142
diff changeset
   238
          val ty' = typ_of dty;
b6a103ace4db continued
haftmann
parents: 26142
diff changeset
   239
          val random' = if can DatatypeAux.dest_DtRec dty
b6a103ace4db continued
haftmann
parents: 26142
diff changeset
   240
            then random_aux $ @{term "i\<Colon>index"} $ @{term "j\<Colon>index"}
b6a103ace4db continued
haftmann
parents: 26142
diff changeset
   241
            else random ty' $ @{term "j\<Colon>index"}
b6a103ace4db continued
haftmann
parents: 26142
diff changeset
   242
          val is_rec' = is_rec orelse DatatypeAux.is_rec_type dty;
b6a103ace4db continued
haftmann
parents: 26142
diff changeset
   243
          val t' = StateMonad.mbind ty' ty @{typ seed} random' (Abs ("", ty', t))
b6a103ace4db continued
haftmann
parents: 26142
diff changeset
   244
        in (is_rec', t') end;
b6a103ace4db continued
haftmann
parents: 26142
diff changeset
   245
      fun mk_cons_t (c, dtys) =
b6a103ace4db continued
haftmann
parents: 26142
diff changeset
   246
        let
b6a103ace4db continued
haftmann
parents: 26142
diff changeset
   247
          val ty' = map typ_of dtys ---> ty;
b6a103ace4db continued
haftmann
parents: 26142
diff changeset
   248
          val t = StateMonad.return ty @{typ seed} (list_comb (Const (c, ty'),
b6a103ace4db continued
haftmann
parents: 26142
diff changeset
   249
            map Bound (length dtys - 1 downto 0)));
b6a103ace4db continued
haftmann
parents: 26142
diff changeset
   250
          val (is_rec, t') = fold_rev add_cons_arg dtys (false, t);
b6a103ace4db continued
haftmann
parents: 26142
diff changeset
   251
        in (is_rec, StateMonad.run ty @{typ seed} t') end;
b6a103ace4db continued
haftmann
parents: 26142
diff changeset
   252
      fun check_empty [] = NONE
b6a103ace4db continued
haftmann
parents: 26142
diff changeset
   253
        | check_empty xs = SOME xs;
b6a103ace4db continued
haftmann
parents: 26142
diff changeset
   254
      fun bundle_cons_ts cons_ts =
b6a103ace4db continued
haftmann
parents: 26142
diff changeset
   255
        let
b6a103ace4db continued
haftmann
parents: 26142
diff changeset
   256
          val ts = map snd cons_ts;
b6a103ace4db continued
haftmann
parents: 26142
diff changeset
   257
          val t = HOLogic.mk_list (lift_ty ty) ts;
b6a103ace4db continued
haftmann
parents: 26142
diff changeset
   258
          val t' = Const (@{const_name select}, HOLogic.listT (lift_ty ty) --> lift_ty (lift_ty ty)) $ t;
b6a103ace4db continued
haftmann
parents: 26142
diff changeset
   259
          val t'' = Const (@{const_name collapse}, lift_ty (lift_ty ty) --> lift_ty ty) $ t';
b6a103ace4db continued
haftmann
parents: 26142
diff changeset
   260
        in t'' end;
b6a103ace4db continued
haftmann
parents: 26142
diff changeset
   261
      fun bundle_conss (some_rec_t, nonrec_t) =
b6a103ace4db continued
haftmann
parents: 26142
diff changeset
   262
        let
b6a103ace4db continued
haftmann
parents: 26142
diff changeset
   263
          val rec' = case some_rec_t
b6a103ace4db continued
haftmann
parents: 26142
diff changeset
   264
           of SOME rec_t => SOME (HOLogic.mk_prod (@{term "i\<Colon>index"}, rec_t))
b6a103ace4db continued
haftmann
parents: 26142
diff changeset
   265
            | NONE => NONE;
b6a103ace4db continued
haftmann
parents: 26142
diff changeset
   266
          val nonrec' = HOLogic.mk_prod (@{term "1\<Colon>index"}, nonrec_t);
b6a103ace4db continued
haftmann
parents: 26142
diff changeset
   267
          val i_ty = HOLogic.mk_prodT (@{typ index}, lift_ty ty);
b6a103ace4db continued
haftmann
parents: 26142
diff changeset
   268
          val t = HOLogic.mk_list i_ty (the_list rec' @ single nonrec');
b6a103ace4db continued
haftmann
parents: 26142
diff changeset
   269
          val t' = Const (@{const_name select_weight}, HOLogic.listT i_ty --> lift_ty (lift_ty ty)) $ t;
b6a103ace4db continued
haftmann
parents: 26142
diff changeset
   270
          val t'' = Const (@{const_name collapse}, lift_ty (lift_ty ty) --> lift_ty ty) $ t';
b6a103ace4db continued
haftmann
parents: 26142
diff changeset
   271
        in t'' end;
b6a103ace4db continued
haftmann
parents: 26142
diff changeset
   272
      val random_rhs = constrs
b6a103ace4db continued
haftmann
parents: 26142
diff changeset
   273
        |> map mk_cons_t 
b6a103ace4db continued
haftmann
parents: 26142
diff changeset
   274
        |> List.partition fst
b6a103ace4db continued
haftmann
parents: 26142
diff changeset
   275
        |> apfst (Option.map bundle_cons_ts o check_empty)
b6a103ace4db continued
haftmann
parents: 26142
diff changeset
   276
        |> apsnd bundle_cons_ts
b6a103ace4db continued
haftmann
parents: 26142
diff changeset
   277
        |> bundle_conss;
b6a103ace4db continued
haftmann
parents: 26142
diff changeset
   278
      val random_aux_undef = (HOLogic.mk_Trueprop o HOLogic.mk_eq)
b6a103ace4db continued
haftmann
parents: 26142
diff changeset
   279
        (random_aux $ @{term "0\<Colon>index"} $ @{term "j\<Colon>index"}, Const (@{const_name undefined}, lift_ty ty))
b6a103ace4db continued
haftmann
parents: 26142
diff changeset
   280
      val random_aux_eq = (HOLogic.mk_Trueprop o HOLogic.mk_eq)
b6a103ace4db continued
haftmann
parents: 26142
diff changeset
   281
        (random_aux $ @{term "Suc_index i"} $ @{term "j\<Colon>index"}, random_rhs);
b6a103ace4db continued
haftmann
parents: 26142
diff changeset
   282
      val random_eq = (HOLogic.mk_Trueprop o HOLogic.mk_eq) (Const (@{const_name random},
b6a103ace4db continued
haftmann
parents: 26142
diff changeset
   283
        @{typ index} --> lift_ty ty) $ @{term "i\<Colon>index"},
b6a103ace4db continued
haftmann
parents: 26142
diff changeset
   284
          random_aux $ @{term "i\<Colon>index"} $ @{term "i\<Colon>index"});
b6a103ace4db continued
haftmann
parents: 26142
diff changeset
   285
      val del_func = Attrib.internal (fn _ => Thm.declaration_attribute
b6a103ace4db continued
haftmann
parents: 26142
diff changeset
   286
        (fn thm => Context.mapping (Code.del_func thm) I));
b6a103ace4db continued
haftmann
parents: 26142
diff changeset
   287
      fun add_code simps lthy =
b6a103ace4db continued
haftmann
parents: 26142
diff changeset
   288
        let
b6a103ace4db continued
haftmann
parents: 26142
diff changeset
   289
          val thy = ProofContext.theory_of lthy;
b6a103ace4db continued
haftmann
parents: 26142
diff changeset
   290
          val thm = @{thm random_aux_if}
b6a103ace4db continued
haftmann
parents: 26142
diff changeset
   291
            |> Drule.instantiate' [SOME (Thm.ctyp_of thy ty)] [SOME (Thm.cterm_of thy random_aux)]
b6a103ace4db continued
haftmann
parents: 26142
diff changeset
   292
            |> (fn thm => thm OF simps)
b6a103ace4db continued
haftmann
parents: 26142
diff changeset
   293
            |> singleton (ProofContext.export lthy (ProofContext.init thy))
b6a103ace4db continued
haftmann
parents: 26142
diff changeset
   294
        in
b6a103ace4db continued
haftmann
parents: 26142
diff changeset
   295
          lthy
b6a103ace4db continued
haftmann
parents: 26142
diff changeset
   296
          |> LocalTheory.theory (PureThy.note Thm.internalK (random_aux_name ^ "_code", thm)
b6a103ace4db continued
haftmann
parents: 26142
diff changeset
   297
               #-> Code.add_func)
b6a103ace4db continued
haftmann
parents: 26142
diff changeset
   298
        end;
b6a103ace4db continued
haftmann
parents: 26142
diff changeset
   299
    in
b6a103ace4db continued
haftmann
parents: 26142
diff changeset
   300
      thy
b6a103ace4db continued
haftmann
parents: 26142
diff changeset
   301
      |> TheoryTarget.instantiation ([tyco], vs, @{sort random})
b6a103ace4db continued
haftmann
parents: 26142
diff changeset
   302
      |> PrimrecPackage.add_primrec [(random_aux_name, SOME ty_aux, NoSyn)]
b6a103ace4db continued
haftmann
parents: 26142
diff changeset
   303
           [(("", [del_func]), random_aux_undef), (("", [del_func]), random_aux_eq)]
b6a103ace4db continued
haftmann
parents: 26142
diff changeset
   304
      |-> add_code
b6a103ace4db continued
haftmann
parents: 26142
diff changeset
   305
      |> `(fn lthy => Syntax.check_term lthy random_eq)
b6a103ace4db continued
haftmann
parents: 26142
diff changeset
   306
      |-> (fn eq => Specification.definition (NONE, (("", []), eq)))
b6a103ace4db continued
haftmann
parents: 26142
diff changeset
   307
      |> snd
b6a103ace4db continued
haftmann
parents: 26142
diff changeset
   308
      |> Class.prove_instantiation_instance (K (Class.intro_classes_tac []))
b6a103ace4db continued
haftmann
parents: 26142
diff changeset
   309
      |> LocalTheory.exit
b6a103ace4db continued
haftmann
parents: 26142
diff changeset
   310
      |> ProofContext.theory_of
b6a103ace4db continued
haftmann
parents: 26142
diff changeset
   311
    end;
b6a103ace4db continued
haftmann
parents: 26142
diff changeset
   312
  fun add_random_inst [tyco] = (fn thy => case try (random_inst tyco) thy
b6a103ace4db continued
haftmann
parents: 26142
diff changeset
   313
       of SOME thy => thy
b6a103ace4db continued
haftmann
parents: 26142
diff changeset
   314
        | NONE => (warning ("Failed to generate random elements for type" ^ tyco); thy))
b6a103ace4db continued
haftmann
parents: 26142
diff changeset
   315
    | add_random_inst tycos = tap (fn _ => warning
b6a103ace4db continued
haftmann
parents: 26142
diff changeset
   316
        ("Will not generated random elements for mutual recursive types " ^ commas (map quote tycos)));
b6a103ace4db continued
haftmann
parents: 26142
diff changeset
   317
in DatatypePackage.interpretation add_random_inst end
b6a103ace4db continued
haftmann
parents: 26142
diff changeset
   318
*}
26038
55a02586776d towards quickcheck
haftmann
parents: 24994
diff changeset
   319
55a02586776d towards quickcheck
haftmann
parents: 24994
diff changeset
   320
instantiation int :: random
55a02586776d towards quickcheck
haftmann
parents: 24994
diff changeset
   321
begin
55a02586776d towards quickcheck
haftmann
parents: 24994
diff changeset
   322
55a02586776d towards quickcheck
haftmann
parents: 24994
diff changeset
   323
definition
55a02586776d towards quickcheck
haftmann
parents: 24994
diff changeset
   324
  "random n = (do
55a02586776d towards quickcheck
haftmann
parents: 24994
diff changeset
   325
     (b, m) \<leftarrow> random n;
55a02586776d towards quickcheck
haftmann
parents: 24994
diff changeset
   326
     return (if b then int m else - int m)
55a02586776d towards quickcheck
haftmann
parents: 24994
diff changeset
   327
   done)"
55a02586776d towards quickcheck
haftmann
parents: 24994
diff changeset
   328
55a02586776d towards quickcheck
haftmann
parents: 24994
diff changeset
   329
instance ..
55a02586776d towards quickcheck
haftmann
parents: 24994
diff changeset
   330
55a02586776d towards quickcheck
haftmann
parents: 24994
diff changeset
   331
end
55a02586776d towards quickcheck
haftmann
parents: 24994
diff changeset
   332
55a02586776d towards quickcheck
haftmann
parents: 24994
diff changeset
   333
code_reserved SML Quickcheck
55a02586776d towards quickcheck
haftmann
parents: 24994
diff changeset
   334
55a02586776d towards quickcheck
haftmann
parents: 24994
diff changeset
   335
55a02586776d towards quickcheck
haftmann
parents: 24994
diff changeset
   336
subsection {* Quickcheck generator *}
55a02586776d towards quickcheck
haftmann
parents: 24994
diff changeset
   337
55a02586776d towards quickcheck
haftmann
parents: 24994
diff changeset
   338
ML {*
55a02586776d towards quickcheck
haftmann
parents: 24994
diff changeset
   339
structure Quickcheck =
55a02586776d towards quickcheck
haftmann
parents: 24994
diff changeset
   340
struct
55a02586776d towards quickcheck
haftmann
parents: 24994
diff changeset
   341
55a02586776d towards quickcheck
haftmann
parents: 24994
diff changeset
   342
open Quickcheck;
55a02586776d towards quickcheck
haftmann
parents: 24994
diff changeset
   343
55a02586776d towards quickcheck
haftmann
parents: 24994
diff changeset
   344
val eval_ref : (unit -> int -> int * int -> term list option * (int * int)) option ref = ref NONE;
55a02586776d towards quickcheck
haftmann
parents: 24994
diff changeset
   345
55a02586776d towards quickcheck
haftmann
parents: 24994
diff changeset
   346
fun mk_generator_expr prop tys =
55a02586776d towards quickcheck
haftmann
parents: 24994
diff changeset
   347
  let
55a02586776d towards quickcheck
haftmann
parents: 24994
diff changeset
   348
    val bounds = map_index (fn (i, ty) => (i, ty)) tys;
55a02586776d towards quickcheck
haftmann
parents: 24994
diff changeset
   349
    val result = list_comb (prop, map (fn (i, _) => Bound (length tys - i - 1)) bounds);
55a02586776d towards quickcheck
haftmann
parents: 24994
diff changeset
   350
    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
   351
    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
   352
      $ 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
   353
    val return = @{term "Pair \<Colon> term list option \<Rightarrow> seed \<Rightarrow> term list option \<times> seed"};
55a02586776d towards quickcheck
haftmann
parents: 24994
diff changeset
   354
    fun mk_bindtyp ty = @{typ seed} --> HOLogic.mk_prodT (ty, @{typ seed});
55a02586776d towards quickcheck
haftmann
parents: 24994
diff changeset
   355
    fun mk_bindclause (i, ty) t = Const (@{const_name mbind}, mk_bindtyp ty
55a02586776d towards quickcheck
haftmann
parents: 24994
diff changeset
   356
      --> (ty --> mk_bindtyp @{typ "term list option"}) --> mk_bindtyp @{typ "term list option"})
55a02586776d towards quickcheck
haftmann
parents: 24994
diff changeset
   357
      $ (Const (@{const_name random}, @{typ index} --> mk_bindtyp ty)
55a02586776d towards quickcheck
haftmann
parents: 24994
diff changeset
   358
        $ Bound i) $ Abs ("a", ty, t);
55a02586776d towards quickcheck
haftmann
parents: 24994
diff changeset
   359
    val t = fold_rev mk_bindclause bounds (return $ check);
55a02586776d towards quickcheck
haftmann
parents: 24994
diff changeset
   360
  in Abs ("n", @{typ index}, t) end;
55a02586776d towards quickcheck
haftmann
parents: 24994
diff changeset
   361
55a02586776d towards quickcheck
haftmann
parents: 24994
diff changeset
   362
fun compile_generator_expr thy prop tys =
55a02586776d towards quickcheck
haftmann
parents: 24994
diff changeset
   363
  let
55a02586776d towards quickcheck
haftmann
parents: 24994
diff changeset
   364
    val f = CodePackage.eval_term ("Quickcheck.eval_ref", eval_ref) thy
55a02586776d towards quickcheck
haftmann
parents: 24994
diff changeset
   365
      (mk_generator_expr prop tys) [];
55a02586776d towards quickcheck
haftmann
parents: 24994
diff changeset
   366
  in f #> run #> (Option.map o map) (Code.postprocess_term thy) end;
55a02586776d towards quickcheck
haftmann
parents: 24994
diff changeset
   367
26261
b6a103ace4db continued
haftmann
parents: 26142
diff changeset
   368
fun VALUE prop tys thy =
b6a103ace4db continued
haftmann
parents: 26142
diff changeset
   369
  let
b6a103ace4db continued
haftmann
parents: 26142
diff changeset
   370
    val t = mk_generator_expr prop tys;
b6a103ace4db continued
haftmann
parents: 26142
diff changeset
   371
    val eq = Logic.mk_equals (Free ("VALUE", fastype_of t), t)
b6a103ace4db continued
haftmann
parents: 26142
diff changeset
   372
  in
b6a103ace4db continued
haftmann
parents: 26142
diff changeset
   373
    thy
b6a103ace4db continued
haftmann
parents: 26142
diff changeset
   374
    |> TheoryTarget.init NONE
b6a103ace4db continued
haftmann
parents: 26142
diff changeset
   375
    |> Specification.definition (NONE, (("", []), eq))
b6a103ace4db continued
haftmann
parents: 26142
diff changeset
   376
    |> snd
b6a103ace4db continued
haftmann
parents: 26142
diff changeset
   377
    |> LocalTheory.exit
b6a103ace4db continued
haftmann
parents: 26142
diff changeset
   378
    |> ProofContext.theory_of
b6a103ace4db continued
haftmann
parents: 26142
diff changeset
   379
  end;
b6a103ace4db continued
haftmann
parents: 26142
diff changeset
   380
26038
55a02586776d towards quickcheck
haftmann
parents: 24994
diff changeset
   381
end
55a02586776d towards quickcheck
haftmann
parents: 24994
diff changeset
   382
*}
55a02586776d towards quickcheck
haftmann
parents: 24994
diff changeset
   383
55a02586776d towards quickcheck
haftmann
parents: 24994
diff changeset
   384
ML {* val f = Quickcheck.compile_generator_expr @{theory}
55a02586776d towards quickcheck
haftmann
parents: 24994
diff changeset
   385
  @{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
   386
55a02586776d towards quickcheck
haftmann
parents: 24994
diff changeset
   387
ML {* f 5 |> (Option.map o map) (Sign.string_of_term @{theory}) *}
55a02586776d towards quickcheck
haftmann
parents: 24994
diff changeset
   388
ML {* f 5 |> (Option.map o map) (Sign.string_of_term @{theory}) *}
55a02586776d towards quickcheck
haftmann
parents: 24994
diff changeset
   389
ML {* f 20 |> (Option.map o map) (Sign.string_of_term @{theory}) *}
55a02586776d towards quickcheck
haftmann
parents: 24994
diff changeset
   390
ML {* f 20 |> (Option.map o map) (Sign.string_of_term @{theory}) *}
55a02586776d towards quickcheck
haftmann
parents: 24994
diff changeset
   391
ML {* f 20 |> (Option.map o map) (Sign.string_of_term @{theory}) *}
55a02586776d towards quickcheck
haftmann
parents: 24994
diff changeset
   392
ML {* f 20 |> (Option.map o map) (Sign.string_of_term @{theory}) *}
55a02586776d towards quickcheck
haftmann
parents: 24994
diff changeset
   393
ML {* f 25 |> (Option.map o map) (Sign.string_of_term @{theory}) *}
55a02586776d towards quickcheck
haftmann
parents: 24994
diff changeset
   394
ML {* f 1 |> (Option.map o map) (Sign.string_of_term @{theory}) *}
55a02586776d towards quickcheck
haftmann
parents: 24994
diff changeset
   395
ML {* f 1 |> (Option.map o map) (Sign.string_of_term @{theory}) *}
55a02586776d towards quickcheck
haftmann
parents: 24994
diff changeset
   396
ML {* f 2 |> (Option.map o map) (Sign.string_of_term @{theory}) *}
55a02586776d towards quickcheck
haftmann
parents: 24994
diff changeset
   397
ML {* f 2 |> (Option.map o map) (Sign.string_of_term @{theory}) *}
55a02586776d towards quickcheck
haftmann
parents: 24994
diff changeset
   398
55a02586776d towards quickcheck
haftmann
parents: 24994
diff changeset
   399
ML {* val f = Quickcheck.compile_generator_expr @{theory}
55a02586776d towards quickcheck
haftmann
parents: 24994
diff changeset
   400
  @{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
   401
26261
b6a103ace4db continued
haftmann
parents: 26142
diff changeset
   402
(*setup {* Quickcheck.VALUE @{term "\<lambda>(n::int) (m::int) (q::int). n = m + q + 1"} [@{typ int}, @{typ int}, @{typ int}] *}
b6a103ace4db continued
haftmann
parents: 26142
diff changeset
   403
b6a103ace4db continued
haftmann
parents: 26142
diff changeset
   404
export_code VALUE in SML module_name QuickcheckExample file "~~/../../gen_code/quickcheck.ML"
b6a103ace4db continued
haftmann
parents: 26142
diff changeset
   405
b6a103ace4db continued
haftmann
parents: 26142
diff changeset
   406
definition "FOO = (True, Suc 0)"
b6a103ace4db continued
haftmann
parents: 26142
diff changeset
   407
b6a103ace4db continued
haftmann
parents: 26142
diff changeset
   408
code_module (test) QuickcheckExample
b6a103ace4db continued
haftmann
parents: 26142
diff changeset
   409
  file "~~/../../gen_code/quickcheck'.ML"
b6a103ace4db continued
haftmann
parents: 26142
diff changeset
   410
  contains FOO*)
b6a103ace4db continued
haftmann
parents: 26142
diff changeset
   411
26038
55a02586776d towards quickcheck
haftmann
parents: 24994
diff changeset
   412
ML {* f 5 |> (Option.map o map) (Sign.string_of_term @{theory}) *}
55a02586776d towards quickcheck
haftmann
parents: 24994
diff changeset
   413
ML {* f 5 |> (Option.map o map) (Sign.string_of_term @{theory}) *}
55a02586776d towards quickcheck
haftmann
parents: 24994
diff changeset
   414
ML {* f 20 |> (Option.map o map) (Sign.string_of_term @{theory}) *}
55a02586776d towards quickcheck
haftmann
parents: 24994
diff changeset
   415
ML {* f 20 |> (Option.map o map) (Sign.string_of_term @{theory}) *}
55a02586776d towards quickcheck
haftmann
parents: 24994
diff changeset
   416
ML {* f 20 |> (Option.map o map) (Sign.string_of_term @{theory}) *}
55a02586776d towards quickcheck
haftmann
parents: 24994
diff changeset
   417
ML {* f 20 |> (Option.map o map) (Sign.string_of_term @{theory}) *}
55a02586776d towards quickcheck
haftmann
parents: 24994
diff changeset
   418
ML {* f 25 |> (Option.map o map) (Sign.string_of_term @{theory}) *}
55a02586776d towards quickcheck
haftmann
parents: 24994
diff changeset
   419
ML {* f 1 |> (Option.map o map) (Sign.string_of_term @{theory}) *}
55a02586776d towards quickcheck
haftmann
parents: 24994
diff changeset
   420
ML {* f 1 |> (Option.map o map) (Sign.string_of_term @{theory}) *}
55a02586776d towards quickcheck
haftmann
parents: 24994
diff changeset
   421
ML {* f 2 |> (Option.map o map) (Sign.string_of_term @{theory}) *}
55a02586776d towards quickcheck
haftmann
parents: 24994
diff changeset
   422
ML {* f 2 |> (Option.map o map) (Sign.string_of_term @{theory}) *}
26261
b6a103ace4db continued
haftmann
parents: 26142
diff changeset
   423
ML {* f 3 |> (Option.map o map) (Sign.string_of_term @{theory}) *}
b6a103ace4db continued
haftmann
parents: 26142
diff changeset
   424
ML {* f 4 |> (Option.map o map) (Sign.string_of_term @{theory}) *}
b6a103ace4db continued
haftmann
parents: 26142
diff changeset
   425
ML {* f 4 |> (Option.map o map) (Sign.string_of_term @{theory}) *}
26038
55a02586776d towards quickcheck
haftmann
parents: 24994
diff changeset
   426
26142
3d5df9a56537 some steps towards automated generators
haftmann
parents: 26042
diff changeset
   427
ML {* val f = Quickcheck.compile_generator_expr @{theory}
26261
b6a103ace4db continued
haftmann
parents: 26142
diff changeset
   428
  @{term "\<lambda>(xs\<Colon>nat list) ys. rev (xs @ ys) = rev xs @ rev ys"}
b6a103ace4db continued
haftmann
parents: 26142
diff changeset
   429
  [@{typ "nat list"}, @{typ "nat list"}] *}
26142
3d5df9a56537 some steps towards automated generators
haftmann
parents: 26042
diff changeset
   430
3d5df9a56537 some steps towards automated generators
haftmann
parents: 26042
diff changeset
   431
ML {* f 15 |> (Option.map o map) (Sign.string_of_term @{theory}) *}
3d5df9a56537 some steps towards automated generators
haftmann
parents: 26042
diff changeset
   432
ML {* f 5 |> (Option.map o map) (Sign.string_of_term @{theory}) *}
3d5df9a56537 some steps towards automated generators
haftmann
parents: 26042
diff changeset
   433
ML {* f 20 |> (Option.map o map) (Sign.string_of_term @{theory}) *}
3d5df9a56537 some steps towards automated generators
haftmann
parents: 26042
diff changeset
   434
ML {* f 20 |> (Option.map o map) (Sign.string_of_term @{theory}) *}
3d5df9a56537 some steps towards automated generators
haftmann
parents: 26042
diff changeset
   435
ML {* f 20 |> (Option.map o map) (Sign.string_of_term @{theory}) *}
3d5df9a56537 some steps towards automated generators
haftmann
parents: 26042
diff changeset
   436
ML {* f 20 |> (Option.map o map) (Sign.string_of_term @{theory}) *}
3d5df9a56537 some steps towards automated generators
haftmann
parents: 26042
diff changeset
   437
ML {* f 25 |> (Option.map o map) (Sign.string_of_term @{theory}) *}
3d5df9a56537 some steps towards automated generators
haftmann
parents: 26042
diff changeset
   438
ML {* f 1 |> (Option.map o map) (Sign.string_of_term @{theory}) *}
3d5df9a56537 some steps towards automated generators
haftmann
parents: 26042
diff changeset
   439
ML {* f 1 |> (Option.map o map) (Sign.string_of_term @{theory}) *}
3d5df9a56537 some steps towards automated generators
haftmann
parents: 26042
diff changeset
   440
ML {* f 2 |> (Option.map o map) (Sign.string_of_term @{theory}) *}
3d5df9a56537 some steps towards automated generators
haftmann
parents: 26042
diff changeset
   441
ML {* f 2 |> (Option.map o map) (Sign.string_of_term @{theory}) *}
3d5df9a56537 some steps towards automated generators
haftmann
parents: 26042
diff changeset
   442
ML {* f 4 |> (Option.map o map) (Sign.string_of_term @{theory}) *}
3d5df9a56537 some steps towards automated generators
haftmann
parents: 26042
diff changeset
   443
ML {* f 4 |> (Option.map o map) (Sign.string_of_term @{theory}) *}
3d5df9a56537 some steps towards automated generators
haftmann
parents: 26042
diff changeset
   444
ML {* f 5 |> (Option.map o map) (Sign.string_of_term @{theory}) *}
3d5df9a56537 some steps towards automated generators
haftmann
parents: 26042
diff changeset
   445
ML {* f 8 |> (Option.map o map) (Sign.string_of_term @{theory}) *}
3d5df9a56537 some steps towards automated generators
haftmann
parents: 26042
diff changeset
   446
ML {* f 8 |> (Option.map o map) (Sign.string_of_term @{theory}) *}
3d5df9a56537 some steps towards automated generators
haftmann
parents: 26042
diff changeset
   447
ML {* f 8 |> (Option.map o map) (Sign.string_of_term @{theory}) *}
26261
b6a103ace4db continued
haftmann
parents: 26142
diff changeset
   448
ML {* f 88 |> (Option.map o map) (Sign.string_of_term @{theory}) *}
26038
55a02586776d towards quickcheck
haftmann
parents: 24994
diff changeset
   449
55a02586776d towards quickcheck
haftmann
parents: 24994
diff changeset
   450
subsection {* Incremental function generator *}
55a02586776d towards quickcheck
haftmann
parents: 24994
diff changeset
   451
55a02586776d towards quickcheck
haftmann
parents: 24994
diff changeset
   452
ML {*
55a02586776d towards quickcheck
haftmann
parents: 24994
diff changeset
   453
structure Quickcheck =
55a02586776d towards quickcheck
haftmann
parents: 24994
diff changeset
   454
struct
55a02586776d towards quickcheck
haftmann
parents: 24994
diff changeset
   455
55a02586776d towards quickcheck
haftmann
parents: 24994
diff changeset
   456
open Quickcheck;
55a02586776d towards quickcheck
haftmann
parents: 24994
diff changeset
   457
55a02586776d towards quickcheck
haftmann
parents: 24994
diff changeset
   458
fun random_fun (eq : 'a -> 'a -> bool)
55a02586776d towards quickcheck
haftmann
parents: 24994
diff changeset
   459
    (random : seed -> 'b * seed)
55a02586776d towards quickcheck
haftmann
parents: 24994
diff changeset
   460
    (random_split : seed -> seed * seed)
55a02586776d towards quickcheck
haftmann
parents: 24994
diff changeset
   461
    (seed : seed) =
55a02586776d towards quickcheck
haftmann
parents: 24994
diff changeset
   462
  let
55a02586776d towards quickcheck
haftmann
parents: 24994
diff changeset
   463
    val (seed', seed'') = random_split seed;
55a02586776d towards quickcheck
haftmann
parents: 24994
diff changeset
   464
    val state = ref (seed', []);
55a02586776d towards quickcheck
haftmann
parents: 24994
diff changeset
   465
    fun random_fun' x =
55a02586776d towards quickcheck
haftmann
parents: 24994
diff changeset
   466
      let
55a02586776d towards quickcheck
haftmann
parents: 24994
diff changeset
   467
        val (seed, fun_map) = ! state;
55a02586776d towards quickcheck
haftmann
parents: 24994
diff changeset
   468
      in case AList.lookup (uncurry eq) fun_map x
55a02586776d towards quickcheck
haftmann
parents: 24994
diff changeset
   469
       of SOME y => y
55a02586776d towards quickcheck
haftmann
parents: 24994
diff changeset
   470
        | NONE => let
55a02586776d towards quickcheck
haftmann
parents: 24994
diff changeset
   471
              val (y, seed') = random seed;
55a02586776d towards quickcheck
haftmann
parents: 24994
diff changeset
   472
              val _ = state := (seed', (x, y) :: fun_map);
55a02586776d towards quickcheck
haftmann
parents: 24994
diff changeset
   473
            in y end
55a02586776d towards quickcheck
haftmann
parents: 24994
diff changeset
   474
      end;
55a02586776d towards quickcheck
haftmann
parents: 24994
diff changeset
   475
  in (random_fun', seed'') end;
55a02586776d towards quickcheck
haftmann
parents: 24994
diff changeset
   476
55a02586776d towards quickcheck
haftmann
parents: 24994
diff changeset
   477
end
55a02586776d towards quickcheck
haftmann
parents: 24994
diff changeset
   478
*}
55a02586776d towards quickcheck
haftmann
parents: 24994
diff changeset
   479
55a02586776d towards quickcheck
haftmann
parents: 24994
diff changeset
   480
axiomatization
55a02586776d towards quickcheck
haftmann
parents: 24994
diff changeset
   481
  random_fun_aux :: "('a \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> (seed \<Rightarrow> 'b \<times> seed)
55a02586776d towards quickcheck
haftmann
parents: 24994
diff changeset
   482
    \<Rightarrow> (seed \<Rightarrow> seed \<times> seed) \<Rightarrow> seed \<Rightarrow> ('a \<Rightarrow> 'b) \<times> seed"
55a02586776d towards quickcheck
haftmann
parents: 24994
diff changeset
   483
55a02586776d towards quickcheck
haftmann
parents: 24994
diff changeset
   484
code_const random_fun_aux (SML "Quickcheck.random'_fun")
55a02586776d towards quickcheck
haftmann
parents: 24994
diff changeset
   485
55a02586776d towards quickcheck
haftmann
parents: 24994
diff changeset
   486
instantiation "fun" :: (term_of, term_of) term_of
55a02586776d towards quickcheck
haftmann
parents: 24994
diff changeset
   487
begin
55a02586776d towards quickcheck
haftmann
parents: 24994
diff changeset
   488
55a02586776d towards quickcheck
haftmann
parents: 24994
diff changeset
   489
instance ..
55a02586776d towards quickcheck
haftmann
parents: 24994
diff changeset
   490
55a02586776d towards quickcheck
haftmann
parents: 24994
diff changeset
   491
end
55a02586776d towards quickcheck
haftmann
parents: 24994
diff changeset
   492
55a02586776d towards quickcheck
haftmann
parents: 24994
diff changeset
   493
code_const "Eval.term_of :: ('a\<Colon>term_of \<Rightarrow> 'b\<Colon>term_of) \<Rightarrow> _"
55a02586776d towards quickcheck
haftmann
parents: 24994
diff changeset
   494
  (SML "(fn '_ => Const (\"arbitrary\", dummyT))")
55a02586776d towards quickcheck
haftmann
parents: 24994
diff changeset
   495
26042
e7a421d1f5c1 continued
haftmann
parents: 26038
diff changeset
   496
instantiation "fun" :: (eq, "{type, random}") random
26038
55a02586776d towards quickcheck
haftmann
parents: 24994
diff changeset
   497
begin
55a02586776d towards quickcheck
haftmann
parents: 24994
diff changeset
   498
55a02586776d towards quickcheck
haftmann
parents: 24994
diff changeset
   499
definition
55a02586776d towards quickcheck
haftmann
parents: 24994
diff changeset
   500
  "random n = random_fun_aux (op =) (random n) split_seed"
55a02586776d towards quickcheck
haftmann
parents: 24994
diff changeset
   501
55a02586776d towards quickcheck
haftmann
parents: 24994
diff changeset
   502
instance ..
55a02586776d towards quickcheck
haftmann
parents: 24994
diff changeset
   503
55a02586776d towards quickcheck
haftmann
parents: 24994
diff changeset
   504
end
55a02586776d towards quickcheck
haftmann
parents: 24994
diff changeset
   505
55a02586776d towards quickcheck
haftmann
parents: 24994
diff changeset
   506
ML {* val f = Quickcheck.compile_generator_expr @{theory}
55a02586776d towards quickcheck
haftmann
parents: 24994
diff changeset
   507
  @{term "\<lambda>f k. int (f k) = k"} [@{typ "int \<Rightarrow> nat"}, @{typ int}] *}
55a02586776d towards quickcheck
haftmann
parents: 24994
diff changeset
   508
55a02586776d towards quickcheck
haftmann
parents: 24994
diff changeset
   509
ML {* f 20 |> (Option.map o map) (Sign.string_of_term @{theory}) *}
55a02586776d towards quickcheck
haftmann
parents: 24994
diff changeset
   510
ML {* f 20 |> (Option.map o map) (Sign.string_of_term @{theory}) *}
55a02586776d towards quickcheck
haftmann
parents: 24994
diff changeset
   511
ML {* f 20 |> (Option.map o map) (Sign.string_of_term @{theory}) *}
55a02586776d towards quickcheck
haftmann
parents: 24994
diff changeset
   512
ML {* f 20 |> (Option.map o map) (Sign.string_of_term @{theory}) *}
55a02586776d towards quickcheck
haftmann
parents: 24994
diff changeset
   513
ML {* f 20 |> (Option.map o map) (Sign.string_of_term @{theory}) *}
55a02586776d towards quickcheck
haftmann
parents: 24994
diff changeset
   514
ML {* f 20 |> (Option.map o map) (Sign.string_of_term @{theory}) *}
55a02586776d towards quickcheck
haftmann
parents: 24994
diff changeset
   515
55a02586776d towards quickcheck
haftmann
parents: 24994
diff changeset
   516
end