Theory Tables_nat

theory Tables_nat
imports Tables_real
begin

declare le_of_int_ceiling[simp] (* MOVE *)

(* Final version with l :: nat in fully localized form, no duplication *)

locale TableInv = Table0 f1 f2 f1' f2' e c for f1 f2 f1' f2' e c :: real +
fixes l0 :: nat
assumes l0f2e: "l0 ≥ 1/(f2 * (e-1))"
assumes l0f1c: "l0 ≥ 1/(f1 * (c-1))"

assumes l0f2f1e: "l0 ≥ f1/(f2 - f1*e)"
assumes l0f2f1c: "l0 ≥ f2/(f2 - f1*c)"
begin

lemma l0_gr0[arith]: "l0 > 0"
proof -
  have "0 < 1/(f2*(e-1))" by(simp)
  also note l0f2e
  finally show ?thesis by simp
qed

lemma f1_l0: assumes "l0 ≤ l/c" shows "f1*(l/c) ≤ f1*l - 1"
proof -
  have "1 = f1*((c-1)/c)*(c*(1/(f1*(c-1))))"
    using f1'_le_f2' f2'_less_f2 by(simp add: field_simps)
  also note l0f1c
  also have l': "c*l0 ≤ l" using assms(1) by(simp add: field_simps)
  finally show ?thesis by(simp add: divide_le_cancel) (simp add: field_simps)
qed

fun nxt :: "op⇩t⇩b ⇒ nat*nat ⇒ nat*nat" where
"nxt Ins (n,l) =
 (n+1, if n+1 ≤ f2*l then l else nat⌈e*l⌉)" |
"nxt Del (n,l) =
 (n-1, if f1*l ≤ real(n-1) then l else if l0 ≤ ⌊l/c⌋ then nat⌊l/c⌋ else l)"

fun T :: "op⇩t⇩b ⇒ nat*nat ⇒ real" where
"T Ins (n,l) = (if n+1 ≤ f2*l then 1 else n+1)" |
"T Del (n,l) = (if f1*l ≤ real(n-1) then 1 else if l0 ≤ ⌊l/c⌋ then n else 1)"

fun invar :: "nat * nat ⇒ bool" where
"invar(n,l) = (l ≥ l0 ∧ (⌊l/c⌋ ≥ l0 ⟶ f1*l ≤ n) ∧ n ≤ f2*l)"

lemma invar_init: "invar (0,l0)"
by (auto simp: le_floor_iff field_simps)

lemma invar_pres: assumes "invar s" shows "invar(nxt f s)"
proof -
  obtain n l where [simp]: "s = (n,l)" by fastforce
  from assms have "l0 ≤ l" and "n ≤ f2*l" by auto
  show ?thesis
  proof (cases f)
    case [simp]: Ins
    show ?thesis
    proof cases
      assume "n+1 ≤ f2*l" thus ?thesis using assms by (auto)
    next
      assume 0: "¬ n+1 ≤ f2*l"
      have f1: "f1 * ⌈e*l⌉ ≤ n+1"
      proof -
        have "⌈e*l⌉ ≤ e*l + 1" by linarith
        hence "f1 * ⌈e*l⌉ ≤ f1 * (e*l + 1)" by simp
        also have "… ≤ f2*l"
        proof -
          have "f1 ≤ (f2 - f1*e)*l0"
            using l0f2f1e f1f2e by(simp add: field_simps)
          also note ‹l0 ≤ l›
          finally show ?thesis using f1f2e[simplified field_simps]
            by (simp add:ac_simps mult_left_mono) (simp add:algebra_simps)
       qed
       finally show ?thesis using 0 by linarith
      qed
      have "n+1 ≤ f2*e*l"
      proof -
        have "n+1 ≤ f2*l+1" using ‹n ≤ f2*l› by linarith
        also have "1 = f2*(e-1)*(1/(f2*(e-1)))" by(simp)
        also note l0f2e
        also note ‹l0 ≤ l›
        finally show ?thesis by simp (simp add: algebra_simps)
      qed
      also have "f2*e*l ≤ f2*⌈e*l⌉" by simp
      finally have f2: "n+1 ≤ f2*⌈e*l⌉" .
      have "l < e*l" using ‹l0 ≤ l› by simp
      hence "l0 ≤ e*l" using ‹l0≤l› by linarith
      with 0 f1 f2 show ?thesis by (auto simp add: field_simps) linarith
    qed
  next
    case [simp]: Del
    show ?thesis
    proof cases
      assume "f1*l ≤ real n - 1"
      thus ?thesis using assms by(auto)
    next
      assume 0: "¬ f1*l ≤ real n - 1"
      show ?thesis
      proof cases
        assume "n=0" thus ?thesis using 0 assms by(simp add: field_simps)
      next
        assume "n ≠ 0"
        show ?thesis
        proof cases
          assume l: "l0 ≤ ⌊l/c⌋"
          hence l': "l0 ≤ l/c" by linarith
          have "f1 * ⌊l/c⌋ ≤ f1*(l/c)" by(simp del: times_divide_eq_right)
          hence f1: "f1*⌊l/c⌋ ≤ n-1" using l' f1_l0[OF l'] assms ‹n ≠ 0›
            by(simp add: le_floor_iff)
          have "n-1 ≤ f2 * ⌊l/c⌋"
          proof -
            have "n-1 < f1*l" using 0 ‹n ≠ 0› by linarith
            also have "f1*l ≤ f2*(l/c) - f2"
            proof -
              have "(f2 - f1*c)*l0 ≥ f2"
                using l0f2f1c f1cf2 by(simp add: field_simps)
              with mult_left_mono[OF ‹l0 ≤ l/c›, of "f2-f1*c"] f1cf2
              have "(f2 - f1*c)*(l/c) ≥ f2" by linarith
              thus ?thesis by(simp add: field_simps)
            qed
            also have "… ≤ f2*⌊l/c⌋"
            proof -
              have "l/c - 1 ≤ ⌊l/c⌋" by linarith
              from mult_left_mono[OF this, of f2] show ?thesis
                by(simp add: algebra_simps)
            qed
            finally show ?thesis using 0 ‹n ≠ 0› by linarith
          qed
          with l 0 f1 ‹n ≠ 0› show ?thesis by (auto)
        next
          assume "¬ l0 ≤ ⌊l/c⌋"
          with 0 assms show ?thesis by (auto simp add: field_simps)
        qed
      qed
    qed
  qed
qed

end

locale Table1 = TableInv +
assumes f2f2': "l0 ≥ 1/(f2 - f2')"
assumes f1'f1: "l0 ≥ 1/((f1' - f1)*c)"
begin

definition "ai = f2/(f2-f2')"
definition "ad = f1/(f1'-f1)"

lemma aigr0[arith]: "ai > 1"
using f2'_less_f2 by(simp add: ai_def field_simps)

lemma adgr0[arith]: "ad > 0"
using f1_less_f1' by(simp add: ad_def field_simps)

lemma f1'ad[arith]: "f1'*ad > 0"
by simp

lemma f2'ai[arith]: "f2'*ai > 0"
by simp

fun Φ :: "nat * nat ⇒ real" where
"Φ (n,l) = (if n ≥ f2'*l then ai*(n - f2'*l) else
  if n ≤ f1'*l ∧ l0 ≤ ⌊l/c⌋ then ad*(f1'*l - n) else 0)"

lemma Phi_Psi: "Φ (n,l) = Ψ (l0 ≤ ⌊l/c⌋) ai ad (f1'*l) (f2'*l) n"
by(simp)

abbreviation "U ≡ λf _. case f of Ins ⇒ ai+1 + f1'*ad | Del ⇒ ad+1 + f2'*ai"

interpretation tb: Amortized
  where init = "(0,l0)" and nxt = nxt
  and inv = invar
  and T = T and Φ = Φ
  and U = U
proof (standard, goal_cases)
  case 1 show ?case by (fact invar_init)
next
  case 2 thus ?case by(fact invar_pres)
next
  case (3 s) thus ?case by(cases s)(simp split: if_splits)
next
  case 4 show ?case
    by(auto simp: field_simps mult_le_0_iff le_floor_iff)
next
  case (5 s f)
  obtain n l where [simp]: "s = (n,l)" by fastforce
  show ?case
  proof (cases f)
    case [simp]: Ins
    show ?thesis (is "?A ≤ _")
    proof cases
      assume "n+1 ≤ f2*l"
      hence "?A ≤ ai+1" by(simp del: Φ.simps Ψ.simps add: Phi_Psi Psi_diff_Ins)
      thus ?thesis by simp
    next
      assume [arith]: "¬ n+1 ≤ f2*l"
      have [arith]: "l ≥ l0"  "n ≤ f2*l" using 5 by auto
      have "(f2 - f2')*l ≥ 1"
        using mult_mono[OF order_refl, of l0 l "f2-f2'"] f2'_less_f2 f2f2'
        by (simp add: field_simps)
      hence "n ≥ f2'*l" by(simp add: algebra_simps)
      hence Phi: "Φ s = ai * (n - f2'*l)" by simp
      have [simp]: "real (nat ⌈e*l⌉) = real_of_int ⌈e*l⌉"
        by (simp add: order.order_iff_strict)
      have "?A ≤ n - ai*(f2 - f2')*l + ai + 1 + f1'*ad" (is "_ ≤ ?R")
      proof cases
        assume f2': "n+1 < f2'*⌈e*l⌉"
        show ?thesis
        proof cases
          assume "n+1 ≤ f1'*⌈e*l⌉"
          hence "?A ≤ n+1 + ad*(f1'*⌈e*l⌉-(n+1)) - ai*(n - f2'*l)"
            using Phi f2' by simp
          also have "f1'*⌈e*l⌉ - (n+1) ≤ f1'"
          proof -
            have "f1'*⌈e*l⌉ ≤ f1'*(e*l + 1)" by(simp)
            also have "… = f1'*e*l + f1'" by(simp add: algebra_simps)
            also have "f1'*e*l ≤ f2*l" using f1'ef2 by(simp)
            finally show ?thesis by linarith
          qed
          also have "n+1+ad*f1'-ai*(n-f2'*l) = n+ai*(-real(n+1)+f2'*l)+ai+f1'*ad+1"
            by(simp add: algebra_simps)
          also have "-real(n+1) ≤ -f2*l" by linarith
          finally show ?thesis by(simp add: algebra_simps) (* f1'*ad *)
        next
          assume "¬ n+1 ≤ f1'*⌈e*l⌉"
          hence "?A = n+1 - ai*(n - f2'*l)" using Phi f2' by (simp)
          also have "n+1-ai*(n-f2'*l) = n+ai*(-real(n+1)+f2'*l)+ai+1"
            by(simp add: algebra_simps)
          also have "-real(n+1) ≤ -f2*l" by linarith
          also have "n+ai*(-f2*l+f2'*l)+ai+1 ≤ ?R"
            by(simp add: algebra_simps)
          finally show ?thesis by(simp)
        qed
      next
        assume "¬ n+1 < f2'*⌈e*l⌉"
        hence "?A = n + ai*(-f2'*⌈e*l⌉ + f2'*l) + ai+1" using Phi
          by(simp add: algebra_simps)
        also have "-f2'*⌈e*l⌉ ≤ -f2'*e*l" by(simp)
        also have "-f2'*e ≤ -f2" using f2_le_f2'e by linarith
        also have "n+ai*(-f2*l+f2'*l)+ai+1 ≤ ?R" by(simp add: algebra_simps)
        finally show ?thesis by(simp)
      qed
      also have "… = n - f2*l + ai+f1'*ad+1" using f2'_less_f2
        by(simp add: ai_def)
      finally show ?thesis by simp
    qed
  next
    case [simp]: Del
    have [arith]: "l ≥ l0" using 5 by simp
    show ?thesis
    proof cases
      assume "n=0" with 5 show ?thesis
        by(simp add: mult_le_0_iff field_simps)
    next
      assume [arith]: "n≠0"
      show ?thesis (is "?A ≤ _")
      proof cases
        assume "real n - 1 ≥ f1*l ∨ ⌊l/c⌋ < l0"
        hence "?A ≤ ad+1" using f1'_le_f2'
          by(auto simp del: Φ.simps Ψ.simps simp add: Phi_Psi Psi_diff_Del)
        thus ?thesis by simp
      next
        assume "¬ (real n - 1 ≥ f1*l ∨ ⌊l/c⌋ < l0)"
        hence n: "real n - 1 < f1*l" and lc': "⌊l/c⌋ ≥ l0" and lc: "l/c ≥ l0"
          by linarith+
        have "f1'*l ≤ f2'*l" using f1'_le_f2' by simp
        have "(f1' - f1)*l ≥ 1" using mult_mono[OF order_refl, of l0 "l/c" "f1'-f1"]
          lc f1_less_f1' f1'f1 by (simp add: field_simps)
        hence "n < f1'*l" using n by(simp add: algebra_simps)
        hence Phi: "Φ s = ad*(f1'*l - n)"
          apply(simp) using ‹f1'*l ≤ f2'*l› lc by linarith
        have "?A ≤ n - ad*(f1' - f1)*l + ad + f2'*ai" (is "_ ≤ ?R + _")
        proof cases
          assume f2': "n-1 < f2'*⌊l/c⌋"
          show ?thesis
          proof cases
            assume "n-1 < f1'*⌊l/c⌋ ∧ ⌊⌊l/c⌋/c⌋ ≥ l0"
            hence "Φ (nxt f s) = ad*(f1'*⌊l/c⌋ - (n-1))" using f2' n lc' by(auto)
            hence "?A = n + ad*(f1'*⌊l/c⌋ - (n-1)) - (ad*(f1'*l - n))"
              using Phi n lc' by (simp add: algebra_simps)
            also have "⌊l/c⌋ ≤ l/c" by(simp)
            also have "n+ad*(f1'*(l/c)-(n-1))-(ad*(f1'*l-n)) = n+ad*(f1'/c-f1')*l+ad"
              by(simp add: algebra_simps)
            also note f1'c_le_f1
            finally have "?A ≤ ?R" by(simp add: algebra_simps)
            thus ?thesis by linarith
          next
            assume "¬(n-1 < f1'*⌊l/c⌋ ∧ ⌊⌊l/c⌋/c⌋ ≥ l0)"
            hence "Φ (nxt f s) = 0" using f2' n lc' by(auto)
            hence "?A = n + ad*(n - f1'*l)" using Phi n lc'
              by (simp add: algebra_simps)
            also have "… = n + ad*(n-1 - f1'*l) + ad" by(simp add: algebra_simps)
            also have "n-1 ≤ f1*l" using n by linarith
            finally have "?A ≤ ?R" by (simp add: algebra_simps)
            thus ?thesis by linarith
          qed
        next
          assume f2': "¬ n-1 < f2'*⌊l/c⌋"
          hence "?A = n + ai*(n-1-f2'*⌊l/c⌋) - ad*(f1'*l - n)"
            using Phi n lc' by (simp)
          also have "n-1-f2'*⌊l/c⌋ ≤ f2'"
          proof -
            have "f1*l ≤ f2'*(l/c)" using f1f2'c by(simp add: field_simps)
            hence "n-1 < f2'*(l/c)" using n by linarith
            also have "l/c ≤ ⌊l/c⌋ + 1" by linarith
            finally show ?thesis by(fastforce simp: algebra_simps)
          qed
          also have "n+ai*f2'-ad*(f1'*l-n) = n + ad*(n-1 - f1'*l) + ad + f2'*ai"
            by(simp add: algebra_simps)
          also have "n-1 ≤ f1*l" using n by linarith
          finally show ?thesis by(simp add: algebra_simps)
        qed
        also have "… = n - f1*l + ad + f2'*ai" using f1_less_f1' by(simp add: ad_def)
        finally show ?thesis using n by simp
      qed
    qed
  qed
qed

end

locale Table2_f1f2'' = TableInv +
fixes f1'' f2'' :: real

locale Table2 = Table2_f1f2'' +
assumes f2f2'': "(f2 - f2'')*l0 ≥ 1"
assumes f1''f1: "(f1'' - f1)*c*l0 ≥ 1"

assumes f1_less_f1'': "f1 < f1''"
assumes f1''_less_f1': "f1'' < f1'"
assumes f2'_less_f2'': "f2' < f2''"
assumes f2''_less_f2: "f2'' < f2"
assumes f1''_f1': "l ≥ real l0 ⟹ f1'' * (l+1) ≤ f1'*l"
assumes f2'_f2'': "l ≥ real l0 ⟹ f2' * l ≤ f2'' * (l-1)"
begin

definition "ai = f2 / (f2 - f2'')"
definition "ad = f1 / (f1'' - f1)"

lemma f1''_gr0[arith]: "f1'' > 0"
using f1_less_f1'' f1 by linarith

lemma f2''_gr0[arith]: "f2'' > 0"
using f2' f2'_less_f2'' by linarith

lemma aigr0[arith]: "ai > 0"
using f2''_less_f2 by(simp add: ai_def field_simps)

lemma adgr0[arith]: "ad > 0"
using f1_less_f1'' by(simp add: ad_def field_simps)

fun Φ :: "nat * nat ⇒ real" where
"Φ(n,l) = (if n ≥ f2''*l then ai*(n - f2''*l) else
  if n ≤ f1''*l ∧ l0 ≤ ⌊l/c⌋ then ad*(f1''*l - n) else 0)"

lemma Phi_Psi: "Φ (n,l) = Ψ (l0 ≤ ⌊l/c⌋) ai ad (f1''*l) (f2''*l) n"
by(simp)

abbreviation "U ≡ λf _. case f of Ins ⇒ ai+1 | Del ⇒ ad+1"

interpretation tb: Amortized
  where init = "(0,l0)" and nxt = nxt
  and inv = invar
  and T = T and Φ = Φ
  and U = U
proof (standard, goal_cases)
  case 1 show ?case by (fact invar_init)
next
  case 2 thus ?case by(fact invar_pres)
next
  case (3 s) thus ?case by(cases s)(simp split: if_splits)
next
  case 4 show ?case
    by(auto simp: field_simps mult_le_0_iff le_floor_iff)
next
  case (5 s f)
  obtain n l where [simp]: "s = (n,l)" by fastforce
  show ?case
  proof (cases f)
    case [simp]: Ins
    show ?thesis (is "?L ≤ _")
    proof cases
      assume "n+1 ≤ f2*l"
      thus ?thesis by(simp del: Φ.simps Ψ.simps add: Phi_Psi Psi_diff_Ins)
    next
      assume [arith]: "¬ n+1 ≤ f2*l"
      have [arith]: "l ≥ l0"  "n ≤ f2*l" using 5 by auto
      have "l0 ≤ e*l" using ‹l0 ≤ l› e1 mult_mono[of 1 e l0 l] by simp
      have "(f2 - f2'')*l ≥ 1"
        using mult_mono[OF order_refl, of l0 l "f2-f2''"] f2''_less_f2 f2f2''
        by (simp add: algebra_simps)
      hence "n ≥ f2''*l" by(simp add: algebra_simps)
      hence Phi: "Φ s = ai * (n - f2''*l)" by simp
      have [simp]: "real (nat ⌈e*l⌉) = real_of_int ⌈e*l⌉"
        by (simp add: order.order_iff_strict)
      have "?L ≤ n - ai*(f2 - f2'')*l + ai + 1" (is "_ ≤ ?R")
      proof cases
        assume f2'': "n+1 < f2''*⌈e*l⌉"
        have "f1''*⌈e*l⌉ ≤ f1''*(e*l + 1)" by(simp)
        also note f1''_f1'[OF ‹l0 ≤ e*l›]
        also have "f1'*(e*l) ≤ f2*l" using f1'ef2 by(simp)
        also have "f2*l ≤ n+1" by linarith
        finally have "?L ≤ n+1 - ai*(n - f2''*l)"
          using Phi f2'' by (simp)
        also have "n+1-ai*(n-f2''*l) = n+ai*(-real(n+1)+f2''*l)+ai+1"
          by(simp add: algebra_simps)
        also have "-real(n+1) ≤ -f2*l" by linarith
        finally show ?thesis by(simp add: algebra_simps)
      next
        assume "¬ n+1 < f2''*⌈e*l⌉"
        hence "?L = n + ai*(-f2''*⌈e*l⌉ + f2''*l) + ai+1" using Phi
          by(simp add: algebra_simps)
        also have "-f2''*⌈e*l⌉ ≤ -f2''*e*l" by(simp)
        also have "-f2''*e ≤ -f2'*e" using f2'_less_f2'' by(simp)
        also have "-f2'*e ≤ -f2" using f2_le_f2'e by(simp)
        also have "n+ai*(-f2*l+f2''*l)+ai+1 ≤ ?R" by(simp add: algebra_simps)
        finally show ?thesis by(simp)
      qed
      also have "… = n - f2*l + ai+1" using f2''_less_f2
        by(simp add: ai_def)
      finally show ?thesis by simp
    qed
  next
    case [simp]: Del
    have [arith]: "l ≥ l0" using 5 by simp
    show ?thesis
    proof cases
      assume "n=0" with 5 show ?thesis
        by(simp add: mult_le_0_iff field_simps)
    next
      assume [arith]: "n≠0"
      show ?thesis (is "?A ≤ _")
      proof cases
        assume "real n - 1 ≥ f1*l ∨ ⌊l/c⌋ < l0"
        thus ?thesis using f1''_less_f1' f1'_le_f2' f2'_less_f2''
          by(auto simp del: Φ.simps Ψ.simps simp add: Phi_Psi Psi_diff_Del)
      next
        assume "¬ (real n - 1 ≥ f1*l ∨ ⌊l/c⌋ < l0)"
        hence n: "real n - 1 < f1*l" and lc': "⌊l/c⌋ ≥ l0" and lc: "l/c ≥ l0"
          by linarith+
        have "f1''*l ≤ f2''*l"
          using f1''_less_f1' f1'_le_f2' f2'_less_f2'' by simp
        have "(f1'' - f1)*l ≥ 1"
          using mult_mono[OF order_refl, of l0 "l/c" "f1''-f1"] lc f1_less_f1'' f1''f1
          by (simp add: field_simps)
        hence "n < f1''*l" using n by(simp add: algebra_simps)
        hence Phi: "Φ s = ad*(f1''*l - n)"
          apply(simp) using ‹f1''*l ≤ f2''*l› lc by linarith
        have f2': "n-1 < f2''*⌊l/c⌋"
        proof -
          have "n-1 < f1*l" using n by linarith
          also have "f1*l ≤ f2'*(l/c)" using f1f2'c by(auto simp: field_simps)
          also note f2'_f2''[OF ‹l/c≥l0›]
          also have "f2''*(l/c - 1) ≤ f2''*⌊l/c⌋" by simp
          finally show ?thesis by(simp)
        qed
        have "?A ≤ n - ad*(f1'' - f1)*l + ad"
        proof cases
          assume "n-1 < f1''*⌊l/c⌋ ∧ ⌊⌊l/c⌋/c⌋ ≥ l0"
          hence "Φ (nxt f s) = ad*(f1''*⌊l/c⌋ - (n-1))" using f2' n lc' by(auto)
          hence "?A = n + ad*(f1''*⌊l/c⌋ - (n-1)) - (ad*(f1''*l - n))"
            using Phi n lc' by (simp add: algebra_simps)
          also have "⌊l/c⌋ ≤ l/c" by(simp)
          also have "n+ad*(f1''*(l/c)-(n-1))-(ad*(f1''*l-n)) = n+ad*(f1''/c-f1'')*l+ad"
            by(simp add: algebra_simps)
          also have "f1''/c ≤ f1'/c" using f1''_less_f1' by(simp add: field_simps)
          also note f1'c_le_f1
          finally show ?thesis by(simp add: algebra_simps)
        next
          assume "¬(n-1 < f1''*⌊l/c⌋ ∧ ⌊⌊l/c⌋/c⌋ ≥ l0)"
          hence "Φ (nxt f s) = 0" using f2' n lc' by(auto)
          hence "?A = n + ad*(n - f1''*l)" using Phi n lc'
            by (simp add: algebra_simps)
          also have "… = n + ad*(n-1 - f1''*l) + ad" by(simp add: algebra_simps)
          also have "n-1 ≤ f1*l" using n by linarith
          finally show ?thesis by (simp add: algebra_simps)
        qed
        also have "… = n - f1*l + ad" using f1_less_f1'' by(simp add: ad_def)
        finally show ?thesis using n by simp
      qed
    qed
  qed
qed

end


locale Table3 = Table2_f1f2'' +
assumes f1''_def: "f1'' = (f1'::real)*l0/(l0+1)"
assumes f2''_def: "f2'' = (f2'::real)*l0/(l0-1)"

(* they imply (f2 - f2'')*l0 ≥ 1 and (f1 - f1'')*l0*c ≥ 1 *)
assumes l0_f2f2': "l0 ≥ (f2+1)/(f2-f2')"
assumes l0_f1f1': "l0 ≥ (f1'*c+1)/((f1'-f1)*c)"

(* they imply f1<f1'' and f2'<f2'' and l0 > 1 *)
assumes l0_f1_f1': "l0 > f1/((f1'-f1))"
assumes l0_f2_f2': "l0 > f2/(f2-f2')"
begin

lemma l0_gr1: "l0 > 1"
proof -
  have "f2/(f2-f2') ≥ 1" using f2'_less_f2 by(simp add: field_simps)
  thus ?thesis using l0_f2_f2' f2'_less_f2 by linarith
qed

lemma f1''_less_f1': "f1'' < f1'"
by(simp add: f1''_def field_simps)

lemma f1_less_f1'': "f1 < f1''"
proof -
  have "1 + l0 > 0" by (simp add: add_pos_pos)
  hence "f1''> f1 ⟷ l0 > f1/((f1'-f1))"
    using f1_less_f1' by(simp add: f1''_def field_simps)
  also have "… ⟷ True" using l0_f1_f1' by blast
  finally show ?thesis by blast
qed

lemma f2'_less_f2'': "f2' < f2''"
using l0_gr1 by(simp add: f2''_def field_simps)

lemma f2''_less_f2: "f2'' < f2"
proof -
  have "f2''< f2 ⟷ l0 > f2/(f2-f2')"
    using f2'_less_f2 l0_gr1 by(simp add: f2''_def field_simps)
  also have "… ⟷ True" using l0_f2_f2' by blast
  finally show ?thesis by blast
qed

(* This is the real constraint we want, not l0_f2f2',
   but it involves f2'', which depends on l0 *)
lemma f2f2'': "(f2 - f2'')*l0 ≥ 1"
proof -
  have "(f2 - f2'')*(l0-1) ≥ 1"
    using l0_gr1 l0_f2f2' f2'_less_f2
    by(simp add: f2''_def algebra_simps del: of_nat_diff) (simp add: field_simps)
  thus ?thesis using f2''_less_f2 by (simp add: algebra_simps)
qed

(* This is the real constraint we want, not l0_f1f1',
   but it involves f1'', which depends on l0 *)
lemma f1''f1: "(f1'' - f1)*c*l0 ≥ 1"
proof -
  have "1 ≤ (f1' - f1)*c*l0 - f1'*c" using l0_f1f1' f1_less_f1'
    by(simp add: field_simps)
  also have "… = (f1'*((l0-1)/l0) - f1)*c*l0"
    by(simp add: field_simps)
  also have "(l0-1)/l0 ≤ l0/(l0+1)"
    by(simp add: field_simps)
  also have "f1'*(l0/(l0+1)) = f1'*l0/(l0+1)"
    by(simp add: algebra_simps)
  also note f1''_def[symmetric]
  finally show ?thesis by(simp)
qed

lemma f1''_f1': assumes "l ≥ real l0" shows "f1''*(l+1) ≤ f1' * l"
proof -
  have "f1''*(l+1) = f1'*(l0/(l0+1))*(l+1)"
    by(simp add: f1''_def field_simps)
  also have "l0/(l0+1) ≤ l/(l+1)" using assms
    by(simp add: field_simps)
  finally show ?thesis using ‹l0 ≤ l› by(simp)
qed

lemma f2'_f2'': assumes "l ≥ real l0" shows "f2' * l ≤ f2'' * (l-1)"
proof -
  have "f2' * l = f2' * l + f2'*((l0-1)/(l0-1) - 1)" using l0_gr1 by simp
  also have "(l0-1)/(l0-1) ≤ (l-1)/(l0-1)" using ‹l≥l0› by(simp)
  also have "f2'*l + f2'*((l-1)/(l0-1) - 1) = f2''*(l-1)"
    using l0_gr1 by(simp add: f2''_def field_simps)
  finally show ?thesis by simp
qed


sublocale Table2
proof
qed (fact f1_less_f1'' f1''_less_f1' f2'_less_f2'' f2''_less_f2 f1''f1 f2f2'' f1''_f1' f2'_f2'')+

end

end