1structure OmegaSymbolic :> OmegaSymbolic = 2struct 3 4(* This file implements the horrid part of the Omega test, when you have to 5 do quantifier elimination symbolically, and without the benefit of being 6 able to work outside the logic. 7 8 In particular, this means that this part of the procedure has to work 9 using the theorems in OmegaTheory. 10 11 Input is a term of the form 12 ?x. r1 /\ r2 /\ .. rn 13 where each rn is in "Omega leaf normal form", i.e. 14 0 <= c1 * v1 + c2 * v2 + c3 * v3 + c 15*) 16 17open HolKernel boolLib intSyntax 18 19open integerTheory OmegaTheory 20 21val lhand = rand o rator 22 23 24val REWRITE_CONV = GEN_REWRITE_CONV TOP_DEPTH_CONV bool_rewrites 25 26fun EVERY_CONJ_CONV c t = 27 if is_conj t then BINOP_CONV (EVERY_CONJ_CONV c) t 28 else c t 29 30fun EVERY_DISJ_CONV c t = 31 if is_disj t then BINOP_CONV (EVERY_DISJ_CONV c) t 32 else c t 33 34fun ERR f msg = HOL_ERR { origin_structure = "OmegaSymbolic", 35 origin_function = f, 36 message = msg} 37 38(* ---------------------------------------------------------------------- 39 clause_to_evals v t 40 41 where v is a variable, and t is a conjunction of <= or divisibility 42 leaves. 43 Returns a theorem of the form 44 t = (evalleft v lefts /\ evalright v rights) /\ extras 45 where v is not free in extras. Extras may be the term T. 46 47 ---------------------------------------------------------------------- *) 48 49val pvar = mk_var("p", bool) 50val qvar = mk_var("q", bool) 51val xvar = mk_var("x", int_ty) 52fun clause_to_evals v tm = let 53 val step0 = REWRITE_CONV [GSYM CONJ_ASSOC] 54 fun step1 tm = INST [pvar |-> tm, xvar |-> v] eval_base 55 fun mk_upper cf t = let 56 (* cf will be the negative coefficient of v *) 57 val poscf_t = mk_mult(term_of_int (Arbint.~ cf), v) 58 in 59 K (SYM (SPECL [poscf_t, zero_tm, rand t] INT_LE_LADD)) THENC 60 FORK_CONV (REWR_CONV INT_ADD_RID, REWR_CONV INT_ADD_COMM) THENC 61 RAND_CONV OmegaMath.SORT_AND_GATHER1_CONV 62 end t 63 fun mk_lower cf t = let 64 (* cf will be the positive coefficient of v *) 65 val neg_t = mk_negated(mk_mult(term_of_int cf, v)) 66 in 67 K (SYM (SPECL [neg_t, zero_tm, rand t] INT_LE_LADD)) THENC 68 FORK_CONV (REWR_CONV INT_ADD_RID, REWR_CONV INT_ADD_COMM) THENC 69 RAND_CONV (RAND_CONV (REWR_CONV INT_NEG_LMUL) THENC 70 OmegaMath.SORT_AND_GATHER1_CONV THENC 71 REWR_CONV (GSYM INT_NEGNEG)) THENC 72 REWR_CONV INT_LE_NEG 73 end t 74 75 fun normal_step tm = let 76 val (c1, c2) = dest_conj tm 77 val (evals, ex) = dest_conj c1 78 val (ups, lows) = dest_conj evals 79 val (ex1, ex2, up, low, cval, get_t) = 80 if is_conj c2 then 81 (eval_step_extra3, eval_step_extra4, eval_step_upper2, 82 eval_step_lower2, RAND_CONV o LAND_CONV, #1 o dest_conj) 83 else 84 (eval_step_extra1, eval_step_extra2, eval_step_upper1, 85 eval_step_lower1, RAND_CONV, I) 86 val t = get_t c2 87 val cf = if is_neg t orelse is_divides t then Arbint.zero 88 else CooperMath.sum_var_coeffs v (rand t) 89 in 90 if cf = Arbint.zero then 91 if is_const ex then REWR_CONV ex1 92 else REWR_CONV ex2 93 else if Arbint.<(cf, Arbint.zero) then 94 cval (mk_upper cf) THENC REWR_CONV up 95 else 96 cval (mk_lower cf) THENC REWR_CONV low 97 end tm 98in 99 step0 THENC step1 THENC REPEATC normal_step 100end tm 101 102(* ---------------------------------------------------------------------- 103 prove_every_fstnzero t 104 105 t is a term of the form ``[ (num, int); (num, int); ... (num, int)]`` 106 This function attempts to prove |- EVERY fst_nzero ^t 107 ---------------------------------------------------------------------- *) 108 109val c_ty = pairSyntax.mk_prod(numSyntax.num, int_ty) 110val clist_ty = listSyntax.mk_list_type c_ty 111val nil_t = listSyntax.mk_nil c_ty 112val every_t = mk_thy_const {Thy = "list", Name = "EVERY", 113 Ty = (c_ty --> bool) --> clist_ty --> bool}; 114val (every_nil, every_cons) = CONJ_PAIR listTheory.EVERY_DEF 115 116val fst_nzero_t = mk_thy_const {Thy = "Omega", Name = "fst_nzero", 117 Ty = c_ty --> bool}; 118val every_fst_nzero_nil = EQT_ELIM (ISPEC fst_nzero_t every_nil) 119val every_fst_nzero_cons = ISPEC fst_nzero_t every_cons 120fun prove_fstnzero t = 121 EQT_ELIM ((REWR_CONV fst_nzero_def THENC 122 RAND_CONV (REWR_CONV pairTheory.FST) THENC 123 CooperMath.REDUCE_CONV) (mk_comb(fst_nzero_t, t))) 124 125fun prove_every_fstnzero list_t = 126 case total listSyntax.dest_cons list_t of 127 NONE => every_fst_nzero_nil 128 | SOME (h,t) => let 129 val fnz_th = prove_fstnzero h 130 val rest = prove_every_fstnzero t 131 in 132 EQ_MP (SYM (SPECL [h, t] every_fst_nzero_cons)) 133 (CONJ fnz_th rest) 134 end 135 136(* ---------------------------------------------------------------------- 137 prove_every_fst1 t 138 139 t is a term of the form ``[ (num, int); (num, int); ... (num, int)]`` 140 This function attempts to prove |- EVERY fst1 ^t 141 ---------------------------------------------------------------------- *) 142 143val fst1_t = ``Omega$fst1 : num # int -> bool`` 144val every_fst1_nil = EQT_ELIM (ISPEC fst1_t every_nil) 145val every_fst1_cons = ISPEC fst1_t every_cons 146fun prove_fst1 t = 147 EQT_ELIM ((REWR_CONV fst1_def THENC 148 LAND_CONV (REWR_CONV pairTheory.FST) THENC 149 CooperMath.REDUCE_CONV) (mk_comb(fst1_t, t))) 150 151fun prove_every_fst1 list_t = 152 case total listSyntax.dest_cons list_t of 153 NONE => every_fst1_nil 154 | SOME(h,t) => let 155 val h_th = prove_fst1 h 156 val t_th = prove_every_fst1 t 157 in 158 EQ_MP (SYM (SPECL [h,t] every_fst1_cons)) (CONJ h_th t_th) 159 end 160 161(* ---------------------------------------------------------------------- 162 prove_every_fst_lt_m m t 163 164 t is a term of the form ``[ (num, int); (num, int); ... (num, int)]`` 165 m is a term of type :num, and a numeral. 166 This function attempts to prove |- EVERY (\p. FST p <= ^m) ^t 167 ---------------------------------------------------------------------- *) 168 169fun abs_t m = let 170 val p = mk_var("p", c_ty) 171 val body = numSyntax.mk_leq(pairSyntax.mk_fst p, m) 172in 173 mk_abs(p, body) 174end 175 176fun prove_fst_lt_m abs_t t = 177 EQT_ELIM ((BETA_CONV THENC LAND_CONV (REWR_CONV pairTheory.FST) THENC 178 CooperMath.REDUCE_CONV) (mk_comb(abs_t, t))) 179 180fun prove_every_fst_lt_m m t = let 181 val absn = abs_t m 182 fun recurse list_t = 183 case total listSyntax.dest_cons list_t of 184 NONE => EQT_ELIM (ISPEC absn every_nil) 185 | SOME(h,t) => 186 EQ_MP (SYM (ISPECL [absn, h, t] every_cons)) 187 (CONJ (prove_fst_lt_m absn h) (recurse t)) 188in 189 recurse t 190end 191 192(* ---------------------------------------------------------------------- 193 calculate_shadow (sdef, rowdef) t 194 195 sdef is a the "shadow definition", i.e. a couple of theorems 196 defining the shadow type (the conjuncts of real_shadow_def or 197 dark_shadow_def) and rowdef is the analogous pair of theorems 198 defining the corresponding row function (conjuncts of 199 rshadow_row_def or dark_shadow_row_def) 200 ---------------------------------------------------------------------- *) 201 202 203fun munge_to_altform varname th = let 204 val (nilth, consth0) = CONJ_PAIR th 205 val consth = SPEC_ALL consth0 206in 207 (REWRITE_RULE [nilth] (INST [mk_var(varname, clist_ty) |-> nil_t] consth), 208 consth) 209end 210 211val alt_dshadow = munge_to_altform "uppers" dark_shadow_def 212val alt_drow = munge_to_altform "rs" dark_shadow_row_def 213val alt_rshadow = munge_to_altform "ls" real_shadow_def 214val alt_rrow = munge_to_altform "rs" rshadow_row_def 215 216fun calculate_shadow (sdef, rowdef) = let 217 val (s1, scons) = sdef 218 val (r1, rcons) = rowdef 219 val mathnorm = OmegaMath.leaf_normalise 220 fun calculate_row t = 221 ((REWR_CONV r1 THENC mathnorm) ORELSEC 222 (REWR_CONV rcons THENC FORK_CONV (mathnorm, calculate_row))) t 223 fun main t = 224 ((REWR_CONV s1 THENC calculate_row) ORELSEC 225 (REWR_CONV scons THENC FORK_CONV (calculate_row, main))) t 226in 227 main 228end 229 230(* ---------------------------------------------------------------------- 231 expand_evals tm 232 233 tm is of form evalupper x list1 /\ evallower x list2 234 rewrite away the evallower and evalupper terms, keeping everything 235 right associated 236 ---------------------------------------------------------------------- *) 237 238val (evalhi10, evalhi_cons0) = munge_to_altform "cs" evalupper_def 239val (evallo1, evallo_cons) = munge_to_altform "cs" evallower_def 240 241val evalhi1 = AP_THM (AP_TERM conjunction evalhi10) qvar 242val evalhi_cons = 243 CONV_RULE (RAND_CONV (REWR_CONV (GSYM CONJ_ASSOC))) 244 (AP_THM (AP_TERM conjunction evalhi_cons0) qvar) 245 246 247val expand_evals = let 248 fun reclos tm = 249 (REWR_CONV evallo1 ORELSEC 250 (REWR_CONV evallo_cons THENC RAND_CONV reclos)) tm 251 fun rechis tm = 252 ((REWR_CONV evalhi1 THENC RAND_CONV reclos) ORELSEC 253 (REWR_CONV evalhi_cons THENC RAND_CONV rechis)) tm 254in 255 rechis 256end 257 258 259 260(* ---------------------------------------------------------------------- 261 do_divisibility_analysis v ctxt tm 262 263 tm is of the form ?x. (c * x = e) /\ c1 /\ c2 /\ c3 264 where each ci is either of the form d * x <= U or L <= e * x. 265 If e contains any variables that appear in ctxt, then 266 leaf_normalise all of the ci's and the equality term and then rename 267 x to be v (which is its correct name). 268 269 Otherwise, multiply the ci's through so as to make them include 270 c * x as a subterm, then rewrite with the first conjunct, and then 271 leaf normalise. The variable x will have been eliminated from all 272 but the first conjunct. Then push the ?x inwards, and turn that 273 first conjunct into a divides term (c int_divides e). 274 ---------------------------------------------------------------------- *) 275 276fun lcmify v c c_i tm = let 277 (* tm either d * v <= U or L <= e * v, need c * v to be present *) 278 val (l,r) = dest_leq tm 279 val (accessor, cval) = 280 if rand r ~~ v then (rand, RAND_CONV) else (lhand, LAND_CONV) 281 val d = lhand (accessor tm) 282in 283 if d ~~ c then ALL_CONV 284 else let 285 open CooperMath 286 val d_i = int_of_term d 287 val lc = lcm(c_i, d_i) 288 fun multiply_through tm = 289 if lc <> d_i then let 290 val f_i = Arbint.div(lc, d_i) 291 val f = term_of_int f_i 292 val zero_lt_f = 293 EQT_ELIM (REDUCE_CONV (mk_less(zero_tm, f))) 294 val finisher = 295 if f ~~ c then 296 REWR_CONV INT_MUL_ASSOC THENC 297 LAND_CONV (REWR_CONV INT_MUL_COMM) THENC 298 REWR_CONV (GSYM INT_MUL_ASSOC) 299 else 300 REWR_CONV INT_MUL_ASSOC THENC LAND_CONV REDUCE_CONV 301 in 302 (K (SYM (MP (SPECL [f, l, r] INT_LE_MONO) zero_lt_f)) THENC 303 cval finisher) tm 304 end 305 else ALL_CONV tm 306 fun divide_out tm = 307 if lc <> c_i andalso rand (accessor tm) ~~ v then let 308 val f_i = Arbint.div(lc, c_i) 309 val f = term_of_int f_i 310 val fc_eq_l = CooperMath.REDUCE_CONV(mk_mult(f, c)) 311 in 312 (cval (LAND_CONV (K (SYM fc_eq_l)) THENC 313 REWR_CONV (GSYM INT_MUL_ASSOC))) tm 314 end 315 else ALL_CONV tm 316 in 317 multiply_through THENC divide_out 318 end 319end tm 320 321fun do_divisibility_analysis v ctxt tm = let 322 val (x, body) = dest_exists tm 323 val (eqterm, rest) = dest_conj body 324in 325 if not (null (op_intersect aconv (free_vars (rand eqterm)) ctxt)) then 326 (* leave it as an equality *) 327 BINDER_CONV (EVERY_CONJ_CONV OmegaMath.leaf_normalise) THENC 328 RAND_CONV (ALPHA_CONV v) 329 else let 330 val c = lhand (lhand eqterm) 331 val c_i = int_of_term c 332 fun ctxt_rwt tm = let 333 val (c1, c2) = dest_conj tm 334 val thm0 = DISCH_ALL (REWRITE_CONV [ASSUME c1] c2) 335 in 336 MATCH_MP CooperThms.simple_conj_congruence thm0 337 end 338 in 339 BINDER_CONV (RAND_CONV (EVERY_CONJ_CONV (lcmify x c c_i)) THENC 340 ctxt_rwt) THENC 341 EXISTS_AND_CONV THENC 342 LAND_CONV (BINDER_CONV (LAND_CONV (REWR_CONV INT_MUL_COMM)) THENC 343 REWR_CONV (GSYM INT_DIVIDES) THENC 344 RAND_CONV OmegaMath.sum_normalise THENC 345 CooperMath.minimise_divides) THENC 346 RAND_CONV (EVERY_CONJ_CONV OmegaMath.leaf_normalise) THENC 347 REWRITE_CONV [] 348 end 349end tm 350 351 352 353 354(* ---------------------------------------------------------------------- 355 calculate_nightmare ctxt t 356 357 t is a term of the form ?x. nightmare x m ups lows tlist. 358 This function expands it into an equation of the form 359 |- t = D1 \/ D2 \/ D3 \/ .. Dn 360 Each Di is either free of x entirely (but with a divides term present 361 as the first conjunct) or is of the form 362 ?x. (c * x = R) /\ C1 /\ C2 /\ .. Cn 363 where x is absent in all of the Ci, and where R includes at least 364 one variable y, which is present in the list of variables ctxt. 365 366 In this latter situation, the equality and one of the x or y will 367 be eliminated through OmegaEq. In the former situation, the divides 368 term will need special treatment later. 369 ---------------------------------------------------------------------- *) 370 371val (cnightmare10, cnightmare_cons0) = munge_to_altform "rs" calc_nightmare_def 372 373val reassoc_internals = LEFT_AND_EXISTS_CONV THENC 374 BINDER_CONV (REWR_CONV (GSYM CONJ_ASSOC)) 375val cnightmare1 = CONV_RULE (RAND_CONV reassoc_internals) 376 (AP_THM (AP_TERM conjunction cnightmare10) pvar) 377 378val cnightmare_cons = 379 CONV_RULE (RAND_CONV (REWR_CONV RIGHT_AND_OVER_OR THENC 380 LAND_CONV reassoc_internals)) 381 (AP_THM (AP_TERM conjunction cnightmare_cons0) pvar) 382 383fun calculate_nightmare ctxt tm = let 384 val (v, body) = dest_exists tm 385 val reducer = 386 BINDER_CONV (LAND_CONV (RAND_CONV 387 (RAND_CONV CooperMath.REDUCE_CONV))) THENC 388 OmegaMath.calculate_range_disjunct 389 fun recurse t = 390 ((REWR_CONV cnightmare1 THENC reducer) ORELSEC 391 (REWR_CONV cnightmare_cons THENC LAND_CONV reducer THENC 392 RAND_CONV recurse)) t 393in 394 BINDER_CONV (REWR_CONV calculational_nightmare THENC 395 RAND_CONV expand_evals THENC 396 recurse THENC REWRITE_CONV []) THENC 397 CooperSyntax.push_in_exists THENC 398 EVERY_DISJ_CONV (do_divisibility_analysis v ctxt) THENC 399 REWRITE_CONV [] 400end tm 401 402 403(* ---------------------------------------------------------------------- 404 apply_fmve cty t 405 406 t is of the form ?x. c1 /\ c2 /\ c3 .. /\ cn 407 408 Every ci is a valid Omega leaf. This function converts the body 409 into a term involving eval_left and eval_right and an "extra" bit, 410 pushes the existential in over the former pair, and then uses an 411 appropriate rewrite from OmegaTheory. The right choice of rewrite 412 is specified through the parameter cty. 413 ---------------------------------------------------------------------- *) 414 415datatype ctype = VACUOUS_LOW | VACUOUS_UP | EXACT_LOW | EXACT_UP 416 | NIGHTMARE of (term * term list) 417(* the nightmare constructor takes a pair as an argument: 418 * the term is of type ``:num``, corresponding to 419 the maximum coefficient of the variable to be eliminated in an 420 upper bound constraint 421 * the list of terms is a list of other existentially quantified 422 variables that have scope over this clause *) 423 424fun apply_fmve ctype = let 425 fun initially t = let 426 val (v, body) = dest_exists t 427 in 428 BINDER_CONV (clause_to_evals v) THENC EXISTS_AND_CONV 429 end t 430 431 fun finisher t = let 432 val (v,body) = dest_exists t 433 val (e_ups, e_lows) = dest_conj body 434 val ups = rand e_ups 435 val lows = rand e_lows 436 val ups_nzero = prove_every_fstnzero ups 437 val lows_nzero = prove_every_fstnzero lows 438 in 439 case ctype of 440 VACUOUS_LOW => REWRITE_CONV [evalupper_def] THENC 441 K (EQT_INTRO (MATCH_MP onlylowers_satisfiable lows_nzero)) 442 | VACUOUS_UP => REWRITE_CONV [evallower_def] THENC 443 K (EQT_INTRO (MATCH_MP onlyuppers_satisfiable ups_nzero)) 444 | EXACT_LOW => let 445 val low_fst1 = prove_every_fst1 lows 446 val disj = DISJ2 (list_mk_comb(every_t, [fst1_t, ups])) low_fst1 447 val th = MP (MATCH_MP exact_shadow_case (CONJ ups_nzero lows_nzero)) 448 disj 449 in 450 K th THENC calculate_shadow (alt_rshadow, alt_rrow) 451 end 452 | EXACT_UP => let 453 val up_fst1 = prove_every_fst1 ups 454 val disj = DISJ1 up_fst1 (list_mk_comb(every_t, [fst1_t, lows])) 455 val th = MP (MATCH_MP exact_shadow_case (CONJ ups_nzero lows_nzero)) 456 disj 457 in 458 K th THENC calculate_shadow (alt_rshadow, alt_rrow) 459 end 460 | NIGHTMARE (m,ctxt) => let 461 val uppers_lt_m = prove_every_fst_lt_m m ups 462 in 463 K (MATCH_MP alternative_equivalence 464 (LIST_CONJ [ups_nzero, lows_nzero, uppers_lt_m])) THENC 465 RAND_CONV (RAND_CONV (ALPHA_CONV v)) THENC 466 LAND_CONV (calculate_shadow (alt_dshadow, alt_drow) THENC 467 REWRITE_CONV []) THENC 468 RAND_CONV (calculate_nightmare ctxt) 469 end 470 end t 471 fun elim_rT tm = (if Teq (rand tm) then REWR_CONV CooperThms.T_and_r 472 else ALL_CONV) tm 473in 474 initially THENC LAND_CONV finisher THENC elim_rT 475end 476 477 478(* ---------------------------------------------------------------------- 479 best_variable_to_eliminate vs t 480 481 Given a list of variables vs, and a conjunction of leaves t, pick the 482 variable that should be eliminated. Do this by scanning the term 483 while maintaining a map to information about that variable. 484 ---------------------------------------------------------------------- *) 485 486type varinfo = { maxupc : Arbint.int ref, maxloc : Arbint.int ref, 487 numups : int ref, numlos : int ref } 488fun new_varinfo () : varinfo = 489 { maxupc = ref Arbint.zero, maxloc = ref Arbint.zero, 490 numups = ref 0, numlos = ref 0} 491exception NotFound 492 493fun variable_information vs t = let 494 val table = ref (Redblackmap.mkDict Term.compare) 495 fun ins_initial_recs v = 496 table := Redblackmap.insert (!table, v, new_varinfo()) 497 val _ = app ins_initial_recs vs 498 fun examine_cv t = let 499 val (c, v) = dest_mult t 500 val c_i = int_of_term c 501 in 502 case Redblackmap.peek (!table, v) of 503 NONE => () 504 | SOME {maxupc, maxloc, numups, numlos} => 505 if Arbint.<(c_i, Arbint.zero) then (* upper bound *) 506 (maxupc := Arbint.max(!maxupc, Arbint.~ c_i); 507 numups := !numups + 1) 508 else 509 (maxloc := Arbint.max(!maxloc, c_i); 510 numlos := !numlos + 1) 511 end handle HOL_ERR _ => () 512in 513 app examine_cv (List.concat (map (strip_plus o rand) (strip_conj t))); 514 table 515end 516 517fun findleast gt f l = 518 case l of 519 [] => raise Fail "findleast : empty list" 520 | h::t => let 521 fun recurse (acc as (e, v)) l = 522 case l of 523 [] => (e, v) 524 | h::t => let val v' = f h 525 in 526 if gt(v, v') then recurse (h, v') t 527 else recurse acc t 528 end 529 in 530 recurse (h, f h) t 531 end 532 533fun best_variable_to_eliminate vs t = let 534 val table = variable_information vs t 535 val items = Redblackmap.listItems (!table) 536 fun is_vacuous (_, {numups, numlos,...}) = !numups = 0 orelse !numlos = 0 537 fun is_exact (_, {maxloc, maxupc,...}) = !maxloc = Arbint.one orelse 538 !maxupc = Arbint.one 539in 540 case List.find is_vacuous items of 541 NONE => let 542 val exacts = filter is_exact items 543 in 544 if null exacts then let 545 fun f (_, {maxloc, maxupc, ...}) = Arbint.max(!maxloc, !maxupc) 546 val ((v, {maxupc, ...}), _) = findleast Arbint.> f items 547 in 548 (v, 549 NIGHTMARE (rand (term_of_int (!maxupc)), op_set_diff aconv vs [v])) 550 end 551 else let 552 fun f (_, {numups, numlos,...}) = !numups * !numlos 553 val ((v, {maxupc, maxloc,...}), _) = findleast op> f exacts 554 in 555 (v, if !maxupc = Arbint.one then EXACT_UP else EXACT_LOW) 556 end 557 end 558 | SOME (v, {numups, numlos,...}) => (v, if !numlos = 0 then VACUOUS_UP 559 else VACUOUS_LOW) 560end 561 562 563 564 565(* ---------------------------------------------------------------------- 566 eliminate_an_existential t 567 568 t is of the form ?x1..xn. body, where body is a conjunction of 569 fully normalised leaves. This function picks one of the quantifiers 570 to eliminate, and then does this. 571 ---------------------------------------------------------------------- *) 572 573fun push_nthvar_to_bot n tm = 574 if n <= 0 then TRY_CONV (SWAP_VARS_CONV THENC 575 BINDER_CONV (push_nthvar_to_bot 0)) tm 576 else BINDER_CONV (push_nthvar_to_bot (n - 1)) tm 577 578fun eliminate_an_existential0 t = let 579 val (vs, body) = strip_exists t 580 val (eliminate, category) = best_variable_to_eliminate vs body 581 val v_n = index (aconv eliminate) vs 582 fun check_for_eqs tm = let 583 val (lvs, body) = strip_exists tm 584 in 585 if length lvs = length vs then 586 Profile.profile "eq" OmegaMath.OmegaEq 587 else 588 ALL_CONV 589 end tm 590 fun mypush_in_exs tm = let 591 val (vs, body) = strip_exists tm 592 in 593 CooperSyntax.push_in_exists THENC 594 EVERY_DISJ_CONV (RENAME_VARS_CONV (map (#1 o dest_var) vs) THENC 595 check_for_eqs) 596 end tm 597in 598 push_nthvar_to_bot v_n THENC 599 LAST_EXISTS_CONV (apply_fmve category) THENC 600 mypush_in_exs 601end t 602 603val eliminate_an_existential = 604 TRY_CONV OmegaMath.eliminate_negative_divides THENC 605 EVERY_DISJ_CONV (TRY_CONV OmegaMath.eliminate_positive_divides THENC 606 eliminate_an_existential0) THENC 607 REWRITE_CONV [] 608 609(* ---------------------------------------------------------------------- 610 eliminate_existentials t 611 612 given a normalised term of the form 613 ?x1..xn. body 614 eliminate all of its existentials. 615 ---------------------------------------------------------------------- *) 616 617fun eliminate_existentials tm = 618 if is_exists tm then 619 (eliminate_an_existential THENC 620 EVERY_DISJ_CONV eliminate_existentials) tm 621 else REWRITE_CONV [] tm 622 623 624(* ---------------------------------------------------------------------- 625 sym_normalise tm 626 627 tm is of form 628 ?x1..xn. body 629 where body has no nested quantifiers. Only difference with the 630 normalisation routine in OmegaShell is that we don't automatically 631 eliminate divisibility terms, because we're not necessarily going 632 to be able to. We also have to eliminate equality terms that survive 633 the attempt to get rid of them with OmegaEq. 634 ---------------------------------------------------------------------- *) 635 636fun ISCONST_CONV tm = if is_const tm then ALL_CONV tm else NO_CONV tm 637fun IFEXISTS c tm = if is_exists tm then c tm else ALL_CONV tm 638 639val sym_normalise = let 640 fun push_exs tm = let 641 val vs = map (#1 o dest_var) (#1 (strip_exists tm)) 642 in 643 CooperSyntax.push_in_exists THENC EVERY_DISJ_CONV (RENAME_VARS_CONV vs) 644 end tm 645 open OmegaMath 646 val elim_eq = REWR_CONV (GSYM INT_LE_ANTISYM) THENC 647 RAND_CONV leaf_normalise 648in 649 STRIP_QUANT_CONV (Canon.NNF_CONV leaf_normalise false THENC 650 REPEATC (CHANGED_CONV CSimp.csimp THENC 651 REWRITE_CONV [])) THENC 652 push_exs THENC 653 EVERY_DISJ_CONV (OmegaEq THENC DEPTH_CONV elim_eq THENC 654 TRY_CONV (REWR_CONV EXISTS_SIMP) THENC 655 IFEXISTS 656 (STRIP_QUANT_CONV Canon.PROP_DNF_CONV THENC push_exs)) 657end 658 659 660(* ---------------------------------------------------------------------- 661 find_deep_existentials tm 662 663 ---------------------------------------------------------------------- *) 664 665fun is_bool_binop t = let 666 val (f,args) = strip_comb t 667in 668 length args = 2 andalso is_const f andalso 669 (List.exists (same_const f) [conjunction, disjunction] 670 orelse same_const f equality andalso type_of (hd args) = bool) 671end 672 673fun IFEXISTS c tm = if is_exists tm then c tm else ALL_CONV tm 674 675fun findelim_deep_existential tm = let 676in 677 if is_forall tm then 678 (STRIP_QUANT_CONV findelim_deep_existential) ORELSEC 679 (CooperSyntax.flip_foralls THENC RAND_CONV findelim_deep_existential) 680 else if is_exists tm then 681 (STRIP_QUANT_CONV findelim_deep_existential) ORELSEC 682 (sym_normalise THENC EVERY_DISJ_CONV (IFEXISTS eliminate_an_existential)) 683 else if is_bool_binop tm then 684 (LAND_CONV findelim_deep_existential) ORELSEC 685 (RAND_CONV findelim_deep_existential) 686 else if is_neg tm then 687 RAND_CONV findelim_deep_existential 688 else 689 NO_CONV 690end tm 691 692end (* struct *) 693