Лучше ли построить сублокаль из класса или локали? - PullRequest
Новая
       6

Лучше ли построить сублокаль из класса или локали?

0 голосов
/ 15 февраля 2019

Я в замешательстве. 

class Nonde_choice=
fixes nodt :: " 'a ⇒ 'a ⇒ 'a" (infixl "⊓" 70)
  assumes  commutative [simp]: "(x ⊓ y) = (y ⊓ x)"
    and associative [simp]: "((x ⊓ y) ⊓ z) = (x ⊓ (y ⊓ z))"
    and idempotent [simp]: "(x ⊓ x)= x"
sublocale  nonde_choice: comm_monoid_set Nonde_choice neutral_element_for_nonde_choice
  defines nonde_choice = nonde_choice.F ..

Все нормально. Далее просто доказательство. И, 

locale Nonde_choice=
fixes nodt :: " 'a ⇒ 'a ⇒ 'a" (infixl "⊓" 70)
  assumes  commutative [simp]: "(x ⊓ y) = (y ⊓ x)"
    and associative [simp]: "((x ⊓ y) ⊓ z) = (x ⊓ (y ⊓ z))"
    and idempotent [simp]: "(x ⊓ x)= x"
sublocale  nonde_choice: comm_monoid_set Nonde_choice neutral_element_for_nonde_choice
  defines nonde_choice = nonde_choice.F ..

затем, предупреждение и вывод: 

Type unification failed: Clash of types "bool" and "_ ⇒ _"
Failed to meet type constraint:
Term:  Nonde_choice :: (??'a ⇒ ??'a ⇒ ??'a) ⇒ bool
Type:  (??'a ⇒ ??'a ⇒ ??'a) ⇒ (??'a ⇒ ??'a ⇒ ??'a) ⇒ ??'a ⇒ ??'a ⇒ ??'a

Я предпочитаю первый случай. Но если я выбираю первую ситуацию. Затем мне нужно изменить другие операции.Потому что ifjudge сообщает об ошибке: 

Type error in application: incompatible operand type

Operator:  (⊓) :: ??'a ⇒ ??'a ⇒ ??'a
Operand:   a :* x :: 'a

мои другие операторы: 

locale newoperation =
  fixes  next_two :: "'b ⇒ 'a ⇒ 'a" (infixl ":*" 70)
    and  compl :: "'b ⇒ 'b"  ("¬* _" [40] 40)
  assumes doucompl[simp]: "(¬* (¬* x)) = x"

locale ifjudge = newoperation + Nonde_choice +
  fixes ifte :: "'b ⇒'a ⇒ 'a ⇒ 'a"
  assumes  negate [simp]: "ifte a x y = (a :* x) ⊓ ((¬* a) :* y)"

Кажется, я не очень понимаю разницу между языком и классом. Я надеюсь, что кто-то может дать мненесколько советов.Заранее спасибо.

...