Coinductive

Andreas Lochbihler 🌐 with contributions from Johannes Hölzl 📧

February 12, 2010

This is a development version of this entry. It might change over time and is not stable. Please refer to release versions for citations.

Abstract

This article collects formalisations of general-purpose coinductive data types and sets. Currently, it contains coinductive natural numbers, coinductive lists, i.e. lazy lists or streams, infinite streams, coinductive terminated lists, coinductive resumptions, a library of operations on coinductive lists, and a version of König's lemma as an application for coinductive lists.
The initial theory was contributed by Paulson and Wenzel. Extensions and other coinductive formalisations of general interest are welcome.

License

BSD License

History

April 3, 2014
ccpo structure on codatatypes used to define ldrop, ldropWhile, lfilter, lconcat as least fixpoint; ccpo topology on coinductive lists contributed by Johannes Hölzl; added examples (revision 23cd8156bd42)
September 20, 2013
stream theory uses type and operations from HOL/BNF/Examples/Stream (revision 692809b2b262)
March 13, 2013
construct codatatypes with the BNF package and adjust the definitions and proofs, setup for lifting and transfer packages (revision f593eda5b2c0)
June 27, 2012
new codatatype stream with operations (with contributions by Peter Gammie) (revision dd789a56473c)
July 20, 2011
new codatatype resumption (revision 811364c776c7)
February 1, 2011
lazy implementation of coinductive (terminated) lists for the code generator (revision 6034973dce83)
August 17, 2010
Koenig's lemma as an example application for coinductive lists (revision f81ce373fa96)
August 4, 2010
terminated lazy lists: setup for quotient package; more lemmas (revision 6ead626f1d01)
June 28, 2010
new codatatype terminated lazy lists (revision e12de475c558)
June 10, 2010
coinductive lists: setup for quotient package (revision 015574f3bf3c)

Topics

Session Coinductive