1

我正在试验代码生成器。我的理论包含一个编码不变量的数据类型：

typedef small = "{x::nat. x < 10}" morphisms to_nat small
  by (rule exI[where x = 0], simp)

definition "is_one x ⟷ x = small 1"

现在我想导出is_one. 看来我首先必须为代码生成器设置数据类型，如下所示：

code_datatype small

instantiation small :: equal
begin
  definition "HOL.equal a b ⟷ to_nat a = to_nat b" 
  instance
  apply default
  unfolding equal_small_def
  apply (rule to_nat_inject)
  done
end

lemma [code abstype]: "small (to_nat x) = x" by (rule to_nat_inverse)

现在我可以定义一个is_one不违反抽象的代码方程：

definition [code del]:"small_one = small 1"
declare is_one_def[code del]
lemma [code]: "is_one x ⟷ x = small_one" unfolding is_one_def small_one_def..
lemma [code abstract]: "to_nat small_one = 1"
  unfolding small_one_def by (rule small_inverse, simp)

export_code is_one in Haskell file -

问题1：我可以避免将定义small_one拉出is_one吗？

现在我有一个小项目的复合值：

definition foo :: "small set list" where "foo = [ {small (10-i), small i} . i <- [2,3,4] ]"

在这种形式下，我无法使用它导出代码（“代码方程式 foo 中的抽象违规...”）。

问题 2：如何[code abstract]为这样的值定义引理？似乎代码生成器不接受形式的引理map to_nat foo = ...。

4

2 回答 2

3

对于具有由code_abstractsuch声明的不变量的类型small，任何代码方程都不能包含抽象函数small。因此，如果您希望is_one在 type 上表示等式测试small，您必须先定义一个常数small 1并证明相应的代码方程to_nat。这就是你所做的。但是，在表示类型上使用相等会更容易nat，即内联实现equal_class.equal；然后，您不需要equal为small任何一个实例化。

lemma is_one_code [code]: "is_one x ⟷ to_nat x = 1"
by(cases x)(simp add: is_one_def small_inject small_inverse)

该lifting软件包会自动为您完成大部分工作：

setup_lifting type_definition_small
lift_definition is_one :: "small => bool" is "%x. x = 1" ..
export_code is_one in SML file -

不幸的是，代码生成器不支持涉及抽象类型的复合返回类型，如small set list. 如Isabelle/HOL 中的数据细化中所述，第 1 节。3.2，您必须将类型包装为自己small set list的类型构造函数并使用 type进行定义。然后将类型表示为不变量。small_set_listfoosmall_set_listsmall_set_listnat set listlist_all (%A. ALL x:A. x < 10)

于 2013-04-16T15:46:53.647 回答
0

除了 Andreas 的解释和综合解决方案之外，我还找到了一种避免引入新类型的解决方法。假设foo在很多地方都没有使用，比如说，只在

definition "in_foo x = (∀s ∈ set foo. x ∈ s)"

尝试导出代码in_foo会出现“抽象违规”错误。但是使用程序细化，我可以避免有问题的代码：

我code_thms用来找出如何foo使用并发现它被用作list_all (op ∈ ?x) foo. 现在我重写了这个特殊的用法foo而不提small：

lemma [code_unfold]:
  "list_all (op ∈ x) foo ⟷
    list_all (op ∈ (to_nat x))  [ {(10-i), i} . i <- [2, 3, 4] ]"
  unfolding foo_def by (auto simp add: small_inverse small_inject)

（如果我定义foousing lift_definition，之后的证明apply transfer会更简单。）

foo在这个转换之后，它基本上捕获了满足 的不变量的所有成员small，代码导出按预期工作：

export_code in_foo in Haskell file -
于 2013-04-16T19:49:45.820 回答