[isabelle] conversion in Isabelle
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?
This archive was generated by a fusion of
Pipermail (Mailman edition) and