*To*: "Thomas Arthur Leck Sewell" <tsewell at cse.unsw.edu.au>*Subject*: Re: [isabelle] need help with quantified ints*From*: "Perry James" <perry at dsrg.org>*Date*: Fri, 20 Jun 2008 08:17:15 -0400*Cc*: isabelle-users <isabelle-users at cl.cam.ac.uk>, Patrice Chalin <chalin at encs.concordia.ca>*In-reply-to*: <Pine.LNX.4.64.0806202054050.1369@weill.orchestra.cse.unsw.EDU.AU>*References*: <20d5caff0806191432n5f0a77e1q112a7b34154a0e69@mail.gmail.com> <Pine.LNX.4.64.0806202054050.1369@weill.orchestra.cse.unsw.EDU.AU>*Sender*: perry.dsrg at gmail.com

Hi Thomas, Thanks for your reply. The trick in n_less_val_disj will be added to my bag. I've played with variations on it and am not having much luck. The problem I'm having is that the values in my lemma are ints, not nats. Even though n itself is a nat, it is cast to int for the comparisons. Thus all the nice tools for working with the much simpler nats are not available (at least with my limited skills). Best regards, Perry On Fri, Jun 20, 2008 at 7:16 AM, Thomas Arthur Leck Sewell < tsewell at cse.unsw.edu.au> wrote: > Firstly, you can use (case_tac n) instead of (cases n) to do more or less > exactly the same thing, except that n can be a qyantified variable. This > follows a pattern in isabelle, with induct_tac, rule_tac, drule_tac etc > allowing in various ways the specification of a constant that only exists > within the context of the rule. > > Something to think about for your particular case - you're working with an > assumption that a variable is less than a constant, in this case n <= 12. > There's a trick for getting all the cases at once. Oddly, I don't seem to be > able to get it working for <= thisevening, but consider the trick for > 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 > > The reduction to cases can more or less take care of itself. I'm sure > there's a nice way to do this for int n <= 12, but I'll leave you to figure > out what it might be. > > 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" >> >>

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

**Re: [isabelle] need help with quantified ints***From:*Thomas Arthur Leck Sewell

- 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