The Isabelle/Isar Reference Manual documents the proof methods
coinduct. However, there is also the proof method
coinduction. Compared to
coinduction seems to be superior; in particular, it can derive the bisimulation relation to use from the goal, something that
coinduct apparently can’t do. I cannot remember having seen
coinduction documented anywhere; I only encountered it in some AFP proof. Is there a documentation of
Oh, it seems that my coworker, @Javier Diaz, has already found it: it’s already cited in a paper we’re currently writing. :sweat_smile: Thank you, Javi, my related-work wonder. :grinning_face_with_smiling_eyes: The document I sought is the paper Truly Modular (Co)datatypes for Isabelle/HOL.
Last updated: Dec 07 2023 at 08:19 UTC