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
.
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.