1.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.2 +++ b/src/HOL/Random_Sequence.thy	Wed Jan 20 11:56:45 2010 +0100
     1.3 @@ -0,0 +1,61 @@
     1.4 +
     1.5 +(* Author: Lukas Bulwahn, TU Muenchen *)
     1.6 +
     1.7 +theory Random_Sequence
     1.8 +imports Quickcheck DSequence
     1.9 +begin
    1.10 +
    1.11 +types 'a random_dseq = "code_numeral \<Rightarrow> code_numeral \<Rightarrow> Random.seed \<Rightarrow> ('a DSequence.dseq \<times> Random.seed)"
    1.12 +
    1.13 +definition empty :: "'a random_dseq"
    1.14 +where
    1.15 +  "empty = (%nrandom size. Pair (DSequence.empty))"
    1.16 +
    1.17 +definition single :: "'a => 'a random_dseq"
    1.18 +where
    1.19 +  "single x = (%nrandom size. Pair (DSequence.single x))"
    1.20 +
    1.21 +definition bind :: "'a random_dseq => ('a \<Rightarrow> 'b random_dseq) \<Rightarrow> 'b random_dseq"
    1.22 +where
    1.23 +  "bind R f = (\<lambda>nrandom size s. let
    1.24 +     (P, s') = R nrandom size s;
    1.25 +     (s1, s2) = Random.split_seed s'
    1.26 +  in (DSequence.bind P (%a. fst (f a nrandom size s1)), s2))"
    1.27 +
    1.28 +definition union :: "'a random_dseq => 'a random_dseq => 'a random_dseq"
    1.29 +where
    1.30 +  "union R1 R2 = (\<lambda>nrandom size s. let
    1.31 +     (S1, s') = R1 nrandom size s; (S2, s'') = R2 nrandom size s'
    1.32 +  in (DSequence.union S1 S2, s''))"
    1.33 +
    1.34 +definition if_random_dseq :: "bool => unit random_dseq"
    1.35 +where
    1.36 +  "if_random_dseq b = (if b then single () else empty)"
    1.37 +
    1.38 +definition not_random_dseq :: "unit random_dseq => unit random_dseq"
    1.39 +where
    1.40 +  "not_random_dseq R = (\<lambda>nrandom size s. let
    1.41 +     (S, s') = R nrandom size s
    1.42 +   in (DSequence.not_seq S, s'))"
    1.43 +
    1.44 +fun Random :: "(code_numeral \<Rightarrow> Random.seed \<Rightarrow> (('a \<times> (unit \<Rightarrow> term)) \<times> Random.seed)) \<Rightarrow> 'a random_dseq"
    1.45 +where
    1.46 +  "Random g nrandom = (%size. if nrandom <= 0 then (Pair DSequence.empty) else
    1.47 +     (scomp (g size) (%r. scomp (Random g (nrandom - 1) size) (%rs. Pair (DSequence.union (DSequence.single (fst r)) rs)))))"
    1.48 +
    1.49 +definition map :: "('a => 'b) => 'a random_dseq => 'b random_dseq"
    1.50 +where
    1.51 +  "map f P = bind P (single o f)"
    1.52 +
    1.53 +(*
    1.54 +hide const DSequence.empty DSequence.single DSequence.eval
    1.55 +  DSequence.map_seq DSequence.bind DSequence.union DSequence.if_seq DSequence.not_seq
    1.56 +  DSequence.map
    1.57 +*)
    1.58 +
    1.59 +hide (open) const empty single bind union if_random_dseq not_random_dseq Random map
    1.60 +
    1.61 +hide type DSequence.dseq random_dseq
    1.62 +hide (open) fact empty_def single_def bind_def union_def if_random_dseq_def not_random_dseq_def Random_def map_def
    1.63 +
    1.64 +end
    1.65 \ No newline at end of file