533 (ObjectLogic.full_atomize_tac) THEN' |
533 (ObjectLogic.full_atomize_tac) THEN' |
534 REPEAT_ALL_NEW (FIRST' [ |
534 REPEAT_ALL_NEW (FIRST' [ |
535 rtac rel_refl, |
535 rtac rel_refl, |
536 atac, |
536 atac, |
537 rtac @{thm universal_twice}, |
537 rtac @{thm universal_twice}, |
|
538 (rtac @{thm impI} THEN' atac), |
538 rtac @{thm implication_twice}, |
539 rtac @{thm implication_twice}, |
539 (fn i => CHANGED (asm_full_simp_tac ((Simplifier.context ctxt HOL_ss) addsimps |
540 EqSubst.eqsubst_tac ctxt [0] |
540 [(@{thm equiv_res_forall} OF [rel_eqv]), |
541 [(@{thm equiv_res_forall} OF [rel_eqv]), |
541 (@{thm equiv_res_exists} OF [rel_eqv])]) i)), |
542 (@{thm equiv_res_exists} OF [rel_eqv])], |
542 (rtac @{thm impI} THEN' (asm_full_simp_tac (Simplifier.context ctxt HOL_ss)) THEN' rtac rel_refl), |
543 (rtac @{thm impI} THEN' (asm_full_simp_tac (Simplifier.context ctxt HOL_ss)) THEN' rtac rel_refl), |
543 (rtac @{thm RIGHT_RES_FORALL_REGULAR}) |
544 (rtac @{thm RIGHT_RES_FORALL_REGULAR}) |
544 ]); |
545 ]); |
545 val cthm = Goal.prove lthy [] [] g (fn x => tac (#context x) 1); |
546 val cthm = Goal.prove lthy [] [] g (fn x => tac (#context x) 1); |
546 in |
547 in |
846 fun findaps_all rty tm = |
847 fun findaps_all rty tm = |
847 case tm of |
848 case tm of |
848 Abs(_, T, b) => |
849 Abs(_, T, b) => |
849 findaps_all rty (subst_bound ((Free ("x", T)), b)) |
850 findaps_all rty (subst_bound ((Free ("x", T)), b)) |
850 | (f $ a) => (findaps_all rty f @ findaps_all rty a) |
851 | (f $ a) => (findaps_all rty f @ findaps_all rty a) |
851 | Free (_, (T as (Type (_, (_ :: _))))) => (if needs_lift rty T then [T] else []) |
852 | Free (_, (T as (Type ("fun", (_ :: _))))) => (if needs_lift rty T then [T] else []) |
852 | _ => []; |
853 | _ => []; |
853 fun findaps rty tm = distinct (op =) (findaps_all rty tm) |
854 fun findaps rty tm = distinct (op =) (findaps_all rty tm) |
854 *} |
855 *} |
855 |
856 |
856 ML {* |
857 ML {* |
857 fun make_simp_lam_prs_thm lthy quot_thm typ = |
858 fun make_simp_prs_thm lthy quot_thm thm typ = |
858 let |
859 let |
859 val (_, [lty, rty]) = dest_Type typ; |
860 val (_, [lty, rty]) = dest_Type typ; |
860 val thy = ProofContext.theory_of lthy; |
861 val thy = ProofContext.theory_of lthy; |
861 val (lcty, rcty) = (ctyp_of thy lty, ctyp_of thy rty) |
862 val (lcty, rcty) = (ctyp_of thy lty, ctyp_of thy rty) |
862 val inst = [SOME lcty, NONE, SOME rcty]; |
863 val inst = [SOME lcty, NONE, SOME rcty]; |
863 val lpi = Drule.instantiate' inst [] @{thm LAMBDA_PRS}; |
864 val lpi = Drule.instantiate' inst [] thm; |
864 val tac = |
865 val tac = |
865 (compose_tac (false, @{thm LAMBDA_PRS}, 2)) THEN_ALL_NEW |
866 (compose_tac (false, lpi, 2)) THEN_ALL_NEW |
866 (quotient_tac quot_thm); |
867 (quotient_tac quot_thm); |
867 val t = Goal.prove lthy [] [] (concl_of lpi) (fn _ => tac 1); |
868 val t = Goal.prove lthy [] [] (concl_of lpi) (fn _ => tac 1); |
868 val ts = @{thm HOL.sym} OF [t] |
869 in |
869 in |
870 MetaSimplifier.rewrite_rule [@{thm eq_reflection} OF @{thms id_apply}] t |
870 MetaSimplifier.rewrite_rule [@{thm eq_reflection} OF @{thms id_apply}] ts |
|
871 end |
871 end |
872 *} |
872 *} |
873 |
873 |
874 ML {* |
874 ML {* |
875 fun simp_allex_prs lthy quot thm = |
875 fun simp_allex_prs lthy quot thm = |
927 val consts = lookup_quot_consts defs; |
927 val consts = lookup_quot_consts defs; |
928 val t_a = atomize_thm t; |
928 val t_a = atomize_thm t; |
929 val t_r = regularize t_a rty rel rel_eqv rel_refl lthy; |
929 val t_r = regularize t_a rty rel rel_eqv rel_refl lthy; |
930 val t_t = repabs lthy t_r consts rty qty quot rel_refl trans2 rsp_thms; |
930 val t_t = repabs lthy t_r consts rty qty quot rel_refl trans2 rsp_thms; |
931 val abs = findabs rty (prop_of t_a); |
931 val abs = findabs rty (prop_of t_a); |
932 val simp_lam_prs_thms = map (make_simp_lam_prs_thm lthy quot) abs; |
932 val aps = findaps rty (prop_of t_a); |
933 val t_l = repeat_eqsubst_thm lthy simp_lam_prs_thms t_t; |
933 val app_prs_thms = map (make_simp_prs_thm lthy quot @{thm APP_PRS}) aps; |
|
934 val lam_prs_thms = map (make_simp_prs_thm lthy quot @{thm LAMBDA_PRS}) abs; |
|
935 val t_l = repeat_eqsubst_thm lthy (lam_prs_thms @ app_prs_thms) t_t; |
934 val t_a = simp_allex_prs lthy quot t_l; |
936 val t_a = simp_allex_prs lthy quot t_l; |
935 val defs_sym = add_lower_defs lthy defs; |
937 val defs_sym = add_lower_defs lthy defs; |
936 val t_d = repeat_eqsubst_thm lthy defs_sym t_a; |
938 val t_d = repeat_eqsubst_thm lthy defs_sym t_a; |
937 val t_r = MetaSimplifier.rewrite_rule [reps_same] t_d; |
939 val t_r = MetaSimplifier.rewrite_rule [reps_same] t_d; |
938 in |
940 in |