src/HOL/Lazy_Sequence.thy
 author bulwahn Wed Jan 20 11:56:45 2010 +0100 (2010-01-20) changeset 34948 2d5f2a9f7601 child 34957 3b1957113753 permissions -rw-r--r--
```     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 fun yieldn :: "code_numeral => 'a lazy_sequence => 'a list * 'a lazy_sequence"
```
```    24 where
```
```    25   "yieldn i S = (if i = 0 then ([], S) else
```
```    26     case yield S of
```
```    27       None => ([], S)
```
```    28     | Some (x, S') => let
```
```    29        (xs, S'') = yieldn (i - 1) S'
```
```    30       in (x # xs, S''))"
```
```    31
```
```    32 lemma [simp]: "yield xq = Some (x, xq') ==> size xq' < size xq"
```
```    33 by (cases xq) auto
```
```    34
```
```    35 lemma yield_Seq [code]:
```
```    36   "yield (Lazy_Sequence f) = f ()"
```
```    37 unfolding Lazy_Sequence_def by (cases "f ()") auto
```
```    38
```
```    39 lemma Seq_yield:
```
```    40   "Lazy_Sequence (%u. yield f) = f"
```
```    41 unfolding Lazy_Sequence_def by (cases f) auto
```
```    42
```
```    43 lemma lazy_sequence_size_code [code]:
```
```    44   "lazy_sequence_size s xq = (case yield xq of None => 0 | Some (x, xq') => s x + lazy_sequence_size s xq' + 1)"
```
```    45 by (cases xq) auto
```
```    46
```
```    47 lemma size_code [code]:
```
```    48   "size xq = (case yield xq of None => 0 | Some (x, xq') => size xq' + 1)"
```
```    49 by (cases xq) auto
```
```    50
```
```    51 lemma [code]: "eq_class.eq xq yq = (case (yield xq, yield yq) of
```
```    52   (None, None) => True | (Some (x, xq'), Some (y, yq')) => (HOL.eq x y) \<and> (eq_class.eq xq yq) | _ => False)"
```
```    53 apply (cases xq) apply (cases yq) apply (auto simp add: eq_class.eq_equals)
```
```    54 apply (cases yq) apply (auto simp add: eq_class.eq_equals) done
```
```    55
```
```    56 lemma seq_case [code]:
```
```    57   "lazy_sequence_case f g xq = (case (yield xq) of None => f | Some (x, xq') => g x xq')"
```
```    58 by (cases xq) auto
```
```    59
```
```    60 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'))"
```
```    61 by (cases xq) auto
```
```    62
```
```    63 definition empty :: "'a lazy_sequence"
```
```    64 where
```
```    65   [code]: "empty = Lazy_Sequence (%u. None)"
```
```    66
```
```    67 definition single :: "'a => 'a lazy_sequence"
```
```    68 where
```
```    69   [code]: "single x = Lazy_Sequence (%u. Some (x, empty))"
```
```    70
```
```    71 primrec append :: "'a lazy_sequence => 'a lazy_sequence => 'a lazy_sequence"
```
```    72 where
```
```    73   "append Empty yq = yq"
```
```    74 | "append (Insert x xq) yq = Insert x (append xq yq)"
```
```    75
```
```    76 lemma [code]:
```
```    77   "append xq yq = Lazy_Sequence (%u. case yield xq of
```
```    78      None => yield yq
```
```    79   | Some (x, xq') => Some (x, append xq' yq))"
```
```    80 unfolding Lazy_Sequence_def
```
```    81 apply (cases "xq")
```
```    82 apply auto
```
```    83 apply (cases "yq")
```
```    84 apply auto
```
```    85 done
```
```    86
```
```    87 primrec flat :: "'a lazy_sequence lazy_sequence => 'a lazy_sequence"
```
```    88 where
```
```    89   "flat Empty = Empty"
```
```    90 | "flat (Insert xq xqq) = append xq (flat xqq)"
```
```    91
```
```    92 lemma [code]:
```
```    93   "flat xqq = Lazy_Sequence (%u. case yield xqq of
```
```    94     None => None
```
```    95   | Some (xq, xqq') => yield (append xq (flat xqq')))"
```
```    96 apply (cases "xqq")
```
```    97 apply (auto simp add: Seq_yield)
```
```    98 unfolding Lazy_Sequence_def
```
```    99 by auto
```
```   100
```
```   101 primrec map :: "('a => 'b) => 'a lazy_sequence => 'b lazy_sequence"
```
```   102 where
```
```   103   "map f Empty = Empty"
```
```   104 | "map f (Insert x xq) = Insert (f x) (map f xq)"
```
```   105
```
```   106 lemma [code]:
```
```   107   "map f xq = Lazy_Sequence (%u. Option.map (%(x, xq'). (f x, map f xq')) (yield xq))"
```
```   108 apply (cases xq)
```
```   109 apply (auto simp add: Seq_yield)
```
```   110 unfolding Lazy_Sequence_def
```
```   111 apply auto
```
```   112 done
```
```   113
```
```   114 definition bind :: "'a lazy_sequence => ('a => 'b lazy_sequence) => 'b lazy_sequence"
```
```   115 where
```
```   116   [code]: "bind xq f = flat (map f xq)"
```
```   117
```
```   118 definition if_seq :: "bool => unit lazy_sequence"
```
```   119 where
```
```   120   "if_seq b = (if b then single () else empty)"
```
```   121
```
```   122 definition not_seq :: "unit lazy_sequence => unit lazy_sequence"
```
```   123 where
```
```   124   "not_seq xq = (case yield xq of None => single () | Some ((), xq) => empty)"
```
```   125
```
```   126 subsection {* Code setup *}
```
```   127
```
```   128 ML {*
```
```   129 signature LAZY_SEQUENCE =
```
```   130 sig
```
```   131   datatype 'a lazy_sequence = Lazy_Sequence of unit -> ('a * 'a lazy_sequence) option
```
```   132   val yield : 'a lazy_sequence -> ('a * 'a lazy_sequence) option
```
```   133   val yieldn : int -> 'a lazy_sequence -> ('a list * 'a lazy_sequence)
```
```   134 end;
```
```   135
```
```   136 structure Lazy_Sequence : LAZY_SEQUENCE =
```
```   137 struct
```
```   138
```
```   139 @{code_datatype lazy_sequence = Lazy_Sequence}
```
```   140
```
```   141 val yield = @{code yield}
```
```   142
```
```   143 val yieldn = @{code yieldn}
```
```   144
```
```   145 end;
```
```   146 *}
```
```   147
```
```   148 code_reserved Eval Lazy_Sequence
```
```   149
```
```   150 code_type lazy_sequence (Eval "_/ Lazy'_Sequence.lazy'_sequence")
```
```   151
```
```   152 code_const Lazy_Sequence (Eval "Lazy'_Sequence.Lazy'_Sequence")
```
```   153
```
```   154 hide (open) type lazy_sequence
```
```   155 hide (open) const Empty Insert Lazy_Sequence yield yieldn empty single append flat map bind if_seq not_seq
```
```   156 hide (open) fact yield.simps yieldn.simps empty_def single_def append.simps flat.simps map.simps bind_def if_seq_def not_seq_def
```
```   157
```
```   158 end
```