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 "(f⇩1 :: face) ≅ f⇩2 ≡ vertices f⇩1 ≅ vertices f⇩2"

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 (* *)
  "f⇗n⇖ ∙ v ≡ (f ∙ ^^ n) v"

lemma nextV2: "f⇗2⇖∙v = 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 ∈ ℱ g⇙ edges f"
end

definition neighbors :: "graph ⇒ vertex ⇒ vertex list" where
 "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 ‹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