536 ((prop_of thm), |
536 ((prop_of thm), |
537 (my_reg lthy rel rty (prop_of thm))) |
537 (my_reg lthy rel rty (prop_of thm))) |
538 *} |
538 *} |
539 |
539 |
540 lemma universal_twice: "(\<And>x. (P x \<longrightarrow> Q x)) \<Longrightarrow> ((\<forall>x. P x) \<longrightarrow> (\<forall>x. Q x))" |
540 lemma universal_twice: "(\<And>x. (P x \<longrightarrow> Q x)) \<Longrightarrow> ((\<forall>x. P x) \<longrightarrow> (\<forall>x. Q x))" |
541 apply (auto) |
541 by auto |
542 done |
|
543 |
542 |
544 lemma implication_twice: "(c \<longrightarrow> a) \<Longrightarrow> (a \<Longrightarrow> b \<longrightarrow> d) \<Longrightarrow> (a \<longrightarrow> b) \<longrightarrow> (c \<longrightarrow> d)" |
543 lemma implication_twice: "(c \<longrightarrow> a) \<Longrightarrow> (a \<Longrightarrow> b \<longrightarrow> d) \<Longrightarrow> (a \<longrightarrow> b) \<longrightarrow> (c \<longrightarrow> d)" |
545 apply (auto) |
544 by auto |
546 done |
545 |
|
546 (*lemma equality_twice: "a = c \<Longrightarrow> b = d \<Longrightarrow> (a = b \<longrightarrow> c = d)" |
|
547 by auto*) |
547 |
548 |
548 ML {* |
549 ML {* |
549 fun regularize thm rty rel rel_eqv rel_refl lthy = |
550 fun regularize thm rty rel rel_eqv rel_refl lthy = |
550 let |
551 let |
551 val g = build_regularize_goal thm rty rel lthy; |
552 val g = build_regularize_goal thm rty rel lthy; |
555 rtac rel_refl, |
556 rtac rel_refl, |
556 atac, |
557 atac, |
557 rtac @{thm universal_twice}, |
558 rtac @{thm universal_twice}, |
558 (rtac @{thm impI} THEN' atac), |
559 (rtac @{thm impI} THEN' atac), |
559 rtac @{thm implication_twice}, |
560 rtac @{thm implication_twice}, |
|
561 (*rtac @{thm equality_twice},*) |
560 EqSubst.eqsubst_tac ctxt [0] |
562 EqSubst.eqsubst_tac ctxt [0] |
561 [(@{thm equiv_res_forall} OF [rel_eqv]), |
563 [(@{thm equiv_res_forall} OF [rel_eqv]), |
562 (@{thm equiv_res_exists} OF [rel_eqv])], |
564 (@{thm equiv_res_exists} OF [rel_eqv])], |
563 (rtac @{thm impI} THEN' (asm_full_simp_tac (Simplifier.context ctxt HOL_ss)) THEN' rtac rel_refl), |
565 (rtac @{thm impI} THEN' (asm_full_simp_tac (Simplifier.context ctxt HOL_ss)) THEN' rtac rel_refl), |
564 (rtac @{thm RIGHT_RES_FORALL_REGULAR}) |
566 (rtac @{thm RIGHT_RES_FORALL_REGULAR}) |
706 end |
708 end |
707 handle _ => no_tac |
709 handle _ => no_tac |
708 ) |
710 ) |
709 *} |
711 *} |
710 |
712 |
711 ML {* |
|
712 fun res_forall_rsp_tac ctxt = |
|
713 (simp_tac ((Simplifier.context ctxt HOL_ss) addsimps @{thms FUN_REL.simps})) |
|
714 THEN' rtac @{thm allI} THEN' rtac @{thm allI} THEN' rtac @{thm impI} |
|
715 THEN' instantiate_tac @{thm RES_FORALL_RSP} ctxt THEN' |
|
716 (simp_tac ((Simplifier.context ctxt HOL_ss) addsimps @{thms FUN_REL.simps})) |
|
717 *} |
|
718 |
|
719 ML {* |
|
720 fun res_exists_rsp_tac ctxt = |
|
721 (simp_tac ((Simplifier.context ctxt HOL_ss) addsimps @{thms FUN_REL.simps})) |
|
722 THEN' rtac @{thm allI} THEN' rtac @{thm allI} THEN' rtac @{thm impI} |
|
723 THEN' instantiate_tac @{thm RES_EXISTS_RSP} ctxt THEN' |
|
724 (simp_tac ((Simplifier.context ctxt HOL_ss) addsimps @{thms FUN_REL.simps})) |
|
725 *} |
|
726 |
713 |
727 |
714 |
728 ML {* |
715 ML {* |
729 fun quotient_tac quot_thm = |
716 fun quotient_tac quot_thm = |
730 REPEAT_ALL_NEW (FIRST' [ |
717 REPEAT_ALL_NEW (FIRST' [ |
768 end |
755 end |
769 handle _ => no_tac) |
756 handle _ => no_tac) |
770 *} |
757 *} |
771 |
758 |
772 ML {* |
759 ML {* |
|
760 val res_forall_rsp_tac = Subgoal.FOCUS (fn {concl, context = ctxt, ...} => |
|
761 let |
|
762 val _ $ (_ $ (Const (@{const_name Ball}, _) $ _) $ (Const (@{const_name Ball}, _) $ _)) = term_of concl |
|
763 in |
|
764 ((simp_tac ((Simplifier.context ctxt HOL_ss) addsimps @{thms FUN_REL.simps})) |
|
765 THEN' rtac @{thm allI} THEN' rtac @{thm allI} THEN' rtac @{thm impI} |
|
766 THEN' instantiate_tac @{thm RES_FORALL_RSP} ctxt THEN' |
|
767 (simp_tac ((Simplifier.context ctxt HOL_ss) addsimps @{thms FUN_REL.simps}))) 1 |
|
768 end |
|
769 handle _ => no_tac |
|
770 ) |
|
771 *} |
|
772 |
|
773 ML {* |
|
774 val res_exists_rsp_tac = Subgoal.FOCUS (fn {concl, context = ctxt, ...} => |
|
775 let |
|
776 val _ $ (_ $ (Const (@{const_name Bex}, _) $ _) $ (Const (@{const_name Bex}, _) $ _)) = term_of concl |
|
777 in |
|
778 ((simp_tac ((Simplifier.context ctxt HOL_ss) addsimps @{thms FUN_REL.simps})) |
|
779 THEN' rtac @{thm allI} THEN' rtac @{thm allI} THEN' rtac @{thm impI} |
|
780 THEN' instantiate_tac @{thm RES_EXISTS_RSP} ctxt THEN' |
|
781 (simp_tac ((Simplifier.context ctxt HOL_ss) addsimps @{thms FUN_REL.simps}))) 1 |
|
782 end |
|
783 handle _ => no_tac |
|
784 ) |
|
785 *} |
|
786 |
|
787 ML {* |
773 fun r_mk_comb_tac ctxt rty quot_thm reflex_thm trans_thm rsp_thms = |
788 fun r_mk_comb_tac ctxt rty quot_thm reflex_thm trans_thm rsp_thms = |
774 (FIRST' [ |
789 (FIRST' [ |
775 (* rtac @{thm FUN_QUOTIENT}, |
790 (* rtac @{thm FUN_QUOTIENT}, |
776 rtac quot_thm, |
791 rtac quot_thm, |
777 rtac @{thm IDENTITY_QUOTIENT},*) |
792 rtac @{thm IDENTITY_QUOTIENT},*) |
778 rtac trans_thm, |
793 rtac trans_thm, |
779 LAMBDA_RES_TAC ctxt, |
794 LAMBDA_RES_TAC ctxt, |
780 res_forall_rsp_tac ctxt, |
795 res_forall_rsp_tac ctxt, |
781 res_exists_rsp_tac ctxt, |
796 res_exists_rsp_tac ctxt, |
782 ( |
797 FIRST' (map rtac rsp_thms), |
783 (simp_tac ((Simplifier.context ctxt HOL_ss) addsimps rsp_thms)) |
|
784 THEN_ALL_NEW (fn _ => no_tac) |
|
785 ), |
|
786 (instantiate_tac @{thm REP_ABS_RSP(1)} ctxt THEN' (RANGE [quotient_tac quot_thm])), |
798 (instantiate_tac @{thm REP_ABS_RSP(1)} ctxt THEN' (RANGE [quotient_tac quot_thm])), |
787 rtac refl, |
799 rtac refl, |
788 (* rtac @{thm arg_cong2[of _ _ _ _ "op ="]},*) |
800 (* rtac @{thm arg_cong2[of _ _ _ _ "op ="]},*) |
789 (APPLY_RSP_TAC rty ctxt THEN' (RANGE [quotient_tac quot_thm, quotient_tac quot_thm])), |
801 (APPLY_RSP_TAC rty ctxt THEN' (RANGE [quotient_tac quot_thm, quotient_tac quot_thm])), |
790 Cong_Tac.cong_tac @{thm cong}, |
802 Cong_Tac.cong_tac @{thm cong}, |
891 MetaSimplifier.rewrite_rule [@{thm eq_reflection} OF @{thms id_apply}] t |
903 MetaSimplifier.rewrite_rule [@{thm eq_reflection} OF @{thms id_apply}] t |
892 end |
904 end |
893 *} |
905 *} |
894 |
906 |
895 ML {* |
907 ML {* |
896 fun simp_allex_prs quot thms thm = |
908 fun findallex_all rty qty tm = |
|
909 case tm of |
|
910 Const (@{const_name All}, T) $ (s as (Abs(_, _, b))) => |
|
911 let |
|
912 val (tya, tye) = findallex_all rty qty s |
|
913 in if needs_lift rty T then |
|
914 ((T :: tya), tye) |
|
915 else (tya, tye) end |
|
916 | Const (@{const_name Ex}, T) $ (s as (Abs(_, _, b))) => |
|
917 let |
|
918 val (tya, tye) = findallex_all rty qty s |
|
919 in if needs_lift rty T then |
|
920 (tya, (T :: tye)) |
|
921 else (tya, tye) end |
|
922 | Abs(_, T, b) => |
|
923 findallex_all rty qty (subst_bound ((Free ("x", T)), b)) |
|
924 | f $ a => |
|
925 let |
|
926 val (a1, e1) = findallex_all rty qty f; |
|
927 val (a2, e2) = findallex_all rty qty a; |
|
928 in (a1 @ a2, e1 @ e2) end |
|
929 | _ => ([], []); |
|
930 *} |
|
931 ML {* |
|
932 fun findallex rty qty tm = |
897 let |
933 let |
898 val ts = [@{thm FORALL_PRS} OF [quot], @{thm EXISTS_PRS} OF [quot]] @ thms |
934 val (a, e) = findallex_all rty qty tm; |
899 val sym_ts = map (fn x => @{thm "HOL.sym"} OF [x]) ts; |
935 val (ad, ed) = (map domain_type a, map domain_type e); |
900 val eq_ts = map (fn x => @{thm "eq_reflection"} OF [x]) sym_ts |
936 val (au, eu) = (distinct (op =) ad, distinct (op =) ed) |
901 in |
937 in |
902 MetaSimplifier.rewrite_rule eq_ts thm |
938 (map (old_exchange_ty rty qty) au, map (old_exchange_ty rty qty) eu) |
903 end |
939 end |
904 *} |
940 *} |
|
941 |
|
942 ML {* |
|
943 fun make_allex_prs_thm lthy quot_thm thm typ = |
|
944 let |
|
945 val (_, [lty, rty]) = dest_Type typ; |
|
946 val thy = ProofContext.theory_of lthy; |
|
947 val (lcty, rcty) = (ctyp_of thy lty, ctyp_of thy rty) |
|
948 val inst = [NONE, SOME lcty]; |
|
949 val lpi = Drule.instantiate' inst [] thm; |
|
950 val tac = |
|
951 (compose_tac (false, lpi, 1)) THEN_ALL_NEW |
|
952 (quotient_tac quot_thm); |
|
953 val gc = Drule.strip_imp_concl (cprop_of lpi); |
|
954 val t = Goal.prove_internal [] gc (fn _ => tac 1) |
|
955 val t_noid = MetaSimplifier.rewrite_rule [@{thm eq_reflection} OF @{thms id_apply}] t; |
|
956 val t_sym = @{thm "HOL.sym"} OF [t_noid]; |
|
957 val t_eq = @{thm "eq_reflection"} OF [t_sym] |
|
958 in |
|
959 t_eq |
|
960 end |
|
961 *} |
|
962 |
905 |
963 |
906 ML {* |
964 ML {* |
907 fun lookup_quot_data lthy qty = |
965 fun lookup_quot_data lthy qty = |
908 let |
966 let |
909 val SOME quotdata = find_first (fn x => matches ((#qtyp x), qty)) (quotdata_lookup lthy) |
967 val SOME quotdata = find_first (fn x => matches ((#qtyp x), qty)) (quotdata_lookup lthy) |
945 val (trans2, reps_same, quot) = lookup_quot_thms lthy qty_name; |
1003 val (trans2, reps_same, quot) = lookup_quot_thms lthy qty_name; |
946 val consts = lookup_quot_consts defs; |
1004 val consts = lookup_quot_consts defs; |
947 val t_a = atomize_thm t; |
1005 val t_a = atomize_thm t; |
948 val t_r = regularize t_a rty rel rel_eqv rel_refl lthy; |
1006 val t_r = regularize t_a rty rel rel_eqv rel_refl lthy; |
949 val t_t = repabs lthy t_r consts rty qty quot rel_refl trans2 rsp_thms; |
1007 val t_t = repabs lthy t_r consts rty qty quot rel_refl trans2 rsp_thms; |
|
1008 val (alls, exs) = findallex rty qty (prop_of t_a); |
|
1009 val allthms = map (make_allex_prs_thm lthy quot @{thm FORALL_PRS}) alls |
|
1010 val exthms = map (make_allex_prs_thm lthy quot @{thm EXISTS_PRS}) exs |
|
1011 val t_a = MetaSimplifier.rewrite_rule (allthms @ exthms) t_t |
950 val abs = findabs rty (prop_of t_a); |
1012 val abs = findabs rty (prop_of t_a); |
951 val aps = findaps rty (prop_of t_a); |
1013 val aps = findaps rty (prop_of t_a); |
952 val app_prs_thms = map (make_simp_prs_thm lthy quot @{thm APP_PRS}) aps; |
1014 val app_prs_thms = map (make_simp_prs_thm lthy quot @{thm APP_PRS}) aps; |
953 val lam_prs_thms = map (make_simp_prs_thm lthy quot @{thm LAMBDA_PRS}) abs; |
1015 val lam_prs_thms = map (make_simp_prs_thm lthy quot @{thm LAMBDA_PRS}) abs; |
954 val t_a = simp_allex_prs quot [] t_t; |
|
955 val t_l = repeat_eqsubst_thm lthy (lam_prs_thms @ app_prs_thms) t_a; |
1016 val t_l = repeat_eqsubst_thm lthy (lam_prs_thms @ app_prs_thms) t_a; |
956 val defs_sym = add_lower_defs lthy defs; |
1017 val defs_sym = add_lower_defs lthy defs; |
957 val defs_sym_eq = map (fn x => eq_reflection OF [x]) defs_sym; |
1018 val defs_sym_eq = map (fn x => eq_reflection OF [x]) defs_sym; |
958 val t_d0 = MetaSimplifier.rewrite_rule defs_sym_eq t_l; |
1019 val t_d0 = MetaSimplifier.rewrite_rule defs_sym_eq t_l; |
959 val t_d = repeat_eqsubst_thm lthy defs_sym t_d0; |
1020 val t_d = repeat_eqsubst_thm lthy defs_sym t_d0; |