# Theory Coinductive_List

theory Coinductive_List
imports Sublist Simps_Case_Conv Coinductive_Nat
```(*  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: llist.coinduct_strong)(auto intro!: exI simp add: llength_ltl ltl_ltake)

lemma take_list_of:
assumes "lfinite xs"
shows "take n (list_of xs) = list_of (ltake (enat n) xs)"
using assms
by(induct arbitrary: n)
(simp_all add: take_Cons zero_enat_def[symmetric] eSuc_enat[symmetric] split: nat.split)

lemma ltake_eq_ltake_antimono:
"⟦ ltake n xs = ltake n ys; m ≤ n ⟧ ⟹ ltake m xs = ltake m ys"
by (metis ltake_ltake min_def)

lemma ltake_is_lprefix [simp, intro]: "ltake n xs ⊑ xs"
by(coinduction arbitrary: xs n)(auto simp add: ltl_ltake)

lemma lprefix_ltake_same [simp]:
"ltake n xs ⊑ ltake m xs ⟷ n ≤ m ∨ llength xs ≤ m"
(is "?lhs ⟷ ?rhs")
proof(rule iffI disjCI)+
assume ?lhs "¬ llength xs ≤ m"
thus "n ≤ m"
proof(coinduction arbitrary: n m xs rule: enat_le_coinduct)
case (le n m xs)
thus ?case by(cases xs)(auto 4 3 simp add: ltake_LCons split: co.enat.splits)
qed
next
assume ?rhs
thus ?lhs
proof
assume "n ≤ m"
thus ?thesis
by(coinduction arbitrary: n m xs)(auto 4 4 simp add: ltl_ltake epred_le_epredI)
qed

lemma fixes f F
defines "F ≡ λltake n xs. case xs of LNil ⇒ LNil | LCons x xs ⇒ case n of 0 ⇒ LNil | eSuc n ⇒ LCons x (ltake n xs)"
shows ltake_conv_fixp: "ltake ≡ curry (ccpo.fixp (fun_lub lSup) (fun_ord (⊑)) (λltake. case_prod (F (curry ltake))))" (is "?lhs ≡ ?rhs")
and ltake_mono: "⋀nxs. mono_llist (λltake. case nxs of (n, xs) ⇒ F (curry ltake) n 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 n xs
show "?lhs n xs = ?rhs n xs"
proof(coinduction arbitrary: n 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 prod.split co.enat.split)
qed
qed

lemma monotone_ltake: "monotone (rel_prod (≤) (⊑)) (⊑) (case_prod ltake)"
by(rule llist.fixp_preserves_mono2[OF ltake_mono ltake_conv_fixp]) simp

lemma mono2mono_ltake1[THEN llist.mono2mono, cont_intro, simp]:
shows monotone_ltake1: "monotone (≤) (⊑) (λn. ltake n xs)"
using monotone_ltake by auto

lemma mono2mono_ltake2[THEN llist.mono2mono, cont_intro, simp]:
shows monotone_ltake2: "monotone (⊑) (⊑) (ltake n)"
using monotone_ltake by auto

lemma mcont_ltake: "mcont (prod_lub Sup lSup) (rel_prod (≤) (⊑)) lSup (⊑) (case_prod ltake)"
by(rule llist.fixp_preserves_mcont2[OF ltake_mono ltake_conv_fixp]) simp

lemma mcont2mcont_ltake1 [THEN llist.mcont2mcont, cont_intro, simp]:
shows mcont_ltake1: "mcont Sup (≤) lSup (⊑) (λn. ltake n xs)"
using mcont_ltake by auto

lemma mcont2mcont_ltake2 [THEN llist.mcont2mcont, cont_intro, simp]:
shows mcont_ltake2: "mcont lSup (⊑) lSup (⊑) (ltake n)"
using mcont_ltake by auto

lemma [partial_function_mono]: "mono_llist F ⟹ mono_llist (λf. ltake n (F f))"
by(rule mono2mono_ltake2)

lemma llist_induct2:
assumes adm: "ccpo.admissible (prod_lub lSup lSup) (rel_prod (⊑) (⊑)) (λx. P (fst x) (snd x))"
and LNil: "P LNil LNil"
and LCons1: "⋀x xs. ⟦ lfinite xs; P xs LNil ⟧ ⟹ P (LCons x xs) LNil"
and LCons2: "⋀y ys. ⟦ lfinite ys; P LNil ys ⟧ ⟹ P LNil (LCons y ys)"
and LCons: "⋀x xs y ys. ⟦ lfinite xs; lfinite ys; P xs ys ⟧ ⟹ P (LCons x xs) (LCons y ys)"
shows "P xs ys"
proof -
let ?C = "(λn. (ltake n xs, ltake n ys)) ` range enat"
have "Complete_Partial_Order.chain (rel_prod (⊑) (⊑)) ?C"
by(rule chainI) auto
with adm have "P (fst (prod_lub lSup lSup ?C)) (snd (prod_lub lSup lSup ?C))"
fix xsys
assume "xsys ∈ ?C"
then obtain n where "xsys = (ltake (enat n) xs, ltake (enat n) ys)" by auto
moreover {
fix xs :: "'a llist"
assume "lfinite xs"
hence "P xs LNil" by induct(auto intro: LNil LCons1) }
note 1 = this
{ fix ys :: "'b llist"
assume "lfinite ys"
hence "P LNil ys" by induct(auto intro: LNil LCons2) }
note 2 = this
have "P (ltake (enat n) xs) (ltake (enat n) ys)"
by(induct n arbitrary: xs ys)(auto simp add: zero_enat_def[symmetric] LNil eSuc_enat[symmetric] ltake_eSuc split: llist.split intro: LNil LCons 1 2)
ultimately show "P (fst xsys) (snd xsys)" by simp
qed simp
also have "fst (prod_lub lSup lSup ?C) = xs"
unfolding prod_lub_def fst_conv
by(subst image_image)(simp add: mcont_contD[OF mcont_ltake1, symmetric] ltake_all)
also have "snd (prod_lub lSup lSup ?C) = ys"
unfolding prod_lub_def snd_conv
by(subst image_image)(simp add: mcont_contD[OF mcont_ltake1, symmetric] ltake_all)
finally show ?thesis .
qed

lemma ldropn_0 [simp]: "ldropn 0 xs = xs"

lemma ldropn_LNil [code, simp]: "ldropn n LNil = LNil"

lemma ldropn_lnull: "lnull xs ⟹ ldropn n xs = LNil"

lemma ldropn_LCons [code]:
"ldropn n (LCons x xs) = (case n of 0 ⇒ LCons x xs | Suc n' ⇒ ldropn n' xs)"

lemma ldropn_Suc: "ldropn (Suc n) xs = (case xs of LNil ⇒ LNil | LCons x xs' ⇒ ldropn n xs')"
by(simp split: llist.split)(simp add: ldropn_def funpow_swap1)

lemma ldropn_Suc_LCons [simp]: "ldropn (Suc n) (LCons x xs) = ldropn n xs"

lemma ltl_ldropn: "ltl (ldropn n xs) = ldropn n (ltl xs)"
proof(induct n arbitrary: xs)
case 0 thus ?case by simp
next
case (Suc n)
thus ?case
by(cases xs)(simp_all add: ldropn_Suc split: llist.split)
qed

lemma ldrop_simps [simp]:
shows ldrop_LNil: "ldrop n LNil = LNil"
and ldrop_0: "ldrop 0 xs = xs"
and ldrop_eSuc_LCons: "ldrop (eSuc n) (LCons x xs) = ldrop n xs"

lemma ldrop_lnull: "lnull xs ⟹ ldrop n xs = LNil"

lemma fixes f F
defines "F ≡ λldropn xs. case xs of LNil ⇒ λ_. LNil | LCons x xs ⇒ λn. if n = 0 then LCons x xs else ldropn xs (n - 1)"
shows ldrop_conv_fixp: "(λxs n. ldropn n xs) ≡ ccpo.fixp (fun_lub (fun_lub lSup)) (fun_ord (fun_ord lprefix)) (λldrop. F ldrop)" (is "?lhs ≡ ?rhs")
and ldrop_mono: "⋀xs. mono_llist_lift (λldrop. F ldrop 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 n xs
show "?lhs xs n = ?rhs xs n"
by(induction n arbitrary: xs)
(subst llist_lift.mono_body_fixp[OF mono], simp add: F_def split: llist.split)+
qed

lemma ldropn_fixp_case_conv:
"(λxs. case xs of LNil ⇒ λ_. LNil | LCons x xs ⇒ λn. if n = 0 then LCons x xs else f xs (n - 1)) =
(λxs n. case xs of LNil ⇒ LNil | LCons x xs ⇒ if n = 0 then LCons x xs else f xs (n - 1))"
by(auto simp add: fun_eq_iff split: llist.split)

lemma monotone_ldropn_aux: "monotone lprefix (fun_ord lprefix) (λxs n. ldropn n xs)"
by(rule llist_lift.fixp_preserves_mono1[OF ldrop_mono ldrop_conv_fixp])

lemma mono2mono_ldropn[THEN llist.mono2mono, cont_intro, simp]:
shows monotone_ldropn': "monotone lprefix lprefix (λxs. ldropn n xs)"
using monotone_ldropn_aux by(auto simp add: monotone_def fun_ord_def)

lemma mcont_ldropn_aux: "mcont lSup lprefix (fun_lub lSup) (fun_ord lprefix) (λxs n. ldropn n xs)"
by(rule llist_lift.fixp_preserves_mcont1[OF ldrop_mono ldrop_conv_fixp])

lemma mcont2mcont_ldropn [THEN llist.mcont2mcont, cont_intro, simp]:
shows mcont_ldropn: "mcont lSup lprefix lSup lprefix (ldropn n)"
using mcont_ldropn_aux by(auto simp add: mcont_fun_lub_apply)

lemma monotone_enat_cocase [cont_intro, simp]:
"⟦ ⋀n. monotone (≤) ord (λn. f n (eSuc n));
⋀n. ord a (f n (eSuc n)); ord a a ⟧
⟹ monotone (≤) ord (λn. case n of 0 ⇒ a | eSuc n' ⇒ f n' n)"
by(rule monotone_enat_le_case)

lemma monotone_ldrop: "monotone (rel_prod (=) (⊑)) (⊑) (case_prod ldrop)"
by(rule llist.fixp_preserves_mono2[OF ldrop.mono ldrop_def]) simp

lemma mono2mono_ldrop2 [THEN llist.mono2mono, cont_intro, simp]:
shows monotone_ldrop2: "monotone (⊑) (⊑) (ldrop n)"

lemma mcont_ldrop: "mcont (prod_lub the_Sup lSup) (rel_prod (=) (⊑)) lSup (⊑) (case_prod ldrop)"
by(rule llist.fixp_preserves_mcont2[OF ldrop.mono ldrop_def]) simp

lemma mcont2monct_ldrop2 [THEN llist.mcont2mcont, cont_intro, simp]:
shows mcont_ldrop2: "mcont lSup (⊑) lSup (⊑) (ldrop n)"

lemma ldrop_eSuc_conv_ltl: "ldrop (eSuc n) xs = ltl (ldrop n xs)"
proof(induct xs arbitrary: n)
case LCons thus ?case by(cases n rule: co.enat.exhaust) simp_all
qed simp_all

lemma ldrop_ltl: "ldrop n (ltl xs) = ldrop (eSuc n) xs"
proof(induct xs arbitrary: n)
case LCons thus ?case by(cases n rule: co.enat.exhaust) simp_all
qed simp_all

lemma lnull_ldropn [simp]: "lnull (ldropn n xs) ⟷ llength xs ≤ enat n"
proof(induction n arbitrary: xs)
case (Suc n)
from Suc.IH[of "ltl xs"] show ?case

lemma ldrop_eq_LNil [simp]: "ldrop n xs = LNil ⟷ llength xs ≤ n"
proof(induction xs arbitrary: n)
case (LCons x xs n)
thus ?case by(cases n rule: co.enat.exhaust) simp_all
qed simp_all

lemma lnull_ldrop [simp]: "lnull (ldrop n xs) ⟷ llength xs ≤ n"
unfolding lnull_def by(fact ldrop_eq_LNil)

lemma ldropn_eq_LNil: "(ldropn n xs = LNil) = (llength xs ≤ enat n)"
using lnull_ldropn unfolding lnull_def .

lemma ldropn_all: "llength xs ≤ enat m ⟹ ldropn m xs = LNil"

lemma ldrop_all: "llength xs ≤ m ⟹ ldrop m xs = LNil"
by(simp)

lemma ltl_ldrop: "ltl (ldrop n xs) = ldrop n (ltl xs)"

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

lemma ldrop_LCons:
"ldrop n (LCons x xs) = (case n of 0 ⇒ LCons x xs | eSuc n' ⇒ ldrop n' xs)"
by(cases n rule: enat_coexhaust) simp_all

lemma ldrop_inf [code, simp]: "ldrop ∞ xs = LNil"

lemma ldrop_enat [code]: "ldrop (enat n) xs = ldropn n xs"
proof(induct n arbitrary: xs)
case Suc thus ?case

lemma lfinite_ldropn [simp]: "lfinite (ldropn n xs) = lfinite xs"
by(induct n arbitrary: xs)(simp_all add: ldropn_Suc split: llist.split)

lemma lfinite_ldrop [simp]:
"lfinite (ldrop n xs) ⟷ lfinite xs ∨ n = ∞"

lemma ldropn_ltl: "ldropn n (ltl xs) = ldropn (Suc n) xs"

lemmas ldrop_eSuc_ltl = ldropn_ltl[symmetric]

lemma lset_ldropn_subset: "lset (ldropn n xs) ⊆ lset xs"
by(induct n arbitrary: xs)(fastforce simp add: ldropn_Suc split: llist.split_asm)+

lemma in_lset_ldropnD: "x ∈ lset (ldropn n xs) ⟹ x ∈ lset xs"
using lset_ldropn_subset[of n xs] by auto

lemma lset_ldrop_subset: "lset (ldrop n xs) ⊆ lset xs"
proof(induct xs arbitrary: n)
case LCons thus ?case
by(cases n rule: co.enat.exhaust) auto
qed simp_all

lemma in_lset_ldropD: "x ∈ lset (ldrop n xs) ⟹ x ∈ lset xs"
using lset_ldrop_subset[of n xs] by(auto)

lemma lappend_ltake_ldrop: "lappend (ltake n xs) (ldrop n xs) = xs"
by(coinduction arbitrary: n xs rule: llist.coinduct_strong)
(auto simp add: ldrop_ltl ltl_ltake intro!: arg_cong2[where f=lappend])

lemma ldropn_lappend:
"ldropn n (lappend xs ys) =
(if enat n < llength xs then lappend (ldropn n xs) ys
else ldropn (n - the_enat (llength xs)) ys)"
proof(induct n arbitrary: xs)
case 0
thus ?case by(simp add: zero_enat_def[symmetric] lappend_lnull1)
next
case (Suc n)
{ fix zs
assume "llength zs ≤ enat n"
hence "the_enat (eSuc (llength zs)) = Suc (the_enat (llength zs))"
by(auto intro!: the_enat_eSuc iff del: not_infinity_eq) }
note eq = this
from Suc show ?case
by(cases xs)(auto simp add: not_less not_le eSuc_enat[symmetric] eq)
qed

lemma ldropn_lappend2:
"llength xs ≤ enat n ⟹ ldropn n (lappend xs ys) = ldropn (n - the_enat (llength xs)) ys"

lemma lappend_ltake_enat_ldropn [simp]: "lappend (ltake (enat n) xs) (ldropn n xs) = xs"
by(fold ldrop_enat)(rule lappend_ltake_ldrop)

lemma ldrop_lappend:
"ldrop n (lappend xs ys) =
(if n < llength xs then lappend (ldrop n xs) ys
else ldrop (n - llength xs) ys)"
― ‹cannot prove this directly using fixpoint induction,
because @{term "(-) :: enat ⇒ enat ⇒ enat"} is not a least fixpoint›
by(cases n)(cases "llength xs", simp_all add: ldropn_lappend not_less ldrop_enat)

lemma ltake_plus_conv_lappend:
"ltake (n + m) xs = lappend (ltake n xs) (ltake m (ldrop n xs))"

lemma ldropn_eq_LConsD:
"ldropn n xs = LCons y ys ⟹ enat n < llength xs"
proof(induct n arbitrary: xs)
case 0 thus ?case by(simp add: zero_enat_def[symmetric])
next
case (Suc n) thus ?case by(cases xs)(simp_all add: Suc_ile_eq)
qed

lemma ldrop_eq_LConsD:
"ldrop n xs = LCons y ys ⟹ n < llength xs"

lemma ldropn_lmap [simp]: "ldropn n (lmap f xs) = lmap f (ldropn n xs)"
by(induct n arbitrary: xs)(simp_all add: ldropn_Suc split: llist.split)

lemma ldrop_lmap [simp]: "ldrop n (lmap f xs) = lmap f (ldrop n xs)"
proof(induct xs arbitrary: n)
case LCons thus ?case by(cases n rule: co.enat.exhaust) simp_all
qed simp_all

lemma ldropn_ldropn [simp]:
"ldropn n (ldropn m xs) = ldropn (n + m) xs"
by(induct m arbitrary: xs)(auto simp add: ldropn_Suc split: llist.split)

lemma ldrop_ldrop [simp]:
"ldrop n (ldrop m xs) = ldrop (n + m) xs"
proof(induct xs arbitrary: m)
qed simp_all

lemma llength_ldropn [simp]: "llength (ldropn n xs) = llength xs - enat n"
proof(induct n arbitrary: xs)
case 0 thus ?case by(simp add: zero_enat_def[symmetric])
next
case (Suc n) thus ?case by(cases xs)(simp_all add: eSuc_enat[symmetric])
qed

lemma enat_llength_ldropn:
"enat n ≤ llength xs ⟹ enat (n - m) ≤ llength (ldropn m xs)"
by(cases "llength xs") simp_all

lemma ldropn_llist_of [simp]: "ldropn n (llist_of xs) = llist_of (drop n xs)"
proof(induct n arbitrary: xs)
case Suc thus ?case by(cases xs) simp_all
qed simp

lemma ldrop_llist_of: "ldrop (enat n) (llist_of xs) = llist_of (drop n xs)"
proof(induct xs arbitrary: n)
case Cons thus ?case by(cases n)(simp_all add: zero_enat_def[symmetric] eSuc_enat[symmetric])
qed simp

lemma drop_list_of:
"lfinite xs ⟹ drop n (list_of xs) = list_of (ldropn n xs)"
by (metis ldropn_llist_of list_of_llist_of llist_of_list_of)

lemma llength_ldrop: "llength (ldrop n xs) = (if n = ∞ then 0 else llength xs - n)"
proof(induct xs arbitrary: n)
case (LCons x xs)
thus ?case by simp(cases n rule: co.enat.exhaust, simp_all)
qed simp_all

lemma ltake_ldropn: "ltake n (ldropn m xs) = ldropn m (ltake (n + enat m) xs)"
by(induct m arbitrary: n xs)(auto simp add: zero_enat_def[symmetric] ldropn_Suc eSuc_enat[symmetric] iadd_Suc_right split: llist.split)

lemma ldropn_ltake: "ldropn n (ltake m xs) = ltake (m - enat n) (ldropn n xs)"
by(induct n arbitrary: m xs)(auto simp add: zero_enat_def[symmetric] ltake_LCons ldropn_Suc eSuc_enat[symmetric] iadd_Suc_right split: llist.split co.enat.split_asm)

lemma ltake_ldrop: "ltake n (ldrop m xs) = ldrop m (ltake (n + m) xs)"

lemma ldrop_ltake: "ldrop n (ltake m xs) = ltake (m - n) (ldrop n xs)"
by(induct xs arbitrary: n m)(simp_all add: ltake_LCons ldrop_LCons split: co.enat.split)

subsection ‹Taking the \$n\$-th element of a lazy list: @{term "lnth" }›

lemma lnth_LNil:
"lnth LNil n = undefined n"

lemma lnth_0 [simp]:
"lnth (LCons x xs) 0 = x"

lemma lnth_Suc_LCons [simp]:
"lnth (LCons x xs) (Suc n) = lnth xs n"

lemma lnth_LCons:
"lnth (LCons x xs) n = (case n of 0 ⇒ x | Suc n' ⇒ lnth xs n')"
by(cases n) simp_all

lemma lnth_LCons': "lnth (LCons x xs) n = (if n = 0 then x else lnth xs (n - 1))"

lemma lhd_conv_lnth:
"¬ lnull xs ⟹ lhd xs = lnth xs 0"

lemmas lnth_0_conv_lhd = lhd_conv_lnth[symmetric]

lemma lnth_ltl: "¬ lnull xs ⟹ lnth (ltl xs) n = lnth xs (Suc n)"

lemma lhd_ldropn:
"enat n < llength xs ⟹ lhd (ldropn n xs) = lnth xs n"
proof(induct n arbitrary: xs)
case 0 thus ?case by(cases xs) auto
next
case (Suc n)
from ‹enat (Suc n) < llength xs› obtain x xs'
where [simp]: "xs = LCons x xs'" by(cases xs) auto
from ‹enat (Suc n) < llength xs›
have "enat n < llength xs'" by(simp add: Suc_ile_eq)
hence "lhd (ldropn n xs') = lnth xs' n" by(rule Suc)
thus ?case by simp
qed

lemma lhd_ldrop:
assumes "n < llength xs"
shows "lhd (ldrop n xs) = lnth xs (the_enat n)"
proof -
from assms obtain n' where n: "n = enat n'" by(cases n) auto
from assms show ?thesis unfolding n
proof(induction n' arbitrary: xs)
case 0 thus ?case
next
case (Suc n')
thus ?case
qed
qed

lemma lnth_beyond:
"llength xs ≤ enat n ⟹ lnth xs n = undefined (n - (case llength xs of enat m ⇒ m))"
proof(induct n arbitrary: xs)
case 0 thus ?case by(simp add: zero_enat_def[symmetric] lnth_def lnull_def)
next
case Suc thus ?case
by(cases xs)(simp_all add: zero_enat_def lnth_def eSuc_enat[symmetric] split: enat.split, auto simp add: eSuc_enat)
qed

lemma lnth_lmap [simp]:
"enat n < llength xs ⟹ lnth (lmap f xs) n = f (lnth xs n)"
proof(induct n arbitrary: xs)
case 0 thus ?case by(cases xs) simp_all
next
case (Suc n)
from ‹enat (Suc n) < llength xs› obtain x xs'
where xs: "xs = LCons x xs'" and len: "enat n < llength xs'"
from len have "lnth (lmap f xs') n = f (lnth xs' n)" by(rule Suc)
with xs show ?case by simp
qed

lemma lnth_ldropn [simp]:
"enat (n + m) < llength xs ⟹ lnth (ldropn n xs) m = lnth xs (m + n)"
proof(induct n arbitrary: xs)
case (Suc n)
from ‹enat (Suc n + m) < llength xs›
obtain x xs' where "xs = LCons x xs'" by(cases xs) auto
moreover with ‹enat (Suc n + m) < llength xs›
have "enat (n + m) < llength xs'" by(simp add: Suc_ile_eq)
hence "lnth (ldropn n xs') m = lnth xs' (m + n)" by(rule Suc)
ultimately show ?case by simp
qed simp

lemma lnth_ldrop [simp]:
"n + enat m < llength xs ⟹ lnth (ldrop n xs) m = lnth xs (m + the_enat n)"

lemma in_lset_conv_lnth:
"x ∈ lset xs ⟷ (∃n. enat n < llength xs ∧ lnth xs n = x)"
(is "?lhs ⟷ ?rhs")
proof
assume ?rhs
then obtain n where "enat n < llength xs" "lnth xs n = x" by blast
thus ?lhs
proof(induct n arbitrary: xs)
case 0
thus ?case
next
case (Suc n)
thus ?case
qed
next
assume ?lhs
thus ?rhs
proof(induct)
case (find xs)
show ?case by(auto intro: exI[where x=0] simp add: zero_enat_def[symmetric])
next
case (step x' xs)
thus ?case
by(auto 4 4 intro: exI[where x="Suc n" for n] ileI1 simp add: eSuc_enat[symmetric])
qed
qed

lemma lset_conv_lnth: "lset xs = {lnth xs n|n. enat n < llength xs}"

lemma lnth_llist_of [simp]: "lnth (llist_of xs) = nth xs"
proof(rule ext)
fix n
show "lnth (llist_of xs) n = xs ! n"
proof(induct xs arbitrary: n)
case Nil thus ?case by(cases n)(simp_all add: nth_def lnth_def)
next
case Cons thus ?case by(simp add: lnth_LCons split: nat.split)
qed
qed

lemma nth_list_of [simp]:
assumes "lfinite xs"
shows "nth (list_of xs) = lnth xs"
using assms
by induct(auto intro: simp add: nth_def lnth_LNil nth_Cons split: nat.split)

lemma lnth_lappend1:
"enat n < llength xs ⟹ lnth (lappend xs ys) n = lnth xs n"
proof(induct n arbitrary: xs)
case 0 thus ?case by(auto simp add: zero_enat_def[symmetric] not_lnull_conv)
next
case (Suc n)
from ‹enat (Suc n) < llength xs› obtain x xs'
where [simp]: "xs = LCons x xs'" and len: "enat n < llength xs'"
from len have "lnth (lappend xs' ys) n = lnth xs' n" by(rule Suc)
thus ?case by simp
qed

lemma lnth_lappend_llist_of:
"lnth (lappend (llist_of xs) ys) n =
(if n < length xs then xs ! n else lnth ys (n - length xs))"
proof(induct xs arbitrary: n)
case (Cons x xs) thus ?case by(cases n) auto
qed simp

lemma lnth_lappend2:
"⟦ llength xs = enat k; k ≤ n ⟧ ⟹ lnth (lappend xs ys) n = lnth ys (n - k)"
proof(induct n arbitrary: xs k)
case 0 thus ?case by(simp add: zero_enat_def[symmetric] lappend_lnull1)
next
case (Suc n) thus ?case
by(cases xs)(auto simp add: eSuc_def zero_enat_def split: enat.split_asm)
qed

lemma lnth_lappend:
"lnth (lappend xs ys) n = (if enat n < llength xs then lnth xs n else lnth ys (n - the_enat (llength xs)))"
by(cases "llength xs")(auto simp add: lnth_lappend1 lnth_lappend2)

lemma lnth_ltake:
"enat m < n ⟹ lnth (ltake n xs) m = lnth xs m"
proof(induct m arbitrary: xs n)
case 0 thus ?case
by(cases n rule: enat_coexhaust)(auto, cases xs, auto)
next
case (Suc m)
from ‹enat (Suc m) < n› obtain n' where "n = eSuc n'"
by(cases n rule: enat_coexhaust) auto
with ‹enat (Suc m) < n› have "enat m < n'" by(simp add: eSuc_enat[symmetric])
with Suc ‹n = eSuc n'› show ?case by(cases xs) auto
qed

lemma ldropn_Suc_conv_ldropn:
"enat n < llength xs ⟹ LCons (lnth xs n) (ldropn (Suc n) xs) = ldropn n xs"
proof(induct n arbitrary: xs)
case 0 thus ?case by(cases xs) auto
next
case (Suc n)
from ‹enat (Suc n) < llength xs› obtain x xs'
where [simp]: "xs = LCons x xs'" by(cases xs) auto
from ‹enat (Suc n) < llength xs›
have "enat n < llength xs'" by(simp add: Suc_ile_eq)
hence "LCons (lnth xs' n) (ldropn (Suc n) xs') = ldropn n xs'" by(rule Suc)
thus ?case by simp
qed

lemma ltake_Suc_conv_snoc_lnth:
"enat m < llength xs ⟹ ltake (enat (Suc m)) xs = lappend (ltake (enat m) xs) (LCons (lnth xs m) LNil)"
by(metis eSuc_enat eSuc_plus_1 ltake_plus_conv_lappend ldrop_enat ldropn_Suc_conv_ldropn ltake_0 ltake_eSuc_LCons one_eSuc)

lemma lappend_eq_lappend_conv:
assumes len: "llength xs = llength us"
shows "lappend xs ys = lappend us vs ⟷
xs = us ∧ (lfinite xs ⟶ ys = vs)" (is "?lhs ⟷ ?rhs")
proof
assume ?rhs
thus ?lhs by(auto simp add: lappend_inf)
next
assume eq: ?lhs
show ?rhs
proof(intro conjI impI)
show "xs = us" using len eq
proof(coinduction arbitrary: xs us)
case (Eq_llist xs us)
thus ?case
by(cases xs us rule: llist.exhaust[case_product llist.exhaust]) auto
qed
assume "lfinite xs"
then obtain xs' where "xs = llist_of xs'"
hence "lappend (llist_of xs') ys = lappend (llist_of xs') vs"
using eq ‹xs = us› by blast
thus "ys = vs"
by (induct xs') simp_all
qed
qed

subsection‹iterates›

lemmas iterates [code, nitpick_simp] = iterates.ctr
and lnull_iterates = iterates.simps(1)
and lhd_iterates = iterates.simps(2)
and ltl_iterates = iterates.simps(3)

lemma lfinite_iterates [iff]: "¬ lfinite (iterates f x)"
proof
assume "lfinite (iterates f x)"
thus False
by(induct zs≡"iterates f x" arbitrary: x rule: lfinite_induct) auto
qed

lemma lmap_iterates: "lmap f (iterates f x) = iterates f (f x)"
by(coinduction arbitrary: x) auto

lemma iterates_lmap: "iterates f x = LCons x (lmap f (iterates f x))"

lemma lappend_iterates: "lappend (iterates f x) xs = iterates f x"
by(coinduction arbitrary: x) auto

lemma [simp]:
fixes f :: "'a ⇒ 'a"
shows lnull_funpow_lmap: "lnull ((lmap f ^^ n) xs) ⟷ lnull xs"
and lhd_funpow_lmap: "¬ lnull xs ⟹ lhd ((lmap f ^^ n) xs) = (f ^^ n) (lhd xs)"
and ltl_funpow_lmap: "¬ lnull xs ⟹ ltl ((lmap f ^^ n) xs) = (lmap f ^^ n) (ltl xs)"
by(induct n) simp_all

lemma iterates_equality:
assumes h: "⋀x. h x = LCons x (lmap f (h x))"
shows "h = iterates f"
proof -
{ fix x
have "¬ lnull (h x)" "lhd (h x) = x" "ltl (h x) = lmap f (h x)"
by(subst h, simp)+ }
note [simp] = this

{ fix x
define n :: nat where "n = 0"
have "(lmap f ^^ n) (h x) = (lmap f ^^ n) (iterates f x)"
by(coinduction arbitrary: n)(auto simp add: funpow_swap1 lmap_iterates intro: exI[where x="Suc n" for n]) }
thus ?thesis by auto
qed

lemma llength_iterates [simp]: "llength (iterates f x) = ∞"
by(coinduction arbitrary: x rule: enat_coinduct)(auto simp add: epred_llength)

lemma ldropn_iterates: "ldropn n (iterates f x) = iterates f ((f ^^ n) x)"
proof(induct n arbitrary: x)
case 0 thus ?case by simp
next
case (Suc n)
have "ldropn (Suc n) (iterates f x) = ldropn n (iterates f (f x))"
by(subst iterates)simp
also have "… = iterates f ((f ^^ n) (f x))" by(rule Suc)
finally show ?case by(simp add: funpow_swap1)
qed

lemma ldrop_iterates: "ldrop (enat n) (iterates f x) = iterates f ((f ^^ n) x)"
proof(induct n arbitrary: x)
case Suc thus ?case

lemma lnth_iterates [simp]: "lnth (iterates f x) n = (f ^^ n) x"
proof(induct n arbitrary: x)
case 0 thus ?case by(subst iterates) simp
next
case (Suc n)
hence "lnth (iterates f (f x)) n = (f ^^ n) (f x)" .
thus ?case by(subst iterates)(simp add: funpow_swap1)
qed

lemma lset_iterates:
"lset (iterates f x) = {(f ^^ n) x|n. True}"

lemma lset_repeat [simp]: "lset (repeat x) = {x}"

subsection ‹
More on the prefix ordering on lazy lists: @{term "lprefix"} and @{term "lstrict_prefix"}
›

lemma lstrict_prefix_code [code, simp]:
"lstrict_prefix LNil LNil ⟷ False"
"lstrict_prefix LNil (LCons y ys) ⟷ True"
"lstrict_prefix (LCons x xs) LNil ⟷ False"
"lstrict_prefix (LCons x xs) (LCons y ys) ⟷ x = y ∧ lstrict_prefix xs ys"

lemma lmap_lprefix: "xs ⊑ ys ⟹ lmap f xs ⊑ lmap f ys"
by(rule monotoneD[OF monotone_lmap])

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

lemma lprefix_llength_le: "xs ⊑ ys ⟹ llength xs ≤ llength ys"
using monotone_llength by(rule monotoneD)

lemma lstrict_prefix_llength_less:
assumes "lstrict_prefix xs ys"
shows "llength xs < llength ys"
proof(rule ccontr)
assume "¬ llength xs < llength ys"
moreover from ‹lstrict_prefix xs ys› have "xs ⊑ ys" "xs ≠ ys"
unfolding lstrict_prefix_def by simp_all
from ‹xs ⊑ ys› have "llength xs ≤ llength ys"
by(rule lprefix_llength_le)
ultimately have "llength xs = llength ys" by auto
with ‹xs ⊑ ys› have "xs = ys"
by(rule lprefix_llength_eq_imp_eq)
with ‹xs ≠ ys› show False by contradiction
qed

lemma lstrict_prefix_lfinite1: "lstrict_prefix xs ys ⟹ lfinite xs"
by (metis lstrict_prefix_def not_lfinite_lprefix_conv_eq)

lemma wfP_lstrict_prefix: "wfP lstrict_prefix"
proof(unfold wfP_def)
have "wf {(x :: enat, y). x < y}"
unfolding wf_def by(blast intro: less_induct)
hence "wf (inv_image {(x, y). x < y} llength)" by(rule wf_inv_image)
moreover have "{(xs, ys). lstrict_prefix xs ys} ⊆ inv_image {(x, y). x < y} llength"
by(auto intro: lstrict_prefix_llength_less)
ultimately show "wf {(xs, ys). lstrict_prefix xs ys}" by(rule wf_subset)
qed

lemma llist_less_induct[case_names less]:
"(⋀xs. (⋀ys. lstrict_prefix ys xs ⟹ P ys) ⟹ P xs) ⟹ P xs"
by(rule wfP_induct[OF wfP_lstrict_prefix]) blast

lemma ltake_enat_eq_imp_eq: "(⋀n. ltake (enat n) xs = ltake (enat n) ys) ⟹ xs = ys"
by(coinduction arbitrary: xs ys)(auto simp add: zero_enat_def lnull_def neq_LNil_conv ltake_eq_LNil_iff eSuc_enat[symmetric] elim: allE[where x="Suc n" for n])

lemma ltake_enat_lprefix_imp_lprefix:
assumes "⋀n. lprefix (ltake (enat n) xs) (ltake (enat n) ys)"
shows "lprefix xs ys"
proof -
have "ccpo.admissible Sup (≤) (λn. ltake n xs ⊑ ltake n ys)" by simp
hence "ltake (Sup (range enat)) xs ⊑ ltake (Sup (range enat)) ys"
qed

lemma lprefix_conv_lappend: "xs ⊑ ys ⟷ (∃zs. ys = lappend xs zs)" (is "?lhs ⟷ ?rhs")
proof(rule iffI)
assume ?lhs
hence "ys = lappend xs (ldrop (llength xs) ys)"
by(coinduction arbitrary: xs ys)(auto dest: lprefix_lnullD lprefix_lhdD intro: lprefix_ltlI simp add: not_lnull_conv lprefix_LCons_conv intro: exI[where x=LNil])
thus ?rhs ..
next
assume ?rhs
thus ?lhs by(coinduct rule: lprefix_coinduct) auto
qed

lemma lappend_lprefixE:
assumes "lappend xs ys ⊑ zs"
obtains zs' where "zs = lappend xs zs'"
using assms unfolding lprefix_conv_lappend by(auto simp add: lappend_assoc)

lemma lprefix_lfiniteD:
"⟦ xs ⊑ ys; lfinite ys ⟧ ⟹ lfinite xs"
unfolding lprefix_conv_lappend by auto

lemma lprefix_lappendD:
assumes "xs ⊑ lappend ys zs"
shows "xs ⊑ ys ∨ ys ⊑ xs"
proof(rule ccontr)
assume "¬ (xs ⊑ ys ∨ ys ⊑ xs)"
hence "¬ xs ⊑ ys" "¬ ys ⊑ xs" by simp_all
from ‹xs ⊑ lappend ys zs› obtain xs'
where "lappend xs xs' = lappend ys zs"
unfolding lprefix_conv_lappend by auto
hence eq: "lappend (ltake (llength ys) xs) (lappend (ldrop (llength ys) xs) xs') =
lappend ys zs"
unfolding lappend_assoc[symmetric] by(simp only: lappend_ltake_ldrop)
moreover have "llength xs ≥ llength ys"
proof(rule ccontr)
assume "¬ ?thesis"
hence "llength xs < llength ys" by simp
hence "ltake (llength ys) xs = xs" by(simp add: ltake_all)
hence "lappend xs (lappend (ldrop (llength ys) xs) xs') =
lappend (ltake (llength xs) ys) (lappend (ldrop (llength xs) ys) zs)"
unfolding lappend_assoc[symmetric] lappend_ltake_ldrop
hence xs: "xs = ltake (llength xs) ys" using ‹llength xs < llength ys›
by(subst (asm) lappend_eq_lappend_conv)(auto simp add: min_def)
have "xs ⊑ ys" by(subst xs) auto
with ‹¬ xs ⊑ ys› show False by contradiction
qed
ultimately have ys: "ys = ltake (llength ys) xs"
have "ys ⊑ xs" by(subst ys) auto
with ‹¬ ys ⊑ xs› show False by contradiction
qed

lemma lstrict_prefix_lappend_conv:
"lstrict_prefix xs (lappend xs ys) ⟷ lfinite xs ∧ ¬ lnull ys"
proof -
{ assume "lfinite xs" "xs = lappend xs ys"
hence "lnull ys" by induct auto }
thus ?thesis
by(auto simp add: lstrict_prefix_def lprefix_lappend lappend_inf lappend_lnull2
elim: contrapos_np)
qed

lemma lprefix_llist_ofI:
"∃zs. ys = xs @ zs ⟹ llist_of xs ⊑ llist_of ys"

lemma lprefix_llist_of [simp]: "llist_of xs ⊑ llist_of ys ⟷ prefix xs ys"
by(auto simp add: prefix_def lprefix_conv_lappend)(metis lfinite_lappend lfinite_llist_of list_of_lappend list_of_llist_of lappend_llist_of_llist_of)+

lemma llimit_induct [case_names LNil LCons limit]:
― ‹The limit case is just an instance of admissibility›
assumes LNil: "P LNil"
and LCons: "⋀x xs. ⟦ lfinite xs; P xs ⟧ ⟹ P (LCons x xs)"
and limit: "(⋀ys. lstrict_prefix ys xs ⟹ P ys) ⟹ P xs"
shows "P xs"
proof(rule limit)
fix ys
assume "lstrict_prefix ys xs"
hence "lfinite ys" by(rule lstrict_prefix_lfinite1)
thus "P ys" by(induct)(blast intro: LNil LCons)+
qed

lemma lmap_lstrict_prefix:
"lstrict_prefix xs ys ⟹ lstrict_prefix (lmap f xs) (lmap f ys)"
by (metis llength_lmap lmap_lprefix lprefix_llength_eq_imp_eq lstrict_prefix_def)

lemma lprefix_lnthD:
assumes "xs ⊑ ys" and "enat n < llength xs"
shows "lnth xs n = lnth ys n"
using assms by (metis lnth_lappend1 lprefix_conv_lappend)

lemma lfinite_lSup_chain:
assumes chain: "Complete_Partial_Order.chain (⊑) A"
shows "lfinite (lSup A) ⟷ finite A ∧ (∀xs ∈ A. lfinite xs)" (is "?lhs ⟷ ?rhs")
proof(intro iffI conjI)
assume ?lhs
then obtain n where n: "llength (lSup A) = enat n" unfolding lfinite_conv_llength_enat ..
have "llength ` A ⊆ {..<enat (Suc n)}"
by(auto dest!: chain_lprefix_lSup[OF chain] lprefix_llength_le simp add: n intro: le_less_trans)
hence "finite (llength ` A)" by(rule finite_subset)(simp add: finite_lessThan_enat_iff)
moreover have "inj_on llength A" by(rule inj_onI)(auto 4 3 dest: chainD[OF chain] lprefix_llength_eq_imp_eq)
ultimately show "finite A" by(rule finite_imageD)
next
assume ?rhs
hence "finite A" "∀xs∈A. lfinite xs" by simp_all
show ?lhs
proof(cases "A = {}")
case False
with chain ‹finite A›
have "lSup A ∈ A" by(rule ccpo.in_chain_finite[OF llist_ccpo])
with ‹∀xs∈A. lfinite xs› show ?thesis ..
qed simp
qed(rule lfinite_lSupD)

text ‹Setup for @{term "lprefix"} for Nitpick›

definition finite_lprefix :: "'a llist ⇒ 'a llist ⇒ bool"
where "finite_lprefix = (⊑)"

lemma finite_lprefix_nitpick_simps [nitpick_simp]:
"finite_lprefix xs LNil ⟷ xs = LNil"
"finite_lprefix LNil xs ⟷ True"
"finite_lprefix xs (LCons y ys) ⟷
xs = LNil ∨ (∃xs'. xs = LCons y xs' ∧ finite_lprefix xs' ys)"

lemma lprefix_nitpick_simps [nitpick_simp]:
"xs ⊑ ys = (if lfinite xs then finite_lprefix xs ys else xs = ys)"

hide_const (open) finite_lprefix
hide_fact (open) finite_lprefix_def finite_lprefix_nitpick_simps lprefix_nitpick_simps

subsection ‹Length of the longest common prefix›

lemma llcp_simps [simp, code, nitpick_simp]:
shows llcp_LNil1: "llcp LNil ys = 0"
and llcp_LNil2: "llcp xs LNil = 0"
and llcp_LCons: "llcp (LCons x xs) (LCons y ys) = (if x = y then eSuc (llcp xs ys) else 0)"
by(simp_all add: llcp_def enat_unfold split: llist.split)

lemma llcp_eq_0_iff:
"llcp xs ys = 0 ⟷ lnull xs ∨ lnull ys ∨ lhd xs ≠ lhd ys"

lemma epred_llcp:
"⟦ ¬ lnull xs; ¬ lnull ys; lhd xs = lhd ys ⟧
⟹  epred (llcp xs ys) = llcp (ltl xs) (ltl ys)"

lemma llcp_commute: "llcp xs ys = llcp ys xs"
by(coinduction arbitrary: xs ys rule: enat_coinduct)(auto simp add: llcp_eq_0_iff epred_llcp)

lemma llcp_same_conv_length [simp]: "llcp xs xs = llength xs"
by(coinduction arbitrary: xs rule: enat_coinduct)(auto simp add: llcp_eq_0_iff epred_llcp epred_llength)

lemma llcp_lappend_same [simp]:
"llcp (lappend xs ys) (lappend xs zs) = llength xs + llcp ys zs"

lemma llcp_lprefix1 [simp]: "xs ⊑ ys ⟹ llcp xs ys = llength xs"
by (metis add_0_right lappend_LNil2 llcp_LNil1 llcp_lappend_same lprefix_conv_lappend)

lemma llcp_lprefix2 [simp]: "ys ⊑ xs ⟹ llcp xs ys = llength ys"
by (metis llcp_commute llcp_lprefix1)

lemma llcp_le_length: "llcp xs ys ≤ min (llength xs) (llength ys)"
proof -
define m n where "m = llcp xs ys" and "n = min (llength xs) (llength ys)"
hence "(m, n) ∈ {(llcp xs ys, min (llength xs) (llength ys)) |xs ys :: 'a llist. True}" by blast
thus "m ≤ n"
proof(coinduct rule: enat_leI)
case (Leenat m n)
then obtain xs ys :: "'a llist" where "m = llcp xs ys" "n = min (llength xs) (llength ys)" by blast
thus ?case
by(cases xs ys rule: llist.exhaust[case_product llist.exhaust])(auto 4 3 intro!: exI[where x="Suc 0"] simp add: eSuc_enat[symmetric] iadd_Suc_right zero_enat_def[symmetric])
qed
qed

lemma llcp_ltake1: "llcp (ltake n xs) ys = min n (llcp xs ys)"
by(coinduction arbitrary: n xs ys rule: enat_coinduct)(auto simp add: llcp_eq_0_iff enat_min_eq_0_iff epred_llcp ltl_ltake)

lemma llcp_ltake2: "llcp xs (ltake n ys) = min n (llcp xs ys)"
by(metis llcp_commute llcp_ltake1)

lemma llcp_ltake [simp]: "llcp (ltake n xs) (ltake m ys) = min (min n m) (llcp xs ys)"
by(metis llcp_ltake1 llcp_ltake2 min.assoc)

subsection ‹Zipping two lazy lists to a lazy list of pairs @{term "lzip" }›

lemma lzip_simps [simp, code, nitpick_simp]:
"lzip LNil ys = LNil"
"lzip xs LNil = LNil"
"lzip (LCons x xs) (LCons y ys) = LCons (x, y) (lzip xs ys)"
by(auto intro: llist.expand)

lemma lnull_lzip [simp]: "lnull (lzip xs ys) ⟷ lnull xs ∨ lnull ys"

lemma lzip_eq_LNil_conv: "lzip xs ys = LNil ⟷ xs = LNil ∨ ys = LNil"
using lnull_lzip unfolding lnull_def .

lemmas lhd_lzip = lzip.sel(1)
and ltl_lzip = lzip.sel(2)

lemma lzip_eq_LCons_conv:
"lzip xs ys = LCons z zs ⟷
(∃x xs' y ys'. xs = LCons x xs' ∧ ys = LCons y ys' ∧ z = (x, y) ∧ zs = lzip xs' ys')"
by(cases xs ys rule: llist.exhaust[case_product llist.exhaust]) auto

lemma lzip_lappend:
"llength xs = llength us
⟹ lzip (lappend xs ys) (lappend us vs) = lappend (lzip xs us) (lzip ys vs)"
by(coinduction arbitrary: xs ys us vs rule: llist.coinduct_strong)(auto 4 6 simp add: llength_ltl)

lemma llength_lzip [simp]:
"llength (lzip xs ys) = min (llength xs) (llength ys)"
by(coinduction arbitrary: xs ys rule: enat_coinduct)(auto simp add: enat_min_eq_0_iff epred_llength)

lemma ltake_lzip: "ltake n (lzip xs ys) = lzip (ltake n xs) (ltake n ys)"
by(coinduction arbitrary: xs ys n)(auto simp add: ltl_ltake)

lemma ldropn_lzip [simp]:
"ldropn n (lzip xs ys) = lzip (ldropn n xs) (ldropn n ys)"
by(induct n arbitrary: xs ys)(simp_all add: ldropn_Suc split: llist.split)

lemma
fixes F
defines "F ≡ λlzip (xs, ys). case xs of LNil ⇒ LNil | LCons x xs' ⇒ case ys of LNil ⇒ LNil | LCons y ys' ⇒ LCons (x, y) (curry lzip xs' ys')"
shows lzip_conv_fixp: "lzip ≡ curry (ccpo.fixp (fun_lub lSup) (fun_ord (⊑)) F)" (is "?lhs ≡ ?rhs")
and lzip_mono: "mono_llist (λlzip. F lzip xs)" (is "?mono xs")
proof(intro eq_reflection ext)
show mono: "⋀xs. ?mono xs" unfolding F_def by(tactic ‹Partial_Function.mono_tac @{context} 1›)
fix xs ys
show "lzip xs ys = ?rhs xs ys"
proof(coinduction arbitrary: xs ys)
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 monotone_lzip: "monotone (rel_prod (⊑) (⊑)) (⊑) (case_prod lzip)"
by(rule llist.fixp_preserves_mono2[OF lzip_mono lzip_conv_fixp]) simp

lemma mono2mono_lzip1 [THEN llist.mono2mono, cont_intro, simp]:
shows monotone_lzip1: "monotone (⊑) (⊑) (λxs. lzip xs ys)"

lemma mono2mono_lzip2 [THEN llist.mono2mono, cont_intro, simp]:
shows monotone_lzip2: "monotone (⊑) (⊑) (λys. lzip xs ys)"

lemma mcont_lzip: "mcont (prod_lub lSup lSup) (rel_prod (⊑) (⊑)) lSup (⊑) (case_prod lzip)"
by(rule llist.fixp_preserves_mcont2[OF lzip_mono lzip_conv_fixp]) simp

lemma mcont2mcont_lzip1 [THEN llist.mcont2mcont, cont_intro, simp]:
shows mcont_lzip1: "mcont lSup (⊑) lSup (⊑) (λxs. lzip xs ys)"

lemma mcont2mcont_lzip2 [THEN llist.mcont2mcont, cont_intro, simp]:
shows mcont_lzip2: "mcont lSup (⊑) lSup (⊑) (λys. lzip xs ys)"

lemma ldrop_lzip [simp]: "ldrop n (lzip xs ys) = lzip (ldrop n xs) (ldrop n ys)"
proof(induct xs arbitrary: ys n)
case LCons
thus ?case by(cases ys n rule: llist.exhaust[case_product co.enat.exhaust]) simp_all
qed simp_all

lemma lzip_iterates:
"lzip (iterates f x) (iterates g y) = iterates (λ(x, y). (f x, g y)) (x, y)"
by(coinduction arbitrary: x y) auto

lemma lzip_llist_of [simp]:
"lzip (llist_of xs) (llist_of ys) = llist_of (zip xs ys)"
proof(induct xs arbitrary: ys)
case (Cons x xs')
thus ?case by(cases ys) simp_all
qed simp

lemma lnth_lzip:
"⟦ enat n < llength xs; enat n < llength ys ⟧
⟹ lnth (lzip xs ys) n = (lnth xs n, lnth ys n)"
proof(induct n arbitrary: xs ys)
case 0 thus ?case
next
case (Suc n)
thus ?case
by(cases xs ys rule: llist.exhaust[case_product llist.exhaust])(auto simp add: eSuc_enat[symmetric])
qed

lemma lset_lzip:
"lset (lzip xs ys) =
{(lnth xs n, lnth ys n)|n. enat n < min (llength xs) (llength ys)}"

lemma lset_lzipD1: "(x, y) ∈ lset (lzip xs ys) ⟹ x ∈ lset xs"
proof(induct "lzip xs ys" arbitrary: xs ys rule: lset_induct)
case [symmetric]: find
thus ?case by(auto simp add: lzip_eq_LCons_conv)
next
case (step z zs)
thus ?case by -(drule sym, auto simp add: lzip_eq_LCons_conv)
qed

lemma lset_lzipD2: "(x, y) ∈ lset (lzip xs ys) ⟹ y ∈ lset ys"
proof(induct "lzip xs ys" arbitrary: xs ys rule: lset_induct)
case [symmetric]: find
thus ?case by(auto simp add: lzip_eq_LCons_conv)
next
case (step z zs)
thus ?case by -(drule sym, auto simp add: lzip_eq_LCons_conv)
qed

lemma lset_lzip_same [simp]: "lset (lzip xs xs) = (λx. (x, x)) ` lset xs"
by(auto 4 3 simp add: lset_lzip in_lset_conv_lnth)

lemma lfinite_lzip [simp]:
"lfinite (lzip xs ys) ⟷ lfinite xs ∨ lfinite ys" (is "?lhs ⟷ ?rhs")
proof
assume ?lhs
thus ?rhs
by(induct zs≡"lzip xs ys" arbitrary: xs ys rule: lfinite_induct) fastforce+
next
assume ?rhs (is "?xs ∨ ?ys")
thus ?lhs
proof
assume ?xs
thus ?thesis
proof(induct arbitrary: ys)
case (lfinite_LConsI xs x)
thus ?case by(cases ys) simp_all
qed simp
next
assume ?ys
thus ?thesis
proof(induct arbitrary: xs)
case (lfinite_LConsI ys y)
thus ?case by(cases xs) simp_all
qed simp
qed
qed

lemma lzip_eq_lappend_conv:
assumes eq: "lzip xs ys = lappend us vs"
shows "∃xs' xs'' ys' ys''. xs = lappend xs' xs'' ∧ ys = lappend ys' ys'' ∧
llength xs' = llength ys' ∧ us = lzip xs' ys' ∧
vs = lzip xs'' ys''"
proof -
let ?xs' = "ltake (llength us) xs"
let ?xs'' = "ldrop (llength us) xs"
let ?ys' = "ltake (llength us) ys"
let ?ys'' = "ldrop (llength us) ys"

from eq have "llength (lzip xs ys) = llength (lappend us vs)" by simp
hence "min (llength xs) (llength ys) ≥ llength us"
hence len: "llength xs ≥ llength us" "llength ys ≥ llength us" by(auto)

hence leneq: "llength ?xs' = llength ?ys'" by(simp add: min_def)
have xs: "xs = lappend ?xs' ?xs''" and ys: "ys = lappend ?ys' ?ys''"
hence "lappend us vs = lzip (lappend ?xs' ?xs'') (lappend ?ys' ?ys'')"
using eq by simp
with len have "lappend us vs = lappend (lzip ?xs' ?ys') (lzip ?xs'' ?ys'')"
hence us: "us = lzip ?xs' ?ys'"
and vs: "lfinite us ⟶ vs = lzip ?xs'' ?ys''" using len
show ?thesis
proof(cases "lfinite us")
case True
with leneq xs ys us vs len show ?thesis by fastforce
next
case False
let ?xs'' = "lmap fst vs"
let ?ys'' = "lmap snd vs"
from False have "lappend us vs = us" by(simp add: lappend_inf)
moreover from False have "llength us = ∞"
by(rule not_lfinite_llength)
moreover with len
have "llength xs = ∞" "llength ys = ∞" by auto
moreover with ‹llength us = ∞›
have "xs = ?xs'" "ys = ?ys'" by(simp_all add: ltake_all)
from ‹llength us = ∞› len
have "¬ lfinite ?xs'" "¬ lfinite ?ys'"
by(auto simp del: llength_ltake lfinite_ltake
with ‹xs = ?xs'› ‹ys = ?ys'›
have "xs = lappend ?xs' ?xs''" "ys = lappend ?ys' ?ys''"
moreover have "vs = lzip ?xs'' ?ys''"
by(coinduction arbitrary: vs) auto
ultimately show ?thesis using eq by(fastforce simp add: ltake_all)
qed
qed

lemma lzip_lmap [simp]:
"lzip (lmap f xs) (lmap g ys) = lmap (λ(x, y). (f x, g y)) (lzip xs ys)"
by(coinduction arbitrary: xs ys) auto

lemma lzip_lmap1:
"lzip (lmap f xs) ys = lmap (λ(x, y). (f x, y)) (lzip xs ys)"
by(subst (4) llist.map_ident[symmetric])(simp only: lzip_lmap)

lemma lzip_lmap2:
"lzip xs (lmap f ys) = lmap (λ(x, y). (x, f y)) (lzip xs ys)"
by(subst (1) llist.map_ident[symmetric])(simp only: lzip_lmap)

lemma lmap_fst_lzip_conv_ltake:
"lmap fst (lzip xs ys) = ltake (min (llength xs) (llength ys)) xs"
by(coinduction arbitrary: xs ys)(auto simp add: enat_min_eq_0_iff ltl_ltake epred_llength)

lemma lmap_snd_lzip_conv_ltake:
"lmap snd (lzip xs ys) = ltake (min (llength xs) (llength ys)) ys"
by(coinduction arbitrary: xs ys)(auto simp add: enat_min_eq_0_iff ltl_ltake epred_llength)

lemma lzip_conv_lzip_ltake_min_llength:
"lzip xs ys =
lzip (ltake (min (llength xs) (llength ys)) xs)
(ltake (min (llength xs) (llength ys)) ys)"
by(coinduction arbitrary: xs ys)(auto simp add: enat_min_eq_0_iff ltl_ltake epred_llength)

subsection ‹Taking and dropping from a lazy list: @{term "ltakeWhile"} and @{term "ldropWhile"}›

lemma ltakeWhile_simps [simp, code, nitpick_simp]:
shows ltakeWhile_LNil: "ltakeWhile P LNil = LNil"
and ltakeWhile_LCons: "ltakeWhile P (LCons x xs) = (if P x then LCons x (ltakeWhile P xs) else LNil)"
by(auto simp add: ltakeWhile_def intro: llist.expand)

lemma ldropWhile_simps [simp, code]:
shows ldropWhile_LNil: "ldropWhile P LNil = LNil"
and ldropWhile_LCons: "ldropWhile P (LCons x xs) = (if P x then ldropWhile P xs else LCons x xs)"

lemma fixes f F P
defines "F ≡ λltakeWhile xs. case xs of LNil ⇒ LNil | LCons x xs ⇒ if P x then LCons x (ltakeWhile xs) else LNil"
shows ltakeWhile_conv_fixp: "ltakeWhile P ≡ ccpo.fixp (fun_lub lSup) (fun_ord lprefix) F" (is "?lhs ≡ ?rhs")
and ltakeWhile_mono: "⋀xs. mono_llist (λltakeWhile. F ltakeWhile 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 prod.split co.enat.split)
qed
qed

lemma mono2mono_ltakeWhile[THEN llist.mono2mono, cont_intro, simp]:
shows monotone_ltakeWhile: "monotone lprefix lprefix (ltakeWhile P)"
by(rule llist.fixp_preserves_mono1[OF ltakeWhile_mono ltakeWhile_conv_fixp]) simp

lemma mcont2mcont_ltakeWhile [THEN llist.mcont2mcont, cont_intro, simp]:
shows mcont_ltakeWhile: "mcont lSup lprefix lSup lprefix (ltakeWhile P)"
by(rule llist.fixp_preserves_mcont1[OF ltakeWhile_mono ltakeWhile_conv_fixp]) simp

lemma mono_llist_ltakeWhile [partial_function_mono]:
"mono_llist F ⟹ mono_llist (λf. ltakeWhile P (F f))"
by(rule mono2mono_ltakeWhile)

lemma mono2mono_ldropWhile [THEN llist.mono2mono, cont_intro, simp]:
shows monotone_ldropWhile: "monotone (⊑) (⊑) (ldropWhile P)"
by(rule llist.fixp_preserves_mono1[OF ldropWhile.mono ldropWhile_def]) simp

lemma mcont2mcont_ldropWhile [THEN llist.mcont2mcont, cont_intro, simp]:
shows mcont_ldropWhile: "mcont lSup (⊑) lSup (⊑) (ldropWhile P)"
by(rule llist.fixp_preserves_mcont1[OF ldropWhile.mono ldropWhile_def]) simp

lemma lnull_ltakeWhile [simp]: "lnull (ltakeWhile P xs) ⟷ (¬ lnull xs ⟶ ¬ P (lhd xs))"
by(cases xs) simp_all

lemma ltakeWhile_eq_LNil_iff: "ltakeWhile P xs = LNil ⟷ (xs ≠ LNil ⟶ ¬ P (lhd xs))"
using lnull_ltakeWhile unfolding lnull_def .

lemmas lhd_ltakeWhile = ltakeWhile.sel(1)

lemma ltl_ltakeWhile:
"ltl (ltakeWhile P xs) = (if P (lhd xs) then ltakeWhile P (ltl xs) else LNil)"
by(cases xs) simp_all

lemma lprefix_ltakeWhile: "ltakeWhile P xs ⊑ xs"
by(coinduction arbitrary: xs)(auto simp add: ltl_ltakeWhile)

lemma llength_ltakeWhile_le: "llength (ltakeWhile P xs) ≤ llength xs"
by(rule lprefix_llength_le)(rule lprefix_ltakeWhile)

lemma ltakeWhile_nth: "enat i < llength (ltakeWhile P xs) ⟹ lnth (ltakeWhile P xs) i = lnth xs i"
by(rule lprefix_lnthD[OF lprefix_ltakeWhile])

lemma ltakeWhile_all: "∀x∈lset xs. P x ⟹ ltakeWhile P xs = xs"
by(coinduction arbitrary: xs)(auto 4 3 simp add: ltl_ltakeWhile simp del: ltakeWhile.disc_iff dest: in_lset_ltlD)

lemma lset_ltakeWhileD:
assumes "x ∈ lset (ltakeWhile P xs)"
shows "x ∈ lset xs ∧ P x"
using assms
by(induct ys≡"ltakeWhile P xs" arbitrary: xs rule: llist_set_induct)(auto simp add: ltl_ltakeWhile dest: in_lset_ltlD)

lemma lset_ltakeWhile_subset:
"lset (ltakeWhile P xs) ⊆ lset xs ∩ {x. P x}"
by(auto dest: lset_ltakeWhileD)

lemma ltakeWhile_all_conv: "ltakeWhile P xs = xs ⟷ lset xs ⊆ {x. P x}"
by (metis Int_Collect Int_absorb2 le_infE lset_ltakeWhile_subset ltakeWhile_all)

lemma llength_ltakeWhile_all: "llength (ltakeWhile P xs) = llength xs ⟷ ltakeWhile P xs = xs"
by(auto intro: lprefix_llength_eq_imp_eq lprefix_ltakeWhile)

lemma ldropWhile_eq_LNil_iff: "ldropWhile P xs = LNil ⟷ (∀x ∈ lset xs. P x)"
by(induct xs) simp_all

lemma lnull_ldropWhile [simp]:
"lnull (ldropWhile P xs) ⟷ (∀x ∈ lset xs. P x)" (is "?lhs ⟷ ?rhs")

lemma lset_ldropWhile_subset:
"lset (ldropWhile P xs) ⊆ lset xs"
by(induct xs) auto

lemma in_lset_ldropWhileD: "x ∈ lset (ldropWhile P xs) ⟹ x ∈ lset xs"
using lset_ldropWhile_subset[of P xs] by auto

lemma ltakeWhile_lmap: "ltakeWhile P (lmap f xs) = lmap f (ltakeWhile (P ∘ f) xs)"
by(coinduction arbitrary: xs)(auto simp add: ltl_ltakeWhile)

lemma ldropWhile_lmap: "ldropWhile P (lmap f xs) = lmap f (ldropWhile (P ∘ f) xs)"
by(induct xs) simp_all

lemma llength_ltakeWhile_lt_iff: "llength (ltakeWhile P xs) < llength xs ⟷ (∃x∈lset xs. ¬ P x)"
(is "?lhs ⟷ ?rhs")
proof
assume ?lhs
hence "ltakeWhile P xs ≠ xs" by auto
thus ?rhs by(auto simp add: ltakeWhile_all_conv)
next
assume ?rhs
hence "ltakeWhile P xs ≠ xs" by(auto simp add: ltakeWhile_all_conv)
thus ?lhs unfolding llength_ltakeWhile_all[symmetric]
using llength_ltakeWhile_le[of P xs] by(auto)
qed

lemma ltakeWhile_K_False [simp]: "ltakeWhile (λ_. False) xs = LNil"

lemma ltakeWhile_K_True [simp]: "ltakeWhile (λ_. True) xs = xs"
by(coinduction arbitrary: xs) simp

lemma ldropWhile_K_False [simp]: "ldropWhile (λ_. False) = id"
proof
fix xs
show "ldropWhile (λ_. False) xs = id xs"
by(induct xs) simp_all
qed

lemma ldropWhile_K_True [simp]: "ldropWhile (λ_. True) xs = LNil"
by(induct xs)(simp_all)

lemma lappend_ltakeWhile_ldropWhile [simp]:
"lappend (ltakeWhile P xs) (ldropWhile P xs) = xs"
by(coinduction arbitrary: xs rule: llist.coinduct_strong)(auto 4 4 simp add: not_lnull_conv lset_lnull intro: ccontr)

lemma ltakeWhile_lappend:
"ltakeWhile P (lappend xs ys) =
(if ∃x∈lset xs. ¬ P x then ltakeWhile P xs
else lappend xs (ltakeWhile P ys))"
proof(coinduction arbitrary: xs rule: llist.coinduct_strong)
case (Eq_llist xs)
have ?lnull by(auto simp add: lset_lnull)
moreover have ?LCons
by(clarsimp split: if_split_asm split del: if_split simp add: ltl_ltakeWhile)(auto 4 3 simp add: not_lnull_conv)
ultimately show ?case ..
qed

lemma ldropWhile_lappend:
"ldropWhile P (lappend xs ys) =
(if ∃x∈lset xs. ¬ P x then lappend (ldropWhile P xs) ys
else if lfinite xs then ldropWhile P ys else LNil)"
proof(cases "∃x∈lset xs. ¬ P x")
case True
then obtain x where "x ∈ lset xs" "¬ P x"  by blast
thus ?thesis by induct simp_all
next
case False
note xs = this
show ?thesis
proof(cases "lfinite xs")
case False
thus ?thesis using xs by(simp add: lappend_inf)
next
case True
thus ?thesis using xs by induct simp_all
qed
qed

lemma lfinite_ltakeWhile:
"lfinite (ltakeWhile P xs) ⟷ lfinite xs ∨ (∃x ∈ lset xs. ¬ P x)" (is "?lhs ⟷ ?rhs")
proof
assume ?lhs
thus ?rhs by(auto simp add: ltakeWhile_all)
next
assume "?rhs"
thus ?lhs
proof
assume "lfinite xs"
with lprefix_ltakeWhile show ?thesis by(rule lprefix_lfiniteD)
next
assume "∃x∈lset xs. ¬ P x"
then obtain x where "x ∈ lset xs" "¬ P x" by blast
thus ?thesis by(induct rule: lset_induct) simp_all
qed
qed

lemma llength_ltakeWhile_eq_infinity:
"llength (ltakeWhile P xs) = ∞ ⟷ ¬ lfinite xs ∧ ltakeWhile P xs = xs"
unfolding llength_ltakeWhile_all[symmetric] llength_eq_infty_conv_lfinite[symmetric]
by(auto)(auto simp add: llength_eq_infty_conv_lfinite lfinite_ltakeWhile intro: sym)

lemma llength_ltakeWhile_eq_infinity':
"llength (ltakeWhile P xs) = ∞ ⟷ ¬ lfinite xs ∧ (∀x∈lset xs. P x)"
by (metis lfinite_ltakeWhile llength_eq_infty_conv_lfinite)

lemma lzip_ltakeWhile_fst: "lzip (ltakeWhile P xs) ys = ltakeWhile (P ∘ fst) (lzip xs ys)"
by(coinduction arbitrary: xs ys)(auto simp add: ltl_ltakeWhile simp del: simp del: ltakeWhile.disc_iff)

lemma lzip_ltakeWhile_snd: "lzip xs (ltakeWhile P ys) = ltakeWhile (P ∘ snd) (lzip xs ys)"
by(coinduction arbitrary: xs ys)(auto simp add: ltl_ltakeWhile)

lemma ltakeWhile_lappend1:
"⟦ x ∈ lset xs; ¬ P x ⟧ ⟹ ltakeWhile P (lappend xs ys) = ltakeWhile P xs"
by(induct rule: lset_induct) simp_all

lemma ltakeWhile_lappend2:
"lset xs ⊆ {x. P x}
⟹ ltakeWhile P (lappend xs ys) = lappend xs (ltakeWhile P ys)"
by(coinduction arbitrary: xs ys rule: llist.coinduct_strong)(auto 4 4 simp add: not_lnull_conv lappend_lnull1)

lemma ltakeWhile_cong [cong, fundef_cong]:
assumes xs: "xs = ys"
and PQ: "⋀x. x ∈ lset ys ⟹ P x = Q x"
shows "ltakeWhile P xs = ltakeWhile Q ys"
using PQ unfolding xs
by(coinduction arbitrary: ys)(auto simp add: ltl_ltakeWhile not_lnull_conv)

lemma lnth_llength_ltakeWhile:
assumes len: "llength (ltakeWhile P xs) < llength xs"
shows "¬ P (lnth xs (the_enat (llength (ltakeWhile P xs))))"
proof
assume P: "P (lnth xs (the_enat (llength (ltakeWhile P xs))))"
from len obtain len where "llength (ltakeWhile P xs) = enat len"
by(cases "llength (ltakeWhile P xs)") auto
with P len show False apply simp
proof(induct len arbitrary: xs)
case 0 thus ?case by(simp add: zero_enat_def[symmetric] lnth_0_conv_lhd)
next
case (Suc len) thus ?case by(cases xs)(auto split: if_split_asm simp add: eSuc_enat[symmetric])
qed
qed

lemma assumes "∃x∈lset xs. ¬ P x"
shows lhd_ldropWhile: "¬ P (lhd (ldropWhile P xs))" (is ?thesis1)
and lhd_ldropWhile_in_lset: "lhd (ldropWhile P xs) ∈ lset xs" (is ?thesis2)
proof -
from assms obtain x where "x ∈ lset xs" "¬ P x" by blast
thus ?thesis1 ?thesis2 by induct simp_all
qed

lemma ldropWhile_eq_ldrop:
"ldropWhile P xs = ldrop (llength (ltakeWhile P xs)) xs"
(is "?lhs = ?rhs")
proof(rule lprefix_antisym)
show "?lhs ⊑ ?rhs"
by(induct arbitrary: xs rule: ldropWhile.fixp_induct)(auto split: llist.split)
show "?rhs ⊑ ?lhs"
proof(induct arbitrary: xs rule: ldrop.fixp_induct)
case (3 ldrop xs)
thus ?case by(cases xs) auto
qed simp_all
qed

lemma ldropWhile_cong [cong]:
"⟦ xs = ys; ⋀x. x ∈ lset ys ⟹ P x = Q x ⟧ ⟹ ldropWhile P xs = ldropWhile Q ys"

lemma ltakeWhile_repeat:
"ltakeWhile P (repeat x) = (if P x then repeat x else LNil)"
by(coinduction arbitrary: x)(auto simp add: ltl_ltakeWhile)

lemma ldropWhile_repeat: "ldropWhile P (repeat x) = (if P x then LNil else repeat x)"

lemma lfinite_ldropWhile: "lfinite (ldropWhile P xs) ⟷ (∃x ∈ lset xs. ¬ P x) ⟶ lfinite xs"
by(auto simp add: ldropWhile_eq_ldrop llength_eq_infty_conv_lfinite lfinite_ltakeWhile)

lemma llength_ldropWhile:
"llength (ldropWhile P xs) =
(if ∃x∈lset xs. ¬ P x then llength xs - llength (ltakeWhile P xs) else 0)"
by(auto simp add: ldropWhile_eq_ldrop llength_ldrop llength_ltakeWhile_all ltakeWhile_all_conv llength_ltakeWhile_eq_infinity zero_enat_def dest!: lfinite_llength_enat)

lemma lhd_ldropWhile_conv_lnth:
"∃x∈lset xs. ¬ P x ⟹ lhd (ldropWhile P xs) = lnth xs (the_enat (llength (ltakeWhile P xs)))"

subsection ‹@{term "llist_all2"}›

lemmas llist_all2_LNil_LNil = llist.rel_inject(1)
lemmas llist_all2_LNil_LCons = llist.rel_distinct(1)
lemmas llist_all2_LCons_LNil = llist.rel_distinct(2)
lemmas llist_all2_LCons_LCons = llist.rel_inject(2)

lemma llist_all2_LNil1 [simp]: "llist_all2 P LNil xs ⟷ xs = LNil"
by(cases xs) simp_all

lemma llist_all2_LNil2 [simp]: "llist_all2 P xs LNil ⟷ xs = LNil"
by(cases xs) simp_all

lemma llist_all2_LCons1:
"llist_all2 P (LCons x xs) ys ⟷ (∃y ys'. ys = LCons y ys' ∧ P x y ∧ llist_all2 P xs ys')"
by(cases ys) simp_all

lemma llist_all2_LCons2:
"llist_all2 P xs (LCons y ys) ⟷ (∃x xs'. xs = LCons x xs' ∧ P x y ∧ llist_all2 P xs' ys)"
by(cases xs) simp_all

lemma llist_all2_llist_of [simp]:
"llist_all2 P (llist_of xs) (llist_of ys) = list_all2 P xs ys"
by(induct xs ys rule: list_induct2')(simp_all)

lemma llist_all2_conv_lzip:
"llist_all2 P xs ys ⟷ llength xs = llength ys ∧ (∀(x, y) ∈ lset (lzip xs ys). P x y)"
by(auto 4 4 elim!: GrpE simp add:
llist_all2_def lmap_fst_lzip_conv_ltake lmap_snd_lzip_conv_ltake ltake_all
intro!: GrpI relcomppI[of _ xs _ _ ys])

lemma llist_all2_llengthD:
"llist_all2 P xs ys ⟹ llength xs = llength ys"

lemma llist_all2_lnullD: "llist_all2 P xs ys ⟹ lnull xs ⟷ lnull ys"
unfolding lnull_def by auto

lemma llist_all2_all_lnthI:
"⟦ llength xs = llength ys;
⋀n. enat n < llength xs ⟹ P (lnth xs n) (lnth ys n) ⟧
⟹ llist_all2 P xs ys"

lemma llist_all2_lnthD:
"⟦ llist_all2 P xs ys; enat n < llength xs ⟧ ⟹ P (lnth xs n) (lnth ys n)"

lemma llist_all2_lnthD2:
"⟦ llist_all2 P xs ys; enat n < llength ys ⟧ ⟹ P (lnth xs n) (lnth ys n)"

lemma llist_all2_conv_all_lnth:
"llist_all2 P xs ys ⟷
llength xs = llength ys ∧
(∀n. enat n < llength ys ⟶ P (lnth xs n) (lnth ys n))"
by(auto dest: llist_all2_llengthD llist_all2_lnthD2 intro: llist_all2_all_lnthI)

lemma llist_all2_True [simp]: "llist_all2 (λ_ _. True) xs ys ⟷ llength xs = llength ys"

lemma llist_all2_reflI:
"(⋀x. x ∈ lset xs ⟹ P x x) ⟹ llist_all2 P xs xs"

lemma llist_all2_lmap1:
"llist_all2 P (lmap f xs) ys ⟷ llist_all2 (λx. P (f x)) xs ys"

lemma llist_all2_lmap2:
"llist_all2 P xs (lmap g ys) ⟷ llist_all2 (λx y. P x (g y)) xs ys"

lemma llist_all2_lfiniteD:
"llist_all2 P xs ys ⟹ lfinite xs ⟷ lfinite ys"

lemma llist_all2_coinduct[consumes 1, case_names LNil LCons, case_conclusion LCons lhd ltl, coinduct pred]:
assumes major: "X xs ys"
and step:
"⋀xs ys. X xs ys ⟹ lnull xs ⟷ lnull ys"
"⋀xs ys. ⟦ X xs ys; ¬ lnull xs; ¬ lnull ys ⟧ ⟹ P (lhd xs) (lhd ys) ∧ (X (ltl xs) (ltl ys) ∨ llist_all2 P (ltl xs) (ltl ys))"
shows "llist_all2 P xs ys"
proof(rule llist_all2_all_lnthI)
from major show "llength xs = llength ys"
by(coinduction arbitrary: xs ys rule: enat_coinduct)(auto 4 3 dest: step llist_all2_llengthD simp add: epred_llength)

fix n
assume "enat n < llength xs"
thus "P (lnth xs n) (lnth ys n)"
using major ‹llength xs = llength ys›
proof(induct n arbitrary: xs ys)
case 0 thus ?case
by(cases "lnull xs")(auto dest: step simp add: zero_enat_def[symmetric] lnth_0_conv_lhd)
next
case (Suc n)
from step[OF ‹X xs ys›] ‹enat (Suc n) < llength xs› Suc show ?case
by(auto 4 3 simp add: not_lnull_conv Suc_ile_eq intro: Suc.hyps llist_all2_lnthD dest: llist_all2_llengthD)
qed
qed

lemma llist_all2_cases[consumes 1, case_names LNil LCons, cases pred]:
assumes "llist_all2 P xs ys"
obtains (LNil) "xs = LNil" "ys = LNil"
| (LCons) x xs' y ys'
where "xs = LCons x xs'" and "ys = LCons y ys'"
and "P x y" and "llist_all2 P xs' ys'"
using assms

lemma llist_all2_mono:
"⟦ llist_all2 P xs ys; ⋀x y. P x y ⟹ P' x y ⟧ ⟹ llist_all2 P' xs ys"

lemma llist_all2_left: "llist_all2 (λx _. P x) xs ys ⟷ llength xs = llength ys ∧ (∀x∈lset xs. P x)"

lemma llist_all2_right: "llist_all2 (λ_. P) xs ys ⟷ llength xs = llength ys ∧ (∀x∈lset ys. P x)"

lemma llist_all2_lsetD1: "⟦ llist_all2 P xs ys; x ∈ lset xs ⟧ ⟹ ∃y∈lset ys. P x y"
by(auto 4 4 simp add: llist_all2_conv_lzip lset_lzip lset_conv_lnth split_beta lnth_lzip simp del: split_paired_All)

lemma llist_all2_lsetD2: "⟦ llist_all2 P xs ys; y ∈ lset ys ⟧ ⟹ ∃x∈lset xs. P x y"
by(auto 4 4 simp add: llist_all2_conv_lzip lset_lzip lset_conv_lnth split_beta lnth_lzip simp del: split_paired_All)

lemma llist_all2_conj:
"llist_all2 (λx y. P x y ∧ Q x y) xs ys ⟷ llist_all2 P xs ys ∧ llist_all2 Q xs ys"

lemma llist_all2_lhdD:
"⟦ llist_all2 P xs ys; ¬ lnull xs ⟧ ⟹ P (lhd xs) (lhd ys)"

lemma llist_all2_lhdD2:
"⟦ llist_all2 P xs ys; ¬ lnull ys ⟧ ⟹ P (lhd xs) (lhd ys)"

lemma llist_all2_ltlI:
"llist_all2 P xs ys ⟹ llist_all2 P (ltl xs) (ltl ys)"

lemma llist_all2_lappendI:
assumes 1: "llist_all2 P xs ys"
and 2: "⟦ lfinite xs; lfinite ys ⟧ ⟹ llist_all2 P xs' ys'"
shows "llist_all2 P (lappend xs xs') (lappend ys ys')"
proof(cases "lfinite xs")
case True
with 1 have "lfinite ys" by(auto dest: llist_all2_lfiniteD)
from 1 2[OF True this] show ?thesis
by(coinduction arbitrary: xs ys)(auto dest: llist_all2_lnullD llist_all2_lhdD intro: llist_all2_ltlI simp add: lappend_eq_LNil_iff)
next
case False
with 1 have "¬ lfinite ys" by(auto dest: llist_all2_lfiniteD)
with False 1 show ?thesis by(simp add: lappend_inf)
qed

lemma llist_all2_lappend1D:
assumes "llist_all2 P (lappend xs xs') ys"
shows "llist_all2 P xs (ltake (llength xs) ys)"
and "lfinite xs ⟹ llist_all2 P xs' (ldrop (llength xs) ys)"
proof -
from assms have len: "llength xs + llength xs' = llength ys" by(auto dest: llist_all2_llengthD)
hence len_xs: "llength xs ≤ llength ys" and len_xs': "llength xs' ≤ llength ys"
by (metis enat_le_plus_same llength_lappend)+

show "llist_all2 P xs (ltake (llength xs) ys)"
proof(rule llist_all2_all_lnthI)
show "llength xs = llength (ltake (llength xs) ys)"
next
fix n
assume n: "enat n < llength xs"
also have "… ≤ llength (lappend xs xs')" by(simp add: enat_le_plus_same)
finally have "P (lnth (lappend xs xs') n) (lnth ys n)"
using assms by -(rule llist_all2_lnthD)
also from n have "lnth ys n = lnth (ltake (llength xs) ys) n" by(rule lnth_ltake[symmetric])
also from n have "lnth (lappend xs xs') n = lnth xs n" by(simp add: lnth_lappend1)
finally show "P (lnth xs n) (lnth (ltake (llength xs) ys) n)" .
qed

assume "lfinite xs"
thus "llist_all2 P xs' (ldrop (llength xs) ys)" using assms
by(induct arbitrary: ys)(auto simp add: llist_all2_LCons1)
qed

lemma lmap_eq_lmap_conv_llist_all2:
"lmap f xs = lmap g ys ⟷ llist_all2 (λx y. f x = g y) xs ys" (is "?lhs ⟷ ?rhs")
proof
assume ?lhs
thus ?rhs
by(coinduction arbitrary: xs ys)(auto simp add: neq_LNil_conv lnull_def LNil_eq_lmap lmap_eq_LNil)
next
assume ?rhs
thus ?lhs
by(coinduction arbitrary: xs ys)(auto dest: llist_all2_lnullD llist_all2_lhdD llist_all2_ltlI)
qed

lemma llist_all2_expand:
"⟦ lnull xs ⟷ lnull ys;
⟦ ¬ lnull xs; ¬ lnull ys ⟧ ⟹ P (lhd xs) (lhd ys) ∧ llist_all2 P (ltl xs) (ltl ys) ⟧
⟹ llist_all2 P xs ys"

lemma llist_all2_llength_ltakeWhileD:
assumes major: "llist_all2 P xs ys"
and Q: "⋀x y. P x y ⟹ Q1 x ⟷ Q2 y"
shows "llength (ltakeWhile Q1 xs) = llength (ltakeWhile Q2 ys)"
using major
by(coinduction arbitrary: xs ys rule: enat_coinduct)(auto 4 3 simp add: not_lnull_conv llist_all2_LCons1 llist_all2_LCons2 dest!: Q)

lemma llist_all2_lzipI:
"⟦ llist_all2 P xs ys; llist_all2 P' xs' ys' ⟧
⟹ llist_all2 (rel_prod P P') (lzip xs xs') (lzip ys ys')"
by(coinduction arbitrary: xs xs' ys ys')(auto 6 6 dest: llist_all2_lhdD llist_all2_lnullD intro: llist_all2_ltlI)

lemma llist_all2_ltakeI:
"llist_all2 P xs ys ⟹ llist_all2 P (ltake n xs) (ltake n ys)"

lemma llist_all2_ldropnI:
"llist_all2 P xs ys ⟹ llist_all2 P (ldropn n xs) (ldropn n ys)"
by(cases "llength ys")(auto simp add: llist_all2_conv_all_lnth)

lemma llist_all2_ldropI:
"llist_all2 P xs ys ⟹ llist_all2 P (ldrop n xs) (ldrop n ys)"
by(cases "llength ys")(auto simp add: llist_all2_conv_all_lnth llength_ldrop)

lemma llist_all2_lSupI:
assumes "Complete_Partial_Order.chain (rel_prod (⊑) (⊑)) Y" "∀(xs, ys)∈Y. llist_all2 P xs ys"
shows "llist_all2 P (lSup (fst ` Y)) (lSup (snd ` Y))"
using assms
proof(coinduction arbitrary: Y)
case LNil
thus ?case
by(auto dest: llist_all2_lnullD simp add: split_beta)
next
case (LCons Y)
note chain = ‹Complete_Partial_Order.chain _ Y›
from LCons have Y: "⋀xs ys. (xs, ys) ∈ Y ⟹ llist_all2 P xs ys" by blast
from LCons obtain xs ys where xsysY: "(xs, ys) ∈ Y"
and [simp]: "¬ lnull xs" "¬ lnull ys"
by(auto 4 3 dest: llist_all2_lnullD simp add: split_beta)
from xsysY have "lhd xs ∈ lhd ` (fst ` Y ∩ {xs. ¬ lnull xs})"
by(auto intro: rev_image_eqI)
hence "(THE x. x ∈ lhd ` (fst ` Y ∩ {xs. ¬ lnull xs})) = lhd xs"
by(rule the_equality)(auto dest!: lprefix_lhdD chainD[OF chain xsysY])
moreover from xsysY have "lhd ys ∈ lhd ` (snd ` Y ∩ {xs. ¬ lnull xs})"
by(auto intro: rev_image_eqI)
hence "(THE x. x ∈ lhd ` (snd ` Y ∩ {xs. ¬ lnull xs})) = lhd ys"
by(rule the_equality)(auto dest!: lprefix_lhdD chainD[OF chain xsysY])
moreover from xsysY have "llist_all2 P xs ys" by(rule Y)
hence "P (lhd xs) (lhd ys)" by(rule llist_all2_lhdD) simp
ultimately have ?lhd using LCons by simp
moreover {
let ?Y = "map_prod ltl ltl ` (Y ∩ {(xs, ys). ¬ lnull xs ∧ ¬ lnull ys})"
have "Complete_Partial_Order.chain (rel_prod (⊑) (⊑)) ?Y"
by(rule chainI)(auto 4 3 dest: Y chainD[OF chain] intro: lprefix_ltlI)
moreover
have "ltl ` (fst ` Y ∩ {xs. ¬ lnull xs}) = fst ` ?Y"
and "ltl ` (snd ` Y ∩ {xs. ¬ lnull xs}) = snd ` ?Y"
by(fastforce simp add: image_image dest: Y llist_all2_lnullD intro: rev_image_eqI)+
ultimately have ?ltl by(auto 4 3 intro: llist_all2_ltlI dest: Y) }
ultimately show ?case ..
qed

assumes f: "mcont lub ord lSup (⊑) (λx. f x)"
and g: "mcont lub ord lSup (⊑) (λx. g x)"
shows "ccpo.admissible lub ord (λx. llist_all2 P (f x) (g x))"
fix Y
assume chain: "Complete_Partial_Order.chain ord Y"
and Y: "∀x∈Y. llist_all2 P (f x) (g x)"
and "Y ≠ {}"
from chain have "Complete_Partial_Order.chain (rel_prod (⊑) (⊑)) ((λx. (f x, g x)) ` Y)"
by(rule chain_imageI)(auto intro: mcont_monoD[OF f] mcont_monoD[OF g])
from llist_all2_lSupI[OF this, of P] chain Y
show "llist_all2 P (f (lub Y)) (g (lub Y))" using ‹Y ≠ {}›
by(simp add: mcont_contD[OF f chain] mcont_contD[OF g chain] image_image)
qed

lemmas [cont_intro] =
ccpo.mcont2mcont[OF llist_ccpo _ mcont_fst]
ccpo.mcont2mcont[OF llist_ccpo _ mcont_snd]

lemmas ldropWhile_fixp_parallel_induct =
parallel_fixp_induct_1_1[OF llist_partial_function_definitions llist_partial_function_definitions
ldropWhile.mono ldropWhile.mono ldropWhile_def ldropWhile_def, case_names adm LNil step]

lemma llist_all2_ldropWhileI:
assumes *: "llist_all2 P xs ys"
and Q: "⋀x y. P x y ⟹ Q1 x ⟷ Q2 y"
shows "llist_all2 P (ldropWhile Q1 xs) (ldropWhile Q2 ys)"
― ‹cannot prove this with parallel induction over @{term xs} and @{term ys}
because @{term "λx. ¬ llist_all2 P (f x) (g x)"} is not admissible.›
using * by(induction arbitrary: xs ys rule: ldropWhile_fixp_parallel_induct)(auto split: llist.split dest: Q)

lemma llist_all2_same [simp]: "llist_all2 P xs xs ⟷ (∀x∈lset xs. P x x)"
by(auto simp add: llist_all2_conv_all_lnth in_lset_conv_lnth Ball_def)

lemma llist_all2_trans:
"⟦ llist_all2 P xs ys; llist_all2 P ys zs; transp P ⟧
⟹ llist_all2 P xs zs"
apply(rule llist_all2_all_lnthI)
apply(frule llist_all2_llengthD)
apply(drule (1) llist_all2_lnthD)
apply(drule llist_all2_lnthD)
apply simp
apply(erule (2) transpD)
done

subsection ‹The last element @{term "llast"}›

lemma llast_LNil: "llast LNil = undefined"

lemma llast_LCons: "llast (LCons x xs) = (if lnull xs then x else llast xs)"
by(cases "llength xs")(auto simp add: llast_def eSuc_def zero_enat_def not_lnull_conv split: enat.splits)

lemma llast_linfinite: "¬ lfinite xs ⟹ llast xs = undefined"

lemma [simp, code]:
shows llast_singleton: "llast (LCons x LNil) = x"
and llast_LCons2: "llast (LCons x (LCons y xs)) = llast (LCons y xs)"

lemma llast_lappend:
"llast (lappend xs ys) = (if lnull ys then llast xs else if lfinite xs then llast ys else undefined)"
proof(cases "lfinite xs")
case True
hence "¬ lnull ys ⟹ llast (lappend xs ys) = llast ys"
with True show ?thesis by(simp add: lappend_lnull2)
next
case False thus ?thesis by(simp add: llast_linfinite)
qed

lemma llast_lappend_LCons [simp]:
"lfinite xs ⟹ llast (lappend xs (LCons y ys)) = llast (LCons y ys)"

lemma llast_ldropn: "enat n < llength xs ⟹ llast (ldropn n xs) = llast xs"
proof(induct n arbitrary: xs)
case 0 thus ?case by simp
next
case (Suc n) thus ?case by(cases xs)(auto simp add: Suc_ile_eq llast_LCons)
qed

lemma llast_ldrop:
assumes "n < llength xs"
shows "llast (ldrop n xs) = llast xs"
proof -
from assms obtain n' where n: "n = enat n'" by(cases n) auto
show ?thesis using assms unfolding n
proof(induct n' arbitrary: xs)
case 0 thus ?case by(simp add: zero_enat_def[symmetric])
next
case Suc thus ?case by(cases xs)(auto simp add: eSuc_enat[symmetric] llast_LCons)
qed
qed

lemma llast_llist_of [simp]: "llast (llist_of xs) = last xs"
by(induct xs)(auto simp add: last_def zero_enat_def llast_LCons llast_LNil)

lemma llast_conv_lnth: "llength xs = eSuc (enat n) ⟹ llast xs = lnth xs n"
by(clarsimp simp add: llast_def zero_enat_def[symmetric] eSuc_enat split: nat.split)

lemma llast_lmap:
assumes "lfinite xs" "¬ lnull xs"
shows "llast (lmap f xs) = f (llast xs)"
using assms
proof induct
case (lfinite_LConsI xs)
thus ?case by(cases xs) simp_all
qed simp

subsection ‹Distinct lazy lists @{term "ldistinct"}›

inductive_simps ldistinct_LCons [code, simp]:
"ldistinct (LCons x xs)"

lemma ldistinct_LNil_code [code]:
"ldistinct LNil = True"
by simp

lemma ldistinct_llist_of [simp]:
"ldistinct (llist_of xs) ⟷ distinct xs"
by(induct xs) auto

lemma ldistinct_coinduct [consumes 1, case_names ldistinct, case_conclusion ldistinct lhd ltl, coinduct pred: ldistinct]:
assumes "X xs"
and step: "⋀xs. ⟦ X xs; ¬ lnull xs ⟧
⟹ lhd xs ∉ lset (ltl xs) ∧ (X (ltl xs) ∨ ldistinct (ltl xs))"
shows "ldistinct xs"
using ‹X xs›
proof(coinduct)
case (ldistinct xs)
thus ?case by(cases xs)(auto dest: step)
qed

lemma ldistinct_lhdD:
"⟦ ldistinct xs; ¬ lnull xs ⟧ ⟹ lhd xs ∉ lset (ltl xs)"

lemma ldistinct_ltlI:
"ldistinct xs ⟹ ldistinct (ltl xs)"
by(cases xs) simp_all

lemma ldistinct_lSup:
"⟦ Complete_Partial_Order.chain (⊑) Y; ∀xs∈Y. ldistinct xs ⟧
⟹ ldistinct (lSup Y)"
proof(coinduction arbitrary: Y)
case (ldistinct Y)
hence chain: "Complete_Partial_Order.chain (⊑) Y"
and distinct: "⋀xs. xs ∈ Y ⟹ ldistinct xs" by blast+
have ?lhd using chain by(auto 4 4 simp add: lset_lSup chain_lprefix_ltl dest: distinct lhd_lSup_eq ldistinct_lhdD)
moreover have ?ltl by(auto 4 3 simp add: chain_lprefix_ltl chain intro: ldistinct_ltlI distinct)
ultimately show ?case ..
qed

assumes mcont: "mcont lub ord lSup (⊑) (λx. f x)"
shows "ccpo.admissible lub ord (λx. ldistinct (f x))"
fix Y
assume chain: "Complete_Partial_Order.chain ord Y"
and distinct: "∀x∈Y. ldistinct (f x)"
and "Y ≠ {}"
thus "ldistinct (f (lub Y))"
by(simp add: mcont_contD[OF mcont] ldistinct_lSup chain_imageI mcont_monoD[OF mcont])
qed

lemma ldistinct_lappend:
"ldistinct (lappend xs ys) ⟷ ldistinct xs ∧ (lfinite xs ⟶ ldistinct ys ∧ lset xs ∩ lset ys = {})"
(is "?lhs = ?rhs")
proof(intro iffI conjI strip)
assume "?lhs"
thus "ldistinct xs"

assume "lfinite xs"
thus "ldistinct ys" "lset xs ∩ lset ys = {}"
using ‹?lhs› by induct simp_all
next
assume "?rhs"
thus ?lhs
by(coinduction arbitrary: xs)(auto simp add: not_lnull_conv in_lset_lappend_iff)
qed

lemma ldistinct_lprefix:
"⟦ ldistinct xs; ys ⊑ xs ⟧ ⟹ ldistinct ys"

"ccpo.admissible lSup (⊑) (λx. ¬ ldistinct x)"
by(rule ccpo.admissibleI)(auto dest: ldistinct_lprefix intro: chain_lprefix_lSup)

lemma ldistinct_ltake: "ldistinct xs ⟹ ldistinct (ltake n xs)"
by (metis ldistinct_lprefix ltake_is_lprefix)

lemma ldistinct_ldropn:
"ldistinct xs ⟹ ldistinct (ldropn n xs)"
by(induct n arbitrary: xs)(simp, case_tac xs, simp_all)

lemma ldistinct_ldrop: "ldistinct xs ⟹ ldistinct (ldrop n xs)"
proof(induct xs arbitrary: n)
case (LCons x xs) thus ?case
by(cases n rule: co.enat.exhaust) simp_all
qed simp_all

lemma ldistinct_conv_lnth:
"ldistinct xs ⟷ (∀i j. enat i < llength xs ⟶ enat j < llength xs ⟶ i ≠ j ⟶ lnth xs i ≠ lnth xs j)"
(is "?lhs ⟷ ?rhs")
proof(intro iffI strip)
assume "?rhs"
thus "?lhs"
proof(coinduct xs)
case (ldistinct xs)
from ‹¬ lnull xs›
obtain x xs' where LCons: "xs = LCons x xs'"
have "x ∉ lset xs'"
proof
assume "x ∈ lset xs'"
then obtain j where "enat j < llength xs'" "lnth xs' j = x"
unfolding lset_conv_lnth by auto
hence "enat 0 < llength xs" "enat (Suc j) < llength xs" "lnth xs (Suc j) = x" "lnth xs 0 = x"
thus False by(auto dest: ldistinct(1)[rule_format])
qed
moreover {
fix i j
assume "enat i < llength xs'" "enat j < llength xs'" "i ≠ j"
hence "enat (Suc i) < llength xs" "enat (Suc j) < llength xs"
with ‹i ≠ j› have "lnth xs (Suc i) ≠ lnth xs (Suc j)"
by(auto dest: ldistinct(1)[rule_format])
hence "lnth xs' i ≠ lnth xs' j" unfolding LCons by simp }
ultimately show ?case using LCons by simp
qed
next
assume "?lhs"
fix i j
assume "enat i < llength xs" "enat j < llength xs" "i ≠ j"
thus "lnth xs i ≠ lnth xs j"
proof(induct i j rule: wlog_linorder_le)
case symmetry thus ?case by simp
next
case (le i j)
from ‹?lhs› have "ldistinct (ldropn i xs)" by(rule ldistinct_ldropn)
also note ldropn_Suc_conv_ldropn[symmetric]
also from le have "i < j" by simp
hence "lnth xs j ∈ lset (ldropn (Suc i) xs)" using le unfolding in_lset_conv_lnth
by(cases "llength xs")(auto intro!: exI[where x="j - Suc i"])
ultimately show ?case using ‹enat i < llength xs› by auto
qed
qed

lemma ldistinct_lmap [simp]:
"ldistinct (lmap f xs) ⟷ ldistinct xs ∧ inj_on f (lset xs)"
(is "?lhs ⟷ ?rhs")
proof(intro iffI conjI)
assume dist: ?lhs
thus "ldistinct xs"

show "inj_on f (lset xs)"
proof(rule inj_onI)
fix x y
assume "x ∈ lset xs" and "y ∈ lset xs" and "f x = f y"
then obtain i j
where "enat i < llength xs" "x = lnth xs i" "enat j < llength xs" "y = lnth xs j"
unfolding lset_conv_lnth by blast
with dist ‹f x = f y› show "x = y"
unfolding ldistinct_conv_lnth by auto
qed
next
assume ?rhs
thus ?lhs
by(coinduction arbitrary: xs)(auto simp add: not_lnull_conv)
qed

lemma ldistinct_lzipI1: "ldistinct xs ⟹ ldistinct (lzip xs ys)"
by(coinduction arbitrary: xs ys)(auto simp add: not_lnull_conv dest: lset_lzipD1)

lemma ldistinct_lzipI2: "ldistinct ys ⟹ ldistinct (lzip xs ys)"
by(coinduction arbitrary: xs ys)(auto 4 3 simp add: not_lnull_conv dest: lset_lzipD2)

subsection ‹Sortedness @{term lsorted}›

context ord begin

coinductive lsorted :: "'a llist ⇒ bool"
where
LNil [simp]: "lsorted LNil"
| Singleton [simp]: "lsorted (LCons x LNil)"
| LCons_LCons: "⟦ x ≤ y; lsorted (LCons y xs) ⟧ ⟹ lsorted (LCons x (LCons y xs))"

inductive_simps lsorted_LCons_LCons [simp]:
"lsorted (LCons x (LCons y xs))"

inductive_simps lsorted_code [code]:
"lsorted LNil"
"lsorted (LCons x LNil)"
"lsorted (LCons x (LCons y xs))"

lemma lsorted_coinduct' [consumes 1, case_names lsorted, case_conclusion lsorted lhd ltl, coinduct pred: lsorted]:
assumes major: "X xs"
and step: "⋀xs. ⟦ X xs; ¬ lnull xs; ¬ lnull (ltl xs) ⟧ ⟹ lhd xs ≤ lhd (ltl xs) ∧ (X (ltl xs) ∨ lsorted (ltl xs))"
shows "lsorted xs"
using major by coinduct(subst disj_commute, auto 4 4 simp add: neq_LNil_conv dest: step)

lemma lsorted_ltlI: "lsorted xs ⟹ lsorted (ltl xs)"
by(erule lsorted.cases) simp_all

lemma lsorted_lhdD:
"⟦ lsorted xs; ¬ lnull xs; ¬ lnull (ltl xs) ⟧ ⟹ lhd xs ≤ lhd (ltl xs)"
by(auto elim: lsorted.cases)

lemma lsorted_LCons':
"lsorted (LCons x xs) ⟷ (¬ lnull xs ⟶ x ≤ lhd xs ∧ lsorted xs)"
by(cases xs) auto

lemma lsorted_lSup:
"⟦ Complete_Partial_Order.chain (⊑) Y; ∀xs ∈ Y. lsorted xs ⟧
⟹ lsorted (lSup Y)"
proof(coinduction arbitrary: Y)
case (lsorted Y)
hence sorted: "⋀xs. xs ∈ Y ⟹ lsorted xs" by blast
note chain = ‹Complete_Partial_Order.chain (⊑) Y›
from ‹¬ lnull (lSup Y)› ‹¬ lnull (ltl (lSup Y))›
obtain xs where "xs ∈ Y" "¬ lnull xs" "¬ lnull (ltl xs)" by auto
hence "lhd (lSup Y) = lhd xs" "lhd (ltl (lSup Y)) = lhd (ltl xs)" "lhd xs ≤ lhd (ltl xs)"
using chain sorted by(auto intro: lhd_lSup_eq chain_lprefix_ltl lsorted_lhdD)
hence ?lhd by simp
moreover have ?ltl using chain sorted by(auto intro: chain_lprefix_ltl lsorted_ltlI)
ultimately show ?case ..
qed

lemma lsorted_lprefixD:
"⟦ xs ⊑ ys; lsorted ys ⟧ ⟹ lsorted xs"
proof(coinduction arbitrary: xs ys)
case (lsorted xs ys)
hence "lhd xs = lhd ys" "lhd (ltl xs) = lhd (ltl ys)"
by(auto dest: lprefix_lhdD lprefix_ltlI)
moreover have "lhd ys ≤ lhd (ltl ys)" using lsorted
by(auto intro: lsorted_lhdD dest: lprefix_lnullD lprefix_ltlI)
ultimately have ?lhd by simp
moreover have ?ltl using lsorted by(blast intro: lsorted_ltlI lprefix_ltlI)
ultimately show ?case ..
qed

assumes mcont: "mcont lub ord lSup (⊑) (λx. f x)"
and ccpo: "class.ccpo lub ord (mk_less ord)"
shows "ccpo.admissible lub ord (λx. lsorted (f x))"
fix Y
assume chain: "Complete_Partial_Order.chain ord Y"
and sorted: "∀x∈Y. lsorted (f x)"
and "Y ≠ {}"
thus "lsorted (f (lub Y))"
by(simp add: mcont_contD[OF mcont] lsorted_lSup chain_imageI mcont_monoD[OF mcont])
qed

"ccpo.admissible lSup (⊑) (λxs. ¬ lsorted xs)"
by(rule ccpo.admissibleI)(auto dest: lsorted_lprefixD[rotated] intro: chain_lprefix_lSup)

lemma lsorted_ltake [simp]: "lsorted xs ⟹ lsorted (ltake n xs)"
by(rule lsorted_lprefixD)(rule ltake_is_lprefix)

lemma lsorted_ldropn [simp]: "lsorted xs ⟹ lsorted (ldropn n xs)"
by(induct n arbitrary: xs)(fastforce simp add: ldropn_Suc lsorted_LCons' ldropn_lnull split: llist.split)+

lemma lsorted_ldrop [simp]: "lsorted xs ⟹ lsorted (ldrop n xs)"
by(induct xs arbitrary: n)(auto simp add: ldrop_LCons lsorted_LCons' ldrop_lnull split: co.enat.split)

end

declare
ord.lsorted_code [code]

context preorder begin

lemma lsorted_LCons:
"lsorted (LCons x xs) ⟷ lsorted xs ∧ (∀y∈lset xs. x ≤ y)" (is "?lhs ⟷ ?rhs")
proof
assume ?lhs
{ fix y
assume "y ∈ lset xs"
hence "x ≤ y" using ‹?lhs›
by(induct arbitrary: x)(auto intro: order_trans) }
with ‹?lhs› show ?rhs by cases auto
next
assume ?rhs
thus ?lhs by(cases xs) simp_all
qed

lemma lsorted_coinduct [consumes 1, case_names lsorted, case_conclusion lsorted lhd ltl, coinduct pred: lsorted]:
assumes major: "X xs"
and step: "⋀xs. ⟦ X xs; ¬ lnull xs ⟧ ⟹ (∀x ∈ lset (ltl xs). lhd xs ≤ x) ∧ (X (ltl xs) ∨ lsorted (ltl xs))"
shows "lsorted xs"
using major by(coinduct rule: lsorted_coinduct')(auto dest: step)

lemma lsortedD: "⟦ lsorted xs; ¬ lnull xs; y ∈ lset (ltl xs) ⟧ ⟹ lhd xs ≤ y"

end

lemma lsorted_lmap':
assumes "ord.lsorted orda xs" "monotone orda ordb f"
shows "ord.lsorted ordb (lmap f xs)"
using ‹ord.lsorted orda xs›
by(coinduction arbitrary: xs rule: ord.lsorted_coinduct')(auto intro: monotoneD[OF ‹monotone orda ordb f›] ord.lsorted_lhdD ord.lsorted_ltlI)

lemma lsorted_lmap:
assumes "lsorted xs" "monotone (≤) (≤) f"
shows "lsorted (lmap f xs)"
using ‹lsorted xs›
by(coinduction arbitrary: xs rule: lsorted_coinduct')(auto intro: monotoneD[OF ‹monotone (≤) (≤) f›] lsorted_lhdD lsorted_ltlI)

context linorder begin

lemma lsorted_ldistinct_lset_unique:
"⟦ lsorted xs; ldistinct xs; lsorted ys; ldistinct ys; lset xs = lset ys ⟧
⟹ xs = ys"
proof(coinduction arbitrary: xs ys)
case (Eq_llist xs ys)
hence ?lnull by(cases ys)(auto simp add: lset_lnull)
moreover from Eq_llist have ?LCons
by(auto 4 3 intro: lsorted_ltlI ldistinct_ltlI simp add: not_lnull_conv insert_eq_iff lsorted_LCons split: if_split_asm)
ultimately show ?case ..
qed

end

lemma lsorted_llist_of[simp]: "lsorted (llist_of xs) ⟷ sorted xs"
by(induct xs)(auto simp: lsorted_LCons)

subsection ‹Lexicographic order on lazy lists: @{term "llexord"}›

lemma llexord_coinduct [consumes 1, case_names llexord, coinduct pred: llexord]:
assumes X: "X xs ys"
and step: "⋀xs ys. ⟦ X xs ys; ¬ lnull xs ⟧
⟹ ¬ lnull ys ∧
(¬ lnull ys ⟶ r (lhd xs) (lhd ys) ∨
lhd xs = lhd ys ∧ (X (ltl xs) (ltl ys) ∨ llexord r (ltl xs) (ltl ys)))"
shows "llexord r xs ys"
using X
proof(coinduct)
case (llexord xs ys)
thus ?case
by(cases xs ys rule: llist.exhaust[case_product llist.exhaust])(auto dest: step)
qed

lemma llexord_refl [simp, intro!]:
"llexord r xs xs"
proof -
define ys where "ys = xs"
hence "xs = ys" by simp
thus "llexord r xs ys"
by(coinduct xs ys) auto
qed

lemma llexord_LCons_LCons [simp]:
"llexord r (LCons x xs) (LCons y ys) ⟷ (x = y ∧ llexord r xs ys ∨ r x y)"
by(auto intro: llexord.intros(1,2) elim: llexord.cases)

lemma lnull_llexord [simp]: "lnull xs ⟹ llexord r xs ys"
unfolding lnull_def by simp

lemma llexord_LNil_right [simp]:
"lnull ys ⟹ llexord r xs ys ⟷ lnull xs"
by(auto elim: llexord.cases)

lemma llexord_LCons_left:
"llexord r (LCons x xs) ys ⟷
(∃y ys'. ys = LCons y ys' ∧ (x = y ∧ llexord r xs ys' ∨ r x y))"
by(cases ys)(auto elim: llexord.cases)

lemma lprefix_imp_llexord:
assumes "xs ⊑ ys"
shows "llexord r xs ys"
using assms

lemma llexord_empty:
"llexord (λx y. False) xs ys = xs ⊑ ys"
proof
assume "llexord (λx y. False) xs ys"
thus "xs ⊑ ys"
by(coinduct)(auto elim: llexord.cases)
qed(rule lprefix_imp_llexord)

lemma llexord_append_right:
"llexord r xs (lappend xs ys)"

lemma llexord_lappend_leftI:
assumes "llexord r ys zs"
shows "llexord r (lappend xs ys) (lappend xs zs)"
proof(cases "lfinite xs")
case True thus ?thesis by induct (simp_all add: assms)
next
case False thus ?thesis by(simp add: lappend_inf)
qed

lemma llexord_lappend_leftD:
assumes lex: "llexord r (lappend xs ys) (lappend xs zs)"
and fin: "lfinite xs"
and irrefl: "!!x. x ∈ lset xs ⟹ ¬ r x x"
shows "llexord r ys zs"
using fin lex irrefl by(induct) simp_all

lemma llexord_lappend_left:
"⟦ lfinite xs; !!x. x ∈ lset xs ⟹ ¬ r x x ⟧
⟹ llexord r (lappend xs ys) (lappend xs zs) ⟷ llexord r ys zs"
by(blast intro: llexord_lappend_leftI llexord_lappend_leftD)

lemma antisym_llexord:
assumes r: "antisymp r"
and irrefl: "⋀x. ¬ r x x"
shows "antisymp (llexord r)"
proof(rule antisympI)
fix xs ys
assume "llexord r xs ys"
and "llexord r ys xs"
hence "llexord r xs ys ∧ llexord r ys xs" by auto
thus "xs = ys"
by (coinduct rule: llist.coinduct)
(auto 4 3 simp add: not_lnull_conv irrefl dest: antisympD[OF r, simplified])
qed

lemma llexord_antisym:
"⟦ llexord r xs ys; llexord r ys xs;
!!a b. ⟦ r a b; r b a ⟧ ⟹ False ⟧
⟹ xs = ys"
using antisympD[OF antisym_llexord, of r xs ys]
by(auto intro: antisympI)

lemma llexord_trans:
assumes 1: "llexord r xs ys"
and 2: "llexord r ys zs"
and trans: "!!a b c. ⟦ r a b; r b c ⟧ ⟹ r a c"
shows "llexord r xs zs"
proof -
from 1 2 have "∃ys. llexord r xs ys ∧ llexord r ys zs" by blast
thus ?thesis
by(coinduct)(auto 4 3 simp add: not_lnull_conv llexord_LCons_left dest: trans)
qed

lemma trans_llexord:
"transp r ⟹ transp (llexord r)"
by(auto intro!: transpI elim: llexord_trans dest: transpD)

lemma llexord_linear:
assumes linear: "!!x y. r x y ∨ x = y ∨ r y x"
shows "llexord r xs ys ∨ llexord r ys xs"
proof(rule disjCI)
assume "¬ llexord r ys xs"
thus "llexord r xs ys"
proof(coinduct rule: llexord_coinduct)
case (llexord xs ys)
show ?case
proof(cases xs)
case LNil thus ?thesis using llexord by simp
next
case (LCons x xs')
with ‹¬ llexord r ys xs› obtain y ys'
where ys: "ys = LCons y ys'" "¬ r y x" "y ≠ x ∨ ¬ llexord r ys' xs'"
by(cases ys) auto
with ‹¬ r y x› linear[of x y] ys LCons show ?thesis by auto
qed
qed
qed

lemma llexord_code [code]:
"llexord r LNil ys = True"
"llexord r (LCons x xs) LNil = False"
"llexord r (LCons x xs) (LCons y ys) = (r x y ∨ x = y ∧ llexord r xs ys)"
by auto

lemma llexord_conv:
"llexord r xs ys ⟷
xs = ys ∨
(∃zs xs' y ys'. lfinite zs ∧ xs = lappend zs xs' ∧ ys = lappend zs (LCons y ys') ∧
(xs' = LNil ∨ r (lhd xs') y))"
(is "?lhs ⟷ ?rhs")
proof
assume ?lhs
show ?rhs (is "_ ∨ ?prefix")
proof(rule disjCI)
assume "¬ ?prefix"
with ‹?lhs› show "xs = ys"
proof(coinduction arbitrary: xs ys)
case (Eq_llist xs ys)
hence "llexord r xs ys"
and prefix: "⋀zs xs' y ys'. ⟦ lfinite zs; xs = lappend zs xs';
ys = lappend zs (LCons y ys') ⟧
⟹ xs' ≠ LNil ∧ ¬ r (lhd xs') y"
by auto
from ‹llexord r xs ys› show ?case
proof(cases)
case (llexord_LCons_eq xs' ys' x)
{ fix zs xs'' y ys''
assume "lfinite zs" "xs' = lappend zs xs''"
and "ys' = lappend zs (LCons y ys'')"
hence "lfinite (LCons x zs)" "xs = lappend (LCons x zs) xs''"
and "ys = lappend (LCons x zs) (LCons y ys'')"
using llexord_LCons_eq by simp_all
hence "xs'' ≠ LNil ∧ ¬ r (lhd xs'') y" by(rule prefix) }
with llexord_LCons_eq show ?thesis by auto
next
case (llexord_LCons_less x y xs' ys')
with prefix[of LNil xs y ys'] show ?thesis by simp
next
case llexord_LNil
thus ?thesis using prefix[of LNil xs "lhd ys" "ltl ys"]
by(cases ys) simp_all
qed
qed
qed
next
assume ?rhs
thus ?lhs
proof(coinduct xs ys)
case (llexord xs ys)
show ?case
proof(cases xs)
case LNil thus ?thesis using llexord by simp
next
case (LCons x xs')
with llexord obtain y ys' where "ys = LCons y ys'"
by(cases ys)(auto dest: sym simp add: LNil_eq_lappend_iff)
show ?thesis
proof(cases "x = y")
case True
from llexord(1) show ?thesis
proof
assume "xs = ys"
with True LCons ‹ys = LCons y ys'› show ?thesis by simp
next
assume "∃zs xs' y ys'. lfinite zs ∧ xs = lappend zs xs' ∧
ys = lappend zs (LCons y ys') ∧
(xs' = LNil ∨ r (lhd xs') y)"
then obtain zs xs' y' ys''
where "lfinite zs" "xs = lappend zs xs'"
and "ys = lappend zs (LCons y' ys'')"
and "xs' = LNil ∨ r (lhd xs') y'" by blast
with True LCons ‹ys = LCons y ys'›
show ?thesis by(cases zs) auto
qed
next
case False
with LCons llexord ‹ys = LCons y ys'›
have "r x y" by(fastforce elim: lfinite.cases)
with LCons ‹ys = LCons y ys'› show ?thesis by auto
qed
qed
qed
qed

lemma llexord_conv_ltake_index:
"llexord r xs ys ⟷
(llength xs ≤ llength ys ∧ ltake (llength xs) ys = xs) ∨
(∃n. enat n < min (llength xs) (llength ys) ∧
ltake (enat n) xs = ltake (enat n) ys ∧ r (lnth xs n) (lnth ys n))"
(is "?lhs ⟷ ?rhs")
proof(rule iffI)
assume ?lhs
thus ?rhs (is "?A ∨ ?B") unfolding llexord_conv
proof
assume "xs = ys" thus ?thesis by(simp add: ltake_all)
next
assume "∃zs xs' y ys'. lfinite zs ∧ xs = lappend zs xs' ∧
ys = lappend zs (LCons y ys') ∧
(xs' = LNil ∨ r (lhd xs') y)"
then obtain zs xs' y ys'
where "lfinite zs" "xs' = LNil ∨ r (lhd xs') y"
and [simp]: "xs = lappend zs xs'" "ys = lappend zs (LCons y ys')"
by blast
show ?thesis
proof(cases xs')
case LNil
hence ?A by(auto intro: enat_le_plus_same simp add: ltake_lappend1 ltake_all)
thus ?thesis ..
next
case LCons
with ‹xs' = LNil ∨ r (lhd xs') y› have "r (lhd xs') y" by simp
from ‹lfinite zs› obtain zs' where [simp]: "zs = llist_of zs'"
unfolding lfinite_eq_range_llist_of by blast
with LCons have "enat (length zs') < min (llength xs) (llength ys)"
by(auto simp add: less_enat_def eSuc_def split: enat.split)
moreover have "ltake (enat (length zs')) xs = ltake (enat (length zs')) ys"
moreover have "r (lnth xs (length zs')) (lnth ys (length zs'))"
using LCons ‹r (lhd xs') y›
ultimately have ?B by blast
thus ?thesis ..
qed
qed
next
assume ?rhs (is "?A ∨ ?B")
thus ?lhs
proof
assume ?A thus ?thesis
proof(coinduct)
case (llexord xs ys)
thus ?case by(cases xs, simp)(cases ys, auto)
qed
next
assume "?B"
then obtain n where len: "enat n < min (llength xs) (llength ys)"
and takexs: "ltake (enat n) xs = ltake (enat n) ys"
and r: "r (lnth xs n) (lnth ys n)" by blast
have "xs = lappend (ltake (enat n) xs) (ldrop (enat n) xs)"
by(simp only: lappend_ltake_ldrop)
moreover from takexs len
have "ys = lappend (ltake (enat n) xs) (LCons (lnth ys n) (ldrop (enat (Suc n)) ys))"
moreover from r len
have "r (lhd (ldrop (enat n) xs)) (lnth ys n)"
moreover have "lfinite (ltake (enat n) xs)" by simp
ultimately show ?thesis unfolding llexord_conv by blast
qed
qed

lemma llexord_llist_of:
"llexord r (llist_of xs) (llist_of ys) ⟷
xs = ys ∨ (xs, ys) ∈ lexord {(x, y). r x y}"
(is "?lhs ⟷ ?rhs")
proof
assume ?lhs
{ fix zs xs' y ys'
assume "lfinite zs" "llist_of xs = lappend zs xs'"
and "llist_of ys = lappend zs (LCons y ys')"
and "xs' = LNil ∨ r (lhd xs') y"
from ‹lfinite zs› obtain zs' where [simp]: "zs = llist_of zs'"
unfolding lfinite_eq_range_llist_of by blast
have "lfinite (llist_of xs)" by simp
hence "lfinite xs'" unfolding ‹llist_of xs = lappend zs xs'› by simp
then obtain XS' where [simp]: "xs' = llist_of XS'"
unfolding lfinite_eq_range_llist_of by blast
from ‹llist_of xs = lappend zs xs'› have [simp]: "xs = zs' @ XS'"
have "lfinite (llist_of ys)" by simp
hence "lfinite ys'" unfolding ‹llist_of ys = lappend zs (LCons y ys')› by simp
then obtain YS' where [simp]: "ys' = llist_of YS'"
unfolding lfinite_eq_range_llist_of by blast
from ‹llist_of ys = lappend zs (LCons y ys')› have [simp]: "ys = zs' @ y # YS'"
by(auto simp add: llist_of.simps(2)[symmetric] lappend_llist_of_llist_of simp del: llist_of.simps(2))
have "(∃a ys'. ys = xs @ a # ys') ∨
(∃zs a b. r a b ∧ (∃xs'. xs = zs @ a # xs') ∧ (∃ys'. ys = zs @ b # ys'))"
(is "?A ∨ ?B")
proof(cases xs')
case LNil thus ?thesis by(auto simp add: llist_of_eq_LNil_conv)
next
case (LCons x xs'')
with ‹xs' = LNil ∨ r (lhd xs') y›
have "r (lhd xs') y" by(auto simp add: llist_of_eq_LCons_conv)
with LCons have ?B by(auto simp add: llist_of_eq_LCons_conv) fastforce
thus ?thesis ..
qed
hence "(xs, ys) ∈ {(x, y). ∃a v. y = x @ a # v ∨
(∃u a b v w. (a, b) ∈ {(x, y). r x y} ∧
x = u @ a # v ∧ y = u @ b # w)}"
by auto }
with ‹?lhs› show ?rhs
unfolding lexord_def llexord_conv llist_of_inject by blast
next
assume "?rhs"
thus ?lhs
proof
assume "xs = ys" thus ?thesis by simp
next
assume "(xs, ys) ∈ lexord {(x, y). r x y}"
thus ?thesis
by(coinduction arbitrary: xs ys)(auto, auto simp add: neq_Nil_conv)
qed
qed

subsection ‹The filter functional on lazy lists: @{term "lfilter"}›

lemma lfilter_code [simp, code]:
shows lfilter_LNil: "lfilter P LNil = LNil"
and lfilter_LCons: "lfilter P (LCons x xs) = (if P x then LCons x (lfilter P xs) else lfilter P xs)"

declare lfilter.mono[cont_intro]

lemma mono2mono_lfilter[THEN llist.mono2mono, simp, cont_intro]:
shows monotone_lfilter: "monotone (⊑) (⊑) (lfilter P)"
by(rule llist.fixp_preserves_mono1[OF lfilter.mono lfilter_def]) simp

lemma mcont2mcont_lfilter[THEN llist.mcont2mcont, simp, cont_intro]:
shows mcont_lfilter: "mcont lSup (⊑) lSup (⊑) (lfilter P)"
by(rule llist.fixp_preserves_mcont1[OF lfilter.mono lfilter_def]) simp

lemma lfilter_mono [partial_function_mono]:
"mono_llist A ⟹ mono_llist (λf. lfilter P (A f))"
by(rule mono2mono_lfilter)

lemma lfilter_LCons_seek: "~ (p x) ==> lfilter p (LCons x l) = lfilter p l"
by simp

lemma lfilter_LCons_found:
"P x ⟹ lfilter P (LCons x xs) = LCons x (lfilter P xs)"
by simp

lemma lfilter_eq_LNil: "lfilter P xs = LNil ⟷ (∀x ∈ lset xs. ¬ P x)"
by(induction xs) simp_all

fix P xs
have "(lfilter P xs = LNil) ⟷ (∀x ∈ lset xs. ¬ P x)"
proof(intro iffI strip)
assume "∀x ∈ lset xs. ¬ P x"
hence "lfilter P xs ⊑ LNil"
by(induction arbitrary: xs rule: lfilter.fixp_induct)(simp_all split: llist.split del: lprefix_LNil)
thus "lfilter P xs = LNil" by simp
next
fix x
assume "x ∈ lset xs" "lfilter P xs = LNil"
thus "¬ P x" by induction(simp_all split: if_split_asm)
qed
end

lemma diverge_lfilter_LNil [simp]: "∀x∈lset xs. ¬ P x ⟹ lfilter P xs = LNil"

lemmas lfilter_False = diverge_lfilter_LNil

lemma lnull_lfilter [simp]: "lnull (lfilter P xs) ⟷ (∀x∈lset xs. ¬ P x)"

lemmas lfilter_empty_conv = lfilter_eq_LNil

lemma lhd_lfilter [simp]: "lhd (lfilter P xs) = lhd (ldropWhile (Not ∘ P) xs)"
proof(cases "∃x∈lset xs. P x")
case True
then obtain x where "x ∈ lset xs" and "P x" by blast
from ‹x ∈ lset xs› show ?thesis by induct(simp_all add: ‹P x›)

lemma ltl_lfilter: "ltl (lfilter P xs) = lfilter P (ltl (ldropWhile (Not ∘ P) xs))"
by(induct xs) simp_all

lemma lfilter_eq_LCons:
"lfilter P xs = LCons x xs' ⟹
∃xs''. xs' = lfilter P xs'' ∧ ldropWhile (Not ∘ P) xs = LCons x xs''"
by(drule eq_LConsD)(auto intro!: exI simp add: ltl_lfilter o_def ldropWhile_eq_LNil_iff intro: llist.expand)

lemma lfilter_K_True [simp]: "lfilter (%_. True) xs = xs"
by(induct xs) simp_all

lemma lfitler_K_False [simp]: "lfilter (λ_. False) xs = LNil"
by simp

lemma lfilter_lappend_lfinite [simp]:
"lfinite xs ⟹ lfilter P (lappend xs ys) = lappend (lfilter P xs) (lfilter P ys)"
by(induct rule: lfinite.induct) auto

lemma lfinite_lfilterI [simp]: "lfinite xs ⟹ lfinite (lfilter P xs)"
by(induct rule: lfinite.induct) simp_all

lemma lset_lfilter [simp]: "lset (lfilter P xs) = {x ∈ lset xs. P x}"

notepad begin ― ‹show @{thm [source] lset_lfilter} by fixpoint induction›
note [simp del] = lset_lfilter
fix P xs
have "lset (lfilter P xs) = lset xs ∩ {x. P x}" (is "?lhs = ?rhs")
proof
show "?lhs ⊆ ?rhs"
by(induct arbitrary: xs rule: lfilter.fixp_induct)(auto split: llist.split)
show "?rhs ⊆ ?lhs"
proof
fix x
assume "x ∈ ?rhs"
hence "x ∈ lset xs" "P x" by simp_all
thus "x ∈ ?lhs" by induction simp_all
qed
qed
end

lemma lfilter_lfilter: "lfilter P (lfilter Q xs) = lfilter (λx. P x ∧ Q x) xs"
by(induction xs) simp_all

notepad begin ― ‹show @{thm [source] lfilter_lfilter} by fixpoint induction›
fix P Q xs
have "∀xs. lfilter P (lfilter Q xs) ⊑ lfilter (λx. P x ∧ Q x) xs"
by(rule lfilter.fixp_induct)(auto split: llist.split)
moreover have "∀xs. lfilter (λx. P x ∧ Q x) xs ⊑ lfilter P (lfilter Q xs)"
by(rule lfilter.fixp_induct)(auto split: llist.split)
ultimately have "lfilter P (lfilter Q xs) = lfilter (λx. P x ∧ Q x) xs"
by(blast intro: lprefix_antisym)
end

lemma lfilter_idem [simp]: "lfilter P (lfilter P xs) = lfilter P xs"

lemma lfilter_lmap: "lfilter P (lmap f xs) = lmap f (lfilter (P o f) xs)"
by(induct xs) simp_all

lemma lfilter_llist_of [simp]:
"lfilter P (llist_of xs) = llist_of (filter P xs)"
by(induct xs) simp_all

lemma lfilter_cong [cong]:
assumes xsys: "xs = ys"
and set: "⋀x. x ∈ lset ys ⟹ P x = Q x"
shows "lfilter P xs = lfilter Q ys"
using set unfolding xsys

lemma llength_lfilter_ile:
"llength (lfilter P xs) ≤ llength xs"
by(induct xs)(auto intro: order_trans)

lemma lfinite_lfilter:
"lfinite (lfilter P xs) ⟷
lfinite xs ∨ finite {n. enat n < llength xs ∧ P (lnth xs n)}"
proof
assume "lfinite (lfilter P xs)"
{ assume "¬ lfinite xs"
with ‹lfinite (lfilter P xs)›
have "finite {n. enat n < llength xs ∧ P (lnth xs n)}"
proof(induct ys≡"lfilter P xs" arbitrary: xs rule: lfinite_induct)
case LNil
hence "∀x∈lset xs. ¬ P x" by(auto)
hence eq: "{n. enat n < llength xs ∧ P (lnth xs n)} = {}"
show ?case unfolding eq ..
next
case (LCons xs)
from ‹¬ lnull (lfilter P xs)›
have exP: "∃x∈lset xs. P x" by simp
let ?xs = "ltl (ldropWhile (λx. ¬ P x) xs)"
let ?xs' = "ltakeWhile (λx. ¬ P x) xs"
from exP obtain n where n: "llength ?xs' = enat n"
using lfinite_conv_llength_enat[of ?xs']
have "finite ({n. enat n < llength ?xs} ∩ {n. P (lnth ?xs n)})" (is "finite ?A")
hence "finite ((λm. n + 1 + m) ` ({n. enat n < llength ?xs} ∩ {n. P (lnth ?xs n)}))"
(is "finite (?f ` _)")
by(rule finite_imageI)
moreover have xs: "xs = lappend ?xs' (LCons (lhd (ldropWhile (λx. ¬ P x) xs)) ?xs)"
using exP by simp
{ fix m
assume "m < n"
hence "lnth ?xs' m ∈ lset ?xs'" using n
unfolding in_lset_conv_lnth by auto
hence "¬ P (lnth ?xs' m)" by(auto dest: lset_ltakeWhileD) }
hence "{n. enat n < llength xs ∧ P (lnth xs n)} ⊆ insert (the_enat (llength ?xs')) (?f ` ?A)"
using n by(subst (1 2) xs)(cases "llength ?xs", auto simp add: lnth_lappend not_less not_le lnth_LCons' eSuc_enat split: if_split_asm intro!: rev_image_eqI)
ultimately show ?case by(auto intro: finite_subset)
qed }
thus "lfinite xs ∨ finite {n. enat n < llength xs ∧ P (lnth xs n)}" by blast
next
assume "lfinite xs ∨ finite {n. enat n < llength xs ∧ P (lnth xs n)}"
moreover {
assume "lfinite xs"
with llength_lfilter_ile[of P xs] have "lfinite (lfilter P xs)"
} moreover {
assume nfin: "¬ lfinite xs"
hence len: "llength xs = ∞" by(rule not_lfinite_llength)
assume fin: "finite {n. enat n < llength xs ∧ P (lnth xs n)}"
then obtain m where "{n. enat n < llength xs ∧ P (lnth xs n)} ⊆ {..<m}"
unfolding finite_nat_iff_bounded by auto
hence "⋀n. ⟦ m ≤ n; enat n < llength xs ⟧ ⟹ ¬ P (lnth xs n)" by auto
hence "lfinite (lfilter P xs)"
proof(induct m arbitrary: xs)
case 0
hence "lnull (lfilter P xs)" by(auto simp add: in_lset_conv_lnth)
thus ?case by simp
next
case (Suc m)
{ fix n
assume "m ≤ n" "enat n < llength (ltl xs)"
hence "Suc m ≤ Suc n" "enat (Suc n) < llength xs"
by(case_tac [!] xs)(auto simp add: Suc_ile_eq)
hence "¬ P (lnth xs (Suc n))" by(rule Suc)
hence "¬ P (lnth (ltl xs) n)"
using ‹enat n < llength (ltl xs)› by(cases xs) (simp_all) }
hence "lfinite (lfilter P (ltl xs))" by(rule Suc)
thus ?case by(cases xs) simp_all
qed }
ultimately show "lfinite (lfilter P xs)" by blast
qed

lemma lfilter_eq_LConsD:
assumes "lfilter P ys = LCons x xs"
shows "∃us vs. ys = lappend us (LCons x vs) ∧ lfinite us ∧
(∀u∈lset us. ¬ P u) ∧ P x ∧ xs = lfilter P vs"
proof -
let ?us = "ltakeWhile (Not ∘ P) ys"
and ?vs = "ltl (ldropWhile (Not ∘ P) ys)"
from assms have "¬ lnull (lfilter P ys)" by auto
hence exP: "∃x∈lset ys. P x" by simp
from eq_LConsD[OF assms]
have x: "x = lhd (ldropWhile (Not ∘ P) ys)"
and xs: "xs = ltl (lfilter P ys)" by auto
from exP
have "ys = lappend ?us (LCons x ?vs)" unfolding x by simp
moreover have "lfinite ?us" using exP by(simp add: lfinite_ltakeWhile)
moreover have "∀u∈lset ?us. ¬ P u" by(auto dest: lset_ltakeWhileD)
moreover have "P x" unfolding x o_def
using exP by(rule lhd_ldropWhile[where P="Not ∘ P", simplified])
moreover have "xs = lfilter P ?vs" unfolding xs by(simp add: ltl_lfilter)
ultimately show ?thesis by blast
qed

lemma lfilter_eq_lappend_lfiniteD:
assumes "lfilter P xs = lappend ys zs" and "lfinite ys"
shows "∃us vs. xs = lappend us vs ∧ lfinite us ∧
ys = lfilter P us ∧ zs = lfilter P vs"
using ‹lfinite ys› ‹lfilter P xs = lappend ys zs›
proof(induct arbitrary: xs zs)
case lfinite_LNil
hence "xs = lappend LNil xs" "LNil = lfilter P LNil" "zs = lfilter P xs"
by simp_all
thus ?case by blast
next
case (lfinite_LConsI ys y)
note IH = ‹⋀xs zs. lfilter P xs = lappend ys zs ⟹
∃us vs. xs = lappend us vs ∧ lfinite us ∧
ys = lfilter P us ∧ zs = lfilter P vs›
from ‹lfilter P xs = lappend (LCons y ys) zs›
have "lfilter P xs = LCons y (lappend ys zs)" by simp
from lfilter_eq_LConsD[OF this] obtain us vs
where xs: "xs = lappend us (LCons y vs)" "lfinite us"
"P y" "∀u∈lset us. ¬ P u"
and vs: "lfilter P vs = lappend ys zs" by auto
from IH[OF vs] obtain us' vs' where "vs = lappend us' vs'" "lfinite us'"
and "ys = lfilter P us'" "zs = lfilter P vs'" by blast
with xs show ?case
by(fastforce simp add: lappend_snocL1_conv_LCons2[symmetric, where ys="lappend us' vs'"]
lappend_assoc[symmetric])
qed

lemma ldistinct_lfilterI: "ldistinct xs ⟹ ldistinct (lfilter P xs)"
by(induction xs) simp_all

fix P xs
assume *: "ldistinct xs"
from * have "ldistinct (lfilter P xs) ∧ lset (lfilter P xs) ⊆ lset xs"
by(induction arbitrary: xs rule: lfilter.fixp_induct)(simp_all split: llist.split, fastforce)
from * have "ldistinct (lfilter P xs)"
― ‹only works because we use strong fixpoint induction›
by(induction arbitrary: xs rule: lfilter.fixp_induct)(simp_all split: llist.split, auto 4 4 dest: monotone_lset[THEN monotoneD] simp add: fun_ord_def)
end

lemma ldistinct_lfilterD:
"⟦ ldistinct (lfilter P xs); enat n < llength xs; enat m < llength xs; P a; lnth xs n = a; lnth xs m = a ⟧ ⟹ m = n"
proof(induct n m rule: wlog_linorder_le)
case symmetry thus ?case by simp
next
case (le n m)
thus ?case
proof(induct n arbitrary: xs m)
case 0 thus ?case
proof(cases m)
case 0 thus ?thesis .
next
case (Suc m')
with 0 show ?thesis