# HG changeset patch
# User huffman
# Date 1239388521 25200
# Node ID a7cc0ef93269cb575ffdd6be3c17e17ae3259cf6
# Parent  fde434961f576b1a3e675c083f810e983dcbdafa
set up domain package in Domain.thy

diff -r fde434961f57 -r a7cc0ef93269 src/HOLCF/Domain.thy
--- a/src/HOLCF/Domain.thy	Wed Apr 08 20:29:15 2009 +0200
+++ b/src/HOLCF/Domain.thy	Fri Apr 10 11:35:21 2009 -0700
@@ -6,6 +6,14 @@
 
 theory Domain
 imports Ssum Sprod Up One Tr Fixrec
+uses
+  ("Tools/cont_consts.ML")
+  ("Tools/cont_proc.ML")
+  ("Tools/domain/domain_library.ML")
+  ("Tools/domain/domain_syntax.ML")
+  ("Tools/domain/domain_axioms.ML")
+  ("Tools/domain/domain_theorems.ML")
+  ("Tools/domain/domain_extender.ML")
 begin
 
 defaultsort pcpo
@@ -193,4 +201,15 @@
 
 lemmas exh_casedists = exh_casedist1 exh_casedist2 exh_casedist3
 
+
+subsection {* Installing the domain package *}
+
+use "Tools/cont_consts.ML"
+use "Tools/cont_proc.ML"
+use "Tools/domain/domain_library.ML"
+use "Tools/domain/domain_syntax.ML"
+use "Tools/domain/domain_axioms.ML"
+use "Tools/domain/domain_theorems.ML"
+use "Tools/domain/domain_extender.ML"
+
 end
diff -r fde434961f57 -r a7cc0ef93269 src/HOLCF/HOLCF.thy
--- a/src/HOLCF/HOLCF.thy	Wed Apr 08 20:29:15 2009 +0200
+++ b/src/HOLCF/HOLCF.thy	Fri Apr 10 11:35:21 2009 -0700
@@ -9,13 +9,6 @@
   Domain ConvexPD Algebraic Universal Sum_Cpo Main
 uses
   "holcf_logic.ML"
-  "Tools/cont_consts.ML"
-  "Tools/cont_proc.ML"
-  "Tools/domain/domain_library.ML"
-  "Tools/domain/domain_syntax.ML"
-  "Tools/domain/domain_axioms.ML"
-  "Tools/domain/domain_theorems.ML"
-  "Tools/domain/domain_extender.ML"
   "Tools/adm_tac.ML"
 begin
 
diff -r fde434961f57 -r a7cc0ef93269 src/HOLCF/Tools/cont_consts.ML
--- a/src/HOLCF/Tools/cont_consts.ML	Wed Apr 08 20:29:15 2009 +0200
+++ b/src/HOLCF/Tools/cont_consts.ML	Fri Apr 10 11:35:21 2009 -0700
@@ -18,8 +18,6 @@
 
 (* misc utils *)
 
-open HOLCFLogic;
-
 fun first  (x,_,_) = x;
 fun second (_,x,_) = x;
 fun third  (_,_,x) = x;
@@ -66,7 +64,7 @@
             (c2,change_arrow n T,mx   ),
             trans_rules c2 c n mx) end;
 
-fun cfun_arity (Type(n,[_,T])) = if n = cfun_arrow then 1+cfun_arity T else 0
+fun cfun_arity (Type(n,[_,T])) = if n = @{type_name "->"} then 1+cfun_arity T else 0
 |   cfun_arity _               = 0;
 
 fun is_contconst (_,_,NoSyn   ) = false
diff -r fde434961f57 -r a7cc0ef93269 src/HOLCF/Tools/domain/domain_library.ML
--- a/src/HOLCF/Tools/domain/domain_library.ML	Wed Apr 08 20:29:15 2009 +0200
+++ b/src/HOLCF/Tools/domain/domain_library.ML	Fri Apr 10 11:35:21 2009 -0700
@@ -34,8 +34,6 @@
 
 structure Domain_Library = struct
 
-open HOLCFLogic;
-
 exception Impossible of string;
 fun Imposs msg = raise Impossible ("Domain:"^msg);
 
@@ -72,7 +70,7 @@
       | index_vnames([],occupied) = [];
 in index_vnames(map nonreserved ids, [("O",0),("o",0)]) end;
 
-fun pcpo_type sg t = Sign.of_sort sg (Sign.certify_typ sg t, pcpoS);
+fun pcpo_type sg t = Sign.of_sort sg (Sign.certify_typ sg t, @{sort pcpo});
 fun string_of_typ sg = Syntax.string_of_typ_global sg o Sign.certify_typ sg;
 
 (* ----- constructor list handling ----- *)
@@ -99,6 +97,17 @@
 (* ----- support for type and mixfix expressions ----- *)
 
 infixr 5 -->;
+fun mk_uT T = Type(@{type_name "u"}, [T]);
+fun mk_cfunT (T, U) = Type(@{type_name "->"}, [T, U]);
+fun mk_sprodT (T, U) = Type(@{type_name "**"}, [T, U]);
+fun mk_ssumT (T, U) = Type(@{type_name "++"}, [T, U]);
+val oneT = @{typ one};
+val trT = @{typ tr};
+
+infixr 6 ->>;
+val op ->> = mk_cfunT;
+
+fun mk_TFree s = TFree ("'" ^ s, @{sort pcpo});
 
 (* ----- support for term expressions ----- *)