Как доказать эту простую теорему в Изабель?

Question

Я определяю очень простую функцию replace, которая заменяет 1 на 0 при сохранении других входных значений. Я хочу доказать, что вывод функции не может быть 1. Как этого добиться?

Вот код.

theory Question
  imports Main
begin
fun replace :: "nat ⇒ nat" where
"replace (Suc 0) = 0" |
"replace x = x"

theorem no1: "replace x ≠ (Suc 0)"
  sorry
end

Спасибо!

Answer 1

Существует несколько подходов для доказательства утверждения, которое вы пытаетесь доказать.

---

Вы можете попытаться использовать sledgehammer для автоматического поиска доказательства, например,

theorem no1: "replace x ≠ (Suc 0)"
  by sledgehammer
  (*using replace.elims by blast*)

Как только доказательство будет найдено, вы можете удалить явный вызов команды sledgehammer.

Возможно, несколько лучшим способом указать доказательство, найденное sledgehammer, будет

theorem no1': "replace x ≠ (Suc 0)"
  by (auto elim: replace.elims)

---

Вы также можете попытаться предоставить более специализированное доказательство. Например,

theorem no1: "replace x ≠ (Suc 0)"
  by (cases x rule: replace.cases) simp_all

В этом доказательстве рассматриваются различные случаи, которые может иметь значение x, а затем используется упрощение (в сочетании с простыми правилами, предоставленными командой fun во время определения вашего функция) до конца sh доказательство. Вы можете увидеть все теоремы, которые сгенерированы командой fun, введя print_theorems сразу после спецификации replace, например

fun replace :: "nat ⇒ nat" where
  "replace (Suc 0) = 0" |
  "replace x = x"

print_theorems 

---

Конечно, есть и другие способы доказать результат, который вы пытаетесь доказать. Хороший способ улучшить вашу способность находить такие доказательства - прочитать документацию и учебные пособия по Изабель. Моей собственной отправной точкой для изучения Изабель была книга "Конкретная семантика" Тобиаса Нипкова и Джервина Кляйна.