238 (*isolate the bound variable in an sqrt equation; 'bdv' is a meta-constant*) |
238 (*isolate the bound variable in an sqrt equation; 'bdv' is a meta-constant*) |
239 val sqrt_isolate = prep_rls( |
239 val sqrt_isolate = prep_rls( |
240 Rls {id = "sqrt_isolate", preconds = [], rew_ord = ("termlessI",termlessI), |
240 Rls {id = "sqrt_isolate", preconds = [], rew_ord = ("termlessI",termlessI), |
241 erls = RootEq_erls, srls = Erls, calc = [], |
241 erls = RootEq_erls, srls = Erls, calc = [], |
242 rules = [ |
242 rules = [ |
243 Thm("sqrt_square_1",num_str sqrt_square_1), |
243 Thm("sqrt_square_1",num_str @{sqrt_square_1), |
244 (* (sqrt a)^^^2 -> a *) |
244 (* (sqrt a)^^^2 -> a *) |
245 Thm("sqrt_square_2",num_str sqrt_square_2), |
245 Thm("sqrt_square_2",num_str @{sqrt_square_2), |
246 (* sqrt (a^^^2) -> a *) |
246 (* sqrt (a^^^2) -> a *) |
247 Thm("sqrt_times_root_1",num_str sqrt_times_root_1), |
247 Thm("sqrt_times_root_1",num_str @{sqrt_times_root_1), |
248 (* sqrt a sqrt b -> sqrt(ab) *) |
248 (* sqrt a sqrt b -> sqrt(ab) *) |
249 Thm("sqrt_times_root_2",num_str sqrt_times_root_2), |
249 Thm("sqrt_times_root_2",num_str @{sqrt_times_root_2), |
250 (* a sqrt b sqrt c -> a sqrt(bc) *) |
250 (* a sqrt b sqrt c -> a sqrt(bc) *) |
251 Thm("sqrt_square_equation_both_1", |
251 Thm("sqrt_square_equation_both_1", |
252 num_str sqrt_square_equation_both_1), |
252 num_str @{sqrt_square_equation_both_1), |
253 (* (sqrt a + sqrt b = sqrt c + sqrt d) -> |
253 (* (sqrt a + sqrt b = sqrt c + sqrt d) -> |
254 (a+2*sqrt(a)*sqrt(b)+b) = c+2*sqrt(c)*sqrt(d)+d) *) |
254 (a+2*sqrt(a)*sqrt(b)+b) = c+2*sqrt(c)*sqrt(d)+d) *) |
255 Thm("sqrt_square_equation_both_2", |
255 Thm("sqrt_square_equation_both_2", |
256 num_str sqrt_square_equation_both_2), |
256 num_str @{sqrt_square_equation_both_2), |
257 (* (sqrt a - sqrt b = sqrt c + sqrt d) -> |
257 (* (sqrt a - sqrt b = sqrt c + sqrt d) -> |
258 (a-2*sqrt(a)*sqrt(b)+b) = c+2*sqrt(c)*sqrt(d)+d) *) |
258 (a-2*sqrt(a)*sqrt(b)+b) = c+2*sqrt(c)*sqrt(d)+d) *) |
259 Thm("sqrt_square_equation_both_3", |
259 Thm("sqrt_square_equation_both_3", |
260 num_str sqrt_square_equation_both_3), |
260 num_str @{sqrt_square_equation_both_3), |
261 (* (sqrt a + sqrt b = sqrt c - sqrt d) -> |
261 (* (sqrt a + sqrt b = sqrt c - sqrt d) -> |
262 (a+2*sqrt(a)*sqrt(b)+b) = c-2*sqrt(c)*sqrt(d)+d) *) |
262 (a+2*sqrt(a)*sqrt(b)+b) = c-2*sqrt(c)*sqrt(d)+d) *) |
263 Thm("sqrt_square_equation_both_4", |
263 Thm("sqrt_square_equation_both_4", |
264 num_str sqrt_square_equation_both_4), |
264 num_str @{sqrt_square_equation_both_4), |
265 (* (sqrt a - sqrt b = sqrt c - sqrt d) -> |
265 (* (sqrt a - sqrt b = sqrt c - sqrt d) -> |
266 (a-2*sqrt(a)*sqrt(b)+b) = c-2*sqrt(c)*sqrt(d)+d) *) |
266 (a-2*sqrt(a)*sqrt(b)+b) = c-2*sqrt(c)*sqrt(d)+d) *) |
267 Thm("sqrt_isolate_l_add1", |
267 Thm("sqrt_isolate_l_add1", |
268 num_str sqrt_isolate_l_add1), |
268 num_str @{sqrt_isolate_l_add1), |
269 (* a+b*sqrt(x)=d -> b*sqrt(x) = d-a *) |
269 (* a+b*sqrt(x)=d -> b*sqrt(x) = d-a *) |
270 Thm("sqrt_isolate_l_add2", |
270 Thm("sqrt_isolate_l_add2", |
271 num_str sqrt_isolate_l_add2), |
271 num_str @{sqrt_isolate_l_add2), |
272 (* a+ sqrt(x)=d -> sqrt(x) = d-a *) |
272 (* a+ sqrt(x)=d -> sqrt(x) = d-a *) |
273 Thm("sqrt_isolate_l_add3", |
273 Thm("sqrt_isolate_l_add3", |
274 num_str sqrt_isolate_l_add3), |
274 num_str @{sqrt_isolate_l_add3), |
275 (* a+b*c/sqrt(x)=d->b*c/sqrt(x)=d-a *) |
275 (* a+b*c/sqrt(x)=d->b*c/sqrt(x)=d-a *) |
276 Thm("sqrt_isolate_l_add4", |
276 Thm("sqrt_isolate_l_add4", |
277 num_str sqrt_isolate_l_add4), |
277 num_str @{sqrt_isolate_l_add4), |
278 (* a+c/sqrt(x)=d -> c/sqrt(x) = d-a *) |
278 (* a+c/sqrt(x)=d -> c/sqrt(x) = d-a *) |
279 Thm("sqrt_isolate_l_add5", |
279 Thm("sqrt_isolate_l_add5", |
280 num_str sqrt_isolate_l_add5), |
280 num_str @{sqrt_isolate_l_add5), |
281 (* a+b*c/f*sqrt(x)=d->b*c/f*sqrt(x)=d-a *) |
281 (* a+b*c/f*sqrt(x)=d->b*c/f*sqrt(x)=d-a *) |
282 Thm("sqrt_isolate_l_add6", |
282 Thm("sqrt_isolate_l_add6", |
283 num_str sqrt_isolate_l_add6), |
283 num_str @{sqrt_isolate_l_add6), |
284 (* a+c/f*sqrt(x)=d -> c/f*sqrt(x) = d-a *) |
284 (* a+c/f*sqrt(x)=d -> c/f*sqrt(x) = d-a *) |
285 (*Thm("sqrt_isolate_l_div",num_str sqrt_isolate_l_div),*) |
285 (*Thm("sqrt_isolate_l_div",num_str @{sqrt_isolate_l_div),*) |
286 (* b*sqrt(x) = d sqrt(x) d/b *) |
286 (* b*sqrt(x) = d sqrt(x) d/b *) |
287 Thm("sqrt_isolate_r_add1", |
287 Thm("sqrt_isolate_r_add1", |
288 num_str sqrt_isolate_r_add1), |
288 num_str @{sqrt_isolate_r_add1), |
289 (* a= d+e*sqrt(x) -> a-d=e*sqrt(x) *) |
289 (* a= d+e*sqrt(x) -> a-d=e*sqrt(x) *) |
290 Thm("sqrt_isolate_r_add2", |
290 Thm("sqrt_isolate_r_add2", |
291 num_str sqrt_isolate_r_add2), |
291 num_str @{sqrt_isolate_r_add2), |
292 (* a= d+ sqrt(x) -> a-d= sqrt(x) *) |
292 (* a= d+ sqrt(x) -> a-d= sqrt(x) *) |
293 Thm("sqrt_isolate_r_add3", |
293 Thm("sqrt_isolate_r_add3", |
294 num_str sqrt_isolate_r_add3), |
294 num_str @{sqrt_isolate_r_add3), |
295 (* a=d+e*g/sqrt(x)->a-d=e*g/sqrt(x)*) |
295 (* a=d+e*g/sqrt(x)->a-d=e*g/sqrt(x)*) |
296 Thm("sqrt_isolate_r_add4", |
296 Thm("sqrt_isolate_r_add4", |
297 num_str sqrt_isolate_r_add4), |
297 num_str @{sqrt_isolate_r_add4), |
298 (* a= d+g/sqrt(x) -> a-d=g/sqrt(x) *) |
298 (* a= d+g/sqrt(x) -> a-d=g/sqrt(x) *) |
299 Thm("sqrt_isolate_r_add5", |
299 Thm("sqrt_isolate_r_add5", |
300 num_str sqrt_isolate_r_add5), |
300 num_str @{sqrt_isolate_r_add5), |
301 (* a=d+e*g/h*sqrt(x)->a-d=e*g/h*sqrt(x)*) |
301 (* a=d+e*g/h*sqrt(x)->a-d=e*g/h*sqrt(x)*) |
302 Thm("sqrt_isolate_r_add6", |
302 Thm("sqrt_isolate_r_add6", |
303 num_str sqrt_isolate_r_add6), |
303 num_str @{sqrt_isolate_r_add6), |
304 (* a= d+g/h*sqrt(x) -> a-d=g/h*sqrt(x) *) |
304 (* a= d+g/h*sqrt(x) -> a-d=g/h*sqrt(x) *) |
305 (*Thm("sqrt_isolate_r_div",num_str sqrt_isolate_r_div),*) |
305 (*Thm("sqrt_isolate_r_div",num_str @{sqrt_isolate_r_div),*) |
306 (* a=e*sqrt(x) -> a/e = sqrt(x) *) |
306 (* a=e*sqrt(x) -> a/e = sqrt(x) *) |
307 Thm("sqrt_square_equation_left_1", |
307 Thm("sqrt_square_equation_left_1", |
308 num_str sqrt_square_equation_left_1), |
308 num_str @{sqrt_square_equation_left_1), |
309 (* sqrt(x)=b -> x=b^2 *) |
309 (* sqrt(x)=b -> x=b^2 *) |
310 Thm("sqrt_square_equation_left_2", |
310 Thm("sqrt_square_equation_left_2", |
311 num_str sqrt_square_equation_left_2), |
311 num_str @{sqrt_square_equation_left_2), |
312 (* c*sqrt(x)=b -> c^2*x=b^2 *) |
312 (* c*sqrt(x)=b -> c^2*x=b^2 *) |
313 Thm("sqrt_square_equation_left_3",num_str sqrt_square_equation_left_3), |
313 Thm("sqrt_square_equation_left_3",num_str @{sqrt_square_equation_left_3), |
314 (* c/sqrt(x)=b -> c^2/x=b^2 *) |
314 (* c/sqrt(x)=b -> c^2/x=b^2 *) |
315 Thm("sqrt_square_equation_left_4",num_str sqrt_square_equation_left_4), |
315 Thm("sqrt_square_equation_left_4",num_str @{sqrt_square_equation_left_4), |
316 (* c*d/sqrt(x)=b -> c^2*d^2/x=b^2 *) |
316 (* c*d/sqrt(x)=b -> c^2*d^2/x=b^2 *) |
317 Thm("sqrt_square_equation_left_5",num_str sqrt_square_equation_left_5), |
317 Thm("sqrt_square_equation_left_5",num_str @{sqrt_square_equation_left_5), |
318 (* c/d*sqrt(x)=b -> c^2/d^2x=b^2 *) |
318 (* c/d*sqrt(x)=b -> c^2/d^2x=b^2 *) |
319 Thm("sqrt_square_equation_left_6",num_str sqrt_square_equation_left_6), |
319 Thm("sqrt_square_equation_left_6",num_str @{sqrt_square_equation_left_6), |
320 (* c*d/g*sqrt(x)=b -> c^2*d^2/g^2x=b^2 *) |
320 (* c*d/g*sqrt(x)=b -> c^2*d^2/g^2x=b^2 *) |
321 Thm("sqrt_square_equation_right_1",num_str sqrt_square_equation_right_1), |
321 Thm("sqrt_square_equation_right_1",num_str @{sqrt_square_equation_right_1), |
322 (* a=sqrt(x) ->a^2=x *) |
322 (* a=sqrt(x) ->a^2=x *) |
323 Thm("sqrt_square_equation_right_2",num_str sqrt_square_equation_right_2), |
323 Thm("sqrt_square_equation_right_2",num_str @{sqrt_square_equation_right_2), |
324 (* a=c*sqrt(x) ->a^2=c^2*x *) |
324 (* a=c*sqrt(x) ->a^2=c^2*x *) |
325 Thm("sqrt_square_equation_right_3",num_str sqrt_square_equation_right_3), |
325 Thm("sqrt_square_equation_right_3",num_str @{sqrt_square_equation_right_3), |
326 (* a=c/sqrt(x) ->a^2=c^2/x *) |
326 (* a=c/sqrt(x) ->a^2=c^2/x *) |
327 Thm("sqrt_square_equation_right_4",num_str sqrt_square_equation_right_4), |
327 Thm("sqrt_square_equation_right_4",num_str @{sqrt_square_equation_right_4), |
328 (* a=c*d/sqrt(x) ->a^2=c^2*d^2/x *) |
328 (* a=c*d/sqrt(x) ->a^2=c^2*d^2/x *) |
329 Thm("sqrt_square_equation_right_5",num_str sqrt_square_equation_right_5), |
329 Thm("sqrt_square_equation_right_5",num_str @{sqrt_square_equation_right_5), |
330 (* a=c/e*sqrt(x) ->a^2=c^2/e^2x *) |
330 (* a=c/e*sqrt(x) ->a^2=c^2/e^2x *) |
331 Thm("sqrt_square_equation_right_6",num_str sqrt_square_equation_right_6) |
331 Thm("sqrt_square_equation_right_6",num_str @{sqrt_square_equation_right_6) |
332 (* a=c*d/g*sqrt(x) ->a^2=c^2*d^2/g^2*x *) |
332 (* a=c*d/g*sqrt(x) ->a^2=c^2*d^2/g^2*x *) |
333 ],scr = Script ((term_of o the o (parse thy)) "empty_script") |
333 ],scr = Script ((term_of o the o (parse thy)) "empty_script") |
334 }:rls); |
334 }:rls); |
335 |
335 |
336 ruleset' := overwritelthy thy (!ruleset', |
336 ruleset' := overwritelthy thy (!ruleset', |
341 val l_sqrt_isolate = prep_rls( |
341 val l_sqrt_isolate = prep_rls( |
342 Rls {id = "l_sqrt_isolate", preconds = [], |
342 Rls {id = "l_sqrt_isolate", preconds = [], |
343 rew_ord = ("termlessI",termlessI), |
343 rew_ord = ("termlessI",termlessI), |
344 erls = RootEq_erls, srls = Erls, calc = [], |
344 erls = RootEq_erls, srls = Erls, calc = [], |
345 rules = [ |
345 rules = [ |
346 Thm("sqrt_square_1",num_str sqrt_square_1), |
346 Thm("sqrt_square_1",num_str @{sqrt_square_1), |
347 (* (sqrt a)^^^2 -> a *) |
347 (* (sqrt a)^^^2 -> a *) |
348 Thm("sqrt_square_2",num_str sqrt_square_2), |
348 Thm("sqrt_square_2",num_str @{sqrt_square_2), |
349 (* sqrt (a^^^2) -> a *) |
349 (* sqrt (a^^^2) -> a *) |
350 Thm("sqrt_times_root_1",num_str sqrt_times_root_1), |
350 Thm("sqrt_times_root_1",num_str @{sqrt_times_root_1), |
351 (* sqrt a sqrt b -> sqrt(ab) *) |
351 (* sqrt a sqrt b -> sqrt(ab) *) |
352 Thm("sqrt_times_root_2",num_str sqrt_times_root_2), |
352 Thm("sqrt_times_root_2",num_str @{sqrt_times_root_2), |
353 (* a sqrt b sqrt c -> a sqrt(bc) *) |
353 (* a sqrt b sqrt c -> a sqrt(bc) *) |
354 Thm("sqrt_isolate_l_add1",num_str sqrt_isolate_l_add1), |
354 Thm("sqrt_isolate_l_add1",num_str @{sqrt_isolate_l_add1), |
355 (* a+b*sqrt(x)=d -> b*sqrt(x) = d-a *) |
355 (* a+b*sqrt(x)=d -> b*sqrt(x) = d-a *) |
356 Thm("sqrt_isolate_l_add2",num_str sqrt_isolate_l_add2), |
356 Thm("sqrt_isolate_l_add2",num_str @{sqrt_isolate_l_add2), |
357 (* a+ sqrt(x)=d -> sqrt(x) = d-a *) |
357 (* a+ sqrt(x)=d -> sqrt(x) = d-a *) |
358 Thm("sqrt_isolate_l_add3",num_str sqrt_isolate_l_add3), |
358 Thm("sqrt_isolate_l_add3",num_str @{sqrt_isolate_l_add3), |
359 (* a+b*c/sqrt(x)=d->b*c/sqrt(x)=d-a *) |
359 (* a+b*c/sqrt(x)=d->b*c/sqrt(x)=d-a *) |
360 Thm("sqrt_isolate_l_add4",num_str sqrt_isolate_l_add4), |
360 Thm("sqrt_isolate_l_add4",num_str @{sqrt_isolate_l_add4), |
361 (* a+c/sqrt(x)=d -> c/sqrt(x) = d-a *) |
361 (* a+c/sqrt(x)=d -> c/sqrt(x) = d-a *) |
362 Thm("sqrt_isolate_l_add5",num_str sqrt_isolate_l_add5), |
362 Thm("sqrt_isolate_l_add5",num_str @{sqrt_isolate_l_add5), |
363 (* a+b*c/f*sqrt(x)=d->b*c/f*sqrt(x)=d-a *) |
363 (* a+b*c/f*sqrt(x)=d->b*c/f*sqrt(x)=d-a *) |
364 Thm("sqrt_isolate_l_add6",num_str sqrt_isolate_l_add6), |
364 Thm("sqrt_isolate_l_add6",num_str @{sqrt_isolate_l_add6), |
365 (* a+c/f*sqrt(x)=d -> c/f*sqrt(x) = d-a *) |
365 (* a+c/f*sqrt(x)=d -> c/f*sqrt(x) = d-a *) |
366 (*Thm("sqrt_isolate_l_div",num_str sqrt_isolate_l_div),*) |
366 (*Thm("sqrt_isolate_l_div",num_str @{sqrt_isolate_l_div),*) |
367 (* b*sqrt(x) = d sqrt(x) d/b *) |
367 (* b*sqrt(x) = d sqrt(x) d/b *) |
368 Thm("sqrt_square_equation_left_1",num_str sqrt_square_equation_left_1), |
368 Thm("sqrt_square_equation_left_1",num_str @{sqrt_square_equation_left_1), |
369 (* sqrt(x)=b -> x=b^2 *) |
369 (* sqrt(x)=b -> x=b^2 *) |
370 Thm("sqrt_square_equation_left_2",num_str sqrt_square_equation_left_2), |
370 Thm("sqrt_square_equation_left_2",num_str @{sqrt_square_equation_left_2), |
371 (* a*sqrt(x)=b -> a^2*x=b^2*) |
371 (* a*sqrt(x)=b -> a^2*x=b^2*) |
372 Thm("sqrt_square_equation_left_3",num_str sqrt_square_equation_left_3), |
372 Thm("sqrt_square_equation_left_3",num_str @{sqrt_square_equation_left_3), |
373 (* c/sqrt(x)=b -> c^2/x=b^2 *) |
373 (* c/sqrt(x)=b -> c^2/x=b^2 *) |
374 Thm("sqrt_square_equation_left_4",num_str sqrt_square_equation_left_4), |
374 Thm("sqrt_square_equation_left_4",num_str @{sqrt_square_equation_left_4), |
375 (* c*d/sqrt(x)=b -> c^2*d^2/x=b^2 *) |
375 (* c*d/sqrt(x)=b -> c^2*d^2/x=b^2 *) |
376 Thm("sqrt_square_equation_left_5",num_str sqrt_square_equation_left_5), |
376 Thm("sqrt_square_equation_left_5",num_str @{sqrt_square_equation_left_5), |
377 (* c/d*sqrt(x)=b -> c^2/d^2x=b^2 *) |
377 (* c/d*sqrt(x)=b -> c^2/d^2x=b^2 *) |
378 Thm("sqrt_square_equation_left_6",num_str sqrt_square_equation_left_6) |
378 Thm("sqrt_square_equation_left_6",num_str @{sqrt_square_equation_left_6) |
379 (* c*d/g*sqrt(x)=b -> c^2*d^2/g^2x=b^2 *) |
379 (* c*d/g*sqrt(x)=b -> c^2*d^2/g^2x=b^2 *) |
380 ], |
380 ], |
381 scr = Script ((term_of o the o (parse thy)) "empty_script") |
381 scr = Script ((term_of o the o (parse thy)) "empty_script") |
382 }:rls); |
382 }:rls); |
383 |
383 |
390 val r_sqrt_isolate = prep_rls( |
390 val r_sqrt_isolate = prep_rls( |
391 Rls {id = "r_sqrt_isolate", preconds = [], |
391 Rls {id = "r_sqrt_isolate", preconds = [], |
392 rew_ord = ("termlessI",termlessI), |
392 rew_ord = ("termlessI",termlessI), |
393 erls = RootEq_erls, srls = Erls, calc = [], |
393 erls = RootEq_erls, srls = Erls, calc = [], |
394 rules = [ |
394 rules = [ |
395 Thm("sqrt_square_1",num_str sqrt_square_1), |
395 Thm("sqrt_square_1",num_str @{sqrt_square_1), |
396 (* (sqrt a)^^^2 -> a *) |
396 (* (sqrt a)^^^2 -> a *) |
397 Thm("sqrt_square_2",num_str sqrt_square_2), |
397 Thm("sqrt_square_2",num_str @{sqrt_square_2), |
398 (* sqrt (a^^^2) -> a *) |
398 (* sqrt (a^^^2) -> a *) |
399 Thm("sqrt_times_root_1",num_str sqrt_times_root_1), |
399 Thm("sqrt_times_root_1",num_str @{sqrt_times_root_1), |
400 (* sqrt a sqrt b -> sqrt(ab) *) |
400 (* sqrt a sqrt b -> sqrt(ab) *) |
401 Thm("sqrt_times_root_2",num_str sqrt_times_root_2), |
401 Thm("sqrt_times_root_2",num_str @{sqrt_times_root_2), |
402 (* a sqrt b sqrt c -> a sqrt(bc) *) |
402 (* a sqrt b sqrt c -> a sqrt(bc) *) |
403 Thm("sqrt_isolate_r_add1",num_str sqrt_isolate_r_add1), |
403 Thm("sqrt_isolate_r_add1",num_str @{sqrt_isolate_r_add1), |
404 (* a= d+e*sqrt(x) -> a-d=e*sqrt(x) *) |
404 (* a= d+e*sqrt(x) -> a-d=e*sqrt(x) *) |
405 Thm("sqrt_isolate_r_add2",num_str sqrt_isolate_r_add2), |
405 Thm("sqrt_isolate_r_add2",num_str @{sqrt_isolate_r_add2), |
406 (* a= d+ sqrt(x) -> a-d= sqrt(x) *) |
406 (* a= d+ sqrt(x) -> a-d= sqrt(x) *) |
407 Thm("sqrt_isolate_r_add3",num_str sqrt_isolate_r_add3), |
407 Thm("sqrt_isolate_r_add3",num_str @{sqrt_isolate_r_add3), |
408 (* a=d+e*g/sqrt(x)->a-d=e*g/sqrt(x)*) |
408 (* a=d+e*g/sqrt(x)->a-d=e*g/sqrt(x)*) |
409 Thm("sqrt_isolate_r_add4",num_str sqrt_isolate_r_add4), |
409 Thm("sqrt_isolate_r_add4",num_str @{sqrt_isolate_r_add4), |
410 (* a= d+g/sqrt(x) -> a-d=g/sqrt(x) *) |
410 (* a= d+g/sqrt(x) -> a-d=g/sqrt(x) *) |
411 Thm("sqrt_isolate_r_add5",num_str sqrt_isolate_r_add5), |
411 Thm("sqrt_isolate_r_add5",num_str @{sqrt_isolate_r_add5), |
412 (* a=d+e*g/h*sqrt(x)->a-d=e*g/h*sqrt(x)*) |
412 (* a=d+e*g/h*sqrt(x)->a-d=e*g/h*sqrt(x)*) |
413 Thm("sqrt_isolate_r_add6",num_str sqrt_isolate_r_add6), |
413 Thm("sqrt_isolate_r_add6",num_str @{sqrt_isolate_r_add6), |
414 (* a= d+g/h*sqrt(x) -> a-d=g/h*sqrt(x) *) |
414 (* a= d+g/h*sqrt(x) -> a-d=g/h*sqrt(x) *) |
415 (*Thm("sqrt_isolate_r_div",num_str sqrt_isolate_r_div),*) |
415 (*Thm("sqrt_isolate_r_div",num_str @{sqrt_isolate_r_div),*) |
416 (* a=e*sqrt(x) -> a/e = sqrt(x) *) |
416 (* a=e*sqrt(x) -> a/e = sqrt(x) *) |
417 Thm("sqrt_square_equation_right_1",num_str sqrt_square_equation_right_1), |
417 Thm("sqrt_square_equation_right_1",num_str @{sqrt_square_equation_right_1), |
418 (* a=sqrt(x) ->a^2=x *) |
418 (* a=sqrt(x) ->a^2=x *) |
419 Thm("sqrt_square_equation_right_2",num_str sqrt_square_equation_right_2), |
419 Thm("sqrt_square_equation_right_2",num_str @{sqrt_square_equation_right_2), |
420 (* a=c*sqrt(x) ->a^2=c^2*x *) |
420 (* a=c*sqrt(x) ->a^2=c^2*x *) |
421 Thm("sqrt_square_equation_right_3",num_str sqrt_square_equation_right_3), |
421 Thm("sqrt_square_equation_right_3",num_str @{sqrt_square_equation_right_3), |
422 (* a=c/sqrt(x) ->a^2=c^2/x *) |
422 (* a=c/sqrt(x) ->a^2=c^2/x *) |
423 Thm("sqrt_square_equation_right_4",num_str sqrt_square_equation_right_4), |
423 Thm("sqrt_square_equation_right_4",num_str @{sqrt_square_equation_right_4), |
424 (* a=c*d/sqrt(x) ->a^2=c^2*d^2/x *) |
424 (* a=c*d/sqrt(x) ->a^2=c^2*d^2/x *) |
425 Thm("sqrt_square_equation_right_5",num_str sqrt_square_equation_right_5), |
425 Thm("sqrt_square_equation_right_5",num_str @{sqrt_square_equation_right_5), |
426 (* a=c/e*sqrt(x) ->a^2=c^2/e^2x *) |
426 (* a=c/e*sqrt(x) ->a^2=c^2/e^2x *) |
427 Thm("sqrt_square_equation_right_6",num_str sqrt_square_equation_right_6) |
427 Thm("sqrt_square_equation_right_6",num_str @{sqrt_square_equation_right_6) |
428 (* a=c*d/g*sqrt(x) ->a^2=c^2*d^2/g^2*x *) |
428 (* a=c*d/g*sqrt(x) ->a^2=c^2*d^2/g^2*x *) |
429 ], |
429 ], |
430 scr = Script ((term_of o the o (parse thy)) "empty_script") |
430 scr = Script ((term_of o the o (parse thy)) "empty_script") |
431 }:rls); |
431 }:rls); |
432 |
432 |
437 val rooteq_simplify = prep_rls( |
437 val rooteq_simplify = prep_rls( |
438 Rls {id = "rooteq_simplify", |
438 Rls {id = "rooteq_simplify", |
439 preconds = [], rew_ord = ("termlessI",termlessI), |
439 preconds = [], rew_ord = ("termlessI",termlessI), |
440 erls = RootEq_erls, srls = Erls, calc = [], |
440 erls = RootEq_erls, srls = Erls, calc = [], |
441 (*asm_thm = [("sqrt_square_1","")],*) |
441 (*asm_thm = [("sqrt_square_1","")],*) |
442 rules = [Thm ("real_assoc_1",num_str real_assoc_1), |
442 rules = [Thm ("real_assoc_1",num_str @{real_assoc_1), |
443 (* a+(b+c) = a+b+c *) |
443 (* a+(b+c) = a+b+c *) |
444 Thm ("real_assoc_2",num_str real_assoc_2), |
444 Thm ("real_assoc_2",num_str @{real_assoc_2), |
445 (* a*(b*c) = a*b*c *) |
445 (* a*(b*c) = a*b*c *) |
446 Calc ("op +",eval_binop "#add_"), |
446 Calc ("op +",eval_binop "#add_"), |
447 Calc ("op -",eval_binop "#sub_"), |
447 Calc ("op -",eval_binop "#sub_"), |
448 Calc ("op *",eval_binop "#mult_"), |
448 Calc ("op *",eval_binop "#mult_"), |
449 Calc ("HOL.divide", eval_cancel "#divide_"), |
449 Calc ("HOL.divide", eval_cancel "#divide_"), |
450 Calc ("Root.sqrt",eval_sqrt "#sqrt_"), |
450 Calc ("Root.sqrt",eval_sqrt "#sqrt_"), |
451 Calc ("Atools.pow" ,eval_binop "#power_"), |
451 Calc ("Atools.pow" ,eval_binop "#power_"), |
452 Thm("real_plus_binom_pow2",num_str real_plus_binom_pow2), |
452 Thm("real_plus_binom_pow2",num_str @{real_plus_binom_pow2), |
453 Thm("real_minus_binom_pow2",num_str real_minus_binom_pow2), |
453 Thm("real_minus_binom_pow2",num_str @{real_minus_binom_pow2), |
454 Thm("realpow_mul",num_str realpow_mul), |
454 Thm("realpow_mul",num_str @{realpow_mul), |
455 (* (a * b)^n = a^n * b^n*) |
455 (* (a * b)^n = a^n * b^n*) |
456 Thm("sqrt_times_root_1",num_str sqrt_times_root_1), |
456 Thm("sqrt_times_root_1",num_str @{sqrt_times_root_1), |
457 (* sqrt b * sqrt c = sqrt(b*c) *) |
457 (* sqrt b * sqrt c = sqrt(b*c) *) |
458 Thm("sqrt_times_root_2",num_str sqrt_times_root_2), |
458 Thm("sqrt_times_root_2",num_str @{sqrt_times_root_2), |
459 (* a * sqrt a * sqrt b = a * sqrt(a*b) *) |
459 (* a * sqrt a * sqrt b = a * sqrt(a*b) *) |
460 Thm("sqrt_square_2",num_str sqrt_square_2), |
460 Thm("sqrt_square_2",num_str @{sqrt_square_2), |
461 (* sqrt (a^^^2) = a *) |
461 (* sqrt (a^^^2) = a *) |
462 Thm("sqrt_square_1",num_str sqrt_square_1) |
462 Thm("sqrt_square_1",num_str @{sqrt_square_1) |
463 (* sqrt a ^^^ 2 = a *) |
463 (* sqrt a ^^^ 2 = a *) |
464 ], |
464 ], |
465 scr = Script ((term_of o the o (parse thy)) "empty_script") |
465 scr = Script ((term_of o the o (parse thy)) "empty_script") |
466 }:rls); |
466 }:rls); |
467 ruleset' := overwritelthy thy (!ruleset', |
467 ruleset' := overwritelthy thy (!ruleset', |