# Theory GraphGA

```section ‹Generic Algorithms for Graphs›
theory GraphGA
imports
GraphSpec
begin

definition gga_from_list ::
⇒ ('V,'W,'G) graph_from_list"
where
"gga_from_list e a u l ≡
let (nl,el) = l;
g1 = foldl (λg v. a v g) (e ()) nl
in foldl (λg (v,e,v'). u v e v' g) g1 el"

lemma gga_from_list_correct:
fixes α :: "'G ⇒ ('V,'W) graph"
assumes "graph_empty α invar e"
shows "graph_from_list α invar (gga_from_list e a u)"
proof -
interpret
graph_empty α invar e +
by fact+

{
fix nl el
define g1 where "g1 = foldl (λg v. a v g) (e ()) nl"
define g2 where "g2 = foldl (λg (v,e,v'). u v e v' g) g1 el"
have "invar g1 ∧ α g1 = ⦇ nodes = set nl, edges = {} ⦈"
unfolding g1_def
by (induct nl rule: rev_induct)
hence "invar g2
∧ α g2 = ⦇ nodes = set nl ∪ fst`set el ∪ snd`snd`set el,
edges = set el ⦈"
unfolding g2_def
hence "invar g2 ∧ adjl_α (nl,el) = α g2"
}
thus ?thesis
unfolding gga_from_list_def [abs_def]
apply unfold_locales
apply auto
done
qed

term map_iterator_product

locale gga_edges_it_defs =
graph_nodes_it_defs nodes_list_it +
graph_succ_it_defs succ_list_it
for nodes_list_it :: "('V,'W,'V list,'G) graph_nodes_it"
and succ_list_it :: "('V,'W,('W×'V) list,'G) graph_succ_it"
begin
definition gga_edges_list_it ::
"('V,'W,('V×'W×'V) list,'G) graph_edges_it"
where "gga_edges_list_it G ≡ set_iterator_product
(nodes_it G) (succ_it G)"
local_setup ‹Locale_Code.lc_decl_del @{term gga_edges_list_it}›
end
setup ‹
gga_edges_it_defs.gga_edges_list_it_def[abs_def]
})
›

locale gga_edges_it = gga_edges_it_defs nodes_list_it succ_list_it
+ graph α invar
+ graph_nodes_it α invar nodes_list_it
+ graph_succ_it α invar succ_list_it
for α :: "'G ⇒ ('V,'W) graph"
and invar
and nodes_list_it :: "('V,'W,'V list,'G) graph_nodes_it"
and succ_list_it :: "('V,'W,('W×'V) list,'G) graph_succ_it"
begin
lemma gga_edges_list_it_impl:
shows "graph_edges_it α invar gga_edges_list_it"
proof
fix g
assume INV: "invar g"

from set_iterator_product_correct[OF
nodes_it_correct[OF INV] succ_it_correct[OF INV]]
have "set_iterator (set_iterator_product (nodes_it g) (λv. succ_it g v))
(SIGMA v:nodes (α g). succ (α g) v)
" .
also have "(SIGMA v:nodes (α g). succ (α g) v) = edges (α g)"
unfolding succ_def
by (auto dest: valid_graph.E_validD[OF valid[OF INV]])

finally show "set_iterator (gga_edges_list_it g) (edges (α g))"
unfolding gga_edges_list_it_def .
qed
end

locale gga_to_list_defs_loc =
graph_nodes_it_defs nodes_list_it
+ graph_edges_it_defs edges_list_it
for nodes_list_it :: "('V,'W,'V list,'G) graph_nodes_it"
and edges_list_it :: "('V,'W,('V×'W×'V) list,'G) graph_edges_it"
begin
definition gga_to_list ::
"('V,'W,'G) graph_to_list"
where
"gga_to_list g ≡
(nodes_it g (λ_. True) (#) [], edges_it g (λ_. True) (#) [])
"
end

locale gga_to_list_loc = gga_to_list_defs_loc nodes_list_it edges_list_it +
graph α invar
+ graph_nodes_it α invar nodes_list_it
+ graph_edges_it α invar edges_list_it
for α :: "'G ⇒ ('V,'W) graph" and invar
and nodes_list_it :: "('V,'W,'V list,'G) graph_nodes_it"
and edges_list_it :: "('V,'W,('V×'W×'V) list,'G) graph_edges_it"
begin

lemma gga_to_list_correct:
shows "graph_to_list α invar gga_to_list"
proof
fix g
assume [simp, intro!]: "invar g"
then interpret valid_graph "α g" by (rule valid)

have "set (nodes_it g (λ_. True) (#) []) = V"
apply (rule_tac I="λit σ. set σ = V - it"
in set_iterator_rule_P[OF nodes_it_correct])
by auto
moreover have "set (edges_it g (λ_. True) (#) []) = E"
apply (rule_tac I="λit σ. set σ = E - it"
in set_iterator_rule_P[OF edges_it_correct])
by auto
ultimately show "adjl_α (gga_to_list g) = α g"