Theory ResidualGraph

section ‹Residual Graph›
theory ResidualGraph
imports Network
begin
text ‹
  In this theory, we define the residual graph.
  ›

subsection ‹Definition›
text ‹The \emph{residual graph} of a network and a flow indicates how much 
  flow can be effectively pushed along or reverse to a network edge,
  by increasing or decreasing the flow on that edge:›
definition residualGraph :: "_ graph => _ flow => _ graph"
where "residualGraph c f ≡ λ(u, v).
  if (u, v) ∈ Graph.E c then
    c (u, v) - f (u, v)
  else if (v, u) ∈ Graph.E c then
    f (v, u)
  else
    0"

(*<*) (* Old syntax, not used any more *)
  notation (in Graph_Syntax) residualGraph ("⟨\<C>⇩\<f>/ _,/ _⟩" 1000)
(*>*)

text ‹Let's fix a network with a flow @{term f} on it›
context NFlow
begin
  text ‹We abbreviate the residual graph by @{term cf}.›
  abbreviation "cf ≡ residualGraph c f"
  sublocale cf!: Graph cf .
  lemmas cf_def = residualGraph_def[of c f]

subsection ‹Properties›

text ‹The edges of the residual graph are either parallel or reverse 
  to the edges of the network.›
lemma cfE_ss_invE: "Graph.E cf ⊆ E ∪ E¯"
  unfolding residualGraph_def Graph.E_def
  by auto

text ‹The nodes of the residual graph are exactly the nodes of the network.›
lemma resV_netV[simp]: "cf.V = V"
proof
  show "V ⊆ Graph.V cf"
  proof 
    fix u
    assume "u ∈ V"
    then obtain v where "(u, v) ∈ E ∨ (v, u) ∈ E" unfolding V_def by auto
    (* TODO: Use nifty new Isabelle2016 case-distinction features here! *)
    moreover {
      assume "(u, v) ∈ E"
      then have "(u, v) ∈ Graph.E cf ∨ (v, u) ∈ Graph.E cf"
      proof (cases)
        assume "f (u, v) = 0"
        then have "cf (u, v) = c (u, v)"
          unfolding residualGraph_def using `(u, v) ∈ E` by (auto simp:)
        then have "cf (u, v) ≠ 0" using `(u, v) ∈ E` unfolding E_def by auto
        thus ?thesis unfolding Graph.E_def by auto
      next
        assume "f (u, v) ≠ 0"
        then have "cf (v, u) = f (u, v)" unfolding residualGraph_def
          using `(u, v) ∈ E` no_parallel_edge by auto
        then have "cf (v, u) ≠ 0" using ‹f (u, v) ≠ 0› by auto
        thus ?thesis unfolding Graph.E_def by auto
      qed
    } moreover {
      assume "(v, u) ∈ E"
      then have "(v, u) ∈ Graph.E cf ∨ (u, v) ∈ Graph.E cf"
      proof (cases)
        assume "f (v, u) = 0"
        then have "cf (v, u) = c (v, u)"
          unfolding residualGraph_def using `(v, u) ∈ E` by (auto)
        then have "cf (v, u) ≠ 0" using `(v, u) ∈ E` unfolding E_def by auto
        thus ?thesis unfolding Graph.E_def by auto
      next
        assume "f (v, u) ≠ 0"
        then have "cf (u, v) = f (v, u)" unfolding residualGraph_def
          using `(v, u) ∈ E` no_parallel_edge by auto
        then have "cf (u, v) ≠ 0" using ‹f (v, u) ≠ 0› by auto
        thus ?thesis unfolding Graph.E_def by auto
      qed
    } ultimately show "u∈cf.V" unfolding cf.V_def by auto
  qed  
next
  show "Graph.V cf ⊆ V" using cfE_ss_invE unfolding Graph.V_def by auto
qed

text ‹Note, that Isabelle is powerful enough to prove the above case 
  distinctions completely automatically, although it takes some time:›
lemma "cf.V = V"
  unfolding residualGraph_def Graph.E_def Graph.V_def
  using no_parallel_edge[unfolded E_def]
  by auto
  
text ‹As the residual graph has the same nodes as the network, it is also finite:›
sublocale cf!: Finite_Graph cf
  by unfold_locales auto

text ‹The capacities on the edges of the residual graph are non-negative›
lemma resE_nonNegative: "cf e ≥ 0"
proof (cases e; simp)
  fix u v
  {
    assume "(u, v) ∈ E"
    then have "cf (u, v) = c (u, v) - f (u, v)" unfolding cf_def by auto
    hence "cf (u,v) ≥ 0" 
      using capacity_const cap_non_negative by auto
  } moreover {
    assume "(v, u) ∈ E"
    then have "cf (u,v) = f (v, u)" 
      using no_parallel_edge unfolding cf_def by auto
    hence "cf (u,v) ≥ 0" 
      using capacity_const by auto
  } moreover {
    assume "(u, v) ∉ E" "(v, u) ∉ E"
    hence "cf (u,v) ≥ 0" unfolding residualGraph_def by simp
  } ultimately show "cf (u,v) ≥ 0" by blast
qed

text ‹Again, there is an automatic proof›
lemma "cf e ≥ 0"
  apply (cases e)
  unfolding residualGraph_def
  using no_parallel_edge capacity_const cap_positive
  by auto

text ‹All edges of the residual graph are labeled with positive capacities:›
corollary resE_positive: "e ∈ cf.E ==> cf e > 0"
proof -
  assume "e ∈ cf.E"
  hence "cf e ≠ 0" unfolding cf.E_def by auto
  thus ?thesis using resE_nonNegative by (meson eq_iff not_le)
qed 
      
(* TODO: Only one usage: Move or remove! *)  
lemma reverse_flow: "Flow cf s t f' ==> ∀(u, v) ∈ E. f' (v, u) ≤ f (u, v)"
proof -
  assume asm: "Flow cf s t f'"
  {
    fix u v
    assume "(u, v) ∈ E"
    
    then have "cf (v, u) = f (u, v)"
      unfolding residualGraph_def using no_parallel_edge by auto
    moreover have "f' (v, u) ≤ cf (v, u)" using asm[unfolded Flow_def] by auto
    ultimately have "f' (v, u) ≤ f (u, v)" by metis
  }
  thus ?thesis by auto
qed  

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