0

这是 Isabelle 代码生成的后续内容：容器的抽象引理？：

我想为the_question以下理论生成代码：

theory Scratch imports Main begin

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

definition a_pred :: "small ⇒ bool"
  where "a_pred = undefined"

definition "smaller j = [small i . i <- [0 ..< to_nat j]]" 

definition "the_question j = (∀i ∈ set (smaller j). a_pred j)"

问题是方程smaller不适合代码生成，因为它提到了抽象函数small。

现在根据 Andreas 对我最后一个问题的回答和关于数据细化的论文，下一步是为小数集引入一种类型，并smaller为该类型创建一个定义：

typedef small_list = "{l. ∀x∈ set l. (x::nat) < 10}" by (rule exI[where x = "[]"], auto)
code_datatype Abs_small_list
lemma [code abstype]: "Abs_small_list (Rep_small_list x) = x" by (rule Rep_small_list_inverse)

definition "smaller' j = Abs_small_list [ i . i <- [0 ..< to_nat j]]"
lemma smaller'_code[code abstract]: "Rep_small_list (smaller' j) = [ i . i <- [0 ..< to_nat j]]"
  unfolding smaller'_def
  by (rule Abs_small_list_inverse, cases j, auto elim: less_trans simp add: small_inverse)

现在smaller'是可执行的。据我了解，我需要将操作重新定义small list为操作small_list：

definition "small_list_all P l = list_all P (map small (Rep_small_list l))"

lemma[code]: "the_question j = small_list_all a_pred (smaller' j)"
  unfolding small_list_all_def the_question_def smaller'_code smaller_def Ball_set by simp

我可以为the_question. 但是 的定义small_list_all不适合代码生成，因为它提到了抽象态射small。如何使small_list_all可执行文件？

（请注意，我无法展开 的代码方程a_pred，因为问题实际上发生在实际递归的代码方程中a_pred。另外，我想避免涉及在运行时重新检查不变量的黑客行为。）

4

2 回答 2

2

对于一般问题，我没有很好的解决方案，但这里有一个想法可以让您the_question在这种特殊情况下生成代码。

首先，predecessor :: "small ⇒ small使用抽象代码方程定义一个函数（可能使用lift_definitionfrom λn::nat. n - 1）。

smaller现在您可以证明其 rhs 使用 if-then-elsepredecessor和正常列表操作的新代码方程：

lemma smaller_code [code]:
  "smaller j = (if to_nat j = 0 then []
    else let k = predecessor j in smaller k @ [k])"

（如果您愿意定义一个辅助函数，当然可以实现更高效的实现。）

代码生成现在应该适用于smaller，因为此代码方程式不使用 function small。

于 2013-04-30T22:17:56.357 回答
0

简短的回答是否定的，它不起作用。

长答案是通常有可能的解决方法。布赖恩在他的回答中展示了一个。一般的想法似乎是

将除了最终返回值（即高阶函数或返回抽象值容器的函数）之外在协变位置具有抽象类型的函数分离为多个辅助函数，以便抽象值仅构造为辅助函数之一的单个返回值功能。

在 Brian 的例子中，这个函数是predecessor. 或者，作为另一个简单的例子，假设一个函数

definition smallPrime :: "nat ⇒ small option"
  where "smallPrime n = (if n ∈ {2,3,5,7} then Some (small n) else None)"

这个定义不是一个有效的代码方程，因为small. 但这得出一个：

definition smallPrimeHelper :: "nat ⇒ small"
  where "smallPrimeHelper n = (if n ∈ {2,3,5,7} then small n else small 0)"
lemma [code abstract]: "to_nat (smallPrimeHelper n) = (if n ∈ {2,3,5,7} then n else 0)"
  by (auto simp add: smallPrimeHelper_def intro: small_inverse)
lemma [code_unfold]: "smallPrime n = (if n ∈ {2,3,5,7} then Some (smallPrimeHelper n) else None)"
  unfolding smallPrime_def smallPrimeHelper_def by simp

如果想避免谓词的冗余计算（这可能比 更复杂∈ {2,3,5,7}，可以通过引入抽象视图来使助手的返回类型更智能，即包含计算结果和从中构造抽象类型所需的信息：

typedef smallPrime_view = "{(x::nat, b::bool). x < 10 ∧ b = (x ∈ {2,3,5,7})}"
  by (rule exI[where x = "(2, True)"], auto)
setup_lifting type_definition_small
setup_lifting type_definition_smallPrime_view

对于视图，我们有一个构建它的函数和将结果分开的访问器，并带有一些关于它们的引理：

lift_definition smallPrimeHelper' :: "nat ⇒ smallPrime_view"
  is "λ n. if n ∈ {2,3,5,7} then (n, True) else (0, False)" by simp
lift_definition smallPrimeView_pred :: "smallPrime_view ⇒ bool"
  is "λ spv :: (nat × bool) . snd spv" by auto
lift_definition smallPrimeView_small :: "smallPrime_view ⇒ small"
  is "λ spv :: (nat × bool) . fst spv" by auto
lemma [simp]: "smallPrimeView_pred (smallPrimeHelper' n) ⟷ (n ∈ {2,3,5,7})"
  by transfer simp
lemma [simp]: "n ∈ {2,3,5,7} ⟹ to_nat (smallPrimeView_small (smallPrimeHelper' n)) = n"
  by transfer auto
lemma [simp]: "n ∈ {2,3,5,7} ⟹ smallPrimeView_small (smallPrimeHelper' n) = small n"
  by (auto intro: iffD1[OF to_nat_inject] simp add: small_inverse)

有了它，我们可以推导出一个只进行一次检查的代码方程：

lemma [code]: "smallPrime n = 
  (let spv = smallPrimeHelper' n in
   (if smallPrimeView_pred spv
    then Some (smallPrimeView_small spv)
    else None))"
   by (auto simp add: smallPrime_def Let_def)
于 2013-05-02T21:37:12.450 回答