src/HOL/New_DSequence.thy
changeset 36902 c6bae4456741
parent 36176 3fe7e97ccca8
child 39183 512c10416590
equal deleted inserted replaced
36901:a20c5484dc9c 36902:c6bae4456741
     5 
     5 
     6 theory New_DSequence
     6 theory New_DSequence
     7 imports Random_Sequence
     7 imports Random_Sequence
     8 begin
     8 begin
     9 
     9 
    10 section {* Positive Depth-Limited Sequence *}
    10 subsection {* Positive Depth-Limited Sequence *}
    11 
    11 
    12 types 'a pos_dseq = "code_numeral => 'a Lazy_Sequence.lazy_sequence"
    12 types 'a pos_dseq = "code_numeral => 'a Lazy_Sequence.lazy_sequence"
    13 
    13 
    14 definition pos_empty :: "'a pos_dseq"
    14 definition pos_empty :: "'a pos_dseq"
    15 where
    15 where
    41  
    41  
    42 definition pos_map :: "('a => 'b) => 'a pos_dseq => 'b pos_dseq"
    42 definition pos_map :: "('a => 'b) => 'a pos_dseq => 'b pos_dseq"
    43 where
    43 where
    44   "pos_map f xq = (%i. Lazy_Sequence.map f (xq i))"
    44   "pos_map f xq = (%i. Lazy_Sequence.map f (xq i))"
    45 
    45 
    46 section {* Negative Depth-Limited Sequence *}
    46 subsection {* Negative Depth-Limited Sequence *}
    47 
    47 
    48 types 'a neg_dseq = "code_numeral => 'a Lazy_Sequence.hit_bound_lazy_sequence"
    48 types 'a neg_dseq = "code_numeral => 'a Lazy_Sequence.hit_bound_lazy_sequence"
    49 
    49 
    50 definition neg_empty :: "'a neg_dseq"
    50 definition neg_empty :: "'a neg_dseq"
    51 where
    51 where
    77 
    77 
    78 definition neg_map :: "('a => 'b) => 'a neg_dseq => 'b neg_dseq"
    78 definition neg_map :: "('a => 'b) => 'a neg_dseq => 'b neg_dseq"
    79 where
    79 where
    80   "neg_map f xq = (%i. Lazy_Sequence.hb_map f (xq i))"
    80   "neg_map f xq = (%i. Lazy_Sequence.hb_map f (xq i))"
    81 
    81 
    82 section {* Negation *}
    82 subsection {* Negation *}
    83 
    83 
    84 definition pos_not_seq :: "unit neg_dseq => unit pos_dseq"
    84 definition pos_not_seq :: "unit neg_dseq => unit pos_dseq"
    85 where
    85 where
    86   "pos_not_seq xq = (%i. Lazy_Sequence.hb_not_seq (xq i))"
    86   "pos_not_seq xq = (%i. Lazy_Sequence.hb_not_seq (xq i))"
    87 
    87