CentraleSupélec LMF, UMR CNRS 9021
Département informatique Laboratoire Méthodes Formelles
Bât Breguet, 3 rue Joliot-Curie Bât 650 Ada Lovelace, Université Paris Sud
91190 Gif-sur-Yvette, France Rue Noetzlin, 91190 Gif-sur-Yvette, France
Tutoriel : types de données, fonctions et preuves en Isabelle

Ce tutoriel présente les fonctionnalités de base que nous utiliserons pour définir la sémantique du langage Niklaus :

  • définition de types de données
  • définition de fonctions
  • preuves par application de règles (apply) ou structurées (bloc proof/qed en Isar)

D'autres constructions seront présentées lorsqu'elles seront nécessaires.

Note : vous pouvez copier-coller le listing ci-dessous dans un fichier TutoList.thy pour l'utiliser dans Isabelle.

Installation d'Isabelle

Pour installer isabelle sur votre ordinateur, consultez https://isabelle.in.tum.de/

Exercice

Après avoir fait ce tutoriel, définissez une fonction snoc l x qui ajoute x à la fin de l, ainsi qu'une fonction rev_snoc l qui utilise snoc pour inverser l. Prouvez que rev_snoc l = rev l.

Vous pouvez utiliser la commande sledgehammer à la place d'une preuve. Cette commande utilise des solveurs externes pour essayer de trouver une preuve. En cas de succès, il ne reste qu'à remplacer l'appel à sledgehammer par la preuve qu'il a trouvée (il suffit pour cela de cliquer sur le texte de la preuve dans la console). Dans l'exemple ci-dessus, vous pouvez donc commencer par remplacer sorry par sledgehammer pour trouver les preuves.

Un exercice plus difficile

Définissez une fonction rev_acc qui inverse une liste par accumulation dans un second argument, et prouvez que rev_acc l [] = rev l. Dans cette démonstration, l'hypothèse de récurrence est trop faible car elle ne traite que le cas ou le second argument de rev_acc est la liste vide. Il faut donc établir un lemme plus général qui permettra de faire le raisonnement par induction. De plus, pour démontrer ce lemme par induction, nous aurons besoin de l'utiliser avec une autre valeur du second argument de rev_acc, il faut donc indiquer que cet argument est une variable libre grâce à arbitrary: r si l'argument est r.

Code du tutoriel

À enregistrer dans un fichier de nom TutoList.thy.