Search code examples
isabelle

How do I convert a predicate to a function in Isabelle?

In Isabelle HOL, I have a predicate on two numbers like this: 

definition f :: "nat ⇒ nat ⇒ bool"
  where 
    ...

I can prove that this predicate is morally a function:

lemma f_function:
  fixes x :: nat
  shows "∃! y . f x y""
  ...

Intuitively, this should be enough for me to construct a function f' :: nat ⇒ nat that is provably equivalent to f', i.e.:

lemma f'_correct:
  "f x y = (f' x = y)"

But how do I do that?

definition f' :: "nat ⇒ nat"
  where
    "f' x ≡ ?"

What do I put in for the question mark?

Solution

  • The typical approach is to use the definite description operator THE:

    definition f' :: "nat ⇒ nat" where "f' x = (THE y. f x y)"

    If you have already proven that this y is unique, you can then use e.g. the theorem theI' to show that f x (f' x) holds and theI_unique to show that if f x y holds, then y = f' x.

    For more information about THE, SOME, etc. see the following: