src/HOLCF/One.thy
changeset 243 c22b85994e17
child 625 119391dd1d59
     1.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.2 +++ b/src/HOLCF/One.thy	Wed Jan 19 17:35:01 1994 +0100
     1.3 @@ -0,0 +1,53 @@
     1.4 +(*  Title: 	HOLCF/one.thy
     1.5 +    ID:         $Id$
     1.6 +    Author: 	Franz Regensburger
     1.7 +    Copyright   1993 Technische Universitaet Muenchen
     1.8 +
     1.9 +Introduve atomic type one = (void)u
    1.10 +
    1.11 +This is the first type that is introduced using a domain isomorphism.
    1.12 +The type axiom 
    1.13 +
    1.14 +	arities one :: pcpo
    1.15 +
    1.16 +and the continuity of the Isomorphisms are taken for granted. Since the
    1.17 +type is not recursive, it could be easily introduced in a purely conservative
    1.18 +style as it was used for the types sprod, ssum, lift. The definition of the 
    1.19 +ordering is canonical using abstraction and representation, but this would take
    1.20 +again a lot of internal constants. It can easily be seen that the axioms below
    1.21 +are consistent.
    1.22 +
    1.23 +The partial ordering on type one is implicitly defined via the
    1.24 +isomorphism axioms and the continuity of abs_one and rep_one.
    1.25 +
    1.26 +We could also introduce the function less_one with definition
    1.27 +
    1.28 +less_one(x,y) = rep_one[x] << rep_one[y]
    1.29 +
    1.30 +
    1.31 +*)
    1.32 +
    1.33 +One = ccc1+
    1.34 +
    1.35 +types one 0
    1.36 +arities one :: pcpo
    1.37 +
    1.38 +consts
    1.39 +	abs_one		:: "(void)u -> one"
    1.40 +	rep_one		:: "one -> (void)u"
    1.41 +	one 		:: "one"
    1.42 +	one_when 	:: "'c -> one -> 'c"
    1.43 +
    1.44 +rules
    1.45 +  abs_one_iso	"abs_one[rep_one[u]] = u"
    1.46 +  rep_one_iso  "rep_one[abs_one[x]] = x"
    1.47 +
    1.48 +  one_def	"one == abs_one[up[UU]]"
    1.49 +  one_when_def "one_when == (LAM c u.lift[LAM x.c][rep_one[u]])"
    1.50 +
    1.51 +end
    1.52 +
    1.53 +
    1.54 +
    1.55 +
    1.56 +