683 Logic.mk_equals (rtrm, Syntax.check_term lthy (inj_REPABS lthy (rtrm, qtrm))) |
683 Logic.mk_equals (rtrm, Syntax.check_term lthy (inj_REPABS lthy (rtrm, qtrm))) |
684 *} |
684 *} |
685 |
685 |
686 section {* RepAbs injection tactic *} |
686 section {* RepAbs injection tactic *} |
687 (* |
687 (* |
688 |
|
689 To prove that the regularised theorem implies the abs/rep injected, we first |
688 To prove that the regularised theorem implies the abs/rep injected, we first |
690 atomize it and then try: |
689 atomize it and then try: |
691 |
690 |
692 1) theorems 'trans2' from the appropriate QUOT_TYPE |
691 1) theorems 'trans2' from the appropriate QUOT_TYPE |
693 2) remove lambdas from both sides (LAMBDA_RES_TAC) |
692 2) remove lambdas from both sides (LAMBDA_RES_TAC) |
832 SOLVES' (simp_tac (HOL_ss addsimps @{thms FUN_REL.simps})), |
831 SOLVES' (simp_tac (HOL_ss addsimps @{thms FUN_REL.simps})), |
833 WEAK_LAMBDA_RES_TAC ctxt, |
832 WEAK_LAMBDA_RES_TAC ctxt, |
834 CHANGED' (asm_full_simp_tac (HOL_ss addsimps @{thms FUN_REL_EQ})) |
833 CHANGED' (asm_full_simp_tac (HOL_ss addsimps @{thms FUN_REL_EQ})) |
835 ]) |
834 ]) |
836 *} |
835 *} |
|
836 |
|
837 (* |
|
838 To prove that the regularised theorem implies the abs/rep injected, |
|
839 we try: |
|
840 |
|
841 1) theorems 'trans2' from the appropriate QUOT_TYPE |
|
842 2) remove lambdas from both sides (LAMBDA_RES_TAC) |
|
843 3) remove Ball/Bex from the right hand side |
|
844 4) use user-supplied RSP theorems |
|
845 5) remove rep_abs from the right side |
|
846 6) reflexivity of equality |
|
847 7) split applications of lifted type (apply_rsp) |
|
848 8) split applications of non-lifted type (cong_tac) |
|
849 9) apply extentionality |
|
850 10) reflexivity of the relation |
|
851 11) assumption |
|
852 (Lambdas under respects may have left us some assumptions) |
|
853 12) proving obvious higher order equalities by simplifying fun_rel |
|
854 (not sure if it is still needed?) |
|
855 13) unfolding lambda on one side |
|
856 14) simplifying (= ===> =) for simpler respectfulness |
|
857 |
|
858 *) |
|
859 |
|
860 ML {* |
|
861 fun r_mk_comb_tac' ctxt rty quot_thm reflex_thm trans_thm rsp_thms = |
|
862 REPEAT_ALL_NEW (FIRST' [ |
|
863 (K (print_tac "start")) THEN' (K no_tac), |
|
864 DT ctxt "1" (rtac trans_thm), |
|
865 DT ctxt "2" (LAMBDA_RES_TAC ctxt), |
|
866 DT ctxt "3" (rtac @{thm RES_FORALL_RSP}), |
|
867 DT ctxt "4" (ball_rsp_tac ctxt), |
|
868 DT ctxt "5" (rtac @{thm RES_EXISTS_RSP}), |
|
869 DT ctxt "6" (bex_rsp_tac ctxt), |
|
870 DT ctxt "7" (FIRST' (map rtac rsp_thms)), |
|
871 DT ctxt "8" (rtac refl), |
|
872 DT ctxt "9" ((instantiate_tac @{thm REP_ABS_RSP(1)} ctxt |
|
873 THEN' (RANGE [SOLVES' (quotient_tac quot_thm)]))), |
|
874 DT ctxt "A" ((APPLY_RSP_TAC rty ctxt THEN' |
|
875 (RANGE [SOLVES' (quotient_tac quot_thm), SOLVES' (quotient_tac quot_thm)]))), |
|
876 DT ctxt "B" (Cong_Tac.cong_tac @{thm cong}), |
|
877 DT ctxt "C" (rtac @{thm ext}), |
|
878 DT ctxt "D" (rtac reflex_thm), |
|
879 DT ctxt "E" (atac), |
|
880 DT ctxt "F" (SOLVES' (simp_tac (HOL_ss addsimps @{thms FUN_REL.simps}))), |
|
881 DT ctxt "G" (WEAK_LAMBDA_RES_TAC ctxt), |
|
882 DT ctxt "H" (CHANGED' (asm_full_simp_tac (HOL_ss addsimps @{thms FUN_REL_EQ}))) |
|
883 ]) |
|
884 *} |
|
885 |
837 |
886 |
838 |
887 |
839 (****************************************) |
888 (****************************************) |
840 (* cleaning of the theorem *) |
889 (* cleaning of the theorem *) |
841 (****************************************) |
890 (****************************************) |