Isabelle/HOL中如何实现已声明的类型与常量？

问题1解答 #

typedecl和consts在全局理论层面声明的都是未解释的抽象类型/常量，一旦完成全局声明，就无法在当前理论及其所有子理论中给它们追加具体定义了：

• 全局typedecl本质是引入了一个全新的、无内部结构的原子类型，系统仅知道它是一个合法类型，没有其他预设属性，也不能再绑定到已有的具体类型上
• 全局consts声明的常量同理，仅确定了它的类型签名，没有默认取值，也不能后续直接用普通定义命令给它赋值，否则会报重复声明错误

如果你需要可灵活绑定具体实现的「接口式声明」，不要用全局的typedecl/consts，改用*区域（Locale）*机制来声明参数化的类型和常量即可。

问题2解答 #

全局声明的typedecl/consts无法实现多实现的接口效果，但是基于Locale机制可以完美满足这个需求：
你可以在Locale中把需要作为接口的类型、常量声明为Locale的参数，之后在不同的理论中，只要符合接口的类型约束，就可以用interpretation命令给Locale参数绑定不同的具体类型、常量实现，相当于同一个接口有多个不同的实现，和你预期的效果一致。
示例结构如下：

(* 定义接口Locale *)
locale state_interface =
  fixes M :: "('state × 'state) set"
    and L :: "'state ⇒ 'atom set"
begin
  (* 可以在Locale内基于接口写通用的引理、证明 *)
end

(* 实现1：用nat作为state类型，自定义对应的M和L *)
interpretation nat_state: state_interface 
  where M = "{(x,y) :: nat × nat. x < y}"
    and L = "(λs :: nat. {''a'', ''b''})"
  by unfold_locales auto

(* 实现2：用string作为state类型，另一套M和L实现 *)
interpretation string_state: state_interface
  where M = "{(x,y) :: string × string. length x < length y}"
    and L = "(λs. set s)"
  by unfold_locales auto

关于defs命令的说明 #

defs确实在Isabelle2021及后续版本中已经被正式移除，它是早期版本中用来给提前通过consts声明的常量追加定义的命令，现在的替代方案为：

• 如果是要定义普通全局常量，直接用definition命令一步完成类型声明+定义即可，不需要提前调用consts：

  (* 旧写法 *)
  consts f :: "nat ⇒ nat"
  defs f_def: "f x ≡ x + 1"
  
  (* 新写法 *)
  definition f :: "nat ⇒ nat" where
    "f x ≡ x + 1"
  

• 如果确实需要先声明未解释常量再补充约束/定义，统一在Locale或axiomatization块中处理即可。

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