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
|
neuper@38077
|
22 |
found in ~~/src/Tools/isac/Knowledge/Diff.thy:
|
wneuper@59472
|
23 |
\<close>
|
wneuper@59472
|
24 |
ML \<open>
|
walther@59871
|
25 |
val diff_sum = ThmC.numerals_to_Free @{thm diff_sum};
|
walther@59871
|
26 |
val diff_pow = ThmC.numerals_to_Free @{thm diff_pow};
|
walther@59871
|
27 |
val diff_var = ThmC.numerals_to_Free @{thm diff_var};
|
walther@59871
|
28 |
val diff_const = ThmC.numerals_to_Free @{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"})]);
|
wneuper@59472
|
40 |
\<close>
|
wneuper@59472
|
41 |
text \<open>... and let us differentiate the term t:\<close>
|
wneuper@59472
|
42 |
ML \<open>
|
wneuper@59395
|
43 |
val t = (Thm.term_of o the o (TermC.parse thy)) "d_d x (x^^^2 + x + y)";
|
neuper@38067
|
44 |
|
walther@59868
|
45 |
val SOME (t, _) = Rewrite.rewrite_inst_ thy ro er true inst diff_sum t; UnparseC.term t;
|
walther@59868
|
46 |
val SOME (t, _) = Rewrite.rewrite_inst_ thy ro er true inst diff_sum t; UnparseC.term t;
|
walther@59868
|
47 |
val SOME (t, _) = Rewrite.rewrite_inst_ thy ro er true inst diff_pow t; UnparseC.term t;
|
walther@59868
|
48 |
val SOME (t, _) = Rewrite.rewrite_inst_ thy ro er true inst diff_var t; UnparseC.term t;
|
walther@59868
|
49 |
val SOME (t, _) = Rewrite.rewrite_inst_ thy ro er true inst diff_const t; UnparseC.term t;
|
wneuper@59472
|
50 |
\<close>
|
wneuper@59472
|
51 |
text \<open>Please, scoll up the Output-window to check the 5 steps of rewriting !
|
neuper@38077
|
52 |
You might not be satisfied by the result "2 * x ^^^ (2 - 1) + 1 + 0".
|
neuper@38067
|
53 |
|
neuper@38077
|
54 |
ISAC has a set of rules called 'make_polynomial', which simplifies the result:
|
wneuper@59472
|
55 |
\<close>
|
wneuper@59472
|
56 |
ML \<open>
|
walther@59868
|
57 |
val SOME (t, _) = Rewrite.rewrite_set_ thy true make_polynomial t; UnparseC.term t;
|
walther@59901
|
58 |
Rewrite.trace_on := false;
|
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@59868
|
71 |
val t = @{term "%x. x^2 + x + y"}; TermC.atomwy t; UnparseC.term t;
|
wneuper@59472
|
72 |
\<close>
|
wneuper@59472
|
73 |
text \<open>Since this notation does not conform to present high-school matheatics
|
neuper@38077
|
74 |
ISAC introduced the 'bdv' mechanism. This mechanism is also used for equation
|
neuper@38077
|
75 |
solving in ISAC.
|
wneuper@59472
|
76 |
\<close>
|
neuper@38067
|
77 |
|
wneuper@59472
|
78 |
section \<open>Conditional and ordered rewriting\<close>
|
wneuper@59472
|
79 |
text \<open>We have already seen conditional rewriting above when we used the rule
|
wneuper@59472
|
80 |
diff_const; let us try:\<close>
|
wneuper@59472
|
81 |
ML \<open>
|
wneuper@59395
|
82 |
val t1 = (Thm.term_of o the o (TermC.parse thy)) "d_d x (a*BC*x*z)";
|
wneuper@59382
|
83 |
Rewrite.rewrite_inst_ thy ro er true inst diff_const t1;
|
neuper@38077
|
84 |
|
wneuper@59395
|
85 |
val t2 = (Thm.term_of o the o (TermC.parse thy)) "d_d x (a*BC*y*z)";
|
wneuper@59382
|
86 |
Rewrite.rewrite_inst_ thy ro er true inst diff_const t2;
|
wneuper@59472
|
87 |
\<close>
|
wneuper@59472
|
88 |
text \<open>For term t1 the assumption 'not (x occurs_in "a*BC*x*z")' is false,
|
neuper@38077
|
89 |
since x occurs in t1 actually; thus the rule following implication '==>' is
|
neuper@38077
|
90 |
not applied and rewrite_inst_ returns NONE.
|
neuper@38077
|
91 |
For term t2 is 'not (x occurs_in "a*BC*y*z")' true, thus the rule is applied.
|
wneuper@59472
|
92 |
\<close>
|
neuper@38067
|
93 |
|
wneuper@59472
|
94 |
subsection \<open>ordered rewriting\<close>
|
wneuper@59472
|
95 |
text \<open>Let us start with an example; in order to see what is going on we tell
|
neuper@38077
|
96 |
Isabelle to show all brackets:
|
wneuper@59472
|
97 |
\<close>
|
wneuper@59472
|
98 |
ML \<open>
|
neuper@42090
|
99 |
(*show_brackets := true; TODO*)
|
walther@59868
|
100 |
val t0 = (Thm.term_of o the o (TermC.parse thy)) "2*a + 3*b + 4*a"; UnparseC.term t0;
|
neuper@38077
|
101 |
(*show_brackets := false;*)
|
wneuper@59472
|
102 |
\<close>
|
wneuper@59472
|
103 |
text \<open>Now we want to bring 4*a close to 2*a in order to get 6*a:
|
wneuper@59472
|
104 |
\<close>
|
wneuper@59472
|
105 |
ML \<open>
|
walther@59868
|
106 |
val SOME (t, _) = Rewrite.rewrite_ thy ro er true @{thm add.assoc} t0; UnparseC.term t;
|
walther@59868
|
107 |
val SOME (t, _) = Rewrite.rewrite_ thy ro er true @{thm add.left_commute} t; UnparseC.term t;
|
walther@59868
|
108 |
val SOME (t, _) = Rewrite.rewrite_ thy ro er true @{thm add.commute} t; UnparseC.term t;
|
walther@59868
|
109 |
val SOME (t, _) = Rewrite.rewrite_ thy ro er true @{thm real_num_collect} t; UnparseC.term t;
|
wneuper@59472
|
110 |
\<close>
|
wneuper@59472
|
111 |
text \<open>That is fine, we just need to add 2+4 !!!!! See the next section below.
|
neuper@38077
|
112 |
|
neuper@38077
|
113 |
But we cannot automate such ordering with what we know so far: If we put
|
wneuper@59118
|
114 |
add.assoc, add.left_commute and add.commute into one ruleset (your have used
|
neuper@38077
|
115 |
ruleset 'make_polynomial' already), then all the rules are applied as long
|
neuper@38077
|
116 |
as one rule is applicable (that is the way such rulesets work).
|
neuper@38077
|
117 |
Try to step through the ML-sections without skipping one of them ...
|
wneuper@59472
|
118 |
\<close>
|
walther@59868
|
119 |
ML \<open>val SOME (t, _) = Rewrite.rewrite_ thy ro er true @{thm add.commute} t; UnparseC.term t\<close>
|
walther@59868
|
120 |
ML \<open>val SOME (t, _) = Rewrite.rewrite_ thy ro er true @{thm add.commute} t; UnparseC.term t\<close>
|
walther@59868
|
121 |
ML \<open>val SOME (t, _) = Rewrite.rewrite_ thy ro er true @{thm add.commute} t; UnparseC.term t\<close>
|
walther@59868
|
122 |
ML \<open>val SOME (t, _) = Rewrite.rewrite_ thy ro er true @{thm add.commute} t; UnparseC.term t\<close>
|
wneuper@59472
|
123 |
text \<open>... you can go forever, the ruleset is 'not terminating'.
|
neuper@38077
|
124 |
The theory of rewriting makes this kind of rulesets terminate by the use of
|
neuper@38077
|
125 |
'rewrite orders':
|
neuper@38077
|
126 |
Given two terms t1 and t2 we describe rewriting by: t1 ~~> t2. Then
|
neuper@38077
|
127 |
'ordered rewriting' is: t2 < t1 ==> t1 ~~> t2. That means, a rule is only
|
neuper@38077
|
128 |
applied, when the result t2 is 'smaller', '<', than the one to be rewritten.
|
neuper@38077
|
129 |
Defining such a '<' is not trivial, see ~~/src/Tools/isacKnowledge/Poly.thy
|
neuper@38077
|
130 |
for 'fun has_degree_in' etc.
|
wneuper@59472
|
131 |
\<close>
|
neuper@38067
|
132 |
|
wneuper@59472
|
133 |
subsection \<open>Simplification in ISAC\<close>
|
wneuper@59472
|
134 |
text \<open>
|
neuper@38077
|
135 |
With the introduction into rewriting, ordered rewriting and conditional
|
neuper@38077
|
136 |
rewriting we have seen all what is necessary for the practice of rewriting.
|
neuper@38077
|
137 |
|
neuper@38077
|
138 |
One basic technique of 'symbolic computation' which uses rewriting is
|
neuper@38077
|
139 |
simplification, that means: transform terms into an equivalent form which is
|
neuper@38077
|
140 |
as simple as possible.
|
neuper@38077
|
141 |
Isabelle has powerful and efficient simplifiers. Nevertheless, ISAC has another
|
neuper@38077
|
142 |
kind of simplifiers, which groups rulesets such that the trace of rewrites is
|
neuper@38077
|
143 |
more readable in ISAC's worksheets.
|
neuper@38077
|
144 |
|
neuper@38077
|
145 |
Here are examples of of how ISAC's simplifier work:
|
wneuper@59472
|
146 |
\<close>
|
wneuper@59472
|
147 |
ML \<open>
|
neuper@42090
|
148 |
(*show_brackets := false; TODO*)
|
wneuper@59395
|
149 |
val t1 = (Thm.term_of o the o (TermC.parse thy)) "(a - b) * (a^^^2 + a*b + b^^^2)";
|
walther@59868
|
150 |
val SOME (t, _) = Rewrite.rewrite_set_ thy true make_polynomial t1; UnparseC.term t;
|
wneuper@59472
|
151 |
\<close>
|
wneuper@59472
|
152 |
ML \<open>
|
wneuper@59395
|
153 |
val t2 = (Thm.term_of o the o (TermC.parse thy))
|
neuper@38077
|
154 |
"(2 / (x + 3) + 2 / (x - 3)) / (8 * x / (x ^^^ 2 - 9))";
|
walther@59868
|
155 |
val SOME (t, _) = Rewrite.rewrite_set_ thy true norm_Rational t2; UnparseC.term t;
|
wneuper@59472
|
156 |
\<close>
|
wneuper@59472
|
157 |
text \<open>The simplifiers are quite busy when finding the above results. you can
|
walther@59901
|
158 |
watch them at work by setting the switch 'Rewrite.trace_on:\<close>
|
wneuper@59472
|
159 |
ML \<open>
|
walther@59901
|
160 |
Celem.Rewrite.trace_on := false;
|
neuper@38077
|
161 |
tracing "+++begin++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++";
|
walther@59868
|
162 |
val SOME (t, _) = Rewrite.rewrite_set_ thy true norm_Rational t2; UnparseC.term t;
|
neuper@38077
|
163 |
tracing "+++end++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++";
|
walther@59901
|
164 |
Celem.Rewrite.trace_on := false;
|
wneuper@59472
|
165 |
\<close>
|
wneuper@59472
|
166 |
text \<open>You see what happend when you click the checkbox <Tracing> on the bar
|
neuper@38077
|
167 |
separating this window from the Output-window.
|
neuper@38077
|
168 |
|
neuper@38077
|
169 |
So, it might be better to take simpler examples for watching the simplifiers.
|
wneuper@59472
|
170 |
\<close>
|
neuper@38067
|
171 |
|
neuper@38077
|
172 |
|
wneuper@59472
|
173 |
section \<open>Experiments with a simplifier conserving minus\<close>
|
neuper@38077
|
174 |
|
wneuper@59472
|
175 |
text \<open>We conclude the section on rewriting with starting into an experimental
|
neuper@38077
|
176 |
development. This development has been urged by teachers using ISAC for
|
neuper@38077
|
177 |
introduction to algebra with students at the age of 12-14.
|
neuper@38077
|
178 |
|
neuper@38077
|
179 |
The teachers requested ISAC to keep the minus, for instance in the above
|
neuper@38077
|
180 |
result "a^3 + -1 * b^3" (here ISAC should write "a^3 - * b^3") and also
|
neuper@38077
|
181 |
in all intermediate steps.
|
neuper@38077
|
182 |
|
neuper@38077
|
183 |
So we started to develop (in German !) such a simplifier in
|
neuper@38077
|
184 |
~~/src/Tools/isac/Knowledge/PolyMinus.thy
|
wneuper@59472
|
185 |
\<close>
|
neuper@38067
|
186 |
|
wneuper@59472
|
187 |
subsection \<open>What already works\<close>
|
wneuper@59472
|
188 |
ML \<open>
|
wneuper@59395
|
189 |
val t2 = (Thm.term_of o the o (TermC.parse thy))
|
neuper@38080
|
190 |
"5*e + 6*f - 8*g - 9 - 7*e - 4*f + 10*g + 12";
|
walther@59868
|
191 |
val SOME (t, _) = Rewrite.rewrite_set_ thy true rls_p_33 t2; UnparseC.term t;
|
wneuper@59472
|
192 |
\<close>
|
wneuper@59472
|
193 |
text \<open>Try your own examples !\<close>
|
neuper@38067
|
194 |
|
wneuper@59472
|
195 |
subsection \<open>This raises questions about didactics\<close>
|
wneuper@59472
|
196 |
text \<open>Oberserve the '-' ! That works out. But see the efforts in PolyMinus.thy
|
wneuper@59472
|
197 |
\<close>
|
wneuper@59472
|
198 |
ML \<open>
|
neuper@38077
|
199 |
@{thm subtrahiere};
|
neuper@38077
|
200 |
@{thm subtrahiere_von_1};
|
neuper@38077
|
201 |
@{thm subtrahiere_1};
|
wneuper@59472
|
202 |
\<close>
|
wneuper@59472
|
203 |
text \<open>That would not be so bad. But it is only a little part of what else is
|
neuper@38077
|
204 |
required:
|
wneuper@59472
|
205 |
\<close>
|
wneuper@59472
|
206 |
ML \<open>
|
neuper@38077
|
207 |
@{thm subtrahiere_x_plus_minus};
|
neuper@38077
|
208 |
@{thm subtrahiere_x_plus1_minus};
|
neuper@38077
|
209 |
@{thm subtrahiere_x_plus_minus1};
|
neuper@38077
|
210 |
@{thm subtrahiere_x_minus_plus};
|
neuper@38077
|
211 |
@{thm subtrahiere_x_minus1_plus};
|
neuper@38077
|
212 |
@{thm subtrahiere_x_minus_plus1};
|
neuper@38077
|
213 |
@{thm subtrahiere_x_minus_minus};
|
neuper@38077
|
214 |
@{thm subtrahiere_x_minus1_minus};
|
neuper@38077
|
215 |
@{thm subtrahiere_x_minus_minus1};
|
wneuper@59472
|
216 |
\<close>
|
wneuper@59472
|
217 |
text \<open>So, learning so many rules, and learning to apply these rules, is futile.
|
neuper@38077
|
218 |
Actually, most of our students are unable to apply theorems.
|
neuper@38077
|
219 |
|
neuper@38077
|
220 |
But if you look at 'make_polynomial' or even 'norm_Rational' you see,
|
neuper@38077
|
221 |
that these general simplifiers require about 10% than rulesets for '-'.
|
neuper@38077
|
222 |
|
neuper@38077
|
223 |
So, we might have better chances to teach our student to apply theorems
|
neuper@38077
|
224 |
without '-' ?
|
wneuper@59472
|
225 |
\<close>
|
neuper@38077
|
226 |
|
wneuper@59472
|
227 |
subsection \<open>This does not yet work\<close>
|
wneuper@59472
|
228 |
ML \<open>
|
wneuper@59395
|
229 |
val t = (Thm.term_of o the o (TermC.parse thy))
|
neuper@38077
|
230 |
"(2*a - 5*b) * (2*a + 5*b)";
|
walther@59868
|
231 |
Rewrite.rewrite_set_ thy true rls_p_33 t; UnparseC.term t;
|
wneuper@59472
|
232 |
\<close>
|
neuper@38067
|
233 |
|
neuper@38067
|
234 |
end
|