810 shows "(R1 ===> R2) f g" |
810 shows "(R1 ===> R2) f g" |
811 using a by (simp add: FUN_REL.simps) |
811 using a by (simp add: FUN_REL.simps) |
812 |
812 |
813 ML {* |
813 ML {* |
814 val LAMBDA_RES_TAC = |
814 val LAMBDA_RES_TAC = |
815 SUBGOAL (fn (goal, i) => |
815 Subgoal.FOCUS (fn {concl, ...} => |
816 case goal of |
816 case (term_of concl) of |
817 (_ $ (_ $ (Abs _) $ (Abs _))) => rtac @{thm FUN_REL_I} i |
817 (_ $ (_ $ (Abs _) $ (Abs _))) => rtac @{thm FUN_REL_I} 1 |
818 | _ => no_tac) |
818 | _ => no_tac) |
819 *} |
819 *} |
820 |
820 |
821 ML {* |
821 ML {* |
822 fun WEAK_LAMBDA_RES_TAC ctxt i st = |
822 val WEAK_LAMBDA_RES_TAC = |
823 (case (term_of o #concl o fst) (Subgoal.focus ctxt i st) of |
823 Subgoal.FOCUS (fn {concl, ...} => |
824 (_ $ (_ $ _ $ (Abs(_, _, _)))) => |
824 case (term_of concl) of |
825 (EqSubst.eqsubst_tac ctxt [0] @{thms FUN_REL.simps}) THEN' |
825 (_ $ (_ $ _ $ (Abs _))) => rtac @{thm FUN_REL_I} 1 |
826 (rtac @{thm allI}) THEN' (rtac @{thm allI}) THEN' (rtac @{thm impI}) |
826 | (_ $ (_ $ (Abs _) $ _)) => rtac @{thm FUN_REL_I} 1 |
827 | (_ $ (_ $ (Abs(_, _, _)) $ _)) => |
827 | _ => no_tac) |
828 (EqSubst.eqsubst_tac ctxt [0] @{thms FUN_REL.simps}) THEN' |
|
829 (rtac @{thm allI}) THEN' (rtac @{thm allI}) THEN' (rtac @{thm impI}) |
|
830 | _ => fn _ => no_tac) i st |
|
831 *} |
828 *} |
832 |
829 |
833 ML {* (* Legacy *) |
830 ML {* (* Legacy *) |
834 fun needs_lift (rty as Type (rty_s, _)) ty = |
831 fun needs_lift (rty as Type (rty_s, _)) ty = |
835 case ty of |
832 case ty of |
837 (s = rty_s) orelse (exists (needs_lift rty) tys) |
834 (s = rty_s) orelse (exists (needs_lift rty) tys) |
838 | _ => false |
835 | _ => false |
839 |
836 |
840 *} |
837 *} |
841 |
838 |
842 (* Doesn't work *) |
839 ML {* |
843 ML {* |
840 fun APPLY_RSP_TAC rty = |
844 fun APPLY_RSP_TAC rty = Subgoal.FOCUS (fn {concl, ...} => |
841 Subgoal.FOCUS (fn {concl, ...} => |
845 let |
842 case (term_of concl) of |
846 val (_ $ (R $ (f $ _) $ (_ $ _))) = term_of concl; |
843 (_ $ (R $ (f $ _) $ (_ $ _))) => |
847 val pat = Drule.strip_imp_concl (cprop_of @{thm APPLY_RSP}); |
844 let |
848 val insts = Thm.match (pat, concl) |
845 val pat = Drule.strip_imp_concl (cprop_of @{thm APPLY_RSP}); |
849 in |
846 val insts = Thm.match (pat, concl) |
850 if needs_lift rty (type_of f) then rtac (Drule.instantiate insts @{thm APPLY_RSP}) 1 |
847 in |
851 else no_tac |
848 if needs_lift rty (fastype_of f) |
852 end |
849 then rtac (Drule.instantiate insts @{thm APPLY_RSP}) 1 |
853 handle _ => no_tac) |
850 else no_tac |
854 *} |
851 end |
855 |
852 | _ => no_tac) |
856 |
853 *} |
857 |
854 |
858 ML {* |
855 ML {* |
859 val ball_rsp_tac = Subgoal.FOCUS (fn {concl, context = ctxt, ...} => |
856 val ball_rsp_tac = |
860 let |
857 Subgoal.FOCUS (fn {concl, context = ctxt, ...} => |
861 val _ $ (_ $ (Const (@{const_name Ball}, _) $ _) $ |
858 case (term_of concl) of |
862 (Const (@{const_name Ball}, _) $ _)) = term_of concl |
859 (_ $ (_ $ (Const (@{const_name Ball}, _) $ _) $ (Const (@{const_name Ball}, _) $ _))) => |
863 in |
860 ((simp_tac (HOL_ss addsimps @{thms FUN_REL.simps})) |
864 ((simp_tac (HOL_ss addsimps @{thms FUN_REL.simps})) |
861 THEN' rtac @{thm allI} THEN' rtac @{thm allI} THEN' rtac @{thm impI} |
865 THEN' rtac @{thm allI} THEN' rtac @{thm allI} THEN' rtac @{thm impI} |
862 THEN' instantiate_tac @{thm RES_FORALL_RSP} ctxt THEN' |
866 THEN' instantiate_tac @{thm RES_FORALL_RSP} ctxt THEN' |
863 (simp_tac (HOL_ss addsimps @{thms FUN_REL.simps}))) 1 |
867 (simp_tac (HOL_ss addsimps @{thms FUN_REL.simps}))) 1 |
864 |_ => no_tac) |
868 end |
865 *} |
869 handle _ => no_tac) |
866 |
870 *} |
867 ML {* |
871 |
868 val bex_rsp_tac = |
872 ML {* |
869 Subgoal.FOCUS (fn {concl, context = ctxt, ...} => |
873 val bex_rsp_tac = Subgoal.FOCUS (fn {concl, context = ctxt, ...} => |
870 case (term_of concl) of |
874 let |
871 (_ $ (_ $ (Const (@{const_name Bex}, _) $ _) $ (Const (@{const_name Bex}, _) $ _))) => |
875 val _ $ (_ $ (Const (@{const_name Bex}, _) $ _) $ |
872 ((simp_tac (HOL_ss addsimps @{thms FUN_REL.simps})) |
876 (Const (@{const_name Bex}, _) $ _)) = term_of concl |
873 THEN' rtac @{thm allI} THEN' rtac @{thm allI} THEN' rtac @{thm impI} |
877 in |
874 THEN' instantiate_tac @{thm RES_EXISTS_RSP} ctxt THEN' |
878 ((simp_tac (HOL_ss addsimps @{thms FUN_REL.simps})) |
875 (simp_tac (HOL_ss addsimps @{thms FUN_REL.simps}))) 1 |
879 THEN' rtac @{thm allI} THEN' rtac @{thm allI} THEN' rtac @{thm impI} |
876 | _ => no_tac) |
880 THEN' instantiate_tac @{thm RES_EXISTS_RSP} ctxt THEN' |
|
881 (simp_tac (HOL_ss addsimps @{thms FUN_REL.simps}))) 1 |
|
882 end |
|
883 handle _ => no_tac) |
|
884 *} |
877 *} |
885 |
878 |
886 ML {* |
879 ML {* |
887 fun SOLVES' tac = tac THEN_ALL_NEW (fn _ => no_tac) |
880 fun SOLVES' tac = tac THEN_ALL_NEW (fn _ => no_tac) |
888 *} |
881 *} |
889 |
882 |
890 ML {* |
883 ML {* |
891 fun r_mk_comb_tac ctxt rty quot_thms rel_refl trans2 rsp_thms = |
884 fun r_mk_comb_tac ctxt rty quot_thms rel_refl trans2 rsp_thms = |
892 (FIRST' [resolve_tac trans2, |
885 (FIRST' [resolve_tac trans2, |
893 LAMBDA_RES_TAC, |
886 LAMBDA_RES_TAC ctxt, |
894 rtac @{thm RES_FORALL_RSP}, |
887 rtac @{thm RES_FORALL_RSP}, |
895 ball_rsp_tac ctxt, |
888 ball_rsp_tac ctxt, |
896 rtac @{thm RES_EXISTS_RSP}, |
889 rtac @{thm RES_EXISTS_RSP}, |
897 bex_rsp_tac ctxt, |
890 bex_rsp_tac ctxt, |
898 resolve_tac rsp_thms, |
891 resolve_tac rsp_thms, |
899 rtac @{thm refl}, |
892 rtac @{thm refl}, |
900 (instantiate_tac @{thm REP_ABS_RSP(1)} ctxt THEN' |
893 (instantiate_tac @{thm REP_ABS_RSP(1)} ctxt THEN' |
901 (RANGE [SOLVES' (quotient_tac quot_thms)])), |
894 (RANGE [SOLVES' (quotient_tac quot_thms)])), |
902 (APPLY_RSP_TAC rty ctxt THEN' |
895 (APPLY_RSP_TAC rty ctxt THEN' |
903 (RANGE [SOLVES' (quotient_tac quot_thms), SOLVES' (quotient_tac quot_thms)])), |
896 (RANGE [SOLVES' (quotient_tac quot_thms), SOLVES' (quotient_tac quot_thms)])), |
904 Cong_Tac.cong_tac @{thm cong}, |
897 Cong_Tac.cong_tac @{thm cong}, |
905 rtac @{thm ext}, |
898 rtac @{thm ext}, |
906 resolve_tac rel_refl, |
899 resolve_tac rel_refl, |
907 atac, |
900 atac, |
944 (* "cong" rule of the of the relation *) |
937 (* "cong" rule of the of the relation *) |
945 (* \<lbrakk>a \<approx> c; b \<approx> d\<rbrakk> \<Longrightarrow> (a \<approx> b) = (c \<approx> d) *) |
938 (* \<lbrakk>a \<approx> c; b \<approx> d\<rbrakk> \<Longrightarrow> (a \<approx> b) = (c \<approx> d) *) |
946 DT ctxt "1" (resolve_tac trans2), |
939 DT ctxt "1" (resolve_tac trans2), |
947 |
940 |
948 (* (R1 ===> R2) (\<lambda>x\<dots>) (\<lambda>\<dots>) \<Longrightarrow> \<lbrakk>R1 x y\<rbrakk> \<Longrightarrow> R2 (\<dots>x) (\<dots>y) *) |
941 (* (R1 ===> R2) (\<lambda>x\<dots>) (\<lambda>\<dots>) \<Longrightarrow> \<lbrakk>R1 x y\<rbrakk> \<Longrightarrow> R2 (\<dots>x) (\<dots>y) *) |
949 DT ctxt "2" (LAMBDA_RES_TAC), |
942 DT ctxt "2" (LAMBDA_RES_TAC ctxt), |
950 |
943 |
951 (* R (Ball\<dots>) (Ball\<dots>) \<Longrightarrow> R (\<dots>) (\<dots>) *) |
944 (* R (Ball\<dots>) (Ball\<dots>) \<Longrightarrow> R (\<dots>) (\<dots>) *) |
952 DT ctxt "3" (rtac @{thm RES_FORALL_RSP}), |
945 DT ctxt "3" (rtac @{thm RES_FORALL_RSP}), |
953 |
946 |
954 DT ctxt "4" (ball_rsp_tac ctxt), |
947 DT ctxt "4" (ball_rsp_tac ctxt), |
961 (* reflexivity of operators arising from Cong_tac *) |
954 (* reflexivity of operators arising from Cong_tac *) |
962 DT ctxt "8" (rtac @{thm refl}), |
955 DT ctxt "8" (rtac @{thm refl}), |
963 |
956 |
964 (* R (\<dots>) (Rep (Abs \<dots>)) \<Longrightarrow> R (\<dots>) (\<dots>) *) |
957 (* R (\<dots>) (Rep (Abs \<dots>)) \<Longrightarrow> R (\<dots>) (\<dots>) *) |
965 (* observe ---> *) |
958 (* observe ---> *) |
966 DT ctxt "9" ((instantiate_tac @{thm REP_ABS_RSP(1)} ctxt |
959 DT ctxt "9" ((instantiate_tac @{thm REP_ABS_RSP(1)} ctxt |
967 THEN' (RANGE [SOLVES' (quotient_tac quot_thms)]))), |
960 THEN' (RANGE [SOLVES' (quotient_tac quot_thms)]))), |
968 |
961 |
969 (* R (t $ \<dots>) (t' $ \<dots>) \<Longrightarrow> APPLY_RSP provided type of t needs lifting *) |
962 (* R (t $ \<dots>) (t' $ \<dots>) \<Longrightarrow> APPLY_RSP provided type of t needs lifting *) |
970 DT ctxt "A" ((APPLY_RSP_TAC rty ctxt THEN' |
963 DT ctxt "A" ((APPLY_RSP_TAC rty ctxt THEN' |
971 (RANGE [SOLVES' (quotient_tac quot_thms), SOLVES' (quotient_tac quot_thms)]))), |
964 (RANGE [SOLVES' (quotient_tac quot_thms), SOLVES' (quotient_tac quot_thms)]))), |
972 |
965 |
973 (* R (t $ \<dots>) (t' $ \<dots>) \<Longrightarrow> Cong provided R = (op =) and t does not need lifting *) |
966 (* R (t $ \<dots>) (t' $ \<dots>) \<Longrightarrow> Cong provided R = (op =) and t does not need lifting *) |
974 DT ctxt "B" (Cong_Tac.cong_tac @{thm cong}), |
967 DT ctxt "B" (Cong_Tac.cong_tac @{thm cong}), |
975 |
968 |