Theory Augmenting_Flow

section ‹Augmenting Flows›
theory Augmenting_Flow
imports Residual_Graph
begin

text ‹
  In this theory, we define the concept of an augmenting flow,
  augmentation with a flow, and show that augmentation of a flow 
  with an augmenting flow yields a valid flow again.
  ›

text ‹We assume that there is a network with a flow @{term f} on it›
context NFlow
begin

subsection ‹Augmentation of a Flow›
text ‹The flow can be augmented by another flow, by adding the flows 
  of edges parallel to edges in the network, and subtracting the edges 
  reverse to edges in the network.›
(* TODO: Define in network locale, with ↑ syntax. *)
definition augment :: "'capacity flow  'capacity flow"
where "augment f'  λ(u, v).
  if (u, v)  E then
    f (u, v) + f' (u, v) - f' (v, u)
  else
    0"

text ‹We define a syntax similar to Cormen et el.:›    
abbreviation (input) augment_syntax (infix "" 55) 
  where "f f'. ff'  NFlow.augment c f f'"
text ‹such that we can write @{term [source] "ff'"} for the flow @{term f} 
  augmented by @{term f'}.›


subsection ‹Augmentation yields Valid Flow›
text ‹We show that, if we augment the flow with a valid flow of
  the residual graph, the augmented flow is a valid flow again, i.e. 
  it satisfies the capacity and conservation constraints:›
context 
  ― ‹Let the \emph{residual flow} @{term f'} be a flow in the residual graph›
  fixes f' :: "'capacity flow"
  assumes f'_flow: "Flow cf s t f'"
begin  

interpretation f': Flow cf s t f' by (rule f'_flow)

subsubsection ‹Capacity Constraint›
text ‹First, we have to show that the new flow satisfies the capacity constraint:›
(* FIXME: Indentation unfortunate, but required to extract snippet for latex presentation *)    
text_raw ‹\DefineSnippet{augment_flow_presv_cap}{›  
lemma augment_flow_presv_cap: 
  shows "0  (ff')(u,v)  (ff')(u,v)  c(u,v)"
proof (cases "(u,v)E"; rule conjI) 
  assume [simp]: "(u,v)E"
  hence "f(u,v) = cf(v,u)" 
    using no_parallel_edge by (auto simp: residualGraph_def)
  also have "cf(v,u)  f'(v,u)" using f'.capacity_const by auto
  finally(*<*)(xtrans)(*>*) have "f'(v,u)  f(u,v)" .

(*<*){
    note [trans] = xtrans
  (*>*)text_raw ‹\isanewline›

  text_raw ‹\ \ ›have "(ff')(u,v) = f(u,v) + f'(u,v) - f'(v,u)"
    by (auto simp: augment_def)
  also have "  f(u,v) + f'(u,v) - f(u,v)"
  (*<*)(is "_  ")(*>*)  using f'(v,u)  f(u,v) by auto
  also have " = f'(u,v)" by auto
  also have "  0" using f'.capacity_const by auto
  finally show "(ff')(u,v)  0" .
  (*<*)}(*>*)
    
  have "(ff')(u,v) = f(u,v) + f'(u,v) - f'(v,u)" 
    by (auto simp: augment_def)
  also have "  f(u,v) + f'(u,v)" using f'.capacity_const by auto
  also have "  f(u,v) + cf(u,v)" using f'.capacity_const by auto
  also have " = f(u,v) + c(u,v) - f(u,v)" 
    by (auto simp: residualGraph_def)
  also have " = c(u,v)" by auto
  finally show "(ff')(u, v)  c(u, v)" .
qed (auto simp: augment_def cap_positive)
text_raw ‹}%EndSnippet›

  
subsubsection ‹Conservation Constraint›
text ‹In order to show the conservation constraint, we need some 
  auxiliary lemmas first.›

text ‹As there are no parallel edges in the network, and all edges 
  in the residual graph are either parallel or reverse to a network edge,
  we can split summations of the residual flow over outgoing/incoming edges in the 
  residual graph to summations over outgoing/incoming edges in the network.

  Note that the term @{term E``{u}} characterizes the successor nodes of @{term u},
  and @{term E¯``{u}} characterizes the predecessor nodes of @{term u}.
›
(* TODO: Introduce pred/succ functions on Graph *)
private lemma split_rflow_outgoing: 
  "(vcf.E``{u}. f' (u,v)) = (vE``{u}. f'(u,v)) + (vE¯``{u}. f'(u,v))"
  (is "?LHS = ?RHS")
proof -
  from no_parallel_edge have DJ: "E``{u}  E¯``{u} = {}" by auto

  have "?LHS = (vE``{u}  E¯``{u}. f' (u,v))"
    apply (rule sum.mono_neutral_left)
    using cfE_ss_invE
    by (auto intro: finite_Image)
  also have " = ?RHS"
    apply (subst sum.union_disjoint[OF _ _ DJ])
    by (auto intro: finite_Image)
  finally show "?LHS = ?RHS" .
qed  

private lemma split_rflow_incoming: 
  "(vcf.E¯``{u}. f' (v,u)) = (vE``{u}. f'(v,u)) + (vE¯``{u}. f'(v,u))"
  (is "?LHS = ?RHS")
proof -
  from no_parallel_edge have DJ: "E``{u}  E¯``{u} = {}" by auto

  have "?LHS = (vE``{u}  E¯``{u}. f' (v,u))"
    apply (rule sum.mono_neutral_left)
    using cfE_ss_invE
    by (auto intro: finite_Image)
  also have " = ?RHS"
    apply (subst sum.union_disjoint[OF _ _ DJ])
    by (auto intro: finite_Image)
  finally show "?LHS = ?RHS" .
qed  

text ‹For proving the conservation constraint, let's fix a node @{term u}, which
  is neither the source nor the sink: ›
context 
  fixes u :: node
  assumes U_ASM: "uV - {s,t}"
begin  

text ‹We first show an auxiliary lemma to compare the 
  effective residual flow on incoming network edges to
  the effective residual flow on outgoing network edges.
  
  Intuitively, this lemma shows that the effective residual flow added to the 
  network edges satisfies the conservation constraint.
›
private lemma flow_summation_aux:
  shows "(vE``{u}. f' (u,v))  - (vE``{u}. f' (v,u))
       = (vE¯``{u}. f' (v,u)) - (vE¯``{u}. f' (u,v))"
   (is "?LHS = ?RHS" is "?A - ?B = ?RHS")
proof -
  text ‹The proof is by splitting the flows, and careful 
    cancellation of the summands.›
  have "?A = (vcf.E``{u}. f' (u, v)) - (vE¯``{u}. f' (u, v))"
    by (simp add: split_rflow_outgoing)
  also have "(vcf.E``{u}. f' (u, v)) = (vcf.E¯``{u}. f' (v, u))"  
    using U_ASM
    by (simp add: f'.conservation_const_pointwise)
  finally have "?A = (vcf.E¯``{u}. f' (v, u)) - (vE¯``{u}. f' (u, v))" 
    by simp
  moreover
  have "?B = (vcf.E¯``{u}. f' (v, u)) - (vE¯``{u}. f' (v, u))"
    by (simp add: split_rflow_incoming)
  ultimately show "?A - ?B = ?RHS" by simp
qed    

text ‹Finally, we are ready to prove that the augmented flow satisfies the 
  conservation constraint:›
lemma augment_flow_presv_con: 
  shows "(e  outgoing u. augment f' e) = (e  incoming u. augment f' e)"
    (is "?LHS = ?RHS")
proof -
  text ‹We define shortcuts for the successor and predecessor nodes of @{term u} 
    in the network:›
  let ?Vo = "E``{u}" let ?Vi = "E¯``{u}"

  text ‹Using the auxiliary lemma for the effective residual flow,
    the proof is straightforward:›
  have "?LHS = (v?Vo. augment f' (u,v))"
    by (auto simp: sum_outgoing_pointwise)
  also have " 
    = (v?Vo. f (u,v) + f'(u,v) - f'(v,u))"  
    by (auto simp: augment_def)
  also have " 
    = (v?Vo. f (u,v)) + (v?Vo. f' (u,v)) - (v?Vo. f' (v,u))"
    by (auto simp: sum_subtractf sum.distrib)
  also have " 
    = (v?Vi. f (v,u)) + (v?Vi. f' (v,u)) - (v?Vi. f' (u,v))" 
    by (auto simp: conservation_const_pointwise[OF U_ASM] flow_summation_aux)
  also have " 
    = (v?Vi. f (v,u) + f' (v,u) - f' (u,v))" 
    by (auto simp: sum_subtractf sum.distrib)
  also have " 
    = (v?Vi. augment f' (v,u))"  
    by (auto simp: augment_def)
  also have " 
    = ?RHS"
    by (auto simp: sum_incoming_pointwise)
  finally show "?LHS = ?RHS" .
qed  
text ‹Note that we tried to follow the proof presented by Cormen et al.~cite"CLRS09" 
  as closely as possible. Unfortunately, this proof generalizes the summation to all 
  nodes immediately, rendering the first equation invalid.
  Trying to fix this error, we encountered that the step that uses the conservation 
  constraints on the augmenting flow is more subtle as indicated in the original proof.
  Thus, we moved this argument to an auxiliary lemma. ›


end ― ‹@{term u} is node›

text ‹As main result, we get that the augmented flow is again a valid flow.›
corollary augment_flow_presv: "Flow c s t (ff')"
  using augment_flow_presv_cap augment_flow_presv_con 
  by (rule_tac intro_Flow) auto

subsection ‹Value of the Augmented Flow›
text ‹Next, we show that the value of the augmented flow is the sum of the values
  of the original flow and the augmenting flow.›
  
lemma augment_flow_value: "Flow.val c s (ff') = val + Flow.val cf s f'"
proof -
  interpret f'': Flow c s t "ff'" using augment_flow_presv . 

  txt ‹For this proof, we set up Isabelle's rewriting engine for rewriting of sums.
    In particular, we add lemmas to convert sums over incoming or outgoing 
    edges to sums over all vertices. This allows us to write the summations
    from Cormen et al.~a bit more concise, leaving some of the tedious 
    calculation work to the computer.›
  note sum_simp_setup[simp] = 
    sum_outgoing_alt[OF capacity_const] s_node
    sum_incoming_alt[OF capacity_const]
    cf.sum_outgoing_alt[OF f'.capacity_const]
    cf.sum_incoming_alt[OF f'.capacity_const]
    sum_outgoing_alt[OF f''.capacity_const]
    sum_incoming_alt[OF f''.capacity_const]
    sum_subtractf sum.distrib
  
  txt ‹Note that, if neither an edge nor its reverse is in the graph,
    there is also no edge in the residual graph, and thus the flow value
    is zero.›  
  have aux1: "f'(u,v) = 0" if "(u,v)E" "(v,u)E" for u v
  proof -
    from that cfE_ss_invE have "(u,v)cf.E" by auto
    thus "f'(u,v) = 0" by auto
  qed  

  txt ‹Now, the proposition follows by straightforward rewriting of 
    the summations:›
  have "f''.val = (uV. augment f' (s, u) - augment f' (u, s))" 
    unfolding f''.val_def by simp
  also have " = (uV. f (s, u) - f (u, s) + (f' (s, u) - f' (u, s)))"
    ― ‹Note that this is the crucial step of the proof, which Cormen et al. leave as an exercise.›
    by (rule sum.cong) (auto simp: augment_def no_parallel_edge aux1)
  also have " = val + Flow.val cf s f'"  
    unfolding val_def f'.val_def by simp
  finally show "f''.val = val + f'.val" .  
qed    

txt ‹Note, there is also an automatic proof. When creating the above 
    explicit proof, this automatic one has been used to extract meaningful
    subgoals, abusing Isabelle as a term rewriter.›
lemma "Flow.val c s (ff') = val + Flow.val cf s f'"
proof -
  interpret f'': Flow c s t "ff'" using augment_flow_presv . 

  have aux1: "f'(u,v) = 0" if A: "(u,v)E" "(v,u)E" for u v
  proof -
    from A cfE_ss_invE have "(u,v)cf.E" by auto
    thus "f'(u,v) = 0" by auto
  qed  

  show ?thesis
    unfolding val_def f'.val_def f''.val_def
    apply (simp del:
      add: 
      sum_outgoing_alt[OF capacity_const] s_node
      sum_incoming_alt[OF capacity_const]
      sum_outgoing_alt[OF f''.capacity_const]
      sum_incoming_alt[OF f''.capacity_const]
      cf.sum_outgoing_alt[OF f'.capacity_const]
      cf.sum_incoming_alt[OF f'.capacity_const]
      sum_subtractf[symmetric] sum.distrib[symmetric]
      )
    apply (rule sum.cong)
    apply (auto simp: augment_def no_parallel_edge aux1)
    done
qed


end ― ‹Augmenting flow›
end ― ‹Network flow›

end ― ‹Theory›