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

Question

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

IGoogle умные конструкторы, и они, кажется, используются в таких языках, как 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