src/ZF/ex/LList.thy
author lcp
Tue Aug 16 18:58:42 1994 +0200 (1994-08-16)
changeset 532 851df239ac8b
parent 515 abcc438e7c27
child 753 ec86863e87c8
permissions -rw-r--r--
ZF/Makefile,ROOT.ML, ZF/ex/Integ.thy: updated for EquivClass
     1 (*  Title: 	ZF/ex/LList.thy
     2     ID:         $Id$
     3     Author: 	Lawrence C Paulson, Cambridge University Computer Laboratory
     4     Copyright   1994  University of Cambridge
     5 
     6 Codatatype definition of Lazy Lists
     7 
     8 Equality for llist(A) as a greatest fixed point
     9 
    10 Functions for Lazy Lists
    11 
    12 STILL NEEDS:
    13 co_recursion for defining lconst, flip, etc.
    14 a typing rule for it, based on some notion of "productivity..."
    15 *)
    16 
    17 LList = QUniv + "Datatype" +
    18 
    19 consts
    20   llist  :: "i=>i"
    21 
    22 codatatype
    23   "llist(A)" = LNil | LCons ("a: A", "l: llist(A)")
    24 
    25 
    26 (*Coinductive definition of equality*)
    27 consts
    28   lleq :: "i=>i"
    29 
    30 (*Previously used <*> in the domain and variant pairs as elements.  But
    31   standard pairs work just as well.  To use variant pairs, must change prefix
    32   a q/Q to the Sigma, Pair and converse rules.*)
    33 coinductive
    34   domains "lleq(A)" <= "llist(A) * llist(A)"
    35   intrs
    36     LNil  "<LNil, LNil> : lleq(A)"
    37     LCons "[| a:A; <l,l'>: lleq(A) |] ==> <LCons(a,l), LCons(a,l')>: lleq(A)"
    38   type_intrs  "llist.intrs"
    39 
    40 
    41 (*Lazy list functions; flip is not definitional!*)
    42 consts
    43   lconst   :: "i => i"
    44   flip     :: "i => i"
    45 
    46 rules
    47   lconst_def  "lconst(a) == lfp(univ(a), %l. LCons(a,l))"
    48 
    49   flip_LNil   "flip(LNil) = LNil"
    50 
    51   flip_LCons  "[| x:bool; l: llist(bool) |] ==> \
    52 \              flip(LCons(x,l)) = LCons(not(x), flip(l))"
    53 
    54 end
    55