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 "∀B∈P1 ∪ P2 ∪ wrap B2 ∪ {{v} |v. v ∈ V - {u}}. W B ≤ c"
    using bprules(4) by blast
  ultimately have 4: "∀B∈P1 ∪ 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 "∀B∈P1 ∪ wrap B1 ∪ P2 ∪ {{v} |v. v ∈ V - {u}}. W B ≤ c"
    using bprules(4) by blast
  ultimately have 4: "∀B∈P1 ∪ 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 "∃x∈B. ∃y∈B. 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 (verit) 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 (verit) 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 "∀B∈P1 ∪ 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 (verit) 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 (simp flip: of_nat_mult)
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, opaque_lifting) 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 ≠ {} ⟹ ∀B∈P1 ∪ 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 "∀B∈P1. B ∩ L ≠ {}" using assms(3) invrules(2) by blast
  then have 2: "(V - {u}) ∩ L ≠ {} ⟹ ∀B∈P1 ∪ 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 ≠ {} ⟹ ∀B∈P1 ∪ wrap B1. B ∩ L ≠ {}" using invrules(2) by blast
  then have 2: "(V - {u}) ∩ L ≠ {} ⟹ ∀B∈P1 ∪ 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 ≠ {} ⟹ ∀B∈P1 ∪ 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))" "∀B∈P1. 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 "(∀B∈P1 ∪ 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})))
              ∧ (∀B∈P1 ∪ 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 ≠ {} ⟹ ∀B∈P1 ∪ 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))" "∀B∈P1. 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 "(∀B∈P1 ∪ 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}))
              ∧ (∀B∈P1 ∪ 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, opaque_lifting) 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 "∀B∈P1 ∪ P2 ∪ wrap B2 ∪ {{v} |v. v ∈ V - {u}}. W B ≤ c"
    using bprules(4) by blast
  ultimately have 4: "∀B∈P1 ∪ 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

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)]

  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 "∀B∈P1 ∪ wrap B1 ∪ P2 ∪ {{v} |v. v ∈ V - {u}}. W B ≤ c"
    using bprules(4) by blast
  ultimately have 4: "∀B∈P1 ∪ 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

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 ‹From this point onward, we will require a different approach for proving lower bounds.
      Instead of fixing and assuming the definitions of the ‹S› and ‹L› sets, we will introduce
      the abbreviations ‹SU› and ‹LU› for any occurrences of the original ‹S› and ‹L› sets.
      The union of ‹S› and ‹L› can be interpreted as ‹V›. As a result, occurrences of ‹V ∩ S›
      become ‹(S ∪ L) ∩ S = S›, and ‹V ∩ L› become ‹(S ∪ L) ∩ L = L›.
      Occurrences of these sets will have to be replaced appropriately.›
abbreviation SU where
  "SU ≡ {u ∈ U. w u ≤ c / 2}"

abbreviation LU where
  "LU ≡ {u ∈ U. c / 2 < w u}"

text ‹As we will remove elements from ‹S› and ‹L›, we will only be able to show that they remain
      subsets of ‹SU› and ‹LU› respectively.›
abbreviation SL where
  "SL S L ≡ S ⊆ SU ∧ L ⊆ LU"

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)

lemma only_one_L_per_bin:
  assumes "bp P" "B ∈ P"
  shows "∀x ∈ B. ∀y ∈ B. x ≠ y ⟶ x ∉ LU ∨ y ∉ LU"
proof (rule ccontr, simp)
  assume "∃x∈B. ∃y∈B. x ≠ y ∧ y ∈ U ∧ x ∈ U ∧ real c < w x * 2 ∧ real c < w y * 2"
  then obtain x y where *: "x ∈ B" "y ∈ B" "x ≠ y" "x ∈ LU" "y ∈ LU" by auto
  then have "c < w x + w y" 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 (verit) 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

lemma L_lower_bound_card:
  assumes "bp P"
  shows "card LU ≤ card P"
proof -
  have "∀x ∈ LU. ∃B ∈ P. x ∈ B"
    using bpE(3)[OF assms] by blast
  then obtain f where f_def: "∀u ∈ LU. u ∈ f u ∧ f u ∈ P" by metis
  then have "inj_on f LU"
    unfolding inj_on_def using only_one_L_per_bin[OF assms] by blast
  then have card_eq: "card LU = card (f ` LU)" by (simp add: card_image)
  have "f ` LU ⊆ P" using f_def by blast
  moreover have "finite P" using assms by simp
  ultimately have "card (f ` LU) ≤ card P" by (simp add: card_mono)
  then show ?thesis unfolding card_eq .
qed

lemma subset_bp_card:
  assumes "bp P" "M ⊆ P" "∀B ∈ M. B ∩ LU ≠ {}"
  shows "card M ≤ card LU"
proof -
  have "∀B ∈ M. ∃u ∈ LU. u ∈ B" using assms(3) by fast
  then have "∃f. ∀B ∈ M. f B ∈ LU ∧ f B ∈ B" by metis
  then obtain f where f_def: "∀B ∈ M. f B ∈ LU ∧ 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 LU" using U_Finite by auto
  moreover have "f ` M ⊆ LU" using f_def by blast
  ultimately show ?thesis using card_inj_on_le by blast
qed

lemma L_bins_lower_bound_card:
  assumes "bp P" "inv1 P1 P2 B1 B2 (S ∪ L)" "∀B ∈ P1 ∪ wrap B1. B ∩ LU ≠ {}"
      and SL_def: "SL S L"
  shows "card (P1 ∪ wrap B1 ∪ {{v} |v. v ∈ L}) ≤ card P"
proof -
  note invrules = inv1E[OF assms(2)]
  have "∀B ∈ {{v} |v. v ∈ L}. B ∩ LU ≠ {}" using SL_def by blast
  with assms(3) have
    "P1 ∪ wrap B1 ∪ {{v} |v. v ∈ L} ⊆ P1 ∪ wrap B1 ∪ P2 ∪ wrap B2 ∪ {{v} |v. v ∈ S ∪ L}"
    "∀B ∈ P1 ∪ wrap B1 ∪ {{v} |v. v ∈ L}. B ∩ LU ≠ {}" by blast+
  from subset_bp_card[OF invrules(1) this] show ?thesis
    using L_lower_bound_card[OF assms(1)] by linarith
qed

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

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 (verit) 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

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))"

lemma P1_lower_bound_card:
  assumes "bp P" "inv1 P1 P2 B1 B2 (S ∪ L)" "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 ∈ S ∪ L})"
    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 "∀B∈P1 ∪ wrap B1 ∪ P2 ∪ wrap B2 ∪ {{v} |v. v ∈ S ∪ L}. 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 ∈ S ∪ L}). 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 ∈ S ∪ L}. W B)" by (smt (verit) 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" .
  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 (simp flip: of_nat_mult)
qed

lemma P1_B1_lower_bound_card:
  assumes "bp P" "inv1 P1 P2 B1 B2 (S ∪ L)" "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

lemma P2_B2_lower_bound_P1:
  assumes "inv1 P1 P2 B1 B2 (S ∪ L)" "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, opaque_lifting) 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

text ‹We add ‹SL S L› to ‹inv2› to ensure that the ‹S› and ‹L› sets only contain objects with correct weights.›
definition inv2 :: "'a set set ⇒ 'a set set ⇒ 'a set ⇒ 'a set ⇒ 'a set ⇒ 'a set ⇒ bool" where
  "inv2 P1 P2 B1 B2 S L ⟷ inv1 P1 P2 B1 B2 (S ∪ L) ― ‹‹inv1› holds for the partial solution›
                       ∧ (L ≠ {} ⟶ (∀B ∈ P1 ∪ wrap B1. B ∩ LU ≠ {})) ― ‹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››
                       ∧ SL S L ― ‹‹S› and ‹L› are subsets of ‹SU› and ‹LU››"

lemma inv2E:
  assumes "inv2 P1 P2 B1 B2 S L"
  shows "inv1 P1 P2 B1 B2 (S ∪ L)"
    and "L ≠ {} ⟹ ∀B ∈ P1 ∪ wrap B1. B ∩ LU ≠ {}"
    and "bij_exists P1 (⋃(P2 ∪ wrap B2))"
    and "2 * card P2 ≤ card (⋃P2)"
    and "SL S L"
  using assms unfolding inv2_def by blast+

lemma inv2I:
  assumes "inv1 P1 P2 B1 B2 (S ∪ L)"
    and "L ≠ {} ⟹ ∀B ∈ P1 ∪ wrap B1. B ∩ LU ≠ {}"
    and "bij_exists P1 (⋃(P2 ∪ wrap B2))"
    and "2 * card P2 ≤ card (⋃P2)"
    and "SL S L"
  shows "inv2 P1 P2 B1 B2 S L"
  using assms unfolding inv2_def by blast

lemma bin_packing_lower_bound_card:
  assumes "S = {}" "inv2 P1 P2 B1 B2 S L" "bp P"
  shows "card (P1 ∪ wrap B1 ∪ P2 ∪ wrap B2 ∪ {{v} |v. v ∈ S ∪ L}) ≤ 3 / 2 * card P"
proof (cases ‹L = {}›)
  note invrules = inv2E[OF assms(2)]
  case True
  then have "card (P1 ∪ wrap B1 ∪ P2 ∪ wrap B2 ∪ {{v} |v. v ∈ S ∪ L})
           = card (P1 ∪ wrap B1 ∪ P2 ∪ wrap B2)" using assms(1) 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 "card (P1 ∪ wrap B1 ∪ P2 ∪ wrap B2 ∪ {{v} |v. v ∈ S ∪ L})
      = card (P1 ∪ wrap B1 ∪ {{v} |v. v ∈ L} ∪ P2 ∪ wrap B2)"
    using assms(1) by (simp add: Un_commute Un_assoc)
  also have "... ≤ card (P1 ∪ wrap B1 ∪ {{v} |v. v ∈ L}) + card (P2 ∪ wrap B2)"
    using card_Un_le[of ‹P1 ∪ wrap B1 ∪ {{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 False] invrules(5)] 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

definition inv3 :: "'a set set ⇒ 'a set set ⇒ 'a set ⇒ 'a set ⇒ 'a set ⇒ 'a set ⇒ bool" where
  "inv3 P1 P2 B1 B2 S L ⟷ inv2 P1 P2 B1 B2 S L ∧ B2 ⊆ SU"

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

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

lemma loop_init:
  "inv3 {} {} {} {} SU LU"
proof -
  have "SU ∪ LU = U" by auto
  then have *: "inv1 {} {} {} {} (SU ∪ LU)"
    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 {} {} {} {} SU LU" by auto
  from inv3I[OF this] show ?thesis by blast
qed

lemma loop_stepA:
  assumes "inv3 P1 P2 B1 B2 S L" "B1 = {}" "L = {}" "u ∈ S"
  shows "inv3 P1 P2 {u} B2 (S - {u}) L"
proof -
  note invrules = inv2E[OF inv3E(1)[OF assms(1)]]
  have WEIGHT: "W B1 + w u ≤ c" using invrules(5) assms(2,4) by fastforce
  from assms(4) have "u ∈ S ∪ L" by blast
  from inv1_stepA[OF invrules(1) this WEIGHT] assms(2,3) have 1: "inv1 P1 P2 {u} B2 (S - {u} ∪ L)" by simp
  have 2: "L ≠ {} ⟹ ∀B∈P1 ∪ wrap {u}. B ∩ LU ≠ {}" using assms(3) by blast
  from inv2I[OF 1 2] invrules have "inv2 P1 P2 {u} B2 (S - {u}) L" by blast
  from inv3I[OF this] show ?thesis using inv3E(2)[OF assms(1)] .
qed

lemma loop_stepB:
  assumes "inv3 P1 P2 B1 B2 S L" "B1 = {}" "u ∈ L"
  shows "inv3 P1 P2 {u} B2 S (L - {u})"
proof -
  note invrules = inv2E[OF inv3E(1)[OF assms(1)]]
  have WEIGHT: "W B1 + w u ≤ c" using weight invrules(5) assms(2,3) by fastforce

  ― ‹This observation follows from the fact that the ‹S› and ‹L› sets have to be disjoint from each other,
      and allows us to reuse our proofs of the preservation of ‹inv1› by simply replacing ‹V› with ‹S ∪ L››
  have *: "S ∪ L - {u} = S ∪ (L - {u})" using invrules(5) assms(3) by force
  from assms(3) have "u ∈ S ∪ L" by blast
  from inv1_stepA[OF invrules(1) this WEIGHT] assms(2) * have 1: "inv1 P1 P2 {u} B2 (S ∪ (L - {u}))" by simp
  have "∀B∈P1. B ∩ LU ≠ {}" "{u} ∩ LU ≠ {}" using assms(3) invrules(2,5) by blast+
  then have 2: "L ≠ {} ⟹ ∀B∈P1 ∪ wrap {u}. B ∩ LU ≠ {}"
    using assms(3) by (metis (full_types) Un_iff empty_iff insert_iff wrap_not_empty)
  from inv2I[OF 1 2] invrules have "inv2 P1 P2 {u} B2 S (L - {u})" by blast
  from inv3I[OF this] show ?thesis using inv3E(2)[OF assms(1)] .
qed

lemma loop_stepC:
  assumes "inv3 P1 P2 B1 B2 S L" "B1 ≠ {}" "u ∈ S" "W B1 + w(u) ≤ c"
  shows "inv3 P1 P2 (B1 ∪ {u}) B2 (S - {u}) L"
proof -
  note invrules = inv2E[OF inv3E(1)[OF assms(1)]]

  ― ‹Same approach, but removing ‹{u}› from ‹S› instead of ‹L››
  have *: "S ∪ L - {u} = (S - {u}) ∪ L" using invrules(5) assms(3) by force
  from assms(3) have "u ∈ S ∪ L" by blast
  from inv1_stepA[OF invrules(1) this assms(4)] * have 1: "inv1 P1 P2 (B1 ∪ {u}) B2 (S - {u} ∪ L)" by simp
  have "L ≠ {} ⟹ ∀B∈P1 ∪ wrap B1. B ∩ LU ≠ {}" using invrules(2) by blast
  then have 2: "L ≠ {} ⟹ ∀B∈P1 ∪ wrap (B1 ∪ {u}). B ∩ LU ≠ {}"
    by (smt (verit) Int_insert_left Un_empty_right Un_iff Un_insert_right assms(2) insert_not_empty singletonD singletonI wrap_def)
  from inv2I[OF 1 2] invrules have "inv2 P1 P2 (B1 ∪ {u}) B2 (S - {u}) L" by blast
  from inv3I[OF this] show ?thesis using inv3E(2)[OF assms(1)] .
qed

lemma loop_stepD:
  assumes "inv3 P1 P2 B1 B2 S L" "B1 ≠ {}" "u ∈ S" "W B1 + w(u) > c" "W B2 + w(u) ≤ c"
  shows "inv3 (P1 ∪ wrap B1) P2 {} (B2 ∪ {u}) (S - {u}) L"
proof -
  note invrules = inv2E[OF inv3E(1)[OF assms(1)]]
  have *: "S ∪ L - {u} = (S - {u}) ∪ L" using invrules(5) assms(3) by force
  from assms(3) have "u ∈ S ∪ L" by blast
  from inv1_stepB[OF invrules(1) this assms(5)] * have 1: "inv1 (P1 ∪ wrap B1) P2 {} (B2 ∪ {u}) (S - {u} ∪ L)" by simp

  have 2: "L ≠ {} ⟹ ∀B∈P1 ∪ wrap B1 ∪ wrap {}. B ∩ LU ≠ {}"
    using invrules(2) unfolding wrap_empty by blast

  from invrules(3) obtain f where f_def: "bij_betw f P1 (⋃ (P2 ∪ wrap B2))" "∀B∈P1. 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 "(∀B∈P1 ∪ 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})))
              ∧ (∀B∈P1 ∪ 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}) (S - {u}) L" using invrules(4,5) by blast

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

lemma B2_at_least_two_objects:
  assumes "inv3 P1 P2 B1 B2 S L" "u ∈ 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) inv2E(5)[OF inv3E(1)[OF assms(1)]] by force
  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 inv2E(5)[OF inv3E(1)[OF assms(1)]] by simp
    moreover from ‹B2 = {v}› have "W B2 = w v" by simp
    ultimately show ?thesis using assms(2,3) inv2E(5)[OF inv3E(1)[OF assms(1)]] by force
  qed
qed

lemma loop_stepE:
  assumes "inv3 P1 P2 B1 B2 S L" "B1 ≠ {}" "u ∈ S" "W B1 + w(u) > c" "W B2 + w(u) > c"
  shows "inv3 (P1 ∪ wrap B1) (P2 ∪ wrap B2) {} {u} (S - {u}) L"
proof -
  note invrules = inv2E[OF inv3E(1)[OF assms(1)]]
  have *: "S ∪ L - {u} = (S - {u}) ∪ L" using invrules(5) assms(3) by force
  from assms(3) have "u ∈ S ∪ L" by blast
  from inv1_stepC[OF invrules(1) this] * have 1: "inv1 (P1 ∪ wrap B1) (P2 ∪ wrap B2) {} {u} (S - {u} ∪ L)" by simp

  have 2: "L ≠ {} ⟹ ∀B∈P1 ∪ wrap B1 ∪ wrap {}. B ∩ LU ≠ {}"
    using invrules(2) unfolding wrap_empty by blast

  from invrules(3) obtain f where f_def: "bij_betw f P1 (⋃ (P2 ∪ wrap B2))" "∀B∈P1. 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 "(∀B∈P1 ∪ 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}))
              ∧ (∀B∈P1 ∪ 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, opaque_lifting) 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} (S - {u}) L"
    using invrules(5) by blast

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

text ‹The bin packing algorithm as it is proposed on page 78 of 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 S L u
  {True}
  S := {}; L:= {}; V := U;
  WHILE V ≠ {} INV {V ⊆ U ∧ S = {u ∈ U - V. w(u) ≤ c / 2} ∧ L = {u ∈ U - V. c / 2 < w(u)}} DO
    u := (SOME u. u ∈ V);
    IF w(u) ≤ c / 2
    THEN S := S ∪ {u}
    ELSE L := L ∪ {u} FI;
    V := V - {u}
  OD;
  P1 := {}; P2 := {}; B1 := {}; B2 := {};
  WHILE S ≠ {} INV {inv3 P1 P2 B1 B2 S L} DO 
    IF B1 ≠ {}
    THEN u := (SOME u. u ∈ S); S := S - {u}
    ELSE IF L ≠ {}
         THEN u := (SOME u. u ∈ L); L := L - {u}
         ELSE u := (SOME u. u ∈ S); S := S - {u} FI FI;
    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 := L;
  WHILE V ≠ {}
  INV {S = {} ∧ inv3 P1 P2 B1 B2 S L ∧ V ⊆ L ∧ P = P1 ∪ wrap B1 ∪ P2 ∪ wrap B2 ∪ {{v}|v. v ∈ L - V}} DO
    u := (SOME u. u ∈ V); P := P ∪ {{u}}; V := V - {u}
  OD
  {bp P ∧ (∀Q. bp Q ⟶ card P ≤ 3 / 2 * card Q)}"
proof (vcg, goal_cases)
  case (1 P P1 P2 B1 B2 V S L u)
  then show ?case by blast
next
  case (2 P P1 P2 B1 B2 V S L u)
  then show ?case by (auto simp: some_in_eq)
next
  case (3 P P1 P2 B1 B2 V S L u)
  then show ?case using loop_init by force
next
  case (4 P P1 P2 B1 B2 V S L u)
  then have INV: "inv3 P1 P2 B1 B2 S L" ..
  let ?s = "SOME u. u ∈ S"
  let ?l = "SOME u. u ∈ L"
  note SL_def = inv2E(5)[OF inv3E(1)[OF INV]]
  have LIN: "L ≠ {} ⟹ ?l ∈ L" using some_in_eq by metis
  then have LWEIGHT: "L ≠ {} ⟹ w ?l ≤ c" using weight SL_def by blast
  from 4 have "S ≠ {}" ..
  then have IN: "?s ∈ S" using some_in_eq by metis
  then have "w ?s ≤ c" using SL_def by auto
  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 ‹L = {}›) auto
next
  case (5 P P1 P2 B1 B2 V S L u)
  then show ?case by blast
next
  case (6 P P1 P2 B1 B2 V S L u)
  then have *: "(SOME u. u ∈ V) ∈ V" "(SOME u. u ∈ V) ∈ L" by (auto simp add: some_in_eq)
  then have "P1 ∪ wrap B1 ∪ P2 ∪ wrap B2 ∪ {{v} |v. v ∈ L - (V - {SOME u. u ∈ V})}
           = P1 ∪ wrap B1 ∪ P2 ∪ wrap B2 ∪ {{v} |v. v ∈ L - V ∪ {SOME u. u ∈ V}}"
    by blast
  with 6 * show ?case by blast
next
  case (7 P P1 P2 B1 B2 V S L u)
  then have *: "inv2 P1 P2 B1 B2 S L"
    using inv3E(1) by blast
  from inv1E(1)[OF inv2E(1)[OF *]] 7
  have "bp P" by fastforce
  with bin_packing_lower_bound_card[OF _ *] 7
  show ?case by fastforce
qed

end (* BinPacking_Complete *)

end (* Theory *)