1314564Sdimstructure OmegaMath :> OmegaMath = struct 2283625Sdim 3353358Sdimopen HolKernel boolLib intSyntax integerTheory int_arithTheory 4353358Sdimopen CooperMath 5353358Sdimlocal open OmegaTheory in end 6283625Sdim 7283625Sdim(* Fix the grammar used by this file *) 8283625Sdimval ctxt_grammars = (Parse.type_grammar(), Parse.term_grammar()) 9283625Sdimval _ = Parse.temp_set_grammars int_arith_grammars 10283625Sdim 11314564Sdimval REWRITE_CONV = GEN_REWRITE_CONV TOP_DEPTH_CONV bool_rewrites 12283625Sdim 13283625Sdim 14314564Sdimfun ERR f msg = HOL_ERR { origin_structure = "OmegaMath", 15314564Sdim origin_function = f, 16283625Sdim message = msg} 17283625Sdimval lhand = rand o rator 18309124Sdim 19283625Sdim(* ---------------------------------------------------------------------- 20314564Sdim find_summand v tm 21283625Sdim 22283625Sdim finds the summand involving variable v in tm. Raise a HOL_ERR if it's 23283625Sdim not there. tm must be a left-associated sum with one numeral in the 24283625Sdim rightmost position. 25283625Sdim ---------------------------------------------------------------------- *) 26283625Sdim 27283625Sdimexception fs_NotFound 28283625Sdimfun find_summand v tm = let 29283625Sdim fun recurse tm = let 30283625Sdim val (l,r) = dest_plus tm 31283625Sdim in 32283625Sdim if rand r = v then r else recurse l 33283625Sdim end handle HOL_ERR _ => if rand tm = v then tm else raise fs_NotFound 34283625Sdimin 35 recurse (lhand tm) handle fs_NotFound => 36 raise ERR "find_summand" "No such summand" 37end 38 39 40(* ---------------------------------------------------------------------- 41 gcd_eq_check tm 42 43 tm must be of the form 44 0 = r1 + .. + rn 45 where rn is a numeral and all of the other ri's are of the form 46 (numeral * variable) 47 48 If all of the variables have coefficients divisible by some common 49 factor, then this conversion returns an equality either with all the 50 coefficients appropriately smaller, or equating it to false (which 51 will happen if there the numeral term is of the wrong divisibility). 52 53 If there are no variables, will evaluation 0 = rn to true or false. 54 55 If there is nothing to eliminate, then return QConv.UNCHANGED. 56 ---------------------------------------------------------------------- *) 57 58exception Foo 59fun gcd_eq_check tm = let 60 open Arbint 61 val INT_RING_CONV = 62 EQT_ELIM o (REWRITE_CONV [INT_LDISTRIB, INT_MUL_ASSOC] THENC REDUCE_CONV) 63 val r = rand tm 64 val summands = strip_plus r 65 val (vars, numpart) = front_last summands 66 val _ = not (null vars) orelse raise Foo 67 val numpart_i = int_of_term numpart 68 val coeffs = map (abs o int_of_term o #1 o dest_mult) vars 69 val g = gcdl coeffs 70 val _ = g <> one orelse raise UNCHANGED 71 val g_t = term_of_int g 72 fun mapthis t = let 73 val (c, v) = dest_mult t 74 val newc = term_of_int (int_of_term c div g) 75 in 76 mk_mult(newc, v) 77 end 78 val newvars_sum = list_mk_plus (map mapthis vars) 79 val (nq, nr) = divmod(numpart_i, g) 80in 81 if nr = zero then let 82 val varpart = mk_mult(g_t, mk_plus(newvars_sum, term_of_int nq)) 83 val newrhs_th = AP_TERM (rator tm) (INT_RING_CONV(mk_eq(r, varpart))) 84 in 85 K newrhs_th THENC REWR_CONV EQ_SYM_EQ THENC REWR_CONV INT_ENTIRE THENC 86 LAND_CONV REDUCE_CONV THENC REWR_CONV CooperThms.F_or_l THENC 87 REWR_CONV EQ_SYM_EQ 88 end 89 else let 90 val newlhs = mk_negated numpart 91 val newrhs = mk_plus(mk_mult(g_t, newvars_sum), numpart) 92 val newrhs_th = AP_TERM (rator tm) (INT_RING_CONV(mk_eq(r, newrhs))) 93 val g_num_t = rand g_t 94 val g_num_nonzero = 95 EQT_ELIM (REDUCE_CONV 96 (mk_neg(mk_eq(g_num_t, numSyntax.zero_tm)))) 97 in 98 K newrhs_th THENC REWR_CONV eq_move_right_left THENC 99 REWR_CONV EQ_SYM_EQ THENC RAND_CONV (REWR_CONV INT_ADD_LID) THENC 100 K (MP (SPECL [g_num_t, newvars_sum, newlhs] elim_eq_coeffs) 101 g_num_nonzero) THENC 102 LAND_CONV REDUCE_CONV THENC REWR_CONV CooperThms.F_and_l 103 end 104end tm handle Foo => REDUCE_CONV tm 105 106(* ---------------------------------------------------------------------- 107 gcd_le_check tm 108 109 performs a "gcd check" for terms of the form 110 0 <= (c1 * v1) + (c2 * v2) + .. + (cn * vn) + n 111 if there are no variables, evaluates 0 <= n to true or false. 112 ---------------------------------------------------------------------- *) 113 114fun gcd_le_check tm = let 115 open Arbint 116 val INT_RING_CONV = 117 EQT_ELIM o (REWRITE_CONV [INT_LDISTRIB, INT_MUL_ASSOC] THENC REDUCE_CONV) 118 val r = rand tm 119 val (varpart, numpart) = dest_plus r handle HOL_ERR _ => raise Foo 120 val vars = strip_plus varpart 121 val numpart_i = int_of_term numpart 122 val coeffs = map (abs o int_of_term o #1 o dest_mult) vars 123 val g = gcdl coeffs 124 val _ = g <> one orelse raise UNCHANGED 125 val g_t = term_of_int g 126 val zero_lt_g = EQT_ELIM (REDUCE_CONV (mk_less(zero_tm, g_t))) 127 fun mapthis t = let 128 val (c,v) = dest_mult t 129 in 130 mk_mult(term_of_int (int_of_term c div g), v) 131 end 132 val newvars_sum = list_mk_plus (map mapthis vars) 133 val newrhs = mk_plus(mk_mult(g_t, newvars_sum), numpart) 134 val newrhs_th = AP_TERM (rator tm) (INT_RING_CONV (mk_eq(r, newrhs))) 135in 136 K newrhs_th THENC 137 K (MP (SPECL [g_t, numpart, newvars_sum] elim_le_coeffs) zero_lt_g) THENC 138 RAND_CONV (RAND_CONV REDUCE_CONV) 139end tm handle Foo => REDUCE_CONV tm 140 141(* ---------------------------------------------------------------------- 142 gcd_check tm 143 144 combines the above two checks, depending on the relational symbol of 145 the term. 146 ---------------------------------------------------------------------- *) 147 148fun gcd_check tm = 149 case #Name (dest_thy_const (#1 (strip_comb tm))) of 150 "int_le" => gcd_le_check tm 151 | "=" => gcd_eq_check tm 152 | _ => raise ERR "gcd_check" "Term not an = or <=" 153 154(* ---------------------------------------------------------------------- 155 addzero t 156 157 if t (of integer type and not a numeral itself) does not have a 158 numeral as its 'rand, then return thm |- t = t + 0, otherwise 159 ALL_CONV. 160 ---------------------------------------------------------------------- *) 161 162fun addzero t = 163 if is_int_literal t orelse is_int_literal (rand t) then ALL_CONV t 164 else SYM (SPEC t INT_ADD_RID) 165 166(* ---------------------------------------------------------------------- 167 LASSOC_ADD_CONV tm 168 169 left-associates a single addition, turning a + (b + c) into 170 (a + b) + c 171 ---------------------------------------------------------------------- *) 172 173val LASSOC_ADD_CONV = REWR_CONV INT_ADD_ASSOC 174 175(* ---------------------------------------------------------------------- 176 RASSOC_ADD_CONV tm 177 178 right-associates a single addition, turning (a + b) + c into 179 a + (b + c) 180 ---------------------------------------------------------------------- *) 181 182val RASSOC_ADD_CONV = let 183 val th = GSYM INT_ADD_ASSOC 184in 185 REWR_CONV th 186end 187 188(* ---------------------------------------------------------------------- 189 RTOP_TWO_CONV c tm 190 191 applies conversion c to the term a + b, where a and b are the 192 two rightmost summands of tm. The term is reassociated to present 193 these two terms this way if necessary, and then put back into left- 194 associative afterwards if necessary. c should produce at most an 195 addition of two terms. 196 ---------------------------------------------------------------------- *) 197 198fun RTOP_TWO_CONV c tm = let 199 val (l,r) = dest_plus tm 200in 201 if is_plus l then 202 RASSOC_ADD_CONV THENC RAND_CONV c THENC 203 TRY_CONV LASSOC_ADD_CONV 204 else 205 c 206end tm 207 208(* ---------------------------------------------------------------------- 209 PAIRWISE_GATHER_CONV tm 210 211 given that tm = tm1 + tm2, returns an equation of the form 212 tm1 + tm2 = result 213 where result is a "gathering" transformation as per 214 SORT_AND_GATHER1_CONV below 215 ---------------------------------------------------------------------- *) 216 217val SYM_RDISTRIB = GSYM INT_RDISTRIB 218fun PAIRWISE_GATHER_CONV tm = let 219 val (tm1,tm2) = dest_plus tm 220in 221 if is_int_literal tm1 then 222 if is_int_literal tm2 then REDUCE_CONV 223 else (* is_mult tm2 *) REWR_CONV INT_ADD_COMM 224 else (* is_mult tm1 *) 225 if is_int_literal tm2 then ALL_CONV 226 else (* is_mult tm2 *) let 227 val (c1,v1) = dest_mult tm1 228 val (c2,v2) = dest_mult tm2 229 in 230 case Term.compare(v1,v2) of 231 LESS => ALL_CONV 232 | EQUAL => REWR_CONV SYM_RDISTRIB THENC LAND_CONV REDUCE_CONV 233 | GREATER => REWR_CONV INT_ADD_COMM 234 end 235end tm 236 237(* ---------------------------------------------------------------------- 238 CHECK_ZERO_CONV tm 239 240 checks for summands of tm being of the form 241 0 * y 242 and eliminates them. Assume that tm is left-associated, and with 243 a numeral as its rightmost summand. 244 ---------------------------------------------------------------------- *) 245 246val CHECK_RZERO_CONV = let 247 fun recurse tm = let 248 val (l,r) = dest_plus tm 249 in 250 case total dest_plus l of 251 SOME(ll, lr) => let 252 val (c,v) = dest_mult lr 253 in 254 if c = zero_tm then 255 LAND_CONV (RAND_CONV (REWR_CONV INT_MUL_LZERO) THENC 256 REWR_CONV INT_ADD_RID) THENC recurse 257 else LAND_CONV recurse 258 end 259 | NONE => let 260 val (c,v) = dest_mult l 261 in 262 if c = zero_tm then LAND_CONV (REWR_CONV INT_MUL_LZERO) THENC 263 REWR_CONV INT_ADD_LID 264 else ALL_CONV 265 end 266 end tm 267in 268 TRY_CONV recurse 269end 270 271(* ---------------------------------------------------------------------- 272 SORT_AND_GATHER1_CONV tm 273 274 effectively does one step of an insertion sort on tm. Taking a term 275 of the form 276 x + y 277 where y is not itself an addition, and where x is already in normal 278 form, this function transforms the input by moving y left "into" x 279 until it comes to the appropriate resting place. 280 281 Transformations and continuations are 282 283 ... + num1 + num2 --> ... + num stop 284 ... + c * v + num --> ... + c * v + num stop 285 ... + num + c * v --> ... + c * v + num cont 286 ... + c1 * v1 + c2 * v2 --> ... + c1 * v1 + c2 * v2 stop (if v1 < v2) 287 ... + c1 * v1 + c2 * v1 --> ... + (c1 + c2) * v1 stop 288 ... + c1 * v1 + c2 * v2 --> ... + c2 * v2 + c1 * v1 cont (if v2 < v1) 289 290 Eliminates summands which have zero coefficients, as long as the 291 term being inserted into is in normal form, complete with numeral 292 as rightmost summand. 293 294 ---------------------------------------------------------------------- *) 295 296fun SORT_AND_GATHER1_CONV tm = 297 (RTOP_TWO_CONV PAIRWISE_GATHER_CONV THENC 298 TRY_CONV (LAND_CONV SORT_AND_GATHER1_CONV) THENC 299 CHECK_RZERO_CONV) tm 300 301(* ---------------------------------------------------------------------- 302 INTERNAL_SG1_CONV tm 303 304 does the insertion sort of SORT_AND_GATHER1_CONV, but doesn't 305 attempt to normalise zero-coefficients. 306 307 ---------------------------------------------------------------------- *) 308 309fun INTERNAL_SG1_CONV tm = 310 (RTOP_TWO_CONV PAIRWISE_GATHER_CONV THENC 311 TRY_CONV (LAND_CONV INTERNAL_SG1_CONV)) tm 312 313(* ---------------------------------------------------------------------- 314 SORT_AND_GATHER_CONV tm 315 316 perform SORT_AND_GATHER1_CONV steps repeatedly to sort a sum term. 317 ---------------------------------------------------------------------- *) 318 319fun SORT_AND_GATHER_CONV tm = let 320 fun prepare_insertion tm = 321 (* term is a sum, if right argument is singleton, insert it using 322 SORT_AND_GATHER1_CONV, otherwise, reassociate and recurse *) 323 if is_plus (rand tm) then 324 (LASSOC_ADD_CONV THENC LAND_CONV SORT_AND_GATHER_CONV THENC 325 SORT_AND_GATHER_CONV) tm 326 else 327 INTERNAL_SG1_CONV tm 328in 329 if is_plus tm then 330 LAND_CONV SORT_AND_GATHER_CONV THENC prepare_insertion THENC 331 addzero THENC CHECK_RZERO_CONV 332 else 333 addzero THENC CHECK_RZERO_CONV 334end tm 335 336(* ---------------------------------------------------------------------- 337 S_AND_G_MULT tm 338 339 as for SORT_AND_GATHER_CONV, but also taking into account summands 340 of the form c * (...) where the ... represents another summand. 341 ---------------------------------------------------------------------- *) 342 343fun S_AND_G_MULT tm = let 344 fun prepare_insertion tm = 345 (* term is a sum, if right argument is singleton, insert it using 346 SORT_AND_GATHER1_CONV, otherwise, reassociate and recurse *) 347 if is_plus (rand tm) then 348 (LASSOC_ADD_CONV THENC LAND_CONV S_AND_G_MULT THENC S_AND_G_MULT) tm 349 else if is_mult (rand tm) andalso not (is_var (rand (rand tm))) then 350 (RAND_CONV LINEAR_MULT THENC prepare_insertion) tm 351 else 352 SORT_AND_GATHER1_CONV tm 353in 354 if is_plus tm then 355 LAND_CONV S_AND_G_MULT THENC prepare_insertion 356 else if is_mult tm andalso not (is_var (rand tm)) then 357 CooperMath.LINEAR_MULT THENC S_AND_G_MULT 358 else 359 ALL_CONV 360end tm 361 362 363 364 365(* ---------------------------------------------------------------------- 366 NEG_SUM_CONV tm 367 368 tm of form ~(cv + dv + ev + n) 369 ---------------------------------------------------------------------- *) 370 371fun NEG_SUM_CONV tm = 372 ((REWR_CONV INT_NEG_ADD THENC BINOP_CONV NEG_SUM_CONV) ORELSEC 373 (REWR_CONV INT_NEG_LMUL THENC 374 TRY_CONV (LAND_CONV (REWR_CONV INT_NEGNEG))) ORELSEC 375 TRY_CONV (REWR_CONV INT_NEGNEG)) tm 376 377 378(* ---------------------------------------------------------------------- 379 MOVE_VCOEFF_TO_FRONT v tm 380 381 moves the summand featuring variable v to the front of the sum 382 tm. Of course, this doesn't preserve the order in the sum. 383 ---------------------------------------------------------------------- *) 384 385(* ``!x y. x = y + (x + ~y)`` *) 386val front_put_thm = prove( 387 ``!x y. x = y + (x + ~y)``, 388 REPEAT GEN_TAC THEN 389 CONV_TAC (RAND_CONV (RAND_CONV (REWR_CONV INT_ADD_COMM))) THEN 390 REWRITE_TAC [INT_ADD_ASSOC, INT_ADD_RINV, INT_ADD_LID]); 391fun MOVE_VCOEFF_TO_FRONT v tm = let 392 val cv = find_summand v tm 393 val th = SPECL [tm,cv] front_put_thm 394in 395 K th THENC RAND_CONV (RAND_CONV NEG_SUM_CONV THENC SORT_AND_GATHER1_CONV) 396end tm 397 398(* ---------------------------------------------------------------------- 399 NORMALISE_MULT tm 400 401 normalises the multiplicative term tm, gathering up coefficients, 402 and ususally turning it into the form n * (v1 * v2 * ... vn), 403 where n is a numeral and the v's are the other multiplicands in 404 the term, sorted into the order specified by Term.compare. Works 405 over both :num and :int. Negations are also lifted out, so that only 406 the numeral is negated. 407 408 If the term is a multiplication of numerals, will reduce to just 409 one numeral. If the term includes no numerals, no extra 'n' will 410 be introduced but the multiplicands will be sorted. 411 412 Fails if the term is not a multiplication. 413 414 ---------------------------------------------------------------------- *) 415 416fun NORMALISE_MULT0 t = let 417 open arithmeticTheory 418 (* t is a multiplication term, over either :num or :int *) 419 val (dest, strip, mk, listmk, AC, is_lit, MULT_LID, one_tm) = 420 if numSyntax.is_mult t then 421 (numSyntax.dest_mult, 422 numSyntax.strip_mult, 423 numSyntax.mk_mult, 424 numSyntax.list_mk_mult, 425 EQT_ELIM o AC_CONV (MULT_ASSOC, MULT_COMM), 426 numSyntax.is_numeral, 427 GSYM arithmeticTheory.MULT_LEFT_1, 428 numSyntax.term_of_int 1) 429 else if intSyntax.is_mult t then 430 (intSyntax.dest_mult, 431 intSyntax.strip_mult, 432 intSyntax.mk_mult, 433 intSyntax.list_mk_mult, 434 EQT_ELIM o AC_CONV (INT_MUL_ASSOC, INT_MUL_COMM), 435 intSyntax.is_int_literal, 436 GSYM INT_MUL_LID, 437 intSyntax.one_tm) 438 else raise ERR "NORMALISE_MULT" "Term not a multiplication" 439 val ms = strip t 440 val (nums, others) = partition is_lit ms 441 fun sort nums others t = let 442 val newt = mk(listmk nums, listmk (Listsort.sort Term.compare others)) 443 in 444 K (AC(mk_eq(t,newt))) THENC LAND_CONV REDUCE_CONV 445 end t 446in 447 if null others then REDUCE_CONV 448 else if null nums then 449 REWR_CONV MULT_LID THENC sort [one_tm] others 450 else 451 sort nums others 452end t 453 454val NORMALISE_MULT = 455 NORMALISE_MULT0 THENC REWRITE_CONV [GSYM INT_NEG_RMUL, GSYM INT_NEG_LMUL, 456 INT_NEGNEG] THENC 457 REWRITE_CONV [INT_NEG_LMUL] THENC 458 TRY_CONV (FIRST_CONV (map REWR_CONV [arithmeticTheory.MULT_LEFT_1, 459 INT_MUL_LID])) 460 461 462(* ---------------------------------------------------------------------- 463 leaf_normalise t 464 465 Takes a "leaf term" (a relational operator over integer values) and 466 normalises it to either an equality, a <= or a disjunction of two 467 (un-normalised) <= leaves. (The latter happens if called onto 468 normalise ~(x = y)). 469 ---------------------------------------------------------------------- *) 470 471fun EVERY_SUMMAND c tm = 472 if is_plus tm then BINOP_CONV (EVERY_SUMMAND c) tm 473 else c tm 474 475local 476 val lt_elim = SPEC_ALL int_arithTheory.less_to_leq_samer 477 val tac = REWRITE_TAC [GSYM int_le, INT_NOT_LE, lt_elim, int_gt, 478 INT_LE_RADD, int_ge, GSYM INT_LE_ANTISYM, 479 DE_MORGAN_THM] 480 val not_le = prove(``~(x <= y) = (y + 1i <= x)``, tac) 481 val not_lt = prove(``~(x:int < y) = y <= x``, tac) 482 val not_gt = prove(``~(x:int > y) = x <= y``, tac) 483 val not_ge = prove(``~(x >= y) = x + 1i <= y``, tac) 484 val not_eq = prove(``~(x = y:int) = y + 1 <= x \/ x + 1 <= y``, tac) 485 val ge_elim = prove(``x:int >= y = y <= x``, tac) 486 val gt_elim = prove(``x > y = y + 1i <= x``, tac) 487 val eq_elim = prove(``(x:int = y) = (x <= y /\ y <= x)``, tac) 488 val mult1 = GSYM INT_MUL_LID 489in 490 491fun MULT1_CONV tm = if not (is_mult tm) andalso not (is_int_literal tm) then 492 REWR_CONV mult1 tm 493 else ALL_CONV tm 494 495val sum_normalise = 496 REWRITE_CONV [INT_NEG_ADD, INT_LDISTRIB, INT_RDISTRIB, 497 INT_NEG_LMUL, INT_NEGNEG, INT_NEG_0, 498 int_sub] THENC 499 EVERY_SUMMAND (TRY_CONV NORMALISE_MULT THENC MULT1_CONV) THENC 500 REWRITE_CONV [GSYM INT_NEG_RMUL, GSYM INT_NEG_LMUL, 501 INT_NEGNEG] THENC 502 REWRITE_CONV [INT_NEG_LMUL] THENC 503 SORT_AND_GATHER_CONV 504 505val norm_divides = 506 LAND_CONV CooperMath.REDUCE_CONV THENC 507 RAND_CONV sum_normalise THENC 508 REWRITE_CONV [INT_DIVIDES_NEG] THENC 509 CooperMath.minimise_divides THENC 510 CooperMath.check_divides 511 512fun normalise_numbers tm = let 513 val MK_LEQ = 514 TRY_CONV (FIRST_CONV (map REWR_CONV [lt_elim, not_le, not_lt, not_gt, 515 not_ge, ge_elim, gt_elim])) THENC 516 (REWR_CONV int_arithTheory.le_move_all_right ORELSEC 517 REWR_CONV int_arithTheory.eq_move_all_right) 518 val base_normaliser = RAND_CONV sum_normalise THENC gcd_check 519in 520 if (is_leq tm orelse is_eq tm) andalso lhand tm = zero_tm then 521 if is_plus (rand tm) then let 522 val (rl, rr) = dest_plus (rand tm) 523 fun mult_ok acc tm = let 524 val (c,v) = dest_mult tm 525 in 526 is_int_literal c andalso is_var v andalso 527 (case acc of 528 NONE => true 529 | SOME v0 => Term.compare(v0, v) = GREATER) 530 end handle HOL_ERR _ => false 531 fun rhs_ok acc tm = let 532 val (l,r) = dest_plus tm 533 in 534 mult_ok acc r andalso rhs_ok (SOME (rand r)) l 535 end handle HOL_ERR _ => mult_ok acc tm 536 in 537 if is_int_literal rr andalso rhs_ok NONE rl then 538 if is_eq tm andalso is_negated (lhand (hd (strip_plus rl))) then 539 REWR_CONV (GSYM INT_EQ_NEG) THENC 540 LAND_CONV (REWR_CONV INT_NEG_0) THENC base_normaliser 541 else NO_CONV 542 else base_normaliser 543 end 544 else if is_int_literal (rand tm) then CooperMath.REDUCE_CONV 545 else base_normaliser 546 else if is_divides tm then 547 CHANGED_CONV norm_divides 548 else if is_neg tm andalso is_divides (rand tm) then 549 CHANGED_CONV (RAND_CONV norm_divides) 550 else MK_LEQ THENC base_normaliser 551end tm 552 553val leaf_normalise = 554 (REWR_CONV not_eq THENC BINOP_CONV normalise_numbers) ORELSEC 555 normalise_numbers 556end (* local *) 557 558 559(* ---------------------------------------------------------------------- 560 PRENEX_CONV t 561 562 a prenexer which differs from Canon.PRENEX_CONV only in that it pulls 563 quantifiers out of the then or else branches of conditional 564 expressions. 565 ---------------------------------------------------------------------- *) 566 567val tac = COND_CASES_TAC THEN REWRITE_TAC [] 568val COND_FA_THEN_THM = 569 prove(``(if p then !x:'a. P x else q) = !x. if p then P x else q``, tac) 570val COND_FA_ELSE_THM = 571 prove(``(if p then q else !x:'a. P x) = !x. if p then q else P x``, tac) 572val COND_EX_THEN_THM = 573 prove(``(if p then ?x:'a. P x else q) = ?x. if p then P x else q``, tac) 574val COND_EX_ELSE_THM = 575 prove(``(if p then q else ?x:'a. P x) = ?x. if p then q else P x``, tac) 576 577fun COND_FA_THEN tm = let 578 val (g, t, e) = dest_cond tm 579 val (v, _) = dest_forall t 580in 581 HO_REWR_CONV COND_FA_THEN_THM THENC RAND_CONV (ALPHA_CONV v) 582end tm 583fun COND_FA_ELSE tm = let 584 val (g, t, e) = dest_cond tm 585 val (v, _) = dest_forall e 586in 587 HO_REWR_CONV COND_FA_ELSE_THM THENC RAND_CONV (ALPHA_CONV v) 588end tm 589fun COND_EX_THEN tm = let 590 val (g, t, e) = dest_cond tm 591 val (v, _) = dest_exists t 592in 593 HO_REWR_CONV COND_EX_THEN_THM THENC RAND_CONV (ALPHA_CONV v) 594end tm 595fun COND_EX_ELSE tm = let 596 val (g, t, e) = dest_cond tm 597 val (v, _) = dest_exists e 598in 599 HO_REWR_CONV COND_EX_ELSE_THM THENC RAND_CONV (ALPHA_CONV v) 600end tm 601 602val PRENEX_CONV = 603 TOP_DEPTH_CONV 604 (FIRST_CONV [NOT_FORALL_CONV, NOT_EXISTS_CONV, 605 AND_FORALL_CONV, OR_EXISTS_CONV, 606 RIGHT_AND_FORALL_CONV, LEFT_AND_FORALL_CONV, 607 RIGHT_AND_EXISTS_CONV, LEFT_AND_EXISTS_CONV, 608 RIGHT_IMP_FORALL_CONV, LEFT_IMP_FORALL_CONV, 609 RIGHT_IMP_EXISTS_CONV, LEFT_IMP_EXISTS_CONV, 610 RIGHT_OR_FORALL_CONV, LEFT_OR_FORALL_CONV, 611 RIGHT_OR_EXISTS_CONV, LEFT_OR_EXISTS_CONV, 612 COND_FA_THEN, COND_FA_ELSE, COND_EX_THEN, COND_EX_ELSE]) 613 614(* generate_nway_casesplit n: generates the theorem 615 P v1 .. vn = P F F .. F F \/ P F F .. F T \/ P F F .. T F \/ 616 P F F .. T T \/ ... \/ P T T .. F F \/ 617 P T T .. F T \/ P T T .. T F \/ P T T .. T T 618 that is, the 2^n possibilities for n boolean variables. 619 Performance is exponential, so beware *) 620 621fun generate_nway_casesplit n = let 622 val _ = n >= 1 orelse raise Fail "generate_nway_casesplit: n < 1" 623 fun genty n = if n = 1 then bool --> bool 624 else bool --> (genty (n - 1)) 625 val P_ty = genty n 626 val P_t = mk_var("P", P_ty) 627 fun gen_cases (m, vs, t) = 628 if m < n then let 629 val v = mk_var("v"^Int.toString m, bool) 630 val vT = (m + 1, v::vs, mk_comb(t, T)) 631 val vF = (m + 1, (mk_neg v)::vs, mk_comb(t, F)) 632 in 633 mk_disj(gen_cases vT, gen_cases vF) 634 end 635 else 636 mk_conj(t, list_mk_conj vs) 637 val RHS = gen_cases (0, [], P_t) 638 fun gen_vars n acc = 639 if n < 0 then acc 640 else gen_vars (n - 1) (mk_var("v"^Int.toString n, bool)::acc) 641 val vars = gen_vars (n - 1) [] 642in 643 GEN P_t (GENL vars 644 (prove(mk_eq(list_mk_comb(P_t, vars), RHS), 645 MAP_EVERY BOOL_CASES_TAC vars THEN REWRITE_TAC []))) 646end 647 648fun UNBETA_LIST tlist = 649 case tlist of 650 [] => ALL_CONV 651 | (t::ts) => UNBETA_CONV t THENC RATOR_CONV (UNBETA_LIST ts) 652 653 654 655(* ---------------------------------------------------------------------- 656 reveal_a_disj t 657 658 if t is "morally" a disjunction, map it clear that this is the case 659 by rewriting appropriately. 660 ---------------------------------------------------------------------- *) 661 662val not_beq = prove( 663 ``~(b1 = b2) = b1 /\ ~b2 \/ ~b1 /\ b2``, 664 BOOL_CASES_TAC ``b1:bool`` THEN REWRITE_TAC []); 665val beq = prove( 666 ``(b1 = b2) = b1 /\ b2 \/ ~b1 /\ ~b2``, 667 BOOL_CASES_TAC ``b1:bool`` THEN REWRITE_TAC []); 668 669fun reveal_a_disj tm = 670 if is_disj tm then ALL_CONV tm 671 else 672 (FIRST_CONV (map REWR_CONV [beq, not_beq, IMP_DISJ_THM, 673 CooperThms.NOT_AND]) ORELSEC 674 (REWR_CONV CooperThms.NOT_NOT_P THENC reveal_a_disj)) tm 675 676 677(* ---------------------------------------------------------------------- 678 normalise_guard t 679 680 t is a conditional expression with a single leaf term as its guard. 681 If this is a <= leaf, flip its sense (and the corresponding then and 682 else branches) so that the coefficient of the first variable is 683 positive 684 ---------------------------------------------------------------------- *) 685 686val FLIP_COND = prove( 687 ``(if g then t:'a else e) = if ~g then e else t``, 688 COND_CASES_TAC THEN REWRITE_TAC []); 689 690fun normalise_guard t = let 691 val _ = dest_cond t 692 fun make_guard_positive t = let 693 val (g, _, _) = dest_cond t 694 in 695 if is_leq g then let 696 val t1 = hd (strip_plus (rand g)) 697 in 698 if is_negated (#1 (dest_mult t1)) handle HOL_ERR _ => false then 699 REWR_CONV FLIP_COND THENC 700 RATOR_CONV (LAND_CONV leaf_normalise) 701 else 702 ALL_CONV 703 end 704 else 705 ALL_CONV 706 end t 707in 708 RATOR_CONV (LAND_CONV leaf_normalise) THENC make_guard_positive 709end t 710 711fun TOP_SWEEP_ONCE_CONV c t = 712 (TRY_CONV c THENC SUB_CONV (TOP_SWEEP_ONCE_CONV c)) t 713 714val normalise_guards = TOP_SWEEP_ONCE_CONV normalise_guard 715 716(* ---------------------------------------------------------------------- 717 cond_removal0 t 718 719 If t contains conditional expressions where guards of these appear 720 more than once, then do a case-split on these guard expressions at 721 the top level. 722 E.g., 723 (if g then t else e) /\ (if g then t' else e') 724 will turn into 725 g /\ t /\ t' \/ g /\ e /\ e' 726 727 ---------------------------------------------------------------------- *) 728 729fun cond_removal0 t = let 730 open Binarymap 731 val condexps = List.map (hd o #2 o strip_comb) (find_terms is_cond t) 732 val empty_map = mkDict Term.compare 733 fun my_insert(g, m) = 734 case peek(m,g) of 735 NONE => insert(m, g, 1) 736 | SOME n => insert(m, g, n + 1) 737 val final_map = List.foldl my_insert empty_map condexps 738 fun find_gt2 (t,n,l) = if n >= 2 then t::l else l 739 val gt2_guards = foldl find_gt2 [] final_map 740 val n = assert (curry op < 0) (length gt2_guards) 741 val case_split = generate_nway_casesplit n 742in 743 UNBETA_LIST (List.rev gt2_guards) THENC 744 REWR_CONV case_split THENC 745 EVERY_DISJ_CONV (LAND_CONV LIST_BETA_CONV THENC REWRITE_CONV []) 746end t 747 748(* ---------------------------------------------------------------------- 749 cond_removal t 750 751 Perform cond_removal0 on all of t's disjunctions, not being put off 752 by disjunctions hiding as negated conjunctions. 753 ---------------------------------------------------------------------- *) 754 755fun cond_removal t = 756 ((reveal_a_disj THENC BINOP_CONV cond_removal) ORELSEC 757 (normalise_guards THENC cond_removal0)) t 758 759 760(* ---------------------------------------------------------------------- 761 calculate_range_disjunct tm 762 763 tm is of form ?i. (0 <= i /\ i <= u) /\ ... 764 transform this into an appropriate number of disjuncts (or possibly 765 false, if u < 0), of the form 766 P(0) \/ P(1) \/ ... \/ P(u) 767 ---------------------------------------------------------------------- *) 768 769val refl_case = prove( 770 ``!u P. (?i:int. (u <= i /\ i <= u) /\ P i) = P u``, 771 REWRITE_TAC [INT_LE_ANTISYM] THEN REPEAT GEN_TAC THEN EQ_TAC THEN 772 STRIP_TAC THEN ASM_REWRITE_TAC [] THEN Q.EXISTS_TAC `u` THEN 773 ASM_REWRITE_TAC []); 774val nonrefl_case = prove( 775 ``!lo hi P. (?i:int. (lo <= i /\ i <= hi) /\ P i) = 776 lo <= hi /\ (P lo \/ ?i. (lo + 1 <= i /\ i <= hi) /\ P i)``, 777 REPEAT STRIP_TAC THEN EQ_TAC THEN STRIP_TAC THENL [ 778 Q.ASM_CASES_TAC `i = lo` THENL [ 779 POP_ASSUM SUBST_ALL_TAC THEN ASM_REWRITE_TAC [], 780 REWRITE_TAC [LEFT_AND_OVER_OR] THEN 781 DISJ2_TAC THEN CONJ_TAC THENL [ 782 IMP_RES_TAC INT_LE_TRANS, 783 ALL_TAC 784 ] THEN Q.EXISTS_TAC `i` THEN ASM_REWRITE_TAC [] THEN 785 REWRITE_TAC [GSYM int_arithTheory.less_to_leq_samer] THEN 786 RULE_ASSUM_TAC (REWRITE_RULE [INT_LE_LT]) THEN 787 POP_ASSUM_LIST (MAP_EVERY STRIP_ASSUME_TAC) THEN 788 POP_ASSUM SUBST_ALL_TAC THEN 789 FIRST_X_ASSUM (fn th => MP_TAC th THEN REWRITE_TAC [] THEN NO_TAC) 790 ], 791 Q.EXISTS_TAC `lo` THEN ASM_REWRITE_TAC [INT_LE_REFL], 792 Q.EXISTS_TAC `i` THEN ASM_REWRITE_TAC [] THEN 793 MATCH_MP_TAC INT_LE_TRANS THEN Q.EXISTS_TAC `lo + 1` THEN 794 ASM_REWRITE_TAC [INT_LE_ADDR] THEN CONV_TAC CooperMath.REDUCE_CONV 795 ]); 796 797 798fun calculate_range_disjunct tm = let 799 val (i, body) = dest_exists tm 800 fun recurse tm = 801 ((REWR_CONV refl_case THENC BETA_CONV) ORELSEC 802 (REWR_CONV nonrefl_case THENC 803 LAND_CONV CooperMath.REDUCE_CONV THENC 804 (REWR_CONV CooperThms.F_and_l ORELSEC 805 (REWR_CONV CooperThms.T_and_l THENC 806 FORK_CONV(BETA_CONV, 807 BINDER_CONV (LAND_CONV 808 (LAND_CONV CooperMath.REDUCE_CONV)) THENC 809 recurse))))) tm 810in 811 BINDER_CONV (RAND_CONV (UNBETA_CONV i)) THENC recurse 812end tm 813 814(* ---------------------------------------------------------------------- 815 rel_coeff v tm 816 817 returns the coefficient (a term that is a numeral) of variable v in 818 relational term tm. A relational term is of the form 819 0 <relop> r1 + ... + rn + n 820 where all of the ri are numerals multiplied by variables, and the n 821 is a bare numerals. Further, it is assumed that any given variable 822 occurs once. Returns zero as the coefficient of a variable not 823 present. 824 ---------------------------------------------------------------------- *) 825 826fun rel_coeff v tm = let 827 fun recurse t = let 828 val (l,r) = dest_plus t 829 in 830 if rand r = v then lhand r 831 else recurse l 832 end handle HOL_ERR _ => if rand t = v then lhand t else zero_tm 833in 834 recurse (lhand (rand tm)) 835end 836 837 838(* ---------------------------------------------------------------------- 839 find_eliminable_equality vset acc conjunctions 840 841 finds an equality that can be eliminated from the conjunctions. This 842 has to be done wrt a set of variables that have scope over the 843 conjunctions. Returns a new version of acc, the fields of which are 844 (leastv, conj, rest) 845 of types 846 ((term * Arbint) option * term option * term list) 847 848 leastv is the variable that has the least coefficient coupled with 849 that least coefficient. NONE if there is none such. 850 851 conj is the conjunct in which leastv was found to be least. Again, 852 NONE if there is nothing eliminable. 853 854 rest is the list of all the unsatisfactory conjuncts. 855 856 ---------------------------------------------------------------------- *) 857 858fun find_eliminable_equality vs (acc as (leastv, conj, rest)) cs = let 859 fun ocons NONE xs = xs | ocons (SOME x) xs = x::xs 860 fun doclause (acc as (leastv, conj, rest)) unexamined c k = let 861 val fvs = FVL [lhand (rand c)] empty_tmset 862 val i = HOLset.intersection(vs,fvs) 863 fun check_mins (v, (leastv, changed)) = let 864 open Arbint 865 val v_coeff = abs (int_of_term (rel_coeff v c)) 866 in 867 case leastv of 868 NONE => (SOME(v,v_coeff), true) 869 | SOME(v', min) => if v_coeff < min then (SOME (v,v_coeff), true) 870 else (leastv, changed) 871 end 872 (* if this clause isn't interesting, we need to continue (by calling k) 873 but we also need to put c onto the list of things seen so far; here's 874 the "unchanged" accumulated state that we'll pass to k in these 875 cases *) 876 val unchanged_acc = (leastv, conj, c::rest) 877 in 878 case HOLset.numItems i of 879 0 => k unchanged_acc 880 | 1 => let 881 val v = hd (HOLset.listItems i) 882 in 883 if Arbint.abs (int_of_term (rel_coeff v c)) = Arbint.one then 884 (SOME (v,Arbint.one), SOME c, ocons conj rest @ unexamined) 885 else k unchanged_acc 886 end 887 | sz => let 888 in 889 case HOLset.foldl check_mins (leastv, false) i of 890 (least', true) => k (least', SOME c, ocons conj rest) 891 | (_, false) => k unchanged_acc 892 end 893 end 894in 895 case cs of 896 [] => acc 897 | (c::cs) => if not (is_eq c) then 898 find_eliminable_equality vs (leastv,conj,c::rest) cs 899 else 900 doclause acc cs c 901 (fn acc' => find_eliminable_equality vs acc' cs) 902end 903 904(* ---------------------------------------------------------------------- 905 sum_to_sumc tm 906 907 takes tm (a sum of the form t1 + .. + tn) and returns a theorem of 908 the form 909 |- tm = sumc cs vs 910 where cs is a list of numeral coefficients, and vs a list of 911 variables (except that one of the vs will actually be the numeral 1). 912 ---------------------------------------------------------------------- *) 913 914val sumc_t = ``Omega$sumc`` 915fun sum_to_sumc tm = let 916 fun dest_m t = dest_mult t handle HOL_ERR _ => (t, one_tm) 917 val (cs, vs) = ListPair.unzip (map dest_m (strip_plus tm)) 918 fun mk_list l = listSyntax.mk_list(l, int_ty) 919 val (cs_t, vs_t) = (mk_list ## mk_list) (cs, vs) 920 val sumc_t = list_mk_comb(sumc_t, [cs_t, vs_t]) 921in 922 SYM ((REWRITE_CONV [INT_ADD_ASSOC, OmegaTheory.sumc_def, INT_MUL_RID] THENC 923 REWR_CONV INT_ADD_RID) sumc_t) 924end 925 926(* ---------------------------------------------------------------------- 927 sumc_eliminate reducer tm 928 929 Takes a term of the form 930 sumc (MAP f cs) vs 931 and turns it into a regular sum, assuming that the last v will actually 932 be the integer 1, using the reducer parameter to evaluate each 933 instance of the application of f to c. 934 ---------------------------------------------------------------------- *) 935 936fun sumc_eliminate reducer tm = let 937 open OmegaTheory 938 fun recurse tm = 939 if listSyntax.is_nil (rand (rand tm)) then 940 (REWR_CONV sumc_singleton THENC reducer) tm 941 else 942 (REWR_CONV sumc_nonsingle THENC LAND_CONV (LAND_CONV reducer) THENC 943 RAND_CONV recurse) tm 944in 945 if listSyntax.is_nil (rand tm) then 946 REWRITE_CONV [listTheory.MAP, OmegaTheory.sumc_def] 947 else 948 recurse 949end tm 950 951 952(* ---------------------------------------------------------------------- 953 eliminate_equality v tm 954 955 Takes a variable v, and an equality tm, of the general form 956 0 = r1 + .. + rn 957 and returns a theorem which is an equation of the general form 958 959 |- tm = ?s. (v = ....) /\ tm 960 961 ---------------------------------------------------------------------- *) 962 963val SYM_EQ_NEG = GSYM INT_EQ_NEG 964fun eliminate_equality v tm = let 965 open OmegaTheory 966 val instantiate_eqremoval = 967 C MP TRUTH o CONV_RULE (LAND_CONV REDUCE_CONV) o 968 PART_MATCH (lhand o rand) equality_removal 969 val rhs_th = MOVE_VCOEFF_TO_FRONT v (rand tm) 970 val cv_t = lhand (rand (concl rhs_th)) 971 val dealwith_negative_coefficient = 972 if is_negated (lhand cv_t) then 973 REWR_CONV SYM_EQ_NEG THENC 974 FORK_CONV (REWR_CONV INT_NEG_0, NEG_SUM_CONV) 975 else ALL_CONV 976in 977 RAND_CONV (K rhs_th) THENC dealwith_negative_coefficient THENC 978 RAND_CONV (RAND_CONV sum_to_sumc) THENC instantiate_eqremoval THENC 979 BINDER_CONV 980 (LAND_CONV (* new equality conjunct *) 981 (RAND_CONV (* rhs of equality *) 982 (LAND_CONV (LAND_CONV REDUCE_CONV) THENC 983 RAND_CONV (* sumc term *) 984 (LAND_CONV (LAND_CONV (* first arg of MAP *) 985 (BINDER_CONV (RAND_CONV REDUCE_CONV THENC 986 REWRITE_CONV [modhat_def] THENC 987 REDUCE_CONV))) THENC 988 sumc_eliminate (BETA_CONV THENC REDUCE_CONV)) THENC 989 REWRITE_CONV [INT_MUL_LZERO, INT_ADD_RID, INT_ADD_ASSOC, 990 INT_ADD_LID])) THENC 991 RAND_CONV (* old equality conjunct *) 992 (REWRITE_CONV [sumc_def] THENC 993 REWRITE_CONV [INT_MUL_RID, INT_ADD_ASSOC] THENC 994 RAND_CONV (REWR_CONV INT_ADD_RID))) 995end tm 996 997val eliminate_equality = 998 fn x => (*Profile.profile "eliminate_eq"*) (eliminate_equality x) 999 1000 1001 1002 1003(* ---------------------------------------------------------------------- 1004 OmegaEq : term -> thm 1005 1006 Put all of the above together 1007 ---------------------------------------------------------------------- *) 1008 1009fun push_exvar_to_bot v tm = let 1010 val (bv, body) = dest_exists tm 1011in 1012 if bv = v then (SWAP_VARS_CONV THENC 1013 BINDER_CONV (push_exvar_to_bot v) ORELSEC 1014 ALL_CONV) 1015 else (BINDER_CONV (push_exvar_to_bot v)) 1016end tm 1017 1018val EX_REFL = EQT_INTRO (SPEC_ALL EXISTS_REFL) 1019fun OmegaEq t = let 1020 val (exvars, body) = strip_exists t 1021 val exv_set = HOLset.addList(empty_tmset, exvars) 1022 val gcd_check = (*Profile.profile "gcd_check"*) gcd_check 1023 val _ = length exvars > 0 orelse 1024 raise ERR "OmegaEq" "Term not existentially quantified" 1025 val conjns = strip_conj body 1026 val (vwithleast, conj, rest) = 1027 find_eliminable_equality exv_set (NONE, NONE, []) conjns 1028 val _ = isSome vwithleast orelse raise UNCHANGED 1029 val (to_elim, elimc) = valOf vwithleast 1030 val c = valOf conj 1031 val newrhs = if null rest then c else mk_conj(c, list_mk_conj rest) 1032 val reordered_thm = 1033 EQT_ELIM (AC_CONV(CONJ_ASSOC, CONJ_COMM) (mk_eq(body, newrhs))) 1034 val bring_veq_to_top = let 1035 val (rCONV, finisher) = if null rest then (I, ALL_CONV) 1036 else (LAND_CONV, 1037 LEFT_AND_EXISTS_CONV THENC 1038 BINDER_CONV (REWR_CONV (GSYM CONJ_ASSOC))) 1039 in 1040 if elimc = Arbint.one then 1041 rCONV (phase2_CONV to_elim THENC LAND_CONV (REWR_CONV INT_MUL_LID)) 1042 else 1043 rCONV (eliminate_equality to_elim) THENC finisher 1044 end 1045 fun ifVarsRemain c t = if is_exists t then c t else ALL_CONV t 1046 val (absify, unwinder) = 1047 if null rest andalso elimc = Arbint.one then 1048 (ALL_CONV, REWR_CONV EX_REFL) 1049 else (STRIP_QUANT_CONV (RAND_CONV (UNBETA_CONV to_elim)), 1050 REWR_CONV UNWIND_THM2 THENC BETA_CONV) 1051in 1052 STRIP_QUANT_CONV (K reordered_thm THENC bring_veq_to_top THENC absify) THENC 1053 push_exvar_to_bot to_elim THENC LAST_EXISTS_CONV unwinder THENC 1054 STRIP_QUANT_CONV 1055 (BLEAF_CONV (op THENC) 1056 (TRY_CONV (RAND_CONV S_AND_G_MULT THENC 1057 TRY_CONV gcd_check))) THENC 1058 REWRITE_CONV [EXISTS_SIMP] THENC 1059 ifVarsRemain OmegaEq 1060end t 1061 1062(* some test terms: 1063 1064time OmegaEq ``?x y z. 0 <= 2 * x + ~3 * y + 5 * z + 10 /\ 1065 (0 = 3 * x + 4 * y + ~7 * z + 3)``; 1066 1067time OmegaEq ``?i j. 0 <= 1 * i + 0 /\ 0 <= 1 * j + 0 /\ 1068 (0 = 3 * i + 5 * j + ~1 * n + 0)``; 1069 1070time OmegaEq ``?i j. (0 = 3 * i + 5 * j + ~1 * n + 0)``; 1071 1072time OmegaEq ``?i j. (0 = 3 * i + 6 * j + ~1 * n + 0)``; 1073 1074time OmegaEq ``?x y. (0 = 2 * x + 3 * y + 2) /\ (0 = 2 * x + 3 * y + 4)``; 1075 1076time OmegaEq ``?n. (0 = 1 * n + 1) /\ 0 <= 1 * n + 0``; 1077 1078*) 1079 1080 1081(* ---------------------------------------------------------------------- 1082 eliminate_positive_divides t 1083 1084 t is a term of the form ?x1 .. xn. body, where body is a conjunction 1085 of leaves, possibly including divisibility relations (negated or 1086 positive). This function writes away those (positive) divisibility 1087 relations of the form d | exp where exp includes at least one 1088 variable from x1 .. xn. 1089 ---------------------------------------------------------------------- *) 1090 1091fun eliminate_positive_divides t = let 1092 val (vs, body) = strip_exists t 1093 fun find_divides tm = let 1094 in 1095 if is_conj tm then 1096 (LAND_CONV find_divides THENC LEFT_AND_EXISTS_CONV) ORELSEC 1097 (RAND_CONV find_divides THENC RIGHT_AND_EXISTS_CONV) 1098 else if is_divides tm andalso 1099 not (null (intersect vs (free_vars (rand tm)))) 1100 then 1101 REWR_CONV INT_DIVIDES THENC 1102 BINDER_CONV leaf_normalise 1103 else 1104 NO_CONV 1105 end tm 1106in 1107 STRIP_QUANT_CONV find_divides THENC OmegaEq THENC 1108 REWRITE_CONV [] THENC 1109 TRY_CONV eliminate_positive_divides 1110end t 1111 1112(* ---------------------------------------------------------------------- 1113 eliminate_negative_divides t 1114 1115 t is a term of the form ?x1 .. xn. body, where body is a conjunction 1116 of leaves, possibly including divisibility relations (negated or 1117 positive). This function writes away those negated divisibility 1118 relations of the form ~(d | exp) where exp includes at least one 1119 variable from x1 .. xn. It introduces case splits. 1120 ---------------------------------------------------------------------- *) 1121 1122fun eliminate_negative_divides t = let 1123 val (vs, _) = strip_exists t 1124 fun elim_ndivides tm = let 1125 val (c, d) = dest_divides (rand tm) 1126 val c_neq_0 = EQT_ELIM (CooperMath.REDUCE_CONV 1127 (mk_neg(mk_eq(rand c, numSyntax.zero_tm)))) 1128 in 1129 MP (SPECL [rand c, d] int_arithTheory.NOT_INT_DIVIDES_POS) c_neq_0 1130 end 1131 fun rdistrib tm = 1132 TRY_CONV (REWR_CONV RIGHT_AND_OVER_OR THENC RAND_CONV rdistrib) tm 1133 fun ldistrib tm = 1134 TRY_CONV (REWR_CONV LEFT_AND_OVER_OR THENC RAND_CONV ldistrib) tm 1135 fun find_divides tm = let 1136 in 1137 if is_conj tm then 1138 (LAND_CONV find_divides THENC rdistrib) ORELSEC 1139 (RAND_CONV find_divides THENC ldistrib) 1140 else if is_neg tm andalso 1141 not (null (intersect vs (free_vars (rand (rand tm))))) 1142 then 1143 elim_ndivides THENC 1144 BINDER_CONV (LAND_CONV (RAND_CONV (CooperMath.REDUCE_CONV))) THENC 1145 calculate_range_disjunct THENC 1146 EVERY_DISJ_CONV (RAND_CONV SORT_AND_GATHER1_CONV) 1147 else NO_CONV 1148 end tm 1149 fun push tm = let 1150 val (vs, body) = strip_exists tm 1151 in 1152 CooperSyntax.push_in_exists THENC 1153 EVERY_DISJ_CONV (RENAME_VARS_CONV (map (#1 o dest_var) vs)) 1154 end tm 1155in 1156 STRIP_QUANT_CONV find_divides THENC push THENC 1157 TRY_CONV eliminate_negative_divides 1158end t 1159 1160val _ = Parse.temp_set_grammars ctxt_grammars 1161 1162end (* struct *) 1163