|
Coinductive
Title: |
Coinductive |
Author:
|
Andreas Lochbihler
|
Contributor:
|
Johannes Hölzl (hoelzl /at/ in /dot/ tum /dot/ de)
|
Submission date: |
2010-02-12 |
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. |
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)
|
BibTeX: |
@article{Coinductive-AFP,
author = {Andreas Lochbihler},
title = {Coinductive},
journal = {Archive of Formal Proofs},
month = feb,
year = 2010,
note = {\url{http://isa-afp.org/entries/Coinductive.html},
Formal proof development},
ISSN = {2150-914x},
}
|
License: |
BSD License |
Used by: |
CakeML, CryptHOL, DynamicArchitectures, JinjaThreads, Lazy-Lists-II, Markov_Models, Ordered_Resolution_Prover, Parity_Game, Partial_Order_Reduction, Probabilistic_Noninterference, Stream_Fusion_Code, Topology |
Status: [ok] |
This is a development version of this entry. It might change over time
and is not stable. Please refer to release versions for citations.
|
|