711 assumes a: "\<And>x y. R1 x y \<Longrightarrow> R2 (f x) (g y)" |
711 assumes a: "\<And>x y. R1 x y \<Longrightarrow> R2 (f x) (g y)" |
712 shows "(R1 ===> R2) f g" |
712 shows "(R1 ===> R2) f g" |
713 using a by (simp add: FUN_REL.simps) |
713 using a by (simp add: FUN_REL.simps) |
714 |
714 |
715 ML {* |
715 ML {* |
716 val LAMBDA_RES_TAC2 = |
716 val LAMBDA_RES_TAC = |
717 Subgoal.FOCUS (fn {concl, ...} => |
717 Subgoal.FOCUS (fn {concl, ...} => |
718 case (term_of concl) of |
718 case (term_of concl) of |
719 (_ $ (_ $ (Abs _) $ (Abs _))) => rtac @{thm FUN_REL_I} 1 |
719 (_ $ (_ $ (Abs _) $ (Abs _))) => rtac @{thm FUN_REL_I} 1 |
720 | _ => no_tac) |
720 | _ => no_tac) |
721 *} |
721 *} |
722 |
722 |
723 ML {* |
723 ML {* |
724 val WEAK_LAMBDA_RES_TAC2 = |
724 val WEAK_LAMBDA_RES_TAC = |
725 Subgoal.FOCUS (fn {concl, ...} => |
725 Subgoal.FOCUS (fn {concl, ...} => |
726 case (term_of concl) of |
726 case (term_of concl) of |
727 (_ $ (_ $ _ $ (Abs _))) => rtac @{thm FUN_REL_I} 1 |
727 (_ $ (_ $ _ $ (Abs _))) => rtac @{thm FUN_REL_I} 1 |
728 | (_ $ (_ $ (Abs _) $ _)) => rtac @{thm FUN_REL_I} 1 |
728 | (_ $ (_ $ (Abs _) $ _)) => rtac @{thm FUN_REL_I} 1 |
729 | _ => no_tac) |
729 | _ => no_tac) |
739 *} |
739 *} |
740 |
740 |
741 ML {* |
741 ML {* |
742 fun APPLY_RSP_TAC rty = |
742 fun APPLY_RSP_TAC rty = |
743 Subgoal.FOCUS (fn {concl, ...} => |
743 Subgoal.FOCUS (fn {concl, ...} => |
744 let |
744 case (term_of concl) of |
745 val (_ $ (R $ (f $ _) $ (_ $ _))) = term_of concl; |
745 (_ $ (R $ (f $ _) $ (_ $ _))) => |
746 val pat = Drule.strip_imp_concl (cprop_of @{thm APPLY_RSP}); |
746 let |
747 val insts = Thm.match (pat, concl) |
747 val pat = Drule.strip_imp_concl (cprop_of @{thm APPLY_RSP}); |
748 in |
748 val insts = Thm.match (pat, concl) |
749 if needs_lift rty (type_of f) then |
749 in |
750 rtac (Drule.instantiate insts @{thm APPLY_RSP}) 1 |
750 if needs_lift rty (fastype_of f) |
751 else no_tac |
751 then rtac (Drule.instantiate insts @{thm APPLY_RSP}) 1 |
752 end |
752 else no_tac |
753 handle _ => no_tac) |
753 end |
|
754 | _ => no_tac) |
754 *} |
755 *} |
755 |
756 |
756 ML {* |
757 ML {* |
757 val ball_rsp_tac = |
758 val ball_rsp_tac = |
758 Subgoal.FOCUS (fn {concl, context = ctxt, ...} => |
759 Subgoal.FOCUS (fn {concl, context = ctxt, ...} => |
759 let |
760 case (term_of concl) of |
760 val _ $ (_ $ (Const (@{const_name Ball}, _) $ _) $ |
761 (_ $ (_ $ (Const (@{const_name Ball}, _) $ _) $ (Const (@{const_name Ball}, _) $ _))) => |
761 (Const (@{const_name Ball}, _) $ _)) = term_of concl |
762 ((simp_tac (HOL_ss addsimps @{thms FUN_REL.simps})) |
762 in |
763 THEN' rtac @{thm allI} THEN' rtac @{thm allI} THEN' rtac @{thm impI} |
763 ((simp_tac (HOL_ss addsimps @{thms FUN_REL.simps})) |
764 THEN' instantiate_tac @{thm RES_FORALL_RSP} ctxt THEN' |
764 THEN' rtac @{thm allI} THEN' rtac @{thm allI} THEN' rtac @{thm impI} |
765 (simp_tac (HOL_ss addsimps @{thms FUN_REL.simps}))) 1 |
765 THEN' instantiate_tac @{thm RES_FORALL_RSP} ctxt THEN' |
766 |_ => no_tac) |
766 (simp_tac (HOL_ss addsimps @{thms FUN_REL.simps}))) 1 |
|
767 end |
|
768 handle _ => no_tac) |
|
769 *} |
767 *} |
770 |
768 |
771 ML {* |
769 ML {* |
772 val bex_rsp_tac = |
770 val bex_rsp_tac = |
773 Subgoal.FOCUS (fn {concl, context = ctxt, ...} => |
771 Subgoal.FOCUS (fn {concl, context = ctxt, ...} => |
774 let |
772 case (term_of concl) of |
775 val _ $ (_ $ (Const (@{const_name Bex}, _) $ _) $ |
773 (_ $ (_ $ (Const (@{const_name Bex}, _) $ _) $ (Const (@{const_name Bex}, _) $ _))) => |
776 (Const (@{const_name Bex}, _) $ _)) = term_of concl |
774 ((simp_tac (HOL_ss addsimps @{thms FUN_REL.simps})) |
777 in |
775 THEN' rtac @{thm allI} THEN' rtac @{thm allI} THEN' rtac @{thm impI} |
778 ((simp_tac (HOL_ss addsimps @{thms FUN_REL.simps})) |
776 THEN' instantiate_tac @{thm RES_EXISTS_RSP} ctxt THEN' |
779 THEN' rtac @{thm allI} THEN' rtac @{thm allI} THEN' rtac @{thm impI} |
777 (simp_tac (HOL_ss addsimps @{thms FUN_REL.simps}))) 1 |
780 THEN' instantiate_tac @{thm RES_EXISTS_RSP} ctxt THEN' |
778 | _ => no_tac) |
781 (simp_tac (HOL_ss addsimps @{thms FUN_REL.simps}))) 1 |
|
782 end |
|
783 handle _ => no_tac) |
|
784 *} |
779 *} |
785 |
780 |
786 ML {* |
781 ML {* |
787 fun r_mk_comb_tac ctxt rty quot_thms rel_refl trans2 rsp_thms = |
782 fun r_mk_comb_tac ctxt rty quot_thms rel_refl trans2 rsp_thms = |
788 (FIRST' [resolve_tac trans2, |
783 (FIRST' [resolve_tac trans2, |
789 LAMBDA_RES_TAC2 ctxt, |
784 LAMBDA_RES_TAC ctxt, |
790 rtac @{thm RES_FORALL_RSP}, |
785 rtac @{thm RES_FORALL_RSP}, |
791 ball_rsp_tac ctxt, |
786 ball_rsp_tac ctxt, |
792 rtac @{thm RES_EXISTS_RSP}, |
787 rtac @{thm RES_EXISTS_RSP}, |
793 bex_rsp_tac ctxt, |
788 bex_rsp_tac ctxt, |
794 resolve_tac rsp_thms, |
789 resolve_tac rsp_thms, |
800 Cong_Tac.cong_tac @{thm cong}, |
795 Cong_Tac.cong_tac @{thm cong}, |
801 rtac @{thm ext}, |
796 rtac @{thm ext}, |
802 resolve_tac rel_refl, |
797 resolve_tac rel_refl, |
803 atac, |
798 atac, |
804 SOLVES' (simp_tac (HOL_ss addsimps @{thms FUN_REL.simps})), |
799 SOLVES' (simp_tac (HOL_ss addsimps @{thms FUN_REL.simps})), |
805 WEAK_LAMBDA_RES_TAC2 ctxt, |
800 WEAK_LAMBDA_RES_TAC ctxt, |
806 CHANGED o (asm_full_simp_tac (HOL_ss addsimps @{thms FUN_REL_EQ}))]) |
801 CHANGED o (asm_full_simp_tac (HOL_ss addsimps @{thms FUN_REL_EQ}))]) |
807 |
802 |
808 fun all_r_mk_comb_tac ctxt rty quot_thms rel_refl trans2 rsp_thms = |
803 fun all_r_mk_comb_tac ctxt rty quot_thms rel_refl trans2 rsp_thms = |
809 REPEAT_ALL_NEW (r_mk_comb_tac ctxt rty quot_thms rel_refl trans2 rsp_thms) |
804 REPEAT_ALL_NEW (r_mk_comb_tac ctxt rty quot_thms rel_refl trans2 rsp_thms) |
810 *} |
805 *} |
840 (* "cong" rule of the of the relation *) |
835 (* "cong" rule of the of the relation *) |
841 (* \<lbrakk>a \<approx> c; b \<approx> d\<rbrakk> \<Longrightarrow> (a \<approx> b) = (c \<approx> d) *) |
836 (* \<lbrakk>a \<approx> c; b \<approx> d\<rbrakk> \<Longrightarrow> (a \<approx> b) = (c \<approx> d) *) |
842 DT ctxt "1" (resolve_tac trans2), |
837 DT ctxt "1" (resolve_tac trans2), |
843 |
838 |
844 (* (R1 ===> R2) (\<lambda>x\<dots>) (\<lambda>\<dots>) \<Longrightarrow> \<lbrakk>R1 x y\<rbrakk> \<Longrightarrow> R2 (\<dots>x) (\<dots>y) *) |
839 (* (R1 ===> R2) (\<lambda>x\<dots>) (\<lambda>\<dots>) \<Longrightarrow> \<lbrakk>R1 x y\<rbrakk> \<Longrightarrow> R2 (\<dots>x) (\<dots>y) *) |
845 DT ctxt "2" (LAMBDA_RES_TAC2 ctxt), |
840 DT ctxt "2" (LAMBDA_RES_TAC ctxt), |
846 |
841 |
847 (* R (Ball\<dots>) (Ball\<dots>) \<Longrightarrow> R (\<dots>) (\<dots>) *) |
842 (* R (Ball\<dots>) (Ball\<dots>) \<Longrightarrow> R (\<dots>) (\<dots>) *) |
848 DT ctxt "3" (rtac @{thm RES_FORALL_RSP}), |
843 DT ctxt "3" (rtac @{thm RES_FORALL_RSP}), |
849 |
844 |
850 DT ctxt "4" (ball_rsp_tac ctxt), |
845 DT ctxt "4" (ball_rsp_tac ctxt), |
877 |
872 |
878 (* resolving with R x y assumptions *) |
873 (* resolving with R x y assumptions *) |
879 DT ctxt "E" (atac), |
874 DT ctxt "E" (atac), |
880 |
875 |
881 DT ctxt "F" (SOLVES' (simp_tac (HOL_ss addsimps @{thms FUN_REL.simps}))), |
876 DT ctxt "F" (SOLVES' (simp_tac (HOL_ss addsimps @{thms FUN_REL.simps}))), |
882 DT ctxt "G" (WEAK_LAMBDA_RES_TAC2 ctxt), |
877 DT ctxt "G" (WEAK_LAMBDA_RES_TAC ctxt), |
883 DT ctxt "H" (CHANGED o (asm_full_simp_tac (HOL_ss addsimps @{thms FUN_REL_EQ})))]) |
878 DT ctxt "H" (CHANGED o (asm_full_simp_tac (HOL_ss addsimps @{thms FUN_REL_EQ})))]) |
884 |
879 |
885 fun all_r_mk_comb_tac' ctxt rty quot_thms rel_refl trans2 rsp_thms = |
880 fun all_r_mk_comb_tac' ctxt rty quot_thms rel_refl trans2 rsp_thms = |
886 REPEAT_ALL_NEW (r_mk_comb_tac' ctxt rty quot_thms rel_refl trans2 rsp_thms) |
881 REPEAT_ALL_NEW (r_mk_comb_tac' ctxt rty quot_thms rel_refl trans2 rsp_thms) |
887 *} |
882 *} |
888 |
883 |
889 ML {* |
|
890 fun get_inj_repabs_tac ctxt rel lhs rhs = |
|
891 let |
|
892 val _ = tracing "input" |
|
893 val _ = tracing ("rel: " ^ Syntax.string_of_term ctxt rel) |
|
894 val _ = tracing ("lhs: " ^ Syntax.string_of_term ctxt lhs) |
|
895 val _ = tracing ("rhs: " ^ Syntax.string_of_term ctxt rhs) |
|
896 in |
|
897 case (rel, lhs, rhs) of |
|
898 (_, l, Const _ $ (Const _ $ r)) (* FIXME: not right_match *) |
|
899 => rtac @{thm REP_ABS_RSP(1)} |
|
900 | (_, Const (@{const_name "Ball"}, _) $ _, |
|
901 Const (@{const_name "Ball"}, _) $ _) |
|
902 => rtac @{thm RES_FORALL_RSP} |
|
903 | _ => K no_tac |
|
904 end |
|
905 *} |
|
906 |
|
907 ML {* |
|
908 fun inj_repabs_tac ctxt = |
|
909 SUBGOAL (fn (goal, i) => |
|
910 (case (HOLogic.dest_Trueprop goal) of |
|
911 (rel $ lhs $ rhs) => get_inj_repabs_tac ctxt rel lhs rhs |
|
912 | _ => K no_tac) i) |
|
913 *} |
|
914 |
884 |
915 section {* Cleaning of the theorem *} |
885 section {* Cleaning of the theorem *} |
916 |
886 |
917 ML {* |
887 ML {* |
918 fun applic_prs lthy absrep (rty, qty) = |
888 fun applic_prs lthy absrep (rty, qty) = |