Theory Directed_Graph_Specs

section ‹Abstract Datatype for Weighted Directed Graphs›
theory Directed_Graph_Specs
imports Directed_Graph
begin

locale adt_wgraph =
  fixes α :: "'g ⇒ ('v) wgraph"
    and invar :: "'g ⇒ bool"
    and succ :: "'g ⇒ 'v ⇒ (nat×'v) list"
    and empty_graph :: 'g
    and add_edge :: "'v×'v ⇒ nat ⇒ 'g ⇒ 'g"
  assumes succ_correct: "invar g ⟹ set (succ g u) = {(d,v). α g (u,v) = enat d}"
  assumes empty_graph_correct:
    "invar empty_graph"
    "α empty_graph = (λ_. ∞)"
  assumes add_edge_correct:
    "invar g ⟹ α g e = ∞ ⟹ invar (add_edge e d g)"
    "invar g ⟹ α g e = ∞ ⟹ α (add_edge e d g) = (α g)(e:=enat d)"
begin
  
lemmas wgraph_specs = succ_correct empty_graph_correct add_edge_correct
  
end

locale adt_finite_wgraph = adt_wgraph where α=α for α :: "'g ⇒ ('v) wgraph" +
  assumes finite: "invar g ⟹ finite (WGraph.edges (α g))"


subsection ‹Constructing Weighted Graphs from Lists›  
lemma edges_empty[simp]: "WGraph.edges (λ_. ∞) = {}" 
  by (auto simp: WGraph.edges_def)
  
lemma edges_insert[simp]: 
  "WGraph.edges (g(e:=enat d)) = Set.insert e (WGraph.edges g)" 
  by (auto simp: WGraph.edges_def)

text ‹A list represents a graph if there are no multi-edges or duplicate edges›
definition "valid_graph_rep l ≡ 
  (∀u d d' v. (u,v,d)∈set l ∧ (u,v,d')∈set l ⟶ d=d')
∧ distinct l
  "

text ‹Alternative characterization: all node pairs must be distinct›
lemma valid_graph_rep_code[code]: 
  "valid_graph_rep l ⟷ distinct (map (λ(u,v,_). (u,v)) l)"  
  by (auto simp: valid_graph_rep_def distinct_map inj_on_def)
  
lemma valid_graph_rep_simps[simp]:
  "valid_graph_rep []"
  "valid_graph_rep ((u,v,d) # l) ⟷ valid_graph_rep l ∧ (∀d'. (u,v,d')∉set l)"
  by (auto simp: valid_graph_rep_def)

  
text ‹For a valid graph representation, there is exactly one graph that 
  corresponds to it›  
lemma valid_graph_rep_ex1: 
  "valid_graph_rep l ⟹ ∃! w. ∀u v d. w (u,v) = enat d ⟷ (u,v,d)∈set l"  
  unfolding valid_graph_rep_code
  apply safe
  subgoal 
    apply (rule exI[where x="λ(u,v).
        if ∃d. (u,v,d)∈set l then enat (SOME d. (u,v,d)∈set l) else ∞"])
    by (auto intro: someI simp: distinct_map inj_on_def split: prod.splits; 
           blast)
  subgoal for w w'
    apply (simp add: fun_eq_iff)
    by (metis (mono_tags, opaque_lifting) not_enat_eq)
  done  

text ‹We define this graph using determinate choice›  
definition "wgraph_of_list l ≡ THE w. ∀u v d. w (u,v) = enat d ⟷ (u,v,d)∈set l"  

locale wgraph_from_list_algo = adt_wgraph 
begin

definition "from_list l ≡ fold (λ(u,v,d). add_edge (u,v) d) l empty_graph"

definition "edges_undef l w ≡ ∀u v d. (u,v,d)∈set l ⟶ w (u,v) = ∞"  
  
lemma edges_undef_simps[simp]:
  "edges_undef [] w"  
  "edges_undef l (λ_. ∞)"
  "edges_undef ((u,v,d)#l) w ⟷ edges_undef l w ∧ w (u,v) = ∞"
  "edges_undef l (w((u,v) := enat d)) ⟷ edges_undef l w ∧ (∀d'. (u,v,d')∉set l)"  
  by (auto simp: edges_undef_def)

lemma from_list_correct_aux:
  assumes "valid_graph_rep l"
  assumes "edges_undef l (α g)"
  assumes "invar g"
  defines "g' ≡ fold (λ(u,v,d). add_edge (u,v) d) l g"
  shows "invar g'"
    and "(∀u v d. α g' (u,v) = enat d ⟷ α g (u,v) = enat d ∨ (u,v,d)∈set l)"
  using assms(1-3) unfolding g'_def
  apply (induction l arbitrary: g)
  by (auto simp: wgraph_specs split: if_splits)

lemma from_list_correct':
  assumes "valid_graph_rep l"
  shows "invar (from_list l)" 
    and "(u,v,d)∈set l ⟷ α (from_list l) (u,v) = enat d"
  unfolding from_list_def 
  using from_list_correct_aux[OF assms, where g=empty_graph]
  by (auto simp: wgraph_specs)
  
lemma from_list_correct:
  assumes "valid_graph_rep l"
  shows "invar (from_list l)" "α (from_list l) = wgraph_of_list l"
proof -
  from theI'[OF valid_graph_rep_ex1[OF assms], folded wgraph_of_list_def]
  have "(wgraph_of_list l (u, v) = enat d) = ((u, v, d) ∈ set l)" for u v d 
    by blast

  then show "α (from_list l) = wgraph_of_list l" 
    using from_list_correct_aux[OF assms, where g=empty_graph]
    apply (clarsimp simp: fun_eq_iff wgraph_specs from_list_def)
    apply (metis (no_types) enat.exhaust)
    done
  
  show "invar (from_list l)"
    by (simp add: assms from_list_correct')
    
qed    
    
end



end