1 (* ========================================================================== *)
2 (* FLYSPECK - BOOK FORMALIZATION *)
6 (* Author: Thomas C. Hales *)
8 (* ========================================================================== *)
14 This is the cayleyR function, expressed in terms of the unsquared variables
15 indexing: five vertices v1..v5, yij runs from vi to vj,
16 two tetrahedra, shared face v1,v2,v3.
17 v4 v5 in opposite half-planes.
18 enclosed = y45 = sqrt(x45) is the distance from v4 to v5.
19 [y1,y2,y3,y4,y5,y6,y7,y8,y9]=[y14,y24,y34,y23,y13,y12,y15,y25,y35].
20 y1..y6 is the usual indexing of a simplex.
21 y4..y9 is mod 6 congruent to the usual indexing.
26 module type Mur_def_type = sig
32 flyspeck_needs "leg/cayleyR_def.hl";;
36 module Mur : Mur_def_type = struct
38 let cayleyR = Cayleyr.cayleyR;;
41 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`;;
44 `muR y1 y2 y3 y4 y5 y6 y7 y8 y9 =
45 cayleyR (y6*y6) (y5*y5) (y1*y1) (y7*y7) (y4*y4) (y2*y2) (y8*y8) (y3*y3) (y9*y9)`,
46 ONCE_REWRITE_TAC[FUN_EQ_THM] THEN REWRITE_TAC[muR]);;