1structure CooperShell :> CooperShell = 2struct 3 4open HolKernel boolLib integerTheory 5 arithmeticTheory intSyntax int_arithTheory intReduce 6 CooperSyntax CooperThms CooperMath; 7 8val ERR = mk_HOL_ERR "CooperShell"; 9val lhand = rand o rator 10 11(* Fix the grammar used by this file *) 12structure Parse = struct 13 open Parse 14 val (Type,Term) = parse_from_grammars integer_grammars 15end 16open Parse 17 18val simple_disj_congruence = 19 tautLib.TAUT_PROVE (Term`!p q r. (~p ==> (q = r)) ==> 20 (p \/ q <=> p \/ r)`) 21val simple_conj_congruence = 22 tautLib.TAUT_PROVE (Term`!p q r. (p ==> (q = r)) ==> 23 (p /\ q <=> p /\ r)`) 24 25fun congruential_simplification tm = let 26 val (d1, d2) = dest_disj tm 27in 28 if is_disj d1 then 29 REWR_CONV (GSYM DISJ_ASSOC) THENC congruential_simplification 30 else if is_conj d1 then 31 LAND_CONV congruential_simplification THENC 32 RAND_CONV congruential_simplification 33 else if Teq d1 then 34 K (SPEC d2 T_or_l) 35 else if Feq d1 then 36 K (SPEC d2 F_or_l) 37 else let 38 val notd1_t = mk_neg d1 39 val notd1_thm = ASSUME notd1_t 40 val notd1 = 41 if is_neg d1 then 42 EQT_INTRO (CONV_RULE (REWR_CONV NOT_NOT_P) notd1_thm) 43 else EQF_INTRO (notd1_thm) 44 val d2_rewritten = SOME (DISCH notd1_t (REWRITE_CONV [notd1] d2)) 45 handle UNCHANGED => NONE 46 in 47 case d2_rewritten of 48 NONE => RAND_CONV congruential_simplification 49 | SOME d2thm => 50 K (MATCH_MP simple_disj_congruence d2thm) THENC 51 (REWR_CONV T_or_r ORELSEC REWR_CONV F_or_r ORELSEC 52 RAND_CONV congruential_simplification) 53 end 54end tm handle HOL_ERR _ => let 55 val (c1, c2) = dest_conj tm 56in 57 if is_conj c1 then 58 REWR_CONV (GSYM CONJ_ASSOC) THENC congruential_simplification 59 else if is_disj c1 then 60 LAND_CONV congruential_simplification THENC 61 RAND_CONV congruential_simplification 62 else if Teq c1 then 63 K (SPEC c2 T_and_l) 64 else if Feq c1 then 65 K (SPEC c2 F_and_l) 66 else let 67 val c2_rewritten = 68 SOME (DISCH c1 (REWRITE_CONV [EQT_INTRO (ASSUME c1)] c2)) 69 handle UNCHANGED => NONE 70 in 71 case c2_rewritten of 72 NONE => RAND_CONV congruential_simplification 73 | SOME th => 74 K (MATCH_MP simple_conj_congruence th) THENC 75 (REWR_CONV T_and_r ORELSEC REWR_CONV F_and_r ORELSEC 76 RAND_CONV congruential_simplification) 77 end 78end tm handle HOL_ERR _ => 79 if is_neg tm then RAND_CONV congruential_simplification tm 80 else ALL_CONV tm 81 82val unwind_constraint = UNCONSTRAIN THENC resquan_remove 83 84val p6_step = prove( 85 ``(?x:int. K (lo < x /\ x <= hi) x /\ P x) <=> 86 lo < hi /\ (P hi \/ (?x:int. K (lo < x /\ x <= hi - 1) x /\ P x))``, 87 REWRITE_TAC [combinTheory.K_THM, LEFT_AND_OVER_OR] THEN 88 EQ_TAC THENL [ 89 CONV_TAC 90 (LAND_CONV (ONCE_REWRITE_CONV [restricted_quantification_simp])) THEN 91 STRIP_TAC THENL [ 92 FIRST_X_ASSUM SUBST_ALL_TAC THEN ASM_REWRITE_TAC [], 93 ASM_REWRITE_TAC [] THEN DISJ2_TAC THEN 94 Q.EXISTS_TAC `x` THEN ASM_REWRITE_TAC [] 95 ], 96 STRIP_TAC THENL [ 97 Q.EXISTS_TAC `hi` THEN ASM_REWRITE_TAC [INT_LE_REFL], 98 ONCE_REWRITE_TAC [restricted_quantification_simp] THEN 99 Q.EXISTS_TAC `x` THEN ASM_REWRITE_TAC [] 100 ] 101 ]); 102 103fun p6_recurse tm = let 104 (* tm of form ?x. K (lo < x /\ x <= hi) x /\ P x *) 105in 106 REWR_CONV p6_step THENC 107 LAND_CONV REDUCE_CONV THENC 108 (REWR_CONV F_and_l ORELSEC 109 (REWR_CONV T_and_l THENC 110 LAND_CONV BETA_CONV THENC 111 RAND_CONV (BINDER_CONV (* under ?x. *) 112 (LAND_CONV (* into K (..) x *) 113 (LAND_CONV (* into lo < x /\ x <= hi - 1 *) 114 (RAND_CONV REDUCE_CONV))) THENC 115 p6_recurse))) 116end tm 117 118 119 120fun phase6_CONV tm = let 121 (* succeeds on disjuncts of the form 122 ?x. K (lo < x /\ x <= hi) x /\ P x 123 and converts these to 124 P (lo + 1) \/ P (lo + 2) \/ ... P hi 125 where each argument to P is actually a real numeral (not an expression) 126 *) 127 val (v, _) = dest_exists tm 128in 129 BINDER_CONV (RAND_CONV (UNBETA_CONV v)) THENC 130 p6_recurse THENC PURE_REWRITE_CONV [F_or_r] 131end tm 132 133(* 134val phase6_CONV = Profile.profile "phase6" phase6_CONV 135*) 136 137fun vphase6_CONV tm = let 138 (* as above, but works over the constraint attached to v, not the one 139 immediately under the binder *) 140 val (v, body) = dest_exists tm 141in 142 BINDER_CONV (move_conj_left (is_vconstraint v)) THENC 143 phase6_CONV 144end tm; 145 146fun elim_vars_round_r tm = let 147 val (l,r) = dest_eq tm 148 handle HOL_ERR _ => dest_less tm 149 val lvars = filter (not o null o free_vars) (strip_plus l) 150 val rvars = filter (not o null o free_vars) (strip_plus r) 151in 152 case op_intersect aconv lvars rvars of 153 [] => NO_CONV 154 | (h::_) => phase2_CONV (hd (free_vars h)) 155end tm 156 157 158val obvious_improvements = 159 ADDITIVE_TERMS_CONV (TRY_CONV collect_additive_consts) THENC 160 STRIP_QUANT_CONV 161 (BLEAF_CONV (op THENC) (elim_vars_round_r ORELSEC 162 TRY_CONV check_divides) THENC 163 REDUCE_CONV) 164 165fun do_equality_simplifications tm = let 166 (* term is existentially quantified. May contain leaf terms of the form 167 v = e, where v is the variable quantified. If there is such a term at 168 the top level of conjuncts, then use UNWIND_CONV to eliminate the 169 quantifier entirely, otherwise, descend the term looking for such 170 terms in the middle of conjunctions and eliminate the equality from the 171 neighbouring conjuncts. *) 172 val (bvar, body) = dest_exists tm 173 fun eq_term tm = is_eq tm andalso lhs tm ~~ bvar 174 fun neq_term t = eq_term (dest_neg t) handle HOL_ERR _ => false 175 176 fun reveal_eq tm = let 177 (* tm is a "conjunctive" term, in which there is an equality of the 178 form (bvar = e). 179 180 Our mission, should we choose to accept it, is to selectively rewrite 181 with de-morgan's thm to reveal the tm to be of the form: 182 P /\ Q /\ (bvar = e) /\ R 183 *) 184 val (c1,c2) = dest_conj tm 185 (* easy case because the top level operator is already correct *) 186 val subconv = 187 if List.exists eq_term (cpstrip_conj c1) then LAND_CONV 188 else RAND_CONV 189 in 190 subconv reveal_eq tm 191 end handle HOL_ERR _ => let 192 val tm0 = dest_neg tm 193 in 194 if is_neg tm0 then 195 (REWR_CONV NOT_NOT_P THENC reveal_eq) tm 196 else (* must be a disjunction *) 197 (REWR_CONV NOT_OR THENC reveal_eq) tm 198 end handle HOL_ERR _ => ALL_CONV tm 199 200 fun reveal_neq tm = let 201 (* tm is a "disjunctive" term in which there is a negated equality *) 202 val (d1,d2) = dest_disj tm 203 val subconv = if List.exists neq_term (cpstrip_disj d1) then LAND_CONV 204 else RAND_CONV 205 in 206 subconv reveal_neq tm 207 end handle HOL_ERR _ => let 208 val tm0 = dest_neg tm 209 in 210 if is_neg tm0 then 211 (REWR_CONV NOT_NOT_P THENC reveal_neq) tm 212 else if is_conj tm0 then 213 (REWR_CONV NOT_AND THENC reveal_neq) tm 214 else ALL_CONV tm 215 end handle HOL_ERR _ => ALL_CONV tm 216 217 fun descend_and_eliminate tm = 218 if is_conj tm then 219 if List.exists eq_term (cpstrip_conj tm) then let 220 val revealed = reveal_eq tm 221 val revealed_t = rhs (concl revealed) 222 val (eqt, rest) = Lib.pluck eq_term (strip_conj revealed_t) 223 val rearranged_t = mk_conj(eqt, list_mk_conj rest) 224 val rearranged = EQT_ELIM (AC_CONV (CONJ_ASSOC, CONJ_COMM) 225 (mk_eq(revealed_t, rearranged_t))) 226 val eliminated = 227 (RAND_CONV (UNBETA_CONV bvar) THENC 228 REWR_CONV CONJ_EQ_ELIM THENC 229 RAND_CONV BETA_CONV) rearranged_t 230 in 231 TRANS (TRANS revealed rearranged) eliminated 232 end 233 else 234 cpEVERY_CONJ_CONV descend_and_eliminate tm 235 else if is_disj tm then 236 if List.exists neq_term (cpstrip_disj tm) then let 237 val revealed = reveal_neq tm 238 val revealed_t = rhs (concl revealed) 239 val (eqt, rest) = Lib.pluck neq_term (strip_disj revealed_t) 240 val rearranged_t = mk_disj(eqt, list_mk_disj rest) 241 val rearranged = EQT_ELIM (AC_CONV (DISJ_ASSOC, DISJ_COMM) 242 (mk_eq(revealed_t, rearranged_t))) 243 val eliminated = 244 (RAND_CONV (UNBETA_CONV bvar) THENC 245 REWR_CONV DISJ_NEQ_ELIM THENC 246 RAND_CONV BETA_CONV) rearranged_t 247 in 248 TRANS (TRANS revealed rearranged) eliminated 249 end 250 else 251 cpEVERY_DISJ_CONV descend_and_eliminate tm 252 else if is_neg tm then 253 RAND_CONV descend_and_eliminate tm 254 else ALL_CONV tm 255in 256 if List.exists eq_term (cpstrip_conj body) then 257 BINDER_CONV reveal_eq THENC Unwind.UNWIND_EXISTS_CONV 258 else 259 BINDER_CONV descend_and_eliminate 260end tm 261 262fun reveal_a_disj tm = 263 if is_disj tm then ALL_CONV tm 264 else let 265 val tm0 = dest_neg tm 266 in 267 if is_conj tm0 then REWR_CONV NOT_AND tm 268 else (REWR_CONV NOT_NOT_P THENC reveal_a_disj) tm 269 end 270 271 272 273open CooperCore 274local 275 fun stop_if_exelim tm = 276 if is_exists tm then NO_CONV tm 277 else REDUCE_CONV tm 278in 279 fun eliminate_existential tm = let 280 val (bvar, body) = dest_exists tm 281 handle HOL_ERR _ => 282 raise ERR "eliminate_existential" "term not an exists" 283 val base_case = 284 BINDER_CONV (phase2_CONV bvar THENC 285 REPEATC (CHANGED_CONV congruential_simplification) THENC 286 REDUCE_CONV) THENC 287 ((REWR_CONV EXISTS_SIMP THENC REWRITE_CONV []) ORELSEC 288 (phase3_CONV THENC do_equality_simplifications THENC 289 (stop_if_exelim ORELSEC 290 (phase4_CONV THENC phase5_CONV)))) 291 in 292 if cpis_disj body then 293 BINDER_CONV reveal_a_disj THENC EXISTS_OR_CONV THENC 294 (RAND_CONV eliminate_existential) THENC 295 (LAND_CONV eliminate_existential) 296 else 297 base_case THENC EVERY_DISJ_CONV obvious_improvements 298 end tm 299end 300 301val eliminate_existential_entirely = 302 (* used to eliminate an existential, and to lose any constraint *) 303 (* existentials underneath; basically eliminate_existential followed *) 304 (* by phase 6 *) 305 eliminate_existential THENC 306 EVERY_DISJ_CONV 307 (TRY_CONV phase6_CONV THENC 308 (* variables substituted in might result in ground 309 multiplication terms *) 310 REDUCE_CONV THENC obvious_improvements) 311 312 313fun eliminate_quantifier tm = let 314(* assume that there are no quantifiers below the one we're eliminating *) 315in 316 if is_forall tm then 317 flip_forall THENC RAND_CONV eliminate_existential_entirely 318 else if is_exists tm then 319 eliminate_existential_entirely 320 else if is_exists1 tm then 321 HO_REWR_CONV cpEU_THM THENC 322 RAND_CONV (BINDER_CONV eliminate_quantifier THENC 323 eliminate_quantifier) THENC 324 RATOR_CONV (RAND_CONV eliminate_quantifier) 325 else 326 raise ERR "eliminate_quantifier" 327 "Not a forall or an exists or a unique exists" 328end tm 329 330fun find_low_quantifier tm = let 331 fun underc g f = 332 case f of 333 NONE => NONE 334 | SOME f' => SOME (g o f') 335in 336 if (is_forall tm orelse is_exists tm orelse is_exists1 tm) then 337 case find_low_quantifier (#2 (dest_abs (#2 (dest_comb tm)))) of 338 NONE => SOME I 339 | x => underc BINDER_CONV x 340 else if is_comb tm then 341 case find_low_quantifier (rand tm) of 342 NONE => underc RATOR_CONV (find_low_quantifier (rator tm)) 343 | x => underc RAND_CONV x 344 else 345 NONE 346end 347 348fun myfind f [] = NONE 349 | myfind f (h::t) = case f h of NONE => myfind f t | x => x 350 351fun find_equality tm = let 352 (* if there is an equality term as a conjunct underneath any number of 353 disjuncts, then return one of the free variables of that equality *) 354 fun check_conj tm = 355 if is_eq tm then let 356 val fvs = free_vars tm 357 in 358 if not (null fvs) then SOME (hd fvs) else NONE 359 end else NONE 360in 361 myfind check_conj (cpstrip_conj tm) 362end 363 364fun best_var vars tm = let 365 (* Finds the variable in the list vars that occurs in term tm so as 366 to minimise the number of splits necessary if that variable was 367 chosen to eliminate. The rating given to a variable is 368 the minimum of its a and b-var counts. 369 370 Weights variables slightly higher for appearing earlier in the 371 list vars, this means that unnecessary swapping of existential 372 variables is avoided. Assume that all variables in term and all 373 the variables in the list are of type int. Return SOME n, or 374 NONE if vars is the empty list *) 375 fun assess_leaf v negp t = let 376 (* returns a-count and b-count for v in term t, with negp true if 377 term is under a negation *) 378 val (f, args) = strip_comb t 379 val (arg1, arg2) = (hd args, hd (tl args)) 380 val c1 = sum_var_coeffs v arg1 381 val c2 = sum_var_coeffs v arg2 382 open Arbint 383 in 384 if c1 = c2 then (zero,zero) 385 else if same_const f less_tm then 386 if negp then 387 if Arbint.<(c1, c2) then (one,zero) else (zero,one) 388 else 389 if Arbint.<(c1, c2) then (zero,one) else (one,zero) 390 else (one,one) (* must be an equality *) 391 end 392 fun assess negp map t = let 393 val (f, args) = strip_comb t 394 in 395 if same_const f boolSyntax.negation then assess (not negp) map (hd args) 396 else if same_const f boolSyntax.conjunction orelse 397 same_const f boolSyntax.disjunction 398 then 399 assess negp (assess negp map (hd args)) (hd (tl args)) 400 else if is_const t then 401 (* happens when we have a vacuous quantification over true or false *) 402 map 403 else let 404 fun foldthis (v, map) = let 405 open Arbint 406 val (a,b) = assess_leaf v negp t 407 val (a0,b0) = Binarymap.find(map, v) 408 handle Binarymap.NotFound => (zero,zero) 409 in 410 Binarymap.insert(map, v, (a + a0, b + b0)) 411 end 412 in 413 List.foldl foldthis map vars 414 end 415 end 416 val initial_map = Binarymap.mkDict Term.compare 417in 418 case vars of 419 [] => NONE 420 | [x] => SOME x 421 | (v::vs) => let 422 val final_map = assess false initial_map tm 423 val start = (v, Arbint.min(Binarymap.find(final_map, v)) 424 handle Binarymap.NotFound => Arbint.zero) 425 fun findmin (v, acc as (minvar, minc)) = let 426 val vc = Arbint.min(Binarymap.find(final_map, v)) 427 handle Binarymap.NotFound => Arbint.zero 428 in 429 if Arbint.<=(vc, minc) then (v, vc) else acc 430 end 431 in 432 SOME (#1 (List.foldl findmin start vs)) 433 end 434end 435 436 437 438fun pull_last_exists_to_top tm = let 439 val (v, body) = dest_exists tm 440in 441 if is_exists body then 442 (BINDER_CONV pull_last_exists_to_top THENC 443 SWAP_VARS_CONV) tm 444 else 445 ALL_CONV tm 446end 447 448fun push_nthvar_to_bot n tm = 449 if n <= 0 then TRY_CONV (SWAP_VARS_CONV THENC 450 BINDER_CONV (push_nthvar_to_bot 0)) tm 451 else BINDER_CONV (push_nthvar_to_bot (n - 1)) tm 452 453fun listlex_compare c (l1, l2) = 454 (* do a lexicographic comparison of list1 and list2, using c to compare 455 their elements *) 456 case (l1, l2) of 457 ([], []) => EQUAL 458 | (h::t, []) => GREATER 459 | ([], h::t) => LESS 460 | (h1::t1, h2::t2) => 461 case c(h1, h2) of 462 EQUAL => listlex_compare c (t1, t2) 463 | x => x 464 465fun find_dup c l = 466 (* l is a sorted list; find the first duplicated element, according to c *) 467 case l of 468 [] => NONE 469 | [_] => NONE 470 | (h1 :: (tail as (h2 :: t))) => if c(h1, h2) = EQUAL then SOME h1 471 else find_dup c tail 472 473val do_muls = ONCE_DEPTH_CONV LINEAR_MULT 474 475fun find_triangle_eliminable vset dcsts csts = let 476 (* pick an element of vset to minimise the blow-up after doing a 477 Cooper triangle elimination on the two dcsts The list csts is of 478 range constraints from the problem. 479 480 Recall that 481 m | ax + b /\ n | ux + v 482 gets turned into 483 mn | dx + vmp + bnq /\ d | av - ub 484 where 485 d = gcd(mu, an) = pum + qan 486 487 If vset has two elements, then the second conjunct of the result will 488 be a divides constraint over just one variable, and we can pick the 489 variable that results in the best performance. It's not clear what 490 should be done if there are more variables. 491 492 For the moment, and this is probably a god-awful HACK, just return 493 the hd of the list vset. 494 *) 495in 496 if length vset > 2 then (hd vset, hd (tl vset)) 497 else let 498 open Arbint 499 val dcst1 = hd dcsts 500 val dcst2 = hd (tl dcsts) 501 val (m, rhs1) = dest_divides dcst1 502 val m_i = int_of_term m 503 val (n, rhs2) = dest_divides dcst2 504 val n_i = int_of_term n 505 fun calculate_score v_to_go v_to_remain = let 506 val a_i = abs (sum_var_coeffs v_to_go rhs1) 507 val u_i = abs (sum_var_coeffs v_to_go rhs2) 508 val d0_i = gcd(m_i, n_i) 509 val b_i = sum_var_coeffs v_to_remain rhs1 510 val v_i = sum_var_coeffs v_to_remain rhs2 511 val remain0_i = a_i * v_i - u_i * b_i 512 val divide_by = gcd(d0_i, abs remain0_i) 513 val remain_i = remain0_i div divide_by 514 val d_i = d0_i div divide_by 515 val cst = valOf (List.find (is_vconstraint v_to_remain) csts) 516 in 517 constraint_size cst div d_i 518 end 519 val v1 = hd vset 520 val v2 = hd (tl vset) 521 val v1_score = calculate_score v1 v2 522 val v2_score = calculate_score v2 v1 523 in 524 if v1_score > v2_score then (v2,v1) else (v1,v2) 525 end 526end 527 528 529 530 531 532 533fun finish_pure_goal1 tm = let 534 (* tm is of the form 535 ?x1 .. xn. K1 /\ K2 /\ .. /\ Kn /\ P (x1..xn) /\ 536 c1 | ... /\ c2 | ... 537 where the Ki's are constraints (one per existential variable). 538 In this stage of the process we try to do "delta elimination" to 539 avoid having to consider all of the possibilities in the 540 constraints. Sometimes this is not possible, but the effect of this 541 function is to make one step of progress regardless. 542 543 The ideal situation is when one of the ex. variables is mentioned just 544 once in a divisibility term's right-hand-side. If this situation holds 545 we can use simplify_constrained_disjunct to make progress. Otherwise, 546 if two divisibility constraints exist with the same set of free 547 variables on the right hand side, we can make progress by using 548 Cooper's first lemma to change this, producing two new divisibility 549 constraints, one of which has one fewer variable than the original. 550 551 If neither situation holds, then we have no choice but to expand 552 one of the variables, as per phase6. We pick the variable with the 553 smallest range. 554 *) 555 val (vars, body) = strip_exists tm 556 val (constraints, nonconstraints) = 557 partition is_constraint (cpstrip_conj body) 558 val (div_constraints, others) = partition is_divides nonconstraints 559 val divc_rhses = map (#2 o dest_divides) div_constraints 560 val canonicalise_varsets = Listsort.sort Term.compare 561 fun free_vars' t = (t, free_vars t) 562 fun nzero_coeffs (t, vlist) = 563 filter (fn v => sum_var_coeffs v t <> Arbint.zero) vlist 564 val div_varsets = 565 map (canonicalise_varsets o nzero_coeffs o free_vars') divc_rhses 566in 567 case List.find (fn lst => length lst = 1) div_varsets of 568 SOME vs => let 569 (* found a singleton divisibility constraint *) 570 val v = hd vs 571 in 572 push_nthvar_to_bot (index (aconv v) vars) THENC 573 STRIP_QUANT_CONV (phase2_CONV v) THENC 574 LAST_EXISTS_CONV simplify_constrained_disjunct THENC 575 do_muls 576 end 577 | NONE => let 578 val vset_compare = listlex_compare Term.compare 579 val sorted_vsets = Listsort.sort vset_compare div_varsets 580 in 581 case find_dup vset_compare sorted_vsets of 582 SOME vset => let 583 fun my_constraint tm = 584 is_divides tm andalso 585 tml_eq (canonicalise_varsets (free_vars (#2 (dest_divides tm)))) 586 vset 587 val (var_to_eliminate, var_to_keep) = 588 find_triangle_eliminable 589 vset 590 (List.take(List.filter my_constraint div_constraints, 2)) 591 constraints 592 in 593 STRIP_QUANT_CONV 594 (move_conj_left my_constraint THENC 595 RAND_CONV (move_conj_left my_constraint) THENC 596 REWR_CONV CONJ_ASSOC THENC 597 LAND_CONV (phase2_CONV var_to_eliminate THENC 598 REWRITE_CONV [GSYM INT_ADD_ASSOC] THENC 599 elim_paired_divides THENC 600 phase1_CONV THENC phase2_CONV var_to_keep THENC 601 BINOP_CONV (TRY_CONV check_divides) THENC 602 REWRITE_CONV [INT_DIVIDES_1])) 603 end 604 | NONE => let 605 (* look for constraint with least range *) 606 fun min (c_tm, acc as (accv, acci)) = let 607 val i = constraint_size c_tm 608 in 609 if Arbint.<(i,acci) then (constraint_var c_tm, i) else acc 610 end 611 val init = let val c = hd constraints 612 in (constraint_var c, constraint_size c) 613 end 614 val (minv, _) = List.foldl min init (tl constraints) 615 in 616 push_nthvar_to_bot (index (aconv minv) vars) THENC 617 LAST_EXISTS_CONV vphase6_CONV THENC 618 push_in_exists 619 end 620 end 621end tm 622 623fun finish_pure_goal tm = 624 if is_exists tm then 625 ((REWR_CONV EXISTS_SIMP ORELSEC finish_pure_goal1) THENC 626 EVERY_DISJ_CONV (obvious_improvements THENC finish_pure_goal)) tm 627 else REDUCE_CONV tm 628 629 630(* 631 val tm0 = ``?w. ((y = 2 * w) \/ (y = 2 * w + 1)) /\ x <= w /\ w < z`` 632 val tm = rhs (concl (phase1_CONV tm0)) 633 634 val tm0 = 635 ``!x y z. 2 * x < y /\ y < 2 * z ==> 636 (~(1 * y + ~1 < 2 * x) /\ 1 * y + ~1 < 2 * z /\ 637 2 int_divides 1 * y + ~1 \/ 638 ~(1 * y < 2 * x) /\ 1 * y < 2 * z /\ 2 int_divides 1 * y) \/ 639 ~(1 * y + ~1 < 2 * x) /\ 1 * y + ~1 < 2 * z /\ 640 2 int_divides 1 * y + ~1 \/ 641 ((2 * z + ~2 = 1 * y) \/ (2 * z + ~2 = 1 * y + ~1)) /\ 642 ~(2 * z + ~2 < 2 * x)`` 643 val tm = rand (rhs (concl ((phase1_CONV THENC flip_foralls) tm0))) 644 645val tm0 = 646 ``!x. 647 0 <= x ==> 648 !x'. 649 0 <= x' ==> 650 x' <= x ==> 651 !x''. 652 0 <= x'' ==> 653 (~(x <= x') \/ (x'' + x = x'' + x') \/ 654 x'' <= 0 /\ x'' + x' <= x) /\ 655 (x <= x' \/ 656 (~(x'' + x' <= x) \/ (x'' + x' = x) \/ x'' <= 0 /\ x <= x') /\ 657 (x'' + x' <= x \/ (x'' + (x + x') = x + (x'' + x')) \/ 658 x'' <= 0 /\ x + (x'' + x') <= x + x')) \/ 659 (x'' + x' <= x \/ x'' <= 0) /\ x'' + x' <= x + 0`` 660 661val tm = rand (rhs (concl ((phase1_CONV THENC move_quants_up THENC 662 flip_foralls) tm0))) 663 664 665*) 666 667fun pure_goal0 tm = let 668 (* pure_goal is called on those goals that have all existential 669 quantifiers; these are assumed to be at the head of the term *) 670 val (vars, body) = strip_exists tm 671 fun pull_out_and_recurse n tm = let 672 (* tm is of the form ?x1 .. xn. p *) 673 (* where p may or may not have an existential quantifier *) 674 (* if there is a quantifier over p, want to pull it out to the front *) 675 (* of the list and then recurse just underneath it, otherwise recurse *) 676 (* immediately *) 677 val (vars, body) = strip_exists tm 678 in 679 if length vars = n then pure_goal0 tm 680 else (pull_last_exists_to_top THENC BINDER_CONV pure_goal0) tm 681 end 682in 683 if null vars then REDUCE_CONV 684 else if cpis_disj body then 685 STRIP_QUANT_CONV reveal_a_disj THENC 686 push_in_exists THENC BINOP_CONV pure_goal0 THENC 687 REDUCE_CONV 688 else let 689 val next_var = 690 case find_equality body of 691 NONE => valOf (best_var vars body) 692 | SOME v => v 693 in 694 push_nthvar_to_bot (index (aconv next_var) vars) THENC 695 LAST_EXISTS_CONV eliminate_existential THENC 696 TRY_CONV push_in_exists THENC 697 EVERY_DISJ_CONV (pull_out_and_recurse (length vars - 1) THENC 698 TRY_CONV push_in_exists) 699 end 700end tm 701 702(* 703val pure_goal0 = Profile.profile "pure_goal0" pure_goal0 704val finish_pure_goal = Profile.profile "finish_pure_goal" finish_pure_goal 705*) 706 707val pure_goal = pure_goal0 THENC EVERY_DISJ_CONV finish_pure_goal THENC 708 REDUCE_CONV 709 710val tm100 = term_of_int (Arbint.fromInt 100) 711fun counter_example tm = let 712 open seqmonad 713 infix >- >> ++ 714 fun rule f th = (seq.result (f th, ())) handle HOL_ERR _ => seq.empty 715 fun test th = 716 if Feq (concl th) then 717 seq.result(EQF_INTRO (NOT_INTRO (DISCH tm th)),()) 718 else seq.empty 719 fun spec n th = let 720 in 721 if is_forall (concl th) then 722 if n > 0 then 723 ((rule (SPEC zero_tm) ++ rule (SPEC tm100)) >> 724 spec (n - 1)) 725 else rule (SPEC one_tm) >> spec (n - 1) 726 else 727 rule (CONV_RULE REDUCE_CONV) >> test 728 end th 729in 730 case seq.cases (spec 5 (ASSUME tm)) of 731 NONE => NO_CONV tm 732 | SOME ((th,()),_) => th 733end 734 735 736fun decide_pure_presburger_term tm = let 737 (* no free variables allowed *) 738 val phase0_CONV = 739 (* rewrites out conditional expression terms *) 740 TOP_DEPTH_CONV (REWR_CONV COND_EXPAND ORELSEC 741 REWR_CONV COND_RATOR ORELSEC 742 IntDP_Munge.NBOOL_COND_RAND_CONV ORELSEC 743 IntDP_Munge.COND_ABS_CONV) 744 745 fun mainwork tm = let 746 in 747 case find_low_quantifier tm of 748 NONE => REDUCE_CONV 749 | SOME f => 750 f eliminate_quantifier THENC 751 REWRITE_CONV [] 752 end tm 753 fun strategy tm = 754 case goal_qtype tm of 755 NEITHER => (mainwork THENC strategy) tm 756 | EITHER => REDUCE_CONV tm 757 | qsUNIV => 758 (move_quants_up THENC 759 ((* counter_example ORELSEC *) 760 (flip_foralls THENC 761 RAND_CONV pure_goal THENC REDUCE_CONV))) tm 762 | qsEXISTS => (move_quants_up THENC pure_goal) tm 763in 764 phase0_CONV THENC phase1_CONV THENC strategy 765end tm 766 767(* the following is useful in debugging the above; given an f, the 768 function term_at_f will return the term "living" at f, as long as there 769 are no terms of the form (I tm) in the original. 770 local fun I_CONV tm = SYM (ISPEC tm combinTheory.I_THM) 771 val I_tm = Term`I:bool->bool b` 772 in 773 fun term_at_f f tm = 774 rand (find_term (can (match_term I_tm)) (rhs (concl (f I_CONV tm)))) 775 end 776 another useful function is this, which allows for the elimination 777 of the specified number of quantifiers: 778 fun elim_nqs n tm = let 779 in 780 if n <= 0 then ALL_CONV 781 else 782 case find_low_quantifier tm of 783 NONE => ALL_CONV 784 | SOME f => f eliminate_quantifier THENC REWRITE_CONV [] THENC 785 elim_nqs (n - 1) 786 end tm 787 788*) 789 790end 791