Re: [isabelle] the minimum of a set



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







This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.