## Dealing with descriptions in Isabelle/HOL: least, greatest, whatever

[examples

Isabelle

newbies

descriptions

sledgehammer

David Hilbert

]
A description is a term that designates “the least”, “the greatest” or simply “any” *x* such that Φ(*x*): it describes the desired value (or simply *any suitable* value) in the language of its properties.
The built-in facts governing `Min`

, `Max`

, etc. are straightforward, but getting what you want from them is often frustrating.
Let’s take a look at a few contrived, but (I hope) illustrative examples, leaving all the proofs to sledgehammer.

### The range of description operators

A great variety of functions are available. Here are the main ones:

`Least`

/`Greatest`

denote the least/greatest value satisfying a given predicate calculus*formula*. The corresponding Isabelle keyword is`LEAST`

/`GREATEST`

.`Min`

/`Max`

: these functions are suitable for non-empty,**finite**sets. The underlying type must be linearly ordered (belong to type class`linorder`

).`Inf`

/`Sup`

are functions to denote the infimum/supremum of possibly infinite or empty sets. These come in two versions, for complete lattices and for conditionally complete lattices.`Eps`

is Hilbert’s $\epsilon$-operator, which yields the full axiom of choice (AC). The corresponding Isabelle keyword is`SOME`

. Although a*unique*description operator also exists, it has become obsolete: Isabelle/HOL no longer offers the option to work without AC. (That option remains available in Isabelle/ZF.)

Unsurprisingly, some of these are defined in terms of others, with `Eps`

as the base primitive. Type classes play a major role. For example, a type in class `wellorder`

is guaranteed to have suitable `Least`

elements for any non-False predicate.

### A silly theorem statement

The following nonsensical “theorem” will be the basis for a couple of simple examples. We are given a set 𝒮 of nonempty open balls (in a metric space) and a set `L`

of lists of natural numbers.
Our task is to prove something or other.

lemma fixes 𝒮 :: "'a::metric_space set set" and L :: "nat list set" assumes "𝒮 ⊆ {ball x r | x r. r>0}" and "L ≠ {}" shows "P 𝒮 L"

### Example 1: defining the radius and centre of a ball

Every element of 𝒮 has the form `ball x r`

, where `x`

is its centre and `r`

is its necessarily positive radius:

have "⋀B. B ∈ 𝒮 ⟹ ∃x. ∃r>0. B = ball x r" using assms by blast

Whenever you have such a forall-exists fact, you can transform it into exists-forall, obtaining a function. Note that the transformation from $\forall x.\, \exists y.\, \Phi(x,y)$ into
$\exists f.\, \forall x.\, \Phi(x,\,f(x))$ can require AC, in general.
You could define $f$ explicitly using Hilbert’s epsilon, but there’s an easier way.
All you have to do is write out the properties you want, as long as they are clearly based on the previous forall-exists result.
For the proof, simply call `metis`

.
Here, we get two functions at the same time!

then obtain centre rad where rad: "⋀B. B ∈ 𝒮 ⟹ rad B > 0" and centre: "⋀B. B ∈ 𝒮 ⟹ B = ball (centre B) (rad B)" by metis

If you try this and the `metis`

call hangs, it’s likely that your forall-exists formula is too complicated (or just wrong). Simplify it by making definitions.

### Example 2: What is the minimum radius?

The infimum of all the radii of the balls in 𝒮 is easily defined. It exists because there’s a lower bound (zero). The use of the image operator is typical: this is the simplest way to denote the set of all radii of elements of 𝒮.

define infrad where "infrad ≡ Inf (rad ` 𝒮)"

The key property of the infimum is that no other ball in 𝒮 has a smaller radius.

have "infrad ≤ rad B" if "B ∈ 𝒮" for B by (smt (verit, best) bdd_below.I cINF_lower image_iff infrad_def rad that)

It’s possible for the infimum of a set to be strictly smaller than every element; for example, the infimum of the set of positive reals is zero. But if the set is finite and nonempty, its infimum is actually an element.

have "∃B ∈ 𝒮. rad B = infrad" if "finite 𝒮" "𝒮 ≠ {}" by (smt (verit) empty_is_image finite_imageI finite_less_Inf_iff imageE infrad_def that)

### Example 3: Find a list of minimum length

If you want to grab an element minimising some attribute, obtain the minimum value of the attribute first.
Here, we define the minimum of all the lengths of the lists in `L`

.
Note, again, the use of the image operator.

define minl where "minl = Inf (length ` L)"

Now we can obtain an element of `L`

of length `minl`

.
It exists because the set `L`

is non-empty. That set does not have to be finite because *every* set of natural numbers has a least element.

obtain l0 where "l0 ∈ L" "length l0 = minl" by (metis Inf_nat_def1 empty_is_image imageE minl_def ‹L ≠ {}›)

Now we check the key property, namely that the length of `l0`

is minimal among the lengths of every element of `L`

.

then have "length l0 ≤ length l" if "l ∈ L" for l by (simp add: cINF_lower minl_def that)

### Final remarks

Novices often seem to let their formulas get too large. Remember to use definitions to keep your formulas small, especially in situations such as these.
You may wonder whether `minl`

needed to be defined at all, as it’s almost nothing.
And indeed `l0`

can still be obtained, but the proof is an order of magnitude slower: simplicity really matters here.
And just a reminder, **every one** of the proofs above was found by sledgehammer.