41 \<close> |
41 \<close> |
42 text \<open>... and let us differentiate the term t:\<close> |
42 text \<open>... and let us differentiate the term t:\<close> |
43 ML \<open> |
43 ML \<open> |
44 val t = TermC.parseNEW' ctxt "d_d x (x\<up>2 + x + y)"; |
44 val t = TermC.parseNEW' ctxt "d_d x (x\<up>2 + x + y)"; |
45 |
45 |
46 val SOME (t, _) = Rewrite.rewrite_inst_ thy ro er true inst diff_sum t; UnparseC.term t; |
46 val SOME (t, _) = Rewrite.rewrite_inst_ ctxt ro er true inst diff_sum t; UnparseC.term t; |
47 val SOME (t, _) = Rewrite.rewrite_inst_ thy ro er true inst diff_sum t; UnparseC.term t; |
47 val SOME (t, _) = Rewrite.rewrite_inst_ ctxt ro er true inst diff_sum t; UnparseC.term t; |
48 val SOME (t, _) = Rewrite.rewrite_inst_ thy ro er true inst diff_pow t; UnparseC.term t; |
48 val SOME (t, _) = Rewrite.rewrite_inst_ ctxt ro er true inst diff_pow t; UnparseC.term t; |
49 val SOME (t, _) = Rewrite.rewrite_inst_ thy ro er true inst diff_var t; UnparseC.term t; |
49 val SOME (t, _) = Rewrite.rewrite_inst_ ctxt ro er true inst diff_var t; UnparseC.term t; |
50 val SOME (t, _) = Rewrite.rewrite_inst_ thy ro er true inst diff_const t; UnparseC.term t; |
50 val SOME (t, _) = Rewrite.rewrite_inst_ ctxt ro er true inst diff_const t; UnparseC.term t; |
51 \<close> |
51 \<close> |
52 text \<open>Please, scoll up the Output-window to check the 5 steps of rewriting ! |
52 text \<open>Please, scoll up the Output-window to check the 5 steps of rewriting ! |
53 You might not be satisfied by the result "2 * x \<up> (2 - 1) + 1 + 0". |
53 You might not be satisfied by the result "2 * x \<up> (2 - 1) + 1 + 0". |
54 |
54 |
55 ISAC has a set of rules called 'make_polynomial', which simplifies the result: |
55 ISAC has a set of rules called 'make_polynomial', which simplifies the result: |
56 \<close> |
56 \<close> |
57 ML \<open> |
57 ML \<open> |
58 val SOME (t, _) = Rewrite.rewrite_set_ thy true make_polynomial t; UnparseC.term t; |
58 val SOME (t, _) = Rewrite.rewrite_set_ ctxt true make_polynomial t; UnparseC.term t; |
59 Rewrite.trace_on := false; (*true false*) |
|
60 \<close> |
59 \<close> |
61 |
60 |
62 section \<open>Note on bound variables\<close> |
61 section \<open>Note on bound variables\<close> |
63 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 |
64 (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 |
156 val SOME (t, _) = Rewrite.rewrite_set_ ctxt true norm_Rational t2; UnparseC.term t; |
155 val SOME (t, _) = Rewrite.rewrite_set_ ctxt true norm_Rational t2; UnparseC.term t; |
157 \<close> |
156 \<close> |
158 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 |
159 watch them at work by setting the switch 'Rewrite.trace_on:\<close> |
158 watch them at work by setting the switch 'Rewrite.trace_on:\<close> |
160 ML \<open> |
159 ML \<open> |
161 Rewrite.trace_on := false; (*true false*) |
|
162 tracing "+++begin++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++"; |
160 tracing "+++begin++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++"; |
163 val SOME (t, _) = Rewrite.rewrite_set_ ctxt true norm_Rational t2; UnparseC.term t; |
161 val SOME (t, _) = Rewrite.rewrite_set_ ctxt true norm_Rational t2; UnparseC.term t; |
164 tracing "+++end++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++"; |
162 tracing "+++end++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++"; |
165 Rewrite.trace_on := false; (*true false*) |
|
166 \<close> |
163 \<close> |
167 text \<open>You see what happend when you click the checkbox <Tracing> on the bar |
164 text \<open>You see what happend when you click the checkbox <Tracing> on the bar |
168 separating this window from the Output-window. |
165 separating this window from the Output-window. |
169 |
166 |
170 So, it might be better to take simpler examples for watching the simplifiers. |
167 So, it might be better to take simpler examples for watching the simplifiers. |