needs "../formal_lp/hypermap/ineqs/lp_ineqs.hl";;


module Lp_head_ineqs = struct

open Lp_ineqs;;

let add_head_ineqs () =
  let _ = map add_lp_ineq_str
  [
    "azim_lo", false, 
		"!d. d IN dart H ==> &0 <= azim_mod d", 
		Some Lp_ineqs_proofs.azim_lo;
		
    "azim_hi", false, 
		"!d. d IN dart H ==> azim_mod d <= pi", 
		Some Lp_ineqs_proofs.azim_hi;
		
    "azim2_lo", false, 
		"!d. d IN dart H ==> &0 <= azim2_mod d", 
		Some Lp_ineqs_proofs.azim2_lo;
		
    "azim2_hi", false, 
		"!d. d IN dart H ==> azim2_mod d <= pi", 
		Some Lp_ineqs_proofs.azim2_hi;
		
    "azim3_lo", false, 
		"!d. d IN dart H ==> &0 <= azim3_mod d", 
		Some Lp_ineqs_proofs.azim3_lo;
		
    "azim3_hi", false, 
		"!d. d IN dart H ==> azim3_mod d <= pi", 
		Some Lp_ineqs_proofs.azim3_hi;
		
    "rhazim_lo", false, 
		"!d. d IN dart H ==> &0 <= rhazim_mod d", 
		Some Lp_ineqs_proofs.rhazim_lo;
		
    "rhazim_hi", false, 
		"!d. d IN dart H ==> rhazim_mod d <= pi + sol0", 
		Some Lp_ineqs_proofs.rhazim_hi;
		
    "rhazim2_lo", false, 
		"!d. d IN dart H ==> &0 <= rhazim2_mod d", 
		Some Lp_ineqs_proofs.rhazim2_lo;
		
    "rhazim2_hi", false, 
		"!d. d IN dart H ==> rhazim2_mod d <= pi + sol0", 
		Some Lp_ineqs_proofs.rhazim2_hi;
		
    "rhazim3_lo", false, 
		"!d. d IN dart H ==> &0 <= rhazim3_mod d", 
		Some Lp_ineqs_proofs.rhazim3_lo;
		
    "rhazim3_hi", false, 
		"!d. d IN dart H ==> rhazim3_mod d <= pi + sol0", 
		Some Lp_ineqs_proofs.rhazim3_hi;

    "ln_lo", false, 
		"!x. x IN V ==> &0 <= ln_mod x", 
		Some Lp_ineqs_proofs.ln_lo;
		
    "ln_hi", false, 
		"!x. x IN V ==> ln_mod x <= &1", 
		Some Lp_ineqs_proofs.ln_hi;
		
    "rho_lo", false, 
		"!x. x IN V ==> &1 <= rho_mod x", 
		Some Lp_ineqs_proofs.rho_lo;
		
    "rho_hi", false, 
		"!x. x IN V ==> rho_mod x <= &1 + sol0 / pi", 
		Some Lp_ineqs_proofs.rho_hi;
		
    "yn_lo", false, 
		"!x. x IN V ==> &2 <= yn_mod x", 
		Some Lp_ineqs_proofs.yn_lo;
		
    "yn_hi", false, 
		"!x. x IN V ==> yn_mod x <= #2.52", 
		Some Lp_ineqs_proofs.yn_hi;

    "ye_lo", false, 
		"!d. d IN dart H ==> &2 <= ye_mod d", 
		Some Lp_ineqs_proofs.ye_lo;
		
    "ye_hi", false, 
		"!d. d IN dart H ==> ye_mod d <= &3 ==> ye_mod d <= &3", 
		None;
		
    "ye_hi", true, 
		"!d. d IN dart H ==> ye_mod d <= &3", 
		Some Lp_ineqs_proofs.ye_hi_std;

    "y1_lo", false, 
		"!d. d IN dart H ==> &2 <= y1_mod d", 
		Some Lp_ineqs_proofs.y1_lo;
		
    "y1_hi", false, 
		"!d. d IN dart H ==> y1_mod d <= #2.52", 
		Some Lp_ineqs_proofs.y1_hi;
		
    "y2_lo", false, 
		"!d. d IN dart H ==> &2 <= y2_mod d", 
		Some Lp_ineqs_proofs.y2_lo;
		
    "y2_hi", false, 
		"!d. d IN dart H ==> y2_mod d <= #2.52", 
		Some Lp_ineqs_proofs.y2_hi;
		
    "y3_lo", false, 
		"!d. d IN dart H ==> &2 <= y3_mod d", 
		Some Lp_ineqs_proofs.y3_lo;
		
    "y3_hi", false, 
		"!d. d IN dart H ==> y3_mod d <= #2.52", 
		Some Lp_ineqs_proofs.y3_hi;
		
    "y4_lo", false, 
		"!d. d IN dart H ==> &2 <= y4_mod d", 
		Some Lp_ineqs_proofs.y4_lo;
		
    "y5_lo", false, 
		"!d. d IN dart H ==> &2 <= y5_mod d", 
		Some Lp_ineqs_proofs.y5_lo;
		
    "y6_lo", false, 
		"!d. d IN dart H ==> &2 <= y6_mod d", 
		Some Lp_ineqs_proofs.y6_lo;
		
    "y8_lo", false, 
		"!d. d IN dart H ==> &2 <= y8_mod d", 
		Some Lp_ineqs_proofs.y8_lo;
		
    "y9_lo", false, 
		"!d. d IN dart H ==> &2 <= y9_mod d", 
		Some Lp_ineqs_proofs.y9_lo;
		
    "y4_hi", false, 
		"!d. d IN dart H ==> y4_mod d <= &3 ==> y4_mod d <= &3", 
		None;
		
    "y5_hi", false, 
		"!d. d IN dart H ==> y5_mod d <= &3==> y5_mod d <= &3", 
		None;
		
    "y6_hi", false, 
		"!d. d IN dart H ==> y6_mod d <= &3==> y6_mod d <= &3", 
		None;
		
    "y8_hi", false, 
		"!d. d IN dart H ==> y8_mod d <= #2.52==> y8_mod d <= #2.52", 
		None;
		
    "y9_hi", false, 
		"!d. d IN dart H ==> y9_mod d <= #2.52==> y9_mod d <= #2.52", 
		None;
		
    "y4_hi", true, 
		"!d. d IN dart H ==> y4_mod d <= &3", 
		Some Lp_ineqs_proofs.y4_hi_std;
		
    "y5_hi", true, 
		"!d. d IN dart H ==> y5_mod d <= &3", 
		Some Lp_ineqs_proofs.y5_hi_std;
		
    "y6_hi", true, 
		"!d. d IN dart H ==> y6_mod d <= &3", 
		Some Lp_ineqs_proofs.y6_hi_std;
		
    "y8_hi", true, 
		"!d. d IN dart H ==> y8_mod d <= #2.52", 
		Some Lp_ineqs_proofs.y8_hi_std;
		
    "y9_hi", true, 
		"!d. d IN dart H ==> y9_mod d <= #2.52", 
		Some Lp_ineqs_proofs.y9_hi_std;

    "sol_lo", false, 
		"!f. f IN face_set H ==> &0 <= sol_mod f", 
		Some Lp_ineqs_proofs.sol_lo;
		
    "sol_hi", false, 
		"!f. f IN face_set H ==> sol_mod f <= &4 * pi", 
		Some Lp_ineqs_proofs.sol_hi;
		
    "tau_lo", false, 
		"!f. f IN face_set H ==> &0 <= tau_mod f", 
		Some Lp_ineqs_proofs.tau_lo;
		
    "tau_hi", false, 
		"!f. f IN face_set H ==> tau_mod f <= tgt", 
		Some Lp_ineqs_proofs.tau_hi;

    "azim_sum", false, 
		"!n. n IN node_set H ==> sum n azim_mod = &2 * pi", 
		Some Lp_ineqs_proofs.azim_sum;
		
    "rhazim_sum", false, 
		"!n. n IN node_set H ==> sum n rhazim_mod = &2 * pi * rho_mod (node_mod (CHOICE n))", 
                Some Lp_ineqs_proofs.rhazim_sum;

    "sol_sum3", false, 
		"!f. f IN face_set H ==> (CARD f = 3 ==> sum f azim_mod = sol_mod f + pi)", 
		Some Lp_ineqs_proofs.sol_sum3;
		
    "sol_sum4", false, 
		"!f. f IN face_set H ==> (CARD f = 4 ==> sum f azim_mod = sol_mod f + &2 * pi)",
		Some Lp_ineqs_proofs.sol_sum4;
		
    "sol_sum5", false, 
		"!f. f IN face_set H ==> (CARD f = 5 ==> sum f azim_mod = sol_mod f + &3 * pi)",
		Some Lp_ineqs_proofs.sol_sum5;
		
    "sol_sum6", false, 
		"!f. f IN face_set H ==> (CARD f = 6 ==> sum f azim_mod = sol_mod f + &4 * pi)",
		Some Lp_ineqs_proofs.sol_sum6;
		
    "tau_sum3", false, 
		"!f. f IN face_set H ==> (CARD f = 3 ==> sum f rhazim_mod = tau_mod f + (pi + sol0))",
		Some Lp_ineqs_proofs.tau_sum3;
		
    "tau_sum4", false, 
		"!f. f IN face_set H ==> (CARD f = 4 ==> sum f rhazim_mod = tau_mod f + &2 * (pi + sol0))",
		Some Lp_ineqs_proofs.tau_sum4;
		
    "tau_sum5", false, 
		"!f. f IN face_set H ==> (CARD f = 5 ==> sum f rhazim_mod = tau_mod f + &3 * (pi + sol0))",
		Some Lp_ineqs_proofs.tau_sum5;
		
    "tau_sum6", false, 
		"!f. f IN face_set H ==> (CARD f = 6 ==> sum f rhazim_mod = tau_mod f + &4 * (pi + sol0))",
		Some Lp_ineqs_proofs.tau_sum6;

    "ln_def", false, 
		"!x. x IN V ==> ln_mod x = (#2.52 - yn_mod x) / #0.52", 
		Some Lp_ineqs_proofs.ln_def;
    "rho_def", false, 
		"!x. x IN V ==> rho_mod x = (&1 + sol0 / pi) - ln_mod x * sol0 / pi", 
		Some Lp_ineqs_proofs.rho_def;
    "edge_sym", false, 
		"!d. d IN dart H ==> ye_mod d = ye_mod (edge_map H d):real", 
		Some Lp_ineqs_proofs.edge_sym;

    "y1_def", false, 
		"!d. d IN dart H ==> y1_mod d = yn_mod (node_mod d):real", 
		Some Lp_ineqs_proofs.y1_def;
		
    "y2_def", false, 
		"!d. d IN dart H ==> y2_mod d = yn_mod (node_mod (face_map H d)):real", 
		Some Lp_ineqs_proofs.y2_def;
		
    "y3_def", false, 
		"!d. d IN dart H ==> y3_mod d = yn_mod (node_mod (inverse (face_map H) d)):real", 
		Some Lp_ineqs_proofs.y3_def;
		
    "y4_def", false, 
		"!d. d IN dart H ==> y4_mod d = ye_mod (face_map H d):real", 
		Some Lp_ineqs_proofs.y4_def;

    "y5_def", false, 
		"!d. d IN dart H ==> y5_mod d = ye_mod (inverse (face_map H) d):real", 
		Some Lp_ineqs_proofs.y5_def;
		
    "y6_def", false, 
		"!d. d IN dart H ==> y6_mod d = ye_mod d:real", 
		Some Lp_ineqs_proofs.y6_def;
		
    "y8_def", false, 
		"!d. d IN dart H ==> y8_mod d = y5_mod (inverse (face_map H) d):real", 
		Some Lp_ineqs_proofs.y8_def;
		
    "y9_def", false, 
		"!d. d IN dart H ==> y9_mod d = ye_mod (face_map H d):real", 
		Some Lp_ineqs_proofs.y9_def;

    "azim2c", false, 
		"!d. d IN dart H ==> azim2_mod d = azim_mod (face_map H d):real", 
		Some Lp_ineqs_proofs.azim2c;
		
    "azim3c", false, 
		"!d. d IN dart H ==> azim3_mod d = azim_mod (inverse (face_map H) d):real", 
		Some Lp_ineqs_proofs.azim3c;
		
    "rhazim2c", false, 
		"!d. d IN dart H ==> rhazim2_mod d = rhazim_mod (face_map H d):real",
		Some Lp_ineqs_proofs.rhazim2c;
		
    "rhazim3c", false, 
		"!d. d IN dart H ==> rhazim3_mod d = rhazim_mod (inverse (face_map H) d):real", 
		Some Lp_ineqs_proofs.rhazim3c;

    "RHA", false, 
		"!d. d IN dart H ==> rhazim_mod d >= azim_mod d:real", 
		Some Lp_ineqs_proofs.RHA;
		
    "RHB", false, 
		"!d. d IN dart H ==> rhazim_mod d <= azim_mod d * (&1 + sol0 / pi)", 
		Some Lp_ineqs_proofs.RHB;

    "RHBLO", false, 
		"!d. d IN dart H ==> yn_mod (node_mod d) <= #2.18 ==> rhazim_mod d <= azim_mod d * rho218", 
		Some Lp_ineqs_proofs.RHBLO;

    "RHBHI", false, 
		"!d. d IN dart H ==> #2.18 <= yn_mod (node_mod d) ==> rhazim_mod d >= azim_mod d * rho218", 
		Some Lp_ineqs_proofs.RHBHI;

    "yy1", false,
                "!d. d IN darts_k 3 H ==> #6.25 <= y4_mod d + y5_mod d + y6_mod d ==> #6.25 <= y4_mod d + y5_mod d + y6_mod d",
                None;

    "yy2", false,
                "!d. d IN darts_k 3 H ==> y4_mod d + y5_mod d + y6_mod d <= #6.25 ==> y4_mod d + y5_mod d + y6_mod d <= #6.25",
                None;

    "yy3", false,
                "!x. x IN V ==> #2.18 <= yn_mod x ==> #2.18 <= yn_mod x",
                None;

    "yy4", false,
                "!x. x IN V ==> yn_mod x <= #2.18 ==> yn_mod x <= #2.18",
                None;

    "yy5", false,
                "!x. x IN V ==> #2.36 <= yn_mod x ==> #2.36 <= yn_mod x",
                None;

    "yy6", false,
                "!x. x IN V ==> yn_mod x <= #2.36 ==> yn_mod x <= #2.36",
                None;

    "yy7", false,
                "!x. x IN V ==> #2.18 <= yn_mod x ==> #2.18 <= yn_mod x",
                None;

    "yy8", false, 
		"!d. d IN dart H ==> #2.25 <= ye_mod d ==> #2.25 <= ye_mod d", 
		None;

    "yy9", false, 
		"!d. d IN dart H ==> ye_mod d <= #2.25 ==> ye_mod d <= #2.25", 
		None;

    "yy10", false, 
		"!d. d IN dart H ==> ye_mod d <= #2.52 ==> ye_mod d <= #2.52", 
		None;
		
    "yy10", true, 
		"!d. d IN dart H ==> ye_mod d <= #2.52", 
		Some Lp_ineqs_proofs.yy10_std;

    "yy11", false,
                "!d. d IN darts_k 3 H ==> #2.52 <= y4_mod d ==> #2.52 <= y4_mod d",
                None;

    "yy12", false,
                "!d. d IN darts_k 3 H ==> sqrt8 <= y4_mod d ==> sqrt8 <= y4_mod d",
                None;

    "yy13", false,
                "!d. d IN darts_k 3 H ==> y5_mod d <= #2.52 ==> y5_mod d <= #2.52",
                None;

    "yy14", false,
                "!d. d IN darts_k 3 H ==> y6_mod d <= #2.52 ==> y6_mod d <= #2.52",
                None;
		
    "yy15", false, 
		"!d. d IN darts_k 3 H ==> y4_mod d <= sqrt8 ==> y4_mod d <= sqrt8", 
		None;
  ] in
    (* The main inequality *)
  let main_ineq = 
    let th1 = (add_lp_hyp false o UNDISCH_ALL o SPEC_ALL) Lp_ineqs_proofs.lnsum_ineq in
      (* Add an artificial ALL statement *)
      (REWRITE_RULE[ALL_MEM] o GEN `v:num` o DISCH `MEM (v:num) (list_of_elements L)`) th1 in
  let _ = add_lp_list_ineq ("main", false, main_ineq) in

  (* Main estimate inequalities *)
  let _ = map add_lp_ineq_th
  [
    "tau3", false, Lp_main_estimate.ineq_tau3;
    "tau4", false, Lp_main_estimate.ineq_tau4;
    "tau5", false, Lp_main_estimate.ineq_tau5;
    "tau6", false, Lp_main_estimate.ineq_tau6;
    "tau4", true, Lp_main_estimate.ineq_tau4_std;
    "tau5", true, Lp_main_estimate.ineq_tau5_std;
    "tau6", true, Lp_main_estimate.ineq_tau6_std;
    "tauB5h", false, Lp_main_estimate.ineq_tau5_pro;
    "tauB4h", false, Lp_main_estimate.ineq_tau4_pro;
    "tau5h", false, Lp_main_estimate.ineq_tau5_diags;
    "tau5h", true, Lp_main_estimate.ineq_tau5_diags_std;
  ] in
  let crossdiag_ineq = (add_lp_hyp true o UNDISCH_ALL o SPEC_ALL o REWRITE_RULE[GSYM IMP_IMP]) Lp_ineqs_proofs2.crossdiag_list in
  let _ = add_lp_list_ineq ("crossdiag", false, crossdiag_ineq) in

  let _ = add_lp_ineq_th ("perimZ", false, Lp_ineqs_proofs2.perimZ) in
  let _ = add_lp_ineq_th ("perimZ", true, Lp_ineqs_proofs2.perimZ_std) in

  let yapex_sup_flat = (add_lp_hyp true o UNDISCH_ALL o SPEC_ALL o REWRITE_RULE[GSYM IMP_IMP] o Hypermap_and_fan.let_RULE)
    Lp_ineqs_proofs2.yapex_sup_flat_list in
  let _ = add_lp_list_ineq ("yapex_sup_flat", false, yapex_sup_flat) in
    ();;

end;;