src/HOL/Random_Sequence.thy
changeset 51126 df86080de4cb
parent 50055 94041d602ecb
child 51143 0a2371e7ced3
     1.1 --- a/src/HOL/Random_Sequence.thy	Thu Feb 14 17:58:28 2013 +0100
     1.2 +++ b/src/HOL/Random_Sequence.thy	Thu Feb 14 15:27:10 2013 +0100
     1.3 @@ -1,32 +1,34 @@
     1.4  
     1.5  (* Author: Lukas Bulwahn, TU Muenchen *)
     1.6  
     1.7 +header {* Various kind of sequences inside the random monad *}
     1.8 +
     1.9  theory Random_Sequence
    1.10 -imports Quickcheck
    1.11 +imports Random_Pred
    1.12  begin
    1.13  
    1.14 -type_synonym 'a random_dseq = "code_numeral \<Rightarrow> code_numeral \<Rightarrow> Random.seed \<Rightarrow> ('a DSequence.dseq \<times> Random.seed)"
    1.15 +type_synonym 'a random_dseq = "code_numeral \<Rightarrow> code_numeral \<Rightarrow> Random.seed \<Rightarrow> ('a Limited_Sequence.dseq \<times> Random.seed)"
    1.16  
    1.17  definition empty :: "'a random_dseq"
    1.18  where
    1.19 -  "empty = (%nrandom size. Pair (DSequence.empty))"
    1.20 +  "empty = (%nrandom size. Pair (Limited_Sequence.empty))"
    1.21  
    1.22  definition single :: "'a => 'a random_dseq"
    1.23  where
    1.24 -  "single x = (%nrandom size. Pair (DSequence.single x))"
    1.25 +  "single x = (%nrandom size. Pair (Limited_Sequence.single x))"
    1.26  
    1.27  definition bind :: "'a random_dseq => ('a \<Rightarrow> 'b random_dseq) \<Rightarrow> 'b random_dseq"
    1.28  where
    1.29    "bind R f = (\<lambda>nrandom size s. let
    1.30       (P, s') = R nrandom size s;
    1.31       (s1, s2) = Random.split_seed s'
    1.32 -  in (DSequence.bind P (%a. fst (f a nrandom size s1)), s2))"
    1.33 +  in (Limited_Sequence.bind P (%a. fst (f a nrandom size s1)), s2))"
    1.34  
    1.35  definition union :: "'a random_dseq => 'a random_dseq => 'a random_dseq"
    1.36  where
    1.37    "union R1 R2 = (\<lambda>nrandom size s. let
    1.38       (S1, s') = R1 nrandom size s; (S2, s'') = R2 nrandom size s'
    1.39 -  in (DSequence.union S1 S2, s''))"
    1.40 +  in (Limited_Sequence.union S1 S2, s''))"
    1.41  
    1.42  definition if_random_dseq :: "bool => unit random_dseq"
    1.43  where
    1.44 @@ -36,26 +38,120 @@
    1.45  where
    1.46    "not_random_dseq R = (\<lambda>nrandom size s. let
    1.47       (S, s') = R nrandom size s
    1.48 -   in (DSequence.not_seq S, s'))"
    1.49 -
    1.50 -fun Random :: "(code_numeral \<Rightarrow> Random.seed \<Rightarrow> (('a \<times> (unit \<Rightarrow> term)) \<times> Random.seed)) \<Rightarrow> 'a random_dseq"
    1.51 -where
    1.52 -  "Random g nrandom = (%size. if nrandom <= 0 then (Pair DSequence.empty) else
    1.53 -     (scomp (g size) (%r. scomp (Random g (nrandom - 1) size) (%rs. Pair (DSequence.union (DSequence.single (fst r)) rs)))))"
    1.54 +   in (Limited_Sequence.not_seq S, s'))"
    1.55  
    1.56  definition map :: "('a => 'b) => 'a random_dseq => 'b random_dseq"
    1.57  where
    1.58    "map f P = bind P (single o f)"
    1.59  
    1.60 -(*
    1.61 -hide_const DSequence.empty DSequence.single DSequence.eval
    1.62 -  DSequence.map_seq DSequence.bind DSequence.union DSequence.if_seq DSequence.not_seq
    1.63 -  DSequence.map
    1.64 -*)
    1.65 +fun Random :: "(code_numeral \<Rightarrow> Random.seed \<Rightarrow> (('a \<times> (unit \<Rightarrow> term)) \<times> Random.seed)) \<Rightarrow> 'a random_dseq"
    1.66 +where
    1.67 +  "Random g nrandom = (%size. if nrandom <= 0 then (Pair Limited_Sequence.empty) else
    1.68 +     (scomp (g size) (%r. scomp (Random g (nrandom - 1) size) (%rs. Pair (Limited_Sequence.union (Limited_Sequence.single (fst r)) rs)))))"
    1.69 +
    1.70 +
    1.71 +type_synonym 'a pos_random_dseq = "code_numeral \<Rightarrow> code_numeral \<Rightarrow> Random.seed \<Rightarrow> 'a Limited_Sequence.pos_dseq"
    1.72 +
    1.73 +definition pos_empty :: "'a pos_random_dseq"
    1.74 +where
    1.75 +  "pos_empty = (%nrandom size seed. Limited_Sequence.pos_empty)"
    1.76 +
    1.77 +definition pos_single :: "'a => 'a pos_random_dseq"
    1.78 +where
    1.79 +  "pos_single x = (%nrandom size seed. Limited_Sequence.pos_single x)"
    1.80 +
    1.81 +definition pos_bind :: "'a pos_random_dseq => ('a \<Rightarrow> 'b pos_random_dseq) \<Rightarrow> 'b pos_random_dseq"
    1.82 +where
    1.83 +  "pos_bind R f = (\<lambda>nrandom size seed. Limited_Sequence.pos_bind (R nrandom size seed) (%a. f a nrandom size seed))"
    1.84 +
    1.85 +definition pos_decr_bind :: "'a pos_random_dseq => ('a \<Rightarrow> 'b pos_random_dseq) \<Rightarrow> 'b pos_random_dseq"
    1.86 +where
    1.87 +  "pos_decr_bind R f = (\<lambda>nrandom size seed. Limited_Sequence.pos_decr_bind (R nrandom size seed) (%a. f a nrandom size seed))"
    1.88 +
    1.89 +definition pos_union :: "'a pos_random_dseq => 'a pos_random_dseq => 'a pos_random_dseq"
    1.90 +where
    1.91 +  "pos_union R1 R2 = (\<lambda>nrandom size seed. Limited_Sequence.pos_union (R1 nrandom size seed) (R2 nrandom size seed))"
    1.92 +
    1.93 +definition pos_if_random_dseq :: "bool => unit pos_random_dseq"
    1.94 +where
    1.95 +  "pos_if_random_dseq b = (if b then pos_single () else pos_empty)"
    1.96 +
    1.97 +definition pos_iterate_upto :: "(code_numeral => 'a) => code_numeral => code_numeral => 'a pos_random_dseq"
    1.98 +where
    1.99 +  "pos_iterate_upto f n m = (\<lambda>nrandom size seed. Limited_Sequence.pos_iterate_upto f n m)"
   1.100 +
   1.101 +definition pos_map :: "('a => 'b) => 'a pos_random_dseq => 'b pos_random_dseq"
   1.102 +where
   1.103 +  "pos_map f P = pos_bind P (pos_single o f)"
   1.104 +
   1.105 +fun iter :: "(Random.seed \<Rightarrow> ('a \<times> (unit \<Rightarrow> term)) \<times> Random.seed)
   1.106 +  \<Rightarrow> code_numeral \<Rightarrow> Random.seed \<Rightarrow> 'a Lazy_Sequence.lazy_sequence"
   1.107 +where
   1.108 +  "iter random nrandom seed =
   1.109 +    (if nrandom = 0 then Lazy_Sequence.empty else Lazy_Sequence.Lazy_Sequence (%u. let ((x, _), seed') = random seed in Some (x, iter random (nrandom - 1) seed')))"
   1.110 +
   1.111 +definition pos_Random :: "(code_numeral \<Rightarrow> Random.seed \<Rightarrow> ('a \<times> (unit \<Rightarrow> term)) \<times> Random.seed)
   1.112 +  \<Rightarrow> 'a pos_random_dseq"
   1.113 +where
   1.114 +  "pos_Random g = (%nrandom size seed depth. iter (g size) nrandom seed)"
   1.115 +
   1.116 +
   1.117 +type_synonym 'a neg_random_dseq = "code_numeral \<Rightarrow> code_numeral \<Rightarrow> Random.seed \<Rightarrow> 'a Limited_Sequence.neg_dseq"
   1.118  
   1.119 -hide_const (open) empty single bind union if_random_dseq not_random_dseq Random map
   1.120 +definition neg_empty :: "'a neg_random_dseq"
   1.121 +where
   1.122 +  "neg_empty = (%nrandom size seed. Limited_Sequence.neg_empty)"
   1.123 +
   1.124 +definition neg_single :: "'a => 'a neg_random_dseq"
   1.125 +where
   1.126 +  "neg_single x = (%nrandom size seed. Limited_Sequence.neg_single x)"
   1.127 +
   1.128 +definition neg_bind :: "'a neg_random_dseq => ('a \<Rightarrow> 'b neg_random_dseq) \<Rightarrow> 'b neg_random_dseq"
   1.129 +where
   1.130 +  "neg_bind R f = (\<lambda>nrandom size seed. Limited_Sequence.neg_bind (R nrandom size seed) (%a. f a nrandom size seed))"
   1.131 +
   1.132 +definition neg_decr_bind :: "'a neg_random_dseq => ('a \<Rightarrow> 'b neg_random_dseq) \<Rightarrow> 'b neg_random_dseq"
   1.133 +where
   1.134 +  "neg_decr_bind R f = (\<lambda>nrandom size seed. Limited_Sequence.neg_decr_bind (R nrandom size seed) (%a. f a nrandom size seed))"
   1.135 +
   1.136 +definition neg_union :: "'a neg_random_dseq => 'a neg_random_dseq => 'a neg_random_dseq"
   1.137 +where
   1.138 +  "neg_union R1 R2 = (\<lambda>nrandom size seed. Limited_Sequence.neg_union (R1 nrandom size seed) (R2 nrandom size seed))"
   1.139 +
   1.140 +definition neg_if_random_dseq :: "bool => unit neg_random_dseq"
   1.141 +where
   1.142 +  "neg_if_random_dseq b = (if b then neg_single () else neg_empty)"
   1.143 +
   1.144 +definition neg_iterate_upto :: "(code_numeral => 'a) => code_numeral => code_numeral => 'a neg_random_dseq"
   1.145 +where
   1.146 +  "neg_iterate_upto f n m = (\<lambda>nrandom size seed. Limited_Sequence.neg_iterate_upto f n m)"
   1.147  
   1.148 -hide_type DSequence.dseq random_dseq
   1.149 -hide_fact (open) empty_def single_def bind_def union_def if_random_dseq_def not_random_dseq_def Random.simps map_def
   1.150 +definition neg_not_random_dseq :: "unit pos_random_dseq => unit neg_random_dseq"
   1.151 +where
   1.152 +  "neg_not_random_dseq R = (\<lambda>nrandom size seed. Limited_Sequence.neg_not_seq (R nrandom size seed))"
   1.153 +
   1.154 +definition neg_map :: "('a => 'b) => 'a neg_random_dseq => 'b neg_random_dseq"
   1.155 +where
   1.156 +  "neg_map f P = neg_bind P (neg_single o f)"
   1.157 +
   1.158 +definition pos_not_random_dseq :: "unit neg_random_dseq => unit pos_random_dseq"
   1.159 +where
   1.160 +  "pos_not_random_dseq R = (\<lambda>nrandom size seed. Limited_Sequence.pos_not_seq (R nrandom size seed))"
   1.161 +
   1.162  
   1.163 -end
   1.164 \ No newline at end of file
   1.165 +hide_const (open)
   1.166 +  empty single bind union if_random_dseq not_random_dseq map Random
   1.167 +  pos_empty pos_single pos_bind pos_decr_bind pos_union pos_if_random_dseq pos_iterate_upto
   1.168 +  pos_not_random_dseq pos_map iter pos_Random
   1.169 +  neg_empty neg_single neg_bind neg_decr_bind neg_union neg_if_random_dseq neg_iterate_upto
   1.170 +  neg_not_random_dseq neg_map
   1.171 +
   1.172 +hide_fact (open) empty_def single_def bind_def union_def if_random_dseq_def not_random_dseq_def
   1.173 +  map_def Random.simps
   1.174 +  pos_empty_def pos_single_def pos_bind_def pos_decr_bind_def pos_union_def pos_if_random_dseq_def
   1.175 +  pos_iterate_upto_def pos_not_random_dseq_def pos_map_def iter.simps pos_Random_def
   1.176 +  neg_empty_def neg_single_def neg_bind_def neg_decr_bind_def neg_union_def neg_if_random_dseq_def
   1.177 +  neg_iterate_upto_def neg_not_random_dseq_def neg_map_def
   1.178 +
   1.179 +end
   1.180 +