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