644 val trancl_into_rtrancl = @{thm trancl_into_rtrancl}; |
644 val trancl_into_rtrancl = @{thm trancl_into_rtrancl}; |
645 val rtrancl_trancl_trancl = @{thm rtrancl_trancl_trancl}; |
645 val rtrancl_trancl_trancl = @{thm rtrancl_trancl_trancl}; |
646 val trancl_rtrancl_trancl = @{thm trancl_rtrancl_trancl}; |
646 val trancl_rtrancl_trancl = @{thm trancl_rtrancl_trancl}; |
647 val rtrancl_trans = @{thm rtrancl_trans}; |
647 val rtrancl_trans = @{thm rtrancl_trans}; |
648 |
648 |
649 fun decomp (Trueprop $ t) = |
649 fun decomp (@{const Trueprop} $ t) = |
650 let fun dec (Const ("op :", _) $ (Const ("Pair", _) $ a $ b) $ rel ) = |
650 let fun dec (Const ("op :", _) $ (Const ("Pair", _) $ a $ b) $ rel ) = |
651 let fun decr (Const ("Transitive_Closure.rtrancl", _ ) $ r) = (r,"r*") |
651 let fun decr (Const ("Transitive_Closure.rtrancl", _ ) $ r) = (r,"r*") |
652 | decr (Const ("Transitive_Closure.trancl", _ ) $ r) = (r,"r+") |
652 | decr (Const ("Transitive_Closure.trancl", _ ) $ r) = (r,"r+") |
653 | decr r = (r,"r"); |
653 | decr r = (r,"r"); |
654 val (rel,r) = decr (Envir.beta_eta_contract rel); |
654 val (rel,r) = decr (Envir.beta_eta_contract rel); |
655 in SOME (a,b,rel,r) end |
655 in SOME (a,b,rel,r) end |
656 | dec _ = NONE |
656 | dec _ = NONE |
657 in dec t end; |
657 in dec t end |
|
658 | decomp _ = NONE; |
658 |
659 |
659 end); |
660 end); |
660 |
661 |
661 structure Tranclp_Tac = Trancl_Tac_Fun ( |
662 structure Tranclp_Tac = Trancl_Tac_Fun ( |
662 struct |
663 struct |
667 val trancl_into_rtrancl = @{thm tranclp_into_rtranclp}; |
668 val trancl_into_rtrancl = @{thm tranclp_into_rtranclp}; |
668 val rtrancl_trancl_trancl = @{thm rtranclp_tranclp_tranclp}; |
669 val rtrancl_trancl_trancl = @{thm rtranclp_tranclp_tranclp}; |
669 val trancl_rtrancl_trancl = @{thm tranclp_rtranclp_tranclp}; |
670 val trancl_rtrancl_trancl = @{thm tranclp_rtranclp_tranclp}; |
670 val rtrancl_trans = @{thm rtranclp_trans}; |
671 val rtrancl_trans = @{thm rtranclp_trans}; |
671 |
672 |
672 fun decomp (Trueprop $ t) = |
673 fun decomp (@{const Trueprop} $ t) = |
673 let fun dec (rel $ a $ b) = |
674 let fun dec (rel $ a $ b) = |
674 let fun decr (Const ("Transitive_Closure.rtranclp", _ ) $ r) = (r,"r*") |
675 let fun decr (Const ("Transitive_Closure.rtranclp", _ ) $ r) = (r,"r*") |
675 | decr (Const ("Transitive_Closure.tranclp", _ ) $ r) = (r,"r+") |
676 | decr (Const ("Transitive_Closure.tranclp", _ ) $ r) = (r,"r+") |
676 | decr r = (r,"r"); |
677 | decr r = (r,"r"); |
677 val (rel,r) = decr rel; |
678 val (rel,r) = decr rel; |
678 in SOME (a, b, rel, r) end |
679 in SOME (a, b, rel, r) end |
679 | dec _ = NONE |
680 | dec _ = NONE |
680 in dec t end; |
681 in dec t end |
|
682 | decomp _ = NONE; |
681 |
683 |
682 end); |
684 end); |
683 *} |
685 *} |
684 |
686 |
685 declaration {* fn _ => |
687 declaration {* fn _ => |