(*  Author:     Gertrud Bauer, Tobias Nipkow
The definitions should be identical to the ones in the file
http://code.google.com/p/flyspeck/source/browse/trunk/text_formalization/tame/tame_defs.hl
by Thomas Hales. Modulo a few inessential rearrangements.
*)

section‹Tameness›

theory Tame
imports Graph ListSum
begin


subsection ‹Constants \label{sec:TameConstants}›

definition squanderTarget :: "nat" where
 "squanderTarget ≡ 15410" 

definition excessTCount :: "nat" (*<*) (\<open>\<a>\<close>)(*>*)where

 "a ≡ 6295"

definition squanderVertex :: "nat → nat → nat" (*<*)(\<open>\<b>\<close>)(*>*)where

 "b p q ≡ if p = 0 ∧ q = 3 then 6177
     else if p = 0 ∧ q = 4 then 9696
     else if p = 1 ∧ q = 2 then 6557
     else if p = 1 ∧ q = 3 then 6176
     else if p = 2 ∧ q = 1 then 7967
     else if p = 2 ∧ q = 2 then 4116
     else if p = 2 ∧ q = 3 then 12846
     else if p = 3 ∧ q = 1 then 3106
     else if p = 3 ∧ q = 2 then 8165
     else if p = 4 ∧ q = 0 then 3466
     else if p = 4 ∧ q = 1 then 3655
     else if p = 5 ∧ q = 0 then 395
     else if p = 5 ∧ q = 1 then 11354
     else if p = 6 ∧ q = 0 then 6854
     else if p = 7 ∧ q = 0 then 14493
     else squanderTarget"

definition squanderFace :: "nat → nat" (*<*)(\<open>\<d>\<close>)(*>*)where

 "d n ≡ if n = 3 then 0
     else if n = 4 then 2058
     else if n = 5 then 4819
     else if n = 6 then 7120
     else squanderTarget" 

text_raw‹
 index{‹a›}
 index{‹b›}
 index{‹d›}
 ›

subsection‹Separated sets of vertices \label{sec:TameSeparated}›


text ‹A set of vertices $V$ is {\em separated},
 index{separated}
 index{‹separated›}
  the following conditions hold:
 ›

text ‹2. No two vertices in V are adjacent:›

definition separated₂ :: "graph → vertex set → bool" where
 "separated₂ g V ≡ ∀v ∈ V. ∀f ∈ set (facesAt g v). f∙v ∉ V"

text ‹3. No two vertices lie on a common quadrilateral:›

definition separated₃ :: "graph → vertex set → bool" where
 "separated₃ 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{‹separated›}
  no two vertices are adjacent or lie on a common quadrilateral:›

definition separated :: "graph → vertex set → bool" where
 "separated g V ≡ separated₂ g V ∧ separated₃ g V"

subsection‹Admissible weight assignments\label{sec:TameAdmissible}›

text ‹
  weight assignment ‹w :: face → nat›
  a natural number to every face.

 index{‹admissible›}
 index{admissible weight assignment}

  formalize the admissibility requirements as follows:
 ›

definition admissible₁ :: "(face → nat) → graph → bool" where  
 "admissible₁ w g ≡ ∀f ∈ F g. d |vertices f| ≤ w f"

definition admissible₂ :: "(face → nat) → graph → bool" where  
 "admissible₂ w g ≡
  ∀v ∈ V g. except g v = 0 ⟶ b (tri g v) (quad g v) ≤ (∑_{∈facesAt g v} w f)"

definition admissible₃ :: "(face → nat) → graph → bool" where  
 "admissible₃ w g ≡
  ∀v ∈ V g. vertextype g v = (5,0,1) ⟶ (∑_{∈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₁ w g ∧ admissible₂ w g ∧ admissible₃ 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
  less than the target:›

definition tame13a :: "graph → bool" where
"tame13a g = (∃w. admissible w g ∧ (∑ _{∈ 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
(*>*)