(* ========================================================================== *)
(* FLYSPECK - BOOK FORMALIZATION *)
(* *)
(* Definition: cayleyR *)
(* Chapter: LEG *)
(* Author: Thomas C. Hales *)
(* Date: 2010-02-07 *)
(* ========================================================================== *)
(*
This is the 5 vertex Cayley-Menger determinant
EDSFZOT
NUHSVLM
See http://www.math.pitt.edu/~thales/papers/Lemmas_Elementary_Geometry.pdf
Properties of cayleyR have been formalized by Nguyen Quang Truong
*)
module type Cayleyr_def_type = sig
val cayleyR : thm
val cayleyR_quadratic : thm
end;;
module Cayleyr : Cayleyr_def_type = struct
let cayleyR =
new_definition `cayleyR x12 x13 x14 x15 x23 x24 x25 x34 x35 x45 =
-- (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 +
&2 *x15*x15*x23*x24 - x13*x13*x24*x24 + &2 *x13*x15*x24*x24 - x15*x15*x24*x24 - &2 *x13*x14*x23*x25 +
&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 +
&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 -
&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 +
&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 -
&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 -
x12*x12*x34*x34 + &2 *x12*x15*x34*x34 - x15*x15*x34*x34 + &2 *x12*x25*x34*x34 + &2 *x15*x25*x34*x34 -
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 +
&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 +
&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 +
&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 +
&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 -
x12*x12*x35*x35 + &2 *x12*x14*x35*x35 - x14*x14*x35*x35 + &2 *x12*x24*x35*x35 + &2 *x14*x24*x35*x35 -
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 +
&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 -
&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 -
&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 -
&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 +
&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 -
&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 -
x13*x13*x45*x45 + &2 *x12*x23*x45*x45 + &2 *x13*x23*x45*x45 - x23*x23*x45*x45` ;;
let cayleyR_quadratic = prove( `cayleyR x12 x13 x14 x15 x23 x24 x25 x34 x35 =
\ x45 .
( let a = (((-- &1) * (x12 pow 2)) + (((-- &1) * ((x13 + ((-- &1) * x23)) pow 2)) +
(&2 * (x12 * (x13 + x23))))) in
let b = (&2 * (((x13 pow 2) * (x24 + x25)) + (((x12 pow 2) * (x34 + x35)) + ((x23 *
((x15 * (x23 + (((-- &1) * x24) + ((-- &1) * x34)))) + ((x25 * x34) + ((x14 *
((&2 * x15) + (x23 + (((-- &1) * x25) + ((-- &1) * x35))))) + (x24 * x35)))))
+ (((-- &1) * (x13 * ((x23 * x24) + ((x23 * x25) + (((-- &2) * (x24 * x25)) +
((x15 * (x23 + (x24 + ((-- &1) * x34)))) + ((x25 * x34) + ((x14 * (x23 + (x25
+ ((-- &1) * x35)))) + (x24 * x35))))))))) + (x12 * ((&2 * (x13 * x23)) +
(((-- &1) * (x14 * x23)) + (((-- &1) * (x15 * x23)) + (((-- &1) * (x13 *
x24)) + ((x15 * x24) + (((-- &1) * (x13 * x25)) + ((x14 * x25) + (((-- &1) *
(x13 * x34)) + (((-- &1) * (x15 * x34)) + (((-- &1) * (x23 * x34)) + (((--
&1) * (x25 * x34)) + (((-- &1) * (x13 * x35)) + (((-- &1) * (x14 * x35)) +
(((-- &1) * (x23 * x35)) + (((-- &1) * (x24 * x35)) + (&2 * (x34 *
x35))))))))))))))))))))))) in
let c = (((-- &1) * ((x15 pow 2) * ((x23 pow 2) + (((x24 + ((-- &1) * x34)) pow 2) +
((-- &2) * (x23 * (x24 + x34))))))) + (((-- &1) * (((x13 * x24) + (((-- &1) *
(x13 * x25)) + (((-- &1) * (x12 * x34)) + ((x25 * x34) + ((x12 * x35) + ((--
&1) * (x24 * x35))))))) pow 2)) + (((-- &1) * ((x14 pow 2) * ((x23 pow 2) +
(((x25 + ((-- &1) * x35)) pow 2) + ((-- &2) * (x23 * (x25 + x35))))))) +
(((-- &2) * (x15 * (((-- &2) * (x23 * (x24 * x34))) + ((x23 * (x25 * x34)) +
((x24 * (x25 * x34)) + (((-- &1) * (x25 * (x34 pow 2))) + ((x13 * (((-- &1) *
(x24 pow 2)) + ((x23 * (x24 + ((-- &1) * x25))) + ((x25 * x34) + (x24 * (x25
+ (x34 + ((-- &2) * x35)))))))) + ((x23 * (x24 * x35)) + (((-- &1) * ((x24 pow 2)
* x35)) + ((x24 * (x34 * x35)) + (x12 * ((x23 * (x34 + ((-- &1) * x35)))
+ ((x34 * (((-- &2) * x25) + (((-- &1) * x34) + x35))) + (x24 * (x34 +
x35))))))))))))))) + (&2 * (x14 * ((x12 * (x23 * x34)) + (((-- &1) * (x12 *
(x25 * x34))) + (((-- &1) * (x23 * (x25 * x34))) + (((x25 pow 2) * x34) +
(((-- &1) * (x12 * (x23 * x35))) + ((&2 * (x12 * (x24 * x35))) + (((-- &1) *
(x23 * (x24 * x35))) + (((-- &1) * (x12 * (x25 * x35))) + ((&2 * (x23 * (x25
* x35))) + (((-- &1) * (x24 * (x25 * x35))) + (((-- &1) * (x12 * (x34 *
x35))) + (((-- &1) * (x25 * (x34 * x35))) + ((x12 * (x35 pow 2)) + ((x24 * (x35
pow 2)) + ((x13 * ((x23 * (x24 + ((-- &1) * x25))) + ((x25 * (x25 + ((&2 *
x34) + ((-- &1) * x35)))) + ((-- &1) * (x24 * (x25 + x35)))))) + (x15 * ((x23
pow 2) + (((x24 + ((-- &1) * x34)) * (x25 + ((-- &1) * x35))) + ((-- &1) *
(x23 * (x24 + (x25 + (x34 + x35))))))))))))))))))))))))))))) in
(a * x45 pow 2 + b * x45 + c))`,
(ONCE_REWRITE_TAC[
FUN_EQ_THM]) THEN
BETA_TAC THEN
( REWRITE_TAC[cayleyR]) THEN
(REPEAT LET_TAC) THEN
(EXPAND_TAC "a") THEN
(EXPAND_TAC "b") THEN
(EXPAND_TAC "c") THEN
(ARITH_TAC));;