Theory Union_Find_Impl

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

section ‹Implementation of union find›

theory Union_Find_Impl
  imports SepAuto "../Functional/Union_Find"
begin

text ‹
  Development follows theory Union\_Find in
  \<^cite>‹"Separation_Logic_Imperative_HOL-AFP"› by Lammich and Meis.
›

type_synonym uf = "nat array × nat array"
  
definition is_uf :: "nat ⇒ (nat×nat) set ⇒ uf ⇒ assn" where [rewrite_ent]:
  "is_uf n R u = (∃⇩Al szl. snd u ↦⇩a l * fst u ↦⇩a szl *
        ↑(ufa_invar l) * ↑(ufa_α l = R) * ↑(length l = n) * ↑(length szl = n))"

definition uf_init :: "nat ⇒ uf Heap" where
  "uf_init n = do {
     l ← Array.of_list [0..<n];
     szl ← Array.new n (1::nat);
     return (szl, l)
   }"

text ‹Correctness of uf\_init.›
theorem uf_init_rule [hoare_triple]:
  "<emp> uf_init n <is_uf n (uf_init_rel n)>" by auto2
  
partial_function (heap) uf_rep_of :: "nat array ⇒ nat ⇒ nat Heap" where
  "uf_rep_of p i = do {
     n ← Array.nth p i;
     if n = i then return i else uf_rep_of p n
   }"
  
lemma uf_rep_of_rule [hoare_triple]:
  "ufa_invar l ⟹ i < length l ⟹
   <p ↦⇩a l>
   uf_rep_of p i
   <λr. p ↦⇩a l * ↑(r = rep_of l i)>"
@proof @prop_induct "ufa_invar l ∧ i < length l" @qed

partial_function (heap) uf_compress :: "nat ⇒ nat ⇒ nat array ⇒ unit Heap" where
  "uf_compress i ci p = (
    if i = ci then return ()
    else do {
      ni ← Array.nth p i;
      uf_compress ni ci p;
      Array.upd i ci p;
      return ()
    })"

lemma uf_compress_rule [hoare_triple]:
  "ufa_invar l ⟹ i < length l ⟹
   <p ↦⇩a l>
    uf_compress i (rep_of l i) p
   <λ_. ∃⇩Al'. p ↦⇩a l' * ↑(ufa_invar l' ∧ length l' = length l ∧
              (∀i<length l. rep_of l' i = rep_of l i))>"
@proof @prop_induct "ufa_invar l ∧ i < length l" @qed

definition uf_rep_of_c :: "nat array ⇒ nat ⇒ nat Heap" where
  "uf_rep_of_c p i = do {
    ci ← uf_rep_of p i;
    uf_compress i ci p;
    return ci
  }"

lemma uf_rep_of_c_rule [hoare_triple]:
  "ufa_invar l ⟹ i < length l ⟹
   <p ↦⇩a l>
   uf_rep_of_c p i
   <λr. ∃⇩Al'. p ↦⇩a l' * ↑(r = rep_of l i ∧ ufa_invar l' ∧ length l' = length l ∧
                          (∀i<length l. rep_of l' i = rep_of l i))>"
  by auto2

definition uf_cmp :: "uf ⇒ nat ⇒ nat ⇒ bool Heap" where
  "uf_cmp u i j = do {
    n ← Array.len (snd u);
    if (i≥n ∨ j≥n) then return False
    else do {
      ci ← uf_rep_of_c (snd u) i;
      cj ← uf_rep_of_c (snd u) j;
      return (ci = cj)
    }
  }"

text ‹Correctness of compare.›
theorem uf_cmp_rule [hoare_triple]:
  "<is_uf n R u>
   uf_cmp u i j
   <λr. is_uf n R u * ↑(r ⟷ (i,j)∈R)>" by auto2

definition uf_union :: "uf ⇒ nat ⇒ nat ⇒ uf Heap" where
  "uf_union u i j = do {
    ci ← uf_rep_of (snd u) i;
    cj ← uf_rep_of (snd u) j;
    if (ci = cj) then return u
    else do {
      si ← Array.nth (fst u) ci;
      sj ← Array.nth (fst u) cj;
      if si < sj then do {
        Array.upd ci cj (snd u);
        Array.upd cj (si+sj) (fst u);
        return u
      } else do { 
        Array.upd cj ci (snd u);
        Array.upd ci (si+sj) (fst u);
        return u
      }
    }
  }"

text ‹Correctness of union.›
theorem uf_union_rule [hoare_triple]:
  "i < n ⟹ j < n ⟹
   <is_uf n R u>
   uf_union u i j
   <is_uf n (per_union R i j)>" by auto2

setup ‹del_prfstep_thm @{thm is_uf_def}›

end