src/HOLCF/tr1.thy
author wenzelm
Thu Aug 27 20:46:36 1998 +0200 (1998-08-27)
changeset 5400 645f46a24c72
parent 243 c22b85994e17
permissions -rw-r--r--
made tutorial first;
     1 (*  Title: 	HOLCF/tr1.thy
     2     ID:         $Id$
     3     Author: 	Franz Regensburger
     4     Copyright   1993 Technische Universitaet Muenchen
     5 
     6 Introduve the domain of truth values tr = {UU,TT,FF}
     7 
     8 This type is introduced using a domain isomorphism.
     9 
    10 The type axiom 
    11 
    12 	arities tr :: pcpo
    13 
    14 and the continuity of the Isomorphisms are taken for granted. Since the
    15 type is not recursive, it could be easily introduced in a purely conservative
    16 style as it was used for the types sprod, ssum, lift. The definition of the 
    17 ordering is canonical using abstraction and representation, but this would take
    18 again a lot of internal constants. It can be easily seen that the axioms below
    19 are consistent.
    20 
    21 Partial Ordering is implicit in isomorphims abs_tr,rep_tr and their continuity
    22 
    23 *)
    24 
    25 Tr1 = One +
    26 
    27 types tr 0
    28 arities tr :: pcpo
    29 
    30 consts
    31 	abs_tr		:: "one ++ one -> tr"
    32 	rep_tr		:: "tr -> one ++ one"
    33 	TT 		:: "tr"
    34 	FF		:: "tr"
    35 	tr_when 	:: "'c -> 'c -> tr -> 'c"
    36 
    37 rules
    38 
    39   abs_tr_iso	"abs_tr[rep_tr[u]] = u"
    40   rep_tr_iso	"rep_tr[abs_tr[x]] = x"
    41 
    42   TT_def	"TT == abs_tr[sinl[one]]"
    43   FF_def	"FF == abs_tr[sinr[one]]"
    44 
    45   tr_when_def "tr_when == (LAM e1 e2 t.when[LAM x.e1][LAM y.e2][rep_tr[t]])"
    46 
    47 end
    48 
    49 
    50 
    51 
    52 
    53 
    54 
    55 
    56 
    57