Theory Separations

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