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