*To*: cl-isabelle-users at lists.cam.ac.uk*Subject*: Re: [isabelle] Isabelle, Diophantine equations*From*: Tjark Weber <tjark.weber at gmx.de>*Date*: Thu, 28 Jun 2007 16:53:52 +0200*Cc*: Jan Pax <pax0 at seznam.cz>*In-reply-to*: <1444.2613-13609-1233315984-1182497716@seznam.cz>*References*: <1444.2613-13609-1233315984-1182497716@seznam.cz>*User-agent*: KMail/1.8

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

**References**:**[isabelle] Isabelle, Diophantine equations***From:*Jan Pax

- Previous by Date: [isabelle] Problem with recdef (permissive)
- Next by Date: [isabelle] Problem with Isar/Isabelle Induct method
- Previous by Thread: [isabelle] Isabelle, Diophantine equations
- Next by Thread: [isabelle] VerAS: last call for papers
- Cl-isabelle-users June 2007 archives indexes sorted by: [ thread ] [ subject ] [ author ] [ date ]
- Cl-isabelle-users list archive Table of Contents
- More information about the Cl-isabelle-users mailing list