equal
deleted
inserted
replaced
39 (@{theory "Isac_Knowledge"}, tless_true, eval_rls, [(@{term "bdv::real"}, @{term "x::real"})]); |
39 (@{theory "Isac_Knowledge"}, tless_true, eval_rls, [(@{term "bdv::real"}, @{term "x::real"})]); |
40 val ctxt = Proof_Context.init_global thy; (*required for parsing*) |
40 val ctxt = Proof_Context.init_global thy; (*required for parsing*) |
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 = 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 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 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 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 t; |
78 |
78 |
79 section \<open>Conditional and ordered rewriting\<close> |
79 section \<open>Conditional and ordered rewriting\<close> |
80 text \<open>We have already seen conditional rewriting above when we used the rule |
80 text \<open>We have already seen conditional rewriting above when we used the rule |
81 diff_const; let us try:\<close> |
81 diff_const; let us try:\<close> |
82 ML \<open> |
82 ML \<open> |
83 val t1 = TermC.parseNEW' ctxt "d_d x (a*BC*x*z)"; |
83 val t1 = ParseC.parse_test ctxt "d_d x (a*BC*x*z)"; |
84 Rewrite.rewrite_inst_ ctxt ro er true inst diff_const t1; |
84 Rewrite.rewrite_inst_ ctxt ro er true inst diff_const t1; |
85 |
85 |
86 val t2 = TermC.parseNEW' ctxt "d_d x (a*BC*y*z)"; |
86 val t2 = ParseC.parse_test ctxt "d_d x (a*BC*y*z)"; |
87 Rewrite.rewrite_inst_ ctxt ro er true inst diff_const t2; |
87 Rewrite.rewrite_inst_ ctxt ro er true inst diff_const t2; |
88 \<close> |
88 \<close> |
89 text \<open>For term t1 the assumption 'not (x occurs_in "a*BC*x*z")' is false, |
89 text \<open>For term t1 the assumption 'not (x occurs_in "a*BC*x*z")' is false, |
90 since x occurs in t1 actually; thus the rule following implication '==>' is |
90 since x occurs in t1 actually; thus the rule following implication '==>' is |
91 not applied and rewrite_inst_ returns NONE. |
91 not applied and rewrite_inst_ returns NONE. |
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 = TermC.parseNEW' 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 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> |
145 |
145 |
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 = TermC.parseNEW' 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 t; |
152 \<close> |
152 \<close> |
153 ML \<open> |
153 ML \<open> |
154 val t2 = TermC.parseNEW' 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 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> |
183 $ISABELLE_ISAC/Knowledge/PolyMinus.thy |
183 $ISABELLE_ISAC/Knowledge/PolyMinus.thy |
184 \<close> |
184 \<close> |
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 = TermC.parseNEW' 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 t; |
191 \<close> |
191 \<close> |
192 text \<open>Try your own examples !\<close> |
192 text \<open>Try your own examples !\<close> |
193 |
193 |
223 without '-' ? |
223 without '-' ? |
224 \<close> |
224 \<close> |
225 |
225 |
226 subsection \<open>This does not yet work\<close> |
226 subsection \<open>This does not yet work\<close> |
227 ML \<open> |
227 ML \<open> |
228 val t = TermC.parseNEW' ctxt |
228 val t = ParseC.parse_test ctxt |
229 "(2*a - 5*b) * (2*a + 5*b)"; |
229 "(2*a - 5*b) * (2*a + 5*b)"; |
230 Rewrite.rewrite_set_ ctxt true rls_p_33 t; UnparseC.term t; |
230 Rewrite.rewrite_set_ ctxt true rls_p_33 t; UnparseC.term t; |
231 \<close> |
231 \<close> |
232 |
232 |
233 end |
233 end |