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); uv  invar (add_edge (u,v) d g)"
    "invar g; (u,v)edges (αg g); uv 
       αg (add_edge (u,v) d g) = ins_edge (u,v) (αg g)"
    "invar g; (u,v)edges (αg g); uv 
       α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); uv 
    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. uv)"
  
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)  uv  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. uv)  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