Email Gateway (Aug 18 2022 at 12:41): Email Gateway (Aug 18 2022 at 12:41):From: barzan stefania <stefania_barzan@yahoo.com>
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
Email Gateway (Aug 18 2022 at 12:41):From: Tobias Nipkow <nipkow@in.tum.de>
How is it possible to make conversion in Isabelle?
You apply a conversion function. The basic ones are
nat :: int => nat
int :: nat => int
real :: 'a => real
Warning: nat(i) = 0 if i<0.
For example if i have (x::int), g^(nat x) doesnt give any error...but what type is (nat x)?
nat.
Tobias
Last updated: May 03 2024 at 04:19 UTC