Theory Plane

(*  Author:     Gertrud Bauer
*)

section‹Plane Graph Enumeration›

theory Plane
imports Enumerator FaceDivision RTranCl
begin


definition maxGon :: "nat ⇒ nat" where
"maxGon p ≡ p+3"

declare maxGon_def [simp]


definition duplicateEdge :: "graph ⇒ face ⇒ vertex ⇒ vertex ⇒ bool" where
 "duplicateEdge g f a b ≡ 
  2 ≤ directedLength f a b ∧ 2 ≤ directedLength f b a ∧ b ∈ set (neighbors g a)"

primrec containsUnacceptableEdgeSnd :: 
      "(nat ⇒ nat ⇒ bool) ⇒ nat ⇒ nat list ⇒ bool" where
 "containsUnacceptableEdgeSnd N v [] = False" |
 "containsUnacceptableEdgeSnd N v (w#ws) = 
     (case ws of [] ⇒ False
         | (w'#ws') ⇒ if v < w ∧ w < w' ∧ N w w' then True
                      else containsUnacceptableEdgeSnd N w ws)"

primrec containsUnacceptableEdge :: "(nat ⇒ nat ⇒ bool) ⇒ nat list ⇒ bool" where
 "containsUnacceptableEdge N [] = False" |
 "containsUnacceptableEdge N (v#vs) =
     (case vs of [] ⇒ False
           | (w#ws) ⇒ if v < w ∧ N v w then True
                      else containsUnacceptableEdgeSnd N v vs)"

definition containsDuplicateEdge :: "graph ⇒ face ⇒ vertex ⇒ nat list ⇒ bool" where
 "containsDuplicateEdge g f v is ≡ 
     containsUnacceptableEdge (λi j. duplicateEdge g f (f⇗i⇖∙v) (f⇗j⇖∙v)) is" 

definition containsDuplicateEdge' :: "graph ⇒ face ⇒ vertex ⇒ nat list ⇒ bool" where
 "containsDuplicateEdge' g f v is ≡ 
  2 ≤ |is| ∧ 
  ((∃k < |is| - 2. let i0 = is!k; i1 = is!(k+1); i2 = is!(k+2) in
    (duplicateEdge g f (f⇗i1 ⇖∙v) (f⇗i2 ⇖∙v)) ∧ (i0 < i1) ∧ (i1 < i2))
  ∨ (let i0 = is!0; i1 = is!1 in
    (duplicateEdge g f (f⇗i0 ⇖∙v) (f⇗i1 ⇖∙v)) ∧ (i0 < i1)))" 


definition generatePolygon :: "nat ⇒ vertex ⇒ face ⇒ graph ⇒ graph list" where
 "generatePolygon n v f g ≡ 
     let enumeration = enumerator n |vertices f|;
     enumeration = [is ← enumeration. ¬ containsDuplicateEdge g f v is];
     vertexLists = [indexToVertexList f v is. is ← enumeration] in
     [subdivFace g f vs. vs ← vertexLists]"

definition next_plane0 :: "nat ⇒ graph ⇒ graph list" (‹next'_plane0⇘_⇙›) where
 "next_plane0⇘p⇙ g ≡
     if final g then [] 
     else ⨆⇘f∈nonFinals g⇙ ⨆⇘v∈vertices f⇙ ⨆⇘i∈[3..<Suc(maxGon p)]⇙ generatePolygon i v f g"


definition Seed :: "nat ⇒ graph" (‹Seed⇘_⇙›) where
  "Seed⇘p⇙ ≡ graph(maxGon p)"

lemma Seed_not_final[iff]: "¬ final (Seed p)"
by(simp add:Seed_def graph_def finalGraph_def nonFinals_def)

definition PlaneGraphs0 :: "graph set" where 
"PlaneGraphs0 ≡ ⋃p. {g. Seed⇘p⇙ [next_plane0⇘p⇙]→* g ∧ final g}"

end