src/HOL/ex/CodeRandom.thy
author haftmann
Wed Dec 27 19:10:03 2006 +0100 (2006-12-27 ago)
changeset 21912 ff45788e7bf9
parent 21876 96a601bc59d8
permissions -rw-r--r--
dropped section header
haftmann@20400
     1
(*  ID:         $Id$
haftmann@20400
     2
    Author:     Florian Haftmann, TU Muenchen
haftmann@20400
     3
*)
haftmann@20400
     4
haftmann@20400
     5
header {* A simple random engine *}
haftmann@20400
     6
haftmann@20400
     7
theory CodeRandom
haftmann@21192
     8
imports State_Monad
haftmann@20400
     9
begin
haftmann@20400
    10
haftmann@20400
    11
consts
haftmann@20400
    12
  pick :: "(nat \<times> 'a) list \<Rightarrow> nat \<Rightarrow> 'a"
haftmann@20400
    13
haftmann@20400
    14
primrec
haftmann@20400
    15
  "pick (x#xs) n = (let (k, v) = x in
haftmann@20400
    16
    if n < k then v else pick xs (n - k))"
haftmann@20400
    17
haftmann@20400
    18
lemma pick_def [code, simp]:
haftmann@20400
    19
  "pick ((k, v)#xs) n = (if n < k then v else pick xs (n - k))" by simp
haftmann@20400
    20
declare pick.simps [simp del, code del]
haftmann@20400
    21
haftmann@20400
    22
typedecl randseed
haftmann@20400
    23
haftmann@21113
    24
axiomatization
haftmann@20400
    25
  random_shift :: "randseed \<Rightarrow> randseed"
haftmann@21113
    26
haftmann@21113
    27
axiomatization
haftmann@20400
    28
  random_seed :: "randseed \<Rightarrow> nat"
haftmann@20400
    29
haftmann@20400
    30
definition
wenzelm@21404
    31
  random :: "nat \<Rightarrow> randseed \<Rightarrow> nat \<times> randseed" where
haftmann@20400
    32
  "random n s = (random_seed s mod n, random_shift s)"
haftmann@20400
    33
haftmann@20400
    34
lemma random_bound:
haftmann@20400
    35
  assumes "0 < n"
haftmann@20400
    36
  shows "fst (random n s) < n"
haftmann@20400
    37
proof -
haftmann@20400
    38
  from prems mod_less_divisor have "!!m .m mod n < n" by auto
haftmann@20400
    39
  then show ?thesis unfolding random_def by simp 
haftmann@20400
    40
qed
haftmann@20400
    41
haftmann@20400
    42
lemma random_random_seed [simp]:
haftmann@20400
    43
  "snd (random n s) = random_shift s" unfolding random_def by simp
haftmann@20400
    44
haftmann@20400
    45
definition
wenzelm@21404
    46
  select :: "'a list \<Rightarrow> randseed \<Rightarrow> 'a \<times> randseed" where
haftmann@21192
    47
  [simp]: "select xs = (do
haftmann@21192
    48
      n \<leftarrow> random (length xs);
haftmann@21192
    49
      return (nth xs n)
haftmann@21192
    50
    done)"
wenzelm@21404
    51
definition
wenzelm@21404
    52
  select_weight :: "(nat \<times> 'a) list \<Rightarrow> randseed \<Rightarrow> 'a \<times> randseed" where
haftmann@21192
    53
  [simp]: "select_weight xs = (do
haftmann@21192
    54
      n \<leftarrow> random (foldl (op +) 0 (map fst xs));
haftmann@21192
    55
      return (pick xs n)
haftmann@21192
    56
    done)"
haftmann@20400
    57
haftmann@20400
    58
lemma
haftmann@20400
    59
  "select (x#xs) s = select_weight (map (Pair 1) (x#xs)) s"
haftmann@20400
    60
proof (induct xs)
haftmann@21192
    61
  case Nil show ?case by (simp add: monad_collapse random_def)
haftmann@20400
    62
next
haftmann@20400
    63
  have map_fst_Pair: "!!xs y. map fst (map (Pair y) xs) = replicate (length xs) y"
haftmann@20400
    64
  proof -
haftmann@20400
    65
    fix xs
haftmann@20400
    66
    fix y
haftmann@20400
    67
    show "map fst (map (Pair y) xs) = replicate (length xs) y"
haftmann@20400
    68
      by (induct xs) simp_all
haftmann@20400
    69
  qed
haftmann@20400
    70
  have pick_nth: "!!xs n. n < length xs \<Longrightarrow> pick (map (Pair 1) xs) n = nth xs n"
haftmann@20400
    71
  proof -
haftmann@20400
    72
    fix xs
haftmann@20400
    73
    fix n
haftmann@20400
    74
    assume "n < length xs"
haftmann@20400
    75
    then show "pick (map (Pair 1) xs) n = nth xs n"
wenzelm@20503
    76
    proof (induct xs arbitrary: n)
haftmann@20400
    77
      case Nil then show ?case by simp
haftmann@20400
    78
    next
haftmann@20400
    79
      case (Cons x xs) show ?case
haftmann@20400
    80
      proof (cases n)
haftmann@20400
    81
        case 0 then show ?thesis by simp
haftmann@20400
    82
      next
haftmann@20400
    83
        case (Suc _)
haftmann@20400
    84
    from Cons have "n < length (x # xs)" by auto
haftmann@20400
    85
        then have "n < Suc (length xs)" by simp
haftmann@20400
    86
        with Suc have "n - 1 < Suc (length xs) - 1" by auto
haftmann@20400
    87
        with Cons have "pick (map (Pair (1\<Colon>nat)) xs) (n - 1) = xs ! (n - 1)" by auto
haftmann@20400
    88
        with Suc show ?thesis by auto
haftmann@20400
    89
      qed
haftmann@20400
    90
    qed
haftmann@20400
    91
  qed
haftmann@20400
    92
  have sum_length: "!!xs. foldl (op +) 0 (map fst (map (Pair 1) xs)) = length xs"
haftmann@20400
    93
  proof -
haftmann@20400
    94
    have replicate_append:
haftmann@20400
    95
      "!!x xs y. replicate (length (x # xs)) y = replicate (length xs) y @ [y]"
haftmann@20400
    96
      by (simp add: replicate_app_Cons_same)
haftmann@20400
    97
    fix xs
haftmann@20400
    98
    show "foldl (op +) 0 (map fst (map (Pair 1) xs)) = length xs"
haftmann@20400
    99
    unfolding map_fst_Pair proof (induct xs)
haftmann@20400
   100
      case Nil show ?case by simp
haftmann@20400
   101
    next
haftmann@20400
   102
      case (Cons x xs) then show ?case unfolding replicate_append by simp
haftmann@20400
   103
    qed
haftmann@20400
   104
  qed
haftmann@20400
   105
  have pick_nth_random:
haftmann@20400
   106
    "!!x xs s. pick (map (Pair 1) (x#xs)) (fst (random (length (x#xs)) s)) = nth (x#xs) (fst (random (length (x#xs)) s))"
haftmann@20400
   107
  proof -
haftmann@20400
   108
    fix s
haftmann@20400
   109
    fix x
haftmann@20400
   110
    fix xs
haftmann@20400
   111
    have bound: "fst (random (length (x#xs)) s) < length (x#xs)" by (rule random_bound) simp
haftmann@20400
   112
    from pick_nth [OF bound] show
haftmann@20400
   113
      "pick (map (Pair 1) (x#xs)) (fst (random (length (x#xs)) s)) = nth (x#xs) (fst (random (length (x#xs)) s))" .
haftmann@20400
   114
  qed
haftmann@21192
   115
  have pick_nth_random_do:
haftmann@21192
   116
    "!!x xs s. (do n \<leftarrow> random (length (x#xs)); return (pick (map (Pair 1) (x#xs)) n) done) s =
haftmann@21192
   117
      (do n \<leftarrow> random (length (x#xs)); return (nth (x#xs) n) done) s"
haftmann@21192
   118
  unfolding monad_collapse split_def unfolding pick_nth_random ..
haftmann@20400
   119
  case (Cons x xs) then show ?case
haftmann@21192
   120
    unfolding select_weight_def sum_length pick_nth_random_do
haftmann@21192
   121
    by simp
haftmann@20400
   122
qed
haftmann@20400
   123
haftmann@20400
   124
definition
wenzelm@21404
   125
  random_int :: "int \<Rightarrow> randseed \<Rightarrow> int * randseed" where
haftmann@21192
   126
  "random_int k = (do n \<leftarrow> random (nat k); return (int n) done)"
haftmann@20400
   127
haftmann@20400
   128
lemma random_nat [code]:
haftmann@21192
   129
  "random n = (do k \<leftarrow> random_int (int n); return (nat k) done)"
haftmann@21192
   130
unfolding random_int_def by simp
haftmann@20400
   131
haftmann@21113
   132
axiomatization
haftmann@21113
   133
  run_random :: "(randseed \<Rightarrow> 'a * randseed) \<Rightarrow> 'a"
haftmann@21113
   134
haftmann@20400
   135
ML {*
haftmann@20400
   136
signature RANDOM =
haftmann@20400
   137
sig
haftmann@20400
   138
  type seed = IntInf.int;
haftmann@20400
   139
  val seed: unit -> seed;
haftmann@20400
   140
  val value: IntInf.int -> seed -> IntInf.int * seed;
haftmann@20400
   141
end;
haftmann@20400
   142
haftmann@20400
   143
structure Random : RANDOM =
haftmann@20400
   144
struct
haftmann@20400
   145
haftmann@20406
   146
open IntInf;
haftmann@20406
   147
haftmann@20400
   148
exception RANDOM;
haftmann@20400
   149
haftmann@20406
   150
type seed = int;
haftmann@20400
   151
haftmann@20400
   152
local
haftmann@20406
   153
  val a = fromInt 16807;
haftmann@20406
   154
    (*greetings to SML/NJ*)
haftmann@20406
   155
  val m = (the o fromString) "2147483647";
haftmann@20400
   156
in
haftmann@20406
   157
  fun next s = (a * s) mod m;
haftmann@20400
   158
end;
haftmann@20400
   159
haftmann@20400
   160
local
haftmann@20406
   161
  val seed_ref = ref (fromInt 1);
haftmann@20400
   162
in
haftmann@20400
   163
  fun seed () =
haftmann@20400
   164
    let
haftmann@20400
   165
      val r = next (!seed_ref)
haftmann@20400
   166
    in
haftmann@20400
   167
      (seed_ref := r; r)
haftmann@20400
   168
    end;
haftmann@20400
   169
end;
haftmann@20400
   170
haftmann@20400
   171
fun value h s =
haftmann@20400
   172
  if h < 1 then raise RANDOM
haftmann@20406
   173
  else (s mod (h - 1), seed ());
haftmann@20400
   174
haftmann@20400
   175
end;
haftmann@20400
   176
*}
haftmann@20400
   177
haftmann@20453
   178
code_type randseed
haftmann@21113
   179
  (SML "Random.seed")
haftmann@20400
   180
haftmann@20453
   181
code_const random_int
haftmann@21113
   182
  (SML "Random.value")
haftmann@21113
   183
haftmann@21113
   184
code_const run_random
haftmann@21113
   185
  (SML "case _ (Random.seed ()) of (x, '_) => x")
haftmann@20400
   186
haftmann@20453
   187
code_gen select select_weight
haftmann@21545
   188
  (SML #)
haftmann@20400
   189
haftmann@20400
   190
end