# Theory Separations

theory Separations
imports Helpers Graph
```section ‹Separations›

theory Separations imports Helpers Graph begin

locale Separation = v0_v1_Digraph +
fixes S :: "'a set"
assumes S_V: "S ⊆ V"
and v0_notin_S: "v0 ∉ S"
and v1_notin_S: "v1 ∉ S"
and S_separates: "⋀xs. v0↝xs↝v1 ⟹ set xs ∩ S ≠ {}"

lemma (in Separation) finite_S [simp]: "finite S" using S_V finite_subset finite_vertex_set by auto

lemma (in v0_v1_Digraph) subgraph_separation_extend:
assumes "v ≠ v0" "v ≠ v1" "v ∈ V"
and "Separation (remove_vertex v) v0 v1 S"
shows "Separation G v0 v1 (insert v S)"
proof (rule Separation.intro)
interpret G: Separation "remove_vertex v" v0 v1 S using assms(4) .
show "v0_v1_Digraph G v0 v1" using v0_v1_Digraph_axioms .
show "Separation_axioms G v0 v1 (insert v S)" proof
show "insert v S ⊆ V" by (meson G.S_V assms(3) insert_subsetI remove_vertex_V' subset_trans)
show "v0 ∉ insert v S" using G.v0_notin_S assms(1) by blast
show "v1 ∉ insert v S" using G.v1_notin_S assms(2) by blast
next
fix xs assume "v0 ↝xs↝ v1"
show "set xs ∩ insert v S ≠ {}" proof (cases)
assume "v ∉ set xs"
then have "v0 ↝xs↝⇘remove_vertex v⇙ v1"
using remove_vertex_path_from_to ‹v0 ↝xs↝ v1› assms(3) by blast
then show ?thesis by (simp add: G.S_separates)
qed simp
qed
qed

lemma (in v0_v1_Digraph) subgraph_separation_min_size:
assumes "v ≠ v0" "v ≠ v1" "v ∈ V"
and no_small_separation: "⋀S. Separation G v0 v1 S ⟹ card S ≥ Suc n"
and "Separation (remove_vertex v) v0 v1 S"
shows "card S ≥ n"
using subgraph_separation_extend
by (metis Separation.finite_S Suc_leD assms card_insert_disjoint insert_absorb not_less_eq_eq)

lemma (in v0_v1_Digraph) path_exists_if_no_separation:
assumes "S ⊆ V" "v0 ∉ S" "v1 ∉ S" "¬Separation G v0 v1 S"
shows "∃xs. v0↝xs↝v1 ∧ set xs ∩ S = {}"
by (meson assms Separation.intro Separation_axioms.intro v0_v1_Digraph_axioms)

end
```