Re: [isabelle] need help



The following theorems may be of some use:
  IntDiv.zmod_zadd_left_eq
  IntDiv.zmod_zadd_right_eq
  IntDiv.zmod_zmult1_eq
  IntDiv.zmod_zmult1_eq'
  IntDiv.zpower_zmod

In particular, you can use them to prove congruence rules for modular 
arithmetic, such as:
[| x mod p = x' mod p; y mod p = y' mod p |]
 ==> (x + y) mod p = (x' + y') mod p

and similarly for subtraction, multiplication and exponentiation. I'm not sure 
if this will give you everything you want, but at least this should allow you 
to remove the inner mod operations from your subgoals.

- Brian

On Wednesday 06 December 2006 08:55, kuecuek at rbg.informatik.tu-darmstadt.de 
wrote:
> hallo,
>
> i try to solve an equation but it is realy complex can anybody help me?
> if i try with numbers then i can show it with "auto" but if i use variables
> then i can not proof it.
>
>
> the equations below are given
>
> y1 ^2 = x1 ^3 + a*x1 + b
> y2 ^2 = x2 ^ 3 + a*x2 + b
>
> and
>
> x3 =  ((((y1 - y2) *  ((x1 - x2) ^ nat (p -2 ))) mod p) ^ 2 - x1 - x2) mod
> p y3 = ((((y1 - y2) *  ((x1 - x2) ^ nat (p -2 ))) mod p) * (x1 - x3) - y1)
> mod p
>
>
> and i must to show that y3^2 = x3^3 + a*x3 + b
>
> if you put the definitionof y3 and x3 in last equation you would see how
> complex it is :(
>
> can anybody give a trick to proof something like that?
>
> thanks a lot





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