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