equal
deleted
inserted
replaced
1 (* Title: HOLCF/tr1.thy |
|
2 ID: $Id$ |
|
3 Author: Franz Regensburger |
|
4 Copyright 1993 Technische Universitaet Muenchen |
|
5 |
|
6 Introduce the domain of truth values tr = one ++ one |
|
7 |
|
8 The type is axiomatized as the least solution of a domain equation. |
|
9 The functor term that specifies the domain equation is: |
|
10 |
|
11 FT = <++,K_{one},K_{one}> |
|
12 |
|
13 For details see chapter 5 of: |
|
14 |
|
15 [Franz Regensburger] HOLCF: Eine konservative Erweiterung von HOL um LCF, |
|
16 Dissertation, Technische Universit"at M"unchen, 1994 |
|
17 |
|
18 *) |
|
19 |
|
20 Tr1 = One + |
|
21 |
|
22 types tr 0 |
|
23 arities tr :: pcpo |
|
24 |
|
25 consts |
|
26 abs_tr :: "one ++ one -> tr" |
|
27 rep_tr :: "tr -> one ++ one" |
|
28 TT :: "tr" |
|
29 FF :: "tr" |
|
30 tr_when :: "'c -> 'c -> tr -> 'c" |
|
31 |
|
32 rules |
|
33 |
|
34 abs_tr_iso "abs_tr`(rep_tr`u) = u" |
|
35 rep_tr_iso "rep_tr`(abs_tr`x) = x" |
|
36 |
|
37 defs |
|
38 |
|
39 TT_def "TT == abs_tr`(sinl`one)" |
|
40 FF_def "FF == abs_tr`(sinr`one)" |
|
41 |
|
42 tr_when_def "tr_when == |
|
43 (LAM e1 e2 t. sswhen`(LAM x.e1)`(LAM y.e2)`(rep_tr`t))" |
|
44 |
|
45 end |
|