515 Logic.mk_implies |
515 Logic.mk_implies |
516 ((prop_of thm), |
516 ((prop_of thm), |
517 (my_reg lthy rel rty (prop_of thm))) |
517 (my_reg lthy rel rty (prop_of thm))) |
518 *} |
518 *} |
519 |
519 |
520 lemma eq_rr: "(\<And>x. R x x) \<Longrightarrow> a = b \<Longrightarrow> R a b" |
520 lemma universal_twice: "(\<And>x. (P x \<longrightarrow> Q x)) \<Longrightarrow> ((\<forall>x. P x) \<longrightarrow> (\<forall>x. Q x))" |
521 by (auto) |
521 apply (auto) |
|
522 done |
|
523 |
|
524 lemma implication_twice: "(c \<longrightarrow> a) \<Longrightarrow> (a \<Longrightarrow> b \<longrightarrow> d) \<Longrightarrow> (a \<longrightarrow> b) \<longrightarrow> (c \<longrightarrow> d)" |
|
525 apply (auto) |
|
526 done |
522 |
527 |
523 ML {* |
528 ML {* |
524 fun regularize thm rty rel rel_eqv rel_refl lthy = |
529 fun regularize thm rty rel rel_eqv rel_refl lthy = |
525 let |
530 let |
526 val g = build_regularize_goal thm rty rel lthy; |
531 val g = build_regularize_goal thm rty rel lthy; |
527 fun tac ctxt = |
532 fun tac ctxt = |
|
533 (ObjectLogic.full_atomize_tac) THEN' |
528 REPEAT_ALL_NEW (FIRST' [ |
534 REPEAT_ALL_NEW (FIRST' [ |
529 rtac rel_refl, |
535 rtac rel_refl, |
530 atac, |
536 atac, |
531 (rtac @{thm allI} THEN' dtac @{thm spec}), |
537 rtac @{thm universal_twice}, |
|
538 rtac @{thm implication_twice}, |
532 (fn i => CHANGED (asm_full_simp_tac ((Simplifier.context ctxt HOL_ss) addsimps |
539 (fn i => CHANGED (asm_full_simp_tac ((Simplifier.context ctxt HOL_ss) addsimps |
533 [(@{thm equiv_res_forall} OF [rel_eqv]), |
540 [(@{thm equiv_res_forall} OF [rel_eqv]), |
534 (@{thm equiv_res_exists} OF [rel_eqv])]) i)), |
541 (@{thm equiv_res_exists} OF [rel_eqv])]) i)), |
535 MetisTools.metis_tac ctxt [], |
542 (rtac @{thm impI} THEN' (asm_full_simp_tac (Simplifier.context ctxt HOL_ss)) THEN' rtac rel_refl), |
536 rtac (@{thm eq_rr} OF [rel_refl]), |
543 (rtac @{thm RIGHT_RES_FORALL_REGULAR}) |
537 ((rtac @{thm RIGHT_RES_FORALL_REGULAR}) THEN' (RANGE [fn _ => all_tac, atac])) |
544 ]); |
538 ]); |
|
539 val cthm = Goal.prove lthy [] [] g (fn x => tac (#context x) 1); |
545 val cthm = Goal.prove lthy [] [] g (fn x => tac (#context x) 1); |
540 in |
546 in |
541 cthm OF [thm] |
547 cthm OF [thm] |
542 end |
548 end |
543 *} |
549 *} |