1 needs "../formal_lp/hypermap/ineqs/lp_ineqs_defs.hl";;
2 needs "../formal_lp/hypermap/ineqs/lp_gen_theory-compiled.hl";;
4 module Lp_gen_ineqs = struct
8 open Hypermap_and_fan;;
14 (* mod-file variables and definitions *)
19 "dart", `:real^3#real^3`;
20 "face", `:real^3#real^3->bool`;
23 let mk_mod name set = mk_var (name, mk_fun_ty (assoc set sets) `:real`) in
25 `hypermap_of_fan (V,E)`, `H:(real^3#real^3)hypermap`;
26 `FST:real^3#real^3->real^3`, `node_mod:real^3#real^3->real^3`;
27 `azim_dart (V,E)`, mk_mod "azim_mod" "dart";
28 `azim2_fan (V,E)`, mk_mod "azim2_mod" "dart";
29 `azim3_fan (V,E)`, mk_mod "azim3_mod" "dart";
30 `rhazim_fan (V,E)`, mk_mod "rhazim_mod" "dart";
31 `rhazim2_fan (V,E)`, mk_mod "rhazim2_mod" "dart";
32 `rhazim3_fan (V,E)`, mk_mod "rhazim3_mod" "dart";
33 `ln_fan`, mk_mod "ln_mod" "node";
34 `yn_fan`, mk_mod "yn_mod" "node";
35 `rho_fan`, mk_mod "rho_mod" "node";
36 `ye_fan`, mk_mod "ye_mod" "dart";
37 `y1_fan`, mk_mod "y1_mod" "dart";
38 `y2_fan`, mk_mod "y2_mod" "dart";
39 `y3_fan (V,E)`, mk_mod "y3_mod" "dart";
40 `y4_fan (V,E)`, mk_mod "y4_mod" "dart";
41 `y5_fan (V,E)`, mk_mod "y5_mod" "dart";
42 `y6_fan`, mk_mod "y6_mod" "dart";
43 `y8_fan (V,E)`, mk_mod "y8_mod" "dart";
44 `y9_fan (V,E)`, mk_mod "y9_mod" "dart";
45 `y4'_fan (V,E)`, mk_mod "y4'_mod" "dart";
46 `sol_fan (V,E)`, mk_mod "sol_mod" "face";
47 `tau_fan (V,E)`, mk_mod "tau_mod" "face";
55 (* For a term in the form `!x. x IN set H ==> P x` returns a theorem
56 hyp_iso g (G,H), !x. x IN set H ==> P x |- !y. y IN set G ==> P (g y) *)
60 `darts_k 6 (H:(A)hypermap)`, spec_var_th iso_darts_k_trans 0 `6`;
61 `darts_k 5 (H:(A)hypermap)`, spec_var_th iso_darts_k_trans 0 `5`;
62 `darts_k 4 (H:(A)hypermap)`, spec_var_th iso_darts_k_trans 0 `4`;
63 `darts_k 3 (H:(A)hypermap)`, spec_var_th iso_darts_k_trans 0 `3`;
64 `dart (H:(A)hypermap)`, iso_dart_trans;
65 `face_set (H:(A)hypermap)`, iso_face_trans;
66 `node_set (H:(A)hypermap)`, iso_node_trans;
67 `V:C->bool`, bij_trans;
71 let x_tm, tm = dest_forall ineq in
73 try (fst o dest_fun_ty o type_of) x_tm with Failure _ -> type_of x_tm in
74 let ty_list = [x_ty, aty; x_ty, cty] in
75 let iso_list = map (fun tm, th -> inst ty_list tm, INST_TYPE ty_list th) iso_list0 in
76 let set, p_tm' = dest_binary "==>" tm in
77 let set_th = assoc (rand set) iso_list in
78 let p_tm = mk_abs (x_tm, p_tm') in
79 let p_var = mk_var ("P", type_of (rand set)) in
80 let th1 = (SPEC_ALL o ONCE_REWRITE_RULE[RIGHT_IMP_FORALL_THM] o REWRITE_RULE[IMP_IMP]) set_th in
81 BETA_RULE (INST[p_tm, p_var] th1), ty_list;;
84 (* For an inequality term returns an isomorphism theorem *)
86 let th_rule th = (UNDISCH_ALL o SPEC_ALL o REWRITE_RULE[RIGHT_IMP_FORALL_THM]) th in
88 th_rule components_iso_image;
89 th_rule hyp_iso_comm_special;
90 th_rule hyp_iso_inv_comm;
91 th_rule card_face_iso;
92 th_rule card_face_dart_iso;
97 `d IN darts_k 3 (G:(B)hypermap)`, (INST[`3`, `k:num`] o th_rule) darts_k_subset;
98 `d IN darts_k 4 (G:(B)hypermap)`, (INST[`4`, `k:num`] o th_rule) darts_k_subset;
99 `d IN darts_k 5 (G:(B)hypermap)`, (INST[`5`, `k:num`] o th_rule) darts_k_subset;
100 `d IN darts_k 6 (G:(B)hypermap)`, (INST[`6`, `k:num`] o th_rule) darts_k_subset;
104 let iso_trans_th, ty_list = get_iso_thm ineq in
105 let th0 = UNDISCH_ALL (PURE_REWRITE_RULE[GSYM IMP_IMP] iso_trans_th) in
106 let gen_var, rtm = dest_forall(concl th0) in
107 let ths = map (INST_TYPE ty_list) ths0 and
108 sub_ths = map (fun tm, th -> inst ty_list tm, INST_TYPE ty_list th) sub_ths0 in
109 let ants = lhand rtm in
110 let th1 = UNDISCH (SPEC_ALL th0) in
111 (* General isomorphism rewrites *)
112 let th2 = PURE_REWRITE_RULE ths th1 in
115 let sub_th = assoc ants sub_ths in
117 with Failure _ -> th2 in
118 GEN gen_var (DISCH ants th3);;
122 let th_rule = (UNDISCH_ALL o INST_TYPE [`:num`, aty; `:num`, `:D`; `:real^3`, `:C`] o
123 SPEC_ALL o REWRITE_RULE[GSYM IMP_IMP; RIGHT_IMP_FORALL_THM]) in
124 (* |- !d. d IN set_of_list s ==> P d <=> !d. MEM d s ==> P d *)
125 let ths_all = map th_rule
139 th_rule card_face_eq_length_find_face;
140 th_rule card_set_of_list_face;
141 th_rule card_set_of_list_node;
142 th_rule fst_choice_of_list_node;
143 UNDISCH_ALL (ISPEC `L:((num)list)list` components_hypermap_of_list);
144 th_rule e_list_ext_eq_e_list;
145 th_rule fst_iso_trans;
150 `MEM (d:num#num) (list_of_darts3 L)`, th_rule list_of_darts3_subset;
151 `MEM (d:num#num) (list_of_darts4 L)`, th_rule list_of_darts4_subset;
152 `MEM (d:num#num) (list_of_darts5 L)`, th_rule list_of_darts5_subset;
153 `MEM (d:num#num) (list_of_darts6 L)`, th_rule list_of_darts6_subset;
157 (* G -> hypermap_of_list (L:((num)list)list) *)
158 let s1 = INST_TYPE [`:real^3#real^3`, aty; `:num#num`, bty; `:real^3`, `:C`; `:num`, `:D`] iso_th in
159 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
160 (* Convert conditions in the form !d. d IN set_of_list s to !d. MEM d s *)
161 let s3 = PURE_REWRITE_RULE ths_all s2 in
162 let gen_var2, rtm = dest_forall (concl s3) in
163 let ants2 = lhand rtm in
164 let s4 = UNDISCH (SPEC_ALL s3) in
165 (* Instantiate all variables *)
166 let s5 = INST var_inst_list s4 in
167 (* Additional rewrites *)
168 let s6 = PURE_REWRITE_RULE ths_more s5 in
171 let mem_th = assoc ants2 ths_mem in
173 with Failure _ -> s6 in
174 let s8 = GEN gen_var2 (DISCH ants2 s7) in
175 let s9 = PURE_REWRITE_RULE list_var_rewrites s8 in
176 let s10 = PURE_REWRITE_RULE[ALL_MEM] s9 in
177 (* Rewrite the main inequality hypothesis with the COMPONENTS_HYPERMAP_OF_FAN theorem *)
178 let gen_hyp = find is_forall (hyp s10) in
179 let eq_th = REWRITE_CONV[UNDISCH_ALL (ISPECL [`V:real^3->bool`; `E:(real^3->bool)->bool`] COMPONENTS_HYPERMAP_OF_FAN)] gen_hyp in
180 let imp_th = if (rand (concl eq_th) = `T`) then EQT_ELIM eq_th else UNDISCH (MATCH_MP EQ_IMP (SYM eq_th)) in
181 PROVE_HYP imp_th s10;;
184 let generate_ineq ineq_tm =
185 let th1 = build_iso_th ineq_tm in
196 let test_ineq1 = `!d. d IN dart (H:(A)hypermap) ==> rhazim3_mod d <= pi + sol0`;;
197 let test_ineq2 = `!f. f IN face_set (H:(A)hypermap) ==> sol_mod f <= &4 * pi`;;
198 let test_ineq3 = `!f. f IN face_set (H:(A)hypermap) ==> (CARD f = 5 ==>
199 sum f azim_mod = sol_mod f + &3 * pi)`;;
200 let test_ineq4 = `!n. n IN node_set (H:(A)hypermap) ==> sum n azim_mod = &2 * pi`;;
201 let test_ineq5 = `!x. x IN (V:C->bool) ==> ln_mod x = (#2.52 - yn_mod x) / #0.52`;;
202 let edge_sym = `!d. d IN dart (H:(A)hypermap) ==> ye_mod d = ye_mod (edge_map H d):real`;;
203 let y1_def = `!d. d IN dart (H:(A)hypermap) ==> y1_mod d = yn_mod (node_mod d:C):real`;;
204 let y2_def = `!d. d IN dart (H:(A)hypermap) ==> y2_mod d = yn_mod (node_mod (face_map H d):C):real`;;
205 let y8_def = `!d. d IN dart (H:(A)hypermap) ==> y8_mod d = y5_mod (inverse (face_map H) d):real`;;
206 let rhazim_sum = `!n. n IN node_set (H:(A)hypermap) ==> sum n rhazim_mod = &2 * pi * rho_mod (node_mod (CHOICE n):C)`;;
207 let test_ineq6 = `!d. d IN darts_k 4 (H:(A)hypermap) ==>
208 (((tau_mod (face H d)) + ((#4.72 * (azim_mod d)) - #6.248)) - #0.0) >= #0.0`;;
209 let test_ineq7 = `!d. d IN dart (H:(A)hypermap) ==> CARD (face H d) = 3 ==> y4_mod d = y8_mod d:real`;;
210 let test_ineq8 = `!d. d IN dart (H:(A)hypermap) ==> &2 <= y4'_mod d`;;
211 let test_ineq9 = `!d. d IN darts_k 3 (H:(A)hypermap) ==> y4_mod d = ye_mod (face_map H d):real`;;
212 let test_ineq10 = `!d. d IN darts_k 3 (H:(A)hypermap) ==> ye_mod d = ye_mod (edge_map H d):real`;;
213 let test_ineq11 = `!d. d IN darts_k 5 (H:(A)hypermap) ==> tau_mod (face H d) >= #0.4819`;;
214 let test_ineq12 = `!d. d IN dart (H:(A)hypermap) ==> 3 < CARD (face H d) ==> #2.52 <= y4_mod d`;;
216 generate_ineq test_ineq1;;
217 generate_ineq test_ineq2;;
218 generate_ineq test_ineq3;;
219 generate_ineq test_ineq4;;
220 generate_ineq test_ineq5;;
221 generate_ineq test_ineq6;;
222 generate_ineq test_ineq7;;
223 generate_ineq test_ineq8;;
224 generate_ineq test_ineq9;;
225 generate_ineq test_ineq10;;
226 generate_ineq test_ineq11;;
227 generate_ineq test_ineq12;;
229 generate_ineq edge_sym;;
230 generate_ineq y1_def;;
231 generate_ineq y2_def;;
232 generate_ineq y8_def;;
233 generate_ineq rhazim_sum;;