(* ID: $Id: Generator.thy,v 1.3 2006/01/11 19:40:43 nipkow Exp $ Author: Gertrud Bauer, Tobias Nipkow *) header {* Enumeration of Tame Plane Graphs *} theory Generator imports Vector Plane1 Tame begin text{* \paragraph{Lower bounds for total weight} *} constdefs faceSquanderLowerBound :: "graph => nat" "faceSquanderLowerBound g ≡ ∑f ∈ finals g \<d> |vertices f|" constdefs d3_const :: nat "d3_const == \<d> 3" d4_const :: nat "d4_const == \<d> 4" excessAtType :: "nat => nat => nat => nat" "excessAtType t q e ≡ if e = 0 then if 6 < t + q then squanderTarget else \<b> t q - t * d3_const - q * d4_const else if t + q + e ≠ 5 then 0 else \<a> t" declare d3_const_def[simp] d4_const_def[simp] constdefs ExcessAt :: "graph => vertex => nat" "ExcessAt g v ≡ if ¬ finalVertex g v then 0 else excessAtType (tri g v) (quad g v) (except g v)" constdefs ExcessTable :: "graph => vertex list => (vertex × nat) list" "ExcessTable g vs ≡ [(v, ExcessAt g v). v ∈ [v ∈ vs. 0 < ExcessAt g v ]]" text{* Implementation: *} lemma [code]: "ExcessTable g = filtermap (λv. let e = ExcessAt g v in if 0 < e then Some (v, e) else None)" by (rule ext) (simp add: ExcessTable_def filtermap_conv) (* FIXME delete stupid removeKeyList *) constdefs deleteAround :: "graph => vertex => (vertex × nat) list => (vertex × nat) list" "deleteAround g v ps ≡ let fs = facesAt g v; ws = \<Squnion>f∈fs if |vertices f| = 4 then [f•v, f2•v] else [f•v] in removeKeyList ws ps" (*<*) text{* Implementation: *} lemma [code]: "deleteAround g v ps = (let vs = (λf. let n = f•v in if |vertices f| = 4 then [n, f•n] else [n]) in removeKeyList (concat(map vs (facesAt g v))) ps)" by (simp only: Let_def deleteAround_def nextV2) lemma length_deleteAround: "length (deleteAround g v ps) ≤ length ps" by (auto simp only: deleteAround_def length_removeKeyList Let_def) consts ExcessNotAtRec :: "(nat, nat) table => graph => nat" recdef ExcessNotAtRec "measure (λps. size ps)" "ExcessNotAtRec [] = (%g. 0)" "ExcessNotAtRec (p#ps) = (%g. max (ExcessNotAtRec ps g) (snd p + ExcessNotAtRec (deleteAround g (fst p) ps) g))" (hints recdef_simp: less_Suc_eq_le length_deleteAround) constdefs ExcessNotAt :: "graph => vertex option => nat" "ExcessNotAt g v_opt ≡ let ps = ExcessTable g (vertices g) in case v_opt of None => ExcessNotAtRec ps g | Some v => ExcessNotAtRec (deleteAround g v ps) g" (*<*) constdefs squanderLowerBound :: "graph => nat" "squanderLowerBound g ≡ faceSquanderLowerBound g + ExcessNotAt g None" text{* \paragraph{Tame graph enumeration} *} constdefs makeTrianglesFinal :: "graph => graph" "makeTrianglesFinal g ≡ foldl (%g f. makeFaceFinal f g) g [f ∈ faces g. ¬ final f ∧ triangle f]" constdefs is_tame7 :: "graph => bool" "is_tame7 g ≡ squanderLowerBound g < squanderTarget" notame :: "graph => bool" "notame g ≡ ¬ (tame45 g ∧ is_tame7 g)" generatePolygonTame :: "nat => vertex => face => graph => graph list" "generatePolygonTame n v f g ≡ let enumeration = enum n |vertices f|; enumeration = [is ∈ enumeration. ¬ containsDuplicateEdge g f v is]; vertexLists = [indexToVertexList f v is. is ∈ enumeration] in [g' ∈ [subdivFace g f vs. vs ∈ vertexLists] . ¬ notame g']" constdefs polysizes :: "nat => graph => nat list" "polysizes p g ≡ let lb = squanderLowerBound g in [n ∈ [3 .. maxGon p]. lb + \<d> n < squanderTarget]" constdefs next_tame0 :: "nat => graph => graph list" ("next'_tame0_") "next_tame0p g ≡ let fs = nonFinals g in if fs = [] then [] else let f = minimalFace fs; v = minimalVertex g f in \<Squnion>i ∈ polysizes p g generatePolygonTame i v f g" next_tame1 :: "nat => graph => graph list" ("next'_tame1_") "next_tame1p ≡ map makeTrianglesFinal o next_tame0p" text{*\noindent Extensionally, @{const next_tame0} is just @{term"filter P o next_plane p"} for some suitable @{text P}. But efficiency suffers considerably if we first create many graphs and then filter out the ones not in @{const polysizes}. *} end
lemma
ExcessTable g = filtermap (λv. let e = ExcessAt g v in if 0 < e then Some (v, e) else None)
lemma
deleteAround g v ps = (let vs = λf. let n = f • v in if |vertices f| = 4 then [n, f • n] else [n] in removeKeyList (concat (map vs (facesAt g v))) ps)
lemma length_deleteAround:
|deleteAround g v ps| ≤ |ps|