| Home |
| About |
| Submission |
| Updating Entries |
| Using Entries |
| Search |
| Statistics |
| Index |
| Download |
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. |
|
Proof outline Proof document |
| Browse theories |
| Download this entry |
Older releases:
|