1 (* ------------------------------------------------------------------ *)
2 (* Generate Definition files from the Collection in Elementary Geometry *)
3 (* ------------------------------------------------------------------ *)
7 (* let _ = set_root_dir "/flyspeck_google/source/text_formalization";; *)
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` ";;
33 let mkd def code comments needlist =
37 author="Thomas C. Hales";
43 output_template_def ud;;
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"]
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"] [];;
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`;;"
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"];;
66 mkd "abc_of_quadratic"
67 "new_definition `abc_of_quadratic f =
71 ((p + n)/(&2) - c, (p -n)/(&2), c)` ;;" ["f = \\x. a x^2 + b x + c, extract a b c"] [];;
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"];;