Email Gateway (Aug 18 2022 at 12:06): Email Gateway (Aug 18 2022 at 12:06):From: Richard Warburton <richard.warburton@gmail.com>
I was wondering if someone knew of any good examples of papers using
coinduction within Isabelle/HOL? If there were available theory
files relating to such papers it would also be most helpful.
regards,
Richard Warburton
Email Gateway (Aug 18 2022 at 12:07):From: Makarius <makarius@sketis.net>
Here are some theories using coinduction:
http://isabelle.in.tum.de/library/HOL/Library/Coinductive_List.html
http://afp.sourceforge.net/entries/Lazy-Lists-II.shtml
The second is based on an old version of the first, namely
http://isabelle.in.tum.de/library/HOL/Induct/LList.html
Makarius
Email Gateway (Aug 18 2022 at 12:08):From: Jeremy Dawson <jeremy@rsise.anu.edu.au>
Richard Warburton wrote:
Richard,
My paper in TPHOLs last year has an example of the use of coinduction:
Jeremy E. Dawson, Formalising Generalised Substitutions
<file:///home/web/jeremy/public_html/pubs/fgc/fgs/> In 20th
International Conference on Theorem Proving in Higher Order Logics
Kaiserslautern, September 2007 (TPHOLs 2007), LNCS 4732, 54-69
Link at http://users.rsise.anu.edu.au/~jeremy/
The use of coinduction was a significant improvement on the way I'd done
the same thing previously, so I give it a fair amount of detail
Jeremy
Email Gateway (Aug 18 2022 at 12:09):From: Richard Warburton <richard.warburton@gmail.com>
Thanks, these are all quite useful.
Richard
Last updated: Jan 04 2025 at 20:18 UTC