[isabelle] Existence and Uniqueness

[José Manuel Rodriguez Caballero]

Hello,
Recently, I proved that there exists a unique function satisfying certain
condition. More precisely,

theorem DyckExistsUniq :
‹∃! f :: nat ⇒ DCHR list. (f 0 = [])∧(∀ n. n ≥ 1 ⟶ n ∈ DyckClass (f n) ∧
DyckPath (f n))›

Reference:
https://github.com/josephcmac/Folklore-and-miscellaneous-results-in-number-theory/blob/master/DyckPathOfANumberExistenceUniq.thy

It would be nice to use this function f as any other function defined in
Isabelle/HOL, e.g.,

definition f :: "nat => DCHR list" ...

or

fun f :: "nat => DCHR list" ...

Is there a way to give a fixed name to this function f in order to use it
without mentioning theorem DyckExistsUniq all the times?

Kind Regards,
Jose M.

[Manuel Eberl]

You can use the unique choice operator "The". You can write something
like "THE x. P x", and that gives you the unique value x for which P
holds, or something undefined if no such value exists.

If you've already proven unique existence (with ∃!), there are a few
theorems (theI', the1_equality) that you can use to get the properties
you want.

There is also the general choice combinator "Some" (Hilbert's epsilon
operator) for cases where the value being chosen is not unique.


There is also the "specification" command which allows you to do pretty
much to the same thing: Convert an existence proof into an actual value.
The following example defines a "n-th prime" function:

consts f :: "nat ⇒ nat"

specification (f)
  prime_f: "prime (f n)"
  card_primes_less_f: "card {q. prime q ∧ q < f n} = n"
(* proof *)

The specification command is basically a small wrapper around the choice
operator "Some", as can be seen by inspecting f_def after it. Frankly, I
don't see it being used very often these days, and it only works on the
toplevel, not inside proofs. So I personally usually just use "The" or
"Some" directly.

Manuel

Post by José Manuel Rodriguez Caballero
Hello,
Recently, I proved that there exists a unique function satisfying certain
condition. More precisely,
‹∃! f :: nat ⇒ DCHR list. (f 0 = [])∧(∀ n. n ≥ 1 ⟶ n ∈ DyckClass (f n) ∧
DyckPath (f n))›
https://github.com/josephcmac/Folklore-and-miscellaneous-results-in-number-theory/blob/master/DyckPathOfANumberExistenceUniq.thy
It would be nice to use this function f as any other function defined in
Isabelle/HOL, e.g.,
definition f :: "nat => DCHR list" ...
or
fun f :: "nat => DCHR list" ...
Is there a way to give a fixed name to this function f in order to use it
without mentioning theorem DyckExistsUniq all the times?
Kind Regards,
Jose M.