499 if (needs_lift rty T) then |
499 if (needs_lift rty T) then |
500 (mk_bex ty1) $ (mk_resp ty2 $ rrel) $ (apply_subt (my_reg lthy rel rty) t) |
500 (mk_bex ty1) $ (mk_resp ty2 $ rrel) $ (apply_subt (my_reg lthy rel rty) t) |
501 else |
501 else |
502 Const (@{const_name "Ex"}, ty) $ apply_subt (my_reg lthy rel rty) t |
502 Const (@{const_name "Ex"}, ty) $ apply_subt (my_reg lthy rel rty) t |
503 end |
503 end |
|
504 | Const (@{const_name "op ="}, ty) $ t => |
|
505 if needs_lift rty (fastype_of t) then |
|
506 (tyRel (fastype_of t) rty rel lthy) $ t |
|
507 else Const (@{const_name "op ="}, ty) $ (my_reg lthy rel rty t) |
504 | t1 $ t2 => (my_reg lthy rel rty t1) $ (my_reg lthy rel rty t2) |
508 | t1 $ t2 => (my_reg lthy rel rty t1) $ (my_reg lthy rel rty t2) |
505 | _ => trm |
509 | _ => trm |
506 *} |
510 *} |
507 |
511 |
508 text {* Assumes that the given theorem is atomized *} |
512 text {* Assumes that the given theorem is atomized *} |
511 Logic.mk_implies |
515 Logic.mk_implies |
512 ((prop_of thm), |
516 ((prop_of thm), |
513 (my_reg lthy rel rty (prop_of thm))) |
517 (my_reg lthy rel rty (prop_of thm))) |
514 *} |
518 *} |
515 |
519 |
516 ML {* |
520 lemma eq_rr: "(\<And>x. R x x) \<Longrightarrow> a = b \<Longrightarrow> R a b" |
517 fun regularize thm rty rel rel_eqv lthy = |
521 by (auto) |
|
522 |
|
523 ML {* |
|
524 fun regularize thm rty rel rel_eqv rel_refl lthy = |
518 let |
525 let |
519 val g = build_regularize_goal thm rty rel lthy; |
526 val g = build_regularize_goal thm rty rel lthy; |
520 fun tac ctxt = |
527 fun tac ctxt = |
521 (asm_full_simp_tac ((Simplifier.context ctxt HOL_ss) addsimps |
528 REPEAT_ALL_NEW (FIRST' [ |
|
529 rtac rel_refl, |
|
530 atac, |
|
531 (rtac @{thm allI} THEN' dtac @{thm spec}), |
|
532 (fn i => CHANGED (asm_full_simp_tac ((Simplifier.context ctxt HOL_ss) addsimps |
522 [(@{thm equiv_res_forall} OF [rel_eqv]), |
533 [(@{thm equiv_res_forall} OF [rel_eqv]), |
523 (@{thm equiv_res_exists} OF [rel_eqv])])) THEN_ALL_NEW |
534 (@{thm equiv_res_exists} OF [rel_eqv])]) i)), |
524 (((rtac @{thm RIGHT_RES_FORALL_REGULAR}) THEN' (RANGE [fn _ => all_tac, atac]) THEN' |
535 MetisTools.metis_tac ctxt [], |
525 (MetisTools.metis_tac ctxt [])) ORELSE' (MetisTools.metis_tac ctxt [])); |
536 rtac (@{thm eq_rr} OF [rel_refl]), |
|
537 ((rtac @{thm RIGHT_RES_FORALL_REGULAR}) THEN' (RANGE [fn _ => all_tac, atac])) |
|
538 ]); |
526 val cthm = Goal.prove lthy [] [] g (fn x => tac (#context x) 1); |
539 val cthm = Goal.prove lthy [] [] g (fn x => tac (#context x) 1); |
527 in |
540 in |
528 cthm OF [thm] |
541 cthm OF [thm] |
529 end |
542 end |
530 *} |
543 *} |
905 fun lift_thm lthy qty qty_name rsp_thms defs t = let |
918 fun lift_thm lthy qty qty_name rsp_thms defs t = let |
906 val (rty, rel, rel_refl, rel_eqv) = lookup_quot_data lthy qty; |
919 val (rty, rel, rel_refl, rel_eqv) = lookup_quot_data lthy qty; |
907 val (trans2, reps_same, quot) = lookup_quot_thms lthy qty_name; |
920 val (trans2, reps_same, quot) = lookup_quot_thms lthy qty_name; |
908 val consts = lookup_quot_consts defs; |
921 val consts = lookup_quot_consts defs; |
909 val t_a = atomize_thm t; |
922 val t_a = atomize_thm t; |
910 val t_r = regularize t_a rty rel rel_eqv lthy; |
923 val t_r = regularize t_a rty rel rel_eqv rel_refl lthy; |
911 val t_t = repabs lthy t_r consts rty qty quot rel_refl trans2 rsp_thms; |
924 val t_t = repabs lthy t_r consts rty qty quot rel_refl trans2 rsp_thms; |
912 val abs = findabs rty (prop_of t_a); |
925 val abs = findabs rty (prop_of t_a); |
913 val simp_lam_prs_thms = map (make_simp_lam_prs_thm lthy quot) abs; |
926 val simp_lam_prs_thms = map (make_simp_lam_prs_thm lthy quot) abs; |
914 val t_l = repeat_eqsubst_thm lthy simp_lam_prs_thms t_t; |
927 val t_l = repeat_eqsubst_thm lthy simp_lam_prs_thms t_t; |
915 val t_a = simp_allex_prs lthy quot t_l; |
928 val t_a = simp_allex_prs lthy quot t_l; |