bulwahn@34948: 
bulwahn@34948: (* Author: Lukas Bulwahn, TU Muenchen *)
bulwahn@34948: 
bulwahn@34948: header {* Lazy sequences *}
bulwahn@34948: 
bulwahn@34948: theory Lazy_Sequence
haftmann@50055: imports Predicate
bulwahn@34948: begin
bulwahn@34948: 
haftmann@51126: subsection {* Type of lazy sequences *}
bulwahn@34948: 
blanchet@58152: datatype_new (dead 'a) lazy_sequence = lazy_sequence_of_list "'a list"
bulwahn@34948: 
haftmann@51126: primrec list_of_lazy_sequence :: "'a lazy_sequence \<Rightarrow> 'a list"
bulwahn@34948: where
haftmann@51126:   "list_of_lazy_sequence (lazy_sequence_of_list xs) = xs"
haftmann@51126: 
haftmann@51126: lemma lazy_sequence_of_list_of_lazy_sequence [simp]:
haftmann@51126:   "lazy_sequence_of_list (list_of_lazy_sequence xq) = xq"
haftmann@51126:   by (cases xq) simp_all
haftmann@51126: 
haftmann@51126: lemma lazy_sequence_eqI:
haftmann@51126:   "list_of_lazy_sequence xq = list_of_lazy_sequence yq \<Longrightarrow> xq = yq"
haftmann@51126:   by (cases xq, cases yq) simp
haftmann@51126: 
haftmann@51126: lemma lazy_sequence_eq_iff:
haftmann@51126:   "xq = yq \<longleftrightarrow> list_of_lazy_sequence xq = list_of_lazy_sequence yq"
haftmann@51126:   by (auto intro: lazy_sequence_eqI)
bulwahn@34948: 
haftmann@51126: lemma size_lazy_sequence_eq [code]:
blanchet@56846:   "size_lazy_sequence f xq = Suc (size_list f (list_of_lazy_sequence xq))"
blanchet@58152:   "size xq = Suc (length (list_of_lazy_sequence xq))"
blanchet@56846:   by (cases xq, simp)+
haftmann@51126: 
blanchet@55416: lemma case_lazy_sequence [simp]:
blanchet@55416:   "case_lazy_sequence f xq = f (list_of_lazy_sequence xq)"
haftmann@51126:   by (cases xq) auto
haftmann@51126: 
blanchet@55416: lemma rec_lazy_sequence [simp]:
blanchet@55416:   "rec_lazy_sequence f xq = f (list_of_lazy_sequence xq)"
haftmann@51126:   by (cases xq) auto
bulwahn@34948: 
haftmann@51126: definition Lazy_Sequence :: "(unit \<Rightarrow> ('a \<times> 'a lazy_sequence) option) \<Rightarrow> 'a lazy_sequence"
haftmann@51126: where
haftmann@51126:   "Lazy_Sequence f = lazy_sequence_of_list (case f () of
haftmann@51126:     None \<Rightarrow> []
haftmann@51126:   | Some (x, xq) \<Rightarrow> x # list_of_lazy_sequence xq)"
haftmann@51126: 
haftmann@51126: code_datatype Lazy_Sequence
haftmann@51126: 
haftmann@51126: declare list_of_lazy_sequence.simps [code del]
blanchet@55642: declare lazy_sequence.case [code del]
blanchet@55642: declare lazy_sequence.rec [code del]
bulwahn@34948: 
haftmann@51126: lemma list_of_Lazy_Sequence [simp]:
haftmann@51126:   "list_of_lazy_sequence (Lazy_Sequence f) = (case f () of
haftmann@51126:     None \<Rightarrow> []
haftmann@51126:   | Some (x, xq) \<Rightarrow> x # list_of_lazy_sequence xq)"
haftmann@51126:   by (simp add: Lazy_Sequence_def)
haftmann@51126: 
haftmann@51126: definition yield :: "'a lazy_sequence \<Rightarrow> ('a \<times> 'a lazy_sequence) option"
haftmann@51126: where
haftmann@51126:   "yield xq = (case list_of_lazy_sequence xq of
haftmann@51126:     [] \<Rightarrow> None
haftmann@51126:   | x # xs \<Rightarrow> Some (x, lazy_sequence_of_list xs))" 
haftmann@51126: 
haftmann@51126: lemma yield_Seq [simp, code]:
haftmann@51126:   "yield (Lazy_Sequence f) = f ()"
haftmann@51126:   by (cases "f ()") (simp_all add: yield_def split_def)
haftmann@51126: 
blanchet@55413: lemma case_yield_eq [simp]: "case_option g h (yield xq) =
blanchet@55413:   case_list g (\<lambda>x. curry h x \<circ> lazy_sequence_of_list) (list_of_lazy_sequence xq)"
haftmann@51126:   by (cases "list_of_lazy_sequence xq") (simp_all add: yield_def)
bulwahn@34948: 
blanchet@56846: lemma size_lazy_sequence_code [code]:
blanchet@56846:   "size_lazy_sequence s xq = (case yield xq of
haftmann@51126:     None \<Rightarrow> 1
blanchet@56846:   | Some (x, xq') \<Rightarrow> Suc (s x + size_lazy_sequence s xq'))"
blanchet@56846:   by (cases "list_of_lazy_sequence xq") (simp_all add: size_lazy_sequence_eq)
bulwahn@34948: 
haftmann@51126: lemma equal_lazy_sequence_code [code]:
haftmann@51126:   "HOL.equal xq yq = (case (yield xq, yield yq) of
haftmann@51126:     (None, None) \<Rightarrow> True
haftmann@51126:   | (Some (x, xq'), Some (y, yq')) \<Rightarrow> HOL.equal x y \<and> HOL.equal xq yq
haftmann@51126:   | _ \<Rightarrow> False)"
haftmann@51126:   by (simp_all add: lazy_sequence_eq_iff equal_eq split: list.splits)
haftmann@38857: 
haftmann@38857: lemma [code nbe]:
haftmann@38857:   "HOL.equal (x :: 'a lazy_sequence) x \<longleftrightarrow> True"
haftmann@38857:   by (fact equal_refl)
bulwahn@34948: 
bulwahn@34948: definition empty :: "'a lazy_sequence"
bulwahn@34948: where
haftmann@51126:   "empty = lazy_sequence_of_list []"
bulwahn@34948: 
haftmann@51126: lemma list_of_lazy_sequence_empty [simp]:
haftmann@51126:   "list_of_lazy_sequence empty = []"
haftmann@51126:   by (simp add: empty_def)
bulwahn@34948: 
haftmann@51126: lemma empty_code [code]:
haftmann@51126:   "empty = Lazy_Sequence (\<lambda>_. None)"
haftmann@51126:   by (simp add: lazy_sequence_eq_iff)
bulwahn@34948: 
haftmann@51126: definition single :: "'a \<Rightarrow> 'a lazy_sequence"
haftmann@51126: where
haftmann@51126:   "single x = lazy_sequence_of_list [x]"
bulwahn@34948: 
haftmann@51126: lemma list_of_lazy_sequence_single [simp]:
haftmann@51126:   "list_of_lazy_sequence (single x) = [x]"
haftmann@51126:   by (simp add: single_def)
haftmann@51126: 
haftmann@51126: lemma single_code [code]:
haftmann@51126:   "single x = Lazy_Sequence (\<lambda>_. Some (x, empty))"
haftmann@51126:   by (simp add: lazy_sequence_eq_iff)
haftmann@51126: 
haftmann@51126: definition append :: "'a lazy_sequence \<Rightarrow> 'a lazy_sequence \<Rightarrow> 'a lazy_sequence"
bulwahn@34948: where
haftmann@51126:   "append xq yq = lazy_sequence_of_list (list_of_lazy_sequence xq @ list_of_lazy_sequence yq)"
haftmann@51126: 
haftmann@51126: lemma list_of_lazy_sequence_append [simp]:
haftmann@51126:   "list_of_lazy_sequence (append xq yq) = list_of_lazy_sequence xq @ list_of_lazy_sequence yq"
haftmann@51126:   by (simp add: append_def)
bulwahn@34948: 
haftmann@51126: lemma append_code [code]:
haftmann@51126:   "append xq yq = Lazy_Sequence (\<lambda>_. case yield xq of
haftmann@51126:     None \<Rightarrow> yield yq
haftmann@51126:   | Some (x, xq') \<Rightarrow> Some (x, append xq' yq))"
haftmann@51126:   by (simp_all add: lazy_sequence_eq_iff split: list.splits)
haftmann@51126: 
haftmann@51126: definition map :: "('a \<Rightarrow> 'b) \<Rightarrow> 'a lazy_sequence \<Rightarrow> 'b lazy_sequence"
bulwahn@34948: where
haftmann@51126:   "map f xq = lazy_sequence_of_list (List.map f (list_of_lazy_sequence xq))"
haftmann@51126: 
haftmann@51126: lemma list_of_lazy_sequence_map [simp]:
haftmann@51126:   "list_of_lazy_sequence (map f xq) = List.map f (list_of_lazy_sequence xq)"
haftmann@51126:   by (simp add: map_def)
haftmann@51126: 
haftmann@51126: lemma map_code [code]:
haftmann@51126:   "map f xq =
blanchet@55466:     Lazy_Sequence (\<lambda>_. map_option (\<lambda>(x, xq'). (f x, map f xq')) (yield xq))"
haftmann@51126:   by (simp_all add: lazy_sequence_eq_iff split: list.splits)
haftmann@51126: 
haftmann@51126: definition flat :: "'a lazy_sequence lazy_sequence \<Rightarrow> 'a lazy_sequence"
haftmann@51126: where
haftmann@51126:   "flat xqq = lazy_sequence_of_list (concat (List.map list_of_lazy_sequence (list_of_lazy_sequence xqq)))"
bulwahn@34948: 
haftmann@51126: lemma list_of_lazy_sequence_flat [simp]:
haftmann@51126:   "list_of_lazy_sequence (flat xqq) = concat (List.map list_of_lazy_sequence (list_of_lazy_sequence xqq))"
haftmann@51126:   by (simp add: flat_def)
bulwahn@34948: 
haftmann@51126: lemma flat_code [code]:
haftmann@51126:   "flat xqq = Lazy_Sequence (\<lambda>_. case yield xqq of
haftmann@51126:     None \<Rightarrow> None
haftmann@51126:   | Some (xq, xqq') \<Rightarrow> yield (append xq (flat xqq')))"
haftmann@51126:   by (simp add: lazy_sequence_eq_iff split: list.splits)
haftmann@51126: 
haftmann@51126: definition bind :: "'a lazy_sequence \<Rightarrow> ('a \<Rightarrow> 'b lazy_sequence) \<Rightarrow> 'b lazy_sequence"
bulwahn@34948: where
haftmann@51126:   "bind xq f = flat (map f xq)"
bulwahn@34948: 
haftmann@51126: definition if_seq :: "bool \<Rightarrow> unit lazy_sequence"
bulwahn@34948: where
bulwahn@34948:   "if_seq b = (if b then single () else empty)"
bulwahn@34948: 
haftmann@51126: definition those :: "'a option lazy_sequence \<Rightarrow> 'a lazy_sequence option"
bulwahn@36049: where
blanchet@55466:   "those xq = map_option lazy_sequence_of_list (List.those (list_of_lazy_sequence xq))"
haftmann@51126:   
haftmann@51143: function iterate_upto :: "(natural \<Rightarrow> 'a) \<Rightarrow> natural \<Rightarrow> natural \<Rightarrow> 'a lazy_sequence"
haftmann@51126: where
haftmann@51126:   "iterate_upto f n m =
haftmann@51126:     Lazy_Sequence (\<lambda>_. if n > m then None else Some (f n, iterate_upto f (n + 1) m))"
haftmann@51126:   by pat_completeness auto
bulwahn@36049: 
haftmann@51143: termination by (relation "measure (\<lambda>(f, n, m). nat_of_natural (m + 1 - n))")
haftmann@51143:   (auto simp add: less_natural_def)
bulwahn@36049: 
haftmann@51126: definition not_seq :: "unit lazy_sequence \<Rightarrow> unit lazy_sequence"
bulwahn@34948: where
haftmann@51126:   "not_seq xq = (case yield xq of
haftmann@51126:     None \<Rightarrow> single ()
haftmann@51126:   | Some ((), xq) \<Rightarrow> empty)"
bulwahn@34948: 
haftmann@51126:   
haftmann@51126: subsection {* Code setup *}
bulwahn@34948: 
haftmann@36533: code_reflect Lazy_Sequence
haftmann@36533:   datatypes lazy_sequence = Lazy_Sequence
haftmann@51126: 
haftmann@51126: ML {*
haftmann@51126: signature LAZY_SEQUENCE =
haftmann@51126: sig
haftmann@51126:   datatype 'a lazy_sequence = Lazy_Sequence of (unit -> ('a * 'a Lazy_Sequence.lazy_sequence) option)
haftmann@51126:   val map: ('a -> 'b) -> 'a lazy_sequence -> 'b lazy_sequence
haftmann@51126:   val yield: 'a lazy_sequence -> ('a * 'a lazy_sequence) option
haftmann@51126:   val yieldn: int -> 'a lazy_sequence -> 'a list * 'a lazy_sequence
haftmann@51126: end;
haftmann@51126: 
haftmann@51126: structure Lazy_Sequence : LAZY_SEQUENCE =
haftmann@51126: struct
haftmann@51126: 
haftmann@51126: datatype lazy_sequence = datatype Lazy_Sequence.lazy_sequence;
haftmann@51126: 
haftmann@51126: fun map f = @{code Lazy_Sequence.map} f;
haftmann@51126: 
haftmann@51126: fun yield P = @{code Lazy_Sequence.yield} P;
haftmann@51126: 
haftmann@51126: fun yieldn k = Predicate.anamorph yield k;
haftmann@51126: 
haftmann@51126: end;
haftmann@51126: *}
haftmann@51126: 
bulwahn@34948: 
bulwahn@40051: subsection {* Generator Sequences *}
bulwahn@40051: 
bulwahn@40051: subsubsection {* General lazy sequence operation *}
bulwahn@40051: 
haftmann@51126: definition product :: "'a lazy_sequence \<Rightarrow> 'b lazy_sequence \<Rightarrow> ('a \<times> 'b) lazy_sequence"
bulwahn@40051: where
haftmann@51126:   "product s1 s2 = bind s1 (\<lambda>a. bind s2 (\<lambda>b. single (a, b)))"
bulwahn@40051: 
bulwahn@40051: 
hoelzl@40056: subsubsection {* Small lazy typeclasses *}
bulwahn@40051: 
bulwahn@40051: class small_lazy =
haftmann@51143:   fixes small_lazy :: "natural \<Rightarrow> 'a lazy_sequence"
bulwahn@40051: 
bulwahn@40051: instantiation unit :: small_lazy
bulwahn@40051: begin
bulwahn@40051: 
haftmann@51126: definition "small_lazy d = single ()"
bulwahn@40051: 
bulwahn@40051: instance ..
bulwahn@40051: 
bulwahn@40051: end
bulwahn@40051: 
bulwahn@40051: instantiation int :: small_lazy
bulwahn@40051: begin
bulwahn@40051: 
bulwahn@40051: text {* maybe optimise this expression -> append (single x) xs == cons x xs 
bulwahn@40051: Performance difference? *}
bulwahn@40051: 
haftmann@51126: function small_lazy' :: "int \<Rightarrow> int \<Rightarrow> int lazy_sequence"
haftmann@51126: where
haftmann@51126:   "small_lazy' d i = (if d < i then empty
haftmann@51126:     else append (single i) (small_lazy' d (i + 1)))"
haftmann@51126:     by pat_completeness auto
bulwahn@40051: 
bulwahn@40051: termination 
bulwahn@40051:   by (relation "measure (%(d, i). nat (d + 1 - i))") auto
bulwahn@40051: 
haftmann@51126: definition
haftmann@51143:   "small_lazy d = small_lazy' (int (nat_of_natural d)) (- (int (nat_of_natural d)))"
bulwahn@40051: 
bulwahn@40051: instance ..
bulwahn@40051: 
bulwahn@40051: end
bulwahn@40051: 
bulwahn@40051: instantiation prod :: (small_lazy, small_lazy) small_lazy
bulwahn@40051: begin
bulwahn@40051: 
bulwahn@40051: definition
bulwahn@40051:   "small_lazy d = product (small_lazy d) (small_lazy d)"
bulwahn@40051: 
bulwahn@40051: instance ..
bulwahn@40051: 
bulwahn@40051: end
bulwahn@40051: 
bulwahn@40051: instantiation list :: (small_lazy) small_lazy
bulwahn@40051: begin
bulwahn@40051: 
haftmann@51143: fun small_lazy_list :: "natural \<Rightarrow> 'a list lazy_sequence"
bulwahn@40051: where
haftmann@51126:   "small_lazy_list d = append (single [])
haftmann@51126:     (if d > 0 then bind (product (small_lazy (d - 1))
haftmann@51126:       (small_lazy (d - 1))) (\<lambda>(x, xs). single (x # xs)) else empty)"
bulwahn@40051: 
bulwahn@40051: instance ..
bulwahn@40051: 
bulwahn@40051: end
bulwahn@40051: 
huffman@36902: subsection {* With Hit Bound Value *}
bulwahn@36030: text {* assuming in negative context *}
bulwahn@36030: 
bulwahn@42163: type_synonym 'a hit_bound_lazy_sequence = "'a option lazy_sequence"
bulwahn@36030: 
bulwahn@36030: definition hit_bound :: "'a hit_bound_lazy_sequence"
bulwahn@36030: where
haftmann@51126:   "hit_bound = Lazy_Sequence (\<lambda>_. Some (None, empty))"
bulwahn@36030: 
haftmann@51126: lemma list_of_lazy_sequence_hit_bound [simp]:
haftmann@51126:   "list_of_lazy_sequence hit_bound = [None]"
haftmann@51126:   by (simp add: hit_bound_def)
haftmann@51126:   
haftmann@51126: definition hb_single :: "'a \<Rightarrow> 'a hit_bound_lazy_sequence"
bulwahn@36030: where
haftmann@51126:   "hb_single x = Lazy_Sequence (\<lambda>_. Some (Some x, empty))"
bulwahn@36030: 
haftmann@51126: definition hb_map :: "('a \<Rightarrow> 'b) \<Rightarrow> 'a hit_bound_lazy_sequence \<Rightarrow> 'b hit_bound_lazy_sequence"
bulwahn@36030: where
blanchet@55466:   "hb_map f xq = map (map_option f) xq"
haftmann@51126: 
haftmann@51126: lemma hb_map_code [code]:
haftmann@51126:   "hb_map f xq =
blanchet@55466:     Lazy_Sequence (\<lambda>_. map_option (\<lambda>(x, xq'). (map_option f x, hb_map f xq')) (yield xq))"
blanchet@55466:   using map_code [of "map_option f" xq] by (simp add: hb_map_def)
bulwahn@36030: 
haftmann@51126: definition hb_flat :: "'a hit_bound_lazy_sequence hit_bound_lazy_sequence \<Rightarrow> 'a hit_bound_lazy_sequence"
haftmann@51126: where
haftmann@51126:   "hb_flat xqq = lazy_sequence_of_list (concat
blanchet@55466:     (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)))"
bulwahn@36030: 
haftmann@51126: lemma list_of_lazy_sequence_hb_flat [simp]:
haftmann@51126:   "list_of_lazy_sequence (hb_flat xqq) =
blanchet@55466:     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))"
haftmann@51126:   by (simp add: hb_flat_def)
bulwahn@36030: 
haftmann@51126: lemma hb_flat_code [code]:
haftmann@51126:   "hb_flat xqq = Lazy_Sequence (\<lambda>_. case yield xqq of
haftmann@51126:     None \<Rightarrow> None
haftmann@51126:   | Some (xq, xqq') \<Rightarrow> yield
haftmann@51126:      (append (case xq of None \<Rightarrow> hit_bound | Some xq \<Rightarrow> xq) (hb_flat xqq')))"
haftmann@51126:   by (simp add: lazy_sequence_eq_iff split: list.splits option.splits)
bulwahn@36030: 
haftmann@51126: definition hb_bind :: "'a hit_bound_lazy_sequence \<Rightarrow> ('a \<Rightarrow> 'b hit_bound_lazy_sequence) \<Rightarrow> 'b hit_bound_lazy_sequence"
bulwahn@36030: where
haftmann@51126:   "hb_bind xq f = hb_flat (hb_map f xq)"
bulwahn@36030: 
haftmann@51126: definition hb_if_seq :: "bool \<Rightarrow> unit hit_bound_lazy_sequence"
bulwahn@36030: where
bulwahn@36030:   "hb_if_seq b = (if b then hb_single () else empty)"
bulwahn@36030: 
haftmann@51126: definition hb_not_seq :: "unit hit_bound_lazy_sequence \<Rightarrow> unit lazy_sequence"
bulwahn@36030: where
haftmann@51126:   "hb_not_seq xq = (case yield xq of
haftmann@51126:     None \<Rightarrow> single ()
haftmann@51126:   | Some (x, xq) \<Rightarrow> empty)"
bulwahn@36030: 
haftmann@51126: hide_const (open) yield empty single append flat map bind
haftmann@51126:   if_seq those iterate_upto not_seq product
haftmann@51126: 
haftmann@51126: hide_fact (open) yield_def empty_def single_def append_def flat_def map_def bind_def
haftmann@51126:   if_seq_def those_def not_seq_def product_def 
bulwahn@34948: 
bulwahn@34948: end