Theory Generator

Up to index of Isabelle/HOL/Tame

theory Generator
imports Vector Plane1 Tame
begin

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