如何在Isabelle的Bar locale中复用Foo locale的'foo类型变量？

问题场景 #

想要在一个locale中定义Foo相关的常量，再在另一个localeBar中继承Foo并添加新函数，同时让Bar复用Foo中的'foo类型变量。但原代码运行报错，因为Bar继承Foo时，Foo的'foo被自动重命名为'a，和Bar中声明的'foo不是同一类型变量，导致类型不匹配。

原错误代码：

locale Foo =       fixes theFoo  ::  'foo
locale Bar = Foo + fixes makeBar :: "'foo ⇒ 'bar"

context Bar
begin
definition theBar :: 'bar where "theBar = makeBar theFoo"
(* 此处theFoo类型为'a，而非'foo，导致类型不匹配 *)
end

解决方案 #

在定义Bar时，显式指定父localeFoo的类型变量为'foo，将父locale的类型变量与子locale的类型变量绑定，避免自动重命名。

修正后的代码：

locale Foo = fixes theFoo :: 'foo
locale Bar = Foo 'foo + fixes makeBar :: "'foo ⇒ 'bar"

context Bar
begin
definition theBar :: 'bar where "theBar = makeBar theFoo"
(* 此时theFoo类型为'foo，与makeBar参数类型匹配 *)
end

原理说明 #

Isabelle中，当locale继承时若未显式指定类型变量，会自动对父locale的类型变量进行重命名（比如将'foo改为'a）。通过Foo 'foo的写法，明确告诉系统将父localeFoo的类型变量'foo绑定到当前子locale的'foo上，确保两者是同一个类型变量，从而解决类型不匹配问题。

内容的提问来源于stack exchange，提问作者Proof-By-Sledgehammer