Как преобразовать предикат в функцию в Изабель? - PullRequest
Новая
       15

Как преобразовать предикат в функцию в Изабель?

1 голос
/ 09 марта 2020

В Изабель Холь у меня есть предикат с двумя числами, подобными этому: 

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

Я могу доказать, что этот предикат морально является функцией: 

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

Интуитивно, это должно мне будет достаточно построить функцию f' :: nat ⇒ nat, которая доказуемо эквивалентна f', то есть: 

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

Но как мне это сделать? 

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

Что мне делать? поставить вопросительный знак?

1 Ответ

3 голосов
/ 09 марта 2020

Типичный подход заключается в использовании оператора определенного описания THE: 

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

Если вы уже доказали, что y уникален, вы можете использовать, например, теорему theI' для покажите, что выполняется f x (f' x) и theI_unique, чтобы показать, что если выполняется f x y, то y = f' x.

Для получения дополнительной информации о THE, SOME и т. д. c. см. следующее:

...