*To*: Tobias Nipkow <nipkow at in.tum.de>*Subject*: Re: [isabelle] need help with quantified ints*From*: Thomas Arthur Leck Sewell <tsewell at cse.unsw.EDU.AU>*Date*: Mon, 23 Jun 2008 11:26:39 +1000 (EST)*Cc*: isabelle-users <isabelle-users at cl.cam.ac.uk>, Patrice Chalin <chalin at encs.concordia.ca>, Perry James <perry at dsrg.org>*In-reply-to*: <485E8105.3000809@in.tum.de>*References*: <20d5caff0806191432n5f0a77e1q112a7b34154a0e69@mail.gmail.com> <Pine.LNX.4.64.0806202054050.1369@weill.orchestra.cse.unsw.EDU.AU> <485E8105.3000809@in.tum.de>

Perhaps a more direct specialisation to your problem is to use the "int _ <= _" pattern in the helper lemma. Also, as Tobias points out, these helpers can be proven by arith: lemma int_le_val_disj: "m > 0 ==> (int n <= m) = (int n = m | int n <= m - 1)" by arith lemma "int n <= 12 ==> P" apply (simp add: int_le_val_disj) oops A similar trick was used in our project to prove that {0 ..< 5} was equal to {0, 1, 2, 3, 4} - once again, specialisation to the syntactic form in which the < appears was helpful. Yours, Thomas.

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

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

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

- Previous by Date: Re: [isabelle] need help with quantified ints
- Next by Date: [isabelle] Associate Professorship at TUM, Germany
- 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