Comment utiliser des motifs complexes dans les fonctions?

Question

Voici une fonction exemple:

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 me montre l'erreur suivante:

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

Pourquoi pattern-matching fonctionne bien pour Some ∞ et ne fonctionne pas pour Some 0? ∞ est une constante pour la classe infinity et 0 est une constante pour la classe zero. Quelle est la différence entre ces constantes?

Answer 1

Le modèle correspondant à fun ne fonctionne que pour les constructeurs, généralement générés à l'aide des commandes datatype et codatatype. (En fait, il suffit qu'ils soient enregistrés comme constructeurs libres en utilisant free_constructors.) Les naturels étendus enat tels que définis dans ~~/src/HOL/Library/Extended_Nat ont deux constructeurs de ce type enregistrés: ∞ et enat :: nat ⇒ enat. Donc, 0 n'est pas un constructeur de enat, mais des naturels naturels nat. Donc, si vous écrivez

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

à la place, cela fonctionnera car il n'y a que des constructeurs enregistrés dans les modèles.

À l'inverse, si vos importations de théorie Coinductive_Nat de l'entrée APF Coinductive, puis enat est enregistré pour avoir les constructeurs 0 et eSuc, à savoir, comme si elle était un codatatype. Ensuite, vous pouvez faire correspondre le motif sur 0, mais vous ne pouvez plus faire correspondre le motif sur ∞.