Isabelle的代码生成：容器的抽象引理？ [英] Isabelle's Code generation: Abstraction lemmas for containers?

问题描述

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

I am experimenting with the Code generator. My theory contains a datatype that encodes an invariant:

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 的代码。看来我首先必须为代码生成器设置数据类型，如下所示：

Now I want to export code for is_one. It seems that I first have to set up the data type for the code generator as follows:

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 定义一个代码方程不违反抽象：

And now I am able to define a code equation for is_one that does not violate the abstraction:

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 ： C我避免从 is_one 中拉出 small_one 的定义吗？

Question 1: Can I avoid pulling the definition of small_one out of is_one?

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

Now I have a compound value of small items:

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

在这种形式下，我无法导出代码

In that form, I cannot export code using it ("Abstraction violation in code equation foo...").

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

Question 2: How do I define an [code abstract] lemma for such a value? It seems that the code generator does not accept lemmas of the form map to_nat foo = ....

推荐答案

对于带有 code_abstract 声明的不变量的类型，例如 small ，没有代码方程可以包含抽象函数 small 。因此，如果要在<$ c中进行相等性测试$ c> is_one 要以类型 small 表示，则必须为 small 1 并首先使用 to_nat 证明相应的代码方程式，这就是您所做的，但是，对表示类型<$ c $使用相等性会更容易c> nat ，即内联实现 equal_class.equal ;那么，您也无需为 small 实例化 equal 。

For types with invariants declared by code_abstract such as small, no code equation may contain the abstraction function small. Consequently, if you want the equality test in is_one to be expressed on type small, you have to define a constant for small 1 and prove the corresponding code equation with to_nat first. This is what you have done. However, it would be easier to use equality on the representation type nat, i.e., inline the implementation equal_class.equal; then, you do not need to instantiate equal for small either.

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

起重软件包会自动为您完成大部分操作：

The lifting package does most of this for you automatically:

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

不幸的是，代码生成器不支持复合返回类型涉及诸如小集合列表中的抽象类型。如 Isabelle / HOL中的数据优化中所述。 3.2 ，您必须将类型 small set list 包装为自身的类型构造函数 small_set_list 用 small_set_list 定义 foo 。然后将类型 small_set_list 表示为 nat set list ，并带有不变的 list_all（％A。全部x：A.x <10）。

Unfortunately, the code generator does not support compound return types that involve abstract types like in small set list. As described in Data Refinement in Isabelle/HOL, sect. 3.2, you have to wrap the type small set list as a type constructor small_set_list of its own and define foo with type small_set_list. The type small_set_list is then represented as nat set list with the invariant list_all (%A. ALL x:A. x < 10).

这篇关于Isabelle的代码生成：容器的抽象引理？的文章就介绍到这了，希望我们推荐的答案对大家有所帮助，也希望大家多多支持IT屋！