Theory Network

section ‹Flows, Cuts, and Networks›
theory Network
imports Graph
begin
text ‹
  In this theory, we define the basic concepts of flows, cuts, 
  and (flow) networks.
  ›  

subsection ‹Definitions›

subsubsection ‹Flows›
text ‹An $s$-$t$ flow on a graph is a labeling of the edges with 
  real values, such that: 
  \begin{description}
    \item[capacity constraint] the flow on each edge is non-negative and 
      does not exceed the edge's capacity;
    \item[conservation constraint] for all nodes except $s$ and $t$, 
      the incoming flows equal the outgoing flows.
  \end{description}    
›

type_synonym 'capacity flow = "edge => 'capacity"

locale Flow = Graph c for c :: "'capacity::linordered_idom graph" +
  fixes s t :: node
  fixes f :: "'capacity::linordered_idom flow"
  (* TODO: Move ∀-quantifiers to meta-level!? *)
  assumes capacity_const: "∀e. 0 ≤ f e ∧ f e ≤ c e"
  assumes conservation_const: "∀v ∈ V - {s, t}. 
    (∑e ∈ incoming v. f e) = (∑e ∈ outgoing v. f e)"
begin
  text ‹The value of a flow is the flow that leaves $s$ and does not return.›
  definition val :: "'capacity"
    where "val ≡ (∑e ∈ outgoing s. f e) - (∑e ∈ incoming s. f e)"
end

locale Finite_Flow = Flow c s t f + Finite_Graph c 
  for c :: "'capacity::linordered_idom graph" and s t f

(*<*) (* Old syntax, not used any more *)
  context Graph_Syntax begin    
    abbreviation Flow_val :: "'capacity::linordered_idom graph => node => 'capacity flow => 'capacity"
      ("\<lbrace>_,/ _/ \<parallel>⇩F/ |_|\<rbrace>" 1000) 
    where "\<lbrace>c, s \<parallel>⇩F |f|\<rbrace> ≡ Flow.val c s f"
  end  
(*>*)


subsubsection ‹Cuts›
text ‹A cut is a partitioning of the nodes into two sets. 
  We define it by just specifying one of the partitions.›
type_synonym cut = "node set" 

locale Cut = Graph +  (* TODO: We probably do not need the cut-locale, 
  only NCut.*)
  fixes k :: cut
  assumes cut_ss_V: "k ⊆ V"

subsubsection ‹Networks›
text ‹A network is a finite graph with two distinct nodes, source and sink, 
  such that all edges are labeled with positive capacities. 
  Moreover, we assume that 
  \begin{itemize}
    \item the source has no incoming edges, and the sink has no outgoing edges
    \item we allow no parallel edges, i.e., for any edge, the reverse edge must not be in the network
    \item Every node must lay on a path from the source to the sink
  \end{itemize}
›

locale Network = Graph c for c :: "'capacity::linordered_idom graph" +
  fixes s t :: node
  assumes s_node: "s ∈ V"
  assumes t_node: "t ∈ V"
  assumes s_not_t: "s ≠ t"
  assumes cap_non_negative: "∀u v. c (u, v) ≥ 0"
  assumes no_incoming_s: "∀u. (u, s) ∉ E"
  assumes no_outgoing_t: "∀u. (t, u) ∉ E"
  assumes no_parallel_edge: "∀u v. (u, v) ∈ E --> (v, u) ∉ E"
  assumes nodes_on_st_path: "∀v ∈ V. connected s v ∧ connected v t"
  assumes finite_reachable: "finite (reachableNodes s)"
begin
  text ‹Our assumptions imply that there are no self loops›
  lemma no_self_loop: "∀u. (u, u) ∉ E"
    using no_parallel_edge by auto

  text ‹A flow is maximal, if it has a maximal value›  
  definition isMaxFlow :: "_ flow => bool" 
  where "isMaxFlow f ≡ Flow c s t f ∧ 
    (∀f'. Flow c s t f' --> Flow.val c s f' ≤ Flow.val c s f)"

end  
  
subsubsection ‹Networks with Flows and Cuts›  
text ‹For convenience, we define locales for a network with a fixed flow,
  and a network with a fixed cut›

locale NFlow = Network c s t + Flow c s t f 
  for c :: "'capacity::linordered_idom graph" and s t f

lemma (in Network) isMaxFlow_alt: 
  "isMaxFlow f <-> NFlow c s t f ∧ 
    (∀f'. NFlow c s t f' --> Flow.val c s f' ≤ Flow.val c s f)"
  unfolding isMaxFlow_def     
  by (auto simp: NFlow_def) (intro_locales)

text ‹A cut in a network separates the source from the sink›
locale NCut = Network c s t + Cut c k 
  for c :: "'capacity::linordered_idom graph" and s t k +
  assumes s_in_cut: "s ∈ k"
  assumes t_ni_cut: "t ∉ k"
begin
  text ‹The capacity of the cut is the capacity of all edges going from the 
    source's side to the sink's side.›
  definition cap :: "'capacity"
    where "cap ≡ (∑e ∈ outgoing' k. c e)"
end

text ‹A minimum cut is a cut with minimum capacity.› 
(* TODO: The definitions of min-cut and max-flow are done in different contexts. 
  Align, probably both in network context! *)
definition isMinCut :: "_ graph => nat => nat => cut => bool" 
where "isMinCut c s t k ≡ NCut c s t k ∧
  (∀k'. NCut c s t k' --> NCut.cap c k ≤ NCut.cap c k')"
  
(*<*) (* Old Syntax, not used any more*)
abbreviation (in Graph_Syntax) NCut_cap :: "'capacity::linordered_idom graph => node set => 'capacity"
  ("\<lbrace>_/ \<parallel>⇩N⇩C/ Cap/ (_)\<rbrace>" 1000) 
where "\<lbrace>c \<parallel>⇩N⇩C Cap k\<rbrace> ≡ NCut.cap c k"
(*>*)

subsection ‹Properties›
subsubsection ‹Flows›

context Flow 
begin

text ‹Only edges are labeled with non-zero flows›
lemma zero_flow_simp[simp]:
  "(u,v)∉E ==> f(u,v) = 0"
  by (metis capacity_const eq_iff zero_cap_simp)

text ‹We provide a useful equivalent formulation of the 
  conservation constraint.›
lemma conservation_const_pointwise: 
  assumes "u∈V - {s,t}"
  shows "(∑v∈E``{u}. f (u,v)) = (∑v∈E¯``{u}. f (v,u))"
  using conservation_const assms
  by (auto simp: sum_incoming_pointwise sum_outgoing_pointwise)

end -- ‹Flow›   

context Finite_Flow 
begin

text ‹The summation of flows over incoming/outgoing edges can be 
  extended to a summation over all possible predecessor/successor nodes,
  as the additional flows are all zero.›  
lemma sum_outgoing_alt_flow:
  fixes g :: "edge => 'capacity"
  assumes "u∈V"
  shows "(∑e∈outgoing u. f e) = (∑v∈V. f (u,v))"
  apply (subst sum_outgoing_alt)
  using assms capacity_const
  by auto
  
lemma sum_incoming_alt_flow:
  fixes g :: "edge => 'capacity"
  assumes "u∈V"
  shows "(∑e∈incoming u. f e) = (∑v∈V. f (v,u))"
  apply (subst sum_incoming_alt)
  using assms capacity_const
  by auto
end -- ‹Finite Flow›   

subsubsection ‹Networks›  
context Network
begin
text ‹The network constraints implies that all nodes are 
  reachable from the source node›  

lemma reachable_is_V[simp]: "reachableNodes s = V"
proof
  show "V ⊆ reachableNodes s"
  unfolding reachableNodes_def using s_node nodes_on_st_path
    by auto
qed (simp add: s_node reachable_ss_V)

sublocale Finite_Graph 
  apply unfold_locales
  using reachable_is_V finite_reachable by auto
  
lemma cap_positive: "e ∈ E ==> c e > 0"
  unfolding E_def using cap_non_negative le_neq_trans by fastforce 

lemma V_not_empty: "V≠{}" using s_node by auto
lemma E_not_empty: "E≠{}" using V_not_empty by (auto simp: V_def)

end -- ‹Network›

subsubsection ‹Networks with Flow›

context NFlow 
begin

sublocale Finite_Flow by unfold_locales

text ‹As there are no edges entering the source/leaving the sink, 
  also the corresponding flow values are zero:›
lemma no_inflow_s: "∀e ∈ incoming s. f e = 0" (is ?thesis)
proof (rule ccontr)
  assume "¬(∀e ∈ incoming s. f e = 0)"
  then obtain e where obt1: "e ∈ incoming s ∧ f e ≠ 0" by blast
  then have "e ∈ E" using incoming_def by auto
  thus "False" using obt1 no_incoming_s incoming_def by auto
qed
  
lemma no_outflow_t: "∀e ∈ outgoing t. f e = 0"
proof (rule ccontr)
  assume "¬(∀e ∈ outgoing t. f e = 0)"
  then obtain e where obt1: "e ∈ outgoing t ∧ f e ≠ 0" by blast
  then have "e ∈ E" using outgoing_def by auto
  thus "False" using obt1 no_outgoing_t outgoing_def by auto
qed

text ‹Thus, we can simplify the definition of the value:›  
corollary val_alt: "val = (∑e ∈ outgoing s. f e)"
  unfolding val_def by (auto simp: no_inflow_s)

text ‹For an edge, there is no reverse edge, and thus, no flow in the reverse direction:›
lemma zero_rev_flow_simp[simp]: "(u,v)∈E ==> f(v,u) = 0"
  using no_parallel_edge by auto

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