Theory MFMC_Unbounded
section ‹The max-flow min-cut theorems in unbounded networks›
theory MFMC_Unbounded imports
MFMC_Web
MFMC_Flow_Attainability
MFMC_Reduction
begin
subsection ‹More about waves›
lemma SINK_plus_current: "SINK (plus_current f g) = SINK f ∩ SINK g"
by(auto simp add: SINK.simps set_eq_iff d_OUT_def nn_integral_0_iff emeasure_count_space_eq_0 add_eq_0_iff_both_eq_0)
abbreviation plus_web :: "('v, 'more) web_scheme ⇒ 'v current ⇒ 'v current ⇒ 'v current" (‹_ ⌢ı _› [66, 66] 65)
where "plus_web Γ f g ≡ plus_current f (g ↿ Γ / f)"
lemma d_OUT_plus_web:
fixes Γ (structure)
shows "d_OUT (f ⌢ g) x = d_OUT f x + d_OUT (g ↿ Γ / f) x" (is "?lhs = ?rhs")
proof -
have "?lhs = d_OUT f x + (∑⇧+ y. (if x ∈ RF⇧∘ (TER f) then 0 else g (x, y) * indicator (- RF (TER f)) y))"
unfolding d_OUT_def by(subst nn_integral_add[symmetric])(auto intro!: nn_integral_cong split: split_indicator)
also have "… = ?rhs" by(auto simp add: d_OUT_def intro!: arg_cong2[where f="(+)"] nn_integral_cong)
finally show "?thesis" .
qed
lemma d_IN_plus_web:
fixes Γ (structure)
shows "d_IN (f ⌢ g) y = d_IN f y + d_IN (g ↿ Γ / f) y" (is "?lhs = ?rhs")
proof -
have "?lhs = d_IN f y + (∑⇧+ x. (if y ∈ RF (TER f) then 0 else g (x, y) * indicator (- RF⇧∘ (TER f)) x))"
unfolding d_IN_def by(subst nn_integral_add[symmetric])(auto intro!: nn_integral_cong split: split_indicator)
also have "… = ?rhs" by(auto simp add: d_IN_def intro!: arg_cong2[where f="(+)"] nn_integral_cong)
finally show ?thesis .
qed
lemma plus_web_greater: "f e ≤ (f ⌢⇘Γ⇙ g) e"
by(cases e)(auto split: split_indicator)
lemma current_plus_web:
fixes Γ (structure)
shows "⟦ current Γ f; wave Γ f; current Γ g ⟧ ⟹ current Γ (f ⌢ g)"
by(blast intro: current_plus_current current_restrict_current)
context
fixes Γ :: "('v, 'more) web_scheme" (structure)
and f g :: "'v current"
assumes f: "current Γ f"
and w: "wave Γ f"
and g: "current Γ g"
begin
context
fixes x :: "'v"
assumes x: "x ∈ ℰ (TER f ∪ TER g)"
begin
qualified lemma RF_f: "x ∉ RF⇧∘ (TER f)"
proof
assume *: "x ∈ RF⇧∘ (TER f)"
from x obtain p y where p: "path Γ x p y" and y: "y ∈ B Γ"
and bypass: "⋀z. ⟦x ≠ y; z ∈ set p⟧ ⟹ z = x ∨ z ∉ TER f ∪ TER g" by(rule ℰ_E) blast
from rtrancl_path_distinct[OF p] obtain p'
where p: "path Γ x p' y" and p': "set p' ⊆ set p" and distinct: "distinct (x # p')" .
from * have x': "x ∈ RF (TER f)" and ℰ: "x ∉ ℰ (TER f)" by(auto simp add: roofed_circ_def)
hence "x ∉ TER f" using not_essentialD[OF _ p y] p' bypass by blast
with roofedD[OF x' p y] obtain z where z: "z ∈ set p'" "z ∈ TER f" by auto
with p have "y ∈ set p'" by(auto dest!: rtrancl_path_last intro: last_in_set)
with distinct have "x ≠ y" by auto
with bypass z p' distinct show False by auto
qed
private lemma RF_g: "x ∉ RF⇧∘ (TER g)"
proof
assume *: "x ∈ RF⇧∘ (TER g)"
from x obtain p y where p: "path Γ x p y" and y: "y ∈ B Γ"
and bypass: "⋀z. ⟦x ≠ y; z ∈ set p⟧ ⟹ z = x ∨ z ∉ TER f ∪ TER g" by(rule ℰ_E) blast
from rtrancl_path_distinct[OF p] obtain p'
where p: "path Γ x p' y" and p': "set p' ⊆ set p" and distinct: "distinct (x # p')" .
from * have x': "x ∈ RF (TER g)" and ℰ: "x ∉ ℰ (TER g)" by(auto simp add: roofed_circ_def)
hence "x ∉ TER g" using not_essentialD[OF _ p y] p' bypass by blast
with roofedD[OF x' p y] obtain z where z: "z ∈ set p'" "z ∈ TER g" by auto
with p have "y ∈ set p'" by(auto dest!: rtrancl_path_last intro: last_in_set)
with distinct have "x ≠ y" by auto
with bypass z p' distinct show False by auto
qed
lemma TER_plus_web_aux:
assumes SINK: "x ∈ SINK (g ↿ Γ / f)" (is "_ ∈ SINK ?g")
shows "x ∈ TER (f ⌢ g)"
proof
from x obtain p y where p: "path Γ x p y" and y: "y ∈ B Γ"
and bypass: "⋀z. ⟦x ≠ y; z ∈ set p⟧ ⟹ z = x ∨ z ∉ TER f ∪ TER g" by(rule ℰ_E) blast
from rtrancl_path_distinct[OF p] obtain p'
where p: "path Γ x p' y" and p': "set p' ⊆ set p" and distinct: "distinct (x # p')" .
from RF_f have "x ∈ SINK f"
by(auto simp add: roofed_circ_def SINK.simps dest: waveD_OUT[OF w])
thus "x ∈ SINK (f ⌢ g)" using SINK
by(simp add: SINK.simps d_OUT_plus_web)
show "x ∈ SAT Γ (f ⌢ g)"
proof(cases "x ∈ TER f")
case True
hence "x ∈ SAT Γ f" by simp
moreover have "… ⊆ SAT Γ (f ⌢ g)" by(rule SAT_mono plus_web_greater)+
ultimately show ?thesis by blast
next
case False
with x have "x ∈ TER g" by auto
from False RF_f have "x ∉ RF (TER f)" by(auto simp add: roofed_circ_def)
moreover { fix z
assume z: "z ∈ RF⇧∘ (TER f)"
have "(z, x) ∉ ❙E"
proof
assume "(z, x) ∈ ❙E"
hence path': "path Γ z (x # p') y" using p by(simp add: rtrancl_path.step)
from z have "z ∈ RF (TER f)" by(simp add: roofed_circ_def)
from roofedD[OF this path' y] False
consider (path) z' where "z' ∈ set p'" "z' ∈ TER f" | (TER) "z ∈ TER f" by auto
then show False
proof cases
{ case (path z')
with p distinct have "x ≠ y"
by(auto 4 3 intro: last_in_set elim: rtrancl_path.cases dest: rtrancl_path_last[symmetric])
from bypass[OF this, of z'] path False p' show False by auto }
note that = this
case TER
with z have "¬ essential Γ (B Γ) (TER f) z" by(simp add: roofed_circ_def)
from not_essentialD[OF this path' y] False obtain z' where "z' ∈ set p'" "z' ∈ TER f" by auto
thus False by(rule that)
qed
qed }
ultimately have "d_IN ?g x = d_IN g x" unfolding d_IN_def
by(intro nn_integral_cong)(clarsimp split: split_indicator simp add: currentD_outside[OF g])
hence "d_IN (f ⌢ g) x ≥ d_IN g x"
by(simp add: d_IN_plus_web)
with ‹x ∈ TER g› show ?thesis by(auto elim!: SAT.cases intro: SAT.intros)
qed
qed
qualified lemma SINK_TER_in'':
assumes "⋀x. x ∉ RF (TER g) ⟹ d_OUT g x = 0"
shows "x ∈ SINK g"
using RF_g by(auto simp add: roofed_circ_def SINK.simps assms)
end
lemma wave_plus: "wave (quotient_web Γ f) (g ↿ Γ / f) ⟹ wave Γ (f ⌢ g)"
using f w by(rule wave_plus_current)(rule current_restrict_current[OF w g])
lemma TER_plus_web'':
assumes "⋀x. x ∉ RF (TER g) ⟹ d_OUT g x = 0"
shows "ℰ (TER f ∪ TER g) ⊆ TER (f ⌢ g)"
proof
fix x
assume *: "x ∈ ℰ (TER f ∪ TER g)"
moreover have "x ∈ SINK (g ↿ Γ / f)"
by(rule in_SINK_restrict_current)(rule MFMC_Unbounded.SINK_TER_in''[OF f w g * assms])
ultimately show "x ∈ TER (f ⌢ g)" by(rule TER_plus_web_aux)
qed
lemma TER_plus_web': "wave Γ g ⟹ ℰ (TER f ∪ TER g) ⊆ TER (f ⌢ g)"
by(rule TER_plus_web'')(rule waveD_OUT)
lemma wave_plus': "wave Γ g ⟹ wave Γ (f ⌢ g)"
by(rule wave_plus)(rule wave_restrict_current[OF f w g])
end
lemma RF_TER_plus_web:
fixes Γ (structure)
assumes f: "current Γ f"
and w: "wave Γ f"
and g: "current Γ g"
and w': "wave Γ g"
shows "RF (TER (f ⌢ g)) = RF (TER f ∪ TER g)"
proof
have "RF (ℰ (TER f ∪ TER g)) ⊆ RF (TER (f ⌢ g))"
by(rule roofed_mono)(rule TER_plus_web'[OF f w g w'])
also have "RF (ℰ (TER f ∪ TER g)) = RF (TER f ∪ TER g)" by(rule RF_essential)
finally show "… ⊆ RF (TER (f ⌢ g))" .
next
have fg: "current Γ (f ⌢ g)" using f w g by(rule current_plus_web)
show "RF (TER (f ⌢ g)) ⊆ RF (TER f ∪ TER g)"
proof(intro subsetI roofedI)
fix x p y
assume RF: "x ∈ RF (TER (f ⌢ g))" and p: "path Γ x p y" and y: "y ∈ B Γ"
from roofedD[OF RF p y] obtain z where z: "z ∈ set (x # p)" and TER: "z ∈ TER (f ⌢ g)" by auto
from TER have SINK: "z ∈ SINK f"
by(auto simp add: SINK.simps d_OUT_plus_web add_eq_0_iff_both_eq_0)
from TER have "z ∈ SAT Γ (f ⌢ g)" by simp
hence SAT: "z ∈ SAT Γ f ∪ SAT Γ g"
by(cases "z ∈ RF (TER f)")(auto simp add: currentD_SAT[OF f] currentD_SAT[OF g] currentD_SAT[OF fg] d_IN_plus_web d_IN_restrict_current_outside restrict_current_IN_not_RF[OF g] wave_not_RF_IN_zero[OF f w])
show "(∃z∈set p. z ∈ TER f ∪ TER g) ∨ x ∈ TER f ∪ TER g"
proof(cases "z ∈ RF (TER g)")
case False
hence "z ∈ SINK g" by(simp add: SINK.simps waveD_OUT[OF w'])
with SINK SAT have "z ∈ TER f ∪ TER g" by auto
thus ?thesis using z by auto
next
case True
from split_list[OF z] obtain ys zs where split: "x # p = ys @ z # zs" by blast
with p have "path Γ z zs y" by(auto elim: rtrancl_path_appendE simp add: Cons_eq_append_conv)
from roofedD[OF True this y] split show ?thesis by(auto simp add: Cons_eq_append_conv)
qed
qed
qed
lemma RF_TER_Sup:
fixes Γ (structure)
assumes f: "⋀f. f ∈ Y ⟹ current Γ f"
and w: "⋀f. f ∈ Y ⟹ wave Γ f"
and Y: "Complete_Partial_Order.chain (≤) Y" "Y ≠ {}" "countable (support_flow (Sup Y))"
shows "RF (TER (Sup Y)) = RF (⋃f∈Y. TER f)"
proof(rule set_eqI iffI)+
fix x
assume x: "x ∈ RF (TER (Sup Y))"
have "x ∈ RF (RF (⋃f∈Y. TER f))"
proof
fix p y
assume p: "path Γ x p y" and y: "y ∈ B Γ"
from roofedD[OF x p y] obtain z where z: "z ∈ set (x # p)" and TER: "z ∈ TER (Sup Y)" by auto
from TER have SINK: "z ∈ SINK f" if "f ∈ Y" for f using that by(auto simp add: SINK_Sup[OF Y])
from Y(2) obtain f where y: "f ∈ Y" by blast
show "(∃z∈set p. z ∈ RF (⋃f∈Y. TER f)) ∨ x ∈ RF (⋃f∈Y. TER f)"
proof(cases "∃f∈Y. z ∈ RF (TER f)")
case True
then obtain f where fY: "f ∈ Y" and zf: "z ∈ RF (TER f)" by blast
from zf have "z ∈ RF (⋃f∈Y. TER f)" by(rule in_roofed_mono)(auto intro: fY)
with z show ?thesis by auto
next
case False
hence *: "d_IN f z = 0" if "f ∈ Y" for f using that by(auto intro: wave_not_RF_IN_zero[OF f w])
hence "d_IN (Sup Y) z = 0" using Y(2) by(simp add: d_IN_Sup[OF Y])
with TER have "z ∈ SAT Γ f" using *[OF y]
by(simp add: SAT.simps)
with SINK[OF y] have "z ∈ TER f" by simp
with z y show ?thesis by(auto intro: roofed_greaterI)
qed
qed
then show "x ∈ RF (⋃f∈Y. TER f)" unfolding roofed_idem .
next
fix x
assume x: "x ∈ RF (⋃f∈Y. TER f)"
have "x ∈ RF (RF (TER (⨆Y)))"
proof(rule roofedI)
fix p y
assume p: "path Γ x p y" and y: "y ∈ B Γ"
from roofedD[OF x p y] obtain z f where *: "z ∈ set (x # p)"
and **: "f ∈ Y" and TER: "z ∈ TER f" by auto
have "z ∈ RF (TER (Sup Y))"
proof(rule ccontr)
assume z: "z ∉ RF (TER (Sup Y))"
have "wave Γ (Sup Y)" using Y(1-2) w Y(3) by(rule wave_lub)
hence "d_OUT (Sup Y) z = 0" using z by(rule waveD_OUT)
hence "z ∈ SINK (Sup Y)" by(simp add: SINK.simps)
moreover have "z ∈ SAT Γ (Sup Y)" using TER SAT_Sup_upper[OF **, of Γ] by blast
ultimately have "z ∈ TER (Sup Y)" by simp
hence "z ∈ RF (TER (Sup Y))" by(rule roofed_greaterI)
with z show False by contradiction
qed
thus "(∃z∈set p. z ∈ RF (TER (Sup Y))) ∨ x ∈ RF (TER (Sup Y))" using * by auto
qed
then show "x ∈ RF (TER (⨆Y))" unfolding roofed_idem .
qed
subsection ‹Hindered webs with reduced weights›
context countable_bipartite_web begin
context
fixes u :: "'v ⇒ ennreal"
and ε
defines "ε ≡ (∫⇧+ y. u y ∂count_space (B Γ))"
assumes u_outside: "⋀x. x ∉ B Γ ⟹ u x = 0"
and finite_ε: "ε ≠ ⊤"
begin
private lemma u_A: "x ∈ A Γ ⟹ u x = 0"
using u_outside[of x] disjoint by auto
private lemma u_finite: "u y ≠ ⊤"
proof(cases "y ∈ B Γ")
case True
have "u y ≤ ε" unfolding ε_def by(rule nn_integral_ge_point)(simp add: True)
also have "… < ⊤" using finite_ε by (simp add: less_top[symmetric])
finally show ?thesis by simp
qed(simp add: u_outside)
lemma hindered_reduce:
assumes u: "u ≤ weight Γ"
assumes hindered_by: "hindered_by (Γ⦇weight := weight Γ - u⦈) ε" (is "hindered_by ?Γ _")
shows "hindered Γ"
proof -
note [simp] = u_finite
let ?TER = "TER⇘?Γ⇙"
from hindered_by obtain f
where hindrance_by: "hindrance_by ?Γ f ε"
and f: "current ?Γ f"
and w: "wave ?Γ f" by cases
from hindrance_by obtain a where a: "a ∈ A Γ" "a ∉ ℰ⇘?Γ⇙ (?TER f)"
and a_le: "d_OUT f a < weight Γ a"
and ε_less: "weight Γ a - d_OUT f a > ε"
and ε_nonneg: "ε ≥ 0" by(auto simp add: u_A hindrance_by.simps)
from f have f': "current Γ f" by(rule current_weight_mono)(auto intro: diff_le_self_ennreal)
write Some (‹⟨_⟩›)
define edge'
where "edge' xo yo =
(case (xo, yo) of
(None, Some y) ⇒ y ∈ ❙V ∧ y ∉ A Γ
| (Some x, Some y) ⇒ edge Γ x y ∨ edge Γ y x
| _ ⇒ False)" for xo yo
define cap
where "cap e =
(case e of
(None, Some y) ⇒ if y ∈ ❙V then u y else 0
| (Some x, Some y) ⇒ if edge Γ x y ∧ x ≠ a then f (x, y) else if edge Γ y x then max (weight Γ x) (weight Γ y) + 1 else 0
| _ ⇒ 0)" for e
define Ψ where "Ψ = ⦇edge = edge', capacity = cap, source = None, sink = Some a⦈"
have edge'_simps [simp]:
"edge' None ⟨y⟩ ⟷ y ∈ ❙V ∧ y ∉ A Γ"
"edge' xo None ⟷ False"
"edge' ⟨x⟩ ⟨y⟩ ⟷ edge Γ x y ∨ edge Γ y x"
for xo x y by(simp_all add: edge'_def split: option.split)
have edge_None1E [elim!]: thesis if "edge' None y" "⋀z. ⟦ y = ⟨z⟩; z ∈ ❙V; z ∉ A Γ ⟧ ⟹ thesis" for y thesis
using that by(simp add: edge'_def split: option.split_asm sum.split_asm)
have edge_Some1E [elim!]: thesis if "edge' ⟨x⟩ y" "⋀z. ⟦ y = ⟨z⟩; edge Γ x z ∨ edge Γ z x ⟧ ⟹ thesis" for x y thesis
using that by(simp add: edge'_def split: option.split_asm sum.split_asm)
have edge_Some2E [elim!]: thesis if "edge' x ⟨y⟩" "⟦ x = None; y ∈ ❙V; y ∉ A Γ ⟧ ⟹ thesis" "⋀z. ⟦ x = ⟨z⟩; edge Γ z y ∨ edge Γ y z ⟧ ⟹ thesis" for x y thesis
using that by(simp add: edge'_def split: option.split_asm sum.split_asm)
have cap_simps [simp]:
"cap (None, ⟨y⟩) = (if y ∈ ❙V then u y else 0)"
"cap (xo, None) = 0"
"cap (⟨x⟩, ⟨y⟩) =
(if edge Γ x y ∧ x ≠ a then f (x, y) else if edge Γ y x then max (weight Γ x) (weight Γ y) + 1 else 0)"
for xo x y by(simp_all add: cap_def split: option.split)
have Ψ_sel [simp]:
"edge Ψ = edge'"
"capacity Ψ = cap"
"source Ψ = None"
"sink Ψ = ⟨a⟩"
by(simp_all add: Ψ_def)
have cap_outside1: "¬ vertex Γ x ⟹ cap (⟨x⟩, y) = 0" for x y
by(cases y)(auto simp add: vertex_def)
have capacity_A_weight: "d_OUT cap ⟨x⟩ ≤ weight Γ x" if "x ∈ A Γ" for x
proof -
have "d_OUT cap ⟨x⟩ ≤ (∑⇧+ y∈range Some. f (x, the y))"
using that disjoint a(1) unfolding d_OUT_def
by(auto 4 4 intro!: nn_integral_mono simp add: nn_integral_count_space_indicator notin_range_Some currentD_outside[OF f] split: split_indicator dest: edge_antiparallel bipartite_E)
also have "… = d_OUT f x" by(simp add: d_OUT_def nn_integral_count_space_reindex)
also have "… ≤ weight Γ x" using f' by(rule currentD_weight_OUT)
finally show ?thesis .
qed
have flow_attainability: "flow_attainability Ψ"
proof
have "❙E⇘Ψ⇙ = (λ(x, y). (⟨x⟩, ⟨y⟩)) ` ❙E ∪ (λ(x, y). (⟨y⟩, ⟨x⟩)) ` ❙E ∪ (λx. (None, ⟨x⟩)) ` (❙V ∩ - A Γ)"
by(auto simp add: edge'_def split: option.split_asm)
thus "countable ❙E⇘Ψ⇙" by simp
next
fix v
assume "v ≠ sink Ψ"
consider (sink) "v = None" | (A) x where "v = ⟨x⟩" "x ∈ A Γ"
| (B) y where "v = ⟨y⟩" "y ∉ A Γ" "y ∈ ❙V" | (outside) x where "v = ⟨x⟩" "x ∉ ❙V"
by(cases v) auto
then show "d_IN (capacity Ψ) v ≠ ⊤ ∨ d_OUT (capacity Ψ) v ≠ ⊤"
proof cases
case sink thus ?thesis by(simp add: d_IN_def)
next
case (A x)
thus ?thesis using capacity_A_weight[of x] by (auto simp: top_unique)
next
case (B y)
have "d_IN (capacity Ψ) v ≤ (∑⇧+ x. f (the x, y) * indicator (range Some) x + u y * indicator {None} x)"
using B disjoint bipartite_V a(1) unfolding d_IN_def
by(auto 4 4 intro!: nn_integral_mono simp add: nn_integral_count_space_indicator notin_range_Some currentD_outside[OF f] split: split_indicator dest: edge_antiparallel bipartite_E)
also have "… = (∑⇧+ x∈range Some. f (the x, y)) + u y"
by(subst nn_integral_add)(simp_all add: nn_integral_count_space_indicator)
also have "… = d_IN f y + u y" by(simp add: d_IN_def nn_integral_count_space_reindex)
also have "d_IN f y ≤ weight Γ y" using f' by(rule currentD_weight_IN)
finally show ?thesis by(auto simp add: add_right_mono top_unique split: if_split_asm)
next
case outside
hence "d_OUT (capacity Ψ) v = 0"
by(auto simp add: d_OUT_def nn_integral_0_iff_AE AE_count_space cap_def vertex_def split: option.split)
thus ?thesis by simp
qed
next
show "capacity Ψ e ≠ ⊤" for e using weight_finite
by(auto simp add: cap_def max_def vertex_def currentD_finite[OF f'] split: option.split prod.split simp del: weight_finite)
show "capacity Ψ e = 0" if "e ∉ ❙E⇘Ψ⇙" for e
using that bipartite_V disjoint
by(auto simp add: cap_def max_def intro: u_outside split: option.split prod.split)
show "¬ edge Ψ x (source Ψ)" for x by simp
show "¬ edge Ψ x x" for x by(cases x)(simp_all add: no_loop)
show "source Ψ ≠ sink Ψ" by simp
qed
then interpret Ψ: flow_attainability "Ψ" .
define α where "α = (⨆g∈{g. flow Ψ g}. value_flow Ψ g)"
have α_le: "α ≤ ε"
proof -
have "α ≤ d_OUT cap None" unfolding α_def by(rule SUP_least)(auto intro!: d_OUT_mono dest: flowD_capacity)
also have "… ≤ ∫⇧+ y. cap (None, y) ∂count_space (range Some)" unfolding d_OUT_def
by(auto simp add: nn_integral_count_space_indicator notin_range_Some intro!: nn_integral_mono split: split_indicator)
also have "… ≤ ε" unfolding ε_def
by (subst (2) nn_integral_count_space_indicator, auto simp add: nn_integral_count_space_reindex u_outside intro!: nn_integral_mono split: split_indicator)
finally show ?thesis by simp
qed
then have finite_flow: "α ≠ ⊤" using finite_ε by (auto simp: top_unique)
from Ψ.ex_max_flow
obtain j where j: "flow Ψ j"
and value_j: "value_flow Ψ j = α"
and IN_j: "⋀x. d_IN j x ≤ α"
unfolding α_def by auto
have j_le_f: "j (Some x, Some y) ≤ f (x, y)" if "edge Γ x y" for x y
using that flowD_capacity[OF j, of "(Some x, Some y)"] a(1) disjoint
by(auto split: if_split_asm dest: bipartite_E intro: order_trans)
have IN_j_finite [simp]: "d_IN j x ≠ ⊤" for x using finite_flow by(rule neq_top_trans)(simp add: IN_j)
have j_finite[simp]: "j (x, y) < ⊤" for x y
by (rule le_less_trans[OF d_IN_ge_point]) (simp add: IN_j_finite[of y] less_top[symmetric])
have OUT_j_finite: "d_OUT j x ≠ ⊤" for x
proof(cases "x = source Ψ ∨ x = sink Ψ")
case True thus ?thesis
proof cases
case left thus ?thesis using finite_flow value_j by simp
next
case right
have "d_OUT (capacity Ψ) ⟨a⟩ ≠ ⊤" using capacity_A_weight[of a] a(1) by(auto simp: top_unique)
thus ?thesis unfolding right[simplified]
by(rule neq_top_trans)(rule d_OUT_mono flowD_capacity[OF j])+
qed
next
case False then show ?thesis by(simp add: flowD_KIR[OF j])
qed
have IN_j_le_weight: "d_IN j ⟨x⟩ ≤ weight Γ x" for x
proof(cases "x ∈ A Γ")
case xA: True
show ?thesis
proof(cases "x = a")
case True
have "d_IN j ⟨x⟩ ≤ α" by(rule IN_j)
also have "… ≤ ε" by(rule α_le)
also have "ε < weight Γ a" using ε_less diff_le_self_ennreal less_le_trans by blast
finally show ?thesis using True by(auto intro: order.strict_implies_order)
next
case False
have "d_IN j ⟨x⟩ = d_OUT j ⟨x⟩" using flowD_KIR[OF j, of "Some x"] False by simp
also have "… ≤ d_OUT cap ⟨x⟩" using flowD_capacity[OF j] by(auto intro: d_OUT_mono)
also have "… ≤ weight Γ x" using xA by(rule capacity_A_weight)
finally show ?thesis .
qed
next
case xA: False
show ?thesis
proof(cases "x ∈ B Γ")
case True
have "d_IN j ⟨x⟩ ≤ d_IN cap ⟨x⟩" using flowD_capacity[OF j] by(auto intro: d_IN_mono)
also have "… ≤ (∑⇧+ z. f (the z, x) * indicator (range Some) z) + (∑⇧+ z :: 'v option. u x * indicator {None} z)"
using True disjoint
by(subst nn_integral_add[symmetric])(auto simp add: vertex_def currentD_outside[OF f] d_IN_def B_out intro!: nn_integral_mono split: split_indicator)
also have "… = d_IN f x + u x"
by(simp add: nn_integral_count_space_indicator[symmetric] nn_integral_count_space_reindex d_IN_def)
also have "… ≤ weight Γ x" using currentD_weight_IN[OF f, of x] u_finite[of x]
using ε_less u by (auto simp add: ennreal_le_minus_iff le_fun_def)
finally show ?thesis .
next
case False
with xA have "x ∉ ❙V" using bipartite_V by blast
then have "d_IN j ⟨x⟩ = 0" using False
by(auto simp add: d_IN_def nn_integral_0_iff emeasure_count_space_eq_0 vertex_def edge'_def split: option.split_asm intro!: Ψ.flowD_outside[OF j])
then show ?thesis
by simp
qed
qed
let ?j = "j ∘ map_prod Some Some ∘ prod.swap"
have finite_j_OUT: "(∑⇧+ y∈❙O❙U❙T x. j (⟨x⟩, ⟨y⟩)) ≠ ⊤" (is "?j_OUT ≠ _") if "x ∈ A Γ" for x
using currentD_finite_OUT[OF f', of x]
by(rule neq_top_trans)(auto intro!: nn_integral_mono j_le_f simp add: d_OUT_def nn_integral_count_space_indicator outgoing_def split: split_indicator)
have j_OUT_eq: "?j_OUT x = d_OUT j ⟨x⟩" if "x ∈ A Γ" for x
proof -
have "?j_OUT x = (∑⇧+ y∈range Some. j (Some x, y))" using that disjoint
by(simp add: nn_integral_count_space_reindex)(auto 4 4 simp add: nn_integral_count_space_indicator outgoing_def intro!: nn_integral_cong Ψ.flowD_outside[OF j] dest: bipartite_E split: split_indicator)
also have "… = d_OUT j ⟨x⟩"
by(auto simp add: d_OUT_def nn_integral_count_space_indicator notin_range_Some intro!: nn_integral_cong Ψ.flowD_outside[OF j] split: split_indicator)
finally show ?thesis .
qed
define g where "g = f ⊕ ?j"
have g_simps: "g (x, y) = (f ⊕ ?j) (x, y)" for x y by(simp add: g_def)
have OUT_g_A: "d_OUT g x = d_OUT f x + d_IN j ⟨x⟩ - d_OUT j ⟨x⟩" if "x ∈ A Γ" for x
proof -
have "d_OUT g x = (∑⇧+ y∈❙O❙U❙T x. f (x, y) + j (⟨y⟩, ⟨x⟩) - j (⟨x⟩, ⟨y⟩))"
by(auto simp add: d_OUT_def g_simps currentD_outside[OF f'] outgoing_def nn_integral_count_space_indicator intro!: nn_integral_cong)
also have "… = (∑⇧+ y∈❙O❙U❙T x. f (x, y) + j (⟨y⟩, ⟨x⟩)) - (∑⇧+ y∈❙O❙U❙T x. j (⟨x⟩, ⟨y⟩))"
(is "_ = _ - ?j_OUT") using finite_j_OUT[OF that]
by(subst nn_integral_diff)(auto simp add: AE_count_space outgoing_def intro!: order_trans[OF j_le_f])
also have "… = (∑⇧+ y∈❙O❙U❙T x. f (x, y)) + (∑⇧+ y∈❙O❙U❙T x. j (Some y, Some x)) - ?j_OUT"
(is "_ = ?f + ?j_IN - _") by(subst nn_integral_add) simp_all
also have "?f = d_OUT f x" by(subst d_OUT_alt_def[where G=Γ])(simp_all add: currentD_outside[OF f])
also have "?j_OUT = d_OUT j ⟨x⟩" using that by(rule j_OUT_eq)
also have "?j_IN = (∑⇧+ y∈range Some. j (y, ⟨x⟩))" using that disjoint
by(simp add: nn_integral_count_space_reindex)(auto 4 4 simp add: nn_integral_count_space_indicator outgoing_def intro!: nn_integral_cong Ψ.flowD_outside[OF j] split: split_indicator dest: bipartite_E)
also have "… = d_IN j (Some x)" using that disjoint
by(auto 4 3 simp add: d_IN_def nn_integral_count_space_indicator notin_range_Some intro!: nn_integral_cong Ψ.flowD_outside[OF j] split: split_indicator)
finally show ?thesis by simp
qed
have OUT_g_B: "d_OUT g x = 0" if "x ∉ A Γ" for x
using disjoint that
by(auto simp add: d_OUT_def nn_integral_0_iff_AE AE_count_space g_simps dest: bipartite_E)
have OUT_g_a: "d_OUT g a < weight Γ a" using a(1)
proof -
have "d_OUT g a = d_OUT f a + d_IN j ⟨a⟩ - d_OUT j ⟨a⟩" using a(1) by(rule OUT_g_A)
also have "… ≤ d_OUT f a + d_IN j ⟨a⟩"
by(rule diff_le_self_ennreal)
also have "… < weight Γ a + d_IN j ⟨a⟩ - ε"
using finite_ε ε_less currentD_finite_OUT[OF f']
by (simp add: less_diff_eq_ennreal less_top ac_simps)
also have "… ≤ weight Γ a"
using IN_j[THEN order_trans, OF α_le] by (simp add: ennreal_minus_le_iff)
finally show ?thesis .
qed
have OUT_jj: "d_OUT ?j x = d_IN j ⟨x⟩ - j (None, ⟨x⟩)" for x
proof -
have "d_OUT ?j x = (∑⇧+ y∈range Some. j (y, ⟨x⟩))" by(simp add: d_OUT_def nn_integral_count_space_reindex)
also have "… = d_IN j ⟨x⟩ - (∑⇧+ y. j (y, ⟨x⟩) * indicator {None} y)" unfolding d_IN_def
by(subst nn_integral_diff[symmetric])(auto simp add: max_def Ψ.flowD_finite[OF j] AE_count_space nn_integral_count_space_indicator split: split_indicator intro!: nn_integral_cong)
also have "… = d_IN j ⟨x⟩ - j (None, ⟨x⟩)" by(simp add: max_def)
finally show ?thesis .
qed
have OUT_jj_finite [simp]: "d_OUT ?j x ≠ ⊤" for x
by(simp add: OUT_jj)
have IN_g: "d_IN g x = d_IN f x + j (None, ⟨x⟩)" for x
proof(cases "x ∈ B Γ")
case True
have finite: "(∑⇧+ y∈❙I❙N x. j (Some y, Some x)) ≠ ⊤" using currentD_finite_IN[OF f', of x]
by(rule neq_top_trans)(auto intro!: nn_integral_mono j_le_f simp add: d_IN_def nn_integral_count_space_indicator incoming_def split: split_indicator)
have "d_IN g x = d_IN (f ⊕ ?j) x" by(simp add: g_def)
also have "… = (∑⇧+ y∈❙I❙N x. f (y, x) + j (Some x, Some y) - j (Some y, Some x))"
by(auto simp add: d_IN_def currentD_outside[OF f'] incoming_def nn_integral_count_space_indicator intro!: nn_integral_cong)
also have "… = (∑⇧+ y∈❙I❙N x. f (y, x) + j (Some x, Some y)) - (∑⇧+ y∈❙I❙N x. j (Some y, Some x))"
(is "_ = _ - ?j_IN") using finite
by(subst nn_integral_diff)(auto simp add: AE_count_space incoming_def intro!: order_trans[OF j_le_f])
also have "… = (∑⇧+ y∈❙I❙N x. f (y, x)) + (∑⇧+ y∈❙I❙N x. j (Some x, Some y)) - ?j_IN"
(is "_ = ?f + ?j_OUT - _") by(subst nn_integral_add) simp_all
also have "?f = d_IN f x" by(subst d_IN_alt_def[where G=Γ])(simp_all add: currentD_outside[OF f])
also have "?j_OUT = (∑⇧+ y∈range Some. j (Some x, y))" using True disjoint
by(simp add: nn_integral_count_space_reindex)(auto 4 4 simp add: nn_integral_count_space_indicator incoming_def intro!: nn_integral_cong Ψ.flowD_outside[OF j] split: split_indicator dest: bipartite_E)
also have "… = d_OUT j (Some x)" using disjoint
by(auto 4 3 simp add: d_OUT_def nn_integral_count_space_indicator notin_range_Some intro!: nn_integral_cong Ψ.flowD_outside[OF j] split: split_indicator)
also have "… = d_IN j (Some x)" using flowD_KIR[OF j, of "Some x"] True a disjoint by auto
also have "?j_IN = (∑⇧+ y∈range Some. j (y, Some x))" using True disjoint
by(simp add: nn_integral_count_space_reindex)(auto 4 4 simp add: nn_integral_count_space_indicator incoming_def intro!: nn_integral_cong Ψ.flowD_outside[OF j] dest: bipartite_E split: split_indicator)
also have "… = d_IN j (Some x) - (∑⇧+ y :: 'v option. j (None, Some x) * indicator {None} y)"
unfolding d_IN_def using flowD_capacity[OF j, of "(None, Some x)"]
by(subst nn_integral_diff[symmetric])
(auto simp add: nn_integral_count_space_indicator AE_count_space top_unique image_iff
intro!: nn_integral_cong ennreal_diff_self split: split_indicator if_split_asm)
also have "d_IN f x + d_IN j (Some x) - … = d_IN f x + j (None, Some x)"
using ennreal_add_diff_cancel_right[OF IN_j_finite[of "Some x"], of "d_IN f x + j (None, Some x)"]
apply(subst diff_diff_ennreal')
apply(auto simp add: d_IN_def intro!: nn_integral_ge_point ennreal_diff_le_mono_left)
apply(simp add: ac_simps)
done
finally show ?thesis .
next
case False
hence "d_IN g x = 0" "d_IN f x = 0" "j (None, ⟨x⟩) = 0"
using disjoint currentD_IN[OF f', of x] bipartite_V currentD_outside_IN[OF f'] u_outside[OF False] flowD_capacity[OF j, of "(None, ⟨x⟩)"]
by(cases "vertex Γ x"; auto simp add: d_IN_def nn_integral_0_iff_AE AE_count_space g_simps dest: bipartite_E split: if_split_asm)+
thus ?thesis by simp
qed
have g: "current Γ g"
proof
show "d_OUT g x ≤ weight Γ x" for x
proof(cases "x ∈ A Γ")
case False
thus ?thesis by(simp add: OUT_g_B)
next
case True
with OUT_g_a show ?thesis
by(cases "x = a")(simp_all add: OUT_g_A flowD_KIR[OF j] currentD_weight_OUT[OF f'])
qed
show "d_IN g x ≤ weight Γ x" for x
proof(cases "x ∈ B Γ")
case False
hence "d_IN g x = 0" using disjoint
by(auto simp add: d_IN_def nn_integral_0_iff_AE AE_count_space g_simps dest: bipartite_E)
thus ?thesis by simp
next
case True
have "d_IN g x ≤ (weight Γ x - u x) + u x" unfolding IN_g
using currentD_weight_IN[OF f, of x] flowD_capacity[OF j, of "(None, Some x)"] True bipartite_V
by(intro add_mono)(simp_all split: if_split_asm)
also have "… = weight Γ x"
using u by (intro diff_add_cancel_ennreal) (simp add: le_fun_def)
finally show ?thesis .
qed
show "g e = 0" if "e ∉ ❙E" for e using that
by(cases e)(auto simp add: g_simps)
qed
define cap' where "cap' = (λ(x, y). if edge Γ x y then g (x, y) else if edge Γ y x then 1 else 0)"
have cap'_simps [simp]: "cap' (x, y) = (if edge Γ x y then g (x, y) else if edge Γ y x then 1 else 0)"
for x y by(simp add: cap'_def)
define G where "G = ⦇edge = λx y. cap' (x, y) > 0⦈"
have G_sel [simp]: "edge G x y ⟷ cap' (x, y) > 0" for x y by(simp add: G_def)
define reachable where "reachable x = (edge G)⇧*⇧* x a" for x
have reachable_alt_def: "reachable ≡ λx. ∃p. path G x p a"
by(simp add: reachable_def [abs_def] rtranclp_eq_rtrancl_path)
have [simp]: "reachable a" by(auto simp add: reachable_def)
have AB_edge: "edge G x y" if "edge Γ y x" for x y
using that
by(auto dest: edge_antiparallel simp add: min_def le_neq_trans add_eq_0_iff_both_eq_0)
have reachable_AB: "reachable y" if "reachable x" "(x, y) ∈ ❙E" for x y
using that by(auto simp add: reachable_def simp del: G_sel dest!: AB_edge intro: rtrancl_path.step)
have reachable_BA: "g (x, y) = 0" if "reachable y" "(x, y) ∈ ❙E" "¬ reachable x" for x y
proof(rule ccontr)
assume "g (x, y) ≠ 0"
then have "g (x, y) > 0" by (simp add: zero_less_iff_neq_zero)
hence "edge G x y" using that by simp
then have "reachable x" using ‹reachable y›
unfolding reachable_def by(rule converse_rtranclp_into_rtranclp)
with ‹¬ reachable x› show False by contradiction
qed
have reachable_V: "vertex Γ x" if "reachable x" for x
proof -
from that obtain p where p: "path G x p a" unfolding reachable_alt_def ..
then show ?thesis using rtrancl_path_nth[OF p, of 0] a(1) A_vertex
by(cases "p = []")(auto 4 3 simp add: vertex_def elim: rtrancl_path.cases split: if_split_asm)
qed
have finite_j_IN: "(∫⇧+ y. j (Some y, Some x) ∂count_space (❙I❙N x)) ≠ ⊤" for x
proof -
have "(∫⇧+ y. j (Some y, Some x) ∂count_space (❙I❙N x)) ≤ d_IN f x"
by(auto intro!: nn_integral_mono j_le_f simp add: d_IN_def nn_integral_count_space_indicator incoming_def split: split_indicator)
thus ?thesis using currentD_finite_IN[OF f', of x] by (auto simp: top_unique)
qed
have j_outside: "j (x, y) = 0" if "¬ edge Ψ x y" for x y
using that flowD_capacity[OF j, of "(x, y)"] Ψ.capacity_outside[of "(x, y)"]
by(auto)
define h where "h = (λ(x, y). if reachable x ∧ reachable y then g (x, y) else 0)"
have h_simps [simp]: "h (x, y) = (if reachable x ∧ reachable y then g (x, y) else 0)" for x y
by(simp add: h_def)
have h_le_g: "h e ≤ g e" for e by(cases e) simp
have OUT_h: "d_OUT h x = (if reachable x then d_OUT g x else 0)" for x
proof -
have "d_OUT h x = (∑⇧+ y∈❙O❙U❙T x. h (x, y))" using h_le_g currentD_outside[OF g]
by(intro d_OUT_alt_def) auto
also have "… = (∑⇧+ y∈❙O❙U❙T x. if reachable x then g (x, y) else 0)"
by(auto intro!: nn_integral_cong simp add: outgoing_def dest: reachable_AB)
also have "… = (if reachable x then d_OUT g x else 0)"
by(auto intro!: d_OUT_alt_def[symmetric] currentD_outside[OF g])
finally show ?thesis .
qed
have IN_h: "d_IN h x = (if reachable x then d_IN g x else 0)" for x
proof -
have "d_IN h x = (∑⇧+ y∈❙I❙N x. h (y, x))"
using h_le_g currentD_outside[OF g] by(intro d_IN_alt_def) auto
also have "… = (∑⇧+ y∈❙I❙N x. if reachable x then g (y, x) else 0)"
by(auto intro!: nn_integral_cong simp add: incoming_def dest: reachable_BA)
also have "… = (if reachable x then d_IN g x else 0)"
by(auto intro!: d_IN_alt_def[symmetric] currentD_outside[OF g])
finally show ?thesis .
qed
have h: "current Γ h" using g h_le_g
proof(rule current_leI)
show "d_OUT h x ≤ d_IN h x" if "x ∉ A Γ" for x
by(simp add: OUT_h IN_h currentD_OUT_IN[OF g that])
qed
have reachable_full: "j (None, ⟨y⟩) = u y" if reach: "reachable y" for y
proof(rule ccontr)
assume "j (None, ⟨y⟩) ≠ u y"
with flowD_capacity[OF j, of "(None, ⟨y⟩)"]
have le: "j (None, ⟨y⟩) < u y" by(auto split: if_split_asm simp add: u_outside Ψ.flowD_outside[OF j] zero_less_iff_neq_zero)
then obtain y: "y ∈ B Γ" and uy: "u y > 0" using u_outside[of y]
by(cases "y ∈ B Γ"; cases "u y = 0") (auto simp add: zero_less_iff_neq_zero)
from reach obtain q where q: "path G y q a" and distinct: "distinct (y # q)"
unfolding reachable_alt_def by(auto elim: rtrancl_path_distinct)
have q_Nil: "q ≠ []" using q a(1) disjoint y by(auto elim!: rtrancl_path.cases)
let ?E = "zip (y # q) q"
define E where "E = (None, Some y) # map (map_prod Some Some) ?E"
define ζ where "ζ = Min (insert (u y - j (None, Some y)) (cap' ` set ?E))"
let ?j' = "λe. (if e ∈ set E then ζ else 0) + j e"
define j' where "j' = cleanup ?j'"
have j_free: "0 < cap' e" if "e ∈ set ?E" for e using that unfolding E_def list.sel
proof -
from that obtain i where e: "e = ((y # q) ! i, q ! i)"
and i: "i < length q" by(auto simp add: set_zip)
have e': "edge G ((y # q) ! i) (q ! i)" using q i by(rule rtrancl_path_nth)
thus ?thesis using e by(simp)
qed
have ζ_pos: "0 < ζ" unfolding ζ_def using le
by(auto intro: j_free diff_gr0_ennreal)
have ζ_le: "ζ ≤ cap' e" if "e ∈ set ?E" for e using that unfolding ζ_def by auto
have finite_ζ [simplified]: "ζ < ⊤" unfolding ζ_def
by(intro Min_less_iff[THEN iffD2])(auto simp add: less_top[symmetric])
have E_antiparallel: "(x', y') ∈ set ?E ⟹ (y', x') ∉ set ?E" for x' y'
using distinct
apply(auto simp add: in_set_zip nth_Cons in_set_conv_nth)
apply(auto simp add: distinct_conv_nth split: nat.split_asm)
by (metis Suc_lessD less_Suc_eq less_irrefl_nat)
have OUT_j': "d_OUT ?j' x' = ζ * card (set [(x'', y) ← E. x'' = x']) + d_OUT j x'" for x'
proof -
have "d_OUT ?j' x' = d_OUT (λe. if e ∈ set E then ζ else 0) x' + d_OUT j x'"
using ζ_pos by(intro d_OUT_add)
also have "d_OUT (λe. if e ∈ set E then ζ else 0) x' = ∫⇧+ y. ζ * indicator (set E) (x', y) ∂count_space UNIV"
unfolding d_OUT_def by(rule nn_integral_cong)(simp)
also have "… = (∫⇧+ e. ζ * indicator (set E) e ∂embed_measure (count_space UNIV) (Pair x'))"
by(simp add: measurable_embed_measure1 nn_integral_embed_measure)
also have "… = (∫⇧+ e. ζ * indicator (set [(x'', y) ← E. x'' = x']) e ∂count_space UNIV)"
by(auto simp add: embed_measure_count_space' nn_integral_count_space_indicator intro!: nn_integral_cong split: split_indicator)
also have "… = ζ * card (set [(x'', y) ← E. x'' = x'])" using ζ_pos by(simp add: nn_integral_cmult)
finally show ?thesis .
qed
have IN_j': "d_IN ?j' x' = ζ * card (set [(y, x'') ← E. x'' = x']) + d_IN j x'" for x'
proof -
have "d_IN ?j' x' = d_IN (λe. if e ∈ set E then ζ else 0) x' + d_IN j x'"
using ζ_pos by(intro d_IN_add)
also have "d_IN (λe. if e ∈ set E then ζ else 0) x' = ∫⇧+ y. ζ * indicator (set E) (y, x') ∂count_space UNIV"
unfolding d_IN_def by(rule nn_integral_cong)(simp)
also have "… = (∫⇧+ e. ζ * indicator (set E) e ∂embed_measure (count_space UNIV) (λy. (y, x')))"
by(simp add: measurable_embed_measure1 nn_integral_embed_measure)
also have "… = (∫⇧+ e. ζ * indicator (set [(y, x'') ← E. x'' = x']) e ∂count_space UNIV)"
by(auto simp add: embed_measure_count_space' nn_integral_count_space_indicator intro!: nn_integral_cong split: split_indicator)
also have "… = ζ * card (set [(y, x'') ← E. x'' = x'])"
using ζ_pos by(auto simp add: nn_integral_cmult)
finally show ?thesis .
qed
have j': "flow Ψ j'"
proof
fix e :: "'v option edge"
consider (None) "e = (None, Some y)"
| (Some) x y where "e = (Some x, Some y)" "(x, y) ∈ set ?E"
| (old) x y where "e = (Some x, Some y)" "(x, y) ∉ set ?E"
| y' where "e = (None, Some y')" "y ≠ y'"
| "e = (None, None)" | x where "e = (Some x, None)"
by(cases e; case_tac a; case_tac b)(auto)
then show "j' e ≤ capacity Ψ e" using uy ζ_pos flowD_capacity[OF j, of e]
proof(cases)
case None
have "ζ ≤ u y - j (None, Some y)" by(simp add: ζ_def)
then have "ζ + j (None, Some y) ≤ u y"
using ζ_pos by (auto simp add: ennreal_le_minus_iff)
thus ?thesis using reachable_V[OF reach] None Ψ.flowD_outside[OF j, of "(Some y, None)"] uy
by(auto simp add: j'_def E_def)
next
case (Some x' y')
have e: "ζ ≤ cap' (x', y')" using Some(2) by(rule ζ_le)
then consider (backward) "edge Γ x' y'" "x' ≠ a" | (forward) "edge Γ y' x'" "¬ edge Γ x' y'"
| (a') "edge Γ x' y'" "x' = a"
using Some ζ_pos by(auto split: if_split_asm)
then show ?thesis
proof cases
case backward
have "ζ ≤ f (x', y') + j (Some y', Some x') - j (Some x', Some y')"
using e backward Some(1) by(simp add: g_simps)
hence "ζ + j (Some x', Some y') - j (Some y', Some x') ≤ (f (x', y') + j (Some y', Some x') - j (Some x', Some y')) + j (Some x', Some y') - j (Some y', Some x')"
by(intro ennreal_minus_mono add_right_mono) simp_all
also have "… = f (x', y')"
using j_le_f[OF ‹edge Γ x' y'›]
by(simp_all add: add_increasing2 less_top diff_add_assoc2_ennreal)
finally show ?thesis using Some backward
by(auto simp add: j'_def E_def dest: in_set_tlD E_antiparallel)
next
case forward
have "ζ + j (Some x', Some y') - j (Some y', Some x') ≤ ζ + j (Some x', Some y')"
by(rule diff_le_self_ennreal)
also have "j (Some x', Some y') ≤ d_IN j (Some y')"
by(rule d_IN_ge_point)
also have "… ≤ weight Γ y'" by(rule IN_j_le_weight)
also have "ζ ≤ 1" using e forward by simp
finally have "ζ + j (Some x', Some y') - j (Some y', Some x') ≤ max (weight Γ x') (weight Γ y') + 1"
by(simp add: add_left_mono add_right_mono max_def)(metis (no_types, lifting) add.commute add_right_mono less_imp_le less_le_trans not_le)
then show ?thesis using Some forward e
by(auto simp add: j'_def E_def max_def dest: in_set_tlD E_antiparallel)
next
case a'
with Some have "a ∈ set (map fst (zip (y # q) q))" by(auto intro: rev_image_eqI)
also have "map fst (zip (y # q) q) = butlast (y # q)" by(induction q arbitrary: y) auto
finally have False using rtrancl_path_last[OF q q_Nil] distinct q_Nil
by(cases q rule: rev_cases) auto
then show ?thesis ..
qed
next
case (old x' y')
hence "j' e ≤ j e" using ζ_pos
by(auto simp add: j'_def E_def intro!: diff_le_self_ennreal)
also have "j e ≤ capacity Ψ e" using j by(rule flowD_capacity)
finally show ?thesis .
qed(auto simp add: j'_def E_def Ψ.flowD_outside[OF j] uy)
next
fix x'
assume x': "x' ≠ source Ψ" "x' ≠ sink Ψ"
then obtain x'' where x'': "x' = Some x''" by auto
have "d_OUT ?j' x' = ζ * card (set [(x'', y) ← E. x'' = x']) + d_OUT j x'" by(rule OUT_j')
also have "card (set [(x'', y) ← E. x'' = x']) = card (set [(y, x'') ← E. x'' = x'])" (is "?lhs = ?rhs")
proof -
have "?lhs = length [(x'', y) ← E. x'' = x']" using distinct
by(subst distinct_card)(auto simp add: E_def filter_map distinct_map inj_map_prod' distinct_zipI1)
also have "… = length [x''' ← map fst ?E. x''' = x'']"
by(simp add: E_def x'' split_beta cong: filter_cong)
also have "map fst ?E = butlast (y # q)" by(induction q arbitrary: y) simp_all
also have "[x''' ← butlast (y # q). x''' = x''] = [x''' ← y # q. x''' = x'']"
using q_Nil rtrancl_path_last[OF q q_Nil] x' x''
by(cases q rule: rev_cases) simp_all
also have "q = map snd ?E" by(induction q arbitrary: y) auto
also have "length [x''' ← y # …. x''' = x''] = length [x'' ← map snd E. x'' = x']" using x''
by(simp add: E_def cong: filter_cong)
also have "… = length [(y, x'') ← E. x'' = x']" by(simp cong: filter_cong add: split_beta)
also have "… = ?rhs" using distinct
by(subst distinct_card)(auto simp add: E_def filter_map distinct_map inj_map_prod' distinct_zipI1)
finally show ?thesis .
qed
also have "ζ * … + d_OUT j x' = d_IN ?j' x'"
unfolding flowD_KIR[OF j x'] by(rule IN_j'[symmetric])
also have "d_IN ?j' x' ≠ ⊤"
using Ψ.flowD_finite_IN[OF j x'(2)] finite_ζ IN_j'[of x'] by (auto simp: top_add ennreal_mult_eq_top_iff)
ultimately show "KIR j' x'" unfolding j'_def by(rule KIR_cleanup)
qed
hence "value_flow Ψ j' ≤ α" unfolding α_def by(auto intro: SUP_upper)
moreover have "value_flow Ψ j' > value_flow Ψ j"
proof -
have "value_flow Ψ j + 0 < value_flow Ψ j + ζ * 1"
using ζ_pos value_j finite_flow by simp
also have "[(x', y') ← E. x' = None] = [(None, Some y)]"
using q_Nil by(cases q)(auto simp add: E_def filter_map cong: filter_cong split_beta)
hence "ζ * 1 ≤ ζ * card (set [(x', y') ← E. x' = None])" using ζ_pos
by(intro mult_left_mono)(auto simp add: E_def real_of_nat_ge_one_iff neq_Nil_conv card.insert_remove)
also have "value_flow Ψ j + … = value_flow Ψ ?j'"
using OUT_j' by(simp add: add.commute)
also have "… = value_flow Ψ j'" unfolding j'_def
by(subst value_flow_cleanup)(auto simp add: E_def Ψ.flowD_outside[OF j])
finally show ?thesis by(simp add: add_left_mono)
qed
ultimately show False using finite_flow ζ_pos value_j
by(cases "value_flow Ψ j" ζ rule: ennreal2_cases) simp_all
qed
have sep_h: "y ∈ TER h" if reach: "reachable y" and y: "y ∈ B Γ" and TER: "y ∈ ?TER f" for y
proof(rule ccontr)
assume y': "y ∉ TER h"
from y a(1) disjoint have yna: "y ≠ a" by auto
from reach obtain p' where "path G y p' a" unfolding reachable_alt_def ..
then obtain p' where p': "path G y p' a" and distinct: "distinct (y # p')" by(rule rtrancl_path_distinct)
have SINK: "y ∈ SINK h" using y disjoint
by(auto simp add: SINK.simps d_OUT_def nn_integral_0_iff emeasure_count_space_eq_0 intro: currentD_outside[OF g] dest: bipartite_E)
have hg: "d_IN h y = d_IN g y" using reach by(simp add: IN_h)
also have "… = d_IN f y + j (None, Some y)" by(simp add: IN_g)
also have "d_IN f y = weight Γ y - u y" using currentD_weight_IN[OF f, of y] y disjoint TER
by(auto elim!: SAT.cases)
also have "d_IN h y < weight Γ y" using y' currentD_weight_IN[OF g, of y] y disjoint SINK
by(auto intro: SAT.intros)
ultimately have le: "j (None, Some y) < u y"
by(cases "weight Γ y" "u y" "j (None, Some y)" rule: ennreal3_cases; cases "u y ≤ weight Γ y")
(auto simp: ennreal_minus ennreal_plus[symmetric] add_top ennreal_less_iff ennreal_neg simp del: ennreal_plus)
moreover from reach have "j (None, ⟨y⟩) = u y" by(rule reachable_full)
ultimately show False by simp
qed
have w': "wave Γ h"
proof
show sep: "separating Γ (TER h)"
proof(rule ccontr)
assume "¬ ?thesis"
then obtain x p y where x: "x ∈ A Γ" and y: "y ∈ B Γ" and p: "path Γ x p y"
and x': "x ∉ TER h" and bypass: "⋀z. z ∈ set p ⟹ z ∉ TER h"
by(auto simp add: separating_gen.simps)
from p disjoint x y have p_eq: "p = [y]" and edge: "(x, y) ∈ ❙E"
by -(erule rtrancl_path.cases, auto dest: bipartite_E)+
from p_eq bypass have y': "y ∉ TER h" by simp
have "reachable x" using x' by(rule contrapos_np)(simp add: SINK.simps d_OUT_def SAT.A x)
hence reach: "reachable y" using edge by(rule reachable_AB)
have *: "x ∉ ℰ⇘?Γ⇙ (?TER f)" using x'
proof(rule contrapos_nn)
assume *: "x ∈ ℰ⇘?Γ⇙ (?TER f)"
have "d_OUT h x ≤ d_OUT g x" using h_le_g by(rule d_OUT_mono)
also from * have "x ≠ a" using a by auto
then have "d_OUT j (Some x) = d_IN j (Some x)" by(auto intro: flowD_KIR[OF j])
hence "d_OUT g x ≤ d_OUT f x" using OUT_g_A[OF x] IN_j[of "Some x"] finite_flow
by(auto split: if_split_asm)
also have "… = 0" using * by(auto elim: SINK.cases)
finally have "x ∈ SINK h" by(simp add: SINK.simps)
with x show "x ∈ TER h" by(simp add: SAT.A)
qed
from p p_eq x y have "path ?Γ x [y] y" "x ∈ A ?Γ" "y ∈ B ?Γ" by simp_all
from * separatingD[OF separating_essential, OF waveD_separating, OF w this]
have "y ∈ ?TER f" by auto
with reach y have "y ∈ TER h" by(rule sep_h)
with y' show False by contradiction
qed
qed(rule h)
have OUT_g_a: "d_OUT g a = d_OUT h a" by(simp add: OUT_h)
have "a ∉ ℰ (TER h)"
proof
assume *: "a ∈ ℰ (TER h)"
have "j (Some a, Some y) = 0" for y
using flowD_capacity[OF j, of "(Some a, Some y)"] a(1) disjoint
by(auto split: if_split_asm dest: bipartite_E)
then have "d_OUT f a ≤ d_OUT g a" unfolding d_OUT_def
by(intro nn_integral_mono)(auto simp add: g_simps currentD_outside[OF f] intro: )
then have "a ∈ SINK f" using OUT_g_a * by(simp add: SINK.simps)
with a(1) have "a ∈ ?TER f" by(auto intro: SAT.A)
with a(2) have a': "¬ essential Γ (B Γ) (?TER f) a" by simp
from * obtain y where ay: "edge Γ a y" and y: "y ∈ B Γ" and y': "y ∉ TER h" using disjoint a(1)
by(auto 4 4 simp add: essential_def elim: rtrancl_path.cases dest: bipartite_E)
from not_essentialD[OF a' rtrancl_path.step, OF ay rtrancl_path.base y]
have TER: "y ∈ ?TER f" by simp
have "reachable y" using ‹reachable a› by(rule reachable_AB)(simp add: ay)
hence "y ∈ TER h" using y TER by(rule sep_h)
with y' show False by contradiction
qed
with ‹a ∈ A Γ› have "hindrance Γ h"
proof
have "d_OUT h a = d_OUT g a" by(simp add: OUT_g_a)
also have "… ≤ d_OUT f a + ∫⇧+ y. j (Some y, Some a) ∂count_space UNIV"
unfolding d_OUT_def d_IN_def
by(subst nn_integral_add[symmetric])(auto simp add: g_simps intro!: nn_integral_mono diff_le_self_ennreal)
also have "(∫⇧+ y. j (Some y, Some a) ∂count_space UNIV) = (∫⇧+ y. j (y, Some a) ∂embed_measure (count_space UNIV) Some)"
by(simp add: nn_integral_embed_measure measurable_embed_measure1)
also have "… ≤ d_IN j (Some a)" unfolding d_IN_def
by(auto simp add: embed_measure_count_space nn_integral_count_space_indicator intro!: nn_integral_mono split: split_indicator)
also have "… ≤ α" by(rule IN_j)
also have "… ≤ ε" by(rule α_le)
also have "d_OUT f a + … < d_OUT f a + (weight Γ a - d_OUT f a)" using ε_less
using currentD_finite_OUT[OF f'] by (simp add: ennreal_add_left_cancel_less)
also have "… = weight Γ a"
using a_le by simp
finally show "d_OUT h a < weight Γ a" by(simp add: add_left_mono)
qed
then show ?thesis using h w' by(blast intro: hindered.intros)
qed
end
corollary hindered_reduce_current:
fixes ε g
defines "ε ≡ ∑⇧+ x∈B Γ. d_IN g x - d_OUT g x"
assumes g: "current Γ g"
and ε_finite: "ε ≠ ⊤"
and hindered: "hindered_by (Γ ⊖ g) ε"
shows "hindered Γ"
proof -
define Γ' where "Γ' = Γ⦇weight := λx. if x ∈ A Γ then weight Γ x - d_OUT g x else weight Γ x⦈"
have Γ'_sel [simp]:
"edge Γ' = edge Γ"
"A Γ' = A Γ"
"B Γ' = B Γ"
"weight Γ' x = (if x ∈ A Γ then weight Γ x - d_OUT g x else weight Γ x)"
"vertex Γ' = vertex Γ"
"web.more Γ' = web.more Γ"
for x by(simp_all add: Γ'_def)
have "countable_bipartite_web Γ'"
by unfold_locales(simp_all add: A_in B_out A_vertex disjoint bipartite_V no_loop weight_outside currentD_outside_OUT[OF g] currentD_weight_OUT[OF g] edge_antiparallel, rule bipartite_E)
then interpret Γ': countable_bipartite_web Γ' .
let ?u = "λx. (d_IN g x - d_OUT g x) * indicator (- A Γ) x"
have "hindered Γ'"
proof(rule Γ'.hindered_reduce)
show "?u x = 0" if "x ∉ B Γ'" for x using that bipartite_V
by(cases "vertex Γ' x")(auto simp add: currentD_outside_OUT[OF g] currentD_outside_IN[OF g])
have *: "(∑⇧+ x∈B Γ'. ?u x) = ε" using disjoint
by(auto intro!: nn_integral_cong simp add: ε_def nn_integral_count_space_indicator currentD_outside_OUT[OF g] currentD_outside_IN[OF g] not_vertex split: split_indicator)
thus "(∑⇧+ x∈B Γ'. ?u x) ≠ ⊤" using ε_finite by simp
have **: "Γ'⦇weight := weight Γ' - ?u⦈ = Γ ⊖ g"
using currentD_weight_IN[OF g] currentD_OUT_IN[OF g] currentD_IN[OF g] currentD_finite_OUT[OF g]
by(intro web.equality)(simp_all add: fun_eq_iff diff_diff_ennreal' ennreal_diff_le_mono_left)
show "hindered_by (Γ'⦇weight := weight Γ' - ?u⦈) (∑⇧+ x∈B Γ'. ?u x)"
unfolding * ** by(fact hindered)
show "(λx. (d_IN g x - d_OUT g x) * indicator (- A Γ) x) ≤ weight Γ'"
using currentD_weight_IN[OF g]
by (simp add: le_fun_def ennreal_diff_le_mono_left)
qed
then show ?thesis
by(rule hindered_mono_web[rotated -1]) simp_all
qed
end
subsection ‹Reduced weight in a loose web›
definition reduce_weight :: "('v, 'more) web_scheme ⇒ 'v ⇒ real ⇒ ('v, 'more) web_scheme"
where "reduce_weight Γ x r = Γ⦇weight := λy. weight Γ y - (if x = y then r else 0)⦈"
lemma reduce_weight_sel [simp]:
"edge (reduce_weight Γ x r) = edge Γ"
"A (reduce_weight Γ x r) = A Γ"
"B (reduce_weight Γ x r) = B Γ"
"vertex (reduce_weight Γ x r) = vertex Γ"
"weight (reduce_weight Γ x r) y = (if x = y then weight Γ x - r else weight Γ y)"
"web.more (reduce_weight Γ x r) = web.more Γ"
by(simp_all add: reduce_weight_def zero_ennreal_def[symmetric] vertex_def fun_eq_iff)
lemma essential_reduce_weight [simp]: "essential (reduce_weight Γ x r) = essential Γ"
by(simp add: fun_eq_iff essential_def)
lemma roofed_reduce_weight [simp]: "roofed_gen (reduce_weight Γ x r) = roofed_gen Γ"
by(simp add: fun_eq_iff roofed_def)
context countable_bipartite_web begin
context begin
private