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
*)

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
(*>*)

Constants \label{sec:TameConstants}

Separated sets of vertices \label{sec:TameSeparated}

Admissible weight assignments\label{sec:TameAdmissible}

Tameness \label{sec:TameDef}