Isabelle中interpretation后如何使用locale内定义的函数与术语

Isabelle 中的普通 locale 不属于类型系统的 sort 范畴，因此无法直接放在类型约束位使用，以下提供两种符合你需求的实现方式：

方案1：使用多参数类型类（匹配Haskell多参数typeclass使用习惯） #

Isabelle 原生支持多参数类型类，你可以直接将原locale改写为类定义，即可使用你想要的类型约束语法：

(* 定义多参数类型类 *)
class myclass =
  fixes name :: "'a => 'b"
    and params :: "'a => 'p"
begin
fun equalParams :: "'a => 'a => bool" where
"equalParams a b = (params a = params b)"
end

(* 给你的自定义类型实现该类 *)
instantiation actionT1 :: (type, type, type) myclass
begin
definition name_actionT1 :: "('b, 'c, 'd) actionT1 => 'b" where
"name_actionT1 = name" (* 复用datatype自带的name选择子 *)
definition params_actionT1 :: "('b, 'c, 'd) actionT1 => 'c * 'd" where
"params_actionT1 a = (c a, d a)"
instance by intro_classes (* 完成实例化证明 *)
end

(* 此时就可以使用你期望的类型约束写法定义函数 *)
fun f :: "'a :: myclass => 'b" where
"f a = name a"

此时只要类型变量标注了:: myclass约束，就可以直接调用类中定义的name、params、equalParams等所有函数，和Haskell多参数类型类的使用逻辑一致。

方案2：保留locale结构，将通用函数定义在locale内部 #

如果你需要使用locale的复杂扩展能力（比如额外的公理假设、子locale继承等），不需要改动现有locale定义，只需把你要写的通用函数放在locale内部即可：

locale mylocale =
   fixes name :: "'a => 'b"
     and params :: "'a => 'p"
begin
fun equalParams :: "'a => 'a => bool" where
"equalParams a b = (params a = params b)"

(* 所有通用函数直接在locale内部定义，自动可调用locale内的其他函数 *)
fun f :: "'a => 'b" where
"f a = name a"
end

完成你原有的interpretation操作后，就可以直接调用实例化后的函数：

• 命名interpretation下用action.f调用，对应('b,'c,'d) actionT1 => 'b类型
• 未命名interpretation下直接用f调用即可

内容的提问来源于stack exchange，提问作者Kookie