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 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;;