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

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？ ∞ 是 class infinity 的常量，0 是 class 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"

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

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

上进行模式匹配

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

How to use complex patterns in functions?

isabelle