Up to index of Isabelle/HOL/Tame
theory Plane(* ID: $Id: Plane.thy,v 1.2 2006/01/09 06:56:13 nipkow Exp $
Author: Gertrud Bauer
*)
header{* Plane Graph Enumeration *}
theory Plane
imports Enumerator FaceDivision RTranCl
begin
constdefs
maxGon :: "nat => nat"
"maxGon p ≡ p+3"
declare maxGon_def [simp]
constdefs duplicateEdge :: "graph => face => vertex => vertex => bool"
"duplicateEdge g f a b ≡
2 ≤ directedLength f a b ∧ 2 ≤ directedLength f b a ∧ b mem (neighbors g a)"
consts containsUnacceptableEdgeSnd ::
"(nat => nat => bool) => nat => nat list => bool"
primrec "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)"
consts containsUnacceptableEdge :: "(nat => nat => bool) => nat list => bool"
primrec "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)"
constdefs containsDuplicateEdge :: "graph => face => vertex => nat list => bool"
"containsDuplicateEdge g f v is ≡
containsUnacceptableEdge (λi j. duplicateEdge g f (fi•v) (fj•v)) is"
constdefs containsDuplicateEdge' :: "graph => face => vertex => nat list => bool"
"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 (fi1 •v) (fi2 •v)) ∧ (i0 < i1) ∧ (i1 < i2))
∨ (let i0 = is!0; i1 = is!1 in
(duplicateEdge g f (fi0 •v) (fi1 •v)) ∧ (i0 < i1)))"
constdefs generatePolygon :: "nat => vertex => face => graph => graph list"
"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]"
constdefs next_plane0 :: "nat => graph => graph list" ("next'_plane0_")
"next_plane0p g ≡
if final g then []
else \<Squnion>f∈nonFinals g \<Squnion>v∈vertices f \<Squnion>i∈[3..maxGon p] generatePolygon i v f g"
constdefs Seed :: "nat => graph" ("Seed_")
"Seedp ≡ graph(maxGon p)"
lemma Seed_not_final[iff]: "¬ final (Seed p)"
by(simp add:Seed_def graph_def finalGraph_def nonFinals_def)
constdefs
PlaneGraphs0 :: "graph set"
"PlaneGraphs0 ≡ \<Union>p. {g. Seedp [next_plane0p]->* g ∧ final g}"
end
lemma Seed_not_final:
¬ final Seedp