667 end |
667 end |
668 handle _ => no_tac |
668 handle _ => no_tac |
669 ) |
669 ) |
670 *} |
670 *} |
671 |
671 |
672 |
|
673 |
|
674 ML {* |
672 ML {* |
675 fun quotient_tac quot_thm = |
673 fun quotient_tac quot_thm = |
676 REPEAT_ALL_NEW (FIRST' [ |
674 REPEAT_ALL_NEW (FIRST' [ |
677 rtac @{thm FUN_QUOTIENT}, |
675 rtac @{thm FUN_QUOTIENT}, |
678 rtac quot_thm, |
676 rtac quot_thm, |
679 rtac @{thm IDENTITY_QUOTIENT} |
677 rtac @{thm IDENTITY_QUOTIENT}, |
|
678 (fn i => CHANGED (simp_tac (HOL_ss addsimps @{thms FUN_MAP_I}) i) THEN rtac @{thm IDENTITY_QUOTIENT} i) |
680 ]) |
679 ]) |
681 *} |
680 *} |
682 |
681 |
683 ML {* |
682 ML {* |
684 fun LAMBDA_RES_TAC ctxt i st = |
683 fun LAMBDA_RES_TAC ctxt i st = |
764 atac, |
763 atac, |
765 ( |
764 ( |
766 (simp_tac ((Simplifier.context ctxt HOL_ss) addsimps @{thms FUN_REL.simps})) |
765 (simp_tac ((Simplifier.context ctxt HOL_ss) addsimps @{thms FUN_REL.simps})) |
767 THEN_ALL_NEW (fn _ => no_tac) |
766 THEN_ALL_NEW (fn _ => no_tac) |
768 ), |
767 ), |
769 WEAK_LAMBDA_RES_TAC ctxt |
768 WEAK_LAMBDA_RES_TAC ctxt, |
|
769 (fn i => CHANGED (asm_full_simp_tac (HOL_ss addsimps @{thms FUN_REL_EQ}) i)) |
770 ]) |
770 ]) |
771 *} |
771 *} |
772 |
772 |
773 ML {* |
773 ML {* |
774 fun repabs lthy thm constructors rty qty quot_thm reflex_thm trans_thm rsp_thms = |
774 fun repabs lthy thm constructors rty qty quot_thm reflex_thm trans_thm rsp_thms = |
791 lemma map_id: "map id x = x" |
791 lemma map_id: "map id x = x" |
792 apply (induct x) |
792 apply (induct x) |
793 apply (simp_all add: map.simps) |
793 apply (simp_all add: map.simps) |
794 done |
794 done |
795 |
795 |
|
796 ML {* |
|
797 fun simp_ids lthy thm = |
|
798 thm |
|
799 |> MetaSimplifier.rewrite_rule @{thms id_def_sym} |
|
800 |> repeat_eqsubst_thm lthy @{thms FUN_MAP_I id_apply prod_fun_id map_id} |
|
801 *} |
|
802 |
796 text {* expects atomized definition *} |
803 text {* expects atomized definition *} |
797 ML {* |
804 ML {* |
798 fun add_lower_defs_aux ctxt thm = |
805 fun add_lower_defs_aux lthy thm = |
799 let |
806 let |
800 val e1 = @{thm fun_cong} OF [thm]; |
807 val e1 = @{thm fun_cong} OF [thm]; |
801 val f = eqsubst_thm ctxt @{thms fun_map.simps} e1; |
808 val f = eqsubst_thm lthy @{thms fun_map.simps} e1; |
802 val g = MetaSimplifier.rewrite_rule @{thms id_def_sym} f; |
809 val g = simp_ids lthy f |
803 val h = repeat_eqsubst_thm ctxt @{thms FUN_MAP_I id_apply prod_fun_id map_id} g |
|
804 in |
810 in |
805 thm :: (add_lower_defs_aux ctxt h) |
811 (simp_ids lthy thm) :: (add_lower_defs_aux lthy g) |
806 end |
812 end |
807 handle _ => [thm] |
813 handle _ => [simp_ids lthy thm] |
808 *} |
814 *} |
809 |
815 |
810 ML {* |
816 ML {* |
811 fun add_lower_defs ctxt defs = |
817 fun add_lower_defs lthy def = |
812 let |
818 let |
813 val defs_pre_sym = map symmetric defs |
819 val def_pre_sym = symmetric def |
814 val defs_atom = map atomize_thm defs_pre_sym |
820 val def_atom = atomize_thm def_pre_sym |
815 val defs_all = flat (map (add_lower_defs_aux ctxt) defs_atom) |
821 val defs_all = add_lower_defs_aux lthy def_atom |
816 in |
822 in |
817 map Thm.varifyT defs_all |
823 map Thm.varifyT defs_all |
818 end |
824 end |
819 *} |
825 *} |
820 |
826 |
1010 val abs = findabs rty (prop_of t_a); |
1016 val abs = findabs rty (prop_of t_a); |
1011 val aps = findaps rty (prop_of t_a); |
1017 val aps = findaps rty (prop_of t_a); |
1012 val app_prs_thms = map (applic_prs lthy rty qty absrep) aps; |
1018 val app_prs_thms = map (applic_prs lthy rty qty absrep) aps; |
1013 val lam_prs_thms = map (make_simp_prs_thm lthy quot @{thm LAMBDA_PRS}) abs; |
1019 val lam_prs_thms = map (make_simp_prs_thm lthy quot @{thm LAMBDA_PRS}) abs; |
1014 val t_l = repeat_eqsubst_thm lthy (lam_prs_thms @ app_prs_thms) t_a; |
1020 val t_l = repeat_eqsubst_thm lthy (lam_prs_thms @ app_prs_thms) t_a; |
1015 val defs_sym = add_lower_defs lthy defs; |
1021 val defs_sym = flat (map (add_lower_defs lthy) defs); |
1016 val defs_sym_eq = map (fn x => eq_reflection OF [x]) defs_sym; |
1022 val defs_sym_eq = map (fn x => eq_reflection OF [x]) defs_sym; |
1017 val t_d0 = MetaSimplifier.rewrite_rule defs_sym_eq t_l; |
1023 val t_id = simp_ids lthy t_l; |
|
1024 val t_d0 = MetaSimplifier.rewrite_rule defs_sym_eq t_id; |
1018 val t_d = repeat_eqsubst_thm lthy defs_sym t_d0; |
1025 val t_d = repeat_eqsubst_thm lthy defs_sym t_d0; |
1019 val t_r = MetaSimplifier.rewrite_rule [reps_same] t_d; |
1026 val t_r = MetaSimplifier.rewrite_rule [reps_same] t_d; |
1020 val t_rv = ObjectLogic.rulify t_r |
1027 val t_rv = ObjectLogic.rulify t_r |
1021 in |
1028 in |
1022 Thm.varifyT t_rv |
1029 Thm.varifyT t_rv |