*To*: Paqui <paqui.lucio at ehu.es>*Subject*: Re: [isabelle] the minimum of a set*From*: "Gergely Buday" <gbuday at gmail.com>*Date*: Tue, 4 Mar 2008 11:22:05 +0100*Cc*: cl-isabelle-users at lists.cam.ac.uk*In-reply-to*: <003301c87d55$1120e600$65a0e30a@X1Paqui>*References*: <003301c87d55$1120e600$65a0e30a@X1Paqui>

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

**Follow-Ups**:**Re: [isabelle] the minimum of a set***From:*Paqui Lucio

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

- Previous by Date: [isabelle] Russell'08, final call, extended deadline
- Next by Date: Re: [isabelle] the minimum of a set
- Previous by Thread: [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