Theory Generator

(*  Author: Gertrud Bauer, Tobias Nipkow *)

section ‹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⇙ 𝖽 |vertices f|"

definition d3_const :: nat where
"d3_const == 𝖽 3"

definition  d4_const :: nat where
"d4_const == 𝖽 4"

definition excessAtType :: "nat ⇒ nat ⇒ nat ⇒ nat" where
"excessAtType t q e ≡
    if e = 0 then if 7 < t + q then squanderTarget
                  else 𝖻 t q - t * d3_const - q * d4_const
    else if t + q + e ≠ 6 then 0
         else if t=5 then 𝖺 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 ← [v ← 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)

(* FIXME delete stupid removeKeyList *)
definition deleteAround :: "graph ⇒ vertex ⇒ (vertex × nat) list ⇒ (vertex × nat) list" where
 "deleteAround g v ps ≡
      let fs = facesAt g v;
      ws = ⨆⇘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 ← enumeration. ¬ containsDuplicateEdge g f v is];
     vertexLists = [indexToVertexList f v is. is ← enumeration]
     in
     [g' ← [subdivFace g f vs. vs ← vertexLists] . ¬ notame g']"

definition polysizes :: "nat ⇒ graph ⇒ nat list" where
"polysizes p g ≡
    let lb = squanderLowerBound g in
    [n ← [3 ..< Suc(maxGon p)]. lb + 𝖽 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 ⨆⇘i ∈ polysizes p g⇙ generatePolygonTame i v f g"

text‹\noindent Extensionally, @{const next_tame0} is just
@{term"filter P ∘ next_plane p"} for some suitable ‹P›. But
efficiency suffers considerably if we first create many graphs and
then filter out the ones not in @{const polysizes}.›

end