Theory Ordered_Resolution_Prover.Lazy_List_Liminf

(*  Title:       Supremum and Liminf of Lazy Lists
    Author:      Jasmin Blanchette <j.c.blanchette at vu.nl>, 2014, 2017, 2020
    Author:      Dmitriy Traytel <traytel at inf.ethz.ch>, 2014
    Maintainer:  Jasmin Blanchette <j.c.blanchette at vu.nl>
*)

section ‹Supremum and Liminf of Lazy Lists›

theory Lazy_List_Liminf
  imports Coinductive.Coinductive_List
begin

text ‹
Lazy lists, as defined in the \emph{Archive of Formal Proofs}, provide finite and infinite lists in
one type, defined coinductively. The present theory introduces the concept of the union of all
elements of a lazy list of sets and the limit of such a lazy list. The definitions are stated more
generally in terms of lattices. The basis for this theory is Section 4.1 (``Theorem Proving
Processes'') of Bachmair and Ganzinger's chapter.
›


subsection ‹Library›

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


subsection ‹Supremum›

definition Sup_llist :: "'a set llist ⇒ 'a set" where
  "Sup_llist Xs = (⋃i ∈ {i. enat i < llength Xs}. lnth Xs i)"

lemma lnth_subset_Sup_llist: "enat i < llength Xs ⟹ lnth Xs i ⊆ Sup_llist Xs"
  unfolding Sup_llist_def by auto

lemma Sup_llist_imp_exists_index: "x ∈ Sup_llist Xs ⟹ ∃i. enat i < llength Xs ∧ x ∈ lnth Xs i"
  unfolding Sup_llist_def by auto

lemma exists_index_imp_Sup_llist: "enat i < llength Xs ⟹ x ∈ lnth Xs i ⟹ x ∈ Sup_llist Xs"
  unfolding Sup_llist_def by auto

lemma Sup_llist_LNil[simp]: "Sup_llist LNil = {}"
  unfolding Sup_llist_def by auto

lemma Sup_llist_LCons[simp]: "Sup_llist (LCons X Xs) = X ∪ Sup_llist Xs"
  unfolding Sup_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 obtain i where len: "enat i < llength (LCons X Xs)" and nth: "x ∈ lnth (LCons X Xs) i"
    by blast
  from nth have "x ∈ X ∨ i > 0 ∧ x ∈ lnth Xs (i - 1)"
    by (metis lnth_LCons' neq0_conv)
  then have "x ∈ X ∨ (∃i. enat i < llength Xs ∧ x ∈ lnth Xs i)"
    by (metis len Suc_pred' eSuc_enat iless_Suc_eq less_irrefl llength_LCons not_less order_trans)
  then show "x ∈ X ∪ (⋃i ∈ {i. enat i < llength Xs}. lnth Xs i)"
    by blast
qed ((auto)[], metis i0_lb lnth_0 zero_enat_def, metis Suc_ile_eq lnth_Suc_LCons)

lemma lhd_subset_Sup_llist: "¬ lnull Xs ⟹ lhd Xs ⊆ Sup_llist Xs"
  by (cases Xs) simp_all


subsection ‹Supremum up-to›

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

lemma Sup_upto_llist_eq_Sup_llist_ltake: "Sup_upto_llist Xs j = Sup_llist (ltake (eSuc j) Xs)"
  unfolding Sup_upto_llist_def Sup_llist_def
  by (smt (verit) Collect_cong Sup.SUP_cong iless_Suc_eq lnth_ltake less_llength_ltake mem_Collect_eq)

lemma Sup_upto_llist_enat_0[simp]:
  "Sup_upto_llist Xs (enat 0) = (if lnull Xs then {} else lhd Xs)"
proof (cases "lnull Xs")
  case True
  then show ?thesis
    unfolding Sup_upto_llist_def by auto
next
  case False
  show ?thesis
    unfolding Sup_upto_llist_def image_def by (simp add: lhd_conv_lnth enat_0 enat_0_iff)
qed

lemma Sup_upto_llist_Suc[simp]:
  "Sup_upto_llist Xs (enat (Suc j)) =
   Sup_upto_llist Xs (enat j) ∪ (if enat (Suc j) < llength Xs then lnth Xs (Suc j) else {})"
  unfolding Sup_upto_llist_def image_def by (auto intro: le_SucI elim: le_SucE)

lemma Sup_upto_llist_infinity[simp]: "Sup_upto_llist Xs ∞ = Sup_llist Xs"
  unfolding Sup_upto_llist_def Sup_llist_def by simp

lemma Sup_upto_llist_0[simp]: "Sup_upto_llist Xs 0 = (if lnull Xs then {} else lhd Xs)"
  unfolding zero_enat_def by (rule Sup_upto_llist_enat_0)

lemma Sup_upto_llist_eSuc[simp]:
  "Sup_upto_llist Xs (eSuc j) =
   (case j of
      enat k ⇒ Sup_upto_llist Xs (enat (Suc k))
    | ∞ ⇒ Sup_llist Xs)"
  by (auto simp: eSuc_enat split: enat.split)

lemma Sup_upto_llist_mono[simp]: "j ≤ k ⟹ Sup_upto_llist Xs j ⊆ Sup_upto_llist Xs k"
  unfolding Sup_upto_llist_def by auto

lemma Sup_upto_llist_subset_Sup_llist: "Sup_upto_llist Xs j ⊆ Sup_llist Xs"
  unfolding Sup_llist_def Sup_upto_llist_def by auto

lemma elem_Sup_llist_imp_Sup_upto_llist:
  "x ∈ Sup_llist Xs ⟹ ∃j < llength Xs. x ∈ Sup_upto_llist Xs (enat j)"
  unfolding Sup_llist_def Sup_upto_llist_def by blast

lemma lnth_subset_Sup_upto_llist: "j < llength Xs ⟹ lnth Xs j ⊆ Sup_upto_llist Xs j"
  unfolding Sup_upto_llist_def by auto

lemma finite_Sup_llist_imp_Sup_upto_llist:
  assumes "finite X" and "X ⊆ Sup_llist Xs"
  shows "∃k. X ⊆ Sup_upto_llist Xs (enat k)"
  using assms
proof induct
  case (insert x X)
  then have x: "x ∈ Sup_llist Xs" and X: "X ⊆ Sup_llist Xs"
    by simp+
  from x obtain k where k: "x ∈ Sup_upto_llist Xs (enat k)"
    using elem_Sup_llist_imp_Sup_upto_llist by fast
  from X obtain k' where k': "X ⊆ Sup_upto_llist Xs (enat k')"
    using insert.hyps(3) by fast
  have "insert x X ⊆ Sup_upto_llist Xs (max k k')"
    using k k' by (metis (mono_tags) Sup_upto_llist_mono enat_ord_simps(1) insert_subset
      max.cobounded1 max.cobounded2 subset_iff)
  then show ?case
    by fast
qed simp


subsection ‹Liminf›

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

lemma Liminf_llist_LNil[simp]: "Liminf_llist LNil = {}"
  unfolding Liminf_llist_def by simp

lemma Liminf_llist_LCons:
  "Liminf_llist (LCons X Xs) = (if lnull Xs then X else Liminf_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 ≤ j ∧ enat j ≤ llength Xs ⟶ x ∈ lnth (LCons X Xs) j)"
      then have "∃i. enat (Suc i) ≤ llength Xs
        ∧ (∀j. Suc i ≤ j ∧ enat j ≤ llength Xs ⟶ x ∈ lnth (LCons X Xs) j)"
        by (cases "llength Xs",
            metis not_lnull_conv[THEN iffD1, OF nnull] Suc_le_D eSuc_enat eSuc_ile_mono
              llength_LCons not_less_eq_eq zero_enat_def zero_le,
            metis Suc_leD enat_ord_code(3))
      then have "∃i. enat i < llength Xs ∧ (∀j. i ≤ j ∧ enat j < llength Xs ⟶ x ∈ lnth Xs j)"
        by (metis Suc_ile_eq Suc_n_not_le_n lift_Suc_mono_le lnth_Suc_LCons nat_le_linear)
    }
    then show "?lhs ⊆ ?rhs"
      by (simp add: Liminf_llist_def nnull) (rule subsetI, simp)

    {
      fix x
      assume "∃i. enat i < llength Xs ∧ (∀j. i ≤ j ∧ enat j < llength Xs ⟶ x ∈ lnth Xs j)"
      then obtain i where
        i: "enat i < llength Xs" and
        j: "∀j. i ≤ j ∧ enat j < llength Xs ⟶ x ∈ lnth Xs j"
        by blast

      have "enat (Suc i) ≤ llength Xs"
        using i by (simp add: Suc_ile_eq)
      moreover have "∀j. Suc i ≤ j ∧ enat j ≤ llength Xs ⟶ x ∈ lnth (LCons X Xs) j"
        using Suc_ile_eq Suc_le_D j by force
      ultimately have "∃i. enat i ≤ llength Xs ∧ (∀j. i ≤ j ∧ enat j ≤ llength Xs ⟶
        x ∈ lnth (LCons X Xs) j)"
        by blast
    }
    then show "?rhs ⊆ ?lhs"
      by (simp add: Liminf_llist_def nnull) (rule subsetI, simp)
  qed
qed (simp add: Liminf_llist_def enat_0_iff(1))

lemma lfinite_Liminf_llist: "lfinite Xs ⟹ Liminf_llist Xs = (if lnull Xs then {} 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: Liminf_llist_LCons LCons.IH[unfolded xs, simplified] llast_LCons)
qed (simp add: Liminf_llist_def)

lemma Liminf_llist_ltl: "¬ lnull (ltl Xs) ⟹ Liminf_llist Xs = Liminf_llist (ltl Xs)"
  by (metis Liminf_llist_LCons lhd_LCons_ltl lnull_ltlI)

lemma Liminf_llist_subset_Sup_llist: "Liminf_llist Xs ⊆ Sup_llist Xs"
  unfolding Liminf_llist_def Sup_llist_def by fast

lemma image_Liminf_llist_subset: "f ` Liminf_llist Ns ⊆ Liminf_llist (lmap ((`) f) Ns)"
  unfolding Liminf_llist_def by auto

lemma Liminf_llist_imp_exists_index:
  "x ∈ Liminf_llist Xs ⟹ ∃i. enat i < llength Xs ∧ x ∈ lnth Xs i"
  unfolding Liminf_llist_def by auto

lemma not_Liminf_llist_imp_exists_index:
  "¬ lnull Xs ⟹ x ∉ Liminf_llist Xs ⟹ enat i < llength Xs ⟹
   (∃j. i ≤ j ∧ enat j < llength Xs ∧ x ∉ lnth Xs j)"
  unfolding Liminf_llist_def by auto

lemma finite_subset_Liminf_llist_imp_exists_index:
  assumes
    nnil: "¬ lnull Xs" and
    fin: "finite X" and
    in_lim: "X ⊆ Liminf_llist Xs"
  shows "∃i. enat i < llength Xs ∧ X ⊆ (⋂j ∈ {j. i ≤ j ∧ enat j < llength Xs}. lnth Xs j)"
proof -
  show ?thesis
  proof (cases "X = {}")
    case True
    then show ?thesis
      using nnil by (auto intro: exI[of _ 0] simp: zero_enat_def[symmetric])
  next
    case nemp: False

    have in_lim':
      "∀x ∈ X. ∃i. enat i < llength Xs ∧ x ∈ (⋂j ∈ {j. i ≤ j ∧ enat j < llength Xs}. lnth Xs j)"
      using in_lim[unfolded Liminf_llist_def] in_mono by fastforce
    obtain i_of where
      i_of_lt: "∀x ∈ X. enat (i_of x) < llength Xs" and
      in_inter: "∀x ∈ X. x ∈ (⋂j ∈ {j. i_of x ≤ j ∧ enat j < llength Xs}. lnth Xs j)"
      using bchoice[OF in_lim'] by blast

    define i_max where
      "i_max = Max (i_of ` X)"

    have "i_max ∈ i_of ` X"
      by (simp add: fin i_max_def nemp)
    then obtain x_max where
      x_max_in: "x_max ∈ X" and
      i_max_is: "i_max = i_of x_max"
      unfolding i_max_def by blast
    have le_i_max: "∀x ∈ X. i_of x ≤ i_max"
      unfolding i_max_def by (simp add: fin)
    have "enat i_max < llength Xs"
      using i_of_lt x_max_in i_max_is by auto
    moreover have "X ⊆ (⋂j ∈ {j. i_max ≤ j ∧ enat j < llength Xs}. lnth Xs j)"
    proof
      fix x
      assume x_in: "x ∈ X"
      then have x_in_inter: "x ∈ (⋂j ∈ {j. i_of x ≤ j ∧ enat j < llength Xs}. lnth Xs j)"
        using in_inter by auto
      moreover have "{j. i_max ≤ j ∧ enat j < llength Xs}
        ⊆ {j. i_of x ≤ j ∧ enat j < llength Xs}"
        using x_in le_i_max by auto
      ultimately show "x ∈ (⋂j ∈ {j. i_max ≤ j ∧ enat j < llength Xs}. lnth Xs j)"
        by auto
    qed
    ultimately show ?thesis
      by auto
  qed
qed

lemma Liminf_llist_lmap_image:
  assumes f_inj: "inj_on f (Sup_llist (lmap g xs))"
  shows "Liminf_llist (lmap (λx. f ` g x) xs) = f ` Liminf_llist (lmap g xs)" (is "?lhs = ?rhs")
proof
  show "?lhs ⊆ ?rhs"
  proof
    fix x
    assume "x ∈ Liminf_llist (lmap (λx. f ` g x) xs)"
    then obtain i where
      i_lt: "enat i < llength xs" and
      x_in_fgj: "∀j. i ≤ j ⟶ enat j < llength xs ⟶ x ∈ f ` g (lnth xs j)"
      unfolding Liminf_llist_def by auto

    have ex_in_gi: "∃y. y ∈ g (lnth xs i) ∧ x = f y"
      using f_inj i_lt x_in_fgj unfolding inj_on_def Sup_llist_def by auto
    have "∃y. ∀j. i ≤ j ⟶ enat j < llength xs ⟶ y ∈ g (lnth xs j) ∧ x = f y"
      apply (rule exI[of _ "SOME y. y ∈ g (lnth xs i) ∧ x = f y"])
      using someI_ex[OF ex_in_gi] x_in_fgj f_inj i_lt x_in_fgj unfolding inj_on_def Sup_llist_def
      by simp (metis (no_types, lifting) imageE)
    then show "x ∈ f ` Liminf_llist (lmap g xs)"
      using i_lt unfolding Liminf_llist_def by auto
  qed
next
  show "?rhs ⊆ ?lhs"
    using image_Liminf_llist_subset[of f "lmap g xs", unfolded llist.map_comp] by auto
qed

lemma Liminf_llist_lmap_union:
  assumes "∀x ∈ lset xs. ∀Y ∈ lset xs. g x ∩ h Y = {}"
  shows "Liminf_llist (lmap (λx. g x ∪ h x) xs) =
    Liminf_llist (lmap g xs) ∪ Liminf_llist (lmap h xs)" (is "?lhs = ?rhs")
proof (intro equalityI subsetI)
  fix x
  assume x_in: "x ∈ ?lhs"
  then obtain i where
    i_lt: "enat i < llength xs" and
    j: "∀j. i ≤ j ∧ enat j < llength xs ⟶ x ∈ g (lnth xs j) ∨ x ∈ h (lnth xs j)"
    using x_in[unfolded Liminf_llist_def, simplified] by blast

  then have "(∃i'. enat i' < llength xs ∧ (∀j. i' ≤ j ∧ enat j < llength xs ⟶ x ∈ g (lnth xs j)))
     ∨ (∃i'. enat i' < llength xs ∧ (∀j. i' ≤ j ∧ 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 Liminf_llist_def by simp
next
  fix x
  show "x ∈ ?rhs ⟹ x ∈ ?lhs"
    using assms unfolding Liminf_llist_def by auto
qed

lemma Liminf_set_filter_commute:
  "Liminf_llist (lmap (λX. {x ∈ X. p x}) Xs) = {x ∈ Liminf_llist Xs. p x}"
  unfolding Liminf_llist_def by force


subsection ‹Liminf up-to›

definition Liminf_upto_llist :: "'a set llist ⇒ enat ⇒ 'a set" where
  "Liminf_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 Liminf_upto_llist_eq_Liminf_llist_ltake:
  "Liminf_upto_llist Xs j = Liminf_llist (ltake (eSuc j) Xs)"
  unfolding Liminf_upto_llist_def Liminf_llist_def
  by (auto simp add: lnth_ltake less_llength_ltake)

lemma Liminf_upto_llist_enat[simp]:
  "Liminf_upto_llist Xs (enat k) =
   (if enat k < llength Xs then lnth Xs k else if lnull Xs then {} else llast Xs)"
proof (cases "enat k < llength Xs")
  case True
  then show ?thesis
    unfolding Liminf_upto_llist_def by force
next
  case k_ge: False
  show ?thesis
proof (cases "lnull Xs")
  case nil: True
  then show ?thesis
    unfolding Liminf_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 "Liminf_upto_llist Xs (enat k) = llast Xs"
    using j nnil lfinite_Liminf_llist[OF fin] nnil
    unfolding Liminf_upto_llist_def Liminf_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 Liminf_upto_llist_infinity[simp]: "Liminf_upto_llist Xs ∞ = Liminf_llist Xs"
  unfolding Liminf_upto_llist_def Liminf_llist_def by simp

lemma Liminf_upto_llist_0[simp]:
  "Liminf_upto_llist Xs 0 = (if lnull Xs then {} else lhd Xs)"
  unfolding Liminf_upto_llist_def image_def
  by (simp add: enat_0[symmetric]) (simp add: enat_0 lnth_0_conv_lhd)

lemma Liminf_upto_llist_eSuc[simp]:
  "Liminf_upto_llist Xs (eSuc j) =
   (case j of
      enat k ⇒ Liminf_upto_llist Xs (enat (Suc k))
    | ∞ ⇒ Liminf_llist Xs)"
  by (auto simp: eSuc_enat split: enat.split)

lemma elem_Liminf_llist_imp_Liminf_upto_llist:
  "x ∈ Liminf_llist Xs ⟹
   ∃i < llength Xs. ∀j. i ≤ j ∧ j < llength Xs ⟶ x ∈ Liminf_upto_llist Xs (enat j)"
  unfolding Liminf_llist_def Liminf_upto_llist_def using enat_ord_simps(1) by force

end