Comment appliquer l'analyse de cas dans Isabelle ? Je cherchais quelque chose de similaire à apply (induct x) (qui est utilisé pour l'induction).
Réponse
Trop de publicités?
L'analyse de cas est généralement effectuée avec le cases (voir aussi "cas (méthode)" dans l'index de l'annuaire de l'UE). Manuel de référence Isabelle/Isar d'Isabelle2014). Si vous êtes un débutant, je vous recommande le tutoriel Programmation et validation en Isabelle/HOL .
Notez que depuis Isabelle 2014, la documentation est également disponible dans l'IDE Isabelle/jEdit dans le panneau Documentation.
