[isabelle] conversion in Isabelle



Hi all!

I want to prove something like this: g^x=h^y ==> g^(x*inv y)=h, for g and h integers and also h is a power of g.  x and y are integers mod p, p prime. So i can use the fact that inv y=y^(p-2) mod p.
 
If i work with the function power from Power.thy, i need to have natural exponent.  
I also need to be able to apply an inverse function for the exponent. Is there  any other power function or some inverse for naturals mod p=prime?

How is it possible to make conversion in Isabelle? For example if i have (x::int), g^(nat x) doesnt give any error...but what type is (nat x)? If is a bool...then i cannot do operations like : g^(nat x)*g^(nat y)=g^(nat (x+y))...is that right?

Thank you,
stefania



      




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