neuper@38067
|
1 |
(*
|
neuper@38077
|
2 |
cd /usr/local/Isabelle/test/Tools/isac/ADDTESTS/course/
|
neuper@38077
|
3 |
/usr/local/Isabelle/bin/isabelle jedit -l Isac T2_Rewriting.thy &
|
neuper@38067
|
4 |
*)
|
neuper@38067
|
5 |
|
neuper@38067
|
6 |
theory T2_Rewriting imports Isac begin
|
neuper@38067
|
7 |
|
neuper@38067
|
8 |
section {* Rewriting *}
|
neuper@38067
|
9 |
|
neuper@38077
|
10 |
text {* \emph{Rewriting} is a technique of Symbolic Computation, which is
|
neuper@38077
|
11 |
appropriate to make a 'transparent system', because it is intuitively
|
neuper@38077
|
12 |
comprehensible. For a thourogh introduction see the book of Tobias Nipkow,
|
neuper@38067
|
13 |
http://www4.informatik.tu-muenchen.de/~nipkow/TRaAT/
|
neuper@38067
|
14 |
|
neuper@38077
|
15 |
subsection {* Introduction to rewriting *}
|
neuper@38067
|
16 |
|
neuper@38067
|
17 |
text {* Rewriting creates calculations which look like written by hand; see the
|
neuper@38067
|
18 |
ISAC tutoring system ! ISAC finds the rules automatically. Here we start by
|
neuper@38077
|
19 |
telling the rules ourselves.
|
neuper@38077
|
20 |
Let's differentiate after we have identified the rules for differentiation, as
|
neuper@38077
|
21 |
found in ~~/src/Tools/isac/Knowledge/Diff.thy:
|
neuper@38077
|
22 |
*}
|
neuper@38077
|
23 |
ML {*
|
neuper@38077
|
24 |
val diff_sum = num_str @{thm diff_sum};
|
neuper@38077
|
25 |
val diff_pow = num_str @{thm diff_pow};
|
neuper@38077
|
26 |
val diff_var = num_str @{thm diff_var};
|
neuper@38077
|
27 |
val diff_const = num_str @{thm diff_const};
|
neuper@38077
|
28 |
*}
|
neuper@38077
|
29 |
text {* Looking at the rules (abbreviated by 'thm' above), we see the
|
neuper@38077
|
30 |
differential operator abbreviated by 'd_d ?bdv', where '?bdv' is the bound
|
neuper@38077
|
31 |
variable.
|
neuper@38077
|
32 |
Can you read diff_const in the Ouput window ?
|
neuper@38067
|
33 |
|
neuper@38077
|
34 |
Please, skip this introductory ML-section in the first go ...*}
|
neuper@38077
|
35 |
ML {*
|
neuper@38077
|
36 |
print_depth 1;
|
neuper@38077
|
37 |
val (thy, ro, er, inst) =
|
neuper@38077
|
38 |
(theory "Isac", tless_true, eval_rls, [(@{term "bdv::real"}, @{term "x::real"})]);
|
neuper@38077
|
39 |
*}
|
neuper@38077
|
40 |
text {* ... and let us differentiate the term t: *}
|
neuper@38077
|
41 |
ML {*
|
neuper@38077
|
42 |
val t = (term_of o the o (parse thy)) "d_d x (x^^^2 + x + y)";
|
neuper@38067
|
43 |
|
neuper@38077
|
44 |
val SOME (t, _) = rewrite_inst_ thy ro er true inst diff_sum t; term2str t;
|
neuper@38077
|
45 |
val SOME (t, _) = rewrite_inst_ thy ro er true inst diff_sum t; term2str t;
|
neuper@38077
|
46 |
val SOME (t, _) = rewrite_inst_ thy ro er true inst diff_pow t; term2str t;
|
neuper@38077
|
47 |
val SOME (t, _) = rewrite_inst_ thy ro er true inst diff_var t; term2str t;
|
neuper@38077
|
48 |
val SOME (t, _) = rewrite_inst_ thy ro er true inst diff_const t; term2str t;
|
neuper@38077
|
49 |
*}
|
neuper@38077
|
50 |
text {* Please, scoll up the Output-window to check the 5 steps of rewriting !
|
neuper@38077
|
51 |
You might not be satisfied by the result "2 * x ^^^ (2 - 1) + 1 + 0".
|
neuper@38067
|
52 |
|
neuper@38077
|
53 |
ISAC has a set of rules called 'make_polynomial', which simplifies the result:
|
neuper@38077
|
54 |
*}
|
neuper@38077
|
55 |
ML {*
|
neuper@38077
|
56 |
val SOME (t, _) = rewrite_set_ thy true make_polynomial t; term2str t;
|
neuper@38077
|
57 |
trace_rewrite := false;
|
neuper@38067
|
58 |
*}
|
neuper@38067
|
59 |
|
neuper@38077
|
60 |
subsection {* Note on bound variables *}
|
neuper@38077
|
61 |
text {* You may have noticed that rewrite_ above could distinguish between x
|
neuper@38077
|
62 |
(d_d x x = 1) and y (d_d x y = 0). ISAC does this by instantiating theorems
|
neuper@38077
|
63 |
before application: given [(@{term "bdv::real"}, @{term "x::real"})] the
|
neuper@38077
|
64 |
theorem diff_sum becomes "d_d x (?u + ?v) = d_d x ?u + d_d x ?v".
|
neuper@38077
|
65 |
|
neuper@38077
|
66 |
Isabelle does this differently by variables bound by a 'lambda' %, see
|
neuper@38077
|
67 |
http://isabelle.in.tum.de/dist/library/HOL/HOL-Multivariate_Analysis/Derivative.html
|
neuper@38077
|
68 |
*}
|
neuper@38067
|
69 |
ML {*
|
neuper@38077
|
70 |
val t = @{term "%x. x^2 + x + y"}; atomwy t; term2str t;
|
neuper@38077
|
71 |
*}
|
neuper@38077
|
72 |
text {* Since this notation does not conform to present high-school matheatics
|
neuper@38077
|
73 |
ISAC introduced the 'bdv' mechanism. This mechanism is also used for equation
|
neuper@38077
|
74 |
solving in ISAC.
|
neuper@38067
|
75 |
*}
|
neuper@38067
|
76 |
|
neuper@38077
|
77 |
subsection {* Conditional and ordered rewriting *}
|
neuper@38077
|
78 |
text {* We have already seen conditional rewriting above when we used the rule
|
neuper@38077
|
79 |
diff_const; let us try: *}
|
neuper@38077
|
80 |
ML {*
|
neuper@38077
|
81 |
val t1 = (term_of o the o (parse thy)) "d_d x (a*BC*x*z)";
|
neuper@38077
|
82 |
rewrite_inst_ thy ro er true inst diff_const t1;
|
neuper@38077
|
83 |
|
neuper@38077
|
84 |
val t2 = (term_of o the o (parse thy)) "d_d x (a*BC*y*z)";
|
neuper@38077
|
85 |
rewrite_inst_ thy ro er true inst diff_const t2;
|
neuper@38077
|
86 |
*}
|
neuper@38077
|
87 |
text {* For term t1 the assumption 'not (x occurs_in "a*BC*x*z")' is false,
|
neuper@38077
|
88 |
since x occurs in t1 actually; thus the rule following implication '==>' is
|
neuper@38077
|
89 |
not applied and rewrite_inst_ returns NONE.
|
neuper@38077
|
90 |
For term t2 is 'not (x occurs_in "a*BC*y*z")' true, thus the rule is applied.
|
neuper@38067
|
91 |
*}
|
neuper@38067
|
92 |
|
neuper@38077
|
93 |
subsubsection {* ordered rewriting *}
|
neuper@38077
|
94 |
text {* Let us start with an example; in order to see what is going on we tell
|
neuper@38077
|
95 |
Isabelle to show all brackets:
|
neuper@38077
|
96 |
*}
|
neuper@38067
|
97 |
ML {*
|
neuper@38077
|
98 |
show_brackets := true;
|
neuper@38077
|
99 |
val t0 = (term_of o the o (parse thy)) "2*a + 3*b + 4*a"; term2str t0;
|
neuper@38077
|
100 |
(*show_brackets := false;*)
|
neuper@38077
|
101 |
*}
|
neuper@38077
|
102 |
text {* Now we want to bring 4*a close to 2*a in order to get 6*a:
|
neuper@38077
|
103 |
*}
|
neuper@38077
|
104 |
ML {*
|
neuper@38077
|
105 |
val SOME (t, _) = rewrite_ thy ro er true @{thm add_assoc} t0; term2str t;
|
neuper@38077
|
106 |
val SOME (t, _) = rewrite_ thy ro er true @{thm add_left_commute} t; term2str t;
|
neuper@38077
|
107 |
val SOME (t, _) = rewrite_ thy ro er true @{thm add_commute} t; term2str t;
|
neuper@38077
|
108 |
val SOME (t, _) = rewrite_ thy ro er true @{thm real_num_collect} t; term2str t;
|
neuper@38077
|
109 |
*}
|
neuper@38077
|
110 |
text {* That is fine, we just need to add 2+4 !!!!! See the next section below.
|
neuper@38077
|
111 |
|
neuper@38077
|
112 |
But we cannot automate such ordering with what we know so far: If we put
|
neuper@38077
|
113 |
add_assoc, add_left_commute and add_commute into one ruleset (your have used
|
neuper@38077
|
114 |
ruleset 'make_polynomial' already), then all the rules are applied as long
|
neuper@38077
|
115 |
as one rule is applicable (that is the way such rulesets work).
|
neuper@38077
|
116 |
Try to step through the ML-sections without skipping one of them ...
|
neuper@38077
|
117 |
*}
|
neuper@38077
|
118 |
ML {*val SOME (t, _) = rewrite_ thy ro er true @{thm add_commute} t; term2str t*}
|
neuper@38077
|
119 |
ML {*val SOME (t, _) = rewrite_ thy ro er true @{thm add_commute} t; term2str t*}
|
neuper@38077
|
120 |
ML {*val SOME (t, _) = rewrite_ thy ro er true @{thm add_commute} t; term2str t*}
|
neuper@38077
|
121 |
ML {*val SOME (t, _) = rewrite_ thy ro er true @{thm add_commute} t; term2str t*}
|
neuper@38077
|
122 |
text {* ... you can go forever, the ruleset is 'not terminating'.
|
neuper@38077
|
123 |
The theory of rewriting makes this kind of rulesets terminate by the use of
|
neuper@38077
|
124 |
'rewrite orders':
|
neuper@38077
|
125 |
Given two terms t1 and t2 we describe rewriting by: t1 ~~> t2. Then
|
neuper@38077
|
126 |
'ordered rewriting' is: t2 < t1 ==> t1 ~~> t2. That means, a rule is only
|
neuper@38077
|
127 |
applied, when the result t2 is 'smaller', '<', than the one to be rewritten.
|
neuper@38077
|
128 |
Defining such a '<' is not trivial, see ~~/src/Tools/isacKnowledge/Poly.thy
|
neuper@38077
|
129 |
for 'fun has_degree_in' etc.
|
neuper@38067
|
130 |
*}
|
neuper@38067
|
131 |
|
neuper@38077
|
132 |
subsection {* Simplification in ISAC *}
|
neuper@38077
|
133 |
text {*
|
neuper@38077
|
134 |
With the introduction into rewriting, ordered rewriting and conditional
|
neuper@38077
|
135 |
rewriting we have seen all what is necessary for the practice of rewriting.
|
neuper@38077
|
136 |
|
neuper@38077
|
137 |
One basic technique of 'symbolic computation' which uses rewriting is
|
neuper@38077
|
138 |
simplification, that means: transform terms into an equivalent form which is
|
neuper@38077
|
139 |
as simple as possible.
|
neuper@38077
|
140 |
Isabelle has powerful and efficient simplifiers. Nevertheless, ISAC has another
|
neuper@38077
|
141 |
kind of simplifiers, which groups rulesets such that the trace of rewrites is
|
neuper@38077
|
142 |
more readable in ISAC's worksheets.
|
neuper@38077
|
143 |
|
neuper@38077
|
144 |
Here are examples of of how ISAC's simplifier work:
|
neuper@38077
|
145 |
*}
|
neuper@38077
|
146 |
ML {*
|
neuper@38077
|
147 |
show_brackets := false;
|
neuper@38077
|
148 |
val t1 = (term_of o the o (parse thy)) "(a - b) * (a^^^2 + a*b + b^^^2)";
|
neuper@38077
|
149 |
val SOME (t, _) = rewrite_set_ thy true make_polynomial t1; term2str t;
|
neuper@38077
|
150 |
*}
|
neuper@38077
|
151 |
ML {*
|
neuper@38077
|
152 |
val t2 = (term_of o the o (parse thy))
|
neuper@38077
|
153 |
"(2 / (x + 3) + 2 / (x - 3)) / (8 * x / (x ^^^ 2 - 9))";
|
neuper@38077
|
154 |
val SOME (t, _) = rewrite_set_ thy true norm_Rational t2; term2str t;
|
neuper@38077
|
155 |
*}
|
neuper@38077
|
156 |
text {* The simplifiers are quite busy when finding the above results. you can
|
neuper@38077
|
157 |
watch them at work by setting the switch 'trace_rewrite:*}
|
neuper@38077
|
158 |
ML {*
|
neuper@38077
|
159 |
trace_rewrite := true;
|
neuper@38077
|
160 |
tracing "+++begin++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++";
|
neuper@38077
|
161 |
val SOME (t, _) = rewrite_set_ thy true norm_Rational t2; term2str t;
|
neuper@38077
|
162 |
tracing "+++end++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++";
|
neuper@38077
|
163 |
trace_rewrite := false;
|
neuper@38077
|
164 |
*}
|
neuper@38077
|
165 |
text {* You see what happend when you click the checkbox <Tracing> on the bar
|
neuper@38077
|
166 |
separating this window from the Output-window.
|
neuper@38077
|
167 |
|
neuper@38077
|
168 |
So, it might be better to take simpler examples for watching the simplifiers.
|
neuper@38067
|
169 |
*}
|
neuper@38067
|
170 |
|
neuper@38077
|
171 |
|
neuper@38077
|
172 |
section {* Experiments with a simplifier conserving minus *}
|
neuper@38077
|
173 |
|
neuper@38077
|
174 |
text {* We conclude the section on rewriting with starting into an experimental
|
neuper@38077
|
175 |
development. This development has been urged by teachers using ISAC for
|
neuper@38077
|
176 |
introduction to algebra with students at the age of 12-14.
|
neuper@38077
|
177 |
|
neuper@38077
|
178 |
The teachers requested ISAC to keep the minus, for instance in the above
|
neuper@38077
|
179 |
result "a^3 + -1 * b^3" (here ISAC should write "a^3 - * b^3") and also
|
neuper@38077
|
180 |
in all intermediate steps.
|
neuper@38077
|
181 |
|
neuper@38077
|
182 |
So we started to develop (in German !) such a simplifier in
|
neuper@38077
|
183 |
~~/src/Tools/isac/Knowledge/PolyMinus.thy
|
neuper@38067
|
184 |
*}
|
neuper@38067
|
185 |
|
neuper@38077
|
186 |
subsection {* What already works *}
|
neuper@38077
|
187 |
ML {*
|
neuper@38077
|
188 |
val t2 = (term_of o the o (parse thy))
|
neuper@38077
|
189 |
"- r - 2 * s - 3 * t + 5 + 4 * r + 8 * s - 5 * t - 2";
|
neuper@38077
|
190 |
val SOME (t, _) = rewrite_set_ thy true rls_p_33 t2; term2str t;
|
neuper@38077
|
191 |
*}
|
neuper@38077
|
192 |
text {* Try your own examples ! *}
|
neuper@38067
|
193 |
|
neuper@38077
|
194 |
subsection {* This raises questions about didactics *}
|
neuper@38077
|
195 |
text {* Oberserve the '-' ! That works out. But see the efforts in PolyMinus.thy
|
neuper@38077
|
196 |
*}
|
neuper@38077
|
197 |
ML {*
|
neuper@38077
|
198 |
@{thm subtrahiere};
|
neuper@38077
|
199 |
@{thm subtrahiere_von_1};
|
neuper@38077
|
200 |
@{thm subtrahiere_1};
|
neuper@38077
|
201 |
*}
|
neuper@38077
|
202 |
text {* That would not be so bad. But it is only a little part of what else is
|
neuper@38077
|
203 |
required:
|
neuper@38077
|
204 |
*}
|
neuper@38077
|
205 |
ML {*
|
neuper@38077
|
206 |
@{thm subtrahiere_x_plus_minus};
|
neuper@38077
|
207 |
@{thm subtrahiere_x_plus1_minus};
|
neuper@38077
|
208 |
@{thm subtrahiere_x_plus_minus1};
|
neuper@38077
|
209 |
@{thm subtrahiere_x_minus_plus};
|
neuper@38077
|
210 |
@{thm subtrahiere_x_minus1_plus};
|
neuper@38077
|
211 |
@{thm subtrahiere_x_minus_plus1};
|
neuper@38077
|
212 |
@{thm subtrahiere_x_minus_minus};
|
neuper@38077
|
213 |
@{thm subtrahiere_x_minus1_minus};
|
neuper@38077
|
214 |
@{thm subtrahiere_x_minus_minus1};
|
neuper@38077
|
215 |
*}
|
neuper@38077
|
216 |
text {* So, learning so many rules, and learning to apply these rules, is futile.
|
neuper@38077
|
217 |
Actually, most of our students are unable to apply theorems.
|
neuper@38077
|
218 |
|
neuper@38077
|
219 |
But if you look at 'make_polynomial' or even 'norm_Rational' you see,
|
neuper@38077
|
220 |
that these general simplifiers require about 10% than rulesets for '-'.
|
neuper@38077
|
221 |
|
neuper@38077
|
222 |
So, we might have better chances to teach our student to apply theorems
|
neuper@38077
|
223 |
without '-' ?
|
neuper@38077
|
224 |
*}
|
neuper@38077
|
225 |
|
neuper@38077
|
226 |
subsection {* This does not yet work *}
|
neuper@38077
|
227 |
ML {*
|
neuper@38077
|
228 |
val t = (term_of o the o (parse thy))
|
neuper@38077
|
229 |
"(2*a - 5*b) * (2*a + 5*b)";
|
neuper@38077
|
230 |
rewrite_set_ thy true rls_p_33 t; term2str t;
|
neuper@38067
|
231 |
*}
|
neuper@38067
|
232 |
|
neuper@38067
|
233 |
end
|