| Home |
| About |
| Submission |
| Updating Entries |
| Using Entries |
| Search |
| Statistics |
| Index |
| Download |
Infinite Lists
| Title: | Infinite Lists |
| Author: | David Trachtenherz |
| Submission date: | 2011-02-23 |
| Abstract: | 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). |
| BibTeX: |
@article{List-Infinite-AFP,
author = {David Trachtenherz},
title = {Infinite Lists},
journal = {Archive of Formal Proofs},
month = feb,
year = 2011,
note = {\url{http://isa-afp.org/entries/List-Infinite.html},
Formal proof development},
ISSN = {2150-914x},
}
|
| License: | BSD License |
| Used by: | Nat-Interval-Logic |
| 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 |