Theory Ford_Fulkerson

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 sum.union_disjoint[symmetric]) (auto simp: outgoing'_def)
    also have "outgoing' k ∪ ?LCL = (⋃y∈k-{s}. outgoing y) ∪ outgoing s"
      by (auto simp: outgoing_def outgoing'_def s_in_cut)
    also have "(∑e∈(⋃(outgoing ` (k - {s})) ∪ outgoing s). f e) 
      = (∑e∈(⋃(outgoing ` (k - {s}))). f e) + (∑e∈outgoing s. f e)"  
      by (rule sum.union_disjoint) 
         (auto simp: outgoing_def intro: finite_Image)
    also have "(∑e∈(⋃(outgoing ` (k - {s}))). f e) 
      = (∑y ∈ k - {s}. ?SOG y)"
      by (rule sum.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 sum.union_disjoint[symmetric]) (auto simp: incoming'_def)
    also have "incoming' k ∪ ?LCL = (⋃y∈k-{s}. incoming y) ∪ incoming s"
      by (auto simp: incoming_def incoming'_def s_in_cut)
    also have "(∑e∈(⋃(incoming ` (k - {s})) ∪ incoming s). f e) 
      = (∑e∈(⋃(incoming ` (k - {s}))). f e) + (∑e∈incoming s. f e)"  
      by (rule sum.union_disjoint) 
         (auto simp: incoming_def intro: finite_Image)
    also have "(∑e∈(⋃(incoming ` (k - {s}))). f e) 
      = (∑y ∈ k - {s}. ?SIN y)"
      by (rule sum.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 sum_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 sum_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 Flow_def NFlow_def NPreflow_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': Flow c s t f' .
    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.›
corollary 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.›
corollary 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›
corollary (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 "NCut c s t k'" and "val = NCut.cap c k'"
    by blast
  thus "val = cap"
    using ‹isMinCut c s t k› weak_duality
    unfolding isMinCut_def by auto
qed    

end ― ‹Theory›