Theory Min_Max_Least_Greatest_FSet

theory Min_Max_Least_Greatest_FSet
  imports
    Min_Max_Least_Greatest_Set
    "HOL-Library.FSet"
begin

section ‹Minimal and maximal elements›

definition is_minimal_in_fset_wrt :: "('a ⇒ 'a ⇒ bool) ⇒ 'a fset ⇒ 'a ⇒ bool" where
  "transp_on (fset X) R ⟹ asymp_on (fset X) R ⟹
    is_minimal_in_fset_wrt R X = is_minimal_in_set_wrt R (fset X)"

definition is_maximal_in_fset_wrt :: "('a ⇒ 'a ⇒ bool) ⇒ 'a fset ⇒ 'a ⇒ bool" where
  "transp_on (fset X) R ⟹ asymp_on (fset X) R ⟹
    is_maximal_in_fset_wrt R X = is_maximal_in_set_wrt R (fset X)"

context
  fixes X R
  assumes
    trans: "transp_on (fset X) R" and
    asym: "asymp_on (fset X) R"
begin


subsection ‹Conversions›

lemma is_minimal_in_fset_wrt_iff:
  "is_minimal_in_fset_wrt R X x ⟷ x |∈| X ∧ fBall X (λy. y ≠ x ⟶ ¬ R y x)"
  using is_minimal_in_set_wrt_iff[OF trans asym]
  using is_minimal_in_fset_wrt_def[OF trans asym]
  by simp

lemma is_maximal_in_fset_wrt_iff:
  "is_maximal_in_fset_wrt R X x ⟷ x |∈| X ∧ fBall X (λy. y ≠ x ⟶ ¬ R x y)"
  using is_maximal_in_set_wrt_iff[OF trans asym]
  using is_maximal_in_fset_wrt_def[OF trans asym]
  by simp


subsection ‹Existence›

lemma ex_minimal_in_fset_wrt:
  "X ≠ {||} ⟹ ∃m. is_minimal_in_fset_wrt R X m"
  using trans asym ex_minimal_in_set_wrt[of "fset X" R] is_minimal_in_fset_wrt_def
  by (metis all_not_fin_conv empty_iff finite_fset)

lemma ex_maximal_in_fset_wrt:
  "X ≠ {||} ⟹ ∃m. is_maximal_in_fset_wrt R X m"
  using trans asym ex_maximal_in_set_wrt[of "fset X" R] is_maximal_in_fset_wrt_def
  by (metis all_not_fin_conv empty_iff finite_fset)

end


subsection ‹Non-existence›

lemma not_is_minimal_in_fset_wrt_fempty[simp]: "⋀R x. ¬ is_minimal_in_fset_wrt R {||} x"
  using is_minimal_in_fset_wrt_iff[of "{||}"]
  by (simp add: transp_on_def asymp_on_def)

lemma not_is_maximal_in_fset_wrt_fempty[simp]: "⋀R x. ¬ is_maximal_in_fset_wrt R {||} x"
  using is_maximal_in_fset_wrt_iff[of "{||}"]
  by (simp add: transp_on_def asymp_on_def)


subsection ‹Miscellaneous›

lemma is_minimal_in_fset_wrt_ffilter_iff:
  assumes
    tran: "transp_on (fset (ffilter P X)) R" and
    asym: "asymp_on (fset (ffilter P X)) R"
  shows "is_minimal_in_fset_wrt R (ffilter P X) x ⟷
    (x |∈| X ∧ P x ∧ fBall (X - {|x|}) (λy. P y ⟶ ¬ R y x))"
proof -
  have "is_minimal_in_fset_wrt R (ffilter P X) x ⟷ is_minimal_in_set_wrt R ({y ∈ fset X. P y}) x"
    using is_minimal_in_fset_wrt_iff[OF tran asym]
    using is_minimal_in_set_wrt_iff[OF tran asym]
    by (simp only: ffilter.rep_eq Set.filter_def)
  also have "… ⟷ x |∈| X ∧ P x ∧ (∀y∈fset X - {x}. P y ⟶ ¬ R y x)"
  proof (rule is_minimal_in_set_wrt_filter_iff)
    show "transp_on {y. y |∈| X ∧ P y} R"
      using tran ffilter.rep_eq Set.filter_def by metis
  next
    show "asymp_on {y. y |∈| X ∧ P y} R"
      using asym ffilter.rep_eq Set.filter_def by metis
  qed
  finally show ?thesis
    by simp
qed

lemma is_minimal_in_fset_wrt_finsertI:
  assumes trans: "transp_on (fset (finsert y X)) R" and asym: "asymp_on (fset (finsert y X)) R"
  shows "R y x ⟹ is_minimal_in_fset_wrt R X x ⟹ is_minimal_in_fset_wrt R (finsert y X) y"
  using trans asym is_minimal_in_set_wrt_insertI[of _ "fset _", folded fset_simps]
  by (smt (verit) asymp_on_def finsertCI finsertE is_minimal_in_fset_wrt_iff transp_on_def)


section ‹Least and greatest elements›

definition is_least_in_fset_wrt :: "('a ⇒ 'a ⇒ bool) ⇒ 'a fset ⇒ 'a ⇒ bool" where
  "transp_on (fset X) R ⟹ asymp_on (fset X) R ⟹ totalp_on (fset X) R ⟹
    is_least_in_fset_wrt R X = is_least_in_set_wrt R (fset X)"

definition is_greatest_in_fset_wrt :: "('a ⇒ 'a ⇒ bool) ⇒ 'a fset ⇒ 'a ⇒ bool" where
  "transp_on (fset X) R ⟹ asymp_on (fset X) R ⟹ totalp_on (fset X) R ⟹
    is_greatest_in_fset_wrt R X = is_greatest_in_set_wrt R (fset X)"

context
  fixes X R
  assumes
    trans: "transp_on (fset X) R" and
    asym: "asymp_on (fset X) R" and
    tot: "totalp_on (fset X) R"
begin

subsection ‹Conversions›

lemma is_least_in_fset_wrt_iff:
  "is_least_in_fset_wrt R X x ⟷ x |∈| X ∧ fBall X (λy. y ≠ x ⟶ R x y)"
  using is_least_in_set_wrt_iff[OF trans asym tot]
  using is_least_in_fset_wrt_def[OF trans asym tot]
  by simp

lemma is_greatest_in_fset_wrt_iff:
  "is_greatest_in_fset_wrt R X x ⟷ x |∈| X ∧ fBall X (λy. y ≠ x ⟶ R y x)"
  using is_greatest_in_set_wrt_iff[OF trans asym tot]
  using is_greatest_in_fset_wrt_def[OF trans asym tot]
  by simp

lemma is_minimal_in_fset_wrt_eq_is_least_in_fset_wrt:
  "is_minimal_in_fset_wrt R X = is_least_in_fset_wrt R X"
  using trans asym tot is_minimal_in_set_wrt_eq_is_least_in_set_wrt
  by (metis is_least_in_fset_wrt_def is_minimal_in_fset_wrt_def)

lemma is_maximal_in_fset_wrt_eq_is_greatest_in_fset_wrt:
  "is_maximal_in_fset_wrt R X = is_greatest_in_fset_wrt R X"
  using trans asym tot is_maximal_in_set_wrt_eq_is_greatest_in_set_wrt
  by (metis is_greatest_in_fset_wrt_def is_maximal_in_fset_wrt_def)


subsection ‹Uniqueness›

lemma Uniq_is_least_in_fset_wrt[intro]:
  "∃⇩≤⇩1x. is_least_in_fset_wrt R X x"
  using trans asym tot Uniq_is_least_in_set_wrt
  by (metis is_least_in_fset_wrt_def)

lemma Uniq_is_greatest_in_fset_wrt[intro]:
  "∃⇩≤⇩1x. is_greatest_in_fset_wrt R X x"
  using trans asym tot Uniq_is_greatest_in_set_wrt
  by (metis is_greatest_in_fset_wrt_def)


subsection ‹Existence›

lemma ex_least_in_fset_wrt:
  "X ≠ {||} ⟹ ∃x. is_least_in_fset_wrt R X x"
  using trans asym tot ex_least_in_set_wrt
  by (metis bot_fset.rep_eq finite_fset fset_cong is_least_in_fset_wrt_def)

lemma ex_greatest_in_fset_wrt:
  "X ≠ {||} ⟹ ∃x. is_greatest_in_fset_wrt R X x"
  using trans asym tot ex_greatest_in_set_wrt
  by (metis bot_fset.rep_eq finite_fset fset_cong is_greatest_in_fset_wrt_def)

lemma ex1_least_in_fset_wrt:
  "X ≠ {||} ⟹ ∃!x. is_least_in_fset_wrt R X x"
  using Uniq_is_least_in_fset_wrt ex_least_in_fset_wrt
  by (metis Uniq_def)

lemma ex1_greatest_in_fset_wrt:
  "X ≠ {||} ⟹ ∃!x. is_greatest_in_fset_wrt R X x"
  using Uniq_is_greatest_in_fset_wrt ex_greatest_in_fset_wrt
  by (metis Uniq_def)

end


subsection ‹Nonexistence›

lemma not_is_least_in_fset_wrt_fempty[simp]: "⋀R x. ¬ is_least_in_fset_wrt R {||} x"
  using is_least_in_fset_wrt_iff[of "{||}"]
  by (simp add: transp_on_def asymp_on_def)

lemma not_is_greatest_in_fset_wrt_fempty[simp]: "⋀R x. ¬ is_greatest_in_fset_wrt R {||} x"
  using is_greatest_in_fset_wrt_iff[of "{||}"]
  by (simp add: transp_on_def asymp_on_def)


subsection ‹Miscellaneous›

lemma is_least_in_ffilter_wrt_iff:
  assumes
    trans: "transp_on (fset (ffilter P X)) R" and
    asym: "asymp_on (fset (ffilter P X)) R" and
    tot: "totalp_on (fset (ffilter P X)) R"
  shows "is_least_in_fset_wrt R (ffilter P X) x ⟷
    (x |∈| X ∧ P x ∧ fBall X (λy. y ≠ x ⟶ P y ⟶ R x y))"
  unfolding is_least_in_fset_wrt_iff[OF trans asym tot] by auto

lemma is_least_in_ffilter_wrt_swap_predicate:
  assumes
    trans: "transp_on (fset X) R" and
    asym: "asymp_on (fset X) R" and
    tot: "totalp_on (fset X) R"
  assumes
    y_least: "is_least_in_fset_wrt R (ffilter P X) y" and
    same_on_prefix: "⋀x. x |∈| X ⟹ R⇧=⇧= x y ⟹ P x ⟷ Q x"
  shows "is_least_in_fset_wrt R (ffilter Q X) y"
proof -
  have "⋀P. fset (ffilter P X) ⊆ fset X"
    by simp

  hence
    linorder_wrt_P:
      "transp_on (fset (ffilter P X)) R"
      "asymp_on (fset (ffilter P X)) R"
      "totalp_on (fset (ffilter P X)) R" and
    linorder_wrt_Q:
      "transp_on (fset (ffilter Q X)) R"
      "asymp_on (fset (ffilter Q X)) R"
      "totalp_on (fset (ffilter Q X)) R"
    unfolding atomize_conj
    using trans asym tot by (metis transp_on_subset asymp_on_subset totalp_on_subset)

  have "y |∈| X" and "P y" and y_lt: "∀z |∈| X. z ≠ y ⟶ P z ⟶ R y z"
    using y_least unfolding is_least_in_ffilter_wrt_iff[OF linorder_wrt_P] by argo+

  show ?thesis
    unfolding is_least_in_ffilter_wrt_iff[OF linorder_wrt_Q]
  proof (intro conjI ballI impI)

    show "y |∈| X"
      using ‹y |∈| X› .

    show "Q y"
      using same_on_prefix[of y] ‹y |∈| X› ‹P y› by simp

    fix z
    assume "z |∈| X" and "z ≠ y" and "Q z"
    then show "R y z"
      using y_lt[rule_format, of z]
      using same_on_prefix[of z]
      by (metis ‹y |∈| X› sup2I1 tot totalp_onD)
  qed
qed
  
lemma ex_is_least_in_ffilter_wrt_iff:
  assumes
    trans: "transp_on (fset (ffilter P X)) R" and
    asym: "asymp_on (fset (ffilter P X)) R" and
    tot: "totalp_on (fset (ffilter P X)) R"
  shows "(∃x. is_least_in_fset_wrt R (ffilter P X) x) ⟷ (∃x |∈| X. P x)"
  by (metis asym bot_fset.rep_eq empty_iff ex_least_in_fset_wrt ffmember_filter
      is_least_in_fset_wrt_iff local.trans tot)


section ‹Hide stuff›

text ‹We restrict the public interface to ease future internal changes.›

hide_fact is_minimal_in_fset_wrt_def is_maximal_in_fset_wrt_def
hide_fact is_least_in_fset_wrt_def is_greatest_in_fset_wrt_def


section ‹Integration in type classes›

abbreviation (in order) is_minimal_in_fset where
  "is_minimal_in_fset ≡ is_minimal_in_fset_wrt (<)"

abbreviation (in order) is_maximal_in_fset where
  "is_maximal_in_fset ≡ is_maximal_in_fset_wrt (<)"

lemmas (in order) is_minimal_in_fset_iff =
  is_minimal_in_fset_wrt_iff[OF transp_on_less asymp_on_less]

lemmas (in order) is_maximal_in_fset_iff =
  is_maximal_in_fset_wrt_iff[OF transp_on_less asymp_on_less]

lemmas (in order) ex_minimal_in_fset =
  ex_minimal_in_fset_wrt[OF transp_on_less asymp_on_less]

lemmas (in order) ex_maximal_in_fset =
  ex_maximal_in_fset_wrt[OF transp_on_less asymp_on_less]

lemmas (in order) is_minimal_in_fset_ffilter_iff =
  is_minimal_in_fset_wrt_ffilter_iff[OF transp_on_less asymp_on_less]

lemmas (in order) is_minimal_in_fset_finsertI =
  is_minimal_in_fset_wrt_finsertI[OF transp_on_less asymp_on_less]


abbreviation (in linorder) is_least_in_fset where
  "is_least_in_fset ≡ is_least_in_fset_wrt (<)"

abbreviation (in linorder) is_greatest_in_fset where
  "is_greatest_in_fset ≡ is_greatest_in_fset_wrt (<)"

lemmas (in linorder) is_least_in_fset_iff =
  is_least_in_fset_wrt_iff[OF transp_on_less asymp_on_less totalp_on_less]

lemmas (in linorder) is_greatest_in_fset_iff =
  is_greatest_in_fset_wrt_iff[OF transp_on_less asymp_on_less totalp_on_less]

lemmas (in linorder) is_minimal_in_fset_eq_is_least_in_fset =
  is_minimal_in_fset_wrt_eq_is_least_in_fset_wrt[OF transp_on_less asymp_on_less totalp_on_less]

lemmas (in linorder) is_maximal_in_fset_eq_is_greatest_in_fset =
  is_maximal_in_fset_wrt_eq_is_greatest_in_fset_wrt[OF transp_on_less asymp_on_less totalp_on_less]

lemmas (in linorder) Uniq_is_least_in_fset[intro] =
  Uniq_is_least_in_fset_wrt[OF transp_on_less asymp_on_less totalp_on_less]

lemmas (in linorder) Uniq_is_greatest_in_fset[intro] =
  Uniq_is_greatest_in_fset_wrt[OF transp_on_less asymp_on_less totalp_on_less]

lemmas (in linorder) ex_least_in_fset =
  ex_least_in_fset_wrt[OF transp_on_less asymp_on_less totalp_on_less]

lemmas (in linorder) ex_greatest_in_fset =
  ex_greatest_in_fset_wrt[OF transp_on_less asymp_on_less totalp_on_less]

lemmas (in linorder) ex1_least_in_fset =
  ex1_least_in_fset_wrt[OF transp_on_less asymp_on_less totalp_on_less]

lemmas (in linorder) ex1_greatest_in_fset =
  ex1_greatest_in_fset_wrt[OF transp_on_less asymp_on_less totalp_on_less]

lemmas (in linorder) is_least_in_ffilter_iff =
  is_least_in_ffilter_wrt_iff[OF transp_on_less asymp_on_less totalp_on_less]

lemmas (in linorder) ex_is_least_in_ffilter_iff =
  ex_is_least_in_ffilter_wrt_iff[OF transp_on_less asymp_on_less totalp_on_less]

lemmas (in linorder) is_least_in_ffilter_swap_predicate =
  is_least_in_ffilter_wrt_swap_predicate[OF transp_on_less asymp_on_less totalp_on_less]

end