module Lp_ineqs_def = struct

open Sphere;;
open Fan_defs;;

(* Definitions of all fan variables *)

let azim2_fan = new_definition `azim2_fan (V,E) (x:real^3#real^3) = azim_dart (V,E) (f_fan_pair_ext (V,E) x)`;;
let azim3_fan = new_definition `azim3_fan (V,E) (x:real^3#real^3) = azim_dart (V,E) (inverse (f_fan_pair_ext (V,E)) x)`;;
let yn_fan = new_definition `yn_fan (v:real^3) = norm v`;;
let ln_fan = new_definition `ln_fan (v:real^3) = lmfun (yn_fan v / &2)`;;
let rho_fan = new_definition `rho_fan (v:real^3) = abs (&1 + const1 * (&1 - ln_fan v))`;;
let ye_fan = new_definition `ye_fan (x:real^3#real^3) = dist x`;;
let y1_fan = new_definition `y1_fan (x:real^3#real^3) = norm (FST x)`;;
let y2_fan = new_definition `y2_fan (x:real^3#real^3) = norm (SND x)`;;
let y3_fan = new_definition `y3_fan (V,E) (x:real^3#real^3) = norm (FST (inverse (f_fan_pair_ext (V,E)) x))`;;
let y4_fan = new_definition `y4_fan (V,E) (x:real^3#real^3) = dist (f_fan_pair_ext (V,E) x)`;;
let y5_fan = new_definition `y5_fan (V,E) (x:real^3#real^3) = dist (inverse (f_fan_pair_ext (V,E)) x)`;;
let y6_fan = new_definition `y6_fan (x:real^3#real^3) = dist x`;;
let y8_fan = new_definition `y8_fan (V,E) (x:real^3#real^3) = y5_fan (V,E) (inverse (f_fan_pair_ext (V,E)) x)`;;
let y9_fan = new_definition `y9_fan (V,E) (x:real^3#real^3) = dist (f_fan_pair_ext (V,E) x)`;;
let rhazim_fan = new_definition `rhazim_fan (V,E) (x:real^3#real^3) = abs (&1 + const1 * (&1 - lmfun (h_dart x))) * azim_dart (V,E) x`;;
let rhazim2_fan = new_definition `rhazim2_fan (V,E) (x:real^3#real^3) = rhazim_fan (V,E) (f_fan_pair_ext (V,E) x)`;;
let rhazim3_fan = new_definition `rhazim3_fan (V,E) (x:real^3#real^3) = rhazim_fan (V,E) (inverse (f_fan_pair_ext (V,E)) x)`;;
(* All variables must be positive without any side conditions *)
let sol_fan = new_definition `sol_fan (V,E) f = abs (sum f (\x. azim_dart (V,E) x - pi) + &2 * pi)`;;
let tau_fan = new_definition `tau_fan (V,E) f = abs (tauVEF (V,E,f))`;;
(* A diagonal *)
let y4'_fan = new_definition `y4'_fan (V,E) (x:real^3#real^3) = dist (SND x, FST (inverse (f_fan_pair_ext (V,E)) x))`;;
let y7_fan = new_definition 
	`y7_fan (V,E) (x:real^3#real^3) = norm (FST ((inverse (f_fan_pair_ext (V,E)) POWER 2) x))`;;
let fan_defs =
[
  azim2_fan; azim3_fan; yn_fan; ln_fan; ye_fan;
  rho_fan; sol_fan; tau_fan; rhazim_fan; rhazim2_fan; rhazim3_fan;
  y1_fan; y2_fan; y3_fan; y4_fan; y5_fan; y6_fan; y8_fan; y9_fan; y4'_fan;
]


(* Variables for lists *)
(* g - an isomorphism from hypermap_of_list to hypermap_of_fan *)
(* fan = (V,E) - a fan *)
(* g x = h (FST x), h (SND x) *)

let list_defs = map new_definition
  [
    `azim_list (g,fan) = (azim_dart fan o g):num#num->real`;
    `azim2_list (g,fan) = (azim2_fan fan o g):num#num->real`;
    `azim3_list (g,fan) = (azim3_fan fan o g):num#num->real`;
    `yn_list h = (yn_fan o h):num->real`;
    `ln_list h = (ln_fan o h):num->real`;
    `rho_list h = (rho_fan o h):num->real`;
    `rhazim_list (g,fan) = (rhazim_fan fan o g):num#num->real`;
    `rhazim2_list (g,fan) = (rhazim2_fan fan o g):num#num->real`;
    `rhazim3_list (g,fan) = (rhazim3_fan fan o g):num#num->real`;
    `(ye_list g):(num#num->real) = ye_fan o g`;
    `(sol_list (g,fan)):(num#num->bool)->real = sol_fan fan o IMAGE g`;
    `(tau_list (g,fan)):(num#num->bool)->real = tau_fan fan o IMAGE g`;
    `(y1_list g):(num#num->real) = y1_fan o g`;
    `(y2_list g):(num#num->real) = y2_fan o g`;
    `(y3_list (g,fan)):(num#num->real) = y3_fan fan o g`;
    `(y4_list (g,fan)):(num#num->real) = y4_fan fan o g`;
    `(y5_list (g,fan)):(num#num->real) = y5_fan fan o g`;
    `(y6_list g):(num#num->real) = y6_fan o g`;
    `(y8_list (g,fan)):(num#num->real) = y8_fan fan o g`;
    `(y9_list (g,fan)):(num#num->real) = y9_fan fan o g`;
    `(y4'_list (g,fan)):(num#num->real) = y4'_fan fan o g`;
  ];;


let list_defs2 = map (REWRITE_RULE[FUN_EQ_THM; o_THM]) list_defs;;

let list_defs_th = end_itlist CONJ list_defs;;

let list_var_rewrites =
  map GSYM list_defs @ map GSYM list_defs2;;


(* All variables are nonnegative *)

let AZIM_DART_POS = 
prove(`&0 <= azim_dart (V,E) x`,

   MP_TAC (ISPEC `x:real^3#real^3` PAIR_SURJECTIVE) THEN
     STRIP_TAC THEN
     ASM_REWRITE_TAC[azim_dart] THEN
     COND_CASES_TAC THENL
     [
       MP_TAC PI_APPROX_32 THEN REAL_ARITH_TAC;
       ALL_TAC
     ] THEN
     REWRITE_TAC[azim_fan] THEN
     COND_CASES_TAC THEN REWRITE_TAC[azim] THEN
     MP_TAC PI_APPROX_32 THEN REAL_ARITH_TAC);;

let DIST_POS = 
prove(`!x:(real^3#real^3). &0 <= dist x`,

   GEN_TAC THEN MP_TAC (ISPEC `x:real^3#real^3` PAIR_SURJECTIVE) THEN
     STRIP_TAC THEN ASM_REWRITE_TAC[dist; NORM_POS_LE]);;

let list_var_pos = map (fun tm -> prove(tm,
			GEN_TAC THEN REWRITE_TAC list_defs2 THEN 
			  MP_TAC (ISPEC `fan:(real^3->bool)#((real^3->bool)->bool)` PAIR_SURJECTIVE) THEN
			  STRIP_TAC THEN ASM_REWRITE_TAC fan_defs THEN
			  TRY (MATCH_MP_TAC REAL_LE_MUL) THEN
			  REWRITE_TAC[AZIM_DART_POS; REAL_ABS_POS; NORM_POS_LE; DIST_POS; Fnjlbxs.lmfun_ge0]))
[
  `!x. &0 <= azim_list (g,fan) x`;
  `!x. &0 <= azim2_list (g,fan) x`;
  `!x. &0 <= azim3_list (g,fan) x`;
  `!x. &0 <= rhazim_list (g,fan) x`;
  `!x. &0 <= rhazim2_list (g,fan) x`;
  `!x. &0 <= rhazim3_list (g,fan) x`;
  `!v. &0 <= yn_list h v`;
  `!v. &0 <= ln_list h v`;
  `!v. &0 <= rho_list h v`;
  `!f. &0 <= sol_list (g,fan) f`;
  `!f. &0 <= tau_list (g,fan) f`;
  `!x. &0 <= ye_list g x`;
  `!x. &0 <= y1_list g x`;
  `!x. &0 <= y2_list g x`;
  `!x. &0 <= y3_list (g,fan) x`;
  `!x. &0 <= y4_list (g,fan) x`;
  `!x. &0 <= y5_list (g,fan) x`;
  `!x. &0 <= y6_list g x`;
  `!x. &0 <= y8_list (g,fan) x`;
  `!x. &0 <= y9_list (g,fan) x`;
  `!x. &0 <= y4'_list (g,fan) x`;
];;


end;;