744 assumes a: "\<And>x y. R1 x y \<Longrightarrow> R2 (f x) (g y)" |
744 assumes a: "\<And>x y. R1 x y \<Longrightarrow> R2 (f x) (g y)" |
745 shows "(R1 ===> R2) f g" |
745 shows "(R1 ===> R2) f g" |
746 using a by (simp add: FUN_REL.simps) |
746 using a by (simp add: FUN_REL.simps) |
747 |
747 |
748 ML {* |
748 ML {* |
749 val LAMBDA_RES_TAC = |
749 val LAMBDA_RES_TAC2 = |
750 SUBGOAL (fn (goal, i) => |
750 Subgoal.FOCUS (fn {concl, ...} => |
751 case goal of |
751 case (term_of concl) of |
752 (_ $ (_ $ (Abs _) $ (Abs _))) => rtac @{thm FUN_REL_I} i |
752 (_ $ (_ $ (Abs _) $ (Abs _))) => rtac @{thm FUN_REL_I} 1 |
753 | _ => no_tac) |
753 | _ => no_tac) |
754 *} |
754 *} |
755 |
755 |
756 ML {* |
756 ML {* |
757 fun WEAK_LAMBDA_RES_TAC ctxt i st = |
757 val WEAK_LAMBDA_RES_TAC2 = |
758 (case (term_of o #concl o fst) (Subgoal.focus ctxt i st) of |
758 Subgoal.FOCUS (fn {concl, ...} => |
759 (_ $ (_ $ _ $ (Abs(_, _, _)))) => |
759 case (term_of concl) of |
760 (EqSubst.eqsubst_tac ctxt [0] @{thms FUN_REL.simps}) THEN' |
760 (_ $ (_ $ _ $ (Abs _))) => rtac @{thm FUN_REL_I} 1 |
761 (rtac @{thm allI}) THEN' (rtac @{thm allI}) THEN' (rtac @{thm impI}) |
761 | (_ $ (_ $ (Abs _) $ _)) => rtac @{thm FUN_REL_I} 1 |
762 | (_ $ (_ $ (Abs(_, _, _)) $ _)) => |
762 | _ => no_tac) |
763 (EqSubst.eqsubst_tac ctxt [0] @{thms FUN_REL.simps}) THEN' |
|
764 (rtac @{thm allI}) THEN' (rtac @{thm allI}) THEN' (rtac @{thm impI}) |
|
765 | _ => fn _ => no_tac) i st |
|
766 *} |
763 *} |
767 |
764 |
768 ML {* (* Legacy *) |
765 ML {* (* Legacy *) |
769 fun needs_lift (rty as Type (rty_s, _)) ty = |
766 fun needs_lift (rty as Type (rty_s, _)) ty = |
770 case ty of |
767 case ty of |
774 |
771 |
775 *} |
772 *} |
776 |
773 |
777 ML {* |
774 ML {* |
778 fun APPLY_RSP_TAC rty = |
775 fun APPLY_RSP_TAC rty = |
779 CSUBGOAL (fn (concl, i) => |
776 Subgoal.FOCUS (fn {concl, ...} => |
780 let |
777 let |
781 val (_ $ (R $ (f $ _) $ (_ $ _))) = term_of concl; |
778 val (_ $ (R $ (f $ _) $ (_ $ _))) = term_of concl; |
782 val pat = Drule.strip_imp_concl (cprop_of @{thm APPLY_RSP}); |
779 val pat = Drule.strip_imp_concl (cprop_of @{thm APPLY_RSP}); |
783 val insts = Thm.match (pat, concl) |
780 val insts = Thm.match (pat, concl) |
784 in |
781 in |
785 if needs_lift rty (type_of f) |
782 if needs_lift rty (type_of f) then |
786 then rtac (Drule.instantiate insts @{thm APPLY_RSP}) i |
783 rtac (Drule.instantiate insts @{thm APPLY_RSP}) 1 |
787 else no_tac |
784 else no_tac |
788 end |
785 end |
789 handle _ => no_tac) |
786 handle _ => no_tac) |
790 *} |
787 *} |
791 |
788 |
820 *} |
817 *} |
821 |
818 |
822 ML {* |
819 ML {* |
823 fun r_mk_comb_tac ctxt rty quot_thms rel_refl trans2 rsp_thms = |
820 fun r_mk_comb_tac ctxt rty quot_thms rel_refl trans2 rsp_thms = |
824 (FIRST' [resolve_tac trans2, |
821 (FIRST' [resolve_tac trans2, |
825 LAMBDA_RES_TAC, |
822 LAMBDA_RES_TAC2 ctxt, |
826 rtac @{thm RES_FORALL_RSP}, |
823 rtac @{thm RES_FORALL_RSP}, |
827 ball_rsp_tac ctxt, |
824 ball_rsp_tac ctxt, |
828 rtac @{thm RES_EXISTS_RSP}, |
825 rtac @{thm RES_EXISTS_RSP}, |
829 bex_rsp_tac ctxt, |
826 bex_rsp_tac ctxt, |
830 resolve_tac rsp_thms, |
827 resolve_tac rsp_thms, |
831 rtac @{thm refl}, |
828 rtac @{thm refl}, |
832 (instantiate_tac @{thm REP_ABS_RSP(1)} ctxt THEN' |
829 (instantiate_tac @{thm REP_ABS_RSP(1)} ctxt THEN' |
833 (RANGE [SOLVES' (quotient_tac quot_thms)])), |
830 (RANGE [SOLVES' (quotient_tac quot_thms)])), |
834 (APPLY_RSP_TAC rty THEN' |
831 (APPLY_RSP_TAC rty ctxt THEN' |
835 (RANGE [SOLVES' (quotient_tac quot_thms), SOLVES' (quotient_tac quot_thms)])), |
832 (RANGE [SOLVES' (quotient_tac quot_thms), SOLVES' (quotient_tac quot_thms)])), |
836 Cong_Tac.cong_tac @{thm cong}, |
833 Cong_Tac.cong_tac @{thm cong}, |
837 rtac @{thm ext}, |
834 rtac @{thm ext}, |
838 resolve_tac rel_refl, |
835 resolve_tac rel_refl, |
839 atac, |
836 atac, |
840 SOLVES' (simp_tac (HOL_ss addsimps @{thms FUN_REL.simps})), |
837 SOLVES' (simp_tac (HOL_ss addsimps @{thms FUN_REL.simps})), |
841 WEAK_LAMBDA_RES_TAC ctxt, |
838 WEAK_LAMBDA_RES_TAC2 ctxt, |
842 CHANGED o (asm_full_simp_tac (HOL_ss addsimps @{thms FUN_REL_EQ}))]) |
839 CHANGED o (asm_full_simp_tac (HOL_ss addsimps @{thms FUN_REL_EQ}))]) |
843 |
840 |
844 fun all_r_mk_comb_tac ctxt rty quot_thms rel_refl trans2 rsp_thms = |
841 fun all_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) |
842 REPEAT_ALL_NEW (r_mk_comb_tac ctxt rty quot_thms rel_refl trans2 rsp_thms) |
846 *} |
843 *} |
876 (* "cong" rule of the of the relation *) |
873 (* "cong" rule of the of the relation *) |
877 (* \<lbrakk>a \<approx> c; b \<approx> d\<rbrakk> \<Longrightarrow> (a \<approx> b) = (c \<approx> d) *) |
874 (* \<lbrakk>a \<approx> c; b \<approx> d\<rbrakk> \<Longrightarrow> (a \<approx> b) = (c \<approx> d) *) |
878 DT ctxt "1" (resolve_tac trans2), |
875 DT ctxt "1" (resolve_tac trans2), |
879 |
876 |
880 (* (R1 ===> R2) (\<lambda>x\<dots>) (\<lambda>\<dots>) \<Longrightarrow> \<lbrakk>R1 x y\<rbrakk> \<Longrightarrow> R2 (\<dots>x) (\<dots>y) *) |
877 (* (R1 ===> R2) (\<lambda>x\<dots>) (\<lambda>\<dots>) \<Longrightarrow> \<lbrakk>R1 x y\<rbrakk> \<Longrightarrow> R2 (\<dots>x) (\<dots>y) *) |
881 DT ctxt "2" (LAMBDA_RES_TAC), |
878 DT ctxt "2" (LAMBDA_RES_TAC2 ctxt), |
882 |
879 |
883 (* R (Ball\<dots>) (Ball\<dots>) \<Longrightarrow> R (\<dots>) (\<dots>) *) |
880 (* R (Ball\<dots>) (Ball\<dots>) \<Longrightarrow> R (\<dots>) (\<dots>) *) |
884 DT ctxt "3" (rtac @{thm RES_FORALL_RSP}), |
881 DT ctxt "3" (rtac @{thm RES_FORALL_RSP}), |
885 |
882 |
886 DT ctxt "4" (ball_rsp_tac ctxt), |
883 DT ctxt "4" (ball_rsp_tac ctxt), |
897 (* observe ---> *) |
894 (* observe ---> *) |
898 DT ctxt "9" ((instantiate_tac @{thm REP_ABS_RSP(1)} ctxt |
895 DT ctxt "9" ((instantiate_tac @{thm REP_ABS_RSP(1)} ctxt |
899 THEN' (RANGE [SOLVES' (quotient_tac quot_thms)]))), |
896 THEN' (RANGE [SOLVES' (quotient_tac quot_thms)]))), |
900 |
897 |
901 (* R (t $ \<dots>) (t' $ \<dots>) \<Longrightarrow> APPLY_RSP provided type of t needs lifting *) |
898 (* R (t $ \<dots>) (t' $ \<dots>) \<Longrightarrow> APPLY_RSP provided type of t needs lifting *) |
902 DT ctxt "A" ((APPLY_RSP_TAC rty THEN' |
899 DT ctxt "A" ((APPLY_RSP_TAC rty ctxt THEN' |
903 (RANGE [SOLVES' (quotient_tac quot_thms), SOLVES' (quotient_tac quot_thms)]))), |
900 (RANGE [SOLVES' (quotient_tac quot_thms), SOLVES' (quotient_tac quot_thms)]))), |
904 |
901 |
905 (* R (t $ \<dots>) (t' $ \<dots>) \<Longrightarrow> Cong provided R = (op =) and t does not need lifting *) |
902 (* R (t $ \<dots>) (t' $ \<dots>) \<Longrightarrow> Cong provided R = (op =) and t does not need lifting *) |
906 DT ctxt "B" (Cong_Tac.cong_tac @{thm cong}), |
903 DT ctxt "B" (Cong_Tac.cong_tac @{thm cong}), |
907 |
904 |
913 |
910 |
914 (* resolving with R x y assumptions *) |
911 (* resolving with R x y assumptions *) |
915 DT ctxt "E" (atac), |
912 DT ctxt "E" (atac), |
916 |
913 |
917 DT ctxt "F" (SOLVES' (simp_tac (HOL_ss addsimps @{thms FUN_REL.simps}))), |
914 DT ctxt "F" (SOLVES' (simp_tac (HOL_ss addsimps @{thms FUN_REL.simps}))), |
918 DT ctxt "G" (WEAK_LAMBDA_RES_TAC ctxt), |
915 DT ctxt "G" (WEAK_LAMBDA_RES_TAC2 ctxt), |
919 DT ctxt "H" (CHANGED o (asm_full_simp_tac (HOL_ss addsimps @{thms FUN_REL_EQ})))]) |
916 DT ctxt "H" (CHANGED o (asm_full_simp_tac (HOL_ss addsimps @{thms FUN_REL_EQ})))]) |
920 |
917 |
921 fun all_r_mk_comb_tac' ctxt rty quot_thms rel_refl trans2 rsp_thms = |
918 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) |
919 REPEAT_ALL_NEW (r_mk_comb_tac' ctxt rty quot_thms rel_refl trans2 rsp_thms) |
923 *} |
920 *} |