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