Theory Prim_Abstract

section ‹Abstract Prim Algorithm›
theory Prim_Abstract
imports 
  Main 
  Common
  Undirected_Graph
  "HOL-Eisbach.Eisbach"
begin
    
subsection ‹Generic Algorithm: Light Edges\label{sec:generic_mst}›

definition "is_subset_MST w g A ≡ ∃t. is_MST w g t ∧ A ⊆ edges t"  

lemma is_subset_MST_empty[simp]: "connected g ⟹ is_subset_MST w g {}"
  using exists_MST unfolding is_subset_MST_def by blast

text ‹We fix a start node and a weighted graph›
locale Prim =
  fixes w :: "'v set ⇒ nat" and g :: "'v ugraph" and r :: 'v
begin

text ‹Reachable part of the graph›
definition "rg ≡ component_of g r"

lemma reachable_connected[simp, intro!]: "connected rg" 
  unfolding rg_def by auto
  
lemma reachable_edges_subset: "edges rg ⊆ edges g" 
  unfolding rg_def by (rule component_edges_subset)

definition "light_edge C u v 
  ≡   u∈C ∧ v∉C ∧ (u,v)∈edges rg 
    ∧ (∀(u',v')∈edges rg ∩ C×-C. w {u,v} ≤ w {u',v'})"  

definition "respects_cut A C ≡ A ⊆ C×C ∪ (-C)×(-C)"
    
lemma light_edge_is_safe:
  fixes A :: "('v×'v) set" and C :: "'v set"
  assumes subset_MST: "is_subset_MST w rg A"
  assumes respects_cut: "respects_cut A C"
  assumes light_edge: "light_edge C u v"
  shows "is_subset_MST w rg ({(v,u)} ∪ A)"
proof -
  have crossing_edge: "u∈C" "v∉C" "(u,v)∈edges rg"
    and min_edge: "∀(u',v')∈edges rg ∩ C×-C. w {u,v} ≤ w {u',v'}"
    using light_edge unfolding light_edge_def by auto

  from subset_MST obtain T where T: "is_MST w rg T" "A ⊆ edges T" 
    unfolding is_subset_MST_def by auto
  hence "tree T" "edges T ⊆ edges rg" "nodes T = nodes rg" 
    by (simp_all add: is_MST_def is_spanning_tree_def)
  hence "connected T" by(simp_all add: tree_def)
  show ?thesis
  proof cases
    assume "(u,v) ∈ edges T"
    thus ?thesis unfolding is_subset_MST_def using T by (auto simp: edges_sym')
  next
    assume "(u,v) ∉ edges T" hence "(v,u)∉edges T" by (auto simp: edges_sym')
    from ‹(u,v)∈edges rg› obtain p where p: "path T u p v" "simple p"
      by (metis connectedD ‹connected T› ‹nodes T = nodes rg› nodesI 
          rtrancl_edges_iff_path simplify_pathE)
      
    have [simp]: "u≠v" using crossing_edge by blast
      
    from find_crossing_edge_on_path[OF p(1), where P="λx. x∉C"] 
         crossing_edge(1,2)
    obtain x y p1 p2 where xy: "(x,y) ∈ set p" "x ∈ C" "y ∉ C"
      and ux: "path (restrict_edges T (-{(x,y),(y,x)})) u p1 x" 
      and yv: "path (restrict_edges T (-{(x,y),(y,x)})) y p2 v"
      using path_change[OF crossing_edge(1,2) p] by blast
    have "(x,y) ∈ edges T" 
      by (meson contra_subsetD p(1) path_edges xy(1))

    let ?E' = "edges T - {(x,y),(y,x)}"
      
    from split_tree[OF ‹tree T› ‹(x,y)∈edges T›]
      obtain T1 T2 where T12: 
        "tree T1" "tree T2" 
        and "nodes T1 ∩ nodes T2 = {}" 
        and "nodes T = nodes T1 ∪ nodes T2"
        and "edges T1 ∪ edges T2 = ?E'"
        and "nodes T1 = { u . (x,u)∈?E'⇧*}"
        and "nodes T2 = { u . (y,u)∈?E'⇧*}"
        and "x∈nodes T1" "y∈nodes T2" .
    
    let ?T' = "ins_edge (u,v) (graph_join T1 T2)"    

    have "is_spanning_tree rg ?T'" proof -
      
      have E'_sym: "sym (?E'⇧*)" 
        by (meson edgesT_diff_sng_inv_eq sym_conv_converse_eq sym_rtrancl)
      
      have "u∈nodes T1" 
        unfolding ‹nodes T1 = _›
        using path_rtrancl_edgesD[OF ux] by (auto dest: symD[OF E'_sym])
        
      have "v∈nodes T2" 
        unfolding ‹nodes T2 = _›
        using path_rtrancl_edgesD[OF yv] by auto
              
      have "tree ?T'" by (rule join_trees) fact+

      show "is_spanning_tree rg ?T'"
        unfolding is_spanning_tree_def
        using ‹nodes T = nodes rg› ‹nodes T = nodes T1 ∪ nodes T2›[symmetric] 
        using ‹tree ?T'› ‹u≠v›
        using ‹edges T ⊆ edges rg› ‹edges T1 ∪ edges T2 = ?E'›
        apply simp
        by (metis Diff_subset crossing_edge(3) edges_sym' insert_absorb 
              nodesI(2) subset_trans)
    qed
    moreover 
      
    have "weight w ?T' ≤ weight w T'" if "is_spanning_tree rg T'" for T'
    proof -
      have ww: "w {u,v} ≤ w{x,y}" 
        using min_edge ‹(x,y)∈edges T› ‹edges T ⊆ edges rg› ‹x∈C› ‹y∉C›
        by blast
        
      have "weight w ?T' = weight w T - w {x,y} + w{u,v}"
        using ‹(u, v) ∉ edges T› ‹(x, y) ∈ edges T› 
        using ‹edges T1 ∪ edges T2 = edges T - {(x, y), (y, x)}› ‹u ≠ v›
        by (smt Diff_eq Diff_subset add.commute contra_subsetD edges_join 
              edges_restrict_edges minus_inv_sym_aux sup.idem weight_cong 
              weight_del_edge weight_ins_edge)
      also have "… ≤ weight w T" 
        using weight_ge_edge[OF ‹(x,y)∈edges T›, of w] ww by auto
      also have "weight w T ≤ weight w T'" using T(1) ‹is_spanning_tree rg T'›
        unfolding is_MST_def by simp
      finally show ?thesis . 
    qed
    ultimately have "is_MST w rg ?T'" using is_MST_def by blast
    have "{(u,v),(v,u)} ∪ A ⊆ edges ?T'" 
      using T(2) respects_cut xy(2,3) ‹edges T1 ∪ edges T2 = ?E'›
      unfolding respects_cut_def 
      by auto
      
    with ‹is_MST w rg ?T'› show ?thesis unfolding is_subset_MST_def by force
  qed
qed        

end    
   
subsection ‹Abstract Prim: Growing a Tree\label{sec:prim_algo}›
context Prim begin 

text ‹The current nodes› 
definition "S A ≡ {r} ∪ fst`A ∪ snd`A"

lemma respects_cut': "A ⊆ S A × S A"
  unfolding S_def by force

corollary respects_cut: "respects_cut A (S A)" 
  unfolding respects_cut_def using respects_cut' by auto
  
text ‹Refined invariant: Adds connectedness of ‹A››
definition "prim_invar1 A ≡ is_subset_MST w rg A ∧ (∀(u,v)∈A. (v,r)∈A⇧*)"

text ‹Measure: Number of nodes not in tree›
definition "T_measure1 A = card (nodes rg - S A)"

end

text ‹We use a locale that fixes a state and assumes the invariant›
locale Prim_Invar1_loc = 
  Prim w g r for w g and r :: 'v +
  fixes A :: "('v×'v) set"
  assumes invar1: "prim_invar1 A"
begin  
lemma subset_MST: "is_subset_MST w rg A" 
  using invar1 unfolding prim_invar1_def by auto
  
lemma A_connected: "(u,v)∈A ⟹ (v,r)∈A⇧*" 
  using invar1 unfolding prim_invar1_def by auto

lemma S_alt_def: "S A = {r} ∪ fst`A" 
  unfolding S_def
  apply (safe;simp)
  by (metis A_connected Domain_fst Not_Domain_rtrancl)

lemma finite_rem_nodes[simp,intro!]: "finite (nodes rg - S A)" by auto

lemma A_edges: "A ⊆ edges g"  
  using subset_MST
  by (meson is_MST_def is_spanning_tree_def is_subset_MST_def 
        reachable_edges_subset subset_eq)

lemma S_reachable: "S A ⊆ nodes rg"  
  unfolding S_alt_def
  by (smt DomainE Un_insert_left fst_eq_Domain insert_subset is_MST_def 
        is_spanning_tree_def is_subset_MST_def nodesI(1) nodes_of_component 
        reachable_nodes_refl rg_def subset_MST subset_iff sup_bot.left_neutral)
  
lemma S_edge_reachable: "⟦u∈S A; (u,v)∈edges g ⟧ ⟹ (u,v)∈edges rg"  
  using S_reachable unfolding rg_def
  using reachable_nodes_step'(2) by fastforce
    
lemma edges_S_rg_edges: "edges g ∩ S A×-S A = edges rg ∩ S A×-S A"
  using S_edge_reachable reachable_edges_subset by auto
      
lemma T_measure1_less: "T_measure1 A < card (nodes rg)"
  unfolding T_measure1_def S_def
  by (metis Diff_subset S_def S_reachable Un_insert_left le_supE nodes_finite 
        psubsetI psubset_card_mono singletonI subset_Diff_insert)


lemma finite_A[simp, intro!]: "finite A"
  using A_edges finite_subset by auto

lemma finite_S[simp, intro!]: "finite (S A)" 
  using S_reachable rev_finite_subset by blast

(* TODO: Used? *)
lemma S_A_consistent[simp, intro!]: "nodes_edges_consistent (S A) (A∪A¯)"
  unfolding nodes_edges_consistent_def
  apply (intro conjI)
  subgoal by simp
  subgoal using A_edges irrefl_def by fastforce
  subgoal by (simp add: sym_Un_converse)
  using respects_cut' by auto
    
      
end

context Prim begin

lemma invar1_initial: "prim_invar1 {}"
  by (auto simp: is_subset_MST_def prim_invar1_def exists_MST)

lemma maintain_invar1:
  assumes invar: "prim_invar1 A"
  assumes light_edge: "light_edge (S A) u v"
  shows "prim_invar1 ({(v,u)}∪A) 
       ∧ T_measure1 ({(v,u)}∪A) < T_measure1 A" (is "?G1 ∧ ?G2")
proof

  from invar interpret Prim_Invar1_loc w g r A by unfold_locales

  from light_edge have "u∈S A" "v∉S A" by (simp_all add: light_edge_def)
      
  show ?G1
    unfolding prim_invar1_def
  proof (intro conjI)
    show "is_subset_MST w rg ({(v, u)} ∪ A)"
      by (rule light_edge_is_safe[OF subset_MST respects_cut light_edge])
      
  next
    show "∀(ua, va)∈{(v, u)} ∪ A. (va, r) ∈ ({(v, u)} ∪ A)⇧*"
      apply safe
      subgoal
        using A_connected
        by (simp add: rtrancl_insert) 
           (metis DomainE S_alt_def converse_rtrancl_into_rtrancl ‹u∈S A› 
                    fst_eq_Domain insertE insert_is_Un rtrancl_eq_or_trancl)
      subgoal using A_connected by (simp add: rtrancl_insert)
      done
  qed
  then interpret N: Prim_Invar1_loc w g r "{(v,u)}∪A" by unfold_locales
  
  have "S A ⊂ S ({(v,u)}∪A)" using ‹v∉S A›
    unfolding S_def by auto
  then show "?G2" unfolding T_measure1_def
    using S_reachable N.S_reachable
    by (auto intro!: psubset_card_mono)

qed  

lemma invar1_finish:
  assumes INV: "prim_invar1 A"
  assumes FIN: "edges g ∩ S A×-S A = {}"
  shows "is_MST w rg (graph {r} A)"
proof -
  from INV interpret Prim_Invar1_loc w g r A by unfold_locales

  from subset_MST obtain t where MST: "is_MST w rg t" and "A ⊆ edges t"
    unfolding is_subset_MST_def by auto
  
  have "S A = nodes t"
  proof safe
    fix u
    show "u∈S A ⟹ u∈nodes t" using MST
      unfolding is_MST_def is_spanning_tree_def
      using S_reachable by auto
  next
    fix u
    assume "u∈nodes t"
    hence "u∈nodes rg"
      using MST is_MST_def is_spanning_tree_def by force
    hence 1: "(u,r)∈(edges rg)⇧*" by (simp add: connectedD rg_def)
    have "r∈S A" by (simp add: S_def)
    show "u∈S A" proof (rule ccontr)
      assume "u∉S A"
      from find_crossing_edge_rtrancl[where P="λu. u∈S A", OF 1 ‹u∉S A› ‹r∈S A›] 
        FIN reachable_edges_subset 
      show False
        by (smt ComplI IntI contra_subsetD edges_sym' emptyE mem_Sigma_iff)
        
    qed
  qed
  also have "nodes t = nodes rg" 
    using MST unfolding is_MST_def is_spanning_tree_def
    by auto
  finally have S_eq: "S A = nodes rg" .
  
  define t' where "t' = graph {r} A"
  
  have [simp]: "nodes t' = S A" and Et': "edges t' = (A∪A¯)" unfolding t'_def 
    using A_edges
    by (auto simp: graph_accs S_def)
  
  hence "edges t' ⊆ edges t"
    by (smt UnE ‹A ⊆ edges t› converseD edges_sym' subrelI subset_eq)
  
  have "is_spanning_tree rg t'"
  proof -
    have "connected t'"  
      apply rule
      apply (simp add: Et' S_def)
      apply safe
      apply ((simp add: A_connected converse_rtrancl_into_rtrancl 
                        in_rtrancl_UnI rtrancl_converse
             )+
      ) [4]
      apply simp_all [4]
      apply ((meson A_connected in_rtrancl_UnI r_into_rtrancl 
                rtrancl_converseI rtrancl_trans
             )+
      ) [4]
      done
  
    moreover have "cycle_free t'"
      by (meson MST ‹edges t' ⊆ edges t› cycle_free_antimono is_MST_def 
                is_spanning_tree_def tree_def)      
    moreover have "edges t' ⊆ edges rg"
      by (meson MST ‹edges t' ⊆ edges t› dual_order.trans is_MST_def 
            is_spanning_tree_def)
    ultimately show ?thesis
      unfolding is_spanning_tree_def tree_def
      by (auto simp: S_eq)
  qed                              
  then show ?thesis
    using MST weight_mono[OF ‹edges t' ⊆ edges t›]
    unfolding t'_def is_MST_def 
    using dual_order.trans by blast
qed    
        
end

subsection ‹Prim: Using a Priority Queue\label{sec:using_pq}›
text ‹We define a new locale. Note that we could also reuse @{locale Prim}, however,
  this would complicate referencing the constants later in the theories from 
  which we generate the paper.
›
locale Prim2 = Prim w g r for w :: "'v set ⇒ nat" and g :: "'v ugraph" and r :: 'v
begin  

text ‹Abstraction to edge set›
definition "A Q π ≡ {(u,v). π u = Some v ∧ Q u = ∞}"


text ‹Initialization›
definition initQ :: "'v ⇒ enat"  where "initQ ≡ (λ_. ∞)(r := 0)"
definition initπ :: "'v ⇒ 'v option" where "initπ ≡ Map.empty"  


text ‹Step›  
definition "upd_cond Q π u v' ≡ 
    (v',u) ∈ edges g 
  ∧ v'≠r ∧ (Q v' = ∞ ⟶ π v' = None)
  ∧ enat (w {v',u}) < Q v'"
  
text ‹State after inner loop›  
definition "Qinter Q π u v' 
  = (if upd_cond Q π u v' then enat (w {v',u}) else Q v')"

text ‹State after one step›  
definition "Q' Q π u ≡ (Qinter Q π u)(u:=∞)"
definition "π' Q π u v' = (if upd_cond Q π u v' then Some u else π v')"

definition "prim_invar2_init Q π ≡ Q=initQ ∧ π=initπ"

definition "prim_invar2_ctd Q π ≡ let A = A Q π; S = S A in
  prim_invar1 A
∧ π r = None ∧ Q r = ∞  
∧ (∀(u,v)∈edges rg ∩ (-S)×S. Q u ≠ ∞)
∧ (∀u. Q u ≠ ∞ ⟶ π u ≠ None)
∧ (∀u v. π u = Some v ⟶ v∈S ∧ (u,v)∈edges rg)
∧ (∀u v d. Q u = enat d ∧ π u = Some v 
      ⟶ d=w {u,v} ∧ (∀v'∈S. (u,v')∈edges rg ⟶ d ≤ w {u,v'}))  
"

lemma prim_invar2_ctd_alt_aux1: 
  assumes "prim_invar1 (A Q π)"
  assumes "Q u ≠ ∞" "u≠r"  
  shows "u∉S (A Q π)"
proof -
  interpret Prim_Invar1_loc w g r "A Q π" by unfold_locales fact
  show ?thesis
    unfolding S_alt_def unfolding A_def using assms
    by auto
qed

lemma prim_invar2_ctd_alt: "prim_invar2_ctd Q π ⟷ (
  let A = A Q π; S = S A; cE=edges rg ∩ (-S)×S in
    prim_invar1 A
  ∧ π r = None ∧ Q r = ∞  
  ∧ (∀(u,v)∈cE. Q u ≠ ∞)
  ∧ (∀u v. π u = Some v ⟶ v∈S ∧ (u,v)∈edges rg)
  ∧ (∀u d. Q u = enat d 
      ⟶ (∃v. π u = Some v ∧ d=w {u,v} ∧ (∀v'. (u,v')∈cE ⟶ d ≤ w {u,v'})))
)"
  unfolding prim_invar2_ctd_def Let_def
  using prim_invar2_ctd_alt_aux1[of Q π]
  apply safe
  subgoal by auto
  subgoal by (auto 0 3)
  subgoal by (auto 0 3)
  subgoal by clarsimp (metis (no_types,lifting) option.simps(3))
  done

definition "prim_invar2 Q π ≡ prim_invar2_init Q π ∨ prim_invar2_ctd Q π"
  
definition "T_measure2 Q π 
  ≡ if Q r = ∞ then T_measure1 (A Q π) else card (nodes rg)"


lemma Q'_init_eq: 
  "Q' initQ initπ r = (λu. if (u,r)∈edges rg then enat (w {u,r}) else ∞)"
  apply (rule ext) 
  using reachable_edges_subset
  apply (simp add: Q'_def Qinter_def upd_cond_def initQ_def initπ_def)
  by (auto simp: Prim.rg_def edges_sym' reachable_nodes_step'(2))

lemma π'_init_eq: 
  "π' initQ initπ r = (λu. if (u,r)∈edges rg then Some r else None)"  
  apply (rule ext) 
  using reachable_edges_subset
  apply (simp add: π'_def upd_cond_def initQ_def initπ_def)
  by (auto simp: Prim.rg_def edges_sym' reachable_nodes_step'(2))

lemma A_init_eq: "A initQ initπ = {}"  
  unfolding A_def initπ_def 
  by auto

lemma S_empty: "S {} = {r}" unfolding S_def by (auto simp: A_init_eq)
      
lemma maintain_invar2_first_step: 
  assumes INV: "prim_invar2_init Q π"
  assumes UNS: "Q u = enat d"
  shows "prim_invar2_ctd (Q' Q π u) (π' Q π u)" (is ?G1)
    and "T_measure2 (Q' Q π u) (π' Q π u) < T_measure2 Q π" (is ?G2)
proof -
  from INV have [simp]: "Q=initQ" "π=initπ"
    unfolding prim_invar2_init_def by auto
  from UNS have [simp]: "u=r" by (auto simp: initQ_def split: if_splits) 
    
    
  note Q'_init_eq π'_init_eq A_init_eq 
    
  have [simp]: "(A (Q' initQ initπ r) (π' initQ initπ r)) = {}"
    apply (simp add: Q'_init_eq π'_init_eq)
    by (auto simp: A_def split: if_splits)
  
  show ?G1
    apply (simp add: prim_invar2_ctd_def Let_def invar1_initial)
    by (auto simp: Q'_init_eq π'_init_eq S_empty split: if_splits)
    
  have [simp]: "Q' initQ initπ r r = ∞"  
    by (auto simp: Q'_init_eq)
    
  have [simp]: "initQ r = 0" by (simp add: initQ_def) 
    
  show ?G2  
    unfolding T_measure2_def 
    apply simp
    apply (simp add: T_measure1_def S_empty)
    by (metis card_Diff1_less nodes_finite nodes_of_component 
          reachable_nodes_refl rg_def)
  
qed    
  
lemma maintain_invar2_first_step_presentation: 
  assumes INV: "prim_invar2_init Q π"
  assumes UNS: "Q u = enat d"
  shows "prim_invar2_ctd (Q' Q π u) (π' Q π u)
       ∧ T_measure2 (Q' Q π u) (π' Q π u) < T_measure2 Q π"
  using maintain_invar2_first_step assms by blast

end

(*<*)
(*
  This locale is only used to present the invariant in the paper.
*)
locale Prim_Invar2_ctd_Presentation_Loc =
  fixes w g and r :: 'v and Q π A S rg cE
  assumes I: "Prim2.prim_invar2_ctd w g r Q π"
  defines local_A_def: "A ≡ Prim2.A Q π"
  defines local_S_def: "S ≡ Prim.S r A"
  defines local_rg_def: "rg ≡ Prim.rg g r"
  defines local_cE_def: "cE ≡ edges rg ∩ (-S)×S"
begin  

lemma 
      invar1: "Prim.prim_invar1 w g r A" (is ?G1)
  and root_contained: "π r = None ∧ Q r = ∞" (is ?G2)
  and Q_defined: "∀(u,v)∈cE. Q u ≠ ∞" (is ?G3)
  and π_edges: "∀u v. π u = Some v ⟶ v∈S ∧ (u,v)∈edges rg" (is ?G4)
  and Q_min: "∀u d. Q u = enat d 
      ⟶ (∃v. π u = Some v ∧ d=w {u,v} ∧ (∀v'. (u,v')∈cE ⟶ d ≤ w {u,v'}))" 
      (is ?G5)
proof -
  interpret Prim2 w g r .
  
  show ?G1 ?G2 ?G3 ?G4 ?G5
    using I
    unfolding local_A_def local_S_def local_rg_def local_cE_def 
              prim_invar2_ctd_alt Let_def
    by simp_all
qed    

end

lemma (in Prim2) Prim_Invar2_ctd_Presentation_Loc_eq:
  "Prim_Invar2_ctd_Presentation_Loc w g r Q π ⟷ prim_invar2_ctd Q π"
  unfolding Prim_Invar2_ctd_Presentation_Loc_def ..

(*>*)

text ‹Again, we define a locale to fix a state and assume the invariant› 
locale Prim_Invar2_ctd_loc =   
  Prim2 w g r for w g and r :: 'v +
  fixes Q π
  assumes invar2: "prim_invar2_ctd Q π"
begin

sublocale Prim_Invar1_loc w g r "A Q π"
  using invar2 unfolding prim_invar2_ctd_def
  apply unfold_locales by (auto simp: Let_def)

lemma upd_cond_alt: "upd_cond Q π u v' ⟷ 
  (v',u) ∈ edges g ∧ v'∉S (A Q π) ∧ enat (w {v',u}) < Q v'" 
  unfolding upd_cond_def S_alt_def unfolding A_def
  by (auto simp: fst_eq_Domain)
  
lemma π_root: "π r = None"
  and Q_root: "Q r = ∞" 
  and Q_defined: "⟦ (u,v)∈edges rg; u∉S (A Q π); v∈S (A Q π) ⟧ ⟹ Q u ≠ ∞"
  and π_defined: "⟦ Q u ≠ ∞ ⟧ ⟹ π u ≠ None"
  and frontier: "π u = Some v ⟹ v∈S (A Q π)"
  and edges: "π u = Some v ⟹ (u,v)∈edges rg"
  and Q_π_consistent: "⟦ Q u = enat d; π u = Some v ⟧ ⟹ d = w {u,v}" 
  and Q_min: "Q u = enat d 
      ⟹ (∀v'∈S (A Q π). (u,v')∈edges rg ⟶ d ≤ w {u,v'})"
  using invar2 unfolding prim_invar2_ctd_def Let_def by auto

lemma π_def_on_S: "⟦u∈S (A Q π); u≠r⟧ ⟹ π u ≠ None"
  unfolding S_alt_def
  unfolding A_def
  by auto 
  
lemma π_def_on_edges_to_S: "⟦v∈S (A Q π); u≠r; (u,v)∈edges rg⟧ ⟹ π u ≠ None"
  apply (cases "u∈S (A Q π)")
  subgoal using π_def_on_S by auto
  subgoal by (simp add: Q_defined π_defined)
  done
  
lemma Q_min_is_light:  
  assumes UNS: "Q u = enat d"
  assumes MIN: "∀v. enat d ≤ Q v"
  obtains v where "π u = Some v" "light_edge (S (A Q π)) v u"
proof -
  let ?A = "A Q π"
  let ?S = "S ?A"

  from UNS obtain v where 
    S1[simp]: "π u = Some v" "d = w {u,v}"
    using π_defined Q_π_consistent 
    by blast
          
  have "v∈?S" using frontier[of u v] by auto
    
  have [simp]: "u≠r" using π_root using S1 by (auto simp del: S1)
  
  have "u∉?S" unfolding S_alt_def unfolding A_def using UNS by auto
  
  have "(v,u)∈edges rg" using edges[OF S1(1)]
    by (meson edges_sym' rev_subsetD)
  
  have M: "∀(u', v')∈edges rg ∩ ?S × - ?S. w {v, u} ≤ w {u', v'}"
  proof safe
    fix a b
    assume "(a,b)∈edges rg" "a∈?S" "b∉?S"
    hence "(b,a)∈edges rg" by (simp add: edges_sym')
  
    from Q_defined[OF ‹(b,a)∈edges rg› ‹b∉?S› ‹a∈?S›] 
      obtain d' where 1: "Q b = enat d'" by blast 
    with π_defined obtain a' where "π b = Some a'" by auto
    from MIN 1 have "d≤d'" by (metis enat_ord_simps(1))
    also from Q_min[OF 1] ‹(b,a)∈edges rg› ‹a∈?S› have "d'≤w {b,a}" by blast  
    finally show "w {v,u} ≤ w {a,b}" by (simp add: insert_commute)
  qed  

  have LE: "light_edge ?S v u" using invar1 ‹v∈?S› ‹u∉?S› ‹(v,u)∈edges rg› M
    unfolding light_edge_def by blast
  
  thus ?thesis using that by auto
qed
      
lemma maintain_invar_ctd: 
  assumes UNS: "Q u = enat d"
  assumes MIN: "∀v. enat d ≤ Q v"
  shows "prim_invar2_ctd (Q' Q π u) (π' Q π u)" (is ?G1)
    and "T_measure2 (Q' Q π u) (π' Q π u) < T_measure2 Q π" (is ?G2)
proof -
  let ?A = "A Q π"
  let ?S = "S ?A"

  from Q_min_is_light[OF UNS MIN] obtain v where 
    [simp]: "π u = Some v" and LE: "light_edge ?S v u" .

  let ?Q' = "Q' Q π u"
  let ?π' = "π' Q π u"
  let ?A' = "A ?Q' ?π'"
  let ?S' = "S ?A'"
  
  have NA: "?A' = {(u,v)} ∪ ?A"
    unfolding A_def  
    unfolding Q'_def π'_def upd_cond_def Qinter_def
    by (auto split: if_splits)
  
  from maintain_invar1[OF invar1 LE]
  have "prim_invar1 ?A'" and M1: "T_measure1 ?A' < T_measure1 ?A" 
    by (auto simp: NA) 
  then interpret N: Prim_Invar1_loc w g r ?A' by unfold_locales
              
  have [simp]: "?S' = insert u ?S"
    unfolding S_alt_def N.S_alt_def
    unfolding Q'_def Qinter_def π'_def upd_cond_def
    unfolding A_def
    by (auto split: if_splits simp: image_iff)
    
  show ?G1
    unfolding prim_invar2_ctd_def Let_def  
    apply safe
    subgoal by fact
    subgoal 
      unfolding π'_def upd_cond_def
      by (auto simp: π_root)
    subgoal 
      by (simp add: Prim2.Q'_def Prim2.Qinter_def Prim2.upd_cond_def Q_root)
    subgoal for a b
      apply simp
      apply safe
      subgoal
        unfolding Q'_def Qinter_def upd_cond_def
        apply (simp add: S_alt_def A_def)
        apply safe
        subgoal using reachable_edges_subset by blast
        subgoal by (simp add: Prim.S_def)
        subgoal by (metis (no_types) A_def Q_defined edges frontier)
        subgoal using not_infinity_eq by fastforce
        done
      subgoal
        unfolding S_alt_def N.S_alt_def 
        unfolding A_def Q'_def Qinter_def upd_cond_def
        apply (simp; safe; (auto;fail)?)
        subgoal
        proof -
          assume a1: "(a, r) ∈ edges rg"
          assume "a ∉ fst ` {(u, v). π u = Some v ∧ Q u = ∞}"
          then have "a ∉ fst ` A Q π"
            by (simp add: A_def)
          then show ?thesis
            using a1 
            by (metis (no_types) S_alt_def Q_defined Un_insert_left 
                  edges_irrefl' insert_iff not_infinity_eq sup_bot.left_neutral)
        qed 
        subgoal by (simp add: fst_eq_Domain)
        subgoal 
          apply clarsimp
          by (smt Domain.intros Q_defined π_def_on_edges_to_S case_prod_conv 
                edges enat.exhaust frontier fst_eq_Domain mem_Collect_eq 
                option.exhaust) 
        subgoal by (simp add: fst_eq_Domain) 
        done
      done
    subgoal 
      by (metis Q'_def Qinter_def π'_def π_defined enat.distinct(2) 
            fun_upd_apply not_None_eq)
      
    subgoal
      by (metis ‹S (A (Q' Q π u) (π' Q π u)) = insert u (S (A Q π))› π'_def 
            frontier insertCI option.inject)
    subgoal
      by (metis N.S_edge_reachable upd_cond_def 
          ‹S (A (Q' Q π u) (π' Q π u)) = insert u (S (A Q π))› π'_def edges 
          edges_sym' insertI1 option.inject)
    subgoal
      by (smt Q'_def π'_def Q_π_consistent Qinter_def fun_upd_apply 
            insert_absorb not_enat_eq option.inject the_enat.simps)
    subgoal for v' d'
      apply clarsimp
      unfolding Q'_def Qinter_def upd_cond_def      
      using Q_min
      apply (clarsimp split: if_splits; safe)
      apply (all ‹(auto;fail)?›)
      subgoal by (simp add: le_less less_le_trans)
      subgoal using π_def_on_edges_to_S by auto
      subgoal using reachable_edges_subset by auto
      subgoal by (simp add: Q_root)
      done
    done       
  then interpret N: Prim_Invar2_ctd_loc w g r ?Q' ?π' by unfold_locales

  show ?G2  
    unfolding T_measure2_def
    by (auto simp: Q_root N.Q_root M1)
    
qed      

end

  
context Prim2 begin

lemma maintain_invar2_ctd: 
  assumes INV: "prim_invar2_ctd Q π"
  assumes UNS: "Q u = enat d"
  assumes MIN: "∀v. enat d ≤ Q v"
  shows "prim_invar2_ctd (Q' Q π u) (π' Q π u)" (is ?G1)
    and "T_measure2 (Q' Q π u) (π' Q π u) < T_measure2 Q π" (is ?G2)
proof -
  interpret Prim_Invar2_ctd_loc w g r Q π using INV by unfold_locales
  from maintain_invar_ctd[OF UNS MIN] show ?G1 ?G2 by auto
qed

lemma Q_min_is_light_presentation:  
  assumes INV: "prim_invar2_ctd Q π"
  assumes UNS: "Q u = enat d"
  assumes MIN: "∀v. enat d ≤ Q v"
  obtains v where "π u = Some v" "light_edge (S (A Q π)) v u"
proof -
  interpret Prim_Invar2_ctd_loc w g r Q π using INV by unfold_locales
  from Q_min_is_light[OF UNS MIN] show ?thesis using that .
qed

lemma maintain_invar2_ctd_presentation: 
  assumes INV: "prim_invar2_ctd Q π"
  assumes UNS: "Q u = enat d"
  assumes MIN: "∀v. enat d ≤ Q v"
  shows "prim_invar2_ctd (Q' Q π u) (π' Q π u)
       ∧ T_measure2 (Q' Q π u) (π' Q π u) < T_measure2 Q π"
  using maintain_invar2_ctd assms by blast

lemma not_invar2_ctd_init: 
  "prim_invar2_init Q π ⟹ ¬prim_invar2_ctd Q π"
  unfolding prim_invar2_init_def prim_invar2_ctd_def initQ_def Let_def 
  by (auto)

lemma invar2_init_init: "prim_invar2_init initQ initπ"
  unfolding prim_invar2_init_def by auto
  
lemma invar2_init: "prim_invar2 initQ initπ"
  unfolding prim_invar2_def using invar2_init_init by auto

lemma maintain_invar2: 
  assumes A: "prim_invar2 Q π"  
  assumes UNS: "Q u = enat d"
  assumes MIN: "∀v. enat d ≤ Q v"
  shows "prim_invar2 (Q' Q π u) (π' Q π u)" (is ?G1)
    and "T_measure2 (Q' Q π u) (π' Q π u) < T_measure2 Q π" (is ?G2)
  using A unfolding prim_invar2_def
  using maintain_invar2_first_step[of Q,OF _ UNS]
  using maintain_invar2_ctd[OF _ UNS MIN]
  using not_invar2_ctd_init
  apply blast+
  done

lemma invar2_ctd_finish:  
  assumes INV: "prim_invar2_ctd Q π"  
  assumes FIN: "Q = (λ_. ∞)"
  shows "is_MST w rg (graph {r} {(u, v). π u = Some v})"
proof -  
  from INV interpret Prim_Invar2_ctd_loc w g r Q π by unfold_locales

  let ?A = "A Q π" let ?S="S ?A"
  
  have FC: "edges g ∩ ?S × - ?S = {}" 
  proof (safe; simp)
    fix a b
    assume "(a,b)∈edges g" "a∈?S" "b∉?S"
    with Q_defined[OF edges_sym'] S_edge_reachable have "Q b ≠ ∞" 
      by blast
    with FIN show False by auto
  qed
  
  have Aeq: "?A = {(u, v). π u = Some v}"
    unfolding A_def using FIN by auto
  
  from invar1_finish[OF invar1 FC, unfolded Aeq] show ?thesis .
qed
  
  
lemma invar2_finish:  
  assumes INV: "prim_invar2 Q π"  
  assumes FIN: "Q = (λ_. ∞)"
  shows "is_MST w rg (graph {r} {(u, v). π u = Some v})"
proof -  
  from INV have "prim_invar2_ctd Q π"
    unfolding prim_invar2_def prim_invar2_init_def initQ_def
    by (auto simp: fun_eq_iff FIN split: if_splits)
  with FIN invar2_ctd_finish show ?thesis by blast  
qed
  
end


subsection ‹Refinement of Inner Foreach Loop\label{sec:using_foreach}›

context Prim2 begin

definition "foreach_body u ≡ λ(v,d) (Q,π).
  if v=r then (Q,π)
  else
    case (Q v, π v) of
      (∞,None) ⇒ (Q(v:=enat d), π(v↦u))
    | (enat d',_) ⇒ if d<d' then (Q(v:=enat d), π(v↦u)) else (Q,π)
    | (∞,Some _) ⇒ (Q,π)
  "

lemma foreach_body_alt: "foreach_body u = (λ(v,d) (Q,π). 
  if v≠r ∧ (π v = None ∨ Q v ≠ ∞) ∧ enat d < Q v then
    (Q(v:=enat d), π(v↦u))
  else 
    (Q,π)
)"  
  unfolding foreach_body_def S_def
  by (auto split: enat.splits option.splits simp: fst_eq_Domain fun_eq_iff)

definition foreach where
  "foreach u adjs Qπ = foldr (foreach_body u) adjs Qπ"

definition "⋀Q V. 
  Qigen Q π u adjs v = (if v ∉ fst`set adjs then Q v else Qinter Q π u v)"
definition "⋀Q V π. 
  π'gen Q π u adjs v = (if v ∉ fst`set adjs then π v else π' Q π u v)"

context begin

private lemma Qc: 
  "Qigen Q π u ((v, w {u, v}) # adjs) x 
  = (if x=v then Qinter Q π u v else Qigen Q π u adjs x)" for x
  unfolding Qigen_def by auto
  
private lemma πc: 
  "π'gen Q π u ((v, w {u, v}) # adjs) x 
  = (if x=v then π' Q π u v else π'gen Q π u adjs x)" for x
  unfolding π'gen_def by auto

lemma foreach_refine_gen:
  assumes "set adjs ⊆ {(v,d). (u,v)∈edges g ∧ w {u,v} = d}"          
  shows "foreach u adjs (Q,π) = (Qigen Q π u adjs,π'gen Q π u adjs)"
  using assms
  unfolding foreach_def
proof (induction adjs arbitrary: Q π)
  case Nil
  have INVAR_INIT: "Qigen Q π u [] = Q" "π'gen Q π u [] = π" for Q π
    unfolding assms Qigen_def π'gen_def 
    by (auto simp: fun_eq_iff image_def Q'_def π'_def edges_def)
  with Nil show ?case by (simp add: INVAR_INIT)
next
  case (Cons a adjs)
  obtain v d where [simp]: "a=(v,d)" by (cases a)
  
  have [simp]: "u≠v" "v≠u" using Cons.prems by auto
    
  have QinfD: "Qigen Q π u adjs v = ∞ ⟹ Q v = ∞"  
    unfolding Qigen_def Q'_def Qinter_def by (auto split: if_splits)
    
  show ?case using Cons.prems
    apply (cases a)
    apply (clarsimp simp: Cons.IH)
    unfolding foreach_body_def
    apply (clarsimp; safe)
    subgoal by (auto simp: Qigen_def Qinter_def upd_cond_def)
    subgoal by (auto simp: π'gen_def π'_def upd_cond_def)
    subgoal
      apply (clarsimp split: enat.split option.split simp: πc Qc fun_eq_iff)
      unfolding Qinter_def Qigen_def π'_def π'gen_def upd_cond_def
      apply (safe; simp split: if_splits add: insert_commute)
      by (auto dest: edges_sym')
    done
    
qed
      
lemma foreach_refine:
  assumes "set adjs = {(v,d). (u,v)∈edges g ∧ w {u,v} = d}"
  shows "foreach u adjs (Q,π) = (Qinter Q π u,π' Q π u)"
proof -
  have INVAR_INIT: "Qigen Q π u [] = Q" "π'gen Q π u [] = π" for Q π
    unfolding assms Qigen_def π'gen_def 
    by (auto simp: fun_eq_iff image_def Q'_def π'_def edges_def)
  from assms have 1: "set adjs ⊆ {(v,d). (u,v)∈edges g ∧ w {u,v} = d}" 
    by simp
  have [simp]: 
    "v ∈ fst ` {(v, d). (u, v) ∈ edges g ∧ w {u, v} = d} 
    ⟷ (u,v)∈edges g" 
    for v
    by force
    
  show ?thesis 
    unfolding foreach_refine_gen[OF 1] 
    unfolding Qigen_def π'gen_def assms upd_cond_def Qinter_def π'_def
    by (auto simp: fun_eq_iff image_def dest: edges_sym')      
    
qed

end
end

end