# Theory Tame

Up to index of Isabelle/HOL/Tame

theory Tame
imports Graph ListSum
begin

(*  ID:         $Id: Tame.thy,v 1.3 2006/01/11 19:40:45 nipkow Exp$
Author:     Gertrud Bauer, Tobias Nipkow
*)

theory Tame
imports Graph ListSum
begin

subsection {* Constants \label{sec:TameConstants}*}

constdefs squanderTarget :: "nat"
"squanderTarget ≡ 14800"

constdefs excessTCount :: "nat => nat" (*<*) ("\<a>")(*>*)

"\<a> t ≡ if t < 3 then squanderTarget
else if t = 3 then 1400
else if t = 4 then 1500
else 0"

constdefs squanderVertex :: "nat => nat => nat"  (*<*)("\<b>")(*>*)

"\<b> p q ≡ if p = 0 ∧ q = 3 then 7135
else if p = 0 ∧ q = 4 then 10649
else if p = 1 ∧ q = 2 then  6950
else if p = 1 ∧ q = 3 then  7135
else if p = 2 ∧ q = 1 then  8500
else if p = 2 ∧ q = 2 then  4756
else if p = 2 ∧ q = 3 then 12981
else if p = 3 ∧ q = 1 then  3642
else if p = 3 ∧ q = 2 then  8334
else if p = 4 ∧ q = 0 then  4139
else if p = 4 ∧ q = 1 then  3781
else if p = 5 ∧ q = 0 then   550
else if p = 5 ∧ q = 1 then 11220
else if p = 6 ∧ q = 0 then  6339
else squanderTarget"

constdefs scoreFace :: "nat => int" (*<*)("\<c>")(*>*)

"\<c> n ≡ if n = 3 then 1000
else if n = 4 then 0
else if n = 5 then -1030
else if n = 6 then -2060
else if n = 7 then -3030
else if n = 8 then -3030
else -3030"

constdefs squanderFace :: "nat => nat" (*<*)("\<d>")(*>*)

"\<d> n ≡ if n = 3 then 0
else if n = 4 then 2378
else if n = 5 then 4896
else if n = 6 then 7414
else if n = 7 then 9932
else if n = 8 then 10916
else squanderTarget"

text_raw{*
\index{@{text "\<a>"}}
\index{@{text "\<b>"}}
\index{@{text "\<c>"}}
\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 {*  1. For each vertex in $V$ there is an exceptional face
containing it: *}

constdefs separated1 :: "graph => vertex set => bool"
"separated1 g V ≡ ∀v ∈ V. except g v ≠ 0"

text {*  2. No two vertices in V are adjacent: *}

constdefs separated2 :: "graph => vertex set => bool"
"separated2 g V ≡ ∀v ∈ V. ∀f ∈ set (facesAt g v). f•v ∉ V"

text {*  3. No two vertices lie on a common quadrilateral: *}

constdefs separated3 :: "graph => vertex set => bool"
"separated3 g V ≡
∀v ∈ V. ∀f ∈ set (facesAt g v). |vertices f|≤4 --> \<V> f ∩ V = {v}"

text {*  A set of vertices  is  called {\em preseparated},
\index{preseparated} \index{@{text "preSeparated"}}
iff no two vertices are adjacent or lie on a common quadrilateral: *}

constdefs preSeparated :: "graph => vertex set => bool"
"preSeparated g V ≡ separated2 g V ∧ separated3 g V"

text {*  4. Every vertex in V has degree 5: *}

constdefs separated4 :: "graph => vertex set => bool"
"separated4 g V ≡ ∀v ∈ V. degree g v = 5"

constdefs separated :: "graph => vertex set => bool"
"separated g V ≡
separated1 g V ∧ separated2 g V ∧ separated3 g V ∧ separated4 g V"

text {*
A weight assignment @{text "w :: face => nat"}
assigns a natural number to every face.

We formalize the admissibility requirements as follows:
*}

text {*  1. $\isasymd(|f|) \leq w (f)$: *}

constdefs admissible1 :: "(face => nat) => graph => bool"
"admissible1 w g ≡ ∀f ∈ \<F> g. \<d> |vertices f| ≤ w f"

text {*  2. If $v$ has type $(p, q)$, then
$\isasymb(p, q) \leq \sum\limits_{v\in f} w(f)$: *}

constdefs admissible2 :: "(face => nat) => graph => bool"
∀v ∈ \<V> g. except g v = 0 --> \<b> (tri g v) (quad g v) ≤ ∑f∈facesAt g v w f"

text {* 4. Let $V$ be any separated set  of vertices. \\
Then  $\sum\limits_{v\in V} \isasyma(tri(v)) \leq \sum\limits_{V \cap f \neq \emptyset} (w(f) - d (|f|))$: *}
(* fixme set (vertices f) ∩ set V ≠ {} *)

constdefs admissible3 :: "(face => nat) => graph => bool"
∀V. separated g (set V) ∧ set V ⊆ \<V> g -->
(∑v∈V \<a> (tri g v))
+ (∑f∈[f∈faces g. ∃v ∈ set V. f ∈ set (facesAt g v)] \<d> |vertices f| )
≤ ∑f∈[f∈faces g. ∃v ∈ set V. f ∈ set (facesAt g v)] w f"

text {* Finally we define admissibility of weights functions. *}

constdefs admissible :: "(face => nat) => graph => bool"

subsection{* Tameness \label{sec:TameDef} *}

text {* 1. The length of each face is (at least 3 and) at most 8: *}

constdefs tame1 :: "graph => bool"
"tame1 g ≡ ∀f ∈ \<F> g. 3 ≤ |vertices f| ∧ |vertices f| ≤ 8"

text {* 2.\  Every 3-cycle is a face or the opposite of a
face: *}

text {* A face given by a vertex list @{text "vs"} is contained
in a graph $g$, if it is isomorphic to one of the faces in $g$.
The notation @{text "f ∈≅ F"} means  @{text "∃f'∈ F. f ≅ f'"},
where @{text "≅"} is the equivalence relation on faces
(see Chapter~\ref{sec:Isomorphism}).
*}

text {* The notions @{text is_path} and @{text is_cycle} are defined
locally (rather than in the theory of graphs) because no lemmas need
to be proved about them because the generation of tame graphs uses
these same executable functions as the definition of tameness. Hence
there is nothing to prove. *}

consts is_path :: "graph => vertex list => bool"
primrec
"is_path g [] = True"
"is_path g (u#vs) = (case vs of [] => True
| v#ws => v ∈ set(neighbors g u) ∧ is_path g vs)"

constdefs
is_cycle :: "graph => vertex list => bool"
"is_cycle g vs ≡ hd vs ∈ set(neighbors g (last vs)) ∧ is_path g vs"

constdefs tame2 :: "graph => bool"
"tame2 g ≡
∀a b c. is_cycle g [a,b,c] ∧ distinct [a,b,c] -->
(∃f ∈ \<F> g. vertices f ≅ [a,b,c] ∨ vertices f ≅ [c,b,a])"

text {*
3.\ Every 4-cycle surrounds one of the following configurations:\\

%\begin{center}
%\end{center}
*}

constdefs tameConf1:: "vertex => vertex => vertex => vertex => vertex list list"
"tameConf1 a b c d ≡ [[a,b,c,d]]"

constdefs tameConf2:: "vertex => vertex => vertex => vertex => vertex list list"
"tameConf2 a b c d ≡ [[a,b,c], [a,c,d]]"

constdefs tameConf3 :: "vertex => vertex => vertex => vertex => vertex => vertex list list"
"tameConf3 a b c d e ≡  [[a,b,e], [b,c,e], [a,e,c,d]]"

constdefs tameConf4 :: "vertex => vertex => vertex => vertex => vertex => vertex list list"
"tameConf4 a b c d e ≡ [[a,b,e], [b,c,e], [c,d,e], [d,a,e]]"

text {*
Given a fixed 4-cycle and using the convention of drawing faces clockwise,
a tame configuration can occur in the interior'
or on the outside of the 4-cycle.
For configuration @{text "tameConf2"} there are two possible rotations of
the triangles, for configuration
@{text "tameConf3"} there are 4.
The notation @{text "F1 ⊆≅ F2 "} means  @{text "∀f ∈ F1. f ∈≅ F2"}.

Note that our definition only ensures the existence of certain
faces in the graph, not the fact that no other  faces of the graph
may lie in the interior or on the outside. Hence it is slightly
weaker than the definition in Hales' paper.

*}

constdefs tame_quad :: "graph => vertex => vertex => vertex => vertex => bool"
"tame_quad g a b c d ≡
set(tameConf1 a b c d) ⊆≅ vertices  \<F> g
∨ set(tameConf2 a b c d) ⊆≅ vertices  \<F> g
∨ set(tameConf2 b c d a) ⊆≅ vertices  \<F> g
∨ (∃e ∈ \<V> g - {a,b,c,d}.
set(tameConf3 a b c d e) ⊆≅ vertices  \<F> g
∨ set(tameConf3 b c d a e) ⊆≅ vertices  \<F> g
∨ set(tameConf3 c d a b e) ⊆≅ vertices  \<F> g
∨ set(tameConf3 d a b c e) ⊆≅ vertices  \<F> g
∨ set(tameConf4 a b c d e) ⊆≅ vertices  \<F> g)"

constdefs tame3 :: "graph => bool"
"tame3 g ≡ ∀a b c d. is_cycle g [a,b,c,d] ∧ distinct[a,b,c,d] -->
tame_quad g a b c d ∨ tame_quad g d c b a"

text {* 4. The degree of every  vertex is at least 2 and at most 6: *}

constdefs tame45 :: "graph => bool"
"tame45 g ≡ ∀v ∈ \<V> g. degree g v ≤ (if except g v = 0 then 6 else 5)"
(*
text {*   5. If a vertex is contained in an exceptional face,
then the degree of the vertex is at most 5: *}

constdefs tame5 :: "graph => bool"
"tame5 g ≡  ∀f ∈ \<F> g. ∀v ∈ \<V> f. 5 ≤ |vertices f| --> degree g v ≤ 5"
*)
text {*  6. The following inequality holds: *}

constdefs tame6 :: "graph => bool"
"tame6 g ≡ 8000 ≤ ∑f ∈ faces g \<c> |vertices f|"

text {* This property implies that there are at least 8 triangles in a
tame graph.  *}

text {* 7. There exists an admissible weight assignment of total
weight less than the target: *}

constdefs tame7 :: "graph => bool"
"tame7 g ≡ ∃w. admissible w g ∧ ∑f ∈ faces g w f < squanderTarget"

text {* 8. We formalize the additional restriction (compared with the
original definition) that tame graphs do not contain two adjacent
vertices of type $(4,0)$: *}

constdefs type40 :: "graph => vertex => bool"
"type40 g v ≡ tri g v = 4 ∧ quad g v = 0 ∧ except g v = 0"

constdefs tame8 :: "graph => bool"
"tame8 g ≡ ¬(∃v∈ \<V> g. type40 g v ∧ (∃w∈ set(neighbors g v). type40 g w))"

text {* Finally we define the notion of tameness. *}

constdefs tame :: "graph => bool"
"tame g ≡
tame1 g ∧ tame2 g ∧ tame3 g ∧ tame45 g (*∧ tame5 g*) ∧ tame6 g ∧ tame7 g
∧ tame8 g"
(*<*)
end
(*>*)
`