Theory Set_System

theory Set_System
  imports Main
begin

section ‹AI-Authored proof formalization via independence systems›

subsection ‹Independence Systems›

text ‹
  An independence system consists of a finite ground set \<^term>‹E› and a family \<^term>‹F›
  of subsets satisfying: (1) the empty set is in \<^term>‹F›, and (2) \<^term>‹F› is hereditary
  (downward closed under subsets).
›

locale indep_system =
  fixes E :: "'a set" and indep :: "'a set ⇒ bool"
  assumes finite_E: "finite E"
  assumes empty_indep: "indep {}"
  assumes indep_subset_carrier: "⋀F. indep F ⟹ F ⊆ E"
  assumes hereditary: "⋀F F'. indep F ⟹ F' ⊆ F ⟹ indep F'"

text ‹
  A maximal independent set is one where no element can be added while preserving independence.
›

definition (in indep_system) maximal :: "'a set ⇒ bool" where
  "maximal F ⟷ indep F ∧ (∀e ∈ E - F. ¬ indep (F ∪ {e}))"

lemma (in indep_system) maximalI:
  assumes "indep F" "⋀e. e ∈ E - F ⟹ ¬ indep (F ∪ {e})"
  shows "maximal F"
  unfolding maximal_def using assms by blast

lemma (in indep_system) maximalD:
  assumes "maximal F"
  shows "indep F" "⋀e. e ∈ E - F ⟹ ¬ indep (F ∪ {e})"
  using assms unfolding maximal_def by blast+

subsection ‹Best-In-Greedy Algorithm›

text ‹
  The Best-In-Greedy algorithm processes elements of \<^term>‹E› in a given order, 
  greedily adding each element if independence is preserved.
  We model it as a fold over a list.
›

definition greedy_step :: "('a set ⇒ bool) ⇒ 'a ⇒ 'a set ⇒ 'a set" where
  "greedy_step indep e F = (if indep (F ∪ {e}) then F ∪ {e} else F)"

definition best_in_greedy :: "('a set ⇒ bool) ⇒ 'a list ⇒ 'a set" where
  "best_in_greedy indep es = foldl (λF e. greedy_step indep e F) {} es"

text ‹
  We define the sequence of intermediate sets produced by the greedy algorithm.
›

fun greedy_partial :: "('a set ⇒ bool) ⇒ 'a list ⇒ nat ⇒ 'a set" where
  "greedy_partial indep es 0 = {}" |
  "greedy_partial indep es (Suc i) = 
    greedy_step indep (es ! i) (greedy_partial indep es i)"


text ‹The final result equals the partial result after processing all elements.›

lemma best_in_greedy_foldl_partial:
  assumes "n ≤ length es"
  shows "foldl (λF e. greedy_step indep e F) {} (take n es) = greedy_partial indep es n" 
  using assms
proof (induction n)
  case 0
  then show ?case by simp
next
  case (Suc n)
  thus ?case
    by (simp add: take_Suc_conv_app_nth)
qed

lemma best_in_greedy_eq_partial:
  "best_in_greedy indep es = greedy_partial indep es (length es)"
  unfolding best_in_greedy_def
  using best_in_greedy_foldl_partial[of "length es" es indep]
  by simp

subsubsection ‹Properties of \<^term>‹greedy_partial››

text ‹The partial result is monotonically increasing.›

lemma greedy_partial_mono:
  "i ≤ j ⟹ greedy_partial indep es i ⊆ greedy_partial indep es j"
proof (induction j)
  case 0
  then show ?case by simp
next
  case (Suc j)
  then show ?case
    by (cases "i = Suc j") (auto simp: greedy_step_def)
qed

text ‹If an element was skipped at step \<^term>‹j›, adding it to F\_{j-1} was not independent.›

lemma greedy_partial_skip:
  assumes "j < length es" "es ! j ∉ greedy_partial indep es (Suc j)"
  shows "¬ indep (greedy_partial indep es j ∪ {es ! j})"
  using assms by (simp add: greedy_step_def split: if_splits)

text ‹The partial set is always contained in the first i elements.›

lemma greedy_partial_subset:
  assumes "i ≤ length es"
  shows "greedy_partial indep es i ⊆ set (take i es)"
  using assms
proof (induction i)
  case 0
  then show ?case by simp
next
  case (Suc i)
  then have "greedy_partial indep es i ⊆ set (take i es)" by simp
  moreover have "set (take i es) ⊆ set (take (Suc i) es)"
    by (simp add: set_take_subset_set_take)
  moreover have "es ! i ∈ set (take (Suc i) es)"
    using Suc.prems by (simp add: take_Suc_conv_app_nth)
  ultimately show ?case 
    by (auto simp: greedy_step_def)
qed


subsubsection ‹Theorem: Best-In-Greedy returns a maximal independent set›

text ‹
  Theorem 2.1 of larry2.tex (Theorem 13.9 of Korte-Vygen).
  If (E, indep) is an independence system and es is a permutation of E,
  then the Best-In-Greedy output is a maximal independent set.
  
  First we show the greedy output is independent, by induction.
›

lemma (in indep_system) greedy_partial_indep:
  assumes "i ≤ length es" "set es ⊆ E"
  shows "indep (greedy_partial indep es i)"
  using assms
proof (induction i)
  case 0
  then show ?case using empty_indep by simp
next
  case (Suc i)
  then have IH: "indep (greedy_partial indep es i)" by simp
  show ?case
  proof (cases "indep (greedy_partial indep es i ∪ {es ! i})")
    case True
    then show ?thesis by (simp add: greedy_step_def)
  next
    case False
    then show ?thesis using IH by (simp add: greedy_step_def)
  qed
qed

text ‹Now the main theorem.›

theorem (in indep_system) best_in_greedy_maximal:
  assumes perm: "set es = E" and distinct: "distinct es"
  shows "maximal (best_in_greedy indep es)"
proof (rule maximalI)
  have set_es: "set es ⊆ E" using perm by simp

  show indep_result: "indep (best_in_greedy indep es)"
    unfolding best_in_greedy_eq_partial
    using greedy_partial_indep[of "length es" es] set_es by simp

  fix e assume e_outside: "e ∈ E - best_in_greedy indep es"
  show "¬ indep (best_in_greedy indep es ∪ {e})"
  proof -
    from e_outside perm have "e ∈ set es" by simp
    then obtain j where j: "j < length es" "es ! j = e" 
      by (metis in_set_conv_nth)
    from e_outside have "e ∉ greedy_partial indep es (length es)"
      unfolding best_in_greedy_eq_partial by simp
    then have "e ∉ greedy_partial indep es (Suc j)"
      using greedy_partial_mono[of "Suc j" "length es" indep es] j by auto
    then have not_indep_j: "¬ indep (greedy_partial indep es j ∪ {e})"
      using greedy_partial_skip[of j es indep] j by simp
    have sub: "greedy_partial indep es j ∪ {e} ⊆ best_in_greedy indep es ∪ {e}"
      unfolding best_in_greedy_eq_partial 
      using greedy_partial_mono[of j "length es" indep es] j by auto
    show "¬ indep (best_in_greedy indep es ∪ {e})"
    proof 
      assume "indep (best_in_greedy indep es ∪ {e})"
      then show False using hereditary[OF _ sub] not_indep_j by blast
    qed
  qed
qed


end