Session Approximation_Algorithms

Theory Approx_VC_Hoare

section "Vertex Cover"

theory Approx_VC_Hoare
imports "HOL-Hoare.Hoare_Logic"
begin

text ‹The algorithm is classical, the proof is based on and augments the one
by Berghammer and M\"uller-Olm \cite{BerghammerM03}.›

subsection "Graph"

text ‹A graph is simply a set of edges, where an edge is a 2-element set.›

definition vertex_cover :: "'a set set  'a set  bool" where
"vertex_cover E C = (e  E. e  C  {})"

abbreviation matching :: "'a set set  bool" where
"matching M  pairwise disjnt M"

lemma card_matching_vertex_cover:
  " finite C;  matching M;  M  E;  vertex_cover E C   card M  card C"
apply(erule card_le_if_inj_on_rel[where r = "λe v. v  e"])
 apply (meson disjnt_def disjnt_iff vertex_cover_def subsetCE)
by (meson disjnt_iff pairwise_def)


subsection "The Approximation Algorithm"

text ‹Formulated using a simple(!) predefined Hoare-logic.
This leads to a streamlined proof based on standard invariant reasoning.

The nondeterministic selection of an element from a set F› is simulated by @{term "SOME x. x  F"}.
The SOME› operator is built into HOL: @{term "SOME x. P x"} denotes some x› that satisfies P›
if such an x› exists; otherwise it denotes an arbitrary element. Note that there is no
actual nondeterminism involved: @{term "SOME x. P x"} is some fixed element
but in general we don't know which one. Proofs about SOME› are notoriously tedious.
Typically it involves showing first that @{prop "x. P x"}. Then @{thm someI_ex} implies
@{prop"P (SOME x. P x)"}. There are a number of (more) useful related theorems:
just click on @{thm someI_ex} to be taken there.›

text ‹Convenient notation for choosing an arbitrary element from a set:›
abbreviation "some A  SOME x. x  A"

locale Edges =
  fixes E :: "'a set set"
  assumes finE: "finite E"
  assumes edges2: "e  E  card e = 2"
begin

text ‹The invariant:›

definition "inv_matching C F M =
  (matching M  M  E  card C  2 * card M  (e  M. f  F. e  f = {}))"

definition invar :: "'a set  'a set set  bool" where
"invar C F = (F  E  vertex_cover (E-F) C  finite C  (M. inv_matching C F M))"

text ‹Preservation of the invariant by the loop body:›

lemma invar_step:
  assumes "F  {}" "invar C F"
  shows "invar (C  some F) (F - {e'  F. some F  e'  {}})"
proof -
  from assms(2) obtain M where "F  E" and vc: "vertex_cover (E-F) C" and fC: "finite C"
    and m: "matching M" "M  E" and card: "card C  2 * card M"
    and disj: "e  M. f  F. e  f = {}"
  by (auto simp: invar_def inv_matching_def)
  let ?e = "SOME e. e  F"
  have "?e  F" using F  {} by (simp add: some_in_eq)
  hence fe': "finite ?e" using F  E edges2 by(intro card_ge_0_finite) auto
  have "?e  M" using edges2 ?e  F disj F  E by fastforce
  have card': "card (C  ?e)  2 * card (insert ?e M)"
    using ?e  F ?e  M card_Un_le[of C ?e] F  E edges2 card finite_subset[OF m(2) finE]
    by fastforce
  let ?M = "M  {?e}"
  have vc': "vertex_cover (E - (F - {e'  F. ?e  e'  {}})) (C  ?e)"
    using vc by(auto simp: vertex_cover_def)
  have m': "inv_matching (C  ?e) (F - {e'  F. ?e  e'  {}}) ?M"
    using m card' F  E ?e  F disj
    by(auto simp: inv_matching_def Int_commute disjnt_def pairwise_insert)
  show ?thesis using F  E vc' fC fe' m' by(auto simp add: invar_def Let_def)
qed


lemma approx_vertex_cover:
"VARS C F
  {True}
  C := {};
  F := E;
  WHILE F  {}
  INV {invar C F}
  DO C := C  some F;
     F := F - {e'  F. some F  e'  {}}
  OD
  {vertex_cover E C  (C'. finite C'  vertex_cover E C'  card C  2 * card C')}"
proof (vcg, goal_cases)
  case (1 C F)
  have "inv_matching {} E {}" by (auto simp add: inv_matching_def)
  with 1 show ?case by (auto simp add: invar_def vertex_cover_def)
next
  case (2 C F)
  thus ?case using invar_step[of F C] by(auto simp: Let_def)
next
  case (3 C F)
  then obtain M :: "'a set set" where
    post: "vertex_cover E C" "matching M" "M  E" "card C  2 * card M"
    by(auto simp: invar_def inv_matching_def)

  have opt: "card C  2 * card C'" if C': "finite C'" "vertex_cover E C'" for C'
  proof -
    note post(4)
    also have "2 * card M  2 * card C'"
    using card_matching_vertex_cover[OF C'(1) post(2,3) C'(2)] by simp
    finally show "card C  2 * card C'" .
  qed

  show ?case using post(1) opt by auto
qed

end (* locale Graph *)

subsection "Version for Hypergraphs"

text ‹Almost the same. We assume that the degree of every edge is bounded.›

locale Bounded_Hypergraph =
  fixes E :: "'a set set"
  fixes k :: nat
  assumes finE: "finite E"
  assumes edge_bnd: "e  E  finite e  card e  k"
  assumes E1: "{}  E"
begin

definition "inv_matching C F M =
  (matching M  M  E  card C  k * card M  (e  M. f  F. e  f = {}))"

definition invar :: "'a set  'a set set  bool" where
"invar C F = (F  E  vertex_cover (E-F) C  finite C  (M. inv_matching C F M))"

lemma invar_step:
  assumes "F  {}" "invar C F"
  shows "invar (C  some F) (F - {e'  F. some F  e'  {}})"
proof -
  from assms(2) obtain M where "F  E" and vc: "vertex_cover (E-F) C" and fC: "finite C"
    and m: "matching M" "M  E" and card: "card C  k * card M"
    and disj: "e  M. f  F. e  f = {}"
  by (auto simp: invar_def inv_matching_def)
  let ?e = "SOME e. e  F"
  have "?e  F" using F  {} by (simp add: some_in_eq)
  hence fe': "finite ?e" using F  E assms(2) edge_bnd by blast
  have "?e  M" using E1 ?e  F disj F  E by fastforce
  have card': "card (C  ?e)  k * card (insert ?e M)"
    using ?e  F ?e  M card_Un_le[of C ?e] F  E edge_bnd card finite_subset[OF m(2) finE]
    by fastforce
  let ?M = "M  {?e}"
  have vc': "vertex_cover (E - (F - {e'  F. ?e  e'  {}})) (C  ?e)"
    using vc by(auto simp: vertex_cover_def)
  have m': "inv_matching (C  ?e) (F - {e'  F. ?e  e'  {}}) ?M"
    using m card' F  E ?e  F disj
    by(auto simp: inv_matching_def Int_commute disjnt_def pairwise_insert)
  show ?thesis using F  E vc' fC fe' m' by(auto simp add: invar_def Let_def)
qed


lemma approx_vertex_cover_bnd:
"VARS C F
  {True}
  C := {};
  F := E;
  WHILE F  {}
  INV {invar C F}
  DO C := C  some F;
     F := F - {e'  F. some F  e'  {}}
  OD
  {vertex_cover E C  (C'. finite C'  vertex_cover E C'  card C  k * card C')}"
proof (vcg, goal_cases)
  case (1 C F)
  have "inv_matching {} E {}" by (auto simp add: inv_matching_def)
  with 1 show ?case by (auto simp add: invar_def vertex_cover_def)
next
  case (2 C F)
  thus ?case using invar_step[of F C] by(auto simp: Let_def)
next
  case (3 C F)
  then obtain M :: "'a set set" where
    post: "vertex_cover E C" "matching M" "M  E" "card C  k * card M"
    by(auto simp: invar_def inv_matching_def)

  have opt: "card C  k * card C'" if C': "finite C'" "vertex_cover E C'" for C'
  proof -
    note post(4)
    also have "k * card M  k * card C'"
    using card_matching_vertex_cover[OF C'(1) post(2,3) C'(2)] by simp
    finally show "card C  k * card C'" .
  qed

  show ?case using post(1) opt by auto
qed

end (* locale Bounded_Hypergraph *)

end

Theory Approx_SC_Hoare

section ‹Set Cover›

theory Approx_SC_Hoare
imports
  "HOL-Hoare.Hoare_Logic"
  Complex_Main (* "HOL-Analysis.Harmonic_Numbers" *)
begin

text ‹This is a formalization of the set cover algorithm and proof
in the book by Kleinberg and Tardos \cite{KleinbergT06}.›

definition harm :: "nat  'a :: real_normed_field" where
  "harm n = (k=1..n. inverse (of_nat k))"
(* For simplicity defined locally instead of importing HOL-Analysis.Harmonic_Numbers.
   Only the definition, no theorems are needed.
*)

locale Set_Cover = (* Set Cover *)
  fixes w :: "nat  real"
    and m :: nat
    and S :: "nat  'a set"
  assumes S_finite: "i  {1..m}. finite (S i)"
      and w_nonneg: "i. 0  w i"
begin

definition U :: "'a set" where
  "U = (i  {1..m}. S i)"

lemma S_subset: "i  {1..m}. S i  U"
  using U_def by blast

lemma U_finite: "finite U"
  unfolding U_def using S_finite by blast

lemma empty_cover: "m = 0  U = {}"
  using U_def by simp

definition sc :: "nat set  'a set  bool" where
  "sc C X  C  {1..m}  (i  C. S i) = X"

definition cost :: "'a set  nat  real" where
  "cost R i = w i / card (S i  R)"

lemma cost_nonneg: "0  cost R i"
  using w_nonneg by (simp add: cost_def)

text cost R i = 0› if card (S i ∩ R) = 0›! Needs to be accounted for separately in min_arg›.›
fun min_arg :: "'a set  nat  nat" where
  "min_arg R 0 = 1"
| "min_arg R (Suc x) =
   (let j = min_arg R x
    in if S j  R = {}  (S (Suc x)  R  {}  cost R (Suc x) < cost R j) then (Suc x) else j)"

lemma min_in_range: "k > 0  min_arg R k  {1..k}"
  by (induction k) (force simp: Let_def)+

lemma min_empty: "S (min_arg R k)  R = {}  i  {1..k}. S i  R = {}"
proof (induction k)
  case (Suc k)
  from Suc.prems have prem: "S (min_arg R k)  R = {}" by (auto simp: Let_def split: if_splits)
  with Suc.IH have IH: "i  {1..k}. S i  R = {}" .
  show ?case proof fix i assume "i  {1..Suc k}" show "S i  R = {}"
    proof (cases i = Suc k)
      case True with Suc.prems prem show ?thesis by simp
    next
      case False with IH i  {1..Suc k} show ?thesis by simp
    qed
  qed
qed simp

lemma min_correct: " i  {1..k}; S i  R  {}   cost R (min_arg R k)  cost R i"
proof (induction k)
  case (Suc k)
  show ?case proof (cases i = Suc k)
    case True with Suc.prems show ?thesis by (auto simp: Let_def)
  next
    case False with Suc.prems Suc.IH have IH: "cost R (min_arg R k)  cost R i" by simp
    from Suc.prems False min_empty[of R k] have "S (min_arg R k)  R  {}" by force
    with IH show ?thesis by (auto simp: Let_def)
  qed
qed simp

text ‹Correctness holds quite trivially for both m = 0 and m > 0
      (assuming a set cover can be found at all, otherwise algorithm would not terminate).›
lemma set_cover_correct:
"VARS (R :: 'a set) (C :: nat set) (i :: nat)
  {True}
  R := U; C := {};
  WHILE R  {} INV {R  U  sc C (U - R)} DO
  i := min_arg R m;
  R := R - S i;
  C := C  {i}
  OD
  {sc C U}"
proof (vcg, goal_cases)
  case 2 show ?case proof (cases m)
    case 0
    from empty_cover[OF this] 2 show ?thesis by (auto simp: sc_def)
  next
    case Suc then have "m > 0" by simp
    from min_in_range[OF this] 2 show ?thesis using S_subset by (auto simp: sc_def)
  qed
qed (auto simp: sc_def)

definition c_exists :: "nat set  'a set  bool" where
  "c_exists C R = (c. sum w C = sum c (U - R)  (i. 0  c i)
                 (k  {1..m}. sum c (S k  (U - R))
                    (j = card (S k  R) + 1..card (S k). inverse j) * w k))"

definition inv :: "nat set  'a set  bool" where
  "inv C R  sc C (U - R)  R  U  c_exists C R"

lemma invI:
  assumes "sc C (U - R)" "R  U"
          "c. sum w C = sum c (U - R)  (i. 0  c i)
         (k  {1..m}. sum c (S k  (U - R))
                       (j = card (S k  R) + 1..card (S k). inverse j) * w k)"
    shows "inv C R" using assms by (auto simp: inv_def c_exists_def)

lemma invD:
  assumes "inv C R"
  shows "sc C (U - R)" "R  U"
        "c. sum w C = sum c (U - R)  (i. 0  c i)
       (k  {1..m}. sum c (S k  (U - R))
                     (j = card (S k  R) + 1..card (S k). inverse j) * w k)"
  using assms by (auto simp: inv_def c_exists_def)

lemma inv_init: "inv {} U"
proof (rule invI, goal_cases)
  case 3
  let ?c = "(λ_. 0) :: 'a  real"
  have "sum w {} = sum ?c (U - U)" by simp
  moreover {
    have "k  {1..m}. 0  (j = card (S k  U) + 1..card (S k). inverse j) * w k"
      by (simp add: sum_nonneg w_nonneg)
    then have "(k{1..m}. sum ?c (S k  (U - U))
              (j = card (S k  U) + 1..card (S k). inverse j) * w k)" by simp
  }
  ultimately show ?case by blast
qed (simp_all add: sc_def)

lemma inv_step:
  assumes "inv C R" "R  {}"
  defines [simp]: "i  min_arg R m"
  shows "inv (C  {i}) (R - (S i))"
proof (cases m)
  case 0
  from empty_cover[OF this] invD(2)[OF assms(1)] have "R = {}" by blast
  then show ?thesis using assms(2) by simp
next
  case Suc then have "0 < m" by simp
  note hyp = invD[OF assms(1)]
  show ?thesis proof (rule invI, goal_cases)
      ― ‹Correctness›
    case 1 have "i  {1..m}" using min_in_range[OF 0 < m] by simp
    with hyp(1) S_subset show ?case by (auto simp: sc_def)
  next
    case 2 from hyp(2) show ?case by auto
  next
    case 3
      ― ‹Set Cover grows›
    have "i  {1..m}. S i  R  {}"
      using assms(2) U_def hyp(2) by blast
    then have "S i  R  {}" using min_empty by auto
    then have "0 < card (S i  R)"
      using S_finite min_in_range[OF 0 < m] by auto

      ― ‹Proving properties of cost function›
    from hyp(3) obtain c where "sum w C = sum c (U - R)" "i. 0  c i" and
      SUM: "k{1..m}. sum c (S k  (U - R))
         (j = card (S k  R) + 1..card (S k). inverse j) * w k" by blast
    let ?c = "(λx. if x  S i  R then cost R i else c x)"

      ― ‹Proof of Lemma 11.9›
    have "finite (U - R)" "finite (S i  R)" "(U - R)  (S i  R) = {}"
      using U_finite S_finite min_in_range[OF 0 < m] by auto
    then have "sum ?c (U - R  (S i  R)) = sum ?c (U - R) + sum ?c (S i  R)"
      by (rule sum.union_disjoint)
    moreover have U_split: "U - (R - S i) = U - R  (S i  R)" using hyp(2) by blast
    moreover {
      have "sum ?c (S i  R) = card (S i  R) * cost R i" by simp
      also have "... = w i" unfolding cost_def using 0 < card (S i  R) by simp
      finally have "sum ?c (S i  R) = w i" .
    }
    ultimately have "sum ?c (U - (R - S i)) = sum ?c (U - R) + w i" by simp
    moreover {
      have "C  {i} = {}" using hyp(1) S i  R  {} by (auto simp: sc_def)
      from sum.union_disjoint[OF _ _ this] have "sum w (C  {i}) = sum w C + w i"
        using hyp(1) by (auto simp: sc_def intro: finite_subset)
    }
    ultimately have 1: "sum w (C  {i}) = sum ?c (U - (R - S i))" ― ‹Lemma 11.9›
      using ‹sum w C = sum c (U - R) by simp

    have 2: "i. 0  ?c i" using i. 0  c i cost_nonneg by simp

      ― ‹Proof of Lemma 11.10›
    have 3: "k{1..m}. sum ?c (S k  (U - (R - S i)))
           (j = card (S k  (R - S i)) + 1..card (S k). inverse j) * w k"
    proof
      fix k assume "k  {1..m}"
      let ?rem = "S k  R" ― ‹Remaining elements to be covered›
      let ?add = "S k  S i  R" ― ‹Elements that will be covered in this step›
      let ?cov = "S k  (U - R)" ― ‹Covered elements›

      ― ‹Transforming left and right sides›
      have "sum ?c (S k  (U - (R - S i))) = sum ?c (S k  (U - R  (S i  R)))"
        unfolding U_split ..
      also have "... = sum ?c (?cov  ?add)"
        by (simp add: Int_Un_distrib Int_assoc)
      also have "... = sum ?c ?cov + sum ?c ?add"
        by (rule sum.union_disjoint) (insert S_finite k  _, auto)
      finally have lhs:
        "sum ?c (S k  (U - (R - S i))) = sum ?c ?cov + sum ?c ?add" .
      have "S k  (R - S i) = ?rem - ?add" by blast
      then have "card (S k  (R - S i)) = card (?rem - ?add)" by simp
      also have "... = card ?rem - card ?add"
        using S_finite k  _ by (auto intro: card_Diff_subset)
      finally have rhs:
        "card (S k  (R - S i)) + 1 = card ?rem - card ?add + 1" by simp
      
      ― ‹The apparent complexity of the remaining proof is deceiving. Much of this is just about
          convincing Isabelle that these sum transformations are allowed.›
      have "sum ?c ?add = card ?add * cost R i" by simp
      also have "...  card ?add * cost R k"
        proof (cases "?rem = {}")
          case True
          then have "card ?add = 0" by (auto simp: card_eq_0_iff)
          then show ?thesis by simp
        next
          case False
          from min_correct[OF k  _ this] have "cost R i  cost R k" by simp
          then show ?thesis by (simp add: mult_left_mono)
        qed
      also have "... = card ?add * inverse (card ?rem) * w k"
        by (simp add: cost_def divide_inverse_commute)
      also have "... = (j  {card ?rem - card ?add + 1 .. card ?rem}. inverse (card ?rem)) * w k"
        proof -
          have "card ?add  card ?rem"
            using S_finite k  _ by (blast intro: card_mono)
          then show ?thesis by (simp add: sum_distrib_left)
        qed
      also have "...  (j  {card ?rem - card ?add + 1 .. card ?rem}. inverse j) * w k"
        proof -
          have "j  {card ?rem - card ?add + 1 .. card ?rem}. inverse (card ?rem)  inverse j"
            by force
          then have "(j  {card ?rem - card ?add + 1 .. card ?rem}. inverse (card ?rem))
                    (j  {card ?rem - card ?add + 1 .. card ?rem}. inverse j)"
            by (blast intro: sum_mono)
          with w_nonneg show ?thesis by (blast intro: mult_right_mono)
        qed
      finally have "sum ?c ?add
                  (j  {card ?rem - card ?add + 1 .. card ?rem}. inverse j) * w k" .
      moreover from SUM have "sum ?c ?cov 
                            (j  {card ?rem + 1 .. card (S k)}. inverse j) * w k"
        using k  {1..m} by simp
      ultimately have "sum ?c (S k  (U - (R - S i)))
                     ((j  {card ?rem - card ?add + 1 .. card ?rem}. inverse j) +
                        (j  {card ?rem + 1 .. card (S k)}. inverse j)) * w k"
        unfolding lhs by argo
      also have "... = (j  {card ?rem - card ?add + 1 .. card (S k)}. inverse j) * w k"
        proof -
          have sum_split: "b  {a .. c}  sum f {a .. c} = sum f {a .. b} + sum f {Suc b .. c}"
            for f :: "nat  real" and a b c :: nat
          proof -
            assume "b  {a .. c}"
            then have "{a .. b}  {Suc b .. c} = {a .. c}" by force
            moreover have "{a .. b}  {Suc b .. c} = {}"
              using b  {a .. c} by auto
            ultimately show ?thesis by (metis finite_atLeastAtMost sum.union_disjoint)
          qed

          have "(j  {card ?rem - card ?add + 1 .. card (S k)}. inverse j)
              = (j  {card ?rem - card ?add + 1 .. card ?rem}. inverse j)
              + (j  {card ?rem + 1 .. card (S k)}. inverse j)"
            proof (cases ?add = {})
              case False
              then have "0 < card ?add" "0 < card ?rem"
                using S_finite k  _ by fastforce+
              then have "Suc (card ?rem - card ?add)  card ?rem" by simp
              moreover have "card ?rem  card (S k)"
                using S_finite k  _ by (simp add: card_mono)
              ultimately show ?thesis by (auto intro: sum_split)
            qed simp
          then show ?thesis by algebra
        qed
      finally show "sum ?c (S k  (U - (R - S i)))
                  (j  {card (S k  (R - S i)) + 1 .. card (S k)}. inverse j) * w k"
        unfolding rhs .
    qed

    from 1 2 3 show ?case by blast
  qed
qed

lemma cover_sum:
  fixes c :: "'a  real"
  assumes "sc C V" "i. 0  c i"
  shows "sum c V  (i  C. sum c (S i))"
proof -
  from assms(1) have "finite C" by (auto simp: sc_def finite_subset)
  then show ?thesis using assms(1)
  proof (induction C arbitrary: V rule: finite_induct)
    case (insert i C)
    have V_split: "( (S ` insert i C)) = ( (S ` C))  S i" by auto
    have finite: "finite ( (S ` C))" "finite (S i)"
      using insert S_finite by (auto simp: sc_def)

    have "sum c (S i) - sum c ( (S ` C)  S i)  sum c (S i)"
      using assms(2) by (simp add: sum_nonneg)
    then have "sum c ( (S ` insert i C))  sum c ( (S ` C)) + sum c (S i)"
      unfolding V_split using sum_Un[OF finite, of c] by linarith
    moreover have "(iinsert i C. sum c (S i)) = (i  C. sum c (S i)) + sum c (S i)"
      by (simp add: insert.hyps)
    ultimately show ?case using insert by (fastforce simp: sc_def)
  qed (simp add: sc_def)
qed

abbreviation H :: "nat  real" where "H  harm"

definition d_star :: nat ("d*") where "d*  Max (card ` (S ` {1..m}))"

lemma set_cover_bound:
  assumes "inv C {}" "sc C' U"
  shows "sum w C  H d* * sum w C'"
proof -
  from invD(3)[OF assms(1)] obtain c where
    "sum w C = sum c U" "i. 0  c i" and H_bound:
    "k  {1..m}. sum c (S k)  H (card (S k)) * w k" ― ‹Lemma 11.10›
    by (auto simp: harm_def Int_absorb2 S_subset)

  have "k  {1..m}. card (S k)  d*" by (auto simp: d_star_def)
  then have "k  {1..m}. H (card (S k))  H d*" by (auto simp: harm_def intro!: sum_mono2)
  with H_bound have "k  {1..m}. sum c (S k)  H d* * w k"
    by (metis atLeastAtMost_iff atLeastatMost_empty_iff empty_iff mult_right_mono w_nonneg)
  moreover have "C'  {1..m}" using assms(2) by (simp add: sc_def)
  ultimately have "i  C'. sum c (S i)  H d* * w i" by blast
  then have "(i  C'. sum c (S i))  H d* * sum w C'"
    by (auto simp: sum_distrib_left intro: sum_mono)

  have "sum w C = sum c U" by fact ― ‹Lemma 11.9›
  also have "...  (i  C'. sum c (S i))" by (rule cover_sum[OF assms(2)]) fact
  also have "...  H d* * sum w C'" by fact
  finally show ?thesis .
qed

theorem set_cover_approx:
"VARS (R :: 'a set) (C :: nat set) (i :: nat)
  {True}
  R := U; C := {};
  WHILE R  {} INV {inv C R} DO
  i := min_arg R m;
  R := R - S i;
  C := C  {i}
  OD
  {sc C U  (C'. sc C' U  sum w C  H d* * sum w C')}"
proof (vcg, goal_cases)
  case 1 show ?case by (rule inv_init)
next
  case 2 thus ?case using inv_step ..
next
  case (3 R C i)
  then have "sc C U" unfolding inv_def by auto
  with 3 show ?case by (auto intro: set_cover_bound)
qed

end (* Set Cover *)

end (* Theory *)

Theory Approx_MIS_Hoare

section "Independent Set"

theory Approx_MIS_Hoare
imports
  "HOL-Hoare.Hoare_Logic"
  "HOL-Library.Disjoint_Sets"
begin


text ‹The algorithm is classical, the proofs are inspired by the ones
by Berghammer and M\"uller-Olm \cite{BerghammerM03}.
In particular the approximation ratio is improved from Δ+1› to Δ›.›


subsection "Graph"

text ‹A set set is simply a set of edges, where an edge is a 2-element set.›

definition independent_vertices :: "'a set set  'a set  bool" where
"independent_vertices E S  S  E  (v1 v2. v1  S  v2  S  {v1, v2}  E)"

locale Graph_E =
  fixes E :: "'a set set"
  assumes finite_E: "finite E"
  assumes edges2: "e  E  card e = 2"
begin

fun vertices :: "'a set set  'a set" where
"vertices G = G"

abbreviation V :: "'a set" where
"V  vertices E"

definition approximation_miv :: "nat  'a set  bool" where
"approximation_miv n S  independent_vertices E S  (S'. independent_vertices E S'  card S'  card S * n)"

fun neighbors :: "'a  'a set" where
"neighbors v = {u. {u,v}  E}"

fun degree_vertex :: "'a  nat" where
"degree_vertex v = card (neighbors v)"

abbreviation Δ :: nat where
"Δ  Max{degree_vertex u|u. u  V}"

lemma finite_edges: "e  E  finite e"
  using card_ge_0_finite and edges2 by force

lemma finite_V: "finite V"
  using finite_edges and finite_E by auto

lemma finite_neighbors: "finite (neighbors u)"
  using finite_V and rev_finite_subset [of V "neighbors u"] by auto

lemma independent_vertices_finite: "independent_vertices E S  finite S"
  by (metis rev_finite_subset independent_vertices_def vertices.simps finite_V)

lemma edge_ex_vertices: "e  E  u v. u  v  e = {u, v}"
proof -
  assume "e  E"
  then have "card e = Suc (Suc 0)" using edges2 by auto
  then show "u v. u  v  e = {u, v}"
    by (metis card_eq_SucD insertI1)
qed

lemma Δ_pos [simp]: "E = {}  0 < Δ"
proof cases
  assume "E = {}"
  then show "E = {}  0 < Δ" by auto
next
  assume 1: "E  {}"
  then have "V  {}" using edges2 by fastforce
  moreover have "finite {degree_vertex u |u. u  V}"
    by (metis finite_V finite_imageI Setcompr_eq_image)
  ultimately have 2:  {degree_vertex u |u. u  V}" using Max_in by auto
  have  0"
  proof
    assume = 0"
    with 2 obtain u where 3: "u  V" and 4: "degree_vertex u = 0" by auto
    from 3 obtain e where 5: "e  E" and "u  e" by auto
    moreover with 4 have "v. {u, v}  e" using finite_neighbors insert_absorb by fastforce
    ultimately show False using edge_ex_vertices by auto
  qed
  then show "E = {}  0 < Δ" by auto
qed

lemma Δ_max_degree: "u  V  degree_vertex u  Δ"
proof -
  assume H: "u  V"
  have "finite {degree_vertex u |u. u  V}"
    by (metis finite_V finite_imageI Setcompr_eq_image)
  with H show "degree_vertex u  Δ" using Max_ge by auto
qed

subsection ‹Wei's algorithm: (Δ+1)›-approximation›

text ‹The 'functional' part of the invariant, used to prove that the algorithm produces an independent set of vertices.›

definition inv_iv :: "'a set  'a set  bool" where
"inv_iv S X  independent_vertices E S
             X  V
             (v1  (V - X). v2  S. {v1, v2}  E)
             S  X"

text ‹Strenghten the invariant with an approximation ratio r›:›

definition inv_approx :: "'a set  'a set  nat  bool" where
"inv_approx S X r  inv_iv S X  card X  card S * r"

text ‹Preservation of the functional invariant:›

lemma inv_preserv:
  fixes S :: "'a set"
    and X :: "'a set"
    and x :: "'a"
  assumes inv: "inv_iv S X"
      and x_def: "x  V - X"
    shows "inv_iv (insert x S) (X  neighbors x  {x})"
proof -
  have inv1: "independent_vertices E S"
   and inv2: "X  V"
   and inv3: "S  X"
   and inv4: "v1 v2. v1  (V - X)  v2  S  {v1, v2}  E"
    using inv unfolding inv_iv_def by auto
  have finite_S: "finite S" using inv1 and independent_vertices_finite by auto
  have S1: "y  S. {x, y}  E" using inv4 and x_def by blast
  have S2: "x  S. y  S. {x, y}  E" using inv1 unfolding independent_vertices_def by metis
  have S3: "v1  insert x S  v2  insert x S  {v1, v2}  E" for v1 v2
    proof -
      assume "v1  insert x S" and "v2  insert x S"
      then consider
          (a) "v1 = x" and "v2 = x"
        | (b) "v1 = x" and "v2  S"
        | (c) "v1  S" and "v2 = x"
        | (d) "v1  S" and "v2  S"
        by auto
      then show "{v1, v2}  E"
      proof cases
        case a then show ?thesis using edges2 by force
      next
        case b then show ?thesis using S1 by auto
      next
        case c then show ?thesis using S1 by (metis doubleton_eq_iff)
      next
        case d then show ?thesis using S2 by auto
      qed
    qed
  (* invariant conjunct 1 *)
  have "independent_vertices E (insert x S)"
    using S3 and inv1 and x_def unfolding independent_vertices_def by auto
  (* invariant conjunct 2 *)
  moreover have "X  neighbors x  {x}  V"
  proof
    fix xa
    assume "xa  X  neighbors x  {x}"
    then consider (a) "xa  X" | (b) "xa  neighbors x" | (c) "xa = x" by auto
    then show "xa  V"
    proof cases
      case a
      then show ?thesis using inv2 by blast
    next
      case b
      then show ?thesis by auto
    next
      case c
      then show ?thesis using x_def by blast
    qed
  qed
  (* invariant conjunct 3 *)
  moreover have "insert x S  X  neighbors x  {x}" using inv3 by auto
  (* invariant conjunct 4 *)
  moreover have "v1  V - (X  neighbors x  {x})  v2  insert x S  {v1, v2}  E" for v1 v2
  proof -
    assume H: "v1  V - (X  neighbors x  {x})" and "v2  insert x S"
    then consider (a) "v2 = x" | (b) "v2  S" by auto
    then show "{v1, v2}  E"
    proof cases
      case a
      with H have "v1  neighbors v2" by blast
      then show ?thesis by auto
    next
      case b
      from H have "v1  V - X" by blast
      with b and inv4 show ?thesis by blast
    qed
  qed
  (* conclusion *)
  ultimately show "inv_iv (insert x S) (X  neighbors x  {x})" unfolding inv_iv_def by blast
qed

lemma inv_approx_preserv:
  assumes inv: "inv_approx S X (Δ + 1)"
      and x_def: "x  V - X"
    shows "inv_approx (insert x S) (X  neighbors x  {x}) (Δ + 1)"
proof -
  have finite_S: "finite S" using inv and independent_vertices_finite
    unfolding inv_approx_def inv_iv_def by auto
  have Sx: "x  S" using inv and x_def unfolding inv_approx_def inv_iv_def by blast
  (* main invariant is preserved *)
  from inv have "inv_iv S X" unfolding inv_approx_def by auto
  with x_def have "inv_iv (insert x S) (X  neighbors x  {x})"
  proof (intro inv_preserv, auto) qed
  (* the approximation ratio is preserved (at most Δ+1 vertices are removed in any iteration) *)
  moreover have "card (X  neighbors x  {x})  card (insert x S) * (Δ + 1)"
  proof -
    have "degree_vertex x  Δ" using Δ_max_degree and x_def by auto
    then have "card (neighbors x  {x})  Δ + 1" using card_Un_le [of "neighbors x" "{x}"] by auto
    then have "card (X  neighbors x  {x})  card X + Δ + 1" using card_Un_le [of X "neighbors x  {x}"] by auto
    also have "...  card S * (Δ + 1) + Δ + 1" using inv unfolding inv_approx_def by auto
    also have "... = card (insert x S) * (Δ + 1)" using finite_S and Sx by auto
    finally show ?thesis .
  qed
  (* conclusion *)
  ultimately show "inv_approx (insert x S) (X  neighbors x  {x}) (Δ + 1)"
    unfolding inv_approx_def by auto
qed

(* the antecedent combines inv_approx (for an arbitrary ratio r) and the negated post-condition *)
lemma inv_approx: "independent_vertices E S  card V  card S * r  approximation_miv r S"
proof -
  assume 1: "independent_vertices E S" and 2: "card V  card S * r"
  have "independent_vertices E S'  card S'  card S * r" for S'
  proof -
    assume  "independent_vertices E S'"
    then have "S'  V" unfolding independent_vertices_def by auto
    then have "card S'  card V" using finite_V and card_mono by auto
    also have "...  card S * r" using 2 by auto
    finally show "card S'  card S * r" .
  qed
  with 1 show "approximation_miv r S" unfolding approximation_miv_def by auto
qed

theorem wei_approx_Δ_plus_1:
"VARS (S :: 'a set) (X :: 'a set) (x :: 'a)
  { True }
  S := {};
  X := {};
  WHILE X  V
  INV { inv_approx S X (Δ + 1) }
  DO x := (SOME x. x  V - X);
     S := insert x S;
     X := X  neighbors x  {x}
  OD
  { approximation_miv (Δ + 1) S }"
proof (vcg, goal_cases)
  case (1 S X x) (* invariant initially true *)
  then show ?case unfolding inv_approx_def inv_iv_def independent_vertices_def by auto
next
  case (2 S X x) (* invariant preserved by loop *)
  (* definedness of assignment *)
  let ?x = "(SOME x. x  V - X)"
  have "V - X  {}" using 2 unfolding inv_approx_def inv_iv_def by blast
  then have "?x  V - X" using some_in_eq by metis
  with 2 show ?case using inv_approx_preserv by auto
next
  case (3 S X x) (* invariant implies post-condition *)
  then show ?case using inv_approx unfolding inv_approx_def inv_iv_def by auto
qed


subsection ‹Wei's algorithm: Δ›-approximation›

text ‹The previous approximation uses very little information about the optimal solution (it has at most as many vertices as the set itself). With some extra effort we can improve the ratio to Δ› instead of Δ+1›. In order to do that we must show that among the vertices removed in each iteration, at most Δ› could belong to an optimal solution. This requires carrying around a set P› (via a ghost variable) which records the vertices deleted in each iteration.›

definition inv_partition :: "'a set  'a set  'a set set  bool" where
"inv_partition S X P  inv_iv S X
                      P = X
                      (p  P. s  V. p = {s}  neighbors s)
                      card P = card S
                      finite P"

lemma inv_partition_preserv:
  assumes inv: "inv_partition S X P"
      and x_def: "x  V - X"
    shows "inv_partition (insert x S) (X  neighbors x  {x}) (insert ({x}  neighbors x) P)"
proof -
  have finite_S: "finite S" using inv and independent_vertices_finite
    unfolding inv_partition_def inv_iv_def by auto
  have Sx: "x  S" using inv and x_def unfolding inv_partition_def inv_iv_def by blast
  (* main invariant is preserved *)
  from inv have "inv_iv S X" unfolding inv_partition_def by auto
  with x_def have "inv_iv (insert x S) (X  neighbors x  {x})"
  proof (intro inv_preserv, auto) qed
  (* conjunct 1 *)
  moreover have "(insert ({x}  neighbors x) P) = X  neighbors x  {x}"
    using inv unfolding inv_partition_def by auto
  (* conjunct 2 *)
  moreover have "(pinsert ({x}  neighbors x) P. s  V. p = {s}  neighbors s)"
    using inv and x_def unfolding inv_partition_def by auto
  (* conjunct 3 *)
  moreover have "card (insert ({x}  neighbors x) P) = card (insert x S)"
  proof -
    from x_def and inv have "x  P" unfolding inv_partition_def by auto
    then have "{x}  neighbors x  P" by auto
    then have "card (insert ({x}  neighbors x) P) = card P + 1" using inv unfolding inv_partition_def by auto
    moreover have "card (insert x S) = card S + 1" using Sx and finite_S by auto
    ultimately show ?thesis using inv unfolding inv_partition_def by auto
  qed
  (* conjunct 4 *)
  moreover have "finite (insert ({x}  neighbors x) P)"
    using inv unfolding inv_partition_def by auto
  (* conclusion *)
  ultimately show "inv_partition (insert x S) (X  neighbors x  {x}) (insert ({x}  neighbors x) P)"
    unfolding inv_partition_def by auto
qed

lemma card_Union_le_sum_card:
  fixes U :: "'a set set"
  assumes "u  U. finite u"
  shows "card (U)  sum card U"
proof (cases "finite U")
  case False
  then show "card (U)  sum card U"
    using card_eq_0_iff finite_UnionD by auto
next
  case True
  then show "card (U)  sum card U"
  proof (induct U rule: finite_induct)
    case empty
    then show ?case by auto
  next
    case (insert x F)
    then have "card((insert x F))  card(x) + card (F)" using card_Un_le by auto
    also have "...  card(x) + sum card F" using insert.hyps by auto
    also have "... = sum card (insert x F)" using sum.insert_if and insert.hyps by auto
    finally show ?case .
  qed
qed

(* this lemma could be more generally about U :: "nat set", but this makes its application more difficult later *)
lemma sum_card:
  fixes U :: "'a set set"
    and n :: nat
  assumes "S  U. card S  n"
  shows "sum card U  card U * n"
proof cases
  assume "infinite U  U = {}"
  then have "sum card U = 0" using sum.infinite by auto
  then show "sum card U  card U * n" by auto
next
  assume "¬(infinite U  U = {})"
  with assms have "finite U" and "U  {}"and "S  U. card S  n" by auto
  then show "sum card U  card U * n"
  proof (induct U rule: finite_ne_induct)
    case (singleton x)
    then show ?case by auto
  next
    case (insert x F)
    assume "Sinsert x F. card S  n"
    then have 1:"card x  n" and 2:"sum card F  card F * n" using insert.hyps by auto
    then have "sum card (insert x F) = card x + sum card F" using sum.insert_if and insert.hyps by auto
    also have "...  n + card F * n" using 1 and 2 by auto
    also have "... = card (insert x F) * n" using card_insert_if and insert.hyps by auto
    finally show ?case .
  qed
qed

(* among the vertices deleted in each iteration, at most Δ can belong to an independent set of
   vertices: the chosen vertex or (some of) its neighbors *)
lemma x_or_neighbors:
  fixes P :: "'a set set"
    and S :: "'a set"
  assumes inv: "pP. s  V. p = {s}  neighbors s"
      and ivS: "independent_vertices E S"
    shows "p  P. card (S  p)  Δ"
proof
  fix p
  assume "p  P"
  then obtain s where 1: "s  V  p = {s}  neighbors s" using inv by blast
  then show "card (S  p)  Δ"
  proof cases
    assume "s  S"
    then have "S  neighbors s = {}" using ivS unfolding independent_vertices_def by auto
    then have "S  p  {s}" using 1 by auto
    then have 2: "card (S  p)  1" using subset_singletonD by fastforce
    consider (a) "E = {}" | (b) "0 < Δ" using Δ_pos by auto
    then show "card (S  p)  Δ"
    proof cases
      case a
      then have "S = {}" using ivS unfolding independent_vertices_def by auto
      then show ?thesis by auto
    next
      case b
      then show ?thesis using 2 by auto
    qed  
  next
    assume "s  S"
    with 1 have "S  p  neighbors s" by auto
    then have "card (S  p)  degree_vertex s" using card_mono and finite_neighbors by auto
    then show "card (S  p)  Δ" using 1 and Δ_max_degree [of s] by auto
  qed
qed

(* the premise combines the invariant and the negated post-condition *)
lemma inv_partition_approx: "inv_partition S V P  approximation_miv Δ S"
proof -
  assume H1: "inv_partition S V P"
  then have "independent_vertices E S" unfolding inv_partition_def inv_iv_def by auto
  moreover have "independent_vertices E S'  card S'  card S * Δ" for S'
  proof -
    let ?I = "{S'  p | p. p  P}"
    (* split the optimal solution among the sets of P, which cover V so no element is
       lost. We obtain a cover of S' and show the required bound on its cardinality *)
    assume H2: "independent_vertices E S'"
    then have "S'  V" unfolding independent_vertices_def using vertices.simps by blast
    with H1 have "S' = S'  P" unfolding inv_partition_def by auto
    then have "S' = (p  P. S'  p)" using Int_Union by auto
    then have "S' = ?I" by blast
    moreover have "finite S'" using H2 and independent_vertices_finite by auto
    then have "p  P  finite (S'  p)" for p by auto
    ultimately have "card S'  sum card ?I" using card_Union_le_sum_card [of ?I] by auto
    also have "...  card ?I * Δ"
      using x_or_neighbors [of P S']
        and sum_card [of ?I Δ]
        and H1 and H2 unfolding inv_partition_def by auto
    also have "...  card P * Δ"
    proof -
      have "finite P" using H1 unfolding inv_partition_def by auto
      then have "card ?I  card P"
        using Setcompr_eq_image [of "λp. S'  p" P]
          and card_image_le unfolding inv_partition_def by auto
      then show ?thesis by auto
    qed
    also have "... = card S * Δ" using H1 unfolding inv_partition_def by auto
    ultimately show "card S'  card S * Δ" by auto
  qed
  ultimately show "approximation_miv Δ S" unfolding approximation_miv_def by auto
qed

theorem wei_approx_Δ:
"VARS (S :: 'a set) (X :: 'a set) (x :: 'a)
  { True }
  S := {};
  X := {};
  WHILE X  V
  INV { P. inv_partition S X P }
  DO x := (SOME x. x  V - X);
     S := insert x S;
     X := X  neighbors x  {x}
  OD
  { approximation_miv Δ S }"
proof (vcg, goal_cases)
  case (1 S X x) (* invariant initially true *)
  (* the invariant is initially true with the ghost variable P := {} *)
  have "inv_partition {} {} {}" unfolding inv_partition_def inv_iv_def independent_vertices_def by auto
  then show ?case by auto
next
  case (2 S X x) (* invariant preserved by loop *)
  (* definedness of assignment *)
  let ?x = "(SOME x. x  V - X)"
  from 2 obtain P where I: "inv_partition S X P" by auto 
  then have "V - X  {}" using 2 unfolding inv_partition_def by auto
  then have "?x  V - X" using some_in_eq by metis
  (* show that the invariant is true with the ghost variable P := insert ({?x} ∪ neighbors ?x) P *)
  with I have "inv_partition (insert ?x S) (X  neighbors ?x  {?x}) (insert ({?x}  neighbors ?x) P)"
    using inv_partition_preserv by blast
  then show ?case by auto
next
  case (3 S X x) (* invariant implies post-condition *)
  then show ?case using inv_partition_approx unfolding inv_approx_def by auto
qed

subsection "Wei's algorithm with dynamically computed approximation ratio"

text ‹In this subsection, we augment the algorithm with a variable used to compute the effective approximation ratio of the solution. In addition, the vertex of smallest degree is picked. With this heuristic, the algorithm achieves an approximation ratio of (Δ+2)/3›, but this is not proved here.›

definition vertex_heuristic :: "'a set  'a  bool" where
"vertex_heuristic X v = (u  V - X. card (neighbors v - X)  card (neighbors u - X))"

(* this lemma is needed to show that there exist a vertex to be picked by the heuristic *)
lemma ex_min_finite_set:
  fixes S :: "'a set"
    and f :: "'a  nat"
    shows "finite S  S  {}  x. x  S  (y  S. f x  f y)"
          (is "?P1  ?P2  x. ?minf S x")
proof (induct S rule: finite_ne_induct)
  case (singleton x)
  have "?minf {x} x" by auto
  then show ?case by auto
next
  case (insert x F)
  from insert(4) obtain y where Py: "?minf F y" by auto
  show "z. ?minf (insert x F) z"
  proof cases
    assume "f x < f y"
    then have "?minf (insert x F) x" using Py by auto
    then show ?case by auto
  next
    assume "¬f x < f y"
    then have "?minf (insert x F) y" using Py by auto
    then show ?case by auto
  qed
qed

lemma inv_approx_preserv2:
  fixes S :: "'a set"
    and X :: "'a set"
    and s :: nat
    and x :: "'a"
  assumes inv: "inv_approx S X s"
      and x_def: "x  V - X"
    shows "inv_approx (insert x S) (X  neighbors x  {x}) (max (card (neighbors x  {x} - X)) s)"
proof -
  have finite_S: "finite S" using inv and independent_vertices_finite unfolding inv_approx_def inv_iv_def by auto
  have Sx: "x  S" using inv and x_def unfolding inv_approx_def inv_iv_def by blast
  (* main invariant is preserved *)
  from inv have "inv_iv S X" unfolding inv_approx_def by auto
  with x_def have "inv_iv (insert x S) (X  neighbors x  {x})"
  proof (intro inv_preserv, auto) qed
  (* the approximation ratio is preserved *)
  moreover have "card (X  neighbors x  {x})  card (insert x S) * max (card (neighbors x  {x} - X)) s"
  proof -
    let ?N = "neighbors x  {x} - X"
    have "card (X  ?N)  card X + card ?N" using card_Un_le [of X ?N] by auto
    also have "...  card S * s + card ?N" using inv unfolding inv_approx_def by auto
    also have "...  card S * max (card ?N) s + card ?N" by auto
    also have "...  card S * max (card ?N) s + max (card ?N) s" by auto
    also have "... = card (insert x S) * max (card ?N) s" using Sx and finite_S by auto
    finally show ?thesis by auto
  qed
  (* conclusion *)
  ultimately show "inv_approx (insert x S) (X  neighbors x  {x}) (max (card (neighbors x  {x} - X)) s)"
    unfolding inv_approx_def by auto
qed

theorem wei_approx_min_degree_heuristic:
"VARS (S :: 'a set) (X :: 'a set) (x :: 'a) (r :: nat)
  { True }
  S := {};
  X := {};
  r := 0;
  WHILE X  V
  INV { inv_approx S X r }
  DO x := (SOME x. x  V - X  vertex_heuristic X x);
     S := insert x S;
     r := max (card (neighbors x  {x} - X)) r;
     X := X  neighbors x  {x}
  OD
  { approximation_miv r S }"
proof (vcg, goal_cases)
  case (1 S X x r) (* invariant initially true *)
  then show ?case unfolding inv_approx_def inv_iv_def independent_vertices_def by auto
next
  case (2 S X x r) (* invariant preserved by loop *)
  (* definedness of assignment *)
  let ?x = "(SOME x. x  V - X  vertex_heuristic X x)"
  have "V - X  {}" using 2 unfolding inv_approx_def inv_iv_def by blast
  moreover have "finite (V - X)" using 2 and finite_V by auto
  ultimately have "x. x  V - X  vertex_heuristic X x"
    using ex_min_finite_set [where ?f = "λx. card (neighbors x - X)"]
    unfolding vertex_heuristic_def by auto
  then have x_def: "?x  V - X  vertex_heuristic X ?x"
    using someI_ex [where ?P = "λx. x  V - X  vertex_heuristic X x"] by auto
  with 2 show ?case using inv_approx_preserv2 by auto
next
  case (3 S X x r)
  then show ?case using inv_approx unfolding inv_approx_def inv_iv_def by auto
qed

end
end

Theory Approx_LB_Hoare

section ‹Load Balancing›

theory Approx_LB_Hoare
  imports Complex_Main "HOL-Hoare.Hoare_Logic"
begin

text ‹This is a formalization of the load balancing algorithms and proofs
in the book by Kleinberg and Tardos \cite{KleinbergT06}.›

hide_const (open) sorted

(* TODO: mv *)

lemma sum_le_card_Max: " finite A; A  {}   sum f A  card A * Max (f ` A)"
proof(induction A rule: finite_ne_induct)
  case (singleton x)
  then show ?case by simp
next
  case (insert x F)
  then show ?case by (auto simp: max_def order.trans[of "sum f F" "card F * Max (f ` F)"])
qed

lemma Max_const[simp]: " finite A; A  {}   Max ((λ_. c) ` A) = c"
using Max_in image_is_empty by blast

abbreviation Max0 :: "nat set  nat" where
"Max0 N  (if N={} then 0 else Max N)"

fun f_Max0 :: "(nat  nat)  nat  nat" where
  "f_Max0 f 0 = 0"
| "f_Max0 f (Suc x) = max (f (Suc x)) (f_Max0 f x)"

lemma f_Max0_equiv: "f_Max0 f n = Max0 (f ` {1..n})"
  by (induction n) (auto simp: not_le atLeastAtMostSuc_conv)

lemma f_Max0_correct:
  "x  {1..m}. T x  f_Max0 T m"
  "m > 0  x  {1..m}. T x = f_Max0 T m"
   apply (induction m)
     apply simp_all
   apply (metis atLeastAtMost_iff le_Suc_eq max.cobounded1 max.coboundedI2)
  subgoal for m by (cases m = 0) (auto simp: max_def)
  done

lemma f_Max0_mono:
  "y  T x  f_Max0 (T (x := y)) m  f_Max0 T m"
  "T x  y  f_Max0 T m  f_Max0 (T (x := y)) m"
  by (induction m) auto

lemma f_Max0_out_of_range [simp]:
  "x  {1..k}  f_Max0 (T (x := y)) k = f_Max0 T k"
  by (induction k) auto

lemma fun_upd_f_Max0:
  assumes "x  {1..m}" "T x  y"
  shows "f_Max0 (T (x := y)) m = max y (f_Max0 T m)"
  using assms by (induction m) auto

locale LoadBalancing = (* Load Balancing *)
  fixes t :: "nat  nat"
    and m :: nat
    and n :: nat
  assumes m_gt_0: "m > 0"
begin

subsection ‹Formalization of a Correct Load Balancing›

subsubsection ‹Definition›

definition lb :: "(nat  nat)  (nat  nat set)  nat  bool" where
  "lb T A j = ((x  {1..m}. y  {1..m}. x  y  A x  A y = {}) ― ‹No job is assigned to more than one machine›
              (x  {1..m}. A x) = {1..j} ― ‹Every job is assigned›
              (x  {1..m}. (j  A x. t j) = T x) ― ‹The processing times sum up to the correct load›)"

abbreviation makespan :: "(nat  nat)  nat" where
  "makespan T  f_Max0 T m"

lemma makespan_def': "makespan T = Max (T ` {1..m})"
  using m_gt_0 by (simp add: f_Max0_equiv)
(*
lemma makespan_correct:
  "∀x ∈ {1..m}. T x ≤ makespan T m"
  "m > 0 ⟹ ∃x ∈ {1..m}. T x = makespan T m"
   apply (induction m)
     apply simp_all
   apply (metis atLeastAtMost_iff le_Suc_eq max.cobounded1 max.coboundedI2)
  subgoal for m by (cases ‹m = 0›) (auto simp: max_def)
  done

lemma no_machines_lb_iff_no_jobs: "lb T A j 0 ⟷ j = 0"
  unfolding lb_def by auto

lemma machines_if_jobs: "⟦ lb T A j m; j > 0 ⟧ ⟹ m > 0"
  using no_machines_lb_iff_no_jobs by (cases m) auto
*)

lemma makespan_correct:
  "x  {1..m}. T x  makespan T"
  "x  {1..m}. T x = makespan T"
  using f_Max0_correct m_gt_0 by auto

lemma lbE:
  assumes "lb T A j"
  shows "x  {1..m}. y  {1..m}. x  y  A x  A y = {}"
        "(x  {1..m}. A x) = {1..j}"
        "x  {1..m}. (y  A x. t y) = T x"
  using assms unfolding lb_def by blast+

lemma lbI:
  assumes "x  {1..m}. y  {1..m}. x  y  A x  A y = {}"
          "(x  {1..m}. A x) = {1..j}"
          "x  {1..m}. (y  A x. t y) = T x"
  shows "lb T A j" using assms unfolding lb_def by blast

lemma A_lb_finite [simp]:
  assumes "lb T A j" "x  {1..m}"
  shows "finite (A x)"
  by (metis lbE(2) assms finite_UN finite_atLeastAtMost)

text ‹If A x› is pairwise disjoint for all x ∈ {1..m}›, then the the sum over the sums of the
      individual A x› is equal to the sum over the union of all A x›.›
lemma sum_sum_eq_sum_Un:
  fixes A :: "nat  nat set"
  assumes "x  {1..m}. y  {1..m}. x  y  A x  A y = {}"
      and "x  {1..m}. finite (A x)"
  shows "(x  {1..m}. (y  A x. t y)) = (x  (y  {1..m}. A y). t x)"
  using assms
proof (induction m)
  case (Suc m)
  have FINITE: "finite (x  {1..m}. A x)" "finite (A (Suc m))"
    using Suc.prems(2) by auto
  have "x  {1..m}. A x  A (Suc m) = {}"
    using Suc.prems(1) by simp
  then have DISJNT: "(x  {1..m}. A x)  (A (Suc m)) = {}" using Union_disjoint by blast
  have "(x  (y  {1..m}. A y). t x) + (x  A (Suc m). t x)
      = (x  ((y  {1..m}. A y)  A (Suc m)). t x)"
    using sum.union_disjoint[OF FINITE DISJNT, symmetric] .
  also have "... = (x  (y  {1..Suc m}. A y). t x)"
    by (metis UN_insert image_Suc_lessThan image_insert inf_sup_aci(5) lessThan_Suc)
  finally show ?case using Suc by auto
qed simp

text ‹If T› and A› are a correct load balancing for j› jobs and m› machines, 
      then the sum of the loads has to be equal to the sum of the processing times of the jobs›
lemma lb_impl_job_sum:
  assumes "lb T A j"
  shows "(x  {1..m}. T x) = (x  {1..j}. t x)"
proof -
  note lbrules = lbE[OF assms]
  from assms have FINITE: "x  {1..m}. finite (A x)" by simp
  have "(x  {1..m}. T x) = (x  {1..m}. (y  A x. t y))"
    using lbrules(3) by simp
  also have "... = (x  {1..j}. t x)"
    using sum_sum_eq_sum_Un[OF lbrules(1) FINITE]
    unfolding lbrules(2) .
  finally show ?thesis .
qed

subsubsection ‹Lower Bounds for the Makespan›

text ‹If T› and A› are a correct load balancing for j› jobs and m› machines, then the processing time
      of any job x ∈ {1..j}› is a lower bound for the load of some machine y ∈ {1..m}›
lemma job_lower_bound_machine:
  assumes "lb T A j" "x  {1..j}"
  shows "y  {1..m}. t x  T y"
proof -
  note lbrules = lbE[OF assms(1)]
  have "y  {1..m}. x  A y" using lbrules(2) assms(2) by blast
  then obtain y where y_def: "y  {1..m}" "x  A y" ..
  moreover have "finite (A y)" using assms(1) y_def(1) by simp
  ultimately have "t x  (x  A y. t x)" using lbrules(1) member_le_sum by fast
  also have "... = T y" using lbrules(3) y_def(1) by blast
  finally show ?thesis using y_def(1) by blast
qed

text ‹As the load of any machine is a lower bound for the makespan, the processing time 
      of any job x ∈ {1..j}› has to also be a lower bound for the makespan.
      Follows from @{thm [source] job_lower_bound_machine} and @{thm [source] makespan_correct}.›
lemma job_lower_bound_makespan:
  assumes "lb T A j" "x  {1..j}"
  shows "t x  makespan T"
  by (meson job_lower_bound_machine[OF assms] makespan_correct(1) le_trans)

text ‹The makespan over j› jobs is a lower bound for the makespan of any correct load balancing for j› jobs.›
lemma max_job_lower_bound_makespan:
  assumes "lb T A j"
  shows "Max0 (t ` {1..j})  makespan T"
  using job_lower_bound_makespan[OF assms] by fastforce

lemma job_dist_lower_bound_makespan:
  assumes "lb T A j"
  shows "(x  {1..j}. t x) / m  makespan T"
proof -
  have "(x  {1..j}. t x)  m * makespan T"
    using assms lb_impl_job_sum[symmetric]
      and sum_le_card_Max[of "{1..m}"] m_gt_0 by (simp add: makespan_def')
  then have "real (x  {1..j}. t x)  real m * real (makespan T)"
    using of_nat_mono by fastforce
  then show ?thesis by (simp add: field_simps m_gt_0)
qed

subsection ‹The Greedy Approximation Algorithm›

text ‹This function will perform a linear scan from k ∈ {1..m}› and return the index of the machine with minimum load assuming m > 0›
fun mink :: "(nat  nat)  nat  nat" where
  "mink T 0 = 1"
| "mink T (Suc x) =
   (let k = mink T x
    in if T (Suc x) < T k then (Suc x) else k)"

lemma min_correct:
  "x  {1..m}. T (mink T m)  T x"
  by (induction m) (auto simp: Let_def le_Suc_eq, force)

lemma min_in_range:
  "k > 0  (mink T k)  {1..k}"
  by (induction k) (auto simp: Let_def, force+)

lemma add_job:
  assumes "lb T A j" "x  {1..m}"
  shows "lb (T (x := T x + t (Suc j))) (A (x := A x  {Suc j})) (Suc j)"
    (is ‹lb ?T ?A _)
proof -
  note lbrules = lbE[OF assms(1)]

  ― ‹Rule 1: @{term ?A} pairwise disjoint›
  have NOTIN: "i  {1..m}. Suc j  A i" using lbrules(2) assms(2) by force
  with lbrules(1) have "i  {1..m}. i  x  A i  (A x  {Suc j}) = {}"
    using assms(2) by blast
  then have 1: "x  {1..m}. y  {1..m}. x  y  ?A x  ?A y = {}"
    using lbrules(1) by simp

  ― ‹Rule 2: @{term ?A} contains all jobs›
  have "(y  {1..m}. ?A y) = (y  {1..m}. A y)  {Suc j}"
    using UNION_fun_upd assms(2) by auto
  also have "... = {1..Suc j}" unfolding lbrules(2) by auto
  finally have 2: "(y  {1..m}. ?A y) = {1..Suc j}" .

  ― ‹Rule 3: @{term ?A} sums to @{term ?T}
  have "(i  ?A x. t i) = (i  A x  {Suc j}. t i)" by simp
  moreover have "A x  {Suc j} = {}" using NOTIN assms(2) by blast
  moreover have "finite (A x)" "finite {Suc j}" using assms by simp+
  ultimately have "(i  ?A x. t i) = (i  A x. t i) + (i  {Suc j}. t i)"
    using sum.union_disjoint by simp
  also have "... = T x + t (Suc j)" using lbrules(3) assms(2) by simp
  finally have "(i  ?A x. t i) = ?T x" by simp
  then have 3: "i  {1..m}. (j  ?A i. t j) = ?T i"
    using lbrules(3) assms(2) by simp

  from lbI[OF 1 2 3] show ?thesis .
qed

lemma makespan_mono:
  "y  T x  makespan (T (x := y))  makespan T"
  "T x  y  makespan T  makespan (T (x := y))"
  using f_Max0_mono by auto

lemma smaller_optimum:
  assumes "lb T A (Suc j)"
  shows "T' A'. lb T' A' j  makespan T'  makespan T"
proof -
  note lbrules = lbE[OF assms]
  have "x  {1..m}. Suc j  A x" using lbrules(2) by auto
  then obtain x where x_def: "x  {1..m}" "Suc j  A x" ..
  let ?T = "T (x := T x - t (Suc j))"
  let ?A = "A (x := A x - {Suc j})"

  ― ‹Rule 1: @{term ?A} pairwise disjoint›
  from lbrules(1) have "i  {1..m}. i  x  A i  (A x - {Suc j}) = {}"
    using x_def(1) by blast
  then have 1: "x  {1..m}. y  {1..m}. x  y  ?A x  ?A y = {}"
    using lbrules(1) by auto

  ― ‹Rule 2: @{term ?A} contains all jobs›
  have NOTIN: "i  {1..m}. i  x  Suc j  A i" using lbrules(1) x_def by blast
  then have "(y  {1..m}. ?A y) = (y  {1..m}. A y) - {Suc j}"
    using UNION_fun_upd x_def by auto
  also have "... = {1..j}" unfolding lbrules(2) by auto
  finally have 2: "(y  {1..m}. ?A y) = {1..j}" .

  ― ‹Rule 3: @{term ?A} sums to @{term ?T}
  have "(i  A x - {Suc j}. t i) = (i  A x. t i) - t (Suc j)"
    by (simp add: sum_diff1_nat x_def(2))
  also have "... = T x - t (Suc j)" using lbrules(3) x_def(1) by simp
  finally have "(i  ?A x. t i) = ?T x" by simp
  then have 3: "i  {1..m}. (j  ?A i. t j) = ?T i"
    using lbrules(3) x_def(1) by simp

  ― ‹@{term makespan} is not larger›
  have "lb ?T ?A j  makespan ?T  makespan T"
    using lbI[OF 1 2 3] makespan_mono(1) by force
  then show ?thesis by blast
qed

text ‹If the processing time y› does not contribute to the makespan, we can ignore it.›
lemma remove_small_job:
  assumes "makespan (T (x := T x + y))  T x + y"
  shows   "makespan (T (x := T x + y)) = makespan T"
proof -
  let ?T = "T (x := T x + y)"
  have NOT_X: "makespan ?T  ?T x" using assms(1) by simp
  then have "i  {1..m}. makespan ?T = ?T i  i  x"
    using makespan_correct(2) by metis
  then obtain i where i_def: "i  {1..m}" "makespan ?T = ?T i" "i  x" by blast
  then have "?T i = T i" using NOT_X by simp
  moreover from this have "makespan T = T i"
    by (metis i_def(1,2) antisym_conv le_add1 makespan_mono(2) makespan_correct(1))
  ultimately show ?thesis using i_def(2) by simp
qed

lemma greedy_makespan_no_jobs [simp]:
  "makespan (λ_. 0) = 0"
  using m_gt_0 by (simp add: makespan_def')

lemma min_avg: "m * T (mink T m)  (i  {1..m}. T i)"
           (is _ * ?T  ?S)
proof -
  have "(_  {1..m}. ?T)  ?S"
    using sum_mono[of {1..m} λ_. ?T T]
      and min_correct by blast
  then show ?thesis by simp
qed

definition inv1 :: "(nat  nat)  (nat  nat set)  nat  bool" where
  "inv1 T A j = (lb T A j  j  n  (T' A'. lb T' A' j  makespan T  2 * makespan T'))"

lemma inv1E:
  assumes "inv1 T A j"
  shows "lb T A j" "j  n"
        "lb T' A' j  makespan T  2 * makespan T'"
  using assms unfolding inv1_def by blast+

lemma inv1I:
  assumes "lb T A j" "j  n" "T' A'. lb T' A' j  makespan T  2 * makespan T'"
  shows "inv1 T A j" using assms unfolding inv1_def by blast

lemma inv1_step:
  assumes "inv1 T A j" "j < n"
  shows "inv1 (T ((mink T m) := T (mink T m) + t (Suc j)))
              (A ((mink T m) := A (mink T m)  {Suc j})) (Suc j)"
    (is ‹inv1 ?T ?A _)
proof -
  note invrules = inv1E[OF assms(1)]
  ― ‹Greedy is correct›
  have LB: "lb ?T ?A (Suc j)"
    using add_job[OF invrules(1) min_in_range[OF m_gt_0]] by blast
  ― ‹Greedy maintains approximation factor›
  have MK: "T' A'. lb T' A' (Suc j)  makespan ?T  2 * makespan T'"
  proof rule+
    fix T1 A1 assume "lb T1 A1 (Suc j)"
    from smaller_optimum[OF this]
    obtain T0 A0 where "lb T0 A0 j" "makespan T0  makespan T1" by blast
    then have IH: "makespan T  2 * makespan T1"
      using invrules(3) by force
    show "makespan ?T  2 * makespan T1"
    proof (cases ‹makespan ?T = T (mink T m) + t (Suc j))
      case True
      have "m * T (mink T m)  (i  {1..m}. T i)" by (rule min_avg)
      also have "... = (i  {1..j}. t i)" by (rule lb_impl_job_sum[OF invrules(1)])
      finally have "real m * T (mink T m)  (i  {1..j}. t i)"
        by (auto dest: of_nat_mono)
      with m_gt_0 have "T (mink T m)  (i  {1..j}. t i) / m"
        by (simp add: field_simps)
      then have "T (mink T m)  makespan T1"
        using job_dist_lower_bound_makespan[OF ‹lb T0 A0 j] 
          and ‹makespan T0  makespan T1 by linarith
      moreover have "t (Suc j)  makespan T1"
        using job_lower_bound_makespan[OF ‹lb T1 A1 (Suc j)] by simp
      ultimately show ?thesis unfolding True by simp
    next
      case False show ?thesis using remove_small_job[OF False] IH by simp
    qed
  qed
  from inv1I[OF LB _ MK] show ?thesis using assms(2) by simp
qed

lemma simple_greedy_approximation:
"VARS T A i j
{True}
T := (λ_. 0);
A := (λ_. {});
j := 0;
WHILE j < n INV {inv1 T A j} DO
  i := mink T m;
  j := (Suc j);
  A := A (i := A(i)  {j});
  T := T (i := T(i) + t j)
OD
{lb T A n  (T' A'. lb T' A' n  makespan T  2 * makespan T')}"
proof (vcg, goal_cases)
  case (1 T A i j)
  then show ?case by (simp add: lb_def inv1_def)
next
  case (2 T A i j)
  then show ?case using inv1_step by simp
next
  case (3 T A i j)
  then show ?case unfolding inv1_def by force
qed

definition sorted :: "nat  bool" where
  "sorted j = (x  {1..j}. y  {1..x}. t x  t y)"

lemma sorted_smaller [simp]: " sorted j; j  j'   sorted j'"
  unfolding sorted_def by simp

lemma j_gt_m_pigeonhole:
  assumes "lb T A j" "j > m"
  shows "x  {1..j}. y  {1..j}. z  {1..m}. x  y  x  A z  y  A z"
proof -
  have "x  {1..j}. y  {1..m}. x  A y"
    using lbE(2)[OF assms(1)] by blast
  then have "f. x  {1..j}. x  A (f x)  f x  {1..m}" by metis
  then obtain f where f_def: "x  {1..j}. x  A (f x)  f x  {1..m}" ..
  then have "card (f ` {1..j})  card {1..m}"
    by (meson card_mono finite_atLeastAtMost image_subset_iff)
  also have "... < card {1..j}" using assms(2) by simp
  finally have "card (f ` {1..j}) < card {1..j}" .
  then have "¬ inj_on f {1..j}" using pigeonhole by blast
  then have "x  {1..j}. y  {1..j}. x  y  f x = f y"
    unfolding inj_on_def by blast
  then show ?thesis using f_def by metis
qed

text ‹If T› and A› are a correct load balancing for j› jobs and m› machines with j > m›,
      and the jobs are sorted in descending order, then there exists a machine x ∈ {1..m}›
      whose load is at least twice as large as the processing time of job j›.›
lemma sorted_job_lower_bound_machine:
  assumes "lb T A j" "j > m" "sorted j"
  shows "x  {1..m}. 2 * t j  T x"
proof -
  ― ‹Step 1: Obtaining the jobs›
  note lbrules = lbE[OF assms(1)]
  obtain j1 j2 x where *:
    "j1  {1..j}" "j2  {1..j}" "x  {1..m}" "j1  j2" "j1  A x" "j2  A x"
    using j_gt_m_pigeonhole[OF assms(1,2)] by blast

  ― ‹Step 2: Jobs contained in sum›
  have "finite (A x)" using assms(1) *(3) by simp
  then have SUM: "(i  A x. t i) = t j1 + t j2 + (i  A x - {j1} - {j2}. t i)"
    using *(4-6) by (simp add: sum.remove)

  ― ‹Step 3: Proof of lower bound›
  have "t j  t j1" "t j  t j2"
    using assms(3) *(1-2) unfolding sorted_def by auto
  then have "2 * t j  t j1 + t j2" by simp
  also have "...  (i  A x. t i)" unfolding SUM by simp
  finally have "2 * t j  T x" using lbrules(3) *(3) by simp
  then show ?thesis using *(3) by blast
qed

text ‹Reasoning analogous to @{thm [source] job_lower_bound_makespan}.›
lemma sorted_job_lower_bound_makespan:
  assumes "lb T A j" "j > m" "sorted j"
  shows "2 * t j  makespan T"
proof -
  obtain x where x_def: "x  {1..m}" "2 * t j  T x"
    using sorted_job_lower_bound_machine[OF assms] ..
  with makespan_correct(1) have "T x  makespan T" by blast
  with x_def(2) show ?thesis by simp
qed

lemma min_zero:
  assumes "x  {1..k}" "T x = 0"
  shows "T (mink T k) = 0"
  using assms(1)
proof (induction k)
  case (Suc k)
  show ?case proof (cases x = Suc k)
    case True
    then show ?thesis using assms(2) by (simp add: Let_def)
  next
    case False
    with Suc have "T (mink T k) = 0" by simp
    then show ?thesis by simp
  qed
qed simp

lemma min_zero_index:
  assumes "x  {1..k}" "T x = 0"
  shows "mink T k  x"
  using assms(1)
proof (induction k)
  case (Suc k)
  show ?case proof (cases x = Suc k)
    case True
    then show ?thesis using min_in_range[of "Suc k"] by simp
  next
    case False
    with Suc.prems have "x  {1..k}" by simp
    from min_zero[OF this, of T] assms(2) Suc.IH[OF this]
    show ?thesis by simp
  qed
qed simp

definition inv2 :: "(nat  nat)  (nat  nat set)  nat  bool" where
  "inv2 T A j = (lb T A j  j  n
                 (T' A'. lb T' A' j  makespan T  3 / 2 * makespan T') 
                 (x > j. T x = 0)
                 (j  m  makespan T = Max0 (t ` {1..j})))"

lemma inv2E:
  assumes "inv2 T A j"
  shows "lb T A j" "j  n"
        "lb T' A' j  makespan T  3 / 2 * makespan T'"
        "x > j. T x = 0" "j  m  makespan T = Max0 (t ` {1..j})"
  using assms unfolding inv2_def by blast+

lemma inv2I:
  assumes "lb T A j" "j  n"
          "T' A'. lb T' A' j  makespan T  3 / 2 * makespan T'"
          "x > j. T x = 0"
          "j  m  makespan T = Max0 (t ` {1..j})"
  shows "inv2 T A j"
  unfolding inv2_def using assms by blast

lemma inv2_step:
  assumes "sorted n" "inv2 T A j" "j < n"
  shows "inv2 (T (mink T m := T(mink T m) + t(Suc j)))
              (A (mink T m := A(mink T m)  {Suc j})) (Suc j)"
    (is ‹inv2 ?T ?A _)
proof (cases ‹Suc j > m)
  case True note invrules = inv2E[OF assms(2)]
  ― ‹Greedy is correct›
  have LB: "lb ?T ?A (Suc j)"
    using add_job[OF invrules(1) min_in_range[OF m_gt_0]] by blast
  ― ‹Greedy maintains approximation factor›
  have MK: "T' A'. lb T' A' (Suc j)  makespan ?T  3 / 2 * makespan T'"
  proof rule+
    fix T1 A1 assume "lb T1 A1 (Suc j)"
    from smaller_optimum[OF this]
    obtain T0 A0 where "lb T0 A0 j" "makespan T0  makespan T1" by blast
    then have IH: "makespan T  3 / 2 * makespan T1"
      using invrules(3) by force
    show "makespan ?T  3 / 2 * makespan T1"
    proof (cases ‹makespan ?T = T (mink T m) + t (Suc j))
      case True
      have "m * T (mink T m)  (i  {1..m}. T i)" by (rule min_avg)
      also have "... = (i  {1..j}. t i)" by (rule lb_impl_job_sum[OF invrules(1)])
      finally have "real m * T (mink T m)  (i  {1..j}. t i)"
        by (auto dest: of_nat_mono)
      with m_gt_0 have "T (mink T m)  (i  {1..j}. t i) / m"
        by (simp add: field_simps)
      then have "T (mink T m)  makespan T1"
        using job_dist_lower_bound_makespan[OF ‹lb T0 A0 j] 
          and ‹makespan T0  makespan T1 by linarith
      moreover have "2 * t (Suc j)  makespan T1"
        using sorted_job_lower_bound_makespan[OF ‹lb T1 A1 (Suc j) ‹Suc j > m]
          and assms(1,3) by simp
      ultimately show ?thesis unfolding True by simp
    next
      case False show ?thesis using remove_small_job[OF False] IH by simp
    qed
  qed
  have "x > Suc j. ?T x = 0"
    using invrules(4) min_in_range[OF m_gt_0, of T] True by simp
  with inv2I[OF LB _ MK] show ?thesis using assms(3) True by simp
next
  case False
  then have IN_RANGE: "Suc j  {1..m}" by simp
  note invrules = inv2E[OF assms(2)]
  then have "T (Suc j) = 0" by blast

  ― ‹Greedy is correct›
  have LB: "lb ?T ?A (Suc j)"
    using add_job[OF invrules(1) min_in_range[OF m_gt_0]] by blast

  ― ‹Greedy is trivially optimal›
  from IN_RANGE T (Suc j) = 0 have "mink T m  Suc j"
    using min_zero_index by blast
  with invrules(4) have EMPTY: "x > Suc j. ?T x = 0" by simp
  from IN_RANGE T (Suc j) = 0 have "T (mink T m) = 0"
    using min_zero by blast
  with fun_upd_f_Max0[OF min_in_range[OF m_gt_0]] invrules(5) False
  have TRIV: "makespan ?T = Max0 (t ` {1..Suc j})" unfolding f_Max0_equiv[symmetric] by simp
  have MK: "T' A'. lb T' A' (Suc j)  makespan ?T  3 / 2 * makespan T'"
    by (auto simp: TRIV[folded f_Max0_equiv]
            dest!: max_job_lower_bound_makespan[folded f_Max0_equiv])

  from inv2I[OF LB _ MK EMPTY TRIV] show ?thesis using assms(3) by simp
qed

lemma sorted_greedy_approximation:
"sorted n  VARS T A i j
{True}
T := (λ_. 0);
A := (λ_. {});
j := 0;
WHILE j < n INV {inv2 T A j} DO
  i := mink T m;
  j := (Suc j);
  A := A (i := A(i)  {j});
  T := T (i := T(i) + t j)
OD
{lb T A n  (T' A'. lb T' A' n  makespan T  3 / 2 * makespan T')}"
proof (vcg, goal_cases)
  case (1 T A i j)
  then show ?case by (simp add: lb_def inv2_def)
next
  case (2 T A i j)
  then show ?case using inv2_step by simp
next
  case (3 T A i j)
  then show ?case unfolding inv2_def by force
qed

end (* LoadBalancing *)

end (* Theory *)

Theory Approx_BP_Hoare

section ‹Bin Packing›

theory Approx_BP_Hoare
  imports Complex_Main "HOL-Hoare.Hoare_Logic" "HOL-Library.Disjoint_Sets"
begin

text ‹The algorithm and proofs are based on the work by Berghammer and Reuter @{cite BerghammerR03}.›

subsection ‹Formalization of a Correct Bin Packing›

text ‹Definition of the unary operator ⟦⋅⟧› from the article.
      B› will only be wrapped into a set if it is non-empty.›
definition wrap :: "'a set  'a set set" where
  "wrap B = (if B = {} then {} else {B})"

lemma wrap_card:
  "card (wrap B)  1"
  unfolding wrap_def by auto

text ‹If M› and N› are pairwise disjoint with V› and not yet contained in V,
      then the union of M› and N› is also pairwise disjoint with V›.›
lemma pairwise_disjnt_Un:
  assumes "pairwise disjnt ({M}  {N}  V)" "M  V" "N  V"
  shows "pairwise disjnt ({M  N}  V)"
  using assms unfolding pairwise_def by auto

text ‹A Bin Packing Problem is defined like in the article:›
locale BinPacking =
  fixes U :: "'a set" ― ‹A finite, non-empty set of objects›
    and w :: "'a  real" ― ‹A mapping from objects to their respective weights (positive real numbers)›
    and c :: nat ― ‹The maximum capacity of a bin (a natural number)›
    and S :: "'a set" ― ‹The set of small› objects (weight no larger than 1/2› of c›)›
    and L :: "'a set" ― ‹The set of large› objects (weight larger than 1/2› of c›)›
  assumes weight: "u  U. 0 < w(u)  w(u)  c"
      and U_Finite: "finite U"
      and U_NE: "U  {}"
      and S_def: "S = {u  U. w(u)  c / 2}"
      and L_def: "L = U - S"
begin

text ‹In the article, this is defined as w› as well. However, to avoid ambiguity,
      we will abbreviate the weight of a bin as W›.›
abbreviation W :: "'a set  real" where
  "W B  (u  B. w(u))"

text P› constitutes as a correct bin packing if P› is a partition of U›
      (as defined in @{thm [source] partition_on_def}) and the weights of
      the bins do not exceed their maximum capacity c›.›
definition bp :: "'a set set  bool" where
  "bp P  partition_on U P  (B  P. W(B)  c)"

lemma bpE:
  assumes "bp P"
  shows "pairwise disjnt P" "{}  P" "P = U" "B  P. W(B)  c"
  using assms unfolding bp_def partition_on_def by blast+

lemma bpI:
  assumes "pairwise disjnt P" "{}  P" "P = U" "B  P. W(B)  c"
  shows "bp P"
  using assms unfolding bp_def partition_on_def by blast

text ‹Although we assume the S› and L› sets as given, manually obtaining them from U› is trivial
      and can be achieved in linear time. Proposed by the article @{cite "BerghammerR03"}.›
lemma S_L_set_generation:
"VARS S L W u
  {True}
  S := {}; L := {}; W := U;
  WHILE W  {}
  INV {W  U  S = {v  U - W. w(v)  c / 2}  L = {v  U - W. w(v) > c / 2}} DO
    u := (SOME u. u  W);
    IF 2 * w(u)  c
    THEN S := S  {u}
    ELSE L := L  {u} FI;
    W := W - {u}
  OD
  {S = {v  U. w(v)  c / 2}  L = {v  U. w(v) > c / 2}}"
  by vcg (auto simp: some_in_eq)

subsection ‹The Proposed Approximation Algorithm›

subsubsection ‹Functional Correctness›

text ‹According to the article, inv1 holds if P1 ∪ wrap B1 ∪ P2 ∪ wrap B2 ∪ {{v} |v. v ∈ V}›
      is a correct solution for the bin packing problem @{cite BerghammerR03}. However, various
      assumptions made in the article seem to suggest that more information is demanded from this
      invariant and, indeed, mere correctness (as defined in @{thm [source] bp_def}) does not appear to suffice.
      To amend this, four additional conjuncts have been added to this invariant, whose necessity
      will be explained in the following proofs. It should be noted that there may be other (shorter) ways to amend this invariant.
      This approach, however, makes for rather straight-forward proofs, as these conjuncts can be utilized and proved in relatively few steps.›
definition inv1 :: "'a set set  'a set set  'a set  'a set  'a set  bool" where
  "inv1 P1 P2 B1 B2 V  bp (P1  wrap B1  P2  wrap B2  {{v} |v. v  V}) ― ‹A correct solution to the bin packing problem›
                        (P1  wrap B1  P2  wrap B2) = U - V ― ‹The partial solution does not contain objects that have not yet been assigned›
                        B1  (P1  P2  wrap B2) ― ‹B1 is distinct from all the other bins›
                        B2  (P1  wrap B1  P2) ― ‹B2 is distinct from all the other bins›
                        (P1  wrap B1)  (P2  wrap B2) = {} ― ‹The first and second partial solutions are disjoint from each other.›"
(*
lemma "partition_on U (P1 ∪ wrap B1 ∪ P2 ∪ wrap B2 ∪ {{v} |v. v ∈ V}) ⟹ u ∈ V ⟹
partition_on U (P1 ∪ wrap (insert u B1) ∪ P2 ∪ wrap B2 ∪ {{v} |v. v ∈ (V-{u})})"
  nitpick*)
lemma inv1E:
  assumes "inv1 P1 P2 B1 B2 V"
  shows "bp (P1  wrap B1  P2  wrap B2  {{v} |v. v  V})"
    and "(P1  wrap B1  P2  wrap B2) = U - V"
    and "B1  (P1  P2  wrap B2)"
    and "B2  (P1  wrap B1  P2)"
    and "(P1  wrap B1)  (P2  wrap B2) = {}"
  using assms unfolding inv1_def by auto

lemma inv1I:
  assumes "bp (P1  wrap B1  P2  wrap B2  {{v} |v. v  V})"
    and "(P1  wrap B1  P2  wrap B2) = U - V"
    and "B1  (P1  P2  wrap B2)"
    and "B2  (P1  wrap B1  P2)"
    and "(P1  wrap B1)  (P2  wrap B2) = {}"
  shows "inv1 P1 P2 B1 B2 V"
  using assms unfolding inv1_def by blast

lemma wrap_Un [simp]: "wrap (M  {x}) = {M  {x}}" unfolding wrap_def by simp
lemma wrap_empty [simp]: "wrap {} = {}" unfolding wrap_def by simp
lemma wrap_not_empty [simp]: "M  {}  wrap M = {M}" unfolding wrap_def by simp

text ‹If inv1 holds for the current partial solution, and the weight of an object u ∈ V› added to B1 does
      not exceed its capacity, then inv1 also holds if B1 and {u}› are replaced by B1 ∪ {u}›.›
lemma inv1_stepA:
  assumes "inv1 P1 P2 B1 B2 V" "u  V" "W(B1) + w(u)  c"
  shows "inv1 P1 P2 (B1  {u}) B2 (V - {u})"
proof -
  note invrules = inv1E[OF assms(1)] and bprules = bpE[OF invrules(1)]

  text ‹In the proof for Theorem 3.2› of the article it is erroneously argued that
        if P1 ∪ wrap B1 ∪ P2 ∪ wrap B2 ∪ {{v} |v. v ∈ V}› is a partition of U›,
        then the same holds if B1 is replaced by B1 ∪ {u}›.
        This is, however, not necessarily the case if B1 or {u}› are already contained in the partial solution.
        Suppose P1 contains the non-empty bin B1, then P1 ∪ wrap B1 would still be pairwise disjoint, provided P1 was pairwise disjoint before, as the union simply ignores the duplicate B1. Now, if the algorithm modifies B1 by adding an element from V› such that B1 becomes some non-empty B1'› with B1 ∩ B1' ≠ ∅› and B1' ∉ P1, one can see that this property would no longer be preserved.
        To avoid such a situation, we will use the first additional conjunct in inv1 to ensure that {u}›
        is not yet contained in the partial solution, and the second additional conjunct to ensure that B1
        is not yet contained in the partial solution.›

  ― ‹Rule 1: Pairwise Disjoint›
  have NOTIN: "M  P1  wrap B1  P2  wrap B2  {{v} |v. v  V - {u}}. u  M"
    using invrules(2) assms(2) by blast
  have "{{v} |v. v  V} = {{u}}  {{v} |v. v  V - {u}}"
    using assms(2) by blast
  then have "pairwise disjnt (P1  wrap B1  P2  wrap B2  ({{u}}  {{v} |v. v  V - {u}}))"
    using bprules(1) assms(2) by simp
  then have "pairwise disjnt (wrap B1  {{u}}  P1  P2  wrap B2  {{v} |v. v  V - {u}})" by (simp add: Un_commute)
  then have assm: "pairwise disjnt (wrap B1  {{u}}  (P1  P2  wrap B2  {{v} |v. v  V - {u}}))" by (simp add: Un_assoc)
  have "pairwise disjnt ({B1  {u}}  (P1  P2  wrap B2  {{v} |v. v  V - {u}}))"
  proof (cases B1 = {})
    case True with assm show ?thesis by simp
  next
    case False
    with assm have assm: "pairwise disjnt ({B1}  {{u}}  (P1  P2  wrap B2  {{v} |v. v  V - {u}}))" by simp
    from NOTIN have "{u}  P1  P2  wrap B2  {{v} |v. v  V - {u}}" by blast
    from pairwise_disjnt_Un[OF assm _ this] invrules(2,3) show ?thesis
      using False by auto
  qed
  then have 1: "pairwise disjnt (P1  wrap (B1  {u})  P2  wrap B2  {{v} |v. v  V - {u}})"
    unfolding wrap_Un by simp

  ― ‹Rule 2: No empty sets›
  from bprules(2) have 2: "{}  P1  wrap (B1  {u})  P2  wrap B2  {{v} |v. v  V - {u}}"
    unfolding wrap_def by simp

  ― ‹Rule 3: Union preserved›
  from bprules(3) have " (P1  wrap B1  P2  wrap B2  {{u}}  {{v} |v. v  V - {u}}) = U"
    using assms(2) by blast
  then have 3: " (P1  wrap (B1  {u})  P2  wrap B2  {{v} |v. v  V - {u}}) = U"
    unfolding wrap_def by force

  ― ‹Rule 4: Weights below capacity›
  have "0 < w u" using weight assms(2) bprules(3) by blast
  have "finite B1" using bprules(3) U_Finite by (cases B1 = {}) auto
  then have "W (B1  {u})  W B1 + w u" using 0 < w u by (cases u  B1) (auto simp: insert_absorb)
  also have "...  c" using assms(3) .
  finally have "W (B1  {u})  c" .
  then have "B  wrap (B1  {u}). W B  c" unfolding wrap_Un by blast
  moreover have "BP1  P2  wrap B2  {{v} |v. v  V - {u}}. W B  c"
    using bprules(4) by blast
  ultimately have 4: "BP1  wrap (B1  {u})  P2  wrap B2  {{v} |v. v  V - {u}}. W B  c" by blast
  from bpI[OF 1 2 3 4] have 1: "bp (P1  wrap (B1  {u})  P2  wrap B2  {{v} |v. v  V - {u}})" .

  ― ‹Auxiliary information is preserved›
  have "u  U" using assms(2) bprules(3) by blast
  then have R: "U - (V - {u}) = U - V  {u}" by blast
  have L: " (P1  wrap (B1  {u})  P2  wrap B2) =  (P1  wrap B1  P2  wrap B2)  {u}"
    unfolding wrap_def using NOTIN by auto
  have 2: " (P1  wrap (B1  {u})  P2  wrap B2) = U - (V - {u})"
    unfolding L R invrules(2) ..
  have 3: "B1  {u}  P1  P2  wrap B2"
    using NOTIN by auto
  have 4: "B2  P1  wrap (B1  {u})  P2"
    using invrules(4) NOTIN unfolding wrap_def by fastforce
  have 5: "(P1  wrap (B1  {u}))  (P2  wrap B2) = {}"
    using invrules(5) NOTIN unfolding wrap_Un by auto

  from inv1I[OF 1 2 3 4 5] show ?thesis .
qed

text ‹If inv1 holds for the current partial solution, and the weight of an object u ∈ V› added to B2 does
      not exceed its capacity, then inv1 also holds if B2 and {u}› are replaced by B2 ∪ {u}›.›
lemma inv1_stepB:
  assumes "inv1 P1 P2 B1 B2 V" "u  V" "W B2 + w u  c"
  shows "inv1 (P1  wrap B1) P2 {} (B2  {u}) (V - {u})"
proof -
  note invrules = inv1E[OF assms(1)] and bprules = bpE[OF invrules(1)]

text ‹The argumentation here is similar to the one in @{thm [source] inv1_stepA} with
      B1 replaced with B2 and using the first and third additional conjuncts of inv1
      to amend the issue, instead of the first and second.›
  ― ‹Rule 1: Pairwise Disjoint›
  have NOTIN: "M  P1  wrap B1  P2  wrap B2  {{v} |v. v  V - {u}}. u  M"
    using invrules(2) assms(2) by blast
  have "{{v} |v. v  V} = {{u}}  {{v} |v. v  V - {u}}"
    using assms(2) by blast
  then have "pairwise disjnt (P1  wrap B1  P2  wrap B2  {{u}}  {{v} |v. v  V - {u}})"
    using bprules(1) assms(2) by simp
  then have assm: "pairwise disjnt (wrap B2  {{u}}  (P1  wrap B1  P2  {{v} |v. v  V - {u}}))"
    by (simp add: Un_assoc Un_commute)
  have "pairwise disjnt ({B2  {u}}  (P1  wrap B1  P2  {{v} |v. v  V - {u}}))"
  proof (cases B2 = {})
    case True with assm show ?thesis by simp
  next
    case False
    with assm have assm: "pairwise disjnt ({B2}  {{u}}  (P1  wrap B1  P2  {{v} |v. v  V - {u}}))" by simp
    from NOTIN have "{u}  P1  wrap B1  P2  {{v} |v. v  V - {u}}" by blast
    from pairwise_disjnt_Un[OF assm _ this] invrules(2,4) show ?thesis
      using False by auto
  qed
  then have 1: "pairwise disjnt (P1  wrap B1  wrap {}  P2  wrap (B2  {u})  {{v} |v. v  V - {u}})"
    unfolding wrap_Un by simp

  ― ‹Rule 2: No empty sets›
  from bprules(2) have 2: "{}  P1  wrap B1  wrap {}  P2  wrap (B2  {u})  {{v} |v. v  V - {u}}"
    unfolding wrap_def by simp

  ― ‹Rule 3: Union preserved›
  from bprules(3) have " (P1  wrap B1  P2  wrap B2  {{u}}  {{v} |v. v  V - {u}}) = U"
    using assms(2) by blast
  then have 3: " (P1  wrap B1  wrap {}  P2  wrap (B2  {u})  {{v} |v. v  V - {u}}) = U"
    unfolding wrap_def by force

  ― ‹Rule 4: Weights below capacity›
  have "0 < w u" using weight assms(2) bprules(3) by blast
  have "finite B2" using bprules(3) U_Finite by (cases B2 = {}) auto
  then have "W (B2  {u})  W B2 + w u" using 0 < w u by (cases u  B2) (auto simp: insert_absorb)
  also have "...  c" using assms(3) .
  finally have "W (B2  {u})  c" .
  then have "B  wrap (B2  {u}). W B  c" unfolding wrap_Un by blast
  moreover have "BP1  wrap B1  P2  {{v} |v. v  V - {u}}. W B  c"
    using bprules(4) by blast
  ultimately have 4: "BP1  wrap B1  wrap {}  P2  wrap (B2  {u})  {{v} |v. v  V - {u}}. W B  c"
    by auto
  from bpI[OF 1 2 3 4] have 1: "bp (P1  wrap B1  wrap {}  P2  wrap (B2  {u})  {{v} |v. v  V - {u}})" .

  ― ‹Auxiliary information is preserved›
  have "u  U" using assms(2) bprules(3) by blast
  then have R: "U - (V - {u}) = U - V  {u}" by blast
  have L: " (P1  wrap B1  wrap {}  P2  wrap (B2  {u})) =  (P1  wrap B1  wrap {}  P2  wrap B2)  {u}"
    unfolding wrap_def using NOTIN by auto
  have 2: " (P1  wrap B1  wrap {}  P2  wrap (B2  {u})) = U - (V - {u})"
    unfolding L R using invrules(2) by simp
  have 3: "{}  P1  wrap B1  P2  wrap (B2  {u})"
    using bpE(2)[OF 1] by simp
  have 4: "B2  {u}  P1  wrap B1  wrap {}  P2"
    using NOTIN by auto
  have 5: "(P1  wrap B1  wrap {})  (P2  wrap (B2  {u})) = {}"
    using invrules(5) NOTIN unfolding wrap_empty wrap_Un by auto

  from inv1I[OF 1 2 3 4 5] show ?thesis .
qed

text ‹If inv1 holds for the current partial solution, then inv1 also holds if B1 and B2 are
      added to P1 and P2 respectively, B1 is emptied and B2 initialized with u ∈ V›.›
lemma inv1_stepC:
  assumes "inv1 P1 P2 B1 B2 V" "u  V"
  shows "inv1 (P1  wrap B1) (P2  wrap B2) {} {u} (V - {u})"
proof -
  note invrules = inv1E[OF assms(1)]
  ― ‹Rule 1-4: Correct Bin Packing›
  have "P1  wrap B1  wrap {}  (P2  wrap B2)  wrap {u}  {{v} |v. v  V - {u}}
      = P1  wrap B1  P2  wrap B2  {{u}}  {{v} |v. v  V - {u}}"
    by (metis (no_types, lifting) Un_assoc Un_empty_right insert_not_empty wrap_empty wrap_not_empty)
  also have "... = P1  wrap B1  P2  wrap B2  {{v} |v. v  V}"
    using assms(2) by auto
  finally have EQ: "P1  wrap B1  wrap {}  (P2  wrap B2)  wrap {u}  {{v} |v. v  V - {u}}
                  = P1  wrap B1  P2  wrap B2  {{v} |v. v  V}" .
  from invrules(1) have 1: "bp (P1  wrap B1  wrap {}  (P2  wrap B2)  wrap {u}  {{v} |v. v  V - {u}})"
    unfolding EQ .

  ― ‹Auxiliary information is preserved›
  have NOTIN: "M  P1  wrap B1  P2  wrap B2  {{v} |v. v  V - {u}}. u  M"
    using invrules(2) assms(2) by blast
  have "u  U" using assms(2) bpE(3)[OF invrules(1)] by blast
  then have R: "U - (V - {u}) = U - V  {u}" by blast
  have L: " (P1  wrap B1  wrap {}  (P2  wrap B2)  wrap {u}) =  (P1  wrap B1  wrap {}  (P2  wrap B2))  {u}"
    unfolding wrap_def using NOTIN by auto
  have 2: " (P1  wrap B1  wrap {}  (P2  wrap B2)  wrap {u}) = U - (V - {u})"
    unfolding L R using invrules(2) by auto
  have 3: "{}  P1  wrap B1  (P2  wrap B2)  wrap {u}"
    using bpE(2)[OF 1] by simp
  have 4: "{u}  P1  wrap B1  wrap {}  (P2  wrap B2)"
    using NOTIN by auto
  have 5: "(P1  wrap B1  wrap {})  (P2  wrap B2  wrap {u}) = {}"
    using invrules(5) NOTIN unfolding wrap_def by force

  from inv1I[OF 1 2 3 4 5] show ?thesis .
qed

text ‹A simplified version of the bin packing algorithm proposed in the article.
      It serves as an introduction into the approach taken, and, while it does not provide the desired
      approximation factor, it does ensure that P› is a correct solution of the bin packing problem.›
lemma simple_bp_correct:
"VARS P P1 P2 B1 B2 V u
  {True}
  P1 := {}; P2 := {}; B1 := {}; B2 := {}; V := U;
  WHILE V  S  {} INV {inv1 P1 P2 B1 B2 V} DO
    u := (SOME u. u  V); V := V - {u};
    IF W(B1) + w(u)  c
    THEN B1 := B1  {u}
    ELSE IF W(B2) + w(u)  c
         THEN B2 := B2  {u}
         ELSE P2 := P2  wrap B2; B2 := {u} FI;
         P1 := P1  wrap B1; B1 := {} FI
  OD;
  P := P1  wrap B1  P2  wrap B2  {{v} | v. v  V}
  {bp P}"
proof (vcg, goal_cases)
  case (1 P P1 P2 B1 B2 V u)
  show ?case
    unfolding bp_def partition_on_def pairwise_def wrap_def inv1_def
    using weight by auto
next
  case (2 P P1 P2 B1 B2 V u)
  then have INV: "inv1 P1 P2 B1 B2 V" ..
  from 2 have "V  {}" by blast
  then have IN: "(SOME u. u  V)  V" by (simp add: some_in_eq)
  from inv1_stepA[OF INV IN] inv1_stepB[OF INV IN] inv1_stepC[OF INV IN]
  show ?case by blast
next
  case (3 P P1 P2 B1 B2 V u)
  then show ?case unfolding inv1_def by blast
qed

subsubsection ‹Lower Bounds for the Bin Packing Problem›

lemma bp_bins_finite [simp]:
  assumes "bp P"
  shows "B  P. finite B"
  using bpE(3)[OF assms] U_Finite by (meson Sup_upper finite_subset)

lemma bp_sol_finite [simp]:
  assumes "bp P"
  shows "finite P"
  using bpE(3)[OF assms] U_Finite by (simp add: finite_UnionD)

text ‹If P› is a solution of the bin packing problem, then no bin in P› may contain more than
      one large object.›
lemma only_one_L_per_bin:
  assumes "bp P" "B  P"
  shows "x  B. y  B. x  y  x  L  y  L"
proof (rule ccontr, simp)
  assume "xB. yB. x  y  x  L  y  L"
  then obtain x y where *: "x  B" "y  B" "x  y" "x  L" "y  L" by blast
  then have "c < w x + w y" using L_def S_def by force
  have "finite B" using assms by simp
  have "y  B - {x}" using *(2,3) by blast
  have "W B = W (B - {x}) + w x"
    using *(1) ‹finite B by (simp add: sum.remove)
  also have "... = W (B - {x} - {y}) + w x + w y"
    using y  B - {x} ‹finite B by (simp add: sum.remove)
  finally have *: "W B = W (B - {x} - {y}) + w x + w y" .
  have "u  B. 0 < w u" using bpE(3)[OF assms(1)] assms(2) weight by blast
  then have "0  W (B - {x} - {y})" by (smt DiffD1 sum_nonneg)
  with * have "c < W B" using c < w x + w y by simp
  then show False using bpE(4)[OF assms(1)] assms(2) by fastforce
qed

text ‹If P› is a solution of the bin packing problem, then the amount of large objects
      is a lower bound for the amount of bins in P.›
lemma L_lower_bound_card:
  assumes "bp P"
  shows "card L  card P"
proof -
  have "x  L. B  P. x  B"
    using bpE(3)[OF assms] L_def by blast
  then obtain f where f_def: "u  L. u  f u  f u  P" by metis
  then have "inj_on f L"
    unfolding inj_on_def using only_one_L_per_bin[OF assms] by blast
  then have card_eq: "card L = card (f ` L)" by (simp add: card_image)
  have "f ` L  P" using f_def by blast
  moreover have "finite P" using assms by simp
  ultimately have "card (f ` L)  card P" by (simp add: card_mono)
  then show ?thesis unfolding card_eq .
qed

text ‹If P› is a solution of the bin packing problem, then the amount of bins of a subset of P
      in which every bin contains a large object is a lower bound on the amount of large objects.›
lemma subset_bp_card:
  assumes "bp P" "M  P" "B  M. B  L  {}"
  shows "card M  card L"
proof -
  have "B  M. u  L. u  B" using assms(3) by fast
  then have "f. B  M. f B  L  f B  B" by metis
  then obtain f where f_def: "B  M. f B  L  f B  B" ..
  have "inj_on f M"
  proof (rule ccontr)
    assume "¬ inj_on f M"
    then have "x  M. y  M. x  y  f x = f y" unfolding inj_on_def by blast
    then obtain x y where *: "x  M" "y  M" "x  y" "f x = f y" by blast
    then have "u. u  x  u  y" using f_def by metis
    then have "x  y  {}" by blast
    moreover have "pairwise disjnt M" using pairwise_subset[OF bpE(1)[OF assms(1)] assms(2)] .
    ultimately show False using * unfolding pairwise_def disjnt_def by simp
  qed
  moreover have "finite L" using L_def U_Finite by blast
  moreover have "f ` M  L" using f_def by blast
  ultimately show ?thesis using card_inj_on_le by blast
qed

text ‹If P› is a correct solution of the bin packing problem, inv1 holds for the partial solution,
      and every bin in P1 ∪ wrap B1 contains a large object, then the amount of bins in
      P1 ∪ wrap B1 ∪ {{v} |v. v ∈ V ∩ L}› is a lower bound for the amount of bins in P›.›
lemma L_bins_lower_bound_card:
  assumes "bp P" "inv1 P1 P2 B1 B2 V" "B  P1  wrap B1. B  L  {}"
  shows "card (P1  wrap B1  {{v} |v. v  V  L})  card P"
proof -
  note invrules = inv1E[OF assms(2)]
  have "B  {{v} |v. v  V  L}. B  L  {}" by blast
  with assms(3) have
    "P1  wrap B1  {{v} |v. v  V  L}  P1  wrap B1  P2  wrap B2  {{v} |v. v  V}"
    "B  P1  wrap B1  {{v} |v. v  V  L}. B  L  {}" by blast+
  from subset_bp_card[OF invrules(1) this] show ?thesis
    using L_lower_bound_card[OF assms(1)] by linarith
qed

text ‹If P› is a correct solution of the bin packing problem, then the sum of the weights of the
      objects is equal to the sum of the weights of the bins in P›.›
lemma sum_Un_eq_sum_sum:
  assumes "bp P"
  shows "(u  U. w u) = (B  P. W B)"
proof -
  have FINITE: "B  P. finite B" using assms by simp
  have DISJNT: "A  P. B  P. A  B  A  B = {}"
    using bpE(1)[OF assms] unfolding pairwise_def disjnt_def .
  have "(u  (P). w u) = (B  P. W B)"
    using sum.Union_disjoint[OF FINITE DISJNT] by auto
  then show ?thesis unfolding bpE(3)[OF assms] .
qed

text ‹If P› is a correct solution of the bin packing problem, then the sum of the weights of the items
      is a lower bound of amount of bins in P› multiplied by their maximum capacity.›
lemma sum_lower_bound_card:
  assumes "bp P"
  shows "(u  U. w u)  c * card P"
proof -
  have *: "B  P. 0 < W B  W B  c"
    using bpE(2-4)[OF assms] weight by (metis UnionI assms bp_bins_finite sum_pos)
  have "(u  U. w u) = (B  P. W B)"
    using sum_Un_eq_sum_sum[OF assms] .
  also have "...  (B  P. c)" using sum_mono * by fastforce
  also have "... = c * card P" by simp
  finally show ?thesis .
qed

lemma bp_NE:
  assumes "bp P"
  shows "P  {}"
  using U_NE bpE(3)[OF assms] by blast

lemma sum_Un_ge:
  fixes f :: "_  real"
  assumes "finite M" "finite N" "B  M  N. 0 < f B"
  shows "sum f M  sum f (M  N)"
proof -
  have "0  sum f N - sum f (M  N)"
    using assms by (smt DiffD1 inf.cobounded2 UnCI sum_mono2)
  then have "sum f M  sum f M + sum f N - sum f (M  N)"
    by simp
  also have "... = sum f (M  N)"
    using sum_Un[OF assms(1,2), symmetric] .
  finally show ?thesis .
qed

text ‹If bij_exists› holds, one can obtain a function which is bijective between the bins in P›
and the objects in V› such that an object returned by the function would cause the bin to
exceed its capacity.›
definition bij_exists :: "'a set set  'a set  bool" where
  "bij_exists P V = (f. bij_betw f P V  (B  P. W B + w (f B) > c))"

text ‹If P› is a functionally correct solution of the bin packing problem, inv1 holds for the
partial solution, and such a bijective function exists between the bins in P1 and the objects in
@{term "P2  wrap B2"}, the following strict lower bound can be shown:›
lemma P1_lower_bound_card:
  assumes "bp P" "inv1 P1 P2 B1 B2 V" "bij_exists P1 ((P2  wrap B2))"
  shows "card P1 + 1  card P"
proof (cases P1 = {})
  case True
  have "finite P" using assms(1) by simp
  then have "1  card P" using bp_NE[OF assms(1)]
    by (metis Nat.add_0_right Suc_diff_1 Suc_le_mono card_gt_0_iff le0 mult_Suc_right nat_mult_1)
  then show ?thesis unfolding True by simp
next
  note invrules = inv1E[OF assms(2)]
  case False
  obtain f where f_def: "bij_betw f P1 ((P2  wrap B2))" "B  P1. W B + w (f B) > c"
    using assms(3) unfolding bij_exists_def by blast
  have FINITE: "finite P1" "finite (P2  wrap B2)" "finite (P1  P2  wrap B2)" "finite (wrap B1  {{v} |v. v  V})"
    using inv1E(1)[OF assms(2)] bp_sol_finite by blast+

  have F: "B  P2  wrap B2. finite B" using invrules(1) by simp
  have D: "A  P2  wrap B2. B  P2  wrap B2. A  B  A  B = {}"
    using bpE(1)[OF invrules(1)] unfolding pairwise_def disjnt_def by auto
  have sum_eq: "W ( (P2  wrap B2)) = (B  P2  wrap B2. W B)"
    using sum.Union_disjoint[OF F D] by auto

  have "BP1  wrap B1  P2  wrap B2  {{v} |v. v  V}. 0 < W B"
    using bpE(2,3)[OF invrules(1)] weight by (metis (no_types, lifting) UnionI bp_bins_finite invrules(1) sum_pos)
  then have "(B  P1  P2  wrap B2. W B)  (B  P1  P2  wrap B2  (wrap B1  {{v} |v. v  V}). W B)"
    using sum_Un_ge[OF FINITE(3,4), of W] by blast
  also have "... = (B  P1  wrap B1  P2  wrap B2  {{v} |v. v  V}. W B)" by (smt Un_assoc Un_commute) 
  also have "... = W U" using sum_Un_eq_sum_sum[OF invrules(1), symmetric] .
  finally have *: "(B  P1  P2  wrap B2. W B)  W U" .

  ― ‹This follows from the fourth and final additional conjunct of inv1 and is necessary to combine the sums of the bins
      of the two partial solutions. This does not inherently follow from the union being a correct solution,
      as this need not be the case if P1 and P2 ∪ wrap B2 happened to be equal.›
  have DISJNT: "P1  (P2  wrap B2) = {}" using invrules(5) by blast

  ― ‹This part of the proof is based on the proof on page 72 of the article @{cite BerghammerR03}.›
  have "c * card P1 = (B  P1. c)" by simp
  also have "... < (B  P1. W B + w (f B))"
    using f_def(2) sum_strict_mono[OF FINITE(1) False] by fastforce
  also have "... = (B  P1. W B) + (B  P1. w (f B))"
    by (simp add: Groups_Big.comm_monoid_add_class.sum.distrib)
  also have "... = (B  P1. W B) + W ( (P2  wrap B2))" unfolding sum.reindex_bij_betw[OF f_def(1), of w] ..
  also have "... = (B  P1. W B) + (B  P2  wrap B2. W B)" unfolding sum_eq ..
  also have "... = (B  P1  P2  wrap B2. W B)" using sum.union_disjoint[OF FINITE(1,2) DISJNT, of W] by (simp add: Un_assoc)
  also have "...  (u  U. w u)" using * .
  also have "...  c * card P" using sum_lower_bound_card[OF assms(1)] .
  finally show ?thesis by (meson discrete nat_mult_less_cancel_disj of_nat_less_imp_less)
qed

text ‹As @{thm wrap_card} holds, it follows that the amount of bins in P1 ∪ wrap B1
      are a lower bound for the amount of bins in P›.›
lemma P1_B1_lower_bound_card:
  assumes "bp P" "inv1 P1 P2 B1 B2 V" "bij_exists P1 ((P2  wrap B2))"
  shows "card (P1  wrap B1)  card P"
proof -
  have "card (P1  wrap B1)  card P1 + card (wrap B1)"
    using card_Un_le by blast
  also have "...  card P1 + 1" using wrap_card by simp
  also have "...  card P" using P1_lower_bound_card[OF assms] .
  finally show ?thesis .
qed

text ‹If inv1 holds, there are at most half as many bins in P2 as there are objects in P2, and we can again
      obtain a bijective function between the bins in P1 and the objects of the second partial solution,
      then the amount of bins in the second partial solution are a strict lower bound for half the bins of
      the first partial solution.›
lemma P2_B2_lower_bound_P1:
  assumes "inv1 P1 P2 B1 B2 V" "2 * card P2  card (P2)" "bij_exists P1 ((P2  wrap B2))"
  shows "2 * card (P2  wrap B2)  card P1 + 1"
proof -
  note invrules = inv1E[OF assms(1)] and bprules = bpE[OF invrules(1)]

  have "pairwise disjnt (P2  wrap B2)"
    using bprules(1) pairwise_subset by blast
  moreover have "B2  P2" using invrules(4) by simp
  ultimately have DISJNT: "P2  B2 = {}"
    by (auto, metis (no_types, hide_lams) sup_bot.right_neutral Un_insert_right disjnt_iff mk_disjoint_insert pairwise_insert wrap_Un)

  have "finite (P2)" using U_Finite bprules(3) by auto
  have "finite B2" using bp_bins_finite[OF invrules(1)] wrap_not_empty by blast
  have "finite P2" "finite (wrap B2)" using bp_sol_finite[OF invrules(1)] by blast+
  have DISJNT2: "P2  wrap B2 = {}" unfolding wrap_def using B2  P2 by auto
  have "card (wrap B2)  card B2"
  proof (cases B2 = {})
    case False
    then have "1  card B2" by (simp add: leI ‹finite B2)
    then show ?thesis using wrap_card[of B2] by linarith
  qed simp

  ― ‹This part of the proof is based on the proof on page 73 of the article @{cite BerghammerR03}.›
  from assms(2) have "2 * card P2 + 2 * card (wrap B2)  card (P2) + card (wrap B2) + 1"
    using wrap_card[of B2] by linarith
  then have "2 * (card P2 + card (wrap B2))  card (P2) + card B2 + 1"
    using ‹card (wrap B2)  card B2 by simp
  then have "2 * (card (P2  wrap B2))  card (P2  B2) + 1"
    using card_Un_disjoint[OF ‹finite (P2) ‹finite B2 DISJNT]
      and card_Un_disjoint[OF ‹finite P2 ‹finite (wrap B2) DISJNT2] by argo
  then have "2 * (card (P2  wrap B2))  card ((P2  wrap B2)) + 1"
    by (cases B2 = {}) (auto simp: Un_commute)
  then show "2 * (card (P2  wrap B2))  card P1 + 1"
    using assms(3) bij_betw_same_card unfolding bij_exists_def by metis
qed

subsubsection ‹Proving the Approximation Factor›

text ‹We define inv2 as it is defined in the article.
      These conjuncts allow us to prove the desired approximation factor.›
definition inv2 :: "'a set set  'a set set  'a set  'a set  'a set  bool" where
  "inv2 P1 P2 B1 B2 V  inv1 P1 P2 B1 B2 V ― ‹inv1 holds for the partial solution›
                        (V  L  {}  (B  P1  wrap B1. B  L  {})) ― ‹If there are still large objects left, then every bin of the first partial solution must contain a large object›
                        bij_exists P1 ((P2  wrap B2)) ― ‹There exists a bijective function between the bins of the first partial solution and the objects of the second one›
                        (2 * card P2  card (P2)) ― ‹There are at most twice as many bins in P2 as there are objects in P2"

lemma inv2E:
  assumes "inv2 P1 P2 B1 B2 V"
  shows "inv1 P1 P2 B1 B2 V"
    and "V  L  {}  B  P1  wrap B1. B  L  {}"
    and "bij_exists P1 ((P2  wrap B2))"
    and "2 * card P2  card (P2)"
  using assms unfolding inv2_def by blast+

lemma inv2I:
  assumes "inv1 P1 P2 B1 B2 V"
    and "V  L  {}  B  P1  wrap B1. B  L  {}"
    and "bij_exists P1 ((P2  wrap B2))"
    and "2 * card P2  card (P2)"
  shows "inv2 P1 P2 B1 B2 V"
  using assms unfolding inv2_def by blast

text ‹If P› is a correct solution of the bin packing problem, inv2 holds for the partial solution,
      and there are no more small objects left to be distributed, then the amount of bins of the partial solution
      is no larger than 3 / 2› of the amount of bins in P›. This proof strongly follows the proof in
      Theorem 4.1› of the article @{cite BerghammerR03}.›
lemma bin_packing_lower_bound_card:
  assumes "V  S = {}" "inv2 P1 P2 B1 B2 V" "bp P"
  shows "card (P1  wrap B1  P2  wrap B2  {{v} |v. v  V})  3 / 2 * card P"
proof (cases V = {})
  note invrules = inv2E[OF assms(2)]
  case True
  then have "card (P1  wrap B1  P2  wrap B2  {{v} |v. v  V})
           = card (P1  wrap B1  P2  wrap B2)" by simp
  also have "...  card (P1  wrap B1) + card (P2  wrap B2)"
    using card_Un_le[of P1  wrap B1] by (simp add: Un_assoc)
  also have "...  card P + card (P2  wrap B2)"
    using P1_B1_lower_bound_card[OF assms(3) invrules(1,3)] by simp
  also have "...  card P + card P / 2"
    using P2_B2_lower_bound_P1[OF invrules(1,4,3)]
      and P1_lower_bound_card[OF assms(3) invrules(1,3)] by linarith
  finally show ?thesis by linarith
next
  note invrules = inv2E[OF assms(2)]
  case False
  have "U = S  L" using S_def L_def by blast
  then have *: "V = V  L"
    using bpE(3)[OF inv1E(1)[OF invrules(1)]]
      and assms(1) by blast
  with False have NE: "V  L  {}" by simp
  have "card (P1  wrap B1  P2  wrap B2  {{v} |v. v  V})
      = card (P1  wrap B1  {{v} |v. v  V  L}  P2  wrap B2)"
    using * by (simp add: Un_commute Un_assoc)
  also have "...  card (P1  wrap B1  {{v} |v. v  V  L}) + card (P2  wrap B2)"
    using card_Un_le[of P1  wrap B1  {{v} |v. v  V  L}] by (simp add: Un_assoc)
  also have "...  card P + card (P2  wrap B2)"
    using L_bins_lower_bound_card[OF assms(3) invrules(1) invrules(2)[OF NE]] by linarith
  also have "...  card P + card P / 2"
    using P2_B2_lower_bound_P1[OF invrules(1,4,3)]
      and P1_lower_bound_card[OF assms(3) invrules(1,3)] by linarith
  finally show ?thesis by linarith
qed

text ‹We define inv3 as it is defined in the article.
      This final conjunct allows us to prove that the invariant will be maintained by the algorithm.›
definition inv3 :: "'a set set  'a set set  'a set  'a set  'a set  bool" where
  "inv3 P1 P2 B1 B2 V  inv2 P1 P2 B1 B2 V  B2  S"

lemma inv3E:
  assumes "inv3 P1 P2 B1 B2 V"
  shows "inv2 P1 P2 B1 B2 V" and "B2  S"
  using assms unfolding inv3_def by blast+

lemma inv3I:
  assumes "inv2 P1 P2 B1 B2 V" and "B2  S"
  shows "inv3 P1 P2 B1 B2 V"
  using assms unfolding inv3_def by blast

lemma loop_init:
  "inv3 {} {} {} {} U"
proof -
  have *: "inv1 {} {} {} {} U"
    unfolding bp_def partition_on_def pairwise_def wrap_def inv1_def
    using weight by auto
  have "bij_exists {} ( ({}  wrap {}))"
    using bij_betwI' unfolding bij_exists_def by fastforce
  from inv2I[OF * _ this] have "inv2 {} {} {} {} U" by auto
  from inv3I[OF this] show ?thesis by blast
qed

text ‹If B1 is empty and there are no large objects left, then inv3 will be maintained
      if B1 is initialized with u ∈ V ∩ S›.›
lemma loop_stepA:
  assumes "inv3 P1 P2 B1 B2 V" "B1 = {}" "V  L = {}" "u  V  S"
  shows "inv3 P1 P2 {u} B2 (V - {u})"
proof -
  note invrules = inv2E[OF inv3E(1)[OF assms(1)]]
  have WEIGHT: "W B1 + w u  c" using S_def assms(2,4) by simp
  from assms(4) have "u  V" by blast
  from inv1_stepA[OF invrules(1) this WEIGHT] assms(2) have 1: "inv1 P1 P2 {u} B2 (V - {u})" by simp
  have 2: "(V - {u})  L  {}  BP1  wrap {u}. B  L  {}" using assms(3) by blast
  from inv2I[OF 1 2] invrules have "inv2 P1 P2 {u} B2 (V - {u})" by blast
  from inv3I[OF this] show ?thesis using inv3E(2)[OF assms(1)] .
qed

text ‹If B1 is empty and there are large objects left, then inv3 will be maintained
      if B1 is initialized with u ∈ V ∩ L›.›
lemma loop_stepB:
  assumes "inv3 P1 P2 B1 B2 V" "B1 = {}" "u  V  L"
  shows "inv3 P1 P2 {u} B2 (V - {u})"
proof -
  note invrules = inv2E[OF inv3E(1)[OF assms(1)]]
  have WEIGHT: "W B1 + w u  c" using L_def weight assms(2,3) by simp
  from assms(3) have "u  V" by blast
  from inv1_stepA[OF invrules(1) this WEIGHT] assms(2) have 1: "inv1 P1 P2 {u} B2 (V - {u})" by simp
  have "BP1. B  L  {}" using assms(3) invrules(2) by blast
  then have 2: "(V - {u})  L  {}  BP1  wrap {u}. B  L  {}"
    using assms(3) by (metis Int_iff UnE empty_iff insertE singletonI wrap_not_empty)
  from inv2I[OF 1 2] invrules have "inv2 P1 P2 {u} B2 (V - {u})" by blast
  from inv3I[OF this] show ?thesis using inv3E(2)[OF assms(1)] .
qed

text ‹If B1 is not empty and u ∈ V ∩ S› does not exceed its maximum capacity, then inv3
      will be maintained if B1 and {u}› are replaced with B1 ∪ {u}›.›
lemma loop_stepC:
  assumes "inv3 P1 P2 B1 B2 V" "B1  {}" "u  V  S" "W B1 + w(u)  c"
  shows "inv3 P1 P2 (B1  {u}) B2 (V - {u})"
proof -
  note invrules = inv2E[OF inv3E(1)[OF assms(1)]]
  from assms(3) have "u  V" by blast
  from inv1_stepA[OF invrules(1) this assms(4)] have 1: "inv1 P1 P2 (B1  {u}) B2 (V - {u})" .
  have "(V - {u})  L  {}  BP1  wrap B1. B  L  {}" using invrules(2) by blast
  then have 2: "(V - {u})  L  {}  BP1  wrap (B1  {u}). B  L  {}"
    by (metis Int_commute Un_empty_right Un_insert_right assms(2) disjoint_insert(2) insert_iff wrap_not_empty)
  from inv2I[OF 1 2] invrules have "inv2 P1 P2 (B1  {u}) B2 (V - {u})" by blast
  from inv3I[OF this] show ?thesis using inv3E(2)[OF assms(1)] .
qed

text ‹If B1 is not empty and u ∈ V ∩ S› does exceed its maximum capacity but not the capacity of B2,
      then inv3 will be maintained if B1 is added to P1 and emptied, and B2 and {u}› are replaced with B2 ∪ {u}›.›
lemma loop_stepD:
  assumes "inv3 P1 P2 B1 B2 V" "B1  {}" "u  V  S" "W B1 + w(u) > c" "W B2 + w(u)  c"
  shows "inv3 (P1  wrap B1) P2 {} (B2  {u}) (V - {u})"
proof -
  note invrules = inv2E[OF inv3E(1)[OF assms(1)]]
  from assms(3) have "u  V" by blast
  from inv1_stepB[OF invrules(1) this assms(5)] have 1: "inv1 (P1  wrap B1) P2 {} (B2  {u}) (V - {u})" .

  have 2: "(V - {u})  L  {}  BP1  wrap B1  wrap {}. B  L  {}"
    using invrules(2) unfolding wrap_empty by blast

  from invrules(3) obtain f where f_def: "bij_betw f P1 ( (P2  wrap B2))" "BP1. c < W B + w (f B)" unfolding bij_exists_def by blast
  have "B1  P1" using inv1E(3)[OF invrules(1)] by blast
  have "u  ( (P2  wrap B2))" using inv1E(2)[OF invrules(1)] assms(3) by blast
  then have "( (P2  wrap (B2  {u}))) = ( (P2  wrap B2  {{u}}))"
    by (metis Sup_empty Un_assoc Union_Un_distrib ccpo_Sup_singleton wrap_empty wrap_not_empty)
  also have "... = ( (P2  wrap B2))  {u}" by simp
  finally have UN: "( (P2  wrap (B2  {u}))) = ( (P2  wrap B2))  {u}" .
  have "wrap B1 = {B1}" using wrap_not_empty[of B1] assms(2) by simp
  let ?f = "f (B1 := u)"
  have BIJ: "bij_betw ?f (P1  wrap B1) ( (P2  wrap (B2  {u})))"
    unfolding wrap_empty ‹wrap B1 = {B1} UN using f_def(1) B1  P1 u  ( (P2  wrap B2))
    by (metis (no_types, lifting) bij_betw_cong fun_upd_other fun_upd_same notIn_Un_bij_betw3)
  have "c < W B1 + w (?f B1)" using assms(4) by simp
  then have "(BP1  wrap B1. c < W B + w (?f B))"
    unfolding ‹wrap B1 = {B1} using f_def(2) by simp
  with BIJ have "bij_betw ?f (P1  wrap B1) ( (P2  wrap (B2  {u})))
               (BP1  wrap B1. c < W B + w (?f B))" by blast
  then have 3: "bij_exists (P1  wrap B1) ( (P2  wrap (B2  {u})))"
    unfolding bij_exists_def by blast
  from inv2I[OF 1 2 3] have "inv2 (P1  wrap B1) P2 {} (B2  {u}) (V - {u})" using invrules(4) by blast

  from inv3I[OF this] show ?thesis using inv3E(2)[OF assms(1)] assms(3) by blast
qed

text ‹If the maximum capacity of B2 is exceeded by u ∈ V ∩ S›,
      then B2 must contain at least two objects.›
lemma B2_at_least_two_objects:
  assumes "inv3 P1 P2 B1 B2 V" "u  V  S" "W B2 + w(u) > c"
  shows "2  card B2"
proof (rule ccontr, simp add: not_le)
  have FINITE: "finite B2" using inv1E(1)[OF inv2E(1)[OF inv3E(1)[OF assms(1)]]]
    by (metis (no_types, lifting) Finite_Set.finite.simps U_Finite Union_Un_distrib bpE(3) ccpo_Sup_singleton finite_Un wrap_not_empty)
  assume "card B2 < 2"
  then consider (0) "card B2 = 0" | (1) "card B2 = 1" by linarith
  then show False proof cases
    case 0 then have "B2 = {}" using FINITE by simp
    then show ?thesis using assms(2,3) S_def by simp
  next
    case 1 then obtain v where "B2 = {v}"
      using card_1_singletonE by auto
    with inv3E(2)[OF assms(1)] have "2 * w v  c" using S_def by simp
    moreover from B2 = {v} have "W B2 = w v" by simp
    ultimately show ?thesis using assms(2,3) S_def by simp
  qed
qed

text ‹If B1 is not empty and u ∈ V ∩ S› exceeds the maximum capacity of both B1 and B2,
      then inv3 will be maintained if B1 and B2 are added to P1 and P2 respectively,
      emptied, and B2 initialized with u›.›
lemma loop_stepE:
  assumes "inv3 P1 P2 B1 B2 V" "B1  {}" "u  V  S" "W B1 + w(u) > c" "W B2 + w(u) > c"
  shows "inv3 (P1  wrap B1) (P2  wrap B2) {} {u} (V - {u})"
proof -
  note invrules = inv2E[OF inv3E(1)[OF assms(1)]]
  from assms(3) have "u  V" by blast
  from inv1_stepC[OF invrules(1) this] have 1: "inv1 (P1  wrap B1) (P2  wrap B2) {} {u} (V - {u})" .

  have 2: "(V - {u})  L  {}  BP1  wrap B1  wrap {}. B  L  {}"
    using invrules(2) unfolding wrap_empty by blast

  from invrules(3) obtain f where f_def: "bij_betw f P1 ( (P2  wrap B2))" "BP1. c < W B + w (f B)" unfolding bij_exists_def by blast
  have "B1  P1" using inv1E(3)[OF invrules(1)] by blast
  have "u  ( (P2  wrap B2))" using inv1E(2)[OF invrules(1)] assms(3) by blast
  have "( (P2  wrap B2  wrap {u})) = ( (P2  wrap B2  {{u}}))" unfolding wrap_def by simp
  also have "... = ( (P2  wrap B2))  {u}" by simp
  finally have UN: "( (P2  wrap B2  wrap {u})) = ( (P2  wrap B2))  {u}" .
  have "wrap B1 = {B1}" using wrap_not_empty[of B1] assms(2) by simp
  let ?f = "f (B1 := u)"
  have BIJ: "bij_betw ?f (P1  wrap B1) ( (P2  wrap B2  wrap {u}))"
    unfolding wrap_empty ‹wrap B1 = {B1} UN using f_def(1) B1  P1 u  ( (P2  wrap B2))
    by (metis (no_types, lifting) bij_betw_cong fun_upd_other fun_upd_same notIn_Un_bij_betw3)
  have "c < W B1 + w (?f B1)" using assms(4) by simp
  then have "(BP1  wrap B1. c < W B + w (?f B))"
    unfolding ‹wrap B1 = {B1} using f_def(2) by simp
  with BIJ have "bij_betw ?f (P1  wrap B1) ( (P2  wrap B2  wrap {u}))
               (BP1  wrap B1. c < W B + w (?f B))" by blast
  then have 3: "bij_exists (P1  wrap B1) ( (P2  wrap B2  wrap {u}))"
    unfolding bij_exists_def by blast

  have 4: "2 * card (P2  wrap B2)  card ( (P2  wrap B2))"
  proof -
    note bprules = bpE[OF inv1E(1)[OF invrules(1)]]
    have "pairwise disjnt (P2  wrap B2)"
      using bprules(1) pairwise_subset by blast
    moreover have "B2  P2" using inv1E(4)[OF invrules(1)]  by simp
    ultimately have DISJNT: "P2  B2 = {}"
      by (auto, metis (no_types, hide_lams) sup_bot.right_neutral Un_insert_right disjnt_iff mk_disjoint_insert pairwise_insert wrap_Un)
    have "finite (P2)" using U_Finite bprules(3) by auto
    have "finite B2" using inv1E(1)[OF invrules(1)] bp_bins_finite wrap_not_empty by blast

    have "2 * card (P2  wrap B2)  2 * (card P2 + card (wrap B2))"
      using card_Un_le[of P2 ‹wrap B2] by simp
    also have "...  2 * card P2 + 2" using wrap_card by auto
    also have "...  card ( P2) + 2" using invrules(4) by simp
    also have "...  card ( P2) + card B2" using B2_at_least_two_objects[OF assms(1,3,5)] by simp
    also have "... = card ( (P2  {B2}))" using DISJNT card_Un_disjoint[OF ‹finite (P2) ‹finite B2] by (simp add: Un_commute)
    also have "... = card ( (P2  wrap B2))" by (cases B2 = {}) auto
    finally show ?thesis .
  qed
  from inv2I[OF 1 2 3 4] have "inv2 (P1  wrap B1) (P2  wrap B2) {} {u} (V - {u})" .

  from inv3I[OF this] show ?thesis using assms(3) by blast
qed

text ‹The bin packing algorithm as it is proposed in the article @{cite BerghammerR03}.
      P› will not only be a correct solution of the bin packing problem, but the amount of bins
      will be a lower bound for 3 / 2› of the amount of bins of any correct solution Q›, and thus
      guarantee an approximation factor of 3 / 2› for the optimum.›
lemma bp_approx:
"VARS P P1 P2 B1 B2 V u
  {True}
  P1 := {}; P2 := {}; B1 := {}; B2 := {}; V := U;
  WHILE V  S  {} INV {inv3 P1 P2 B1 B2 V} DO 
    IF B1  {}
    THEN u := (SOME u. u  V  S)
    ELSE IF V  L  {}
         THEN u := (SOME u. u  V  L)
         ELSE u := (SOME u. u  V  S) FI FI;
    V := V - {u};
    IF W(B1) + w(u)  c
    THEN B1 := B1  {u}
    ELSE IF W(B2) + w(u)  c
         THEN B2 := B2  {u}
         ELSE P2 := P2  wrap B2; B2 := {u} FI;
         P1 := P1  wrap B1; B1 := {} FI
  OD;
  P := P1  wrap B1  P2  wrap B2  {{v} | v. v  V}
  {bp P  (Q. bp Q  card P  3 / 2 * card Q)}"
proof (vcg, goal_cases)
case (1 P P1 P2 B1 B2 V u)
  then show ?case by (simp add: loop_init)
next
  case (2 P P1 P2 B1 B2 V u)
  then have INV: "inv3 P1 P2 B1 B2 V" ..
  let ?s = "SOME u. u  V  S"
  let ?l = "SOME u. u  V  L"
  have LIN: "V  L  {}  ?l  V  L" using some_in_eq by metis
  then have LWEIGHT: "V  L  {}  w ?l  c" using L_def weight by blast
  from 2 have "V  S  {}" ..
  then have IN: "?s  V  S" using some_in_eq by metis
  then have "w ?s  c" using S_def by simp

  then show ?case
    using LWEIGHT loop_stepA[OF INV _ _ IN] loop_stepB[OF INV _ LIN] loop_stepC[OF INV _ IN]
      and loop_stepD[OF INV _ IN] loop_stepE[OF INV _ IN] by (cases B1 = {}, cases V  L = {}) auto
next
  case (3 P P1 P2 B1 B2 V u)
  then have INV: "inv3 P1 P2 B1 B2 V" and EMPTY: "V  S = {}" by blast+
  from inv1E(1)[OF inv2E(1)[OF inv3E(1)[OF INV]]] and bin_packing_lower_bound_card[OF EMPTY inv3E(1)[OF INV]]
    show ?case by blast
qed

end (* BinPacking *)

subsection ‹The Full Linear Time Version of the Proposed Algorithm›

text ‹Finally, we prove the Algorithm proposed on page 78 of the article @{cite BerghammerR03}.
      This version generates the S and L sets beforehand and uses them directly to calculate the solution,
      thus removing the need for intersection operations, and ensuring linear time if we can
      perform insertion, removal, and selection of an element, the union of two sets,
      and the emptiness test in constant time› @{cite BerghammerR03}.›

locale BinPacking_Complete =
  fixes U :: "'a set" ― ‹A finite, non-empty set of objects›
    and w :: "'a  real" ― ‹A mapping from objects to their respective weights (positive real numbers)›
    and c :: nat ― ‹The maximum capacity of a bin (as a natural number)›
  assumes weight: "u  U. 0 < w(u)  w(u)  c"
      and U_Finite: "finite U"
      and U_NE: "U  {}"
begin

text ‹The correctness proofs will be identical to the ones of the simplified algorithm.›

abbreviation W :: "'a set  real" where
  "W B  (u  B. w(u))"

definition bp :: "'a set set  bool" where
  "bp P  partition_on U P  (B  P. W(B)  c)"

lemma bpE:
  assumes "bp P"
  shows "pairwise disjnt P" "{}  P" "P = U" "B  P. W(B)  c"
  using assms unfolding bp_def partition_on_def by blast+

lemma bpI:
  assumes "pairwise disjnt P" "{}  P" "P = U" "B  P. W(B)  c"
  shows "bp P"
  using assms unfolding bp_def partition_on_def by blast

definition inv1 :: "'a set set  'a set set  'a set  'a set  'a set  bool" where
  "inv1 P1 P2 B1 B2 V  bp (P1  wrap B1  P2  wrap B2  {{v} |v. v  V}) ― ‹A correct solution to the bin packing problem›
                        (P1  wrap B1  P2  wrap B2) = U - V ― ‹The partial solution does not contain objects that have not yet been assigned›
                        B1  (P1  P2  wrap B2) ― ‹B1 is distinct from all the other bins›
                        B2  (P1  wrap B1  P2) ― ‹B2 is distinct from all the other bins›
                        (P1  wrap B1)  (P2  wrap B2) = {} ― ‹The first and second partial solutions are disjoint from each other.›"

lemma inv1E:
  assumes "inv1 P1 P2 B1 B2 V"
  shows "bp (P1  wrap B1  P2  wrap B2  {{v} |v. v  V})"
    and "(P1  wrap B1  P2  wrap B2) = U - V"
    and "B1  (P1  P2  wrap B2)"
    and "B2  (P1  wrap B1  P2)"
    and "(P1  wrap B1)  (P2  wrap B2) = {}"
  using assms unfolding inv1_def by auto

lemma inv1I:
  assumes "bp (P1  wrap B1  P2  wrap B2  {{v} |v. v  V})"
    and "(P1  wrap B1  P2  wrap B2) = U - V"
    and "B1  (P1  P2  wrap B2)"
    and "B2  (P1  wrap B1  P2)"
    and "(P1  wrap B1)  (P2  wrap B2) = {}"
  shows "inv1 P1 P2 B1 B2 V"
  using assms unfolding inv1_def by blast

lemma wrap_Un [simp]: "wrap (M  {x}) = {M  {x}}" unfolding wrap_def by simp
lemma wrap_empty [simp]: "wrap {} = {}" unfolding wrap_def by simp
lemma wrap_not_empty [simp]: "M  {}  wrap M = {M}" unfolding wrap_def by simp

lemma inv1_stepA:
  assumes "inv1 P1 P2 B1 B2 V" "u  V" "W(B1) + w(u)  c"
  shows "inv1 P1 P2 (B1  {u}) B2 (V - {u})"
proof -
  note invrules = inv1E[OF assms(1)] and bprules = bpE[OF invrules(1)]

  ― ‹Rule 1: Pairwise Disjoint›
  have NOTIN: "M  P1  wrap B1  P2  wrap B2  {{v} |v. v  V - {u}}. u  M"
    using invrules(2) assms(2) by blast
  have "{{v} |v. v  V} = {{u}}  {{v} |v. v  V - {u}}"
    using assms(2) by blast
  then have "pairwise disjnt (P1  wrap B1  P2  wrap B2  ({{u}}  {{v} |v. v  V - {u}}))"
    using bprules(1) assms(2) by simp
  then have "pairwise disjnt (wrap B1  {{u}}  P1  P2  wrap B2  {{v} |v. v  V - {u}})" by (simp add: Un_commute)
  then have assm: "pairwise disjnt (wrap B1  {{u}}  (P1  P2  wrap B2  {{v} |v. v  V - {u}}))" by (simp add: Un_assoc)
  have "pairwise disjnt ({B1  {u}}  (P1  P2  wrap B2  {{v} |v. v  V - {u}}))"
  proof (cases B1 = {})
    case True with assm show ?thesis by simp
  next
    case False
    with assm have assm: "pairwise disjnt ({B1}  {{u}}  (P1  P2  wrap B2  {{v} |v. v  V - {u}}))" by simp
    from NOTIN have "{u}  P1  P2  wrap B2  {{v} |v. v  V - {u}}" by blast
    from pairwise_disjnt_Un[OF assm _ this] invrules(2,3) show ?thesis
      using False by auto
  qed
  then have 1: "pairwise disjnt (P1  wrap (B1  {u})  P2  wrap B2  {{v} |v. v  V - {u}})"
    unfolding wrap_Un by simp

  ― ‹Rule 2: No empty sets›
  from bprules(2) have 2: "{}  P1  wrap (B1  {u})  P2  wrap B2  {{v} |v. v  V - {u}}"
    unfolding wrap_def by simp

  ― ‹Rule 3: Union preserved›
  from bprules(3) have " (P1  wrap B1  P2  wrap B2  {{u}}  {{v} |v. v  V - {u}}) = U"
    using assms(2) by blast
  then have 3: " (P1  wrap (B1  {u})  P2  wrap B2  {{v} |v. v  V - {u}}) = U"
    unfolding wrap_def by force

  ― ‹Rule 4: Weights below capacity›
  have "0 < w u" using weight assms(2) bprules(3) by blast
  have "finite B1" using bprules(3) U_Finite by (cases B1 = {}) auto
  then have "W (B1  {u})  W B1 + w u" using 0 < w u by (cases u  B1) (auto simp: insert_absorb)
  also have "...  c" using assms(3) .
  finally have "W (B1  {u})  c" .
  then have "B  wrap (B1  {u}). W B  c" unfolding wrap_Un by blast
  moreover have "BP1  P2  wrap B2  {{v} |v. v  V - {u}}. W B  c"
    using bprules(4) by blast
  ultimately have 4: "BP1  wrap (B1  {u})  P2  wrap B2  {{v} |v. v  V - {u}}. W B  c" by blast
  from bpI[OF 1 2 3 4] have 1: "bp (P1  wrap (B1  {u})  P2  wrap B2  {{v} |v. v  V - {u}})" .

  ― ‹Auxiliary information is preserved›
  have "u  U" using assms(2) bprules(3) by blast
  then have R: "U - (V - {u}) = U - V  {u}" by blast
  have L: " (P1  wrap (B1  {u})  P2  wrap B2) =  (P1  wrap B1  P2  wrap B2)  {u}"
    unfolding wrap_def using NOTIN by auto
  have 2: "