Theory Lazy_List_Limsup

(*  Title:       Limsup of Lazy Lists
    Author:      Asta Halkjær From <ahfrom at dtu.dk>, 2021

    Modelled on Ordered_Resolution_Prover.Lazy_List_Liminf
*)

section ‹Limsup of Lazy Lists›

theory Lazy_List_Limsup
  imports Coinductive.Coinductive_List
begin

subsection ‹Library›

lemma less_llength_ltake: "i < llength (ltake k Xs) ⟷ i < k ∧ i < llength Xs"
  by simp

subsection ‹Infimum›

definition Inf_llist :: ‹'a set llist ⇒ 'a set› where
  ‹Inf_llist Xs = (⋂i ∈ {i. enat i < llength Xs}. lnth Xs i)›

lemma Inf_llist_subset_lnth: ‹enat i < llength Xs ⟹ Inf_llist Xs ⊆ lnth Xs i›
  unfolding Inf_llist_def by fast

lemma Inf_llist_imp_exists_index:
  assumes ‹¬ lnull Xs›
  shows ‹x ∈ Inf_llist Xs ⟹ ∃i. enat i < llength Xs ∧ x ∈ lnth Xs i›
  unfolding Inf_llist_def using assms
  by (metis INT_E i0_less llength_eq_0 mem_Collect_eq zero_enat_def)

lemma Inf_llist_imp_all_index: ‹x ∈ Inf_llist Xs ⟹ ∀i. enat i < llength Xs ⟶ x ∈ lnth Xs i›
  unfolding Inf_llist_def by blast

lemma all_index_imp_Inf_llist: ‹∀i. enat i < llength Xs ⟶ x ∈ lnth Xs i ⟹ x ∈ Inf_llist Xs›
  unfolding Inf_llist_def by auto

lemma Inf_llist_LNil[simp]: ‹Inf_llist LNil = UNIV›
  unfolding Inf_llist_def by auto

lemma Inf_llist_LCons[simp]: ‹Inf_llist (LCons X Xs) = X ∩ Inf_llist Xs›
  unfolding Inf_llist_def
proof (intro subset_antisym subsetI)
  fix x
  assume ‹x ∈ (⋂i ∈ {i. enat i < llength (LCons X Xs)}. lnth (LCons X Xs) i)›
  then have ‹enat i < llength (LCons X Xs) ⟶ x ∈ lnth (LCons X Xs) i› for i
    by blast
  then have ‹x ∈ X ∧ (∀i. enat i < llength Xs ⟶ x ∈ lnth Xs i)›
    by (metis Suc_ile_eq iless_Suc_eq llength_LCons lnth_0 lnth_Suc_LCons zero_enat_def zero_le)
  then show ‹x ∈ X ∩ (⋂i ∈ {i. enat i < llength Xs}. lnth Xs i)›
    by blast
next
  fix x
  assume ‹x ∈ X ∩ ⋂ (lnth Xs ` {i. enat i < llength Xs})›
  then have ‹x ∈ X ∧ (∀i. enat i < llength Xs ⟶ x ∈ lnth Xs i)›
    by simp
  then have ‹∀i. enat i ≤ llength Xs ⟶ x ∈ lnth (LCons X Xs) i›
    by (metis Suc_diff_1 Suc_ile_eq lnth_0 lnth_Suc_LCons neq0_conv)
  then show ‹x ∈ ⋂ (lnth (LCons X Xs) ` {i. enat i < llength (LCons X Xs)})›
    by simp
qed

lemma lhd_subset_Inf_llist: ‹¬ lnull Xs ⟹ Inf_llist Xs ⊆ lhd Xs›
  by (cases Xs) simp_all

subsection ‹Infimum up-to›

definition Inf_upto_llist :: ‹'a set llist ⇒ enat ⇒ 'a set› where
  ‹Inf_upto_llist Xs j = (⋂i ∈ {i. enat i < llength Xs ∧ enat i ≤ j}. lnth Xs i)›

lemma Inf_upto_llist_eq_Inf_llist_ltake: ‹Inf_upto_llist Xs j = Inf_llist (ltake (eSuc j) Xs)›
  unfolding Inf_upto_llist_def Inf_llist_def
  by (smt (verit, best) Collect_cong Sup.SUP_cong iless_Suc_eq less_llength_ltake lnth_ltake
      mem_Collect_eq)

lemma Inf_upto_llist_enat_0[simp]:
  ‹Inf_upto_llist Xs (enat 0) = (if lnull Xs then UNIV else lhd Xs)›
  unfolding Inf_upto_llist_def image_def
  by (cases ‹lnull Xs›) (auto simp: lhd_conv_lnth enat_0 enat_0_iff)

lemma Inf_upto_llist_Suc[simp]:
  ‹Inf_upto_llist Xs (enat (Suc j)) =
   Inf_upto_llist Xs (enat j) ∩ (if enat (Suc j) < llength Xs then lnth Xs (Suc j) else UNIV)›
  unfolding Inf_upto_llist_def image_def by (auto intro: le_SucI elim: le_SucE)

lemma Inf_upto_llist_infinity[simp]: ‹Inf_upto_llist Xs ∞ = Inf_llist Xs›
  unfolding Inf_upto_llist_def Inf_llist_def by simp

lemma Inf_upto_llist_0[simp]: ‹Inf_upto_llist Xs 0 = (if lnull Xs then UNIV else lhd Xs)›
  unfolding zero_enat_def by (rule Inf_upto_llist_enat_0)

lemma Inf_upto_llist_eSuc[simp]:
  ‹Inf_upto_llist Xs (eSuc j) =
   (case j of
      enat k ⇒ Inf_upto_llist Xs (enat (Suc k))
    | ∞ ⇒ Inf_llist Xs)›
  by (auto simp: eSuc_enat split: enat.split)

lemma Inf_upto_llist_anti[simp]: ‹j ≤ k ⟹ Inf_upto_llist Xs k ⊆ Inf_upto_llist Xs j›
  unfolding Inf_upto_llist_def by auto

lemma Inf_llist_subset_Inf_upto_llist: ‹Inf_llist Xs ⊆ Inf_upto_llist Xs j›
  unfolding Inf_llist_def Inf_upto_llist_def by auto

lemma elem_Inf_llist_imp_Inf_upto_llist:
  ‹x ∈ Inf_llist Xs ⟹ x ∈ Inf_upto_llist Xs (enat j)›
  unfolding Inf_llist_def Inf_upto_llist_def by blast

lemma Inf_upto_llist_subset_lnth: ‹j < llength Xs ⟹ Inf_upto_llist Xs j ⊆ lnth Xs j›
  unfolding Inf_upto_llist_def by auto

lemma Inf_llist_imp_Inf_upto_llist:
  assumes ‹X ⊆ Inf_llist Xs›
  shows ‹X ⊆ Inf_upto_llist Xs (enat k)›
  using assms elem_Inf_llist_imp_Inf_upto_llist by fast

subsection ‹Limsup›

definition Limsup_llist :: ‹'a set llist ⇒ 'a set› where
  ‹Limsup_llist Xs =
   (⋂i ∈ {i. enat i < llength Xs}. ⋃j ∈ {j. i ≤ j ∧ enat j < llength Xs}. lnth Xs j)›

lemma Limsup_llist_LNil[simp]: ‹Limsup_llist LNil = UNIV›
  unfolding Limsup_llist_def by simp

lemma Limsup_llist_LCons:
  ‹Limsup_llist (LCons X Xs) = (if lnull Xs then X else Limsup_llist Xs)› (is ‹?lhs = ?rhs›)
proof (cases "lnull Xs")
  case nnull: False
  show ?thesis
  proof
    {
      fix x
      assume ‹∀i. enat i ≤ llength Xs ⟶ (∃j ≥ i. enat j ≤ llength Xs ∧ x ∈ lnth (LCons X Xs) j)›
      then have ‹∀i. enat i < llength Xs ⟶ (∃j ≥ i. enat j < llength Xs ∧ x ∈ lnth Xs j)›
        by (metis Suc_ile_eq Suc_le_D Suc_le_mono lnth_Suc_LCons)
    }
    then show ‹?lhs ⊆ ?rhs›
      by (auto simp: Limsup_llist_def nnull)

    {
      fix x
      assume ‹∀i. enat i < llength Xs ⟶ (∃j ≥ i. enat j < llength Xs ∧ x ∈ lnth Xs j)›
      then have ‹∀i. enat i ≤ llength Xs ⟶
          (∃j ≥ i. enat j ≤ llength Xs ∧ x ∈ lnth (LCons X Xs) j)›
        by (metis Suc_ile_eq Suc_le_D iless_Suc_eq llength_LCons lnth_Suc_LCons nat_le_linear
            nnull not_less_eq_eq not_lnull_conv zero_enat_def zero_le)
    }
    then show "?rhs ⊆ ?lhs"
      by (auto simp: Limsup_llist_def nnull)
  qed
qed (simp add: Limsup_llist_def enat_0_iff(1))

lemma lfinite_Limsup_llist: ‹lfinite Xs ⟹ Limsup_llist Xs = (if lnull Xs then UNIV else llast Xs)›
proof (induction rule: lfinite_induct)
  case (LCons xs)
  then obtain y ys where xs: ‹xs = LCons y ys›
    by (meson not_lnull_conv)
  show ?case
    unfolding xs by (simp add: Limsup_llist_LCons LCons.IH[unfolded xs, simplified] llast_LCons)
qed (simp add: Limsup_llist_def)

lemma Limsup_llist_ltl: ‹¬ lnull (ltl Xs) ⟹ Limsup_llist Xs = Limsup_llist (ltl Xs)›
  by (metis Limsup_llist_LCons lhd_LCons_ltl lnull_ltlI)

lemma Inf_llist_subset_Limsup_llist: ‹Inf_llist Xs ⊆ Limsup_llist Xs›
  unfolding Limsup_llist_def Inf_llist_def by fast

lemma image_Limsup_llist_subset: ‹f ` Limsup_llist Ns ⊆ Limsup_llist (lmap ((`) f) Ns)›
  unfolding Limsup_llist_def by fastforce

lemma Limsup_llist_imp_exists_index:
  assumes ‹¬ lnull Xs›
  shows ‹x ∈ Limsup_llist Xs ⟹ ∃i. enat i < llength Xs ∧ x ∈ lnth Xs i›
  unfolding Limsup_llist_def using assms
  by simp (metis i0_less llength_eq_0 zero_enat_def)

lemma finite_subset_Limsup_llist_imp_exists_index:
  assumes
    nnil: ‹¬ lnull Xs› and
    fin: ‹finite X› and
    in_sup: ‹X ⊆ Limsup_llist Xs›
  shows ‹∀i. enat i < llength Xs ⟶ X ⊆ (⋃j ∈ {j. i ≤ j ∧ enat j < llength Xs}. lnth Xs j)›
  using assms unfolding Limsup_llist_def by blast

lemma Limsup_llist_lmap_image:
  assumes f_inj: ‹inj_on f (Inf_llist (lmap g xs))›
  shows ‹Limsup_llist (lmap (λx. f ` g x) xs) = f ` Limsup_llist (lmap g xs)› (is ‹?lhs = ?rhs›)
  oops

lemma Limsup_llist_lmap_union:
  assumes ‹∀x ∈ lset xs. ∀y ∈ lset xs. g x ∩ h y = {}›
  shows ‹Limsup_llist (lmap (λx. g x ∪ h x) xs) =
    Limsup_llist (lmap g xs) ∪ Limsup_llist (lmap h xs)› (is ‹?lhs = ?rhs›)
proof (intro equalityI subsetI)
  fix x
  assume x_in: ‹x ∈ ?lhs›
  then have ‹∀i. enat i < llength xs ⟶ (∃j ≥ i. enat j < llength xs ∧
      (x ∈ g (lnth xs j) ∨ x ∈ h (lnth xs j)))›
    unfolding Limsup_llist_def by auto
  then have ‹(∀i'. enat i' < llength xs ⟶ (∃j ≥ i'. enat j < llength xs ∧ x ∈ g (lnth xs j)))
     ∨ (∀i'. enat i' < llength xs ⟶ (∃j ≥ i'. enat j < llength xs ∧ x ∈ h (lnth xs j)))›
    using assms[unfolded disjoint_iff_not_equal] by (metis in_lset_conv_lnth)
  then show ‹x ∈ ?rhs›
    unfolding Limsup_llist_def by simp
next
  fix x
  show ‹x ∈ ?rhs ⟹ x ∈ ?lhs›
    using assms unfolding Limsup_llist_def by auto
qed

lemma Limsup_set_filter_commute:
  assumes ‹¬ lnull Xs›
  shows ‹Limsup_llist (lmap (λX. {x ∈ X. p x}) Xs) = {x ∈ Limsup_llist Xs. p x}› (is ‹?lhs = ?rhs›)
proof (intro equalityI subsetI)
  fix x
  assume ‹x ∈ ?lhs›
  then show ‹x ∈ ?rhs›
    unfolding Limsup_llist_def
    by simp (metis assms i0_less llength_eq_0 zero_enat_def)
qed (simp add: Limsup_llist_def)

subsection ‹Limsup up-to›

definition Limsup_upto_llist :: ‹'a set llist ⇒ enat ⇒ 'a set› where
  ‹Limsup_upto_llist Xs k =
   (⋂i ∈ {i. enat i < llength Xs ∧ enat i ≤ k}.
      ⋃j ∈ {j. i ≤ j ∧ enat j < llength Xs ∧ enat j ≤ k}. lnth Xs j)›

lemma Limsup_upto_llist_eq_Limsup_llist_ltake:
  ‹Limsup_upto_llist Xs j = Limsup_llist (ltake (eSuc j) Xs)›
  unfolding Limsup_upto_llist_def Limsup_llist_def
  by (smt Collect_cong Sup.SUP_cong iless_Suc_eq lnth_ltake less_llength_ltake mem_Collect_eq)

lemma Limsup_upto_llist_enat[simp]:
  ‹Limsup_upto_llist Xs (enat k) =
   (if enat k < llength Xs then lnth Xs k else if lnull Xs then UNIV else llast Xs)›
proof (cases ‹enat k < llength Xs›)
  case True
  then show ?thesis
    unfolding Limsup_upto_llist_def by force
next
  case k_ge: False
  show ?thesis
proof (cases ‹lnull Xs›)
  case nil: True
  then show ?thesis
    unfolding Limsup_upto_llist_def by simp
next
  case nnil: False
  then obtain j where
    j: ‹eSuc (enat j) = llength Xs›
    using k_ge by (metis eSuc_enat_iff enat_ile le_less_linear lhd_LCons_ltl llength_LCons)

  have fin: ‹lfinite Xs›
    using k_ge not_lfinite_llength by fastforce
  have le_k: ‹enat i < llength Xs ∧ i ≤ k ⟷ enat i < llength Xs› for i
    using k_ge linear order_le_less_subst2 by fastforce
  have ‹Limsup_upto_llist Xs (enat k) = llast Xs›
    using j nnil lfinite_Limsup_llist[OF fin] nnil
    unfolding Limsup_upto_llist_def Limsup_llist_def using llast_conv_lnth[OF j[symmetric]]
    by (simp add: le_k)
  then show ?thesis
    using k_ge nnil by simp
  qed
qed

lemma Limsup_upto_llist_infinity[simp]: ‹Limsup_upto_llist Xs ∞ = Limsup_llist Xs›
  unfolding Limsup_upto_llist_def Limsup_llist_def by simp

lemma Limsup_upto_llist_0[simp]:
  ‹Limsup_upto_llist Xs 0 = (if lnull Xs then UNIV else lhd Xs)›
  unfolding Limsup_upto_llist_def image_def
  by (simp add: enat_0[symmetric]) (simp add: enat_0 lnth_0_conv_lhd)

lemma Limsup_upto_llist_eSuc[simp]:
  ‹Limsup_upto_llist Xs (eSuc j) =
   (case j of
      enat k ⇒ Limsup_upto_llist Xs (enat (Suc k))
    | ∞ ⇒ Limsup_llist Xs)›
  by (auto simp: eSuc_enat split: enat.split)

lemma Liminf_upto_llist_imp_elem_Limsup_llist:
  assumes ‹∃i < llength Xs. ∀j ≥ i. j < llength Xs ⟶ x ∈ Limsup_upto_llist Xs (enat j)›
  shows ‹x ∈ Limsup_llist Xs›
  using assms by (simp add: Limsup_llist_def Limsup_upto_llist_def)
    (metis dual_order.strict_implies_order enat_iless enat_less_imp_le enat_ord_simps(1) not_less)

end