equal
deleted
inserted
replaced
713 end |
713 end |
714 *} |
714 *} |
715 |
715 |
716 section {* RepAbs Injection Tactic *} |
716 section {* RepAbs Injection Tactic *} |
717 |
717 |
718 (* TODO: check if it still works with first_order_match *) |
|
719 ML {* |
718 ML {* |
720 fun instantiate_tac thm = |
719 fun instantiate_tac thm = |
721 Subgoal.FOCUS (fn {concl, ...} => |
720 Subgoal.FOCUS (fn {concl, ...} => |
722 let |
721 let |
723 val pat = Drule.strip_imp_concl (cprop_of thm) |
722 val pat = Drule.strip_imp_concl (cprop_of thm) |
769 (_ $ (Const (@{const_name Bex}, _) $ _) |
768 (_ $ (Const (@{const_name Bex}, _) $ _) |
770 $ (Const (@{const_name Bex}, _) $ _)) => rtac @{thm FUN_REL_I} i |
769 $ (Const (@{const_name Bex}, _) $ _)) => rtac @{thm FUN_REL_I} i |
771 | _ => no_tac) |
770 | _ => no_tac) |
772 *} |
771 *} |
773 |
772 |
774 ML {* (* Legacy *) |
|
775 fun needs_lift (rty as Type (rty_s, _)) ty = |
|
776 case ty of |
|
777 Type (s, tys) => (s = rty_s) orelse (exists (needs_lift rty) tys) |
|
778 | _ => false |
|
779 |
|
780 *} |
|
781 |
|
782 definition |
773 definition |
783 "QUOT_TRUE x \<equiv> True" |
774 "QUOT_TRUE x \<equiv> True" |
784 |
775 |
785 ML {* |
776 ML {* |
786 fun find_qt_asm asms = |
777 fun find_qt_asm asms = |
795 | _ => error "find_qt_asm" |
786 | _ => error "find_qt_asm" |
796 end |
787 end |
797 *} |
788 *} |
798 |
789 |
799 ML {* |
790 ML {* |
800 fun APPLY_RSP_TAC rty = |
791 val APPLY_RSP_TAC = |
801 Subgoal.FOCUS (fn {concl, asms, ...} => |
|
802 case ((HOLogic.dest_Trueprop (term_of concl))) of |
|
803 ((_ $ (f $ _) $ (_ $ _))) => |
|
804 let |
|
805 val (asmf, asma) = find_qt_asm (map term_of asms); |
|
806 val pat = Drule.strip_imp_concl (cprop_of @{thm APPLY_RSP}); |
|
807 val insts = Thm.first_order_match (pat, concl) |
|
808 in |
|
809 if (fastype_of asmf) = (fastype_of f) |
|
810 then no_tac |
|
811 else rtac (Drule.instantiate insts @{thm APPLY_RSP}) 1 |
|
812 end |
|
813 | _ => no_tac) |
|
814 *} |
|
815 |
|
816 ML {* |
|
817 val APPLY_RSP_TAC' = |
|
818 Subgoal.FOCUS (fn {concl, asms, context,...} => |
792 Subgoal.FOCUS (fn {concl, asms, context,...} => |
819 case ((HOLogic.dest_Trueprop (term_of concl))) of |
793 case ((HOLogic.dest_Trueprop (term_of concl))) of |
820 ((R2 $ (f $ x) $ (g $ y))) => |
794 ((R2 $ (f $ x) $ (g $ y))) => |
821 let |
795 let |
822 val (asmf, asma) = find_qt_asm (map term_of asms); |
796 val (asmf, asma) = find_qt_asm (map term_of asms); |
958 (* observe ---> *) |
932 (* observe ---> *) |
959 NDT ctxt "9" ((instantiate_tac @{thm REP_ABS_RSP} ctxt |
933 NDT ctxt "9" ((instantiate_tac @{thm REP_ABS_RSP} ctxt |
960 THEN' (RANGE [SOLVES' (quotient_tac ctxt quot_thms)]))), |
934 THEN' (RANGE [SOLVES' (quotient_tac ctxt quot_thms)]))), |
961 |
935 |
962 (* R (t $ \<dots>) (t' $ \<dots>) ----> APPLY_RSP provided type of t needs lifting *) |
936 (* R (t $ \<dots>) (t' $ \<dots>) ----> APPLY_RSP provided type of t needs lifting *) |
963 NDT ctxt "A" (APPLY_RSP_TAC' ctxt THEN' |
937 NDT ctxt "A" (APPLY_RSP_TAC ctxt THEN' |
964 (RANGE [SOLVES' (quotient_tac ctxt quot_thms), SOLVES' (quotient_tac ctxt quot_thms), |
938 (RANGE [SOLVES' (quotient_tac ctxt quot_thms), SOLVES' (quotient_tac ctxt quot_thms), |
965 quot_true_tac ctxt (fst o dest_comb), quot_true_tac ctxt (snd o dest_comb)])), |
939 quot_true_tac ctxt (fst o dest_comb), quot_true_tac ctxt (snd o dest_comb)])), |
966 |
940 |
967 (* (op =) (t $ \<dots>) (t' $ \<dots>) ----> Cong provided type of t does not need lifting *) |
941 (* (op =) (t $ \<dots>) (t' $ \<dots>) ----> Cong provided type of t does not need lifting *) |
968 (* merge with previous tactic *) |
942 (* merge with previous tactic *) |