src/HOL/DSequence.thy
author bulwahn
Wed Jan 20 18:08:08 2010 +0100 (2010-01-20)
changeset 34953 a053ad2a7a72
parent 34948 2d5f2a9f7601
child 36024 c1ce2f60b0f2
permissions -rw-r--r--
adopting Sequences
     1 
     2 (* Author: Lukas Bulwahn, TU Muenchen *)
     3 
     4 header {* Depth-Limited Sequences with failure element *}
     5 
     6 theory DSequence
     7 imports Lazy_Sequence Code_Numeral
     8 begin
     9 
    10 types 'a dseq = "code_numeral => bool => 'a Lazy_Sequence.lazy_sequence option"
    11 
    12 definition empty :: "'a dseq"
    13 where
    14   "empty = (%i pol. Some Lazy_Sequence.empty)"
    15 
    16 definition single :: "'a => 'a dseq"
    17 where
    18   "single x = (%i pol. Some (Lazy_Sequence.single x))"
    19 
    20 fun eval :: "'a dseq => code_numeral => bool => 'a Lazy_Sequence.lazy_sequence option"
    21 where
    22   "eval f i pol = f i pol"
    23 
    24 definition yield :: "'a dseq => code_numeral => bool => ('a * 'a dseq) option" 
    25 where
    26   "yield dseq i pol = (case eval dseq i pol of
    27     None => None
    28   | Some s => Option.map (apsnd (%r i pol. Some r)) (Lazy_Sequence.yield s))"
    29 
    30 definition yieldn :: "code_numeral => 'a dseq => code_numeral => bool => 'a list * 'a dseq"
    31 where
    32   "yieldn n dseq i pol = (case eval dseq i pol of
    33     None => ([], %i pol. None)
    34   | Some s => let (xs, s') = Lazy_Sequence.yieldn n s in (xs, %i pol. Some s))"
    35 
    36 fun map_seq :: "('a => 'b dseq) => 'a Lazy_Sequence.lazy_sequence => 'b dseq"
    37 where
    38   "map_seq f xq i pol = (case Lazy_Sequence.yield xq of
    39     None => Some Lazy_Sequence.empty
    40   | Some (x, xq') => (case eval (f x) i pol of
    41       None => None
    42     | Some yq => (case map_seq f xq' i pol of
    43         None => None
    44       | Some zq => Some (Lazy_Sequence.append yq zq))))"
    45 
    46 definition bind :: "'a dseq => ('a => 'b dseq) => 'b dseq"
    47 where
    48   "bind x f = (%i pol. 
    49      if i = 0 then
    50        (if pol then Some Lazy_Sequence.empty else None)
    51      else
    52        (case x (i - 1) pol of
    53          None => None
    54        | Some xq => map_seq f xq i pol))"
    55 
    56 definition union :: "'a dseq => 'a dseq => 'a dseq"
    57 where
    58   "union x y = (%i pol. case (x i pol, y i pol) of
    59       (Some xq, Some yq) => Some (Lazy_Sequence.append xq yq)
    60     | _ => None)"
    61 
    62 definition if_seq :: "bool => unit dseq"
    63 where
    64   "if_seq b = (if b then single () else empty)"
    65 
    66 definition not_seq :: "unit dseq => unit dseq"
    67 where
    68   "not_seq x = (%i pol. case x i (\<not>pol) of
    69     None => Some Lazy_Sequence.empty
    70   | Some xq => (case Lazy_Sequence.yield xq of
    71       None => Some (Lazy_Sequence.single ())
    72     | Some _ => Some (Lazy_Sequence.empty)))"
    73 
    74 definition map :: "('a => 'b) => 'a dseq => 'b dseq"
    75 where
    76   "map f g = (%i pol. case g i pol of
    77      None => None
    78    | Some xq => Some (Lazy_Sequence.map f xq))"
    79 
    80 ML {*
    81 signature DSEQUENCE =
    82 sig
    83   type 'a dseq = int -> bool -> 'a Lazy_Sequence.lazy_sequence option
    84   val yield : 'a dseq -> int -> bool -> ('a * 'a dseq) option
    85   val yieldn : int -> 'a dseq -> int -> bool -> 'a list * 'a dseq
    86   val map : ('a -> 'b) -> 'a dseq -> 'b dseq
    87 end;
    88 
    89 structure DSequence : DSEQUENCE =
    90 struct
    91 
    92 type 'a dseq = int -> bool -> 'a Lazy_Sequence.lazy_sequence option
    93 
    94 val yieldn = @{code yieldn}
    95 val yield = @{code yield}
    96 val map = @{code map}
    97 
    98 end;
    99 *}
   100 
   101 code_reserved Eval DSequence
   102 (*
   103 hide type Sequence.seq
   104 
   105 hide const Sequence.Seq Sequence.yield Sequence.yieldn Sequence.empty Sequence.single
   106   Sequence.append Sequence.flat Sequence.map Sequence.bind Sequence.ifpred Sequence.not_seq
   107 *)
   108 hide (open) const empty single eval map_seq bind union if_seq not_seq map
   109 hide (open) fact empty_def single_def eval.simps map_seq.simps bind_def union_def
   110   if_seq_def not_seq_def map_def
   111 
   112 end