Theory Approx_LB_Hoare

section ‹Load Balancing›

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

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

hide_const (open) sorted

(* TODO: mv *)

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

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

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

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

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

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

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

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

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

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

subsection ‹Formalization of a Correct Load Balancing›

subsubsection ‹Definition›

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

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

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

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

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

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

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

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

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

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

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

subsubsection ‹Lower Bounds for the Makespan›

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

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

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

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

subsection ‹The Greedy Approximation Algorithm›

text ‹This function will perform a linear scan from k ∈ {1..m}› and return the index of the machine with minimum load assuming m > 0›
fun 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)]

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

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

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

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

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

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

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

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

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

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

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

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

lemma min_avg: "m * T (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 inv1 :: "(nat  nat)  (nat  nat set)  nat  bool" where
  "inv1 T A j = (lb T A j  j  n  (T' A'. lb T' A' j  makespan T  2 * makespan T'))"

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

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

lemma inv1_step:
  assumes "inv1 T A j" "j < n"
  shows "inv1 (T ((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 inv1 ?T ?A _)
proof -
  note invrules = inv1E[OF assms(1)]
  ― ‹Greedy is correct›
  have LB: "lb ?T ?A (Suc j)"
    using add_job[OF invrules(1) min_in_range[OF m_gt_0]] by blast
  ― ‹Greedy maintains approximation factor›
  have MK: "T' A'. lb T' A' (Suc j)  makespan ?T  2 * makespan T'"
  proof rule+
    fix T1 A1 assume "lb T1 A1 (Suc j)"
    from smaller_optimum[OF this]
    obtain T0 A0 where "lb T0 A0 j" "makespan T0  makespan T1" by blast
    then have IH: "makespan T  2 * makespan T1"
      using invrules(3) by force
    show "makespan ?T  2 * makespan T1"
    proof (cases makespan ?T = T (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 T1"
        using job_dist_lower_bound_makespan[OF lb T0 A0 j] 
          and makespan T0  makespan T1 by linarith
      moreover have "t (Suc j)  makespan T1"
        using job_lower_bound_makespan[OF lb T1 A1 (Suc j)] by simp
      ultimately show ?thesis unfolding True by simp
    next
      case False show ?thesis using remove_small_job[OF False] IH by simp
    qed
  qed
  from inv1I[OF LB _ MK] show ?thesis using assms(2) by simp
qed

lemma simple_greedy_approximation:
"VARS T A i j
{True}
T := (λ_. 0);
A := (λ_. {});
j := 0;
WHILE j < n INV {inv1 T A j} DO
  i := 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 inv1_def)
next
  case (2 T A i j)
  then show ?case using inv1_step by simp
next
  case (3 T A i j)
  then show ?case unfolding inv1_def by force
qed

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

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

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

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

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

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

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

lemma min_zero:
  assumes "x  {1..k}" "T x = 0"
  shows "T (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 inv2 :: "(nat  nat)  (nat  nat set)  nat  bool" where
  "inv2 T A j = (lb T A j  j  n
                 (T' A'. lb T' A' j  makespan T  3 / 2 * makespan T') 
                 (x > j. T x = 0)
                 (j  m  makespan T = Max0 (t ` {1..j})))"

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

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

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

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

  ― ‹Greedy is trivially optimal›
  from IN_RANGE T (Suc j) = 0 have "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_Max0[OF min_in_range[OF m_gt_0]] invrules(5) False
  have TRIV: "makespan ?T = Max0 (t ` {1..Suc j})" unfolding f_Max0_equiv[symmetric] by simp
  have MK: "T' A'. lb T' A' (Suc j)  makespan ?T  3 / 2 * makespan T'"
    by (auto simp: TRIV[folded f_Max0_equiv]
            dest!: max_job_lower_bound_makespan[folded f_Max0_equiv])

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

lemma sorted_greedy_approximation:
"sorted n  VARS T A i j
{True}
T := (λ_. 0);
A := (λ_. {});
j := 0;
WHILE j < n INV {inv2 T A j} DO
  i := 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 inv2_def)
next
  case (2 T A i j)
  then show ?case using inv2_step by simp
next
  case (3 T A i j)
  then show ?case unfolding inv2_def by force
qed

end (* LoadBalancing *)

end (* Theory *)