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 |
|
wneuper@59592
|
6 |
theory T2_Rewriting imports Isac.Isac_Knowledge
|
wneuper@59460
|
7 |
begin
|
neuper@38067
|
8 |
|
wneuper@59472
|
9 |
chapter \<open>Rewriting\<close>
|
neuper@38067
|
10 |
|
wneuper@59472
|
11 |
text \<open>\emph{Rewriting} is a technique of Symbolic Computation, which is
|
neuper@38077
|
12 |
appropriate to make a 'transparent system', because it is intuitively
|
neuper@38077
|
13 |
comprehensible. For a thourogh introduction see the book of Tobias Nipkow,
|
neuper@38067
|
14 |
http://www4.informatik.tu-muenchen.de/~nipkow/TRaAT/
|
neuper@38067
|
15 |
|
wneuper@59472
|
16 |
section {* Introduction to rewriting\<close>
|
neuper@38067
|
17 |
|
wneuper@59472
|
18 |
text \<open>Rewriting creates calculations which look like written by hand; see the
|
neuper@38067
|
19 |
ISAC tutoring system ! ISAC finds the rules automatically. Here we start by
|
neuper@38077
|
20 |
telling the rules ourselves.
|
neuper@38077
|
21 |
Let's differentiate after we have identified the rules for differentiation, as
|
wenzelm@60192
|
22 |
found in $ISABELLE_ISAC/Knowledge/Diff.thy:
|
wneuper@59472
|
23 |
\<close>
|
wneuper@59472
|
24 |
ML \<open>
|
Walther@60424
|
25 |
val diff_sum = @{thm diff_sum};
|
Walther@60424
|
26 |
val diff_pow = @{thm diff_pow};
|
Walther@60424
|
27 |
val diff_var = @{thm diff_var};
|
Walther@60424
|
28 |
val diff_const = @{thm diff_const};
|
wneuper@59472
|
29 |
\<close>
|
wneuper@59472
|
30 |
text \<open>Looking at the rules (abbreviated by 'thm' above), we see the
|
neuper@38077
|
31 |
differential operator abbreviated by 'd_d ?bdv', where '?bdv' is the bound
|
neuper@38077
|
32 |
variable.
|
neuper@38077
|
33 |
Can you read diff_const in the Ouput window ?
|
neuper@38067
|
34 |
|
wneuper@59472
|
35 |
Please, skip this introductory ML-section in the first go ...\<close>
|
wneuper@59472
|
36 |
ML \<open>
|
wneuper@59348
|
37 |
(*default_print_depth 1;*)
|
neuper@38077
|
38 |
val (thy, ro, er, inst) =
|
wneuper@59592
|
39 |
(@{theory "Isac_Knowledge"}, tless_true, eval_rls, [(@{term "bdv::real"}, @{term "x::real"})]);
|
Walther@60424
|
40 |
val ctxt = Proof_Context.init_global thy; (*required for parsing*)
|
wneuper@59472
|
41 |
\<close>
|
wneuper@59472
|
42 |
text \<open>... and let us differentiate the term t:\<close>
|
wneuper@59472
|
43 |
ML \<open>
|
Walther@60424
|
44 |
val t = TermC.parseNEW' ctxt "d_d x (x\<up>2 + x + y)";
|
neuper@38067
|
45 |
|
Walther@60501
|
46 |
val SOME (t, _) = Rewrite.rewrite_inst_ ctxt ro er true inst diff_sum t; UnparseC.term t;
|
Walther@60501
|
47 |
val SOME (t, _) = Rewrite.rewrite_inst_ ctxt ro er true inst diff_sum t; UnparseC.term t;
|
Walther@60501
|
48 |
val SOME (t, _) = Rewrite.rewrite_inst_ ctxt ro er true inst diff_pow t; UnparseC.term t;
|
Walther@60501
|
49 |
val SOME (t, _) = Rewrite.rewrite_inst_ ctxt ro er true inst diff_var t; UnparseC.term t;
|
Walther@60501
|
50 |
val SOME (t, _) = Rewrite.rewrite_inst_ ctxt ro er true inst diff_const t; UnparseC.term t;
|
wneuper@59472
|
51 |
\<close>
|
wneuper@59472
|
52 |
text \<open>Please, scoll up the Output-window to check the 5 steps of rewriting !
|
walther@60242
|
53 |
You might not be satisfied by the result "2 * x \<up> (2 - 1) + 1 + 0".
|
neuper@38067
|
54 |
|
neuper@38077
|
55 |
ISAC has a set of rules called 'make_polynomial', which simplifies the result:
|
wneuper@59472
|
56 |
\<close>
|
wneuper@59472
|
57 |
ML \<open>
|
Walther@60501
|
58 |
val SOME (t, _) = Rewrite.rewrite_set_ ctxt true make_polynomial t; UnparseC.term t;
|
wneuper@59472
|
59 |
\<close>
|
neuper@38067
|
60 |
|
wneuper@59472
|
61 |
section \<open>Note on bound variables\<close>
|
wneuper@59472
|
62 |
text \<open>You may have noticed that rewrite_ above could distinguish between x
|
neuper@38077
|
63 |
(d_d x x = 1) and y (d_d x y = 0). ISAC does this by instantiating theorems
|
neuper@38077
|
64 |
before application: given [(@{term "bdv::real"}, @{term "x::real"})] the
|
neuper@38077
|
65 |
theorem diff_sum becomes "d_d x (?u + ?v) = d_d x ?u + d_d x ?v".
|
neuper@38077
|
66 |
|
neuper@38077
|
67 |
Isabelle does this differently by variables bound by a 'lambda' %, see
|
neuper@38077
|
68 |
http://isabelle.in.tum.de/dist/library/HOL/HOL-Multivariate_Analysis/Derivative.html
|
wneuper@59472
|
69 |
\<close>
|
wneuper@59472
|
70 |
ML \<open>
|
Walther@60650
|
71 |
val t = @{term "%x. x^2 + x + y"};
|
Walther@60650
|
72 |
TermC.atom_write_detail @{context} t; UnparseC.term_in_ctxt @{context} t;
|
wneuper@59472
|
73 |
\<close>
|
wneuper@59472
|
74 |
text \<open>Since this notation does not conform to present high-school matheatics
|
neuper@38077
|
75 |
ISAC introduced the 'bdv' mechanism. This mechanism is also used for equation
|
neuper@38077
|
76 |
solving in ISAC.
|
wneuper@59472
|
77 |
\<close>
|
neuper@38067
|
78 |
|
wneuper@59472
|
79 |
section \<open>Conditional and ordered rewriting\<close>
|
wneuper@59472
|
80 |
text \<open>We have already seen conditional rewriting above when we used the rule
|
wneuper@59472
|
81 |
diff_const; let us try:\<close>
|
wneuper@59472
|
82 |
ML \<open>
|
Walther@60424
|
83 |
val t1 = TermC.parseNEW' ctxt "d_d x (a*BC*x*z)";
|
Walther@60500
|
84 |
Rewrite.rewrite_inst_ ctxt ro er true inst diff_const t1;
|
neuper@38077
|
85 |
|
Walther@60424
|
86 |
val t2 = TermC.parseNEW' ctxt "d_d x (a*BC*y*z)";
|
Walther@60500
|
87 |
Rewrite.rewrite_inst_ ctxt ro er true inst diff_const t2;
|
wneuper@59472
|
88 |
\<close>
|
wneuper@59472
|
89 |
text \<open>For term t1 the assumption 'not (x occurs_in "a*BC*x*z")' is false,
|
neuper@38077
|
90 |
since x occurs in t1 actually; thus the rule following implication '==>' is
|
neuper@38077
|
91 |
not applied and rewrite_inst_ returns NONE.
|
neuper@38077
|
92 |
For term t2 is 'not (x occurs_in "a*BC*y*z")' true, thus the rule is applied.
|
wneuper@59472
|
93 |
\<close>
|
neuper@38067
|
94 |
|
wneuper@59472
|
95 |
subsection \<open>ordered rewriting\<close>
|
wneuper@59472
|
96 |
text \<open>Let us start with an example; in order to see what is going on we tell
|
neuper@38077
|
97 |
Isabelle to show all brackets:
|
wneuper@59472
|
98 |
\<close>
|
wneuper@59472
|
99 |
ML \<open>
|
neuper@42090
|
100 |
(*show_brackets := true; TODO*)
|
Walther@60424
|
101 |
val t0 = TermC.parseNEW' ctxt "2*a + 3*b + 4*a::real"; UnparseC.term t0;
|
neuper@38077
|
102 |
(*show_brackets := false;*)
|
wneuper@59472
|
103 |
\<close>
|
wneuper@59472
|
104 |
text \<open>Now we want to bring 4*a close to 2*a in order to get 6*a:
|
wneuper@59472
|
105 |
\<close>
|
wneuper@59472
|
106 |
ML \<open>
|
Walther@60500
|
107 |
val SOME (t, _) = Rewrite.rewrite_ ctxt ro er true @{thm add.assoc} t0; UnparseC.term t;
|
Walther@60500
|
108 |
val SOME (t, _) = Rewrite.rewrite_ ctxt ro er true @{thm add.left_commute} t; UnparseC.term t;
|
Walther@60500
|
109 |
val SOME (t, _) = Rewrite.rewrite_ ctxt ro er true @{thm add.commute} t; UnparseC.term t;
|
Walther@60500
|
110 |
val SOME (t, _) = Rewrite.rewrite_ ctxt ro er true @{thm real_num_collect} t; UnparseC.term t;
|
wneuper@59472
|
111 |
\<close>
|
wneuper@59472
|
112 |
text \<open>That is fine, we just need to add 2+4 !!!!! See the next section below.
|
neuper@38077
|
113 |
|
neuper@38077
|
114 |
But we cannot automate such ordering with what we know so far: If we put
|
wneuper@59118
|
115 |
add.assoc, add.left_commute and add.commute into one ruleset (your have used
|
neuper@38077
|
116 |
ruleset 'make_polynomial' already), then all the rules are applied as long
|
neuper@38077
|
117 |
as one rule is applicable (that is the way such rulesets work).
|
neuper@38077
|
118 |
Try to step through the ML-sections without skipping one of them ...
|
wneuper@59472
|
119 |
\<close>
|
Walther@60500
|
120 |
ML \<open>val SOME (t, _) = Rewrite.rewrite_ ctxt ro er true @{thm add.commute} t; UnparseC.term t\<close>
|
Walther@60500
|
121 |
ML \<open>val SOME (t, _) = Rewrite.rewrite_ ctxt ro er true @{thm add.commute} t; UnparseC.term t\<close>
|
Walther@60500
|
122 |
ML \<open>val SOME (t, _) = Rewrite.rewrite_ ctxt ro er true @{thm add.commute} t; UnparseC.term t\<close>
|
Walther@60500
|
123 |
ML \<open>val SOME (t, _) = Rewrite.rewrite_ ctxt ro er true @{thm add.commute} t; UnparseC.term t\<close>
|
wneuper@59472
|
124 |
text \<open>... you can go forever, the ruleset is 'not terminating'.
|
neuper@38077
|
125 |
The theory of rewriting makes this kind of rulesets terminate by the use of
|
neuper@38077
|
126 |
'rewrite orders':
|
neuper@38077
|
127 |
Given two terms t1 and t2 we describe rewriting by: t1 ~~> t2. Then
|
neuper@38077
|
128 |
'ordered rewriting' is: t2 < t1 ==> t1 ~~> t2. That means, a rule is only
|
neuper@38077
|
129 |
applied, when the result t2 is 'smaller', '<', than the one to be rewritten.
|
neuper@38077
|
130 |
Defining such a '<' is not trivial, see ~~/src/Tools/isacKnowledge/Poly.thy
|
neuper@38077
|
131 |
for 'fun has_degree_in' etc.
|
wneuper@59472
|
132 |
\<close>
|
neuper@38067
|
133 |
|
wneuper@59472
|
134 |
subsection \<open>Simplification in ISAC\<close>
|
wneuper@59472
|
135 |
text \<open>
|
neuper@38077
|
136 |
With the introduction into rewriting, ordered rewriting and conditional
|
neuper@38077
|
137 |
rewriting we have seen all what is necessary for the practice of rewriting.
|
neuper@38077
|
138 |
|
neuper@38077
|
139 |
One basic technique of 'symbolic computation' which uses rewriting is
|
neuper@38077
|
140 |
simplification, that means: transform terms into an equivalent form which is
|
neuper@38077
|
141 |
as simple as possible.
|
neuper@38077
|
142 |
Isabelle has powerful and efficient simplifiers. Nevertheless, ISAC has another
|
neuper@38077
|
143 |
kind of simplifiers, which groups rulesets such that the trace of rewrites is
|
neuper@38077
|
144 |
more readable in ISAC's worksheets.
|
neuper@38077
|
145 |
|
neuper@38077
|
146 |
Here are examples of of how ISAC's simplifier work:
|
wneuper@59472
|
147 |
\<close>
|
wneuper@59472
|
148 |
ML \<open>
|
neuper@42090
|
149 |
(*show_brackets := false; TODO*)
|
Walther@60424
|
150 |
val t1 = TermC.parseNEW' ctxt "(a - b) * (a\<up>2 + a*b + b\<up>2)";
|
Walther@60500
|
151 |
val SOME (t, _) = Rewrite.rewrite_set_ ctxt true make_polynomial t1; UnparseC.term t;
|
wneuper@59472
|
152 |
\<close>
|
wneuper@59472
|
153 |
ML \<open>
|
Walther@60424
|
154 |
val t2 = TermC.parseNEW' ctxt
|
walther@60242
|
155 |
"(2 / (x + 3) + 2 / (x - 3)) / (8 * x / (x \<up> 2 - 9))";
|
Walther@60500
|
156 |
val SOME (t, _) = Rewrite.rewrite_set_ ctxt true norm_Rational t2; UnparseC.term t;
|
wneuper@59472
|
157 |
\<close>
|
wneuper@59472
|
158 |
text \<open>The simplifiers are quite busy when finding the above results. you can
|
walther@59901
|
159 |
watch them at work by setting the switch 'Rewrite.trace_on:\<close>
|
wneuper@59472
|
160 |
ML \<open>
|
neuper@38077
|
161 |
tracing "+++begin++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++";
|
Walther@60500
|
162 |
val SOME (t, _) = Rewrite.rewrite_set_ ctxt true norm_Rational t2; UnparseC.term t;
|
neuper@38077
|
163 |
tracing "+++end++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++";
|
wneuper@59472
|
164 |
\<close>
|
wneuper@59472
|
165 |
text \<open>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.
|
wneuper@59472
|
169 |
\<close>
|
neuper@38067
|
170 |
|
neuper@38077
|
171 |
|
wneuper@59472
|
172 |
section \<open>Experiments with a simplifier conserving minus\<close>
|
neuper@38077
|
173 |
|
wneuper@59472
|
174 |
text \<open>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
|
wenzelm@60192
|
183 |
$ISABELLE_ISAC/Knowledge/PolyMinus.thy
|
wneuper@59472
|
184 |
\<close>
|
neuper@38067
|
185 |
|
wneuper@59472
|
186 |
subsection \<open>What already works\<close>
|
wneuper@59472
|
187 |
ML \<open>
|
Walther@60424
|
188 |
val t2 = TermC.parseNEW' ctxt
|
Walther@60424
|
189 |
"5*e + 6*f - 8*g - 9 - 7*e - 4*f + 10*g + 12::real";
|
Walther@60500
|
190 |
val SOME (t, _) = Rewrite.rewrite_set_ ctxt true rls_p_33 t2; UnparseC.term t;
|
wneuper@59472
|
191 |
\<close>
|
wneuper@59472
|
192 |
text \<open>Try your own examples !\<close>
|
neuper@38067
|
193 |
|
wneuper@59472
|
194 |
subsection \<open>This raises questions about didactics\<close>
|
wneuper@59472
|
195 |
text \<open>Oberserve the '-' ! That works out. But see the efforts in PolyMinus.thy
|
wneuper@59472
|
196 |
\<close>
|
wneuper@59472
|
197 |
ML \<open>
|
neuper@38077
|
198 |
@{thm subtrahiere};
|
neuper@38077
|
199 |
@{thm subtrahiere_von_1};
|
neuper@38077
|
200 |
@{thm subtrahiere_1};
|
wneuper@59472
|
201 |
\<close>
|
wneuper@59472
|
202 |
text \<open>That would not be so bad. But it is only a little part of what else is
|
neuper@38077
|
203 |
required:
|
wneuper@59472
|
204 |
\<close>
|
wneuper@59472
|
205 |
ML \<open>
|
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};
|
wneuper@59472
|
215 |
\<close>
|
wneuper@59472
|
216 |
text \<open>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 '-' ?
|
wneuper@59472
|
224 |
\<close>
|
neuper@38077
|
225 |
|
wneuper@59472
|
226 |
subsection \<open>This does not yet work\<close>
|
wneuper@59472
|
227 |
ML \<open>
|
Walther@60424
|
228 |
val t = TermC.parseNEW' ctxt
|
neuper@38077
|
229 |
"(2*a - 5*b) * (2*a + 5*b)";
|
Walther@60500
|
230 |
Rewrite.rewrite_set_ ctxt true rls_p_33 t; UnparseC.term t;
|
wneuper@59472
|
231 |
\<close>
|
neuper@38067
|
232 |
|
neuper@38067
|
233 |
end
|