Это хорошая идея для расширения стандартных типов и операций? - PullRequest
Новая
       6

Это хорошая идея для расширения стандартных типов и операций?

0 голосов
/ 20 сентября 2018

Мне нужно определить расширенный тип bool (ebool = bool ∪ {⊥}) и набор операций для этого типа (соединение и т. Д.).

Вот теория: 

theory EboolTest
  imports Main "~~/src/HOL/Library/Adhoc_Overloading"
begin

notation
  bot ("⊥")

declare [[coercion_enabled]]

typedef ebool = "UNIV :: bool option set" ..

definition ebool :: "bool ⇒ ebool" where
  "ebool b = Abs_ebool (Some b)"

declare [[coercion "ebool :: bool ⇒ ebool"]]

instantiation ebool :: bot
begin
definition "⊥ ≡ Abs_ebool None"
instance ..
end

free_constructors case_ebool for
  ebool
| "⊥ :: ebool"
  apply (metis Rep_ebool_inverse bot_ebool_def ebool_def not_Some_eq)
  apply (smt Abs_ebool_inverse ebool_def iso_tuple_UNIV_I option.inject)
  by (simp add: Abs_ebool_inject bot_ebool_def ebool_def)

lemmas ebool2_cases = ebool.exhaust[case_product ebool.exhaust]
lemmas ebool3_cases = ebool.exhaust[case_product ebool.exhaust ebool.exhaust]

fun ebool_and :: "ebool ⇒ ebool ⇒ ebool" (infixr "∧" 35) where
  "ebool_and a b = ebool (HOL.conj a b)"
| "ebool_and False _ = False"
| "ebool_and _ False = False"
| "ebool_and ⊥ _ = ⊥"
| "ebool_and _ ⊥ = ⊥"

no_notation HOL.conj (infixr "∧" 35)
consts "(∧)" :: "'a ⇒ 'a ⇒ 'a"
adhoc_overloading "(∧)" HOL.conj
adhoc_overloading "(∧)" ebool_and

end

Следующее работает отлично: 

value "True ∧ (False::ebool)"
value "True ∧ ⊥"

Но следующее возвращает ebool, но я ожидаю увидеть bool: 

value "True ∧ False"

Кажется, мой подход плохой.Не могли бы вы предложить лучший подход?Может я вообще не хорошо перегружать стандартные операции?

1 Ответ

0 голосов
/ 20 сентября 2018

Прежде всего, я немного удивлен, что это: 

consts "(∧)" :: "'a ⇒ 'a ⇒ 'a"

работает вообще.Это звучит как ошибка, потому что нотация (...) зарезервирована для системы.(Честно говоря, это печатает предупреждение, и если вы точно не знаете, что делаете, неразумно их игнорировать.)

Но, возвращаясь к вашей настоящей проблеме, я не думаю, что выследует использовать adhoc_overloading для перегрузки синтаксиса, который в противном случае был бы предоставлен Main.

Существуют альтернативы.Например, вы можете использовать жирную версию.Это используется в этой теории .

Или вы можете использовать другой символ, например &&.

В качестве добавления: я считаю, что между принуждениями могут быть странные взаимодействияи временная перегрузка.Оба инструмента хороши сами по себе, но будьте осторожны, если они взаимодействуют друг с другом.

...