Re: [isabelle] the minimum of a set



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 archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.