Theory Connectivity_Impl

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

section ‹Implementation of connectivity on graphs›

theory Connectivity_Impl
  imports Union_Find_Impl "../Functional/Connectivity"
begin

text ‹Imperative version of graph-connectivity example.›

subsection ‹Constructing the connected relation›

fun connected_rel_imp :: "nat ⇒ (nat × nat) list ⇒ nat ⇒ uf Heap" where
  "connected_rel_imp n es 0 = do { p ← uf_init n; return p }"
| "connected_rel_imp n es (Suc k) = do {
    p ← connected_rel_imp n es k;
    p' ← uf_union p (fst (es ! k)) (snd (es ! k));
    return p' }"

lemma connected_rel_imp_to_fun [hoare_triple]:
  "is_valid_graph n (set es) ⟹ k ≤ length es ⟹
   <emp>
   connected_rel_imp n es k
   <is_uf n (connected_rel_ind n es k)>"
@proof @induct k @qed

lemma connected_rel_imp_correct [hoare_triple]:
  "is_valid_graph n (set es) ⟹
   <emp>
   connected_rel_imp n es (length es)
   <is_uf n (connected_rel n (set es))>" by auto2

subsection ‹Connectedness tests›

text ‹Correctness of the algorithm for detecting connectivity.›
theorem uf_cmp_correct [hoare_triple]:
  "<is_uf n (connected_rel n S) p>
   uf_cmp p i j
   <λr. is_uf n (connected_rel n S) p * ↑(r ⟷ has_path n S i j)>" by auto2

end