Theory LList

(*
 * Lazy lists.
 * (C)opyright 2009-2011, Peter Gammie, peteg42 at gmail.com.
 * License: BSD
 *)

(*<*)
theory LList
imports
  HOLCF
  Nats
begin
(*>*)

section‹The fully-lazy list type.›

text‹The list can contain anything that is a predomain.›

default_sort predomain

domain 'a llist =
    lnil ("lnil")
  | lcons (lazy "'a") (lazy "'a llist") (infixr ":@" 65)

(*<*)
(* Why aren't these in the library? *)

lemma llist_map_eval_simps[simp]:
  "llist_mapf = "
  "llist_mapflnil = lnil"
  "llist_mapf(x :@ xs) = fx :@ llist_mapfxs"
    apply (subst llist_map_unfold)
    apply simp
   apply (subst llist_map_unfold)
   apply (simp add: lnil_def)
  apply (subst llist_map_unfold)
  apply (simp add: lcons_def)
  done
(*>*)

lemma llist_case_distr_strict:
  "f =   f(llist_caseghxxs) = llist_case(fg)(Λ x xs. f(hxxs))xxs"
  by (cases xxs) simp_all

fixrec lsingleton :: "('a::predomain)  'a llist"
where
  "lsingletonx = x :@ lnil"

fixrec lappend :: "'a llist  'a llist  'a llist"
where
  "lappendlnilys = ys"
| "lappend(x :@ xs)ys = x :@ (lappendxsys)"

abbreviation
  lappend_syn :: "'a llist  'a llist  'a llist" (infixr ":++" 65) where
  "xs :++ ys  lappendxsys"

lemma lappend_strict': "lappend = (Λ a. )"
  by fixrec_simp

text‹This gives us that @{thm lappend_strict'}.›

text ‹This is where we use @{thm inst_cfun_pcpo}
lemma lappend_strict[simp]: "lappend = "
  by (rule cfun_eqI) (simp add: lappend_strict')

lemma lappend_assoc: "(xs :++ ys) :++ zs = xs :++ (ys :++ zs)"
  by (induct xs, simp_all)

lemma lappend_lnil_id_left[simp]: "lappendlnil = ID"
  by (rule cfun_eqI) simp

lemma lappend_lnil_id_right[simp]: "xs :++ lnil = xs"
  by (induct xs) simp_all

fixrec lconcat :: "'a llist llist  'a llist"
where
  "lconcatlnil = lnil"
| "lconcat(x :@ xs) = x :++ lconcatxs"

lemma lconcat_strict[simp]: "lconcat = "
  by fixrec_simp

fixrec lall :: "('a  tr)  'a llist  tr"
where
  "lallplnil = TT"
| "lallp(x :@ xs) = (px andalso lallpxs)"

lemma lall_strict[simp]: "lallp = "
  by fixrec_simp

fixrec lfilter :: "('a  tr)  'a llist  'a llist"
where
  "lfilterplnil = lnil"
| "lfilterp(x :@ xs) = If px then x :@ lfilterpxs else lfilterpxs"

lemma lfilter_strict[simp]: "lfilterp = "
  by fixrec_simp

lemma lfilter_const_true: "lfilter(Λ x. TT)xs = xs"
  by (induct xs, simp_all)

lemma lfilter_lnil: "(lfilterpxs = lnil) = (lall(neg oo p)xs = TT)"
proof(induct xs)
  fix a l assume indhyp: "(lfilterpl = lnil) = (lall(Tr.neg oo p)l = TT)"
  thus "(lfilterp(a :@ l) = lnil) = (lall(Tr.neg oo p)(a :@ l) = TT)"
    by (cases "pa" rule: trE, simp_all)
qed simp_all

lemma filter_filter: "lfilterp(lfilterqxs) = lfilter(Λ x. qx andalso px)xs"
proof(induct xs)
  fix a l assume "lfilterp(lfilterql) = lfilter(Λ(x::'a). qx andalso px)l"
  thus "lfilterp(lfilterq(a :@ l)) = lfilter(Λ(x::'a). qx andalso px)(a :@ l)"
    by (cases "qa" rule: trE, simp_all)
qed simp_all

fixrec ldropWhile :: "('a  tr)  'a llist  'a llist"
where
  "ldropWhileplnil = lnil"
| "ldropWhilep(x :@ xs) = If px then ldropWhilepxs else x :@ xs"

lemma ldropWhile_strict[simp]: "ldropWhilep = "
  by fixrec_simp

lemma ldropWhile_lnil: "(ldropWhilepxs = lnil) = (lallpxs = TT)"
proof(induct xs)
  fix a l assume "(ldropWhilepl = lnil) = (lallpl = TT)"
  thus "(ldropWhilep(a :@ l) = lnil) = (lallp(a :@ l) = TT)"
    by (cases "pa" rule: trE, simp_all)
qed simp_all

fixrec literate :: "('a  'a)  'a  'a llist"
where
  "literatefx = x :@ literatef(fx)"

declare literate.simps[simp del]

text‹This order of tests is convenient for the nub proof. I can
imagine the other would be convenient for other proofs...›

fixrec lmember :: "('a  'a  tr)  'a  'a llist  tr"
where
  "lmembereqxlnil = FF"
| "lmembereqx(lconsyys) = (lmembereqxys orelse eqyx)"

lemma lmember_strict[simp]: "lmembereqx = "
  by fixrec_simp

fixrec llength :: "'a llist  Nat"
where
  "llengthlnil = 0"
| "llength(lconsxxs) = 1 + llengthxs"

lemma llength_strict[simp]: "llength = "
  by fixrec_simp

fixrec lmap :: "('a  'b)  'a llist  'b llist"
where
  "lmapflnil = lnil"
| "lmapf(x :@ xs) = fx :@ lmapfxs"

lemma lmap_strict[simp]: "lmapf = "
  by fixrec_simp

lemma lmap_lmap:
  "lmapf(lmapgxs) = lmap(f oo g)xs"
  by (induct xs) simp_all

text ‹The traditional list monad uses lconcatMap as its bind.›

definition
  "lconcatMap  (Λ f. lconcat oo lmapf)"

lemma lconcatMap_comp_simps[simp]:
  "lconcatMapf = "
  "lconcatMapflnil = lnil"
  "lconcatMapf(x :@ xs) = fx :++ lconcatMapfxs"
  by (simp_all add: lconcatMap_def)

lemma lconcatMap_lsingleton[simp]:
  "lconcatMaplsingletonx = x"
  by (induct x) (simp_all add: lconcatMap_def)

text‹This @{term "zipWith"} function is only fully defined if the
lists have the same length.›

fixrec lzipWith0 :: "('a  'b  'c)  'a llist  'b llist  'c llist"
where
  "lzipWith0f(a :@ as)(b :@ bs) = fab :@ lzipWith0fasbs"
| "lzipWith0flnillnil = lnil"

lemma lzipWith0_stricts [simp]:
  "lzipWith0fys = "
  "lzipWith0flnil = "
  "lzipWith0f(x :@ xs) = "
  by fixrec_simp+

lemma lzipWith0_undefs [simp]:
  "lzipWith0flnil(y :@ ys) = "
  "lzipWith0f(x :@ xs)lnil = "
  by fixrec_simp+

text‹This @{term "zipWith"} function follows Haskell's in being more
permissive: zipping uneven lists results in a list as long as the
shortest one. This is what the backtracking monad expects.›

fixrec lzipWith :: "('a  'b  'c)  'a llist  'b llist  'c llist"
where
  "lzipWithf(a :@ as)(b :@ bs) = fab :@ lzipWithfasbs"
| (unchecked) "lzipWithfxsys = lnil"

lemma lzipWith_simps [simp]:
  "lzipWithf(x :@ xs)(y :@ ys) = fxy :@ lzipWithfxsys"
  "lzipWithf(x :@ xs)lnil = lnil"
  "lzipWithflnil(y :@ ys) = lnil"
  "lzipWithflnillnil = lnil"
  by fixrec_simp+

lemma lzipWith_stricts [simp]:
  "lzipWithfys = "
  "lzipWithf(x :@ xs) = "
  by fixrec_simp+

text‹Homomorphism properties, see Bird's life's work.›

lemma lmap_lappend_dist:
  "lmapf(xs :++ ys) = lmapfxs :++ lmapfys"
  by (induct xs) simp_all

lemma lconcat_lappend_dist:
  "lconcat(xs :++ ys) = lconcatxs :++ lconcatys"
  by (induct xs) (simp_all add: lappend_assoc)

lemma lconcatMap_assoc:
  "lconcatMaph(lconcatMapgf) = lconcatMap(Λ v. lconcatMaph(gv))f"
  by (induct f) (simp_all add: lmap_lappend_dist lconcat_lappend_dist lconcatMap_def)

lemma lconcatMap_lappend_dist:
  "lconcatMapf(xs :++ ys) = lconcatMapfxs :++ lconcatMapfys"
  unfolding lconcatMap_def by (simp add: lconcat_lappend_dist lmap_lappend_dist)

(* The following avoid some case_tackery. *)

lemma lmap_not_bottoms[simp]:
  "x    lmapfx  "
  by (cases x) simp_all

lemma lsingleton_not_bottom[simp]:
  "lsingletonx  "
  by simp

lemma lappend_not_bottom[simp]:
  " xs  ; xs = lnil  ys     xs :++ ys  "
  apply (cases xs)
  apply simp_all
  done

default_sort "domain"

(*<*)
end
(*>*)