src/HOL/Random_Sequence.thy
author wenzelm
Mon Aug 31 21:28:08 2015 +0200 (2015-08-31)
changeset 61070 b72a990adfe2
parent 60758 d8d85a8172b5
child 67091 1393c2340eec
permissions -rw-r--r--
prefer symbols;
bulwahn@34948
     1
bulwahn@34948
     2
(* Author: Lukas Bulwahn, TU Muenchen *)
bulwahn@34948
     3
wenzelm@60758
     4
section \<open>Various kind of sequences inside the random monad\<close>
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 \<Rightarrow> natural \<Rightarrow> Random.seed \<Rightarrow> ('a Limited_Sequence.dseq \<times> 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 \<Rightarrow> 'b random_dseq) \<Rightarrow> 'b random_dseq"
bulwahn@34948
    21
where
bulwahn@34948
    22
  "bind R f = (\<lambda>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 = (\<lambda>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 = (\<lambda>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 \<Rightarrow> Random.seed \<Rightarrow> (('a \<times> (unit \<Rightarrow> term)) \<times> Random.seed)) \<Rightarrow> '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 \<Rightarrow> natural \<Rightarrow> Random.seed \<Rightarrow> '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 \<Rightarrow> 'b pos_random_dseq) \<Rightarrow> 'b pos_random_dseq"
haftmann@51126
    64
where
haftmann@51126
    65
  "pos_bind R f = (\<lambda>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 \<Rightarrow> 'b pos_random_dseq) \<Rightarrow> 'b pos_random_dseq"
haftmann@51126
    68
where
haftmann@51126
    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))"
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 = (\<lambda>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 = (\<lambda>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 \<Rightarrow> ('a \<times> (unit \<Rightarrow> term)) \<times> Random.seed)
haftmann@51143
    88
  \<Rightarrow> natural \<Rightarrow> Random.seed \<Rightarrow> '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 \<Rightarrow> Random.seed \<Rightarrow> ('a \<times> (unit \<Rightarrow> term)) \<times> Random.seed)
haftmann@51126
    94
  \<Rightarrow> '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 \<Rightarrow> natural \<Rightarrow> Random.seed \<Rightarrow> '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 \<Rightarrow> 'b neg_random_dseq) \<Rightarrow> 'b neg_random_dseq"
haftmann@51126
   110
where
haftmann@51126
   111
  "neg_bind R f = (\<lambda>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 \<Rightarrow> 'b neg_random_dseq) \<Rightarrow> 'b neg_random_dseq"
haftmann@51126
   114
where
haftmann@51126
   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))"
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 = (\<lambda>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 = (\<lambda>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 = (\<lambda>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 = (\<lambda>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