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. v0xsv1  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
    fix xs assume "v0 xs v1"
    show "set xs  insert v S  {}" proof (cases)
      assume "v  set xs"
      then have "v0 xsremove_vertex vv1"
        using remove_vertex_path_from_to v0 xs v1 assms(3) by blast
      then show ?thesis by (simp add: G.S_separates)
    qed simp

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. v0xsv1  set xs  S = {}"
  by (meson assms Separation.intro Separation_axioms.intro v0_v1_Digraph_axioms)