(* ========================================================================== *)
(* FLYSPECK - BOOK FORMALIZATION                                              *)
(*                                                                            *)
(* Chapter: Trigonometry                                               *)
(* Author: Thomas C. Hales                                                    *)
(* Date: 2010-02-09                                                           *)
(* ========================================================================== *)




(* summary of the trig chapter *)




(*

Known issues:

-- Flypaper defines sin and cos by their power series. HOL Light defines them
through complex analysis.

-- NUHSVLM: 5 points in R3 ==> cayleyR = 0, moved to collect_geom2.ml. Slow to run.
     I will keep it out of the daily build.

-- Some results (marked LEG) may have been formalized but not imported from legacy directory.
Lemmas in Elementary Geometry.  Now in leg/ directory.

-- some minor results that haven't been done or located are marked UNKNOWN  below

-- polar_cycle deprecated 2011-08-01.

*)


module type Trigonometry_type = sig

end;;

flyspeck_needs "general/sphere.hl";;
flyspeck_needs "leg/enclosed_def.hl";;
flyspeck_needs "leg/collect_geom.hl";;
flyspeck_needs "trigonometry/trig1.hl";;
flyspeck_needs "trigonometry/trig2.hl";;


module Trigonometry (* : Trigonometry_type *)  = struct

(*
let LIST_MK_CONJ b = match b with
   [] -> TRUTH
  |b::bs as a-> let g = itlist (curry mk_conj) (map concl bs) (concl b) in prove(g,REWRITE_TAC a);;
*)
  let LIST_MK_CONJ (b:thm list) = b;;

let UNKNOWN = REWRITE_RULE[TRUTH] (new_definition `unknown = T`);;

 let elimin  = REWRITE_RULE[IN];;

let FOYTTIX1 = cos;;
let FOYTTIX2 = sin;;
let FOYTTIX=LIST_MK_CONJ [FOYTTIX1;FOYTTIX2];;

let YIXJNJQ1 = SIN_0;;
let YIXJNJQ2 = COS_0;;
let YIXJNJQ = LIST_MK_CONJ [YIXJNJQ1;YIXJNJQ2];;

let WPMXVYZ = SIN_CIRCLE;; 

let WNYVJPE1 = SIN_ADD;;
let WNYVJPE2 = COS_ADD;;
let WNYVJPE = LIST_MK_CONJ [WNYVJPE1;WNYVJPE2];;

let KGLLRQT1 = COS_NEG;;
let KGLLRQT2 = SIN_NEG;;
let KGLLRQT = LIST_MK_CONJ [KGLLRQT1;KGLLRQT2];;

(* cos(pi/2) = 0 *)
let CFXEKKP1 =  COS_PI2;;
let CFXEKKP2 =  COS_POS_PI2;;

(* This is combined between two lemmas *)
let ZSKECZV = COS_POS_PI_LE;;

(* Lemma label{lemma:sin-pi2} *)
let CPIREMF1 = SIN_PI2;;
let CPIREMF2 = SIN_POS_PI_LE;;
let CPIREMF = LIST_MK_CONJ [CPIREMF1;CPIREMF2];;

(* Lemma label{lemma:cos-sin} *)
let SCEZKRH1 = GSYM COS_SIN;;
let SCEZKRH2 = GSYM SIN_COS;;

let SCEZKRH = LIST_MK_CONJ [SCEZKRH1;SCEZKRH2];;

let WIBGJRR = SIN_POS_PI_LE;;

let LLOYXRK1 = prove(`!x. cos(pi/ &2 + x) = -- (sin x)`,
   REWRITE_TAC[REAL_ARITH `x + y = x - (-- y)`;GSYM SIN_COS;SIN_NEG]);;
let LLOYXRK2 = prove(`!x. sin(pi/ &2 + x) = cos x`,
   REWRITE_TAC[REAL_ARITH `x + y = x - (-- y)`;GSYM COS_SIN;COS_NEG]);;
let LLOYXRK3 = SIN_PERIODIC_PI;;
let LLOYXRK4 = COS_PERIODIC_PI;;
let LLOYXRK5 = SIN_PERIODIC;;
let LLOYXRK6 = COS_PERIODIC;;
let LLOYXRK = LIST_MK_CONJ [LLOYXRK1;LLOYXRK2;LLOYXRK3;LLOYXRK4;LLOYXRK5;LLOYXRK6];;

(* sin non-negative *)
let WIBGJRR = SIN_POS_PI_LE;;

(* definition label{def:tan} *)
 let BIRXGXP = tan ;;

(* Lemma label{lemma:tan-add} *)
let KWYPRWZ = TAN_ADD;;

(* Lemma label{lemma:tan-pi4} *)
let KSQDZSF = TAN_PI4;;

(* tan increasing and one-to-one *)
let UTNKIAC = TAN_MONO_LT;;

let RIQVMHH1 = atn;;
let RIQVMHH2 =  ATN_BOUNDS ;;
let RIQVMHH=LIST_MK_CONJ [RIQVMHH1;RIQVMHH2];;


let EWITKLU  = ATN_TAN ;;

let YTXYLRB = ATN_1 ;;

let OKENMAM= HAS_REAL_DERIVATIVE_ATN;;


let LQCXGZX = ATN_MONO_LT_EQ ;;

(* atan2 *)
let GYKGARD = Sphere.atn2;;
let QZTBJMH1 = acs;;
let QZTBJMH2 = COS_ACS;;
let QZTBJMH3 = ACS_COS;;
let QZTBJMH = LIST_MK_CONJ [ QZTBJMH1; QZTBJMH2; QZTBJMH3];;
let FMGMALU = SIN_ACS;;
let OUIJTWY = Trigonometry2.acs_atn2 ;;
(* let asn = asn;; *)


(* VECTOR GEOMETRY *)

let KRZJIAD = (`:real^N`,`v$i`,`vec 0`);;

let WHIAXYD1 =  [`(x:real^3) + (y:real^3)`;`(x:real^3) - (x:real^3)`;
  `-- (x:real^3)`;`t % (x:real^3)`];;
let WHIAXYD2 = VECTOR_ADD_ASSOC;;
let WHIAXYD3 = VECTOR_ADD_SYM;;
let WHIAXYD = ( WHIAXYD1, WHIAXYD2, WHIAXYD3);;


let VFPCZBI =  [`(x:real^3) dot (y:real^3)`];;

let XHVXJVB = vector_norm;;


(*CAUCHY SCHWARZ Lemma label{} *)
let JJKJALK = NORM_CAUCHY_SCHWARZ ;;


(*TRIANGLE INEQ  Lemma label{} *)
let OIPLPTM1 = NORM_TRIANGLE ;;
let OIPLPTM2 = NORM_TRIANGLE_EQ ;;
let OIPLPTM = LIST_MK_CONJ [OIPLPTM1;OIPLPTM2];;

(* AFFINE GEOMETRY *)

let KVLZSAQ1 = AFFINE;;
let KVLZSAQ2 = Sphere.aff;;  (* deprecated *)
let KVLZSAQ = LIST_MK_CONJ [KVLZSAQ1;KVLZSAQ2];;

(* see also affsign;; lin_combo;; *)

let BYFLKYM1 = Sphere.aff;;
let BYFLKYM2 = Sphere.aff_ge_def;;
let BYFLKYM3 = Sphere.aff_gt_def;;
let BYFLKYM4 = Sphere.aff_lt_def;;
let BYFLKYM5 = Sphere.aff_le_def;;
let BYFLKYM = LIST_MK_CONJ [BYFLKYM1;BYFLKYM2;BYFLKYM3;BYFLKYM4;BYFLKYM5];;

let OWECYNV1 = convex;;
let OWECYNV2 = `(hull) convex`;;
let OWECYNV = (OWECYNV1,OWECYNV2);;

let GDCZMLO = CONVEX_HULL_AFF_GE;;

let UIVNNRR1 = prove(
  `!V. (aff_ge V EMPTY = aff_gt V EMPTY)`,
  REWRITE_TAC[aff_ge_def;aff_gt_def;affsign]  THEN
  STRIP_TAC THEN 
  ONCE_REWRITE_TAC[FUN_EQ_THM] THEN
  REWRITE_TAC[affsign;elimin NOT_IN_EMPTY]
);;

let UIVNNRR2 = AFF_GT_EQ_AFFINE_HULL;;
let UIVNNRR = LIST_MK_CONJ [UIVNNRR1;UIVNNRR2];;

let LLOUBAX = cone ;;
let SWKFLBJ1 = Sphere.line ;;
let SWKFLBJ2 = collinear ;;
let parallel = define `parallel (v:real^N) w = collinear {(vec 0),v,w}`;;
let SWKFLBJ3 = parallel;;
let  SWKFLBJ = LIST_MK_CONJ [ SWKFLBJ1; SWKFLBJ2; SWKFLBJ3];;

let JLWZFBH1 = plane ;;
let JLWZFBH2 = Sphere.closed_half_plane;;
let JLWZFBH3 = Sphere.open_half_plane;;
let  JLWZFBH4  = coplanar ;;
let JLWZFBH = LIST_MK_CONJ [JLWZFBH1;JLWZFBH2;JLWZFBH3;JLWZFBH4];;

let OAUVFPS1 = Sphere.closed_half_space ;;
let OAUVFPS2 = Sphere.open_half_space ;;
let OAUVFPS = LIST_MK_CONJ [OAUVFPS1;OAUVFPS2];;

let AVWKGNB = delta_x;;

let LBEVAKV = Collect_geom.DELTA_POS_4POINTS;;
let CTCZHMR = LIST_MK_CONJ [LBEVAKV;Collect_geom.POLFLZY];; (* Delta pos LEG [line 2690;line 3010], *) 


let KZVHHBG = LIST_MK_CONJ [Collect_geom.LTCTBAN;Collect_geom.GJWYYPS;Collect_geom.GDLRUZB];;

let NUHSVLM = UNKNOWN;; (* " implemented in collect_geom2.hl" ;;  *)

(* CayleyR results: lines from legacy/collect_geom.ml LEG:
2337/LTCTBAN: ups is leading coeff of quadratic cayleyR
2725/GJWYYPS: discriminant of cayleyR
2894/GDLRUZB: disc(cayleyR)=0 <=> one of tetra are coplanar
3010/NUHSVLM: 5 points in R3 ==> cayleyR = 0

RPFVZDI:  enclosed function defined
*)

let RPFVZDI = Enclosed.enclosed;; (* "implemented in enclosed_def.hl ";; *)


let WZYUXVC = arcV ;;

let ACNBFRL = UNKNOWN ;; (* arcV atn2 *)

let PQQDENV = Trigonometry1.ACS_ARCLENGTH;;

let HQTBPCM1 = LAW_OF_COSINES ;;
let HQTBPCM2 = Trigonometry1.DIST_LAW_OF_COS ;;
let HQTBPCM = LIST_MK_CONJ [HQTBPCM1;HQTBPCM2];;


let OBPIOXD = Sphere.ups_x;; (* upsilon def *)
let QRAAWFS = LIST_MK_CONJ [Trigonometry2.UPS_X_POS;Collect_geom.FHFMKIY];;
let IHIQXLM = Trigonometry1.UPS_X_SQUARES;; (* upsilon factors *)

let UKBAHKV = Trigonometry1.VECTOR_LAW_OF_SINES ;; (* slightly different from book *)

let GVWTZKY = UNKNOWN;; (* arc, atn2 *)


(* cross product something *)
let FCUAGA = cross;;
let KVVWPNA = NORM_CROSS ;; (* norm cross and ups, combine with UKBAHKV *)

(* Lemma label{} *)
(* cross product order and distribution with dot product *)
let BKMUSOX1 = CROSS_SKEW ;;
let BKMUSOX2 = CROSS_TRIPLE ;;
let  BKMUSOX = LIST_MK_CONJ [ BKMUSOX1; BKMUSOX2];;

(* Definition label{def:dih} *)
let dihV = dihV ;;

let RLXWSTK = Trigonometry2.RLXWSTK;;

let NLVWBBW = Trigonometry2.NLVWBBW;;  

let OJEKOJF = Trigonometry2.OJEKOJF;; 

let JLPSDHF = Euler_main_theorem.EULER_TRIANGLE;; (* euler_triangle ;; *) 


let KEITDWB = Trigonometry2.ARCV_INEQUALTY ;;
let FGNMPAV = Trigonometry2.FGNMPAV ;;

let FEVNANL = LIST_MK_CONJ [Trigonometry1.atn2_spec;Trigonometry1.ATAN2_EXISTS];;

let AXBTGQX = orthonormal;;  (* much more has been proved about orthonormal vectors *)

let QAUQIEC = UNKNOWN;; (* "not found, adapted orthonormization ";; *)

let EYFCXPP = [Trigonometry2.EYFCXPP;(* see also CYLINDER_CORDINATE *)
	       Trigonometry2.CYLINDER_CORDINATE];;

let azim = azim ;;  

let QQZKTXU = Trigonometry2.QQZKTXU;;
let JBDNJJB = Trigonometry2.JBDNJJB;;

(* zenith angle *)

let QAFHJNM =Trigonometry2.QAFHJNM;;
let XPHCPNY = SPHERICAL_COORDINATES ;;

(* Cycle *)

(* DEPRECATED 2011-08-01. let TNZQDCX = Sphere.polar_cycle;; *)

let PDPFQUK = Trigonometry2.PDPFQUK;;
let ISRTTNZ = Trigonometry2.ISRTTNZ;;
let KFKHLWK = Trigonometry2.cyclic_set;;
let YESEEWW = Sphere.azim_cycle;;
let NLOFMTR = UNKNOWN;; (* "not found, of doubtful use";; *)
let YVREJIS =  Trigonometry2.YVREJIS;;
let ULEKUUB = UNKNOWN;; (* "not found, fan version given as Topology.ULEKUUB";; *)

(* spherical triangle inequality *)

let KEITDWB = Trigonometry2.KEITDWB;;
let FGNMPAV = Trigonometry2.FGNMPAV;;


end;;