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 [simp]:
  "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 (