Theory UGraph_Impl

section "Kruskal on UGraphs"

theory UGraph_Impl
imports
 Kruskal_Impl UGraph
begin

definition "α = (λ(u,w,v). Upair u v)"

subsection "Interpreting ‹Kruskl_Impl› with a UGraph"

abbreviation (in uGraph)
  "getEdges_SPEC csuper_E
    ≡ (SPEC (λL. distinct (map α L) ∧ α ` set L = E 
                ∧ (∀(a, wv, b)∈set L. w (α (a, wv, b)) = wv) ∧ set L ⊆ csuper_E))"

locale uGraph_impl = uGraph E w for E :: "nat uprod set" and w :: "nat uprod ⇒ int" +
  fixes getEdges_impl :: "(nat × int × nat) list Heap" and csuper_E :: "(nat × int × nat) set" 
  assumes getEdges_impl:
    "(uncurry0 getEdges_impl, uncurry0 (getEdges_SPEC csuper_E))
       ∈ unit_assn⇧k →⇩a list_assn (nat_assn ×⇩a int_assn ×⇩a nat_assn)"
begin

 

  abbreviation "V ≡ ⋃ (set_uprod ` E)"


  lemma max_node_is_Max_V: " E = α ` set la ⟹  max_node la = Max (insert 0 V)"
  proof -
    assume E: "E = α ` set la"
    have *: "fst ` set la ∪ (snd ∘ snd) ` set la = (⋃x∈set la. case x of (x1, x1a, x2a) ⇒ {x1, x2a})"
      by auto force 
    show ?thesis  
    unfolding E using *
    by (auto simp add: α_def  max_node_def prod.case_distrib) 
  qed




sublocale s: Kruskal_Impl E "⋃(set_uprod ` E)" set_uprod "λu v e. Upair u v = e"
  "subforest" "uconnectedV"  w α "PR_CONST (λ(u,w,v). RETURN (u,v))"
  "PR_CONST (getEdges_SPEC csuper_E)"
 getEdges_impl "csuper_E" " (λ(u,w,v). return (u,v))" 
  unfolding subforest_def
proof (unfold_locales, goal_cases) 
  show "finite E" by simp
next
  fix E'
  assume "forest E' ∧ E' ⊆ E"
  then show "E' ⊆ E" by auto
next
  show "forest {} ∧ {} ⊆ E" apply (auto simp: decycle_def forest_def)
    using epath.elims(2) by fastforce 
next
  fix X Y
  assume "forest X ∧ X ⊆ E" "Y ⊆ X" 
  then show "forest Y ∧ Y ⊆ E" using forest_mono by auto
next
  case (5 u v)
  then show ?case unfolding uconnected_def apply auto 
    using epath.elims(2) by force 
next
  case (6 E1 E2 u v)
  then have "(u, v) ∈ (uconnected E1)" and uv: "u ∈ V" "v ∈ V"
    by auto
  then obtain p where 1: "epath E1 u p v" unfolding uconnected_def by auto 
  from 6 uv have 2: "¬(∃p.  epath E2 u p v)" unfolding uconnected_def by auto
  from 1 2 have "∃a b. (a, b) ∉ uconnected E2
           ∧ Upair a b ∉ E2 ∧ Upair a b ∈ E1" by(rule findaugmenting_edge)
  then show ?case by auto
next
  case (7 F e u v)
  note f = ‹forest F ∧ F ⊆ E›
  note notin = ‹e ∈ E - F› ‹Upair u v = e›
  from notin ecard2 have unv: "u≠v" by fastforce
  show "(forest (insert e F) ∧ insert e F ⊆ E) = ((u, v) ∉ uconnectedV F)"
  proof
    assume a: "forest (insert e F) ∧ insert e F ⊆ E "
    have "(u, v) ∉ uconnected F" apply(rule insert_stays_forest_means_not_connected)
      using notin a unv by auto
    then show "((u, v) ∉ Restr (uconnected F) V)" by auto
  next 
    assume a: "(u, v) ∉ Restr (uconnected F) V"
    have "forest (insert (Upair u v) F)" apply(rule augment_forest_overedges[where E=E])
      using notin f a unv  by auto 
    moreover have "insert e F ⊆ E"
      using notin f by auto
    ultimately show "forest (insert e F) ∧ insert e F ⊆ E" using notin by auto
  qed
next      
  fix F
  assume "F⊆E"
  show "equiv V (uconnectedV F)" by(rule equiv_vert_uconnected)
next                                 
  case (9 F)
  then show ?case  by auto
next
  case (10 x y F)
  then show ?case using insert_uconnectedV_per' by metis
next
  case (11 x)
  then show ?case apply(cases x) by auto
next
  case (12 u v e)
  then show ?case by auto
next
  case (13 u v e)
  then show ?case by auto
next
  case (14 a F e)
  then show ?case using ecard2 by force
next
  case (15 v)
  then show ?case using ecard2 by auto
next
  case 16
  show "V ⊆ V" by auto
next
  case 17
  show "finite V" by simp
next
  case (18 a b e T)
  then show ?case 
    apply auto
    subgoal unfolding uconnected_def apply auto apply(rule exI[where x="[e]"]) apply simp
        using ecard2 by force
    subgoal by force
    subgoal by force 
    done
next
  case (19 xi x)
  then show ?case by (auto split: prod.splits simp: α_def)
next
  case 20
  show ?case by auto
next
  case 21
  show ?case using getEdges_impl by simp
next
  case (22 l)
  from max_node_is_Max_V[OF 22] show "max_node l = Max (insert 0 V)" .
next
  case (23)
  then show ?case
    apply sepref_to_hoare by sep_auto 
qed
 
lemma spanningForest_eq_basis: "spanningForest = s.basis"
  unfolding spanningForest_def  s.basis_def by auto

lemma minSpanningForest_eq_minbasis: "minSpanningForest = s.minBasis"
  unfolding minSpanningForest_def  s.MSF_def spanningForest_eq_basis by auto

lemma kruskal_correct': 
  "<emp> kruskal getEdges_impl (λ(u,w,v). return (u,v)) ()
    <λr. ↑ (distinct r ∧ set r ⊆ csuper_E ∧ s.MSF (set (map α r)))>⇩t"
  using s.kruskal_correct_forest   by auto

lemma kruskal_correct:
  "<emp> kruskal getEdges_impl (λ(u,w,v). return (u,v)) ()
    <λr. ↑ (distinct r ∧ set r ⊆ csuper_E ∧ minSpanningForest (set (map α r)))>⇩t"
  using s.kruskal_correct_forest minSpanningForest_eq_minbasis  by auto

end

subsection "Kruskal on UGraph from list of concrete edges"


definition "uGraph_from_list_α_weight L e = (THE w. ∃a' b'. Upair a' b' = e ∧ (a', w, b') ∈ set L)"
abbreviation "uGraph_from_list_α_edges L ≡ α ` set L"

locale fromlist = fixes
  L :: "(nat × int × nat) list"
assumes dist: "distinct (map α L)" and no_selfloop: "∀u w v. (u,w,v)∈set L ⟶ u≠v"
begin

lemma not_distinct_map: "a∈set l ⟹ b∈set l ⟹ a≠b ⟹ α a = α b ⟹ ¬ distinct (map α l)"
   
  by (meson distinct_map_eq)  

lemma ii: "(a, aa, b) ∈ set L ⟹ uGraph_from_list_α_weight L (Upair a b) = aa"
  unfolding uGraph_from_list_α_weight_def
  apply rule
  subgoal by auto
  apply clarify
  subgoal for w a' b'
    apply(auto) 
    subgoal using distinct_map_eq[OF dist, of "(a, aa, b)" "(a, w, b)"]
      unfolding α_def by auto
    subgoal using distinct_map_eq[OF dist, of "(a, aa, b)" "(a', w, b')"]
      unfolding α_def by fastforce
    done
  done
 
sublocale uGraph_impl "α ` set L" "uGraph_from_list_α_weight L" "return L" "set L" 
proof (unfold_locales)
  fix e assume *: "e ∈ α ` set L"
  from * obtain u w v where "(u,w,v) ∈ set L" "e = α (u, w, v)" by auto
  then show "proper_uprod e" using no_selfloop unfolding α_def by auto
next
  show "finite (α ` set L)" by auto
next
  show "(uncurry0 (return L),uncurry0((SPEC
          (λLa. distinct (map α La) ∧ α ` set La = α ` set L 
      ∧ (∀(aa, wv, ba)∈set La. uGraph_from_list_α_weight L (α (aa, wv, ba)) = wv)
      ∧ set La ⊆ set L))))
    ∈ unit_assn⇧k →⇩a list_assn (nat_assn ×⇩a int_assn ×⇩a nat_assn)"
    apply sepref_to_hoare using dist  apply sep_auto
    subgoal using ii unfolding α_def by auto
    subgoal by simp
    subgoal by (auto simp: pure_fold list_assn_emp)   
    done
qed
  
lemmas kruskal_correct = kruskal_correct

definition (in -) "kruskal_algo L = kruskal (return L) (λ(u,w,v). return (u,v)) ()"

end 

subsection ‹Outside the locale›

definition uGraph_from_list_invar :: "(nat×int×nat) list ⇒ bool" where
  "uGraph_from_list_invar L = (distinct (map α L) ∧ (∀p∈set L. case p of (u,w,v) ⇒u≠v))"

lemma uGraph_from_list_invar_conv: "uGraph_from_list_invar L = fromlist L"
  by(auto simp add: uGraph_from_list_invar_def fromlist_def)

lemma uGraph_from_list_invar_subset: 
  "uGraph_from_list_invar L ⟹ set L'⊆ set L ⟹ distinct L' ⟹ uGraph_from_list_invar L'"
  unfolding uGraph_from_list_invar_def by (auto simp: distinct_map inj_on_subset)  


lemma  uGraph_from_list_α_inj_on: "uGraph_from_list_invar E ⟹ inj_on α (set E)"
  by(auto simp: distinct_map uGraph_from_list_invar_def  )

lemma sum_easier: "uGraph_from_list_invar L 
    ⟹ set E ⊆ set L
    ⟹ sum (uGraph_from_list_α_weight L) (uGraph_from_list_α_edges E) = sum (λ(u,w,v). w) (set E)"
 proof -
  assume a: "uGraph_from_list_invar L"
  assume b: "set E ⊆ set L" 

  have *: "⋀e. e∈set E ⟹
   ((λe. THE w. ∃a' b'. Upair a' b' = e ∧ (a', w, b') ∈ set L) ∘ α) e
       = (case e of (u, w, v) ⇒ w)"
    apply simp
    apply(rule the_equality) 
    subgoal using b by(auto simp: α_def split: prod.splits)   
    subgoal using a b apply(auto simp: uGraph_from_list_invar_def distinct_map split: prod.splits)  
      using α_def 
      by (smt α_def inj_onD old.prod.case prod.inject set_mp)  
    done
 
  have inj_on_E: "inj_on α (set E)"
    apply(rule inj_on_subset)
    apply(rule uGraph_from_list_α_inj_on) by fact+ 

  show ?thesis
    unfolding uGraph_from_list_α_weight_def
    apply(subst sum.reindex[OF inj_on_E] ) 
    using * by auto 
qed
 


lemma corr: "uGraph_from_list_invar L ⟹
  <emp> kruskal_algo L
     <λF. ↑ (uGraph_from_list_invar F ∧ set F ⊆ set L ∧               
       uGraph.minSpanningForest (uGraph_from_list_α_edges L)
         (uGraph_from_list_α_weight L) (uGraph_from_list_α_edges F))>⇩t"
  apply(sep_auto heap: fromlist.kruskal_correct
          simp: uGraph_from_list_invar_conv kruskal_algo_def  ) 
  using uGraph_from_list_invar_subset uGraph_from_list_invar_conv by simp



lemma "uGraph_from_list_invar L ⟹
  <emp> kruskal_algo L
     <λF. ↑ (uGraph_from_list_invar F ∧ set F ⊆ set L ∧
       uGraph.spanningForest (uGraph_from_list_α_edges L) (uGraph_from_list_α_edges F)
      ∧ (∀F'. uGraph.spanningForest (uGraph_from_list_α_edges L) (uGraph_from_list_α_edges F')
          ⟶ set F' ⊆ set L ⟶  sum (λ(u,w,v). w) (set F) ≤ sum (λ(u,w,v). w) (set F')))>⇩t"
proof -
  assume a: "uGraph_from_list_invar L"
  then interpret fromlist L apply unfold_locales by (auto simp: uGraph_from_list_invar_def)
  from a show ?thesis
    by(sep_auto heap: corr simp: minSpanningForest_def sum_easier)
qed


subsection ‹Kruskal with input check›

definition "kruskal' L = kruskal (return L)  (λ(u,w,v). return (u,v)) ()"

definition "kruskal_checked L = (if uGraph_from_list_invar L
                             then do { F ← kruskal' L; return (Some F) }
                             else return None)"

 
lemma "<emp> kruskal_checked L <λ
    Some F ⇒ ↑ (uGraph_from_list_invar L ∧ set F ⊆ set L
       ∧ uGraph.minSpanningForest (uGraph_from_list_α_edges L) (uGraph_from_list_α_weight L)
           (uGraph_from_list_α_edges F))
  | None ⇒ ↑ (¬ uGraph_from_list_invar L)>⇩t"
  unfolding kruskal_checked_def
  apply(cases "uGraph_from_list_invar L") apply simp_all
  subgoal proof -
    assume [simp]: "uGraph_from_list_invar L"
    then interpret fromlist L apply unfold_locales by(auto simp: uGraph_from_list_invar_def)
    show ?thesis unfolding kruskal'_def by (sep_auto heap: kruskal_correct)   
  qed
  subgoal by sep_auto
  done 

subsection ‹Code export›

export_code uGraph_from_list_invar checking SML_imp
export_code kruskal_checked checking SML_imp

ML_val ‹
  val export_nat = @{code integer_of_nat}
  val import_nat = @{code nat_of_integer}
  val export_int = @{code integer_of_int}
  val import_int = @{code int_of_integer}
  val import_list = map (fn (a,b,c) => (import_nat a, (import_int b, import_nat c)))
  val export_list = map (fn (a,(b,c)) => (export_nat a, export_int b, export_nat c))
  val export_Some_list = (fn SOME l => SOME (export_list l) | NONE => NONE)

  fun kruskal l = @{code kruskal} (fn () => import_list l) (fn (a,(_,c)) => fn () => (a,c)) () ()
                     |> export_list 
  fun kruskal_checked l = @{code kruskal_checked} (import_list l) ()  |> export_Some_list


  val result = kruskal [(1,~9,2),(2,~3,3),(3,~4,1)]
  val result4 = kruskal [(1,~100,4), (3,64,5), (1,13,2), (3,20,2), (2,5,5), (4,80,3), (4,40,5)]

  val result' = kruskal_checked [(1,~9,2),(2,~3,3),(3,~4,1)]
  val result1' = kruskal_checked [(1,~9,2),(2,~3,3),(3,~4,1),(1,5,3)]
  val result2' = kruskal_checked [(1,~9,2),(2,~3,3),(3,~4,1),(3,~4,1)]
  val result3' = kruskal_checked [(1,~9,2),(2,~3,3),(3,~4,1),(1,~4,1)]
  val result4' = kruskal_checked [(1,~100,4), (3,64,5), (1,13,2), (3,20,2),
                                   (2,5,5), (4,80,3), (4,40,5)]
›


end