1

我正在尝试使用传输包为自定义数据类型建立归纳规则，但apply transfer对我不起作用。这是一个简单的例子：

theory TransferHO imports Main begin

typedef pos = "{x :: nat. x > 0}" by blast
setup_lifting  type_definition_pos

lift_definition one :: pos is 1 by auto
lift_definition S :: "pos ⇒ pos" is Suc by auto

lemma
  assumes "P one"
  assumes "⋀ x. P x ⟹ P (S x)"
  shows "P n"
  using assms
  apply transfer

这个时候目标还是

⋀P x. P one ⟹ (⋀x. P x ⟹ P (S x)) ⟹ P x

并不是

⋀P x. P 1 ⟹ (⋀x. x > 0 ⟹ P x ⟹ P (Suc x)) ⟹ x > 0 ⟹ P x

我会期待的。在证明它之前我需要做什么来转移引理？

另外，一般来说，如何才能更好地控制apply transfer，或者至少是更好的调试方式？

4

1 回答 1

3

转移的结果通常不是唯一的，转移方法仅计算可能的解决方案之一，但您可以回溯back以循环其他解决方案。在您的特定示例中，您在回溯 53 次后找到了您想要的结果（至少使用 Isabelle2013-1-RC3）。解决方案的顺序由[transfer_rule]声明的顺序决定，因此回溯的数量可能会从一个版本到下一个版本发生变化。

不幸的是，transfer如果有很多解决方案，它几乎无法控制目标的位置。

于 2013-10-28T12:43:43.913 回答