src/HOL/Lazy_Sequence.thy
 author huffman Sun Apr 01 16:09:58 2012 +0200 (2012-04-01) changeset 47255 30a1692557b0 parent 45214 66ba67adafab child 50055 94041d602ecb permissions -rw-r--r--
removed Nat_Numeral.thy, moving all theorems elsewhere
```     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]: "HOL.equal xq yq = (case (yield xq, yield yq) of
```
```    43   (None, None) => True | (Some (x, xq'), Some (y, yq')) => (HOL.equal x y) \<and> (HOL.equal xq yq) | _ => False)"
```
```    44 apply (cases xq) apply (cases yq) apply (auto simp add: equal_eq)
```
```    45 apply (cases yq) apply (auto simp add: equal_eq) done
```
```    46
```
```    47 lemma [code nbe]:
```
```    48   "HOL.equal (x :: 'a lazy_sequence) x \<longleftrightarrow> True"
```
```    49   by (fact equal_refl)
```
```    50
```
```    51 lemma seq_case [code]:
```
```    52   "lazy_sequence_case f g xq = (case (yield xq) of None => f | Some (x, xq') => g x xq')"
```
```    53 by (cases xq) auto
```
```    54
```
```    55 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'))"
```
```    56 by (cases xq) auto
```
```    57
```
```    58 definition empty :: "'a lazy_sequence"
```
```    59 where
```
```    60   [code]: "empty = Lazy_Sequence (%u. None)"
```
```    61
```
```    62 definition single :: "'a => 'a lazy_sequence"
```
```    63 where
```
```    64   [code]: "single x = Lazy_Sequence (%u. Some (x, empty))"
```
```    65
```
```    66 primrec append :: "'a lazy_sequence => 'a lazy_sequence => 'a lazy_sequence"
```
```    67 where
```
```    68   "append Empty yq = yq"
```
```    69 | "append (Insert x xq) yq = Insert x (append xq yq)"
```
```    70
```
```    71 lemma [code]:
```
```    72   "append xq yq = Lazy_Sequence (%u. case yield xq of
```
```    73      None => yield yq
```
```    74   | Some (x, xq') => Some (x, append xq' yq))"
```
```    75 unfolding Lazy_Sequence_def
```
```    76 apply (cases "xq")
```
```    77 apply auto
```
```    78 apply (cases "yq")
```
```    79 apply auto
```
```    80 done
```
```    81
```
```    82 primrec flat :: "'a lazy_sequence lazy_sequence => 'a lazy_sequence"
```
```    83 where
```
```    84   "flat Empty = Empty"
```
```    85 | "flat (Insert xq xqq) = append xq (flat xqq)"
```
```    86
```
```    87 lemma [code]:
```
```    88   "flat xqq = Lazy_Sequence (%u. case yield xqq of
```
```    89     None => None
```
```    90   | Some (xq, xqq') => yield (append xq (flat xqq')))"
```
```    91 apply (cases "xqq")
```
```    92 apply (auto simp add: Seq_yield)
```
```    93 unfolding Lazy_Sequence_def
```
```    94 by auto
```
```    95
```
```    96 primrec map :: "('a => 'b) => 'a lazy_sequence => 'b lazy_sequence"
```
```    97 where
```
```    98   "map f Empty = Empty"
```
```    99 | "map f (Insert x xq) = Insert (f x) (map f xq)"
```
```   100
```
```   101 lemma [code]:
```
```   102   "map f xq = Lazy_Sequence (%u. Option.map (%(x, xq'). (f x, map f xq')) (yield xq))"
```
```   103 apply (cases xq)
```
```   104 apply (auto simp add: Seq_yield)
```
```   105 unfolding Lazy_Sequence_def
```
```   106 apply auto
```
```   107 done
```
```   108
```
```   109 definition bind :: "'a lazy_sequence => ('a => 'b lazy_sequence) => 'b lazy_sequence"
```
```   110 where
```
```   111   [code]: "bind xq f = flat (map f xq)"
```
```   112
```
```   113 definition if_seq :: "bool => unit lazy_sequence"
```
```   114 where
```
```   115   "if_seq b = (if b then single () else empty)"
```
```   116
```
```   117 function iterate_upto :: "(code_numeral => 'a) => code_numeral => code_numeral => 'a Lazy_Sequence.lazy_sequence"
```
```   118 where
```
```   119   "iterate_upto f n m = Lazy_Sequence.Lazy_Sequence (%u. if n > m then None else Some (f n, iterate_upto f (n + 1) m))"
```
```   120 by pat_completeness auto
```
```   121
```
```   122 termination by (relation "measure (%(f, n, m). Code_Numeral.nat_of (m + 1 - n))") auto
```
```   123
```
```   124 definition not_seq :: "unit lazy_sequence => unit lazy_sequence"
```
```   125 where
```
```   126   "not_seq xq = (case yield xq of None => single () | Some ((), xq) => empty)"
```
```   127
```
```   128 subsection {* Code setup *}
```
```   129
```
```   130 fun anamorph :: "('a \<Rightarrow> ('b \<times> 'a) option) \<Rightarrow> code_numeral \<Rightarrow> 'a \<Rightarrow> 'b list \<times> 'a" where
```
```   131   "anamorph f k x = (if k = 0 then ([], x)
```
```   132     else case f x of None \<Rightarrow> ([], x) | Some (v, y) \<Rightarrow>
```
```   133       let (vs, z) = anamorph f (k - 1) y
```
```   134     in (v # vs, z))"
```
```   135
```
```   136 definition yieldn :: "code_numeral \<Rightarrow> 'a lazy_sequence \<Rightarrow> 'a list \<times> 'a lazy_sequence" where
```
```   137   "yieldn = anamorph yield"
```
```   138
```
```   139 code_reflect Lazy_Sequence
```
```   140   datatypes lazy_sequence = Lazy_Sequence
```
```   141   functions map yield yieldn
```
```   142
```
```   143 subsection {* Generator Sequences *}
```
```   144
```
```   145
```
```   146 subsubsection {* General lazy sequence operation *}
```
```   147
```
```   148 definition product :: "'a Lazy_Sequence.lazy_sequence \<Rightarrow> 'b Lazy_Sequence.lazy_sequence \<Rightarrow> ('a * 'b) Lazy_Sequence.lazy_sequence"
```
```   149 where
```
```   150   "product s1 s2 = Lazy_Sequence.bind s1 (%a. Lazy_Sequence.bind s2 (%b. Lazy_Sequence.single (a, b)))"
```
```   151
```
```   152
```
```   153 subsubsection {* Small lazy typeclasses *}
```
```   154
```
```   155 class small_lazy =
```
```   156   fixes small_lazy :: "code_numeral \<Rightarrow> 'a Lazy_Sequence.lazy_sequence"
```
```   157
```
```   158 instantiation unit :: small_lazy
```
```   159 begin
```
```   160
```
```   161 definition "small_lazy d = Lazy_Sequence.single ()"
```
```   162
```
```   163 instance ..
```
```   164
```
```   165 end
```
```   166
```
```   167 instantiation int :: small_lazy
```
```   168 begin
```
```   169
```
```   170 text {* maybe optimise this expression -> append (single x) xs == cons x xs
```
```   171 Performance difference? *}
```
```   172
```
```   173 function small_lazy' :: "int => int => int Lazy_Sequence.lazy_sequence"
```
```   174 where "small_lazy' d i = (if d < i then Lazy_Sequence.empty else
```
```   175   Lazy_Sequence.append (Lazy_Sequence.single i) (small_lazy' d (i + 1)))"
```
```   176 by pat_completeness auto
```
```   177
```
```   178 termination
```
```   179   by (relation "measure (%(d, i). nat (d + 1 - i))") auto
```
```   180
```
```   181 definition "small_lazy d = small_lazy' (Code_Numeral.int_of d) (- (Code_Numeral.int_of d))"
```
```   182
```
```   183 instance ..
```
```   184
```
```   185 end
```
```   186
```
```   187 instantiation prod :: (small_lazy, small_lazy) small_lazy
```
```   188 begin
```
```   189
```
```   190 definition
```
```   191   "small_lazy d = product (small_lazy d) (small_lazy d)"
```
```   192
```
```   193 instance ..
```
```   194
```
```   195 end
```
```   196
```
```   197 instantiation list :: (small_lazy) small_lazy
```
```   198 begin
```
```   199
```
```   200 fun small_lazy_list :: "code_numeral => 'a list Lazy_Sequence.lazy_sequence"
```
```   201 where
```
```   202   "small_lazy_list d = Lazy_Sequence.append (Lazy_Sequence.single []) (if d > 0 then Lazy_Sequence.bind (product (small_lazy (d - 1)) (small_lazy (d - 1))) (%(x, xs). Lazy_Sequence.single (x # xs)) else Lazy_Sequence.empty)"
```
```   203
```
```   204 instance ..
```
```   205
```
```   206 end
```
```   207
```
```   208 subsection {* With Hit Bound Value *}
```
```   209 text {* assuming in negative context *}
```
```   210
```
```   211 type_synonym 'a hit_bound_lazy_sequence = "'a option lazy_sequence"
```
```   212
```
```   213 definition hit_bound :: "'a hit_bound_lazy_sequence"
```
```   214 where
```
```   215   [code]: "hit_bound = Lazy_Sequence (%u. Some (None, empty))"
```
```   216
```
```   217 definition hb_single :: "'a => 'a hit_bound_lazy_sequence"
```
```   218 where
```
```   219   [code]: "hb_single x = Lazy_Sequence (%u. Some (Some x, empty))"
```
```   220
```
```   221 primrec hb_flat :: "'a hit_bound_lazy_sequence hit_bound_lazy_sequence => 'a hit_bound_lazy_sequence"
```
```   222 where
```
```   223   "hb_flat Empty = Empty"
```
```   224 | "hb_flat (Insert xq xqq) = append (case xq of None => hit_bound | Some xq => xq) (hb_flat xqq)"
```
```   225
```
```   226 lemma [code]:
```
```   227   "hb_flat xqq = Lazy_Sequence (%u. case yield xqq of
```
```   228     None => None
```
```   229   | Some (xq, xqq') => yield (append (case xq of None => hit_bound | Some xq => xq) (hb_flat xqq')))"
```
```   230 apply (cases "xqq")
```
```   231 apply (auto simp add: Seq_yield)
```
```   232 unfolding Lazy_Sequence_def
```
```   233 by auto
```
```   234
```
```   235 primrec hb_map :: "('a => 'b) => 'a hit_bound_lazy_sequence => 'b hit_bound_lazy_sequence"
```
```   236 where
```
```   237   "hb_map f Empty = Empty"
```
```   238 | "hb_map f (Insert x xq) = Insert (Option.map f x) (hb_map f xq)"
```
```   239
```
```   240 lemma [code]:
```
```   241   "hb_map f xq = Lazy_Sequence (%u. Option.map (%(x, xq'). (Option.map f x, hb_map f xq')) (yield xq))"
```
```   242 apply (cases xq)
```
```   243 apply (auto simp add: Seq_yield)
```
```   244 unfolding Lazy_Sequence_def
```
```   245 apply auto
```
```   246 done
```
```   247
```
```   248 definition hb_bind :: "'a hit_bound_lazy_sequence => ('a => 'b hit_bound_lazy_sequence) => 'b hit_bound_lazy_sequence"
```
```   249 where
```
```   250   [code]: "hb_bind xq f = hb_flat (hb_map f xq)"
```
```   251
```
```   252 definition hb_if_seq :: "bool => unit hit_bound_lazy_sequence"
```
```   253 where
```
```   254   "hb_if_seq b = (if b then hb_single () else empty)"
```
```   255
```
```   256 definition hb_not_seq :: "unit hit_bound_lazy_sequence => unit lazy_sequence"
```
```   257 where
```
```   258   "hb_not_seq xq = (case yield xq of None => single () | Some (x, xq) => empty)"
```
```   259
```
```   260 hide_type (open) lazy_sequence
```
```   261 hide_const (open) Empty Insert Lazy_Sequence yield empty single append flat map bind if_seq
```
```   262   iterate_upto not_seq product
```
```   263
```
```   264 hide_fact yield.simps empty_def single_def append.simps flat.simps map.simps bind_def
```
```   265   iterate_upto.simps product_def if_seq_def not_seq_def
```
```   266
```
```   267 end
```