2 cd /usr/local/Isabelle/test/Tools/isac/ADDTESTS/course/
3 /usr/local/Isabelle/bin/isabelle jedit -l Isac T2_Rewriting.thy &
6 theory T2_Rewriting imports Isac.Isac_Knowledge
9 chapter \<open>Rewriting\<close>
11 text \<open>\emph{Rewriting} is a technique of Symbolic Computation, which is
12 appropriate to make a 'transparent system', because it is intuitively
13 comprehensible. For a thourogh introduction see the book of Tobias Nipkow,
14 http://www4.informatik.tu-muenchen.de/~nipkow/TRaAT/
16 section {* Introduction to rewriting\<close>
18 text \<open>Rewriting creates calculations which look like written by hand; see the
19 ISAC tutoring system ! ISAC finds the rules automatically. Here we start by
20 telling the rules ourselves.
21 Let's differentiate after we have identified the rules for differentiation, as
22 found in $ISABELLE_ISAC/Knowledge/Diff.thy:
25 val diff_sum = @{thm diff_sum};
26 val diff_pow = @{thm diff_pow};
27 val diff_var = @{thm diff_var};
28 val diff_const = @{thm diff_const};
30 text \<open>Looking at the rules (abbreviated by 'thm' above), we see the
31 differential operator abbreviated by 'd_d ?bdv', where '?bdv' is the bound
33 Can you read diff_const in the Ouput window ?
35 Please, skip this introductory ML-section in the first go ...\<close>
37 (*default_print_depth 1;*)
38 val (thy, ro, er, inst) =
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*)
42 text \<open>... and let us differentiate the term t:\<close>
44 val t = TermC.parseNEW' ctxt "d_d x (x\<up>2 + x + y)";
46 val SOME (t, _) = Rewrite.rewrite_inst_ thy 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;
48 val SOME (t, _) = Rewrite.rewrite_inst_ thy 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;
50 val SOME (t, _) = Rewrite.rewrite_inst_ thy ro er true inst diff_const t; UnparseC.term t;
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".
55 ISAC has a set of rules called 'make_polynomial', which simplifies the result:
58 val SOME (t, _) = Rewrite.rewrite_set_ thy true make_polynomial t; UnparseC.term t;
59 Rewrite.trace_on := false; (*true false*)
62 section \<open>Note on bound variables\<close>
63 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
65 before application: given [(@{term "bdv::real"}, @{term "x::real"})] the
66 theorem diff_sum becomes "d_d x (?u + ?v) = d_d x ?u + d_d x ?v".
68 Isabelle does this differently by variables bound by a 'lambda' %, see
69 http://isabelle.in.tum.de/dist/library/HOL/HOL-Multivariate_Analysis/Derivative.html
72 val t = @{term "%x. x^2 + x + y"}; TermC.atomwy t; UnparseC.term t;
74 text \<open>Since this notation does not conform to present high-school matheatics
75 ISAC introduced the 'bdv' mechanism. This mechanism is also used for equation
79 section \<open>Conditional and ordered rewriting\<close>
80 text \<open>We have already seen conditional rewriting above when we used the rule
81 diff_const; let us try:\<close>
83 val t1 = TermC.parseNEW' ctxt "d_d x (a*BC*x*z)";
84 Rewrite.rewrite_inst_ thy ro er true inst diff_const t1;
86 val t2 = TermC.parseNEW' ctxt "d_d x (a*BC*y*z)";
87 Rewrite.rewrite_inst_ thy ro er true inst diff_const t2;
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
91 not applied and rewrite_inst_ returns NONE.
92 For term t2 is 'not (x occurs_in "a*BC*y*z")' true, thus the rule is applied.
95 subsection \<open>ordered rewriting\<close>
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:
100 (*show_brackets := true; TODO*)
101 val t0 = TermC.parseNEW' ctxt "2*a + 3*b + 4*a::real"; UnparseC.term t0;
102 (*show_brackets := false;*)
104 text \<open>Now we want to bring 4*a close to 2*a in order to get 6*a:
107 val SOME (t, _) = Rewrite.rewrite_ thy ro er true @{thm add.assoc} t0; UnparseC.term t;
108 val SOME (t, _) = Rewrite.rewrite_ thy ro er true @{thm add.left_commute} t; UnparseC.term t;
109 val SOME (t, _) = Rewrite.rewrite_ thy ro er true @{thm add.commute} t; UnparseC.term t;
110 val SOME (t, _) = Rewrite.rewrite_ thy ro er true @{thm real_num_collect} t; UnparseC.term t;
112 text \<open>That is fine, we just need to add 2+4 !!!!! See the next section below.
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
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).
118 Try to step through the ML-sections without skipping one of them ...
120 ML \<open>val SOME (t, _) = Rewrite.rewrite_ thy ro er true @{thm add.commute} t; UnparseC.term t\<close>
121 ML \<open>val SOME (t, _) = Rewrite.rewrite_ thy ro er true @{thm add.commute} t; UnparseC.term t\<close>
122 ML \<open>val SOME (t, _) = Rewrite.rewrite_ thy ro er true @{thm add.commute} t; UnparseC.term t\<close>
123 ML \<open>val SOME (t, _) = Rewrite.rewrite_ thy ro er true @{thm add.commute} t; UnparseC.term t\<close>
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
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
129 applied, when the result t2 is 'smaller', '<', than the one to be rewritten.
130 Defining such a '<' is not trivial, see ~~/src/Tools/isacKnowledge/Poly.thy
131 for 'fun has_degree_in' etc.
134 subsection \<open>Simplification in ISAC\<close>
136 With the introduction into rewriting, ordered rewriting and conditional
137 rewriting we have seen all what is necessary for the practice of rewriting.
139 One basic technique of 'symbolic computation' which uses rewriting is
140 simplification, that means: transform terms into an equivalent form which is
141 as simple as possible.
142 Isabelle has powerful and efficient simplifiers. Nevertheless, ISAC has another
143 kind of simplifiers, which groups rulesets such that the trace of rewrites is
144 more readable in ISAC's worksheets.
146 Here are examples of of how ISAC's simplifier work:
149 (*show_brackets := false; TODO*)
150 val t1 = TermC.parseNEW' ctxt "(a - b) * (a\<up>2 + a*b + b\<up>2)";
151 val SOME (t, _) = Rewrite.rewrite_set_ thy true make_polynomial t1; UnparseC.term t;
154 val t2 = TermC.parseNEW' ctxt
155 "(2 / (x + 3) + 2 / (x - 3)) / (8 * x / (x \<up> 2 - 9))";
156 val SOME (t, _) = Rewrite.rewrite_set_ thy true norm_Rational t2; UnparseC.term t;
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>
161 Rewrite.trace_on := false; (*true false*)
162 tracing "+++begin++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++";
163 val SOME (t, _) = Rewrite.rewrite_set_ thy true norm_Rational t2; UnparseC.term t;
164 tracing "+++end++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++";
165 Rewrite.trace_on := false; (*true false*)
167 text \<open>You see what happend when you click the checkbox <Tracing> on the bar
168 separating this window from the Output-window.
170 So, it might be better to take simpler examples for watching the simplifiers.
174 section \<open>Experiments with a simplifier conserving minus\<close>
176 text \<open>We conclude the section on rewriting with starting into an experimental
177 development. This development has been urged by teachers using ISAC for
178 introduction to algebra with students at the age of 12-14.
180 The teachers requested ISAC to keep the minus, for instance in the above
181 result "a^3 + -1 * b^3" (here ISAC should write "a^3 - * b^3") and also
182 in all intermediate steps.
184 So we started to develop (in German !) such a simplifier in
185 $ISABELLE_ISAC/Knowledge/PolyMinus.thy
188 subsection \<open>What already works\<close>
190 val t2 = TermC.parseNEW' ctxt
191 "5*e + 6*f - 8*g - 9 - 7*e - 4*f + 10*g + 12::real";
192 val SOME (t, _) = Rewrite.rewrite_set_ thy true rls_p_33 t2; UnparseC.term t;
194 text \<open>Try your own examples !\<close>
196 subsection \<open>This raises questions about didactics\<close>
197 text \<open>Oberserve the '-' ! That works out. But see the efforts in PolyMinus.thy
201 @{thm subtrahiere_von_1};
202 @{thm subtrahiere_1};
204 text \<open>That would not be so bad. But it is only a little part of what else is
208 @{thm subtrahiere_x_plus_minus};
209 @{thm subtrahiere_x_plus1_minus};
210 @{thm subtrahiere_x_plus_minus1};
211 @{thm subtrahiere_x_minus_plus};
212 @{thm subtrahiere_x_minus1_plus};
213 @{thm subtrahiere_x_minus_plus1};
214 @{thm subtrahiere_x_minus_minus};
215 @{thm subtrahiere_x_minus1_minus};
216 @{thm subtrahiere_x_minus_minus1};
218 text \<open>So, learning so many rules, and learning to apply these rules, is futile.
219 Actually, most of our students are unable to apply theorems.
221 But if you look at 'make_polynomial' or even 'norm_Rational' you see,
222 that these general simplifiers require about 10% than rulesets for '-'.
224 So, we might have better chances to teach our student to apply theorems
228 subsection \<open>This does not yet work\<close>
230 val t = TermC.parseNEW' ctxt
231 "(2*a - 5*b) * (2*a + 5*b)";
232 Rewrite.rewrite_set_ thy true rls_p_33 t; UnparseC.term t;