# Theory Approx_VC_Hoare

section "Vertex Cover"

theory Approx_VC_Hoare
imports "HOL-Hoare.Hoare_Logic"
begin

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

subsection "Graph"

text â€¹A graph is simply a set of edges, where an edge is a 2-element set.â€º

definition vertex_cover :: "'a set set â‡’ 'a set â‡’ bool" where
"vertex_cover E C = (âˆ€e âˆˆ E. e âˆ© C â‰  {})"

abbreviation matching :: "'a set set â‡’ bool" where
"matching M â‰¡ pairwise disjnt M"

lemma card_matching_vertex_cover:
"âŸ¦ finite C;  matching M;  M âŠ† E;  vertex_cover E C âŸ§ âŸ¹ card M â‰¤ card C"
apply(erule card_le_if_inj_on_rel[where r = "Î»e v. v âˆˆ e"])
apply (meson disjnt_def disjnt_iff vertex_cover_def subsetCE)
by (meson disjnt_iff pairwise_def)

subsection "The Approximation Algorithm"

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

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

text â€¹Convenient notation for choosing an arbitrary element from a set:â€º
abbreviation "some A â‰¡ SOME x. x âˆˆ A"

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

text â€¹The invariant:â€º

definition "inv_matching C F M =
(matching M âˆ§ M âŠ† E âˆ§ card C â‰¤ 2 * card M âˆ§ (âˆ€e âˆˆ M. âˆ€f âˆˆ F. e âˆ© f = {}))"

definition invar :: "'a set â‡’ 'a set set â‡’ bool" where
"invar C F = (F âŠ† E âˆ§ vertex_cover (E-F) C âˆ§ finite C âˆ§ (âˆƒM. inv_matching C F M))"

text â€¹Preservation of the invariant by the loop body:â€º

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

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

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

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

end (* locale Graph *)

subsection "Version for Hypergraphs"

text â€¹Almost the same. We assume that the degree of every edge is bounded.â€º

locale Bounded_Hypergraph =
fixes E :: "'a set set"
fixes k :: nat
assumes finE: "finite E"
assumes edge_bnd: "e âˆˆ E âŸ¹ finite e âˆ§ card e â‰¤ k"
assumes E1: "{} âˆ‰ E"
begin

definition "inv_matching C F M =
(matching M âˆ§ M âŠ† E âˆ§ card C â‰¤ k * card M âˆ§ (âˆ€e âˆˆ M. âˆ€f âˆˆ F. e âˆ© f = {}))"

definition invar :: "'a set â‡’ 'a set set â‡’ bool" where
"invar C F = (F âŠ† E âˆ§ vertex_cover (E-F) C âˆ§ finite C âˆ§ (âˆƒM. inv_matching C F M))"

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

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

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

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

end (* locale Bounded_Hypergraph *)

end


# Theory Approx_SC_Hoare

section â€¹Set Coverâ€º

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

text â€¹This is a formalization of the set cover algorithm and proof
in the book by Kleinberg and Tardos \cite{KleinbergT06}.â€º

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

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

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

lemma S_subset: "âˆ€i âˆˆ {1..m}. S i âŠ† U"
using U_def by blast

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

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

definition sc :: "nat set â‡’ 'a set â‡’ bool" where
"sc C X âŸ· C âŠ† {1..m} âˆ§ (â‹ƒi âˆˆ C. S i) = X"

definition cost :: "'a set â‡’ nat â‡’ real" where
"cost R i = w i / card (S i âˆ© R)"

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

text â€¹â€¹cost R i = 0â€º if â€¹card (S i âˆ© R) = 0â€º! Needs to be accounted for separately in â€¹min_argâ€º.â€º
fun min_arg :: "'a set â‡’ nat â‡’ nat" where
"min_arg R 0 = 1"
| "min_arg R (Suc x) =
(let j = min_arg R x
in if S j âˆ© R = {} âˆ¨ (S (Suc x) âˆ© R â‰  {} âˆ§ cost R (Suc x) < cost R j) then (Suc x) else j)"

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

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

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

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

definition c_exists :: "nat set â‡’ 'a set â‡’ bool" where
"c_exists C R = (âˆƒc. sum w C = sum c (U - R) âˆ§ (âˆ€i. 0 â‰¤ c i)
âˆ§ (âˆ€k âˆˆ {1..m}. sum c (S k âˆ© (U - R))
â‰¤ (âˆ‘j = card (S k âˆ© R) + 1..card (S k). inverse j) * w k))"

definition inv :: "nat set â‡’ 'a set â‡’ bool" where
"inv C R âŸ· sc C (U - R) âˆ§ R âŠ† U âˆ§ c_exists C R"

lemma invI:
assumes "sc C (U - R)" "R âŠ† U"
"âˆƒc. sum w C = sum c (U - R) âˆ§ (âˆ€i. 0 â‰¤ c i)
âˆ§ (âˆ€k âˆˆ {1..m}. sum c (S k âˆ© (U - R))
â‰¤ (âˆ‘j = card (S k âˆ© R) + 1..card (S k). inverse j) * w k)"
shows "inv C R" using assms by (auto simp: inv_def c_exists_def)

lemma invD:
assumes "inv C R"
shows "sc C (U - R)" "R âŠ† U"
"âˆƒc. sum w C = sum c (U - R) âˆ§ (âˆ€i. 0 â‰¤ c i)
âˆ§ (âˆ€k âˆˆ {1..m}. sum c (S k âˆ© (U - R))
â‰¤ (âˆ‘j = card (S k âˆ© R) + 1..card (S k). inverse j) * w k)"
using assms by (auto simp: inv_def c_exists_def)

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

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

â€• â€¹Proving properties of cost functionâ€º
from hyp(3) obtain c where "sum w C = sum c (U - R)" "âˆ€i. 0 â‰¤ c i" and
SUM: "âˆ€kâˆˆ{1..m}. sum c (S k âˆ© (U - R))
â‰¤ (âˆ‘j = card (S k âˆ© R) + 1..card (S k). inverse j) * w k" by blast
let ?c = "(Î»x. if x âˆˆ S i âˆ© R then cost R i else c x)"

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

have 2: "âˆ€i. 0 â‰¤ ?c i" using â€¹âˆ€i. 0 â‰¤ c iâ€º cost_nonneg by simp

â€• â€¹Proof of Lemma 11.10â€º
have 3: "âˆ€kâˆˆ{1..m}. sum ?c (S k âˆ© (U - (R - S i)))
â‰¤ (âˆ‘j = card (S k âˆ© (R - S i)) + 1..card (S k). inverse j) * w k"
proof
fix k assume "k âˆˆ {1..m}"
let ?rem = "S k âˆ© R" â€• â€¹Remaining elements to be coveredâ€º
let ?add = "S k âˆ© S i âˆ© R" â€• â€¹Elements that will be covered in this stepâ€º
let ?cov = "S k âˆ© (U - R)" â€• â€¹Covered elementsâ€º

â€• â€¹Transforming left and right sidesâ€º
have "sum ?c (S k âˆ© (U - (R - S i))) = sum ?c (S k âˆ© (U - R âˆª (S i âˆ© R)))"
unfolding U_split ..
also have "... = sum ?c (?cov âˆª ?add)"
by (simp add: Int_Un_distrib Int_assoc)
also have "... = sum ?c ?cov + sum ?c ?add"
by (rule sum.union_disjoint) (insert S_finite â€¹k âˆˆ _â€º, auto)
finally have lhs:
"sum ?c (S k âˆ© (U - (R - S i))) = sum ?c ?cov + sum ?c ?add" .
have "S k âˆ© (R - S i) = ?rem - ?add" by blast
then have "card (S k âˆ© (R - S i)) = card (?rem - ?add)" by simp
also have "... = card ?rem - card ?add"
using S_finite â€¹k âˆˆ _â€º by (auto intro: card_Diff_subset)
finally have rhs:
"card (S k âˆ© (R - S i)) + 1 = card ?rem - card ?add + 1" by simp

â€• â€¹The apparent complexity of the remaining proof is deceiving. Much of this is just about
convincing Isabelle that these sum transformations are allowed.â€º
have "sum ?c ?add = card ?add * cost R i" by simp
also have "... â‰¤ card ?add * cost R k"
proof (cases "?rem = {}")
case True
then have "card ?add = 0" by (auto simp: card_eq_0_iff)
then show ?thesis by simp
next
case False
from min_correct[OF â€¹k âˆˆ _â€º this] have "cost R i â‰¤ cost R k" by simp
then show ?thesis by (simp add: mult_left_mono)
qed
also have "... = card ?add * inverse (card ?rem) * w k"
by (simp add: cost_def divide_inverse_commute)
also have "... = (âˆ‘j âˆˆ {card ?rem - card ?add + 1 .. card ?rem}. inverse (card ?rem)) * w k"
proof -
have "card ?add â‰¤ card ?rem"
using S_finite â€¹k âˆˆ _â€º by (blast intro: card_mono)
then show ?thesis by (simp add: sum_distrib_left)
qed
also have "... â‰¤ (âˆ‘j âˆˆ {card ?rem - card ?add + 1 .. card ?rem}. inverse j) * w k"
proof -
have "âˆ€j âˆˆ {card ?rem - card ?add + 1 .. card ?rem}. inverse (card ?rem) â‰¤ inverse j"
by force
then have "(âˆ‘j âˆˆ {card ?rem - card ?add + 1 .. card ?rem}. inverse (card ?rem))
â‰¤ (âˆ‘j âˆˆ {card ?rem - card ?add + 1 .. card ?rem}. inverse j)"
by (blast intro: sum_mono)
with w_nonneg show ?thesis by (blast intro: mult_right_mono)
qed
finally have "sum ?c ?add
â‰¤ (âˆ‘j âˆˆ {card ?rem - card ?add + 1 .. card ?rem}. inverse j) * w k" .
moreover from SUM have "sum ?c ?cov
â‰¤ (âˆ‘j âˆˆ {card ?rem + 1 .. card (S k)}. inverse j) * w k"
using â€¹k âˆˆ {1..m}â€º by simp
ultimately have "sum ?c (S k âˆ© (U - (R - S i)))
â‰¤ ((âˆ‘j âˆˆ {card ?rem - card ?add + 1 .. card ?rem}. inverse j) +
(âˆ‘j âˆˆ {card ?rem + 1 .. card (S k)}. inverse j)) * w k"
unfolding lhs by argo
also have "... = (âˆ‘j âˆˆ {card ?rem - card ?add + 1 .. card (S k)}. inverse j) * w k"
proof -
have sum_split: "b âˆˆ {a .. c} âŸ¹ sum f {a .. c} = sum f {a .. b} + sum f {Suc b .. c}"
for f :: "nat â‡’ real" and a b c :: nat
proof -
assume "b âˆˆ {a .. c}"
then have "{a .. b} âˆª {Suc b .. c} = {a .. c}" by force
moreover have "{a .. b} âˆ© {Suc b .. c} = {}"
using â€¹b âˆˆ {a .. c}â€º by auto
ultimately show ?thesis by (metis finite_atLeastAtMost sum.union_disjoint)
qed

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

from 1 2 3 show ?case by blast
qed
qed

lemma cover_sum:
fixes c :: "'a â‡’ real"
assumes "sc C V" "âˆ€i. 0 â‰¤ c i"
shows "sum c V â‰¤ (âˆ‘i âˆˆ C. sum c (S i))"
proof -
from assms(1) have "finite C" by (auto simp: sc_def finite_subset)
then show ?thesis using assms(1)
proof (induction C arbitrary: V rule: finite_induct)
case (insert i C)
have V_split: "(â‹ƒ (S  insert i C)) = (â‹ƒ (S  C)) âˆª S i" by auto
have finite: "finite (â‹ƒ (S  C))" "finite (S i)"
using insert S_finite by (auto simp: sc_def)

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

abbreviation H :: "nat â‡’ real" where "H â‰¡ harm"

definition d_star :: nat ("dâ‡§*") where "dâ‡§* â‰¡ Max (card  (S  {1..m}))"

lemma set_cover_bound:
assumes "inv C {}" "sc C' U"
shows "sum w C â‰¤ H dâ‡§* * sum w C'"
proof -
from invD(3)[OF assms(1)] obtain c where
"sum w C = sum c U" "âˆ€i. 0 â‰¤ c i" and H_bound:
"âˆ€k âˆˆ {1..m}. sum c (S k) â‰¤ H (card (S k)) * w k" â€• â€¹Lemma 11.10â€º
by (auto simp: harm_def Int_absorb2 S_subset)

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

have "sum w C = sum c U" by fact â€• â€¹Lemma 11.9â€º
also have "... â‰¤ (âˆ‘i âˆˆ C'. sum c (S i))" by (rule cover_sum[OF assms(2)]) fact
also have "... â‰¤ H dâ‡§* * sum w C'" by fact
finally show ?thesis .
qed

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

end (* Set Cover *)

end (* Theory *)


# Theory Approx_MIS_Hoare

section "Independent Set"

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

text â€¹The algorithm is classical, the proofs are inspired by the ones
by Berghammer and M\"uller-Olm \cite{BerghammerM03}.
In particular the approximation ratio is improved from â€¹Î”+1â€º to â€¹Î”â€º.â€º

subsection "Graph"

text â€¹A set set is simply a set of edges, where an edge is a 2-element set.â€º

definition independent_vertices :: "'a set set â‡’ 'a set â‡’ bool" where
"independent_vertices E S âŸ· S âŠ† â‹ƒE âˆ§ (âˆ€v1 v2. v1 âˆˆ S âˆ§ v2 âˆˆ S âŸ¶ {v1, v2} âˆ‰ E)"

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

fun vertices :: "'a set set â‡’ 'a set" where
"vertices G = â‹ƒG"

abbreviation V :: "'a set" where
"V â‰¡ vertices E"

definition approximation_miv :: "nat â‡’ 'a set â‡’ bool" where
"approximation_miv n S âŸ· independent_vertices E S âˆ§ (âˆ€S'. independent_vertices E S' âŸ¶ card S' â‰¤ card S * n)"

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

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

abbreviation Î” :: nat where
"Î” â‰¡ Max{degree_vertex u|u. u âˆˆ V}"

lemma finite_edges: "e âˆˆ E âŸ¹ finite e"
using card_ge_0_finite and edges2 by force

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

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

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

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

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

lemma Î”_max_degree: "u âˆˆ V âŸ¹ degree_vertex u â‰¤ Î”"
proof -
assume H: "u âˆˆ V"
have "finite {degree_vertex u |u. u âˆˆ V}"
by (metis finite_V finite_imageI Setcompr_eq_image)
with H show "degree_vertex u â‰¤ Î”" using Max_ge by auto
qed

subsection â€¹Wei's algorithm: â€¹(Î”+1)â€º-approximationâ€º

text â€¹The 'functional' part of the invariant, used to prove that the algorithm produces an independent set of vertices.â€º

definition inv_iv :: "'a set â‡’ 'a set â‡’ bool" where
"inv_iv S X âŸ· independent_vertices E S
âˆ§ X âŠ† V
âˆ§ (âˆ€v1 âˆˆ (V - X). âˆ€v2 âˆˆ S. {v1, v2} âˆ‰ E)
âˆ§ S âŠ† X"

text â€¹Strenghten the invariant with an approximation ratio â€¹râ€º:â€º

definition inv_approx :: "'a set â‡’ 'a set â‡’ nat â‡’ bool" where
"inv_approx S X r âŸ· inv_iv S X âˆ§ card X â‰¤ card S * r"

text â€¹Preservation of the functional invariant:â€º

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

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

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

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

subsection â€¹Wei's algorithm: â€¹Î”â€º-approximationâ€º

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

definition inv_partition :: "'a set â‡’ 'a set â‡’ 'a set set â‡’ bool" where
"inv_partition S X P âŸ· inv_iv S X
âˆ§ â‹ƒP = X
âˆ§ (âˆ€p âˆˆ P. âˆƒs âˆˆ V. p = {s} âˆª neighbors s)
âˆ§ card P = card S
âˆ§ finite P"

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

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

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

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

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

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

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

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

definition vertex_heuristic :: "'a set â‡’ 'a â‡’ bool" where
"vertex_heuristic X v = (âˆ€u âˆˆ V - X. card (neighbors v - X) â‰¤ card (neighbors u - X))"

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

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

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

end
end

# Theory Approx_LB_Hoare

section â€¹Load Balancingâ€º

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

text â€¹This is a formalization of the load balancing algorithms and proofs
in the book by Kleinberg and Tardos \cite{KleinbergT06}.â€º

hide_const (open) sorted

(* TODO: mv *)

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

lemma Max_const[simp]: "âŸ¦ finite A; A â‰  {} âŸ§ âŸ¹ Max ((Î»_. c)  A) = c"
using Max_in image_is_empty by blast

abbreviation Maxâ‡©0 :: "nat set â‡’ nat" where
"Maxâ‡©0 N â‰¡ (if N={} then 0 else Max N)"

fun f_Maxâ‡©0 :: "(nat â‡’ nat) â‡’ nat â‡’ nat" where
"f_Maxâ‡©0 f 0 = 0"
| "f_Maxâ‡©0 f (Suc x) = max (f (Suc x)) (f_Maxâ‡©0 f x)"

lemma f_Maxâ‡©0_equiv: "f_Maxâ‡©0 f n = Maxâ‡©0 (f  {1..n})"
by (induction n) (auto simp: not_le atLeastAtMostSuc_conv)

"âˆ€x âˆˆ {1..m}. T x â‰¤ f_Maxâ‡©0 T m"
"m > 0 âŸ¹ âˆƒx âˆˆ {1..m}. T x = f_Maxâ‡©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 â€¹m = 0â€º) (auto simp: max_def)
done

"y â‰¤ T x âŸ¹ f_Maxâ‡©0 (T (x := y)) m â‰¤ f_Maxâ‡©0 T m"
"T x â‰¤ y âŸ¹ f_Maxâ‡©0 T m â‰¤ f_Maxâ‡©0 (T (x := y)) m"
by (induction m) auto

"x âˆ‰ {1..k} âŸ¹ f_Maxâ‡©0 (T (x := y)) k = f_Maxâ‡©0 T k"
by (induction k) auto

assumes "x âˆˆ {1..m}" "T x â‰¤ y"
shows "f_Maxâ‡©0 (T (x := y)) m = max y (f_Maxâ‡©0 T m)"
using assms by (induction m) auto

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

subsection â€¹Formalization of a Correct Load Balancingâ€º

subsubsection â€¹Definitionâ€º

definition lb :: "(nat â‡’ nat) â‡’ (nat â‡’ nat set) â‡’ nat â‡’ bool" where
"lb T A j = ((âˆ€x âˆˆ {1..m}. âˆ€y âˆˆ {1..m}. x â‰  y âŸ¶ A x âˆ© A y = {}) â€• â€¹No job is assigned to more than one machineâ€º
âˆ§ (â‹ƒx âˆˆ {1..m}. A x) = {1..j} â€• â€¹Every job is assignedâ€º
âˆ§ (âˆ€x âˆˆ {1..m}. (âˆ‘j âˆˆ A x. t j) = T x) â€• â€¹The processing times sum up to the correct loadâ€º)"

abbreviation makespan :: "(nat â‡’ nat) â‡’ nat" where
"makespan T â‰¡ f_Maxâ‡©0 T m"

lemma makespan_def': "makespan T = Max (T  {1..m})"
(*
lemma makespan_correct:
"âˆ€x âˆˆ {1..m}. T x â‰¤ makespan T m"
"m > 0 âŸ¹ âˆƒx âˆˆ {1..m}. T x = makespan T m"
apply (induction m)
apply simp_all
apply (metis atLeastAtMost_iff le_Suc_eq max.cobounded1 max.coboundedI2)
subgoal for m by (cases â€¹m = 0â€º) (auto simp: max_def)
done

lemma no_machines_lb_iff_no_jobs: "lb T A j 0 âŸ· j = 0"
unfolding lb_def by auto

lemma machines_if_jobs: "âŸ¦ lb T A j m; j > 0 âŸ§ âŸ¹ m > 0"
using no_machines_lb_iff_no_jobs by (cases m) auto
*)

lemma makespan_correct:
"âˆ€x âˆˆ {1..m}. T x â‰¤ makespan T"
"âˆƒx âˆˆ {1..m}. T x = makespan T"
using f_Maxâ‡©0_correct m_gt_0 by auto

lemma lbE:
assumes "lb T A j"
shows "âˆ€x âˆˆ {1..m}. âˆ€y âˆˆ {1..m}. x â‰  y âŸ¶ A x âˆ© A y = {}"
"(â‹ƒx âˆˆ {1..m}. A x) = {1..j}"
"âˆ€x âˆˆ {1..m}. (âˆ‘y âˆˆ A x. t y) = T x"
using assms unfolding lb_def by blast+

lemma lbI:
assumes "âˆ€x âˆˆ {1..m}. âˆ€y âˆˆ {1..m}. x â‰  y âŸ¶ A x âˆ© A y = {}"
"(â‹ƒx âˆˆ {1..m}. A x) = {1..j}"
"âˆ€x âˆˆ {1..m}. (âˆ‘y âˆˆ A x. t y) = T x"
shows "lb T A j" using assms unfolding lb_def by blast

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

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

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

subsubsection â€¹Lower Bounds for the Makespanâ€º

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

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

text â€¹The makespan over â€¹jâ€º jobs is a lower bound for the makespan of any correct load balancing for â€¹jâ€º jobs.â€º
lemma max_job_lower_bound_makespan:
assumes "lb T A j"
shows "Maxâ‡©0 (t  {1..j}) â‰¤ makespan T"
using job_lower_bound_makespan[OF assms] by fastforce

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

subsection â€¹The Greedy Approximation Algorithmâ€º

text â€¹This function will perform a linear scan from â€¹k âˆˆ {1..m}â€º and return the index of the machine with minimum load assuming â€¹m > 0â€ºâ€º
fun minâ‡©k :: "(nat â‡’ nat) â‡’ nat â‡’ nat" where
"minâ‡©k T 0 = 1"
| "minâ‡©k T (Suc x) =
(let k = minâ‡©k T x
in if T (Suc x) < T k then (Suc x) else k)"

lemma min_correct:
"âˆ€x âˆˆ {1..m}. T (minâ‡©k T m) â‰¤ T x"
by (induction m) (auto simp: Let_def le_Suc_eq, force)

lemma min_in_range:
"k > 0 âŸ¹ (minâ‡©k T k) âˆˆ {1..k}"
by (induction k) (auto simp: Let_def, force+)

assumes "lb T A j" "x âˆˆ {1..m}"
shows "lb (T (x := T x + t (Suc j))) (A (x := A x âˆª {Suc j})) (Suc j)"
(is â€¹lb ?T ?A _â€º)
proof -
note lbrules = lbE[OF assms(1)]

â€• â€¹Rule 1: @{term ?A} pairwise disjointâ€º
have NOTIN: "âˆ€i âˆˆ {1..m}. Suc j âˆ‰ A i" using lbrules(2) assms(2) by force
with lbrules(1) have "âˆ€i âˆˆ {1..m}. i â‰  x âŸ¶ A i âˆ© (A x âˆª {Suc j}) = {}"
using assms(2) by blast
then have 1: "âˆ€x âˆˆ {1..m}. âˆ€y âˆˆ {1..m}. x â‰  y âŸ¶ ?A x âˆ© ?A y = {}"
using lbrules(1) by simp

â€• â€¹Rule 2: @{term ?A} contains all jobsâ€º
have "(â‹ƒy âˆˆ {1..m}. ?A y) = (â‹ƒy âˆˆ {1..m}. A y) âˆª {Suc j}"
using UNION_fun_upd assms(2) by auto
also have "... = {1..Suc j}" unfolding lbrules(2) by auto
finally have 2: "(â‹ƒy âˆˆ {1..m}. ?A y) = {1..Suc j}" .

â€• â€¹Rule 3: @{term ?A} sums to @{term ?T}â€º
have "(âˆ‘i âˆˆ ?A x. t i) = (âˆ‘i âˆˆ A x âˆª {Suc j}. t i)" by simp
moreover have "A x âˆ© {Suc j} = {}" using NOTIN assms(2) by blast
moreover have "finite (A x)" "finite {Suc j}" using assms by simp+
ultimately have "(âˆ‘i âˆˆ ?A x. t i) = (âˆ‘i âˆˆ A x. t i) + (âˆ‘i âˆˆ {Suc j}. t i)"
using sum.union_disjoint by simp
also have "... = T x + t (Suc j)" using lbrules(3) assms(2) by simp
finally have "(âˆ‘i âˆˆ ?A x. t i) = ?T x" by simp
then have 3: "âˆ€i âˆˆ {1..m}. (âˆ‘j âˆˆ ?A i. t j) = ?T i"
using lbrules(3) assms(2) by simp

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

lemma makespan_mono:
"y â‰¤ T x âŸ¹ makespan (T (x := y)) â‰¤ makespan T"
"T x â‰¤ y âŸ¹ makespan T â‰¤ makespan (T (x := y))"
using f_Maxâ‡©0_mono by auto

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

â€• â€¹Rule 1: @{term ?A} pairwise disjointâ€º
from lbrules(1) have "âˆ€i âˆˆ {1..m}. i â‰  x âŸ¶ A i âˆ© (A x - {Suc j}) = {}"
using x_def(1) by blast
then have 1: "âˆ€x âˆˆ {1..m}. âˆ€y âˆˆ {1..m}. x â‰  y âŸ¶ ?A x âˆ© ?A y = {}"
using lbrules(1) by auto

â€• â€¹Rule 2: @{term ?A} contains all jobsâ€º
have NOTIN: "âˆ€i âˆˆ {1..m}. i â‰  x âŸ¶ Suc j âˆ‰ A i" using lbrules(1) x_def by blast
then have "(â‹ƒy âˆˆ {1..m}. ?A y) = (â‹ƒy âˆˆ {1..m}. A y) - {Suc j}"
using UNION_fun_upd x_def by auto
also have "... = {1..j}" unfolding lbrules(2) by auto
finally have 2: "(â‹ƒy âˆˆ {1..m}. ?A y) = {1..j}" .

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

â€• â€¹@{term makespan} is not largerâ€º
have "lb ?T ?A j âˆ§ makespan ?T â‰¤ makespan T"
using lbI[OF 1 2 3] makespan_mono(1) by force
then show ?thesis by blast
qed

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

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

lemma min_avg: "m * T (minâ‡©k T m) â‰¤ (âˆ‘i âˆˆ {1..m}. T i)"
(is â€¹_ * ?T â‰¤ ?Sâ€º)
proof -
have "(âˆ‘_ âˆˆ {1..m}. ?T) â‰¤ ?S"
using sum_mono[of â€¹{1..m}â€º â€¹Î»_. ?Tâ€º T]
and min_correct by blast
then show ?thesis by simp
qed

definition invâ‡©1 :: "(nat â‡’ nat) â‡’ (nat â‡’ nat set) â‡’ nat â‡’ bool" where
"invâ‡©1 T A j = (lb T A j âˆ§ j â‰¤ n âˆ§ (âˆ€T' A'. lb T' A' j âŸ¶ makespan T â‰¤ 2 * makespan T'))"

assumes "invâ‡©1 T A j"
shows "lb T A j" "j â‰¤ n"
"lb T' A' j âŸ¹ makespan T â‰¤ 2 * makespan T'"
using assms unfolding invâ‡©1_def by blast+

assumes "lb T A j" "j â‰¤ n" "âˆ€T' A'. lb T' A' j âŸ¶ makespan T â‰¤ 2 * makespan T'"
shows "invâ‡©1 T A j" using assms unfolding invâ‡©1_def by blast

assumes "invâ‡©1 T A j" "j < n"
shows "invâ‡©1 (T ((minâ‡©k T m) := T (minâ‡©k T m) + t (Suc j)))
(A ((minâ‡©k T m) := A (minâ‡©k T m) âˆª {Suc j})) (Suc j)"
(is â€¹invâ‡©1 ?T ?A _â€º)
proof -
note invrules = invâ‡©1E[OF assms(1)]
â€• â€¹Greedy is correctâ€º
have LB: "lb ?T ?A (Suc j)"
using add_job[OF invrules(1) min_in_range[OF m_gt_0]] by blast
â€• â€¹Greedy maintains approximation factorâ€º
have MK: "âˆ€T' A'. lb T' A' (Suc j) âŸ¶ makespan ?T â‰¤ 2 * makespan T'"
proof rule+
from smaller_optimum[OF this]
then have IH: "makespan T â‰¤ 2 * makespan Tâ‡©1"
using invrules(3) by force
show "makespan ?T â‰¤ 2 * makespan Tâ‡©1"
proof (cases â€¹makespan ?T = T (minâ‡©k T m) + t (Suc j)â€º)
case True
have "m * T (minâ‡©k T m) â‰¤ (âˆ‘i âˆˆ {1..m}. T i)" by (rule min_avg)
also have "... = (âˆ‘i âˆˆ {1..j}. t i)" by (rule lb_impl_job_sum[OF invrules(1)])
finally have "real m * T (minâ‡©k T m) â‰¤ (âˆ‘i âˆˆ {1..j}. t i)"
by (auto dest: of_nat_mono)
with m_gt_0 have "T (minâ‡©k T m) â‰¤ (âˆ‘i âˆˆ {1..j}. t i) / m"
by (simp add: field_simps)
then have "T (minâ‡©k T m) â‰¤ makespan Tâ‡©1"
and â€¹makespan Tâ‡©0 â‰¤ makespan Tâ‡©1â€º by linarith
moreover have "t (Suc j) â‰¤ makespan Tâ‡©1"
using job_lower_bound_makespan[OF â€¹lb Tâ‡©1 Aâ‡©1 (Suc j)â€º] by simp
ultimately show ?thesis unfolding True by simp
next
case False show ?thesis using remove_small_job[OF False] IH by simp
qed
qed
from invâ‡©1I[OF LB _ MK] show ?thesis using assms(2) by simp
qed

lemma simple_greedy_approximation:
"VARS T A i j
{True}
T := (Î»_. 0);
A := (Î»_. {});
j := 0;
WHILE j < n INV {invâ‡©1 T A j} DO
i := minâ‡©k T m;
j := (Suc j);
A := A (i := A(i) âˆª {j});
T := T (i := T(i) + t j)
OD
{lb T A n âˆ§ (âˆ€T' A'. lb T' A' n âŸ¶ makespan T â‰¤ 2 * makespan T')}"
proof (vcg, goal_cases)
case (1 T A i j)
then show ?case by (simp add: lb_def invâ‡©1_def)
next
case (2 T A i j)
then show ?case using invâ‡©1_step by simp
next
case (3 T A i j)
then show ?case unfolding invâ‡©1_def by force
qed

definition sorted :: "nat â‡’ bool" where
"sorted j = (âˆ€x âˆˆ {1..j}. âˆ€y âˆˆ {1..x}. t x â‰¤ t y)"

lemma sorted_smaller [simp]: "âŸ¦ sorted j; j â‰¥ j' âŸ§ âŸ¹ sorted j'"
unfolding sorted_def by simp

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

text â€¹If â€¹Tâ€º and â€¹Aâ€º are a correct load balancing for â€¹jâ€º jobs and â€¹mâ€º machines with â€¹j > mâ€º,
and the jobs are sorted in descending order, then there exists a machine â€¹x âˆˆ {1..m}â€º
whose load is at least twice as large as the processing time of job â€¹jâ€º.â€º
lemma sorted_job_lower_bound_machine:
assumes "lb T A j" "j > m" "sorted j"
shows "âˆƒx âˆˆ {1..m}. 2 * t j â‰¤ T x"
proof -
â€• â€¹Step 1: Obtaining the jobsâ€º
note lbrules = lbE[OF assms(1)]
"jâ‡©1 âˆˆ {1..j}" "jâ‡©2 âˆˆ {1..j}" "x âˆˆ {1..m}" "jâ‡©1 â‰  jâ‡©2" "jâ‡©1 âˆˆ A x" "jâ‡©2 âˆˆ A x"
using j_gt_m_pigeonhole[OF assms(1,2)] by blast

â€• â€¹Step 2: Jobs contained in sumâ€º
have "finite (A x)" using assms(1) *(3) by simp
then have SUM: "(âˆ‘i âˆˆ A x. t i) = t jâ‡©1 + t jâ‡©2 + (âˆ‘i âˆˆ A x - {jâ‡©1} - {jâ‡©2}. t i)"
using *(4-6) by (simp add: sum.remove)

â€• â€¹Step 3: Proof of lower boundâ€º
have "t j â‰¤ t jâ‡©1" "t j â‰¤ t jâ‡©2"
using assms(3) *(1-2) unfolding sorted_def by auto
then have "2 * t j â‰¤ t jâ‡©1 + t jâ‡©2" by simp
also have "... â‰¤ (âˆ‘i âˆˆ A x. t i)" unfolding SUM by simp
finally have "2 * t j â‰¤ T x" using lbrules(3) *(3) by simp
then show ?thesis using *(3) by blast
qed

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

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

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

definition invâ‡©2 :: "(nat â‡’ nat) â‡’ (nat â‡’ nat set) â‡’ nat â‡’ bool" where
"invâ‡©2 T A j = (lb T A j âˆ§ j â‰¤ n
âˆ§ (âˆ€T' A'. lb T' A' j âŸ¶ makespan T â‰¤ 3 / 2 * makespan T')
âˆ§ (âˆ€x > j. T x = 0)
âˆ§ (j â‰¤ m âŸ¶ makespan T = Maxâ‡©0 (t  {1..j})))"

assumes "invâ‡©2 T A j"
shows "lb T A j" "j â‰¤ n"
"lb T' A' j âŸ¹ makespan T â‰¤ 3 / 2 * makespan T'"
"âˆ€x > j. T x = 0" "j â‰¤ m âŸ¹ makespan T = Maxâ‡©0 (t  {1..j})"
using assms unfolding invâ‡©2_def by blast+

assumes "lb T A j" "j â‰¤ n"
"âˆ€T' A'. lb T' A' j âŸ¶ makespan T â‰¤ 3 / 2 * makespan T'"
"âˆ€x > j. T x = 0"
"j â‰¤ m âŸ¹ makespan T = Maxâ‡©0 (t  {1..j})"
shows "invâ‡©2 T A j"
unfolding invâ‡©2_def using assms by blast

assumes "sorted n" "invâ‡©2 T A j" "j < n"
shows "invâ‡©2 (T (minâ‡©k T m := T(minâ‡©k T m) + t(Suc j)))
(A (minâ‡©k T m := A(minâ‡©k T m) âˆª {Suc j})) (Suc j)"
(is â€¹invâ‡©2 ?T ?A _â€º)
proof (cases â€¹Suc j > mâ€º)
case True note invrules = invâ‡©2E[OF assms(2)]
â€• â€¹Greedy is correctâ€º
have LB: "lb ?T ?A (Suc j)"
using add_job[OF invrules(1) min_in_range[OF m_gt_0]] by blast
â€• â€¹Greedy maintains approximation factorâ€º
have MK: "âˆ€T' A'. lb T' A' (Suc j) âŸ¶ makespan ?T â‰¤ 3 / 2 * makespan T'"
proof rule+
from smaller_optimum[OF this]
then have IH: "makespan T â‰¤ 3 / 2 * makespan Tâ‡©1"
using invrules(3) by force
show "makespan ?T â‰¤ 3 / 2 * makespan Tâ‡©1"
proof (cases â€¹makespan ?T = T (minâ‡©k T m) + t (Suc j)â€º)
case True
have "m * T (minâ‡©k T m) â‰¤ (âˆ‘i âˆˆ {1..m}. T i)" by (rule min_avg)
also have "... = (âˆ‘i âˆˆ {1..j}. t i)" by (rule lb_impl_job_sum[OF invrules(1)])
finally have "real m * T (minâ‡©k T m) â‰¤ (âˆ‘i âˆˆ {1..j}. t i)"
by (auto dest: of_nat_mono)
with m_gt_0 have "T (minâ‡©k T m) â‰¤ (âˆ‘i âˆˆ {1..j}. t i) / m"
by (simp add: field_simps)
then have "T (minâ‡©k T m) â‰¤ makespan Tâ‡©1"
and â€¹makespan Tâ‡©0 â‰¤ makespan Tâ‡©1â€º by linarith
moreover have "2 * t (Suc j) â‰¤ makespan Tâ‡©1"
using sorted_job_lower_bound_makespan[OF â€¹lb Tâ‡©1 Aâ‡©1 (Suc j)â€º â€¹Suc j > mâ€º]
and assms(1,3) by simp
ultimately show ?thesis unfolding True by simp
next
case False show ?thesis using remove_small_job[OF False] IH by simp
qed
qed
have "âˆ€x > Suc j. ?T x = 0"
using invrules(4) min_in_range[OF m_gt_0, of T] True by simp
with invâ‡©2I[OF LB _ MK] show ?thesis using assms(3) True by simp
next
case False
then have IN_RANGE: "Suc j âˆˆ {1..m}" by simp
note invrules = invâ‡©2E[OF assms(2)]
then have "T (Suc j) = 0" by blast

â€• â€¹Greedy is correctâ€º
have LB: "lb ?T ?A (Suc j)"
using add_job[OF invrules(1) min_in_range[OF m_gt_0]] by blast

â€• â€¹Greedy is trivially optimalâ€º
from IN_RANGE â€¹T (Suc j) = 0â€º have "minâ‡©k T m â‰¤ Suc j"
using min_zero_index by blast
with invrules(4) have EMPTY: "âˆ€x > Suc j. ?T x = 0" by simp
from IN_RANGE â€¹T (Suc j) = 0â€º have "T (minâ‡©k T m) = 0"
using min_zero by blast
with fun_upd_f_Maxâ‡©0[OF min_in_range[OF m_gt_0]] invrules(5) False
have TRIV: "makespan ?T = Maxâ‡©0 (t  {1..Suc j})" unfolding f_Maxâ‡©0_equiv[symmetric] by simp
have MK: "âˆ€T' A'. lb T' A' (Suc j) âŸ¶ makespan ?T â‰¤ 3 / 2 * makespan T'"
by (auto simp: TRIV[folded f_Maxâ‡©0_equiv]

from invâ‡©2I[OF LB _ MK EMPTY TRIV] show ?thesis using assms(3) by simp
qed

lemma sorted_greedy_approximation:
"sorted n âŸ¹ VARS T A i j
{True}
T := (Î»_. 0);
A := (Î»_. {});
j := 0;
WHILE j < n INV {invâ‡©2 T A j} DO
i := minâ‡©k T m;
j := (Suc j);
A := A (i := A(i) âˆª {j});
T := T (i := T(i) + t j)
OD
{lb T A n âˆ§ (âˆ€T' A'. lb T' A' n âŸ¶ makespan T â‰¤ 3 / 2 * makespan T')}"
proof (vcg, goal_cases)
case (1 T A i j)
then show ?case by (simp add: lb_def invâ‡©2_def)
next
case (2 T A i j)
then show ?case using invâ‡©2_step by simp
next
case (3 T A i j)
then show ?case unfolding invâ‡©2_def by force
qed

end (* LoadBalancing *)

end (* Theory *)

# Theory Approx_BP_Hoare

section â€¹Bin Packingâ€º

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

text â€¹The algorithm and proofs are based on the work by Berghammer and Reuter @{cite BerghammerR03}.â€º

subsection â€¹Formalization of a Correct Bin Packingâ€º

text â€¹Definition of the unary operator â€¹âŸ¦â‹…âŸ§â€º from the article.
â€¹Bâ€º will only be wrapped into a set if it is non-empty.â€º
definition wrap :: "'a set â‡’ 'a set set" where
"wrap B = (if B = {} then {} else {B})"

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

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

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

text â€¹In the article, this is defined as â€¹wâ€º as well. However, to avoid ambiguity,
we will abbreviate the weight of a bin as â€¹Wâ€º.â€º
abbreviation W :: "'a set â‡’ real" where
"W B â‰¡ (âˆ‘u âˆˆ B. w(u))"

text â€¹â€¹Pâ€º constitutes as a correct bin packing if â€¹Pâ€º is a partition of â€¹Uâ€º
(as defined in @{thm [source] partition_on_def}) and the weights of
the bins do not exceed their maximum capacity â€¹câ€º.â€º
definition bp :: "'a set set â‡’ bool" where
"bp P âŸ· partition_on U P âˆ§ (âˆ€B âˆˆ P. W(B) â‰¤ c)"

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

lemma bpI:
assumes "pairwise disjnt P" "{} âˆ‰ P" "â‹ƒP = U" "âˆ€B âˆˆ P. W(B) â‰¤ c"
shows "bp P"
using assms unfolding bp_def partition_on_def by blast

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

subsection â€¹The Proposed Approximation Algorithmâ€º

subsubsection â€¹Functional Correctnessâ€º

text â€¹According to the article, â€¹invâ‡©1â€º holds if â€¹Pâ‡©1 âˆª wrap Bâ‡©1 âˆª Pâ‡©2 âˆª wrap Bâ‡©2 âˆª {{v} |v. v âˆˆ V}â€º
is a correct solution for the bin packing problem @{cite BerghammerR03}. However, various
assumptions made in the article seem to suggest that more information is demanded from this
invariant and, indeed, mere correctness (as defined in @{thm [source] bp_def}) does not appear to suffice.
To amend this, four additional conjuncts have been added to this invariant, whose necessity
will be explained in the following proofs. It should be noted that there may be other (shorter) ways to amend this invariant.
This approach, however, makes for rather straight-forward proofs, as these conjuncts can be utilized and proved in relatively few steps.â€º
definition invâ‡©1 :: "'a set set â‡’ 'a set set â‡’ 'a set â‡’ 'a set â‡’ 'a set â‡’ bool" where
"invâ‡©1 Pâ‡©1 Pâ‡©2 Bâ‡©1 Bâ‡©2 V âŸ· bp (Pâ‡©1 âˆª wrap Bâ‡©1 âˆª Pâ‡©2 âˆª wrap Bâ‡©2 âˆª {{v} |v. v âˆˆ V}) â€• â€¹A correct solution to the bin packing problemâ€º
âˆ§ â‹ƒ(Pâ‡©1 âˆª wrap Bâ‡©1 âˆª Pâ‡©2 âˆª wrap Bâ‡©2) = U - V â€• â€¹The partial solution does not contain objects that have not yet been assignedâ€º
âˆ§ Bâ‡©1 âˆ‰ (Pâ‡©1 âˆª Pâ‡©2 âˆª wrap Bâ‡©2) â€• â€¹â€¹Bâ‡©1â€º is distinct from all the other binsâ€º
âˆ§ Bâ‡©2 âˆ‰ (Pâ‡©1 âˆª wrap Bâ‡©1 âˆª Pâ‡©2) â€• â€¹â€¹Bâ‡©2â€º is distinct from all the other binsâ€º
âˆ§ (Pâ‡©1 âˆª wrap Bâ‡©1) âˆ© (Pâ‡©2 âˆª wrap Bâ‡©2) = {} â€• â€¹The first and second partial solutions are disjoint from each other.â€º"
(*
lemma "partition_on U (Pâ‡©1 âˆª wrap Bâ‡©1 âˆª Pâ‡©2 âˆª wrap Bâ‡©2 âˆª {{v} |v. v âˆˆ V}) âŸ¹ u âˆˆ V âŸ¹
partition_on U (Pâ‡©1 âˆª wrap (insert u Bâ‡©1) âˆª Pâ‡©2 âˆª wrap Bâ‡©2 âˆª {{v} |v. v âˆˆ (V-{u})})"
nitpick*)
shows "bp (Pâ‡©1 âˆª wrap Bâ‡©1 âˆª Pâ‡©2 âˆª wrap Bâ‡©2 âˆª {{v} |v. v âˆˆ V})"
and "â‹ƒ(Pâ‡©1 âˆª wrap Bâ‡©1 âˆª Pâ‡©2 âˆª wrap Bâ‡©2) = U - V"
using assms unfolding invâ‡©1_def by auto

assumes "bp (Pâ‡©1 âˆª wrap Bâ‡©1 âˆª Pâ‡©2 âˆª wrap Bâ‡©2 âˆª {{v} |v. v âˆˆ V})"
and "â‹ƒ(Pâ‡©1 âˆª wrap Bâ‡©1 âˆª Pâ‡©2 âˆª wrap Bâ‡©2) = U - V"
using assms unfolding invâ‡©1_def by blast

lemma wrap_Un [simp]: "wrap (M âˆª {x}) = {M âˆª {x}}" unfolding wrap_def by simp
lemma wrap_empty [simp]: "wrap {} = {}" unfolding wrap_def by simp
lemma wrap_not_empty [simp]: "M â‰  {} âŸ· wrap M = {M}" unfolding wrap_def by simp

text â€¹If â€¹invâ‡©1â€º holds for the current partial solution, and the weight of an object â€¹u âˆˆ Vâ€º added to â€¹Bâ‡©1â€º does
not exceed its capacity, then â€¹invâ‡©1â€º also holds if â€¹Bâ‡©1â€º and â€¹{u}â€º are replaced by â€¹Bâ‡©1 âˆª {u}â€º.â€º
proof -
note invrules = invâ‡©1E[OF assms(1)] and bprules = bpE[OF invrules(1)]

text â€¹In the proof for â€¹Theorem 3.2â€º of the article it is erroneously argued that
if â€¹Pâ‡©1 âˆª wrap Bâ‡©1 âˆª Pâ‡©2 âˆª wrap Bâ‡©2 âˆª {{v} |v. v âˆˆ V}â€º is a partition of â€¹Uâ€º,
then the same holds if â€¹Bâ‡©1â€º is replaced by â€¹Bâ‡©1 âˆª {u}â€º.
This is, however, not necessarily the case if â€¹Bâ‡©1â€º or â€¹{u}â€º are already contained in the partial solution.
Suppose â€¹Pâ‡©1â€º contains the non-empty bin â€¹Bâ‡©1â€º, then â€¹Pâ‡©1 âˆª wrap Bâ‡©1â€º would still be pairwise disjoint, provided â€¹Pâ‡©1â€º was pairwise disjoint before, as the union simply ignores the duplicate â€¹Bâ‡©1â€º. Now, if the algorithm modifies â€¹Bâ‡©1â€º by adding an element from â€¹Vâ€º such that â€¹Bâ‡©1â€º becomes some non-empty â€¹Bâ‡©1'â€º with â€¹Bâ‡©1 âˆ© Bâ‡©1' â‰  âˆ…â€º and â€¹Bâ‡©1' âˆ‰ Pâ‡©1â€º, one can see that this property would no longer be preserved.
To avoid such a situation, we will use the first additional conjunct in â€¹invâ‡©1â€º to ensure that â€¹{u}â€º
is not yet contained in the partial solution, and the second additional conjunct to ensure that â€¹Bâ‡©1â€º
is not yet contained in the partial solution.â€º

â€• â€¹Rule 1: Pairwise Disjointâ€º
have NOTIN: "âˆ€M âˆˆ Pâ‡©1 âˆª wrap Bâ‡©1 âˆª Pâ‡©2 âˆª wrap Bâ‡©2 âˆª {{v} |v. v âˆˆ V - {u}}. u âˆ‰ M"
using invrules(2) assms(2) by blast
have "{{v} |v. v âˆˆ V} = {{u}} âˆª {{v} |v. v âˆˆ V - {u}}"
using assms(2) by blast
then have "pairwise disjnt (Pâ‡©1 âˆª wrap Bâ‡©1 âˆª Pâ‡©2 âˆª wrap Bâ‡©2 âˆª ({{u}} âˆª {{v} |v. v âˆˆ V - {u}}))"
using bprules(1) assms(2) by simp
then have "pairwise disjnt (wrap Bâ‡©1 âˆª {{u}} âˆª Pâ‡©1 âˆª Pâ‡©2 âˆª wrap Bâ‡©2 âˆª {{v} |v. v âˆˆ V - {u}})" by (simp add: Un_commute)
then have assm: "pairwise disjnt (wrap Bâ‡©1 âˆª {{u}} âˆª (Pâ‡©1 âˆª Pâ‡©2 âˆª wrap Bâ‡©2 âˆª {{v} |v. v âˆˆ V - {u}}))" by (simp add: Un_assoc)
have "pairwise disjnt ({Bâ‡©1 âˆª {u}} âˆª (Pâ‡©1 âˆª Pâ‡©2 âˆª wrap Bâ‡©2 âˆª {{v} |v. v âˆˆ V - {u}}))"
proof (cases â€¹Bâ‡©1 = {}â€º)
case True with assm show ?thesis by simp
next
case False
with assm have assm: "pairwise disjnt ({Bâ‡©1} âˆª {{u}} âˆª (Pâ‡©1 âˆª Pâ‡©2 âˆª wrap Bâ‡©2 âˆª {{v} |v. v âˆˆ V - {u}}))" by simp
from NOTIN have "{u} âˆ‰ Pâ‡©1 âˆª Pâ‡©2 âˆª wrap Bâ‡©2 âˆª {{v} |v. v âˆˆ V - {u}}" by blast
from pairwise_disjnt_Un[OF assm _ this] invrules(2,3) show ?thesis
using False by auto
qed
then have 1: "pairwise disjnt (Pâ‡©1 âˆª wrap (Bâ‡©1 âˆª {u}) âˆª Pâ‡©2 âˆª wrap Bâ‡©2 âˆª {{v} |v. v âˆˆ V - {u}})"
unfolding wrap_Un by simp

â€• â€¹Rule 2: No empty setsâ€º
from bprules(2) have 2: "{} âˆ‰ Pâ‡©1 âˆª wrap (Bâ‡©1 âˆª {u}) âˆª Pâ‡©2 âˆª wrap Bâ‡©2 âˆª {{v} |v. v âˆˆ V - {u}}"
unfolding wrap_def by simp

â€• â€¹Rule 3: Union preservedâ€º
from bprules(3) have "â‹ƒ (Pâ‡©1 âˆª wrap Bâ‡©1 âˆª Pâ‡©2 âˆª wrap Bâ‡©2 âˆª {{u}} âˆª {{v} |v. v âˆˆ V - {u}}) = U"
using assms(2) by blast
then have 3: "â‹ƒ (Pâ‡©1 âˆª wrap (Bâ‡©1 âˆª {u}) âˆª Pâ‡©2 âˆª wrap Bâ‡©2 âˆª {{v} |v. v âˆˆ V - {u}}) = U"
unfolding wrap_def by force

â€• â€¹Rule 4: Weights below capacityâ€º
have "0 < w u" using weight assms(2) bprules(3) by blast
have "finite Bâ‡©1" using bprules(3) U_Finite by (cases â€¹Bâ‡©1 = {}â€º) auto
then have "W (Bâ‡©1 âˆª {u}) â‰¤ W Bâ‡©1 + w u" using â€¹0 < w uâ€º by (cases â€¹u âˆˆ Bâ‡©1â€º) (auto simp: insert_absorb)
also have "... â‰¤ c" using assms(3) .
finally have "W (Bâ‡©1 âˆª {u}) â‰¤ c" .
then have "âˆ€B âˆˆ wrap (Bâ‡©1 âˆª {u}). W B â‰¤ c" unfolding wrap_Un by blast
moreover have "âˆ€BâˆˆPâ‡©1 âˆª Pâ‡©2 âˆª wrap Bâ‡©2 âˆª {{v} |v. v âˆˆ V - {u}}. W B â‰¤ c"
using bprules(4) by blast
ultimately have 4: "âˆ€BâˆˆPâ‡©1 âˆª wrap (Bâ‡©1 âˆª {u}) âˆª Pâ‡©2 âˆª wrap Bâ‡©2 âˆª {{v} |v. v âˆˆ V - {u}}. W B â‰¤ c" by blast
from bpI[OF 1 2 3 4] have 1: "bp (Pâ‡©1 âˆª wrap (Bâ‡©1 âˆª {u}) âˆª Pâ‡©2 âˆª wrap Bâ‡©2 âˆª {{v} |v. v âˆˆ V - {u}})" .

â€• â€¹Auxiliary information is preservedâ€º
have "u âˆˆ U" using assms(2) bprules(3) by blast
then have R: "U - (V - {u}) = U - V âˆª {u}" by blast
have L: "â‹ƒ (Pâ‡©1 âˆª wrap (Bâ‡©1 âˆª {u}) âˆª Pâ‡©2 âˆª wrap Bâ‡©2) = â‹ƒ (Pâ‡©1 âˆª wrap Bâ‡©1 âˆª Pâ‡©2 âˆª wrap Bâ‡©2) âˆª {u}"
unfolding wrap_def using NOTIN by auto
have 2: "â‹ƒ (Pâ‡©1 âˆª wrap (Bâ‡©1 âˆª {u}) âˆª Pâ‡©2 âˆª wrap Bâ‡©2) = U - (V - {u})"
unfolding L R invrules(2) ..
using NOTIN by auto
using invrules(4) NOTIN unfolding wrap_def by fastforce
using invrules(5) NOTIN unfolding wrap_Un by auto

from invâ‡©1I[OF 1 2 3 4 5] show ?thesis .
qed

text â€¹If â€¹invâ‡©1â€º holds for the current partial solution, and the weight of an object â€¹u âˆˆ Vâ€º added to â€¹Bâ‡©2â€º does
not exceed its capacity, then â€¹invâ‡©1â€º also holds if â€¹Bâ‡©2â€º and â€¹{u}â€º are replaced by â€¹Bâ‡©2 âˆª {u}â€º.â€º
proof -
note invrules = invâ‡©1E[OF assms(1)] and bprules = bpE[OF invrules(1)]

text â€¹The argumentation here is similar to the one in @{thm [source] invâ‡©1_stepA} with
â€¹Bâ‡©1â€º replaced with â€¹Bâ‡©2â€º and using the first and third additional conjuncts of â€¹invâ‡©1â€º
to amend the issue, instead of the first and second.â€º
â€• â€¹Rule 1: Pairwise Disjointâ€º
have NOTIN: "âˆ€M âˆˆ Pâ‡©1 âˆª wrap Bâ‡©1 âˆª Pâ‡©2 âˆª wrap Bâ‡©2 âˆª {{v} |v. v âˆˆ V - {u}}. u âˆ‰ M"
using invrules(2) assms(2) by blast
have "{{v} |v. v âˆˆ V} = {{u}} âˆª {{v} |v. v âˆˆ V - {u}}"
using assms(2) by blast
then have "pairwise disjnt (Pâ‡©1 âˆª wrap Bâ‡©1 âˆª Pâ‡©2 âˆª wrap Bâ‡©2 âˆª {{u}} âˆª {{v} |v. v âˆˆ V - {u}})"
using bprules(1) assms(2) by simp
then have assm: "pairwise disjnt (wrap Bâ‡©2 âˆª {{u}} âˆª (Pâ‡©1 âˆª wrap Bâ‡©1 âˆª Pâ‡©2 âˆª {{v} |v. v âˆˆ V - {u}}))"
by (simp add: Un_assoc Un_commute)
have "pairwise disjnt ({Bâ‡©2 âˆª {u}} âˆª (Pâ‡©1 âˆª wrap Bâ‡©1 âˆª Pâ‡©2 âˆª {{v} |v. v âˆˆ V - {u}}))"
proof (cases â€¹Bâ‡©2 = {}â€º)
case True with assm show ?thesis by simp
next
case False
with assm have assm: "pairwise disjnt ({Bâ‡©2} âˆª {{u}} âˆª (Pâ‡©1 âˆª wrap Bâ‡©1 âˆª Pâ‡©2 âˆª {{v} |v. v âˆˆ V - {u}}))" by simp
from NOTIN have "{u} âˆ‰ Pâ‡©1 âˆª wrap Bâ‡©1 âˆª Pâ‡©2 âˆª {{v} |v. v âˆˆ V - {u}}" by blast
from pairwise_disjnt_Un[OF assm _ this] invrules(2,4) show ?thesis
using False by auto
qed
then have 1: "pairwise disjnt (Pâ‡©1 âˆª wrap Bâ‡©1 âˆª wrap {} âˆª Pâ‡©2 âˆª wrap (Bâ‡©2 âˆª {u}) âˆª {{v} |v. v âˆˆ V - {u}})"
unfolding wrap_Un by simp

â€• â€¹Rule 2: No empty setsâ€º
from bprules(2) have 2: "{} âˆ‰ Pâ‡©1 âˆª wrap Bâ‡©1 âˆª wrap {} âˆª Pâ‡©2 âˆª wrap (Bâ‡©2 âˆª {u}) âˆª {{v} |v. v âˆˆ V - {u}}"
unfolding wrap_def by simp

â€• â€¹Rule 3: Union preservedâ€º
from bprules(3) have "â‹ƒ (Pâ‡©1 âˆª wrap Bâ‡©1 âˆª Pâ‡©2 âˆª wrap Bâ‡©2 âˆª {{u}} âˆª {{v} |v. v âˆˆ V - {u}}) = U"
using assms(2) by blast
then have 3: "â‹ƒ (Pâ‡©1 âˆª wrap Bâ‡©1 âˆª wrap {} âˆª Pâ‡©2 âˆª wrap (Bâ‡©2 âˆª {u}) âˆª {{v} |v. v âˆˆ V - {u}}) = U"
unfolding wrap_def by force

â€• â€¹Rule 4: Weights below capacityâ€º
have "0 < w u" using weight assms(2) bprules(3) by blast
have "finite Bâ‡©2" using bprules(3) U_Finite by (cases â€¹Bâ‡©2 = {}â€º) auto
then have "W (Bâ‡©2 âˆª {u}) â‰¤ W Bâ‡©2 + w u" using â€¹0 < w uâ€º by (cases â€¹u âˆˆ Bâ‡©2â€º) (auto simp: insert_absorb)
also have "... â‰¤ c" using assms(3) .
finally have "W (Bâ‡©2 âˆª {u}) â‰¤ c" .
then have "âˆ€B âˆˆ wrap (Bâ‡©2 âˆª {u}). W B â‰¤ c" unfolding wrap_Un by blast
moreover have "âˆ€BâˆˆPâ‡©1 âˆª wrap Bâ‡©1 âˆª Pâ‡©2 âˆª {{v} |v. v âˆˆ V - {u}}. W B â‰¤ c"
using bprules(4) by blast
ultimately have 4: "âˆ€BâˆˆPâ‡©1 âˆª wrap Bâ‡©1 âˆª wrap {} âˆª Pâ‡©2 âˆª wrap (Bâ‡©2 âˆª {u}) âˆª {{v} |v. v âˆˆ V - {u}}. W B â‰¤ c"
by auto
from bpI[OF 1 2 3 4] have 1: "bp (Pâ‡©1 âˆª wrap Bâ‡©1 âˆª wrap {} âˆª Pâ‡©2 âˆª wrap (Bâ‡©2 âˆª {u}) âˆª {{v} |v. v âˆˆ V - {u}})" .

â€• â€¹Auxiliary information is preservedâ€º
have "u âˆˆ U" using assms(2) bprules(3) by blast
then have R: "U - (V - {u}) = U - V âˆª {u}" by blast
have L: "â‹ƒ (Pâ‡©1 âˆª wrap Bâ‡©1 âˆª wrap {} âˆª Pâ‡©2 âˆª wrap (Bâ‡©2 âˆª {u})) = â‹ƒ (Pâ‡©1 âˆª wrap Bâ‡©1 âˆª wrap {} âˆª Pâ‡©2 âˆª wrap Bâ‡©2) âˆª {u}"
unfolding wrap_def using NOTIN by auto
have 2: "â‹ƒ (Pâ‡©1 âˆª wrap Bâ‡©1 âˆª wrap {} âˆª Pâ‡©2 âˆª wrap (Bâ‡©2 âˆª {u})) = U - (V - {u})"
unfolding L R using invrules(2) by simp
have 3: "{} âˆ‰ Pâ‡©1 âˆª wrap Bâ‡©1 âˆª Pâ‡©2 âˆª wrap (Bâ‡©2 âˆª {u})"
using bpE(2)[OF 1] by simp
have 4: "Bâ‡©2 âˆª {u} âˆ‰ Pâ‡©1 âˆª wrap Bâ‡©1 âˆª wrap {} âˆª Pâ‡©2"
using NOTIN by auto
have 5: "(Pâ‡©1 âˆª wrap Bâ‡©1 âˆª wrap {}) âˆ© (Pâ‡©2 âˆª wrap (Bâ‡©2 âˆª {u})) = {}"
using invrules(5) NOTIN unfolding wrap_empty wrap_Un by auto

from invâ‡©1I[OF 1 2 3 4 5] show ?thesis .
qed

text â€¹If â€¹invâ‡©1â€º holds for the current partial solution, then â€¹invâ‡©1â€º also holds if â€¹Bâ‡©1â€º and â€¹Bâ‡©2â€º are
proof -
note invrules = invâ‡©1E[OF assms(1)]
â€• â€¹Rule 1-4: Correct Bin Packingâ€º
have "Pâ‡©1 âˆª wrap Bâ‡©1 âˆª wrap {} âˆª (Pâ‡©2 âˆª wrap Bâ‡©2) âˆª wrap {u} âˆª {{v} |v. v âˆˆ V - {u}}
= Pâ‡©1 âˆª wrap Bâ‡©1 âˆª Pâ‡©2 âˆª wrap Bâ‡©2 âˆª {{u}} âˆª {{v} |v. v âˆˆ V - {u}}"
by (metis (no_types, lifting) Un_assoc Un_empty_right insert_not_empty wrap_empty wrap_not_empty)
also have "... = Pâ‡©1 âˆª wrap Bâ‡©1 âˆª Pâ‡©2 âˆª wrap Bâ‡©2 âˆª {{v} |v. v âˆˆ V}"
using assms(2) by auto
finally have EQ: "Pâ‡©1 âˆª wrap Bâ‡©1 âˆª wrap {} âˆª (Pâ‡©2 âˆª wrap Bâ‡©2) âˆª wrap {u} âˆª {{v} |v. v âˆˆ V - {u}}
= Pâ‡©1 âˆª wrap Bâ‡©1 âˆª Pâ‡©2 âˆª wrap Bâ‡©2 âˆª {{v} |v. v âˆˆ V}" .
from invrules(1) have 1: "bp (Pâ‡©1 âˆª wrap Bâ‡©1 âˆª wrap {} âˆª (Pâ‡©2 âˆª wrap Bâ‡©2) âˆª wrap {u} âˆª {{v} |v. v âˆˆ V - {u}})"
unfolding EQ .

â€• â€¹Auxiliary information is preservedâ€º
have NOTIN: "âˆ€M âˆˆ Pâ‡©1 âˆª wrap Bâ‡©1 âˆª Pâ‡©2 âˆª wrap Bâ‡©2 âˆª {{v} |v. v âˆˆ V - {u}}. u âˆ‰ M"
using invrules(2) assms(2) by blast
have "u âˆˆ U" using assms(2) bpE(3)[OF invrules(1)] by blast
then have R: "U - (V - {u}) = U - V âˆª {u}" by blast
have L: "â‹ƒ (Pâ‡©1 âˆª wrap Bâ‡©1 âˆª wrap {} âˆª (Pâ‡©2 âˆª wrap Bâ‡©2) âˆª wrap {u}) = â‹ƒ (Pâ‡©1 âˆª wrap Bâ‡©1 âˆª wrap {} âˆª (Pâ‡©2 âˆª wrap Bâ‡©2)) âˆª {u}"
unfolding wrap_def using NOTIN by auto
have 2: "â‹ƒ (Pâ‡©1 âˆª wrap Bâ‡©1 âˆª wrap {} âˆª (Pâ‡©2 âˆª wrap Bâ‡©2) âˆª wrap {u}) = U - (V - {u})"
unfolding L R using invrules(2) by auto
have 3: "{} âˆ‰ Pâ‡©1 âˆª wrap Bâ‡©1 âˆª (Pâ‡©2 âˆª wrap Bâ‡©2) âˆª wrap {u}"
using bpE(2)[OF 1] by simp
have 4: "{u} âˆ‰ Pâ‡©1 âˆª wrap Bâ‡©1 âˆª wrap {} âˆª (Pâ‡©2 âˆª wrap Bâ‡©2)"
using NOTIN by auto
have 5: "(Pâ‡©1 âˆª wrap Bâ‡©1 âˆª wrap {}) âˆ© (Pâ‡©2 âˆª wrap Bâ‡©2 âˆª wrap {u}) = {}"
using invrules(5) NOTIN unfolding wrap_def by force

from invâ‡©1I[OF 1 2 3 4 5] show ?thesis .
qed

text â€¹A simplified version of the bin packing algorithm proposed in the article.
It serves as an introduction into the approach taken, and, while it does not provide the desired
approximation factor, it does ensure that â€¹Pâ€º is a correct solution of the bin packing problem.â€º
lemma simple_bp_correct:
{True}
Pâ‡©1 := {}; Pâ‡©2 := {}; Bâ‡©1 := {}; Bâ‡©2 := {}; V := U;
u := (SOME u. u âˆˆ V); V := V - {u};
IF W(Bâ‡©1) + w(u) â‰¤ c
ELSE IF W(Bâ‡©2) + w(u) â‰¤ c
OD;
P := Pâ‡©1 âˆª wrap Bâ‡©1 âˆª Pâ‡©2 âˆª wrap Bâ‡©2 âˆª {{v} | v. v âˆˆ V}
{bp P}"
proof (vcg, goal_cases)
show ?case
unfolding bp_def partition_on_def pairwise_def wrap_def invâ‡©1_def
using weight by auto
next
from 2 have "V â‰  {}" by blast
then have IN: "(SOME u. u âˆˆ V) âˆˆ V" by (simp add: some_in_eq)
from invâ‡©1_stepA[OF INV IN] invâ‡©1_stepB[OF INV IN] invâ‡©1_stepC[OF INV IN]
show ?case by blast
next
then show ?case unfolding invâ‡©1_def by blast
qed

subsubsection â€¹Lower Bounds for the Bin Packing Problemâ€º

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

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

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

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

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

text â€¹If â€¹Pâ€º is a correct solution of the bin packing problem, â€¹invâ‡©1â€º holds for the partial solution,
and every bin in â€¹Pâ‡©1 âˆª wrap Bâ‡©1â€º contains a large object, then the amount of bins in
â€¹Pâ‡©1 âˆª wrap Bâ‡©1 âˆª {{v} |v. v âˆˆ V âˆ© L}â€º is a lower bound for the amount of bins in â€¹Pâ€º.â€º
lemma L_bins_lower_bound_card:
shows "card (Pâ‡©1 âˆª wrap Bâ‡©1 âˆª {{v} |v. v âˆˆ V âˆ© L}) â‰¤ card P"
proof -
note invrules = invâ‡©1E[OF assms(2)]
have "âˆ€B âˆˆ {{v} |v. v âˆˆ V âˆ© L}. B âˆ© L â‰  {}" by blast
with assms(3) have
"Pâ‡©1 âˆª wrap Bâ‡©1 âˆª {{v} |v. v âˆˆ V âˆ© L} âŠ† Pâ‡©1 âˆª wrap Bâ‡©1 âˆª Pâ‡©2 âˆª wrap Bâ‡©2 âˆª {{v} |v. v âˆˆ V}"
"âˆ€B âˆˆ Pâ‡©1 âˆª wrap Bâ‡©1 âˆª {{v} |v. v âˆˆ V âˆ© L}. B âˆ© L â‰  {}" by blast+
from subset_bp_card[OF invrules(1) this] show ?thesis
using L_lower_bound_card[OF assms(1)] by linarith
qed

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

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

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

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

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

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

have F: "âˆ€B âˆˆ Pâ‡©2 âˆª wrap Bâ‡©2. finite B" using invrules(1) by simp
have D: "âˆ€A âˆˆ Pâ‡©2 âˆª wrap Bâ‡©2. âˆ€B âˆˆ Pâ‡©2 âˆª wrap Bâ‡©2. A â‰  B âŸ¶ A âˆ© B = {}"
using bpE(1)[OF invrules(1)] unfolding pairwise_def disjnt_def by auto
have sum_eq: "W (â‹ƒ (Pâ‡©2 âˆª wrap Bâ‡©2)) = (âˆ‘B âˆˆ Pâ‡©2 âˆª wrap Bâ‡©2. W B)"
using sum.Union_disjoint[OF F D] by auto

have "âˆ€BâˆˆPâ‡©1 âˆª wrap Bâ‡©1 âˆª Pâ‡©2 âˆª wrap Bâ‡©2 âˆª {{v} |v. v âˆˆ V}. 0 < W B"
using bpE(2,3)[OF invrules(1)] weight by (metis (no_types, lifting) UnionI bp_bins_finite invrules(1) sum_pos)
then have "(âˆ‘B âˆˆ Pâ‡©1 âˆª Pâ‡©2 âˆª wrap Bâ‡©2. W B) â‰¤ (âˆ‘B âˆˆ Pâ‡©1 âˆª Pâ‡©2 âˆª wrap Bâ‡©2 âˆª (wrap Bâ‡©1 âˆª {{v} |v. v âˆˆ V}). W B)"
using sum_Un_ge[OF FINITE(3,4), of W] by blast
also have "... = (âˆ‘B âˆˆ Pâ‡©1 âˆª wrap Bâ‡©1 âˆª Pâ‡©2 âˆª wrap Bâ‡©2 âˆª {{v} |v. v âˆˆ V}. W B)" by (smt Un_assoc Un_commute)
also have "... = W U" using sum_Un_eq_sum_sum[OF invrules(1), symmetric] .
finally have *: "(âˆ‘B âˆˆ Pâ‡©1 âˆª Pâ‡©2 âˆª wrap Bâ‡©2. W B) â‰¤ W U" .

â€• â€¹This follows from the fourth and final additional conjunct of â€¹invâ‡©1â€º 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 â€¹Pâ‡©1â€º and â€¹Pâ‡©2 âˆª wrap Bâ‡©2â€º happened to be equal.â€º
have DISJNT: "Pâ‡©1 âˆ© (Pâ‡©2 âˆª wrap Bâ‡©2) = {}" using invrules(5) by blast

â€• â€¹This part of the proof is based on the proof on page 72 of the article @{cite BerghammerR03}.â€º
have "c * card Pâ‡©1 = (âˆ‘B âˆˆ Pâ‡©1. c)" by simp
also have "... < (âˆ‘B âˆˆ Pâ‡©1. W B + w (f B))"
using f_def(2) sum_strict_mono[OF FINITE(1) False] by fastforce
also have "... = (âˆ‘B âˆˆ Pâ‡©1. W B) + (âˆ‘B âˆˆ Pâ‡©1. w (f B))"
also have "... = (âˆ‘B âˆˆ Pâ‡©1. W B) + W (â‹ƒ (Pâ‡©2 âˆª wrap Bâ‡©2))" unfolding sum.reindex_bij_betw[OF f_def(1), of w] ..
also have "... = (âˆ‘B âˆˆ Pâ‡©1. W B) + (âˆ‘B âˆˆ Pâ‡©2 âˆª wrap Bâ‡©2. W B)" unfolding sum_eq ..
also have "... = (âˆ‘B âˆˆ Pâ‡©1 âˆª Pâ‡©2 âˆª wrap Bâ‡©2. W B)" using sum.union_disjoint[OF FINITE(1,2) DISJNT, of W] by (simp add: Un_assoc)
also have "... â‰¤ (âˆ‘u âˆˆ U. w u)" using * .
also have "... â‰¤ c * card P" using sum_lower_bound_card[OF assms(1)] .
finally show ?thesis by (meson discrete nat_mult_less_cancel_disj of_nat_less_imp_less)
qed

text â€¹As @{thm wrap_card} holds, it follows that the amount of bins in â€¹Pâ‡©1 âˆª wrap Bâ‡©1â€º
are a lower bound for the amount of bins in â€¹Pâ€º.â€º
shows "card (Pâ‡©1 âˆª wrap Bâ‡©1) â‰¤ card P"
proof -
using card_Un_le by blast
also have "... â‰¤ card Pâ‡©1 + 1" using wrap_card by simp
also have "... â‰¤ card P" using Pâ‡©1_lower_bound_card[OF assms] .
finally show ?thesis .
qed

text â€¹If â€¹invâ‡©1â€º holds, there are at most half as many bins in â€¹Pâ‡©2â€º as there are objects in â€¹Pâ‡©2â€º, and we can again
obtain a bijective function between the bins in â€¹Pâ‡©1â€º 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.â€º
shows "2 * card (Pâ‡©2 âˆª wrap Bâ‡©2) â‰¤ card Pâ‡©1 + 1"
proof -
note invrules = invâ‡©1E[OF assms(1)] and bprules = bpE[OF invrules(1)]

have "pairwise disjnt (Pâ‡©2 âˆª wrap Bâ‡©2)"
using bprules(1) pairwise_subset by blast
moreover have "Bâ‡©2 âˆ‰ Pâ‡©2" using invrules(4) by simp
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 (â‹ƒPâ‡©2)" using U_Finite bprules(3) by auto
have "finite Bâ‡©2" using bp_bins_finite[OF invrules(1)] wrap_not_empty by blast
have "finite Pâ‡©2" "finite (wrap Bâ‡©2)" using bp_sol_finite[OF invrules(1)] by blast+
have "card (wrap Bâ‡©2) â‰¤ card Bâ‡©2"
proof (cases â€¹Bâ‡©2 = {}â€º)
case False
then have "1 â‰¤ card Bâ‡©2" by (simp add: leI â€¹finite Bâ‡©2â€º)
then show ?thesis using wrap_card[of Bâ‡©2] by linarith
qed simp

â€• â€¹This part of the proof is based on the proof on page 73 of the article @{cite BerghammerR03}.â€º
from assms(2) have "2 * card Pâ‡©2 + 2 * card (wrap Bâ‡©2) â‰¤ card (â‹ƒPâ‡©2) + card (wrap Bâ‡©2) + 1"
using wrap_card[of Bâ‡©2] by linarith
then have "2 * (card Pâ‡©2 + card (wrap Bâ‡©2)) â‰¤ card (â‹ƒPâ‡©2) + card Bâ‡©2 + 1"
using â€¹card (wrap Bâ‡©2) â‰¤ card Bâ‡©2â€º by simp
then have "2 * (card (Pâ‡©2 âˆª wrap Bâ‡©2)) â‰¤ card (â‹ƒPâ‡©2 âˆª Bâ‡©2) + 1"
using card_Un_disjoint[OF â€¹finite (â‹ƒPâ‡©2)â€º â€¹finite Bâ‡©2â€º DISJNT]
and card_Un_disjoint[OF â€¹finite Pâ‡©2â€º â€¹finite (wrap Bâ‡©2)â€º DISJNT2] by argo
then have "2 * (card (Pâ‡©2 âˆª wrap Bâ‡©2)) â‰¤ card (â‹ƒ(Pâ‡©2 âˆª wrap Bâ‡©2)) + 1"
by (cases â€¹Bâ‡©2 = {}â€º) (auto simp: Un_commute)
then show "2 * (card (Pâ‡©2 âˆª wrap Bâ‡©2)) â‰¤ card Pâ‡©1 + 1"
using assms(3) bij_betw_same_card unfolding bij_exists_def by metis
qed

subsubsection â€¹Proving the Approximation Factorâ€º

text â€¹We define â€¹invâ‡©2â€º as it is defined in the article.
These conjuncts allow us to prove the desired approximation factor.â€º
definition invâ‡©2 :: "'a set set â‡’ 'a set set â‡’ 'a set â‡’ 'a set â‡’ 'a set â‡’ bool" where
âˆ§ (V âˆ© L â‰  {} âŸ¶ (âˆ€B âˆˆ Pâ‡©1 âˆª wrap Bâ‡©1. B âˆ© L â‰  {})) â€• â€¹If there are still large objects left, then every bin of the first partial solution must contain a large objectâ€º
âˆ§ bij_exists Pâ‡©1 (â‹ƒ(Pâ‡©2 âˆª wrap Bâ‡©2)) â€• â€¹There exists a bijective function between the bins of the first partial solution and the objects of the second oneâ€º
âˆ§ (2 * card Pâ‡©2 â‰¤ card (â‹ƒPâ‡©2)) â€• â€¹There are at most twice as many bins in â€¹Pâ‡©2â€º as there are objects in â€¹Pâ‡©2â€ºâ€º"

and "V âˆ© L â‰  {} âŸ¹ âˆ€B âˆˆ Pâ‡©1 âˆª wrap Bâ‡©1. B âˆ© L â‰  {}"
and "2 * card Pâ‡©2 â‰¤ card (â‹ƒPâ‡©2)"
using assms unfolding invâ‡©2_def by blast+

and "V âˆ© L â‰  {} âŸ¹ âˆ€B âˆˆ Pâ‡©1 âˆª wrap Bâ‡©1. B âˆ© L â‰  {}"
and "2 * card Pâ‡©2 â‰¤ card (â‹ƒPâ‡©2)"
using assms unfolding invâ‡©2_def by blast

text â€¹If â€¹Pâ€º is a correct solution of the bin packing problem, â€¹invâ‡©2â€º holds for the partial solution,
and there are no more small objects left to be distributed, then the amount of bins of the partial solution
is no larger than â€¹3 / 2â€º of the amount of bins in â€¹Pâ€º. This proof strongly follows the proof in
â€¹Theorem 4.1â€º of the article @{cite BerghammerR03}.â€º
lemma bin_packing_lower_bound_card:
shows "card (Pâ‡©1 âˆª wrap Bâ‡©1 âˆª Pâ‡©2 âˆª wrap Bâ‡©2 âˆª {{v} |v. v âˆˆ V}) â‰¤ 3 / 2 * card P"
proof (cases â€¹V = {}â€º)
note invrules = invâ‡©2E[OF assms(2)]
case True
then have "card (Pâ‡©1 âˆª wrap Bâ‡©1 âˆª Pâ‡©2 âˆª wrap Bâ‡©2 âˆª {{v} |v. v âˆˆ V})
also have "... â‰¤ card (Pâ‡©1 âˆª wrap Bâ‡©1) + card (Pâ‡©2 âˆª wrap Bâ‡©2)"
using card_Un_le[of â€¹Pâ‡©1 âˆª wrap Bâ‡©1â€º] by (simp add: Un_assoc)
also have "... â‰¤ card P + card (Pâ‡©2 âˆª wrap Bâ‡©2)"
also have "... â‰¤ card P + card P / 2"
and Pâ‡©1_lower_bound_card[OF assms(3) invrules(1,3)] by linarith
finally show ?thesis by linarith
next
note invrules = invâ‡©2E[OF assms(2)]
case False
have "U = S âˆª L" using S_def L_def by blast
then have *: "V = V âˆ© L"
using bpE(3)[OF invâ‡©1E(1)[OF invrules(1)]]
and assms(1) by blast
with False have NE: "V âˆ© L â‰  {}" by simp
have "card (Pâ‡©1 âˆª wrap Bâ‡©1 âˆª Pâ‡©2 âˆª wrap Bâ‡©2 âˆª {{v} |v. v âˆˆ V})
= card (Pâ‡©1 âˆª wrap Bâ‡©1 âˆª {{v} |v. v âˆˆ V âˆ© L} âˆª Pâ‡©2 âˆª wrap Bâ‡©2)"
using * by (simp add: Un_commute Un_assoc)
also have "... â‰¤ card (Pâ‡©1 âˆª wrap Bâ‡©1 âˆª {{v} |v. v âˆˆ V âˆ© L}) + card (Pâ‡©2 âˆª wrap Bâ‡©2)"
using card_Un_le[of â€¹Pâ‡©1 âˆª wrap Bâ‡©1 âˆª {{v} |v. v âˆˆ V âˆ© L}â€º] by (simp add: Un_assoc)
also have "... â‰¤ card P + card (Pâ‡©2 âˆª wrap Bâ‡©2)"
using L_bins_lower_bound_card[OF assms(3) invrules(1) invrules(2)[OF NE]] by linarith
also have "... â‰¤ card P + card P / 2"
and Pâ‡©1_lower_bound_card[OF assms(3) invrules(1,3)] by linarith
finally show ?thesis by linarith
qed

text â€¹We define â€¹invâ‡©3â€º as it is defined in the article.
This final conjunct allows us to prove that the invariant will be maintained by the algorithm.â€º
definition invâ‡©3 :: "'a set set â‡’ 'a set set â‡’ 'a set â‡’ 'a set â‡’ 'a set â‡’ bool" where

using assms unfolding invâ‡©3_def by blast+

using assms unfolding invâ‡©3_def by blast

lemma loop_init:
"invâ‡©3 {} {} {} {} U"
proof -
have *: "invâ‡©1 {} {} {} {} U"
unfolding bp_def partition_on_def pairwise_def wrap_def invâ‡©1_def
using weight by auto
have "bij_exists {} (â‹ƒ ({} âˆª wrap {}))"
using bij_betwI' unfolding bij_exists_def by fastforce
from invâ‡©2I[OF * _ this] have "invâ‡©2 {} {} {} {} U" by auto
from invâ‡©3I[OF this] show ?thesis by blast
qed

text â€¹If â€¹Bâ‡©1â€º is empty and there are no large objects left, then â€¹invâ‡©3â€º will be maintained
if â€¹Bâ‡©1â€º is initialized with â€¹u âˆˆ V âˆ© Sâ€º.â€º
lemma loop_stepA:
proof -
have WEIGHT: "W Bâ‡©1 + w u â‰¤ c" using S_def assms(2,4) by simp
from assms(4) have "u âˆˆ V" by blast
from invâ‡©1_stepA[OF invrules(1) this WEIGHT] assms(2) have 1: "invâ‡©1 Pâ‡©1 Pâ‡©2 {u} Bâ‡©2 (V - {u})" by simp
have 2: "(V - {u}) âˆ© L â‰  {} âŸ¹ âˆ€BâˆˆPâ‡©1 âˆª wrap {u}. B âˆ© L â‰  {}" using assms(3) by blast
from invâ‡©3I[OF this] show ?thesis using invâ‡©3E(2)[OF assms(1)] .
qed

text â€¹If â€¹Bâ‡©1â€º is empty and there are large objects left, then â€¹invâ‡©3â€º will be maintained
if â€¹Bâ‡©1â€º is initialized with â€¹u âˆˆ V âˆ© Lâ€º.â€º
lemma loop_stepB:
proof -
have WEIGHT: "W Bâ‡©1 + w u â‰¤ c" using L_def weight assms(2,3) by simp
from assms(3) have "u âˆˆ V" by blast
from invâ‡©1_stepA[OF invrules(1) this WEIGHT] assms(2) have 1: "invâ‡©1 Pâ‡©1 Pâ‡©2 {u} Bâ‡©2 (V - {u})" by simp
have "âˆ€BâˆˆPâ‡©1. B âˆ© L â‰  {}" using assms(3) invrules(2) by blast
then have 2: "(V - {u}) âˆ© L â‰  {} âŸ¹ âˆ€BâˆˆPâ‡©1 âˆª wrap {u}. B âˆ© L â‰  {}"
using assms(3) by (metis Int_iff UnE empty_iff insertE singletonI wrap_not_empty)
from invâ‡©3I[OF this] show ?thesis using invâ‡©3E(2)[OF assms(1)] .
qed

text â€¹If â€¹Bâ‡©1â€º is not empty and â€¹u âˆˆ V âˆ© Sâ€º does not exceed its maximum capacity, then â€¹invâ‡©3â€º
will be maintained if â€¹Bâ‡©1â€º and â€¹{u}â€º are replaced with â€¹Bâ‡©1 âˆª {u}â€º.â€º
lemma loop_stepC:
proof -
from assms(3) have "u âˆˆ V" by blast
have "(V - {u}) âˆ© L â‰  {} âŸ¹ âˆ€BâˆˆPâ‡©1 âˆª wrap Bâ‡©1. B âˆ© L â‰  {}" using invrules(2) by blast
then have 2: "(V - {u}) âˆ© L â‰  {} âŸ¹ âˆ€BâˆˆPâ‡©1 âˆª wrap (Bâ‡©1 âˆª {u}). B âˆ© L â‰  {}"
by (metis Int_commute Un_empty_right Un_insert_right assms(2) disjoint_insert(2) insert_iff wrap_not_empty)
from invâ‡©3I[OF this] show ?thesis using invâ‡©3E(2)[OF assms(1)] .
qed

text â€¹If â€¹Bâ‡©1â€º is not empty and â€¹u âˆˆ V âˆ© Sâ€º does exceed its maximum capacity but not the capacity of â€¹Bâ‡©2â€º,
then â€¹invâ‡©3â€º will be maintained if â€¹Bâ‡©1â€º is added to â€¹Pâ‡©1â€º and emptied, and â€¹Bâ‡©2â€º and â€¹{u}â€º are replaced with â€¹Bâ‡©2 âˆª {u}â€º.â€º
lemma loop_stepD:
proof -
from assms(3) have "u âˆˆ V" by blast
from invâ‡©1_stepB[OF invrules(1) this assms(5)] have 1: "invâ‡©1 (Pâ‡©1 âˆª wrap Bâ‡©1) Pâ‡©2 {} (Bâ‡©2 âˆª {u}) (V - {u})" .

have 2: "(V - {u}) âˆ© L â‰  {} âŸ¹ âˆ€BâˆˆPâ‡©1 âˆª wrap Bâ‡©1 âˆª wrap {}. B âˆ© L â‰  {}"
using invrules(2) unfolding wrap_empty by blast

from invrules(3) obtain f where f_def: "bij_betw f Pâ‡©1 (â‹ƒ (Pâ‡©2 âˆª wrap Bâ‡©2))" "âˆ€BâˆˆPâ‡©1. c < W B + w (f B)" unfolding bij_exists_def by blast
have "u âˆ‰ (â‹ƒ (Pâ‡©2 âˆª wrap Bâ‡©2))" using invâ‡©1E(2)[OF invrules(1)] assms(3) by blast
then have "(â‹ƒ (Pâ‡©2 âˆª wrap (Bâ‡©2 âˆª {u}))) = (â‹ƒ (Pâ‡©2 âˆª wrap Bâ‡©2 âˆª {{u}}))"
by (metis Sup_empty Un_assoc Union_Un_distrib ccpo_Sup_singleton wrap_empty wrap_not_empty)
also have "... = (â‹ƒ (Pâ‡©2 âˆª wrap Bâ‡©2)) âˆª {u}" by simp
finally have UN: "(â‹ƒ (Pâ‡©2 âˆª wrap (Bâ‡©2 âˆª {u}))) = (â‹ƒ (Pâ‡©2 âˆª wrap Bâ‡©2)) âˆª {u}" .
have "wrap Bâ‡©1 = {Bâ‡©1}" using wrap_not_empty[of Bâ‡©1] assms(2) by simp
let ?f = "f (Bâ‡©1 := u)"
have BIJ: "bij_betw ?f (Pâ‡©1 âˆª wrap Bâ‡©1) (â‹ƒ (Pâ‡©2 âˆª wrap (Bâ‡©2 âˆª {u})))"
by (metis (no_types, lifting) bij_betw_cong fun_upd_other fun_upd_same notIn_Un_bij_betw3)
have "c < W Bâ‡©1 + w (?f Bâ‡©1)" using assms(4) by simp
then have "(âˆ€BâˆˆPâ‡©1 âˆª wrap Bâ‡©1. c < W B + w (?f B))"
unfolding â€¹wrap Bâ‡©1 = {Bâ‡©1}â€º using f_def(2) by simp
with BIJ have "bij_betw ?f (Pâ‡©1 âˆª wrap Bâ‡©1) (â‹ƒ (Pâ‡©2 âˆª wrap (Bâ‡©2 âˆª {u})))
âˆ§ (âˆ€BâˆˆPâ‡©1 âˆª wrap Bâ‡©1. c < W B + w (?f B))" by blast
then have 3: "bij_exists (Pâ‡©1 âˆª wrap Bâ‡©1) (â‹ƒ (Pâ‡©2 âˆª wrap (Bâ‡©2 âˆª {u})))"
unfolding bij_exists_def by blast
from invâ‡©2I[OF 1 2 3] have "invâ‡©2 (Pâ‡©1 âˆª wrap Bâ‡©1) Pâ‡©2 {} (Bâ‡©2 âˆª {u}) (V - {u})" using invrules(4) by blast

from invâ‡©3I[OF this] show ?thesis using invâ‡©3E(2)[OF assms(1)] assms(3) by blast
qed

text â€¹If the maximum capacity of â€¹Bâ‡©2â€º is exceeded by â€¹u âˆˆ V âˆ© Sâ€º,
then â€¹Bâ‡©2â€º must contain at least two objects.â€º
shows "2 â‰¤ card Bâ‡©2"
proof (rule ccontr, simp add: not_le)
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â‡©2 < 2"
then consider (0) "card Bâ‡©2 = 0" | (1) "card Bâ‡©2 = 1" by linarith
then show False proof cases
case 0 then have "Bâ‡©2 = {}" using FINITE by simp
then show ?thesis using assms(2,3) S_def by simp
next
case 1 then obtain v where "Bâ‡©2 = {v}"
using card_1_singletonE by auto
with invâ‡©3E(2)[OF assms(1)] have "2 * w v â‰¤ c" using S_def by simp
moreover from â€¹Bâ‡©2 = {v}â€º have "W Bâ‡©2 = w v" by simp
ultimately show ?thesis using assms(2,3) S_def by simp
qed
qed

text â€¹If â€¹Bâ‡©1â€º is not empty and â€¹u âˆˆ V âˆ© Sâ€º exceeds the maximum capacity of both â€¹Bâ‡©1â€º and â€¹Bâ‡©2â€º,
emptied, and â€¹Bâ‡©2â€º initialized with â€¹uâ€º.â€º
lemma loop_stepE:
proof -
from assms(3) have "u âˆˆ V" by blast
from invâ‡©1_stepC[OF invrules(1) this] have 1: "invâ‡©1 (Pâ‡©1 âˆª wrap Bâ‡©1) (Pâ‡©2 âˆª wrap Bâ‡©2) {} {u} (V - {u})" .

have 2: "(V - {u}) âˆ© L â‰  {} âŸ¹ âˆ€BâˆˆPâ‡©1 âˆª wrap Bâ‡©1 âˆª wrap {}. B âˆ© L â‰  {}"
using invrules(2) unfolding wrap_empty by blast

from invrules(3) obtain f where f_def: "bij_betw f Pâ‡©1 (â‹ƒ (Pâ‡©2 âˆª wrap Bâ‡©2))" "âˆ€BâˆˆPâ‡©1. c < W B + w (f B)" unfolding bij_exists_def by blast
have "u âˆ‰ (â‹ƒ (Pâ‡©2 âˆª wrap Bâ‡©2))" using invâ‡©1E(2)[OF invrules(1)] assms(3) by blast
have "(â‹ƒ (Pâ‡©2 âˆª wrap Bâ‡©2 âˆª wrap {u})) = (â‹ƒ (Pâ‡©2 âˆª wrap Bâ‡©2 âˆª {{u}}))" unfolding wrap_def by simp
also have "... = (â‹ƒ (Pâ‡©2 âˆª wrap Bâ‡©2)) âˆª {u}" by simp
finally have UN: "(â‹ƒ (Pâ‡©2 âˆª wrap Bâ‡©2 âˆª wrap {u})) = (â‹ƒ (Pâ‡©2 âˆª wrap Bâ‡©2)) âˆª {u}" .
have "wrap Bâ‡©1 = {Bâ‡©1}" using wrap_not_empty[of Bâ‡©1] assms(2) by simp
let ?f = "f (Bâ‡©1 := u)"
have BIJ: "bij_betw ?f (Pâ‡©1 âˆª wrap Bâ‡©1) (â‹ƒ (Pâ‡©2 âˆª wrap Bâ‡©2 âˆª wrap {u}))"
by (metis (no_types, lifting) bij_betw_cong fun_upd_other fun_upd_same notIn_Un_bij_betw3)
have "c < W Bâ‡©1 + w (?f Bâ‡©1)" using assms(4) by simp
then have "(âˆ€BâˆˆPâ‡©1 âˆª wrap Bâ‡©1. c < W B + w (?f B))"
unfolding â€¹wrap Bâ‡©1 = {Bâ‡©1}â€º using f_def(2) by simp
with BIJ have "bij_betw ?f (Pâ‡©1 âˆª wrap Bâ‡©1) (â‹ƒ (Pâ‡©2 âˆª wrap Bâ‡©2 âˆª wrap {u}))
âˆ§ (âˆ€BâˆˆPâ‡©1 âˆª wrap Bâ‡©1. c < W B + w (?f B))" by blast
then have 3: "bij_exists (Pâ‡©1 âˆª wrap Bâ‡©1) (â‹ƒ (Pâ‡©2 âˆª wrap Bâ‡©2 âˆª wrap {u}))"
unfolding bij_exists_def by blast

have 4: "2 * card (Pâ‡©2 âˆª wrap Bâ‡©2) â‰¤ card (â‹ƒ (Pâ‡©2 âˆª wrap Bâ‡©2))"
proof -
note bprules = bpE[OF invâ‡©1E(1)[OF invrules(1)]]
have "pairwise disjnt (Pâ‡©2 âˆª wrap Bâ‡©2)"
using bprules(1) pairwise_subset by blast
moreover have "Bâ‡©2 âˆ‰ Pâ‡©2" using invâ‡©1E(4)[OF invrules(1)]  by simp
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 (â‹ƒPâ‡©2)" using U_Finite bprules(3) by auto
have "finite Bâ‡©2" using invâ‡©1E(1)[OF invrules(1)] bp_bins_finite wrap_not_empty by blast

have "2 * card (Pâ‡©2 âˆª wrap Bâ‡©2) â‰¤ 2 * (card Pâ‡©2 + card (wrap Bâ‡©2))"
using card_Un_le[of Pâ‡©2 â€¹wrap Bâ‡©2â€º] by simp
also have "... â‰¤ 2 * card Pâ‡©2 + 2" using wrap_card by auto
also have "... â‰¤ card (â‹ƒ Pâ‡©2) + 2" using invrules(4) by simp
also have "... â‰¤ card (â‹ƒ Pâ‡©2) + card Bâ‡©2" using Bâ‡©2_at_least_two_objects[OF assms(1,3,5)] by simp
also have "... = card (â‹ƒ (Pâ‡©2 âˆª {Bâ‡©2}))" using DISJNT card_Un_disjoint[OF â€¹finite (â‹ƒPâ‡©2)â€º â€¹finite Bâ‡©2â€º] by (simp add: Un_commute)
also have "... = card (â‹ƒ (Pâ‡©2 âˆª wrap Bâ‡©2))" by (cases â€¹Bâ‡©2 = {}â€º) auto
finally show ?thesis .
qed
from invâ‡©2I[OF 1 2 3 4] have "invâ‡©2 (Pâ‡©1 âˆª wrap Bâ‡©1) (Pâ‡©2 âˆª wrap Bâ‡©2) {} {u} (V - {u})" .

from invâ‡©3I[OF this] show ?thesis using assms(3) by blast
qed

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

then show ?case
using LWEIGHT loop_stepA[OF INV _ _ IN] loop_stepB[OF INV _ LIN] loop_stepC[OF INV _ IN]
and loop_stepD[OF INV _ IN] loop_stepE[OF INV _ IN] by (cases â€¹Bâ‡©1 = {}â€º, cases â€¹V âˆ© L = {}â€º) auto
next
show ?case by blast
qed

end (* BinPacking *)

subsection â€¹The Full Linear Time Version of the Proposed Algorithmâ€º

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

locale BinPacking_Complete =
fixes U :: "'a set" â€• â€¹A finite, non-empty set of objectsâ€º
and w :: "'a â‡’ real" â€• â€¹A mapping from objects to their respective weights (positive real numbers)â€º
and c :: nat â€• â€¹The maximum capacity of a bin (as a natural number)â€º
assumes weight: "âˆ€u âˆˆ U. 0 < w(u) âˆ§ w(u) â‰¤ c"
and U_Finite: "finite U"
and U_NE: "U â‰  {}"
begin

text â€¹The correctness proofs will be identical to the ones of the simplified algorithm.â€º

abbreviation W :: "'a set â‡’ real" where
"W B â‰¡ (âˆ‘u âˆˆ B. w(u))"

definition bp :: "'a set set â‡’ bool" where
"bp P âŸ· partition_on U P âˆ§ (âˆ€B âˆˆ P. W(B) â‰¤ c)"

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

lemma bpI:
assumes "pairwise disjnt P" "{} âˆ‰ P" "â‹ƒP = U" "âˆ€B âˆˆ P. W(B) â‰¤ c"
shows "bp P"
using assms unfolding bp_def partition_on_def by blast

definition invâ‡©1 :: "'a set set â‡’ 'a set set â‡’ 'a set â‡’ 'a set â‡’ 'a set â‡’ bool" where
"invâ‡©1 Pâ‡©1 Pâ‡©2 Bâ‡©1 Bâ‡©2 V âŸ· bp (Pâ‡©1 âˆª wrap Bâ‡©1 âˆª Pâ‡©2 âˆª wrap Bâ‡©2 âˆª {{v} |v. v âˆˆ V}) â€• â€¹A correct solution to the bin packing problemâ€º
âˆ§ â‹ƒ(Pâ‡©1 âˆª wrap Bâ‡©1 âˆª Pâ‡©2 âˆª wrap Bâ‡©2) = U - V â€• â€¹The partial solution does not contain objects that have not yet been assignedâ€º
âˆ§ Bâ‡©1 âˆ‰ (Pâ‡©1 âˆª Pâ‡©2 âˆª wrap Bâ‡©2) â€• â€¹â€¹Bâ‡©1â€º is distinct from all the other binsâ€º
âˆ§ Bâ‡©2 âˆ‰ (Pâ‡©1 âˆª wrap Bâ‡©1 âˆª Pâ‡©2) â€• â€¹â€¹Bâ‡©2â€º is distinct from all the other binsâ€º
âˆ§ (Pâ‡©1 âˆª wrap Bâ‡©1) âˆ© (Pâ‡©2 âˆª wrap Bâ‡©2) = {} â€• â€¹The first and second partial solutions are disjoint from each other.â€º"

shows "bp (Pâ‡©1 âˆª wrap Bâ‡©1 âˆª Pâ‡©2 âˆª wrap Bâ‡©2 âˆª {{v} |v. v âˆˆ V})"
and "â‹ƒ(Pâ‡©1 âˆª wrap Bâ‡©1 âˆª Pâ‡©2 âˆª wrap Bâ‡©2) = U - V"
using assms unfolding invâ‡©1_def by auto

assumes "bp (Pâ‡©1 âˆª wrap Bâ‡©1 âˆª Pâ‡©2 âˆª wrap Bâ‡©2 âˆª {{v} |v. v âˆˆ V})"
and "â‹ƒ(Pâ‡©1 âˆª wrap Bâ‡©1 âˆª Pâ‡©2 âˆª wrap Bâ‡©2) = U - V"
using assms unfolding invâ‡©1_def by blast

lemma wrap_Un [simp]: "wrap (M âˆª {x}) = {M âˆª {x}}" unfolding wrap_def by simp
lemma wrap_empty [simp]: "wrap {} = {}" unfolding wrap_def by simp
lemma wrap_not_empty [simp]: "M â‰  {} âŸ· wrap M = {M}" unfolding wrap_def by simp

proof -
note invrules = invâ‡©1E[OF assms(1)] and bprules = bpE[OF invrules(1)]

â€• â€¹Rule 1: Pairwise Disjointâ€º
have NOTIN: "âˆ€M âˆˆ Pâ‡©1 âˆª wrap Bâ‡©1 âˆª Pâ‡©2 âˆª wrap Bâ‡©2 âˆª {{v} |v. v âˆˆ V - {u}}. u âˆ‰ M"
using invrules(2) assms(2) by blast
have "{{v} |v. v âˆˆ V} = {{u}} âˆª {{v} |v. v âˆˆ V - {u}}"
using assms(2) by blast
then have "pairwise disjnt (Pâ‡©1 âˆª wrap Bâ‡©1 âˆª Pâ‡©2 âˆª wrap Bâ‡©2 âˆª ({{u}} âˆª {{v} |v. v âˆˆ V - {u}}))"
using bprules(1) assms(2) by simp
then have "pairwise disjnt (wrap Bâ‡©1 âˆª {{u}} âˆª Pâ‡©1 âˆª Pâ‡©2 âˆª wrap Bâ‡©2 âˆª {{v} |v. v âˆˆ V - {u}})" by (simp add: Un_commute)
then have assm: "pairwise disjnt (wrap Bâ‡©1 âˆª {{u}} âˆª (Pâ‡©1 âˆª Pâ‡©2 âˆª wrap Bâ‡©2 âˆª {{v} |v. v âˆˆ V - {u}}))" by (simp add: Un_assoc)
have "pairwise disjnt ({Bâ‡©1 âˆª {u}} âˆª (Pâ‡©1 âˆª Pâ‡©2 âˆª wrap Bâ‡©2 âˆª {{v} |v. v âˆˆ V - {u}}))"
proof (cases â€¹Bâ‡©1 = {}â€º)
case True with assm show ?thesis by simp
next
case False
with assm have assm: "pairwise disjnt ({Bâ‡©1} âˆª {{u}} âˆª (Pâ‡©1 âˆª Pâ‡©2 âˆª wrap Bâ‡©2 âˆª {{v} |v. v âˆˆ V - {u}}))" by simp
from NOTIN have "{u} âˆ‰ Pâ‡©1 âˆª Pâ‡©2 âˆª wrap Bâ‡©2 âˆª {{v} |v. v âˆˆ V - {u}}" by blast
from pairwise_disjnt_Un[OF assm _ this] invrules(2,3) show ?thesis
using False by auto
qed
then have 1: "pairwise disjnt (Pâ‡©1 âˆª wrap (Bâ‡©1 âˆª {u}) âˆª Pâ‡©2 âˆª wrap Bâ‡©2 âˆª {{v} |v. v âˆˆ V - {u}})"
unfolding wrap_Un by simp

â€• â€¹Rule 2: No empty setsâ€º
from bprules(2) have 2: "{} âˆ‰ Pâ‡©1 âˆª wrap (Bâ‡©1 âˆª {u}) âˆª Pâ‡©2 âˆª wrap Bâ‡©2 âˆª {{v} |v. v âˆˆ V - {u}}"
unfolding wrap_def by simp

â€• â€¹Rule 3: Union preservedâ€º
from bprules(3) have "â‹ƒ (Pâ‡©1 âˆª wrap Bâ‡©1 âˆª Pâ‡©2 âˆª wrap Bâ‡©2 âˆª {{u}} âˆª {{v} |v. v âˆˆ V - {u}}) = U"
using assms(2) by blast
then have 3: "â‹ƒ (Pâ‡©1 âˆª wrap (Bâ‡©1 âˆª {u}) âˆª Pâ‡©2 âˆª wrap Bâ‡©2 âˆª {{v} |v. v âˆˆ V - {u}}) = U"
unfolding wrap_def by force

â€• â€¹Rule 4: Weights below capacityâ€º
have "0 < w u" using weight assms(2) bprules(3) by blast
have "finite Bâ‡©1" using bprules(3) U_Finite by (cases â€¹Bâ‡©1 = {}â€º) auto
then have "W (Bâ‡©1 âˆª {u}) â‰¤ W Bâ‡©1 + w u" using â€¹0 < w uâ€º by (cases â€¹u âˆˆ Bâ‡©1â€º) (auto simp: insert_absorb)
also have "... â‰¤ c" using assms(3) .
finally have "W (Bâ‡©1 âˆª {u}) â‰¤ c" .
then have "âˆ€B âˆˆ wrap (Bâ‡©1 âˆª {u}). W B â‰¤ c" unfolding wrap_Un by blast
moreover have "âˆ€BâˆˆPâ‡©1 âˆª Pâ‡©2 âˆª wrap Bâ‡©2 âˆª {{v} |v. v âˆˆ V - {u}}. W B â‰¤ c"
using bprules(4) by blast
ultimately have 4: "âˆ€BâˆˆPâ‡©1 âˆª wrap (Bâ‡©1 âˆª {u}) âˆª Pâ‡©2 âˆª wrap Bâ‡©2 âˆª {{v} |v. v âˆˆ V - {u}}. W B â‰¤ c" by blast
from bpI[OF 1 2 3 4] have 1: "bp (Pâ‡©1 âˆª wrap (Bâ‡©1 âˆª {u}) âˆª Pâ‡©2 âˆª wrap Bâ‡©2 âˆª {{v} |v. v âˆˆ V - {u}})" .

â€• â€¹Auxiliary information is preservedâ€º
have "u âˆˆ U" using assms(2) bprules(3) by blast
then have R: "U - (V - {u}) = U - V âˆª {u}" by blast
have L: "â‹ƒ (Pâ‡©1 âˆª wrap (Bâ‡©1 âˆª {u}) âˆª Pâ‡©2 âˆª wrap Bâ‡©2) = â‹ƒ (Pâ‡©1 âˆª wrap Bâ‡©1 âˆª Pâ‡©2 âˆª wrap Bâ‡©2) âˆª {u}"
unfolding wrap_def using NOTIN by auto
have 2: "â‹