Theory MFMC_Reduction
section ‹Reductions›
theory MFMC_Reduction imports
MFMC_Web
begin
subsection ‹From a web to a bipartite web›
definition bipartite_web_of :: "('v, 'more) web_scheme ⇒ ('v + 'v, 'more) web_scheme"
where
"bipartite_web_of Γ =
⦇edge = λuv uv'. case (uv, uv') of (Inl u, Inr v) ⇒ edge Γ u v ∨ u = v ∧ u ∈ vertices Γ ∧ u ∉ A Γ ∧ v ∉ B Γ | _ ⇒ False,
weight = λuv. case uv of Inl u ⇒ if u ∈ B Γ then 0 else weight Γ u | Inr u ⇒ if u ∈ A Γ then 0 else weight Γ u,
A = Inl ` (vertices Γ - B Γ),
B = Inr ` (- A Γ),
… = web.more Γ⦈"
lemma bipartite_web_of_sel [simp]: fixes Γ (structure) shows
"edge (bipartite_web_of Γ) (Inl u) (Inr v) ⟷ edge Γ u v ∨ u = v ∧ u ∈ ❙V ∧ u ∉ A Γ ∧ v ∉ B Γ"
"edge (bipartite_web_of Γ) uv (Inl u) ⟷ False"
"edge (bipartite_web_of Γ) (Inr v) uv ⟷ False"
"weight (bipartite_web_of Γ) (Inl u) = (if u ∈ B Γ then 0 else weight Γ u)"
"weight (bipartite_web_of Γ) (Inr v) = (if v ∈ A Γ then 0 else weight Γ v)"
"A (bipartite_web_of Γ) = Inl ` (❙V - B Γ)"
"B (bipartite_web_of Γ) = Inr ` (- A Γ)"
by(simp_all add: bipartite_web_of_def split: sum.split)
lemma edge_bipartite_webI1: "edge Γ u v ⟹ edge (bipartite_web_of Γ) (Inl u) (Inr v)"
by(auto)
lemma edge_bipartite_webI2:
"⟦ u ∈ ❙V⇘Γ⇙; u ∉ A Γ; u ∉ B Γ ⟧ ⟹ edge (bipartite_web_of Γ) (Inl u) (Inr u)"
by(auto)
lemma edge_bipartite_webE:
fixes Γ (structure)
assumes "edge (bipartite_web_of Γ) uv uv'"
obtains u v where "uv = Inl u" "uv' = Inr v" "edge Γ u v"
| u where "uv = Inl u" "uv' = Inr u" "u ∈ ❙V" "u ∉ A Γ" "u ∉ B Γ"
using assms by(cases uv uv' rule: sum.exhaust[case_product sum.exhaust]) auto
lemma E_bipartite_web:
fixes Γ (structure) shows
"❙E⇘bipartite_web_of Γ⇙ = (λ(x, y). (Inl x, Inr y)) ` ❙E ∪ (λx. (Inl x, Inr x)) ` (❙V - A Γ - B Γ)"
by(auto elim: edge_bipartite_webE)
context web begin
lemma vertex_bipartite_web [simp]:
"vertex (bipartite_web_of Γ) (Inl x) ⟷ vertex Γ x ∧ x ∉ B Γ"
"vertex (bipartite_web_of Γ) (Inr x) ⟷ vertex Γ x ∧ x ∉ A Γ"
by(auto 4 4 simp add: vertex_def dest: B_out A_in intro: edge_bipartite_webI1 edge_bipartite_webI2 elim!: edge_bipartite_webE)
definition separating_of_bipartite :: "('v + 'v) set ⇒ 'v set"
where
"separating_of_bipartite S =
(let A_S = Inl -` S; B_S = Inr -` S in (A_S ∩ B_S) ∪ (A Γ ∩ A_S) ∪ (B Γ ∩ B_S))"
context
fixes S :: "('v + 'v) set"
assumes sep: "separating (bipartite_web_of Γ) S"
begin
text ‹Proof of separation follows \<^cite>‹Aharoni1983EJC››
lemma separating_of_bipartite_aux:
assumes p: "path Γ x p y" and y: "y ∈ B Γ"
and x: "x ∈ A Γ ∨ Inr x ∈ S"
shows "(∃z∈set p. z ∈ separating_of_bipartite S) ∨ x ∈ separating_of_bipartite S"
proof(cases "p = []")
case True
with p have "x = y" by cases auto
with y x have "x ∈ separating_of_bipartite S" using disjoint
by(auto simp add: separating_of_bipartite_def Let_def)
thus ?thesis ..
next
case nNil: False
define inmarked where "inmarked x ⟷ x ∈ A Γ ∨ Inr x ∈ S" for x
define outmarked where "outmarked x ⟷ x ∈ B Γ ∨ Inl x ∈ S" for x
let ?Γ = "bipartite_web_of Γ"
let ?double = "λx. inmarked x ∧ outmarked x"
define tailmarked where "tailmarked = (λ(x, y :: 'v). outmarked x)"
define headmarked where "headmarked = (λ(x :: 'v, y). inmarked y)"
have marked_E: "tailmarked e ∨ headmarked e" if "e ∈ ❙E" for e
proof(cases e)
case (Pair x y)
with that have "path ?Γ (Inl x) [Inr y] (Inr y)" by(auto intro!: rtrancl_path.intros)
from separatingD[OF sep this] that Pair show ?thesis
by(fastforce simp add: vertex_def inmarked_def outmarked_def tailmarked_def headmarked_def)
qed
have "∃z∈set (x # p). ?double z"
proof -
have "inmarked ((x # p) ! (i + 1)) ∨ outmarked ((x # p) ! i)" if "i < length p" for i
using rtrancl_path_nth[OF p that] marked_E[of "((x # p) ! i, p ! i)"] that
by(auto simp add: tailmarked_def headmarked_def nth_Cons split: nat.split)
hence "{i. i < length p ∧ inmarked (p ! i)} ∪ {i. i < length (x # butlast p) ∧ outmarked ((x # butlast p) ! i)} = {i. i < length p}"
(is "?in ∪ ?out = _") using nNil
by(force simp add: nth_Cons' nth_butlast elim: meta_allE[where x=0] cong del: old.nat.case_cong_weak)
hence "length p + 2 = card (?in ∪ ?out) + 2" by simp
also have "… ≤ (card ?in + 1) + (card ?out + 1)" by(simp add: card_Un_le)
also have "card ?in = card ((λi. Inl (i + 1) :: _ + nat) ` ?in)"
by(rule card_image[symmetric])(simp add: inj_on_def)
also have "… + 1 = card (insert (Inl 0) {Inl (Suc i) :: _ + nat|i. i < length p ∧ inmarked (p ! i)})"
by(subst card_insert_if)(auto intro!: arg_cong[where f=card])
also have "… = card {Inl i :: nat + nat|i. i < length (x # p) ∧ inmarked ((x # p) ! i)}" (is "_ = card ?in")
using x by(intro arg_cong[where f=card])(auto simp add: nth_Cons inmarked_def split: nat.split_asm)
also have "card ?out = card ((Inr :: _ ⇒ nat + _) ` ?out)" by(simp add: card_image)
also have "… + 1 = card (insert (Inr (length p)) {Inr i :: nat + _|i. i < length p ∧ outmarked ((x # p) ! i)})"
using nNil by(subst card_insert_if)(auto intro!: arg_cong[where f=card] simp add: nth_Cons nth_butlast cong: nat.case_cong)
also have "… = card {Inr i :: nat + _|i. i < length (x # p) ∧ outmarked ((x # p) ! i)}" (is "_ = card ?out")
using nNil rtrancl_path_last[OF p nNil] y
by(intro arg_cong[where f=card])(auto simp add: outmarked_def last_conv_nth)
also have "card ?in + card ?out = card (?in ∪ ?out)"
by(rule card_Un_disjoint[symmetric]) auto
also let ?f = "case_sum id id"
have "?f ` (?in ∪ ?out) ⊆ {i. i < length (x # p)}" by auto
from card_mono[OF _ this] have "card (?f ` (?in ∪ ?out)) ≤ length p + 1" by simp
ultimately have "¬ inj_on ?f (?in ∪ ?out)" by(intro pigeonhole) simp
then obtain i where "i < length (x # p)" "?double ((x # p) ! i)"
by(auto simp add: inj_on_def)
thus ?thesis by(auto simp add: set_conv_nth)
qed
moreover have "z ∈ separating_of_bipartite S" if "?double z" for z using that disjoint
by(auto simp add: separating_of_bipartite_def Let_def inmarked_def outmarked_def)
ultimately show ?thesis by auto
qed
lemma separating_of_bipartite:
"separating Γ (separating_of_bipartite S)"
by(rule separating_gen.intros)(erule (1) separating_of_bipartite_aux; simp)
end
lemma current_bipartite_web_finite:
assumes f: "current (bipartite_web_of Γ) f" (is "current ?Γ _")
shows "f e ≠ ⊤"
proof(cases e)
case (Pair x y)
have "f e ≤ d_OUT f x" unfolding Pair d_OUT_def by(rule nn_integral_ge_point) simp
also have "… ≤ weight ?Γ x" by(rule currentD_weight_OUT[OF f])
also have "… < ⊤" by(cases x)(simp_all add: less_top[symmetric])
finally show ?thesis by simp
qed
definition current_of_bipartite :: "('v + 'v) current ⇒ 'v current"
where "current_of_bipartite f = (λ(x, y). f (Inl x, Inr y) * indicator ❙E (x, y))"
lemma current_of_bipartite_simps [simp]: "current_of_bipartite f (x, y) = f (Inl x, Inr y) * indicator ❙E (x, y)"
by(simp add: current_of_bipartite_def)
lemma d_OUT_current_of_bipartite:
assumes f: "current (bipartite_web_of Γ) f"
shows "d_OUT (current_of_bipartite f) x = d_OUT f (Inl x) - f (Inl x, Inr x)"
proof -
have "d_OUT (current_of_bipartite f) x = ∫⇧+ y. f (Inl x, y) * indicator ❙E (x, projr y) ∂count_space (range Inr)"
by(simp add: d_OUT_def nn_integral_count_space_reindex)
also have "… = d_OUT f (Inl x) - ∫⇧+ y. f (Inl x, y) * indicator {Inr x} y ∂count_space UNIV" (is "_ = _ - ?rest")
unfolding d_OUT_def by(subst nn_integral_diff[symmetric])(auto 4 4 simp add: current_bipartite_web_finite[OF f] AE_count_space nn_integral_count_space_indicator no_loop split: split_indicator intro!: nn_integral_cong intro: currentD_outside[OF f] elim: edge_bipartite_webE)
finally show ?thesis by simp
qed
lemma d_IN_current_of_bipartite:
assumes f: "current (bipartite_web_of Γ) f"
shows "d_IN (current_of_bipartite f) x = d_IN f (Inr x) - f (Inl x, Inr x)"
proof -
have "d_IN (current_of_bipartite f) x = ∫⇧+ y. f (y, Inr x) * indicator ❙E (projl y, x) ∂count_space (range Inl)"
by(simp add: d_IN_def nn_integral_count_space_reindex)
also have "… = d_IN f (Inr x) - ∫⇧+ y. f (y, Inr x) * indicator {Inl x} y ∂count_space UNIV" (is "_ = _ - ?rest")
unfolding d_IN_def by(subst nn_integral_diff[symmetric])(auto 4 4 simp add: current_bipartite_web_finite[OF f] AE_count_space nn_integral_count_space_indicator no_loop split: split_indicator intro!: nn_integral_cong intro: currentD_outside[OF f] elim: edge_bipartite_webE)
finally show ?thesis by simp
qed
lemma current_current_of_bipartite:
assumes f: "current (bipartite_web_of Γ) f" (is "current ?Γ _")
and w: "wave (bipartite_web_of Γ) f"
shows "current Γ (current_of_bipartite f)" (is "current _ ?f")
proof
fix x
have "d_OUT ?f x ≤ d_OUT f (Inl x)"
by(simp add: d_OUT_current_of_bipartite[OF f] diff_le_self_ennreal)
also have "… ≤ weight Γ x"
using currentD_weight_OUT[OF f, of "Inl x"]
by(simp split: if_split_asm)
finally show "d_OUT ?f x ≤ weight Γ x" .
next
fix x
have "d_IN ?f x ≤ d_IN f (Inr x)"
by(simp add: d_IN_current_of_bipartite[OF f] diff_le_self_ennreal)
also have "… ≤ weight Γ x"
using currentD_weight_IN[OF f, of "Inr x"]
by(simp split: if_split_asm)
finally show "d_IN ?f x ≤ weight Γ x" .
next
have OUT: "d_OUT ?f b = 0" if "b ∈ B Γ" for b using that
by(auto simp add: d_OUT_def nn_integral_0_iff emeasure_count_space_eq_0 intro!: currentD_outside[OF f] dest: B_out)
show "d_OUT ?f x ≤ d_IN ?f x" if A: "x ∉ A Γ" for x
proof(cases "x ∈ B Γ ∨ x ∉ ❙V")
case True
then show ?thesis
proof
assume "x ∈ B Γ"
with OUT[OF this] show ?thesis by auto
next
assume "x ∉ ❙V"
hence "d_OUT ?f x = 0" by(auto simp add: d_OUT_def vertex_def nn_integral_0_iff emeasure_count_space_eq_0 intro!: currentD_outside[OF f])
thus ?thesis by simp
qed
next
case B [simplified]: False
have "d_OUT ?f x = d_OUT f (Inl x) - f (Inl x, Inr x)" (is "_ = _ - ?rest")
by(simp add: d_OUT_current_of_bipartite[OF f])
also have "d_OUT f (Inl x) ≤ d_IN f (Inr x)"
proof(rule ccontr)
assume "¬ ?thesis"
hence *: "d_IN f (Inr x) < d_OUT f (Inl x)" by(simp add: not_less)
also have "… ≤ weight Γ x" using currentD_weight_OUT[OF f, of "Inl x"] B by simp
finally have "Inr x ∉ TER⇘?Γ⇙ f" using A by(auto elim!: SAT.cases)
moreover have "Inl x ∉ TER⇘?Γ⇙ f" using * by(auto simp add: SINK.simps)
moreover have "path ?Γ (Inl x) [Inr x] (Inr x)"
by(rule rtrancl_path.step)(auto intro!: rtrancl_path.base simp add: no_loop A B)
ultimately show False using waveD_separating[OF w] A B by(auto dest!: separatingD)
qed
hence "d_OUT f (Inl x) - ?rest ≤ d_IN f (Inr x) - ?rest" by(rule ennreal_minus_mono) simp
also have "… = d_IN ?f x" by(simp add: d_IN_current_of_bipartite[OF f])
finally show ?thesis .
qed
show "?f e = 0" if "e ∉ ❙E" for e using that by(cases e)(auto)
qed
lemma TER_current_of_bipartite:
assumes f: "current (bipartite_web_of Γ) f" (is "current ?Γ _")
and w: "wave (bipartite_web_of Γ) f"
shows "TER (current_of_bipartite f) = separating_of_bipartite (TER⇘bipartite_web_of Γ⇙ f)"
(is "TER ?f = separating_of_bipartite ?TER")
proof(rule set_eqI)
fix x
consider (A) "x ∈ A Γ" "x ∈ ❙V" | (B) "x ∈ B Γ" "x ∈ ❙V"
| (inner) "x ∉ A Γ" "x ∉ B Γ" "x ∈ ❙V" | (outside) "x ∉ ❙V" by auto
thus "x ∈ TER ?f ⟷ x ∈ separating_of_bipartite ?TER"
proof cases
case A
hence "d_OUT ?f x = d_OUT f (Inl x)" using currentD_outside[OF f, of "Inl x" "Inr x"]
by(simp add: d_OUT_current_of_bipartite[OF f] no_loop)
thus ?thesis using A disjoint
by(auto simp add: separating_of_bipartite_def Let_def SINK.simps intro!: SAT.A imageI)
next
case B
then have "d_IN ?f x = d_IN f (Inr x)"
using currentD_outside[OF f, of "Inl x" "Inr x"]
by(simp add: d_IN_current_of_bipartite[OF f] no_loop)
moreover have "d_OUT ?f x = 0" using B currentD_outside[OF f, of "Inl x" "Inr x"]
by(simp add: d_OUT_current_of_bipartite[OF f] no_loop)(auto simp add: d_OUT_def nn_integral_0_iff emeasure_count_space_eq_0 intro!: currentD_outside[OF f] elim!: edge_bipartite_webE dest: B_out)
moreover have "d_OUT f (Inr x) = 0" using B disjoint by(intro currentD_OUT[OF f]) auto
ultimately show ?thesis using B
by(auto simp add: separating_of_bipartite_def Let_def SINK.simps SAT.simps)
next
case outside
with current_current_of_bipartite[OF f w] have "d_OUT ?f x = 0" "d_IN ?f x = 0"
by(rule currentD_outside_OUT currentD_outside_IN)+
moreover from outside have "Inl x ∉ vertices ?Γ" "Inr x ∉ vertices ?Γ" by auto
hence "d_OUT f (Inl x) = 0" "d_IN f (Inl x) = 0" "d_OUT f (Inr x) = 0" "d_IN f (Inr x) = 0"
by(blast intro: currentD_outside_OUT[OF f] currentD_outside_IN[OF f])+
ultimately show ?thesis using outside weight_outside[of x]
by(auto simp add: separating_of_bipartite_def Let_def SINK.simps SAT.simps not_le)
next
case inner
show ?thesis
proof
assume "x ∈ separating_of_bipartite ?TER"
with inner have l: "Inl x ∈ ?TER" and r: "Inr x ∈ ?TER"
by(auto simp add: separating_of_bipartite_def Let_def)
have "f (Inl x, Inr x) ≤ d_OUT f (Inl x)"
unfolding d_OUT_def by(rule nn_integral_ge_point) simp
with l have 0: "f (Inl x, Inr x) = 0"
by(auto simp add: SINK.simps)
with l have "x ∈ SINK ?f" by(simp add: SINK.simps d_OUT_current_of_bipartite[OF f])
moreover from r have "Inr x ∈ SAT ?Γ f" by auto
with inner have "x ∈ SAT Γ ?f"
by(auto elim!: SAT.cases intro!: SAT.IN simp add: 0 d_IN_current_of_bipartite[OF f])
ultimately show "x ∈ TER ?f" by simp
next
assume *: "x ∈ TER ?f"
have "d_IN f (Inr x) ≤ weight ?Γ (Inr x)" using f by(rule currentD_weight_IN)
also have "… ≤ weight Γ x" using inner by simp
also have "… ≤ d_IN ?f x" using inner * by(auto elim: SAT.cases)
also have "… ≤ d_IN f (Inr x)"
by(simp add: d_IN_current_of_bipartite[OF f] max_def diff_le_self_ennreal)
ultimately have eq: "d_IN ?f x = d_IN f (Inr x)" by simp
hence 0: "f (Inl x, Inr x) = 0"
using ennreal_minus_cancel_iff[of "d_IN f (Inr x)" "f (Inl x, Inr x)" 0] currentD_weight_IN[OF f, of "Inr x"] inner
d_IN_ge_point[of f "Inl x" "Inr x"]
by(auto simp add: d_IN_current_of_bipartite[OF f] top_unique)
have "Inl x ∈ ?TER" "Inr x ∈ ?TER" using inner * currentD_OUT[OF f, of "Inr x"]
by(auto simp add: SAT.simps SINK.simps d_OUT_current_of_bipartite[OF f] 0 eq)
thus "x ∈ separating_of_bipartite ?TER" unfolding separating_of_bipartite_def Let_def by blast
qed
qed
qed
lemma wave_current_of_bipartite:
assumes f: "current (bipartite_web_of Γ) f" (is "current ?Γ _")
and w: "wave (bipartite_web_of Γ) f"
shows "wave Γ (current_of_bipartite f)" (is "wave _ ?f")
proof
have sep': "separating Γ (separating_of_bipartite (TER⇘?Γ⇙ f))"
by(rule separating_of_bipartite)(rule waveD_separating[OF w])
then show sep: "separating Γ (TER (current_of_bipartite f))"
by(simp add: TER_current_of_bipartite[OF f w])
fix x
assume "x ∉ RF (TER ?f)"
then obtain p y where p: "path Γ x p y" and y: "y ∈ B Γ" and x: "x ∉ TER ?f"
and bypass: "⋀z. z ∈ set p ⟹ z ∉ TER ?f"
by(auto simp add: roofed_def elim: rtrancl_path_distinct)
from p obtain p' where p': "path Γ x p' y" and distinct: "distinct (x # p')"
and subset: "set p' ⊆ set p" by(auto elim: rtrancl_path_distinct)
consider (outside) "x ∉ ❙V" | (A) "x ∈ A Γ" | (B) "x ∈ B Γ" | (inner) "x ∈ ❙V" "x ∉ A Γ" "x ∉ B Γ" by auto
then show "d_OUT ?f x = 0"
proof cases
case outside
with f w show ?thesis by(rule currentD_outside_OUT[OF current_current_of_bipartite])
next
case A
from separatingD[OF sep p A y] bypass have "x ∈ TER ?f" by blast
thus ?thesis by(simp add: SINK.simps)
next
case B
with f w show ?thesis by(rule currentD_OUT[OF current_current_of_bipartite])
next
case inner
hence "path ?Γ (Inl x) [Inr x] (Inr x)" by(auto intro!: rtrancl_path.intros)
from inner waveD_separating[OF w, THEN separatingD, OF this]
consider (Inl) "Inl x ∈ TER⇘?Γ⇙ f" | (Inr) "Inr x ∈ TER⇘?Γ⇙ f" by auto
then show ?thesis
proof cases
case Inl
thus ?thesis
by(auto simp add: SINK.simps d_OUT_current_of_bipartite[OF f] max_def)
next
case Inr
with separating_of_bipartite_aux[OF waveD_separating[OF w] p y] x bypass
have False unfolding TER_current_of_bipartite[OF f w] by blast
thus ?thesis ..
qed
qed
qed
end
context countable_web begin
lemma countable_bipartite_web_of: "countable_bipartite_web (bipartite_web_of Γ)" (is "countable_bipartite_web ?Γ")
proof
show "❙V⇘?Γ⇙ ⊆ A ?Γ ∪ B ?Γ"
apply(rule subsetI)
subgoal for x by(cases x) auto
done
show "A ?Γ ⊆ ❙V⇘?Γ⇙" by auto
show "x ∈ A ?Γ ∧ y ∈ B ?Γ" if "edge ?Γ x y" for x y using that
by(cases x y rule: sum.exhaust[case_product sum.exhaust])(auto simp add: inj_image_mem_iff vertex_def B_out A_in)
show "A ?Γ ∩ B ?Γ = {}" by auto
show "countable ❙E⇘?Γ⇙" by(simp add: E_bipartite_web)
show "weight ?Γ x ≠ ⊤" for x by(cases x) simp_all
show "weight (bipartite_web_of Γ) x = 0" if "x ∉ ❙V⇘?Γ⇙" for x using that
by(cases x)(auto simp add: weight_outside)
qed
end
context web begin
lemma unhindered_bipartite_web_of:
assumes loose: "loose Γ"
shows "¬ hindered (bipartite_web_of Γ)"
proof
assume "hindered (bipartite_web_of Γ)" (is "hindered ?Γ")
then obtain f where f: "current ?Γ f" and w: "wave ?Γ f" and hind: "hindrance ?Γ f" by cases
from f w have "current Γ (current_of_bipartite f)" by(rule current_current_of_bipartite)
moreover from f w have "wave Γ (current_of_bipartite f)" by(rule wave_current_of_bipartite)
ultimately have *: "current_of_bipartite f = zero_current" by(rule looseD_wave[OF loose])
have zero: "f (Inl x, Inr y) = 0" if "x ≠ y" for x y using that *[THEN fun_cong, of "(x, y)"]
by(cases "edge Γ x y")(auto intro: currentD_outside[OF f])
have OUT: "d_OUT f (Inl x) = f (Inl x, Inr x)" for x
proof -
have "d_OUT f (Inl x) = (∑⇧+ y. f (Inl x, y) * indicator {Inr x} y)" unfolding d_OUT_def
using zero currentD_outside[OF f]
apply(intro nn_integral_cong)
subgoal for y by(cases y)(auto split: split_indicator)
done
also have "… = f (Inl x, Inr x)" by simp
finally show ?thesis .
qed
have IN: "d_IN f (Inr x) = f (Inl x, Inr x)" for x
proof -
have "d_IN f (Inr x) = (∑⇧+ y. f (y, Inr x) * indicator {Inl x} y)" unfolding d_IN_def
using zero currentD_outside[OF f]
apply(intro nn_integral_cong)
subgoal for y by(cases y)(auto split: split_indicator)
done
also have "… = f (Inl x, Inr x)" by simp
finally show ?thesis .
qed
let ?TER = "TER⇘?Γ⇙ f"
from hind obtain a where a: "a ∈ A ?Γ" and nℰ: "a ∉ ℰ⇘?Γ⇙ (TER⇘?Γ⇙ f)"
and OUT_a: "d_OUT f a < weight ?Γ a" by cases
from a obtain a' where a': "a = Inl a'" and v: "vertex Γ a'" and b: "a' ∉ B Γ" by auto
have A: "a' ∈ A Γ"
proof(rule ccontr)
assume A: "a' ∉ A Γ"
hence "edge ?Γ (Inl a') (Inr a')" using v b by simp
hence p: "path ?Γ (Inl a') [Inr a'] (Inr a')" by(simp add: rtrancl_path_simps)
from separatingD[OF waveD_separating[OF w] this] b v A
have "Inl a' ∈ ?TER ∨ Inr a' ∈ ?TER" by auto
thus False
proof cases
case left
hence "d_OUT f (Inl a') = 0" by(simp add: SINK.simps)
moreover hence "d_IN f (Inr a') = 0" by(simp add: OUT IN)
ultimately have "Inr a' ∉ ?TER" using v b A OUT_a a' by(auto simp add: SAT.simps)
then have "essential ?Γ (B ?Γ) ?TER (Inl a')" using A
by(intro essentialI[OF p]) simp_all
with nℰ left a' show False by simp
next
case right
hence "d_IN f (Inr a') = weight Γ a'" using A by(auto simp add: currentD_SAT[OF f])
hence "d_OUT f (Inl a') = weight Γ a'" by(simp add: IN OUT)
with OUT_a a' b show False by simp
qed
qed
moreover
from A have "d_OUT f (Inl a') = 0" using currentD_outside[OF f, of "Inl a'" "Inr a'"]
by(simp add: OUT no_loop)
with b v have TER: "Inl a' ∈ ?TER" by(simp add: SAT.A SINK.simps)
with nℰ a' have ness: "¬ essential ?Γ (B ?Γ) ?TER (Inl a')" by simp
have "a' ∉ ℰ (TER zero_current)"
proof
assume "a' ∈ ℰ (TER zero_current)"
then obtain p y where p: "path Γ a' p y" and y: "y ∈ B Γ"
and bypass: "⋀z. z ∈ set p ⟹ z ∉ TER zero_current"
by(rule ℰ_E_RF)(auto intro: roofed_greaterI)
from p show False
proof cases
case base with y A disjoint show False by auto
next
case (step x p')
from step(2) have "path ?Γ (Inl a') [Inr x] (Inr x)" by(simp add: rtrancl_path_simps)
from not_essentialD[OF ness this] bypass[of x] step(1)
have "Inr x ∈ ?TER" by simp
with bypass[of x] step(1) have "d_IN f (Inr x) > 0"
by(auto simp add: currentD_SAT[OF f] zero_less_iff_neq_zero)
hence x: "Inl x ∉ ?TER" by(auto simp add: SINK.simps OUT IN)
from step(1) have "set (x # p') ⊆ set p" by auto
with ‹path Γ x p' y› x y show False
proof induction
case (base x)
thus False using currentD_outside_IN[OF f, of "Inl x"] currentD_outside_OUT[OF f, of "Inl x"]
by(auto simp add: currentD_SAT[OF f] SINK.simps dest!: bypass)
next
case (step x z p' y)
from step.prems(3) bypass[of x] weight_outside[of x] have x: "vertex Γ x" by(auto)
from ‹edge Γ x z› have "path ?Γ (Inl x) [Inr z] (Inr z)" by(simp add: rtrancl_path_simps)
from separatingD[OF waveD_separating[OF w] this] step.prems(1) step.prems(3) bypass[of z] x ‹edge Γ x z›
have "Inr z ∈ ?TER" by(force simp add: B_out inj_image_mem_iff)
with bypass[of z] step.prems(3) ‹edge Γ x z› have "d_IN f (Inr z) > 0"
by(auto simp add: currentD_SAT[OF f] A_in zero_less_iff_neq_zero)
hence x: "Inl z ∉ ?TER" by(auto simp add: SINK.simps OUT IN)
with step.IH[OF this] step.prems(2,3) show False by auto
qed
qed
qed
moreover have "d_OUT zero_current a' < weight Γ a'"
using OUT_a a' b by (auto simp: zero_less_iff_neq_zero)
ultimately have "hindrance Γ zero_current" by(rule hindrance)
with looseD_hindrance[OF loose] show False by contradiction
qed
lemma (in -) divide_less_1_iff_ennreal: "a / b < (1::ennreal) ⟷ (0 < b ∧ a < b ∨ b = 0 ∧ a = 0 ∨ b = top)"
by (cases a; cases b; cases "b = 0")
(auto simp: divide_ennreal ennreal_less_iff ennreal_top_divide)
lemma linkable_bipartite_web_ofD:
assumes link: "linkable (bipartite_web_of Γ)" (is "linkable ?Γ")
and countable: "countable ❙E"
shows "linkable Γ"
proof -
from link obtain f where wf: "web_flow ?Γ f" and link: "linkage ?Γ f" by blast
from wf have f: "current ?Γ f" by(rule web_flowD_current)
define f' where "f' = current_of_bipartite f"
have IN_le_OUT: "d_IN f' x ≤ d_OUT f' x" if "x ∉ B Γ" for x
proof(cases "x ∈ ❙V")
case True
have "d_IN f' x = d_IN f (Inr x) - f (Inl x, Inr x)" (is "_ = _ - ?rest")
by(simp add: f'_def d_IN_current_of_bipartite[OF f])
also have "… ≤ weight ?Γ (Inr x) - ?rest"
using currentD_weight_IN[OF f, of "Inr x"] by(rule ennreal_minus_mono) simp
also have "… ≤ weight ?Γ (Inl x) - ?rest" using that ennreal_minus_mono by(auto)
also have "weight ?Γ (Inl x) = d_OUT f (Inl x)" using that linkageD[OF link, of "Inl x"] True by auto
also have "… - ?rest = d_OUT f' x"
by(simp add: f'_def d_OUT_current_of_bipartite[OF f])
finally show ?thesis .
next
case False
with currentD_outside_OUT[OF f, of "Inl x"] currentD_outside_IN[OF f, of "Inr x"]
show ?thesis by(simp add: f'_def d_IN_current_of_bipartite[OF f] d_OUT_current_of_bipartite[OF f])
qed
have link: "linkage Γ f'"
proof
show "d_OUT f' a = weight Γ a" if "a ∈ A Γ" for a
proof(cases "a ∈ ❙V")
case True
from that have "a ∉ B Γ" using disjoint by auto
with that True linkageD[OF link, of "Inl a"] ennreal_minus_cancel_iff[of _ _ 0] currentD_outside[OF f, of "Inl a" "Inr a"]
show ?thesis by(clarsimp simp add: f'_def d_OUT_current_of_bipartite[OF f] max_def no_loop)
next
case False
with weight_outside[OF this] currentD_outside[OF f, of "Inl a" "Inr a"] currentD_outside_OUT[OF f, of "Inl a"]
show ?thesis by(simp add: f'_def d_OUT_current_of_bipartite[OF f] no_loop)
qed
qed
define F where "F = {g. (∀e. 0 ≤ g e) ∧ (∀e. e ∉ ❙E ⟶ g e = 0) ∧
(∀x. x ∉ B Γ ⟶ d_IN g x ≤ d_OUT g x) ∧
linkage Γ g ∧
(∀x∈A Γ. d_IN g x = 0) ∧
(∀x. d_OUT g x ≤ weight Γ x) ∧
(∀x. d_IN g x ≤ weight Γ x) ∧
(∀x∈B Γ. d_OUT g x = 0) ∧ g ≤ f'}"
define leq where "leq = restrict_rel F {(f, f'). f' ≤ f}"
have F: "Field leq = F" by(auto simp add: leq_def)
have F_I [intro?]: "f ∈ Field leq" if "⋀e. 0 ≤ f e" and "⋀e. e ∉ ❙E ⟹ f e = 0"
and "⋀x. x ∉ B Γ ⟹ d_IN f x ≤ d_OUT f x" and "linkage Γ f"
and "⋀x. x ∈ A Γ ⟹ d_IN f x = 0" and "⋀x. d_OUT f x ≤ weight Γ x"
and "⋀x. d_IN f x ≤ weight Γ x" and "⋀x. x ∈ B Γ ⟹ d_OUT f x = 0"
and "f ≤ f'" for f using that by(simp add: F F_def)
have F_nonneg: "0 ≤ f e" if "f ∈ Field leq" for f e using that by(cases e)(simp add: F F_def)
have F_outside: "f e = 0" if "f ∈ Field leq" "e ∉ ❙E" for f e using that by(cases e)(simp add: F F_def)
have F_IN_OUT: "d_IN f x ≤ d_OUT f x" if "f ∈ Field leq" "x ∉ B Γ" for f x using that by(simp add: F F_def)
have F_link: "linkage Γ f" if "f ∈ Field leq" for f using that by(simp add: F F_def)
have F_IN: "d_IN f x = 0" if "f ∈ Field leq" "x ∈ A Γ" for f x using that by(simp add: F F_def)
have F_OUT: "d_OUT f x = 0" if "f ∈ Field leq" "x ∈ B Γ" for f x using that by(simp add: F F_def)
have F_weight_OUT: "d_OUT f x ≤ weight Γ x" if "f ∈ Field leq" for f x using that by(simp add: F F_def)
have F_weight_IN: "d_IN f x ≤ weight Γ x" if "f ∈ Field leq" for f x using that by(simp add: F F_def)
have F_le: "f e ≤ f' e" if "f ∈ Field leq" for f e using that by(cases e)(simp add: F F_def le_fun_def)
have F_finite_OUT: "d_OUT f x ≠ ⊤" if "f ∈ Field leq" for f x
proof -
have "d_OUT f x ≤ weight Γ x" by(rule F_weight_OUT[OF that])
also have "… < ⊤" by(simp add: less_top[symmetric])
finally show ?thesis by simp
qed
have F_finite: "f e ≠ ⊤" if "f ∈ Field leq" for f e
proof(cases e)
case (Pair x y)
have "f e ≤ d_OUT f x" unfolding Pair d_OUT_def by(rule nn_integral_ge_point) simp
also have "… < ⊤" by(simp add: F_finite_OUT[OF that] less_top[symmetric])
finally show ?thesis by simp
qed
have f': "f' ∈ Field leq"
proof
show "0 ≤ f' e" for e by(cases e)(simp add: f'_def)
show "f' e = 0" if "e ∉ ❙E" for e using that by(clarsimp split: split_indicator_asm simp add: f'_def)
show "d_IN f' x ≤ d_OUT f' x" if "x ∉ B Γ" for x using that by(rule IN_le_OUT)
show "linkage Γ f'" by(rule link)
show "d_IN f' x = 0" if "x ∈ A Γ" for x using that currentD_IN[OF f, of "Inl x"] disjoint
currentD_outside[OF f, of "Inl x" "Inr x"] currentD_outside_IN[OF f, of "Inr x"]
by(cases "x ∈ ❙V")(auto simp add: d_IN_current_of_bipartite[OF f] no_loop f'_def)
show "d_OUT f' x = 0" if "x ∈ B Γ" for x using that currentD_OUT[OF f, of "Inr x"] disjoint
currentD_outside[OF f, of "Inl x" "Inr x"] currentD_outside_OUT[OF f, of "Inl x"]
by(cases "x ∈ ❙V")(auto simp add: d_OUT_current_of_bipartite[OF f] no_loop f'_def)
show "d_OUT f' x ≤ weight Γ x" for x using currentD_weight_OUT[OF f, of "Inl x"]
by(simp add: d_OUT_current_of_bipartite[OF f] ennreal_diff_le_mono_left f'_def split: if_split_asm)
show "d_IN f' x ≤ weight Γ x" for x using currentD_weight_IN[OF f, of "Inr x"]
by(simp add: d_IN_current_of_bipartite[OF f] ennreal_diff_le_mono_left f'_def split: if_split_asm)
qed simp
have F_leI: "g ∈ Field leq" if f: "f ∈ Field leq" and le: "⋀e. g e ≤ f e"
and nonneg: "⋀e. 0 ≤ g e" and IN_OUT: "⋀x. x ∉ B Γ ⟹ d_IN g x ≤ d_OUT g x"
and link: "linkage Γ g"
for f g
proof
show "g e = 0" if "e ∉ ❙E" for e using nonneg[of e] F_outside[OF f that] le[of e] by simp
show "d_IN g a = 0" if "a ∈ A Γ" for a
using d_IN_mono[of g a f, OF le] F_IN[OF f that] by auto
show "d_OUT g b = 0" if "b ∈ B Γ" for b
using d_OUT_mono[of g b f, OF le] F_OUT[OF f that] by auto
show "d_OUT g x ≤ weight Γ x" for x
using d_OUT_mono[of g x f, OF le] F_weight_OUT[OF f] by(rule order_trans)
show "d_IN g x ≤ weight Γ x" for x
using d_IN_mono[of g x f, OF le] F_weight_IN[OF f] by(rule order_trans)
show "g ≤ f'" using order_trans[OF le F_le[OF f]] by(auto simp add: le_fun_def)
qed(blast intro: IN_OUT link nonneg)+
have chain_Field: "Inf M ∈ F" if M: "M ∈ Chains leq" and nempty: "M ≠ {}" for M
proof -
from nempty obtain g0 where g0_in_M: "g0 ∈ M" by auto
with M have g0: "g0 ∈ Field leq" by(rule Chains_FieldD)
from M have "M ∈ Chains {(g, g'). g' ≤ g}"
by(rule mono_Chains[THEN subsetD, rotated])(auto simp add: leq_def in_restrict_rel_iff)
then have "Complete_Partial_Order.chain (≥) M" by(rule Chains_into_chain)
hence chain': "Complete_Partial_Order.chain (≤) M" by(simp add: chain_dual)
have "support_flow f' ⊆ ❙E" using F_outside[OF f'] by(auto intro: ccontr simp add: support_flow.simps)
then have countable': "countable (support_flow f')"
by(rule countable_subset)(simp add: E_bipartite_web countable "❙V_def")
have finite_OUT: "d_OUT f' x ≠ ⊤" for x using weight_finite[of x]
by(rule neq_top_trans)(rule F_weight_OUT[OF f'])
have finite_IN: "d_IN f' x ≠ ⊤" for x using weight_finite[of x]
by(rule neq_top_trans)(rule F_weight_IN[OF f'])
have OUT_M: "d_OUT (Inf M) x = (INF g∈M. d_OUT g x)" for x using chain' nempty countable' _ finite_OUT
by(rule d_OUT_Inf)(auto dest!: Chains_FieldD[OF M] simp add: leq_def F_nonneg F_le)
have IN_M: "d_IN (Inf M) x = (INF g∈M. d_IN g x)" for x using chain' nempty countable' _ finite_IN
by(rule d_IN_Inf)(auto dest!: Chains_FieldD[OF M] simp add: leq_def F_nonneg F_le)
show "Inf M ∈ F" using g0 unfolding F[symmetric]
proof(rule F_leI)
show "(Inf M) e ≤ g0 e" for e using g0_in_M by(auto intro: INF_lower)
show "0 ≤ (Inf M) e" for e by(auto intro!: INF_greatest dest: F_nonneg dest!: Chains_FieldD[OF M])
show "d_IN (Inf M) x ≤ d_OUT (Inf M) x" if "x ∉ B Γ" for x using that
by(auto simp add: IN_M OUT_M intro!: INF_mono dest: Chains_FieldD[OF M] intro: F_IN_OUT[OF _ that])
show "linkage Γ (Inf M)" using nempty
by(simp add: linkage.simps OUT_M F_link[THEN linkageD] Chains_FieldD[OF M] cong: INF_cong)
qed
qed
let ?P = "λg z. z ∉ A Γ ∧ z ∉ B Γ ∧ d_OUT g z > d_IN g z"
define link
where "link g =
(if ∃z. ?P g z then
let z = SOME z. ?P g z; factor = d_IN g z / d_OUT g z
in (λ(x, y). (if x = z then factor else 1) * g (x, y))
else g)" for g
have increasing: "link g ≤ g ∧ link g ∈ Field leq" if g: "g ∈ Field leq" for g
proof(cases "∃z. ?P g z")
case False
thus ?thesis using that by(auto simp add: link_def leq_def)
next
case True
define z where "z = Eps (?P g)"
from True have "?P g z" unfolding z_def by(rule someI_ex)
hence A: "z ∉ A Γ" and B: "z ∉ B Γ" and less: "d_IN g z < d_OUT g z" by simp_all
let ?factor = "d_IN g z / d_OUT g z"
have link [simp]: "link g (x, y) = (if x = z then ?factor else 1) * g (x, y)" for x y
using True by(auto simp add: link_def z_def Let_def)
have "?factor ≤ 1" (is "?factor ≤ _") using less
by(cases "d_OUT g z" "d_IN g z" rule: ennreal2_cases) (simp_all add: ennreal_less_iff divide_ennreal)
hence le': "?factor * g (x, y) ≤ 1 * g (x, y)" for y x
by(rule mult_right_mono)(simp add: F_nonneg[OF g])
hence le: "link g e ≤ g e" for e by(cases e)simp
have "link g ∈ Field leq" using g le
proof(rule F_leI)
show nonneg: "0 ≤ link g e" for e
using F_nonneg[OF g, of e] by(cases e) simp
show "linkage Γ (link g)" using that A F_link[OF g] by(clarsimp simp add: linkage.simps d_OUT_def)
fix x
assume x: "x ∉ B Γ"
have "d_IN (link g) x ≤ d_IN g x" unfolding d_IN_def using le' by(auto intro: nn_integral_mono)
also have "… ≤ d_OUT (link g) x"
proof(cases "x = z")
case True
have "d_IN g x = d_OUT (link g) x" unfolding d_OUT_def
using True F_weight_IN[OF g, of x] F_IN_OUT[OF g x] F_finite_OUT F_finite_OUT[OF g, of x]
by(cases "d_OUT g z = 0")
(auto simp add: nn_integral_divide nn_integral_cmult d_OUT_def[symmetric] ennreal_divide_times less_top)
thus ?thesis by simp
next
case False
have "d_IN g x ≤ d_OUT g x" using x by(rule F_IN_OUT[OF g])
also have "… ≤ d_OUT (link g) x" unfolding d_OUT_def using False by(auto intro!: nn_integral_mono)
finally show ?thesis .
qed
finally show "d_IN (link g) x ≤ d_OUT (link g) x" .
qed
with le g show ?thesis unfolding F by(simp add: leq_def le_fun_def del: link)
qed
have "bourbaki_witt_fixpoint Inf leq link" using chain_Field increasing unfolding leq_def
by(intro bourbaki_witt_fixpoint_restrict_rel)(auto intro: Inf_greatest Inf_lower)
then interpret bourbaki_witt_fixpoint Inf leq link .
define g where "g = fixp_above f'"
have g: "g ∈ Field leq" using f' unfolding g_def by(rule fixp_above_Field)
hence "linkage Γ g" by(rule F_link)
moreover
have "web_flow Γ g"
proof(intro web_flow.intros current.intros)
show "d_OUT g x ≤ weight Γ x" for x using g by(rule F_weight_OUT)
show "d_IN g x ≤ weight Γ x" for x using g by(rule F_weight_IN)
show "d_IN g x = 0" if "x ∈ A Γ" for x using g that by(rule F_IN)
show B: "d_OUT g x = 0" if "x ∈ B Γ" for x using g that by(rule F_OUT)
show "g e = 0" if "e ∉ ❙E" for e using g that by(rule F_outside)
show KIR: "KIR g x" if A: "x ∉ A Γ" and B: "x ∉ B Γ" for x
proof(rule ccontr)
define z where "z = Eps (?P g)"
assume "¬ KIR g x"
with F_IN_OUT[OF g B] have "d_OUT g x > d_IN g x" by simp
with A B have Ex: "∃x. ?P g x" by blast
then have "?P g z" unfolding z_def by(rule someI_ex)
hence A: "z ∉ A Γ" and B: "z ∉ B Γ" and less: "d_IN g z < d_OUT g z" by simp_all
let ?factor = "d_IN g z / d_OUT g z"
have "∃y. edge Γ z y ∧ g (z, y) > 0"
proof(rule ccontr)
assume "¬ ?thesis"
hence "d_OUT g z = 0" using F_outside[OF g]
by(force simp add: d_OUT_def nn_integral_0_iff_AE AE_count_space not_less)
with less show False by simp
qed
then obtain y where y: "edge Γ z y" and gr0: "g (z, y) > 0" by blast
have "?factor < 1" (is "?factor < _") using less
by(cases "d_OUT g z" "d_IN g z" rule: ennreal2_cases)
(auto simp add: ennreal_less_iff divide_ennreal)
hence le': "?factor * g (z, y) < 1 * g (z, y)" using gr0 F_finite[OF g]
by(intro ennreal_mult_strict_right_mono) (auto simp: less_top)
hence "link g (z, y) ≠ g (z, y)" using Ex by(auto simp add: link_def z_def Let_def)
hence "link g ≠ g" by(auto simp add: fun_eq_iff)
moreover have "link g = g" using f' unfolding g_def by(rule fixp_above_unfold[symmetric])
ultimately show False by contradiction
qed
show "d_OUT g x ≤ d_IN g x" if "x ∉ A Γ" for x using KIR[of x] that B[of x]
by(cases "x ∈ B Γ") auto
qed
ultimately show ?thesis by blast
qed
end
subsection ‹Extending a wave by a linkage›
lemma linkage_quotient_webD:
fixes Γ :: "('v, 'more) web_scheme" (structure) and h g
defines "k ≡ plus_current h g"
assumes f: "current Γ f"
and w: "wave Γ f"
and wg: "web_flow (quotient_web Γ f) g" (is "web_flow ?Γ _")
and link: "linkage (quotient_web Γ f) g"
and trim: "trimming Γ f h"
shows "web_flow Γ k"
and "orthogonal_current Γ k (ℰ (TER f))"
proof -
from wg have g: "current ?Γ g" by(rule web_flowD_current)
from trim obtain h: "current Γ h" and w': "wave Γ h" and h_le_f: "⋀e. h e ≤ f e"
and KIR: "⋀x. ⟦x ∈ RF⇧∘ (TER f); x ∉ A Γ⟧ ⟹ KIR h x"
and TER: "TER h ⊇ ℰ (TER f) - A Γ"
by(cases)(auto simp add: le_fun_def)
have eq: "quotient_web Γ f = quotient_web Γ h" using w trim by(rule quotient_web_trimming)
let ?T = "ℰ (TER f)"
have RFc: "RF⇧∘ (TER h) = RF⇧∘ (TER f)"
by(subst (1 2) roofed_circ_essential[symmetric])(simp only: trimming_ℰ[OF w trim])
have OUT_k: "d_OUT k x = (if x ∈ RF⇧∘ (TER f) then d_OUT h x else d_OUT g x)" for x
using OUT_plus_current[OF h w', of g] web_flowD_current[OF wg] unfolding eq k_def RFc by simp
have RF: "RF (TER h) = RF (TER f)"
by(subst (1 2) RF_essential[symmetric])(simp only: trimming_ℰ[OF w trim])
have IN_k: "d_IN k x = (if x ∈ RF (TER f) then d_IN h x else d_IN g x)" for x
using IN_plus_current[OF h w', of g] web_flowD_current[OF wg] unfolding eq k_def RF by simp
have k: "current Γ k" unfolding k_def using h w' g unfolding eq by(rule current_plus_current)
then show wk: "web_flow Γ k"
proof(rule web_flow)
fix x
assume "x ∈ ❙V" and A: "x ∉ A Γ" and B: "x ∉ B Γ"
show "KIR k x"
proof(cases "x ∈ ℰ (TER f)")
case False
thus ?thesis using A KIR[of x] web_flowD_KIR[OF wg, of x] B by(auto simp add: OUT_k IN_k roofed_circ_def)
next
case True
with A TER have [simp]: "d_OUT h x = 0" and "d_IN h x ≥ weight Γ x"
by(auto simp add: SINK.simps elim: SAT.cases)
with currentD_weight_IN[OF h, of x] have [simp]: "d_IN h x = weight Γ x" by auto
from linkageD[OF link, of x] True currentD_IN[OF g, of x] B
have "d_OUT g x = weight Γ x" "d_IN g x = 0" by(auto simp add: roofed_circ_def)
thus ?thesis using True by(auto simp add: IN_k OUT_k roofed_circ_def intro: roofed_greaterI)
qed
qed
have h_le_k: "h e ≤ k e" for e unfolding k_def plus_current_def by(rule add_increasing2) simp_all
hence "SAT Γ h ⊆ SAT Γ k" by(rule SAT_mono)
hence SAT: "?T ⊆ SAT Γ k" using TER by(auto simp add: elim!: SAT.cases intro: SAT.intros)
show "orthogonal_current Γ k ?T"
proof(rule orthogonal_current)
show "weight Γ x ≤ d_IN k x" if "x ∈ ?T" "x ∉ A Γ" for x
using subsetD[OF SAT, of x] that by(auto simp add: currentD_SAT[OF k])
next
fix x
assume x: "x ∈ ?T" and A: "x ∈ A Γ" and B: "x ∉ B Γ"
with d_OUT_mono[of h x f, OF h_le_f] have "d_OUT h x = 0" by(auto simp add: SINK.simps)
moreover from linkageD[OF link, of x] x A have "d_OUT g x = weight ?Γ x" by simp
ultimately show "d_OUT k x = weight Γ x" using x A currentD_IN[OF f A] B
by(auto simp add: d_OUT_add roofed_circ_def k_def plus_current_def )
next
fix u v
assume v: "v ∈ RF ?T" and u: "u ∉ RF⇧∘ ?T"
have "h (u, v) ≤ f (u, v)" by(rule h_le_f)
also have "… ≤ d_OUT f u" unfolding d_OUT_def by(rule nn_integral_ge_point) simp
also have "… = 0" using u using RF_essential[of Γ "TER f"]
by(auto simp add: roofed_circ_def SINK.simps intro: waveD_OUT[OF w])
finally have "h (u, v) = 0" by simp
moreover have "g (u, v) = 0" using g v RF_essential[of Γ "TER f"]
by(auto intro: currentD_outside simp add: roofed_circ_def)
ultimately show "k (u, v) = 0" by(simp add: k_def)
qed
qed
context countable_web begin
lemma ex_orthogonal_current':
assumes loose_linkable: "⋀f. ⟦ current Γ f; wave Γ f; loose (quotient_web Γ f) ⟧ ⟹ linkable (quotient_web Γ f)"
shows "∃f S. web_flow Γ f ∧ separating Γ S ∧ orthogonal_current Γ f S"
proof -
from ex_maximal_wave[OF countable]
obtain f where f: "current Γ f"
and w: "wave Γ f"
and maximal: "⋀w. ⟦ current Γ w; wave Γ w; f ≤ w ⟧ ⟹ f = w" by blast
from ex_trimming[OF f w countable weight_finite] obtain h where h: "trimming Γ f h" ..
let ?Γ = "quotient_web Γ f"
interpret Γ: countable_web "?Γ" by(rule countable_web_quotient_web)
have "loose ?Γ" using f w maximal by(rule loose_quotient_web[OF weight_finite])
with f w have "linkable ?Γ" by(rule loose_linkable)
then obtain g where wg: "web_flow ?Γ g" and link: "linkage ?Γ g" by blast
let ?k = "plus_current h g"
have "web_flow Γ ?k" "orthogonal_current Γ ?k (ℰ (TER f))"
by(rule linkage_quotient_webD[OF f w wg link h])+
moreover have "separating Γ (ℰ (TER f))"
using waveD_separating[OF w] by(rule separating_essential)
ultimately show ?thesis by blast
qed
end
subsection ‹From a network to a web›
definition web_of_network :: "('v, 'more) network_scheme ⇒ ('v edge, 'more) web_scheme"
where
"web_of_network Δ =
⦇edge = λ(x, y) (y', z). y' = y ∧ edge Δ x y ∧ edge Δ y z,
weight = capacity Δ,
A = {(source Δ, x)|x. edge Δ (source Δ) x},
B = {(x, sink Δ)|x. edge Δ x (sink Δ)},
… = network.more Δ⦈"
lemma web_of_network_sel [simp]:
fixes Δ (structure) shows
"edge (web_of_network Δ) e e' ⟷ e ∈ ❙E ∧ e' ∈ ❙E ∧ snd e = fst e'"
"weight (web_of_network Δ) e = capacity Δ e"
"A (web_of_network Δ) = {(source Δ, x)|x. edge Δ (source Δ) x}"
"B (web_of_network Δ) = {(x, sink Δ)|x. edge Δ x (sink Δ)}"
by(auto simp add: web_of_network_def split: prod.split)
lemma vertex_web_of_network [simp]:
"vertex (web_of_network Δ) (x, y) ⟷ edge Δ x y ∧ (∃z. edge Δ y z ∨ edge Δ z x)"
by(auto simp add: vertex_def Domainp.simps Rangep.simps)
definition flow_of_current :: "('v, 'more) network_scheme ⇒ 'v edge current ⇒ 'v flow"
where "flow_of_current Δ f e = max (d_OUT f e) (d_IN f e)"
lemma flow_flow_of_current:
fixes Δ (structure) and Γ
defines [simp]: "Γ ≡ web_of_network Δ"
assumes fw: "web_flow Γ f"
shows "flow Δ (flow_of_current Δ f)" (is "flow _ ?f")
proof
from fw have f: "current Γ f" and KIR: "⋀x. ⟦ x ∉ A Γ; x ∉ B Γ ⟧ ⟹ KIR f x"
by(auto 4 3 dest: web_flowD_current web_flowD_KIR)
show "?f e ≤ capacity Δ e" for e
using currentD_weight_OUT[OF f, of e] currentD_weight_IN[OF f, of e]
by(simp add: flow_of_current_def)
fix x
assume x: "x ≠ source Δ" "x ≠ sink Δ"
have "d_OUT ?f x = (∑⇧+ y. d_IN f (x, y))" unfolding d_OUT_def
by(simp add: flow_of_current_def max_absorb2 currentD_OUT_IN[OF f] x)
also have "… = (∑⇧+ y. ∑⇧+ e∈range (λz. (z, x)). f (e, x, y))"
by(auto simp add: nn_integral_count_space_indicator d_IN_def intro!: nn_integral_cong currentD_outside[OF f] split: split_indicator)
also have "… = (∑⇧+ z∈UNIV. ∑⇧+ y. f ((z, x), x, y))"
by(subst nn_integral_snd_count_space[of "case_prod _", simplified])
(simp add: nn_integral_count_space_reindex nn_integral_fst_count_space[of "case_prod _", simplified])
also have "… = (∑⇧+ z. ∑⇧+ e∈range (Pair x). f ((z, x), e))"
by(simp add: nn_integral_count_space_reindex)
also have "… = (∑⇧+ z. d_OUT f (z, x))"
by(auto intro!: nn_integral_cong currentD_outside[OF f] simp add: d_OUT_def nn_integral_count_space_indicator split: split_indicator)
also have "… = (∑⇧+ z∈{z. edge Δ z x}. d_OUT f (z, x))"
by(auto intro!: nn_integral_cong currentD_outside_OUT[OF f] simp add: nn_integral_count_space_indicator split: split_indicator)
also have "… = (∑⇧+ z∈{z. edge Δ z x}. max (d_OUT f (z, x)) (d_IN f (z, x)))"
proof(rule nn_integral_cong)
show "d_OUT f (z, x) = max (d_OUT f (z, x)) (d_IN f (z, x))"
if "z ∈ space (count_space {z. edge Δ z x})" for z using currentD_IN[OF f] that
by(cases "z = source Δ")(simp_all add: max_absorb1 currentD_IN[OF f] KIR x)
qed
also have "… = (∑⇧+ z. max (d_OUT f (z, x)) (d_IN f (z, x)))"
by(auto intro!: nn_integral_cong currentD_outside_OUT[OF f] currentD_outside_IN[OF f] simp add: nn_integral_count_space_indicator max_def split: split_indicator)
also have "… = d_IN ?f x" by(simp add: flow_of_current_def d_IN_def)
finally show "KIR ?f x" .
qed
text ‹
The reduction of Conjecture 1.2 to Conjecture 3.6 is flawed in \<^cite>‹"AharoniBergerGeorgakopoulusPerlsteinSpruessel2011JCT"›.
Not every essential A-B separating set of vertices in @{term "web_of_network Δ"} is an s-t-cut in
@{term Δ}, as the following counterexample shows.
The network @{term Δ} has five nodes @{term "s"}, @{term "t"}, @{term "x"}, @{term "y"} and @{term "z"}
and edges @{term "(s, x)"}, @{term "(x, y)"}, @{term "(y, z)"}, @{term "(y, t)"} and @{term "(z, t)"}.
For @{term "web_of_network Δ"}, the set @{term "S = {(x, y), (y, z)}"} is essential and A-B separating.
(@{term "(x, y)"} is essential due to the path @{term "[(y, z)]"} and @{term "(y, z)"} is essential
due to the path @{term "[(z, t)]"}). However, @{term S} is not a cut in @{term Δ} because the node @{term y}
has an outgoing edge that is in @{term S} and one that is not in @{term S}.
However, this can be remedied if all edges carry positive capacity. Then, orthogonality of the current
rules out the above possibility.
›
lemma cut_RF_separating:
fixes Δ (structure)
assumes sep: "separating_network Δ V"
and sink: "sink Δ ∉ V"
shows "cut Δ (RF⇧N V)"
proof
show "source Δ ∈ RF⇧N V" by(rule roofedI)(auto dest: separatingD[OF sep])
show "sink Δ ∉ RF⇧N V" using sink by(auto dest: roofedD[OF _ rtrancl_path.base])
qed
context
fixes Δ :: "('v, 'more) network_scheme" and Γ (structure)
defines Γ_def: "Γ ≡ web_of_network Δ"
begin
lemma separating_network_cut_of_sep:
assumes sep: "separating Γ S"
and source_sink: "source Δ ≠ sink Δ"
shows "separating_network Δ (fst ` ℰ S)"
proof
define s t where "s = source Δ" and "t = sink Δ"
fix p
assume p: "path Δ s p t"
with p source_sink have "p ≠ []" by cases(auto simp add: s_def t_def)
with p have p': "path Γ (s, hd p) (zip p (tl p)) (last (s # butlast p), t)"
proof(induction)
case (step x y p z)
then show ?case by(cases p)(auto elim: rtrancl_path.cases intro: rtrancl_path.intros simp add: Γ_def)
qed simp
from sep have "separating Γ (ℰ S)" by(rule separating_essential)
from this p' have "(∃z∈set (zip p (tl p)). z ∈ ℰ S) ∨ (s, hd p) ∈ ℰ S"
apply(rule separatingD)
using rtrancl_path_nth[OF p, of 0] rtrancl_path_nth[OF p, of "length p - 1"] ‹p ≠ []› rtrancl_path_last[OF p]
apply(auto simp add: Γ_def s_def t_def hd_conv_nth last_conv_nth nth_butlast nth_Cons' cong: if_cong split: if_split_asm)
apply(metis One_nat_def Suc_leI cancel_comm_monoid_add_class.diff_cancel le_antisym length_butlast length_greater_0_conv list.size(3))+
done
then show "(∃z∈set p. z ∈ fst ` ℰ S) ∨ s ∈ fst ` ℰ S"
by(auto dest!: set_zip_leftD intro: rev_image_eqI)
qed
definition cut_of_sep :: "('v × 'v) set ⇒ 'v set"
where "cut_of_sep S = RF⇧N⇘Δ⇙ (fst ` ℰ S)"
lemma separating_cut:
assumes sep: "separating Γ S"
and neq: "source Δ ≠ sink Δ"
and sink_out: "⋀x. ¬ edge Δ (sink Δ) x"
shows "cut Δ (cut_of_sep S)"
unfolding cut_of_sep_def
proof(rule cut_RF_separating)
show "separating_network Δ (fst ` ℰ S)" using sep neq by(rule separating_network_cut_of_sep)
show "sink Δ ∉ fst ` ℰ S"
proof
assume "sink Δ ∈ fst ` ℰ S"
then obtain x where "(sink Δ, x) ∈ ℰ S" by auto
hence "(sink Δ, x) ∈ ❙V" by(auto simp add: Γ_def dest!: essential_vertex)
then show False by(simp add: Γ_def sink_out)
qed
qed
context
fixes f :: "'v edge current" and S
assumes wf: "web_flow Γ f"
and ortho: "orthogonal_current Γ f S"
and sep: "separating Γ S"
and capacity_pos: "⋀e. e ∈ ❙E⇘Δ⇙ ⟹ capacity Δ e > 0"
begin
private lemma f: "current Γ f" using wf by(rule web_flowD_current)
lemma orthogonal_leave_RF:
assumes e: "edge Δ x y"
and x: "x ∈ (cut_of_sep S)"
and y: "y ∉ (cut_of_sep S)"
shows "(x, y) ∈ S"
proof -
from y obtain p where p: "path Δ y p (sink Δ)" and y': "y ∉ fst ` ℰ S"
and bypass: "⋀z. z ∈ set p ⟹ z ∉ fst ` ℰ S" by(auto simp add: roofed_def cut_of_sep_def Γ_def[symmetric])
from e p have p': "path Δ x (y # p) (sink Δ)" ..
from roofedD[OF x[unfolded cut_of_sep_def] this] y' bypass have "x ∈ fst ` ℰ S" by(auto simp add: Γ_def[symmetric])
then obtain z where xz: "(x, z) ∈ ℰ S" by auto
then obtain q b where q: "path Γ (x, z) q b" and b: "b ∈ B Γ"
and distinct: "distinct ((x, z) # q)" and bypass': "⋀z. z ∈ set q ⟹ z ∉ RF S"
by(rule ℰ_E_RF) blast
define p' where "p' = y # p"
hence "p' ≠ []" by simp
with p' have "path Γ (x, hd p') (zip p' (tl p')) (last (x # butlast p'), sink Δ)"
unfolding p'_def[symmetric]
proof(induction)
case (step x y p z)
then show ?case
by(cases p)(auto elim: rtrancl_path.cases intro: rtrancl_path.intros simp add: Γ_def)
qed simp
then have p'': "path Γ (x, y) (zip (y # p) p) (last (x # butlast (y # p)), sink Δ)" (is "path _ ?y ?p ?t")
by(simp add: p'_def)
have "(?y # ?p) ! length p = ?t" using rtrancl_path_last[OF p'] p rtrancl_path_last[OF p]
apply(auto split: if_split_asm simp add: nth_Cons butlast_conv_take take_Suc_conv_app_nth split: nat.split elim: rtrancl_path.cases)
apply(simp add: last_conv_nth)
done
moreover have "length p < length (?y # ?p)" by simp
ultimately have t: "?t ∈ B Γ" using rtrancl_path_nth[OF p'', of "length p - 1"] e
by(cases p)(simp_all add: Γ_def split: if_split_asm)
show S: "(x, y) ∈ S"
proof(cases "x = source Δ")
case True
from separatingD[OF separating_essential, OF sep p'' _ t] e True
consider (z) z z' where "(z, z') ∈ set ?p" "(z, z') ∈ ℰ S" | "(x, y) ∈ S" by(auto simp add: Γ_def)
thus ?thesis
proof cases
case (z z)
hence "z ∈ set p" "z ∈ fst ` ℰ S"
using y' by(auto dest!: set_zip_leftD intro: rev_image_eqI)
hence False by(auto dest: bypass)
thus ?thesis ..
qed
next
case False
have "∃e. edge Γ e (x, z) ∧ f (e, (x, z)) > 0"
proof(rule ccontr)
assume "¬ ?thesis"
then have "d_IN f (x, z) = 0" unfolding d_IN_def using currentD_outside[OF f, of _ "(x, z)"]
by(force simp add: nn_integral_0_iff_AE AE_count_space not_less)
moreover
from xz have "(x, z) ∈ S" by auto
hence "(x, z) ∈ SAT Γ f" by(rule orthogonal_currentD_SAT[OF ortho])
with False have "d_IN f (x, z) ≥ capacity Δ (x, z)" by(auto simp add: SAT.simps Γ_def)
ultimately have "¬ capacity Δ (x, z) > 0" by auto
hence "¬ edge Δ x z" using capacity_pos[of "(x, z)"] by auto
moreover with q have "b = (x, z)" by cases(auto simp add: Γ_def)
with b have "edge Δ x z" by(simp add: Γ_def)
ultimately show False by contradiction
qed
then obtain u where ux: "edge Δ u x" and xz': "edge Δ x z" and uxz: "edge Γ (u, x) (x, z)"
and gt0: "f ((u, x), (x, z)) > 0" by(auto simp add: Γ_def)
have "(u, x) ∈ RF⇧∘ S" using orthogonal_currentD_in[OF ortho, of "(x, z)" "(u, x)"] gt0 xz
by(fastforce intro: roofed_greaterI)
hence ux_RF: "(u, x) ∈ RF (ℰ S)" and ux_ℰ: "(u, x) ∉ ℰ S" unfolding RF_essential by(simp_all add: roofed_circ_def)
from ux e have "edge Γ (u, x) (x, y)" by(simp add: Γ_def)
hence "path Γ (u, x) ((x, y) # ?p) ?t" using p'' ..
from roofedD[OF ux_RF this t] ux_ℰ
consider "(x, y) ∈ S" | (z) z z' where "(z, z') ∈ set ?p" "(z, z') ∈ ℰ S" by auto
thus ?thesis
proof cases
case (z z)
with bypass[of z] y' have False by(fastforce dest!: set_zip_leftD intro: rev_image_eqI)
thus ?thesis ..
qed
qed
qed
lemma orthogonal_flow_of_current:
assumes source_sink: "source Δ ≠ sink Δ"
and sink_out: "⋀x. ¬ edge Δ (sink Δ) x"
and no_direct_edge: "¬ edge Δ (source Δ) (sink Δ)"
shows "orthogonal Δ (flow_of_current Δ f) (cut_of_sep S)" (is "orthogonal _ ?f ?S")
proof
fix x y
assume e: "edge Δ x y" and "x ∈ ?S" and "y ∉ ?S"
then have S: "(x, y) ∈ S"by(rule orthogonal_leave_RF)
show "?f (x, y) = capacity Δ (x, y)"
proof(cases "x = source Δ")
case False
with orthogonal_currentD_SAT[OF ortho S]
have "weight Γ (x, y) ≤ d_IN f (x, y)" by cases(simp_all add: Γ_def)
with False currentD_OUT_IN[OF f, of "(x, y)"] currentD_weight_IN[OF f, of "(x, y)"]
show ?thesis by(simp add: flow_of_current_def Γ_def max_def)
next
case True
with orthogonal_currentD_A[OF ortho S] e currentD_weight_IN[OF f, of "(x, y)"] no_direct_edge
show ?thesis by(auto simp add: flow_of_current_def Γ_def max_def)
qed
next
from sep source_sink sink_out have cut: "cut Δ ?S" by(rule separating_cut)
fix x y
assume xy: "edge Δ x y"
and x: "x ∉ ?S"
and y: "y ∈ ?S"
from x obtain p where p: "path Δ x p (sink Δ)" and x': "x ∉ fst ` ℰ S"
and bypass: "⋀z. z ∈ set p ⟹ z ∉ fst ` ℰ S" by(auto simp add: roofed_def cut_of_sep_def)
have source: "x ≠ source Δ"
proof
assume "x = source Δ"
have "separating_network Δ (fst ` ℰ S)" using sep source_sink by(rule separating_network_cut_of_sep)
from separatingD[OF this p] ‹x = source Δ› x show False
by(auto dest: bypass intro: roofed_greaterI simp add: cut_of_sep_def)
qed
hence A: "(x, y) ∉ A Γ" by(simp add: Γ_def)
have "f ((u, v), x, y) = 0" for u v
proof(cases "edge Γ (u, v) (x, y)")
case False with f show ?thesis by(rule currentD_outside)
next
case True
hence [simp]: "v = x" and ux: "edge Δ u x" by(auto simp add: Γ_def)
have "(x, y) ∈ RF S"
proof
fix q b
assume q: "path Γ (x, y) q b" and b: "b ∈ B Γ"
define xy where "xy = (x, y)"
from q have "path Δ (snd xy) (map snd q) (snd b)" unfolding xy_def[symmetric]
by(induction)(auto intro: rtrancl_path.intros simp add: Γ_def)
with b have "path Δ y (map snd q) (sink Δ)" by(auto simp add: xy_def Γ_def)
from roofedD[OF y[unfolded cut_of_sep_def] this] have "∃z∈set (y # map snd q). z ∈ ?S"
by(auto intro: roofed_greaterI simp add: cut_of_sep_def)
from split_list_last_prop[OF this] obtain xs z ys where decomp: "y # map snd q = xs @ z # ys"
and z: "z ∈ ?S" and last: "⋀z. z ∈ set ys ⟹ z ∉ ?S" by auto
from decomp obtain x' xs' z'' ys' where decomp': "(x', y) # q = xs' @ (z'', z) # ys'"
and "xs = map snd xs'" and ys: "ys = map snd ys'" and x': "xs' = [] ⟹ x' = x"
by(fastforce simp add: Cons_eq_append_conv map_eq_append_conv)
from cut z have z_sink: "z ≠ sink Δ" by cases(auto)
then have "ys' ≠ []" using rtrancl_path_last[OF q] decomp' b x' q
by(auto simp add: Cons_eq_append_conv Γ_def elim: rtrancl_path.cases)
then obtain w z''' ys'' where ys': "ys' = (w, z''') # ys''" by(auto simp add: neq_Nil_conv)
from q[THEN rtrancl_path_nth, of "length xs'"] decomp' ys' x' have "edge Γ (z'', z) (w, z''')"
by(auto simp add: Cons_eq_append_conv nth_append)
hence w: "w = z" and zz''': "edge Δ z z'''" by(auto simp add: Γ_def)
from ys' ys last[of z'''] have "z''' ∉ ?S" by simp
with zz''' z have "(z, z''') ∈ S" by(rule orthogonal_leave_RF)
moreover have "(z, z''') ∈ set q" using decomp' ys' w by(auto simp add: Cons_eq_append_conv)
ultimately show "(∃z∈set q. z ∈ S) ∨ (x, y) ∈ S" by blast
qed
moreover
have "(u, x) ∉ RF⇧∘ S"
proof
assume "(u, x) ∈ RF⇧∘ S"
hence ux_RF: "(u, x) ∈ RF (ℰ S)" and ux_ℰ: "(u, x) ∉ ℰ S"
unfolding RF_essential by(simp_all add: roofed_circ_def)
have "x ≠ sink Δ" using p xy by cases(auto simp add: sink_out)
with p have nNil: "p ≠ []" by(auto elim: rtrancl_path.cases)
with p have "edge Δ x (hd p)" by cases auto
with ux have "edge Γ (u, x) (x, hd p)" by(simp add: Γ_def)
moreover
from p nNil have "path Γ (x, hd p) (zip p (tl p)) (last (x # butlast p), sink Δ)" (is "path _ ?x ?p ?t")
proof(induction)
case (step x y p z)
then show ?case
by(cases p)(auto elim: rtrancl_path.cases intro: rtrancl_path.intros simp add: Γ_def)
qed simp
ultimately have p': "path Γ (u, x) (?x # ?p) ?t" ..
have "(?x # ?p) ! (length p - 1) = ?t" using rtrancl_path_last[OF p] p nNil
apply(auto split: if_split_asm simp add: nth_Cons butlast_conv_take take_Suc_conv_app_nth not_le split: nat.split elim: rtrancl_path.cases)
apply(simp add: last_conv_nth nth_tl)
done
moreover have "length p - 1 < length (?x # ?p)" by simp
ultimately have t: "?t ∈ B Γ" using rtrancl_path_nth[OF p', of "length p - 1"]
by(cases p)(simp_all add: Γ_def split: if_split_asm)
from roofedD[OF ux_RF p' t] ux_ℰ consider (X) "(x, hd p) ∈ ℰ S"
| (z) z z' where "(z, z') ∈ set (zip p (tl p))" "(z, z') ∈ ℰ S" by auto
thus False
proof cases
case X with x' show False by(auto simp add: cut_of_sep_def intro: rev_image_eqI)
next
case (z z)
with bypass[of z] show False by(auto 4 3 simp add: cut_of_sep_def intro: rev_image_eqI dest!: set_zip_leftD)
qed
qed
ultimately show ?thesis unfolding ‹v = x› by(rule orthogonal_currentD_in[OF ortho])
qed
then have "d_IN f (x, y) = 0" unfolding d_IN_def
by(simp add: nn_integral_0_iff emeasure_count_space_eq_0)
with currentD_OUT_IN[OF f A] show "flow_of_current Δ f (x, y) = 0"
by(simp add: flow_of_current_def max_def)
qed
end
end
subsection ‹Avoiding antiparallel edges and self-loops›
context antiparallel_edges begin
abbreviation cut' :: "'a vertex set ⇒ 'a set" where "cut' S ≡ Vertex -` S"
lemma cut_cut': "cut Δ'' S ⟹ cut Δ (cut' S)"
by(auto simp add: cut.simps)
lemma IN_Edge: "❙I❙N⇘Δ''⇙ (Edge x y) = (if edge Δ x y then {Vertex x} else {})"
by(auto simp add: incoming_def)
lemma OUT_Edge: "❙O❙U❙T⇘Δ''⇙ (Edge x y) = (if edge Δ x y then {Vertex y} else {})"
by(auto simp add: outgoing_def)
interpretation Δ'': countable_network Δ'' by(rule Δ''_countable_network)
lemma d_IN_Edge:
assumes f: "flow Δ'' f"
shows "d_IN f (Edge x y) = f (Vertex x, Edge x y)"
by(subst d_IN_alt_def[OF Δ''.flowD_outside[OF f], of _ Δ''])(simp_all add: IN_Edge nn_integral_count_space_indicator max_def Δ''.flowD_outside[OF f])
lemma d_OUT_Edge:
assumes f: "flow Δ'' f"
shows "d_OUT f (Edge x y) = f (Edge x y, Vertex y)"
by(subst d_OUT_alt_def[OF Δ''.flowD_outside[OF f], of _ Δ''])(simp_all add: OUT_Edge nn_integral_count_space_indicator max_def Δ''.flowD_outside[OF f])
lemma orthogonal_cut':
assumes ortho: "orthogonal Δ'' f S"
and f: "flow Δ'' f"
shows "orthogonal Δ (collect f) (cut' S)"
proof
show "collect f (x, y) = capacity Δ (x, y)" if edge: "edge Δ x y" and x: "x ∈ cut' S" and y: "y ∉ cut' S" for x y
proof(cases "Edge x y ∈ S")
case True
from y have "Vertex y ∉ S" by auto
from orthogonalD_out[OF ortho _ True this] edge show ?thesis by simp
next
case False
from x have "Vertex x ∈ S" by auto
from orthogonalD_out[OF ortho _ this False] edge
have "capacity Δ (x, y) = d_IN f (Edge x y)" by(simp add: d_IN_Edge[OF f])
also have "… = d_OUT f (Edge x y)" by(simp add: flowD_KIR[OF f])
also have "… = f (Edge x y, Vertex y)" using edge by(simp add: d_OUT_Edge[OF f])
finally show ?thesis by simp
qed
show "collect f (x, y) = 0" if edge: "edge Δ x y" and x: "x ∉ cut' S" and y: "y ∈ cut' S" for x y
proof(cases "Edge x y ∈ S")
case True
from x have "Vertex x ∉ S" by auto
from orthogonalD_in[OF ortho _ this True] edge have "0 = d_IN f (Edge x y)" by(simp add: d_IN_Edge[OF f])
also have "… = d_OUT f (Edge x y)" by(simp add: flowD_KIR[OF f])
also have "… = f (Edge x y, Vertex y)" using edge by(simp add: d_OUT_Edge[OF f])
finally show ?thesis by simp
next
case False
from y have "Vertex y ∈ S" by auto
from orthogonalD_in[OF ortho _ False this] edge show ?thesis by simp
qed
qed
end
context countable_network begin
lemma countable_web_web_of_network:
assumes source_in: "⋀x. ¬ edge Δ x (source Δ)"
and sink_out: "⋀y. ¬ edge Δ (sink Δ) y"
and undead: "⋀x y. edge Δ x y ⟹ (∃z. edge Δ y z) ∨ (∃z. edge Δ z x)"
and source_sink: "¬ edge Δ (source Δ) (sink Δ)"
and no_loop: "⋀x. ¬ edge Δ x x"
shows "countable_web (web_of_network Δ)" (is "countable_web ?Γ")
proof
show "¬ edge ?Γ y x" if "x ∈ A ?Γ" for x y using that by(clarsimp simp add: source_in)
show "¬ edge ?Γ x y" if "x ∈ B ?Γ" for x y using that by(clarsimp simp add: sink_out)
show "A ?Γ ⊆ ❙V⇘?Γ⇙" by(auto 4 3 dest: undead)
show "A ?Γ ∩ B ?Γ = {}" using source_sink by auto
show "¬ edge ?Γ x x" for x by(auto simp add: no_loop)
show "weight ?Γ x = 0" if "x ∉ ❙V⇘?Γ⇙" for x using that undead
by(cases x)(auto intro!: capacity_outside)
show "weight ?Γ x ≠ ⊤" for x using capacity_finite[of x] by(cases x) simp
have "❙E⇘?Γ⇙ ⊆ ❙E × ❙E" by auto
thus "countable ❙E⇘?Γ⇙" by(rule countable_subset)(simp)
qed
lemma max_flow_min_cut':
assumes ex_orthogonal_current: " ∃f S. web_flow (web_of_network Δ) f ∧ separating (web_of_network Δ) S ∧ orthogonal_current (web_of_network Δ) f S"
and source_in: "⋀x. ¬ edge Δ x (source Δ)"
and sink_out: "⋀y. ¬ edge Δ (sink Δ) y"
and undead: "⋀x y. edge Δ x y ⟹ (∃z. edge Δ y z) ∨ (∃z. edge Δ z x)"
and source_sink: "¬ edge Δ (source Δ) (sink Δ)"
and no_loop: "⋀x. ¬ edge Δ x x"
and capacity_pos: "⋀e. e ∈ ❙E ⟹ capacity Δ e > 0"
shows "∃f S. flow Δ f ∧ cut Δ S ∧ orthogonal Δ f S"
proof -
let ?Γ = "web_of_network Δ"
from ex_orthogonal_current obtain f S
where f: "web_flow (web_of_network Δ) f"
and S: "separating (web_of_network Δ) S"
and ortho: "orthogonal_current (web_of_network Δ) f S" by blast+
let ?f = "flow_of_current Δ f" and ?S = "cut_of_sep Δ S"
from f have "flow Δ ?f" by(rule flow_flow_of_current)
moreover have "cut Δ ?S" using S source_neq_sink sink_out by(rule separating_cut)
moreover have "orthogonal Δ ?f ?S" using f ortho S capacity_pos source_neq_sink sink_out source_sink
by(rule orthogonal_flow_of_current)
ultimately show ?thesis by blast
qed
subsection ‹Eliminating zero edges and incoming edges to @{term source} and outgoing edges of @{term sink}›
definition Δ''' :: "'v network" where "Δ''' =
⦇edge = λx y. edge Δ x y ∧ capacity Δ (x, y) > 0 ∧ y ≠ source Δ ∧ x ≠ sink Δ,
capacity = λ(x, y). if x = sink Δ ∨ y = source Δ then 0 else capacity Δ (x, y),
source = source Δ,
sink = sink Δ⦈"
lemma Δ'''_sel [simp]:
"edge Δ''' x y ⟷ edge Δ x y ∧ capacity Δ (x, y) > 0 ∧ y ≠ source Δ ∧ x ≠ sink Δ"
"capacity Δ''' (x, y) = (if x = sink Δ ∨ y = source Δ then 0 else capacity Δ (x, y))"
"source Δ''' = source Δ"
"sink Δ''' = sink Δ"
for x y by(simp_all add: Δ'''_def)
lemma Δ'''_countable_network: "countable_network Δ'''"
proof(unfold_locales)
have "❙E⇘Δ'''⇙ ⊆ ❙E" by auto
then show "countable ❙E⇘Δ'''⇙" by(rule countable_subset) simp
show "capacity Δ''' e = 0" if "e ∉ ❙E⇘Δ'''⇙" for e
using capacity_outside[of e] that by(auto split: if_split_asm intro: ccontr)
qed(auto simp add: split: if_split_asm)
lemma flow_Δ''':
assumes f: "flow Δ''' f" and cut: "cut Δ''' S" and ortho: "orthogonal Δ''' f S"
shows "flow Δ f" "cut Δ S" "orthogonal Δ f S"
proof -
interpret Δ''': countable_network Δ''' by(rule Δ'''_countable_network)
show "flow Δ f"
proof
show "f e ≤ capacity Δ e" for e using flowD_capacity[OF f, of e]
by(cases e)(simp split: if_split_asm)
show "KIR f x" if "x ≠ source Δ" "x ≠ sink Δ" for x using flowD_KIR[OF f, of x] that by simp
qed
show "cut Δ S" using cut by(simp add: cut.simps)
show "orthogonal Δ f S"
proof
show "f (x, y) = capacity Δ (x, y)" if edge: "edge Δ x y" and x: "x ∈ S" and y: "y ∉ S" for x y
proof(cases "edge Δ''' x y")
case True
with orthogonalD_out[OF ortho this x y] show ?thesis by simp
next
case False
from cut y x have xy: "y ≠ source Δ ∧ x ≠ sink Δ" by(cases) auto
with xy edge False have "capacity Δ (x, y) = 0" by simp
with Δ'''.flowD_outside[OF f, of "(x, y)"] False show ?thesis by simp
qed
show "f (x, y) = 0" if edge: "edge Δ x y" and x: "x ∉ S" and y: "y ∈ S" for x y
using orthogonalD_in[OF ortho _ x y] Δ'''.flowD_outside[OF f, of "(x, y)"]
by(cases "edge Δ''' x y")simp_all
qed
qed
end
end