From: Michael Foster <jmafoster1@sheffield.ac.uk>

Hello,

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.

Best,

Michael F.

From: Manuel Eberl <eberlm@in.tum.de>

Hello,

this can be expressed fairly naturally with the "is_arg_min" construct

from the library, then you don't have to prove anything.

lemma

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

Cheers,

Manuel

From: Tobias Nipkow <nipkow@in.tum.de>

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.

Tobias

smime.p7s

From: Michael Foster <jmafoster1@sheffield.ac.uk>

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