1structure CooperMath :> CooperMath = struct 2 3 local open gcdTheory in end 4 5 open HolKernel boolLib intSyntax integerTheory 6 int_arithTheory intReduce CooperThms CooperSyntax 7 8 type num = Arbnum.num 9 10 val cooper_compset = int_compset() 11 val _ = computeLib.add_thms [gcdTheory.GCD_EFFICIENTLY] cooper_compset 12 val REDUCE_CONV = computeLib.CBV_CONV cooper_compset 13 14val ERR = mk_HOL_ERR "CooperMath"; 15 16fun lhand t = rand (rator t) 17 18(* Fix the grammar used by this file *) 19structure Parse = struct 20 open Parse 21 val (Type,Term) = parse_from_grammars integer_grammars 22end 23open Parse 24 25(*---------------------------------------------------------------------------*) 26(* Function to compute the Greatest Common Divisor of two integers. *) 27(*---------------------------------------------------------------------------*) 28 29local open Arbint in 30fun gcd' i j = let 31 val r = i mod j 32in if r = zero then j else gcd' j r 33end 34 35fun gcd (i,j) = 36 if i < zero orelse j < zero then raise ERR "gcd""negative arguments to gcd" 37 else if i = zero then j else if j = zero then i 38 else if i < j then gcd' j i else gcd' i j 39end (* local *) 40 41fun gcdl l = 42 case l of 43 [] => raise ERR "gcdl" "empty list" 44 | (h::t) => foldl gcd h t 45 46(*---------------------------------------------------------------------------*) 47(* Function to compute the Lowest Common Multiple of two integers. *) 48(*---------------------------------------------------------------------------*) 49 50fun lcm (i,j) = let open Arbint in (i * j) div (gcd (i,j)) end 51handle _ => raise ERR "lcm" "negative arguments to lcm"; 52 53fun lcml ints = 54 case ints of 55 [] => raise ERR "lcml" "empty list" 56 | [x] => x 57 | (x::y::xs) => lcml (lcm (x, y)::xs) 58 59 60 fun extended_gcd(a, b) = let 61 open Arbnum 62 in 63 if b = zero then (a,(Arbint.one,Arbint.zero)) 64 else let 65 val (q,r) = divmod (a,b) 66 val (d,(x,y)) = extended_gcd(b,r) 67 open Arbint 68 in 69 (d,(y,x - fromNat q * y)) 70 end 71 end 72 73 val gcd_t = prim_mk_const {Thy = "gcd", Name = "gcd"} 74 75fun sum_var_coeffs var tm = let 76 open Arbint 77in 78 if is_plus tm then 79 sum_var_coeffs var (rand (rator tm)) + sum_var_coeffs var (rand tm) 80 else if is_mult tm then let 81 val (l,r) = (rand (rator tm), rand tm) 82 in 83 if r = var then int_of_term l else zero 84 end else zero 85end 86 87datatype dir = Left | Right 88datatype termtype = EQ | LT 89 90fun dir_of_pair Left (l,r) = l 91 | dir_of_pair Right (l,r) = r 92fun term_at Left tm = rand (rator tm) 93 | term_at Right tm = rand tm 94 95fun conv_at Left = LAND_CONV 96 | conv_at Right = RAND_CONV 97 98(* moves summands from one side or the other of a less-than or an 99 equality term *) 100local 101 val myrewrite_conv = REWRITE_CONV [INT_NEG_ADD, INT_NEGNEG, INT_NEG_LMUL] 102in 103 fun move_terms_from ttype dir P tm = let 104 val arg = term_at dir tm 105 val arg_summands = strip_plus arg 106 in 107 case partition P arg_summands of 108 ([], to_stay) => REFL tm (* none to move *) 109 | (to_move, []) => let 110 (* all must move *) 111 val move_conv = 112 case (dir,ttype) of 113 (Left, LT) => REWR_CONV lt_move_all_right 114 | (Right, LT) => REWR_CONV lt_move_all_left 115 | (Left, EQ) => REWR_CONV eq_move_all_right 116 | (Right, EQ) => REWR_CONV eq_move_all_left 117 in 118 (move_conv THENC myrewrite_conv) tm 119 end 120 | (to_move, to_stay) => let 121 val new_arg = mk_plus(list_mk_plus to_move, list_mk_plus to_stay) 122 val arg_eq_new = EQT_ELIM (AC_CONV (INT_ADD_ASSOC, INT_ADD_COMM) 123 (mk_eq(arg, new_arg))) 124 val move_conv = 125 case (dir,ttype) of 126 (Left, LT) => REWR_CONV lt_move_left_right 127 | (Right, LT) => REWR_CONV lt_move_left_left 128 | (Left, EQ) => REWR_CONV eq_move_left_right 129 | (Right, EQ) => REWR_CONV eq_move_left_left 130 in 131 (conv_at dir (K arg_eq_new) THENC move_conv THENC myrewrite_conv) tm 132 end 133 end 134end 135 136fun collect_terms tm = let 137 (* assuming that tm is of the form c * x + d * x + e * x 138 turns it into (c + d + e) * x 139 *) 140in 141 if is_plus tm then 142 BINOP_CONV collect_terms THENC REWR_CONV (GSYM INT_RDISTRIB) 143 else 144 ALL_CONV 145end tm 146 147fun collect_in_sum var tm = let 148 (* all terms involving var in tm are collected together such that the 149 form of the tm becomes c * var + e *) 150 val summands = strip_plus tm 151in 152 case partition (free_in var) summands of 153 ([], _) => ALL_CONV 154 | (_, []) => collect_terms THENC LAND_CONV REDUCE_CONV 155 | (withvar, without) => let 156 val newterm = mk_plus(list_mk_plus withvar, list_mk_plus without) 157 val tm_eq_newterm = EQT_ELIM (AC_CONV (INT_ADD_ASSOC, INT_ADD_COMM) 158 (mk_eq(tm, newterm))) 159 in 160 K tm_eq_newterm THENC (LAND_CONV (collect_terms THENC 161 LAND_CONV REDUCE_CONV)) 162 end 163end tm 164 165 166 167 fun elim_sdivides tm0 = let 168 (* term of form c | x + d *) 169 val (l,r) = dest_divides tm0 170 val normalise_plus_thm = 171 (if not (is_plus r) then RAND_CONV (REWR_CONV (GSYM INT_ADD_RID)) 172 else REFL) tm0 173 val tm1 = rhs (concl normalise_plus_thm) 174 val normalised_thm = let 175 val (lp,_) = dest_plus (rand tm1) 176 in 177 if not (is_mult lp) then 178 TRANS normalise_plus_thm 179 (RAND_CONV (LAND_CONV (REWR_CONV (GSYM INT_MUL_LID))) tm1) 180 else 181 normalise_plus_thm 182 end 183 val tm = rhs (concl normalised_thm) 184 val r = rand tm 185 val m = l 186 val m_nt = rand l 187 val (a,b) = let 188 val (lp,rp) = dest_plus r 189 in 190 (#1 (dest_mult lp), rp) 191 end 192 (* gcdthm2 of the form 193 m | ax + b = d | b /\ ?t. ... 194 where d is the gcd of m and a *) 195 val a_nt = dest_injected a 196 val m_n = numSyntax.dest_numeral m_nt 197 val a_n = numSyntax.dest_numeral a_nt 198 val (d_n, (x_i, y_i)) = extended_gcd(m_n, a_n) 199 (* x_i * m_n + y_i * a_n = d_n *) 200 val m_nonz = 201 EQT_ELIM (REDUCE_CONV (mk_neg(mk_eq(m_nt,numSyntax.zero_tm)))) 202 val a_nonz = 203 EQT_ELIM (REDUCE_CONV (mk_neg(mk_eq(a_nt,numSyntax.zero_tm)))) 204 val pa_qm = mk_plus(mk_mult(term_of_int y_i, a), 205 mk_mult(term_of_int x_i, m)) 206 val pa_qm_eq_d = REDUCE_CONV pa_qm 207 val rwt = 208 if d_n = Arbnum.one then let 209 val hyp = LIST_CONJ [pa_qm_eq_d, m_nonz, a_nonz] 210 in 211 MATCH_MP gcd21_thm hyp 212 end 213 else let 214 val d_eq_pa_qm = SYM pa_qm_eq_d 215 val gcd_eq_d = REDUCE_CONV (list_mk_comb(gcd_t, [a_nt, m_nt])) 216 val d_eq_gcd = SYM gcd_eq_d 217 val d_nonz = 218 EQT_ELIM (REDUCE_CONV (mk_neg(mk_eq(rhs (concl gcd_eq_d), 219 numSyntax.zero_tm)))) 220 in 221 MATCH_MP gcdthm2 (LIST_CONJ [d_eq_gcd, d_eq_pa_qm, d_nonz, 222 m_nonz, a_nonz]) 223 end 224 val replaced = REWR_CONV rwt THENC REDUCE_CONV THENC 225 ONCE_REWRITE_CONV [INT_MUL_COMM] THENC 226 ONCE_REWRITE_CONV [INT_ADD_COMM] 227 in 228 TRANS normalised_thm (replaced tm) 229 end 230 231 232 val simplify_constraints = let 233 (* applied to term of the form lo < e /\ e <= hi 234 where e is generally of the form c * x [+ b] 235 *) 236 fun elim_coeff tm = let 237 (* term of form d < c * x, d may be negative, c is +ve digit *) 238 val r = rand tm (* i.e., &c * x *) 239 val c = rand (rand (rator r)) 240 val cnonz = EQF_ELIM (REDUCE_CONV (mk_eq(c,numSyntax.zero_tm))) 241 in 242 if is_negated (rand (rator tm)) then (* ~d < c * x *) 243 REWR_CONV (GSYM INT_LT_NEG) THENC (* ~(c * x) < ~~d *) 244 RAND_CONV (REWR_CONV INT_NEGNEG) THENC (* ~(c * x) < d *) 245 LAND_CONV (REWR_CONV INT_NEG_MINUS1 THENC (* ~1 * (c * x) < d *) 246 REWR_CONV INT_MUL_COMM THENC (* (c * x) * ~1 < d *) 247 REWR_CONV (GSYM INT_MUL_ASSOC)) THENC 248 (* c * (x * ~1) < d *) 249 REWR_CONV (MATCH_MP elim_lt_coeffs2 cnonz) THENC 250 (* x * ~1 < if ... *) 251 REWR_CONV (GSYM INT_LT_NEG) THENC (* ~(if ..) < ~(x * ~1) *) 252 RAND_CONV (REWR_CONV INT_NEG_RMUL THENC (* ... < x * ~~1 *) 253 RAND_CONV (REWR_CONV INT_NEGNEG) THENC 254 (* ... < x * 1 *) 255 REWR_CONV INT_MUL_RID) THENC 256 REDUCE_CONV 257 else 258 REWR_CONV (MATCH_MP elim_lt_coeffs1 cnonz) THENC 259 REDUCE_CONV 260 end tm 261 val do_lt_case = 262 (* deal with tm of form e < c * x [+ b] *) 263 move_terms_from LT Right (null o free_vars) THENC 264 REDUCE_CONV THENC elim_coeff 265 in 266 LAND_CONV do_lt_case THENC 267 RAND_CONV (REWR_CONV elim_le THENC 268 RAND_CONV do_lt_case THENC 269 REWR_CONV (GSYM elim_le)) 270 end 271 272 273 274 fun factor_out g g_t tm = 275 if is_plus tm then BINOP_CONV (factor_out g g_t) tm 276 else let 277 open Arbint 278 val (c,v) = dest_mult tm 279 val c_n = int_of_term c 280 val new_c = c_n div g 281 val new_c_t = term_of_int new_c 282 val new_c_thm = SYM (REDUCE_CONV (mk_mult(g_t,new_c_t))) 283 val cx_eq_thm0 = LAND_CONV (K new_c_thm) tm 284 val reassociate = SYM (SPECL [v, new_c_t, g_t] 285 integerTheory.INT_MUL_ASSOC) 286 in 287 TRANS cx_eq_thm0 reassociate 288 end handle HOL_ERR _ => REFL tm 289 290 fun factor_out_lits g g_t tm = 291 if is_plus tm then BINOP_CONV (factor_out_lits g g_t) tm 292 else if is_int_literal tm then let 293 val tm_i = int_of_term tm 294 val factor = Arbint.div(tm_i, g) 295 val factor_t = term_of_int factor 296 in 297 SYM (REDUCE_CONV (mk_mult(g_t, factor_t))) 298 end 299 else REFL tm 300 301 302fun check_divides tm = let 303 val (l,r) = dest_divides tm 304 val rterms = strip_plus r 305 fun getc t = Arbint.abs (int_of_term (rand (rator t))) 306 fun pull_out_divisor tm = 307 TRY_CONV (BINOP_CONV pull_out_divisor THENC 308 REWR_CONV (GSYM INT_LDISTRIB)) tm 309in 310 case List.mapPartial (Lib.total getc) rterms of 311 [] => CHANGED_CONV REDUCE_CONV tm 312 | cs => let 313 val g = gcdl (int_of_term l :: cs) 314 in 315 if g <> Arbint.one then let 316 val g_t = term_of_int g 317 val g_t_lt0 = EQT_ELIM (REDUCE_CONV (mk_less(zero_tm, g_t))) 318 val divq = Arbint.div(int_of_term l, g) 319 val divisor_ok = SYM (REDUCE_CONV (mk_mult(g_t, term_of_int divq))) 320 in 321 case Lib.total (Lib.pluck is_int_literal) rterms of 322 NONE => 323 (* note that factor_out g g_t always changes the term as 324 far as QConv.THENQC is concerned, so the first line 325 below can not raise QConv.UNCHANGED *) 326 RAND_CONV (factor_out g g_t THENC pull_out_divisor) THENC 327 LAND_CONV (K divisor_ok) THENC 328 REWR_CONV (GSYM (MATCH_MP justify_divides g_t_lt0)) THENC 329 REWRITE_CONV [INT_DIVIDES_1] 330 | SOME(literal,rest) => let 331 val literal_i = int_of_term literal 332 val (litq, litr) = Arbint.divmod(literal_i, g) 333 val sorted = 334 EQT_ELIM (AC_CONV (INT_ADD_ASSOC, INT_ADD_COMM) 335 (mk_eq(r, 336 mk_plus(list_mk_plus rest, 337 literal)))) 338 in 339 if litr = Arbint.zero then let 340 val literal_ok = 341 SYM (REDUCE_CONV (mk_mult(g_t, term_of_int litq))) 342 in 343 RAND_CONV (K sorted THENC 344 factor_out g g_t THENC 345 RAND_CONV (K literal_ok) THENC 346 pull_out_divisor) THENC 347 LAND_CONV (K divisor_ok) THENC 348 REWR_CONV (GSYM (MATCH_MP justify_divides g_t_lt0)) THENC 349 REWRITE_CONV [INT_DIVIDES_1] THENC 350 TRY_CONV check_divides 351 end 352 else 353 RAND_CONV (K sorted THENC 354 factor_out g g_t THENC 355 REWRITE_CONV [GSYM INT_LDISTRIB]) THENC 356 LAND_CONV (K divisor_ok) THENC 357 REWR_CONV justify_divides2 THENC 358 RAND_CONV REDUCE_CONV THENC REWR_CONV F_and_r 359 end 360 end 361 else 362 (* gcd is 1, but if l divides any of the summands on the right *) 363 (* these can still be eliminated *) 364 let 365 val li = int_of_term l 366 fun getn t = getc t handle HOL_ERR _ => Arbint.abs (int_of_term t) 367 val rns = map getn rterms 368 fun ldivs t = Arbint.mod(getn t, li) = Arbint.zero 369 val (ldivs, lndivs) = partition ldivs rterms 370 in 371 if not (null ldivs) then let 372 val sorted = 373 EQT_ELIM (AC_CONV (INT_ADD_ASSOC, INT_ADD_COMM) 374 (mk_eq(r, 375 mk_plus(list_mk_plus ldivs, 376 list_mk_plus lndivs)))) 377 in 378 RAND_CONV (K sorted THENC 379 LAND_CONV (factor_out li l THENC 380 factor_out_lits li l THENC 381 REWRITE_CONV [GSYM INT_LDISTRIB])) THENC 382 REWR_CONV justify_divides3 THENC 383 TRY_CONV check_divides 384 end 385 else let 386 val r_gcd = gcdl rns 387 in 388 if r_gcd <> Arbint.one then let 389 val r_gcdt = term_of_int r_gcd 390 val gcd_term = 391 list_mk_comb(gcd_t, 392 [dest_injected l, 393 numSyntax.mk_numeral (Arbint.toNat r_gcd)]) 394 in 395 RAND_CONV (factor_out r_gcd r_gcdt THENC 396 factor_out_lits r_gcd r_gcdt THENC 397 REWRITE_CONV [GSYM INT_LDISTRIB]) THENC 398 REWR_CONV 399 (MATCH_MP INT_DIVIDES_RELPRIME_MUL 400 (REDUCE_CONV gcd_term)) 401 end 402 else 403 ALL_CONV 404 end 405 end 406 end tm 407end 408 409fun EVERY_SUMMAND_CONV c t = 410 if is_plus t then BINOP_CONV (EVERY_SUMMAND_CONV c) t 411 else c t 412 413 414fun minimise_divides tm = let 415 val (l,r) = dest_divides tm 416 val l_i = int_of_term l 417 val _ = Arbint.<(Arbint.zero, l_i) orelse 418 raise ERR "minimise_divides" "LHS of divides not positive" 419 fun rhs_ok t = let 420 val (l,r) = dest_plus t 421 in 422 rhs_ok l andalso rhs_ok r 423 end handle HOL_ERR _ => let 424 val c = #1 (dest_mult t) handle HOL_ERR _ => t 425 val ci = int_of_term c 426 open Arbint 427 in 428 zero <= ci andalso ci < l_i 429 end 430 val _ = not (rhs_ok r) orelse raise UNCHANGED 431 fun split_summand t = let 432 val ((c, v), cval) = (dest_mult t, LAND_CONV) 433 handle HOL_ERR _ => ((t, one_tm), I) 434 val c_i = int_of_term c 435 val (d, m) = Arbint.divmod(c_i, l_i) 436 val _ = d <> Arbint.zero orelse raise UNCHANGED 437 val ld_pl_m = 438 SYM (REDUCE_CONV (mk_plus(mk_mult(l, term_of_int d), term_of_int m))) 439 in 440 cval (K ld_pl_m) THENC 441 TRY_CONV (REWR_CONV INT_RDISTRIB THENC 442 LAND_CONV (REWR_CONV (GSYM INT_MUL_ASSOC))) 443 end t 444 fun sort1 tm = let 445 (* tm is of form (l * x + y) + z, Here we add z to the appropriate 446 sub-term *) 447 val z = rand tm 448 in 449 if (lhand z = l handle HOL_ERR _ => false) then 450 REWR_CONV INT_ADD_COMM THENC REWR_CONV INT_ADD_ASSOC THENC 451 LAND_CONV (REWR_CONV (GSYM INT_LDISTRIB)) 452 else REWR_CONV (GSYM INT_ADD_ASSOC) 453 end tm 454 fun sort tm = 455 if is_plus tm then (LAND_CONV sort THENC sort1) tm 456 else (REWR_CONV (GSYM INT_ADD_LID) THENC 457 LAND_CONV (REWR_CONV (GSYM INT_ADD_LID) THENC 458 LAND_CONV (K (SYM (SPEC l INT_MUL_RZERO)))) THENC 459 sort1) tm 460in 461 RAND_CONV (EVERY_SUMMAND_CONV split_summand THENC 462 REWRITE_CONV [INT_ADD_ASSOC] THENC sort) THENC 463 REWR_CONV int_arithTheory.justify_divides3 THENC 464 REWRITE_CONV [INT_ADD_LID, INT_ADD_RID, INT_MUL_LZERO] 465end tm 466 467 468fun elim_paired_divides tm = let 469 val (c1, c2) = dest_conj tm 470 val (mi, ax_b) = dest_divides c1 471 val (ni, ux_v) = dest_divides c2 472 val (ax, b) = dest_plus ax_b 473 val (ux, v) = dest_plus ux_v 474 val (ai, x) = dest_mult ax 475 val (ui, _) = dest_mult ux 476 val a = dest_injected ai 477 val u = dest_injected ui 478 val m = dest_injected mi 479 val n = dest_injected ni 480 val m_nzero = EQT_ELIM (REDUCE_CONV (mk_neg(mk_eq(m, numSyntax.zero_tm)))) 481 val n_nzero = EQT_ELIM (REDUCE_CONV (mk_neg(mk_eq(n, numSyntax.zero_tm)))) 482 val a_nzero = EQT_ELIM (REDUCE_CONV (mk_neg(mk_eq(a, numSyntax.zero_tm)))) 483 val u_nzero = EQT_ELIM (REDUCE_CONV (mk_neg(mk_eq(u, numSyntax.zero_tm)))) 484 val um = numSyntax.mk_mult(u,m) 485 val an = numSyntax.mk_mult(a,n) 486 val d_eq_gcd = SYM (REDUCE_CONV (list_mk_comb(gcd_t, [um,an]))) 487 val (d_an,(p_ai,q_ai)) = 488 extended_gcd (Arbint.toNat (Arbint.*(int_of_term ui, int_of_term mi)), 489 Arbint.toNat (Arbint.*(int_of_term ai, int_of_term ni))) 490 val d = lhs (concl d_eq_gcd) 491 val di = mk_injected d 492 val p = term_of_int p_ai 493 val q = term_of_int q_ai 494 val pum = list_mk_mult [p, ui, mi] 495 val qan = list_mk_mult [q, ai, ni] 496 val d_eq_pum_qan = EQT_ELIM (REDUCE_CONV (mk_eq(di, mk_plus(pum, qan)))) 497 val th0 = 498 MATCH_MP cooper_lemma_1 499 (LIST_CONJ [d_eq_gcd, d_eq_pum_qan, m_nzero, 500 n_nzero, a_nzero, u_nzero]) 501 val th = REWR_CONV th0 tm 502in 503 th 504end 505 506 507val my_INT_MUL_LID = prove( 508 ``(1 * (c * d) = c * d) /\ 509 (~1 * (c * d) = ~c * d) /\ 510 (1 * (c * d + x) = c * d + x) /\ 511 (~1 * (c * d + x) = ~c * d + ~x) /\ 512 (~~x = x)``, 513 REWRITE_TAC [INT_MUL_LID, GSYM INT_NEG_MINUS1, INT_NEG_LMUL, 514 INT_NEG_ADD, INT_NEGNEG]); 515 516 517fun BLEAF_CONV connector c tm = 518 case bop_characterise tm of 519 NONE => c tm 520 | SOME NEGN => RAND_CONV (BLEAF_CONV connector c) tm 521 | SOME _ => connector(LAND_CONV (BLEAF_CONV connector c), 522 RAND_CONV (BLEAF_CONV connector c)) 523 tm 524 525 526 527 528(* ---------------------------------------------------------------------- 529 Initial phases of the Cooper transformation 530 ---------------------------------------------------------------------- *) 531 532 533(* Phase 1 *) 534val remove_bare_vars = let 535 fun Munge t = if is_var t then REWR_CONV (GSYM INT_MUL_LID) t 536 else if intSyntax.is_mult t then ALL_CONV t 537 else NO_CONV t 538in 539 ONCE_DEPTH_CONV Munge 540end 541 542val remove_negated_vars = let 543 fun remove_negated tm = let 544 (* turn ~ var into ~1 * var *) 545 val t0 = dest_negated tm (* exception raised when term not a negation 546 will be trapped appropriately by DEPTH_CONV 547 below *) 548 in 549 if is_var t0 then 550 REWR_CONV INT_NEG_MINUS1 tm 551 else 552 NO_CONV tm 553 end 554in 555 DEPTH_CONV remove_negated 556end 557 558local 559 val basic_rewrite_conv = 560 REWRITE_CONV [boolTheory.NOT_IMP, 561 boolTheory.IMP_DISJ_THM, boolTheory.EQ_IMP_THM, 562 elim_le, elim_ge, elim_gt, 563 INT_SUB_CALCULATE, INT_RDISTRIB, INT_LDISTRIB, 564 INT_NEG_LMUL, INT_NEG_ADD, INT_NEGNEG, INT_NEG_0, 565 INT_MUL_RZERO, INT_MUL_LZERO] 566 fun flip_muls tm = 567 if is_mult tm andalso not (is_var (rand tm)) then let 568 val mcands = strip_mult tm 569 val (var, rest) = Lib.pluck is_var mcands 570 in 571 EQT_ELIM (AC_CONV (INT_MUL_ASSOC, INT_MUL_SYM) 572 (mk_eq(tm, mk_mult(list_mk_mult rest, var)))) 573 end handle HOL_ERR {origin_structure = "Lib", ...} => ALL_CONV tm 574 else if is_comb tm then 575 (RATOR_CONV flip_muls THENC RAND_CONV flip_muls) tm 576 else if is_abs tm then 577 ABS_CONV flip_muls tm 578 else 579 ALL_CONV tm 580in 581 val phase1_CONV = 582 (* formula must be quantifier free *) 583 DEPTH_CONV RED_CONV THENC 584 basic_rewrite_conv THENC remove_negated_vars THENC 585 remove_bare_vars THENC flip_muls THENC 586 DEPTH_CONV RED_CONV THENC REWRITE_CONV [] 587end 588 589(* 590val phase1_CONV = Profile.profile "phase1" phase1_CONV 591*) 592 593(* Phase 2 *) 594(* phase 2 massages the terms so that all of the < terms have one side or 595 the other with just n * x on it, where n is a non-negative integer, and x 596 is the variable we're going to eliminate, unless x can be entirely 597 eliminated, in which case the 0 * x is reduced to 0. 598 599 All equality terms are similarly rewritten so that any involving 600 x have a term of the form c * x on the left hand side. 601 602 Further, all of the int_divides terms (negated or not) involving 603 our variable are cast in the form 604 c1 int_divides (c2 * x) + e 605 where both c1 and c2 are positive constants 606 607 Finally, if the coefficients of variables in less-than or equality terms 608 have a gcd > 1, then we can divide through by that gcd. 609*) 610 611 612val INT_DIVIDES_NEG = CONV_RULE (DEPTH_CONV FORALL_AND_CONV) INT_DIVIDES_NEG 613val INT_NEG_FLIP_LTL = prove( 614 ``!x y. ~x < y = ~y < x``, 615 REPEAT GEN_TAC THEN 616 CONV_TAC (RAND_CONV (RAND_CONV (REWR_CONV (GSYM INT_NEGNEG)))) THEN 617 REWRITE_TAC [INT_LT_NEG]); 618val INT_NEG_FLIP_LTR = prove( 619 ``!x y. x < ~y = y < ~x``, 620 REPEAT GEN_TAC THEN 621 CONV_TAC (RAND_CONV (LAND_CONV (REWR_CONV (GSYM INT_NEGNEG)))) THEN 622 REWRITE_TAC [INT_LT_NEG]); 623 624val negated_elim_lt_coeffs1 = 625 (ONCE_REWRITE_RULE [INT_NEG_FLIP_LTR] o 626 REWRITE_RULE [GSYM INT_NEG_RMUL] o 627 Q.SPECL [`n`, `m`, `~x`]) 628 elim_lt_coeffs1; 629val negated_elim_lt_coeffs2 = 630 (ONCE_REWRITE_RULE [INT_NEG_FLIP_LTL] o 631 REWRITE_RULE [GSYM INT_NEG_RMUL] o 632 Q.SPECL [`n`, `m`, `~x`]) 633 elim_lt_coeffs2; 634 635 636 637val elim_eq_coeffs' = 638 CONV_RULE (STRIP_QUANT_CONV (RAND_CONV 639 (BINOP_CONV (ONCE_REWRITE_CONV [EQ_SYM_EQ])))) 640 elim_eq_coeffs 641 642local 643 val myrewrite_conv = REWRITE_CONV [INT_NEG_ADD, INT_NEG_LMUL, INT_NEGNEG] 644 fun normalise_eqs var tm = 645 if is_eq tm andalso free_in var (rhs tm) then 646 REWR_CONV EQ_SYM_EQ tm 647 else 648 ALL_CONV tm 649in 650 fun phase2_CONV var tm = let 651 val land = rand o rator 652 fun dealwith_negative_divides tm = let 653 val coeff = if is_plus (rand tm) then land (land (rand tm)) 654 else land (rand tm) 655 in 656 if is_negated coeff then 657 REWR_CONV (GSYM (CONJUNCT1 INT_DIVIDES_NEG)) THENC myrewrite_conv 658 else 659 ALL_CONV 660 end tm 661 fun collect_up_other_freevars tm = let 662 val fvs = 663 Listsort.sort (String.compare o (#1 ## #1) o (dest_var ## dest_var)) 664 (free_vars tm) 665 in 666 EVERY_CONV (map collect_in_sum fvs) tm 667 end 668 in 669 if is_disj tm orelse is_conj tm then 670 BINOP_CONV (phase2_CONV var) tm 671 else if is_neg tm then 672 RAND_CONV (phase2_CONV var) tm 673 else if free_in var tm then let 674 val ((l,r),tt) = (dest_less tm, LT) handle HOL_ERR _ => (dest_eq tm, EQ) 675 open Arbint 676 val var_onL = sum_var_coeffs var l 677 val var_onR = sum_var_coeffs var r 678 val (dir1, dir2) = if var_onL < var_onR then (Left, Right) 679 else (Right, Left) 680 (* dir2 is the side where x will be ending up *) 681 val move_CONV = 682 move_terms_from tt dir1 (free_in var) THENC 683 move_terms_from tt dir2 (not o free_in var) 684 685 fun factor_out_over_sum tm = let 686 (* tm is a sum of multiplications where the left hand argument 687 of each multiplication is the same numeral. We want to turn 688 c * x + c * y + ... + c * z 689 into 690 c * (x + y + ... + z) 691 *) 692 in 693 REWRITE_CONV [GSYM INT_LDISTRIB] tm 694 end 695 696 fun fiddle_negs tm = let 697 (* used over a sum of multiplications to fix 698 ~a * (b * c) into a * (~b * c) *) 699 val _ = dest_mult tm 700 in 701 TRY_CONV (REWR_CONV (GSYM INT_NEG_LMUL) THENC 702 REWR_CONV INT_NEG_RMUL THENC 703 RAND_CONV (REWR_CONV INT_NEG_LMUL)) tm 704 end handle HOL_ERR _ => BINOP_CONV fiddle_negs tm 705 706 fun reduce_by_gcd tm = let 707 val (l,r) = (land tm, rand tm) 708 val ts = strip_plus l @ strip_plus r 709 val coeffs = 710 List.mapPartial (fn a => if is_var (rand a) then 711 SOME (rand (rator a)) 712 else NONE) ts 713 (* if there are no variables left in the term, the following will 714 raise an exception, which is fine; it will be caught by the 715 TRY_CONV above us *) 716 val g = gcdl (map (Arbint.abs o intSyntax.int_of_term) coeffs) 717 val _ = g <> one orelse raise ERR "" "" 718 val g_t = term_of_int g 719 val gnum_t = rand g_t 720 val gnum_nonzero = 721 EQF_ELIM (REDUCE_CONV (mk_eq(gnum_t, numSyntax.zero_tm))) 722 val dir1_numeral = 723 List.find is_int_literal (strip_plus (dir_of_pair dir1 (l,r))) 724 val negative_numeral = 725 case dir1_numeral of 726 NONE => false 727 | SOME t => is_negated t 728 val elim_coeffs_thm = 729 case (tt, dir2, negative_numeral) of 730 (LT, Left, false) => MATCH_MP elim_lt_coeffs2 gnum_nonzero 731 | (LT, Left, true) => MATCH_MP negated_elim_lt_coeffs1 gnum_nonzero 732 | (LT, Right, false) => MATCH_MP elim_lt_coeffs1 gnum_nonzero 733 | (LT, Right, true) => MATCH_MP negated_elim_lt_coeffs2 gnum_nonzero 734 | (EQ, Left, _) => MATCH_MP elim_eq_coeffs gnum_nonzero 735 | (EQ, Right, _) => MATCH_MP elim_eq_coeffs' gnum_nonzero 736 in 737 BINOP_CONV (factor_out g g_t) THENC 738 move_terms_from tt dir1 is_mult THENC 739 conv_at dir2 fiddle_negs THENC 740 conv_at dir2 factor_out_over_sum THENC 741 REWR_CONV elim_coeffs_thm THENC 742 REDUCE_CONV 743 end tm 744 in 745 (move_CONV THENC conv_at dir2 collect_terms THENC 746 conv_at dir1 collect_up_other_freevars THENC 747 TRY_CONV (conv_at dir1 collect_additive_consts) THENC 748 conv_at dir2 (LAND_CONV REDUCE_CONV) THENC 749 REWRITE_CONV [INT_MUL_LZERO, INT_ADD_LID, INT_ADD_RID] THENC 750 TRY_CONV (reduce_by_gcd THENC TRY_CONV move_CONV) THENC 751 normalise_eqs var) tm 752 end handle HOL_ERR _ => 753 if is_divides tm then 754 (TRY_CONV (REWR_CONV (CONJUNCT2 INT_DIVIDES_NEG)) THENC 755 RAND_CONV (collect_in_sum var) THENC 756 dealwith_negative_divides THENC 757 RAND_CONV (TRY_CONV (RAND_CONV collect_up_other_freevars)) THENC 758 REWRITE_CONV [INT_MUL_LZERO] THENC REDUCE_CONV) tm 759 else ALL_CONV tm 760 else ALL_CONV tm 761 end 762end 763 764val phase2_CONV = 765 fn t => (*Profile.profile "phase2"*) (QCONV (phase2_CONV t)) 766 767(* Phase 3 *) 768(* phase three takes all of the coefficients of the variable we're 769 eliminating, and calculates their LCM. Every term is then altered to 770 be of the form 771 LCM x < .. or .. < LCM x 772 Then, we can rewrite 773 ?x. .... LCM x ... LCM x ... 774 to 775 ?x'. .... x' .... x' .... /\ LCM divides x' 776 every occurrence of LCM x is replaced with a new variable 777 778*) 779 780fun find_coeff_binop var term = let 781 val (_, args) = strip_comb term (* operator will be < *) 782 val arg1 = hd args 783 val arg2 = hd (tl args) 784in 785 if is_mult arg1 andalso rand arg1 = var then 786 SOME (int_of_term (rand (rator arg1))) 787 else if is_mult arg2 andalso rand arg2 = var then 788 SOME (int_of_term (rand (rator arg2))) 789 else 790 NONE 791end 792 793fun find_coeff_divides var term = let 794 val (_, args) = strip_comb term (* operator will be int_divides *) 795 val arg = hd (tl args) (* first arg is uninteresting, it should be 796 just a constant *) 797 fun recurse_on_rhs t = 798 if is_plus t then recurse_on_rhs (rand (rator t)) 799 else if is_mult t andalso rand t = var then 800 SOME (int_of_term (rand (rator t))) 801 else 802 NONE 803in 804 recurse_on_rhs arg 805end 806 807fun find_coeffs var term = let 808 (* have disj/conj term including the following sorts of leaves that involve 809 the var x: 810 i. c * x < e 811 ii. e < c * x 812 iii. ~(c * x = e) 813 iv. c * x = e 814 v. ~(e = c * x) 815 vi. e = c * x 816 vii. d | c * x + e0 817 viii. ~(d | c * x + e0) 818 want to get list of c's, which should all be integer constants. 819 The e0 may not be present. 820 *) 821 fun deal_with_binop acc tm = 822 case find_coeff_binop var tm of 823 NONE => acc 824 | SOME i => i :: acc 825 fun recurse acc tm = 826 if is_disj tm orelse is_conj tm then 827 recurse (recurse acc (rand tm)) (rand (rator tm)) 828 else if is_less tm orelse is_eq tm then 829 deal_with_binop acc tm 830 else if is_neg tm then 831 recurse acc (rand tm) 832 else if is_divides tm then 833 case find_coeff_divides var tm of 834 NONE => acc 835 | SOME x => x :: acc 836 else 837 acc 838in 839 Lib.mk_set (recurse [] term) 840end 841 842fun find_coeff var term = (* works over un-negated leaves *) 843 if is_divides term then find_coeff_divides var term 844 else if is_less term orelse is_eq term then find_coeff_binop var term 845 else NONE 846 847 848 849 850(* Phase 3 multiplies up all coefficients of x in order to make them 851 the lcm, and then eliminates this, by changing 852 ?x. P (c * x) 853 to 854 ?x. P x /\ c | x 855*) 856(* this phase has to be done at the level of the existential quantifier *) 857(* assume that the existential quantifier still has occurrences of the 858 bound variable in the body *) 859fun LINEAR_MULT tm = let 860 (* tm is of form c * (e1 + e2 + ... en), where each 861 ei is either a constant, or c' * v, with v a variable. 862 This conversion distributes the c over all the ei's *) 863 val _ = if not (is_mult tm) then ignore (NO_CONV tm) else () 864 865 (* use this rather than is_mult, because the only binops about are 866 multiplications *) 867 fun is_binop tm = length (#2 (strip_comb tm)) = 2 868 fun leaf_case tm = 869 if not (is_binop (rand tm)) then REDUCE_CONV tm 870 else (REWR_CONV INT_MUL_ASSOC THENC LAND_CONV REDUCE_CONV) tm 871 fun recurse tm = 872 ((REWR_CONV INT_LDISTRIB THENC BINOP_CONV recurse) ORELSEC leaf_case) tm 873in 874 recurse tm 875end 876 877 878 879(* Phase 3 multiplies up all coefficients of x in order to make them 880 the lcm, and then eliminates this, by changing 881 ?x. P (c * x) 882 to 883 ?x. P x /\ c | x 884*) 885(* this phase has to be done at the level of the existential quantifier *) 886(* assume that the existential quantifier still has occurrences of the 887 bound variable in the body *) 888 fun phase3_CONV term = let 889 val (var, body) = Psyntax.dest_exists term 890 (* first calculate the desired LCM *) 891 val coeffs = find_coeffs var body 892 val lcm = lcml coeffs 893 (* now descend to each less-than term, and update the coefficients of 894 var to be the same lcm *) 895 fun multiply_by_CONV zero_lti cat = 896 case cat of 897 rDIV => REWR_CONV (MATCH_MP justify_divides zero_lti) THENC 898 RAND_CONV LINEAR_MULT THENC LAND_CONV REDUCE_CONV 899 | rLT => REWR_CONV (MATCH_MP lt_justify_multiplication zero_lti) THENC 900 BINOP_CONV LINEAR_MULT 901 | rEQ => REWR_CONV (MATCH_MP eq_justify_multiplication zero_lti) THENC 902 BINOP_CONV LINEAR_MULT 903 904 fun LCMify term = 905 if is_disj term orelse is_conj term then 906 BINOP_CONV LCMify term 907 else if is_neg term then RAND_CONV LCMify term 908 else 909 case (find_coeff var term) of 910 NONE => ALL_CONV term 911 | SOME c => let 912 val i = Arbint.div(lcm, c) 913 in 914 if i = Arbint.one then ALL_CONV term 915 else let 916 val cat = categorise_leaf term 917 val zero_lti = 918 EQT_ELIM (REDUCE_CONV (mk_less(zero_tm, term_of_int i))) 919 in 920 multiply_by_CONV zero_lti cat 921 end term 922 end 923 fun absify_CONV tm = let 924 val arg = mk_mult(term_of_int lcm, var) 925 val body = Term.subst[(arg |-> var)] tm 926 in 927 SYM (BETA_CONV (mk_comb(mk_abs(var, body), arg))) 928 end 929 val eliminate_1divides = 930 if lcm = Arbint.one then 931 BINDER_CONV (RAND_CONV (K 932 (EQT_INTRO (CONJUNCT1 933 (SPEC var INT_DIVIDES_1)))) THENC 934 REWR_CONV T_and_r) 935 else 936 ALL_CONV 937 in 938 (BINDER_CONV (LCMify THENC absify_CONV) THENC 939 REWR_CONV lcm_eliminate THENC 940 RENAME_VARS_CONV [fst (dest_var var)] THENC 941 BINDER_CONV (LAND_CONV BETA_CONV) THENC 942 eliminate_1divides) 943 term 944 end 945 946(* 947val phase3_CONV = Profile.profile "phase3" phase3_CONV 948*) 949 950(* "sophisticated" simplification routines *) 951fun simplify_constrained_disjunct tm = let 952 (* takes a term of the form 953 ?j. ... /\ K (d1 < j /\ j <= d2) j /\ ... 954 and simplifies it *) 955 (* if there is a "conjunct" at the top level of the conjuncts of the 956 form 957 c | x [ + d] 958 where x is the bound variable of the neginf abstraction, and where 959 d, if present at all, is a numeral, then we can reduce the number 960 of cases needed to be considered, using the theorem 961 int_arithTheory.gcdthm2. *) 962 open CooperSyntax 963 val (var, body) = dest_exists tm 964 val body_conjuncts = filter (not o is_constraint) (cpstrip_conj body) 965 966 fun find_sdivides v c tm = let 967 (* knowing that a simple divides term over variable v is a "conjunct" 968 of tm, apply conversion c to that term *) 969 val (l,r) = dest_conj tm 970 in 971 if List.exists (simple_divides v) (cpstrip_conj l) then 972 LAND_CONV (find_sdivides v c) tm 973 else 974 RAND_CONV (find_sdivides v c) tm 975 end handle HOL_ERR _ => let 976 val tm0 = dest_neg tm 977 in 978 if is_neg tm0 then 979 (REWR_CONV NOT_NOT_P THENC find_sdivides v c) tm 980 else (REWR_CONV NOT_OR THENC find_sdivides v c) tm 981 end handle HOL_ERR _ => (* must be there *) let 982 (* possible that phase2 will eliminate variable entirely, turning the 983 term into either true or false *) 984 fun check_vars tm = if is_const tm then ALL_CONV tm else c tm 985 in 986 (phase1_CONV THENC phase2_CONV v THENC check_vars) tm 987 end 988 989 fun pull_out_exists tm = let 990 (* pulls out a nested existential quantifier to the head of the term *) 991 val (c1, c2) = dest_conj tm 992 val (cvl, thm) = 993 if has_exists c1 then (LAND_CONV, GSYM LEFT_EXISTS_AND_THM) 994 else (RAND_CONV, GSYM RIGHT_EXISTS_AND_THM) 995 in 996 (cvl pull_out_exists THENC HO_REWR_CONV thm) tm 997 end handle HOL_ERR _ => 998 if is_exists tm then ALL_CONV tm 999 else NO_CONV tm 1000 1001 1002 fun find_cst v c tm = let 1003 fun atleaf tm = 1004 if is_vconstraint v tm then c tm 1005 else NO_CONV tm 1006 in 1007 BLEAF_CONV (op ORELSEC) atleaf tm 1008 end 1009 1010 fun simp_if_rangeonly tm = let 1011 (* simplifies ?x. K (lo < x /\ x <= hi) x to T, *) 1012 (* knowing that a contradictory constraint would have already been *) 1013 (* dealt with *) 1014 val (bv, body) = dest_exists tm 1015 in 1016 if is_constraint body then 1017 BINDER_CONV (UNCONSTRAIN THENC resquan_onestep) THENC 1018 EXISTS_OR_CONV THENC 1019 LAND_CONV remove_vacuous_existential THENC 1020 REWR_CONV T_or_l 1021 else 1022 ALL_CONV 1023 end tm 1024 1025 fun pull_eliminate tm = 1026 (* it's possible that there is no existential to pull out because 1027 elim_sdivides will have rewritten the divides term to false. *) 1028 if has_exists (rand tm) then 1029 (BINDER_CONV pull_out_exists THENC 1030 SWAP_VARS_CONV THENC 1031 BINDER_CONV Unwind.UNWIND_EXISTS_CONV THENC 1032 (fn tm => let val (v, _) = dest_exists tm 1033 in 1034 BINDER_CONV (find_cst v 1035 (IN_CONSTRAINT simplify_constraints)) 1036 end tm) THENC 1037 simp_if_rangeonly) tm 1038 else 1039 REWRITE_CONV [] tm 1040 1041 val mainwork = 1042 if List.exists (simple_divides var) body_conjuncts then 1043 (*Profile.profile "simpcst.mainwork.simpelim"*) ( 1044 1045 BINDER_CONV (find_sdivides var elim_sdivides) THENC 1046 pull_eliminate THENC 1047 (* variable was present in form 1 * v or ~1 * v; have now just replaced it 1048 with things of the form c * v' [+ c'], so now have bunch of terms of form 1049 1 * (c * v' [+ y]) or ~1 * (c * v [+ y]); get rid of these *) 1050 PURE_REWRITE_CONV [my_INT_MUL_LID]) THENC 1051 (* have another go at this, recursively, but allow for the fact that 1052 we may have reduced the term to true or false or whatever *) 1053 TRY_CONV simplify_constrained_disjunct 1054 else if List.all (not o mem var o free_vars) body_conjuncts then 1055 (* case where existential only has scope over constraint, and 1056 bound variable doesn't appear elsewhere, which can happen if 1057 the F term is something like (\x. F), which tends to happen in 1058 the construction of the neginf term. *) 1059 (*Profile.profile "simpcst.mainwork.vacuous"*) ( 1060 push_in_exists_and_follow 1061 (BINDER_CONV (UNCONSTRAIN THENC resquan_onestep) THENC 1062 EXISTS_OR_CONV THENC 1063 LAND_CONV remove_vacuous_existential THENC 1064 REWR_CONV T_or_l) THENC 1065 REWRITE_CONV [] 1066 ) 1067 else 1068 ALL_CONV 1069in 1070 (BINDER_CONV ((*Profile.profile "simpcst.quick"*) (find_cst var quick_cst_elim)) THENC 1071 ((*Profile.profile "simpcst.unwind"*) Unwind.UNWIND_EXISTS_CONV ORELSEC REWRITE_CONV []) THENC 1072 (*Profile.profile "simpcst.r_i_g"*) reduce_if_ground) ORELSEC 1073 (*Profile.profile "simpcst.mainwork"*) mainwork 1074end tm 1075 1076 1077end (* struct *) 1078