header {* Graph *}
theory Graph
imports Rotation
begin
syntax (xsymbols)
"_UNION1" :: "pttrns => 'b set => 'b set" ("(3\<Union>(00⇘_⇙)/ _)" [0, 10] 10)
"_INTER1" :: "pttrns => 'b set => 'b set" ("(3\<Inter>(00⇘_⇙)/ _)" [0, 10] 10)
"_UNION" :: "pttrn => 'a set => 'b set => 'b set" ("(3\<Union>(00⇘_∈_⇙)/ _)" [0, 0, 10] 10)
"_INTER" :: "pttrn => 'a set => 'b set => 'b set" ("(3\<Inter>(00⇘_∈_⇙)/ _)" [0, 0, 10] 10)
subsection{* Notation *}
type_synonym vertex = "nat"
consts
vertices :: "'a => vertex list"
edges :: "'a => (vertex × vertex) set" ("\<E>")
abbreviation vertices_set :: "'a => vertex set" ("\<V>") where
"\<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"
consts type :: "'a => facetype"
overloading
final_face ≡ "final :: face => bool"
type_face ≡ "type :: face => facetype"
vertices_face ≡ "vertices :: face => vertex list"
begin
primrec final_face where
"final (Face vs f) = (case f of Final => True | Nonfinal => False)"
primrec type_face where
"type (Face vs f) = f"
primrec vertices_face where
"vertices (Face vs f) = vs"
end
defs (overloaded) cong_face_def:
"f⇣1 ≅ (f⇣2::face) ≡ vertices f⇣1 ≅ vertices f⇣2"
text {* The following operation makes a face final. *}
definition setFinal :: "face => face" where
"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. *}
primrec nextElem :: "'a list => 'a => 'a => 'a" where
"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)"
definition nextVertex :: "face => vertex => vertex" ("_ •" [999]) where
"f • ≡ let vs = vertices f in nextElem vs (hd vs)"
text {* @{text nextVertices} is $n$-fold application of
@{text nextvertex}. *}
definition nextVertices :: "face => nat => vertex => vertex" ("_⇗_⇖ • _" [100, 0, 100]) where
"f⇗n⇖ • v ≡ (f • ^^ n) v"
lemma nextV2: "f⇗2⇖•v = f• (f• v)"
by (simp add: nextVertices_def eval_nat_numeral)
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"
overloading
op_graph ≡ "Graph.op :: face => face"
begin
primrec op_graph where "(Face vs f)⇗op⇖ = Face (rev vs) f"
end
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
definition prevVertex :: "face => vertex => vertex" ("_⇗-1⇖ •" [100]) where
"f⇗-1⇖ • v ≡ (let vs = vertices f in nextElem (rev vs) (last vs) v)"
abbreviation
triangle :: "face => bool" where
"triangle f == |vertices f| = 3"
subsection {* Graphs *}
datatype graph = Graph "(face list)" "nat" "face list list" "nat list"
primrec faces :: "graph => face list" where
"faces (Graph fs n f h) = fs"
abbreviation
Faces :: "graph => face set" ("\<F>") where
"\<F> g == set(faces g)"
primrec countVertices :: "graph => nat" where
"countVertices (Graph fs n f h) = n"
overloading
vertices_graph ≡ "vertices :: graph => vertex list"
begin
primrec vertices_graph where "vertices (Graph fs n f h) = [0 ..< n]"
end
lemma vertices_graph: "vertices g = [0 ..< countVertices g]"
by (induct g) simp
lemma in_vertices_graph:
"v ∈ set (vertices g) = (v < countVertices g)"
by (simp add:vertices_graph)
lemma len_vertices_graph:
"|vertices g| = countVertices g"
by (simp add:vertices_graph)
primrec faceListAt :: "graph => face list list" where
"faceListAt (Graph fs n f h) = f"
definition facesAt :: "graph => vertex => face list" where
"facesAt g v ≡ (*if v ∈ set(vertices g) then*) faceListAt g ! v (*else []*)"
primrec heights :: "graph => nat list" where
"heights (Graph fs n f h) = h"
definition height :: "graph => vertex => nat" where
"height g v ≡ heights g ! v"
definition graph :: "nat => graph" where
"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 *}
definition finals :: "graph => face list" where
"finals g ≡ [f \<leftarrow> faces g. final f]"
definition nonFinals :: "graph => face list" where
"nonFinals g ≡ [f \<leftarrow> faces g. ¬ final f]"
definition countNonFinals :: "graph => nat" where
"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)
definition finalVertex :: "graph => vertex => bool" where
"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"
by (auto simp add: finalVertex_def)
text {* counting faces *}
definition degree :: "graph => vertex => nat" where
"degree g v ≡ |facesAt g v|"
definition tri :: "graph => vertex => nat" where
"tri g v ≡ |[f \<leftarrow> facesAt g v. final f ∧ |vertices f| = 3]|"
definition quad :: "graph => vertex => nat" where
"quad g v ≡ |[f \<leftarrow> facesAt g v. final f ∧ |vertices f| = 4]|"
definition except :: "graph => vertex => nat" where
"except g v ≡ |[f \<leftarrow> facesAt g v. final f ∧ 5 ≤ |vertices f| ]|"
definition vertextype :: "graph => vertex => nat × nat × nat" where
"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 ≤ quad g v" by (simp add: quad_def)
lemma[simp]: "0 ≤ except g v" by (simp add: except_def)
definition exceptionalVertex :: "graph => vertex => bool" where
"exceptionalVertex g v ≡ except g v ≠ 0"
definition noExceptionals :: "graph => vertex set => bool" where
"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"
definition neighbors :: "graph => vertex => vertex list" where
"neighbors g v ≡ [f•v. f \<leftarrow> facesAt g v]"
subsection {* Navigation in graphs *}
text {*
The function $s'$ permutating the faces at a vertex,
is implemeted by the function @{text nextFace}
*}
definition nextFace :: "graph × vertex => face => face" ("_ •") where
nextFace_def_aux: "p • ≡ λf. (let (g,v) = p; fs = (facesAt g v) in
(case fs of [] => f
| g#gs => nextElem fs (hd fs) f))"
definition directedLength :: "face => vertex => vertex => nat" where
"directedLength f a b ≡
if a = b then 0 else |(between (vertices f) a b)| + 1"
subsection {* Code generator setup *}
definition final_face :: "face => bool" where
final_face_code_def: "final_face = final"
declare final_face_code_def [symmetric, code_unfold]
lemma final_face_code [code]:
"final_face (Face vs Final) <-> True"
"final_face (Face vs Nonfinal) <-> False"
by (simp_all add: final_face_code_def)
definition final_graph :: "graph => bool" where
final_graph_code_def: "final_graph = final"
declare final_graph_code_def [symmetric, code_unfold]
lemma final_graph_code [code]: "final_graph g = List.null (nonFinals g)"
unfolding final_graph_code_def finalGraph_def null_def ..
definition vertices_face :: "face => vertex list" where
vertices_face_code_def: "vertices_face = vertices"
declare vertices_face_code_def [symmetric, code_unfold]
lemma vertices_face_code [code]: "vertices_face (Face vs f) = vs"
unfolding vertices_face_code_def by simp
definition vertices_graph :: "graph => vertex list" where
vertices_graph_code_def: "vertices_graph = vertices"
declare vertices_graph_code_def [symmetric, code_unfold]
lemma vertices_graph_code [code]:
"vertices_graph (Graph fs n f h) = [0 ..< n]"
unfolding vertices_graph_code_def by simp
end