src/HOLCF/One.thy

Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
in HOL.

(*  Title: 	HOLCF/one.thy
    ID:         $Id$
    Author: 	Franz Regensburger
    Copyright   1993 Technische Universitaet Muenchen

Introduve atomic type one = (void)u

This is the first type that is introduced using a domain isomorphism.
The type axiom 

	arities one :: pcpo

and the continuity of the Isomorphisms are taken for granted. Since the
type is not recursive, it could be easily introduced in a purely conservative
style as it was used for the types sprod, ssum, lift. The definition of the 
ordering is canonical using abstraction and representation, but this would take
again a lot of internal constants. It can easily be seen that the axioms below
are consistent.

The partial ordering on type one is implicitly defined via the
isomorphism axioms and the continuity of abs_one and rep_one.

We could also introduce the function less_one with definition

less_one(x,y) = rep_one[x] << rep_one[y]


*)

One = ccc1+

types one 0
arities one :: pcpo

consts
	abs_one		:: "(void)u -> one"
	rep_one		:: "one -> (void)u"
	one 		:: "one"
	one_when 	:: "'c -> one -> 'c"

rules
  abs_one_iso	"abs_one[rep_one[u]] = u"
  rep_one_iso  "rep_one[abs_one[x]] = x"

  one_def	"one == abs_one[up[UU]]"
  one_when_def "one_when == (LAM c u.lift[LAM x.c][rep_one[u]])"

end