(* ID: $Id: Graph.thy,v 1.1 2006/01/04 13:43:49 nipkow Exp $
Author: Gertrud Bauer, Tobias Nipkow
*)
header {* Graph *}
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"
defs (overloaded) cong_face_def:
"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)"
by (simp add: nextVertices_def nat_number)
(*<*) 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)"
by (simp add:vertices_graph)
lemma len_vertices_graph[THEN eq_reflection, code unfold]:
"|vertices g| = countVertices g"
by (simp add:vertices_graph)
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"
by (auto simp add: finalVertex_def)
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 ≤ quad g v" by (simp add: quad_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
lemma nextV2:
f2 • v = f • (f • v)
lemma
vertices (fop) = (vertices f)op
lemma
xs ≠ [] ==> hd (rev xs) = last xs
lemma
f1op • v1 == if vertices f1 = [] then hd (vertices f1) else let vs = vertices f1 in nextElem (rev vs) (last vs) v1
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)
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
0 ≤ quad g v
lemma
0 ≤ except g v
lemma nextFace_def:
(g, v) • f == let fs = facesAt g v in case fs of [] => f | g # gs => nextElem fs (hd 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