text_formalization/leg/muR_def.hl

   1 (* ========================================================================== *)
   2 (* FLYSPECK - BOOK FORMALIZATION                                              *)
   3 (*                                                                            *)
   4 (* Definition: muR                                                            *)
   5 (* Chapter: LEG                                                               *)
   6 (* Author: Thomas C. Hales                                                    *)
   7 (* Date: 2010-02-07                                                           *)
   8 (* ========================================================================== *)
   9
  10
  11
  12
  13 (*
  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.
  22 *)
  23
  24
  25
  26 module type Mur_def_type = sig
  27   val muR : thm
  28   val muRa : thm
  29 end;;
  30
  31
  32 flyspeck_needs "leg/cayleyR_def.hl";;
  33
  34
  35
  36 module Mur : Mur_def_type = struct
  37
  38   let cayleyR = Cayleyr.cayleyR;;
  39
  40  let muR =
  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`;;
  42
  43  let muRa = prove(
  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]);;
  47
  48 end;;
  49