src/ZF/ex/llistfn.thy

Addition of cardinals and order types, various tidying

(*  Title: 	ZF/ex/llist-fn.thy
    ID:         $Id$
    Author: 	Lawrence C Paulson, Cambridge University Computer Laboratory
    Copyright   1993  University of Cambridge

Functions for Lazy Lists in Zermelo-Fraenkel Set Theory 

STILL NEEDS:
co_recursion for defining lconst, flip, etc.
a typing rule for it, based on some notion of "productivity..."
*)

LListFn = LList + LList_Eq +
consts
  lconst   :: "i => i"
  flip     :: "i => i"

rules
  lconst_def  "lconst(a) == lfp(univ(a), %l. LCons(a,l))"

  flip_LNil   "flip(LNil) = LNil"

  flip_LCons  "[| x:bool; l: llist(bool) |] ==> \
\              flip(LCons(x,l)) = LCons(not(x), flip(l))"

end