# Theory Coinductive_List

```(*  Title:      Coinductive_List.thy
Author:     Andreas Lochbihler
*)

section ‹Coinductive lists and their operations›

theory Coinductive_List
imports
"HOL-Library.Infinite_Set"
"HOL-Library.Sublist"
"HOL-Library.Simps_Case_Conv"
Coinductive_Nat
begin

subsection ‹Auxiliary lemmata›

lemma funpow_Suc_conv [simp]: "(Suc ^^ n) m = m + n"
by(induct n arbitrary: m) simp_all

lemma wlog_linorder_le [consumes 0, case_names le symmetry]:
assumes le: "⋀a b :: 'a :: linorder. a ≤ b ⟹ P a b"
and sym: "P b a ⟹ P a b"
shows "P a b"
proof(cases "a ≤ b")
case True thus ?thesis by(rule le)
next
case False
hence "b ≤ a" by simp
hence "P b a" by(rule le)
thus ?thesis by(rule sym)
qed

subsection ‹Type definition›

codatatype (lset: 'a) llist =
lnull: LNil
| LCons (lhd: 'a) (ltl: "'a llist")
for
map: lmap
rel: llist_all2
where
"lhd LNil = undefined"
| "ltl LNil = LNil"

text ‹
Coiterator setup.
›

primcorec unfold_llist :: "('a ⇒ bool) ⇒ ('a ⇒ 'b) ⇒ ('a ⇒ 'a) ⇒ 'a ⇒ 'b llist" where
"p a ⟹ unfold_llist p g21 g22 a = LNil" |
"_ ⟹ unfold_llist p g21 g22 a = LCons (g21 a) (unfold_llist p g21 g22 (g22 a))"

declare
unfold_llist.ctr(1) [simp]
llist.corec(1) [simp]

text ‹
The following setup should be done by the BNF package.
›

text ‹congruence rule›

declare llist.map_cong [cong]

text ‹Code generator setup›

lemma corec_llist_never_stop: "corec_llist IS_LNIL LHD (λ_. False) MORE LTL x = unfold_llist IS_LNIL LHD LTL x"
by(coinduction arbitrary: x) auto

lemma eq_LConsD: "xs = LCons y ys ⟹ xs ≠ LNil ∧ lhd xs = y ∧ ltl xs = ys"
by auto

lemma
shows LNil_eq_lmap: "LNil = lmap f xs ⟷ xs = LNil"
and lmap_eq_LNil: "lmap f xs = LNil ⟷ xs = LNil"
by(cases xs,simp_all)+

declare llist.map_sel(1)[simp]

lemma ltl_lmap[simp]: "ltl (lmap f xs) = lmap f (ltl xs)"
by(cases xs, simp_all)

declare llist.map_ident[simp]

lemma lmap_eq_LCons_conv:
"lmap f xs = LCons y ys ⟷
(∃x xs'. xs = LCons x xs' ∧ y = f x ∧ ys = lmap f xs')"
by(cases xs)(auto)

lemma lmap_conv_unfold_llist:
"lmap f = unfold_llist (λxs. xs = LNil) (f ∘ lhd) ltl" (is "?lhs = ?rhs")
proof
fix x
show "?lhs x = ?rhs x" by(coinduction arbitrary: x) auto
qed

lemma lmap_unfold_llist:
"lmap f (unfold_llist IS_LNIL LHD LTL b) = unfold_llist IS_LNIL (f ∘ LHD) LTL b"
by(coinduction arbitrary: b) auto

lemma lmap_corec_llist:
"lmap f (corec_llist IS_LNIL LHD endORmore TTL_end TTL_more b) =
corec_llist IS_LNIL (f ∘ LHD) endORmore (lmap f ∘ TTL_end) TTL_more b"
by(coinduction arbitrary: b rule: llist.coinduct_strong) auto

lemma unfold_llist_ltl_unroll:
"unfold_llist IS_LNIL LHD LTL (LTL b) = unfold_llist (IS_LNIL ∘ LTL) (LHD ∘ LTL) LTL b"
by(coinduction arbitrary: b) auto

lemma ltl_unfold_llist:
"ltl (unfold_llist IS_LNIL LHD LTL a) =
(if IS_LNIL a then LNil else unfold_llist IS_LNIL LHD LTL (LTL a))"
by(simp)

lemma unfold_llist_eq_LCons [simp]:
"unfold_llist IS_LNIL LHD LTL b = LCons x xs ⟷
¬ IS_LNIL b ∧ x = LHD b ∧ xs = unfold_llist IS_LNIL LHD LTL (LTL b)"
by(subst unfold_llist.code) auto

lemma unfold_llist_id [simp]: "unfold_llist lnull lhd ltl xs = xs"
by(coinduction arbitrary: xs) simp_all

lemma lset_eq_empty [simp]: "lset xs = {} ⟷ lnull xs"
by(cases xs) simp_all

declare llist.set_sel(1)[simp]

lemma lset_ltl: "lset (ltl xs) ⊆ lset xs"
by(cases xs) auto

lemma in_lset_ltlD: "x ∈ lset (ltl xs) ⟹ x ∈ lset xs"
using lset_ltl[of xs] by auto

text ‹induction rules›

theorem llist_set_induct[consumes 1, case_names find step]:
assumes "x ∈ lset xs" and "⋀xs. ¬ lnull xs ⟹ P (lhd xs) xs"
and "⋀xs y. ⟦¬ lnull xs; y ∈ lset (ltl xs); P y (ltl xs)⟧ ⟹ P y xs"
shows "P x xs"
using assms by(induct)(fastforce simp del: llist.disc(2) iff: llist.disc(2), auto)

text ‹Test quickcheck setup›

lemma "⋀xs. xs = LNil"
quickcheck[random, expect=counterexample]
quickcheck[exhaustive, expect=counterexample]
oops

lemma "LCons x xs = LCons x xs"
quickcheck[narrowing, expect=no_counterexample]
oops

subsection ‹Properties of predefined functions›

lemmas lhd_LCons = llist.sel(1)
lemmas ltl_simps = llist.sel(2,3)

lemmas lhd_LCons_ltl = llist.collapse(2)

lemma lnull_ltlI [simp]: "lnull xs ⟹ lnull (ltl xs)"
unfolding lnull_def by simp

lemma neq_LNil_conv: "xs ≠ LNil ⟷ (∃x xs'. xs = LCons x xs')"
by(cases xs) auto

lemma not_lnull_conv: "¬ lnull xs ⟷ (∃x xs'. xs = LCons x xs')"

lemma lset_LCons:
"lset (LCons x xs) = insert x (lset xs)"
by simp

lemma lset_intros:
"x ∈ lset (LCons x xs)"
"x ∈ lset xs ⟹ x ∈ lset (LCons x' xs)"
by simp_all

lemma lset_cases [elim?]:
assumes "x ∈ lset xs"
obtains xs' where "xs = LCons x xs'"
| x' xs' where "xs = LCons x' xs'" "x ∈ lset xs'"
using assms by(cases xs) auto

lemma lset_induct' [consumes 1, case_names find step]:
assumes major: "x ∈ lset xs"
and 1: "⋀xs. P (LCons x xs)"
and 2: "⋀x' xs. ⟦ x ∈ lset xs; P xs ⟧ ⟹ P (LCons x' xs)"
shows "P xs"
using major apply(induct y≡"x" xs rule: llist_set_induct)
using 1 2 by(auto simp add: not_lnull_conv)

lemma lset_induct [consumes 1, case_names find step, induct set: lset]:
assumes major: "x ∈ lset xs"
and find: "⋀xs. P (LCons x xs)"
and step: "⋀x' xs. ⟦ x ∈ lset xs; x ≠ x'; P xs ⟧ ⟹ P (LCons x' xs)"
shows "P xs"
using major
apply(induct rule: lset_induct')
apply(rule find)
apply(case_tac "x'=x")
done

lemmas lset_LNil = llist.set(1)

lemma lset_lnull: "lnull xs ⟹ lset xs = {}"
by(auto dest: llist.collapse)

text ‹Alternative definition of @{term lset} for nitpick›

inductive lsetp :: "'a llist ⇒ 'a ⇒ bool"
where
"lsetp (LCons x xs) x"
| "lsetp xs x ⟹ lsetp (LCons x' xs) x"

lemma lset_into_lsetp:
"x ∈ lset xs ⟹ lsetp xs x"
by(induct rule: lset_induct)(blast intro: lsetp.intros)+

lemma lsetp_into_lset:
"lsetp xs x ⟹ x ∈ lset xs"
by(induct rule: lsetp.induct)(blast intro: lset_intros)+

lemma lset_eq_lsetp [nitpick_unfold]:
"lset xs = {x. lsetp xs x}"
by(auto intro: lset_into_lsetp dest: lsetp_into_lset)

hide_const (open) lsetp
hide_fact (open) lsetp.intros lsetp.cases lsetp.induct lset_into_lsetp lset_eq_lsetp

text ‹code setup for @{term lset}›

definition gen_lset :: "'a set ⇒ 'a llist ⇒ 'a set"
where "gen_lset A xs = A ∪ lset xs"

lemma gen_lset_code [code]:
"gen_lset A LNil = A"
"gen_lset A (LCons x xs) = gen_lset (insert x A) xs"

lemma lset_code [code]:
"lset = gen_lset {}"

definition lmember :: "'a ⇒ 'a llist ⇒ bool"
where "lmember x xs ⟷ x ∈ lset xs"

lemma lmember_code [code]:
"lmember x LNil ⟷ False"
"lmember x (LCons y ys) ⟷ x = y ∨ lmember x ys"

lemma lset_lmember [code_unfold]:
"x ∈ lset xs ⟷ lmember x xs"

lemmas lset_lmap [simp] = llist.set_map

subsection ‹The subset of finite lazy lists @{term "lfinite"}›

inductive lfinite :: "'a llist ⇒ bool"
where
lfinite_LNil:  "lfinite LNil"
| lfinite_LConsI: "lfinite xs ⟹ lfinite (LCons x xs)"

declare lfinite_LNil [iff]

lemma lnull_imp_lfinite [simp]: "lnull xs ⟹ lfinite xs"
by(auto dest: llist.collapse)

lemma lfinite_LCons [simp]: "lfinite (LCons x xs) = lfinite xs"
by(auto elim: lfinite.cases intro: lfinite_LConsI)

lemma lfinite_ltl [simp]: "lfinite (ltl xs) = lfinite xs"
by(cases xs) simp_all

lemma lfinite_code [code]:
"lfinite LNil = True"
"lfinite (LCons x xs) = lfinite xs"
by simp_all

lemma lfinite_induct [consumes 1, case_names LNil LCons]:
assumes lfinite: "lfinite xs"
and LNil: "⋀xs. lnull xs ⟹ P xs"
and LCons: "⋀xs. ⟦ lfinite xs; ¬ lnull xs; P (ltl xs) ⟧ ⟹ P xs"
shows "P xs"
using lfinite by(induct)(auto intro: LCons LNil)

lemma lfinite_imp_finite_lset:
assumes "lfinite xs"
shows "finite (lset xs)"
using assms by induct auto

subsection ‹Concatenating two lists: @{term "lappend"}›

primcorec lappend :: "'a llist ⇒ 'a llist ⇒ 'a llist"
where
"lappend xs ys = (case xs of LNil ⇒ ys | LCons x xs' ⇒ LCons x (lappend xs' ys))"

simps_of_case lappend_code [code, simp, nitpick_simp]: lappend.code

lemmas lappend_LNil_LNil = lappend_code(1)[where ys = LNil]

lemma lappend_simps [simp]:
shows lhd_lappend: "lhd (lappend xs ys) = (if lnull xs then lhd ys else lhd xs)"
and ltl_lappend: "ltl (lappend xs ys) = (if lnull xs then ltl ys else lappend (ltl xs) ys)"
by(case_tac [!] xs) simp_all

lemma lnull_lappend [simp]:
"lnull (lappend xs ys) ⟷ lnull xs ∧ lnull ys"

lemma lappend_eq_LNil_iff:
"lappend xs ys = LNil ⟷ xs = LNil ∧ ys = LNil"
using lnull_lappend unfolding lnull_def .

lemma LNil_eq_lappend_iff:
"LNil = lappend xs ys ⟷ xs = LNil ∧ ys = LNil"
by(auto dest: sym simp add: lappend_eq_LNil_iff)

lemma lappend_LNil2 [simp]: "lappend xs LNil = xs"
by(coinduction arbitrary: xs) simp_all

lemma shows lappend_lnull1: "lnull xs ⟹ lappend xs ys = ys"
and lappend_lnull2: "lnull ys ⟹ lappend xs ys = xs"
unfolding lnull_def by simp_all

lemma lappend_assoc: "lappend (lappend xs ys) zs = lappend xs (lappend ys zs)"
by(coinduction arbitrary: xs rule: llist.coinduct_strong) auto

lemma lmap_lappend_distrib:
"lmap f (lappend xs ys) = lappend (lmap f xs) (lmap f ys)"
by(coinduction arbitrary: xs rule: llist.coinduct_strong) auto

lemma lappend_snocL1_conv_LCons2:
"lappend (lappend xs (LCons y LNil)) ys = lappend xs (LCons y ys)"

lemma lappend_ltl: "¬ lnull xs ⟹ lappend (ltl xs) ys = ltl (lappend xs ys)"
by simp

lemma lfinite_lappend [simp]:
"lfinite (lappend xs ys) ⟷ lfinite xs ∧ lfinite ys"
(is "?lhs ⟷ ?rhs")
proof
assume ?lhs thus ?rhs
proof(induct zs≡"lappend xs ys" arbitrary: xs ys)
case lfinite_LNil
next
case (lfinite_LConsI zs z)
thus ?case by(cases xs)(cases ys, simp_all)
qed
next
assume ?rhs (is "?xs ∧ ?ys")
then obtain ?xs ?ys ..
thus ?lhs by induct simp_all
qed

lemma lappend_inf: "¬ lfinite xs ⟹ lappend xs ys = xs"
by(coinduction arbitrary: xs) auto

lemma lfinite_lmap [simp]:
"lfinite (lmap f xs) = lfinite xs"
(is "?lhs ⟷ ?rhs")
proof
assume ?lhs
thus ?rhs
by(induct zs≡"lmap f xs" arbitrary: xs rule: lfinite_induct) fastforce+
next
assume ?rhs
thus ?lhs by(induct) simp_all
qed

lemma lset_lappend_lfinite [simp]:
"lfinite xs ⟹ lset (lappend xs ys) = lset xs ∪ lset ys"
by(induct rule: lfinite.induct) auto

lemma lset_lappend: "lset (lappend xs ys) ⊆ lset xs ∪ lset ys"
proof(cases "lfinite xs")
case True
thus ?thesis by simp
next
case False
thus ?thesis by(auto simp add: lappend_inf)
qed

lemma lset_lappend1: "lset xs ⊆ lset (lappend xs ys)"
by(rule subsetI)(erule lset_induct, simp_all)

lemma lset_lappend_conv: "lset (lappend xs ys) = (if lfinite xs then lset xs ∪ lset ys else lset xs)"

lemma in_lset_lappend_iff: "x ∈ lset (lappend xs ys) ⟷ x ∈ lset xs ∨ lfinite xs ∧ x ∈ lset ys"

lemma split_llist_first:
assumes "x ∈ lset xs"
shows "∃ys zs. xs = lappend ys (LCons x zs) ∧ lfinite ys ∧ x ∉ lset ys"
using assms
proof(induct)
case find thus ?case by(auto intro: exI[where x=LNil])
next
case step thus ?case by(fastforce intro: exI[where x="LCons a b" for a b])
qed

lemma split_llist: "x ∈ lset xs ⟹ ∃ys zs. xs = lappend ys (LCons x zs) ∧ lfinite ys"
by(blast dest: split_llist_first)

subsection ‹The prefix ordering on lazy lists: @{term "lprefix"}›

coinductive lprefix :: "'a llist ⇒ 'a llist ⇒ bool" (infix "⊑" 65)
where
LNil_lprefix [simp, intro!]: "LNil ⊑ xs"
| Le_LCons: "xs ⊑ ys ⟹ LCons x xs ⊑ LCons x ys"

lemma lprefixI [consumes 1, case_names lprefix,
case_conclusion lprefix LeLNil LeLCons]:
assumes major: "(xs, ys) ∈ X"
and step:
"⋀xs ys. (xs, ys) ∈ X
⟹ lnull xs ∨ (∃x xs' ys'. xs = LCons x xs' ∧ ys = LCons x ys' ∧
((xs', ys') ∈ X ∨ xs' ⊑ ys'))"
shows "xs ⊑ ys"
using major by(rule lprefix.coinduct)(auto dest: step)

lemma lprefix_coinduct [consumes 1, case_names lprefix, case_conclusion lprefix LNil LCons, coinduct pred: lprefix]:
assumes major: "P xs ys"
and step: "⋀xs ys. P xs ys
⟹ (lnull ys ⟶ lnull xs) ∧
(¬ lnull xs ⟶ ¬ lnull ys ⟶ lhd xs = lhd ys ∧ (P (ltl xs) (ltl ys) ∨ ltl xs ⊑ ltl ys))"
shows "xs ⊑ ys"
proof -
from major have "(xs, ys) ∈ {(xs, ys). P xs ys}" by simp
thus ?thesis
proof(coinduct rule: lprefixI)
case (lprefix xs ys)
hence "P xs ys" by simp
from step[OF this] show ?case
qed
qed

lemma lprefix_refl [intro, simp]: "xs ⊑ xs"
by(coinduction arbitrary: xs) simp_all

lemma lprefix_LNil [simp]: "xs ⊑ LNil ⟷ lnull xs"
unfolding lnull_def by(subst lprefix.simps)simp

lemma lprefix_lnull: "lnull ys ⟹ xs ⊑ ys ⟷ lnull xs"
unfolding lnull_def by auto

lemma lnull_lprefix: "lnull xs ⟹ lprefix xs ys"

lemma lprefix_LCons_conv:
"xs ⊑ LCons y ys ⟷
xs = LNil ∨ (∃xs'. xs = LCons y xs' ∧ xs' ⊑ ys)"
by(subst lprefix.simps) simp

lemma LCons_lprefix_LCons [simp]:
"LCons x xs ⊑ LCons y ys ⟷ x = y ∧ xs ⊑ ys"

lemma LCons_lprefix_conv:
"LCons x xs ⊑ ys ⟷ (∃ys'. ys = LCons x ys' ∧ xs ⊑ ys')"
by(cases ys)(auto)

lemma lprefix_ltlI: "xs ⊑ ys ⟹ ltl xs ⊑ ltl ys"

lemma lprefix_code [code]:
"LNil ⊑ ys ⟷ True"
"LCons x xs ⊑ LNil ⟷ False"
"LCons x xs ⊑ LCons y ys ⟷ x = y ∧ xs ⊑ ys"
by simp_all

lemma lprefix_lhdD: "⟦ xs ⊑ ys; ¬ lnull xs ⟧ ⟹ lhd xs = lhd ys"

lemma lprefix_lnullD: "⟦ xs ⊑ ys; lnull ys ⟧ ⟹ lnull xs"
by(auto elim: lprefix.cases)

lemma lprefix_not_lnullD: "⟦ xs ⊑ ys; ¬ lnull xs ⟧ ⟹ ¬ lnull ys"
by(auto elim: lprefix.cases)

lemma lprefix_expand:
"(¬ lnull xs ⟹ ¬ lnull ys ∧ lhd xs = lhd ys ∧ ltl xs ⊑ ltl ys) ⟹ xs ⊑ ys"
by(cases xs ys rule: llist.exhaust[case_product llist.exhaust])(simp_all)

lemma lprefix_antisym:
"⟦ xs ⊑ ys; ys ⊑ xs ⟧ ⟹ xs = ys"
by(coinduction arbitrary: xs ys)(auto simp add: not_lnull_conv lprefix_lnull)

lemma lprefix_trans [trans]:
"⟦ xs ⊑ ys; ys ⊑ zs ⟧ ⟹ xs ⊑ zs"
by(coinduction arbitrary: xs ys zs)(auto 4 3 dest: lprefix_lnullD lprefix_lhdD intro: lprefix_ltlI)

lemma preorder_lprefix [cont_intro]:
"class.preorder (⊑) (mk_less (⊑))"
by(unfold_locales)(auto simp add: mk_less_def intro: lprefix_trans)

lemma lprefix_lsetD:
assumes "xs ⊑ ys"
shows "lset xs ⊆ lset ys"
proof
fix x
assume "x ∈ lset xs"
thus "x ∈ lset ys" using assms
by(induct arbitrary: ys)(auto simp add: LCons_lprefix_conv)
qed

lemma lprefix_lappend_sameI:
assumes "xs ⊑ ys"
shows "lappend zs xs ⊑ lappend zs ys"
proof(cases "lfinite zs")
case True
thus ?thesis using assms by induct auto

lemma not_lfinite_lprefix_conv_eq:
assumes nfin: "¬ lfinite xs"
shows "xs ⊑ ys ⟷ xs = ys"
proof
assume "xs ⊑ ys"
with nfin show "xs = ys"
by(coinduction arbitrary: xs ys)(auto dest: lprefix_lnullD lprefix_lhdD intro: lprefix_ltlI)
qed simp

lemma lprefix_lappend: "xs ⊑ lappend xs ys"
by(coinduction arbitrary: xs) auto

lemma lprefix_down_linear:
assumes "xs ⊑ zs" "ys ⊑ zs"
shows "xs ⊑ ys ∨ ys ⊑ xs"
proof(rule disjCI)
assume "¬ ys ⊑ xs"
with assms show "xs ⊑ ys"
by(coinduction arbitrary: xs ys zs)(auto simp add: not_lnull_conv LCons_lprefix_conv, simp add: lnull_def)
qed

lemma lprefix_lappend_same [simp]:
"lappend xs ys ⊑ lappend xs zs ⟷ (lfinite xs ⟶ ys ⊑ zs)"
(is "?lhs ⟷ ?rhs")
proof
assume "?lhs"
show "?rhs"
proof
assume "lfinite xs"
thus "ys ⊑ zs" using ‹?lhs› by(induct) simp_all
qed
next
assume "?rhs"
show ?lhs
proof(cases "lfinite xs")
case True
hence yszs: "ys ⊑ zs" by(rule ‹?rhs›[rule_format])
from True show ?thesis by induct (simp_all add: yszs)
next
case False thus ?thesis by(simp add: lappend_inf)
qed
qed

subsection ‹Setup for partial\_function›

primcorec lSup :: "'a llist set ⇒ 'a llist"
where
"lSup A =
(if ∀x∈A. lnull x then LNil
else LCons (THE x. x ∈ lhd ` (A ∩ {xs. ¬ lnull xs})) (lSup (ltl ` (A ∩ {xs. ¬ lnull xs}))))"

declare lSup.simps[simp del]

lemma lnull_lSup [simp]: "lnull (lSup A) ⟷ (∀x∈A. lnull x)"

lemma lhd_lSup [simp]: "∃x∈A. ¬ lnull x ⟹ lhd (lSup A) = (THE x. x ∈ lhd ` (A ∩ {xs. ¬ lnull xs}))"

lemma ltl_lSup [simp]: "ltl (lSup A) = lSup (ltl ` (A ∩ {xs. ¬ lnull xs}))"
by(cases "∀xs∈A. lnull xs")(auto 4 3 simp add: lSup_def intro: llist.expand)

lemma lhd_lSup_eq:
assumes chain: "Complete_Partial_Order.chain (⊑) Y"
shows "⟦ xs ∈ Y; ¬ lnull xs ⟧ ⟹ lhd (lSup Y) = lhd xs"
by(subst lhd_lSup)(auto 4 3 dest: chainD[OF chain] lprefix_lhdD intro!: the_equality)

lemma lSup_empty [simp]: "lSup {} = LNil"

lemma lSup_singleton [simp]: "lSup {xs} = xs"
by(coinduction arbitrary: xs) simp_all

lemma LCons_image_Int_not_lnull: "(LCons x ` A ∩ {xs. ¬ lnull xs}) = LCons x ` A"
by auto

lemma lSup_LCons: "A ≠ {} ⟹ lSup (LCons x ` A) = LCons x (lSup A)"
by(rule llist.expand)(auto simp add: image_image lhd_lSup exI LCons_image_Int_not_lnull intro!: the_equality)

lemma lSup_eq_LCons_iff:
"lSup Y = LCons x xs ⟷ (∃x∈Y. ¬ lnull x) ∧ x = (THE x. x ∈ lhd ` (Y ∩ {xs. ¬ lnull xs})) ∧ xs = lSup (ltl ` (Y ∩ {xs. ¬ lnull xs}))"
by(auto dest: eq_LConsD simp add: lnull_def[symmetric] intro: llist.expand)

lemma lSup_insert_LNil: "lSup (insert LNil Y) = lSup Y"
by(rule llist.expand) simp_all

lemma lSup_minus_LNil: "lSup (Y - {LNil}) = lSup Y"
using lSup_insert_LNil[where Y="Y - {LNil}", symmetric]
by(cases "LNil ∈ Y")(simp_all add: insert_absorb)

lemma chain_lprefix_ltl:
assumes chain: "Complete_Partial_Order.chain (⊑) A"
shows "Complete_Partial_Order.chain (⊑) (ltl ` (A ∩ {xs. ¬ lnull xs}))"
by(auto intro!: chainI dest: chainD[OF chain] intro: lprefix_ltlI)

lemma lSup_finite_prefixes: "lSup {ys. ys ⊑ xs ∧ lfinite ys} = xs" (is "lSup (?C xs) = _")
proof(coinduction arbitrary: xs)
case (Eq_llist xs)
have ?lnull
moreover
have "¬ lnull xs ⟹ ltl ` ({ys. ys ⊑ xs ∧ lfinite ys} ∩ {xs. ¬ lnull xs}) = {ys. ys ⊑ ltl xs ∧ lfinite ys}"
by(auto 4 4 intro!: rev_image_eqI[where x="LCons (lhd xs) ys" for ys] intro: llist.expand lprefix_ltlI simp add: LCons_lprefix_conv)
hence ?LCons by(auto 4 3 intro!: the_equality dest: lprefix_lhdD intro: rev_image_eqI)
ultimately show ?case ..
qed

lemma lSup_finite_gen_prefixes:
assumes "zs ⊑ xs" "lfinite zs"
shows "lSup {ys. ys ⊑ xs ∧ zs ⊑ ys ∧ lfinite ys} = xs"
using ‹lfinite zs› ‹zs ⊑ xs›
proof(induction arbitrary: xs)
case lfinite_LNil
next
case (lfinite_LConsI zs z)
from ‹LCons z zs ⊑ xs› obtain xs' where xs: "xs = LCons z xs'"
and "zs ⊑ xs'" by(auto simp add: LCons_lprefix_conv)
show ?case (is "?lhs = ?rhs")
proof(rule llist.expand)
show "lnull ?lhs = lnull ?rhs" using xs lfinite_LConsI
by(auto 4 3 simp add: lprefix_LCons_conv del: disjCI intro: disjI2)
next
assume lnull: "¬ lnull ?lhs" "¬ lnull ?rhs"
have "lhd ?lhs = lhd ?rhs" using lnull xs
by(auto intro!: rev_image_eqI simp add: LCons_lprefix_conv)
moreover
have "ltl ` ({ys. ys ⊑ xs ∧ LCons z zs ⊑ ys ∧ lfinite ys} ∩ {xs. ¬ lnull xs}) =
{ys. ys ⊑ xs' ∧ zs ⊑ ys ∧ lfinite ys}"
using xs ‹¬ lnull ?rhs›
by(auto 4 3 simp add: lprefix_LCons_conv intro: rev_image_eqI del: disjCI intro: disjI2)
hence "ltl ?lhs = ltl ?rhs" using lfinite_LConsI.IH[OF ‹zs ⊑ xs'›] xs by simp
ultimately show "lhd ?lhs = lhd ?rhs ∧ ltl ?lhs = ltl ?rhs" ..
qed
qed

lemma lSup_strict_prefixes:
"¬ lfinite xs ⟹ lSup {ys. ys ⊑ xs ∧ ys ≠ xs} = xs"
(is "_ ⟹ lSup (?C xs) = _")
proof(coinduction arbitrary: xs)
case (Eq_llist xs)
then obtain x x' xs' where xs: "xs = LCons x (LCons x' xs')" "¬ lfinite xs'"
by(cases xs)(simp, rename_tac xs', case_tac xs', auto)
hence ?lnull by(auto intro: exI[where x="LCons x (LCons x' LNil)"])
moreover hence "¬ lnull (lSup {ys. ys ⊑ xs ∧ ys ≠ xs})" using xs by auto
hence "lhd (lSup {ys. ys ⊑ xs ∧ ys ≠ xs}) = lhd xs" using xs
by(auto 4 3 intro!: the_equality intro: rev_image_eqI dest: lprefix_lhdD)
moreover from xs
have "ltl ` ({ys. ys ⊑ xs ∧ ys ≠ xs} ∩ {xs. ¬ lnull xs}) = {ys. ys ⊑ ltl xs ∧ ys ≠ ltl xs}"
by(auto simp add: lprefix_LCons_conv intro: image_eqI[where x="LCons x (LCons x' ys)" for ys] image_eqI[where x="LCons x LNil"])
ultimately show ?case using Eq_llist by clarsimp
qed

lemma chain_lprefix_lSup:
"⟦ Complete_Partial_Order.chain (⊑) A; xs ∈ A ⟧
⟹ xs ⊑ lSup A"
proof(coinduction arbitrary: xs A)
case (lprefix xs A)
note chain = ‹Complete_Partial_Order.chain (⊑) A›
from ‹xs ∈ A› show ?case
by(auto 4 3 dest: chainD[OF chain] lprefix_lhdD intro: chain_lprefix_ltl[OF chain] intro!: the_equality[symmetric])
qed

lemma chain_lSup_lprefix:
"⟦ Complete_Partial_Order.chain (⊑) A; ⋀xs. xs ∈ A ⟹ xs ⊑ zs ⟧
⟹ lSup A ⊑ zs"
proof(coinduction arbitrary: A zs)
case (lprefix A zs)
note chain = ‹Complete_Partial_Order.chain (⊑) A›
from ‹∀xs. xs ∈ A ⟶ xs ⊑ zs›
show ?case
by(auto 4 4 dest: lprefix_lnullD lprefix_lhdD intro: chain_lprefix_ltl[OF chain] lprefix_ltlI rev_image_eqI intro!: the_equality)
qed

lemma llist_ccpo [simp, cont_intro]: "class.ccpo lSup (⊑) (mk_less (⊑))"
by(unfold_locales)(auto dest: lprefix_antisym intro: lprefix_trans chain_lprefix_lSup chain_lSup_lprefix simp add: mk_less_def)

lemma llist_partial_function_definitions:
"partial_function_definitions (⊑) lSup"
by(unfold_locales)(auto dest: lprefix_antisym intro: lprefix_trans chain_lprefix_lSup chain_lSup_lprefix)

interpretation llist: partial_function_definitions "(⊑)" lSup
rewrites "lSup {} ≡ LNil"
by(rule llist_partial_function_definitions)(simp)

abbreviation "mono_llist ≡ monotone (fun_ord (⊑)) (⊑)"

interpretation llist_lift: partial_function_definitions "fun_ord lprefix" "fun_lub lSup"
rewrites "fun_lub lSup {} ≡ λ_. LNil"
by(rule llist_partial_function_definitions[THEN partial_function_lift])(simp)

abbreviation "mono_llist_lift ≡ monotone (fun_ord (fun_ord lprefix)) (fun_ord lprefix)"

lemma lprefixes_chain:
"Complete_Partial_Order.chain (⊑) {ys. lprefix ys xs}"
by(rule chainI)(auto dest: lprefix_down_linear)

lemma llist_gen_induct:
and step: "∃zs. zs ⊑ xs ∧ lfinite zs ∧ (∀ys. zs ⊑ ys ⟶ ys ⊑ xs ⟶ lfinite ys ⟶ P ys)"
shows "P xs"
proof -
from step obtain zs
where zs: "zs ⊑ xs" "lfinite zs"
and ys: "⋀ys. ⟦ zs ⊑ ys; ys ⊑ xs; lfinite ys ⟧ ⟹ P ys" by blast
let ?C = "{ys. ys ⊑ xs ∧ zs ⊑ ys ∧ lfinite ys}"
from lprefixes_chain[of xs]
have "Complete_Partial_Order.chain (⊑) ?C"
by(auto dest: chain_compr)
with adm have "P (lSup ?C)"
also have "lSup ?C  = xs"
using lSup_finite_gen_prefixes[OF zs] by simp
finally show ?thesis .
qed

lemma llist_induct [case_names adm LNil LCons, induct type: llist]:
and LNil: "P LNil"
and LCons: "⋀x xs. ⟦ lfinite xs; P xs ⟧ ⟹ P (LCons x xs)"
shows "P xs"
proof -
{ fix ys :: "'a llist"
assume "lfinite ys"
hence "P ys" by(induct)(simp_all add: LNil LCons) }
note [intro] = this
by(rule llist_gen_induct)(auto intro: exI[where x=LNil])
qed

lemma LCons_mono [partial_function_mono, cont_intro]:
"mono_llist A ⟹ mono_llist (λf. LCons x (A f))"
by(rule monotoneI)(auto dest: monotoneD)

lemma mono2mono_LCons [THEN llist.mono2mono, simp, cont_intro]:
shows monotone_LCons: "monotone (⊑) (⊑) (LCons x)"
by(auto intro: monotoneI)

lemma mcont2mcont_LCons [THEN llist.mcont2mcont, simp, cont_intro]:
shows mcont_LCons: "mcont lSup (⊑) lSup (⊑) (LCons x)"
by(simp add: mcont_def monotone_LCons lSup_LCons[symmetric] contI)

lemma mono2mono_ltl[THEN llist.mono2mono, simp, cont_intro]:
shows monotone_ltl: "monotone (⊑) (⊑) ltl"
by(auto intro: monotoneI lprefix_ltlI)

lemma cont_ltl: "cont lSup (⊑) lSup (⊑) ltl"
proof(rule contI)
fix Y :: "'a llist set"
assume "Y ≠ {}"
have "ltl (lSup Y) = lSup (insert LNil (ltl ` (Y ∩ {xs. ¬ lnull xs})))"
also have "insert LNil (ltl ` (Y ∩ {xs. ¬ lnull xs})) = insert LNil (ltl ` Y)" by auto
also have "lSup … = lSup (ltl ` Y)" by(simp add: lSup_insert_LNil)
finally show "ltl (lSup Y) = lSup (ltl ` Y)" .
qed

lemma mcont2mcont_ltl [THEN llist.mcont2mcont, simp, cont_intro]:
shows mcont_ltl: "mcont lSup (⊑) lSup (⊑) ltl"

lemma llist_case_mono [partial_function_mono, cont_intro]:
assumes lnil: "monotone orda ordb lnil"
and lcons: "⋀x xs. monotone orda ordb (λf. lcons f x xs)"
shows "monotone orda ordb (λf. case_llist (lnil f) (lcons f) x)"
by(rule monotoneI)(auto split: llist.split dest: monotoneD[OF lnil] monotoneD[OF lcons])

lemma mcont_llist_case [cont_intro, simp]:
"⟦ mcont luba orda lubb ordb (λx. f x); ⋀x xs. mcont luba orda lubb ordb (λy. g x xs y) ⟧
⟹ mcont luba orda lubb ordb (λy. case xs of LNil ⇒ f y | LCons x xs' ⇒ g x xs' y)"
by(cases xs) simp_all

lemma monotone_lprefix_case [cont_intro, simp]:
assumes mono: "⋀x. monotone (⊑) (⊑) (λxs. f x xs (LCons x xs))"
shows "monotone (⊑) (⊑) (λxs. case xs of LNil ⇒ LNil | LCons x xs' ⇒ f x xs' xs)"
by(rule llist.monotone_if_bot[where f="λxs. f (lhd xs) (ltl xs) xs" and bound=LNil])(auto 4 3 split: llist.split simp add: not_lnull_conv LCons_lprefix_conv dest: monotoneD[OF mono])

lemma mcont_lprefix_case_aux:
fixes f bot
defines "g ≡ λxs. f (lhd xs) (ltl xs) (LCons (lhd xs) (ltl xs))"
assumes mcont: "⋀x. mcont lSup (⊑) lub ord (λxs. f x xs (LCons x xs))"
and ccpo: "class.ccpo lub ord (mk_less ord)"
and bot: "⋀x. ord bot x"
shows "mcont lSup (⊑) lub ord (λxs. case xs of LNil ⇒ bot | LCons x xs' ⇒ f x xs' xs)"
proof(rule llist.mcont_if_bot[where f=g and bound=LNil and bot=bot, OF ccpo bot])
fix Y :: "'a llist set"
assume chain: "Complete_Partial_Order.chain (⊑) Y"
and Y: "Y ≠ {}" "⋀x. x ∈ Y ⟹ ¬ x ⊑ LNil"
from Y have Y': "Y ∩ {xs. ¬ lnull xs} ≠ {}" by auto
from Y obtain x xs where "LCons x xs ∈ Y" by(fastforce simp add: not_lnull_conv)
with Y(2) have eq: "Y = LCons x ` (ltl ` (Y ∩ {xs. ¬ lnull xs}))"
by(force dest: chainD[OF chain] simp add: LCons_lprefix_conv lprefix_LCons_conv intro: imageI rev_image_eqI)
show "g (lSup Y) = lub (g ` Y)"
by(subst (1 2) eq)(simp add: lSup_LCons Y' g_def mcont_contD[OF mcont] chain chain_lprefix_ltl, simp add: image_image)
qed(auto 4 3 split: llist.split simp add: not_lnull_conv LCons_lprefix_conv g_def intro: mcont_monoD[OF mcont])

lemma mcont_lprefix_case [cont_intro, simp]:
assumes "⋀x. mcont lSup (⊑) lSup (⊑) (λxs. f x xs (LCons x xs))"
shows "mcont lSup (⊑) lSup (⊑) (λxs. case xs of LNil ⇒ LNil | LCons x xs' ⇒ f x xs' xs)"
using assms by(rule mcont_lprefix_case_aux)(simp_all add: llist_ccpo)

lemma monotone_lprefix_case_lfp [cont_intro, simp]:
fixes f :: "_ ⇒ _ :: order_bot"
assumes mono: "⋀x. monotone (⊑) (≤) (λxs. f x xs (LCons x xs))"
shows "monotone (⊑) (≤) (λxs. case xs of LNil ⇒ ⊥ | LCons x xs ⇒ f x xs (LCons x xs))"
by(rule llist.monotone_if_bot[where bound=LNil and bot=⊥ and f="λxs. f (lhd xs) (ltl xs) xs"])(auto 4 3 simp add: not_lnull_conv LCons_lprefix_conv dest: monotoneD[OF mono] split: llist.split)

lemma mcont_lprefix_case_lfp [cont_intro, simp]:
fixes f :: "_ => _ :: complete_lattice"
assumes "⋀x. mcont lSup (⊑) Sup (≤) (λxs. f x xs (LCons x xs))"
shows "mcont lSup (⊑) Sup (≤) (λxs. case xs of LNil ⇒ ⊥ | LCons x xs ⇒ f x xs (LCons x xs))"
using assms by(rule mcont_lprefix_case_aux)(rule complete_lattice_ccpo', simp)

declaration ‹Partial_Function.init "llist" @{term llist.fixp_fun}
@{term llist.mono_body} @{thm llist.fixp_rule_uc} @{thm llist.fixp_strong_induct_uc} NONE›

subsection ‹Monotonicity and continuity of already defined functions›

lemma fixes f F
defines "F ≡ λlmap xs. case xs of LNil ⇒ LNil | LCons x xs ⇒ LCons (f x) (lmap xs)"
shows lmap_conv_fixp: "lmap f ≡ ccpo.fixp (fun_lub lSup) (fun_ord (⊑)) F" (is "?lhs ≡ ?rhs")
and lmap_mono: "⋀xs. mono_llist (λlmap. F lmap xs)" (is "PROP ?mono")
proof(intro eq_reflection ext)
show mono: "PROP ?mono" unfolding F_def by(tactic ‹Partial_Function.mono_tac @{context} 1›)
fix xs
show "?lhs xs = ?rhs xs"
proof(coinduction arbitrary: xs)
case Eq_llist
show ?case by(subst (1 3 4) llist.mono_body_fixp[OF mono])(auto simp add: F_def split: llist.split)
qed
qed

lemma mono2mono_lmap[THEN llist.mono2mono, simp, cont_intro]:
shows monotone_lmap: "monotone (⊑) (⊑) (lmap f)"
by(rule llist.fixp_preserves_mono1[OF lmap_mono lmap_conv_fixp]) simp

lemma mcont2mcont_lmap[THEN llist.mcont2mcont, simp, cont_intro]:
shows mcont_lmap: "mcont lSup (⊑) lSup (⊑) (lmap f)"
by(rule llist.fixp_preserves_mcont1[OF lmap_mono lmap_conv_fixp]) simp

lemma [partial_function_mono]: "mono_llist F ⟹ mono_llist (λf. lmap g (F f))"
by(rule mono2mono_lmap)

lemma mono_llist_lappend2 [partial_function_mono]:
"mono_llist A ⟹ mono_llist (λf. lappend xs (A f))"
by(auto intro!: monotoneI lprefix_lappend_sameI simp add: fun_ord_def dest: monotoneD)

lemma mono2mono_lappend2 [THEN llist.mono2mono, cont_intro, simp]:
shows monotone_lappend2: "monotone (⊑) (⊑) (lappend xs)"
by(rule monotoneI)(rule lprefix_lappend_sameI)

lemma mcont2mcont_lappend2 [THEN llist.mcont2mcont, cont_intro, simp]:
shows mcont_lappend2: "mcont lSup (⊑) lSup (⊑) (lappend xs)"
proof(cases "lfinite xs")
case True
thus ?thesis by induct(simp_all add: monotone_lappend2)
next
case False
hence "lappend xs = (λ_. xs)" by(simp add: fun_eq_iff lappend_inf)
thus ?thesis by(simp add: ccpo.cont_const[OF llist_ccpo])
qed

lemma fixes f F
defines "F ≡ λlset xs. case xs of LNil ⇒ {} | LCons x xs ⇒ insert x (lset xs)"
shows lset_conv_fixp: "lset ≡ ccpo.fixp (fun_lub Union) (fun_ord (⊆)) F" (is "_ ≡ ?fixp")
and lset_mono: "⋀x. monotone (fun_ord (⊆)) (⊆) (λf. F f x)" (is "PROP ?mono")
proof(rule eq_reflection ext antisym subsetI)+
show mono: "PROP ?mono" unfolding F_def by(tactic ‹Partial_Function.mono_tac @{context} 1›)
fix x xs
show "?fixp xs ⊆ lset xs"
by(induct arbitrary: xs rule: lfp.fixp_induct_uc[of "λx. x" F "λx. x", OF mono reflexive refl])(auto simp add: F_def split: llist.split)

assume "x ∈ lset xs"
thus "x ∈ ?fixp xs" by induct(subst lfp.mono_body_fixp[OF mono], simp add: F_def)+
qed

lemma mono2mono_lset [THEN lfp.mono2mono, cont_intro, simp]:
shows monotone_lset: "monotone (⊑) (⊆) lset"
by(rule lfp.fixp_preserves_mono1[OF lset_mono lset_conv_fixp]) simp

lemma mcont2mcont_lset[THEN mcont2mcont, cont_intro, simp]:
shows mcont_lset: "mcont lSup (⊑) Union (⊆) lset"
by(rule lfp.fixp_preserves_mcont1[OF lset_mono lset_conv_fixp]) simp

lemma lset_lSup: "Complete_Partial_Order.chain (⊑) Y ⟹ lset (lSup Y) = ⋃(lset ` Y)"
by(cases "Y = {}")(simp_all add: mcont_lset[THEN mcont_contD])

lemma lfinite_lSupD: "lfinite (lSup A) ⟹ ∀xs ∈ A. lfinite xs"
by(induct ys≡"lSup A" arbitrary: A rule: lfinite_induct) fastforce+

lemma monotone_enat_le_lprefix_case [cont_intro, simp]:
"monotone (≤) (⊑) (λx. f x (eSuc x)) ⟹ monotone (≤) (⊑) (λx. case x of 0 ⇒ LNil | eSuc x' ⇒ f x' x)"
by(erule monotone_enat_le_case) simp_all

lemma mcont_enat_le_lprefix_case [cont_intro, simp]:
assumes "mcont Sup (≤) lSup (⊑) (λx. f x (eSuc x))"
shows "mcont Sup (≤) lSup (⊑) (λx. case x of 0 ⇒ LNil | eSuc x' ⇒ f x' x)"
using llist_ccpo assms by(rule mcont_enat_le_case) simp

lemma compact_LConsI:
assumes "ccpo.compact lSup (⊑) xs"
shows "ccpo.compact lSup (⊑) (LCons x xs)"
using llist_ccpo
proof(rule ccpo.compactI)
from assms have "ccpo.admissible lSup (⊑) (λys. ¬ xs ⊑ ys)" by cases
hence [cont_intro]: "ccpo.admissible lSup (⊑) (λys. ¬ xs ⊑ ltl ys)"
have [cont_intro]: "ccpo.admissible lSup (⊑) (λys. ¬ lnull ys ∧ lhd ys ≠ x)"
fix Y
assume chain: "Complete_Partial_Order.chain (⊑) Y"
and *: "Y ≠ {}" "∀ys∈Y. ¬ lnull ys ∧ lhd ys ≠ x"
from * show "¬ lnull (lSup Y) ∧ lhd (lSup Y) ≠ x"
by(subst lhd_lSup)(auto 4 4 dest: chainD[OF chain] intro!: the_equality[symmetric] dest: lprefix_lhdD)
qed

have eq: "(λys. ¬ LCons x xs ⊑ ys) = (λys. ¬ xs ⊑ ltl ys ∨ ys = LNil ∨ ¬ lnull ys ∧ lhd ys ≠ x)"
by(auto simp add: fun_eq_iff LCons_lprefix_conv neq_LNil_conv)
show "ccpo.admissible lSup (⊑) (λys. ¬ LCons x xs ⊑ ys)"
qed

lemma compact_LConsD:
assumes "ccpo.compact lSup (⊑) (LCons x xs)"
shows "ccpo.compact lSup (⊑) xs"
using llist_ccpo
proof(rule ccpo.compactI)
from assms have "ccpo.admissible lSup (⊑) (λys. ¬ LCons x xs ⊑ ys)" by cases
hence "ccpo.admissible lSup (⊑) (λys. ¬ LCons x xs ⊑ LCons x ys)"
thus "ccpo.admissible lSup (⊑) (λys. ¬ xs ⊑ ys)" by simp
qed

lemma compact_LCons_iff [simp]:
"ccpo.compact lSup (⊑) (LCons x xs) ⟷ ccpo.compact lSup (⊑) xs"
by(blast intro: compact_LConsI compact_LConsD)

lemma compact_lfiniteI:
"lfinite xs ⟹ ccpo.compact lSup (⊑) xs"
by(induction rule: lfinite.induct) simp_all

lemma compact_lfiniteD:
assumes "ccpo.compact lSup (⊑) xs"
shows "lfinite xs"
proof(rule ccontr)
assume inf: "¬ lfinite xs"

from assms have "ccpo.admissible lSup (⊑) (λys. ¬ xs ⊑ ys)" by cases
moreover let ?C = "{ys. ys ⊑ xs ∧ ys ≠ xs}"
have "Complete_Partial_Order.chain (⊑) ?C"
using lprefixes_chain[of xs] by(auto dest: chain_compr)
moreover have "?C ≠ {}" using inf by(cases xs) auto
ultimately have "¬ xs ⊑ lSup ?C"
also have "lSup ?C = xs" using inf by(rule lSup_strict_prefixes)
finally show False by simp
qed

lemma compact_eq_lfinite [simp]: "ccpo.compact lSup (⊑) = lfinite"
by(blast intro: compact_lfiniteI compact_lfiniteD)

subsection ‹More function definitions›

primcorec iterates :: "('a ⇒ 'a) ⇒ 'a ⇒ 'a llist"
where "iterates f x = LCons x (iterates f (f x))"

primrec llist_of :: "'a list ⇒ 'a llist"
where
"llist_of [] = LNil"
| "llist_of (x#xs) = LCons x (llist_of xs)"

definition list_of :: "'a llist ⇒ 'a list"
where [code del]: "list_of xs = (if lfinite xs then inv llist_of xs else undefined)"

definition llength :: "'a llist ⇒ enat"
where [code del]:
"llength = enat_unfold lnull ltl"

primcorec ltake :: "enat ⇒ 'a llist ⇒ 'a llist"
where
"n = 0 ∨ lnull xs ⟹ lnull (ltake n xs)"
| "lhd (ltake n xs) = lhd xs"
| "ltl (ltake n xs) = ltake (epred n) (ltl xs)"

definition ldropn :: "nat ⇒ 'a llist ⇒ 'a llist"
where "ldropn n xs = (ltl ^^ n) xs"

context notes [[function_internals]]
begin

partial_function (llist) ldrop :: "enat ⇒ 'a llist ⇒ 'a llist"
where
"ldrop n xs = (case n of 0 ⇒ xs | eSuc n' ⇒ case xs of LNil ⇒ LNil | LCons x xs' ⇒ ldrop n' xs')"

end

primcorec ltakeWhile :: "('a ⇒ bool) ⇒ 'a llist ⇒ 'a llist"
where
"lnull xs ∨ ¬ P (lhd xs) ⟹ lnull (ltakeWhile P xs)"
| "lhd (ltakeWhile P xs) = lhd xs"
| "ltl (ltakeWhile P xs) = ltakeWhile P (ltl xs)"

context fixes P :: "'a ⇒ bool"
notes [[function_internals]]
begin

partial_function (llist) ldropWhile :: "'a llist ⇒ 'a llist"
where "ldropWhile xs = (case xs of LNil ⇒ LNil | LCons x xs' ⇒ if P x then ldropWhile xs' else xs)"

partial_function (llist) lfilter :: "'a llist ⇒ 'a llist"
where "lfilter xs = (case xs of LNil ⇒ LNil | LCons x xs' ⇒ if P x then LCons x (lfilter xs') else lfilter xs')"

end

primrec lnth :: "'a llist ⇒ nat ⇒ 'a"
where
"lnth xs 0 = (case xs of LNil ⇒ undefined (0 :: nat) | LCons x xs' ⇒ x)"
| "lnth xs (Suc n) = (case xs of LNil ⇒ undefined (Suc n) | LCons x xs' ⇒ lnth xs' n)"

declare lnth.simps [simp del]

primcorec lzip :: "'a llist ⇒ 'b llist ⇒ ('a × 'b) llist"
where
"lnull xs ∨ lnull ys ⟹ lnull (lzip xs ys)"
| "lhd (lzip xs ys) = (lhd xs, lhd ys)"
| "ltl (lzip xs ys) = lzip (ltl xs) (ltl ys)"

definition llast :: "'a llist ⇒ 'a"
where [nitpick_simp]:
"llast xs = (case llength xs of enat n ⇒ (case n of 0 ⇒ undefined | Suc n' ⇒ lnth xs n') | ∞ ⇒ undefined)"

coinductive ldistinct :: "'a llist ⇒ bool"
where
LNil [simp]: "ldistinct LNil"
| LCons: "⟦ x ∉ lset xs; ldistinct xs ⟧ ⟹ ldistinct (LCons x xs)"

hide_fact (open) LNil LCons

definition inf_llist :: "(nat ⇒ 'a) ⇒ 'a llist"
where [code del]: "inf_llist f = lmap f (iterates Suc 0)"

abbreviation repeat :: "'a ⇒ 'a llist"
where "repeat ≡ iterates (λx. x)"

definition lstrict_prefix :: "'a llist ⇒ 'a llist ⇒ bool"
where [code del]: "lstrict_prefix xs ys ≡ xs ⊑ ys ∧ xs ≠ ys"

text ‹longest common prefix›
definition llcp :: "'a llist ⇒ 'a llist ⇒ enat"
where [code del]:
"llcp xs ys =
enat_unfold (λ(xs, ys). lnull xs ∨ lnull ys ∨ lhd xs ≠ lhd ys) (map_prod ltl ltl) (xs, ys)"

coinductive llexord :: "('a ⇒ 'a ⇒ bool) ⇒ 'a llist ⇒ 'a llist ⇒ bool"
for r :: "'a ⇒ 'a ⇒ bool"
where
llexord_LCons_eq: "llexord r xs ys ⟹ llexord r (LCons x xs) (LCons x ys)"
| llexord_LCons_less: "r x y ⟹ llexord r (LCons x xs) (LCons y ys)"
| llexord_LNil [simp, intro!]: "llexord r LNil ys"

context notes [[function_internals]]
begin

partial_function (llist) lconcat :: "'a llist llist ⇒ 'a llist"
where "lconcat xss = (case xss of LNil ⇒ LNil | LCons xs xss' ⇒ lappend xs (lconcat xss'))"

end

definition lhd' :: "'a llist ⇒ 'a option" where
"lhd' xs = (if lnull xs then None else Some (lhd xs))"

lemma lhd'_simps[simp]:
"lhd' LNil = None"
"lhd' (LCons x xs) = Some x"
unfolding lhd'_def by auto

definition ltl' :: "'a llist ⇒ 'a llist option" where
"ltl' xs = (if lnull xs then None else Some (ltl xs))"

lemma ltl'_simps[simp]:
"ltl' LNil = None"
"ltl' (LCons x xs) = Some xs"
unfolding ltl'_def by auto

definition lnths :: "'a llist ⇒ nat set ⇒ 'a llist"
where "lnths xs A = lmap fst (lfilter (λ(x, y). y ∈ A) (lzip xs (iterates Suc 0)))"

definition (in monoid_add) lsum_list :: "'a llist ⇒ 'a"
where "lsum_list xs = (if lfinite xs then sum_list (list_of xs) else 0)"

subsection ‹Converting ordinary lists to lazy lists: @{term "llist_of"}›

lemma lhd_llist_of [simp]: "lhd (llist_of xs) = hd xs"

lemma ltl_llist_of [simp]: "ltl (llist_of xs) = llist_of (tl xs)"
by(cases xs) simp_all

lemma lfinite_llist_of [simp]: "lfinite (llist_of xs)"
by(induct xs) auto

lemma lfinite_eq_range_llist_of: "lfinite xs ⟷ xs ∈ range llist_of"
proof
assume "lfinite xs"
thus "xs ∈ range llist_of"
by(induct rule: lfinite.induct)(auto intro: llist_of.simps[symmetric])
next
assume "xs ∈ range llist_of"
thus "lfinite xs" by(auto intro: lfinite_llist_of)
qed

lemma lnull_llist_of [simp]: "lnull (llist_of xs) ⟷ xs = []"
by(cases xs) simp_all

lemma llist_of_eq_LNil_conv:
"llist_of xs = LNil ⟷ xs = []"
by(cases xs) simp_all

lemma llist_of_eq_LCons_conv:
"llist_of xs = LCons y ys ⟷ (∃xs'. xs = y # xs' ∧ ys = llist_of xs')"
by(cases xs) auto

lemma lappend_llist_of_llist_of:
"lappend (llist_of xs) (llist_of ys) = llist_of (xs @ ys)"
by(induct xs) simp_all

lemma lfinite_rev_induct [consumes 1, case_names Nil snoc]:
assumes fin: "lfinite xs"
and Nil: "P LNil"
and snoc: "⋀x xs. ⟦ lfinite xs; P xs ⟧ ⟹ P (lappend xs (LCons x LNil))"
shows "P xs"
proof -
from fin obtain xs' where xs: "xs = llist_of xs'"
unfolding lfinite_eq_range_llist_of by blast
show ?thesis unfolding xs
by(induct xs' rule: rev_induct)(auto simp add: Nil lappend_llist_of_llist_of[symmetric] dest: snoc[rotated])
qed

lemma lappend_llist_of_LCons:
"lappend (llist_of xs) (LCons y ys) = lappend (llist_of (xs @ [y])) ys"
by(induct xs) simp_all

lemma lmap_llist_of [simp]:
"lmap f (llist_of xs) = llist_of (map f xs)"
by(induct xs) simp_all

lemma lset_llist_of [simp]: "lset (llist_of xs) = set xs"
by(induct xs) simp_all

lemma llist_of_inject [simp]: "llist_of xs = llist_of ys ⟷ xs = ys"
proof
assume "llist_of xs = llist_of ys"
thus "xs = ys"
proof(induct xs arbitrary: ys)
case Nil thus ?case by(cases ys) auto
next
case Cons thus ?case by(cases ys) auto
qed
qed simp

lemma inj_llist_of [simp]: "inj llist_of"
by(rule inj_onI) simp

subsection ‹Converting finite lazy lists to ordinary lists: @{term "list_of"}›

lemma list_of_llist_of [simp]: "list_of (llist_of xs) = xs"
by(fastforce simp add: list_of_def intro: inv_f_f inj_onI)

lemma llist_of_list_of [simp]: "lfinite xs ⟹ llist_of (list_of xs) = xs"
unfolding lfinite_eq_range_llist_of by auto

lemma list_of_LNil [simp, nitpick_simp]: "list_of LNil = []"
using list_of_llist_of[of "[]"] by simp

lemma list_of_LCons [simp]: "lfinite xs ⟹ list_of (LCons x xs) = x # list_of xs"
proof(induct arbitrary: x rule: lfinite.induct)
case lfinite_LNil
show ?case using list_of_llist_of[of "[x]"] by simp
next
case (lfinite_LConsI xs' x')
from ‹list_of (LCons x' xs') = x' # list_of xs'› show ?case
using list_of_llist_of[of "x # x' # list_of xs'"]
llist_of_list_of[OF ‹lfinite xs'›] by simp
qed

lemma list_of_LCons_conv [nitpick_simp]:
"list_of (LCons x xs) = (if lfinite xs then x # list_of xs else undefined)"

lemma list_of_lappend:
assumes "lfinite xs" "lfinite ys"
shows "list_of (lappend xs ys) = list_of xs @ list_of ys"
using ‹lfinite xs› by induct(simp_all add: ‹lfinite ys›)

lemma list_of_lmap [simp]:
assumes "lfinite xs"
shows "list_of (lmap f xs) = map f (list_of xs)"
using assms by induct simp_all

lemma set_list_of [simp]:
assumes "lfinite xs"
shows "set (list_of xs) = lset xs"
using assms by(induct)(simp_all)

lemma hd_list_of [simp]: "lfinite xs ⟹ hd (list_of xs) = lhd xs"

lemma tl_list_of: "lfinite xs ⟹ tl (list_of xs) = list_of (ltl xs)"

text ‹Efficient implementation via tail recursion suggested by Brian Huffman›

definition list_of_aux :: "'a list ⇒ 'a llist ⇒ 'a list"
where "list_of_aux xs ys = (if lfinite ys then rev xs @ list_of ys else undefined)"

lemma list_of_code [code]: "list_of = list_of_aux []"

lemma list_of_aux_code [code]:
"list_of_aux xs LNil = rev xs"
"list_of_aux xs (LCons y ys) = list_of_aux (y # xs) ys"

subsection ‹The length of a lazy list: @{term "llength"}›

lemma [simp, nitpick_simp]:
shows llength_LNil: "llength LNil = 0"
and llength_LCons: "llength (LCons x xs) = eSuc (llength xs)"

lemma llength_eq_0 [simp]: "llength xs = 0 ⟷ lnull xs"
by(cases xs) simp_all

lemma llength_lnull [simp]: "lnull xs ⟹ llength xs = 0"
by simp

lemma epred_llength:
"epred (llength xs) = llength (ltl xs)"
by(cases xs) simp_all

lemmas llength_ltl = epred_llength[symmetric]

lemma llength_lmap [simp]: "llength (lmap f xs) = llength xs"
by(coinduction arbitrary: xs rule: enat_coinduct)(auto simp add: epred_llength)

lemma llength_lappend [simp]: "llength (lappend xs ys) = llength xs + llength ys"

lemma llength_llist_of [simp]:
"llength (llist_of xs) = enat (length xs)"

lemma length_list_of:
"lfinite xs ⟹ enat (length (list_of xs)) = llength xs"
apply(rule sym)
by(induct rule: lfinite.induct)(auto simp add: eSuc_enat zero_enat_def)

lemma length_list_of_conv_the_enat:
"lfinite xs ⟹ length (list_of xs) = the_enat (llength xs)"
unfolding lfinite_eq_range_llist_of by auto

lemma llength_eq_enat_lfiniteD: "llength xs = enat n ⟹ lfinite xs"
proof(induct n arbitrary: xs)
case [folded zero_enat_def]: 0
thus ?case by simp
next
case (Suc n)
note len = ‹llength xs = enat (Suc n)›
then obtain x xs' where "xs = LCons x xs'"
moreover with len have "llength xs' = enat n"
hence "lfinite xs'" by(rule Suc)
ultimately show ?case by simp
qed

lemma lfinite_llength_enat:
assumes "lfinite xs"
shows "∃n. llength xs = enat n"
using assms
by induct(auto simp add: eSuc_def zero_enat_def)

lemma lfinite_conv_llength_enat:
"lfinite xs ⟷ (∃n. llength xs = enat n)"
by(blast dest: llength_eq_enat_lfiniteD lfinite_llength_enat)

lemma not_lfinite_llength:
"¬ lfinite xs ⟹ llength xs = ∞"

lemma llength_eq_infty_conv_lfinite:
"llength xs = ∞ ⟷ ¬ lfinite xs"

lemma lfinite_finite_index: "lfinite xs ⟹ finite {n. enat n < llength xs}"
by(auto dest: lfinite_llength_enat)

text ‹tail-recursive implementation for @{term llength}›

definition gen_llength :: "nat ⇒ 'a llist ⇒ enat"
where "gen_llength n xs = enat n + llength xs"

lemma gen_llength_code [code]:
"gen_llength n LNil = enat n"
"gen_llength n (LCons x xs) = gen_llength (n + 1) xs"

lemma llength_code [code]: "llength = gen_llength 0"

lemma fixes F
defines "F ≡ λllength xs. case xs of LNil ⇒ 0 | LCons x xs ⇒ eSuc (llength xs)"
shows llength_conv_fixp: "llength ≡ ccpo.fixp (fun_lub Sup) (fun_ord (≤)) F" (is "_ ≡ ?fixp")
and llength_mono: "⋀xs. monotone (fun_ord (≤)) (≤) (λllength. F llength xs)" (is "PROP ?mono")
proof(intro eq_reflection ext)
show mono: "PROP ?mono" unfolding F_def by(tactic ‹Partial_Function.mono_tac @{context} 1›)
fix xs
show "llength xs = ?fixp xs"
by(coinduction arbitrary: xs rule: enat_coinduct)(subst (1 2 3) lfp.mono_body_fixp[OF mono], fastforce simp add: F_def split: llist.split del: iffI)+
qed

lemma mono2mono_llength[THEN lfp.mono2mono, simp, cont_intro]:
shows monotone_llength: "monotone (⊑) (≤) llength"
by(rule lfp.fixp_preserves_mono1[OF llength_mono llength_conv_fixp])(fold bot_enat_def, simp)

lemma mcont2mcont_llength[THEN lfp.mcont2mcont, simp, cont_intro]:
shows mcont_llength: "mcont lSup (⊑) Sup (≤) llength"
by(rule lfp.fixp_preserves_mcont1[OF llength_mono llength_conv_fixp])(fold bot_enat_def, simp)

subsection ‹Taking and dropping from lazy lists: @{term "ltake"}, @{term "ldropn"}, and @{term "ldrop"}›

lemma ltake_LNil [simp, code, nitpick_simp]: "ltake n LNil = LNil"
by simp

lemma ltake_0 [simp]: "ltake 0 xs = LNil"

lemma ltake_eSuc_LCons [simp]:
"ltake (eSuc n) (LCons x xs) = LCons x (ltake n xs)"
by(rule llist.expand)(simp_all)

lemma ltake_eSuc:
"ltake (eSuc n) xs =
(case xs of LNil ⇒ LNil | LCons x xs' ⇒ LCons x (ltake n xs'))"
by(cases xs) simp_all

lemma lnull_ltake [simp]: "lnull (ltake n xs) ⟷ lnull xs ∨ n = 0"
by(cases n xs rule: enat_coexhaust[case_product llist.exhaust]) simp_all

lemma ltake_eq_LNil_iff: "ltake n xs = LNil ⟷ xs = LNil ∨ n = 0"
by(cases n xs rule: enat_coexhaust[case_product llist.exhaust]) simp_all

lemma LNil_eq_ltake_iff [simp]: "LNil = ltake n xs ⟷ xs = LNil ∨ n = 0"
by(cases n xs rule: enat_coexhaust[case_product llist.exhaust]) simp_all

lemma ltake_LCons [code, nitpick_simp]:
"ltake n (LCons x xs) =
(case n of 0 ⇒ LNil | eSuc n' ⇒ LCons x (ltake n' xs))"
by(rule llist.expand)(simp_all split: co.enat.split)

lemma lhd_ltake [simp]: "n ≠ 0 ⟹ lhd (ltake n xs) = lhd xs"
by(cases n xs rule: enat_coexhaust[case_product llist.exhaust]) simp_all

lemma ltl_ltake: "ltl (ltake n xs) = ltake (epred n) (ltl xs)"
by(cases n xs rule: enat_coexhaust[case_product llist.exhaust]) simp_all

lemmas ltake_epred_ltl = ltl_ltake [symmetric]

declare ltake.sel(2) [simp del]

lemma ltake_ltl: "ltake n (ltl xs) = ltl (ltake (eSuc n) xs)"
by(cases xs) simp_all

lemma llength_ltake [simp]: "llength (ltake n xs) = min n (llength xs)"
by(coinduction arbitrary: n xs rule: enat_coinduct)(auto 4 3 simp add: enat_min_eq_0_iff epred_llength ltl_ltake)

lemma ltake_lmap [simp]: "ltake n (lmap f xs) = lmap f (ltake n xs)"
by(coinduction arbitrary: n xs)(auto 4 3 simp add: ltl_ltake)

lemma ltake_ltake [simp]: "ltake n (ltake m xs) = ltake (min n m) xs"
by(coinduction arbitrary: n m xs)(auto 4 4 simp add: enat_min_eq_0_iff ltl_ltake)

lemma lset_ltake: "lset (ltake n xs) ⊆ lset xs"
proof(rule subsetI)
fix x
assume "x ∈ lset (ltake n xs)"
thus "x ∈ lset xs"
proof(induct "ltake n xs" arbitrary: xs n rule: lset_induct)
case find thus ?case
by(cases xs)(simp, cases n rule: enat_coexhaust, simp_all)
next
case step thus ?case
by(cases xs)(simp, cases n rule: enat_coexhaust, simp_all)
qed
qed

lemma ltake_all: "llength xs ≤ m ⟹ ltake m xs = xs"
by(coinduction arbitrary: m xs)(auto simp add: epred_llength[symmetric] ltl_ltake intro: epred_le_epredI)

lemma ltake_llist_of [simp]:
"ltake (enat n) (llist_of xs) = llist_of (take n xs)"
proof(induct n arbitrary: xs)
case 0
thus ?case unfolding zero_enat_def[symmetric]
by(cases xs) simp_all
next
case (Suc n)
thus ?case unfolding eSuc_enat[symmetric]
by(cases xs) simp_all
qed

lemma lfinite_ltake [simp]:
"lfinite (ltake n xs) ⟷ lfinite xs ∨ n < ∞"
(is "?lhs ⟷ ?rhs")
proof
assume ?lhs
thus ?rhs
by(induct ys≡"ltake n xs" arbitrary: n xs rule: lfinite_induct)(fastforce simp add: zero_enat_def ltl_ltake)+
next
assume ?rhs (is "?xs ∨ ?n")
thus ?lhs
proof
assume ?xs thus ?thesis
by(induct xs arbitrary: n)(simp_all add: ltake_LCons split: enat_cosplit)
next
assume ?n
then obtain n' where "n = enat n'" by auto
moreover have "lfinite (ltake (enat n') xs)"
by(induct n' arbitrary: xs)
(auto simp add: zero_enat_def[symmetric] eSuc_enat[symmetric] ltake_eSuc
split: llist.split)
ultimately show ?thesis by simp
qed
qed

lemma ltake_lappend1:  "n ≤ llength xs ⟹ ltake n (lappend xs ys) = ltake n xs"
by(coinduction arbitrary: n xs)(auto intro!: exI simp add: llength_ltl epred_le_epredI ltl_ltake)

lemma ltake_lappend2:
"llength xs ≤ n ⟹ ltake n (lappend xs ys) = lappend xs (ltake (n - llength xs) ys)"
by(coinduction arbitrary: n xs rule: llist.coinduct_strong)(auto intro!: exI simp add: llength_ltl epred_le_epredI ltl_ltake)

lemma ltake_lappend:
"ltake n (lappend xs ys) = lappend (ltake n xs) (ltake (n - llength xs) ys)"
by(coinduction arbitrary: n xs ys rule: <```