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