src/ZF/ex/CoUnit.thy
author lcp
Tue Aug 16 18:58:42 1994 +0200 (1994-08-16)
changeset 532 851df239ac8b
parent 515 abcc438e7c27
child 810 91c68f74f458
permissions -rw-r--r--
ZF/Makefile,ROOT.ML, ZF/ex/Integ.thy: updated for EquivClass
     1 (*  Title: 	ZF/ex/CoUnit.ML
     2     ID:         $Id$
     3     Author: 	Lawrence C Paulson, Cambridge University Computer Laboratory
     4     Copyright   1994  University of Cambridge
     5 
     6 Trivial codatatype definitions, one of which goes wrong!
     7 
     8 See discussion in 
     9   L C Paulson.  A Concrete Final Coalgebra Theorem for ZF Set Theory.
    10   Report 334,  Cambridge University Computer Laboratory.  1994.
    11 *)
    12 
    13 CoUnit = QUniv + "Datatype" +
    14 
    15 (*This degenerate definition does not work well because the one constructor's
    16   definition is trivial!  The same thing occurs with Aczel's Special Final
    17   Coalgebra Theorem
    18 *)
    19 consts
    20   counit :: "i"
    21 codatatype
    22   "counit" = Con ("x: counit")
    23 
    24 
    25 (*A similar example, but the constructor is non-degenerate and it works!
    26   The resulting set is a singleton.
    27 *)
    28 
    29 consts
    30   counit2 :: "i"
    31 codatatype
    32   "counit2" = Con2 ("x: counit2", "y: counit2")
    33 
    34 end