Email Gateway (Aug 18 2022 at 11:29): Email Gateway (Aug 18 2022 at 11:29):From: Florian Haftmann <florian.haftmann@informatik.tu-muenchen.de>
Hi Paqui,
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
signature.asc
Email Gateway (Aug 18 2022 at 11:30):From: Gergely Buday <gbuday@gmail.com>
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.
Email Gateway (Aug 18 2022 at 11:30):From: Paqui Lucio <paqui.lucio@ehu.es>
El mar, 04-03-2008 a las 11:22 +0100, Gergely Buday escribió:
This was what I suspected first, but
have "\<not>({x. P(x)} = {})" by auto
gives successfully:
have {x. P(x)} ~= {}
Regards,
Paqui
Email Gateway (Aug 18 2022 at 11:30):From: Florian Haftmann <florian.haftmann@informatik.tu-muenchen.de>
Even then you need finiteness to proceed, e.g.:
fix P :: "'a::linorder => bool"
have "{x. P x} ~= {}" sorry
then obtain x xs where "{x. P x} = insert x xs" by blast
moreover have "finite xs" sorry
ultimately have "Min {x. P x} <= x" by auto
Hope this helps
Florian
florian.haftmann.vcf
signature.asc
Email Gateway (Aug 18 2022 at 11:37):From: Paqui <paqui.lucio@ehu.es>
Hi,
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)", .
Please, some help?,
Paqui
Paqui Lucio
Basque Country University
Spain
Last updated: May 03 2024 at 04:19 UTC