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