### 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

- Computer science/Functional programming

### 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

- ConcurrentHOL
- Continued Fractions
- 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

## Cite

×

Coinductive-AFP

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

Download

## Download

× Download latest

Older releases:

- Sep 13, 2023 : Isabelle2023
- Oct 27, 2022 : Isabelle2022
- Dec 14, 2021 : Isabelle2021-1
- Feb 23, 2021 : Isabelle2021
- Apr 18, 2020 : Isabelle2020
- Jun 11, 2019 : Isabelle2019
- Aug 16, 2018 : Isabelle2018
- Oct 10, 2017 : Isabelle2017
- Dec 17, 2016 : Isabelle2016-1
- Feb 22, 2016 : Isabelle2016
- May 27, 2015 : Isabelle2015
- Aug 28, 2014 : Isabelle2014
- Dec 11, 2013 : Isabelle2013-2
- Nov 17, 2013 : Isabelle2013-1
- Mar 2, 2013 : Isabelle2013
- Feb 16, 2013 : Isabelle2013
- May 24, 2012 : Isabelle2012
- Oct 11, 2011 : Isabelle2011-1
- Feb 11, 2011 : Isabelle2011
- Jun 30, 2010 : Isabelle2009-2
- Feb 15, 2010 : Isabelle2009-1
- Feb 14, 2010 : Isabelle2009-1