(* ========================================================================== *)
(* FLYSPECK - BOOK FORMALIZATION                                              *)
(*                                                                            *)
(* Definition: muR                                                            *)
(* Chapter: LEG                                                               *)
(* Author: Thomas C. Hales                                                    *)
(* Date: 2010-02-07                                                           *)
(* ========================================================================== *)




(*
This is the cayleyR function, expressed in terms of the unsquared variables
indexing: five vertices v1..v5, yij runs from vi to vj,
two tetrahedra, shared face v1,v2,v3.
v4 v5 in opposite half-planes.
enclosed = y45 = sqrt(x45) is the distance from v4 to v5.
[y1,y2,y3,y4,y5,y6,y7,y8,y9]=[y14,y24,y34,y23,y13,y12,y15,y25,y35].
y1..y6 is the usual indexing of a simplex.
y4..y9 is mod 6 congruent to the usual indexing.
*)



module type Mur_def_type = sig
  val muR : thm
  val muRa : thm
end;;


flyspeck_needs "leg/cayleyR_def.hl";;



module Mur : Mur_def_type = struct

  let cayleyR = Cayleyr.cayleyR;;

 
let muR = 
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`;;
 
let muRa = 
prove(
  `muR  y1 y2 y3 y4 y5 y6 y7 y8 y9 = 
   cayleyR (y6*y6) (y5*y5) (y1*y1) (y7*y7) (y4*y4) (y2*y2) (y8*y8)  (y3*y3) (y9*y9)`,

  ONCE_REWRITE_TAC[FUN_EQ_THM] THEN REWRITE_TAC[muR]);;
end;;