# Re: [isabelle] Isabelle, Diophantine equations

```Jan,

On Friday 22 June 2007 09:35, Jan Pax wrote:
>   could someone please tell me how to handle Diophantine equations in
> Isabelle and give me some simple example?
>   For example how to try to prove or disprove
>
>      all x, exits y, x^4=y^2
>
>      exists x, exists y, x^4 = 1 + x + y^2
>
>      exists x, exists y, x^2 (1 + y) = 1 + x + y^2

it seems that you haven't received a public reply yet, so I'll try to make
some potentially useful remarks.

- I don't think there's a decision procedure available at the moment which
specifically targets Diophantine equations.  "arith" should be able to deal
with linear ones though: e.g.

lemma "EX (x::int) y. 5*x + 3*y = 1"
by arith

- Addition and power function are generic in Isabelle, available not only for
integers, but also for other types.  Since you consider Diophantine
equations, you'll probably want to use "int" type annotations: e.g.

lemma "ALL (x::int). EX y. x^4 = y^2"

Otherwise use "Isabelle > Settings > Show Types" (and possibly "Isabelle >
Settings > Show Sorts") to show the types inferred by the system.

Here's a proof of the above lemma:

apply (rule allI)
apply (rule_tac x="x^2" in exI)
apply (simp add: power_mult [symmetric])
done

- You can use the "ProofGeneral > Find Theorems" feature to search for
existing lemmas.  E.g. search for theorems containing

"(_ ^ _) ^ _"

to find the "power_mult" theorem (among others) that was used in the above
proof.

- "quickcheck" will try to disprove your current goal by instantiating free
variables with random values.  This means you can also use it to find
witnesses for existential statements, by negating the statement: e.g.

lemma "~ (x::int)^4 = 1 + x + y^2"
quickcheck

might print

Counterexample found:
x = -1::int
y = -1::int

which would suggest the following proof of your second equation:

lemma "EX (x::int) y. x^4 = 1 + x + y^2"
apply (rule_tac x="-1" in exI)
apply (rule_tac x="-1" in exI)
apply simp
done

Likewise for your third equation,

lemma "~ x^2 * (1 + y) = 1 + x + y^2"
quickcheck

might print

Counterexample found:
x = -2::int
y = -1::int

Best,
Tjark

```

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