text_formalization/leg/cayleyR_def.hl

   1 (* ========================================================================== *)
   2 (* FLYSPECK - BOOK FORMALIZATION                                              *)
   3 (*                                                                            *)
   4 (* Definition: cayleyR                                                        *)
   5 (* Chapter: LEG                                                               *)
   6 (* Author: Thomas C. Hales                                                    *)
   7 (* Date: 2010-02-07                                                           *)
   8 (* ========================================================================== *)
   9
  10
  11
  12
  13 (*
  14 This is the 5 vertex Cayley-Menger determinant
  15 EDSFZOT
  16 NUHSVLM
  17 See http://www.math.pitt.edu/~thales/papers/Lemmas_Elementary_Geometry.pdf
  18 Properties of cayleyR have been formalized by Nguyen Quang Truong
  19 *)
  20
  21
  22
  23 module type Cayleyr_def_type = sig
  24   val cayleyR : thm
  25   val cayleyR_quadratic : thm
  26 end;;
  27
  28
  29 module Cayleyr : Cayleyr_def_type = struct
  30
  31
  32  let cayleyR =
  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` ;;
  56
  57 let cayleyR_quadratic = prove( `cayleyR x12 x13 x14 x15  x23 x24 x25  x34 x35 =
  58  \ x45 .
  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
  96   BETA_TAC THEN
  97   (  REWRITE_TAC[cayleyR]) THEN
  98   (REPEAT LET_TAC) THEN
  99   (EXPAND_TAC "a") THEN
 100   (EXPAND_TAC "b") THEN
 101   (EXPAND_TAC "c") THEN
 102   (ARITH_TAC));;
 103
 104
 105 end;;
 106