1439 ML {* |
1439 ML {* |
1440 fun mk_inj_REPABS_goal lthy (rtrm, qtrm) = |
1440 fun mk_inj_REPABS_goal lthy (rtrm, qtrm) = |
1441 Logic.mk_equals (rtrm, Syntax.check_term lthy (inj_REPABS lthy (rtrm, qtrm))) |
1441 Logic.mk_equals (rtrm, Syntax.check_term lthy (inj_REPABS lthy (rtrm, qtrm))) |
1442 *} |
1442 *} |
1443 |
1443 |
1444 |
1444 (* Final wrappers *) |
|
1445 |
|
1446 |
|
1447 ML {* |
|
1448 fun regularize_goal lthy thm rel_eqv rel_refl qtrm = |
|
1449 let |
|
1450 val reg_trm = mk_REGULARIZE_goal lthy (prop_of thm) qtrm; |
|
1451 fun tac ctxt = |
|
1452 (ObjectLogic.full_atomize_tac) THEN' |
|
1453 REPEAT_ALL_NEW (FIRST' [ |
|
1454 rtac rel_refl, |
|
1455 atac, |
|
1456 rtac @{thm universal_twice}, |
|
1457 (rtac @{thm impI} THEN' atac), |
|
1458 rtac @{thm implication_twice}, |
|
1459 EqSubst.eqsubst_tac ctxt [0] |
|
1460 [(@{thm equiv_res_forall} OF [rel_eqv]), |
|
1461 (@{thm equiv_res_exists} OF [rel_eqv])], |
|
1462 (* For a = b \<longrightarrow> a \<approx> b *) |
|
1463 (rtac @{thm impI} THEN' (asm_full_simp_tac HOL_ss) THEN' rtac rel_refl), |
|
1464 (rtac @{thm RIGHT_RES_FORALL_REGULAR}) |
|
1465 ]); |
|
1466 val cthm = Goal.prove lthy [] [] reg_trm |
|
1467 (fn {context, ...} => tac context 1); |
|
1468 in |
|
1469 cthm OF [thm] |
|
1470 end |
|
1471 *} |
|
1472 |
|
1473 ML {* |
|
1474 fun repabs_goal lthy thm rty quot_thm reflex_thm trans_thm rsp_thms qtrm = |
|
1475 let |
|
1476 val rg = Syntax.check_term lthy (mk_inj_REPABS_goal lthy ((prop_of thm), qtrm)); |
|
1477 fun tac ctxt = (ObjectLogic.full_atomize_tac) THEN' |
|
1478 (REPEAT_ALL_NEW (r_mk_comb_tac ctxt rty quot_thm reflex_thm trans_thm rsp_thms)); |
|
1479 val cthm = Goal.prove lthy [] [] rg (fn x => tac (#context x) 1); |
|
1480 in |
|
1481 @{thm Pure.equal_elim_rule1} OF [cthm, thm] |
|
1482 end |
|
1483 *} |
|
1484 |
|
1485 ML {* |
|
1486 fun lift_thm_goal lthy qty qty_name rsp_thms defs rthm goal = |
|
1487 let |
|
1488 val (rty, rel, rel_refl, rel_eqv) = lookup_quot_data lthy qty; |
|
1489 val (trans2, reps_same, absrep, quot) = lookup_quot_thms lthy qty_name; |
|
1490 val t_a = atomize_thm rthm; |
|
1491 val goal_a = atomize_goal (ProofContext.theory_of lthy) goal; |
|
1492 val t_r = regularize_goal lthy t_a rel_eqv rel_refl goal_a; |
|
1493 val t_t = repabs_goal lthy t_r rty quot rel_refl trans2 rsp_thms goal_a; |
|
1494 val (alls, exs) = findallex lthy rty qty (prop_of t_a); |
|
1495 val allthms = map (make_allex_prs_thm lthy quot @{thm FORALL_PRS}) alls |
|
1496 val exthms = map (make_allex_prs_thm lthy quot @{thm EXISTS_PRS}) exs |
|
1497 val t_a = MetaSimplifier.rewrite_rule (allthms @ exthms) t_t |
|
1498 val abs = findabs rty (prop_of t_a); |
|
1499 val aps = findaps rty (prop_of t_a); |
|
1500 val app_prs_thms = map (applic_prs lthy rty qty absrep) aps; |
|
1501 val lam_prs_thms = map (make_simp_prs_thm lthy quot @{thm LAMBDA_PRS}) abs; |
|
1502 val t_l = repeat_eqsubst_thm lthy (lam_prs_thms @ app_prs_thms) t_a; |
|
1503 val defs_sym = flat (map (add_lower_defs lthy) defs); |
|
1504 val defs_sym_eq = map (fn x => eq_reflection OF [x]) defs_sym; |
|
1505 val t_id = simp_ids lthy t_l; |
|
1506 val t_d0 = MetaSimplifier.rewrite_rule defs_sym_eq t_id; |
|
1507 val t_d = repeat_eqsubst_thm lthy defs_sym t_d0; |
|
1508 val t_r = MetaSimplifier.rewrite_rule [reps_same] t_d; |
|
1509 val t_rv = ObjectLogic.rulify t_r |
|
1510 in |
|
1511 Thm.varifyT t_rv |
1445 end |
1512 end |
1446 |
1513 *} |
|
1514 |
|
1515 |
|
1516 end |
|
1517 |
|
1518 |