(* ID: $Id: Tame.thy,v 1.3 2006/01/11 19:40:45 nipkow Exp $ Author: Gertrud Bauer, Tobias Nipkow *) header{* Tameness *} 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" 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: *} 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" "admissible2 w g ≡ ∀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" "admissible3 w g ≡ ∀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" "admissible w g ≡ admissible1 w g ∧ admissible2 w g ∧ admissible3 w g" 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} %\includegraphics[scale=0.85]{graphics/quadcases} %\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 (*>*)