Wolfgang Jeltsch (Mar 30 2023 at 19:07): Wolfgang Jeltsch (Mar 30 2023 at 19:07):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?
Wolfgang Jeltsch (Mar 31 2023 at 20:20):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: May 02 2024 at 04:18 UTC