header {* Enumeration of Tame Plane Graphs *}
theory Generator
imports Plane1 Tame
begin
text{* \paragraph{Lower bounds for total weight} *}
definition faceSquanderLowerBound :: "graph => nat" where
"faceSquanderLowerBound g ≡ ∑⇘f ∈ finals g⇙ \<d> |vertices f|"
definition d3_const :: nat where
"d3_const == \<d> 3"
definition d4_const :: nat where
"d4_const == \<d> 4"
definition excessAtType :: "nat => nat => nat => nat" where
"excessAtType t q e ≡
if e = 0 then if 7 < t + q then squanderTarget
else \<b> t q - t * d3_const - q * d4_const
else if t + q + e ≠ 6 then 0
else if t=5 then \<a> else squanderTarget"
declare d3_const_def[simp] d4_const_def[simp]
definition ExcessAt :: "graph => vertex => nat" where
"ExcessAt g v ≡ if ¬ finalVertex g v then 0
else excessAtType (tri g v) (quad g v) (except g v)"
definition ExcessTable :: "graph => vertex list => (vertex × nat) list" where
"ExcessTable g vs ≡
[(v, ExcessAt g v). v \<leftarrow> [v \<leftarrow> vs. 0 < ExcessAt g v ]]"
text{* Implementation: *}
lemma [code]:
"ExcessTable g =
List.map_filter (λv. let e = ExcessAt g v in if 0 < e then Some (v, e) else None)"
by (rule ext) (simp add: ExcessTable_def map_filter_def)
definition deleteAround :: "graph => vertex => (vertex × nat) list => (vertex × nat) list" where
"deleteAround g v ps ≡
let fs = facesAt g v;
ws = \<Squnion>⇘f∈fs⇙ if |vertices f| = 4 then [f•v, f⇗2⇖•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: concat_map_singleton 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)
function ExcessNotAtRec :: "(nat, nat) table => graph => nat" where
"ExcessNotAtRec [] = (%g. 0)"
| "ExcessNotAtRec ((x, y)#ps) = (%g. max (ExcessNotAtRec ps g)
(y + ExcessNotAtRec (deleteAround g x ps) g))"
by pat_completeness auto
termination by (relation "measure size")
(auto simp add: length_deleteAround less_Suc_eq_le)
definition ExcessNotAt :: "graph => vertex option => nat" where
"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"
definition squanderLowerBound :: "graph => nat" where
"squanderLowerBound g ≡ faceSquanderLowerBound g + ExcessNotAt g None"
text{* \paragraph{Tame graph enumeration} *}
definition is_tame13a :: "graph => bool" where
"is_tame13a g ≡ squanderLowerBound g < squanderTarget"
definition notame :: "graph => bool" where
"notame g ≡ ¬ (tame10ub g ∧ tame11b g)"
definition notame7 :: "graph => bool" where
"notame7 g ≡ ¬ (tame10ub g ∧ tame11b g ∧ is_tame13a g)"
definition generatePolygonTame :: "nat => vertex => face => graph => graph list" where
"generatePolygonTame n v f g ≡
let
enumeration = enum n |vertices f|;
enumeration = [is \<leftarrow> enumeration. ¬ containsDuplicateEdge g f v is];
vertexLists = [indexToVertexList f v is. is \<leftarrow> enumeration]
in
[g' \<leftarrow> [subdivFace g f vs. vs \<leftarrow> vertexLists] . ¬ notame g']"
definition polysizes :: "nat => graph => nat list" where
"polysizes p g ≡
let lb = squanderLowerBound g in
[n \<leftarrow> [3 ..< Suc(maxGon p)]. lb + \<d> n < squanderTarget]"
definition next_tame0 :: "nat => graph => graph list" ("next'_tame0⇘_⇙") where
"next_tame0⇘p⇙ 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"
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