如何在语言环境中定义归纳谓词？

Question

这是一个简单的语言环境示例：

locale test =
  fixes test_less_eq :: "'a ⇒ 'a ⇒ bool"
begin

inductive test_eq where
  "test_less_eq x y ⟹ test_less_eq y x ⟹ test_eq x y"

end

它定义了归纳test_eq。它可以使用 definition 来定义，但我需要它是一个归纳谓词。

然后我定义了一个简单的语言环境解释并尝试使用它：

interpretation interp: test "op <" .

inductive some_pred where
  "interp.test_eq x y ⟹
   some_pred x y"

code_pred [show_modes] some_pred .

问题是 code_pred 出现以下错误：

Type mismatch of predicate test.test_eq (trying to match ?'a
                   ⇒ ?'a ⇒ bool and ('a ⇒ 'a ⇒ bool)
                                      ⇒ 'a ⇒ 'a ⇒ bool) in ?x1 < ?y1 ⟹
          ?y1 < ?x1 ⟹ interp.test_eq ?x1 ?y1

错误的原因是什么以及如何解决？

Answer 1

谓词编译器从未被本地化，即它不能直接处理在语言环境中定义的谓词。尽管如此，还是有两种方法可以完成这项工作。

或者，使用带有 defines 子句的 global_interpretation 来为谓词引入一个新常量（普通的 interpretation 只引入一个缩写）。然后，你还得重新声明引入规则code_pred，并证明相应的消除规则。

global_interpretation interp: test "op <" 
  defines interp_test_eq = interp.test_eq .

declare interp.test_eq.intros[code_pred_intro]

code_pred interp_test_eq by(rule interp.test_eq.cases)

或者，保持解释不变，重新声明locale中的定义映射到的内部常量的引入规则。这是 <locale_name>.<predicate_name>，即您的 test.test_eq。这仅在您的语言环境没有假设时有效。

declare test.test_eq.intros[code_pred_intro]

code_pred test.test_eq by(rule test.test_eq.cases)

如何在语言环境中定义归纳谓词？

How to define an inductive predicate inside locale?

isabelle