1(* ------------------------------------------------------------------------- *) 2(* A real simpset (includes Peano arithmetic and pairs). *) 3(* ------------------------------------------------------------------------- *) 4structure realSimps :> realSimps = 5struct 6 7open HolKernel Parse boolLib realTheory simpLib realSyntax 8 9 10(* Fix the grammar used by this file *) 11structure Parse = struct 12 open Parse 13 val (Type,Term) = parse_from_grammars realTheory.real_grammars 14end 15 16open Parse 17 18val arith_ss = boolSimps.bool_ss ++ pairSimps.PAIR_ss ++ numSimps.ARITH_ss ++ 19 numSimps.REDUCE_ss 20 21val real_SS = simpLib.SSFRAG 22 {name = SOME"real", 23 ac = [], 24 congs = [], 25 convs = [], 26 dprocs = [], 27 filter = NONE, 28 rewrs = [(* addition *) 29 REAL_ADD_LID, REAL_ADD_RID, 30 (* subtraction *) 31 REAL_SUB_REFL, REAL_SUB_RZERO, 32 (* multiplication *) 33 REAL_MUL_LID, REAL_MUL_RID, REAL_MUL_LZERO, REAL_MUL_RZERO, 34 (* division *) 35 REAL_OVER1, REAL_DIV_ADD, 36 (* less than or equal *) 37 REAL_LE_REFL, REAL_LE_01, REAL_LE_RADD, 38 (* less than *) 39 REAL_LT_01, REAL_LT_INV_EQ, 40 (* pushing out negations *) 41 REAL_NEGNEG, REAL_LE_NEG2, REAL_SUB_RNEG, REAL_NEG_SUB, 42 REAL_MUL_RNEG, REAL_MUL_LNEG, 43 (* cancellations *) 44 REAL_SUB_ADD2, REAL_MUL_SUB1_CANCEL, REAL_MUL_SUB2_CANCEL, 45 REAL_LE_SUB_CANCEL2, REAL_ADD_SUB, REAL_SUB_ADD, REAL_ADD_SUB_ALT, 46 REAL_SUB_SUB2, 47 (* halves *) 48 REAL_LT_HALF1, REAL_HALF_BETWEEN, REAL_NEG_HALF, 49 REAL_DIV_DENOM_CANCEL2, REAL_DIV_INNER_CANCEL2, 50 REAL_DIV_OUTER_CANCEL2, REAL_DIV_REFL2, 51 (* thirds *) 52 REAL_NEG_THIRD, REAL_DIV_DENOM_CANCEL3, REAL_THIRDS_BETWEEN, 53 REAL_DIV_INNER_CANCEL3, REAL_DIV_OUTER_CANCEL3, REAL_DIV_REFL3, 54 (* injections to the naturals *) 55 REAL_INJ, REAL_ADD, REAL_LE, REAL_LT, REAL_MUL, 56 (* pos *) 57 REAL_POS_EQ_ZERO, REAL_POS_POS, REAL_POS_INFLATE, 58 REAL_POS_LE_ZERO, 59 (* min *) 60 REAL_MIN_REFL, REAL_MIN_LE1, REAL_MIN_LE2, REAL_MIN_ADD, 61 REAL_MIN_SUB, 62 (* max *) 63 REAL_MAX_REFL, REAL_LE_MAX1, REAL_LE_MAX2, REAL_MAX_ADD, 64 REAL_MAX_SUB]}; 65 66val real_ac_SS = simpLib.SSFRAG { 67 name = SOME"real_ac", 68 ac = [(SPEC_ALL REAL_ADD_ASSOC, SPEC_ALL REAL_ADD_SYM), 69 (SPEC_ALL REAL_MUL_ASSOC, SPEC_ALL REAL_MUL_SYM)], 70 convs = [], 71 dprocs = [], 72 filter = NONE, 73 rewrs = [], 74 congs = []}; 75 76(* ---------------------------------------------------------------------- 77 simple calculation over the reals 78 ---------------------------------------------------------------------- *) 79 80(* there are a whole bunch of theorems at the bottom of realScript designed 81 to be used as calculational rewrites, but they are too general: with 82 a rewrite with a LHS such as x * (y/z), you will get far too many rewrites 83 happening. Instead we need to specialise these variables so that the 84 rewrites only apply when the variables look as if they're literals. 85 86 To do this, we specialise with terms of the form &v and ~&v. 87 We could go "the whole hog" here and further specialise the v's to be 88 one of either NUMERAL (BIT1 v), NUMERAL (BIT2 v) or 0, 89 but this seems over the top. 90*) 91 92 93 94val num_eq_0 = prove( 95 Term`~(NUMERAL (BIT1 n) = 0n) /\ ~(NUMERAL (BIT2 n) = 0n)`, 96 REWRITE_TAC [numeralTheory.numeral_distrib, numeralTheory.numeral_eq]); 97 98fun two_nats rv nv th = let 99 open numSyntax 100 val nb1_t = mk_injected (mk_comb(numeral_tm, mk_comb(bit1_tm, nv))) 101 val nb2_t = mk_injected (mk_comb(numeral_tm, mk_comb(bit2_tm, nv))) 102in 103 [INST [rv |-> nb1_t] th, INST [rv |-> nb2_t] th] 104end 105 106fun posnegonly rv nv th = let 107 val injected = mk_injected (mk_comb(numSyntax.numeral_tm, nv)) 108in 109 [INST [rv |-> injected] th, INST [rv |-> mk_negated injected] th] 110end 111 112fun posneg0split rv nv th = let 113 val injected = mk_injected (mk_comb(numSyntax.numeral_tm, nv)) 114in 115 [INST [rv |-> realSyntax.zero_tm] th, 116 INST [rv |-> injected] th, INST [rv |-> mk_negated injected] th] 117end 118 119datatype splitting = posneg | posneg0 | nb12 120 121fun splitfn posneg = posnegonly 122 | splitfn posneg0 = posneg0split 123 | splitfn nb12 = two_nats 124 125fun transform vs th = let 126 val T_imp = hd (CONJUNCTS (SPEC_ALL IMP_CLAUSES)) 127 val rwt = 128 REWRITE_CONV ([REAL_INJ, REAL_NEGNEG, REAL_NEG_EQ0, 129 num_eq_0, REAL_LT, REAL_LE, REAL_DIV_LZERO, 130 REAL_MUL_RZERO, REAL_MUL_LZERO, 131 REAL_ADD_LID, REAL_ADD_RID, 132 arithmeticTheory.ZERO_LESS_EQ] @ 133 (map (fn n => List.nth(CONJUNCTS le_int, n)) [1,3])) 134 fun simp t = let 135 val impconv = if is_imp t then LAND_CONV rwt THENC REWR_CONV T_imp 136 else ALL_CONV 137 in 138 impconv THENC RAND_CONV rwt 139 end t 140 val nvs = map (fn (t,_) => mk_var(#1 (dest_var t), numSyntax.num)) vs 141 142 fun recurse vs nvs th = 143 if null vs then [th] 144 else let 145 val (v,split) = hd vs 146 val nv = hd nvs 147 val newths = map (CONV_RULE simp) (splitfn split v nv th) 148 in 149 List.concat (map (recurse (tl vs) (tl nvs)) newths) 150 end 151in 152 recurse vs nvs th 153end 154 155val x = mk_var("x", real_ty) 156val y = mk_var("y", real_ty) 157val z = mk_var("z", real_ty) 158val u = mk_var("u", real_ty) 159val v = mk_var("v", real_ty) 160 161val add_rats = 162 transform [(x, posneg), (y, nb12), (u, posneg), (v, nb12)] add_rat 163val add_ratls = transform [(x, posneg), (y,nb12), (z, posneg0)] add_ratl 164val add_ratrs = transform [(x, posneg0), (y, posneg), (z, nb12)] add_ratr 165 166val mult_rats = 167 transform [(x,posneg), (y, nb12), (u, posneg), (v, nb12)] mult_rat 168val mult_ratls = transform [(x, posneg), (y, nb12), (z, posneg0)] mult_ratl 169val mult_ratrs = transform [(x, posneg0), (y, posneg), (z, nb12)] mult_ratr 170 171val neg_ths = REAL_NEG_0 :: transform [(y, nb12)] neg_rat 172 173val sub1 = SPECL [mk_div(x,y), mk_div(u,v)] real_sub 174val sub1 = transform [(x, posneg), (y, nb12), (u, posneg), (v, nb12)] sub1 175val sub2 = SPECL [x, mk_div(u,v)] real_sub 176val sub2 = transform [(x, posneg0), (u, posneg), (v, nb12)] sub2 177val sub3 = SPECL [mk_div(x,y), z] real_sub 178val sub3 = transform [(x, posneg), (y, nb12), (z, posneg0)] sub3 179val sub4 = transform [(x, posneg0), (y, posneg0)] (SPEC_ALL real_sub) 180 181val div_rats = transform [(x, posneg), (y, nb12), (u, posneg), (v, nb12)] div_rat 182val div_ratls = transform [(x, posneg), (y, nb12), (z, nb12)] div_ratl 183val div_ratrs = transform [(x, posneg), (z, nb12), (y, posneg)] div_ratr 184val div_eq_1 = transform [(x, nb12)] (SPEC_ALL REAL_DIV_REFL) 185 186val max_ints = transform [(x, posneg0), (y, posneg0)] (SPEC_ALL max_def) 187val min_ints = transform [(x, posneg0), (y, posneg0)] (SPEC_ALL min_def) 188val max_rats = 189 transform [(x, posneg), (y, nb12), (u, posneg), (v, nb12)] 190 (SPECL [mk_div(x,y), mk_div(u,v)] max_def) 191val max_ratls = 192 transform [(x, posneg), (y, nb12), (u, posneg0)] 193 (SPECL [mk_div(x,y), u] max_def) 194val max_ratrs = 195 transform [(x, posneg), (y, nb12), (u, posneg0)] 196 (SPECL [u, mk_div(x,y)] max_def) 197val min_rats = 198 transform [(x, posneg), (y, nb12), (u, posneg), (v, nb12)] 199 (SPECL [mk_div(x,y), mk_div(u,v)] min_def) 200val min_ratls = 201 transform [(x, posneg), (y, nb12), (u, posneg0)] 202 (SPECL [mk_div(x,y), u] min_def) 203val min_ratrs = 204 transform [(x, posneg), (y, nb12), (u, posneg0)] 205 (SPECL [u, mk_div(x,y)] min_def) 206 207local 208 val (a, b, c, d) = 209 Lib.quadruple_of_list (Drule.CONJUNCTS realTheory.NUM_FLOOR_EQNS) 210 val rule = REWRITE_RULE [GSYM arithmeticTheory.NOT_ZERO_LT_ZERO, num_eq_0] 211 val r1 = rule o Q.INST [`m` |-> `NUMERAL (BIT1 m)`] 212 val r2 = rule o Q.INST [`m` |-> `NUMERAL (BIT2 m)`] 213in 214 val flr = Drule.LIST_CONJ [a, b, r1 c, r2 c, r1 d, r2 d] 215end 216 217val abs1 = SPEC (mk_div(x,y)) realTheory.abs 218val abs1 = transform [(x,posneg), (y, nb12)] abs1 219val abs2 = SPEC x realTheory.abs 220val abs2 = transform [(x,posneg)] abs2 221 222val n = mk_var("n", numSyntax.num) 223val m = mk_var("m", numSyntax.num) 224fun to_numeraln th = INST [n |-> mk_comb(numSyntax.numeral_tm, n), 225 m |-> mk_comb(numSyntax.numeral_tm, m)] th 226 227val op_rwts = 228 [to_numeraln mult_ints, to_numeraln add_ints, flr, NUM_CEILING_NUM_FLOOR, 229 REAL_DIV_LZERO, REAL_NEGNEG] @ 230 transform [(x,posneg0)] (SPEC_ALL REAL_ADD_LID) @ 231 transform [(x,posneg)] (SPEC_ALL REAL_ADD_RID) @ 232 transform [(x,posneg0)] (SPEC_ALL REAL_MUL_LZERO) @ 233 transform [(x,posneg)] (SPEC_ALL REAL_MUL_RZERO) @ 234 neg_ths @ 235 add_rats @ add_ratls @ add_ratrs @ 236 mult_rats @ mult_ratls @ mult_ratrs @ 237 sub1 @ sub2 @ sub3 @ sub4 @ 238 div_rats @ div_ratls @ div_ratrs @ div_eq_1 @ 239 max_ratls @ max_ratrs @ max_rats @ max_ints @ 240 min_ratls @ min_ratrs @ min_rats @ min_ints @ 241 (realTheory.REAL_ABS_0 :: abs1) @ abs2 242 243fun nat2nat th = let 244 val simp = REWRITE_RULE [REAL_INJ, REAL_NEGNEG, REAL_NEG_EQ0, num_eq_0] 245 val th0 = 246 if free_in ``n:num`` (concl th) then 247 map simp ([INST [``n:num`` |-> ``NUMERAL (BIT1 n)``] th, 248 INST [``n:num`` |-> ``NUMERAL (BIT2 n)``] th]) 249 else [th] 250in 251 if free_in ``m:num`` (concl th) then 252 List.concat 253 (map (fn th => map simp 254 [INST [``m:num`` |-> ``NUMERAL(BIT1 m)``] th, 255 INST [``m:num`` |-> ``NUMERAL(BIT2 m)``] th]) 256 th0) 257 else th0 258end 259 260val lt_rats = 261 List.concat (map (transform [(x,posneg), (u,posneg)]) (nat2nat lt_rat)) 262val lt_ratls = 263 List.concat (map (transform [(x,posneg), (u,posneg0)]) (nat2nat lt_ratl)) 264val lt_ratrs = 265 List.concat (map (transform [(x,posneg0), (u,posneg)]) (nat2nat lt_ratr)) 266 267val le_rats = 268 List.concat (map (transform [(x,posneg), (u,posneg)]) (nat2nat le_rat)) 269val le_ratls = 270 List.concat (map (transform [(x,posneg), (u,posneg0)]) (nat2nat le_ratl)) 271val le_ratrs = 272 List.concat (map (transform [(x,posneg0), (u,posneg)]) (nat2nat le_ratr)) 273 274val eq_rats = transform [(x, posneg), (y, nb12), (u, posneg), (v, nb12)] eq_rat 275val eq_ratls = transform [(x, posneg), (y, nb12), (z, posneg0)] eq_ratl 276val eq_ratrs = transform [(x, posneg), (y, nb12), (z, posneg0)] eq_ratr 277 278val real_gts = transform [(x, posneg0), (y, posneg0)] (SPEC_ALL real_gt) 279val real_ges = transform [(x, posneg0), (y, posneg0)] (SPEC_ALL real_ge) 280 281val real_gt_rats = 282 transform [(x, posneg), (y, nb12), (u, posneg), (v, nb12)] 283 (SPECL [mk_div(x,y), mk_div(u,v)] real_gt) 284val real_gt_ratls = 285 transform [(x, posneg), (y, nb12), (u, posneg0)] 286 (SPECL [mk_div(x,y), u] real_gt) 287val real_gt_ratrs = 288 transform [(x, posneg), (y, nb12), (u, posneg0)] 289 (SPECL [u, mk_div(x,y)] real_gt) 290 291val real_ge_rats = 292 transform [(x, posneg), (y, nb12), (u, posneg), (v, nb12)] 293 (SPECL [mk_div(x,y), mk_div(u,v)] real_ge) 294val real_ge_ratls = 295 transform [(x, posneg), (y, nb12), (u, posneg0)] 296 (SPECL [mk_div(x,y), u] real_ge) 297val real_ge_ratrs = 298 transform [(x, posneg), (y, nb12), (u, posneg0)] 299 (SPECL [u, mk_div(x,y)] real_ge) 300 301val rel_rwts = [eq_ints, le_int, lt_int] @ 302 eq_rats @ eq_ratls @ eq_ratrs @ 303 lt_rats @ lt_ratls @ lt_ratrs @ 304 le_rats @ le_ratrs @ le_ratls @ 305 real_gts @ real_gt_rats @ real_gt_ratls @ real_gt_ratrs @ 306 real_ges @ real_ge_rats @ real_ge_ratls @ real_ge_ratrs 307 308val rwts = pow_rat :: (op_rwts @ rel_rwts) 309 310val n_compset = reduceLib.num_compset() 311val _ = computeLib.add_thms (mult_ints:: mult_rats) n_compset 312 313fun elim_common_factor t = let 314 open realSyntax Arbint 315 val (n,d) = dest_div t 316 val n_i = int_of_term n 317in 318 if n_i = zero then REWR_CONV REAL_DIV_LZERO t 319 else let 320 val d_i = int_of_term d 321 val _ = d_i > zero orelse 322 raise mk_HOL_ERR "realSimps" "elim_common_factor" 323 "denominator must be positive" 324 val g = fromNat (Arbnum.gcd (toNat (abs n_i), toNat (abs d_i))) 325 val _ = g <> one orelse 326 raise mk_HOL_ERR "realSimps" "elim_common_factor" 327 "No common factor" 328 val frac_1 = mk_div(term_of_int g, term_of_int g) 329 val frac_new_t = mk_div(term_of_int (n_i div g), term_of_int (d_i div g)) 330 val mul_t = mk_mult(frac_new_t, frac_1) 331 val eqn1 = computeLib.CBV_CONV n_compset mul_t 332 val frac_1_eq_1 = FIRST_CONV (map REWR_CONV div_eq_1) frac_1 333 val eqn2 = 334 TRANS (SYM eqn1) (AP_TERM(mk_comb(mult_tm, frac_new_t)) frac_1_eq_1) 335 in 336 CONV_RULE (RAND_CONV (REWR_CONV REAL_MUL_RID THENC 337 TRY_CONV (REWR_CONV REAL_OVER1))) 338 eqn2 339 end 340end 341 342 343val ecf_patterns = [Term`&(NUMERAL n) / &(NUMERAL (BIT1 m))`, 344 Term`&(NUMERAL n) / &(NUMERAL (BIT2 m))`, 345 Term`~&(NUMERAL n) / &(NUMERAL (BIT1 m))`, 346 Term`~&(NUMERAL n) / &(NUMERAL (BIT2 m))`] 347 348val simpset_convs = map (fn p => {conv = K (K elim_common_factor), 349 key = SOME ([], p), 350 name = "realSimps.elim_common_factor", 351 trace = 2}) ecf_patterns 352 353val REAL_REDUCE_ss = SSFRAG 354 {name = SOME "REAL_REDUCE", 355 ac = [], congs =[], 356 convs = simpset_convs, 357 dprocs = [], filter = NONE, 358 rewrs = rwts} 359 360val real_ss = arith_ss ++ real_SS ++ REAL_REDUCE_ss 361 362val real_ac_ss = real_ss ++ real_ac_SS 363 364fun real_compset () = let 365 open computeLib 366 val compset = reduceLib.num_compset() 367 val _ = add_thms rwts compset 368 val _ = add_conv (div_tm, 2, elim_common_factor) compset 369in 370 compset 371end 372 373(* add real calculation facilities to global functionality *) 374val _ = let open computeLib in 375 add_funs rwts ; 376 add_convs [(div_tm, 2, elim_common_factor)] 377 end 378 379val _ = BasicProvers.augment_srw_ss [REAL_REDUCE_ss] 380 381(* ---------------------------------------------------------------------- 382 REAL_ARITH_ss 383 384 embedding RealArith into a simpset fragment. 385 Derived from code to do the same for the natural numbers, which is in 386 src/num/arith/src/numSimps.sml 387 and 388 src/num/arith/src/Gen_arith.sml 389 ---------------------------------------------------------------------- *) 390 391fun contains_var tm = 392 if is_var tm then true 393 else if is_real_literal tm then false 394 else let 395 val (l, r) = dest_plus tm 396 handle HOL_ERR _ => 397 dest_mult tm 398 handle HOL_ERR _ => dest_minus tm 399 in 400 contains_var l orelse contains_var r 401 end handle HOL_ERR _ => contains_var (dest_absval tm) 402 handle HOL_ERR _ => true 403 (* final default value is true because the term in question must be a 404 complicated non-presburger thing that will get treated as a variable 405 anyway. *) 406 407fun is_linear_mult tm = let 408 val (l,r) = dest_mult tm 409in 410 not (contains_var l andalso contains_var r) 411end 412 413fun arg1 tm = rand (rator tm) 414val arg2 = rand 415 416fun non_presburger_subterms tm = 417 (non_presburger_subterms (#2 (dest_forall tm))) handle _ => 418 (non_presburger_subterms (dest_neg tm)) handle _ => 419 (if (is_conj tm) orelse (is_disj tm) orelse (is_imp tm) orelse 420 (is_eq tm) orelse 421 (is_less tm) orelse (is_leq tm) orelse 422 (is_great tm) orelse (is_geq tm) orelse 423 (is_plus tm) orelse (is_minus tm) orelse 424 (is_linear_mult tm handle _ => false) 425 then Lib.union (non_presburger_subterms (arg1 tm)) 426 (non_presburger_subterms (arg2 tm)) 427 else if (is_real_literal tm) then [] 428 else [tm]); 429 430fun is_num_var tm = is_var tm andalso type_of tm = real_ty 431val is_presburger = (all is_num_var) o non_presburger_subterms; 432 433 434 435fun cond_has_arith_components tm = 436 if boolSyntax.is_cond tm then let 437 val {cond,rarm,larm} = Rsyntax.dest_cond tm 438 in 439 List.all is_arith [cond, rarm, larm] 440 end 441 else true 442and is_arith tm = 443 is_presburger tm orelse 444 List.all (fn t => type_of t = real_ty andalso cond_has_arith_components t) 445 (non_presburger_subterms tm) 446 447fun contains_forall sense tm = 448 if is_conj tm orelse is_disj tm then 449 List.exists (contains_forall sense) (#2 (strip_comb tm)) 450 else if is_neg tm then 451 contains_forall (not sense) (rand tm) 452 else if is_imp tm then 453 contains_forall (not sense) (rand (rator tm)) orelse 454 contains_forall sense (rand tm) 455 else if is_forall tm then 456 sense orelse contains_forall sense (#2 (dest_forall tm)) 457 else if is_exists tm then 458 not sense orelse contains_forall sense (#2 (dest_exists tm)) 459 else false 460 461(* This function determines whether or not to add something as context 462 to the arithmetic decision procedure. Because the d.p. can't 463 handle implications with nested foralls on the left hand side, we 464 eliminate those here. More generally, we can't allow the formula 465 to be added to have any positive universals, because these will 466 translate into negative ones in the context of the wider goal, and 467 thus cause the goal to be rejected. *) 468 469fun is_arith_thm thm = 470 not (null (hyp thm)) andalso is_arith (concl thm) andalso 471 (not (contains_forall true (concl thm))); 472 473val is_arith_asm = is_arith_thm o ASSUME 474 475val ARITH = RealArith.REAL_ARITH 476 477open Trace Cache Traverse 478fun CTXT_ARITH thms tm = let 479 val context = map concl thms 480 fun try gl = let 481 val gl' = list_mk_imp(context,gl) 482 val _ = trace (5, LZ_TEXT (fn () => "Trying cached arithmetic d.p. on "^ 483 term_to_string gl')) 484 in 485 rev_itlist (C MP) thms (ARITH gl') 486 end 487 val thm = EQT_INTRO (try tm) 488 handle (e as HOL_ERR _) => 489 if tm <> F then EQF_INTRO (try(mk_neg tm)) else raise e 490in 491 trace(1,PRODUCE(tm,"REAL_ARITH",thm)); thm 492end 493 494fun crossprod (ll : 'a list list) : 'a list list = 495 case ll of 496 [] => [[]] 497 | h::t => let 498 val c = crossprod t 499 in 500 List.concat (map (fn hel => map (cons hel) c) h) 501 end 502fun prim_dest_const t = let 503 val {Thy,Name,...} = dest_thy_const t 504in 505 (Thy,Name) 506end 507 508fun dpvars t = let 509 fun recurse bnds acc t = let 510 val (f, args) = strip_comb t 511 fun go2() = let 512 val (t1, t2) = (hd args, hd (tl args)) 513 in 514 recurse bnds (recurse bnds acc t1) t2 515 end 516 fun go1 () = recurse bnds acc (hd args) 517 in 518 case Lib.total prim_dest_const f of 519 SOME ("bool", "~") => go1() 520 | SOME ("bool", "/\\") => go2() 521 | SOME ("bool", "\\/") => go2() 522 | SOME ("min", "==>") => go2() 523 | SOME ("min", "=") => go2() 524 | SOME ("bool", "COND") => let 525 val (t1,t2,t3) = (hd args, hd (tl args), hd (tl (tl args))) 526 in 527 recurse bnds (recurse bnds (recurse bnds acc t1) t2) t3 528 end 529 | SOME ("realax", "real_add") => go2() 530 | SOME ("real", "real_sub") => go2() 531 | SOME ("real", "real_gt") => go2() 532 | SOME ("realax", "real_lt") => go2() 533 | SOME ("real", "real_lte") => go2() 534 | SOME ("real", "real_ge") => go2() 535 | SOME ("realax", "real_neg") => go1() 536 | SOME ("real", "abs") => go1() 537 | SOME ("realax", "real_mul") => let 538 val args = realSyntax.strip_mult t 539 val arg_vs = map (HOLset.listItems o recurse bnds empty_tmset) args 540 val cs = crossprod (filter (not o null) arg_vs) 541 val var_ts = map (realSyntax.list_mk_mult o Listsort.sort Term.compare) 542 cs 543 in 544 List.foldl (fn (t,acc)=>HOLset.add(acc,t)) acc var_ts 545 end 546 | SOME ("bool", "!") => let 547 val (v, bod) = dest_abs (hd args) 548 in 549 recurse (HOLset.add(bnds, v)) acc bod 550 end 551 | SOME ("bool", "?") => let 552 val (v, bod) = dest_abs (hd args) 553 in 554 recurse (HOLset.add(bnds, v)) acc bod 555 end 556 | SOME _ => if realSyntax.is_real_literal t then acc 557 else HOLset.add(acc, t) 558 | NONE => if is_var t then if HOLset.member(bnds, t) then acc 559 else HOLset.add(acc, t) 560 else HOLset.add(acc, t) 561 end 562in 563 HOLset.listItems (recurse empty_tmset empty_tmset t) 564end 565 566 567val (CACHED_ARITH,arith_cache) = let 568 fun check tm = 569 let val ty = type_of tm 570 in 571 (ty=Type.bool andalso (is_arith tm orelse tm = F)) 572 end; 573in 574 RCACHE (dpvars, check,CTXT_ARITH) 575 (* the check function determines whether or not a term might be handled 576 by the decision procedure -- we want to handle F, because it's possible 577 that we have accumulated a contradictory context. *) 578end; 579 580val ARITH_REDUCER = let 581 exception CTXT of thm list; 582 fun get_ctxt e = (raise e) handle CTXT c => c 583 fun add_ctxt(ctxt, newthms) = let 584 val addthese = filter is_arith_thm (flatten (map CONJUNCTS newthms)) 585 in 586 CTXT (addthese @ get_ctxt ctxt) 587 end 588in 589 REDUCER {name = SOME"ARITH_REDUCER", 590 addcontext = add_ctxt, 591 apply = fn args => CACHED_ARITH (get_ctxt (#context args)), 592 initial = CTXT []} 593end; 594 595val REAL_ARITH_ss = 596 SSFRAG 597 {name=SOME"REAL_ARITH", 598 convs = [], rewrs = [], congs = [], 599 filter = NONE, ac = [], dprocs = [ARITH_REDUCER]}; 600 601end 602