(*  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" (‹E›)

abbreviation vertices_set :: "'a → vertex set" (‹V›) where
  "V f ≡ set (vertices f)"


subsection ‹Faces›

text ‹
  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₁ :: face) ≅ f₂ ≡ vertices f₁ ≅ vertices f₂"

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" (*<*)(\<open>_ \<bullet>\<close> [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" (*<*)(\<open>_\<^bsup>_\<^esup> \<bullet> _\<close> [100, 0, 100]) (*>*)where (* *)
  "f ∙ v ≡ (f ∙ ^^ n) v"

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

(*<*)
overloading edges_face ≡ "edges :: face → (vertex × vertex) set"
begin
  definition "E f ≡ {(a, f ∙ a)|a. a ∈ V f}"
end
(*>*)

(*<*)consts op :: "'a \<Rightarrow> 'a" (\<open>_\<^bsup>op\<^esup>\<close> [1000] 999)  (*>*) (* *)
overloading op_vertices ≡ "Graph.op :: vertex list → vertex list"
begin
  definition "(vs::vertex list) ≡ rev vs"
end

overloading op_graph ≡ "Graph.op :: face → face"
begin
  primrec op_graph where "(Face vs f) = Face (rev vs) f"
end

(*<*)
lemma [simp]: "vertices ((f::face)) = (vertices f)"
  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" (*<*)(\<open>_\<^bsup>-1\<^esup> \<bullet>\<close> [100]) (*>*)where (* *)
  "f¹ ∙ 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" (‹F›) where
  "F 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 "E (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›
\<close>

definition nextFace :: "definition nextFace :: "graph \<times> vertex \<Rightarrow> face \<Rightarrow> face" (*<*)(‹_ ∙›) (*>*)where
(*<*) nextFace_def_aux: "p \<bullet> \<equiv> \<lambda>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 [code_abbrev]: "final_face = final"

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 [code_abbrev]: "final_graph = final"

lemma final_graph_code [code]: "final_graph g = List.null (nonFinals g)"
  by (simp add: final_graph_code_def finalGraph_def)

definition vertices_face :: "face → vertex list" where
  vertices_face_code_def [code_abbrev]: "vertices_face = vertices"

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 [code_abbrev]: "vertices_graph = vertices"

lemma vertices_graph_code [code]:
  "vertices_graph (Graph fs n f h) = [0 ..< n]"
  unfolding vertices_graph_code_def by simp

end