Isabelle:我如何识别两个具有相同但不相同参数的祖先语言环境？

Question

我有一个语言环境结构，其中某个语言环境作为另一个语言环境的祖先出现了两次，一次是通过继承，另一次是通过几个sublocale解释的序列。该祖先语言环境的两个实例的参数是相等的，但不是完全相同的(它们的相等必须并且可以通过证明来建立)。如何让Isabelle将这两个祖先语言环境实例合并为一个，就像当参数相同时所做的那样？

下面这个最小的例子演示了我的情况：

theory Diamond
  imports Main
begin

typedecl a
typedecl b
typedecl c

consts a_from_b :: "b ⇒ a"
consts b_from_a_and_c :: "[a, c] ⇒ b"

lemma equality: "a_from_b (b_from_a_and_c a c) = a"
  sorry

locale a =
  fixes a :: a

locale b =
  fixes b :: b
begin

sublocale a "a_from_b b" .

end

locale c = a +
  fixes c :: c
begin

sublocale b "b_from_a_and_c a c" .

end

end

命令print_dependencies! c会产生以下输出：

dependencies:
  a "a"
  a "a_from_b (b_from_a_and_c a c)"
  b "b_from_a_and_c a c"
  c "a" "c"

显然，a有两个实例。如何利用上述代码中提到的引理将这两个区域设置实例转换为单个实例a "a"？我尝试通过将locale c声明中的sublocale解释更改为以下代码来实现此目的：

sublocale b "b_from_a_and_c a c" rewrites "a = a_from_b (b_from_a_and_c a c)"
  by (simp add: equality)

但是，这会导致Isabelle挂起。

Answer 1

问题最后提到的想法几乎是可行的。只是rewrite方程式的两个边必须互换：

sublocale b "b_from_a_and_c a c" rewrites "a_from_b (b_from_a_and_c a c) = a"
  by (fact equality)

进行此更改后，print_dependencies! c将生成以下输出：

dependencies:
  a "a"
  b "b_from_a_and_c a c"
  c "a" "c"