equal
deleted
inserted
replaced
811 end |
811 end |
812 end |
812 end |
813 | _ => no_tac) |
813 | _ => no_tac) |
814 *} |
814 *} |
815 |
815 |
|
816 ML {* |
|
817 val APPLY_RSP1_TAC = |
|
818 Subgoal.FOCUS (fn {concl, asms, context,...} => |
|
819 case ((HOLogic.dest_Trueprop (term_of concl))) of |
|
820 ((R2 $ (f $ x) $ (g $ y))) => |
|
821 let |
|
822 val (asmf, asma) = find_qt_asm (map term_of asms); |
|
823 in |
|
824 if (fastype_of asmf) = (fastype_of f) then no_tac else let |
|
825 val ty_a = fastype_of x; |
|
826 val ty_b = fastype_of asma; |
|
827 val ty_c = range_type (type_of f); |
|
828 (* val ty_d = range_type (type_of asmf);*) |
|
829 val thy = ProofContext.theory_of context; |
|
830 val ty_inst = map (fn x => SOME (ctyp_of thy x)) [ty_a, ty_b, ty_c]; |
|
831 val [R2, f, g, x, y] = map (cterm_of thy) [R2, f, g, x, y]; |
|
832 val t_inst = [NONE, NONE, NONE, SOME R2, SOME f, SOME g, SOME x, SOME y]; |
|
833 val thm = Drule.instantiate' ty_inst t_inst @{thm APPLY_RSP1} |
|
834 (*val _ = tracing (Syntax.string_of_term @{context} (prop_of thm))*) |
|
835 in |
|
836 rtac thm 1 |
|
837 end |
|
838 end |
|
839 | _ => no_tac) |
|
840 *} |
|
841 |
816 |
842 |
817 ML {* |
843 ML {* |
818 fun SOLVES' tac = tac THEN_ALL_NEW (fn _ => no_tac) |
844 fun SOLVES' tac = tac THEN_ALL_NEW (fn _ => no_tac) |
819 *} |
845 *} |
820 |
846 |
998 |
1024 |
999 ML {* |
1025 ML {* |
1000 fun inj_repabs_tac' ctxt rel_refl trans2 = |
1026 fun inj_repabs_tac' ctxt rel_refl trans2 = |
1001 (FIRST' [ |
1027 (FIRST' [ |
1002 inj_repabs_tac_fast ctxt trans2, |
1028 inj_repabs_tac_fast ctxt trans2, |
1003 NDT ctxt "A" (APPLY_RSP_TAC ctxt THEN' |
1029 NDT ctxt "A" (APPLY_RSP1_TAC ctxt THEN' |
1004 (RANGE [SOLVES' (quotient_tac ctxt), SOLVES' (quotient_tac ctxt), |
1030 (RANGE [SOLVES' (quotient_tac ctxt), |
1005 quot_true_tac ctxt (fst o dest_comb), quot_true_tac ctxt (snd o dest_comb)])), |
1031 quot_true_tac ctxt (fst o dest_comb), quot_true_tac ctxt (snd o dest_comb)])), |
1006 NDT ctxt "B" (Cong_Tac.cong_tac @{thm cong} THEN' |
1032 NDT ctxt "B" (Cong_Tac.cong_tac @{thm cong} THEN' |
1007 (RANGE [quot_true_tac ctxt (fst o dest_comb), quot_true_tac ctxt (snd o dest_comb)])), |
1033 (RANGE [quot_true_tac ctxt (fst o dest_comb), quot_true_tac ctxt (snd o dest_comb)])), |
1008 NDT ctxt "C" (rtac @{thm ext} THEN' quot_true_tac ctxt unlam), |
1034 NDT ctxt "C" (rtac @{thm ext} THEN' quot_true_tac ctxt unlam), |
1009 NDT ctxt "E" (atac), |
1035 NDT ctxt "E" (atac), |