src/HOLCF/one.thy

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOLCF/one.thy	Wed Jan 19 17:35:01 1994 +0100
@@ -0,0 +1,53 @@
+(*  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
+
+
+
+
+