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
lcp@515
     1
(*  Title: 	ZF/ex/CoUnit.ML
lcp@515
     2
    ID:         $Id$
lcp@515
     3
    Author: 	Lawrence C Paulson, Cambridge University Computer Laboratory
lcp@515
     4
    Copyright   1994  University of Cambridge
lcp@515
     5
lcp@515
     6
Trivial codatatype definitions, one of which goes wrong!
lcp@515
     7
lcp@515
     8
See discussion in 
lcp@515
     9
  L C Paulson.  A Concrete Final Coalgebra Theorem for ZF Set Theory.
lcp@515
    10
  Report 334,  Cambridge University Computer Laboratory.  1994.
lcp@515
    11
*)
lcp@515
    12
lcp@515
    13
CoUnit = QUniv + "Datatype" +
lcp@515
    14
lcp@515
    15
(*This degenerate definition does not work well because the one constructor's
lcp@515
    16
  definition is trivial!  The same thing occurs with Aczel's Special Final
lcp@515
    17
  Coalgebra Theorem
lcp@515
    18
*)
lcp@515
    19
consts
lcp@515
    20
  counit :: "i"
lcp@515
    21
codatatype
lcp@515
    22
  "counit" = Con ("x: counit")
lcp@515
    23
lcp@515
    24
lcp@515
    25
(*A similar example, but the constructor is non-degenerate and it works!
lcp@515
    26
  The resulting set is a singleton.
lcp@515
    27
*)
lcp@515
    28
lcp@515
    29
consts
lcp@515
    30
  counit2 :: "i"
lcp@515
    31
codatatype
lcp@515
    32
  "counit2" = Con2 ("x: counit2", "y: counit2")
lcp@515
    33
lcp@515
    34
end