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