src/HOLCF/one.thy
author paulson
Mon Dec 07 18:26:25 1998 +0100 (1998-12-07)
changeset 6019 0e55c2fb2ebb
parent 243 c22b85994e17
permissions -rw-r--r--
tidying
     1 (*  Title: 	HOLCF/one.thy
     2     ID:         $Id$
     3     Author: 	Franz Regensburger
     4     Copyright   1993 Technische Universitaet Muenchen
     5 
     6 Introduve atomic type one = (void)u
     7 
     8 This is the first type that is introduced using a domain isomorphism.
     9 The type axiom 
    10 
    11 	arities one :: pcpo
    12 
    13 and the continuity of the Isomorphisms are taken for granted. Since the
    14 type is not recursive, it could be easily introduced in a purely conservative
    15 style as it was used for the types sprod, ssum, lift. The definition of the 
    16 ordering is canonical using abstraction and representation, but this would take
    17 again a lot of internal constants. It can easily be seen that the axioms below
    18 are consistent.
    19 
    20 The partial ordering on type one is implicitly defined via the
    21 isomorphism axioms and the continuity of abs_one and rep_one.
    22 
    23 We could also introduce the function less_one with definition
    24 
    25 less_one(x,y) = rep_one[x] << rep_one[y]
    26 
    27 
    28 *)
    29 
    30 One = ccc1+
    31 
    32 types one 0
    33 arities one :: pcpo
    34 
    35 consts
    36 	abs_one		:: "(void)u -> one"
    37 	rep_one		:: "one -> (void)u"
    38 	one 		:: "one"
    39 	one_when 	:: "'c -> one -> 'c"
    40 
    41 rules
    42   abs_one_iso	"abs_one[rep_one[u]] = u"
    43   rep_one_iso  "rep_one[abs_one[x]] = x"
    44 
    45   one_def	"one == abs_one[up[UU]]"
    46   one_when_def "one_when == (LAM c u.lift[LAM x.c][rep_one[u]])"
    47 
    48 end
    49 
    50 
    51 
    52 
    53