Théories

Une théorie Isabelle doit se trouver dans un fichier de même nom que la théorie, avec l'extension .thy.

Types de données

Types prédéfinis

bool

le type des booléens, avec les valeurs True et False et les opérateurs ∧, ∨, ¬, ⟶

nat

le type des entiers naturels, construit avec 0 et Suc nat

int

le type des entiers relatifs (int n donne l'entier correspondant au naturel n)

string

le type des chaînes de caractères (listes de caractères, littéraux de la forme ''abcdef'')

Collections paramétrées

α list

liste d'éléments de type α. [] est la liste vide, x#l ajoute l'élément x en tête de la liste l, et l1@l2 concatène les listes l1 et l2. hd donne le premier d'une liste, tl donne la liste privée de son premier élément.

α set

ensemble d'éléments de type α. {} est l'ensemble vide, {a, b, c} est un ensemble défini en extension, {x. P(x)} est défini en compréhension par le prédicat P. Par exemple, {n::nat. ∃k. n = 2*k} est l'ensemble des naturels pairs. Une syntaxe plus compacte est également disponible {2*k | k::nat. True}. Les opérations usuelles (∈, ⋃, ⋂, ⊆) sont disponibles.

Produit cartésien

Le produit cartésien de deux types 'α et 'β est 'α × 'β. Une telle paire se note entre parenthèses : (a, b) est de type 'α × 'β si a est de type 'α et b de type 'β.

Ici, 'α et 'β sont des variables de type, que l'on reconnait au guillemet simple qui précède leur nom.

On accède au premier élément de la paire à l'aide de l'opérateur fst, et au second à l'aide de l'opérateur snd. Ainsi, fst (a, b) = a et snd (a, b) = b.

Fonctions

Le type des fonctions à n argument de types respectifs 't1, 't2, ..., 'tn et rendant un résultat de type 't est :

qui s'écrit également 't1 ⇒ 't2 ⇒ ... ⇒ 'tn ⇒ 't.

Par exemple, le type de la fonction :

est nat ⇒ nat ⇒ nat (qui peut également s'écrire [nat, nat] ⇒ nat).

Types synonymes

Il est possible de définir un nouveau nom pour un type, en général pour améliorer la lisibilité des théories :

Types inductifs

Un type inductif est défini en donnant ses constructeurs, c'est-à-dire toutes les formes que peuvent prendre les termes de ce type :

Cette définition crée le type exemple, un terme de type exemple pouvant soit être la constante Vide, soit construit par le constructeur Entier à partir d'un int, soit construit par le constructeur Exemple à partir d'un autre exemple. La commande term permet d'afficher la valeur et le type d'un terme.

La définition d'un type inductif génère un certain nombre de théorèmes, qui indiquent par exemple que les différentes formes du type sont distinctes, et qui permettent de faire des preuves par induction sur le type. Ces théorèmes sont affichés par la commande print_theorems placée après la définition du type.

Termes

Les termes (à placer entre doubles guillemets) sont formés par application de fonctions (constructeurs de types inclus) à d'autres termes. Il est également possible d'utiliser des notations infixées (comme + pour la fonction plus), ainsi que les constructions suivantes :

if c then a else b

où c est un booléen, et a et b deux termes de même type.

let x=t in u

qui est équivalent à u dans lequel toutes les occurrences libres de x ont été remplacées par t.

case e of p₁ ⇒ e₁ | p₂ ⇒ e₂ | ... | p_n ⇒ e_n

donne e_i si p_i est la première forme à laquelle correspond e.

L'égalité des termes est notée =, elle correspond à l'équivalence pour les termes de type bool.

Les quantificateurs se notent ∀x. P et ∃x. P. L'existence d'un élément unique se note ∃!x. P.

Pour lever l'ambiguïté sur le type d'un terme, on peut le faire suivre de ::type, et il faut généralement placer le tout entre parenthèses (voir les exemples).

Definitions et fonctions

Il est possible de définir des constantes pour rendre une théorie plus lisible. La forme générale d'une définition est :

Il est également possible d'indiquer le type de la constante :

Exemple :

Ce genre de définition ne peut pas être récursif, la constante en cours de définition ne doit pas apparaître dans la définition.

Pour définir une fonction récursive, il faut utiliser les commandes primrec et fun. primrec permet de définir des fonctions récursives primitives, c'est-à-dire des fonctions dans lesquelles chaque appel récursif supprime un constructeur d'un des arguments, ce qui garantit la terminaison. Par exemple :

Pour définir une fonction totale récursive sous une forme non primitive, on utilise fun. On peut dans ce cas utiliser des motifs plus généraux pour les termes de gauche, et la récursion n'est pas limitée aux types inductifs. Par exemple, dans la définition suivante de la suite de Fibonacci, le motif fib (Suc 0) n'est pas un motif primitif (les motifs du type nat sont 0 et Suc n) :

Les fonctions définies en Isabelle/HOL sont totales et terminent. La preuve de la terminaison est le plus souvent automatique avec fun, mais dans certains cas, il peut être nécessaire de faire cette preuve à la main.

La définition d'une fonction avec primrec ou fun déclare des règles de simplification qui sont utilisées par le simplificateur d'Isabelle pour réécrire les termes. Ces règles servent dans les démonstration de théorèmes et pour calculer la fonction avec value. Vous pouvez afficher ces règles pour les fonctions fac et fib à l'aide des commandes suivantes :

Théorèmes et preuves

Un théorème est introduit par la commande lemma ou par la commande theorem. Le choix de l'une ou l'autre commande indique uniquement l'importance que l'on accorde au théorème.

La preuve d'un théorème se fait en utilisant des faits déjà connus et des règles de déduction.

Une règle de déduction classique est le modus ponens : {$\displaystyle\frac{P\rightarrow Q \quad P}{Q} (mp)$}, qui s'écrit en Isabelle :

Les variables précédées d'un point d'interrogation sont des variables schématiques, qui peuvent être remplacées par n'importe quel terme. On peut les considérer comme des variables "super-libres".

Si nous voulons démontrer le théorème ⟦(P ∧ Q) ⟶ R; P ∧ Q⟧ ⟹ R, nous pouvons le faire grâce au modus ponens en unifiant ?P et P ∧ Q, et ?Q et R :

La ligne 2 utilise la méthode rule pour utiliser le théorème mp. Cette méthode unifie la conclusion de de ce qui doit être démontré (le but, ou goal) avec la conclusion du théorème mp. Ici, elle unifie donc ?Q avec R. Elle remplace ensuite le but courant par autant de buts qu'il y a de prémisses dans le théorème, chacun de ces buts consistant à montrer que les prémisses du but courant entraînent celles du théorème. Ici, le théorème ''mp' a deux prémisses : ?P ⟶ ?Q et ?P. Le but sera donc remplacé par les deux buts :

On voit que ?Q a été unifié avec R.

Le premier but peut être montré en unifiant ?P et (P ∧ Q), ce qui donne (P ∧ Q) ⟶ R ⟹ (P ∧ Q) ⟶ R. Un tel but est traité par la méthode assumption, qui décharge un but si sa conclusion est unifiable avec une des prémisses.

Il ne reste alors que le but (P ∧ Q) ⟶ R ⟹ ?P, qui se traite par la méthode assumption en unifiant ?P et (P ∧ Q) ⟶ R. La commande done permet de finir la preuve.

Règles d'introduction

Certaines règles permettent d'introduire un symbole logique. Par exemple, si on a P et Q, on peut obtenir P ∧ Q : {$\displaystyle\frac{P \quad Q}{P \wedge Q} (conjI)$}. Cette règle d'introduction de la conjonction s'écrit en Isabelle :

Avec cette règle, on peut facilement démontrer le théorème suivant :

Le signe + après la dernière commande apply indique qu'il faut l'appliquer autant de fois que possible.

Affichez les règles d'introduction de la disjonction (disjI1 et disjI2) et de l'implication (impI) à l'aide de la commande thm.

Règles d'élimination

Certaines règles permettent d'éliminer un un symbole. Par exemple, si on a P ∧ Q, on peut avoir P et on peut avoir Q : {$\displaystyle\frac{P\wedge Q}{P} (conjonct1)$} et {$\displaystyle\frac{P\wedge Q}{Q} (conjonct2)$}.

On peut utiliser conjunct1 pour démontrer que ⟦(P ∧ Q) ∧ R⟧ ⟹ P ∧ Q :

Il existe une méthode erule plus adaptée aux règles d'élimination. Cette méthode fonctionne lorsque l'on peut unifier simultanément la conclusion de la règle avec celle du but, et la première prémisse de la règle avec une des prémisses du but. Elle considère la première prémisse du théorème comme prouvée, et remplace le but par les buts correspondant aux prémisses suivantes. Dans cet exemple, erule permet de faire la preuve en une seule étape : en unifiant ?P avec P ∧ Q, et ?Q avec R.