Isabelle中类导入locale的方法及多类型类假设复用问题咨询

我在开发自己的locale时也遇到过类似的需求，下面分享几个实用的方法来解决你提到的两个核心问题：

一、将类导入Locale并复用其定理 #

其实Isabelle/HOL里有几种简便的方式把类的约束和定理引入到locale中：

• 直接在类型变量上添加类约束：定义locale时，给类型变量加上类的限定，比如你想复用semigroup类的定理，可以这么写：

  locale my_semigroup_locale =
    fixes op :: "'a :: semigroup ⇒ 'a ⇒ 'a"
    assumes custom_assumption: "op x (op y z) = op (op x y) z"
  

  这样在这个locale内部，你可以直接引用semigroup类的所有预定义定理，比如semigroup.assoc，不需要额外导入步骤。
• 通过interpretation关联类：如果你的locale里已经定义了一套符合某个类公理的操作，可以用interpretation来正式关联该类，从而复用其定理：

  locale my_custom_locale =
    fixes f :: "'a ⇒ 'a ⇒ 'a"
    assumes f_assoc: "f x (f y z) = f (f x y) z"
  begin
    interpretation semigroup "f" by (standard, rule f_assoc)
    -- 现在可以直接用semigroup的定理了，比如semigroup.assoc
  end
  

二、在类/假设中使用多种类型 #

如果需要处理多类型的类约束或者在locale假设里结合多种类型，这些方法会帮到你：

• 多参数类定义：你可以定义带有多个类型参数的类，每个参数都可以加上独立的类约束，比如：

  class my_multi_class = "'a :: ord" + "'b :: monoid" +
    fixes map_to_monoid :: "'a ⇒ 'b"
    assumes map_mono: "x ≤ y ⇒ map_to_monoid x ⊕ map_to_monoid y = map_to_monoid y"
  

  这里'a需要满足ord类约束，'b需要满足monoid类约束，完美实现多类型的类关联。
• Locale中叠加多类约束：如果只是在locale里需要同时使用多个类的定理，可以直接给类型变量叠加多个类约束：

  locale multi_constraint_locale =
    fixes elem :: "'a :: semigroup + monoid"
    assumes "elem ⊕ 1 = elem"
  

  这里'a同时满足semigroup和monoid的约束，你可以在locale里自由复用这两个类的所有定理。

额外实用技巧 #

• 用thm <class_name>_class.*命令可以快速查看某个类的所有预定义定理，比如thm monoid_class.*，方便你找到需要复用的定理。
• 如果遇到符号冲突，可以在locale内部用notation或abbreviation重新定义符号，避免和现有库的定义冲突。

内容的提问来源于stack exchange，提问作者user9716869 - supports Ukraine