Theory Generator

(*  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