# Theory GraphSpec

```section "Graph Interface"
theory GraphSpec
imports Main Graph
Collections.Collections
(*"../Collections/Lib/Proper_Iterator"*)
begin
text ‹
This theory defines an ICF-style interface for graphs.
›

type_synonym ('V,'W,'G) graph_α = "'G ⇒ ('V,'W) graph"

locale graph =
fixes α :: "'G ⇒ ('V,'W) graph"
fixes invar :: "'G ⇒ bool"
assumes finite[simp, intro!]:
"invar g ⟹ finite (nodes (α g))"
"invar g ⟹ finite (edges (α g))"
assumes valid: "invar g ⟹ valid_graph (α g)"

type_synonym ('V,'W,'G) graph_empty = "unit ⇒ 'G"
locale graph_empty = graph +
constrains α :: "'G ⇒ ('V,'W) graph"
fixes empty :: "unit ⇒ 'G"
assumes empty_correct:
"α (empty ()) = Graph.empty"
"invar (empty ())"

type_synonym ('V,'W,'G) graph_add_node = "'V ⇒ 'G ⇒ 'G"
constrains α :: "'G ⇒ ('V,'W) graph"
fixes add_node :: "'V ⇒ 'G ⇒ 'G"
"invar g ⟹ invar (add_node v g)"
"invar g ⟹ α (add_node v g) = Graph.add_node v (α g)"

type_synonym ('V,'W,'G) graph_delete_node = "'V ⇒ 'G ⇒ 'G"
locale graph_delete_node = graph +
constrains α :: "'G ⇒ ('V,'W) graph"
fixes delete_node :: "'V ⇒ 'G ⇒ 'G"
assumes delete_node_correct:
"invar g ⟹ invar (delete_node v g)"
"invar g ⟹ α (delete_node v g) = Graph.delete_node v (α g)"

type_synonym ('V,'W,'G) graph_add_edge = "'V ⇒'W ⇒ 'V ⇒ 'G ⇒ 'G"
constrains α :: "'G ⇒ ('V,'W) graph"
fixes add_edge :: "'V ⇒ 'W ⇒ 'V ⇒ 'G ⇒ 'G"
"invar g ⟹ invar (add_edge v e v' g)"
"invar g ⟹ α (add_edge v e v' g) = Graph.add_edge v e v' (α g)"

type_synonym ('V,'W,'G) graph_delete_edge = "'V ⇒'W ⇒ 'V ⇒ 'G ⇒ 'G"
locale graph_delete_edge = graph +
constrains α :: "'G ⇒ ('V,'W) graph"
fixes delete_edge :: "'V ⇒ 'W ⇒ 'V ⇒ 'G ⇒ 'G"
assumes delete_edge_correct:
"invar g ⟹ invar (delete_edge v e v' g)"
"invar g ⟹ α (delete_edge v e v' g) = Graph.delete_edge v e v' (α g)"

type_synonym ('V,'W,'σ,'G) graph_nodes_it = "'G ⇒ ('V,'σ) set_iterator"

locale graph_nodes_it_defs =
fixes nodes_list_it :: "'G ⇒ ('V,'V list) set_iterator"
begin
definition "nodes_it g ≡ it_to_it (nodes_list_it g)"
end

locale graph_nodes_it = graph α invar + graph_nodes_it_defs nodes_list_it
for α :: "'G ⇒ ('V,'W) graph" and invar and
nodes_list_it :: "'G ⇒ ('V,'V list) set_iterator"
+
assumes nodes_list_it_correct:
"invar g ⟹ set_iterator (nodes_list_it g) (Graph.nodes (α g))"
begin
lemma nodes_it_correct:
"invar g ⟹ set_iterator (nodes_it g) (Graph.nodes (α g))"
unfolding nodes_it_def
apply (rule it_to_it_correct)
by (rule nodes_list_it_correct)

lemma pi_nodes_it[icf_proper_iteratorI]:
"proper_it (nodes_it S) (nodes_it S)"
unfolding nodes_it_def
by (intro icf_proper_iteratorI)

lemma nodes_it_proper[proper_it]:
"proper_it' nodes_it nodes_it"
apply (rule proper_it'I)
by (rule pi_nodes_it)

end

type_synonym ('V,'W,'σ,'G) graph_edges_it
= "'G ⇒ (('V×'W×'V),'σ) set_iterator"

locale graph_edges_it_defs =
fixes edges_list_it :: "('V,'W,('V×'W×'V) list,'G) graph_edges_it"
begin
definition "edges_it g ≡ it_to_it (edges_list_it g)"
end

locale graph_edges_it = graph α invar + graph_edges_it_defs edges_list_it
for α :: "'G ⇒ ('V,'W) graph" and invar and
edges_list_it :: "('V,'W,('V×'W×'V) list,'G) graph_edges_it"
+
assumes edges_list_it_correct:
"invar g ⟹ set_iterator (edges_list_it g) (Graph.edges (α g))"
begin
lemma edges_it_correct:
"invar g ⟹ set_iterator (edges_it g) (Graph.edges (α g))"
unfolding edges_it_def
apply (rule it_to_it_correct)
by (rule edges_list_it_correct)

lemma pi_edges_it[icf_proper_iteratorI]:
"proper_it (edges_it S) (edges_it S)"
unfolding edges_it_def
by (intro icf_proper_iteratorI)

lemma edges_it_proper[proper_it]:
"proper_it' edges_it edges_it"
apply (rule proper_it'I)
by (rule pi_edges_it)

end

type_synonym ('V,'W,'σ,'G) graph_succ_it =
"'G ⇒ 'V ⇒ ('W×'V,'σ) set_iterator"

locale graph_succ_it_defs =
fixes succ_list_it :: "'G ⇒ 'V ⇒ ('W×'V,('W×'V) list) set_iterator"
begin
definition "succ_it g v ≡ it_to_it (succ_list_it g v)"
end

locale graph_succ_it = graph α invar + graph_succ_it_defs succ_list_it
for α :: "'G ⇒ ('V,'W) graph" and invar and
succ_list_it :: "'G ⇒ 'V ⇒ ('W×'V,('W×'V) list) set_iterator" +
assumes succ_list_it_correct:
"invar g ⟹ set_iterator (succ_list_it g v) (Graph.succ (α g) v)"
begin
lemma succ_it_correct:
"invar g ⟹ set_iterator (succ_it g v) (Graph.succ (α g) v)"
unfolding succ_it_def
apply (rule it_to_it_correct)
by (rule succ_list_it_correct)

lemma pi_succ_it[icf_proper_iteratorI]:
"proper_it (succ_it S v) (succ_it S v)"
unfolding succ_it_def
by (intro icf_proper_iteratorI)

lemma succ_it_proper[proper_it]:
"proper_it' (λS. succ_it S v) (λS. succ_it S v)"
apply (rule proper_it'I)
by (rule pi_succ_it)

end

type_synonym ('V,'W) adj_list = "'V list × ('V×'W×'V) list"

"adjl_α l ≡ let (nl,el) = l in ⦇
nodes = set nl ∪ fst`set el ∪ snd`snd`set el,
edges = set el
⦈"

(* TODO: Do we have naming conventions for such a lemma ? *)
apply (unfold_locales)
by force+

type_synonym ('V,'W,'G) graph_from_list = "('V,'W) adj_list ⇒ 'G"
locale graph_from_list = graph +
constrains α :: "'G ⇒ ('V,'W) graph"
fixes from_list :: "('V,'W) adj_list ⇒ 'G"
assumes from_list_correct:
"invar (from_list l)"
"α (from_list l) = adjl_α l"

type_synonym ('V,'W,'G) graph_to_list = "'G ⇒ ('V,'W) adj_list"
locale graph_to_list = graph +
constrains α :: "'G ⇒ ('V,'W) graph"
fixes to_list :: "'G ⇒ ('V,'W) adj_list"
assumes to_list_correct:
"invar g ⟹ adjl_α (to_list g) = α g"

subsection ‹Record Based Interface›
record ('V,'W,'G) graph_ops =
gop_α :: "('V,'W,'G) graph_α"
gop_invar :: "'G ⇒ bool"
gop_empty :: "('V,'W,'G) graph_empty"
gop_delete_node :: "('V,'W,'G) graph_delete_node"
gop_delete_edge :: "('V,'W,'G) graph_delete_edge"
gop_from_list :: "('V,'W,'G) graph_from_list"
gop_to_list :: "('V,'W,'G) graph_to_list"
gop_nodes_list_it :: "'G ⇒ ('V,'V list) set_iterator"
gop_edges_list_it :: "('V,'W,('V×'W×'V) list,'G) graph_edges_it"
gop_succ_list_it :: "'G ⇒ 'V ⇒ ('W×'V,('W×'V) list) set_iterator"

locale StdGraphDefs =
graph_nodes_it_defs "gop_nodes_list_it ops"
+ graph_edges_it_defs "gop_edges_list_it ops"
+ graph_succ_it_defs "gop_succ_list_it ops"
for ops :: "('V,'W,'G,'m) graph_ops_scheme"
begin
abbreviation α where "α ≡ gop_α ops"
abbreviation invar where "invar ≡ gop_invar ops"
abbreviation empty where "empty ≡ gop_empty ops"
abbreviation delete_node where "delete_node ≡ gop_delete_node ops"
abbreviation delete_edge where "delete_edge ≡ gop_delete_edge ops"
abbreviation from_list where "from_list ≡ gop_from_list ops"
abbreviation to_list where "to_list ≡ gop_to_list ops"
abbreviation nodes_list_it where "nodes_list_it ≡ gop_nodes_list_it ops"
abbreviation edges_list_it where "edges_list_it ≡ gop_edges_list_it ops"
abbreviation succ_list_it  where "succ_list_it ≡ gop_succ_list_it ops"
end

locale StdGraph = StdGraphDefs +
graph α invar +
graph_empty α invar empty +
graph_delete_node α invar delete_node +
graph_delete_edge α invar delete_edge +
graph_from_list α invar from_list +
graph_to_list α invar to_list +
graph_nodes_it α invar nodes_list_it +
graph_edges_it α invar edges_list_it +
graph_succ_it α invar succ_list_it
begin
lemmas correct = empty_correct add_node_correct delete_node_correct
from_list_correct to_list_correct

end

subsection ‹Refinement Framework Bindings›
lemma (in graph_nodes_it) nodes_it_is_iterator[refine_transfer]:
"invar g ⟹ set_iterator (nodes_it g) (nodes (α g))"
by (rule nodes_it_correct)

lemma (in graph_edges_it) edges_it_is_iterator[refine_transfer]:
"invar g ⟹ set_iterator (edges_it g) (edges (α g))"
by (rule edges_it_correct)

lemma (in graph_succ_it) succ_it_is_iterator[refine_transfer]:
"invar g ⟹ set_iterator (succ_it g v) (Graph.succ (α g) v)"
by (rule succ_it_correct)

lemma (in graph) drh[refine_dref_RELATES]: "RELATES (build_rel α invar)"

(*text {* Autodet bindings: *}

lemma (in graph_nodes_it) graph_nodes_it_t[trans_uc]:
"DETREFe g (build_rel α invar) g' ⟹
set_iterator (nodes_it g) (nodes g')"
using nodes_it_correct by auto

lemma (in graph_succ_it) graph_succ_it_t[trans_uc]:
"DETREFe g (build_rel α invar) g' ⟹ DETREFe v Id v' ⟹
set_iterator (succ_it g v) (succ g' v')"
using succ_it_correct by auto

lemma (in graph_edges_it) graph_edges_it_t[trans_uc]:
"DETREFe g (build_rel α invar) g' ⟹
set_iterator (edges_it g) (edges g')"
using edges_it_correct by auto*)

end
```