Définir des fonctions entre constantes dans Isabelle

Question

Je suis un mathématicien qui commence à s'habituer à Isabelle, et quelque chose qui devrait être incroyablement simple s'est avéré frustrant. Comment définir une fonction entre deux constantes? Dites, la fonction f: {1,2,3} \ à {1,2,4} mappage 1 à 1, 2 à 4 et 3 à 2?

Je suppose que je réussi à définir les ensembles comme des constantes t1 et t2 sans incident, mais (je suppose, car ils sont pas des types de données) Je ne peux pas essayer quelque chose comme

definition f ::"t1 => t2" where 
"f 1 = 1" | 
"f 2 = 4" | 
"f 3 = 2" 

Je crois doit y avoir une idée fausse fondamentale derrière cette difficulté, alors j'apprécie toute orientation.

Answer 1

Votre question comporte plusieurs aspects.

Tout d'abord, pour obtenir quelque chose de travailler rapidement, utilisez le mot-clé fun au lieu de definition, comme ceci:

fun test :: "nat ⇒ nat" where 
    "test (Suc 0) = 1" | 
    "test (Suc (Suc 0)) = 4" | 
    "test (Suc (Suc (Suc 0))) = 2" | 
    "test _ = undefined" 

Vous ne pouvez pas match de motif sur des arguments directement dans la tête de la définition en utilisant le mot-clé definition, alors que vous pouvez avec fun. Notez également que j'ai remplacé les littéraux numériques surchargés (1, 2, 3, etc.) par les constructeurs pour le type de données nat (0 et Suc) dans la correspondance de modèle.

Une alternative serait de rester avec definition, mais pousser l'analyse de cas de l'argument de la fonction à l'intérieur du corps de la définition en utilisant une instruction case, comme ceci:

definition test2 :: "nat ⇒ nat" where 
    "test2 x ≡ 
    case x of 
     (Suc 0) ⇒ 1 
    | (Suc (Suc 0)) ⇒ 4 
    | (Suc (Suc (Suc 0))) ⇒ 2 
    | _ ⇒ undefined" 

Notez que les définitions comme test2 ne sont pas déplié par le simplificateur par défaut, et vous devrez ajouter manuellement le théorème test2_def au simpset du simulateur si vous voulez étendre les occurrences de test2 dans une preuve.

Vous pouvez également définir de nouveaux types (vous ne pouvez pas utiliser des ensembles en tant que types, directement, comme vous essayez de le faire) correspondant à vos deux ensembles de trois éléments avec typedef, mais personnellement je resterais avec nat.

EDIT: utiliser typedef, faire quelque chose comme:

typedef t1 = "{x::nat. x = 1 ∨ x = 2 ∨ x = 3}" 
    by auto 

definition test :: "t1 ⇒ t1" where 
    "test x ≡ 
    case (Rep_t1 x) of 
    | Suc 0 ⇒ Abs_t1 1 
    | Suc (Suc 0) ⇒ Abs_t1 4 
    | Suc (Suc (Suc 0)) ⇒ Abs_t1 2" 

Bien que, je ne pas utiliser jamais vraiment moi-même typedef, et si cela peut ne pas être la meilleure façon d'utiliser ce et d'autres peuvent éventuellement suggérer d'une autre manière. Ce que typedef fait est de découper un nouveau type d'un existant, en identifiant un ensemble non-vide d'habitants pour le nouveau type. L'obligation de preuve, ici close par auto, est simplement de démontrer que l'ensemble définissant pour le nouveau type est en effet non vide, et dans ce cas je suis en train de découper un ensemble de trois éléments naturels en un nouveau type, appelé t1, donc la preuve est assez triviale. Deux nouvelles constantes sont créées, Abs_t1 et Rep_t1, ce qui vous permet de passer d'un mode naturel au nouveau type. Si vous mettez un print_theorems après la commande typedef, vous verrez plusieurs nouveaux théorèmes sur t1 qu'Isabelle a générés automatiquement pour vous.