Theory Connectivity

(*
  File: Connectivity.thy
  Author: Bohua Zhan
*)

section ‹Connectedness for a set of undirected edges.›

theory Connectivity
  imports Union_Find
begin

text ‹A simple application of union-find for graph connectivity.›

fun is_path :: "nat ⇒ (nat × nat) set ⇒ nat list ⇒ bool" where
  "is_path n S [] = False"
| "is_path n S (x # xs) =
   (if xs = [] then x < n else ((x, hd xs) ∈ S ∨ (hd xs, x) ∈ S) ∧ is_path n S xs)"
setup ‹fold add_rewrite_rule @{thms is_path.simps}›

definition has_path :: "nat ⇒ (nat × nat) set ⇒ nat ⇒ nat ⇒ bool" where [rewrite]:
  "has_path n S i j ⟷ (∃p. is_path n S p ∧ hd p = i ∧ last p = j)"

lemma is_path_nonempty [forward]: "is_path n S p ⟹ p ≠ []" by auto2
lemma nonempty_is_not_path [resolve]: "¬is_path n S []" by auto2

lemma is_path_extend [forward]:
  "is_path n S p ⟹ S ⊆ T ⟹ is_path n T p"
@proof @induct p @qed

lemma has_path_extend [forward]:
  "has_path n S i j ⟹ S ⊆ T ⟹ has_path n T i j" by auto2

definition joinable :: "nat list ⇒ nat list ⇒ bool" where [rewrite]:
  "joinable p q ⟷ (last p = hd q)"

definition path_join :: "nat list ⇒ nat list ⇒ nat list" where [rewrite]:
  "path_join p q = p @ tl q"
setup ‹register_wellform_data ("path_join p q", ["joinable p q"])›
setup ‹add_prfstep_check_req ("path_join p q", "joinable p q")›

lemma path_join_hd [rewrite]: "p ≠ [] ⟹ hd (path_join p q) = hd p" by auto2

lemma path_join_last [rewrite]: "joinable p q ⟹ q ≠ [] ⟹ last (path_join p q) = last q"
@proof @have "q = hd q # tl q" @case "tl q = []" @qed

lemma path_join_is_path [backward]:
  "joinable p q ⟹ is_path n S p ⟹ is_path n S q ⟹ is_path n S (path_join p q)"
@proof @induct p @qed

lemma has_path_trans [forward]:
  "has_path n S i j ⟹ has_path n S j k ⟹ has_path n S i k"
@proof
  @obtain p where "is_path n S p" "hd p = i" "last p = j"
  @obtain q where "is_path n S q" "hd q = j" "last q = k"
  @have "is_path n S (path_join p q)"
@qed

definition is_valid_graph :: "nat ⇒ (nat × nat) set ⇒ bool" where [rewrite]:
  "is_valid_graph n S ⟷ (∀p∈S. fst p < n ∧ snd p < n)"

lemma has_path_single1 [backward1]:
  "is_valid_graph n S ⟹ (a, b) ∈ S ⟹ has_path n S a b"
@proof @have "is_path n S [a, b]" @qed

lemma has_path_single2 [backward1]:
  "is_valid_graph n S ⟹ (a, b) ∈ S ⟹ has_path n S b a"
@proof @have "is_path n S [b, a]" @qed

lemma has_path_refl [backward2]:
  "is_valid_graph n S ⟹ a < n ⟹ has_path n S a a"
@proof @have "is_path n S [a]" @qed

definition connected_rel :: "nat ⇒ (nat × nat) set ⇒ (nat × nat) set" where
  "connected_rel n S = {(a,b). has_path n S a b}"

lemma connected_rel_iff [rewrite]:
  "(a, b) ∈ connected_rel n S ⟷ has_path n S a b" using connected_rel_def by simp

lemma connected_rel_trans [forward]:
  "trans (connected_rel n S)" by auto2

lemma connected_rel_refl [backward2]:
  "is_valid_graph n S ⟹ a < n ⟹ (a, a) ∈ connected_rel n S" by auto2

lemma is_path_per_union [rewrite]:
  "is_valid_graph n (S ∪ {(a, b)}) ⟹
   has_path n (S ∪ {(a, b)}) i j ⟷ (i, j) ∈ per_union (connected_rel n S) a b"
@proof
  @let "R = connected_rel n S"
  @let "S' = S ∪ {(a, b)}" @have "S ⊆ S'"
  @case "(i, j) ∈ per_union R a b" @with
    @case "(i, a) ∈ R ∧ (b, j) ∈ R" @with
      @have "has_path n S' i a" @have "has_path n S' a b" @have "has_path n S' b j"
    @end
    @case "(i, b) ∈ R ∧ (a, j) ∈ R" @with
      @have "has_path n S' i b" @have "has_path n S' b a" @have "has_path n S' a j"
    @end
  @end
  @case "has_path n S' i j" @with
    @have (@rule) "∀p. is_path n S' p ⟶ (hd p, last p) ∈ per_union R a b" @with
      @induct p @with
      @subgoal "p = x # xs" @case "xs = []"
        @have "(x, hd xs) ∈ per_union R a b" @with
          @have "is_valid_graph n S"
          @case "(x, hd xs) ∈ S'" @with @case "(x, hd xs) ∈ S" @end
          @case "(hd xs, x) ∈ S'" @with @case "(hd xs, x) ∈ S" @end
        @end
      @endgoal @end
    @end
    @obtain p where "is_path n S' p" "hd p = i" "last p = j"
  @end
@qed

lemma connected_rel_union [rewrite]:
  "is_valid_graph n (S ∪ {(a, b)}) ⟹
   connected_rel n (S ∪ {(a, b)}) = per_union (connected_rel n S) a b" by auto2

lemma connected_rel_init [rewrite]:
  "connected_rel n {} = uf_init_rel n"
@proof
  @have "is_valid_graph n {}"
  @have "∀i j. has_path n {} i j ⟷ (i, j) ∈ uf_init_rel n" @with
    @case "has_path n {} i j" @with
      @obtain p where "is_path n {} p" "hd p = i" "last p = j"
      @have "p = hd p # tl p"
    @end
  @end
@qed

fun connected_rel_ind :: "nat ⇒ (nat × nat) list ⇒ nat ⇒ (nat × nat) set" where
  "connected_rel_ind n es 0 = uf_init_rel n"
| "connected_rel_ind n es (Suc k) =
   (let R = connected_rel_ind n es k; p = es ! k in
      per_union R (fst p) (snd p))"
setup ‹fold add_rewrite_rule @{thms connected_rel_ind.simps}›

lemma connected_rel_ind_rule [rewrite]:
  "is_valid_graph n (set es) ⟹ k ≤ length es ⟹
   connected_rel_ind n es k = connected_rel n (set (take k es))"
@proof @induct k @with
  @subgoal "k = Suc m"
    @have "is_valid_graph n (set (take (Suc m) es))"
  @endgoal @end
@qed

text ‹Correctness of the functional algorithm.›
theorem connected_rel_ind_compute [rewrite]:
  "is_valid_graph n (set es) ⟹
   connected_rel_ind n es (length es) = connected_rel n (set es)" by auto2

end