1(* ---------------------------------------------------------------------* 2 * A symbolic calculator for the HOL "num" arithmetic. * 3 * * 4 * When using this with natural arithmetic, note that the fact that * 5 * m-n=0 for n>m is not taken into account. It assumes that * 6 * subtraction is always being used in a "well behaved" way. * 7 * ---------------------------------------------------------------------*) 8 9structure numSimps :> numSimps = 10struct 11 12open Arbint HolKernel Parse boolLib liteLib 13 Arith reduceLib Arith_cons 14 simpLib Traverse Cache Trace; 15 16open NumRelNorms 17 18structure Parse = (* Fix the grammar used by this file *) 19struct 20 open Parse 21 val (Type,Term) = parse_from_grammars arithmeticTheory.arithmetic_grammars 22end 23open Parse 24 25val num_ty = numSyntax.num 26val zero_tm = numSyntax.zero_tm 27val dest_suc = numSyntax.dest_suc; 28val mk_numeral = term_of_int; 29val dest_numeral = int_of_term; 30 31val ARITH = EQT_ELIM o ARITH_CONV; 32 33(*---------------------------------------------------------------------------*) 34(* REDUCE_ss: simpset fragment that reduces ground arithmetic expressions *) 35(*---------------------------------------------------------------------------*) 36 37local 38 fun reducer t = 39 let open numSyntax 40 val (_, args) = strip_comb t 41 fun reducible t = 42 is_numeral t orelse (is_suc t andalso reducible (snd (dest_comb t))) 43 in 44 if List.all reducible args then 45 CHANGED_CONV reduceLib.REDUCE_CONV t 46 else 47 NO_CONV t 48 end 49 fun mk_redconv0 pat = 50 {name = "REDUCE_CONV (arithmetic reduction)", 51 trace = 2, 52 key = SOME([], pat), conv = K (K reducer)} 53 val x = mk_var("x", num_ty) 54 val y = mk_var("y", num_ty) 55 fun mk_unary_rconv op_t = mk_redconv0 (mk_comb(op_t, x)) 56 fun mk_redconv op_t = mk_redconv0 (list_mk_comb(op_t, [x, y])) 57in 58val REDUCE_ss = 59 let open numSyntax 60 in simpLib.SSFRAG 61 {name = SOME"REDUCE", 62 convs = mk_unary_rconv even_tm :: 63 mk_unary_rconv odd_tm :: 64 mk_unary_rconv pre_tm :: 65 mk_unary_rconv suc_tm :: 66 mk_unary_rconv div2_tm :: 67 map mk_redconv [mult_tm, plus_tm, minus_tm, 68 div_tm, mod_tm, exp_tm, 69 less_tm, leq_tm, greater_tm, geq_tm, 70 min_tm, max_tm, Term`$= : num -> num -> bool`], 71 rewrs = [], congs = [], filter = NONE, ac = [], dprocs = []} 72 end 73end; 74 75 76(*---------------------------------------------------------------------------*) 77(* Set of rewrites used in arith_ss. *) 78(*---------------------------------------------------------------------------*) 79 80local open arithmeticTheory 81 val sym_lhs = CONV_RULE ((BINDER_CONV o BINDER_CONV 82 o RATOR_CONV o RAND_CONV) SYM_CONV) 83 val one_suc = Rewrite.PURE_REWRITE_RULE [ONE] 84 val add_sym = Rewrite.ONCE_REWRITE_RULE [ADD_SYM] 85in 86val arithmetic_rewrites = [ 87 (* suc *) 88 ARITH(Term `!x. ((SUC x = 1) = (x=0)) /\ ((1 = SUC x) = (x = 0))`), 89 ARITH(Term`!x. ((SUC x = 2) = (x=1)) /\ ((2 = SUC x) = (x=1))`), 90 (* addition *) 91 ADD_0, add_sym ADD_0, ADD_EQ_0, sym_lhs ADD_EQ_0, 92 ADD_INV_0_EQ, add_sym ADD_INV_0_EQ, 93 (* multiplication *) 94 MULT_EQ_0, sym_lhs MULT_EQ_0, 95 MULT_EQ_1, sym_lhs MULT_EQ_1, 96 MULT_0, ONCE_REWRITE_RULE [MULT_COMM] MULT_0, 97 one_suc MULT_EQ_1, one_suc (sym_lhs MULT_EQ_1), 98 MULT_RIGHT_1, MULT_LEFT_1, 99 (* subtraction *) 100 SUB_EQUAL_0, SUC_SUB1, SUB_0, ADD_SUB, add_sym ADD_SUB, SUB_EQ_0, 101 sym_lhs SUB_EQ_0, SUB_LESS_EQ, SUB_MONO_EQ, SUB_RIGHT_GREATER, 102 SUB_RIGHT_LESS, SUB_RIGHT_GREATER_EQ, SUB_RIGHT_LESS_EQ, prim_recTheory.PRE, 103 (* exponentiation *) 104 EXP_EQ_0, EXP_1, EXP_EQ_1, ZERO_LT_EXP, EXP_EXP_INJECTIVE, 105 EXP_BASE_INJECTIVE, 106 EXP_BASE_LT_MONO, EXP_BASE_LE_MONO, EXP_EXP_LT_MONO, EXP_EXP_LE_MONO, 107 108 (* order relations and arith. ops *) 109 LESS_EQ_0, prim_recTheory.LESS_0, LESS_EQ_ADD, 110 ARITH ``0 <= x``, ARITH ``SUC x > 0``, ARITH ``x >= 0``, 111 ARITH ``x < SUC x``, ARITH ``x <= SUC x``, 112 ARITH ``x < x + c = 0 < c``, ARITH ``x < c + x = 0 < c``, 113 ARITH ``x <= x + c = 0 <= c``, ARITH ``x <= c + x = 0 <= c``, 114 LESS_EQ_REFL, ARITH ``x >= x``, 115 LESS_MONO_ADD_EQ, add_sym LESS_MONO_ADD_EQ, 116 ADD_MONO_LESS_EQ, add_sym ADD_MONO_LESS_EQ, 117 EQ_MONO_ADD_EQ, add_sym EQ_MONO_ADD_EQ, 118 ARITH ``x + y < w + x = y < w``, ARITH ``y + x < x + w = y < w``, 119 prim_recTheory.INV_SUC_EQ, LESS_MONO_EQ, LESS_EQ_MONO, 120 LESS_MULT_MONO, MULT_SUC_EQ, MULT_MONO_EQ, 121 NOT_SUC_LESS_EQ, 122 MULT_EXP_MONO, LE_MULT_LCANCEL, LE_MULT_RCANCEL, 123 LT_MULT_LCANCEL, LT_MULT_RCANCEL, 124 LT_MULT_CANCEL_LBARE, LT_MULT_CANCEL_RBARE, 125 LE_MULT_CANCEL_LBARE, LE_MULT_CANCEL_RBARE, 126 127 (* falsities *) 128 NOT_EXP_0, NOT_ODD_EQ_EVEN, NOT_SUC_ADD_LESS_EQ, 129 130 NOT_SUC_LESS_EQ_0, prim_recTheory.NOT_LESS_0, prim_recTheory.LESS_REFL, 131 ARITH ``~(x > x)``, 132 133 (* mins and maxs *) 134 MIN_0, MAX_0, MIN_IDEM, MAX_IDEM, MIN_LE, MAX_LE, MIN_LT, MAX_LT, 135 MIN_MAX_EQ, MIN_MAX_LT, 136 137 (* mods and divs *) 138 X_MOD_Y_EQ_X, DIVMOD_ID, DIV_1, MOD_1, LESS_MOD, ZERO_MOD, MOD_MOD, 139 NUMERAL_MULT_EQ_DIV, MOD_LESS, DIV_LESS 140 ] 141end; 142 143val ARITH_RWTS_ss = 144 simpLib.SSFRAG 145 {name=SOME"ARITH_RWTS", 146 convs = [], rewrs = arithmetic_rewrites, congs = [], 147 filter = NONE, ac = [], dprocs = []}; 148 149(*---------------------------------------------------------------------------*) 150(* Add the ground reducer and the arithmetic rewrites to srw_ss. If you want *) 151(* to use the dec. proc. with srw_ss, you have to add ARITH_DP_ss to the *) 152(* first argument list of SRW_TAC *) 153(*---------------------------------------------------------------------------*) 154 155val _ = BasicProvers.augment_srw_ss [REDUCE_ss, ARITH_RWTS_ss] 156 157 158(* ---------------------------------------------------------------------* 159 * LIN: Linear arithmetic expressions * 160 * ---------------------------------------------------------------------*) 161 162datatype lin = LIN of (term * int) list * int; 163 164val mk_lin = 165 let val tmord = pair_compare (Term.compare, Arbint.compare) 166 val tmlt = lt_of_ord tmord; 167 fun shrink_likes ((tm1,k1)::(tm2,k2)::rest) = 168 if aconv tm1 tm2 then 169 if (k1+k2 = zero) then shrink_likes rest 170 else shrink_likes ((tm1,k1+k2)::rest) 171 else (tm1,k1)::shrink_likes((tm2,k2)::rest) 172 | shrink_likes x = x 173 val canon_tms = shrink_likes o sort (curry tmlt) 174 fun mk_tm (tm, k) = if k = zero then failwith "mk_tm: zero term" 175 else (tm, k) 176 in fn (k,x) => LIN (canon_tms (mapfilter mk_tm k),x) 177 end; 178 179fun dest_lin (LIN p) = p; 180 181(* --------------------------------------------------------------------- 182 * LIN <--> HOL 183 * --------------------------------------------------------------------*) 184 185fun is_pos_tm (tm,n) = n > zero 186fun is_neg_tm (tm,n) = n < zero 187 188fun term_of_tm (tm,n) = 189 if (abs n = one) then tm 190 else mk_mult (mk_numeral (abs n),tm); 191 192val list_mk_plus = end_foldr mk_plus (* right associates additions; ugh! *) 193 194fun term_of_lin (LIN (tms,k)) = 195 let val pos_terms = map term_of_tm (filter is_pos_tm tms) 196 val neg_terms = 197 (map term_of_tm (filter is_neg_tm tms))@ 198 (if k < zero then [mk_numeral (~k)] else []) 199 val const_term = if k > zero then SOME (mk_numeral k) else NONE 200 in 201 case const_term of 202 SOME x => 203 if (null pos_terms) then 204 if (null neg_terms) then x 205 else mk_minus(x,list_mk_plus neg_terms) 206 else if (null neg_terms) then list_mk_plus(pos_terms@[x]) 207 else mk_minus(list_mk_plus (pos_terms@[x]), 208 list_mk_plus neg_terms) 209 | NONE => 210 if (null pos_terms) then 211 if (null neg_terms) then zero_tm 212 else failwith "no positive terms" 213 else if (null neg_terms) then list_mk_plus pos_terms 214 else mk_minus(list_mk_plus pos_terms,list_mk_plus neg_terms) 215 end; 216 217fun negate (x,y:int) = (x,~y); 218 219fun lin_of_term tm = 220 let val (t1,t2) = dest_plus tm 221 val (l1,k1) = dest_lin(lin_of_term t1) 222 val (l2,k2) = dest_lin(lin_of_term t2) 223 in mk_lin(l1@l2,k1+k2) 224 end 225 handle HOL_ERR _ => 226 let val (t1,t2) = dest_minus tm 227 val (l1,k1) = dest_lin(lin_of_term t1) 228 val (l2,k2) = dest_lin(lin_of_term t2) 229 in mk_lin(l1@map negate l2,k1 - k2) 230 end 231(* 232 handle HOL_ERR _ => 233 let val (l1,k1) = dest_lin(lin_of_term (dest_suc tm)) 234 in LIN(l1,k1+1) 235 end 236*) 237 handle HOL_ERR _ => 238 mk_lin([], dest_numeral tm) 239 handle HOL_ERR _ => 240 let val (t1, t2) = dest_mult tm 241 val n = dest_numeral t1 242 in 243 mk_lin([(t2, n)], zero) 244 end 245 handle HOL_ERR _ => 246 mk_lin([(tm,one)], zero); 247 248val linear_reduction = term_of_lin o lin_of_term; 249 250(* --------------------------------------------------------------------- 251 * is_arith 252 * 253 * Decide whether something looks like something which may be 254 * either decideable by ARITH_CONV or useful for ARITH_CONV. 255 * 256 * EXAMPLES 257 * is_arith (--`~(1 = 2)`--); (* true *) 258 * is_arith (--`~(LENGTH [1] = 0)`--); (* true *) 259 * is_arith (--`~(x:'a = y)`--); (* false *) 260 * is_arith (--`!z:num. ~(x:'a = y)`--); (* false *) 261 * is_arith (--`!z:num. ~(z = y)`--); (* true *) 262 * is_arith (--`!P. !z:num. ~(z = y) /\ P`--); (* false *) 263 * is_arith (--`(!i. i < 1 + n' ==> (f i = f' i)) ==> 1 + n > 0`--); 264 (* false *) 265 * --------------------------------------------------------------------*) 266(* there might still be bugs in this.... DRS 5 Aug 96 *) 267 268fun cond_has_arith_components tm = 269 if boolSyntax.is_cond tm then let 270 val (cond,rarm,larm) = dest_cond tm 271 in 272 List.all is_arith [cond, rarm, larm] 273 end 274 else true 275and 276 is_arith tm = 277 is_presburger tm orelse 278 List.all (fn t => type_of t = num_ty andalso cond_has_arith_components t) 279 (non_presburger_subterms tm) 280 281(* 282 if (is_forall tm) then 283 (type_of (bvar (rand tm)) = num_ty andalso is_presburger(body(rand tm))) 284 else if is_exists tm then 285 (type_of (bvar (rand tm)) = num_ty andalso is_arith (body (rand tm))) 286 else if (is_abs tm) then false 287 else if (is_geq tm) orelse (is_less tm) orelse 288 (is_leq tm) orelse (is_great tm) then true 289 else if (is_conj tm) orelse (is_disj tm) orelse (is_imp tm) 290 orelse (is_eq tm andalso type_of (rhs tm) = Type.bool) then 291 is_arith (lhand tm) andalso is_arith (rand tm) 292 else if (is_neg tm) then is_arith (dest_neg tm) 293 else if (is_eq tm) then (type_of (rhs tm) = num_ty andalso 294 no_bool_vars_in (lhs tm) andalso 295 no_bool_vars_in (rhs tm)) 296 else false; 297*) 298 299fun contains_forall sense tm = 300 if is_conj tm orelse is_disj tm then 301 List.exists (contains_forall sense) (#2 (strip_comb tm)) 302 else if is_neg tm then 303 contains_forall (not sense) (rand tm) 304 else if is_imp tm then 305 contains_forall (not sense) (rand (rator tm)) orelse 306 contains_forall sense (rand tm) 307 else if is_forall tm then 308 sense orelse contains_forall sense (#2 (dest_forall tm)) 309 else if is_exists tm then 310 not sense orelse contains_forall sense (#2 (dest_exists tm)) 311 else false 312 313 314(* This function determines whether or not to add something as context to 315 the arithmetic decision procedure. Because arithLib.ARITH_CONV can't 316 handle implications with nested foralls on the left hand side, we 317 eliminate those here. More generally, we can't allow the formula to be 318 added to have any positive universals, because these will translate 319 into negative ones in the context of the wider goal, and thus cause 320 the goal to be rejected. *) 321 322fun is_arith_thm thm = let 323 val con = concl thm 324in 325 (not (null (hyp thm)) orelse null (free_vars con)) andalso 326 not (contains_forall true con) andalso is_arith con 327end 328 329 330val is_arith_asm = is_arith_thm o ASSUME 331 332type ctxt = thm list; 333 334fun contains_minus t = List.exists numSyntax.is_minus (numSyntax.strip_plus t) 335 336fun CTXT_ARITH thms tm = 337 if 338 (type_of tm = Type.bool) andalso 339 (is_arith tm orelse (tm = F andalso not (null thms))) 340 then let 341 val context = map concl thms 342 fun try gl = let 343 val gl' = list_mk_imp(context,gl) 344 val _ = trace (5, LZ_TEXT (fn () => "Trying cached arithmetic d.p. on "^ 345 term_to_string gl')) 346 in 347 rev_itlist (C MP) thms (ARITH gl') 348 end 349 val thm = if not (is_conj tm) then 350 EQT_INTRO (try tm) 351 handle (e as HOL_ERR _) => 352 if tm <> F andalso not (is_disj tm) then 353 EQF_INTRO (try(mk_neg tm)) 354 else raise e 355 else EQF_INTRO (try (mk_neg tm)) 356 in 357 trace(1,PRODUCE(tm,"ARITH",thm)); thm 358 end 359 else 360 if type_of tm = num_ty then let 361 val _ = trace(5, LZ_TEXT (fn () => "Linear reduction on "^ 362 term_to_string tm)) 363 val reduction = linear_reduction tm 364 in 365 if aconv reduction tm then 366 (trace (5, TEXT ("No reduction possible")); 367 failwith "CTXT_ARITH: no reduction possible") 368 else if contains_minus tm then let 369 val context = map concl thms 370 val gl = list_mk_imp(context,mk_eq(tm,reduction)) 371 val _ = trace(6, LZ_TEXT (fn () => "Calling ARITH on reduction: "^ 372 term_to_string gl)) 373 val thm = rev_itlist (C MP) thms (ARITH gl) 374 in 375 trace(1,PRODUCE(tm,"ARITH",thm)); thm 376 end 377 else ADDR_CANON_CONV tm 378 end 379 else failwith "CTXT_ARITH: not applicable"; 380 381val boring_ts = [numSyntax.bit1_tm, numSyntax.bit2_tm, numSyntax.numeral_tm] 382fun is_boring t = let 383 val (f,x) = dest_comb t 384in 385 List.exists (same_const f) boring_ts 386end handle HOL_ERR _ => is_const t 387 388fun prim_dest_const t = let 389 val {Thy,Name,...} = dest_thy_const t 390in 391 (Thy,Name) 392end 393 394fun dp_vars t = let 395 fun recurse bnds acc t = let 396 val (f, args) = strip_comb t 397 fun go1() = recurse bnds acc (hd args) 398 fun go2() = recurse bnds (recurse bnds acc (hd args)) (hd (tl args)) 399 in 400 case Lib.total prim_dest_const f of 401 SOME ("bool", "~") => go1() 402 | SOME ("bool", "/\\") => go2() 403 | SOME ("bool", "\\/") => go2() 404 | SOME ("min", "==>") => go2() 405 | SOME ("min", "=") => go2() 406 | SOME ("bool", "COND") => let 407 val (t1,t2,t3) = (hd args, hd (tl args), hd (tl (tl args))) 408 in 409 recurse bnds (recurse bnds (recurse bnds acc t1) t2) t3 410 end 411 | SOME ("num", "SUC") => go1() 412 | SOME ("prim_rec", "<") => go2() 413 | SOME ("arithmetic", "+") => go2() 414 | SOME ("arithmetic", "-") => go2() 415 | SOME ("arithmetic", "<=") => go2() 416 | SOME ("arithmetic", ">") => go2() 417 | SOME ("arithmetic", ">=") => go2() 418 | SOME ("arithmetic", "*") => let 419 val (t1, t2) = (hd args, hd (tl args)) 420 in 421 if numSyntax.is_numeral t1 then recurse bnds acc t2 422 else if numSyntax.is_numeral t2 then 423 recurse bnds acc t1 424 else HOLset.add(acc, t) 425 end 426 | SOME ("bool", "!") => let 427 val (v, bod) = dest_abs (hd args) 428 in 429 recurse (HOLset.add(bnds, v)) acc bod 430 end 431 | SOME ("bool", "?") => let 432 val (v, bod) = dest_abs (hd args) 433 in 434 recurse (HOLset.add(bnds, v)) acc bod 435 end 436 | SOME _ => if numSyntax.is_numeral t then acc 437 else HOLset.add(acc, t) 438 | NONE => if is_var t then if HOLset.member(bnds, t) then acc 439 else HOLset.add(acc, t) 440 else HOLset.add(acc, t) 441 end 442in 443 HOLset.listItems (recurse empty_tmset empty_tmset t) 444end 445 446val (CACHED_ARITH,arith_cache) = let 447 fun check tm = let 448 val ty = type_of tm 449 in 450 (ty = num_ty andalso not (is_boring tm)) 451 orelse 452 (ty=Type.bool andalso (is_arith tm orelse tm = F)) 453 end 454in 455 RCACHE (dp_vars, check, CTXT_ARITH) 456 (* the check function determines whether or not a term might be handled 457 by the decision procedure -- we want to handle F, because it's possible 458 that we have accumulated a contradictory context. *) 459end; 460 461fun ARITH_REDUCER fil = let 462 exception CTXT of thm list; 463 fun get_ctxt e = (raise e) handle CTXT c => c 464 fun add_ctxt(ctxt, newthms) = let 465 val addthese = filter (fn thm => 466 (is_arith_thm thm andalso fil thm)) (flatten (map CONJUNCTS newthms)) 467 in 468 CTXT (addthese @ get_ctxt ctxt) 469 end 470in 471 REDUCER {name=SOME"ARITH_REDUCER", 472 addcontext = add_ctxt, 473 apply = fn args => CACHED_ARITH (get_ctxt (#context args)), 474 initial = CTXT []} 475end; 476 477(*---------------------------------------------------------------------------*) 478(* Finally, a simpset including the arithmetic decision procedure *) 479(*---------------------------------------------------------------------------*) 480 481fun ARITH_DP_FILTER_ss fil = 482 SSFRAG {name=SOME"ARITH_DP", 483 convs = [{conv = K (K MUL_CANON_CONV), 484 key = SOME([], ``x * y``), 485 name = "MUL_CANON_CONV", trace = 2}], 486 rewrs = [], congs = [], 487 filter = NONE, ac = [], dprocs = [ARITH_REDUCER fil]}; 488 489val ARITH_DP_ss = ARITH_DP_FILTER_ss (K true); 490 491val old_dp_ss = 492 SSFRAG {name=SOME"OLD_ARITH_DP", 493 convs = [], rewrs = [], congs = [], filter = NONE, ac = [], 494 dprocs = [ARITH_REDUCER (K true)]}; 495 496(*---------------------------------------------------------------------------*) 497(* And one containing the dec. proc. and the set of arithmetic rewrites. But *) 498(* not REDUCE_ss (since that is a component of std_ss already). *) 499(*---------------------------------------------------------------------------*) 500 501val ARITH_ss = merge_ss [ARITH_RWTS_ss, ARITH_DP_ss]; 502val old_ARITH_ss = merge_ss [ARITH_RWTS_ss, old_dp_ss]; 503 504fun clear_arith_caches() = clear_cache arith_cache; 505 506(*---------------------------------------------------------------------------*) 507(* Simpset for ordered AC rewriting on terms with + and *. *) 508(*---------------------------------------------------------------------------*) 509 510val ARITH_AC_ss = 511 let open arithmeticTheory 512 in ac_ss [(ADD_SYM,ADD_ASSOC), (MULT_SYM,MULT_ASSOC)] 513 end 514 515(*---------------------------------------------------------------------------*) 516(* Development of a simpset that eliminates "SUC n" in favour of n *) 517(*---------------------------------------------------------------------------*) 518 519val SUC_PRE = UNDISCH (ARITH ``0 < m ==> (SUC (PRE m) = m)``); 520 521fun mDISCH t th = 522 if is_eq (concl th) then DISCH t th 523 else let 524 val ant = #1 (dest_imp (concl th)) 525 val conjoined = ASSUME (mk_conj(t, ant)) 526 in 527 DISCH_ALL (MP (MP (DISCH_ALL th) (CONJUNCT1 conjoined)) 528 (CONJUNCT2 conjoined)) 529 end 530 531fun check_for_bads s l r = 532 if is_eq l andalso is_eq r andalso is_suc (lhs l) andalso 533 is_suc (rhs l) 534 then raise mk_HOL_ERR "numSimps" s "Won't convert SUC-injectivity" 535 else if is_suc l then 536 raise mk_HOL_ERR "numSimps" s "Won't convert direct SUC terms" 537 else () 538 539fun eliminate_single_SUC th = let 540 open numSyntax 541 (* theorem of form |- P(n) ==> (f (SUC n) = g n) 542 or |- f (SUC n) = g n 543 with only occurrences of n on LHS being wrapped inside SUC terms. 544 Also check that theorem is not (SUC n = SUC m) = (n = m) *) 545 val (ant, w) = strip_imp (concl th) 546 val (l, r) = dest_eq w 547 val () = check_for_bads "eliminate_single_SUC" l r 548 val lsucs = find_terms (fn t => is_suc t andalso is_var (rand t)) l 549 fun is_v_sucless v t = 550 case dest_term t of 551 COMB(f, x) => if x = v then not (f = suc_tm) 552 else is_v_sucless v f orelse is_v_sucless v x 553 | VAR _ => t = v 554 | LAMB(bv, body) => free_in v t andalso is_v_sucless v body 555 | CONST _ => false 556 val v = rand (valOf (List.find (not o C is_v_sucless l o rand) lsucs)) 557 val base_rewrite = INST [mk_var ("m", num) |-> v] SUC_PRE 558 val base_thm = INST [v |-> numSyntax.mk_pre v] th 559in 560 mDISCH (mk_less(zero_tm, v)) (REWRITE_RULE [base_rewrite] base_thm) 561end handle Option.Option => 562 raise mk_HOL_ERR "numSimps" "eliminate_single_SUC" 563 "No applicable SUC term to eliminate" 564 565 566fun eliminate_SUCn th = let 567 (* theorem of form |- P n ==> (f (SUC n) n = g n) 568 or |- f (SUC n) n = g n *) 569 open numSyntax 570 val (ant, w) = strip_imp (concl th) 571 val (l, r) = dest_eq w 572 val () = check_for_bads "eliminate_SUCn" l r 573 val lsucs = find_terms (fn t => is_suc t andalso is_var (rand t)) l 574 val v = rand (valOf (List.find (is_var o rand) lsucs)) 575 val gv = genvar num 576 val asm = mk_eq(mk_suc v, gv) 577in 578 mDISCH asm (REWRITE_RULE [ASSUME asm] th) 579end handle Option.Option => 580 raise mk_HOL_ERR "numSimps" "eliminate_SUCn" 581 "No applicable SUC term to eliminate" 582 583val SUC_FILTER_ss = let 584 fun numfilter (th,bnd) = let 585 val newth = repeat eliminate_SUCn 586 (repeat eliminate_single_SUC th) 587 in 588 if aconv (concl newth) (concl th) then [(th,bnd)] 589 else [(th,bnd), (newth,bnd)] 590 end 591in 592 simpLib.SSFRAG 593 {name=SOME"SUC_FILTER", 594 convs = [], rewrs = [], congs = [], 595 filter = SOME numfilter, ac = [], dprocs = []} 596end; 597 598val MOD_ss = let 599 open arithmeticTheory simpLib 600 val rsd = {refl = MODEQ_REFL, trans = MODEQ_TRANS, 601 weakenings = [MODEQ_INTRO_CONG], 602 subsets = [], 603 rewrs = [MODEQ_NUMERAL, MODEQ_MOD, MODEQ_0]} 604 val RSD_ss = relsimp_ss rsd 605 val congs = SSFRAG {dprocs = [], ac = [], rewrs = [], 606 congs = [MODEQ_PLUS_CONG, MODEQ_MULT_CONG, MODEQ_SUC_CONG, 607 MODEQ_EXP_CONG], 608 filter = NONE, convs = [], name = NONE} 609in 610 merge_ss [RSD_ss, congs] |> name_ss "MOD_ss" 611end 612 613val _ = BasicProvers.augment_srw_ss [MOD_ss] 614 615(* ---------------------------------------------------------------------- 616 ARITH_NORM_ss 617 618 Simpset fragment for (aggressive) normalisation of arithmetic 619 expressions. No embedded decision procedure (as in arith_ss) means 620 that its handling of subtraction will be patchy, but it will also 621 make it fast enough to be included in the stateful rewriter. 622 ---------------------------------------------------------------------- *) 623 624val ARITH_NORM_ss = let 625 open simpLib NumRelNorms Arith Conv 626 fun conv (k, c, n) = {key = SOME ([], k), conv = K (K c), 627 name = n, trace = 3} 628 val DECIDE = EQT_ELIM o ARITH_CONV 629in 630 SSFRAG {ac = [], 631 name = SOME "ARITH_NORM", 632 congs = [], 633 convs = [conv (``x + y``, ADDR_CANON_CONV, "ADDR_CANON_CONV"), 634 conv (``x * y``, MUL_CANON_CONV, "MUL_CANON_CONV"), 635 conv (``x < y``, 636 BINOP_CONV ADDR_CANON_CONV THENC sum_lt_norm, 637 "LT_CANON_CONV"), 638 conv (``x = y:num``, 639 BINOP_CONV ADDR_CANON_CONV THENC sum_eq_norm, 640 "NUMEQ_CANON_CONV"), 641 conv (``x <= y:num``, 642 BINOP_CONV ADDR_CANON_CONV THENC sum_leq_norm, 643 "LEQ_CANON_CONV")], 644 rewrs = [arithmeticTheory.GREATER_DEF, 645 arithmeticTheory.GREATER_EQ, 646 DECIDE ``x < y - z <=> x + z < y``, 647 DECIDE ``x - y <= z <=> x <= y + z``, 648 DECIDE ``x <= y - z <=> (x = 0) \/ x + z <= y``, 649 DECIDE ``x - y < z <=> 0 < z /\ x < z + y``, 650 DECIDE ``(x - y = z) <=> x < y /\ (z = 0) \/ (x = y + z)``, 651 DECIDE ``(x <> 0) = 0 < x``, 652 DECIDE ``(0 <> x) = 0 < x``, 653 DECIDE ``~(0 < x) = (x = 0)``], 654 dprocs = [], filter = NONE} 655end 656 657(* val _ = BasicProvers.augment_srw_ss [ARITH_NORM_ss] *) 658 659 660 661end (* numSimps *) 662