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