Theory Coinductive_Nat

(*  Title:       Coinductive natural numbers
Author:      Andreas Lochbihler
Maintainer:  Andreas Lochbihler
*)

section ‹Extended natural numbers as a codatatype›

theory Coinductive_Nat imports
"HOL-Library.Extended_Nat"
"HOL-Library.Complete_Partial_Order2"
begin

lemma inj_enat [simp]: "inj_on enat A"

lemma Sup_range_enat [simp]: "Sup (range enat) = ∞"
by(auto dest: finite_imageD simp add: Sup_enat_def)

fixes a b :: enat shows "a ≠ ∞ ⟹ a + b - a = b"
by(cases b) auto

lemma enat_the_enat: "n ≠ ∞ ⟹ enat (the_enat n) = n"
by auto

lemma enat_min_eq_0_iff:
fixes a b :: enat
shows "min a b = 0 ⟷ a = 0 ∨ b = 0"

lemma enat_le_plus_same: "x ≤ (x :: enat) + y" "x ≤ y + x"
by(auto simp add: less_eq_enat_def plus_enat_def split: enat.split)

lemma the_enat_0 [simp]: "the_enat 0 = 0"

lemma the_enat_eSuc: "n ≠ ∞ ⟹ the_enat (eSuc n) = Suc (the_enat n)"

coinductive_set enat_set :: "enat set"
where "0 ∈ enat_set"
| "n ∈ enat_set ⟹ (eSuc n) ∈ enat_set"

lemma enat_set_eq_UNIV [simp]: "enat_set = UNIV"
proof
show "enat_set ⊆ UNIV" by blast
show "UNIV ⊆ enat_set"
proof
fix x :: enat
assume "x ∈ UNIV"
thus "x ∈ enat_set"
proof coinduct
case (enat_set x)
show ?case
proof(cases "x = 0")
case True thus ?thesis by simp
next
case False
then obtain n where "x = eSuc n"
by(cases x)(fastforce simp add: eSuc_def zero_enat_def gr0_conv_Suc
split: enat.splits)+
thus ?thesis by auto
qed
qed
qed
qed

subsection ‹Case operator›

lemma enat_coexhaust:
obtains (0) "n = 0"
| (eSuc) n' where "n = eSuc n'"
proof -
have "n ∈ enat_set" by auto
thus thesis by cases (erule that)+
qed

locale co begin

free_constructors (plugins del: code) case_enat for
"0::enat"
| eSuc epred
where
"epred 0 = 0"
apply (erule enat_coexhaust, assumption)
apply (rule eSuc_inject)
by (rule zero_ne_eSuc)

end

lemma enat_cocase_0 [simp]: "co.case_enat z s 0 = z"
by (rule co.enat.case(1))

lemma enat_cocase_eSuc [simp]: "co.case_enat z s (eSuc n) = s n"
by (rule co.enat.case(2))

lemma neq_zero_conv_eSuc: "n ≠ 0 ⟷ (∃n'. n = eSuc n')"
by(cases n rule: enat_coexhaust) simp_all

lemma enat_cocase_cert:
assumes "CASE ≡ co.case_enat c d"
shows "(CASE 0 ≡ c) &&& (CASE (eSuc n) ≡ d n)"
using assms by simp_all

lemma enat_cosplit_asm:
"P (co.case_enat c d n) = (¬ (n = 0 ∧ ¬ P c ∨ (∃m. n = eSuc m ∧ ¬ P (d m))))"
by (rule co.enat.split_asm)

lemma enat_cosplit:
"P (co.case_enat c d n) = ((n = 0 ⟶ P c) ∧ (∀m. n = eSuc m ⟶ P (d m)))"
by (rule co.enat.split)

abbreviation epred :: "enat => enat" where "epred ≡ co.epred"

lemma epred_0 [simp]: "epred 0 = 0" by(rule co.enat.sel(1))
lemma epred_eSuc [simp]: "epred (eSuc n) = n" by(rule co.enat.sel(2))
declare co.enat.collapse[simp]
lemma epred_conv_minus: "epred n = n - 1"
by(cases n rule: co.enat.exhaust)(simp_all)

subsection ‹Corecursion for @{typ enat}›

lemma case_enat_numeral [simp]: "case_enat f i (numeral v) = (let n = numeral v in f n)"

lemma case_enat_0 [simp]: "case_enat f i 0 = f 0"

lemma [simp]:
shows max_eSuc_eSuc: "max (eSuc n) (eSuc m) = eSuc (max n m)"
and min_eSuc_eSuc: "min (eSuc n) (eSuc m) = eSuc (min n m)"

definition epred_numeral :: "num ⇒ enat"
where [code del]: "epred_numeral = enat ∘ pred_numeral"

lemma numeral_eq_eSuc: "numeral k = eSuc (epred_numeral k)"
by(simp add: numeral_eq_Suc eSuc_def epred_numeral_def numeral_eq_enat)

lemma epred_numeral_simps [simp]:
"epred_numeral num.One = 0"
"epred_numeral (num.Bit0 k) = numeral (Num.BitM k)"
"epred_numeral (num.Bit1 k) = numeral (num.Bit0 k)"

lemma [simp]:
shows eq_numeral_eSuc: "numeral k = eSuc n ⟷ epred_numeral k = n"
and Suc_eq_numeral: "eSuc n = numeral k ⟷ n = epred_numeral k"
and less_numeral_Suc: "numeral k < eSuc n ⟷ epred_numeral k < n"
and less_eSuc_numeral: "eSuc n < numeral k ⟷ n < epred_numeral k"
and le_numeral_eSuc: "numeral k ≤ eSuc n ⟷ epred_numeral k ≤ n"
and le_eSuc_numeral: "eSuc n ≤ numeral k ⟷ n ≤ epred_numeral k"
and diff_eSuc_numeral: "eSuc n - numeral k = n - epred_numeral k"
and diff_numeral_eSuc: "numeral k - eSuc n = epred_numeral k - n"
and max_eSuc_numeral: "max (eSuc n) (numeral k) = eSuc (max n (epred_numeral k))"
and max_numeral_eSuc: "max (numeral k) (eSuc n) = eSuc (max (epred_numeral k) n)"
and min_eSuc_numeral: "min (eSuc n) (numeral k) = eSuc (min n (epred_numeral k))"
and min_numeral_eSuc: "min (numeral k) (eSuc n) = eSuc (min (epred_numeral k) n)"

lemma enat_cocase_numeral [simp]:
"co.case_enat a f (numeral v) = (let pv = epred_numeral v in f pv)"

"co.case_enat a f ((numeral v) + n) = (let pv = epred_numeral v in f (pv + n))"

lemma [simp]:
shows epred_1: "epred 1 = 0"
and epred_numeral: "epred (numeral i) = epred_numeral i"
and epred_Infty: "epred ∞ = ∞"
and epred_enat: "epred (enat m) = enat (m - 1)"
by(simp_all add: epred_conv_minus one_enat_def zero_enat_def eSuc_def epred_numeral_def numeral_eq_enat split: enat.split)

lemmas epred_simps = epred_0 epred_1 epred_numeral epred_eSuc epred_Infty epred_enat

lemma epred_iadd1: "a ≠ 0 ⟹ epred (a + b) = epred a + b"
apply(cases a b rule: enat.exhaust[case_product enat.exhaust])
apply(simp_all add: epred_conv_minus eSuc_def one_enat_def zero_enat_def split: enat.splits)
done

lemma epred_min [simp]: "epred (min a b) = min (epred a) (epred b)"
by(cases a b rule: enat_coexhaust[case_product enat_coexhaust]) simp_all

lemma epred_le_epredI: "n ≤ m ⟹ epred n ≤ epred m"
by(cases m n rule: enat_coexhaust[case_product enat_coexhaust]) simp_all

lemma epred_minus_epred [simp]:
"m ≠ 0 ⟹ epred n - epred m = n - m"
by(cases n m rule: enat_coexhaust[case_product enat_coexhaust])(simp_all add: epred_conv_minus)

lemma eSuc_epred: "n ≠ 0 ⟹ eSuc (epred n) = n"
by(cases n rule: enat_coexhaust) simp_all

lemma epred_inject: "⟦ x ≠ 0; y ≠ 0 ⟧ ⟹ epred x = epred y ⟷ x = y"
by(cases x y rule: enat.exhaust[case_product enat.exhaust])(auto simp add: zero_enat_def)

lemma monotone_fun_eSuc[partial_function_mono]:
"monotone (fun_ord (λy x. x ≤ y)) (λy x. x ≤ y) (λf. eSuc (f x))"
by (auto simp: monotone_def fun_ord_def)

partial_function (gfp) enat_unfold :: "('a ⇒ bool) ⇒ ('a ⇒ 'a) ⇒ 'a ⇒ enat" where
enat_unfold [code, nitpick_simp]:
"enat_unfold stop next a = (if stop a then 0 else eSuc (enat_unfold stop next (next a)))"

lemma enat_unfold_stop [simp]: "stop a ⟹ enat_unfold stop next a = 0"

lemma enat_unfold_next: "¬ stop a ⟹ enat_unfold stop next a = eSuc (enat_unfold stop next (next a))"

lemma enat_unfold_eq_0 [simp]:
"enat_unfold stop next a = 0 ⟷ stop a"

lemma epred_enat_unfold [simp]:
"epred (enat_unfold stop next a) = (if stop a then 0 else enat_unfold stop next (next a))"

lemma epred_max: "epred (max x y) = max (epred x) (epred y)"
by(cases x y rule: enat.exhaust[case_product enat.exhaust]) simp_all

lemma epred_Max:
assumes "finite A" "A ≠ {}"
shows "epred (Max A) = Max (epred  A)"
using assms
proof induction
case (insert x A)
thus ?case by(cases "A = {}")(simp_all add: epred_max)
qed simp

lemma finite_imageD2: "⟦ finite (f  A); inj_on f (A - B); finite B ⟧ ⟹ finite A"
by (metis Diff_subset finite_Diff2 image_mono inj_on_finite)

lemma epred_Sup: "epred (Sup A) = Sup (epred  A)"
by(auto 4 4 simp add: bot_enat_def Sup_enat_def epred_Max inj_on_def neq_zero_conv_eSuc dest: finite_imageD2[where B="{0}"])

subsection ‹Less as greatest fixpoint›

coinductive_set Le_enat :: "(enat × enat) set"
where
Le_enat_zero: "(0, n) ∈ Le_enat"
| Le_enat_add: "⟦ (m, n) ∈ Le_enat; k ≠ 0 ⟧ ⟹ (eSuc m, n + k) ∈ Le_enat"

lemma ile_into_Le_enat:
"m ≤ n ⟹ (m, n) ∈ Le_enat"
proof -
assume "m ≤ n"
hence "(m, n) ∈ {(m, n)|m n. m ≤ n}" by simp
thus ?thesis
proof coinduct
case (Le_enat m n)
hence "m ≤ n" by simp
show ?case
proof(cases "m = 0")
case True
hence ?Le_enat_zero by simp
thus ?thesis ..
next
case False
with ‹m ≤ n› obtain m' n' where "m = eSuc m'" "n = n' + 1" "m' ≤ n'"
by(cases m rule: enat_coexhaust, simp)
(cases n rule: enat_coexhaust, auto simp add: eSuc_plus_1[symmetric])
thus ?thesis ..
qed
qed
qed

lemma Le_enat_imp_ile_enat_k:
"(m, n) ∈ Le_enat ⟹ n < enat l ⟹ m < enat l"
proof(induct l arbitrary: m n)
case 0
next
case (Suc l)
from ‹(m, n) ∈ Le_enat› show ?case
proof cases
case Le_enat_zero
with ‹n < enat (Suc l)› show ?thesis by auto
next
from ‹n = N + K› ‹n < enat (Suc l)› ‹K ≠ 0›
have "N < enat l" by(cases N)(cases K, auto simp add: zero_enat_def)
with ‹(M, N) ∈ Le_enat› have "M < enat l" by(rule Suc)
with ‹m = eSuc M› show ?thesis by(simp add: eSuc_enat[symmetric])
qed
qed

lemma enat_less_imp_le:
assumes k: "!!k. n < enat k ⟹ m < enat k"
shows "m ≤ n"
proof(cases n)
case (enat n')
with k[of "Suc n'"] show ?thesis by(cases m) simp_all
qed simp

lemma Le_enat_imp_ile:
"(m, n) ∈ Le_enat ⟹ m ≤ n"
by(rule enat_less_imp_le)(erule Le_enat_imp_ile_enat_k)

lemma Le_enat_eq_ile:
"(m, n) ∈ Le_enat ⟷ m ≤ n"
by(blast intro: Le_enat_imp_ile ile_into_Le_enat)

lemma enat_leI [consumes 1, case_names Leenat, case_conclusion Leenat zero eSuc]:
assumes major: "(m, n) ∈ X"
and step:
"⋀m n. (m, n) ∈ X
⟹ m = 0 ∨ (∃m' n' k. m = eSuc m' ∧ n = n' + enat k ∧ k ≠ 0 ∧
((m', n') ∈ X ∨ m' ≤ n'))"
shows "m ≤ n"
apply(rule Le_enat.coinduct[unfolded Le_enat_eq_ile, where X="λx y. (x, y) ∈ X"])
apply(fastforce simp add: zero_enat_def dest: step intro: major)+
done

lemma enat_le_coinduct[consumes 1, case_names le, case_conclusion le 0 eSuc]:
assumes P: "P m n"
and step:
"⋀m n. P m n
⟹ (n = 0 ⟶ m = 0) ∧
(m ≠ 0 ⟶ n ≠ 0 ⟶ (∃k n'. P (epred m) n' ∧ epred n = n' + k) ∨ epred m ≤ epred n)"
shows "m ≤ n"
proof -
from P have "(m, n) ∈ {(m, n). P m n}" by simp
thus ?thesis
proof(coinduct rule: enat_leI)
case (Leenat m n)
hence "P m n" by simp
show ?case
proof(cases m rule: enat_coexhaust)
case 0
thus ?thesis by simp
next
case (eSuc m')
with step[OF ‹P m n›]
have "n ≠ 0" and disj: "(∃k n'. P m' n' ∧ epred n = n' + k) ∨ m' ≤ epred n" by auto
from ‹n ≠ 0› obtain n' where n': "n = eSuc n'"
by(cases n rule: enat_coexhaust) auto
from disj show ?thesis
proof
assume "m' ≤ epred n"
with eSuc n' show ?thesis
by(auto 4 3 intro: exI[where x="Suc 0"] simp add: eSuc_enat[symmetric] iadd_Suc_right zero_enat_def[symmetric])
next
assume "∃k n'. P m' n' ∧ epred n = n' + k"
then obtain k n'' where n'': "epred n = n'' + k" and k: "P m' n''" by blast
show ?thesis using eSuc k n' n''
qed
qed
qed
qed

subsection ‹Equality as greatest fixpoint›

lemma enat_equalityI [consumes 1, case_names Eq_enat,
case_conclusion Eq_enat zero eSuc]:
assumes major: "(m, n) ∈ X"
and step:
"⋀m n. (m, n) ∈ X
⟹ m = 0 ∧ n = 0 ∨ (∃m' n'. m = eSuc m' ∧ n = eSuc n' ∧ ((m', n') ∈ X ∨ m' = n'))"
shows "m = n"
proof(rule antisym)
from major show "m ≤ n"
by(coinduct rule: enat_leI)
(drule step, auto simp add: eSuc_plus_1 enat_1[symmetric])

from major have "(n, m) ∈ {(n, m). (m, n) ∈ X}" by simp
thus "n ≤ m"
proof(coinduct rule: enat_leI)
case (Leenat n m)
hence "(m, n) ∈ X" by simp
from step[OF this] show ?case
qed
qed

lemma enat_coinduct [consumes 1, case_names Eq_enat, case_conclusion Eq_enat zero eSuc]:
assumes major: "P m n"
and step: "⋀m n. P m n
⟹ (m = 0 ⟷ n = 0) ∧
(m ≠ 0 ⟶ n ≠ 0 ⟶ P (epred m) (epred n) ∨ epred m = epred n)"
shows "m = n"
proof -
from major have "(m, n) ∈ {(m, n). P m n}" by simp
thus ?thesis
proof(coinduct rule: enat_equalityI)
case (Eq_enat m n)
hence "P m n" by simp
from step[OF this] show ?case
by(cases m n rule: enat_coexhaust[case_product enat_coexhaust]) auto
qed
qed

lemma enat_coinduct2 [consumes 1, case_names zero eSuc]:
"⟦ P m n; ⋀m n. P m n ⟹ m = 0 ⟷ n = 0;
⋀m n. ⟦ P m n; m ≠ 0; n ≠ 0 ⟧ ⟹ P (epred m) (epred n) ∨ epred m = epred n ⟧
⟹ m = n"
by(erule enat_coinduct) blast

subsection ‹Uniqueness of corecursion›

lemma enat_unfold_unique:
assumes h: "!!x. h x = (if stop x then 0 else eSuc (h (next x)))"
shows "h x = enat_unfold stop next x"
by(coinduction arbitrary: x rule: enat_coinduct)(subst (1 3) h, auto)

subsection ‹Setup for partial\_function›

lemma enat_diff_cancel_left: "⟦ m ≤ x; m ≤ y ⟧ ⟹ x - m = y - m ⟷ x = (y :: enat)"
by(cases x y m rule: enat.exhaust[case_product enat.exhaust[case_product enat.exhaust]])(simp_all, arith)

lemma finite_lessThan_enatI:
assumes "m ≠ ∞"
shows "finite {..<m :: enat}"
proof -
from assms obtain m' where m: "m = enat m'" by auto
have "{..<enat m'} ⊆ enat  {..<m'}"
by(rule subsetI)(case_tac x, auto)
thus ?thesis unfolding m by(rule finite_subset) simp
qed

lemma infinite_lessThan_infty: "¬ finite {..<∞ :: enat}"
proof
have "range enat ⊆ {..<∞}" by auto
moreover assume "finite {..<∞ :: enat}"
ultimately have "finite (range enat)" by(rule finite_subset)
hence "finite (UNIV :: nat set)"
thus False by simp
qed

lemma finite_lessThan_enat_iff:
"finite {..<m :: enat} ⟷ m ≠ ∞"
by(cases m)(auto intro: finite_lessThan_enatI simp add: infinite_lessThan_infty)

lemma enat_minus_mono1: "x ≤ y ⟹ x - m ≤ y - (m :: enat)"
by(cases m x y rule: enat.exhaust[case_product enat.exhaust[case_product enat.exhaust]]) simp_all

lemma max_enat_minus1: "max n m - k = max (n - k) (m - k :: enat)"
by(cases n m k rule: enat.exhaust[case_product enat.exhaust[case_product enat.exhaust]]) simp_all

lemma Max_enat_minus1:
assumes "finite A" "A ≠ {}"
shows "Max A - m = Max ((λn :: enat. n - m)  A)"
using assms proof induct
case (insert x A)
thus ?case by(cases "A = {}")(simp_all add: max_enat_minus1)
qed simp

lemma Sup_enat_minus1:
assumes "m ≠ ∞"
shows "⨆A - m = ⨆((λn :: enat. n - m)  A)"
proof -
from assms obtain m' where "m = enat m'" by auto
thus ?thesis
by(auto simp add: Sup_enat_def Max_enat_minus1 finite_lessThan_enat_iff enat_diff_cancel_left inj_on_def dest!: finite_imageD2[where B="{..<enat m'}"])
qed

assumes "Y ≠ {}"
shows "Sup ((λy :: enat. y+x)  Y) = Sup Y + x"
proof(cases "finite Y")
case True
next
case False
thus ?thesis
proof(cases x)
case (enat x')
hence "¬ finite ((λy. y+x)  Y)" using False
by(auto dest!: finite_imageD intro: inj_onI)
with False show ?thesis by(simp add: Sup_enat_def assms)
next
case infinity
hence "(+) x  Y = {∞}" using assms by auto
thus ?thesis using infinity by(simp add: image_constant_conv assms)
qed
qed

"Y ≠ {} ⟹ Sup ((λy :: enat. x + y)  Y) = x + Sup Y"

lemma mono2mono_eSuc [THEN lfp.mono2mono, cont_intro, simp]:
shows monotone_eSuc: "monotone (≤) (≤) eSuc"
by(rule monotoneI) simp

lemma mcont2mcont_eSuc [THEN lfp.mcont2mcont, cont_intro, simp]:
shows mcont_eSuc: "mcont Sup (≤) Sup (≤) eSuc"
by(intro mcontI contI)(simp_all add: monotone_eSuc eSuc_Sup)

lemma mono2mono_epred [THEN lfp.mono2mono, cont_intro, simp]:
shows monotone_epred: "monotone (≤) (≤) epred"

lemma mcont2mcont_epred [THEN lfp.mcont2mcont, cont_intro, simp]:
shows mcont_epred: "mcont Sup (≤) Sup (≤) epred"
by(simp add: mcont_def monotone_epred cont_def epred_Sup)

lemma enat_cocase_mono [partial_function_mono, cont_intro]:
"⟦ monotone orda ordb zero; ⋀n. monotone orda ordb (λf. esuc f n) ⟧
⟹ monotone orda ordb (λf. co.case_enat (zero f) (esuc f) x)"
by(cases x rule: co.enat.exhaust) simp_all

lemma enat_cocase_mcont [cont_intro, simp]:
"⟦ mcont luba orda lubb ordb zero; ⋀n. mcont luba orda lubb ordb (λf. esuc f n) ⟧
⟹ mcont luba orda lubb ordb (λf. co.case_enat (zero f) (esuc f) x)"
by(cases x rule: co.enat.exhaust) simp_all

lemma eSuc_mono [partial_function_mono]:
"monotone (fun_ord (≤)) (≤) f ⟹ monotone (fun_ord (≤)) (≤) (λx. eSuc (f x))"
by(rule mono2mono_eSuc)

lemma mono2mono_enat_minus1 [THEN lfp.mono2mono, cont_intro, simp]:
shows monotone_enat_minus1: "monotone (≤) (≤) (λn. n - m :: enat)"
by(rule monotoneI)(rule enat_minus_mono1)

lemma mcont2mcont_enat_minus [THEN lfp.mcont2mcont, cont_intro, simp]:
shows mcont_enat_minus: "m ≠ ∞ ⟹ mcont Sup (≤) Sup (≤) (λn. n - m :: enat)"
by(rule mcontI)(simp_all add: monotone_enat_minus1 contI Sup_enat_minus1)

lemma monotone_eadd1: "monotone (≤) (≤) (λx. x + y :: enat)"
by(auto intro!: monotoneI)

lemma monotone_eadd2: "monotone (≤) (≤) (λy. x + y :: enat)"
by(auto intro!: monotoneI)

shows monotone_eadd: "monotone (rel_prod (≤) (≤)) (≤) (λ(x, y). x + y :: enat)"

lemma mcont_eadd2: "mcont Sup (≤) Sup (≤) (λy. x + y :: enat)"

lemma mcont_eadd1: "mcont Sup (≤) Sup (≤) (λx. x + y :: enat)"

"⟦ mcont lub ord Sup (≤) (λx. f x);
mcont lub ord Sup (≤) (λx. g x) ⟧
⟹ mcont lub ord Sup (≤) (λx. f x + g x :: enat)"

"⟦ monotone (fun_ord (≤)) (≤) f; monotone (fun_ord (≤)) (≤) g ⟧
⟹ monotone (fun_ord (≤)) (≤) (λx. f x + g x :: enat)"

lemma monotone_max_enat1: "monotone (≤) (≤) (λx. max x y :: enat)"
by(auto intro!: monotoneI simp add: max_def)

lemma monotone_max_enat2: "monotone (≤) (≤) (λy. max x y :: enat)"
by(auto intro!: monotoneI simp add: max_def)

lemma mono2mono_max_enat[THEN lfp.mono2mono2, cont_intro, simp]:
shows monotone_max_enat: "monotone (rel_prod (≤) (≤)) (≤) (λ(x, y). max x y :: enat)"

lemma max_Sup_enat2:
assumes "Y ≠ {}"
shows "max x (Sup Y) = Sup ((λy :: enat. max x y)  Y)"
proof(cases "finite Y")
case True
hence "max x (Max Y) = Max (max x  Y)" using assms
proof(induct)
case (insert y Y)
thus ?case
by(cases "Y = {}")(simp_all, metis max.assoc max.left_commute max.left_idem)
qed simp
thus ?thesis using True by(simp add: Sup_enat_def assms)
next
case False
show ?thesis
proof(cases x)
case infinity
hence "max x  Y = {∞}" using assms by auto
thus ?thesis using False by(simp add: Sup_enat_def assms)
next
case (enat x')
{ assume "finite (max x  Y)"
hence "finite (max x  {y ∈ Y. y > x})"
by(rule finite_subset[rotated]) auto
hence "finite {y ∈ Y. y > x}"
by(rule finite_imageD)(auto intro!: inj_onI simp add: max_def split: if_split_asm)
moreover have "finite {y ∈ Y. y ≤ x}"
ultimately have "finite ({y ∈ Y. y > x} ∪ {y ∈ Y. y ≤ x})" by simp
also have "{y ∈ Y. y > x} ∪ {y ∈ Y. y ≤ x} = Y" by auto
finally have "finite Y" . }
thus ?thesis using False by(auto simp add: Sup_enat_def assms)
qed
qed

lemma max_Sup_enat1:
"Y ≠ {} ⟹ max (Sup Y) x = Sup ((λy :: enat. max y x)  Y)"
by(subst (1 2) max.commute)(rule max_Sup_enat2)

lemma mcont_max_enat1: "mcont Sup (≤) Sup (≤) (λx. max x y :: enat)"
by(auto intro!: mcontI contI max_Sup_enat1 simp add: monotone_max_enat1)

lemma mcont_max_enat2: "mcont Sup (≤) Sup (≤) (λy. max x y :: enat)"
by(auto intro!: mcontI contI max_Sup_enat2 simp add: monotone_max_enat2)

lemma mcont2mcont_max_enat [cont_intro, simp]:
"⟦ mcont lub ord Sup (≤) (λx. f x);
mcont lub ord Sup (≤) (λx. g x) ⟧
⟹ mcont lub ord Sup (≤) (λx. max (f x) (g x) :: enat)"
by(best intro: ccpo.mcont2mcont'[OF complete_lattice_ccpo] mcont_max_enat1 mcont_max_enat2 ccpo.mcont_const[OF complete_lattice_ccpo])

lemma max_enat_partial_function_mono [partial_function_mono]:
"⟦ monotone (fun_ord (≤)) (≤) f; monotone (fun_ord (≤)) (≤) g ⟧
⟹ monotone (fun_ord (≤)) (≤) (λx. max (f x) (g x) :: enat)"
by(rule mono2mono_max_enat)

lemma chain_epredI:
"Complete_Partial_Order.chain (≤) Y
⟹ Complete_Partial_Order.chain (≤) (epred  (Y ∩ {x. x ≠ 0}))"
by(auto intro: chainI dest: chainD)

lemma monotone_enat_le_case:
fixes bot
assumes mono: "monotone (≤) ord (λx. f x (eSuc x))"
and ord: "⋀x. ord bot (f x (eSuc x))"
and bot: "ord bot bot"
shows "monotone (≤) ord (λx. case x of 0 ⇒ bot | eSuc x' ⇒ f x' x)"
proof -
have "monotone (≤) ord (λx. if x ≤ 0 then bot else f (epred x) x)"
proof(rule monotone_if_bot)
fix x y :: enat
assume "x ≤ y" "¬ x ≤ 0"
thus "ord (f (epred x) x) (f (epred y) y)"
by(cases x y rule: co.enat.exhaust[case_product co.enat.exhaust])(auto intro: monotoneD[OF mono])
next
fix x :: enat
assume "¬ x ≤ 0"
thus "ord bot (f (epred x) x)"
by(cases x rule: co.enat.exhaust)(auto intro: ord)
qed(rule bot)
also have "(λx. if x ≤ 0 then bot else f (epred x) x) = (λx. case x of 0 ⇒ bot | eSuc x' ⇒ f x' x)"
by(auto simp add: fun_eq_iff split: co.enat.split)
finally show ?thesis .
qed

lemma mcont_enat_le_case:
fixes bot
assumes ccpo: "class.ccpo lub ord (mk_less ord)"
and mcont: "mcont Sup (≤) lub ord (λx. f x (eSuc x))"
and ord: "⋀x. ord bot (f x (eSuc x))"
shows "mcont Sup (≤) lub ord (λx. case x of 0 ⇒ bot | eSuc x' ⇒ f x' x)"
proof -
from ccpo
have "mcont Sup (≤) lub ord (λx. if x ≤ 0 then bot else f (epred x) x)"
proof(rule mcont_if_bot)
fix x y :: enat
assume "x ≤ y" "¬ x ≤ 0"
thus "ord (f (epred x) x) (f (epred y) y)"
by(cases x y rule: co.enat.exhaust[case_product co.enat.exhaust])(auto intro: mcont_monoD[OF mcont])
next
fix Y :: "enat set"
assume chain: "Complete_Partial_Order.chain (≤) Y"
and Y: "Y ≠ {}" "⋀x. x ∈ Y ⟹ ¬ x ≤ 0"
from Y have Y': "Y ∩ {x. x ≠ 0} ≠ {}" by auto
from Y(2) have eq: "Y = eSuc  (epred  (Y ∩ {x. x ≠ 0}))"
by(fastforce intro: rev_image_eqI)
let ?Y = "epred  (Y ∩ {x. x ≠ 0})"
from chain_epredI [OF chain] Y'
have "f (⨆?Y) (eSuc (⨆?Y)) = lub ((λx. f x (eSuc x))  ?Y)"
using mcont [THEN mcont_contD] by blast
moreover from chain_epredI [OF chain] Y'
have "⨆(eSuc  ?Y) = eSuc (⨆?Y)"
using mcont_eSuc [THEN mcont_contD, symmetric] by blast
ultimately show "f (epred (Sup Y)) (Sup Y) = lub ((λx. f (epred x) x)  Y)"
by (subst (1 2 3) eq) (simp add: image_image)
next
fix x :: enat
assume "¬ x ≤ 0"
thus "ord bot (f (epred x) x)"
by(cases x rule: co.enat.exhaust)(auto intro: ord)
qed
also have "(λx. if x ≤ 0 then bot else f (epred x) x) = (λx. case x of 0 ⇒ bot | eSuc x' ⇒ f x' x)"
by(auto simp add: fun_eq_iff split: co.enat.split)
finally show ?thesis .
qed

subsection ‹Misc.›

"enat x + y < enat x + z ⟷ y < z"
by(cases y)(case_tac [!] z, simp_all)

lemma enat_add1_eq [simp]: "enat x + y = enat x + z ⟷ y = z"

lemma enat_add2_eq [simp]: "y + enat x = z + enat x ⟷ y = z"

lemma enat_less_enat_plusI: "x < y ⟹ enat x < enat y + z"
by(cases z) simp_all

lemma enat_less_enat_plusI2:
"enat y < z ⟹ enat (x + y) < enat x + z"

lemma min_enat1_conv_enat: "⋀a b. min (enat a) b = enat (case b of enat b' ⇒ min a b' | ∞ ⇒ a)"
and min_enat2_conv_enat: "⋀a b. min a (enat b) = enat (case a of enat a' ⇒ min a' b | ∞ ⇒ b)"
by(simp_all split: enat.split)

lemma eSuc_le_iff: "eSuc x ≤ y ⟷ (∃y'. y = eSuc y' ∧ x ≤ y')"
by(cases y rule: co.enat.exhaust) simp_all

lemma eSuc_eq_infinity_iff: "eSuc n = ∞ ⟷ n = ∞"

lemma infinity_eq_eSuc_iff: "∞ = eSuc n ⟷ n = ∞"

lemma enat_cocase_inf: "(case ∞ of 0 ⇒ a | eSuc b ⇒ f b) = f ∞"
by(auto split: co.enat.split simp add: infinity_eq_eSuc_iff)

lemma eSuc_Inf: "eSuc (Inf A) = Inf (eSuc  A)"
proof -
{ assume "A ≠ {}"
then obtain a where "a ∈ A" by blast
then have "eSuc (LEAST a. a ∈ A) = (LEAST a. a ∈ eSuc  A)"
proof (rule LeastI2_wellorder)
fix a assume "a ∈ A" and b: "∀b. b ∈ A ⟶ a ≤ b"
then have a: "eSuc a ∈ eSuc  A"
by auto
then show "eSuc a = (LEAST a. a ∈ eSuc  A)"
by (rule LeastI2_wellorder) (metis (full_types) b a antisym eSuc_le_iff imageE)
qed }
then show ?thesis
qed

end


Theory Coinductive_List

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

section ‹Coinductive lists and their operations›

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

subsection ‹Auxiliary lemmata›

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

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

subsection ‹Type definition›

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

text ‹
Coiterator setup.
›

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

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

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

text ‹congruence rule›

declare llist.map_cong [cong]

text ‹Code generator setup›

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

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

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

declare llist.map_sel(1)[simp]

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

declare llist.map_ident[simp]

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

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

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

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

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

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

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

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

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

declare llist.set_sel(1)[simp]

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

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

text ‹induction rules›

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

text ‹Test quickcheck setup›

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

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

subsection ‹Properties of predefined functions›

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

lemmas lhd_LCons_ltl = llist.collapse(2)

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

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

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

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

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

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

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

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

lemmas lset_LNil = llist.set(1)

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

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

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

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

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

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

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

text ‹code setup for @{term lset}›

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

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

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

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

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

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

lemmas lset_lmap [simp] = llist.set_map

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

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

declare lfinite_LNil [iff]

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

lemma lnull_lprefix: "lnull xs ⟹ lprefix xs ys"

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

subsection ‹Setup for partial\_function›

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

declare lSup.simps[simp del]

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

subsection ‹Monotonicity and continuity of already defined functions›

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

subsection ‹More function definitions›

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

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

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

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

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

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

context notes [[function_internals]]
begin

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

end

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

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

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

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

end

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

declare lnth.simps [simp del]

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

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

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

hide_fact (open) LNil LCons

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

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

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

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

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

context notes [[function_internals]]
begin

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

end

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

lemmas llength_ltl = epred_llength[symmetric]

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

lemmas ltake_epred_ltl = ltl_ltake [symmetric]

declare ltake.sel(2) [simp del]

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

lemma fixes f F
defines "F ≡ λldropn xs. case xs of LNil ⇒ λ_. LNil | LCons x xs ⇒ λn. if n = 0 then LCons x xs else ldropn xs (n - 1)"
shows ldrop_conv_fixp: "(λxs n. ldropn n xs) ≡ ccpo.fixp (fun_lub (fun_lub lSup)) (fun_ord (fun_ord lprefix)) (λldrop. F ldrop)" (is "?lhs ≡ ?rhs")
and ldrop_mono: "⋀xs. mono_llist_lift (λldrop. F ldrop xs)" (is "PROP ?mono")
proof(intro eq_reflection ext)
show mono: "PROP ?mono" unfolding F_def by(tactic ‹Partial_Function.mono_tac @{context} 1›)
fix n xs
show "?lhs xs n = ?rhs xs n"
by(induction n arbitrary: xs)
(subst llist_lift.mono_body_fixp[OF mono], simp add: F_def split: llist.split)+
qed

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

lemmas ldrop_eSuc_ltl = ldropn_ltl[symmetric]

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

lemma lnth_LNil:
"lnth LNil n = undefined n"

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

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

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

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

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

lemmas lnth_0_conv_lhd = lhd_conv_lnth[symmetric]

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

subsection‹iterates›

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

subsection ‹Length of the longest common prefix›

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

lemma monotone_lzip: "monotone (rel_prod (⊑) (⊑)) (⊑) (case_prod lzip)"
by(rule llist.fixp_preserves_mono2[OF lzip_mono lzip_conv_fixp]) simp

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

lemma mono2mono_ldropWhile [THEN llist.mono2mono, cont_intro, simp]:
shows monotone_ldropWhile: "monotone `