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