Theory UnionFind_Impl

theory UnionFind_Impl
imports  "../../Refine_Imperative_HOL/Sepref" UnionFind  
begin

section "Union find Implementation"

subsection "MOP interface"

context
  fixes t ::  "nat ⇒ nat"
begin

  definition "mop_per_init n = SPECT [ per_init' n ↦ enat (t n) ]"

  lemma progress_mop_per_init[progress_rules]: "t n > 0 ⟹ progress (mop_per_init n)"
    unfolding mop_per_init_def by (auto intro!: progress_rules simp add:   zero_enat_def) 

  lemma mop_per_init: "tt ≤ lst (SPECT [ per_init' n ↦ t n]) Q ⟹ tt
           ≤ lst (mop_per_init n) Q" unfolding mop_per_init_def by simp

  sepref_register "mop_per_init" 
end

context
  fixes t ::  "('a × 'a) set ⇒ nat"
begin

  definition "mop_per_compare R a b = SPECT [ per_compare R a b ↦ enat (t R) ]"

  sepref_register "mop_per_compare" 
end

context
  fixes t ::  "('a × 'a) set ⇒ nat"
begin

  definition "mop_per_union R a b = SPECT [ per_union R a b ↦ enat (t R) ]"

  sepref_register "mop_per_union" 
end



subsection "Implementation Locale"


type_synonym uf = "nat array × nat array"

locale UnionFind_Impl = 
  fixes is_uf :: "(nat×nat) set ⇒ uf ⇒ assn"
      and uf_init :: "nat ⇒ uf Heap"
      and uf_init_time :: "nat ⇒ nat"
      and uf_cmp :: "uf ⇒ nat ⇒ nat ⇒ bool Heap"
      and uf_cmp_time :: "nat ⇒ nat"
      and uf_union :: "uf ⇒ nat ⇒ nat ⇒ uf Heap"
      and uf_union_time :: "nat ⇒ nat"
    assumes 
per_init'_sepref_rule[sepref_fr_rules]:  "⋀t x' x. uf_init_time x' ≤ t x' ⟹
     hn_refine (hn_ctxt nat_assn x' x) (uf_init x)
         (hn_ctxt nat_assn x' x)  
             is_uf (PR_CONST (mop_per_init t) $  x' )" 

  and

per_compare_sepref_rule[sepref_fr_rules]:  "⋀t R' R a' a b' b . uf_cmp_time (card (Domain R')) ≤ t R' ⟹
     hn_refine (hn_ctxt is_uf R' R * hn_ctxt nat_assn a' a * hn_ctxt nat_assn b' b) (uf_cmp R a b)
         (hn_ctxt is_uf R' R * hn_ctxt nat_assn a' a * hn_ctxt nat_assn b' b) 
             bool_assn (PR_CONST (mop_per_compare t) $  R' $ a' $ b' )" 

  and

per_union_sepref_rule[sepref_fr_rules]:  "⋀t R' R a' a b' b . a' ∈ Domain R' ⟹ b' ∈ Domain R'
  ⟹ uf_union_time (card (Domain R')) ≤ t R' ⟹ 
     hn_refine (hn_ctxt is_uf R' R * hn_ctxt nat_assn a' a * hn_ctxt nat_assn b' b) (uf_union R a b)
         (hn_invalid is_uf R' R * hn_ctxt nat_assn a' a * hn_ctxt nat_assn b' b) 
             is_uf (PR_CONST (mop_per_union t) $  R' $ a' $ b' )" 

begin


thm per_init'_sepref_rule[to_hfref]
thm per_compare_sepref_rule[to_hfref]
thm per_union_sepref_rule[to_hfref]


end



end