Commit ae96332b authored by gerwin.klein@nicta.com.au's avatar gerwin.klein@nicta.com.au
Browse files

new entry MFMC_Countable by Andreas Lochbihler

parent 402c9a28eaeb
[MFMC_Countable]
title = A formal proof of the max-flow min-cut theorem for countable networks
author = Andreas Lochbihler <http://www.infsec.ethz.ch/people/andreloc>
date = 2016-05-09
topic = Mathematics/Graph Theory
abstract =
This article formalises a proof of the maximum-flow minimal-cut
theorem for networks with countably many edges. A network is a
directed graph with non-negative real-valued edge labels and two
dedicated vertices, the source and the sink. A flow in a network
assigns non-negative real numbers to the edges such that for all
vertices except for the source and the sink, the sum of values on
incoming edges equals the sum of values on outgoing edges. A cut is a
subset of the vertices which contains the source, but not the sink.
Our theorem states that in every network, there is a flow and a cut
such that the flow saturates all the edges going out of the cut and is
zero on all the incoming edges. The proof is based on the paper
<emph>The Max-Flow Min-Cut theorem for countable networks</emph> by
Aharoni et al. As an application, we derive a characterisation of the
lifting operation for relations on discrete probability distributions,
which leads to a concise proof of its distributivity over relation
composition.
[Liouville_Numbers]
title = Liouville numbers
author = Manuel Eberl <http://in.tum.de/~eberlm>
......
(* Author: Andreas Lochbihler, ETH Zurich *)
section \<open>Preliminaries\<close>
theory MFMC_Misc imports
"~~/src/HOL/Probability/Probability"
"~~/src/HOL/Library/Transitive_Closure_Table"
"../Coinductive/Complete_Partial_Order2"
"~~/src/HOL/Library/Bourbaki_Witt_Fixpoint"
begin
hide_const (open) cycle
hide_const (open) path
hide_const (open) cut
hide_const (open) orthogonal
lemmas disjE [consumes 1, case_names left right, cases pred] = disjE
lemma inj_on_Pair2 [simp]: "inj_on (Pair x) A"
by(simp add: inj_on_def)
lemma inj_on_Pair1 [simp]: "inj_on (\<lambda>x. (x, y)) A"
by(simp add: inj_on_def)
lemma inj_map_prod': "\<lbrakk> inj f; inj g \<rbrakk> \<Longrightarrow> inj_on (map_prod f g) X"
by(rule subset_inj_on[OF prod.inj_map subset_UNIV])
lemma not_range_Inr: "x \<notin> range Inr \<longleftrightarrow> x \<in> range Inl"
by(cases x) auto
lemma not_range_Inl: "x \<notin> range Inl \<longleftrightarrow> x \<in> range Inr"
by(cases x) auto
lemma Chains_into_chain: "M \<in> Chains {(x, y). R x y} \<Longrightarrow> Complete_Partial_Order.chain R M"
by(simp add: Chains_def chain_def)
lemma chain_dual: "Complete_Partial_Order.chain op \<ge> = Complete_Partial_Order.chain op \<le>"
by(auto simp add: fun_eq_iff chain_def)
lemma ereal_diff_le_mono_left: "\<lbrakk> x \<le> z; 0 \<le> y \<rbrakk> \<Longrightarrow> x - y \<le> (z :: ereal)"
by(cases x y z rule: ereal3_cases) simp_all
lemma neg_0_less_iff_less_erea [simp]: "0 < - a \<longleftrightarrow> (a :: ereal) < 0"
by(cases a) simp_all
lemma not_infty_ereal: "\<bar>x\<bar> \<noteq> \<infinity> \<longleftrightarrow> (\<exists>x'. x = ereal x')"
by(cases x) simp_all
lemma neq_PInf_trans: fixes x y :: ereal shows "\<lbrakk> y \<noteq> \<infinity>; x \<le> y \<rbrakk> \<Longrightarrow> x \<noteq> \<infinity>"
by auto
lemma mult_2_ereal: "ereal 2 * x = x + x"
by(cases x) simp_all
lemma ereal_diff_le_self: "0 \<le> y \<Longrightarrow> x - y \<le> (x :: ereal)"
by(cases x y rule: ereal2_cases) simp_all
lemma ereal_le_add_self: "0 \<le> y \<Longrightarrow> x \<le> x + (y :: ereal)"
by(cases x y rule: ereal2_cases) simp_all
lemma ereal_le_add_self2: "0 \<le> y \<Longrightarrow> x \<le> y + (x :: ereal)"
by(cases x y rule: ereal2_cases) simp_all
lemma ereal_le_add_mono1: "\<lbrakk> x \<le> y; 0 \<le> (z :: ereal) \<rbrakk> \<Longrightarrow> x \<le> y + z"
using add_mono by fastforce
lemma ereal_le_add_mono2: "\<lbrakk> x \<le> z; 0 \<le> (y :: ereal) \<rbrakk> \<Longrightarrow> x \<le> y + z"
using add_mono by fastforce
lemma ereal_diff_nonpos:
fixes a b :: ereal shows "\<lbrakk> a \<le> b; a = \<infinity> \<Longrightarrow> b \<noteq> \<infinity>; a = -\<infinity> \<Longrightarrow> b \<noteq> -\<infinity> \<rbrakk> \<Longrightarrow> a - b \<le> 0"
by (cases rule: ereal2_cases[of a b]) auto
lemma minus_ereal_0 [simp]: "x - ereal 0 = x"
by(simp add: zero_ereal_def[symmetric])
lemma ereal_diff_eq_0_iff: fixes a b :: ereal
shows "(\<bar>a\<bar> = \<infinity> \<Longrightarrow> \<bar>b\<bar> \<noteq> \<infinity>) \<Longrightarrow> a - b = 0 \<longleftrightarrow> a = b"
by(cases a b rule: ereal2_cases) simp_all
lemma SUP_ereal_eq_0_iff_nonneg:
fixes f :: "_ \<Rightarrow> ereal" and A
assumes nonneg: "\<forall>x\<in>A. f x \<ge> 0"
and A:"A \<noteq> {}"
shows "(SUP x:A. f x) = 0 \<longleftrightarrow> (\<forall>x\<in>A. f x = 0)" (is "?lhs \<longleftrightarrow> ?rhs")
proof(intro iffI ballI)
fix x
assume "?lhs" "x \<in> A"
from \<open>x \<in> A\<close> have "f x \<le> (SUP x:A. f x)" by(rule SUP_upper)
with \<open>?lhs\<close> show "f x = 0" using nonneg \<open>x \<in> A\<close> by auto
qed(simp cong: SUP_cong add: A)
lemma ereal_divide_le_posI:
fixes x y z :: ereal
shows "x > 0 \<Longrightarrow> z \<noteq> - \<infinity> \<Longrightarrow> z \<le> x * y \<Longrightarrow> z / x \<le> y"
by (cases rule: ereal3_cases[of x y z])(auto simp: field_simps split: split_if_asm)
lemma add_diff_eq_ereal: fixes x y z :: ereal
shows "x + (y - z) = x + y - z"
by(cases x y z rule: ereal3_cases) simp_all
lemma ereal_diff_gr0:
fixes a b :: ereal shows "a < b \<Longrightarrow> 0 < b - a"
by (cases rule: ereal2_cases[of a b]) auto
lemma ereal_minus_minus: fixes x y z :: ereal shows
"(\<bar>y\<bar> = \<infinity> \<Longrightarrow> \<bar>z\<bar> \<noteq> \<infinity>) \<Longrightarrow> x - (y - z) = x + z - y"
by(cases x y z rule: ereal3_cases) simp_all
lemma diff_add_eq_ereal: fixes a b c :: ereal shows "a - b + c = a + c - b"
by(cases a b c rule: ereal3_cases) simp_all
lemma diff_diff_commute_ereal: fixes x y z :: ereal shows "x - y - z = x - z - y"
by(cases x y z rule: ereal3_cases) simp_all
lemma ereal_diff_eq_MInfty_iff: fixes x y :: ereal shows "x - y = -\<infinity> \<longleftrightarrow> x = -\<infinity> \<and> y \<noteq> -\<infinity> \<or> y = \<infinity> \<and> \<bar>x\<bar> \<noteq> \<infinity>"
by(cases x y rule: ereal2_cases) simp_all
lemma ereal_diff_add_inverse: fixes x y :: ereal shows "\<bar>x\<bar> \<noteq> \<infinity> \<Longrightarrow> x + y - x = y"
by(cases x y rule: ereal2_cases) simp_all
lemma Cauchy_real_Suc_diff:
fixes X :: "nat \<Rightarrow> real" and x :: real
assumes bounded: "\<And>n. \<bar>f (Suc n) - f n\<bar> \<le> (c / x ^ n)"
and x: "1 < x"
shows "Cauchy f"
proof(cases "c > 0")
case c: True
show ?thesis
proof(rule metric_CauchyI)
fix \<epsilon> :: real
assume "0 < \<epsilon>"
from bounded[of 0] x have c_nonneg: "0 \<le> c" by simp
from x have "0 < ln x" by simp
from reals_Archimedean3[OF this] obtain M :: nat
where "ln (c * x) - ln (\<epsilon> * (x - 1)) < real M * ln x" by blast
hence "exp (ln (c * x) - ln (\<epsilon> * (x - 1))) < exp (real M * ln x)" by(rule exp_less_mono)
hence M: "c * (1 / x) ^ M / (1 - 1 / x) < \<epsilon>" using \<open>0 < \<epsilon>\<close> x c
by(simp add: exp_diff exp_real_of_nat_mult field_simps)
{ fix n m :: nat
assume "n \<ge> M" "m \<ge> M"
then have "\<bar>f m - f n\<bar> \<le> c * ((1 / x) ^ M - (1 / x) ^ max m n) / (1 - 1 / x)"
proof(induction n m rule: linorder_wlog)
case sym thus ?case by(simp add: abs_minus_commute max.commute min.commute)
next
case (le m n)
then show ?case
proof(induction k\<equiv>"n - m" arbitrary: n m)
case 0 thus ?case using x c_nonneg by(simp add: field_simps mult_left_mono)
next
case (Suc k m n)
from \<open>Suc k = _\<close> obtain m' where m: "m = Suc m'" by(cases m) simp_all
with \<open>Suc k = _\<close> Suc.prems have "k = m' - n" "n \<le> m'" "M \<le> n" "M \<le> m'" by simp_all
hence "\<bar>f m' - f n\<bar> \<le> c * ((1 / x) ^ M - (1 / x) ^ (max m' n)) / (1 - 1 / x)" by(rule Suc)
also have "\<dots> = c * ((1 / x) ^ M - (1 / x) ^ m') / (1 - 1 / x)" using \<open>n \<le> m'\<close> by(simp add: max_def)
moreover
from bounded have "\<bar>f m - f m'\<bar> \<le> (c / x ^ m')" by(simp add: m)
ultimately have "\<bar>f m' - f n\<bar> + \<bar>f m - f m'\<bar> \<le> c * ((1 / x) ^ M - (1 / x) ^ m') / (1 - 1 / x) + \<dots>" by simp
also have "\<dots> \<le> c * ((1 / x) ^ M - (1 / x) ^ m) / (1 - 1 / x)" using m x by(simp add: field_simps)
also have "\<bar>f m - f n\<bar> \<le> \<bar>f m' - f n\<bar> + \<bar>f m - f m'\<bar>"
using abs_triangle_ineq4[of "f m' - f n" "f m - f m'"] by simp
ultimately show ?case using \<open>n \<le> m\<close> by(simp add: max_def)
qed
qed
also have "\<dots> < c * (1 / x) ^ M / (1 - 1 / x)" using x c by(auto simp add: field_simps)
also have "\<dots> < \<epsilon>" using M .
finally have "\<bar>f m - f n\<bar> < \<epsilon>" . }
thus "\<exists>M. \<forall>m\<ge>M. \<forall>n\<ge>M. dist (f m) (f n) < \<epsilon>" unfolding dist_real_def by blast
qed
next
case False
with bounded[of 0] have [simp]: "c = 0" by simp
have eq: "f m = f 0" for m
proof(induction m)
case (Suc m) from bounded[of m] Suc.IH show ?case by simp
qed simp
show ?thesis by(rule metric_CauchyI)(subst (1 2) eq; simp)
qed
lemma complete_lattice_ccpo_dual:
"class.ccpo Inf op \<ge> (op > :: _ :: complete_lattice \<Rightarrow> _)"
by(unfold_locales)(auto intro: Inf_lower Inf_greatest)
lemma card_eq_1_iff: "card A = Suc 0 \<longleftrightarrow> (\<exists>x. A = {x})"
using card_eq_SucD by auto
lemma nth_rotate1: "n < length xs \<Longrightarrow> rotate1 xs ! n = xs ! (Suc n mod length xs)"
apply(cases xs; clarsimp simp add: nth_append not_less)
apply(subgoal_tac "n = length list"; simp)
done
lemma set_zip_rightI: "\<lbrakk> x \<in> set ys; length xs \<ge> length ys \<rbrakk> \<Longrightarrow> \<exists>z. (z, x) \<in> set (zip xs ys)"
by(fastforce simp add: in_set_zip in_set_conv_nth simp del: length_greater_0_conv intro!: nth_zip conjI[rotated])
lemma map_eq_append_conv:
"map f xs = ys @ zs \<longleftrightarrow> (\<exists>ys' zs'. xs = ys' @ zs' \<and> ys = map f ys' \<and> zs = map f zs')"
by(auto 4 4 intro: exI[where x="take (length ys) xs"] exI[where x="drop (length ys) xs"] simp add: append_eq_conv_conj take_map drop_map dest: sym)
lemma rotate1_append:
"rotate1 (xs @ ys) = (if xs = [] then rotate1 ys else tl xs @ ys @ [hd xs])"
by(clarsimp simp add: neq_Nil_conv)
lemma in_set_tlD: "x \<in> set (tl xs) \<Longrightarrow> x \<in> set xs"
by(cases xs) simp_all
lemma tendsto_diff_ereal:
fixes x y :: ereal
assumes x: "\<bar>x\<bar> \<noteq> \<infinity>" and y: "\<bar>y\<bar> \<noteq> \<infinity>"
assumes f: "(f \<longlongrightarrow> x) F" and g: "(g \<longlongrightarrow> y) F"
shows "((\<lambda>x. f x - g x) \<longlongrightarrow> x - y) F"
proof -
from x obtain r where x': "x = ereal r" by (cases x) auto
with f have "((\<lambda>i. real_of_ereal (f i)) \<longlongrightarrow> r) F" by simp
moreover
from y obtain p where y': "y = ereal p" by (cases y) auto
with g have "((\<lambda>i. real_of_ereal (g i)) \<longlongrightarrow> p) F" by simp
ultimately have "((\<lambda>i. real_of_ereal (f i) - real_of_ereal (g i)) \<longlongrightarrow> r - p) F"
by (rule tendsto_diff)
moreover
from eventually_finite[OF x f] eventually_finite[OF y g]
have "eventually (\<lambda>x. f x - g x = ereal (real_of_ereal (f x) - real_of_ereal (g x))) F"
by eventually_elim auto
ultimately show ?thesis
by (simp add: x' y' cong: filterlim_cong)
qed
lemma countable_converseI:
assumes "countable A"
shows "countable (converse A)"
proof -
have "converse A = prod.swap ` A" by auto
then show ?thesis using assms by simp
qed
lemma countable_converse [simp]: "countable (converse A) \<longleftrightarrow> countable A"
using countable_converseI[of A] countable_converseI[of "converse A"] by auto
lemma nn_integral_count_space_reindex:
"inj_on f A \<Longrightarrow>(\<integral>\<^sup>+ y. g y \<partial>count_space (f ` A)) = (\<integral>\<^sup>+ x. g (f x) \<partial>count_space A)"
by(simp add: embed_measure_count_space'[symmetric] nn_integral_embed_measure' measurable_embed_measure1)
syntax
"_nn_sum" :: "pttrn \<Rightarrow> 'a set \<Rightarrow> 'b \<Rightarrow> 'b::comm_monoid_add" ("(2\<Sum>\<^sup>+ _\<in>_./ _)" [0, 51, 10] 10)
"_nn_sum_UNIV" :: "pttrn \<Rightarrow> 'b \<Rightarrow> 'b::comm_monoid_add" ("(2\<Sum>\<^sup>+ _./ _)" [0, 10] 10)
translations
"\<Sum>\<^sup>+ i\<in>A. b" \<rightleftharpoons> "CONST nn_integral (CONST count_space A) (\<lambda>i. b)"
"\<Sum>\<^sup>+ i. b" \<rightleftharpoons> "\<Sum>\<^sup>+ i\<in>CONST UNIV. b"
inductive_simps rtrancl_path_simps:
"rtrancl_path R x [] y"
"rtrancl_path R x (a # bs) y"
definition restrict_rel :: "'a set \<Rightarrow> ('a \<times> 'a) set \<Rightarrow> ('a \<times> 'a) set"
where "restrict_rel A R = {(x, y)\<in>R. x \<in> A \<and> y \<in> A}"
lemma in_restrict_rel_iff: "(x, y) \<in> restrict_rel A R \<longleftrightarrow> (x, y) \<in> R \<and> x \<in> A \<and> y \<in> A"
by(simp add: restrict_rel_def)
lemma restrict_relE: "\<lbrakk> (x, y) \<in> restrict_rel A R; \<lbrakk> (x, y) \<in> R; x \<in> A; y \<in> A \<rbrakk> \<Longrightarrow> thesis \<rbrakk> \<Longrightarrow> thesis"
by(simp add: restrict_rel_def)
lemma restrict_relI [intro!]: "\<lbrakk> (x, y) \<in> R; x \<in> A; y \<in> A \<rbrakk> \<Longrightarrow> (x, y) \<in> restrict_rel A R"
by(simp add: restrict_rel_def)
lemma Field_restrict_rel_subset: "Field (restrict_rel A R) \<subseteq> A \<inter> Field R"
by(auto simp add: Field_def in_restrict_rel_iff)
lemma Field_restrict_rel [simp]: "Refl R \<Longrightarrow> Field (restrict_rel A R) = A \<inter> Field R"
using Field_restrict_rel_subset[of A R]
by auto (auto simp add: Field_def dest: refl_onD)
lemma Partial_order_restrict_rel:
assumes "Partial_order R"
shows "Partial_order (restrict_rel A R)"
proof -
from assms have "Refl R" by(simp add: order_on_defs)
from Field_restrict_rel[OF this, of A] assms show ?thesis
by(simp add: order_on_defs trans_def antisym_def)
(auto intro: FieldI1 FieldI2 intro!: refl_onI simp add: in_restrict_rel_iff elim: refl_onD)
qed
lemma Chains_restrict_relD: "M \<in> Chains (restrict_rel A leq) \<Longrightarrow> M \<in> Chains leq"
by(auto simp add: Chains_def in_restrict_rel_iff)
lemma bourbaki_witt_fixpoint_restrict_rel:
assumes leq: "Partial_order leq"
and chain_Field: "\<And>M. \<lbrakk> M \<in> Chains (restrict_rel A leq); M \<noteq> {} \<rbrakk> \<Longrightarrow> lub M \<in> A"
and lub_least: "\<And>M z. \<lbrakk> M \<in> Chains leq; M \<noteq> {}; \<And>x. x \<in> M \<Longrightarrow> (x, z) \<in> leq \<rbrakk> \<Longrightarrow> (lub M, z) \<in> leq"
and lub_upper: "\<And>M z. \<lbrakk> M \<in> Chains leq; z \<in> M \<rbrakk> \<Longrightarrow> (z, lub M) \<in> leq"
and increasing: "\<And>x. \<lbrakk> x \<in> A; x \<in> Field leq \<rbrakk> \<Longrightarrow> (x, f x) \<in> leq \<and> f x \<in> A"
shows "bourbaki_witt_fixpoint lub (restrict_rel A leq) f"
proof
show "Partial_order (restrict_rel A leq)" using leq by(rule Partial_order_restrict_rel)
next
from leq have Refl: "Refl leq" by(simp add: order_on_defs)
{ fix M z
assume M: "M \<in> Chains (restrict_rel A leq)"
presume z: "z \<in> M"
hence "M \<noteq> {}" by auto
with M have lubA: "lub M \<in> A" by(rule chain_Field)
from M have M': "M \<in> Chains leq" by(rule Chains_restrict_relD)
then have *: "(z, lub M) \<in> leq" using z by(rule lub_upper)
hence "lub M \<in> Field leq" by(rule FieldI2)
with lubA show "lub M \<in> Field (restrict_rel A leq)" by(simp add: Field_restrict_rel[OF Refl])
from Chains_FieldD[OF M z] have "z \<in> A" by(simp add: Field_restrict_rel[OF Refl])
with * lubA show "(z, lub M ) \<in> restrict_rel A leq" by auto
fix z
assume upper: "\<And>x. x \<in> M \<Longrightarrow> (x, z) \<in> restrict_rel A leq"
from upper[OF z] have "z \<in> Field (restrict_rel A leq)" by(auto simp add: Field_def)
with Field_restrict_rel_subset[of A leq] have "z \<in> A" by blast
moreover from lub_least[OF M' \<open>M \<noteq> {}\<close>] upper have "(lub M, z) \<in> leq"
by(auto simp add: in_restrict_rel_iff)
ultimately show "(lub M, z) \<in> restrict_rel A leq" using lubA by(simp add: in_restrict_rel_iff) }
{ fix x
assume "x \<in> Field (restrict_rel A leq)"
hence "x \<in> A" "x \<in> Field leq" by(simp_all add: Field_restrict_rel[OF Refl])
with increasing[OF this] show "(x, f x) \<in> restrict_rel A leq" by auto }
show "(SOME x. x \<in> M) \<in> M" "(SOME x. x \<in> M) \<in> M" if "M \<noteq> {}" for M :: "'a set"
using that by(auto intro: someI)
qed
lemma Field_le [simp]: "Field {(x :: _ :: preorder, y). x \<le> y} = UNIV"
by(auto intro: FieldI1)
lemma Field_ge [simp]: "Field {(x :: _ :: preorder, y). y \<le> x} = UNIV"
by(auto intro: FieldI1)
lemma refl_le [simp]: "refl {(x :: _ :: preorder, y). x \<le> y}"
by(auto intro!: refl_onI simp add: Field_def)
lemma refl_ge [simp]: "refl {(x :: _ :: preorder, y). y \<le> x}"
by(auto intro!: refl_onI simp add: Field_def)
lemma partial_order_le [simp]: "partial_order_on UNIV {(x :: _ :: order, x'). x \<le> x'}"
by(auto simp add: order_on_defs trans_def antisym_def)
lemma partial_order_ge [simp]: "partial_order_on UNIV {(x :: _ :: order, x'). x' \<le> x}"
by(auto simp add: order_on_defs trans_def antisym_def)
lemma incseq_chain_range: "incseq f \<Longrightarrow> Complete_Partial_Order.chain op \<le> (range f)"
apply(rule chainI; clarsimp)
subgoal for x y using linear[of x y] by(auto dest: incseqD)
done
end
\ No newline at end of file
This source diff could not be displayed because it is too large. You can view the blob instead.
chapter AFP
session "MFMC_Countable" (AFP) = "HOL-Probability" +
options [timeout = 600]
theories [document = false]
"~~/src/HOL/Library/Transitive_Closure_Table"
"~~/src/HOL/Library/Bourbaki_Witt_Fixpoint"
"../Coinductive/Complete_Partial_Order2"
theories
Rel_PMF_Characterisation
document_files
"root.tex"
"root.bib"
(* Author: Andreas Lochbihler, ETH Zurich *)
theory Rel_PMF_Characterisation imports
Max_Flow_Min_Cut_Countable
begin
section \<open>Characterisation of @{const rel_pmf}\<close>
context begin
private datatype ('a, 'b) vertex = Source | Sink | Left 'a | Right 'b
private lemma inj_Left [simp]: "inj_on Left X"
by(simp add: inj_on_def)
private lemma inj_Right [simp]: "inj_on Right X"
by(simp add: inj_on_def)
proposition rel_pmf_measureI:
fixes p :: "'a pmf" and q :: "'b pmf"
assumes le: "\<And>A. measure (measure_pmf p) A \<le> measure (measure_pmf q) {y. \<exists>x\<in>A. R x y}"
shows "rel_pmf R p q"
proof -
have DomR: "\<exists>y\<in>set_pmf q. R x y" if "x \<in> set_pmf p" for x
proof(rule ccontr)
assume *: "\<not> ?thesis"
from le[of "{x}"] have "pmf p x \<le> measure (measure_pmf q) {y. R x y}"
by(auto simp add: pmf.rep_eq)
also have "\<dots> = 0" using * by(auto simp add: measure_pmf_zero_iff)
finally show False using that by(auto dest: pmf_positive)
qed
have RanR: "\<exists>x\<in>set_pmf p. R x y" if "y \<in> set_pmf q" for y
proof(rule ccontr)
assume *: "\<not> ?thesis"
then have "measure (measure_pmf q) {y. \<exists>x\<in>set_pmf p. R x y} + measure (measure_pmf q) {y} = measure (measure_pmf q) ({y. \<exists>x\<in>set_pmf p. R x y} \<union> {y})"
by(intro measure_pmf.finite_measure_Union[symmetric]) auto
also have "\<dots> \<le> 1" by simp
also have "measure (measure_pmf p) (set_pmf p) = 1" by(simp add: measure_pmf.prob_eq_1 AE_measure_pmf)
then have "1 \<le> measure (measure_pmf q) {y. \<exists>x\<in>set_pmf p. R x y}" using le[of "set_pmf p"] by auto
ultimately have "measure (measure_pmf q) {y} \<le> 0" by auto
with that show False by(auto dest: pmf_positive simp add: pmf.rep_eq)
qed
def edge' \<equiv> "\<lambda>xv yv. case (xv, yv) of
(Source, Left x) \<Rightarrow> x \<in> set_pmf p
| (Left x, Right y) \<Rightarrow> R x y \<and> x \<in> set_pmf p \<and> y \<in> set_pmf q
| (Right y, Sink) \<Rightarrow> y \<in> set_pmf q
| _ \<Rightarrow> False"
have edge'_simps [simp]:
"edge' xv (Left x) \<longleftrightarrow> xv = Source \<and> x \<in> set_pmf p"
"edge' (Left x) (Right y) \<longleftrightarrow> R x y \<and> x \<in> set_pmf p \<and> y \<in> set_pmf q"
"edge' (Right y) yv \<longleftrightarrow> yv = Sink \<and> y \<in> set_pmf q"
"edge' Source (Right y) \<longleftrightarrow> False"
"edge' Source Sink \<longleftrightarrow> False"
"edge' xv Source \<longleftrightarrow> False"
"edge' Sink yv \<longleftrightarrow> False"
"edge' (Left x) Sink \<longleftrightarrow> False"
for xv yv x y by(simp_all add: edge'_def split: vertex.split)
have edge'_cases[cases pred]: thesis if "edge' xv yv"
"\<And>x. \<lbrakk> xv = Source; yv = Left x; x \<in> set_pmf p \<rbrakk> \<Longrightarrow> thesis"
"\<And>x y. \<lbrakk> xv = Left x; yv = Right y; R x y; x \<in> set_pmf p; y \<in> set_pmf q \<rbrakk> \<Longrightarrow> thesis"
"\<And>y. \<lbrakk> xv = Right y; yv = Sink; y \<in> set_pmf q \<rbrakk> \<Longrightarrow> thesis"
for thesis xv yv using that by(simp add: edge'_def split: prod.split_asm vertex.split_asm)
have edge'_SourceE [elim!]: thesis if "edge' Source yv" "\<And>x. \<lbrakk> yv = Left x; x \<in> set_pmf p \<rbrakk> \<Longrightarrow> thesis"
for yv thesis using that by(auto elim: edge'_cases)
have edge'_LeftE [elim!]: thesis if "edge' (Left x) yv" "\<And>y. \<lbrakk> yv = Right y; R x y; x \<in> set_pmf p; y \<in> set_pmf q \<rbrakk> \<Longrightarrow> thesis"
for x yv thesis using that by(auto elim: edge'_cases)
have edge'_RightE [elim!]: thesis if "edge' xv (Right y)" "\<And>x. \<lbrakk> xv = Left x; R x y; x \<in> set_pmf p; y \<in> set_pmf q \<rbrakk> \<Longrightarrow> thesis"
for xv y thesis using that by(auto elim: edge'_cases)
have edge'_SinkE [elim!]: thesis if "edge' xv Sink" "\<And>y. \<lbrakk> xv = Right y; y \<in> set_pmf q \<rbrakk> \<Longrightarrow> thesis"
for xv thesis using that by(auto elim: edge'_cases)
have edge'1: "x \<in> set_pmf p \<Longrightarrow> edge' Source (Left x)"
and edge'2: "\<lbrakk> R x y; x \<in> set_pmf p; y \<in> set_pmf q \<rbrakk> \<Longrightarrow> edge' (Left x) (Right y)"
and edge'3: "y \<in> set_pmf q \<Longrightarrow> edge' (Right y) Sink"
for x y by simp_all
note edge'I[intro] = this
def cap \<equiv> "(\<lambda>(xv, yv). case (xv, yv) of
(Source, Left x) \<Rightarrow> pmf p x
| (Left x, Right y) \<Rightarrow> if R x y \<and> x \<in> set_pmf p \<and> y \<in> set_pmf q then 2 else 0
| (Right y, Sink) \<Rightarrow> pmf q y
| _ \<Rightarrow> 0) :: ('a, 'b) vertex flow"
have cap_simps [simp]:
"cap (xv, Left x) = (if xv = Source then ereal (pmf p x) else 0)"
"cap (Left x, Right y) = (if R x y \<and> x \<in> set_pmf p \<and> y \<in> set_pmf q then 2 else 0)"
"cap (Right y, yv) = (if yv = Sink then ereal (pmf q y) else 0)"
"cap (Source, Right y) = 0"
"cap (Source, Sink) = 0"
"cap (xv, Source) = 0"
"cap (Sink, yv) = 0"
"cap (Left x, Sink) = 0"
for xv yv x y by(simp_all add: cap_def split: vertex.split)
def \<Delta> \<equiv> "\<lparr>edge = edge', capacity = cap, source = Source, sink = Sink\<rparr>"
write \<Delta> (structure)
have \<Delta>_sel [simp]:
"edge \<Delta> = edge'"
"capacity \<Delta> = cap"
"source \<Delta> = Source"
"sink \<Delta> = Sink"
by(simp_all add: \<Delta>_def)
have IN_Left [simp]: "\<^bold>I\<^bold>N (Left x) = (if x \<in> set_pmf p then {Source} else {})" for x
by(auto simp add: incoming_def)
have OUT_Right [simp]: "\<^bold>O\<^bold>U\<^bold>T (Right y) = (if y \<in> set_pmf q then {Sink} else {})" for y
by(auto simp add: outgoing_def)
interpret network: countable_network \<Delta>
proof
show "source \<Delta> \<noteq> sink \<Delta>" by simp
show "capacity \<Delta> e = 0" if "e \<notin> \<^bold>E" for e using that
by(cases e)(auto simp add: edge'_def pmf_eq_0_set_pmf split: vertex.split_asm)
show "0 \<le> capacity \<Delta> e" for e by(auto simp add: cap_def pmf_nonneg split: prod.split vertex.split)
show "capacity \<Delta> e \<noteq> \<infinity>" for e by(auto simp add: cap_def split: prod.split vertex.split)
have "\<^bold>E \<subseteq> ((Pair Source \<circ> Left) ` set_pmf p) \<union> (map_prod Left Right ` (set_pmf p \<times> set_pmf q)) \<union> ((\<lambda>y. (Right y, Sink)) ` set_pmf q)"
by(auto elim: edge'_cases)
thus "countable \<^bold>E" by(rule countable_subset) auto
qed
from network.max_flow_min_cut obtain f S
where f: "flow \<Delta> f" and cut: "cut \<Delta> S" and ortho: "orthogonal \<Delta> f S" by blast
from cut obtain Source: "Source \<in> S" and Sink: "Sink \<notin> S" by cases simp
have f_finite [simp]: "f e \<noteq> \<infinity>" "\<bar>f e\<bar> \<noteq> \<infinity>" "f e \<noteq> - \<infinity>" for e
using network.flowD_finite[OF f, of e] flowD_nonneg[OF f, of e] by simp_all
have OUT_cap_Source: "d_OUT cap Source = 1"
proof -
have "d_OUT cap Source = (\<Sum>\<^sup>+ y\<in>range Left. cap (Source, y))"
by(auto 4 4 simp add: d_OUT_def nn_integral_count_space_indicator intro!: nn_integral_cong network.capacity_outside[simplified] split: split_indicator)
also have "\<dots> = (\<Sum>\<^sup>+ y. pmf p y)" by(simp add: nn_integral_count_space_reindex)
also have "\<dots> = 1" by(simp add: nn_integral_pmf)
finally show ?thesis .
qed
have IN_cap_Left: "d_IN cap (Left x) = pmf p x" for x
by(subst d_IN_alt_def[of _ \<Delta>])(simp_all add: pmf_eq_0_set_pmf pmf_nonneg nn_integral_count_space_indicator max_def)
have OUT_cap_Right: "d_OUT cap (Right y) = pmf q y" for y
by(subst d_OUT_alt_def[of _ \<Delta>])(simp_all add: pmf_eq_0_set_pmf pmf_nonneg nn_integral_count_space_indicator max_def)
have IN_f_Left: "d_IN f (Left x) = f (Source, Left x)" for x
by(subst d_IN_alt_def[of _ \<Delta>])(simp_all add: nn_integral_count_space_indicator max_def network.flowD_outside[OF f] flowD_nonneg[OF f])
have OUT_f_Right: "d_OUT f (Right y) = f (Right y, Sink)" for y
by(subst d_OUT_alt_def[of _ \<Delta>])(simp_all add: nn_integral_count_space_indicator max_def network.flowD_outside[OF f] flowD_nonneg[OF f])
have S_LR: "Right y \<in> S" if Left: "Left x \<in> S" and edge: "R x y" "x \<in> set_pmf p" "y \<in> set_pmf q" for x y
proof(rule ccontr)
assume Right: "Right y \<notin> S"
from edge have "edge \<Delta> (Left x) (Right y)" by simp
from orthogonalD_out[OF ortho this Left Right] edge have "2 = f (Left x, Right y)" by simp
also have "\<dots> \<le> d_OUT f (Left x)" unfolding d_OUT_def by(rule nn_integral_ge_point) simp
also have "\<dots> = d_IN f (Left x)" using f by(rule flowD_KIR) simp_all
also have "\<dots> \<le> d_IN cap (Left x)" using flowD_capacity_IN[OF f, of "Left x"] by simp
also have "\<dots> = pmf p x" by(rule IN_cap_Left)
also have "\<dots> \<le> 1" by(simp add: pmf_le_1)
finally show False by simp
qed
have "value_flow \<Delta> f \<le> 1" using flowD_capacity_OUT[OF f, of Source] by(simp add: OUT_cap_Source)
moreover have "1 \<le> value_flow \<Delta> f"
proof -
let ?L = "Left -` S \<inter> set_pmf p"
let ?R = "{y|y x. x \<in> set_pmf p \<and> Left x \<in> S \<and> R x y \<and> y \<in> set_pmf q}"
have "value_flow \<Delta> f = (\<Sum>\<^sup>+ x\<in>range Left. f (Source, x))" unfolding d_OUT_def
by(auto simp add: nn_integral_count_space_indicator intro!: nn_integral_cong network.flowD_outside[OF f] split: split_indicator)
also have "\<dots> = (\<Sum>\<^sup>+ x. f (Source, Left x) * indicator ?L x) + (\<Sum>\<^sup>+ x. f (Source, Left x) * indicator (- ?L) x)"
by(subst nn_integral_add[symmetric])(auto simp add: flowD_nonneg[OF f] nn_integral_count_space_reindex intro!: nn_integral_cong split: split_indicator)
also have "(\<Sum>\<^sup>+ x. f (Source, Left x) * indicator (- ?L) x) = (\<Sum>\<^sup>+ x\<in>- ?L. cap (Source, Left x))"
using orthogonalD_out[OF ortho _ Source]
apply(auto simp add: set_pmf_iff network.flowD_outside[OF f] flowD_nonneg[OF f] nn_integral_count_space_indicator intro!: nn_integral_cong split: split_indicator)
subgoal for x by(cases "x \<in> set_pmf p")(auto simp add: set_pmf_iff zero_ereal_def[symmetric] network.flowD_outside[OF f])
done
also have "\<dots> = (\<Sum>\<^sup>+ x\<in>- ?L. pmf p x)" by simp
also have "\<dots> = emeasure (measure_pmf p) (- ?L)" by(simp add: nn_integral_pmf)
also have "(\<Sum>\<^sup>+ x. f (Source, Left x) * indicator ?L x) = (\<Sum>\<^sup>+ x\<in>?L. d_IN f (Left x))"
by(subst d_IN_alt_def[of _ \<Delta>])(auto simp add: network.flowD_outside[OF f] nn_integral_count_space_indicator max_def flowD_nonneg[OF f] intro!: nn_integral_cong)
also have "\<dots> = (\<Sum>\<^sup>+ x\<in>?L. d_OUT f (Left x))"
by(rule nn_integral_cong flowD_KIR[OF f, symmetric])+ simp_all
also have "\<dots> = (\<Sum>\<^sup>+ x. \<Sum>\<^sup>+ y. f (Left x, y) * indicator (range Right) y * indicator ?L x)"
by(auto simp add: d_OUT_def nn_integral_count_space_indicator intro!: nn_integral_cong network.flowD_outside[OF f] split: split_indicator)
also have "\<dots> = (\<Sum>\<^sup>+ y\<in>range Right. \<Sum>\<^sup>+ x. f (Left x, y) * indicator ?L x)"
by(subst nn_integral_fst_count_space[where f="case_prod _", simplified])
(simp add: nn_integral_snd_count_space[where f="case_prod _", simplified] nn_integral_count_space_indicator nn_integral_cmult[symmetric] mult_ac)
also have "\<dots> = (\<Sum>\<^sup>+ y. \<Sum>\<^sup>+ x. f (Left x, Right y) * indicator ?L x)"
by(simp add: nn_integral_count_space_reindex)
also have "\<dots> = (\<Sum>\<^sup>+ y. \<Sum>\<^sup>+ x. f (Left x, Right y) * indicator ?L x * indicator {y|x. Right y \<in> S \<and> x \<in> set_pmf p \<and> Left x \<in> S \<and> R x y \<and> y \<in> set_pmf q} y)"
apply(rule nn_integral_cong)+
subgoal for y x
by(cases "R x y" "y \<in> set_pmf q" rule: bool.exhaust[case_product bool.exhaust])
(auto split: split_indicator dest: S_LR simp add: network.flowD_outside[OF f])
done
also have "\<dots> = (\<Sum>\<^sup>+ y. \<Sum>\<^sup>+ x. f (Left x, Right y) * indicator ?R y)"
apply(rule nn_integral_cong)+
subgoal for y x
by(cases "R x y" "x \<in> set_pmf p" rule: bool.exhaust[case_product bool.exhaust])
(auto split: split_indicator simp add: orthogonalD_in[OF ortho] network.flowD_outside[OF f] dest: S_LR)
done
also have "\<dots> = (\<Sum>\<^sup>+ y\<in>?R. \<Sum>\<^sup>+ x\<in>range Left. f (x, Right y))"
by(simp add: nn_integral_count_space_reindex)(auto simp add: nn_integral_count_space_indicator nn_integral_multc intro!: nn_integral_cong arg_cong2[where f="op *"] split: split_indicator)
also have "\<dots> = (\<Sum>\<^sup>+ y\<in>?R. d_IN f (Right y))"
by(auto simp add: d_IN_def nn_integral_count_space_indicator intro!: nn_integral_cong network.flowD_outside[OF f] split: split_indicator)
also have "\<dots> = (\<Sum>\<^sup>+ y\<in>?R. d_OUT f (Right y))" using flowD_KIR[OF f] by simp
also have "\<dots> = (\<Sum>\<^sup>+ y\<in>?R. d_OUT cap (Right y))"
by(auto 4 3 intro!: nn_integral_cong simp add: d_OUT_def network.flowD_outside[OF f] Sink dest: S_LR intro: orthogonalD_out[OF ortho, of "Right _" Sink, simplified])
also have "\<dots> = (\<Sum>\<^sup>+ y\<in>?R. pmf q y)" by(simp add: OUT_cap_Right)
also have "\<dots> = emeasure (measure_pmf q) ?R" by(simp add: nn_integral_pmf)
also have "\<dots> \<ge> emeasure (measure_pmf p) ?L" using le[of ?L]
by(auto elim!: order_trans simp add: measure_pmf.emeasure_eq_measure AE_measure_pmf_iff intro!: measure_pmf.finite_measure_mono_AE)
ultimately have "value_flow \<Delta> f \<ge> emeasure (measure_pmf p) ?L + emeasure (measure_pmf p) (- ?L)"
by(simp add: add_right_mono)
also have "emeasure (measure_pmf p) ?L + emeasure (measure_pmf p) (- ?L) = emeasure (measure_pmf p) (?L \<union> - ?L)"
by(subst plus_emeasure) auto
also have "?L \<union> -?L = UNIV" by blast
finally show ?thesis by simp
qed
ultimately have val: "value_flow \<Delta> f = 1" by simp
have SAT_p: "f (Source, Left x) = pmf p x" for x
proof(rule antisym)
show "f (Source, Left x) \<le> pmf p x" using flowD_capacity[OF f, of "(Source, Left x)"] by simp
show "pmf p x \<le> f (Source, Left x)"
proof(rule ccontr)
assume *: "\<not> ?thesis"
have finite: "(\<Sum>\<^sup>+ y. f (Source, Left y) * indicator (- {x}) y) \<noteq> \<infinity>"
proof -
have "(\<Sum>\<^sup>+ y. f (Source, Left y) * indicator (- {x}) y) \<le> (\<Sum>\<^sup>+ y\<in>range Left. f (Source, y))"
by(auto simp add: nn_integral_count_space_reindex flowD_nonneg[OF f] intro!: nn_integral_mono split: split_indicator)
also have "\<dots> = value_flow \<Delta> f"
by(auto simp add: d_OUT_def nn_integral_count_space_indicator intro!: nn_integral_cong network.flowD_outside[OF f] split: split_indicator)
finally show ?thesis using val by auto
qed