504 if (needs_lift rty T) then |
504 if (needs_lift rty T) then |
505 (mk_bex ty1) $ (mk_resp ty2 $ rrel) $ (apply_subt (my_reg lthy rel rty) t) |
505 (mk_bex ty1) $ (mk_resp ty2 $ rrel) $ (apply_subt (my_reg lthy rel rty) t) |
506 else |
506 else |
507 Const (@{const_name "Ex"}, ty) $ apply_subt (my_reg lthy rel rty) t |
507 Const (@{const_name "Ex"}, ty) $ apply_subt (my_reg lthy rel rty) t |
508 end |
508 end |
|
509 | Const (@{const_name "op ="}, ty) $ t => |
|
510 if needs_lift rty (fastype_of t) then |
|
511 (tyRel (fastype_of t) rty rel lthy) $ t |
|
512 else Const (@{const_name "op ="}, ty) $ (my_reg lthy rel rty t) |
509 | t1 $ t2 => (my_reg lthy rel rty t1) $ (my_reg lthy rel rty t2) |
513 | t1 $ t2 => (my_reg lthy rel rty t1) $ (my_reg lthy rel rty t2) |
510 | _ => trm |
514 | _ => trm |
511 *} |
515 *} |
512 |
516 |
513 text {* Assumes that the given theorem is atomized *} |
517 text {* Assumes that the given theorem is atomized *} |
516 Logic.mk_implies |
520 Logic.mk_implies |
517 ((prop_of thm), |
521 ((prop_of thm), |
518 (my_reg lthy rel rty (prop_of thm))) |
522 (my_reg lthy rel rty (prop_of thm))) |
519 *} |
523 *} |
520 |
524 |
521 ML {* |
525 lemma universal_twice: "(\<And>x. (P x \<longrightarrow> Q x)) \<Longrightarrow> ((\<forall>x. P x) \<longrightarrow> (\<forall>x. Q x))" |
522 fun regularize thm rty rel rel_eqv lthy = |
526 apply (auto) |
|
527 done |
|
528 |
|
529 lemma implication_twice: "(c \<longrightarrow> a) \<Longrightarrow> (a \<Longrightarrow> b \<longrightarrow> d) \<Longrightarrow> (a \<longrightarrow> b) \<longrightarrow> (c \<longrightarrow> d)" |
|
530 apply (auto) |
|
531 done |
|
532 |
|
533 ML {* |
|
534 fun regularize thm rty rel rel_eqv rel_refl lthy = |
523 let |
535 let |
524 val g = build_regularize_goal thm rty rel lthy; |
536 val g = build_regularize_goal thm rty rel lthy; |
525 fun tac ctxt = |
537 fun tac ctxt = |
526 (asm_full_simp_tac ((Simplifier.context ctxt HOL_ss) addsimps |
538 (ObjectLogic.full_atomize_tac) THEN' |
|
539 REPEAT_ALL_NEW (FIRST' [ |
|
540 rtac rel_refl, |
|
541 atac, |
|
542 rtac @{thm universal_twice}, |
|
543 (rtac @{thm impI} THEN' atac), |
|
544 rtac @{thm implication_twice}, |
|
545 EqSubst.eqsubst_tac ctxt [0] |
527 [(@{thm equiv_res_forall} OF [rel_eqv]), |
546 [(@{thm equiv_res_forall} OF [rel_eqv]), |
528 (@{thm equiv_res_exists} OF [rel_eqv])])) THEN_ALL_NEW |
547 (@{thm equiv_res_exists} OF [rel_eqv])], |
529 (((rtac @{thm RIGHT_RES_FORALL_REGULAR}) THEN' (RANGE [fn _ => all_tac, atac]) THEN' |
548 (rtac @{thm impI} THEN' (asm_full_simp_tac (Simplifier.context ctxt HOL_ss)) THEN' rtac rel_refl), |
530 (MetisTools.metis_tac ctxt [])) ORELSE' (MetisTools.metis_tac ctxt [])); |
549 (rtac @{thm RIGHT_RES_FORALL_REGULAR}) |
|
550 ]); |
531 val cthm = Goal.prove lthy [] [] g (fn x => tac (#context x) 1); |
551 val cthm = Goal.prove lthy [] [] g (fn x => tac (#context x) 1); |
532 in |
552 in |
533 cthm OF [thm] |
553 cthm OF [thm] |
534 end |
554 end |
535 *} |
555 *} |
549 Type (s, tys) => Type (s, map (old_exchange_ty rty qty) tys) |
569 Type (s, tys) => Type (s, map (old_exchange_ty rty qty) tys) |
550 | _ => ty |
570 | _ => ty |
551 ) |
571 ) |
552 *} |
572 *} |
553 |
573 |
554 ML {* make_const_def *} |
|
555 |
|
556 ML {* |
574 ML {* |
557 fun old_get_fun flag rty qty lthy ty = |
575 fun old_get_fun flag rty qty lthy ty = |
558 get_fun flag [(qty, rty)] lthy ty |
576 get_fun flag [(qty, rty)] lthy ty |
559 *} |
577 |
560 |
|
561 ML {* |
|
562 fun old_make_const_def nconst_bname otrm mx rty qty lthy = |
578 fun old_make_const_def nconst_bname otrm mx rty qty lthy = |
563 make_const_def nconst_bname otrm mx [(qty, rty)] lthy |
579 make_const_def nconst_bname otrm mx [(qty, rty)] lthy |
564 *} |
580 *} |
565 |
581 |
566 text {* Does the same as 'subst' in a given prop or theorem *} |
582 text {* Does the same as 'subst' in a given prop or theorem *} |
836 fun findaps_all rty tm = |
852 fun findaps_all rty tm = |
837 case tm of |
853 case tm of |
838 Abs(_, T, b) => |
854 Abs(_, T, b) => |
839 findaps_all rty (subst_bound ((Free ("x", T)), b)) |
855 findaps_all rty (subst_bound ((Free ("x", T)), b)) |
840 | (f $ a) => (findaps_all rty f @ findaps_all rty a) |
856 | (f $ a) => (findaps_all rty f @ findaps_all rty a) |
841 | Free (_, (T as (Type (_, (_ :: _))))) => (if needs_lift rty T then [T] else []) |
857 | Free (_, (T as (Type ("fun", (_ :: _))))) => (if needs_lift rty T then [T] else []) |
842 | _ => []; |
858 | _ => []; |
843 fun findaps rty tm = distinct (op =) (findaps_all rty tm) |
859 fun findaps rty tm = distinct (op =) (findaps_all rty tm) |
844 *} |
860 *} |
845 |
861 |
846 ML {* |
862 ML {* |
847 fun make_simp_lam_prs_thm lthy quot_thm typ = |
863 fun make_simp_prs_thm lthy quot_thm thm typ = |
848 let |
864 let |
849 val (_, [lty, rty]) = dest_Type typ; |
865 val (_, [lty, rty]) = dest_Type typ; |
850 val thy = ProofContext.theory_of lthy; |
866 val thy = ProofContext.theory_of lthy; |
851 val (lcty, rcty) = (ctyp_of thy lty, ctyp_of thy rty) |
867 val (lcty, rcty) = (ctyp_of thy lty, ctyp_of thy rty) |
852 val inst = [SOME lcty, NONE, SOME rcty]; |
868 val inst = [SOME lcty, NONE, SOME rcty]; |
853 val lpi = Drule.instantiate' inst [] @{thm LAMBDA_PRS}; |
869 val lpi = Drule.instantiate' inst [] thm; |
854 val tac = |
870 val tac = |
855 (compose_tac (false, @{thm LAMBDA_PRS}, 2)) THEN_ALL_NEW |
871 (compose_tac (false, lpi, 2)) THEN_ALL_NEW |
856 (quotient_tac quot_thm); |
872 (quotient_tac quot_thm); |
857 val t = Goal.prove lthy [] [] (concl_of lpi) (fn _ => tac 1); |
873 val t = Goal.prove lthy [] [] (concl_of lpi) (fn _ => tac 1); |
858 val ts = @{thm HOL.sym} OF [t] |
874 in |
859 in |
875 MetaSimplifier.rewrite_rule [@{thm eq_reflection} OF @{thms id_apply}] t |
860 MetaSimplifier.rewrite_rule [@{thm eq_reflection} OF @{thms id_apply}] ts |
|
861 end |
876 end |
862 *} |
877 *} |
863 |
878 |
864 ML {* |
879 ML {* |
865 fun simp_allex_prs lthy quot thm = |
880 fun simp_allex_prs lthy quot thm = |
914 fun lift_thm lthy qty qty_name rsp_thms defs t = let |
929 fun lift_thm lthy qty qty_name rsp_thms defs t = let |
915 val (rty, rel, rel_refl, rel_eqv) = lookup_quot_data lthy qty; |
930 val (rty, rel, rel_refl, rel_eqv) = lookup_quot_data lthy qty; |
916 val (trans2, reps_same, quot) = lookup_quot_thms lthy qty_name; |
931 val (trans2, reps_same, quot) = lookup_quot_thms lthy qty_name; |
917 val consts = lookup_quot_consts defs; |
932 val consts = lookup_quot_consts defs; |
918 val t_a = atomize_thm t; |
933 val t_a = atomize_thm t; |
919 val t_r = regularize t_a rty rel rel_eqv lthy; |
934 val t_r = regularize t_a rty rel rel_eqv rel_refl lthy; |
920 val t_t = repabs lthy t_r consts rty qty quot rel_refl trans2 rsp_thms; |
935 val t_t = repabs lthy t_r consts rty qty quot rel_refl trans2 rsp_thms; |
921 val abs = findabs rty (prop_of t_a); |
936 val abs = findabs rty (prop_of t_a); |
922 val simp_lam_prs_thms = map (make_simp_lam_prs_thm lthy quot) abs; |
937 val aps = findaps rty (prop_of t_a); |
923 val t_l = repeat_eqsubst_thm lthy simp_lam_prs_thms t_t; |
938 val app_prs_thms = map (make_simp_prs_thm lthy quot @{thm APP_PRS}) aps; |
|
939 val lam_prs_thms = map (make_simp_prs_thm lthy quot @{thm LAMBDA_PRS}) abs; |
|
940 val t_l = repeat_eqsubst_thm lthy (lam_prs_thms @ app_prs_thms) t_t; |
924 val t_a = simp_allex_prs lthy quot t_l; |
941 val t_a = simp_allex_prs lthy quot t_l; |
925 val defs_sym = add_lower_defs lthy defs; |
942 val defs_sym = add_lower_defs lthy defs; |
926 val t_d = repeat_eqsubst_thm lthy defs_sym t_a; |
943 val t_d = repeat_eqsubst_thm lthy defs_sym t_a; |
927 val t_r = MetaSimplifier.rewrite_rule [reps_same] t_d; |
944 val t_r = MetaSimplifier.rewrite_rule [reps_same] t_d; |
928 in |
945 in |