src/ZF/ex/LListFn.thy
author lcp
Tue Aug 16 18:58:42 1994 +0200 (1994-08-16)
changeset 532 851df239ac8b
parent 120 09287f26bfb8
permissions -rw-r--r--
ZF/Makefile,ROOT.ML, ZF/ex/Integ.thy: updated for EquivClass
clasohm@0
     1
(*  Title: 	ZF/ex/llist-fn.thy
clasohm@0
     2
    ID:         $Id$
clasohm@0
     3
    Author: 	Lawrence C Paulson, Cambridge University Computer Laboratory
clasohm@0
     4
    Copyright   1993  University of Cambridge
clasohm@0
     5
clasohm@0
     6
Functions for Lazy Lists in Zermelo-Fraenkel Set Theory 
lcp@120
     7
lcp@120
     8
STILL NEEDS:
lcp@120
     9
co_recursion for defining lconst, flip, etc.
lcp@120
    10
a typing rule for it, based on some notion of "productivity..."
clasohm@0
    11
*)
clasohm@0
    12
lcp@120
    13
LListFn = LList + LList_Eq +
clasohm@0
    14
consts
clasohm@0
    15
  lconst   :: "i => i"
lcp@120
    16
  flip     :: "i => i"
clasohm@0
    17
clasohm@0
    18
rules
clasohm@0
    19
  lconst_def  "lconst(a) == lfp(univ(a), %l. LCons(a,l))"
clasohm@0
    20
lcp@120
    21
  flip_LNil   "flip(LNil) = LNil"
lcp@120
    22
lcp@120
    23
  flip_LCons  "[| x:bool; l: llist(bool) |] ==> \
lcp@120
    24
\              flip(LCons(x,l)) = LCons(not(x), flip(l))"
lcp@120
    25
clasohm@0
    26
end