Theory Coinductive.Coinductive_List

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

section ‹Coinductive lists and their operations›

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

subsection ‹Auxiliary lemmata›

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

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

subsection ‹Type definition›

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


text ‹
  Coiterator setup.
›

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

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

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

text ‹congruence rule›

declare llist.map_cong [cong]

text ‹Code generator setup›

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

text ‹lemmas about generated constants›

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')"
unfolding lnull_def by(simp add: neq_LNil_conv)

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")
apply(simp_all add: find step)
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"
by(auto simp add: gen_lset_def)

lemma lset_code [code]:
  "lset = gen_lset {}"
by(simp add: gen_lset_def fun_eq_iff)

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"
by(simp_all add: lmember_def)

lemma lset_lmember [code_unfold]:
  "x ∈ lset xs ⟷ lmember x xs"
by(simp add: lmember_def)

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:
  "lnull (lappend xs ys) ⟷ lnull xs ∧ lnull ys"
by(auto simp add: lappend_def)

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)"
by(simp add: lappend_assoc)

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
    thus ?case by(simp add: LNil_eq_lappend_iff)
  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)"
by(simp add: lappend_inf)

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

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
      by(cases xs)(auto simp add: not_lnull_conv)
  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"
by(simp add: lnull_def)

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"
by(simp add: lprefix_LCons_conv)

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"
by(cases ys)(auto simp add: lprefix_LCons_conv)

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"
by(clarsimp simp add: not_lnull_conv LCons_lprefix_conv)

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
qed(simp add: lappend_inf)

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)"
by(simp add: lSup_def)

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

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"
by(simp add: lSup_def)

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
    by(cases xs)(auto simp add: lprefix_LCons_conv)
  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
  thus ?case by(simp add: lSup_finite_prefixes)
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)

lemmas [cont_intro] = ccpo.admissible_leI[OF llist_ccpo]

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:
  assumes adm: "ccpo.admissible lSup (⊑) P"
  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)"
    by(rule ccpo.admissibleD)(auto intro: ys zs)
  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]:
  assumes adm: "ccpo.admissible lSup (⊑) P"
  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
  show ?thesis using adm
    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})))"
    by(simp add: lSup_insert_LNil)
  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"
by(simp add: mcont_def monotone_ltl cont_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)"
    using mcont_ltl by(rule admissible_subst)
  have [cont_intro]: "ccpo.admissible lSup (⊑) (λys. ¬ lnull ys ∧ lhd ys ≠ x)"
  proof(rule ccpo.admissibleI)
    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)"
    by(simp add: eq)
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)"
    by(rule admissible_subst)(rule mcont_LCons)
  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"
    by(rule ccpo.admissibleD)(auto dest: lprefix_antisym)
  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"
by(cases xs)(simp_all add: hd_def lhd_def)

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)"
by(auto)(auto simp add: list_of_def)

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"
by(clarsimp simp add: lfinite_eq_range_llist_of)

lemma tl_list_of: "lfinite xs ⟹ tl (list_of xs) = list_of (ltl xs)"
by(auto simp add: lfinite_eq_range_llist_of)

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 []"
by(simp add: fun_eq_iff list_of_def list_of_aux_def)

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"
by(simp_all add: list_of_aux_def)

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)"
by(simp_all add: llength_def enat_unfold)

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"
by(coinduction arbitrary: xs ys rule: enat_coinduct)(simp_all add: iadd_is_0 epred_iadd1 split_paired_all epred_llength, auto)

lemma llength_llist_of [simp]:
  "llength (llist_of xs) = enat (length xs)"
by(induct xs)(simp_all add: zero_enat_def eSuc_def)

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'"
    by(cases xs)(auto simp add: zero_enat_def)
  moreover with len have "llength xs' = enat n"
    by(simp add: eSuc_def split: enat.split_asm)
  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 = ∞"
by(simp add: lfinite_conv_llength_enat)

lemma llength_eq_infty_conv_lfinite:
  "llength xs = ∞ ⟷ ¬ lfinite xs"
by(simp add: lfinite_conv_llength_enat)

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"
by(simp_all add: gen_llength_def iadd_Suc eSuc_enat[symmetric] iadd_Suc_right)

lemma llength_code [code]: "llength = gen_llength 0"
by(simp add: gen_llength_def fun_eq_iff zero_enat_def)

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"
by(simp add: ltake_def)

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(simp add: ltake_all)
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))"
  proof(rule ccpo.admissibleD)
    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"
by(simp add: ldropn_def)

lemma ldropn_LNil [code, simp]: "ldropn n LNil = LNil"
by(induct n)(simp_all add: ldropn_def)

lemma ldropn_lnull: "lnull xs ⟹ ldropn n xs = LNil"
by(simp add: lnull_def)

lemma ldropn_LCons [code]:
  "ldropn n (LCons x xs) = (case n of 0 ⇒ LCons x xs | Suc n' ⇒ ldropn n' xs)"
by(cases n)(simp_all add: ldropn_def funpow_swap1)

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"
by(simp add: ldropn_LCons)

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"
by(simp_all add: ldrop.simps split: co.enat.split)

lemma ldrop_lnull: "lnull xs ⟹ ldrop n xs = LNil"
by(simp add: lnull_def)

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])
  (simp add: ldropn_fixp_case_conv monotone_fun_ord_apply)

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])
  (simp add: ldropn_fixp_case_conv mcont_fun_lub_apply)

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)"
by(simp add: monotone_ldrop[simplified])

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)"
by(simp add: mcont_ldrop[simplified])

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
    by(cases xs)(simp_all add: eSuc_enat[symmetric])
qed(simp add: zero_enat_def[symmetric])

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"
by(simp add: ldropn_eq_LNil)

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

lemma ltl_ldrop: "ltl (ldrop n xs) = ldrop n (ltl xs)"
by(simp add: ldrop_eSuc_conv_ltl ldrop_ltl)

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"
by(induction xs)(simp_all add: ldrop_LCons enat_cocase_inf)

lemma ldrop_enat [code]: "ldrop (enat n) xs = ldropn n xs"
proof(induct n arbitrary: xs)
  case Suc thus ?case
    by(cases xs)(simp_all add: eSuc_enat[symmetric])
qed(simp add: zero_enat_def[symmetric])

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 = ∞"
by(cases n)(simp_all add: ldrop_enat)

lemma ldropn_ltl: "ldropn n (ltl xs) = ldropn (Suc n) xs"
by(simp add: ldropn_def funpow_swap1)

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"
by(auto simp add: ldropn_lappend)

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))"
by(coinduction arbitrary: n m xs rule: llist.coinduct_strong)(auto intro!: exI simp add: iadd_is_0 ltl_ltake epred_iadd1 ldrop_ltl)

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"
by(rule ccontr)(simp add: not_less ldrop_all)

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)
  case LCons thus ?case by(cases m rule: co.enat.exhaust)(simp_all add: iadd_Suc_right)
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)"
by(induct xs arbitrary: n m)(simp_all add: ldrop_LCons iadd_Suc_right split: co.enat.split)

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"
by(cases n)(simp_all add: lnth.simps)

lemma lnth_0 [simp]:
  "lnth (LCons x xs) 0 = x"
by(simp add: lnth.simps)

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

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))"
by(simp add: lnth_LCons split: nat.split)

lemma lhd_conv_lnth:
  "¬ lnull xs ⟹ lhd xs = lnth xs 0"
by(auto simp add: lhd_def not_lnull_conv)

lemmas lnth_0_conv_lhd = lhd_conv_lnth[symmetric]

lemma lnth_ltl: "¬ lnull xs ⟹ lnth (ltl xs) n = lnth xs (Suc n)"
by(auto simp add: not_lnull_conv)

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
      by(simp add: zero_enat_def[symmetric] lhd_conv_lnth)
  next
    case (Suc n')
    thus ?case
      by(cases xs)(simp_all add: eSuc_enat[symmetric], simp add: eSuc_enat)
  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'"
    by(cases xs)(auto simp add: Suc_ile_eq)
  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)"
by(cases n)(simp_all add: ldrop_enat)

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
      by(auto simp add: zero_enat_def[symmetric] not_lnull_conv)
  next
    case (Suc n)
    thus ?case
      by(cases xs)(auto simp add: eSuc_enat[symmetric])
  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}"
by(auto simp add: in_lset_conv_lnth)

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'"
    by(cases xs)(auto simp add: Suc_ile_eq)
  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'"
      by(auto simp add: lfinite_eq_range_llist_of)
    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))"
by(simp add: lmap_iterates)(rule iterates)

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
    by(subst iterates)(simp add: eSuc_enat[symmetric] funpow_swap1)
qed(simp add: zero_enat_def[symmetric])

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}"
by(auto simp add: lset_conv_lnth)

lemma lset_repeat [simp]: "lset (repeat x) = {x}"
by(simp add: lset_iterates id_def[symmetric])

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"
by(auto simp add: lstrict_prefix_def)

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"
    by(rule ccpo.admissibleD)(auto intro: assms)
  thus ?thesis by(simp add: ltake_all)
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
      using eq by(simp add: lappend_assoc)
    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"
    by(subst (asm) lappend_eq_lappend_conv)(simp_all add: min_def)
  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"
by(clarsimp simp add: lappend_llist_of_llist_of[symmetric] lprefix_lappend)

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)"
by(simp_all add: lprefix_LCons_conv finite_lprefix_def lnull_def)

lemma lprefix_nitpick_simps [nitpick_simp]:
  "xs ⊑ ys = (if lfinite xs then finite_lprefix xs ys else xs = ys)"
by(simp add: finite_lprefix_def not_lfinite_lprefix_conv_eq)

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"
by(simp add: llcp_def)

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

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"
by(coinduction arbitrary: xs rule: enat_coinduct)(auto simp add: iadd_is_0 llcp_eq_0_iff epred_iadd1 epred_llcp epred_llength)

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"
by(simp add: lzip_def)

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)"
by(simp add: monotone_lzip[simplified])

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

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)"
by(simp add: mcont_lzip[simplified])

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

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
    by(simp add: zero_enat_def[symmetric] lnth_0_conv_lhd)
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)}"
by(auto simp add: lset_conv_lnth lnth_lzip)(auto intro!: exI simp add: lnth_lzip)

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"
    by(auto simp add: enat_le_plus_same)
  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''"
    by(simp_all add: lappend_ltake_ldrop)
  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'')"
    by(simp add: lzip_lappend min_def)
  hence us: "us = lzip ?xs' ?ys'"
    and vs: "lfinite us ⟶ vs = lzip ?xs'' ?ys''" using len
    by(simp_all add: min_def lappend_eq_lappend_conv)
  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
             simp add: ltake_all dest: lfinite_llength_enat)
    with ‹xs = ?xs'› ‹ys = ?ys'›
    have "xs = lappend ?xs' ?xs''" "ys = lappend ?ys' ?ys''"
      by(simp_all add: lappend_inf)
    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)"
by(simp_all add: ldropWhile.simps)

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")
unfolding lnull_def by(simp add: ldropWhile_eq_LNil_iff)

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"
by(simp add: ltakeWhile_def)

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"
by(simp add: ldropWhile_eq_ldrop)

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)"
by(simp add: ldropWhile_eq_ldrop ltakeWhile_repeat)

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)))"
by(simp add: ldropWhile_eq_ldrop lhd_ldrop llength_ltakeWhile_lt_iff)

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"
by(simp add: llist_all2_conv_lzip)

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"
by(auto simp add: llist_all2_conv_lzip lset_lzip)

lemma llist_all2_lnthD:
  "⟦ llist_all2 P xs ys; enat n < llength xs ⟧ ⟹ P (lnth xs n) (lnth ys n)"
by(fastforce simp add: llist_all2_conv_lzip lset_lzip)

lemma llist_all2_lnthD2:
  "⟦ llist_all2 P xs ys; enat n < llength ys ⟧ ⟹ P (lnth xs n) (lnth ys n)"
by(fastforce simp add: llist_all2_conv_lzip lset_lzip)

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"
by(simp add: llist_all2_conv_all_lnth)

lemma llist_all2_reflI:
  "(⋀x. x ∈ lset xs ⟹ P x x) ⟹ llist_all2 P xs xs"
by(auto simp add: llist_all2_conv_all_lnth lset_conv_lnth)

lemma llist_all2_lmap1:
  "llist_all2 P (lmap f xs) ys ⟷ llist_all2 (λx. P (f x)) xs ys"
by(auto simp add: llist_all2_conv_all_lnth)

lemma llist_all2_lmap2:
  "llist_all2 P xs (lmap g ys) ⟷ llist_all2 (λx y. P x (g y)) xs ys"
by(auto simp add: llist_all2_conv_all_lnth)

lemma llist_all2_lfiniteD:
  "llist_all2 P xs ys ⟹ lfinite xs ⟷ lfinite ys"
by(drule llist_all2_llengthD)(simp add: lfinite_conv_llength_enat)

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
by(cases xs)(auto simp add: llist_all2_LCons1)

lemma llist_all2_mono:
  "⟦ llist_all2 P xs ys; ⋀x y. P x y ⟹ P' x y ⟧ ⟹ llist_all2 P' xs ys"
by(auto simp add: llist_all2_conv_all_lnth)

lemma llist_all2_left: "llist_all2 (λx _. P x) xs ys ⟷ llength xs = llength ys ∧ (∀x∈lset xs. P x)"
by(fastforce simp add: llist_all2_conv_all_lnth lset_conv_lnth)

lemma llist_all2_right: "llist_all2 (λ_. P) xs ys ⟷ llength xs = llength ys ∧ (∀x∈lset ys. P x)"
by(fastforce simp add: llist_all2_conv_all_lnth lset_conv_lnth)

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"
by(auto simp add: llist_all2_conv_all_lnth)

lemma llist_all2_lhdD:
  "⟦ llist_all2 P xs ys; ¬ lnull xs ⟧ ⟹ P (lhd xs) (lhd ys)"
by(auto simp add: not_lnull_conv llist_all2_LCons1)

lemma llist_all2_lhdD2:
  "⟦ llist_all2 P xs ys; ¬ lnull ys ⟧ ⟹ P (lhd xs) (lhd ys)"
by(auto simp add: not_lnull_conv llist_all2_LCons2)

lemma llist_all2_ltlI:
  "llist_all2 P xs ys ⟹ llist_all2 P (ltl xs) (ltl ys)"
by(cases xs)(auto simp add: llist_all2_LCons1)

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)"
      using len_xs by(simp add: min_def)
  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"
by(cases xs)(auto simp add: not_lnull_conv)

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)"
by(auto simp add: llist_all2_conv_all_lnth lnth_ltake)

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

lemma admissible_llist_all2 [cont_intro, simp]:
  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))"
proof(rule ccpo.admissibleI)
  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(simp add: llist_all2_llengthD)
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"
by(simp add: llast_def zero_enat_def)

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"
by(simp add: llast_def lfinite_conv_llength_enat)

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

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"
    by(induct rule: lfinite.induct)(simp_all add: llast_LCons)
  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)"
by(simp add: llast_lappend)

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"}›

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

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

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)"
by(clarsimp simp add: not_lnull_conv)

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

lemma admissible_ldistinct [cont_intro, simp]:
  assumes mcont: "mcont lub ord lSup (⊑) (λx. f x)"
  shows "ccpo.admissible lub ord (λx. ldistinct (f x))"
proof(rule ccpo.admissibleI)
  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"
    by(coinduct)(auto simp add: not_lnull_conv in_lset_lappend_iff)

  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"
by(clarsimp simp add: lprefix_conv_lappend ldistinct_lappend)

lemma admissible_not_ldistinct[THEN admissible_subst, cont_intro, simp]:
  "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'"
      by(auto simp add: not_lnull_conv)
    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"
        by(simp_all add: LCons Suc_ile_eq zero_enat_def[symmetric])
      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"
        by(simp_all add: LCons Suc_ile_eq)
      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"
    by(coinduct)(auto simp add: not_lnull_conv)

  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

lemma admissible_lsorted [cont_intro, simp]:
  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))"
proof(rule ccpo.admissibleI)
  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

lemma admissible_not_lsorted[THEN admissible_subst, cont_intro, simp]:
  "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]
  ord.admissible_lsorted [cont_intro, simp]
  ord.admissible_not_lsorted [THEN admissible_subst, cont_intro, simp]

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"
by(clarsimp simp add: not_lnull_conv lsorted_LCons)

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
by(coinduct)(auto simp add: not_lnull_conv LCons_lprefix_conv)

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)"
by(rule lprefix_imp_llexord)(auto simp add: lprefix_conv_lappend)

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"
        by(simp add: ltake_lappend1)
      moreover have "r (lnth xs (length zs')) (lnth ys (length zs'))"
        using LCons ‹r (lhd xs') y›
        by(simp add: lappend_llist_of_LCons lnth_lappend1)
      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))"
      by(simp add: ldropn_Suc_conv_ldropn ldrop_enat)
    moreover from r len
    have "r (lhd (ldrop (enat n) xs)) (lnth ys n)"
      by(simp add: lhd_ldrop)
    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'"
      by(simp add: lappend_llist_of_llist_of)
    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)"
by(simp_all add: lfilter.simps)

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

notepad begin
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"
by(simp add: lfilter_eq_LNil)

lemmas lfilter_False = diverge_lfilter_LNil

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

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›)
qed(simp add: o_def)

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}"
by induct(auto simp add: Collect_conj_eq)

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"
by(simp add: lfilter_lfilter)

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
by(induction ys)(simp_all add: Bex_def[symmetric])

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)} = {}"
        by(auto simp add: lset_conv_lnth)
      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']
        by(auto simp add: lfinite_ltakeWhile)
      have "finite ({n. enat n < llength ?xs} ∩ {n. P (lnth ?xs n)})" (is "finite ?A")
        using LCons [[simproc add: finite_Collect]] by(auto simp add: ltl_lfilter lfinite_ldropWhile)
      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)"
      by(auto simp add: lfinite_eq_range_llist_of)
  } 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

notepad begin
  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
        by(cases xs)(simp_all add: Suc_ile_eq, auto simp add: lset_conv_lnth)
    qed
  next
    case (Suc n)
    from ‹Suc n ≤ m› obtain m' where m [simp]: "m = Suc m'" by(cases m) simp
    with ‹Suc n ≤ m› have "n ≤ m'" by simp
    moreover from ‹enat (Suc n) < llength xs›
    obtain x xs' where xs [simp]: "xs = LCons x xs'" by(cases xs) simp
    from ‹ldistinct (lfilter P xs)› have "ldistinct (lfilter P xs')" by(simp split: if_split_asm)
    moreover from ‹enat (Suc n) < llength xs› ‹enat m < llength xs›
    have "enat n < llength xs'" "enat m' < llength xs'" by(simp_all add: Suc_ile_eq)
    moreover note ‹P a›
    moreover have "lnth xs' n = a" "lnth xs' m' = a"
      using ‹lnth xs (Suc n) = a› ‹lnth xs m = a› by simp_all
    ultimately have "m' = n" by(rule Suc)
    thus ?case by simp
  qed
qed

lemmas lfilter_fixp_parallel_induct =
  parallel_fixp_induct_1_1[OF llist_partial_function_definitions llist_partial_function_definitions
    lfilter.mono lfilter.mono lfilter_def lfilter_def, case_names adm LNil step]

lemma llist_all2_lfilterI:
  assumes *: "llist_all2 P xs ys"
  and Q: "⋀x y. P x y ⟹ Q1 x ⟷ Q2 y"
  shows "llist_all2 P (lfilter Q1 xs) (lfilter Q2 ys)"
using * by(induction arbitrary: xs ys rule: lfilter_fixp_parallel_induct)(auto split: llist.split dest: Q)

lemma distinct_filterD:
  "⟦ distinct (filter P xs); n < length xs; m < length xs; P x; xs ! n = x; xs ! m = x ⟧ ⟹ m = n"
using ldistinct_lfilterD[of P "llist_of xs" n m x] by simp

lemma lprefix_lfilterI:
  "xs ⊑ ys ⟹ lfilter P xs ⊑ lfilter P ys"
by(rule monotoneD[OF monotone_lfilter])

context preorder begin

lemma lsorted_lfilterI:
  "lsorted xs ⟹ lsorted (lfilter P xs)"
by(induct xs)(simp_all add: lsorted_LCons)

lemma lsorted_lfilter_same:
  "lsorted (lfilter (λx. x = c) xs)"
by(induct xs)(auto simp add: lsorted_LCons)

end

lemma lfilter_id_conv: "lfilter P xs = xs ⟷ (∀x∈lset xs. P x)" (is "?lhs ⟷ ?rhs")
proof
  assume ?rhs thus ?lhs by(induct xs) auto
next
  assume ?lhs
  with lset_lfilter[of P xs] show ?rhs by auto
qed

lemma lfilter_repeat [simp]: "lfilter P (repeat x) = (if P x then repeat x else LNil)"
by(simp add: lfilter_id_conv)

subsection ‹Concatenating all lazy lists in a lazy list: @{term "lconcat"}›

lemma lconcat_simps [simp, code]:
  shows lconcat_LNil: "lconcat LNil = LNil"
  and lconcat_LCons: "lconcat (LCons xs xss) = lappend xs (lconcat xss)"
by(simp_all add: lconcat.simps)

declare lconcat.mono[cont_intro]

lemma mono2mono_lconcat[THEN llist.mono2mono, cont_intro, simp]:
  shows monotone_lconcat: "monotone (⊑) (⊑) lconcat"
by(rule llist.fixp_preserves_mono1[OF lconcat.mono lconcat_def]) simp

lemma mcont2mcont_lconcat[THEN llist.mcont2mcont, cont_intro, simp]:
  shows mcont_lconcat: "mcont lSup (⊑) lSup (⊑) lconcat"
by(rule llist.fixp_preserves_mcont1[OF lconcat.mono lconcat_def]) simp

lemma lconcat_eq_LNil: "lconcat xss = LNil ⟷ lset xss ⊆ {LNil}" (is "?lhs ⟷ ?rhs")
by(induction xss)(auto simp add: lappend_eq_LNil_iff)

lemma lnull_lconcat [simp]: "lnull (lconcat xss) ⟷ lset xss ⊆ {xs. lnull xs}"
unfolding lnull_def by(simp add: lconcat_eq_LNil)

lemma lconcat_llist_of:
  "lconcat (llist_of (map llist_of xs)) = llist_of (concat xs)"
by(induct xs)(simp_all add: lappend_llist_of_llist_of)

lemma lhd_lconcat [simp]:
  "⟦ ¬ lnull xss; ¬ lnull (lhd xss) ⟧ ⟹ lhd (lconcat xss) = lhd (lhd xss)"
by(clarsimp simp add: not_lnull_conv)

lemma ltl_lconcat [simp]:
  "⟦ ¬ lnull xss; ¬ lnull (lhd xss) ⟧ ⟹ ltl (lconcat xss) = lappend (ltl (lhd xss)) (lconcat (ltl xss))"
by(clarsimp simp add: not_lnull_conv)

lemma lmap_lconcat:
  "lmap f (lconcat xss) = lconcat (lmap (lmap f) xss)"
by(induct xss)(simp_all add: lmap_lappend_distrib)

lemma lconcat_lappend [simp]:
  assumes "lfinite xss"
  shows "lconcat (lappend xss yss) = lappend (lconcat xss) (lconcat yss)"
using assms
by induct (simp_all add: lappend_assoc)

lemma lconcat_eq_LCons_conv:
  "lconcat xss = LCons x xs ⟷
  (∃xs' xss' xss''. xss = lappend (llist_of xss') (LCons (LCons x xs') xss'') ∧
                    xs = lappend xs' (lconcat xss'') ∧ set xss' ⊆ {xs. lnull xs})"
  (is "?lhs ⟷ ?rhs")
proof
  assume "?rhs"
  then obtain xs' xss' xss''
    where "xss = lappend (llist_of xss') (LCons (LCons x xs') xss'')"
    and "xs = lappend xs' (lconcat xss'')"
    and "set xss' ⊆ {xs. lnull xs}" by blast
  moreover from ‹set xss' ⊆ {xs. lnull xs}›
  have "lnull (lconcat (llist_of xss'))" by simp
  ultimately show ?lhs by(simp add: lappend_lnull1)
next
  assume "?lhs"
  hence "¬ lnull (lconcat xss)" by simp
  hence "¬ lset xss ⊆ {xs. lnull xs}" by simp
  hence "¬ lnull (lfilter (λxs. ¬ lnull xs) xss)" by(auto)
  then obtain y ys where yys: "lfilter (λxs. ¬ lnull xs) xss = LCons y ys"
    unfolding not_lnull_conv by auto
  from lfilter_eq_LConsD[OF this]
  obtain us vs where xss: "xss = lappend us (LCons y vs)"
    and "lfinite us"
    and "lset us ⊆ {xs. lnull xs}" "¬ lnull y"
    and ys: "ys = lfilter (λxs. ¬ lnull xs) vs" by blast
  from ‹lfinite us› obtain us' where [simp]: "us = llist_of us'"
    unfolding lfinite_eq_range_llist_of by blast
  from ‹lset us ⊆ {xs. lnull xs}› have us: "lnull (lconcat us)"
    unfolding lnull_lconcat .
  from ‹¬ lnull y› obtain y' ys' where y: "y = LCons y' ys'"
    unfolding not_lnull_conv by blast
  from ‹?lhs› us have [simp]: "y' = x" "xs = lappend ys' (lconcat vs)"
    unfolding xss y by(simp_all add: lappend_lnull1)
  from ‹lset us ⊆ {xs. lnull xs}› ys show ?rhs unfolding xss y by simp blast
qed

lemma llength_lconcat_lfinite_conv_sum:
  assumes "lfinite xss"
  shows "llength (lconcat xss) = (∑i | enat i < llength xss. llength (lnth xss i))"
using assms
proof(induct)
  case lfinite_LNil thus ?case by simp
next
  case (lfinite_LConsI xss xs)
  have "{i. enat i ≤ llength xss} = insert 0 {Suc i|i. enat i < llength xss}"
    by(auto simp add: zero_enat_def[symmetric] Suc_ile_eq gr0_conv_Suc)
  also have "… = insert 0 (Suc ` {i. enat i < llength xss})" by auto
  also have "0 ∉ Suc ` {i. enat i < llength xss}" by auto
  moreover from ‹lfinite xss› have "finite {i. enat i < llength xss}"
    by(rule lfinite_finite_index)
  ultimately show ?case using lfinite_LConsI
    by(simp add: sum.reindex)
qed

lemma lconcat_lfilter_neq_LNil:
  "lconcat (lfilter (λxs. ¬ lnull xs) xss) = lconcat xss"
by(induct xss)(simp_all add: lappend_lnull1)

lemmas lconcat_fixp_parallel_induct =
  parallel_fixp_induct_1_1[OF llist_partial_function_definitions llist_partial_function_definitions
    lconcat.mono lconcat.mono lconcat_def lconcat_def, case_names adm LNil step]

lemma llist_all2_lconcatI:
  "llist_all2 (llist_all2 A) xss yss
  ⟹ llist_all2 A (lconcat xss) (lconcat yss)"
by(induct arbitrary: xss yss rule: lconcat_fixp_parallel_induct)(auto split: llist.split intro: llist_all2_lappendI)

lemma llength_lconcat_eqI:
  fixes xss :: "'a llist llist" and yss :: "'b llist llist"
  assumes "llist_all2 (λxs ys. llength xs = llength ys) xss yss"
  shows "llength (lconcat xss) = llength (lconcat yss)"
apply(rule llist_all2_llengthD[where P="λ_ _. True"])
apply(rule llist_all2_lconcatI)
apply(simp add: llist_all2_True[abs_def] assms)
done

lemma lset_lconcat_lfinite:
  "∀xs ∈ lset xss. lfinite xs ⟹ lset (lconcat xss) = (⋃xs∈lset xss. lset xs)"
by(induction xss) auto

lemma lconcat_ltake:
  "lconcat (ltake (enat n) xss) = ltake (∑i<n. llength (lnth xss i)) (lconcat xss)"
proof(induct n arbitrary: xss)
  case 0 thus ?case by(simp add: zero_enat_def[symmetric])
next
  case (Suc n)
  show ?case
  proof(cases xss)
    case LNil thus ?thesis by simp
  next
    case (LCons xs xss')
    hence "lconcat (ltake (enat (Suc n)) xss) = lappend xs (lconcat (ltake (enat n) xss'))"
      by(simp add: eSuc_enat[symmetric])
    also have "lconcat (ltake (enat n) xss') = ltake (∑i<n. llength (lnth xss' i)) (lconcat xss')" by(rule Suc)
    also have "lappend xs … = ltake (llength xs + (∑i<n. llength (lnth xss' i))) (lappend xs (lconcat xss'))"
      by(cases "llength xs")(simp_all add: ltake_plus_conv_lappend ltake_lappend1 ltake_all ldropn_lappend2 lappend_inf lfinite_conv_llength_enat ldrop_enat)
    also have "(∑i<n. llength (lnth xss' i)) = (∑i=1..<Suc n. llength (lnth xss i))"
      by (rule sum.reindex_cong [symmetric, of Suc])
        (auto simp add: LCons image_iff less_Suc_eq_0_disj)
    also have "llength xs + … = (∑i<Suc n. llength (lnth xss i))"
      unfolding atLeast0LessThan[symmetric] LCons
      by(subst (2) sum.atLeast_Suc_lessThan) simp_all
    finally show ?thesis using LCons by simp
  qed
qed

lemma lnth_lconcat_conv:
  assumes "enat n < llength (lconcat xss)"
  shows "∃m n'. lnth (lconcat xss) n = lnth (lnth xss m) n' ∧ enat n' < llength (lnth xss m) ∧
                enat m < llength xss ∧ enat n = (∑i<m . llength (lnth xss i)) + enat n'"
using assms
proof(induct n arbitrary: xss)
  case 0
  hence "¬ lnull (lconcat xss)" by auto
  then obtain x xs where concat_xss: "lconcat xss = LCons x xs"
    unfolding not_lnull_conv by blast
  then obtain xs' xss' xss''
    where xss: "xss = lappend (llist_of xss') (LCons (LCons x xs') xss'')"
    and xs: "xs = lappend xs' (lconcat xss'')"
    and LNil: "set xss' ⊆ {xs. lnull xs}"
    unfolding lconcat_eq_LCons_conv by blast
  from LNil have "lnull (lconcat (llist_of xss'))" by simp
  moreover have [simp]: "lnth xss (length xss') = LCons x xs'"
    unfolding xss by(simp add: lnth_lappend2)
  ultimately have "lnth (lconcat xss) 0 = lnth (lnth xss (length xss')) 0"
    using concat_xss xss by(simp)
  moreover have "enat 0 < llength (lnth xss (length xss'))"
    by(simp add: zero_enat_def[symmetric])
  moreover have "enat (length xss') < llength xss" unfolding xss
    by simp
  moreover have "(∑i < length xss'. llength (lnth xss i)) = (∑i < length xss'. 0)"
  proof(rule sum.cong)
    show "{..< length xss'} = {..< length xss'}" by simp
  next
    fix i
    assume "i ∈ {..< length xss'}"
    hence "xss' ! i ∈ set xss'" unfolding in_set_conv_nth by blast
    with LNil have "xss' ! i = LNil" by auto
    moreover from ‹i ∈ {..< length xss'}› have "lnth xss i = xss' ! i"
      unfolding xss by(simp add: lnth_lappend1)
    ultimately show "llength (lnth xss i) = 0" by simp
  qed
  hence "enat 0 = (∑i<length xss'. llength (lnth xss i)) + enat 0"
    by(simp add: zero_enat_def[symmetric])
  ultimately show ?case by blast
next
  case (Suc n)
  from ‹enat (Suc n) < llength (lconcat xss)›
  have "¬ lnull (lconcat xss)" by auto
  then obtain x xs where concat_xss: "lconcat xss = LCons x xs"
    unfolding not_lnull_conv by blast
  then obtain xs' xss' xss'' where xss: "xss = lappend (llist_of xss') (LCons (LCons x xs') xss'')"
    and xs: "xs = lappend xs' (lconcat xss'')"
    and LNil: "set xss' ⊆ {xs. lnull xs}"
    unfolding lconcat_eq_LCons_conv by blast
  from LNil have concat_xss': "lnull (lconcat (llist_of xss'))" by simp
  from xs have "xs = lconcat (LCons xs' xss'')" by simp
  with concat_xss ‹enat (Suc n) < llength (lconcat xss)›
  have "enat n < llength (lconcat (LCons xs' xss''))"
    by(simp add: Suc_ile_eq)
  from Suc.hyps[OF this] obtain m n'
    where nth_n: "lnth (lconcat (LCons xs' xss'')) n = lnth (lnth (LCons xs' xss'') m) n'"
    and n': "enat n' < llength (lnth (LCons xs' xss'') m)"
    and m': "enat m < llength (LCons xs' xss'')"
    and n_eq: "enat n = (∑i < m. llength (lnth (LCons xs' xss'') i)) + enat n'"
    by blast
  from n_eq obtain N where N: "(∑i < m. llength (lnth (LCons xs' xss'') i)) = enat N"
    and n: "n = N + n'"
    by(cases "∑i < m. llength (lnth (LCons xs' xss'') i)") simp_all


  { fix i
    assume i: "i < length xss'"
    hence "xss' ! i = LNil" using LNil unfolding set_conv_nth by auto
    hence "lnth xss i = LNil" using i unfolding xss
      by(simp add: lnth_lappend1) }
  note lnth_prefix = this

  show ?case
  proof(cases "m > 0")
    case True
    then obtain m' where [simp]: "m = Suc m'" by(cases m) auto
    have "lnth (lconcat xss) (Suc n) = lnth (lnth xss (m + length xss')) n'"
      using concat_xss' nth_n unfolding xss by(simp add: lnth_lappend2 lappend_lnull1)
    moreover have "enat n' < llength (lnth xss (m + length xss'))"
      using concat_xss' n' unfolding xss by(simp add: lnth_lappend2)
    moreover have "enat (m + length xss') < llength xss"
      using concat_xss' m' unfolding xss
      apply (simp add: Suc_ile_eq)
      apply (simp add: eSuc_enat[symmetric] eSuc_plus_1
        plus_enat_simps(1)[symmetric] del: plus_enat_simps(1))
      done
    moreover have "enat (m + length xss') < llength xss"
      using m' unfolding xss
      apply(simp add: Suc_ile_eq)
      apply (simp add: eSuc_enat[symmetric] eSuc_plus_1
        plus_enat_simps(1)[symmetric] del: plus_enat_simps(1))
      done
    moreover
    { have "(∑i < m + length xss'. llength (lnth xss i)) =
            (∑i < length xss'. llength (lnth xss i)) +
            (∑i = length xss'..<m + length xss'. llength (lnth xss i))"
        by(subst (1 2) atLeast0LessThan[symmetric])(subst sum.atLeastLessThan_concat, simp_all)
      also from lnth_prefix have "(∑i < length xss'. llength (lnth xss i)) = 0" by simp
      also have "{length xss'..<m + length xss'} = {0+length xss'..<m+length xss'}" by auto
      also have "(∑i = 0 + length xss'..<m + length xss'. llength (lnth xss i)) =
                (∑i = 0..<m. llength (lnth xss (i + length xss')))"
        by(rule sum.shift_bounds_nat_ivl)
      also have "… = (∑i = 0..<m. llength (lnth (LCons (LCons x xs') xss'') i))"
        unfolding xss by(subst lnth_lappend2) simp+
      also have "… = eSuc (llength xs') + (∑i = Suc 0..<m. llength (lnth (LCons (LCons x xs') xss'') i))"
        by(subst sum.atLeast_Suc_lessThan) simp_all
      also {
        fix i
        assume "i ∈ {Suc 0..<m}"
        then obtain i' where "i = Suc i'" by(cases i) auto
        hence "llength (lnth (LCons (LCons x xs') xss'') i) = llength (lnth (LCons xs' xss'') i)"
          by simp }
      hence "(∑i = Suc 0..<m. llength (lnth (LCons (LCons x xs') xss'') i)) =
             (∑i = Suc 0..<m. llength (lnth (LCons xs' xss'') i))" by(simp)
      also have "eSuc (llength xs') + … = 1 + (llength (lnth (LCons xs' xss'') 0) + …)"
        by(simp add: eSuc_plus_1 ac_simps)
      also note sum.atLeast_Suc_lessThan[symmetric, OF ‹0 < m›]
      finally have "enat (Suc n) = (∑i<m + length xss'. llength (lnth xss i)) + enat n'"
        unfolding eSuc_enat[symmetric] n_eq by(simp add: eSuc_plus_1 ac_simps atLeast0LessThan) }
    ultimately show ?thesis by blast
  next
    case False
    hence [simp]: "m = 0" by auto
    have "lnth (lconcat xss) (Suc n) = lnth (lnth xss (length xss')) (Suc n')"
      using concat_xss n_eq xs n'
      unfolding xss by(simp add: lnth_lappend1 lnth_lappend2)
    moreover have "enat (Suc n') < llength (lnth xss (length xss'))"
      using concat_xss n' unfolding xss by(simp add: lnth_lappend2 Suc_ile_eq)
    moreover have "enat (length xss') < llength xss" unfolding xss
      by simp
    moreover from lnth_prefix have "(∑i<length xss'. llength (lnth xss i)) = 0" by simp
    hence "enat (Suc n) = (∑i<length xss'. llength (lnth xss i)) + enat (Suc n')"
      using n_eq by simp
    ultimately show ?thesis by blast
  qed
qed

lemma lprefix_lconcatI:
  "xss ⊑ yss ⟹ lconcat xss ⊑ lconcat yss"
by(rule monotoneD[OF monotone_lconcat])

lemma lnth_lconcat_ltake:
  assumes "enat w < llength (lconcat (ltake (enat n) xss))"
  shows "lnth (lconcat (ltake (enat n) xss)) w = lnth (lconcat xss) w"
using assms by(auto intro: lprefix_lnthD lprefix_lconcatI)

lemma lfinite_lconcat [simp]:
  "lfinite (lconcat xss) ⟷ lfinite (lfilter (λxs. ¬ lnull xs) xss) ∧ (∀xs ∈ lset xss. lfinite xs)"
  (is "?lhs ⟷ ?rhs")
proof
  assume "?lhs"
  thus "?rhs" (is "?concl xss")
  proof(induct "lconcat xss" arbitrary: xss)
    case [symmetric]: lfinite_LNil
    moreover hence "lnull (lfilter (λxs. ¬ lnull xs) xss)"
      by(auto simp add: lconcat_eq_LNil)
    ultimately show ?case by(auto)
  next
    case (lfinite_LConsI xs x)
    from ‹LCons x xs = lconcat xss›[symmetric]
    obtain xs' xss' xss'' where xss [simp]: "xss = lappend (llist_of xss') (LCons (LCons x xs') xss'')"
      and xs [simp]: "xs = lappend xs' (lconcat xss'')"
      and xss': "set xss' ⊆ {xs. lnull xs}" unfolding lconcat_eq_LCons_conv by blast
    have "xs = lconcat (LCons xs' xss'')" by simp
    hence "?concl (LCons xs' xss'')" by(rule lfinite_LConsI)
    thus ?case using ‹lfinite xs› xss' by(auto split: if_split_asm)
  qed
next
  assume "?rhs"
  then obtain "lfinite (lfilter (λxs. ¬ lnull xs) xss)"
    and "∀xs∈lset xss. lfinite xs" ..
  thus ?lhs
  proof(induct "lfilter (λxs. ¬ lnull xs) xss" arbitrary: xss)
    case lfinite_LNil
    from ‹LNil = lfilter (λxs. ¬ lnull xs) xss›[symmetric]
    have "lset xss ⊆ {xs. lnull xs}" unfolding lfilter_empty_conv by blast
    hence "lnull (lconcat xss)" by(simp)
    thus ?case by(simp)
  next
    case (lfinite_LConsI xs x)
    from lfilter_eq_LConsD[OF ‹LCons x xs = lfilter (λxs. ¬ lnull xs) xss›[symmetric]]
    obtain xss' xss'' where xss [simp]: "xss = lappend xss' (LCons x xss'')"
      and xss': "lfinite xss'" "lset xss' ⊆ {xs. lnull xs}"
      and x: "¬ lnull x"
      and xs [simp]: "xs = lfilter (λxs. ¬ lnull xs) xss''" by blast
    moreover
    from ‹∀xs∈lset xss. lfinite xs› xss' have "∀xs∈lset xss''. lfinite xs" by auto
    with xs have "lfinite (lconcat xss'')" by(rule lfinite_LConsI)
    ultimately show ?case using ‹∀xs∈lset xss. lfinite xs› by(simp)
  qed
qed

lemma list_of_lconcat:
  assumes "lfinite xss"
  and "∀xs ∈ lset xss. lfinite xs"
  shows "list_of (lconcat xss) = concat (list_of (lmap list_of xss))"
using assms by induct(simp_all add: list_of_lappend)

lemma lfilter_lconcat_lfinite:
  "∀xs∈lset xss. lfinite xs
  ⟹ lfilter P (lconcat xss) = lconcat (lmap (lfilter P) xss)"
by(induct xss) simp_all

lemma lconcat_repeat_LNil [simp]: "lconcat (repeat LNil) = LNil"
by(simp add: lconcat_eq_LNil)

lemma lconcat_lmap_singleton [simp]: "lconcat (lmap (λx. LCons (f x) LNil) xs) = lmap f xs"
by(induct xs) simp_all

lemma lset_lconcat_subset: "lset (lconcat xss) ⊆ (⋃xs∈lset xss. lset xs)"
by(induct xss)(auto dest: subsetD[OF lset_lappend])

lemma ldistinct_lconcat:
  "⟦ ldistinct xss; ⋀ys. ys ∈ lset xss ⟹ ldistinct ys;
     ⋀ys zs. ⟦ ys ∈ lset xss; zs ∈ lset xss; ys ≠ zs ⟧ ⟹ lset ys ∩ lset zs = {} ⟧
  ⟹ ldistinct (lconcat xss)"
apply(induction arbitrary: xss rule: lconcat.fixp_induct)
apply(auto simp add: ldistinct_lappend fun_ord_def split: llist.split)
apply(blast dest!: subsetD[OF lprefix_lsetD] subsetD[OF lset_lconcat_subset])
done

subsection ‹Sublist view of a lazy list: @{term "lnths"}›

lemma lnths_empty [simp]: "lnths xs {} = LNil"
by(auto simp add: lnths_def split_def lfilter_empty_conv)

lemma lzip_LCons_iterates_eq:
  "lzip (LCons x xs) (iterates f y) = LCons (x, y) (lzip xs (iterates f (f y)))"
  by (simp add: iterates [of f y])

lemma lzip_iterates_LCons_eq:
  "lzip (iterates f x) (LCons y ys) = LCons (x, y) (lzip (iterates f (f x)) ys)"
  by (simp add: iterates [of f x])

lemma lnths_LNil [simp]: "lnths LNil A = LNil"
by(simp add: lnths_def)

lemma lnths_LCons:
  "lnths (LCons x xs) A =
  (if 0 ∈ A then LCons x (lnths xs {n. Suc n ∈ A}) else lnths xs {n. Suc n ∈ A})"
proof -
  let ?it = "iterates Suc"
  let ?f = "λ(x, y). (x, Suc y)"
  { fix n
    have "lzip xs (?it (Suc n)) = lmap ?f (lzip xs (?it n))"
      by(coinduction arbitrary: xs n)(auto)
    hence "lmap fst (lfilter (λ(x, y). y ∈ A) (lzip xs (?it (Suc n)))) =
           lmap fst (lfilter (λ(x, y). Suc y ∈ A) (lzip xs (?it n)))"
      by(simp add: lfilter_lmap o_def split_def llist.map_comp) }
  then show ?thesis
    by (auto simp add: lnths_def lzip_LCons_iterates_eq)
qed

lemma lset_lnths:
  "lset (lnths xs I) = {lnth xs i|i. enat i<llength xs ∧ i ∈ I}"
apply(auto simp add: lnths_def lset_lzip)
apply(rule_tac x="(lnth xs i, i)" in image_eqI)
apply auto
done

lemma lset_lnths_subset: "lset (lnths xs I) ⊆ lset xs"
by(auto simp add: lset_lnths in_lset_conv_lnth)

lemma lnths_singleton [simp]:
  "lnths (LCons x LNil) A = (if 0 : A then LCons x LNil else LNil)"
by (simp add: lnths_LCons)

lemma lnths_upt_eq_ltake [simp]:
  "lnths xs {..<n} = ltake (enat n) xs"
apply(rule sym)
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] lnths_LCons lessThan_def)
qed

lemma lnths_llist_of [simp]:
  "lnths (llist_of xs) A = llist_of (nths xs A)"
by(induct xs arbitrary: A)(simp_all add: lnths_LCons nths_Cons)

lemma llength_lnths_ile: "llength (lnths xs A) ≤ llength xs"
proof -
  have "llength (lfilter (λ(x, y). y ∈ A) (lzip xs (iterates Suc 0))) ≤
        llength (lzip xs (iterates Suc 0))"
    by(rule llength_lfilter_ile)
  thus ?thesis by(simp add: lnths_def)
qed

lemma lnths_lmap [simp]:
  "lnths (lmap f xs) A = lmap f (lnths xs A)"
by(simp add: lnths_def lzip_lmap1 llist.map_comp lfilter_lmap o_def split_def)

lemma lfilter_conv_lnths:
  "lfilter P xs = lnths xs {n. enat n < llength xs ∧ P (lnth xs n)}"
proof -
  have "lnths xs {n. enat n < llength xs ∧ P (lnth xs n)} =
        lmap fst (lfilter (λ(x, y). enat y < llength xs ∧ P (lnth xs y))
                          (lzip xs (iterates Suc 0)))"
    by(simp add: lnths_def)
  also have "∀(x, y)∈lset (lzip xs (iterates Suc 0)). enat y < llength xs ∧ x = lnth xs y"
    by(auto simp add: lset_lzip)
  hence "lfilter (λ(x, y). enat y < llength xs ∧ P (lnth xs y)) (lzip xs (iterates Suc 0)) =
         lfilter (P ∘ fst) (lzip xs (iterates Suc 0))"
    by -(rule lfilter_cong[OF refl], auto)
  also have "lmap fst (lfilter (P ∘ fst) (lzip xs (iterates Suc 0))) =
            lfilter P (lmap fst (lzip xs (iterates Suc 0)))"
    unfolding lfilter_lmap ..
  also have "lmap fst (lzip xs (iterates Suc 0)) = xs"
    by(simp add: lmap_fst_lzip_conv_ltake ltake_all)
  finally show ?thesis ..
qed

lemma ltake_iterates_Suc:
  "ltake (enat n) (iterates Suc m) = llist_of [m..<n + m]"
proof(induct n arbitrary: m)
  case 0 thus ?case by(simp add: zero_enat_def[symmetric])
next
  case (Suc n)
  have "ltake (enat (Suc n)) (iterates Suc m) =
        LCons m (ltake (enat n) (iterates Suc (Suc m)))"
    by(subst iterates)(simp add: eSuc_enat[symmetric])
  also note Suc
  also have "LCons m (llist_of [Suc m..<n + Suc m]) = llist_of [m..<Suc n+m]"
    unfolding llist_of.simps[symmetric]
    by(auto simp del: llist_of.simps simp add: upt_conv_Cons)
  finally show ?case .
qed

lemma lnths_lappend_lfinite:
  assumes len: "llength xs = enat k"
  shows "lnths (lappend xs ys) A =
         lappend (lnths xs A) (lnths ys {n. n + k ∈ A})"
proof -
  let ?it = "iterates Suc"
  from assms have fin: "lfinite xs" by(rule llength_eq_enat_lfiniteD)
  have "lnths (lappend xs ys) A =
    lmap fst (lfilter (λ(x, y). y ∈ A) (lzip (lappend xs ys) (?it 0)))"
    by(simp add: lnths_def)
  also have "?it 0 = lappend (ltake (enat k) (?it 0)) (ldrop (enat k) (?it 0))"
    by(simp only: lappend_ltake_ldrop)
  also note lzip_lappend
  also note lfilter_lappend_lfinite
  also note lmap_lappend_distrib
  also have "lzip xs (ltake (enat k) (?it 0)) = lzip xs (?it 0)"
    using len by(subst (1 2) lzip_conv_lzip_ltake_min_llength) simp
  also note lnths_def[symmetric]
  also have "ldrop (enat k) (?it 0) = ?it k"
    by(simp add: ldrop_iterates)
  also { fix n m
    have "?it (n + m) = lmap (λn. n + m) (?it n)"
      by(coinduction arbitrary: n)(force)+ }
  from this[of 0 k] have "?it k = lmap (λn. n + k) (?it 0)" by simp
  also note lzip_lmap2
  also note lfilter_lmap
  also note llist.map_comp
  also have "fst ∘ (λ(x, y). (x, y + k)) = fst"
    by(simp add: o_def split_def)
  also have "(λ(x, y). y ∈ A) ∘ (λ(x, y). (x, y + k)) = (λ(x, y). y ∈ {n. n + k ∈ A})"
    by(simp add: fun_eq_iff)
  also note lnths_def[symmetric]
  finally show ?thesis using len by simp
qed

lemma lnths_split:
  "lnths xs A =
   lappend (lnths (ltake (enat n) xs) A) (lnths (ldropn n xs) {m. n + m ∈ A})"
proof(cases "enat n ≤ llength xs")
  case False thus ?thesis by(auto simp add: ltake_all ldropn_all)
next
  case True
  have "xs = lappend (ltake (enat n) xs) (ldrop (enat n) xs)"
    by(simp only: lappend_ltake_ldrop)
  hence "xs = lappend (ltake (enat n) xs) (ldropn n xs)" by simp
  hence "lnths xs A = lnths (lappend (ltake (enat n) xs) (ldropn n xs)) A"
    by(simp)
  also note lnths_lappend_lfinite[where k=n]
  finally show ?thesis using True by(simp add: min_def ac_simps)
qed

lemma lnths_cong:
  assumes "xs = ys" and A: "⋀n. enat n < llength ys ⟹ n ∈ A ⟷ n ∈ B"
  shows "lnths xs A = lnths ys B"
proof -
  have "lfilter (λ(x, y). y ∈ A) (lzip ys (iterates Suc 0)) =
        lfilter (λ(x, y). y ∈ B) (lzip ys (iterates Suc 0))"
    by(rule lfilter_cong[OF refl])(auto simp add: lset_lzip A)
  thus ?thesis unfolding ‹xs = ys› lnths_def by simp
qed

lemma lnths_insert:
  assumes n: "enat n < llength xs"
  shows "lnths xs (insert n A) =
         lappend (lnths (ltake (enat n) xs) A) (LCons (lnth xs n)
                 (lnths (ldropn (Suc n) xs) {m. Suc (n + m) ∈ A}))"
proof -
  have "lnths xs (insert n A) =
        lappend (lnths (ltake (enat n) xs) (insert n A))
                (lnths (ldropn n xs) {m. n + m ∈ (insert n A)})"
    by(rule lnths_split)
  also have "lnths (ltake (enat n) xs) (insert n A) =
            lnths (ltake (enat n) xs) A"
    by(rule lnths_cong[OF refl]) simp
  also { from n obtain X XS where "ldropn n xs = LCons X XS"
      by(cases "ldropn n xs")(auto simp add: ldropn_eq_LNil)
    moreover have "lnth (ldropn n xs) 0 = lnth xs n"
      using n by(simp)
    moreover have "ltl (ldropn n xs) = ldropn (Suc n) xs"
      by(cases xs)(simp_all add: ltl_ldropn)
    ultimately have "ldropn n xs = LCons (lnth xs n) (ldropn (Suc n) xs)" by simp
    hence "lnths (ldropn n xs) {m. n + m ∈ insert n A} =
           LCons (lnth xs n) (lnths (ldropn (Suc n) xs) {m. Suc (n + m) ∈ A})"
      by(simp add: lnths_LCons) }
  finally show ?thesis .
qed

lemma lfinite_lnths [simp]:
  "lfinite (lnths xs A) ⟷ lfinite xs ∨ finite A"
proof
  assume "lfinite (lnths xs A)"
  hence "lfinite xs ∨
         finite {n. enat n < llength xs ∧ (λ(x, y). y ∈ A) (lnth (lzip xs (iterates Suc 0)) n)}"
    by(simp add: lnths_def lfinite_lfilter)
  also have "{n. enat n < llength xs ∧ (λ(x, y). y ∈ A) (lnth (lzip xs (iterates Suc 0)) n)} =
            {n. enat n < llength xs ∧ n ∈ A}" by(auto simp add: lnth_lzip)
  finally show "lfinite xs ∨ finite A"
    by(auto simp add: not_lfinite_llength elim: contrapos_np)
next
  assume "lfinite xs ∨ finite A"
  moreover
  have "{n. enat n < llength xs ∧ (λ(x, y). y ∈ A) (lnth (lzip xs (iterates Suc 0)) n)} =
        {n. enat n < llength xs ∧ n ∈ A}" by(auto simp add: lnth_lzip)
  ultimately show "lfinite (lnths xs A)"
    by(auto simp add: lnths_def lfinite_lfilter)
qed

subsection ‹@{const "lsum_list"}›

context monoid_add begin

lemma lsum_list_0 [simp]: "lsum_list (lmap (λ_. 0) xs) = 0"
by(simp add: lsum_list_def)

lemma lsum_list_llist_of [simp]: "lsum_list (llist_of xs) = sum_list xs"
by(simp add: lsum_list_def)

lemma lsum_list_lappend: "⟦ lfinite xs; lfinite ys ⟧ ⟹ lsum_list (lappend xs ys) = lsum_list xs + lsum_list ys"
by(simp add: lsum_list_def list_of_lappend)

lemma lsum_list_LNil [simp]: "lsum_list LNil = 0"
by(simp add: lsum_list_def)

lemma lsum_list_LCons [simp]: "lfinite xs ⟹ lsum_list (LCons x xs) = x + lsum_list xs"
by(simp add: lsum_list_def)

lemma lsum_list_inf [simp]: "¬ lfinite xs ⟹ lsum_list xs = 0"
by(simp add: lsum_list_def)

end

lemma lsum_list_mono:
  fixes f :: "'a ⇒ 'b :: {monoid_add, ordered_ab_semigroup_add}"
  assumes "⋀x. x ∈ lset xs ⟹ f x ≤ g x"
  shows "lsum_list (lmap f xs) ≤ lsum_list (lmap g xs)"
using assms
by(auto simp add: lsum_list_def intro: sum_list_mono)

subsection ‹
  Alternative view on @{typ "'a llist"} as datatype
  with constructors @{term "llist_of"} and @{term "inf_llist"}
›

lemma lnull_inf_llist [simp]: "¬ lnull (inf_llist f)"
by(simp add: inf_llist_def)

lemma inf_llist_neq_LNil: "inf_llist f ≠ LNil"
using lnull_inf_llist unfolding lnull_def .

lemmas LNil_neq_inf_llist = inf_llist_neq_LNil[symmetric]

lemma lhd_inf_llist [simp]: "lhd (inf_llist f) = f 0"
by(simp add: inf_llist_def)

lemma ltl_inf_llist [simp]: "ltl (inf_llist f) = inf_llist (λn. f (Suc n))"

by(simp add: inf_llist_def lmap_iterates[symmetric] llist.map_comp)

lemma inf_llist_rec [code, nitpick_simp]:
  "inf_llist f = LCons (f 0) (inf_llist (λn. f (Suc n)))"
by(rule llist.expand) simp_all

lemma lfinite_inf_llist [iff]: "¬ lfinite (inf_llist f)"
by(simp add: inf_llist_def)

lemma iterates_conv_inf_llist:
  "iterates f a = inf_llist (λn. (f ^^ n) a)"
by(coinduction arbitrary: a)(auto simp add: funpow_swap1)

lemma inf_llist_neq_llist_of [simp]:
  "llist_of xs ≠ inf_llist f"
   "inf_llist f ≠ llist_of xs"
using lfinite_llist_of[of xs] lfinite_inf_llist[of f] by fastforce+

lemma lnth_inf_llist [simp]: "lnth (inf_llist f) n = f n"
proof(induct n arbitrary: f)
  case 0 thus ?case by(subst inf_llist_rec) simp
next
  case (Suc n)
  from Suc[of "λn. f (Suc n)"] show ?case
    by(subst inf_llist_rec) simp
qed

lemma inf_llist_lprefix [simp]: "inf_llist f ⊑ xs ⟷ xs = inf_llist f"
by(auto simp add: not_lfinite_lprefix_conv_eq)

lemma llength_inf_llist [simp]: "llength (inf_llist f) = ∞"
by(simp add: inf_llist_def)

lemma lset_inf_llist [simp]: "lset (inf_llist f) = range f"
by(auto simp add: lset_conv_lnth)

lemma inf_llist_inj [simp]:
  "inf_llist f = inf_llist g ⟷ f = g"
unfolding inf_llist_def lmap_eq_lmap_conv_llist_all2
by(simp add: iterates_conv_inf_llist fun_eq_iff)

lemma inf_llist_lnth [simp]: "¬ lfinite xs ⟹ inf_llist (lnth xs) = xs"
by(coinduction arbitrary: xs)(auto simp add: lnth_0_conv_lhd fun_eq_iff lnth_ltl)

lemma llist_exhaust:
  obtains (llist_of) ys where "xs = llist_of ys"
       | (inf_llist) f where "xs = inf_llist f"
proof(cases "lfinite xs")
  case True
  then obtain ys where "xs = llist_of ys"
    unfolding lfinite_eq_range_llist_of by auto
  thus ?thesis by(rule that)
next
  case False
  hence "xs = inf_llist (lnth xs)" by simp
  thus thesis by(rule that)
qed

lemma lappend_inf_llist [simp]: "lappend (inf_llist f) xs = inf_llist f"
by(simp add: lappend_inf)

lemma lmap_inf_llist [simp]:
  "lmap f (inf_llist g) = inf_llist (f o g)"
by(simp add: inf_llist_def llist.map_comp)

lemma ltake_enat_inf_llist [simp]:
  "ltake (enat n) (inf_llist f) = llist_of (map f [0..<n])"
by(simp add: inf_llist_def ltake_iterates_Suc)

lemma ldropn_inf_llist [simp]:
  "ldropn n (inf_llist f) = inf_llist (λm. f (m + n))"
unfolding inf_llist_def ldropn_lmap ldropn_iterates
by(simp add: iterates_conv_inf_llist o_def)

lemma ldrop_enat_inf_llist:
  "ldrop (enat n) (inf_llist f) = inf_llist (λm. f (m + n))"
proof(induct n arbitrary: f)
  case Suc thus ?case by(subst inf_llist_rec)(simp add: eSuc_enat[symmetric])
qed(simp add: zero_enat_def[symmetric])

lemma lzip_inf_llist_inf_llist [simp]:
  "lzip (inf_llist f) (inf_llist g) = inf_llist (λn. (f n, g n))"
by(coinduction arbitrary: f g) auto

lemma lzip_llist_of_inf_llist [simp]:
  "lzip (llist_of xs) (inf_llist f) = llist_of (zip xs (map f [0..<length xs]))"
proof(induct xs arbitrary: f)
  case Nil thus ?case by simp
next
  case (Cons x xs)
  have "map f [0..<length (x # xs)] = f 0 # map (λn. f (Suc n)) [0..<length xs]"
    by(simp add: upt_conv_Cons map_Suc_upt[symmetric] del: upt_Suc)
  with Cons[of "λn. f (Suc n)"]
  show ?case by(subst inf_llist_rec)(simp)
qed

lemma lzip_inf_llist_llist_of [simp]:
  "lzip (inf_llist f) (llist_of xs) = llist_of (zip (map f [0..<length xs]) xs)"
proof(induct xs arbitrary: f)
  case Nil thus ?case by simp
next
  case (Cons x xs)
  have "map f [0..<length (x # xs)] = f 0 # map (λn. f (Suc n)) [0..<length xs]"
    by(simp add: upt_conv_Cons map_Suc_upt[symmetric] del: upt_Suc)
  with Cons[of "λn. f (Suc n)"]
  show ?case by(subst inf_llist_rec)(simp)
qed

lemma llist_all2_inf_llist [simp]:
  "llist_all2 P (inf_llist f) (inf_llist g) ⟷ (∀n. P (f n) (g n))"
by(simp add: llist_all2_conv_lzip)

lemma llist_all2_llist_of_inf_llist [simp]:
  "¬ llist_all2 P (llist_of xs) (inf_llist f)"
by(simp add: llist_all2_conv_lzip)

lemma llist_all2_inf_llist_llist_of [simp]:
  "¬ llist_all2 P (inf_llist f) (llist_of xs)"
by(simp add: llist_all2_conv_lzip)

lemma (in monoid_add) lsum_list_infllist: "lsum_list (inf_llist f) = 0"
by simp

subsection ‹Setup for lifting and transfer›

subsubsection ‹Relator and predicator properties›

abbreviation "llist_all == pred_llist"

subsubsection ‹Transfer rules for the Transfer package›

context includes lifting_syntax
begin

lemma set1_pre_llist_transfer [transfer_rule]:
  "(rel_pre_llist A B ===> rel_set A) set1_pre_llist set1_pre_llist"
by(auto simp add: rel_pre_llist_def vimage2p_def rel_fun_def set1_pre_llist_def rel_set_def collect_def sum_set_defs prod_set_defs elim: rel_sum.cases split: sum.split_asm)

lemma set2_pre_llist_transfer [transfer_rule]:
  "(rel_pre_llist A B ===> rel_set B) set2_pre_llist set2_pre_llist"
by(auto simp add: rel_pre_llist_def vimage2p_def rel_fun_def set2_pre_llist_def rel_set_def collect_def sum_set_defs prod_set_defs elim: rel_sum.cases split: sum.split_asm)

lemma LNil_transfer [transfer_rule]: "llist_all2 P LNil LNil"
by simp

lemma LCons_transfer [transfer_rule]:
  "(A ===> llist_all2 A ===> llist_all2 A) LCons LCons"
unfolding rel_fun_def by simp

lemma case_llist_transfer [transfer_rule]:
  "(B ===> (A ===> llist_all2 A ===> B) ===> llist_all2 A ===> B)
    case_llist case_llist"
unfolding rel_fun_def by (simp split: llist.split)

lemma unfold_llist_transfer [transfer_rule]:
  "((A ===> (=)) ===> (A ===> B) ===> (A ===> A) ===> A ===> llist_all2 B) unfold_llist unfold_llist"
proof(rule rel_funI)+
  fix IS_LNIL1 :: "'a ⇒ bool" and IS_LNIL2 LHD1 LHD2 LTL1 LTL2 x y
  assume rel: "(A ===> (=)) IS_LNIL1 IS_LNIL2" "(A ===> B) LHD1 LHD2" "(A ===> A) LTL1 LTL2"
    and "A x y"
  from ‹A x y›
  show "llist_all2 B (unfold_llist IS_LNIL1 LHD1 LTL1 x) (unfold_llist IS_LNIL2 LHD2 LTL2 y)"
    apply(coinduction arbitrary: x y)
    using rel by(auto 4 4 elim: rel_funE)
qed

lemma llist_corec_transfer [transfer_rule]:
  "((A ===> (=)) ===> (A ===> B) ===> (A ===> (=)) ===> (A ===> llist_all2 B) ===> (A ===> A) ===> A ===> llist_all2 B) corec_llist corec_llist"
proof(rule rel_funI)+
  fix IS_LNIL1 :: "'a ⇒ bool" and IS_LNIL2 LHD1 LHD2
    and STOP1 :: "'a ⇒ bool" and STOP2 MORE1 MORE2 LTL1 LTL2 x y
  assume [transfer_rule]: "(A ===> (=)) IS_LNIL1 IS_LNIL2 " "(A ===> B) LHD1 LHD2"
    "(A ===> (=)) STOP1 STOP2" "(A ===> llist_all2 B) MORE1 MORE2" "(A ===> A) LTL1 LTL2"
  assume "A x y"
  thus "llist_all2 B (corec_llist IS_LNIL1 LHD1 STOP1 MORE1 LTL1 x) (corec_llist IS_LNIL2 LHD2 STOP2 MORE2 LTL2 y)"
  proof(coinduction arbitrary: x y)
    case [transfer_rule]: (LNil x y)
    show ?case by simp transfer_prover
  next
    case (LCons x y)
    note [transfer_rule] = ‹A x y›
    have ?lhd by(simp add: LCons[simplified]) transfer_prover
    moreover
    have "STOP1 x = STOP2 y" "llist_all2 B (MORE1 x) (MORE2 y)" "A (LTL1 x) (LTL2 y)" by transfer_prover+
    hence ?ltl by(auto simp add: LCons[simplified])
    ultimately show ?case ..
  qed
qed

lemma ltl_transfer [transfer_rule]:
  "(llist_all2 A ===> llist_all2 A) ltl ltl"
  unfolding ltl_def[abs_def] by transfer_prover

lemma lset_transfer [transfer_rule]:
  "(llist_all2 A ===> rel_set A) lset lset"
by (intro rel_funI rel_setI) (auto simp only: in_lset_conv_lnth llist_all2_conv_all_lnth Bex_def)

lemma lmap_transfer [transfer_rule]:
  "((A ===> B) ===> llist_all2 A ===> llist_all2 B) lmap lmap"
by(auto simp add: rel_fun_def llist_all2_lmap1 llist_all2_lmap2 elim: llist_all2_mono)

lemma lappend_transfer [transfer_rule]:
  "(llist_all2 A ===> llist_all2 A ===> llist_all2 A) lappend lappend"
by(auto simp add: rel_fun_def intro: llist_all2_lappendI)

lemma iterates_transfer [transfer_rule]:
  "((A ===> A) ===> A ===> llist_all2 A) iterates iterates"
unfolding iterates_def split_def corec_llist_never_stop by transfer_prover

lemma lfinite_transfer [transfer_rule]:
  "(llist_all2 A ===> (=)) lfinite lfinite"
by(auto dest: llist_all2_lfiniteD)

lemma llist_of_transfer [transfer_rule]:
  "(list_all2 A ===> llist_all2 A) llist_of llist_of"
unfolding llist_of_def by transfer_prover

lemma llength_transfer [transfer_rule]:
  "(llist_all2 A ===> (=)) llength llength"
by(auto dest: llist_all2_llengthD)

lemma ltake_transfer [transfer_rule]:
  "((=) ===> llist_all2 A ===> llist_all2 A) ltake ltake"
by(auto intro: llist_all2_ltakeI)

lemma ldropn_transfer [transfer_rule]:
  "((=) ===> llist_all2 A ===> llist_all2 A) ldropn ldropn"
unfolding ldropn_def[abs_def] by transfer_prover

lemma ldrop_transfer [transfer_rule]:
  "((=) ===> llist_all2 A ===> llist_all2 A) ldrop ldrop"
by(auto intro: llist_all2_ldropI)

lemma ltakeWhile_transfer [transfer_rule]:
  "((A ===> (=)) ===> llist_all2 A ===> llist_all2 A) ltakeWhile ltakeWhile"
proof(rule rel_funI)+
  fix P :: "'a ⇒ bool" and Q :: "'b ⇒ bool" and xs :: "'a llist" and ys :: "'b llist"
  assume PQ: "(A ===> (=)) P Q"
  assume "llist_all2 A xs ys"
  thus "llist_all2 A (ltakeWhile P xs) (ltakeWhile Q ys)"
    apply(coinduction arbitrary: xs ys)
    using PQ by(auto 4 4 elim: rel_funE simp add: not_lnull_conv llist_all2_LCons2 llist_all2_LCons1)
qed

lemma ldropWhile_transfer [transfer_rule]:
  "((A ===> (=)) ===> llist_all2 A ===> llist_all2 A) ldropWhile ldropWhile"
unfolding ldropWhile_eq_ldrop[abs_def] by transfer_prover

lemma lzip_ltransfer [transfer_rule]:
  "(llist_all2 A ===> llist_all2 B ===> llist_all2 (rel_prod A B)) lzip lzip"
by(auto intro: llist_all2_lzipI)

lemma inf_llist_transfer [transfer_rule]:
  "(((=) ===> A) ===> llist_all2 A) inf_llist inf_llist"
unfolding inf_llist_def[abs_def] by transfer_prover

lemma lfilter_transfer [transfer_rule]:
  "((A ===> (=)) ===> llist_all2 A ===> llist_all2 A) lfilter lfilter"
by(auto simp add: rel_fun_def intro: llist_all2_lfilterI)

lemma lconcat_transfer [transfer_rule]:
  "(llist_all2 (llist_all2 A) ===> llist_all2 A) lconcat lconcat"
by(auto intro: llist_all2_lconcatI)

lemma lnths_transfer [transfer_rule]:
  "(llist_all2 A ===> (=) ===> llist_all2 A) lnths lnths"
unfolding lnths_def[abs_def] by transfer_prover

lemma llist_all_transfer [transfer_rule]:
  "((A ===> (=)) ===> llist_all2 A ===> (=)) llist_all llist_all"
unfolding pred_llist_def[abs_def] by transfer_prover

lemma llist_all2_rsp:
  assumes r: "∀x y. R x y ⟶ (∀a b. R a b ⟶ S x a = T y b)"
  and l1: "llist_all2 R x y"
  and l2: "llist_all2 R a b"
  shows "llist_all2 S x a = llist_all2 T y b"
proof(cases "llength x = llength a")
  case True
  thus ?thesis using l1 l2
    by(simp add: llist_all2_conv_all_lnth)(blast dest: r[rule_format])
next
  case False
  with llist_all2_llengthD[OF l1] llist_all2_llengthD[OF l2]
  show ?thesis by(simp add: llist_all2_conv_all_lnth)
qed

lemma llist_all2_transfer [transfer_rule]:
  "((R ===> R ===> (=)) ===> llist_all2 R ===> llist_all2 R ===> (=)) llist_all2 llist_all2"
by (simp add: llist_all2_rsp rel_fun_def)

end

no_notation lprefix (infix ‹⊑› 65)

end