Re: [isabelle] solving an equation in isabelle



Kuecuek,

> the important things in the equation are :
> 
> (((y1-y2)^nat (p - 3)) - x1 ) ^3 = .....

There is a new mthod (not yet included in the repository) to solve similar 
problems based on Groebner bases. Yet I do'nt think that it would work for 
these instances. The key questions are:
a) is nat a variable?
b) can you get rid of substraction (-) in your context

If the answer to both is yes, then the method would work for you. 
Unfortunately It might take time to include it.

Otherwise try stuff like ring_eq_simps and add appropriate theorems for 
power.

Aemin.





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