Theory Augmenting_Path

section ‹Augmenting Paths›
theory Augmenting_Path
imports ResidualGraph
begin
text ‹We define the concept of an augmenting path in the residual graph,
  and the residual flow induced by an augmenting path.›

text ‹We fix a network with a flow @{term f} on it.›
context NFlow
begin

subsection ‹Definitions›

text ‹An \emph{augmenting path} is a simple path from the source to the sink in the residual graph:›
definition isAugmentingPath :: "path => bool"
where "isAugmentingPath p ≡ cf.isSimplePath s p t"

text ‹The \emph{residual capacity} of an augmenting path is the smallest capacity 
  annotated to its edges:›
definition resCap :: "path => 'capacity"
where "resCap p ≡ Min {cf e | e. e ∈ set p}"

lemma resCap_alt: "resCap p = Min (cf`set p)"  
  -- ‹Useful characterization for finiteness arguments›
  unfolding resCap_def apply (rule arg_cong[where f=Min]) by auto

text ‹An augmenting path induces an \emph{augmenting flow}, which pushes as 
  much flow as possible along the path:›
definition augmentingFlow :: "path => 'capacity flow"
where "augmentingFlow p ≡ λ(u, v).
  if (u, v) ∈ (set p) then
    resCap p
  else
    0"

(*<*) (* Old syntax sugar, not used any more *)
end
  locale NFlow_Loc_Syntax = Graph_Loc_Syntax + NFlow begin
    notation isAugmentingPath ("⟨=>⇧A/ _⟩" 1000)
    notation resCap ("⟨∇/ _⟩" 1000)
    notation augmentingFlow ("⟨\<F>⇩\<p>/ _⟩" 1000)
  end

  context Graph_Syntax begin  
    abbreviation NFlow_isAugmentingPath :: "_ graph => nat => nat => _ flow => path => bool"
      ("\<lbrace>_,/ _,/ _,/ _/ \<parallel>⇩N⇩F/ ⟨=>⇧A/ _⟩\<rbrace>" 1000)
    where "\<lbrace>c, s, t, f \<parallel>⇩N⇩F ⟨=>⇧A p⟩\<rbrace> ≡ NFlow.isAugmentingPath c s t f p"
    
    abbreviation NFlow_resCap :: "_ graph => _ flow => path => _"
      ("\<lbrace>_,/ _/ \<parallel>⇩N⇩F/ ⟨∇/ _⟩\<rbrace>" 1000)
    where "\<lbrace>c, f \<parallel>⇩N⇩F ⟨∇ p⟩\<rbrace> ≡ NFlow.resCap c f p"
    
    abbreviation NFlow_augmentingFlow :: "_ graph => _ flow => path => _ flow"
      ("\<lbrace>_,/ _/ \<parallel>⇩N⇩F/ ⟨\<F>⇩\<p>/ _⟩\<rbrace>" 1000)
    where "\<lbrace>c, f \<parallel>⇩N⇩F ⟨\<F>⇩\<p> p⟩\<rbrace> ≡ NFlow.augmentingFlow c f p"
  end
context NFlow begin
(*>*)

subsection ‹Augmenting Flow is Valid Flow›
text ‹In this section, we show that the augmenting flow induced by an 
  augmenting path is a valid flow in the residual graph.

  We start with some auxiliary lemmas.›

text ‹The residual capacity of an augmenting path is always positive.›
lemma resCap_gzero_aux: "cf.isPath s p t ==> 0<resCap p"
proof -
  assume PATH: "cf.isPath s p t"
  hence "set p≠{}" using s_not_t by (auto)
  moreover have "∀e∈set p. cf e > 0"
    using cf.isPath_edgeset[OF PATH] resE_positive by (auto)
  ultimately show ?thesis unfolding resCap_alt by (auto)
qed 

lemma resCap_gzero: "isAugmentingPath p ==> 0<resCap p"
  using resCap_gzero_aux[of p] 
  by (auto simp: isAugmentingPath_def cf.isSimplePath_def)

text ‹As all edges of the augmenting flow have the same value, we can factor 
  this out from a summation:›
lemma setsum_augmenting_alt:
  assumes "finite A"          
  shows "(∑e ∈ A. (augmentingFlow p) e) 
        = resCap p * of_nat (card (A∩set p))"
proof -
  have "(∑e ∈ A. (augmentingFlow p) e) = setsum (λ_. resCap p) (A∩set p)"
    apply (subst setsum.inter_restrict)
    apply (auto simp: augmentingFlow_def assms)
    done
  thus ?thesis by auto
qed  

lemma augFlow_resFlow: "isAugmentingPath p ==> Flow cf s t (augmentingFlow p)"
proof (unfold_locales; intro allI ballI)
  assume AUG: "isAugmentingPath p"
  hence SPATH: "cf.isSimplePath s p t" by (simp add: isAugmentingPath_def)
  hence PATH: "cf.isPath s p t" by (simp add: cf.isSimplePath_def)

  { text ‹We first show the capacity constraint›
    fix e
    show "0 ≤ (augmentingFlow p) e ∧ (augmentingFlow p) e ≤ cf e"
    proof cases 
      assume "e ∈ set p"
      hence "resCap p ≤ cf e" unfolding resCap_alt by auto
      moreover  have "(augmentingFlow p) e = resCap p" 
        unfolding augmentingFlow_def using ‹e ∈ set p› by auto
      moreover have "0 < resCap p" using resCap_gzero[OF AUG] by simp 
      ultimately show ?thesis by auto
    next
      assume "e ∉ set p"
      hence "(augmentingFlow p) e = 0" unfolding augmentingFlow_def by auto
      thus ?thesis using resE_nonNegative by auto
    qed
  } 

  { text ‹Next, we show the conservation constraint›
    fix v
    assume asm_s: "v ∈ Graph.V cf - {s, t}"

    have "card (Graph.incoming cf v ∩ set p) = card (Graph.outgoing cf v ∩ set p)"
    proof (cases)  
      assume "v∈set (cf.pathVertices_fwd s p)"
      from cf.split_path_at_vertex[OF this PATH] obtain p1 p2 where
        P_FMT: "p=p1@p2" 
        and 1: "cf.isPath s p1 v"
        and 2: "cf.isPath v p2 t" 
        .
      from 1 obtain p1' u1 where [simp]: "p1=p1'@[(u1,v)]"    
        using asm_s by (cases p1 rule: rev_cases) (auto simp: split_path_simps)
      from 2 obtain p2' u2 where [simp]: "p2=(v,u2)#p2'"    
        using asm_s by (cases p2) (auto)
      from 
        cf.isSPath_sg_outgoing[OF SPATH, of v u2]  
        cf.isSPath_sg_incoming[OF SPATH, of u1 v]
        cf.isPath_edgeset[OF PATH] 
      have "cf.outgoing v ∩ set p = {(v,u2)}" "cf.incoming v ∩ set p = {(u1,v)}"
        by (fastforce simp: P_FMT cf.outgoing_def cf.incoming_def)+
      thus ?thesis by auto
    next
      assume "v∉set (cf.pathVertices_fwd s p)"
      then have "∀u. (u,v)∉set p ∧ (v,u)∉set p"
        by (auto dest: cf.pathVertices_edge[OF PATH])
      hence "cf.incoming v ∩ set p = {}" "cf.outgoing v ∩ set p = {}"
        by (auto simp: cf.incoming_def cf.outgoing_def)
      thus ?thesis by auto
    qed  
    thus "(∑e ∈ Graph.incoming cf v. (augmentingFlow p) e) =
      (∑e ∈ Graph.outgoing cf v. (augmentingFlow p) e)"
      by (auto simp: setsum_augmenting_alt)
  }
qed


subsection ‹Value of Augmenting Flow is Residual Capacity›
text ‹Finally, we show that the value of the augmenting flow is the residual 
  capacity of the augmenting path›

lemma augFlow_val: 
  "isAugmentingPath p ==> Flow.val cf s (augmentingFlow p) = resCap p"
proof -
  assume AUG: "isAugmentingPath p"
  with augFlow_resFlow interpret f!: Flow cf s t "augmentingFlow p" .

  note AUG 
  hence SPATH: "cf.isSimplePath s p t" by (simp add: isAugmentingPath_def)
  hence PATH: "cf.isPath s p t" by (simp add: cf.isSimplePath_def)
  then obtain v p' where "p=(s,v)#p'" "(s,v)∈cf.E" 
    using s_not_t by (cases p) auto
  hence "cf.outgoing s ∩ set p = {(s,v)}"  
    using cf.isSPath_sg_outgoing[OF SPATH, of s v] 
    using cf.isPath_edgeset[OF PATH] 
    by (fastforce simp: cf.outgoing_def)
  moreover have "cf.incoming s ∩ set p = {}" using SPATH no_incoming_s
    by (auto 
      simp: cf.incoming_def ‹p=(s,v)#p'› in_set_conv_decomp[where xs=p']
      simp: cf.isSimplePath_append cf.isSimplePath_cons)  
  ultimately show ?thesis
    unfolding f.val_def
    by (auto simp: setsum_augmenting_alt)
qed    

end -- ‹Network with flow›
end -- ‹Theory›