# Theory Graph

Up to index of Isabelle/HOL/Tame

theory Graph
imports Rotation
begin

(*  ID:         \$Id: Graph.thy,v 1.1 2006/01/04 13:43:49 nipkow Exp \$
Author:     Gertrud Bauer, Tobias Nipkow
*)

theory Graph
imports Rotation
begin

syntax (xsymbols)
"@UNION1"     :: "pttrns => 'b set => 'b set"           ("(3\<Union>(00_)/ _)" 10)
"@INTER1"     :: "pttrns => 'b set => 'b set"           ("(3\<Inter>(00_)/ _)" 10)
"@UNION"      :: "pttrn => 'a set => 'b set => 'b set"  ("(3\<Union>(00_∈_)/ _)" 10)
"@INTER"      :: "pttrn => 'a set => 'b set => 'b set"  ("(3\<Inter>(00_∈_)/ _)" 10)

subsection{* Notation *}

types vertex = "nat"

consts
vertices :: "'a => vertex list"
edges :: "'a => (vertex × vertex) set" ("\<E>")

syntax "_Vertices" :: "'a => vertex set" ("\<V>")
translations "\<V> f" == "set(vertices f)"

subsection {* Faces *}

text {*
We represent faces by (distinct) lists of vertices and a face type.
*}

datatype facetype = Final | Nonfinal

datatype face = Face "(vertex list)"  facetype

consts final :: "'a => bool"
primrec
"final (Face vs f) = (case f of Final => True | Nonfinal => False)"

consts type :: "'a => facetype"
primrec "type (Face vs f) = f"

primrec
"vertices (Face vs f) = vs"

"f1 ≅ (f2::face) ≡ vertices f1 ≅ vertices f2"

text {* The following operation makes a face final. *}

constdefs setFinal :: "face => face"
"setFinal f ≡ Face (vertices f) Final"

text {* The function @{text nextVertex} (written @{text "f • v"}) is based on
@{text nextElem}, that returns the successor of an element in a list.  *}

consts nextElem :: "'a list => 'a => 'a => 'a"
primrec
"nextElem [] b x = b"
"nextElem (a#as) b x =
(if x=a then (case as of [] => b | (a'#as') => a') else nextElem as b x)"

constdefs nextVertex :: "face => vertex => vertex" (*<*) ("_ •")(*>*) (* *)
"f • v ≡ let vs = vertices f in nextElem vs (hd vs) v"

text {* @{text nextVertices} is \$n\$-fold application of
@{text nextvertex}. *}

constdefs nextVertices :: "face => nat => vertex => vertex" (*<*)("__ • _")(*>*) (* *)
"fn • v ≡ ((f •)^n) v"

lemma nextV2: "f2•v = f• (f• v)"

(*<*) defs edges_face_def: (*>*)
"edges (f::face) ≡ {(a, f • a)|a. a ∈ \<V> f}"

(*<*)consts op :: "'a => 'a" ("_op" [1000] 999)  (*>*) (* *)

defs (*<*) op_vertices_def:(*>*) "(vs::vertex list)op ≡ rev vs"
primrec "(Face vs f)op = Face (rev vs) f"  (*<*)
lemma [simp]: "vertices ((f::face)op) = (vertices f)op"
by (induct f) (simp add: op_vertices_def)
lemma [simp]: "xs ≠ [] ==> hd (rev xs)= last xs"
by(induct xs) simp_all
lemma [THEN eq_reflection, code unfold]: "fop•v = (if
vertices f = [] then hd (vertices f)
else (let vs = vertices f in nextElem (rev vs) (last vs) v))"
by (simp add: nextVertex_def op_vertices_def) (*>*) (* *)

constdefs prevVertex :: "face => vertex => vertex" (*<*)("_-1 •")(*>*) (* *)
"f-1 • v ≡ (let vs = vertices f in nextElem (rev vs) (last vs) v)"

syntax triangle :: "face => bool"
translations "triangle f" == "|vertices f| = 3"

subsection {* Graphs *}

datatype graph = Graph "(face list)" "nat" "face list list" "nat list"

consts faces :: "graph => face list"
primrec "faces (Graph fs n f h) = fs"

syntax "_Faces" :: "graph => face set" ("\<F>")
translations "\<F> g" == "set(faces g)"

consts countVertices :: "graph => nat"
primrec "countVertices (Graph fs n f h) = n"

primrec "vertices (Graph fs n f h) = [0 ..< n]"

lemma vertices_graph: "vertices g = [0 ..< countVertices g]"
by (induct g) simp

lemma in_vertices_graph[THEN eq_reflection, code unfold]:
"v ∈ set (vertices g) = (v < countVertices g)"

lemma len_vertices_graph[THEN eq_reflection, code unfold]:
"|vertices g| = countVertices g"

consts faceListAt :: "graph => face list list"
primrec
"faceListAt (Graph fs n f h) = f"

constdefs facesAt :: "graph => vertex => face list"
"facesAt g v ≡ if v ∈ set(vertices g) then faceListAt g ! v else []"

consts heights :: "graph => nat list"
primrec
"heights (Graph fs n f h) = h"

constdefs height :: "graph => vertex => nat"
"height g v ≡ heights g ! v"

lemma graph_split:
"g = Graph (faces g)
(countVertices g)
(faceListAt g)
(heights g)"
by (induct g) simp

constdefs graph :: "nat => graph"
"graph n ≡
(let vs = [0 ..< n];
fs = [ Face vs Final, Face (rev vs) Nonfinal]
in (Graph fs n (replicate n fs) (replicate n 0)))"

subsection{* Operations on graphs *}

text {* final graph, final / nonfinal faces *}

constdefs finals :: "graph => face list"
"finals g ≡ [f ∈ faces g. final f]"

constdefs nonFinals :: "graph => face list"
"nonFinals g ≡ [f ∈ faces g. ¬ final f]"

constdefs countNonFinals :: "graph => nat"
"countNonFinals g ≡ |nonFinals g|"

defs finalGraph_def: "final g ≡ (nonFinals g = [])"

lemma finalGraph_faces[simp]: "final g ==> finals g = faces g"
by (simp add: finalGraph_def finals_def nonFinals_def filter_compl1)

lemma finalGraph_face: "final g ==> f ∈ set (faces g) ==> final f"
by (simp only: finalGraph_faces[symmetric]) (simp add: finals_def)

constdefs finalVertex :: "graph => vertex => bool"
"finalVertex g v ≡ ∀f ∈ set(facesAt g v). final f"

lemma finalVertex_final_face[dest]:
"finalVertex g v ==> f ∈ set (facesAt g v) ==> final f"

text {* counting faces *}

constdefs degree :: "graph => vertex => nat"
"degree g v ≡ |facesAt g v|"

constdefs tri :: "graph => vertex => nat"
"tri g v ≡ |[f: facesAt g v. final f ∧ |vertices f| = 3]|"

constdefs quad :: "graph => vertex => nat"
"quad g v ≡ |[f: facesAt g v. final f ∧ |vertices f| = 4]|"

constdefs except :: "graph => vertex => nat"
"except g v ≡ |[f: facesAt g v. final f ∧ 5 ≤ |vertices f| ]|"

constdefs vertextype :: "graph => vertex => nat × nat × nat"
"vertextype g v ≡ (tri g v, quad g v, except g v)"

lemma[simp]: "0 ≤ tri g v" by (simp add: tri_def)

lemma[simp]: "0 ≤ except g v" by (simp add: except_def)

constdefs exceptionalVertex :: "graph => vertex => bool"
"exceptionalVertex g v ≡ except g v ≠ 0"

constdefs noExceptionals :: "graph => vertex set => bool"
"noExceptionals g V ≡ (∀v ∈ V. ¬ exceptionalVertex g v)"

text {* An edge \$(a,b)\$ is contained in face f,
\$b\$ is the successor of \$a\$ in \$f\$. *}

defs edges_graph_def: (*>*)
"edges (g::graph) ≡ \<Union>f ∈ \<F> g edges f"

constdefs neighbors :: "graph => vertex => vertex list"
"neighbors g v ≡ [f•v. f ∈ facesAt g v]"

subsection {* Navigation in graphs *}

text {*
The function \$s'\$ permutating the faces at a vertex,
is implemeted by the function @{text nextFace}
*}

constdefs nextFace :: "graph × vertex => face => face" (*<*) ("_ •")(*>*)
(*<*) "p • ≡ λf. (let (g,v) = p; fs = (facesAt g v) in
(case fs of [] => f
| g#gs => nextElem fs (hd fs) f))"  (*>*)
(*<*) lemma nextFace_def: (*>*)

"(g,v) • f ≡ (let fs = (facesAt g v) in
(case fs of [] => f
| g#gs => nextElem fs (hd fs) f))"
(*<*) by (simp add: nextFace_def) (*>*)

(* Unused: *)
constdefs prevFace :: "graph × vertex => face => face" (*<*) ("_-1 •")(*>*)
(*<*) "p-1 • ≡
λf. (let (g,v) = p; fs = (facesAt g v) in
(case fs of [] => f
| g#gs => nextElem (rev fs) (last fs) f))"  (*>*)
(*<*) lemma prevFace_def: (*>*)

"(g,v)-1 • f ≡ (let fs = (facesAt g v) in
(case fs of [] => f
| g#gs => nextElem (rev fs) (last fs) f))"
(*<*) by (simp add: prevFace_def) (*>*)

(* precondition a b in f *)
constdefs directedLength :: "face => vertex => vertex => nat"
"directedLength f a b ≡
if a = b then 0 else |(between (vertices f) a b)| + 1"

end

### Faces

lemma nextV2:

f2v = f • (fv)

lemma

vertices (fop) = (vertices f)op

lemma

xs ≠ [] ==> hd (rev xs) = last xs

lemma

f1opv1 ==
if vertices f1 = [] then hd (vertices f1)
else let vs = vertices f1 in nextElem (rev vs) (last vs) v1

### Graphs

lemma vertices_graph:

vertices g = [0..<countVertices g]

lemma in_vertices_graph:

v1 ∈ \<V> g1 == v1 < countVertices g1

lemma len_vertices_graph:

|vertices g1| == countVertices g1

lemma graph_split:

g = Graph (faces g) (countVertices g) (faceListAt g) (heights g)

### Operations on graphs

lemma finalGraph_faces:

final g ==> finals g = faces g

lemma finalGraph_face:

[| final g; f ∈ \<F> g |] ==> final f

lemma finalVertex_final_face:

[| finalVertex g v; f ∈ set (facesAt g v) |] ==> final f

lemma

0 ≤ tri g v

lemma

lemma

0 ≤ except g v