Theory Graph

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