Theory Graph

(*  Author:     Gertrud Bauer, Tobias Nipkow
*)

section ‹Graph›

theory Graph
imports Rotation
begin

syntax
  "_UNION1"     :: "pttrns  'b set  'b set"           ("(3(‹unbreakable›_)/ _)" [0, 10] 10)
  "_INTER1"     :: "pttrns  'b set  'b set"           ("(3(‹unbreakable›_)/ _)" [0, 10] 10)
  "_UNION"      :: "pttrn  'a set  'b set  'b set"  ("(3(‹unbreakable›__)/ _)" [0, 0, 10] 10)
  "_INTER"      :: "pttrn  'a set  'b set  'b set"  ("(3(‹unbreakable›__)/ _)" [0, 0, 10] 10)


subsection‹Notation›

type_synonym vertex = "nat"

consts
  vertices :: "'a  vertex list"
  edges :: "'a  (vertex × vertex) set" ("")

abbreviation vertices_set :: "'a  vertex set" ("𝒱") where
  "𝒱 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"
  cong_face  "pr_isomorphic :: face  face  bool"
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"

definition cong_face :: "face  face  bool"
  where "(f1 :: face)  f2  vertices f1  vertices f2"

end

text ‹The following operation makes a face final.›

definition setFinal :: "face  face" where
  "setFinal f  Face (vertices f) Final"


text ‹The function nextVertex› (written f ∙ v›) is based on
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 nextVertices› is $n$-fold application of
nextvertex›.›

definition nextVertices :: "face  nat  vertex  vertex" (*<*)("__  _" [100, 0, 100]) (*>*)where (* *)
  "fn v  (f  ^^ n) v"

lemma nextV2: "f2v = f (f v)"
by (simp add: nextVertices_def eval_nat_numeral)

(*<*)
overloading edges_face  "edges :: face  (vertex × vertex) set"
begin
  definition " f  {(a, f  a)|a. a  𝒱 f}"
end
(*>*)

(*<*)consts op :: "'a  'a" ("_op" [1000] 999)  (*>*) (* *)
overloading op_vertices  "Graph.op :: vertex list  vertex list"
begin
  definition "(vs::vertex list)op  rev vs"
end

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" ("") where
  " 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  faces g. final f]"

definition nonFinals :: "graph  face list" where
  "nonFinals g  [f  faces g. ¬ final f]"

definition countNonFinals :: "graph  nat" where
  "countNonFinals g  |nonFinals g|"

overloading finalGraph  "final :: graph  bool"
begin
  definition "finalGraph g  (nonFinals g = [])"
end

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  facesAt g v. final f  |vertices f| = 3]|"

definition quad :: "graph  vertex  nat" where
 "quad g v  |[f  facesAt g v. final f  |vertices f| = 4]|"

definition except :: "graph  vertex  nat" where
 "except g v  |[f  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$.›
(*>*)
overloading edges_graph  "edges :: graph  (vertex × vertex) set"
begin
  definition " (g::graph)  f   gedges f"
end

definition neighbors :: "graph  vertex  vertex list" where
 "neighbors g v  [fv. f  facesAt g v]"


subsection ‹Navigation in graphs›

text ‹
The function $s'$ permutating the faces at a vertex,
is implemeted by the function 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))"  (*>*)


(* precondition a b in 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