Email Gateway (Aug 18 2022 at 13:13): Email Gateway (Aug 18 2022 at 13:13):From: Jens Doll <jd@cococo.de>
Symbolic computing might be the base for the next computer generation. It
also means having more powerful hardware. I recently came across the
symbolic newton method for rational functions, which is an iteration,
where the initial value is not known and which is carried out
symbolically. The resulting expression grows exponentially for nonlinear
functions and soon exceeds machine power. I now wonder, if the resulting
expression could be reduced by some Isabelle tactics, The sample can be
found under
http://cococo.de/products/windows/Columbo/sample4.html
and I would like to receive comments, if the case is of interests.
Jens
Email Gateway (Aug 18 2022 at 13:14):From: Tjark Weber <webertj@in.tum.de>
Jens,
I'd try "apply simp", or perhaps "apply auto". Various useful
theorems, e.g., "0 * a = 0", are installed as simplification
rules by default. Others may have to be added manually.
If you only care about simplification, rather than theorem
proving, a computer algebra system (such as Maple) might be
the better tool for this task.
Regards,
Tjark
Last updated: May 03 2024 at 08:18 UTC