1 needs "../formal_lp/hypermap/ineqs/lp_ineqs.hl";;
4 module Lp_head_ineqs = struct
8 let add_head_ineqs () =
9 let _ = map add_lp_ineq_str
12 "!d. d IN dart H ==> &0 <= azim_mod d",
13 Some Lp_ineqs_proofs.azim_lo;
16 "!d. d IN dart H ==> azim_mod d <= pi",
17 Some Lp_ineqs_proofs.azim_hi;
20 "!d. d IN dart H ==> &0 <= azim2_mod d",
21 Some Lp_ineqs_proofs.azim2_lo;
24 "!d. d IN dart H ==> azim2_mod d <= pi",
25 Some Lp_ineqs_proofs.azim2_hi;
28 "!d. d IN dart H ==> &0 <= azim3_mod d",
29 Some Lp_ineqs_proofs.azim3_lo;
32 "!d. d IN dart H ==> azim3_mod d <= pi",
33 Some Lp_ineqs_proofs.azim3_hi;
36 "!d. d IN dart H ==> &0 <= rhazim_mod d",
37 Some Lp_ineqs_proofs.rhazim_lo;
40 "!d. d IN dart H ==> rhazim_mod d <= pi + sol0",
41 Some Lp_ineqs_proofs.rhazim_hi;
44 "!d. d IN dart H ==> &0 <= rhazim2_mod d",
45 Some Lp_ineqs_proofs.rhazim2_lo;
48 "!d. d IN dart H ==> rhazim2_mod d <= pi + sol0",
49 Some Lp_ineqs_proofs.rhazim2_hi;
52 "!d. d IN dart H ==> &0 <= rhazim3_mod d",
53 Some Lp_ineqs_proofs.rhazim3_lo;
56 "!d. d IN dart H ==> rhazim3_mod d <= pi + sol0",
57 Some Lp_ineqs_proofs.rhazim3_hi;
60 "!x. x IN V ==> &0 <= ln_mod x",
61 Some Lp_ineqs_proofs.ln_lo;
64 "!x. x IN V ==> ln_mod x <= &1",
65 Some Lp_ineqs_proofs.ln_hi;
68 "!x. x IN V ==> &1 <= rho_mod x",
69 Some Lp_ineqs_proofs.rho_lo;
72 "!x. x IN V ==> rho_mod x <= &1 + sol0 / pi",
73 Some Lp_ineqs_proofs.rho_hi;
76 "!x. x IN V ==> &2 <= yn_mod x",
77 Some Lp_ineqs_proofs.yn_lo;
80 "!x. x IN V ==> yn_mod x <= #2.52",
81 Some Lp_ineqs_proofs.yn_hi;
84 "!d. d IN dart H ==> &2 <= ye_mod d",
85 Some Lp_ineqs_proofs.ye_lo;
88 "!d. d IN dart H ==> ye_mod d <= &3 ==> ye_mod d <= &3",
92 "!d. d IN dart H ==> ye_mod d <= &3",
93 Some Lp_ineqs_proofs.ye_hi_std;
96 "!d. d IN dart H ==> &2 <= y1_mod d",
97 Some Lp_ineqs_proofs.y1_lo;
100 "!d. d IN dart H ==> y1_mod d <= #2.52",
101 Some Lp_ineqs_proofs.y1_hi;
104 "!d. d IN dart H ==> &2 <= y2_mod d",
105 Some Lp_ineqs_proofs.y2_lo;
108 "!d. d IN dart H ==> y2_mod d <= #2.52",
109 Some Lp_ineqs_proofs.y2_hi;
112 "!d. d IN dart H ==> &2 <= y3_mod d",
113 Some Lp_ineqs_proofs.y3_lo;
116 "!d. d IN dart H ==> y3_mod d <= #2.52",
117 Some Lp_ineqs_proofs.y3_hi;
120 "!d. d IN dart H ==> &2 <= y4_mod d",
121 Some Lp_ineqs_proofs.y4_lo;
124 "!d. d IN dart H ==> &2 <= y5_mod d",
125 Some Lp_ineqs_proofs.y5_lo;
128 "!d. d IN dart H ==> &2 <= y6_mod d",
129 Some Lp_ineqs_proofs.y6_lo;
132 "!d. d IN dart H ==> &2 <= y8_mod d",
133 Some Lp_ineqs_proofs.y8_lo;
136 "!d. d IN dart H ==> &2 <= y9_mod d",
137 Some Lp_ineqs_proofs.y9_lo;
140 "!d. d IN dart H ==> y4_mod d <= &3 ==> y4_mod d <= &3",
144 "!d. d IN dart H ==> y5_mod d <= &3==> y5_mod d <= &3",
148 "!d. d IN dart H ==> y6_mod d <= &3==> y6_mod d <= &3",
152 "!d. d IN dart H ==> y8_mod d <= #2.52==> y8_mod d <= #2.52",
156 "!d. d IN dart H ==> y9_mod d <= #2.52==> y9_mod d <= #2.52",
160 "!d. d IN dart H ==> y4_mod d <= &3",
161 Some Lp_ineqs_proofs.y4_hi_std;
164 "!d. d IN dart H ==> y5_mod d <= &3",
165 Some Lp_ineqs_proofs.y5_hi_std;
168 "!d. d IN dart H ==> y6_mod d <= &3",
169 Some Lp_ineqs_proofs.y6_hi_std;
172 "!d. d IN dart H ==> y8_mod d <= #2.52",
173 Some Lp_ineqs_proofs.y8_hi_std;
176 "!d. d IN dart H ==> y9_mod d <= #2.52",
177 Some Lp_ineqs_proofs.y9_hi_std;
180 "!f. f IN face_set H ==> &0 <= sol_mod f",
181 Some Lp_ineqs_proofs.sol_lo;
184 "!f. f IN face_set H ==> sol_mod f <= &4 * pi",
185 Some Lp_ineqs_proofs.sol_hi;
188 "!f. f IN face_set H ==> &0 <= tau_mod f",
189 Some Lp_ineqs_proofs.tau_lo;
192 "!f. f IN face_set H ==> tau_mod f <= tgt",
193 Some Lp_ineqs_proofs.tau_hi;
196 "!n. n IN node_set H ==> sum n azim_mod = &2 * pi",
197 Some Lp_ineqs_proofs.azim_sum;
200 "!n. n IN node_set H ==> sum n rhazim_mod = &2 * pi * rho_mod (node_mod (CHOICE n))",
201 Some Lp_ineqs_proofs.rhazim_sum;
204 "!f. f IN face_set H ==> (CARD f = 3 ==> sum f azim_mod = sol_mod f + pi)",
205 Some Lp_ineqs_proofs.sol_sum3;
208 "!f. f IN face_set H ==> (CARD f = 4 ==> sum f azim_mod = sol_mod f + &2 * pi)",
209 Some Lp_ineqs_proofs.sol_sum4;
212 "!f. f IN face_set H ==> (CARD f = 5 ==> sum f azim_mod = sol_mod f + &3 * pi)",
213 Some Lp_ineqs_proofs.sol_sum5;
216 "!f. f IN face_set H ==> (CARD f = 6 ==> sum f azim_mod = sol_mod f + &4 * pi)",
217 Some Lp_ineqs_proofs.sol_sum6;
220 "!f. f IN face_set H ==> (CARD f = 3 ==> sum f rhazim_mod = tau_mod f + (pi + sol0))",
221 Some Lp_ineqs_proofs.tau_sum3;
224 "!f. f IN face_set H ==> (CARD f = 4 ==> sum f rhazim_mod = tau_mod f + &2 * (pi + sol0))",
225 Some Lp_ineqs_proofs.tau_sum4;
228 "!f. f IN face_set H ==> (CARD f = 5 ==> sum f rhazim_mod = tau_mod f + &3 * (pi + sol0))",
229 Some Lp_ineqs_proofs.tau_sum5;
232 "!f. f IN face_set H ==> (CARD f = 6 ==> sum f rhazim_mod = tau_mod f + &4 * (pi + sol0))",
233 Some Lp_ineqs_proofs.tau_sum6;
236 "!x. x IN V ==> ln_mod x = (#2.52 - yn_mod x) / #0.52",
237 Some Lp_ineqs_proofs.ln_def;
239 "!x. x IN V ==> rho_mod x = (&1 + sol0 / pi) - ln_mod x * sol0 / pi",
240 Some Lp_ineqs_proofs.rho_def;
242 "!d. d IN dart H ==> ye_mod d = ye_mod (edge_map H d):real",
243 Some Lp_ineqs_proofs.edge_sym;
246 "!d. d IN dart H ==> y1_mod d = yn_mod (node_mod d):real",
247 Some Lp_ineqs_proofs.y1_def;
250 "!d. d IN dart H ==> y2_mod d = yn_mod (node_mod (face_map H d)):real",
251 Some Lp_ineqs_proofs.y2_def;
254 "!d. d IN dart H ==> y3_mod d = yn_mod (node_mod (inverse (face_map H) d)):real",
255 Some Lp_ineqs_proofs.y3_def;
258 "!d. d IN dart H ==> y4_mod d = ye_mod (face_map H d):real",
259 Some Lp_ineqs_proofs.y4_def;
262 "!d. d IN dart H ==> y5_mod d = ye_mod (inverse (face_map H) d):real",
263 Some Lp_ineqs_proofs.y5_def;
266 "!d. d IN dart H ==> y6_mod d = ye_mod d:real",
267 Some Lp_ineqs_proofs.y6_def;
270 "!d. d IN dart H ==> y8_mod d = y5_mod (inverse (face_map H) d):real",
271 Some Lp_ineqs_proofs.y8_def;
274 "!d. d IN dart H ==> y9_mod d = ye_mod (face_map H d):real",
275 Some Lp_ineqs_proofs.y9_def;
278 "!d. d IN dart H ==> azim2_mod d = azim_mod (face_map H d):real",
279 Some Lp_ineqs_proofs.azim2c;
282 "!d. d IN dart H ==> azim3_mod d = azim_mod (inverse (face_map H) d):real",
283 Some Lp_ineqs_proofs.azim3c;
286 "!d. d IN dart H ==> rhazim2_mod d = rhazim_mod (face_map H d):real",
287 Some Lp_ineqs_proofs.rhazim2c;
290 "!d. d IN dart H ==> rhazim3_mod d = rhazim_mod (inverse (face_map H) d):real",
291 Some Lp_ineqs_proofs.rhazim3c;
294 "!d. d IN dart H ==> rhazim_mod d >= azim_mod d:real",
295 Some Lp_ineqs_proofs.RHA;
298 "!d. d IN dart H ==> rhazim_mod d <= azim_mod d * (&1 + sol0 / pi)",
299 Some Lp_ineqs_proofs.RHB;
302 "!d. d IN dart H ==> yn_mod (node_mod d) <= #2.18 ==> rhazim_mod d <= azim_mod d * rho218",
303 Some Lp_ineqs_proofs.RHBLO;
306 "!d. d IN dart H ==> #2.18 <= yn_mod (node_mod d) ==> rhazim_mod d >= azim_mod d * rho218",
307 Some Lp_ineqs_proofs.RHBHI;
310 "!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",
314 "!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",
318 "!x. x IN V ==> #2.18 <= yn_mod x ==> #2.18 <= yn_mod x",
322 "!x. x IN V ==> yn_mod x <= #2.18 ==> yn_mod x <= #2.18",
326 "!x. x IN V ==> #2.36 <= yn_mod x ==> #2.36 <= yn_mod x",
330 "!x. x IN V ==> yn_mod x <= #2.36 ==> yn_mod x <= #2.36",
334 "!x. x IN V ==> #2.18 <= yn_mod x ==> #2.18 <= yn_mod x",
338 "!d. d IN dart H ==> #2.25 <= ye_mod d ==> #2.25 <= ye_mod d",
342 "!d. d IN dart H ==> ye_mod d <= #2.25 ==> ye_mod d <= #2.25",
346 "!d. d IN dart H ==> ye_mod d <= #2.52 ==> ye_mod d <= #2.52",
350 "!d. d IN dart H ==> ye_mod d <= #2.52",
351 Some Lp_ineqs_proofs.yy10_std;
354 "!d. d IN darts_k 3 H ==> #2.52 <= y4_mod d ==> #2.52 <= y4_mod d",
358 "!d. d IN darts_k 3 H ==> sqrt8 <= y4_mod d ==> sqrt8 <= y4_mod d",
362 "!d. d IN darts_k 3 H ==> y5_mod d <= #2.52 ==> y5_mod d <= #2.52",
366 "!d. d IN darts_k 3 H ==> y6_mod d <= #2.52 ==> y6_mod d <= #2.52",
370 "!d. d IN darts_k 3 H ==> y4_mod d <= sqrt8 ==> y4_mod d <= sqrt8",
373 (* The main inequality *)
375 let th1 = (add_lp_hyp false o UNDISCH_ALL o SPEC_ALL) Lp_ineqs_proofs.lnsum_ineq in
376 (* Add an artificial ALL statement *)
377 (REWRITE_RULE[ALL_MEM] o GEN `v:num` o DISCH `MEM (v:num) (list_of_elements L)`) th1 in
378 let _ = add_lp_list_ineq ("main", false, main_ineq) in
380 (* Main estimate inequalities *)
381 let _ = map add_lp_ineq_th
383 "tau3", false, Lp_main_estimate.ineq_tau3;
384 "tau4", false, Lp_main_estimate.ineq_tau4;
385 "tau5", false, Lp_main_estimate.ineq_tau5;
386 "tau6", false, Lp_main_estimate.ineq_tau6;
387 "tau4", true, Lp_main_estimate.ineq_tau4_std;
388 "tau5", true, Lp_main_estimate.ineq_tau5_std;
389 "tau6", true, Lp_main_estimate.ineq_tau6_std;
390 "tauB5h", false, Lp_main_estimate.ineq_tau5_pro;
391 "tauB4h", false, Lp_main_estimate.ineq_tau4_pro;
392 "tau5h", false, Lp_main_estimate.ineq_tau5_diags;
393 "tau5h", true, Lp_main_estimate.ineq_tau5_diags_std;
395 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
396 let _ = add_lp_list_ineq ("crossdiag", false, crossdiag_ineq) in
398 let _ = add_lp_ineq_th ("perimZ", false, Lp_ineqs_proofs2.perimZ) in
399 let _ = add_lp_ineq_th ("perimZ", true, Lp_ineqs_proofs2.perimZ_std) in
401 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)
402 Lp_ineqs_proofs2.yapex_sup_flat_list in
403 let _ = add_lp_list_ineq ("yapex_sup_flat", false, yapex_sup_flat) in