*To*: Perry James <perry at dsrg.org>*Subject*: Re: [isabelle] need help with quantified ints*From*: Thomas Arthur Leck Sewell <tsewell at cse.unsw.EDU.AU>*Date*: Fri, 20 Jun 2008 21:16:17 +1000 (EST)*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>

n < 12: lemma n_less_val_disj: "m ~= (0 :: nat) ==> (n < m) = (n = m - 1 | n < m - 1)" apply (case_tac n, simp_all) apply fastsimp apply (case_tac m, simp_all) apply fastsimp done lemma test_this: "n < (12 :: nat) ==> P" apply (simp add: n_less_val_disj) oops

Yours, Thomas. On Thu, 19 Jun 2008, 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"

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

**Re: [isabelle] need help with quantified ints***From:*Tobias Nipkow

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

- Previous by Date: [isabelle] Herlihy, Milner, Hoare, O'Hearn etc.: LASER summer school
- Next by Date: Re: [isabelle] need help with quantified ints
- Previous by Thread: [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