Анализ случая определения функции в Изабель - PullRequest
Новая
       13

Анализ случая определения функции в Изабель

0 голосов
/ 14 марта 2020

Представьте, что у меня есть определение функции с тремя случаями: 

function f where 
    eq1 if cond1 
  | eq2 if cond2
  | eq3 if cond3

Как я могу доказать какое-то уравнение: 

f x y = f y x

, используя анализ случая в левой части?

Просто письмо «Применить» (случаи f.cases) не работает для меня Я получаю сообщение об ошибке

Неопределенная константа: "f" ⌂

Ответы [ 2 ]

2 голосов
/ 19 марта 2020

Чтобы дополнить ответ user9716869, вот минимальный рабочий пример: 

function f where
  "f x y = 0" if "x = y" | 
  "f x y = Suc 0" if "x ≠ y"
by auto
termination by lexicographic_order

lemma "f x y = f y x"
proof (cases ‹(x, y)› rule: f.cases)
  case (1 x y)
  then show ?thesis
    by simp
next
  case (2 x y)
  then show ?thesis
    by simp
qed
2 голосов
/ 18 марта 2020

Я решил опубликовать свой комментарий в качестве ответа, пытаясь закрыть эту проблему.

Для вашего случая использования должна быть возможность использования apply(cases ‹(x, y)› rule: f.cases) (или аналогичного). Однако, это поможет увидеть минимальный рабочий пример, прежде чем можно будет это подтвердить.

Для получения дополнительной информации о методе cases см. Раздел 6.5.2 «Методы проверки» в Isar-ref.

...