(* 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