Theory MFMC_Network

theory MFMC_Network imports
  MFMC_Misc
begin

section ‹Graphs›

type_synonym 'v edge = "'v × 'v"

record 'v graph =
  edge :: "'v ⇒ 'v ⇒ bool"

abbreviation edges :: "('v, 'more) graph_scheme ⇒ 'v edge set" ("❙Eı")
where "❙E⇘G⇙ ≡ {(x, y). edge G x y}"

definition outgoing :: "('v, 'more) graph_scheme ⇒ 'v ⇒ 'v set" ("❙O❙U❙Tı")
where "❙O❙U❙T⇘G⇙ x = {y. (x, y) ∈ ❙E⇘G⇙}"

definition incoming :: "('v, 'more) graph_scheme ⇒ 'v ⇒ 'v set" ("❙I❙Nı")
where "❙I❙N⇘G⇙ y = {x. (x, y) ∈ ❙E⇘G⇙}"

text ‹
  Vertices are implicitly defined as the endpoints of edges, so we do not allow isolated vertices.
  For the purpose of flows, this does not matter as isolated vertices cannot contribute to a flow.
  The advantage is that we do not need any invariant on graphs that the endpoints of edges are a
  subset of the vertices. Conversely, this design choice makes a few proofs about reductions on webs
  harder, because we have to adjust other sets which are supposed to be part of the vertices.
›

definition vertex :: "('v, 'more) graph_scheme ⇒ 'v ⇒ bool"
where "vertex G x ⟷ Domainp (edge G) x ∨ Rangep (edge G) x"

lemma vertexI:
  shows vertexI1: "edge Γ x y ⟹ vertex Γ x"
  and vertexI2: "edge Γ x y ⟹ vertex Γ y"
by(auto simp add: vertex_def)

abbreviation vertices :: "('v, 'more) graph_scheme ⇒ 'v set" ("❙Vı")
where "❙V⇘G⇙ ≡ Collect (vertex G)"

lemma "❙V_def": "❙V⇘G⇙ = fst ` ❙E⇘G⇙ ∪ snd ` ❙E⇘G⇙"
by(auto 4 3 simp add: vertex_def intro: rev_image_eqI prod.expand)

type_synonym 'v path = "'v list"

abbreviation path :: "('v, 'more) graph_scheme ⇒ 'v ⇒ 'v path ⇒ 'v ⇒ bool"
where "path G ≡ rtrancl_path (edge G)"

inductive cycle :: "('v, 'more) graph_scheme ⇒ 'v path ⇒ bool"
  for G
where ― ‹Cycles must not pass through the same node multiple times. Otherwise, the cycle might
  enter a node via two different edges and leave it via just one edge. Thus, the clean-up lemma
  would not hold any more.›
  cycle: "⟦ path G v p v; p ≠ []; distinct p ⟧ ⟹ cycle G p"

inductive_simps cycle_Nil [simp]: "cycle G Nil"

abbreviation cycles :: "('v, 'more) graph_scheme ⇒ 'v path set"
where "cycles G ≡ Collect (cycle G)"

lemma countable_cycles [simp]:
  assumes "countable (❙V⇘G⇙)"
  shows "countable (cycles G)"
proof -
  have "cycles G ⊆ lists ❙V⇘G⇙"
    by(auto elim!: cycle.cases dest: rtrancl_path_Range_end rtrancl_path_Range simp add: vertex_def)
  thus ?thesis by(rule countable_subset)(simp add: assms)
qed

definition cycle_edges :: "'v path ⇒ 'v edge list"
where "cycle_edges p = zip p (rotate1 p)"

lemma cycle_edges_not_Nil: "cycle G p ⟹ cycle_edges p ≠ []"
by(auto simp add: cycle_edges_def cycle.simps neq_Nil_conv zip_Cons1 split: list.split)

lemma distinct_cycle_edges:
  "cycle G p ⟹ distinct (cycle_edges p)"
by(erule cycle.cases)(simp add: cycle_edges_def distinct_zipI2)

lemma cycle_enter_leave_same:
  assumes "cycle G p"
  shows "card (set [(x', y) ← cycle_edges p. x' = x]) = card (set [(x', y) ← cycle_edges p. y = x])"
  (is "?lhs = ?rhs")
using assms
proof cases
  case (cycle v)
  from distinct_cycle_edges[OF assms]
  have "?lhs = length [x' ← map fst (cycle_edges p). x' = x]"
    by(subst distinct_card; simp add: filter_map o_def split_def)
  also have "… = (if x ∈ set p then 1 else 0)" using cycle
    by(auto simp add: cycle_edges_def filter_empty_conv length_filter_conv_card card_eq_1_iff in_set_conv_nth dest: nth_eq_iff_index_eq)
  also have "… = length [y ← map snd (cycle_edges p). y = x]" using cycle
    apply(auto simp add: cycle_edges_def filter_empty_conv Suc_length_conv intro!: exI[where x=x])
    apply(drule split_list_first)
    apply(auto dest: split_list_first simp add: append_eq_Cons_conv rotate1_append filter_empty_conv split: if_split_asm dest: in_set_tlD)
    done
  also have "… = ?rhs" using distinct_cycle_edges[OF assms]
    by(subst distinct_card; simp add: filter_map o_def split_def)
  finally show ?thesis .
qed

lemma cycle_leave_ex_enter:
  assumes "cycle G p" and "(x, y) ∈ set (cycle_edges p)"
  shows "∃z. (z, x) ∈ set (cycle_edges p)"
using assms
by(cases)(auto 4 3 simp add: cycle_edges_def cong: conj_cong split: if_split_asm intro: set_zip_rightI dest: set_zip_leftD)

lemma cycle_edges_edges:
  assumes "cycle G p"
  shows "set (cycle_edges p) ⊆ ❙E⇘G⇙"
proof
  fix x
  assume "x ∈ set (cycle_edges p)"
  then obtain i where x: "x = (p ! i, rotate1 p ! i)" and i: "i < length p"
    by(auto simp add: cycle_edges_def set_zip)
  from assms obtain v where p: "path G v p v" and "p ≠ []" and "distinct p" by cases
  let ?i = "Suc i mod length p"
  have "?i < length p" by (simp add: ‹p ≠ []›)
  note rtrancl_path_nth[OF p this]
  also have "(v # p) ! ?i = p ! i"
  proof(cases "Suc i < length p")
    case True thus ?thesis by simp
  next
    case False
    with i have "Suc i = length p" by simp
    moreover from p ‹p ≠ []› have "last p = v" by(rule rtrancl_path_last)
    ultimately show ?thesis using ‹p ≠ []› by(simp add: last_conv_nth)(metis diff_Suc_Suc diff_zero)
  qed
  also have "p ! ?i = rotate1 p ! i" using i by(simp add: nth_rotate1)
  finally show "x ∈ ❙E⇘G⇙" by(simp add: x)
qed


section ‹Network and Flow›

record 'v network = "'v graph" +
  capacity :: "'v edge ⇒ ennreal"
  source :: "'v"
  sink :: "'v"

type_synonym 'v flow = "'v edge ⇒ ennreal"

inductive_set support_flow :: "'v flow ⇒ 'v edge set"
  for f
where "f e > 0 ⟹ e ∈ support_flow f"

lemma support_flow_conv: "support_flow f = {e. f e > 0}"
by(auto simp add: support_flow.simps)

lemma not_in_support_flowD: "x ∉ support_flow f ⟹ f x = 0"
by(simp add: support_flow_conv)

definition d_OUT :: "'v flow ⇒ 'v ⇒ ennreal"
where "d_OUT g x = (∑⇧+ y. g (x, y))"

definition d_IN :: "'v flow ⇒ 'v ⇒ ennreal"
where "d_IN g y = (∑⇧+ x. g (x, y))"

lemma d_OUT_mono: "(⋀y. f (x, y) ≤ g (x, y)) ⟹ d_OUT f x ≤ d_OUT g x"
by(auto simp add: d_OUT_def le_fun_def intro: nn_integral_mono)

lemma d_IN_mono: "(⋀x. f (x, y) ≤ g (x, y)) ⟹ d_IN f y ≤ d_IN g y"
by(auto simp add: d_IN_def le_fun_def intro: nn_integral_mono)

lemma d_OUT_0 [simp]: "d_OUT (λ_. 0) x = 0"
by(simp add: d_OUT_def)

lemma d_IN_0 [simp]: "d_IN (λ_. 0) x = 0"
by(simp add: d_IN_def)

lemma d_OUT_add: "d_OUT (λe. f e + g e) x = d_OUT f x + d_OUT g x"
unfolding d_OUT_def by(simp add: nn_integral_add)

lemma d_IN_add: "d_IN (λe. f e + g e) x = d_IN f x + d_IN g x"
unfolding d_IN_def by(simp add: nn_integral_add)

lemma d_OUT_cmult: "d_OUT (λe. c * f e) x = c * d_OUT f x"
by(simp add: d_OUT_def nn_integral_cmult)

lemma d_IN_cmult: "d_IN (λe. c * f e) x = c * d_IN f x"
by(simp add: d_IN_def nn_integral_cmult)

lemma d_OUT_ge_point: "f (x, y) ≤ d_OUT f x"
by(auto simp add: d_OUT_def intro!: nn_integral_ge_point)

lemma d_IN_ge_point: "f (y, x) ≤ d_IN f x"
by(auto simp add: d_IN_def intro!: nn_integral_ge_point)

lemma d_OUT_monotone_convergence_SUP:
  assumes "incseq (λn y. f n (x, y))"
  shows "d_OUT (λe. SUP n. f n e) x = (SUP n. d_OUT (f n) x)"
unfolding d_OUT_def by(rule nn_integral_monotone_convergence_SUP[OF assms]) simp

lemma d_IN_monotone_convergence_SUP:
  assumes "incseq (λn x. f n (x, y))"
  shows "d_IN (λe. SUP n. f n e) y = (SUP n. d_IN (f n) y)"
unfolding d_IN_def by(rule nn_integral_monotone_convergence_SUP[OF assms]) simp

lemma d_OUT_diff:
  assumes "⋀y. g (x, y) ≤ f (x, y)" "d_OUT g x ≠ ⊤"
  shows "d_OUT (λe. f e - g e) x = d_OUT f x - d_OUT g x"
using assms by(simp add: nn_integral_diff d_OUT_def)

lemma d_IN_diff:
  assumes "⋀x. g (x, y) ≤ f (x, y)" "d_IN g y ≠ ⊤"
  shows "d_IN (λe. f e - g e) y = d_IN f y - d_IN g y"
using assms by(simp add: nn_integral_diff d_IN_def)

lemma fixes G (structure)
  shows d_OUT_alt_def: "(⋀y. (x, y) ∉ ❙E ⟹ g (x, y) = 0) ⟹ d_OUT g x = (∑⇧+  y∈❙O❙U❙T x. g (x, y))"
  and d_IN_alt_def: "(⋀x. (x, y) ∉ ❙E ⟹ g (x, y) = 0) ⟹ d_IN g y = (∑⇧+ x∈❙I❙N y. g (x, y))"
unfolding d_OUT_def d_IN_def
by(fastforce simp add: max_def d_OUT_def d_IN_def nn_integral_count_space_indicator outgoing_def incoming_def intro!: nn_integral_cong split: split_indicator)+

lemma d_OUT_alt_def2: "d_OUT g x = (∑⇧+ y∈{y. (x, y) ∈ support_flow g}. g (x, y))"
  and d_IN_alt_def2: "d_IN g y = (∑⇧+ x∈{x. (x, y) ∈ support_flow g}. g (x, y))"
unfolding d_OUT_def d_IN_def
by(auto simp add: max_def d_OUT_def d_IN_def nn_integral_count_space_indicator outgoing_def incoming_def support_flow.simps intro!: nn_integral_cong split: split_indicator)+

definition d_diff :: "('v edge ⇒ ennreal) ⇒ 'v ⇒ ennreal"
where "d_diff g x = d_OUT g x - d_IN g x"

abbreviation KIR :: "('v edge ⇒ ennreal) ⇒ 'v ⇒ bool"
where "KIR f x ≡ d_OUT f x = d_IN f x"

inductive_set SINK :: "('v edge ⇒ ennreal) ⇒ 'v set"
  for f
where SINK: "d_OUT f x = 0 ⟹ x ∈ SINK f"

lemma SINK_mono:
  assumes "⋀e. f e ≤ g e"
  shows "SINK g ⊆ SINK f"
proof(rule subsetI; erule SINK.cases; hypsubst)
  fix x
  assume "d_OUT g x = 0"
  moreover have "d_OUT f x ≤ d_OUT g x" using assms by(rule d_OUT_mono)
  ultimately have "d_OUT f x = 0" by simp
  thus "x ∈ SINK f" ..
qed

lemma SINK_mono': "f ≤ g ⟹ SINK g ⊆ SINK f"
by(rule SINK_mono)(rule le_funD)

lemma support_flow_Sup: "support_flow (Sup Y) = (⋃f∈Y. support_flow f)"
by(auto simp add: support_flow_conv less_SUP_iff)

lemma
  assumes chain: "Complete_Partial_Order.chain (≤) Y"
  and Y: "Y ≠ {}"
  and countable: "countable (support_flow (Sup Y))"
  shows d_OUT_Sup: "d_OUT (Sup Y) x = (SUP f∈Y. d_OUT f x)" (is "?OUT x" is "?lhs1 x = ?rhs1 x")
  and d_IN_Sup: "d_IN (Sup Y) y = (SUP f∈Y. d_IN f y)" (is "?IN" is "?lhs2 = ?rhs2")
  and SINK_Sup: "SINK (Sup Y) = (⋂f∈Y. SINK f)" (is "?SINK")
proof -
  have chain': "Complete_Partial_Order.chain (≤) ((λf y. f (x, y)) ` Y)" for x using chain
    by(rule chain_imageI)(simp add: le_fun_def)
  have countable': "countable {y. (x, y) ∈ support_flow (Sup Y)}" for x
    using _ countable[THEN countable_image[where f=snd]]
    by(rule countable_subset)(auto intro: prod.expand rev_image_eqI)
  { fix x
    have "?lhs1 x = (∑⇧+ y∈{y. (x, y) ∈ support_flow (Sup Y)}. SUP f∈Y. f (x, y))"
      by(subst d_OUT_alt_def2; simp)
    also have "… = (SUP f∈Y. ∑⇧+ y∈{y. (x, y) ∈ support_flow (Sup Y)}. f (x, y))" using Y
      by(rule nn_integral_monotone_convergence_SUP_countable)(auto simp add: chain' intro: countable')
    also have "… = ?rhs1 x" unfolding d_OUT_alt_def2
      by(auto 4 3 simp add: support_flow_Sup max_def nn_integral_count_space_indicator intro!: nn_integral_cong SUP_cong split: split_indicator dest: not_in_support_flowD)
    finally show "?OUT x" . }
  note out = this

  have chain'': "Complete_Partial_Order.chain (≤) ((λf x. f (x, y)) ` Y)" for y using chain
    by(rule chain_imageI)(simp add: le_fun_def)
  have countable'': "countable {x. (x, y) ∈ support_flow (Sup Y)}" for y
    using _ countable[THEN countable_image[where f=fst]]
    by(rule countable_subset)(auto intro: prod.expand rev_image_eqI)
  have "?lhs2 = (∑⇧+ x∈{x. (x, y) ∈ support_flow (Sup Y)}. SUP f∈Y. f (x, y))"
    by(subst d_IN_alt_def2; simp)
  also have "… = (SUP f∈Y. ∑⇧+ x∈{x. (x, y) ∈ support_flow (Sup Y)}. f (x, y))" using Y
    by(rule nn_integral_monotone_convergence_SUP_countable)(simp_all add: chain'' countable'')
  also have "… = ?rhs2" unfolding d_IN_alt_def2
    by(auto 4 3 simp add: support_flow_Sup max_def nn_integral_count_space_indicator intro!: nn_integral_cong SUP_cong split: split_indicator dest: not_in_support_flowD)
  finally show ?IN .

  show ?SINK by(rule set_eqI)(simp add: SINK.simps out Y bot_ennreal[symmetric])
qed

lemma
  assumes chain: "Complete_Partial_Order.chain (≤) Y"
  and Y: "Y ≠ {}"
  and countable: "countable (support_flow f)"
  and bounded: "⋀g e. g ∈ Y ⟹ g e ≤ f e"
  shows d_OUT_Inf: "d_OUT f x ≠ top ⟹ d_OUT (Inf Y) x = (INF g∈Y. d_OUT g x)" (is "_ ⟹ ?OUT" is "_ ⟹ ?lhs1 = ?rhs1")
  and d_IN_Inf: "d_IN f x ≠ top ⟹ d_IN (Inf Y) x = (INF g∈Y. d_IN g x)" (is "_ ⟹ ?IN" is "_ ⟹ ?lhs2 = ?rhs2")
proof -
  text ‹We take a detour here via suprema because we have more theorems about @{const nn_integral}
    with suprema than with infinma.›

  from Y obtain g0 where g0: "g0 ∈ Y" by auto
  have g0_le_f: "g0 e ≤ f e" for e by(rule bounded[OF g0])

  have "support_flow (SUP g∈Y. (λe. f e - g e)) ⊆ support_flow f"
    by(clarsimp simp add: support_flow.simps less_SUP_iff elim!: less_le_trans intro!: diff_le_self_ennreal)
  then have countable': "countable (support_flow (SUP g∈Y. (λe. f e - g e)))" by(rule countable_subset)(rule countable)

  have "Complete_Partial_Order.chain (≥) Y" using chain by(simp add: chain_dual)
  hence chain': "Complete_Partial_Order.chain (≤) ((λg e. f e - g e) ` Y)"
    by(rule chain_imageI)(auto simp add: le_fun_def intro: ennreal_minus_mono)

  { assume finite: "d_OUT f x ≠ top"
    have finite' [simp]: "f (x, y) ≠ ⊤" for y using finite
      by(rule neq_top_trans) (rule d_OUT_ge_point)

    have finite'_g: "g (x, y) ≠ ⊤" if "g ∈ Y" for g y using finite'[of y]
      by(rule neq_top_trans)(rule bounded[OF that])

    have finite1: "(∑⇧+ y. f (x, y) - (INF g∈Y. g (x, y))) ≠ top"
      using finite by(rule neq_top_trans)(auto simp add: d_OUT_def intro!: nn_integral_mono)
    have finite2: "d_OUT g x ≠ top" if "g ∈ Y" for g using finite
      by(rule neq_top_trans)(auto intro: d_OUT_mono bounded[OF that])

    have bounded1: "(⨅g∈Y. d_OUT g x) ≤ d_OUT f x"
      using Y by (blast intro: INF_lower2 d_OUT_mono bounded)

    have "?lhs1 = (∑⇧+ y. INF g∈Y. g (x, y))" by(simp add: d_OUT_def)
    also have "… = d_OUT f x - (∑⇧+ y. f (x, y) - (INF g∈Y. g (x, y)))" unfolding d_OUT_def
      using finite1 g0_le_f
      apply(subst nn_integral_diff[symmetric])
      apply(auto simp add: AE_count_space intro!: diff_le_self_ennreal INF_lower2[OF g0] nn_integral_cong diff_diff_ennreal[symmetric])
      done
    also have "(∑⇧+ y. f (x, y) - (INF g∈Y. g (x, y))) = d_OUT (λe. SUP g∈Y. f e - g e) x"
      unfolding d_OUT_def by(subst SUP_const_minus_ennreal)(simp_all add: Y)
    also have "… = (SUP h∈(λg e. f e - g e) ` Y. d_OUT h x)" using countable' chain' Y
      by(subst d_OUT_Sup[symmetric])(simp_all add: SUP_apply[abs_def])
    also have "… = (SUP g∈Y. d_OUT (λe. f e - g e) x)" unfolding image_image ..
    also have "… = (SUP g∈Y. d_OUT f x - d_OUT g x)"
      by(rule SUP_cong[OF refl] d_OUT_diff)+(auto intro: bounded simp add: finite2)
    also have "… = d_OUT f x - ?rhs1" by(subst SUP_const_minus_ennreal)(simp_all add: Y)
    also have "d_OUT f x - … = ?rhs1"
      using Y by(subst diff_diff_ennreal)(simp_all add: bounded1 finite)
    finally show ?OUT .
  next
    assume finite: "d_IN f x ≠ top"
    have finite' [simp]: "f (y, x) ≠ ⊤" for y using finite
      by(rule neq_top_trans) (rule d_IN_ge_point)

    have finite'_g: "g (y, x) ≠ ⊤" if "g ∈ Y" for g y using finite'[of y]
      by(rule neq_top_trans)(rule bounded[OF that])

    have finite1: "(∑⇧+ y. f (y, x) - (INF g∈Y. g (y, x))) ≠ top"
      using finite by(rule neq_top_trans)(auto simp add: d_IN_def diff_le_self_ennreal intro!: nn_integral_mono)
    have finite2: "d_IN g x ≠ top" if "g ∈ Y" for g using finite
      by(rule neq_top_trans)(auto intro: d_IN_mono bounded[OF that])

    have bounded1: "(⨅g∈Y. d_IN g x) ≤ d_IN f x"
      using Y by (blast intro: INF_lower2 d_IN_mono bounded)

    have "?lhs2 = (∑⇧+ y. INF g∈Y. g (y, x))" by(simp add: d_IN_def)
    also have "… = d_IN f x - (∑⇧+ y. f (y, x) - (INF g∈Y. g (y, x)))" unfolding d_IN_def
      using finite1 g0_le_f
      apply(subst nn_integral_diff[symmetric])
      apply(auto simp add: AE_count_space intro!: diff_le_self_ennreal INF_lower2[OF g0] nn_integral_cong diff_diff_ennreal[symmetric])
      done
    also have "(∑⇧+ y. f (y, x) - (INF g∈Y. g (y, x))) = d_IN (λe. SUP g∈Y. f e - g e) x"
      unfolding d_IN_def by(subst SUP_const_minus_ennreal)(simp_all add: Y)
    also have "… = (SUP h∈(λg e. f e - g e) ` Y. d_IN h x)" using countable' chain' Y
      by(subst d_IN_Sup[symmetric])(simp_all add: SUP_apply[abs_def])
    also have "… = (SUP g∈Y. d_IN (λe. f e - g e) x)" unfolding image_image ..
    also have "… = (SUP g∈Y. d_IN f x - d_IN g x)"
      by(rule SUP_cong[OF refl] d_IN_diff)+(auto intro: bounded simp add: finite2)
    also have "… = d_IN f x - ?rhs2" by(subst SUP_const_minus_ennreal)(simp_all add: Y)
    also have "d_IN f x - … = ?rhs2"
      by(subst diff_diff_ennreal)(simp_all add: finite bounded1)
    finally show ?IN . }
qed

inductive flow :: "('v, 'more) network_scheme ⇒ 'v flow ⇒ bool"
  for Δ (structure) and f
where
  flow: "⟦ ⋀e. f e ≤ capacity Δ e;
     ⋀x. ⟦ x ≠ source Δ; x ≠ sink Δ ⟧ ⟹ KIR f x ⟧
  ⟹ flow Δ f"

lemma flowD_capacity: "flow Δ f ⟹ f e ≤ capacity Δ e"
by(cases e)(simp add: flow.simps)

lemma flowD_KIR: "⟦ flow Δ f; x ≠ source Δ; x ≠ sink Δ ⟧ ⟹ KIR f x"
by(simp add: flow.simps)

lemma flowD_capacity_OUT: "flow Δ f ⟹ d_OUT f x ≤ d_OUT (capacity Δ) x"
by(rule d_OUT_mono)(erule flowD_capacity)

lemma flowD_capacity_IN: "flow Δ f ⟹ d_IN f x ≤ d_IN (capacity Δ) x"
by(rule d_IN_mono)(erule flowD_capacity)

abbreviation value_flow :: "('v, 'more) network_scheme ⇒ ('v edge ⇒ ennreal) ⇒ ennreal"
where "value_flow Δ f ≡ d_OUT f (source Δ)"

subsection ‹Cut›

type_synonym 'v cut = "'v set"

inductive cut :: "('v, 'more) network_scheme ⇒ 'v cut ⇒ bool"
  for Δ and S
where cut: "⟦ source Δ ∈ S; sink Δ ∉ S ⟧ ⟹ cut Δ S"

inductive orthogonal :: "('v, 'more) network_scheme ⇒ 'v flow ⇒ 'v cut ⇒ bool"
  for Δ f S
where
  "⟦ ⋀x y. ⟦ edge Δ x y; x ∈ S; y ∉ S ⟧ ⟹ f (x, y) = capacity Δ (x, y);
     ⋀x y. ⟦ edge Δ x y; x ∉ S; y ∈ S ⟧ ⟹ f (x, y) = 0 ⟧
  ⟹ orthogonal Δ f S"

lemma orthogonalD_out:
  "⟦ orthogonal Δ f S; edge Δ x y; x ∈ S; y ∉ S ⟧ ⟹ f (x, y) = capacity Δ (x, y)"
by(simp add: orthogonal.simps)

lemma orthogonalD_in:
  "⟦ orthogonal Δ f S; edge Δ x y; x ∉ S; y ∈ S ⟧ ⟹ f (x, y) = 0"
by(simp add: orthogonal.simps)



subsection ‹Countable network›

locale countable_network =
  fixes Δ :: "('v, 'more) network_scheme" (structure)
  assumes countable_E [simp]: "countable ❙E"
  and source_neq_sink [simp]: "source Δ ≠ sink Δ"
  and capacity_outside: "e ∉ ❙E ⟹ capacity Δ e = 0"
  and capacity_finite [simp]: "capacity Δ e ≠ ⊤"
begin

lemma sink_neq_source [simp]: "sink Δ ≠ source Δ"
using source_neq_sink[symmetric] .

lemma countable_V [simp]: "countable ❙V"
unfolding "❙V_def" using countable_E by auto

lemma flowD_outside:
  assumes g: "flow Δ g"
  shows "e ∉ ❙E ⟹ g e = 0"
using flowD_capacity[OF g, of e] capacity_outside[of e] by simp

lemma flowD_finite:
  assumes "flow Δ g"
  shows "g e ≠ ⊤"
using flowD_capacity[OF assms, of e] by (auto simp: top_unique)

lemma zero_flow [simp]: "flow Δ (λ_. 0)"
by(rule flow.intros) simp_all

end

subsection ‹Reduction for avoiding antiparallel edges›

locale antiparallel_edges = countable_network Δ
  for Δ :: "('v, 'more) network_scheme" (structure)
begin

text ‹We eliminate the assumption of antiparallel edges by adding a vertex for every edge.
  Thus, antiparallel edges are split up into a cycle of 4 edges. This idea already appears in
  \<^cite>‹Aharoni1983EJC›.›

datatype (plugins del: transfer size) 'v' vertex = Vertex 'v' | Edge 'v' 'v'

inductive edg :: "'v vertex ⇒ 'v vertex ⇒ bool"
where
  OUT: "edge Δ x y ⟹ edg (Vertex x) (Edge x y)"
| IN: "edge Δ x y ⟹ edg (Edge x y) (Vertex y)"

inductive_simps edg_simps [simp]:
  "edg (Vertex x) v"
  "edg (Edge x y) v"
  "edg v (Vertex x)"
  "edg v (Edge x y)"

fun split :: "'v flow ⇒ 'v vertex flow"
where
  "split f (Vertex x, Edge x' y) = (if x' = x then f (x, y) else 0)"
| "split f (Edge x y', Vertex y) = (if y' = y then f (x, y) else 0)"
| "split f _ = 0"

lemma split_Vertex1_eq_0I: "(⋀z. y ≠ Edge x z) ⟹ split f (Vertex x, y) = 0"
by(cases y) auto

lemma split_Vertex2_eq_0I: "(⋀z. y ≠ Edge z x) ⟹ split f (y, Vertex x) = 0"
by(cases y) simp_all

lemma split_Edge1_eq_0I: "(⋀z. y ≠ Vertex x) ⟹ split f (Edge z x, y) = 0"
by(cases y) simp_all

lemma split_Edge2_eq_0I: "(⋀z. y ≠ Vertex x) ⟹ split f (y, Edge x z) = 0"
by(cases y) simp_all

definition Δ'' :: "'v vertex network"
where "Δ'' = ⦇edge = edg, capacity = split (capacity Δ), source = Vertex (source Δ), sink = Vertex (sink Δ)⦈"

lemma Δ''_sel [simp]:
  "edge Δ'' = edg"
  "capacity Δ'' = split (capacity Δ)"
  "source Δ'' = Vertex (source Δ)"
  "sink Δ'' = Vertex (sink Δ)"
by(simp_all add: Δ''_def)

lemma "❙E_Δ''": "❙E⇘Δ''⇙ = (λ(x, y). (Vertex x, Edge x y)) ` ❙E ∪ (λ(x, y). (Edge x y, Vertex y)) ` ❙E"
by(auto elim: edg.cases)

lemma "❙V_Δ''": "❙V⇘Δ''⇙ = Vertex ` ❙V ∪ case_prod Edge ` ❙E"
by(auto 4 4 simp add: vertex_def elim!: edg.cases)

lemma inj_on_Edge1 [simp]: "inj_on (λx. Edge x y) A"
by(simp add: inj_on_def)

lemma inj_on_Edge2 [simp]: "inj_on (Edge x) A"
by(simp add: inj_on_def)

lemma d_IN_split_Vertex [simp]: "d_IN (split f) (Vertex x) = d_IN f x" (is "?lhs = ?rhs")
proof(rule trans)
  show "?lhs = (∑⇧+ v'∈range (λy. Edge y x). split f (v', Vertex x))"
    by(auto intro!: nn_integral_cong split_Vertex2_eq_0I simp add: d_IN_def nn_integral_count_space_indicator split: split_indicator)
  show "… = ?rhs" by(simp add: nn_integral_count_space_reindex d_IN_def)
qed

lemma d_OUT_split_Vertex [simp]: "d_OUT (split f) (Vertex x) = d_OUT f x" (is "?lhs = ?rhs")
proof(rule trans)
  show "?lhs = (∑⇧+ v'∈range (Edge x). split f (Vertex x, v'))"
    by(auto intro!: nn_integral_cong split_Vertex1_eq_0I simp add: d_OUT_def nn_integral_count_space_indicator split: split_indicator)
  show "… = ?rhs" by(simp add: nn_integral_count_space_reindex d_OUT_def)
qed

lemma d_IN_split_Edge [simp]: "d_IN (split f) (Edge x y) = max 0 (f (x, y))" (is "?lhs = ?rhs")
proof(rule trans)
  show "?lhs = (∑⇧+ v'. split f (v', Edge x y) * indicator {Vertex x} v')"
    unfolding d_IN_def by(rule nn_integral_cong)(simp add: split_Edge2_eq_0I split: split_indicator)
  show "… = ?rhs" by(simp add: max_def)
qed

lemma d_OUT_split_Edge [simp]: "d_OUT (split f) (Edge x y) = max 0 (f (x, y))" (is "?lhs = ?rhs")
proof(rule trans)
  show "?lhs = (∑⇧+ v'. split f (Edge x y, v') * indicator {Vertex y} v')"
    unfolding d_OUT_def by(rule nn_integral_cong)(simp add: split_Edge1_eq_0I split: split_indicator)
  show "… = ?rhs" by(simp add: max_def)
qed

lemma Δ''_countable_network: "countable_network Δ''"
proof
  show "countable ❙E⇘Δ''⇙" unfolding "❙E_Δ''" by(simp)
  show "source Δ'' ≠ sink Δ''" by auto
  show "capacity Δ'' e = 0" if "e ∉ ❙E⇘Δ''⇙" for e using that
    by(cases "(capacity Δ, e)" rule: split.cases)(auto simp add: capacity_outside)
  show "capacity Δ'' e ≠ top" for e by(cases "(capacity Δ, e)" rule: split.cases)(auto)
qed

interpretation Δ'': countable_network Δ'' by(rule Δ''_countable_network)

lemma flow_split [simp]:
  assumes "flow Δ f"
  shows "flow Δ'' (split f)"
proof
  show "split f e ≤ capacity Δ'' e" for e
    by(cases "(f, e)" rule: split.cases)(auto intro: flowD_capacity[OF assms] intro: SUP_upper2 assms)
  show "KIR (split f) x" if "x ≠ source Δ''" "x ≠ sink Δ''" for x
    using that by(cases "x")(auto dest: flowD_KIR[OF assms])
qed

abbreviation (input) collect :: "'v vertex flow ⇒ 'v flow"
where "collect f ≡ (λ(x, y). f (Edge x y, Vertex y))"

lemma d_OUT_collect:
  assumes f: "flow Δ'' f"
  shows "d_OUT (collect f) x = d_OUT f (Vertex x)"
proof -
  have "d_OUT (collect f) x = (∑⇧+ y. f (Edge x y, Vertex y))"
    by(simp add: nn_integral_count_space_reindex d_OUT_def)
  also have "… = (∑⇧+ y∈range (Edge x). f (Vertex x, y))"
  proof(clarsimp simp add: nn_integral_count_space_reindex intro!: nn_integral_cong)
    fix y
    have "(∑⇧+ z. f (Edge x y, z) * indicator {Vertex y} z) = d_OUT f (Edge x y)"
      unfolding d_OUT_def by(rule nn_integral_cong)(simp split: split_indicator add: Δ''.flowD_outside[OF f])
    also have "… = d_IN f (Edge x y)" using f by(rule flowD_KIR) simp_all
    also have "… = (∑⇧+ z. f (z, Edge x y) * indicator {Vertex x} z)"
      unfolding d_IN_def by(rule nn_integral_cong)(simp split: split_indicator add: Δ''.flowD_outside[OF f])
    finally show "f (Edge x y, Vertex y) = f (Vertex x, Edge x y)"
      by(simp add: max_def)
  qed
  also have "… = d_OUT f (Vertex x)"
    by(auto intro!: nn_integral_cong Δ''.flowD_outside[OF f] simp add: nn_integral_count_space_indicator d_OUT_def split: split_indicator)
  finally show ?thesis .
qed

lemma flow_collect [simp]:
  assumes f: "flow Δ'' f"
  shows "flow Δ (collect f)"
proof
  show "collect f e ≤ capacity Δ e" for e using flowD_capacity[OF f, of "(case_prod Edge e, Vertex (snd e))"]
    by(cases e)(simp)

  fix x
  assume x: "x ≠ source Δ" "x ≠ sink Δ"
  have "d_OUT (collect f) x = d_OUT f (Vertex x)" using f by(rule d_OUT_collect)
  also have "… = d_IN f (Vertex x)" using x flowD_KIR[OF f, of "Vertex x"] by(simp)
  also have "… = (∑⇧+ y∈range (λz. Edge z x). f (y, Vertex x))"
    by(auto intro!: nn_integral_cong Δ''.flowD_outside[OF f] simp add: nn_integral_count_space_indicator d_IN_def split: split_indicator)
  also have "… = d_IN (collect f) x" by(simp add: nn_integral_count_space_reindex d_IN_def)
  finally show "KIR (collect f) x" .
qed

lemma value_collect: "flow Δ'' f ⟹ value_flow Δ (collect f) = value_flow Δ'' f"
by(simp add: d_OUT_collect)

end

end