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.
The initial theory was contributed by Paulson and Wenzel. Extensions and other coinductive formalisations of general interest are welcome.
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
- Coinductive_Nat
- Coinductive_List
- Coinductive_List_Prefix
- Coinductive_Stream
- TLList
- Quotient_Coinductive_List
- Quotient_TLList
- Coinductive
- Lazy_LList
- Lazy_TLList
- CCPO_Topology
- LList_CCPO_Topology
- TLList_CCPO
- TLList_CCPO_Examples
- Koenigslemma
- LMirror
- Hamming_Stream
- Resumption
- Coinductive_Examples
Used by
- A Hoare Logic for Diverging Programs
- Partial Order Reduction
- CakeML
- Formalization of Bachmair and Ganzinger’s Ordered Resolution Prover
- Dynamic Architectures
- CryptHOL
- Positional Determinacy of Parity Games
- Stream Fusion in HOL with Code Generation
- Probabilistic Noninterference
- Markov Models
- Jinja with Threads
- Lazy Lists II
- Topology