diff --git a/thys/Approximation_Algorithms/Approx_BP_Hoare.thy b/thys/Approximation_Algorithms/Approx_BP_Hoare.thy
new file mode 100755
--- /dev/null
+++ b/thys/Approximation_Algorithms/Approx_BP_Hoare.thy
@@ -0,0 +1,1706 @@
+section \<open>Bin Packing\<close>
+
+theory Approx_BP_Hoare
+  imports Complex_Main "HOL-Hoare.Hoare_Logic" "HOL-Library.Disjoint_Sets"
+begin
+
+text \<open>The algorithm and proofs are based on the work by Berghammer and Reuter @{cite BerghammerR03}.\<close>
+
+subsection \<open>Formalization of a Correct Bin Packing\<close>
+
+text \<open>Definition of the unary operator \<open>\<lbrakk>\<cdot>\<rbrakk>\<close> from the article.
+      \<open>B\<close> will only be wrapped into a set if it is non-empty.\<close>
+definition wrap :: "'a set \<Rightarrow> 'a set set" where
+  "wrap B = (if B = {} then {} else {B})"
+
+lemma wrap_card:
+  "card (wrap B) \<le> 1"
+  unfolding wrap_def by auto
+
+text \<open>If \<open>M\<close> and \<open>N\<close> are pairwise disjoint with \<open>V\<close> and not yet contained in V,
+      then the union of \<open>M\<close> and \<open>N\<close> is also pairwise disjoint with \<open>V\<close>.\<close>
+lemma pairwise_disjnt_Un:
+  assumes "pairwise disjnt ({M} \<union> {N} \<union> V)" "M \<notin> V" "N \<notin> V"
+  shows "pairwise disjnt ({M \<union> N} \<union> V)"
+  using assms unfolding pairwise_def by auto
+
+text \<open>A Bin Packing Problem is defined like in the article:\<close>
+locale BinPacking =
+  fixes U :: "'a set" \<comment> \<open>A finite, non-empty set of objects\<close>
+    and w :: "'a \<Rightarrow> real" \<comment> \<open>A mapping from objects to their respective weights (positive real numbers)\<close>
+    and c :: nat \<comment> \<open>The maximum capacity of a bin (a natural number)\<close>
+    and S :: "'a set" \<comment> \<open>The set of \<open>small\<close> objects (weight no larger than \<open>1/2\<close> of \<open>c\<close>)\<close>
+    and L :: "'a set" \<comment> \<open>The set of \<open>large\<close> objects (weight larger than \<open>1/2\<close> of \<open>c\<close>)\<close>
+  assumes weight: "\<forall>u \<in> U. 0 < w(u) \<and> w(u) \<le> c"
+      and U_Finite: "finite U"
+      and U_NE: "U \<noteq> {}"
+      and S_def: "S = {u \<in> U. w(u) \<le> c / 2}"
+      and L_def: "L = U - S"
+begin
+
+text \<open>In the article, this is defined as \<open>w\<close> as well. However, to avoid ambiguity,
+      we will abbreviate the weight of a bin as \<open>W\<close>.\<close>
+abbreviation W :: "'a set \<Rightarrow> real" where
+  "W B \<equiv> (\<Sum>u \<in> B. w(u))"
+
+text \<open>\<open>P\<close> constitutes as a correct bin packing if \<open>P\<close> is a partition of \<open>U\<close>
+      (as defined in @{thm [source] partition_on_def}) and the weights of
+      the bins do not exceed their maximum capacity \<open>c\<close>.\<close>
+definition bp :: "'a set set \<Rightarrow> bool" where
+  "bp P \<longleftrightarrow> partition_on U P \<and> (\<forall>B \<in> P. W(B) \<le> c)"
+
+lemma bpE:
+  assumes "bp P"
+  shows "pairwise disjnt P" "{} \<notin> P" "\<Union>P = U" "\<forall>B \<in> P. W(B) \<le> c"
+  using assms unfolding bp_def partition_on_def by blast+
+
+lemma bpI:
+  assumes "pairwise disjnt P" "{} \<notin> P" "\<Union>P = U" "\<forall>B \<in> P. W(B) \<le> c"
+  shows "bp P"
+  using assms unfolding bp_def partition_on_def by blast
+
+text \<open>Although we assume the \<open>S\<close> and \<open>L\<close> sets as given, manually obtaining them from \<open>U\<close> is trivial
+      and can be achieved in linear time. Proposed by the article @{cite "BerghammerR03"}.\<close>
+lemma S_L_set_generation:
+"VARS S L W u
+  {True}
+  S := {}; L := {}; W := U;
+  WHILE W \<noteq> {}
+  INV {W \<subseteq> U \<and> S = {v \<in> U - W. w(v) \<le> c / 2} \<and> L = {v \<in> U - W. w(v) > c / 2}} DO
+    u := (SOME u. u \<in> W);
+    IF 2 * w(u) \<le> c
+    THEN S := S \<union> {u}
+    ELSE L := L \<union> {u} FI;
+    W := W - {u}
+  OD
+  {S = {v \<in> U. w(v) \<le> c / 2} \<and> L = {v \<in> U. w(v) > c / 2}}"
+  by vcg (auto simp: some_in_eq)
+
+subsection \<open>The Proposed Approximation Algorithm\<close>
+
+subsubsection \<open>Functional Correctness\<close>
+
+text \<open>According to the article, \<open>inv\<^sub>1\<close> holds if \<open>P\<^sub>1 \<union> wrap B\<^sub>1 \<union> P\<^sub>2 \<union> wrap B\<^sub>2 \<union> {{v} |v. v \<in> V}\<close>
+      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.\<close>
+definition inv\<^sub>1 :: "'a set set \<Rightarrow> 'a set set \<Rightarrow> 'a set \<Rightarrow> 'a set \<Rightarrow> 'a set \<Rightarrow> bool" where
+  "inv\<^sub>1 P\<^sub>1 P\<^sub>2 B\<^sub>1 B\<^sub>2 V \<longleftrightarrow> bp (P\<^sub>1 \<union> wrap B\<^sub>1 \<union> P\<^sub>2 \<union> wrap B\<^sub>2 \<union> {{v} |v. v \<in> V}) \<comment> \<open>A correct solution to the bin packing problem\<close>
+                       \<and> \<Union>(P\<^sub>1 \<union> wrap B\<^sub>1 \<union> P\<^sub>2 \<union> wrap B\<^sub>2) = U - V \<comment> \<open>The partial solution does not contain objects that have not yet been assigned\<close>
+                       \<and> B\<^sub>1 \<notin> (P\<^sub>1 \<union> P\<^sub>2 \<union> wrap B\<^sub>2) \<comment> \<open>\<open>B\<^sub>1\<close> is distinct from all the other bins\<close>
+                       \<and> B\<^sub>2 \<notin> (P\<^sub>1 \<union> wrap B\<^sub>1 \<union> P\<^sub>2) \<comment> \<open>\<open>B\<^sub>2\<close> is distinct from all the other bins\<close>
+                       \<and> (P\<^sub>1 \<union> wrap B\<^sub>1) \<inter> (P\<^sub>2 \<union> wrap B\<^sub>2) = {} \<comment> \<open>The first and second partial solutions are disjoint from each other.\<close>"
+(*
+lemma "partition_on U (P\<^sub>1 \<union> wrap B\<^sub>1 \<union> P\<^sub>2 \<union> wrap B\<^sub>2 \<union> {{v} |v. v \<in> V}) \<Longrightarrow> u \<in> V \<Longrightarrow>
+partition_on U (P\<^sub>1 \<union> wrap (insert u B\<^sub>1) \<union> P\<^sub>2 \<union> wrap B\<^sub>2 \<union> {{v} |v. v \<in> (V-{u})})"
+  nitpick*)
+lemma inv\<^sub>1E:
+  assumes "inv\<^sub>1 P\<^sub>1 P\<^sub>2 B\<^sub>1 B\<^sub>2 V"
+  shows "bp (P\<^sub>1 \<union> wrap B\<^sub>1 \<union> P\<^sub>2 \<union> wrap B\<^sub>2 \<union> {{v} |v. v \<in> V})"
+    and "\<Union>(P\<^sub>1 \<union> wrap B\<^sub>1 \<union> P\<^sub>2 \<union> wrap B\<^sub>2) = U - V"
+    and "B\<^sub>1 \<notin> (P\<^sub>1 \<union> P\<^sub>2 \<union> wrap B\<^sub>2)"
+    and "B\<^sub>2 \<notin> (P\<^sub>1 \<union> wrap B\<^sub>1 \<union> P\<^sub>2)"
+    and "(P\<^sub>1 \<union> wrap B\<^sub>1) \<inter> (P\<^sub>2 \<union> wrap B\<^sub>2) = {}"
+  using assms unfolding inv\<^sub>1_def by auto
+
+lemma inv\<^sub>1I:
+  assumes "bp (P\<^sub>1 \<union> wrap B\<^sub>1 \<union> P\<^sub>2 \<union> wrap B\<^sub>2 \<union> {{v} |v. v \<in> V})"
+    and "\<Union>(P\<^sub>1 \<union> wrap B\<^sub>1 \<union> P\<^sub>2 \<union> wrap B\<^sub>2) = U - V"
+    and "B\<^sub>1 \<notin> (P\<^sub>1 \<union> P\<^sub>2 \<union> wrap B\<^sub>2)"
+    and "B\<^sub>2 \<notin> (P\<^sub>1 \<union> wrap B\<^sub>1 \<union> P\<^sub>2)"
+    and "(P\<^sub>1 \<union> wrap B\<^sub>1) \<inter> (P\<^sub>2 \<union> wrap B\<^sub>2) = {}"
+  shows "inv\<^sub>1 P\<^sub>1 P\<^sub>2 B\<^sub>1 B\<^sub>2 V"
+  using assms unfolding inv\<^sub>1_def by blast
+
+lemma wrap_Un [simp]: "wrap (M \<union> {x}) = {M \<union> {x}}" unfolding wrap_def by simp
+lemma wrap_empty [simp]: "wrap {} = {}" unfolding wrap_def by simp
+lemma wrap_not_empty [simp]: "M \<noteq> {} \<longleftrightarrow> wrap M = {M}" unfolding wrap_def by simp
+
+text \<open>If \<open>inv\<^sub>1\<close> holds for the current partial solution, and the weight of an object \<open>u \<in> V\<close> added to \<open>B\<^sub>1\<close> does
+      not exceed its capacity, then \<open>inv\<^sub>1\<close> also holds if \<open>B\<^sub>1\<close> and \<open>{u}\<close> are replaced by \<open>B\<^sub>1 \<union> {u}\<close>.\<close>
+lemma inv\<^sub>1_stepA:
+  assumes "inv\<^sub>1 P\<^sub>1 P\<^sub>2 B\<^sub>1 B\<^sub>2 V" "u \<in> V" "W(B\<^sub>1) + w(u) \<le> c"
+  shows "inv\<^sub>1 P\<^sub>1 P\<^sub>2 (B\<^sub>1 \<union> {u}) B\<^sub>2 (V - {u})"
+proof -
+  note invrules = inv\<^sub>1E[OF assms(1)] and bprules = bpE[OF invrules(1)]
+
+  text \<open>In the proof for \<open>Theorem 3.2\<close> of the article it is erroneously argued that
+        if \<open>P\<^sub>1 \<union> wrap B\<^sub>1 \<union> P\<^sub>2 \<union> wrap B\<^sub>2 \<union> {{v} |v. v \<in> V}\<close> is a partition of \<open>U\<close>,
+        then the same holds if \<open>B\<^sub>1\<close> is replaced by \<open>B\<^sub>1 \<union> {u}\<close>.
+        This is, however, not necessarily the case if \<open>B\<^sub>1\<close> or \<open>{u}\<close> are already contained in the partial solution.
+        Suppose \<open>P\<^sub>1\<close> contains the non-empty bin \<open>B\<^sub>1\<close>, then \<open>P\<^sub>1 \<union> wrap B\<^sub>1\<close> would still be pairwise disjoint, provided \<open>P\<^sub>1\<close> was pairwise disjoint before, as the union simply ignores the duplicate \<open>B\<^sub>1\<close>. Now, if the algorithm modifies \<open>B\<^sub>1\<close> by adding an element from \<open>V\<close> such that \<open>B\<^sub>1\<close> becomes some non-empty \<open>B\<^sub>1'\<close> with \<open>B\<^sub>1 \<inter> B\<^sub>1' \<noteq> \<emptyset>\<close> and \<open>B\<^sub>1' \<notin> P\<^sub>1\<close>, one can see that this property would no longer be preserved.
+        To avoid such a situation, we will use the first additional conjunct in \<open>inv\<^sub>1\<close> to ensure that \<open>{u}\<close>
+        is not yet contained in the partial solution, and the second additional conjunct to ensure that \<open>B\<^sub>1\<close>
+        is not yet contained in the partial solution.\<close>
+
+  \<comment> \<open>Rule 1: Pairwise Disjoint\<close>
+  have NOTIN: "\<forall>M \<in> P\<^sub>1 \<union> wrap B\<^sub>1 \<union> P\<^sub>2 \<union> wrap B\<^sub>2 \<union> {{v} |v. v \<in> V - {u}}. u \<notin> M"
+    using invrules(2) assms(2) by blast
+  have "{{v} |v. v \<in> V} = {{u}} \<union> {{v} |v. v \<in> V - {u}}"
+    using assms(2) by blast
+  then have "pairwise disjnt (P\<^sub>1 \<union> wrap B\<^sub>1 \<union> P\<^sub>2 \<union> wrap B\<^sub>2 \<union> ({{u}} \<union> {{v} |v. v \<in> V - {u}}))"
+    using bprules(1) assms(2) by simp
+  then have "pairwise disjnt (wrap B\<^sub>1 \<union> {{u}} \<union> P\<^sub>1 \<union> P\<^sub>2 \<union> wrap B\<^sub>2 \<union> {{v} |v. v \<in> V - {u}})" by (simp add: Un_commute)
+  then have assm: "pairwise disjnt (wrap B\<^sub>1 \<union> {{u}} \<union> (P\<^sub>1 \<union> P\<^sub>2 \<union> wrap B\<^sub>2 \<union> {{v} |v. v \<in> V - {u}}))" by (simp add: Un_assoc)
+  have "pairwise disjnt ({B\<^sub>1 \<union> {u}} \<union> (P\<^sub>1 \<union> P\<^sub>2 \<union> wrap B\<^sub>2 \<union> {{v} |v. v \<in> V - {u}}))"
+  proof (cases \<open>B\<^sub>1 = {}\<close>)
+    case True with assm show ?thesis by simp
+  next
+    case False
+    with assm have assm: "pairwise disjnt ({B\<^sub>1} \<union> {{u}} \<union> (P\<^sub>1 \<union> P\<^sub>2 \<union> wrap B\<^sub>2 \<union> {{v} |v. v \<in> V - {u}}))" by simp
+    from NOTIN have "{u} \<notin> P\<^sub>1 \<union> P\<^sub>2 \<union> wrap B\<^sub>2 \<union> {{v} |v. v \<in> 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 (P\<^sub>1 \<union> wrap (B\<^sub>1 \<union> {u}) \<union> P\<^sub>2 \<union> wrap B\<^sub>2 \<union> {{v} |v. v \<in> V - {u}})"
+    unfolding wrap_Un by simp
+
+  \<comment> \<open>Rule 2: No empty sets\<close>
+  from bprules(2) have 2: "{} \<notin> P\<^sub>1 \<union> wrap (B\<^sub>1 \<union> {u}) \<union> P\<^sub>2 \<union> wrap B\<^sub>2 \<union> {{v} |v. v \<in> V - {u}}"
+    unfolding wrap_def by simp
+
+  \<comment> \<open>Rule 3: Union preserved\<close>
+  from bprules(3) have "\<Union> (P\<^sub>1 \<union> wrap B\<^sub>1 \<union> P\<^sub>2 \<union> wrap B\<^sub>2 \<union> {{u}} \<union> {{v} |v. v \<in> V - {u}}) = U"
+    using assms(2) by blast
+  then have 3: "\<Union> (P\<^sub>1 \<union> wrap (B\<^sub>1 \<union> {u}) \<union> P\<^sub>2 \<union> wrap B\<^sub>2 \<union> {{v} |v. v \<in> V - {u}}) = U"
+    unfolding wrap_def by force
+
+  \<comment> \<open>Rule 4: Weights below capacity\<close>
+  have "0 < w u" using weight assms(2) bprules(3) by blast
+  have "finite B\<^sub>1" using bprules(3) U_Finite by (cases \<open>B\<^sub>1 = {}\<close>) auto
+  then have "W (B\<^sub>1 \<union> {u}) \<le> W B\<^sub>1 + w u" using \<open>0 < w u\<close> by (cases \<open>u \<in> B\<^sub>1\<close>) (auto simp: insert_absorb)
+  also have "... \<le> c" using assms(3) .
+  finally have "W (B\<^sub>1 \<union> {u}) \<le> c" .
+  then have "\<forall>B \<in> wrap (B\<^sub>1 \<union> {u}). W B \<le> c" unfolding wrap_Un by blast
+  moreover have "\<forall>B\<in>P\<^sub>1 \<union> P\<^sub>2 \<union> wrap B\<^sub>2 \<union> {{v} |v. v \<in> V - {u}}. W B \<le> c"
+    using bprules(4) by blast
+  ultimately have 4: "\<forall>B\<in>P\<^sub>1 \<union> wrap (B\<^sub>1 \<union> {u}) \<union> P\<^sub>2 \<union> wrap B\<^sub>2 \<union> {{v} |v. v \<in> V - {u}}. W B \<le> c" by blast
+  from bpI[OF 1 2 3 4] have 1: "bp (P\<^sub>1 \<union> wrap (B\<^sub>1 \<union> {u}) \<union> P\<^sub>2 \<union> wrap B\<^sub>2 \<union> {{v} |v. v \<in> V - {u}})" .
+
+  \<comment> \<open>Auxiliary information is preserved\<close>
+  have "u \<in> U" using assms(2) bprules(3) by blast
+  then have R: "U - (V - {u}) = U - V \<union> {u}" by blast
+  have L: "\<Union> (P\<^sub>1 \<union> wrap (B\<^sub>1 \<union> {u}) \<union> P\<^sub>2 \<union> wrap B\<^sub>2) = \<Union> (P\<^sub>1 \<union> wrap B\<^sub>1 \<union> P\<^sub>2 \<union> wrap B\<^sub>2) \<union> {u}"
+    unfolding wrap_def using NOTIN by auto
+  have 2: "\<Union> (P\<^sub>1 \<union> wrap (B\<^sub>1 \<union> {u}) \<union> P\<^sub>2 \<union> wrap B\<^sub>2) = U - (V - {u})"
+    unfolding L R invrules(2) ..
+  have 3: "B\<^sub>1 \<union> {u} \<notin> P\<^sub>1 \<union> P\<^sub>2 \<union> wrap B\<^sub>2"
+    using NOTIN by auto
+  have 4: "B\<^sub>2 \<notin> P\<^sub>1 \<union> wrap (B\<^sub>1 \<union> {u}) \<union> P\<^sub>2"
+    using invrules(4) NOTIN unfolding wrap_def by fastforce
+  have 5: "(P\<^sub>1 \<union> wrap (B\<^sub>1 \<union> {u})) \<inter> (P\<^sub>2 \<union> wrap B\<^sub>2) = {}"
+    using invrules(5) NOTIN unfolding wrap_Un by auto
+
+  from inv\<^sub>1I[OF 1 2 3 4 5] show ?thesis .
+qed
+
+text \<open>If \<open>inv\<^sub>1\<close> holds for the current partial solution, and the weight of an object \<open>u \<in> V\<close> added to \<open>B\<^sub>2\<close> does
+      not exceed its capacity, then \<open>inv\<^sub>1\<close> also holds if \<open>B\<^sub>2\<close> and \<open>{u}\<close> are replaced by \<open>B\<^sub>2 \<union> {u}\<close>.\<close>
+lemma inv\<^sub>1_stepB:
+  assumes "inv\<^sub>1 P\<^sub>1 P\<^sub>2 B\<^sub>1 B\<^sub>2 V" "u \<in> V" "W B\<^sub>2 + w u \<le> c"
+  shows "inv\<^sub>1 (P\<^sub>1 \<union> wrap B\<^sub>1) P\<^sub>2 {} (B\<^sub>2 \<union> {u}) (V - {u})"
+proof -
+  note invrules = inv\<^sub>1E[OF assms(1)] and bprules = bpE[OF invrules(1)]
+
+text \<open>The argumentation here is similar to the one in @{thm [source] inv\<^sub>1_stepA} with
+      \<open>B\<^sub>1\<close> replaced with \<open>B\<^sub>2\<close> and using the first and third additional conjuncts of \<open>inv\<^sub>1\<close>
+      to amend the issue, instead of the first and second.\<close>
+  \<comment> \<open>Rule 1: Pairwise Disjoint\<close>
+  have NOTIN: "\<forall>M \<in> P\<^sub>1 \<union> wrap B\<^sub>1 \<union> P\<^sub>2 \<union> wrap B\<^sub>2 \<union> {{v} |v. v \<in> V - {u}}. u \<notin> M"
+    using invrules(2) assms(2) by blast
+  have "{{v} |v. v \<in> V} = {{u}} \<union> {{v} |v. v \<in> V - {u}}"
+    using assms(2) by blast
+  then have "pairwise disjnt (P\<^sub>1 \<union> wrap B\<^sub>1 \<union> P\<^sub>2 \<union> wrap B\<^sub>2 \<union> {{u}} \<union> {{v} |v. v \<in> V - {u}})"
+    using bprules(1) assms(2) by simp
+  then have assm: "pairwise disjnt (wrap B\<^sub>2 \<union> {{u}} \<union> (P\<^sub>1 \<union> wrap B\<^sub>1 \<union> P\<^sub>2 \<union> {{v} |v. v \<in> V - {u}}))"
+    by (simp add: Un_assoc Un_commute)
+  have "pairwise disjnt ({B\<^sub>2 \<union> {u}} \<union> (P\<^sub>1 \<union> wrap B\<^sub>1 \<union> P\<^sub>2 \<union> {{v} |v. v \<in> V - {u}}))"
+  proof (cases \<open>B\<^sub>2 = {}\<close>)
+    case True with assm show ?thesis by simp
+  next
+    case False
+    with assm have assm: "pairwise disjnt ({B\<^sub>2} \<union> {{u}} \<union> (P\<^sub>1 \<union> wrap B\<^sub>1 \<union> P\<^sub>2 \<union> {{v} |v. v \<in> V - {u}}))" by simp
+    from NOTIN have "{u} \<notin> P\<^sub>1 \<union> wrap B\<^sub>1 \<union> P\<^sub>2 \<union> {{v} |v. v \<in> 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 (P\<^sub>1 \<union> wrap B\<^sub>1 \<union> wrap {} \<union> P\<^sub>2 \<union> wrap (B\<^sub>2 \<union> {u}) \<union> {{v} |v. v \<in> V - {u}})"
+    unfolding wrap_Un by simp
+
+  \<comment> \<open>Rule 2: No empty sets\<close>
+  from bprules(2) have 2: "{} \<notin> P\<^sub>1 \<union> wrap B\<^sub>1 \<union> wrap {} \<union> P\<^sub>2 \<union> wrap (B\<^sub>2 \<union> {u}) \<union> {{v} |v. v \<in> V - {u}}"
+    unfolding wrap_def by simp
+
+  \<comment> \<open>Rule 3: Union preserved\<close>
+  from bprules(3) have "\<Union> (P\<^sub>1 \<union> wrap B\<^sub>1 \<union> P\<^sub>2 \<union> wrap B\<^sub>2 \<union> {{u}} \<union> {{v} |v. v \<in> V - {u}}) = U"
+    using assms(2) by blast
+  then have 3: "\<Union> (P\<^sub>1 \<union> wrap B\<^sub>1 \<union> wrap {} \<union> P\<^sub>2 \<union> wrap (B\<^sub>2 \<union> {u}) \<union> {{v} |v. v \<in> V - {u}}) = U"
+    unfolding wrap_def by force
+
+  \<comment> \<open>Rule 4: Weights below capacity\<close>
+  have "0 < w u" using weight assms(2) bprules(3) by blast
+  have "finite B\<^sub>2" using bprules(3) U_Finite by (cases \<open>B\<^sub>2 = {}\<close>) auto
+  then have "W (B\<^sub>2 \<union> {u}) \<le> W B\<^sub>2 + w u" using \<open>0 < w u\<close> by (cases \<open>u \<in> B\<^sub>2\<close>) (auto simp: insert_absorb)
+  also have "... \<le> c" using assms(3) .
+  finally have "W (B\<^sub>2 \<union> {u}) \<le> c" .
+  then have "\<forall>B \<in> wrap (B\<^sub>2 \<union> {u}). W B \<le> c" unfolding wrap_Un by blast
+  moreover have "\<forall>B\<in>P\<^sub>1 \<union> wrap B\<^sub>1 \<union> P\<^sub>2 \<union> {{v} |v. v \<in> V - {u}}. W B \<le> c"
+    using bprules(4) by blast
+  ultimately have 4: "\<forall>B\<in>P\<^sub>1 \<union> wrap B\<^sub>1 \<union> wrap {} \<union> P\<^sub>2 \<union> wrap (B\<^sub>2 \<union> {u}) \<union> {{v} |v. v \<in> V - {u}}. W B \<le> c"
+    by auto
+  from bpI[OF 1 2 3 4] have 1: "bp (P\<^sub>1 \<union> wrap B\<^sub>1 \<union> wrap {} \<union> P\<^sub>2 \<union> wrap (B\<^sub>2 \<union> {u}) \<union> {{v} |v. v \<in> V - {u}})" .
+
+  \<comment> \<open>Auxiliary information is preserved\<close>
+  have "u \<in> U" using assms(2) bprules(3) by blast
+  then have R: "U - (V - {u}) = U - V \<union> {u}" by blast
+  have L: "\<Union> (P\<^sub>1 \<union> wrap B\<^sub>1 \<union> wrap {} \<union> P\<^sub>2 \<union> wrap (B\<^sub>2 \<union> {u})) = \<Union> (P\<^sub>1 \<union> wrap B\<^sub>1 \<union> wrap {} \<union> P\<^sub>2 \<union> wrap B\<^sub>2) \<union> {u}"
+    unfolding wrap_def using NOTIN by auto
+  have 2: "\<Union> (P\<^sub>1 \<union> wrap B\<^sub>1 \<union> wrap {} \<union> P\<^sub>2 \<union> wrap (B\<^sub>2 \<union> {u})) = U - (V - {u})"
+    unfolding L R using invrules(2) by simp
+  have 3: "{} \<notin> P\<^sub>1 \<union> wrap B\<^sub>1 \<union> P\<^sub>2 \<union> wrap (B\<^sub>2 \<union> {u})"
+    using bpE(2)[OF 1] by simp
+  have 4: "B\<^sub>2 \<union> {u} \<notin> P\<^sub>1 \<union> wrap B\<^sub>1 \<union> wrap {} \<union> P\<^sub>2"
+    using NOTIN by auto
+  have 5: "(P\<^sub>1 \<union> wrap B\<^sub>1 \<union> wrap {}) \<inter> (P\<^sub>2 \<union> wrap (B\<^sub>2 \<union> {u})) = {}"
+    using invrules(5) NOTIN unfolding wrap_empty wrap_Un by auto
+
+  from inv\<^sub>1I[OF 1 2 3 4 5] show ?thesis .
+qed
+
+text \<open>If \<open>inv\<^sub>1\<close> holds for the current partial solution, then \<open>inv\<^sub>1\<close> also holds if \<open>B\<^sub>1\<close> and \<open>B\<^sub>2\<close> are
+      added to \<open>P\<^sub>1\<close> and \<open>P\<^sub>2\<close> respectively, \<open>B\<^sub>1\<close> is emptied and \<open>B\<^sub>2\<close> initialized with \<open>u \<in> V\<close>.\<close>
+lemma inv\<^sub>1_stepC:
+  assumes "inv\<^sub>1 P\<^sub>1 P\<^sub>2 B\<^sub>1 B\<^sub>2 V" "u \<in> V"
+  shows "inv\<^sub>1 (P\<^sub>1 \<union> wrap B\<^sub>1) (P\<^sub>2 \<union> wrap B\<^sub>2) {} {u} (V - {u})"
+proof -
+  note invrules = inv\<^sub>1E[OF assms(1)]
+  \<comment> \<open>Rule 1-4: Correct Bin Packing\<close>
+  have "P\<^sub>1 \<union> wrap B\<^sub>1 \<union> wrap {} \<union> (P\<^sub>2 \<union> wrap B\<^sub>2) \<union> wrap {u} \<union> {{v} |v. v \<in> V - {u}}
+      = P\<^sub>1 \<union> wrap B\<^sub>1 \<union> P\<^sub>2 \<union> wrap B\<^sub>2 \<union> {{u}} \<union> {{v} |v. v \<in> V - {u}}"
+    by (metis (no_types, lifting) Un_assoc Un_empty_right insert_not_empty wrap_empty wrap_not_empty)
+  also have "... = P\<^sub>1 \<union> wrap B\<^sub>1 \<union> P\<^sub>2 \<union> wrap B\<^sub>2 \<union> {{v} |v. v \<in> V}"
+    using assms(2) by auto
+  finally have EQ: "P\<^sub>1 \<union> wrap B\<^sub>1 \<union> wrap {} \<union> (P\<^sub>2 \<union> wrap B\<^sub>2) \<union> wrap {u} \<union> {{v} |v. v \<in> V - {u}}
+                  = P\<^sub>1 \<union> wrap B\<^sub>1 \<union> P\<^sub>2 \<union> wrap B\<^sub>2 \<union> {{v} |v. v \<in> V}" .
+  from invrules(1) have 1: "bp (P\<^sub>1 \<union> wrap B\<^sub>1 \<union> wrap {} \<union> (P\<^sub>2 \<union> wrap B\<^sub>2) \<union> wrap {u} \<union> {{v} |v. v \<in> V - {u}})"
+    unfolding EQ .
+
+  \<comment> \<open>Auxiliary information is preserved\<close>
+  have NOTIN: "\<forall>M \<in> P\<^sub>1 \<union> wrap B\<^sub>1 \<union> P\<^sub>2 \<union> wrap B\<^sub>2 \<union> {{v} |v. v \<in> V - {u}}. u \<notin> M"
+    using invrules(2) assms(2) by blast
+  have "u \<in> U" using assms(2) bpE(3)[OF invrules(1)] by blast
+  then have R: "U - (V - {u}) = U - V \<union> {u}" by blast
+  have L: "\<Union> (P\<^sub>1 \<union> wrap B\<^sub>1 \<union> wrap {} \<union> (P\<^sub>2 \<union> wrap B\<^sub>2) \<union> wrap {u}) = \<Union> (P\<^sub>1 \<union> wrap B\<^sub>1 \<union> wrap {} \<union> (P\<^sub>2 \<union> wrap B\<^sub>2)) \<union> {u}"
+    unfolding wrap_def using NOTIN by auto
+  have 2: "\<Union> (P\<^sub>1 \<union> wrap B\<^sub>1 \<union> wrap {} \<union> (P\<^sub>2 \<union> wrap B\<^sub>2) \<union> wrap {u}) = U - (V - {u})"
+    unfolding L R using invrules(2) by auto
+  have 3: "{} \<notin> P\<^sub>1 \<union> wrap B\<^sub>1 \<union> (P\<^sub>2 \<union> wrap B\<^sub>2) \<union> wrap {u}"
+    using bpE(2)[OF 1] by simp
+  have 4: "{u} \<notin> P\<^sub>1 \<union> wrap B\<^sub>1 \<union> wrap {} \<union> (P\<^sub>2 \<union> wrap B\<^sub>2)"
+    using NOTIN by auto
+  have 5: "(P\<^sub>1 \<union> wrap B\<^sub>1 \<union> wrap {}) \<inter> (P\<^sub>2 \<union> wrap B\<^sub>2 \<union> wrap {u}) = {}"
+    using invrules(5) NOTIN unfolding wrap_def by force
+
+  from inv\<^sub>1I[OF 1 2 3 4 5] show ?thesis .
+qed
+
+text \<open>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 \<open>P\<close> is a correct solution of the bin packing problem.\<close>
+lemma simple_bp_correct:
+"VARS P P\<^sub>1 P\<^sub>2 B\<^sub>1 B\<^sub>2 V u
+  {True}
+  P\<^sub>1 := {}; P\<^sub>2 := {}; B\<^sub>1 := {}; B\<^sub>2 := {}; V := U;
+  WHILE V \<inter> S \<noteq> {} INV {inv\<^sub>1 P\<^sub>1 P\<^sub>2 B\<^sub>1 B\<^sub>2 V} DO
+    u := (SOME u. u \<in> V); V := V - {u};
+    IF W(B\<^sub>1) + w(u) \<le> c
+    THEN B\<^sub>1 := B\<^sub>1 \<union> {u}
+    ELSE IF W(B\<^sub>2) + w(u) \<le> c
+         THEN B\<^sub>2 := B\<^sub>2 \<union> {u}
+         ELSE P\<^sub>2 := P\<^sub>2 \<union> wrap B\<^sub>2; B\<^sub>2 := {u} FI;
+         P\<^sub>1 := P\<^sub>1 \<union> wrap B\<^sub>1; B\<^sub>1 := {} FI
+  OD;
+  P := P\<^sub>1 \<union> wrap B\<^sub>1 \<union> P\<^sub>2 \<union> wrap B\<^sub>2 \<union> {{v} | v. v \<in> V}
+  {bp P}"
+proof (vcg, goal_cases)
+  case (1 P P\<^sub>1 P\<^sub>2 B\<^sub>1 B\<^sub>2 V u)
+  show ?case
+    unfolding bp_def partition_on_def pairwise_def wrap_def inv\<^sub>1_def
+    using weight by auto
+next
+  case (2 P P\<^sub>1 P\<^sub>2 B\<^sub>1 B\<^sub>2 V u)
+  then have INV: "inv\<^sub>1 P\<^sub>1 P\<^sub>2 B\<^sub>1 B\<^sub>2 V" ..
+  from 2 have "V \<noteq> {}" by blast
+  then have IN: "(SOME u. u \<in> V) \<in> V" by (simp add: some_in_eq)
+  from inv\<^sub>1_stepA[OF INV IN] inv\<^sub>1_stepB[OF INV IN] inv\<^sub>1_stepC[OF INV IN]
+  show ?case by blast
+next
+  case (3 P P\<^sub>1 P\<^sub>2 B\<^sub>1 B\<^sub>2 V u)
+  then show ?case unfolding inv\<^sub>1_def by blast
+qed
+
+subsubsection \<open>Lower Bounds for the Bin Packing Problem\<close>
+
+lemma bp_bins_finite [simp]:
+  assumes "bp P"
+  shows "\<forall>B \<in> 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 \<open>If \<open>P\<close> is a solution of the bin packing problem, then no bin in \<open>P\<close> may contain more than
+      one large object.\<close>
+lemma only_one_L_per_bin:
+  assumes "bp P" "B \<in> P"
+  shows "\<forall>x \<in> B. \<forall>y \<in> B. x \<noteq> y \<longrightarrow> x \<notin> L \<or> y \<notin> L"
+proof (rule ccontr, simp)
+  assume "\<exists>x\<in>B. \<exists>y\<in>B. x \<noteq> y \<and> x \<in> L \<and> y \<in> L"
+  then obtain x y where *: "x \<in> B" "y \<in> B" "x \<noteq> y" "x \<in> L" "y \<in> 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 \<in> B - {x}" using *(2,3) by blast
+  have "W B = W (B - {x}) + w x"
+    using *(1) \<open>finite B\<close> by (simp add: sum.remove)
+  also have "... = W (B - {x} - {y}) + w x + w y"
+    using \<open>y \<in> B - {x}\<close> \<open>finite B\<close> by (simp add: sum.remove)
+  finally have *: "W B = W (B - {x} - {y}) + w x + w y" .
+  have "\<forall>u \<in> B. 0 < w u" using bpE(3)[OF assms(1)] assms(2) weight by blast
+  then have "0 \<le> W (B - {x} - {y})" by (smt DiffD1 sum_nonneg)
+  with * have "c < W B" using \<open>c < w x + w y\<close> by simp
+  then show False using bpE(4)[OF assms(1)] assms(2) by fastforce
+qed
+
+text \<open>If \<open>P\<close> 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.\<close>
+lemma L_lower_bound_card:
+  assumes "bp P"
+  shows "card L \<le> card P"
+proof -
+  have "\<forall>x \<in> L. \<exists>B \<in> P. x \<in> B"
+    using bpE(3)[OF assms] L_def by blast
+  then obtain f where f_def: "\<forall>u \<in> L. u \<in> f u \<and> f u \<in> 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 \<subseteq> P" using f_def by blast
+  moreover have "finite P" using assms by simp
+  ultimately have "card (f ` L) \<le> card P" by (simp add: card_mono)
+  then show ?thesis unfolding card_eq .
+qed
+
+text \<open>If \<open>P\<close> 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.\<close>
+lemma subset_bp_card:
+  assumes "bp P" "M \<subseteq> P" "\<forall>B \<in> M. B \<inter> L \<noteq> {}"
+  shows "card M \<le> card L"
+proof -
+  have "\<forall>B \<in> M. \<exists>u \<in> L. u \<in> B" using assms(3) by fast
+  then have "\<exists>f. \<forall>B \<in> M. f B \<in> L \<and> f B \<in> B" by metis
+  then obtain f where f_def: "\<forall>B \<in> M. f B \<in> L \<and> f B \<in> B" ..
+  have "inj_on f M"
+  proof (rule ccontr)
+    assume "\<not> inj_on f M"
+    then have "\<exists>x \<in> M. \<exists>y \<in> M. x \<noteq> y \<and> f x = f y" unfolding inj_on_def by blast
+    then obtain x y where *: "x \<in> M" "y \<in> M" "x \<noteq> y" "f x = f y" by blast
+    then have "\<exists>u. u \<in> x \<and> u \<in> y" using f_def by metis
+    then have "x \<inter> y \<noteq> {}" 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 \<subseteq> L" using f_def by blast
+  ultimately show ?thesis using card_inj_on_le by blast
+qed
+
+text \<open>If \<open>P\<close> is a correct solution of the bin packing problem, \<open>inv\<^sub>1\<close> holds for the partial solution,
+      and every bin in \<open>P\<^sub>1 \<union> wrap B\<^sub>1\<close> contains a large object, then the amount of bins in
+      \<open>P\<^sub>1 \<union> wrap B\<^sub>1 \<union> {{v} |v. v \<in> V \<inter> L}\<close> is a lower bound for the amount of bins in \<open>P\<close>.\<close>
+lemma L_bins_lower_bound_card:
+  assumes "bp P" "inv\<^sub>1 P\<^sub>1 P\<^sub>2 B\<^sub>1 B\<^sub>2 V" "\<forall>B \<in> P\<^sub>1 \<union> wrap B\<^sub>1. B \<inter> L \<noteq> {}"
+  shows "card (P\<^sub>1 \<union> wrap B\<^sub>1 \<union> {{v} |v. v \<in> V \<inter> L}) \<le> card P"
+proof -
+  note invrules = inv\<^sub>1E[OF assms(2)]
+  have "\<forall>B \<in> {{v} |v. v \<in> V \<inter> L}. B \<inter> L \<noteq> {}" by blast
+  with assms(3) have
+    "P\<^sub>1 \<union> wrap B\<^sub>1 \<union> {{v} |v. v \<in> V \<inter> L} \<subseteq> P\<^sub>1 \<union> wrap B\<^sub>1 \<union> P\<^sub>2 \<union> wrap B\<^sub>2 \<union> {{v} |v. v \<in> V}"
+    "\<forall>B \<in> P\<^sub>1 \<union> wrap B\<^sub>1 \<union> {{v} |v. v \<in> V \<inter> L}. B \<inter> L \<noteq> {}" by blast+
+  from subset_bp_card[OF invrules(1) this] show ?thesis
+    using L_lower_bound_card[OF assms(1)] by linarith
+qed
+
+text \<open>If \<open>P\<close> 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 \<open>P\<close>.\<close>
+lemma sum_Un_eq_sum_sum:
+  assumes "bp P"
+  shows "(\<Sum>u \<in> U. w u) = (\<Sum>B \<in> P. W B)"
+proof -
+  have FINITE: "\<forall>B \<in> P. finite B" using assms by simp
+  have DISJNT: "\<forall>A \<in> P. \<forall>B \<in> P. A \<noteq> B \<longrightarrow> A \<inter> B = {}"
+    using bpE(1)[OF assms] unfolding pairwise_def disjnt_def .
+  have "(\<Sum>u \<in> (\<Union>P). w u) = (\<Sum>B \<in> P. W B)"
+    using sum.Union_disjoint[OF FINITE DISJNT] by auto
+  then show ?thesis unfolding bpE(3)[OF assms] .
+qed
+
+text \<open>If \<open>P\<close> 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 \<open>P\<close> multiplied by their maximum capacity.\<close>
+lemma sum_lower_bound_card:
+  assumes "bp P"
+  shows "(\<Sum>u \<in> U. w u) \<le> c * card P"
+proof -
+  have *: "\<forall>B \<in> P. 0 < W B \<and> W B \<le> c"
+    using bpE(2-4)[OF assms] weight by (metis UnionI assms bp_bins_finite sum_pos)
+  have "(\<Sum>u \<in> U. w u) = (\<Sum>B \<in> P. W B)"
+    using sum_Un_eq_sum_sum[OF assms] .
+  also have "... \<le> (\<Sum>B \<in> 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 \<noteq> {}"
+  using U_NE bpE(3)[OF assms] by blast
+
+lemma sum_Un_ge:
+  fixes f :: "_ \<Rightarrow> real"
+  assumes "finite M" "finite N" "\<forall>B \<in> M \<union> N. 0 < f B"
+  shows "sum f M \<le> sum f (M \<union> N)"
+proof -
+  have "0 \<le> sum f N - sum f (M \<inter> N)"
+    using assms by (smt DiffD1 inf.cobounded2 UnCI sum_mono2)
+  then have "sum f M \<le> sum f M + sum f N - sum f (M \<inter> N)"
+    by simp
+  also have "... = sum f (M \<union> N)"
+    using sum_Un[OF assms(1,2), symmetric] .
+  finally show ?thesis .
+qed
+
+text \<open>If \<open>bij_exists\<close> holds, one can obtain a function which is bijective between the bins in \<open>P\<close>
+and the objects in \<open>V\<close> such that an object returned by the function would cause the bin to
+exceed its capacity.\<close>
+definition bij_exists :: "'a set set \<Rightarrow> 'a set \<Rightarrow> bool" where
+  "bij_exists P V = (\<exists>f. bij_betw f P V \<and> (\<forall>B \<in> P. W B + w (f B) > c))"
+
+text \<open>If \<open>P\<close> is a functionally correct solution of the bin packing problem, \<open>inv\<^sub>1\<close> holds for the
+partial solution, and such a bijective function exists between the bins in \<open>P\<^sub>1\<close> and the objects in
+@{term "P\<^sub>2 \<union> wrap B\<^sub>2"}, the following strict lower bound can be shown:\<close>
+lemma P\<^sub>1_lower_bound_card:
+  assumes "bp P" "inv\<^sub>1 P\<^sub>1 P\<^sub>2 B\<^sub>1 B\<^sub>2 V" "bij_exists P\<^sub>1 (\<Union>(P\<^sub>2 \<union> wrap B\<^sub>2))"
+  shows "card P\<^sub>1 + 1 \<le> card P"
+proof (cases \<open>P\<^sub>1 = {}\<close>)
+  case True
+  have "finite P" using assms(1) by simp
+  then have "1 \<le> 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 = inv\<^sub>1E[OF assms(2)]
+  case False
+  obtain f where f_def: "bij_betw f P\<^sub>1 (\<Union>(P\<^sub>2 \<union> wrap B\<^sub>2))" "\<forall>B \<in> P\<^sub>1. W B + w (f B) > c"
+    using assms(3) unfolding bij_exists_def by blast
+  have FINITE: "finite P\<^sub>1" "finite (P\<^sub>2 \<union> wrap B\<^sub>2)" "finite (P\<^sub>1 \<union> P\<^sub>2 \<union> wrap B\<^sub>2)" "finite (wrap B\<^sub>1 \<union> {{v} |v. v \<in> V})"
+    using inv\<^sub>1E(1)[OF assms(2)] bp_sol_finite by blast+
+
+  have F: "\<forall>B \<in> P\<^sub>2 \<union> wrap B\<^sub>2. finite B" using invrules(1) by simp
+  have D: "\<forall>A \<in> P\<^sub>2 \<union> wrap B\<^sub>2. \<forall>B \<in> P\<^sub>2 \<union> wrap B\<^sub>2. A \<noteq> B \<longrightarrow> A \<inter> B = {}"
+    using bpE(1)[OF invrules(1)] unfolding pairwise_def disjnt_def by auto
+  have sum_eq: "W (\<Union> (P\<^sub>2 \<union> wrap B\<^sub>2)) = (\<Sum>B \<in> P\<^sub>2 \<union> wrap B\<^sub>2. W B)"
+    using sum.Union_disjoint[OF F D] by auto
+
+  have "\<forall>B\<in>P\<^sub>1 \<union> wrap B\<^sub>1 \<union> P\<^sub>2 \<union> wrap B\<^sub>2 \<union> {{v} |v. v \<in> 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 "(\<Sum>B \<in> P\<^sub>1 \<union> P\<^sub>2 \<union> wrap B\<^sub>2. W B) \<le> (\<Sum>B \<in> P\<^sub>1 \<union> P\<^sub>2 \<union> wrap B\<^sub>2 \<union> (wrap B\<^sub>1 \<union> {{v} |v. v \<in> V}). W B)"
+    using sum_Un_ge[OF FINITE(3,4), of W] by blast
+  also have "... = (\<Sum>B \<in> P\<^sub>1 \<union> wrap B\<^sub>1 \<union> P\<^sub>2 \<union> wrap B\<^sub>2 \<union> {{v} |v. v \<in> 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 *: "(\<Sum>B \<in> P\<^sub>1 \<union> P\<^sub>2 \<union> wrap B\<^sub>2. W B) \<le> W U" .
+
+  \<comment> \<open>This follows from the fourth and final additional conjunct of \<open>inv\<^sub>1\<close> 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 \<open>P\<^sub>1\<close> and \<open>P\<^sub>2 \<union> wrap B\<^sub>2\<close> happened to be equal.\<close>
+  have DISJNT: "P\<^sub>1 \<inter> (P\<^sub>2 \<union> wrap B\<^sub>2) = {}" using invrules(5) by blast
+
+  \<comment> \<open>This part of the proof is based on the proof on page 72 of the article @{cite BerghammerR03}.\<close>
+  have "c * card P\<^sub>1 = (\<Sum>B \<in> P\<^sub>1. c)" by simp
+  also have "... < (\<Sum>B \<in> P\<^sub>1. W B + w (f B))"
+    using f_def(2) sum_strict_mono[OF FINITE(1) False] by fastforce
+  also have "... = (\<Sum>B \<in> P\<^sub>1. W B) + (\<Sum>B \<in> P\<^sub>1. w (f B))"
+    by (simp add: Groups_Big.comm_monoid_add_class.sum.distrib)
+  also have "... = (\<Sum>B \<in> P\<^sub>1. W B) + W (\<Union> (P\<^sub>2 \<union> wrap B\<^sub>2))" unfolding sum.reindex_bij_betw[OF f_def(1), of w] ..
+  also have "... = (\<Sum>B \<in> P\<^sub>1. W B) + (\<Sum>B \<in> P\<^sub>2 \<union> wrap B\<^sub>2. W B)" unfolding sum_eq ..
+  also have "... = (\<Sum>B \<in> P\<^sub>1 \<union> P\<^sub>2 \<union> wrap B\<^sub>2. W B)" using sum.union_disjoint[OF FINITE(1,2) DISJNT, of W] by (simp add: Un_assoc)
+  also have "... \<le> (\<Sum>u \<in> U. w u)" using * .
+  also have "... \<le> 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 \<open>As @{thm wrap_card} holds, it follows that the amount of bins in \<open>P\<^sub>1 \<union> wrap B\<^sub>1\<close>
+      are a lower bound for the amount of bins in \<open>P\<close>.\<close>
+lemma P\<^sub>1_B\<^sub>1_lower_bound_card:
+  assumes "bp P" "inv\<^sub>1 P\<^sub>1 P\<^sub>2 B\<^sub>1 B\<^sub>2 V" "bij_exists P\<^sub>1 (\<Union>(P\<^sub>2 \<union> wrap B\<^sub>2))"
+  shows "card (P\<^sub>1 \<union> wrap B\<^sub>1) \<le> card P"
+proof -
+  have "card (P\<^sub>1 \<union> wrap B\<^sub>1) \<le> card P\<^sub>1 + card (wrap B\<^sub>1)"
+    using card_Un_le by blast
+  also have "... \<le> card P\<^sub>1 + 1" using wrap_card by simp
+  also have "... \<le> card P" using P\<^sub>1_lower_bound_card[OF assms] .
+  finally show ?thesis .
+qed
+
+text \<open>If \<open>inv\<^sub>1\<close> holds, there are at most half as many bins in \<open>P\<^sub>2\<close> as there are objects in \<open>P\<^sub>2\<close>, and we can again
+      obtain a bijective function between the bins in \<open>P\<^sub>1\<close> 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.\<close>
+lemma P\<^sub>2_B\<^sub>2_lower_bound_P\<^sub>1:
+  assumes "inv\<^sub>1 P\<^sub>1 P\<^sub>2 B\<^sub>1 B\<^sub>2 V" "2 * card P\<^sub>2 \<le> card (\<Union>P\<^sub>2)" "bij_exists P\<^sub>1 (\<Union>(P\<^sub>2 \<union> wrap B\<^sub>2))"
+  shows "2 * card (P\<^sub>2 \<union> wrap B\<^sub>2) \<le> card P\<^sub>1 + 1"
+proof -
+  note invrules = inv\<^sub>1E[OF assms(1)] and bprules = bpE[OF invrules(1)]
+
+  have "pairwise disjnt (P\<^sub>2 \<union> wrap B\<^sub>2)"
+    using bprules(1) pairwise_subset by blast
+  moreover have "B\<^sub>2 \<notin> P\<^sub>2" using invrules(4) by simp
+  ultimately have DISJNT: "\<Union>P\<^sub>2 \<inter> B\<^sub>2 = {}"
+    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 (\<Union>P\<^sub>2)" using U_Finite bprules(3) by auto
+  have "finite B\<^sub>2" using bp_bins_finite[OF invrules(1)] wrap_not_empty by blast
+  have "finite P\<^sub>2" "finite (wrap B\<^sub>2)" using bp_sol_finite[OF invrules(1)] by blast+
+  have DISJNT2: "P\<^sub>2 \<inter> wrap B\<^sub>2 = {}" unfolding wrap_def using \<open>B\<^sub>2 \<notin> P\<^sub>2\<close> by auto
+  have "card (wrap B\<^sub>2) \<le> card B\<^sub>2"
+  proof (cases \<open>B\<^sub>2 = {}\<close>)
+    case False
+    then have "1 \<le> card B\<^sub>2" by (simp add: leI \<open>finite B\<^sub>2\<close>)
+    then show ?thesis using wrap_card[of B\<^sub>2] by linarith
+  qed simp
+
+  \<comment> \<open>This part of the proof is based on the proof on page 73 of the article @{cite BerghammerR03}.\<close>
+  from assms(2) have "2 * card P\<^sub>2 + 2 * card (wrap B\<^sub>2) \<le> card (\<Union>P\<^sub>2) + card (wrap B\<^sub>2) + 1"
+    using wrap_card[of B\<^sub>2] by linarith
+  then have "2 * (card P\<^sub>2 + card (wrap B\<^sub>2)) \<le> card (\<Union>P\<^sub>2) + card B\<^sub>2 + 1"
+    using \<open>card (wrap B\<^sub>2) \<le> card B\<^sub>2\<close> by simp
+  then have "2 * (card (P\<^sub>2 \<union> wrap B\<^sub>2)) \<le> card (\<Union>P\<^sub>2 \<union> B\<^sub>2) + 1"
+    using card_Un_disjoint[OF \<open>finite (\<Union>P\<^sub>2)\<close> \<open>finite B\<^sub>2\<close> DISJNT]
+      and card_Un_disjoint[OF \<open>finite P\<^sub>2\<close> \<open>finite (wrap B\<^sub>2)\<close> DISJNT2] by argo
+  then have "2 * (card (P\<^sub>2 \<union> wrap B\<^sub>2)) \<le> card (\<Union>(P\<^sub>2 \<union> wrap B\<^sub>2)) + 1"
+    by (cases \<open>B\<^sub>2 = {}\<close>) (auto simp: Un_commute)
+  then show "2 * (card (P\<^sub>2 \<union> wrap B\<^sub>2)) \<le> card P\<^sub>1 + 1"
+    using assms(3) bij_betw_same_card unfolding bij_exists_def by metis
+qed
+
+subsubsection \<open>Proving the Approximation Factor\<close>
+
+text \<open>We define \<open>inv\<^sub>2\<close> as it is defined in the article.
+      These conjuncts allow us to prove the desired approximation factor.\<close>
+definition inv\<^sub>2 :: "'a set set \<Rightarrow> 'a set set \<Rightarrow> 'a set \<Rightarrow> 'a set \<Rightarrow> 'a set \<Rightarrow> bool" where
+  "inv\<^sub>2 P\<^sub>1 P\<^sub>2 B\<^sub>1 B\<^sub>2 V \<longleftrightarrow> inv\<^sub>1 P\<^sub>1 P\<^sub>2 B\<^sub>1 B\<^sub>2 V \<comment> \<open>\<open>inv\<^sub>1\<close> holds for the partial solution\<close>
+                       \<and> (V \<inter> L \<noteq> {} \<longrightarrow> (\<forall>B \<in> P\<^sub>1 \<union> wrap B\<^sub>1. B \<inter> L \<noteq> {})) \<comment> \<open>If there are still large objects left, then every bin of the first partial solution must contain a large object\<close>
+                       \<and> bij_exists P\<^sub>1 (\<Union>(P\<^sub>2 \<union> wrap B\<^sub>2)) \<comment> \<open>There exists a bijective function between the bins of the first partial solution and the objects of the second one\<close>
+                       \<and> (2 * card P\<^sub>2 \<le> card (\<Union>P\<^sub>2)) \<comment> \<open>There are at most twice as many bins in \<open>P\<^sub>2\<close> as there are objects in \<open>P\<^sub>2\<close>\<close>"
+
+lemma inv\<^sub>2E:
+  assumes "inv\<^sub>2 P\<^sub>1 P\<^sub>2 B\<^sub>1 B\<^sub>2 V"
+  shows "inv\<^sub>1 P\<^sub>1 P\<^sub>2 B\<^sub>1 B\<^sub>2 V"
+    and "V \<inter> L \<noteq> {} \<Longrightarrow> \<forall>B \<in> P\<^sub>1 \<union> wrap B\<^sub>1. B \<inter> L \<noteq> {}"
+    and "bij_exists P\<^sub>1 (\<Union>(P\<^sub>2 \<union> wrap B\<^sub>2))"
+    and "2 * card P\<^sub>2 \<le> card (\<Union>P\<^sub>2)"
+  using assms unfolding inv\<^sub>2_def by blast+
+
+lemma inv\<^sub>2I:
+  assumes "inv\<^sub>1 P\<^sub>1 P\<^sub>2 B\<^sub>1 B\<^sub>2 V"
+    and "V \<inter> L \<noteq> {} \<Longrightarrow> \<forall>B \<in> P\<^sub>1 \<union> wrap B\<^sub>1. B \<inter> L \<noteq> {}"
+    and "bij_exists P\<^sub>1 (\<Union>(P\<^sub>2 \<union> wrap B\<^sub>2))"
+    and "2 * card P\<^sub>2 \<le> card (\<Union>P\<^sub>2)"
+  shows "inv\<^sub>2 P\<^sub>1 P\<^sub>2 B\<^sub>1 B\<^sub>2 V"
+  using assms unfolding inv\<^sub>2_def by blast
+
+text \<open>If \<open>P\<close> is a correct solution of the bin packing problem, \<open>inv\<^sub>2\<close> 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 \<open>3 / 2\<close> of the amount of bins in \<open>P\<close>. This proof strongly follows the proof in
+      \<open>Theorem 4.1\<close> of the article @{cite BerghammerR03}.\<close>
+lemma bin_packing_lower_bound_card:
+  assumes "V \<inter> S = {}" "inv\<^sub>2 P\<^sub>1 P\<^sub>2 B\<^sub>1 B\<^sub>2 V" "bp P"
+  shows "card (P\<^sub>1 \<union> wrap B\<^sub>1 \<union> P\<^sub>2 \<union> wrap B\<^sub>2 \<union> {{v} |v. v \<in> V}) \<le> 3 / 2 * card P"
+proof (cases \<open>V = {}\<close>)
+  note invrules = inv\<^sub>2E[OF assms(2)]
+  case True
+  then have "card (P\<^sub>1 \<union> wrap B\<^sub>1 \<union> P\<^sub>2 \<union> wrap B\<^sub>2 \<union> {{v} |v. v \<in> V})
+           = card (P\<^sub>1 \<union> wrap B\<^sub>1 \<union> P\<^sub>2 \<union> wrap B\<^sub>2)" by simp
+  also have "... \<le> card (P\<^sub>1 \<union> wrap B\<^sub>1) + card (P\<^sub>2 \<union> wrap B\<^sub>2)"
+    using card_Un_le[of \<open>P\<^sub>1 \<union> wrap B\<^sub>1\<close>] by (simp add: Un_assoc)
+  also have "... \<le> card P + card (P\<^sub>2 \<union> wrap B\<^sub>2)"
+    using P\<^sub>1_B\<^sub>1_lower_bound_card[OF assms(3) invrules(1,3)] by simp
+  also have "... \<le> card P + card P / 2"
+    using P\<^sub>2_B\<^sub>2_lower_bound_P\<^sub>1[OF invrules(1,4,3)]
+      and P\<^sub>1_lower_bound_card[OF assms(3) invrules(1,3)] by linarith
+  finally show ?thesis by linarith
+next
+  note invrules = inv\<^sub>2E[OF assms(2)]
+  case False
+  have "U = S \<union> L" using S_def L_def by blast
+  then have *: "V = V \<inter> L"
+    using bpE(3)[OF inv\<^sub>1E(1)[OF invrules(1)]]
+      and assms(1) by blast
+  with False have NE: "V \<inter> L \<noteq> {}" by simp
+  have "card (P\<^sub>1 \<union> wrap B\<^sub>1 \<union> P\<^sub>2 \<union> wrap B\<^sub>2 \<union> {{v} |v. v \<in> V})
+      = card (P\<^sub>1 \<union> wrap B\<^sub>1 \<union> {{v} |v. v \<in> V \<inter> L} \<union> P\<^sub>2 \<union> wrap B\<^sub>2)"
+    using * by (simp add: Un_commute Un_assoc)
+  also have "... \<le> card (P\<^sub>1 \<union> wrap B\<^sub>1 \<union> {{v} |v. v \<in> V \<inter> L}) + card (P\<^sub>2 \<union> wrap B\<^sub>2)"
+    using card_Un_le[of \<open>P\<^sub>1 \<union> wrap B\<^sub>1 \<union> {{v} |v. v \<in> V \<inter> L}\<close>] by (simp add: Un_assoc)
+  also have "... \<le> card P + card (P\<^sub>2 \<union> wrap B\<^sub>2)"
+    using L_bins_lower_bound_card[OF assms(3) invrules(1) invrules(2)[OF NE]] by linarith
+  also have "... \<le> card P + card P / 2"
+    using P\<^sub>2_B\<^sub>2_lower_bound_P\<^sub>1[OF invrules(1,4,3)]
+      and P\<^sub>1_lower_bound_card[OF assms(3) invrules(1,3)] by linarith
+  finally show ?thesis by linarith
+qed
+
+text \<open>We define \<open>inv\<^sub>3\<close> as it is defined in the article.
+      This final conjunct allows us to prove that the invariant will be maintained by the algorithm.\<close>
+definition inv\<^sub>3 :: "'a set set \<Rightarrow> 'a set set \<Rightarrow> 'a set \<Rightarrow> 'a set \<Rightarrow> 'a set \<Rightarrow> bool" where
+  "inv\<^sub>3 P\<^sub>1 P\<^sub>2 B\<^sub>1 B\<^sub>2 V \<longleftrightarrow> inv\<^sub>2 P\<^sub>1 P\<^sub>2 B\<^sub>1 B\<^sub>2 V \<and> B\<^sub>2 \<subseteq> S"
+
+lemma inv\<^sub>3E:
+  assumes "inv\<^sub>3 P\<^sub>1 P\<^sub>2 B\<^sub>1 B\<^sub>2 V"
+  shows "inv\<^sub>2 P\<^sub>1 P\<^sub>2 B\<^sub>1 B\<^sub>2 V" and "B\<^sub>2 \<subseteq> S"
+  using assms unfolding inv\<^sub>3_def by blast+
+
+lemma inv\<^sub>3I:
+  assumes "inv\<^sub>2 P\<^sub>1 P\<^sub>2 B\<^sub>1 B\<^sub>2 V" and "B\<^sub>2 \<subseteq> S"
+  shows "inv\<^sub>3 P\<^sub>1 P\<^sub>2 B\<^sub>1 B\<^sub>2 V"
+  using assms unfolding inv\<^sub>3_def by blast
+
+lemma loop_init:
+  "inv\<^sub>3 {} {} {} {} U"
+proof -
+  have *: "inv\<^sub>1 {} {} {} {} U"
+    unfolding bp_def partition_on_def pairwise_def wrap_def inv\<^sub>1_def
+    using weight by auto
+  have "bij_exists {} (\<Union> ({} \<union> wrap {}))"
+    using bij_betwI' unfolding bij_exists_def by fastforce
+  from inv\<^sub>2I[OF * _ this] have "inv\<^sub>2 {} {} {} {} U" by auto
+  from inv\<^sub>3I[OF this] show ?thesis by blast
+qed
+
+text \<open>If \<open>B\<^sub>1\<close> is empty and there are no large objects left, then \<open>inv\<^sub>3\<close> will be maintained
+      if \<open>B\<^sub>1\<close> is initialized with \<open>u \<in> V \<inter> S\<close>.\<close>
+lemma loop_stepA:
+  assumes "inv\<^sub>3 P\<^sub>1 P\<^sub>2 B\<^sub>1 B\<^sub>2 V" "B\<^sub>1 = {}" "V \<inter> L = {}" "u \<in> V \<inter> S"
+  shows "inv\<^sub>3 P\<^sub>1 P\<^sub>2 {u} B\<^sub>2 (V - {u})"
+proof -
+  note invrules = inv\<^sub>2E[OF inv\<^sub>3E(1)[OF assms(1)]]
+  have WEIGHT: "W B\<^sub>1 + w u \<le> c" using S_def assms(2,4) by simp
+  from assms(4) have "u \<in> V" by blast
+  from inv\<^sub>1_stepA[OF invrules(1) this WEIGHT] assms(2) have 1: "inv\<^sub>1 P\<^sub>1 P\<^sub>2 {u} B\<^sub>2 (V - {u})" by simp
+  have 2: "(V - {u}) \<inter> L \<noteq> {} \<Longrightarrow> \<forall>B\<in>P\<^sub>1 \<union> wrap {u}. B \<inter> L \<noteq> {}" using assms(3) by blast
+  from inv\<^sub>2I[OF 1 2] invrules have "inv\<^sub>2 P\<^sub>1 P\<^sub>2 {u} B\<^sub>2 (V - {u})" by blast
+  from inv\<^sub>3I[OF this] show ?thesis using inv\<^sub>3E(2)[OF assms(1)] .
+qed
+
+text \<open>If \<open>B\<^sub>1\<close> is empty and there are large objects left, then \<open>inv\<^sub>3\<close> will be maintained
+      if \<open>B\<^sub>1\<close> is initialized with \<open>u \<in> V \<inter> L\<close>.\<close>
+lemma loop_stepB:
+  assumes "inv\<^sub>3 P\<^sub>1 P\<^sub>2 B\<^sub>1 B\<^sub>2 V" "B\<^sub>1 = {}" "u \<in> V \<inter> L"
+  shows "inv\<^sub>3 P\<^sub>1 P\<^sub>2 {u} B\<^sub>2 (V - {u})"
+proof -
+  note invrules = inv\<^sub>2E[OF inv\<^sub>3E(1)[OF assms(1)]]
+  have WEIGHT: "W B\<^sub>1 + w u \<le> c" using L_def weight assms(2,3) by simp
+  from assms(3) have "u \<in> V" by blast
+  from inv\<^sub>1_stepA[OF invrules(1) this WEIGHT] assms(2) have 1: "inv\<^sub>1 P\<^sub>1 P\<^sub>2 {u} B\<^sub>2 (V - {u})" by simp
+  have "\<forall>B\<in>P\<^sub>1. B \<inter> L \<noteq> {}" using assms(3) invrules(2) by blast
+  then have 2: "(V - {u}) \<inter> L \<noteq> {} \<Longrightarrow> \<forall>B\<in>P\<^sub>1 \<union> wrap {u}. B \<inter> L \<noteq> {}"
+    using assms(3) by (metis Int_iff UnE empty_iff insertE singletonI wrap_not_empty)
+  from inv\<^sub>2I[OF 1 2] invrules have "inv\<^sub>2 P\<^sub>1 P\<^sub>2 {u} B\<^sub>2 (V - {u})" by blast
+  from inv\<^sub>3I[OF this] show ?thesis using inv\<^sub>3E(2)[OF assms(1)] .
+qed
+
+text \<open>If \<open>B\<^sub>1\<close> is not empty and \<open>u \<in> V \<inter> S\<close> does not exceed its maximum capacity, then \<open>inv\<^sub>3\<close>
+      will be maintained if \<open>B\<^sub>1\<close> and \<open>{u}\<close> are replaced with \<open>B\<^sub>1 \<union> {u}\<close>.\<close>
+lemma loop_stepC:
+  assumes "inv\<^sub>3 P\<^sub>1 P\<^sub>2 B\<^sub>1 B\<^sub>2 V" "B\<^sub>1 \<noteq> {}" "u \<in> V \<inter> S" "W B\<^sub>1 + w(u) \<le> c"
+  shows "inv\<^sub>3 P\<^sub>1 P\<^sub>2 (B\<^sub>1 \<union> {u}) B\<^sub>2 (V - {u})"
+proof -
+  note invrules = inv\<^sub>2E[OF inv\<^sub>3E(1)[OF assms(1)]]
+  from assms(3) have "u \<in> V" by blast
+  from inv\<^sub>1_stepA[OF invrules(1) this assms(4)] have 1: "inv\<^sub>1 P\<^sub>1 P\<^sub>2 (B\<^sub>1 \<union> {u}) B\<^sub>2 (V - {u})" .
+  have "(V - {u}) \<inter> L \<noteq> {} \<Longrightarrow> \<forall>B\<in>P\<^sub>1 \<union> wrap B\<^sub>1. B \<inter> L \<noteq> {}" using invrules(2) by blast
+  then have 2: "(V - {u}) \<inter> L \<noteq> {} \<Longrightarrow> \<forall>B\<in>P\<^sub>1 \<union> wrap (B\<^sub>1 \<union> {u}). B \<inter> L \<noteq> {}"
+    by (metis Int_commute Un_empty_right Un_insert_right assms(2) disjoint_insert(2) insert_iff wrap_not_empty)
+  from inv\<^sub>2I[OF 1 2] invrules have "inv\<^sub>2 P\<^sub>1 P\<^sub>2 (B\<^sub>1 \<union> {u}) B\<^sub>2 (V - {u})" by blast
+  from inv\<^sub>3I[OF this] show ?thesis using inv\<^sub>3E(2)[OF assms(1)] .
+qed
+
+text \<open>If \<open>B\<^sub>1\<close> is not empty and \<open>u \<in> V \<inter> S\<close> does exceed its maximum capacity but not the capacity of \<open>B\<^sub>2\<close>,
+      then \<open>inv\<^sub>3\<close> will be maintained if \<open>B\<^sub>1\<close> is added to \<open>P\<^sub>1\<close> and emptied, and \<open>B\<^sub>2\<close> and \<open>{u}\<close> are replaced with \<open>B\<^sub>2 \<union> {u}\<close>.\<close>
+lemma loop_stepD:
+  assumes "inv\<^sub>3 P\<^sub>1 P\<^sub>2 B\<^sub>1 B\<^sub>2 V" "B\<^sub>1 \<noteq> {}" "u \<in> V \<inter> S" "W B\<^sub>1 + w(u) > c" "W B\<^sub>2 + w(u) \<le> c"
+  shows "inv\<^sub>3 (P\<^sub>1 \<union> wrap B\<^sub>1) P\<^sub>2 {} (B\<^sub>2 \<union> {u}) (V - {u})"
+proof -
+  note invrules = inv\<^sub>2E[OF inv\<^sub>3E(1)[OF assms(1)]]
+  from assms(3) have "u \<in> V" by blast
+  from inv\<^sub>1_stepB[OF invrules(1) this assms(5)] have 1: "inv\<^sub>1 (P\<^sub>1 \<union> wrap B\<^sub>1) P\<^sub>2 {} (B\<^sub>2 \<union> {u}) (V - {u})" .
+
+  have 2: "(V - {u}) \<inter> L \<noteq> {} \<Longrightarrow> \<forall>B\<in>P\<^sub>1 \<union> wrap B\<^sub>1 \<union> wrap {}. B \<inter> L \<noteq> {}"
+    using invrules(2) unfolding wrap_empty by blast
+
+  from invrules(3) obtain f where f_def: "bij_betw f P\<^sub>1 (\<Union> (P\<^sub>2 \<union> wrap B\<^sub>2))" "\<forall>B\<in>P\<^sub>1. c < W B + w (f B)" unfolding bij_exists_def by blast
+  have "B\<^sub>1 \<notin> P\<^sub>1" using inv\<^sub>1E(3)[OF invrules(1)] by blast
+  have "u \<notin> (\<Union> (P\<^sub>2 \<union> wrap B\<^sub>2))" using inv\<^sub>1E(2)[OF invrules(1)] assms(3) by blast
+  then have "(\<Union> (P\<^sub>2 \<union> wrap (B\<^sub>2 \<union> {u}))) = (\<Union> (P\<^sub>2 \<union> wrap B\<^sub>2 \<union> {{u}}))"
+    by (metis Sup_empty Un_assoc Union_Un_distrib ccpo_Sup_singleton wrap_empty wrap_not_empty)
+  also have "... = (\<Union> (P\<^sub>2 \<union> wrap B\<^sub>2)) \<union> {u}" by simp
+  finally have UN: "(\<Union> (P\<^sub>2 \<union> wrap (B\<^sub>2 \<union> {u}))) = (\<Union> (P\<^sub>2 \<union> wrap B\<^sub>2)) \<union> {u}" .
+  have "wrap B\<^sub>1 = {B\<^sub>1}" using wrap_not_empty[of B\<^sub>1] assms(2) by simp
+  let ?f = "f (B\<^sub>1 := u)"
+  have BIJ: "bij_betw ?f (P\<^sub>1 \<union> wrap B\<^sub>1) (\<Union> (P\<^sub>2 \<union> wrap (B\<^sub>2 \<union> {u})))"
+    unfolding wrap_empty \<open>wrap B\<^sub>1 = {B\<^sub>1}\<close> UN using f_def(1) \<open>B\<^sub>1 \<notin> P\<^sub>1\<close> \<open>u \<notin> (\<Union> (P\<^sub>2 \<union> wrap B\<^sub>2))\<close>
+    by (metis (no_types, lifting) bij_betw_cong fun_upd_other fun_upd_same notIn_Un_bij_betw3)
+  have "c < W B\<^sub>1 + w (?f B\<^sub>1)" using assms(4) by simp
+  then have "(\<forall>B\<in>P\<^sub>1 \<union> wrap B\<^sub>1. c < W B + w (?f B))"
+    unfolding \<open>wrap B\<^sub>1 = {B\<^sub>1}\<close> using f_def(2) by simp
+  with BIJ have "bij_betw ?f (P\<^sub>1 \<union> wrap B\<^sub>1) (\<Union> (P\<^sub>2 \<union> wrap (B\<^sub>2 \<union> {u})))
+              \<and> (\<forall>B\<in>P\<^sub>1 \<union> wrap B\<^sub>1. c < W B + w (?f B))" by blast
+  then have 3: "bij_exists (P\<^sub>1 \<union> wrap B\<^sub>1) (\<Union> (P\<^sub>2 \<union> wrap (B\<^sub>2 \<union> {u})))"
+    unfolding bij_exists_def by blast
+  from inv\<^sub>2I[OF 1 2 3] have "inv\<^sub>2 (P\<^sub>1 \<union> wrap B\<^sub>1) P\<^sub>2 {} (B\<^sub>2 \<union> {u}) (V - {u})" using invrules(4) by blast
+
+  from inv\<^sub>3I[OF this] show ?thesis using inv\<^sub>3E(2)[OF assms(1)] assms(3) by blast
+qed
+
+text \<open>If the maximum capacity of \<open>B\<^sub>2\<close> is exceeded by \<open>u \<in> V \<inter> S\<close>,
+      then \<open>B\<^sub>2\<close> must contain at least two objects.\<close>
+lemma B\<^sub>2_at_least_two_objects:
+  assumes "inv\<^sub>3 P\<^sub>1 P\<^sub>2 B\<^sub>1 B\<^sub>2 V" "u \<in> V \<inter> S" "W B\<^sub>2 + w(u) > c"
+  shows "2 \<le> card B\<^sub>2"
+proof (rule ccontr, simp add: not_le)
+  have FINITE: "finite B\<^sub>2" using inv\<^sub>1E(1)[OF inv\<^sub>2E(1)[OF inv\<^sub>3E(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 B\<^sub>2 < 2"
+  then consider (0) "card B\<^sub>2 = 0" | (1) "card B\<^sub>2 = 1" by linarith
+  then show False proof cases
+    case 0 then have "B\<^sub>2 = {}" using FINITE by simp
+    then show ?thesis using assms(2,3) S_def by simp
+  next
+    case 1 then obtain v where "B\<^sub>2 = {v}"
+      using card_1_singletonE by auto
+    with inv\<^sub>3E(2)[OF assms(1)] have "2 * w v \<le> c" using S_def by simp
+    moreover from \<open>B\<^sub>2 = {v}\<close> have "W B\<^sub>2 = w v" by simp
+    ultimately show ?thesis using assms(2,3) S_def by simp
+  qed
+qed
+
+text \<open>If \<open>B\<^sub>1\<close> is not empty and \<open>u \<in> V \<inter> S\<close> exceeds the maximum capacity of both \<open>B\<^sub>1\<close> and \<open>B\<^sub>2\<close>,
+      then \<open>inv\<^sub>3\<close> will be maintained if \<open>B\<^sub>1\<close> and \<open>B\<^sub>2\<close> are added to \<open>P\<^sub>1\<close> and \<open>P\<^sub>2\<close> respectively,
+      emptied, and \<open>B\<^sub>2\<close> initialized with \<open>u\<close>.\<close>
+lemma loop_stepE:
+  assumes "inv\<^sub>3 P\<^sub>1 P\<^sub>2 B\<^sub>1 B\<^sub>2 V" "B\<^sub>1 \<noteq> {}" "u \<in> V \<inter> S" "W B\<^sub>1 + w(u) > c" "W B\<^sub>2 + w(u) > c"
+  shows "inv\<^sub>3 (P\<^sub>1 \<union> wrap B\<^sub>1) (P\<^sub>2 \<union> wrap B\<^sub>2) {} {u} (V - {u})"
+proof -
+  note invrules = inv\<^sub>2E[OF inv\<^sub>3E(1)[OF assms(1)]]
+  from assms(3) have "u \<in> V" by blast
+  from inv\<^sub>1_stepC[OF invrules(1) this] have 1: "inv\<^sub>1 (P\<^sub>1 \<union> wrap B\<^sub>1) (P\<^sub>2 \<union> wrap B\<^sub>2) {} {u} (V - {u})" .
+
+  have 2: "(V - {u}) \<inter> L \<noteq> {} \<Longrightarrow> \<forall>B\<in>P\<^sub>1 \<union> wrap B\<^sub>1 \<union> wrap {}. B \<inter> L \<noteq> {}"
+    using invrules(2) unfolding wrap_empty by blast
+
+  from invrules(3) obtain f where f_def: "bij_betw f P\<^sub>1 (\<Union> (P\<^sub>2 \<union> wrap B\<^sub>2))" "\<forall>B\<in>P\<^sub>1. c < W B + w (f B)" unfolding bij_exists_def by blast
+  have "B\<^sub>1 \<notin> P\<^sub>1" using inv\<^sub>1E(3)[OF invrules(1)] by blast
+  have "u \<notin> (\<Union> (P\<^sub>2 \<union> wrap B\<^sub>2))" using inv\<^sub>1E(2)[OF invrules(1)] assms(3) by blast
+  have "(\<Union> (P\<^sub>2 \<union> wrap B\<^sub>2 \<union> wrap {u})) = (\<Union> (P\<^sub>2 \<union> wrap B\<^sub>2 \<union> {{u}}))" unfolding wrap_def by simp
+  also have "... = (\<Union> (P\<^sub>2 \<union> wrap B\<^sub>2)) \<union> {u}" by simp
+  finally have UN: "(\<Union> (P\<^sub>2 \<union> wrap B\<^sub>2 \<union> wrap {u})) = (\<Union> (P\<^sub>2 \<union> wrap B\<^sub>2)) \<union> {u}" .
+  have "wrap B\<^sub>1 = {B\<^sub>1}" using wrap_not_empty[of B\<^sub>1] assms(2) by simp
+  let ?f = "f (B\<^sub>1 := u)"
+  have BIJ: "bij_betw ?f (P\<^sub>1 \<union> wrap B\<^sub>1) (\<Union> (P\<^sub>2 \<union> wrap B\<^sub>2 \<union> wrap {u}))"
+    unfolding wrap_empty \<open>wrap B\<^sub>1 = {B\<^sub>1}\<close> UN using f_def(1) \<open>B\<^sub>1 \<notin> P\<^sub>1\<close> \<open>u \<notin> (\<Union> (P\<^sub>2 \<union> wrap B\<^sub>2))\<close>
+    by (metis (no_types, lifting) bij_betw_cong fun_upd_other fun_upd_same notIn_Un_bij_betw3)
+  have "c < W B\<^sub>1 + w (?f B\<^sub>1)" using assms(4) by simp
+  then have "(\<forall>B\<in>P\<^sub>1 \<union> wrap B\<^sub>1. c < W B + w (?f B))"
+    unfolding \<open>wrap B\<^sub>1 = {B\<^sub>1}\<close> using f_def(2) by simp
+  with BIJ have "bij_betw ?f (P\<^sub>1 \<union> wrap B\<^sub>1) (\<Union> (P\<^sub>2 \<union> wrap B\<^sub>2 \<union> wrap {u}))
+              \<and> (\<forall>B\<in>P\<^sub>1 \<union> wrap B\<^sub>1. c < W B + w (?f B))" by blast
+  then have 3: "bij_exists (P\<^sub>1 \<union> wrap B\<^sub>1) (\<Union> (P\<^sub>2 \<union> wrap B\<^sub>2 \<union> wrap {u}))"
+    unfolding bij_exists_def by blast
+
+  have 4: "2 * card (P\<^sub>2 \<union> wrap B\<^sub>2) \<le> card (\<Union> (P\<^sub>2 \<union> wrap B\<^sub>2))"
+  proof -
+    note bprules = bpE[OF inv\<^sub>1E(1)[OF invrules(1)]]
+    have "pairwise disjnt (P\<^sub>2 \<union> wrap B\<^sub>2)"
+      using bprules(1) pairwise_subset by blast
+    moreover have "B\<^sub>2 \<notin> P\<^sub>2" using inv\<^sub>1E(4)[OF invrules(1)]  by simp
+    ultimately have DISJNT: "\<Union>P\<^sub>2 \<inter> B\<^sub>2 = {}"
+      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 (\<Union>P\<^sub>2)" using U_Finite bprules(3) by auto
+    have "finite B\<^sub>2" using inv\<^sub>1E(1)[OF invrules(1)] bp_bins_finite wrap_not_empty by blast
+
+    have "2 * card (P\<^sub>2 \<union> wrap B\<^sub>2) \<le> 2 * (card P\<^sub>2 + card (wrap B\<^sub>2))"
+      using card_Un_le[of P\<^sub>2 \<open>wrap B\<^sub>2\<close>] by simp
+    also have "... \<le> 2 * card P\<^sub>2 + 2" using wrap_card by auto
+    also have "... \<le> card (\<Union> P\<^sub>2) + 2" using invrules(4) by simp
+    also have "... \<le> card (\<Union> P\<^sub>2) + card B\<^sub>2" using B\<^sub>2_at_least_two_objects[OF assms(1,3,5)] by simp
+    also have "... = card (\<Union> (P\<^sub>2 \<union> {B\<^sub>2}))" using DISJNT card_Un_disjoint[OF \<open>finite (\<Union>P\<^sub>2)\<close> \<open>finite B\<^sub>2\<close>] by (simp add: Un_commute)
+    also have "... = card (\<Union> (P\<^sub>2 \<union> wrap B\<^sub>2))" by (cases \<open>B\<^sub>2 = {}\<close>) auto
+    finally show ?thesis .
+  qed
+  from inv\<^sub>2I[OF 1 2 3 4] have "inv\<^sub>2 (P\<^sub>1 \<union> wrap B\<^sub>1) (P\<^sub>2 \<union> wrap B\<^sub>2) {} {u} (V - {u})" .
+
+  from inv\<^sub>3I[OF this] show ?thesis using assms(3) by blast
+qed
+
+text \<open>The bin packing algorithm as it is proposed in the article @{cite BerghammerR03}.
+      \<open>P\<close> will not only be a correct solution of the bin packing problem, but the amount of bins
+      will be a lower bound for \<open>3 / 2\<close> of the amount of bins of any correct solution \<open>Q\<close>, and thus
+      guarantee an approximation factor of \<open>3 / 2\<close> for the optimum.\<close>
+lemma bp_approx:
+"VARS P P\<^sub>1 P\<^sub>2 B\<^sub>1 B\<^sub>2 V u
+  {True}
+  P\<^sub>1 := {}; P\<^sub>2 := {}; B\<^sub>1 := {}; B\<^sub>2 := {}; V := U;
+  WHILE V \<inter> S \<noteq> {} INV {inv\<^sub>3 P\<^sub>1 P\<^sub>2 B\<^sub>1 B\<^sub>2 V} DO 
+    IF B\<^sub>1 \<noteq> {}
+    THEN u := (SOME u. u \<in> V \<inter> S)
+    ELSE IF V \<inter> L \<noteq> {}
+         THEN u := (SOME u. u \<in> V \<inter> L)
+         ELSE u := (SOME u. u \<in> V \<inter> S) FI FI;
+    V := V - {u};
+    IF W(B\<^sub>1) + w(u) \<le> c
+    THEN B\<^sub>1 := B\<^sub>1 \<union> {u}
+    ELSE IF W(B\<^sub>2) + w(u) \<le> c
+         THEN B\<^sub>2 := B\<^sub>2 \<union> {u}
+         ELSE P\<^sub>2 := P\<^sub>2 \<union> wrap B\<^sub>2; B\<^sub>2 := {u} FI;
+         P\<^sub>1 := P\<^sub>1 \<union> wrap B\<^sub>1; B\<^sub>1 := {} FI
+  OD;
+  P := P\<^sub>1 \<union> wrap B\<^sub>1 \<union> P\<^sub>2 \<union> wrap B\<^sub>2 \<union> {{v} | v. v \<in> V}
+  {bp P \<and> (\<forall>Q. bp Q \<longrightarrow> card P \<le> 3 / 2 * card Q)}"
+proof (vcg, goal_cases)
+case (1 P P\<^sub>1 P\<^sub>2 B\<^sub>1 B\<^sub>2 V u)
+  then show ?case by (simp add: loop_init)
+next
+  case (2 P P\<^sub>1 P\<^sub>2 B\<^sub>1 B\<^sub>2 V u)
+  then have INV: "inv\<^sub>3 P\<^sub>1 P\<^sub>2 B\<^sub>1 B\<^sub>2 V" ..
+  let ?s = "SOME u. u \<in> V \<inter> S"
+  let ?l = "SOME u. u \<in> V \<inter> L"
+  have LIN: "V \<inter> L \<noteq> {} \<Longrightarrow> ?l \<in> V \<inter> L" using some_in_eq by metis
+  then have LWEIGHT: "V \<inter> L \<noteq> {} \<Longrightarrow> w ?l \<le> c" using L_def weight by blast
+  from 2 have "V \<inter> S \<noteq> {}" ..
+  then have IN: "?s \<in> V \<inter> S" using some_in_eq by metis
+  then have "w ?s \<le> 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 \<open>B\<^sub>1 = {}\<close>, cases \<open>V \<inter> L = {}\<close>) auto
+next
+  case (3 P P\<^sub>1 P\<^sub>2 B\<^sub>1 B\<^sub>2 V u)
+  then have INV: "inv\<^sub>3 P\<^sub>1 P\<^sub>2 B\<^sub>1 B\<^sub>2 V" and EMPTY: "V \<inter> S = {}" by blast+
+  from inv\<^sub>1E(1)[OF inv\<^sub>2E(1)[OF inv\<^sub>3E(1)[OF INV]]] and bin_packing_lower_bound_card[OF EMPTY inv\<^sub>3E(1)[OF INV]]
+    show ?case by blast
+qed
+
+end (* BinPacking *)
+
+subsection \<open>The Full Linear Time Version of the Proposed Algorithm\<close>
+
+text \<open>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 \<open>insertion, removal, and selection of an element, the union of two sets,
+      and the emptiness test in constant time\<close> @{cite BerghammerR03}.\<close>
+
+locale BinPacking_Complete =
+  fixes U :: "'a set" \<comment> \<open>A finite, non-empty set of objects\<close>
+    and w :: "'a \<Rightarrow> real" \<comment> \<open>A mapping from objects to their respective weights (positive real numbers)\<close>
+    and c :: nat \<comment> \<open>The maximum capacity of a bin (as a natural number)\<close>
+  assumes weight: "\<forall>u \<in> U. 0 < w(u) \<and> w(u) \<le> c"
+      and U_Finite: "finite U"
+      and U_NE: "U \<noteq> {}"
+begin
+
+text \<open>The correctness proofs will be identical to the ones of the simplified algorithm.\<close>
+
+abbreviation W :: "'a set \<Rightarrow> real" where
+  "W B \<equiv> (\<Sum>u \<in> B. w(u))"
+
+definition bp :: "'a set set \<Rightarrow> bool" where
+  "bp P \<longleftrightarrow> partition_on U P \<and> (\<forall>B \<in> P. W(B) \<le> c)"
+
+lemma bpE:
+  assumes "bp P"
+  shows "pairwise disjnt P" "{} \<notin> P" "\<Union>P = U" "\<forall>B \<in> P. W(B) \<le> c"
+  using assms unfolding bp_def partition_on_def by blast+
+
+lemma bpI:
+  assumes "pairwise disjnt P" "{} \<notin> P" "\<Union>P = U" "\<forall>B \<in> P. W(B) \<le> c"
+  shows "bp P"
+  using assms unfolding bp_def partition_on_def by blast
+
+definition inv\<^sub>1 :: "'a set set \<Rightarrow> 'a set set \<Rightarrow> 'a set \<Rightarrow> 'a set \<Rightarrow> 'a set \<Rightarrow> bool" where
+  "inv\<^sub>1 P\<^sub>1 P\<^sub>2 B\<^sub>1 B\<^sub>2 V \<longleftrightarrow> bp (P\<^sub>1 \<union> wrap B\<^sub>1 \<union> P\<^sub>2 \<union> wrap B\<^sub>2 \<union> {{v} |v. v \<in> V}) \<comment> \<open>A correct solution to the bin packing problem\<close>
+                       \<and> \<Union>(P\<^sub>1 \<union> wrap B\<^sub>1 \<union> P\<^sub>2 \<union> wrap B\<^sub>2) = U - V \<comment> \<open>The partial solution does not contain objects that have not yet been assigned\<close>
+                       \<and> B\<^sub>1 \<notin> (P\<^sub>1 \<union> P\<^sub>2 \<union> wrap B\<^sub>2) \<comment> \<open>\<open>B\<^sub>1\<close> is distinct from all the other bins\<close>
+                       \<and> B\<^sub>2 \<notin> (P\<^sub>1 \<union> wrap B\<^sub>1 \<union> P\<^sub>2) \<comment> \<open>\<open>B\<^sub>2\<close> is distinct from all the other bins\<close>
+                       \<and> (P\<^sub>1 \<union> wrap B\<^sub>1) \<inter> (P\<^sub>2 \<union> wrap B\<^sub>2) = {} \<comment> \<open>The first and second partial solutions are disjoint from each other.\<close>"
+
+lemma inv\<^sub>1E:
+  assumes "inv\<^sub>1 P\<^sub>1 P\<^sub>2 B\<^sub>1 B\<^sub>2 V"
+  shows "bp (P\<^sub>1 \<union> wrap B\<^sub>1 \<union> P\<^sub>2 \<union> wrap B\<^sub>2 \<union> {{v} |v. v \<in> V})"
+    and "\<Union>(P\<^sub>1 \<union> wrap B\<^sub>1 \<union> P\<^sub>2 \<union> wrap B\<^sub>2) = U - V"
+    and "B\<^sub>1 \<notin> (P\<^sub>1 \<union> P\<^sub>2 \<union> wrap B\<^sub>2)"
+    and "B\<^sub>2 \<notin> (P\<^sub>1 \<union> wrap B\<^sub>1 \<union> P\<^sub>2)"
+    and "(P\<^sub>1 \<union> wrap B\<^sub>1) \<inter> (P\<^sub>2 \<union> wrap B\<^sub>2) = {}"
+  using assms unfolding inv\<^sub>1_def by auto
+
+lemma inv\<^sub>1I:
+  assumes "bp (P\<^sub>1 \<union> wrap B\<^sub>1 \<union> P\<^sub>2 \<union> wrap B\<^sub>2 \<union> {{v} |v. v \<in> V})"
+    and "\<Union>(P\<^sub>1 \<union> wrap B\<^sub>1 \<union> P\<^sub>2 \<union> wrap B\<^sub>2) = U - V"
+    and "B\<^sub>1 \<notin> (P\<^sub>1 \<union> P\<^sub>2 \<union> wrap B\<^sub>2)"
+    and "B\<^sub>2 \<notin> (P\<^sub>1 \<union> wrap B\<^sub>1 \<union> P\<^sub>2)"
+    and "(P\<^sub>1 \<union> wrap B\<^sub>1) \<inter> (P\<^sub>2 \<union> wrap B\<^sub>2) = {}"
+  shows "inv\<^sub>1 P\<^sub>1 P\<^sub>2 B\<^sub>1 B\<^sub>2 V"
+  using assms unfolding inv\<^sub>1_def by blast
+
+lemma wrap_Un [simp]: "wrap (M \<union> {x}) = {M \<union> {x}}" unfolding wrap_def by simp
+lemma wrap_empty [simp]: "wrap {} = {}" unfolding wrap_def by simp
+lemma wrap_not_empty [simp]: "M \<noteq> {} \<longleftrightarrow> wrap M = {M}" unfolding wrap_def by simp
+
+lemma inv\<^sub>1_stepA:
+  assumes "inv\<^sub>1 P\<^sub>1 P\<^sub>2 B\<^sub>1 B\<^sub>2 V" "u \<in> V" "W(B\<^sub>1) + w(u) \<le> c"
+  shows "inv\<^sub>1 P\<^sub>1 P\<^sub>2 (B\<^sub>1 \<union> {u}) B\<^sub>2 (V - {u})"
+proof -
+  note invrules = inv\<^sub>1E[OF assms(1)] and bprules = bpE[OF invrules(1)]
+
+  \<comment> \<open>Rule 1: Pairwise Disjoint\<close>
+  have NOTIN: "\<forall>M \<in> P\<^sub>1 \<union> wrap B\<^sub>1 \<union> P\<^sub>2 \<union> wrap B\<^sub>2 \<union> {{v} |v. v \<in> V - {u}}. u \<notin> M"
+    using invrules(2) assms(2) by blast
+  have "{{v} |v. v \<in> V} = {{u}} \<union> {{v} |v. v \<in> V - {u}}"
+    using assms(2) by blast
+  then have "pairwise disjnt (P\<^sub>1 \<union> wrap B\<^sub>1 \<union> P\<^sub>2 \<union> wrap B\<^sub>2 \<union> ({{u}} \<union> {{v} |v. v \<in> V - {u}}))"
+    using bprules(1) assms(2) by simp
+  then have "pairwise disjnt (wrap B\<^sub>1 \<union> {{u}} \<union> P\<^sub>1 \<union> P\<^sub>2 \<union> wrap B\<^sub>2 \<union> {{v} |v. v \<in> V - {u}})" by (simp add: Un_commute)
+  then have assm: "pairwise disjnt (wrap B\<^sub>1 \<union> {{u}} \<union> (P\<^sub>1 \<union> P\<^sub>2 \<union> wrap B\<^sub>2 \<union> {{v} |v. v \<in> V - {u}}))" by (simp add: Un_assoc)
+  have "pairwise disjnt ({B\<^sub>1 \<union> {u}} \<union> (P\<^sub>1 \<union> P\<^sub>2 \<union> wrap B\<^sub>2 \<union> {{v} |v. v \<in> V - {u}}))"
+  proof (cases \<open>B\<^sub>1 = {}\<close>)
+    case True with assm show ?thesis by simp
+  next
+    case False
+    with assm have assm: "pairwise disjnt ({B\<^sub>1} \<union> {{u}} \<union> (P\<^sub>1 \<union> P\<^sub>2 \<union> wrap B\<^sub>2 \<union> {{v} |v. v \<in> V - {u}}))" by simp
+    from NOTIN have "{u} \<notin> P\<^sub>1 \<union> P\<^sub>2 \<union> wrap B\<^sub>2 \<union> {{v} |v. v \<in> 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 (P\<^sub>1 \<union> wrap (B\<^sub>1 \<union> {u}) \<union> P\<^sub>2 \<union> wrap B\<^sub>2 \<union> {{v} |v. v \<in> V - {u}})"
+    unfolding wrap_Un by simp
+
+  \<comment> \<open>Rule 2: No empty sets\<close>
+  from bprules(2) have 2: "{} \<notin> P\<^sub>1 \<union> wrap (B\<^sub>1 \<union> {u}) \<union> P\<^sub>2 \<union> wrap B\<^sub>2 \<union> {{v} |v. v \<in> V - {u}}"
+    unfolding wrap_def by simp
+
+  \<comment> \<open>Rule 3: Union preserved\<close>
+  from bprules(3) have "\<Union> (P\<^sub>1 \<union> wrap B\<^sub>1 \<union> P\<^sub>2 \<union> wrap B\<^sub>2 \<union> {{u}} \<union> {{v} |v. v \<in> V - {u}}) = U"
+    using assms(2) by blast
+  then have 3: "\<Union> (P\<^sub>1 \<union> wrap (B\<^sub>1 \<union> {u}) \<union> P\<^sub>2 \<union> wrap B\<^sub>2 \<union> {{v} |v. v \<in> V - {u}}) = U"
+    unfolding wrap_def by force
+
+  \<comment> \<open>Rule 4: Weights below capacity\<close>
+  have "0 < w u" using weight assms(2) bprules(3) by blast
+  have "finite B\<^sub>1" using bprules(3) U_Finite by (cases \<open>B\<^sub>1 = {}\<close>) auto
+  then have "W (B\<^sub>1 \<union> {u}) \<le> W B\<^sub>1 + w u" using \<open>0 < w u\<close> by (cases \<open>u \<in> B\<^sub>1\<close>) (auto simp: insert_absorb)
+  also have "... \<le> c" using assms(3) .
+  finally have "W (B\<^sub>1 \<union> {u}) \<le> c" .
+  then have "\<forall>B \<in> wrap (B\<^sub>1 \<union> {u}). W B \<le> c" unfolding wrap_Un by blast
+  moreover have "\<forall>B\<in>P\<^sub>1 \<union> P\<^sub>2 \<union> wrap B\<^sub>2 \<union> {{v} |v. v \<in> V - {u}}. W B \<le> c"
+    using bprules(4) by blast
+  ultimately have 4: "\<forall>B\<in>P\<^sub>1 \<union> wrap (B\<^sub>1 \<union> {u}) \<union> P\<^sub>2 \<union> wrap B\<^sub>2 \<union> {{v} |v. v \<in> V - {u}}. W B \<le> c" by blast
+  from bpI[OF 1 2 3 4] have 1: "bp (P\<^sub>1 \<union> wrap (B\<^sub>1 \<union> {u}) \<union> P\<^sub>2 \<union> wrap B\<^sub>2 \<union> {{v} |v. v \<in> V - {u}})" .
+
+  \<comment> \<open>Auxiliary information is preserved\<close>
+  have "u \<in> U" using assms(2) bprules(3) by blast
+  then have R: "U - (V - {u}) = U - V \<union> {u}" by blast
+  have L: "\<Union> (P\<^sub>1 \<union> wrap (B\<^sub>1 \<union> {u}) \<union> P\<^sub>2 \<union> wrap B\<^sub>2) = \<Union> (P\<^sub>1 \<union> wrap B\<^sub>1 \<union> P\<^sub>2 \<union> wrap B\<^sub>2) \<union> {u}"
+    unfolding wrap_def using NOTIN by auto
+  have 2: "\<Union> (P\<^sub>1 \<union> wrap (B\<^sub>1 \<union> {u}) \<union> P\<^sub>2 \<union> wrap B\<^sub>2) = U - (V - {u})"
+    unfolding L R invrules(2) ..
+  have 3: "B\<^sub>1 \<union> {u} \<notin> P\<^sub>1 \<union> P\<^sub>2 \<union> wrap B\<^sub>2"
+    using NOTIN by auto
+  have 4: "B\<^sub>2 \<notin> P\<^sub>1 \<union> wrap (B\<^sub>1 \<union> {u}) \<union> P\<^sub>2"
+    using invrules(4) NOTIN unfolding wrap_def by fastforce
+  have 5: "(P\<^sub>1 \<union> wrap (B\<^sub>1 \<union> {u})) \<inter> (P\<^sub>2 \<union> wrap B\<^sub>2) = {}"
+    using invrules(5) NOTIN unfolding wrap_Un by auto
+
+  from inv\<^sub>1I[OF 1 2 3 4 5] show ?thesis .
+qed
+
+lemma inv\<^sub>1_stepB:
+  assumes "inv\<^sub>1 P\<^sub>1 P\<^sub>2 B\<^sub>1 B\<^sub>2 V" "u \<in> V" "W B\<^sub>2 + w u \<le> c"
+  shows "inv\<^sub>1 (P\<^sub>1 \<union> wrap B\<^sub>1) P\<^sub>2 {} (B\<^sub>2 \<union> {u}) (V - {u})"
+proof -
+  note invrules = inv\<^sub>1E[OF assms(1)] and bprules = bpE[OF invrules(1)]
+
+  have NOTIN: "\<forall>M \<in> P\<^sub>1 \<union> wrap B\<^sub>1 \<union> P\<^sub>2 \<union> wrap B\<^sub>2 \<union> {{v} |v. v \<in> V - {u}}. u \<notin> M"
+    using invrules(2) assms(2) by blast
+  have "{{v} |v. v \<in> V} = {{u}} \<union> {{v} |v. v \<in> V - {u}}"
+    using assms(2) by blast
+  then have "pairwise disjnt (P\<^sub>1 \<union> wrap B\<^sub>1 \<union> P\<^sub>2 \<union> wrap B\<^sub>2 \<union> {{u}} \<union> {{v} |v. v \<in> V - {u}})"
+    using bprules(1) assms(2) by simp
+  then have assm: "pairwise disjnt (wrap B\<^sub>2 \<union> {{u}} \<union> (P\<^sub>1 \<union> wrap B\<^sub>1 \<union> P\<^sub>2 \<union> {{v} |v. v \<in> V - {u}}))"
+    by (simp add: Un_assoc Un_commute)
+  have "pairwise disjnt ({B\<^sub>2 \<union> {u}} \<union> (P\<^sub>1 \<union> wrap B\<^sub>1 \<union> P\<^sub>2 \<union> {{v} |v. v \<in> V - {u}}))"
+  proof (cases \<open>B\<^sub>2 = {}\<close>)
+    case True with assm show ?thesis by simp
+  next
+    case False
+    with assm have assm: "pairwise disjnt ({B\<^sub>2} \<union> {{u}} \<union> (P\<^sub>1 \<union> wrap B\<^sub>1 \<union> P\<^sub>2 \<union> {{v} |v. v \<in> V - {u}}))" by simp
+    from NOTIN have "{u} \<notin> P\<^sub>1 \<union> wrap B\<^sub>1 \<union> P\<^sub>2 \<union> {{v} |v. v \<in> 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 (P\<^sub>1 \<union> wrap B\<^sub>1 \<union> wrap {} \<union> P\<^sub>2 \<union> wrap (B\<^sub>2 \<union> {u}) \<union> {{v} |v. v \<in> V - {u}})"
+    unfolding wrap_Un by simp
+
+  \<comment> \<open>Rule 2: No empty sets\<close>
+  from bprules(2) have 2: "{} \<notin> P\<^sub>1 \<union> wrap B\<^sub>1 \<union> wrap {} \<union> P\<^sub>2 \<union> wrap (B\<^sub>2 \<union> {u}) \<union> {{v} |v. v \<in> V - {u}}"
+    unfolding wrap_def by simp
+
+  \<comment> \<open>Rule 3: Union preserved\<close>
+  from bprules(3) have "\<Union> (P\<^sub>1 \<union> wrap B\<^sub>1 \<union> P\<^sub>2 \<union> wrap B\<^sub>2 \<union> {{u}} \<union> {{v} |v. v \<in> V - {u}}) = U"
+    using assms(2) by blast
+  then have 3: "\<Union> (P\<^sub>1 \<union> wrap B\<^sub>1 \<union> wrap {} \<union> P\<^sub>2 \<union> wrap (B\<^sub>2 \<union> {u}) \<union> {{v} |v. v \<in> V - {u}}) = U"
+    unfolding wrap_def by force
+
+  \<comment> \<open>Rule 4: Weights below capacity\<close>
+  have "0 < w u" using weight assms(2) bprules(3) by blast
+  have "finite B\<^sub>2" using bprules(3) U_Finite by (cases \<open>B\<^sub>2 = {}\<close>) auto
+  then have "W (B\<^sub>2 \<union> {u}) \<le> W B\<^sub>2 + w u" using \<open>0 < w u\<close> by (cases \<open>u \<in> B\<^sub>2\<close>) (auto simp: insert_absorb)
+  also have "... \<le> c" using assms(3) .
+  finally have "W (B\<^sub>2 \<union> {u}) \<le> c" .
+  then have "\<forall>B \<in> wrap (B\<^sub>2 \<union> {u}). W B \<le> c" unfolding wrap_Un by blast
+  moreover have "\<forall>B\<in>P\<^sub>1 \<union> wrap B\<^sub>1 \<union> P\<^sub>2 \<union> {{v} |v. v \<in> V - {u}}. W B \<le> c"
+    using bprules(4) by blast
+  ultimately have 4: "\<forall>B\<in>P\<^sub>1 \<union> wrap B\<^sub>1 \<union> wrap {} \<union> P\<^sub>2 \<union> wrap (B\<^sub>2 \<union> {u}) \<union> {{v} |v. v \<in> V - {u}}. W B \<le> c"
+    by auto
+  from bpI[OF 1 2 3 4] have 1: "bp (P\<^sub>1 \<union> wrap B\<^sub>1 \<union> wrap {} \<union> P\<^sub>2 \<union> wrap (B\<^sub>2 \<union> {u}) \<union> {{v} |v. v \<in> V - {u}})" .
+
+  \<comment> \<open>Auxiliary information is preserved\<close>
+  have "u \<in> U" using assms(2) bprules(3) by blast
+  then have R: "U - (V - {u}) = U - V \<union> {u}" by blast
+  have L: "\<Union> (P\<^sub>1 \<union> wrap B\<^sub>1 \<union> wrap {} \<union> P\<^sub>2 \<union> wrap (B\<^sub>2 \<union> {u})) = \<Union> (P\<^sub>1 \<union> wrap B\<^sub>1 \<union> wrap {} \<union> P\<^sub>2 \<union> wrap B\<^sub>2) \<union> {u}"
+    unfolding wrap_def using NOTIN by auto
+  have 2: "\<Union> (P\<^sub>1 \<union> wrap B\<^sub>1 \<union> wrap {} \<union> P\<^sub>2 \<union> wrap (B\<^sub>2 \<union> {u})) = U - (V - {u})"
+    unfolding L R using invrules(2) by simp
+  have 3: "{} \<notin> P\<^sub>1 \<union> wrap B\<^sub>1 \<union> P\<^sub>2 \<union> wrap (B\<^sub>2 \<union> {u})"
+    using bpE(2)[OF 1] by simp
+  have 4: "B\<^sub>2 \<union> {u} \<notin> P\<^sub>1 \<union> wrap B\<^sub>1 \<union> wrap {} \<union> P\<^sub>2"
+    using NOTIN by auto
+  have 5: "(P\<^sub>1 \<union> wrap B\<^sub>1 \<union> wrap {}) \<inter> (P\<^sub>2 \<union> wrap (B\<^sub>2 \<union> {u})) = {}"
+    using invrules(5) NOTIN unfolding wrap_empty wrap_Un by auto
+
+  from inv\<^sub>1I[OF 1 2 3 4 5] show ?thesis .
+qed
+
+lemma inv\<^sub>1_stepC:
+  assumes "inv\<^sub>1 P\<^sub>1 P\<^sub>2 B\<^sub>1 B\<^sub>2 V" "u \<in> V"
+  shows "inv\<^sub>1 (P\<^sub>1 \<union> wrap B\<^sub>1) (P\<^sub>2 \<union> wrap B\<^sub>2) {} {u} (V - {u})"
+proof -
+  note invrules = inv\<^sub>1E[OF assms(1)]
+  \<comment> \<open>Rule 1-4: Correct Bin Packing\<close>
+  have "P\<^sub>1 \<union> wrap B\<^sub>1 \<union> wrap {} \<union> (P\<^sub>2 \<union> wrap B\<^sub>2) \<union> wrap {u} \<union> {{v} |v. v \<in> V - {u}}
+      = P\<^sub>1 \<union> wrap B\<^sub>1 \<union> P\<^sub>2 \<union> wrap B\<^sub>2 \<union> {{u}} \<union> {{v} |v. v \<in> V - {u}}"
+    by (metis (no_types, lifting) Un_assoc Un_empty_right insert_not_empty wrap_empty wrap_not_empty)
+  also have "... = P\<^sub>1 \<union> wrap B\<^sub>1 \<union> P\<^sub>2 \<union> wrap B\<^sub>2 \<union> {{v} |v. v \<in> V}"
+    using assms(2) by auto
+  finally have EQ: "P\<^sub>1 \<union> wrap B\<^sub>1 \<union> wrap {} \<union> (P\<^sub>2 \<union> wrap B\<^sub>2) \<union> wrap {u} \<union> {{v} |v. v \<in> V - {u}}
+                  = P\<^sub>1 \<union> wrap B\<^sub>1 \<union> P\<^sub>2 \<union> wrap B\<^sub>2 \<union> {{v} |v. v \<in> V}" .
+  from invrules(1) have 1: "bp (P\<^sub>1 \<union> wrap B\<^sub>1 \<union> wrap {} \<union> (P\<^sub>2 \<union> wrap B\<^sub>2) \<union> wrap {u} \<union> {{v} |v. v \<in> V - {u}})"
+    unfolding EQ .
+
+  \<comment> \<open>Auxiliary information is preserved\<close>
+  have NOTIN: "\<forall>M \<in> P\<^sub>1 \<union> wrap B\<^sub>1 \<union> P\<^sub>2 \<union> wrap B\<^sub>2 \<union> {{v} |v. v \<in> V - {u}}. u \<notin> M"
+    using invrules(2) assms(2) by blast
+  have "u \<in> U" using assms(2) bpE(3)[OF invrules(1)] by blast
+  then have R: "U - (V - {u}) = U - V \<union> {u}" by blast
+  have L: "\<Union> (P\<^sub>1 \<union> wrap B\<^sub>1 \<union> wrap {} \<union> (P\<^sub>2 \<union> wrap B\<^sub>2) \<union> wrap {u}) = \<Union> (P\<^sub>1 \<union> wrap B\<^sub>1 \<union> wrap {} \<union> (P\<^sub>2 \<union> wrap B\<^sub>2)) \<union> {u}"
+    unfolding wrap_def using NOTIN by auto
+  have 2: "\<Union> (P\<^sub>1 \<union> wrap B\<^sub>1 \<union> wrap {} \<union> (P\<^sub>2 \<union> wrap B\<^sub>2) \<union> wrap {u}) = U - (V - {u})"
+    unfolding L R using invrules(2) by auto
+  have 3: "{} \<notin> P\<^sub>1 \<union> wrap B\<^sub>1 \<union> (P\<^sub>2 \<union> wrap B\<^sub>2) \<union> wrap {u}"
+    using bpE(2)[OF 1] by simp
+  have 4: "{u} \<notin> P\<^sub>1 \<union> wrap B\<^sub>1 \<union> wrap {} \<union> (P\<^sub>2 \<union> wrap B\<^sub>2)"
+    using NOTIN by auto
+  have 5: "(P\<^sub>1 \<union> wrap B\<^sub>1 \<union> wrap {}) \<inter> (P\<^sub>2 \<union> wrap B\<^sub>2 \<union> wrap {u}) = {}"
+    using invrules(5) NOTIN unfolding wrap_def by force
+
+  from inv\<^sub>1I[OF 1 2 3 4 5] show ?thesis .
+qed
+
+text \<open>From this point onward, we will require a different approach for proving lower bounds.
+      Instead of fixing and assuming the definitions of the \<open>S\<close> and \<open>L\<close> sets, we will introduce
+      the abbreviations \<open>S\<^sub>U\<close> and \<open>L\<^sub>U\<close> for any occurrences of the original \<open>S\<close> and \<open>L\<close> sets.
+      The union of \<open>S\<close> and \<open>L\<close> can be interpreted as \<open>V\<close>. As a result, occurrences of \<open>V \<inter> S\<close>
+      become \<open>(S \<union> L) \<inter> S = S\<close>, and \<open>V \<inter> L\<close> become \<open>(S \<union> L) \<inter> L = L\<close>.
+      Occurrences of these sets will have to be replaced appropriately.\<close>
+abbreviation S\<^sub>U where
+  "S\<^sub>U \<equiv> {u \<in> U. w u \<le> c / 2}"
+
+abbreviation L\<^sub>U where
+  "L\<^sub>U \<equiv> {u \<in> U. c / 2 < w u}"
+
+text \<open>As we will remove elements from \<open>S\<close> and \<open>L\<close>, we will only be able to show that they remain
+      subsets of \<open>S\<^sub>U\<close> and \<open>L\<^sub>U\<close> respectively.\<close>
+abbreviation SL where
+  "SL S L \<equiv> S \<subseteq> S\<^sub>U \<and> L \<subseteq> L\<^sub>U"
+
+lemma bp_bins_finite [simp]:
+  assumes "bp P"
+  shows "\<forall>B \<in> 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 \<in> P"
+  shows "\<forall>x \<in> B. \<forall>y \<in> B. x \<noteq> y \<longrightarrow> x \<notin> L\<^sub>U \<or> y \<notin> L\<^sub>U"
+proof (rule ccontr, simp)
+  assume "\<exists>x\<in>B. \<exists>y\<in>B. x \<noteq> y \<and> y \<in> U \<and> x \<in> U \<and> real c < w x * 2 \<and> real c < w y * 2"
+  then obtain x y where *: "x \<in> B" "y \<in> B" "x \<noteq> y" "x \<in> L\<^sub>U" "y \<in> L\<^sub>U" by auto
+  then have "c < w x + w y" by force
+  have "finite B" using assms by simp
+  have "y \<in> B - {x}" using *(2,3) by blast
+  have "W B = W (B - {x}) + w x"
+    using *(1) \<open>finite B\<close> by (simp add: sum.remove)
+  also have "... = W (B - {x} - {y}) + w x + w y"
+    using \<open>y \<in> B - {x}\<close> \<open>finite B\<close> by (simp add: sum.remove)
+  finally have *: "W B = W (B - {x} - {y}) + w x + w y" .
+  have "\<forall>u \<in> B. 0 < w u" using bpE(3)[OF assms(1)] assms(2) weight by blast
+  then have "0 \<le> W (B - {x} - {y})" by (smt DiffD1 sum_nonneg)
+  with * have "c < W B" using \<open>c < w x + w y\<close> 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 L\<^sub>U \<le> card P"
+proof -
+  have "\<forall>x \<in> L\<^sub>U. \<exists>B \<in> P. x \<in> B"
+    using bpE(3)[OF assms] by blast
+  then obtain f where f_def: "\<forall>u \<in> L\<^sub>U. u \<in> f u \<and> f u \<in> P" by metis
+  then have "inj_on f L\<^sub>U"
+    unfolding inj_on_def using only_one_L_per_bin[OF assms] by blast
+  then have card_eq: "card L\<^sub>U = card (f ` L\<^sub>U)" by (simp add: card_image)
+  have "f ` L\<^sub>U \<subseteq> P" using f_def by blast
+  moreover have "finite P" using assms by simp
+  ultimately have "card (f ` L\<^sub>U) \<le> card P" by (simp add: card_mono)
+  then show ?thesis unfolding card_eq .
+qed
+
+lemma subset_bp_card:
+  assumes "bp P" "M \<subseteq> P" "\<forall>B \<in> M. B \<inter> L\<^sub>U \<noteq> {}"
+  shows "card M \<le> card L\<^sub>U"
+proof -
+  have "\<forall>B \<in> M. \<exists>u \<in> L\<^sub>U. u \<in> B" using assms(3) by fast
+  then have "\<exists>f. \<forall>B \<in> M. f B \<in> L\<^sub>U \<and> f B \<in> B" by metis
+  then obtain f where f_def: "\<forall>B \<in> M. f B \<in> L\<^sub>U \<and> f B \<in> B" ..
+  have "inj_on f M"
+  proof (rule ccontr)
+    assume "\<not> inj_on f M"
+    then have "\<exists>x \<in> M. \<exists>y \<in> M. x \<noteq> y \<and> f x = f y" unfolding inj_on_def by blast
+    then obtain x y where *: "x \<in> M" "y \<in> M" "x \<noteq> y" "f x = f y" by blast
+    then have "\<exists>u. u \<in> x \<and> u \<in> y" using f_def by metis
+    then have "x \<inter> y \<noteq> {}" 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\<^sub>U" using U_Finite by auto
+  moreover have "f ` M \<subseteq> L\<^sub>U" 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" "inv\<^sub>1 P\<^sub>1 P\<^sub>2 B\<^sub>1 B\<^sub>2 (S \<union> L)" "\<forall>B \<in> P\<^sub>1 \<union> wrap B\<^sub>1. B \<inter> L\<^sub>U \<noteq> {}"
+      and SL_def: "SL S L"
+  shows "card (P\<^sub>1 \<union> wrap B\<^sub>1 \<union> {{v} |v. v \<in> L}) \<le> card P"
+proof -
+  note invrules = inv\<^sub>1E[OF assms(2)]
+  have "\<forall>B \<in> {{v} |v. v \<in> L}. B \<inter> L\<^sub>U \<noteq> {}" using SL_def by blast
+  with assms(3) have
+    "P\<^sub>1 \<union> wrap B\<^sub>1 \<union> {{v} |v. v \<in> L} \<subseteq> P\<^sub>1 \<union> wrap B\<^sub>1 \<union> P\<^sub>2 \<union> wrap B\<^sub>2 \<union> {{v} |v. v \<in> S \<union> L}"
+    "\<forall>B \<in> P\<^sub>1 \<union> wrap B\<^sub>1 \<union> {{v} |v. v \<in> L}. B \<inter> L\<^sub>U \<noteq> {}" 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 "(\<Sum>u \<in> U. w u) = (\<Sum>B \<in> P. W B)"
+proof -
+  have FINITE: "\<forall>B \<in> P. finite B" using assms by simp
+  have DISJNT: "\<forall>A \<in> P. \<forall>B \<in> P. A \<noteq> B \<longrightarrow> A \<inter> B = {}"
+    using bpE(1)[OF assms] unfolding pairwise_def disjnt_def .
+  have "(\<Sum>u \<in> (\<Union>P). w u) = (\<Sum>B \<in> 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 "(\<Sum>u \<in> U. w u) \<le> c * card P"
+proof -
+  have *: "\<forall>B \<in> P. 0 < W B \<and> W B \<le> c"
+    using bpE(2-4)[OF assms] weight by (metis UnionI assms bp_bins_finite sum_pos)
+  have "(\<Sum>u \<in> U. w u) = (\<Sum>B \<in> P. W B)"
+    using sum_Un_eq_sum_sum[OF assms] .
+  also have "... \<le> (\<Sum>B \<in> 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 \<noteq> {}"
+  using U_NE bpE(3)[OF assms] by blast
+
+lemma sum_Un_ge:
+  fixes f :: "_ \<Rightarrow> real"
+  assumes "finite M" "finite N" "\<forall>B \<in> M \<union> N. 0 < f B"
+  shows "sum f M \<le> sum f (M \<union> N)"
+proof -
+  have "0 \<le> sum f N - sum f (M \<inter> N)"
+    using assms by (smt DiffD1 inf.cobounded2 UnCI sum_mono2)
+  then have "sum f M \<le> sum f M + sum f N - sum f (M \<inter> N)"
+    by simp
+  also have "... = sum f (M \<union> N)"
+    using sum_Un[OF assms(1,2), symmetric] .
+  finally show ?thesis .
+qed
+
+definition bij_exists :: "'a set set \<Rightarrow> 'a set \<Rightarrow> bool" where
+  "bij_exists P V = (\<exists>f. bij_betw f P V \<and> (\<forall>B \<in> P. W B + w (f B) > c))"
+
+lemma P\<^sub>1_lower_bound_card:
+  assumes "bp P" "inv\<^sub>1 P\<^sub>1 P\<^sub>2 B\<^sub>1 B\<^sub>2 (S \<union> L)" "bij_exists P\<^sub>1 (\<Union>(P\<^sub>2 \<union> wrap B\<^sub>2))"
+  shows "card P\<^sub>1 + 1 \<le> card P"
+proof (cases \<open>P\<^sub>1 = {}\<close>)
+  case True
+  have "finite P" using assms(1) by simp
+  then have "1 \<le> 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 = inv\<^sub>1E[OF assms(2)]
+  case False
+  obtain f where f_def: "bij_betw f P\<^sub>1 (\<Union>(P\<^sub>2 \<union> wrap B\<^sub>2))" "\<forall>B \<in> P\<^sub>1. W B + w (f B) > c"
+    using assms(3) unfolding bij_exists_def by blast
+  have FINITE: "finite P\<^sub>1" "finite (P\<^sub>2 \<union> wrap B\<^sub>2)" "finite (P\<^sub>1 \<union> P\<^sub>2 \<union> wrap B\<^sub>2)" "finite (wrap B\<^sub>1 \<union> {{v} |v. v \<in> S \<union> L})"
+    using inv\<^sub>1E(1)[OF assms(2)] bp_sol_finite by blast+
+
+  have F: "\<forall>B \<in> P\<^sub>2 \<union> wrap B\<^sub>2. finite B" using invrules(1) by simp
+  have D: "\<forall>A \<in> P\<^sub>2 \<union> wrap B\<^sub>2. \<forall>B \<in> P\<^sub>2 \<union> wrap B\<^sub>2. A \<noteq> B \<longrightarrow> A \<inter> B = {}"
+    using bpE(1)[OF invrules(1)] unfolding pairwise_def disjnt_def by auto
+  have sum_eq: "W (\<Union> (P\<^sub>2 \<union> wrap B\<^sub>2)) = (\<Sum>B \<in> P\<^sub>2 \<union> wrap B\<^sub>2. W B)"
+    using sum.Union_disjoint[OF F D] by auto
+
+  have "\<forall>B\<in>P\<^sub>1 \<union> wrap B\<^sub>1 \<union> P\<^sub>2 \<union> wrap B\<^sub>2 \<union> {{v} |v. v \<in> S \<union> 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 "(\<Sum>B \<in> P\<^sub>1 \<union> P\<^sub>2 \<union> wrap B\<^sub>2. W B) \<le> (\<Sum>B \<in> P\<^sub>1 \<union> P\<^sub>2 \<union> wrap B\<^sub>2 \<union> (wrap B\<^sub>1 \<union> {{v} |v. v \<in> S \<union> L}). W B)"
+    using sum_Un_ge[OF FINITE(3,4), of W] by blast
+  also have "... = (\<Sum>B \<in> P\<^sub>1 \<union> wrap B\<^sub>1 \<union> P\<^sub>2 \<union> wrap B\<^sub>2 \<union> {{v} |v. v \<in> S \<union> L}. W B)" by (smt Un_assoc Un_commute) 
+  also have "... = W U" using sum_Un_eq_sum_sum[OF invrules(1), symmetric] .
+  finally have *: "(\<Sum>B \<in> P\<^sub>1 \<union> P\<^sub>2 \<union> wrap B\<^sub>2. W B) \<le> W U" .
+  have DISJNT: "P\<^sub>1 \<inter> (P\<^sub>2 \<union> wrap B\<^sub>2) = {}" using invrules(5) by blast
+
+  \<comment> \<open>This part of the proof is based on the proof on page 72 of the article @{cite BerghammerR03}.\<close>
+  have "c * card P\<^sub>1 = (\<Sum>B \<in> P\<^sub>1. c)" by simp
+  also have "... < (\<Sum>B \<in> P\<^sub>1. W B + w (f B))"
+    using f_def(2) sum_strict_mono[OF FINITE(1) False] by fastforce
+  also have "... = (\<Sum>B \<in> P\<^sub>1. W B) + (\<Sum>B \<in> P\<^sub>1. w (f B))"
+    by (simp add: Groups_Big.comm_monoid_add_class.sum.distrib)
+  also have "... = (\<Sum>B \<in> P\<^sub>1. W B) + W (\<Union> (P\<^sub>2 \<union> wrap B\<^sub>2))" unfolding sum.reindex_bij_betw[OF f_def(1), of w] ..
+  also have "... = (\<Sum>B \<in> P\<^sub>1. W B) + (\<Sum>B \<in> P\<^sub>2 \<union> wrap B\<^sub>2. W B)" unfolding sum_eq ..
+  also have "... = (\<Sum>B \<in> P\<^sub>1 \<union> P\<^sub>2 \<union> wrap B\<^sub>2. W B)" using sum.union_disjoint[OF FINITE(1,2) DISJNT, of W] by (simp add: Un_assoc)
+  also have "... \<le> (\<Sum>u \<in> U. w u)" using * .
+  also have "... \<le> 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
+
+lemma P\<^sub>1_B\<^sub>1_lower_bound_card:
+  assumes "bp P" "inv\<^sub>1 P\<^sub>1 P\<^sub>2 B\<^sub>1 B\<^sub>2 (S \<union> L)" "bij_exists P\<^sub>1 (\<Union>(P\<^sub>2 \<union> wrap B\<^sub>2))"
+  shows "card (P\<^sub>1 \<union> wrap B\<^sub>1) \<le> card P"
+proof -
+  have "card (P\<^sub>1 \<union> wrap B\<^sub>1) \<le> card P\<^sub>1 + card (wrap B\<^sub>1)"
+    using card_Un_le by blast
+  also have "... \<le> card P\<^sub>1 + 1" using wrap_card by simp
+  also have "... \<le> card P" using P\<^sub>1_lower_bound_card[OF assms] .
+  finally show ?thesis .
+qed
+
+lemma P\<^sub>2_B\<^sub>2_lower_bound_P\<^sub>1:
+  assumes "inv\<^sub>1 P\<^sub>1 P\<^sub>2 B\<^sub>1 B\<^sub>2 (S \<union> L)" "2 * card P\<^sub>2 \<le> card (\<Union>P\<^sub>2)" "bij_exists P\<^sub>1 (\<Union>(P\<^sub>2 \<union> wrap B\<^sub>2))"
+  shows "2 * card (P\<^sub>2 \<union> wrap B\<^sub>2) \<le> card P\<^sub>1 + 1"
+proof -
+  note invrules = inv\<^sub>1E[OF assms(1)] and bprules = bpE[OF invrules(1)]
+
+  have "pairwise disjnt (P\<^sub>2 \<union> wrap B\<^sub>2)"
+    using bprules(1) pairwise_subset by blast
+  moreover have "B\<^sub>2 \<notin> P\<^sub>2" using invrules(4) by simp
+  ultimately have DISJNT: "\<Union>P\<^sub>2 \<inter> B\<^sub>2 = {}"
+    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 (\<Union>P\<^sub>2)" using U_Finite bprules(3) by auto
+  have "finite B\<^sub>2" using bp_bins_finite[OF invrules(1)] wrap_not_empty by blast
+  have "finite P\<^sub>2" "finite (wrap B\<^sub>2)" using bp_sol_finite[OF invrules(1)] by blast+
+  have DISJNT2: "P\<^sub>2 \<inter> wrap B\<^sub>2 = {}" unfolding wrap_def using \<open>B\<^sub>2 \<notin> P\<^sub>2\<close> by auto
+  have "card (wrap B\<^sub>2) \<le> card B\<^sub>2"
+  proof (cases \<open>B\<^sub>2 = {}\<close>)
+    case False
+    then have "1 \<le> card B\<^sub>2" by (simp add: leI \<open>finite B\<^sub>2\<close>)
+    then show ?thesis using wrap_card[of B\<^sub>2] by linarith
+  qed simp
+
+  \<comment> \<open>This part of the proof is based on the proof on page 73 of the article @{cite BerghammerR03}.\<close>
+  from assms(2) have "2 * card P\<^sub>2 + 2 * card (wrap B\<^sub>2) \<le> card (\<Union>P\<^sub>2) + card (wrap B\<^sub>2) + 1"
+    using wrap_card[of B\<^sub>2] by linarith
+  then have "2 * (card P\<^sub>2 + card (wrap B\<^sub>2)) \<le> card (\<Union>P\<^sub>2) + card B\<^sub>2 + 1"
+    using \<open>card (wrap B\<^sub>2) \<le> card B\<^sub>2\<close> by simp
+  then have "2 * (card (P\<^sub>2 \<union> wrap B\<^sub>2)) \<le> card (\<Union>P\<^sub>2 \<union> B\<^sub>2) + 1"
+    using card_Un_disjoint[OF \<open>finite (\<Union>P\<^sub>2)\<close> \<open>finite B\<^sub>2\<close> DISJNT]
+      and card_Un_disjoint[OF \<open>finite P\<^sub>2\<close> \<open>finite (wrap B\<^sub>2)\<close> DISJNT2] by argo
+  then have "2 * (card (P\<^sub>2 \<union> wrap B\<^sub>2)) \<le> card (\<Union>(P\<^sub>2 \<union> wrap B\<^sub>2)) + 1"
+    by (cases \<open>B\<^sub>2 = {}\<close>) (auto simp: Un_commute)
+  then show "2 * (card (P\<^sub>2 \<union> wrap B\<^sub>2)) \<le> card P\<^sub>1 + 1"
+    using assms(3) bij_betw_same_card unfolding bij_exists_def by metis
+qed
+
+text \<open>We add \<open>SL S L\<close> to \<open>inv\<^sub>2\<close> to ensure that the \<open>S\<close> and \<open>L\<close> sets only contain objects with correct weights.\<close>
+definition inv\<^sub>2 :: "'a set set \<Rightarrow> 'a set set \<Rightarrow> 'a set \<Rightarrow> 'a set \<Rightarrow> 'a set \<Rightarrow> 'a set \<Rightarrow> bool" where
+  "inv\<^sub>2 P\<^sub>1 P\<^sub>2 B\<^sub>1 B\<^sub>2 S L \<longleftrightarrow> inv\<^sub>1 P\<^sub>1 P\<^sub>2 B\<^sub>1 B\<^sub>2 (S \<union> L) \<comment> \<open>\<open>inv\<^sub>1\<close> holds for the partial solution\<close>
+                       \<and> (L \<noteq> {} \<longrightarrow> (\<forall>B \<in> P\<^sub>1 \<union> wrap B\<^sub>1. B \<inter> L\<^sub>U \<noteq> {})) \<comment> \<open>If there are still large objects left, then every bin of the first partial solution must contain a large object\<close>
+                       \<and> bij_exists P\<^sub>1 (\<Union>(P\<^sub>2 \<union> wrap B\<^sub>2)) \<comment> \<open>There exists a bijective function between the bins of the first partial solution and the objects of the second one\<close>
+                       \<and> (2 * card P\<^sub>2 \<le> card (\<Union>P\<^sub>2)) \<comment> \<open>There are at most twice as many bins in \<open>P\<^sub>2\<close> as there are objects in \<open>P\<^sub>2\<close>\<close>
+                       \<and> SL S L \<comment> \<open>\<open>S\<close> and \<open>L\<close> are subsets of \<open>S\<^sub>U\<close> and \<open>L\<^sub>U\<close>\<close>"
+
+lemma inv\<^sub>2E:
+  assumes "inv\<^sub>2 P\<^sub>1 P\<^sub>2 B\<^sub>1 B\<^sub>2 S L"
+  shows "inv\<^sub>1 P\<^sub>1 P\<^sub>2 B\<^sub>1 B\<^sub>2 (S \<union> L)"
+    and "L \<noteq> {} \<Longrightarrow> \<forall>B \<in> P\<^sub>1 \<union> wrap B\<^sub>1. B \<inter> L\<^sub>U \<noteq> {}"
+    and "bij_exists P\<^sub>1 (\<Union>(P\<^sub>2 \<union> wrap B\<^sub>2))"
+    and "2 * card P\<^sub>2 \<le> card (\<Union>P\<^sub>2)"
+    and "SL S L"
+  using assms unfolding inv\<^sub>2_def by blast+
+
+lemma inv\<^sub>2I:
+  assumes "inv\<^sub>1 P\<^sub>1 P\<^sub>2 B\<^sub>1 B\<^sub>2 (S \<union> L)"
+    and "L \<noteq> {} \<Longrightarrow> \<forall>B \<in> P\<^sub>1 \<union> wrap B\<^sub>1. B \<inter> L\<^sub>U \<noteq> {}"
+    and "bij_exists P\<^sub>1 (\<Union>(P\<^sub>2 \<union> wrap B\<^sub>2))"
+    and "2 * card P\<^sub>2 \<le> card (\<Union>P\<^sub>2)"
+    and "SL S L"
+  shows "inv\<^sub>2 P\<^sub>1 P\<^sub>2 B\<^sub>1 B\<^sub>2 S L"
+  using assms unfolding inv\<^sub>2_def by blast
+
+lemma bin_packing_lower_bound_card:
+  assumes "S = {}" "inv\<^sub>2 P\<^sub>1 P\<^sub>2 B\<^sub>1 B\<^sub>2 S L" "bp P"
+  shows "card (P\<^sub>1 \<union> wrap B\<^sub>1 \<union> P\<^sub>2 \<union> wrap B\<^sub>2 \<union> {{v} |v. v \<in> S \<union> L}) \<le> 3 / 2 * card P"
+proof (cases \<open>L = {}\<close>)
+  note invrules = inv\<^sub>2E[OF assms(2)]
+  case True
+  then have "card (P\<^sub>1 \<union> wrap B\<^sub>1 \<union> P\<^sub>2 \<union> wrap B\<^sub>2 \<union> {{v} |v. v \<in> S \<union> L})
+           = card (P\<^sub>1 \<union> wrap B\<^sub>1 \<union> P\<^sub>2 \<union> wrap B\<^sub>2)" using assms(1) by simp
+  also have "... \<le> card (P\<^sub>1 \<union> wrap B\<^sub>1) + card (P\<^sub>2 \<union> wrap B\<^sub>2)"
+    using card_Un_le[of \<open>P\<^sub>1 \<union> wrap B\<^sub>1\<close>] by (simp add: Un_assoc)
+  also have "... \<le> card P + card (P\<^sub>2 \<union> wrap B\<^sub>2)"
+    using P\<^sub>1_B\<^sub>1_lower_bound_card[OF assms(3) invrules(1,3)] by simp
+  also have "... \<le> card P + card P / 2"
+    using P\<^sub>2_B\<^sub>2_lower_bound_P\<^sub>1[OF invrules(1,4,3)]
+      and P\<^sub>1_lower_bound_card[OF assms(3) invrules(1,3)] by linarith
+  finally show ?thesis by linarith
+next
+  note invrules = inv\<^sub>2E[OF assms(2)]
+  case False
+  have "card (P\<^sub>1 \<union> wrap B\<^sub>1 \<union> P\<^sub>2 \<union> wrap B\<^sub>2 \<union> {{v} |v. v \<in> S \<union> L})
+      = card (P\<^sub>1 \<union> wrap B\<^sub>1 \<union> {{v} |v. v \<in> L} \<union> P\<^sub>2 \<union> wrap B\<^sub>2)"
+    using assms(1) by (simp add: Un_commute Un_assoc)
+  also have "... \<le> card (P\<^sub>1 \<union> wrap B\<^sub>1 \<union> {{v} |v. v \<in> L}) + card (P\<^sub>2 \<union> wrap B\<^sub>2)"
+    using card_Un_le[of \<open>P\<^sub>1 \<union> wrap B\<^sub>1 \<union> {{v} |v. v \<in> L}\<close>] by (simp add: Un_assoc)
+  also have "... \<le> card P + card (P\<^sub>2 \<union> wrap B\<^sub>2)"
+    using L_bins_lower_bound_card[OF assms(3) invrules(1) invrules(2)[OF False] invrules(5)] by linarith
+  also have "... \<le> card P + card P / 2"
+    using P\<^sub>2_B\<^sub>2_lower_bound_P\<^sub>1[OF invrules(1,4,3)]
+      and P\<^sub>1_lower_bound_card[OF assms(3) invrules(1,3)] by linarith
+  finally show ?thesis by linarith
+qed
+
+definition inv\<^sub>3 :: "'a set set \<Rightarrow> 'a set set \<Rightarrow> 'a set \<Rightarrow> 'a set \<Rightarrow> 'a set \<Rightarrow> 'a set \<Rightarrow> bool" where
+  "inv\<^sub>3 P\<^sub>1 P\<^sub>2 B\<^sub>1 B\<^sub>2 S L \<longleftrightarrow> inv\<^sub>2 P\<^sub>1 P\<^sub>2 B\<^sub>1 B\<^sub>2 S L \<and> B\<^sub>2 \<subseteq> S\<^sub>U"
+
+lemma inv\<^sub>3E:
+  assumes "inv\<^sub>3 P\<^sub>1 P\<^sub>2 B\<^sub>1 B\<^sub>2 S L"
+  shows "inv\<^sub>2 P\<^sub>1 P\<^sub>2 B\<^sub>1 B\<^sub>2 S L" and "B\<^sub>2 \<subseteq> S\<^sub>U"
+  using assms unfolding inv\<^sub>3_def by blast+
+
+lemma inv\<^sub>3I:
+  assumes "inv\<^sub>2 P\<^sub>1 P\<^sub>2 B\<^sub>1 B\<^sub>2 S L" and "B\<^sub>2 \<subseteq> S\<^sub>U"
+  shows "inv\<^sub>3 P\<^sub>1 P\<^sub>2 B\<^sub>1 B\<^sub>2 S L"
+  using assms unfolding inv\<^sub>3_def by blast
+
+lemma loop_init:
+  "inv\<^sub>3 {} {} {} {} S\<^sub>U L\<^sub>U"
+proof -
+  have "S\<^sub>U \<union> L\<^sub>U = U" by auto
+  then have *: "inv\<^sub>1 {} {} {} {} (S\<^sub>U \<union> L\<^sub>U)"
+    unfolding bp_def partition_on_def pairwise_def wrap_def inv\<^sub>1_def
+    using weight by auto
+  have "bij_exists {} (\<Union> ({} \<union> wrap {}))"
+    using bij_betwI' unfolding bij_exists_def by fastforce
+  from inv\<^sub>2I[OF * _ this] have "inv\<^sub>2 {} {} {} {} S\<^sub>U L\<^sub>U" by auto
+  from inv\<^sub>3I[OF this] show ?thesis by blast
+qed
+
+lemma loop_stepA:
+  assumes "inv\<^sub>3 P\<^sub>1 P\<^sub>2 B\<^sub>1 B\<^sub>2 S L" "B\<^sub>1 = {}" "L = {}" "u \<in> S"
+  shows "inv\<^sub>3 P\<^sub>1 P\<^sub>2 {u} B\<^sub>2 (S - {u}) L"
+proof -
+  note invrules = inv\<^sub>2E[OF inv\<^sub>3E(1)[OF assms(1)]]
+  have WEIGHT: "W B\<^sub>1 + w u \<le> c" using invrules(5) assms(2,4) by fastforce
+  from assms(4) have "u \<in> S \<union> L" by blast
+  from inv\<^sub>1_stepA[OF invrules(1) this WEIGHT] assms(2,3) have 1: "inv\<^sub>1 P\<^sub>1 P\<^sub>2 {u} B\<^sub>2 (S - {u} \<union> L)" by simp
+  have 2: "L \<noteq> {} \<Longrightarrow> \<forall>B\<in>P\<^sub>1 \<union> wrap {u}. B \<inter> L\<^sub>U \<noteq> {}" using assms(3) by blast
+  from inv\<^sub>2I[OF 1 2] invrules have "inv\<^sub>2 P\<^sub>1 P\<^sub>2 {u} B\<^sub>2 (S - {u}) L" by blast
+  from inv\<^sub>3I[OF this] show ?thesis using inv\<^sub>3E(2)[OF assms(1)] .
+qed
+
+lemma loop_stepB:
+  assumes "inv\<^sub>3 P\<^sub>1 P\<^sub>2 B\<^sub>1 B\<^sub>2 S L" "B\<^sub>1 = {}" "u \<in> L"
+  shows "inv\<^sub>3 P\<^sub>1 P\<^sub>2 {u} B\<^sub>2 S (L - {u})"
+proof -
+  note invrules = inv\<^sub>2E[OF inv\<^sub>3E(1)[OF assms(1)]]
+  have WEIGHT: "W B\<^sub>1 + w u \<le> c" using weight invrules(5) assms(2,3) by fastforce
+
+  \<comment> \<open>This observation follows from the fact that the \<open>S\<close> and \<open>L\<close> sets have to be disjoint from each other,
+      and allows us to reuse our proofs of the preservation of \<open>inv\<^sub>1\<close> by simply replacing \<open>V\<close> with \<open>S \<union> L\<close>\<close>
+  have *: "S \<union> L - {u} = S \<union> (L - {u})" using invrules(5) assms(3) by force
+  from assms(3) have "u \<in> S \<union> L" by blast
+  from inv\<^sub>1_stepA[OF invrules(1) this WEIGHT] assms(2) * have 1: "inv\<^sub>1 P\<^sub>1 P\<^sub>2 {u} B\<^sub>2 (S \<union> (L - {u}))" by simp
+  have "\<forall>B\<in>P\<^sub>1. B \<inter> L\<^sub>U \<noteq> {}" "{u} \<inter> L\<^sub>U \<noteq> {}" using assms(3) invrules(2,5) by blast+
+  then have 2: "L \<noteq> {} \<Longrightarrow> \<forall>B\<in>P\<^sub>1 \<union> wrap {u}. B \<inter> L\<^sub>U \<noteq> {}"
+    using assms(3) by (metis (full_types) Un_iff empty_iff insert_iff wrap_not_empty)
+  from inv\<^sub>2I[OF 1 2] invrules have "inv\<^sub>2 P\<^sub>1 P\<^sub>2 {u} B\<^sub>2 S (L - {u})" by blast
+  from inv\<^sub>3I[OF this] show ?thesis using inv\<^sub>3E(2)[OF assms(1)] .
+qed
+
+lemma loop_stepC:
+  assumes "inv\<^sub>3 P\<^sub>1 P\<^sub>2 B\<^sub>1 B\<^sub>2 S L" "B\<^sub>1 \<noteq> {}" "u \<in> S" "W B\<^sub>1 + w(u) \<le> c"
+  shows "inv\<^sub>3 P\<^sub>1 P\<^sub>2 (B\<^sub>1 \<union> {u}) B\<^sub>2 (S - {u}) L"
+proof -
+  note invrules = inv\<^sub>2E[OF inv\<^sub>3E(1)[OF assms(1)]]
+
+  \<comment> \<open>Same approach, but removing \<open>{u}\<close> from \<open>S\<close> instead of \<open>L\<close>\<close>
+  have *: "S \<union> L - {u} = (S - {u}) \<union> L" using invrules(5) assms(3) by force
+  from assms(3) have "u \<in> S \<union> L" by blast
+  from inv\<^sub>1_stepA[OF invrules(1) this assms(4)] * have 1: "inv\<^sub>1 P\<^sub>1 P\<^sub>2 (B\<^sub>1 \<union> {u}) B\<^sub>2 (S - {u} \<union> L)" by simp
+  have "L \<noteq> {} \<Longrightarrow> \<forall>B\<in>P\<^sub>1 \<union> wrap B\<^sub>1. B \<inter> L\<^sub>U \<noteq> {}" using invrules(2) by blast
+  then have 2: "L \<noteq> {} \<Longrightarrow> \<forall>B\<in>P\<^sub>1 \<union> wrap (B\<^sub>1 \<union> {u}). B \<inter> L\<^sub>U \<noteq> {}"
+    by (smt Int_insert_left Un_empty_right Un_iff Un_insert_right assms(2) insert_not_empty singletonD singletonI wrap_def)
+  from inv\<^sub>2I[OF 1 2] invrules have "inv\<^sub>2 P\<^sub>1 P\<^sub>2 (B\<^sub>1 \<union> {u}) B\<^sub>2 (S - {u}) L" by blast
+  from inv\<^sub>3I[OF this] show ?thesis using inv\<^sub>3E(2)[OF assms(1)] .
+qed
+
+lemma loop_stepD:
+  assumes "inv\<^sub>3 P\<^sub>1 P\<^sub>2 B\<^sub>1 B\<^sub>2 S L" "B\<^sub>1 \<noteq> {}" "u \<in> S" "W B\<^sub>1 + w(u) > c" "W B\<^sub>2 + w(u) \<le> c"
+  shows "inv\<^sub>3 (P\<^sub>1 \<union> wrap B\<^sub>1) P\<^sub>2 {} (B\<^sub>2 \<union> {u}) (S - {u}) L"
+proof -
+  note invrules = inv\<^sub>2E[OF inv\<^sub>3E(1)[OF assms(1)]]
+  have *: "S \<union> L - {u} = (S - {u}) \<union> L" using invrules(5) assms(3) by force
+  from assms(3) have "u \<in> S \<union> L" by blast
+  from inv\<^sub>1_stepB[OF invrules(1) this assms(5)] * have 1: "inv\<^sub>1 (P\<^sub>1 \<union> wrap B\<^sub>1) P\<^sub>2 {} (B\<^sub>2 \<union> {u}) (S - {u} \<union> L)" by simp
+
+  have 2: "L \<noteq> {} \<Longrightarrow> \<forall>B\<in>P\<^sub>1 \<union> wrap B\<^sub>1 \<union> wrap {}. B \<inter> L\<^sub>U \<noteq> {}"
+    using invrules(2) unfolding wrap_empty by blast
+
+  from invrules(3) obtain f where f_def: "bij_betw f P\<^sub>1 (\<Union> (P\<^sub>2 \<union> wrap B\<^sub>2))" "\<forall>B\<in>P\<^sub>1. c < W B + w (f B)" unfolding bij_exists_def by blast
+  have "B\<^sub>1 \<notin> P\<^sub>1" using inv\<^sub>1E(3)[OF invrules(1)] by blast
+  have "u \<notin> (\<Union> (P\<^sub>2 \<union> wrap B\<^sub>2))" using inv\<^sub>1E(2)[OF invrules(1)] assms(3) by blast
+  then have "(\<Union> (P\<^sub>2 \<union> wrap (B\<^sub>2 \<union> {u}))) = (\<Union> (P\<^sub>2 \<union> wrap B\<^sub>2 \<union> {{u}}))"
+    by (metis Sup_empty Un_assoc Union_Un_distrib ccpo_Sup_singleton wrap_empty wrap_not_empty)
+  also have "... = (\<Union> (P\<^sub>2 \<union> wrap B\<^sub>2)) \<union> {u}" by simp
+  finally have UN: "(\<Union> (P\<^sub>2 \<union> wrap (B\<^sub>2 \<union> {u}))) = (\<Union> (P\<^sub>2 \<union> wrap B\<^sub>2)) \<union> {u}" .
+  have "wrap B\<^sub>1 = {B\<^sub>1}" using wrap_not_empty[of B\<^sub>1] assms(2) by simp
+  let ?f = "f (B\<^sub>1 := u)"
+  have BIJ: "bij_betw ?f (P\<^sub>1 \<union> wrap B\<^sub>1) (\<Union> (P\<^sub>2 \<union> wrap (B\<^sub>2 \<union> {u})))"
+    unfolding wrap_empty \<open>wrap B\<^sub>1 = {B\<^sub>1}\<close> UN using f_def(1) \<open>B\<^sub>1 \<notin> P\<^sub>1\<close> \<open>u \<notin> (\<Union> (P\<^sub>2 \<union> wrap B\<^sub>2))\<close>
+    by (metis (no_types, lifting) bij_betw_cong fun_upd_other fun_upd_same notIn_Un_bij_betw3)
+  have "c < W B\<^sub>1 + w (?f B\<^sub>1)" using assms(4) by simp
+  then have "(\<forall>B\<in>P\<^sub>1 \<union> wrap B\<^sub>1. c < W B + w (?f B))"
+    unfolding \<open>wrap B\<^sub>1 = {B\<^sub>1}\<close> using f_def(2) by simp
+  with BIJ have "bij_betw ?f (P\<^sub>1 \<union> wrap B\<^sub>1) (\<Union> (P\<^sub>2 \<union> wrap (B\<^sub>2 \<union> {u})))
+              \<and> (\<forall>B\<in>P\<^sub>1 \<union> wrap B\<^sub>1. c < W B + w (?f B))" by blast
+  then have 3: "bij_exists (P\<^sub>1 \<union> wrap B\<^sub>1) (\<Union> (P\<^sub>2 \<union> wrap (B\<^sub>2 \<union> {u})))"
+    unfolding bij_exists_def by blast
+  from inv\<^sub>2I[OF 1 2 3] have "inv\<^sub>2 (P\<^sub>1 \<union> wrap B\<^sub>1) P\<^sub>2 {} (B\<^sub>2 \<union> {u}) (S - {u}) L" using invrules(4,5) by blast
+
+  from inv\<^sub>3I[OF this] show ?thesis using inv\<^sub>3E(2)[OF assms(1)] assms(3) invrules(5) by blast
+qed
+
+lemma B\<^sub>2_at_least_two_objects:
+  assumes "inv\<^sub>3 P\<^sub>1 P\<^sub>2 B\<^sub>1 B\<^sub>2 S L" "u \<in> S" "W B\<^sub>2 + w(u) > c"
+  shows "2 \<le> card B\<^sub>2"
+proof (rule ccontr, simp add: not_le)
+  have FINITE: "finite B\<^sub>2" using inv\<^sub>1E(1)[OF inv\<^sub>2E(1)[OF inv\<^sub>3E(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 B\<^sub>2 < 2"
+  then consider (0) "card B\<^sub>2 = 0" | (1) "card B\<^sub>2 = 1" by linarith
+  then show False proof cases
+    case 0 then have "B\<^sub>2 = {}" using FINITE by simp
+    then show ?thesis using assms(2,3) inv\<^sub>2E(5)[OF inv\<^sub>3E(1)[OF assms(1)]] by force
+  next
+    case 1 then obtain v where "B\<^sub>2 = {v}"
+      using card_1_singletonE by auto
+    with inv\<^sub>3E(2)[OF assms(1)] have "2 * w v \<le> c" using inv\<^sub>2E(5)[OF inv\<^sub>3E(1)[OF assms(1)]] by simp
+    moreover from \<open>B\<^sub>2 = {v}\<close> have "W B\<^sub>2 = w v" by simp
+    ultimately show ?thesis using assms(2,3) inv\<^sub>2E(5)[OF inv\<^sub>3E(1)[OF assms(1)]] by force
+  qed
+qed
+
+lemma loop_stepE:
+  assumes "inv\<^sub>3 P\<^sub>1 P\<^sub>2 B\<^sub>1 B\<^sub>2 S L" "B\<^sub>1 \<noteq> {}" "u \<in> S" "W B\<^sub>1 + w(u) > c" "W B\<^sub>2 + w(u) > c"
+  shows "inv\<^sub>3 (P\<^sub>1 \<union> wrap B\<^sub>1) (P\<^sub>2 \<union> wrap B\<^sub>2) {} {u} (S - {u}) L"
+proof -
+  note invrules = inv\<^sub>2E[OF inv\<^sub>3E(1)[OF assms(1)]]
+  have *: "S \<union> L - {u} = (S - {u}) \<union> L" using invrules(5) assms(3) by force
+  from assms(3) have "u \<in> S \<union> L" by blast
+  from inv\<^sub>1_stepC[OF invrules(1) this] * have 1: "inv\<^sub>1 (P\<^sub>1 \<union> wrap B\<^sub>1) (P\<^sub>2 \<union> wrap B\<^sub>2) {} {u} (S - {u} \<union> L)" by simp
+
+  have 2: "L \<noteq> {} \<Longrightarrow> \<forall>B\<in>P\<^sub>1 \<union> wrap B\<^sub>1 \<union> wrap {}. B \<inter> L\<^sub>U \<noteq> {}"
+    using invrules(2) unfolding wrap_empty by blast
+
+  from invrules(3) obtain f where f_def: "bij_betw f P\<^sub>1 (\<Union> (P\<^sub>2 \<union> wrap B\<^sub>2))" "\<forall>B\<in>P\<^sub>1. c < W B + w (f B)" unfolding bij_exists_def by blast
+  have "B\<^sub>1 \<notin> P\<^sub>1" using inv\<^sub>1E(3)[OF invrules(1)] by blast
+  have "u \<notin> (\<Union> (P\<^sub>2 \<union> wrap B\<^sub>2))" using inv\<^sub>1E(2)[OF invrules(1)] assms(3) by blast
+  have "(\<Union> (P\<^sub>2 \<union> wrap B\<^sub>2 \<union> wrap {u})) = (\<Union> (P\<^sub>2 \<union> wrap B\<^sub>2 \<union> {{u}}))" unfolding wrap_def by simp
+  also have "... = (\<Union> (P\<^sub>2 \<union> wrap B\<^sub>2)) \<union> {u}" by simp
+  finally have UN: "(\<Union> (P\<^sub>2 \<union> wrap B\<^sub>2 \<union> wrap {u})) = (\<Union> (P\<^sub>2 \<union> wrap B\<^sub>2)) \<union> {u}" .
+  have "wrap B\<^sub>1 = {B\<^sub>1}" using wrap_not_empty[of B\<^sub>1] assms(2) by simp
+  let ?f = "f (B\<^sub>1 := u)"
+  have BIJ: "bij_betw ?f (P\<^sub>1 \<union> wrap B\<^sub>1) (\<Union> (P\<^sub>2 \<union> wrap B\<^sub>2 \<union> wrap {u}))"
+    unfolding wrap_empty \<open>wrap B\<^sub>1 = {B\<^sub>1}\<close> UN using f_def(1) \<open>B\<^sub>1 \<notin> P\<^sub>1\<close> \<open>u \<notin> (\<Union> (P\<^sub>2 \<union> wrap B\<^sub>2))\<close>
+    by (metis (no_types, lifting) bij_betw_cong fun_upd_other fun_upd_same notIn_Un_bij_betw3)
+  have "c < W B\<^sub>1 + w (?f B\<^sub>1)" using assms(4) by simp
+  then have "(\<forall>B\<in>P\<^sub>1 \<union> wrap B\<^sub>1. c < W B + w (?f B))"
+    unfolding \<open>wrap B\<^sub>1 = {B\<^sub>1}\<close> using f_def(2) by simp
+  with BIJ have "bij_betw ?f (P\<^sub>1 \<union> wrap B\<^sub>1) (\<Union> (P\<^sub>2 \<union> wrap B\<^sub>2 \<union> wrap {u}))
+              \<and> (\<forall>B\<in>P\<^sub>1 \<union> wrap B\<^sub>1. c < W B + w (?f B))" by blast
+  then have 3: "bij_exists (P\<^sub>1 \<union> wrap B\<^sub>1) (\<Union> (P\<^sub>2 \<union> wrap B\<^sub>2 \<union> wrap {u}))"
+    unfolding bij_exists_def by blast
+
+  have 4: "2 * card (P\<^sub>2 \<union> wrap B\<^sub>2) \<le> card (\<Union> (P\<^sub>2 \<union> wrap B\<^sub>2))"
+  proof -
+    note bprules = bpE[OF inv\<^sub>1E(1)[OF invrules(1)]]
+    have "pairwise disjnt (P\<^sub>2 \<union> wrap B\<^sub>2)"
+      using bprules(1) pairwise_subset by blast
+    moreover have "B\<^sub>2 \<notin> P\<^sub>2" using inv\<^sub>1E(4)[OF invrules(1)]  by simp
+    ultimately have DISJNT: "\<Union>P\<^sub>2 \<inter> B\<^sub>2 = {}"
+      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 (\<Union>P\<^sub>2)" using U_Finite bprules(3) by auto
+    have "finite B\<^sub>2" using inv\<^sub>1E(1)[OF invrules(1)] bp_bins_finite wrap_not_empty by blast
+
+    have "2 * card (P\<^sub>2 \<union> wrap B\<^sub>2) \<le> 2 * (card P\<^sub>2 + card (wrap B\<^sub>2))"
+      using card_Un_le[of P\<^sub>2 \<open>wrap B\<^sub>2\<close>] by simp
+    also have "... \<le> 2 * card P\<^sub>2 + 2" using wrap_card by auto
+    also have "... \<le> card (\<Union> P\<^sub>2) + 2" using invrules(4) by simp
+    also have "... \<le> card (\<Union> P\<^sub>2) + card B\<^sub>2" using B\<^sub>2_at_least_two_objects[OF assms(1,3,5)] by simp
+    also have "... = card (\<Union> (P\<^sub>2 \<union> {B\<^sub>2}))" using DISJNT card_Un_disjoint[OF \<open>finite (\<Union>P\<^sub>2)\<close> \<open>finite B\<^sub>2\<close>] by (simp add: Un_commute)
+    also have "... = card (\<Union> (P\<^sub>2 \<union> wrap B\<^sub>2))" by (cases \<open>B\<^sub>2 = {}\<close>) auto
+    finally show ?thesis .
+  qed
+  from inv\<^sub>2I[OF 1 2 3 4] have "inv\<^sub>2 (P\<^sub>1 \<union> wrap B\<^sub>1) (P\<^sub>2 \<union> wrap B\<^sub>2) {} {u} (S - {u}) L"
+    using invrules(5) by blast
+
+  from inv\<^sub>3I[OF this] show ?thesis using assms(3) invrules(5) by blast
+qed
+
+text \<open>The bin packing algorithm as it is proposed on page 78 of the article @{cite BerghammerR03}.
+      \<open>P\<close> will not only be a correct solution of the bin packing problem, but the amount of bins
+      will be a lower bound for \<open>3 / 2\<close> of the amount of bins of any correct solution \<open>Q\<close>, and thus
+      guarantee an approximation factor of \<open>3 / 2\<close> for the optimum.\<close>
+lemma bp_approx:
+"VARS P P\<^sub>1 P\<^sub>2 B\<^sub>1 B\<^sub>2 V S L u
+  {True}
+  S := {}; L:= {}; V := U;
+  WHILE V \<noteq> {} INV {V \<subseteq> U \<and> S = {u \<in> U - V. w(u) \<le> c / 2} \<and> L = {u \<in> U - V. c / 2 < w(u)}} DO
+    u := (SOME u. u \<in> V);
+    IF w(u) \<le> c / 2
+    THEN S := S \<union> {u}
+    ELSE L := L \<union> {u} FI;
+    V := V - {u}
+  OD;
+  P\<^sub>1 := {}; P\<^sub>2 := {}; B\<^sub>1 := {}; B\<^sub>2 := {};
+  WHILE S \<noteq> {} INV {inv\<^sub>3 P\<^sub>1 P\<^sub>2 B\<^sub>1 B\<^sub>2 S L} DO 
+    IF B\<^sub>1 \<noteq> {}
+    THEN u := (SOME u. u \<in> S); S := S - {u}
+    ELSE IF L \<noteq> {}
+         THEN u := (SOME u. u \<in> L); L := L - {u}
+         ELSE u := (SOME u. u \<in> S); S := S - {u} FI FI;
+    IF W(B\<^sub>1) + w(u) \<le> c
+    THEN B\<^sub>1 := B\<^sub>1 \<union> {u}
+    ELSE IF W(B\<^sub>2) + w(u) \<le> c
+         THEN B\<^sub>2 := B\<^sub>2 \<union> {u}
+         ELSE P\<^sub>2 := P\<^sub>2 \<union> wrap B\<^sub>2; B\<^sub>2 := {u} FI;
+         P\<^sub>1 := P\<^sub>1 \<union> wrap B\<^sub>1; B\<^sub>1 := {} FI
+  OD;
+  P := P\<^sub>1 \<union> wrap B\<^sub>1 \<union> P\<^sub>2 \<union> wrap B\<^sub>2; V := L;
+  WHILE V \<noteq> {}
+  INV {S = {} \<and> inv\<^sub>3 P\<^sub>1 P\<^sub>2 B\<^sub>1 B\<^sub>2 S L \<and> V \<subseteq> L \<and> P = P\<^sub>1 \<union> wrap B\<^sub>1 \<union> P\<^sub>2 \<union> wrap B\<^sub>2 \<union> {{v}|v. v \<in> L - V}} DO
+    u := (SOME u. u \<in> V); P := P \<union> {{u}}; V := V - {u}
+  OD
+  {bp P \<and> (\<forall>Q. bp Q \<longrightarrow> card P \<le> 3 / 2 * card Q)}"
+proof (vcg, goal_cases)
+  case (1 P P\<^sub>1 P\<^sub>2 B\<^sub>1 B\<^sub>2 V S L u)
+  then show ?case by blast
+next
+  case (2 P P\<^sub>1 P\<^sub>2 B\<^sub>1 B\<^sub>2 V S L u)
+  then show ?case by (auto simp: some_in_eq)
+next
+  case (3 P P\<^sub>1 P\<^sub>2 B\<^sub>1 B\<^sub>2 V S L u)
+  then show ?case using loop_init by force
+next
+  case (4 P P\<^sub>1 P\<^sub>2 B\<^sub>1 B\<^sub>2 V S L u)
+  then have INV: "inv\<^sub>3 P\<^sub>1 P\<^sub>2 B\<^sub>1 B\<^sub>2 S L" ..
+  let ?s = "SOME u. u \<in> S"
+  let ?l = "SOME u. u \<in> L"
+  note SL_def = inv\<^sub>2E(5)[OF inv\<^sub>3E(1)[OF INV]]
+  have LIN: "L \<noteq> {} \<Longrightarrow> ?l \<in> L" using some_in_eq by metis
+  then have LWEIGHT: "L \<noteq> {} \<Longrightarrow> w ?l \<le> c" using weight SL_def by blast
+  from 4 have "S \<noteq> {}" ..
+  then have IN: "?s \<in> S" using some_in_eq by metis
+  then have "w ?s \<le> 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 \<open>B\<^sub>1 = {}\<close>, cases \<open>L = {}\<close>) auto
+next
+  case (5 P P\<^sub>1 P\<^sub>2 B\<^sub>1 B\<^sub>2 V S L u)
+  then show ?case by blast
+next
+  case (6 P P\<^sub>1 P\<^sub>2 B\<^sub>1 B\<^sub>2 V S L u)
+  then have *: "(SOME u. u \<in> V) \<in> V" "(SOME u. u \<in> V) \<in> L" by (auto simp add: some_in_eq)
+  then have "P\<^sub>1 \<union> wrap B\<^sub>1 \<union> P\<^sub>2 \<union> wrap B\<^sub>2 \<union> {{v} |v. v \<in> L - (V - {SOME u. u \<in> V})}
+           = P\<^sub>1 \<union> wrap B\<^sub>1 \<union> P\<^sub>2 \<union> wrap B\<^sub>2 \<union> {{v} |v. v \<in> L - V \<union> {SOME u. u \<in> V}}"
+    by blast
+  with 6 * show ?case by blast
+next
+  case (7 P P\<^sub>1 P\<^sub>2 B\<^sub>1 B\<^sub>2 V S L u)
+  then have *: "inv\<^sub>2 P\<^sub>1 P\<^sub>2 B\<^sub>1 B\<^sub>2 S L"
+    using inv\<^sub>3E(1) by blast
+  from inv\<^sub>1E(1)[OF inv\<^sub>2E(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 *)
\ No newline at end of file
diff --git a/thys/Approximation_Algorithms/Approx_LB_Hoare.thy b/thys/Approximation_Algorithms/Approx_LB_Hoare.thy
new file mode 100644
--- /dev/null
+++ b/thys/Approximation_Algorithms/Approx_LB_Hoare.thy
@@ -0,0 +1,609 @@
+section \<open>Load Balancing\<close>
+
+theory Approx_LB_Hoare
+  imports Complex_Main "HOL-Hoare.Hoare_Logic"
+begin
+
+text \<open>This is formalization of the load balancing algorithms and proofs
+in the book by Kleinberg and Tardos \cite{KleinbergT06}.\<close>
+
+hide_const (open) sorted
+
+(* TODO: mv *)
+
+lemma sum_le_card_Max: "\<lbrakk> finite A; A \<noteq> {} \<rbrakk> \<Longrightarrow> sum f A \<le> 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]: "\<lbrakk> finite A; A \<noteq> {} \<rbrakk> \<Longrightarrow> Max ((\<lambda>_. c) ` A) = c"
+using Max_in image_is_empty by blast
+
+abbreviation Max\<^sub>0 :: "nat set \<Rightarrow> nat" where
+"Max\<^sub>0 N \<equiv> (if N={} then 0 else Max N)"
+
+fun f_Max\<^sub>0 :: "(nat \<Rightarrow> nat) \<Rightarrow> nat \<Rightarrow> nat" where
+  "f_Max\<^sub>0 f 0 = 0"
+| "f_Max\<^sub>0 f (Suc x) = max (f (Suc x)) (f_Max\<^sub>0 f x)"
+
+lemma f_Max\<^sub>0_equiv: "f_Max\<^sub>0 f n = Max\<^sub>0 (f ` {1..n})"
+  by (induction n) (auto simp: not_le atLeastAtMostSuc_conv)
+
+lemma f_Max\<^sub>0_correct:
+  "\<forall>x \<in> {1..m}. T x \<le> f_Max\<^sub>0 T m"
+  "m > 0 \<Longrightarrow> \<exists>x \<in> {1..m}. T x = f_Max\<^sub>0 T m"
+   apply (induction m)
+     apply simp_all
+   apply (metis atLeastAtMost_iff le_Suc_eq max.cobounded1 max.coboundedI2)
+  subgoal for m by (cases \<open>m = 0\<close>) (auto simp: max_def)
+  done
+
+lemma f_Max\<^sub>0_mono:
+  "y \<le> T x \<Longrightarrow> f_Max\<^sub>0 (T (x := y)) m \<le> f_Max\<^sub>0 T m"
+  "T x \<le> y \<Longrightarrow> f_Max\<^sub>0 T m \<le> f_Max\<^sub>0 (T (x := y)) m"
+  by (induction m) auto
+
+lemma f_Max\<^sub>0_out_of_range [simp]:
+  "x \<notin> {1..k} \<Longrightarrow> f_Max\<^sub>0 (T (x := y)) k = f_Max\<^sub>0 T k"
+  by (induction k) auto
+
+lemma fun_upd_f_Max\<^sub>0:
+  assumes "x \<in> {1..m}" "T x \<le> y"
+  shows "f_Max\<^sub>0 (T (x := y)) m = max y (f_Max\<^sub>0 T m)"
+  using assms by (induction m) auto
+
+locale LoadBalancing = (* Load Balancing *)
+  fixes t :: "nat \<Rightarrow> nat"
+    and m :: nat
+    and n :: nat
+  assumes m_gt_0: "m > 0"
+begin
+
+subsection \<open>Formalization of a Correct Load Balancing\<close>
+
+subsubsection \<open>Definition\<close>
+
+definition lb :: "(nat \<Rightarrow> nat) \<Rightarrow> (nat \<Rightarrow> nat set) \<Rightarrow> nat \<Rightarrow> bool" where
+  "lb T A j = ((\<forall>x \<in> {1..m}. \<forall>y \<in> {1..m}. x \<noteq> y \<longrightarrow> A x \<inter> A y = {}) \<comment> \<open>No job is assigned to more than one machine\<close>
+             \<and> (\<Union>x \<in> {1..m}. A x) = {1..j} \<comment> \<open>Every job is assigned\<close>
+             \<and> (\<forall>x \<in> {1..m}. (\<Sum>j \<in> A x. t j) = T x) \<comment> \<open>The processing times sum up to the correct load\<close>)"
+
+abbreviation makespan :: "(nat \<Rightarrow> nat) \<Rightarrow> nat" where
+  "makespan T \<equiv> f_Max\<^sub>0 T m"
+
+lemma makespan_def': "makespan T = Max (T ` {1..m})"
+  using m_gt_0 by (simp add: f_Max\<^sub>0_equiv)
+(*
+lemma makespan_correct:
+  "\<forall>x \<in> {1..m}. T x \<le> makespan T m"
+  "m > 0 \<Longrightarrow> \<exists>x \<in> {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 \<open>m = 0\<close>) (auto simp: max_def)
+  done
+
+lemma no_machines_lb_iff_no_jobs: "lb T A j 0 \<longleftrightarrow> j = 0"
+  unfolding lb_def by auto
+
+lemma machines_if_jobs: "\<lbrakk> lb T A j m; j > 0 \<rbrakk> \<Longrightarrow> m > 0"
+  using no_machines_lb_iff_no_jobs by (cases m) auto
+*)
+
+lemma makespan_correct:
+  "\<forall>x \<in> {1..m}. T x \<le> makespan T"
+  "\<exists>x \<in> {1..m}. T x = makespan T"
+  using f_Max\<^sub>0_correct m_gt_0 by auto
+
+lemma lbE:
+  assumes "lb T A j"
+  shows "\<forall>x \<in> {1..m}. \<forall>y \<in> {1..m}. x \<noteq> y \<longrightarrow> A x \<inter> A y = {}"
+        "(\<Union>x \<in> {1..m}. A x) = {1..j}"
+        "\<forall>x \<in> {1..m}. (\<Sum>y \<in> A x. t y) = T x"
+  using assms unfolding lb_def by blast+
+
+lemma lbI:
+  assumes "\<forall>x \<in> {1..m}. \<forall>y \<in> {1..m}. x \<noteq> y \<longrightarrow> A x \<inter> A y = {}"
+          "(\<Union>x \<in> {1..m}. A x) = {1..j}"
+          "\<forall>x \<in> {1..m}. (\<Sum>y \<in> 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 \<in> {1..m}"
+  shows "finite (A x)"
+  by (metis lbE(2) assms finite_UN finite_atLeastAtMost)
+
+text \<open>If \<open>A x\<close> is pairwise disjoint for all \<open>x \<in> {1..m}\<close>, then the the sum over the sums of the
+      individual \<open>A x\<close> is equal to the sum over the union of all \<open>A x\<close>.\<close>
+lemma sum_sum_eq_sum_Un:
+  fixes A :: "nat \<Rightarrow> nat set"
+  assumes "\<forall>x \<in> {1..m}. \<forall>y \<in> {1..m}. x \<noteq> y \<longrightarrow> A x \<inter> A y = {}"
+      and "\<forall>x \<in> {1..m}. finite (A x)"
+  shows "(\<Sum>x \<in> {1..m}. (\<Sum>y \<in> A x. t y)) = (\<Sum>x \<in> (\<Union>y \<in> {1..m}. A y). t x)"
+  using assms
+proof (induction m)
+  case (Suc m)
+  have FINITE: "finite (\<Union>x \<in> {1..m}. A x)" "finite (A (Suc m))"
+    using Suc.prems(2) by auto
+  have "\<forall>x \<in> {1..m}. A x \<inter> A (Suc m) = {}"
+    using Suc.prems(1) by simp
+  then have DISJNT: "(\<Union>x \<in> {1..m}. A x) \<inter> (A (Suc m)) = {}" using Union_disjoint by blast
+  have "(\<Sum>x \<in> (\<Union>y \<in> {1..m}. A y). t x) + (\<Sum>x \<in> A (Suc m). t x)
+      = (\<Sum>x \<in> ((\<Union>y \<in> {1..m}. A y) \<union> A (Suc m)). t x)"
+    using sum.union_disjoint[OF FINITE DISJNT, symmetric] .
+  also have "... = (\<Sum>x \<in> (\<Union>y \<in> {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 \<open>If \<open>T\<close> and \<open>A\<close> are a correct load balancing for \<open>j\<close> jobs and \<open>m\<close> machines, 
+      then the sum of the loads has to be equal to the sum of the processing times of the jobs\<close>
+lemma lb_impl_job_sum:
+  assumes "lb T A j"
+  shows "(\<Sum>x \<in> {1..m}. T x) = (\<Sum>x \<in> {1..j}. t x)"
+proof -
+  note lbrules = lbE[OF assms]
+  from assms have FINITE: "\<forall>x \<in> {1..m}. finite (A x)" by simp
+  have "(\<Sum>x \<in> {1..m}. T x) = (\<Sum>x \<in> {1..m}. (\<Sum>y \<in> A x. t y))"
+    using lbrules(3) by simp
+  also have "... = (\<Sum>x \<in> {1..j}. t x)"
+    using sum_sum_eq_sum_Un[OF lbrules(1) FINITE]
+    unfolding lbrules(2) .
+  finally show ?thesis .
+qed
+
+subsubsection \<open>Lower Bounds for the Makespan\<close>
+
+text \<open>If \<open>T\<close> and \<open>A\<close> are a correct load balancing for \<open>j\<close> jobs and \<open>m\<close> machines, then the processing time
+      of any job \<open>x \<in> {1..j}\<close> is a lower bound for the load of some machine \<open>y \<in> {1..m}\<close>\<close>
+lemma job_lower_bound_machine:
+  assumes "lb T A j" "x \<in> {1..j}"
+  shows "\<exists>y \<in> {1..m}. t x \<le> T y"
+proof -
+  note lbrules = lbE[OF assms(1)]
+  have "\<exists>y \<in> {1..m}. x \<in> A y" using lbrules(2) assms(2) by blast
+  then obtain y where y_def: "y \<in> {1..m}" "x \<in> A y" ..
+  moreover have "finite (A y)" using assms(1) y_def(1) by simp
+  ultimately have "t x \<le> (\<Sum>x \<in> 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 \<open>As the load of any machine is a lower bound for the makespan, the processing time 
+      of any job \<open>x \<in> {1..j}\<close> has to also be a lower bound for the makespan.
+      Follows from @{thm [source] job_lower_bound_machine} and @{thm [source] makespan_correct}.\<close>
+lemma job_lower_bound_makespan:
+  assumes "lb T A j" "x \<in> {1..j}"
+  shows "t x \<le> makespan T"
+  by (meson job_lower_bound_machine[OF assms] makespan_correct(1) le_trans)
+
+text \<open>The makespan over \<open>j\<close> jobs is a lower bound for the makespan of any correct load balancing for \<open>j\<close> jobs.\<close>
+lemma max_job_lower_bound_makespan:
+  assumes "lb T A j"
+  shows "Max\<^sub>0 (t ` {1..j}) \<le> makespan T"
+  using job_lower_bound_makespan[OF assms] by fastforce
+
+lemma job_dist_lower_bound_makespan:
+  assumes "lb T A j"
+  shows "(\<Sum>x \<in> {1..j}. t x) / m \<le> makespan T"
+proof -
+  have "(\<Sum>x \<in> {1..j}. t x) \<le> 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 (\<Sum>x \<in> {1..j}. t x) \<le> real m * real (makespan T)"
+    using of_nat_mono by fastforce
+  then show ?thesis by (simp add: field_simps m_gt_0)
+qed
+
+subsection \<open>The Greedy Approximation Algorithm\<close>
+
+text \<open>This function will perform a linear scan from \<open>k \<in> {1..m}\<close> and return the index of the machine with minimum load assuming \<open>m > 0\<close>\<close>
+fun min\<^sub>k :: "(nat \<Rightarrow> nat) \<Rightarrow> nat \<Rightarrow> nat" where
+  "min\<^sub>k T 0 = 1"
+| "min\<^sub>k T (Suc x) =
+   (let k = min\<^sub>k T x
+    in if T (Suc x) < T k then (Suc x) else k)"
+
+lemma min_correct:
+  "\<forall>x \<in> {1..m}. T (min\<^sub>k T m) \<le> T x"
+  by (induction m) (auto simp: Let_def le_Suc_eq, force)
+
+lemma min_in_range:
+  "k > 0 \<Longrightarrow> (min\<^sub>k T k) \<in> {1..k}"
+  by (induction k) (auto simp: Let_def, force+)
+
+lemma add_job:
+  assumes "lb T A j" "x \<in> {1..m}"
+  shows "lb (T (x := T x + t (Suc j))) (A (x := A x \<union> {Suc j})) (Suc j)"
+    (is \<open>lb ?T ?A _\<close>)
+proof -
+  note lbrules = lbE[OF assms(1)]
+
+  \<comment> \<open>Rule 1: @{term ?A} pairwise disjoint\<close>
+  have NOTIN: "\<forall>i \<in> {1..m}. Suc j \<notin> A i" using lbrules(2) assms(2) by force
+  with lbrules(1) have "\<forall>i \<in> {1..m}. i \<noteq> x \<longrightarrow> A i \<inter> (A x \<union> {Suc j}) = {}"
+    using assms(2) by blast
+  then have 1: "\<forall>x \<in> {1..m}. \<forall>y \<in> {1..m}. x \<noteq> y \<longrightarrow> ?A x \<inter> ?A y = {}"
+    using lbrules(1) by simp
+
+  \<comment> \<open>Rule 2: @{term ?A} contains all jobs\<close>
+  have "(\<Union>y \<in> {1..m}. ?A y) = (\<Union>y \<in> {1..m}. A y) \<union> {Suc j}"
+    using UNION_fun_upd assms(2) by auto
+  also have "... = {1..Suc j}" unfolding lbrules(2) by auto
+  finally have 2: "(\<Union>y \<in> {1..m}. ?A y) = {1..Suc j}" .
+
+  \<comment> \<open>Rule 3: @{term ?A} sums to @{term ?T}\<close>
+  have "(\<Sum>i \<in> ?A x. t i) = (\<Sum>i \<in> A x \<union> {Suc j}. t i)" by simp
+  moreover have "A x \<inter> {Suc j} = {}" using NOTIN assms(2) by blast
+  moreover have "finite (A x)" "finite {Suc j}" using assms by simp+
+  ultimately have "(\<Sum>i \<in> ?A x. t i) = (\<Sum>i \<in> A x. t i) + (\<Sum>i \<in> {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 "(\<Sum>i \<in> ?A x. t i) = ?T x" by simp
+  then have 3: "\<forall>i \<in> {1..m}. (\<Sum>j \<in> ?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 \<le> T x \<Longrightarrow> makespan (T (x := y)) \<le> makespan T"
+  "T x \<le> y \<Longrightarrow> makespan T \<le> makespan (T (x := y))"
+  using f_Max\<^sub>0_mono by auto
+
+lemma smaller_optimum:
+  assumes "lb T A (Suc j)"
+  shows "\<exists>T' A'. lb T' A' j \<and> makespan T' \<le> makespan T"
+proof -
+  note lbrules = lbE[OF assms]
+  have "\<exists>x \<in> {1..m}. Suc j \<in> A x" using lbrules(2) by auto
+  then obtain x where x_def: "x \<in> {1..m}" "Suc j \<in> A x" ..
+  let ?T = "T (x := T x - t (Suc j))"
+  let ?A = "A (x := A x - {Suc j})"
+
+  \<comment> \<open>Rule 1: @{term ?A} pairwise disjoint\<close>
+  from lbrules(1) have "\<forall>i \<in> {1..m}. i \<noteq> x \<longrightarrow> A i \<inter> (A x - {Suc j}) = {}"
+    using x_def(1) by blast
+  then have 1: "\<forall>x \<in> {1..m}. \<forall>y \<in> {1..m}. x \<noteq> y \<longrightarrow> ?A x \<inter> ?A y = {}"
+    using lbrules(1) by auto
+
+  \<comment> \<open>Rule 2: @{term ?A} contains all jobs\<close>
+  have NOTIN: "\<forall>i \<in> {1..m}. i \<noteq> x \<longrightarrow> Suc j \<notin> A i" using lbrules(1) x_def by blast
+  then have "(\<Union>y \<in> {1..m}. ?A y) = (\<Union>y \<in> {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: "(\<Union>y \<in> {1..m}. ?A y) = {1..j}" .
+
+  \<comment> \<open>Rule 3: @{term ?A} sums to @{term ?T}\<close>
+  have "(\<Sum>i \<in> A x - {Suc j}. t i) = (\<Sum>i \<in> 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 "(\<Sum>i \<in> ?A x. t i) = ?T x" by simp
+  then have 3: "\<forall>i \<in> {1..m}. (\<Sum>j \<in> ?A i. t j) = ?T i"
+    using lbrules(3) x_def(1) by simp
+
+  \<comment> \<open>@{term makespan} is not larger\<close>
+  have "lb ?T ?A j \<and> makespan ?T \<le> makespan T"
+    using lbI[OF 1 2 3] makespan_mono(1) by force
+  then show ?thesis by blast
+qed
+
+text \<open>If the processing time \<open>y\<close> does not contribute to the makespan, we can ignore it.\<close>
+lemma remove_small_job:
+  assumes "makespan (T (x := T x + y)) \<noteq> 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 \<noteq> ?T x" using assms(1) by simp
+  then have "\<exists>i \<in> {1..m}. makespan ?T = ?T i \<and> i \<noteq> x"
+    using makespan_correct(2) by metis
+  then obtain i where i_def: "i \<in> {1..m}" "makespan ?T = ?T i" "i \<noteq> 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 (\<lambda>_. 0) = 0"
+  using m_gt_0 by (simp add: makespan_def')
+
+lemma min_avg: "m * T (min\<^sub>k T m) \<le> (\<Sum>i \<in> {1..m}. T i)"
+           (is \<open>_ * ?T \<le> ?S\<close>)
+proof -
+  have "(\<Sum>_ \<in> {1..m}. ?T) \<le> ?S"
+    using sum_mono[of \<open>{1..m}\<close> \<open>\<lambda>_. ?T\<close> T]
+      and min_correct by blast
+  then show ?thesis by simp
+qed
+
+definition inv\<^sub>1 :: "(nat \<Rightarrow> nat) \<Rightarrow> (nat \<Rightarrow> nat set) \<Rightarrow> nat \<Rightarrow> bool" where
+  "inv\<^sub>1 T A j = (lb T A j \<and> j \<le> n \<and> (\<forall>T' A'. lb T' A' j \<longrightarrow> makespan T \<le> 2 * makespan T'))"
+
+lemma inv\<^sub>1E:
+  assumes "inv\<^sub>1 T A j"
+  shows "lb T A j" "j \<le> n"
+        "lb T' A' j \<Longrightarrow> makespan T \<le> 2 * makespan T'"
+  using assms unfolding inv\<^sub>1_def by blast+
+
+lemma inv\<^sub>1I:
+  assumes "lb T A j" "j \<le> n" "\<forall>T' A'. lb T' A' j \<longrightarrow> makespan T \<le> 2 * makespan T'"
+  shows "inv\<^sub>1 T A j" using assms unfolding inv\<^sub>1_def by blast
+
+lemma inv\<^sub>1_step:
+  assumes "inv\<^sub>1 T A j" "j < n"
+  shows "inv\<^sub>1 (T ((min\<^sub>k T m) := T (min\<^sub>k T m) + t (Suc j)))
+              (A ((min\<^sub>k T m) := A (min\<^sub>k T m) \<union> {Suc j})) (Suc j)"
+    (is \<open>inv\<^sub>1 ?T ?A _\<close>)
+proof -
+  note invrules = inv\<^sub>1E[OF assms(1)]
+  \<comment> \<open>Greedy is correct\<close>
+  have LB: "lb ?T ?A (Suc j)"
+    using add_job[OF invrules(1) min_in_range[OF m_gt_0]] by blast
+  \<comment> \<open>Greedy maintains approximation factor\<close>
+  have MK: "\<forall>T' A'. lb T' A' (Suc j) \<longrightarrow> makespan ?T \<le> 2 * makespan T'"
+  proof rule+
+    fix T\<^sub>1 A\<^sub>1 assume "lb T\<^sub>1 A\<^sub>1 (Suc j)"
+    from smaller_optimum[OF this]
+    obtain T\<^sub>0 A\<^sub>0 where "lb T\<^sub>0 A\<^sub>0 j" "makespan T\<^sub>0 \<le> makespan T\<^sub>1" by blast
+    then have IH: "makespan T \<le> 2 * makespan T\<^sub>1"
+      using invrules(3) by force
+    show "makespan ?T \<le> 2 * makespan T\<^sub>1"
+    proof (cases \<open>makespan ?T = T (min\<^sub>k T m) + t (Suc j)\<close>)
+      case True
+      have "m * T (min\<^sub>k T m) \<le> (\<Sum>i \<in> {1..m}. T i)" by (rule min_avg)
+      also have "... = (\<Sum>i \<in> {1..j}. t i)" by (rule lb_impl_job_sum[OF invrules(1)])
+      finally have "real m * T (min\<^sub>k T m) \<le> (\<Sum>i \<in> {1..j}. t i)"
+        by (auto dest: of_nat_mono)
+      with m_gt_0 have "T (min\<^sub>k T m) \<le> (\<Sum>i \<in> {1..j}. t i) / m"
+        by (simp add: field_simps)
+      then have "T (min\<^sub>k T m) \<le> makespan T\<^sub>1"
+        using job_dist_lower_bound_makespan[OF \<open>lb T\<^sub>0 A\<^sub>0 j\<close>] 
+          and \<open>makespan T\<^sub>0 \<le> makespan T\<^sub>1\<close> by linarith
+      moreover have "t (Suc j) \<le> makespan T\<^sub>1"
+        using job_lower_bound_makespan[OF \<open>lb T\<^sub>1 A\<^sub>1 (Suc j)\<close>] 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 inv\<^sub>1I[OF LB _ MK] show ?thesis using assms(2) by simp
+qed
+
+lemma simple_greedy_approximation:
+"VARS T A i j
+{True}
+T := (\<lambda>_. 0);
+A := (\<lambda>_. {});
+j := 0;
+WHILE j < n INV {inv\<^sub>1 T A j} DO
+  i := min\<^sub>k T m;
+  j := (Suc j);
+  A := A (i := A(i) \<union> {j});
+  T := T (i := T(i) + t j)
+OD
+{lb T A n \<and> (\<forall>T' A'. lb T' A' n \<longrightarrow> makespan T \<le> 2 * makespan T')}"
+proof (vcg, goal_cases)
+  case (1 T A i j)
+  then show ?case by (simp add: lb_def inv\<^sub>1_def)
+next
+  case (2 T A i j)
+  then show ?case using inv\<^sub>1_step by simp
+next
+  case (3 T A i j)
+  then show ?case unfolding inv\<^sub>1_def by force
+qed
+
+definition sorted :: "nat \<Rightarrow> bool" where
+  "sorted j = (\<forall>x \<in> {1..j}. \<forall>y \<in> {1..x}. t x \<le> t y)"
+
+lemma sorted_smaller [simp]: "\<lbrakk> sorted j; j \<ge> j' \<rbrakk> \<Longrightarrow> sorted j'"
+  unfolding sorted_def by simp
+
+lemma j_gt_m_pigeonhole:
+  assumes "lb T A j" "j > m"
+  shows "\<exists>x \<in> {1..j}. \<exists>y \<in> {1..j}. \<exists>z \<in> {1..m}. x \<noteq> y \<and> x \<in> A z \<and> y \<in> A z"
+proof -
+  have "\<forall>x \<in> {1..j}. \<exists>y \<in> {1..m}. x \<in> A y"
+    using lbE(2)[OF assms(1)] by blast
+  then have "\<exists>f. \<forall>x \<in> {1..j}. x \<in> A (f x) \<and> f x \<in> {1..m}" by metis
+  then obtain f where f_def: "\<forall>x \<in> {1..j}. x \<in> A (f x) \<and> f x \<in> {1..m}" ..
+  then have "card (f ` {1..j}) \<le> 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 "\<not> inj_on f {1..j}" using pigeonhole by blast
+  then have "\<exists>x \<in> {1..j}. \<exists>y \<in> {1..j}. x \<noteq> y \<and> f x = f y"
+    unfolding inj_on_def by blast
+  then show ?thesis using f_def by metis
+qed
+
+text \<open>If \<open>T\<close> and \<open>A\<close> are a correct load balancing for \<open>j\<close> jobs and \<open>m\<close> machines with \<open>j > m\<close>,
+      and the jobs are sorted in descending order, then there exists a machine \<open>x \<in> {1..m}\<close>
+      whose load is at least twice as large as the processing time of job \<open>j\<close>.\<close>
+lemma sorted_job_lower_bound_machine:
+  assumes "lb T A j" "j > m" "sorted j"
+  shows "\<exists>x \<in> {1..m}. 2 * t j \<le> T x"
+proof -
+  \<comment> \<open>Step 1: Obtaining the jobs\<close>
+  note lbrules = lbE[OF assms(1)]
+  obtain j\<^sub>1 j\<^sub>2 x where *:
+    "j\<^sub>1 \<in> {1..j}" "j\<^sub>2 \<in> {1..j}" "x \<in> {1..m}" "j\<^sub>1 \<noteq> j\<^sub>2" "j\<^sub>1 \<in> A x" "j\<^sub>2 \<in> A x"
+    using j_gt_m_pigeonhole[OF assms(1,2)] by blast
+
+  \<comment> \<open>Step 2: Jobs contained in sum\<close>
+  have "finite (A x)" using assms(1) *(3) by simp
+  then have SUM: "(\<Sum>i \<in> A x. t i) = t j\<^sub>1 + t j\<^sub>2 + (\<Sum>i \<in> A x - {j\<^sub>1} - {j\<^sub>2}. t i)"
+    using *(4-6) by (simp add: sum.remove)
+
+  \<comment> \<open>Step 3: Proof of lower bound\<close>
+  have "t j \<le> t j\<^sub>1" "t j \<le> t j\<^sub>2"
+    using assms(3) *(1-2) unfolding sorted_def by auto
+  then have "2 * t j \<le> t j\<^sub>1 + t j\<^sub>2" by simp
+  also have "... \<le> (\<Sum>i \<in> A x. t i)" unfolding SUM by simp
+  finally have "2 * t j \<le> T x" using lbrules(3) *(3) by simp
+  then show ?thesis using *(3) by blast
+qed
+
+text \<open>Reasoning analogous to @{thm [source] job_lower_bound_makespan}.\<close>
+lemma sorted_job_lower_bound_makespan:
+  assumes "lb T A j" "j > m" "sorted j"
+  shows "2 * t j \<le> makespan T"
+proof -
+  obtain x where x_def: "x \<in> {1..m}" "2 * t j \<le> T x"
+    using sorted_job_lower_bound_machine[OF assms] ..
+  with makespan_correct(1) have "T x \<le> makespan T" by blast
+  with x_def(2) show ?thesis by simp
+qed
+
+lemma min_zero:
+  assumes "x \<in> {1..k}" "T x = 0"
+  shows "T (min\<^sub>k T k) = 0"
+  using assms(1)
+proof (induction k)
+  case (Suc k)
+  show ?case proof (cases \<open>x = Suc k\<close>)
+    case True
+    then show ?thesis using assms(2) by (simp add: Let_def)
+  next
+    case False
+    with Suc have "T (min\<^sub>k T k) = 0" by simp
+    then show ?thesis by simp
+  qed
+qed simp
+
+lemma min_zero_index:
+  assumes "x \<in> {1..k}" "T x = 0"
+  shows "min\<^sub>k T k \<le> x"
+  using assms(1)
+proof (induction k)
+  case (Suc k)
+  show ?case proof (cases \<open>x = Suc k\<close>)
+    case True
+    then show ?thesis using min_in_range[of "Suc k"] by simp
+  next
+    case False
+    with Suc.prems have "x \<in> {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 inv\<^sub>2 :: "(nat \<Rightarrow> nat) \<Rightarrow> (nat \<Rightarrow> nat set) \<Rightarrow> nat \<Rightarrow> bool" where
+  "inv\<^sub>2 T A j = (lb T A j \<and> j \<le> n
+                \<and> (\<forall>T' A'. lb T' A' j \<longrightarrow> makespan T \<le> 3 / 2 * makespan T') 
+                \<and> (\<forall>x > j. T x = 0)
+                \<and> (j \<le> m \<longrightarrow> makespan T = Max\<^sub>0 (t ` {1..j})))"
+
+lemma inv\<^sub>2E:
+  assumes "inv\<^sub>2 T A j"
+  shows "lb T A j" "j \<le> n"
+        "lb T' A' j \<Longrightarrow> makespan T \<le> 3 / 2 * makespan T'"
+        "\<forall>x > j. T x = 0" "j \<le> m \<Longrightarrow> makespan T = Max\<^sub>0 (t ` {1..j})"
+  using assms unfolding inv\<^sub>2_def by blast+
+
+lemma inv\<^sub>2I:
+  assumes "lb T A j" "j \<le> n"
+          "\<forall>T' A'. lb T' A' j \<longrightarrow> makespan T \<le> 3 / 2 * makespan T'"
+          "\<forall>x > j. T x = 0"
+          "j \<le> m \<Longrightarrow> makespan T = Max\<^sub>0 (t ` {1..j})"
+  shows "inv\<^sub>2 T A j"
+  unfolding inv\<^sub>2_def using assms by blast
+
+lemma inv\<^sub>2_step:
+  assumes "sorted n" "inv\<^sub>2 T A j" "j < n"
+  shows "inv\<^sub>2 (T (min\<^sub>k T m := T(min\<^sub>k T m) + t(Suc j)))
+              (A (min\<^sub>k T m := A(min\<^sub>k T m) \<union> {Suc j})) (Suc j)"
+    (is \<open>inv\<^sub>2 ?T ?A _\<close>)
+proof (cases \<open>Suc j > m\<close>)
+  case True note invrules = inv\<^sub>2E[OF assms(2)]
+  \<comment> \<open>Greedy is correct\<close>
+  have LB: "lb ?T ?A (Suc j)"
+    using add_job[OF invrules(1) min_in_range[OF m_gt_0]] by blast
+  \<comment> \<open>Greedy maintains approximation factor\<close>
+  have MK: "\<forall>T' A'. lb T' A' (Suc j) \<longrightarrow> makespan ?T \<le> 3 / 2 * makespan T'"
+  proof rule+
+    fix T\<^sub>1 A\<^sub>1 assume "lb T\<^sub>1 A\<^sub>1 (Suc j)"
+    from smaller_optimum[OF this]
+    obtain T\<^sub>0 A\<^sub>0 where "lb T\<^sub>0 A\<^sub>0 j" "makespan T\<^sub>0 \<le> makespan T\<^sub>1" by blast
+    then have IH: "makespan T \<le> 3 / 2 * makespan T\<^sub>1"
+      using invrules(3) by force
+    show "makespan ?T \<le> 3 / 2 * makespan T\<^sub>1"
+    proof (cases \<open>makespan ?T = T (min\<^sub>k T m) + t (Suc j)\<close>)
+      case True
+      have "m * T (min\<^sub>k T m) \<le> (\<Sum>i \<in> {1..m}. T i)" by (rule min_avg)
+      also have "... = (\<Sum>i \<in> {1..j}. t i)" by (rule lb_impl_job_sum[OF invrules(1)])
+      finally have "real m * T (min\<^sub>k T m) \<le> (\<Sum>i \<in> {1..j}. t i)"
+        by (auto dest: of_nat_mono)
+      with m_gt_0 have "T (min\<^sub>k T m) \<le> (\<Sum>i \<in> {1..j}. t i) / m"
+        by (simp add: field_simps)
+      then have "T (min\<^sub>k T m) \<le> makespan T\<^sub>1"
+        using job_dist_lower_bound_makespan[OF \<open>lb T\<^sub>0 A\<^sub>0 j\<close>] 
+          and \<open>makespan T\<^sub>0 \<le> makespan T\<^sub>1\<close> by linarith
+      moreover have "2 * t (Suc j) \<le> makespan T\<^sub>1"
+        using sorted_job_lower_bound_makespan[OF \<open>lb T\<^sub>1 A\<^sub>1 (Suc j)\<close> \<open>Suc j > m\<close>]
+          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 "\<forall>x > Suc j. ?T x = 0"
+    using invrules(4) min_in_range[OF m_gt_0, of T] True by simp
+  with inv\<^sub>2I[OF LB _ MK] show ?thesis using assms(3) True by simp
+next
+  case False
+  then have IN_RANGE: "Suc j \<in> {1..m}" by simp
+  note invrules = inv\<^sub>2E[OF assms(2)]
+  then have "T (Suc j) = 0" by blast
+
+  \<comment> \<open>Greedy is correct\<close>
+  have LB: "lb ?T ?A (Suc j)"
+    using add_job[OF invrules(1) min_in_range[OF m_gt_0]] by blast
+
+  \<comment> \<open>Greedy is trivially optimal\<close>
+  from IN_RANGE \<open>T (Suc j) = 0\<close> have "min\<^sub>k T m \<le> Suc j"
+    using min_zero_index by blast
+  with invrules(4) have EMPTY: "\<forall>x > Suc j. ?T x = 0" by simp
+  from IN_RANGE \<open>T (Suc j) = 0\<close> have "T (min\<^sub>k T m) = 0"
+    using min_zero by blast
+  with fun_upd_f_Max\<^sub>0[OF min_in_range[OF m_gt_0]] invrules(5) False
+  have TRIV: "makespan ?T = Max\<^sub>0 (t ` {1..Suc j})" unfolding f_Max\<^sub>0_equiv[symmetric] by simp
+  have MK: "\<forall>T' A'. lb T' A' (Suc j) \<longrightarrow> makespan ?T \<le> 3 / 2 * makespan T'"
+    by (auto simp: TRIV[folded f_Max\<^sub>0_equiv]
+            dest!: max_job_lower_bound_makespan[folded f_Max\<^sub>0_equiv])
+
+  from inv\<^sub>2I[OF LB _ MK EMPTY TRIV] show ?thesis using assms(3) by simp
+qed
+
+lemma sorted_greedy_approximation:
+"sorted n \<Longrightarrow> VARS T A i j
+{True}
+T := (\<lambda>_. 0);
+A := (\<lambda>_. {});
+j := 0;
+WHILE j < n INV {inv\<^sub>2 T A j} DO
+  i := min\<^sub>k T m;
+  j := (Suc j);
+  A := A (i := A(i) \<union> {j});
+  T := T (i := T(i) + t j)
+OD
+{lb T A n \<and> (\<forall>T' A'. lb T' A' n \<longrightarrow> makespan T \<le> 3 / 2 * makespan T')}"
+proof (vcg, goal_cases)
+  case (1 T A i j)
+  then show ?case by (simp add: lb_def inv\<^sub>2_def)
+next
+  case (2 T A i j)
+  then show ?case using inv\<^sub>2_step by simp
+next
+  case (3 T A i j)
+  then show ?case unfolding inv\<^sub>2_def by force
+qed
+
+end (* LoadBalancing *)
+
+end (* Theory *)
\ No newline at end of file
diff --git a/thys/Approximation_Algorithms/Approx_MIS_Hoare.thy b/thys/Approximation_Algorithms/Approx_MIS_Hoare.thy
new file mode 100755
--- /dev/null
+++ b/thys/Approximation_Algorithms/Approx_MIS_Hoare.thy
@@ -0,0 +1,561 @@
+section "Independent Set"
+
+theory Approx_MIS_Hoare
+imports
+  "HOL-Hoare.Hoare_Logic"
+  "HOL-Library.Disjoint_Sets"
+begin
+
+
+text \<open>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 \<open>\<Delta>+1\<close> to \<open>\<Delta>\<close>.\<close>
+
+
+subsection "Graph"
+
+text \<open>A set set is simply a set of edges, where an edge is a 2-element set.\<close>
+
+definition independent_vertices :: "'a set set \<Rightarrow> 'a set \<Rightarrow> bool" where
+"independent_vertices E S \<longleftrightarrow> S \<subseteq> \<Union>E \<and> (\<forall>v1 v2. v1 \<in> S \<and> v2 \<in> S \<longrightarrow> {v1, v2} \<notin> E)"
+
+locale Graph_E =
+  fixes E :: "'a set set"
+  assumes finite_E: "finite E"
+  assumes edges2: "e \<in> E \<Longrightarrow> card e = 2"
+begin
+
+fun vertices :: "'a set set \<Rightarrow> 'a set" where
+"vertices G = \<Union>G"
+
+abbreviation V :: "'a set" where
+"V \<equiv> vertices E"
+
+definition approximation_miv :: "nat \<Rightarrow> 'a set \<Rightarrow> bool" where
+"approximation_miv n S \<longleftrightarrow> independent_vertices E S \<and> (\<forall>S'. independent_vertices E S' \<longrightarrow> card S' \<le> card S * n)"
+
+fun neighbors :: "'a \<Rightarrow> 'a set" where
+"neighbors v = {u. {u,v} \<in> E}"
+
+fun degree_vertex :: "'a \<Rightarrow> nat" where
+"degree_vertex v = card (neighbors v)"
+
+abbreviation \<Delta> :: nat where
+"\<Delta> \<equiv> Max{degree_vertex u|u. u \<in> V}"
+
+lemma finite_edges: "e \<in> E \<Longrightarrow> 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 \<Longrightarrow> finite S"
+  by (metis rev_finite_subset independent_vertices_def vertices.simps finite_V)
+
+lemma edge_ex_vertices: "e \<in> E \<Longrightarrow> \<exists>u v. u \<noteq> v \<and> e = {u, v}"
+proof -
+  assume "e \<in> E"
+  then have "card e = Suc (Suc 0)" using edges2 by auto
+  then show "\<exists>u v. u \<noteq> v \<and> e = {u, v}"
+    by (metis card_eq_SucD insertI1)
+qed
+
+lemma \<Delta>_pos [simp]: "E = {} \<or> 0 < \<Delta>"
+proof cases
+  assume "E = {}"
+  then show "E = {} \<or> 0 < \<Delta>" by auto
+next
+  assume 1: "E \<noteq> {}"
+  then have "V \<noteq> {}" using edges2 by fastforce
+  moreover have "finite {degree_vertex u |u. u \<in> V}"
+    by (metis finite_V finite_imageI Setcompr_eq_image)
+  ultimately have 2: "\<Delta> \<in> {degree_vertex u |u. u \<in> V}" using Max_in by auto
+  have "\<Delta> \<noteq> 0"
+  proof
+    assume "\<Delta> = 0"
+    with 2 obtain u where 3: "u \<in> V" and 4: "degree_vertex u = 0" by auto
+    from 3 obtain e where 5: "e \<in> E" and "u \<in> e" by auto
+    moreover with 4 have "\<forall>v. {u, v} \<noteq> e" using finite_neighbors insert_absorb by fastforce
+    ultimately show False using edge_ex_vertices by auto
+  qed
+  then show "E = {} \<or> 0 < \<Delta>" by auto
+qed
+
+lemma \<Delta>_max_degree: "u \<in> V \<Longrightarrow> degree_vertex u \<le> \<Delta>"
+proof -
+  assume H: "u \<in> V"
+  have "finite {degree_vertex u |u. u \<in> V}"
+    by (metis finite_V finite_imageI Setcompr_eq_image)
+  with H show "degree_vertex u \<le> \<Delta>" using Max_ge by auto
+qed
+
+subsection \<open>Wei's algorithm: \<open>(\<Delta>+1)\<close>-approximation\<close>
+
+text \<open>The 'functional' part of the invariant, used to prove that the algorithm produces an independent set of vertices.\<close>
+
+definition inv_iv :: "'a set \<Rightarrow> 'a set \<Rightarrow> bool" where
+"inv_iv S X \<longleftrightarrow> independent_vertices E S
+            \<and> X \<subseteq> V
+            \<and> (\<forall>v1 \<in> (V - X). \<forall>v2 \<in> S. {v1, v2} \<notin> E)
+            \<and> S \<subseteq> X"
+
+text \<open>Strenghten the invariant with an approximation ratio \<open>r\<close>:\<close>
+
+definition inv_approx :: "'a set \<Rightarrow> 'a set \<Rightarrow> nat \<Rightarrow> bool" where
+"inv_approx S X r \<longleftrightarrow> inv_iv S X \<and> card X \<le> card S * r"
+
+text \<open>Preservation of the functional invariant:\<close>
+
+lemma inv_preserv:
+  fixes S :: "'a set"
+    and X :: "'a set"
+    and x :: "'a"
+  assumes inv: "inv_iv S X"
+      and x_def: "x \<in> V - X"
+    shows "inv_iv (insert x S) (X \<union> neighbors x \<union> {x})"
+proof -
+  have inv1: "independent_vertices E S"
+   and inv2: "X \<subseteq> V"
+   and inv3: "S \<subseteq> X"
+   and inv4: "\<forall>v1 v2. v1 \<in> (V - X) \<and> v2 \<in> S \<longrightarrow> {v1, v2} \<notin> E"
+    using inv unfolding inv_iv_def by auto
+  have finite_S: "finite S" using inv1 and independent_vertices_finite by auto
+  have S1: "\<forall>y \<in> S. {x, y} \<notin> E" using inv4 and x_def by blast
+  have S2: "\<forall>x \<in> S. \<forall>y \<in> S. {x, y} \<notin> E" using inv1 unfolding independent_vertices_def by metis
+  have S3: "v1 \<in> insert x S \<Longrightarrow> v2 \<in> insert x S \<Longrightarrow> {v1, v2} \<notin> E" for v1 v2
+    proof -
+      assume "v1 \<in> insert x S" and "v2 \<in> insert x S"
+      then consider
+          (a) "v1 = x" and "v2 = x"
+        | (b) "v1 = x" and "v2 \<in> S"
+        | (c) "v1 \<in> S" and "v2 = x"
+        | (d) "v1 \<in> S" and "v2 \<in> S"
+        by auto
+      then show "{v1, v2} \<notin> 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 \<union> neighbors x \<union> {x} \<subseteq> V"
+  proof
+    fix xa
+    assume "xa \<in> X \<union> neighbors x \<union> {x}"
+    then consider (a) "xa \<in> X" | (b) "xa \<in> neighbors x" | (c) "xa = x" by auto
+    then show "xa \<in> 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 \<subseteq> X \<union> neighbors x \<union> {x}" using inv3 by auto
+  (* invariant conjunct 4 *)
+  moreover have "v1 \<in> V - (X \<union> neighbors x \<union> {x}) \<Longrightarrow> v2 \<in> insert x S \<Longrightarrow> {v1, v2} \<notin> E" for v1 v2
+  proof -
+    assume H: "v1 \<in> V - (X \<union> neighbors x \<union> {x})" and "v2 \<in> insert x S"
+    then consider (a) "v2 = x" | (b) "v2 \<in> S" by auto
+    then show "{v1, v2} \<notin> E"
+    proof cases
+      case a
+      with H have "v1 \<notin> neighbors v2" by blast
+      then show ?thesis by auto
+    next
+      case b
+      from H have "v1 \<in> V - X" by blast
+      with b and inv4 show ?thesis by blast
+    qed
+  qed
+  (* conclusion *)
+  ultimately show "inv_iv (insert x S) (X \<union> neighbors x \<union> {x})" unfolding inv_iv_def by blast
+qed
+
+lemma inv_approx_preserv:
+  assumes inv: "inv_approx S X (\<Delta> + 1)"
+      and x_def: "x \<in> V - X"
+    shows "inv_approx (insert x S) (X \<union> neighbors x \<union> {x}) (\<Delta> + 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 \<notin> 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 \<union> neighbors x \<union> {x})"
+  proof (intro inv_preserv, auto) qed
+  (* the approximation ratio is preserved (at most \<Delta>+1 vertices are removed in any iteration) *)
+  moreover have "card (X \<union> neighbors x \<union> {x}) \<le> card (insert x S) * (\<Delta> + 1)"
+  proof -
+    have "degree_vertex x \<le> \<Delta>" using \<Delta>_max_degree and x_def by auto
+    then have "card (neighbors x \<union> {x}) \<le> \<Delta> + 1" using card_Un_le [of "neighbors x" "{x}"] by auto
+    then have "card (X \<union> neighbors x \<union> {x}) \<le> card X + \<Delta> + 1" using card_Un_le [of X "neighbors x \<union> {x}"] by auto
+    also have "... \<le> card S * (\<Delta> + 1) + \<Delta> + 1" using inv unfolding inv_approx_def by auto
+    also have "... = card (insert x S) * (\<Delta> + 1)" using finite_S and Sx by auto
+    finally show ?thesis .
+  qed
+  (* conclusion *)
+  ultimately show "inv_approx (insert x S) (X \<union> neighbors x \<union> {x}) (\<Delta> + 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 \<Longrightarrow> card V \<le> card S * r \<Longrightarrow> approximation_miv r S"
+proof -
+  assume 1: "independent_vertices E S" and 2: "card V \<le> card S * r"
+  have "independent_vertices E S' \<Longrightarrow> card S' \<le> card S * r" for S'
+  proof -
+    assume  "independent_vertices E S'"
+    then have "S' \<subseteq> V" unfolding independent_vertices_def by auto
+    then have "card S' \<le> card V" using finite_V and card_mono by auto
+    also have "... \<le> card S * r" using 2 by auto
+    finally show "card S' \<le> card S * r" .
+  qed
+  with 1 show "approximation_miv r S" unfolding approximation_miv_def by auto
+qed
+
+theorem wei_approx_\<Delta>_plus_1:
+"VARS (S :: 'a set) (X :: 'a set) (x :: 'a)
+  { True }
+  S := {};
+  X := {};
+  WHILE X \<noteq> V
+  INV { inv_approx S X (\<Delta> + 1) }
+  DO x := (SOME x. x \<in> V - X);
+     S := insert x S;
+     X := X \<union> neighbors x \<union> {x}
+  OD
+  { approximation_miv (\<Delta> + 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 \<in> V - X)"
+  have "V - X \<noteq> {}" using 2 unfolding inv_approx_def inv_iv_def by blast
+  then have "?x \<in> 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 \<open>Wei's algorithm: \<open>\<Delta>\<close>-approximation\<close>
+
+text \<open>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 \<open>\<Delta>\<close> instead of \<open>\<Delta>+1\<close>. In order to do that we must show that among the vertices removed in each iteration, at most \<open>\<Delta>\<close> could belong to an optimal solution. This requires carrying around a set \<open>P\<close> (via a ghost variable) which records the vertices deleted in each iteration.\<close>
+
+definition inv_partition :: "'a set \<Rightarrow> 'a set \<Rightarrow> 'a set set \<Rightarrow> bool" where
+"inv_partition S X P \<longleftrightarrow> inv_iv S X
+                     \<and> \<Union>P = X
+                     \<and> (\<forall>p \<in> P. \<exists>s \<in> V. p = {s} \<union> neighbors s)
+                     \<and> card P = card S
+                     \<and> finite P"
+
+lemma inv_partition_preserv:
+  assumes inv: "inv_partition S X P"
+      and x_def: "x \<in> V - X"
+    shows "inv_partition (insert x S) (X \<union> neighbors x \<union> {x}) (insert ({x} \<union> 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 \<notin> 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 \<union> neighbors x \<union> {x})"
+  proof (intro inv_preserv, auto) qed
+  (* conjunct 1 *)
+  moreover have "\<Union>(insert ({x} \<union> neighbors x) P) = X \<union> neighbors x \<union> {x}"
+    using inv unfolding inv_partition_def by auto
+  (* conjunct 2 *)
+  moreover have "(\<forall>p\<in>insert ({x} \<union> neighbors x) P. \<exists>s \<in> V. p = {s} \<union> neighbors s)"
+    using inv and x_def unfolding inv_partition_def by auto
+  (* conjunct 3 *)
+  moreover have "card (insert ({x} \<union> neighbors x) P) = card (insert x S)"
+  proof -
+    from x_def and inv have "x \<notin> \<Union>P" unfolding inv_partition_def by auto
+    then have "{x} \<union> neighbors x \<notin> P" by auto
+    then have "card (insert ({x} \<union> 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} \<union> neighbors x) P)"
+    using inv unfolding inv_partition_def by auto
+  (* conclusion *)
+  ultimately show "inv_partition (insert x S) (X \<union> neighbors x \<union> {x}) (insert ({x} \<union> neighbors x) P)"
+    unfolding inv_partition_def by auto
+qed
+
+lemma card_Union_le_sum_card:
+  fixes U :: "'a set set"
+  assumes "\<forall>u \<in> U. finite u"
+  shows "card (\<Union>U) \<le> sum card U"
+proof (cases "finite U")
+  case False
+  then show "card (\<Union>U) \<le> sum card U"
+    using card_eq_0_iff finite_UnionD by auto
+next
+  case True
+  then show "card (\<Union>U) \<le> sum card U"
+  proof (induct U rule: finite_induct)
+    case empty
+    then show ?case by auto
+  next
+    case (insert x F)
+    then have "card(\<Union>(insert x F)) \<le> card(x) + card (\<Union>F)" using card_Un_le by auto
+    also have "... \<le> 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 "\<forall>S \<in> U. card S \<le> n"
+  shows "sum card U \<le> card U * n"
+proof cases
+  assume "infinite U \<or> U = {}"
+  then have "sum card U = 0" using sum.infinite by auto
+  then show "sum card U \<le> card U * n" by auto
+next
+  assume "\<not>(infinite U \<or> U = {})"
+  with assms have "finite U" and "U \<noteq> {}"and "\<forall>S \<in> U. card S \<le> n" by auto
+  then show "sum card U \<le> card U * n"
+  proof (induct U rule: finite_ne_induct)
+    case (singleton x)
+    then show ?case by auto
+  next
+    case (insert x F)
+    assume "\<forall>S\<in>insert x F. card S \<le> n"
+    then have 1:"card x \<le> n" and 2:"sum card F \<le> 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 "... \<le> 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 \<Delta> 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: "\<forall>p\<in>P. \<exists>s \<in> V. p = {s} \<union> neighbors s"
+      and ivS: "independent_vertices E S"
+    shows "\<forall>p \<in> P. card (S \<inter> p) \<le> \<Delta>"
+proof
+  fix p
+  assume "p \<in> P"
+  then obtain s where 1: "s \<in> V \<and> p = {s} \<union> neighbors s" using inv by blast
+  then show "card (S \<inter> p) \<le> \<Delta>"
+  proof cases
+    assume "s \<in> S"
+    then have "S \<inter> neighbors s = {}" using ivS unfolding independent_vertices_def by auto
+    then have "S \<inter> p \<subseteq> {s}" using 1 by auto
+    then have 2: "card (S \<inter> p) \<le> 1" using subset_singletonD by fastforce
+    consider (a) "E = {}" | (b) "0 < \<Delta>" using \<Delta>_pos by auto
+    then show "card (S \<inter> p) \<le> \<Delta>"
+    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 \<notin> S"
+    with 1 have "S \<inter> p \<subseteq> neighbors s" by auto
+    then have "card (S \<inter> p) \<le> degree_vertex s" using card_mono and finite_neighbors by auto
+    then show "card (S \<inter> p) \<le> \<Delta>" using 1 and \<Delta>_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 \<Longrightarrow> approximation_miv \<Delta> 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' \<Longrightarrow> card S' \<le> card S * \<Delta>" for S'
+  proof -
+    let ?I = "{S' \<inter> p | p. p \<in> 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' \<subseteq> V" unfolding independent_vertices_def using vertices.simps by blast
+    with H1 have "S' = S' \<inter> \<Union>P" unfolding inv_partition_def by auto
+    then have "S' = (\<Union>p \<in> P. S' \<inter> p)" using Int_Union by auto
+    then have "S' = \<Union>?I" by blast
+    moreover have "finite S'" using H2 and independent_vertices_finite by auto
+    then have "p \<in> P \<Longrightarrow> finite (S' \<inter> p)" for p by auto
+    ultimately have "card S' \<le> sum card ?I" using card_Union_le_sum_card [of ?I] by auto
+    also have "... \<le> card ?I * \<Delta>"
+      using x_or_neighbors [of P S']
+        and sum_card [of ?I \<Delta>]
+        and H1 and H2 unfolding inv_partition_def by auto
+    also have "... \<le> card P * \<Delta>"
+    proof -
+      have "finite P" using H1 unfolding inv_partition_def by auto
+      then have "card ?I \<le> card P"
+        using Setcompr_eq_image [of "\<lambda>p. S' \<inter> p" P]
+          and card_image_le unfolding inv_partition_def by auto
+      then show ?thesis by auto
+    qed
+    also have "... = card S * \<Delta>" using H1 unfolding inv_partition_def by auto
+    ultimately show "card S' \<le> card S * \<Delta>" by auto
+  qed
+  ultimately show "approximation_miv \<Delta> S" unfolding approximation_miv_def by auto
+qed
+
+theorem wei_approx_\<Delta>:
+"VARS (S :: 'a set) (X :: 'a set) (x :: 'a)
+  { True }
+  S := {};
+  X := {};
+  WHILE X \<noteq> V
+  INV { \<exists>P. inv_partition S X P }
+  DO x := (SOME x. x \<in> V - X);
+     S := insert x S;
+     X := X \<union> neighbors x \<union> {x}
+  OD
+  { approximation_miv \<Delta> 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 \<in> V - X)"
+  from 2 obtain P where I: "inv_partition S X P" by auto 
+  then have "V - X \<noteq> {}" using 2 unfolding inv_partition_def by auto
+  then have "?x \<in> V - X" using some_in_eq by metis
+  (* show that the invariant is true with the ghost variable P := insert ({?x} \<union> neighbors ?x) P *)
+  with I have "inv_partition (insert ?x S) (X \<union> neighbors ?x \<union> {?x}) (insert ({?x} \<union> 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 \<open>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 \<open>(\<Delta>+2)/3\<close>, but this is not proved here.\<close>
+
+definition vertex_heuristic :: "'a set \<Rightarrow> 'a \<Rightarrow> bool" where
+"vertex_heuristic X v = (\<forall>u \<in> V - X. card (neighbors v - X) \<le> 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 \<Rightarrow> nat"
+    shows "finite S \<Longrightarrow> S \<noteq> {} \<Longrightarrow> \<exists>x. x \<in> S \<and> (\<forall>y \<in> S. f x \<le> f y)"
+          (is "?P1 \<Longrightarrow> ?P2 \<Longrightarrow> \<exists>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 "\<exists>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 "\<not>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 \<in> V - X"
+    shows "inv_approx (insert x S) (X \<union> neighbors x \<union> {x}) (max (card (neighbors x \<union> {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 \<notin> 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 \<union> neighbors x \<union> {x})"
+  proof (intro inv_preserv, auto) qed
+  (* the approximation ratio is preserved *)
+  moreover have "card (X \<union> neighbors x \<union> {x}) \<le> card (insert x S) * max (card (neighbors x \<union> {x} - X)) s"
+  proof -
+    let ?N = "neighbors x \<union> {x} - X"
+    have "card (X \<union> ?N) \<le> card X + card ?N" using card_Un_le [of X ?N] by auto
+    also have "... \<le> card S * s + card ?N" using inv unfolding inv_approx_def by auto
+    also have "... \<le> card S * max (card ?N) s + card ?N" by auto
+    also have "... \<le> 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 \<union> neighbors x \<union> {x}) (max (card (neighbors x \<union> {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 \<noteq> V
+  INV { inv_approx S X r }
+  DO x := (SOME x. x \<in> V - X \<and> vertex_heuristic X x);
+     S := insert x S;
+     r := max (card (neighbors x \<union> {x} - X)) r;
+     X := X \<union> neighbors x \<union> {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 \<in> V - X \<and> vertex_heuristic X x)"
+  have "V - X \<noteq> {}" 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 "\<exists>x. x \<in> V - X \<and> vertex_heuristic X x"
+    using ex_min_finite_set [where ?f = "\<lambda>x. card (neighbors x - X)"]
+    unfolding vertex_heuristic_def by auto
+  then have x_def: "?x \<in> V - X \<and> vertex_heuristic X ?x"
+    using someI_ex [where ?P = "\<lambda>x. x \<in> V - X \<and> 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
\ No newline at end of file
diff --git a/thys/Approximation_Algorithms/Approx_VC_Hoare.thy b/thys/Approximation_Algorithms/Approx_VC_Hoare.thy
new file mode 100644
--- /dev/null
+++ b/thys/Approximation_Algorithms/Approx_VC_Hoare.thy
@@ -0,0 +1,202 @@
+section "Vertex Cover"
+
+theory Approx_VC_Hoare
+imports "HOL-Hoare.Hoare_Logic"
+begin
+
+text \<open>The algorithm is classical, the proof is based on and augments the one
+by Berghammer and M\"uller-Olm \cite{BerghammerM03}.\<close>
+
+subsection "Graph"
+
+text \<open>A graph is simply a set of edges, where an edge is a 2-element set.\<close>
+
+definition vertex_cover :: "'a set set \<Rightarrow> 'a set \<Rightarrow> bool" where
+"vertex_cover E C = (\<forall>e \<in> E. e \<inter> C \<noteq> {})"
+
+abbreviation matching :: "'a set set \<Rightarrow> bool" where
+"matching M \<equiv> pairwise disjnt M"
+
+lemma card_matching_vertex_cover:
+  "\<lbrakk> finite C;  matching M;  M \<subseteq> E;  vertex_cover E C \<rbrakk> \<Longrightarrow> card M \<le> card C"
+apply(erule card_le_if_inj_on_rel[where r = "\<lambda>e v. v \<in> e"])
+ apply (meson disjnt_def disjnt_iff vertex_cover_def subsetCE)
+by (meson disjnt_iff pairwise_def)
+
+
+subsection "The Approximation Algorithm"
+
+text \<open>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 \<open>F\<close> is simulated by @{term "SOME x. x \<in> F"}.
+The \<open>SOME\<close> operator is built into HOL: @{term "SOME x. P x"} denotes some \<open>x\<close> that satisfies \<open>P\<close>
+if such an \<open>x\<close> 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 \<open>SOME\<close> are notoriously tedious.
+Typically it involves showing first that @{prop "\<exists>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.\<close>
+
+text \<open>Convenient notation for choosing an arbitrary element from a set:\<close>
+abbreviation "some A \<equiv> SOME x. x \<in> A"
+
+locale Edges =
+  fixes E :: "'a set set"
+  assumes finE: "finite E"
+  assumes edges2: "e \<in> E \<Longrightarrow> card e = 2"
+begin
+
+text \<open>The invariant:\<close>
+
+definition "inv_matching C F M =
+  (matching M \<and> M \<subseteq> E \<and> card C \<le> 2 * card M \<and> (\<forall>e \<in> M. \<forall>f \<in> F. e \<inter> f = {}))"
+
+definition invar :: "'a set \<Rightarrow> 'a set set \<Rightarrow> bool" where
+"invar C F = (F \<subseteq> E \<and> vertex_cover (E-F) C \<and> finite C \<and> (\<exists>M. inv_matching C F M))"
+
+text \<open>Preservation of the invariant by the loop body:\<close>
+
+lemma invar_step:
+  assumes "F \<noteq> {}" "invar C F"
+  shows "invar (C \<union> some F) (F - {e' \<in> F. some F \<inter> e' \<noteq> {}})"
+proof -
+  from assms(2) obtain M where "F \<subseteq> E" and vc: "vertex_cover (E-F) C" and fC: "finite C"
+    and m: "matching M" "M \<subseteq> E" and card: "card C \<le> 2 * card M"
+    and disj: "\<forall>e \<in> M. \<forall>f \<in> F. e \<inter> f = {}"
+  by (auto simp: invar_def inv_matching_def)
+  let ?e = "SOME e. e \<in> F"
+  have "?e \<in> F" using \<open>F \<noteq> {}\<close> by (simp add: some_in_eq)
+  hence fe': "finite ?e" using \<open>F \<subseteq> E\<close> edges2 by(intro card_ge_0_finite) auto
+  have "?e \<notin> M" using edges2 \<open>?e \<in> F\<close> disj \<open>F \<subseteq> E\<close> by fastforce
+  have card': "card (C \<union> ?e) \<le> 2 * card (insert ?e M)"
+    using \<open>?e \<in> F\<close> \<open>?e \<notin> M\<close> card_Un_le[of C ?e] \<open>F \<subseteq> E\<close> edges2 card finite_subset[OF m(2) finE]
+    by fastforce
+  let ?M = "M \<union> {?e}"
+  have vc': "vertex_cover (E - (F - {e' \<in> F. ?e \<inter> e' \<noteq> {}})) (C \<union> ?e)"
+    using vc by(auto simp: vertex_cover_def)
+  have m': "inv_matching (C \<union> ?e) (F - {e' \<in> F. ?e \<inter> e' \<noteq> {}}) ?M"
+    using m card' \<open>F \<subseteq> E\<close> \<open>?e \<in> F\<close> disj
+    by(auto simp: inv_matching_def Int_commute disjnt_def pairwise_insert)
+  show ?thesis using \<open>F \<subseteq> E\<close> 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 \<noteq> {}
+  INV {invar C F}
+  DO C := C \<union> some F;
+     F := F - {e' \<in> F. some F \<inter> e' \<noteq> {}}
+  OD
+  {vertex_cover E C \<and> (\<forall>C'. finite C' \<and> vertex_cover E C' \<longrightarrow> card C \<le> 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 \<subseteq> E" "card C \<le> 2 * card M"
+    by(auto simp: invar_def inv_matching_def)
+
+  have opt: "card C \<le> 2 * card C'" if C': "finite C'" "vertex_cover E C'" for C'
+  proof -
+    note post(4)
+    also have "2 * card M \<le> 2 * card C'"
+    using card_matching_vertex_cover[OF C'(1) post(2,3) C'(2)] by simp
+    finally show "card C \<le> 2 * card C'" .
+  qed
+
+  show ?case using post(1) opt by auto
+qed
+
+end (* locale Graph *)
+
+subsection "Version for Hypergraphs"
+
+text \<open>Almost the same. We assume that the degree of every edge is bounded.\<close>
+
+locale Bounded_Hypergraph =
+  fixes E :: "'a set set"
+  fixes k :: nat
+  assumes finE: "finite E"
+  assumes edge_bnd: "e \<in> E \<Longrightarrow> finite e \<and> card e \<le> k"
+  assumes E1: "{} \<notin> E"
+begin
+
+definition "inv_matching C F M =
+  (matching M \<and> M \<subseteq> E \<and> card C \<le> k * card M \<and> (\<forall>e \<in> M. \<forall>f \<in> F. e \<inter> f = {}))"
+
+definition invar :: "'a set \<Rightarrow> 'a set set \<Rightarrow> bool" where
+"invar C F = (F \<subseteq> E \<and> vertex_cover (E-F) C \<and> finite C \<and> (\<exists>M. inv_matching C F M))"
+
+lemma invar_step:
+  assumes "F \<noteq> {}" "invar C F"
+  shows "invar (C \<union> some F) (F - {e' \<in> F. some F \<inter> e' \<noteq> {}})"
+proof -
+  from assms(2) obtain M where "F \<subseteq> E" and vc: "vertex_cover (E-F) C" and fC: "finite C"
+    and m: "matching M" "M \<subseteq> E" and card: "card C \<le> k * card M"
+    and disj: "\<forall>e \<in> M. \<forall>f \<in> F. e \<inter> f = {}"
+  by (auto simp: invar_def inv_matching_def)
+  let ?e = "SOME e. e \<in> F"
+  have "?e \<in> F" using \<open>F \<noteq> {}\<close> by (simp add: some_in_eq)
+  hence fe': "finite ?e" using \<open>F \<subseteq> E\<close> assms(2) edge_bnd by blast
+  have "?e \<notin> M" using E1 \<open>?e \<in> F\<close> disj \<open>F \<subseteq> E\<close> by fastforce
+  have card': "card (C \<union> ?e) \<le> k * card (insert ?e M)"
+    using \<open>?e \<in> F\<close> \<open>?e \<notin> M\<close> card_Un_le[of C ?e] \<open>F \<subseteq> E\<close> edge_bnd card finite_subset[OF m(2) finE]
+    by fastforce
+  let ?M = "M \<union> {?e}"
+  have vc': "vertex_cover (E - (F - {e' \<in> F. ?e \<inter> e' \<noteq> {}})) (C \<union> ?e)"
+    using vc by(auto simp: vertex_cover_def)
+  have m': "inv_matching (C \<union> ?e) (F - {e' \<in> F. ?e \<inter> e' \<noteq> {}}) ?M"
+    using m card' \<open>F \<subseteq> E\<close> \<open>?e \<in> F\<close> disj
+    by(auto simp: inv_matching_def Int_commute disjnt_def pairwise_insert)
+  show ?thesis using \<open>F \<subseteq> E\<close> 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 \<noteq> {}
+  INV {invar C F}
+  DO C := C \<union> some F;
+     F := F - {e' \<in> F. some F \<inter> e' \<noteq> {}}
+  OD
+  {vertex_cover E C \<and> (\<forall>C'. finite C' \<and> vertex_cover E C' \<longrightarrow> card C \<le> 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 \<subseteq> E" "card C \<le> k * card M"
+    by(auto simp: invar_def inv_matching_def)
+
+  have opt: "card C \<le> k * card C'" if C': "finite C'" "vertex_cover E C'" for C'
+  proof -
+    note post(4)
+    also have "k * card M \<le> k * card C'"
+    using card_matching_vertex_cover[OF C'(1) post(2,3) C'(2)] by simp
+    finally show "card C \<le> k * card C'" .
+  qed
+
+  show ?case using post(1) opt by auto
+qed
+
+end (* locale Bounded_Hypergraph *)
+
+end
diff --git a/thys/Approximation_Algorithms/ROOT b/thys/Approximation_Algorithms/ROOT
new file mode 100644
--- /dev/null
+++ b/thys/Approximation_Algorithms/ROOT
@@ -0,0 +1,15 @@
+chapter AFP
+
+session Approximation_Algorithms (AFP) = HOL +
+  options [timeout = 600]
+  sessions
+    "HOL-Library"
+    "HOL-Hoare"
+  theories
+    Approx_VC_Hoare
+    Approx_MIS_Hoare
+    Approx_LB_Hoare
+    Approx_BP_Hoare
+  document_files
+    "root.bib"
+    "root.tex"
diff --git a/thys/Approximation_Algorithms/document/root.bib b/thys/Approximation_Algorithms/document/root.bib
new file mode 100644
--- /dev/null
+++ b/thys/Approximation_Algorithms/document/root.bib
@@ -0,0 +1,41 @@
+@string{Springer="Springer"}
+@string{LNCS="LNCS"}
+
+@inproceedings{BerghammerM03,
+  author    = {Rudolf Berghammer and Markus M{\"{u}}ller{-}Olm},
+  title     = {Formal Development and Verification of Approximation Algorithms Using
+               Auxiliary Variables},
+  booktitle = {Logic Based Program Synthesis and Transformation, {LOPSTR} 2003},
+  pages     = {59--74},
+  year      = {2003},
+  crossref  = {DBLP:conf/lopstr/2003},
+  doi       = {10.1007/978-3-540-25938-1\_6},
+}
+
+@proceedings{DBLP:conf/lopstr/2003,
+  editor    = {Maurice Bruynooghe},
+  title     = {Logic Based Program Synthesis and Transformation, {LOPSTR} 2003},
+  series    = {LNCS},
+  volume    = {3018},
+  publisher = {Springer},
+  year      = {2004},
+}
+
+@article{BerghammerR03,
+  author    = {Rudolf Berghammer and Florian Reuter},
+  title     = {A linear approximation algorithm for bin packing with absolute approximation
+               factor 3/2},
+  journal   = {Sci. Comput. Program.},
+  volume    = {48},
+  number    = {1},
+  pages     = {67--80},
+  year      = {2003},
+  doi       = {10.1016/S0167-6423(03)00011-X},
+}
+
+@book{KleinbergT06,
+  author    = {Jon M. Kleinberg and {\'{E}}va Tardos},
+  title     = {Algorithm Design},
+  publisher = {Addison-Wesley},
+  year      = {2006},
+}
diff --git a/thys/Approximation_Algorithms/document/root.tex b/thys/Approximation_Algorithms/document/root.tex
new file mode 100644
--- /dev/null
+++ b/thys/Approximation_Algorithms/document/root.tex
@@ -0,0 +1,34 @@
+\documentclass[11pt,a4paper]{article}
+\usepackage{isabelle,isabellesym}
+
+% this should be the last package used
+\usepackage{pdfsetup}
+
+% urls in roman style, theory text in math-similar italics
+\urlstyle{rm}
+\isabellestyle{it}
+
+
+\begin{document}
+
+\title{Verified Approximation Algorithms}
+\author{Robin E{\ss}mann, Tobias Nipkow and Simon Robillard}
+\maketitle
+
+\begin{abstract}
+We present the first formal verifications of approximation algorithms
+for NP-complete optimization problems:
+vertex cover, independent set, load balancing, and bin packing.
+The proofs correct incompletnesses in existing proofs
+and improve the approximation ratio in one case.
+\end{abstract}
+
+\tableofcontents
+
+% include generated text of all theories
+\input{session}
+
+\bibliographystyle{abbrv}
+\bibliography{root}
+
+\end{document}
diff --git a/thys/ROOTS b/thys/ROOTS
--- a/thys/ROOTS
+++ b/thys/ROOTS
@@ -1,513 +1,514 @@
 AODV
 Auto2_HOL
 Auto2_Imperative_HOL
 AVL-Trees
 AWN
 Abortable_Linearizable_Modules
 Abs_Int_ITP2012
 Abstract-Hoare-Logics
 Abstract-Rewriting
 Abstract_Completeness
 Abstract_Soundness
 Adaptive_State_Counting
 Affine_Arithmetic
 Aggregation_Algebras
 Akra_Bazzi
 Algebraic_Numbers
 Algebraic_VCs
 Allen_Calculus
 Amortized_Complexity
 AnselmGod
 Applicative_Lifting
+Approximation_Algorithms
 Architectural_Design_Patterns
 Aristotles_Assertoric_Syllogistic
 ArrowImpossibilityGS
 AutoFocus-Stream
 Automatic_Refinement
 AxiomaticCategoryTheory
 BDD
 BNF_Operations
 Bell_Numbers_Spivey
 Berlekamp_Zassenhaus
 Bernoulli
 Bertrands_Postulate
 Bicategory
 BinarySearchTree
 Binding_Syntax_Theory
 Binomial-Heaps
 Binomial-Queues
 BNF_CC
 Bondy
 Boolean_Expression_Checkers
 Bounded_Deducibility_Security
 Buchi_Complementation
 Budan_Fourier
 Buffons_Needle
 Buildings
 BytecodeLogicJmlTypes
 C2KA_DistributedSystems
 CAVA_Automata
 CAVA_LTL_Modelchecker
 CCS
 CISC-Kernel
 CRDT
 CYK
 CakeML
 CakeML_Codegen
 Call_Arity
 Card_Equiv_Relations
 Card_Multisets
 Card_Number_Partitions
 Card_Partitions
 Cartan_FP
 Case_Labeling
 Catalan_Numbers
 Category
 Category2
 Category3
 Cauchy
 Cayley_Hamilton
 Certification_Monads
 Chord_Segments
 Circus
 Clean
 ClockSynchInst
 Closest_Pair_Points
 CofGroups
 Coinductive
 Coinductive_Languages
 Collections
 Comparison_Sort_Lower_Bound
 Compiling-Exceptions-Correctly
 Completeness
 Complete_Non_Orders
 Complx
 ComponentDependencies
 ConcurrentGC
 ConcurrentIMP
 Concurrent_Ref_Alg
 Concurrent_Revisions
 Consensus_Refined
 Constructive_Cryptography
 Constructor_Funs
 Containers
 CoreC++
 Core_DOM
 Count_Complex_Roots
 CryptHOL
 CryptoBasedCompositionalProperties
 DFS_Framework
 DPT-SAT-Solver
 DataRefinementIBP
 Datatype_Order_Generator
 Decl_Sem_Fun_PL
 Decreasing-Diagrams
 Decreasing-Diagrams-II
 Deep_Learning
 Density_Compiler
 Dependent_SIFUM_Refinement
 Dependent_SIFUM_Type_Systems
 Depth-First-Search
 Derangements
 Deriving
 Descartes_Sign_Rule
 Dict_Construction
 Differential_Dynamic_Logic
 Differential_Game_Logic
 Dijkstra_Shortest_Path
 Diophantine_Eqns_Lin_Hom
 Dirichlet_L
 Dirichlet_Series
 Discrete_Summation
 DiscretePricing
 DiskPaxos
 DynamicArchitectures
 Dynamic_Tables
 E_Transcendental
 Echelon_Form
 EdmondsKarp_Maxflow
 Efficient-Mergesort
 Elliptic_Curves_Group_Law
 Encodability_Process_Calculi
 Epistemic_Logic
 Ergodic_Theory
 Error_Function
 Euler_MacLaurin
 Euler_Partition
 Example-Submission
 Factored_Transition_System_Bounding
 Farkas
 FFT
 FLP
 FOL-Fitting
 FOL_Harrison
 FOL_Seq_Calc1
 Falling_Factorial_Sum
 FeatherweightJava
 Featherweight_OCL
 Fermat3_4
 FileRefinement
 FinFun
 Finger-Trees
 Finite_Automata_HF
 First_Order_Terms
 First_Welfare_Theorem
 Fishburn_Impossibility
 Fisher_Yates
 Flow_Networks
 Floyd_Warshall
 Flyspeck-Tame
 FocusStreamsCaseStudies
 Formal_SSA
 Formula_Derivatives
 Fourier
 Free-Boolean-Algebra
 Free-Groups
 FunWithFunctions
 FunWithTilings
 Functional-Automata
 Functional_Ordered_Resolution_Prover
 GPU_Kernel_PL
 Gabow_SCC
 Game_Based_Crypto
 Gauss-Jordan-Elim-Fun
 Gauss_Jordan
 Gauss_Sums
 GenClock
 General-Triangle
 Generalized_Counting_Sort
 Generic_Deriving
 Generic_Join
 GewirthPGCProof
 Girth_Chromatic
 GoedelGod
 GraphMarkingIBP
 Graph_Saturation
 Graph_Theory
 Green
 Groebner_Bases
 Groebner_Macaulay
 Gromov_Hyperbolicity
 Group-Ring-Module
 HOL-CSP
 HOLCF-Prelude
 HRB-Slicing
 Heard_Of
 HereditarilyFinite
 Hermite
 Hidden_Markov_Models
 Higher_Order_Terms
 Hoare_Time
 HotelKeyCards
 Huffman
 Hybrid_Logic
 Hybrid_Multi_Lane_Spatial_Logic
 Hybrid_Systems_VCs
 HyperCTL
 IEEE_Floating_Point
 IMAP-CRDT
 IMO2019
 IMP2
 IMP2_Binary_Heap
 IP_Addresses
 Imperative_Insertion_Sort
 Impossible_Geometry
 Incompleteness
 Incredible_Proof_Machine
 Inductive_Confidentiality
 InfPathElimination
 InformationFlowSlicing
 InformationFlowSlicing_Inter
 Integration
 Interval_Arithmetic_Word32
 Iptables_Semantics
 Irrationality_J_Hancl
 Isabelle_C
 Isabelle_Meta_Model
 Jacobson_Basic_Algebra
 Jinja
 JinjaThreads
 JiveDataStoreModel
 Jordan_Hoelder
 Jordan_Normal_Form
 KAD
 KAT_and_DRA
 KBPs
 KD_Tree
 Key_Agreement_Strong_Adversaries
 Kleene_Algebra
 Knot_Theory
 Knuth_Morris_Pratt
 Koenigsberg_Friendship
 Kruskal
 Kuratowski_Closure_Complement
 LLL_Basis_Reduction
 LLL_Factorization
 LOFT
 LTL
 LTL_to_DRA
 LTL_to_GBA
 LTL_Master_Theorem
 Lam-ml-Normalization
 LambdaAuth
 LambdaMu
 Lambda_Free_KBOs
 Lambda_Free_RPOs
 Landau_Symbols
 Laplace_Transform
 Latin_Square
 LatticeProperties
 Lambda_Free_EPO
 Launchbury
 Lazy-Lists-II
 Lazy_Case
 Lehmer
 Lifting_Definition_Option
 LightweightJava
 LinearQuantifierElim
 Linear_Inequalities
 Linear_Programming
 Linear_Recurrences
 Liouville_Numbers
 List-Index
 List-Infinite
 List_Interleaving
 List_Inversions
 List_Update
 LocalLexing
 Localization_Ring
 Locally-Nameless-Sigma
 Lowe_Ontological_Argument
 Lower_Semicontinuous
 Lp
 MFMC_Countable
 MSO_Regex_Equivalence
 Markov_Models
 Marriage
 Mason_Stothers
 Matrix
 Matrix_Tensor
 Matroids
 Max-Card-Matching
 Median_Of_Medians_Selection
 Menger
 MFOTL_Monitor
 MiniML
 Minimal_SSA
 Minkowskis_Theorem
 Minsky_Machines
 Modal_Logics_for_NTS
 Modular_Assembly_Kit_Security
 Monad_Memo_DP
 Monad_Normalisation
 MonoBoolTranAlgebra
 MonoidalCategory
 Monomorphic_Monad
 MuchAdoAboutTwo
 Multirelations
 Multi_Party_Computation
 Myhill-Nerode
 Name_Carrying_Type_Inference
 Nat-Interval-Logic
 Native_Word
 Nested_Multisets_Ordinals
 Network_Security_Policy_Verification
 Neumann_Morgenstern_Utility
 No_FTL_observers
 Nominal2
 Noninterference_CSP
 Noninterference_Concurrent_Composition
 Noninterference_Generic_Unwinding
 Noninterference_Inductive_Unwinding
 Noninterference_Ipurge_Unwinding
 Noninterference_Sequential_Composition
 NormByEval
 Nullstellensatz
 Octonions
 Open_Induction
 OpSets
 Optics
 Optimal_BST
 Orbit_Stabiliser
 Order_Lattice_Props
 Ordered_Resolution_Prover
 Ordinal
 Ordinals_and_Cardinals
 Ordinary_Differential_Equations
 PCF
 PLM
 Pell
 POPLmark-deBruijn
 PSemigroupsConvolution
 Pairing_Heap
 Paraconsistency
 Parity_Game
 Partial_Function_MR
 Partial_Order_Reduction
 Password_Authentication_Protocol
 Perfect-Number-Thm
 Perron_Frobenius
 Pi_Calculus
 Pi_Transcendental
 Planarity_Certificates
 Polynomial_Factorization
 Polynomial_Interpolation
 Polynomials
 Poincare_Bendixson
 Pop_Refinement
 Posix-Lexing
 Possibilistic_Noninterference
 Pratt_Certificate
 Presburger-Automata
 Prim_Dijkstra_Simple
 Prime_Distribution_Elementary
 Prime_Harmonic_Series
 Prime_Number_Theorem
 Priority_Queue_Braun
 Priority_Search_Trees
 Probabilistic_Noninterference
 Probabilistic_Prime_Tests
 Probabilistic_System_Zoo
 Probabilistic_Timed_Automata
 Probabilistic_While
 Projective_Geometry
 Program-Conflict-Analysis
 Promela
 Proof_Strategy_Language
 PropResPI
 Propositional_Proof_Systems
 Prpu_Maxflow
 PseudoHoops
 Psi_Calculi
 Ptolemys_Theorem
 QHLProver
 QR_Decomposition
 Quantales
 Quaternions
 Quick_Sort_Cost
 RIPEMD-160-SPARK
 ROBDD
 RSAPSS
 Ramsey-Infinite
 Random_BSTs
 Randomised_BSTs
 Random_Graph_Subgraph_Threshold
 Randomised_Social_Choice
 Rank_Nullity_Theorem
 Real_Impl
 Recursion-Theory-I
 Refine_Imperative_HOL
 Refine_Monadic
 RefinementReactive
 Regex_Equivalence
 Regular-Sets
 Regular_Algebras
 Relation_Algebra
 Rep_Fin_Groups
 Residuated_Lattices
 Resolution_FOL
 Rewriting_Z
 Ribbon_Proofs
 Robbins-Conjecture
 Root_Balanced_Tree
 Routing
 Roy_Floyd_Warshall
 Safe_OCL
 SATSolverVerification
 SDS_Impossibility
 SIFPL
 SIFUM_Type_Systems
 SPARCv8
 Secondary_Sylow
 Security_Protocol_Refinement
 Selection_Heap_Sort
 SenSocialChoice
 Separata
 Separation_Algebra
 Separation_Logic_Imperative_HOL
 SequentInvertibility
 Shivers-CFA
 ShortestPath
 Show
 Sigma_Commit_Crypto
 Signature_Groebner
 Simpl
 Simple_Firewall
 Simplex
 Skew_Heap
 Skip_Lists
 Slicing
 Smooth_Manifolds
 Sort_Encodings
 Source_Coding_Theorem
 Special_Function_Bounds
 Splay_Tree
 Sqrt_Babylonian
 Stable_Matching
 Statecharts
 Stellar_Quorums
 Stern_Brocot
 Stewart_Apollonius
 Stirling_Formula
 Stochastic_Matrices
 Stone_Algebras
 Stone_Kleene_Relation_Algebras
 Stone_Relation_Algebras
 Store_Buffer_Reduction
 Stream-Fusion
 Stream_Fusion_Code
 Strong_Security
 Sturm_Sequences
 Sturm_Tarski
 Stuttering_Equivalence
 Subresultants
 SumSquares
 SuperCalc
 Surprise_Paradox
 Symmetric_Polynomials
 Szpilrajn
 TESL_Language
 TLA
 Tail_Recursive_Functions
 Tarskis_Geometry
 Taylor_Models
 Timed_Automata
 Topology
 TortoiseHare
 Transcendence_Series_Hancl_Rucki
 Transformer_Semantics
 Transition_Systems_and_Automata
 Transitive-Closure
 Transitive-Closure-II
 Treaps
 Tree-Automata
 Tree_Decomposition
 Triangle
 Trie
 Twelvefold_Way
 Tycon
 Types_Tableaus_and_Goedels_God
 Universal_Turing_Machine
 UPF
 UPF_Firewall
 UpDown_Scheme
 UTP
 Valuation
 VectorSpace
 Verified-Prover
 VerifyThis2018
 VerifyThis2019
 Vickrey_Clarke_Groves
 VolpanoSmith
 WHATandWHERE_Security
 WebAssembly
 Weight_Balanced_Trees
 Well_Quasi_Orders
 Winding_Number_Eval
 Word_Lib
 WorkerWrapper
 XML
 Zeta_Function
 Zeta_3_Irrational
 ZFC_in_HOL
 pGCL