locale - 如何在不收到警告且不使用类型类的情况下重载符号？

Question

首先，在不太了解类型类的情况下，类型类似乎是重载类型符号的最佳方式，除非我不能使用类型类，或者还不知道如何使用。我没有使用类型类。

其次，我很确定我不想覆盖对所有类型都有意义的运算符的符号，例如 \<in> , \<times> , * , \<union>等

但是，像 + 这样的运算符对我的类型没有意义sT ，尽管这与我的第一点有关。我最终想要 +对类型 sT => sT => sT 具有多重含义，我认为这不会发生。

一个例子的四个版本

为了使我的问题具体化并表明我不是唯一遇到问题的人，我从 Klein's course 中举了一个简单的例子。 ，文件为 Demo14.thy .

在示例的四个版本之后，我问，“对于第四个示例，我可以去掉警告吗？”

他从一个没有警告或错误的简单示例开始:

locale semi =
  fixes prod :: "['a, 'a] => 'a" (infixl "\<cdot>" 70)
  assumes assoc: "(x \<cdot> y) \<cdot> z = x \<cdot> (y \<cdot> z)" 

他使用 \<cdot> ，这代表了我到目前为止所做的，没有使用 Isabelle/HOL 已经声明的符号。

我改变了他的\<cdot>至 + ，我得到一个错误:

locale semi2 =
  fixes prod :: "['a, 'a] => 'a" (infixl "+" 70)
  assumes assoc: "(x + y) + z = x + (y + z)"

查看 HOL 源代码后，我看到了 +已为类型定义 ('a => 'a => 'a) ，特别是对于某些类型类。

我修改semi2确保它不是特定于 'a一个人，然后我只收到警告:

locale semi3 =
  fixes prod :: "('a => 'a) => ('a => 'a) => 'a" (infixl "+" 70)
  assumes assoc: "(x + y) + z = x + (y + z)"

我真正关心的是第四个版本，它给出了警告，即使我已经插入了 (x::sT) :

locale semi4 =
  fixes prod :: "sT => sT => sT" (infixl "+" 70)
  assumes assoc: "((x::sT) + y) + z = x + (y + z)"

警告是:

Ambiguous input
produces 16 parse trees (10 displayed):
[...]
Fortunately, only one parse tree is type correct,
but you may still want to disambiguate your grammar or your input.

总结与问题

对于我自己，我总结如下:运算符 +已在许多地方定义，特别是类型 'a => 'a => 'a ，它通常也将其定义为 sT => sT => sT .正因为如此，证明者做了​​很多工作，在最终弄清楚我的 semi4 之后是唯一 + 的地方已为类型定义 sT => sT => sT , 它让我使用它。

我不知道我的摘要，但我可以修复 semi4这样它就不会给我警告？

(注意:根据示例，从数学上讲，使用符号 * 代替 + 更有意义，但 * 是我不想覆盖的符号。)

Answer 1

我想我已经解决了大部分问题。

假设你有一个函数

myFun :: "myT => myT => myT", 

并且您想使用加号 + 作为表示法。

关键是定义+的上下文。在全局层面，至少有两种方式。一种是简单的方法

myFun (infixl "+" 70)

另一种方法是在类型类定义中定义+。特别是在 Groups.thy , 在第 136 行是两行

class plus =
  fixes plus :: "'a \<Rightarrow> 'a \<Rightarrow> 'a"  (infixl "+" 65)

因此，在前言中，简短的回答是，在全局范围内，只有一种方法可以在尝试对 myFun::"myT 使用 + 时消除警告=> myT => myT"，也就是将类型myT实例化为类型类plus，用于函数myFun。

这样做非常简单，我将在此处展示如何做，并且它独立于 Groups.thy 中使用 plus 的所有语言环境和其他类。

但是，在全局级别定义类型 myT 之后，无论是通过简单方式还是通过类型类，尝试为类型 (myT) 再次定义 + => myT => myT) 将在全局级别和语言环境中导致错误。

现在说得通了。重载语法的使用都是基于类型推断，因此特定类型的特定语法只能分配给一个函数。

对于语言环境，+在不同语言环境中的使用是独立的。警告的原因是类型类定义 plus。您无法摆脱语言环境的警告，因为 plus 已被定义为 ('a => 'a => 'a) 的类型类，即全局定义。

这是一些带有注释的代码。为 myT 实例化 plus 需要全部 5 行。

  typedecl myT

--"Two locales can both use '+'. The warning is because '+' has been defined
   in a type class for 'a. If anything defines '+' globally for type myT, these
   locales will give an error for trying to use it."
locale semi1 =
  fixes plus :: "myT => myT => myT" (infixl "+" 70)
  assumes assoc: "((x::myT) + y) + z = x + (y + z)"
locale semi2 =
  fixes plus :: "myT => myT => myT" (infixl "+" 70)
  assumes assoc: "((x::myT) + y) + z = x + (y + z)"


--"DEFINING PLUS HERE GLOBALLY FOR (myT => myT => myT) RESERVES IT EXCLUSIVELY"

definition myFun :: "myT => myT => myT" (infixl "+" 70) where
  "myFun x y = x"
--"Use of 'value' will give a warning if '+' is instantiated globablly prior
   to this point."
value "(x::myT) + y"


--"PLUS HAS BEEN DEFINED ALREADY. SWITCH THIS NEXT SECTION WITH THAT ABOVE AND
    myFun THEN GETS THE ERROR. DELETE myFun AND THE ERROR GOES AWAY."

definition myT_plus_f :: "myT => myT => myT" where
  "myT_plus_f x y = x"

instantiation myT :: plus
begin
  definition plus_myT:
    "x + y = myT_plus_f x y"  --"Error here if '+' globally defined prior to this for type myT."
  instance ..
end
--"No warning here if '+' instantiated for myT; error if '+' defined globablly for
   type myT."
value "(x::myT) + y"


--"ERRORS HERE FOR LOCALES BECAUSE '+' IS DEFINED GLOBALLY"

locale semi3 =
  fixes plus :: "sT => sT => sT" (infixl "+" 70)
  assumes assoc: "((x::sT) + y) + z = x + (y + z)"
locale semi4 =
  fixes plus :: "sT => sT => sT" (infixl "+" 70)
  assumes assoc: "((x::sT) + y) + z = x + (y + z)"