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

lemma lhd_lSup [simp]: "xA. ¬ 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 "xsA. 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  (xY. ¬ 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  {}" "ysY. ¬ 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