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

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

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

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


design-patterns theorem-proving isabelle
person Rodrigo    schedule 23.10.2018    source источник

Ответы (1)


arrow_upward
0
arrow_downward

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

Вы можете увидеть пример такого поведения в 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
person Rodrigo    schedule 29.10.2018