1(* ========================================================================= *) 2(* Linear decision procedure for the reals, plus some proof procedures. *) 3(* *) 4(* John Harrison, University of Cambridge Computer Laboratory *) 5(* (c) Copyright, University of Cambridge 1998 *) 6(* *) 7(* Ported to hol98 by Joe Hurd, 2 Oct 1998 *) 8(* ========================================================================= *) 9 10 11structure RealArith :> RealArith = 12struct 13 14 15(* 16app load ["Arbint", 17 "reduceLib", 18 "pairTheory", 19 "numLib", 20 "realTheory", 21 "PairedLambda", 22 "tautLib", 23 "Ho_rewrite", 24 "jrhUtils", 25 "Canon_Port", 26 "liteLib", "AC", "numLib" (*goofy*)]; 27*) 28 29open HolKernel Parse boolLib pairLib hol88Lib numLib reduceLib tautLib 30 pairTheory numTheory prim_recTheory arithmeticTheory 31 realTheory Ho_Rewrite jrhUtils Canon_Port AC numSyntax Arbint; 32 33 34(*---------------------------------------------------------------------------*) 35(* Establish the required grammar(s) for executing this file *) 36(*---------------------------------------------------------------------------*) 37 38val ambient_grammars = Parse.current_grammars(); 39val _ = Parse.temp_set_grammars realTheory.real_grammars; 40 41(*----------------------------------------------------------------------- *) 42(* The trace system. *) 43(* ---------------------------------------------------------------------- *) 44 45local 46 open Int 47 val traceval = ref 0 48 49 fun trace_pure s () = print s 50 fun check f = if !traceval > 0 then f() else () 51 infix >> 52 fun (f >> g) () = (f () ; g ()) 53 val _ = register_trace ("RealArith dp", traceval, 1) 54 fun trace_line () = print "\n" 55 local 56 fun tl f [] = (fn () => ()) 57 | tl f [h] = f h 58 | tl f (h::t) = (f h >> trace_pure ", " >> tl f t) 59 in 60 fun trace_list_pure f l () = 61 (trace_pure "[" >> tl f l >> trace_pure "]") () 62 end 63 fun trace_term_pure t () = print (term_to_string t) 64 fun trace_thm_pure t = trace_term_pure (concl t) 65in 66 fun trace s = check (trace_pure (s ^ "\n")) 67 fun trace_term t = check (trace_term_pure t >> trace_line) 68 fun trace_term_list l = 69 check (trace_list_pure trace_term_pure l >> trace_line) 70 fun trace_thm t = check (trace_thm_pure t >> trace_line) 71 fun trace_thm_list l = check (trace_list_pure trace_thm_pure l >> trace_line) 72end; 73 74(* ------------------------------------------------------------------------- *) 75(* Functions to be compatible with hol-light. *) 76(* ------------------------------------------------------------------------- *) 77 78fun failwith s = liteLib.failwith s 79fun fail () = failwith "No message"; 80 81fun term_lt u t = Term.compare(u,t) = LESS 82fun term_le t u = not (term_lt u t); 83 84fun el0 n l = if n <= zero then hd l 85 else el0 (n - one) (tl l) handle _ => raise Fail "RealArith.el0" 86 87fun index x = 88 let 89 fun ind n [] = failwith "index" 90 | ind n (h::t) = if x = h then n else ind (n + one) t 91 in 92 ind zero 93 end 94 95fun index_ac x = let 96 fun ind n [] = failwith "index_ac" 97 | ind n (h::t) = if aconv x h then n else ind (n + one) t 98in 99 ind zero 100end 101 102 103fun remove P [] = failwith "remove" 104 | remove P (h::t) = if P h then (h,t) else 105 let 106 val (e,l) = remove P t 107 in 108 (e, h::l) 109 end; 110 111fun chop_list n l = 112 if n = zero then ([],l) else 113 let 114 val (m,l') = chop_list (n-one) (Lib.trye tl l) 115 in 116 (Lib.trye hd l::m, l') 117 end 118 handle HOL_ERR _ => failwith "chop_list"; 119 120val mk_binop = 121 let 122 fun mk_binop_alt t = curry (liteLib.mk_binop t); 123 in 124 mk_binop_alt 125 end; 126 127fun list_mk_binop op_alt = end_itlist (mk_binop op_alt); 128 129val REFUTE_THEN = 130 let 131 val conv = REWR_CONV(TAUT_PROVE (Term`p = ~p ==> F`)) 132 in 133 fn ttac => CONV_TAC conv THEN DISCH_THEN ttac 134 end; 135 136val PRESIMP_CONV = 137 GEN_REWRITE_CONV DEPTH_CONV 138 [NOT_CLAUSES, AND_CLAUSES, OR_CLAUSES, IMP_CLAUSES, EQ_CLAUSES, 139 FORALL_SIMP, EXISTS_SIMP, EXISTS_OR_THM, FORALL_AND_THM, 140 LEFT_EXISTS_AND_THM, RIGHT_EXISTS_AND_THM, 141 LEFT_FORALL_OR_THM, RIGHT_FORALL_OR_THM]; 142 143val TAUT = TAUT_PROVE; 144 145val NUM_LE_CONV = LE_CONV; 146val NUM_LT_CONV = LT_CONV; 147val NUM_ADD_CONV = ADD_CONV; 148 149(* ------------------------------------------------------------------------- *) 150(* Functions dealing with numbers (numerals) in theorems. *) 151(* ------------------------------------------------------------------------- *) 152 153 154val mk_numeral = mk_numeral o toNat 155val dest_numeral = fromNat o dest_numeral 156 157val amp = Term`(&) :num -> real`; 158 159val is_numconst = 160 fn tm => 161 let 162 val (l,r) = dest_comb tm 163 in 164 l = amp andalso is_numeral r 165 end 166 handle HOL_ERR _ => false; 167 168fun mk_numconst n = mk_comb(amp, mk_numeral n); 169 170fun dest_numconst tm = 171 let 172 val (l,r) = dest_comb tm 173 in 174 if l = amp then 175 dest_numeral r 176 else 177 failwith "dest_numconst" 178 end; 179 180val dsub = Term`$~ :real->real`; 181val is_intconst = 182 fn tm => 183 is_numconst tm orelse 184 let 185 val (l,r) = dest_comb tm 186 in 187 l = dsub andalso is_numconst r 188 end 189 handle HOL_ERR _ => false; 190 191 192fun mk_intconst n = 193 if n < zero then 194 mk_comb(dsub,mk_numconst(~n)) 195 else 196 mk_numconst(n); 197 198fun dest_intconst tm = 199 if (rator tm = dsub handle HOL_ERR _ => false) then 200 ~(dest_numconst(rand tm)) 201 else 202 dest_numconst(tm); 203 204 205(* ------------------------------------------------------------------------- *) 206(* Preparing the real linear decision procedure. *) 207(* ------------------------------------------------------------------------- *) 208 209val LE_0 = arithmeticTheory.ZERO_LESS_EQ; 210val LE = arithmeticTheory.LE; 211val NOT_LE = arithmeticTheory.NOT_LESS_EQUAL; 212val LE_ANTISYM = GSYM arithmeticTheory.EQ_LESS_EQ; 213 214val REAL_ADD_AC_98 = (REAL_ADD_ASSOC, REAL_ADD_SYM); 215 216val REAL_MUL_AC_98 = (REAL_MUL_ASSOC, REAL_MUL_SYM) 217 218val EQ_REFL_T = GEN_ALL (MATCH_MP (TAUT_PROVE (Term`a ==> (a = T)`) ) 219 (SPEC_ALL EQ_REFL)); 220 221val real_abs = realTheory.abs; 222 223val ETA_THM = boolTheory.ETA_THM; 224 225 226val EXISTS_UNIQUE_THM = prove 227 (Term`!P. (?!x:'a. P x) = (?x. P x) /\ (!x x'. P x /\ P x' ==> (x = x'))`, 228 GEN_TAC THEN REWRITE_TAC [EXISTS_UNIQUE_DEF] 229 THEN BETA_TAC THEN BETA_TAC THEN REFL_TAC); 230 231val (NNF_CONV,NNFC_CONV) = 232 let 233 val NOT_EXISTS_UNIQUE_THM = prove 234 (Term`~(?!x:'a. P x) = (!x. ~P x) \/ ?x x'. P x /\ P x' /\ ~(x = x')`, 235 REWRITE_TAC[EXISTS_UNIQUE_THM, DE_MORGAN_THM, NOT_EXISTS_THM] THEN 236 REWRITE_TAC[NOT_FORALL_THM, NOT_IMP, CONJ_ASSOC]) 237 val common_tauts = 238 [TAUT (Term`~~p:bool = p`), 239 TAUT (Term`~(p /\ q) = ~p \/ ~q`), 240 TAUT (Term`~(p \/ q) = ~p /\ ~q`), 241 TAUT (Term`~(p ==> q) = p /\ ~q`), 242 TAUT (Term`p ==> q = ~p \/ q`), 243 NOT_FORALL_THM, 244 NOT_EXISTS_THM, 245 EXISTS_UNIQUE_THM, 246 NOT_EXISTS_UNIQUE_THM] 247 val dnf_tauts = 248 map (TAUT o Term) 249 [`~(p = q) = (p /\ ~q) \/ (~p /\ q)`, 250 `(p = q) = (p /\ q) \/ (~p /\ ~q)`] 251 val cnf_tauts = 252 map (TAUT o Term) 253 [`~(p = q) = (p \/ q) /\ (~p \/ ~q)`, 254 `(p = q) = (p \/ ~q) /\ (~p \/ q)`] 255 val NNF_CONV = 256 GEN_REWRITE_CONV TOP_SWEEP_CONV (common_tauts @ dnf_tauts) 257 val NNFC_CONV = 258 GEN_REWRITE_CONV TOP_SWEEP_CONV (common_tauts @ cnf_tauts) 259 fun SINGLE_SWEEP_CONV conv tm = 260 let 261 val th = conv tm 262 val tm' = rand(concl th) 263 val th' = if is_abs tm' then NNFC_CONV tm' 264 else SUB_CONV (SINGLE_SWEEP_CONV conv) tm' 265 in 266 TRANS th th' 267 end 268 handle HOL_ERR _ => 269 if is_abs tm then NNFC_CONV tm else 270 SUB_CONV (SINGLE_SWEEP_CONV conv) tm 271 in 272 (NNF_CONV, 273 SINGLE_SWEEP_CONV (GEN_REWRITE_CONV I (common_tauts @ dnf_tauts))) 274 end; 275 276val PROP_DNF_CONV = 277 GEN_REWRITE_CONV REDEPTH_CONV 278 [TAUT (Term`a /\ (b \/ c) = (a /\ b) \/ (a /\ c)`), 279 TAUT (Term`(a \/ b) /\ c = (a /\ c) \/ (b /\ c)`), 280 GSYM CONJ_ASSOC, GSYM DISJ_ASSOC]; 281 282(* ------------------------------------------------------------------------- *) 283(* First all the comparison operators. *) 284(* ------------------------------------------------------------------------- *) 285 286val (REAL_INT_LE_CONV,REAL_INT_LT_CONV, 287 REAL_INT_GE_CONV,REAL_INT_GT_CONV,REAL_INT_EQ_CONV) = 288 let 289 val tth = 290 TAUT (Term`(F /\ F = F) /\ (F /\ T = F) /\ (T /\ F = F) /\ (T /\ T = T)`) 291 val nth = TAUT (Term`(~T = F) /\ (~F = T)`) 292 val NUM2_EQ_CONV = 293 liteLib.COMB2_CONV (RAND_CONV NEQ_CONV) NEQ_CONV THENC 294 GEN_REWRITE_CONV I [tth] 295 val NUM2_NE_CONV = 296 RAND_CONV NUM2_EQ_CONV THENC 297 GEN_REWRITE_CONV I [nth] 298 val [pth_le1, pth_le2a, pth_le2b, pth_le3] = (CONJUNCTS o prove) 299 (Term`(~(&m) <= &n = T) /\ 300 (&m <= (&n : real) = m <= n) /\ 301 (~(&m) <= ~(&n) = n <= m) /\ 302 (&m <= ~(&n) = (m = 0) /\ (n = 0))`, 303 REWRITE_TAC[REAL_LE_NEG2] THEN 304 REWRITE_TAC[REAL_LE_LNEG, REAL_LE_RNEG] THEN 305 REWRITE_TAC[REAL_ADD, REAL_OF_NUM_LE, LE_0] THEN 306 REWRITE_TAC[LE, ADD_EQ_0]) 307 val REAL_INT_LE_CONV = FIRST_CONV 308 [GEN_REWRITE_CONV I [pth_le1], 309 GEN_REWRITE_CONV I [pth_le2a, pth_le2b] THENC NUM_LE_CONV, 310 GEN_REWRITE_CONV I [pth_le3] THENC NUM2_EQ_CONV] 311 val [pth_lt1, pth_lt2a, pth_lt2b, pth_lt3] = (CONJUNCTS o prove) 312 (Term`(&m < ~(&n) = F) /\ 313 (&m < (&n :real) = m < n) /\ 314 (~(&m) < ~(&n) = n < m) /\ 315 (~(&m) < &n = ~((m = 0) /\ (n = 0)))`, 316 REWRITE_TAC[pth_le1, pth_le2a, pth_le2b, pth_le3, 317 GSYM NOT_LE, real_lt] THEN 318 CONV_TAC tautLib.TAUT_CONV) 319 val REAL_INT_LT_CONV = FIRST_CONV 320 [GEN_REWRITE_CONV I [pth_lt1], 321 GEN_REWRITE_CONV I [pth_lt2a, pth_lt2b] THENC NUM_LT_CONV, 322 GEN_REWRITE_CONV I [pth_lt3] THENC NUM2_NE_CONV] 323 val [pth_ge1, pth_ge2a, pth_ge2b, pth_ge3] = (CONJUNCTS o prove) 324 (Term`(&m >= ~(&n) = T) /\ 325 (&m >= (&n :real) = n <= m) /\ 326 (~(&m) >= ~(&n) = m <= n) /\ 327 (~(&m) >= &n = (m = 0) /\ (n = 0))`, 328 REWRITE_TAC[pth_le1, pth_le2a, pth_le2b, pth_le3, real_ge] THEN 329 CONV_TAC tautLib.TAUT_CONV) 330 val REAL_INT_GE_CONV = FIRST_CONV 331 [GEN_REWRITE_CONV I [pth_ge1], 332 GEN_REWRITE_CONV I [pth_ge2a, pth_ge2b] THENC NUM_LE_CONV, 333 GEN_REWRITE_CONV I [pth_ge3] THENC NUM2_EQ_CONV] 334 val [pth_gt1, pth_gt2a, pth_gt2b, pth_gt3] = (CONJUNCTS o prove) 335 (Term`(~(&m) > &n = F) /\ 336 (&m > (&n :real) = n < m) /\ 337 (~(&m) > ~(&n) = m < n) /\ 338 (&m > ~(&n) = ~((m = 0) /\ (n = 0)))`, 339 REWRITE_TAC[pth_lt1, pth_lt2a, pth_lt2b, pth_lt3, real_gt] THEN 340 CONV_TAC tautLib.TAUT_CONV) 341 val REAL_INT_GT_CONV = FIRST_CONV 342 [GEN_REWRITE_CONV I [pth_gt1], 343 GEN_REWRITE_CONV I [pth_gt2a, pth_gt2b] THENC NUM_LT_CONV, 344 GEN_REWRITE_CONV I [pth_gt3] THENC NUM2_NE_CONV] 345 val [pth_eq1a, pth_eq1b, pth_eq2a, pth_eq2b] = (CONJUNCTS o prove) 346 (Term`((&m = (&n :real)) = (m = n)) /\ 347 ((~(&m) = ~(&n)) = (m = n)) /\ 348 ((~(&m) = &n) = (m = 0) /\ (n = 0)) /\ 349 ((&m = ~(&n)) = (m = 0) /\ (n = 0))`, 350 REWRITE_TAC[GSYM REAL_LE_ANTISYM, GSYM LE_ANTISYM] THEN 351 REWRITE_TAC[pth_le1, pth_le2a, pth_le2b, pth_le3, LE, LE_0] THEN 352 CONV_TAC tautLib.TAUT_CONV) 353 val REAL_INT_EQ_CONV = FIRST_CONV 354 [GEN_REWRITE_CONV I [pth_eq1a, pth_eq1b] THENC NEQ_CONV, 355 GEN_REWRITE_CONV I [pth_eq2a, pth_eq2b] THENC NUM2_EQ_CONV] 356 in 357 (REAL_INT_LE_CONV,REAL_INT_LT_CONV, 358 REAL_INT_GE_CONV,REAL_INT_GT_CONV,REAL_INT_EQ_CONV) 359 end; 360 361(* ------------------------------------------------------------------------- *) 362(* Negation & multiplication. *) 363(* ------------------------------------------------------------------------- *) 364 365val REAL_INT_NEG_CONV = 366 let 367 val pth = prove 368 (``(~(&0) = &0) /\ 369 (~(~(&x)) = &x)``, 370 REWRITE_TAC[REAL_NEG_NEG, REAL_NEG_0]) 371 in 372 GEN_REWRITE_CONV I [pth] 373 end; 374 375val REAL_INT_MUL_CONV = 376 let 377 val pth0 = prove 378 (``(&0 * (&x :real) = &0) /\ 379 (&0 * ~(&x) = &0) /\ 380 ((&x :real) * &0 = &0) /\ 381 (~(&x :real) * &0 = &0)``, 382 REWRITE_TAC[REAL_MUL_LZERO, REAL_MUL_RZERO]) 383 val (pth1,pth2) = (CONJ_PAIR o prove) 384 (``((&m * &n = &(m * n) :real) /\ 385 (~(&m) * ~(&n) = &(m * n) :real)) /\ 386 ((~(&m) * &n = ~(&(m * n) :real)) /\ 387 (&m * ~(&n) = ~(&(m * n) :real)))``, 388 REWRITE_TAC[REAL_MUL_LNEG, REAL_MUL_RNEG, REAL_NEG_NEG] THEN 389 REWRITE_TAC[REAL_OF_NUM_MUL]) 390 in 391 FIRST_CONV 392 [GEN_REWRITE_CONV I [pth0], 393 GEN_REWRITE_CONV I [pth1] THENC RAND_CONV MUL_CONV, 394 GEN_REWRITE_CONV I [pth2] THENC RAND_CONV(RAND_CONV MUL_CONV)] 395 end; 396 397(* ------------------------------------------------------------------------- *) 398(* Conversion to normalize product terms, i.e: *) 399(* *) 400(* Separate out (and multiply out) integer constants, put the term in *) 401(* the form "([-]&n) * x" where either x is a canonically ordered product *) 402(* of the non-integer-constants, or is "&1". *) 403(* ------------------------------------------------------------------------- *) 404 405val REAL_PROD_NORM_CONV = 406 let 407 val REAL_MUL_AC = AC REAL_MUL_AC_98 408 val x_tm = ``x:real`` 409 val mul_tm = ``$* : real -> real -> real`` 410 val pth1 = SYM(SPEC x_tm REAL_MUL_RID) 411 val pth2 = SYM(SPEC x_tm REAL_MUL_LID) 412 val binops_mul = liteLib.binops mul_tm 413 val list_mk_binop_mul = list_mk_binop mul_tm 414 val mk_binop_mul = mk_binop mul_tm 415 in 416 fn tm => 417 let 418 val _ = trace "REAL_PROD_NORM_CONV" 419 val _ = trace_term tm 420 val factors = binops_mul tm 421 val (consts,others) = partition is_intconst factors 422 val res = 423 if others = [] then 424 let 425 val th1 = QCONV (DEPTH_CONV REAL_INT_MUL_CONV) tm 426 in 427 TRANS th1 (INST [(rand(concl th1),x_tm)] pth1) 428 end 429 else 430 let 431 val sothers = sort term_lt others 432 in 433 if consts = [] then 434 let 435 val t = mk_eq (tm, list_mk_binop_mul sothers) 436 val th1 = REAL_MUL_AC t 437 in 438 TRANS th1 (INST [(rand(concl th1),x_tm)] pth2) 439 end 440 else 441 let 442 val th1 = REAL_MUL_AC 443 (mk_eq(tm,mk_binop_mul(list_mk_binop_mul consts) 444 (list_mk_binop_mul sothers))) 445 val tm1 = rand(concl th1) 446 val th2 = AP_TERM mul_tm (QCONV (DEPTH_CONV REAL_INT_MUL_CONV) 447 (liteLib.lhand tm1)) 448 in 449 TRANS th1 (AP_THM th2 (rand tm1)) 450 end 451 end 452 val _ = trace_thm res 453 val _ = trace "done REAL_PROD_NORM_CONV" 454 in 455 res 456 end 457 end; 458 459(* ------------------------------------------------------------------------- *) 460(* Addition and subtraction. *) 461(* ------------------------------------------------------------------------- *) 462 463val REAL_INT_ADD_CONV = 464 let 465 val neg_tm = ``$~ :real->real`` 466 val amp_tm = ``(&) :num -> real`` 467 val add_tm = ``$+ : real -> real -> real`` 468 val dest = liteLib.dest_binop add_tm 469 val m_tm = ``m:num`` and n_tm = ``n:num`` 470 val pth0 = prove 471 (``(~(&m) + &m = &0) /\ 472 (&m + ~(&m) = &0)``, 473 REWRITE_TAC[REAL_ADD_LINV, REAL_ADD_RINV]) 474 val [pth1, pth2, pth3, pth4, pth5, pth6] = (CONJUNCTS o prove) 475 (``(~(&m) + ~(&n :real) = ~(&(m + n))) /\ 476 (~(&m) + &(m + n) = &n) /\ 477 (~(&(m + n)) + &m = ~(&n)) /\ 478 (&(m + n) + ~(&m) = &n) /\ 479 (&m + ~(&(m + n)) = ~(&n)) /\ 480 (&m + &n = &(m + n) :real)``, 481 REWRITE_TAC[GSYM REAL_ADD, REAL_NEG_ADD] THEN 482 REWRITE_TAC[REAL_ADD_ASSOC, REAL_ADD_LINV, REAL_ADD_LID] THEN 483 REWRITE_TAC[REAL_ADD_RINV, REAL_ADD_LID] THEN 484 ONCE_REWRITE_TAC[REAL_ADD_SYM] THEN 485 REWRITE_TAC[REAL_ADD_ASSOC, REAL_ADD_LINV, REAL_ADD_LID] THEN 486 REWRITE_TAC[REAL_ADD_RINV, REAL_ADD_LID]) 487 in 488 GEN_REWRITE_CONV I [pth0] ORELSEC 489 (fn tm => 490 let 491 val (l,r) = dest tm 492 in 493 if rator l = neg_tm then 494 if rator r = neg_tm then 495 let 496 val th1 = INST [(rand(rand l),m_tm), (rand(rand r),n_tm)] pth1 497 val tm1 = rand(rand(rand(concl th1))) 498 val th2 = AP_TERM neg_tm (AP_TERM amp_tm (NUM_ADD_CONV tm1)) 499 in 500 TRANS th1 th2 501 end 502 else 503 let 504 val m = rand(rand l) 505 val n = rand r 506 val m' = dest_numeral m 507 val n' = dest_numeral n 508 in 509 if m' <= n' then 510 let 511 val p = mk_numeral (n' - m') 512 val th1 = INST [(m,m_tm), (p,n_tm)] pth2 513 val th2 = NUM_ADD_CONV (rand(rand(liteLib.lhand(concl th1)))) 514 val th3 = AP_TERM (rator tm) (AP_TERM amp_tm (SYM th2)) 515 in 516 TRANS th3 th1 517 end 518 else 519 let 520 val p = mk_numeral (m' - n') 521 val th1 = INST [(n,m_tm), (p,n_tm)] pth3 522 val th2 = NUM_ADD_CONV 523 (rand(rand(liteLib.lhand 524 (liteLib.lhand(concl th1))))) 525 val th3 = AP_TERM neg_tm (AP_TERM amp_tm (SYM th2)) 526 val th4 = AP_THM (AP_TERM add_tm th3) (rand tm) 527 in 528 TRANS th4 th1 529 end 530 end 531 else 532 if rator r = neg_tm then 533 let 534 val m = rand l and n = rand(rand r) 535 val m' = dest_numeral m and n' = dest_numeral n 536 in 537 if n' <= m' then 538 let 539 val p = mk_numeral (m' - n') 540 val th1 = INST [(n,m_tm), (p,n_tm)] pth4 541 val th2 = NUM_ADD_CONV (rand(liteLib.lhand(liteLib.lhand(concl th1)))) 542 val th3 = AP_TERM add_tm (AP_TERM amp_tm (SYM th2)) 543 val th4 = AP_THM th3 (rand tm) 544 in 545 TRANS th4 th1 546 end 547 else 548 let 549 val p = mk_numeral (n' - m') 550 val th1 = INST [(m,m_tm), (p,n_tm)] pth5 551 val th2 = NUM_ADD_CONV (rand(rand(rand(liteLib.lhand(concl th1))))) 552 val th3 = AP_TERM neg_tm (AP_TERM amp_tm (SYM th2)) 553 val th4 = AP_TERM (rator tm) th3 554 in 555 TRANS th4 th1 556 end 557 end 558 else 559 let 560 val th1 = INST [(rand l,m_tm), (rand r,n_tm)] pth6 561 val tm1 = rand(rand(concl th1)) 562 val th2 = AP_TERM amp_tm (NUM_ADD_CONV tm1) 563 in 564 TRANS th1 th2 565 end 566 end 567 handle HOL_ERR _ => failwith "REAL_INT_ADD_CONV") 568 end; 569 570(* ------------------------------------------------------------------------- *) 571(* Add together canonically ordered standard linear lists. *) 572(* ------------------------------------------------------------------------- *) 573 574val LINEAR_ADD = 575 let 576 val pth0a = prove 577 (``&0 + x = x :real``, 578 REWRITE_TAC[REAL_ADD_LID]) 579 val pth0b = prove 580 (``x + &0 = x :real``, 581 REWRITE_TAC[REAL_ADD_RID]) 582 val x_tm = ``x:real`` 583 val [pth1, pth2, pth3, pth4, pth5, pth6] = (CONJUNCTS o prove) 584 (``((l1 + r1) + (l2 + r2) = (l1 + l2) + (r1 + r2):real) /\ 585 ((l1 + r1) + tm2 = l1 + (r1 + tm2):real) /\ 586 (tm1 + (l2 + r2) = l2 + (tm1 + r2)) /\ 587 ((l1 + r1) + tm2 = (l1 + tm2) + r1) /\ 588 (tm1 + tm2 = tm2 + tm1) /\ 589 (tm1 + (l2 + r2) = (tm1 + l2) + r2)``, 590(REPEAT CONJ_TAC 591 THEN REWRITE_TAC[realTheory.REAL_ADD_ASSOC] 592 THEN TRY (MATCH_ACCEPT_TAC realTheory.REAL_ADD_SYM) THENL 593 [REWRITE_TAC[GSYM realTheory.REAL_ADD_ASSOC] THEN AP_TERM_TAC 594 THEN ONCE_REWRITE_TAC [realTheory.REAL_ADD_SYM] 595 THEN Rewrite.GEN_REWRITE_TAC RAND_CONV 596 Rewrite.empty_rewrites [realTheory.REAL_ADD_SYM] 597 THEN REWRITE_TAC[GSYM realTheory.REAL_ADD_ASSOC] THEN AP_TERM_TAC 598 THEN MATCH_ACCEPT_TAC realTheory.REAL_ADD_SYM, 599 ONCE_REWRITE_TAC [realTheory.REAL_ADD_SYM] THEN AP_TERM_TAC 600 THEN MATCH_ACCEPT_TAC realTheory.REAL_ADD_SYM, 601 REWRITE_TAC[GSYM realTheory.REAL_ADD_ASSOC] THEN AP_TERM_TAC 602 THEN MATCH_ACCEPT_TAC realTheory.REAL_ADD_SYM])) 603 val tm1_tm = ``tm1:real`` 604 val l1_tm = ``l1:real`` 605 val r1_tm = ``r1:real`` 606 val tm2_tm = ``tm2:real`` 607 val l2_tm = ``l2:real`` 608 val r2_tm = ``r2:real`` 609 val add_tm = ``$+ :real->real->real`` 610 val dest = liteLib.dest_binop add_tm 611 val mk = mk_binop add_tm 612 val zero_tm = ``&0 :real`` 613 val COEFF_CONV = 614 QCONV (REWR_CONV (GSYM REAL_ADD_RDISTRIB) THENC 615 LAND_CONV REAL_INT_ADD_CONV) 616 fun linear_add tm1 tm2 = 617 let 618 val _ = trace "linear_add" 619 val _ = trace_term tm1 620 val _ = trace_term tm2 621 val res = 622 let 623 val ltm = mk tm1 tm2 624 in 625 if tm1 = zero_tm then INST [(tm2,x_tm)] pth0a 626 else if tm2 = zero_tm then INST [(tm1,x_tm)] pth0b else 627 let 628 val (l1,r1) = dest tm1 629 val v1 = rand l1 630 val _ = trace "v1 =" 631 val _ = trace_term v1 632 in 633 let 634 val (l2,r2) = dest tm2 635 val v2 = rand l2 636 val _ = trace "v2 =" 637 val _ = trace_term v2 638 in 639 if aconv v1 v2 then 640 let 641 val th1 = INST [(l1,l1_tm), (l2,l2_tm), 642 (r1,r1_tm), (r2,r2_tm)] pth1 643 val th2 = CONV_RULE (RAND_CONV(LAND_CONV COEFF_CONV)) th1 644 val ctm = rator(rand(concl th2)) 645 in 646 TRANS th2 (AP_TERM ctm (linear_add r1 r2)) 647 end 648 (* handle e as HOL_ERR => Raise e *) 649 else if term_lt v1 v2 then 650 let 651 val th1 = INST [(l1,l1_tm), (r1,r1_tm), (tm2,tm2_tm)] pth2 652 val ctm = rator(rand(concl th1)) 653 in 654 TRANS th1 (AP_TERM ctm (linear_add r1 tm2)) 655 end 656 else 657 let 658 val th1 = INST [(tm1,tm1_tm), (l2,l2_tm), (r2,r2_tm)] pth3 659 val ctm = rator(rand(concl th1)) 660 in 661 TRANS th1 (AP_TERM ctm (linear_add tm1 r2)) 662 end 663 end 664 handle HOL_ERR _ => 665 let 666 val _ = trace "can't add_dest term2" 667 val v2 = rand tm2 668 val _ = trace "v2 =" 669 val _ = trace_term v2 670 in 671 if aconv v1 v2 then 672 let 673 val th1 = INST [(l1,l1_tm), (r1,r1_tm), (tm2,tm2_tm)] pth4 674 in 675 CONV_RULE (RAND_CONV(LAND_CONV COEFF_CONV)) th1 676 end 677 else if term_lt v1 v2 then 678 let 679 val th1 = INST [(l1,l1_tm), (r1,r1_tm), (tm2,tm2_tm)] pth2 680 val ctm = rator(rand(concl th1)) 681 in 682 TRANS th1 (AP_TERM ctm (linear_add r1 tm2)) 683 end 684 else 685 INST [(tm1,tm1_tm), (tm2,tm2_tm)] pth5 686 end 687 end 688 handle _ => 689 let 690 val _ = trace "can't add_dest term1" 691 val v1 = rand tm1 692 in 693 let 694 val (l2,r2) = dest tm2 695 val v2 = rand l2 696 in 697 if aconv v1 v2 then 698 let 699 val th1 = INST [(tm1,tm1_tm), (l2,l2_tm), (r2,r2_tm)] pth6 700 in 701 CONV_RULE (RAND_CONV(LAND_CONV COEFF_CONV)) th1 702 end 703 else if term_lt v1 v2 then 704 REFL ltm 705 else 706 let 707 val th1 = INST [(tm1,tm1_tm), (l2,l2_tm), (r2,r2_tm)] pth3 708 val ctm = rator(rand(concl th1)) 709 in 710 TRANS th1 (AP_TERM ctm (linear_add tm1 r2)) 711 end 712 end 713 handle _ => 714 let 715 val _ = trace "can't add_dest term2 either" 716 val v2 = rand tm2 717 in 718 if aconv v1 v2 then 719 COEFF_CONV ltm 720 else if term_lt v1 v2 then 721 REFL ltm 722 else 723 INST [(tm1,tm1_tm), (tm2,tm2_tm)] pth5 724 end 725 end 726 end 727 val _ = trace_thm res 728 val _ = trace "done linear_add" 729 in 730 res 731 end 732 in 733 fn tm1 => fn tm2 => 734 let 735 val _ = trace "LINEAR_ADD" 736 val _ = trace_term tm1 737 val _ = trace_term tm2 738 val th = linear_add tm1 tm2 739 val tm = rand(concl th) 740 val zth = 741 QCONV (GEN_REWRITE_CONV 742 DEPTH_CONV 743 [REAL_MUL_LZERO, REAL_ADD_LID, REAL_ADD_RID]) tm 744 val res = TRANS th zth 745 val _ = trace_thm res 746 val _ = trace "done LINEAR_ADD" 747 in 748 res 749 end 750 end; 751 752(* ------------------------------------------------------------------------- *) 753(* Collection of like terms. *) 754(* ------------------------------------------------------------------------- *) 755 756val COLLECT_CONV = 757 let 758 val add_tm = ``$+ :real->real->real`` 759 val dest = liteLib.dest_binop add_tm 760 fun collect tm = 761 let 762 val (l,r) = dest tm 763 val lth = collect l 764 val rth = collect r 765 val xth = LINEAR_ADD (rand(concl lth)) (rand(concl rth)) 766 in 767 TRANS (MK_COMB(AP_TERM add_tm lth,rth)) xth 768 end 769 handle HOL_ERR _ => REFL tm 770 in 771 collect 772 end; 773 774(* ------------------------------------------------------------------------- *) 775(* Normalize a term in the standard linear form. *) 776(* ------------------------------------------------------------------------- *) 777 778val REAL_SUM_NORM_CONV = 779 let 780 val REAL_ADD_AC = AC REAL_ADD_AC_98 781 val pth1 = prove (``~x = ~(&1) * x``, 782 REWRITE_TAC[REAL_MUL_LNEG, REAL_MUL_LID]) 783 val pth2 = prove (``x - y:real = x + ~(&1) * y``, 784 REWRITE_TAC[real_sub, GSYM pth1]) 785 val ptm = ``$~ :real->real`` 786 val stm = ``$+ :real->real->real`` 787 val one_tm = ``&1 :real`` 788 val binops_add = liteLib.binops stm 789 val list_mk_binop_add = list_mk_binop stm 790 fun prelim_conv t = 791 let 792 val _ = trace "prelim_conv" 793 fun c1 t = (trace "gen_rewrite 1"; 794 trace_term t; 795 GEN_REWRITE_CONV I [pth1] t) 796 fun c2 t = (trace "gen_rewrite 2"; 797 trace_term t; 798 GEN_REWRITE_CONV I [pth2] t) 799 fun c3 t = (trace "gen_rewrite 3"; trace_term t; 800 GEN_REWRITE_CONV TOP_DEPTH_CONV 801 [REAL_ADD_LDISTRIB, REAL_ADD_RDISTRIB] t) 802 fun c4 t = (trace "gen_rewrite 4"; trace_term t; 803 GEN_REWRITE_CONV DEPTH_CONV 804 [REAL_MUL_LZERO, REAL_MUL_RZERO, 805 REAL_MUL_LID, REAL_MUL_RID, 806 REAL_ADD_LID, REAL_ADD_RID] t) 807 val c = DEPTH_CONV((c1 o assert(fn t => not (rand t = one_tm))) 808 ORELSEC c2) THENC c3 THENC c4 809 val res = c t 810 val _ = trace "done prelim_conv" 811 in 812 res 813 end 814 in 815 fn tm => 816 let 817 val _ = trace "REAL_SUM_NORM_CONV" 818 val _ = trace_term tm 819 val th1 = QCONV prelim_conv tm 820 val th2 = liteLib.DEPTH_BINOP_CONV stm 821 (QCONV REAL_PROD_NORM_CONV) (rand(concl th1)) 822 val tm2 = rand(concl th2) 823 val elements = binops_add tm2 824 val selements = sort (fn x => fn y => term_le (rand x) (rand y)) 825 elements 826 val th3 = REAL_ADD_AC(mk_eq(tm2,list_mk_binop_add selements)) 827 val th4 = COLLECT_CONV (rand(concl th3)) 828 val res = itlist TRANS [th1, th2, th3] th4 829 val _ = trace "done REAL_SUM_NORM_CONV" 830 in 831 res 832 end 833 end; 834 835(* ------------------------------------------------------------------------- *) 836(* Produce negated forms of canonicalization theorems. *) 837(* ------------------------------------------------------------------------- *) 838 839val REAL_NEGATE_CANON = 840 let 841 val pth1 = prove 842 (``((a:real <= b = &0 <= X) = (b < a = &0 < ~X)) /\ 843 ((a:real < b = &0 < X) = (b <= a = &0 <= ~X))``, 844 REWRITE_TAC[real_lt, REAL_LE_LNEG, REAL_LE_RNEG] THEN 845 REWRITE_TAC[REAL_ADD_RID, REAL_ADD_LID] THEN 846 CONV_TAC tautLib.TAUT_CONV) 847 val pth2 = prove 848 (``~((~a) * x + z :real) = a * x + ~z``, 849 REWRITE_TAC[GSYM REAL_MUL_LNEG, REAL_NEG_ADD, REAL_NEG_NEG]) 850 val pth3 = prove 851 (``~(a * x + z :real) = ~a * x + ~z``, 852 REWRITE_TAC[REAL_NEG_ADD, GSYM REAL_MUL_LNEG]) 853 val pth4 = prove 854 (``~(~a * x :real) = a * x``, 855 REWRITE_TAC[REAL_MUL_LNEG, REAL_NEG_NEG]) 856 val pth5 = prove 857 (``~(a * x :real) = ~a * x``, 858 REWRITE_TAC[REAL_MUL_LNEG]) 859 val rewr1_CONV = FIRST_CONV (map REWR_CONV [pth2, pth3]) 860 val rewr2_CONV = FIRST_CONV (map REWR_CONV [pth4, pth5]) 861 fun distrib_neg_conv tm = 862 let 863 val _ = trace "distrib_neg_conv" 864 val _ = trace_term tm 865 val res = 866 let 867 val th = rewr1_CONV tm 868 val _ = trace "ok so far" 869 val t = rand (concl th) 870 val _ = trace_term t 871 in 872 TRANS th (RAND_CONV distrib_neg_conv t) 873 end 874 handle HOL_ERR _ => rewr2_CONV tm 875 val _ = trace "done distrib_neg_conv" 876 in 877 res 878 end 879 in 880 fn th => 881 let 882 val _ = trace "REAL_NEGATE_CANON" 883 val _ = trace_thm th 884 val th1 = GEN_REWRITE_RULE I [pth1] th 885 val _ = trace_thm th1 886 val t = rand (concl th1) 887 val _ = trace_term t 888 val res = TRANS th1 (RAND_CONV distrib_neg_conv t) 889 val _ = trace "done REAL_NEGATE_CANON" 890 in 891 res 892 end 893 end; 894 895(* ------------------------------------------------------------------------- *) 896(* Version for whole atom, with intelligent cacheing. *) 897(* ------------------------------------------------------------------------- *) 898 899val (clear_atom_cache,REAL_ATOM_NORM_CONV) = 900 let 901 val right_CONV = RAND_CONV REAL_SUM_NORM_CONV 902 val atomcache = ref [] 903 fun lookup_cache tm = first (fn th => liteLib.lhand(concl th) = tm) (!atomcache) 904 fun clear_atom_cache () = (atomcache := []) 905 val pth2 = prove 906 (``(a:real < b = c < d:real) = (b <= a = d <= c)``, 907 REWRITE_TAC[real_lt] THEN CONV_TAC tautLib.TAUT_CONV) 908 val pth3 = prove 909 (``(a:real <= b = c <= d:real) = (b < a = d < c)``, 910 REWRITE_TAC[real_lt] THEN CONV_TAC tautLib.TAUT_CONV) 911 val negate_CONV = GEN_REWRITE_CONV I [pth2,pth3] 912 val le_tm = ``$<= :real->real->bool`` 913 val lt_tm = ``$< :real->real->bool`` 914 in 915 (clear_atom_cache, 916 fn tm => (trace "REAL_ATOM_NORM_CONV"; lookup_cache tm 917 handle HOL_ERR _ => 918 let 919 val th = right_CONV tm 920 in 921 (atomcache := th::(!atomcache); 922 let 923 val th' = REAL_NEGATE_CANON th 924 in 925 atomcache := th'::(!atomcache) 926 end 927 handle HOL_ERR _ => (); 928 th) 929 end)) 930 end; 931 932(* ------------------------------------------------------------------------- *) 933(* Combinators. *) 934(* ------------------------------------------------------------------------- *) 935 936infix F_F; 937fun (f F_F g) (x, y) = (f x, g y); 938 939(* ------------------------------------------------------------------------- *) 940(* Replication and sequences. *) 941(* ------------------------------------------------------------------------- *) 942 943fun upto n = 944 let 945 fun down l n = if n < zero then l else down (n::l) (n - one) 946 in 947 down [] n 948 end; 949 950(* ------------------------------------------------------------------------- *) 951(* Encodings of linear inequalities with justifications. *) 952(* ------------------------------------------------------------------------- *) 953 954datatype lineq_type = Eq | Le | Lt; 955 956datatype injust = Given of thm 957 | Multiplied of int * injust 958 | Added of injust * injust; 959 960datatype lineq = Lineq of int * lineq_type * int list * injust; 961 962fun injust_eq (Given t, Given t') = (dest_thm t = dest_thm t') 963 | injust_eq (Multiplied (i,j), Multiplied (i',j')) = 964 (i = i') andalso injust_eq (j,j') 965 | injust_eq (Added (j1,j2), Added (j1',j2')) = 966 injust_eq (j1,j1') andalso injust_eq (j2,j2') 967 | injust_eq (j,j') = false; 968 969fun lineq_eq (Lineq(i,t,l,j),Lineq(i',t',l',j')) = 970 i = i' andalso t = t' andalso l = l' andalso injust_eq (j,j'); 971 972(* ------------------------------------------------------------------------- *) 973(* The main refutation-finding code. *) 974(* ------------------------------------------------------------------------- *) 975 976fun is_trivial (Lineq(_,_,l,_)) = all ((curry op=) zero) l; 977 978fun find_answer (ans as Lineq (k,ty,l,_)) = 979 if ty = Eq andalso (not (k = zero)) 980 orelse ty = Le andalso k > zero 981 orelse ty = Lt andalso k >= zero 982 then 983 ans 984 else 985 failwith "find_answer"; 986 987fun calc_blowup l = 988 let 989 val (p,n) = partition ((curry op<) zero) (filter ((curry op<>) zero) l) 990 in 991 (fromInt (length p)) * (fromInt (length n)) 992 end; 993 994(* ------------------------------------------------------------------------- *) 995(* "Set" operations on lists. *) 996(* ------------------------------------------------------------------------- *) 997 998fun union l1 l2 = itlist insert l1 l2; 999 1000fun Union l = itlist union l []; 1001 1002(* ------------------------------------------------------------------------- *) 1003(* GCD and LCM. *) 1004(* ------------------------------------------------------------------------- *) 1005 1006fun abs x = if x < zero then ~x else x; 1007 1008fun sgn x = x >= zero; 1009 1010val gcd = 1011 let 1012 fun gxd x y = 1013 if y = zero then x else gxd y (x mod y) 1014 in 1015 fn x => fn y => if x < y then gxd y x else gxd x y 1016 end; 1017 1018fun lcm x y = (x * y) div gcd x y; 1019 1020(* ------------------------------------------------------------------------- *) 1021(* Calculate new (in)equality type after addition. *) 1022(* ------------------------------------------------------------------------- *) 1023 1024val find_add_type = 1025 fn (Eq,x) => x 1026 | (x,Eq) => x 1027 | (_,Lt) => Lt 1028 | (Lt,_) => Lt 1029 | (Le,Le) => Le; 1030 1031(* ------------------------------------------------------------------------- *) 1032(* Add together (in)equations. *) 1033(* ------------------------------------------------------------------------- *) 1034 1035fun add_ineq (i1 as Lineq(k1,ty1,l1,just1)) (i2 as Lineq(k2,ty2,l2,just2)) = 1036 let 1037 val l = map2 (curry op+) l1 l2 1038 in 1039 Lineq(k1+k2,find_add_type(ty1,ty2),l,Added(just1,just2)) 1040 end; 1041 1042(* ------------------------------------------------------------------------- *) 1043(* Multiply out an (in)equation. *) 1044(* ------------------------------------------------------------------------- *) 1045 1046fun multiply_ineq n (i as Lineq(k,ty,l,just)) = 1047 if n = one then i 1048 else if n = zero andalso ty = Lt then failwith "multiply_ineq" 1049 else if n < zero andalso (ty = Le orelse ty = Lt) then 1050 failwith "multiply_ineq" 1051 else Lineq(n * k,ty,map ((curry op* ) n) l,Multiplied(n,just)); 1052 1053(* ------------------------------------------------------------------------- *) 1054(* Elimination of variable between a single pair of (in)equations. *) 1055(* If they're both inequalities, 1st coefficient must be +ve, 2nd -ve. *) 1056(* ------------------------------------------------------------------------- *) 1057 1058fun elim_var v (i1 as Lineq(k1,ty1,l1,just1)) (i2 as Lineq(k2,ty2,l2,just2)) = 1059 let 1060 val c1 = el0 v l1 1061 val c2 = el0 v l2 1062 val m = lcm (abs c1) (abs c2) 1063 val m1 = m div (abs c1) 1064 val m2 = m div (abs c2) 1065 val (n1,n2) = 1066 if sgn(c1) = sgn(c2) 1067 then if ty1 = Eq 1068 then (~m1,m2) 1069 else if ty2 = Eq 1070 then (m1,~m2) 1071 else failwith "elim_var" 1072 else (m1,m2) 1073 val (p1,p2) = 1074 if ty1 = Eq andalso ty2 = Eq andalso (n1 = ~one orelse n2 = ~one) 1075 then (~n1,~n2) 1076 else (n1,n2) 1077 in 1078 add_ineq (multiply_ineq n1 i1) (multiply_ineq n2 i2) 1079 end; 1080 1081(* ------------------------------------------------------------------------- *) 1082(* All pairs arising from applying a function over two lists. *) 1083(* ------------------------------------------------------------------------- *) 1084 1085fun allpairs f l1 l2 = itlist (union o C map l2 o f) l1 []; 1086fun op_allpairs eq f l1 l2 = itlist ((op_union eq) o C map l2 o f) l1 []; 1087 1088(* ------------------------------------------------------------------------- *) 1089(* Main elimination code: *) 1090(* *) 1091(* (1) Looks for immediate solutions (false assertions with no variables). *) 1092(* *) 1093(* (2) If there are any equations, picks a variable with the lowest absolute *) 1094(* coefficient in any of them, and uses it to eliminate. *) 1095(* *) 1096(* (3) Otherwise, chooses a variable in the inequality to minimize the *) 1097(* blowup (number of consequences generated) and eliminates it. *) 1098(* ------------------------------------------------------------------------- *) 1099 1100fun elim ineqs = 1101 let 1102 val _ = trace ("elim: #(ineqs) = " ^ (Int.toString (length ineqs)) ^ ".") 1103 val (triv,nontriv) = partition is_trivial ineqs 1104 val res = 1105 if not (null triv) then tryfind find_answer triv 1106 handle HOL_ERR _ => elim nontriv 1107 else 1108 if null nontriv then failwith "elim" else 1109 let 1110 val (eqs,noneqs) = partition (fn (Lineq(_,ty,_,_)) => ty = Eq) 1111 nontriv 1112 in 1113 if not (null eqs) then 1114 let 1115 val clists = map (fn (Lineq(_,_,l,_)) => l) eqs 1116 val sclist = sort (fn x => fn y => abs(x) <= abs(y)) 1117 (filter ((curry op<>) zero) (Union clists)) 1118 val _ = trace ("elim: #(sclist) = " 1119 ^ (Int.toString (length sclist)) ^ ".") 1120 val c = hd sclist 1121 val (v,eq) = tryfind 1122 (fn (i as Lineq(_,_,l,_)) => (index c l,i)) eqs 1123 val othereqs = filter (not o ((curry lineq_eq) eq)) eqs 1124 val (ioth,roth) = 1125 partition (fn (Lineq(_,_,l,_)) => el0 v l = zero) 1126 (othereqs @ noneqs) 1127 val others = map (elim_var v eq) roth @ ioth 1128 in 1129 elim others 1130 end 1131 else 1132 let 1133 val lists = map (fn (Lineq(_,_,l,_)) => l) noneqs 1134 val _ = trace ("elim: #(lists) = " 1135 ^ (Int.toString (length lists)) ^ ".") 1136 val numlist = upto (fromInt (length(hd lists)) - one) 1137 val coeffs = map (fn i => map (el0 i) lists) numlist 1138 val blows = map calc_blowup coeffs 1139 val iblows = zip blows numlist 1140 val _ = trace ("elim: #(iblows) = " 1141 ^ (Int.toString (length iblows)) ^ ".") 1142 val iblows' = filter ((curry op<>) zero o fst) iblows 1143 val _ = trace ("elim: #(iblows') = " 1144 ^ (Int.toString (length iblows')) ^ ".") 1145 val (c,v) = Lib.trye hd 1146 (sort (fn x => fn y => fst(x) <= fst(y)) iblows') 1147 val (no,yes) = partition 1148 (fn (Lineq(_,_,l,_)) => el0 v l = zero) ineqs 1149 val (pos,neg) = partition 1150 (fn (Lineq(_,_,l,_)) => el0 v l > zero) yes 1151 in 1152 elim (no @ op_allpairs (curry lineq_eq) (elim_var v) pos neg) 1153 end 1154 end 1155 val _ = trace "done elim" 1156 in 1157 res 1158 end 1159 1160 1161(* ------------------------------------------------------------------------- *) 1162(* Multiply standard linear list by a constant. *) 1163(* ------------------------------------------------------------------------- *) 1164 1165val LINEAR_MULT = 1166 let 1167 val mult_tm = ``$* :real->real->real`` 1168 val zero_tm = ``&0 :real`` 1169 val x_tm = ``x:real`` 1170 val add_tm = ``$+ :real->real->real`` 1171 val pth = prove 1172 (``x * &0 = &0 :real``, 1173 REWRITE_TAC[REAL_MUL_RZERO]) 1174 val conv1 = GEN_REWRITE_CONV TOP_SWEEP_CONV [REAL_ADD_LDISTRIB] 1175 val conv2 = liteLib.DEPTH_BINOP_CONV add_tm 1176 (REWR_CONV REAL_MUL_ASSOC THENC LAND_CONV REAL_INT_MUL_CONV) 1177 in 1178 fn n => fn tm => 1179 if tm = zero_tm then INST [(n,x_tm)] pth else 1180 let 1181 val ltm = mk_comb(mk_comb(mult_tm,n),tm) 1182 in 1183 (conv1 THENC conv2) ltm 1184 end 1185 end; 1186 1187(* ------------------------------------------------------------------------- *) 1188(* Translate back a proof. *) 1189(* ------------------------------------------------------------------------- *) 1190 1191val REAL_LT_LADD_IMP = prove( 1192 ``!x y z:real. y < z ==> x + y < x + z``, 1193 ACCEPT_TAC (((GEN ``x:real``) 1194 o (GEN ``y:real``) 1195 o (GEN ``z:real``) 1196 o fst 1197 o EQ_IMP_RULE 1198 o SPEC_ALL 1199 o GSYM) 1200 REAL_LT_LADD)); 1201 1202fun op_assoc eq x [] = failwith "op_assoc: mapping does not exist" 1203 | op_assoc eq x ((x',y')::t) = if eq x x' then (x',y') else op_assoc eq x t; 1204 1205val TRANSLATE_PROOF = 1206 let 1207 val TRIVIAL_CONV = DEPTH_CONV 1208 (CHANGED_CONV REAL_INT_NEG_CONV ORELSEC 1209 REAL_INT_ADD_CONV ORELSEC 1210 REAL_INT_MUL_CONV ORELSEC 1211 REAL_INT_LE_CONV ORELSEC 1212 REAL_INT_EQ_CONV ORELSEC 1213 REAL_INT_LT_CONV) THENC 1214 GEN_REWRITE_CONV TOP_DEPTH_CONV (implicit_rewrites()) 1215 1216 val ADD_INEQS = 1217 let 1218 val a_tm = ``a:real`` 1219 val b_tm = ``b:real`` 1220 val pths = (CONJUNCTS o prove) 1221 (``((&0 = a) /\ (&0 = b) ==> (&0 = a + b :real)) /\ 1222 ((&0 = a) /\ (&0 <= b) ==> (&0 <= a + b :real)) /\ 1223 ((&0 = a) /\ (&0 < b) ==> (&0 < a + b :real)) /\ 1224 ((&0 <= a) /\ (&0 = b) ==> (&0 <= a + b :real)) /\ 1225 ((&0 <= a) /\ (&0 <= b) ==> (&0 <= a + b :real)) /\ 1226 ((&0 <= a) /\ (&0 < b) ==> (&0 < a + b :real)) /\ 1227 ((&0 < a) /\ (&0 = b) ==> (&0 < a + b :real)) /\ 1228 ((&0 < a) /\ (&0 <= b) ==> (&0 < a + b :real)) /\ 1229 ((&0 < a) /\ (&0 < b) ==> (&0 < a + b :real))``, 1230 CONV_TAC(ONCE_DEPTH_CONV SYM_CONV) THEN 1231 REPEAT STRIP_TAC THEN 1232 ASM_REWRITE_TAC[REAL_ADD_LID, REAL_ADD_RID] THENL 1233 [MATCH_MP_TAC REAL_LE_TRANS, 1234 MATCH_MP_TAC REAL_LET_TRANS, 1235 MATCH_MP_TAC REAL_LTE_TRANS, 1236 MATCH_MP_TAC REAL_LT_TRANS] THEN 1237 EXISTS_TAC ``a:real`` THEN ASM_REWRITE_TAC[] THEN 1238 GEN_REWRITE_TAC LAND_CONV [GSYM REAL_ADD_RID] THEN 1239 (MATCH_MP_TAC REAL_LE_LADD_IMP ORELSE MATCH_MP_TAC REAL_LT_LADD_IMP) 1240 THEN ASM_REWRITE_TAC[]) 1241 in 1242 fn th1 => fn th2 => 1243 let 1244 val a = rand(concl th1) 1245 val b = rand(concl th2) 1246 val xth = tryfind 1247 (C MP (CONJ th1 th2) o INST [(a,a_tm), (b,b_tm)]) pths 1248 val yth = LINEAR_ADD a b 1249 in 1250 EQ_MP (AP_TERM (rator(concl xth)) yth) xth 1251 end 1252 end 1253 val MULTIPLY_INEQS = 1254 let 1255 val pths = (CONJUNCTS o prove) 1256 (``((&0 = y) ==> (&0 = x * y :real)) /\ 1257 (&0 <= y ==> &0 <= x ==> &0 <= x * y :real) /\ 1258 (&0 < y ==> &0 < x ==> &0 < x * y :real)``, 1259 CONV_TAC(ONCE_DEPTH_CONV SYM_CONV) THEN 1260 REPEAT STRIP_TAC THEN ASM_REWRITE_TAC[REAL_MUL_RZERO] THENL 1261 [MATCH_MP_TAC REAL_LE_MUL, 1262 MATCH_MP_TAC REAL_LT_MUL] THEN 1263 ASM_REWRITE_TAC[]) 1264 val x_tm = ``x:real`` 1265 val y_tm = ``y:real`` 1266 in 1267 fn x => fn th => 1268 let 1269 val y = rand(concl th) 1270 val xth = tryfind (C MP th o INST[(x,x_tm), (y,y_tm)]) pths 1271 val wth = if is_imp(concl xth) then 1272 MP (CONV_RULE(LAND_CONV TRIVIAL_CONV) xth) TRUTH else xth 1273 val yth = LINEAR_MULT x (rand(rand(concl wth))) 1274 in 1275 EQ_MP (AP_TERM (rator(concl wth)) yth) wth 1276 end 1277 end 1278 in 1279 fn refutation => 1280 let 1281 val _ = trace "TRANSLATE_PROOF" 1282 val cache = ref [] 1283 fun translate refut = 1284 snd (op_assoc (curry injust_eq) refut (!cache)) 1285 handle HOL_ERR _ 1286 => case refut 1287 of Given(th) => (cache:= (refut,th)::(!cache); th) 1288 | Added(r1,r2) => 1289 let 1290 val th1 = translate r1 1291 val _ = trace_thm th1 1292 val th2 = translate r2 1293 val _ = trace_thm th2 1294 val th = ADD_INEQS th1 th2 1295 val _ = trace_thm th 1296 in 1297 (cache:= (refut,th)::(!cache); th) 1298 end 1299 | Multiplied(n,r) => 1300 let 1301 val th1 = translate r 1302 val th = MULTIPLY_INEQS (mk_intconst n) th1 1303 in 1304 (cache:= (refut,th)::(!cache); th) 1305 end 1306 val res = CONV_RULE TRIVIAL_CONV (translate refutation) 1307 val _ = trace "done TRANSLATE_PROOF" 1308 in 1309 res 1310 end 1311 end; 1312 1313(* ------------------------------------------------------------------------- *) 1314(* Refute a conjunction of equations and/or inequations. *) 1315(* ------------------------------------------------------------------------- *) 1316 1317val REAL_SIMPLE_ARITH_REFUTER = 1318 let 1319 val trivthm = prove(``&0 < &0 :real = F``, 1320 REWRITE_TAC[REAL_LE_REFL, real_lt]) 1321 val add_tm = ``$+ :real->real->real`` 1322 val one_tm = ``&1 :real`` 1323 val zero_tm = ``&0 :real`` 1324 val less_tm = ``$< :real->real->bool`` 1325 val false_tm = ``F`` 1326 fun fixup_atom th = 1327 let 1328 val _ = trace "fixup_atom" 1329 val _ = trace_term (snd (dest_thm th)) 1330 val th0 = CONV_RULE REAL_ATOM_NORM_CONV th 1331 val _ = trace_thm th0 1332 val tm0 = concl th0 1333 in 1334 if rand tm0 = zero_tm then 1335 if rator(rator tm0) = less_tm then EQ_MP trivthm th0 1336 else failwith "trivially true, so useless in refutation" 1337 else th0 1338 end 1339 val eq_tm = ``$= :real->real->bool`` 1340 val le_tm = ``$<= :real->real->bool`` 1341 val lt_tm = ``$< :real->real->bool`` 1342 in 1343 fn ths0 => 1344 let 1345 val _ = trace "REAL_SIMPLE_ARITH_REFUTER" 1346 val _ = trace ("#(ths0) = " ^ (Int.toString (length ths0)) ^ ".") 1347 val _ = trace_thm_list ths0 1348 val ths = mapfilter fixup_atom ths0 1349 val _ = trace ("#(ths) = " ^ (Int.toString (length ths)) ^ ".") 1350 val _ = trace_thm_list ths 1351 val res = 1352 first (fn th => concl th = false_tm) ths 1353 handle HOL_ERR _ => 1354 let 1355 val allvars = itlist 1356 (op_union aconv o map rand o liteLib.binops add_tm o 1357 rand o concl) ths [] 1358 val vars = 1359 if mem one_tm allvars then one_tm::subtract allvars [one_tm] 1360 else one_tm::allvars 1361 fun unthmify th = 1362 let 1363 val t = concl th 1364 val op_alt = rator(rator t) 1365 val right = rand t 1366 val rights = liteLib.binops add_tm right 1367 val cvps = map (((dest_intconst o rand) 1368 F_F (C index_ac vars)) o dest_comb) rights 1369 val k = ~((fst (rev_assoc zero cvps)) 1370 handle HOL_ERR _ => zero) 1371 val l = Lib.trye tl (map (fn v => (fst (rev_assoc v cvps) 1372 handle HOL_ERR _ => zero)) 1373 (upto (fromInt (length(vars)) - one))) 1374 val ty = if op_alt = eq_tm then Eq 1375 else if op_alt = le_tm then Le 1376 else if op_alt = lt_tm then Lt 1377 else failwith "unknown op" 1378 in 1379 Lineq(k,ty,l,Given th) 1380 end 1381 val ineqs = map unthmify ths 1382 val _ = trace ("#(ineqs) = " ^ (Int.toString (length ineqs)) ^ ".") 1383 val (Lineq(_,_,_,proof)) = elim ineqs 1384 in 1385 TRANSLATE_PROOF proof 1386 end 1387 val _ = trace_thm res 1388 val _ = trace "done REAL_SIMPLE_ARITH_REFUTER" 1389 in 1390 res 1391 end 1392 end; 1393 1394(* ------------------------------------------------------------------------- *) 1395(* General case: canonicalize and split up, then refute the bits. *) 1396(* ------------------------------------------------------------------------- *) 1397 1398val PURE_REAL_ARITH_TAC = 1399 let 1400 val ZERO_LEFT_CONV = 1401 let 1402 val pth = prove 1403 (``((x = y) = (&0 = y + ~x)) /\ 1404 (x <= y = &0 <= y + ~x) /\ 1405 (x < y = &0 < y + ~x)``, 1406 REWRITE_TAC[real_lt, GSYM REAL_LE_LNEG, REAL_LE_NEG2] THEN 1407 REWRITE_TAC[GSYM REAL_LE_RNEG, REAL_NEG_NEG] THEN 1408 REWRITE_TAC[GSYM REAL_LE_ANTISYM, GSYM REAL_LE_LNEG, 1409 GSYM REAL_LE_RNEG, REAL_LE_NEG2, REAL_NEG_NEG]) 1410 val zero_tm = ``&0 :real`` 1411 in 1412 let 1413 val raw_CONV = GEN_REWRITE_CONV I [pth] THENC 1414 GEN_REWRITE_CONV TOP_SWEEP_CONV 1415 [REAL_ADD_LID, REAL_NEG_ADD, REAL_NEG_NEG] 1416 in 1417 fn tm => if liteLib.lhand tm = zero_tm then REFL tm else raw_CONV tm 1418 end 1419 end 1420 val init_CONV = GEN_REWRITE_CONV TOP_DEPTH_CONV [ 1421 FORALL_SIMP, EXISTS_SIMP, 1422 real_gt, real_ge, real_sub, 1423 REAL_ADD_LDISTRIB, REAL_ADD_RDISTRIB, 1424 REAL_MUL_LNEG, REAL_MUL_RNEG, REAL_NEG_NEG, REAL_NEG_ADD, 1425 REAL_MUL_LZERO, REAL_MUL_RZERO, 1426 REAL_MUL_LID, REAL_MUL_RID, 1427 REAL_ADD_LID, REAL_ADD_RID] THENC 1428 REPEATC (CHANGED_CONV Sub_and_cond.COND_ELIM_CONV) THENC PRENEX_CONV 1429 val eq_tm = ``$= :real->real->bool`` 1430 val le_tm = ``$<= :real->real->bool`` 1431 val lt_tm = ``$< :real->real->bool`` 1432 val (ABS_ELIM_TAC1,ABS_ELIM_TAC2,ABS_ELIM_TAC3) = 1433 let 1434 val plus_tm = ``$+ :real->real->real`` 1435 val abs_tm = ``abs:real->real`` 1436 val neg_tm = ``$~: real->real`` 1437 val strip_plus = liteLib.binops plus_tm 1438 val list_mk_plus = list_mk_binop plus_tm 1439 fun is_abstm tm = is_comb tm andalso rator tm = abs_tm 1440 fun is_negtm tm = is_comb tm andalso rator tm = neg_tm 1441 val REAL_ADD_AC = AC REAL_ADD_AC_98 1442 fun is_negabstm tm = is_negtm tm andalso is_abstm(rand tm) 1443 val ABS_ELIM_THM = prove ( 1444 ``(&0 <= ~(abs(x)) + y = &0 <= x + y /\ &0 <= ~x + y) /\ 1445 (&0 < ~(abs(x)) + y = &0 < x + y /\ &0 < ~x + y)``, 1446 REWRITE_TAC[real_abs] THEN COND_CASES_TAC 1447 THEN ASM_REWRITE_TAC[] THEN 1448 REWRITE_TAC[REAL_NEG_NEG] THEN 1449 REWRITE_TAC [ 1450 TAUT_PROVE ``(a = a /\ b) = (a ==> b)``, 1451 TAUT_PROVE ``(b = a /\ b) = (b ==> a)`` 1452 ] 1453 THEN REPEAT STRIP_TAC THEN 1454 MAP_FIRST MATCH_MP_TAC [REAL_LE_TRANS, REAL_LTE_TRANS] THEN 1455 FIRST_ASSUM(fn th => EXISTS_TAC(rand(concl th)) THEN 1456 CONJ_TAC THENL [ACCEPT_TAC th, ALL_TAC]) THEN 1457 ASM_REWRITE_TAC[] THEN ONCE_REWRITE_TAC[REAL_ADD_SYM] THEN 1458 MATCH_MP_TAC REAL_LE_LADD_IMP THEN 1459 MATCH_MP_TAC REAL_LE_TRANS THEN EXISTS_TAC ``&0 :real`` THEN 1460 REWRITE_TAC[REAL_LE_LNEG, REAL_LE_RNEG] THEN 1461 ASM_REWRITE_TAC[REAL_ADD_RID, REAL_ADD_LID] THEN 1462 MP_TAC (SPEC(Term`&0 :real`) (SPEC (Term`x:real`) 1463 REAL_LE_TOTAL)) 1464 THEN ASM_REWRITE_TAC[]) 1465 val ABS_ELIM_RULE = GEN_REWRITE_RULE I [ABS_ELIM_THM] 1466 val NEG_DISTRIB_RULE = 1467 GEN_REWRITE_RULE (RAND_CONV o TOP_SWEEP_CONV) 1468 [REAL_NEG_ADD, REAL_NEG_NEG] 1469 val REDISTRIB_RULE = CONV_RULE init_CONV 1470 val ABS_CASES_THM = prove 1471 (``(abs(x) = x) \/ (abs(x) = ~x)``, 1472 REWRITE_TAC[real_abs] THEN COND_CASES_TAC 1473 THEN REWRITE_TAC[]) 1474 val ABS_STRONG_CASES_THM = prove ( 1475 ``&0 <= x /\ (abs(x) = x) \/ 1476 (&0 <= ~x) /\ (abs(x) = ~x)``, 1477 REWRITE_TAC[real_abs] THEN COND_CASES_TAC 1478 THEN REWRITE_TAC[] THEN 1479 REWRITE_TAC[REAL_LE_RNEG, REAL_ADD_LID] THEN 1480 MP_TAC (SPEC(Term`&0 :real`) 1481 (SPEC (Term`x:real`) REAL_LE_TOTAL)) 1482 THEN ASM_REWRITE_TAC[]) 1483 val x_tm = ``x:real`` 1484 fun ABS_ELIM_TAC1 th = 1485 let 1486 val (tmx,tm0) = dest_comb(concl th) 1487 val op_alt = rator tmx 1488 in 1489 (trace "ABS_ELIM_TAC1"; 1490 if op_alt <> le_tm andalso op_alt <> lt_tm 1491 then failwith "ABS_ELIM_TAC1" else 1492 let 1493 val tms = strip_plus tm0 1494 val tm = first is_negabstm tms 1495 val n = index tm tms 1496 val (ltms,rtms) = chop_list n tms 1497 val ntms = tm::(ltms @ tl rtms) 1498 val th1 = AP_TERM tmx 1499 (REAL_ADD_AC (mk_eq(tm0, list_mk_plus ntms))) 1500 val th2 = ABS_ELIM_RULE (EQ_MP th1 th) 1501 in 1502 CONJUNCTS_THEN ASSUME_TAC (NEG_DISTRIB_RULE th2) 1503 end) 1504 end 1505 fun ABS_ELIM_TAC2 th = 1506 let 1507 val (tmx,tm0) = dest_comb(concl th) 1508 val op_alt = rator tmx 1509 in 1510 (trace "ABS_ELIM_TAC2"; 1511 if op_alt <> le_tm andalso op_alt <> lt_tm 1512 then failwith "ABS_ELIM_TAC1" 1513 else 1514 let 1515 val tms = strip_plus tm0 1516 val tm = first is_abstm tms 1517 in 1518 DISJ_CASES_THEN2 1519 (fn th => RULE_ASSUM_TAC (SUBS [th])) 1520 (fn th => RULE_ASSUM_TAC (NEG_DISTRIB_RULE o SUBS [th])) 1521 (INST [(rand tm,x_tm)] ABS_CASES_THM) 1522 end) 1523 end 1524 fun ABS_ELIM_TAC3 th = 1525 let 1526 val tm = find_term is_abstm (concl th) 1527 in 1528 (trace "ABS_ELIM_TAC2"; 1529 DISJ_CASES_THEN2 1530 (CONJUNCTS_THEN2 ASSUME_TAC (fn th => RULE_ASSUM_TAC (SUBS [th]))) 1531 (CONJUNCTS_THEN2 (ASSUME_TAC o REDISTRIB_RULE) 1532 (fn th => RULE_ASSUM_TAC (REDISTRIB_RULE o SUBS [th]))) 1533 (INST [(rand tm,x_tm)] ABS_STRONG_CASES_THM)) 1534 end 1535 in 1536 (ABS_ELIM_TAC1,ABS_ELIM_TAC2,ABS_ELIM_TAC3) 1537 end 1538 val atom_CONV = 1539 let 1540 val pth = prove 1541 (``(~(x:real <= y) = y < x) /\ 1542 (~(x:real < y) = y <= x) /\ 1543 (~(x = y) = (x:real) < y \/ y < x)``, 1544 REWRITE_TAC[real_lt] THEN REWRITE_TAC[GSYM DE_MORGAN_THM] THEN 1545 REWRITE_TAC[REAL_LE_ANTISYM] THEN AP_TERM_TAC THEN 1546 MATCH_ACCEPT_TAC EQ_SYM_EQ) 1547 in 1548 GEN_REWRITE_CONV I [pth] 1549 end 1550 fun DISCARD_UNREAL_TAC th = 1551 let 1552 val tm = concl th 1553 in 1554 if is_comb tm andalso 1555 let 1556 val tm' = rator tm 1557 in 1558 is_comb tm' andalso 1559 let 1560 val tm'' = rator tm' 1561 in 1562 tm'' = eq_tm orelse tm'' = le_tm orelse tm'' = lt_tm 1563 end 1564 end 1565 then failwith "DISCARD_UNREAL_TAC" 1566 else 1567 ALL_TAC 1568 end 1569 in 1570 fn g => 1571 let 1572 val _ = trace "PURE_REAL_ARITH_TAC" 1573 val tac = 1574 REPEAT GEN_TAC THEN 1575 CONV_TAC init_CONV THEN 1576 REPEAT GEN_TAC THEN 1577 REFUTE_THEN(MP_TAC o 1578 CONV_RULE 1579 (PRESIMP_CONV THENC NNF_CONV THENC SKOLEM_CONV THENC 1580 PRENEX_CONV THENC ONCE_DEPTH_CONV atom_CONV THENC 1581 PROP_DNF_CONV)) THEN 1582 DISCH_THEN(REPEAT_TCL 1583 (CHOOSE_THEN ORELSE_TCL DISJ_CASES_THEN ORELSE_TCL 1584 CONJUNCTS_THEN) 1585 ASSUME_TAC) THEN 1586 TRY(FIRST_ASSUM CONTR_TAC) THEN 1587 REPEAT(FIRST_X_ASSUM DISCARD_UNREAL_TAC) THEN 1588 RULE_ASSUM_TAC(CONV_RULE ZERO_LEFT_CONV) THEN 1589 REPEAT(FIRST_X_ASSUM ABS_ELIM_TAC1 ORELSE 1590 FIRST_ASSUM ABS_ELIM_TAC2 ORELSE 1591 FIRST_ASSUM ABS_ELIM_TAC3) THEN 1592 POP_ASSUM_LIST(ACCEPT_TAC o REAL_SIMPLE_ARITH_REFUTER) 1593 val res = tac g 1594 val _ = trace "done PURE_REAL_ARITH_TAC" 1595 in 1596 res 1597 end 1598 end; 1599 1600fun REAL_ARITH_TAC g = 1601 let 1602 val _ = trace "REAL_ARITH_TAC" 1603 val res = (POP_ASSUM_LIST(K ALL_TAC) THEN PURE_REAL_ARITH_TAC) g 1604 val _ = trace "done REAL_ARITH_TAC" 1605 in 1606 res 1607 end; 1608 1609fun REAL_ASM_ARITH_TAC g = 1610 let 1611 val _ = trace "REAL_ASM_ARITH_TAC" 1612 val res = (REPEAT (POP_ASSUM MP_TAC) THEN PURE_REAL_ARITH_TAC) g 1613 val _ = trace "done REAL_ASM_ARITH_TAC" 1614 in 1615 res 1616 end; 1617 1618(* ------------------------------------------------------------------------- *) 1619(* Rule version. *) 1620(* ------------------------------------------------------------------------- *) 1621 1622fun REAL_ARITH tm = 1623 let 1624 val _ = trace "REAL_ARITH" 1625 val res = Tactical.default_prover (tm,REAL_ARITH_TAC) 1626 val _ = trace "done REAL_ARITH" 1627 in 1628 res 1629 end; 1630 1631(* ------------------------------------------------------------------------- *) 1632 1633(*Terms to test the real linear decison procedure: 1634REAL_ARITH (Term`x + y:real = y + x`); 1635REAL_ARITH (Term`&0 < x ==> &0 <= x`); 1636REAL_ARITH (Term`x + ~x = &0`); 1637REAL_ARITH (Term`&0 <= x ==> &0 <= y ==> &0 <= x + y`); 1638REAL_ARITH (Term`&1 * x + &0 = x`); 1639REAL_ARITH (Term`&3 * x + &4 * x = &7 * x`); 1640REAL_ARITH (Term`&300 * x + &400 * x = &700 * x`); 1641REAL_ARITH (Term`x < y:real ==> x <= y`); 1642REAL_ARITH (Term`(x + z:real = y + z) ==> (x = y)`); 1643REAL_ARITH (Term`(x <= y:real /\ y <= z) ==> x <= z`); 1644REAL_ARITH (Term`x:real <= y ==> y < z ==> x < z`); 1645REAL_ARITH (Term`&0 < x /\ &0 < y ==> x + y < &1 1646 ==> &144 * x + &100 * y < &144`); 1647REAL_ARITH (Term`!x y. x <= ~y = x + y <= &0`); 1648*) 1649 1650(*---------------------------------------------------------------------------*) 1651(* Restore the ambient grammar in force when this file started executing. *) 1652(*---------------------------------------------------------------------------*) 1653 1654val _ = Parse.temp_set_grammars ambient_grammars; 1655 1656end; 1657