Stream: Archive Mirror: Isabelle Users Mailing List

Topic: [isabelle] Existence and Uniqueness

view this post on Zulip Email Gateway (Aug 22 2022 at 18:32):

From: José Manuel Rodriguez Caballero <josephcmac@gmail.com>
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.

Last updated: Nov 21 2024 at 12:39 UTC