*To*: John Munroe <munddr at gmail.com>*Subject*: Re: [isabelle] A simple lemma*From*: Makarius <makarius at sketis.net>*Date*: Tue, 8 May 2012 13:15:57 +0200 (CEST)*Cc*: cl-isabelle-users at lists.cam.ac.uk*In-reply-to*: <CAP0k5J4ZWK1q+bBTtoXFBYySjA_7rx7QF87+p0WYB5kaZ_Dwyg@mail.gmail.com>*References*: <CAP0k5J4ZWK1q+bBTtoXFBYySjA_7rx7QF87+p0WYB5kaZ_Dwyg@mail.gmail.com>*User-agent*: Alpine 2.00 (LNX 1167 2008-08-23)

On Mon, 7 May 2012, John Munroe wrote:

I'm having trouble proving the following, could someone please help? axiomatization T :: "real set" and S :: "real set" where ax1: "T = {1,2}" and ax2: "S = {1,2,3}" lemma "ALL t:T. EX s : S. even t <-> s*t=6" I expect it to be true since only 2 in T is even.

Axiomatizations are bad by default; better use a local context. In Isabelle2012 (e.g. RC2) you can do it like this: context fixes T :: "real set" and S :: "real set" assumes ax1: "T = {1,2}" and ax2: "S = {1,2,3}" begin lemma "ALL t:T. EX s : S. even t <-> s*t=6"

Makarius

**References**:**[isabelle] A simple lemma***From:*John Munroe

- Previous by Date: Re: [isabelle] locales and proofs programming bugs
- Next by Date: Re: [isabelle] Dealing with Cases
- Previous by Thread: Re: [isabelle] A simple lemma
- Next by Thread: [isabelle] Dealing with Cases
- Cl-isabelle-users May 2012 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