src/HOL/DSequence.thy
changeset 34948 2d5f2a9f7601
child 34953 a053ad2a7a72
     1.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.2 +++ b/src/HOL/DSequence.thy	Wed Jan 20 11:56:45 2010 +0100
     1.3 @@ -0,0 +1,112 @@
     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 DSequence
    1.10 +imports Lazy_Sequence Code_Numeral
    1.11 +begin
    1.12 +
    1.13 +types 'a dseq = "code_numeral => bool => 'a Lazy_Sequence.lazy_sequence option"
    1.14 +
    1.15 +definition empty :: "'a dseq"
    1.16 +where
    1.17 +  "empty = (%i pol. Some Lazy_Sequence.empty)"
    1.18 +
    1.19 +definition single :: "'a => 'a dseq"
    1.20 +where
    1.21 +  "single x = (%i pol. Some (Lazy_Sequence.single x))"
    1.22 +
    1.23 +fun eval :: "'a dseq => code_numeral => bool => 'a Lazy_Sequence.lazy_sequence option"
    1.24 +where
    1.25 +  "eval f i pol = f i pol"
    1.26 +
    1.27 +definition yield :: "'a dseq => code_numeral => bool => ('a * 'a dseq) option" 
    1.28 +where
    1.29 +  "yield dseq i pol = (case eval dseq i pol of
    1.30 +    None => None
    1.31 +  | Some s => Option.map (apsnd (%r i pol. Some r)) (Lazy_Sequence.yield s))"
    1.32 +
    1.33 +definition yieldn :: "code_numeral => 'a dseq => code_numeral => bool => 'a list * 'a dseq"
    1.34 +where
    1.35 +  "yieldn n dseq i pol = (case eval dseq i pol of
    1.36 +    None => ([], %i pol. None)
    1.37 +  | Some s => let (xs, s') = Lazy_Sequence.yieldn n s in (xs, %i pol. Some s))"
    1.38 +
    1.39 +fun map_seq :: "('a => 'b dseq) => 'a Lazy_Sequence.lazy_sequence => 'b dseq"
    1.40 +where
    1.41 +  "map_seq f xq i pol = (case Lazy_Sequence.yield xq of
    1.42 +    None => Some Lazy_Sequence.empty
    1.43 +  | Some (x, xq') => (case eval (f x) i pol of
    1.44 +      None => None
    1.45 +    | Some yq => (case map_seq f xq' i pol of
    1.46 +        None => None
    1.47 +      | Some zq => Some (Lazy_Sequence.append yq zq))))"
    1.48 +
    1.49 +fun bind :: "'a dseq => ('a => 'b dseq) => 'b dseq"
    1.50 +where
    1.51 +  "bind x f = (%i pol. 
    1.52 +     if i = 0 then
    1.53 +       (if pol then Some Lazy_Sequence.empty else None)
    1.54 +     else
    1.55 +       (case x (i - 1) pol of
    1.56 +         None => None
    1.57 +       | Some xq => map_seq f xq i pol))"
    1.58 +
    1.59 +fun union :: "'a dseq => 'a dseq => 'a dseq"
    1.60 +where
    1.61 +  "union x y = (%i pol. case (x i pol, y i pol) of
    1.62 +      (Some xq, Some yq) => Some (Lazy_Sequence.append xq yq)
    1.63 +    | _ => None)"
    1.64 +
    1.65 +definition if_seq :: "bool => unit dseq"
    1.66 +where
    1.67 +  "if_seq b = (if b then single () else empty)"
    1.68 +
    1.69 +fun not_seq :: "unit dseq => unit dseq"
    1.70 +where
    1.71 +  "not_seq x = (%i pol. case x i (\<not>pol) of
    1.72 +    None => Some Lazy_Sequence.empty
    1.73 +  | Some xq => (case Lazy_Sequence.yield xq of
    1.74 +      None => Some (Lazy_Sequence.single ())
    1.75 +    | Some _ => Some (Lazy_Sequence.empty)))"
    1.76 +
    1.77 +fun map :: "('a => 'b) => 'a dseq => 'b dseq"
    1.78 +where
    1.79 +  "map f g = (%i pol. case g i pol of
    1.80 +     None => None
    1.81 +   | Some xq => Some (Lazy_Sequence.map f xq))"
    1.82 +
    1.83 +ML {*
    1.84 +signature DSEQUENCE =
    1.85 +sig
    1.86 +  type 'a dseq = int -> bool -> 'a Lazy_Sequence.lazy_sequence option
    1.87 +  val yield : 'a dseq -> int -> bool -> ('a * 'a dseq) option
    1.88 +  val yieldn : int -> 'a dseq -> int -> bool -> 'a list * 'a dseq
    1.89 +  val map : ('a -> 'b) -> 'a dseq -> 'b dseq
    1.90 +end;
    1.91 +
    1.92 +structure DSequence : DSEQUENCE =
    1.93 +struct
    1.94 +
    1.95 +type 'a dseq = int -> bool -> 'a Lazy_Sequence.lazy_sequence option
    1.96 +
    1.97 +val yieldn = @{code yieldn}
    1.98 +val yield = @{code yield}
    1.99 +val map = @{code map}
   1.100 +
   1.101 +end;
   1.102 +*}
   1.103 +
   1.104 +code_reserved Eval DSequence
   1.105 +(*
   1.106 +hide type Sequence.seq
   1.107 +
   1.108 +hide const Sequence.Seq Sequence.yield Sequence.yieldn Sequence.empty Sequence.single
   1.109 +  Sequence.append Sequence.flat Sequence.map Sequence.bind Sequence.ifpred Sequence.not_seq
   1.110 +*)
   1.111 +hide (open) const empty single eval map_seq bind union if_seq not_seq map
   1.112 +hide (open) fact empty_def single_def eval.simps map_seq.simps bind.simps union.simps
   1.113 +  if_seq_def not_seq.simps map.simps
   1.114 +
   1.115 +end