Coinductive

Andreas Lochbihler with contributions from Johannes Hölzl

12 February 2010

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.
BSD License

Change history

[2010-06-10] coinductive lists setup for quotient package (revision 015574f3bf3c)
[2010-06-28] new codatatype terminated lazy lists (revision e12de475c558)
[2010-08-04] terminated lazy lists setup for quotient package; more lemmas (revision 6ead626f1d01)
[2010-08-17] Koenig's lemma as an example application for coinductive lists (revision f81ce373fa96)
[2011-02-01] lazy implementation of coinductive (terminated) lists for the code generator (revision 6034973dce83)
[2011-07-20] new codatatype resumption (revision 811364c776c7)
[2012-06-27] new codatatype stream with operations (with contributions by Peter Gammie) (revision dd789a56473c)
[2013-03-13] construct codatatypes with the BNF package and adjust the definitions and proofs, setup for lifting and transfer packages (revision f593eda5b2c0)
[2013-09-20] stream theory uses type and operations from HOL/BNF/Examples/Stream (revision 692809b2b262)
[2014-04-03] 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)

Used by

Topics

Related Entries

Theories

Cite

×
@article{Coinductive-AFP,
  author  = {Andreas Lochbihler},
  title   = {Coinductive},
  journal = {Archive of Formal Proofs},
  month   = February,
  year    = 2010,
  note    = {\url{http://isa-afp.org/entries/Coinductive.html},
            Formal proof development},
  ISSN    = {2150-914x},
}
Download