Theory MFMC_Flow_Attainability

theory MFMC_Flow_Attainability imports
  MFMC_Network
begin

section ‹Attainability of flows in networks›

subsection ‹Cleaning up flows›

text ‹If there is a flow along antiparallel edges, it suffices to consider the difference.›

definition cleanup :: "'a flow  'a flow"
where "cleanup f = (λ(a, b). if f (a, b) > f (b, a) then f (a, b) - f (b, a) else 0)"

lemma cleanup_simps [simp]:
  "cleanup f (a, b) = (if f (a, b) > f (b, a) then f (a, b) - f (b, a) else 0)"
by(simp add: cleanup_def)

lemma value_flow_cleanup:
  assumes [simp]: "x. f (x, source Δ) = 0"
  shows "value_flow Δ (cleanup f) = value_flow Δ f"
unfolding d_OUT_def
by (auto simp add: not_less intro!: nn_integral_cong intro: antisym)

lemma KIR_cleanup:
  assumes KIR: "KIR f x"
  and finite_IN: "d_IN f x  "
  shows "KIR (cleanup f) x"
proof -
  from finite_IN KIR have finite_OUT: "d_OUT f x  " by simp

  have finite_IN: "(+ yA. f (y, x))  " for A
    using finite_IN by(rule neq_top_trans)(auto simp add: d_IN_def nn_integral_count_space_indicator intro!: nn_integral_mono split: split_indicator)
  have finite_OUT: "(+ yA. f (x, y))  " for A
    using finite_OUT by(rule neq_top_trans)(auto simp add: d_OUT_def nn_integral_count_space_indicator intro!: nn_integral_mono split: split_indicator)
  have finite_in: "f (x, y)  " for y using d_OUT f x  
    by(rule neq_top_trans) (rule d_OUT_ge_point)

  let ?M = "{y. f (x, y) > f (y, x)}"

  have "d_OUT (cleanup f) x = (+ y?M. f (x, y) - f (y, x))"
    by(auto simp add: d_OUT_def nn_integral_count_space_indicator intro!: nn_integral_cong)
  also have " = (+ y?M. f (x, y)) - (+ y?M. f (y, x))" using finite_IN
    by(subst nn_integral_diff)(auto simp add: AE_count_space)
  also have " = (d_OUT f x - (+ y{y. f (x, y)  f (y, x)}. f (x, y))) - (+ y?M. f (y, x))"
    unfolding d_OUT_def d_IN_def using finite_IN finite_OUT
    apply(simp add: nn_integral_count_space_indicator)
    apply(subst (2) nn_integral_diff[symmetric])
    apply(auto simp add: AE_count_space finite_in split: split_indicator intro!: arg_cong2[where f="(-)"] intro!: nn_integral_cong)
    done
  also have " = (d_IN f x - (+ y?M. f (y, x))) - (+ y{y. f (x, y)  f (y, x)}. f (x, y))"
    using KIR by(simp add: diff_diff_commute_ennreal)
  also have " = (+ y{y. f (x, y)  f (y, x)}. f (y, x)) - (+ y{y. f (x, y)  f (y, x)}. f (x, y))"
    using finite_IN finite_IN[of "{ _ }"]
    apply(simp add: d_IN_def nn_integral_count_space_indicator)
    apply(subst nn_integral_diff[symmetric])
    apply(auto simp add: d_IN_def AE_count_space split: split_indicator intro!: arg_cong2[where f="(-)"] intro!: nn_integral_cong)
    done
  also have " = (+ y{y. f (x, y)  f (y, x)}. f (y, x) - f (x, y))" using finite_OUT
    by(subst nn_integral_diff)(auto simp add: AE_count_space)
  also have " = d_IN (cleanup f) x" using finite_in
    by(auto simp add: d_IN_def nn_integral_count_space_indicator intro!: ennreal_diff_self nn_integral_cong split: split_indicator)
  finally show "KIR (cleanup f) x" .
qed

locale flow_attainability = countable_network Δ
  for Δ :: "('v, 'more) network_scheme" (structure)
  +
  assumes finite_capacity: "x. x  sink Δ  d_IN (capacity Δ) x    d_OUT (capacity Δ) x  "
  and no_loop: "x. ¬ edge Δ x x"
  and source_in: "x. ¬ edge Δ x (source Δ)"
begin

lemma source_in_not_cycle:
  assumes "cycle Δ p"
  shows "(x, source Δ)  set (cycle_edges p)"
using cycle_edges_edges[OF assms] source_in[of x] by(auto)

lemma source_out_not_cycle:
  "cycle Δ p  (source Δ, x)  set (cycle_edges p)"
by(auto dest: cycle_leave_ex_enter source_in_not_cycle)

lemma flowD_source_IN:
  assumes "flow Δ f"
  shows "d_IN f (source Δ) = 0"
proof -
  have "d_IN f (source Δ) = (+ yIN (source Δ). f (y, source Δ))"
    by(rule d_IN_alt_def)(simp add: flowD_outside[OF assms])
  also have " = (+ yIN (source Δ). 0)"
    by(rule nn_integral_cong)(simp add: source_in incoming_def)
  finally show ?thesis by simp
qed

lemma flowD_finite_IN:
  assumes f: "flow Δ f" and x: "x  sink Δ"
  shows "d_IN f x  top"
proof(cases "x = source Δ")
  case True thus ?thesis by(simp add: flowD_source_IN[OF f])
next
  case False
  from finite_capacity[OF x] show ?thesis
  proof
    assume *: "d_IN (capacity Δ) x  "
    from flowD_capacity[OF f] have "d_IN f x  d_IN (capacity Δ) x" by(rule d_IN_mono)
    also have " < " using * by (simp add: less_top)
    finally show ?thesis by simp
  next
    assume *: "d_OUT (capacity Δ) x  "
    have "d_IN f x = d_OUT f x" using flowD_KIR[OF f False x] by simp
    also have "  d_OUT (capacity Δ) x" using flowD_capacity[OF f] by(rule d_OUT_mono)
    also have " < " using * by (simp add: less_top)
    finally show ?thesis by simp
  qed
qed

lemma flowD_finite_OUT:
  assumes "flow Δ f" "x  source Δ" "x  sink Δ"
  shows "d_OUT f x  "
using flowD_KIR[OF assms] assms by(simp add: flowD_finite_IN)

end

locale flow_network = flow_attainability
  +
  fixes g :: "'v flow"
  assumes g: "flow Δ g"
  and g_finite: "value_flow Δ g  "
  and nontrivial: "V - {source Δ, sink Δ}  {}"
begin

lemma g_outside: "e  E  g e = 0"
by(rule flowD_outside)(rule g)

lemma g_loop [simp]: "g (x, x) = 0"
by(rule g_outside)(simp add: no_loop)

lemma finite_IN_g: "x  sink Δ  d_IN g x  top"
by(rule flowD_finite_IN[OF g])

lemma finite_OUT_g:
  assumes "x  sink Δ"
  shows "d_OUT g x  top"
proof(cases "x = source Δ")
  case True
  with g_finite show ?thesis by simp
next
  case False
  with g have "KIR g x" using assms by(auto dest: flowD_KIR)
  with finite_IN_g[of x] False assms show ?thesis by(simp)
qed

lemma g_source_in [simp]: "g (x, source Δ) = 0"
by(rule g_outside)(simp add: source_in)

lemma finite_g [simp]: "g e  top"
  by(rule flowD_finite[OF g])


definition enum_v :: "nat  'v"
where "enum_v n = from_nat_into (V - {source Δ, sink Δ}) (fst (prod_decode n))"

lemma range_enum_v: "range enum_v  V - {source Δ, sink Δ}"
using from_nat_into[OF nontrivial] by(auto simp add: enum_v_def)

lemma enum_v_repeat:
  assumes x: "x  V" "x  source Δ" "x  sink Δ"
  shows "i'>i. enum_v i' = x"
proof -
  let ?V = "V - {source Δ, sink Δ}"
  let ?n = "to_nat_on ?V x"
  let ?A = "{?n} × (UNIV :: nat set)"
  from x have x': "x  V - {source Δ, sink Δ}" by simp
  have "infinite ?A" by(auto dest: finite_cartesian_productD2)
  hence "infinite (prod_encode ` ?A)" by(auto dest: finite_imageD simp add: inj_prod_encode)
  then obtain i' where "i' > i" "i'  prod_encode ` ?A"
    unfolding infinite_nat_iff_unbounded by blast
  from this(2) have "enum_v i' = x" using x by(clarsimp simp add: enum_v_def)
  with i' > i show ?thesis by blast
qed

fun h_plus :: "nat  'v edge  ennreal"
where
  "h_plus 0 (x, y) = (if x = source Δ then g (x, y) else 0)"
| "h_plus (Suc i) (x, y) =
  (if enum_v (Suc i) = x  d_OUT (h_plus i) x < d_IN (h_plus i) x then
   let total = d_IN (h_plus i) x - d_OUT (h_plus i) x;
       share = g (x, y) - h_plus i (x, y);
       shares = d_OUT g x - d_OUT (h_plus i) x
   in h_plus i (x, y) + share * total / shares
   else h_plus i (x, y))"


lemma h_plus_le_g: "h_plus i e  g e"
proof(induction i arbitrary: e and e)
  case 0 thus ?case by(cases e) simp
next
  case (Suc i)
  { fix x y
    assume enum: "x = enum_v (Suc i)"
    assume less: "d_OUT (h_plus i) x < d_IN (h_plus i) x"
    from enum have x: "x  source Δ" "x  sink Δ" using range_enum_v
      by(auto dest: sym intro: rev_image_eqI)

    define share where "share = g (x, y) - h_plus i (x, y)"
    define shares where "shares = d_OUT g x - d_OUT (h_plus i) x"
    define total where "total = d_IN (h_plus i) x - d_OUT (h_plus i) x"
    let ?h = "h_plus i (x, y) + share * total / shares"

    have "d_OUT (h_plus i) x  d_OUT g x" by(rule d_OUT_mono)(rule Suc.IH)
    also have " < top" using finite_OUT_g[of x] x by (simp add: less_top)
    finally have "d_OUT (h_plus i) x  " by simp
    then have shares_eq: "shares = (+ y. g (x, y) - h_plus i (x, y))" unfolding shares_def d_OUT_def
      by(subst nn_integral_diff)(simp_all add: AE_count_space Suc.IH)

    have *: "share / shares  1"
    proof (cases "share = 0")
      case True thus ?thesis by(simp)
    next
      case False
      hence "share > 0" using h_plus i (x, y)  g _
        by(simp add: share_def dual_order.strict_iff_order)
      moreover have "share  shares" unfolding share_def shares_eq by(rule nn_integral_ge_point)simp
      ultimately show ?thesis by(simp add: divide_le_posI_ennreal)
    qed

    note shares_def
    also have "d_OUT g x = d_IN g x" by(rule flowD_KIR[OF g x])
    also have "d_IN (h_plus i) x  d_IN g x" by(rule d_IN_mono)(rule Suc.IH)
    ultimately have *: "total  shares" unfolding total_def by(simp add: ennreal_minus_mono)
    moreover have "total > 0" unfolding total_def using less by (clarsimp simp add: diff_gr0_ennreal)
    ultimately have "total / shares  1" by(intro divide_le_posI_ennreal)(simp_all)
    hence "share * (total / shares)  share * 1"
      by(rule mult_left_mono) simp
    hence "?h  h_plus i (x, y) + share" by(simp add: ennreal_times_divide add_mono)
    also have " = g (x, y)" unfolding share_def using h_plus i (x, y)  g _ finite_g[of "(x, y)"]
      by simp
    moreover
    note calculation }
  note * = this
  show ?case using Suc.IH * by(cases e) clarsimp
qed

lemma h_plus_outside: "e  E  h_plus i e = 0"
by (metis g_outside h_plus_le_g le_zero_eq)

lemma h_plus_not_infty [simp]: "h_plus i e  top"
using h_plus_le_g[of i e] by (auto simp: top_unique)

lemma h_plus_mono: "h_plus i e  h_plus (Suc i) e"
proof(cases e)
  case [simp]: (Pair x y)
  { assume "d_OUT (h_plus i) x < d_IN (h_plus i) x"
    hence "h_plus i (x, y) + 0  h_plus i (x, y) + (g (x, y) - h_plus i (x, y)) * (d_IN (h_plus i) x - d_OUT (h_plus i) x) / (d_OUT g x - d_OUT (h_plus i) x)"
      by(intro add_left_mono d_OUT_mono le_funI) (simp_all add: h_plus_le_g) }
  then show ?thesis by clarsimp
qed

lemma h_plus_mono': "i  j  h_plus i e  h_plus j e"
by(induction rule: dec_induct)(auto intro: h_plus_mono order_trans)

lemma d_OUT_h_plus_not_infty': "x  sink Δ  d_OUT (h_plus i) x  top"
using d_OUT_mono[of "h_plus i" x g, OF h_plus_le_g] finite_OUT_g[of x] by (auto simp: top_unique)

lemma h_plus_OUT_le_IN:
  assumes "x  source Δ"
  shows "d_OUT (h_plus i) x  d_IN (h_plus i) x"
proof(induction i)
  case 0
  thus ?case using assms by(simp add: d_OUT_def)
next
  case (Suc i)
  have "d_OUT (h_plus (Suc i)) x  d_IN (h_plus i) x"
  proof(cases "enum_v (Suc i) = x  d_OUT (h_plus i) x < d_IN (h_plus i) x")
    case False
    thus ?thesis using Suc.IH by(simp add: d_OUT_def cong: conj_cong)
  next
    case True
    hence x: "x  sink Δ" and le: "d_OUT (h_plus i) x < d_IN (h_plus i) x" using range_enum_v by auto
    let ?r = "λy. (g (x, y) - h_plus i (x, y)) * (d_IN (h_plus i) x - d_OUT (h_plus i) x) / (d_OUT g x - d_OUT (h_plus i) x)"
    have "d_OUT (h_plus (Suc i)) x = d_OUT (h_plus i) x + (+ y. ?r y)"
      using True unfolding d_OUT_def h_plus.simps by(simp add: AE_count_space nn_integral_add)
    also from True have "x  source Δ" "x  sink Δ" using range_enum_v by auto
    from flowD_KIR[OF g this] le d_IN_mono[of "h_plus i" x g, OF h_plus_le_g]
    have le': "d_OUT (h_plus i) x < d_OUT g x" by(simp)
    then have "(+ y. ?r y) =
      (d_IN (h_plus i) x - d_OUT (h_plus i) x) * ((+ y. g (x, y) - h_plus i (x, y)) / (d_OUT g x - d_OUT (h_plus i) x))"
      by(subst mult.commute, subst ennreal_times_divide[symmetric])
        (simp add: nn_integral_cmult nn_integral_divide Suc.IH diff_gr0_ennreal)
    also have "(+ y. g (x, y) - h_plus i (x, y)) = d_OUT g x - d_OUT (h_plus i) x" using x
      by(subst nn_integral_diff)(simp_all add: d_OUT_def[symmetric] h_plus_le_g d_OUT_h_plus_not_infty')
    also have " /  = 1" using le' finite_OUT_g[of x] x
      by(auto intro!: ennreal_divide_self dest: diff_gr0_ennreal simp: less_top[symmetric])
    also have "d_OUT (h_plus i) x + (d_IN (h_plus i) x - d_OUT (h_plus i) x) * 1 = d_IN (h_plus i) x" using x
      by (simp add: Suc)
    finally show ?thesis by simp
  qed
  also have "  d_IN (h_plus (Suc i)) x" by(rule d_IN_mono)(rule h_plus_mono)
  finally show ?case .
qed

lemma h_plus_OUT_eq_IN:
  assumes enum: "enum_v (Suc i) = x"
  shows "d_OUT (h_plus (Suc i)) x = d_IN (h_plus i) x"
proof(cases "d_OUT (h_plus i) x < d_IN (h_plus i) x")
  case False
  from enum have "x  source Δ" using range_enum_v by auto
  from h_plus_OUT_le_IN[OF this, of i] False have "d_OUT (h_plus i) x = d_IN (h_plus i) x" by auto
  with False enum show ?thesis by(simp add: d_OUT_def)
next
  case True
  from enum have x: "x  source Δ" and sink: "x  sink Δ" using range_enum_v by auto
  let ?r = "λy. (g (x, y) - h_plus i (x, y)) * (d_IN (h_plus i) x - d_OUT (h_plus i) x) / (d_OUT g x - d_OUT (h_plus i) x)"
  have "d_OUT (h_plus (Suc i)) x = d_OUT (h_plus i) x + (+ y. ?r y)"
    using True enum unfolding d_OUT_def h_plus.simps by(simp add: AE_count_space nn_integral_add)
  also from True enum have "x  source Δ" "x  sink Δ" using range_enum_v by auto
  from flowD_KIR[OF g this] True d_IN_mono[of "h_plus i" x g, OF h_plus_le_g]
  have le': "d_OUT (h_plus i) x < d_OUT g x" by(simp)
  then have "(+ y. ?r y ) =
    (d_IN (h_plus i) x - d_OUT (h_plus i) x) * ((+ y. g (x, y) - h_plus i (x, y)) / (d_OUT g x - d_OUT (h_plus i) x))"
    by(subst mult.commute, subst ennreal_times_divide[symmetric])
      (simp add: nn_integral_cmult nn_integral_divide h_plus_OUT_le_IN[OF x] diff_gr0_ennreal)
  also have "(+ y. g (x, y) - h_plus i (x, y)) = d_OUT g x - d_OUT (h_plus i) x" using sink
    by(subst nn_integral_diff)(simp_all add: d_OUT_def[symmetric] h_plus_le_g d_OUT_h_plus_not_infty')
  also have " /  = 1" using le' finite_OUT_g[of x] sink
    by(auto intro!: ennreal_divide_self dest: diff_gr0_ennreal simp: less_top[symmetric])
  also have "d_OUT (h_plus i) x + (d_IN (h_plus i) x - d_OUT (h_plus i) x) * 1 = d_IN (h_plus i) x" using sink
    by (simp add: h_plus_OUT_le_IN x)
  finally show ?thesis .
qed

lemma h_plus_source_in [simp]: "h_plus i (x, source Δ) = 0"
by(induction i)simp_all

lemma h_plus_sum_finite: "(+ e. h_plus i e)  top"
proof(induction i)
  case 0
  have "(+ eUNIV. h_plus 0 e) = (+ (x, y). h_plus 0 (x, y))"
    by(simp del: h_plus.simps)
  also have " = (+ (x, y)range (Pair (source Δ)). h_plus 0 (x, y))"
    by(auto simp add: nn_integral_count_space_indicator intro!: nn_integral_cong)
  also have " = value_flow Δ g" by(simp add: d_OUT_def nn_integral_count_space_reindex)
  also have " < " using g_finite by (simp add: less_top)
  finally show ?case by simp
next
  case (Suc i)
  define xi where "xi = enum_v (Suc i)"
  then have xi: "xi  source Δ" "xi  sink Δ" using range_enum_v by auto
  show ?case
  proof(cases "d_OUT (h_plus i) xi < d_IN (h_plus i) xi")
    case False
    hence "(+ eUNIV. h_plus (Suc i) e) = (+ e. h_plus i e)"
      by(auto intro!: nn_integral_cong simp add: xi_def)
    with Suc.IH show ?thesis by simp
  next
    case True
    have less: "d_OUT (h_plus i) xi < d_OUT g xi"
      using True flowD_KIR[OF g xi] d_IN_mono[of "h_plus i" xi, OF h_plus_le_g]
      by simp

    have "(+ e. h_plus (Suc i) e) =
      (+ eUNIV. h_plus i e) + (+ (x, y). ((g (x, y) - h_plus i (x, y)) * (d_IN (h_plus i) x - d_OUT (h_plus i) x) / (d_OUT g x - d_OUT (h_plus i) x)) * indicator (range (Pair xi)) (x, y))"
      (is "_ = ?IH + ?rest" is "_ = _ + + (x, y). ?f x y * _ _") using xi True
      by(subst nn_integral_add[symmetric])(auto simp add: xi_def split_beta AE_count_space intro!: nn_integral_cong split: split_indicator intro!: h_plus_le_g h_plus_OUT_le_IN d_OUT_mono le_funI)
    also have "?rest = (+ (x, y)range (Pair xi). ?f x y)"
      by(simp add: nn_integral_count_space_indicator split_def)
    also have " = (+ y. ?f xi y)" by(simp add: nn_integral_count_space_reindex)
    also have " = (+ y. g (xi, y) - h_plus i (xi, y)) * ((d_IN (h_plus i) xi - d_OUT (h_plus i) xi) / (d_OUT g xi - d_OUT (h_plus i) xi))"
      (is "_ = ?integral * ?factor")  using True less
      by(simp add: nn_integral_multc nn_integral_divide diff_gr0_ennreal ennreal_times_divide)
    also have "?integral = d_OUT g xi - d_OUT (h_plus i) xi" unfolding d_OUT_def using xi
      by(subst nn_integral_diff)(simp_all add: h_plus_le_g d_OUT_def[symmetric] d_OUT_h_plus_not_infty')
    also have " * ?factor = (d_IN (h_plus i) xi - d_OUT (h_plus i) xi)" using xi
      apply (subst ennreal_times_divide)
      apply (subst mult.commute)
      apply (subst ennreal_mult_divide_eq)
      apply (simp_all add: diff_gr0_ennreal finite_OUT_g less zero_less_iff_neq_zero[symmetric])
      done
    also have "  " using h_plus_OUT_eq_IN[OF refl, of i, folded xi_def, symmetric] xi
      by(simp add: d_OUT_h_plus_not_infty')
    ultimately show ?thesis using Suc.IH by simp
  qed
qed

lemma d_OUT_h_plus_not_infty [simp]: "d_OUT (h_plus i) x  top"
proof -
  have "d_OUT (h_plus i) x  (+ yUNIV. + x. h_plus i (x, y))"
    unfolding d_OUT_def by(rule nn_integral_mono nn_integral_ge_point)+ simp
  also have " < " using h_plus_sum_finite by(simp add: nn_integral_snd_count_space less_top)
  finally show ?thesis by simp
qed

definition enum_cycle :: "nat  'v path"
where "enum_cycle = from_nat_into (cycles Δ)"

lemma cycle_enum_cycle [simp]: "cycles Δ  {}  cycle Δ (enum_cycle n)"
unfolding enum_cycle_def using from_nat_into[of "cycles Δ" n] by simp

context
  fixes h' :: "'v flow"
  assumes finite_h': "h' e  top"
begin

fun h_minus_aux :: "nat  'v edge  ennreal"
where
  "h_minus_aux 0 e = 0"
| "h_minus_aux (Suc j) e =
  (if e  set (cycle_edges (enum_cycle j)) then
     h_minus_aux j e + Min {h' e' - h_minus_aux j e'|e'. e'set (cycle_edges (enum_cycle j))}
   else h_minus_aux j e)"

lemma h_minus_aux_le_h': "h_minus_aux j e  h' e"
proof(induction j e rule: h_minus_aux.induct)
  case 0: (1 e) show ?case by simp
next
  case Suc: (2 j e)
  { assume e: "e  set (cycle_edges (enum_cycle j))"
    then have "h_minus_aux j e + Min {h' e' - h_minus_aux j e' |e'. e'  set (cycle_edges (enum_cycle j))} 
      h_minus_aux j e + (h' e - h_minus_aux j e)"
      using [[simproc add: finite_Collect]] by(cases e rule: prod.exhaust)(auto intro!: add_mono Min_le)
    also have " = h' e" using e finite_h'[of e] Suc.IH(2)[of e]
      by(cases e rule: prod.exhaust)
        (auto simp add: add_diff_eq_ennreal top_unique intro!: ennreal_add_diff_cancel_left)
    also note calculation }
  then show ?case using Suc by clarsimp
qed

lemma h_minus_aux_finite [simp]: "h_minus_aux j e  top"
using h_minus_aux_le_h'[of j e] finite_h'[of e] by (auto simp: top_unique)

lemma h_minus_aux_mono: "h_minus_aux j e  h_minus_aux (Suc j) e"
proof(cases "e  set (cycle_edges (enum_cycle j)) = True")
  case True
  have "h_minus_aux j e + 0  h_minus_aux (Suc j) e" unfolding h_minus_aux.simps True if_True
    using True [[simproc add: finite_Collect]]
    by(cases e)(rule add_mono, auto intro!: Min.boundedI simp add: h_minus_aux_le_h')
  thus ?thesis by simp
qed simp

lemma d_OUT_h_minus_aux:
  assumes "cycles Δ  {}"
  shows "d_OUT (h_minus_aux j) x = d_IN (h_minus_aux j) x"
proof(induction j)
  case 0 show ?case by simp
next
  case (Suc j)
  define C where "C = enum_cycle j"
  define δ where "δ = Min {h' e' - h_minus_aux j e' |e'. e'  set (cycle_edges C)}"

  have "d_OUT (h_minus_aux (Suc j)) x =
    (+ y. h_minus_aux j (x, y) + (if (x, y)  set (cycle_edges C) then δ else 0))"
    unfolding d_OUT_def by(simp add: if_distrib C_def δ_def cong del: if_weak_cong)
  also have " = d_OUT (h_minus_aux j) x + (+ y. δ * indicator (set (cycle_edges C)) (x, y))"
    (is "_ = _ + ?add")
    by(subst nn_integral_add)(auto simp add: AE_count_space d_OUT_def intro!: arg_cong2[where f="(+)"] nn_integral_cong)
  also have "?add = (+ erange (Pair x). δ * indicator {(x', y). (x', y)  set (cycle_edges C)  x' = x} e)"
    by(auto simp add: nn_integral_count_space_reindex intro!: nn_integral_cong split: split_indicator)
  also have " = δ * card (set (filter (λ(x', y). x' = x) (cycle_edges C)))"
    using [[simproc add: finite_Collect]]
    apply(subst nn_integral_cmult_indicator; auto)
    apply(subst emeasure_count_space; auto simp add: split_def)
    done
  also have "card (set (filter (λ(x', y). x' = x) (cycle_edges C))) = card (set (filter (λ(x', y). y = x) (cycle_edges C)))"
    unfolding C_def by(rule cycle_enter_leave_same)(rule cycle_enum_cycle[OF assms])
  also have "δ *  =  (+ erange (λx'. (x', x)). δ * indicator {(x', y). (x', y)  set (cycle_edges C)  y = x} e)"
    using [[simproc add: finite_Collect]]
    apply(subst nn_integral_cmult_indicator; auto)
    apply(subst emeasure_count_space; auto simp add: split_def)
    done
  also have " = (+ x'. δ * indicator (set (cycle_edges C)) (x', x))"
    by(auto simp add: nn_integral_count_space_reindex intro!: nn_integral_cong split: split_indicator)
  also have "d_OUT (h_minus_aux j) x +  = (+ x'. h_minus_aux j (x', x) + δ * indicator (set (cycle_edges C)) (x', x))"
    unfolding Suc.IH d_IN_def by(simp add: nn_integral_add[symmetric])
  also have " = d_IN (h_minus_aux (Suc j)) x" unfolding d_IN_def
    by(auto intro!: nn_integral_cong simp add: δ_def C_def split: split_indicator)
  finally show ?case .
qed

lemma h_minus_aux_source:
  assumes "cycles Δ  {}"
  shows "h_minus_aux j (source Δ, y) = 0"
proof(induction j)
  case 0 thus ?case by simp
next
  case (Suc j)
  have "(source Δ, y)  set (cycle_edges (enum_cycle j))"
  proof
    assume *: "(source Δ, y)  set (cycle_edges (enum_cycle j))"
    have cycle: "cycle Δ (enum_cycle j)" using assms by(rule cycle_enum_cycle)
    from cycle_leave_ex_enter[OF this *]
    obtain z where "(z, source Δ)  set (cycle_edges (enum_cycle j))" ..
    with cycle_edges_edges[OF cycle] have "(z, source Δ)  E" ..
    thus False using source_in[of z] by simp
  qed
  then show ?case using Suc.IH by simp
qed

lemma h_minus_aux_cycle:
  fixes j defines "C  enum_cycle j"
  assumes "cycles Δ  {}"
  shows "eset (cycle_edges C). h_minus_aux (Suc j) e = h' e"
proof -
  let ?A = "{h' e' - h_minus_aux j e'|e'. e'  set (cycle_edges C)}"
  from assms have "cycle Δ C" by auto
  from cycle_edges_not_Nil[OF this] have "Min ?A  ?A" using [[simproc add: finite_Collect]]
    by(intro Min_in)(fastforce simp add: neq_Nil_conv)+
  then obtain e' where e: "e'  set (cycle_edges C)"
    and "Min ?A = h' e' - h_minus_aux j e'" by auto
  hence "h_minus_aux (Suc j) e' = h' e'"
    by(simp add: C_def h_minus_aux_le_h')
  with e show ?thesis by blast
qed

end

fun h_minus :: "nat  'v edge  ennreal"
where
  "h_minus 0 e = 0"
| "h_minus (Suc i) e = h_minus i e + (SUP j. h_minus_aux (λe'. h_plus (Suc i) e' - h_minus i e') j e)"

lemma h_minus_le_h_plus: "h_minus i e  h_plus i e"
proof(induction i e rule: h_minus.induct)
  case 0: (1 e) show ?case by simp
next
  case Suc: (2 i e)
  note IH = Suc.IH(2)[OF UNIV_I]
  let ?h' = "λe'. h_plus (Suc i) e' - h_minus i e'"
  have h': "?h' e'  top" for e' using IH(1)[of e'] by simp

  have "(j. h_minus_aux ?h' j e)  ?h' e" by(rule SUP_least)(rule h_minus_aux_le_h'[OF h'])
  hence "h_minus (Suc i) e  h_minus i e + " by(simp add: add_mono)
  also have " = h_plus (Suc i) e" using IH[of e] h_plus_mono[of i e]
    by auto
  finally show ?case .
qed

lemma finite_h': "h_plus (Suc i) e - h_minus i e  top"
  by simp

lemma h_minus_mono: "h_minus i e  h_minus (Suc i) e"
proof -
  have "h_minus i e + 0  h_minus (Suc i) e" unfolding h_minus.simps
    by(rule add_mono; simp add: SUP_upper2)
  thus ?thesis by simp
qed

lemma h_minus_finite [simp]: "h_minus i e  "
proof -
  have "h_minus i e  h_plus i e" by(rule h_minus_le_h_plus)
  also have " < " by (simp add: less_top[symmetric])
  finally show ?thesis by simp
qed

lemma d_OUT_h_minus:
  assumes cycles: "cycles Δ  {}"
  shows "d_OUT (h_minus i) x = d_IN (h_minus i) x"
proof(induction i)
  case (Suc i)
  let ?h' = "λe. h_plus (Suc i) e - h_minus i e"
  have "d_OUT (λe. h_minus (Suc i) e) x = d_OUT (h_minus i) x + d_OUT (λe. SUP j. h_minus_aux ?h' j e) x"
    by(simp add: d_OUT_add SUP_upper2)
  also have "d_OUT (λe. SUP j. h_minus_aux ?h' j e) x = (SUP j. d_OUT (h_minus_aux ?h' j) x)"
    by(rule d_OUT_monotone_convergence_SUP incseq_SucI le_funI h_minus_aux_mono finite_h')+
  also have " = (SUP j. d_IN (h_minus_aux ?h' j) x)"
    by(rule SUP_cong[OF refl])(rule d_OUT_h_minus_aux[OF finite_h' cycles])
  also have " = d_IN (λe. SUP j. h_minus_aux ?h' j e) x"
    by(rule d_IN_monotone_convergence_SUP[symmetric] incseq_SucI le_funI h_minus_aux_mono finite_h')+
  also have "d_OUT (h_minus i) x +  = d_IN (λe. h_minus (Suc i) e) x" using Suc.IH
    by(simp add: d_IN_add SUP_upper2)
  finally show ?case .
qed simp

lemma h_minus_source:
  assumes "cycles Δ  {}"
  shows "h_minus n (source Δ, y) = 0"
by(induction n)(simp_all add: h_minus_aux_source[OF finite_h' assms])

lemma h_minus_source_in [simp]: "h_minus i (x, source Δ) = 0"
using h_minus_le_h_plus[of i "(x, source Δ)"] by simp

lemma h_minus_OUT_finite [simp]: "d_OUT (h_minus i) x  top"
proof -
  have "d_OUT (h_minus i) x  d_OUT (h_plus i) x" by(rule d_OUT_mono)(rule h_minus_le_h_plus)
  also have " < " by (simp add: less_top[symmetric])
  finally show ?thesis by simp
qed

lemma h_minus_cycle:
  assumes "cycle Δ C"
  shows "eset (cycle_edges C). h_minus i e = h_plus i e"
proof(cases i)
  case (Suc i)
  let ?h' = "λe. h_plus (Suc i) e - h_minus i e"
  from assms have cycles: "cycles Δ  {}" by auto
  with assms from_nat_into_surj[of "cycles Δ" C] obtain j where j: "C = enum_cycle j"
    by(auto simp add: enum_cycle_def)
  from h_minus_aux_cycle[of "?h'" j, OF finite_h' cycles] j
  obtain e where e: "e  set (cycle_edges C)" and "h_minus_aux ?h' (Suc j) e = ?h' e" by(auto)
  then have "h_plus (Suc i) e = h_minus i e + h_minus_aux ?h' (Suc j) e"
    using order_trans[OF h_minus_le_h_plus h_plus_mono]
    by (subst eq_commute) simp
  also have "  h_minus (Suc i) e" unfolding h_minus.simps
    by(intro add_mono SUP_upper; simp)
  finally show ?thesis using e h_minus_le_h_plus[of "Suc i" e] Suc by auto
next
  case 0
  from cycle_edges_not_Nil[OF assms] obtain x y where e: "(x, y)  set (cycle_edges C)"
    by(fastforce simp add: neq_Nil_conv)
  then have "x  source Δ" using assms by(auto dest: source_out_not_cycle)
  hence "h_plus 0 (x, y) = 0" by simp
  with e 0 show ?thesis by(auto simp del: h_plus.simps)
qed

abbreviation lim_h_plus :: "'v edge  ennreal"
where "lim_h_plus e  SUP n. h_plus n e"

abbreviation lim_h_minus :: "'v edge  ennreal"
where "lim_h_minus e  SUP n. h_minus n e"

lemma lim_h_plus_le_g: "lim_h_plus e  g e"
by(rule SUP_least)(rule h_plus_le_g)

lemma lim_h_plus_finite [simp]: "lim_h_plus e  top"
proof -
  have "lim_h_plus e  g e" by(rule lim_h_plus_le_g)
  also have " < top" by (simp add: less_top[symmetric])
  finally show ?thesis unfolding less_top .
qed

lemma lim_h_minus_le_lim_h_plus: "lim_h_minus e  lim_h_plus e"
by(rule SUP_mono)(blast intro: h_minus_le_h_plus)

lemma lim_h_minus_finite [simp]: "lim_h_minus e  top"
proof -
  have "lim_h_minus e  lim_h_plus e" by(rule lim_h_minus_le_lim_h_plus)
  also have " < top" unfolding less_top[symmetric] by (rule lim_h_plus_finite)
  finally show ?thesis unfolding less_top[symmetric] by simp
qed

lemma lim_h_minus_IN_finite [simp]:
  assumes "x  sink Δ"
  shows "d_IN lim_h_minus x  top"
proof -
  have "d_IN lim_h_minus x  d_IN lim_h_plus x"
    by(intro d_IN_mono le_funI lim_h_minus_le_lim_h_plus)
  also have "  d_IN g x" by(intro d_IN_mono le_funI lim_h_plus_le_g)
  also have " < " using assms by(simp add: finite_IN_g less_top[symmetric])
  finally show ?thesis by simp
qed

lemma lim_h_plus_OUT_IN:
  assumes "x  source Δ" "x  sink Δ"
  shows "d_OUT lim_h_plus x = d_IN lim_h_plus x"
proof(cases "x  V")
  case True
  have "d_OUT lim_h_plus x = (SUP n. d_OUT (h_plus n) x)"
    by(rule d_OUT_monotone_convergence_SUP incseq_SucI le_funI h_plus_mono)+
  also have " = (SUP n. d_IN (h_plus n) x)" (is "?lhs = ?rhs")
  proof(rule antisym)
    show "?lhs  ?rhs" by(rule SUP_mono)(auto intro: h_plus_OUT_le_IN[OF assms(1)])
    show "?rhs  ?lhs"
    proof(rule SUP_mono)
      fix i
      from enum_v_repeat[OF True assms, of i]
      obtain i' where "i' > i" "enum_v i' = x" by auto
      moreover then obtain i'' where i': "i' = Suc i''" by(cases i') auto
      ultimately have "d_OUT (h_plus i') x = d_IN (h_plus i'') x" using  x  source Δ
        by(simp add: h_plus_OUT_eq_IN)
      moreover have "i  i''" using i < i' i' by simp
      then have "d_IN (h_plus i) x  d_IN (h_plus i'') x" by(intro d_IN_mono h_plus_mono')
      ultimately have "d_IN (h_plus i) x  d_OUT (h_plus i') x" by simp
      thus "i'UNIV. d_IN (h_plus i) x  d_OUT (h_plus i') x" by blast
    qed
  qed
  also have " = d_IN lim_h_plus x"
    by(rule d_IN_monotone_convergence_SUP[symmetric] incseq_SucI le_funI h_plus_mono)+
  finally show ?thesis .
next
  case False
  have "(x, y)  support_flow lim_h_plus" for y using False h_plus_outside[of "(x, y)"]
    by(fastforce elim!: support_flow.cases simp add: less_SUP_iff vertex_def)
  moreover have "(y, x)  support_flow lim_h_plus" for y using False h_plus_outside[of "(y, x)"]
    by(fastforce elim!: support_flow.cases simp add: less_SUP_iff vertex_def)
  ultimately show ?thesis
    by(auto simp add: d_OUT_alt_def2 d_IN_alt_def2 AE_count_space intro!: nn_integral_cong_AE)
qed

lemma lim_h_minus_OUT_IN:
  assumes cycles: "cycles Δ  {}"
  shows "d_OUT lim_h_minus x = d_IN lim_h_minus x"
proof -
  have "d_OUT lim_h_minus x = (SUP n. d_OUT (h_minus n) x)"
    by(rule d_OUT_monotone_convergence_SUP incseq_SucI le_funI h_minus_mono)+
  also have " = (SUP n. d_IN (h_minus n) x)" using cycles by(simp add: d_OUT_h_minus)
  also have " = d_IN lim_h_minus x"
    by(rule d_IN_monotone_convergence_SUP[symmetric] incseq_SucI le_funI h_minus_mono)+
  finally show ?thesis .
qed

definition h :: "'v edge  ennreal"
where "h e = lim_h_plus e - (if cycles Δ  {} then lim_h_minus e else 0)"

lemma h_le_lim_h_plus: "h e  lim_h_plus e"
by (simp add: h_def)

lemma h_le_g: "h e  g e"
using h_le_lim_h_plus[of e] lim_h_plus_le_g[of e] by simp

lemma flow_h: "flow Δ h"
proof
  fix e
  have "h e  lim_h_plus e" by(rule h_le_lim_h_plus)
  also have "  g e" by(rule lim_h_plus_le_g)
  also have "  capacity Δ e" using g by(rule flowD_capacity)
  finally show "h e  " .
next
  fix x
  assume "x  source Δ" "x  sink Δ"
  then show "KIR h x"
    by (cases "cycles Δ = {}")
       (auto simp add: h_def[abs_def] lim_h_plus_OUT_IN d_OUT_diff d_IN_diff lim_h_minus_le_lim_h_plus lim_h_minus_OUT_IN)
qed

lemma value_h_plus: "value_flow Δ (h_plus i) = value_flow Δ g" (is "?lhs = ?rhs")
proof(rule antisym)
  show "?lhs  ?rhs" by(rule d_OUT_mono)(rule h_plus_le_g)

  have "?rhs  value_flow Δ (h_plus 0)"
    by(auto simp add: d_OUT_def cong: if_cong intro!: nn_integral_mono)
  also have "  value_flow Δ (h_plus i)"
    by(rule d_OUT_mono)(rule h_plus_mono'; simp)
  finally show "?rhs  ?lhs" .
qed

lemma value_h: "value_flow Δ h = value_flow Δ g" (is "?lhs = ?rhs")
proof(rule antisym)
  have "?lhs  value_flow Δ lim_h_plus" using ennreal_minus_mono
    by(fastforce simp add: h_def intro!: d_OUT_mono)
  also have "  ?rhs" by(rule d_OUT_mono)(rule lim_h_plus_le_g)
  finally show "?lhs  ?rhs" .

  show "?rhs  ?lhs"
    by(auto simp add: d_OUT_def h_def h_minus_source cong: if_cong intro!: nn_integral_mono SUP_upper2[where i=0])
qed


definition h_diff :: "nat  'v edge  ennreal"
where "h_diff i e = h_plus i e - (if cycles Δ  {} then h_minus i e else 0)"

lemma d_IN_h_source [simp]: "d_IN (h_diff i) (source Δ) = 0"
by(simp add: d_IN_def h_diff_def cong del: if_weak_cong)

lemma h_diff_le_h_plus: "h_diff i e  h_plus i e"
by(simp add: h_diff_def)

lemma h_diff_le_g: "h_diff i e  g e"
using h_diff_le_h_plus[of i e] h_plus_le_g[of i e] by simp

lemma h_diff_loop [simp]: "h_diff i (x, x) = 0"
using h_diff_le_g[of i "(x, x)"] by simp

lemma supp_h_diff_edges: "support_flow (h_diff i)  E"
proof
  fix e
  assume "e  support_flow (h_diff i)"
  then have "0 < h_diff i e" by(auto elim: support_flow.cases)
  also have "h_diff i e  h_plus i e" by(rule h_diff_le_h_plus)
  finally show "e  E" using h_plus_outside[of e i] by(cases "e  E") auto
qed

lemma h_diff_OUT_le_IN:
  assumes "x  source Δ"
  shows "d_OUT (h_diff i) x  d_IN (h_diff i) x"
proof(cases "cycles Δ  {}")
  case False
  thus ?thesis using assms by(simp add: h_diff_def[abs_def] h_plus_OUT_le_IN)
next
  case cycles: True
  then have "d_OUT (h_diff i) x = d_OUT (h_plus i) x - d_OUT (h_minus i) x"
    unfolding h_diff_def[abs_def] using assms
    by (simp add: h_minus_le_h_plus d_OUT_diff)
  also have "  d_IN (h_plus i) x - d_IN (h_minus i) x" using cycles assms
    by(intro ennreal_minus_mono h_plus_OUT_le_IN)(simp_all add: d_OUT_h_minus)
  also have " = d_IN (h_diff i) x" using cycles
    unfolding h_diff_def[abs_def] by(subst d_IN_diff)(simp_all add: h_minus_le_h_plus d_OUT_h_minus[symmetric])
  finally show ?thesis .
qed

lemma h_diff_cycle:
  assumes "cycle Δ p"
  shows "eset (cycle_edges p). h_diff i e = 0"
proof -
  from h_minus_cycle[OF assms, of i] obtain e
    where e: "e  set (cycle_edges p)" and "h_minus i e = h_plus i e" by auto
  hence "h_diff i e = 0" using assms by(auto simp add: h_diff_def)
  with e show ?thesis by blast
qed

lemma d_IN_h_le_value': "d_IN (h_diff i) x  value_flow Δ (h_plus i)"
proof -
  let ?supp = "support_flow (h_diff i)"
  define X where "X = {y. (y, x)  ?supp^*} - {x}"

  { fix x y
    assume x: "x  X" and y: "y  X"
    { assume yx: "(y, x)  ?supp*" and neq: "y  x" and xy: "(x, y)  ?supp"
      from yx obtain p' where "rtrancl_path (λx y. (x, y)  ?supp) y p' x"
        unfolding rtrancl_def rtranclp_eq_rtrancl_path by auto
      then obtain p where p: "rtrancl_path (λx y. (x, y)  ?supp) y p x"
        and distinct: "distinct (y # p)" by(rule rtrancl_path_distinct)
      with neq have "p  []" by(auto elim: rtrancl_path.cases)

      from xy have "(x, y)  E" using supp_h_diff_edges[of i] by(auto)
      moreover from p have "path Δ y p x"
        by(rule rtrancl_path_mono)(auto dest: supp_h_diff_edges[THEN subsetD])
      ultimately have "path Δ x (y # p) x" by(auto intro: rtrancl_path.intros)
      hence cycle: "cycle Δ (y # p)" using _ distinct by(rule cycle) simp
      from h_diff_cycle[OF this, of i] obtain e
        where e: "e  set (cycle_edges (y # p))" and 0: "h_diff i e = 0" by blast
      from e obtain n where e': "e = ((y # p) ! n, (p @ [y]) ! n)" and n: "n < Suc (length p)"
        by(auto simp add: cycle_edges_def set_zip)
      have "e  ?supp"
      proof(cases "n = length p")
        case True
        with rtrancl_path_last[OF p] p  [] have "(y # p) ! n = x"
          by(cases p)(simp_all add: last_conv_nth del: last.simps)
        with e' True have "e = (x, y)" by simp
        with xy show ?thesis by simp
      next
        case False
        with n have "n < length p" by simp
        with rtrancl_path_nth[OF p this] e' show ?thesis by(simp add: nth_append)
      qed
      with 0 have False by(simp add: support_flow.simps) }
    hence "(x, y)  ?supp" using x y
      by(auto simp add: X_def intro: converse_rtrancl_into_rtrancl)
    then have "h_diff i (x, y) = 0"
      by(simp add: support_flow.simps) }
  note acyclic = this

  { fix y
    assume "y  X"
    hence "(y, x)  ?supp" by(auto simp add: X_def support_flow.simps intro: not_in_support_flowD)
    hence "h_diff i (y, x) = 0"  by(simp add: support_flow.simps) }
  note in_X = this

  let ?diff = "λx. (+ y. h_diff i (x, y) * indicator X x * indicator X y)"
  have finite2: "(+ x. ?diff x)  top" (is "?lhs  _")
  proof -
    have "?lhs  (+ xUNIV. + y. h_plus i (x, y))"
      by(intro nn_integral_mono)(auto simp add: h_diff_def split: split_indicator)
    also have " = (+ e. h_plus i e)" by(rule nn_integral_fst_count_space)
    also have " < " by(simp add: h_plus_sum_finite less_top[symmetric])
    finally show ?thesis by simp
  qed
  have finite1: "?diff x  top" for x
    using finite2 by(rule neq_top_trans)(rule nn_integral_ge_point, simp)
  have finite3: "(+ x. d_OUT (h_diff i) x * indicator (X - {source Δ}) x)  " (is "?lhs  _")
  proof -
    have "?lhs  (+ xUNIV. + y. h_plus i (x, y))" unfolding d_OUT_def
      apply(simp add: nn_integral_multc[symmetric])
      apply(intro nn_integral_mono)
      apply(auto simp add: h_diff_def split: split_indicator)
      done
    also have " = (+ e. h_plus i e)" by(rule nn_integral_fst_count_space)
    also have " < " by(simp add: h_plus_sum_finite less_top[symmetric])
    finally show ?thesis by simp
  qed

  have "d_IN (h_diff i) x = (+ y. h_diff i (y, x) * indicator X y)" unfolding d_IN_def
    by(rule nn_integral_cong)(simp add: in_X split: split_indicator)
  also have "  (+ x- X. + y. h_diff i (y, x) * indicator X y)"
    by(rule nn_integral_ge_point)(simp add: X_def)
  also have " = (+ xUNIV. + y. h_diff i (y, x) * indicator X y * indicator (- X) x)"
    by(simp add: nn_integral_multc nn_integral_count_space_indicator)
  also have " = (+ xUNIV. + y. h_diff i (x, y) * indicator X x * indicator (- X) y)"
    by(subst nn_integral_snd_count_space[where f="case_prod _", simplified])(simp add: nn_integral_fst_count_space[where f="case_prod _", simplified])
  also have " = (+ xUNIV. (+ y. h_diff i (x, y) * indicator X x * indicator (- X) y) + (?diff x - ?diff x))"
    by(simp add: finite1)
  also have " = (+ xUNIV. (+ y. h_diff i (x, y) * indicator X x * indicator (- X) y + h_diff i (x, y) * indicator X x * indicator X y) - ?diff x)"
    apply (subst add_diff_eq_ennreal)
    apply simp
    by(subst nn_integral_add[symmetric])(simp_all add:)
  also have " = (+ xUNIV. (+ y. h_diff i (x, y) * indicator X x) - ?diff x)"
    by(auto intro!: nn_integral_cong arg_cong2[where f="(-)"] split: split_indicator)
  also have " = (+ xUNIV. + yUNIV. h_diff i (x, y) * indicator X x) - (+ x. ?diff x)"
    by(subst nn_integral_diff)(auto simp add: AE_count_space finite2 intro!: nn_integral_mono split: split_indicator)
  also have "(+ xUNIV. + yUNIV. h_diff i (x, y) * indicator X x) = (+ x. d_OUT (h_diff i) x * indicator X x)"
    unfolding d_OUT_def by(simp add: nn_integral_multc)
  also have " = (+ x. d_OUT (h_diff i) x * indicator (X - {source Δ}) x + value_flow Δ (h_diff i) * indicator X (source Δ) * indicator {source Δ} x)"
    by(rule nn_integral_cong)(simp split: split_indicator)
  also have " = (+ x. d_OUT (h_diff i) x * indicator (X - {source Δ}) x) + value_flow Δ (h_diff i) * indicator X (source Δ)"
    (is "_ = ?out" is "_ = _ + ?value")
    by(subst nn_integral_add) simp_all
  also have "(+ xUNIV. + y. h_diff i (x, y) * indicator X x * indicator X y) =
             (+ xUNIV. + y. h_diff i (x, y) * indicator X y)"
    using acyclic by(intro nn_integral_cong)(simp split: split_indicator)
  also have " = (+ yUNIV. + x. h_diff i (x, y) * indicator X y)"
    by(subst nn_integral_snd_count_space[where f="case_prod _", simplified])(simp add: nn_integral_fst_count_space[where f="case_prod _", simplified])
  also have " = (+ y. d_IN (h_diff i) y * indicator X y)" unfolding d_IN_def
    by(simp add: nn_integral_multc)
  also have " = (+ y. d_IN (h_diff i) y * indicator (X - {source Δ}) y)"
    by(rule nn_integral_cong)(simp split: split_indicator)
  also have "?out -   (+ x. d_OUT (h_diff i) x * indicator (X - {source Δ}) x) -  + ?value"
    by (auto simp add: add_ac intro!: add_diff_le_ennreal)
  also have "  0 + ?value" using h_diff_OUT_le_IN finite3
    by(intro nn_integral_mono add_right_mono)(auto split: split_indicator intro!: diff_eq_0_ennreal nn_integral_mono simp add: less_top)
  also have "  value_flow Δ (h_diff i)" by(simp split: split_indicator)
  also have "  value_flow Δ (h_plus i)" by(rule d_OUT_mono le_funI h_diff_le_h_plus)+
  finally show ?thesis .
qed

lemma d_IN_h_le_value: "d_IN h x  value_flow Δ h" (is "?lhs  ?rhs")
proof -
  have [tendsto_intros]: "(λi. h_plus i e)  lim_h_plus e" for e
    by(rule LIMSEQ_SUP incseq_SucI h_plus_mono)+
  have [tendsto_intros]: "(λi. h_minus i e)  lim_h_minus e" for e
    by(rule LIMSEQ_SUP incseq_SucI h_minus_mono)+
  have "(λi. h_diff i e)  lim_h_plus e - (if cycles Δ  {} then lim_h_minus e else 0)" for e
    by(auto intro!: tendsto_intros tendsto_diff_ennreal simp add: h_diff_def simp del: Sup_eq_top_iff SUP_eq_top_iff)
  then have "d_IN h x = (+ y. liminf (λi. h_diff i (y, x)))"
    by(simp add: d_IN_def h_def tendsto_iff_Liminf_eq_Limsup)
  also have "  liminf (λi. d_IN (h_diff i) x)" unfolding d_IN_def
    by(rule nn_integral_liminf) simp_all
  also have "  liminf (λi. value_flow Δ h)" using d_IN_h_le_value'[of _ x]
    by(intro Liminf_mono eventually_sequentiallyI)(auto simp add: value_h_plus value_h)
  also have " = value_flow Δ h" by(simp add: Liminf_const)
  finally show ?thesis .
qed

lemma flow_cleanup: ― ‹Lemma 5.4›
  "h  g. flow Δ h  value_flow Δ h = value_flow Δ g  (x. d_IN h x  value_flow Δ h)"
by(intro exI[where x=h] conjI strip le_funI d_IN_h_le_value flow_h value_h h_le_g)

end

subsection ‹Residual network›

context countable_network begin

definition residual_network :: "'v flow  ('v, 'more) network_scheme"
where "residual_network f =
  edge = λx y. edge Δ x y  edge Δ y x  y  source Δ,
   capacity = λ(x, y). if edge Δ x y then capacity Δ (x, y) - f (x, y) else if y = source Δ then 0 else f (y, x),
   source = source Δ, sink = sink Δ,  = network.more Δ "

lemma residual_network_sel [simp]:
  "edge (residual_network f) x y  edge Δ x y  edge Δ y x  y  source Δ"
  "capacity (residual_network f) (x, y) = (if edge Δ x y then capacity Δ (x, y) - f (x, y) else if y = source Δ then 0 else f (y, x))"
  "source (residual_network f) = source Δ"
  "sink (residual_network f) = sink Δ"
  "network.more (residual_network f) = network.more Δ"
by(simp_all add: residual_network_def)

lemma "E_residual_network": "Eresidual_network f= E  {(x, y). (y, x)  E  y  source Δ}"
by auto

lemma vertices_residual_network [simp]: "vertex (residual_network f) = vertex Δ"
by(auto simp add: vertex_def fun_eq_iff)

inductive wf_residual_network :: "bool"
where " x y. (x, y)  E  (y, x)  E; (source Δ, sink Δ)  E   wf_residual_network"

lemma wf_residual_networkD:
  " wf_residual_network; edge Δ x y   ¬ edge Δ y x"
  " wf_residual_network; e  E   prod.swap e  E"
  " wf_residual_network; edge Δ (source Δ) (sink Δ)   False"
by(auto simp add: wf_residual_network.simps)

lemma residual_countable_network:
  assumes wf: "wf_residual_network"
  and f: "flow Δ f"
  shows "countable_network (residual_network f)" (is "countable_network ")
proof
  have "countable (converse E)" by simp
  then have "countable {(x, y). (y, x)  E  y  source Δ}"
    by(rule countable_subset[rotated]) auto
  then show "countable E⇙" unfolding "E_residual_network" by simp

  show "source   sink " by simp
  show "capacity  e = 0" if "e  E⇙" for e using that by(cases e)(auto intro: flowD_outside[OF f])
  show "capacity  e  top" for e
    using flowD_finite[OF f] by(cases e) auto
qed

end

context antiparallel_edges begin

interpretation Δ'': countable_network Δ'' by(rule Δ''_countable_network)

lemma Δ''_flow_attainability:
  assumes "flow_attainability_axioms Δ"
  shows "flow_attainability Δ''"
proof -
  interpret flow_attainability Δ using _ assms by(rule flow_attainability.intro) unfold_locales
  show ?thesis
  proof
    show "d_IN (capacity Δ'') v    d_OUT (capacity Δ'') v  " if "v  sink Δ''" for v
      using that finite_capacity by(cases v)(simp_all add: max_def)
    show "¬ edge Δ'' v v" for v by(auto elim: edg.cases)
    show "¬ edge Δ'' v (source Δ'')" for v by(simp add: source_in)
  qed
qed

lemma Δ''_wf_residual_network:
  assumes no_loop: "x. ¬ edge Δ x x"
  shows "Δ''.wf_residual_network"
by(auto simp add: Δ''.wf_residual_network.simps assms elim!: edg.cases)

end

subsection ‹The attainability theorem›

context flow_attainability begin

lemma residual_flow_attainability:
  assumes wf: "wf_residual_network"
  and f: "flow Δ f"
  shows "flow_attainability (residual_network f)" (is "flow_attainability ")
proof -
  interpret res: countable_network "residual_network f" by(rule residual_countable_network[OF assms])
  show ?thesis
  proof
    fix x
    assume sink: "x  sink "
    then consider (source) "x = source Δ" | (IN) "d_IN (capacity Δ) x  " | (OUT) "x  source Δ" "d_OUT (capacity Δ) x  "
      using finite_capacity[of x] by auto
    then show "d_IN (capacity ) x    d_OUT (capacity ) x  "
    proof(cases)
      case source
      hence "d_IN (capacity ) x = 0" by(simp add: d_IN_def source_in)
      thus ?thesis by simp
    next
      case IN
      have "d_IN (capacity ) x =
        (+ y. (capacity Δ (y, x) - f (y, x)) * indicator E (y, x) +
              (if x = source Δ then 0 else f (x, y) * indicator E (x, y)))"
        using flowD_outside[OF f] unfolding d_IN_def
        by(auto intro!: nn_integral_cong split: split_indicator dest: wf_residual_networkD[OF wf])
      also have " = (+ y. (capacity Δ (y, x) - f (y, x)) * indicator E (y, x)) +
        (+ y. (if x = source Δ then 0 else f (x, y) * indicator E (x, y)))"
        (is "_ = ?in + ?out")
        by(subst nn_integral_add)(auto simp add: AE_count_space split: split_indicator intro!: flowD_capacity[OF f])
      also have "  d_IN (capacity Δ) x + (if x = source Δ then 0 else d_OUT f x)" (is "_  ?in + ?rest")
        unfolding d_IN_def d_OUT_def
        by(rule add_mono)(auto intro!: nn_integral_mono split: split_indicator simp add: nn_integral_0_iff_AE AE_count_space intro!: diff_le_self_ennreal)
      also consider (source) "x = source Δ" | (inner) "x  source Δ" "x  sink Δ" using sink by auto
      then have "?rest < "
      proof cases
        case inner
        show ?thesis using inner flowD_finite_OUT[OF f inner] by (simp add: less_top)
      qed simp
      ultimately show ?thesis using IN sink by (auto simp: less_top[symmetric] top_unique)
    next
      case OUT
      have "d_OUT (capacity ) x =
        (+ y. (capacity Δ (x, y) - f (x, y)) * indicator E (x, y) +
              (if y = source Δ then 0 else f (y, x) * indicator E (y, x)))"
        using flowD_outside[OF f] unfolding d_OUT_def
        by(auto intro!: nn_integral_cong split: split_indicator dest: wf_residual_networkD[OF wf] simp add: source_in)
      also have " = (+ y. (capacity Δ (x, y) - f (x, y)) * indicator E (x, y)) +
        (+ y. (if y = source Δ then 0 else f (y, x) * indicator E (y, x)))"
        (is "_ = ?in + ?out")
        by(subst nn_integral_add)(auto simp add: AE_count_space split: split_indicator intro!: flowD_capacity[OF f])
      also have "  d_OUT (capacity Δ) x + d_IN f x" (is "_  ?out + ?rest")
        unfolding d_IN_def d_OUT_def
        by(rule add_mono)(auto intro!: nn_integral_mono split: split_indicator simp add: nn_integral_0_iff_AE AE_count_space intro!: diff_le_self_ennreal)
      also have "?rest = d_OUT f x" using flowD_KIR[OF f OUT(1)] sink by simp
      also have "?out +   ?out + ?out" by(intro add_left_mono d_OUT_mono flowD_capacity[OF f])
      finally show ?thesis using OUT by (auto simp: top_unique)
    qed
  next
    show "¬ edge  x x" for x by(simp add: no_loop)
    show "¬ edge  x (source )" for x by(simp add: source_in)
  qed
qed

end

definition plus_flow :: "('v, 'more) graph_scheme  'v flow  'v flow  'v flow" (infixr "ı" 65)
where "plus_flow G f g = (λ(x, y). if edge G x y then f (x, y) + g (x, y) - g (y, x) else 0)"

lemma plus_flow_simps [simp]: fixes G (structure) shows
  "(f  g) (x, y) = (if edge G x y then f (x, y) + g (x, y) - g (y, x) else 0)"
by(simp add: plus_flow_def)

lemma plus_flow_outside: fixes G (structure) shows "e  E  (f  g) e = 0"
by(cases e) simp

lemma
  fixes Δ (structure)
  assumes f_outside: "e. e  E  f e = 0"
  and g_le_f: "x y. edge Δ x y  g (y, x)  f (x, y)"
  shows OUT_plus_flow: "d_IN g x  top  d_OUT (f  g) x = d_OUT f x + (+ yUNIV. g (x, y) * indicator E (x, y)) - (+ y. g (y, x) * indicator E (x, y))"
    (is "_  ?OUT" is "_  _ = _ + ?g_out - ?g_out'")
  and IN_plus_flow: "d_OUT g x  top  d_IN (f  g) x = d_IN f x + (+ yUNIV. g (y, x) * indicator E (y, x)) - (+ y. g (x, y) * indicator E (y, x))"
    (is "_  ?IN" is "_  _ = _ + ?g_in - ?g_in'")
proof -
  assume "d_IN g x  top"
  then have finite1: "(+ y. g (y, x) * indicator A (f y))  top" for A f
    by(rule neq_top_trans)(auto split: split_indicator simp add: d_IN_def intro!: nn_integral_mono)

  have "d_OUT (f  g) x = (+ y. (g (x, y) + (f (x, y) - g (y, x))) * indicator E (x, y))"
    unfolding d_OUT_def by(rule nn_integral_cong)(simp split: split_indicator add: add_diff_eq_ennreal add.commute ennreal_diff_add_assoc g_le_f)
  also have " = ?g_out + (+ y. (f (x, y) - g (y, x)) * indicator E (x, y))"
    (is "_ = _ + ?rest")
    by(subst nn_integral_add[symmetric])(auto simp add: AE_count_space g_le_f split: split_indicator intro!: nn_integral_cong)
  also have "?rest = (+ y. f (x, y) * indicator E (x, y)) - ?g_out'" (is "_ = ?f - _")
    apply(subst nn_integral_diff[symmetric])
    apply(auto intro!: nn_integral_cong split: split_indicator simp add: AE_count_space g_le_f finite1)
    done
  also have "?f = d_OUT f x" unfolding d_OUT_def using f_outside
    by(auto intro!: nn_integral_cong split: split_indicator)
  also have "(+ y. g (x, y) * indicator E (x, y)) + (d_OUT f x - (+ y. g (y, x) * indicator E (x, y))) =
     d_OUT f x + ?g_out - ?g_out'"
     by (subst ennreal_diff_add_assoc[symmetric])
        (auto simp: ac_simps d_OUT_def intro!: nn_integral_mono g_le_f split: split_indicator)
  finally show ?OUT .
next
  assume "d_OUT g x  top"
  then have finite2: "(+ y. g (x, y) * indicator A (f y))  top" for A f
    by(rule neq_top_trans)(auto split: split_indicator simp add: d_OUT_def intro!: nn_integral_mono)

  have "d_IN (f  g) x = (+ y. (g (y, x) + (f (y, x) - g (x, y))) * indicator E (y, x))"
    unfolding d_IN_def by(rule nn_integral_cong)(simp split: split_indicator add: add_diff_eq_ennreal add.commute ennreal_diff_add_assoc g_le_f)
  also have " = (+ yUNIV. g (y, x) * indicator E (y, x)) + (+ y. (f (y, x) - g (x, y)) * indicator E (y, x))"
    (is "_ = _ + ?rest")
    by(subst nn_integral_add[symmetric])(auto simp add: AE_count_space g_le_f split: split_indicator intro!: nn_integral_cong)
  also have "?rest = (+ y. f (y, x) * indicator E (y, x))- ?g_in'"
    by(subst nn_integral_diff[symmetric])(auto intro!: nn_integral_cong split: split_indicator simp add: add_ac add_diff_eq_ennreal AE_count_space g_le_f finite2)
  also have "(+ y. f (y, x) * indicator E (y, x)) = d_IN f x"
    unfolding d_IN_def using f_outside by(auto intro!: nn_integral_cong split: split_indicator)
  also have "(+ y. g (y, x) * indicator E (y, x)) + (d_IN f x - (+ y. g (x, y) * indicator E (y, x))) =
     d_IN f x + ?g_in - ?g_in'"
     by (subst ennreal_diff_add_assoc[symmetric])
        (auto simp: ac_simps d_IN_def intro!: nn_integral_mono g_le_f split: split_indicator)
  finally show ?IN .
qed

context countable_network begin

lemma d_IN_plus_flow:
  assumes wf: "wf_residual_network"
  and f: "flow Δ f"
  and g: "flow (residual_network f) g"
  shows "d_IN (f  g) x  d_IN f x + d_IN g x"
proof -
  have "d_IN (f  g) x  (+ y. f (y, x) + g (y, x))" unfolding d_IN_def
    by(rule nn_integral_mono)(auto intro: diff_le_self_ennreal)
  also have " = d_IN f x + d_IN g x"
    by(subst nn_integral_add)(simp_all add: d_IN_def)
  finally show ?thesis .
qed

lemma scale_flow:
  assumes f: "flow Δ f"
  and c: "c  1"
  shows "flow Δ (λe. c * f e)"
proof(intro flow.intros)
  fix e
  from c have "c * f e  1 * f e" by(rule mult_right_mono) simp
  also have "  capacity Δ e" using flowD_capacity[OF f, of e] by simp
  finally show "c * f e  " .
next
  fix x
  assume x: "x  source Δ" "x  sink Δ"
  have "d_OUT (λe. c * f e) x = c * d_OUT f x" by(simp add: d_OUT_cmult)
  also have "d_OUT f x = d_IN f x" using f x by(rule flowD_KIR)
  also have "c *  = d_IN (λe. c * f e) x" by(simp add: d_IN_cmult)
  finally show "KIR (λe. c * f e) x" .
qed

lemma value_scale_flow:
  "value_flow Δ (λe. c * f e) = c * value_flow Δ f"
by(rule d_OUT_cmult)

lemma value_flow:
  assumes f: "flow Δ f"
  and source_out: "y. edge Δ (source Δ) y  y = x"
  shows "value_flow Δ f = f (source Δ, x)"
proof -
  have "value_flow Δ f = (+ yOUT (source Δ). f (source Δ, y))"
    by(rule d_OUT_alt_def)(simp add: flowD_outside[OF f])
  also have " = (+ y. f (source Δ, y) * indicator {x} y)"
    by(subst nn_integral_count_space_indicator)(auto intro!: nn_integral_cong split: split_indicator simp add: outgoing_def source_out)
  also have " = f (source Δ, x)" by(simp add: one_ennreal_def[symmetric] max_def)
  finally show ?thesis .
qed

end

context flow_attainability begin

lemma value_plus_flow:
  assumes wf: "wf_residual_network"
  and f: "flow Δ f"
  and g: "flow (residual_network f) g"
  shows "value_flow Δ (f  g) = value_flow Δ f + value_flow Δ g"
proof -
  interpret RES: countable_network "residual_network f" using wf f by(rule residual_countable_network)
  have "value_flow Δ (f  g) = (+ y. f (source Δ, y) + g (source Δ, y))"
    unfolding d_OUT_def by(rule nn_integral_cong)(simp add: flowD_outside[OF f] RES.flowD_outside[OF g] source_in)
  also have " = value_flow Δ f + value_flow Δ g" unfolding d_OUT_def
    by(rule nn_integral_add) simp_all
  finally show ?thesis .
qed

lemma flow_residual_add: ― ‹Lemma 5.3›
  assumes wf: "wf_residual_network"
  and f: "flow Δ f"
  and g: "flow (residual_network f) g"
  shows "flow Δ (f  g)"
proof
  fix e
  { assume e: "e  E"
    hence "(f  g) e = f e + g e - g (prod.swap e)" by(cases e) simp
    also have "  f e + g e - 0" by(rule ennreal_minus_mono) simp_all
    also have "  f e + (capacity Δ e - f e)"
      using e flowD_capacity[OF g, of e] by(simp split: prod.split_asm add: add_mono)
    also have " = capacity Δ e" using flowD_capacity[OF f, of e]
      by simp
    also note calculation }
  thus "(f  g) e  capacity Δ e" by(cases e) auto
next
  fix x
  assume x: "x  source Δ" "x  sink Δ"
  have g_le_f: "g (y, x)  f (x, y)" if "edge Δ x y" for x y
    using that flowD_capacity[OF g, of "(y, x)"]
    by(auto split: if_split_asm dest: wf_residual_networkD[OF wf] elim: order_trans)

  interpret RES: flow_attainability "residual_network f" using wf f by(rule residual_flow_attainability)

  have finite1: "(+ y. g (y, x) * indicator A (f y))  " for A f
    using RES.flowD_finite_IN[OF g, of x]
    by(rule neq_top_trans)(auto simp add: x d_IN_def split: split_indicator intro: nn_integral_mono)
  have finite2: "(+ y. g (x, y) * indicator A (f y))  " for A f
    using RES.flowD_finite_OUT[OF g, of x]
    by(rule neq_top_trans)(auto simp add: x d_OUT_def split: split_indicator intro: nn_integral_mono)

  have "d_OUT (f  g) x = d_OUT f x + (+ y. g (x, y) * indicator E (x, y)) - (+ y. g (y, x) * indicator E (x, y))"
    (is "_ = ?f + ?g_out - ?g_in")
    using flowD_outside[OF f] g_le_f RES.flowD_finite_IN[OF g, of x]
    by(rule OUT_plus_flow)(simp_all add: x)
  also have "?f = d_IN f x" using f x by(auto dest: flowD_KIR)
  also have "?g_out = (+ y. g (x, y) * indicator (- E) (y, x))"
  proof -
    have "(+ y. g (x, y) * indicator (- E) (y, x)) =
          (+ y. g (x, y) * indicator E (x, y)) + (+ y. g (x, y) * indicator (- E) (x, y) * indicator (- E) (y, x))"
      by(subst nn_integral_add[symmetric])(auto simp add: AE_count_space dest: wf_residual_networkD[OF wf] split: split_indicator intro!: nn_integral_cong)
    also have "(+ y. g (x, y) * indicator (- E) (x, y) * indicator (- E) (y, x)) = 0"
      using RES.flowD_outside[OF g]
      by(auto simp add: nn_integral_0_iff_AE AE_count_space split: split_indicator)
    finally show ?thesis by simp
  qed
  also have " = (+ y. g (x, y) - g (x, y) * indicator E (y, x))"
    by(rule nn_integral_cong)(simp split: split_indicator add: RES.flowD_finite[OF g])
  also have " = d_OUT g x - (+ y. g (x, y) * indicator E (y, x))"
    (is "_ = _ - ?g_in_E") unfolding d_OUT_def
    by(subst nn_integral_diff)(simp_all add: AE_count_space finite2 split: split_indicator)
  also have "d_IN f x + (d_OUT g x - (+ y. g (x, y) * indicator E (y, x))) - ?g_in =
    ((d_IN f x + d_OUT g x) - (+ y. g (x, y) * indicator E (y, x))) - ?g_in"
    by (subst add_diff_eq_ennreal) (auto simp: d_OUT_def intro!: nn_integral_mono split: split_indicator)
  also have "d_OUT g x = d_IN g x" using x g by(auto dest: flowD_KIR)
  also have " = (+ yUNIV. g (y, x) * indicator (- E) (y, x)) + (+ y. g (y, x) * indicator E (y, x))"
    (is "_ = ?x + ?g_in_E'")
    by(subst nn_integral_add[symmetric])(auto intro!: nn_integral_cong simp add: d_IN_def AE_count_space split: split_indicator)
  also have "?x = ?g_in"
  proof -
    have "?x = (+ y. g (y, x) * indicator (- E) (x, y) * indicator (- E) (y, x)) + ?g_in"
      by(subst nn_integral_add[symmetric])(auto simp add: AE_count_space  dest: wf_residual_networkD[OF wf] split: split_indicator intro!: nn_integral_cong)
    also have "(+ y. g (y, x) * indicator (- E) (x, y) * indicator (- E) (y, x)) = 0"
      using RES.flowD_outside[OF g]
      by(auto simp add: nn_integral_0_iff_AE AE_count_space split: split_indicator)
    finally show ?thesis by simp
  qed
  also have "(d_IN f x + (?g_in + ?g_in_E') - ?g_in_E) - ?g_in =
    d_IN f x + ?g_in_E' + ?g_in - ?g_in - ?g_in_E"
    by (subst diff_diff_commute_ennreal) (simp add: ac_simps)
  also have " = d_IN f x + ?g_in_E' - ?g_in_E"
    by (subst ennreal_add_diff_cancel_right) (simp_all add: finite1)
  also have " = d_IN (f  g) x"
    using flowD_outside[OF f]  g_le_f RES.flowD_finite_OUT[OF g, of x]
    by(rule IN_plus_flow[symmetric])(simp_all add: x)
  finally show "KIR (f  g) x" by simp
qed

definition minus_flow :: "'v flow  'v flow  'v flow" (infixl "" 65)
where
  "f  g = (λ(x, y). if edge Δ x y then f (x, y) - g (x, y) else if edge Δ y x then g (y, x) - f (y, x) else 0)"

lemma minus_flow_simps [simp]:
  "(f  g) (x, y) = (if edge Δ x y then f (x, y) - g (x, y) else if edge Δ y x then g (y, x) - f (y, x) else 0)"
by(simp add: minus_flow_def)

lemma minus_flow:
  assumes wf: "wf_residual_network"
  and f: "flow Δ f"
  and g: "flow Δ g"
  and value_le: "value_flow Δ g  value_flow Δ f"
  and f_finite: "f (source Δ, x)  "
  and source_out: "y. edge Δ (source Δ) y  y = x"
  shows "flow (residual_network g) (f  g)" (is "flow  ?f")
proof
  show "?f e  capacity  e" for e
    using value_le f_finite flowD_capacity[OF g] flowD_capacity[OF f]
    by(cases e)(auto simp add: source_in source_out value_flow[OF f source_out] value_flow[OF g source_out] less_top
                     intro!: diff_le_self_ennreal diff_eq_0_ennreal ennreal_minus_mono)

  fix x
  assume "x  source " "x  sink "
  hence x: "x  source Δ" "x  sink Δ" by simp_all

  have finite_f_in: "(+ y. f (y, x) * indicator A y)  top" for A
    using flowD_finite_IN[OF f, of x]
    by(rule neq_top_trans)(auto simp add: x d_IN_def split: split_indicator intro!: nn_integral_mono)
  have finite_f_out: "(+ y. f (x, y) * indicator A y)  top" for A
    using flowD_finite_OUT[OF f, of x]
    by(rule neq_top_trans)(auto simp add: x d_OUT_def split: split_indicator intro!: nn_integral_mono)
  have finite_f[simp]: "f (x, y)  top" "f (y, x)  top" for y
    using finite_f_in[of "{y}"] finite_f_out[of "{y}"] by auto

  have finite_g_in: "(+ y. g (y, x) * indicator A y)  top" for A
    using flowD_finite_IN[OF g, of x]
    by(rule neq_top_trans)(auto simp add: x d_IN_def split: split_indicator intro!: nn_integral_mono)
  have finite_g_out: "(+ y. g (x, y) * indicator A y)  top" for A
    using flowD_finite_OUT[OF g x]
    by(rule neq_top_trans)(auto simp add: x d_OUT_def split: split_indicator intro!: nn_integral_mono)
  have finite_g[simp]: "g (x, y)  top" "g (y, x)  top" for y
    using finite_g_in[of "{y}"] finite_g_out[of "{y}"] by auto

  have "d_OUT (f  g) x = (+ y. (f (x, y) - g (x, y)) * indicator E (x, y) * indicator {y. g (x, y)  f (x, y)} y) +
    (+ y. (g (y, x) - f (y, x)) * indicator E (y, x) * indicator {y. f (y, x) < g (y, x)} y)"
    (is "_ = ?out + ?in" is "_ = (+ y_. _ * ?f_ge_g y) + (+ y_. _ * ?g_gt_f y)")
    using flowD_finite[OF g]
    apply(subst nn_integral_add[symmetric])
    apply(auto 4 4 simp add: d_OUT_def not_le less_top[symmetric] intro!: nn_integral_cong
           dest!: wf_residual_networkD[OF wf] split: split_indicator intro!: diff_eq_0_ennreal)
    done
  also have "?in = (+ y. (g (y, x) - f (y, x)) * ?g_gt_f y)"
    using flowD_outside[OF f] flowD_outside[OF g] by(auto intro!: nn_integral_cong split: split_indicator)
  also have " = (+ yUNIV. g (y, x) * ?g_gt_f y) - (+ y. f (y, x) * ?g_gt_f y)" (is "_ = ?g_in - ?f_in")
    using finite_f_in
    by(subst nn_integral_diff[symmetric])(auto simp add: AE_count_space split: split_indicator intro!: nn_integral_cong)
  also have "?out = (+ y. (f (x, y) - g (x, y)) * ?f_ge_g y)"
    using flowD_outside[OF f] flowD_outside[OF g] by(auto intro!: nn_integral_cong split: split_indicator)
  also have " = (+ y. f (x, y) * ?f_ge_g y) - (+ y. g (x, y) * ?f_ge_g y)" (is "_ = ?f_out - ?g_out")
    using finite_g_out
    by(subst nn_integral_diff[symmetric])(auto simp add: AE_count_space split: split_indicator intro!: nn_integral_cong)
  also have "?f_out = d_OUT f x - (+ y. f (x, y) * indicator {y. f (x, y) < g (x, y)} y)" (is "_ = _ - ?f_out_less")
    unfolding d_OUT_def using flowD_finite[OF f] using finite_f_out
    by(subst nn_integral_diff[symmetric])(auto split: split_indicator intro!: nn_integral_cong)
  also have "?g_out = d_OUT g x - (+ y. g (x, y) * indicator {y. f (x, y) < g (x, y)} y)" (is "_ = _ - ?g_less_f")
    unfolding d_OUT_def using flowD_finite[OF g] finite_g_out
    by(subst nn_integral_diff[symmetric])(auto split: split_indicator intro!: nn_integral_cong)
  also have "d_OUT f x - ?f_out_less - (d_OUT g x - ?g_less_f) + (?g_in - ?f_in) =
    (?g_less_f + (d_OUT f x - ?f_out_less)) - d_OUT g x + (?g_in - ?f_in)"
    by (subst diff_diff_ennreal')
       (auto simp: ac_simps d_OUT_def nn_integral_diff[symmetric] finite_g_out finite_f_out intro!: nn_integral_mono split: split_indicator )
  also have " = ?g_less_f + d_OUT f x - ?f_out_less - d_OUT g x + (?g_in - ?f_in)"
    by (subst add_diff_eq_ennreal)
       (auto simp: d_OUT_def intro!: nn_integral_mono split: split_indicator)
  also have " = d_OUT f x + ?g_less_f - ?f_out_less - d_OUT g x + (?g_in - ?f_in)"
    by (simp add: ac_simps)
  also have " = d_OUT f x + (?g_less_f - ?f_out_less) - d_OUT g x + (?g_in - ?f_in)"
    by (subst add_diff_eq_ennreal[symmetric])
       (auto intro!: nn_integral_mono split: split_indicator)
  also have " = (?g_in - ?f_in) + ((?g_less_f - ?f_out_less) + d_OUT f x - d_OUT g x)"
    by (simp add: ac_simps)
  also have " = ((?g_in - ?f_in) + ((?g_less_f - ?f_out_less) + d_OUT f x)) - d_OUT g x"
    apply (subst add_diff_eq_ennreal)
    apply (simp_all add: d_OUT_def)
    apply (subst nn_integral_diff[symmetric])
    apply (auto simp: AE_count_space finite_f_out nn_integral_add[symmetric] not_less diff_add_cancel_ennreal intro!: nn_integral_mono split: split_indicator)
    done
  also have " = ((?g_less_f - ?f_out_less) + (d_OUT f x + (?g_in - ?f_in))) - d_OUT g x"
    by (simp add: ac_simps)
  also have " = ((?g_less_f - ?f_out_less) + (d_IN f x + (?g_in - ?f_in))) - d_IN g x"
    unfolding flowD_KIR[OF f x] flowD_KIR[OF g x] ..
  also have " = (?g_less_f - ?f_out_less) + ((d_IN f x + (?g_in - ?f_in)) - d_IN g x)"
    apply (subst (2) add_diff_eq_ennreal)
    apply (simp_all add: d_IN_def)
    apply (subst nn_integral_diff[symmetric])
    apply (auto simp: AE_count_space finite_f_in finite_f_out nn_integral_add[symmetric] not_less  ennreal_ineq_diff_add[symmetric]
                intro!: nn_integral_mono split: split_indicator)
    done
  also have " = (?g_less_f - ?f_out_less) + (d_IN f x + ?g_in - d_IN g x - ?f_in)"
    by (subst (2) add_diff_eq_ennreal) (auto intro!: nn_integral_mono split: split_indicator simp: diff_diff_commute_ennreal)
  also have " = (?g_less_f - ?f_out_less) + (d_IN f x - (d_IN g x - ?g_in) - ?f_in)"
    apply (subst diff_diff_ennreal')
    apply (auto simp: d_IN_def intro!: nn_integral_mono split: split_indicator)
    apply (subst nn_integral_diff[symmetric])
    apply (auto simp: AE_count_space finite_g_in intro!: nn_integral_mono split: split_indicator)
    done
  also have " =(d_IN f x - ?f_in) - (d_IN g x - ?g_in) + (?g_less_f - ?f_out_less)"
    by (simp add: ac_simps diff_diff_commute_ennreal)
  also have "?g_less_f - ?f_out_less = (+ y. (g (x, y) - f (x, y)) * indicator {y. f (x, y) < g (x, y)} y)" using finite_f_out
    by(subst nn_integral_diff[symmetric])(auto simp add: AE_count_space split: split_indicator intro!: nn_integral_cong)
  also have " = (+ y. (g (x, y) - f (x, y)) * indicator E (x, y) * indicator {y. f (x, y) < g (x, y)} y)" (is "_ = ?diff_out")
    using flowD_outside[OF f] flowD_outside[OF g] by(auto intro!: nn_integral_cong split: split_indicator)
  also have "d_IN f x - ?f_in = (+ y. f (y, x) * indicator {y. g (y, x)  f (y, x)} y)"
    unfolding d_IN_def using finite_f_in
    apply(subst nn_integral_diff[symmetric])
    apply(auto simp add: AE_count_space split: split_indicator intro!: nn_integral_cong)
    done
  also have "d_IN g x - ?g_in = (+ y. g (y, x) * indicator {y. g (y, x)  f (y, x)} y)"
    unfolding d_IN_def using finite_g_in
    by(subst nn_integral_diff[symmetric])(auto simp add: flowD_finite[OF g] AE_count_space split: split_indicator intro!: nn_integral_cong)
  also have "(+ yUNIV. f (y, x) * indicator {y. g (y, x)  f (y, x)} y) -  = (+ y. (f (y, x) - g (y, x)) * indicator {y. g (y, x)  f (y, x)} y)"
    using finite_g_in
    by(subst nn_integral_diff[symmetric])(auto simp add: flowD_finite[OF g] AE_count_space split: split_indicator intro!: nn_integral_cong)
  also have " = (+ y. (f (y, x) - g (y, x)) * indicator E (y, x) * indicator {y. g (y, x)  f (y, x)} y)"
    using flowD_outside[OF f] flowD_outside[OF g] by(auto intro!: nn_integral_cong split: split_indicator)
  also have " + ?diff_out = d_IN ?f x"
    using flowD_finite[OF g]
    apply(subst nn_integral_add[symmetric])
    apply(auto 4 4 simp add: d_IN_def not_le less_top[symmetric] intro!: nn_integral_cong
               dest!: wf_residual_networkD[OF wf] split: split_indicator intro: diff_eq_0_ennreal)
    done
  finally show "KIR ?f x" .
qed

lemma value_minus_flow:
  assumes f: "flow Δ f"
  and g: "flow Δ g"
  and value_le: "value_flow Δ g  value_flow Δ f"
  and source_out: "y. edge Δ (source Δ) y  y = x"
  shows "value_flow Δ (f  g) = value_flow Δ f - value_flow Δ g" (is "?value")
proof -
  have "value_flow Δ (f  g) = (+ yOUT (source Δ). (f  g) (source Δ, y))"
    by(subst d_OUT_alt_def)(auto simp add: flowD_outside[OF f] flowD_outside[OF g] source_in)
  also have " = (+ y. (f (source Δ, y) - g (source Δ, y)) * indicator {x} y)"
    by(subst nn_integral_count_space_indicator)(auto intro!: nn_integral_cong split: split_indicator simp add: outgoing_def source_out)
  also have " = f (source Δ, x) - g (source Δ, x)"
    using value_le value_flow[OF f source_out] value_flow[OF g source_out]
    by(auto simp add: one_ennreal_def[symmetric] max_def not_le intro: antisym)
  also have " = value_flow Δ f - value_flow Δ g" using f g source_out by(simp add: value_flow)
  finally show ?value .
qed

context
  fixes α
  defines "α  (SUP g{g. flow Δ g}. value_flow Δ g)"
begin

lemma flow_by_value:
  assumes "v < α"
  and real[rule_format]: "f. α =   flow Δ f  value_flow Δ f < α"
  obtains f where "flow Δ f" "value_flow Δ f = v"
proof -
  have α_pos: "α > 0" using assms by (auto simp add: zero_less_iff_neq_zero)
  from v < α obtain f where f: "flow Δ f" and v: "v < value_flow Δ f"
    unfolding α_def less_SUP_iff by blast
  have [simp]: "value_flow Δ f  "
  proof
    assume val: "value_flow Δ f = "
    from f have "value_flow Δ f  α" unfolding α_def by(blast intro: SUP_upper2)
    with val have "α = " by (simp add: top_unique)
    from real[OF this f] val show False by simp
  qed
  let ?f = "λe. (v / value_flow Δ f) * f e"
  note f
  moreover
  have *: "0 < value_flow Δ f"
    using v < value_flow Δ f by (auto simp add: zero_less_iff_neq_zero)
  then have "v / value_flow Δ f  1" using v
    by (auto intro!: divide_le_posI_ennreal)
  ultimately have "flow Δ ?f" by (rule scale_flow)
  moreover {
    have "value_flow Δ ?f = v * (value_flow Δ f / value_flow Δ f)"
      by(subst value_scale_flow)(simp add: divide_ennreal_def ac_simps)
    also have " = v" using * by(subst ennreal_divide_self) (auto simp: less_top[symmetric])
    also note calculation }
  ultimately show ?thesis by(rule that)
qed

theorem ex_max_flow':
  assumes wf: "wf_residual_network"
  assumes source_out: "y. edge Δ (source Δ) y  y = x"
  and nontrivial: "V - {source Δ, sink Δ}  {}"
  and real: "α = ennreal α'" and α'_nonneg[simp]: "0  α'"
  shows "f. flow Δ f  value_flow Δ f = α  (x. d_IN f x  value_flow Δ f)"
proof -
  have α'_not_neg[simp]: "¬ α' < 0"
    using α'_nonneg by linarith

  let ?v = "λi. (1 - (1 / 2) ^ i) * α"
  let ?v_r = "λi. ennreal ((1 - (1 / 2) ^ i) * α')"
  have v_eq: "?v i = ?v_r i" for i
    by (auto simp: real ennreal_mult power_le_one ennreal_lessI ennreal_minus[symmetric]
                   ennreal_power[symmetric] divide_ennreal_def)
  have "f. flow Δ f  value_flow Δ f = ?v i" for i :: nat
  proof(cases "α = 0")
    case True thus ?thesis by(auto intro!: exI[where x="λ_. 0"])
  next
    case False
    then have "?v i < α"
      unfolding v_eq by (auto simp: real field_simps intro!: ennreal_lessI) (simp_all add: less_le)
    then obtain f where "flow Δ f" and "value_flow Δ f = ?v i"
      by(rule flow_by_value)(simp add: real)
    thus ?thesis by blast
  qed
  then obtain f_aux where f_aux: "i. flow Δ (f_aux i)"
    and value_aux: "i. value_flow Δ (f_aux i) = ?v_r i"
    unfolding v_eq by moura

  define f_i where "f_i = rec_nat (λ_. 0) (λi f_i.
    let g = f_aux (Suc i)  f_i;
      k_i = SOME k. k  g  flow (residual_network f_i) k  value_flow (residual_network f_i) k = value_flow (residual_network f_i) g  (x. d_IN k x  value_flow (residual_network f_i) k)
    in f_i  k_i)"
  let ?P = "λi k. k  f_aux (Suc i)  f_i i  flow (residual_network (f_i i)) k  value_flow (residual_network (f_i i)) k = value_flow (residual_network (f_i i)) (f_aux (Suc i)  f_i i)  (x. d_IN k x  value_flow (residual_network (f_i i)) k)"
  define k_i where "k_i i = Eps (?P i)" for i

  have f_i_simps [simp]: "f_i 0 = (λ_. 0)" "f_i (Suc i) = f_i i  k_i i" for i
    by(simp_all add: f_i_def Let_def k_i_def)

  have k_i: "flow (residual_network (f_i i)) (k_i i)" (is ?k_i)
    and value_k_i: "value_flow (residual_network (f_i i)) (k_i i) = value_flow (residual_network (f_i i)) (f_aux (Suc i)  f_i i)" (is "?value_k_i")
    and IN_k_i: "d_IN (k_i i) x  value_flow (residual_network (f_i i)) (k_i i)" (is "?IN_k_i")
    and value_diff: "value_flow (residual_network (f_i i)) (f_aux (Suc i)  f_i i) = value_flow Δ (f_aux (Suc i)) - value_flow Δ (f_i i)" (is "?value_diff")
    if "flow_network Δ (f_i i)" and value_f_i: "value_flow Δ (f_i i) = value_flow Δ (f_aux i)" for i x
  proof -
    let ?RES = "residual_network (f_i i)"
    interpret fn: flow_network Δ "f_i i" by(rule that)
    interpret RES: flow_attainability "?RES" using wf fn.g by(rule residual_flow_attainability)
    have le: "value_flow Δ (f_i i)  value_flow Δ (f_aux (Suc i))"
      unfolding value_aux value_f_i
      unfolding v_eq by (rule ennreal_leI) (auto simp: field_simps)
    with wf f_aux fn.g have res_flow: "flow ?RES (f_aux (Suc i)  f_i i)"
      using flowD_finite[OF f_aux] source_out
      by(rule minus_flow)
    show value': ?value_diff by(simp add: value_minus_flow[OF f_aux fn.g le source_out])
    also have " < "
      unfolding value_aux v_eq by (auto simp: less_top[symmetric])
    finally have "value_flow ?RES (f_aux (Suc i)  f_i i)  " by simp
    then have fn': "flow_network ?RES (f_aux (Suc i)  f_i i)"
      using nontrivial res_flow by(unfold_locales) simp_all
    then interpret fn': flow_network "?RES" "f_aux (Suc i)  f_i i" .
    from fn'.flow_cleanup show ?k_i ?value_k_i ?IN_k_i unfolding k_i_def by(rule someI2_ex; blast)+
  qed

  have fn_i: "flow_network Δ (f_i i)"
    and value_f_i: "value_flow Δ (f_i i) = value_flow Δ (f_aux i)"
    and d_IN_i: "d_IN (f_i i) x  value_flow Δ (f_i i)"  for i x
  proof(induction i)
    case 0
    { case 1 show ?case using nontrivial by(unfold_locales)(simp_all add: f_aux value_aux) }
    { case 2 show ?case by(simp add: value_aux) }
    { case 3 show ?case by(simp) }
  next
    case (Suc i)
    interpret fn: flow_network Δ "f_i i" using Suc.IH(1) .
    let ?RES = "residual_network (f_i i)"

    have k_i: "flow ?RES (k_i i)"
      and value_k_i: "value_flow ?RES (k_i i) = value_flow ?RES (f_aux (Suc i)  f_i i)"
      and d_IN_k_i: "d_IN (k_i i) x  value_flow ?RES (k_i i)" for x
      using Suc.IH(1-2) by(rule k_i value_k_i IN_k_i)+

    interpret RES: flow_attainability "?RES" using wf fn.g by(rule residual_flow_attainability)
    have le: "value_flow Δ (f_i i)  value_flow Δ (f_aux (Suc i))"
      unfolding value_aux Suc.IH(2) v_eq using α'_nonneg by(intro ennreal_leI)(simp add: real field_simps)
    { case 1 show ?case unfolding f_i_simps
      proof
        show "flow Δ (f_i i  k_i i)" using wf fn.g k_i by(rule flow_residual_add)
        with RES.flowD_finite[OF k_i] show "value_flow Δ (f_i i  k_i i)  "
          by(simp add: value_flow[OF _ source_out])
      qed(rule nontrivial) }
    from value_k_i have value_k: "value_flow ?RES (k_i i) = value_flow Δ (f_aux (Suc i)) - value_flow Δ (f_aux i)"
      by(simp add: value_minus_flow[OF f_aux fn.g le source_out] Suc.IH)
    { case 2 show ?case using value_k
        by(auto simp add: source_out value_plus_flow[OF wf fn.g k_i] Suc.IH value_aux field_simps intro!: ennreal_leI) }
    note value_f = this
    { case 3
      have "d_IN (f_i i  k_i i) x  d_IN (f_i i) x + d_IN (k_i i) x"
        using fn.g k_i by(rule d_IN_plus_flow[OF wf])
      also have "  value_flow Δ (f_i i) + d_IN (k_i i) x" using Suc.IH(3) by(rule add_right_mono)
      also have "  value_flow Δ (f_i i) + value_flow ?RES (k_i i)" using d_IN_k_i by(rule add_left_mono)
      also have " = value_flow Δ (f_i (Suc i))" unfolding value_f Suc.IH(2) value_k
        by(auto simp add: value_aux field_simps intro!: ennreal_leI)
      finally show ?case by simp }
  qed
  interpret fn: flow_network Δ "f_i i" for i by(rule fn_i)
  note k_i = k_i[OF fn_i value_f_i] and value_k_i = value_k_i[OF fn_i value_f_i]
    and IN_k_i = IN_k_i[OF fn_i value_f_i] and value_diff = value_diff[OF fn_i value_f_i]

  have "x0. f_i i e = ennreal x" for i e
    using fn.finite_g[of i e] by (cases "f_i i e") auto
  then obtain f_i' where f_i': "i e. f_i i e = ennreal (f_i' i e)" and [simp]: "i e. 0  f_i' i e"
    by metis

  { fix i e
    obtain x y :: 'v where e: "e = (x, y)" by(cases e)
    have "k_i i (x, y)  d_IN (k_i i) y" by (rule d_IN_ge_point)
    also have "  value_flow (residual_network (f_i i)) (k_i i)" by(rule IN_k_i)
    also have " < " using value_k_i[of i] value_diff[of i]
      by(simp add: value_k_i value_f_i value_aux real less_top[symmetric])
    finally have "x0. k_i i e = ennreal x"
      by(cases "k_i i e")(auto simp add: e) }
  then obtain k_i' where k_i': "i e. k_i i e = ennreal (k_i' i e)" and k_i'_nonneg[simp]: "i e. 0  k_i' i e"
    by metis

  have wf_k: "(x, y)  E  k_i i (y, x)  f_i i (x, y) + k_i i (x, y)" for i x y
    using flowD_capacity[OF k_i, of i "(y, x)"]
    by (auto split: if_split_asm dest: wf_residual_networkD[OF wf] elim: order_trans)

  have f_i'_0[simp]: "f_i' 0 = (λ_. 0)" using f_i_simps(1) by (simp del: f_i_simps add: fun_eq_iff f_i')

  have f_i'_Suc[simp]: "f_i' (Suc i) e =  (if e  E then f_i' i e + (k_i' i e - k_i' i (prod.swap e)) else 0)" for i e
    using f_i_simps(2)[of i, unfolded fun_eq_iff, THEN spec, of e] wf_k[of "fst e" "snd e" i]
    by (auto simp del: f_i_simps ennreal_plus
             simp add: fun_eq_iff f_i' k_i' ennreal_plus[symmetric] ennreal_minus split: if_split_asm)

  have k_i'_le: "k_i' i e  α' / 2 ^ (Suc i)" for i e
  proof -
    obtain x y where e: "e = (x, y)" by(cases e)
    have "k_i' i (x, y)  d_IN (k_i' i) y" by (rule d_IN_ge_point)
    also have "  value_flow (residual_network (f_i i)) (k_i' i)"
      using IN_k_i[of i y] by(simp add: k_i'[abs_def])
    also have " = α' / 2 ^ (Suc i)" using value_k_i[of i] value_diff[of i]
      by(simp add: value_f_i value_aux real k_i'[abs_def] field_simps ennreal_minus mult_le_cancel_left1)
    finally show ?thesis using e by simp
  qed

  have convergent: "convergent (λi. f_i' i e)" for e
  proof(cases "α' > 0")
    case False
    obtain x y where [simp]: "e = (x, y)" by(cases e)

    { fix i
      from False α'_nonneg have "α' = 0" by simp
      moreover have "f_i i (x, y)  d_IN (f_i i) y" by (rule d_IN_ge_point)
      ultimately have "f_i i (x, y) = 0" using d_IN_i[of i y]
        by(simp add: value_f_i value_aux real) }
    thus ?thesis by(simp add: f_i' convergent_const)
  next
    case α'_pos: True
    show ?thesis
    proof(rule real_Cauchy_convergent Cauchy_real_Suc_diff)+
      fix n
      have "¦k_i' n e - k_i' n (prod.swap e)¦  ¦k_i' n e¦ + ¦k_i' n (prod.swap e)¦"
        by (rule abs_triangle_ineq4)
      then have "¦k_i' n e - k_i' n (prod.swap e)¦  α' / 2 ^ n"
        using k_i'_le[of n e] k_i'_le[of n "prod.swap e"] by simp
      then have "¦f_i' (Suc n) e - f_i' n e¦  α' / 2 ^ n"
        using flowD_outside[OF fn.g] by (cases e) (auto simp: f_i')
      thus "¦f_i' (Suc n) e - f_i' n e¦  α' / 2 ^ n" by simp
    qed simp
  qed
  then obtain f' where f': "e. (λi. f_i' i e)  f' e" unfolding convergent_def by metis
  hence f: "e. (λi. f_i i e)  ennreal (f' e)" unfolding f_i' by simp

  have f'_nonneg: "0  f' e" for e
    by (rule LIMSEQ_le_const[OF f']) auto

  let ?k = "λi x y. (k_i' i (x, y) - k_i' i (y, x)) * indicator E (x, y)"
  have sum_i': "f_i' i (x, y) = (j<i. ?k j x y)" for x y i
    by (induction i) auto

  have summable_nk: "summable (λi. ¦?k i x y¦)" for x y
  proof(rule summable_rabs_comparison_test)
    show "N. iN. ¦?k i x y¦  α' * (1 / 2) ^ i"
    proof (intro exI allI impI)
      fix i have "¦?k i x y¦  k_i' i (x, y) + k_i' i (y, x)"
        by (auto intro!: abs_triangle_ineq4[THEN order_trans] split: split_indicator)
      also have "  α' * (1 / 2) ^ i"
        using k_i'_le[of i "(x, y)"] k_i'_le[of i "(y, x)"] α'_nonneg k_i'_nonneg[of i "(x, y)"] k_i'_nonneg[of i "(y, x)"]
        by(auto simp add: abs_real_def power_divide split: split_indicator)
      finally show "¦?k i x y¦  α' * (1 / 2) ^ i"
        by simp
    qed
    show "summable (λi. α' * (1 / 2) ^ i)"
      by(rule summable_mult complete_algebra_summable_geometric)+ simp
  qed
  hence summable_k: "summable (λi. ?k i x y)" for x y by(auto intro: summable_norm_cancel)

  have suminf: "(i. (k_i' i (x, y) - k_i' i (y, x)) * indicator E (x, y)) = f' (x, y)" for x y
    by(rule LIMSEQ_unique[OF summable_LIMSEQ])(simp_all add: sum_i'[symmetric] f' summable_k)

  have flow: "flow Δ f'"
  proof
    fix e
    have "f' e  Sup {..capacity Δ e}" using _ f
      by(rule Sup_lim)(simp add: flowD_capacity[OF fn.g])
    then show "f' e  capacity Δ e" by simp
  next
    fix x
    assume x: "x  source Δ" "x  sink Δ"

    have integrable_f_i: "integrable (count_space UNIV) (λy. f_i' i (x, y))" for i
      using flowD_finite_OUT[OF fn.g x, of i] by(auto intro!: integrableI_bounded simp add: f_i' d_OUT_def less_top)
    have integrable_f_i': "integrable (count_space UNIV) (λy. f_i' i (y, x))" for i
      using flowD_finite_IN[OF fn.g, of x i] x by(auto intro!: integrableI_bounded simp add: f_i' d_IN_def less_top)

    have integral_k_bounded: "(+ y. norm (?k i x y))  α' / 2 ^ i" (is ?thesis1)
      and integral_k'_bounded: "(+ y. norm (?k i y x))  α' / 2 ^ i" (is ?thesis2) for i
    proof -
      define b where "b = (+ y. k_i i (x, y) + k_i i (y, x))"
      have "b = d_OUT (k_i i) x + d_IN (k_i i) x" unfolding b_def
        by(subst nn_integral_add)(simp_all add: d_OUT_def d_IN_def)
      also have "d_OUT (k_i i) x = d_IN (k_i i) x" using k_i by(rule flowD_KIR)(simp_all add: x)
      also have " +   value_flow Δ (k_i i) + value_flow Δ (k_i i)"
        using IN_k_i[of i x, simplified] by-(rule add_mono)
      also have "  α' / 2 ^ i" using value_k_i[of i] value_diff[of i]
        by(simp add: value_aux value_f_i  field_simps ennreal_minus_if ennreal_plus_if mult_le_cancel_left1
                del: ennreal_plus)
      also have "(+ yUNIV. norm (?k i x y))  b" and "(+ y. norm (?k i y x))  b" unfolding b_def
        by(rule nn_integral_mono; simp add: abs_real_def k_i' ennreal_plus_if del:  ennreal_plus split: split_indicator)+
      ultimately show ?thesis1 ?thesis2 by(auto)
    qed

    have integrable_k: "integrable (count_space UNIV) (λy. ?k i x y)"
      and integrable_k': "integrable (count_space UNIV) (λy. ?k i y x)" for i
      using integral_k_bounded[of i] integral_k'_bounded[of i] real
      by(auto intro!: integrableI_bounded simp: less_top[symmetric] top_unique ennreal_divide_eq_top_iff)

    have summable'_k: "summable (λi.  y. ¦?k i x y¦ count_space UNIV)"
    proof(rule summable_comparison_test)
      have "¦ y. ¦?k i x y¦ count_space UNIV¦  α' * (1 / 2) ^ i" for i
        using integral_norm_bound_ennreal[OF integrable_norm, OF integrable_k, of i] integral_k_bounded[of i]
        by(bestsimp simp add: real power_divide dest: order_trans)
      thus "N. iN. norm ( y. ¦?k i x y¦ count_space UNIV)  α' * (1 / 2) ^ i"
        by auto
      show "summable (λi. α' * (1 / 2) ^ i)"
        by(rule summable_mult complete_algebra_summable_geometric)+ simp
    qed
    have summable'_k': "summable (λi.  y. ¦?k i y x¦ count_space UNIV)"
    proof(rule summable_comparison_test)
      have "¦ y. ¦?k i y x¦ count_space UNIV¦  α' * (1 / 2) ^ i" for i
        using integral_norm_bound_ennreal[OF integrable_norm, OF integrable_k', of i] integral_k'_bounded[of i]
        by(bestsimp simp add: real power_divide dest: order_trans)
      thus "N. iN. norm ( y. ¦?k i y x¦ count_space UNIV)  α' * (1 / 2) ^ i" by auto
      show "summable (λi. α' * (1 / 2) ^ i)"
        by(rule summable_mult complete_algebra_summable_geometric)+ simp
    qed

    have "(λi.  y. ?k i x y count_space UNIV) sums  y. (i. ?k i x y) count_space UNIV"
      using integrable_k by(rule sums_integral)(simp_all add: summable_nk summable'_k)
    also have " =  y. f' (x, y) count_space UNIV" by(rule Bochner_Integration.integral_cong[OF refl])(rule suminf)
    finally have "(λi. j<i.  y. ?k j x y count_space UNIV)  " unfolding sums_def .
    also have "(λi. j<i.  y. ?k j x y count_space UNIV) = (λi.  y. f_i' i (x, y) count_space UNIV)"
      unfolding sum_i' by(rule ext Bochner_Integration.integral_sum[symmetric] integrable_k)+
    finally have "(λi. ennreal ( y. f_i' i (x, y) count_space UNIV))  ennreal ( y. f' (x, y) count_space UNIV)" by simp
    also have "(λi. ennreal ( y. f_i' i (x, y) count_space UNIV)) = (λi. d_OUT (f_i i) x)"
      unfolding d_OUT_def f_i' by(rule ext nn_integral_eq_integral[symmetric] integrable_f_i)+ simp
    also have "ennreal ( y. f' (x, y) count_space UNIV) = d_OUT f' x"
      unfolding d_OUT_def by(rule nn_integral_eq_integral[symmetric])(simp_all add: f'_nonneg, simp add: suminf[symmetric] integrable_suminf integrable_k summable_nk summable'_k)
    also have "(λi. d_OUT (f_i i) x) = (λi. d_IN (f_i i) x)"
      using flowD_KIR[OF fn.g x] by(simp)
    finally have *: "(λi. d_IN (f_i i) x)  d_OUT (λx. ennreal (f' x)) x" .

    have "(λi.  y. ?k i y x count_space UNIV) sums  y. (i. ?k i y x) count_space UNIV"
      using integrable_k' by(rule sums_integral)(simp_all add: summable_nk summable'_k')
    also have " =  y. f' (y, x) count_space UNIV" by(rule Bochner_Integration.integral_cong[OF refl])(rule suminf)
    finally have "(λi. j<i.  y. ?k j y x count_space UNIV)  " unfolding sums_def .
    also have "(λi. j<i.  y. ?k j y x count_space UNIV) = (λi.  y. f_i' i (y, x) count_space UNIV)"
      unfolding sum_i' by(rule ext Bochner_Integration.integral_sum[symmetric] integrable_k')+
    finally have "(λi. ennreal ( y. f_i' i (y, x) count_space UNIV))  ennreal ( y. f' (y, x) count_space UNIV)" by simp
    also have "(λi. ennreal ( y. f_i' i (y, x) count_space UNIV)) = (λi. d_IN (f_i i) x)"
      unfolding d_IN_def f_i' by(rule ext nn_integral_eq_integral[symmetric] integrable_f_i')+ simp
    also have "ennreal ( y. f' (y, x) count_space UNIV) = d_IN f' x"
      unfolding d_IN_def by(rule nn_integral_eq_integral[symmetric])(simp_all add: f'_nonneg, simp add: suminf[symmetric] integrable_suminf integrable_k' summable_nk summable'_k')
    finally show "d_OUT f' x = d_IN f' x" using * by(blast intro: LIMSEQ_unique)
  qed
  moreover
  { have "incseq (λi. value_flow Δ (f_i i))"
      by(rule incseq_SucI)(simp add: value_aux value_f_i real field_simps α'_nonneg ennreal_leI del: f_i_simps)
    then have "(λi. value_flow Δ (f_i i))  (SUP i. value_flow Δ (f_i i))" by(rule LIMSEQ_SUP)
    also have "(SUP i. value_flow Δ (f_i i)) = α"
    proof -
      have "α - (SUP i. value_flow Δ (f_i i)) = (INF i. α - value_flow Δ (f_i i))"
        by(simp add: ennreal_SUP_const_minus real)
      also have "α - value_flow Δ (f_i i) = α' / 2 ^ i" for i
        by(simp add: value_f_i value_aux real ennreal_minus_if field_simps mult_le_cancel_left1)
      hence "(INF i. α - value_flow Δ (f_i i)) = (INF i. ennreal (α' / 2  ^ i))"
        by(auto intro: INF_cong)
      also have " = 0"
      proof(rule LIMSEQ_unique)
        show "(λi. α' / 2 ^ i)  (INF i. ennreal (α' / 2  ^ i))"
          by(rule LIMSEQ_INF)(simp add: field_simps real decseq_SucI)
      qed(simp add: LIMSEQ_divide_realpow_zero real ennreal_0[symmetric] del: ennreal_0)
      finally show "(SUP i. value_flow Δ (f_i i)) = α"
        apply (intro antisym)
        apply (auto simp: α_def intro!: SUP_mono fn.g) []
        apply (rule ennreal_minus_eq_0)
        apply assumption
        done
    qed
    also have "(λi. value_flow Δ (f_i i))  value_flow Δ f'"
      by(simp add: value_flow[OF flow source_out] value_flow[OF fn.g source_out] f)
    ultimately have "value_flow Δ f' = α" by(blast intro: LIMSEQ_unique) }
  note value_f = this
  moreover {
    fix x
    have "d_IN f' x = + y. liminf (λi. f_i i (y, x)) count_space UNIV" unfolding d_IN_def using f
      by(simp add: tendsto_iff_Liminf_eq_Limsup)
    also have "  liminf (λi. d_IN (f_i i) x)" unfolding d_IN_def
      by(rule nn_integral_liminf)(simp_all add:)
    also have "  liminf (λi. α)" using d_IN_i[of _ x] fn.g
      by(auto intro!: Liminf_mono SUP_upper2 eventually_sequentiallyI simp add: α_def)
    also have " = value_flow Δ f'" using value_f by(simp add: Liminf_const)
    also note calculation
  } ultimately show ?thesis by blast
qed

theorem ex_max_flow'': ― ‹eliminate assumption of no antiparallel edges using locale @{const wf_residual_network}
  assumes source_out: "y. edge Δ (source Δ) y  y = x"
  and nontrivial: "E  {}"
  and real: "α = ennreal α'" and nn[simp]: "0  α'"
  shows "f. flow Δ f  value_flow Δ f = α  (x. d_IN f x  value_flow Δ f)"
proof -
  interpret antiparallel_edges Δ ..
  interpret Δ'': flow_attainability Δ''
    by(rule Δ''_flow_attainability flow_attainability.axioms(2))+unfold_locales
  have wf_Δ'': "Δ''.wf_residual_network"
    by(rule Δ''_wf_residual_network; simp add: no_loop)

  have source_out': "edge Δ'' (source Δ'') y  y = Edge (source Δ) x" for y
    by(auto simp add: source_out)
  have nontrivial': "VΔ''- {source Δ'', sink Δ''}  {}" using nontrivial by(auto simp add: "V_Δ''")

  have "(SUP g  {g. flow Δ'' g}. value_flow Δ'' g) = (SUP g  {g. flow Δ g}. value_flow Δ g)" (is "?lhs = ?rhs")
  proof(intro antisym SUP_least; unfold mem_Collect_eq)
    fix g
    assume g: "flow Δ'' g"
    hence "value_flow Δ'' g = value_flow Δ (collect g)" by(simp add: value_collect)
    also { from g have "flow Δ (collect g)" by simp }
    then have "  ?rhs" by(blast intro: SUP_upper2)
    finally show "value_flow Δ'' g  " .
  next
    fix g
    assume g: "flow Δ g"
    hence "value_flow Δ g = value_flow Δ'' (split g)" by simp
    also { from g have "flow Δ'' (split g)" by simp }
    then have "  ?lhs" by(blast intro: SUP_upper2)
    finally show "value_flow Δ g  ?lhs" .
  qed
  with real have eq: "(SUP g  {g. flow Δ'' g}. value_flow Δ'' g) = ennreal α'" by(simp add: α_def)
  from Δ''.ex_max_flow'[OF wf_Δ'' source_out' nontrivial' eq]
  obtain f where f: "flow Δ'' f"
    and "value_flow Δ'' f = α"
    and IN: "x. d_IN f x  value_flow Δ'' f" unfolding eq real using nn by blast
  hence "flow Δ (collect f)" and "value_flow Δ (collect f) = α" by(simp_all add: value_collect)
  moreover {
    fix x
    have "d_IN (collect f) x = (+ yrange (λy. Edge y x). f (y, Vertex x))"
      by(simp add: nn_integral_count_space_reindex d_IN_def)
    also have "  d_IN f (Vertex x)" unfolding d_IN_def
      by (auto intro!: nn_integral_mono simp add: nn_integral_count_space_indicator split: split_indicator)
    also have "  value_flow Δ (collect f)" using IN[of "Vertex x"] f by(simp add: value_collect)
    also note calculation }
  ultimately show ?thesis by blast
qed

context begin ― ‹We eliminate the assumption of only one edge leaving the source by introducing a new source vertex.›
private datatype (plugins del: transfer size) 'v' node = SOURCE | Inner (inner: 'v')

private lemma not_Inner_conv: "x  range Inner  x = SOURCE"
by(cases x) auto

private lemma inj_on_Inner [simp]: "inj_on Inner A"
by(simp add: inj_on_def)

private inductive edge' :: "'v node  'v node  bool"
where
  SOURCE: "edge' SOURCE (Inner (source Δ))"
| Inner: "edge Δ x y  edge' (Inner x) (Inner y)"

private inductive_simps edge'_simps [simp]:
  "edge' SOURCE x"
  "edge' (Inner y) x"
  "edge' y SOURCE"
  "edge' y (Inner x)"

private fun capacity' :: "'v node flow"
where
  "capacity' (SOURCE, Inner x) = (if x = source Δ then α else 0)"
| "capacity' (Inner x, Inner y) = capacity Δ (x, y)"
| "capacity' _ = 0"

private lemma capacity'_source_in [simp]: "capacity' (y, Inner (source Δ)) = (if y = SOURCE then α else 0)"
by(cases y)(simp_all add: capacity_outside source_in)

private definition Δ' :: "'v node network"
where "Δ' = edge = edge', capacity = capacity', source = SOURCE, sink = Inner (sink Δ)"

private lemma Δ'_sel [simp]:
  "edge Δ' = edge'"
  "capacity Δ' = capacity'"
  "source Δ' = SOURCE"
  "sink Δ' = Inner (sink Δ)"
by(simp_all add: Δ'_def)

private lemma "E_Δ'": "EΔ'= {(SOURCE, Inner (source Δ))}  (λ(x, y). (Inner x, Inner y)) ` E"
by(auto elim: edge'.cases)

private lemma Δ'_countable_network:
  assumes "α  "
  shows "countable_network Δ'"
proof
  show "countable EΔ'⇙" unfolding "E_Δ'" by simp
  show "source Δ'  sink Δ'" by simp
  show "capacity Δ' e = 0" if "e  EΔ'⇙" for e using that unfolding "E_Δ'"
    by(cases e rule: capacity'.cases)(auto intro: capacity_outside)
  show "capacity Δ' e  " for e by(cases e rule: capacity'.cases)(simp_all add: assms)
qed

private lemma Δ'_flow_attainability:
  assumes "α  "
  shows "flow_attainability Δ'"
proof -
  interpret Δ': countable_network Δ' using assms by(rule Δ'_countable_network)
  show ?thesis
  proof
    show "d_IN (capacity Δ') x    d_OUT (capacity Δ') x  " if sink: "x  sink Δ'" for x
    proof(cases x)
      case (Inner x')
      consider (source) "x' = source Δ" | (IN) "x'  source Δ" "d_IN (capacity Δ) x'  " | (OUT) "d_OUT (capacity Δ) x'  "
        using finite_capacity[of x'] sink Inner by(auto)
      thus ?thesis
      proof(cases)
        case source
        with Inner have "d_IN (capacity Δ') x = (+ y. α * indicator {SOURCE :: 'v node} y)"
          unfolding d_IN_def by(intro nn_integral_cong)(simp split: split_indicator)
        also have " = α" by(simp add: max_def)
        finally show ?thesis using assms by simp
      next
        case IN
        with Inner have "d_IN (capacity Δ') x = (+ yrange Inner. capacity Δ (node.inner y, x'))"
          by(auto simp add: d_IN_def nn_integral_count_space_indicator not_Inner_conv intro!: nn_integral_cong split: split_indicator)
        also have " = d_IN (capacity Δ) x'" unfolding d_IN_def
          by(simp add: nn_integral_count_space_reindex)
        finally show ?thesis using Inner sink IN by(simp)
      next
        case OUT
        from Inner have "d_OUT (capacity Δ') x = (+ yrange Inner. capacity Δ (x', node.inner y))"
          by(auto simp add: d_OUT_def nn_integral_count_space_indicator not_Inner_conv intro!: nn_integral_cong split: split_indicator)
        also have " = d_OUT (capacity Δ) x'" by(simp add: d_OUT_def nn_integral_count_space_reindex)
        finally show ?thesis using OUT by auto
      qed
    qed(simp add: d_IN_def)
    show "¬ edge Δ' x x" for x by(cases x)(simp_all add: no_loop)
    show "¬ edge Δ' x (source Δ')" for x by simp
  qed
qed

private fun lift :: "'v flow  'v node flow"
where
  "lift f (SOURCE, Inner y) = (if y = source Δ then value_flow Δ f else 0)"
| "lift f (Inner x, Inner y) = f (x, y)"
| "lift f _ = 0"

private lemma d_OUT_lift_Inner [simp]: "d_OUT (lift f) (Inner x) = d_OUT f x" (is "?lhs = ?rhs")
proof -
  have "?lhs = (+ yrange Inner. lift f (Inner x, y))"
    by(auto simp add: d_OUT_def nn_integral_count_space_indicator not_Inner_conv intro!: nn_integral_cong split: split_indicator)
  also have " = ?rhs" by(simp add: nn_integral_count_space_reindex d_OUT_def)
  finally show ?thesis .
qed

private lemma d_OUT_lift_SOURCE [simp]: "d_OUT (lift f) SOURCE = value_flow Δ f" (is "?lhs = ?rhs")
proof -
  have "?lhs = (+ y. lift f (SOURCE, y) * indicator {Inner (source Δ)} y)"
    unfolding d_OUT_def by(rule nn_integral_cong)(case_tac x; simp)
  also have " = ?rhs" by(simp add: nn_integral_count_space_indicator max_def)
  finally show ?thesis .
qed

private lemma d_IN_lift_Inner [simp]:
  assumes "x  source Δ"
  shows "d_IN (lift f) (Inner x) = d_IN f x" (is "?lhs = ?rhs")
proof -
  have "?lhs = (+ yrange Inner. lift f (y, Inner x))" using assms
    by(auto simp add: d_IN_def nn_integral_count_space_indicator not_Inner_conv intro!: nn_integral_cong split: split_indicator)
  also have " = ?rhs" by(simp add: nn_integral_count_space_reindex d_IN_def)
  finally show ?thesis .
qed

private lemma d_IN_lift_source [simp]: "d_IN (lift f) (Inner (source Δ)) = value_flow Δ f + d_IN f (source Δ)" (is "?lhs = ?rhs")
proof -
  have "?lhs = (+ y. lift f (y, Inner (source Δ)) * indicator {SOURCE} y) + (+ yrange Inner. lift f (y, Inner (source Δ)))"
    (is "_ = ?SOURCE + ?rest")
    unfolding d_IN_def
    apply(subst nn_integral_count_space_indicator, simp)
    apply(subst nn_integral_add[symmetric])
    apply(auto simp add: AE_count_space max_def not_Inner_conv split: split_indicator intro!: nn_integral_cong)
    done
  also have "?rest = d_IN f (source Δ)" by(simp add: nn_integral_count_space_reindex d_IN_def)
  also have "?SOURCE = value_flow Δ f"
    by(simp add: max_def one_ennreal_def[symmetric] )
  finally show ?thesis .
qed

private lemma flow_lift [simp]:
  assumes "flow Δ f"
  shows "flow Δ' (lift f)"
proof
  show "lift f e  capacity Δ' e" for e
    by(cases e rule: capacity'.cases)(auto intro: flowD_capacity[OF assms] simp add: α_def intro: SUP_upper2 assms)

  fix x
  assume x: "x  source Δ'" "x  sink Δ'"
  then obtain x' where x': "x = Inner x'" by(cases x) auto
  then show "KIR (lift f) x" using x
    by(cases "x' = source Δ")(auto simp add: flowD_source_IN[OF assms] dest: flowD_KIR[OF assms])
qed

private abbreviation (input) unlift :: "'v node flow  'v flow"
where "unlift f  (λ(x, y). f (Inner x, Inner y))"

private lemma flow_unlift [simp]:
  assumes f: "flow Δ' f"
  shows "flow Δ (unlift f)"
proof
  show "unlift f e  capacity Δ e" for e using flowD_capacity[OF f, of "map_prod Inner Inner e"]
    by(cases e)(simp)
next
  fix x
  assume x: "x  source Δ" "x  sink Δ"
  have "d_OUT (unlift f) x = (+ yrange Inner. f (Inner x, y))"
    by(simp add: nn_integral_count_space_reindex d_OUT_def)
  also have " = d_OUT f (Inner x)" using flowD_capacity[OF f, of "(Inner x, SOURCE)"]
    by(auto simp add: nn_integral_count_space_indicator d_OUT_def not_Inner_conv intro!: nn_integral_cong split: split_indicator)
  also have " = d_IN f (Inner x)" using x flowD_KIR[OF f, of "Inner x"] by(simp)
  also have " = (+ yrange Inner. f (y, Inner x))"
    using x flowD_capacity[OF f, of "(SOURCE, Inner x)"]
    by(auto simp add: nn_integral_count_space_indicator d_IN_def not_Inner_conv intro!: nn_integral_cong split: split_indicator)
  also have " = d_IN (unlift f) x" by(simp add: nn_integral_count_space_reindex d_IN_def)
  finally show "KIR (unlift f) x" .
qed

private lemma value_unlift:
  assumes f: "flow Δ' f"
  shows "value_flow Δ (unlift f) = value_flow Δ' f"
proof -
  have "value_flow Δ (unlift f) = (+ yrange Inner. f (Inner (source Δ), y))"
    by(simp add: nn_integral_count_space_reindex d_OUT_def)
  also have " = d_OUT f (Inner (source Δ))" using flowD_capacity[OF f, of "(Inner (source Δ), SOURCE)"]
    by(auto simp add: nn_integral_count_space_indicator d_OUT_def not_Inner_conv intro!: nn_integral_cong split: split_indicator)
  also have " = d_IN f (Inner (source Δ))" using flowD_KIR[OF f, of "Inner (source Δ)"] by(simp)
  also have " = (+ y. f (y, Inner (source Δ)) * indicator {SOURCE} y)"
    unfolding d_IN_def using flowD_capacity[OF f, of "(x, Inner (source Δ))" for x]
    by(intro nn_integral_cong)(auto intro!: antisym split: split_indicator if_split_asm elim: meta_allE)
  also have " = f (SOURCE, Inner (source Δ))" by simp
  also have " = (+ y. f (SOURCE, y) * indicator {Inner (source Δ)} y)"
    by(simp add: one_ennreal_def[symmetric])
  also have " = value_flow Δ' f" unfolding d_OUT_def
    unfolding d_OUT_def using flowD_capacity[OF f, of "(SOURCE, Inner x)" for x] flowD_capacity[OF f, of "(SOURCE, SOURCE)"]
    apply(intro nn_integral_cong)
    apply(case_tac x)
    apply(auto intro!: antisym split: split_indicator if_split_asm elim: meta_allE)
    done
  finally show ?thesis .
qed

theorem ex_max_flow:
  "f. flow Δ f  value_flow Δ f = α  (x. d_IN f x  value_flow Δ f)"
proof(cases "α")
  case (real α')
  hence α: "α  " by simp
  then interpret Δ': flow_attainability Δ' by(rule Δ'_flow_attainability)

  have source_out: "edge Δ' (source Δ') y  y = Inner (source Δ)" for y by(auto)
  have nontrivial: "EΔ' {}" by(auto intro: edge'.intros)

  have eq: "(SUP g  {g. flow Δ' g}. value_flow Δ' g) = (SUP g  {g. flow Δ g}. value_flow Δ g)" (is "?lhs = ?rhs")
  proof(intro antisym SUP_least; unfold mem_Collect_eq)
    fix g
    assume g: "flow Δ' g"
    hence "value_flow Δ' g = value_flow Δ (unlift g)" by(simp add: value_unlift)
    also { from g have "flow Δ (unlift g)" by simp }
    then have "  ?rhs" by(blast intro: SUP_upper2)
    finally show "value_flow Δ' g  " .
  next
    fix g
    assume g: "flow Δ g"
    hence "value_flow Δ g = value_flow Δ' (lift g)" by simp
    also { from g have "flow Δ' (lift g)" by simp }
    then have "  ?lhs" by(blast intro: SUP_upper2)
    finally show "value_flow Δ g  ?lhs" .
  qed
  also have " = ennreal α'" using real by(simp add: α_def)
  finally obtain f where f: "flow Δ' f"
    and value_f: "value_flow Δ' f = (g{g. flow Δ' g}. value_flow Δ' g)"
    and IN_f: "x. d_IN f x  value_flow Δ' f"
    using 0  α' by(blast dest: Δ'.ex_max_flow''[OF source_out nontrivial])
  have "flow Δ (unlift f)" using f by simp
  moreover have "value_flow Δ (unlift f) = α" using f eq value_f by(simp add: value_unlift α_def)
  moreover {
    fix x
    have "d_IN (unlift f) x = (+ yrange Inner. f (y, Inner x))"
      by(simp add: nn_integral_count_space_reindex d_IN_def)
    also have "  d_IN f (Inner x)" unfolding d_IN_def
      by(auto intro!: nn_integral_mono simp add: nn_integral_count_space_indicator split: split_indicator)
    also have "  value_flow Δ (unlift f)" using IN_f[of "Inner x"] f by(simp add: value_unlift)
    also note calculation }
  ultimately show ?thesis by blast
next
  case top
  show ?thesis
  proof(cases "f. flow Δ f  value_flow Δ f = ")
    case True
    with top show ?thesis by auto
  next
    case False
    hence real: "f. α =   flow Δ f  value_flow Δ f < α" using top by (auto simp: less_top)
    { fix i
      have "2 * 2 ^ i < α" using top by (simp_all add: ennreal_mult_less_top power_less_top_ennreal)
      from flow_by_value[OF this real] have "f. flow Δ f  value_flow Δ f = 2 * 2 ^ i" by blast }
    then obtain f_i where f_i: "i. flow Δ (f_i i)"
      and value_i: "i. value_flow Δ (f_i i) = 2 * 2 ^ i" by metis
    define f where "f e = (+ i. f_i i e / (2 * 2 ^ i))" for e
    have "flow Δ f"
    proof
      fix e
      have "f e  (+ i. (SUP i. f_i i e) / (2 * 2 ^ i))" unfolding f_def
        by(rule nn_integral_mono)(auto intro!: divide_right_mono_ennreal SUP_upper)
      also have " = (SUP i. f_i i e) / 2 * (+ i. 1 / 2 ^ i)"
        apply(subst nn_integral_cmult[symmetric])
        apply(auto intro!: nn_integral_cong intro: SUP_upper2
          simp: divide_ennreal_def ennreal_inverse_mult power_less_top_ennreal mult_ac)
        done
      also have "(+ i. 1 / 2 ^ i) = (i. ennreal ((1 / 2) ^ i))"
        by(simp add: nn_integral_count_space_nat power_divide divide_ennreal[symmetric] ennreal_power[symmetric])
      also have " = ennreal (i. (1 / 2) ^ i)"
        by(intro suminf_ennreal2 complete_algebra_summable_geometric) simp_all
      also have " = 2" by(subst suminf_geometric; simp)
      also have "(SUP i. f_i i e) / 2 * 2 = (SUP i. f_i i e)"
        by (simp add: ennreal_divide_times)
      also have "  capacity Δ e" by(rule SUP_least)(rule flowD_capacity[OF f_i])
      finally show "f e  capacity Δ e" .

      fix x
      assume x: "x  source Δ" "x  sink Δ"
      have "d_OUT f x = (+ iUNIV. + y. f_i i (x, y) / (2 * 2 ^ i))"
        unfolding d_OUT_def f_def
        by(subst nn_integral_snd_count_space[where f="case_prod _", simplified])
          (simp add: nn_integral_fst_count_space[where f="case_prod _", simplified])
      also have " = (+ i. d_OUT (f_i i) x / (2 * 2 ^ i))" unfolding d_OUT_def
        by(simp add: nn_integral_divide)
      also have " = (+ i. d_IN (f_i i) x / (2 * 2 ^ i))" by(simp add: flowD_KIR[OF f_i, OF x])
      also have " = (+ iUNIV. + y. f_i i (y, x) / (2 * 2 ^ i))"
        by(simp add: nn_integral_divide d_IN_def)
      also have " = d_IN f x" unfolding d_IN_def f_def
        by(subst nn_integral_snd_count_space[where f="case_prod _", simplified])
          (simp add: nn_integral_fst_count_space[where f="case_prod _", simplified])
      finally show "KIR f x" .
    qed
    moreover {
      have "value_flow Δ f = (+ i. value_flow Δ (f_i i) / (2 * 2 ^ i))"
        unfolding d_OUT_def f_def
        by(subst nn_integral_snd_count_space[where f="case_prod _", simplified])
          (simp add: nn_integral_fst_count_space[where f="case_prod _", simplified] nn_integral_divide[symmetric])
      also have " = "
        by(simp add: value_i ennreal_mult_less_top power_less_top_ennreal)
      finally have "value_flow Δ f = " .
    }
    ultimately show ?thesis using top by auto
  qed
qed

end

end

end

end