746 WEAK_LAMBDA_RES_TAC ctxt |
746 WEAK_LAMBDA_RES_TAC ctxt |
747 ]) |
747 ]) |
748 *} |
748 *} |
749 |
749 |
750 ML {* |
750 ML {* |
751 fun repabs_eq lthy thm constructors rty qty quot_thm reflex_thm trans_thm rsp_thms = |
751 fun repabs lthy thm constructors rty qty quot_thm reflex_thm trans_thm rsp_thms = |
752 let |
752 let |
753 val rt = build_repabs_term lthy thm constructors rty qty; |
753 val rt = build_repabs_term lthy thm constructors rty qty; |
754 val rg = Logic.mk_equals ((Thm.prop_of thm), rt); |
754 val rg = Logic.mk_equals ((Thm.prop_of thm), rt); |
755 fun tac ctxt = (ObjectLogic.full_atomize_tac) THEN' |
755 fun tac ctxt = (ObjectLogic.full_atomize_tac) THEN' |
756 (REPEAT_ALL_NEW (r_mk_comb_tac ctxt rty quot_thm reflex_thm trans_thm rsp_thms)); |
756 (REPEAT_ALL_NEW (r_mk_comb_tac ctxt rty quot_thm reflex_thm trans_thm rsp_thms)); |
757 val cthm = Goal.prove lthy [] [] rg (fn x => tac (#context x) 1); |
757 val cthm = Goal.prove lthy [] [] rg (fn x => tac (#context x) 1); |
758 in |
758 in |
759 (rt, cthm, thm) |
759 @{thm Pure.equal_elim_rule1} OF [cthm, thm] |
760 end |
|
761 *} |
|
762 |
|
763 ML {* |
|
764 fun repabs_eq2 lthy (rt, thm, othm) = |
|
765 let |
|
766 fun tac2 ctxt = |
|
767 (simp_tac ((Simplifier.context ctxt empty_ss) addsimps [symmetric thm])) |
|
768 THEN' (rtac othm); |
|
769 val cthm = Goal.prove lthy [] [] rt (fn x => tac2 (#context x) 1); |
|
770 in |
|
771 cthm |
|
772 end |
760 end |
773 *} |
761 *} |
774 |
762 |
775 section {* Cleaning the goal *} |
763 section {* Cleaning the goal *} |
776 |
764 |
871 |
859 |
872 ML {* |
860 ML {* |
873 fun lift_thm lthy consts rty qty rel rel_eqv rel_refl quot rsp_thms trans2 reps_same t_defs t = let |
861 fun lift_thm lthy consts rty qty rel rel_eqv rel_refl quot rsp_thms trans2 reps_same t_defs t = let |
874 val t_a = atomize_thm t; |
862 val t_a = atomize_thm t; |
875 val t_r = regularize t_a rty rel rel_eqv lthy; |
863 val t_r = regularize t_a rty rel rel_eqv lthy; |
876 val t_t1 = repabs_eq lthy t_r consts rty qty quot rel_refl trans2 rsp_thms; |
864 val t_t = repabs lthy t_r consts rty qty quot rel_refl trans2 rsp_thms; |
877 val t_t2 = repabs_eq2 lthy t_t1; |
|
878 val abs = findabs rty (prop_of t_a); |
865 val abs = findabs rty (prop_of t_a); |
879 val simp_lam_prs_thms = map (make_simp_lam_prs_thm lthy quot) abs; |
866 val simp_lam_prs_thms = map (make_simp_lam_prs_thm lthy quot) abs; |
880 fun simp_lam_prs lthy thm = |
867 fun simp_lam_prs lthy thm = |
881 simp_lam_prs lthy (eqsubst_thm lthy simp_lam_prs_thms thm) |
868 simp_lam_prs lthy (eqsubst_thm lthy simp_lam_prs_thms thm) |
882 handle _ => thm |
869 handle _ => thm |
883 val t_l = simp_lam_prs lthy t_t2; |
870 val t_l = simp_lam_prs lthy t_t; |
884 val t_a = simp_allex_prs lthy quot t_l; |
871 val t_a = simp_allex_prs lthy quot t_l; |
885 val t_defs_sym = add_lower_defs lthy t_defs; |
872 val t_defs_sym = add_lower_defs lthy t_defs; |
886 val t_d = MetaSimplifier.rewrite_rule t_defs_sym t_a; |
873 val t_d = MetaSimplifier.rewrite_rule t_defs_sym t_a; |
887 val t_r = MetaSimplifier.rewrite_rule [reps_same] t_d; |
874 val t_r = MetaSimplifier.rewrite_rule [reps_same] t_d; |
888 in |
875 in |