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 = map (fn s => (SOME {Thy = "real", Name = s}, DB.fetch "real" s)) [ 29 (* addition *) 30 "REAL_ADD_LID", "REAL_ADD_RID", 31 (* subtraction *) 32 "REAL_SUB_REFL", "REAL_SUB_RZERO", 33 (* multiplication *) 34 "REAL_MUL_LID", "REAL_MUL_RID", "REAL_MUL_LZERO", "REAL_MUL_RZERO", 35 (* division *) 36 "REAL_OVER1", "REAL_DIV_ADD", 37 (* less than or equal *) 38 "REAL_LE_REFL", "REAL_LE_01", "REAL_LE_RADD", 39 (* less than *) 40 "REAL_LT_01", "REAL_LT_INV_EQ", 41 (* pushing out negations *) 42 "REAL_NEGNEG", "REAL_LE_NEG2", "REAL_SUB_RNEG", "REAL_NEG_SUB", 43 "REAL_MUL_RNEG", "REAL_MUL_LNEG", 44 (* cancellations *) 45 "REAL_SUB_ADD2", "REAL_MUL_SUB1_CANCEL", "REAL_MUL_SUB2_CANCEL", 46 "REAL_LE_SUB_CANCEL2", "REAL_ADD_SUB", "REAL_SUB_ADD", "REAL_ADD_SUB_ALT", 47 "REAL_SUB_SUB2", 48 (* halves *) 49 "REAL_LT_HALF1", "REAL_HALF_BETWEEN", "REAL_NEG_HALF", 50 "REAL_DIV_DENOM_CANCEL2", "REAL_DIV_INNER_CANCEL2", 51 "REAL_DIV_OUTER_CANCEL2", "REAL_DIV_REFL2", 52 (* thirds *) 53 "REAL_NEG_THIRD", "REAL_DIV_DENOM_CANCEL3", "REAL_THIRDS_BETWEEN", 54 "REAL_DIV_INNER_CANCEL3", "REAL_DIV_OUTER_CANCEL3", "REAL_DIV_REFL3", 55 (* injections to the naturals *) 56 "REAL_INJ", "REAL_ADD", "REAL_LE", "REAL_LT", "REAL_MUL", 57 (* pos *) 58 "REAL_POS_EQ_ZERO", "REAL_POS_POS", "REAL_POS_INFLATE", 59 "REAL_POS_LE_ZERO", 60 (* min *) 61 "REAL_MIN_REFL", "REAL_MIN_LE1", "REAL_MIN_LE2", "REAL_MIN_ADD", 62 "REAL_MIN_SUB", 63 (* max *) 64 "REAL_MAX_REFL", "REAL_LE_MAX1", "REAL_LE_MAX2", "REAL_MAX_ADD", 65 "REAL_MAX_SUB"]}; 66 67val real_ac_SS = simpLib.SSFRAG { 68 name = SOME"real_ac", 69 ac = [(SPEC_ALL REAL_ADD_ASSOC, SPEC_ALL REAL_ADD_SYM), 70 (SPEC_ALL REAL_MUL_ASSOC, SPEC_ALL REAL_MUL_SYM)], 71 convs = [], 72 dprocs = [], 73 filter = NONE, 74 rewrs = [], 75 congs = []}; 76 77(* ---------------------------------------------------------------------- 78 simple calculation over the reals 79 ---------------------------------------------------------------------- *) 80 81(* there are a whole bunch of theorems at the bottom of realScript designed 82 to be used as calculational rewrites, but they are too general: with 83 a rewrite with a LHS such as x * (y/z), you will get far too many rewrites 84 happening. Instead we need to specialise these variables so that the 85 rewrites only apply when the variables look as if they're literals. 86 87 To do this, we specialise with terms of the form &v and ~&v. 88 We could go "the whole hog" here and further specialise the v's to be 89 one of either NUMERAL (BIT1 v), NUMERAL (BIT2 v) or 0, 90 but this seems over the top. 91*) 92 93 94 95val num_eq_0 = prove( 96 Term`~(NUMERAL (BIT1 n) = 0n) /\ ~(NUMERAL (BIT2 n) = 0n)`, 97 REWRITE_TAC [numeralTheory.numeral_distrib, numeralTheory.numeral_eq]); 98 99fun two_nats rv nv th = let 100 open numSyntax 101 val nb1_t = mk_injected (mk_comb(numeral_tm, mk_comb(bit1_tm, nv))) 102 val nb2_t = mk_injected (mk_comb(numeral_tm, mk_comb(bit2_tm, nv))) 103in 104 [INST [rv |-> nb1_t] th, INST [rv |-> nb2_t] th] 105end 106 107fun posnegonly rv nv th = let 108 val injected = mk_injected (mk_comb(numSyntax.numeral_tm, nv)) 109in 110 [INST [rv |-> injected] th, INST [rv |-> mk_negated injected] th] 111end 112 113fun posneg0split rv nv th = let 114 val injected = mk_injected (mk_comb(numSyntax.numeral_tm, nv)) 115in 116 [INST [rv |-> realSyntax.zero_tm] th, 117 INST [rv |-> injected] th, INST [rv |-> mk_negated injected] th] 118end 119 120datatype splitting = posneg | posneg0 | nb12 121 122fun splitfn posneg = posnegonly 123 | splitfn posneg0 = posneg0split 124 | splitfn nb12 = two_nats 125 126fun transform vs th = let 127 val T_imp = hd (CONJUNCTS (SPEC_ALL IMP_CLAUSES)) 128 val rwt = 129 REWRITE_CONV ([REAL_INJ, REAL_NEGNEG, REAL_NEG_EQ0, 130 num_eq_0, REAL_LT, REAL_LE, REAL_DIV_LZERO, 131 REAL_MUL_RZERO, REAL_MUL_LZERO, 132 REAL_ADD_LID, REAL_ADD_RID, 133 arithmeticTheory.ZERO_LESS_EQ] @ 134 (map (fn n => List.nth(CONJUNCTS le_int, n)) [1,3])) 135 fun simp t = let 136 val impconv = if is_imp t then LAND_CONV rwt THENC REWR_CONV T_imp 137 else ALL_CONV 138 in 139 impconv THENC RAND_CONV rwt 140 end t 141 val nvs = map (fn (t,_) => mk_var(#1 (dest_var t), numSyntax.num)) vs 142 143 fun recurse vs nvs th = 144 if null vs then [th] 145 else let 146 val (v,split) = hd vs 147 val nv = hd nvs 148 val newths = map (CONV_RULE simp) (splitfn split v nv th) 149 in 150 List.concat (map (recurse (tl vs) (tl nvs)) newths) 151 end 152in 153 recurse vs nvs th 154end 155 156val x = mk_var("x", real_ty) 157val y = mk_var("y", real_ty) 158val z = mk_var("z", real_ty) 159val u = mk_var("u", real_ty) 160val v = mk_var("v", real_ty) 161 162val add_rats = 163 transform [(x, posneg), (y, nb12), (u, posneg), (v, nb12)] add_rat 164val add_ratls = transform [(x, posneg), (y,nb12), (z, posneg0)] add_ratl 165val add_ratrs = transform [(x, posneg0), (y, posneg), (z, nb12)] add_ratr 166 167val mult_rats = 168 transform [(x,posneg), (y, nb12), (u, posneg), (v, nb12)] mult_rat 169val mult_ratls = transform [(x, posneg), (y, nb12), (z, posneg0)] mult_ratl 170val mult_ratrs = transform [(x, posneg0), (y, posneg), (z, nb12)] mult_ratr 171 172val neg_ths = REAL_NEG_0 :: transform [(y, nb12)] neg_rat 173 174val sub1 = SPECL [mk_div(x,y), mk_div(u,v)] real_sub 175val sub1 = transform [(x, posneg), (y, nb12), (u, posneg), (v, nb12)] sub1 176val sub2 = SPECL [x, mk_div(u,v)] real_sub 177val sub2 = transform [(x, posneg0), (u, posneg), (v, nb12)] sub2 178val sub3 = SPECL [mk_div(x,y), z] real_sub 179val sub3 = transform [(x, posneg), (y, nb12), (z, posneg0)] sub3 180val sub4 = transform [(x, posneg0), (y, posneg0)] (SPEC_ALL real_sub) 181 182val div_rats = transform [(x, posneg), (y, nb12), (u, posneg), (v, nb12)] div_rat 183val div_ratls = transform [(x, posneg), (y, nb12), (z, nb12)] div_ratl 184val div_ratrs = transform [(x, posneg), (z, nb12), (y, posneg)] div_ratr 185val div_eq_1 = transform [(x, nb12)] (SPEC_ALL REAL_DIV_REFL) 186 187val max_ints = transform [(x, posneg0), (y, posneg0)] (SPEC_ALL max_def) 188val min_ints = transform [(x, posneg0), (y, posneg0)] (SPEC_ALL min_def) 189val max_rats = 190 transform [(x, posneg), (y, nb12), (u, posneg), (v, nb12)] 191 (SPECL [mk_div(x,y), mk_div(u,v)] max_def) 192val max_ratls = 193 transform [(x, posneg), (y, nb12), (u, posneg0)] 194 (SPECL [mk_div(x,y), u] max_def) 195val max_ratrs = 196 transform [(x, posneg), (y, nb12), (u, posneg0)] 197 (SPECL [u, mk_div(x,y)] max_def) 198val min_rats = 199 transform [(x, posneg), (y, nb12), (u, posneg), (v, nb12)] 200 (SPECL [mk_div(x,y), mk_div(u,v)] min_def) 201val min_ratls = 202 transform [(x, posneg), (y, nb12), (u, posneg0)] 203 (SPECL [mk_div(x,y), u] min_def) 204val min_ratrs = 205 transform [(x, posneg), (y, nb12), (u, posneg0)] 206 (SPECL [u, mk_div(x,y)] min_def) 207 208local 209 val (a, b, c, d) = 210 Lib.quadruple_of_list (Drule.CONJUNCTS realTheory.NUM_FLOOR_EQNS) 211 val rule = REWRITE_RULE [GSYM arithmeticTheory.NOT_ZERO_LT_ZERO, num_eq_0] 212 val r1 = rule o Q.INST [`m` |-> `NUMERAL (BIT1 m)`] 213 val r2 = rule o Q.INST [`m` |-> `NUMERAL (BIT2 m)`] 214in 215 val flr = Drule.LIST_CONJ [a, b, r1 c, r2 c, r1 d, r2 d] 216end 217 218val abs1 = SPEC (mk_div(x,y)) realTheory.abs 219val abs1 = transform [(x,posneg), (y, nb12)] abs1 220val abs2 = SPEC x realTheory.abs 221val abs2 = transform [(x,posneg)] abs2 222 223val n = mk_var("n", numSyntax.num) 224val m = mk_var("m", numSyntax.num) 225fun to_numeraln th = INST [n |-> mk_comb(numSyntax.numeral_tm, n), 226 m |-> mk_comb(numSyntax.numeral_tm, m)] th 227 228val op_rwts = 229 [to_numeraln mult_ints, to_numeraln add_ints, flr, NUM_CEILING_NUM_FLOOR, 230 REAL_DIV_LZERO, REAL_NEGNEG] @ 231 transform [(x,posneg0)] (SPEC_ALL REAL_ADD_LID) @ 232 transform [(x,posneg)] (SPEC_ALL REAL_ADD_RID) @ 233 transform [(x,posneg0)] (SPEC_ALL REAL_MUL_LZERO) @ 234 transform [(x,posneg)] (SPEC_ALL REAL_MUL_RZERO) @ 235 neg_ths @ 236 add_rats @ add_ratls @ add_ratrs @ 237 mult_rats @ mult_ratls @ mult_ratrs @ 238 sub1 @ sub2 @ sub3 @ sub4 @ 239 div_rats @ div_ratls @ div_ratrs @ div_eq_1 @ 240 max_ratls @ max_ratrs @ max_rats @ max_ints @ 241 min_ratls @ min_ratrs @ min_rats @ min_ints @ 242 (realTheory.REAL_ABS_0 :: abs1) @ abs2 243 244fun nat2nat th = let 245 val simp = REWRITE_RULE [REAL_INJ, REAL_NEGNEG, REAL_NEG_EQ0, num_eq_0] 246 val th0 = 247 if free_in ``n:num`` (concl th) then 248 map simp ([INST [``n:num`` |-> ``NUMERAL (BIT1 n)``] th, 249 INST [``n:num`` |-> ``NUMERAL (BIT2 n)``] th]) 250 else [th] 251in 252 if free_in ``m:num`` (concl th) then 253 List.concat 254 (map (fn th => map simp 255 [INST [``m:num`` |-> ``NUMERAL(BIT1 m)``] th, 256 INST [``m:num`` |-> ``NUMERAL(BIT2 m)``] th]) 257 th0) 258 else th0 259end 260 261val lt_rats = 262 List.concat (map (transform [(x,posneg), (u,posneg)]) (nat2nat lt_rat)) 263val lt_ratls = 264 List.concat (map (transform [(x,posneg), (u,posneg0)]) (nat2nat lt_ratl)) 265val lt_ratrs = 266 List.concat (map (transform [(x,posneg0), (u,posneg)]) (nat2nat lt_ratr)) 267 268val le_rats = 269 List.concat (map (transform [(x,posneg), (u,posneg)]) (nat2nat le_rat)) 270val le_ratls = 271 List.concat (map (transform [(x,posneg), (u,posneg0)]) (nat2nat le_ratl)) 272val le_ratrs = 273 List.concat (map (transform [(x,posneg0), (u,posneg)]) (nat2nat le_ratr)) 274 275val eq_rats = transform [(x, posneg), (y, nb12), (u, posneg), (v, nb12)] eq_rat 276val eq_ratls = transform [(x, posneg), (y, nb12), (z, posneg0)] eq_ratl 277val eq_ratrs = transform [(x, posneg), (y, nb12), (z, posneg0)] eq_ratr 278 279val real_gts = transform [(x, posneg0), (y, posneg0)] (SPEC_ALL real_gt) 280val real_ges = transform [(x, posneg0), (y, posneg0)] (SPEC_ALL real_ge) 281 282val real_gt_rats = 283 transform [(x, posneg), (y, nb12), (u, posneg), (v, nb12)] 284 (SPECL [mk_div(x,y), mk_div(u,v)] real_gt) 285val real_gt_ratls = 286 transform [(x, posneg), (y, nb12), (u, posneg0)] 287 (SPECL [mk_div(x,y), u] real_gt) 288val real_gt_ratrs = 289 transform [(x, posneg), (y, nb12), (u, posneg0)] 290 (SPECL [u, mk_div(x,y)] real_gt) 291 292val real_ge_rats = 293 transform [(x, posneg), (y, nb12), (u, posneg), (v, nb12)] 294 (SPECL [mk_div(x,y), mk_div(u,v)] real_ge) 295val real_ge_ratls = 296 transform [(x, posneg), (y, nb12), (u, posneg0)] 297 (SPECL [mk_div(x,y), u] real_ge) 298val real_ge_ratrs = 299 transform [(x, posneg), (y, nb12), (u, posneg0)] 300 (SPECL [u, mk_div(x,y)] real_ge) 301 302val rel_rwts = [eq_ints, le_int, lt_int] @ 303 eq_rats @ eq_ratls @ eq_ratrs @ 304 lt_rats @ lt_ratls @ lt_ratrs @ 305 le_rats @ le_ratrs @ le_ratls @ 306 real_gts @ real_gt_rats @ real_gt_ratls @ real_gt_ratrs @ 307 real_ges @ real_ge_rats @ real_ge_ratls @ real_ge_ratrs 308 309val rwts = pow_rat :: (op_rwts @ rel_rwts) 310 311val n_compset = reduceLib.num_compset() 312val _ = computeLib.add_thms (mult_ints:: mult_rats) n_compset 313 314fun elim_common_factor t = let 315 open realSyntax Arbint 316 val (n,d) = dest_div t 317 val n_i = int_of_term n 318in 319 if n_i = zero then REWR_CONV REAL_DIV_LZERO t 320 else let 321 val d_i = int_of_term d 322 val _ = d_i > zero orelse 323 raise mk_HOL_ERR "realSimps" "elim_common_factor" 324 "denominator must be positive" 325 val g = fromNat (Arbnum.gcd (toNat (abs n_i), toNat (abs d_i))) 326 val _ = g <> one orelse 327 raise mk_HOL_ERR "realSimps" "elim_common_factor" 328 "No common factor" 329 val frac_1 = mk_div(term_of_int g, term_of_int g) 330 val frac_new_t = mk_div(term_of_int (n_i div g), term_of_int (d_i div g)) 331 val mul_t = mk_mult(frac_new_t, frac_1) 332 val eqn1 = computeLib.CBV_CONV n_compset mul_t 333 val frac_1_eq_1 = FIRST_CONV (map REWR_CONV div_eq_1) frac_1 334 val eqn2 = 335 TRANS (SYM eqn1) (AP_TERM(mk_comb(mult_tm, frac_new_t)) frac_1_eq_1) 336 in 337 CONV_RULE (RAND_CONV (REWR_CONV REAL_MUL_RID THENC 338 TRY_CONV (REWR_CONV REAL_OVER1))) 339 eqn2 340 end 341end 342 343 344val ecf_patterns = [Term`&(NUMERAL n) / &(NUMERAL (BIT1 m))`, 345 Term`&(NUMERAL n) / &(NUMERAL (BIT2 m))`, 346 Term`~&(NUMERAL n) / &(NUMERAL (BIT1 m))`, 347 Term`~&(NUMERAL n) / &(NUMERAL (BIT2 m))`] 348 349val simpset_convs = map (fn p => {conv = K (K elim_common_factor), 350 key = SOME ([], p), 351 name = "realSimps.elim_common_factor", 352 trace = 2}) ecf_patterns 353 354val REAL_REDUCE_ss = SSFRAG 355 {name = SOME "REAL_REDUCE", 356 ac = [], congs =[], 357 convs = simpset_convs, 358 dprocs = [], filter = NONE, 359 rewrs = map (fn th => (NONE, th)) rwts} 360 361val real_ss = arith_ss ++ real_SS ++ REAL_REDUCE_ss 362 363val real_ac_ss = real_ss ++ real_ac_SS 364 365fun real_compset () = let 366 open computeLib 367 val compset = reduceLib.num_compset() 368 val _ = add_thms rwts compset 369 val _ = add_conv (div_tm, 2, elim_common_factor) compset 370in 371 compset 372end 373 374(* add real calculation facilities to global functionality *) 375val _ = let open computeLib in 376 add_funs rwts ; 377 add_convs [(div_tm, 2, elim_common_factor)] 378 end 379 380val addfrags = BasicProvers.logged_addfrags {thyname = "real"} 381val _ = addfrags [REAL_REDUCE_ss] 382 383(* ---------------------------------------------------------------------- 384 REAL_ARITH_ss 385 386 embedding RealArith into a simpset fragment. 387 Derived from code to do the same for the natural numbers, which is in 388 src/num/arith/src/numSimps.sml 389 and 390 src/num/arith/src/Gen_arith.sml 391 ---------------------------------------------------------------------- *) 392 393fun contains_var tm = 394 if is_var tm then true 395 else if is_real_literal tm then false 396 else let 397 val (l, r) = dest_plus tm 398 handle HOL_ERR _ => 399 dest_mult tm 400 handle HOL_ERR _ => dest_minus tm 401 in 402 contains_var l orelse contains_var r 403 end handle HOL_ERR _ => contains_var (dest_absval tm) 404 handle HOL_ERR _ => true 405 (* final default value is true because the term in question must be a 406 complicated non-presburger thing that will get treated as a variable 407 anyway. *) 408 409fun is_linear_mult tm = let 410 val (l,r) = dest_mult tm 411in 412 not (contains_var l andalso contains_var r) 413end 414 415fun arg1 tm = rand (rator tm) 416val arg2 = rand 417 418fun non_presburger_subterms tm = 419 (non_presburger_subterms (#2 (dest_forall tm))) handle _ => 420 (non_presburger_subterms (dest_neg tm)) handle _ => 421 (if (is_conj tm) orelse (is_disj tm) orelse (is_imp tm) orelse 422 (is_eq tm) orelse 423 (is_less tm) orelse (is_leq tm) orelse 424 (is_greater tm) orelse (is_geq tm) orelse 425 (is_plus tm) orelse (is_minus tm) orelse 426 (is_linear_mult tm handle _ => false) 427 then tunion (non_presburger_subterms (arg1 tm)) 428 (non_presburger_subterms (arg2 tm)) 429 else if (is_real_literal tm) then [] 430 else [tm]); 431 432fun is_num_var tm = is_var tm andalso type_of tm = real_ty 433val is_presburger = (all is_num_var) o non_presburger_subterms; 434 435 436 437fun cond_has_arith_components tm = 438 if boolSyntax.is_cond tm then let 439 val {cond,rarm,larm} = Rsyntax.dest_cond tm 440 in 441 List.all is_arith [cond, rarm, larm] 442 end 443 else true 444and is_arith tm = 445 is_presburger tm orelse 446 List.all (fn t => type_of t = real_ty andalso cond_has_arith_components t) 447 (non_presburger_subterms tm) 448 449fun contains_forall sense tm = 450 if is_conj tm orelse is_disj tm then 451 List.exists (contains_forall sense) (#2 (strip_comb tm)) 452 else if is_neg tm then 453 contains_forall (not sense) (rand tm) 454 else if is_imp tm then 455 contains_forall (not sense) (rand (rator tm)) orelse 456 contains_forall sense (rand tm) 457 else if is_forall tm then 458 sense orelse contains_forall sense (#2 (dest_forall tm)) 459 else if is_exists tm then 460 not sense orelse contains_forall sense (#2 (dest_exists tm)) 461 else false 462 463(* This function determines whether or not to add something as context 464 to the arithmetic decision procedure. Because the d.p. can't 465 handle implications with nested foralls on the left hand side, we 466 eliminate those here. More generally, we can't allow the formula 467 to be added to have any positive universals, because these will 468 translate into negative ones in the context of the wider goal, and 469 thus cause the goal to be rejected. *) 470 471fun is_arith_thm thm = 472 not (null (hyp thm)) andalso is_arith (concl thm) andalso 473 (not (contains_forall true (concl thm))); 474 475val is_arith_asm = is_arith_thm o ASSUME 476 477val ARITH = RealArith.REAL_ARITH 478 479open Trace Cache Traverse 480fun CTXT_ARITH thms tm = let 481 val context = map concl thms 482 fun try gl = let 483 val gl' = list_mk_imp(context,gl) 484 val _ = trace (5, LZ_TEXT (fn () => "Trying cached arithmetic d.p. on "^ 485 term_to_string gl')) 486 in 487 rev_itlist (C MP) thms (ARITH gl') 488 end 489 val thm = EQT_INTRO (try tm) 490 handle (e as HOL_ERR _) => 491 if not (Feq tm) then EQF_INTRO (try(mk_neg tm)) else raise e 492in 493 trace(1,PRODUCE(tm,"REAL_ARITH",thm)); thm 494end 495 496fun crossprod (ll : 'a list list) : 'a list list = 497 case ll of 498 [] => [[]] 499 | h::t => let 500 val c = crossprod t 501 in 502 List.concat (map (fn hel => map (cons hel) c) h) 503 end 504fun prim_dest_const t = let 505 val {Thy,Name,...} = dest_thy_const t 506in 507 (Thy,Name) 508end 509 510fun dpvars t = let 511 fun recurse bnds acc t = let 512 val (f, args) = strip_comb t 513 fun go2() = let 514 val (t1, t2) = (hd args, hd (tl args)) 515 in 516 recurse bnds (recurse bnds acc t1) t2 517 end 518 fun go1 () = recurse bnds acc (hd args) 519 in 520 case Lib.total prim_dest_const f of 521 SOME ("bool", "~") => go1() 522 | SOME ("bool", "/\\") => go2() 523 | SOME ("bool", "\\/") => go2() 524 | SOME ("min", "==>") => go2() 525 | SOME ("min", "=") => go2() 526 | SOME ("bool", "COND") => let 527 val (t1,t2,t3) = (hd args, hd (tl args), hd (tl (tl args))) 528 in 529 recurse bnds (recurse bnds (recurse bnds acc t1) t2) t3 530 end 531 | SOME ("realax", "real_add") => go2() 532 | SOME ("real", "real_sub") => go2() 533 | SOME ("real", "real_gt") => go2() 534 | SOME ("realax", "real_lt") => go2() 535 | SOME ("real", "real_lte") => go2() 536 | SOME ("real", "real_ge") => go2() 537 | SOME ("realax", "real_neg") => go1() 538 | SOME ("real", "abs") => go1() 539 | SOME ("realax", "real_mul") => let 540 val args = realSyntax.strip_mult t 541 val arg_vs = map (HOLset.listItems o recurse bnds empty_tmset) args 542 val cs = crossprod (filter (not o null) arg_vs) 543 val var_ts = map (realSyntax.list_mk_mult o Listsort.sort Term.compare) 544 cs 545 in 546 List.foldl (fn (t,acc)=>HOLset.add(acc,t)) acc var_ts 547 end 548 | SOME ("bool", "!") => let 549 val (v, bod) = dest_abs (hd args) 550 in 551 recurse (HOLset.add(bnds, v)) acc bod 552 end 553 | SOME ("bool", "?") => let 554 val (v, bod) = dest_abs (hd args) 555 in 556 recurse (HOLset.add(bnds, v)) acc bod 557 end 558 | SOME _ => if realSyntax.is_real_literal t then acc 559 else HOLset.add(acc, t) 560 | NONE => if is_var t then if HOLset.member(bnds, t) then acc 561 else HOLset.add(acc, t) 562 else HOLset.add(acc, t) 563 end 564in 565 HOLset.listItems (recurse empty_tmset empty_tmset t) 566end 567 568 569val (CACHED_ARITH,arith_cache) = let 570 fun check tm = 571 let val ty = type_of tm 572 in 573 (ty=Type.bool andalso (is_arith tm orelse Feq tm)) 574 end; 575in 576 RCACHE (dpvars, check,CTXT_ARITH) 577 (* the check function determines whether or not a term might be handled 578 by the decision procedure -- we want to handle F, because it's possible 579 that we have accumulated a contradictory context. *) 580end; 581 582val ARITH_REDUCER = let 583 exception CTXT of thm list; 584 fun get_ctxt e = (raise e) handle CTXT c => c 585 fun add_ctxt(ctxt, newthms) = let 586 val addthese = filter is_arith_thm (flatten (map CONJUNCTS newthms)) 587 in 588 CTXT (addthese @ get_ctxt ctxt) 589 end 590in 591 REDUCER {name = SOME"REAL_ARITH_DP", 592 addcontext = add_ctxt, 593 apply = fn args => CACHED_ARITH (get_ctxt (#context args)), 594 initial = CTXT []} 595end; 596 597val REAL_ARITH_ss = 598 SSFRAG 599 {name=SOME"REAL_ARITH", 600 convs = [], rewrs = [], congs = [], 601 filter = NONE, ac = [], dprocs = [ARITH_REDUCER]}; 602 603open AC_Sort realTheory realSyntax 604 605val literalbase = mk_var(" ", real_ty) (* compares less than 'normal' vars *) 606 607fun oksort cmp [] = true 608 | oksort cmp [_] = true 609 | oksort cmp (t1::(rest as (t2::ts))) = 610 cmp(t1,t2) = LESS andalso oksort cmp rest 611 612val x_real = mk_var("x", real_ty) 613val a_num = mk_var("a", numSyntax.num) 614val b_num = mk_var("b", numSyntax.num) 615val NUMERALa = mk_comb(numSyntax.numeral_tm, a_num) 616val NUMERALb = mk_comb(numSyntax.numeral_tm, b_num) 617val MUL_ASSOC' = GSYM REAL_MUL_ASSOC 618val REAL_MUL_RID' = GSYM REAL_MUL_RID 619val REAL_POW_ADD' = GSYM REAL_POW_ADD 620val REAL_POW_INV' = GSYM REAL_POW_INV 621val REAL_POW_INV_NUMERAL' = 622 REAL_POW_INV' |> SPECL [x_real, NUMERALa] |> GENL [x_real, a_num] 623val REAL_POW_POW_NUMERAL = 624 REAL_POW_POW |> SPECL [x_real, NUMERALa, NUMERALb] 625 |> GENL [x_real, a_num, b_num] 626val POW_1' = GSYM POW_1 627val (NEG_FRAC, NEG_DENOM) = CONJ_PAIR neg_rat 628val NEG_INV = REAL_NEG_INV' 629val INV_1OVER = REAL_INV_1OVER 630val NEG_MINUS1' = GSYM REAL_NEG_MINUS1 631val Flor = OR_CLAUSES |> SPEC_ALL |> CONJUNCTS |> el 3 632 633val realreduce_cs = real_compset() 634fun REPORT_ALL_CONV t = 635 (print ("\nGiving up on " ^ term_to_string t ^ "\n"); ALL_CONV t) 636val REAL_REDUCE = 637 PURE_REWRITE_CONV [REAL_INV_1OVER] THENC computeLib.CBV_CONV realreduce_cs 638val NUM_REDUCE = reduceLib.REDUCE_CONV 639 640fun is_literalish t = 641 is_real_literal t orelse 642 case total dest_inv t of 643 NONE => (case total dest_div t of 644 NONE => (case total dest_negated t of 645 NONE => false 646 | SOME t0 => is_literalish t0) 647 | SOME (n,d) => is_literalish n andalso is_literalish d) 648 | SOME t0 => is_literalish t0 649 650val NORMLIT_phase1 = 651 PURE_REWRITE_CONV [NEG_FRAC, NEG_DENOM, NEG_INV, REAL_NEGNEG, INV_1OVER] 652val GCDELIM = REAL_REDUCE 653 654fun is_real_fraction t = 655 is_real_literal t orelse 656 case Exn.capture dest_div t of 657 Exn.Res(n,d) => 658 is_real_literal n andalso is_real_literal d andalso 659 not (is_negated d) 660 | _ => false 661fun REAL_LITCANON t = if is_literalish t then 662 if is_real_fraction t then raise UNCHANGED 663 else 664 (NORMLIT_phase1 THENC REAL_REDUCE) t 665 else NO_CONV t 666 667val NZ_t = prim_mk_const{Thy = "real", Name = "nonzerop"} 668fun is_NZ t = is_comb t andalso rator t ~~ NZ_t 669fun mul_termbase t = 670 if is_real_fraction t then (t, Arbint.one) 671 else if is_NZ t then (t, Arbint.one) 672 else 673 case total dest_pow t of 674 NONE => (case total dest_inv t of 675 NONE => (t, Arbint.one) 676 | SOME t' => (t', Arbint.~ Arbint.one)) 677 | SOME (b0,e) => 678 (case total dest_inv b0 of 679 NONE => if numSyntax.is_numeral e then 680 (b0, Arbint.fromNat (numSyntax.dest_numeral e)) 681 else (t, Arbint.one) 682 | SOME b => 683 if numSyntax.is_numeral e then 684 (b, Arbint.~ (Arbint.fromNat (numSyntax.dest_numeral e))) 685 else (mk_pow(b,e), Arbint.~ Arbint.one)) 686 687fun litcompare(t1,t2) = 688 if is_real_fraction t1 then 689 if is_real_fraction t2 then EQUAL 690 else LESS 691 else if is_real_fraction t2 then GREATER 692 else Term.compare(t1,t2) 693local 694 fun termbase t = #1 (mul_termbase t) 695 (* puts the inverted term on the right *) 696 fun powinv_fix t = 697 let val (l,r) = dest_mult t 698 val (lb,_) = dest_pow l 699 in 700 if is_inv lb then REWR_CONV REAL_MUL_COMM 701 else ALL_CONV 702 end t 703 val normNZs = REWR_CONV nonzerop_mulXX 704 705 val mulcompare = inv_img_cmp termbase litcompare 706 707 val addPOW1 = REWR_CONV POW_1' 708 val mulPOWs = TRY_CONV (REWR_CONV REAL_POW_POW THENC 709 RAND_CONV (REWR_CONV arithmeticTheory.MULT_RIGHT_1)) 710 val POW_E0 = CONJUNCT1 pow 711 val (inv_th1, inv_th2) = CONJ_PAIR realTheory.REAL_INV_nonzerop 712 fun compare_exponents t = 713 let val (l,r) = dest_mult t 714 val (e1,e2) = ((snd o dest_pow) ## (snd o dest_pow)) (l,r) 715 val (m,n) = (numSyntax.dest_numeral ## numSyntax.dest_numeral) (e1,e2) 716 val finish = RAND_CONV NUM_REDUCE 717 val cth = 718 if Arbnum.<(m,n) then 719 MATCH_MP pow_inv_mul_powlt 720 (numSyntax.mk_less(e1,e2) |> NUM_REDUCE |> EQT_ELIM) 721 else 722 MATCH_MP pow_inv_mul_invlt 723 (numSyntax.mk_less(e2,e1) |> NUM_REDUCE |> EQT_ELIM) 724 in 725 REWR_CONV cth THENC finish 726 end t 727 val combine_exponents = 728 (REWR_CONV (GSYM REAL_POW_ADD) THENC 729 RAND_CONV (CHANGED_CONV (computeLib.CBV_CONV realreduce_cs))) ORELSEC 730 (powinv_fix THENC ( 731 REWR_CONV pow_inv_eq ORELSEC 732 compare_exponents ORELSEC 733 REWR_CONV (GSYM POW_2) ORELSEC 734 REPORT_ALL_CONV 735 )) 736 737 fun give_pow t = 738 case total dest_pow t of 739 NONE => addPOW1 t 740 | SOME (b,e) => if numSyntax.is_numeral e then ALL_CONV t else addPOW1 t 741 val mulcombine0 = 742 BINOP_CONV give_pow THENC 743 combine_exponents THENC 744 TRY_CONV (FIRST_CONV (map REWR_CONV [POW_1, POW_E0])) 745 fun mulcombine t = 746 if is_real_fraction (rand t) then REAL_REDUCE t 747 else (normNZs ORELSEC mulcombine0) t 748 749 fun neg_nonnum_conv t = 750 case total dest_negated t of 751 NONE => ALL_CONV t 752 | SOME t0 => if is_real_literal t0 then ALL_CONV t 753 else REWR_CONV REAL_NEG_MINUS1 t 754 fun diag s c t = (print (s t ^ "\n"); c t) 755 756 fun pow_inv_nonnumeral_out t = 757 case total dest_pow t of 758 SOME (b,e) => if numSyntax.is_numeral e then ALL_CONV t 759 else TRY_CONV (LAND_CONV pow_inv_nonnumeral_out THENC 760 REWR_CONV REAL_POW_INV) t 761 | NONE => ALL_CONV t 762 val mulpre = 763 REAL_LITCANON ORELSEC 764 (REWRITE_CONV [REAL_POW_INV_NUMERAL', REAL_INV_INV, 765 REAL_POW_POW_NUMERAL] THENC 766 pow_inv_nonnumeral_out THENC 767 neg_nonnum_conv) 768 769 val mulsort = { 770 assoc = REAL_MUL_ASSOC, 771 comm = REAL_MUL_COMM, 772 dest = realSyntax.dest_mult, 773 mk = realSyntax.mk_mult, 774 cmp = mulcompare, 775 combine = (* diag (fn t => "mulcombine on "^term_to_string t) *) mulcombine, 776 preprocess = (* diag (fn t => "mulpre on "^term_to_string t) *) mulpre 777 } 778 fun leading_coeff_norm t = 779 case total dest_mult t of 780 SOME (l,r) => if is_real_fraction l then 781 (RAND_CONV (PURE_REWRITE_CONV [REAL_MUL_ASSOC]) THENC 782 TRY_CONV (REWR_CONV NEG_MINUS1')) t 783 else PURE_REWRITE_CONV [REAL_MUL_ASSOC] t 784 | _ => ALL_CONV t 785in 786 fun REALMULCANON t = 787 let 788 fun strip A t = 789 case total dest_mult t of 790 SOME(t1,t2) => strip (t2::A) t1 791 | NONE => t::A 792 val (l,r) = dest_mult t handle HOL_ERR _ => raise UNCHANGED 793 val ts = strip [] (if is_real_fraction l then r else t) 794 in 795 if List.exists (fn t => is_mult t orelse is_literalish t) ts orelse 796 not (oksort mulcompare ts) 797 then 798 AC_Sort.sort mulsort THENC 799 TRY_CONV (REWR_CONV REAL_MUL_LID) THENC 800 AC_Sort.sort mulsort THENC 801 REWRITE_CONV[POW_1, nonzerop_NUMERAL, POW_ONE, REAL_MUL_LID, 802 REAL_MUL_RID, nonzerop_pow] THENC 803 leading_coeff_norm 804 else ALL_CONV 805 end t 806end (* local *) 807 808val RMULCANON_ss = SSFRAG { 809 ac = [], congs = [], dprocs = [], filter = NONE, 810 name = SOME "RMULCANON_ss", 811 rewrs = [], 812 convs = [ 813 {conv = K (K REALMULCANON), trace = 2, 814 key = SOME ([], mk_mult(mk_var("x",real_ty), mk_var("y",real_ty))), 815 name = "REALMULCANON"} 816 ] 817} 818 819val _ = addfrags [RMULCANON_ss] 820 821local 822 val x = mk_var("x", real_ty) 823 fun termbase t = 824 if is_real_literal t then mk_abs(x,x) (* sorts last *) 825 else 826 case total dest_mult t of 827 SOME(l,r) => if is_real_literal l then r else t 828 | NONE => dest_negated t handle HOL_ERR _ => t 829 830 val addcompare = inv_img_cmp termbase Term.compare 831 832 val ADD_MUL1 = GSYM REAL_MUL_LID 833 val ADD_RDISTRIB' = GSYM REAL_ADD_RDISTRIB 834 fun give_coeff t = 835 case total dest_mult t of 836 SOME (l,r) => if is_real_literal l then ALL_CONV t 837 else REWR_CONV ADD_MUL1 t 838 | NONE => (REWR_CONV REAL_NEG_MINUS1 ORELSEC REWR_CONV ADD_MUL1) t 839 840 val NEG_MINUS1' = GSYM REAL_NEG_MINUS1 841 val addcombine0 = 842 BINOP_CONV give_coeff THENC REWR_CONV ADD_RDISTRIB' THENC 843 LAND_CONV (computeLib.CBV_CONV realreduce_cs) THENC 844 TRY_CONV (FIRST_CONV (map REWR_CONV [REAL_MUL_LID, REAL_MUL_LZERO])) 845 fun addcombine t = 846 if is_real_literal (rand t) then 847 computeLib.CBV_CONV realreduce_cs t 848 else addcombine0 t 849 850 val addsort = { 851 assoc = REAL_ADD_ASSOC, 852 comm = REAL_ADD_COMM, 853 dest = realSyntax.dest_plus, 854 mk = realSyntax.mk_plus, 855 cmp = addcompare, 856 combine = addcombine, 857 preprocess = REALMULCANON 858 } 859in 860 fun REALADDCANON t = 861 let 862 fun strip A t = 863 case total dest_plus t of 864 SOME(t1,t2) => strip (t2::A) t1 865 | NONE => t::A 866 val ts = strip [] t 867 in 868 if List.exists is_plus ts orelse not (oksort addcompare ts) 869 then 870 AC_Sort.sort addsort THENC 871 PURE_REWRITE_CONV [REAL_ADD_ASSOC, REAL_ADD_LID, REAL_ADD_RID] 872 else ALL_CONV 873 end t 874end (* local *) 875 876val RADDCANON_ss = SSFRAG { 877 ac = [], congs = [], dprocs = [], filter = NONE, 878 name = SOME "RADDCANON_ss", 879 rewrs = [], 880 convs = [ 881 {conv = K (K REALADDCANON), trace = 2, 882 key = SOME ([], mk_plus(mk_var("x",real_ty), mk_var("y",real_ty))), 883 name = "REALADDCANON"} 884 ] 885} 886 887(* val _ = augment_srw_ss [RMULCANON_ss] *) 888fun ifMULT c1 c2 t = if is_mult t then c1 t else c2 t 889fun mul_extract P t = 890 case total dest_mult t of 891 NONE => if P t then ALL_CONV t else NO_CONV t 892 | SOME (l,r) => 893 let 894 in 895 if P l then ALL_CONV 896 else 897 (LAND_CONV (mul_extract P) THENC TRY_CONV (REWR_CONV MUL_ASSOC')) 898 ORELSEC 899 (RAND_CONV (mul_extract P) THENC REWR_CONV REAL_MUL_COMM THENC 900 TRY_CONV (REWR_CONV MUL_ASSOC')) 901 end t 902 903fun mkexp (b0,e) = 904 let 905 val (b,i) = if Arbint.<(e,Arbint.zero) then (mk_inv b0, Arbint.abs e) 906 else (b0,e) 907 in 908 mk_pow(b, numSyntax.mk_numeral (Arbint.toNat i)) 909 end 910 911val sign_rwts = [REAL_POW_POS, REAL_POW_NEG, 912 REAL_POW_GE0, REAL_POW_LE0, 913 ZERO_LT_POW, 914 REAL_LT_INV_EQ, REAL_INV_LT0] 915(* 916fun base_solver asms stk t = 917 let 918 val _ = print ("Solving "^term_to_string t) 919 in 920 case Exn.capture (EQT_ELIM o QCONV (SIMP_CONV (srw_ss() ++ numSimps.ARITH_ss) asms)) t of 921 Exn.Res th => (print " - OK\n"; th) 922 | Exn.Exn e => (print " - FAILED\n"; raise e) 923 end 924 925val R = ���$<= : real -> real -> bool��� 926val Rthms = [(REAL_LE_LMUL, rhs), (REAL_LE_LMUL_NEG, rhs)] 927val R = ���$= : real -> real -> bool��� 928val Rthms = [(REAL_EQ_LMUL, (rand o rhs))] 929val R = ���$< : real -> real -> bool��� 930val Rthms = [(REAL_LT_LMUL, rhs), (REAL_LT_LMUL_NEG, rhs)] 931 932fun solver0 stk t = base_solver [ASSUME ``z <> 0r``] stk t 933val stk = [] 934*) 935fun giveexp t = 936 if is_pow t then ALL_CONV t 937 else REWR_CONV POW_1' t 938fun mulrelnorm0 R Rthms solver0 stk t = 939 let 940 val mkERR = mk_HOL_ERR "realSimps" "mulrelnorm" 941 val (l,r) = dest_binop R (mkERR ("Not a " ^ term_to_string R)) t 942 val sorted_cbases = Listsort.sort (inv_img_cmp #1 litcompare) o 943 map mul_termbase o strip_mult 944 val ls = sorted_cbases l 945 val rs = sorted_cbases r 946 fun solver stk t = 947 let val eqn = QCONV (PURE_REWRITE_CONV sign_rwts) t 948 in 949 EQ_MP (SYM eqn) (solver0 stk (rhs (concl eqn))) 950 end 951 fun apply_thm (th0,_) t = 952 let 953 val th = PART_MATCH (lhs o #2 o strip_imp) th0 t 954 in 955 case total dest_imp (concl th) of 956 NONE => th 957 | SOME (h,c) => MATCH_MP th (solver (t::stk) h) 958 end 959 val apply_thms = FIRST_CONV (map apply_thm Rthms) 960 fun mkmove_th x (th0, f) t = 961 let 962 val th = PART_MATCH (f o #2 o strip_imp) (SPEC x th0) t 963 in 964 case total dest_imp (concl th) of 965 NONE => SYM th 966 | SOME (h,c) => MP th (solver(t::stk) h) |> SYM 967 end 968 fun mkmove_thms xyz = FIRST_CONV (map (mkmove_th xyz) Rthms) 969 970 971 fun positivep i = Arbint.<=(Arbint.zero, i) 972 fun process (l_t,el) (r_t,er) t = 973 if is_real_literal l_t andalso is_real_literal r_t andalso 974 positivep el andalso positivep er 975 then 976 let val li = int_of_term l_t and ri = int_of_term r_t 977 val toN = Arbint.toNat o Arbint.abs 978 val ln = toN li and rn = toN ri 979 val dn = Arbnum.gcd (ln,rn) 980 val _ = dn <> Arbnum.one orelse 981 raise mkERR "Literals are coprime" 982 val di = Arbint.fromNat dn 983 val dt = term_of_int di 984 val lc = Arbint.div(li,di) and rc = Arbint.div(ri,di) 985 val lct = term_of_int lc and rct = term_of_int rc 986 fun mkeq c = mk_mult(dt, c) |> REAL_REDUCE |> SYM 987 val leqn = mkeq lct and reqn = mkeq rct 988 fun extract_n_factor lit eqn = 989 mul_extract (aconv lit) THENC 990 ifMULT (LAND_CONV (K eqn) THENC REWR_CONV MUL_ASSOC') 991 (K eqn) 992 in 993 FORK_CONV(extract_n_factor l_t leqn, extract_n_factor r_t reqn) 994 THENC 995 apply_thms 996 end t 997 else if is_real_fraction l_t orelse is_real_fraction r_t then 998 let 999 fun denom (t,e) = 1000 case total dest_div t of 1001 NONE => if positivep e then Arbint.one 1002 else int_of_term t 1003 | SOME (_, d) => int_of_term d 1004 val ld = denom (l_t, el) 1005 val rd = denom (r_t, er) 1006 val mt = Arbint.*(ld,rd) |> term_of_int 1007 val sidecond1 = mk_less(zero_tm, mt) |> REAL_REDUCE 1008 val sidecond2 = mk_eq(mt,zero_tm) |> REAL_REDUCE 1009 val th = hd Rthms |> #1 |> SPEC mt 1010 |> REWRITE_RULE [sidecond1,sidecond2] 1011 |> GSYM 1012 in 1013 REWR_CONV th 1014 end t 1015 else if el = er then 1016 let fun chk t = pair_eq aconv equal (mul_termbase t) (l_t, el) 1017 val prc = PURE_REWRITE_CONV [REAL_POW_INV'] THENC giveexp 1018 in 1019 BINOP_CONV (mul_extract chk THENC 1020 ifMULT (LAND_CONV prc) 1021 (prc THENC REWR_CONV REAL_MUL_RID')) THENC 1022 apply_thms 1023 end t 1024 else 1025 let val (c,ld,rd) = if Arbint.<(el,er) then 1026 (el,Arbint.zero,Arbint.-(er,el)) 1027 else (er,Arbint.-(el,er), Arbint.zero) 1028 fun chk p t = pair_eq aconv equal p (mul_termbase t) 1029 fun common split i t = 1030 if i = Arbint.zero then 1031 if split then REWR_CONV REAL_MUL_RID' t else ALL_CONV t 1032 else 1033 let 1034 val mul_t = mk_mult(mkexp(l_t,c), mkexp(l_t,i)) 1035 val th = if Arbint.<(c,Arbint.zero) then 1036 if Arbint.<(Arbint.+(c,i), Arbint.zero) then 1037 pow_inv_mul_powlt 1038 else pow_inv_mul_invlt 1039 else REAL_POW_ADD' 1040 fun stage2 t = 1041 let val th0 = PART_MATCH (lhs o #2 o strip_imp) th t 1042 in 1043 case total dest_imp (concl th0) of 1044 NONE => th0 1045 | SOME (l,r) => 1046 MATCH_MP th0 (EQT_ELIM (REAL_REDUCE l)) 1047 end 1048 in 1049 (REWR_CONV REAL_MUL_COMM THENC stage2 THENC 1050 RAND_CONV NUM_REDUCE ) mul_t |> SYM 1051 end 1052 in 1053 FORK_CONV (mul_extract (chk (l_t,el)) THENC 1054 ifMULT (LAND_CONV (giveexp THENC common false ld)) 1055 (giveexp THENC common true ld) THENC 1056 TRY_CONV (REWR_CONV MUL_ASSOC'), 1057 mul_extract (chk (r_t,er)) THENC 1058 ifMULT (LAND_CONV (giveexp THENC common false rd)) 1059 (giveexp THENC common true rd) THENC 1060 TRY_CONV (REWR_CONV MUL_ASSOC')) THENC 1061 apply_thms 1062 end t 1063 fun eqcleanup t = 1064 if is_disj t then 1065 let val subth = solver (t::stk) (mk_neg (lhand t)) 1066 in 1067 LAND_CONV (REWR_CONV (EQF_INTRO subth)) THENC 1068 REWR_CONV Flor 1069 end t 1070 else ALL_CONV t 1071 1072 (* direction = true <=> move from left to right *) 1073 fun maybemove (b,e) t = 1074 if not (is_literalish b) andalso positivep e then NO_CONV t 1075 else 1076 let val f = 1077 if is_literalish b then #2 (dest_div b) 1078 else mk_pow(b, 1079 numSyntax.mk_numeral(Arbint.toNat(Arbint.~ e))) 1080 val (rel, args) = strip_comb t 1081 val l = hd args and r = hd (tl args) 1082 val th = mkmove_thms f t |> CONV_RULE (LAND_CONV eqcleanup) 1083 in 1084 CONV_RULE (RAND_CONV (BINOP_CONV REALMULCANON)) th 1085 end 1086 fun findelim lefts rights t = 1087 case (lefts, rights) of 1088 ([], []) => raise mkERR "No common eliminable terms" 1089 | (l1::ls, []) => (maybemove l1 ORELSEC findelim ls []) t 1090 | ([], r1::rs) => (maybemove r1 ORELSEC findelim [] rs) t 1091 | ((l1 as (bl,_))::ls, (r1 as (br,_))::rs) => 1092 case litcompare(bl,br) of 1093 LESS => (maybemove l1 ORELSEC findelim ls rights) t 1094 | GREATER => (maybemove r1 ORELSEC findelim lefts rs) t 1095 | EQUAL => (process l1 r1 ORELSEC findelim ls rs) t 1096 in 1097 findelim ls rs t 1098 end 1099 1100fun mulrelnorm R Rthms solver stk = 1101 BINOP_CONV REALMULCANON THENC mulrelnorm0 R Rthms solver stk THENC 1102 TRY_CONV (BINOP_CONV REALMULCANON) 1103(* 1104 1105val lenorm = mulrelnorm ���$<= : real -> real -> bool��� 1106 [REAL_LE_LMUL, REAL_LE_LMUL_NEG] solver [] 1107 1108val eqnorm = mulrelnorm ���$=��� [REAL_EQ_LMUL] solver [] 1109val ex1 = eqnorm ���2r * z pow 2 * inv yy = 5 * z pow 2 * inv y * a��� 1110val ex1a = eqnorm ���z * 4 = inv x * 6��� 1111val ex1b = eqnorm ���z pow 4 = inv z pow 3��� 1112 1113val ex2 = lenorm ���2r * inv y pow 2 <= 9 * inv y * z��� 1114val ex3 = lenorm ���2r * inv y <= z * 2���; 1115val ex4 = lenorm ���x pow 3 * 10 <= x pow 5 * y��� 1116val ex5 = lenorm ���z pow 3 * 10 <= z pow 5 * y��� 1117*) 1118fun V s = mk_var(s, real_ty) 1119val x = V "x" and y = V "y" and z = V "z" 1120val RMULRELNORM_ss = SSFRAG { 1121 ac = [], congs = [], dprocs = [], filter = NONE, name = SOME "RMULRELNORM_ss", 1122 rewrs = [], 1123 convs = [ 1124 {key = SOME ([], mk_leq(x,y)), 1125 conv = mulrelnorm leq_tm [(REAL_LE_LMUL, rhs), (REAL_LE_LMUL_NEG, rhs)] , 1126 name = "RMUL_LEQNORM", trace = 2 1127 }, 1128 {key = SOME ([], mk_eq(x,mk_mult(y,z))), 1129 conv = mulrelnorm equality [(REAL_EQ_LMUL, rand o rhs)], 1130 name = "RMUL_EQNORM1", trace = 2 1131 }, 1132 {key = SOME ([], mk_eq(mk_mult(x,y),z)), 1133 conv = mulrelnorm equality [(REAL_EQ_LMUL, rand o rhs)], 1134 name = "RMUL_EQNORM2", trace = 2 1135 }, 1136 {key = SOME ([], mk_less(x,y)), 1137 conv = mulrelnorm less_tm [(REAL_LT_LMUL, rhs), (REAL_LT_LMUL_NEG, rhs)], 1138 name = "RMUL_LTNORM", trace = 2 1139 } 1140 ] 1141} 1142 1143val _ = addfrags [RMULRELNORM_ss] 1144 1145end 1146