Email Gateway (Aug 22 2022 at 18:32): Email Gateway (Aug 22 2022 at 18:32):From: Manuel Eberl <eberlm@in.tum.de>
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
pEpkey.asc
Last updated: Apr 26 2024 at 20:16 UTC