0

我想inductive在locale. 如果没有locale一切正常：

definition "P a b = True"

inductive test :: "'a ⇒ 'a ⇒ bool" where
  "test a a" |
  "test a b ⟹ P b c ⟹ test a c" 

code_pred test .

但是，当我在 a 中尝试相同的操作时locale，它不起作用：

locale localTest
begin
definition "P' a b = True"

inductive test' :: "'a ⇒ 'a ⇒ bool" where
  "test' a a" |
  "test' a b ⟹ P' b c ⟹ test' a c" 

code_pred test' 
end

语言环境中的code_pred行返回以下错误：

Not a constant: test'
4

3 回答 3

2

粗略地说，语言环境是一种抽象机制，允许引入与满足假设属性的某些假设常量相关的新常量，而代码生成则更为具体（您需要实现函数所需的所有信息，而不仅仅是其抽象规范）。

因此，您首先需要解释语言环境，然后才能生成代码。当然，在您的示例中没有假设的常数和属性，因此解释是微不足道的

interpretation test: localTest .

之后，您可以使用

code_pred test.test' .
于 2013-03-10T03:52:39.163 回答
2

您可以给出替代介绍规则（参见isabelle doc codegen第 4.2 节：替代介绍规则），从而避免解释。这也适用于带参数的语言环境（甚至适用于未归纳定义的常量）。您的示例的变体具有参数：

locale l =
  fixes A :: "'a set"
begin
definition "P a b = True"

inductive test :: "'a ⇒ 'a ⇒ bool" where
  "a ∈ A ⟹ test a a" |
  "test a b ⟹ P b c ⟹ test a c" 
end

我们引入一个新常数

definition "foo A = l.test A"

并证明它的引入规则（因此新常数对旧常数是正确的）。

lemma [code_pred_intro]:
  "a ∈ A ⟹ foo A a a"
  "foo A a b ⟹ l.P b c ⟹ foo A a c"
  unfolding foo_def by (fact l.test.intros)+

最后，我们必须证明新的常量也是完整的旧常量：

code_pred foo by (unfold foo_def) (metis l.test.simps)
于 2013-03-11T05:23:32.107 回答
0

在这里完成猜测，但我想知道重命名是否test给test'你带来了麻烦。（考虑code_pred test'改为code_pred "test'"。）

于 2013-03-09T22:11:17.987 回答