733 end |
733 end |
734 handle _ => no_tac) |
734 handle _ => no_tac) |
735 *} |
735 *} |
736 |
736 |
737 ML {* |
737 ML {* |
738 fun quotient_tac quot_thms = |
738 fun quotient_tac ctxt quot_thms = |
739 REPEAT_ALL_NEW (FIRST' |
739 REPEAT_ALL_NEW (FIRST' |
740 [rtac @{thm FUN_QUOTIENT}, |
740 [rtac @{thm FUN_QUOTIENT}, |
741 resolve_tac quot_thms, |
741 resolve_tac quot_thms, |
742 rtac @{thm IDENTITY_QUOTIENT}, |
742 rtac @{thm IDENTITY_QUOTIENT}, |
743 (* For functional identity quotients, (op = ---> op =) *) |
743 (* For functional identity quotients, (op = ---> op =) *) |
744 (* TODO: think about the other way around, if we need to shorten the relation *) |
744 (* TODO: think about the other way around, if we need to shorten the relation *) |
745 CHANGED o (simp_tac (HOL_ss addsimps @{thms id_simps}))]) |
745 CHANGED o (simp_tac ((Simplifier.context ctxt empty_ss) addsimps @{thms id_simps}))]) |
746 *} |
746 *} |
747 |
747 |
748 lemma FUN_REL_I: |
748 lemma FUN_REL_I: |
749 assumes a: "\<And>x y. R1 x y \<Longrightarrow> R2 (f x) (g y)" |
749 assumes a: "\<And>x y. R1 x y \<Longrightarrow> R2 (f x) (g y)" |
750 shows "(R1 ===> R2) f g" |
750 shows "(R1 ===> R2) f g" |
865 NDT ctxt "8" (rtac @{thm refl}), |
865 NDT ctxt "8" (rtac @{thm refl}), |
866 |
866 |
867 (* R (\<dots>) (Rep (Abs \<dots>)) ----> R (\<dots>) (\<dots>) *) |
867 (* R (\<dots>) (Rep (Abs \<dots>)) ----> R (\<dots>) (\<dots>) *) |
868 (* observe ---> *) |
868 (* observe ---> *) |
869 NDT ctxt "9" ((instantiate_tac @{thm REP_ABS_RSP} ctxt |
869 NDT ctxt "9" ((instantiate_tac @{thm REP_ABS_RSP} ctxt |
870 THEN' (RANGE [SOLVES' (quotient_tac quot_thms)]))), |
870 THEN' (RANGE [SOLVES' (quotient_tac ctxt quot_thms)]))), |
871 |
871 |
872 (* R (t $ \<dots>) (t' $ \<dots>) ----> APPLY_RSP provided type of t needs lifting *) |
872 (* R (t $ \<dots>) (t' $ \<dots>) ----> APPLY_RSP provided type of t needs lifting *) |
873 NDT ctxt "A" ((APPLY_RSP_TAC rty ctxt THEN' |
873 NDT ctxt "A" ((APPLY_RSP_TAC rty ctxt THEN' |
874 (RANGE [SOLVES' (quotient_tac quot_thms), SOLVES' (quotient_tac quot_thms)]))), |
874 (RANGE [SOLVES' (quotient_tac ctxt quot_thms), SOLVES' (quotient_tac ctxt quot_thms)]))), |
875 |
875 |
876 (* (op =) (t $ \<dots>) (t' $ \<dots>) ----> Cong provided type of t does not need lifting *) |
876 (* (op =) (t $ \<dots>) (t' $ \<dots>) ----> Cong provided type of t does not need lifting *) |
877 (* merge with previous tactic *) |
877 (* merge with previous tactic *) |
878 NDT ctxt "B" (Cong_Tac.cong_tac @{thm cong}), |
878 NDT ctxt "B" (Cong_Tac.cong_tac @{thm cong}), |
879 |
879 |
907 section {* Cleaning of the theorem *} |
907 section {* Cleaning of the theorem *} |
908 |
908 |
909 |
909 |
910 (* TODO: This is slow *) |
910 (* TODO: This is slow *) |
911 ML {* |
911 ML {* |
912 fun allex_prs_tac lthy quot = |
912 fun allex_prs_tac ctxt quot = |
913 (EqSubst.eqsubst_tac lthy [0] @{thms all_prs ex_prs}) THEN' (quotient_tac quot) |
913 (EqSubst.eqsubst_tac ctxt [0] @{thms all_prs ex_prs}) THEN' (quotient_tac ctxt quot) |
914 *} |
914 *} |
915 |
915 |
916 (* Rewrites the term with LAMBDA_PRS thm. |
916 (* Rewrites the term with LAMBDA_PRS thm. |
917 |
917 |
918 Replaces: (Rep1 ---> Abs2) (\<lambda>x. Rep2 (f (Abs1 x))) |
918 Replaces: (Rep1 ---> Abs2) (\<lambda>x. Rep2 (f (Abs1 x))) |
944 val tyinst = [SOME cty_a, SOME cty_b, SOME cty_c, SOME cty_d]; |
944 val tyinst = [SOME cty_a, SOME cty_b, SOME cty_c, SOME cty_d]; |
945 val tinst = [NONE, NONE, SOME (cterm_of thy r1), NONE, SOME (cterm_of thy a2)] |
945 val tinst = [NONE, NONE, SOME (cterm_of thy r1), NONE, SOME (cterm_of thy a2)] |
946 val lpi = Drule.instantiate' tyinst tinst @{thm LAMBDA_PRS}; |
946 val lpi = Drule.instantiate' tyinst tinst @{thm LAMBDA_PRS}; |
947 val tac = |
947 val tac = |
948 (compose_tac (false, lpi, 2)) THEN_ALL_NEW |
948 (compose_tac (false, lpi, 2)) THEN_ALL_NEW |
949 (quotient_tac quot_thms); |
949 (quotient_tac ctxt quot_thms); |
950 val gc = Drule.strip_imp_concl (cprop_of lpi); |
950 val gc = Drule.strip_imp_concl (cprop_of lpi); |
951 val t = Goal.prove_internal [] gc (fn _ => tac 1) |
951 val t = Goal.prove_internal [] gc (fn _ => tac 1) |
952 val te = @{thm eq_reflection} OF [t] |
952 val te = @{thm eq_reflection} OF [t] |
953 val ts = MetaSimplifier.rewrite_rule @{thms id_simps} te |
953 val ts = MetaSimplifier.rewrite_rule @{thms id_simps} te |
954 val tl = Thm.lhs_of ts; |
954 val tl = Thm.lhs_of ts; |