La fonction Goal permet d'établir un but à
démontrer:
le but est donné dans une chaine de caractère qui sera
analysée.
Exemple:
ML> Goal "(n::int) + 1 <= 0 ==> n < 0";
La réponse d'ISABELLE est d'afficher l'état courant de la preuve. Tant que la preuve n'est pas terminée, l'état courant ressemble à ça:
Level ...où les
G
1 .G1
2. G2
...
n. Gn
Gi, i = 1,2,...,n sont les
sous-buts restant à démontrer.
Pour faire la preuve d'un but, il faut utiliser une "tactique". La
tactique que nous emploierons principalement est la tactique Auto_tac
qui signifie "résoudre automatiquement" (mais isabelle
fournit d'autres tactiques pour les cas difficiles).
On essaie une tactique en tapant by(...) avec le nom de
la tactique
entre les parenthèses. Ici:
by(Auto_tac);
Nous obtenons la réponse No subgoals !
qui signifie que la preuve est terminée (et donc que le
théorème est démontré).