1structure IntDP_Munge :> IntDP_Munge = 2struct 3 4structure Parse = struct 5 open Parse 6 val (Type,Term) = parse_from_grammars int_arithTheory.int_arith_grammars 7end 8open Parse 9 10open HolKernel boolLib intSyntax boolSyntax CooperSyntax integerTheory 11 int_arithTheory intReduce 12 13val ERR = mk_HOL_ERR "IntDP_Munge"; 14 15val normalise_mult = OmegaMath.NORMALISE_MULT 16 17(* this draws on similar code in Richard Boulton's natural number 18 arithmetic decision procedure *) 19 20fun contains_var tm = 21 if numSyntax.is_numeral tm then false 22 else 23 case dest_term tm of 24 COMB(f,x) => contains_var f orelse contains_var x 25 | LAMB(v,b) => contains_var b 26 | VAR _ => true 27 | CONST{Ty, ...} => Ty = numSyntax.num orelse Ty = int_ty 28fun is_linear_mult tm = 29 is_mult tm andalso 30 not (contains_var (rand tm) andalso contains_var (rand (rator tm))) 31fun land tm = rand (rator tm) 32 33fun non_zero tm = 34 if is_negated tm then non_zero (rand tm) 35 else tm !~ zero_tm 36 37(* returns a list of pairs, where the first element of each pair is a non- 38 Presburger term that occurs in tm, and where the second is a boolean 39 that is true if none of the variables that occur in the term are 40 bound by a quantifier. *) 41fun bcmp (b1, b2) = if b1 = b2 then EQUAL else if not b1 then LESS else GREATER 42val cmp = pair_compare (Term.compare, bcmp) 43val E = HOLset.empty cmp 44fun non_presburger_subterms0 ctxt tm = 45 if 46 (is_forall tm orelse is_exists1 tm orelse is_exists tm) andalso 47 (type_of (bvar (rand tm)) = int_ty) 48 then let 49 val abst = rand tm 50 in 51 non_presburger_subterms0 (listset [bvar abst] Un ctxt) (body abst) 52 end 53 else if is_neg tm orelse is_absval tm orelse is_negated tm then 54 non_presburger_subterms0 ctxt (rand tm) 55 else if (is_cond tm) then let 56 val (b, t1, t2) = dest_cond tm 57 in 58 non_presburger_subterms0 ctxt b Un non_presburger_subterms0 ctxt t1 Un 59 non_presburger_subterms0 ctxt t2 60 end 61 else if (is_greater tm orelse is_geq tm orelse is_eq tm orelse 62 is_less tm orelse is_leq tm orelse is_conj tm orelse 63 is_disj tm orelse is_imp tm orelse is_plus tm orelse 64 is_minus tm orelse is_linear_mult tm) then 65 non_presburger_subterms0 ctxt (land tm) Un 66 non_presburger_subterms0 ctxt (rand tm) 67 else if (is_divides tm andalso is_int_literal (land tm)) then 68 non_presburger_subterms0 ctxt (rand tm) 69 else if ((is_div tm orelse is_mod tm) andalso 70 is_int_literal (rand tm) andalso 71 non_zero (rand tm)) then 72 non_presburger_subterms0 ctxt (land tm) 73 else if is_int_literal tm then E 74 else if is_var tm andalso type_of tm = int_ty then E 75 else if Teq tm orelse Feq tm then E 76 else HOLset.add(E, 77 (tm, not (HOLset.foldl 78 (fn (v,acc) => acc orelse free_in v tm) 79 false 80 ctxt))) 81 82val is_presburger = HOLset.isEmpty o non_presburger_subterms0 ES 83fun non_presburger_subterms t = 84 HOLset.foldl (fn ((t,b),A) => t::A) [] (non_presburger_subterms0 ES t) 85 86fun is_natlin_mult tm = 87 numSyntax.is_mult tm andalso 88 not (contains_var (land tm) andalso contains_var (rand tm)) 89 90fun nat_nonpresburgers tm = 91 if is_forall tm orelse is_exists tm orelse is_exists1 tm then 92 nat_nonpresburgers (body (rand tm)) 93 else if is_conj tm orelse is_disj tm orelse 94 (is_imp tm andalso not (is_neg tm)) orelse 95 is_greater tm orelse is_leq tm orelse is_eq tm orelse 96 is_minus tm orelse is_less tm orelse is_geq tm orelse 97 is_linear_mult tm 98 then 99 HOLset.union (nat_nonpresburgers (land tm), nat_nonpresburgers (rand tm)) 100 else if is_neg tm orelse is_injected tm orelse is_Num tm orelse 101 numSyntax.is_suc tm 102 then 103 nat_nonpresburgers (rand tm) 104 else if is_cond tm then 105 HOLset.union 106 (HOLset.union (nat_nonpresburgers (rand (rator (rator tm))), 107 nat_nonpresburgers (land tm)), 108 nat_nonpresburgers (rand tm)) 109 else 110 let open numSyntax 111 in 112 if is_greater tm orelse is_geq tm orelse is_less tm orelse 113 is_leq tm orelse is_plus tm orelse is_minus tm orelse 114 is_natlin_mult tm 115 then 116 HOLset.union (nat_nonpresburgers (land tm), 117 nat_nonpresburgers (rand tm)) 118 else if is_numeral tm then empty_tmset 119 else if is_var tm then empty_tmset 120 else HOLset.add(empty_tmset, tm) 121 end 122 123val x_var = mk_var("x", int_ty) 124val c_var = mk_var("c", int_ty) 125fun elim_div_mod0 exp t = let 126 val divmods = 127 HOLset.listItems (find_free_terms (fn t => is_mod t orelse is_div t) t) 128 fun elim_t to_elim = let 129 val ((num,divisor), c1, c2, thm) = let 130 val (c1, c2) = if exp then (RAND_CONV o LAND_CONV, RAND_CONV o RAND_CONV) 131 else (LAND_CONV o RAND_CONV, RAND_CONV) 132 in 133 (dest_div to_elim, c1, c2, if exp then INT_DIV_P else INT_DIV_FORALL_P) 134 handle HOL_ERR _ => (dest_mod to_elim, c1, c2, 135 if exp then INT_MOD_P else INT_MOD_FORALL_P) 136 end 137 val div_nzero = EQT_ELIM (REDUCE_CONV (mk_neg(mk_eq(divisor, zero_tm)))) 138 val abs_div = REDUCE_CONV (mk_absval divisor) 139 val rwt = MP (Thm.INST [x_var |-> num, c_var |-> divisor] (SPEC_ALL thm)) 140 div_nzero 141 in 142 UNBETA_CONV to_elim THENC REWR_CONV rwt THENC 143 STRIP_QUANT_CONV (c1 REDUCE_CONV THENC c2 BETA_CONV) 144 end 145in 146 case divmods of 147 [] => ALL_CONV 148 | _ => FIRST_CONV (map elim_t divmods) THENC elim_div_mod0 exp 149end t 150 151fun elim_div_mod t = let 152 (* can't just apply elim_div_mod to a term with quantifiers because the 153 elimination of x/c relies on x being free. So we need to traverse 154 the term underneath the quantifiers. It may also help to get the 155 quantifiers to have scope over as little of the term as possible. *) 156 val exp = goal_qtype t = qsEXISTS 157 fun recurse passed_a_binder tm = let 158 in 159 if is_exists tm orelse is_forall tm orelse is_exists1 tm then 160 BINDER_CONV (recurse true) 161 else if is_abs tm then ABS_CONV (recurse true) 162 else 163 (if passed_a_binder then TRY_CONV (elim_div_mod0 exp) 164 else ALL_CONV) THENC 165 SUB_CONV (recurse false) 166 end tm 167in 168 recurse true t 169end 170 171 172fun decide_fv_presburger DPname DP tm = let 173 fun is_int_const tm = type_of tm = int_ty andalso is_const tm 174 val fvs = free_vars tm @ (Lib.op_mk_set aconv (find_terms is_int_const tm)) 175 fun dest_atom tm = dest_const tm handle HOL_ERR _ => dest_var tm 176 fun gen(bv, t) = 177 if is_var bv then mk_forall(bv, t) 178 else let 179 val gv = genvar int_ty 180 in 181 mk_forall(gv, subst [bv |-> gv] t) 182 end 183 val preprocess = elim_div_mod THENC REWRITE_CONV [INT_ABS] 184 val doit = preprocess THENC DP 185in 186 if null fvs then doit tm 187 else let 188 val newtm = List.foldr gen tm fvs (* as there are no non-presburger 189 sub-terms, all these variables 190 will be of integer type *) 191 in 192 EQT_INTRO (SPECL fvs (EQT_ELIM (doit newtm))) 193 end handle HOL_ERR _ => 194 raise ERR DPname 195 ("Tried to prove generalised goal (generalising "^ 196 #1 (dest_atom (hd fvs))^"...) but it was false") 197end 198 199 200fun abs_inj inj_n tm = let 201 val gv = genvar int_ty 202 val tm1 = subst [inj_n |-> gv] tm 203in 204 GSYM (BETA_CONV (mk_comb(mk_abs(gv,tm1), inj_n))) 205end 206 207fun eliminate_nat_quants tm = let 208in 209 if is_forall tm orelse is_exists tm orelse is_exists1 tm then let 210 val (bvar, body) = dest_abs (rand tm) 211 in 212 if type_of bvar = num_ty then let 213 val inj_bvar = mk_comb(int_injection, bvar) 214 val rewrite_qaway = 215 REWR_CONV (if is_forall tm then INT_NUM_FORALL 216 else if is_exists tm then INT_NUM_EXISTS 217 else INT_NUM_UEXISTS) THENC 218 BINDER_CONV (RAND_CONV BETA_CONV) 219 in 220 BINDER_CONV (abs_inj inj_bvar) THENC rewrite_qaway THENC 221 RENAME_VARS_CONV [#1 (dest_var bvar)] THENC 222 BINDER_CONV eliminate_nat_quants 223 end 224 else 225 BINDER_CONV eliminate_nat_quants 226 end 227 else if is_neg tm then (* must test for is_neg before is_imp *) 228 RAND_CONV eliminate_nat_quants 229 else if (is_conj tm orelse is_disj tm orelse is_eq tm orelse 230 is_imp tm) then 231 BINOP_CONV eliminate_nat_quants 232 else if is_cond tm then 233 RAND_CONV eliminate_nat_quants THENC 234 LAND_CONV eliminate_nat_quants THENC 235 RATOR_CONV (RATOR_CONV (RAND_CONV eliminate_nat_quants)) 236 else ALL_CONV 237end tm handle HOL_ERR {origin_function = "REWR_CONV", ...} => 238 raise ERR "IntDP_Munge" "Uneliminable natural number term remains" 239 240 241fun tacTHEN t1 t2 tm = let 242 val (g1, v1) = t1 tm 243 val (g2, v2) = t2 g1 244in 245 (g2, v1 o v2) 246end 247fun tacALL tm = (tm, I) 248fun tacMAP_EVERY tlist = 249 case tlist of 250 [] => tacALL 251 | (t1::ts) => tacTHEN t1 (tacMAP_EVERY ts) 252fun tacCONV c tm = let 253 val thm = c tm 254in 255 (rhs (concl thm), TRANS thm) 256end handle UNCHANGED => (tm, I) 257fun tacRGEN t = let 258 val (fvs, body) = strip_forall t 259 val prove_it = EQT_INTRO o GENL fvs o EQT_ELIM 260in 261 (body, prove_it) 262end 263val op tTHEN = fn (t1, t2) => tacTHEN t1 t2 264infix tTHEN 265 266 267fun subtm_rel (t1, t2) = 268 case Int.compare(term_size t1, term_size t2) of 269 LESS => GREATER 270 | EQUAL => EQUAL 271 | GREATER => LESS 272 273local 274 open arithmeticTheory numSyntax 275 val Num_lemma = prove( 276 ``&(Num i) = if 0 <= i then i else & ((Num o I) i)``, 277 COND_CASES_TAC THEN 278 ASM_REWRITE_TAC [combinTheory.o_THM, integerTheory.INT_OF_NUM, 279 combinTheory.I_THM]) 280 281 val rewrites = [GSYM INT_INJ, GSYM INT_LT, GSYM INT_LE, 282 GREATER_DEF, GREATER_EQ, GSYM INT_ADD, 283 GSYM INT_MUL, INT, INT_NUM_COND, Num_lemma] 284 val p_var = mk_var("p", num) 285 val q_var = mk_var("q", num) 286 fun elim_div_mod0 exp t = let 287 val divmods = 288 HOLset.listItems (find_free_terms (fn t => is_mod t orelse is_div t) t) 289 fun elim_t to_elim = let 290 val ((num,divisor), (thm, c)) = 291 (dest_div to_elim, if exp then (DIV_P, RAND_CONV) 292 else (DIV_P_UNIV, I)) 293 handle HOL_ERR _ => (dest_mod to_elim, if exp then (MOD_P, RAND_CONV) 294 else (MOD_P_UNIV, I)) 295 val div_nzero = EQT_ELIM (REDUCE_CONV (mk_less(zero_tm, divisor))) 296 fun findinst thm = 297 Thm.INST (#1 (match_term (rand (lhs (#2 (dest_imp (concl thm))))) 298 to_elim)) 299 thm 300 val rwt = MP (findinst (SPEC_ALL thm)) div_nzero 301 in 302 UNBETA_CONV to_elim THENC REWR_CONV rwt THENC 303 STRIP_QUANT_CONV (RAND_CONV (c BETA_CONV)) 304 end 305 in 306 case divmods of 307 [] => ALL_CONV 308 | _ => FIRST_CONV (map elim_t divmods) THENC elim_div_mod0 exp 309 end t 310 fun elim_div_mod t = let 311 val exp = goal_qtype t = qsEXISTS andalso 312 HOLset.isEmpty (nat_nonpresburgers t) 313 fun recurse passed_a_binder tm = let 314 in 315 if is_exists tm orelse is_forall tm orelse is_exists1 tm then 316 BINDER_CONV (recurse true) 317 else if is_abs tm then 318 ABS_CONV (recurse true) 319 else 320 (if passed_a_binder then TRY_CONV (elim_div_mod0 exp) 321 else ALL_CONV) THENC 322 SUB_CONV (recurse false) 323 end tm 324 in 325 recurse true t 326 end 327 fun term_size t = let 328 val (f,x) = dest_comb t 329 in 330 term_size f + term_size x 331 end handle HOL_ERR _ => term_size (body t) + 1 332 handle HOL_ERR _ => 1 333 334 (* two functions below derived from RJB's Sub_and_cond.sml *) 335 fun op_of_app tm = op_of_app (rator tm) handle _ => tm 336in 337 fun COND_ABS_CONV tm = let 338 open Rsyntax 339 val {Bvar=v,Body=bdy} = dest_abs tm 340 val {cond,larm=x,rarm=y} = Rsyntax.dest_cond bdy 341 val b = assert (not o tmem v o free_vars) cond 342 val _ = assert (fn t => type_of t <> bool) x 343 val xf = mk_abs{Bvar=v,Body=x} 344 val yf = mk_abs{Bvar=v,Body=y} 345 val th1 = INST_TYPE [alpha |-> type_of v, beta |-> type_of x] COND_ABS 346 val th2 = SPECL [b,xf,yf] th1 347 in 348 CONV_RULE (RATOR_CONV 349 (RAND_CONV (ABS_CONV 350 (RATOR_CONV (RAND_CONV BETA_CONV) THENC 351 RAND_CONV BETA_CONV) THENC 352 ALPHA_CONV v))) th2 353 end handle HOL_ERR _ => failwith "COND_ABS_CONV" 354 val NBOOL_COND_RATOR_CONV = REWR_CONV COND_RATOR 355 fun NBOOL_COND_RAND_CONV tm = let 356 val (f, cnd) = dest_comb tm 357 in 358 if same_const f conditional orelse 359 (type_of (rand cnd) <> bool andalso 360 not (same_const (op_of_app f) conditional)) 361 then 362 (* guard above allows rewrite of 363 COND (COND p q r) x y 364 which will go to 365 (COND p (COND q) (COND r)) x y 366 COND q and COND r will get exposed to x and y ; term duplicates 367 x and y; hope this doens't happen too often. *) 368 REWR_CONV COND_RAND tm 369 else 370 NO_CONV tm 371 end 372 373val nat_rewrites = 374 [arithmeticTheory.LEFT_ADD_DISTRIB, arithmeticTheory.RIGHT_ADD_DISTRIB, 375 arithmeticTheory.MAX_DEF, arithmeticTheory.MIN_DEF, 376 arithmeticTheory.ODD_EXISTS, arithmeticTheory.EVEN_EXISTS] 377 378val dealwith_nats = let 379 val phase1 = 380 tacCONV (PURE_REWRITE_CONV nat_rewrites THENC 381 ONCE_DEPTH_CONV normalise_mult THENC 382 elim_div_mod THENC 383 (* eliminate nasty subtractions *) 384 TOP_DEPTH_CONV (Thm_convs.SUB_NORM_CONV ORELSEC 385 NBOOL_COND_RATOR_CONV ORELSEC 386 NBOOL_COND_RAND_CONV ORELSEC 387 COND_ABS_CONV)) 388 fun do_pbs tm = let 389 val non_pbs0 = HOLset.listItems (nat_nonpresburgers tm) 390 val non_pbs = Listsort.sort subtm_rel 391 (List.filter (equal num_ty o type_of) non_pbs0) 392 val initially = 393 if null non_pbs then tacALL 394 else if goal_qtype tm = qsUNIV then 395 tacCONV move_quants_up tTHEN tacRGEN 396 else tacRGEN 397 fun tactic subtm tm = let 398 (* return both a newtm and a function that will convert a theorem 399 of the form <new term> = T into tm = T *) 400 val gv = genvar numSyntax.num 401 val newterm = mk_forall (gv, Term.subst [subtm |-> gv] tm) 402 fun prove_it thm = 403 EQT_INTRO (SPEC subtm (EQT_ELIM thm)) 404 handle HOL_ERR _ => 405 raise ERR "COOPER_CONV" 406 ("Tried to prove generalised goal (generalising "^ 407 Parse.term_to_string subtm^"...) but it was false") 408 in 409 (newterm, prove_it) 410 end 411 in 412 initially tTHEN tacMAP_EVERY (map tactic non_pbs) 413 end tm 414in 415 phase1 tTHEN do_pbs tTHEN 416 tacCONV (PURE_REWRITE_CONV rewrites THENC eliminate_nat_quants) 417end 418end (* local *) 419 420(* subterms is a list of subterms all of integer type *) 421fun decide_nonpbints_presburger DPname DP subterms tm = let 422 fun tactic subtm tm = 423 (* return both a new term and a function that will convert a theorem 424 of the form <new term> = T into tm = T *) 425 if is_comb subtm andalso rator subtm ~~ int_injection then let 426 val n = rand subtm 427 val thm0 = abs_inj subtm tm (* |- tm = P subtm *) 428 val tm0 = rhs (concl thm0) 429 val gv = genvar num_ty 430 val tm1 = mk_forall(gv, mk_comb (rator tm0, mk_comb(int_injection, gv))) 431 val thm1 = (* |- (!gv. P gv) = !x. 0 <= x ==> P x *) 432 (REWR_CONV INT_NUM_FORALL THENC 433 BINDER_CONV (RAND_CONV BETA_CONV)) tm1 434 fun prove_it thm = let 435 val without_true = EQT_ELIM thm (* |- !x. 0 <= x ==> P x *) 436 val univ_nat = EQ_MP (SYM thm1) without_true 437 val spec_nat = SPEC n univ_nat 438 in 439 EQT_INTRO (EQ_MP (SYM thm0) spec_nat) 440 end 441 in 442 (rhs (concl thm1), prove_it) 443 end 444 else let 445 val gv = genvar int_ty 446 in 447 (mk_forall(gv, subst [subtm |-> gv] tm), 448 EQT_INTRO o SPEC subtm o EQT_ELIM) 449 end 450 val (goal, vfn) = tacMAP_EVERY (map tactic subterms) tm 451 val thm = decide_fv_presburger DPname DP goal 452in 453 vfn thm handle HOL_ERR _ => 454 raise ERR DPname 455 ("Tried to prove generalised goal (generalising "^ 456 Parse.term_to_string (hd subterms)^"...) but it was false") 457end 458 459val int_rewrites = 460 [INT_LDISTRIB, INT_RDISTRIB, INT_MAX, INT_MIN] 461 462fun BASIC_CONV DPname DP tm = let 463 val (natgoal, natvalidation) = dealwith_nats tm 464 val stage1 = PURE_REWRITE_CONV int_rewrites THENC 465 ONCE_DEPTH_CONV normalise_mult 466 fun stage2 tm = 467 let 468 val non_pbs = non_presburger_subterms0 ES tm 469 in 470 if HOLset.isEmpty non_pbs then decide_fv_presburger DPname DP tm 471 else 472 case HOLset.find (fn (t,_) => type_of t <> int_ty) non_pbs of 473 NONE => let 474 val (igoal, initvfn) = 475 case HOLset.find (fn (_, b) => not b) non_pbs of 476 NONE => (tm, I) 477 | SOME _ => 478 if goal_qtype tm = qsUNIV then 479 (tacCONV move_quants_up tTHEN tacRGEN) tm 480 else tacRGEN tm 481 val init_nonpbs = 482 Listsort.sort (inv_img_cmp #1 subtm_rel) 483 (HOLset.listItems 484 (non_presburger_subterms0 ES igoal)) 485 in 486 case List.find (fn (_, b) => not b) init_nonpbs of 487 NONE => 488 initvfn (decide_nonpbints_presburger 489 DPname 490 DP 491 (map #1 init_nonpbs) igoal) 492 | SOME (t, _) => 493 raise ERR DPname 494 ("Couldn't free quantification over non-Presburger "^ 495 "sub-term "^Parse.term_to_string t) 496 end 497 | SOME (t,_) => raise ERR DPname 498 ("Not in the allowed subset; consider "^Parse.term_to_string t) 499 end 500in 501 natvalidation ((stage1 THENC stage2) natgoal) 502end 503 504fun ok_asm th = let 505 val exists_th = goal_qtype (concl th) = qsEXISTS 506 fun check(t, free_p) = 507 mem (type_of t) [intSyntax.int_ty, numSyntax.num] andalso 508 (exists_th orelse free_p) 509 val dodgy_subterms0 = non_presburger_subterms0 ES (concl th) 510 fun ignore_nats ((t, free_p), acc) = let 511 val nat_set = nat_nonpresburgers t 512 fun foldthis (nt, acc) = HOLset.add(acc, (nt, free_p)) 513 in 514 HOLset.foldl foldthis acc nat_set 515 end 516 val dodgy_subterms = HOLset.foldl ignore_nats E dodgy_subterms0 517in 518 not (isSome (HOLset.find (not o check) dodgy_subterms)) 519end 520 521fun conv_tac c = 522 REPEAT (FIRST_X_ASSUM (MP_TAC o assert ok_asm)) THEN 523 CONV_TAC c 524 525end; (* struct *) 526