Isabelle: Есть ли разница между использованием аксиоматизации и типа данных для конструкторов

Question

Основном Есть два способа определить конструктор для моего типа данных:

typedecl basicTest 
datatype test= af basicTest | plus test test (infixl "+" 35) 

или я использую аксиоматизацию:

typedecl basicTest 
datatype test= af basicTest 
axiomatization 
plus :: "test ⇒ test ⇒ test " (infixl "+" 35) 

Я блаженно не подозревая о каких-либо различиях, но я думаю, что есть некоторые: D

Answer 1

Есть много отличий. Только первый дает вам правильный принцип индукции для вашего типа данных, леммы, которые гарантируют, что plus a b что-то отличается от af b и позволит вам определять функции путем сопоставления шаблонов по af и plus.

Последний действительно определяет test как тип, изоморфный basicTest, и утверждает, что на нем существует неопределенная функция plus.

Иными словами, два определения определяют очень разные типы (и аксиоматизация plus не меняет тип).

Answer 2

Как правило, команда print_theorems может использоваться после некоторой команды спецификации, чтобы определить, какие из них являются соответствующими теоремами, которые характеризуют вновь введенные логические сущности. В качестве альтернативы, IDE Prover предоставляет панель запроса с «Контекст/теоремы печати».

Для вышеуказанных typedecl и axiomatization (без фактических аксиом) результат пуст.

Для datatype вы получаете множество фактов, которые могут быть использованы позже в ваших доказательствах.

Побочные примечания:

• верблюжьей случае не используется в Изабеллу, words_are_separated_by_underscore
• имена типов, наиболее константные имена и т.д. в lower_case (главное исключение: Тип данных Конструкторы капитализируются)
• (как правило, обычно сингулярно)