*To*: Perry James <perry at dsrg.org>*Subject*: Re: [isabelle] need help with quantified ints*From*: Amine Chaieb <chaieb at in.tum.de>*Date*: Fri, 20 Jun 2008 14:24:11 +0200*Cc*: isabelle-users <isabelle-users at cl.cam.ac.uk>, Patrice Chalin <chalin at encs.concordia.ca>*In-reply-to*: <20d5caff0806191432n5f0a77e1q112a7b34154a0e69@mail.gmail.com>*References*: <20d5caff0806191432n5f0a77e1q112a7b34154a0e69@mail.gmail.com>*Sender*: Amine Chaieb <chaieb.amine at googlemail.com>*User-agent*: Thunderbird 1.5.0.8 (Macintosh/20061025)

Here is a proof: lemma fixes q qa n assumes n0: "n > 0" and n12: "int n <= 12" and nq: "int n * q = 12" and nqa: "int n * qa = 18" shows "int n <= 6" proof- from nq nqa have "int n dvd 12" "int n dvd 18" unfolding dvd_def by auto hence th: "n dvd 12" "n dvd 18" unfolding int_dvd_iff by auto from gcd_greatest[OF th] have "n dvd 6" by (simp add: gcd.simps) (* This is actually stronger than the final conclusion *) hence "n <= 6" by (rule dvd_imp_le, simp) then show "int n <= 6" by simp qed

Hope it helps, Amine. Perry James wrote:

Hi, I'm having trouble proving the lemma below. My first idea was to "apply (cases n)" since there are only 12 values of n that satisfy the assumption, but that's not possible since n is bound. Also, applying arith, algebra, and auto have no effect. Is there any way to make progress? Thanks in advance, Perry lemma " !! q qa n. [| 0 < n; int n <= 12; int n * q = 12; int n * qa = 18 |] ==> int n <= 6"

**References**:**[isabelle] need help with quantified ints***From:*Perry James

- Previous by Date: Re: [isabelle] need help with quantified ints
- Next by Date: Re: [isabelle] need help with quantified ints
- Previous by Thread: Re: [isabelle] need help with quantified ints
- Next by Thread: Re: [isabelle] need help with quantified ints
- Cl-isabelle-users June 2008 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