equal
deleted
inserted
replaced
723 rtac (Drule.instantiate insts thm) 1 |
723 rtac (Drule.instantiate insts thm) 1 |
724 end |
724 end |
725 handle _ => no_tac) |
725 handle _ => no_tac) |
726 *} |
726 *} |
727 |
727 |
728 ML {* |
|
729 fun CHANGED' tac = (fn i => CHANGED (tac i)) |
|
730 *} |
|
731 |
728 |
732 ML {* |
729 ML {* |
733 fun quotient_tac quot_thm = |
730 fun quotient_tac quot_thm = |
734 REPEAT_ALL_NEW (FIRST' [ |
731 REPEAT_ALL_NEW (FIRST' [ |
735 rtac @{thm FUN_QUOTIENT}, |
732 rtac @{thm FUN_QUOTIENT}, |
736 rtac quot_thm, |
733 rtac quot_thm, |
737 rtac @{thm IDENTITY_QUOTIENT}, |
734 rtac @{thm IDENTITY_QUOTIENT}, |
738 (* For functional identity quotients, (op = ---> op =) *) |
735 (* For functional identity quotients, (op = ---> op =) *) |
739 CHANGED' (simp_tac (HOL_ss addsimps @{thms id_simps})) |
736 CHANGED o (simp_tac (HOL_ss addsimps @{thms id_simps})) |
740 ]) |
737 ]) |
741 *} |
738 *} |
742 |
739 |
743 ML {* |
740 ML {* |
744 fun LAMBDA_RES_TAC ctxt i st = |
741 fun LAMBDA_RES_TAC ctxt i st = |
831 rtac @{thm ext}, |
828 rtac @{thm ext}, |
832 rtac reflex_thm, |
829 rtac reflex_thm, |
833 atac, |
830 atac, |
834 SOLVES' (simp_tac (HOL_ss addsimps @{thms FUN_REL.simps})), |
831 SOLVES' (simp_tac (HOL_ss addsimps @{thms FUN_REL.simps})), |
835 WEAK_LAMBDA_RES_TAC ctxt, |
832 WEAK_LAMBDA_RES_TAC ctxt, |
836 CHANGED' (asm_full_simp_tac (HOL_ss addsimps @{thms FUN_REL_EQ})) |
833 CHANGED o (asm_full_simp_tac (HOL_ss addsimps @{thms FUN_REL_EQ})) |
837 ]) |
834 ]) |
838 *} |
835 *} |
839 |
836 |
840 (* |
837 (* |
841 To prove that the regularised theorem implies the abs/rep injected, |
838 To prove that the regularised theorem implies the abs/rep injected, |
880 DT ctxt "C" (rtac @{thm ext}), |
877 DT ctxt "C" (rtac @{thm ext}), |
881 DT ctxt "D" (rtac reflex_thm), |
878 DT ctxt "D" (rtac reflex_thm), |
882 DT ctxt "E" (atac), |
879 DT ctxt "E" (atac), |
883 DT ctxt "F" (SOLVES' (simp_tac (HOL_ss addsimps @{thms FUN_REL.simps}))), |
880 DT ctxt "F" (SOLVES' (simp_tac (HOL_ss addsimps @{thms FUN_REL.simps}))), |
884 DT ctxt "G" (WEAK_LAMBDA_RES_TAC ctxt), |
881 DT ctxt "G" (WEAK_LAMBDA_RES_TAC ctxt), |
885 DT ctxt "H" (CHANGED' (asm_full_simp_tac (HOL_ss addsimps @{thms FUN_REL_EQ}))) |
882 DT ctxt "H" (CHANGED o (asm_full_simp_tac (HOL_ss addsimps @{thms FUN_REL_EQ}))) |
886 ]) |
883 ]) |
887 *} |
884 *} |
888 |
885 |
889 |
886 |
890 |
887 |