1444 Logic.mk_equals (rtrm, Syntax.check_term lthy (inj_REPABS lthy (rtrm, qtrm))) |
1444 Logic.mk_equals (rtrm, Syntax.check_term lthy (inj_REPABS lthy (rtrm, qtrm))) |
1445 *} |
1445 *} |
1446 |
1446 |
1447 (* Final wrappers *) |
1447 (* Final wrappers *) |
1448 |
1448 |
|
1449 ML {* |
|
1450 fun regularize_tac ctxt rel_eqv rel_refl = |
|
1451 (ObjectLogic.full_atomize_tac) THEN' |
|
1452 REPEAT_ALL_NEW (FIRST' [ |
|
1453 rtac rel_refl, |
|
1454 atac, |
|
1455 rtac @{thm universal_twice}, |
|
1456 (rtac @{thm impI} THEN' atac), |
|
1457 rtac @{thm implication_twice}, |
|
1458 EqSubst.eqsubst_tac ctxt [0] |
|
1459 [(@{thm equiv_res_forall} OF [rel_eqv]), |
|
1460 (@{thm equiv_res_exists} OF [rel_eqv])], |
|
1461 (* For a = b \<longrightarrow> a \<approx> b *) |
|
1462 (rtac @{thm impI} THEN' (asm_full_simp_tac HOL_ss) THEN' rtac rel_refl), |
|
1463 (rtac @{thm RIGHT_RES_FORALL_REGULAR}) |
|
1464 ]); |
|
1465 *} |
1449 |
1466 |
1450 ML {* |
1467 ML {* |
1451 fun regularize_goal lthy thm rel_eqv rel_refl qtrm = |
1468 fun regularize_goal lthy thm rel_eqv rel_refl qtrm = |
1452 let |
1469 let |
1453 val reg_trm = mk_REGULARIZE_goal lthy (prop_of thm) qtrm; |
1470 val reg_trm = mk_REGULARIZE_goal lthy (prop_of thm) qtrm; |
1454 fun tac ctxt = |
1471 fun tac lthy = regularize_tac lthy rel_eqv rel_refl; |
1455 (ObjectLogic.full_atomize_tac) THEN' |
|
1456 REPEAT_ALL_NEW (FIRST' [ |
|
1457 rtac rel_refl, |
|
1458 atac, |
|
1459 rtac @{thm universal_twice}, |
|
1460 (rtac @{thm impI} THEN' atac), |
|
1461 rtac @{thm implication_twice}, |
|
1462 EqSubst.eqsubst_tac ctxt [0] |
|
1463 [(@{thm equiv_res_forall} OF [rel_eqv]), |
|
1464 (@{thm equiv_res_exists} OF [rel_eqv])], |
|
1465 (* For a = b \<longrightarrow> a \<approx> b *) |
|
1466 (rtac @{thm impI} THEN' (asm_full_simp_tac HOL_ss) THEN' rtac rel_refl), |
|
1467 (rtac @{thm RIGHT_RES_FORALL_REGULAR}) |
|
1468 ]); |
|
1469 val cthm = Goal.prove lthy [] [] reg_trm |
1472 val cthm = Goal.prove lthy [] [] reg_trm |
1470 (fn {context, ...} => tac context 1); |
1473 (fn {context, ...} => tac context 1); |
1471 in |
1474 in |
1472 cthm OF [thm] |
1475 cthm OF [thm] |
1473 end |
1476 end |