1(*------------------------------------------------------------------- 2 * UNWIND_EXISTS_CONV : conv 3 * UNWIND_FORALL_CONV : conv 4 * 5 * DESCRIPTION 6 * 7 * UNWIND_EXISTS_CONV eliminates existential 8 * quantifiers where the quantified variable 9 * is restricted to a single point via an equality in the 10 * conjuncts of the body. Given a term of the form 11 * ?x1 x2 ... xn. P1[x1..xn] /\ P2[x1..xn] /\ ... /\ Pm[x1..xn] 12 * where one of Pk is 13 * "x1 = F[x2...xn]" 14 * or "F[x2...xn] = x1" 15 * or "x1" 16 * or "~x1" 17 * UNWIND_EXISTS_CONV eliminates the variable x1 from the existential 18 * quantification and converts the term to 19 * ?x2...xn. P1'[x2...xn] /\ ...P(m-1)'[x2...xn] 20 * where P1' through Pm-1' have any occurrences of x1 substituted as 21 * F[x2...xn]. 22 * 23 * UNWIND_FORALL_CONV eliminates universal 24 * quantifiers where the quantified variable 25 * is restricted to a single point via an equality in the 26 * conjuncts of the body. Given a term of the form 27 * !x1 x2 ... xn. P1[x1..xn] ==> P2[x1..xn] ==> ... ==> Pm[x1..xn] 28 * where one of Pk (k < m) is 29 * "x1 = F[x2...xn]" 30 * or "F[x2...xn] = x1" 31 * or "x1" 32 * or "~x1" 33 * UNWIND_FORALL_CONV eliminates the variable x1 from the 34 * quantification and converts the term to 35 * !x2...xn. P1'[x2...xn] ==> ...P(m-1)'[x2...xn] ==> Pm[x1..xn] 36 * where P1' through Pm-1' have any occurrences of x1 substituted as 37 * F[x2...xn], and Pk has been removed. 38 * 39 * The constraint can also occur within conjuncts of P1, P2 ... P(m-1). 40 * 41 * USES 42 * 43 * Eliminating trivial existential and universal quantifiers. 44 * 45 * EXAMPLES 46 * 47 * - UNWIND_EXISTS_CONV (--`?inp. inp /\ P inp`--); 48 * |- (?inp. inp /\ P inp) = P T : thm 49 * 50 * - UNWIND_EXISTS_CONV (--`?inp (f:'a->num). (inp = f x) /\ P f inp`--); 51 * |- (?inp f. (inp = f x) /\ P f inp) = (?f. P f (f x)) : thm 52 * 53 * - UNWIND_EXISTS_CONV (--`?inp. ~inp /\ P inp`--); 54 * |- (?inp. ~inp /\ P inp) = P F : thm 55 * 56 * UNWIND_FORALL_CONV (--`!x. (x = 3) ==> P x`--); 57 * UNWIND_FORALL_CONV (--`!x. (x = 3) /\ Q x ==> P x`--); 58 * UNWIND_FORALL_CONV (--`!x. (3 = x) /\ Q x ==> P x`--); 59 * UNWIND_FORALL_CONV (--`!x. (x < y) ==> (x = 3) /\ Q x ==> P x`--); 60 * UNWIND_FORALL_CONV (--`!Q R. (x = 3) /\ Q /\ P x ==> R Q`--); 61 * UNWIND_FORALL_CONV (--`!Q R. (x = 3) /\ ~Q /\ P x ==> R Q`--); 62 * 63 * TESTING CODE 64 * 65 *------------------------------------------------------------------------*) 66 67 68structure Unwind :> Unwind = 69struct 70 71open refuteLib HolKernel liteLib boolLib Trace AC Ho_Rewrite; 72 73infix THEN THENC ##; 74 75fun WRAP_ERR x = STRUCT_WRAP "Unwind" x; 76 77(*------------------------------------------------------------------- 78 * find_var_value 79 * 80 * Given a quantified variable $var$, and a list of possible restricting 81 * terms, we return 82 * a conjunct from the list of the form $(var = val)$ or $(val = var)$ 83 * or $var$ or $~var$. 84 * If there is no such conjunct, then the function simply fails. This 85 * whole function would be a whole lot easier in Prolog. 86 * 87 * It is the [[check_var]] function which actually does the work. It 88 * takes a variable and a conjunct and returns a value for that variable 89 * or fails. 90 * 91 *------------------------------------------------------------------------*) 92 93val false_tm = F 94val truth_tm = T 95 96fun check_var var conj = 97 if is_eq conj then let 98 val (arg1, arg2) = dest_eq conj in 99 if (mem arg1 (free_vars arg2) orelse 100 mem arg2 (free_vars arg1)) then 101 failwith "check_var - Duplicate values" else 102 if (arg1 = var) then arg2 else 103 if (arg2 = var) then arg1 104 else failwith "check_var - No value" end 105 else if is_neg conj andalso dest_neg conj = var then false_tm 106 else if var = conj then truth_tm 107 else failwith "check_var - No value"; 108 109fun find_var_value var = 110 let fun fvv [] = failwith "find_var_value - No value equality" 111 | fvv (c::cs) = (c, check_var var c) handle HOL_ERR _ => fvv cs; 112 in fvv 113 end 114 115(*------------------------------------------------------------------- 116 * MOVE_EXISTS_RIGHT_CONV : conv 117 * 118 * If we find that a quantified variable does have a value waiting for 119 * it, then we need to move it rightwards as far as possible in the 120 * string of existentially quantified variables. To do this, we develop 121 * [[MOVE_{EXISTS,FORALL}_RIGHT_CONV]] that perform just this action. 122 * 123 *------------------------------------------------------------------------*) 124 125fun MOVE_EXISTS_RIGHT_CONV tm = let 126 val (vs, body) = strip_exists tm 127in 128 case vs of 129 [] => failwith "MOVE_EXISTS_RIGHT_CONV" 130 | [_] => ALL_CONV tm 131 | (v::others) => let 132 val reordered_vars = others @ [v] 133 val asm = ASSUME body 134 fun one_direction old new = let 135 val thm = 136 foldr (fn (v, th) => EXISTS (mk_exists(v, concl th),v) th) asm new 137 fun foldthis (v, th) = let 138 val hyp_t = hd (hyp th) 139 in 140 CHOOSE (v, ASSUME (mk_exists(v, hyp_t))) th 141 end 142 in 143 DISCH_ALL (List.foldr foldthis thm old) 144 end 145 in 146 IMP_ANTISYM_RULE (one_direction vs reordered_vars) 147 (one_direction reordered_vars vs) 148 149 end 150end 151 152fun MOVE_FORALL_RIGHT_CONV tm = 153 if (is_forall tm) then 154 let val (curvar, subterm) = dest_forall tm in 155 if (is_forall subterm) then 156 (SWAP_VARS_CONV THENC BINDER_CONV MOVE_FORALL_RIGHT_CONV) tm 157 else REFL tm 158 end 159 else failwith "MOVE_FORALL_RIGHT_CONV"; 160 161 162 163(*------------------------------------------------------------------- 164 * Utils 165 *------------------------------------------------------------------------*) 166 167fun split_at f [] = raise failwith"split_at" 168 | split_at f (hd::tl) = 169 if (f hd) 170 then ([],hd,tl) 171 else let val (fr,el,back) = split_at f tl 172 in (hd::fr,el,back) 173 end; 174 175(*------------------------------------------------------------------- 176 * CONJ_TO_FRONT_CONV 177 * 178 * An conjunct nesting is of the form 179 * T1 /\ T2 180 * where each Ti is a conjunct nesting, or a single term T which 181 * is not a conjunct. 182 * 183 * CONJ_TO_FRONT_CONV takes a conjunct nesting and a special conjunct 184 * Txx, and converts the conjunct nesting to 185 * Txx /\ T1 /\ T2 /\ ... /\ Tn 186 * where T1 ... TN are the conjuncts in the conjunct nesting (apart 187 * from Txx). Thus the conjunct nesting is also flattened. 188 * 189 * The implementation of this function may eventually be changed to 190 * maintain the structure of the nestings T1, T2 etc. 191 * 192 * EXAMPLES 193 * profile CONJ_TO_FRONT_CONV (--`x = 3`--,--`(x = 3)`--); 194 * profile CONJ_TO_FRONT_CONV (--`x = 3`--,--`(x = 3) /\ P x`--); 195 * profile CONJ_TO_FRONT_CONV (--`x = 3`--,--`(x = 3) /\ P x /\ Q x`--); 196 * profile CONJ_TO_FRONT_CONV(--`(P:num->bool) x`--,--`(x = 3)/\P x /\ Q x`--); 197 * profile CONJ_TO_FRONT_CONV (--`(Q:num->bool) x`--,--`(x = 3)/\P x/\Q x`--); 198 *------------------------------------------------------------------------*) 199 200fun CONJ_TO_FRONT_CONV conj term = 201 let val conjs = strip_conj term 202 val (front,e,back) = split_at (term_eq conj) conjs 203 handle HOL_ERR _ => failwith "CONJ_TO_FRONT_CONV" 204 val rhs = list_mk_conj (e::(front @ back)) 205 in CONJ_ACI (mk_eq(term,rhs)) 206 end; 207 208(*------------------------------------------------------------------- 209 * IMP_TO_FRONT_CONV 210 * 211 * An antecedant nesting is of the form 212 * T1 ==> T2 ==> ... ==> C 213 * where each Ti is a conjunct nesting. 214 * 215 * IMP_TO_FRONT_CONV transforms an antecedant nesting into the form 216 * Txx ==> T1a ==> T1b ==> ... ==> T2a ==> ... ==> C 217 * where Txx is a special member of one of the conjunct nestings, 218 * and T1a..T1x are the members of conjunct nesting T1 (and so on 219 * for T2, T3 etc.), excluding Txx which is now at the front. 220 * 221 * The implementation of this function may eventually be changed to 222 * maintain the structure of nestings T1, T2 etc. 223 * 224 * NOTE 225 * The implementation of this routine uses tautLib. A more 226 * efficient implementation may be possible, but gross 227 * to code up!! Please supply one if you can work out 228 * the fiddly details of the proof strategy. 229 * 230 * EXAMPLES 231 * profile IMP_TO_FRONT_CONV (--`x = 3`--) (--`(x = 3) ==> P x`--); 232 * profile IMP_TO_FRONT_CONV (--`x = 3`--) (--`(x = 3) /\ Q x ==> P x`--); 233 * profile IMP_TO_FRONT_CONV (--`x = 3`--) (--`(Q x) ==> (x = 3) /\ Q x ==> P x`--); 234 * profile IMP_TO_FRONT_CONV(--`Q:bool`--)(--`(x = 3) /\ Q /\ P x ==> R Q`--); 235 * profile IMP_TO_FRONT_CONV (--`Q:bool`--)(--`(x = 3)/\P x/\Q ==> R Q`--); 236 * IMP_CONJ_CANON (mk_thm([],(--`P ==> Q ==> R`--))); 237 * IMP_CONJ_CANON (mk_thm([],(--`P /\ Q ==> R`--))); 238 * IMP_CONJ_CANON (mk_thm([],(--`P ==> (Q /\ R) ==> Q`--))); 239 240 *------------------------------------------------------------------------*) 241 242(* return a list of terms such that they would be 243 negated disjuncts in a strip_disj of the term, but allowing for the 244 possibility of implications as "encoded" forms of disjunctions. *) 245fun strip_univ_neg acc tm = 246 if is_conj tm then let 247 val (c1, c2) = dest_conj tm 248 in 249 strip_univ_neg (strip_univ_neg acc c2) c1 250 end else tm :: acc 251 252fun strip_univ_pos acc tm = 253 if is_disj tm then let 254 val (d1, d2) = dest_disj tm 255 in 256 strip_univ_pos (strip_univ_pos acc d2) d1 257 end 258 else if is_neg tm then strip_univ_neg acc (dest_neg tm) 259 else if is_imp tm then let 260 val (h,c) = dest_imp tm 261 in 262 strip_univ_neg (strip_univ_pos acc c) h 263 end 264 else acc 265 266val strip_univ = strip_univ_pos [] 267 268(* elim_term returns a term option option with the following semantics: 269 NONE indicates that the et term wasn't found within tm at all 270 SOME NONE indicates that the et term was exactly ~tm 271 SOME (SOME t) indicates that after removing et from tm, t was left 272 If elim_term returns SOME (SOME t) then et ==> t is equivalent to tm; 273 it eliminates et from a negative position with tm. 274 If elim_term returns SOME NONE then et ==> F is equivalent to tm. 275 276 If elim_term_neg returns SOME (SOME t) then et /\ t is equivalent to tm. 277 If elim_term_neg returns SOME NONE then et is equivalent to tm 278*) 279fun elim_term_neg et tm = 280 if is_conj tm then let 281 val (c1, c2) = dest_conj tm 282 in 283 case elim_term_neg et c1 of 284 NONE => let 285 in 286 case elim_term_neg et c2 of 287 NONE => NONE 288 | SOME NONE => SOME (SOME c1) 289 | SOME (SOME t) => SOME (SOME (mk_conj(c1, t))) 290 end 291 | SOME NONE => SOME (SOME c2) 292 | SOME (SOME t) => SOME (SOME (mk_conj(t, c2))) 293 end 294 else if term_eq et tm then 295 SOME NONE 296 else NONE 297 298fun elim_term et tm = 299 if is_imp tm (* want ~P to be considered an implication *) 300 then let val (h,c) = dest_imp tm 301 val (mk_imp, new_c) = 302 if is_neg tm then ((fn (t1, c) => mk_neg t1), NONE) 303 else (mk_imp, SOME c) 304 in case elim_term_neg et h 305 of NONE => let in 306 case elim_term et c 307 of NONE => NONE 308 | SOME NONE => SOME (SOME (mk_neg h)) 309 | SOME (SOME t) => SOME (SOME (mk_imp(h,t))) 310 end 311 | SOME NONE => SOME new_c 312 | SOME (SOME t) => SOME (SOME (mk_imp(t, c))) 313 end 314 else 315 if is_disj tm 316 then let val (d1, d2) = dest_disj tm 317 in case elim_term et d1 318 of NONE => let in 319 case elim_term et d2 320 of NONE => NONE 321 | SOME NONE => SOME (SOME d1) 322 | SOME (SOME t) => SOME (SOME (mk_disj(d1,t))) 323 end 324 | SOME NONE => SOME (SOME d2) 325 | SOME (SOME t) => SOME (SOME (mk_disj(t,d2))) 326 end 327 else NONE 328 329val CONJ_IMP_THM = GSYM AND_IMP_INTRO 330 331val NOT_CONJ_THM = 332 let val th = boolTheory.DE_MORGAN_THM 333 val (l,_) = strip_forall (concl th) 334 val th1 = CONJUNCT1 (SPEC_ALL th) 335 in GENL l th1 336 end; 337 338val NOT_IMP_THM = 339 let val A = Term.mk_var("A",bool) 340 in GEN A (RIGHT_BETA (AP_THM NOT_DEF A)) 341 end; 342 343(* turns top level of term into series of disjunctions *) 344fun disjunctify tm = 345 if is_disj tm then 346 Conv.BINOP_CONV disjunctify tm 347 else if is_neg tm then let 348 val h = dest_neg tm 349 in 350 if is_conj h then (REWR_CONV NOT_CONJ_THM THENC disjunctify) tm 351 else ALL_CONV tm 352 end 353 else if is_imp tm then let 354 val (h,c) = dest_imp tm 355 in 356 if is_conj h then (REWR_CONV CONJ_IMP_THM THENC disjunctify) tm 357 else (REWR_CONV IMP_DISJ_THM THENC RAND_CONV disjunctify) tm 358 end 359 else ALL_CONV tm 360 361 362fun IMP_TO_FRONT_CONV ante tm = 363 case elim_term ante tm of 364 SOME tt => let 365 val newtm = 366 case tt of 367 SOME t => mk_imp (ante, t) 368 | NONE => mk_neg ante 369 val dtm = QCONV disjunctify tm 370 val dnewtm = SYM (QCONV disjunctify newtm) 371 val eq3 = AC_CONV(DISJ_ASSOC, DISJ_COMM) 372 (mk_eq(rhs (concl dtm), lhs (concl dnewtm))) 373 val eq4 = TRANS dtm (TRANS (EQT_ELIM eq3) dnewtm) 374 in 375 if is_neg newtm 376 then TRANS eq4 (SPEC (dest_neg newtm) NOT_IMP_THM) 377 else eq4 378 end 379 | _ => failwith "IMP_TO_FRONT_CONV" 380 381(*------------------------------------------------------------------- 382 * ENSURE_CONJ_CONV 383 * Prove a term is equal to a term which is a conjunct 384 * by introduing T if necessary, as in 385 * P = P /\ T 386 *------------------------------------------------------------------------*) 387 388val TRUTH_CONJ_INTRO_THM = 389 let val P = Term.mk_var("P", bool) 390 in GEN P (SYM (el 2 (CONJUNCTS (SPEC P AND_CLAUSES)))) 391 end; 392 393fun ENSURE_CONJ_CONV tm = 394 if (is_conj tm) then REFL tm else SPEC tm TRUTH_CONJ_INTRO_THM; 395 396(*------------------------------------------------------------------- 397 * ENSURE_VAR_EQ_CONV 398 * Make a term into an equality with a particular 399 * variable on the left in the case it is 400 * of the form P (where P is not an equality) or ~P, otherwise 401 * leave it alone. 402 * <P> P -> P = T 403 * <P> ~P -> P = F 404 * <P> P = Q -> P = Q 405 * <P> Q = P -> P = Q 406 * ENSURE_EQ_CONV (--`P:bool`--) (--`P:bool`--); 407 * ENSURE_EQ_CONV (--`P:bool`--) (--`~P:bool`--); 408 * ENSURE_EQ_CONV (--`P:bool`--) (--`P = (Q:bool)`--); 409 * ENSURE_EQ_CONV (--`P:bool`--) (--`Q = (P:bool)`--); 410 *------------------------------------------------------------------------*) 411 412(*--------------------------------------------------------------------------- 413 !P. ~P = (P = F) 414 !P. P = (P = T) 415 ---------------------------------------------------------------------------*) 416 417val EQF_INTRO_THM = 418let val P = Term.mk_var("P", bool) 419 in GEN P (SYM (el 4 (CONJUNCTS (SPEC P EQ_CLAUSES)))) 420 end; 421 422val EQT_INTRO_THM = 423let val P = Term.mk_var("P", bool) 424 in GEN P (SYM (el 2 (CONJUNCTS (SPEC P EQ_CLAUSES)))) 425 end; 426 427fun ENSURE_EQ_CONV var tm = 428 if (is_eq tm) 429 then if (lhs tm = var) then REFL tm else SYM_CONV tm 430 else if is_neg tm 431 then SPEC (dest_neg tm) EQF_INTRO_THM 432 else SPEC tm EQT_INTRO_THM; 433 434(*------------------------------------------------------------------- 435 * ELIM_EXISTS_CONV : 436 * Eliminate an existential witnessed by an equality somewhere 437 * in the conjunct nesting immediately below the existential. 438 * 439 * EXAMPLES 440 * 441 * val inp = --`inp:bool`--; 442 * - profile (ELIM_EXISTS_CONV (inp,inp)) (--`?inp. inp /\ P inp`--); 443 * - profile (ELIM_EXISTS_CONV (inp, --`inp:bool = y`--)) 444 * (--`?inp. Q inp /\ (inp:bool = y) /\ P inp`--); 445 * - ELIM_EXISTS_CONV (inp,--`~inp`--) (--`?inp. Q inp /\ ~inp /\ P inp`--); 446 * 447 * IMPLEMENTATION: 448 * 1. Convert the body by: 449 * a. Moving the appropriate conjunct to the front of the conjunct 450 * nesting. 451 * b. Abstract the other conjuncts by the 452 * appropriate variable. 453 * c. Ensure the conjunct is an equality (P --> (P = T) etc.) with 454 * the variable to eliminate on the left. 455 * 2. Now apply ELIM_EXISTS_THM 456 *------------------------------------------------------------------------*) 457 458fun ELIM_EXISTS_CONV (var,conj) = 459 RAND_CONV (ABS_CONV 460 (CONJ_TO_FRONT_CONV conj THENC ENSURE_CONJ_CONV THENC 461 LAND_CONV (ENSURE_EQ_CONV var))) 462 THENC HO_REWR_CONV UNWIND_THM2; 463 464(*------------------------------------------------------------------- 465 * ELIM_FORALL_CONV : 466 * Eliminate an universal witnessed by an equality somewhere 467 * in the antecedant nesting immediately below the quantification. 468 * 469 * 470 * EXAMPLES 471 * 472 * val inp = --`inp:bool`--; 473 * - profile (ELIM_FORALL_CONV (inp,inp)) (--`!inp. inp ==> Q inp ==> P inp`--) handle e => Raise e; 474 * - profile (ELIM_FORALL_CONV (inp, --`inp:bool = y`--)) (--`!inp. Q inp ==> (inp:bool = y) ==> P inp`--); 475 * - profile (ELIM_FORALL_CONV (inp,--`~inp`--)) (--`!inp. Q inp /\ R inp ==> ~inp ==> P inp`--); 476 * 477 * IMPLEMENTATION: 478 * 1. Convert the body by: 479 * a. Moving the appropriate antecedent to the front of the 480 * antecedent nesting. 481 * b. Abstract the other antecedents and conclusion by the 482 * appropriate variable. 483 * c. Ensure the antecedent is an equality (P --> (P = T) etc.) with 484 * the variable to eliminate on the left. 485 * 2. Now apply ELIM_FORALL_THM 486 *------------------------------------------------------------------------*) 487 488fun ELIM_FORALL_CONV (var,conj) = 489 RAND_CONV (ABS_CONV 490 (IMP_TO_FRONT_CONV conj THENC LAND_CONV (ENSURE_EQ_CONV var))) 491 THENC HO_REWR_CONV UNWIND_FORALL_THM2; 492 493 494(*------------------------------------------------------------------- 495 * UNWIND_EXISTS_CONV 496 * 497 * Like ELIM_EXISTS_CONV but does variable reordering as well to 498 * work on the top quantifier in a sequence of existenial quantifications. 499 *------------------------------------------------------------------------*) 500 501fun UNWIND_EXISTS_CONV tm = 502 let val (vars, body) = strip_exists tm 503 in if length vars = 0 then failwith "UNWIND_EXISTS_CONV: not applicable" else 504 let val (conj,value) = find_var_value (hd vars) (strip_conj body) 505 handle HOL_ERR _ => failwith "UNWIND_EXISTS_CONV: can't eliminate" 506 in (MOVE_EXISTS_RIGHT_CONV 507 THENC LAST_EXISTS_CONV (ELIM_EXISTS_CONV (hd vars,conj))) tm 508 end 509 end; 510 511(*------------------------------------------------------------------------ 512 * UNWIND_EXISTS_TAC 513 * UNWIND_EXISTS_RULE 514 * 515 *------------------------------------------------------------------------*) 516 517val UNWIND_EXISTS_TAC = CONV_TAC (TOP_DEPTH_CONV UNWIND_EXISTS_CONV) 518val UNWIND_EXISTS_RULE = CONV_RULE UNWIND_EXISTS_CONV 519 520(*------------------------------------------------------------------- 521 * UNWIND_FORALL_CONV 522 * 523 * Like ELIM_FORALL_CONV but does variable reordering as well to 524 * work on any existential in a grouping of existentials. 525 * 526 *------------------------------------------------------------------------*) 527 528fun UNWIND_FORALL_CONV tm = 529 let val (vars, body) = strip_forall tm 530 in if length vars = 0 then failwith "UNWIND_FORALL_CONV: not applicable" else 531 let val (ant,value) = find_var_value (hd vars) (strip_univ body) 532 handle HOL_ERR _ => failwith "UNWIND_FORALL_CONV: no value to eliminate" 533 in (MOVE_FORALL_RIGHT_CONV 534 THENC LAST_FORALL_CONV (ELIM_FORALL_CONV (hd vars,ant))) tm 535 end 536 end; 537 538(*------------------------------------------------------------------------ 539 * UNWIND_FORALL_TAC 540 * UNWIND_FORALL_RULE 541 * 542 *------------------------------------------------------------------------*) 543 544val UNWIND_FORALL_TAC = CONV_TAC (TOP_DEPTH_CONV UNWIND_FORALL_CONV) 545val UNWIND_FORALL_RULE = CONV_RULE UNWIND_FORALL_CONV 546 547end (* struct *) 548