2112 "2 + 10 \<equiv> 2 + (10::nat)"}. The reason is that the pretty-printer for |
2112 "2 + 10 \<equiv> 2 + (10::nat)"}. The reason is that the pretty-printer for |
2113 @{ML_type cterm}s eta-normalises (sic) terms and therefore produces this output. |
2113 @{ML_type cterm}s eta-normalises (sic) terms and therefore produces this output. |
2114 If we get hold of the ``raw'' representation of the produced theorem, |
2114 If we get hold of the ``raw'' representation of the produced theorem, |
2115 we obtain the expected result. |
2115 we obtain the expected result. |
2116 |
2116 |
2117 |
|
2118 @{ML_response [display,gray] |
2117 @{ML_response [display,gray] |
2119 "let |
2118 "let |
2120 val add = @{cterm \"\<lambda>x y. x + (y::nat)\"} |
2119 val add = @{cterm \"\<lambda>x y. x + (y::nat)\"} |
2121 val two = @{cterm \"2::nat\"} |
2120 val two = @{cterm \"2::nat\"} |
2122 val ten = @{cterm \"10::nat\"} |
2121 val ten = @{cterm \"10::nat\"} |
2125 Thm.prop_of (Thm.beta_conversion true ctrm) |
2124 Thm.prop_of (Thm.beta_conversion true ctrm) |
2126 end" |
2125 end" |
2127 "Const (\"==\",\<dots>) $ |
2126 "Const (\"==\",\<dots>) $ |
2128 (Abs (\"x\",\<dots>,Abs (\"y\",\<dots>,\<dots>)) $\<dots>$\<dots>) $ |
2127 (Abs (\"x\",\<dots>,Abs (\"y\",\<dots>,\<dots>)) $\<dots>$\<dots>) $ |
2129 (Const (\"Groups.plus_class.plus\",\<dots>) $ \<dots> $ \<dots>)"} |
2128 (Const (\"Groups.plus_class.plus\",\<dots>) $ \<dots> $ \<dots>)"} |
|
2129 |
|
2130 or in the pretty-printed form |
|
2131 |
|
2132 @{ML_response_fake [display,gray] |
|
2133 "let |
|
2134 val add = @{cterm \"\<lambda>x y. x + (y::nat)\"} |
|
2135 val two = @{cterm \"2::nat\"} |
|
2136 val ten = @{cterm \"10::nat\"} |
|
2137 val ctrm = Thm.capply (Thm.capply add two) ten |
|
2138 val ctxt = @{context} |
|
2139 |> Config.put eta_contract false |
|
2140 |> Config.put show_abbrevs false |
|
2141 in |
|
2142 Thm.prop_of (Thm.beta_conversion true ctrm) |
|
2143 |> pretty_term ctxt |
|
2144 |> pwriteln |
|
2145 end" |
|
2146 "(\<lambda>x y. x + y) 2 10 \<equiv> 2 + 10"} |
2130 |
2147 |
2131 The argument @{ML true} in @{ML beta_conversion in Thm} indicates that |
2148 The argument @{ML true} in @{ML beta_conversion in Thm} indicates that |
2132 the right-hand side should be fully beta-normalised. If instead |
2149 the right-hand side should be fully beta-normalised. If instead |
2133 @{ML false} is given, then only a single beta-reduction is performed |
2150 @{ML false} is given, then only a single beta-reduction is performed |
2134 on the outer-most level. |
2151 on the outer-most level. |