[isabelle] The Symbolic Newton Method

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


and I would like to receive comments, if the case is of interests.


This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.