387 |
387 |
388 |
388 |
389 (*** Meta-Rewriting Rules ***) |
389 (*** Meta-Rewriting Rules ***) |
390 |
390 |
391 val reflexive_thm = |
391 val reflexive_thm = |
392 let val cx = cterm_of Sign.proto_pure (Var(("x",0),TVar(("'a",0),logicS))) |
392 let val cx = cterm_of (sign_of ProtoPure.thy) (Var(("x",0),TVar(("'a",0),logicS))) |
393 in Thm.reflexive cx end; |
393 in Thm.reflexive cx end; |
394 |
394 |
395 val symmetric_thm = |
395 val symmetric_thm = |
396 let val xy = read_cterm Sign.proto_pure ("x::'a::logic == y",propT) |
396 let val xy = read_cterm (sign_of ProtoPure.thy) ("x::'a::logic == y",propT) |
397 in standard(Thm.implies_intr_hyps(Thm.symmetric(Thm.assume xy))) end; |
397 in standard(Thm.implies_intr_hyps(Thm.symmetric(Thm.assume xy))) end; |
398 |
398 |
399 val transitive_thm = |
399 val transitive_thm = |
400 let val xy = read_cterm Sign.proto_pure ("x::'a::logic == y",propT) |
400 let val xy = read_cterm (sign_of ProtoPure.thy) ("x::'a::logic == y",propT) |
401 val yz = read_cterm Sign.proto_pure ("y::'a::logic == z",propT) |
401 val yz = read_cterm (sign_of ProtoPure.thy) ("y::'a::logic == z",propT) |
402 val xythm = Thm.assume xy and yzthm = Thm.assume yz |
402 val xythm = Thm.assume xy and yzthm = Thm.assume yz |
403 in standard(Thm.implies_intr yz (Thm.transitive xythm yzthm)) end; |
403 in standard(Thm.implies_intr yz (Thm.transitive xythm yzthm)) end; |
404 |
404 |
405 (** Below, a "conversion" has type cterm -> thm **) |
405 (** Below, a "conversion" has type cterm -> thm **) |
406 |
406 |
407 val refl_implies = reflexive (cterm_of Sign.proto_pure implies); |
407 val refl_implies = reflexive (cterm_of (sign_of ProtoPure.thy) implies); |
408 |
408 |
409 (*In [A1,...,An]==>B, rewrite the selected A's only -- for rewrite_goals_tac*) |
409 (*In [A1,...,An]==>B, rewrite the selected A's only -- for rewrite_goals_tac*) |
410 (*Do not rewrite flex-flex pairs*) |
410 (*Do not rewrite flex-flex pairs*) |
411 fun goals_conv pred cv = |
411 fun goals_conv pred cv = |
412 let fun gconv i ct = |
412 let fun gconv i ct = |
472 def |
472 def |
473 in equal_elim def' th |
473 in equal_elim def' th |
474 end |
474 end |
475 handle THM _ => err th | bind => err th |
475 handle THM _ => err th | bind => err th |
476 in |
476 in |
477 val flexpair_intr = flexpair_inst (symmetric flexpair_def) |
477 val flexpair_intr = flexpair_inst (symmetric ProtoPure.flexpair_def) |
478 and flexpair_elim = flexpair_inst flexpair_def |
478 and flexpair_elim = flexpair_inst ProtoPure.flexpair_def |
479 end; |
479 end; |
480 |
480 |
481 (*Version for flexflex pairs -- this supports lifting.*) |
481 (*Version for flexflex pairs -- this supports lifting.*) |
482 fun flexpair_abs_elim_list cts = |
482 fun flexpair_abs_elim_list cts = |
483 flexpair_intr o equal_abs_elim_list cts o flexpair_elim; |
483 flexpair_intr o equal_abs_elim_list cts o flexpair_elim; |
484 |
484 |
485 |
485 |
486 (*** Some useful meta-theorems ***) |
486 (*** Some useful meta-theorems ***) |
487 |
487 |
488 (*The rule V/V, obtains assumption solving for eresolve_tac*) |
488 (*The rule V/V, obtains assumption solving for eresolve_tac*) |
489 val asm_rl = trivial(read_cterm Sign.proto_pure ("PROP ?psi",propT)); |
489 val asm_rl = trivial(read_cterm (sign_of ProtoPure.thy) ("PROP ?psi",propT)); |
490 |
490 |
491 (*Meta-level cut rule: [| V==>W; V |] ==> W *) |
491 (*Meta-level cut rule: [| V==>W; V |] ==> W *) |
492 val cut_rl = trivial(read_cterm Sign.proto_pure |
492 val cut_rl = trivial(read_cterm (sign_of ProtoPure.thy) |
493 ("PROP ?psi ==> PROP ?theta", propT)); |
493 ("PROP ?psi ==> PROP ?theta", propT)); |
494 |
494 |
495 (*Generalized elim rule for one conclusion; cut_rl with reversed premises: |
495 (*Generalized elim rule for one conclusion; cut_rl with reversed premises: |
496 [| PROP V; PROP V ==> PROP W |] ==> PROP W *) |
496 [| PROP V; PROP V ==> PROP W |] ==> PROP W *) |
497 val revcut_rl = |
497 val revcut_rl = |
498 let val V = read_cterm Sign.proto_pure ("PROP V", propT) |
498 let val V = read_cterm (sign_of ProtoPure.thy) ("PROP V", propT) |
499 and VW = read_cterm Sign.proto_pure ("PROP V ==> PROP W", propT); |
499 and VW = read_cterm (sign_of ProtoPure.thy) ("PROP V ==> PROP W", propT); |
500 in standard (implies_intr V |
500 in standard (implies_intr V |
501 (implies_intr VW |
501 (implies_intr VW |
502 (implies_elim (assume VW) (assume V)))) |
502 (implies_elim (assume VW) (assume V)))) |
503 end; |
503 end; |
504 |
504 |
505 (*for deleting an unwanted assumption*) |
505 (*for deleting an unwanted assumption*) |
506 val thin_rl = |
506 val thin_rl = |
507 let val V = read_cterm Sign.proto_pure ("PROP V", propT) |
507 let val V = read_cterm (sign_of ProtoPure.thy) ("PROP V", propT) |
508 and W = read_cterm Sign.proto_pure ("PROP W", propT); |
508 and W = read_cterm (sign_of ProtoPure.thy) ("PROP W", propT); |
509 in standard (implies_intr V (implies_intr W (assume W))) |
509 in standard (implies_intr V (implies_intr W (assume W))) |
510 end; |
510 end; |
511 |
511 |
512 (* (!!x. PROP ?V) == PROP ?V Allows removal of redundant parameters*) |
512 (* (!!x. PROP ?V) == PROP ?V Allows removal of redundant parameters*) |
513 val triv_forall_equality = |
513 val triv_forall_equality = |
514 let val V = read_cterm Sign.proto_pure ("PROP V", propT) |
514 let val V = read_cterm (sign_of ProtoPure.thy) ("PROP V", propT) |
515 and QV = read_cterm Sign.proto_pure ("!!x::'a. PROP V", propT) |
515 and QV = read_cterm (sign_of ProtoPure.thy) ("!!x::'a. PROP V", propT) |
516 and x = read_cterm Sign.proto_pure ("x", TFree("'a",logicS)); |
516 and x = read_cterm (sign_of ProtoPure.thy) ("x", TFree("'a",logicS)); |
517 in standard (equal_intr (implies_intr QV (forall_elim x (assume QV))) |
517 in standard (equal_intr (implies_intr QV (forall_elim x (assume QV))) |
518 (implies_intr V (forall_intr x (assume V)))) |
518 (implies_intr V (forall_intr x (assume V)))) |
519 end; |
519 end; |
520 |
520 |
521 (* (PROP ?PhiA ==> PROP ?PhiB ==> PROP ?Psi) ==> |
521 (* (PROP ?PhiA ==> PROP ?PhiB ==> PROP ?Psi) ==> |
522 (PROP ?PhiB ==> PROP ?PhiA ==> PROP ?Psi) |
522 (PROP ?PhiB ==> PROP ?PhiA ==> PROP ?Psi) |
523 `thm COMP swap_prems_rl' swaps the first two premises of `thm' |
523 `thm COMP swap_prems_rl' swaps the first two premises of `thm' |
524 *) |
524 *) |
525 val swap_prems_rl = |
525 val swap_prems_rl = |
526 let val cmajor = read_cterm Sign.proto_pure |
526 let val cmajor = read_cterm (sign_of ProtoPure.thy) |
527 ("PROP PhiA ==> PROP PhiB ==> PROP Psi", propT); |
527 ("PROP PhiA ==> PROP PhiB ==> PROP Psi", propT); |
528 val major = assume cmajor; |
528 val major = assume cmajor; |
529 val cminor1 = read_cterm Sign.proto_pure ("PROP PhiA", propT); |
529 val cminor1 = read_cterm (sign_of ProtoPure.thy) ("PROP PhiA", propT); |
530 val minor1 = assume cminor1; |
530 val minor1 = assume cminor1; |
531 val cminor2 = read_cterm Sign.proto_pure ("PROP PhiB", propT); |
531 val cminor2 = read_cterm (sign_of ProtoPure.thy) ("PROP PhiB", propT); |
532 val minor2 = assume cminor2; |
532 val minor2 = assume cminor2; |
533 in standard |
533 in standard |
534 (implies_intr cmajor (implies_intr cminor2 (implies_intr cminor1 |
534 (implies_intr cmajor (implies_intr cminor2 (implies_intr cminor1 |
535 (implies_elim (implies_elim major minor1) minor2)))) |
535 (implies_elim (implies_elim major minor1) minor2)))) |
536 end; |
536 end; |