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
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)
lemma f_Max⇩0_correct:
"∀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
lemma f_Max⇩0_mono:
"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
lemma f_Max⇩0_out_of_range [simp]:
"x ∉ {1..k} ⟹ f_Max⇩0 (T (x := y)) k = f_Max⇩0 T k"
by (induction k) auto
lemma fun_upd_f_Max⇩0:
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 =
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 = {})
∧ (⋃x ∈ {1..m}. A x) = {1..j}
∧ (∀x ∈ {1..m}. (∑j ∈ A x. t j) = T x) )"
abbreviation makespan :: "(nat ⇒ nat) ⇒ nat" where
"makespan T ≡ f_Max⇩0 T m"
lemma makespan_def': "makespan T = Max (T ` {1..m})"
using m_gt_0 by (simp add: f_Max⇩0_equiv)
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_arg :: "(nat ⇒ nat) ⇒ nat ⇒ nat" where
"min_arg T 0 = 1"
| "min_arg T (Suc x) =
(let k = min_arg T x
in if T (Suc x) < T k then (Suc x) else k)"
lemma min_correct:
"∀x ∈ {1..m}. T (min_arg T m) ≤ T x"
by (induction m) (auto simp: Let_def le_Suc_eq, force)
lemma min_in_range:
"k > 0 ⟹ (min_arg T k) ∈ {1..k}"
by (induction k) (auto simp: Let_def, force+)
lemma add_job:
assumes "lb T A j" "x ∈ {1..m}"
shows "lb (T (x := T x + t (Suc j))) (A (x := A x ∪ {Suc j})) (Suc j)"
(is ‹lb ?T ?A _›)
proof -
note lbrules = lbE[OF assms(1)]
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
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}" .
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})"
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
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}" .
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
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_arg 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'))"
lemma inv⇩1E:
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+
lemma inv⇩1I:
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
lemma inv⇩1_step:
assumes "inv⇩1 T A j" "j < n"
shows "inv⇩1 (T ((min_arg T m) := T (min_arg T m) + t (Suc j)))
(A ((min_arg T m) := A (min_arg T m) ∪ {Suc j})) (Suc j)"
(is ‹inv⇩1 ?T ?A _›)
proof -
note invrules = inv⇩1E[OF assms(1)]
have LB: "lb ?T ?A (Suc j)"
using add_job[OF invrules(1) min_in_range[OF m_gt_0]] by blast
have MK: "∀T' A'. lb T' A' (Suc j) ⟶ makespan ?T ≤ 2 * makespan T'"
proof rule+
fix T⇩1 A⇩1 assume "lb T⇩1 A⇩1 (Suc j)"
from smaller_optimum[OF this]
obtain T⇩0 A⇩0 where "lb T⇩0 A⇩0 j" "makespan T⇩0 ≤ makespan T⇩1" by blast
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_arg T m) + t (Suc j)›)
case True
have "m * T (min_arg 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_arg T m) ≤ (∑i ∈ {1..j}. t i)"
by (auto dest: of_nat_mono)
with m_gt_0 have "T (min_arg T m) ≤ (∑i ∈ {1..j}. t i) / m"
by (simp add: field_simps)
then have "T (min_arg T m) ≤ makespan T⇩1"
using job_dist_lower_bound_makespan[OF ‹lb T⇩0 A⇩0 j›]
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_arg 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 -
note lbrules = lbE[OF assms(1)]
obtain j⇩1 j⇩2 x where *:
"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
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)
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_arg 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_arg 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_arg 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})))"
lemma inv⇩2E:
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+
lemma inv⇩2I:
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
lemma inv⇩2_step:
assumes "sorted n" "inv⇩2 T A j" "j < n"
shows "inv⇩2 (T (min_arg T m := T(min_arg T m) + t(Suc j)))
(A (min_arg T m := A(min_arg 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)]
have LB: "lb ?T ?A (Suc j)"
using add_job[OF invrules(1) min_in_range[OF m_gt_0]] by blast
have MK: "∀T' A'. lb T' A' (Suc j) ⟶ makespan ?T ≤ 3 / 2 * makespan T'"
proof rule+
fix T⇩1 A⇩1 assume "lb T⇩1 A⇩1 (Suc j)"
from smaller_optimum[OF this]
obtain T⇩0 A⇩0 where "lb T⇩0 A⇩0 j" "makespan T⇩0 ≤ makespan T⇩1" by blast
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_arg T m) + t (Suc j)›)
case True
have "m * T (min_arg 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_arg T m) ≤ (∑i ∈ {1..j}. t i)"
by (auto dest: of_nat_mono)
with m_gt_0 have "T (min_arg T m) ≤ (∑i ∈ {1..j}. t i) / m"
by (simp add: field_simps)
then have "T (min_arg T m) ≤ makespan T⇩1"
using job_dist_lower_bound_makespan[OF ‹lb T⇩0 A⇩0 j›]
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
have LB: "lb ?T ?A (Suc j)"
using add_job[OF invrules(1) min_in_range[OF m_gt_0]] by blast
from IN_RANGE ‹T (Suc j) = 0› have "min_arg 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_arg 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]
dest!: max_job_lower_bound_makespan[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_arg 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
end