needs "../formal_lp/hypermap/ineqs/lp_ineqs_defs.hl";;
needs "../formal_lp/hypermap/ineqs/lp_gen_theory-compiled.hl";;
module Lp_gen_ineqs = struct
open Lp_ineqs_def;;
open Hypermap_and_fan;;
open Hypermap_iso;;
open List_hypermap;;
open Lp_gen_theory;;
(* mod-file variables and definitions *)
let var_inst_list =
let sets =
[
"dart", `:real^3#real^3`;
"face", `:real^3#real^3->bool`;
"node", `:real^3`;
] in
let mk_mod name set = mk_var (name, mk_fun_ty (assoc set sets) `:real`) in
[
`hypermap_of_fan (V,E)`, `H:(real^3#real^3)hypermap`;
`FST:real^3#real^3->real^3`, `node_mod:real^3#real^3->real^3`;
`azim_dart (V,E)`, mk_mod "azim_mod" "dart";
`azim2_fan (V,E)`, mk_mod "azim2_mod" "dart";
`azim3_fan (V,E)`, mk_mod "azim3_mod" "dart";
`rhazim_fan (V,E)`, mk_mod "rhazim_mod" "dart";
`rhazim2_fan (V,E)`, mk_mod "rhazim2_mod" "dart";
`rhazim3_fan (V,E)`, mk_mod "rhazim3_mod" "dart";
`ln_fan`, mk_mod "ln_mod" "node";
`yn_fan`, mk_mod "yn_mod" "node";
`rho_fan`, mk_mod "rho_mod" "node";
`ye_fan`, mk_mod "ye_mod" "dart";
`y1_fan`, mk_mod "y1_mod" "dart";
`y2_fan`, mk_mod "y2_mod" "dart";
`y3_fan (V,E)`, mk_mod "y3_mod" "dart";
`y4_fan (V,E)`, mk_mod "y4_mod" "dart";
`y5_fan (V,E)`, mk_mod "y5_mod" "dart";
`y6_fan`, mk_mod "y6_mod" "dart";
`y8_fan (V,E)`, mk_mod "y8_mod" "dart";
`y9_fan (V,E)`, mk_mod "y9_mod" "dart";
`y4'_fan (V,E)`, mk_mod "y4'_mod" "dart";
`sol_fan (V,E)`, mk_mod "sol_mod" "face";
`tau_fan (V,E)`, mk_mod "tau_mod" "face";
];;
(*****************)
(* For a term in the form `!x. x IN set H ==> P x` returns a theorem
hyp_iso g (G,H), !x. x IN set H ==> P x |- !y. y IN set G ==> P (g y) *)
let get_iso_thm =
let iso_list0 =
[
`darts_k 6 (H:(A)hypermap)`, spec_var_th iso_darts_k_trans 0 `6`;
`darts_k 5 (H:(A)hypermap)`, spec_var_th iso_darts_k_trans 0 `5`;
`darts_k 4 (H:(A)hypermap)`, spec_var_th iso_darts_k_trans 0 `4`;
`darts_k 3 (H:(A)hypermap)`, spec_var_th iso_darts_k_trans 0 `3`;
`dart (H:(A)hypermap)`, iso_dart_trans;
`face_set (H:(A)hypermap)`, iso_face_trans;
`node_set (H:(A)hypermap)`, iso_node_trans;
`V:C->bool`, bij_trans;
] in
let cty = `:C` in
fun ineq ->
let x_tm, tm = dest_forall ineq in
let x_ty =
try (fst o dest_fun_ty o type_of) x_tm with Failure _ -> type_of x_tm in
let ty_list = [x_ty, aty; x_ty, cty] in
let iso_list = map (fun tm, th -> inst ty_list tm, INST_TYPE ty_list th) iso_list0 in
let set, p_tm' = dest_binary "==>" tm in
let set_th = assoc (rand set) iso_list in
let p_tm = mk_abs (x_tm, p_tm') in
let p_var = mk_var ("P", type_of (rand set)) in
let th1 = (SPEC_ALL o ONCE_REWRITE_RULE[RIGHT_IMP_FORALL_THM] o REWRITE_RULE[IMP_IMP]) set_th in
BETA_RULE (INST[p_tm, p_var] th1), ty_list;;
(* For an inequality term returns an isomorphism theorem *)
let build_iso_th =
let th_rule th = (UNDISCH_ALL o SPEC_ALL o REWRITE_RULE[RIGHT_IMP_FORALL_THM]) th in
let ths0 = [
th_rule components_iso_image;
th_rule hyp_iso_comm_special;
th_rule hyp_iso_inv_comm;
th_rule card_face_iso;
th_rule card_face_dart_iso;
th_rule sum_node_iso;
th_rule sum_face_iso;
] in
let sub_ths0 = [
`d IN darts_k 3 (G:(B)hypermap)`, (INST[`3`, `k:num`] o th_rule) darts_k_subset;
`d IN darts_k 4 (G:(B)hypermap)`, (INST[`4`, `k:num`] o th_rule) darts_k_subset;
`d IN darts_k 5 (G:(B)hypermap)`, (INST[`5`, `k:num`] o th_rule) darts_k_subset;
`d IN darts_k 6 (G:(B)hypermap)`, (INST[`6`, `k:num`] o th_rule) darts_k_subset;
] in
fun ineq ->
let iso_trans_th, ty_list = get_iso_thm ineq in
let th0 = UNDISCH_ALL (PURE_REWRITE_RULE[GSYM IMP_IMP] iso_trans_th) in
let gen_var, rtm = dest_forall(concl th0) in
let ths = map (INST_TYPE ty_list) ths0 and
sub_ths = map (fun tm, th -> inst ty_list tm, INST_TYPE ty_list th) sub_ths0 in
let ants = lhand rtm in
let th1 = UNDISCH (SPEC_ALL th0) in
(* General isomorphism rewrites *)
let th2 = PURE_REWRITE_RULE ths th1 in
let th3 =
try
let sub_th = assoc ants sub_ths in
PROVE_HYP sub_th th2
with Failure _ -> th2 in
GEN gen_var (DISCH ants th3);;
let build_list_th =
let th_rule = (UNDISCH_ALL o INST_TYPE [`:num`, aty; `:num`, `:D`; `:real^3`, `:C`] o
SPEC_ALL o REWRITE_RULE[GSYM IMP_IMP; RIGHT_IMP_FORALL_THM]) in
(* |- !d. d IN set_of_list s ==> P d <=> !d. MEM d s ==> P d *)
let ths_all = map th_rule
[
sum_node_list_all;
sum_face_list_all;
dart_list_all;
dart3_list_all;
dart4_list_all;
dart5_list_all;
dart6_list_all;
elements_list_all;
] in
let ths_more =
[
th_rule card_face_eq_length_find_face;
th_rule card_set_of_list_face;
th_rule card_set_of_list_node;
th_rule fst_choice_of_list_node;
UNDISCH_ALL (ISPEC `L:((num)list)list` components_hypermap_of_list);
th_rule e_list_ext_eq_e_list;
th_rule fst_iso_trans;
] in
let ths_mem =
[
`MEM (d:num#num) (list_of_darts3 L)`, th_rule list_of_darts3_subset;
`MEM (d:num#num) (list_of_darts4 L)`, th_rule list_of_darts4_subset;
`MEM (d:num#num) (list_of_darts5 L)`, th_rule list_of_darts5_subset;
`MEM (d:num#num) (list_of_darts6 L)`, th_rule list_of_darts6_subset;
] in
fun iso_th ->
(* G -> hypermap_of_list (L:((num)list)list) *)
let s1 = INST_TYPE [`:real^3#real^3`, aty; `:num#num`, bty; `:real^3`, `:C`; `:num`, `:D`] iso_th in
let s2 = INST[`hypermap_of_list (L:((num)list)list)`, `G:(num#num)hypermap`; `elements_of_list L:num->bool`, `R:num->bool`] s1 in
(* Convert conditions in the form !d. d IN set_of_list s to !d. MEM d s *)
let s3 = PURE_REWRITE_RULE ths_all s2 in
let gen_var2, rtm = dest_forall (concl s3) in
let ants2 = lhand rtm in
let s4 = UNDISCH (SPEC_ALL s3) in
(* Instantiate all variables *)
let s5 = INST var_inst_list s4 in
(* Additional rewrites *)
let s6 = PURE_REWRITE_RULE ths_more s5 in
let s7 =
try
let mem_th = assoc ants2 ths_mem in
PROVE_HYP mem_th s6
with Failure _ -> s6 in
let s8 = GEN gen_var2 (DISCH ants2 s7) in
let s9 = PURE_REWRITE_RULE list_var_rewrites s8 in
let s10 = PURE_REWRITE_RULE[ALL_MEM] s9 in
(* Rewrite the main inequality hypothesis with the COMPONENTS_HYPERMAP_OF_FAN theorem *)
let gen_hyp = find is_forall (hyp s10) in
let eq_th = REWRITE_CONV[UNDISCH_ALL (ISPECL [`V:real^3->bool`; `E:(real^3->bool)->bool`] COMPONENTS_HYPERMAP_OF_FAN)] gen_hyp in
let imp_th = if (rand (concl eq_th) = `T`) then EQT_ELIM eq_th else UNDISCH (MATCH_MP EQ_IMP (SYM eq_th)) in
PROVE_HYP imp_th s10;;
let generate_ineq ineq_tm =
let th1 = build_iso_th ineq_tm in
build_list_th th1;;
end;;
(*
open Lp_gen_ineqs;;
let test_ineq1 = `!d. d IN dart (H:(A)hypermap) ==> rhazim3_mod d <= pi + sol0`;;
let test_ineq2 = `!f. f IN face_set (H:(A)hypermap) ==> sol_mod f <= &4 * pi`;;
let test_ineq3 = `!f. f IN face_set (H:(A)hypermap) ==> (CARD f = 5 ==>
sum f azim_mod = sol_mod f + &3 * pi)`;;
let test_ineq4 = `!n. n IN node_set (H:(A)hypermap) ==> sum n azim_mod = &2 * pi`;;
let test_ineq5 = `!x. x IN (V:C->bool) ==> ln_mod x = (#2.52 - yn_mod x) / #0.52`;;
let edge_sym = `!d. d IN dart (H:(A)hypermap) ==> ye_mod d = ye_mod (edge_map H d):real`;;
let y1_def = `!d. d IN dart (H:(A)hypermap) ==> y1_mod d = yn_mod (node_mod d:C):real`;;
let y2_def = `!d. d IN dart (H:(A)hypermap) ==> y2_mod d = yn_mod (node_mod (face_map H d):C):real`;;
let y8_def = `!d. d IN dart (H:(A)hypermap) ==> y8_mod d = y5_mod (inverse (face_map H) d):real`;;
let rhazim_sum = `!n. n IN node_set (H:(A)hypermap) ==> sum n rhazim_mod = &2 * pi * rho_mod (node_mod (CHOICE n):C)`;;
let test_ineq6 = `!d. d IN darts_k 4 (H:(A)hypermap) ==>
(((tau_mod (face H d)) + ((#4.72 * (azim_mod d)) - #6.248)) - #0.0) >= #0.0`;;
let test_ineq7 = `!d. d IN dart (H:(A)hypermap) ==> CARD (face H d) = 3 ==> y4_mod d = y8_mod d:real`;;
let test_ineq8 = `!d. d IN dart (H:(A)hypermap) ==> &2 <= y4'_mod d`;;
let test_ineq9 = `!d. d IN darts_k 3 (H:(A)hypermap) ==> y4_mod d = ye_mod (face_map H d):real`;;
let test_ineq10 = `!d. d IN darts_k 3 (H:(A)hypermap) ==> ye_mod d = ye_mod (edge_map H d):real`;;
let test_ineq11 = `!d. d IN darts_k 5 (H:(A)hypermap) ==> tau_mod (face H d) >= #0.4819`;;
let test_ineq12 = `!d. d IN dart (H:(A)hypermap) ==> 3 < CARD (face H d) ==> #2.52 <= y4_mod d`;;
generate_ineq test_ineq1;;
generate_ineq test_ineq2;;
generate_ineq test_ineq3;;
generate_ineq test_ineq4;;
generate_ineq test_ineq5;;
generate_ineq test_ineq6;;
generate_ineq test_ineq7;;
generate_ineq test_ineq8;;
generate_ineq test_ineq9;;
generate_ineq test_ineq10;;
generate_ineq test_ineq11;;
generate_ineq test_ineq12;;
generate_ineq edge_sym;;
generate_ineq y1_def;;
generate_ineq y2_def;;
generate_ineq y8_def;;
generate_ineq rhazim_sum;;
*)