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 |
2103 note conjI [OF this] |
2104 note conjI [OF this] |
2104 note r [OF this] |
2105 note r [OF this] |
2105 } |
2106 } |
2106 oops |
2107 oops |
2107 |
2108 |
2108 ML {* fun prop ctxt s = |
|
2109 Thm.cterm_of (ProofContext.theory_of ctxt) (Syntax.read_prop ctxt s) *} |
|
2110 |
|
2111 ML {* |
2109 ML {* |
2112 val ctxt0 = @{context}; |
2110 val ctxt0 = @{context}; |
2113 val ctxt = ctxt0; |
2111 val ctxt = ctxt0; |
2114 val (_, ctxt) = Variable.add_fixes ["A", "B", "C"] ctxt; |
2112 val (_, ctxt) = Variable.add_fixes ["A", "B", "C"] ctxt; |
2115 val ([r], ctxt) = Assumption.add_assumes [prop ctxt "A & B \<Longrightarrow> C"] ctxt; |
2113 val ([r], ctxt) = Assumption.add_assumes [@{cprop "A & B \<Longrightarrow> C"}] ctxt |
2116 val (this, ctxt) = Assumption.add_assumes [prop ctxt "A", prop ctxt "B"] ctxt; |
2114 val (this, ctxt) = Assumption.add_assumes [@{cprop "A"}, @{cprop "B"}] ctxt; |
2117 val this = [@{thm conjI} OF this]; |
2115 val this = [@{thm conjI} OF this]; |
2118 val this = r OF this; |
2116 val this = r OF this; |
2119 val this = Assumption.export false ctxt ctxt0 this |
2117 val this = Assumption.export false ctxt ctxt0 this |
2120 val this = Variable.export ctxt ctxt0 [this] |
2118 val this = Variable.export ctxt ctxt0 [this] |
2121 *} |
2119 *} |