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--
```     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
```