Lazy Lists II

 

Title:	Lazy Lists II
Author:	Stefan Friedrich
Submission date:	2004-04-26
Abstract:	This theory contains some useful extensions to the LList (lazy list) theory by Larry Paulson, including finite, infinite, and positive llists over an alphabet, as well as the new constants take and drop and the prefix order of llists. Finally, the notions of safety and liveness in the sense of Alpern and Schneider (1985) are defined.

 

Proof outline Proof document

Browse theories

Download this entry

Older releases: Isabelle 2007: afp-Lazy-Lists-II-2007-11-27.tar.gz Isabelle 2005: afp-Lazy-Lists-II-2005-10-14.tar.gz Isabelle 2004: afp-Lazy-Lists-II-2004-05-21.tar.gz