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_map⋅f⋅⊥ = ⊥"
  "llist_map⋅f⋅lnil = lnil"
  "llist_map⋅f⋅(x :@ xs) = f⋅x :@ llist_map⋅f⋅xs"
    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_case⋅g⋅h⋅xxs) = llist_case⋅(f⋅g)⋅(Λ x xs. f⋅(h⋅x⋅xs))⋅xxs"
  by (cases xxs) simp_all

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

fixrec lappend :: "'a llist → 'a llist → 'a llist"
where
  "lappend⋅lnil⋅ys = ys"
| "lappend⋅(x :@ xs)⋅ys = x :@ (lappend⋅xs⋅ys)"

abbreviation
  lappend_syn :: "'a llist ⇒ 'a llist ⇒ 'a llist" (infixr ":++" 65) where
  "xs :++ ys ≡ lappend⋅xs⋅ys"

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]: "lappend⋅lnil = 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
  "lconcat⋅lnil = lnil"
| "lconcat⋅(x :@ xs) = x :++ lconcat⋅xs"

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

fixrec lall :: "('a → tr) → 'a llist → tr"
where
  "lall⋅p⋅lnil = TT"
| "lall⋅p⋅(x :@ xs) = (p⋅x andalso lall⋅p⋅xs)"

lemma lall_strict[simp]: "lall⋅p⋅⊥ = ⊥"
  by fixrec_simp

fixrec lfilter :: "('a → tr) → 'a llist → 'a llist"
where
  "lfilter⋅p⋅lnil = lnil"
| "lfilter⋅p⋅(x :@ xs) = If p⋅x then x :@ lfilter⋅p⋅xs else lfilter⋅p⋅xs"

lemma lfilter_strict[simp]: "lfilter⋅p⋅⊥ = ⊥"
  by fixrec_simp

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

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

lemma filter_filter: "lfilter⋅p⋅(lfilter⋅q⋅xs) = lfilter⋅(Λ x. q⋅x andalso p⋅x)⋅xs"
proof(induct xs)
  fix a l assume "lfilter⋅p⋅(lfilter⋅q⋅l) = lfilter⋅(Λ(x::'a). q⋅x andalso p⋅x)⋅l"
  thus "lfilter⋅p⋅(lfilter⋅q⋅(a :@ l)) = lfilter⋅(Λ(x::'a). q⋅x andalso p⋅x)⋅(a :@ l)"
    by (cases "q⋅a" rule: trE, simp_all)
qed simp_all

fixrec ldropWhile :: "('a → tr) → 'a llist → 'a llist"
where
  "ldropWhile⋅p⋅lnil = lnil"
| "ldropWhile⋅p⋅(x :@ xs) = If p⋅x then ldropWhile⋅p⋅xs else x :@ xs"

lemma ldropWhile_strict[simp]: "ldropWhile⋅p⋅⊥ = ⊥"
  by fixrec_simp

lemma ldropWhile_lnil: "(ldropWhile⋅p⋅xs = lnil) = (lall⋅p⋅xs = TT)"
proof(induct xs)
  fix a l assume "(ldropWhile⋅p⋅l = lnil) = (lall⋅p⋅l = TT)"
  thus "(ldropWhile⋅p⋅(a :@ l) = lnil) = (lall⋅p⋅(a :@ l) = TT)"
    by (cases "p⋅a" rule: trE, simp_all)
qed simp_all

fixrec literate :: "('a → 'a) → 'a → 'a llist"
where
  "literate⋅f⋅x = x :@ literate⋅f⋅(f⋅x)"

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
  "lmember⋅eq⋅x⋅lnil = FF"
| "lmember⋅eq⋅x⋅(lcons⋅y⋅ys) = (lmember⋅eq⋅x⋅ys orelse eq⋅y⋅x)"

lemma lmember_strict[simp]: "lmember⋅eq⋅x⋅⊥ = ⊥"
  by fixrec_simp

fixrec llength :: "'a llist → Nat"
where
  "llength⋅lnil = 0"
| "llength⋅(lcons⋅x⋅xs) = 1 + llength⋅xs"

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

fixrec lmap :: "('a → 'b) → 'a llist → 'b llist"
where
  "lmap⋅f⋅lnil = lnil"
| "lmap⋅f⋅(x :@ xs) = f⋅x :@ lmap⋅f⋅xs"

lemma lmap_strict[simp]: "lmap⋅f⋅⊥ = ⊥"
  by fixrec_simp

lemma lmap_lmap:
  "lmap⋅f⋅(lmap⋅g⋅xs) = 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 lmap⋅f)"

lemma lconcatMap_comp_simps[simp]:
  "lconcatMap⋅f⋅⊥ = ⊥"
  "lconcatMap⋅f⋅lnil = lnil"
  "lconcatMap⋅f⋅(x :@ xs) = f⋅x :++ lconcatMap⋅f⋅xs"
  by (simp_all add: lconcatMap_def)

lemma lconcatMap_lsingleton[simp]:
  "lconcatMap⋅lsingleton⋅x = 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
  "lzipWith0⋅f⋅(a :@ as)⋅(b :@ bs) = f⋅a⋅b :@ lzipWith0⋅f⋅as⋅bs"
| "lzipWith0⋅f⋅lnil⋅lnil = lnil"

lemma lzipWith0_stricts [simp]:
  "lzipWith0⋅f⋅⊥⋅ys = ⊥"
  "lzipWith0⋅f⋅lnil⋅⊥ = ⊥"
  "lzipWith0⋅f⋅(x :@ xs)⋅⊥ = ⊥"
  by fixrec_simp+

lemma lzipWith0_undefs [simp]:
  "lzipWith0⋅f⋅lnil⋅(y :@ ys) = ⊥"
  "lzipWith0⋅f⋅(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
  "lzipWith⋅f⋅(a :@ as)⋅(b :@ bs) = f⋅a⋅b :@ lzipWith⋅f⋅as⋅bs"
| (unchecked) "lzipWith⋅f⋅xs⋅ys = lnil"

lemma lzipWith_simps [simp]:
  "lzipWith⋅f⋅(x :@ xs)⋅(y :@ ys) = f⋅x⋅y :@ lzipWith⋅f⋅xs⋅ys"
  "lzipWith⋅f⋅(x :@ xs)⋅lnil = lnil"
  "lzipWith⋅f⋅lnil⋅(y :@ ys) = lnil"
  "lzipWith⋅f⋅lnil⋅lnil = lnil"
  by fixrec_simp+

lemma lzipWith_stricts [simp]:
  "lzipWith⋅f⋅⊥⋅ys = ⊥"
  "lzipWith⋅f⋅(x :@ xs)⋅⊥ = ⊥"
  by fixrec_simp+

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

lemma lmap_lappend_dist:
  "lmap⋅f⋅(xs :++ ys) = lmap⋅f⋅xs :++ lmap⋅f⋅ys"
  by (induct xs) simp_all

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

lemma lconcatMap_assoc:
  "lconcatMap⋅h⋅(lconcatMap⋅g⋅f) = lconcatMap⋅(Λ v. lconcatMap⋅h⋅(g⋅v))⋅f"
  by (induct f) (simp_all add: lmap_lappend_dist lconcat_lappend_dist lconcatMap_def)

lemma lconcatMap_lappend_dist:
  "lconcatMap⋅f⋅(xs :++ ys) = lconcatMap⋅f⋅xs :++ lconcatMap⋅f⋅ys"
  unfolding lconcatMap_def by (simp add: lconcat_lappend_dist lmap_lappend_dist)

(* The following avoid some case_tackery. *)

lemma lmap_not_bottoms[simp]:
  "x ≠ ⊥ ⟹ lmap⋅f⋅x ≠ ⊥"
  by (cases x) simp_all

lemma lsingleton_not_bottom[simp]:
  "lsingleton⋅x ≠ ⊥"
  by simp

lemma lappend_not_bottom[simp]:
  "⟦ xs ≠ ⊥; xs = lnil ⟹ ys ≠ ⊥ ⟧ ⟹ xs :++ ys ≠ ⊥"
  apply (cases xs)
  apply simp_all
  done

default_sort "domain"

(*<*)
end
(*>*)