1642 ML %linenosgray{*fun get_thm ctxt (t, n) = |
1642 ML %linenosgray{*fun get_thm ctxt (t, n) = |
1643 let |
1643 let |
1644 val num = HOLogic.mk_number @{typ "nat"} n |
1644 val num = HOLogic.mk_number @{typ "nat"} n |
1645 val goal = Logic.mk_equals (t, num) |
1645 val goal = Logic.mk_equals (t, num) |
1646 in |
1646 in |
1647 Goal.prove ctxt [] [] goal (K (arith_tac ctxt 1)) |
1647 Goal.prove ctxt [] [] goal (K (Arith_Data.arith_tac ctxt 1)) |
1648 end*} |
1648 end*} |
1649 |
1649 |
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 @{ML arith_tac} is |
1655 For our purpose at the moment, proving the meta-equation using |
|
1656 @{ML Arith_Data.arith_tac} is |
1656 fine, but there is also an alternative employing the simplifier with a very |
1657 fine, but there is also an alternative employing the simplifier with a very |
1657 restricted simpset. For the kind of lemmas we want to prove, the simpset |
1658 restricted simpset. For the kind of lemmas we want to prove, the simpset |
1658 @{text "num_ss"} in the code will suffice. |
1659 @{text "num_ss"} in the code will suffice. |
1659 *} |
1660 *} |
1660 |
1661 |
1669 end*} |
1670 end*} |
1670 |
1671 |
1671 text {* |
1672 text {* |
1672 The advantage of @{ML get_thm_alt} is that it leaves very little room for |
1673 The advantage of @{ML get_thm_alt} is that it leaves very little room for |
1673 something to go wrong; in contrast it is much more difficult to predict |
1674 something to go wrong; in contrast it is much more difficult to predict |
1674 what happens with @{ML arith_tac}, especially in more complicated |
1675 what happens with @{ML Arith_Data.arith_tac}, especially in more complicated |
1675 circumstances. The disatvantage of @{ML get_thm_alt} is to find a simpset |
1676 circumstances. The disatvantage of @{ML get_thm_alt} is to find a simpset |
1676 that is sufficiently powerful to solve every instance of the lemmas |
1677 that is sufficiently powerful to solve every instance of the lemmas |
1677 we like to prove. This requires careful tuning, but is often necessary in |
1678 we like to prove. This requires careful tuning, but is often necessary in |
1678 ``production code''.\footnote{It would be of great help if there is another |
1679 ``production code''.\footnote{It would be of great help if there is another |
1679 way than tracing the simplifier to obtain the lemmas that are successfully |
1680 way than tracing the simplifier to obtain the lemmas that are successfully |