Theory Flow_Networks.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› preflow on a graph is a labeling of the edges with 
  values from a linearly ordered integral domain, such that: 
  \begin{description}
    \item[capacity constraint] the flow on each edge is non-negative and 
      does not exceed the edge's capacity;
    \item[non-deficiency constraint] for all nodes except ‹s› and ‹t›, 
      the incoming flow greater or equal to the outgoing flow.
  \end{description}    
›
  
type_synonym 'capacity flow = "edge ⇒ 'capacity"

locale Preflow = Graph c for c :: "'capacity::linordered_idom graph" +
  fixes s t :: node
  fixes f :: "'capacity flow"  
  (* TODO: Move ∀-quantifiers to meta-level!? *)
  assumes capacity_const: "∀e. 0 ≤ f e ∧ f e ≤ c e"
  assumes no_deficient_nodes: "∀v ∈ V-{s,t}.
    (∑e∈outgoing v. f e) ≤ (∑e∈incoming v. f e)" 
begin
end  
  
  
text ‹An ‹s›-‹t› ∗‹flow› on a graph is a preflow that has no active nodes except 
  source and sink, where a node is ∗‹active› iff it has more incoming flow 
  than outgoing flow.
›

locale Flow = Preflow c s t f
  for c :: "'capacity::linordered_idom graph"
  and s t :: node
  and f +
  assumes no_active_nodes: 
    "∀v ∈ V - {s,t}. (∑e∈outgoing v. f e) ≥ (∑e∈incoming v. f e)"
begin
  text ‹For a flow, inflow equals outflow for all nodes except sink and source.
    This is called ∗‹conservation›. ›
  lemma conservation_const: 
    "∀v ∈ V - {s, t}. (∑e ∈ incoming v. f e) = (∑e ∈ outgoing v. f e)"
    using no_deficient_nodes no_active_nodes 
    by force
  
  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_Preflow = Preflow c s t f + Finite_Graph c 
  for c :: "'capacity::linordered_idom graph" and s t f
  
locale Finite_Flow = Flow c s t f + Finite_Preflow c s t f
  for c :: "'capacity::linordered_idom graph" and s t f


subsubsection ‹Cuts›
text ‹A ∗‹cut› is a partitioning of the nodes into two sets. 
  We define it by just specifying one of the partitions. 
  The other partition is implicitly given by the remaining nodes.›
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 
  ▪ The source has no incoming edges, and the sink has no outgoing edges.
  ▪ There are no parallel edges, i.e., for any edge, the reverse edge must not be in the network.
  ▪ Every node must lay on a path from the source to the sink.

  Notes on the formalization
  ▪ We encode the graph by a mapping ‹c›, such that ‹c (u,v)› is 
    the capacity of edge ‹(u,v)›, or ‹0›, if there is no edge from ‹u› to ‹v›.
    Thus, in the formalization below, we only demand 
    that ‹c (u,v) ≥ 0› for all ‹u› and ‹v›.
  ▪ We only demand the set of nodes reachable from the source to be finite.
    Together with the constraint that all nodes lay on a path from the source,
    this implies that the graph is finite.
›

locale Network = Graph c for c :: "'capacity::linordered_idom graph" +
  fixes s t :: node
  assumes s_node[simp, intro!]: "s ∈ V"
  assumes t_node[simp, intro!]: "t ∈ V"
  assumes s_not_t[simp, intro!]: "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 ‹Edges have positive capacity›
  lemma edge_cap_positive: "(u,v)∈E ⟹ c (u,v) > 0"
    unfolding E_def using cap_non_negative[THEN spec2, of u v] by simp
  
  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: reachable_ss_V)
  
  text ‹Thus, the network is actually a finite graph.›
  sublocale Finite_Graph 
    apply unfold_locales
    using reachable_is_V finite_reachable by auto
      
  
  text ‹Our assumptions imply that there are no self loops›
  lemma no_self_loop: "∀u. (u, u) ∉ E"
    using no_parallel_edge by auto

  lemma adjacent_not_self[simp, intro!]: "v ∉ adjacent_nodes v"
    unfolding adjacent_nodes_def using no_self_loop 
    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)"
    
  definition "is_max_flow_val fv ≡ ∃f. isMaxFlow f ∧ fv=Flow.val c s f"

(* TODO: Can we prove existence of a maximum flow *easily*, i.e.,
  without going over the min-cut-max-flow theorem or the Ford-Fulkerson method?
  definition "max_flow_val ≡ THE fv. is_max_flow_val fv"
*)  
    
  lemma t_not_s[simp]: "t ≠ s" using s_not_t by blast

      
  text ‹The excess of a node is the difference between incoming and 
    outgoing flow.› (* TODO: Define in context of preflow!? *)
  definition excess :: "'capacity flow ⇒ node ⇒ 'capacity" where
    "excess f v ≡ (∑e∈incoming v. f e) - (∑e∈outgoing v. f e)"
  
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 NPreflow = Network c s t + Preflow c s t f 
  for c :: "'capacity::linordered_idom graph" and s t f
begin
  
end
    
locale NFlow = NPreflow c s t f + 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 Flow_def NPreflow_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')"

subsection ‹Properties›
subsubsection ‹Flows›

context Preflow 
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)

lemma f_non_negative: "0 ≤ f e"
  using capacity_const by (cases e) auto
    
lemma sum_f_non_negative: "sum f X ≥ 0" using capacity_const
  by (auto simp: sum_nonneg f_non_negative) 
    
end ― ‹Preflow›   
    
context Flow
begin
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)

text ‹The value of the flow is bounded by the capacity of the 
  outgoing edges of the source node›
lemma val_bounded: 
  "-(∑e∈incoming s. c e) ≤ val"
  "val ≤ (∑e∈outgoing s. c e)"
proof -
  have 
    "sum f (outgoing s) ≤ sum c (outgoing s)"
    "sum f (incoming s) ≤ sum c (incoming s)"
    using capacity_const by (auto intro!: sum_mono)
  thus "-(∑e∈incoming s. c e) ≤ val" "val ≤ (∑e∈outgoing s. c e)" 
    using sum_f_non_negative[of "incoming s"] 
    using sum_f_non_negative[of "outgoing s"]  
    unfolding val_def by auto 
qed    
    
    
end ― ‹Flow›   

text ‹Introduce a flow via the conservation constraint›  
lemma (in Graph) intro_Flow:
  assumes cap: "∀e. 0 ≤ f e ∧ f e ≤ c e"
  assumes cons: "∀v ∈ V - {s, t}. 
    (∑e ∈ incoming v. f e) = (∑e ∈ outgoing v. f e)"
  shows "Flow c s t f"  
  using assms by unfold_locales auto  
  
context Finite_Preflow 
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 Preflow›   

subsubsection ‹Networks›  
context Network
begin
  
lemmas [simp] = no_incoming_s no_outgoing_t
  
lemma incoming_s_empty[simp]: "incoming s = {}"
  unfolding incoming_def using no_incoming_s by auto
  
lemma outgoing_t_empty[simp]: "outgoing t = {}"
  unfolding outgoing_def using no_outgoing_t 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)
    
lemma card_V_ge2: "card V ≥ 2"
proof -
  have "2 = card {s,t}" by auto
  also have "{s,t} ⊆ V" by auto
  hence "card {s,t} ≤ card V" by (rule_tac card_mono) auto
  finally show ?thesis .   
qed  
    
lemma zero_is_flow: "Flow c s t (λ_. 0)"
  using cap_non_negative by unfold_locales auto  

lemma max_flow_val_unique: 
  "⟦is_max_flow_val fv1; is_max_flow_val fv2⟧ ⟹ fv1=fv2"    
  unfolding is_max_flow_val_def isMaxFlow_def 
  by (auto simp: antisym)
  
end ― ‹Network›

subsubsection ‹Networks with Flow›

context NPreflow 
begin

sublocale Finite_Preflow 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 ‹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

    
lemma excess_non_negative: "∀v∈V-{s,t}. excess f v ≥ 0"
  unfolding excess_def using no_deficient_nodes by auto
  
lemma excess_nodes_only: "excess f v > 0 ⟹ v ∈ V"  
  unfolding excess_def incoming_def outgoing_def V_def 
  using sum.not_neutral_contains_not_neutral by fastforce
  
lemma excess_non_negative': "∀v ∈ V - {s}. excess f v ≥ 0"
proof -
  have "excess f t ≥ 0" unfolding excess_def outgoing_def 
    by (auto simp: capacity_const sum_nonneg)
  thus ?thesis using excess_non_negative by blast
qed 

lemma excess_s_non_pos: "excess f s ≤ 0"
  unfolding excess_def
  by (simp add: capacity_const sum_nonneg)  
    
end ― ‹Network with preflow›

context NFlow begin  
  sublocale Finite_Preflow by unfold_locales
      
  text ‹There is no outflow from the sink in a network. 
    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)
      
end  
  
end ― ‹Theory›