# Theory LList_CCPO_Topology

```(*  Title:       LList_CCPO_Topology.thy
Author:      Johannes Hölzl, TU Munich
Author:      Andreas Lochbihler, ETH Zurich
*)

section ‹A CCPO topology on lazy lists with examples›

theory LList_CCPO_Topology imports
CCPO_Topology
"../Coinductive_List_Prefix"
begin

lemma closed_Collect_eq_isCont:
fixes f g :: "'a :: t2_space ⇒ 'b::t2_space"
assumes f: "⋀x. isCont f x" and g: "⋀x. isCont g x"
shows "closed {x. f x = g x}"
by (intro closed_Collect_eq continuous_at_imp_continuous_on ballI assms)

instantiation llist :: (type) ccpo_topology
begin

definition open_llist :: "'a llist set ⇒ bool" where
"open_llist A ⟷ (∀C. chain C ⟶ C ≠ {} ⟶ Sup C ∈ A ⟶ C ∩ A ≠ {})"

instance

end

subsection ‹Continuity and closedness of predefined constants›

lemma tendsto_mcont_llist: "mcont lSup lprefix lSup lprefix f ⟹ f ─l→ f l"
by (auto simp add: Sup_llist_def[abs_def] intro!: tendsto_mcont)

lemma tendsto_ltl[THEN tendsto_compose, tendsto_intros]: "ltl ─l→ ltl l"
by (intro tendsto_mcont_llist mcont_ltl)

lemma tendsto_lappend2[THEN tendsto_compose, tendsto_intros]: "lappend l ─l'→ lappend l l'"
by (intro tendsto_mcont_llist mcont_lappend2)

lemma tendsto_LCons[THEN tendsto_compose, tendsto_intros]: "LCons x ─l→ LCons x l"
by (intro tendsto_mcont_llist mcont_LCons)

lemma tendsto_lmap[THEN tendsto_compose, tendsto_intros]: "lmap f ─l→ lmap f l"
by (intro tendsto_mcont_llist mcont_lmap)

lemma tendsto_llength[THEN tendsto_compose, tendsto_intros]: "llength ─l→ llength l"
by (intro tendsto_mcont) (simp add: Sup_llist_def[abs_def])

lemma tendsto_lset[THEN tendsto_compose, tendsto_intros]: "lset ─l→ lset l"

lemma open_lhd: "open {l. ¬ lnull l ∧ lhd l = x}"
unfolding open_ccpo set_eq_iff
proof (simp add: imp_conjL Sup_llist_def del: lhd_lSup, intro allI impI)
fix C assume "Complete_Partial_Order.chain lprefix C" "lhd (lSup C) = x"
moreover assume "∃c∈C. ¬ lnull c"
then obtain c where "c ∈ C" "¬ lnull c"
by auto
ultimately show "∃c. c ∈ C ∧ ¬ lnull c ∧ lhd c = x"
by (force simp: lhd_lSup_eq)
qed

lemma open_LCons': assumes A: "open A" shows "open (LCons x ` A)"
proof -
have "open (ltl -` A ∩ {l. ¬ lnull l ∧ lhd l = x})"
by (intro open_Int open_vimageI open_lhd A tendsto_intros)
also have "(ltl -` A ∩ {l. ¬ lnull l ∧ lhd l = x}) = LCons x ` A"
by force
finally show ?thesis .
qed

lemma open_Ici: "lfinite xs ⟹ open {xs ..}"
proof (induct xs rule: lfinite.induct)
case lfinite_LNil then show ?case
next
case (lfinite_LConsI xs x)
moreover have "{LCons x xs ..} = LCons x ` {xs ..}"
by (auto simp: LCons_lprefix_conv)
ultimately show ?case
by (auto intro: open_LCons')
qed

lemma open_lfinite[simp]: "lfinite x ⟹ open {x}"
proof (induct rule: lfinite.induct)
show "open {LNil}"
using open_ccpo_Iic[of LNil] by (simp add: atMost_def lnull_def)
qed (auto dest: open_LCons')

lemma open_singleton_iff_lfinite: "open {x} ⟷ lfinite x"
proof
assume "lfinite x" then show "open {x}"
unfolding compact_eq_lfinite[symmetric] Sup_llist_def[abs_def, symmetric] less_eq_llist_def[abs_def, symmetric]
by (rule open_singletonI_compact)
next
assume "open {x}"
show "lfinite x"
proof (rule ccontr)
let ?C = "{ys. lprefix ys x ∧ ys ≠ x}"
assume inf: "¬ lfinite x"
note lSup_strict_prefixes[OF this] ‹open {x}›
moreover have "chain ?C"
using lprefixes_chain[of x] by (auto dest: chain_compr)
moreover have "?C ≠ {}"
using inf by (cases x) auto
ultimately show False
by (auto simp: open_ccpo Sup_llist_def)
qed
qed

lemma closure_eq_lfinite:
assumes closed_Q: "closed {xs. Q xs}"
assumes downwards_Q: "⋀xs ys. Q xs ⟹ lprefix ys xs ⟹ Q ys"
shows "{xs. Q xs} = closure {xs. lfinite xs ∧ Q xs}"
proof (rule closure_unique[symmetric])
fix T assume T: "{xs. lfinite xs ∧ Q xs} ⊆ T" and "closed T"

show "{xs. Q xs} ⊆ T"
proof clarify
fix xs :: "'a llist"
let ?F = "{ys. lprefix ys xs ∧ lfinite ys}"
assume "Q xs"
with T downwards_Q have "?F ⊆ T"
by auto
moreover have "chain ?F" "?F ≠ {}"
by (auto intro: lprefixes_chain chain_subset)
moreover have "lSup ?F = xs"
by (rule lSup_finite_prefixes)
ultimately show "xs ∈ T"
using ‹closed T› by (auto simp: closed_ccpo Sup_llist_def)
qed
qed (auto simp: closed_Q)

lemma closure_lfinite: "closure {xs. lfinite xs} = UNIV"
using closure_eq_lfinite[of "λ_. True"] by auto

lemma closed_ldistinct: "closed {xs. ldistinct xs}"
unfolding closed_ccpo by (auto simp: ldistinct_lSup Sup_llist_def subset_eq)

lemma ldistinct_closure: "{xs. ldistinct xs} = closure {xs. lfinite xs ∧ ldistinct xs}"
by (rule closure_eq_lfinite[OF closed_ldistinct ldistinct_lprefix])

lemma closed_ldistinct': "(⋀x. isCont f x) ⟹ closed {xs. ldistinct (f xs)}"
using continuous_closed_vimage[of _ f, OF closed_ldistinct] by auto

lemma closed_lsorted: "closed {xs. lsorted xs}"
unfolding closed_ccpo by (auto simp: lsorted_lSup Sup_llist_def subset_eq)

lemma lsorted_closure: "{xs. lsorted xs} = closure {xs. lfinite xs ∧ lsorted xs}"
by (rule closure_eq_lfinite[OF closed_lsorted lsorted_lprefixD])

lemma closed_lsorted': "(⋀x. isCont f x) ⟹ closed {xs. lsorted (f xs)}"
using continuous_closed_vimage[of _ f, OF closed_lsorted] by auto

lemma closed_in_lset: "closed {l. x ∈ lset l}"
unfolding closed_ccpo by (auto simp add: subset_eq lset_lSup Sup_llist_def)

lemma closed_llist_all2:
"closed {(x, y). llist_all2 R x y}"
proof -
{ fix a b assume *: "⋀A B. open A ⟹ open B ⟹ a ∈ A ⟹ b ∈ B ⟹ (∃x∈A. ∃y∈B. llist_all2 R x y)"
then have "llist_all2 R a b"
proof (coinduction arbitrary: a b)
case LNil
from LNil[rule_format, of "{LNil}" "- {LNil}"] LNil[rule_format, of "- {LNil}" "{LNil}"]
show ?case
by (auto simp: closed_def[symmetric] lnull_def)
next
case LCons
show ?case
proof
show ?lhd
using LCons(1)[rule_format, OF open_lhd open_lhd, of "lhd a" "lhd b"] LCons(2,3)
by (auto dest: llist_all2_lhdD)
show ?ltl
proof (rule, simp, safe)
fix A B assume "open A" "open B" "ltl a ∈ A" "ltl b ∈ B"
with LCons(1)[rule_format, OF open_LCons' open_LCons', of A B "lhd a" "lhd b"] LCons(2,3)
show "∃a'∈A. ∃b'∈B. llist_all2 R a' b'"
by (auto simp: not_lnull_conv)
qed
qed
qed }
then show ?thesis
unfolding closed_def open_prod_def
by (auto simp: subset_eq)
qed

lemma closed_list_all2:
fixes f g :: "'b::t2_space ⇒ 'a llist"
assumes f: "⋀x. isCont f x" and g: "⋀x. isCont g x"
shows "closed {x. llist_all2 R (f x) (g x)}"
using  continuous_closed_vimage[OF closed_llist_all2  isCont_Pair[OF f g]] by simp

lemma at_botI_lfinite[simp]: "lfinite l ⟹ at l = bot"

lemma at_eq_lfinite: "at l = (if lfinite l then bot else at' l)"
by (auto simp: at'_def open_singleton_iff_lfinite)

lemma eventually_lfinite: "eventually lfinite (at' x)"
apply (simp add: at'_def open_singleton_iff_lfinite eventually_principal eventually_at_topological)
apply (intro exI[of _ "{.. x}"] impI conjI open_ccpo_Iic)
apply (auto simp: lstrict_prefix_def intro!: lstrict_prefix_lfinite1)
done

lemma eventually_nhds_llist:
"eventually P (nhds l) ⟷ (∃xs≤l. lfinite xs ∧ (∀ys≥xs. ys ≤ l ⟶ P ys))"
unfolding eventually_nhds
proof safe
let ?F = "{l'. lprefix l' l ∧ lfinite l'}"
fix A assume "open A" "l ∈ A" "∀l∈A. P l"
moreover have "chain ?F" "?F ≠ {}"
by (auto simp: chain_def dest: lprefix_down_linear)
moreover have "Sup ?F = l"
unfolding Sup_llist_def by (rule lSup_finite_prefixes)
ultimately have "∃xs. xs ∈ ?F ∧ (∀ys≥xs. ys ∈ ?F ⟶ P ys)"
using open_ccpoD[of A ?F] by auto
then show "∃xs≤l. lfinite xs ∧ (∀ys≥xs. ys ≤ l ⟶ P ys)"
by (metis (lifting) ‹l ∈ A› ‹∀l∈A. P l› le_llist_conv_lprefix mem_Collect_eq not_lfinite_lprefix_conv_eq)
next
fix xs assume "xs ≤ l" "lfinite xs" "∀ys≥xs. ys ≤ l ⟶ P ys"
then show "∃S. open S ∧ l ∈ S ∧ Ball S P"
by (intro exI[of _ "{xs ..} ∩ {.. l}"] conjI open_Int open_Ici open_ccpo_Iic) auto
qed

lemma nhds_lfinite: "lfinite l ⟹ nhds l = principal {l}"
unfolding filter_eq_iff eventually_principal eventually_nhds_llist
by (auto simp del: le_llist_conv_lprefix)

lemma eventually_at'_llist:
"eventually P (at' l) ⟷ (∃xs≤l. lfinite xs ∧ (∀ys≥xs. lfinite ys ⟶ ys ≤ l ⟶ P ys))"
proof cases
assume "lfinite l"
then show ?thesis
by (auto simp add: eventually_filtermap at'_def open_singleton_iff_lfinite
eventually_principal lfinite_eq_range_llist_of)
next
assume "¬ lfinite l"
then show ?thesis
by (auto simp: eventually_filtermap at'_def open_singleton_iff_lfinite
eventually_at_filter eventually_nhds_llist)
(metis not_lfinite_lprefix_conv_eq)
qed

lemma eventually_at'_llistI: "(⋀xs. lfinite xs ⟹ xs ≤ l ⟹ P xs) ⟹ eventually P (at' l)"
by (auto simp: eventually_at'_llist)

lemma Lim_at'_lfinite: "lfinite xs ⟹ Lim (at' xs) f = f xs"
by (rule tendsto_Lim[OF at'_bot]) (auto simp add: at'_def topological_tendstoI eventually_principal)

lemma filterlim_at'_list:
"(f ⤏ y) (at' (x::'a llist)) ⟹ f ─x→ y"
unfolding at'_def by (auto split: if_split_asm simp: open_singleton_iff_lfinite)

lemma tendsto_mcont_llist': "mcont lSup lprefix lSup lprefix f ⟹ (f ⤏ f x) (at' (x :: 'a llist))"
by(auto simp add: at'_def nhds_lfinite[symmetric] open_singleton_iff_lfinite tendsto_at_iff_tendsto_nhds[symmetric] intro: tendsto_mcont_llist)

lemma tendsto_closed:
assumes eq: "closed {x. P x}"
assumes ev: "⋀ys. lfinite ys ⟹ ys ≤ x ⟹ P ys"
shows "P x"
proof -
have "x ∈ {x. P x}"
proof (rule Lim_in_closed_set)
show "eventually (λx. x ∈ {x. P x}) (at' x)"
unfolding eq using ev
by (force intro!: eventually_at'_llistI)
qed (rule assms tendsto_id_at' at'_bot)+
then show ?thesis
by simp
qed

lemma tendsto_Sup_at':
fixes f :: "'a llist ⇒ 'b::ccpo_topology"
assumes f: "⋀x y. x ≤ y ⟹ lfinite x ⟹ lfinite y ⟹ f x ≤ f y"
shows "(f ⤏ (Sup (f`{xs. lfinite xs ∧ xs ≤ l}))) (at' l)"
proof (rule topological_tendstoI)
let ?F = "{xs. lfinite xs ∧ xs ≤ l}"

have ch_F: "chain (f`?F)" "f`?F ≠ {}"
by (rule chain_imageI[OF chain_subset, OF lprefixes_chain]) (auto simp: f)

fix A assume A: "open A" "Sup (f`?F) ∈ A" then show "eventually (λx. f x ∈ A) (at' l)"
using open_ccpoD[OF _ ch_F, OF A] by (auto simp: eventually_at'_llist f simp del: le_llist_conv_lprefix)
qed

lemma tendsto_Lim_at':
fixes f :: "'a llist ⇒ 'b::ccpo_topology"
assumes f: "⋀l. f l = Lim (at' l) f'"
assumes mono: "⋀x y. x ≤ y ⟹ lfinite x ⟹ lfinite y ⟹ f' x ≤ f' y"
shows "(f ⤏ f l) (at' l)"
unfolding f[abs_def]
apply (subst filterlim_cong[OF refl refl eventually_mono[OF eventually_lfinite Lim_at'_lfinite]])
apply assumption
apply (rule tendsto_LimI[OF tendsto_Sup_at'[OF mono]])
apply assumption+
done

lemma isCont_LCons[THEN isCont_o2[rotated]]: "isCont (LCons x) l"
by (simp add: isCont_def tendsto_LCons tendsto_ident_at)

lemma isCont_lmap[THEN isCont_o2[rotated]]: "isCont (lmap f) l"
by (simp add: isCont_def tendsto_lmap tendsto_ident_at)

lemma isCont_lappend[THEN isCont_o2[rotated]]: "isCont (lappend xs) ys"
by (simp add: isCont_def tendsto_lappend2 tendsto_ident_at)

lemma isCont_lset[THEN isCont_o2[rotated]]: "isCont lset xs"

subsection ‹Define @{term lfilter} as continuous extension›

definition "lfilter' P l = Lim (at' l) (λxs. llist_of (filter P (list_of xs)))"

lemma tendsto_lfilter: "(lfilter' P ⤏ lfilter' P xs) (at' xs)"
by (rule tendsto_Lim_at'[OF lfilter'_def]) (auto simp add: lfinite_eq_range_llist_of less_eq_list_def prefix_def)

lemma isCont_lfilter[THEN isCont_o2[rotated]]: "isCont (lfilter' P) l"
by (simp add: isCont_def filterlim_at'_list tendsto_lfilter)

lemma lfilter'_lfinite[simp]: "lfinite xs ⟹ lfilter' P xs = llist_of (filter P (list_of xs))"

lemma lfilter'_LNil: "lfilter' P LNil = LNil"
by simp

lemma lfilter'_LCons [simp]: "lfilter' P (LCons a xs) = (if P a then LCons a (lfilter' P xs) else lfilter' P xs)"
by (rule tendsto_closed[where x=xs, OF closed_Collect_eq_isCont])
(auto intro!: isCont_lfilter isCont_LCons isCont_If)

lemma ldistinct_lfilter': "ldistinct l ⟹ ldistinct (lfilter' P l)"
by (rule tendsto_closed[OF closed_ldistinct', OF isCont_lfilter])
(auto intro!: distinct_filter dest: ldistinct_lprefix simp: lfinite_eq_range_llist_of)

lemma lfilter'_lmap: "lfilter' P (lmap f xs) = lmap f (lfilter' (P ∘ f) xs)"
by (rule tendsto_closed[where x=xs, OF closed_Collect_eq_isCont])
(auto simp add: filter_map comp_def intro!: isCont_lmap isCont_lfilter)

lemma lfilter'_lfilter': "lfilter' P (lfilter' Q xs) = lfilter' (λx. Q x ∧ P x) xs"
by (rule tendsto_closed[where x=xs, OF closed_Collect_eq_isCont]) (auto intro!: isCont_lfilter)

lemma lfilter'_LNil_I[simp]: "(∀x ∈ lset xs. ¬ P x) ⟹ lfilter' P xs = LNil"
by (rule tendsto_closed[where x=xs, OF closed_Collect_eq_isCont])
(auto simp add: lfinite_eq_range_llist_of llist_of_eq_LNil_conv filter_empty_conv intro: isCont_lfilter dest!: lprefix_lsetD)

lemma lset_lfilter': "lset (lfilter' P xs) = lset xs ∩ {x. P x}"
by(rule tendsto_closed[OF closed_Collect_eq_isCont])
(auto 4 3 intro: isCont_lset isCont_lfilter isCont_inf2)

lemma lfilter'_eq_LNil_iff: "lfilter' P xs = LNil ⟷ (∀x∈lset xs. ¬ P x)"
using lset_lfilter'[of P xs] by auto

lemma lfilter'_eq_lfilter: "lfilter' P xs = lfilter P xs"
using isCont_lfilter
proof(rule tendsto_closed[where x=xs, OF closed_Collect_eq_isCont])
fix ys :: "'a llist"
assume "lfinite ys"
thus "lfilter' P ys = lfilter P ys" by induction simp_all

subsection ‹Define @{term lconcat} as continuous extension›

definition "lconcat' xs = Lim (at' xs) (λxs. foldr lappend (list_of xs) LNil)"

lemma tendsto_lconcat': "(lconcat' ⤏ lconcat' xss) (at' xss)"
apply (rule tendsto_Lim_at'[OF lconcat'_def])
apply (auto simp add: lfinite_eq_range_llist_of less_eq_list_def prefix_def)
apply (induct_tac xa)
apply simp_all
done

lemma isCont_lconcat'[THEN isCont_o2[rotated]]: "isCont lconcat' l"
by (simp add: isCont_def filterlim_at'_list tendsto_lconcat')

lemma lconcat'_lfinite[simp]: "lfinite xs ⟹ lconcat' xs = foldr lappend (list_of xs) LNil"

lemma lconcat'_LNil: "lconcat' LNil = LNil"
by simp

lemma lconcat'_LCons [simp]: "lconcat' (LCons l xs) = lappend l (lconcat' xs)"
by (rule tendsto_closed[where x=xs, OF closed_Collect_eq_isCont])
(auto intro!: isCont_lconcat' isCont_lappend isCont_LCons)

lemma lmap_lconcat: "lmap f (lconcat' xss) = lconcat' (lmap (lmap f) (xss::'a llist llist))"
proof (rule tendsto_closed[where x=xss, OF closed_Collect_eq_isCont])
fix xs :: "'a llist llist"
assume "lfinite xs"
then show "lmap f (lconcat' xs) = lconcat' (lmap (lmap f) xs)"
by (induct xs rule: lfinite.induct) (auto simp: lmap_lappend_distrib)
qed (intro isCont_lconcat' isCont_lappend isCont_LCons continuous_ident isCont_lmap)+

lemmas tendsto_Sup[THEN tendsto_compose, tendsto_intros] =
mcont_SUP[OF mcont_id' mcont_const, THEN tendsto_mcont]

lemma
assumes fin: "∀xs∈lset xss. lfinite xs"
shows "lset (lconcat' xss) = (⋃xs∈lset xss. lset xs)" (is "?lhs = ?rhs")
proof(rule tendsto_unique_eventually[OF at'_bot])
show "eventually (λx. lset (lconcat' x) = (⋃y∈lset x. lset y)) (at' xss)"
proof(rule eventually_at'_llistI)
fix xss'
assume "lfinite xss'" "xss' ≤ xss"
hence "∀xs∈lset xss'. lfinite xs" using fin by (auto dest!: lprefix_lsetD)
with ‹lfinite xss'› show "lset (lconcat' xss') = (⋃xs∈lset xss'. lset xs)"
by (induct xss') auto
qed
qed (rule tendsto_intros tendsto_lconcat' tendsto_id_at')+

subsection ‹Define @{term ldropWhile} as continuous extension›

definition "ldropWhile' P xs = Lim (at' xs) (λxs. llist_of (dropWhile P (list_of xs)))"

lemma tendsto_ldropWhile':
"(ldropWhile' P ⤏ ldropWhile' P xs) (at' xs)"
by (rule tendsto_Lim_at'[OF ldropWhile'_def])
(auto simp add: lfinite_eq_range_llist_of less_eq_list_def prefix_def dropWhile_append dropWhile_False)

lemma isCont_ldropWhile'[THEN isCont_o2[rotated]]: "isCont (ldropWhile' P) l"
by (simp add: isCont_def filterlim_at'_list tendsto_ldropWhile')

lemma ldropWhile'_lfinite[simp]: "lfinite xs ⟹ ldropWhile' P xs = llist_of (dropWhile P (list_of xs))"

lemma ldropWhile'_LNil: "ldropWhile' P LNil = LNil"
by simp

lemma ldropWhile'_LCons [simp]: "ldropWhile' P (LCons l xs) = (if P l then ldropWhile' P xs else LCons l xs)"
by (rule tendsto_closed[where x=xs, OF closed_Collect_eq_isCont])
(auto intro!: isCont_ldropWhile' isCont_If isCont_LCons)

lemma "ldropWhile' P (lmap f xs) = lmap f (ldropWhile' (P ∘ f) xs)"
by (rule tendsto_closed[where x=xs, OF closed_Collect_eq_isCont])
(auto simp add: dropWhile_map comp_def intro!: isCont_lmap isCont_ldropWhile')

lemma ldropWhile'_LNil_I[simp]: "∀x ∈ lset xs. P x ⟹ ldropWhile' P xs = LNil"
by (rule tendsto_closed[where x=xs, OF closed_Collect_eq_isCont])
(auto simp add: llist_of_eq_LNil_conv intro!: isCont_lmap isCont_ldropWhile' dest!: lprefix_lsetD)

lemma lnull_ldropWhile': "lnull (ldropWhile' P xs) ⟷ (∀x ∈ lset xs. P x)" (is "?lhs ⟷ _")
proof (intro iffI ballI)
fix x assume "x ∈ lset xs" ?lhs then show "P x" by induct (simp_all split: if_split_asm)
qed simp

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

subsection ‹Define ‹ldrop› as continuous extension›

primrec edrop where
"edrop n [] = []"
| "edrop n (x # xs) = (case n of eSuc n ⇒ edrop n xs | 0 ⇒ x # xs)"

lemma mono_edrop: "edrop n xs ≤ edrop n (xs @ ys)"
by (induct xs arbitrary: n) (auto split: enat_cosplit)

lemma edrop_mono: "xs ≤ ys ⟹ edrop n xs ≤ edrop n ys"
using mono_edrop[of n xs] by (auto simp add: less_eq_list_def prefix_def)

definition "ldrop' n xs = Lim (at' xs) (llist_of ∘ edrop n ∘ list_of)"

lemma ldrop'_lfinite[simp]: "lfinite xs ⟹ ldrop' n xs = llist_of (edrop n (list_of xs))"

lemma tendsto_ldrop': "(ldrop' n ⤏ ldrop' n l) (at' l)"
by (rule tendsto_Lim_at'[OF ldrop'_def]) (auto simp add: lfinite_eq_range_llist_of intro!: edrop_mono)

lemma isCont_ldrop'[THEN isCont_o2[rotated]]: "isCont (ldrop' n) l"
by (simp add: isCont_def filterlim_at'_list tendsto_ldrop')

lemma "ldrop' n LNil = LNil"
by simp

lemma "ldrop' n (LCons x xs) = (case n of 0 ⇒ LCons x xs | eSuc n ⇒ ldrop' n xs)"
by (rule tendsto_closed[where x=xs, OF closed_Collect_eq_isCont])
(auto intro!: isCont_ldrop' isCont_enat_case isCont_LCons split: enat_cosplit)

primrec up :: "'a :: order ⇒ 'a list ⇒ 'a list" where
"up a [] = []"
| "up a (x # xs) = (if a < x then x # up x xs else up a xs)"

lemma set_upD: "x ∈ set (up y xs) ⟹ x ∈ set xs ∧ y < x"
by (induct xs arbitrary: y) (auto split: if_split_asm intro: less_trans)

lemma prefix_up: "prefix (up a xs) (up a (xs @  ys))"
by (induction xs arbitrary: a) auto

lemma mono_up: "xs ≤ ys ⟹ up a xs ≤ up a ys"
unfolding less_eq_list_def by (subst (asm) prefix_def) (auto intro!: prefix_up)

lemma sorted_up: "sorted (up a xs)"
by (induction xs arbitrary: a) (auto dest: set_upD intro: less_imp_le)

subsection ‹Define more functions on lazy lists as continuous extensions›

definition "lup a xs = Lim (at' xs) (λxs. llist_of (up a (list_of xs)))"

lemma tendsto_lup: "(lup a ⤏ lup a xs) (at' xs)"
by (rule tendsto_Lim_at'[OF lup_def]) (auto simp: lfinite_eq_range_llist_of mono_up)

lemma isCont_lup[THEN isCont_o2[rotated]]: "isCont (lup a) l"
by (simp add: isCont_def filterlim_at'_list tendsto_lup)

lemma lup_lfinite[simp]: "lfinite xs ⟹ lup a xs = llist_of (up a (list_of xs))"

lemma lup_LNil: "lup a LNil = LNil"
by simp

lemma lup_LCons [simp]: "lup a (LCons x xs) = (if a < x then LCons x (lup x xs) else lup a xs)"
by (rule tendsto_closed[where x=xs, OF closed_Collect_eq_isCont])
(auto intro!: isCont_lup isCont_If isCont_LCons)

lemma lset_lup: "lset (lup x xs) ⊆ lset xs ∩ {y. x < y}"
by (rule tendsto_le_ccpo[where g="λxs. lset (lup x xs)" and f="λxs. lset xs ∩ {y. x < y}" and F="at' xs"])
(auto dest!: lprefix_lsetD set_upD intro!:  tendsto_intros at'_bot tendsto_lup eventually_at'_llistI)

lemma lsorted_lup: "lsorted (lup (a::'a::linorder) l)"
by (rule tendsto_closed[OF closed_lsorted', OF isCont_lup])
(auto intro!: sorted_up simp: lprefix_conv_lappend)

context notes [[function_internals]]
begin

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

end

declare lup'.mono[cont_intro]

lemma monotone_lup': "monotone (rel_prod (=) lprefix) lprefix (λ(a, xs). lup' a xs)"
by(rule llist.fixp_preserves_mono2[OF lup'.mono lup'_def]) simp

lemma mono2mono_lup'2[THEN llist.mono2mono, simp, cont_intro]:
shows monotone_lup'2: "monotone lprefix lprefix (lup' a)"
using monotone_lup' by auto

lemma mcont_lup': "mcont (prod_lub the_Sup lSup) (rel_prod (=) lprefix) lSup lprefix (λ(a, xs). lup' a xs)"
by(rule llist.fixp_preserves_mcont2[OF lup'.mono lup'_def]) simp

lemma mcont2mcont_lup'2[THEN llist.mcont2mcont, simp, cont_intro]:
shows mcont_lup'2: "mcont lSup lprefix lSup lprefix (lup' a)"
using mcont_lup' by auto

simps_of_case lup'_simps [simp]: lup'.simps

lemma lset_lup'_subset:
fixes x :: "_ :: preorder"
shows "lset (lup' x xs) ⊆ lset xs ∩ {y. x < y}"
by(induction xs arbitrary: x)(auto intro: less_trans)

lemma in_lset_lup'D:
fixes x :: "_ :: preorder"
assumes "y ∈ lset (lup' x xs)"
shows "y ∈ lset xs ∧ x < y"
using lset_lup'_subset[of x xs] assms by auto

lemma lsorted_lup':
fixes x :: "_ :: preorder"
shows "lsorted (lup' x xs)"
by(induction xs arbitrary: x)(auto simp add: lsorted_LCons dest: in_lset_lup'D intro: less_imp_le)

lemma ldistinct_lup':
fixes x :: "_ :: preorder"
shows "ldistinct (lup' x xs)"
by(induction xs arbitrary: x)(auto dest: in_lset_lup'D)

context fixes f :: "'a ⇒ 'a" begin

partial_function (llist) iterate :: "'a ⇒ 'a llist"
where "iterate x = LCons x (iterate (f x))"

lemma lmap_iterate: "lmap f (iterate x) = iterate (f x)"
by(induction arbitrary: x rule: iterate.fixp_induct) simp_all

end

fun extup extdown  :: "int ⇒ int list ⇒ int list" where
"extup i [] = []"
| "extup i (x # xs) = (if i ≤ x then extup x xs else i # extdown x xs)"
| "extdown i [] = []"
| "extdown i (x # xs) = (if i ≥ x then extdown x xs else i # extup x xs)"

lemma prefix_ext:
"prefix (extup a xs) (extup a (xs @  ys))"
"prefix (extdown a xs) (extdown a (xs @  ys))"
by (induction xs arbitrary: a) auto

lemma mono_ext: assumes "xs ≤ ys" shows "extup a xs ≤ extup a ys" "extdown a xs ≤ extdown a ys"
using assms[unfolded less_eq_list_def prefix_def] by (auto simp: less_eq_list_def prefix_ext)

lemma set_ext: "set (extup a xs) ⊆ {a} ∪ set xs" "set (extdown a xs) ⊆ {a} ∪ set xs"
by (induction xs arbitrary: a) auto

definition "lextup i l = Lim (at' l) (llist_of ∘ extup i ∘ list_of)"
definition "lextdown i l = Lim (at' l) (llist_of ∘ extdown i ∘ list_of)"

lemma tendsto_lextup[tendsto_intros]: "(lextup i ⤏ lextup i xs) (at' xs)"
by (rule tendsto_Lim_at'[OF lextup_def]) (auto simp: lfinite_eq_range_llist_of mono_ext)

lemma tendsto_lextdown[tendsto_intros]: "(lextdown i ⤏ lextdown i xs) (at' xs)"
by (rule tendsto_Lim_at'[OF lextdown_def]) (auto simp: lfinite_eq_range_llist_of mono_ext)

lemma isCont_lextup[THEN isCont_o2[rotated]]: "isCont (lextup a) l"
by (simp add: isCont_def filterlim_at'_list tendsto_lextup)

lemma isCont_lextdown[THEN isCont_o2[rotated]]: "isCont (lextdown a) l"
by (simp add: isCont_def filterlim_at'_list tendsto_lextdown)

lemma lextup_lfinite[simp]: "lfinite xs ⟹ lextup i xs = llist_of (extup i (list_of xs))"

lemma lextdown_lfinite[simp]: "lfinite xs ⟹ lextdown i xs = llist_of (extdown i (list_of xs))"

lemma "lextup i LNil = LNil" "lextdown i LNil = LNil"
by simp_all

lemma "lextup i (LCons x xs) = (if i ≤ x then lextup x xs else LCons i (lextdown x xs))"
by (rule tendsto_closed[where x=xs, OF closed_Collect_eq_isCont])
(auto intro!: isCont_lextdown isCont_lextup isCont_If isCont_LCons)

lemma "lextdown i (LCons x xs) = (if x ≤ i then lextdown x xs else LCons i (lextup x xs))"
by (rule tendsto_closed[where x=xs, OF closed_Collect_eq_isCont])
(auto intro!: isCont_lextdown isCont_lextup isCont_If isCont_LCons)

lemma "lset (lextup a xs) ⊆ {a} ∪ lset xs"
apply (rule tendsto_le_ccpo[where g="λxs. lset (lextup a xs)" and f="λxs. {a} ∪ lset xs" and F="at' xs"])
apply (rule tendsto_intros at'_bot tendsto_lup eventually_at'_llistI tendsto_id_at')+
apply (auto dest!: lprefix_lsetD set_ext[THEN subsetD])
done

lemma "lset (lextdown a xs) ⊆ {a} ∪ lset xs"
apply (rule tendsto_le_ccpo[where g="λxs. lset (lextdown a xs)" and f="λxs. {a} ∪ lset xs" and F="at' xs"])
apply (rule tendsto_intros at'_bot tendsto_lup eventually_at'_llistI tendsto_id_at')+
apply (auto dest!: lprefix_lsetD set_ext[THEN subsetD])
done

lemma distinct_ext:
assumes "distinct xs" "a ∉ set xs"
shows "distinct (extup a xs)" "distinct (extdown a xs)"
using assms set_ext
apply (induction xs arbitrary: a)
apply auto
apply (metis eq_iff insert_iff subset_iff)+
done

lemma "ldistinct xs ⟹ a ∉ lset xs ⟹ ldistinct (lextup a xs)"
by (rule_tac tendsto_closed[OF closed_ldistinct', OF isCont_lextup])
(force simp: lfinite_eq_range_llist_of intro!: distinct_ext dest: ldistinct_lprefix dest: lprefix_lsetD)+

definition esum_list :: "ereal llist ⇒ ereal" where
"esum_list xs = Lim (at' xs) (sum_list ∘ list_of)"

lemma esum_list_lfinite[simp]: "lfinite xs ⟹ esum_list xs = sum_list (list_of xs)"

lemma esum_list_LNil: "esum_list LNil = 0"
by simp

context
fixes xs :: "ereal llist"
assumes xs: "⋀x. x ∈ lset xs ⟹ 0 ≤ x"
begin

lemma esum_list_tendsto_SUP:
"((sum_list∘list_of) ⤏ (SUP ys ∈ {ys. lfinite ys ∧ ys ≤ xs}. esum_list ys)) (at' xs)"
(is "(_ ⤏ ?y) _")
proof (rule order_tendstoI)
fix a assume "a < ?y"
then obtain ys where "llist_of ys ≤ xs" "a < sum_list ys"
by (auto simp: less_SUP_iff lfinite_eq_range_llist_of)
moreover
{ fix zs assume "ys ≤ zs" "llist_of zs ≤ xs"
then obtain ys' where zs: "zs = ys @ ys'"
by (auto simp: prefix_def less_eq_list_def)
with ‹llist_of zs ≤ xs› have nonneg: "0 ≤ sum_list ys'"
using xs by (auto simp: lprefix_conv_lappend sum_list_sum_nth intro: sum_nonneg)
note ‹a < sum_list ys›
also have "sum_list ys ≤ sum_list zs"
using zs add_mono[OF order_refl nonneg] by auto
finally have "a < sum_list zs" . }
ultimately show "eventually (λx. a < (sum_list∘list_of) x) (at' xs)"
unfolding eventually_at'_llist by (auto simp: lfinite_eq_range_llist_of)
next
fix a assume "?y < a" then show "eventually (λx. (sum_list∘list_of) x < a) (at' xs)"
by (auto intro!: eventually_at'_llistI dest: SUP_lessD)
qed

lemma tendsto_esum_list: "(esum_list ⤏ esum_list xs) (at' xs)"
apply (rule filterlim_cong[where g="sum_list ∘ list_of", THEN iffD2, OF refl refl])
apply (rule eventually_mono[OF eventually_lfinite])
apply simp
unfolding esum_list_def
apply (rule tendsto_LimI)
apply (rule esum_list_tendsto_SUP)
done

lemma isCont_esum_list: "isCont esum_list xs"
by (simp add: isCont_def filterlim_at'_list tendsto_esum_list)

end

lemma esum_list_nonneg:
"(⋀x. x ∈ lset xs ⟹ 0 ≤ x) ⟹ 0 ≤ esum_list xs"
by (rule tendsto_le[OF at'_bot tendsto_esum_list tendsto_const])
(auto intro!: eventually_at'_llistI sum_nonneg
simp: lprefix_conv_lappend sum_list_sum_nth lfinite_eq_range_llist_of)

lemma esum_list_LCons:
assumes x: "0 ≤ x" "⋀x. x ∈ lset xs ⟹ 0 ≤ x" shows "esum_list (LCons x xs) = x + esum_list xs"
proof (rule tendsto_unique_eventually[OF at'_bot])
from x show "((λxs. esum_list (LCons x xs)) ⤏ esum_list (LCons x xs)) (at' xs)"
by (intro tendsto_compose[OF filterlim_at'_list[OF tendsto_esum_list] tendsto_LCons]) auto
show "eventually (λxa. esum_list (LCons x xa) = x + esum_list xa) (at' xs)"
using eventually_lfinite by eventually_elim simp
from x show "((λxa. x + esum_list xa) ⤏ x + esum_list xs) (at' xs)"
by (intro esum_list_nonneg tendsto_esum_list tendsto_add_ereal) auto
qed

lemma esum_list_lfilter':
assumes nn: "⋀x. x ∈ lset xs ⟹ 0 ≤ x" shows "esum_list (lfilter' (λx. x ≠ 0) xs) = esum_list xs"
proof (rule tendsto_unique_eventually[OF at'_bot])
show "(esum_list ⤏ esum_list xs) (at' xs)"
using nn by (rule tendsto_esum_list)
from nn show "((λxs. esum_list (lfilter' (λx. x ≠ 0) xs)) ⤏ esum_list (lfilter' (λx. x ≠ 0) xs)) (at' xs)"
by (intro tendsto_compose[OF filterlim_at'_list[OF tendsto_esum_list] tendsto_lfilter]) (auto simp: lset_lfilter')
show "eventually (λxs. esum_list (lfilter' (λx. x ≠ 0) xs) = esum_list xs) (at' xs)"
using eventually_lfinite
by eventually_elim (simp add: sum_list_map_filter[where f = "λx. x" and P="λx. x ≠ 0", simplified])
qed

function f:: "nat list ⇒ nat list" where
"f [] = []"
| "f (x#xs) = (x * 2) # f (f xs)"
by auto pat_completeness

termination f
proof (relation "inv_image natLess length")
fix x xs assume "f_dom xs" then show "(f xs, x # xs) ∈ inv_image natLess length"
by induct (auto simp: f.psimps natLess_def)
qed (auto intro: wf_less simp add: natLess_def)

lemma length_f[simp]: "length (f xs) = length xs"
by (induct rule: f.induct) simp_all

lemma f_mono': "∃ys'. f (xs @ ys) = f xs @ ys'"
proof (induct "length xs" arbitrary: xs ys rule: less_induct)
case less then show ?case
apply (cases xs)
apply auto
apply (metis length_f lessI)
done
qed

lemma f_mono: "xs ≤ ys ⟹ f xs ≤ f ys"
by (auto simp: less_eq_list_def prefix_def f_mono')

definition "f' l = Lim (at' l) (λl. llist_of (f (list_of l)))"

lemma f'_lfinite[simp]: "lfinite xs ⟹ f' xs = llist_of (f (list_of xs))"

lemma tendsto_f': "(f' ⤏ f' l) (at' l)"
by (rule tendsto_Lim_at'[OF f'_def]) (auto simp add: lfinite_eq_range_llist_of intro!: f_mono)

lemma isCont_f'[THEN isCont_o2[rotated]]: "isCont f' l"
by (simp add: isCont_def filterlim_at'_list tendsto_f')

lemma "f' LNil = LNil"
by simp

lemma "f' (LCons x xs) = LCons (x * 2) (f' (f' xs))"
by (rule tendsto_closed[where x=xs, OF closed_Collect_eq_isCont])
(auto intro!: isCont_f' isCont_LCons)

end
```