1 (* theory collecting all knowledge
2 (predicates 'is_rootEq_in', 'is_sqrt_in', 'is_ratEq_in')
3 for PolynomialEquations.
4 alternative dependencies see @{theory "Isac"}
10 (c) by Richard Lang, 2003
13 theory PolyEq imports LinEq RootRatEq begin
17 (*---------scripts--------------------------*)
20 bool list] => bool list"
21 ("((Script Complete'_square (_ _ =))//
26 bool list] => bool list"
27 ("((Script Normalize'_poly (_ _=))//
29 Solve'_d0'_polyeq'_equation
31 bool list] => bool list"
32 ("((Script Solve'_d0'_polyeq'_equation (_ _ =))//
34 Solve'_d1'_polyeq'_equation
36 bool list] => bool list"
37 ("((Script Solve'_d1'_polyeq'_equation (_ _ =))//
39 Solve'_d2'_polyeq'_equation
41 bool list] => bool list"
42 ("((Script Solve'_d2'_polyeq'_equation (_ _ =))//
44 Solve'_d2'_polyeq'_sqonly'_equation
46 bool list] => bool list"
47 ("((Script Solve'_d2'_polyeq'_sqonly'_equation (_ _ =))//
49 Solve'_d2'_polyeq'_bdvonly'_equation
51 bool list] => bool list"
52 ("((Script Solve'_d2'_polyeq'_bdvonly'_equation (_ _ =))//
54 Solve'_d2'_polyeq'_pq'_equation
56 bool list] => bool list"
57 ("((Script Solve'_d2'_polyeq'_pq'_equation (_ _ =))//
59 Solve'_d2'_polyeq'_abc'_equation
61 bool list] => bool list"
62 ("((Script Solve'_d2'_polyeq'_abc'_equation (_ _ =))//
64 Solve'_d3'_polyeq'_equation
66 bool list] => bool list"
67 ("((Script Solve'_d3'_polyeq'_equation (_ _ =))//
69 Solve'_d4'_polyeq'_equation
71 bool list] => bool list"
72 ("((Script Solve'_d4'_polyeq'_equation (_ _ =))//
76 bool list] => bool list"
77 ("((Script Biquadrat'_poly (_ _=))//
80 (*-------------------- rules -------------------------------------------------*)
81 (* type real enforced by op "^^^" *)
83 cancel_leading_coeff1: "Not (c =!= 0) ==> (a + b*bdv + c*bdv^^^2 = 0) =
84 (a/c + b/c*bdv + bdv^^^2 = 0)" and
85 cancel_leading_coeff2: "Not (c =!= 0) ==> (a - b*bdv + c*bdv^^^2 = 0) =
86 (a/c - b/c*bdv + bdv^^^2 = 0)" and
87 cancel_leading_coeff3: "Not (c =!= 0) ==> (a + b*bdv - c*bdv^^^2 = 0) =
88 (a/c + b/c*bdv - bdv^^^2 = 0)" and
90 cancel_leading_coeff4: "Not (c =!= 0) ==> (a + bdv + c*bdv^^^2 = 0) =
91 (a/c + 1/c*bdv + bdv^^^2 = 0)" and
92 cancel_leading_coeff5: "Not (c =!= 0) ==> (a - bdv + c*bdv^^^2 = 0) =
93 (a/c - 1/c*bdv + bdv^^^2 = 0)" and
94 cancel_leading_coeff6: "Not (c =!= 0) ==> (a + bdv - c*bdv^^^2 = 0) =
95 (a/c + 1/c*bdv - bdv^^^2 = 0)" and
97 cancel_leading_coeff7: "Not (c =!= 0) ==> ( b*bdv + c*bdv^^^2 = 0) =
98 ( b/c*bdv + bdv^^^2 = 0)" and
99 cancel_leading_coeff8: "Not (c =!= 0) ==> ( b*bdv - c*bdv^^^2 = 0) =
100 ( b/c*bdv - bdv^^^2 = 0)" and
102 cancel_leading_coeff9: "Not (c =!= 0) ==> ( bdv + c*bdv^^^2 = 0) =
103 ( 1/c*bdv + bdv^^^2 = 0)" and
104 cancel_leading_coeff10:"Not (c =!= 0) ==> ( bdv - c*bdv^^^2 = 0) =
105 ( 1/c*bdv - bdv^^^2 = 0)" and
107 cancel_leading_coeff11:"Not (c =!= 0) ==> (a + b*bdv^^^2 = 0) =
108 (a/b + bdv^^^2 = 0)" and
109 cancel_leading_coeff12:"Not (c =!= 0) ==> (a - b*bdv^^^2 = 0) =
110 (a/b - bdv^^^2 = 0)" and
111 cancel_leading_coeff13:"Not (c =!= 0) ==> ( b*bdv^^^2 = 0) =
112 ( bdv^^^2 = 0/b)" and
114 complete_square1: "(q + p*bdv + bdv^^^2 = 0) =
115 (q + (p/2 + bdv)^^^2 = (p/2)^^^2)" and
116 complete_square2: "( p*bdv + bdv^^^2 = 0) =
117 ( (p/2 + bdv)^^^2 = (p/2)^^^2)" and
118 complete_square3: "( bdv + bdv^^^2 = 0) =
119 ( (1/2 + bdv)^^^2 = (1/2)^^^2)" and
121 complete_square4: "(q - p*bdv + bdv^^^2 = 0) =
122 (q + (p/2 - bdv)^^^2 = (p/2)^^^2)" and
123 complete_square5: "(q + p*bdv - bdv^^^2 = 0) =
124 (q + (p/2 - bdv)^^^2 = (p/2)^^^2)" and
126 square_explicit1: "(a + b^^^2 = c) = ( b^^^2 = c - a)" and
127 square_explicit2: "(a - b^^^2 = c) = (-(b^^^2) = c - a)" and
129 (*bdv_explicit* required type constrain to real in --- (-8 - 2*x + x^^^2 = 0), by rewriting ---*)
130 bdv_explicit1: "(a + bdv = b) = (bdv = - a + (b::real))" and
131 bdv_explicit2: "(a - bdv = b) = ((-1)*bdv = - a + (b::real))" and
132 bdv_explicit3: "((-1)*bdv = b) = (bdv = (-1)*(b::real))" and
134 plus_leq: "(0 <= a + b) = ((-1)*b <= a)"(*Isa?*) and
135 minus_leq: "(0 <= a - b) = ( b <= a)"(*Isa?*) and
138 (*WN0509 compare LinEq.all_left "[|Not(b=!=0)|] ==> (a=b) = (a+(-1)*b=0)"*)
139 all_left: "[|Not(b=!=0)|] ==> (a = b) = (a - b = 0)" and
140 makex1_x: "a^^^1 = a" and
141 real_assoc_1: "a+(b+c) = a+b+c" and
142 real_assoc_2: "a*(b*c) = a*b*c" and
144 (* ---- degree 0 ----*)
145 d0_true: "(0=0) = True" and
146 d0_false: "[|Not(bdv occurs_in a);Not(a=0)|] ==> (a=0) = False" and
147 (* ---- degree 1 ----*)
149 "[|Not(bdv occurs_in a)|] ==> (a + b*bdv = 0) = (b*bdv = (-1)*a)" and
151 "[|Not(bdv occurs_in a)|] ==> (a + bdv = 0) = ( bdv = (-1)*a)" and
153 "[|Not(b=0);Not(bdv occurs_in c)|] ==> (b*bdv = c) = (bdv = c/b)" and
154 (* ---- degree 2 ----*)
156 "[|Not(bdv occurs_in a)|] ==> (a + b*bdv^^^2=0) = (b*bdv^^^2= (-1)*a)" and
158 "[|Not(bdv occurs_in a)|] ==> (a + bdv^^^2=0) = ( bdv^^^2= (-1)*a)" and
160 "[|Not(b=0);Not(bdv occurs_in c)|] ==> (b*bdv^^^2=c) = (bdv^^^2=c/b)" and
162 d2_prescind1: "(a*bdv + b*bdv^^^2 = 0) = (bdv*(a +b*bdv)=0)" and
163 d2_prescind2: "(a*bdv + bdv^^^2 = 0) = (bdv*(a + bdv)=0)" and
164 d2_prescind3: "( bdv + b*bdv^^^2 = 0) = (bdv*(1+b*bdv)=0)" and
165 d2_prescind4: "( bdv + bdv^^^2 = 0) = (bdv*(1+ bdv)=0)" and
166 (* eliminate degree 2 *)
167 (* thm for neg arguments in sqroot have postfix _neg *)
168 d2_sqrt_equation1: "[|(0<=c);Not(bdv occurs_in c)|] ==>
169 (bdv^^^2=c) = ((bdv=sqrt c) | (bdv=(-1)*sqrt c ))" and
170 d2_sqrt_equation1_neg:
171 "[|(c<0);Not(bdv occurs_in c)|] ==> (bdv^^^2=c) = False" and
172 d2_sqrt_equation2: "(bdv^^^2=0) = (bdv=0)" and
173 d2_sqrt_equation3: "(b*bdv^^^2=0) = (bdv=0)"
174 axiomatization where (*AK..if replaced by "and" we get errors:
175 exception PTREE "nth _ []" raised
176 (line 783 of "/usr/local/isabisac/src/Tools/isac/Interpret/ctree.sml"):
177 'fun nth _ [] = raise PTREE "nth _ []"'
179 exception Bind raised
180 (line 1097 of "/usr/local/isabisac/test/Tools/isac/Frontend/interface.sml"):
181 'val (Form f, tac, asms) = pt_extract (pt, p);' *)
182 (* WN120315 these 2 thms need "::real", because no "^^^" constrains type as
183 required in test --- rls d2_polyeq_bdv_only_simplify --- *)
184 d2_reduce_equation1: "(bdv*(a +b*bdv)=0) = ((bdv=0)|(a+b*bdv=(0::real)))" and
185 d2_reduce_equation2: "(bdv*(a + bdv)=0) = ((bdv=0)|(a+ bdv=(0::real)))"
187 axiomatization where (*..if replaced by "and" we get errors:
188 exception PTREE "nth _ []" raised
189 (line 783 of "/usr/local/isabisac/src/Tools/isac/Interpret/ctree.sml"):
190 'fun nth _ [] = raise PTREE "nth _ []"'
192 exception Bind raised
193 (line 1097 of "/usr/local/isabisac/test/Tools/isac/Frontend/interface.sml"):
194 'val (Form f, tac, asms) = pt_extract (pt, p);' *)
195 d2_pqformula1: "[|0<=p^^^2 - 4*q|] ==> (q+p*bdv+ bdv^^^2=0) =
196 ((bdv= (-1)*(p/2) + sqrt(p^^^2 - 4*q)/2)
197 | (bdv= (-1)*(p/2) - sqrt(p^^^2 - 4*q)/2))" and
198 d2_pqformula1_neg: "[|p^^^2 - 4*q<0|] ==> (q+p*bdv+ bdv^^^2=0) = False" and
199 d2_pqformula2: "[|0<=p^^^2 - 4*q|] ==> (q+p*bdv+1*bdv^^^2=0) =
200 ((bdv= (-1)*(p/2) + sqrt(p^^^2 - 4*q)/2)
201 | (bdv= (-1)*(p/2) - sqrt(p^^^2 - 4*q)/2))" and
202 d2_pqformula2_neg: "[|p^^^2 - 4*q<0|] ==> (q+p*bdv+1*bdv^^^2=0) = False" and
203 d2_pqformula3: "[|0<=1 - 4*q|] ==> (q+ bdv+ bdv^^^2=0) =
204 ((bdv= (-1)*(1/2) + sqrt(1 - 4*q)/2)
205 | (bdv= (-1)*(1/2) - sqrt(1 - 4*q)/2))" and
206 d2_pqformula3_neg: "[|1 - 4*q<0|] ==> (q+ bdv+ bdv^^^2=0) = False" and
207 d2_pqformula4: "[|0<=1 - 4*q|] ==> (q+ bdv+1*bdv^^^2=0) =
208 ((bdv= (-1)*(1/2) + sqrt(1 - 4*q)/2)
209 | (bdv= (-1)*(1/2) - sqrt(1 - 4*q)/2))" and
210 d2_pqformula4_neg: "[|1 - 4*q<0|] ==> (q+ bdv+1*bdv^^^2=0) = False" and
211 d2_pqformula5: "[|0<=p^^^2 - 0|] ==> ( p*bdv+ bdv^^^2=0) =
212 ((bdv= (-1)*(p/2) + sqrt(p^^^2 - 0)/2)
213 | (bdv= (-1)*(p/2) - sqrt(p^^^2 - 0)/2))" and
214 (* d2_pqformula5_neg not need p^2 never less zero in R *)
215 d2_pqformula6: "[|0<=p^^^2 - 0|] ==> ( p*bdv+1*bdv^^^2=0) =
216 ((bdv= (-1)*(p/2) + sqrt(p^^^2 - 0)/2)
217 | (bdv= (-1)*(p/2) - sqrt(p^^^2 - 0)/2))" and
218 (* d2_pqformula6_neg not need p^2 never less zero in R *)
219 d2_pqformula7: "[|0<=1 - 0|] ==> ( bdv+ bdv^^^2=0) =
220 ((bdv= (-1)*(1/2) + sqrt(1 - 0)/2)
221 | (bdv= (-1)*(1/2) - sqrt(1 - 0)/2))" and
222 (* d2_pqformula7_neg not need, because 1<0 ==> False*)
223 d2_pqformula8: "[|0<=1 - 0|] ==> ( bdv+1*bdv^^^2=0) =
224 ((bdv= (-1)*(1/2) + sqrt(1 - 0)/2)
225 | (bdv= (-1)*(1/2) - sqrt(1 - 0)/2))" and
226 (* d2_pqformula8_neg not need, because 1<0 ==> False*)
227 d2_pqformula9: "[|Not(bdv occurs_in q); 0<= (-1)*4*q|] ==>
228 (q+ 1*bdv^^^2=0) = ((bdv= 0 + sqrt(0 - 4*q)/2)
229 | (bdv= 0 - sqrt(0 - 4*q)/2))" and
231 "[|Not(bdv occurs_in q); (-1)*4*q<0|] ==> (q+ 1*bdv^^^2=0) = False" and
233 "[|Not(bdv occurs_in q); 0<= (-1)*4*q|] ==> (q+ bdv^^^2=0) =
234 ((bdv= 0 + sqrt(0 - 4*q)/2)
235 | (bdv= 0 - sqrt(0 - 4*q)/2))" and
237 "[|Not(bdv occurs_in q); (-1)*4*q<0|] ==> (q+ bdv^^^2=0) = False" and
239 "[|0<=b^^^2 - 4*a*c|] ==> (c + b*bdv+a*bdv^^^2=0) =
240 ((bdv=( -b + sqrt(b^^^2 - 4*a*c))/(2*a))
241 | (bdv=( -b - sqrt(b^^^2 - 4*a*c))/(2*a)))" and
243 "[|b^^^2 - 4*a*c<0|] ==> (c + b*bdv+a*bdv^^^2=0) = False" and
245 "[|0<=1 - 4*a*c|] ==> (c+ bdv+a*bdv^^^2=0) =
246 ((bdv=( -1 + sqrt(1 - 4*a*c))/(2*a))
247 | (bdv=( -1 - sqrt(1 - 4*a*c))/(2*a)))" and
249 "[|1 - 4*a*c<0|] ==> (c+ bdv+a*bdv^^^2=0) = False" and
251 "[|0<=b^^^2 - 4*1*c|] ==> (c + b*bdv+ bdv^^^2=0) =
252 ((bdv=( -b + sqrt(b^^^2 - 4*1*c))/(2*1))
253 | (bdv=( -b - sqrt(b^^^2 - 4*1*c))/(2*1)))" and
255 "[|b^^^2 - 4*1*c<0|] ==> (c + b*bdv+ bdv^^^2=0) = False" and
257 "[|0<=1 - 4*1*c|] ==> (c + bdv+ bdv^^^2=0) =
258 ((bdv=( -1 + sqrt(1 - 4*1*c))/(2*1))
259 | (bdv=( -1 - sqrt(1 - 4*1*c))/(2*1)))" and
261 "[|1 - 4*1*c<0|] ==> (c + bdv+ bdv^^^2=0) = False" and
263 "[|Not(bdv occurs_in c); 0<=0 - 4*a*c|] ==> (c + a*bdv^^^2=0) =
264 ((bdv=( 0 + sqrt(0 - 4*a*c))/(2*a))
265 | (bdv=( 0 - sqrt(0 - 4*a*c))/(2*a)))" and
267 "[|Not(bdv occurs_in c); 0 - 4*a*c<0|] ==> (c + a*bdv^^^2=0) = False" and
269 "[|Not(bdv occurs_in c); 0<=0 - 4*1*c|] ==> (c+ bdv^^^2=0) =
270 ((bdv=( 0 + sqrt(0 - 4*1*c))/(2*1))
271 | (bdv=( 0 - sqrt(0 - 4*1*c))/(2*1)))" and
273 "[|Not(bdv occurs_in c); 0 - 4*1*c<0|] ==> (c+ bdv^^^2=0) = False" and
275 "[|0<=b^^^2 - 0|] ==> ( b*bdv+a*bdv^^^2=0) =
276 ((bdv=( -b + sqrt(b^^^2 - 0))/(2*a))
277 | (bdv=( -b - sqrt(b^^^2 - 0))/(2*a)))" and
278 (* d2_abcformula7_neg not need b^2 never less zero in R *)
280 "[|0<=b^^^2 - 0|] ==> ( b*bdv+ bdv^^^2=0) =
281 ((bdv=( -b + sqrt(b^^^2 - 0))/(2*1))
282 | (bdv=( -b - sqrt(b^^^2 - 0))/(2*1)))" and
283 (* d2_abcformula8_neg not need b^2 never less zero in R *)
285 "[|0<=1 - 0|] ==> ( bdv+a*bdv^^^2=0) =
286 ((bdv=( -1 + sqrt(1 - 0))/(2*a))
287 | (bdv=( -1 - sqrt(1 - 0))/(2*a)))" and
288 (* d2_abcformula9_neg not need, because 1<0 ==> False*)
290 "[|0<=1 - 0|] ==> ( bdv+ bdv^^^2=0) =
291 ((bdv=( -1 + sqrt(1 - 0))/(2*1))
292 | (bdv=( -1 - sqrt(1 - 0))/(2*1)))" and
293 (* d2_abcformula10_neg not need, because 1<0 ==> False*)
296 (* ---- degree 3 ----*)
298 "(a*bdv + b*bdv^^^2 + c*bdv^^^3=0) = (bdv=0 | (a + b*bdv + c*bdv^^^2=0))" and
300 "( bdv + b*bdv^^^2 + c*bdv^^^3=0) = (bdv=0 | (1 + b*bdv + c*bdv^^^2=0))" and
302 "(a*bdv + bdv^^^2 + c*bdv^^^3=0) = (bdv=0 | (a + bdv + c*bdv^^^2=0))" and
304 "( bdv + bdv^^^2 + c*bdv^^^3=0) = (bdv=0 | (1 + bdv + c*bdv^^^2=0))" and
306 "(a*bdv + b*bdv^^^2 + bdv^^^3=0) = (bdv=0 | (a + b*bdv + bdv^^^2=0))" and
308 "( bdv + b*bdv^^^2 + bdv^^^3=0) = (bdv=0 | (1 + b*bdv + bdv^^^2=0))" and
310 "(a*bdv + bdv^^^2 + bdv^^^3=0) = (bdv=0 | (1 + bdv + bdv^^^2=0))" and
312 "( bdv + bdv^^^2 + bdv^^^3=0) = (bdv=0 | (1 + bdv + bdv^^^2=0))" and
314 "(a*bdv + c*bdv^^^3=0) = (bdv=0 | (a + c*bdv^^^2=0))" and
315 d3_reduce_equation10:
316 "( bdv + c*bdv^^^3=0) = (bdv=0 | (1 + c*bdv^^^2=0))" and
317 d3_reduce_equation11:
318 "(a*bdv + bdv^^^3=0) = (bdv=0 | (a + bdv^^^2=0))" and
319 d3_reduce_equation12:
320 "( bdv + bdv^^^3=0) = (bdv=0 | (1 + bdv^^^2=0))" and
321 d3_reduce_equation13:
322 "( b*bdv^^^2 + c*bdv^^^3=0) = (bdv=0 | ( b*bdv + c*bdv^^^2=0))" and
323 d3_reduce_equation14:
324 "( bdv^^^2 + c*bdv^^^3=0) = (bdv=0 | ( bdv + c*bdv^^^2=0))" and
325 d3_reduce_equation15:
326 "( b*bdv^^^2 + bdv^^^3=0) = (bdv=0 | ( b*bdv + bdv^^^2=0))" and
327 d3_reduce_equation16:
328 "( bdv^^^2 + bdv^^^3=0) = (bdv=0 | ( bdv + bdv^^^2=0))" and
330 "[|Not(bdv occurs_in a)|] ==> (a + b*bdv^^^3=0) = (b*bdv^^^3= (-1)*a)" and
332 "[|Not(bdv occurs_in a)|] ==> (a + bdv^^^3=0) = ( bdv^^^3= (-1)*a)" and
334 "[|Not(b=0);Not(bdv occurs_in a)|] ==> (b*bdv^^^3=c) = (bdv^^^3=c/b)" and
336 "(bdv^^^3=0) = (bdv=0)" and
338 "(bdv^^^3=c) = (bdv = nroot 3 c)" and
340 (* ---- degree 4 ----*)
341 (* RL03.FIXME es wir nicht getestet ob u>0 *)
343 "(c+b*bdv^^^2+a*bdv^^^4=0) =
344 ((a*u^^^2+b*u+c=0) & (bdv^^^2=u))" and
346 (* ---- 7.3.02 von Termorder ---- *)
348 bdv_collect_1: "l * bdv + m * bdv = (l + m) * bdv" and
349 bdv_collect_2: "bdv + m * bdv = (1 + m) * bdv" and
350 bdv_collect_3: "l * bdv + bdv = (l + 1) * bdv" and
352 (* bdv_collect_assoc0_1 "l * bdv + m * bdv + k = (l + m) * bdv + k"
353 bdv_collect_assoc0_2 "bdv + m * bdv + k = (1 + m) * bdv + k"
354 bdv_collect_assoc0_3 "l * bdv + bdv + k = (l + 1) * bdv + k"
356 bdv_collect_assoc1_1: "l * bdv + (m * bdv + k) = (l + m) * bdv + k" and
357 bdv_collect_assoc1_2: "bdv + (m * bdv + k) = (1 + m) * bdv + k" and
358 bdv_collect_assoc1_3: "l * bdv + (bdv + k) = (l + 1) * bdv + k" and
360 bdv_collect_assoc2_1: "k + l * bdv + m * bdv = k + (l + m) * bdv" and
361 bdv_collect_assoc2_2: "k + bdv + m * bdv = k + (1 + m) * bdv" and
362 bdv_collect_assoc2_3: "k + l * bdv + bdv = k + (l + 1) * bdv" and
365 bdv_n_collect_1: "l * bdv^^^n + m * bdv^^^n = (l + m) * bdv^^^n" and
366 bdv_n_collect_2: " bdv^^^n + m * bdv^^^n = (1 + m) * bdv^^^n" and
367 bdv_n_collect_3: "l * bdv^^^n + bdv^^^n = (l + 1) * bdv^^^n" (*order!*) and
369 bdv_n_collect_assoc1_1:
370 "l * bdv^^^n + (m * bdv^^^n + k) = (l + m) * bdv^^^n + k" and
371 bdv_n_collect_assoc1_2: "bdv^^^n + (m * bdv^^^n + k) = (1 + m) * bdv^^^n + k" and
372 bdv_n_collect_assoc1_3: "l * bdv^^^n + (bdv^^^n + k) = (l + 1) * bdv^^^n + k" and
374 bdv_n_collect_assoc2_1: "k + l * bdv^^^n + m * bdv^^^n = k +(l + m) * bdv^^^n" and
375 bdv_n_collect_assoc2_2: "k + bdv^^^n + m * bdv^^^n = k + (1 + m) * bdv^^^n" and
376 bdv_n_collect_assoc2_3: "k + l * bdv^^^n + bdv^^^n = k + (l + 1) * bdv^^^n" and
379 real_minus_div: "- (a / b) = (-1 * a) / b" and
381 separate_bdv: "(a * bdv) / b = (a / b) * (bdv::real)" and
382 separate_bdv_n: "(a * bdv ^^^ n) / b = (a / b) * bdv ^^^ n" and
383 separate_1_bdv: "bdv / b = (1 / b) * (bdv::real)" and
384 separate_1_bdv_n: "bdv ^^^ n / b = (1 / b) * bdv ^^^ n"
389 (*-------------------------rulse-------------------------*)
390 val PolyEq_prls = (*3.10.02:just the following order due to subterm evaluation*)
391 append_rls "PolyEq_prls" e_rls
392 [Calc ("Atools.ident",eval_ident "#ident_"),
393 Calc ("Tools.matches",eval_matches ""),
394 Calc ("Tools.lhs" ,eval_lhs ""),
395 Calc ("Tools.rhs" ,eval_rhs ""),
396 Calc ("Poly.is'_expanded'_in",eval_is_expanded_in ""),
397 Calc ("Poly.is'_poly'_in",eval_is_poly_in ""),
398 Calc ("Poly.has'_degree'_in",eval_has_degree_in ""),
399 Calc ("Poly.is'_polyrat'_in",eval_is_polyrat_in ""),
400 (*Calc ("Atools.occurs'_in",eval_occurs_in ""), *)
401 (*Calc ("Atools.is'_const",eval_const "#is_const_"),*)
402 Calc ("HOL.eq",eval_equal "#equal_"),
403 Calc ("RootEq.is'_rootTerm'_in",eval_is_rootTerm_in ""),
404 Calc ("RatEq.is'_ratequation'_in",eval_is_ratequation_in ""),
405 Thm ("not_true",num_str @{thm not_true}),
406 Thm ("not_false",num_str @{thm not_false}),
407 Thm ("and_true",num_str @{thm and_true}),
408 Thm ("and_false",num_str @{thm and_false}),
409 Thm ("or_true",num_str @{thm or_true}),
410 Thm ("or_false",num_str @{thm or_false})
414 merge_rls "PolyEq_erls" LinEq_erls
415 (append_rls "ops_preds" calculate_Rational
416 [Calc ("HOL.eq",eval_equal "#equal_"),
417 Thm ("plus_leq", num_str @{thm plus_leq}),
418 Thm ("minus_leq", num_str @{thm minus_leq}),
419 Thm ("rat_leq1", num_str @{thm rat_leq1}),
420 Thm ("rat_leq2", num_str @{thm rat_leq2}),
421 Thm ("rat_leq3", num_str @{thm rat_leq3})
425 merge_rls "PolyEq_crls" LinEq_crls
426 (append_rls "ops_preds" calculate_Rational
427 [Calc ("HOL.eq",eval_equal "#equal_"),
428 Thm ("plus_leq", num_str @{thm plus_leq}),
429 Thm ("minus_leq", num_str @{thm minus_leq}),
430 Thm ("rat_leq1", num_str @{thm rat_leq1}),
431 Thm ("rat_leq2", num_str @{thm rat_leq2}),
432 Thm ("rat_leq3", num_str @{thm rat_leq3})
435 val cancel_leading_coeff = prep_rls'(
436 Rls {id = "cancel_leading_coeff", preconds = [],
437 rew_ord = ("e_rew_ord",e_rew_ord),
438 erls = PolyEq_erls, srls = Erls, calc = [], errpatts = [],
440 [Thm ("cancel_leading_coeff1",num_str @{thm cancel_leading_coeff1}),
441 Thm ("cancel_leading_coeff2",num_str @{thm cancel_leading_coeff2}),
442 Thm ("cancel_leading_coeff3",num_str @{thm cancel_leading_coeff3}),
443 Thm ("cancel_leading_coeff4",num_str @{thm cancel_leading_coeff4}),
444 Thm ("cancel_leading_coeff5",num_str @{thm cancel_leading_coeff5}),
445 Thm ("cancel_leading_coeff6",num_str @{thm cancel_leading_coeff6}),
446 Thm ("cancel_leading_coeff7",num_str @{thm cancel_leading_coeff7}),
447 Thm ("cancel_leading_coeff8",num_str @{thm cancel_leading_coeff8}),
448 Thm ("cancel_leading_coeff9",num_str @{thm cancel_leading_coeff9}),
449 Thm ("cancel_leading_coeff10",num_str @{thm cancel_leading_coeff10}),
450 Thm ("cancel_leading_coeff11",num_str @{thm cancel_leading_coeff11}),
451 Thm ("cancel_leading_coeff12",num_str @{thm cancel_leading_coeff12}),
452 Thm ("cancel_leading_coeff13",num_str @{thm cancel_leading_coeff13})
453 ],scr = Prog ((Thm.term_of o the o (parse thy)) "empty_script")}:rls);
455 val prep_rls' = prep_rls @{theory};
458 val complete_square = prep_rls'(
459 Rls {id = "complete_square", preconds = [],
460 rew_ord = ("e_rew_ord",e_rew_ord),
461 erls = PolyEq_erls, srls = Erls, calc = [], errpatts = [],
462 rules = [Thm ("complete_square1",num_str @{thm complete_square1}),
463 Thm ("complete_square2",num_str @{thm complete_square2}),
464 Thm ("complete_square3",num_str @{thm complete_square3}),
465 Thm ("complete_square4",num_str @{thm complete_square4}),
466 Thm ("complete_square5",num_str @{thm complete_square5})
468 scr = Prog ((Thm.term_of o the o (parse thy)) "empty_script")
471 val polyeq_simplify = prep_rls'(
472 Rls {id = "polyeq_simplify", preconds = [],
473 rew_ord = ("termlessI",termlessI),
476 calc = [], errpatts = [],
477 rules = [Thm ("real_assoc_1",num_str @{thm real_assoc_1}),
478 Thm ("real_assoc_2",num_str @{thm real_assoc_2}),
479 Thm ("real_diff_minus",num_str @{thm real_diff_minus}),
480 Thm ("real_unari_minus",num_str @{thm real_unari_minus}),
481 Thm ("realpow_multI",num_str @{thm realpow_multI}),
482 Calc ("Groups.plus_class.plus",eval_binop "#add_"),
483 Calc ("Groups.minus_class.minus",eval_binop "#sub_"),
484 Calc ("Groups.times_class.times",eval_binop "#mult_"),
485 Calc ("Fields.inverse_class.divide", eval_cancel "#divide_e"),
486 Calc ("NthRoot.sqrt",eval_sqrt "#sqrt_"),
487 Calc ("Atools.pow" ,eval_binop "#power_"),
490 scr = Prog ((Thm.term_of o the o (parse thy)) "empty_script")
493 setup {* KEStore_Elems.add_rlss
494 [("cancel_leading_coeff", (Context.theory_name @{theory}, cancel_leading_coeff)),
495 ("complete_square", (Context.theory_name @{theory}, complete_square)),
496 ("PolyEq_erls", (Context.theory_name @{theory}, PolyEq_erls)),
497 ("polyeq_simplify", (Context.theory_name @{theory}, polyeq_simplify))] *}
500 (* ------------- polySolve ------------------ *)
502 (*isolate the bound variable in an d0 equation; 'bdv' is a meta-constant*)
503 val d0_polyeq_simplify = prep_rls'(
504 Rls {id = "d0_polyeq_simplify", preconds = [],
505 rew_ord = ("e_rew_ord",e_rew_ord),
508 calc = [], errpatts = [],
509 rules = [Thm("d0_true",num_str @{thm d0_true}),
510 Thm("d0_false",num_str @{thm d0_false})
512 scr = Prog ((Thm.term_of o the o (parse thy)) "empty_script")
516 (*isolate the bound variable in an d1 equation; 'bdv' is a meta-constant*)
517 val d1_polyeq_simplify = prep_rls'(
518 Rls {id = "d1_polyeq_simplify", preconds = [],
519 rew_ord = ("e_rew_ord",e_rew_ord),
522 calc = [], errpatts = [],
524 Thm("d1_isolate_add1",num_str @{thm d1_isolate_add1}),
525 (* a+bx=0 -> bx=-a *)
526 Thm("d1_isolate_add2",num_str @{thm d1_isolate_add2}),
528 Thm("d1_isolate_div",num_str @{thm d1_isolate_div})
531 scr = Prog ((Thm.term_of o the o (parse thy)) "empty_script")
535 subsection {* degree 2 *}
537 (* isolate the bound variable in an d2 equation with bdv only;
538 "bdv" is a meta-constant substituted for the "x" below by isac's rewriter. *)
539 val d2_polyeq_bdv_only_simplify = prep_rls'(
540 Rls {id = "d2_polyeq_bdv_only_simplify", preconds = [], rew_ord = ("e_rew_ord",e_rew_ord),
541 erls = PolyEq_erls, srls = Erls, calc = [], errpatts = [],
543 [Thm ("d2_prescind1", num_str @{thm d2_prescind1}), (* ax+bx^2=0 -> x(a+bx)=0 *)
544 Thm ("d2_prescind2", num_str @{thm d2_prescind2}), (* ax+ x^2=0 -> x(a+ x)=0 *)
545 Thm ("d2_prescind3", num_str @{thm d2_prescind3}), (* x+bx^2=0 -> x(1+bx)=0 *)
546 Thm ("d2_prescind4", num_str @{thm d2_prescind4}), (* x+ x^2=0 -> x(1+ x)=0 *)
547 Thm ("d2_sqrt_equation1", num_str @{thm d2_sqrt_equation1}), (* x^2=c -> x=+-sqrt(c) *)
548 Thm ("d2_sqrt_equation1_neg", num_str @{thm d2_sqrt_equation1_neg}), (* [0<c] x^2=c -> []*)
549 Thm ("d2_sqrt_equation2", num_str @{thm d2_sqrt_equation2}), (* x^2=0 -> x=0 *)
550 Thm ("d2_reduce_equation1", num_str @{thm d2_reduce_equation1}),(* x(a+bx)=0 -> x=0 |a+bx=0*)
551 Thm ("d2_reduce_equation2", num_str @{thm d2_reduce_equation2}),(* x(a+ x)=0 -> x=0 |a+ x=0*)
552 Thm ("d2_isolate_div", num_str @{thm d2_isolate_div}) (* bx^2=c -> x^2=c/b *)
554 scr = Prog ((Thm.term_of o the o (parse thy)) "empty_script")
558 (* isolate the bound variable in an d2 equation with sqrt only;
559 'bdv' is a meta-constant*)
560 val d2_polyeq_sq_only_simplify = prep_rls'(
561 Rls {id = "d2_polyeq_sq_only_simplify", preconds = [],
562 rew_ord = ("e_rew_ord",e_rew_ord),
565 calc = [], errpatts = [],
566 (*asm_thm = [("d2_sqrt_equation1",""),("d2_sqrt_equation1_neg",""),
567 ("d2_isolate_div","")],*)
568 rules = [Thm("d2_isolate_add1",num_str @{thm d2_isolate_add1}),
569 (* a+ bx^2=0 -> bx^2=(-1)a*)
570 Thm("d2_isolate_add2",num_str @{thm d2_isolate_add2}),
571 (* a+ x^2=0 -> x^2=(-1)a*)
572 Thm("d2_sqrt_equation2",num_str @{thm d2_sqrt_equation2}),
574 Thm("d2_sqrt_equation1",num_str @{thm d2_sqrt_equation1}),
575 (* x^2=c -> x=+-sqrt(c)*)
576 Thm("d2_sqrt_equation1_neg",num_str @{thm d2_sqrt_equation1_neg}),
577 (* [c<0] x^2=c -> x=[] *)
578 Thm("d2_isolate_div",num_str @{thm d2_isolate_div})
579 (* bx^2=c -> x^2=c/b*)
581 scr = Prog ((Thm.term_of o the o (parse thy)) "empty_script")
585 (* isolate the bound variable in an d2 equation with pqFormula;
586 'bdv' is a meta-constant*)
587 val d2_polyeq_pqFormula_simplify = prep_rls'(
588 Rls {id = "d2_polyeq_pqFormula_simplify", preconds = [],
589 rew_ord = ("e_rew_ord",e_rew_ord), erls = PolyEq_erls,
590 srls = Erls, calc = [], errpatts = [],
591 rules = [Thm("d2_pqformula1",num_str @{thm d2_pqformula1}),
593 Thm("d2_pqformula1_neg",num_str @{thm d2_pqformula1_neg}),
595 Thm("d2_pqformula2",num_str @{thm d2_pqformula2}),
597 Thm("d2_pqformula2_neg",num_str @{thm d2_pqformula2_neg}),
599 Thm("d2_pqformula3",num_str @{thm d2_pqformula3}),
601 Thm("d2_pqformula3_neg",num_str @{thm d2_pqformula3_neg}),
603 Thm("d2_pqformula4",num_str @{thm d2_pqformula4}),
605 Thm("d2_pqformula4_neg",num_str @{thm d2_pqformula4_neg}),
607 Thm("d2_pqformula5",num_str @{thm d2_pqformula5}),
609 Thm("d2_pqformula6",num_str @{thm d2_pqformula6}),
611 Thm("d2_pqformula7",num_str @{thm d2_pqformula7}),
613 Thm("d2_pqformula8",num_str @{thm d2_pqformula8}),
615 Thm("d2_pqformula9",num_str @{thm d2_pqformula9}),
617 Thm("d2_pqformula9_neg",num_str @{thm d2_pqformula9_neg}),
619 Thm("d2_pqformula10",num_str @{thm d2_pqformula10}),
621 Thm("d2_pqformula10_neg",num_str @{thm d2_pqformula10_neg}),
623 Thm("d2_sqrt_equation2",num_str @{thm d2_sqrt_equation2}),
625 Thm("d2_sqrt_equation3",num_str @{thm d2_sqrt_equation3})
627 ],scr = Prog ((Thm.term_of o the o (parse thy)) "empty_script")
631 (* isolate the bound variable in an d2 equation with abcFormula;
632 'bdv' is a meta-constant*)
633 val d2_polyeq_abcFormula_simplify = prep_rls'(
634 Rls {id = "d2_polyeq_abcFormula_simplify", preconds = [],
635 rew_ord = ("e_rew_ord",e_rew_ord), erls = PolyEq_erls,
636 srls = Erls, calc = [], errpatts = [],
637 rules = [Thm("d2_abcformula1",num_str @{thm d2_abcformula1}),
639 Thm("d2_abcformula1_neg",num_str @{thm d2_abcformula1_neg}),
641 Thm("d2_abcformula2",num_str @{thm d2_abcformula2}),
643 Thm("d2_abcformula2_neg",num_str @{thm d2_abcformula2_neg}),
645 Thm("d2_abcformula3",num_str @{thm d2_abcformula3}),
647 Thm("d2_abcformula3_neg",num_str @{thm d2_abcformula3_neg}),
649 Thm("d2_abcformula4",num_str @{thm d2_abcformula4}),
651 Thm("d2_abcformula4_neg",num_str @{thm d2_abcformula4_neg}),
653 Thm("d2_abcformula5",num_str @{thm d2_abcformula5}),
655 Thm("d2_abcformula5_neg",num_str @{thm d2_abcformula5_neg}),
657 Thm("d2_abcformula6",num_str @{thm d2_abcformula6}),
659 Thm("d2_abcformula6_neg",num_str @{thm d2_abcformula6_neg}),
661 Thm("d2_abcformula7",num_str @{thm d2_abcformula7}),
663 Thm("d2_abcformula8",num_str @{thm d2_abcformula8}),
665 Thm("d2_abcformula9",num_str @{thm d2_abcformula9}),
667 Thm("d2_abcformula10",num_str @{thm d2_abcformula10}),
669 Thm("d2_sqrt_equation2",num_str @{thm d2_sqrt_equation2}),
671 Thm("d2_sqrt_equation3",num_str @{thm d2_sqrt_equation3})
674 scr = Prog ((Thm.term_of o the o (parse thy)) "empty_script")
679 (* isolate the bound variable in an d2 equation;
680 'bdv' is a meta-constant*)
681 val d2_polyeq_simplify = prep_rls'(
682 Rls {id = "d2_polyeq_simplify", preconds = [],
683 rew_ord = ("e_rew_ord",e_rew_ord), erls = PolyEq_erls,
684 srls = Erls, calc = [], errpatts = [],
685 rules = [Thm("d2_pqformula1",num_str @{thm d2_pqformula1}),
687 Thm("d2_pqformula1_neg",num_str @{thm d2_pqformula1_neg}),
689 Thm("d2_pqformula2",num_str @{thm d2_pqformula2}),
691 Thm("d2_pqformula2_neg",num_str @{thm d2_pqformula2_neg}),
693 Thm("d2_pqformula3",num_str @{thm d2_pqformula3}),
695 Thm("d2_pqformula3_neg",num_str @{thm d2_pqformula3_neg}),
697 Thm("d2_pqformula4",num_str @{thm d2_pqformula4}),
699 Thm("d2_pqformula4_neg",num_str @{thm d2_pqformula4_neg}),
701 Thm("d2_abcformula1",num_str @{thm d2_abcformula1}),
703 Thm("d2_abcformula1_neg",num_str @{thm d2_abcformula1_neg}),
705 Thm("d2_abcformula2",num_str @{thm d2_abcformula2}),
707 Thm("d2_abcformula2_neg",num_str @{thm d2_abcformula2_neg}),
709 Thm("d2_prescind1",num_str @{thm d2_prescind1}),
710 (* ax+bx^2=0 -> x(a+bx)=0 *)
711 Thm("d2_prescind2",num_str @{thm d2_prescind2}),
712 (* ax+ x^2=0 -> x(a+ x)=0 *)
713 Thm("d2_prescind3",num_str @{thm d2_prescind3}),
714 (* x+bx^2=0 -> x(1+bx)=0 *)
715 Thm("d2_prescind4",num_str @{thm d2_prescind4}),
716 (* x+ x^2=0 -> x(1+ x)=0 *)
717 Thm("d2_isolate_add1",num_str @{thm d2_isolate_add1}),
718 (* a+ bx^2=0 -> bx^2=(-1)a*)
719 Thm("d2_isolate_add2",num_str @{thm d2_isolate_add2}),
720 (* a+ x^2=0 -> x^2=(-1)a*)
721 Thm("d2_sqrt_equation1",num_str @{thm d2_sqrt_equation1}),
722 (* x^2=c -> x=+-sqrt(c)*)
723 Thm("d2_sqrt_equation1_neg",num_str @{thm d2_sqrt_equation1_neg}),
724 (* [c<0] x^2=c -> x=[]*)
725 Thm("d2_sqrt_equation2",num_str @{thm d2_sqrt_equation2}),
727 Thm("d2_reduce_equation1",num_str @{thm d2_reduce_equation1}),
728 (* x(a+bx)=0 -> x=0 | a+bx=0*)
729 Thm("d2_reduce_equation2",num_str @{thm d2_reduce_equation2}),
730 (* x(a+ x)=0 -> x=0 | a+ x=0*)
731 Thm("d2_isolate_div",num_str @{thm d2_isolate_div})
732 (* bx^2=c -> x^2=c/b*)
734 scr = Prog ((Thm.term_of o the o (parse thy)) "empty_script")
740 (* isolate the bound variable in an d3 equation; 'bdv' is a meta-constant *)
741 val d3_polyeq_simplify = prep_rls'(
742 Rls {id = "d3_polyeq_simplify", preconds = [],
743 rew_ord = ("e_rew_ord",e_rew_ord), erls = PolyEq_erls,
744 srls = Erls, calc = [], errpatts = [],
746 [Thm("d3_reduce_equation1",num_str @{thm d3_reduce_equation1}),
747 (*a*bdv + b*bdv^^^2 + c*bdv^^^3=0) =
748 (bdv=0 | (a + b*bdv + c*bdv^^^2=0)*)
749 Thm("d3_reduce_equation2",num_str @{thm d3_reduce_equation2}),
750 (* bdv + b*bdv^^^2 + c*bdv^^^3=0) =
751 (bdv=0 | (1 + b*bdv + c*bdv^^^2=0)*)
752 Thm("d3_reduce_equation3",num_str @{thm d3_reduce_equation3}),
753 (*a*bdv + bdv^^^2 + c*bdv^^^3=0) =
754 (bdv=0 | (a + bdv + c*bdv^^^2=0)*)
755 Thm("d3_reduce_equation4",num_str @{thm d3_reduce_equation4}),
756 (* bdv + bdv^^^2 + c*bdv^^^3=0) =
757 (bdv=0 | (1 + bdv + c*bdv^^^2=0)*)
758 Thm("d3_reduce_equation5",num_str @{thm d3_reduce_equation5}),
759 (*a*bdv + b*bdv^^^2 + bdv^^^3=0) =
760 (bdv=0 | (a + b*bdv + bdv^^^2=0)*)
761 Thm("d3_reduce_equation6",num_str @{thm d3_reduce_equation6}),
762 (* bdv + b*bdv^^^2 + bdv^^^3=0) =
763 (bdv=0 | (1 + b*bdv + bdv^^^2=0)*)
764 Thm("d3_reduce_equation7",num_str @{thm d3_reduce_equation7}),
765 (*a*bdv + bdv^^^2 + bdv^^^3=0) =
766 (bdv=0 | (1 + bdv + bdv^^^2=0)*)
767 Thm("d3_reduce_equation8",num_str @{thm d3_reduce_equation8}),
768 (* bdv + bdv^^^2 + bdv^^^3=0) =
769 (bdv=0 | (1 + bdv + bdv^^^2=0)*)
770 Thm("d3_reduce_equation9",num_str @{thm d3_reduce_equation9}),
771 (*a*bdv + c*bdv^^^3=0) =
772 (bdv=0 | (a + c*bdv^^^2=0)*)
773 Thm("d3_reduce_equation10",num_str @{thm d3_reduce_equation10}),
774 (* bdv + c*bdv^^^3=0) =
775 (bdv=0 | (1 + c*bdv^^^2=0)*)
776 Thm("d3_reduce_equation11",num_str @{thm d3_reduce_equation11}),
777 (*a*bdv + bdv^^^3=0) =
778 (bdv=0 | (a + bdv^^^2=0)*)
779 Thm("d3_reduce_equation12",num_str @{thm d3_reduce_equation12}),
780 (* bdv + bdv^^^3=0) =
781 (bdv=0 | (1 + bdv^^^2=0)*)
782 Thm("d3_reduce_equation13",num_str @{thm d3_reduce_equation13}),
783 (* b*bdv^^^2 + c*bdv^^^3=0) =
784 (bdv=0 | ( b*bdv + c*bdv^^^2=0)*)
785 Thm("d3_reduce_equation14",num_str @{thm d3_reduce_equation14}),
786 (* bdv^^^2 + c*bdv^^^3=0) =
787 (bdv=0 | ( bdv + c*bdv^^^2=0)*)
788 Thm("d3_reduce_equation15",num_str @{thm d3_reduce_equation15}),
789 (* b*bdv^^^2 + bdv^^^3=0) =
790 (bdv=0 | ( b*bdv + bdv^^^2=0)*)
791 Thm("d3_reduce_equation16",num_str @{thm d3_reduce_equation16}),
792 (* bdv^^^2 + bdv^^^3=0) =
793 (bdv=0 | ( bdv + bdv^^^2=0)*)
794 Thm("d3_isolate_add1",num_str @{thm d3_isolate_add1}),
795 (*[|Not(bdv occurs_in a)|] ==> (a + b*bdv^^^3=0) =
796 (bdv=0 | (b*bdv^^^3=a)*)
797 Thm("d3_isolate_add2",num_str @{thm d3_isolate_add2}),
798 (*[|Not(bdv occurs_in a)|] ==> (a + bdv^^^3=0) =
799 (bdv=0 | ( bdv^^^3=a)*)
800 Thm("d3_isolate_div",num_str @{thm d3_isolate_div}),
801 (*[|Not(b=0)|] ==> (b*bdv^^^3=c) = (bdv^^^3=c/b*)
802 Thm("d3_root_equation2",num_str @{thm d3_root_equation2}),
803 (*(bdv^^^3=0) = (bdv=0) *)
804 Thm("d3_root_equation1",num_str @{thm d3_root_equation1})
805 (*bdv^^^3=c) = (bdv = nroot 3 c*)
807 scr = Prog ((Thm.term_of o the o (parse thy)) "empty_script")
813 (*isolate the bound variable in an d4 equation; 'bdv' is a meta-constant*)
814 val d4_polyeq_simplify = prep_rls'(
815 Rls {id = "d4_polyeq_simplify", preconds = [],
816 rew_ord = ("e_rew_ord",e_rew_ord), erls = PolyEq_erls,
817 srls = Erls, calc = [], errpatts = [],
819 [Thm("d4_sub_u1",num_str @{thm d4_sub_u1})
820 (* ax^4+bx^2+c=0 -> x=+-sqrt(ax^2+bx^+c) *)
822 scr = Prog ((Thm.term_of o the o (parse thy)) "empty_script")
825 setup {* KEStore_Elems.add_rlss
826 [("d0_polyeq_simplify", (Context.theory_name @{theory}, d0_polyeq_simplify)),
827 ("d1_polyeq_simplify", (Context.theory_name @{theory}, d1_polyeq_simplify)),
828 ("d2_polyeq_simplify", (Context.theory_name @{theory}, d2_polyeq_simplify)),
829 ("d2_polyeq_bdv_only_simplify", (Context.theory_name @{theory}, d2_polyeq_bdv_only_simplify)),
830 ("d2_polyeq_sq_only_simplify", (Context.theory_name @{theory}, d2_polyeq_sq_only_simplify)),
832 ("d2_polyeq_pqFormula_simplify",
833 (Context.theory_name @{theory}, d2_polyeq_pqFormula_simplify)),
834 ("d2_polyeq_abcFormula_simplify",
835 (Context.theory_name @{theory}, d2_polyeq_abcFormula_simplify)),
836 ("d3_polyeq_simplify", (Context.theory_name @{theory}, d3_polyeq_simplify)),
837 ("d4_polyeq_simplify", (Context.theory_name @{theory}, d4_polyeq_simplify))] *}
839 (*------------------------problems------------------------*)
841 (get_pbt ["degree_2","polynomial","univariate","equation"]);
845 setup {* KEStore_Elems.add_pbts
846 [(Specify.prep_pbt thy "pbl_equ_univ_poly" [] e_pblID
847 (["polynomial","univariate","equation"],
848 [("#Given" ,["equality e_e","solveFor v_v"]),
849 ("#Where" ,["~((e_e::bool) is_ratequation_in (v_v::real))",
850 "~((lhs e_e) is_rootTerm_in (v_v::real))",
851 "~((rhs e_e) is_rootTerm_in (v_v::real))"]),
852 ("#Find" ,["solutions v_v'i'"])],
853 PolyEq_prls, SOME "solve (e_e::bool, v_v)", [])),
855 (Specify.prep_pbt thy "pbl_equ_univ_poly_deg0" [] e_pblID
856 (["degree_0","polynomial","univariate","equation"],
857 [("#Given" ,["equality e_e","solveFor v_v"]),
858 ("#Where" ,["matches (?a = 0) e_e",
859 "(lhs e_e) is_poly_in v_v",
860 "((lhs e_e) has_degree_in v_v ) = 0"]),
861 ("#Find" ,["solutions v_v'i'"])],
862 PolyEq_prls, SOME "solve (e_e::bool, v_v)", [["PolyEq","solve_d0_polyeq_equation"]])),
864 (Specify.prep_pbt thy "pbl_equ_univ_poly_deg1" [] e_pblID
865 (["degree_1","polynomial","univariate","equation"],
866 [("#Given" ,["equality e_e","solveFor v_v"]),
867 ("#Where" ,["matches (?a = 0) e_e",
868 "(lhs e_e) is_poly_in v_v",
869 "((lhs e_e) has_degree_in v_v ) = 1"]),
870 ("#Find" ,["solutions v_v'i'"])],
871 PolyEq_prls, SOME "solve (e_e::bool, v_v)", [["PolyEq","solve_d1_polyeq_equation"]])),
873 (Specify.prep_pbt thy "pbl_equ_univ_poly_deg2" [] e_pblID
874 (["degree_2","polynomial","univariate","equation"],
875 [("#Given" ,["equality e_e","solveFor v_v"]),
876 ("#Where" ,["matches (?a = 0) e_e",
877 "(lhs e_e) is_poly_in v_v ",
878 "((lhs e_e) has_degree_in v_v ) = 2"]),
879 ("#Find" ,["solutions v_v'i'"])],
880 PolyEq_prls, SOME "solve (e_e::bool, v_v)", [["PolyEq","solve_d2_polyeq_equation"]])),
881 (Specify.prep_pbt thy "pbl_equ_univ_poly_deg2_sqonly" [] e_pblID
882 (["sq_only","degree_2","polynomial","univariate","equation"],
883 [("#Given" ,["equality e_e","solveFor v_v"]),
884 ("#Where" ,["matches ( ?a + ?v_^^^2 = 0) e_e | " ^
885 "matches ( ?a + ?b*?v_^^^2 = 0) e_e | " ^
886 "matches ( ?v_^^^2 = 0) e_e | " ^
887 "matches ( ?b*?v_^^^2 = 0) e_e" ,
888 "Not (matches (?a + ?v_ + ?v_^^^2 = 0) e_e) &" ^
889 "Not (matches (?a + ?b*?v_ + ?v_^^^2 = 0) e_e) &" ^
890 "Not (matches (?a + ?v_ + ?c*?v_^^^2 = 0) e_e) &" ^
891 "Not (matches (?a + ?b*?v_ + ?c*?v_^^^2 = 0) e_e) &" ^
892 "Not (matches ( ?v_ + ?v_^^^2 = 0) e_e) &" ^
893 "Not (matches ( ?b*?v_ + ?v_^^^2 = 0) e_e) &" ^
894 "Not (matches ( ?v_ + ?c*?v_^^^2 = 0) e_e) &" ^
895 "Not (matches ( ?b*?v_ + ?c*?v_^^^2 = 0) e_e)"]),
896 ("#Find" ,["solutions v_v'i'"])],
897 PolyEq_prls, SOME "solve (e_e::bool, v_v)",
898 [["PolyEq","solve_d2_polyeq_sqonly_equation"]])),
899 (Specify.prep_pbt thy "pbl_equ_univ_poly_deg2_bdvonly" [] e_pblID
900 (["bdv_only","degree_2","polynomial","univariate","equation"],
901 [("#Given", ["equality e_e","solveFor v_v"]),
902 ("#Where", ["matches (?a*?v_ + ?v_^^^2 = 0) e_e | " ^
903 "matches ( ?v_ + ?v_^^^2 = 0) e_e | " ^
904 "matches ( ?v_ + ?b*?v_^^^2 = 0) e_e | " ^
905 "matches (?a*?v_ + ?b*?v_^^^2 = 0) e_e | " ^
906 "matches ( ?v_^^^2 = 0) e_e | " ^
907 "matches ( ?b*?v_^^^2 = 0) e_e "]),
908 ("#Find", ["solutions v_v'i'"])],
909 PolyEq_prls, SOME "solve (e_e::bool, v_v)",
910 [["PolyEq","solve_d2_polyeq_bdvonly_equation"]])),
911 (Specify.prep_pbt thy "pbl_equ_univ_poly_deg2_pq" [] e_pblID
912 (["pqFormula","degree_2","polynomial","univariate","equation"],
913 [("#Given", ["equality e_e","solveFor v_v"]),
914 ("#Where", ["matches (?a + 1*?v_^^^2 = 0) e_e | " ^
915 "matches (?a + ?v_^^^2 = 0) e_e"]),
916 ("#Find", ["solutions v_v'i'"])],
917 PolyEq_prls, SOME "solve (e_e::bool, v_v)", [["PolyEq","solve_d2_polyeq_pq_equation"]])),
918 (Specify.prep_pbt thy "pbl_equ_univ_poly_deg2_abc" [] e_pblID
919 (["abcFormula","degree_2","polynomial","univariate","equation"],
920 [("#Given", ["equality e_e","solveFor v_v"]),
921 ("#Where", ["matches (?a + ?v_^^^2 = 0) e_e | " ^
922 "matches (?a + ?b*?v_^^^2 = 0) e_e"]),
923 ("#Find", ["solutions v_v'i'"])],
924 PolyEq_prls, SOME "solve (e_e::bool, v_v)", [["PolyEq","solve_d2_polyeq_abc_equation"]])),
926 (Specify.prep_pbt thy "pbl_equ_univ_poly_deg3" [] e_pblID
927 (["degree_3","polynomial","univariate","equation"],
928 [("#Given", ["equality e_e","solveFor v_v"]),
929 ("#Where", ["matches (?a = 0) e_e",
930 "(lhs e_e) is_poly_in v_v ",
931 "((lhs e_e) has_degree_in v_v) = 3"]),
932 ("#Find", ["solutions v_v'i'"])],
933 PolyEq_prls, SOME "solve (e_e::bool, v_v)", [["PolyEq","solve_d3_polyeq_equation"]])),
935 (Specify.prep_pbt thy "pbl_equ_univ_poly_deg4" [] e_pblID
936 (["degree_4","polynomial","univariate","equation"],
937 [("#Given", ["equality e_e","solveFor v_v"]),
938 ("#Where", ["matches (?a = 0) e_e",
939 "(lhs e_e) is_poly_in v_v ",
940 "((lhs e_e) has_degree_in v_v) = 4"]),
941 ("#Find", ["solutions v_v'i'"])],
942 PolyEq_prls, SOME "solve (e_e::bool, v_v)", [(*["PolyEq","solve_d4_polyeq_equation"]*)])),
943 (*--- normalize ---*)
944 (Specify.prep_pbt thy "pbl_equ_univ_poly_norm" [] e_pblID
945 (["normalize","polynomial","univariate","equation"],
946 [("#Given", ["equality e_e","solveFor v_v"]),
947 ("#Where", ["(Not((matches (?a = 0 ) e_e ))) |" ^
948 "(Not(((lhs e_e) is_poly_in v_v)))"]),
949 ("#Find", ["solutions v_v'i'"])],
950 PolyEq_prls, SOME "solve (e_e::bool, v_v)", [["PolyEq","normalize_poly"]])),
951 (*-------------------------expanded-----------------------*)
952 (Specify.prep_pbt thy "pbl_equ_univ_expand" [] e_pblID
953 (["expanded","univariate","equation"],
954 [("#Given", ["equality e_e","solveFor v_v"]),
955 ("#Where", ["matches (?a = 0) e_e",
956 "(lhs e_e) is_expanded_in v_v "]),
957 ("#Find", ["solutions v_v'i'"])],
958 PolyEq_prls, SOME "solve (e_e::bool, v_v)", [])),
960 (Specify.prep_pbt thy "pbl_equ_univ_expand_deg2" [] e_pblID
961 (["degree_2","expanded","univariate","equation"],
962 [("#Given", ["equality e_e","solveFor v_v"]),
963 ("#Where", ["((lhs e_e) has_degree_in v_v) = 2"]),
964 ("#Find", ["solutions v_v'i'"])],
965 PolyEq_prls, SOME "solve (e_e::bool, v_v)", [["PolyEq","complete_square"]]))] *}
969 "Script Normalize_poly (e_e::bool) (v_v::real) = " ^
970 "(let e_e =((Try (Rewrite all_left False)) @@ " ^
971 " (Try (Repeat (Rewrite makex1_x False))) @@ " ^
972 " (Try (Repeat (Rewrite_Set expand_binoms False))) @@ " ^
973 " (Try (Repeat (Rewrite_Set_Inst [(bdv,v_v::real)] " ^
974 " make_ratpoly_in False))) @@ " ^
975 " (Try (Repeat (Rewrite_Set polyeq_simplify False)))) e_e " ^
976 " in (SubProblem (PolyEq',[polynomial,univariate,equation], [no_met]) " ^
977 " [BOOL e_e, REAL v_v]))";
981 text {* "-------------------------methods-----------------------" *}
982 setup {* KEStore_Elems.add_mets
983 [Specify.prep_met thy "met_polyeq" [] e_metID
985 {rew_ord'="tless_true",rls'=Atools_erls,calc = [], srls = e_rls, prls=e_rls,
986 crls=PolyEq_crls, errpats = [], nrls = norm_Rational},
988 Specify.prep_met thy "met_polyeq_norm" [] e_metID
989 (["PolyEq","normalize_poly"],
990 [("#Given" ,["equality e_e","solveFor v_v"]),
991 ("#Where" ,["(Not((matches (?a = 0 ) e_e ))) |(Not(((lhs e_e) is_poly_in v_v)))"]),
992 ("#Find" ,["solutions v_v'i'"])],
993 {rew_ord'="termlessI", rls'=PolyEq_erls, srls=e_rls, prls=PolyEq_prls, calc=[],
994 crls=PolyEq_crls, errpats = [], nrls = norm_Rational},
995 "Script Normalize_poly (e_e::bool) (v_v::real) = " ^
996 "(let e_e =((Try (Rewrite all_left False)) @@ " ^
997 " (Try (Repeat (Rewrite makex1_x False))) @@ " ^
998 " (Try (Repeat (Rewrite_Set expand_binoms False))) @@ " ^
999 " (Try (Repeat (Rewrite_Set_Inst [(bdv,v_v::real)] " ^
1000 " make_ratpoly_in False))) @@ " ^
1001 " (Try (Repeat (Rewrite_Set polyeq_simplify False)))) e_e " ^
1002 " in (SubProblem (PolyEq',[polynomial,univariate,equation], [no_met]) " ^
1003 " [BOOL e_e, REAL v_v]))"),
1004 Specify.prep_met thy "met_polyeq_d0" [] e_metID
1005 (["PolyEq","solve_d0_polyeq_equation"],
1006 [("#Given" ,["equality e_e","solveFor v_v"]),
1007 ("#Where" ,["(lhs e_e) is_poly_in v_v ", "((lhs e_e) has_degree_in v_v) = 0"]),
1008 ("#Find" ,["solutions v_v'i'"])],
1009 {rew_ord'="termlessI", rls'=PolyEq_erls, srls=e_rls, prls=PolyEq_prls,
1010 calc=[("sqrt", ("NthRoot.sqrt", eval_sqrt "#sqrt_"))], crls=PolyEq_crls, errpats = [],
1011 nrls = norm_Rational},
1012 "Script Solve_d0_polyeq_equation (e_e::bool) (v_v::real) = " ^
1013 "(let e_e = ((Try (Rewrite_Set_Inst [(bdv,v_v::real)] " ^
1014 " d0_polyeq_simplify False))) e_e " ^
1015 " in ((Or_to_List e_e)::bool list))"),
1016 Specify.prep_met thy "met_polyeq_d1" [] e_metID
1017 (["PolyEq","solve_d1_polyeq_equation"],
1018 [("#Given" ,["equality e_e","solveFor v_v"]),
1019 ("#Where" ,["(lhs e_e) is_poly_in v_v ", "((lhs e_e) has_degree_in v_v) = 1"]),
1020 ("#Find" ,["solutions v_v'i'"])],
1021 {rew_ord'="termlessI", rls'=PolyEq_erls, srls=e_rls, prls=PolyEq_prls,
1022 calc=[("sqrt", ("NthRoot.sqrt", eval_sqrt "#sqrt_"))], crls=PolyEq_crls, errpats = [],
1023 nrls = norm_Rational},
1024 "Script Solve_d1_polyeq_equation (e_e::bool) (v_v::real) = " ^
1025 "(let e_e = ((Try (Rewrite_Set_Inst [(bdv,v_v::real)] " ^
1026 " d1_polyeq_simplify True)) @@ " ^
1027 " (Try (Rewrite_Set polyeq_simplify False)) @@ " ^
1028 " (Try (Rewrite_Set norm_Rational_parenthesized False))) e_e;" ^
1029 " (L_L::bool list) = ((Or_to_List e_e)::bool list) " ^
1030 " in Check_elementwise L_L {(v_v::real). Assumptions} )"),
1031 Specify.prep_met thy "met_polyeq_d22" [] e_metID
1032 (["PolyEq","solve_d2_polyeq_equation"],
1033 [("#Given" ,["equality e_e","solveFor v_v"]),
1034 ("#Where" ,["(lhs e_e) is_poly_in v_v ", "((lhs e_e) has_degree_in v_v) = 2"]),
1035 ("#Find" ,["solutions v_v'i'"])],
1036 {rew_ord'="termlessI", rls'=PolyEq_erls, srls=e_rls, prls=PolyEq_prls,
1037 calc=[("sqrt", ("NthRoot.sqrt", eval_sqrt "#sqrt_"))], crls=PolyEq_crls, errpats = [],
1038 nrls = norm_Rational},
1039 "Script Solve_d2_polyeq_equation (e_e::bool) (v_v::real) = " ^
1040 " (let e_e = ((Try (Rewrite_Set_Inst [(bdv,v_v::real)] " ^
1041 " d2_polyeq_simplify True)) @@ " ^
1042 " (Try (Rewrite_Set polyeq_simplify False)) @@ " ^
1043 " (Try (Rewrite_Set_Inst [(bdv,v_v::real)] " ^
1044 " d1_polyeq_simplify True)) @@ " ^
1045 " (Try (Rewrite_Set polyeq_simplify False)) @@ " ^
1046 " (Try (Rewrite_Set norm_Rational_parenthesized False))) e_e;" ^
1047 " (L_L::bool list) = ((Or_to_List e_e)::bool list) " ^
1048 " in Check_elementwise L_L {(v_v::real). Assumptions} )"),
1049 Specify.prep_met thy "met_polyeq_d2_bdvonly" [] e_metID
1050 (["PolyEq","solve_d2_polyeq_bdvonly_equation"],
1051 [("#Given" ,["equality e_e","solveFor v_v"]),
1052 ("#Where" ,["(lhs e_e) is_poly_in v_v ", "((lhs e_e) has_degree_in v_v) = 2"]),
1053 ("#Find" ,["solutions v_v'i'"])],
1054 {rew_ord'="termlessI", rls'=PolyEq_erls, srls=e_rls, prls=PolyEq_prls,
1055 calc=[("sqrt", ("NthRoot.sqrt", eval_sqrt "#sqrt_"))], crls=PolyEq_crls, errpats = [],
1056 nrls = norm_Rational},
1057 "Script Solve_d2_polyeq_bdvonly_equation (e_e::bool) (v_v::real) =" ^
1058 " (let e_e = ((Try (Rewrite_Set_Inst [(bdv,v_v::real)] " ^
1059 " d2_polyeq_bdv_only_simplify True)) @@ " ^
1060 " (Try (Rewrite_Set polyeq_simplify False)) @@ " ^
1061 " (Try (Rewrite_Set_Inst [(bdv,v_v::real)] " ^
1062 " d1_polyeq_simplify True)) @@ " ^
1063 " (Try (Rewrite_Set polyeq_simplify False)) @@ " ^
1064 " (Try (Rewrite_Set norm_Rational_parenthesized False))) e_e;" ^
1065 " (L_L::bool list) = ((Or_to_List e_e)::bool list) " ^
1066 " in Check_elementwise L_L {(v_v::real). Assumptions} )"),
1067 Specify.prep_met thy "met_polyeq_d2_sqonly" [] e_metID
1068 (["PolyEq","solve_d2_polyeq_sqonly_equation"],
1069 [("#Given" ,["equality e_e","solveFor v_v"]),
1070 ("#Where" ,["(lhs e_e) is_poly_in v_v ", "((lhs e_e) has_degree_in v_v) = 2"]),
1071 ("#Find" ,["solutions v_v'i'"])],
1072 {rew_ord'="termlessI", rls'=PolyEq_erls, srls=e_rls, prls=PolyEq_prls,
1073 calc=[("sqrt", ("NthRoot.sqrt", eval_sqrt "#sqrt_"))], crls=PolyEq_crls, errpats = [],
1074 nrls = norm_Rational},
1075 "Script Solve_d2_polyeq_sqonly_equation (e_e::bool) (v_v::real) =" ^
1076 " (let e_e = ((Try (Rewrite_Set_Inst [(bdv,v_v::real)] " ^
1077 " d2_polyeq_sq_only_simplify True)) @@ " ^
1078 " (Try (Rewrite_Set polyeq_simplify False)) @@ " ^
1079 " (Try (Rewrite_Set norm_Rational_parenthesized False))) e_e; " ^
1080 " (L_L::bool list) = ((Or_to_List e_e)::bool list) " ^
1081 " in Check_elementwise L_L {(v_v::real). Assumptions} )"),
1082 Specify.prep_met thy "met_polyeq_d2_pq" [] e_metID
1083 (["PolyEq","solve_d2_polyeq_pq_equation"],
1084 [("#Given" ,["equality e_e","solveFor v_v"]),
1085 ("#Where" ,["(lhs e_e) is_poly_in v_v ", "((lhs e_e) has_degree_in v_v) = 2"]),
1086 ("#Find" ,["solutions v_v'i'"])],
1087 {rew_ord'="termlessI", rls'=PolyEq_erls, srls=e_rls, prls=PolyEq_prls,
1088 calc=[("sqrt", ("NthRoot.sqrt", eval_sqrt "#sqrt_"))], crls=PolyEq_crls, errpats = [],
1089 nrls = norm_Rational},
1090 "Script Solve_d2_polyeq_pq_equation (e_e::bool) (v_v::real) = " ^
1091 " (let e_e = ((Try (Rewrite_Set_Inst [(bdv,v_v::real)] " ^
1092 " d2_polyeq_pqFormula_simplify True)) @@ " ^
1093 " (Try (Rewrite_Set polyeq_simplify False)) @@ " ^
1094 " (Try (Rewrite_Set norm_Rational_parenthesized False))) e_e;" ^
1095 " (L_L::bool list) = ((Or_to_List e_e)::bool list) " ^
1096 " in Check_elementwise L_L {(v_v::real). Assumptions} )"),
1097 Specify.prep_met thy "met_polyeq_d2_abc" [] e_metID
1098 (["PolyEq","solve_d2_polyeq_abc_equation"],
1099 [("#Given" ,["equality e_e","solveFor v_v"]),
1100 ("#Where" ,["(lhs e_e) is_poly_in v_v ", "((lhs e_e) has_degree_in v_v) = 2"]),
1101 ("#Find" ,["solutions v_v'i'"])],
1102 {rew_ord'="termlessI", rls'=PolyEq_erls,srls=e_rls, prls=PolyEq_prls,
1103 calc=[("sqrt", ("NthRoot.sqrt", eval_sqrt "#sqrt_"))], crls=PolyEq_crls, errpats = [],
1104 nrls = norm_Rational},
1105 "Script Solve_d2_polyeq_abc_equation (e_e::bool) (v_v::real) = " ^
1106 " (let e_e = ((Try (Rewrite_Set_Inst [(bdv,v_v::real)] " ^
1107 " d2_polyeq_abcFormula_simplify True)) @@ " ^
1108 " (Try (Rewrite_Set polyeq_simplify False)) @@ " ^
1109 " (Try (Rewrite_Set norm_Rational_parenthesized False))) e_e;" ^
1110 " (L_L::bool list) = ((Or_to_List e_e)::bool list) " ^
1111 " in Check_elementwise L_L {(v_v::real). Assumptions} )"),
1112 Specify.prep_met thy "met_polyeq_d3" [] e_metID
1113 (["PolyEq","solve_d3_polyeq_equation"],
1114 [("#Given" ,["equality e_e","solveFor v_v"]),
1115 ("#Where" ,["(lhs e_e) is_poly_in v_v ", "((lhs e_e) has_degree_in v_v) = 3"]),
1116 ("#Find" ,["solutions v_v'i'"])],
1117 {rew_ord'="termlessI", rls'=PolyEq_erls, srls=e_rls, prls=PolyEq_prls,
1118 calc=[("sqrt", ("NthRoot.sqrt", eval_sqrt "#sqrt_"))], crls=PolyEq_crls, errpats = [],
1119 nrls = norm_Rational},
1120 "Script Solve_d3_polyeq_equation (e_e::bool) (v_v::real) = " ^
1121 " (let e_e = ((Try (Rewrite_Set_Inst [(bdv,v_v::real)] " ^
1122 " d3_polyeq_simplify True)) @@ " ^
1123 " (Try (Rewrite_Set polyeq_simplify False)) @@ " ^
1124 " (Try (Rewrite_Set_Inst [(bdv,v_v::real)] " ^
1125 " d2_polyeq_simplify True)) @@ " ^
1126 " (Try (Rewrite_Set polyeq_simplify False)) @@ " ^
1127 " (Try (Rewrite_Set_Inst [(bdv,v_v::real)] " ^
1128 " d1_polyeq_simplify True)) @@ " ^
1129 " (Try (Rewrite_Set polyeq_simplify False)) @@ " ^
1130 " (Try (Rewrite_Set norm_Rational_parenthesized False))) e_e;" ^
1131 " (L_L::bool list) = ((Or_to_List e_e)::bool list) " ^
1132 " in Check_elementwise L_L {(v_v::real). Assumptions} )"),
1133 (*.solves all expanded (ie. normalized) terms of degree 2.*)
1134 (*Oct.02 restriction: 'eval_true 0 =< discriminant' ony for integer values
1135 by 'PolyEq_erls'; restricted until Float.thy is implemented*)
1136 Specify.prep_met thy "met_polyeq_complsq" [] e_metID
1137 (["PolyEq","complete_square"],
1138 [("#Given" ,["equality e_e","solveFor v_v"]),
1139 ("#Where" ,["matches (?a = 0) e_e", "((lhs e_e) has_degree_in v_v) = 2"]),
1140 ("#Find" ,["solutions v_v'i'"])],
1141 {rew_ord'="termlessI",rls'=PolyEq_erls,srls=e_rls,prls=PolyEq_prls,
1142 calc=[("sqrt", ("NthRoot.sqrt", eval_sqrt "#sqrt_"))], crls=PolyEq_crls, errpats = [],
1143 nrls = norm_Rational},
1144 "Script Complete_square (e_e::bool) (v_v::real) = " ^
1146 " ((Try (Rewrite_Set_Inst [(bdv,v_v)] cancel_leading_coeff True)) " ^
1147 " @@ (Try (Rewrite_Set_Inst [(bdv,v_v)] complete_square True)) " ^
1148 " @@ (Try (Rewrite square_explicit1 False)) " ^
1149 " @@ (Try (Rewrite square_explicit2 False)) " ^
1150 " @@ (Rewrite root_plus_minus True) " ^
1151 " @@ (Try (Repeat (Rewrite_Inst [(bdv,v_v)] bdv_explicit1 False))) " ^
1152 " @@ (Try (Repeat (Rewrite_Inst [(bdv,v_v)] bdv_explicit2 False))) " ^
1153 " @@ (Try (Repeat " ^
1154 " (Rewrite_Inst [(bdv,v_v)] bdv_explicit3 False))) " ^
1155 " @@ (Try (Rewrite_Set calculate_RootRat False)) " ^
1156 " @@ (Try (Repeat (Calculate SQRT)))) e_e " ^
1157 " in ((Or_to_List e_e)::bool list))")]
1162 (* termorder hacked by MG *)
1163 local (*. for make_polynomial_in .*)
1165 open Term; (* for type order = EQUAL | LESS | GREATER *)
1167 fun pr_ord EQUAL = "EQUAL"
1168 | pr_ord LESS = "LESS"
1169 | pr_ord GREATER = "GREATER";
1171 fun dest_hd' x (Const (a, T)) = (((a, 0), T), 0)
1172 | dest_hd' x (t as Free (a, T)) =
1173 if x = t then ((("|||||||||||||", 0), T), 0) (*WN*)
1174 else (((a, 0), T), 1)
1175 | dest_hd' x (Var v) = (v, 2)
1176 | dest_hd' x (Bound i) = ((("", i), dummyT), 3)
1177 | dest_hd' x (Abs (_, T, _)) = ((("", 0), T), 4);
1179 fun size_of_term' x (Const ("Atools.pow",_) $ Free (var,_) $ Free (pot,_)) =
1182 (if xstr = var then 1000*(the (int_of_str pot)) else 3)
1183 | _ => error ("size_of_term' called with subst = "^
1185 | size_of_term' x (Free (subst,_)) =
1187 (Free (xstr,_)) => (if xstr = subst then 1000 else 1)
1188 | _ => error ("size_of_term' called with subst = "^
1190 | size_of_term' x (Abs (_,_,body)) = 1 + size_of_term' x body
1191 | size_of_term' x (f$t) = size_of_term' x f + size_of_term' x t
1192 | size_of_term' x _ = 1;
1194 fun term_ord' x pr thy (Abs (_, T, t), Abs(_, U, u)) = (* ~ term.ML *)
1195 (case term_ord' x pr thy (t, u) of EQUAL => Term_Ord.typ_ord (T, U) | ord => ord)
1196 | term_ord' x pr thy (t, u) =
1200 val (f, ts) = strip_comb t and (g, us) = strip_comb u;
1201 val _ = tracing ("t= f@ts= \"" ^ term_to_string''' thy f ^ "\" @ \"[" ^
1202 commas (map (term_to_string''' thy) ts) ^ "]\"");
1203 val _ = tracing ("u= g@us= \"" ^ term_to_string''' thy g ^ "\" @ \"[" ^
1204 commas(map (term_to_string''' thy) us) ^ "]\"");
1205 val _ = tracing ("size_of_term(t,u)= (" ^ string_of_int (size_of_term' x t) ^ ", " ^
1206 string_of_int (size_of_term' x u) ^ ")");
1207 val _ = tracing ("hd_ord(f,g) = " ^ (pr_ord o (hd_ord x)) (f,g));
1208 val _ = tracing ("terms_ord(ts,us) = " ^ (pr_ord o (terms_ord x) str false) (ts, us));
1209 val _ = tracing ("-------");
1212 case int_ord (size_of_term' x t, size_of_term' x u) of
1214 let val (f, ts) = strip_comb t and (g, us) = strip_comb u
1216 (case hd_ord x (f, g) of
1217 EQUAL => (terms_ord x str pr) (ts, us)
1221 and hd_ord x (f, g) = (* ~ term.ML *)
1222 prod_ord (prod_ord Term_Ord.indexname_ord Term_Ord.typ_ord)
1223 int_ord (dest_hd' x f, dest_hd' x g)
1224 and terms_ord x str pr (ts, us) =
1225 list_ord (term_ord' x pr (assoc_thy "Isac"))(ts, us);
1229 fun ord_make_polynomial_in (pr:bool) thy subst tu =
1231 (* val _=tracing("*** subs variable is: "^(subst2str subst)); *)
1234 (_,x)::_ => (term_ord' x pr thy tu = LESS)
1235 | _ => error ("ord_make_polynomial_in called with subst = "^
1242 val order_add_mult_in = prep_rls'(
1243 Rls{id = "order_add_mult_in", preconds = [],
1244 rew_ord = ("ord_make_polynomial_in",
1245 ord_make_polynomial_in false @{theory "Poly"}),
1246 erls = e_rls,srls = Erls,
1247 calc = [], errpatts = [],
1248 rules = [Thm ("mult_commute",num_str @{thm mult.commute}),
1250 Thm ("real_mult_left_commute",num_str @{thm real_mult_left_commute}),
1251 (*z1.0 * (z2.0 * z3.0) = z2.0 * (z1.0 * z3.0)*)
1252 Thm ("mult_assoc",num_str @{thm mult.assoc}),
1253 (*z1.0 * z2.0 * z3.0 = z1.0 * (z2.0 * z3.0)*)
1254 Thm ("add_commute",num_str @{thm add.commute}),
1256 Thm ("add_left_commute",num_str @{thm add.left_commute}),
1257 (*x + (y + z) = y + (x + z)*)
1258 Thm ("add_assoc",num_str @{thm add.assoc})
1259 (*z1.0 + z2.0 + z3.0 = z1.0 + (z2.0 + z3.0)*)
1260 ], scr = EmptyScr}:rls);
1264 val collect_bdv = prep_rls'(
1265 Rls{id = "collect_bdv", preconds = [],
1266 rew_ord = ("dummy_ord", dummy_ord),
1267 erls = e_rls,srls = Erls,
1268 calc = [], errpatts = [],
1269 rules = [Thm ("bdv_collect_1",num_str @{thm bdv_collect_1}),
1270 Thm ("bdv_collect_2",num_str @{thm bdv_collect_2}),
1271 Thm ("bdv_collect_3",num_str @{thm bdv_collect_3}),
1273 Thm ("bdv_collect_assoc1_1",num_str @{thm bdv_collect_assoc1_1}),
1274 Thm ("bdv_collect_assoc1_2",num_str @{thm bdv_collect_assoc1_2}),
1275 Thm ("bdv_collect_assoc1_3",num_str @{thm bdv_collect_assoc1_3}),
1277 Thm ("bdv_collect_assoc2_1",num_str @{thm bdv_collect_assoc2_1}),
1278 Thm ("bdv_collect_assoc2_2",num_str @{thm bdv_collect_assoc2_2}),
1279 Thm ("bdv_collect_assoc2_3",num_str @{thm bdv_collect_assoc2_3}),
1282 Thm ("bdv_n_collect_1",num_str @{thm bdv_n_collect_1}),
1283 Thm ("bdv_n_collect_2",num_str @{thm bdv_n_collect_2}),
1284 Thm ("bdv_n_collect_3",num_str @{thm bdv_n_collect_3}),
1286 Thm ("bdv_n_collect_assoc1_1",num_str @{thm bdv_n_collect_assoc1_1}),
1287 Thm ("bdv_n_collect_assoc1_2",num_str @{thm bdv_n_collect_assoc1_2}),
1288 Thm ("bdv_n_collect_assoc1_3",num_str @{thm bdv_n_collect_assoc1_3}),
1290 Thm ("bdv_n_collect_assoc2_1",num_str @{thm bdv_n_collect_assoc2_1}),
1291 Thm ("bdv_n_collect_assoc2_2",num_str @{thm bdv_n_collect_assoc2_2}),
1292 Thm ("bdv_n_collect_assoc2_3",num_str @{thm bdv_n_collect_assoc2_3})
1293 ], scr = EmptyScr}:rls);
1297 (*.transforms an arbitrary term without roots to a polynomial [4]
1298 according to knowledge/Poly.sml.*)
1299 val make_polynomial_in = prep_rls'(
1300 Seq {id = "make_polynomial_in", preconds = []:term list,
1301 rew_ord = ("dummy_ord", dummy_ord),
1302 erls = Atools_erls, srls = Erls,
1303 calc = [], errpatts = [],
1304 rules = [Rls_ expand_poly,
1305 Rls_ order_add_mult_in,
1306 Rls_ simplify_power,
1307 Rls_ collect_numerals,
1309 Thm ("realpow_oneI",num_str @{thm realpow_oneI}),
1310 Rls_ discard_parentheses,
1319 append_rls "separate_bdvs"
1321 [Thm ("separate_bdv", num_str @{thm separate_bdv}),
1322 (*"?a * ?bdv / ?b = ?a / ?b * ?bdv"*)
1323 Thm ("separate_bdv_n", num_str @{thm separate_bdv_n}),
1324 Thm ("separate_1_bdv", num_str @{thm separate_1_bdv}),
1325 (*"?bdv / ?b = (1 / ?b) * ?bdv"*)
1326 Thm ("separate_1_bdv_n", num_str @{thm separate_1_bdv_n}),
1327 (*"?bdv ^^^ ?n / ?b = 1 / ?b * ?bdv ^^^ ?n"*)
1328 Thm ("add_divide_distrib",
1329 num_str @{thm add_divide_distrib})
1330 (*"(?x + ?y) / ?z = ?x / ?z + ?y / ?z"
1331 WN051031 DOES NOT BELONG TO HERE*)
1335 val make_ratpoly_in = prep_rls'(
1336 Seq {id = "make_ratpoly_in", preconds = []:term list,
1337 rew_ord = ("dummy_ord", dummy_ord),
1338 erls = Atools_erls, srls = Erls,
1339 calc = [], errpatts = [],
1340 rules = [Rls_ norm_Rational,
1341 Rls_ order_add_mult_in,
1342 Rls_ discard_parentheses,
1344 (* Rls_ rearrange_assoc, WN060916 why does cancel_p not work?*)
1346 (*Calc ("Fields.inverse_class.divide" ,eval_cancel "#divide_e") too weak!*)
1348 scr = EmptyScr}:rls);
1350 setup {* KEStore_Elems.add_rlss
1351 [("order_add_mult_in", (Context.theory_name @{theory}, order_add_mult_in)),
1352 ("collect_bdv", (Context.theory_name @{theory}, collect_bdv)),
1353 ("make_polynomial_in", (Context.theory_name @{theory}, make_polynomial_in)),
1354 ("make_ratpoly_in", (Context.theory_name @{theory}, make_ratpoly_in)),
1355 ("separate_bdvs", (Context.theory_name @{theory}, separate_bdvs))] *}