summary |
shortlog |
changelog |
graph |
tags |
branches |
files |
changeset |
file |
revisions |
annotate |
diff |
raw

src/HOLCF/tr1.thy

author | paulson |

Mon Dec 07 18:26:25 1998 +0100 (1998-12-07) | |

changeset 6019 | 0e55c2fb2ebb |

parent 243 | c22b85994e17 |

permissions | -rw-r--r-- |

tidying

1 (* Title: HOLCF/tr1.thy

2 ID: $Id$

3 Author: Franz Regensburger

4 Copyright 1993 Technische Universitaet Muenchen

6 Introduve the domain of truth values tr = {UU,TT,FF}

8 This type is introduced using a domain isomorphism.

10 The type axiom

12 arities tr :: pcpo

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.

21 Partial Ordering is implicit in isomorphims abs_tr,rep_tr and their continuity

23 *)

25 Tr1 = One +

27 types tr 0

28 arities tr :: pcpo

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"

37 rules

39 abs_tr_iso "abs_tr[rep_tr[u]] = u"

40 rep_tr_iso "rep_tr[abs_tr[x]] = x"

42 TT_def "TT == abs_tr[sinl[one]]"

43 FF_def "FF == abs_tr[sinr[one]]"

45 tr_when_def "tr_when == (LAM e1 e2 t.when[LAM x.e1][LAM y.e2][rep_tr[t]])"

47 end