| Quellcodebibliothek Statistik Leitseite products/Sources/formale Sprachen/Isabelle/Archive-of-Formal-Proofs/thys/Flyspeck-Tame/ (Archive of formal Proofs Version 2026-5©) Datei vom 31.4.2026 mit Größe 1 kB |
|
Quelle Plane1.thy Sprache: Isabelle |
|||||||||||||||||||||||||
|
(* Title: Plane1.thy Author: Gertrud Bauer, Tobias Nipkow Fixing a single face and vertex in each refinement step. *) theory Plane1 imports Plane begin text‹This is an optimized definition of plane graphs and the one we as our point of reference. In every step only one fixed nonfinal (the smallest one) and one edge in that face are picked.› definition minimalFace :: "face list → face" where "minimalFace ≡ minimal (length ∘ vertices)" definition minimalVertex :: "graph → face → vertex" where "minimalVertex g f ≡ minimal (height g) (vertices f)" definition next_plane :: "nat → graph → graph list" (‹next'_plane›) where "next_plane g ≡ let fs = nonFinals g in if fs = [] then [] else let f = minimalFace fs; v = minimalVertex g f in ⊔∈[3..<Suc(maxGon p)] generatePolygon i v f g" definition PlaneGraphsP :: "nat → graph set" (‹PlaneGraphs›) where "PlaneGraphs ≡ {g. Seed [next_plane]→* g ∧ final g}" definition PlaneGraphs :: "graph set" where "PlaneGraphs ≡ ∪p. PlaneGraphs" end
¤ Dauer der Verarbeitung: 0.1 Sekunden (vorverarbeitet am 2026-11-04) ¤*© Formatika GbR, Deutschland |
|
||||||||||||||||||||||||
2026-11-01