Theory Undirected_Graph_Specs

section ‹Abstract Graph Datatype›
theory Undirected_Graph_Specs
imports Undirected_Graph
begin

subsection ‹Abstract Weighted Graph›

locale adt_wgraph =
  fixes αw :: "'g ⇒ 'v set ⇒ nat" and αg :: "'g ⇒ 'v ugraph"
    and invar :: "'g ⇒ bool"
    and adj :: "'g ⇒ 'v ⇒ ('v×nat) list"
    and empty :: 'g
    and add_edge :: "'v×'v ⇒ nat ⇒ 'g ⇒ 'g"
  assumes adj_correct: "invar g 
    ⟹ set (adj g u) = {(v,d). (u,v)∈edges (αg g) ∧ αw g {u,v} = d}"
  assumes empty_correct:
    "invar empty"
    "αg empty = graph_empty"
    "αw empty = (λ_. 0)"
  assumes add_edge_correct:
    "⟦invar g; (u,v)∉edges (αg g); u≠v⟧ ⟹ invar (add_edge (u,v) d g)"
    "⟦invar g; (u,v)∉edges (αg g); u≠v⟧ 
      ⟹ αg (add_edge (u,v) d g) = ins_edge (u,v) (αg g)"
    "⟦invar g; (u,v)∉edges (αg g); u≠v⟧ 
      ⟹ αw (add_edge (u,v) d g) = (αw g)({u,v}:=d)"
  
begin

lemmas wgraph_specs = adj_correct empty_correct add_edge_correct

lemma empty_spec_presentation: 
  "invar empty ∧ αg empty = graph {} {} ∧ αw empty = (λ_. 0)"
  by (auto simp: wgraph_specs)

lemma add_edge_spec_presentation:
  "⟦invar g; (u,v)∉edges (αg g); u≠v⟧ ⟹
    invar (add_edge (u,v) d g)
  ∧ αg (add_edge (u,v) d g) = ins_edge (u,v) (αg g)
  ∧ αw (add_edge (u,v) d g) = (αw g)({u,v}:=d)"
  by (auto simp: wgraph_specs)
    
end



subsection ‹Generic From-List Algorithm›

definition valid_graph_repr :: "('v×'v) list ⇒ bool" 
  where "valid_graph_repr l ⟷ (∀(u,v)∈set l. u≠v)"
  
definition graph_from_list :: "('v×'v) list ⇒ 'v ugraph"
  where "graph_from_list l = foldr ins_edge l graph_empty"

lemma graph_from_list_foldl: "graph_from_list l = fold ins_edge l graph_empty"  
  unfolding graph_from_list_def
  apply (rule foldr_fold[THEN fun_cong])
  by (auto simp: fun_eq_iff graph_eq_iff edges_ins_edge)

  
lemma nodes_of_graph_from_list: "nodes (graph_from_list l) = fst`set l ∪ snd`set l"
  apply (induction l)
  unfolding graph_from_list_def
  by auto

lemma edges_of_graph_from_list: 
  assumes valid: "valid_graph_repr l"
  shows "edges (graph_from_list l) = set l ∪ (set l)¯"
  using valid apply (induction l)
  unfolding graph_from_list_def valid_graph_repr_def
  by auto



definition "valid_weight_repr l ≡ distinct (map (uedge o fst) l)"
  
definition weight_from_list :: "(('v×'v)×nat) list ⇒ 'v set ⇒ nat" where
  "weight_from_list l ≡ foldr (λ((u,v),d) w. w({u,v}:=d)) l (λ_. 0)"

lemma graph_from_list_simps:
  "graph_from_list [] = graph_empty"
  "graph_from_list ((u,v)#l) = ins_edge (u,v) (graph_from_list l)"
  by (auto simp: graph_from_list_def)

lemma weight_from_list_simps:
  "weight_from_list [] = (λ_. 0)"  
  "weight_from_list (((u,v),d)#xs) = (weight_from_list xs)({u,v}:=d)"
  by (auto simp: weight_from_list_def)
  
lemma valid_graph_repr_simps:
  "valid_graph_repr []"
  "valid_graph_repr ((u,v)#xs) ⟷ u≠v ∧ valid_graph_repr xs"
  unfolding valid_graph_repr_def by auto

lemma valid_weight_repr_simps:
  "valid_weight_repr []"  
  "valid_weight_repr (((u,v),w)#xs) 
    ⟷ uedge (u,v)∉uedge`fst`set xs ∧ valid_weight_repr xs"
  unfolding valid_weight_repr_def
  by (force simp: uedge_def doubleton_eq_iff)+
  
  
lemma weight_from_list_correct: 
  assumes "valid_weight_repr l"
  assumes "((u,v),d)∈set l"
  shows "weight_from_list l {u,v} = d"
proof -
  from assms show ?thesis  
    apply (induction l)
    unfolding valid_weight_repr_def weight_from_list_def
    subgoal by simp
    by (force simp: doubleton_eq_iff)
    
qed    
    
  

context adt_wgraph 
begin
  
definition "valid_wgraph_repr l 
  ⟷ valid_graph_repr (map fst l) ∧ valid_weight_repr l"

definition "from_list l = foldr (λ(e,d). add_edge e d) l empty"


lemma from_list_refine: "valid_wgraph_repr l ⟹ 
    invar (from_list l) 
  ∧ αg (from_list l) = graph_from_list (map fst l)
  ∧ αw (from_list l) = weight_from_list l"
  unfolding from_list_def valid_wgraph_repr_def
  supply [simp] = wgraph_specs graph_from_list_simps weight_from_list_simps
  apply (induction l) 
  subgoal by auto
  subgoal by (
      intro conjI; 
      clarsimp 
        simp: uedge_def valid_graph_repr_simps valid_weight_repr_simps
        split: prod.splits;
      subst wgraph_specs; 
      auto simp: edges_of_graph_from_list
    )
  done  

lemma from_list_correct: 
  assumes "valid_wgraph_repr l"  
  shows 
    "invar (from_list l)"
    "nodes (αg (from_list l)) = fst`fst`set l ∪ snd`fst`set l"
    "edges (αg (from_list l)) = (fst`set l) ∪ (fst`set l)¯"
    "((u,v),d)∈set l ⟹ αw (from_list l) {u,v} = d"
    apply (simp_all add: from_list_refine[OF assms])
    using assms unfolding valid_wgraph_repr_def
    apply (simp_all add: 
      edges_of_graph_from_list nodes_of_graph_from_list weight_from_list_correct)
    done
  
lemma valid_wgraph_repr_presentation: "valid_wgraph_repr l ⟷ 
  (∀((u,v),d)∈set l. u≠v) ∧ distinct [ {u,v}. ((u,v),d)←l ]"
proof -
  have [simp]: "uedge ∘ fst = (λ((u, v), w). {u, v})"
    unfolding uedge_def by auto
  show ?thesis
    unfolding valid_wgraph_repr_def valid_graph_repr_def valid_weight_repr_def
    by (auto split: prod.splits)
qed  
    
lemma from_list_correct_presentation:
  assumes "valid_wgraph_repr l"  
  shows "let gi=from_list l; g=αg gi; w=αw gi in
      invar gi 
    ∧ nodes g = ⋃{{u,v} | u v. ∃d. ((u,v),d)∈set l}
    ∧ edges g = ⋃{{(u,v),(v,u)} | u v. ∃d. ((u,v),d)∈set l}
    ∧ (∀((u,v),d)∈set l. w {u,v}=d)
  "  
  unfolding Let_def from_list_correct(2-3)[OF assms]
  apply (intro conjI)
  subgoal by (simp add: from_list_correct(1)[OF assms])
  subgoal by (auto 0 0 simp: in_set_conv_decomp; blast)
  subgoal by (auto 0 0 simp: in_set_conv_decomp; blast) 
  subgoal using from_list_correct(4)[OF assms] by auto
  done
    
end

end