758 *} |
758 *} |
759 |
759 |
760 ML {* |
760 ML {* |
761 fun r_mk_comb_tac ctxt rty quot_thm reflex_thm trans_thm rsp_thms = |
761 fun r_mk_comb_tac ctxt rty quot_thm reflex_thm trans_thm rsp_thms = |
762 (FIRST' [ |
762 (FIRST' [ |
763 rtac @{thm FUN_QUOTIENT}, |
763 (* rtac @{thm FUN_QUOTIENT}, |
764 rtac quot_thm, |
764 rtac quot_thm, |
765 rtac @{thm IDENTITY_QUOTIENT}, |
765 rtac @{thm IDENTITY_QUOTIENT},*) |
766 rtac trans_thm, |
766 rtac trans_thm, |
767 LAMBDA_RES_TAC ctxt, |
767 LAMBDA_RES_TAC ctxt, |
768 res_forall_rsp_tac ctxt, |
768 res_forall_rsp_tac ctxt, |
769 res_exists_rsp_tac ctxt, |
769 res_exists_rsp_tac ctxt, |
770 ( |
770 ( |
871 val inst = [SOME lcty, NONE, SOME rcty]; |
871 val inst = [SOME lcty, NONE, SOME rcty]; |
872 val lpi = Drule.instantiate' inst [] thm; |
872 val lpi = Drule.instantiate' inst [] thm; |
873 val tac = |
873 val tac = |
874 (compose_tac (false, lpi, 2)) THEN_ALL_NEW |
874 (compose_tac (false, lpi, 2)) THEN_ALL_NEW |
875 (quotient_tac quot_thm); |
875 (quotient_tac quot_thm); |
876 val t = Goal.prove lthy [] [] (concl_of lpi) (fn _ => tac 1); |
876 val gc = Drule.strip_imp_concl (cprop_of lpi); |
|
877 val t = Goal.prove_internal [] gc (fn _ => tac 1) |
877 in |
878 in |
878 MetaSimplifier.rewrite_rule [@{thm eq_reflection} OF @{thms id_apply}] t |
879 MetaSimplifier.rewrite_rule [@{thm eq_reflection} OF @{thms id_apply}] t |
879 end |
880 end |
880 *} |
881 *} |
881 |
882 |
882 ML {* |
883 ML {* |
883 fun simp_allex_prs lthy quot thm = |
884 fun simp_allex_prs quot thms thm = |
884 let |
885 let |
885 val rwf = @{thm FORALL_PRS} OF [quot]; |
886 val ts = [@{thm FORALL_PRS} OF [quot], @{thm EXISTS_PRS} OF [quot]] @ thms |
886 val rwfs = @{thm "HOL.sym"} OF [rwf]; |
887 val sym_ts = map (fn x => @{thm "HOL.sym"} OF [x]) ts; |
887 val rwe = @{thm EXISTS_PRS} OF [quot]; |
888 val eq_ts = map (fn x => @{thm "eq_reflection"} OF [x]) sym_ts |
888 val rwes = @{thm "HOL.sym"} OF [rwe] |
|
889 in |
889 in |
890 (simp_allex_prs lthy quot (eqsubst_thm lthy [rwfs, rwes] thm)) |
890 MetaSimplifier.rewrite_rule eq_ts thm |
891 end |
891 end |
892 handle _ => thm |
|
893 *} |
892 *} |
894 |
893 |
895 ML {* |
894 ML {* |
896 fun lookup_quot_data lthy qty = |
895 fun lookup_quot_data lthy qty = |
897 let |
896 let |
938 val t_t = repabs lthy t_r consts rty qty quot rel_refl trans2 rsp_thms; |
937 val t_t = repabs lthy t_r consts rty qty quot rel_refl trans2 rsp_thms; |
939 val abs = findabs rty (prop_of t_a); |
938 val abs = findabs rty (prop_of t_a); |
940 val aps = findaps rty (prop_of t_a); |
939 val aps = findaps rty (prop_of t_a); |
941 val app_prs_thms = map (make_simp_prs_thm lthy quot @{thm APP_PRS}) aps; |
940 val app_prs_thms = map (make_simp_prs_thm lthy quot @{thm APP_PRS}) aps; |
942 val lam_prs_thms = map (make_simp_prs_thm lthy quot @{thm LAMBDA_PRS}) abs; |
941 val lam_prs_thms = map (make_simp_prs_thm lthy quot @{thm LAMBDA_PRS}) abs; |
943 val t_l = repeat_eqsubst_thm lthy (lam_prs_thms @ app_prs_thms) t_t; |
942 val t_a = simp_allex_prs quot [] t_t; |
944 val t_a = simp_allex_prs lthy quot t_l; |
943 val t_l = repeat_eqsubst_thm lthy (lam_prs_thms @ app_prs_thms) t_a; |
945 val defs_sym = add_lower_defs lthy defs; |
944 val defs_sym = add_lower_defs lthy defs; |
946 val t_d = repeat_eqsubst_thm lthy defs_sym t_a; |
945 val defs_sym_eq = map (fn x => eq_reflection OF [x]) defs_sym; |
|
946 val t_d0 = MetaSimplifier.rewrite_rule defs_sym_eq t_l; |
|
947 val t_d = repeat_eqsubst_thm lthy defs_sym t_d0; |
947 val t_r = MetaSimplifier.rewrite_rule [reps_same] t_d; |
948 val t_r = MetaSimplifier.rewrite_rule [reps_same] t_d; |
948 in |
949 in |
949 ObjectLogic.rulify t_r |
950 ObjectLogic.rulify t_r |
950 end |
951 end |
951 *} |
952 *} |