От «значения» до «леммы»

Question

У меня довольно большой срок foo. Когда я типа

value "foo" 

затем Isabelle оценивает foo до значения, скажем foo_value. Теперь я хотел бы доказать следующую лемму.

lemma "foo = foo_value" 

Какой метод доказательства следует использовать? Я попробовал try, но это приурочено. Наверное, я мог бы продолжить вручную, разворачивая различные определения, которые встречаются в foo, но, безусловно, я должен использовать любой механизм, который использует команда value, правильно?

Answer 1

Есть три способа доказательства, которые соответствуют различным механизмам оценочных value:

• eval использует генератор кода; он соответствует value [code]. Доказательство успешно выполняется, если генерируемый код ML оценивается в True.
• normalization компилирует заявление в механизм символической нормализации в ML. Он имитирует value [nbe].
• code_simp использует упроститель Изабель в качестве оценщика. Он соответствует value [simp].

tutorial on code generation более подробно описывает эти методы доказательства. eval и normalization действуют как оракулы, т. Е. Обходят ядро ​​Изабеллы, тогда как каждый этап оценки code_simp проходит через ядро. Обычно eval быстрее, чем normalization и normalization быстрее, чем code_simp.

Answer 2

Я не уверен, работает ли он во всех случаях, но вы можете попробовать:

lemma "foo = foo_value" 
    by eval 

Во многих случаях by simp также должны работать, и я думаю, eval вроде оракула (в том смысле, что не полностью проверено ядром, пожалуйста, кто-нибудь поправьте меня, если я ошибаюсь).