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

src/HOLCF/One.thy

changeset 625 | 119391dd1d59 |

parent 243 | c22b85994e17 |

child 1168 | 74be52691d62 |

1.1 --- a/src/HOLCF/One.thy Tue Oct 04 13:02:16 1994 +0100 1.2 +++ b/src/HOLCF/One.thy Thu Oct 06 18:40:18 1994 +0100 1.3 @@ -3,27 +3,17 @@ 1.4 Author: Franz Regensburger 1.5 Copyright 1993 Technische Universitaet Muenchen 1.6 1.7 -Introduve atomic type one = (void)u 1.8 +Introduce atomic type one = (void)u 1.9 1.10 -This is the first type that is introduced using a domain isomorphism. 1.11 -The type axiom 1.12 - 1.13 - arities one :: pcpo 1.14 +The type is axiomatized as the least solution of a domain equation. 1.15 +The functor term that specifies the domain equation is: 1.16 1.17 -and the continuity of the Isomorphisms are taken for granted. Since the 1.18 -type is not recursive, it could be easily introduced in a purely conservative 1.19 -style as it was used for the types sprod, ssum, lift. The definition of the 1.20 -ordering is canonical using abstraction and representation, but this would take 1.21 -again a lot of internal constants. It can easily be seen that the axioms below 1.22 -are consistent. 1.23 + FT = <U,K_{void}> 1.24 1.25 -The partial ordering on type one is implicitly defined via the 1.26 -isomorphism axioms and the continuity of abs_one and rep_one. 1.27 +For details see chapter 5 of: 1.28 1.29 -We could also introduce the function less_one with definition 1.30 - 1.31 -less_one(x,y) = rep_one[x] << rep_one[y] 1.32 - 1.33 +[Franz Regensburger] HOLCF: Eine konservative Erweiterung von HOL um LCF, 1.34 + Dissertation, Technische Universit"at M"unchen, 1994 1.35 1.36 *) 1.37