1526 in |
1526 in |
1527 lthy2 |
1527 lthy2 |
1528 end |
1528 end |
1529 *} |
1529 *} |
1530 |
1530 |
1531 |
1531 lemma procedure: |
|
1532 assumes a: "A" |
|
1533 and b: "A \<Longrightarrow> B" |
|
1534 and c: "B = C" |
|
1535 and d: "C = D" |
|
1536 shows "D" |
|
1537 using a b c d |
|
1538 by simp |
|
1539 |
|
1540 ML {* |
|
1541 fun procedure_inst ctxt rtrm qtrm = |
|
1542 let |
|
1543 val thy = ProofContext.theory_of ctxt |
|
1544 val rtrm' = HOLogic.dest_Trueprop rtrm |
|
1545 val qtrm' = HOLogic.dest_Trueprop qtrm |
|
1546 val reg_goal = Syntax.check_term ctxt (REGULARIZE_trm ctxt rtrm' qtrm') |
|
1547 val inj_goal = Syntax.check_term ctxt (inj_REPABS ctxt (reg_goal, qtrm')) |
|
1548 in |
|
1549 Drule.instantiate' [] |
|
1550 [SOME (cterm_of thy rtrm'), |
|
1551 SOME (cterm_of thy reg_goal), |
|
1552 SOME (cterm_of thy inj_goal)] |
|
1553 @{thm procedure} |
1532 end |
1554 end |
1533 |
1555 |
1534 |
1556 fun procedure_tac rthm = |
|
1557 Subgoal.FOCUS (fn {context, concl, ...} => |
|
1558 let |
|
1559 val rthm' = atomize_thm rthm |
|
1560 val rule = procedure_inst context (prop_of rthm') (term_of concl) |
|
1561 in |
|
1562 EVERY1 [rtac rule, rtac rthm'] |
|
1563 end) |
|
1564 *} |
|
1565 |
|
1566 (* FIXME: allex_prs and lambda_prs can be one function *) |
|
1567 |
|
1568 ML {* |
|
1569 fun allex_prs_tac lthy quot = |
|
1570 (EqSubst.eqsubst_tac lthy [0] @{thms FORALL_PRS[symmetric] EXISTS_PRS[symmetric]}) |
|
1571 THEN' (quotient_tac quot); |
|
1572 *} |
|
1573 |
|
1574 ML {* |
|
1575 fun lambda_prs_tac lthy quot = |
|
1576 (EqSubst.eqsubst_tac lthy [0] @{thms LAMBDA_PRS} |
|
1577 THEN' (RANGE [quotient_tac quot, quotient_tac quot])); |
|
1578 *} |
|
1579 |
|
1580 ML {* |
|
1581 fun clean_tac lthy quot defs reps_same = |
|
1582 let |
|
1583 val lower = flat (map (add_lower_defs lthy) defs) |
|
1584 in |
|
1585 (REPEAT_ALL_NEW (allex_prs_tac lthy quot)) THEN' |
|
1586 (REPEAT_ALL_NEW (lambda_prs_tac lthy quot)) THEN' |
|
1587 (REPEAT_ALL_NEW (EqSubst.eqsubst_tac lthy [0] lower)) THEN' |
|
1588 (simp_tac (HOL_ss addsimps [reps_same])) |
|
1589 end |
|
1590 *} |
|
1591 |
|
1592 |
|
1593 end |
|
1594 |
|
1595 |