development/thales/chaff/tame_constants.ml

   1 (* modified from
   2 http://afp.sourceforge.net/browser_info/current/HOL/Flyspeck-Tame/Tame.html
   3 *)
   4 subsection {* Constants \label{sec:TameConstants}*}
   5
   6 constdefs squanderTarget :: "nat"
   7  "squanderTarget ≡ 1541"
   8
   9 constdefs excessTCount :: "nat => nat" (*<*) ("\<a>")(*>*)
  10
  11  "\<a> t ≡ if t < 5 then squanderTarget
  12      else 630"
  13
  14 constdefs squanderVertex :: "nat => nat => nat"  (*<*)("\<b>")(*>*)
  15
  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
  32      else squanderTarget"
  33
  34 constdefs scoreFace :: "nat => int" (*<*)("\<c>")(*>*)
  35
  36  "\<c> n ≡ 0"
  37
  38 constdefs squanderFace :: "nat => nat" (*<*)("\<d>")(*>*)
  39
  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
  46      else squanderTarget"