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
```