equal
deleted
inserted
replaced
1774 Thm.beta_conversion true (Thm.capply (Thm.capply add two) ten) |
1774 Thm.beta_conversion true (Thm.capply (Thm.capply add two) ten) |
1775 end" |
1775 end" |
1776 "((\<lambda>x y. x + y) 2) 10 \<equiv> 2 + 10"} |
1776 "((\<lambda>x y. x + y) 2) 10 \<equiv> 2 + 10"} |
1777 |
1777 |
1778 Note that the actual response in this example is @{term "2 + 10 \<equiv> 2 + (10::nat)"}, |
1778 Note that the actual response in this example is @{term "2 + 10 \<equiv> 2 + (10::nat)"}, |
1779 since the pretty-printer for @{ML_type cterm}s already beta-normalises terms. |
1779 since the pretty-printer for @{ML_type cterm}s eta-normalises terms. |
1780 But how we constructed the term (using the function |
1780 But how we constructed the term (using the function |
1781 @{ML Thm.capply}, which is the application @{ML $} for @{ML_type cterm}s) |
1781 @{ML Thm.capply}, which is the application @{ML $} for @{ML_type cterm}s) |
1782 ensures that the left-hand side must contain beta-redexes. Indeed |
1782 ensures that the left-hand side must contain beta-redexes. Indeed |
1783 if we obtain the ``raw'' representation of the produced theorem, we |
1783 if we obtain the ``raw'' representation of the produced theorem, we |
1784 can see the difference: |
1784 can see the difference: |
1808 in |
1808 in |
1809 Thm.beta_conversion false (Thm.capply add two) |
1809 Thm.beta_conversion false (Thm.capply add two) |
1810 end" |
1810 end" |
1811 "((\<lambda>x y. x + y) 2) \<equiv> \<lambda>y. 2 + y"} |
1811 "((\<lambda>x y. x + y) 2) \<equiv> \<lambda>y. 2 + y"} |
1812 |
1812 |
1813 Again, we actually see as output only the fully normalised term |
1813 Again, we actually see as output only the fully eta-normalised term. |
1814 @{text "\<lambda>y. 2 + y"}. |
|
1815 |
1814 |
1816 The main point of conversions is that they can be used for rewriting |
1815 The main point of conversions is that they can be used for rewriting |
1817 @{ML_type cterm}s. To do this you can use the function @{ML |
1816 @{ML_type cterm}s. To do this you can use the function @{ML |
1818 "Conv.rewr_conv"}, which expects a meta-equation as an argument. Suppose we |
1817 "Conv.rewr_conv"}, which expects a meta-equation as an argument. Suppose we |
1819 want to rewrite a @{ML_type cterm} according to the meta-equation: |
1818 want to rewrite a @{ML_type cterm} according to the meta-equation: |