src/HOL/Lazy_Sequence.thy
author bulwahn
Mon Mar 29 17:30:49 2010 +0200 (2010-03-29)
changeset 36030 1cd962a0b1a6
parent 36024 c1ce2f60b0f2
child 36049 0ce5b7a5c2fd
permissions -rw-r--r--
adding Lazy_Sequences with explicit depth-bound
     1 
     2 (* Author: Lukas Bulwahn, TU Muenchen *)
     3 
     4 header {* Lazy sequences *}
     5 
     6 theory Lazy_Sequence
     7 imports List Code_Numeral
     8 begin
     9 
    10 datatype 'a lazy_sequence = Empty | Insert 'a "'a lazy_sequence"
    11 
    12 definition Lazy_Sequence :: "(unit => ('a * 'a lazy_sequence) option) => 'a lazy_sequence"
    13 where
    14   "Lazy_Sequence f = (case f () of None => Empty | Some (x, xq) => Insert x xq)"
    15 
    16 code_datatype Lazy_Sequence 
    17 
    18 primrec yield :: "'a lazy_sequence => ('a * 'a lazy_sequence) option"
    19 where
    20   "yield Empty = None"
    21 | "yield (Insert x xq) = Some (x, xq)"
    22 
    23 lemma [simp]: "yield xq = Some (x, xq') ==> size xq' < size xq"
    24 by (cases xq) auto
    25 
    26 lemma yield_Seq [code]:
    27   "yield (Lazy_Sequence f) = f ()"
    28 unfolding Lazy_Sequence_def by (cases "f ()") auto
    29 
    30 lemma Seq_yield:
    31   "Lazy_Sequence (%u. yield f) = f"
    32 unfolding Lazy_Sequence_def by (cases f) auto
    33 
    34 lemma lazy_sequence_size_code [code]:
    35   "lazy_sequence_size s xq = (case yield xq of None => 0 | Some (x, xq') => s x + lazy_sequence_size s xq' + 1)"
    36 by (cases xq) auto
    37 
    38 lemma size_code [code]:
    39   "size xq = (case yield xq of None => 0 | Some (x, xq') => size xq' + 1)"
    40 by (cases xq) auto
    41 
    42 lemma [code]: "eq_class.eq xq yq = (case (yield xq, yield yq) of
    43   (None, None) => True | (Some (x, xq'), Some (y, yq')) => (HOL.eq x y) \<and> (eq_class.eq xq yq) | _ => False)"
    44 apply (cases xq) apply (cases yq) apply (auto simp add: eq_class.eq_equals) 
    45 apply (cases yq) apply (auto simp add: eq_class.eq_equals) done
    46 
    47 lemma seq_case [code]:
    48   "lazy_sequence_case f g xq = (case (yield xq) of None => f | Some (x, xq') => g x xq')"
    49 by (cases xq) auto
    50 
    51 lemma [code]: "lazy_sequence_rec f g xq = (case (yield xq) of None => f | Some (x, xq') => g x xq' (lazy_sequence_rec f g xq'))"
    52 by (cases xq) auto
    53 
    54 definition empty :: "'a lazy_sequence"
    55 where
    56   [code]: "empty = Lazy_Sequence (%u. None)"
    57 
    58 definition single :: "'a => 'a lazy_sequence"
    59 where
    60   [code]: "single x = Lazy_Sequence (%u. Some (x, empty))"
    61 
    62 primrec append :: "'a lazy_sequence => 'a lazy_sequence => 'a lazy_sequence"
    63 where
    64   "append Empty yq = yq"
    65 | "append (Insert x xq) yq = Insert x (append xq yq)"
    66 
    67 lemma [code]:
    68   "append xq yq = Lazy_Sequence (%u. case yield xq of
    69      None => yield yq
    70   | Some (x, xq') => Some (x, append xq' yq))"
    71 unfolding Lazy_Sequence_def
    72 apply (cases "xq")
    73 apply auto
    74 apply (cases "yq")
    75 apply auto
    76 done
    77 
    78 primrec flat :: "'a lazy_sequence lazy_sequence => 'a lazy_sequence"
    79 where
    80   "flat Empty = Empty"
    81 | "flat (Insert xq xqq) = append xq (flat xqq)"
    82  
    83 lemma [code]:
    84   "flat xqq = Lazy_Sequence (%u. case yield xqq of
    85     None => None
    86   | Some (xq, xqq') => yield (append xq (flat xqq')))"
    87 apply (cases "xqq")
    88 apply (auto simp add: Seq_yield)
    89 unfolding Lazy_Sequence_def
    90 by auto
    91 
    92 primrec map :: "('a => 'b) => 'a lazy_sequence => 'b lazy_sequence"
    93 where
    94   "map f Empty = Empty"
    95 | "map f (Insert x xq) = Insert (f x) (map f xq)"
    96 
    97 lemma [code]:
    98   "map f xq = Lazy_Sequence (%u. Option.map (%(x, xq'). (f x, map f xq')) (yield xq))"
    99 apply (cases xq)
   100 apply (auto simp add: Seq_yield)
   101 unfolding Lazy_Sequence_def
   102 apply auto
   103 done
   104 
   105 definition bind :: "'a lazy_sequence => ('a => 'b lazy_sequence) => 'b lazy_sequence"
   106 where
   107   [code]: "bind xq f = flat (map f xq)"
   108 
   109 definition if_seq :: "bool => unit lazy_sequence"
   110 where
   111   "if_seq b = (if b then single () else empty)"
   112 
   113 definition not_seq :: "unit lazy_sequence => unit lazy_sequence"
   114 where
   115   "not_seq xq = (case yield xq of None => single () | Some ((), xq) => empty)"
   116 
   117 subsection {* Code setup *}
   118 
   119 ML {*
   120 signature LAZY_SEQUENCE =
   121 sig
   122   datatype 'a lazy_sequence = Lazy_Sequence of unit -> ('a * 'a lazy_sequence) option
   123   val yield : 'a lazy_sequence -> ('a * 'a lazy_sequence) option
   124   val yieldn : int -> 'a lazy_sequence -> ('a list * 'a lazy_sequence)
   125   val map : ('a -> 'b) -> 'a lazy_sequence -> 'b lazy_sequence
   126 end;
   127 
   128 structure Lazy_Sequence : LAZY_SEQUENCE =
   129 struct
   130 
   131 @{code_datatype lazy_sequence = Lazy_Sequence}
   132 
   133 val yield = @{code yield}
   134 
   135 fun anamorph f k x = (if k = 0 then ([], x)
   136   else case f x
   137    of NONE => ([], x)
   138     | SOME (v, y) => let
   139         val (vs, z) = anamorph f (k - 1) y
   140       in (v :: vs, z) end);
   141 
   142 fun yieldn S = anamorph yield S;
   143 
   144 val map = @{code map}
   145 
   146 end;
   147 *}
   148 
   149 code_reserved Eval Lazy_Sequence
   150 
   151 code_type lazy_sequence (Eval "_/ Lazy'_Sequence.lazy'_sequence")
   152 
   153 code_const Lazy_Sequence (Eval "Lazy'_Sequence.Lazy'_Sequence")
   154 
   155 section {* With Hit Bound Value *}
   156 text {* assuming in negative context *}
   157 
   158 types 'a hit_bound_lazy_sequence = "'a option lazy_sequence"
   159 
   160 definition hit_bound :: "'a hit_bound_lazy_sequence"
   161 where
   162   [code]: "hit_bound = Lazy_Sequence (%u. Some (None, empty))"
   163 
   164 
   165 definition hb_single :: "'a => 'a hit_bound_lazy_sequence"
   166 where
   167   [code]: "hb_single x = Lazy_Sequence (%u. Some (Some x, empty))"
   168 
   169 primrec hb_flat :: "'a hit_bound_lazy_sequence hit_bound_lazy_sequence => 'a hit_bound_lazy_sequence"
   170 where
   171   "hb_flat Empty = Empty"
   172 | "hb_flat (Insert xq xqq) = append (case xq of None => hit_bound | Some xq => xq) (hb_flat xqq)"
   173 
   174 lemma [code]:
   175   "hb_flat xqq = Lazy_Sequence (%u. case yield xqq of
   176     None => None
   177   | Some (xq, xqq') => yield (append (case xq of None => hit_bound | Some xq => xq) (hb_flat xqq')))"
   178 apply (cases "xqq")
   179 apply (auto simp add: Seq_yield)
   180 unfolding Lazy_Sequence_def
   181 by auto
   182 
   183 primrec hb_map :: "('a => 'b) => 'a hit_bound_lazy_sequence => 'b hit_bound_lazy_sequence"
   184 where
   185   "hb_map f Empty = Empty"
   186 | "hb_map f (Insert x xq) = Insert (Option.map f x) (hb_map f xq)"
   187 
   188 lemma [code]:
   189   "hb_map f xq = Lazy_Sequence (%u. Option.map (%(x, xq'). (Option.map f x, hb_map f xq')) (yield xq))"
   190 apply (cases xq)
   191 apply (auto simp add: Seq_yield)
   192 unfolding Lazy_Sequence_def
   193 apply auto
   194 done
   195 
   196 definition hb_bind :: "'a hit_bound_lazy_sequence => ('a => 'b hit_bound_lazy_sequence) => 'b hit_bound_lazy_sequence"
   197 where
   198   [code]: "hb_bind xq f = hb_flat (hb_map f xq)"
   199 
   200 definition hb_if_seq :: "bool => unit hit_bound_lazy_sequence"
   201 where
   202   "hb_if_seq b = (if b then hb_single () else empty)"
   203 
   204 definition hb_not_seq :: "unit hit_bound_lazy_sequence => unit lazy_sequence"
   205 where
   206   "hb_not_seq xq = (case yield xq of None => single () | Some (x, xq) => empty)"
   207 
   208 hide (open) type lazy_sequence
   209 hide (open) const Empty Insert Lazy_Sequence yield empty single append flat map bind if_seq not_seq
   210 hide fact yield.simps empty_def single_def append.simps flat.simps map.simps bind_def if_seq_def not_seq_def
   211 
   212 end