2 http://afp.sourceforge.net/browser_info/current/HOL/Flyspeck-Tame/Tame.html
4 subsection {* Constants \label{sec:TameConstants}*}
6 constdefs squanderTarget :: "nat"
7 "squanderTarget ≡ 1541"
9 constdefs excessTCount :: "nat => nat" (*<*) ("\<a>")(*>*)
11 "\<a> t ≡ if t < 5 then squanderTarget
14 constdefs squanderVertex :: "nat => nat => nat" (*<*)("\<b>")(*>*)
16 "\<b> p q ≡ if p = 0 ∧ q = 2 then 1296
17 else if p = 0 ∧ q = 3 then 618
18 else if p = 0 ∧ q = 4 then 1000
19 else if p = 1 ∧ q = 2 then 660
20 else if p = 1 ∧ q = 3 then 618
21 else if p = 2 ∧ q = 1 then 800
22 else if p = 2 ∧ q = 2 then 412
23 else if p = 2 ∧ q = 3 then 1285
24 else if p = 3 ∧ q = 1 then 315
25 else if p = 3 ∧ q = 2 then 830
26 else if p = 4 ∧ q = 0 then 350
27 else if p = 4 ∧ q = 1 then 374
28 else if p = 5 ∧ q = 0 then 40
29 else if p = 5 ∧ q = 1 then 1144
30 else if p = 6 ∧ q = 0 then 689
31 else if p = 7 ∧ q = 0 then 1450
34 constdefs scoreFace :: "nat => int" (*<*)("\<c>")(*>*)
38 constdefs squanderFace :: "nat => nat" (*<*)("\<d>")(*>*)
40 "\<d> n ≡ if n = 3 then 0
41 else if n = 4 then 206
42 else if n = 5 then 483
43 else if n = 6 then 760
44 else if n = 7 then 1038
45 else if n = 8 then 1315