53 |
53 |
54 ISAC has a set of rules called 'make_polynomial', which simplifies the result: |
54 ISAC has a set of rules called 'make_polynomial', which simplifies the result: |
55 \<close> |
55 \<close> |
56 ML \<open> |
56 ML \<open> |
57 val SOME (t, _) = Rewrite.rewrite_set_ thy true make_polynomial t; UnparseC.term t; |
57 val SOME (t, _) = Rewrite.rewrite_set_ thy true make_polynomial t; UnparseC.term t; |
58 Celem.Trace.trace_rewrite := false; |
58 Rewrite.trace_on := false; |
59 \<close> |
59 \<close> |
60 |
60 |
61 section \<open>Note on bound variables\<close> |
61 section \<open>Note on bound variables\<close> |
62 text \<open>You may have noticed that rewrite_ above could distinguish between x |
62 text \<open>You may have noticed that rewrite_ above could distinguish between x |
63 (d_d x x = 1) and y (d_d x y = 0). ISAC does this by instantiating theorems |
63 (d_d x x = 1) and y (d_d x y = 0). ISAC does this by instantiating theorems |
153 val t2 = (Thm.term_of o the o (TermC.parse thy)) |
153 val t2 = (Thm.term_of o the o (TermC.parse thy)) |
154 "(2 / (x + 3) + 2 / (x - 3)) / (8 * x / (x ^^^ 2 - 9))"; |
154 "(2 / (x + 3) + 2 / (x - 3)) / (8 * x / (x ^^^ 2 - 9))"; |
155 val SOME (t, _) = Rewrite.rewrite_set_ thy true norm_Rational t2; UnparseC.term t; |
155 val SOME (t, _) = Rewrite.rewrite_set_ thy true norm_Rational t2; UnparseC.term t; |
156 \<close> |
156 \<close> |
157 text \<open>The simplifiers are quite busy when finding the above results. you can |
157 text \<open>The simplifiers are quite busy when finding the above results. you can |
158 watch them at work by setting the switch 'Trace.trace_rewrite:\<close> |
158 watch them at work by setting the switch 'Rewrite.trace_on:\<close> |
159 ML \<open> |
159 ML \<open> |
160 Celem.Trace.trace_rewrite := false; |
160 Celem.Rewrite.trace_on := false; |
161 tracing "+++begin++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++"; |
161 tracing "+++begin++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++"; |
162 val SOME (t, _) = Rewrite.rewrite_set_ thy true norm_Rational t2; UnparseC.term t; |
162 val SOME (t, _) = Rewrite.rewrite_set_ thy true norm_Rational t2; UnparseC.term t; |
163 tracing "+++end++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++"; |
163 tracing "+++end++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++"; |
164 Celem.Trace.trace_rewrite := false; |
164 Celem.Rewrite.trace_on := false; |
165 \<close> |
165 \<close> |
166 text \<open>You see what happend when you click the checkbox <Tracing> on the bar |
166 text \<open>You see what happend when you click the checkbox <Tracing> on the bar |
167 separating this window from the Output-window. |
167 separating this window from the Output-window. |
168 |
168 |
169 So, it might be better to take simpler examples for watching the simplifiers. |
169 So, it might be better to take simpler examples for watching the simplifiers. |