# Theory Graph

```section ‹Address Graph›

theory Graph
imports Main
begin

text ‹
This theory introduces the graph to be marked as a relation next on
nodes (addresses). We assume that we have a special node nil (the
null address). We have a node root from which we start marking the graph.
We also assume that nil is not related by next to any node and any node is
not related by next to nil.
›

locale node =
fixes nil    :: "'node"
fixes root   :: "'node"

locale graph = node +
fixes "next" :: "('node × 'node) set"
assumes next_not_nil_left: "(!! x . (nil, x) ∉ next)"
assumes next_not_nil_right: "(!! x . (x, nil) ∉ next)"
begin

text ‹
On lists of nodes we introduce two operations similar to
existing hd and tl for getting the head and the tail of
a list. The new function head applied to a nonempty list
returns the head of the list, and it reurns nil when
applied to the empty list. The function tail returns the
tail of the list when applied to a non-empty list, and
it returns the empty list otherwise.
›
definition
"head S ≡ (if S = [] then nil else (hd S))"

definition
"tail (S::'a list) ≡ (if S = [] then [] else (tl S))"

lemma [simp]: "((nil, x) ∈ next) = False"

lemma [simp]: "((x, nil) ∈ next) = False"

"(head S ≠ nil) = (head S = hd S ∧ tail S = tl S ∧ hd S ≠ nil ∧ S ≠ [])"

"head (x # S) = x"

theorem nonempty_tail [simp]:
"tail (x # S) = S"

definition (in graph)
"reach x ≡ {y . (x, y) ∈ next⇧* ∧ y ≠ nil}"

theorem (in graph) reach_nil [simp]: "reach nil = {}"