adopting Sequences
authorbulwahn
Wed Jan 20 18:08:08 2010 +0100 (2010-01-20)
changeset 34953a053ad2a7a72
parent 34952 bd7e347eb768
child 34954 b206c70ea6f0
adopting Sequences
src/HOL/DSequence.thy
src/HOL/Random_Sequence.thy
     1.1 --- a/src/HOL/DSequence.thy	Wed Jan 20 18:02:22 2010 +0100
     1.2 +++ b/src/HOL/DSequence.thy	Wed Jan 20 18:08:08 2010 +0100
     1.3 @@ -43,7 +43,7 @@
     1.4          None => None
     1.5        | Some zq => Some (Lazy_Sequence.append yq zq))))"
     1.6  
     1.7 -fun bind :: "'a dseq => ('a => 'b dseq) => 'b dseq"
     1.8 +definition bind :: "'a dseq => ('a => 'b dseq) => 'b dseq"
     1.9  where
    1.10    "bind x f = (%i pol. 
    1.11       if i = 0 then
    1.12 @@ -53,7 +53,7 @@
    1.13           None => None
    1.14         | Some xq => map_seq f xq i pol))"
    1.15  
    1.16 -fun union :: "'a dseq => 'a dseq => 'a dseq"
    1.17 +definition union :: "'a dseq => 'a dseq => 'a dseq"
    1.18  where
    1.19    "union x y = (%i pol. case (x i pol, y i pol) of
    1.20        (Some xq, Some yq) => Some (Lazy_Sequence.append xq yq)
    1.21 @@ -63,7 +63,7 @@
    1.22  where
    1.23    "if_seq b = (if b then single () else empty)"
    1.24  
    1.25 -fun not_seq :: "unit dseq => unit dseq"
    1.26 +definition not_seq :: "unit dseq => unit dseq"
    1.27  where
    1.28    "not_seq x = (%i pol. case x i (\<not>pol) of
    1.29      None => Some Lazy_Sequence.empty
    1.30 @@ -71,7 +71,7 @@
    1.31        None => Some (Lazy_Sequence.single ())
    1.32      | Some _ => Some (Lazy_Sequence.empty)))"
    1.33  
    1.34 -fun map :: "('a => 'b) => 'a dseq => 'b dseq"
    1.35 +definition map :: "('a => 'b) => 'a dseq => 'b dseq"
    1.36  where
    1.37    "map f g = (%i pol. case g i pol of
    1.38       None => None
    1.39 @@ -106,7 +106,7 @@
    1.40    Sequence.append Sequence.flat Sequence.map Sequence.bind Sequence.ifpred Sequence.not_seq
    1.41  *)
    1.42  hide (open) const empty single eval map_seq bind union if_seq not_seq map
    1.43 -hide (open) fact empty_def single_def eval.simps map_seq.simps bind.simps union.simps
    1.44 -  if_seq_def not_seq.simps map.simps
    1.45 +hide (open) fact empty_def single_def eval.simps map_seq.simps bind_def union_def
    1.46 +  if_seq_def not_seq_def map_def
    1.47  
    1.48  end
     2.1 --- a/src/HOL/Random_Sequence.thy	Wed Jan 20 18:02:22 2010 +0100
     2.2 +++ b/src/HOL/Random_Sequence.thy	Wed Jan 20 18:08:08 2010 +0100
     2.3 @@ -56,6 +56,6 @@
     2.4  hide (open) const empty single bind union if_random_dseq not_random_dseq Random map
     2.5  
     2.6  hide type DSequence.dseq random_dseq
     2.7 -hide (open) fact empty_def single_def bind_def union_def if_random_dseq_def not_random_dseq_def Random_def map_def
     2.8 +hide (open) fact empty_def single_def bind_def union_def if_random_dseq_def not_random_dseq_def Random.simps map_def
     2.9  
    2.10  end
    2.11 \ No newline at end of file