*To*: "Perry James" <perry at dsrg.org>*Subject*: Re: [isabelle] need help with quantified ints*From*: John Matthews <matthews at galois.com>*Date*: Fri, 20 Jun 2008 07:07:27 -0700*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>

Hi Perry,

-john On Jun 19, 2008, at 2:32 PM, 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 theassumption,but that's not possible since n is bound. Also, applying arith,algebra, andauto have no effect. Is there any way to make progress? Thanks in advance, Perrylemma " !! q qa n. [| 0 < n; int n <= 12; int n * q = 12; int n * qa= 18 |]==> int n <= 6"

**Follow-Ups**:**Re: [isabelle] need help with quantified ints***From:*Makarius

**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