development/thales/chaff/general/generate_definitions.ml

   1 (* ------------------------------------------------------------------ *)
   2 (*   Generate Definition files from the Collection in Elementary Geometry           *)
   3 (* ------------------------------------------------------------------ *)
   4
   5 open Template_hol;;
   6
   7 (* let _ = set_root_dir "/flyspeck_google/source/text_formalization";; *)
   8
   9 let cayleyRstr="new_definition `cayleyR x12 x13 x14 x15  x23 x24 x25  x34 x35 x45 =
  10   -- (x14*x14*x23*x23) + &2 *x14*x15*x23*x23 - x15*x15*x23*x23 + &2 *x13*x14*x23*x24 - &2 *x13*x15*x23*x24 - &2 *x14*x15*x23*x24 +
  11    &2 *x15*x15*x23*x24 - x13*x13*x24*x24 + &2 *x13*x15*x24*x24 - x15*x15*x24*x24 - &2 *x13*x14*x23*x25 +
  12    &2 *x14*x14*x23*x25 + &2 *x13*x15*x23*x25 - &2 *x14*x15*x23*x25 + &2 *x13*x13*x24*x25 - &2 *x13*x14*x24*x25 - &2 *x13*x15*x24*x25 +
  13    &2 *x14*x15*x24*x25 - x13*x13*x25*x25 + &2 *x13*x14*x25*x25 - x14*x14*x25*x25 + &2 *x12*x14*x23*x34 - &2 *x12*x15*x23*x34 -
  14    &2 *x14*x15*x23*x34 + &2 *x15*x15*x23*x34 + &2 *x12*x13*x24*x34 - &2 *x12*x15*x24*x34 - &2 *x13*x15*x24*x34 + &2 *x15*x15*x24*x34 +
  15    &4 *x15*x23*x24*x34 - &2 *x12*x13*x25*x34 - &2 *x12*x14*x25*x34 + &4 *x13*x14*x25*x34 + &4 *x12*x15*x25*x34 - &2 *x13*x15*x25*x34 - &2 *x14*x15*x25*x34 -
  16    &2 *x14*x23*x25*x34 - &2 *x15*x23*x25*x34 - &2 *x13*x24*x25*x34 - &2 *x15*x24*x25*x34 + &2 *x13*x25*x25*x34 + &2 *x14*x25*x25*x34 -
  17    x12*x12*x34*x34 + &2 *x12*x15*x34*x34 - x15*x15*x34*x34 + &2 *x12*x25*x34*x34 + &2 *x15*x25*x34*x34 -
  18    x25*x25*x34*x34 - &2 *x12*x14*x23*x35 + &2 *x14*x14*x23*x35 + &2 *x12*x15*x23*x35 - &2 *x14*x15*x23*x35 - &2 *x12*x13*x24*x35 +
  19    &4 *x12*x14*x24*x35 - &2 *x13*x14*x24*x35 - &2 *x12*x15*x24*x35 + &4 *x13*x15*x24*x35 - &2 *x14*x15*x24*x35 - &2 *x14*x23*x24*x35 - &2 *x15*x23*x24*x35 +
  20    &2 *x13*x24*x24*x35 + &2 *x15*x24*x24*x35 + &2 *x12*x13*x25*x35 - &2 *x12*x14*x25*x35 - &2 *x13*x14*x25*x35 + &2 *x14*x14*x25*x35 +
  21    &4 *x14*x23*x25*x35 - &2 *x13*x24*x25*x35 - &2 *x14*x24*x25*x35 + &2 *x12*x12*x34*x35 - &2 *x12*x14*x34*x35 - &2 *x12*x15*x34*x35 +
  22    &2 *x14*x15*x34*x35 - &2 *x12*x24*x34*x35 - &2 *x15*x24*x34*x35 - &2 *x12*x25*x34*x35 - &2 *x14*x25*x34*x35 + &2 *x24*x25*x34*x35 -
  23    x12*x12*x35*x35 + &2 *x12*x14*x35*x35 - x14*x14*x35*x35 + &2 *x12*x24*x35*x35 + &2 *x14*x24*x35*x35 -
  24    x24*x24*x35*x35 + &4 *x12*x13*x23*x45 - &2 *x12*x14*x23*x45 - &2 *x13*x14*x23*x45 - &2 *x12*x15*x23*x45 - &2 *x13*x15*x23*x45 +
  25    &4 *x14*x15*x23*x45 + &2 *x14*x23*x23*x45 + &2 *x15*x23*x23*x45 - &2 *x12*x13*x24*x45 + &2 *x13*x13*x24*x45 + &2 *x12*x15*x24*x45 -
  26    &2 *x13*x15*x24*x45 - &2 *x13*x23*x24*x45 - &2 *x15*x23*x24*x45 - &2 *x12*x13*x25*x45 + &2 *x13*x13*x25*x45 + &2 *x12*x14*x25*x45 -
  27    &2 *x13*x14*x25*x45 - &2 *x13*x23*x25*x45 - &2 *x14*x23*x25*x45 + &4 *x13*x24*x25*x45 + &2 *x12*x12*x34*x45 - &2 *x12*x13*x34*x45 -
  28    &2 *x12*x15*x34*x45 + &2 *x13*x15*x34*x45 - &2 *x12*x23*x34*x45 - &2 *x15*x23*x34*x45 - &2 *x12*x25*x34*x45 - &2 *x13*x25*x34*x45 + &2 *x23*x25*x34*x45 +
  29    &2 *x12*x12*x35*x45 - &2 *x12*x13*x35*x45 - &2 *x12*x14*x35*x45 + &2 *x13*x14*x35*x45 - &2 *x12*x23*x35*x45 - &2 *x14*x23*x35*x45 -
  30    &2 *x12*x24*x35*x45 - &2 *x13*x24*x35*x45 + &2 *x23*x24*x35*x45 + &4 *x12*x34*x35*x45 - x12*x12*x45*x45 + &2 *x12*x13*x45*x45 -
  31    x13*x13*x45*x45 + &2 *x12*x23*x45*x45 + &2 *x13*x23*x45*x45 - x23*x23*x45*x45` ";;
  32
  33 let mkd def code comments needlist =
  34   let ud =
  35     {identifier=def;
  36      chapter="LEG";
  37      author="Thomas C. Hales";
  38      date="2010-02-07";
  39      code=code;
  40      comments=comments;
  41      needlist=needlist;
  42     } in
  43      output_template_def ud;;
  44
  45 mkd "cayleyR" cayleyRstr ["This is the 5 vertex Cayley-Menger determinant";"EDSFZOT";"NUHSVLM";
  46        "See http://www.math.pitt.edu/~thales/papers/Lemmas_Elementary_Geometry.pdf";
  47    "Properties of cayleyR have been formalized by Nguyen Quang Truong"]
  48      [];;
  49
  50 mkd "quadratic_root_plus"
  51    "   new_definition `quadratic_root_plus (a, b, c) = ( -- b + sqrt(b pow 2 - &4 * a * c))/ (&2 * a)`;;"
  52    ["Lemmas Elementary Geometry  (def:calE), RPFVZDI"] [];;
  53
  54 mkd "muR"
  55   "new_definition `muR y1 y2 y3 y4 y5 y6 y7 y8 y9 x = cayleyR (y6*y6) (y5*y5) (y1*y1) (y7*y7) (y4*y4) (y2*y2) (y8*y8)  (y3*y3) (y9*y9) x`;;"
  56   [
  57    "This is the cayleyR function, expressed in terms of the unsquared variables";
  58    "indexing: five vertices v1..v5, yij runs from vi to vj,";
  59    "two tetrahedra, shared face v1,v2,v3.";
  60    "v4 v5 in opposite half-planes.";
  61    "enclosed = y45 = sqrt(x45) is the distance from v4 to v5.";
  62    "[y1,y2,y3,y4,y5,y6,y7,y8,y9]=[y14,y24,y34,y23,y13,y12,y15,y25,y35].";
  63    "y1..y6 is the usual indexing of a simplex.";
  64    "y4..y9 is mod 6 congruent to the usual indexing."] ["leg/cayleyR_def.hl"];;
  65
  66 mkd "abc_of_quadratic"
  67  "new_definition `abc_of_quadratic f =
  68   let c = f (&0) in
  69   let  p = f (&1) in
  70   let n = f (-- &1) in
  71   ((p + n)/(&2) - c, (p -n)/(&2), c)` ;;" ["f = \\x. a x^2 + b x + c, extract a b c"] [];;
  72
  73 mkd "enclosed"
  74  "new_definition `enclosed y1 y2 y3 y4 y5 y6 y7 y8 y9 = sqrt
  75   (quadratic_root_plus (abc_of_quadratic (muR y1 y2 y3 y4 y5 y6 y7 y8 y9)))`;;"
  76   ["The function of 9 variables defined on page 37 of the Kepler Conjecture, DCG vol 36(1), July 2006";
  77    "It is generally typeset as a calligraphic E"] ["leg/muR_def.hl";"leg/abc_of_quadratic_def.hl";"leg/quadratic_root_plus.hl"];;
  78