与伊莎贝尔的代码生成工作：数据细化和高阶函数

Question

这是Isabelle's Code generation: Abstraction lemmas for containers?后续：

我想在下面的理论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的代码公式中。另外，我想避免涉及在运行时重新检查不变量的黑客行为。 ）

Answer 1

简短的回答是no, it does not work。

长的答案是，通常可能有解决方法。 Brian在他的回答中显示了一个。总的想法似乎是

独立已经在协变位置，除了最终的返回值的抽象类型的函数（即高阶函数或返回抽象值的容器功能）到多个辅助功能，使抽象值仅构造为辅助函数之一的单个返回值。

在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) 

Answer 2

我对一般问题没有很好的解决方法，但是这里有一个想法，可以让你在这个特定情况下为the_question生成代码。

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

现在你可以证明一个新的代码方程smaller其RHS使用IF-THEN-ELSE，predecessor和正常列表操作：

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

（更有效的实现当然是可能的，如果你愿意定义一个辅助功能）

代码生成现在应该适用于smaller，因为此代码公式不使用函数small。