如何在函數中使用複雜模式？

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上進行模式匹配，但是您不能再在∞上匹配模式匹配。