*To*: Gergely Buday <gbuday at gmail.com>*Subject*: Re: [isabelle] the minimum of a set*From*: Paqui Lucio <paqui.lucio at ehu.es>*Date*: Tue, 04 Mar 2008 11:55:14 +0100*Cc*: cl-isabelle-users at lists.cam.ac.uk*In-reply-to*: <90d975d30803040222gc5d9bf4w9040b2d3cee5140a@mail.gmail.com>*Organization*: UPV/EHU*References*: <003301c87d55$1120e600$65a0e30a@X1Paqui> <90d975d30803040222gc5d9bf4w9040b2d3cee5140a@mail.gmail.com>*Reply-to*: paqui.lucio at ehu.es

El mar, 04-03-2008 a las 11:22 +0100, Gergely Buday escribió: > On 03/03/2008, Paqui <paqui.lucio at ehu.es> wrote: > > In a proof in Isabelle/HOL, > > I have defined i = Min {x. P(x)}. > > Next, I try to prove that P(i) holds or even that i\<in> Min {x. P(x)} and > > I cannot neither "by auto", nor "by (auto! simp add: Min_def)", > > nor "by (auto! simp add: Min_in)", . > > I guess the problem is that P(x) might not hold for any element, i.e. > the set defined by this predicate can be empty. Then the value of i is > "undefined", so you cannot prove such things about it. > > - Gergely This was what I suspected first, but have "\<not>({x. P(x)} = {})" by auto gives successfully: have {x. P(x)} ~= {} Regards, Paqui -- Paqui Lucio Facultad de Informática Universidad del País Vasco SPAIN

**Follow-Ups**:**Re: [isabelle] the minimum of a set***From:*Florian Haftmann

**References**:**[isabelle] the minimum of a set***From:*Paqui

**Re: [isabelle] the minimum of a set***From:*Gergely Buday

- Previous by Date: Re: [isabelle] the minimum of a set
- Next by Date: [isabelle] Separating function declaration from implementation
- Previous by Thread: Re: [isabelle] the minimum of a set
- Next by Thread: Re: [isabelle] the minimum of a set
- Cl-isabelle-users March 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