1(*===================================================================== *) 2(* FILE : ConseqConv.sml *) 3(* DESCRIPTION : Infrastructure for 'Consequence Conversions'. *) 4(* A ConseqConv is a conversion that turns a term *) 5(* t into a theorem of the form "t' ==> t" *) 6(* *) 7(* AUTHORS : Thomas Tuerk *) 8(* DATE : July 3, 2008 *) 9(* ===================================================================== *) 10 11 12structure ConseqConv :> ConseqConv = 13struct 14 15(* 16quietdec := true; 17*) 18 19open HolKernel Parse boolLib Drule ConseqConvTheory; 20 21(* 22quietdec := false; 23*) 24 25 26 27(*--------------------------------------------------------------------------- 28 * generalise a variable in an implication 29 * 30 * A |- t1 v ==> t2 v 31 * --------------------------------------------- 32 * A |- (!v. t1 v) ==> (!v. t2 v) 33 * 34 *---------------------------------------------------------------------------*) 35 36fun GEN_IMP v thm = 37 let 38 val thm1 = GEN v thm; 39 val thm2 = HO_MATCH_MP MONO_ALL thm1; 40 in 41 thm2 42 end; 43 44fun LIST_GEN_IMP vL thm = 45 foldr (uncurry GEN_IMP) thm vL 46 47 48 49(*--------------------------------------------------------------------------- 50 * generalise a variable in an equation 51 * 52 * A |- t1 v = t2 v 53 * --------------------------------------------- 54 * A |- (!v. t1 v) = (!v. t2 v) 55 * 56 *---------------------------------------------------------------------------*) 57 58fun GEN_EQ v thm = 59 QUANT_CONV (K thm) (mk_forall (v, lhs (concl thm))) 60 61fun LIST_GEN_EQ vL thm = 62 foldr (uncurry GEN_EQ) thm vL 63 64(*--------------------------------------------------------------------------- 65 * Introduces EXISTS on both sides of an implication 66 * 67 * A |- t1 v ==> t2 v 68 * --------------------------------------------- 69 * A |- (?v. t1 v) ==> (?v. t2 v) 70 * 71 *---------------------------------------------------------------------------*) 72fun EXISTS_INTRO_IMP v thm = 73 let 74 val thm1 = GEN v thm; 75 val thm2 = HO_MATCH_MP boolTheory.MONO_EXISTS thm1; 76 in 77 thm2 78 end; 79 80fun LIST_EXISTS_INTRO_IMP vL thm = 81 foldr (uncurry EXISTS_INTRO_IMP) thm vL 82 83 84(*--------------------------------------------------------------------------- 85 * REFL for implications 86 * 87 * REFL_CONSEQ_CONV t = (t ==> t) 88 *---------------------------------------------------------------------------*) 89fun REFL_CONSEQ_CONV t = DISCH t (ASSUME t); 90 91 92(*--------------------------------------------------------------------------- 93 * generalises a thm body and as well the ASSUMPTIONS 94 * 95 * A |- body 96 * --------------------------------------------- 97 * (!v. A) |- !v. body 98 * 99 *---------------------------------------------------------------------------*) 100 101fun GEN_ASSUM v thm = 102 let 103 val assums = filter (free_in v) (hyp thm); 104 val thm2 = foldl (fn (t,thm) => DISCH t thm) thm assums; 105 val thm3 = GEN v thm2; 106 val thm4 = foldl (fn (_,thm) => UNDISCH (HO_MATCH_MP MONO_ALL thm)) 107 thm3 assums; 108 in 109 thm4 110 end 111 112 113 114 115(*Introduces allquantification for all free variables*) 116val SPEC_ALL_TAC:tactic = fn (asm,t) => 117let 118 val asm_vars = FVL asm empty_tmset; 119 val t_vars = FVL [t] empty_tmset; 120 val free_vars = HOLset.difference (t_vars,asm_vars); 121 122 val free_varsL = HOLset.listItems free_vars; 123in 124 ([(asm,list_mk_forall (free_varsL,t))], 125 fn thmL => (SPECL free_varsL (hd thmL))) 126end; 127 128 129 130(*--------------------------------------------------------------------------- 131 - Main types 132 ----------------------------------------------------------------------------*) 133 134datatype CONSEQ_CONV_direction = 135 CONSEQ_CONV_STRENGTHEN_direction 136 | CONSEQ_CONV_WEAKEN_direction 137 | CONSEQ_CONV_UNKNOWN_direction; 138 139datatype CONSEQ_CONV_context = 140 CONSEQ_CONV_NO_CONTEXT 141 | CONSEQ_CONV_IMP_CONTEXT 142 | CONSEQ_CONV_FULL_CONTEXT; 143 144type conseq_conv = term -> thm; 145type directed_conseq_conv = CONSEQ_CONV_direction -> conseq_conv; 146 147 148(*--------------------------------------------------------------------------- 149 - Test cases 150 ---------------------------------------------------------------------------- 151 152val t = ``x > 5``; 153val thm1 = prove (``x > 6 ==> x > 5``, DECIDE_TAC); 154val thm2 = prove (``x > 5 ==> x > 4``, DECIDE_TAC); 155val thm3 = prove (``(x > 5) = (x >= 6)``, DECIDE_TAC); 156val thm4 = prove (``(x > 5) = (x > 5)``, DECIDE_TAC); 157 158 159 160CONSEQ_CONV_WRAPPER___CONVERT_RESULT CONSEQ_CONV_STRENGTHEN_direction thm1 t 161CONSEQ_CONV_WRAPPER___CONVERT_RESULT CONSEQ_CONV_WEAKEN_direction thm1 t 162CONSEQ_CONV_WRAPPER___CONVERT_RESULT CONSEQ_CONV_UNKNOWN_direction thm1 t 163 164CONSEQ_CONV_WRAPPER___CONVERT_RESULT CONSEQ_CONV_STRENGTHEN_direction thm2 t 165CONSEQ_CONV_WRAPPER___CONVERT_RESULT CONSEQ_CONV_WEAKEN_direction thm2 t 166CONSEQ_CONV_WRAPPER___CONVERT_RESULT CONSEQ_CONV_UNKNOWN_direction thm2 t 167 168CONSEQ_CONV_WRAPPER___CONVERT_RESULT CONSEQ_CONV_STRENGTHEN_direction thm3 t 169CONSEQ_CONV_WRAPPER___CONVERT_RESULT CONSEQ_CONV_WEAKEN_direction thm3 t 170CONSEQ_CONV_WRAPPER___CONVERT_RESULT CONSEQ_CONV_UNKNOWN_direction thm3 t 171 172CONSEQ_CONV_WRAPPER___CONVERT_RESULT CONSEQ_CONV_STRENGTHEN_direction thm4 t 173CONSEQ_CONV_WRAPPER___CONVERT_RESULT CONSEQ_CONV_WEAKEN_direction thm4 t 174CONSEQ_CONV_WRAPPER___CONVERT_RESULT CONSEQ_CONV_UNKNOWN_direction thm4 t 175 176 177 ----------------------------------------------------------------------------*) 178 179fun CONSEQ_CONV_WRAPPER___CONVERT_RESULT dir thm t = 180let 181 val thm_term = concl thm; 182in 183 if (aconv thm_term t) then 184 CONSEQ_CONV_WRAPPER___CONVERT_RESULT dir (EQT_INTRO thm) t 185 else if (is_imp_only thm_term) then 186 let 187 val (t1, t2) = dest_imp thm_term; 188 val _ = if (aconv t1 t2) then raise UNCHANGED else (); 189 190 val g' = if (aconv t2 t) then CONSEQ_CONV_STRENGTHEN_direction else 191 if (aconv t1 t) then CONSEQ_CONV_WEAKEN_direction else 192 raise UNCHANGED; 193 val g'' = if (dir = CONSEQ_CONV_UNKNOWN_direction) then g' else dir; 194 val _ = if not (g' = g'') then raise UNCHANGED else (); 195 in 196 (g'', thm) 197 end 198 else if (is_eq thm_term) then 199 (dir, 200 if aconv (lhs thm_term) t andalso not (aconv (rhs thm_term) t) then 201 if (dir = CONSEQ_CONV_UNKNOWN_direction) then 202 thm 203 else if (dir = CONSEQ_CONV_STRENGTHEN_direction) then 204 snd (EQ_IMP_RULE thm) 205 else 206 fst (EQ_IMP_RULE thm) 207 else raise UNCHANGED) 208 else 209 raise UNCHANGED 210end; 211 212 213fun CONSEQ_CONV_WRAPPER conv dir t = 214let 215 val _ = if (type_of t = bool) then () else raise UNCHANGED; 216 val thm = conv dir t; 217in 218 snd (CONSEQ_CONV_WRAPPER___CONVERT_RESULT dir thm t) 219end; 220 221 222fun CHANGED_CHECK_CONSEQ_CONV conv t = 223 let 224 val thm = conv t; 225 val (t1,t2) = dest_imp (concl thm) handle HOL_ERR _ => 226 dest_eq (concl thm); 227 val _ = if (aconv t1 t2) then raise UNCHANGED else (); 228 in 229 thm 230 end; 231 232 233(*like CHANGED_CONV*) 234fun QCHANGED_CONSEQ_CONV conv t = 235 conv t handle UNCHANGED => raise mk_HOL_ERR "bool" "ConseqConv" "QCHANGED_CONSEQ_CONV" 236 237fun CHANGED_CONSEQ_CONV conv = 238 QCHANGED_CONSEQ_CONV (CHANGED_CHECK_CONSEQ_CONV conv) 239 240 241(*like ORELSEC*) 242fun ORELSE_CONSEQ_CONV (c1:conv) c2 t = 243 ((c1 t handle HOL_ERR _ => raise UNCHANGED) handle UNCHANGED => 244 (c2 t handle HOL_ERR _ => raise UNCHANGED)); 245 246 247(*like FIRST_CONV*) 248fun FIRST_CONSEQ_CONV [] t = raise UNCHANGED 249 | FIRST_CONSEQ_CONV ((c1:conv)::L) t = 250 ORELSE_CONSEQ_CONV c1 (FIRST_CONSEQ_CONV L) t; 251 252 253 254 255fun CONSEQ_CONV___GET_SIMPLIFIED_TERM thm t = 256 if aconv (concl thm) t then T else 257 let 258 val (t1,t2) = dest_imp (concl thm) handle HOL_ERR _ => 259 dest_eq (concl thm); 260 in 261 if (aconv t1 t) then t2 else t1 262 end; 263 264 265fun CONSEQ_CONV___OPT_GET_SIMPLIFIED_TERM NONE dir t = t 266 | CONSEQ_CONV___OPT_GET_SIMPLIFIED_TERM (SOME thm) dir t = 267 if dir = CONSEQ_CONV_STRENGTHEN_direction then 268 (fst (dest_imp (concl thm))) 269 else 270 (snd (dest_imp (concl thm))); 271 272 273fun CONSEQ_CONV___GET_DIRECTION thm t = 274 if aconv (concl thm) t then CONSEQ_CONV_UNKNOWN_direction else 275 if (is_eq (concl thm)) then CONSEQ_CONV_UNKNOWN_direction else 276 let 277 val (t1,t2) = dest_imp (concl thm); 278 in 279 if (aconv t1 t) andalso (aconv t2 t) then 280 CONSEQ_CONV_UNKNOWN_direction else 281 if (aconv t2 t) then CONSEQ_CONV_STRENGTHEN_direction else 282 if (aconv t1 t) then CONSEQ_CONV_WEAKEN_direction else 283 raise UNCHANGED 284 end; 285 286 287 288(*--------------------------------------------------------------------------- 289 - Test cases 290 ---------------------------------------------------------------------------- 291 292val t1 = ``x > 5``; 293val t2 = ``x > 3``; 294val t3 = ``x > 4``; 295 296val thm1 = prove (``x > 5 ==> x > 4``, DECIDE_TAC); 297val thm2 = prove (``x > 4 ==> x > 3``, DECIDE_TAC); 298 299val thm3 = prove (``(x > 4) = (x >= 5)``, DECIDE_TAC); 300val thm4 = prove (``(x >= 5) = (5 <= x)``, DECIDE_TAC); 301 302 303val thm1 = prove (``X ==> T``, REWRITE_TAC[]); 304val thm2 = prove (``T ==> T``, REWRITE_TAC[]); 305val t1 = ``X:bool`` 306 307val thm1 = prove (``(?r:'b. P (z:'a)) <=> P z``, PROVE_TAC[]); 308val thm2 = prove (``P (z:'a) ==> P z``, PROVE_TAC[]); 309val t = ``(?r:'b. P (z:'a))`` 310 311THEN_CONSEQ_CONV___combine thm1 thm2 t 312 313 314 315THEN_CONSEQ_CONV___combine thm1 thm2 t1 316THEN_CONSEQ_CONV___combine thm2 thm1 t2 317 318THEN_CONSEQ_CONV___combine thm1 thm3 t1 319THEN_CONSEQ_CONV___combine thm3 thm4 t3 320 321 ----------------------------------------------------------------------------*) 322 323fun is_refl_imp t = 324let 325 val (l1,l2) = dest_imp_only t; 326in 327 aconv l1 l2 328end handle HOL_ERR _ => false; 329 330fun is_refl_eq t = 331let 332 val (l1,l2) = dest_eq t; 333in 334 aconv l1 l2 335end handle HOL_ERR _ => false; 336 337fun is_refl_imp_eq t = is_refl_imp t orelse is_refl_eq t; 338 339 340fun THEN_CONSEQ_CONV___combine thm1 thm2 t = 341 if (is_refl_imp_eq (concl thm1)) then thm2 342 else if (is_refl_imp_eq (concl thm2)) then thm1 343 else if aconv (concl thm1) t then 344 THEN_CONSEQ_CONV___combine (EQT_INTRO thm1) thm2 t 345 else if (is_eq (concl thm1)) andalso aconv (rhs (concl thm1)) (concl thm2) 346 then 347 THEN_CONSEQ_CONV___combine thm1 (EQT_INTRO thm2) t 348 else if (is_eq (concl thm1)) andalso (is_eq (concl thm2)) then 349 TRANS thm1 thm2 350 else 351 let 352 val d1 = CONSEQ_CONV___GET_DIRECTION thm1 t; 353 val t2 = CONSEQ_CONV___GET_SIMPLIFIED_TERM thm1 t; 354 val d2 = if not (d1 = CONSEQ_CONV_UNKNOWN_direction) then d1 else 355 CONSEQ_CONV___GET_DIRECTION thm2 t2; 356 357 val thm1_imp = snd (CONSEQ_CONV_WRAPPER___CONVERT_RESULT d2 thm1 t) 358 handle UNCHANGED => REFL_CONSEQ_CONV t; 359 val thm2_imp = snd (CONSEQ_CONV_WRAPPER___CONVERT_RESULT d2 thm2 t2) 360 handle UNCHANGED => REFL_CONSEQ_CONV t2; 361 in 362 if (d2 = CONSEQ_CONV_STRENGTHEN_direction) then 363 IMP_TRANS thm2_imp thm1_imp 364 else 365 IMP_TRANS thm1_imp thm2_imp 366 end 367 368 369 370(*like THENC*) 371fun THEN_CONSEQ_CONV (c1:conv) c2 t = 372 let 373 val thm0_opt = SOME (c1 t) handle HOL_ERR _ => NONE 374 | UNCHANGED => NONE 375 376 val t2 = if (isSome thm0_opt) then CONSEQ_CONV___GET_SIMPLIFIED_TERM (valOf thm0_opt) t else t; 377 378 val thm1_opt = SOME (c2 t2) handle HOL_ERR _ => NONE 379 | UNCHANGED => NONE 380 in 381 if (isSome thm0_opt) andalso (isSome thm1_opt) then 382 THEN_CONSEQ_CONV___combine (valOf thm0_opt) (valOf thm1_opt) t else 383 if (isSome thm0_opt) then valOf thm0_opt else 384 if (isSome thm1_opt) then valOf thm1_opt else 385 raise UNCHANGED 386 end; 387 388 389fun EVERY_CONSEQ_CONV [] t = raise UNCHANGED 390 | EVERY_CONSEQ_CONV ((c1:conv)::L) t = 391 THEN_CONSEQ_CONV c1 (EVERY_CONSEQ_CONV L) t; 392 393 394 395 396fun CONSEQ_CONV___APPLY_CONV_RULE thm t conv = 397let 398 val r = CONSEQ_CONV___GET_SIMPLIFIED_TERM thm t; 399 val r_thm = conv r; 400in 401 THEN_CONSEQ_CONV___combine thm r_thm t 402end; 403 404 405 406 407 408val FORALL_EQ___CONSEQ_CONV = HO_PART_MATCH (snd o dest_imp) forall_eq_thm; 409val EXISTS_EQ___CONSEQ_CONV = HO_PART_MATCH (snd o dest_imp) exists_eq_thm; 410 411 412 413 (*Like QUANT_CONV for CONSEQ_CONVS. Explicit versions 414 for FORALL and EXISTS are exported, since they have 415 to be handeled separately anyhow.*) 416 417fun FORALL_CONSEQ_CONV conv t = 418 let 419 val (var, body) = dest_forall t; 420 val thm_body = conv body; 421 val thm = GEN var thm_body; 422 val thm2 = if (is_eq (concl thm_body)) then 423 forall_eq_thm 424 else boolTheory.MONO_ALL; 425 val thm3 = HO_MATCH_MP thm2 thm; 426 in 427 thm3 428 end; 429 430fun EXISTS_CONSEQ_CONV conv t = 431 let 432 val (var, body) = dest_exists t; 433 val thm_body = conv body; 434 val thm = GEN var thm_body; 435 val thm2 = if (is_eq (concl thm_body)) then 436 exists_eq_thm 437 else boolTheory.MONO_EXISTS; 438 val thm3 = HO_MATCH_MP thm2 thm; 439 in 440 thm3 441 end; 442 443fun QUANT_CONSEQ_CONV conv t = 444 if (is_forall t) then 445 FORALL_CONSEQ_CONV conv t 446 else if (is_exists t) then 447 EXISTS_CONSEQ_CONV conv t 448 else 449 NO_CONV t; 450 451 452fun TRUE_CONSEQ_CONV t = SPEC t true_imp; 453fun FALSE_CONSEQ_CONV t = SPEC t false_imp; 454 455fun TRUE_FALSE_REFL_CONSEQ_CONV CONSEQ_CONV_STRENGTHEN_direction = FALSE_CONSEQ_CONV 456 | TRUE_FALSE_REFL_CONSEQ_CONV CONSEQ_CONV_WEAKEN_direction = TRUE_CONSEQ_CONV 457 | TRUE_FALSE_REFL_CONSEQ_CONV CONSEQ_CONV_UNKNOWN_direction = REFL 458 459 460 461(*Like DEPTH_CONV for CONSEQ_CONVS. The conversion 462 may generate theorems containing assumptions. These 463 assumptions are propagated to the top level*) 464 465 466fun CONSEQ_CONV_DIRECTION_NEGATE CONSEQ_CONV_UNKNOWN_direction = CONSEQ_CONV_UNKNOWN_direction 467 | CONSEQ_CONV_DIRECTION_NEGATE CONSEQ_CONV_STRENGTHEN_direction = CONSEQ_CONV_WEAKEN_direction 468 | CONSEQ_CONV_DIRECTION_NEGATE CONSEQ_CONV_WEAKEN_direction = CONSEQ_CONV_STRENGTHEN_direction; 469 470 471 472(******************************************************************************) 473(* asm_marker *) 474(******************************************************************************) 475 476val asm_marker_tm = Term `ASM_MARKER` 477fun dest_asm_marker tt = 478let 479 val (oper, aL) = strip_comb tt 480 val _ = if (same_const oper asm_marker_tm) andalso 481 (length aL = 2) then () else Feedback.fail() 482in 483 (el 1 aL, el 2 aL) 484end 485fun mk_asm_marker l t = list_mk_comb(asm_marker_tm, [l,t]) 486fun mk_asm_marker_random_pair t = 487 let val v = genvar bool in (v, mk_asm_marker v t) end 488fun mk_asm_marker_random t = snd (mk_asm_marker_random_pair t) 489 490val is_asm_marker = can dest_asm_marker 491fun dest_neg_asm_marker tt = dest_asm_marker (dest_neg tt) 492val is_neg_asm_marker = can dest_neg_asm_marker 493 494fun asm_marker_ELIM_CONV tt = 495 let 496 val (l, tt) = (dest_asm_marker tt) 497 in 498 SPECL [l,tt] ASM_MARKER_THM 499 end; 500 501fun asm_marker_INTRO_CONV l tt = 502 SPECL [l, tt] (GSYM ASM_MARKER_THM) 503 504 505(******************************************************************************) 506(* DEPTH conv stuff *) 507(******************************************************************************) 508 509(* ------------------------------------- 510 Congruences 511 -------------------------------------*) 512type conseq_conv_congruence_syscall = 513 term list -> thm list -> int -> CONSEQ_CONV_direction -> term -> (int * thm option) 514 515type conseq_conv_congruence = 516 thm list -> conseq_conv_congruence_syscall -> 517 CONSEQ_CONV_direction -> term -> (int * thm) 518 519 520fun conseq_conv_congruence_EXPAND_THM_OPT (thm_opt,t,ass_opt) = 521 let 522 val thm = if isSome thm_opt then valOf thm_opt else REFL_CONSEQ_CONV t; 523 val thm' = if isSome ass_opt then DISCH (valOf ass_opt) thm else thm 524 in 525 thm' 526 end; 527 528fun dir_conv dir = 529 if (dir = CONSEQ_CONV_STRENGTHEN_direction) then 530 (RATOR_CONV o RAND_CONV) else RAND_CONV; 531 532fun check_sys_call sys new_context old_context n dir t = 533 let 534 val (n, thm_opt) = sys new_context old_context n dir t; 535 val _ = if (isSome thm_opt) then () else raise UNCHANGED; 536 in 537 (n, valOf thm_opt) 538 end; 539 540exception CONSEQ_CONV_congruence_exn; 541 542fun CONSEQ_CONV_CONGRUENCE___asm_marker context (sys:conseq_conv_congruence_syscall) dir t = 543 let 544 val (l,b1) = dest_asm_marker t; 545 val (n1, thm1) = check_sys_call sys [] context 0 dir b1; 546 val thm2 = CONV_RULE (BINOP_CONV (asm_marker_INTRO_CONV l)) thm1 547 in 548 (n1, thm2) 549 end handle HOL_ERR _ => raise CONSEQ_CONV_congruence_exn 550 551 552fun trivial_neg_simp t = 553let 554 val t1 = dest_neg t 555in 556 if (same_const t1 T) then 557 NOT_CLAUSES_T 558 else if (same_const t1 F) then 559 NOT_CLAUSES_F 560 else 561 ((K (SPEC (dest_neg t1) NOT_CLAUSES_X)) THENC 562 (TRY_CONV trivial_neg_simp)) F 563end 564 565 566fun CONSEQ_CONV_CONGRUENCE___neg context (sys:conseq_conv_congruence_syscall) dir t = 567 let 568 val b1 = dest_neg t; 569 val (n1, thm1) = check_sys_call sys [] context 0 (CONSEQ_CONV_DIRECTION_NEGATE dir) b1; 570 571 val thm2 = MATCH_MP MONO_NOT thm1 572 val thm3 = CONV_RULE (dir_conv dir trivial_neg_simp) thm2 handle HOL_ERR _ => thm2 573 in 574 (n1, thm3) 575 end handle HOL_ERR _ => raise CONSEQ_CONV_congruence_exn 576 577 578 579fun trivial_conj_simp t = 580let 581 val (t1, t2) = dest_conj t 582in 583 if (same_const t1 T) then 584 SPEC t2 AND_CLAUSES_TX 585 else if (same_const t2 T) then 586 SPEC t1 AND_CLAUSES_XT 587 else if (same_const t1 F) then 588 SPEC t2 AND_CLAUSES_FX 589 else if (same_const t2 F) then 590 SPEC t1 AND_CLAUSES_XF 591 else if (aconv t1 t2) then 592 SPEC t1 AND_CLAUSES_XX 593 else Feedback.fail() 594end 595 596 597fun CONSEQ_CONV_CONGRUENCE___conj context sys dir t = 598 let 599 val (b1,b2) = dest_conj t; 600 601 val (n1, thm1_opt) = sys [b2] context 0 dir b1; 602 val a2 = CONSEQ_CONV___OPT_GET_SIMPLIFIED_TERM thm1_opt dir b1; 603 val (n2, thm2_opt) = sys [a2] context n1 dir b2; 604 605 val _ = if (isSome thm1_opt) orelse (isSome thm2_opt) then () else raise UNCHANGED; 606 val thm1 = conseq_conv_congruence_EXPAND_THM_OPT (thm1_opt, b1, SOME b2); 607 val thm2 = conseq_conv_congruence_EXPAND_THM_OPT (thm2_opt, b2, SOME a2); 608 609 val cong_thm = if (dir = CONSEQ_CONV_STRENGTHEN_direction) then 610 IMP_CONG_conj_strengthen else IMP_CONG_conj_weaken 611 612 val thm3 = MATCH_MP cong_thm (CONJ thm1 thm2) 613 val thm4 = CONV_RULE (dir_conv dir trivial_conj_simp) thm3 handle HOL_ERR _ => thm3 614 in 615 (n2, thm4) 616 end handle HOL_ERR _ => raise CONSEQ_CONV_congruence_exn 617 618 619 620 621fun CONSEQ_CONV_CONGRUENCE___conj_no_context context sys dir t = 622 let 623 val (b1,b2) = dest_conj t; 624 625 val (n1, thm1_opt) = sys [] context 0 dir b1; 626 val a2 = CONSEQ_CONV___OPT_GET_SIMPLIFIED_TERM thm1_opt dir b1; 627 val abort_cond = same_const a2 F; 628 val (n2, thm2_opt) = if abort_cond then (n1, NONE) else sys [] context n1 dir b2; 629 val _ = if (isSome thm1_opt) orelse (isSome thm2_opt) orelse abort_cond then () else raise UNCHANGED; 630 631 val thm1 = conseq_conv_congruence_EXPAND_THM_OPT (thm1_opt, b1, NONE); 632 val thm2 = conseq_conv_congruence_EXPAND_THM_OPT (thm2_opt, b2, NONE); 633 634 val thm3 = MATCH_MP boolTheory.MONO_AND (CONJ thm1 thm2) 635 val thm4 = CONV_RULE (dir_conv dir trivial_conj_simp) thm3 handle HOL_ERR _ => thm3 636 in 637 (n2, thm4) 638 end handle HOL_ERR _ => raise CONSEQ_CONV_congruence_exn 639 640 641 642fun trivial_disj_simp t = 643let 644 val (t1, t2) = dest_disj t 645in 646 if (same_const t1 T) then 647 SPEC t2 OR_CLAUSES_TX 648 else if (same_const t2 T) then 649 SPEC t1 OR_CLAUSES_XT 650 else if (same_const t1 F) then 651 SPEC t2 OR_CLAUSES_FX 652 else if (same_const t2 F) then 653 SPEC t1 OR_CLAUSES_XF 654 else if (aconv t1 t2) then 655 SPEC t1 OR_CLAUSES_XX 656 else Feedback.fail() 657end 658 659 660fun CONSEQ_CONV_CONGRUENCE___disj context (sys:conseq_conv_congruence_syscall) dir t = 661 let 662 val (b1,b2) = dest_disj t; 663 664 val a1 = mk_neg b2; 665 val (n1, thm1_opt) = sys [a1] context 0 dir b1; 666 val a2 = mk_neg (CONSEQ_CONV___OPT_GET_SIMPLIFIED_TERM thm1_opt dir b1); 667 val (n2, thm2_opt) = sys [a2] context n1 dir b2; 668 669 val _ = if (isSome thm1_opt) orelse (isSome thm2_opt) then () else raise UNCHANGED; 670 671 val thm1 = conseq_conv_congruence_EXPAND_THM_OPT (thm1_opt, b1, SOME a1); 672 val thm2 = conseq_conv_congruence_EXPAND_THM_OPT (thm2_opt, b2, SOME a2); 673 674 val cong_thm = 675 if (dir = CONSEQ_CONV_STRENGTHEN_direction) then 676 IMP_CONG_disj_strengthen else IMP_CONG_disj_weaken 677 val thm3 = MATCH_MP cong_thm (CONJ thm1 thm2) 678 val thm4 = CONV_RULE (dir_conv dir trivial_disj_simp) thm3 handle HOL_ERR _ => thm3 679 in 680 (n2, thm4) 681 end handle HOL_ERR _ => raise CONSEQ_CONV_congruence_exn 682 683 684fun CONSEQ_CONV_CONGRUENCE___disj_no_context context (sys:conseq_conv_congruence_syscall) dir t = 685 let 686 val (b1,b2) = dest_disj t; 687 688 val (n1, thm1_opt) = sys [] context 0 dir b1; 689 val a2 = CONSEQ_CONV___OPT_GET_SIMPLIFIED_TERM thm1_opt dir b1; 690 val abort_cond = same_const a2 T; 691 val (n2, thm2_opt) = if abort_cond then (n1, NONE) else sys [] context n1 dir b2; 692 693 val _ = if (isSome thm1_opt) orelse (isSome thm2_opt) then () else raise UNCHANGED; 694 val thm1 = conseq_conv_congruence_EXPAND_THM_OPT (thm1_opt, b1, NONE); 695 val thm2 = conseq_conv_congruence_EXPAND_THM_OPT (thm2_opt, b2, NONE); 696 697 val thm3 = MATCH_MP MONO_OR (CONJ thm1 thm2) 698 val thm4 = CONV_RULE (dir_conv dir trivial_disj_simp) thm3 handle HOL_ERR _ => thm3 699 in 700 (n2, thm4) 701 end handle HOL_ERR _ => raise CONSEQ_CONV_congruence_exn 702 703 704fun trivial_imp_simp t = 705let 706 val (t1, t2) = dest_imp_only t 707in 708 if (same_const t1 T) then 709 SPEC t2 IMP_CLAUSES_TX 710 else if (same_const t2 T) then 711 SPEC t1 IMP_CLAUSES_XT 712 else if (same_const t1 F) then 713 SPEC t2 IMP_CLAUSES_FX 714 else if (same_const t2 F) then 715 CONV_RULE (RHS_CONV trivial_neg_simp) 716 (SPEC t1 IMP_CLAUSES_XF) 717 else if (aconv t1 t2) then 718 SPEC t1 IMP_CLAUSES_XX 719 else Feedback.fail() 720 721end 722 723 724fun CONSEQ_CONV_CONGRUENCE___imp_full_context context (sys:conseq_conv_congruence_syscall) dir t = 725 let 726 val (b1,b2) = dest_imp_only t; 727 728 val a1 = b1; 729 val (n1, thm1_opt) = sys [a1] context 0 dir b2; 730 val a2 = mk_neg (CONSEQ_CONV___OPT_GET_SIMPLIFIED_TERM thm1_opt dir b1); 731 val (n2, thm2_opt) = sys [a2] context n1 (CONSEQ_CONV_DIRECTION_NEGATE dir) b1; 732 733 val _ = if (isSome thm1_opt) orelse (isSome thm2_opt) then () else raise UNCHANGED; 734 val thm1 = conseq_conv_congruence_EXPAND_THM_OPT (thm1_opt, b2, SOME a1); 735 val thm2 = conseq_conv_congruence_EXPAND_THM_OPT (thm2_opt, b1, SOME a2); 736 737 val cong_thm = 738 if (dir = CONSEQ_CONV_STRENGTHEN_direction) then 739 IMP_CONG_imp_strengthen else IMP_CONG_imp_weaken 740 val thm3 = MATCH_MP cong_thm (CONJ thm1 thm2) 741 val thm4 = CONV_RULE (dir_conv dir trivial_imp_simp) thm3 handle HOL_ERR _ => thm3 742 in 743 (n2, thm4) 744 end handle HOL_ERR _ => raise CONSEQ_CONV_congruence_exn; 745 746 747 748fun CONSEQ_CONV_CONGRUENCE___imp_no_context context (sys:conseq_conv_congruence_syscall) dir t = 749 let 750 val (b1,b2) = dest_imp_only t; 751 752 val (n1, thm1_opt) = sys [] context 0 dir b2; 753 val a2 = CONSEQ_CONV___OPT_GET_SIMPLIFIED_TERM thm1_opt dir b2; 754 val abort_cond = same_const a2 T; 755 val (n2, thm2_opt) = if abort_cond then (n1, NONE) else sys [] context n1 (CONSEQ_CONV_DIRECTION_NEGATE dir) b1; 756 757 val _ = if (isSome thm1_opt) orelse (isSome thm2_opt) orelse abort_cond then () else raise UNCHANGED; 758 val thm1 = conseq_conv_congruence_EXPAND_THM_OPT (thm1_opt, b2, NONE); 759 val thm2 = conseq_conv_congruence_EXPAND_THM_OPT (thm2_opt, b1, NONE); 760 761 val thm3 = MATCH_MP MONO_IMP (CONJ thm2 thm1) 762 val thm4 = CONV_RULE (dir_conv dir trivial_imp_simp) thm3 handle HOL_ERR _ => thm3 763 in 764 (n2, thm4) 765 end handle HOL_ERR _ => raise CONSEQ_CONV_congruence_exn; 766 767 768fun CONSEQ_CONV_CONGRUENCE___imp_simple_context context (sys:conseq_conv_congruence_syscall) dir t = 769 let 770 val (b1,b2) = dest_imp_only t; 771 772 val (n1, thm1_opt) = sys [] context 0 (CONSEQ_CONV_DIRECTION_NEGATE dir) b1; 773 val a2 = CONSEQ_CONV___OPT_GET_SIMPLIFIED_TERM thm1_opt (CONSEQ_CONV_DIRECTION_NEGATE dir) b1; 774 val abort_cond = same_const a2 F; 775 val (n2, thm2_opt) = if abort_cond then (n1, NONE) else 776 sys [a2] context n1 dir b2; 777 val _ = if (isSome thm1_opt) orelse (isSome thm2_opt) orelse abort_cond then () else raise UNCHANGED; 778 val thm1 = conseq_conv_congruence_EXPAND_THM_OPT (thm1_opt, b1, NONE); 779 val thm2 = conseq_conv_congruence_EXPAND_THM_OPT (thm2_opt, b2, SOME a2); 780 781 val cong_thm = 782 if (dir = CONSEQ_CONV_STRENGTHEN_direction) then 783 IMP_CONG_simple_imp_strengthen else IMP_CONG_simple_imp_weaken 784 val thm3 = MATCH_MP cong_thm (CONJ thm1 thm2) 785 val thm4 = CONV_RULE (dir_conv dir trivial_imp_simp) thm3 handle HOL_ERR _ => thm3 786 in 787 (n2, thm4) 788 end handle HOL_ERR _ => raise CONSEQ_CONV_congruence_exn; 789 790 791 792 793fun trivial_cond_simp t = 794let 795 val (c, t1, t2) = dest_cond t 796in 797 if (same_const c T) then 798 ISPECL [t1,t2] COND_CLAUSES_CT 799 else if (same_const c F) then 800 ISPECL [t1,t2] COND_CLAUSES_CF 801 else if (same_const t1 T) then 802 SPECL [c, t2] COND_CLAUSES_TT 803 else if (same_const t1 F) then 804 SPECL [c, t2] COND_CLAUSES_TF 805 else if (same_const t2 T) then 806 SPECL [c, t1] COND_CLAUSES_FT 807 else if (same_const t2 F) then 808 SPECL [c, t1] COND_CLAUSES_FF 809 else if (aconv t1 t2) then 810 ISPECL [c,t1] COND_CLAUSES_ID 811 else Feedback.fail() 812end 813 814 815fun CONSEQ_CONV_CONGRUENCE___cond_no_context context (sys:conseq_conv_congruence_syscall) dir t = 816 let 817 val (c,b1,b2) = dest_cond t; 818 val (n1, thm1_opt) = sys [] context 0 dir b1; 819 val (n2, thm2_opt) = sys [] context n1 dir b2; 820 821 val _ = if (isSome thm1_opt) orelse (isSome thm2_opt) then () else raise UNCHANGED; 822 val thm1 = conseq_conv_congruence_EXPAND_THM_OPT (thm1_opt, b1, NONE); 823 val thm2 = conseq_conv_congruence_EXPAND_THM_OPT (thm2_opt, b2, NONE); 824 825 val thm3 = MATCH_MP (ISPEC c IMP_CONG_cond_simple) (CONJ thm1 thm2) 826 val thm4 = CONV_RULE (dir_conv dir trivial_cond_simp) thm3 handle HOL_ERR _ => thm3 827 in 828 (n2, thm4) 829 end handle HOL_ERR _ => raise CONSEQ_CONV_congruence_exn; 830 831 832fun CONSEQ_CONV_CONGRUENCE___cond_context context (sys:conseq_conv_congruence_syscall) dir t = 833 let 834 val (c,b1,b2) = dest_cond t; 835 val (n1, thm1_opt) = sys [c] context 0 dir b1; 836 val (n2, thm2_opt) = sys [mk_neg c] context n1 dir b2; 837 838 val _ = if (isSome thm1_opt) orelse (isSome thm2_opt) then () else raise UNCHANGED; 839 val thm1 = conseq_conv_congruence_EXPAND_THM_OPT (thm1_opt, b1, SOME c); 840 val thm2 = conseq_conv_congruence_EXPAND_THM_OPT (thm2_opt, b2, SOME (mk_neg c)); 841 842 val thm3 = MATCH_MP (ISPEC c IMP_CONG_cond) (CONJ thm1 thm2) 843 val thm4 = CONV_RULE (dir_conv dir trivial_cond_simp) thm3 handle HOL_ERR _ => thm3 844 in 845 (n2, thm4) 846 end handle HOL_ERR _ => raise CONSEQ_CONV_congruence_exn; 847 848 849 850fun var_filter_context v = 851 filter (fn thm => 852 let 853 val fv = FVL ((concl thm)::(hyp thm)) empty_varset; 854 in 855 not (HOLset.member (fv, v)) 856 end) 857 858 859fun CONSEQ_CONV_CONGRUENCE___forall context (sys:conseq_conv_congruence_syscall) dir t = 860 let 861 val (v, b1) = dest_forall t; 862 val (n1, thm1_opt) = sys [] (var_filter_context v context) 0 dir b1; 863 val _ = if (isSome thm1_opt) then () else raise UNCHANGED; 864 865 val thm2 = HO_MATCH_MP MONO_ALL (GEN_ASSUM v (valOf thm1_opt)) 866 val thm3 = CONV_RULE (dir_conv dir FORALL_SIMP_CONV) thm2 handle HOL_ERR _ => thm2 867 in 868 (n1, thm3) 869 end 870 871 872fun CONSEQ_CONV_CONGRUENCE___exists context (sys:conseq_conv_congruence_syscall) dir t = 873 let 874 val (v, b1) = dest_exists t; 875 val (n1, thm1_opt) = sys [] (var_filter_context v context) 0 dir b1; 876 val _ = if (isSome thm1_opt) then () else raise UNCHANGED; 877 878 val thm2 = HO_MATCH_MP boolTheory.MONO_EXISTS (GEN_ASSUM v (valOf thm1_opt)) 879 val thm3 = CONV_RULE (dir_conv dir EXISTS_SIMP_CONV) thm2 handle HOL_ERR _ => thm2 880 in 881 (n1, thm3) 882 end 883 884 885val CONSEQ_CONV_CONGRUENCE___basic_list___full_context = [ 886 CONSEQ_CONV_CONGRUENCE___conj, 887 CONSEQ_CONV_CONGRUENCE___disj, 888 CONSEQ_CONV_CONGRUENCE___neg, 889 CONSEQ_CONV_CONGRUENCE___imp_full_context, 890 CONSEQ_CONV_CONGRUENCE___forall, 891 CONSEQ_CONV_CONGRUENCE___exists, 892 CONSEQ_CONV_CONGRUENCE___cond_context, 893 CONSEQ_CONV_CONGRUENCE___asm_marker] 894 895 896val CONSEQ_CONV_CONGRUENCE___basic_list___no_context = [ 897 CONSEQ_CONV_CONGRUENCE___conj_no_context, 898 CONSEQ_CONV_CONGRUENCE___disj_no_context, 899 CONSEQ_CONV_CONGRUENCE___neg, 900 CONSEQ_CONV_CONGRUENCE___imp_no_context, 901 CONSEQ_CONV_CONGRUENCE___forall, 902 CONSEQ_CONV_CONGRUENCE___exists, 903 CONSEQ_CONV_CONGRUENCE___cond_no_context, 904 CONSEQ_CONV_CONGRUENCE___asm_marker] 905 906val CONSEQ_CONV_CONGRUENCE___basic_list = [ 907 CONSEQ_CONV_CONGRUENCE___conj_no_context, 908 CONSEQ_CONV_CONGRUENCE___disj_no_context, 909 CONSEQ_CONV_CONGRUENCE___neg, 910 CONSEQ_CONV_CONGRUENCE___imp_simple_context, 911 CONSEQ_CONV_CONGRUENCE___forall, 912 CONSEQ_CONV_CONGRUENCE___exists, 913 CONSEQ_CONV_CONGRUENCE___cond_context, 914 CONSEQ_CONV_CONGRUENCE___asm_marker] 915 916 917fun CONSEQ_CONV_get_context_congruences 918 CONSEQ_CONV_NO_CONTEXT = CONSEQ_CONV_CONGRUENCE___basic_list___no_context 919 | CONSEQ_CONV_get_context_congruences 920 CONSEQ_CONV_IMP_CONTEXT = CONSEQ_CONV_CONGRUENCE___basic_list 921 | CONSEQ_CONV_get_context_congruences 922 CONSEQ_CONV_FULL_CONTEXT = CONSEQ_CONV_CONGRUENCE___basic_list___full_context 923 924 925fun step_opt_sub NONE n = NONE 926 | step_opt_sub (SOME m) n = SOME (m - n) 927 928fun step_opt_allows_steps NONE _ _ = true 929 | step_opt_allows_steps (SOME m) n NONE = (n <= m) 930 | step_opt_allows_steps (SOME m) n (SOME w) = 931 (n < m) andalso (n+w <= m); 932 933 934(* ------------------------------------- 935 Context 936 -------------------------------------*) 937 938(* 939 some test data for debugging 940 941val congruence_list = CONSEQ_CONV_CONGRUENCE___basic_list 942 943fun my_conv t = 944 if (aconv t ``xxx:bool``) then 945 mk_thm ([], ``xxx /\ xxx ==> xxx``) 946 else 947 Feedback.fail() 948 949val step_opt = SOME 2; 950val redepth = true 951val conv = (K my_conv) 952 953val t = ``xxx:bool`` 954val n = 0 955val dir = CONSEQ_CONV_STRENGTHEN_direction 956 957*) 958 959 960val NOT_CLAUSES_NEG = CONJUNCT1 NOT_CLAUSES 961val NOT_CLAUSES_T = CONJUNCT1 (CONJUNCT2 NOT_CLAUSES) 962val DE_MORGAN_THM_OR = el 2 963 (CONJUNCTS (Ho_Rewrite.PURE_REWRITE_RULE [FORALL_AND_THM] DE_MORGAN_THM)) 964val NOT_EXISTS_THM2 = CONV_RULE (DEPTH_CONV ETA_CONV) NOT_EXISTS_THM 965 966 967fun mk_context2 l [] = l 968| mk_context2 l (thm::thmL) = 969 if (is_neg (concl thm)) then ( 970 let 971 val body = dest_neg (concl thm); 972 in 973 if (same_const body T) then 974 [CONV_RULE (K NOT_CLAUSES_T) thm] 975 else if (same_const body F) then 976 mk_context2 l thmL 977 else if (is_neg body) then 978 let 979 val thm0 = SPEC (dest_neg body) NOT_CLAUSES_NEG 980 val thm1 = CONV_RULE (K thm0) thm 981 in 982 mk_context2 l (thm1::thmL) 983 end 984 else if (is_eq body) then 985 mk_context2 (thm::(GSYM thm)::l) thmL 986 else if (is_disj body) then 987 let 988 val (t1,t2) = dest_disj body 989 val thm0 = SPECL [t1,t2] DE_MORGAN_THM_OR; 990 val thm1 = CONV_RULE (K thm0) thm 991 in 992 mk_context2 l (thm1::thmL) 993 end 994 else if (is_imp_only body) then 995 let 996 val (t1,t2) = dest_imp_only body 997 val thm0 = SPECL [t1,t2] NOT_IMP; 998 val thm1 = CONV_RULE (K thm0) thm 999 in 1000 mk_context2 l (thm1::thmL) 1001 end 1002 else if (is_exists body) then 1003 let 1004 val thm0 = ISPEC (rand body) NOT_EXISTS_THM2 1005 val thm1 = CONV_RULE (RHS_CONV (QUANT_CONV ( 1006 RAND_CONV BETA_CONV))) thm0 1007 val thm2 = CONV_RULE (K thm1) thm 1008 in 1009 mk_context2 l (thm2::thmL) 1010 end 1011 else if (is_asm_marker body) then 1012 mk_context2 l ((CONV_RULE (RAND_CONV asm_marker_ELIM_CONV) thm)::thmL) 1013 else 1014 mk_context2 (thm::l) thmL 1015 end) 1016 else if (same_const (concl thm) F) then [thm] 1017 else if (same_const (concl thm) T) then 1018 mk_context2 l thmL 1019 else if ((is_forall (concl thm) orelse 1020 (is_conj (concl thm)))) then 1021 mk_context2 l ((BODY_CONJUNCTS thm)@thmL) 1022 else if (is_asm_marker (concl thm)) then 1023 mk_context2 l ((CONV_RULE asm_marker_ELIM_CONV thm)::thmL) 1024 else mk_context2 (thm::l) thmL 1025 1026 1027fun mk_context t = mk_context2 [] [ASSUME t] 1028 1029 1030 1031 1032(* 1033fun mk_context t = profile "mk_context" (fn t => filter_context [] 1034 (BODY_CONJUNCTS (CONV_RULE mk_context_CONV (ASSUME t)))) t 1035 1036 1037fun mk_context t = profile "mk_context 2" (fn t => filter_context [] 1038 (BODY_CONJUNCTS (ASSUME t))) t 1039 1040fun mk_context t = profile "mk_context 3" (fn t => []) t 1041*) 1042 1043fun false_context_sys_call n cthm dir t = 1044let 1045 val thm_t = 1046 if dir = CONSEQ_CONV_STRENGTHEN_direction then 1047 mk_imp (T, t) 1048 else mk_imp (t, F) 1049 val thm = MP (SPEC thm_t FALSITY) cthm 1050in 1051 (n:int, SOME thm) 1052end; 1053 1054(* ----------------------------------- 1055 Caches 1056 ----------------------------------- *) 1057 1058fun get_cache_result NONE m step_opt dir t = NONE 1059 | get_cache_result (SOME (cache_ref, _)) m step_opt dir t = 1060let 1061 val (cache_str, cache_weak) = !cache_ref; 1062 val cached_result = 1063 if (same_const t T) orelse (same_const t F) then 1064 SOME (0, NONE) 1065 else if dir = CONSEQ_CONV_STRENGTHEN_direction then 1066 Redblackmap.peek (cache_str, t) 1067 else 1068 Redblackmap.peek (cache_weak, t); 1069 val cached_result' = if isSome cached_result then 1070 let 1071 val (n, thm_opt) = valOf cached_result; 1072 in 1073 if step_opt_allows_steps step_opt n (SOME m) then 1074 SOME (true, n+m, thm_opt) 1075 else 1076 NONE 1077 end else NONE 1078in 1079 cached_result' 1080end; 1081 1082fun store_cache_result NONE m step_opt dir t (n, thm_opt) = () 1083 | store_cache_result (SOME (cache_ref, cache_pred)) m step_opt dir t (n, thm_opt) = 1084let 1085 (* ajust needed steps *) 1086 val result' = (n - m, thm_opt); 1087 1088 (* was it perhaps aborded early ? *) 1089 val aborted = (isSome step_opt) andalso not (isSome thm_opt); 1090 1091 val no_assums_used = (not (isSome thm_opt)) orelse (null (hyp (valOf thm_opt))); 1092 val cache_result = no_assums_used andalso (not aborted) andalso 1093 (cache_pred (t, result')) 1094 1095in 1096 if not cache_result then () else 1097 let 1098 val (cache_str, cache_weak) = !cache_ref; 1099 val _ = cache_ref := ( 1100 if dir = CONSEQ_CONV_STRENGTHEN_direction then 1101 (Redblackmap.insert (cache_str, t, result'), cache_weak) 1102 else 1103 (cache_str, Redblackmap.insert (cache_weak, t, result'))) 1104 in 1105 () 1106 end 1107end; 1108 1109 1110(* ----------------------------------------- 1111 Main part of DEPTH_CONSEQ_CONV 1112 ----------------------------------------- *) 1113 1114fun STEP_CONSEQ_CONV congruence_list convL = 1115let 1116 fun conv_trans (_,w,c) = 1117 (w, true, fn sys => fn context => fn dir => fn t => 1118 (true, (if isSome w then valOf w else 0, CONSEQ_CONV_WRAPPER (c context) dir t))) 1119 1120 val (beforeL, afterL) = partition (fn (b,w,c) => b) convL 1121 val fL = 1122 (map conv_trans beforeL)@ 1123 (map (fn c => (NONE, false, fn sys => fn context => fn dir => fn t => (false, c context sys dir t))) congruence_list)@ 1124 (map conv_trans afterL) 1125 1126 fun check_fun n step_opt sys context use_congs dir t (w,is_not_cong,c) = 1127 if not (is_not_cong orelse use_congs) then Feedback.fail() else 1128 if not (step_opt_allows_steps step_opt n w) then Feedback.fail() else 1129 let 1130 val (rec_flag, (w', thm)) = c sys context dir t handle UNCHANGED => Feedback.fail(); 1131 in 1132 (rec_flag, n+w', SOME thm) 1133 end 1134in 1135 (fn n => fn step_opt => fn sys => fn context => fn use_congs => fn dir => fn t => 1136 ((tryfind (check_fun n step_opt sys context use_congs dir t) fL) 1137 handle HOL_ERR _ => (false, n, NONE))) 1138end 1139 1140 1141(* 1142val congruence_list = CONSEQ_CONV_CONGRUENCE___basic_list 1143val use_context = true 1144val (cf, p) = valOf CONSEQ_CONV_default_cache_opt 1145val cache_opt = SOME (cf (), p) 1146val step_opt = SOME 3 1147val redepth = true 1148val convL = [(true,1,K (K c_conv))] 1149val t = ``c 0`` 1150val dir = CONSEQ_CONV_STRENGTHEN_direction 1151val n = 3 1152*) 1153 1154fun DEPTH_CONSEQ_CONV_num step_conv cache_opt 1155 redepth context n step_opt use_congs dir t = 1156 let 1157 val _ = if (same_const t T) orelse (same_const t F) then raise UNCHANGED else (); 1158 fun sys new_context old_context m dir t = 1159 let 1160 val _ = if (same_const t T) orelse (same_const t F) then raise UNCHANGED else (); 1161 val context' = flatten (map mk_context new_context); 1162 val false_context = 1163 (not (null context')) andalso 1164 (same_const (concl (hd context')) F) 1165 val context'' = context'@ old_context 1166 in 1167 if false_context then false_context_sys_call m (hd context') dir t else 1168 DEPTH_CONSEQ_CONV_num step_conv cache_opt redepth context'' m 1169 (step_opt_sub step_opt n) true dir t 1170 end handle UNCHANGED => (m, NONE) 1171 | HOL_ERR _ => (m, NONE); 1172 1173 (* try to get it from cache *) 1174 val result_opt = get_cache_result cache_opt n step_opt dir t; 1175 val (congs_flag, n1, thm1_opt) = if isSome result_opt then 1176 valOf result_opt else 1177 step_conv n step_opt sys context use_congs dir t 1178 1179 val do_depth_call = redepth andalso isSome thm1_opt; 1180 val (n2, thm2_opt) = if not do_depth_call then (n1, thm1_opt) else 1181 let 1182 val thm1 = valOf thm1_opt; 1183 val t2 = CONSEQ_CONV___GET_SIMPLIFIED_TERM thm1 t 1184 val (n2, thm2_opt) = 1185 DEPTH_CONSEQ_CONV_num step_conv cache_opt 1186 redepth context n1 step_opt congs_flag dir t2 1187 val thm3_opt = 1188 if isSome thm2_opt then 1189 SOME (THEN_CONSEQ_CONV___combine thm1 (valOf thm2_opt) t) 1190 else thm1_opt 1191 in 1192 (n2, thm3_opt) 1193 end 1194 1195 val _ = store_cache_result cache_opt n step_opt dir t (n2, thm2_opt) 1196 in 1197 (n2, thm2_opt) 1198 end handle UNCHANGED => (n, NONE); 1199 1200type depth_conseq_conv_cache = 1201 ((term, (int * thm option)) Redblackmap.dict * (term, (int * thm option)) Redblackmap.dict) ref 1202type depth_conseq_conv_cache_opt = 1203 ((unit -> depth_conseq_conv_cache) * ((term * (int * thm option)) -> bool)) option 1204 1205(* for debugging 1206fun dest_cache NONE = ([], []) 1207 | dest_cache (SOME (cf, _)) = 1208 let 1209 val (str, weak) = !(cf ()) 1210 in 1211 (Redblackmap.listItems str, 1212 Redblackmap.listItems weak) 1213 end; 1214*) 1215 1216 1217fun mk_DEPTH_CONSEQ_CONV_CACHE_dict () = 1218 (Redblackmap.mkDict (Term.compare), Redblackmap.mkDict (Term.compare)) 1219 1220fun mk_DEPTH_CONSEQ_CONV_CACHE () = 1221 (ref (mk_DEPTH_CONSEQ_CONV_CACHE_dict ())):depth_conseq_conv_cache 1222 1223fun mk_DEPTH_CONSEQ_CONV_CACHE_OPT p = 1224 SOME (mk_DEPTH_CONSEQ_CONV_CACHE, p):depth_conseq_conv_cache_opt 1225 1226fun mk_PERSISTENT_DEPTH_CONSEQ_CONV_CACHE_OPT p = 1227 SOME (K (mk_DEPTH_CONSEQ_CONV_CACHE ()), p):depth_conseq_conv_cache_opt 1228 1229val CONSEQ_CONV_default_cache_opt:depth_conseq_conv_cache_opt = 1230 SOME (mk_DEPTH_CONSEQ_CONV_CACHE, K true); 1231 1232fun clear_CONSEQ_CONV_CACHE (cr:depth_conseq_conv_cache) = 1233 (cr := mk_DEPTH_CONSEQ_CONV_CACHE_dict()) 1234 1235fun clear_CONSEQ_CONV_CACHE_OPT (NONE:depth_conseq_conv_cache_opt) = () 1236 | clear_CONSEQ_CONV_CACHE_OPT (SOME (cr_f, _)) = 1237 ((cr_f ()) := mk_DEPTH_CONSEQ_CONV_CACHE_dict()) 1238 1239(* 1240val c_def = Define `c (n:num) = T` 1241val c_thm = prove (``!n. (c (SUC n))==> c n``, SIMP_TAC std_ss [c_def]) 1242val c_conv = PART_MATCH (snd o dest_imp) c_thm 1243 1244val congruence_list = CONSEQ_CONV_CONGRUENCE___basic_list 1245val cache = NONE 1246val step_opt = SOME 4; 1247val redepth = true; 1248val thm = EXT_DEPTH_CONSEQ_CONV 1249val convL = [(true,1,K (K c_conv))] 1250val n = 0; 1251val context = [] 1252val dir = CONSEQ_CONV_STRENGTHEN_direction; 1253val t = ``c 0`` 1254*) 1255 1256fun EXT_DEPTH_NUM_CONSEQ_CONV congruence_list (cache:depth_conseq_conv_cache_opt) step_opt redepth convL context = 1257 let 1258 val step_conv = STEP_CONSEQ_CONV congruence_list convL; 1259 fun internal_call cache_opt = DEPTH_CONSEQ_CONV_num step_conv cache_opt 1260 redepth context 0 step_opt true; 1261 1262 in 1263 fn dir => fn t => 1264 let 1265 val cache_opt = if isSome cache then SOME ((fst (valOf cache)) (), snd (valOf cache)) else NONE 1266 in 1267 internal_call cache_opt dir t 1268 end 1269 end; 1270 1271 1272fun EXT_DEPTH_CONSEQ_CONV congruence_list (cache:depth_conseq_conv_cache_opt) step_opt redepth convL context dir t = 1273 let 1274 val (_, thm_opt) = EXT_DEPTH_NUM_CONSEQ_CONV congruence_list (cache:depth_conseq_conv_cache_opt) step_opt redepth convL context dir t 1275 val _ = if isSome thm_opt then () else raise UNCHANGED; 1276 in 1277 valOf thm_opt 1278 end; 1279 1280 1281fun CONTEXT_DEPTH_CONSEQ_CONV context conv = 1282 EXT_DEPTH_CONSEQ_CONV (CONSEQ_CONV_get_context_congruences context) 1283 NONE NONE false [(true, SOME 1, conv)] [] 1284fun DEPTH_CONSEQ_CONV conv = 1285 CONTEXT_DEPTH_CONSEQ_CONV CONSEQ_CONV_NO_CONTEXT (K conv) 1286 1287 1288fun CONTEXT_REDEPTH_CONSEQ_CONV context conv = 1289 EXT_DEPTH_CONSEQ_CONV (CONSEQ_CONV_get_context_congruences context) 1290 CONSEQ_CONV_default_cache_opt NONE true [(true,SOME 1,conv)] [] 1291fun REDEPTH_CONSEQ_CONV conv = 1292 CONTEXT_REDEPTH_CONSEQ_CONV CONSEQ_CONV_NO_CONTEXT (K conv) 1293 1294fun CONTEXT_NUM_DEPTH_CONSEQ_CONV context conv n = 1295 EXT_DEPTH_CONSEQ_CONV (CONSEQ_CONV_get_context_congruences context) 1296 CONSEQ_CONV_default_cache_opt (SOME n) true [(true, SOME 1, conv)] [] 1297fun NUM_DEPTH_CONSEQ_CONV conv = CONTEXT_NUM_DEPTH_CONSEQ_CONV CONSEQ_CONV_NO_CONTEXT (K conv) 1298 1299fun CONTEXT_NUM_REDEPTH_CONSEQ_CONV conv n = 1300 EXT_DEPTH_CONSEQ_CONV CONSEQ_CONV_CONGRUENCE___basic_list 1301 CONSEQ_CONV_default_cache_opt (SOME n) true [(true, SOME 1, conv)] [] 1302fun NUM_REDEPTH_CONSEQ_CONV conv = CONTEXT_NUM_REDEPTH_CONSEQ_CONV (K conv) 1303 1304fun CONTEXT_ONCE_DEPTH_CONSEQ_CONV context conv = CONTEXT_NUM_DEPTH_CONSEQ_CONV context conv 1 1305fun ONCE_DEPTH_CONSEQ_CONV conv = NUM_DEPTH_CONSEQ_CONV conv 1 1306 1307 1308(*A tactic that strengthens a boolean goal*) 1309fun CONSEQ_CONV_TAC conv (asm,t) = 1310 ((HO_MATCH_MP_TAC ((CHANGED_CONSEQ_CONV (conv CONSEQ_CONV_STRENGTHEN_direction)) t) 1311 THEN TRY (ACCEPT_TAC TRUTH)) (asm,t) handle UNCHANGED => 1312 ALL_TAC (asm,t)) 1313 1314fun ASM_CONSEQ_CONV_TAC conv (asm,t) = 1315 CONSEQ_CONV_TAC (conv (mk_context2 [] (map ASSUME asm))) (asm, t) 1316 1317fun DEPTH_CONSEQ_CONV_TAC conv = 1318 CONSEQ_CONV_TAC (DEPTH_CONSEQ_CONV conv) 1319 1320fun REDEPTH_CONSEQ_CONV_TAC conv = 1321 CONSEQ_CONV_TAC (REDEPTH_CONSEQ_CONV conv) 1322 1323fun ONCE_DEPTH_CONSEQ_CONV_TAC conv = 1324 CONSEQ_CONV_TAC (ONCE_DEPTH_CONSEQ_CONV conv) 1325 1326fun STRENGTHEN_CONSEQ_CONV conv dir = 1327 if dir = CONSEQ_CONV_WEAKEN_direction then raise UNCHANGED else conv; 1328 1329fun WEAKEN_CONSEQ_CONV conv dir = 1330 if dir = CONSEQ_CONV_STRENGTHEN_direction then raise UNCHANGED else conv; 1331 1332fun DEPTH_STRENGTHEN_CONSEQ_CONV conv = 1333 DEPTH_CONSEQ_CONV (K conv) CONSEQ_CONV_STRENGTHEN_direction; 1334 1335fun REDEPTH_STRENGTHEN_CONSEQ_CONV conv = 1336 REDEPTH_CONSEQ_CONV (K conv) CONSEQ_CONV_STRENGTHEN_direction; 1337 1338 1339(*--------------------------------------------------------------------------- 1340 * if conv ``A`` = |- (A' ==> A) then 1341 * STRENGTHEN_CONSEQ_CONV_RULE ``(A ==> B)`` = |- (A' ==> B) 1342 *---------------------------------------------------------------------------*) 1343 1344fun STRENGTHEN_CONSEQ_CONV_RULE conv thm = let 1345 val (imp_term,_) = dest_imp (concl thm); 1346 val imp_thm = conv CONSEQ_CONV_STRENGTHEN_direction imp_term; 1347 in 1348 IMP_TRANS imp_thm thm 1349 end 1350 1351 1352(*--------------------------------------------------------------------------- 1353 * if conv ``A`` = |- (A' ==> A) then 1354 * WEAKEN_CONSEQ_CONV_RULE ``(A ==> B)`` = |- (A' ==> B) 1355 *---------------------------------------------------------------------------*) 1356 1357fun WEAKEN_CONSEQ_CONV_RULE conv thm = let 1358 val (_, imp_term) = dest_imp (concl thm); 1359 val imp_thm = conv CONSEQ_CONV_WEAKEN_direction imp_term; 1360 in 1361 IMP_TRANS thm imp_thm 1362 end 1363 1364 1365(*--------------------------------------------------------------------------- 1366 * A kind of REWRITE conversion for implications. 1367 * 1368 * CONSEQ_REWR_CONV thm takes thms of either the form 1369 * "|- a ==> c", "|- c = a" or "|- c" 1370 * 1371 * c is handled exactly as "c = T" 1372 * 1373 * If the thm is an equation, a "normal" rewrite is attempted. Otherwise, 1374 * CONDSEQ_REWR_CONV tries to match c or a with the input t and then returns a theorem 1375 * "|- (instantiated a) ==> t" or "|- t ==> (instantiated c)". Which ones happens 1376 * depends on the value of strengten. 1377 *---------------------------------------------------------------------------*) 1378 1379fun CONSEQ_REWR_CONV___with_match ho strengten thm = 1380 if (is_imp_only (concl thm)) then 1381 ((if ho then HO_PART_MATCH else PART_MATCH) ((if strengten then snd else fst) o dest_imp) thm, 1382 ((if strengten then snd else fst) o dest_imp o concl) thm) 1383 else 1384 if (is_eq (concl thm)) then 1385 (PART_MATCH lhs thm, 1386 (lhs o concl) thm) 1387 else 1388 (EQT_INTRO o PART_MATCH I thm, 1389 concl thm) 1390 1391 1392fun CONSEQ_REWR_CONV strengten thm = 1393 fst (CONSEQ_REWR_CONV___with_match false strengten thm); 1394 1395 1396fun CONSEQ_TOP_REWRITE_CONV___EQT_EQF_INTRO thm = 1397 if (is_eq (concl thm) andalso (type_of (lhs (concl thm)) = bool)) then thm else 1398 if (is_imp (concl thm)) then thm else 1399 if (is_neg (concl thm)) then EQF_INTRO thm else 1400 EQT_INTRO thm; 1401 1402fun IMP_EXISTS_PRECOND_CANON thm = 1403 let val th = GEN_ALL thm 1404 val tm = concl th; 1405 val (avs,bod) = strip_forall tm 1406 val (ant,conseq) = dest_imp_only bod 1407 val th1 = SPECL avs (ASSUME tm) 1408 val th2 = UNDISCH th1 1409 val evs = filter(fn v => free_in v ant andalso not(free_in v conseq)) avs 1410 val th3 = itlist SIMPLE_CHOOSE evs (DISCH tm th2) 1411 val tm3 = Lib.trye hd(hyp th3) 1412 in MP (DISCH tm (DISCH tm3 (UNDISCH th3))) th end 1413 handle HOL_ERR _ => thm; 1414 1415 1416fun IMP_FORALL_CONCLUSION_CANON thm = 1417 let val th = GEN_ALL thm 1418 val tm = concl th; 1419 val (avs,bod) = strip_forall tm 1420 val (ant,conseq) = dest_imp_only bod 1421 val th1 = SPECL avs (ASSUME tm) 1422 val th2 = UNDISCH th1 1423 val evs = filter(fn v => not(free_in v ant) andalso free_in v conseq) avs 1424 val th3 = GENL evs th2 1425 val th4 = DISCH ant th3; 1426 val th5 = DISCH tm th4; 1427 val th6 = MP th5 th 1428 in th6 end 1429 handle HOL_ERR _ => thm; 1430 1431 1432fun IMP_QUANT_CANON thm = 1433 let val th = GEN_ALL thm 1434 val tm = concl th; 1435 val (avs,bod) = strip_forall tm 1436 val (ant,conseq) = dest_imp_only bod 1437 val th1 = SPECL avs (ASSUME tm) 1438 val th2 = UNDISCH th1 1439 val evs = filter(fn v => not(free_in v ant) andalso free_in v conseq) avs 1440 val evs2 = filter(fn v => free_in v ant andalso not(free_in v conseq)) avs 1441 val th3 = GENL evs th2 1442 val th4 = itlist SIMPLE_CHOOSE evs2 (DISCH tm th3) 1443 val tm4 = Lib.trye hd(hyp th4) 1444 1445 val th5 = UNDISCH th4; 1446 val th6 = DISCH tm4 th5; 1447 val th7 = DISCH tm th6; 1448 val th8 = MP th7 th 1449 in th8 end 1450 handle HOL_ERR _ => thm; 1451 1452 1453 1454 1455fun CONSEQ_TOP_REWRITE_CONV___PREPARE_STRENGTHEN_THMS thmL = 1456let 1457 val thmL1 = map IMP_EXISTS_PRECOND_CANON thmL; 1458in 1459 thmL1 1460end; 1461 1462 1463fun CONSEQ_TOP_REWRITE_CONV___PREPARE_WEAKEN_THMS thmL = 1464let 1465 val thmL1 = map IMP_FORALL_CONCLUSION_CANON thmL; 1466in 1467 thmL1 1468end; 1469 1470(* val thm0 = prove (``(SUC 1 = 2) = (2 = 2)``, DECIDE_TAC) 1471 val t = ``X ==> (SUC 1 = 2)`` 1472 val (both_thmL,strengthen_thmL,weaken_thmL) = ([thm0], [], []); 1473 val ho = false 1474 val thmL = (append strengthen_thmL both_thmL) 1475*) 1476fun CONSEQ_TOP_REWRITE_CONV___ho_opt ho (both_thmL,strengthen_thmL,weaken_thmL) = 1477 let 1478 fun prepare_general_thmL thmL = 1479 let 1480 val thmL1 = flatten (map BODY_CONJUNCTS thmL); 1481 val thmL2 = map (CONV_RULE (TRY_CONV (REDEPTH_CONV LEFT_IMP_EXISTS_CONV))) thmL1; 1482 val thmL3 = map (CONV_RULE (REDEPTH_CONV RIGHT_IMP_FORALL_CONV)) thmL2; 1483 val thmL4 = map SPEC_ALL thmL3 1484 in 1485 map CONSEQ_TOP_REWRITE_CONV___EQT_EQF_INTRO thmL4 1486 end; 1487 val thmL_st = CONSEQ_TOP_REWRITE_CONV___PREPARE_STRENGTHEN_THMS 1488 (prepare_general_thmL (append strengthen_thmL both_thmL)); 1489 val thmL_we = CONSEQ_TOP_REWRITE_CONV___PREPARE_WEAKEN_THMS 1490 (prepare_general_thmL (append weaken_thmL both_thmL)); 1491 1492 1493 val net_st = foldr (fn ((conv,t),net) => Net.insert (t,conv) net) Net.empty 1494 (map (CONSEQ_REWR_CONV___with_match ho true) thmL_st); 1495 val net_we = foldr (fn ((conv,t),net) => Net.insert (t,conv) net) Net.empty 1496 (map (CONSEQ_REWR_CONV___with_match ho false) thmL_we); 1497 in 1498 (fn dir => fn t => 1499 let 1500 val convL = if (dir = CONSEQ_CONV_STRENGTHEN_direction) then 1501 Net.match t net_st 1502 else if (dir = CONSEQ_CONV_WEAKEN_direction) then 1503 Net.match t net_we 1504 else 1505 append (Net.match t net_st) (Net.match t net_we); 1506 1507 in 1508 FIRST_CONSEQ_CONV convL t 1509 end) 1510 end; 1511 1512 1513 1514fun FULL_EXT_CONSEQ_REWRITE_CONV congruence_list cache step_opt redepth ho 1515 context convL thmLs = 1516 EXT_DEPTH_CONSEQ_CONV congruence_list cache step_opt redepth 1517 (((false, SOME 1, K (CONSEQ_TOP_REWRITE_CONV___ho_opt ho thmLs))):: 1518 (map (fn (b,w,c) => 1519 (b,w, (fn context => K (CHANGED_CONV (c context))))) convL)) context; 1520 1521 1522 1523val CONSEQ_TOP_REWRITE_CONV = 1524 CONSEQ_TOP_REWRITE_CONV___ho_opt false 1525 1526val CONSEQ_TOP_HO_REWRITE_CONV = 1527 CONSEQ_TOP_REWRITE_CONV___ho_opt true 1528 1529fun CONSEQ_TOP_REWRITE_TAC thmLs = 1530 CONSEQ_CONV_TAC (CONSEQ_TOP_REWRITE_CONV thmLs); 1531 1532fun CONSEQ_TOP_HO_REWRITE_TAC thmLs = 1533 CONSEQ_CONV_TAC (CONSEQ_TOP_HO_REWRITE_CONV thmLs); 1534 1535val CONSEQ_REWRITE_CONV = 1536 FULL_EXT_CONSEQ_REWRITE_CONV CONSEQ_CONV_CONGRUENCE___basic_list 1537 CONSEQ_CONV_default_cache_opt NONE true false [] [] 1538 1539val ONCE_CONSEQ_REWRITE_CONV = 1540 FULL_EXT_CONSEQ_REWRITE_CONV CONSEQ_CONV_CONGRUENCE___basic_list 1541 NONE (SOME 1) true false [] [] 1542 1543fun CONSEQ_REWRITE_TAC thmLs = 1544 CONSEQ_CONV_TAC (CONSEQ_REWRITE_CONV thmLs); 1545 1546fun ONCE_CONSEQ_REWRITE_TAC thmLs = 1547 CONSEQ_CONV_TAC (ONCE_CONSEQ_REWRITE_CONV thmLs); 1548 1549val CONSEQ_HO_REWRITE_CONV = 1550 FULL_EXT_CONSEQ_REWRITE_CONV CONSEQ_CONV_CONGRUENCE___basic_list 1551 CONSEQ_CONV_default_cache_opt NONE true true [] [] 1552 1553val ONCE_CONSEQ_HO_REWRITE_CONV = 1554 FULL_EXT_CONSEQ_REWRITE_CONV CONSEQ_CONV_CONGRUENCE___basic_list 1555 NONE (SOME 1) true true [] [] 1556 1557fun CONSEQ_HO_REWRITE_TAC thmLs = 1558 CONSEQ_CONV_TAC (CONSEQ_HO_REWRITE_CONV thmLs); 1559 1560fun ONCE_CONSEQ_HO_REWRITE_TAC thmLs = 1561 CONSEQ_CONV_TAC (ONCE_CONSEQ_HO_REWRITE_CONV thmLs); 1562 1563 1564fun EXT_CONTEXT_CONSEQ_REWRITE_CONV___ho_opt congruence_list cache step_opt ho context convL thmL = 1565 FULL_EXT_CONSEQ_REWRITE_CONV congruence_list 1566 cache step_opt true ho context 1567 ((map (fn c => (true, SOME 1, c)) convL)@ 1568 [(false, NONE, K (REWRITE_CONV thmL)), (false, NONE, fn context => 1569 REWRITE_CONV (context@thmL))]); 1570 1571 1572fun EXT_CONTEXT_CONSEQ_REWRITE_CONV context = 1573 EXT_CONTEXT_CONSEQ_REWRITE_CONV___ho_opt 1574 (CONSEQ_CONV_get_context_congruences context) 1575 CONSEQ_CONV_default_cache_opt NONE false [] 1576 1577val EXT_CONSEQ_REWRITE_CONV = 1578 EXT_CONTEXT_CONSEQ_REWRITE_CONV CONSEQ_CONV_IMP_CONTEXT; 1579 1580fun EXT_CONTEXT_CONSEQ_REWRITE_TAC context convL thmL thmLs = 1581 CONSEQ_CONV_TAC (EXT_CONTEXT_CONSEQ_REWRITE_CONV context convL thmL thmLs); 1582 1583val EXT_CONSEQ_REWRITE_TAC = 1584 EXT_CONTEXT_CONSEQ_REWRITE_TAC CONSEQ_CONV_IMP_CONTEXT 1585 1586 1587fun EXT_CONTEXT_CONSEQ_HO_REWRITE_CONV context = 1588 EXT_CONTEXT_CONSEQ_REWRITE_CONV___ho_opt 1589 (CONSEQ_CONV_get_context_congruences context) 1590 CONSEQ_CONV_default_cache_opt NONE true [] 1591 1592val EXT_CONSEQ_HO_REWRITE_CONV = 1593 EXT_CONTEXT_CONSEQ_HO_REWRITE_CONV CONSEQ_CONV_IMP_CONTEXT 1594 1595fun EXT_CONTEXT_CONSEQ_HO_REWRITE_TAC context convL thmL thmLs = 1596 CONSEQ_CONV_TAC (EXT_CONTEXT_CONSEQ_HO_REWRITE_CONV context convL thmL thmLs); 1597 1598val EXT_CONSEQ_HO_REWRITE_TAC = 1599 EXT_CONTEXT_CONSEQ_HO_REWRITE_TAC CONSEQ_CONV_IMP_CONTEXT 1600 1601 1602 1603 1604(* 1605 1606set_goal ([``x ++ y = x ++ [32]:num list``, ``l = [0:num]``, ``aa:bool``, ``bb:bool``, ``cc:bool``], ``?x. y ++ l = 0::x``) 1607 1608open quantHeuristicsLib 1609fun conv t = snd (EQ_IMP_RULE (QUANT_INSTANTIATE_CONV [] t)); 1610val conv = QUANT_INSTANTIATE_CONV [] THENC SIMP_CONV std_ss [AND_IMP_INTRO]; 1611 1612val (asm,t) = top_goal(); 1613ASSUME_TAC TRUTH 1614DISCH_ASM_CONV_TAC conv 1615 val conv = QUANT_INSTANTIATE_CONV [] 1616*) 1617 1618 1619(*dishes all the assumptions, then applies the conversions 1620 and undisches the results, ASM_MARKER is used to separate these 1621 assumptions*) 1622 1623 1624fun cases_rule [] t = 1625 if aconv t T then TRUTH else EQT_ELIM (REWRITE_CONV [ASM_MARKER_THM] t) 1626 | cases_rule (c::cL) t = 1627 if aconv t T then TRUTH else 1628 let 1629 val thm_f1 = EQT_ELIM (REWRITE_CONV [ASSUME (mk_neg c),ASM_MARKER_THM] t) 1630 val thm_f = ADD_ASSUM (mk_neg c) thm_f1 1631 1632 val thm_t1 = REWRITE_CONV [ASSUME c,ASM_MARKER_THM] t 1633 val thm_t2 = cases_rule cL (rhs (concl thm_t1)) 1634 val thm_t3 = EQ_MP (GSYM thm_t1) thm_t2 1635 val thm_t = ADD_ASSUM c thm_t3 1636 1637 val em_thm = SPEC c EXCLUDED_MIDDLE 1638 in 1639 DISJ_CASES em_thm thm_t thm_f 1640 end; 1641 1642fun ASM_MARKER_CONV (m_base, mL, m_top) tt = 1643let 1644 val (fv, body) = strip_forall tt; 1645 val (m, body') = dest_asm_marker body 1646 val _ = if aconv m m_top then () else Feedback.fail() 1647 1648 val tL = find_terms is_asm_marker body'; 1649 val tmL = map (fn t => (fst (dest_asm_marker t), t)) tL 1650 fun find_mark m = snd (first (fn (m', t) => aconv m m') tmL) 1651 handle HOL_ERR _ => mk_asm_marker m T 1652 1653 val asm_list = map find_mark mL 1654 val base_t = find_mark m_base 1655 val (used_markerL,unused_markerL) = 1656 let 1657 val (l1, l2) = partition (fn t => aconv T (rand t)) (base_t::asm_list) 1658 in 1659 (l2, l1) 1660 end; 1661 1662 1663 val thm_tl = subst (map (fn t => t |-> (rand (rator t))) used_markerL) body' 1664 val thm_tr = subst (map (fn t => (rand (rator t)) |-> t) unused_markerL) 1665 (list_mk_imp (rev mL, m_base)) 1666 val thm_t = mk_eq (thm_tl, thm_tr); 1667 val thm0 = cases_rule mL thm_t 1668 1669 val thm1 = INST (map (fn t => (rand (rator t)) |-> t) used_markerL) thm0 1670 val thm2 = STRIP_QUANT_CONV (RAND_CONV (K thm1)) tt 1671 1672 val new_asm = map rand asm_list 1673 val new_t = rand base_t 1674in 1675 (new_asm, new_t, fv, thm2) 1676end 1677 1678 1679fun asm_marker_ADD_PRECONDITION new_mL tt = 1680if (is_forall tt) then ( 1681 let 1682 val (vs, tt') = strip_forall tt; 1683 val (new_mL', thm0) = asm_marker_ADD_PRECONDITION new_mL tt' 1684 val thm = STRIP_QUANT_CONV (K thm0) tt 1685 in 1686 (new_mL', thm) 1687 end 1688) else if (is_imp_only tt) then ( 1689 let 1690 val (a, c) = dest_imp tt; 1691 val (new_mL', c_thm) = asm_marker_ADD_PRECONDITION new_mL c; 1692 val new_m = genvar bool 1693 val a_thm = asm_marker_INTRO_CONV new_m a 1694 1695 val conv_a = (RATOR_CONV (RAND_CONV (K a_thm))) 1696 val conv_c = RAND_CONV (K c_thm) 1697 fun conv_forall t = (RIGHT_IMP_FORALL_CONV THENC 1698 TRY_CONV (QUANT_CONV conv_forall)) t 1699 1700 fun conv_move_marker ttt = 1701 let 1702 val (a, c) = dest_imp ttt; 1703 val (m, cb) = dest_asm_marker c; 1704 val c_thm = SPECL [m, cb] ASM_MARKER_THM 1705 val ac_thm = SPECL [m, mk_imp(a, cb)] (GSYM ASM_MARKER_THM) 1706 in 1707 (RAND_CONV (K c_thm) THENC (K ac_thm)) ttt 1708 end; 1709 1710 val thm = (conv_a THENC conv_c THENC 1711 (TRY_CONV conv_forall) THENC 1712 (TRY_CONV (STRIP_QUANT_CONV conv_move_marker))) tt 1713 in 1714 (new_m :: new_mL', thm) 1715 end 1716) else (new_mL, REFL tt) 1717 1718(* a simple tactic to remove true form the assumptions *) 1719val REMOVE_TRUE_TAC:tactic = fn (asm, t) => 1720 let 1721 val _ = if not (op_mem aconv T asm) then Feedback.fail() else (); 1722 in 1723 ([(filter (fn t => not (same_const t T)) asm, t)], 1724 hd) 1725 end; 1726 1727 1728val DISCH_ASM_CONV_TAC:(conv -> tactic) = fn conv => fn (asm,t) => 1729let 1730 val fv = HOLset.listItems (FVL (t::asm) empty_tmset) 1731 val (m_base, mt) = mk_asm_marker_random_pair t 1732 val asm_mL = map mk_asm_marker_random_pair asm 1733 val asm_t = foldl (fn (a,t) => mk_imp (snd a, t)) mt asm_mL; 1734 val (m_top, m_asm_t) = mk_asm_marker_random_pair asm_t 1735 val qasm_t = list_mk_forall (fv, m_asm_t); 1736 1737 val mL_org = map fst asm_mL 1738 val thm0a = conv qasm_t; 1739 val thm0 = snd (EQ_IMP_RULE thm0a) handle HOL_ERR _ => thm0a 1740 val (mL, thm1a) = asm_marker_ADD_PRECONDITION mL_org (rand (rator (concl thm0))) 1741 val thm1 = CONV_RULE (RATOR_CONV (RAND_CONV (K thm1a))) thm0 1742 1743 val (new_asm, new_t, new_fv, thm2a) = ASM_MARKER_CONV (m_base, mL, m_top) ((fst o dest_imp o concl) thm1) 1744 val thm2 = CONV_RULE (RATOR_CONV (RAND_CONV (K thm2a))) thm1 1745 1746(*val thmL = [mk_thm (new_asm,new_t)] 1747 val thmL = []*) 1748in 1749 (if aconv new_t T then [] else [(filter (fn t => not (same_const t T)) new_asm,new_t)], fn thmL => 1750 let 1751 val new_thm = if null thmL then TRUTH else hd thmL; 1752 1753 (*build precondition thm*) 1754 val new_m_thm = CONV_RULE (asm_marker_INTRO_CONV m_base) new_thm; 1755 val new_asm_thm = foldl (fn ((m,a),thm) => 1756 CONV_RULE (RATOR_CONV (RAND_CONV (asm_marker_INTRO_CONV m))) 1757 (DISCH a thm)) new_m_thm (zip mL new_asm) 1758 val new_qasm_thm0 = CONV_RULE (asm_marker_INTRO_CONV m_top) new_asm_thm 1759 val new_qasm_thm = GENL new_fv new_qasm_thm0; 1760 1761 (*use modus ponens*) 1762 val qasm_thm = MP thm2 new_qasm_thm; 1763 1764 (*get rid of markers again*) 1765 val asm_thm_m = SPECL fv qasm_thm; 1766 val asm_thm = CONV_RULE asm_marker_ELIM_CONV asm_thm_m 1767 1768 fun ASM_MARKER_UNDISCH thm = ( 1769 ASM_MARKER_UNDISCH ( 1770 UNDISCH (CONV_RULE (RATOR_CONV (RAND_CONV asm_marker_ELIM_CONV)) thm)) 1771 ) handle HOL_ERR _ => thm 1772 val m_thm = ASM_MARKER_UNDISCH asm_thm; 1773 val thm = CONV_RULE asm_marker_ELIM_CONV m_thm 1774 in 1775 thm 1776 end) 1777end handle UNCHANGED => ALL_TAC (asm,t); 1778 1779fun DISCH_ASM_CONSEQ_CONV_TAC c = DISCH_ASM_CONV_TAC (c CONSEQ_CONV_STRENGTHEN_direction); 1780 1781 1782(* 1783fun CONSEQ_SIMP_CONV impThmL ss eqThmL dir = 1784 DEPTH_CONSEQ_CONV (fn d => ORELSE_CONSEQ_CONV (CONSEQ_TOP_REWRITE_CONV impThmL d) 1785 (SIMP_CONV ss eqThmL)) dir 1786*) 1787 1788 1789(*--------------------------------------------------------------------------- 1790 * EXAMPLES 1791 1792Some theorems about finite maps. 1793 1794open pred_setTheory; 1795open finite_mapTheory; 1796 1797val rewrite_every_thm = 1798prove (``FEVERY P FEMPTY /\ 1799 ((FEVERY P f /\ P (x,y)) ==> 1800 FEVERY P (f |+ (x,y)))``, 1801 1802SIMP_TAC std_ss [FEVERY_DEF, FDOM_FEMPTY, 1803 NOT_IN_EMPTY, FAPPLY_FUPDATE_THM, 1804 FDOM_FUPDATE, IN_INSERT] THEN 1805METIS_TAC[]); 1806 1807 1808val FEXISTS_DEF = Define `!P f. FEXISTS P f = ?x. x IN FDOM f /\ P (x,f ' x)`; 1809 1810val rewrite_exists_thm = 1811prove (``(~(FEXISTS P FEMPTY)) /\ 1812 ((FEXISTS P (f |+ (x,y))) ==> 1813 (FEXISTS P f \/ P (x,y))) 1814 ``, 1815 1816 1817SIMP_TAC std_ss [FEXISTS_DEF, FDOM_FEMPTY, 1818 NOT_IN_EMPTY, FAPPLY_FUPDATE_THM, 1819 FDOM_FUPDATE, IN_INSERT] THEN 1820METIS_TAC[]); 1821 1822 1823 1824You can use the FEVERY-theorem to strengthen expressions: 1825 1826CONSEQ_REWRITE_CONV ([],[rewrite_every_thm],[]) CONSEQ_CONV_STRENGTHEN_direction 1827 ``T ==> FEVERY P (g |+ (3, x) |+ (7,z))`` 1828 1829This should result in: 1830 1831val it = 1832 |- (FEVERY P g /\ P (3,x)) /\ P (7,z) ==> FEVERY P (g |+ (3,x) |+ (7,z)) : 1833 thm 1834 1835 1836It works in substructures as well 1837 1838CONSEQ_REWRITE_CONV ([], [rewrite_every_thm],[]) CONSEQ_CONV_STRENGTHEN_direction 1839 ``!g. ?x. Q (g, x) /\ FEVERY P (g |+ (3, x) |+ (7,z)) \/ (z = 12)`` 1840 1841> val it = 1842 |- (!g. 1843 ?x. Q (g,x) /\ (FEVERY P g /\ P (3,x)) /\ P (7,z) \/ (z = 12)) ==> 1844 !g. ?x. Q (g,x) /\ FEVERY P (g |+ (3,x) |+ (7,z)) \/ (z = 12) : thm 1845 1846 1847You can use the FEXISTS-theorem to weaken them: 1848 1849CONSEQ_REWRITE_CONV ([], [], [rewrite_exists_thm]) CONSEQ_CONV_WEAKEN_direction 1850``FEXISTS P (g |+ (3, x) |+ (7,z))`` 1851val thm = it 1852> val it = 1853 |- FEXISTS P (g |+ (3,x) |+ (7,z)) ==> 1854 (FEXISTS P g \/ P (3,x)) \/ P (7,z) : thm 1855 1856 1857 1858Whether to weaken or strengthen subterms is figured out by their position 1859 1860CONSEQ_REWRITE_CONV ([rewrite_exists_thm,rewrite_every_thm],[],[]) CONSEQ_CONV_WEAKEN_direction 1861 ``FEVERY P (g |+ (3, x) |+ (7,z)) ==> FEXISTS P (g |+ (3, x) |+ (7,z))`` 1862 1863> val it = 1864 |- (FEVERY P (g |+ (3,x) |+ (7,z)) ==> 1865 FEXISTS P (g |+ (3,x) |+ (7,z))) ==> 1866 (FEVERY P g /\ P (3,x)) /\ P (7,z) ==> 1867 (FEXISTS P g \/ P (3,x)) \/ P (7,z) : thm 1868(not a useful theorem, ... :-(() 1869 1870 1871However, you can mark some theorem for just beeing used for strengthening / or weakening. 1872The first list contains theorems used for both, then a list of ones used only 1873for strengthening follows and finally one just for weakening. 1874 1875 1876Full context is automatically used with EXT_CONTEXT_CONSEQ_REWRITE_CONV 1877 1878EXT_CONSEQ_REWRITE_CONV [] [] ([],[rewrite_every_thm],[]) CONSEQ_CONV_STRENGTHEN_direction 1879 ``A /\ ((A ==> B) /\ FEVERY P (g |+ (3, x) |+ (7,z)))`` 1880 1881EXT_CONTEXT_CONSEQ_REWRITE_CONV CONSEQ_CONV_FULL_CONTEXT [] [] ([],[rewrite_every_thm],[]) CONSEQ_CONV_STRENGTHEN_direction 1882 ``A /\ ((A ==> B) /\ FEVERY P (g |+ (3, x) |+ (7,z)))`` 1883 1884val thm = 1885EXT_CONTEXT_CONSEQ_REWRITE_CONV CONSEQ_CONV_FULL_CONTEXT [] [] ([],[rewrite_every_thm],[]) CONSEQ_CONV_STRENGTHEN_direction 1886 ``A \/ ((X A ==> B) /\ FEVERY P (g |+ (3, x) |+ (7,z)))`` 1887 1888EXT_CONSEQ_REWRITE_CONV [] [] ([],[rewrite_every_thm],[]) CONSEQ_CONV_STRENGTHEN_direction 1889 ``A ==> A ==> (A /\ FEVERY P (g |+ (3, x) |+ (7,z)))`` 1890 1891EXT_CONTEXT_CONSEQ_REWRITE_CONV CONSEQ_CONV_FULL_CONTEXT [] [] ([],[rewrite_every_thm],[]) CONSEQ_CONV_STRENGTHEN_direction 1892 ``A ==> A ==> (A /\ FEVERY P (g |+ (3, x) |+ (7,z)))`` 1893 1894 1895(*Variables in Context*) 1896 1897 1898EXT_CONTEXT_CONSEQ_REWRITE_CONV CONSEQ_CONV_FULL_CONTEXT [] [] ([],[],[]) CONSEQ_CONV_STRENGTHEN_direction 1899 ``A ==> if c then A else B`` 1900 1901EXT_CONTEXT_CONSEQ_REWRITE_CONV CONSEQ_CONV_FULL_CONTEXT [] [] ([],[],[]) CONSEQ_CONV_STRENGTHEN_direction 1902 ``A n ==> ?n. A n`` 1903 1904show_assums := true 1905EXT_CONTEXT_CONSEQ_REWRITE_CONV CONSEQ_CONV_FULL_CONTEXT [] [] ([],[],[]) CONSEQ_CONV_STRENGTHEN_direction 1906 ``A n ==> ?m. A n`` 1907 1908Test the recursion 1909 1910val c_def = Define `c (n:num) = T` 1911val c_thm = prove (``!n. (c (SUC n))==> c n``, SIMP_TAC std_ss [c_def]) 1912val c_conv = PART_MATCH (snd o dest_imp) c_thm 1913 1914val cache = mk_DEPTH_CONSEQ_CONV_CACHE () 1915val cache_opt = SOME (K cache, 1916 default_depth_conseq_conv_cache_PRED); 1917 1918val thm = EXT_DEPTH_CONSEQ_CONV CONSEQ_CONV_CONGRUENCE___basic_list true 1919 NONE (SOME 3) true [(true,1,K (K c_conv))] 1920 CONSEQ_CONV_STRENGTHEN_direction ``B /\ A ==> c 0``; 1921 1922 1923fun c d t = if (aconv t ``aaa:bool``) then Feedback.fail() else raise UNCHANGED 1924fun d d t = if (aconv t ``aaa:bool``) then mk_thm ([], ``T ==> aaa``) else raise UNCHANGED 1925 1926 EXT_DEPTH_CONSEQ_CONV CONSEQ_CONV_CONGRUENCE___basic_list NONE (SOME 1) false 1927 [(true, SOME 1, K c)] [] CONSEQ_CONV_STRENGTHEN_direction 1928 ``aaa ==> aaa /\ ccc /\ bbb`` 1929 1930 EXT_DEPTH_CONSEQ_CONV CONSEQ_CONV_CONGRUENCE___basic_list NONE (SOME 1) false 1931 [(false, SOME 1, K c), (false, SOME 1, K d)] [] CONSEQ_CONV_STRENGTHEN_direction 1932 ``aaa ==> aaa /\ ccc /\ bbb`` 1933 1934 1935DEPTH_CONSEQ_CONV c CONSEQ_CONV_STRENGTHEN_direction ``ccc ==> aaa /\ bbb`` 1936 1937*) 1938 1939 1940end 1941