(* 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 by intro_classes (simp add: open_llist_def) 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" by(rule tendsto_mcont)(simp add: Sup_llist_def[abs_def]) 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 by (simp add: atLeast_def) 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" by (simp add: at_eq_bot_iff) 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" by(simp add: isCont_def tendsto_lset tendsto_ident_at) 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))" by (simp add: lfilter'_def Lim_at'_lfinite) 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 qed(simp_all add: isCont_def tendsto_mcont_llist mcont_lfilter) 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" by (simp add: lconcat'_def Lim_at'_lfinite) 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))" by (simp add: ldropWhile'_def Lim_at'_lfinite) 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))" by (simp add: ldrop'_def Lim_at'_lfinite) 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))" by (simp add: lup_def Lim_at'_lfinite) 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))" by (simp add: lextup_def Lim_at'_lfinite) lemma lextdown_lfinite[simp]: "lfinite xs ⟹ lextdown i xs = llist_of (extdown i (list_of xs))" by (simp add: lextdown_def Lim_at'_lfinite) 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)" by (simp add: esum_list_def Lim_at'_lfinite) 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))" by (simp add: f'_def Lim_at'_lfinite) 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