Infinite Lists

David Trachtenherz

February 23, 2011

This is a development version of this entry. It might change over time and is not stable. Please refer to release versions for citations.


We introduce a theory of infinite lists in HOL formalized as functions over naturals (folder ListInf, theories ListInf and ListInf_Prefix). It also provides additional results for finite lists (theory ListInf/List2), natural numbers (folder CommonArith, esp. division/modulo, naturals with infinity), sets (folder CommonSet, esp. cutting/truncating sets, traversing sets of naturals).


BSD License


Session List-Infinite