src/HOL/Lazy_Sequence.thy
 author hoelzl Fri Feb 19 13:40:50 2016 +0100 (2016-02-19) changeset 62378 85ed00c1fe7c parent 60758 d8d85a8172b5 permissions -rw-r--r--
generalize more theorems to support enat and ennreal
```     1 (* Author: Lukas Bulwahn, TU Muenchen *)
```
```     2
```
```     3 section \<open>Lazy sequences\<close>
```
```     4
```
```     5 theory Lazy_Sequence
```
```     6 imports Predicate
```
```     7 begin
```
```     8
```
```     9 subsection \<open>Type of lazy sequences\<close>
```
```    10
```
```    11 datatype (plugins only: code extraction) (dead 'a) lazy_sequence =
```
```    12   lazy_sequence_of_list "'a list"
```
```    13
```
```    14 primrec list_of_lazy_sequence :: "'a lazy_sequence \<Rightarrow> 'a list"
```
```    15 where
```
```    16   "list_of_lazy_sequence (lazy_sequence_of_list xs) = xs"
```
```    17
```
```    18 lemma lazy_sequence_of_list_of_lazy_sequence [simp]:
```
```    19   "lazy_sequence_of_list (list_of_lazy_sequence xq) = xq"
```
```    20   by (cases xq) simp_all
```
```    21
```
```    22 lemma lazy_sequence_eqI:
```
```    23   "list_of_lazy_sequence xq = list_of_lazy_sequence yq \<Longrightarrow> xq = yq"
```
```    24   by (cases xq, cases yq) simp
```
```    25
```
```    26 lemma lazy_sequence_eq_iff:
```
```    27   "xq = yq \<longleftrightarrow> list_of_lazy_sequence xq = list_of_lazy_sequence yq"
```
```    28   by (auto intro: lazy_sequence_eqI)
```
```    29
```
```    30 lemma case_lazy_sequence [simp]:
```
```    31   "case_lazy_sequence f xq = f (list_of_lazy_sequence xq)"
```
```    32   by (cases xq) auto
```
```    33
```
```    34 lemma rec_lazy_sequence [simp]:
```
```    35   "rec_lazy_sequence f xq = f (list_of_lazy_sequence xq)"
```
```    36   by (cases xq) auto
```
```    37
```
```    38 definition Lazy_Sequence :: "(unit \<Rightarrow> ('a \<times> 'a lazy_sequence) option) \<Rightarrow> 'a lazy_sequence"
```
```    39 where
```
```    40   "Lazy_Sequence f = lazy_sequence_of_list (case f () of
```
```    41     None \<Rightarrow> []
```
```    42   | Some (x, xq) \<Rightarrow> x # list_of_lazy_sequence xq)"
```
```    43
```
```    44 code_datatype Lazy_Sequence
```
```    45
```
```    46 declare list_of_lazy_sequence.simps [code del]
```
```    47 declare lazy_sequence.case [code del]
```
```    48 declare lazy_sequence.rec [code del]
```
```    49
```
```    50 lemma list_of_Lazy_Sequence [simp]:
```
```    51   "list_of_lazy_sequence (Lazy_Sequence f) = (case f () of
```
```    52     None \<Rightarrow> []
```
```    53   | Some (x, xq) \<Rightarrow> x # list_of_lazy_sequence xq)"
```
```    54   by (simp add: Lazy_Sequence_def)
```
```    55
```
```    56 definition yield :: "'a lazy_sequence \<Rightarrow> ('a \<times> 'a lazy_sequence) option"
```
```    57 where
```
```    58   "yield xq = (case list_of_lazy_sequence xq of
```
```    59     [] \<Rightarrow> None
```
```    60   | x # xs \<Rightarrow> Some (x, lazy_sequence_of_list xs))"
```
```    61
```
```    62 lemma yield_Seq [simp, code]:
```
```    63   "yield (Lazy_Sequence f) = f ()"
```
```    64   by (cases "f ()") (simp_all add: yield_def split_def)
```
```    65
```
```    66 lemma case_yield_eq [simp]: "case_option g h (yield xq) =
```
```    67   case_list g (\<lambda>x. curry h x \<circ> lazy_sequence_of_list) (list_of_lazy_sequence xq)"
```
```    68   by (cases "list_of_lazy_sequence xq") (simp_all add: yield_def)
```
```    69
```
```    70 lemma equal_lazy_sequence_code [code]:
```
```    71   "HOL.equal xq yq = (case (yield xq, yield yq) of
```
```    72     (None, None) \<Rightarrow> True
```
```    73   | (Some (x, xq'), Some (y, yq')) \<Rightarrow> HOL.equal x y \<and> HOL.equal xq yq
```
```    74   | _ \<Rightarrow> False)"
```
```    75   by (simp_all add: lazy_sequence_eq_iff equal_eq split: list.splits)
```
```    76
```
```    77 lemma [code nbe]:
```
```    78   "HOL.equal (x :: 'a lazy_sequence) x \<longleftrightarrow> True"
```
```    79   by (fact equal_refl)
```
```    80
```
```    81 definition empty :: "'a lazy_sequence"
```
```    82 where
```
```    83   "empty = lazy_sequence_of_list []"
```
```    84
```
```    85 lemma list_of_lazy_sequence_empty [simp]:
```
```    86   "list_of_lazy_sequence empty = []"
```
```    87   by (simp add: empty_def)
```
```    88
```
```    89 lemma empty_code [code]:
```
```    90   "empty = Lazy_Sequence (\<lambda>_. None)"
```
```    91   by (simp add: lazy_sequence_eq_iff)
```
```    92
```
```    93 definition single :: "'a \<Rightarrow> 'a lazy_sequence"
```
```    94 where
```
```    95   "single x = lazy_sequence_of_list [x]"
```
```    96
```
```    97 lemma list_of_lazy_sequence_single [simp]:
```
```    98   "list_of_lazy_sequence (single x) = [x]"
```
```    99   by (simp add: single_def)
```
```   100
```
```   101 lemma single_code [code]:
```
```   102   "single x = Lazy_Sequence (\<lambda>_. Some (x, empty))"
```
```   103   by (simp add: lazy_sequence_eq_iff)
```
```   104
```
```   105 definition append :: "'a lazy_sequence \<Rightarrow> 'a lazy_sequence \<Rightarrow> 'a lazy_sequence"
```
```   106 where
```
```   107   "append xq yq = lazy_sequence_of_list (list_of_lazy_sequence xq @ list_of_lazy_sequence yq)"
```
```   108
```
```   109 lemma list_of_lazy_sequence_append [simp]:
```
```   110   "list_of_lazy_sequence (append xq yq) = list_of_lazy_sequence xq @ list_of_lazy_sequence yq"
```
```   111   by (simp add: append_def)
```
```   112
```
```   113 lemma append_code [code]:
```
```   114   "append xq yq = Lazy_Sequence (\<lambda>_. case yield xq of
```
```   115     None \<Rightarrow> yield yq
```
```   116   | Some (x, xq') \<Rightarrow> Some (x, append xq' yq))"
```
```   117   by (simp_all add: lazy_sequence_eq_iff split: list.splits)
```
```   118
```
```   119 definition map :: "('a \<Rightarrow> 'b) \<Rightarrow> 'a lazy_sequence \<Rightarrow> 'b lazy_sequence"
```
```   120 where
```
```   121   "map f xq = lazy_sequence_of_list (List.map f (list_of_lazy_sequence xq))"
```
```   122
```
```   123 lemma list_of_lazy_sequence_map [simp]:
```
```   124   "list_of_lazy_sequence (map f xq) = List.map f (list_of_lazy_sequence xq)"
```
```   125   by (simp add: map_def)
```
```   126
```
```   127 lemma map_code [code]:
```
```   128   "map f xq =
```
```   129     Lazy_Sequence (\<lambda>_. map_option (\<lambda>(x, xq'). (f x, map f xq')) (yield xq))"
```
```   130   by (simp_all add: lazy_sequence_eq_iff split: list.splits)
```
```   131
```
```   132 definition flat :: "'a lazy_sequence lazy_sequence \<Rightarrow> 'a lazy_sequence"
```
```   133 where
```
```   134   "flat xqq = lazy_sequence_of_list (concat (List.map list_of_lazy_sequence (list_of_lazy_sequence xqq)))"
```
```   135
```
```   136 lemma list_of_lazy_sequence_flat [simp]:
```
```   137   "list_of_lazy_sequence (flat xqq) = concat (List.map list_of_lazy_sequence (list_of_lazy_sequence xqq))"
```
```   138   by (simp add: flat_def)
```
```   139
```
```   140 lemma flat_code [code]:
```
```   141   "flat xqq = Lazy_Sequence (\<lambda>_. case yield xqq of
```
```   142     None \<Rightarrow> None
```
```   143   | Some (xq, xqq') \<Rightarrow> yield (append xq (flat xqq')))"
```
```   144   by (simp add: lazy_sequence_eq_iff split: list.splits)
```
```   145
```
```   146 definition bind :: "'a lazy_sequence \<Rightarrow> ('a \<Rightarrow> 'b lazy_sequence) \<Rightarrow> 'b lazy_sequence"
```
```   147 where
```
```   148   "bind xq f = flat (map f xq)"
```
```   149
```
```   150 definition if_seq :: "bool \<Rightarrow> unit lazy_sequence"
```
```   151 where
```
```   152   "if_seq b = (if b then single () else empty)"
```
```   153
```
```   154 definition those :: "'a option lazy_sequence \<Rightarrow> 'a lazy_sequence option"
```
```   155 where
```
```   156   "those xq = map_option lazy_sequence_of_list (List.those (list_of_lazy_sequence xq))"
```
```   157
```
```   158 function iterate_upto :: "(natural \<Rightarrow> 'a) \<Rightarrow> natural \<Rightarrow> natural \<Rightarrow> 'a lazy_sequence"
```
```   159 where
```
```   160   "iterate_upto f n m =
```
```   161     Lazy_Sequence (\<lambda>_. if n > m then None else Some (f n, iterate_upto f (n + 1) m))"
```
```   162   by pat_completeness auto
```
```   163
```
```   164 termination by (relation "measure (\<lambda>(f, n, m). nat_of_natural (m + 1 - n))")
```
```   165   (auto simp add: less_natural_def)
```
```   166
```
```   167 definition not_seq :: "unit lazy_sequence \<Rightarrow> unit lazy_sequence"
```
```   168 where
```
```   169   "not_seq xq = (case yield xq of
```
```   170     None \<Rightarrow> single ()
```
```   171   | Some ((), xq) \<Rightarrow> empty)"
```
```   172
```
```   173
```
```   174 subsection \<open>Code setup\<close>
```
```   175
```
```   176 code_reflect Lazy_Sequence
```
```   177   datatypes lazy_sequence = Lazy_Sequence
```
```   178
```
```   179 ML \<open>
```
```   180 signature LAZY_SEQUENCE =
```
```   181 sig
```
```   182   datatype 'a lazy_sequence = Lazy_Sequence of (unit -> ('a * 'a Lazy_Sequence.lazy_sequence) option)
```
```   183   val map: ('a -> 'b) -> 'a lazy_sequence -> 'b lazy_sequence
```
```   184   val yield: 'a lazy_sequence -> ('a * 'a lazy_sequence) option
```
```   185   val yieldn: int -> 'a lazy_sequence -> 'a list * 'a lazy_sequence
```
```   186 end;
```
```   187
```
```   188 structure Lazy_Sequence : LAZY_SEQUENCE =
```
```   189 struct
```
```   190
```
```   191 datatype lazy_sequence = datatype Lazy_Sequence.lazy_sequence;
```
```   192
```
```   193 fun map f = @{code Lazy_Sequence.map} f;
```
```   194
```
```   195 fun yield P = @{code Lazy_Sequence.yield} P;
```
```   196
```
```   197 fun yieldn k = Predicate.anamorph yield k;
```
```   198
```
```   199 end;
```
```   200 \<close>
```
```   201
```
```   202
```
```   203 subsection \<open>Generator Sequences\<close>
```
```   204
```
```   205 subsubsection \<open>General lazy sequence operation\<close>
```
```   206
```
```   207 definition product :: "'a lazy_sequence \<Rightarrow> 'b lazy_sequence \<Rightarrow> ('a \<times> 'b) lazy_sequence"
```
```   208 where
```
```   209   "product s1 s2 = bind s1 (\<lambda>a. bind s2 (\<lambda>b. single (a, b)))"
```
```   210
```
```   211
```
```   212 subsubsection \<open>Small lazy typeclasses\<close>
```
```   213
```
```   214 class small_lazy =
```
```   215   fixes small_lazy :: "natural \<Rightarrow> 'a lazy_sequence"
```
```   216
```
```   217 instantiation unit :: small_lazy
```
```   218 begin
```
```   219
```
```   220 definition "small_lazy d = single ()"
```
```   221
```
```   222 instance ..
```
```   223
```
```   224 end
```
```   225
```
```   226 instantiation int :: small_lazy
```
```   227 begin
```
```   228
```
```   229 text \<open>maybe optimise this expression -> append (single x) xs == cons x xs
```
```   230 Performance difference?\<close>
```
```   231
```
```   232 function small_lazy' :: "int \<Rightarrow> int \<Rightarrow> int lazy_sequence"
```
```   233 where
```
```   234   "small_lazy' d i = (if d < i then empty
```
```   235     else append (single i) (small_lazy' d (i + 1)))"
```
```   236     by pat_completeness auto
```
```   237
```
```   238 termination
```
```   239   by (relation "measure (%(d, i). nat (d + 1 - i))") auto
```
```   240
```
```   241 definition
```
```   242   "small_lazy d = small_lazy' (int (nat_of_natural d)) (- (int (nat_of_natural d)))"
```
```   243
```
```   244 instance ..
```
```   245
```
```   246 end
```
```   247
```
```   248 instantiation prod :: (small_lazy, small_lazy) small_lazy
```
```   249 begin
```
```   250
```
```   251 definition
```
```   252   "small_lazy d = product (small_lazy d) (small_lazy d)"
```
```   253
```
```   254 instance ..
```
```   255
```
```   256 end
```
```   257
```
```   258 instantiation list :: (small_lazy) small_lazy
```
```   259 begin
```
```   260
```
```   261 fun small_lazy_list :: "natural \<Rightarrow> 'a list lazy_sequence"
```
```   262 where
```
```   263   "small_lazy_list d = append (single [])
```
```   264     (if d > 0 then bind (product (small_lazy (d - 1))
```
```   265       (small_lazy (d - 1))) (\<lambda>(x, xs). single (x # xs)) else empty)"
```
```   266
```
```   267 instance ..
```
```   268
```
```   269 end
```
```   270
```
```   271 subsection \<open>With Hit Bound Value\<close>
```
```   272 text \<open>assuming in negative context\<close>
```
```   273
```
```   274 type_synonym 'a hit_bound_lazy_sequence = "'a option lazy_sequence"
```
```   275
```
```   276 definition hit_bound :: "'a hit_bound_lazy_sequence"
```
```   277 where
```
```   278   "hit_bound = Lazy_Sequence (\<lambda>_. Some (None, empty))"
```
```   279
```
```   280 lemma list_of_lazy_sequence_hit_bound [simp]:
```
```   281   "list_of_lazy_sequence hit_bound = [None]"
```
```   282   by (simp add: hit_bound_def)
```
```   283
```
```   284 definition hb_single :: "'a \<Rightarrow> 'a hit_bound_lazy_sequence"
```
```   285 where
```
```   286   "hb_single x = Lazy_Sequence (\<lambda>_. Some (Some x, empty))"
```
```   287
```
```   288 definition hb_map :: "('a \<Rightarrow> 'b) \<Rightarrow> 'a hit_bound_lazy_sequence \<Rightarrow> 'b hit_bound_lazy_sequence"
```
```   289 where
```
```   290   "hb_map f xq = map (map_option f) xq"
```
```   291
```
```   292 lemma hb_map_code [code]:
```
```   293   "hb_map f xq =
```
```   294     Lazy_Sequence (\<lambda>_. map_option (\<lambda>(x, xq'). (map_option f x, hb_map f xq')) (yield xq))"
```
```   295   using map_code [of "map_option f" xq] by (simp add: hb_map_def)
```
```   296
```
```   297 definition hb_flat :: "'a hit_bound_lazy_sequence hit_bound_lazy_sequence \<Rightarrow> 'a hit_bound_lazy_sequence"
```
```   298 where
```
```   299   "hb_flat xqq = lazy_sequence_of_list (concat
```
```   300     (List.map ((\<lambda>x. case x of None \<Rightarrow> [None] | Some xs \<Rightarrow> xs) \<circ> map_option list_of_lazy_sequence) (list_of_lazy_sequence xqq)))"
```
```   301
```
```   302 lemma list_of_lazy_sequence_hb_flat [simp]:
```
```   303   "list_of_lazy_sequence (hb_flat xqq) =
```
```   304     concat (List.map ((\<lambda>x. case x of None \<Rightarrow> [None] | Some xs \<Rightarrow> xs) \<circ> map_option list_of_lazy_sequence) (list_of_lazy_sequence xqq))"
```
```   305   by (simp add: hb_flat_def)
```
```   306
```
```   307 lemma hb_flat_code [code]:
```
```   308   "hb_flat xqq = Lazy_Sequence (\<lambda>_. case yield xqq of
```
```   309     None \<Rightarrow> None
```
```   310   | Some (xq, xqq') \<Rightarrow> yield
```
```   311      (append (case xq of None \<Rightarrow> hit_bound | Some xq \<Rightarrow> xq) (hb_flat xqq')))"
```
```   312   by (simp add: lazy_sequence_eq_iff split: list.splits option.splits)
```
```   313
```
```   314 definition hb_bind :: "'a hit_bound_lazy_sequence \<Rightarrow> ('a \<Rightarrow> 'b hit_bound_lazy_sequence) \<Rightarrow> 'b hit_bound_lazy_sequence"
```
```   315 where
```
```   316   "hb_bind xq f = hb_flat (hb_map f xq)"
```
```   317
```
```   318 definition hb_if_seq :: "bool \<Rightarrow> unit hit_bound_lazy_sequence"
```
```   319 where
```
```   320   "hb_if_seq b = (if b then hb_single () else empty)"
```
```   321
```
```   322 definition hb_not_seq :: "unit hit_bound_lazy_sequence \<Rightarrow> unit lazy_sequence"
```
```   323 where
```
```   324   "hb_not_seq xq = (case yield xq of
```
```   325     None \<Rightarrow> single ()
```
```   326   | Some (x, xq) \<Rightarrow> empty)"
```
```   327
```
```   328 hide_const (open) yield empty single append flat map bind
```
```   329   if_seq those iterate_upto not_seq product
```
```   330
```
```   331 hide_fact (open) yield_def empty_def single_def append_def flat_def map_def bind_def
```
```   332   if_seq_def those_def not_seq_def product_def
```
```   333
```
```   334 end
```