0

Isabelle 中的这个（修剪掉的）核心递归函数定义

primcorec tree :: "'form fset ⇒ 'vertex ⇒ 'preform ⇒ (('form fset × 'form), ('rule × 'preform) NatRule) dtree" where
 "tree Γ v p =
    (case undefined of Hyp h c ⇒ undefined | Reg c ⇒
    Node undefined (fimage (tree Γ v) undefined)
    )"

产量

Unexpected corecursive call in "case undefined of Reg c ⇒ Node undefined (tree Γ v |`| undefined)" at
  "case case undefined of Reg c ⇒ Node undefined (tree Γ v |`| undefined) of Node uu uua ⇒ uua"

但如果我进一步简化为

primcorec tree :: "'form fset ⇒ 'vertex ⇒ 'preform ⇒ (('form fset × 'form), ('rule × 'preform) NatRule) dtree" where
   "tree Γ v p =
      (Node undefined (fimage (tree Γ v) undefined))"

有用。

我也尝试使用解构视图，即

primcorec tree :: "'form fset ⇒ 'vertex ⇒ 'preform ⇒ (('form fset × 'form), ('rule × 'preform) NatRule) dtree" where
 "cont (tree Γ v p) = (case undefined of Hyp h c ⇒ undefined | Reg c ⇒ (fimage (tree Γ v) undefined))"

现在我收到一条不同的错误消息：Invalid map function at "case undefined of Reg c ⇒ tree Γ v |`| undefined".

可能是什么原因？

使用其他case表达式它可以工作，我没有在文档中找到任何提及限制（数据类型文档中的第 5.1.1 节。）

4

1 回答 1

0

通过私人通信，我被告知解决方案是将(discs_sel)选项添加到datatype构造Hyp函数的来源。

于 2016-02-03T14:44:28.303 回答