section ‹The Ford-Fulkerson Theorem› theory Ford_Fulkerson imports Augmenting_Flow Augmenting_Path begin text ‹In this theory, we prove the Ford-Fulkerson theorem, and its well-known corollary, the min-cut max-flow theorem. › text ‹We fix a network with a flow and a cut› locale NFlowCut = NFlow c s t f + NCut c s t k for c :: "'capacity::linordered_idom graph" and s t f k begin lemma finite_k[simp, intro!]: "finite k" using cut_ss_V finite_V finite_subset[of k V] by blast subsection ‹Net Flow› text ‹We define the \emph{net flow} to be the amount of flow effectively passed over the cut from the source to the sink:› definition netFlow :: "'capacity" where "netFlow ≡ (∑e ∈ outgoing' k. f e) - (∑e ∈ incoming' k. f e)" text ‹We can show that the net flow equals the value of the flow. Note: Cormen et al.~\cite{CLRS09} present a whole page full of summation calculations for this proof, and our formal proof also looks quite complicated. › lemma flow_value: "netFlow = val" proof - let ?LCL = "{(u, v). u ∈ k ∧ v ∈ k ∧ (u, v) ∈ E}" let ?AOG = "{(u, v). u ∈ k ∧ (u, v) ∈ E}" let ?AIN = "{(v, u) | u v. u ∈ k ∧ (v, u) ∈ E}" let ?SOG = "λu. (∑e ∈ outgoing u. f e)" let ?SIN = "λu. (∑e ∈ incoming u. f e)" let ?SOG' = "(∑e ∈ outgoing' k. f e)" let ?SIN' = "(∑e ∈ incoming' k. f e)" text ‹Some setup to make finiteness reasoning implicit› note [[simproc finite_Collect]] have "netFlow = ?SOG' + (∑e ∈ ?LCL. f e) - (?SIN' + (∑e ∈ ?LCL. f e))" (is "_ = ?SAOG - ?SAIN") using netFlow_def by auto also have "?SAOG = (∑y ∈ k - {s}. ?SOG y) + ?SOG s" proof - have "?SAOG = (∑e∈(outgoing' k ∪ ?LCL). f e)" by (rule setsum.union_disjoint[symmetric]) (auto simp: outgoing'_def) also have "outgoing' k ∪ ?LCL = (\<Union>y∈k-{s}. outgoing y) ∪ outgoing s" by (auto simp: outgoing_def outgoing'_def s_in_cut) also have "(∑e∈(UNION (k - {s}) outgoing ∪ outgoing s). f e) = (∑e∈(UNION (k - {s}) outgoing). f e) + (∑e∈outgoing s. f e)" by (rule setsum.union_disjoint) (auto simp: outgoing_def intro: finite_Image) also have "(∑e∈(UNION (k - {s}) outgoing). f e) = (∑y ∈ k - {s}. ?SOG y)" by (rule setsum.UNION_disjoint) (auto simp: outgoing_def intro: finite_Image) finally show ?thesis . qed also have "?SAIN = (∑y ∈ k - {s}. ?SIN y) + ?SIN s" proof - have "?SAIN = (∑e∈(incoming' k ∪ ?LCL). f e)" by (rule setsum.union_disjoint[symmetric]) (auto simp: incoming'_def) also have "incoming' k ∪ ?LCL = (\<Union>y∈k-{s}. incoming y) ∪ incoming s" by (auto simp: incoming_def incoming'_def s_in_cut) also have "(∑e∈(UNION (k - {s}) incoming ∪ incoming s). f e) = (∑e∈(UNION (k - {s}) incoming). f e) + (∑e∈incoming s. f e)" by (rule setsum.union_disjoint) (auto simp: incoming_def intro: finite_Image) also have "(∑e∈(UNION (k - {s}) incoming). f e) = (∑y ∈ k - {s}. ?SIN y)" by (rule setsum.UNION_disjoint) (auto simp: incoming_def intro: finite_Image) finally show ?thesis . qed finally have "netFlow = ((∑y ∈ k - {s}. ?SOG y) + ?SOG s) - ((∑y ∈ k - {s}. ?SIN y) + ?SIN s)" (is "netFlow = ?R") . also have "?R = ?SOG s - ?SIN s" proof - have "(!!u. u ∈ k - {s} ==> ?SOG u = ?SIN u)" using conservation_const cut_ss_V t_ni_cut by force thus ?thesis by auto qed finally show ?thesis unfolding val_def by simp qed text ‹The value of any flow is bounded by the capacity of any cut. This is intuitively clear, as all flow from the source to the sink has to go over the cut.› corollary weak_duality: "val ≤ cap" proof - have "(∑e ∈ outgoing' k. f e) ≤ (∑e ∈ outgoing' k. c e)" (is "?L ≤ ?R") using capacity_const by (metis setsum_mono) then have "(∑e ∈ outgoing' k. f e) ≤ cap" unfolding cap_def by simp moreover have "val ≤ (∑e ∈ outgoing' k. f e)" using netFlow_def by (simp add: capacity_const flow_value setsum_nonneg) ultimately show ?thesis by simp qed end -- ‹Cut› subsection ‹Ford-Fulkerson Theorem› context NFlow begin text ‹We prove three auxiliary lemmas first, and the state the theorem as a corollary› lemma fofu_I_II: "isMaxFlow f ==> ¬ (∃ p. isAugmentingPath p)" unfolding isMaxFlow_alt proof (rule ccontr) assume asm: "NFlow c s t f ∧ (∀f'. NFlow c s t f' --> Flow.val c s f' ≤ Flow.val c s f)" assume asm_c: "¬ ¬ (∃ p. isAugmentingPath p)" then obtain p where obt: "isAugmentingPath p" by blast have fct1: "Flow cf s t (augmentingFlow p)" using obt augFlow_resFlow by auto have fct2: "Flow.val cf s (augmentingFlow p) > 0" using obt augFlow_val resCap_gzero isAugmentingPath_def cf.isSimplePath_def by auto have "NFlow c s t (augment (augmentingFlow p))" using fct1 augment_flow_presv Network_axioms unfolding NFlow_def by auto moreover have "Flow.val c s (augment (augmentingFlow p)) > val" using fct1 fct2 augment_flow_value by auto ultimately show "False" using asm by auto qed lemma fofu_II_III: "¬ (∃ p. isAugmentingPath p) ==> ∃k'. NCut c s t k' ∧ val = NCut.cap c k'" proof (intro exI conjI) let ?S = "cf.reachableNodes s" assume asm: "¬ (∃ p. isAugmentingPath p)" hence "t∉?S" unfolding isAugmentingPath_def cf.reachableNodes_def cf.connected_def by (auto dest: cf.isSPath_pathLE) then show CUT: "NCut c s t ?S" proof unfold_locales show "Graph.reachableNodes cf s ⊆ V" using cf.reachable_ss_V s_node resV_netV by auto show "s ∈ Graph.reachableNodes cf s" unfolding Graph.reachableNodes_def Graph.connected_def by (metis Graph.isPath.simps(1) mem_Collect_eq) qed then interpret NCut c s t ?S . interpret NFlowCut c s t f ?S by intro_locales have "∀(u,v)∈outgoing' ?S. f (u,v) = c (u,v)" proof (rule ballI, rule ccontr, clarify) -- ‹Proof by contradiction› fix u v assume "(u,v)∈outgoing' ?S" hence "(u,v)∈E" "u∈?S" "v∉?S" by (auto simp: outgoing'_def) assume "f (u,v) ≠ c (u,v)" hence "f (u,v) < c (u,v)" using capacity_const by (metis (no_types) eq_iff not_le) hence "cf (u, v) ≠ 0" unfolding residualGraph_def using ‹(u,v)∈E› by auto hence "(u, v) ∈ cf.E" unfolding cf.E_def by simp hence "v∈?S" using ‹u∈?S› by (auto intro: cf.reachableNodes_append_edge) thus False using ‹v∉?S› by auto qed hence "(∑e ∈ outgoing' ?S. f e) = cap" unfolding cap_def by auto moreover have "∀(u,v)∈incoming' ?S. f (u,v) = 0" proof (rule ballI, rule ccontr, clarify) -- ‹Proof by contradiction› fix u v assume "(u,v)∈incoming' ?S" hence "(u,v)∈E" "u∉?S" "v∈?S" by (auto simp: incoming'_def) hence "(v,u)∉E" using no_parallel_edge by auto assume "f (u,v) ≠ 0" hence "cf (v, u) ≠ 0" unfolding residualGraph_def using ‹(u,v)∈E› ‹(v,u)∉E› by auto hence "(v, u) ∈ cf.E" unfolding cf.E_def by simp hence "u∈?S" using ‹v∈?S› cf.reachableNodes_append_edge by auto thus False using ‹u∉?S› by auto qed hence "(∑e ∈ incoming' ?S. f e) = 0" unfolding cap_def by auto ultimately show "val = cap" unfolding flow_value[symmetric] netFlow_def by simp qed lemma fofu_III_I: "∃k. NCut c s t k ∧ val = NCut.cap c k ==> isMaxFlow f" proof clarify fix k assume "NCut c s t k" then interpret NCut c s t k . interpret NFlowCut c s t f k by intro_locales assume "val = cap" { fix f' assume "Flow c s t f'" then interpret fc'!: NFlow c s t f' by intro_locales interpret fc'!: NFlowCut c s t f' k by intro_locales have "fc'.val ≤ cap" using fc'.weak_duality . also note ‹val = cap›[symmetric] finally have "fc'.val ≤ val" . } thus "isMaxFlow f" unfolding isMaxFlow_def by simp unfold_locales qed text ‹Finally we can state the Ford-Fulkerson theorem: › theorem ford_fulkerson: shows "isMaxFlow f <-> ¬ Ex isAugmentingPath" and "¬ Ex isAugmentingPath <-> (∃k. NCut c s t k ∧ val = NCut.cap c k)" using fofu_I_II fofu_II_III fofu_III_I by auto subsection ‹Corollaries› text ‹In this subsection we present a few corollaries of the flow-cut relation and the Ford-Fulkerson theorem. › text ‹The outgoing flow of the source is the same as the incoming flow of the sink. Intuitively, this means that no flow is generated or lost in the network, except at the source and sink.› lemma inflow_t_outflow_s: "(∑e ∈ incoming t. f e) = (∑e ∈ outgoing s. f e)" proof - txt ‹We choose a cut between the sink and all other nodes› let ?K = "V - {t}" interpret NFlowCut c s t f ?K using s_node s_not_t by unfold_locales auto txt ‹The cut is chosen such that its outgoing edges are the incoming edges to the sink, and its incoming edges are the outgoing edges from the sink. Note that the sink has no outgoing edges.› have "outgoing' ?K = incoming t" and "incoming' ?K = {}" using no_self_loop no_outgoing_t unfolding outgoing'_def incoming_def incoming'_def outgoing_def V_def by auto hence "(∑e ∈ incoming t. f e) = netFlow" unfolding netFlow_def by auto also have "netFlow = val" by (rule flow_value) also have "val = (∑e ∈ outgoing s. f e)" by (auto simp: val_alt) finally show ?thesis . qed text ‹As an immediate consequence of the Ford-Fulkerson theorem, we get that there is no augmenting path if and only if the flow is maximal.› lemma noAugPath_iff_maxFlow: "¬ (∃ p. isAugmentingPath p) <-> isMaxFlow f" using ford_fulkerson by blast end -- ‹Network with flow› text ‹The value of the maximum flow equals the capacity of the minimum cut› lemma (in Network) maxFlow_minCut: "[|isMaxFlow f; isMinCut c s t k|] ==> Flow.val c s f = NCut.cap c k" proof - assume "isMaxFlow f" "isMinCut c s t k" then interpret Flow c s t f + NCut c s t k unfolding isMaxFlow_def isMinCut_def by simp_all interpret NFlowCut c s t f k by intro_locales from ford_fulkerson ‹isMaxFlow f› obtain k' where K': "NCut c s t k'" "val = NCut.cap c k'" by blast show "val = cap" using ‹isMinCut c s t k› K' weak_duality unfolding isMinCut_def by auto qed end -- ‹Theory›