1structure CooperCore :> CooperCore = 2struct 3open HolKernel Parse boolLib 4 integerTheory int_arithTheory intReduce 5 intSyntax CooperSyntax CooperMath CooperThms 6 7val ERR = mk_HOL_ERR "CooperCore"; 8 9val lhand = rand o rator 10 11val REWRITE_CONV = GEN_REWRITE_CONV Conv.TOP_DEPTH_CONV bool_rewrites 12 13(* Fix the grammar used by this file *) 14structure Parse :> Parse = struct 15 open Parse 16 val (Type,Term) = parse_from_grammars listTheory.list_grammars 17end 18open Parse 19 20local 21 val prove = INST_TYPE [alpha |-> int_ty] o prove 22 infix THEN 23in 24 25val MEM_base = prove( 26 Term`!e:'a l. MEM e (e::l)`, 27 REWRITE_TAC [listTheory.MEM]); 28val MEM_build = prove( 29 Term`!l1 e1:'a e2. MEM e1 l1 ==> MEM e1 (e2::l1)`, 30 REPEAT STRIP_TAC THEN ASM_REWRITE_TAC [listTheory.MEM]); 31val mem_nilP = prove( 32 ``!P. (?x:'a. MEM x [] /\ P x) = F``, 33 REWRITE_TAC [listTheory.MEM]); 34val mem_singP = prove( 35 ``!P y. (?x:'a. MEM x [y] /\ P x) = P y``, 36 simpLib.SIMP_TAC boolSimps.bool_ss [listTheory.MEM]); 37val mem_consP = prove( 38 ``!P h t. (?x:'a. MEM x (h :: t) /\ P x) = P h \/ (?x. MEM x t /\ P x)``, 39 simpLib.SIMP_TAC boolSimps.bool_ss [listTheory.MEM, RIGHT_AND_OVER_OR, 40 EXISTS_OR_THM]); 41end 42 43fun prove_membership t1 t2 = let 44 val (tmlist, elty) = listSyntax.dest_list t2 45 fun recurse preds thmtodate laters = 46 case (thmtodate, preds, laters) of 47 (NONE, _, []) => raise ERR "prove_membership" "term not found in list" 48 | (NONE, _, x::xs) => 49 if x = t1 then let 50 val tailtm = listSyntax.mk_list(xs, elty) 51 val whole_list = listSyntax.mk_cons(x, tailtm) 52 in 53 recurse preds (SOME (ISPECL [x, tailtm] MEM_base, whole_list)) [] 54 end 55 else 56 recurse (x::preds) NONE xs 57 | (SOME (thm,_), [], _) => thm 58 | (SOME (thm,tmlist), p::ps, _) => let 59 val newlist = listSyntax.mk_cons(p, tmlist) 60 val newthm = MP (ISPECL [tmlist, t1, p] MEM_build) thm 61 in 62 recurse ps (SOME (newthm, newlist)) [] 63 end 64in 65 recurse [] NONE tmlist 66end 67 68fun phase4_CONV tm = let 69 (* have a formula of the form 70 ?x. form 71 where 72 form ::= form /\ form | form \/ form | ~form | leaf 73 and where each leaf either doesn't involve x at all, or is one of 74 the following forms: 75 x < a, 76 b < x, 77 x = a, 78 d int_divides x + u 79 and where all of a, b, u and v are expressions not involving x. 80 *) 81 val {Bvar, Body} = Rsyntax.dest_exists tm 82 val F = rand tm 83 val Fx = mk_comb(F, Bvar) 84 datatype relntype = 85 x_LT of term 86 | LT_x of term 87 | x_EQ of term 88 | DIVIDES of (term * term option) 89 fun rtype_to_term rt = 90 case rt of 91 x_LT t => SOME t 92 | LT_x t => SOME t 93 | x_EQ t => SOME t 94 | _ => NONE 95 val leaf_arguments = let 96 (* traverse the leaves of the term; classifying all those where the 97 Bvar is involved. If 98 x < t then add x_LT t 99 t < x then add LT_x t 100 x = t then add x_EQ t 101 t | x then add DIVIDES(t, NONE) 102 t | x+a then add DIVIDES(t, SOME a) 103 Note that t = x never occur because of normalisation carried out 104 at the end of phase2. 105 106 Pair these with a boolean indicating the parity 107 (true = 0, false = 1) of the number of logical negations passed 108 through to get to the leaf. 109 *) 110 fun recurse posp acc tm = let 111 val (l,r) = dest_disj tm 112 handle HOL_ERR _ => dest_conj tm 113 in 114 recurse posp (recurse posp acc r) l 115 end handle HOL_ERR _ => let 116 val (l,r) = dest_less tm 117 in 118 if l = Bvar then (x_LT r, posp) :: acc 119 else if r = Bvar then (LT_x l, posp) :: acc else acc 120 end handle HOL_ERR _ => let 121 val (l,r) = dest_eq tm 122 in 123 if l = Bvar then (x_EQ r, posp) :: acc else acc 124 end handle HOL_ERR _ => let 125 val (l,r) = dest_divides tm 126 val (first_rhs_arg, rest_rhs) = (I ## SOME) (dest_plus r) 127 handle HOL_ERR _ => (r, NONE) 128 in 129 if first_rhs_arg = Bvar then 130 (DIVIDES (l, rest_rhs), posp) :: acc 131 else acc 132 end handle HOL_ERR _ => (* must be a negation *) 133 recurse (not posp) acc (dest_neg tm) handle HOL_ERR _ => acc 134 in 135 Lib.mk_set (recurse true [] Body) 136 end 137 val use_bis = let 138 fun recurse (ai as (a, afv)) (bi as (b, bfv)) l = 139 case l of 140 [] => (ai, bi) 141 | (x_LT tm, true)::t => recurse (a+1, afv + length (free_vars tm)) bi t 142 | (x_LT tm, false)::t => recurse ai (b+1, bfv + length (free_vars tm)) t 143 | (LT_x tm, true)::t => recurse ai (b+1, bfv + length (free_vars tm)) t 144 | (LT_x tm, false)::t => recurse (a+1, afv + length (free_vars tm)) bi t 145 | _ :: t => recurse ai bi t 146 val ((at,afv), (bt, bfv)) = recurse (0, 0) (0, 0) leaf_arguments 147 in 148 (bt < at) orelse (bt = at andalso bfv < afv) 149 end 150 151 (* need prove either that ?y. !x. x < y ==> (neginf x = F x) or 152 that ?y. !x. y < x ==> (posinf x = F x) 153 depending on the relative numbers of x_LT and LT_x leaves, i.e. 154 our use_bis variable *) 155 val lemma = let 156 val y = genvar int_ty 157 val all_terms = List.mapPartial (rtype_to_term o #1) leaf_arguments 158 val MK_LESS = if use_bis then mk_less else (fn (x,y) => mk_less(y,x)) 159 in 160 if null all_terms then let 161 (* neginf and F are the same *) 162 val without_ex = GEN Bvar (DISCH (MK_LESS(Bvar, y)) (REFL Fx)) 163 in 164 EXISTS (mk_exists(y, concl without_ex), y) without_ex 165 end 166 else let 167 val (minmax_op, minmax_thm, arg_accessor, eqthm_transform) = 168 if use_bis then (min_tm, INT_MIN_LT, rand, I) 169 else (max_tm, INT_MAX_LT, lhand, GSYM) 170 val witness = let 171 fun recurse acc tms = 172 case tms of 173 [] => acc 174 | (x::xs) => recurse (list_mk_comb(minmax_op, [acc, x])) xs 175 in 176 recurse (hd all_terms) (tl all_terms) 177 end 178 fun gen_rewrites acc thm = 179 if is_conj (concl thm) then 180 gen_rewrites (gen_rewrites acc (CONJUNCT1 thm)) (CONJUNCT2 thm) 181 else let 182 val arg = arg_accessor (concl thm) 183 val (hdt, _) = strip_comb arg 184 in 185 if hdt = minmax_op then 186 gen_rewrites acc (MATCH_MP minmax_thm thm) 187 else 188 EQT_INTRO thm :: EQF_INTRO (MATCH_MP INT_LT_GT thm) :: 189 EQF_INTRO (eqthm_transform (MATCH_MP INT_LT_IMP_NE thm)) :: acc 190 end 191 val rewrites = 192 gen_rewrites [] (ASSUME (MK_LESS (Bvar, witness))) 193 val thm0 = 194 (BETA_CONV THENC REWRITE_CONV rewrites THENC UNBETA_CONV Bvar) Fx 195 val thm1 = GEN Bvar (DISCH_ALL thm0) 196 val exform = let 197 val (x, body) = dest_forall (concl thm1) 198 val (_,c) = dest_imp body 199 val newh = MK_LESS(x, y) 200 in 201 mk_exists(y, mk_forall(x, mk_imp(newh, c))) 202 end 203 in 204 EXISTS (exform, witness) thm1 205 end 206 end 207 val neginf = (* call it neginf, though it will be "posinf" if ~ use_bis *) 208 rator (rhs (#2 (dest_imp (#2 (dest_forall 209 (#2 (dest_exists (concl lemma)))))))) 210 211 (* before proceeding, need to calculate the LCM of all the d and e of 212 the above forms, call it delta *) 213 214 val all_delta_tms = let 215 fun collect (DIVIDES(c, _), _) = SOME c 216 | collect _ = NONE 217 in 218 Lib.mk_set (List.mapPartial collect leaf_arguments) 219 end 220 val all_deltas = map int_of_term all_delta_tms 221 val delta = if null all_deltas then Arbint.one else lcml all_deltas 222 val delta_tm = term_of_int delta 223 val divides_info = 224 map (fn ld_tm => 225 (ld_tm, EQT_ELIM (REDUCE_CONV (mk_divides(ld_tm, delta_tm))))) 226 all_delta_tms 227 228 (* further need that !x y. neginf x = neginf (x +/- y * delta_tm) *) 229 (* The argument to neginf only appears as argument to divides terms. 230 We must be able to reduce 231 c int_divides (x +/- y * delta + e) to 232 c int_divides (x + e) 233 given that c is a divisor of delta. We first reduce 234 (x +/- y + e) to (x + e +/- y) 235 using either the theorem move_sub or move_add (proved above). 236 Then we have 237 c int_divides y ==> (c int_divides (x +/- y) = c int_divides x) and 238 c int_divides x ==> c int_divides (x * y) 239 which we specialise with the appropriate values for x and y, and then 240 use rewriting to do the right reductions 241 *) 242 val lemma2 = let 243 val y = genvar int_ty 244 val (tm0, move_thm, divides_thm) = 245 if use_bis then (mk_comb (neginf, mk_minus(Bvar, mk_mult(y, delta_tm))), 246 move_sub, INT_DIVIDES_RSUB) 247 else (mk_comb (neginf, mk_plus(Bvar, mk_mult(y, delta_tm))), 248 move_add, INT_DIVIDES_RADD) 249 fun recurse tm = 250 if is_conj tm orelse is_disj tm then 251 BINOP_CONV recurse tm 252 else if is_neg tm then 253 RAND_CONV recurse tm 254 else let 255 val (local_delta, arg2) = dest_divides tm 256 val (l,r) = dest_plus arg2 257 handle (e as HOL_ERR _) => if use_bis then dest_minus arg2 258 else raise e 259 in 260 if l = Bvar then let 261 (* the original divides term is of form c | x *) 262 val ldel_divides = Lib.assoc local_delta divides_info 263 val ldel_divides_dely = 264 SPEC y (MATCH_MP INT_DIVIDES_RMUL ldel_divides) 265 val ldel_simpler = MATCH_MP divides_thm ldel_divides_dely 266 in 267 REWR_CONV ldel_simpler tm 268 end 269 else let 270 val (ll, lr) = (if use_bis then dest_minus else dest_plus) l 271 val _ = ll = Bvar orelse raise ERR "" "" 272 (* the original divides term of form c | x + e *) 273 (* we're rewriting something like c | (x +/- y * d) + e *) 274 val ldel_divides = Lib.assoc local_delta divides_info 275 val ldel_divides_dely = 276 SPEC y (MATCH_MP INT_DIVIDES_RMUL ldel_divides) 277 val ldel_simpler = MATCH_MP divides_thm ldel_divides_dely 278 in 279 (RAND_CONV (REWR_CONV move_thm) THENC 280 REWR_CONV ldel_simpler) tm 281 end 282 end handle HOL_ERR _ => ALL_CONV tm 283 val c = 284 BETA_CONV THENC recurse THENC UNBETA_CONV Bvar 285 in 286 GENL [y, Bvar] (c tm0) 287 end 288 289 val disj1 = let 290 val i = genvar int_ty 291 val restriction = mk_conj(mk_less(zero_tm, i), 292 mk_leq(i, delta_tm)) 293 in 294 mk_exists(i, mk_conj(restriction, mk_comb(neginf, i))) 295 end 296 297 val (disj2, bis_list_tm) = let 298 (* need all of the bi *) 299 val intlist_ty = mk_thy_type{Args=[int_ty], Tyop="list",Thy="list"} 300 fun find_bi (LT_x t, true) = SOME t 301 | find_bi (x_LT t, false) = SOME (mk_plus(t, mk_negated one_tm)) 302 | find_bi (x_EQ t, true) = SOME (mk_plus(t, mk_negated one_tm)) 303 | find_bi (x_EQ t, false) = SOME t 304 | find_bi _ = NONE 305 fun find_ai (x_LT t, true) = SOME t 306 | find_ai (LT_x t, false) = SOME (mk_plus(t, one_tm)) 307 | find_ai (x_EQ t, true) = SOME (mk_plus(t, one_tm)) 308 | find_ai (x_EQ t, false) = SOME t 309 | find_ai _ = NONE 310 val (find_xi, arith_op) = if use_bis then (find_bi, mk_plus) 311 else (find_ai, mk_minus) 312 val bis = Lib.mk_set (List.mapPartial find_xi leaf_arguments) 313 val bis_list_tm = listSyntax.mk_list(bis, int_ty) 314 val b = genvar int_ty 315 val j = genvar int_ty 316 val brestriction = listSyntax.mk_mem(b, bis_list_tm) 317 val jrestriction = mk_conj(mk_less(zero_tm, j), mk_leq(j, delta_tm)) 318 in 319 (list_mk_exists([b,j], mk_conj(mk_conj(brestriction, jrestriction), 320 mk_comb(F, arith_op(b,j)))), 321 bis_list_tm) 322 end 323 324 (* now must prove that (?x. F x) = disj1 \/ disj2 *) 325 (* first show disj1 ==> (?x. F x) *) 326 327 (* Comments true for use_bis = true. Proof strategy for use_bis = false 328 is the same; we just substitute can_get_big for can_get_small at 329 the crucial moment. 330 331 we have 332 lemma: ?y. !x. x < y ==> (F(x) = neginf(x)) 333 choose y: !x. x < y ==> F(x) = neginf(x) (1) 334 assumption: ?c. (0 < c /\ c <= delta) /\ neginf(c) 335 lemma2: !x y. neginf(x - y * delta) = neginf(x) 336 can_get_small: !x y d. 0 < d ==> ?c. 0 < c /\ y - c * d < x 337 338 need a z such that z < y and neginf(z). Then F(z) will be true. 339 Specialise can_get_small with 340 y, c and delta 341 so 342 0 < delta ==> ?e. 0 < e /\ c - e * delta < y 343 discharge 0 < delta to get 344 ?e. 0 < e /\ c - e * delta < y 345 choose e, take second conjunct 346 c - e * delta < y (2) 347 specialise lemma2 with c, e 348 neginf(c - e * delta) = neginf(c) (3) 349 MATCH_MP (1) and (2) 350 F(c - e * delta) = neginf(c - e * delta) (4) 351 trans with (3) to get 352 F(c - e * delta) = neginf(c) (5) 353 given assumption, 354 F(c - e * delta) (6) 355 so, there exists an x, such that F is true 356 ?x. F x (7) 357 358 *) 359 val zero_lt_delta = EQT_ELIM (REDUCE_CONV (mk_less(zero_tm, delta_tm))) 360 val delta_ok = CONJ zero_lt_delta (SPEC delta_tm INT_LE_REFL) 361 val one_ok = 362 EQT_ELIM (REDUCE_CONV (mk_conj(mk_less(zero_tm, one_tm), 363 mk_leq(one_tm, delta_tm)))) 364 val disj1_implies_exFx = let 365 val (disj1_var, disj1_body) = dest_exists disj1 366 val assumption0 = ASSUME disj1_body 367 val assumption = CONJUNCT2 assumption0 368 val lemma_var = genvar int_ty 369 val thm1 = let 370 val (exvar, lemma_body) = dest_exists (concl lemma) 371 in 372 ASSUME (subst [exvar |-> lemma_var] lemma_body) 373 end 374 val c = rand (concl assumption) 375 val spec_cgs = 376 SPECL [lemma_var, c, delta_tm] (if use_bis then can_get_small 377 else can_get_big) 378 val thm0 = MP spec_cgs zero_lt_delta 379 val e = genvar int_ty 380 val thm2 = let 381 val (v, body) = dest_exists (concl thm0) 382 in 383 CONJUNCT2 (ASSUME (subst [v |-> e] body)) 384 end 385 val thm3 = SPECL [e,c] lemma2 386 val thm4 = MATCH_MP thm1 thm2 387 val thm5 = TRANS thm4 thm3 388 val thm6 = EQ_MP (SYM thm5) assumption 389 val thm7 = EXISTS (tm, rand (concl thm6)) (CONV_RULE BETA_CONV thm6) 390 in 391 CHOOSE(disj1_var, ASSUME disj1) 392 (CHOOSE (lemma_var, lemma) 393 (CHOOSE(e, thm0) thm7)) 394 end 395 396 (* now need to prove that disj2 implies ?x. F x -- this is much 397 simpler, because each disjunct of disj2 is just about an instance 398 of F c *) 399 400 val disj2_implies_exFx = let 401 val (disj2_vars, disj2_body) = strip_exists disj2 402 val assumption0 = ASSUME disj2_body 403 val assumption = CONJUNCT2 assumption0 404 val thm0 = 405 EXISTS(tm, rand(concl assumption)) (CONV_RULE BETA_CONV assumption) 406 val (b,j) = (hd disj2_vars, hd (tl disj2_vars)) 407 in 408 CHOOSE(b, ASSUME disj2) 409 (CHOOSE (j, ASSUME (mk_exists(j, disj2_body))) thm0) 410 end 411 val rhs_implies_exFx = 412 DISCH_ALL (DISJ_CASES (ASSUME(mk_disj(disj1, disj2))) 413 disj1_implies_exFx disj2_implies_exFx) 414 415 (* to do the proof of exFx implies rhs, reason as follows: 416 F x0 (choose_x) 417 specialise excluded middle to get 418 disj2 \/ ~disj2 (disj2_exm) 419 then 420 disj2 |- disj2 421 allows 422 disj2 |- disj1 \/ disj2 (positive_disj2) 423 424 with the other case, (not_disj2) we want to prove that 425 !x. F x ==> F (x - delta) 426 427 first rewrite not_disj2 with NOT_EXISTS_CONV twice and then 428 tautLib.TAUT_PROVE ``~(p /\ q) = p ==> ~q``. This will generate 429 not_thm: 430 |- !b j. MEM b [b1; b2; .. bn] /\ 0 < j /\ j <= delta ==> 431 ~F(b + j) 432 433 so, ASSUME 434 F x |- F x (fx_thm) 435 436 expand out F(x - delta) (i.e. do a BETA_CONV) and traverse this 437 and F(x) in parallel. This is a recursive procedure that takes 438 a F(x) theorem and a F(x - delta) term and produces a theorem 439 with the second term as its conclusion 440 441 Recursive cases are as follows: 442 if is_conj thm then 443 CONJ (recurse (CONJUNCT1 thm) (#1 (dest_conj tm))) 444 (recurse (CONJUNCT2 thm) (#2 (dest_conj tm))) 445 else if is_disj thm then let 446 val (d1_thm0, d2_thm0) = (ASSUME ## ASSUME) (dest_disj (concl thm)) 447 val (d1_tm, d2_tm) = dest_disj tm 448 val d1_thm = recurse d1_thm0 d1_tm 449 val d2_thm = recurse d2_thm0 d2_tm 450 in 451 DISJ_CASES thm d1_thm d2_thm 452 end else if is_neg thm then let 453 val Pxd_tm = dest_neg tm 454 val subres = recurse (ASSUME Pxd_tm) (dest_neg (concl thm)) 455 val false_concl = MP thm subres 456 in 457 EQF_ELIM (DISCH Pxd_tm false_concl) 458 end 459 460 There are seven base cases depending on the form of the term and 461 whether or not we're under a negation; the following are 462 demonstrate what happens when use_bis is true. 463 464 (A) thm = |- x < e 465 tm = x - d < e 466 posp = true 467 468 0 < d (zero_lt_delta) 469 specialise INT_LT_ADD2 with x, e, 0, d to get 470 x < e /\ 0 < d ==> x + 0 < e + d 471 discharge with conjunction of thm and zero_lt_delta to get 472 x + 0 < e + d 473 CONV_RULE (RATOR_CONV (RAND_CONV (REWR_CONV INT_ADD_RID))) to get 474 x < e + d 475 CONV_RULE (REWR_CONV (GSYM INT_LT_SUB_RADD)) to get 476 x - d < e 477 as required 478 479 (B) thm = |- x - d < e 480 tm = |- x < e 481 posp = false 482 483 e + ~1 is one of the bi terms 484 485 ASSUME ~tm 486 |- ~(x < e) 487 REWR_CONV with not_less 488 |- e < x + 1 489 REWR_CONV with (GSYM INT_LT_ADDNEG2) 490 |- e + ~1 < x (lowbound) 491 REWR_CONV thm with less_to_leq_samel 492 |- x - d <= e + ~1 493 REWR_CONV with INT_LE_SUB_RADD 494 |- x <= (e + ~1) + d (highbound) 495 REWR_CONV (lowbound /\ highbound) with in_additive_range 496 |- ?j. (x = (e + ~1) + j) /\ 0 < j /\ j <= d 497 choose j take conjuncts 498 |- (x = (e + ~1) + j) (conj1) 499 |- 0 < j /\ j <= d (conj2) 500 prove e + ~1 in list of bis (membership) 501 match not_thm with membership /\ conj2 502 |- ~P((e + ~1) + j) (notP) 503 AP_TERM P conj1 504 |- P(x) = P((e + ~1) + j) 505 EQ_TRANS with fx_thm 506 |- P((e + ~1) + j) 507 MP with notP 508 |- F 509 CCONTR tm 510 |- x < e as required 511 512 (C) thm = |- e < x 513 tm = e < x - d 514 posp = true 515 516 ASSUME ~tm 517 ... |- ~(e < x - d) (not_tm) 518 REWR_CONV with INT_NOT_LT 519 |- x - d <= e 520 REWR_CONV with INT_LE_SUB_RADD 521 |- x <= e + d (var_leq) 522 REWR_CONV (thm /\ var_leq) with in_additive_range 523 |- ?j. (x = e + j) /\ 0 < j /\ j <= d (exists_j) 524 525 demonstrate that e is in the list of bis, 526 |- MEM e [b1; b2; ... bn] (membership) 527 choose j from exists_j and take conjunct1 528 |- x = e + j (var_eq) 529 and conjunct2 530 |- 0 < j /\ j <= d (j_in_range) 531 match not_thm with membership /\ j_in_range 532 |- ~F(e + j) 533 EQF_INTRO 534 |- F(e + j) = F (not_fej) 535 AP_TERM F (var_eq) 536 |- F(x) = F(e + j) (fx_eq_fej) 537 TRANS fx_eq_fej not_fej 538 |- F(x) = F (fx_eq_F) 539 EQ_MP fx_thm fx_eq_F 540 |- F 541 CCONTR tm 542 |- e < x - d as required 543 544 (D) thm = |- e < x - d 545 tm = |- e < x 546 posp = false 547 548 549 |- 0 < d (zero_lt_delta) 550 REWR_CONV (GSYM INT_NEG_LT0) 551 |- ~d < 0 (part2) 552 REWR_CONV INT_LT_SUB_LADD thm 553 |- e + d < x (part1) 554 MATCH_MP INT_LT_ADD2 (part1 /\ part2) 555 |- e + d + ~d < x + 0 556 CONV_RULE (LAND_CONV (REWR_CONV (GSYM INT_ADD_ASSOC))) 557 |- e + (d + ~d) < x + 0 558 CONV_RULE (LAND_CONV (RAND_CONV (REWR_CONV INT_ADD_RINV))) 559 |- e + 0 < x + 0 560 CONV_RULE (BINOP_CONV (REWR_CONV INT_ADD_RID)) 561 |- e < x 562 563 (E) 564 565 thm = |- x = e 566 tm = x - d = e 567 posp = true 568 569 given our assumption, the thm is an impossibility 570 straightaway. 571 572 specialise not_thm with e + ~1 and 1 to get 573 |- MEM (e + ~1) [...] /\ 0 < 1 /\ 1 <= d ==> 574 ~F(e + ~1 + 1) (spec_not_thm) 575 prove e + ~1 is in list of bis 576 |- MEM (e + ~1) [b1; b2; ... bn] (membership) 577 prove arithmetics of 1 with REDUCE_CONV 578 |- 0 < 1 /\ 1 <= d (one_ok) 579 match membership /\ one_ok against spec_not_thm to get 580 |- ~F(e + ~1 + 1) (not_f_11) 581 EQF_INTRO not_f_11 582 |- F (e + ~1 + 1) = F (f_11_eqF) 583 SYM (SPEC e elim_neg_ones) 584 |- e = e + ~1 + 1 (e_eq_11) 585 TRANS thm e_eq_11 586 |- x = e + ~1 + 1 (x_eq_11) 587 AP_TERM F x_eq_11 588 |- F(x) = F(e + ~1 + 1) (Fx_eq_Fe_11) 589 TRANS Fx_eq_Fe_11 f_11_eqF 590 |- F(x) = F (Fx_eq_F) 591 EQ_MP fx_thm Fx_eq_F 592 |- F 593 CONTR tm 594 |- x - d = e as required 595 596 (F) 597 thm = |- x - d = e 598 tm = x = e 599 posp = false 600 601 e is in bis list 602 603 thm 604 |- x - d = e (xlessd_eq_e) 605 CONV_RULE (REWR_CONV INT_EQ_SUB_RADD) 606 |- x = e + d (x_eq_ed) 607 SPECL [e, d] not_thm 608 |- MEM e [...] /\ 0 < d /\ 1 <= d ==> 609 ~F(e + d) (spec_not_thm) 610 prove e is in list of bis 611 |- MEM e [b1;b2;... bn] (membership) 612 MP spec_not_thm (CONJ membership delta_ok) 613 |- ~F(e + d) (not_fed) 614 EQF_INTRO not_fed 615 |- F(e + d) = F (fed_eq_f) 616 AP_TERM F x_eq_ed 617 |- F(x) = F(e + d) (fx_eq_fed) 618 TRANS fx_eq_fed fed_eq_f 619 |- F(x) = F (fx_eq_f) 620 EQ_MP fx_thm fx_eq_f 621 |- F 622 CCONTR tm 623 |- x = e 624 625 (G) 626 627 thm = |- f int_divides (x + e) 628 tm = f int_divides (x - d + e) 629 posp = _ 630 631 specialise INT_DIVIDES_RMUL and match with divides_info 632 theorem that f int_divides d to get 633 f int_divides (c * d) 634 specialise INT_DIVIDES_RSUB to get 635 f int_divides (c * d) ==> 636 (f int_divides (x + e) - (c * d) = f int_divides (x + e)) 637 match two preceding and GSYM to get 638 f int_divides (x + e) = f int_divides (x + e) - c * d 639 and if C) then EQ_MP this thm to get result. 640 else if D) EQ_MP (AP_TERM ``~`` this) thm to get result 641 642 643 *) 644 645 val exFx_implies_rhs = let 646 val disj2_exm = SPEC disj2 EXCLUDED_MIDDLE 647 val positive_disj2 = DISJ2 disj1 (ASSUME disj2) 648 exception UnexpectedTerm of term 649 val fx_goes_downward = let 650 (* to prove either ~disj2 |- !x. F x ==> F (x - d) (use_bis) or 651 ~disj2 |- !x. F x ==> F (x + d) (~use_bis) *) 652 val not_disj2_0 = mk_neg disj2 653 val not_disj2_thm = ASSUME not_disj2_0 654 val not_thm = 655 CONV_RULE (NOT_EXISTS_CONV THENC 656 BINDER_CONV NOT_EXISTS_CONV THENC 657 STRIP_QUANT_CONV (REWR_CONV NOT_AND_IMP)) 658 not_disj2_thm 659 val fx_thm = ASSUME (mk_comb(F, Bvar)) 660 val fx_thm_expanded = CONV_RULE BETA_CONV fx_thm 661 fun arecurse posp thm tm = let 662 val thm_concl = concl thm 663 in let 664 val (c1, c2) = dest_conj tm 665 in 666 CONJ (arecurse posp (CONJUNCT1 thm) c1) 667 (arecurse posp (CONJUNCT2 thm) c2) 668 end handle HOL_ERR _ => let 669 val (d1_thm0, d2_thm0) = (ASSUME ## ASSUME) (dest_disj thm_concl) 670 val (d1_tm, d2_tm) = dest_disj tm 671 val d1_thm = DISJ1 (arecurse posp d1_thm0 d1_tm) d2_tm 672 val d2_thm = DISJ2 d1_tm (arecurse posp d2_thm0 d2_tm) 673 in 674 DISJ_CASES thm d1_thm d2_thm 675 end handle HOL_ERR _ => let 676 val Pxd_tm = dest_neg tm 677 val subres = arecurse (not posp) (ASSUME Pxd_tm) (dest_neg (concl thm)) 678 val false_concl = MP thm subres 679 in 680 NOT_INTRO (DISCH Pxd_tm false_concl) 681 end handle HOL_ERR _ => let 682 val (lthm,rthm) = dest_less thm_concl 683 val (ltm, rtm) = dest_less tm 684 in 685 (* base cases with less as operator *) 686 if posp then (* thm is positive instance *) 687 if lthm = Bvar then let 688 (* x < e - want to prove that x + d < e 689 do it by contradiction *) 690 val e = rthm 691 val not_tm = ASSUME (mk_neg tm) 692 val leq_var = CONV_RULE (REWR_CONV INT_NOT_LT THENC 693 REWR_CONV (GSYM INT_LE_SUB_RADD)) not_tm 694 (* ~(x + d < e) --> e <= x + d --> e - d <= x *) 695 val exists_j0 = 696 CONV_RULE (REWR_CONV in_subtractive_range) (CONJ leq_var thm) 697 val exists_j = 698 EQ_MP (GEN_ALPHA_CONV (genvar int_ty) (concl exists_j0)) 699 exists_j0 700 (* ?j. (x = e - j) /\ 0 < j /\ j <= d *) 701 val membership = prove_membership e bis_list_tm 702 val (jvar, jbody) = dest_exists (concl exists_j) 703 val choose_j = ASSUME jbody 704 val (var_eq, j_in_range) = CONJ_PAIR choose_j 705 val not_fej = 706 EQF_INTRO (MATCH_MP not_thm (CONJ membership j_in_range)) 707 val fx_eq_fej = AP_TERM F var_eq 708 val fx_eq_F = TRANS fx_eq_fej not_fej 709 val contradiction = EQ_MP fx_eq_F fx_thm 710 in 711 CCONTR tm (CHOOSE(jvar, exists_j) contradiction) 712 end 713 else if rthm = Bvar then let 714 val e = lthm 715 (* e < x - want to prove e < x + d *) 716 val thm0 = SPECL [e, Bvar, zero_tm, delta_tm] INT_LT_ADD2 717 (* e < x /\ 0 < d ==> e + 0 < x + d *) 718 val thm1 = MP thm0 (CONJ thm zero_lt_delta) 719 (* e + 0 < x + d *) 720 in 721 CONV_RULE (LAND_CONV (REWR_CONV INT_ADD_RID)) thm1 722 end 723 else (* Bvar not present *) thm 724 else (* not posp *) 725 if ltm = Bvar then let 726 (* have x + d < e, want to show x < e *) 727 val negdelta_lt_0 = 728 CONV_RULE (REWR_CONV (GSYM INT_NEG_LT0)) zero_lt_delta 729 val stage0 = 730 MATCH_MP INT_LT_ADD2 (CONJ thm negdelta_lt_0) 731 (* (x + d) + ~d < e + 0 *) 732 val stage1 = 733 CONV_RULE (LAND_CONV (REWR_CONV (GSYM INT_ADD_ASSOC))) stage0 734 (* x + (d + ~d) < e + 0 *) 735 val stage2 = 736 CONV_RULE (LAND_CONV (RAND_CONV (REWR_CONV INT_ADD_RINV))) stage1 737 (* x + 0 < e + 0 *) 738 in 739 CONV_RULE (BINOP_CONV (REWR_CONV INT_ADD_RID)) stage2 740 end 741 else if rtm = Bvar then let 742 val e = ltm 743 (* have e < x + d, want to show e < x -- by contradiction *) 744 val not_tm = ASSUME (mk_neg tm) 745 (* |- ~(e < x) *) 746 val x_lt_e1 = CONV_RULE (REWR_CONV not_less) not_tm 747 (* |- x < e + 1 *) 748 val e1_leq_xd = CONV_RULE (REWR_CONV less_to_leq_samer) thm 749 (* |- e + 1 <= x + d *) 750 val e1d_leq_x = 751 CONV_RULE (REWR_CONV (GSYM INT_LE_SUB_RADD)) e1_leq_xd 752 (* |- (e + 1) - d <= x *) 753 val exists_j0 = 754 CONV_RULE (REWR_CONV in_subtractive_range) 755 (CONJ e1d_leq_x x_lt_e1) 756 val exists_j = 757 EQ_MP (GEN_ALPHA_CONV (genvar int_ty) (concl exists_j0)) 758 exists_j0 759 (* ?j. (x = e + 1 - j) /\ 0 < j /\ j <= d *) 760 val membership = prove_membership (mk_plus(e,one_tm)) bis_list_tm 761 val (jvar, jbody) = dest_exists (concl exists_j) 762 val choose_j = ASSUME jbody 763 val (var_eq, j_in_range) = CONJ_PAIR choose_j 764 val not_fej = MATCH_MP not_thm (CONJ membership j_in_range) 765 val fej = EQ_MP (AP_TERM F var_eq) fx_thm 766 in 767 CCONTR tm (CHOOSE(jvar, exists_j) (MP not_fej fej)) 768 end 769 else (* Bvar not present *) thm 770 end handle HOL_ERR _ => let 771 val (lthm,rthm) = dest_eq thm_concl 772 val (ltm, rtm) = dest_eq tm 773 in 774 if posp then 775 if lthm = Bvar then let 776 (* x = e *) 777 val e = rthm 778 val e_plus_1 = mk_plus(e, one_tm) 779 val spec_not_thm = SPECL [e_plus_1, one_tm] not_thm 780 (* MEM (e + 1) [....; e + 1] /\ 0 < 1 /\ 1 <= d ==> 781 ~F(e + 1 - 1) *) 782 val membership = prove_membership e_plus_1 bis_list_tm 783 val not_fe1 = MP spec_not_thm (CONJ membership one_ok) 784 val fe1_eqF = EQF_INTRO not_fe1 785 (* F(e + 1 - 1) = false *) 786 val e_eq_e11 = SYM (SPEC e elim_minus_ones) 787 (* e = e + 1 - 1 *) 788 val x_eq_e11 = TRANS thm e_eq_e11 789 (* x = e + 1 - 1 *) 790 val Fx_eq_Fe11 = AP_TERM F x_eq_e11 791 (* F x = F(e + 1 - 1) *) 792 val Fx_eq_F = TRANS Fx_eq_Fe11 fe1_eqF 793 in 794 CONTR tm (EQ_MP Fx_eq_F fx_thm) 795 end 796 else (* Bvar not present *) 797 thm 798 else (* not posp *) 799 if ltm = Bvar then let 800 (* have x + d = e, want x = e *) 801 val e = rtm 802 val xplusd_eq_e = thm 803 val x_eq_elessd = 804 EQ_MP (SYM (SPECL [Bvar,e,delta_tm] INT_EQ_SUB_LADD)) xplusd_eq_e 805 (* x = e - d *) 806 val F_elessd = EQ_MP (AP_TERM F x_eq_elessd) fx_thm 807 val spec_not_thm = SPECL [e, delta_tm] not_thm 808 val membership = prove_membership e bis_list_tm 809 val not_F_elessd = MP spec_not_thm (CONJ membership delta_ok) 810 in 811 CCONTR tm (MP not_F_elessd F_elessd) 812 end 813 else (* Bvar not present *) thm 814 end handle HOL_ERR _ => let 815 val (c,r) = dest_divides (if posp then thm_concl else tm) 816 val (var, rem) = (I ## SOME) (dest_plus r) 817 handle HOL_ERR _ => (r, NONE) 818 in 819 if var = Bvar then let 820 (* c | x [+ rem] - want to show that c | x + d [ + rem ] *) 821 val c_div_d = Lib.assoc c divides_info 822 val c_div_rplusd0 = 823 SYM (MP (SPECL [c,delta_tm,r] INT_DIVIDES_RADD) c_div_d) 824 (* c | x [+ rem] = c | x [+ rem] + d *) 825 val c_div_rplusd1 = 826 if isSome rem then 827 CONV_RULE (RAND_CONV 828 (RAND_CONV (REWR_CONV move_add))) c_div_rplusd0 829 else c_div_rplusd0 830 val c_div_rplusd = if posp then c_div_rplusd1 else SYM c_div_rplusd1 831 in 832 EQ_MP c_div_rplusd thm 833 end 834 else thm 835 end handle HOL_ERR _ => 836 if is_constraint tm then thm 837 else raise UnexpectedTerm tm 838 end (* need double end, because of double let at start of function *) 839 840 fun brecurse posp thm tm = let 841 val thm_concl = concl thm 842 in let 843 val (c1, c2) = dest_conj tm 844 in 845 CONJ (brecurse posp (CONJUNCT1 thm) c1) 846 (brecurse posp (CONJUNCT2 thm) c2) 847 end handle HOL_ERR _ => let 848 val (d1_thm0, d2_thm0) = (ASSUME ## ASSUME) (dest_disj (concl thm)) 849 val (d1_tm, d2_tm) = dest_disj tm 850 val d1_thm = DISJ1 (brecurse posp d1_thm0 d1_tm) d2_tm 851 val d2_thm = DISJ2 d1_tm (brecurse posp d2_thm0 d2_tm) 852 in 853 DISJ_CASES thm d1_thm d2_thm 854 end handle HOL_ERR _ => let 855 val Pxd_tm = dest_neg tm 856 val subres = brecurse (not posp) (ASSUME Pxd_tm) (dest_neg (concl thm)) 857 val false_concl = MP thm subres 858 in 859 NOT_INTRO (DISCH Pxd_tm false_concl) 860 end handle HOL_ERR _ => let 861 val (lthm,rthm) = dest_less thm_concl 862 val (ltm, rtm) = dest_less tm 863 in 864 (* base cases with less as operator *) 865 if posp then 866 if lthm = Bvar then let 867 (* x < e *) 868 val e = rthm 869 val thm0 = SPECL [Bvar, e, zero_tm, delta_tm] INT_LT_ADD2 870 val thm1 = MP thm0 (CONJ thm zero_lt_delta) 871 val thm2 = 872 CONV_RULE (LAND_CONV (REWR_CONV INT_ADD_RID)) thm1 873 in 874 CONV_RULE (REWR_CONV (GSYM INT_LT_SUB_RADD)) thm2 875 end 876 else if rthm = Bvar then let 877 (* e < x *) 878 val e = lthm 879 val not_tm = ASSUME (mk_neg tm) 880 val var_leq = CONV_RULE (REWR_CONV INT_NOT_LT THENC 881 REWR_CONV INT_LE_SUB_RADD) not_tm 882 val exists_j0 = 883 CONV_RULE (REWR_CONV in_additive_range) (CONJ thm var_leq) 884 val exists_j = 885 EQ_MP (GEN_ALPHA_CONV (genvar int_ty) (concl exists_j0)) 886 exists_j0 887 val membership = prove_membership e bis_list_tm 888 (* choose j from exists_j *) 889 val (jvar, jbody) = dest_exists (concl exists_j) 890 val choose_j = ASSUME jbody 891 val (var_eq, j_in_range) = CONJ_PAIR choose_j 892 val not_fej = 893 EQF_INTRO (MATCH_MP not_thm (CONJ membership j_in_range)) 894 val fx_eq_fej = AP_TERM F var_eq 895 val fx_eq_F = TRANS fx_eq_fej not_fej 896 val contradiction = EQ_MP fx_eq_F fx_thm 897 in 898 CCONTR tm (CHOOSE(jvar, exists_j) contradiction) 899 end 900 else (* Bvar not present *) thm 901 else (* not posp *) 902 if ltm = Bvar then let 903 val e = rtm 904 (* have x - d < e, want x < e - by contradiction *) 905 val not_tm = ASSUME (mk_neg tm) 906 val e_less_x1 = CONV_RULE (REWR_CONV not_less) not_tm 907 (* e < x + 1 *) 908 val lobound = CONV_RULE (REWR_CONV (GSYM INT_LT_ADDNEG2)) e_less_x1 909 (* e + ~1 < x *) 910 val xd_leq_e1 = CONV_RULE (REWR_CONV less_to_leq_samel) thm 911 (* x - d <= e + ~1 *) 912 val hibound = CONV_RULE (REWR_CONV INT_LE_SUB_RADD) xd_leq_e1 913 (* x <= e + ~1 + d *) 914 val exists_j0 = 915 CONV_RULE (REWR_CONV in_additive_range) (CONJ lobound hibound) 916 val exists_j = 917 EQ_MP (GEN_ALPHA_CONV (genvar int_ty) (concl exists_j0)) 918 exists_j0 919 val membership = 920 prove_membership (mk_plus(e,mk_negated one_tm)) bis_list_tm 921 val (jvar, jbody) = dest_exists (concl exists_j) 922 val choose_j = ASSUME jbody 923 val (var_eq, j_in_range) = CONJ_PAIR choose_j 924 val not_fej = MATCH_MP not_thm (CONJ membership j_in_range) 925 val fej = EQ_MP (AP_TERM F var_eq) fx_thm 926 in 927 CCONTR tm (CHOOSE(jvar, exists_j) (MP not_fej fej)) 928 end 929 else if rtm = Bvar then let 930 (* have e < x - d, want e < x *) 931 val ed_lt_x = CONV_RULE (REWR_CONV INT_LT_SUB_LADD) thm 932 (* have e + d < x, want to show e < x *) 933 val negdelta_lt_0 = 934 CONV_RULE (REWR_CONV (GSYM INT_NEG_LT0)) zero_lt_delta 935 val stage0 = 936 MATCH_MP INT_LT_ADD2 (CONJ ed_lt_x negdelta_lt_0) 937 (* (e + d) + ~d < x + 0 *) 938 val stage1 = 939 CONV_RULE (LAND_CONV (REWR_CONV (GSYM INT_ADD_ASSOC))) stage0 940 (* e + (d + ~d) < x + 0 *) 941 val stage2 = 942 CONV_RULE (LAND_CONV (RAND_CONV (REWR_CONV INT_ADD_RINV))) stage1 943 (* e + 0 < x + 0 *) 944 in 945 CONV_RULE (BINOP_CONV (REWR_CONV INT_ADD_RID)) stage2 946 end else (* Bvar not here *) thm 947 end handle HOL_ERR _ => let 948 val (lthm, rthm) = dest_eq thm_concl 949 val (ltm, rtm) = dest_eq tm 950 in 951 if posp then 952 if lthm = Bvar then let 953 (* have x = e, want to show x - d = e *) 954 val e = rtm 955 val e_less1 = mk_plus(e, mk_negated one_tm) 956 val spec_not_thm = SPECL [e_less1, one_tm] not_thm 957 val membership = prove_membership e_less1 bis_list_tm 958 val not_f_11 = MP spec_not_thm (CONJ membership one_ok) 959 val f_11_eqF = EQF_INTRO not_f_11 960 val e_eq_11 = SYM (SPEC e elim_neg_ones) 961 val x_eq_11 = TRANS thm e_eq_11 962 val Fx_eq_Fe_11 = AP_TERM F x_eq_11 963 val Fx_eq_F = TRANS Fx_eq_Fe_11 f_11_eqF 964 in 965 CONTR tm (EQ_MP Fx_eq_F fx_thm) 966 end 967 else thm 968 else (* not posp *) 969 if ltm = Bvar then let 970 (* have x - d = e, want to show x = e *) 971 val e = rthm 972 val xlessd_eq_e = thm 973 val x_eq_ed = CONV_RULE (REWR_CONV INT_EQ_SUB_RADD) xlessd_eq_e 974 val spec_not_thm = SPECL [e, delta_tm] not_thm 975 val membership = prove_membership e bis_list_tm 976 val not_fed = MP spec_not_thm (CONJ membership delta_ok) 977 val fed = EQ_MP (AP_TERM F x_eq_ed) fx_thm 978 in 979 CCONTR tm (MP not_fed fed) 980 end 981 else thm 982 end handle HOL_ERR _ => let 983 val (c,r) = dest_divides (if posp then thm_concl else tm) 984 val (var, rem) = (I ## SOME) (dest_plus r) 985 handle HOL_ERR _ => (r, NONE) 986 in 987 if var = Bvar then let 988 (* c | x [+ rem] - want to show that c | x + d [ + rem ] *) 989 val c_div_d = Lib.assoc c divides_info 990 val c_div_rsubd0 = 991 MP (SPECL [c,delta_tm,r] INT_DIVIDES_RSUB) c_div_d 992 (* c | x [+ rem] = c | x [+ rem] + d *) 993 val c_div_rsubd1 = 994 if isSome rem then 995 CONV_RULE (LAND_CONV 996 (RAND_CONV (REWR_CONV (GSYM move_sub)))) c_div_rsubd0 997 else c_div_rsubd0 998 val c_div_rsubd = if posp then SYM c_div_rsubd1 else c_div_rsubd1 999 in 1000 EQ_MP c_div_rsubd thm 1001 end 1002 else thm 1003 end handle HOL_ERR _ => 1004 if is_constraint tm then thm 1005 else raise UnexpectedTerm tm 1006 end (* again need a double end *) 1007 1008 1009 val (arith_op, recurse) = 1010 if use_bis then (mk_minus, brecurse) else (mk_plus, arecurse) 1011 val fxd_beta_thm = BETA_CONV (mk_comb(F, arith_op(Bvar, delta_tm))) 1012 val fxd_tm = rhs (concl fxd_beta_thm) 1013 val fxd_thm = recurse true fx_thm_expanded fxd_tm 1014 handle UnexpectedTerm tm => 1015 raise ERR "phase4_CONV" 1016 ("Unexpected term: "^term_to_string tm) 1017 in 1018 GEN Bvar (DISCH Fx (EQ_MP (SYM fxd_beta_thm) fxd_thm)) 1019 end 1020 val x0 = genvar int_ty 1021 val Fx0 = mk_comb(F, x0) 1022 val Fx0_thm = ASSUME Fx0 1023 val (change_by_dmultiples, can_become_extreme, change_to_extreme) = 1024 if use_bis then 1025 (MP (SPECL [F, delta_tm, x0] top_and_lessers) 1026 (CONJ fx_goes_downward Fx0_thm), 1027 can_get_small, 1028 subtract_to_small) 1029 else 1030 (MP (SPECL [F, delta_tm, x0] bot_and_greaters) 1031 (CONJ fx_goes_downward Fx0_thm), can_get_big, 1032 add_to_great) 1033 (* this looks like: .. |- !c. 0 < c ==> F (x0 - c * d) *) 1034 (* further have lemma: 1035 |- ?y. !x. x < y ==> (F x = neginf x) 1036 and lemma2: |- !c x. neginf (x - c * d) = neginf x 1037 and can_get_small: |- !x y d. 0 < d ==> ?c. 0 < c /\ y - c * d < x 1038 1039 so, choose a y for lemma 1040 (choose_lemma) . |- !x. x < y ==> (F x = neginf x) 1041 *) 1042 val y = genvar int_ty 1043 val choose_lemma = let 1044 val (exvar, exbody) = dest_exists (concl lemma) 1045 in 1046 ASSUME (subst [exvar |-> y] exbody) 1047 end 1048 (* 1049 specialise can_get_small with [y, x0, d] and MP with zero_lt_delta 1050 (little_c_ex) |- ?c. 0 < c /\ x0 - c * d < y 1051 *) 1052 val little_c_ex = 1053 MP (SPECL [y, x0, delta_tm] can_become_extreme) zero_lt_delta 1054 (* 1055 choose a u for little c 1056 (choose_u) . |- 0 < u /\ x0 - u * d < y 1057 conjunct1 1058 (zero_lt_u) . |- 0 < u 1059 conjunct2 1060 (x0_less_ud) . |- x0 - u * d < y 1061 *) 1062 val u = genvar int_ty 1063 val choose_u = let 1064 val (exvar, exbody) = dest_exists (concl little_c_ex) 1065 in 1066 ASSUME (subst [exvar |-> u] exbody) 1067 end 1068 val zero_lt_u = CONJUNCT1 choose_u 1069 val x0_less_ud = CONJUNCT2 choose_u 1070 (* 1071 SPEC change_by_dmultiples with u, and MP with zero_lt_u to get 1072 (Fx0_less_ud) . |- F (x0 - u * d) 1073 *) 1074 val Fx0_less_ud = MP (SPEC u change_by_dmultiples) zero_lt_u 1075 (* SPEC choose_lemma with x0 - u * d and MP with x0_less_ud to get 1076 (Fneginf_x0_less_ud) . |- F (x0 - u * d) = neginf (x0 - u * d) 1077 *) 1078 val x0_less_ud_tm = if use_bis then lhand (concl x0_less_ud) 1079 else rand (concl x0_less_ud) 1080 val Fneginf_x0_less_ud = 1081 MP (SPEC x0_less_ud_tm choose_lemma) x0_less_ud 1082 (* EQ_MP with Fx0_less_ud to get 1083 (neginf_x0_less_ud) . |- neginf (x0 - u * d) 1084 *) 1085 val neginf_x0_less_ud = EQ_MP Fneginf_x0_less_ud Fx0_less_ud 1086 (* have subtract_to_small 1087 |- !x d. 0 < d ==> 1088 ?k. 0 < x - k * d /\ x - k * d <= d 1089 so specialise this with x0 - u * d and delta_tm, and then MP with 1090 zero_lt_delta to get 1091 (exists_small_k) |- ?k. 0 < x0 - u * d - k * d /\ 1092 x0 - u * d - k * d <= d 1093 *) 1094 val exists_small_k = 1095 MP (SPECL [x0_less_ud_tm, delta_tm] change_to_extreme) zero_lt_delta 1096 (* 1097 choose k, to get 1098 (choose_k) |- 0 < x0 - u * d - k * d /\ x0 - u*d - k*d <= d 1099 *) 1100 val k = genvar int_ty 1101 val choose_k = let 1102 val (exvar, exbody) = dest_exists (concl exists_small_k) 1103 in 1104 ASSUME (subst [exvar |-> k] exbody) 1105 end 1106 val u0_less_crap = rand (rand (rator (concl choose_k))) 1107 val neginf_crap_eq = SPECL [k, x0_less_ud_tm] lemma2 1108 val neginfo_crap = EQ_MP (SYM neginf_crap_eq) neginf_x0_less_ud 1109 val disj1_body = CONJ choose_k neginfo_crap 1110 val disj1_exists = EXISTS(disj1, u0_less_crap) disj1_body 1111 val disj1_or_disj2 = DISJ1 disj1_exists disj2 1112 (* now start discharging the choose obligations *) 1113 val res0 = CHOOSE (k, exists_small_k) disj1_or_disj2 1114 val res1 = CHOOSE (u, little_c_ex) res0 1115 val res2 = CHOOSE (y, lemma) res1 1116 (* and do disj_cases on excluded_middle *) 1117 val res3 = DISJ_CASES disj2_exm positive_disj2 res2 1118 (* choose on x0 to get an existential assumption *) 1119 val res4 = CHOOSE (x0, ASSUME (mk_exists(Bvar, Fx))) res3 1120 in 1121 CONV_RULE (LAND_CONV (BINDER_CONV BETA_CONV)) (DISCH_ALL res4) 1122 end 1123 val thm0 = IMP_ANTISYM_RULE exFx_implies_rhs rhs_implies_exFx 1124 val neginf_constrain = BINDER_CONV (LAND_CONV MK_CONSTRAINT) 1125 val rhs_constrain = BINDER_CONV (LAND_CONV (RAND_CONV MK_CONSTRAINT)) 1126in 1127 CONV_RULE (RAND_CONV (* on rhs *) 1128 (LAND_CONV neginf_constrain THENC 1129 RAND_CONV (BINDER_CONV rhs_constrain))) thm0 1130end 1131 1132(* 1133val phase4_CONV = Profile.profile "phase4" phase4_CONV 1134*) 1135 1136fun LIST_EL_CONV c tm = let 1137 (* applies c to all elements of a literal list tm *) 1138 val (f, args) = strip_comb tm 1139in 1140 case args of 1141 [] => (* nil case *) ALL_CONV tm 1142 | h::t => (* h the element, t the tail of the list *) 1143 (LAND_CONV c THENC RAND_CONV (LIST_EL_CONV c)) tm 1144end 1145 1146 1147fun in_list_CONV tm = let 1148 val (v, body) = dest_exists tm 1149 val (mem_t, _) = dest_conj body 1150 val (_, list_t) = listSyntax.dest_mem mem_t 1151 1152 fun recurse tm = let 1153 val (v, body) = dest_exists tm 1154 val (mem_t, _) = dest_conj body 1155 val (_, list_t) = listSyntax.dest_mem mem_t 1156 (* mem_t = MEM v l and l is not nil, so list_t = CONS h t *) 1157 in 1158 if is_const (rand list_t) then REWR_CONV mem_singP 1159 else REWR_CONV mem_consP THENC RAND_CONV recurse 1160 end tm 1161in 1162 if is_const list_t (* i.e. = [] *) then REWR_CONV mem_nilP tm 1163 else recurse tm 1164end 1165 1166 1167 1168fun elim_bterms tm = let 1169 (* tm is of form 1170 ?b. (MEM b list /\ K ... j) /\ f (b + j) 1171 or 1172 ?b. MEM b list /\ f (b + j) 1173 *) 1174 val (var, body) = dest_exists tm 1175 val initially = if is_conj (lhand body) then REWR_CONV (GSYM CONJ_ASSOC) 1176 else ALL_CONV 1177in 1178 BINDER_CONV (RAND_CONV BETA_CONV THENC initially THENC 1179 (*Profile.profile "eb.abs"*) (RAND_CONV (UNBETA_CONV var))) THENC 1180 (*Profile.profile "eb.in_list"*) in_list_CONV THENC 1181 (*Profile.profile "eb.beta"*) (EVERY_DISJ_CONV (TRY_CONV BETA_CONV)) 1182end tm 1183 1184 1185 1186 1187 1188val phase5_CONV = let 1189 (* have something of the form 1190 (?x. K (0 < x /\ x <= k) x /\ neginf x) \/ 1191 (?b k. (MEM b [..] /\ K (0 < k /\ k <= d) k) /\ F (b + k)) 1192 *) 1193 val prelim_left = BINDER_CONV (RAND_CONV BETA_CONV) 1194 val prelim_right = 1195 STRIP_QUANT_CONV 1196 (RAND_CONV (RAND_CONV 1197 (* turn minus terms F (b - k) into F (b + ~1 * k) *) 1198 (fn t => if is_minus t then 1199 (REWR_CONV int_sub THENC 1200 RAND_CONV (REWR_CONV INT_NEG_MINUS1)) t 1201 else ALL_CONV t)) THENC 1202 (* collect additive consts on elements of list *) 1203 LAND_CONV (LAND_CONV (* first conjunct of three *) 1204 (RAND_CONV (* set [...] (from b IN set [..]) *) 1205 (RAND_CONV (* [...] *) 1206 (LIST_EL_CONV 1207 (TRY_CONV collect_additive_consts)))))) 1208 1209 1210 1211 val elim_bterms_on_right = 1212 (* the second disjunct produced by phase4 is of form 1213 ?b k. (MEM b [...] /\ K (lo < k /\ k <= hi) k) /\ F(b + k) *) 1214 (* first try eliminating trivial constraints on k *) 1215 TRY_CONV (STRIP_QUANT_CONV (LAND_CONV (RAND_CONV quick_cst_elim)) THENC 1216 (BINDER_CONV Unwind.UNWIND_EXISTS_CONV ORELSEC 1217 REWRITE_CONV [])) THENC 1218 (* at this stage, k may or may not have been eliminated by the previous 1219 step, either by becoming false, which will have already turned the 1220 whole term false, or by becoming unwound. 1221 In the former, the TRY_CONV will do nothing because the LAND_CONV 1222 will fail. 1223 Otherwise, the basic action here is to expand out all of the 1224 "b" possibilities in the list *) 1225 TRY_CONV (((SWAP_VARS_CONV THENC BINDER_CONV elim_bterms) ORELSEC 1226 elim_bterms) THENC 1227 reduce_if_ground THENC 1228 push_one_exists_over_many_disjs) 1229 (* 1230 val elim_bterms_on_right = Profile.profile "phase5.er" elim_bterms_on_right 1231 *) 1232in 1233 LAND_CONV prelim_left THENC 1234 RAND_CONV (prelim_right THENC elim_bterms_on_right) THENC 1235 EVERY_DISJ_CONV (TRY_CONV fixup_newvar THENC 1236 ONCE_DEPTH_CONV check_divides THENC 1237 TRY_CONV simplify_constrained_disjunct THENC 1238 TRY_CONV (REWR_CONV EXISTS_SIMP)) 1239end 1240 1241(* 1242val phase5_CONV = Profile.profile "phase5" phase5_CONV 1243*) 1244 1245end 1246