Re: [isabelle] the minimum of a set



Hi Paqui,

> 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)", .

The issue is that {x. P(x)} might be the empty set, in which case Min
{x. P(x)} is unspecified.   Inspect theorems Min_Un Min_insert
Min_singleton to get an idea how you might proceed from the definition
above.

Hope this helps
	Florian

-- 

PGP available:
http://home.informatik.tu-muenchen.de/haftmann/pgp/florian_haftmann_at_informatik_tu_muenchen_de

Attachment: signature.asc
Description: OpenPGP digital signature



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