1492 Conv.abs_conv conv @{context} ctrm |
1492 Conv.abs_conv conv @{context} ctrm |
1493 end" |
1493 end" |
1494 "\<lambda>P. True \<and> P \<and> Foo \<equiv> \<lambda>P. P \<and> Foo"} |
1494 "\<lambda>P. True \<and> P \<and> Foo \<equiv> \<lambda>P. P \<and> Foo"} |
1495 |
1495 |
1496 The conversion that goes under an application is |
1496 The conversion that goes under an application is |
1497 @{ML Conv.combination_conv}. It expects two conversions, which each of them |
1497 @{ML Conv.combination_conv}. It expects two conversions as arguments, |
1498 is applied to the corresponding ``branch'' of the application. |
1498 each of which is applied to the corresponding ``branch'' of the application. |
1499 |
1499 |
1500 We can now apply all these functions in a |
1500 We can now apply all these functions in a |
1501 conversion that recursively descends a term and applies a conversion in all |
1501 conversion that recursively descends a term and applies a conversion in all |
1502 possible positions. |
1502 possible positions. |
1503 *} |
1503 *} |
1596 (Conv.prems_conv ~1 (if_true1_conv ctxt)) then_conv |
1596 (Conv.prems_conv ~1 (if_true1_conv ctxt)) then_conv |
1597 Conv.concl_conv ~1 (all_true1_conv ctxt)) ctxt) i |
1597 Conv.concl_conv ~1 (all_true1_conv ctxt)) ctxt) i |
1598 end)*} |
1598 end)*} |
1599 |
1599 |
1600 text {* |
1600 text {* |
1601 We call the conversions with the argument @{ML "~1"} in order to |
1601 We call the conversions with the argument @{ML "~1"}. This is to |
1602 analyse all parameters, premises and conclusions. If we call it with |
1602 analyse all parameters, premises and conclusions. If we call them with |
1603 a non-negative number, say @{text n}, then these conversions will |
1603 a non-negative number, say @{text n}, then these conversions will |
1604 only be called on @{text n} premises (similar for parameters and |
1604 only be called on @{text n} premises (similar for parameters and |
1605 conclusions). To test the tactic, consider the proof |
1605 conclusions). To test the tactic, consider the proof |
1606 *} |
1606 *} |
1607 |
1607 |
1608 lemma |
1608 lemma |
1609 "if True \<and> P then P else True \<and> False \<Longrightarrow> |
1609 "if True \<and> P then P else True \<and> False \<Longrightarrow> |
1610 (if True \<and> Q then Q else P) \<longrightarrow> True \<and> (True \<and> Q)" |
1610 (if True \<and> Q then True \<and> Q else P) \<longrightarrow> True \<and> (True \<and> Q)" |
1611 apply(tactic {* true1_tac 1 *}) |
1611 apply(tactic {* true1_tac 1 *}) |
1612 txt {* where the tactic yields the goal state |
1612 txt {* where the tactic yields the goal state |
1613 |
1613 |
1614 \begin{minipage}{\textwidth} |
1614 \begin{minipage}{\textwidth} |
1615 @{subgoals [display]} |
1615 @{subgoals [display]} |
1616 \end{minipage} *} |
1616 \end{minipage} *} |
1617 (*<*)oops(*>*) |
1617 (*<*)oops(*>*) |
1618 |
1618 |
1619 text {* |
1619 text {* |
|
1620 As you can see, the premises are rewritten according to @{ML if_true1_conv}, while |
|
1621 the conclusion according to @{ML all_true1_conv}. |
|
1622 |
1620 To sum up this section, conversions are not as powerful as the simplifier |
1623 To sum up this section, conversions are not as powerful as the simplifier |
1621 and simprocs; the advantage of conversions, however, is that you never have |
1624 and simprocs; the advantage of conversions, however, is that you never have |
1622 to worry about non-termination. |
1625 to worry about non-termination. |
1623 |
1626 |
1624 \begin{readmore} |
1627 \begin{readmore} |