header{* Tameness *}
theory Tame
imports Graph ListSum
begin
subsection {* Constants \label{sec:TameConstants}*}
definition squanderTarget :: "nat" where
"squanderTarget ≡ 15410"
definition excessTCount :: "nat" ("\<a>")where
"\<a> ≡ 6300"
definition squanderVertex :: "nat => nat => nat" ("\<b>")where
"\<b> p q ≡ if p = 0 ∧ q = 3 then 6180
else if p = 0 ∧ q = 4 then 9700
else if p = 1 ∧ q = 2 then 6560
else if p = 1 ∧ q = 3 then 6180
else if p = 2 ∧ q = 1 then 7970
else if p = 2 ∧ q = 2 then 4120
else if p = 2 ∧ q = 3 then 12851
else if p = 3 ∧ q = 1 then 3110
else if p = 3 ∧ q = 2 then 8170
else if p = 4 ∧ q = 0 then 3470
else if p = 4 ∧ q = 1 then 3660
else if p = 5 ∧ q = 0 then 400
else if p = 5 ∧ q = 1 then 11360
else if p = 6 ∧ q = 0 then 6860
else if p = 7 ∧ q = 0 then 14500
else squanderTarget"
definition squanderFace :: "nat => nat" ("\<d>")where
"\<d> n ≡ if n = 3 then 0
else if n = 4 then 2060
else if n = 5 then 4819
else if n = 6 then 7578
else squanderTarget"
text_raw{*
\index{@{text "\<a>"}}
\index{@{text "\<b>"}}
\index{@{text "\<d>"}}
*}
subsection{* Separated sets of vertices \label{sec:TameSeparated}*}
text {* A set of vertices $V$ is {\em separated},
\index{separated}
\index{@{text "separated"}}
iff the following conditions hold:
*}
text {* 2. No two vertices in V are adjacent: *}
definition separated⇣2 :: "graph => vertex set => bool" where
"separated⇣2 g V ≡ ∀v ∈ V. ∀f ∈ set (facesAt g v). f•v ∉ V"
text {* 3. No two vertices lie on a common quadrilateral: *}
definition separated⇣3 :: "graph => vertex set => bool" where
"separated⇣3 g V ≡
∀v ∈ V. ∀f ∈ set (facesAt g v). |vertices f|≤4 --> \<V> f ∩ V = {v}"
text {* A set of vertices is called {\em separated},
\index{separated} \index{@{text "separated"}}
iff no two vertices are adjacent or lie on a common quadrilateral: *}
definition separated :: "graph => vertex set => bool" where
"separated g V ≡ separated⇣2 g V ∧ separated⇣3 g V"
subsection{* Admissible weight assignments\label{sec:TameAdmissible} *}
text {*
A weight assignment @{text "w :: face => nat"}
assigns a natural number to every face.
\index{@{text "admissible"}}
\index{admissible weight assignment}
We formalize the admissibility requirements as follows:
*}
definition admissible⇣1 :: "(face => nat) => graph => bool" where
"admissible⇣1 w g ≡ ∀f ∈ \<F> g. \<d> |vertices f| ≤ w f"
definition admissible⇣2 :: "(face => nat) => graph => bool" where
"admissible⇣2 w g ≡
∀v ∈ \<V> g. except g v = 0 --> \<b> (tri g v) (quad g v) ≤ (∑⇘f∈facesAt g v⇙ w f)"
definition admissible⇣3 :: "(face => nat) => graph => bool" where
"admissible⇣3 w g ≡
∀v ∈ \<V> g. vertextype g v = (5,0,1) --> (∑⇘f∈filter triangle (facesAt g v)⇙ w(f)) >= \<a>"
text {* Finally we define admissibility of weights functions. *}
definition admissible :: "(face => nat) => graph => bool" where
"admissible w g ≡ admissible⇣1 w g ∧ admissible⇣2 w g ∧ admissible⇣3 w g"
subsection{* Tameness \label{sec:TameDef} *}
definition tame9a :: "graph => bool" where
"tame9a g ≡ ∀f ∈ \<F> g. 3 ≤ |vertices f| ∧ |vertices f| ≤ 6"
definition tame10 :: "graph => bool" where
"tame10 g = (let n = countVertices g in 13 <= n & n <= 15)"
definition tame10ub :: "graph => bool" where
"tame10ub g = (countVertices g <= 15)"
definition tame11a :: "graph => bool" where
"tame11a g = (∀v ∈ \<V> g. 3 <= degree g v)"
definition tame11b :: "graph => bool" where
"tame11b g = (∀v ∈ \<V> g. degree g v ≤ (if except g v = 0 then 7 else 6))"
definition tame12o :: "graph => bool" where
"tame12o g =
(∀v ∈ \<V> g. except g v ≠ 0 ∧ degree g v = 6 --> vertextype g v = (5,0,1))"
text {* 7. There exists an admissible weight assignment of total
weight less than the target: *}
definition tame13a :: "graph => bool" where
"tame13a g = (∃w. admissible w g ∧ (∑⇘f ∈ faces g⇙ w f) < squanderTarget)"
text {* Finally we define the notion of tameness. *}
definition tame :: "graph => bool" where
"tame g ≡ tame9a g ∧ tame10 g ∧ tame11a g ∧ tame11b g ∧ tame12o g ∧ tame13a g"
end