author | oheimb |
Fri, 13 Dec 1996 18:45:58 +0100 | |
changeset 2394 | 91d8abf108be |
parent 2291 | fbd14a05fb88 |
permissions | -rw-r--r-- |
1479 | 1 |
(* Title: HOLCF/tr1.thy |
243
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
2 |
ID: $Id$ |
1479 | 3 |
Author: Franz Regensburger |
243
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
4 |
Copyright 1993 Technische Universitaet Muenchen |
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
5 |
|
625 | 6 |
Introduce the domain of truth values tr = one ++ one |
243
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
7 |
|
625 | 8 |
The type is axiomatized as the least solution of a domain equation. |
9 |
The functor term that specifies the domain equation is: |
|
243
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
10 |
|
625 | 11 |
FT = <++,K_{one},K_{one}> |
243
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
12 |
|
625 | 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 |
|
243
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
17 |
|
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
18 |
*) |
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
19 |
|
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
20 |
Tr1 = One + |
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
21 |
|
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
22 |
types tr 0 |
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
23 |
arities tr :: pcpo |
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
24 |
|
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
25 |
consts |
1479 | 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" |
|
243
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
31 |
|
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
32 |
rules |
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
33 |
|
1479 | 34 |
abs_tr_iso "abs_tr`(rep_tr`u) = u" |
35 |
rep_tr_iso "rep_tr`(abs_tr`x) = x" |
|
243
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
36 |
|
1168
74be52691d62
The curried version of HOLCF is now just called HOLCF. The old
regensbu
parents:
625
diff
changeset
|
37 |
defs |
243
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
38 |
|
1479 | 39 |
TT_def "TT == abs_tr`(sinl`one)" |
40 |
FF_def "FF == abs_tr`(sinr`one)" |
|
243
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
41 |
|
1168
74be52691d62
The curried version of HOLCF is now just called HOLCF. The old
regensbu
parents:
625
diff
changeset
|
42 |
tr_when_def "tr_when == |
1479 | 43 |
(LAM e1 e2 t. sswhen`(LAM x.e1)`(LAM y.e2)`(rep_tr`t))" |
1274 | 44 |
|
1168
74be52691d62
The curried version of HOLCF is now just called HOLCF. The old
regensbu
parents:
625
diff
changeset
|
45 |
end |