equal
deleted
inserted
replaced
1650 text {* |
1650 text {* |
1651 From the integer value it generates the corresponding number term, called |
1651 From the integer value it generates the corresponding number term, called |
1652 @{text num} (Line 3), and then generates the meta-equation @{text "t \<equiv> num"} |
1652 @{text num} (Line 3), and then generates the meta-equation @{text "t \<equiv> num"} |
1653 (Line 4), which it proves by the arithmetic tactic in Line 6. |
1653 (Line 4), which it proves by the arithmetic tactic in Line 6. |
1654 |
1654 |
1655 For our purpose at the moment, proving the meta-equation using |
1655 For our purpose at the moment, proving the meta-equation using @{ML |
1656 @{ML Arith_Data.arith_tac} is |
1656 arith_tac in Arith_Data} is fine, but there is also an alternative employing |
1657 fine, but there is also an alternative employing the simplifier with a very |
1657 the simplifier with a special simpset. For the kind of lemmas we |
1658 restricted simpset. For the kind of lemmas we want to prove, the simpset |
1658 want to prove here, the simpset @{text "num_ss"} should suffice. |
1659 @{text "num_ss"} in the code will suffice. |
|
1660 *} |
1659 *} |
1661 |
1660 |
1662 ML{*fun get_thm_alt ctxt (t, n) = |
1661 ML{*fun get_thm_alt ctxt (t, n) = |
1663 let |
1662 let |
1664 val num = HOLogic.mk_number @{typ "nat"} n |
1663 val num = HOLogic.mk_number @{typ "nat"} n |
1670 end*} |
1669 end*} |
1671 |
1670 |
1672 text {* |
1671 text {* |
1673 The advantage of @{ML get_thm_alt} is that it leaves very little room for |
1672 The advantage of @{ML get_thm_alt} is that it leaves very little room for |
1674 something to go wrong; in contrast it is much more difficult to predict |
1673 something to go wrong; in contrast it is much more difficult to predict |
1675 what happens with @{ML Arith_Data.arith_tac}, especially in more complicated |
1674 what happens with @{ML arith_tac in Arith_Data}, especially in more complicated |
1676 circumstances. The disatvantage of @{ML get_thm_alt} is to find a simpset |
1675 circumstances. The disatvantage of @{ML get_thm_alt} is to find a simpset |
1677 that is sufficiently powerful to solve every instance of the lemmas |
1676 that is sufficiently powerful to solve every instance of the lemmas |
1678 we like to prove. This requires careful tuning, but is often necessary in |
1677 we like to prove. This requires careful tuning, but is often necessary in |
1679 ``production code''.\footnote{It would be of great help if there is another |
1678 ``production code''.\footnote{It would be of great help if there is another |
1680 way than tracing the simplifier to obtain the lemmas that are successfully |
1679 way than tracing the simplifier to obtain the lemmas that are successfully |