Theory Undirected_Graph_Impl

section ‹Implementation of Weighted Undirected Graph by Map›
theory Undirected_Graph_Impl
imports 
  "HOL-Data_Structures.Map_Specs"
  Common
  Undirected_Graph_Specs
begin

subsection ‹Doubleton Set to Pair›
definition "epair e = (if card e = 2 then Some (SOME (u,v). e={u,v}) else None)"

lemma epair_eqD: "epair e = Some (x,y) ⟹ (x≠y ∧ e={x,y})"
  apply (cases "card e = 2")
  unfolding epair_def
  apply simp_all
  apply (clarsimp simp: card_Suc_eq eval_nat_numeral doubleton_eq_iff)
  by (smt case_prodD case_prodI someI)

lemma epair_not_sng[simp]: "epair e ≠ Some (x,x)"  
  by (auto dest: epair_eqD)

lemma epair_None[simp]: "epair {a,b} = None ⟷ a=b" 
  unfolding epair_def by (auto simp: card2_eq) 
  
subsection ‹Generic Implementation›  

text ‹
  When instantiated with a map ADT, this locale provides a weighted graph ADT.
›
locale wgraph_by_map = 
  M: Map M_empty M_update M_delete M_lookup M_invar 
  
  for M_empty M_update M_delete 
  and M_lookup :: "'m ⇒ 'v ⇒ (('v×nat) list) option" 
  and M_invar 
begin

definition "αnodes_aux g ≡ dom (M_lookup g)"

definition "αedges_aux g 
  ≡ ({(u,v). ∃xs d. M_lookup g u = Some xs ∧ (v,d)∈set xs })"


definition "αg g ≡ graph (αnodes_aux g) (αedges_aux g)"

definition "αw g e ≡ case epair e of 
  Some (u,v) ⇒ (
    case M_lookup g u of 
      None ⇒ 0 
    | Some xs ⇒ the_default 0 (map_of xs v)
    )
| None ⇒ 0"

definition invar :: "'m ⇒ bool" where
  "invar g ≡ 
      M_invar g ∧ finite (dom (M_lookup g))
    ∧ (∀u xs. M_lookup g u = Some xs ⟶ 
          distinct (map fst xs) 
        ∧ u∉set (map fst xs)
        ∧ (∀(v,d)∈set xs. (u,d)∈set (the_default [] (M_lookup g v)))
      )"
  

lemma in_the_default_empty_conv[simp]: 
  "x∈set (the_default [] m) ⟷ (∃xs. m=Some xs ∧ x∈set xs)"
  by (cases m) auto  
  
lemma αedges_irrefl: "invar g ⟹ irrefl (αedges_aux g)" 
  unfolding invar_def irrefl_def αedges_aux_def
  by (force)
  
lemma αedges_sym: "invar g ⟹ sym (αedges_aux g)"  
  unfolding invar_def sym_def αedges_aux_def
  by force 
      
lemma αedges_subset: "invar g ⟹ αedges_aux g ⊆ αnodes_aux g × αnodes_aux g"
  unfolding invar_def αnodes_aux_def αedges_aux_def
  by force
                      
lemma αnodes_finite[simp, intro!]: "invar g ⟹ finite (αnodes_aux g)"
  unfolding invar_def αnodes_aux_def by simp
  
lemma αedges_finite[simp, intro!]: "invar g ⟹ finite (αedges_aux g)"
  using finite_subset[OF αedges_subset] by blast
      
definition adj :: "'m ⇒ 'v ⇒ ('v×nat) list" where
  "adj g v = the_default [] (M_lookup g v)"
  
definition empty :: "'m" where "empty = M_empty"

definition add_edge1 :: "'v×'v ⇒ nat ⇒ 'm ⇒ 'm" where
  "add_edge1 ≡ λ(u,v) d g. M_update u ((v,d) # the_default [] (M_lookup g u)) g"

definition add_edge :: "'v×'v ⇒ nat ⇒ 'm ⇒ 'm" where
  "add_edge ≡ λ(u,v) d g. add_edge1 (v,u) d (add_edge1 (u,v) d g)"
  

lemma edges_αg_aux: "invar g ⟹ edges (αg g) = αedges_aux g" 
  unfolding αg_def using αedges_sym αedges_irrefl
  by (auto simp: irrefl_def graph_accs)
 
lemma nodes_αg_aux: "invar g ⟹ nodes (αg g) = αnodes_aux g"  
  unfolding αg_def using αedges_subset
  by (force simp: graph_accs)

lemma card_doubleton_eq2[simp]: "card {a,b} = 2 ⟷ a≠b" by auto  

lemma the_dflt_Z_eq: "the_default 0 m = d ⟷ (m=None ∧ d=0 ∨ m=Some d)"
  by (cases m) auto

lemma adj_correct_aux:
  "invar g ⟹ set (adj g u) = {(v, d). (u, v) ∈ edges (αg g) ∧ αw g {u, v} = d}"  
  apply (simp add: edges_αg_aux)
  apply safe
  subgoal unfolding adj_def αedges_aux_def by auto
  subgoal for a d 
    unfolding adj_def αw_def
    apply (clarsimp split: prod.splits option.splits simp: the_dflt_Z_eq)
    unfolding invar_def
    by (force dest!: epair_eqD simp: doubleton_eq_iff)+
  subgoal for a 
    unfolding adj_def αw_def
    using αedges_irrefl[of g]
    apply (clarsimp split: prod.splits option.splits)
    apply safe
    subgoal by (auto simp: irrefl_def)
    subgoal 
      apply (clarsimp dest!: epair_eqD simp: doubleton_eq_iff)
      unfolding invar_def αedges_aux_def
      by force
    subgoal  
      apply (clarsimp dest!: epair_eqD simp: doubleton_eq_iff)
      unfolding invar_def αedges_aux_def
      apply clarsimp
      by (smt case_prod_conv map_of_is_SomeI the_default.simps(2))
    done      
  done      
    
lemma invar_empty_aux: "invar empty"  
  by (simp add: invar_def empty_def M.map_specs)

lemma dist_fst_the_dflt_aux: "distinct (map fst (the_default [] m)) 
  ⟷ (∀xs. m = Some xs ⟶ distinct (map fst xs))"  
  by (cases m; auto)

lemma invar_add_edge_aux: 
  "⟦invar g; (u, v) ∉ edges (αg g); u ≠ v⟧ ⟹ invar (add_edge (u, v) d g)"  
  apply (simp add: edges_αg_aux)
  unfolding add_edge_def add_edge1_def invar_def αedges_aux_def
  by (auto simp:  M.map_specs dist_fst_the_dflt_aux; force)
  
  
    
sublocale adt_wgraph αw αg invar adj empty add_edge 
  apply unfold_locales
  subgoal by (simp add: adj_correct_aux)
  subgoal by (simp add: invar_empty_aux)
  subgoal
    apply (simp 
        add: graph_eq_iff nodes_αg_aux invar_empty_aux edges_αg_aux
        add: αnodes_aux_def αedges_aux_def
        )
    apply (simp add: empty_def M.map_specs)
    done
  subgoal
    unfolding αw_def
    by (auto simp: empty_def M.map_specs fun_eq_iff split: option.splits)    
  subgoal by (simp add: invar_add_edge_aux)
  subgoal for g u v d
    apply (simp add: edges_αg_aux nodes_αg_aux graph_eq_iff invar_add_edge_aux)
    apply (rule conjI)
    subgoal
      unfolding add_edge_def add_edge1_def invar_def αnodes_aux_def
      by (auto simp: M.map_specs)
    subgoal
      unfolding add_edge_def add_edge1_def invar_def αedges_aux_def
      by (fastforce simp: M.map_specs split!: if_splits)
    done      
  subgoal for g u v d
    apply (simp add: edges_αg_aux invar_add_edge_aux)
    unfolding invar_def αw_def add_edge_def add_edge1_def
    by (auto 
      dest: epair_eqD 
      simp: fun_eq_iff M.map_specs 
      split!: prod.splits option.splits if_splits)
  done    
          
        
end
  

end