Умный образец конструктора во время прувинга с Изабель

Question

Во время изучения главы 3 " Конкретная семантика" мой инструктор упомянул, что некоторые функции были построены с использованием шаблона "умный конструктор", и заявил, что этот шаблон полезен для доказательства теорем.

Я гуглил умных конструкторов, и они, кажется, используются в таких языках, как Haskell, с которыми я не знаком. Кроме того, в доказательстве теорем не так много ссылок на умных конструкторов.

Итак, что такое шаблон умного конструктора в Изабель и как он может помочь в доказательстве теорем? Может быть, вы даже можете объяснить это с главой 3 книги...

Answer 1

Таким образом, паттерн в основном состоит в определении и доказательстве сложных случаев использования функций в отдельных функциях, а затем объединении их в основную функцию. Это, конечно, облегчит доказательство.

Вы можете увидеть пример этого поведения в AExp.thy из учебника. Упрощенная функция:

fun plus :: "aexp ⇒ aexp ⇒ aexp" where
"plus (N i1) (N i2) = N(i1+i2)" |
"plus (N i) a = (if i = 0 then a else Plus (N i) a)" |
"plus a (N i) = (if i = 0 then a else Plus a (N i))" |
"plus a1 a2 = Plus a1 a2"

Некоторые теоремы о простой функции:

lemma aval_plus [simp]:
  "aval (plus a1 a2) s = aval a1 s + aval a2 s"
apply(induction a1 a2 rule: plus.induct)
apply auto
done

Сочетание фактов находится в:

fun asimp :: "aexp ⇒ aexp" where
"asimp (N n) = N n" |
"asimp (V x) = V x" |
"asimp (Plus a1 a2) = plus (asimp a1) (asimp a2)"

и окончательное доказательство проще:

theorem aval_asimp[simp]:
  "aval (asimp a) s = aval a s"
apply(induction a)
apply (auto)
done