src/HOL/Random_Sequence.thy
changeset 51143 0a2371e7ced3
parent 51126 df86080de4cb
child 58889 5b7a9633cfa8
     1.1 --- a/src/HOL/Random_Sequence.thy	Fri Feb 15 08:31:30 2013 +0100
     1.2 +++ b/src/HOL/Random_Sequence.thy	Fri Feb 15 08:31:31 2013 +0100
     1.3 @@ -7,7 +7,7 @@
     1.4  imports Random_Pred
     1.5  begin
     1.6  
     1.7 -type_synonym 'a random_dseq = "code_numeral \<Rightarrow> code_numeral \<Rightarrow> Random.seed \<Rightarrow> ('a Limited_Sequence.dseq \<times> Random.seed)"
     1.8 +type_synonym 'a random_dseq = "natural \<Rightarrow> natural \<Rightarrow> Random.seed \<Rightarrow> ('a Limited_Sequence.dseq \<times> Random.seed)"
     1.9  
    1.10  definition empty :: "'a random_dseq"
    1.11  where
    1.12 @@ -44,13 +44,13 @@
    1.13  where
    1.14    "map f P = bind P (single o f)"
    1.15  
    1.16 -fun Random :: "(code_numeral \<Rightarrow> Random.seed \<Rightarrow> (('a \<times> (unit \<Rightarrow> term)) \<times> Random.seed)) \<Rightarrow> 'a random_dseq"
    1.17 +fun Random :: "(natural \<Rightarrow> Random.seed \<Rightarrow> (('a \<times> (unit \<Rightarrow> term)) \<times> Random.seed)) \<Rightarrow> 'a random_dseq"
    1.18  where
    1.19    "Random g nrandom = (%size. if nrandom <= 0 then (Pair Limited_Sequence.empty) else
    1.20       (scomp (g size) (%r. scomp (Random g (nrandom - 1) size) (%rs. Pair (Limited_Sequence.union (Limited_Sequence.single (fst r)) rs)))))"
    1.21  
    1.22  
    1.23 -type_synonym 'a pos_random_dseq = "code_numeral \<Rightarrow> code_numeral \<Rightarrow> Random.seed \<Rightarrow> 'a Limited_Sequence.pos_dseq"
    1.24 +type_synonym 'a pos_random_dseq = "natural \<Rightarrow> natural \<Rightarrow> Random.seed \<Rightarrow> 'a Limited_Sequence.pos_dseq"
    1.25  
    1.26  definition pos_empty :: "'a pos_random_dseq"
    1.27  where
    1.28 @@ -76,7 +76,7 @@
    1.29  where
    1.30    "pos_if_random_dseq b = (if b then pos_single () else pos_empty)"
    1.31  
    1.32 -definition pos_iterate_upto :: "(code_numeral => 'a) => code_numeral => code_numeral => 'a pos_random_dseq"
    1.33 +definition pos_iterate_upto :: "(natural => 'a) => natural => natural => 'a pos_random_dseq"
    1.34  where
    1.35    "pos_iterate_upto f n m = (\<lambda>nrandom size seed. Limited_Sequence.pos_iterate_upto f n m)"
    1.36  
    1.37 @@ -85,18 +85,18 @@
    1.38    "pos_map f P = pos_bind P (pos_single o f)"
    1.39  
    1.40  fun iter :: "(Random.seed \<Rightarrow> ('a \<times> (unit \<Rightarrow> term)) \<times> Random.seed)
    1.41 -  \<Rightarrow> code_numeral \<Rightarrow> Random.seed \<Rightarrow> 'a Lazy_Sequence.lazy_sequence"
    1.42 +  \<Rightarrow> natural \<Rightarrow> Random.seed \<Rightarrow> 'a Lazy_Sequence.lazy_sequence"
    1.43  where
    1.44    "iter random nrandom seed =
    1.45      (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.46  
    1.47 -definition pos_Random :: "(code_numeral \<Rightarrow> Random.seed \<Rightarrow> ('a \<times> (unit \<Rightarrow> term)) \<times> Random.seed)
    1.48 +definition pos_Random :: "(natural \<Rightarrow> Random.seed \<Rightarrow> ('a \<times> (unit \<Rightarrow> term)) \<times> Random.seed)
    1.49    \<Rightarrow> 'a pos_random_dseq"
    1.50  where
    1.51    "pos_Random g = (%nrandom size seed depth. iter (g size) nrandom seed)"
    1.52  
    1.53  
    1.54 -type_synonym 'a neg_random_dseq = "code_numeral \<Rightarrow> code_numeral \<Rightarrow> Random.seed \<Rightarrow> 'a Limited_Sequence.neg_dseq"
    1.55 +type_synonym 'a neg_random_dseq = "natural \<Rightarrow> natural \<Rightarrow> Random.seed \<Rightarrow> 'a Limited_Sequence.neg_dseq"
    1.56  
    1.57  definition neg_empty :: "'a neg_random_dseq"
    1.58  where
    1.59 @@ -122,7 +122,7 @@
    1.60  where
    1.61    "neg_if_random_dseq b = (if b then neg_single () else neg_empty)"
    1.62  
    1.63 -definition neg_iterate_upto :: "(code_numeral => 'a) => code_numeral => code_numeral => 'a neg_random_dseq"
    1.64 +definition neg_iterate_upto :: "(natural => 'a) => natural => natural => 'a neg_random_dseq"
    1.65  where
    1.66    "neg_iterate_upto f n m = (\<lambda>nrandom size seed. Limited_Sequence.neg_iterate_upto f n m)"
    1.67