773 | _ => false |
773 | _ => false |
774 |
774 |
775 *} |
775 *} |
776 |
776 |
777 ML {* |
777 ML {* |
778 fun APPLY_RSP_TAC rty = Subgoal.FOCUS (fn {concl, ...} => |
778 fun APPLY_RSP_TAC rty = |
|
779 CSUBGOAL (fn (concl, i) => |
779 let |
780 let |
780 val (_ $ (R $ (f $ _) $ (_ $ _))) = term_of concl; |
781 val (_ $ (R $ (f $ _) $ (_ $ _))) = term_of concl; |
781 val pat = Drule.strip_imp_concl (cprop_of @{thm APPLY_RSP}); |
782 val pat = Drule.strip_imp_concl (cprop_of @{thm APPLY_RSP}); |
782 val insts = Thm.match (pat, concl) |
783 val insts = Thm.match (pat, concl) |
783 in |
784 in |
784 if needs_lift rty (type_of f) then |
785 if needs_lift rty (type_of f) |
785 rtac (Drule.instantiate insts @{thm APPLY_RSP}) 1 |
786 then rtac (Drule.instantiate insts @{thm APPLY_RSP}) i |
786 else no_tac |
787 else no_tac |
787 end |
788 end |
788 handle _ => no_tac) |
789 handle _ => no_tac) |
789 *} |
790 *} |
790 |
791 |
791 ML {* |
792 ML {* |
792 val ball_rsp_tac = Subgoal.FOCUS (fn {concl, context = ctxt, ...} => |
793 val ball_rsp_tac = |
|
794 Subgoal.FOCUS (fn {concl, context = ctxt, ...} => |
793 let |
795 let |
794 val _ $ (_ $ (Const (@{const_name Ball}, _) $ _) $ |
796 val _ $ (_ $ (Const (@{const_name Ball}, _) $ _) $ |
795 (Const (@{const_name Ball}, _) $ _)) = term_of concl |
797 (Const (@{const_name Ball}, _) $ _)) = term_of concl |
796 in |
798 in |
797 ((simp_tac (HOL_ss addsimps @{thms FUN_REL.simps})) |
799 ((simp_tac (HOL_ss addsimps @{thms FUN_REL.simps})) |
801 end |
803 end |
802 handle _ => no_tac) |
804 handle _ => no_tac) |
803 *} |
805 *} |
804 |
806 |
805 ML {* |
807 ML {* |
806 val bex_rsp_tac = Subgoal.FOCUS (fn {concl, context = ctxt, ...} => |
808 val bex_rsp_tac = |
|
809 Subgoal.FOCUS (fn {concl, context = ctxt, ...} => |
807 let |
810 let |
808 val _ $ (_ $ (Const (@{const_name Bex}, _) $ _) $ |
811 val _ $ (_ $ (Const (@{const_name Bex}, _) $ _) $ |
809 (Const (@{const_name Bex}, _) $ _)) = term_of concl |
812 (Const (@{const_name Bex}, _) $ _)) = term_of concl |
810 in |
813 in |
811 ((simp_tac (HOL_ss addsimps @{thms FUN_REL.simps})) |
814 ((simp_tac (HOL_ss addsimps @{thms FUN_REL.simps})) |
816 handle _ => no_tac) |
819 handle _ => no_tac) |
817 *} |
820 *} |
818 |
821 |
819 ML {* |
822 ML {* |
820 fun r_mk_comb_tac ctxt rty quot_thms rel_refl trans2 rsp_thms = |
823 fun r_mk_comb_tac ctxt rty quot_thms rel_refl trans2 rsp_thms = |
821 (FIRST' [ |
824 (FIRST' [resolve_tac trans2, |
822 resolve_tac trans2, |
825 LAMBDA_RES_TAC, |
823 LAMBDA_RES_TAC, |
826 rtac @{thm RES_FORALL_RSP}, |
824 rtac @{thm RES_FORALL_RSP}, |
827 ball_rsp_tac ctxt, |
825 ball_rsp_tac ctxt, |
828 rtac @{thm RES_EXISTS_RSP}, |
826 rtac @{thm RES_EXISTS_RSP}, |
829 bex_rsp_tac ctxt, |
827 bex_rsp_tac ctxt, |
830 resolve_tac rsp_thms, |
828 resolve_tac rsp_thms, |
831 rtac @{thm refl}, |
829 rtac @{thm refl}, |
832 (instantiate_tac @{thm REP_ABS_RSP(1)} ctxt THEN' |
830 (instantiate_tac @{thm REP_ABS_RSP(1)} ctxt THEN' |
833 (RANGE [SOLVES' (quotient_tac quot_thms)])), |
831 (RANGE [SOLVES' (quotient_tac quot_thms)])), |
834 (APPLY_RSP_TAC rty THEN' |
832 (APPLY_RSP_TAC rty ctxt THEN' |
835 (RANGE [SOLVES' (quotient_tac quot_thms), SOLVES' (quotient_tac quot_thms)])), |
833 (RANGE [SOLVES' (quotient_tac quot_thms), SOLVES' (quotient_tac quot_thms)])), |
836 Cong_Tac.cong_tac @{thm cong}, |
834 Cong_Tac.cong_tac @{thm cong}, |
837 rtac @{thm ext}, |
835 rtac @{thm ext}, |
838 resolve_tac rel_refl, |
836 resolve_tac rel_refl, |
839 atac, |
837 atac, |
840 SOLVES' (simp_tac (HOL_ss addsimps @{thms FUN_REL.simps})), |
838 SOLVES' (simp_tac (HOL_ss addsimps @{thms FUN_REL.simps})), |
841 WEAK_LAMBDA_RES_TAC ctxt, |
839 WEAK_LAMBDA_RES_TAC ctxt, |
842 CHANGED o (asm_full_simp_tac (HOL_ss addsimps @{thms FUN_REL_EQ}))]) |
840 CHANGED o (asm_full_simp_tac (HOL_ss addsimps @{thms FUN_REL_EQ})) |
|
841 ]) |
|
842 |
843 |
843 fun all_r_mk_comb_tac ctxt rty quot_thms rel_refl trans2 rsp_thms = |
844 fun all_r_mk_comb_tac ctxt rty quot_thms rel_refl trans2 rsp_thms = |
844 REPEAT_ALL_NEW (r_mk_comb_tac ctxt rty quot_thms rel_refl trans2 rsp_thms) |
845 REPEAT_ALL_NEW (r_mk_comb_tac ctxt rty quot_thms rel_refl trans2 rsp_thms) |
845 *} |
846 *} |
846 |
847 |
896 (* observe ---> *) |
897 (* observe ---> *) |
897 DT ctxt "9" ((instantiate_tac @{thm REP_ABS_RSP(1)} ctxt |
898 DT ctxt "9" ((instantiate_tac @{thm REP_ABS_RSP(1)} ctxt |
898 THEN' (RANGE [SOLVES' (quotient_tac quot_thms)]))), |
899 THEN' (RANGE [SOLVES' (quotient_tac quot_thms)]))), |
899 |
900 |
900 (* R (t $ \<dots>) (t' $ \<dots>) \<Longrightarrow> APPLY_RSP provided type of t needs lifting *) |
901 (* R (t $ \<dots>) (t' $ \<dots>) \<Longrightarrow> APPLY_RSP provided type of t needs lifting *) |
901 DT ctxt "A" ((APPLY_RSP_TAC rty ctxt THEN' |
902 DT ctxt "A" ((APPLY_RSP_TAC rty THEN' |
902 (RANGE [SOLVES' (quotient_tac quot_thms), SOLVES' (quotient_tac quot_thms)]))), |
903 (RANGE [SOLVES' (quotient_tac quot_thms), SOLVES' (quotient_tac quot_thms)]))), |
903 |
904 |
904 (* R (t $ \<dots>) (t' $ \<dots>) \<Longrightarrow> Cong provided R = (op =) and t does not need lifting *) |
905 (* R (t $ \<dots>) (t' $ \<dots>) \<Longrightarrow> Cong provided R = (op =) and t does not need lifting *) |
905 DT ctxt "B" (Cong_Tac.cong_tac @{thm cong}), |
906 DT ctxt "B" (Cong_Tac.cong_tac @{thm cong}), |
906 |
907 |
913 (* resolving with R x y assumptions *) |
914 (* resolving with R x y assumptions *) |
914 DT ctxt "E" (atac), |
915 DT ctxt "E" (atac), |
915 |
916 |
916 DT ctxt "F" (SOLVES' (simp_tac (HOL_ss addsimps @{thms FUN_REL.simps}))), |
917 DT ctxt "F" (SOLVES' (simp_tac (HOL_ss addsimps @{thms FUN_REL.simps}))), |
917 DT ctxt "G" (WEAK_LAMBDA_RES_TAC ctxt), |
918 DT ctxt "G" (WEAK_LAMBDA_RES_TAC ctxt), |
918 DT ctxt "H" (CHANGED o (asm_full_simp_tac (HOL_ss addsimps @{thms FUN_REL_EQ}))) |
919 DT ctxt "H" (CHANGED o (asm_full_simp_tac (HOL_ss addsimps @{thms FUN_REL_EQ})))]) |
919 ]) |
|
920 |
920 |
921 fun all_r_mk_comb_tac' ctxt rty quot_thms rel_refl trans2 rsp_thms = |
921 fun all_r_mk_comb_tac' ctxt rty quot_thms rel_refl trans2 rsp_thms = |
922 REPEAT_ALL_NEW (r_mk_comb_tac' ctxt rty quot_thms rel_refl trans2 rsp_thms) |
922 REPEAT_ALL_NEW (r_mk_comb_tac' ctxt rty quot_thms rel_refl trans2 rsp_thms) |
923 *} |
923 *} |
924 |
924 |