1(* Author: Lukas Bulwahn, TU Muenchen *) 2 3section \<open>Lazy sequences\<close> 4 5theory Lazy_Sequence 6imports Predicate 7begin 8 9subsection \<open>Type of lazy sequences\<close> 10 11datatype (plugins only: code extraction) (dead 'a) lazy_sequence = 12 lazy_sequence_of_list "'a list" 13 14primrec list_of_lazy_sequence :: "'a lazy_sequence \<Rightarrow> 'a list" 15where 16 "list_of_lazy_sequence (lazy_sequence_of_list xs) = xs" 17 18lemma 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 22lemma 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 26lemma 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 30lemma case_lazy_sequence [simp]: 31 "case_lazy_sequence f xq = f (list_of_lazy_sequence xq)" 32 by (cases xq) auto 33 34lemma rec_lazy_sequence [simp]: 35 "rec_lazy_sequence f xq = f (list_of_lazy_sequence xq)" 36 by (cases xq) auto 37 38definition Lazy_Sequence :: "(unit \<Rightarrow> ('a \<times> 'a lazy_sequence) option) \<Rightarrow> 'a lazy_sequence" 39where 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 44code_datatype Lazy_Sequence 45 46declare list_of_lazy_sequence.simps [code del] 47declare lazy_sequence.case [code del] 48declare lazy_sequence.rec [code del] 49 50lemma 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 56definition yield :: "'a lazy_sequence \<Rightarrow> ('a \<times> 'a lazy_sequence) option" 57where 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 62lemma yield_Seq [simp, code]: 63 "yield (Lazy_Sequence f) = f ()" 64 by (cases "f ()") (simp_all add: yield_def split_def) 65 66lemma 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 70lemma 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 77lemma [code nbe]: 78 "HOL.equal (x :: 'a lazy_sequence) x \<longleftrightarrow> True" 79 by (fact equal_refl) 80 81definition empty :: "'a lazy_sequence" 82where 83 "empty = lazy_sequence_of_list []" 84 85lemma list_of_lazy_sequence_empty [simp]: 86 "list_of_lazy_sequence empty = []" 87 by (simp add: empty_def) 88 89lemma empty_code [code]: 90 "empty = Lazy_Sequence (\<lambda>_. None)" 91 by (simp add: lazy_sequence_eq_iff) 92 93definition single :: "'a \<Rightarrow> 'a lazy_sequence" 94where 95 "single x = lazy_sequence_of_list [x]" 96 97lemma list_of_lazy_sequence_single [simp]: 98 "list_of_lazy_sequence (single x) = [x]" 99 by (simp add: single_def) 100 101lemma single_code [code]: 102 "single x = Lazy_Sequence (\<lambda>_. Some (x, empty))" 103 by (simp add: lazy_sequence_eq_iff) 104 105definition append :: "'a lazy_sequence \<Rightarrow> 'a lazy_sequence \<Rightarrow> 'a lazy_sequence" 106where 107 "append xq yq = lazy_sequence_of_list (list_of_lazy_sequence xq @ list_of_lazy_sequence yq)" 108 109lemma 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 113lemma 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 119definition map :: "('a \<Rightarrow> 'b) \<Rightarrow> 'a lazy_sequence \<Rightarrow> 'b lazy_sequence" 120where 121 "map f xq = lazy_sequence_of_list (List.map f (list_of_lazy_sequence xq))" 122 123lemma 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 127lemma 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 132definition flat :: "'a lazy_sequence lazy_sequence \<Rightarrow> 'a lazy_sequence" 133where 134 "flat xqq = lazy_sequence_of_list (concat (List.map list_of_lazy_sequence (list_of_lazy_sequence xqq)))" 135 136lemma 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 140lemma 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 146definition bind :: "'a lazy_sequence \<Rightarrow> ('a \<Rightarrow> 'b lazy_sequence) \<Rightarrow> 'b lazy_sequence" 147where 148 "bind xq f = flat (map f xq)" 149 150definition if_seq :: "bool \<Rightarrow> unit lazy_sequence" 151where 152 "if_seq b = (if b then single () else empty)" 153 154definition those :: "'a option lazy_sequence \<Rightarrow> 'a lazy_sequence option" 155where 156 "those xq = map_option lazy_sequence_of_list (List.those (list_of_lazy_sequence xq))" 157 158function iterate_upto :: "(natural \<Rightarrow> 'a) \<Rightarrow> natural \<Rightarrow> natural \<Rightarrow> 'a lazy_sequence" 159where 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 164termination by (relation "measure (\<lambda>(f, n, m). nat_of_natural (m + 1 - n))") 165 (auto simp add: less_natural_def) 166 167definition not_seq :: "unit lazy_sequence \<Rightarrow> unit lazy_sequence" 168where 169 "not_seq xq = (case yield xq of 170 None \<Rightarrow> single () 171 | Some ((), xq) \<Rightarrow> empty)" 172 173 174subsection \<open>Code setup\<close> 175 176code_reflect Lazy_Sequence 177 datatypes lazy_sequence = Lazy_Sequence 178 179ML \<open> 180signature LAZY_SEQUENCE = 181sig 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 186end; 187 188structure Lazy_Sequence : LAZY_SEQUENCE = 189struct 190 191datatype lazy_sequence = datatype Lazy_Sequence.lazy_sequence; 192 193fun map f = @{code Lazy_Sequence.map} f; 194 195fun yield P = @{code Lazy_Sequence.yield} P; 196 197fun yieldn k = Predicate.anamorph yield k; 198 199end; 200\<close> 201 202 203subsection \<open>Generator Sequences\<close> 204 205subsubsection \<open>General lazy sequence operation\<close> 206 207definition product :: "'a lazy_sequence \<Rightarrow> 'b lazy_sequence \<Rightarrow> ('a \<times> 'b) lazy_sequence" 208where 209 "product s1 s2 = bind s1 (\<lambda>a. bind s2 (\<lambda>b. single (a, b)))" 210 211 212subsubsection \<open>Small lazy typeclasses\<close> 213 214class small_lazy = 215 fixes small_lazy :: "natural \<Rightarrow> 'a lazy_sequence" 216 217instantiation unit :: small_lazy 218begin 219 220definition "small_lazy d = single ()" 221 222instance .. 223 224end 225 226instantiation int :: small_lazy 227begin 228 229text \<open>maybe optimise this expression -> append (single x) xs == cons x xs 230Performance difference?\<close> 231 232function small_lazy' :: "int \<Rightarrow> int \<Rightarrow> int lazy_sequence" 233where 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 238termination 239 by (relation "measure (%(d, i). nat (d + 1 - i))") auto 240 241definition 242 "small_lazy d = small_lazy' (int (nat_of_natural d)) (- (int (nat_of_natural d)))" 243 244instance .. 245 246end 247 248instantiation prod :: (small_lazy, small_lazy) small_lazy 249begin 250 251definition 252 "small_lazy d = product (small_lazy d) (small_lazy d)" 253 254instance .. 255 256end 257 258instantiation list :: (small_lazy) small_lazy 259begin 260 261fun small_lazy_list :: "natural \<Rightarrow> 'a list lazy_sequence" 262where 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 267instance .. 268 269end 270 271subsection \<open>With Hit Bound Value\<close> 272text \<open>assuming in negative context\<close> 273 274type_synonym 'a hit_bound_lazy_sequence = "'a option lazy_sequence" 275 276definition hit_bound :: "'a hit_bound_lazy_sequence" 277where 278 "hit_bound = Lazy_Sequence (\<lambda>_. Some (None, empty))" 279 280lemma list_of_lazy_sequence_hit_bound [simp]: 281 "list_of_lazy_sequence hit_bound = [None]" 282 by (simp add: hit_bound_def) 283 284definition hb_single :: "'a \<Rightarrow> 'a hit_bound_lazy_sequence" 285where 286 "hb_single x = Lazy_Sequence (\<lambda>_. Some (Some x, empty))" 287 288definition hb_map :: "('a \<Rightarrow> 'b) \<Rightarrow> 'a hit_bound_lazy_sequence \<Rightarrow> 'b hit_bound_lazy_sequence" 289where 290 "hb_map f xq = map (map_option f) xq" 291 292lemma 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 297definition hb_flat :: "'a hit_bound_lazy_sequence hit_bound_lazy_sequence \<Rightarrow> 'a hit_bound_lazy_sequence" 298where 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 302lemma 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 307lemma 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 314definition hb_bind :: "'a hit_bound_lazy_sequence \<Rightarrow> ('a \<Rightarrow> 'b hit_bound_lazy_sequence) \<Rightarrow> 'b hit_bound_lazy_sequence" 315where 316 "hb_bind xq f = hb_flat (hb_map f xq)" 317 318definition hb_if_seq :: "bool \<Rightarrow> unit hit_bound_lazy_sequence" 319where 320 "hb_if_seq b = (if b then hb_single () else empty)" 321 322definition hb_not_seq :: "unit hit_bound_lazy_sequence \<Rightarrow> unit lazy_sequence" 323where 324 "hb_not_seq xq = (case yield xq of 325 None \<Rightarrow> single () 326 | Some (x, xq) \<Rightarrow> empty)" 327 328hide_const (open) yield empty single append flat map bind 329 if_seq those iterate_upto not_seq product 330 331hide_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 334end 335