The Isabelle/Isar Reference Manual documents the proof methods induct
, induction
, and coinduct
. However, there is also the proof method coinduction
. Compared to coinduct
, 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 coinduction
somewhere?
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: Oct 12 2024 at 20:18 UTC