src/HOL/New_DSequence.thy
changeset 36017 7516568bebeb
child 36049 0ce5b7a5c2fd
     1.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.2 +++ b/src/HOL/New_DSequence.thy	Mon Mar 29 17:30:34 2010 +0200
     1.3 @@ -0,0 +1,95 @@
     1.4 +
     1.5 +(* Author: Lukas Bulwahn, TU Muenchen *)
     1.6 +
     1.7 +header {* Depth-Limited Sequences with failure element *}
     1.8 +
     1.9 +theory New_DSequence
    1.10 +imports Random_Sequence
    1.11 +begin
    1.12 +
    1.13 +section {* Positive Depth-Limited Sequence *}
    1.14 +
    1.15 +types 'a pos_dseq = "code_numeral => 'a Lazy_Sequence.lazy_sequence"
    1.16 +
    1.17 +definition pos_empty :: "'a pos_dseq"
    1.18 +where
    1.19 +  "pos_empty = (%i. Lazy_Sequence.empty)"
    1.20 +
    1.21 +definition pos_single :: "'a => 'a pos_dseq"
    1.22 +where
    1.23 +  "pos_single x = (%i. Lazy_Sequence.single x)"
    1.24 +
    1.25 +definition pos_bind :: "'a pos_dseq => ('a => 'b pos_dseq) => 'b pos_dseq"
    1.26 +where
    1.27 +  "pos_bind x f = (%i. 
    1.28 +     if i = 0 then
    1.29 +       Lazy_Sequence.empty
    1.30 +     else
    1.31 +       Lazy_Sequence.bind (x (i - 1)) (%a. f a i))"
    1.32 +
    1.33 +definition pos_union :: "'a pos_dseq => 'a pos_dseq => 'a pos_dseq"
    1.34 +where
    1.35 +  "pos_union xq yq = (%i. Lazy_Sequence.append (xq i) (yq i))"
    1.36 +
    1.37 +definition pos_if_seq :: "bool => unit pos_dseq"
    1.38 +where
    1.39 +  "pos_if_seq b = (if b then pos_single () else pos_empty)"
    1.40 +
    1.41 +definition pos_map :: "('a => 'b) => 'a pos_dseq => 'b pos_dseq"
    1.42 +where
    1.43 +  "pos_map f xq = (%i. Lazy_Sequence.map f (xq i))"
    1.44 +
    1.45 +section {* Negative Depth-Limited Sequence *}
    1.46 +
    1.47 +types 'a neg_dseq = "code_numeral => 'a Lazy_Sequence.hit_bound_lazy_sequence"
    1.48 +
    1.49 +definition neg_empty :: "'a neg_dseq"
    1.50 +where
    1.51 +  "neg_empty = (%i. Lazy_Sequence.empty)"
    1.52 +
    1.53 +definition neg_single :: "'a => 'a neg_dseq"
    1.54 +where
    1.55 +  "neg_single x = (%i. Lazy_Sequence.hb_single x)"
    1.56 +
    1.57 +definition neg_bind :: "'a neg_dseq => ('a => 'b neg_dseq) => 'b neg_dseq"
    1.58 +where
    1.59 +  "neg_bind x f = (%i. 
    1.60 +     if i = 0 then
    1.61 +       Lazy_Sequence.hit_bound
    1.62 +     else
    1.63 +       hb_bind (x (i - 1)) (%a. f a i))"
    1.64 +
    1.65 +definition neg_union :: "'a neg_dseq => 'a neg_dseq => 'a neg_dseq"
    1.66 +where
    1.67 +  "neg_union x y = (%i. Lazy_Sequence.append (x i) (y i))"
    1.68 +
    1.69 +definition neg_if_seq :: "bool => unit neg_dseq"
    1.70 +where
    1.71 +  "neg_if_seq b = (if b then neg_single () else neg_empty)"
    1.72 +
    1.73 +definition neg_map :: "('a => 'b) => 'a neg_dseq => 'b neg_dseq"
    1.74 +where
    1.75 +  "neg_map f xq = (%i. Lazy_Sequence.hb_map f (xq i))"
    1.76 +
    1.77 +section {* Negation *}
    1.78 +
    1.79 +definition pos_not_seq :: "unit neg_dseq => unit pos_dseq"
    1.80 +where
    1.81 +  "pos_not_seq xq = (%i. Lazy_Sequence.hb_not_seq (xq i))"
    1.82 +
    1.83 +definition neg_not_seq :: "unit pos_dseq => unit neg_dseq"
    1.84 +where
    1.85 +  "neg_not_seq x = (%i. case Lazy_Sequence.yield (x i) of
    1.86 +    None => Lazy_Sequence.hb_single ()
    1.87 +  | Some ((), xq) => Lazy_Sequence.empty)"
    1.88 +
    1.89 +hide (open) type pos_dseq neg_dseq
    1.90 +
    1.91 +hide (open) const 
    1.92 +  pos_empty pos_single pos_bind pos_union pos_if_seq pos_not_seq
    1.93 +  neg_empty neg_single neg_bind neg_union neg_if_seq neg_not_seq
    1.94 +hide (open) fact
    1.95 +  pos_empty_def pos_single_def pos_bind_def pos_union_def pos_if_seq_def pos_not_seq_def pos_map_def
    1.96 +  neg_empty_def neg_single_def neg_bind_def neg_union_def neg_if_seq_def neg_not_seq_def neg_map_def
    1.97 +
    1.98 +end