Theory Directed_Graph_Impl

section ‹Weighted Digraph Implementation by Adjacency Map›
theory Directed_Graph_Impl
imports 
  Directed_Graph_Specs
  "HOL-Data_Structures.Map_Specs"
begin

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 ⇒ ((nat×'v) list) option" and M_invar 
begin

definition α :: "'m ⇒ ('v) wgraph" where
  "α g ≡ λ(u,v). case M_lookup g u of 
    None ⇒ ∞ 
  | Some l ⇒ if ∃d. (d,v)∈set l then enat (SOME d. (d,v)∈set l) else ∞"

definition invar :: "'m ⇒ bool" where "invar g ≡ 
    M_invar g 
  ∧ (∀l∈ran (M_lookup g). distinct (map snd l)) 
  ∧ finite (WGraph.edges (α g))"

definition succ :: "'m ⇒ 'v ⇒ (nat × 'v) list" where
  "succ g v = the_default [] (M_lookup g v)"
  
definition empty_graph :: "'m" where "empty_graph = M_empty"

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

sublocale adt_finite_wgraph invar succ empty_graph add_edge α
  apply unfold_locales
  subgoal for g u 
    by (cases "M_lookup g u")
       (auto 
          simp: invar_def α_def succ_def ran_def
          intro: distinct_map_snd_inj someI
          split: option.splits
        )
  subgoal by (auto 
                simp: invar_def α_def empty_graph_def add_edge_def M.map_specs 
                split: option.split)
  subgoal by (auto 
                simp: invar_def α_def empty_graph_def add_edge_def M.map_specs 
                split: option.split)
proof -    
  text ‹Explicit proof to nicely handle finiteness constraint, using already
     proved shape of abstract result›
  fix g e d
  assume A: "invar g" "α g e = ∞"
  then show AAE: "α (add_edge e d g) = (α g)(e := enat d)"
    by (auto 
      simp: invar_def α_def add_edge_def M.map_specs
      split: option.splits if_splits prod.splits
    )
  
  from A show "invar (add_edge e d g)"  
    apply (simp add: invar_def AAE)
    by (force
      simp: invar_def α_def empty_graph_def add_edge_def M.map_specs ran_def
      split: option.splits if_splits prod.splits)      
qed (simp add: invar_def)     

end  

end