[TYPES] ordering lemmas about powerdomain operations

[Brian Huffman]

Hello all,

I have been formalizing some properties of powerdomains and their  
operations in the Isabelle theorem prover. For example, one of the  
lemmas that I have proved is the following one about the upper  
powerdomain:

xs + ys << {z} if and only if xs << {z} or ys << {z}

where (+) is the binary union operation, {-} is the monadic unit or  
singleton, and (<<) is the information-ordering relation.

Someone must have proved some ordering lemmas like this previously,  
but I haven't come across any in the papers I have looked at.  
Descriptions of upper or lower powerdomains usually mention that they  
are semilattices with the binary union acting as the meet or join;  
being a semilattice entails a bunch of lemmas about (+) alone, but  
doesn't say anything about properties of (+) combined with {-} as in  
my example above.

Does anyone have a reference to a paper that proves (or even just  
lists) any of these ordering lemmas for powerdomains?

- Brian Huffman