needs "../formal_lp/hypermap/ineqs/lp_ineqs_proofs-compiled.hl";;
needs "../formal_lp/hypermap/ineqs/lp_ineqs_proofs2-compiled.hl";;
needs "../formal_lp/hypermap/ineqs/lp_main_estimate-compiled.hl";;
needs "../formal_lp/hypermap/ineqs/lp_ineqs.hl";;
needs "../formal_lp/hypermap/ineqs/lp_body_ineqs_data.hl";;

module Lp_body_ineqs = struct

open Lp_ineqs_proofs;;
open Lp_ineqs_proofs2;;
open Lp_main_estimate;;
open Sphere;;
open Tame_general;;
open Lp_ineqs;;

let special_list =
  let r = add_lp_hyp true in
    [
      "ineq71", (r ineq71, TRUTH);
      "ineq72", (r ineq72, TRUTH);
      "ineq73", (r ineq73, TRUTH);
      "ineq74", (r ineq74, TRUTH);
      "ineq77", (r ineq77, r ineq77_std);
      "ineq89", (r ineq89, r ineq89_std);
      "ineq90", (r ineq90, r ineq90_std);
      "ineq104", (r ineq104, r ineq104_std);
      "ineq105", (r ineq105, r ineq105_std);
      "ineq106", (r ineq106, r ineq106_std);
      "ineq118", (r ineq_tau4_diag3, r ineq_tau4_diag3_std);
      "ineq119", (r ineq119, r ineq119_std);
      "ineq120", (r ineq120, r ineq120_std);
      "ineq121", (r ineq121, r ineq121_std);
      "ineq122", (r ineq122, r ineq122_std);
    ];;

(**********************)

let DECIMAL_EQ = ARITH_RULE `#2.0 = &2 /\ #2.00 = &2 /\ #2 = &2 /\ #3.0 = &3`;;

let REAL_GT_IMP_GE = ARITH_RULE `a > b ==> a >= b:real`;;

let dih2_y_eq_dih3_y = prove(`dih2_y y1 y2 y3 y4 y5 y6 = dih3_y y1 y3 y2 y4 y6 y5`,
			     REWRITE_TAC[dih2_y; dih3_y]);;

let dih3_y_eq_dih2_y = prove(`dih3_y y1 y2 y3 y4 y5 y6 = dih2_y y1 y3 y2 y4 y6 y5`,
			     REWRITE_TAC[dih2_y; dih3_y]);;

let rhazim2_eq_rhazim3 = prove(`rhazim2 y1 y2 y3 y4 y5 y6 = rhazim3 y1 y3 y2 y4 y6 y5`,
			     REWRITE_TAC[rhazim2; rhazim3; node2_y; node3_y; rhazim; Nonlinear_lemma.dih_y_sym]);;


let rhazim3_eq_rhazim2 = prove(`rhazim3 y1 y2 y3 y4 y5 y6 = rhazim2 y1 y3 y2 y4 y6 y5`,
			     REWRITE_TAC[rhazim2; rhazim3; node2_y; node3_y; rhazim; Nonlinear_lemma.dih_y_sym]);;


let inst_list = [
  `y1_fan d`, `y1:real`;
  `y2_fan d`, `y2:real`;
  `y3_fan (V,E) d`, `y3:real`;
  `y4'_fan (V,E) d`, `y4:real`;
  `y5_fan (V,E) d`, `y5:real`;
  `y6_fan d`, `y6:real`;
  `y7_fan (V,E) d`, `y7:real`;
  `y8_fan (V,E) d`, `y8:real`;
  `y9_fan (V,E) d`, `y9:real`;
];;


let inst_sym_list = [
  `y1_fan d`, `y1:real`;
  `y3_fan (V,E) d`, `y2:real`;
  `y2_fan d`, `y3:real`;
  `y4'_fan (V,E) d`, `y4:real`;
  `y6_fan d`, `y5:real`;
  `y5_fan (V,E) d`, `y6:real`;
];;


let r = UNDISCH o SPEC_ALL o add_lp_hyp true;;
let eq_ths = map r [
  GSYM azim_fan_eq_dih_y;
  GSYM rhazim_fan_eq_rhazim;
];;

let eq3_ths = map r [
  y4'_eq_y4;
  GSYM dart3_azim2_fan_eq_dih2_y;
  GSYM dart3_azim3_fan_eq_dih3_y;
  GSYM dart3_rhazim2_fan_eq_rhazim2;
  GSYM dart3_rhazim3_fan_eq_rhazim3;
  GSYM dart3_sol_fan_eq_sol;
  GSYM dart3_tau_fan_eq_taum;
] @ eq_ths;;

let eq4_ths = map r [
  GSYM dart4_tau_fan_eq_tauq;
] @ eq_ths;;


let bounds_gen_ths = map r [
  y1_lo; y2_lo; y3_lo; y4_lo; y5_lo; y6_lo; y8_lo; y9_lo;
  y1_hi; y2_hi; y3_hi;
  y4'_lo; y7_lo; y7_hi;
];;

let bounds_std_ths = map r [
  y4_hi_std; y5_hi_std; y6_hi_std; y8_hi_std; y9_hi_std;
  y4_hi_std2; y5_hi_std2; y6_hi_std2;
];;

let mk_darts_k_subset_th k =
  let eq_th = add_lp_hyp false Hypermap_and_fan.COMPONENTS_HYPERMAP_OF_FAN in
    (UNDISCH_ALL o REWRITE_RULE[eq_th] o SPEC_ALL o ISPECL[`hypermap_of_fan (V,E)`; mk_small_numeral k])
      Lp_gen_theory.darts_k_subset;;

type lp_data = {
  d_in_tm : term;
  eq_ths : thm list;
  in_th : thm;
};;

let mk_lp_data (tm, eq_ths, in_th) =
  {d_in_tm = tm; eq_ths = eq_ths; in_th = in_th};;

let lp_data = [
  "dart", mk_lp_data (`(d:real^3#real^3) IN dart_of_fan (V,E)`, eq_ths, TRUTH);
  "dart3", mk_lp_data (`(d:real^3#real^3) IN darts_k 3 (hypermap_of_fan (V,E))`, eq3_ths, mk_darts_k_subset_th 3);
  "dart4", mk_lp_data (`(d:real^3#real^3) IN darts_k 4 (hypermap_of_fan (V,E))`, eq4_ths, mk_darts_k_subset_th 4);
];;



let normalize_ineq =
  let normalize th =
    if is_binary "real_gt" (concl th) then
      MATCH_MP REAL_GT_IMP_GE th
    else if is_binary "real_lt" (concl th) then
      MATCH_MP REAL_LT_IMP_LE th
    else
      th in
    fun th ->
      if is_imp (concl th) then
	let p_tm, _ = dest_imp (concl th) in
	let th2 = normalize (UNDISCH th) in
	  DISCH p_tm th2
      else
	normalize th;;

let finalize_th data th =
  let th1 = PROVE_HYP data.in_th th in
  let th2 = normalize_ineq th1 in
  let th3 = (PURE_REWRITE_RULE[GSYM IMP_IMP] o GEN `d:real^3#real^3` o DISCH data.d_in_tm) th2 in
    add_lp_ineqs_hyp th3;;


(* set name, (set definitional theorem, corresponding lp set, generate std flag *)
let ineq_sets = [
  "apex_std3_hll", (Ineq.apex_std3_hll, "dart3", true);
  "apex_flat_h", (Ineq.apex_flat_h, "dart3", false);
  "apex_flat_l", (Ineq.apex_flat_l, "dart3", false);
  "apex_flat_hll", (Ineq.apex_flat_hll, "dart3", false);
  "apex_flat", (Ineq.apex_flat, "dart3", false);
  "apex_std3_lhh", (Ineq.apex_std3_lhh, "dart3", true);
  "apex_sup_flat", (Ineq.apex_sup_flat, "dart3", false);
  "dart_mll_n", (Ineq.dart_mll_n, "dart3", true);
  "dart_mll_w", (Ineq.dart_mll_w, "dart3", true);
  "apex_std3_lll_wxx", (Ineq.apex_std3_lll_wxx, "dart3", true);
  "apex_std3_lll_xww", (Ineq.apex_std3_lll_xww, "dart3", true);
  "apex_std3_small_hll", (Ineq.apex_std3_small_hll, "dart3", true);
  "dart_std3_mini", (Ineq.dart_std3_mini, "dart3", true);
  "dart_std3_lw", (Ineq.dart_std3_lw, "dart3", true);
  "dart_std3", (Ineq.dart_std3, "dart3", true);
  "dart_Hll_w", (Ineq.dart_Hll_w, "dart3", true);
  "dart_Hll_n", (Ineq.dart_Hll_n, "dart3", true);
  "apexfA", (Ineq.apexfA, "dart3", false);
  "apexffA", (Ineq.apexffA, "dart3", false);
  "apex_A", (Ineq.apex_A, "dart3", false);
  "dart_std3_big_200_218", (Ineq.dart_std3_big_200_218, "dart3", true);
  "dart_std3_big", (REWRITE_RULE[GSYM Ineq.dart_std3_big] Ineq.dart_std3, "dart3", true);
  "dart_std3_small", (Ineq.dart_std3_small, "dart3", true);
  "dart4_diag3", (Ineq.dart4_diag3, "dart4", true);
  "dartY", (Ineq.dartY, "dart", false);
  "dartX", (Ineq.dartX, "dart", false);
];;


let gen_body_ineq_ths sym_flag ineq_id set_name =
  let ineq_domain_th, lp_set, std_flag = assoc set_name ineq_sets in
  let data = assoc lp_set lp_data in

  let ineq = (hd o Ineq.getexact) ineq_id in
  let th0 = (SPEC_ALL o ASSUME) (ineq.ineq) in
  let th1 = 
    if sym_flag then
      let t1 = INST inst_sym_list th0 in
	ONCE_REWRITE_RULE[Nonlinear_lemma.dih_y_sym; dih2_y_eq_dih3_y; dih3_y_eq_dih2_y; rhazim2_eq_rhazim3; rhazim3_eq_rhazim2] t1
    else
      INST inst_list th0 in

  let th2 = REWRITE_RULE data.eq_ths th1 in
  let th3 = REWRITE_RULE[ALL; INEQ_ALT; ineq_domain_th; DECIMAL_EQ] th2 in

  let gen_th1 = REWRITE_RULE bounds_gen_ths th3 in
  let gen_th = finalize_th data gen_th1 in
  let std_th =
    if std_flag then
      let std_th1 = REWRITE_RULE bounds_std_ths gen_th1 in
	finalize_th data std_th1
    else
      TRUTH in
    gen_th, std_th;;




(*********************)


let add_body_ineqs () =
  let test (name, _, _) = true in
  let data = filter test Lp_body_ineqs_data.data in
  let sym_data = filter test Lp_body_ineqs_data.sym_data in

  let report s =
    Format.print_string s; Format.print_newline(); Format.print_flush() in
  let counter = ref 0 and
      total = length data + length sym_data in

  let add sym_flag (lp_name, ineq_id, set_name) =
    let _ = counter := !counter + 1 in
    let _ = report (sprintf "Adding %s (%d / %d)" lp_name !counter total) in
    let gen_th, std_th = 
		try assoc lp_name special_list
			with Failure _ -> gen_body_ineq_ths sym_flag ineq_id set_name in
    let _ = add_lp_ineq_th (lp_name, false, gen_th) in
    let _ = if std_th <> TRUTH then add_lp_ineq_th (lp_name, true, std_th) else () in
      () in

  let _ = map (add false) data in
  let _ = map (add true) sym_data in
    ();;

end;;