如何在函数中使用复杂模式？

Question

这是一个示例函数:

fun divide :: "enat option ? enat option ? real option" where
  "divide (Some ?) _ = None"
| "divide _ (Some ?) = None"
| "divide _ (Some 0) = None"
| "divide (Some a) (Some b) = Some (a / b)"
| "divide _ _ = None"

Isabelle HOL向我显示以下错误:

Malformed definition:
Non-constructor pattern not allowed in sequential mode.
?uw_. divide uw_ (Some 0) = None

为什么模式匹配工作正常Some ?并且不起作用Some 0？?是类常量infinity和0对类中的常数zero.这些常数之间有什么区别？

Answer 1

模式匹配fun仅适用于构造函数,通常使用datatype和codatatype命令生成.(事实上​​,如果它们被注册为使用的自由构造函数就足够了free_constructors.)enat定义的扩展自然~~/src/HOL/Library/Extended_Nat有两个这样的构造函数注册:?和enat :: nat ? enat.所以0不是enat普通自然人的构造者,而是普通自然人的构造者nat.所以,如果你写

| "divide _ (Some (enat 0)) = None"

相反,它会起作用,因为模式中只有注册的构造函数.

相反,如果你的理论进口Coinductive_Nat从APF项Coinductive,然后enat是注册有构造函数0和eSuc,即,就好像它是一个codatatype.然后你可以模式匹配0,但你不能再模式匹配?.