如何在locale中定义归纳谓词？

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

谓词编译器从未本地化，即它不能直接处理在区域设置中定义的谓词。尽管如此，有两种方法可以完成这项工作。

要么，使用global_interpretation与defines子句来介绍谓词（纯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_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)