src/HOL/DSequence.thy
 author haftmann Mon Nov 29 13:44:54 2010 +0100 (2010-11-29) changeset 40815 6e2d17cc0d1d parent 36176 3fe7e97ccca8 child 42163 392fd6c4669c permissions -rw-r--r--
equivI has replaced equiv.intro
```     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 fun map_seq :: "('a => 'b dseq) => 'a Lazy_Sequence.lazy_sequence => 'b dseq"
```
```    31 where
```
```    32   "map_seq f xq i pol = (case Lazy_Sequence.yield xq of
```
```    33     None => Some Lazy_Sequence.empty
```
```    34   | Some (x, xq') => (case eval (f x) i pol of
```
```    35       None => None
```
```    36     | Some yq => (case map_seq f xq' i pol of
```
```    37         None => None
```
```    38       | Some zq => Some (Lazy_Sequence.append yq zq))))"
```
```    39
```
```    40 definition bind :: "'a dseq => ('a => 'b dseq) => 'b dseq"
```
```    41 where
```
```    42   "bind x f = (%i pol.
```
```    43      if i = 0 then
```
```    44        (if pol then Some Lazy_Sequence.empty else None)
```
```    45      else
```
```    46        (case x (i - 1) pol of
```
```    47          None => None
```
```    48        | Some xq => map_seq f xq i pol))"
```
```    49
```
```    50 definition union :: "'a dseq => 'a dseq => 'a dseq"
```
```    51 where
```
```    52   "union x y = (%i pol. case (x i pol, y i pol) of
```
```    53       (Some xq, Some yq) => Some (Lazy_Sequence.append xq yq)
```
```    54     | _ => None)"
```
```    55
```
```    56 definition if_seq :: "bool => unit dseq"
```
```    57 where
```
```    58   "if_seq b = (if b then single () else empty)"
```
```    59
```
```    60 definition not_seq :: "unit dseq => unit dseq"
```
```    61 where
```
```    62   "not_seq x = (%i pol. case x i (\<not>pol) of
```
```    63     None => Some Lazy_Sequence.empty
```
```    64   | Some xq => (case Lazy_Sequence.yield xq of
```
```    65       None => Some (Lazy_Sequence.single ())
```
```    66     | Some _ => Some (Lazy_Sequence.empty)))"
```
```    67
```
```    68 definition map :: "('a => 'b) => 'a dseq => 'b dseq"
```
```    69 where
```
```    70   "map f g = (%i pol. case g i pol of
```
```    71      None => None
```
```    72    | Some xq => Some (Lazy_Sequence.map f xq))"
```
```    73
```
```    74 ML {*
```
```    75 signature DSEQUENCE =
```
```    76 sig
```
```    77   type 'a dseq = int -> bool -> 'a Lazy_Sequence.lazy_sequence option
```
```    78   val yield : 'a dseq -> int -> bool -> ('a * 'a dseq) option
```
```    79   val yieldn : int -> 'a dseq -> int -> bool -> 'a list * 'a dseq
```
```    80   val map : ('a -> 'b) -> 'a dseq -> 'b dseq
```
```    81 end;
```
```    82
```
```    83 structure DSequence : DSEQUENCE =
```
```    84 struct
```
```    85
```
```    86 type 'a dseq = int -> bool -> 'a Lazy_Sequence.lazy_sequence option
```
```    87
```
```    88 val yield = @{code yield}
```
```    89 fun yieldn n s d pol = case s d pol of
```
```    90     NONE => ([], fn d => fn pol => NONE)
```
```    91   | SOME s => let val (xs, s') = Lazy_Sequence.yieldn n s in (xs, fn d => fn pol => SOME s') end
```
```    92
```
```    93 val map = @{code map}
```
```    94
```
```    95 end;
```
```    96 *}
```
```    97
```
```    98 code_reserved Eval DSequence
```
```    99 (*
```
```   100 hide_type Sequence.seq
```
```   101
```
```   102 hide_const Sequence.Seq Sequence.yield Sequence.yieldn Sequence.empty Sequence.single
```
```   103   Sequence.append Sequence.flat Sequence.map Sequence.bind Sequence.ifpred Sequence.not_seq
```
```   104 *)
```
```   105 hide_const (open) empty single eval map_seq bind union if_seq not_seq map
```
```   106 hide_fact (open) empty_def single_def eval.simps map_seq.simps bind_def union_def
```
```   107   if_seq_def not_seq_def map_def
```
```   108
```
```   109 end
```