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 = ParseC.parse_test ctxt "d_d x (x\<up>2 + x + y)"; |
44 val t = ParseC.parse_test ctxt "d_d x (x\<up>2 + x + y)"; |
45 |
45 |
46 val SOME (t, _) = Rewrite.rewrite_inst_ ctxt 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_in_ctxt @{context} t; |
47 val SOME (t, _) = Rewrite.rewrite_inst_ ctxt 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_in_ctxt @{context} t; |
48 val SOME (t, _) = Rewrite.rewrite_inst_ ctxt 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_in_ctxt @{context} t; |
49 val SOME (t, _) = Rewrite.rewrite_inst_ ctxt 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_in_ctxt @{context} t; |
50 val SOME (t, _) = Rewrite.rewrite_inst_ ctxt 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_in_ctxt @{context} 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_ ctxt true make_polynomial t; UnparseC.term t; |
58 val SOME (t, _) = Rewrite.rewrite_set_ ctxt true make_polynomial t; UnparseC.term_in_ctxt @{context} t; |
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 |
96 text \<open>Let us start with an example; in order to see what is going on we tell |
96 text \<open>Let us start with an example; in order to see what is going on we tell |
97 Isabelle to show all brackets: |
97 Isabelle to show all brackets: |
98 \<close> |
98 \<close> |
99 ML \<open> |
99 ML \<open> |
100 (*show_brackets := true; TODO*) |
100 (*show_brackets := true; TODO*) |
101 val t0 = ParseC.parse_test ctxt "2*a + 3*b + 4*a::real"; UnparseC.term t0; |
101 val t0 = ParseC.parse_test ctxt "2*a + 3*b + 4*a::real"; UnparseC.term_in_ctxt @{context} t0; |
102 (*show_brackets := false;*) |
102 (*show_brackets := false;*) |
103 \<close> |
103 \<close> |
104 text \<open>Now we want to bring 4*a close to 2*a in order to get 6*a: |
104 text \<open>Now we want to bring 4*a close to 2*a in order to get 6*a: |
105 \<close> |
105 \<close> |
106 ML \<open> |
106 ML \<open> |
107 val SOME (t, _) = Rewrite.rewrite_ ctxt ro er true @{thm add.assoc} t0; UnparseC.term t; |
107 val SOME (t, _) = Rewrite.rewrite_ ctxt ro er true @{thm add.assoc} t0; UnparseC.term_in_ctxt @{context} t; |
108 val SOME (t, _) = Rewrite.rewrite_ ctxt ro er true @{thm add.left_commute} t; UnparseC.term t; |
108 val SOME (t, _) = Rewrite.rewrite_ ctxt ro er true @{thm add.left_commute} t; UnparseC.term_in_ctxt @{context} t; |
109 val SOME (t, _) = Rewrite.rewrite_ ctxt ro er true @{thm add.commute} t; UnparseC.term t; |
109 val SOME (t, _) = Rewrite.rewrite_ ctxt ro er true @{thm add.commute} t; UnparseC.term_in_ctxt @{context} t; |
110 val SOME (t, _) = Rewrite.rewrite_ ctxt ro er true @{thm real_num_collect} t; UnparseC.term t; |
110 val SOME (t, _) = Rewrite.rewrite_ ctxt ro er true @{thm real_num_collect} t; UnparseC.term_in_ctxt @{context} t; |
111 \<close> |
111 \<close> |
112 text \<open>That is fine, we just need to add 2+4 !!!!! See the next section below. |
112 text \<open>That is fine, we just need to add 2+4 !!!!! See the next section below. |
113 |
113 |
114 But we cannot automate such ordering with what we know so far: If we put |
114 But we cannot automate such ordering with what we know so far: If we put |
115 add.assoc, add.left_commute and add.commute into one ruleset (your have used |
115 add.assoc, add.left_commute and add.commute into one ruleset (your have used |
116 ruleset 'make_polynomial' already), then all the rules are applied as long |
116 ruleset 'make_polynomial' already), then all the rules are applied as long |
117 as one rule is applicable (that is the way such rulesets work). |
117 as one rule is applicable (that is the way such rulesets work). |
118 Try to step through the ML-sections without skipping one of them ... |
118 Try to step through the ML-sections without skipping one of them ... |
119 \<close> |
119 \<close> |
120 ML \<open>val SOME (t, _) = Rewrite.rewrite_ ctxt ro er true @{thm add.commute} t; UnparseC.term t\<close> |
120 ML \<open>val SOME (t, _) = Rewrite.rewrite_ ctxt ro er true @{thm add.commute} t; UnparseC.term_in_ctxt @{context} t\<close> |
121 ML \<open>val SOME (t, _) = Rewrite.rewrite_ ctxt ro er true @{thm add.commute} t; UnparseC.term t\<close> |
121 ML \<open>val SOME (t, _) = Rewrite.rewrite_ ctxt ro er true @{thm add.commute} t; UnparseC.term_in_ctxt @{context} t\<close> |
122 ML \<open>val SOME (t, _) = Rewrite.rewrite_ ctxt ro er true @{thm add.commute} t; UnparseC.term t\<close> |
122 ML \<open>val SOME (t, _) = Rewrite.rewrite_ ctxt ro er true @{thm add.commute} t; UnparseC.term_in_ctxt @{context} t\<close> |
123 ML \<open>val SOME (t, _) = Rewrite.rewrite_ ctxt ro er true @{thm add.commute} t; UnparseC.term t\<close> |
123 ML \<open>val SOME (t, _) = Rewrite.rewrite_ ctxt ro er true @{thm add.commute} t; UnparseC.term_in_ctxt @{context} t\<close> |
124 text \<open>... you can go forever, the ruleset is 'not terminating'. |
124 text \<open>... you can go forever, the ruleset is 'not terminating'. |
125 The theory of rewriting makes this kind of rulesets terminate by the use of |
125 The theory of rewriting makes this kind of rulesets terminate by the use of |
126 'rewrite orders': |
126 'rewrite orders': |
127 Given two terms t1 and t2 we describe rewriting by: t1 ~~> t2. Then |
127 Given two terms t1 and t2 we describe rewriting by: t1 ~~> t2. Then |
128 'ordered rewriting' is: t2 < t1 ==> t1 ~~> t2. That means, a rule is only |
128 'ordered rewriting' is: t2 < t1 ==> t1 ~~> t2. That means, a rule is only |
146 Here are examples of of how ISAC's simplifier work: |
146 Here are examples of of how ISAC's simplifier work: |
147 \<close> |
147 \<close> |
148 ML \<open> |
148 ML \<open> |
149 (*show_brackets := false; TODO*) |
149 (*show_brackets := false; TODO*) |
150 val t1 = ParseC.parse_test ctxt "(a - b) * (a\<up>2 + a*b + b\<up>2)"; |
150 val t1 = ParseC.parse_test ctxt "(a - b) * (a\<up>2 + a*b + b\<up>2)"; |
151 val SOME (t, _) = Rewrite.rewrite_set_ ctxt true make_polynomial t1; UnparseC.term t; |
151 val SOME (t, _) = Rewrite.rewrite_set_ ctxt true make_polynomial t1; UnparseC.term_in_ctxt @{context} t; |
152 \<close> |
152 \<close> |
153 ML \<open> |
153 ML \<open> |
154 val t2 = ParseC.parse_test ctxt |
154 val t2 = ParseC.parse_test ctxt |
155 "(2 / (x + 3) + 2 / (x - 3)) / (8 * x / (x \<up> 2 - 9))"; |
155 "(2 / (x + 3) + 2 / (x - 3)) / (8 * x / (x \<up> 2 - 9))"; |
156 val SOME (t, _) = Rewrite.rewrite_set_ ctxt true norm_Rational t2; UnparseC.term t; |
156 val SOME (t, _) = Rewrite.rewrite_set_ ctxt true norm_Rational t2; UnparseC.term_in_ctxt @{context} t; |
157 \<close> |
157 \<close> |
158 text \<open>The simplifiers are quite busy when finding the above results. you can |
158 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> |
159 watch them at work by setting the switch 'Rewrite.trace_on:\<close> |
160 ML \<open> |
160 ML \<open> |
161 tracing "+++begin++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++"; |
161 tracing "+++begin++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++"; |
162 val SOME (t, _) = Rewrite.rewrite_set_ ctxt true norm_Rational t2; UnparseC.term t; |
162 val SOME (t, _) = Rewrite.rewrite_set_ ctxt true norm_Rational t2; UnparseC.term_in_ctxt @{context} t; |
163 tracing "+++end++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++"; |
163 tracing "+++end++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++"; |
164 \<close> |
164 \<close> |
165 text \<open>You see what happend when you click the checkbox <Tracing> on the bar |
165 text \<open>You see what happend when you click the checkbox <Tracing> on the bar |
166 separating this window from the Output-window. |
166 separating this window from the Output-window. |
167 |
167 |
185 |
185 |
186 subsection \<open>What already works\<close> |
186 subsection \<open>What already works\<close> |
187 ML \<open> |
187 ML \<open> |
188 val t2 = ParseC.parse_test ctxt |
188 val t2 = ParseC.parse_test ctxt |
189 "5*e + 6*f - 8*g - 9 - 7*e - 4*f + 10*g + 12::real"; |
189 "5*e + 6*f - 8*g - 9 - 7*e - 4*f + 10*g + 12::real"; |
190 val SOME (t, _) = Rewrite.rewrite_set_ ctxt true rls_p_33 t2; UnparseC.term t; |
190 val SOME (t, _) = Rewrite.rewrite_set_ ctxt true rls_p_33 t2; UnparseC.term_in_ctxt @{context} t; |
191 \<close> |
191 \<close> |
192 text \<open>Try your own examples !\<close> |
192 text \<open>Try your own examples !\<close> |
193 |
193 |
194 subsection \<open>This raises questions about didactics\<close> |
194 subsection \<open>This raises questions about didactics\<close> |
195 text \<open>Oberserve the '-' ! That works out. But see the efforts in PolyMinus.thy |
195 text \<open>Oberserve the '-' ! That works out. But see the efforts in PolyMinus.thy |