Theory MFMC_Web
theory MFMC_Web imports
MFMC_Network
begin
section ‹Webs and currents›
record 'v web = "'v graph" +
weight :: "'v ⇒ ennreal"
A :: "'v set"
B :: "'v set"
lemma vertex_weight_update [simp]: "vertex (weight_update f Γ) = vertex Γ"
by(simp add: vertex_def fun_eq_iff)
type_synonym 'v current = "'v edge ⇒ ennreal"
inductive current :: "('v, 'more) web_scheme ⇒ 'v current ⇒ bool"
for Γ f
where
current:
"⟦ ⋀x. d_OUT f x ≤ weight Γ x;
⋀x. d_IN f x ≤ weight Γ x;
⋀x. x ∉ A Γ ⟹ d_OUT f x ≤ d_IN f x;
⋀a. a ∈ A Γ ⟹ d_IN f a = 0;
⋀b. b ∈ B Γ ⟹ d_OUT f b = 0;
⋀e. e ∉ ❙E⇘Γ⇙ ⟹ f e = 0 ⟧
⟹ current Γ f"
lemma currentD_weight_OUT: "current Γ f ⟹ d_OUT f x ≤ weight Γ x"
by(simp add: current.simps)
lemma currentD_weight_IN: "current Γ f ⟹ d_IN f x ≤ weight Γ x"
by(simp add: current.simps)
lemma currentD_OUT_IN: "⟦ current Γ f; x ∉ A Γ ⟧ ⟹ d_OUT f x ≤ d_IN f x"
by(simp add: current.simps)
lemma currentD_IN: "⟦ current Γ f; a ∈ A Γ ⟧ ⟹ d_IN f a = 0"
by(simp add: current.simps)
lemma currentD_OUT: "⟦ current Γ f; b ∈ B Γ ⟧ ⟹ d_OUT f b = 0"
by(simp add: current.simps)
lemma currentD_outside: "⟦ current Γ f; ¬ edge Γ x y ⟧ ⟹ f (x, y) = 0"
by(blast elim: current.cases)
lemma currentD_outside': "⟦ current Γ f; e ∉ ❙E⇘Γ⇙ ⟧ ⟹ f e = 0"
by(blast elim: current.cases)
lemma currentD_OUT_eq_0:
assumes "current Γ f"
shows "d_OUT f x = 0 ⟷ (∀y. f (x, y) = 0)"
by(simp add: d_OUT_def nn_integral_0_iff emeasure_count_space_eq_0)
lemma currentD_IN_eq_0:
assumes "current Γ f"
shows "d_IN f x = 0 ⟷ (∀y. f (y, x) = 0)"
by(simp add: d_IN_def nn_integral_0_iff emeasure_count_space_eq_0)
lemma current_support_flow:
fixes Γ (structure)
assumes "current Γ f"
shows "support_flow f ⊆ ❙E"
using currentD_outside[OF assms] by(auto simp add: support_flow.simps intro: ccontr)
lemma currentD_outside_IN: "⟦ current Γ f; x ∉ ❙V⇘Γ⇙ ⟧ ⟹ d_IN f x = 0"
by(auto simp add: d_IN_def vertex_def nn_integral_0_iff AE_count_space emeasure_count_space_eq_0 dest: currentD_outside)
lemma currentD_outside_OUT: "⟦ current Γ f; x ∉ ❙V⇘Γ⇙ ⟧ ⟹ d_OUT f x = 0"
by(auto simp add: d_OUT_def vertex_def nn_integral_0_iff AE_count_space emeasure_count_space_eq_0 dest: currentD_outside)
lemma currentD_weight_in: "current Γ h ⟹ h (x, y) ≤ weight Γ y"
by (metis order_trans d_IN_ge_point currentD_weight_IN)
lemma currentD_weight_out: "current Γ h ⟹ h (x, y) ≤ weight Γ x"
by (metis order_trans d_OUT_ge_point currentD_weight_OUT)
lemma current_leI:
fixes Γ (structure)
assumes f: "current Γ f"
and le: "⋀e. g e ≤ f e"
and OUT_IN: "⋀x. x ∉ A Γ ⟹ d_OUT g x ≤ d_IN g x"
shows "current Γ g"
proof
show "d_OUT g x ≤ weight Γ x" for x
using d_OUT_mono[of g x f, OF le] currentD_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] currentD_weight_IN[OF f] by(rule order_trans)
show "d_IN g a = 0" if "a ∈ A Γ" for a
using d_IN_mono[of g a f, OF le] currentD_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] currentD_OUT[OF f that] by auto
show "g e = 0" if "e ∉ ❙E" for e
using currentD_outside'[OF f that] le[of e] by simp
qed(blast intro: OUT_IN)+
lemma current_weight_mono:
"⟦ current Γ f; edge Γ = edge Γ'; A Γ = A Γ'; B Γ = B Γ'; ⋀x. weight Γ x ≤ weight Γ' x ⟧
⟹ current Γ' f"
by(auto 4 3 elim!: current.cases intro!: current.intros intro: order_trans)
abbreviation (input) zero_current :: "'v current"
where "zero_current ≡ λ_. 0"
lemma SINK_0 [simp]: "SINK zero_current = UNIV"
by(auto simp add: SINK.simps)
lemma current_0 [simp]: "current Γ zero_current"
by(auto simp add: current.simps)
inductive web_flow :: "('v, 'more) web_scheme ⇒ 'v current ⇒ bool"
for Γ (structure) and f
where
web_flow: "⟦ current Γ f; ⋀x. ⟦ x ∈ ❙V; x ∉ A Γ; x ∉ B Γ ⟧ ⟹ KIR f x ⟧ ⟹ web_flow Γ f"
lemma web_flowD_current: "web_flow Γ f ⟹ current Γ f"
by(erule web_flow.cases)
lemma web_flowD_KIR: "⟦ web_flow Γ f; x ∉ A Γ; x ∉ B Γ ⟧ ⟹ KIR f x"
apply(cases "x ∈ ❙V⇘Γ⇙")
apply(fastforce elim!: web_flow.cases)
apply(auto simp add: vertex_def d_OUT_def d_IN_def elim!: web_flow.cases)
apply(subst (1 2) currentD_outside[of _ f]; auto)
done
subsection ‹Saturated and terminal vertices›
inductive_set SAT :: "('v, 'more) web_scheme ⇒ 'v current ⇒ 'v set"
for Γ f
where
A: "x ∈ A Γ ⟹ x ∈ SAT Γ f"
| IN: "d_IN f x ≥ weight Γ x ⟹ x ∈ SAT Γ f"
lemma SAT_0 [simp]: "SAT Γ zero_current = A Γ ∪ {x. weight Γ x ≤ 0}"
by(auto simp add: SAT.simps)
lemma SAT_mono:
assumes "⋀e. f e ≤ g e"
shows "SAT Γ f ⊆ SAT Γ g"
proof
fix x
assume "x ∈ SAT Γ f"
thus "x ∈ SAT Γ g"
proof cases
case IN
also have "d_IN f x ≤ d_IN g x" using assms by(rule d_IN_mono)
finally show ?thesis ..
qed(rule SAT.A)
qed
lemma SAT_Sup_upper: "f ∈ Y ⟹ SAT Γ f ⊆ SAT Γ (Sup Y)"
by(rule SAT_mono)(rule Sup_upper[THEN le_funD])
lemma currentD_SAT:
assumes "current Γ f"
shows "x ∈ SAT Γ f ⟷ x ∈ A Γ ∨ d_IN f x = weight Γ x"
using currentD_weight_IN[OF assms, of x] by(auto simp add: SAT.simps)
abbreviation terminal :: "('v, 'more) web_scheme ⇒ 'v current ⇒ 'v set" (‹TERı›)
where "terminal Γ f ≡ SAT Γ f ∩ SINK f"
subsection ‹Separation›
inductive separating_gen :: "('v, 'more) graph_scheme ⇒ 'v set ⇒ 'v set ⇒ 'v set ⇒ bool"
for G A B S
where separating:
"(⋀x y p. ⟦ x ∈ A; y ∈ B; path G x p y ⟧ ⟹ (∃z ∈ set p. z ∈ S) ∨ x ∈ S)
⟹ separating_gen G A B S"
abbreviation separating :: "('v, 'more) web_scheme ⇒ 'v set ⇒ bool"
where "separating Γ ≡ separating_gen Γ (A Γ) (B Γ)"
abbreviation separating_network :: "('v, 'more) network_scheme ⇒ 'v set ⇒ bool"
where "separating_network Δ ≡ separating_gen Δ {source Δ} {sink Δ}"
lemma separating_networkI [intro?]:
"(⋀p. path Δ (source Δ) p (sink Δ) ⟹ (∃z ∈ set p. z ∈ S) ∨ source Δ ∈ S)
⟹ separating_network Δ S"
by(auto intro: separating)
lemma separatingD:
"⋀A B. ⟦ separating_gen G A B S; path G x p y; x ∈ A; y ∈ B ⟧ ⟹ (∃z ∈ set p. z ∈ S) ∨ x ∈ S"
by(blast elim: separating_gen.cases)
lemma separating_left [simp]: "⋀A B. A ⊆ A' ⟹ separating_gen Γ A B A'"
by(auto simp add: separating_gen.simps)
lemma separating_weakening:
"⋀A B. ⟦ separating_gen G A B S; S ⊆ S' ⟧ ⟹ separating_gen G A B S'"
by(rule separating; drule (3) separatingD; blast)
definition essential :: "('v, 'more) graph_scheme ⇒ 'v set ⇒ 'v set ⇒ 'v ⇒ bool"
where
"⋀B. essential G B S x ⟷ (∃p. ∃y∈B. path G x p y ∧ (x ≠ y ⟶ (∀z∈set p. z = x ∨ z ∉ S)))"
abbreviation essential_web :: "('v, 'more) web_scheme ⇒ 'v set ⇒ 'v set" (‹ℰı›)
where "essential_web Γ S ≡ {x∈S. essential Γ (B Γ) S x}"
lemma essential_weight_update [simp]:
"essential (weight_update f G) = essential G"
by(simp add: essential_def fun_eq_iff)
lemma not_essentialD:
"⋀B. ⟦ ¬ essential G B S x; path G x p y; y ∈ B ⟧ ⟹ x ≠ y ∧ (∃z∈set p. z ≠ x ∧ z ∈ S)"
by(simp add: essential_def)
lemma essentialE [elim?, consumes 1, case_names essential, cases pred: essential]:
"⋀B. ⟦ essential G B S x; ⋀p y. ⟦ path G x p y; y ∈ B; ⋀z. ⟦ x ≠ y; z ∈ set p ⟧ ⟹ z = x ∨ z ∉ S ⟧ ⟹ thesis ⟧ ⟹ thesis"
by(auto simp add: essential_def)
lemma essentialI [intro?]:
"⋀B. ⟦ path G x p y; y ∈ B; ⋀z. ⟦ x ≠ y; z ∈ set p ⟧ ⟹ z = x ∨ z ∉ S ⟧ ⟹ essential G B S x"
by(auto simp add: essential_def)
lemma essential_vertex: "⋀B. ⟦ essential G B S x; x ∉ B ⟧ ⟹vertex G x"
by(auto elim!: essentialE simp add: vertex_def elim: rtrancl_path.cases)
lemma essential_BI: "⋀B. x ∈ B ⟹ essential G B S x"
by(auto simp add: essential_def intro: rtrancl_path.base)
lemma ℰ_E [elim?, consumes 1, case_names ℰ, cases set: essential_web]:
fixes Γ (structure)
assumes "x ∈ ℰ S"
obtains p y where "path Γ x p y" "y ∈ B Γ" "⋀z. ⟦ x ≠ y; z ∈ set p ⟧ ⟹ z = x ∨ z ∉ S"
using assms by(auto elim: essentialE)
lemma essential_mono: "⋀B. ⟦ essential G B S x; S' ⊆ S ⟧ ⟹ essential G B S' x"
by(auto simp add: essential_def)
lemma separating_essential:
fixes G A B S
assumes "separating_gen G A B S"
shows "separating_gen G A B {x∈S. essential G B S x}" (is "separating_gen _ _ _ ?E")
proof
fix x y p
assume x: "x ∈ A" and y: "y ∈ B" and p: "path G x p y"
from separatingD[OF assms p x y] have "∃z ∈ set (x # p). z ∈ S" by auto
from split_list_last_prop[OF this] obtain ys z zs where decomp: "x # p = ys @ z # zs"
and z: "z ∈ S" and last: "⋀z. z ∈ set zs ⟹ z ∉ S" by auto
from decomp consider (empty) "ys = []" "x = z" "p = zs"
| (Cons) ys' where "ys = x # ys'" "p = ys' @ z # zs"
by(auto simp add: Cons_eq_append_conv)
then show "(∃z∈set p. z ∈ ?E) ∨ x ∈ ?E"
proof(cases)
case empty
hence "x ∈ ?E" using z p last y by(auto simp add: essential_def)
thus ?thesis ..
next
case (Cons ys')
from p have "path G z zs y" unfolding Cons by(rule rtrancl_path_appendE)
hence "z ∈ ?E" using z y last by(auto simp add: essential_def)
thus ?thesis using Cons by auto
qed
qed
definition roofed_gen :: "('v, 'more) graph_scheme ⇒ 'v set ⇒ 'v set ⇒ 'v set"
where roofed_def: "⋀B. roofed_gen G B S = {x. ∀p. ∀y∈B. path G x p y ⟶ (∃z∈set p. z ∈ S) ∨ x ∈ S}"
abbreviation roofed :: "('v, 'more) web_scheme ⇒ 'v set ⇒ 'v set" (‹RFı›)
where "roofed Γ ≡ roofed_gen Γ (B Γ)"
abbreviation roofed_network :: "('v, 'more) network_scheme ⇒ 'v set ⇒ 'v set" (‹RF⇧Nı›)
where "roofed_network Δ ≡ roofed_gen Δ {sink Δ}"
lemma roofedI [intro?]:
"⋀B. (⋀p y. ⟦ path G x p y; y ∈ B ⟧ ⟹ (∃z∈set p. z ∈ S) ∨ x ∈ S) ⟹ x ∈ roofed_gen G B S"
by(auto simp add: roofed_def)
lemma not_roofedE: fixes B
assumes "x ∉ roofed_gen G B S"
obtains p y where "path G x p y" "y ∈ B" "⋀z. z ∈ set (x # p) ⟹ z ∉ S"
using assms by(auto simp add: roofed_def)
lemma roofed_greater: "⋀B. S ⊆ roofed_gen G B S"
by(auto simp add: roofed_def)
lemma roofed_greaterI: "⋀B. x ∈ S ⟹ x ∈ roofed_gen G B S"
using roofed_greater[of S G] by blast
lemma roofed_mono: "⋀B. S ⊆ S' ⟹ roofed_gen G B S ⊆ roofed_gen G B S'"
by(fastforce simp add: roofed_def)
lemma in_roofed_mono: "⋀B. ⟦ x ∈ roofed_gen G B S; S ⊆ S' ⟧ ⟹ x ∈ roofed_gen G B S'"
using roofed_mono[THEN subsetD] .
lemma roofedD: "⋀B. ⟦ x ∈ roofed_gen G B S; path G x p y; y ∈ B ⟧ ⟹ (∃z∈set p. z ∈ S) ∨ x ∈ S"
unfolding roofed_def by blast
lemma separating_RF_A:
fixes A B
assumes "separating_gen G A B X"
shows "A ⊆ roofed_gen G B X"
by(rule subsetI roofedI)+(erule separatingD[OF assms])
lemma roofed_idem: fixes B shows "roofed_gen G B (roofed_gen G B S) = roofed_gen G B S"
proof(rule equalityI subsetI roofedI)+
fix x p y
assume x: "x ∈ roofed_gen G B (roofed_gen G B S)" and p: "path G x p y" and y: "y ∈ B"
from roofedD[OF x p y] obtain z where *: "z ∈ set (x # p)" and z: "z ∈ roofed_gen G B S" by auto
from split_list[OF *] obtain ys zs where split: "x # p = ys @ z # zs" by blast
with p have p': "path G z zs y" by(auto simp add: Cons_eq_append_conv elim: rtrancl_path_appendE)
from roofedD[OF z p' y] split show "(∃z∈set p. z ∈ S) ∨ x ∈ S"
by(auto simp add: Cons_eq_append_conv)
qed(rule roofed_mono roofed_greater)+
lemma in_roofed_mono': "⋀B. ⟦ x ∈ roofed_gen G B S; S ⊆ roofed_gen G B S' ⟧ ⟹ x ∈ roofed_gen G B S'"
by(subst roofed_idem[symmetric])(erule in_roofed_mono)
lemma roofed_mono': "⋀B. S ⊆ roofed_gen G B S' ⟹ roofed_gen G B S ⊆ roofed_gen G B S'"
by(rule subsetI)(rule in_roofed_mono')
lemma roofed_idem_Un1: fixes B shows "roofed_gen G B (roofed_gen G B S ∪ T) = roofed_gen G B (S ∪ T)"
proof -
have "S ⊆ T ∪ roofed_gen G B S"
by (metis (no_types) UnCI roofed_greater subsetCE subsetI)
then have "S ∪ T ⊆ T ∪ roofed_gen G B S ∧ T ∪ roofed_gen G B S ⊆ roofed_gen G B (S ∪ T)"
by (metis (no_types) Un_subset_iff Un_upper2 roofed_greater roofed_mono sup.commute)
then show ?thesis
by (metis (no_types) roofed_idem roofed_mono subset_antisym sup.commute)
qed
lemma roofed_UN: fixes A B
shows "roofed_gen G B (⋃i∈A. roofed_gen G B (X i)) = roofed_gen G B (⋃i∈A. X i)" (is "?lhs = ?rhs")
proof(rule equalityI)
show "?rhs ⊆ ?lhs" by(rule roofed_mono)(blast intro: roofed_greaterI)
show "?lhs ⊆ ?rhs" by(rule roofed_mono')(blast intro: in_roofed_mono)
qed
lemma RF_essential: fixes Γ (structure) shows "RF (ℰ S) = RF S"
proof(intro set_eqI iffI)
fix x
assume RF: "x ∈ RF S"
show "x ∈ RF (ℰ S)"
proof
fix p y
assume p: "path Γ x p y" and y: "y ∈ B Γ"
from roofedD[OF RF this] have "∃z∈set (x # p). z ∈ S" by auto
from split_list_last_prop[OF this] obtain ys z zs where decomp: "x # p = ys @ z # zs"
and z: "z ∈ S" and last: "⋀z. z ∈ set zs ⟹ z ∉ S" by auto
from decomp consider (empty) "ys = []" "x = z" "p = zs"
| (Cons) ys' where "ys = x # ys'" "p = ys' @ z # zs"
by(auto simp add: Cons_eq_append_conv)
then show "(∃z∈set p. z ∈ ℰ S) ∨ x ∈ ℰ S"
proof(cases)
case empty
hence "x ∈ ℰ S" using z p last y by(auto simp add: essential_def)
thus ?thesis ..
next
case (Cons ys')
from p have "path Γ z zs y" unfolding Cons by(rule rtrancl_path_appendE)
hence "z ∈ ℰ S" using z y last by(auto simp add: essential_def)
thus ?thesis using Cons by auto
qed
qed
qed(blast intro: in_roofed_mono)
lemma essentialE_RF:
fixes Γ (structure) and B
assumes "essential Γ B S x"
obtains p y where "path Γ x p y" "y ∈ B" "distinct (x # p)" "⋀z. z ∈ set p ⟹ z ∉ roofed_gen Γ B S"
proof -
from assms obtain p y where p: "path Γ x p y" and y: "y ∈ B"
and bypass: "⋀z. ⟦ x ≠ y; z ∈ set p ⟧ ⟹ z = x ∨ z ∉ S" by(rule essentialE) blast
from p obtain p' where p': "path Γ x p' y" and distinct: "distinct (x # p')"
and subset: "set p' ⊆ set p" by(rule rtrancl_path_distinct)
{ fix z
assume z: "z ∈ set p'"
hence "y ∈ set p'" using rtrancl_path_last[OF p', symmetric] p'
by(auto elim: rtrancl_path.cases intro: last_in_set)
with distinct z subset have neq: "x ≠ y" and "z ∈ set p" by(auto)
from bypass[OF this] z distinct have "z ∉ S" by auto
have "z ∉ roofed_gen Γ B S"
proof
assume z': "z ∈ roofed_gen Γ B S"
from split_list[OF z] obtain ys zs where decomp: "p' = ys @ z # zs" by blast
with p' have "path Γ z zs y" by(auto elim: rtrancl_path_appendE)
from roofedD[OF z' this y] ‹z ∉ S› obtain z' where "z' ∈ set zs" "z' ∈ S" by auto
with bypass[of z'] neq decomp subset distinct show False by auto
qed }
with p' y distinct show thesis ..
qed
lemma ℰ_E_RF:
fixes Γ (structure)
assumes "x ∈ ℰ S"
obtains p y where "path Γ x p y" "y ∈ B Γ" "distinct (x # p)" "⋀z. z ∈ set p ⟹ z ∉ RF S"
using assms by(auto elim: essentialE_RF)
lemma in_roofed_essentialD:
fixes Γ (structure)
assumes RF: "x ∈ RF S"
and ess: "essential Γ (B Γ) S x"
shows "x ∈ S"
proof -
from ess obtain p y where p: "path Γ x p y" and y: "y ∈ B Γ" and "distinct (x # p)"
and bypass: "⋀z. z ∈ set p ⟹ z ∉ S" by(rule essentialE_RF)(auto intro: roofed_greaterI)
from roofedD[OF RF p y] bypass show "x ∈ S" by auto
qed
lemma separating_RF: fixes Γ (structure) shows "separating Γ (RF S) ⟷ separating Γ S"
proof
assume sep: "separating Γ (RF S)"
show "separating Γ S"
proof
fix x y p
assume p: "path Γ x p y" and x: "x ∈ A Γ" and y: "y ∈ B Γ"
from separatingD[OF sep p x y] have "∃z ∈ set (x # p). z ∈ RF S" by auto
from split_list_last_prop[OF this] obtain ys z zs where split: "x # p = ys @ z # zs"
and z: "z ∈ RF S" and bypass: "⋀z'. z' ∈ set zs ⟹ z' ∉ RF S" by auto
from p split have "path Γ z zs y" by(cases ys)(auto elim: rtrancl_path_appendE)
hence "essential Γ (B Γ) S z" using y
by(rule essentialI)(auto dest: bypass intro: roofed_greaterI)
with z have "z ∈ S" by(rule in_roofed_essentialD)
with split show "(∃z∈set p. z ∈ S) ∨ x ∈ S" by(cases ys)auto
qed
qed(blast intro: roofed_greaterI separating_weakening)
definition roofed_circ :: "('v, 'more) web_scheme ⇒ 'v set ⇒ 'v set" (‹RF⇧∘ı›)
where "roofed_circ Γ S = roofed Γ S - ℰ⇘Γ⇙ S"
lemma roofed_circI: fixes Γ (structure) shows
"⟦ x ∈ RF T; x ∈ T ⟹ ¬ essential Γ (B Γ) T x ⟧ ⟹ x ∈ RF⇧∘ T"
by(simp add: roofed_circ_def)
lemma roofed_circE:
fixes Γ (structure)
assumes "x ∈ RF⇧∘ T"
obtains "x ∈ RF T" "¬ essential Γ (B Γ) T x"
using assms by(auto simp add: roofed_circ_def intro: in_roofed_essentialD)
lemma ℰ_ℰ: fixes Γ (structure) shows "ℰ (ℰ S) = ℰ S"
by(auto intro: essential_mono)
lemma roofed_circ_essential: fixes Γ (structure) shows "RF⇧∘ (ℰ S) = RF⇧∘ S"
unfolding roofed_circ_def RF_essential ℰ_ℰ ..
lemma essential_RF: fixes B
shows "essential G B (roofed_gen G B S) = essential G B S" (is "essential _ _ ?RF = _")
proof(intro ext iffI)
show "essential G B S x" if "essential G B ?RF x" for x using that
by(rule essential_mono)(blast intro: roofed_greaterI)
show "essential G B ?RF x" if "essential G B S x" for x
using that by(rule essentialE_RF)(erule (1) essentialI, blast)
qed
lemma ℰ_RF: fixes Γ (structure) shows "ℰ (RF S) = ℰ S"
by(auto dest: in_roofed_essentialD simp add: essential_RF intro: roofed_greaterI)
lemma essential_ℰ: fixes Γ (structure) shows "essential Γ (B Γ) (ℰ S) = essential Γ (B Γ) S"
by(subst essential_RF[symmetric])(simp only: RF_essential essential_RF)
lemma RF_in_B: fixes Γ (structure) shows "x ∈ B Γ ⟹ x ∈ RF S ⟷ x ∈ S"
by(auto intro: roofed_greaterI dest: roofedD[OF _ rtrancl_path.base])
lemma RF_circ_edge_forward:
fixes Γ (structure)
assumes x: "x ∈ RF⇧∘ S"
and edge: "edge Γ x y"
shows "y ∈ RF S"
proof
fix p z
assume p: "path Γ y p z" and z: "z ∈ B Γ"
from x have rf: "x ∈ RF S" and ness: "x ∉ ℰ S" by(auto elim: roofed_circE)
show "(∃z∈set p. z ∈ S) ∨ y ∈ S"
proof(cases "∃z'∈set (y # p). z' ∈ S")
case False
from edge p have p': "path Γ x (y # p) z" ..
from roofedD[OF rf this z] False have "x ∈ S" by auto
moreover have "essential Γ (B Γ) S x" using p' False z by(auto intro!: essentialI)
ultimately have "x ∈ ℰ S" by simp
with ness show ?thesis by contradiction
qed auto
qed
subsection ‹Waves›
inductive wave :: "('v, 'more) web_scheme ⇒ 'v current ⇒ bool"
for Γ (structure) and f
where
wave:
"⟦ separating Γ (TER f);
⋀x. x ∉ RF (TER f) ⟹ d_OUT f x = 0 ⟧
⟹ wave Γ f"
lemma wave_0 [simp]: "wave Γ zero_current"
by rule simp_all
lemma waveD_separating: "wave Γ f ⟹ separating Γ (TER⇘Γ⇙ f)"
by(simp add: wave.simps)
lemma waveD_OUT: "⟦ wave Γ f; x ∉ RF⇘Γ⇙ (TER⇘Γ⇙ f) ⟧ ⟹ d_OUT f x = 0"
by(simp add: wave.simps)
lemma wave_A_in_RF: fixes Γ (structure)
shows "⟦ wave Γ f; x ∈ A Γ ⟧ ⟹ x ∈ RF (TER f)"
by(auto intro!: roofedI dest!: waveD_separating separatingD)
lemma wave_not_RF_IN_zero:
fixes Γ (structure)
assumes f: "current Γ f"
and w: "wave Γ f"
and x: "x ∉ RF (TER f)"
shows "d_IN f x = 0"
proof -
from x obtain p z where z: "z ∈ B Γ" and p: "path Γ x p z"
and bypass: "⋀z. z ∈ set p ⟹ z ∉ TER f" "x ∉ TER f"
by(clarsimp simp add: roofed_def)
have "f (y, x) = 0" for y
proof(cases "edge Γ y x")
case edge: True
have "d_OUT f y = 0"
proof(cases "y ∈ TER f")
case False
with z p bypass edge have "y ∉ RF (TER f)"
by(auto simp add: roofed_def intro: rtrancl_path.step intro!: exI rev_bexI)
thus "d_OUT f y = 0" by(rule waveD_OUT[OF w])
qed(auto simp add: SINK.simps)
moreover have "f (y, x) ≤ d_OUT f y" by (rule d_OUT_ge_point)
ultimately show ?thesis by simp
qed(simp add: currentD_outside[OF f])
then show "d_IN f x = 0" unfolding d_IN_def
by(simp add: nn_integral_0_iff emeasure_count_space_eq_0)
qed
lemma current_Sup:
fixes Γ (structure)
assumes chain: "Complete_Partial_Order.chain (≤) Y"
and Y: "Y ≠ {}"
and current: "⋀f. f ∈ Y ⟹ current Γ f"
and countable [simp]: "countable (support_flow (Sup Y))"
shows "current Γ (Sup Y)"
proof(rule, goal_cases)
case (1 x)
have "d_OUT (Sup Y) x = (SUP f∈Y. d_OUT f x)" using chain Y by(simp add: d_OUT_Sup)
also have "… ≤ weight Γ x" using 1
by(intro SUP_least)(auto dest!: current currentD_weight_OUT)
finally show ?case .
next
case (2 x)
have "d_IN (Sup Y) x = (SUP f∈Y. d_IN f x)" using chain Y by(simp add: d_IN_Sup)
also have "… ≤ weight Γ x" using 2
by(intro SUP_least)(auto dest!: current currentD_weight_IN)
finally show ?case .
next
case (3 x)
have "d_OUT (Sup Y) x = (SUP f∈Y. d_OUT f x)" using chain Y by(simp add: d_OUT_Sup)
also have "… ≤ (SUP f∈Y. d_IN f x)" using 3
by(intro SUP_mono)(auto dest: current currentD_OUT_IN)
also have "… = d_IN (Sup Y) x" using chain Y by(simp add: d_IN_Sup)
finally show ?case .
next
case (4 a)
have "d_IN (Sup Y) a = (SUP f∈Y. d_IN f a)" using chain Y by(simp add: d_IN_Sup)
also have "… = (SUP f∈Y. 0)" using 4 by(intro SUP_cong)(auto dest!: current currentD_IN)
also have "… = 0" using Y by simp
finally show ?case .
next
case (5 b)
have "d_OUT (Sup Y) b = (SUP f∈Y. d_OUT f b)" using chain Y by(simp add: d_OUT_Sup)
also have "… = (SUP f∈Y. 0)" using 5 by(intro SUP_cong)(auto dest!: current currentD_OUT)
also have "… = 0" using Y by simp
finally show ?case .
next
fix e
assume "e ∉ ❙E"
from currentD_outside'[OF current this] have "f e = 0" if "f ∈ Y" for f using that by simp
hence "Sup Y e = (SUP _∈Y. 0)" by(auto intro: SUP_cong)
then show "Sup Y e = 0" using Y by(simp)
qed
lemma wave_lub:
fixes Γ (structure)
assumes chain: "Complete_Partial_Order.chain (≤) Y"
and Y: "Y ≠ {}"
and wave: "⋀f. f ∈ Y ⟹ wave Γ f"
and countable [simp]: "countable (support_flow (Sup Y))"
shows "wave Γ (Sup Y)"
proof
{ fix x y p
assume p: "path Γ x p y" and y: "y ∈ B Γ"
define P where "P = {x} ∪ set p"
let ?f = "λf. SINK f ∩ P"
have "Complete_Partial_Order.chain (⊇) (?f ` Y)" using chain
by(rule chain_imageI)(auto dest: SINK_mono')
moreover have "… ⊆ Pow P" by auto
hence "finite (?f ` Y)" by(rule finite_subset)(simp add: P_def)
ultimately have "(⋂(?f ` Y)) ∈ ?f ` Y"
by(rule ccpo.in_chain_finite[OF complete_lattice_ccpo_dual])(simp add: Y)
then obtain f where f: "f ∈ Y" and eq: "⋂(?f ` Y) = ?f f" by clarify
hence *: "(⋂f∈Y. SINK f) ∩ P = SINK f ∩ P" by(clarsimp simp add: prod_lub_def Y)+
{ fix g
assume "g ∈ Y" "f ≤ g"
with * have "(⋂f∈Y. SINK f) ∩ P = SINK g ∩ P" by(blast dest: SINK_mono')
then have "TER (Sup Y) ∩ P ⊇ TER g ∩ P"
using SAT_Sup_upper[OF ‹g ∈ Y›, of Γ] SINK_Sup[OF chain Y countable] by blast }
with f have "∃f∈Y. ∀g∈Y. g ≥ f ⟶ TER g ∩ P ⊆ TER (Sup Y) ∩ P" by blast }
note subset = this
show "separating Γ (TER (Sup Y))"
proof
fix x y p
assume *: "path Γ x p y" "y ∈ B Γ" and "x ∈ A Γ"
let ?P = "{x} ∪ set p"
from subset[OF *] obtain f where f:"f ∈ Y"
and subset: "TER f ∩ ?P ⊆ TER (Sup Y) ∩ ?P" by blast
from wave[OF f] have "TER f ∩ ?P ≠ {}" using * ‹x ∈ A Γ›
by(auto simp add: wave.simps dest: separatingD)
with subset show " (∃z∈set p. z ∈ TER (Sup Y)) ∨ x ∈ TER (Sup Y)" by blast
qed
fix x
assume "x ∉ RF (TER (Sup Y))"
then obtain p y where y: "y ∈ B Γ"
and p: "path Γ x p y"
and ter: "TER (Sup Y) ∩ ({x} ∪ set p) = {}" by(auto simp add: roofed_def)
let ?P = "{x} ∪ set p"
from subset[OF p y] obtain f where f: "f ∈ Y"
and subset: "⋀g. ⟦ g ∈ Y; f ≤ g ⟧ ⟹ TER g ∩ ?P ⊆ TER (Sup Y) ∩ ?P" by blast
{ fix g
assume g: "g ∈ Y"
with chain f have "f ≤ g ∨ g ≤ f" by(rule chainD)
hence "d_OUT g x = 0"
proof
assume "f ≤ g"
from subset[OF g this] ter have "TER g ∩ ?P = {}" by blast
with p y have "x ∉ RF (TER g)" by(auto simp add: roofed_def)
with wave[OF g] show ?thesis by(blast elim: wave.cases)
next
assume "g ≤ f"
from subset ter f have "TER f ∩ ?P = {}" by blast
with y p have "x ∉ RF (TER f)" by(auto simp add: roofed_def)
with wave[OF f] have "d_OUT f x = 0" by(blast elim: wave.cases)
moreover have "d_OUT g x ≤ d_OUT f x" using ‹g ≤ f›[THEN le_funD] by(rule d_OUT_mono)
ultimately show ?thesis by simp
qed }
thus "d_OUT (Sup Y) x = 0" using chain Y by(simp add: d_OUT_Sup)
qed
lemma ex_maximal_wave:
fixes Γ (structure)
assumes countable: "countable ❙E"
shows "∃f. current Γ f ∧ wave Γ f ∧ (∀w. current Γ w ∧ wave Γ w ∧ f ≤ w ⟶ f = w)"
proof -
define Field_r where "Field_r = {f. current Γ f ∧ wave Γ f}"
define r where "r = {(f, g). f ∈ Field_r ∧ g ∈ Field_r ∧ f ≤ g}"
have Field_r: "Field r = Field_r" by(auto simp add: Field_def r_def)
have "Partial_order r" unfolding order_on_defs
by(auto intro!: refl_onI transI antisymI simp add: Field_r r_def Field_def)
hence "∃m∈Field r. ∀a∈Field r. (m, a) ∈ r ⟶ a = m"
proof(rule Zorns_po_lemma)
fix Y
assume "Y ∈ Chains r"
hence Y: "Complete_Partial_Order.chain (≤) Y"
and w: "⋀f. f ∈ Y ⟹ wave Γ f"
and f: "⋀f. f ∈ Y ⟹ current Γ f"
by(auto simp add: Chains_def r_def chain_def Field_r_def)
show "∃w ∈ Field r. ∀f ∈ Y. (f, w) ∈ r"
proof(cases "Y = {}")
case True
have "zero_current ∈ Field r" by(simp add: Field_r Field_r_def)
with True show ?thesis by blast
next
case False
have "support_flow (Sup Y) ⊆ ❙E" by(auto simp add: support_flow_Sup elim!: support_flow.cases dest!: f dest: currentD_outside)
hence c: "countable (support_flow (Sup Y))" using countable by(rule countable_subset)
with Y False f w have "Sup Y ∈ Field r" unfolding Field_r Field_r_def
by(blast intro: wave_lub current_Sup)
moreover then have "(f, Sup Y) ∈ r" if "f ∈ Y" for f using w[OF that] f[OF that] that unfolding Field_r
by(auto simp add: r_def Field_r_def intro: Sup_upper)
ultimately show ?thesis by blast
qed
qed
thus ?thesis by(simp add: Field_r Field_r_def)(auto simp add: r_def Field_r_def)
qed
lemma essential_leI:
fixes Γ (structure)
assumes g: "current Γ g" and w: "wave Γ g"
and le: "⋀e. f e ≤ g e"
and x: "x ∈ ℰ (TER g)"
shows "essential Γ (B Γ) (TER f) x"
proof -
from x obtain p y where p: "path Γ x p y" and y: "y ∈ B Γ" and distinct: "distinct (x # p)"
and bypass: "⋀z. z ∈ set p ⟹ z ∉ RF (TER g)" by(rule ℰ_E_RF) blast
show ?thesis using p y
proof
fix z
assume "z ∈ set p"
hence z: "z ∉ RF (TER g)" by(auto dest: bypass)
with w have OUT: "d_OUT g z = 0" and IN: "d_IN g z = 0" by(rule waveD_OUT wave_not_RF_IN_zero[OF g])+
with z have "z ∉ A Γ" "weight Γ z > 0" by(auto intro!: roofed_greaterI simp add: SAT.simps SINK.simps)
moreover from IN d_IN_mono[of f z g, OF le] have "d_IN f z ≤ 0" by(simp)
ultimately have "z ∉ TER f" by(auto simp add: SAT.simps)
then show "z = x ∨ z ∉ TER f" by simp
qed
qed
lemma essential_eq_leI:
fixes Γ (structure)
assumes g: "current Γ g" and w: "wave Γ g"
and le: "⋀e. f e ≤ g e"
and subset: "ℰ (TER g) ⊆ TER f"
shows "ℰ (TER f) = ℰ (TER g)"
proof
show subset: "ℰ (TER g) ⊆ ℰ (TER f)"
proof
fix x
assume x: "x ∈ ℰ (TER g)"
hence "x ∈ TER f" using subset by blast
moreover have "essential Γ (B Γ) (TER f) x" using g w le x by(rule essential_leI)
ultimately show "x ∈ ℰ (TER f)" by simp
qed
show "… ⊆ ℰ (TER g)"
proof
fix x
assume x: "x ∈ ℰ (TER f)"
hence "x ∈ TER f" by auto
hence "x ∈ RF (TER g)"
proof(rule contrapos_pp)
assume x: "x ∉ RF (TER g)"
with w have OUT: "d_OUT g x = 0" and IN: "d_IN g x = 0" by(rule waveD_OUT wave_not_RF_IN_zero[OF g])+
with x have "x ∉ A Γ" "weight Γ x > 0" by(auto intro!: roofed_greaterI simp add: SAT.simps SINK.simps)
moreover from IN d_IN_mono[of f x g, OF le] have "d_IN f x ≤ 0" by(simp)
ultimately show "x ∉ TER f" by(auto simp add: SAT.simps)
qed
moreover have "x ∉ RF⇧∘ (TER g)"
proof
assume "x ∈ RF⇧∘ (TER g)"
hence RF: "x ∈ RF (ℰ (TER g))" and not_E: "x ∉ ℰ (TER g)"
unfolding RF_essential by(simp_all add: roofed_circ_def)
from x obtain p y where p: "path Γ x p y" and y: "y ∈ B Γ" and distinct: "distinct (x # p)"
and bypass: "⋀z. z ∈ set p ⟹ z ∉ RF (TER f)" by(rule ℰ_E_RF) blast
from roofedD[OF RF p y] not_E obtain z where "z ∈ set p" "z ∈ ℰ (TER g)" by blast
with subset bypass[of z] show False by(auto intro: roofed_greaterI)
qed
ultimately show "x ∈ ℰ (TER g)" by(simp add: roofed_circ_def)
qed
qed
subsection ‹Hindrances and looseness›
inductive hindrance_by :: "('v, 'more) web_scheme ⇒ 'v current ⇒ ennreal ⇒ bool"
for Γ (structure) and f and ε
where
hindrance_by:
"⟦ a ∈ A Γ; a ∉ ℰ (TER f); d_OUT f a < weight Γ a; ε < weight Γ a - d_OUT f a ⟧ ⟹ hindrance_by Γ f ε"
inductive hindrance :: "('v, 'more) web_scheme ⇒ 'v current ⇒ bool"
for Γ (structure) and f
where
hindrance:
"⟦ a ∈ A Γ; a ∉ ℰ (TER f); d_OUT f a < weight Γ a ⟧ ⟹ hindrance Γ f"
inductive hindered :: "('v, 'more) web_scheme ⇒ bool"
for Γ (structure)
where hindered: "⟦ hindrance Γ f; current Γ f; wave Γ f ⟧ ⟹ hindered Γ"
inductive hindered_by :: "('v, 'more) web_scheme ⇒ ennreal ⇒ bool"
for Γ (structure) and ε
where hindered_by: "⟦ hindrance_by Γ f ε; current Γ f; wave Γ f ⟧ ⟹ hindered_by Γ ε"
lemma hindrance_into_hindrance_by:
assumes "hindrance Γ f"
shows "∃ε>0. hindrance_by Γ f ε"
using assms
proof cases
case (hindrance a)
let ?ε = "if weight Γ a = ⊤ then 1 else (weight Γ a - d_OUT f a) / 2"
from ‹d_OUT f a < weight Γ a› have "weight Γ a - d_OUT f a > 0" "weight Γ a ≠ ⊤ ⟹ weight Γ a - d_OUT f a < ⊤"
by(simp_all add: diff_gr0_ennreal less_top diff_less_top_ennreal)
from ennreal_mult_strict_left_mono[of 1 2, OF _ this]
have "0 < ?ε" and "?ε < weight Γ a - d_OUT f a" using ‹d_OUT f a < weight Γ a›
by(auto intro!: diff_gr0_ennreal simp: ennreal_zero_less_divide divide_less_ennreal)
with hindrance show ?thesis by(auto intro!: hindrance_by.intros)
qed
lemma hindrance_by_into_hindrance: "hindrance_by Γ f ε ⟹ hindrance Γ f"
by(blast elim: hindrance_by.cases intro: hindrance.intros)
lemma hindrance_conv_hindrance_by: "hindrance Γ f ⟷ (∃ε>0. hindrance_by Γ f ε)"
by(blast intro: hindrance_into_hindrance_by hindrance_by_into_hindrance)
lemma hindered_into_hindered_by: "hindered Γ ⟹ ∃ε>0. hindered_by Γ ε"
by(blast intro: hindered_by.intros elim: hindered.cases dest: hindrance_into_hindrance_by)
lemma hindered_by_into_hindered: "hindered_by Γ ε ⟹ hindered Γ"
by(blast elim: hindered_by.cases intro: hindered.intros dest: hindrance_by_into_hindrance)
lemma hindered_conv_hindered_by: "hindered Γ ⟷ (∃ε>0. hindered_by Γ ε)"
by(blast intro: hindered_into_hindered_by hindered_by_into_hindered)
inductive loose :: "('v, 'more) web_scheme ⇒ bool"
for Γ
where
loose: "⟦ ⋀f. ⟦ current Γ f; wave Γ f ⟧ ⟹ f = zero_current; ¬ hindrance Γ zero_current ⟧
⟹ loose Γ"
lemma looseD_hindrance: "loose Γ ⟹ ¬ hindrance Γ zero_current"
by(simp add: loose.simps)
lemma looseD_wave:
"⟦ loose Γ; current Γ f; wave Γ f ⟧ ⟹ f = zero_current"
by(simp add: loose.simps)
lemma loose_unhindered:
fixes Γ (structure)
assumes "loose Γ"
shows "¬ hindered Γ"
apply auto
apply(erule hindered.cases)
apply(frule (1) looseD_wave[OF assms])
apply simp
using looseD_hindrance[OF assms]
by simp
context
fixes Γ Γ' :: "('v, 'more) web_scheme"
assumes [simp]: "edge Γ = edge Γ'" "A Γ = A Γ'" "B Γ = B Γ'"
and weight_eq: "⋀x. x ∉ A Γ' ⟹ weight Γ x = weight Γ' x"
and weight_le: "⋀a. a ∈ A Γ' ⟹ weight Γ a ≥ weight Γ' a"
begin
private lemma essential_eq: "essential Γ = essential Γ'"
by(simp add: fun_eq_iff essential_def)
qualified lemma TER_eq: "TER⇘Γ⇙ f = TER⇘Γ'⇙ f"
apply(auto simp add: SINK.simps SAT.simps)
apply(erule contrapos_np; drule weight_eq; simp)+
done
qualified lemma separating_eq: "separating_gen Γ = separating_gen Γ'"
by(intro ext iffI; rule separating_gen.intros; drule separatingD; simp)
qualified lemma roofed_eq: "⋀B. roofed_gen Γ B S = roofed_gen Γ' B S"
by(simp add: roofed_def)
lemma wave_eq_web:
"wave Γ f ⟷ wave Γ' f"
by(simp add: wave.simps separating_eq TER_eq roofed_eq)
lemma current_mono_web: "current Γ' f ⟹ current Γ f"
apply(rule current, simp_all add: currentD_OUT_IN currentD_IN currentD_OUT currentD_outside')
subgoal for x by(cases "x ∈ A Γ'")(auto dest!: weight_eq weight_le dest: currentD_weight_OUT intro: order_trans)
subgoal for x by(cases "x ∈ A Γ'")(auto dest!: weight_eq weight_le dest: currentD_weight_IN intro: order_trans)
done
lemma hindrance_mono_web: "hindrance Γ' f ⟹ hindrance Γ f"
apply(erule hindrance.cases)
apply(rule hindrance)
apply simp
apply(unfold TER_eq, simp add: essential_eq)
apply(auto dest!: weight_le)
done
lemma hindered_mono_web: "hindered Γ' ⟹ hindered Γ"
apply(erule hindered.cases)
apply(rule hindered.intros)
apply(erule hindrance_mono_web)
apply(erule current_mono_web)
apply(simp add: wave_eq_web)
done
end
subsection ‹Linkage›
text ‹
The following definition of orthogonality is stronger than the original definition 3.5 in
\<^cite>‹AharoniBergerGeorgakopoulusPerlsteinSpruessel2011JCT› in that the outflow from any
‹A›-vertices in the set must saturate the vertex; @{term "S ⊆ SAT Γ f"} is not enough.
With the original definition of orthogonal current, the reduction from networks to webs fails because
the induced flow need not saturate edges going out of the source. Consider the network with three
nodes ‹s›, ‹x›, and ‹t› and edges ‹(s, x)› and ‹(x, t)› with
capacity ‹1›. Then, the corresponding web has the vertices ‹(s, x)› and
‹(x, t)› and one edge from ‹(s, x)› to ‹(x, t)›. Clearly, the zero current
@{term [source] zero_current} is a web-flow and ‹TER zero_current = {(s, x)}›, which is essential.
Moreover, @{term [source] zero_current} and ‹{(s, x)}› are orthogonal because
@{term [source] zero_current} trivially saturates ‹(s, x)› as this is a vertex in ‹A›.
›
inductive orthogonal_current :: "('v, 'more) web_scheme ⇒ 'v current ⇒ 'v set ⇒ bool"
for Γ (structure) and f S
where orthogonal_current:
"⟦ ⋀x. ⟦ x ∈ S; x ∉ A Γ ⟧ ⟹ weight Γ x ≤ d_IN f x;
⋀x. ⟦ x ∈ S; x ∈ A Γ; x ∉ B Γ ⟧ ⟹ d_OUT f x = weight Γ x;
⋀u v. ⟦ v ∈ RF S; u ∉ RF⇧∘ S ⟧ ⟹ f (u, v) = 0 ⟧
⟹ orthogonal_current Γ f S"
lemma orthogonal_currentD_SAT: "⟦ orthogonal_current Γ f S; x ∈ S ⟧ ⟹ x ∈ SAT Γ f"
by(auto elim!: orthogonal_current.cases intro: SAT.intros)
lemma orthogonal_currentD_A: "⟦ orthogonal_current Γ f S; x ∈ S; x ∈ A Γ; x ∉ B Γ ⟧ ⟹ d_OUT f x = weight Γ x"
by(auto elim: orthogonal_current.cases)
lemma orthogonal_currentD_in: "⟦ orthogonal_current Γ f S; v ∈ RF⇘Γ⇙ S; u ∉ RF⇧∘⇘Γ⇙ S ⟧ ⟹ f (u, v) = 0"
by(auto elim: orthogonal_current.cases)
inductive linkage :: "('v, 'more) web_scheme ⇒ 'v current ⇒ bool"
for Γ f
where
linkage: "(⋀x. x ∈ A Γ ⟹ d_OUT f x = weight Γ x) ⟹ linkage Γ f"
lemma linkageD: "⟦ linkage Γ f; x ∈ A Γ ⟧ ⟹ d_OUT f x = weight Γ x"
by(rule linkage.cases)
abbreviation linkable :: "('v, 'more) web_scheme ⇒ bool"
where "linkable Γ ≡ ∃f. web_flow Γ f ∧ linkage Γ f"
subsection ‹Trimming›
context
fixes Γ :: "('v, 'more) web_scheme" (structure)
and f :: "'v current"
begin
inductive trimming :: "'v current ⇒ bool"
for g
where
trimming:
"⟦ current Γ g; wave Γ g; g ≤ f; ⋀x. ⟦ x ∈ RF⇧∘ (TER f); x ∉ A Γ ⟧ ⟹ KIR g x; ℰ (TER g) - A Γ = ℰ (TER f) - A Γ ⟧
⟹ trimming g"
lemma assumes "trimming g"
shows trimmingD_current: "current Γ g"
and trimmingD_wave: "wave Γ g"
and trimmingD_le: "⋀e. g e ≤ f e"
and trimmingD_KIR: "⟦ x ∈ RF⇧∘ (TER f); x ∉ A Γ ⟧ ⟹ KIR g x"
and trimmingD_ℰ: "ℰ (TER g) - A Γ = ℰ (TER f) - A Γ"
using assms by(blast elim: trimming.cases dest: le_funD)+
lemma ex_trimming:
assumes f: "current Γ f"
and w: "wave Γ f"
and countable: "countable ❙E"
and weight_finite: "⋀x. weight Γ x ≠ ⊤"
shows "∃g. trimming g"
proof -
define F where "F = {g. current Γ g ∧ wave Γ g ∧ g ≤ f ∧ ℰ (TER g) = ℰ (TER f)}"
define leq where "leq = restrict_rel F {(g, g'). g' ≤ g}"
have in_F [simp]: "g ∈ F ⟷ current Γ g ∧ wave Γ g ∧ (∀e. g e ≤ f e) ∧ ℰ (TER g) = ℰ (TER f)" for g
by(simp add: F_def le_fun_def)
have f_finite [simp]: "f e ≠ ⊤" for e
proof(cases e)
case (Pair x y)
have "f (x, y) ≤ d_IN f y" by (rule d_IN_ge_point)
also have "… ≤ weight Γ y" by(rule currentD_weight_IN[OF f])
also have "… < ⊤" by(simp add: weight_finite less_top[symmetric])
finally show ?thesis using Pair by simp
qed
have chainD: "Inf M ∈ F" if M: "M ∈ Chains leq" and nempty: "M ≠ {}" for M
proof -
from nempty obtain g0 where g0: "g0 ∈ M" by auto
have g0_le_f: "g0 e ≤ f e" and g: "current Γ g0" and w0: "wave Γ g0" for e
using Chains_FieldD[OF M g0] by(cases e, auto simp add: leq_def)
have finite_OUT: "d_OUT f x ≠ ⊤" for x using weight_finite[of x]
by(rule neq_top_trans)(rule currentD_weight_OUT[OF f])
have finite_IN: "d_IN f x ≠ ⊤" for x using weight_finite[of x]
by(rule neq_top_trans)(rule currentD_weight_IN[OF f])
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 chain: "Complete_Partial_Order.chain (≥) M" by(rule Chains_into_chain)
hence chain': "Complete_Partial_Order.chain (≤) M" by(simp add: chain_dual)
have countable': "countable (support_flow f)"
using current_support_flow[OF f] by(rule countable_subset)(rule countable)
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)
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)
have c: "current Γ (Inf M)" using g
proof(rule current_leI)
show "(Inf M) e ≤ g0 e" for e using g0 by(auto intro: INF_lower)
show "d_OUT (⨅M) x ≤ d_IN (⨅M) x" if "x ∉ A Γ" for x
by(auto 4 4 simp add: IN_M OUT_M leq_def intro!: INF_mono dest: Chains_FieldD[OF M] intro: currentD_OUT_IN[OF _ that])
qed
have INF_le_f: "Inf M e ≤ f e" for e using g0 by(auto intro!: INF_lower2 g0_le_f)
have eq: "ℰ (TER (Inf M)) = ℰ (TER f)" using f w INF_le_f
proof(rule essential_eq_leI; intro subsetI)
fix x
assume x: "x ∈ ℰ (TER f)"
hence "x ∈ SINK (Inf M)" using d_OUT_mono[of "Inf M" x f, OF INF_le_f]
by(auto simp add: SINK.simps)
moreover from x have "x ∈ SAT Γ g" if "g ∈ M" for g using Chains_FieldD[OF M that] by(auto simp add: leq_def)
hence "x ∈ SAT Γ (Inf M)" by(auto simp add: SAT.simps IN_M intro!: INF_greatest)
ultimately show "x ∈ TER (Inf M)" by auto
qed
have w': "wave Γ (Inf M)"
proof
have "separating Γ (ℰ (TER f))" by(rule separating_essential)(rule waveD_separating[OF w])
then show "separating Γ (TER (Inf M))" unfolding eq[symmetric] by(rule separating_weakening) auto
fix x
assume "x ∉ RF (TER (Inf M))"
hence "x ∉ RF (ℰ (TER (Inf M)))" unfolding RF_essential .
hence "x ∉ RF (TER f)" unfolding eq RF_essential .
hence "d_OUT f x = 0" by(rule waveD_OUT[OF w])
with d_OUT_mono[of _ x f, OF INF_le_f]
show "d_OUT (Inf M) x = 0" by (metis le_zero_eq)
qed
from c w' INF_le_f eq show ?thesis by simp
qed
define trim1
where "trim1 g =
(if trimming g then g
else let z = SOME z. z ∈ RF⇧∘ (TER g) ∧ z ∉ A Γ ∧ ¬ KIR g z;
factor = d_OUT g z / d_IN g z
in (λ(y, x). (if x = z then factor else 1) * g (y, x)))" for g
have increasing: "trim1 g ≤ g ∧ trim1 g ∈ F" if "g ∈ F" for g
proof(cases "trimming g")
case True
thus ?thesis using that by(simp add: trim1_def)
next
case False
let ?P = "λz. z ∈ RF⇧∘ (TER g) ∧ z ∉ A Γ ∧ ¬ KIR g z"
define z where "z = Eps ?P"
from that have g: "current Γ g" and w': "wave Γ g" and le_f: "⋀e. g e ≤ f e"
and ℰ: "ℰ (TER g) = ℰ (TER f)" by(auto simp add: le_fun_def)
{ with False obtain z where z: "z ∈ RF⇧∘ (TER f)" and A: "z ∉ A Γ" and neq: "d_OUT g z ≠ d_IN g z"
by(auto simp add: trimming.simps le_fun_def)
from z have "z ∈ RF⇧∘ (ℰ (TER f))" unfolding roofed_circ_essential .
with ℰ roofed_circ_essential[of Γ "TER g"] have "z ∈ RF⇧∘ (TER g)" by simp
with A neq have "∃x. ?P x" by auto }
hence "?P z" unfolding z_def by(rule someI_ex)
hence RF: "z ∈ RF⇧∘ (TER g)" and A: "z ∉ A Γ" and neq: "d_OUT g z ≠ d_IN g z" by simp_all
let ?factor = "d_OUT g z / d_IN g z"
have trim1 [simp]: "trim1 g (y, x) = (if x = z then ?factor else 1) * g (y, x)" for x y
using False by(auto simp add: trim1_def z_def Let_def)
from currentD_OUT_IN[OF g A] neq have less: "d_OUT g z < d_IN g z" by auto
hence "?factor ≤ 1" (is "?factor ≤ _")
by (auto intro!: divide_le_posI_ennreal simp: zero_less_iff_neq_zero)
hence le': "?factor * g (y, x) ≤ 1 * g (y, x)" for y x
by(rule mult_right_mono) simp
hence le: "trim1 g e ≤ g e" for e by(cases e)simp
moreover {
have c: "current Γ (trim1 g)" using g le
proof(rule current_leI)
fix x
assume x: "x ∉ A Γ"
have "d_OUT (trim1 g) x ≤ d_OUT g x" unfolding d_OUT_def using le' by(auto intro: nn_integral_mono)
also have "… ≤ d_IN (trim1 g) x"
proof(cases "x = z")
case True
have "d_OUT g x = d_IN (trim1 g) x" unfolding d_IN_def
using True currentD_weight_IN[OF g, of x] currentD_OUT_IN[OF g x]
apply (cases "d_IN g x = 0")
apply(auto simp add: nn_integral_divide nn_integral_cmult d_IN_def[symmetric] ennreal_divide_times)
apply (subst ennreal_divide_self)
apply (auto simp: less_top[symmetric] top_unique weight_finite)
done
thus ?thesis by simp
next
case False
have "d_OUT g x ≤ d_IN g x" using x by(rule currentD_OUT_IN[OF g])
also have "… ≤ d_IN (trim1 g) x" unfolding d_IN_def using False by(auto intro!: nn_integral_mono)
finally show ?thesis .
qed
finally show "d_OUT (trim1 g) x ≤ d_IN (trim1 g) x" .
qed
moreover have le_f: "trim1 g ≤ f" using le le_f by(blast intro: le_funI order_trans)
moreover have eq: "ℰ (TER (trim1 g)) = ℰ (TER f)" unfolding ℰ[symmetric] using g w' le
proof(rule essential_eq_leI; intro subsetI)
fix x
assume x: "x ∈ ℰ (TER g)"
hence "x ∈ SINK (trim1 g)" using d_OUT_mono[of "trim1 g" x g, OF le]
by(auto simp add: SINK.simps)
moreover from x have "x ≠ z" using RF by(auto simp add: roofed_circ_def)
hence "d_IN (trim1 g) x = d_IN g x" unfolding d_IN_def by simp
with ‹x ∈ ℰ (TER g)› have "x ∈ SAT Γ (trim1 g)" by(auto simp add: SAT.simps)
ultimately show "x ∈ TER (trim1 g)" by auto
qed
moreover have "wave Γ (trim1 g)"
proof
have "separating Γ (ℰ (TER f))" by(rule separating_essential)(rule waveD_separating[OF w])
then show "separating Γ (TER (trim1 g))" unfolding eq[symmetric] by(rule separating_weakening) auto
fix x
assume "x ∉ RF (TER (trim1 g))"
hence "x ∉ RF (ℰ (TER (trim1 g)))" unfolding RF_essential .
hence "x ∉ RF (TER f)" unfolding eq RF_essential .
hence "d_OUT f x = 0" by(rule waveD_OUT[OF w])
with d_OUT_mono[of _ x f, OF le_f[THEN le_funD]]
show "d_OUT (trim1 g) x = 0" by (metis le_zero_eq)
qed
ultimately have "trim1 g ∈ F" by(simp add: F_def) }
ultimately show ?thesis using that by(simp add: le_fun_def del: trim1)
qed
have "bourbaki_witt_fixpoint Inf leq trim1" using chainD increasing unfolding leq_def
by(intro bourbaki_witt_fixpoint_restrict_rel)(auto intro: Inf_greatest Inf_lower)
then interpret bourbaki_witt_fixpoint Inf leq trim1 .
have f_Field: "f ∈ Field leq" using f w by(simp add: leq_def)
define g where "g = fixp_above f"
have "g ∈ Field leq" using f_Field unfolding g_def by(rule fixp_above_Field)
hence le_f: "g ≤ f"
and g: "current Γ g"
and w': "wave Γ g"
and TER: "ℰ (TER g) = ℰ (TER f)" by(auto simp add: leq_def intro: le_funI)
have "trimming g"
proof(rule ccontr)
let ?P = "λx. x ∈ RF⇧∘ (TER g) ∧ x ∉ A Γ ∧ ¬ KIR g x"
define x where "x = Eps ?P"
assume False: "¬ ?thesis"
hence "∃x. ?P x" using le_f g w' TER
by(auto simp add: trimming.simps roofed_circ_essential[of Γ "TER g", symmetric] roofed_circ_essential[of Γ "TER f", symmetric])
hence "?P x" unfolding x_def by(rule someI_ex)
hence x: "x ∈ RF⇧∘ (TER g)" and A: "x ∉ A Γ" and neq: "d_OUT g x ≠ d_IN g x" by simp_all
from neq have "∃y. edge Γ y x ∧ g (y, x) > 0"
proof(rule contrapos_np)
assume "¬ ?thesis"
hence "d_IN g x = 0" using currentD_outside[OF g, of _ x]
by(force simp add: d_IN_def nn_integral_0_iff_AE AE_count_space not_less)
with currentD_OUT_IN[OF g A] show "KIR g x" by simp
qed
then obtain y where y: "edge Γ y x" and gr0: "g (y, x) > 0" by blast
have [simp]: "g (y, x) ≠ ⊤"
proof -
have "g (y, x) ≤ d_OUT g y" by (rule d_OUT_ge_point)
also have "… ≤ weight Γ y" by(rule currentD_weight_OUT[OF g])
also have "… < ⊤" by(simp add: weight_finite less_top[symmetric])
finally show ?thesis by simp
qed
from neq have factor: "d_OUT g x / d_IN g x ≠ 1"
by (simp add: divide_eq_1_ennreal)
have "trim1 g (y, x) = g (y, x) * (d_OUT g x / d_IN g x)"
by(clarsimp simp add: False trim1_def Let_def x_def[symmetric] mult.commute)
moreover have "… ≠ g (y, x) * 1" unfolding ennreal_mult_cancel_left using gr0 factor by auto
ultimately have "trim1 g (y, x) ≠ g (y, x)" by auto
hence "trim1 g ≠ g" by(auto simp add: fun_eq_iff)
moreover have "trim1 g = g" using f_Field unfolding g_def by(rule fixp_above_unfold[symmetric])
ultimately show False by contradiction
qed
then show ?thesis by blast
qed
end
lemma trimming_ℰ:
fixes Γ (structure)
assumes w: "wave Γ f" and trimming: "trimming Γ f g"
shows "ℰ (TER f) = ℰ (TER g)"
proof(rule set_eqI)
show "x ∈ ℰ (TER f) ⟷ x ∈ ℰ (TER g)" for x
proof(cases "x ∈ A Γ")
case False
thus ?thesis using trimmingD_ℰ[OF trimming] by blast
next
case True
show ?thesis
proof
assume x: "x ∈ ℰ (TER f)"
hence "x ∈ TER g" using d_OUT_mono[of g x f, OF trimmingD_le[OF trimming]] True
by(simp add: SINK.simps SAT.A)
moreover from x have "essential Γ (B Γ) (TER f) x" by simp
then obtain p y where p: "path Γ x p y" and y: "y ∈ B Γ"
and bypass: "⋀z. z ∈ set p ⟹ z ∉ RF (TER f)" by(rule essentialE_RF) blast
from p y have "essential Γ (B Γ) (ℰ (TER g)) x"
proof(rule essentialI)
fix z
assume "z ∈ set p"
hence z: "z ∉ RF (TER f)" by(rule bypass)
with waveD_separating[OF w, THEN separating_RF_A] have "z ∉ A Γ" by blast
with z have "z ∉ ℰ (TER g)" using trimmingD_ℰ[OF trimming] by(auto intro: roofed_greaterI)
thus "z = x ∨ z ∉ ℰ (TER g)" ..
qed
ultimately show "x ∈ ℰ (TER g)" unfolding essential_ℰ by simp
next
assume "x ∈ ℰ (TER g)"
then obtain p y where p: "path Γ x p y" and y: "y ∈ B Γ"
and bypass: "⋀z. z ∈ set p ⟹ z ∉ RF (TER g)" by(rule ℰ_E_RF) blast
have z: "z ∉ ℰ (TER f)" if "z ∈ set p" for z
proof -
from that have z: "z ∉ RF (TER g)" by(rule bypass)
with waveD_separating[OF trimmingD_wave[OF trimming], THEN separating_RF_A] have "z ∉ A Γ" by blast
with z show "z ∉ ℰ (TER f)" using trimmingD_ℰ[OF trimming] by(auto intro: roofed_greaterI)
qed
then have "essential Γ (B Γ) (ℰ (TER f)) x" by(intro essentialI[OF p y]) auto
moreover have "x ∈ TER f"
using waveD_separating[THEN separating_essential, THEN separatingD, OF w p True y] z
by auto
ultimately show "x ∈ ℰ (TER f)" unfolding essential_ℰ by simp
qed
qed
qed
subsection ‹Composition of waves via quotients›
definition quotient_web :: "('v, 'more) web_scheme ⇒ 'v current ⇒ ('v, 'more) web_scheme"
where
"quotient_web Γ f =
⦇edge = λx y. edge Γ x y ∧ x ∉ roofed_circ Γ (TER⇘Γ⇙ f) ∧ y ∉ roofed Γ (TER⇘Γ⇙ f),
weight = λx. if x ∈ RF⇧∘⇘Γ⇙ (TER⇘Γ⇙ f) ∨ x ∈ TER⇘Γ⇙ f ∩ B Γ then 0 else weight Γ x,
A = ℰ⇘Γ⇙ (TER⇘Γ⇙ f) - (B Γ - A Γ),
B = B Γ,
… = web.more Γ⦈"
lemma quotient_web_sel [simp]:
fixes Γ (structure) shows
"edge (quotient_web Γ f) x y ⟷ edge Γ x y ∧ x ∉ RF⇧∘ (TER f) ∧ y ∉ RF (TER f)"
"weight (quotient_web Γ f) x = (if x ∈ RF⇧∘ (TER f) ∨ x ∈ TER⇘Γ⇙ f ∩ B Γ then 0 else weight Γ x)"
"A (quotient_web Γ f) = ℰ (TER f)- (B Γ - A Γ)"
"B (quotient_web Γ f) = B Γ"
"web.more (quotient_web Γ f) = web.more Γ"
by(simp_all add: quotient_web_def)
lemma vertex_quotient_webD: fixes Γ (structure) shows
"vertex (quotient_web Γ f) x ⟹ vertex Γ x ∧ x ∉ RF⇧∘ (TER f)"
by(auto simp add: vertex_def roofed_circ_def)
lemma path_quotient_web:
fixes Γ (structure)
assumes "path Γ x p y"
and "x ∉ RF⇧∘ (TER f)"
and "⋀z. z ∈ set p ⟹ z ∉ RF (TER f)"
shows "path (quotient_web Γ f) x p y"
using assms by(induction)(auto intro: rtrancl_path.intros simp add: roofed_circ_def)
definition restrict_current :: "('v, 'more) web_scheme ⇒ 'v current ⇒ 'v current ⇒ 'v current"
where "restrict_current Γ f g = (λ(x, y). g (x, y) * indicator (- RF⇧∘⇘Γ⇙ (TER⇘Γ⇙ f)) x * indicator (- RF⇘Γ⇙ (TER⇘Γ⇙ f)) y)"
abbreviation restrict_curr :: "'v current ⇒ ('v, 'more) web_scheme ⇒ 'v current ⇒ 'v current" (‹_ ↿ _ '/ _› [100, 0, 100] 100)
where "restrict_curr g Γ f ≡ restrict_current Γ f g"
lemma restrict_current_simps [simp]: fixes Γ (structure) shows
"(g ↿ Γ / f) (x, y) = (g (x, y) * indicator (- RF⇧∘ (TER f)) x * indicator (- RF (TER f)) y)"
by(simp add: restrict_current_def)
lemma d_OUT_restrict_current_outside: fixes Γ (structure) shows
"x ∈ RF⇧∘ (TER f) ⟹ d_OUT (g ↿ Γ / f) x = 0"
by(simp add: d_OUT_def)
lemma d_IN_restrict_current_outside: fixes Γ (structure) shows
"x ∈ RF (TER f) ⟹ d_IN (g ↿ Γ / f) x = 0"
by(simp add: d_IN_def)
lemma restrict_current_le: "(g ↿ Γ / f) e ≤ g e"
by(cases e)(clarsimp split: split_indicator)
lemma d_OUT_restrict_current_le: "d_OUT (g ↿ Γ / f) x ≤ d_OUT g x"
unfolding d_OUT_def by(rule nn_integral_mono, simp split: split_indicator)
lemma d_IN_restrict_current_le: "d_IN (g ↿ Γ / f) x ≤ d_IN g x"
unfolding d_IN_def by(rule nn_integral_mono, simp split: split_indicator)
lemma restrict_current_IN_not_RF:
fixes Γ (structure)
assumes g: "current Γ g"
and x: "x ∉ RF (TER f)"
shows "d_IN (g ↿ Γ / f) x = d_IN g x"
proof -
{
fix y
assume y: "y ∈ RF⇧∘ (TER f)"
have "g (y, x) = 0"
proof(cases "edge Γ y x")
case True
from y have y': "y ∈ RF (TER f)" and essential: "y ∉ ℰ (TER f)" by(simp_all add: roofed_circ_def)
moreover from x obtain p z where z: "z ∈ B Γ" and p: "path Γ x p z"
and bypass: "⋀z. z ∈ set p ⟹ z ∉ TER f" "x ∉ TER f"
by(clarsimp simp add: roofed_def)
from roofedD[OF y' rtrancl_path.step, OF True p z] bypass have "x ∈ TER f ∨ y ∈ TER f" by auto
with roofed_greater[THEN subsetD, of x "TER f" Γ] x have "x ∉ TER f" "y ∈ TER f" by auto
with essential bypass have False
by(auto dest!: not_essentialD[OF _ rtrancl_path.step, OF _ True p z])
thus ?thesis ..
qed(simp add: currentD_outside[OF g]) }
then show ?thesis unfolding d_IN_def
using x by(auto intro!: nn_integral_cong split: split_indicator)
qed
lemma restrict_current_IN_A:
"a ∈ A (quotient_web Γ f) ⟹ d_IN (g ↿ Γ / f) a = 0"
by(simp add: d_IN_restrict_current_outside roofed_greaterI)
lemma restrict_current_nonneg: "0 ≤ g e ⟹ 0 ≤ (g ↿ Γ / f) e"
by(cases e) simp
lemma in_SINK_restrict_current: "x ∈ SINK g ⟹ x ∈ SINK (g ↿ Γ / f)"
using d_OUT_restrict_current_le[of Γ f g x]
by(simp add: SINK.simps)
lemma SAT_restrict_current:
fixes Γ (structure)
assumes f: "current Γ f"
and g: "current Γ g"
shows "SAT (quotient_web Γ f) (g ↿ Γ / f) = RF (TER f) ∪ (SAT Γ g - A Γ)" (is "SAT ?Γ ?g = ?rhs")
proof(intro set_eqI iffI; (elim UnE DiffE)?)
show "x ∈ ?rhs" if "x ∈ SAT ?Γ ?g" for x using that
proof cases
case IN
thus ?thesis using currentD_weight_OUT[OF f, of x]
by(cases "x ∈ RF (TER f)")(auto simp add: d_IN_restrict_current_outside roofed_circ_def restrict_current_IN_not_RF[OF g] SAT.IN currentD_IN[OF g] roofed_greaterI SAT.A SINK.simps RF_in_B split: if_split_asm intro: essentialI[OF rtrancl_path.base])
qed(simp add: roofed_greaterI)
show "x ∈ SAT ?Γ ?g" if "x ∈ RF (TER f)" for x using that
by(auto simp add: SAT.simps roofed_circ_def d_IN_restrict_current_outside)
show "x ∈ SAT ?Γ ?g" if "x ∈ SAT Γ g" "x ∉ A Γ" for x using that
by(auto simp add: SAT.simps roofed_circ_def d_IN_restrict_current_outside restrict_current_IN_not_RF[OF g])
qed
lemma current_restrict_current:
fixes Γ (structure)
assumes w: "wave Γ f"
and g: "current Γ g"
shows "current (quotient_web Γ f) (g ↿ Γ / f)" (is "current ?Γ ?g")
proof
show "d_OUT ?g x ≤ weight ?Γ x" for x
using d_OUT_restrict_current_le[of Γ f g x] currentD_weight_OUT[OF g, of x] currentD_OUT[OF g, of x]
by(auto simp add: d_OUT_restrict_current_outside)
show "d_IN ?g x ≤ weight ?Γ x" for x
using d_IN_restrict_current_le[of Γ f g x] currentD_weight_IN[OF g, of x]
by(auto simp add: d_IN_restrict_current_outside roofed_circ_def)
(subst d_IN_restrict_current_outside[of x Γ f g]; simp add: roofed_greaterI)
fix x
assume "x ∉ A ?Γ"
hence x: "x ∉ ℰ (TER f) - B Γ" by simp
show "d_OUT ?g x ≤ d_IN ?g x"
proof(cases "x ∈ RF (TER f)")
case True
with x have "x ∈ RF⇧∘ (TER f) ∪ B Γ" by(simp add: roofed_circ_def)
with True show ?thesis using currentD_OUT[OF g, of x] d_OUT_restrict_current_le[of Γ f g x]
by(auto simp add: d_OUT_restrict_current_outside d_IN_restrict_current_outside)
next
case False
then obtain p z where z: "z ∈ B Γ" and p: "path Γ x p z"
and bypass: "⋀z. z ∈ set p ⟹ z ∉ TER f" "x ∉ TER f"
by(clarsimp simp add: roofed_def)
from g False have "d_IN ?g x = d_IN g x" by(rule restrict_current_IN_not_RF)
moreover have "d_OUT ?g x ≤ d_OUT g x"
by(rule d_OUT_mono restrict_current_le)+
moreover have "x ∉ A Γ"
using separatingD[OF waveD_separating[OF w] p _ z] bypass by blast
note currentD_OUT_IN[OF g this]
ultimately show ?thesis by simp
qed
next
show "d_IN ?g a = 0" if "a ∈ A ?Γ" for a using that by(rule restrict_current_IN_A)
show "d_OUT ?g b = 0" if "b ∈ B ?Γ" for b
using d_OUT_restrict_current_le[of Γ f g b] currentD_OUT[OF g, of b] that by simp
show "?g e = 0" if "e ∉ ❙E⇘?Γ⇙" for e using that currentD_outside'[OF g, of e]
by(cases e)(auto split: split_indicator)
qed
lemma TER_restrict_current:
fixes Γ (structure)
assumes f: "current Γ f"
and w: "wave Γ f"
and g: "current Γ g"
shows "TER g ⊆ TER⇘quotient_web Γ f⇙ (g ↿ Γ / f)" (is "_ ⊆ ?TER" is "_ ⊆ TER⇘?Γ⇙ ?g")
proof
fix x
assume x: "x ∈ TER g"
hence "x ∈ SINK ?g" by(simp add: in_SINK_restrict_current)
moreover have "x ∈ RF (TER f)" if "x ∈ A Γ"
using waveD_separating[OF w, THEN separatingD, OF _ that] by(rule roofedI)
then have "x ∈ SAT ?Γ ?g" using SAT_restrict_current[OF f g] x by auto
ultimately show "x ∈ ?TER" by simp
qed
lemma wave_restrict_current:
fixes Γ (structure)
assumes f: "current Γ f"
and w: "wave Γ f"
and g: "current Γ g"
and w': "wave Γ g"
shows "wave (quotient_web Γ f) (g ↿ Γ / f)" (is "wave ?Γ ?g")
proof
show "separating ?Γ (TER⇘?Γ⇙ ?g)" (is "separating _ ?TER")
proof
fix x y p
assume "x ∈ A ?Γ" "y ∈ B ?Γ" and p: "path ?Γ x p y"
hence x: "x ∈ ℰ (TER f)" and y: "y ∈ B Γ" and SAT: "x ∈ SAT ?Γ ?g" by(simp_all add: SAT.A)
from p have p': "path Γ x p y" by(rule rtrancl_path_mono) simp
{ assume "x ∉ ?TER"
hence "x ∉ SINK ?g" using SAT by(simp)
hence "x ∉ SINK g" using d_OUT_restrict_current_le[of Γ f g x]
by(auto simp add: SINK.simps)
hence "x ∈ RF (TER g)" using waveD_OUT[OF w'] by(auto simp add: SINK.simps)
from roofedD[OF this p' y] ‹x ∉ SINK g› have "(∃z∈set p. z ∈ ?TER)"
using TER_restrict_current[OF f w g] by blast }
then show "(∃z∈set p. z ∈ ?TER) ∨ x ∈ ?TER" by blast
qed
fix x
assume "x ∉ RF⇘?Γ⇙ ?TER"
hence "x ∉ RF (TER g)"
proof(rule contrapos_nn)
assume *: "x ∈ RF (TER g)"
show "x ∈ RF⇘?Γ⇙ ?TER"
proof
fix p y
assume "path ?Γ x p y" "y ∈ B ?Γ"
hence "path Γ x p y" "y ∈ B Γ" by(auto elim: rtrancl_path_mono)
from roofedD[OF * this] show "(∃z∈set p. z ∈ ?TER) ∨ x ∈ ?TER"
using TER_restrict_current[OF f w g] by blast
qed
qed
with w' have "d_OUT g x = 0" by(rule waveD_OUT)
with d_OUT_restrict_current_le[of Γ f g x]
show "d_OUT ?g x = 0" by simp
qed
definition plus_current :: "'v current ⇒ 'v current ⇒ 'v current"
where "plus_current f g = (λe. f e + g e)"
lemma plus_current_simps [simp]: "plus_current f g e = f e + g e"
by(simp add: plus_current_def)
lemma plus_zero_current [simp]: "plus_current f zero_current = f"
by(simp add: fun_eq_iff)
lemma support_flow_plus_current: "support_flow (plus_current f g) ⊆ support_flow f ∪ support_flow g"
by(clarsimp simp add: support_flow.simps)
context
fixes Γ :: "('v, 'more) web_scheme" (structure) and f g
assumes f: "current Γ f"
and w: "wave Γ f"
and g: "current (quotient_web Γ f) g"
begin
lemma OUT_plus_current: "d_OUT (plus_current f g) x = (if x ∈ RF⇧∘ (TER f) then d_OUT f x else d_OUT g x)" (is "d_OUT ?g _ = _")
proof -
have "d_OUT ?g x = d_OUT f x + d_OUT g x" unfolding plus_current_def
by(subst d_OUT_add) simp_all
also have "… = (if x ∈ RF⇧∘ (TER f) then d_OUT f x else d_OUT g x)"
proof(cases "x ∈ RF⇧∘ (TER f)")
case True
hence "d_OUT g x = 0" by(intro currentD_outside_OUT[OF g])(auto dest: vertex_quotient_webD)
thus ?thesis using True by simp
next
case False
hence "d_OUT f x = 0" by(auto simp add: roofed_circ_def SINK.simps dest: waveD_OUT[OF w])
with False show ?thesis by simp
qed
finally show ?thesis .
qed
lemma IN_plus_current: "d_IN (plus_current f g) x = (if x ∈ RF (TER f) then d_IN f x else d_IN g x)" (is "d_IN ?g _ = _")
proof -
have "d_IN ?g x = d_IN f x + d_IN g x" unfolding plus_current_def
by(subst d_IN_add) simp_all
also consider (RF) "x ∈ RF (TER f) - (B Γ - A Γ)" | (B) "x ∈ RF (TER f)" "x ∈ B Γ - A Γ" | (beyond) "x ∉ RF (TER f)" by blast
then have "d_IN f x + d_IN g x = (if x ∈ RF (TER f) then d_IN f x else d_IN g x)"
proof(cases)
case RF
hence "d_IN g x = 0"
by(cases "x ∈ ℰ (TER f)")(auto intro: currentD_outside_IN[OF g] currentD_IN[OF g] dest!: vertex_quotient_webD simp add: roofed_circ_def)
thus ?thesis using RF by simp
next
case B
hence "d_IN g x = 0" using currentD_outside_IN[OF g, of x] currentD_weight_IN[OF g, of x]
by(auto dest: vertex_quotient_webD simp add: roofed_circ_def)
with B show ?thesis by simp
next
case beyond
from f w beyond have "d_IN f x = 0" by(rule wave_not_RF_IN_zero)
with beyond show ?thesis by simp
qed
finally show ?thesis .
qed
lemma in_TER_plus_current:
assumes RF: "x ∉ RF⇧∘ (TER f)"
and x: "x ∈ TER⇘quotient_web Γ f⇙ g" (is "_ ∈ ?TER _")
shows "x ∈ TER (plus_current f g)" (is "_ ∈ TER ?g")
proof(cases "x ∈ ℰ (TER f) - (B Γ - A Γ)")
case True
with x show ?thesis using currentD_IN[OF g, of x]
by(fastforce intro: roofed_greaterI SAT.intros simp add: SINK.simps OUT_plus_current IN_plus_current elim!: SAT.cases)
next
case *: False
have "x ∈ SAT Γ ?g"
proof(cases "x ∈ B Γ - A Γ")
case False
with x RF * have "weight Γ x ≤ d_IN g x"
by(auto elim!: SAT.cases split: if_split_asm simp add: essential_BI)
also have "… ≤ d_IN ?g x" unfolding plus_current_def by(intro d_IN_mono) simp
finally show ?thesis ..
next
case True
with * x have "weight Γ x ≤ d_IN ?g x" using currentD_OUT[OF f, of x]
by(auto simp add: IN_plus_current RF_in_B SINK.simps roofed_circ_def elim!: SAT.cases split: if_split_asm)
thus ?thesis ..
qed
moreover have "x ∈ SINK ?g" using x by(simp add: SINK.simps OUT_plus_current RF)
ultimately show ?thesis by simp
qed
lemma current_plus_current: "current Γ (plus_current f g)" (is "current _ ?g")
proof
show "d_OUT ?g x ≤ weight Γ x" for x
using currentD_weight_OUT[OF g, of x] currentD_weight_OUT[OF f, of x]
by(auto simp add: OUT_plus_current split: if_split_asm elim: order_trans)
show "d_IN ?g x ≤ weight Γ x" for x
using currentD_weight_IN[OF f, of x] currentD_weight_IN[OF g, of x]
by(auto simp add: IN_plus_current roofed_circ_def split: if_split_asm elim: order_trans)
show "d_OUT ?g x ≤ d_IN ?g x" if "x ∉ A Γ" for x
proof(cases "x ∈ ℰ (TER f)")
case False
thus ?thesis
using currentD_OUT_IN[OF f that] currentD_OUT_IN[OF g, of x] that
by(auto simp add: OUT_plus_current IN_plus_current roofed_circ_def SINK.simps)
next
case True
with that have "d_OUT f x = 0" "weight Γ x ≤ d_IN f x"
by(auto simp add: SINK.simps elim: SAT.cases)
thus ?thesis using that True currentD_OUT_IN[OF g, of x] currentD_weight_OUT[OF g, of x]
by(auto simp add: OUT_plus_current IN_plus_current roofed_circ_def intro: roofed_greaterI split: if_split_asm)
qed
show "d_IN ?g a = 0" if "a ∈ A Γ" for a
using wave_A_in_RF[OF w that] currentD_IN[OF f that] by(simp add: IN_plus_current)
show "d_OUT ?g b = 0" if "b ∈ B Γ" for b
using that currentD_OUT[OF f that] currentD_OUT[OF g, of b] that
by(auto simp add: OUT_plus_current SINK.simps roofed_circ_def intro: roofed_greaterI)
show "?g e = 0" if "e ∉ ❙E" for e using currentD_outside'[OF f, of e] currentD_outside'[OF g, of e] that
by(cases e) auto
qed
context
assumes w': "wave (quotient_web Γ f) g"
begin
lemma separating_TER_plus_current:
assumes x: "x ∈ RF (TER f)" and y: "y ∈ B Γ" and p: "path Γ x p y"
shows "(∃z∈set p. z ∈ TER (plus_current f g)) ∨ x ∈ TER (plus_current f g)" (is "_ ∨ _ ∈ TER ?g")
proof -
from x have "x ∈ RF (ℰ (TER f))" unfolding RF_essential .
from roofedD[OF this p y] have "∃z∈set (x # p). z ∈ ℰ (TER f)" by auto
from split_list_last_prop[OF this] obtain ys z zs
where decomp: "x # p = ys @ z # zs" and z: "z ∈ ℰ (TER f)"
and outside: "⋀z. z ∈ set zs ⟹ z ∉ ℰ (TER f)" by auto
have zs: "path Γ z zs y" using decomp p
by(cases ys)(auto elim: rtrancl_path_appendE)
moreover have "z ∉ RF⇧∘ (TER f)" using z by(simp add: roofed_circ_def)
moreover have RF: "z' ∉ RF (TER f)" if "z' ∈ set zs" for z'
proof
assume "z' ∈ RF (TER f)"
hence z': "z' ∈ RF (ℰ (TER f))" by(simp only: RF_essential)
from split_list[OF that] obtain ys' zs' where decomp': "zs = ys' @ z' # zs'" by blast
with zs have "path Γ z' zs' y" by(auto elim: rtrancl_path_appendE)
from roofedD[OF z' this y] outside decomp' show False by auto
qed
ultimately have p': "path (quotient_web Γ f) z zs y" by(rule path_quotient_web)
show ?thesis
proof(cases "z ∈ B Γ - A Γ")
case False
with separatingD[OF waveD_separating[OF w'] p'] z y
obtain z' where z': "z' ∈ set (z # zs)" and TER: "z' ∈ TER⇘quotient_web Γ f⇙ g" by auto
hence "z' ∈ TER ?g" using in_TER_plus_current[of z'] RF[of z'] ‹z ∉ RF⇧∘ (TER f)› by(auto simp add: roofed_circ_def)
with decomp z' show ?thesis by(cases ys) auto
next
case True
hence "z ∈ TER ?g" using currentD_OUT[OF current_plus_current, of z] z
by(auto simp add: SINK.simps SAT.simps IN_plus_current intro: roofed_greaterI)
then show ?thesis using decomp by(cases ys) auto
qed
qed
lemma wave_plus_current: "wave Γ (plus_current f g)" (is "wave _ ?g")
proof
let ?Γ = "quotient_web Γ f"
let ?TER = "TER⇘?Γ⇙"
show "separating Γ (TER ?g)" using separating_TER_plus_current[OF wave_A_in_RF[OF w]] by(rule separating)
fix x
assume x: "x ∉ RF (TER ?g)"
hence "x ∉ RF (TER f)" by(rule contrapos_nn)(rule roofedI, rule separating_TER_plus_current)
hence *: "x ∉ RF⇧∘ (TER f)" by(simp add: roofed_circ_def)
moreover have "x ∉ RF⇘?Γ⇙ (?TER g)"
proof
assume RF': "x ∈ RF⇘?Γ⇙ (?TER g)"
from x obtain p y where y: "y ∈ B Γ" and p: "path Γ x p y"
and bypass: "⋀z. z ∈ set p ⟹ z ∉ TER ?g" and x': "x ∉ TER ?g"
by(auto simp add: roofed_def)
have RF: "z ∉ RF (TER f)" if "z ∈ set p" for z
proof
assume z: "z ∈ RF (TER f)"
from split_list[OF that] obtain ys' zs' where decomp: "p = ys' @ z # zs'" by blast
with p have "path Γ z zs' y" by(auto elim: rtrancl_path_appendE)
from separating_TER_plus_current[OF z y this] decomp bypass show False by auto
qed
with p have "path ?Γ x p y" using *
by(induction)(auto intro: rtrancl_path.intros simp add: roofed_circ_def)
from roofedD[OF RF' this] y consider (x) "x ∈ ?TER g" | (z) z where "z ∈ set p" "z ∈ ?TER g" by auto
then show False
proof(cases)
case x
with * have "x ∈ TER ?g" by(rule in_TER_plus_current)
with x' show False by contradiction
next
case (z z)
from z(1) have "z ∉ RF (TER f)" by(rule RF)
hence "z ∉ RF⇧∘ (TER f)" by(simp add: roofed_circ_def)
hence "z ∈ TER ?g" using z(2) by(rule in_TER_plus_current)
moreover from z(1) have "z ∉ TER ?g" by(rule bypass)
ultimately show False by contradiction
qed
qed
with w' have "d_OUT g x = 0" by(rule waveD_OUT)
ultimately show "d_OUT ?g x = 0" by(simp add: OUT_plus_current)
qed
end
end
lemma loose_quotient_web:
fixes Γ :: "('v, 'more) web_scheme" (structure)
assumes weight_finite: "⋀x. weight Γ x ≠ ⊤"
and f: "current Γ f"
and w: "wave Γ f"
and maximal: "⋀w. ⟦ current Γ w; wave Γ w; f ≤ w ⟧ ⟹ f = w"
shows "loose (quotient_web Γ f)" (is "loose ?Γ")
proof
fix g
assume g: "current ?Γ g" and w': "wave ?Γ g"
let ?g = "plus_current f g"
from f w g have "current Γ ?g" "wave Γ ?g" by(rule current_plus_current wave_plus_current)+ (rule w')
moreover have "f ≤ ?g" by(clarsimp simp add: le_fun_def add_eq_0_iff_both_eq_0)
ultimately have eq: "f = ?g" by(rule maximal)
have "g e = 0" for e
proof(cases e)
case (Pair x y)
have "f e ≤ d_OUT f x" unfolding Pair by (rule d_OUT_ge_point)
also have "… ≤ weight Γ x" by(rule currentD_weight_OUT[OF f])
also have "… < ⊤" by(simp add: weight_finite less_top[symmetric])
finally show "g e = 0" using Pair eq[THEN fun_cong, of e]
by(cases "f e" "g e" rule: ennreal2_cases)(simp_all add: fun_eq_iff)
qed
thus "g = (λ_. 0)" by(simp add: fun_eq_iff)
next
have 0: "current ?Γ zero_current" by simp
show "¬ hindrance ?Γ zero_current"
proof
assume "hindrance ?Γ zero_current"
then obtain x where a: "x ∈ A ?Γ" and ℰ: "x ∉ ℰ⇘?Γ⇙ (TER⇘?Γ⇙ zero_current)"
and "d_OUT zero_current x < weight ?Γ x" by cases
from a have "x ∈ ℰ (TER f)" by simp
then 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" by(rule ℰ_E) blast
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)
note p'
moreover have RF: "z ∉ RF (TER f)" if "z ∈ set p'" for z
proof
assume z: "z ∈ RF (TER f)"
from split_list[OF that] obtain ys zs where decomp: "p' = ys @ z # zs" by blast
with p' have "y ∈ set p'" by(auto dest!: rtrancl_path_last intro: last_in_set)
with distinct have neq: "x ≠ y" by auto
from decomp p' have "path Γ z zs y" by(auto elim: rtrancl_path_appendE)
from roofedD[OF z this y] obtain z' where "z' ∈ set (z # zs)" "z' ∈ TER f" by auto
with distinct decomp subset bypass[OF neq] show False by auto
qed
moreover have "x ∉ RF⇧∘ (TER f)" using ‹x ∈ ℰ (TER f)› by(simp add: roofed_circ_def)
ultimately have p'': "path ?Γ x p' y"
by(induction)(auto intro: rtrancl_path.intros simp add: roofed_circ_def)
from a ℰ have "¬ essential ?Γ (B ?Γ) (TER⇘?Γ⇙ zero_current) x" by simp
from not_essentialD[OF this p''] y obtain z where neq: "x ≠ y"
and "z ∈ set p'" "z ≠ x" "z ∈ TER⇘?Γ⇙ zero_current" by auto
moreover with subset RF[of z] have "z ∈ TER f"
using currentD_weight_OUT[OF f, of z] currentD_weight_IN[OF f, of z]
by(auto simp add: roofed_circ_def SINK.simps intro: SAT.IN split: if_split_asm)
ultimately show False using bypass[of z] subset by auto
qed
qed
lemma quotient_web_trimming:
fixes Γ (structure)
assumes w: "wave Γ f"
and trimming: "trimming Γ f g"
shows "quotient_web Γ f = quotient_web Γ g" (is "?lhs = ?rhs")
proof(rule web.equality)
from trimming have ℰ: "ℰ (TER g) - A Γ = ℰ (TER f) - A Γ" by cases
have RF: "RF (TER g) = RF (TER f)"
by(subst (1 2) RF_essential[symmetric])(simp only: trimming_ℰ[OF w trimming])
have RFc: "RF⇧∘ (TER g) = RF⇧∘ (TER f)"
by(subst (1 2) roofed_circ_essential[symmetric])(simp only: trimming_ℰ[OF w trimming])
show "edge ?lhs = edge ?rhs" by(rule ext)+(simp add: RF RFc)
have "weight ?lhs = (λx. if x ∈ RF⇧∘ (TER g) ∨ x ∈ RF (TER g) ∩ B Γ then 0 else weight Γ x)"
unfolding RF RFc by(auto simp add: fun_eq_iff RF_in_B)
also have "… = weight ?rhs" by(auto simp add: fun_eq_iff RF_in_B)
finally show "weight ?lhs = weight ?rhs" .
show "A ?lhs = A ?rhs" unfolding quotient_web_sel trimming_ℰ[OF w trimming] ..
qed simp_all
subsection ‹Well-formed webs›
locale web =
fixes Γ :: "('v, 'more) web_scheme" (structure)
assumes A_in: "x ∈ A Γ ⟹ ¬ edge Γ y x"
and B_out: "x ∈ B Γ ⟹ ¬ edge Γ x y"
and A_vertex: "A Γ ⊆ ❙V"
and disjoint: "A Γ ∩ B Γ = {}"
and no_loop: "⋀x. ¬ edge Γ x x"
and weight_outside: "⋀x. x ∉ ❙V ⟹ weight Γ x = 0"
and weight_finite [simp]: "⋀x. weight Γ x ≠ ⊤"
begin
lemma web_weight_update:
assumes "⋀x. ¬ vertex Γ x ⟹ w x = 0"
and "⋀x. w x ≠ ⊤"
shows "web (Γ⦇weight := w⦈)"
by unfold_locales(simp_all add: A_in B_out A_vertex disjoint no_loop assms)
lemma currentI [intro?]:
assumes "⋀x. d_OUT f x ≤ weight Γ x"
and "⋀x. d_IN f x ≤ weight Γ x"
and OUT_IN: "⋀x. ⟦ x ∉ A Γ; x ∉ B Γ ⟧ ⟹ d_OUT f x ≤ d_IN f x"
and outside: "⋀e. e ∉ ❙E ⟹ f e = 0"
shows "current Γ f"
proof
show "d_IN f a = 0" if "a ∈ A Γ" for a using that
by(auto simp add: d_IN_def nn_integral_0_iff emeasure_count_space_eq_0 A_in intro: outside)
show "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 B_out intro: outside)
then show "d_OUT f x ≤ d_IN f x" if "x ∉ A Γ" for x using OUT_IN[OF that]
by(cases "x ∈ B Γ") auto
qed(blast intro: assms)+
lemma currentD_finite_IN:
assumes f: "current Γ f"
shows "d_IN f x ≠ ⊤"
proof(cases "x ∈ ❙V")
case True
have "d_IN f x ≤ weight Γ x" using f by(rule currentD_weight_IN)
also have "… < ⊤" using True weight_finite[of x] by (simp add: less_top[symmetric])
finally show ?thesis by simp
next
case False
then have "d_IN f x = 0"
by(auto simp add: d_IN_def nn_integral_0_iff emeasure_count_space_eq_0 vertex_def intro: currentD_outside[OF f])
thus ?thesis by simp
qed
lemma currentD_finite_OUT:
assumes f: "current Γ f"
shows "d_OUT f x ≠ ⊤"
proof(cases "x ∈ ❙V")
case True
have "d_OUT f x ≤ weight Γ x" using f by(rule currentD_weight_OUT)
also have "… < ⊤" using True weight_finite[of x] by (simp add: less_top[symmetric])
finally show ?thesis by simp
next
case False
then have "d_OUT f x = 0"
by(auto simp add: d_OUT_def nn_integral_0_iff emeasure_count_space_eq_0 vertex_def intro: currentD_outside[OF f])
thus ?thesis by simp
qed
lemma currentD_finite:
assumes f: "current Γ f"
shows "f e ≠ ⊤"
proof(cases e)
case (Pair x y)
have "f (x, y) ≤ d_OUT f x" by (rule d_OUT_ge_point)
also have "… < ⊤" using currentD_finite_OUT[OF f] by (simp add: less_top[symmetric])
finally show ?thesis by(simp add: Pair)
qed
lemma web_quotient_web: "web (quotient_web Γ f)" (is "web ?Γ")
proof
show "¬ edge ?Γ y x" if "x ∈ A ?Γ" for x y using that by(auto intro: roofed_greaterI)
show "¬ edge ?Γ x y" if "x ∈ B ?Γ" for x y using that by(auto simp add: B_out)
show "A ?Γ ∩ B ?Γ = {}" using disjoint by auto
show "A ?Γ ⊆ ❙V⇘?Γ⇙"
proof
fix x
assume "x ∈ A ?Γ"
hence ℰ: "x ∈ ℰ (TER f)" and x: "x ∉ B Γ" using disjoint by auto
from this(1) obtain p y where p: "path Γ x p y" and y: "y ∈ B Γ" and bypass: "⋀z. z ∈ set p ⟹ z ∉ RF (TER f)"
by(rule ℰ_E_RF) blast
from p y x have "p ≠ []" by(auto simp add: rtrancl_path_simps)
with rtrancl_path_nth[OF p, of 0] have "edge Γ x (p ! 0)" by simp
moreover have "x ∉ RF⇧∘ (TER f)" using ℰ by(simp add: roofed_circ_def)
moreover have "p ! 0 ∉ RF (TER f)" using bypass ‹p ≠ []› by auto
ultimately have "edge ?Γ x (p ! 0)" by simp
thus "x ∈ ❙V⇘?Γ⇙" by(auto intro: vertexI1)
qed
show "¬ edge ?Γ x x" for x by(simp add: no_loop)
show "weight ?Γ x = 0" if "x ∉ ❙V⇘?Γ⇙" for x
proof(cases "x ∈ RF⇧∘ (TER f) ∨ x ∈ TER f ∩ B Γ")
case True thus ?thesis by simp
next
case False
hence RF: "x ∉ RF⇧∘ (TER f)" and B: "x ∈ B Γ ⟹ x ∉ TER f" by auto
from RF obtain p y where p: "path Γ x p y" and y: "y ∈ B Γ" and bypass: "⋀z. z ∈ set p ⟹ z ∉ RF (TER f)"
apply(cases "x ∉ RF (RF (TER f))")
apply(auto elim!: not_roofedE)[1]
apply(auto simp add: roofed_circ_def roofed_idem elim: essentialE_RF)
done
from that have "p = []" using p y B RF bypass
by(auto 4 3 simp add: vertex_def dest!: rtrancl_path_nth[where i=0])
with p have xy: "x = y" by(simp add: rtrancl_path_simps)
with B y have "x ∉ TER f" by simp
hence RF': "x ∉ RF (TER f)" using xy y by(subst RF_in_B) auto
have "¬ vertex Γ x"
proof
assume "vertex Γ x"
then obtain x' where "edge Γ x' x" using xy y by(auto simp add: vertex_def B_out)
moreover hence "x' ∉ RF⇧∘ (TER f)" using RF' by(auto dest: RF_circ_edge_forward)
ultimately have "edge ?Γ x' x" using RF' by simp
hence "vertex ?Γ x" by(rule vertexI2)
with that show False by simp
qed
thus ?thesis by(simp add: weight_outside)
qed
show "weight ?Γ x ≠ ⊤" for x by simp
qed
end
locale countable_web = web Γ
for Γ :: "('v, 'more) web_scheme" (structure)
+
assumes countable [simp]: "countable ❙E"
begin
lemma countable_V [simp]: "countable ❙V"
by(simp add: "❙V_def")
lemma countable_web_quotient_web: "countable_web (quotient_web Γ f)" (is "countable_web ?Γ")
proof -
interpret r: web ?Γ by(rule web_quotient_web)
show ?thesis
proof
have "❙E⇘?Γ⇙ ⊆ ❙E" by auto
then show "countable ❙E⇘?Γ⇙" by(rule countable_subset) simp
qed
qed
end
subsection ‹Subtraction of a wave›
definition minus_web :: "('v, 'more) web_scheme ⇒ 'v current ⇒ ('v, 'more) web_scheme" (infixl ‹⊖› 65)
where "Γ ⊖ f = Γ⦇weight := λx. if x ∈ A Γ then weight Γ x - d_OUT f x else weight Γ x + d_OUT f x - d_IN f x⦈"
lemma minus_web_sel [simp]:
"edge (Γ ⊖ f) = edge Γ"
"weight (Γ ⊖ f) x = (if x ∈ A Γ then weight Γ x - d_OUT f x else weight Γ x + d_OUT f x - d_IN f x)"
"A (Γ ⊖ f) = A Γ"
"B (Γ ⊖ f) = B Γ"
"❙V⇘Γ ⊖ f⇙ = ❙V⇘Γ⇙"
"❙E⇘Γ ⊖ f⇙ = ❙E⇘Γ⇙"
"web.more (Γ ⊖ f) = web.more Γ"
by(auto simp add: minus_web_def vertex_def)
lemma vertex_minus_web [simp]: "vertex (Γ ⊖ f) = vertex Γ"
by(simp add: vertex_def fun_eq_iff)
lemma roofed_gen_minus_web [simp]: "roofed_gen (Γ ⊖ f) = roofed_gen Γ"
by(simp add: fun_eq_iff roofed_def)
lemma minus_zero_current [simp]: "Γ ⊖ zero_current = Γ"
by(rule web.equality)(simp_all add: fun_eq_iff)
lemma (in web) web_minus_web:
assumes f: "current Γ f"
shows "web (Γ ⊖ f)"
unfolding minus_web_def
apply(rule web_weight_update)
apply(auto simp: weight_outside currentD_weight_IN[OF f] currentD_outside_OUT[OF f]
currentD_outside_IN[OF f] currentD_weight_OUT[OF f] currentD_finite_OUT[OF f])
done
subsection ‹Bipartite webs›
locale countable_bipartite_web =
fixes Γ :: "('v, 'more) web_scheme" (structure)
assumes bipartite_V: "❙V ⊆ A Γ ∪ B Γ"
and A_vertex: "A Γ ⊆ ❙V"
and bipartite_E: "edge Γ x y ⟹ x ∈ A Γ ∧ y ∈ B Γ"
and disjoint: "A Γ ∩ B Γ = {}"
and weight_outside: "⋀x. x ∉ ❙V ⟹ weight Γ x = 0"
and weight_finite [simp]: "⋀x. weight Γ x ≠ ⊤"
and countable_E [simp]: "countable ❙E"
begin
lemma not_vertex: "⟦ x ∉ A Γ; x ∉ B Γ ⟧ ⟹ ¬ vertex Γ x"
using bipartite_V by blast
lemma no_loop: "¬ edge Γ x x"
using disjoint by(auto dest: bipartite_E)
lemma edge_antiparallel: "edge Γ x y ⟹ ¬ edge Γ y x"
using disjoint by(auto dest: bipartite_E)
lemma A_in: "x ∈ A Γ ⟹ ¬ edge Γ y x"
using disjoint by(auto dest: bipartite_E)
lemma B_out: "x ∈ B Γ ⟹ ¬ edge Γ x y"
using disjoint by(auto dest: bipartite_E)
sublocale countable_web using disjoint
by(unfold_locales)(auto simp add: A_in B_out A_vertex no_loop weight_outside)
lemma currentD_OUT':
assumes f: "current Γ f"
and x: "x ∉ A Γ"
shows "d_OUT f x = 0"
using currentD_outside_OUT[OF f, of x] x currentD_OUT[OF f, of x] bipartite_V by auto
lemma currentD_IN':
assumes f: "current Γ f"
and x: "x ∉ B Γ"
shows "d_IN f x = 0"
using currentD_outside_IN[OF f, of x] x currentD_IN[OF f, of x] bipartite_V by auto
lemma current_bipartiteI [intro?]:
assumes OUT: "⋀x. d_OUT f x ≤ weight Γ x"
and IN: "⋀x. d_IN f x ≤ weight Γ x"
and outside: "⋀e. e ∉ ❙E ⟹ f e = 0"
shows "current Γ f"
proof
fix x
assume "x ∉ A Γ" "x ∉ B Γ"
hence "d_OUT f x = 0" by(auto simp add: d_OUT_def nn_integral_0_iff emeasure_count_space_eq_0 intro!: outside dest: bipartite_E)
then show "d_OUT f x ≤ d_IN f x" by simp
qed(rule OUT IN outside)+
lemma wave_bipartiteI [intro?]:
assumes sep: "separating Γ (TER f)"
and f: "current Γ f"
shows "wave Γ f"
using sep
proof(rule wave.intros)
fix x
assume "x ∉ RF (TER f)"
then consider "x ∉ ❙V" | "x ∈ ❙V" "x ∈ B Γ" using separating_RF_A[OF sep] bipartite_V by auto
then show "d_OUT f x = 0" using currentD_OUT[OF f, of x] currentD_outside_OUT[OF f, of x]
by cases auto
qed
lemma web_flow_iff: "web_flow Γ f ⟷ current Γ f"
using bipartite_V by(auto simp add: web_flow.simps)
end
end