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

【问题标题】：Isabelle: How can I identify two ancestor locales with equal but not identical parameters?Isabelle：如何识别具有相同但不相同参数的两个祖先语言环境？
【发布时间】：2018-12-14 21:07:07
【问题描述】：

我有一个语言环境结构，其中某个语言环境作为另一个语言环境的祖先出现了两次，一次通过继承，另一次通过几个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 挂起。

【问题讨论】：

标签： isabelle

【解决方案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"

【讨论】：