Isabelle中Mixfix annotations的注意点

第一：作为运算符的符号选择

同样方法的用locale声明的一段抽象代数的运算，第一个是没有问题的的，第二个就不可以。这两段的不同在于其中的星号“*”，虽然在图1中看起来一样，但在实际代码里面，两个星号是不一样的。

下面是代码：

locale semigroup =
  fixes f :: "'a ⇒ 'a ⇒ 'a"  (infixl "❙*" 70)
  assumes assoc [simp]: "a ❙* b ❙* c = a ❙* (b ❙* c)"

locale semigroups =
  fixes f :: "'a ⇒ 'a ⇒ 'a"  (infixl "*" 70)
  assumes assoc [simp]: "a * b * c = a * (b * c)"

第二段的报错为：

Ambiguous input
2 terms are type correct:
  (((a * b) * c) = (a * (b * c)))
  (((a * b) * c) = (a * (b * c)))
Failed to parse prop

有歧义的输入，但在报错里面给我们的有歧义的两种情况看起来一样。是这样的，在你引用的theory中，第二个星号已经被定义过，所以当你在你自己的theory再次使用的时候就会产生歧义。
解决的方法1：换一个在引用的theory中没有用过的符号；
解决的方法2：在自己theory中将这个有已经定义过得符号去掉，用no_notation这个命令。

但是在第二的方法，有一点不足：当你在理论A中删掉了""在main理论中的含义，但你在理论B同时引用理论A和其他从main理论中得来（没有删去“”）的理论，则在理论B中则会产生歧义。