Stream: Mirror: Isabelle Users Mailing List

Topic: [isabelle] List minimality proof

view this post on Zulip Email Gateway (Aug 25 2020 at 08:49):

From: Michael Foster <>

As part of a larger project, I have proved what I am calling for want of
a better name "list minimality". That is, if there exists a list l which
satisfies a property P, then there exists a shortest list which
satisfies that property. This particular proof is very useful to me, and
I was somewhat surprised that it had not already been proven. I
therefore thought that it might be of use generally, and wondered
whether there was any possibility of it being included into List.thy?
The proof is quite short (less than 100 lines including all sub-lemmas) 
and I am happy to send it to whoever may be interested.

As an aside, I think I could extend the minimality property to ordered
datatypes reasonably easily and prove that, if there exists an element
which satisfies a given property, there exists a minimal element. I
would be happy to have a go at this if people think this is worthwhile,
and make the proof generally available if I succeed.


Michael F.

view this post on Zulip Email Gateway (Aug 25 2020 at 08:53):

From: Manuel Eberl <>

this can be expressed fairly naturally with the "is_arg_min" construct
from the library, then you don't have to prove anything.

fixes P :: "'a list ⇒ bool"
assumes "∃xs. P xs"
shows "∃xs. is_arg_min length P xs"
using assms is_arg_min_arg_min_nat by metis



view this post on Zulip Email Gateway (Aug 25 2020 at 08:58):

From: Tobias Nipkow <>
The lemma

lemma ex_has_least_nat: "P k ⟹ ∃x. P x ∧ (∀y. P y ⟶ m x ≤ m y)"
for m :: "'a ⇒ nat"

expresses this in greater generality. In your case, m is length.


view this post on Zulip Email Gateway (Aug 26 2020 at 08:26):

From: Michael Foster <>
Both of those are nice proofs. As I said, I was surprised that it hadn't
already been proven - turns out it has! Thanks for pointing me in the
right direction.

Michael F.

Last updated: Sep 25 2021 at 09:17 UTC