1 (* ========================================================================== *)
2 (* FLYSPECK - BOOK FORMALIZATION *)
4 (* Definition: cayleyR *)
6 (* Author: Thomas C. Hales *)
8 (* ========================================================================== *)
14 This is the 5 vertex Cayley-Menger determinant
17 See http://www.math.pitt.edu/~thales/papers/Lemmas_Elementary_Geometry.pdf
18 Properties of cayleyR have been formalized by Nguyen Quang Truong
23 module type Cayleyr_def_type = sig
25 val cayleyR_quadratic : thm
29 module Cayleyr : Cayleyr_def_type = struct
33 new_definition `cayleyR x12 x13 x14 x15 x23 x24 x25 x34 x35 x45 =
34 -- (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 +
35 &2 *x15*x15*x23*x24 - x13*x13*x24*x24 + &2 *x13*x15*x24*x24 - x15*x15*x24*x24 - &2 *x13*x14*x23*x25 +
36 &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 +
37 &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 -
38 &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 +
39 &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 -
40 &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 -
41 x12*x12*x34*x34 + &2 *x12*x15*x34*x34 - x15*x15*x34*x34 + &2 *x12*x25*x34*x34 + &2 *x15*x25*x34*x34 -
42 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 +
43 &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 +
44 &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 +
45 &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 +
46 &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 -
47 x12*x12*x35*x35 + &2 *x12*x14*x35*x35 - x14*x14*x35*x35 + &2 *x12*x24*x35*x35 + &2 *x14*x24*x35*x35 -
48 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 +
49 &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 -
50 &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 -
51 &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 -
52 &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 +
53 &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 -
54 &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 -
55 x13*x13*x45*x45 + &2 *x12*x23*x45*x45 + &2 *x13*x23*x45*x45 - x23*x23*x45*x45` ;;
57 let cayleyR_quadratic = prove( `cayleyR x12 x13 x14 x15 x23 x24 x25 x34 x35 =
59 ( let a = (((-- &1) * (x12 pow 2)) + (((-- &1) * ((x13 + ((-- &1) * x23)) pow 2)) +
60 (&2 * (x12 * (x13 + x23))))) in
61 let b = (&2 * (((x13 pow 2) * (x24 + x25)) + (((x12 pow 2) * (x34 + x35)) + ((x23 *
62 ((x15 * (x23 + (((-- &1) * x24) + ((-- &1) * x34)))) + ((x25 * x34) + ((x14 *
63 ((&2 * x15) + (x23 + (((-- &1) * x25) + ((-- &1) * x35))))) + (x24 * x35)))))
64 + (((-- &1) * (x13 * ((x23 * x24) + ((x23 * x25) + (((-- &2) * (x24 * x25)) +
65 ((x15 * (x23 + (x24 + ((-- &1) * x34)))) + ((x25 * x34) + ((x14 * (x23 + (x25
66 + ((-- &1) * x35)))) + (x24 * x35))))))))) + (x12 * ((&2 * (x13 * x23)) +
67 (((-- &1) * (x14 * x23)) + (((-- &1) * (x15 * x23)) + (((-- &1) * (x13 *
68 x24)) + ((x15 * x24) + (((-- &1) * (x13 * x25)) + ((x14 * x25) + (((-- &1) *
69 (x13 * x34)) + (((-- &1) * (x15 * x34)) + (((-- &1) * (x23 * x34)) + (((--
70 &1) * (x25 * x34)) + (((-- &1) * (x13 * x35)) + (((-- &1) * (x14 * x35)) +
71 (((-- &1) * (x23 * x35)) + (((-- &1) * (x24 * x35)) + (&2 * (x34 *
72 x35))))))))))))))))))))))) in
73 let c = (((-- &1) * ((x15 pow 2) * ((x23 pow 2) + (((x24 + ((-- &1) * x34)) pow 2) +
74 ((-- &2) * (x23 * (x24 + x34))))))) + (((-- &1) * (((x13 * x24) + (((-- &1) *
75 (x13 * x25)) + (((-- &1) * (x12 * x34)) + ((x25 * x34) + ((x12 * x35) + ((--
76 &1) * (x24 * x35))))))) pow 2)) + (((-- &1) * ((x14 pow 2) * ((x23 pow 2) +
77 (((x25 + ((-- &1) * x35)) pow 2) + ((-- &2) * (x23 * (x25 + x35))))))) +
78 (((-- &2) * (x15 * (((-- &2) * (x23 * (x24 * x34))) + ((x23 * (x25 * x34)) +
79 ((x24 * (x25 * x34)) + (((-- &1) * (x25 * (x34 pow 2))) + ((x13 * (((-- &1) *
80 (x24 pow 2)) + ((x23 * (x24 + ((-- &1) * x25))) + ((x25 * x34) + (x24 * (x25
81 + (x34 + ((-- &2) * x35)))))))) + ((x23 * (x24 * x35)) + (((-- &1) * ((x24 pow 2)
82 * x35)) + ((x24 * (x34 * x35)) + (x12 * ((x23 * (x34 + ((-- &1) * x35)))
83 + ((x34 * (((-- &2) * x25) + (((-- &1) * x34) + x35))) + (x24 * (x34 +
84 x35))))))))))))))) + (&2 * (x14 * ((x12 * (x23 * x34)) + (((-- &1) * (x12 *
85 (x25 * x34))) + (((-- &1) * (x23 * (x25 * x34))) + (((x25 pow 2) * x34) +
86 (((-- &1) * (x12 * (x23 * x35))) + ((&2 * (x12 * (x24 * x35))) + (((-- &1) *
87 (x23 * (x24 * x35))) + (((-- &1) * (x12 * (x25 * x35))) + ((&2 * (x23 * (x25
88 * x35))) + (((-- &1) * (x24 * (x25 * x35))) + (((-- &1) * (x12 * (x34 *
89 x35))) + (((-- &1) * (x25 * (x34 * x35))) + ((x12 * (x35 pow 2)) + ((x24 * (x35
90 pow 2)) + ((x13 * ((x23 * (x24 + ((-- &1) * x25))) + ((x25 * (x25 + ((&2 *
91 x34) + ((-- &1) * x35)))) + ((-- &1) * (x24 * (x25 + x35)))))) + (x15 * ((x23
92 pow 2) + (((x24 + ((-- &1) * x34)) * (x25 + ((-- &1) * x35))) + ((-- &1) *
93 (x23 * (x24 + (x25 + (x34 + x35))))))))))))))))))))))))))))) in
94 (a * x45 pow 2 + b * x45 + c))`,
95 (ONCE_REWRITE_TAC[FUN_EQ_THM]) THEN
97 ( REWRITE_TAC[cayleyR]) THEN
100 (EXPAND_TAC "b") THEN
101 (EXPAND_TAC "c") THEN