Как устранить ошибку наследования классов после интерпретации в Изабель? - PullRequest
Новая
       61

Как устранить ошибку наследования классов после интерпретации в Изабель?

1 голос
/ 29 мая 2020

Я получаю сообщение об ошибке, которое я не понимаю в isabelle, когда пытаюсь построить иерархию классов после global_interpretation.

Вот игрушечный нерабочий пример для иллюстрации. 

theory mnwe

imports Main

begin

class natop =
  fixes natop :: "nat \<Rightarrow> 'a \<Rightarrow> 'a"

definition (in natop) list_double :: "'a list \<Rightarrow> 'a list"
  where "list_double xs = map (natop 2) xs"

global_interpretation semiring_1_natop: natop "\<lambda>n x. of_nat n * x"
  defines list_double = semiring_1_natop.list_double
  .

class special_list =
  fixes speclist :: "'a list"

class double_special_list = semiring_1 + special_list +
  assumes "list_double speclist = speclist"

end

Последний класс double_special_list вызывает следующую ошибку: 

Type inference imposes additional sort constraint semiring_1 of type parameter 'a of sort type

А? Класс double_special_list явно наследуется от класса semiring_1 ...

Может ли кто-нибудь объяснить мне, что я делаю неправильно?

Обновление:

Если я опущу class special_list, а вместо этого сделаю 

class double_special_list = semiring_1 +
  fixes speclist :: "'a list"
  assumes "list_double speclist = speclist"

, я получу ошибку 

Type unification failed: Variable 'a::type not of sort semiring_1

, которая снова будет «А?» учитывая спецификацию суперкласса semiring_1.

1 Ответ

0 голосов
/ 30 мая 2020

Хорошо, следующее работает (по крайней мере, не вызывает никаких ошибок), но мне кажется странным со скрытым объявлением суперкласса semiring_1 внутри fixes класса double_special_list. Честно говоря, я не совсем уверен, в чем разница между кодом в моем вопросе и кодом в этом ответе, и почему первый из них является ошибкой, но вот вы go. 

theory answer

imports Main

begin

class natop =
  fixes natop :: "nat \<Rightarrow> 'a \<Rightarrow> 'a"

definition (in natop) list_double :: "'a list \<Rightarrow> 'a list"
  where "list_double xs = map (natop 2) xs"

global_interpretation semiring_1_natop: natop "\<lambda>n x. of_nat n * x"
  defines list_double = semiring_1_natop.list_double
  .

class double_special_list =
  fixes speclist :: "'a::semiring_1 list"
  assumes "list_double speclist = speclist"

lemma test:
  fixes a b c :: "'a::double_special_list"
  shows "a * (b + c) = a * b + a * c"
  by (simp add: algebra_simps)

end
...