formal_lp/hypermap/ineqs/lp_head_ineqs.hl

   1 needs "../formal_lp/hypermap/ineqs/lp_ineqs.hl";;
   2
   3
   4 module Lp_head_ineqs = struct
   5
   6 open Lp_ineqs;;
   7
   8 let add_head_ineqs () =
   9   let _ = map add_lp_ineq_str
  10   [
  11     "azim_lo", false,
  12                 "!d. d IN dart H ==> &0 <= azim_mod d",
  13                 Some Lp_ineqs_proofs.azim_lo;
  14
  15     "azim_hi", false,
  16                 "!d. d IN dart H ==> azim_mod d <= pi",
  17                 Some Lp_ineqs_proofs.azim_hi;
  18
  19     "azim2_lo", false,
  20                 "!d. d IN dart H ==> &0 <= azim2_mod d",
  21                 Some Lp_ineqs_proofs.azim2_lo;
  22
  23     "azim2_hi", false,
  24                 "!d. d IN dart H ==> azim2_mod d <= pi",
  25                 Some Lp_ineqs_proofs.azim2_hi;
  26
  27     "azim3_lo", false,
  28                 "!d. d IN dart H ==> &0 <= azim3_mod d",
  29                 Some Lp_ineqs_proofs.azim3_lo;
  30
  31     "azim3_hi", false,
  32                 "!d. d IN dart H ==> azim3_mod d <= pi",
  33                 Some Lp_ineqs_proofs.azim3_hi;
  34
  35     "rhazim_lo", false,
  36                 "!d. d IN dart H ==> &0 <= rhazim_mod d",
  37                 Some Lp_ineqs_proofs.rhazim_lo;
  38
  39     "rhazim_hi", false,
  40                 "!d. d IN dart H ==> rhazim_mod d <= pi + sol0",
  41                 Some Lp_ineqs_proofs.rhazim_hi;
  42
  43     "rhazim2_lo", false,
  44                 "!d. d IN dart H ==> &0 <= rhazim2_mod d",
  45                 Some Lp_ineqs_proofs.rhazim2_lo;
  46
  47     "rhazim2_hi", false,
  48                 "!d. d IN dart H ==> rhazim2_mod d <= pi + sol0",
  49                 Some Lp_ineqs_proofs.rhazim2_hi;
  50
  51     "rhazim3_lo", false,
  52                 "!d. d IN dart H ==> &0 <= rhazim3_mod d",
  53                 Some Lp_ineqs_proofs.rhazim3_lo;
  54
  55     "rhazim3_hi", false,
  56                 "!d. d IN dart H ==> rhazim3_mod d <= pi + sol0",
  57                 Some Lp_ineqs_proofs.rhazim3_hi;
  58
  59     "ln_lo", false,
  60                 "!x. x IN V ==> &0 <= ln_mod x",
  61                 Some Lp_ineqs_proofs.ln_lo;
  62
  63     "ln_hi", false,
  64                 "!x. x IN V ==> ln_mod x <= &1",
  65                 Some Lp_ineqs_proofs.ln_hi;
  66
  67     "rho_lo", false,
  68                 "!x. x IN V ==> &1 <= rho_mod x",
  69                 Some Lp_ineqs_proofs.rho_lo;
  70
  71     "rho_hi", false,
  72                 "!x. x IN V ==> rho_mod x <= &1 + sol0 / pi",
  73                 Some Lp_ineqs_proofs.rho_hi;
  74
  75     "yn_lo", false,
  76                 "!x. x IN V ==> &2 <= yn_mod x",
  77                 Some Lp_ineqs_proofs.yn_lo;
  78
  79     "yn_hi", false,
  80                 "!x. x IN V ==> yn_mod x <= #2.52",
  81                 Some Lp_ineqs_proofs.yn_hi;
  82
  83     "ye_lo", false,
  84                 "!d. d IN dart H ==> &2 <= ye_mod d",
  85                 Some Lp_ineqs_proofs.ye_lo;
  86
  87     "ye_hi", false,
  88                 "!d. d IN dart H ==> ye_mod d <= &3 ==> ye_mod d <= &3",
  89                 None;
  90
  91     "ye_hi", true,
  92                 "!d. d IN dart H ==> ye_mod d <= &3",
  93                 Some Lp_ineqs_proofs.ye_hi_std;
  94
  95     "y1_lo", false,
  96                 "!d. d IN dart H ==> &2 <= y1_mod d",
  97                 Some Lp_ineqs_proofs.y1_lo;
  98
  99     "y1_hi", false,
 100                 "!d. d IN dart H ==> y1_mod d <= #2.52",
 101                 Some Lp_ineqs_proofs.y1_hi;
 102
 103     "y2_lo", false,
 104                 "!d. d IN dart H ==> &2 <= y2_mod d",
 105                 Some Lp_ineqs_proofs.y2_lo;
 106
 107     "y2_hi", false,
 108                 "!d. d IN dart H ==> y2_mod d <= #2.52",
 109                 Some Lp_ineqs_proofs.y2_hi;
 110
 111     "y3_lo", false,
 112                 "!d. d IN dart H ==> &2 <= y3_mod d",
 113                 Some Lp_ineqs_proofs.y3_lo;
 114
 115     "y3_hi", false,
 116                 "!d. d IN dart H ==> y3_mod d <= #2.52",
 117                 Some Lp_ineqs_proofs.y3_hi;
 118
 119     "y4_lo", false,
 120                 "!d. d IN dart H ==> &2 <= y4_mod d",
 121                 Some Lp_ineqs_proofs.y4_lo;
 122
 123     "y5_lo", false,
 124                 "!d. d IN dart H ==> &2 <= y5_mod d",
 125                 Some Lp_ineqs_proofs.y5_lo;
 126
 127     "y6_lo", false,
 128                 "!d. d IN dart H ==> &2 <= y6_mod d",
 129                 Some Lp_ineqs_proofs.y6_lo;
 130
 131     "y8_lo", false,
 132                 "!d. d IN dart H ==> &2 <= y8_mod d",
 133                 Some Lp_ineqs_proofs.y8_lo;
 134
 135     "y9_lo", false,
 136                 "!d. d IN dart H ==> &2 <= y9_mod d",
 137                 Some Lp_ineqs_proofs.y9_lo;
 138
 139     "y4_hi", false,
 140                 "!d. d IN dart H ==> y4_mod d <= &3 ==> y4_mod d <= &3",
 141                 None;
 142
 143     "y5_hi", false,
 144                 "!d. d IN dart H ==> y5_mod d <= &3==> y5_mod d <= &3",
 145                 None;
 146
 147     "y6_hi", false,
 148                 "!d. d IN dart H ==> y6_mod d <= &3==> y6_mod d <= &3",
 149                 None;
 150
 151     "y8_hi", false,
 152                 "!d. d IN dart H ==> y8_mod d <= #2.52==> y8_mod d <= #2.52",
 153                 None;
 154
 155     "y9_hi", false,
 156                 "!d. d IN dart H ==> y9_mod d <= #2.52==> y9_mod d <= #2.52",
 157                 None;
 158
 159     "y4_hi", true,
 160                 "!d. d IN dart H ==> y4_mod d <= &3",
 161                 Some Lp_ineqs_proofs.y4_hi_std;
 162
 163     "y5_hi", true,
 164                 "!d. d IN dart H ==> y5_mod d <= &3",
 165                 Some Lp_ineqs_proofs.y5_hi_std;
 166
 167     "y6_hi", true,
 168                 "!d. d IN dart H ==> y6_mod d <= &3",
 169                 Some Lp_ineqs_proofs.y6_hi_std;
 170
 171     "y8_hi", true,
 172                 "!d. d IN dart H ==> y8_mod d <= #2.52",
 173                 Some Lp_ineqs_proofs.y8_hi_std;
 174
 175     "y9_hi", true,
 176                 "!d. d IN dart H ==> y9_mod d <= #2.52",
 177                 Some Lp_ineqs_proofs.y9_hi_std;
 178
 179     "sol_lo", false,
 180                 "!f. f IN face_set H ==> &0 <= sol_mod f",
 181                 Some Lp_ineqs_proofs.sol_lo;
 182
 183     "sol_hi", false,
 184                 "!f. f IN face_set H ==> sol_mod f <= &4 * pi",
 185                 Some Lp_ineqs_proofs.sol_hi;
 186
 187     "tau_lo", false,
 188                 "!f. f IN face_set H ==> &0 <= tau_mod f",
 189                 Some Lp_ineqs_proofs.tau_lo;
 190
 191     "tau_hi", false,
 192                 "!f. f IN face_set H ==> tau_mod f <= tgt",
 193                 Some Lp_ineqs_proofs.tau_hi;
 194
 195     "azim_sum", false,
 196                 "!n. n IN node_set H ==> sum n azim_mod = &2 * pi",
 197                 Some Lp_ineqs_proofs.azim_sum;
 198
 199     "rhazim_sum", false,
 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;
 202
 203     "sol_sum3", false,
 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;
 206
 207     "sol_sum4", false,
 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;
 210
 211     "sol_sum5", false,
 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;
 214
 215     "sol_sum6", false,
 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;
 218
 219     "tau_sum3", false,
 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;
 222
 223     "tau_sum4", false,
 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;
 226
 227     "tau_sum5", false,
 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;
 230
 231     "tau_sum6", false,
 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;
 234
 235     "ln_def", false,
 236                 "!x. x IN V ==> ln_mod x = (#2.52 - yn_mod x) / #0.52",
 237                 Some Lp_ineqs_proofs.ln_def;
 238     "rho_def", false,
 239                 "!x. x IN V ==> rho_mod x = (&1 + sol0 / pi) - ln_mod x * sol0 / pi",
 240                 Some Lp_ineqs_proofs.rho_def;
 241     "edge_sym", false,
 242                 "!d. d IN dart H ==> ye_mod d = ye_mod (edge_map H d):real",
 243                 Some Lp_ineqs_proofs.edge_sym;
 244
 245     "y1_def", false,
 246                 "!d. d IN dart H ==> y1_mod d = yn_mod (node_mod d):real",
 247                 Some Lp_ineqs_proofs.y1_def;
 248
 249     "y2_def", false,
 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;
 252
 253     "y3_def", false,
 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;
 256
 257     "y4_def", false,
 258                 "!d. d IN dart H ==> y4_mod d = ye_mod (face_map H d):real",
 259                 Some Lp_ineqs_proofs.y4_def;
 260
 261     "y5_def", false,
 262                 "!d. d IN dart H ==> y5_mod d = ye_mod (inverse (face_map H) d):real",
 263                 Some Lp_ineqs_proofs.y5_def;
 264
 265     "y6_def", false,
 266                 "!d. d IN dart H ==> y6_mod d = ye_mod d:real",
 267                 Some Lp_ineqs_proofs.y6_def;
 268
 269     "y8_def", false,
 270                 "!d. d IN dart H ==> y8_mod d = y5_mod (inverse (face_map H) d):real",
 271                 Some Lp_ineqs_proofs.y8_def;
 272
 273     "y9_def", false,
 274                 "!d. d IN dart H ==> y9_mod d = ye_mod (face_map H d):real",
 275                 Some Lp_ineqs_proofs.y9_def;
 276
 277     "azim2c", false,
 278                 "!d. d IN dart H ==> azim2_mod d = azim_mod (face_map H d):real",
 279                 Some Lp_ineqs_proofs.azim2c;
 280
 281     "azim3c", false,
 282                 "!d. d IN dart H ==> azim3_mod d = azim_mod (inverse (face_map H) d):real",
 283                 Some Lp_ineqs_proofs.azim3c;
 284
 285     "rhazim2c", false,
 286                 "!d. d IN dart H ==> rhazim2_mod d = rhazim_mod (face_map H d):real",
 287                 Some Lp_ineqs_proofs.rhazim2c;
 288
 289     "rhazim3c", false,
 290                 "!d. d IN dart H ==> rhazim3_mod d = rhazim_mod (inverse (face_map H) d):real",
 291                 Some Lp_ineqs_proofs.rhazim3c;
 292
 293     "RHA", false,
 294                 "!d. d IN dart H ==> rhazim_mod d >= azim_mod d:real",
 295                 Some Lp_ineqs_proofs.RHA;
 296
 297     "RHB", false,
 298                 "!d. d IN dart H ==> rhazim_mod d <= azim_mod d * (&1 + sol0 / pi)",
 299                 Some Lp_ineqs_proofs.RHB;
 300
 301     "RHBLO", false,
 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;
 304
 305     "RHBHI", false,
 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;
 308
 309     "yy1", false,
 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",
 311                 None;
 312
 313     "yy2", false,
 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",
 315                 None;
 316
 317     "yy3", false,
 318                 "!x. x IN V ==> #2.18 <= yn_mod x ==> #2.18 <= yn_mod x",
 319                 None;
 320
 321     "yy4", false,
 322                 "!x. x IN V ==> yn_mod x <= #2.18 ==> yn_mod x <= #2.18",
 323                 None;
 324
 325     "yy5", false,
 326                 "!x. x IN V ==> #2.36 <= yn_mod x ==> #2.36 <= yn_mod x",
 327                 None;
 328
 329     "yy6", false,
 330                 "!x. x IN V ==> yn_mod x <= #2.36 ==> yn_mod x <= #2.36",
 331                 None;
 332
 333     "yy7", false,
 334                 "!x. x IN V ==> #2.18 <= yn_mod x ==> #2.18 <= yn_mod x",
 335                 None;
 336
 337     "yy8", false,
 338                 "!d. d IN dart H ==> #2.25 <= ye_mod d ==> #2.25 <= ye_mod d",
 339                 None;
 340
 341     "yy9", false,
 342                 "!d. d IN dart H ==> ye_mod d <= #2.25 ==> ye_mod d <= #2.25",
 343                 None;
 344
 345     "yy10", false,
 346                 "!d. d IN dart H ==> ye_mod d <= #2.52 ==> ye_mod d <= #2.52",
 347                 None;
 348
 349     "yy10", true,
 350                 "!d. d IN dart H ==> ye_mod d <= #2.52",
 351                 Some Lp_ineqs_proofs.yy10_std;
 352
 353     "yy11", false,
 354                 "!d. d IN darts_k 3 H ==> #2.52 <= y4_mod d ==> #2.52 <= y4_mod d",
 355                 None;
 356
 357     "yy12", false,
 358                 "!d. d IN darts_k 3 H ==> sqrt8 <= y4_mod d ==> sqrt8 <= y4_mod d",
 359                 None;
 360
 361     "yy13", false,
 362                 "!d. d IN darts_k 3 H ==> y5_mod d <= #2.52 ==> y5_mod d <= #2.52",
 363                 None;
 364
 365     "yy14", false,
 366                 "!d. d IN darts_k 3 H ==> y6_mod d <= #2.52 ==> y6_mod d <= #2.52",
 367                 None;
 368
 369     "yy15", false,
 370                 "!d. d IN darts_k 3 H ==> y4_mod d <= sqrt8 ==> y4_mod d <= sqrt8",
 371                 None;
 372   ] in
 373     (* The main inequality *)
 374   let main_ineq =
 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
 379
 380   (* Main estimate inequalities *)
 381   let _ = map add_lp_ineq_th
 382   [
 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;
 394   ] in
 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
 397
 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
 400
 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
 404     ();;
 405
 406 end;;