src/ZF/ex/LList.thy
author clasohm
Tue Feb 06 12:27:17 1996 +0100 (1996-02-06)
changeset 1478 2b8c2a7547ab
parent 1401 0c439768f45c
child 11316 b4e71bd751e4
permissions -rw-r--r--
expanded tabs
     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 = 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 defs
    47   lconst_def  "lconst(a) == lfp(univ(a), %l. LCons(a,l))"
    48 
    49 rules
    50   flip_LNil   "flip(LNil) = LNil"
    51 
    52   flip_LCons  "[| x:bool; l: llist(bool) |] ==> 
    53               flip(LCons(x,l)) = LCons(not(x), flip(l))"
    54 
    55 end
    56