230 Thm("d1_isolate_div",num_str d1_isolate_div) |
166 Thm("d1_isolate_div",num_str d1_isolate_div) |
231 (* bx=c -> x=c/b *) |
167 (* bx=c -> x=c/b *) |
232 ], |
168 ], |
233 scr = Script ((term_of o the o (parse thy)) "empty_script") |
169 scr = Script ((term_of o the o (parse thy)) "empty_script") |
234 }:rls); |
170 }:rls); |
|
171 |
235 (* -- d2 -- *) |
172 (* -- d2 -- *) |
236 (*isolate the bound variable in an d2 equation with bdv only; 'bdv' is a meta-constant*) |
173 (* isolate the bound variable in an d2 equation with bdv only; |
|
174 'bdv' is a meta-constant*) |
237 val d2_polyeq_bdv_only_simplify = prep_rls( |
175 val d2_polyeq_bdv_only_simplify = prep_rls( |
238 Rls {id = "d2_polyeq_bdv_only_simplify", preconds = [], |
176 Rls {id = "d2_polyeq_bdv_only_simplify", preconds = [], |
239 rew_ord = ("e_rew_ord",e_rew_ord), |
177 rew_ord = ("e_rew_ord",e_rew_ord), |
240 erls = PolyEq_erls, |
178 erls = PolyEq_erls, |
241 srls = Erls, |
179 srls = Erls, |
242 calc = [], |
180 calc = [], |
243 (*asm_thm = [("d2_sqrt_equation1",""),("d2_sqrt_equation1_neg",""), |
181 (*asm_thm = [("d2_sqrt_equation1",""),("d2_sqrt_equation1_neg",""), |
244 ("d2_isolate_div","")],*) |
182 ("d2_isolate_div","")],*) |
245 rules = [ |
183 rules = [Thm("d2_prescind1",num_str d2_prescind1), |
246 Thm("d2_prescind1",num_str d2_prescind1), (* ax+bx^2=0 -> x(a+bx)=0 *) |
184 (* ax+bx^2=0 -> x(a+bx)=0 *) |
247 Thm("d2_prescind2",num_str d2_prescind2), (* ax+ x^2=0 -> x(a+ x)=0 *) |
185 Thm("d2_prescind2",num_str d2_prescind2), |
248 Thm("d2_prescind3",num_str d2_prescind3), (* x+bx^2=0 -> x(1+bx)=0 *) |
186 (* ax+ x^2=0 -> x(a+ x)=0 *) |
249 Thm("d2_prescind4",num_str d2_prescind4), (* x+ x^2=0 -> x(1+ x)=0 *) |
187 Thm("d2_prescind3",num_str d2_prescind3), |
250 Thm("d2_sqrt_equation1",num_str d2_sqrt_equation1), (* x^2=c -> x=+-sqrt(c)*) |
188 (* x+bx^2=0 -> x(1+bx)=0 *) |
251 Thm("d2_sqrt_equation1_neg",num_str d2_sqrt_equation1_neg), (* [0<c] x^2=c -> [] *) |
189 Thm("d2_prescind4",num_str d2_prescind4), |
252 Thm("d2_sqrt_equation2",num_str d2_sqrt_equation2), (* x^2=0 -> x=0 *) |
190 (* x+ x^2=0 -> x(1+ x)=0 *) |
253 Thm("d2_reduce_equation1",num_str d2_reduce_equation1),(* x(a+bx)=0 -> x=0 | a+bx=0*) |
191 Thm("d2_sqrt_equation1",num_str d2_sqrt_equation1), |
254 Thm("d2_reduce_equation2",num_str d2_reduce_equation2),(* x(a+ x)=0 -> x=0 | a+ x=0*) |
192 (* x^2=c -> x=+-sqrt(c)*) |
255 Thm("d2_isolate_div",num_str d2_isolate_div) (* bx^2=c -> x^2=c/b*) |
193 Thm("d2_sqrt_equation1_neg",num_str d2_sqrt_equation1_neg), |
|
194 (* [0<c] x^2=c -> [] *) |
|
195 Thm("d2_sqrt_equation2",num_str d2_sqrt_equation2), |
|
196 (* x^2=0 -> x=0 *) |
|
197 Thm("d2_reduce_equation1",num_str d2_reduce_equation1), |
|
198 (* x(a+bx)=0 -> x=0 | a+bx=0*) |
|
199 Thm("d2_reduce_equation2",num_str d2_reduce_equation2), |
|
200 (* x(a+ x)=0 -> x=0 | a+ x=0*) |
|
201 Thm("d2_isolate_div",num_str d2_isolate_div) |
|
202 (* bx^2=c -> x^2=c/b*) |
256 ], |
203 ], |
257 scr = Script ((term_of o the o (parse thy)) "empty_script") |
204 scr = Script ((term_of o the o (parse thy)) "empty_script") |
258 }:rls); |
205 }:rls); |
259 (*isolate the bound variable in an d2 equation with sqrt only; 'bdv' is a meta-constant*) |
206 |
|
207 (* isolate the bound variable in an d2 equation with sqrt only; |
|
208 'bdv' is a meta-constant*) |
260 val d2_polyeq_sq_only_simplify = prep_rls( |
209 val d2_polyeq_sq_only_simplify = prep_rls( |
261 Rls {id = "d2_polyeq_sq_only_simplify", preconds = [], |
210 Rls {id = "d2_polyeq_sq_only_simplify", preconds = [], |
262 rew_ord = ("e_rew_ord",e_rew_ord), |
211 rew_ord = ("e_rew_ord",e_rew_ord), |
263 erls = PolyEq_erls, |
212 erls = PolyEq_erls, |
264 srls = Erls, |
213 srls = Erls, |
265 calc = [], |
214 calc = [], |
266 (*asm_thm = [("d2_sqrt_equation1",""),("d2_sqrt_equation1_neg",""), |
215 (*asm_thm = [("d2_sqrt_equation1",""),("d2_sqrt_equation1_neg",""), |
267 ("d2_isolate_div","")],*) |
216 ("d2_isolate_div","")],*) |
268 rules = [ |
217 rules = [Thm("d2_isolate_add1",num_str d2_isolate_add1), |
269 Thm("d2_isolate_add1",num_str d2_isolate_add1), (* a+ bx^2=0 -> bx^2=(-1)a*) |
218 (* a+ bx^2=0 -> bx^2=(-1)a*) |
270 Thm("d2_isolate_add2",num_str d2_isolate_add2), (* a+ x^2=0 -> x^2=(-1)a*) |
219 Thm("d2_isolate_add2",num_str d2_isolate_add2), |
271 Thm("d2_sqrt_equation2",num_str d2_sqrt_equation2), (* x^2=0 -> x=0 *) |
220 (* a+ x^2=0 -> x^2=(-1)a*) |
272 Thm("d2_sqrt_equation1",num_str d2_sqrt_equation1), (* x^2=c -> x=+-sqrt(c)*) |
221 Thm("d2_sqrt_equation2",num_str d2_sqrt_equation2), |
273 Thm("d2_sqrt_equation1_neg",num_str d2_sqrt_equation1_neg),(* [c<0] x^2=c -> x=[] *) |
222 (* x^2=0 -> x=0 *) |
274 Thm("d2_isolate_div",num_str d2_isolate_div) (* bx^2=c -> x^2=c/b*) |
223 Thm("d2_sqrt_equation1",num_str d2_sqrt_equation1), |
|
224 (* x^2=c -> x=+-sqrt(c)*) |
|
225 Thm("d2_sqrt_equation1_neg",num_str d2_sqrt_equation1_neg), |
|
226 (* [c<0] x^2=c -> x=[] *) |
|
227 Thm("d2_isolate_div",num_str d2_isolate_div) |
|
228 (* bx^2=c -> x^2=c/b*) |
275 ], |
229 ], |
276 scr = Script ((term_of o the o (parse thy)) "empty_script") |
230 scr = Script ((term_of o the o (parse thy)) "empty_script") |
277 }:rls); |
231 }:rls); |
278 (*isolate the bound variable in an d2 equation with pqFormula; 'bdv' is a meta-constant*) |
232 |
|
233 (* isolate the bound variable in an d2 equation with pqFormula; |
|
234 'bdv' is a meta-constant*) |
279 val d2_polyeq_pqFormula_simplify = prep_rls( |
235 val d2_polyeq_pqFormula_simplify = prep_rls( |
280 Rls {id = "d2_polyeq_pqFormula_simplify", preconds = [], |
236 Rls {id = "d2_polyeq_pqFormula_simplify", preconds = [], |
281 rew_ord = ("e_rew_ord",e_rew_ord), |
237 rew_ord = ("e_rew_ord",e_rew_ord), erls = PolyEq_erls, |
282 erls = PolyEq_erls, |
238 srls = Erls, calc = [], |
283 srls = Erls, |
239 rules = [Thm("d2_pqformula1",num_str d2_pqformula1), |
284 calc = [], |
240 (* q+px+ x^2=0 *) |
285 (*asm_thm = [("d2_pqformula1",""),("d2_pqformula2",""),("d2_pqformula3",""),("d2_pqformula4",""), |
241 Thm("d2_pqformula1_neg",num_str d2_pqformula1_neg), |
286 ("d2_pqformula5",""),("d2_pqformula6",""),("d2_pqformula7",""),("d2_pqformula8",""), |
242 (* q+px+ x^2=0 *) |
287 ("d2_pqformula9",""),("d2_pqformula10",""), |
243 Thm("d2_pqformula2",num_str d2_pqformula2), |
288 ("d2_pqformula1_neg",""),("d2_pqformula2_neg",""),("d2_pqformula3_neg",""), |
244 (* q+px+1x^2=0 *) |
289 ("d2_pqformula4_neg",""),("d2_pqformula9_neg",""),("d2_pqformula10_neg","")],*) |
245 Thm("d2_pqformula2_neg",num_str d2_pqformula2_neg), |
290 rules = [ |
246 (* q+px+1x^2=0 *) |
291 Thm("d2_pqformula1",num_str d2_pqformula1), (* q+px+ x^2=0 *) |
247 Thm("d2_pqformula3",num_str d2_pqformula3), |
292 Thm("d2_pqformula1_neg",num_str d2_pqformula1_neg), (* q+px+ x^2=0 *) |
248 (* q+ x+ x^2=0 *) |
293 Thm("d2_pqformula2",num_str d2_pqformula2), (* q+px+1x^2=0 *) |
249 Thm("d2_pqformula3_neg",num_str d2_pqformula3_neg), |
294 Thm("d2_pqformula2_neg",num_str d2_pqformula2_neg), (* q+px+1x^2=0 *) |
250 (* q+ x+ x^2=0 *) |
295 Thm("d2_pqformula3",num_str d2_pqformula3), (* q+ x+ x^2=0 *) |
251 Thm("d2_pqformula4",num_str d2_pqformula4), |
296 Thm("d2_pqformula3_neg",num_str d2_pqformula3_neg), (* q+ x+ x^2=0 *) |
252 (* q+ x+1x^2=0 *) |
297 Thm("d2_pqformula4",num_str d2_pqformula4), (* q+ x+1x^2=0 *) |
253 Thm("d2_pqformula4_neg",num_str d2_pqformula4_neg), |
298 Thm("d2_pqformula4_neg",num_str d2_pqformula4_neg), (* q+ x+1x^2=0 *) |
254 (* q+ x+1x^2=0 *) |
299 Thm("d2_pqformula5",num_str d2_pqformula5), (* qx+ x^2=0 *) |
255 Thm("d2_pqformula5",num_str d2_pqformula5), |
300 Thm("d2_pqformula6",num_str d2_pqformula6), (* qx+1x^2=0 *) |
256 (* qx+ x^2=0 *) |
301 Thm("d2_pqformula7",num_str d2_pqformula7), (* x+ x^2=0 *) |
257 Thm("d2_pqformula6",num_str d2_pqformula6), |
302 Thm("d2_pqformula8",num_str d2_pqformula8), (* x+1x^2=0 *) |
258 (* qx+1x^2=0 *) |
303 Thm("d2_pqformula9",num_str d2_pqformula9), (* q +1x^2=0 *) |
259 Thm("d2_pqformula7",num_str d2_pqformula7), |
304 Thm("d2_pqformula9_neg",num_str d2_pqformula9_neg), (* q +1x^2=0 *) |
260 (* x+ x^2=0 *) |
305 Thm("d2_pqformula10",num_str d2_pqformula10), (* q + x^2=0 *) |
261 Thm("d2_pqformula8",num_str d2_pqformula8), |
306 Thm("d2_pqformula10_neg",num_str d2_pqformula10_neg), (* q + x^2=0 *) |
262 (* x+1x^2=0 *) |
307 Thm("d2_sqrt_equation2",num_str d2_sqrt_equation2), (* x^2=0 *) |
263 Thm("d2_pqformula9",num_str d2_pqformula9), |
308 Thm("d2_sqrt_equation3",num_str d2_sqrt_equation3) (* 1x^2=0 *) |
264 (* q +1x^2=0 *) |
309 ], |
265 Thm("d2_pqformula9_neg",num_str d2_pqformula9_neg), |
|
266 (* q +1x^2=0 *) |
|
267 Thm("d2_pqformula10",num_str d2_pqformula10), |
|
268 (* q + x^2=0 *) |
|
269 Thm("d2_pqformula10_neg",num_str d2_pqformula10_neg), |
|
270 (* q + x^2=0 *) |
|
271 Thm("d2_sqrt_equation2",num_str d2_sqrt_equation2), |
|
272 (* x^2=0 *) |
|
273 Thm("d2_sqrt_equation3",num_str d2_sqrt_equation3) |
|
274 (* 1x^2=0 *) |
|
275 ], |
310 scr = Script ((term_of o the o (parse thy)) "empty_script") |
276 scr = Script ((term_of o the o (parse thy)) "empty_script") |
311 }:rls); |
277 }:rls); |
312 (*isolate the bound variable in an d2 equation with abcFormula; 'bdv' is a meta-constant*) |
278 |
|
279 (* isolate the bound variable in an d2 equation with abcFormula; |
|
280 'bdv' is a meta-constant*) |
313 val d2_polyeq_abcFormula_simplify = prep_rls( |
281 val d2_polyeq_abcFormula_simplify = prep_rls( |
314 Rls {id = "d2_polyeq_abcFormula_simplify", preconds = [], |
282 Rls {id = "d2_polyeq_abcFormula_simplify", preconds = [], |
315 rew_ord = ("e_rew_ord",e_rew_ord), |
283 rew_ord = ("e_rew_ord",e_rew_ord), erls = PolyEq_erls, |
316 erls = PolyEq_erls, |
284 srls = Erls, calc = [], |
317 srls = Erls, |
285 rules = [Thm("d2_abcformula1",num_str d2_abcformula1), |
318 calc = [], |
286 (*c+bx+cx^2=0 *) |
319 (*asm_thm = [("d2_abcformula1",""),("d2_abcformula2",""),("d2_abcformula3",""), |
287 Thm("d2_abcformula1_neg",num_str d2_abcformula1_neg), |
320 ("d2_abcformula4",""),("d2_abcformula5",""),("d2_abcformula6",""), |
288 (*c+bx+cx^2=0 *) |
321 ("d2_abcformula7",""),("d2_abcformula8",""),("d2_abcformula9",""), |
289 Thm("d2_abcformula2",num_str d2_abcformula2), |
322 ("d2_abcformula10",""),("d2_abcformula1_neg",""),("d2_abcformula2_neg",""), |
290 (*c+ x+cx^2=0 *) |
323 ("d2_abcformula3_neg",""),("d2_abcformula4_neg",""),("d2_abcformula5_neg",""), |
291 Thm("d2_abcformula2_neg",num_str d2_abcformula2_neg), |
324 ("d2_abcformula6_neg","")],*) |
292 (*c+ x+cx^2=0 *) |
325 rules = [ |
293 Thm("d2_abcformula3",num_str d2_abcformula3), |
326 Thm("d2_abcformula1",num_str d2_abcformula1), (*c+bx+cx^2=0 *) |
294 (*c+bx+ x^2=0 *) |
327 Thm("d2_abcformula1_neg",num_str d2_abcformula1_neg), (*c+bx+cx^2=0 *) |
295 Thm("d2_abcformula3_neg",num_str d2_abcformula3_neg), |
328 Thm("d2_abcformula2",num_str d2_abcformula2), (*c+ x+cx^2=0 *) |
296 (*c+bx+ x^2=0 *) |
329 Thm("d2_abcformula2_neg",num_str d2_abcformula2_neg), (*c+ x+cx^2=0 *) |
297 Thm("d2_abcformula4",num_str d2_abcformula4), |
330 Thm("d2_abcformula3",num_str d2_abcformula3), (*c+bx+ x^2=0 *) |
298 (*c+ x+ x^2=0 *) |
331 Thm("d2_abcformula3_neg",num_str d2_abcformula3_neg), (*c+bx+ x^2=0 *) |
299 Thm("d2_abcformula4_neg",num_str d2_abcformula4_neg), |
332 Thm("d2_abcformula4",num_str d2_abcformula4), (*c+ x+ x^2=0 *) |
300 (*c+ x+ x^2=0 *) |
333 Thm("d2_abcformula4_neg",num_str d2_abcformula4_neg), (*c+ x+ x^2=0 *) |
301 Thm("d2_abcformula5",num_str d2_abcformula5), |
334 Thm("d2_abcformula5",num_str d2_abcformula5), (*c+ cx^2=0 *) |
302 (*c+ cx^2=0 *) |
335 Thm("d2_abcformula5_neg",num_str d2_abcformula5_neg), (*c+ cx^2=0 *) |
303 Thm("d2_abcformula5_neg",num_str d2_abcformula5_neg), |
336 Thm("d2_abcformula6",num_str d2_abcformula6), (*c+ x^2=0 *) |
304 (*c+ cx^2=0 *) |
337 Thm("d2_abcformula6_neg",num_str d2_abcformula6_neg), (*c+ x^2=0 *) |
305 Thm("d2_abcformula6",num_str d2_abcformula6), |
338 Thm("d2_abcformula7",num_str d2_abcformula7), (* bx+ax^2=0 *) |
306 (*c+ x^2=0 *) |
339 Thm("d2_abcformula8",num_str d2_abcformula8), (* bx+ x^2=0 *) |
307 Thm("d2_abcformula6_neg",num_str d2_abcformula6_neg), |
340 Thm("d2_abcformula9",num_str d2_abcformula9), (* x+ax^2=0 *) |
308 (*c+ x^2=0 *) |
341 Thm("d2_abcformula10",num_str d2_abcformula10), (* x+ x^2=0 *) |
309 Thm("d2_abcformula7",num_str d2_abcformula7), |
342 Thm("d2_sqrt_equation2",num_str d2_sqrt_equation2), (* x^2=0 *) |
310 (* bx+ax^2=0 *) |
343 Thm("d2_sqrt_equation3",num_str d2_sqrt_equation3) (* bx^2=0 *) |
311 Thm("d2_abcformula8",num_str d2_abcformula8), |
344 ], |
312 (* bx+ x^2=0 *) |
|
313 Thm("d2_abcformula9",num_str d2_abcformula9), |
|
314 (* x+ax^2=0 *) |
|
315 Thm("d2_abcformula10",num_str d2_abcformula10), |
|
316 (* x+ x^2=0 *) |
|
317 Thm("d2_sqrt_equation2",num_str d2_sqrt_equation2), |
|
318 (* x^2=0 *) |
|
319 Thm("d2_sqrt_equation3",num_str d2_sqrt_equation3) |
|
320 (* bx^2=0 *) |
|
321 ], |
345 scr = Script ((term_of o the o (parse thy)) "empty_script") |
322 scr = Script ((term_of o the o (parse thy)) "empty_script") |
346 }:rls); |
323 }:rls); |
347 (*isolate the bound variable in an d2 equation; 'bdv' is a meta-constant*) |
324 |
|
325 (* isolate the bound variable in an d2 equation; |
|
326 'bdv' is a meta-constant*) |
348 val d2_polyeq_simplify = prep_rls( |
327 val d2_polyeq_simplify = prep_rls( |
349 Rls {id = "d2_polyeq_simplify", preconds = [], |
328 Rls {id = "d2_polyeq_simplify", preconds = [], |
350 rew_ord = ("e_rew_ord",e_rew_ord), |
329 rew_ord = ("e_rew_ord",e_rew_ord), erls = PolyEq_erls, |
351 erls = PolyEq_erls, |
330 srls = Erls, calc = [], |
352 srls = Erls, |
331 rules = [Thm("d2_pqformula1",num_str d2_pqformula1), |
353 calc = [], |
332 (* p+qx+ x^2=0 *) |
354 (*asm_thm = [("d2_pqformula1",""),("d2_pqformula2",""),("d2_pqformula3",""),("d2_pqformula4",""), |
333 Thm("d2_pqformula1_neg",num_str d2_pqformula1_neg), |
355 ("d2_pqformula1_neg",""),("d2_pqformula2_neg",""),("d2_pqformula3_neg",""), |
334 (* p+qx+ x^2=0 *) |
356 ("d2_pqformula4_neg",""), |
335 Thm("d2_pqformula2",num_str d2_pqformula2), |
357 ("d2_abcformula1",""),("d2_abcformula2",""),("d2_abcformula1_neg",""), |
336 (* p+qx+1x^2=0 *) |
358 ("d2_abcformula2_neg",""), ("d2_sqrt_equation1",""), |
337 Thm("d2_pqformula2_neg",num_str d2_pqformula2_neg), |
359 ("d2_sqrt_equation1_neg",""),("d2_isolate_div","")],*) |
338 (* p+qx+1x^2=0 *) |
360 rules = [ |
339 Thm("d2_pqformula3",num_str d2_pqformula3), |
361 Thm("d2_pqformula1",num_str d2_pqformula1), (* p+qx+ x^2=0 *) |
340 (* p+ x+ x^2=0 *) |
362 Thm("d2_pqformula1_neg",num_str d2_pqformula1_neg), (* p+qx+ x^2=0 *) |
341 Thm("d2_pqformula3_neg",num_str d2_pqformula3_neg), |
363 Thm("d2_pqformula2",num_str d2_pqformula2), (* p+qx+1x^2=0 *) |
342 (* p+ x+ x^2=0 *) |
364 Thm("d2_pqformula2_neg",num_str d2_pqformula2_neg), (* p+qx+1x^2=0 *) |
343 Thm("d2_pqformula4",num_str d2_pqformula4), |
365 Thm("d2_pqformula3",num_str d2_pqformula3), (* p+ x+ x^2=0 *) |
344 (* p+ x+1x^2=0 *) |
366 Thm("d2_pqformula3_neg",num_str d2_pqformula3_neg), (* p+ x+ x^2=0 *) |
345 Thm("d2_pqformula4_neg",num_str d2_pqformula4_neg), |
367 Thm("d2_pqformula4",num_str d2_pqformula4), (* p+ x+1x^2=0 *) |
346 (* p+ x+1x^2=0 *) |
368 Thm("d2_pqformula4_neg",num_str d2_pqformula4_neg), (* p+ x+1x^2=0 *) |
347 Thm("d2_abcformula1",num_str d2_abcformula1), |
369 Thm("d2_abcformula1",num_str d2_abcformula1), (* c+bx+cx^2=0 *) |
348 (* c+bx+cx^2=0 *) |
370 Thm("d2_abcformula1_neg",num_str d2_abcformula1_neg), (* c+bx+cx^2=0 *) |
349 Thm("d2_abcformula1_neg",num_str d2_abcformula1_neg), |
371 Thm("d2_abcformula2",num_str d2_abcformula2), (* c+ x+cx^2=0 *) |
350 (* c+bx+cx^2=0 *) |
372 Thm("d2_abcformula2_neg",num_str d2_abcformula2_neg), (* c+ x+cx^2=0 *) |
351 Thm("d2_abcformula2",num_str d2_abcformula2), |
373 Thm("d2_prescind1",num_str d2_prescind1), (* ax+bx^2=0 -> x(a+bx)=0 *) |
352 (* c+ x+cx^2=0 *) |
374 Thm("d2_prescind2",num_str d2_prescind2), (* ax+ x^2=0 -> x(a+ x)=0 *) |
353 Thm("d2_abcformula2_neg",num_str d2_abcformula2_neg), |
375 Thm("d2_prescind3",num_str d2_prescind3), (* x+bx^2=0 -> x(1+bx)=0 *) |
354 (* c+ x+cx^2=0 *) |
376 Thm("d2_prescind4",num_str d2_prescind4), (* x+ x^2=0 -> x(1+ x)=0 *) |
355 Thm("d2_prescind1",num_str d2_prescind1), |
377 Thm("d2_isolate_add1",num_str d2_isolate_add1), (* a+ bx^2=0 -> bx^2=(-1)a*) |
356 (* ax+bx^2=0 -> x(a+bx)=0 *) |
378 Thm("d2_isolate_add2",num_str d2_isolate_add2), (* a+ x^2=0 -> x^2=(-1)a*) |
357 Thm("d2_prescind2",num_str d2_prescind2), |
379 Thm("d2_sqrt_equation1",num_str d2_sqrt_equation1), (* x^2=c -> x=+-sqrt(c)*) |
358 (* ax+ x^2=0 -> x(a+ x)=0 *) |
380 Thm("d2_sqrt_equation1_neg",num_str d2_sqrt_equation1_neg),(* [c<0] x^2=c -> x=[]*) |
359 Thm("d2_prescind3",num_str d2_prescind3), |
381 Thm("d2_sqrt_equation2",num_str d2_sqrt_equation2), (* x^2=0 -> x=0 *) |
360 (* x+bx^2=0 -> x(1+bx)=0 *) |
382 Thm("d2_reduce_equation1",num_str d2_reduce_equation1),(* x(a+bx)=0 -> x=0 | a+bx=0*) |
361 Thm("d2_prescind4",num_str d2_prescind4), |
383 Thm("d2_reduce_equation2",num_str d2_reduce_equation2),(* x(a+ x)=0 -> x=0 | a+ x=0*) |
362 (* x+ x^2=0 -> x(1+ x)=0 *) |
384 Thm("d2_isolate_div",num_str d2_isolate_div) (* bx^2=c -> x^2=c/b*) |
363 Thm("d2_isolate_add1",num_str d2_isolate_add1), |
385 ], |
364 (* a+ bx^2=0 -> bx^2=(-1)a*) |
|
365 Thm("d2_isolate_add2",num_str d2_isolate_add2), |
|
366 (* a+ x^2=0 -> x^2=(-1)a*) |
|
367 Thm("d2_sqrt_equation1",num_str d2_sqrt_equation1), |
|
368 (* x^2=c -> x=+-sqrt(c)*) |
|
369 Thm("d2_sqrt_equation1_neg",num_str d2_sqrt_equation1_neg), |
|
370 (* [c<0] x^2=c -> x=[]*) |
|
371 Thm("d2_sqrt_equation2",num_str d2_sqrt_equation2), |
|
372 (* x^2=0 -> x=0 *) |
|
373 Thm("d2_reduce_equation1",num_str d2_reduce_equation1), |
|
374 (* x(a+bx)=0 -> x=0 | a+bx=0*) |
|
375 Thm("d2_reduce_equation2",num_str d2_reduce_equation2), |
|
376 (* x(a+ x)=0 -> x=0 | a+ x=0*) |
|
377 Thm("d2_isolate_div",num_str d2_isolate_div) |
|
378 (* bx^2=c -> x^2=c/b*) |
|
379 ], |
386 scr = Script ((term_of o the o (parse thy)) "empty_script") |
380 scr = Script ((term_of o the o (parse thy)) "empty_script") |
387 }:rls); |
381 }:rls); |
|
382 |
388 (* -- d3 -- *) |
383 (* -- d3 -- *) |
389 (*isolate the bound variable in an d3 equation; 'bdv' is a meta-constant*) |
384 (* isolate the bound variable in an d3 equation; 'bdv' is a meta-constant *) |
390 val d3_polyeq_simplify = prep_rls( |
385 val d3_polyeq_simplify = prep_rls( |
391 Rls {id = "d3_polyeq_simplify", preconds = [], |
386 Rls {id = "d3_polyeq_simplify", preconds = [], |
392 rew_ord = ("e_rew_ord",e_rew_ord), |
387 rew_ord = ("e_rew_ord",e_rew_ord), erls = PolyEq_erls, |
393 erls = PolyEq_erls, |
388 srls = Erls, calc = [], |
394 srls = Erls, |
389 rules = |
395 calc = [], |
390 [Thm("d3_reduce_equation1",num_str d3_reduce_equation1), |
396 (*asm_thm = [("d3_isolate_div","")],*) |
391 (*a*bdv + b*bdv^^^2 + c*bdv^^^3=0) = |
397 rules = [ |
392 (bdv=0 | (a + b*bdv + c*bdv^^^2=0)*) |
398 Thm("d3_reduce_equation1",num_str d3_reduce_equation1), |
393 Thm("d3_reduce_equation2",num_str d3_reduce_equation2), |
399 (*a*bdv + b*bdv^^^2 + c*bdv^^^3=0) = (bdv=0 | (a + b*bdv + c*bdv^^^2=0)*) |
394 (* bdv + b*bdv^^^2 + c*bdv^^^3=0) = |
400 Thm("d3_reduce_equation2",num_str d3_reduce_equation2), |
395 (bdv=0 | (1 + b*bdv + c*bdv^^^2=0)*) |
401 (* bdv + b*bdv^^^2 + c*bdv^^^3=0) = (bdv=0 | (1 + b*bdv + c*bdv^^^2=0)*) |
396 Thm("d3_reduce_equation3",num_str d3_reduce_equation3), |
402 Thm("d3_reduce_equation3",num_str d3_reduce_equation3), |
397 (*a*bdv + bdv^^^2 + c*bdv^^^3=0) = |
403 (*a*bdv + bdv^^^2 + c*bdv^^^3=0) = (bdv=0 | (a + bdv + c*bdv^^^2=0)*) |
398 (bdv=0 | (a + bdv + c*bdv^^^2=0)*) |
404 Thm("d3_reduce_equation4",num_str d3_reduce_equation4), |
399 Thm("d3_reduce_equation4",num_str d3_reduce_equation4), |
405 (* bdv + bdv^^^2 + c*bdv^^^3=0) = (bdv=0 | (1 + bdv + c*bdv^^^2=0)*) |
400 (* bdv + bdv^^^2 + c*bdv^^^3=0) = |
406 Thm("d3_reduce_equation5",num_str d3_reduce_equation5), |
401 (bdv=0 | (1 + bdv + c*bdv^^^2=0)*) |
407 (*a*bdv + b*bdv^^^2 + bdv^^^3=0) = (bdv=0 | (a + b*bdv + bdv^^^2=0)*) |
402 Thm("d3_reduce_equation5",num_str d3_reduce_equation5), |
408 Thm("d3_reduce_equation6",num_str d3_reduce_equation6), |
403 (*a*bdv + b*bdv^^^2 + bdv^^^3=0) = |
409 (* bdv + b*bdv^^^2 + bdv^^^3=0) = (bdv=0 | (1 + b*bdv + bdv^^^2=0)*) |
404 (bdv=0 | (a + b*bdv + bdv^^^2=0)*) |
410 Thm("d3_reduce_equation7",num_str d3_reduce_equation7), |
405 Thm("d3_reduce_equation6",num_str d3_reduce_equation6), |
411 (*a*bdv + bdv^^^2 + bdv^^^3=0) = (bdv=0 | (1 + bdv + bdv^^^2=0)*) |
406 (* bdv + b*bdv^^^2 + bdv^^^3=0) = |
412 Thm("d3_reduce_equation8",num_str d3_reduce_equation8), |
407 (bdv=0 | (1 + b*bdv + bdv^^^2=0)*) |
413 (* bdv + bdv^^^2 + bdv^^^3=0) = (bdv=0 | (1 + bdv + bdv^^^2=0)*) |
408 Thm("d3_reduce_equation7",num_str d3_reduce_equation7), |
414 Thm("d3_reduce_equation9",num_str d3_reduce_equation9), |
409 (*a*bdv + bdv^^^2 + bdv^^^3=0) = |
415 (*a*bdv + c*bdv^^^3=0) = (bdv=0 | (a + c*bdv^^^2=0)*) |
410 (bdv=0 | (1 + bdv + bdv^^^2=0)*) |
416 Thm("d3_reduce_equation10",num_str d3_reduce_equation10), |
411 Thm("d3_reduce_equation8",num_str d3_reduce_equation8), |
417 (* bdv + c*bdv^^^3=0) = (bdv=0 | (1 + c*bdv^^^2=0)*) |
412 (* bdv + bdv^^^2 + bdv^^^3=0) = |
418 Thm("d3_reduce_equation11",num_str d3_reduce_equation11), |
413 (bdv=0 | (1 + bdv + bdv^^^2=0)*) |
419 (*a*bdv + bdv^^^3=0) = (bdv=0 | (a + bdv^^^2=0)*) |
414 Thm("d3_reduce_equation9",num_str d3_reduce_equation9), |
420 Thm("d3_reduce_equation12",num_str d3_reduce_equation12), |
415 (*a*bdv + c*bdv^^^3=0) = |
421 (* bdv + bdv^^^3=0) = (bdv=0 | (1 + bdv^^^2=0)*) |
416 (bdv=0 | (a + c*bdv^^^2=0)*) |
422 Thm("d3_reduce_equation13",num_str d3_reduce_equation13), |
417 Thm("d3_reduce_equation10",num_str d3_reduce_equation10), |
423 (* b*bdv^^^2 + c*bdv^^^3=0) = (bdv=0 | ( b*bdv + c*bdv^^^2=0)*) |
418 (* bdv + c*bdv^^^3=0) = |
424 Thm("d3_reduce_equation14",num_str d3_reduce_equation14), |
419 (bdv=0 | (1 + c*bdv^^^2=0)*) |
425 (* bdv^^^2 + c*bdv^^^3=0) = (bdv=0 | ( bdv + c*bdv^^^2=0)*) |
420 Thm("d3_reduce_equation11",num_str d3_reduce_equation11), |
426 Thm("d3_reduce_equation15",num_str d3_reduce_equation15), |
421 (*a*bdv + bdv^^^3=0) = |
427 (* b*bdv^^^2 + bdv^^^3=0) = (bdv=0 | ( b*bdv + bdv^^^2=0)*) |
422 (bdv=0 | (a + bdv^^^2=0)*) |
428 Thm("d3_reduce_equation16",num_str d3_reduce_equation16), |
423 Thm("d3_reduce_equation12",num_str d3_reduce_equation12), |
429 (* bdv^^^2 + bdv^^^3=0) = (bdv=0 | ( bdv + bdv^^^2=0)*) |
424 (* bdv + bdv^^^3=0) = |
430 Thm("d3_isolate_add1",num_str d3_isolate_add1), |
425 (bdv=0 | (1 + bdv^^^2=0)*) |
431 (*[|Not(bdv occurs_in a)|] ==> (a + b*bdv^^^3=0) = (bdv=0 | (b*bdv^^^3=a)*) |
426 Thm("d3_reduce_equation13",num_str d3_reduce_equation13), |
432 Thm("d3_isolate_add2",num_str d3_isolate_add2), |
427 (* b*bdv^^^2 + c*bdv^^^3=0) = |
433 (*[|Not(bdv occurs_in a)|] ==> (a + bdv^^^3=0) = (bdv=0 | ( bdv^^^3=a)*) |
428 (bdv=0 | ( b*bdv + c*bdv^^^2=0)*) |
434 Thm("d3_isolate_div",num_str d3_isolate_div), |
429 Thm("d3_reduce_equation14",num_str d3_reduce_equation14), |
435 (*[|Not(b=0)|] ==> (b*bdv^^^3=c) = (bdv^^^3=c/b*) |
430 (* bdv^^^2 + c*bdv^^^3=0) = |
436 Thm("d3_root_equation2",num_str d3_root_equation2), |
431 (bdv=0 | ( bdv + c*bdv^^^2=0)*) |
437 (*(bdv^^^3=0) = (bdv=0) *) |
432 Thm("d3_reduce_equation15",num_str d3_reduce_equation15), |
438 Thm("d3_root_equation1",num_str d3_root_equation1) |
433 (* b*bdv^^^2 + bdv^^^3=0) = |
439 (*bdv^^^3=c) = (bdv = nroot 3 c*) |
434 (bdv=0 | ( b*bdv + bdv^^^2=0)*) |
440 ], |
435 Thm("d3_reduce_equation16",num_str d3_reduce_equation16), |
|
436 (* bdv^^^2 + bdv^^^3=0) = |
|
437 (bdv=0 | ( bdv + bdv^^^2=0)*) |
|
438 Thm("d3_isolate_add1",num_str d3_isolate_add1), |
|
439 (*[|Not(bdv occurs_in a)|] ==> (a + b*bdv^^^3=0) = |
|
440 (bdv=0 | (b*bdv^^^3=a)*) |
|
441 Thm("d3_isolate_add2",num_str d3_isolate_add2), |
|
442 (*[|Not(bdv occurs_in a)|] ==> (a + bdv^^^3=0) = |
|
443 (bdv=0 | ( bdv^^^3=a)*) |
|
444 Thm("d3_isolate_div",num_str d3_isolate_div), |
|
445 (*[|Not(b=0)|] ==> (b*bdv^^^3=c) = (bdv^^^3=c/b*) |
|
446 Thm("d3_root_equation2",num_str d3_root_equation2), |
|
447 (*(bdv^^^3=0) = (bdv=0) *) |
|
448 Thm("d3_root_equation1",num_str d3_root_equation1) |
|
449 (*bdv^^^3=c) = (bdv = nroot 3 c*) |
|
450 ], |
441 scr = Script ((term_of o the o (parse thy)) "empty_script") |
451 scr = Script ((term_of o the o (parse thy)) "empty_script") |
442 }:rls); |
452 }:rls); |
|
453 |
443 (* -- d4 -- *) |
454 (* -- d4 -- *) |
444 (*isolate the bound variable in an d4 equation; 'bdv' is a meta-constant*) |
455 (*isolate the bound variable in an d4 equation; 'bdv' is a meta-constant*) |
445 val d4_polyeq_simplify = prep_rls( |
456 val d4_polyeq_simplify = prep_rls( |
446 Rls {id = "d4_polyeq_simplify", preconds = [], |
457 Rls {id = "d4_polyeq_simplify", preconds = [], |
447 rew_ord = ("e_rew_ord",e_rew_ord), |
458 rew_ord = ("e_rew_ord",e_rew_ord), erls = PolyEq_erls, |
448 erls = PolyEq_erls, |
459 srls = Erls, calc = [], |
449 srls = Erls, |
460 rules = |
450 calc = [], |
461 [Thm("d4_sub_u1",num_str d4_sub_u1) |
451 (*asm_thm = [],*) |
462 (* ax^4+bx^2+c=0 -> x=+-sqrt(ax^2+bx^+c) *) |
452 rules = [Thm("d4_sub_u1",num_str d4_sub_u1) |
463 ], |
453 (* ax^4+bx^2+c=0 -> x=+-sqrt(ax^2+bx^+c) *) |
|
454 ], |
|
455 scr = Script ((term_of o the o (parse thy)) "empty_script") |
464 scr = Script ((term_of o the o (parse thy)) "empty_script") |
456 }:rls); |
465 }:rls); |
457 |
466 |
458 ruleset' := overwritelthy thy (!ruleset', |
467 ruleset' := |
459 [("d0_polyeq_simplify", d0_polyeq_simplify), |
468 overwritelthy thy |
460 ("d1_polyeq_simplify", d1_polyeq_simplify), |
469 (!ruleset', |
461 ("d2_polyeq_simplify", d2_polyeq_simplify), |
470 [("d0_polyeq_simplify", d0_polyeq_simplify), |
462 ("d2_polyeq_bdv_only_simplify", d2_polyeq_bdv_only_simplify), |
471 ("d1_polyeq_simplify", d1_polyeq_simplify), |
463 ("d2_polyeq_sq_only_simplify", d2_polyeq_sq_only_simplify), |
472 ("d2_polyeq_simplify", d2_polyeq_simplify), |
464 ("d2_polyeq_pqFormula_simplify", d2_polyeq_pqFormula_simplify), |
473 ("d2_polyeq_bdv_only_simplify", d2_polyeq_bdv_only_simplify), |
465 ("d2_polyeq_abcFormula_simplify", d2_polyeq_abcFormula_simplify), |
474 ("d2_polyeq_sq_only_simplify", d2_polyeq_sq_only_simplify), |
466 ("d3_polyeq_simplify", d3_polyeq_simplify), |
475 ("d2_polyeq_pqFormula_simplify", d2_polyeq_pqFormula_simplify), |
467 ("d4_polyeq_simplify", d4_polyeq_simplify) |
476 ("d2_polyeq_abcFormula_simplify", |
468 ]); |
477 d2_polyeq_abcFormula_simplify), |
469 |
478 ("d3_polyeq_simplify", d3_polyeq_simplify), |
|
479 ("d4_polyeq_simplify", d4_polyeq_simplify) |
|
480 ]); |
|
481 |
470 (*------------------------problems------------------------*) |
482 (*------------------------problems------------------------*) |
471 (* |
483 (* |
472 (get_pbt ["degree_2","polynomial","univariate","equation"]); |
484 (get_pbt ["degree_2","polynomial","univariate","equation"]); |
473 show_ptyps(); |
485 show_ptyps(); |
474 *) |
486 *) |
475 |
487 |
476 (*-------------------------poly-----------------------*) |
488 (*-------------------------poly-----------------------*) |
477 store_pbt |
489 store_pbt |
478 (prep_pbt PolyEq.thy "pbl_equ_univ_poly" [] e_pblID |
490 (prep_pbt (theory "PolyEq") "pbl_equ_univ_poly" [] e_pblID |
479 (["polynomial","univariate","equation"], |
491 (["polynomial","univariate","equation"], |
480 [("#Given" ,["equality e_","solveFor v_"]), |
492 [("#Given" ,["equality e_","solveFor v_"]), |
481 ("#Where" ,["~((e_::bool) is_ratequation_in (v_::real))", |
493 ("#Where" ,["~((e_::bool) is_ratequation_in (v_::real))", |
482 "~((lhs e_) is_rootTerm_in (v_::real))", |
494 "~((lhs e_) is_rootTerm_in (v_::real))", |
483 "~((rhs e_) is_rootTerm_in (v_::real))"]), |
495 "~((rhs e_) is_rootTerm_in (v_::real))"]), |
525 ], |
537 ], |
526 PolyEq_prls, SOME "solve (e_::bool, v_)", |
538 PolyEq_prls, SOME "solve (e_::bool, v_)", |
527 [["PolyEq","solve_d2_polyeq_equation"]])); |
539 [["PolyEq","solve_d2_polyeq_equation"]])); |
528 |
540 |
529 store_pbt |
541 store_pbt |
530 (prep_pbt PolyEq.thy "pbl_equ_univ_poly_deg2_sqonly" [] e_pblID |
542 (prep_pbt (theory "PolyEq") "pbl_equ_univ_poly_deg2_sqonly" [] e_pblID |
531 (["sq_only","degree_2","polynomial","univariate","equation"], |
543 (["sq_only","degree_2","polynomial","univariate","equation"], |
532 [("#Given" ,["equality e_","solveFor v_"]), |
544 [("#Given" ,["equality e_","solveFor v_"]), |
533 ("#Where" ,["matches ( ?a + ?v_^^^2 = 0) e_ | \ |
545 ("#Where" ,["matches ( ?a + ?v_^^^2 = 0) e_ | " ^ |
534 \matches ( ?a + ?b*?v_^^^2 = 0) e_ | \ |
546 "matches ( ?a + ?b*?v_^^^2 = 0) e_ | " ^ |
535 \matches ( ?v_^^^2 = 0) e_ | \ |
547 "matches ( ?v_^^^2 = 0) e_ | " ^ |
536 \matches ( ?b*?v_^^^2 = 0) e_" , |
548 "matches ( ?b*?v_^^^2 = 0) e_" , |
537 "Not (matches (?a + ?v_ + ?v_^^^2 = 0) e_) &\ |
549 "Not (matches (?a + ?v_ + ?v_^^^2 = 0) e_) &" ^ |
538 \Not (matches (?a + ?b*?v_ + ?v_^^^2 = 0) e_) &\ |
550 "Not (matches (?a + ?b*?v_ + ?v_^^^2 = 0) e_) &" ^ |
539 \Not (matches (?a + ?v_ + ?c*?v_^^^2 = 0) e_) &\ |
551 "Not (matches (?a + ?v_ + ?c*?v_^^^2 = 0) e_) &" ^ |
540 \Not (matches (?a + ?b*?v_ + ?c*?v_^^^2 = 0) e_) &\ |
552 "Not (matches (?a + ?b*?v_ + ?c*?v_^^^2 = 0) e_) &" ^ |
541 \Not (matches ( ?v_ + ?v_^^^2 = 0) e_) &\ |
553 "Not (matches ( ?v_ + ?v_^^^2 = 0) e_) &" ^ |
542 \Not (matches ( ?b*?v_ + ?v_^^^2 = 0) e_) &\ |
554 "Not (matches ( ?b*?v_ + ?v_^^^2 = 0) e_) &" ^ |
543 \Not (matches ( ?v_ + ?c*?v_^^^2 = 0) e_) &\ |
555 "Not (matches ( ?v_ + ?c*?v_^^^2 = 0) e_) &" ^ |
544 \Not (matches ( ?b*?v_ + ?c*?v_^^^2 = 0) e_)"]), |
556 "Not (matches ( ?b*?v_ + ?c*?v_^^^2 = 0) e_)"]), |
545 ("#Find" ,["solutions v_i_"]) |
557 ("#Find" ,["solutions v_i_"]) |
546 ], |
558 ], |
547 PolyEq_prls, SOME "solve (e_::bool, v_)", |
559 PolyEq_prls, SOME "solve (e_::bool, v_)", |
548 [["PolyEq","solve_d2_polyeq_sqonly_equation"]])); |
560 [["PolyEq","solve_d2_polyeq_sqonly_equation"]])); |
549 |
561 |
550 store_pbt |
562 store_pbt |
551 (prep_pbt PolyEq.thy "pbl_equ_univ_poly_deg2_bdvonly" [] e_pblID |
563 (prep_pbt (theory "PolyEq") "pbl_equ_univ_poly_deg2_bdvonly" [] e_pblID |
552 (["bdv_only","degree_2","polynomial","univariate","equation"], |
564 (["bdv_only","degree_2","polynomial","univariate","equation"], |
553 [("#Given" ,["equality e_","solveFor v_"]), |
565 [("#Given" ,["equality e_","solveFor v_"]), |
554 ("#Where" ,["matches (?a*?v_ + ?v_^^^2 = 0) e_ | \ |
566 ("#Where" ,["matches (?a*?v_ + ?v_^^^2 = 0) e_ | " ^ |
555 \matches ( ?v_ + ?v_^^^2 = 0) e_ | \ |
567 "matches ( ?v_ + ?v_^^^2 = 0) e_ | " ^ |
556 \matches ( ?v_ + ?b*?v_^^^2 = 0) e_ | \ |
568 "matches ( ?v_ + ?b*?v_^^^2 = 0) e_ | " ^ |
557 \matches (?a*?v_ + ?b*?v_^^^2 = 0) e_ | \ |
569 "matches (?a*?v_ + ?b*?v_^^^2 = 0) e_ | " ^ |
558 \matches ( ?v_^^^2 = 0) e_ | \ |
570 "matches ( ?v_^^^2 = 0) e_ | " ^ |
559 \matches ( ?b*?v_^^^2 = 0) e_ "]), |
571 "matches ( ?b*?v_^^^2 = 0) e_ "]), |
560 ("#Find" ,["solutions v_i_"]) |
572 ("#Find" ,["solutions v_i_"]) |
561 ], |
573 ], |
562 PolyEq_prls, SOME "solve (e_::bool, v_)", |
574 PolyEq_prls, SOME "solve (e_::bool, v_)", |
563 [["PolyEq","solve_d2_polyeq_bdvonly_equation"]])); |
575 [["PolyEq","solve_d2_polyeq_bdvonly_equation"]])); |
564 |
576 |
565 store_pbt |
577 store_pbt |
566 (prep_pbt PolyEq.thy "pbl_equ_univ_poly_deg2_pq" [] e_pblID |
578 (prep_pbt (theory "PolyEq") "pbl_equ_univ_poly_deg2_pq" [] e_pblID |
567 (["pqFormula","degree_2","polynomial","univariate","equation"], |
579 (["pqFormula","degree_2","polynomial","univariate","equation"], |
568 [("#Given" ,["equality e_","solveFor v_"]), |
580 [("#Given" ,["equality e_","solveFor v_"]), |
569 ("#Where" ,["matches (?a + 1*?v_^^^2 = 0) e_ | \ |
581 ("#Where" ,["matches (?a + 1*?v_^^^2 = 0) e_ | " ^ |
570 \matches (?a + ?v_^^^2 = 0) e_"]), |
582 "matches (?a + ?v_^^^2 = 0) e_"]), |
571 ("#Find" ,["solutions v_i_"]) |
583 ("#Find" ,["solutions v_i_"]) |
572 ], |
584 ], |
573 PolyEq_prls, SOME "solve (e_::bool, v_)", |
585 PolyEq_prls, SOME "solve (e_::bool, v_)", |
574 [["PolyEq","solve_d2_polyeq_pq_equation"]])); |
586 [["PolyEq","solve_d2_polyeq_pq_equation"]])); |
575 |
587 |
576 store_pbt |
588 store_pbt |
577 (prep_pbt PolyEq.thy "pbl_equ_univ_poly_deg2_abc" [] e_pblID |
589 (prep_pbt (theory "PolyEq") "pbl_equ_univ_poly_deg2_abc" [] e_pblID |
578 (["abcFormula","degree_2","polynomial","univariate","equation"], |
590 (["abcFormula","degree_2","polynomial","univariate","equation"], |
579 [("#Given" ,["equality e_","solveFor v_"]), |
591 [("#Given" ,["equality e_","solveFor v_"]), |
580 ("#Where" ,["matches (?a + ?v_^^^2 = 0) e_ | \ |
592 ("#Where" ,["matches (?a + ?v_^^^2 = 0) e_ | " ^ |
581 \matches (?a + ?b*?v_^^^2 = 0) e_"]), |
593 "matches (?a + ?b*?v_^^^2 = 0) e_"]), |
582 ("#Find" ,["solutions v_i_"]) |
594 ("#Find" ,["solutions v_i_"]) |
583 ], |
595 ], |
584 PolyEq_prls, SOME "solve (e_::bool, v_)", |
596 PolyEq_prls, SOME "solve (e_::bool, v_)", |
585 [["PolyEq","solve_d2_polyeq_abc_equation"]])); |
597 [["PolyEq","solve_d2_polyeq_abc_equation"]])); |
586 |
598 |
587 (*--- d3 ---*) |
599 (*--- d3 ---*) |
588 store_pbt |
600 store_pbt |
589 (prep_pbt PolyEq.thy "pbl_equ_univ_poly_deg3" [] e_pblID |
601 (prep_pbt (theory "PolyEq") "pbl_equ_univ_poly_deg3" [] e_pblID |
590 (["degree_3","polynomial","univariate","equation"], |
602 (["degree_3","polynomial","univariate","equation"], |
591 [("#Given" ,["equality e_","solveFor v_"]), |
603 [("#Given" ,["equality e_","solveFor v_"]), |
592 ("#Where" ,["matches (?a = 0) e_", |
604 ("#Where" ,["matches (?a = 0) e_", |
593 "(lhs e_) is_poly_in v_ ", |
605 "(lhs e_) is_poly_in v_ ", |
594 "((lhs e_) has_degree_in v_) = 3"]), |
606 "((lhs e_) has_degree_in v_) = 3"]), |
894 {rew_ord'="termlessI", |
868 {rew_ord'="termlessI", |
895 rls'=PolyEq_erls, |
869 rls'=PolyEq_erls, |
896 srls=e_rls, |
870 srls=e_rls, |
897 prls=PolyEq_prls, |
871 prls=PolyEq_prls, |
898 calc=[("sqrt", ("Root.sqrt", eval_sqrt "#sqrt_"))], |
872 calc=[("sqrt", ("Root.sqrt", eval_sqrt "#sqrt_"))], |
899 crls=PolyEq_crls, nrls=norm_Rational(*, |
873 crls=PolyEq_crls, nrls=norm_Rational}, |
900 (* asm_rls=["d1_polyeq_simplify","d2_polyeq_simplify","d1_polyeq_simplify"],*) |
874 "Script Solve_d3_polyeq_equation (e_::bool) (v_::real) = " ^ |
901 asm_rls=[], |
875 " (let e_ = ((Try (Rewrite_Set_Inst [(bdv,v_::real)] " ^ |
902 asm_thm=[("d3_isolate_div",""),("d1_isolate_div",""),("d2_pqformula1",""), |
876 " d3_polyeq_simplify True)) @@ " ^ |
903 ("d2_pqformula2",""),("d2_pqformula3",""),("d2_pqformula4",""), |
877 " (Try (Rewrite_Set polyeq_simplify False)) @@ " ^ |
904 ("d2_pqformula1_neg",""), ("d2_pqformula2_neg",""),("d2_pqformula3_neg",""), |
878 " (Try (Rewrite_Set_Inst [(bdv,v_::real)] " ^ |
905 ("d2_pqformula4_neg",""), ("d2_abcformula1",""),("d2_abcformula2",""), |
879 " d2_polyeq_simplify True)) @@ " ^ |
906 ("d2_abcformula1_neg",""),("d2_abcformula2_neg",""), |
880 " (Try (Rewrite_Set polyeq_simplify False)) @@ " ^ |
907 ("d2_sqrt_equation1",""),("d2_sqrt_equation1_neg",""), ("d2_isolate_div","")]*)}, |
881 " (Try (Rewrite_Set_Inst [(bdv,v_::real)] " ^ |
908 "Script Solve_d3_polyeq_equation (e_::bool) (v_::real) = \ |
882 " d1_polyeq_simplify True)) @@ " ^ |
909 \ (let e_ = ((Try (Rewrite_Set_Inst [(bdv,v_::real)] \ |
883 " (Try (Rewrite_Set polyeq_simplify False)) @@ " ^ |
910 \ d3_polyeq_simplify True)) @@ \ |
884 " (Try (Rewrite_Set norm_Rational_parenthesized False))) e_;" ^ |
911 \ (Try (Rewrite_Set polyeq_simplify False)) @@ \ |
885 " (L_::bool list) = ((Or_to_List e_)::bool list) " ^ |
912 \ (Try (Rewrite_Set_Inst [(bdv,v_::real)] \ |
886 " in Check_elementwise L_ {(v_::real). Assumptions} )" |
913 \ d2_polyeq_simplify True)) @@ \ |
|
914 \ (Try (Rewrite_Set polyeq_simplify False)) @@ \ |
|
915 \ (Try (Rewrite_Set_Inst [(bdv,v_::real)] \ |
|
916 \ d1_polyeq_simplify True)) @@ \ |
|
917 \ (Try (Rewrite_Set polyeq_simplify False)) @@ \ |
|
918 \ (Try (Rewrite_Set norm_Rational_parenthesized False))) e_;\ |
|
919 \ (L_::bool list) = ((Or_to_List e_)::bool list) \ |
|
920 \ in Check_elementwise L_ {(v_::real). Assumptions} )" |
|
921 )); |
887 )); |
922 |
888 |
923 (*.solves all expanded (ie. normalized) terms of degree 2.*) |
889 (*.solves all expanded (ie. normalized) terms of degree 2.*) |
924 (*Oct.02 restriction: 'eval_true 0 =< discriminant' ony for integer values |
890 (*Oct.02 restriction: 'eval_true 0 =< discriminant' ony for integer values |
925 by 'PolyEq_erls'; restricted until Float.thy is implemented*) |
891 by 'PolyEq_erls'; restricted until Float.thy is implemented*) |
926 store_met |
892 store_met |
927 (prep_met PolyEq.thy "met_polyeq_complsq" [] e_metID |
893 (prep_met (theory "PolyEq") "met_polyeq_complsq" [] e_metID |
928 (["PolyEq","complete_square"], |
894 (["PolyEq","complete_square"], |
929 [("#Given" ,["equality e_","solveFor v_"]), |
895 [("#Given" ,["equality e_","solveFor v_"]), |
930 ("#Where" ,["matches (?a = 0) e_", |
896 ("#Where" ,["matches (?a = 0) e_", |
931 "((lhs e_) has_degree_in v_) = 2"]), |
897 "((lhs e_) has_degree_in v_) = 2"]), |
932 ("#Find" ,["solutions v_i_"]) |
898 ("#Find" ,["solutions v_i_"]) |
933 ], |
899 ], |
934 {rew_ord'="termlessI",rls'=PolyEq_erls,srls=e_rls,prls=PolyEq_prls, |
900 {rew_ord'="termlessI",rls'=PolyEq_erls,srls=e_rls,prls=PolyEq_prls, |
935 calc=[("sqrt", ("Root.sqrt", eval_sqrt "#sqrt_"))], |
901 calc=[("sqrt", ("Root.sqrt", eval_sqrt "#sqrt_"))], |
936 crls=PolyEq_crls, nrls=norm_Rational(*, |
902 crls=PolyEq_crls, nrls=norm_Rational}, |
937 asm_rls=[], |
903 "Script Complete_square (e_::bool) (v_::real) = " ^ |
938 asm_thm=[("root_plus_minus","")]*)}, |
904 "(let e_ = ((Try (Rewrite_Set_Inst [(bdv,v_)] cancel_leading_coeff True))" ^ |
939 "Script Complete_square (e_::bool) (v_::real) = \ |
905 " @@ (Try (Rewrite_Set_Inst [(bdv,v_)] complete_square True)) " ^ |
940 \(let e_ = ((Try (Rewrite_Set_Inst [(bdv,v_)] cancel_leading_coeff True))\ |
906 " @@ (Try (Rewrite square_explicit1 False)) " ^ |
941 \ @@ (Try (Rewrite_Set_Inst [(bdv,v_)] complete_square True)) \ |
907 " @@ (Try (Rewrite square_explicit2 False)) " ^ |
942 \ @@ (Try (Rewrite square_explicit1 False)) \ |
908 " @@ (Rewrite root_plus_minus True) " ^ |
943 \ @@ (Try (Rewrite square_explicit2 False)) \ |
909 " @@ (Try (Repeat (Rewrite_Inst [(bdv,v_)] bdv_explicit1 False))) " ^ |
944 \ @@ (Rewrite root_plus_minus True) \ |
910 " @@ (Try (Repeat (Rewrite_Inst [(bdv,v_)] bdv_explicit2 False))) " ^ |
945 \ @@ (Try (Repeat (Rewrite_Inst [(bdv,v_)] bdv_explicit1 False))) \ |
911 " @@ (Try (Repeat " ^ |
946 \ @@ (Try (Repeat (Rewrite_Inst [(bdv,v_)] bdv_explicit2 False))) \ |
912 " (Rewrite_Inst [(bdv,v_)] bdv_explicit3 False))) " ^ |
947 \ @@ (Try (Repeat \ |
913 " @@ (Try (Rewrite_Set calculate_RootRat False)) " ^ |
948 \ (Rewrite_Inst [(bdv,v_)] bdv_explicit3 False))) \ |
914 " @@ (Try (Repeat (Calculate sqrt_)))) e_ " ^ |
949 \ @@ (Try (Rewrite_Set calculate_RootRat False)) \ |
915 " in ((Or_to_List e_)::bool list))" |
950 \ @@ (Try (Repeat (Calculate sqrt_)))) e_ \ |
|
951 \ in ((Or_to_List e_)::bool list))" |
|
952 )); |
916 )); |
953 (*6.10.02: x^2=64: root_plus_minus -/-/-> |
917 |
954 "Script Complete_square (e_::bool) (v_::real) = \ |
918 |
955 \(let e_ = ((Try (Rewrite_Set_Inst [(bdv,v_)] cancel_leading_coeff True))\ |
919 (* termorder hacked by MG *) |
956 \ @@ (Try (Rewrite_Set_Inst [(bdv,v_)] complete_square True)) \ |
|
957 \ @@ (Try ((Rewrite square_explicit1 False) \ |
|
958 \ Or (Rewrite square_explicit2 False))) \ |
|
959 \ @@ (Rewrite root_plus_minus True) \ |
|
960 \ @@ ((Repeat (Rewrite_Inst [(bdv,v_)] bdv_explicit1 False)) \ |
|
961 \ Or (Repeat (Rewrite_Inst [(bdv,v_)] bdv_explicit2 False))) \ |
|
962 \ @@ (Try (Repeat \ |
|
963 \ (Rewrite_Inst [(bdv,v_)] bdv_explicit3 False))) \ |
|
964 \ @@ (Try (Rewrite_Set calculate_RootRat False)) \ |
|
965 \ @@ (Try (Repeat (Calculate sqrt_)))) e_ \ |
|
966 \ in ((Or_to_List e_)::bool list))"*) |
|
967 |
|
968 "******* PolyEq.ML end *******"; |
|
969 |
|
970 (*eine gehackte termorder*) |
|
971 local (*. for make_polynomial_in .*) |
920 local (*. for make_polynomial_in .*) |
972 |
921 |
973 open Term; (* for type order = EQUAL | LESS | GREATER *) |
922 open Term; (* for type order = EQUAL | LESS | GREATER *) |
974 |
923 |
975 fun pr_ord EQUAL = "EQUAL" |
924 fun pr_ord EQUAL = "EQUAL" |