1 2(* Author: Lukas Bulwahn, TU Muenchen *) 3 4section \<open>Various kind of sequences inside the random monad\<close> 5 6theory Random_Sequence 7imports Random_Pred 8begin 9 10type_synonym 'a random_dseq = "natural \<Rightarrow> natural \<Rightarrow> Random.seed \<Rightarrow> ('a Limited_Sequence.dseq \<times> Random.seed)" 11 12definition empty :: "'a random_dseq" 13where 14 "empty = (%nrandom size. Pair (Limited_Sequence.empty))" 15 16definition single :: "'a => 'a random_dseq" 17where 18 "single x = (%nrandom size. Pair (Limited_Sequence.single x))" 19 20definition bind :: "'a random_dseq => ('a \<Rightarrow> 'b random_dseq) \<Rightarrow> 'b random_dseq" 21where 22 "bind R f = (\<lambda>nrandom size s. let 23 (P, s') = R nrandom size s; 24 (s1, s2) = Random.split_seed s' 25 in (Limited_Sequence.bind P (%a. fst (f a nrandom size s1)), s2))" 26 27definition union :: "'a random_dseq => 'a random_dseq => 'a random_dseq" 28where 29 "union R1 R2 = (\<lambda>nrandom size s. let 30 (S1, s') = R1 nrandom size s; (S2, s'') = R2 nrandom size s' 31 in (Limited_Sequence.union S1 S2, s''))" 32 33definition if_random_dseq :: "bool => unit random_dseq" 34where 35 "if_random_dseq b = (if b then single () else empty)" 36 37definition not_random_dseq :: "unit random_dseq => unit random_dseq" 38where 39 "not_random_dseq R = (\<lambda>nrandom size s. let 40 (S, s') = R nrandom size s 41 in (Limited_Sequence.not_seq S, s'))" 42 43definition map :: "('a => 'b) => 'a random_dseq => 'b random_dseq" 44where 45 "map f P = bind P (single \<circ> f)" 46 47fun Random :: "(natural \<Rightarrow> Random.seed \<Rightarrow> (('a \<times> (unit \<Rightarrow> term)) \<times> Random.seed)) \<Rightarrow> 'a random_dseq" 48where 49 "Random g nrandom = (%size. if nrandom <= 0 then (Pair Limited_Sequence.empty) else 50 (scomp (g size) (%r. scomp (Random g (nrandom - 1) size) (%rs. Pair (Limited_Sequence.union (Limited_Sequence.single (fst r)) rs)))))" 51 52 53type_synonym 'a pos_random_dseq = "natural \<Rightarrow> natural \<Rightarrow> Random.seed \<Rightarrow> 'a Limited_Sequence.pos_dseq" 54 55definition pos_empty :: "'a pos_random_dseq" 56where 57 "pos_empty = (%nrandom size seed. Limited_Sequence.pos_empty)" 58 59definition pos_single :: "'a => 'a pos_random_dseq" 60where 61 "pos_single x = (%nrandom size seed. Limited_Sequence.pos_single x)" 62 63definition pos_bind :: "'a pos_random_dseq => ('a \<Rightarrow> 'b pos_random_dseq) \<Rightarrow> 'b pos_random_dseq" 64where 65 "pos_bind R f = (\<lambda>nrandom size seed. Limited_Sequence.pos_bind (R nrandom size seed) (%a. f a nrandom size seed))" 66 67definition pos_decr_bind :: "'a pos_random_dseq => ('a \<Rightarrow> 'b pos_random_dseq) \<Rightarrow> 'b pos_random_dseq" 68where 69 "pos_decr_bind R f = (\<lambda>nrandom size seed. Limited_Sequence.pos_decr_bind (R nrandom size seed) (%a. f a nrandom size seed))" 70 71definition pos_union :: "'a pos_random_dseq => 'a pos_random_dseq => 'a pos_random_dseq" 72where 73 "pos_union R1 R2 = (\<lambda>nrandom size seed. Limited_Sequence.pos_union (R1 nrandom size seed) (R2 nrandom size seed))" 74 75definition pos_if_random_dseq :: "bool => unit pos_random_dseq" 76where 77 "pos_if_random_dseq b = (if b then pos_single () else pos_empty)" 78 79definition pos_iterate_upto :: "(natural => 'a) => natural => natural => 'a pos_random_dseq" 80where 81 "pos_iterate_upto f n m = (\<lambda>nrandom size seed. Limited_Sequence.pos_iterate_upto f n m)" 82 83definition pos_map :: "('a => 'b) => 'a pos_random_dseq => 'b pos_random_dseq" 84where 85 "pos_map f P = pos_bind P (pos_single \<circ> f)" 86 87fun iter :: "(Random.seed \<Rightarrow> ('a \<times> (unit \<Rightarrow> term)) \<times> Random.seed) 88 \<Rightarrow> natural \<Rightarrow> Random.seed \<Rightarrow> 'a Lazy_Sequence.lazy_sequence" 89where 90 "iter random nrandom seed = 91 (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')))" 92 93definition pos_Random :: "(natural \<Rightarrow> Random.seed \<Rightarrow> ('a \<times> (unit \<Rightarrow> term)) \<times> Random.seed) 94 \<Rightarrow> 'a pos_random_dseq" 95where 96 "pos_Random g = (%nrandom size seed depth. iter (g size) nrandom seed)" 97 98 99type_synonym 'a neg_random_dseq = "natural \<Rightarrow> natural \<Rightarrow> Random.seed \<Rightarrow> 'a Limited_Sequence.neg_dseq" 100 101definition neg_empty :: "'a neg_random_dseq" 102where 103 "neg_empty = (%nrandom size seed. Limited_Sequence.neg_empty)" 104 105definition neg_single :: "'a => 'a neg_random_dseq" 106where 107 "neg_single x = (%nrandom size seed. Limited_Sequence.neg_single x)" 108 109definition neg_bind :: "'a neg_random_dseq => ('a \<Rightarrow> 'b neg_random_dseq) \<Rightarrow> 'b neg_random_dseq" 110where 111 "neg_bind R f = (\<lambda>nrandom size seed. Limited_Sequence.neg_bind (R nrandom size seed) (%a. f a nrandom size seed))" 112 113definition neg_decr_bind :: "'a neg_random_dseq => ('a \<Rightarrow> 'b neg_random_dseq) \<Rightarrow> 'b neg_random_dseq" 114where 115 "neg_decr_bind R f = (\<lambda>nrandom size seed. Limited_Sequence.neg_decr_bind (R nrandom size seed) (%a. f a nrandom size seed))" 116 117definition neg_union :: "'a neg_random_dseq => 'a neg_random_dseq => 'a neg_random_dseq" 118where 119 "neg_union R1 R2 = (\<lambda>nrandom size seed. Limited_Sequence.neg_union (R1 nrandom size seed) (R2 nrandom size seed))" 120 121definition neg_if_random_dseq :: "bool => unit neg_random_dseq" 122where 123 "neg_if_random_dseq b = (if b then neg_single () else neg_empty)" 124 125definition neg_iterate_upto :: "(natural => 'a) => natural => natural => 'a neg_random_dseq" 126where 127 "neg_iterate_upto f n m = (\<lambda>nrandom size seed. Limited_Sequence.neg_iterate_upto f n m)" 128 129definition neg_not_random_dseq :: "unit pos_random_dseq => unit neg_random_dseq" 130where 131 "neg_not_random_dseq R = (\<lambda>nrandom size seed. Limited_Sequence.neg_not_seq (R nrandom size seed))" 132 133definition neg_map :: "('a => 'b) => 'a neg_random_dseq => 'b neg_random_dseq" 134where 135 "neg_map f P = neg_bind P (neg_single \<circ> f)" 136 137definition pos_not_random_dseq :: "unit neg_random_dseq => unit pos_random_dseq" 138where 139 "pos_not_random_dseq R = (\<lambda>nrandom size seed. Limited_Sequence.pos_not_seq (R nrandom size seed))" 140 141 142hide_const (open) 143 empty single bind union if_random_dseq not_random_dseq map Random 144 pos_empty pos_single pos_bind pos_decr_bind pos_union pos_if_random_dseq pos_iterate_upto 145 pos_not_random_dseq pos_map iter pos_Random 146 neg_empty neg_single neg_bind neg_decr_bind neg_union neg_if_random_dseq neg_iterate_upto 147 neg_not_random_dseq neg_map 148 149hide_fact (open) empty_def single_def bind_def union_def if_random_dseq_def not_random_dseq_def 150 map_def Random.simps 151 pos_empty_def pos_single_def pos_bind_def pos_decr_bind_def pos_union_def pos_if_random_dseq_def 152 pos_iterate_upto_def pos_not_random_dseq_def pos_map_def iter.simps pos_Random_def 153 neg_empty_def neg_single_def neg_bind_def neg_decr_bind_def neg_union_def neg_if_random_dseq_def 154 neg_iterate_upto_def neg_not_random_dseq_def neg_map_def 155 156end 157 158