1structure CooperSyntax :> CooperSyntax = struct 2 3(* simple term manipulation functions, some term literals, and some 4 conversions, all intended for very specific use within the 5 implementation of Cooper's algorithm *) 6 7open HolKernel boolLib intSyntax intReduce CooperThms 8open int_arithTheory integerTheory 9 10 11(* Fix the grammar used by this file *) 12structure Parse = struct 13 open Parse 14 val (Type,Term) = parse_from_grammars integer_grammars 15end 16open Parse 17 18val ERR = mk_HOL_ERR "CooperSyntax"; 19 20val not_tm = boolSyntax.negation; 21val num_ty = numSyntax.num 22val true_tm = boolSyntax.T 23val false_tm = boolSyntax.F 24 25fun strip_exists tm = let 26 fun recurse acc tm = let 27 val (v, body) = dest_exists tm 28 in 29 recurse (v::acc) body 30 end handle HOL_ERR _ => (List.rev acc, tm) 31in 32 recurse [] tm 33end 34 35(* ---------------------------------------------------------------------- *) 36(* functions for dealing with "conjunctions" and "disjunctions"; logical *) 37(* operators that might have their meaning concealed under negations *) 38(* ---------------------------------------------------------------------- *) 39 40val cpstrip_conj = let 41 (* treats negations over disjunctions as conjunctions *) 42 fun doit posp acc tm = let 43 val (l,r) = (if posp then dest_conj else dest_disj) tm 44 in 45 doit posp (doit posp acc r) l 46 end handle HOL_ERR _ => let 47 val t0 = dest_neg tm 48 in 49 doit (not posp) acc t0 50 end handle HOL_ERR _ => if posp then tm::acc else mk_neg tm :: acc 51in 52 doit true [] 53end 54 55val cpstrip_disj = let 56 (* treats negations over conjunctions as disjunctions *) 57 fun doit posp acc tm = let 58 val (l,r) = (if posp then dest_disj else dest_conj) tm 59 in 60 doit posp (doit posp acc r) l 61 end handle HOL_ERR _ => let 62 val t0 = dest_neg tm 63 in 64 doit (not posp) acc t0 65 end handle HOL_ERR _ => if posp then tm::acc else mk_neg tm :: acc 66in 67 doit true [] 68end 69 70datatype term_op = CONJN | DISJN | NEGN 71fun characterise t = 72 (case #1 (dest_const (#1 (strip_comb t))) of 73 "/\\" => SOME CONJN 74 | "\\/" => SOME DISJN 75 | "~" => SOME NEGN 76 | _ => NONE) handle HOL_ERR _ => NONE 77val bop_characterise = characterise 78 79 80datatype reltype = rEQ | rDIV | rLT 81fun categorise_leaf tm = let 82 val (c, _) = strip_comb tm 83in 84 case dest_const c of 85 ("int_lt", _) => rLT 86 | ("=", _) => rEQ 87 | ("int_divides", _) => rDIV 88 | _ => raise Fail "categorise leaf applied to non Cooper leaf" 89end 90 91 92fun cpEVERY_CONJ_CONV c tm = let 93 fun findconjunct posp tm = 94 case (characterise tm, posp) of 95 (SOME CONJN, true) => BINOP_CONV (findconjunct posp) tm 96 | (SOME DISJN, false) => BINOP_CONV (findconjunct posp) tm 97 | (SOME NEGN, _) => RAND_CONV (findconjunct (not posp)) tm 98 | _ => c tm 99in 100 findconjunct true tm 101end 102 103fun cpEVERY_DISJ_CONV c tm = let 104 fun finddisj posp tm = 105 case (characterise tm, posp) of 106 (SOME DISJN, true) => BINOP_CONV (finddisj posp) tm 107 | (SOME CONJN, false) => BINOP_CONV (finddisj posp) tm 108 | (SOME NEGN, _) => RAND_CONV (finddisj (not posp)) tm 109 | _ => c tm 110in 111 finddisj true tm 112end 113 114fun cpis_disj tm = 115 is_disj tm orelse let 116 val tm0 = dest_neg tm 117 in 118 cpis_conj tm0 119 end handle HOL_ERR _ => false 120and cpis_conj tm = 121 is_conj tm orelse let 122 val tm0 = dest_neg tm 123 in 124 cpis_disj tm0 125 end handle HOL_ERR _ => false 126 127 128val int_exists = mk_thy_const{Name = "?", Thy = "bool", 129 Ty = (int_ty --> bool) --> bool} 130val int_forall = mk_thy_const{Name = "!", Thy = "bool", 131 Ty = (int_ty --> bool) --> bool} 132 133val has_exists = free_in int_exists 134val has_forall = free_in int_forall 135 136fun has_quant t = 137 (* assumes that all head terms are not abstractions *) 138 if is_abs t then has_quant (body t) 139 else let 140 val (f, args) = strip_comb t 141 in 142 f = int_exists orelse f = int_forall orelse 143 List.exists has_quant args 144 end 145 146 147(* ---------------------------------------------------------------------- 148 goal_qtype t 149 150 returns one of EITHER | NEITHER | qsUNIV | qsEXISTS 151 152 EITHER is returned if t has no quantifiers. 153 NEITHER is returned if t has both sorts 154 qsUNIV is returned if t has only universal quantifiers. 155 qsEXISTS is returned if t has only existential quantifiers. 156 157 Pays attention to negations. Boolean operators in the term must be 158 no more than 159 /\, \/, ~, =, ==> and if-then-else 160 ---------------------------------------------------------------------- *) 161 162datatype qstatus = EITHER | NEITHER | qsUNIV | qsEXISTS 163exception return_NEITHER 164fun negstatus s = case s of qsUNIV => qsEXISTS | qsEXISTS => qsUNIV | x => x 165fun goal_qtype tm = let 166 fun recurse acc tm = let 167 val (l, r) = dest_conj tm 168 handle HOL_ERR _ => dest_disj tm 169 handle HOL_ERR _ => let 170 val (g, t, e) = dest_cond tm 171 in 172 if recurse EITHER g <> EITHER then raise return_NEITHER 173 else (t,e) 174 end 175 handle HOL_ERR _ => let 176 val _ = assert (not o is_neg) tm 177 val (l, r) = dest_imp tm 178 in 179 (mk_neg l, r) 180 end 181 in 182 case (acc, recurse acc l) of 183 (_, EITHER) => recurse acc r 184 | (_, NEITHER) => NEITHER 185 | (EITHER, x) => recurse x r 186 | _ => recurse acc r 187 end handle HOL_ERR _ => let 188 val (f, args) = strip_comb tm 189 in 190 case (#Name (dest_thy_const f), acc) of 191 ("~", _) => negstatus (recurse (negstatus acc) (hd args)) 192 | ("!", qsEXISTS) => NEITHER 193 | ("!", _) => recurse qsUNIV (body (hd args)) 194 | ("?", qsUNIV) => NEITHER 195 | ("?", _) => recurse qsEXISTS (body (hd args)) 196 | ("?!", _) => NEITHER 197 | ("=", _) => if type_of (hd args) = bool then 198 if recurse EITHER (hd args) <> EITHER then 199 NEITHER 200 else if recurse EITHER (hd (tl args)) <> EITHER then 201 NEITHER 202 else acc 203 else acc 204 | _ => acc 205 end handle HOL_ERR _ => acc 206in 207 recurse EITHER tm handle return_NEITHER => NEITHER 208end 209 210(* ---------------------------------------------------------------------- 211 finds sub-terms satisfying given predicate that do not have any of 212 their free variables bound by binders higher in the same term 213 ---------------------------------------------------------------------- *) 214 215fun find_free_terms P t = let 216 fun recurse binders acc tm = let 217 val newset = 218 if P tm then let 219 val tm_frees = FVL [tm] empty_tmset 220 in 221 if HOLset.isEmpty (HOLset.intersection(tm_frees, binders)) then 222 HOLset.add(acc, tm) 223 else acc 224 end 225 else acc 226 in 227 case dest_term tm of 228 LAMB(v, body) => recurse (HOLset.add(binders, v)) newset body 229 | COMB(f,x) => recurse binders (recurse binders newset f) x 230 | _ => newset 231 end 232in 233 recurse empty_tmset empty_tmset t 234end 235 236(* ---------------------------------------------------------------------- *) 237(* Moving quantifiers as high as possible in a term *) 238(* ---------------------------------------------------------------------- *) 239 240val move_quants_up = 241 REDEPTH_CONV (OR_EXISTS_CONV ORELSEC 242 LEFT_OR_EXISTS_CONV ORELSEC RIGHT_OR_EXISTS_CONV ORELSEC 243 LEFT_AND_EXISTS_CONV ORELSEC RIGHT_AND_EXISTS_CONV ORELSEC 244 NOT_EXISTS_CONV ORELSEC NOT_FORALL_CONV ORELSEC 245 AND_FORALL_CONV ORELSEC 246 LEFT_AND_FORALL_CONV ORELSEC RIGHT_AND_FORALL_CONV ORELSEC 247 LEFT_OR_FORALL_CONV ORELSEC RIGHT_OR_FORALL_CONV ORELSEC 248 RIGHT_IMP_FORALL_CONV ORELSEC RIGHT_IMP_EXISTS_CONV ORELSEC 249 LEFT_IMP_FORALL_CONV ORELSEC LEFT_IMP_EXISTS_CONV) 250 251(* ---------------------------------------------------------------------- *) 252(* Takes !x. P x *) 253(* and produces ~(?x. ~P x) *) 254(* ---------------------------------------------------------------------- *) 255local 256 val NOT_EXISTS_THM = 257 GEN_ALL (SYM 258 (PURE_REWRITE_RULE [NOT_CLAUSES] 259 (BETA_RULE (SPEC (Term`\x:'a. ~ P x : bool`) 260 boolTheory.NOT_EXISTS_THM)))) 261in 262 263 fun flip_forall tm = let 264 val (bvar, _) = dest_forall tm 265 in 266 BINDER_CONV (UNBETA_CONV bvar) THENC 267 REWR_CONV NOT_EXISTS_THM THENC 268 RAND_CONV (BINDER_CONV (RAND_CONV BETA_CONV)) THENC 269 RAND_CONV (RENAME_VARS_CONV [#1 (dest_var bvar)]) 270 end tm 271end 272 273 274 275(* ---------------------------------------------------------------------- *) 276(* If term is !x y z... . body *) 277(* change it to ~(?x y z... . body) *) 278(* ---------------------------------------------------------------------- *) 279 280fun flip_foralls tm = let 281 val (bvar, body) = dest_forall tm 282in 283 BINDER_CONV flip_foralls THENC flip_forall THENC 284 TRY_CONV (RAND_CONV (BINDER_CONV (REWR_CONV NOT_NOT_P))) 285end tm handle HOL_ERR _ => ALL_CONV tm 286 287(* ---------------------------------------------------------------------- *) 288(* Counts number of occurrences of variables in term with given name *) 289(* ---------------------------------------------------------------------- *) 290 291fun count_occurrences str tm = let 292 fun recurse acc tm = 293 case strip_comb tm of 294 (f, []) => ((if #1 (dest_var f) = str then 1 + acc else acc) 295 handle HOL_ERR _ => acc) 296 | (_, args) => List.foldl (fn(t,a) => recurse a t) acc args 297in 298 recurse 0 tm 299end 300 301fun count_vars tm = let 302 open Binarymap 303 fun recurse (tm,dict) = 304 case strip_comb tm of 305 (f, []) => let 306 in let 307 val n = #1 (dest_var f) 308 in 309 case peek(dict,n) of 310 NONE => insert(dict, n, 1) 311 | SOME i => insert(dict, n, i+1) 312 end handle HOL_ERR _ => dict end 313 | (_, args) => List.foldl recurse dict args 314in 315 listItems (recurse (tm, mkDict String.compare)) 316end 317 318(* dealing with constraints of the form lo < x /\ x <= hi *) 319val resquan_onestep = 320 REWR_CONV restricted_quantification_simp THENC 321 REDUCE_CONV THENC REWRITE_CONV [] 322 323fun resquan_remove tm = 324 (resquan_onestep THENC TRY_CONV (RAND_CONV resquan_remove) THENC 325 REWRITE_CONV []) tm 326 327 328 329 330 331 332val bmarker_tm = prim_mk_const { Name = "bmarker", Thy = "int_arith"}; 333 334val mk_bmark_thm = GSYM int_arithTheory.bmarker_def 335fun mk_bmark tm = SPEC tm mk_bmark_thm 336 337val NOT_NOT = tautLib.TAUT_PROVE ``~~p:bool = p`` 338 339fun mark_conjunct P tm = let 340in 341 if is_conj tm then 342 LAND_CONV (mark_conjunct P) ORELSEC RAND_CONV (mark_conjunct P) 343 else if is_neg tm then 344 if is_disj (rand tm) then 345 REWR_CONV NOT_OR THENC mark_conjunct P 346 else if is_neg (rand tm) then 347 REWR_CONV NOT_NOT THENC mark_conjunct P 348 else if P tm then 349 mk_bmark 350 else NO_CONV 351 else if P tm then 352 mk_bmark 353 else NO_CONV 354end tm 355 356val move_bmarked_left = PURE_REWRITE_CONV [bmarker_rewrites] THENC 357 LAND_CONV (REWR_CONV int_arithTheory.bmarker_def) 358fun move_conj_left P = mark_conjunct P THENC move_bmarked_left 359 360 361(* special "constraint" terms will be wrapped in K terms, with the 362 variable being constrained as the second argument to the combinator. 363 The only free variable in the constraint term will be the constrained 364 variable. Further a constraint will be of the form 365 d1 < j /\ j <= d2 366 for some pair of integer literals d1 and d2, with the variable j. *) 367val constraint_tm = mk_thy_const {Name = "K", Thy = "combin", 368 Ty = bool --> (int_ty --> bool)} 369fun mk_constraint (v,tm) = list_mk_comb(constraint_tm,[tm,v]) 370fun is_constraint tm = let 371 val (f, args) = strip_comb tm 372in 373 f = constraint_tm andalso length args = 2 374end 375fun is_vconstraint v tm = let 376 val (f, args) = strip_comb tm 377in 378 f = constraint_tm andalso length args = 2 andalso 379 free_vars (hd (tl args)) = [v] 380end 381fun constraint_var tm = rand tm 382val lhand = rand o rator 383fun constraint_size tm = let 384 val (_, args) = strip_comb tm 385 val range_tm = hd args 386 val (lo,hi) = dest_conj range_tm 387in 388 Arbint.-(int_of_term (rand hi), int_of_term (lhand lo)) 389end 390fun dest_constraint tm = 391 if is_constraint tm then let 392 val (_, args) = strip_comb tm 393 val (lo,hi) = dest_conj (hd args) 394 in 395 (rand tm, (lhand lo, rand hi)) 396 end 397 else 398 raise ERR "dest_constraint" "Term not a constraint" 399 400 401 402val K_THM = INST_TYPE [(alpha |-> bool), (beta |-> int_ty)] combinTheory.K_THM 403fun MK_CONSTRAINT tm = 404 case free_vars tm of 405 [] => ALL_CONV tm 406 | [v] => SYM (SPECL [tm,v] K_THM) 407 | _ => raise Fail "MK_CONSTRAINT: Term has too many free variables" 408fun UNCONSTRAIN tm = let 409 val (f, args) = strip_comb tm 410in 411 SPECL args K_THM 412end 413fun IN_CONSTRAINT c = UNCONSTRAIN THENC c THENC MK_CONSTRAINT 414 415fun quick_cst_elim tm = let 416 (* eliminates constraints of the form 417 K (lo < x /\ x <= hi) x 418 where hi - lo <= 1, either replacing it with x = lo, or just false 419 fails (NO_CONV) otherwise. *) 420 val (_, args) = strip_comb tm (* K and its args *) 421 val cst = hd args 422 val (_, cstargs) = strip_comb cst (* two conjuncts *) 423 val lo_cst = hd cstargs 424 val hi_cst = hd (tl cstargs) 425 val lo_t = rand (rator lo_cst) 426 val hi_t = rand hi_cst 427 val lo_i = int_of_term lo_t 428 val hi_i = int_of_term hi_t 429 open Arbint 430in 431 if hi_i - lo_i <= one then 432 (UNCONSTRAIN THENC resquan_remove) tm 433 else 434 NO_CONV tm 435end 436 437fun reduce_if_ground tm = 438 (* calls REDUCE_CONV on a ground term, does nothing otherwise *) 439 if is_exists tm orelse not (HOLset.isEmpty (FVL [tm] empty_tmset)) 440 then ALL_CONV tm 441 else REDUCE_CONV tm 442 443 444fun fixup_newvar tm = let 445 (* takes an existential term and replaces all occurrences of the bound 446 variable in the body with 1 * v, except that we don't need to go 447 looking for this variable under multiplications, nor under 448 constraint terms *) 449 val (v,body) = dest_exists tm 450 val replace_thm = SYM (SPEC v INT_MUL_LID) 451 fun recurse tm = let 452 val (f, args) = strip_comb tm 453 in 454 case args of 455 [] => if Term.compare(v,tm) = EQUAL then replace_thm 456 else ALL_CONV tm 457 | [_] => RAND_CONV recurse tm 458 | [_,_] => if Term.compare(f, constraint_tm) = EQUAL orelse 459 Term.compare(f, mult_tm) = EQUAL then ALL_CONV tm 460 else BINOP_CONV recurse tm 461 | _ => raise ERR "fixup_newvar" 462 ("found ternary operator - "^term_to_string tm) 463 end 464in 465 QCONV (BINDER_CONV recurse) tm 466end 467 468fun myEXISTS_OR_CONV tm = let 469 (* this version of EXISTS_OR_CONV is quicker than the system default, 470 possibly because it doesn't bother with keeping the variable names 471 the same on the RHS of the theorem returned *) 472 val (v,body) = dest_exists tm 473in 474 BINDER_CONV (BINOP_CONV (UNBETA_CONV v)) THENC 475 REWR_CONV EXISTS_OR_THM THENC 476 BINOP_CONV (BINDER_CONV BETA_CONV (* THENC RAND_CONV (ALPHA_CONV v) *)) 477end tm 478 479 480 481(* with ?x. p \/ q \/ r... 482 expand to (?x. p) \/ (?x.q) \/ (?x.r) ... 483*) 484fun push_one_exists_over_many_disjs tm = 485 ((myEXISTS_OR_CONV THENC BINOP_CONV push_one_exists_over_many_disjs) ORELSEC 486 ALL_CONV) tm 487 488fun push_in_exists tm = 489 (* takes all existentials that are over disjuncts, and pushes them *) 490 (* over the disjuncts, preserving the order *) 491 if is_exists tm then 492 (BINDER_CONV push_in_exists THENC 493 push_one_exists_over_many_disjs) tm 494 else 495 ALL_CONV tm 496 497(*val push_in_exists = Profile.profile "push_in" push_in_exists*) 498 499fun remove_vacuous_existential tm = let 500 (* term is of form ?x. x = e *) 501 val value = rhs (#2 (dest_exists tm)) 502 val thm = ISPEC value EXISTS_REFL 503in 504 EQT_INTRO thm 505end 506 507 508fun simple_divides var tm = let 509 (* true if a term is a divides, where the right hand side's only 510 free variable is the parameter var *) 511 val (l,r) = dest_divides tm 512in 513 free_vars r = [var] 514end handle HOL_ERR _ => false 515 516 517local exception foo 518in 519fun push_in_exists_and_follow c tm = let 520 (* looking at 521 ?x. ... /\ P x /\ ... 522 where the ... don't contain any instances of x 523 Push the existential in over the conjuncts and finish by applying c 524 to ?x. P x 525 *) 526 val th0 = EXISTS_AND_CONV tm handle HOL_ERR _ => raise foo 527 val tm1 = rhs (concl th0) 528 val goleft = is_exists (#1 (dest_conj tm1)) 529 val cconval = if goleft then LAND_CONV else RAND_CONV 530in 531 (K th0 THENC cconval (push_in_exists_and_follow c)) tm 532end handle foo => c tm 533end 534 535 536(* given (p \/ q \/ r..) /\ s (with the or's right associated) 537 expand to (p /\ s) \/ (q /\ s) \/ (r /\ s) \/ ... 538*) 539fun expand_right_and_over_or tm = 540 ((REWR_CONV RIGHT_AND_OVER_OR THENC 541 BINOP_CONV expand_right_and_over_or) ORELSEC ALL_CONV) tm 542 543fun ADDITIVE_TERMS_CONV c tm = 544 if is_disj tm orelse is_conj tm then 545 BINOP_CONV (ADDITIVE_TERMS_CONV c) tm 546 else if is_neg tm then RAND_CONV (ADDITIVE_TERMS_CONV c) tm 547 else if is_less tm orelse is_divides tm orelse is_eq tm then 548 BINOP_CONV c tm 549 else ALL_CONV tm 550 551 552end 553