formal_lp/old/arith/prove_lp.hl

   1 needs "arith/arith_int.hl";;
   2
   3 open Arith_hash;;
   4
   5 (********************)
   6 (* Main definitions *)
   7 (********************)
   8
   9 (* A linear function *)
  10 let lin_f = new_definition `lin_f terms =
  11   ITLIST (\tm x. (FST tm) * (SND tm) + x) terms (&0)`;;
  12
  13 (* Example:  let x = `lin_f [&1, x:real; &2, y:real]`;; *)
  14
  15
  16 (**********************)
  17 (* Theorems for lin_f *)
  18 (**********************)
  19
  20 (* Basic properties of lin_f *)
  21 let LIN_F_CONS = prove(`!h t. lin_f (CONS h t) = (FST h * SND h) + lin_f t`,
  22    REWRITE_TAC[lin_f; ITLIST]);;
  23
  24
  25 let LIN_F_EMPTY = prove(`lin_f [] = &0`,
  26                         REWRITE_TAC[lin_f; ITLIST]);;
  27
  28
  29 let LIN_F_APPEND = prove(`!t1 t2. lin_f (APPEND t1 t2) = lin_f t1 + lin_f t2`,
  30    LIST_INDUCT_TAC THEN REWRITE_TAC[APPEND] THENL
  31      [
  32        REWRITE_TAC[LIN_F_EMPTY; REAL_ADD_LID];
  33        ALL_TAC
  34      ] THEN
  35
  36      GEN_TAC THEN
  37      ASM_REWRITE_TAC[LIN_F_CONS; REAL_ADD_ASSOC]);;
  38
  39
  40 (* Sum of two lin_f *)
  41
  42 let LIN_F_SUM_HD = prove(`!v c1 t1 c2 t2 c. c1 + c2 = c ==>
  43     lin_f (CONS (c1,v) t1) + lin_f (CONS (c2,v) t2) = lin_f [c,v] + (lin_f t1 + lin_f t2)`,
  44    REPEAT GEN_TAC THEN REWRITE_TAC[LIN_F_CONS; LIN_F_EMPTY] THEN
  45      DISCH_THEN (fun th -> REWRITE_TAC[SYM th]) THEN REAL_ARITH_TAC);;
  46
  47 let LIN_F_SUM_HD_ZERO = prove(`!v c1 t1 c2 t2. c1 + c2 = &0 ==>
  48     lin_f (CONS (c1,v) t1) + lin_f (CONS (c2,v) t2) = lin_f t1 + lin_f t2`,
  49    REPEAT GEN_TAC THEN DISCH_THEN (MP_TAC o MATCH_MP LIN_F_SUM_HD) THEN
  50      DISCH_THEN (fun th -> REWRITE_TAC[th; LIN_F_CONS; LIN_F_EMPTY]) THEN
  51      REAL_ARITH_TAC);;
  52
  53 let LIN_F_SUM_EMPTY1 = prove(`!x. lin_f [] + lin_f x = lin_f x`,
  54                              REWRITE_TAC[LIN_F_EMPTY; REAL_ADD_LID]);;
  55
  56 let LIN_F_SUM_EMPTY2 = prove(`!x. lin_f x + lin_f [] = lin_f x`,
  57                              REWRITE_TAC[LIN_F_EMPTY; REAL_ADD_RID]);;
  58
  59 let LIN_F_SUM_MOVE1 = prove(`!h t x. lin_f (CONS h t) + lin_f x = lin_f [h] + (lin_f t + lin_f x)`,
  60    REPEAT GEN_TAC THEN REWRITE_TAC[LIN_F_CONS; LIN_F_EMPTY] THEN REAL_ARITH_TAC);;
  61
  62 let LIN_F_SUM_MOVE2 = prove(`!h t x. lin_f x + lin_f (CONS h t) = lin_f [h] + (lin_f x + lin_f t)`,
  63    REPEAT GEN_TAC THEN REWRITE_TAC[LIN_F_CONS; LIN_F_EMPTY] THEN REAL_ARITH_TAC);;
  64
  65
  66 let LIN_F_ADD_SINGLE = prove(`!h t. lin_f [h] + lin_f t = lin_f (CONS h t)`,
  67    REWRITE_TAC[LIN_F_CONS; LIN_F_EMPTY] THEN REAL_ARITH_TAC);;
  68
  69
  70 let LIN_F_ADD_SING_RCANCEL = prove(`!c v t. c * v + lin_f (CONS (--c, v) t)
  71                                        = lin_f t`,
  72    REWRITE_TAC[LIN_F_CONS; LIN_F_EMPTY] THEN REAL_ARITH_TAC);;
  73
  74 let LIN_F_ADD_SING_LCANCEL = prove(`!c v t. --c * v + lin_f (CONS (c, v) t)
  75                                          = lin_f t`,
  76    REWRITE_TAC[LIN_F_CONS; LIN_F_EMPTY] THEN REAL_ARITH_TAC);;
  77
  78
  79 (* Multiplication of lin_f *)
  80
  81 let LIN_F_MUL = prove(`!v t. v * lin_f t = lin_f (MAP (\tm. v * FST tm, SND tm) t)`,
  82    REWRITE_TAC[lin_f] THEN GEN_TAC THEN LIST_INDUCT_TAC THENL
  83      [
  84        REWRITE_TAC[ITLIST; MAP; REAL_MUL_RZERO];
  85        ALL_TAC
  86      ] THEN
  87      REWRITE_TAC[ITLIST; MAP] THEN
  88      ASM_REWRITE_TAC[REAL_ADD_LDISTRIB; REAL_MUL_ASSOC]);;
  89
  90
  91 let LIN_F_MUL_HD = prove(`!x c v t c1. x * c = c1 ==>
  92     x * lin_f (CONS (c,v) t) = lin_f [c1, v] + x * lin_f t`,
  93    REWRITE_TAC[LIN_F_CONS; LIN_F_EMPTY] THEN
  94      REPEAT STRIP_TAC THEN
  95      ASM_REWRITE_TAC[REAL_ARITH `x * (c * v + a) = (x * c) * v + x * a:real`] THEN
  96      REAL_ARITH_TAC);;
  97
  98
  99 let LIN_F_MUL_EMPTY = prove(`!x. x * lin_f [] = lin_f []`,
 100    REWRITE_TAC[LIN_F_EMPTY] THEN REAL_ARITH_TAC);;
 101
 102
 103 (* Theorems for converting sums into lin_f *)
 104 let TO_LIN_F0 = prove(`!x. x = x + lin_f []`, REWRITE_TAC[LIN_F_EMPTY; REAL_ADD_RID]);;
 105
 106 let TO_LIN_F1 = prove(`!a x. a * x = lin_f [a, x]`,
 107    REWRITE_TAC[lin_f; ITLIST; REAL_ADD_RID]);;
 108
 109 let TO_LIN_F = prove(`!c v x t. (c * v + x) + lin_f t = x + lin_f (CONS (c, v) t) /\
 110     c * v + lin_f t = lin_f (CONS (c, v) t)`,
 111    REWRITE_TAC[LIN_F_CONS] THEN REAL_ARITH_TAC);;
 112
 113
 114 (* Special versions of the above theorems (for using with INST) *)
 115
 116 let amp_op = `(&):num->real`;;
 117 let zero_const = `_0`;;
 118
 119 let NUM_ZERO = prove(mk_eq(mk_comb(amp_op,mk_comb(num_const, zero_const)), `&0`),
 120                      REWRITE_TAC[NUM_THM; NUMERAL]);;
 121
 122 let LIN_F_SUM_HD',
 123   LIN_F_SUM_HD_ZERO',
 124   LIN_F_SUM_EMPTY1', LIN_F_SUM_EMPTY2',
 125   LIN_F_SUM_MOVE1', LIN_F_SUM_MOVE2',
 126   LIN_F_ADD_SINGLE' =
 127      UNDISCH_ALL (SPEC_ALL LIN_F_SUM_HD),
 128      UNDISCH_ALL (SPEC_ALL (ONCE_REWRITE_RULE[GSYM NUM_ZERO] LIN_F_SUM_HD_ZERO)),
 129      SPEC_ALL LIN_F_SUM_EMPTY1, SPEC_ALL LIN_F_SUM_EMPTY2,
 130      SPEC_ALL LIN_F_SUM_MOVE1, SPEC_ALL LIN_F_SUM_MOVE2,
 131      SPEC_ALL LIN_F_ADD_SINGLE;;
 132
 133 let LIN_F_MUL_HD', LIN_F_MUL_EMPTY' =
 134   UNDISCH_ALL (SPEC_ALL LIN_F_MUL_HD), SPEC_ALL LIN_F_MUL_EMPTY;;
 135
 136 let LIN_F_ADD_SING_RCANCEL', LIN_F_ADD_SING_LCANCEL' =
 137   SPEC_ALL LIN_F_ADD_SING_RCANCEL, SPEC_ALL LIN_F_ADD_SING_LCANCEL;;
 138
 139
 140 (* A little faster version of PROVE_HYP *)
 141 let MY_PROVE_HYP hyp th = EQ_MP (DEDUCT_ANTISYM_RULE hyp th) hyp;;
 142
 143
 144
 145 (***********************************************)
 146
 147
 148 (* Constants *)
 149
 150 let a_var_real = `a:real` and
 151     b_var_real = `b:real` and
 152     a1_var_real = `a1:real` and
 153     a2_var_real = `a2:real` and
 154     b1_var_real = `b1:real` and
 155     b2_var_real = `b2:real` and
 156     c1_var_real = `c1:real` and
 157     c2_var_real = `c2:real` and
 158     h_var = `h:real#real` and
 159     r_var = `r:(real#real)list` and
 160     x_var = `x:(real#real)list` and
 161     y_var = `y:(real#real)list` and
 162     t_var = `t:(real#real)list` and
 163     x_var_real = `x:real` and
 164     c1_var = `c1:real` and
 165     c2_var = `c2:real` and
 166     c_var = `c:real` and
 167     v_var = `v:real` and
 168     t1_var = `t1:(real#real)list` and
 169     t2_var = `t2:(real#real)list` and
 170     empty_const = `[]:(real)list`;;
 171
 172 let cons_const = `CONS:(real#real)->(real#real)list->(real#real)list` and
 173     empty_const = `[]:(real)list`;;
 174
 175 let plus_op = `(+):real->real->real` and
 176     plus_op_num = `(+):num->num->num` and
 177     le_op = `(<=):real->real->bool` and
 178     ge_op = `(>=):real->real->bool` and
 179     mul_op = `( * ):real->real->real` and
 180     neg_op = `(--):real->real`;;
 181
 182 let real_type = `:real`;;
 183
 184
 185 (* Term constructors *)
 186 let cons h t = mk_comb (mk_comb (cons_const, h), t);;
 187 let negate tm = mk_comb (neg_op, tm);;
 188 let mk_real_int n = mk_comb(amp_op, mk_numeral_array n);;
 189 let mk_real_int64 n = mk_comb(amp_op, mk_int64_numeral_array n);;
 190 let mk_linear cs vars =
 191   let mk_term (c, var) = mk_binop mul_op c (mk_var (var, real_type)) in
 192     list_mk_binop plus_op (map mk_term (zip cs vars));;
 193
 194 let mk_le_ineq lhs rhs = mk_binop le_op lhs rhs;;
 195 let mk_eq_ineq lhs rhs = mk_eq (lhs, rhs);;
 196 let mk_ge_ineq lhs rhs = mk_binop ge_op lhs rhs;;
 197
 198
 199
 200 (************************************************)
 201
 202 (* Computes (lin_f x + lin_f y) with REAL_BITS_ADD_CONV *)
 203 let lin_f_add_conv tm =
 204   let rec lin_f_add_conv2 x y =
 205     if (is_comb y) then
 206       if (is_comb x) then
 207         let hx = rand (rator x) in
 208         let hy = rand (rator y) in
 209         let c1, v1 = dest_pair hx in
 210         let c2, v2 = dest_pair hy in
 211
 212           if v1 = v2 then
 213             let tx, ty = rand x, rand y in
 214             let c_thm = REAL_BITS_ADD_CONV (mk_binop plus_op c1 c2) in
 215             let c = rand (concl c_thm) in
 216               if (rand(rand c) = zero_const) then
 217                 let th0 = INST [v1, v_var; c1, c1_var; tx, t1_var; c2, c2_var; ty, t2_var]
 218                   LIN_F_SUM_HD_ZERO' in
 219                   TRANS (MY_PROVE_HYP c_thm th0) (lin_f_add_conv2 tx ty)
 220               else
 221                 let th0 = INST[v1, v_var; c1, c1_var; tx, t1_var; c2, c2_var; ty, t2_var; c, c_var]
 222                   LIN_F_SUM_HD' in
 223                 let ltm = rator (rand(concl th0)) in
 224                 let th1 = lin_f_add_conv2 tx ty in
 225                 let th2 = TRANS (MY_PROVE_HYP c_thm th0) (AP_TERM ltm th1) in
 226                 let th3 = INST[mk_pair (c, v1), h_var; rand(rand(concl th1)), t_var] LIN_F_ADD_SINGLE' in
 227                   TRANS th2 th3
 228           else
 229             if (v1 < v2) then
 230               let tx = rand x in
 231               let th0 = INST[hx, h_var; tx, t_var; y, x_var] LIN_F_SUM_MOVE1' in
 232               let ltm = rator (rand(concl th0)) in
 233               let th1 = lin_f_add_conv2 tx y in
 234               let th2 = TRANS th0 (AP_TERM ltm th1) in
 235               let th3 = INST[hx, h_var; rand(rand(concl th1)), t_var] LIN_F_ADD_SINGLE' in
 236                 TRANS th2 th3
 237             else
 238               let ty = rand y in
 239               let th0 = INST[hy, h_var; ty, t_var; x, x_var] LIN_F_SUM_MOVE2' in
 240               let ltm = rator (rand(concl th0)) in
 241               let th1 = lin_f_add_conv2 x ty in
 242               let th2 = TRANS th0 (AP_TERM ltm th1) in
 243               let th3 = INST[hy, h_var; rand(rand(concl th1)), t_var] LIN_F_ADD_SINGLE' in
 244                 TRANS th2 th3
 245       else
 246         (* x = [] *)
 247         INST[y, x_var] LIN_F_SUM_EMPTY1'
 248     else
 249       (* y = [] *)
 250       INST[x, x_var] LIN_F_SUM_EMPTY2' in
 251
 252   let larg, rarg = dest_comb tm in
 253   let larg = rand larg in
 254     lin_f_add_conv2 (rand larg) (rand rarg);;
 255
 256
 257
 258 (*********************)
 259 (* lin_f conversions *)
 260 (*********************)
 261
 262
 263 (* Transforms a sum in the form `a * x + b * y + c * z` into `lin_f [(c,z); (b,y); (a,x)]` *)
 264 let LIN_F_RAW_CONV = ONCE_REWRITE_CONV[TO_LIN_F0] THENC REWRITE_CONV[TO_LIN_F];;
 265
 266 let LIN_F_ADD_CONV = lin_f_add_conv;;
 267
 268 (* Transforms a sum into `lin_f` and sorts the terms *)
 269 let LIN_F_CONV = (REWRITE_CONV[TO_LIN_F1] THENC (DEPTH_CONV LIN_F_ADD_CONV));;
 270
 271
 272 (* Computes `v * lin_f y` *)
 273
 274 let rec LIN_F_MUL_CONV tm =
 275   let x, f = dest_binop mul_op tm in
 276   let list = rand f in
 277     if (is_comb list) then
 278       let cons_h, t = dest_comb list in
 279       let h = rand cons_h in
 280       let c, v = dest_pair h in
 281
 282       let product = REAL_BITS_MUL_CONV (mk_binop mul_op x c) in
 283       let c1 = rand(concl product) in
 284       let th = INST[x, x_var_real; c, c_var; v, v_var; t, t_var; c1, c1_var] LIN_F_MUL_HD' in
 285       let th1 = MY_PROVE_HYP product th in
 286       let lplus, tm = dest_comb(rand(concl th1)) in
 287       let th2 = LIN_F_MUL_CONV tm in
 288       let h = mk_pair (c1, v) in
 289       let t = rand(rand(concl th2)) in
 290       let th3 = TRANS th1 (AP_TERM lplus th2) in
 291       let th4 = INST[h, h_var; t, t_var] LIN_F_ADD_SINGLE' in
 292         TRANS th3 th4
 293     else
 294       INST[x, x_var_real] LIN_F_MUL_EMPTY';;
 295
 296
 297 (* Conversion without numerical multiplication *)
 298 let LIN_F_MUL_RAW_CONV = ONCE_REWRITE_CONV[LIN_F_MUL] THENC REWRITE_CONV[MAP];;
 299
 300
 301
 302 (************************************************)
 303
 304
 305 (* Creates an inequality in the correct form *)
 306 let REAL_POS' = SPEC_ALL REAL_POS;;
 307 let REAL_LE_LMUL' = UNDISCH_ALL (REWRITE_RULE[GSYM IMP_IMP] (SPEC_ALL REAL_LE_LMUL));;
 308 let n_var_num = `n:num`;;
 309 let x_var_real = `x:real`;;
 310 let y_var_real = `y:real`;;
 311 let z_var_real = `z:real`;;
 312
 313
 314 let transform_le_ineq (ineq, m) =
 315   let lhs, rhs = dest_binop le_op (concl ineq) in
 316   let lhs_f_th = LIN_F_CONV lhs in
 317   let original_th = EQ_MP (AP_THM (AP_TERM le_op lhs_f_th) rhs) ineq in
 318   let lhs = rand(concl lhs_f_th) in
 319   let pos_th = INST[rand m, n_var_num] REAL_POS' in
 320   let th0 = INST[m, x_var_real; lhs, y_var_real; rhs, z_var_real] REAL_LE_LMUL' in
 321   let th1 = MY_PROVE_HYP pos_th th0 in
 322   let th2 = MY_PROVE_HYP original_th th1 in
 323   let lhs, rhs = dest_binop le_op (concl th2) in
 324   let lhs_th = LIN_F_MUL_CONV lhs in
 325   let rhs_th = REAL_BITS_MUL_CONV rhs in
 326   let th3 = MK_COMB(AP_TERM le_op lhs_th, rhs_th) in
 327     EQ_MP th3 th2;;
 328
 329
 330 let transform_le_ineq_tm (ineq, m) =
 331   let lhs, rhs = dest_binop le_op ineq in
 332   let lhs_f_th = LIN_F_CONV lhs in
 333   let original_th = EQ_MP (AP_THM (AP_TERM le_op lhs_f_th) rhs) (ASSUME ineq) in
 334   let lhs = rand(concl lhs_f_th) in
 335   let pos_th = INST[rand m, n_var_num] REAL_POS' in
 336   let th0 = INST[m, x_var_real; lhs, y_var_real; rhs, z_var_real] REAL_LE_LMUL' in
 337   let th1 = MY_PROVE_HYP pos_th th0 in
 338   let th2 = MY_PROVE_HYP original_th th1 in
 339   let lhs, rhs = dest_binop le_op (concl th2) in
 340   let lhs_th = LIN_F_MUL_CONV lhs in
 341   let rhs_th = REAL_BITS_MUL_CONV rhs in
 342   let th3 = MK_COMB(AP_TERM le_op lhs_th, rhs_th) in
 343     EQ_MP th3 th2;;
 344
 345
 346
 347 (* Computes the sum of two inequalities *)
 348 let REAL_LE_ADD2' = UNDISCH_ALL (REWRITE_RULE[GSYM IMP_IMP] (SPEC_ALL REAL_LE_ADD2));;
 349 let w_var_real = `w:real`;;
 350
 351 (* Computes the sum of two inequalities (with LIN_F_ADD_CONV and REAL_BITS_ADD_CONV) *)
 352 let add_step' ineq1 ineq2 =
 353   let lhs1, rhs1 = dest_binop le_op (concl ineq1) in
 354   let lhs2, rhs2 = dest_binop le_op (concl ineq2) in
 355   let th0 = INST [lhs1, w_var_real; rhs1, x_var_real; lhs2, y_var_real; rhs2, z_var_real]
 356     REAL_LE_ADD2' in
 357   let th1 = MY_PROVE_HYP ineq2 (MY_PROVE_HYP ineq1 th0) in
 358   let lhs, rhs = dest_binop le_op (concl th1) in
 359   let lhs_th = LIN_F_ADD_CONV lhs in
 360   let rhs_th = REAL_BITS_ADD_CONV rhs in
 361     EQ_MP (MK_COMB(AP_TERM le_op lhs_th, rhs_th)) th1;;
 362
 363
 364 (* Computes the sum of lin_f[--c, x;...] and c * x *)
 365 let add_cancel_step ineq var_ineq =
 366   let lhs1, rhs1 = dest_binop le_op (concl var_ineq) in
 367   let lhs2, rhs2 = dest_binop le_op (concl ineq) in
 368   let th0 = INST[lhs1, w_var_real; rhs1, x_var_real; lhs2, y_var_real; rhs2, z_var_real]
 369     REAL_LE_ADD2' in
 370   let th1 = MY_PROVE_HYP ineq (MY_PROVE_HYP var_ineq th0) in
 371   let ctm, vtm = dest_binop mul_op lhs1 in
 372   let ttm = rand(rand lhs2) in
 373     if (rator ctm = neg_op) then
 374       let lhs_th = INST[rand ctm, c_var; vtm, v_var; ttm, t_var] LIN_F_ADD_SING_LCANCEL' in
 375       let rhs_th = REAL_BITS_ADD_CONV (rand(concl th1)) in
 376         EQ_MP (MK_COMB(AP_TERM le_op lhs_th, rhs_th)) th1
 377     else
 378       let lhs_th = INST[ctm, c_var; vtm, v_var; ttm, t_var] LIN_F_ADD_SING_RCANCEL' in
 379       let rhs_th = REAL_BITS_ADD_CONV (rand(concl th1)) in
 380         EQ_MP (MK_COMB(AP_TERM le_op lhs_th, rhs_th)) th1;;
 381
 382
 383
 384 let zero_const_real = `&0`;;
 385
 386 (* Multiplies a linear inequality by a rational positive constant *)
 387 let mul_rat_step ineq c =
 388   let pos_thm = REAL_ARITH (mk_le_ineq zero_const_real c) in
 389   let hyp = CONJ pos_thm ineq in
 390   let th0 = MATCH_MP REAL_LE_LMUL hyp in
 391   let lhs, rhs = dest_binop le_op (concl th0) in
 392   let lhs_th = (LIN_F_MUL_RAW_CONV THENC DEPTH_CONV REAL_RAT_MUL_CONV) lhs in
 393   let rhs_th = REAL_RAT_MUL_CONV rhs in
 394     EQ_MP (MK_COMB (AP_TERM le_op lhs_th, rhs_th)) th0;;
 395
 396
 397
 398 (* Multiplies a linear inequality in the form lin_f x <= y by
 399    a positive integer c *)
 400 let mul_step ineq c =
 401   let lhs, rhs = dest_binop le_op (concl ineq) in
 402   let pos_th = INST[rand c, n_var_num] REAL_POS' in
 403   let th0 = INST[c, x_var_real; lhs, y_var_real; rhs, z_var_real] REAL_LE_LMUL' in
 404   let th1 = MY_PROVE_HYP pos_th th0 in
 405   let th2 = MY_PROVE_HYP ineq th1 in
 406   let lhs, rhs = dest_binop le_op (concl th2) in
 407   let lhs_th = LIN_F_MUL_CONV lhs in
 408   let rhs_th = REAL_BITS_MUL_CONV rhs in
 409   let th3 = MK_COMB(AP_TERM le_op lhs_th, rhs_th) in
 410     EQ_MP th3 th2;;
 411
 412
 413
 414 (* Transformations for variables *)
 415
 416 let VAR_MUL_THM = prove(`!x c1 c2 a b v. &0 <= x /\ x * c1 = a /\ x * c2 = b /\ c1 * v <= c2
 417     ==> a * v <= b`,
 418    REPEAT STRIP_TAC THEN
 419      UNDISCH_TAC `x * c1 = a:real` THEN DISCH_THEN (fun th -> REWRITE_TAC[SYM th]) THEN
 420      UNDISCH_TAC `x * c2 = b:real` THEN DISCH_THEN (fun th -> REWRITE_TAC[SYM th]) THEN
 421      REWRITE_TAC[GSYM REAL_MUL_ASSOC] THEN
 422      MATCH_MP_TAC REAL_LE_LMUL THEN
 423      ASM_REWRITE_TAC[]);;
 424
 425
 426 let VAR_MUL_THM' = (UNDISCH_ALL o SPEC_ALL o (REWRITE_RULE[GSYM IMP_IMP])) VAR_MUL_THM;;
 427
 428 let VAR_ADD_THM = prove(`!x a1 b1 a2 b2 c1 c2. a1 * x <= b1 /\ a2 * x <= b2 /\
 429                           a1 + a2 = c1 /\ b1 + b2 = c2 ==> c1 * x <= c2`,
 430                         REPEAT STRIP_TAC THEN
 431                           EXPAND_TAC "c1" THEN EXPAND_TAC "c2" THEN
 432                           REWRITE_TAC[REAL_ADD_RDISTRIB] THEN
 433                           MATCH_MP_TAC REAL_LE_ADD2 THEN
 434                           ASM_REWRITE_TAC[]);;
 435
 436 let VAR_ADD_THM' = (UNDISCH_ALL o SPEC_ALL o (REWRITE_RULE[GSYM IMP_IMP])) VAR_ADD_THM;;
 437
 438
 439 (* Multiplies c1 * x <= c2 by m *)
 440 let var1_le_transform (var_ineq, m) =
 441   let lhs, c2tm = dest_binop le_op (var_ineq) in
 442   let pos_th = INST[rand m, n_var_num] REAL_POS' in
 443   let c1tm, xtm = dest_binop mul_op lhs in
 444   let c1_th = REAL_BITS_MUL_CONV (mk_binop mul_op m c1tm) in
 445   let c2_th = REAL_BITS_MUL_CONV (mk_binop mul_op m c2tm) in
 446   let th = INST[m, x_var_real; c1tm, c1_var; c2tm, c2_var; xtm, v_var;
 447               rand(concl c1_th), a_var_real; rand(concl c2_th), b_var_real]
 448     VAR_MUL_THM' in
 449     MY_PROVE_HYP pos_th (MY_PROVE_HYP (ASSUME var_ineq) (MY_PROVE_HYP c1_th (MY_PROVE_HYP c2_th th)));;
 450
 451
 452 (* Multiplies the corresponding inequalities and finds the sum of results *)
 453 let var2_le_transform (var_ineq1,m1) (var_ineq2,m2) =
 454   let ineq1 = var1_le_transform (var_ineq1, m1) and
 455       ineq2 = var1_le_transform (var_ineq2, m2) in
 456   let lhs1, b1tm = dest_binop le_op (concl ineq1) in
 457   let lhs2, b2tm = dest_binop le_op (concl ineq2) in
 458   let a1tm, xtm = dest_binop mul_op lhs1 in
 459   let a2tm = rand(rator lhs2) in
 460   let b_th = REAL_BITS_ADD_CONV (mk_binop plus_op b1tm b2tm) in
 461   let a_th = REAL_BITS_ADD_CONV (mk_binop plus_op a1tm a2tm) in
 462   let th0 = INST[a1tm, a1_var_real; a2tm, a2_var_real;
 463                  b1tm, b1_var_real; b2tm, b2_var_real;
 464                  rand(concl a_th), c1_var_real; rand(concl b_th), c2_var_real;
 465                  xtm, x_var_real] VAR_ADD_THM' in
 466     MY_PROVE_HYP ineq2 (MY_PROVE_HYP ineq1 (MY_PROVE_HYP b_th (MY_PROVE_HYP a_th th0)));;
 467
 468
 469
 470
 471
 472 (* The main function *)
 473 (* Example: prove_lp ineqs var_ineqs target_vars `&12` (Int 100000) *)
 474 (* ineq - inequalities obtained from constraints with multipliers *)
 475 (* var_ineqs - bounds for variables as inequalities in the correct form *)
 476 (* target_vars - bounds and multipliers for variables in the objective function *)
 477 (* bound - a bound for the objective function which is proved *)
 478 (* m - a precision constant *)
 479
 480
 481 let LIN_F_EMPTY_LE_0 = prove(`lin_f [] <= &0`, REWRITE_TAC[LIN_F_EMPTY; REAL_LE_REFL]);;
 482 let dummy = REWRITE_RULE[GSYM NUM_ZERO] LIN_F_EMPTY_LE_0;;
 483
 484
 485 let prove_lp_tm ineqs var_ineqs target_vars target_bound precision_constant =
 486   (* Compute the sum of all constraints *)
 487   let r1 = map transform_le_ineq_tm ineqs in
 488   let r2' = List.fold_left add_step' dummy r1 in
 489   let r2 = mul_step r2' (mk_real_int precision_constant) in
 490
 491   (* Use bounds of variables *)
 492   let r3 = List.fold_left add_cancel_step r2 var_ineqs in
 493   let r4 = List.fold_left add_step' dummy (map transform_le_ineq_tm target_vars) in
 494   let r5 = add_step' r3 r4 in
 495
 496   (* Convert the result into a usual form *)
 497   let r6 = CONV_RULE (DEPTH_CONV NUM_TO_NUMERAL_CONV) r5 in
 498   let m = term_of_rat (precision_constant */ precision_constant */ precision_constant) in
 499   let r7 = mul_rat_step r6 (mk_comb (`(/) (&1)`, m)) in
 500   let r8 = REWRITE_RULE[lin_f; ITLIST; REAL_ADD_RID] r7 in
 501   let r9 = EQT_ELIM (REAL_RAT_LE_CONV (mk_binop le_op ((rand o concl) r8) target_bound)) in
 502     MATCH_MP REAL_LE_TRANS (CONJ r8 r9);;
 503
 504
 505 let prove_lp ineqs var_ineqs target_vars target_bound precision_constant =
 506   (* Compute the sum of all constraints *)
 507   let r1 = map transform_le_ineq ineqs in
 508   let r2' = List.fold_left add_step' dummy r1 in
 509   let r2 = mul_step r2' (mk_real_int precision_constant) in
 510
 511   (* Use bounds of variables *)
 512   let r3 = List.fold_left add_cancel_step r2 var_ineqs in
 513   let r4 = List.fold_left add_step' dummy (map transform_le_ineq target_vars) in
 514   let r5 = add_step' r3 r4 in
 515
 516   (* Convert the result into a usual form *)
 517   let r6 = CONV_RULE (DEPTH_CONV NUM_TO_NUMERAL_CONV) r5 in
 518   let m = term_of_rat (precision_constant */ precision_constant */ precision_constant) in
 519   let r7 = mul_rat_step r6 (mk_comb (`(/) (&1)`, m)) in
 520   let r8 = REWRITE_RULE[lin_f; ITLIST; REAL_ADD_RID] r7 in
 521   let r9 = EQT_ELIM (REAL_RAT_LE_CONV (mk_binop le_op ((rand o concl) r8) target_bound)) in
 522     MATCH_MP REAL_LE_TRANS (CONJ r8 r9);;
 523