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

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" 

伊莎贝尔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自由构造。）如在~~/src/HOL/Library/Extended_Nat定义的扩展土黄enat有注册了两个这样的构造：∞和enat :: nat ⇒ enat。所以0不是enat的构造函数，而是普通自然的nat。所以，如果你写

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

相反，它会工作，因为只有模式中注册的构造函数。

相反，如果你的理论进口Coinductive_Nat从APF进入Coinductive，然后enat注册有构造0和eSuc，即，就好像它是一个codatatype。然后，您可以在0上进行模式匹配，但是您不能再在∞上匹配模式匹配。