Theory Kruskal_Refine

section ‹Refine Kruskal›

theory Kruskal_Refine
imports Kruskal SeprefUF
begin
 
subsection ‹Refinement I: cycle check by connectedness›

text ‹As a first refinement step, the check for introduction of a cycle when adding an edge @{term e}
  can be replaced by checking whether the edge's endpoints are already connected. 
  By this we can shift from an edge-centric perspective to a vertex-centric perspective.›

context Kruskal_interface
begin

abbreviation "empty_forest ≡ {}"

abbreviation "a_endpoints e ≡ SPEC (λ(a,b). joins a b e )"

definition kruskal0 
  where "kruskal0 ≡ do {
    l ← obtain_sorted_carrier;
    spanning_forest ← nfoldli l (λ_. True)
        (λe T. do { 
            ASSERT (e ∈ E);      
            (a,b) ← a_endpoints e;
            ASSERT (joins a b e ∧ forest T ∧ e∈E ∧ T ⊆ E);
            if ¬ (a,b) ∈ connected T then
              do { 
                ASSERT (e∉T);
                RETURN (insert e T)
              }
            else 
              RETURN T
        }) empty_forest;
        RETURN spanning_forest
      }"
 

lemma if_subst: "(if indep (insert e T) then
              RETURN (insert e T)
            else 
              RETURN T)
        = (if e∉ T ∧ indep (insert e T) then
              RETURN (insert e T)
            else 
              RETURN T)"
  by auto

lemma kruskal0_refine: "(kruskal0, minWeightBasis) ∈ ⟨Id⟩nres_rel"
  unfolding kruskal0_def minWeightBasis_def 
  apply(subst if_subst)
  apply refine_vcg
            apply refine_dref_type 
            apply (all ‹(auto; fail)?›)
  apply clarsimp
  apply (auto simp: augment_forest)
    using augment_forest joins_connected by blast+


subsection ‹Refinement II: connectedness by PER operation›

text ‹Connectedness in the subgraph spanned by a set of edges is a partial equivalence relation and
  can be represented in a disjoint sets. This data structure is maintained while executing Kruskal's
  algorithm and can be used to efficiently check for connectedness (@{term per_compare}.›


definition corresponding_union_find :: "'a per ⇒ 'edge set ⇒ bool" where
  "corresponding_union_find uf T ≡ (∀a∈V. ∀b∈V. per_compare uf a b ⟷ ((a,b)∈ connected T ))"

definition "uf_graph_invar uf_T
   ≡ case uf_T of (uf, T) ⇒ corresponding_union_find uf T ∧ Domain uf = V"

lemma uf_graph_invarD: "uf_graph_invar (uf, T) ⟹ corresponding_union_find uf T"
  unfolding uf_graph_invar_def by simp

definition "uf_graph_rel ≡ br snd uf_graph_invar"

lemma uf_graph_relsndD: "((a,b),c) ∈ uf_graph_rel ⟹ b=c"
  by(auto simp: uf_graph_rel_def in_br_conv)   

lemma uf_graph_relD: "((a,b),c) ∈ uf_graph_rel ⟹ b=c ∧ uf_graph_invar (a,b)"
  by(auto simp: uf_graph_rel_def in_br_conv)      

definition kruskal1
  where "kruskal1 ≡ do {
    l ← obtain_sorted_carrier;
    let initial_union_find = per_init V;
    (per, spanning_forest) ← nfoldli l (λ_. True)
        (λe (uf, T). do { 
            ASSERT (e ∈ E);
            (a,b) ← a_endpoints e;
            ASSERT (a∈V ∧ b∈V ∧ a ∈ Domain uf ∧ b ∈ Domain uf ∧ T⊆E);
            if ¬ per_compare uf a b then
              do { 
                let uf = per_union uf a b;
                ASSERT (e∉T);
                RETURN (uf, insert e T)
              }
            else 
              RETURN (uf,T)
        }) (initial_union_find, empty_forest);
        RETURN spanning_forest
      }"


lemma corresponding_union_find_empty:
  shows "corresponding_union_find (per_init V) empty_forest"
  by(auto simp: corresponding_union_find_def connected_same per_init_def) 
   

lemma empty_forest_refine: "((per_init V, empty_forest), empty_forest)∈uf_graph_rel"
  using corresponding_union_find_empty
  unfolding  uf_graph_rel_def uf_graph_invar_def 
  by (auto simp: in_br_conv per_init_def)

lemma uf_graph_invar_preserve: 
  assumes "uf_graph_invar (uf, T)" "a∈V" "b∈V"
       "joins a b e" "e∈E" "T⊆E"
  shows "uf_graph_invar (per_union uf a b, insert e T)"
  using assms
  by(auto simp add: uf_graph_invar_def corresponding_union_find_def
                  insert_reachable per_union_def)    

theorem kruskal1_refine: "(kruskal1, kruskal0)∈⟨Id⟩nres_rel"
  unfolding kruskal1_def kruskal0_def Let_def 
  apply (refine_rcg empty_forest_refine)
               apply refine_dref_type 
               apply (auto dest: uf_graph_relD E_inV uf_graph_invarD
      simp: corresponding_union_find_def uf_graph_rel_def
      simp: in_br_conv uf_graph_invar_preserve)  
  by (auto simp: uf_graph_invar_def dest: joins_in_V)  

end
      
end