neuper@37906
|
1 |
(* testexamples for Poly, polynomials
|
neuper@37906
|
2 |
author: Matthias Goldgruber 2003
|
neuper@37906
|
3 |
(c) due to copyright terms
|
neuper@37906
|
4 |
|
neuper@37906
|
5 |
use"../smltest/IsacKnowledge/poly.sml";
|
neuper@37906
|
6 |
use"poly.sml";
|
neuper@37906
|
7 |
****************************************************************.*)
|
neuper@37906
|
8 |
|
neuper@37906
|
9 |
(******************************************************************
|
neuper@37906
|
10 |
WN060104 'SPB' came into 'exp_IsacCore_Simp_Poly_Book.xml'
|
neuper@37906
|
11 |
'SPO' came into 'exp_IsacCore_Simp_Poly_Other.xml'
|
neuper@37906
|
12 |
*******************************************************************)
|
neuper@37906
|
13 |
"-----------------------------------------------------------------";
|
neuper@37906
|
14 |
"table of contents -----------------------------------------------";
|
neuper@37906
|
15 |
"-----------------------------------------------------------------";
|
neuper@37906
|
16 |
"-------- investigate new uniary minus ---------------------------";
|
neuper@37906
|
17 |
"-------- Bsple aus Schalk I -------------------------------------";
|
neuper@37906
|
18 |
"-------- Script 'simplification for_polynomials' ----------------";
|
neuper@37906
|
19 |
"-------- check pbl 'polynomial simplification' -----------------";
|
neuper@37906
|
20 |
"-------- me 'polynomial simplification' Schalk I p.63 No.267b ---";
|
neuper@37906
|
21 |
"-------- norm_Poly NOT COMPLETE ---------------------------------";
|
neuper@37906
|
22 |
"-------- ord_make_polynomial ------------------------------------";
|
neuper@37906
|
23 |
"-----------------------------------------------------------------";
|
neuper@37906
|
24 |
"-----------------------------------------------------------------";
|
neuper@37906
|
25 |
"-----------------------------------------------------------------";
|
neuper@37906
|
26 |
|
neuper@37906
|
27 |
|
neuper@37906
|
28 |
"-------- investigate new uniary minus ---------------------------";
|
neuper@37906
|
29 |
"-------- investigate new uniary minus ---------------------------";
|
neuper@37906
|
30 |
"-------- investigate new uniary minus ---------------------------";
|
neuper@37906
|
31 |
val t = (#prop o rep_thm) real_diff_0; (*"0 - ?x = - ?x"*)
|
neuper@37906
|
32 |
atomty t;
|
neuper@37906
|
33 |
(*** -------------
|
neuper@37906
|
34 |
*** Const ( Trueprop, bool => prop)
|
neuper@37906
|
35 |
*** . Const ( op =, [real, real] => bool)
|
neuper@37906
|
36 |
*** . . Const ( op -, [real, real] => real)
|
neuper@37906
|
37 |
*** . . . Const ( 0, real)
|
neuper@37906
|
38 |
*** . . . Var ((x, 0), real)
|
neuper@37906
|
39 |
*** . . Const ( uminus, real => real)
|
neuper@37906
|
40 |
*** . . . Var ((x, 0), real) *)
|
neuper@37906
|
41 |
|
neuper@37906
|
42 |
val t = (term_of o the o (parse thy)) "-1";
|
neuper@37906
|
43 |
atomty t;
|
neuper@37906
|
44 |
(*** -------------
|
neuper@37906
|
45 |
*** Free ( -1, real) *)
|
neuper@37906
|
46 |
val t = (term_of o the o (parse thy)) "- 1";
|
neuper@37906
|
47 |
atomty t;
|
neuper@37906
|
48 |
(*** -------------
|
neuper@37906
|
49 |
*** Const ( uminus, real => real)
|
neuper@37906
|
50 |
*** . Free ( 1, real) *)
|
neuper@37906
|
51 |
|
neuper@37906
|
52 |
val t = (term_of o the o (parse thy)) "-x"; (*1-x syntyx error !!!*)
|
neuper@37906
|
53 |
atomty t;
|
neuper@37906
|
54 |
(**** -------------
|
neuper@37906
|
55 |
*** Free ( -x, real)*)
|
neuper@37906
|
56 |
val t = (term_of o the o (parse thy)) "- x";
|
neuper@37906
|
57 |
atomty t;
|
neuper@37906
|
58 |
(**** -------------
|
neuper@37906
|
59 |
*** Free ( -x, real) !!!!!!!!!!!!!!!!!!!!!!!! is the same !!!*)
|
neuper@37906
|
60 |
val t = (term_of o the o (parse thy)) "-(x)";
|
neuper@37906
|
61 |
atomty t;
|
neuper@37906
|
62 |
(**** -------------
|
neuper@37906
|
63 |
*** Free ( -x, real)*)
|
neuper@37906
|
64 |
|
neuper@37906
|
65 |
|
neuper@37906
|
66 |
"-------- Bsple aus Schalk I -------------------------------------";
|
neuper@37906
|
67 |
"-------- Bsple aus Schalk I -------------------------------------";
|
neuper@37906
|
68 |
"-------- Bsple aus Schalk I -------------------------------------";
|
neuper@37906
|
69 |
(*SPB Schalk I p.63 No.267b*)
|
neuper@37906
|
70 |
val t = str2term
|
neuper@37906
|
71 |
"(5*x^^^2 + 3) * (2*x^^^7 + 3) - (3*x^^^5 + 8) * (6*x^^^4 - 1)";
|
neuper@37906
|
72 |
val Some (t,_) = rewrite_set_ thy false make_polynomial t; term2str t;
|
neuper@37906
|
73 |
if (term2str t) =
|
neuper@37906
|
74 |
"17 + 15 * x ^^^ 2 + -48 * x ^^^ 4 + 3 * x ^^^ 5 + 6 * x ^^^ 7 + -8 * x ^^^ 9"
|
neuper@37906
|
75 |
then ()
|
neuper@37906
|
76 |
else raise error "poly.sml: diff.behav. in make_polynomial 1";
|
neuper@37906
|
77 |
|
neuper@37906
|
78 |
(*SPB Schalk I p.63 No.275b*)
|
neuper@37906
|
79 |
val t = str2term
|
neuper@37906
|
80 |
"(3*x^^^2 - 2*x*y + y^^^2) * (x^^^2 - 2*y^^^2)";
|
neuper@37906
|
81 |
val Some (t,_) = rewrite_set_ thy false make_polynomial t;
|
neuper@37906
|
82 |
term2str t;
|
neuper@37906
|
83 |
if (term2str t) =
|
neuper@37906
|
84 |
"3 * x ^^^ 4 + -2 * x ^^^ 3 * y + -5 * x ^^^ 2 * y ^^^ 2 + \
|
neuper@37906
|
85 |
\4 * x * y ^^^ 3 +\n-2 * y ^^^ 4"
|
neuper@37906
|
86 |
then ()
|
neuper@37906
|
87 |
else raise error "poly.sml: diff.behav. in make_polynomial 2";
|
neuper@37906
|
88 |
|
neuper@37906
|
89 |
(*SPB Schalk I p.63 No.279b*)
|
neuper@37906
|
90 |
val t = str2term
|
neuper@37906
|
91 |
"(x-a)*(x-b)*(x-c)*(x-d)";
|
neuper@37906
|
92 |
val Some (t,_) = rewrite_set_ thy false make_polynomial t;
|
neuper@37906
|
93 |
term2str t;
|
neuper@37906
|
94 |
(* Richtig! *)
|
neuper@37906
|
95 |
if (term2str t) =
|
neuper@37906
|
96 |
"a * b * c * d + -1 * a * b * c * x + -1 * a * b * d * x + a * b * x ^^^ 2 +\n-1 * a * c * d * x +\na * c * x ^^^ 2 +\na * d * x ^^^ 2 +\n-1 * a * x ^^^ 3 +\n-1 * b * c * d * x +\nb * c * x ^^^ 2 +\nb * d * x ^^^ 2 +\n-1 * b * x ^^^ 3 +\nc * d * x ^^^ 2 +\n-1 * c * x ^^^ 3 +\n-1 * d * x ^^^ 3 +\nx ^^^ 4"
|
neuper@37906
|
97 |
then ()
|
neuper@37906
|
98 |
else raise error "poly.sml: diff.behav. in make_polynomial 3";
|
neuper@37906
|
99 |
|
neuper@37906
|
100 |
(*SPB Schalk I p.63 No.291*)
|
neuper@37906
|
101 |
val t = str2term
|
neuper@37906
|
102 |
"(5+96*x^^^3+8*x*(-4+(7- 3*x)*4*x))*(5*(2- 3*x)- (-15*x*(-8*x- 5)))";
|
neuper@37906
|
103 |
val Some (t,_) = rewrite_set_ thy false make_polynomial t;
|
neuper@37906
|
104 |
term2str t;
|
neuper@37906
|
105 |
if (term2str t) =
|
neuper@37906
|
106 |
"50 + -770 * x + 4520 * x ^^^ 2 + -16320 * x ^^^ 3 + -26880 * x ^^^ 4"
|
neuper@37906
|
107 |
then ()
|
neuper@37906
|
108 |
else raise error "poly.sml: diff.behav. in make_polynomial 4";
|
neuper@37906
|
109 |
|
neuper@37906
|
110 |
(*SPB Schalk I p.64 No.295c*)
|
neuper@37906
|
111 |
val t = str2term
|
neuper@37906
|
112 |
"(13*a^^^4*b^^^9*c - 12*a^^^3*b^^^6*c^^^9)^^^2";
|
neuper@37906
|
113 |
val Some (t,_) = rewrite_set_ thy false make_polynomial t;
|
neuper@37906
|
114 |
term2str t;
|
neuper@37906
|
115 |
if (term2str t) =
|
neuper@37906
|
116 |
"169 * a ^^^ 8 * b ^^^ 18 * c ^^^ 2 + -312 * a ^^^ 7 * b ^^^ 15 * c ^^^ 10\
|
neuper@37906
|
117 |
\ +\n144 * a ^^^ 6 * b ^^^ 12 * c ^^^ 18"
|
neuper@37906
|
118 |
then ()
|
neuper@37906
|
119 |
else raise error "poly.sml: diff.behav. in make_polynomial 5";
|
neuper@37906
|
120 |
|
neuper@37906
|
121 |
(*SPB Schalk I p.64 No.299a*)
|
neuper@37906
|
122 |
val t = str2term
|
neuper@37906
|
123 |
"(x - y)*(x + y)";
|
neuper@37906
|
124 |
val Some (t,_) = rewrite_set_ thy false make_polynomial t;
|
neuper@37906
|
125 |
term2str t;
|
neuper@37906
|
126 |
if (term2str t) =
|
neuper@37906
|
127 |
"x ^^^ 2 + -1 * y ^^^ 2"
|
neuper@37906
|
128 |
then ()
|
neuper@37906
|
129 |
else raise error "poly.sml: diff.behav. in make_polynomial 6";
|
neuper@37906
|
130 |
|
neuper@37906
|
131 |
(*SPB Schalk I p.64 No.300c*)
|
neuper@37906
|
132 |
val t = str2term
|
neuper@37906
|
133 |
"(3*x^^^2*y - 1)*(3*x^^^2*y + 1)";
|
neuper@37906
|
134 |
val Some (t,_) = rewrite_set_ thy false make_polynomial t;
|
neuper@37906
|
135 |
term2str t;
|
neuper@37906
|
136 |
if (term2str t) =
|
neuper@37906
|
137 |
"-1 + 9 * x ^^^ 4 * y ^^^ 2"
|
neuper@37906
|
138 |
then ()
|
neuper@37906
|
139 |
else raise error "poly.sml: diff.behav. in make_polynomial 7";
|
neuper@37906
|
140 |
|
neuper@37906
|
141 |
(*SPB Schalk I p.64 No.302*)
|
neuper@37906
|
142 |
val t = str2term
|
neuper@37906
|
143 |
"(13*x^^^2 + 5)*(13*x^^^2 - 5) - (5*x^^^2 + 3)*(5*x^^^2 - 3) - (12*x^^^2 + 4)*(12*x^^^2 - 4)";
|
neuper@37906
|
144 |
val Some (t,_) = rewrite_set_ thy false make_polynomial t; term2str t;
|
neuper@37906
|
145 |
if term2str t = "0" then ()
|
neuper@37906
|
146 |
else raise error "poly.sml: diff.behav. in make_polynomial 8";
|
neuper@37906
|
147 |
(* Bei Berechnung sollte 3 mal real_plus_minus_binom1_p aus expand_poly verwendet werden *)
|
neuper@37906
|
148 |
|
neuper@37906
|
149 |
|
neuper@37906
|
150 |
(*SPB Schalk I p.64 No.306a*)
|
neuper@37906
|
151 |
val t = str2term "((x^^^2 + 1)*(x^^^2 - 1))^^^2";
|
neuper@37906
|
152 |
val Some (t,_) = rewrite_set_ thy false make_polynomial t; term2str t;
|
neuper@37906
|
153 |
if (term2str t) = "1 + 2 * x ^^^ 4 + 2 * -2 * x ^^^ 4 + x ^^^ 8" then ()
|
neuper@37906
|
154 |
else raise error "poly.sml: diff.behav. in make_polynomial: not confluent \
|
neuper@37906
|
155 |
\2 * x ^^^ 4 + 2 * -2 * x ^^^ 4 = -2 * x ^^^ 4 works again";
|
neuper@37906
|
156 |
|
neuper@37906
|
157 |
|
neuper@37906
|
158 |
(*WN071729 when reducing "rls reduce_012_" for Schaerding,
|
neuper@37906
|
159 |
the above resulted in the term below ... but reduces from then correctly*)
|
neuper@37906
|
160 |
val t = str2term "1 + 2 * x ^^^ 4 + 2 * -2 * x ^^^ 4 + x ^^^ 8";
|
neuper@37906
|
161 |
val Some (t,_) = rewrite_set_ thy false make_polynomial t; term2str t;
|
neuper@37906
|
162 |
if (term2str t) = "1 + -2 * x ^^^ 4 + x ^^^ 8" then ()
|
neuper@37906
|
163 |
else raise error "poly.sml: diff.behav. in make_polynomial 9b";
|
neuper@37906
|
164 |
|
neuper@37906
|
165 |
(*SPB Schalk I p.64 No.296a*)
|
neuper@37906
|
166 |
val t = str2term "(x - a)^^^3";
|
neuper@37906
|
167 |
val Some (t,_) = rewrite_set_ thy false make_polynomial t; term2str t;
|
neuper@37906
|
168 |
if (term2str t) = "-1 * a ^^^ 3 + 3 * a ^^^ 2 * x + -3 * a * x ^^^ 2 + x ^^^ 3"
|
neuper@37906
|
169 |
then () else raise error "poly.sml: diff.behav. in make_polynomial 10";
|
neuper@37906
|
170 |
|
neuper@37906
|
171 |
(*SPB Schalk I p.64 No.296c*)
|
neuper@37906
|
172 |
val t = str2term "(-3*x - 4*y)^^^3";
|
neuper@37906
|
173 |
val Some (t,_) = rewrite_set_ thy false make_polynomial t; term2str t;
|
neuper@37906
|
174 |
if (term2str t) =
|
neuper@37906
|
175 |
"-27 * x ^^^ 3 + -108 * x ^^^ 2 * y + -144 * x * y ^^^ 2 + -64 * y ^^^ 3"
|
neuper@37906
|
176 |
then () else raise error "poly.sml: diff.behav. in make_polynomial 11";
|
neuper@37906
|
177 |
|
neuper@37906
|
178 |
(*SPB Schalk I p.62 No.242c*)
|
neuper@37906
|
179 |
val t = str2term "x^^^(-4)*(x^^^(-4)*y^^^(-2))^^^(-1)*y^^^(-2)";
|
neuper@37906
|
180 |
val Some (t,_) = rewrite_set_ thy false make_polynomial t; term2str t;
|
neuper@37906
|
181 |
if (term2str t) = "1" then ()
|
neuper@37906
|
182 |
else raise error "poly.sml: diff.behav. in make_polynomial 12";
|
neuper@37906
|
183 |
|
neuper@37906
|
184 |
(*SPB Schalk I p.60 No.209a*)
|
neuper@37906
|
185 |
val t = str2term "a^^^(7-x) * a^^^x";
|
neuper@37906
|
186 |
val Some (t,_) = rewrite_set_ thy false make_polynomial t; term2str t;
|
neuper@37906
|
187 |
if term2str t = "a ^^^ 7" then ()
|
neuper@37906
|
188 |
else raise error "poly.sml: diff.behav. in make_polynomial 13";
|
neuper@37906
|
189 |
|
neuper@37906
|
190 |
(*SPB Schalk I p.60 No.209d*)
|
neuper@37906
|
191 |
val t = str2term "d^^^x * d^^^(x+1) * d^^^(2 - 2*x)";
|
neuper@37906
|
192 |
val Some (t,_) = rewrite_set_ thy false make_polynomial t; term2str t;
|
neuper@37906
|
193 |
if term2str t = "d ^^^ 3" then ()
|
neuper@37906
|
194 |
else raise error "poly.sml: diff.behav. in make_polynomial 14";
|
neuper@37906
|
195 |
|
neuper@37906
|
196 |
|
neuper@37906
|
197 |
(*---------------------------------------------------------------------*)
|
neuper@37906
|
198 |
(*------------------ Bsple bei denen es Probleme gibt------------------*)
|
neuper@37906
|
199 |
(*---------------------------------------------------------------------*)
|
neuper@37906
|
200 |
|
neuper@37906
|
201 |
(*Schalk I p.64 No.303*)
|
neuper@37906
|
202 |
val t = str2term "(a + 2*b)*(a^^^2 + 4*b^^^2)*(a - 2*b) - (a - 6*b)*(a^^^2 + 36*b^^^2)*(a + 6*b)";
|
neuper@37906
|
203 |
val Some (t,_) = rewrite_set_ thy false make_polynomial t; term2str t;
|
neuper@37906
|
204 |
if term2str t = "1280 * b ^^^ 4" then ()
|
neuper@37906
|
205 |
else raise error "poly.sml: diff.behav. in make_polynomial 14b";
|
neuper@37906
|
206 |
(* Richtig - aber Binomische Formel wurde nicht verwendet! *)
|
neuper@37906
|
207 |
|
neuper@37906
|
208 |
|
neuper@37906
|
209 |
(*--------------------------------------------------------------------*)
|
neuper@37906
|
210 |
(*----------------------- Eigene Beispiele ---------------------------*)
|
neuper@37906
|
211 |
(*--------------------------------------------------------------------*)
|
neuper@37906
|
212 |
(*SPO*)
|
neuper@37906
|
213 |
val t = str2term "a^^^2*a^^^(-2)";
|
neuper@37906
|
214 |
val Some (t,_) = rewrite_set_ thy false make_polynomial t; term2str t;
|
neuper@37906
|
215 |
if term2str t = "1" then ()
|
neuper@37906
|
216 |
else raise error "poly.sml: diff.behav. in make_polynomial 15";
|
neuper@37906
|
217 |
(*SPO*)
|
neuper@37906
|
218 |
val t = str2term "a + a + a";
|
neuper@37906
|
219 |
val Some (t,_) = rewrite_set_ thy false make_polynomial t; term2str t;
|
neuper@37906
|
220 |
if term2str t = "3 * a" then ()
|
neuper@37906
|
221 |
else raise error "poly.sml: diff.behav. in make_polynomial 16";
|
neuper@37906
|
222 |
(*SPO*)
|
neuper@37906
|
223 |
val t = str2term "a + b + b + b";
|
neuper@37906
|
224 |
val Some (t,_) = rewrite_set_ thy false make_polynomial t; term2str t;
|
neuper@37906
|
225 |
if term2str t = "a + 3 * b" then ()
|
neuper@37906
|
226 |
else raise error "poly.sml: diff.behav. in make_polynomial 17";
|
neuper@37906
|
227 |
(*SPO*)
|
neuper@37906
|
228 |
val t = str2term "a^^^2*b*b^^^(-1)";
|
neuper@37906
|
229 |
val Some (t,_) = rewrite_set_ thy false make_polynomial t; term2str t;
|
neuper@37906
|
230 |
if term2str t = "a ^^^ 2" then ()
|
neuper@37906
|
231 |
else raise error "poly.sml: diff.behav. in make_polynomial 18";
|
neuper@37906
|
232 |
(*SPO*)
|
neuper@37906
|
233 |
val t = str2term "a^^^2*a^^^(-2)";
|
neuper@37906
|
234 |
val Some (t,_) = rewrite_set_ thy false make_polynomial t; term2str t;
|
neuper@37906
|
235 |
if (term2str t) = "1" then ()
|
neuper@37906
|
236 |
else raise error "poly.sml: diff.behav. in make_polynomial 19";
|
neuper@37906
|
237 |
(*SPO*)
|
neuper@37906
|
238 |
val t = str2term "b + a - b";
|
neuper@37906
|
239 |
val Some (t,_) = rewrite_set_ thy false make_polynomial t; term2str t;
|
neuper@37906
|
240 |
if (term2str t) = "a" then ()
|
neuper@37906
|
241 |
else raise error "poly.sml: diff.behav. in make_polynomial 20";
|
neuper@37906
|
242 |
(*SPO*)
|
neuper@37906
|
243 |
val t = str2term "b * a * a";
|
neuper@37906
|
244 |
val Some (t,_) = rewrite_set_ thy false make_polynomial t; term2str t;
|
neuper@37906
|
245 |
if term2str t = "a ^^^ 2 * b" then ()
|
neuper@37906
|
246 |
else raise error "poly.sml: diff.behav. in make_polynomial 21";
|
neuper@37906
|
247 |
(*SPO*)
|
neuper@37906
|
248 |
val t = str2term "(a^^^2)^^^3";
|
neuper@37906
|
249 |
val Some (t,_) = rewrite_set_ thy false make_polynomial t; term2str t;
|
neuper@37906
|
250 |
if term2str t = "a ^^^ 6" then ()
|
neuper@37906
|
251 |
else raise error "poly.sml: diff.behav. in make_polynomial 22";
|
neuper@37906
|
252 |
(*SPO*)
|
neuper@37906
|
253 |
val t = str2term "x^^^2 * y^^^2 + x * x^^^2 * y";
|
neuper@37906
|
254 |
val Some (t,_) = rewrite_set_ thy false make_polynomial t; term2str t;
|
neuper@37906
|
255 |
if term2str t = "x ^^^ 3 * y + x ^^^ 2 * y ^^^ 2" then ()
|
neuper@37906
|
256 |
else raise error "poly.sml: diff.behav. in make_polynomial 23";
|
neuper@37906
|
257 |
(*SPO*)
|
neuper@37906
|
258 |
val t = (term_of o the o (parse thy)) "a^^^2 * (-a)^^^2";
|
neuper@37906
|
259 |
val Some (t,_) = rewrite_set_ thy false make_polynomial t; term2str t;
|
neuper@37906
|
260 |
if (term2str t) = "a ^^^ 4" then ()
|
neuper@37906
|
261 |
else raise error "poly.sml: diff.behav. in make_polynomial 24";
|
neuper@37906
|
262 |
(*SPO*)
|
neuper@37906
|
263 |
val t = str2term "a * b * b^^^(-1) + a";
|
neuper@37906
|
264 |
val Some (t,_) = rewrite_set_ thy false make_polynomial t; term2str t;
|
neuper@37906
|
265 |
if (term2str t) = "2 * a" then ()
|
neuper@37906
|
266 |
else raise error "poly.sml: diff.behav. in make_polynomial 25";
|
neuper@37906
|
267 |
(*SPO*)
|
neuper@37906
|
268 |
val t = str2term "a*c*b^^^(2*n) + 3*a + 5*b^^^(2*n)*c*b";
|
neuper@37906
|
269 |
val Some (t,_) = rewrite_set_ thy false make_polynomial t; term2str t;
|
neuper@37906
|
270 |
if (term2str t) = "3 * a + 5 * b ^^^ (1 + 2 * n) * c + a * b ^^^ (2 * n) * c"
|
neuper@37906
|
271 |
then () else raise error "poly.sml: diff.behav. in make_polynomial 26";
|
neuper@37906
|
272 |
|
neuper@37906
|
273 |
|
neuper@37906
|
274 |
(*MG.27.6.03 -------------vvv-: Verschachtelte Terme -----------*)
|
neuper@37906
|
275 |
(*SPO*)
|
neuper@37906
|
276 |
val t = str2term "(1 + (x*y*a) + x)^^^(1 + (x*y*a) + x)";
|
neuper@37906
|
277 |
val Some (t,_) = rewrite_set_ thy false make_polynomial t;
|
neuper@37906
|
278 |
term2str t;
|
neuper@37906
|
279 |
if term2str t = "(1 + x + a * x * y) ^^^ (1 + x + a * x * y)"
|
neuper@37906
|
280 |
then () else raise error "poly.sml: diff.behav. in make_polynomial 27";(*SPO*)
|
neuper@37906
|
281 |
val t = str2term "(1 + x*(y*z)*zz)^^^(1 + x*(y*z)*zz)";
|
neuper@37906
|
282 |
val Some (t,_) = rewrite_set_ thy false make_polynomial t;
|
neuper@37906
|
283 |
term2str t;
|
neuper@37906
|
284 |
if term2str t = "(1 + x * y * z * zz) ^^^ (1 + x * y * z * zz)"
|
neuper@37906
|
285 |
then () else raise error "poly.sml: diff.behav. in make_polynomial 28";
|
neuper@37906
|
286 |
|
neuper@37906
|
287 |
"-------- Script 'simplification for_polynomials' ----------------";
|
neuper@37906
|
288 |
"-------- Script 'simplification for_polynomials' ----------------";
|
neuper@37906
|
289 |
"-------- Script 'simplification for_polynomials' ----------------";
|
neuper@37906
|
290 |
val str =
|
neuper@37906
|
291 |
"Script SimplifyScript (t_::real) = \
|
neuper@37906
|
292 |
\ ((Rewrite_Set norm_Poly False) t_)";
|
neuper@37906
|
293 |
val sc = ((inst_abs thy) o term_of o the o (parse thy)) str;
|
neuper@37906
|
294 |
atomty sc;
|
neuper@37906
|
295 |
|
neuper@37906
|
296 |
|
neuper@37906
|
297 |
"-------- check pbl 'polynomial simplification' -----------------";
|
neuper@37906
|
298 |
"-------- check pbl 'polynomial simplification' -----------------";
|
neuper@37906
|
299 |
"-------- check pbl 'polynomial simplification' -----------------";
|
neuper@37906
|
300 |
val fmz = ["term ((5*x^^^2 + 3) * (2*x^^^7 + 3) \
|
neuper@37906
|
301 |
\- (3*x^^^5 + 8) * (6*x^^^4 - 1))",
|
neuper@37906
|
302 |
"normalform N"];
|
neuper@37906
|
303 |
(*0*)
|
neuper@37906
|
304 |
case refine fmz ["polynomial","simplification"]of
|
neuper@37906
|
305 |
[Matches (["polynomial", "simplification"], _)] => ()
|
neuper@37906
|
306 |
| _ => raise error "poly.sml diff.behav. in check pbl, refine";
|
neuper@37906
|
307 |
(*...if there is an error, then ...*)
|
neuper@37906
|
308 |
|
neuper@37906
|
309 |
(*1*)
|
neuper@37906
|
310 |
print_depth 7;
|
neuper@37906
|
311 |
val pbt = get_pbt ["polynomial","simplification"];
|
neuper@37906
|
312 |
print_depth 3;
|
neuper@37906
|
313 |
(*if there is ...
|
neuper@37906
|
314 |
> val NoMatch' {Given=gi, Where=wh, Find=fi,...} = match_pbl fmz pbt;
|
neuper@37906
|
315 |
... then trace_rewrite:*)
|
neuper@37906
|
316 |
|
neuper@37906
|
317 |
(*2*)
|
neuper@37906
|
318 |
trace_rewrite:=true;
|
neuper@37906
|
319 |
match_pbl fmz pbt;
|
neuper@37906
|
320 |
trace_rewrite:=false;
|
neuper@37906
|
321 |
(*... if there is no rewrite, then there is something wrong with prls*)
|
neuper@37906
|
322 |
|
neuper@37906
|
323 |
(*3*)
|
neuper@37906
|
324 |
print_depth 7;
|
neuper@37906
|
325 |
val prls = (#prls o get_pbt) ["polynomial","simplification"];
|
neuper@37906
|
326 |
print_depth 3;
|
neuper@37906
|
327 |
val t = str2term "((5*x^^^2 + 3) * (2*x^^^7 + 3) \
|
neuper@37906
|
328 |
\- (3*x^^^5 + 8) * (6*x^^^4 - 1)) is_polyexp";
|
neuper@37906
|
329 |
trace_rewrite:=true;
|
neuper@37906
|
330 |
val Some (t',_) = rewrite_set_ thy false prls t;
|
neuper@37906
|
331 |
trace_rewrite:=false;
|
neuper@37906
|
332 |
if t' = HOLogic.true_const then ()
|
neuper@37906
|
333 |
else raise error "poly.sml: diff.behav. in check pbl 'polynomial..";
|
neuper@37906
|
334 |
(*... if this works, but (*1*) does still NOT work, check types:*)
|
neuper@37906
|
335 |
|
neuper@37906
|
336 |
(*4*)
|
neuper@37906
|
337 |
show_types:=true;
|
neuper@37906
|
338 |
(*
|
neuper@37906
|
339 |
> val NoMatch' {Given=gi, Where=wh, Find=fi,...} = match_pbl fmz pbt;
|
neuper@37906
|
340 |
val wh = [False "(t_::real => real) (is_polyexp::real)"]
|
neuper@37906
|
341 |
......................^^^^^^^^^^^^...............^^^^*)
|
neuper@37906
|
342 |
val Matches' _ = match_pbl fmz pbt;
|
neuper@37906
|
343 |
show_types:=false;
|
neuper@37906
|
344 |
|
neuper@37906
|
345 |
|
neuper@37906
|
346 |
"-------- me 'polynomial simplification' Schalk I p.63 No.267b ---";
|
neuper@37906
|
347 |
"-------- me 'polynomial simplification' Schalk I p.63 No.267b ---";
|
neuper@37906
|
348 |
"-------- me 'polynomial simplification' Schalk I p.63 No.267b ---";
|
neuper@37906
|
349 |
val fmz = ["term ((5*x^^^2 + 3) * (2*x^^^7 + 3) \
|
neuper@37906
|
350 |
\- (3*x^^^5 + 8) * (6*x^^^4 - 1))",
|
neuper@37906
|
351 |
"normalform N"];
|
neuper@37906
|
352 |
val (dI',pI',mI') =
|
neuper@37906
|
353 |
("Poly.thy",["polynomial","simplification"],
|
neuper@37906
|
354 |
["simplification","for_polynomials"]);
|
neuper@37906
|
355 |
val p = e_pos'; val c = [];
|
neuper@37906
|
356 |
val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
|
neuper@37906
|
357 |
val (p,_,f,nxt,_,pt) = me nxt p c pt;
|
neuper@37906
|
358 |
val (p,_,f,nxt,_,pt) = me nxt p c pt;
|
neuper@37924
|
359 |
(writeln o (itms2str_ ctxt)) (get_obj g_pbl pt (fst p));
|
neuper@37906
|
360 |
val (p,_,f,nxt,_,pt) = me nxt p c pt;
|
neuper@37906
|
361 |
val (p,_,f,nxt,_,pt) = me nxt p c pt;
|
neuper@37906
|
362 |
val (p,_,f,nxt,_,pt) = me nxt p c pt;
|
neuper@37906
|
363 |
val (p,_,f,nxt,_,pt) = me nxt p c pt;
|
neuper@37906
|
364 |
val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
|
neuper@37906
|
365 |
val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
|
neuper@37906
|
366 |
val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
|
neuper@37906
|
367 |
if f2str f =
|
neuper@37906
|
368 |
"17 + 15 * x ^^^ 2 + -48 * x ^^^ 4 + 3 * x ^^^ 5 + 6 * x ^^^ 7 + -8 * x ^^^ 9"
|
neuper@37906
|
369 |
then () else raise error "poly.sml diff.behav. in me Schalk I p.63 No.267b";
|
neuper@37906
|
370 |
|
neuper@37906
|
371 |
|
neuper@37906
|
372 |
"-------- interSteps for Schalk 299a -----------------------------";
|
neuper@37906
|
373 |
"-------- interSteps for Schalk 299a -----------------------------";
|
neuper@37906
|
374 |
"-------- interSteps for Schalk 299a -----------------------------";
|
neuper@37906
|
375 |
states:=[];
|
neuper@37906
|
376 |
CalcTree
|
neuper@37906
|
377 |
[(["term ((x - y)*(x + y))", "normalform N"],
|
neuper@37906
|
378 |
("Poly.thy",["polynomial","simplification"],
|
neuper@37906
|
379 |
["simplification","for_polynomials"]))];
|
neuper@37906
|
380 |
Iterator 1;
|
neuper@37906
|
381 |
moveActiveRoot 1;
|
neuper@37906
|
382 |
autoCalculate 1 CompleteCalc;
|
neuper@37906
|
383 |
val ((pt,p),_) = get_calc 1; show_pt pt;
|
neuper@37906
|
384 |
|
neuper@37906
|
385 |
interSteps 1 ([1],Res)(*<ERROR> syserror in detailstep </ERROR>*);
|
neuper@37906
|
386 |
val ((pt,p),_) = get_calc 1; show_pt pt;
|
neuper@37906
|
387 |
if existpt' ([1,1], Frm) pt then ()
|
neuper@37906
|
388 |
else raise error "poly.sml: interSteps doesnt work again 1";
|
neuper@37906
|
389 |
|
neuper@37906
|
390 |
interSteps 1 ([1,1],Res)(*<ERROR> syserror in detailstep </ERROR>*);
|
neuper@37906
|
391 |
val ((pt,p),_) = get_calc 1; show_pt pt;
|
neuper@37906
|
392 |
if existpt' ([1,1,1], Frm) pt then ()
|
neuper@37906
|
393 |
else raise error "poly.sml: interSteps doesnt work again 2";
|
neuper@37906
|
394 |
|
neuper@37906
|
395 |
|
neuper@37906
|
396 |
"-------- norm_Poly NOT COMPLETE ---------------------------------";
|
neuper@37906
|
397 |
"-------- norm_Poly NOT COMPLETE ---------------------------------";
|
neuper@37906
|
398 |
"-------- norm_Poly NOT COMPLETE ---------------------------------";
|
neuper@37906
|
399 |
trace_rewrite:=true;
|
neuper@37906
|
400 |
val Some (f',_) = rewrite_set_ thy false norm_Poly
|
neuper@37906
|
401 |
(str2term "L = k - 2 * q + (k - 2 * q) + (k - 2 * q) + (k - 2 * q) + senkrecht + oben")(*see poly.sml: -- norm_Poly NOT COMPLETE -- TODO MG*);
|
neuper@37906
|
402 |
trace_rewrite:=false;
|
neuper@37906
|
403 |
term2str f';
|
neuper@37906
|
404 |
|
neuper@37906
|
405 |
"-------- ord_make_polynomial ------------------------------------";
|
neuper@37906
|
406 |
"-------- ord_make_polynomial ------------------------------------";
|
neuper@37906
|
407 |
"-------- ord_make_polynomial ------------------------------------";
|
neuper@37906
|
408 |
val t1 = str2term "2 * b + (3 * a + 3 * b)";
|
neuper@37906
|
409 |
val t2 = str2term "3 * a + 3 * b + 2 * b";
|
neuper@37906
|
410 |
|
neuper@37906
|
411 |
if ord_make_polynomial true Poly.thy [] (t1, t2) then ()
|
neuper@37906
|
412 |
else raise error "poly.sml: diff.behav. in ord_make_polynomial";
|
neuper@37906
|
413 |
|
neuper@37906
|
414 |
(*WN071202: ^^^ why then is there no rewriting ...*)
|
neuper@37906
|
415 |
val term = str2term "2*b + (3*a + 3*b)";
|
neuper@37906
|
416 |
val None = rewrite_set_ Isac.thy false order_add_mult term;
|
neuper@37906
|
417 |
|
neuper@37906
|
418 |
(*or why is there no rewriting this way...*)
|
neuper@37906
|
419 |
val t1 = str2term "2 * b + (3 * a + 3 * b)";
|
neuper@37906
|
420 |
val t2 = str2term "3 * a + (2 * b + 3 * b)";
|
neuper@37906
|
421 |
|
neuper@37906
|
422 |
|
neuper@37906
|
423 |
|