merged

--- a/src/HOLCF/Tools/domain/domain_library.ML	Mon Apr 27 11:27:19 2009 +0200
+++ b/src/HOLCF/Tools/domain/domain_library.ML	Mon Apr 27 07:26:17 2009 -0700
@@ -30,9 +30,129 @@
     | _				    => [thm];
 in map zero_var_indexes (at thm) end;
 
+(* infix syntax *)
+
+infixr 5 -->;
+infixr 6 ->>;
+infixr 0 ===>;
+infixr 0 ==>;
+infix 0 ==;
+infix 1 ===;
+infix 1 ~=;
+infix 1 <<;
+infix 1 ~<<;
+
+infix 9 `  ;
+infix 9 `% ;
+infix 9 `%%;
+
+
 (* ----- specific support for domain ---------------------------------------- *)
 
-structure Domain_Library = struct
+signature DOMAIN_LIBRARY =
+sig
+  val Imposs : string -> 'a;
+  val pcpo_type : theory -> typ -> bool;
+  val string_of_typ : theory -> typ -> string;
+
+  (* Creating HOLCF types *)
+  val mk_cfunT : typ * typ -> typ;
+  val ->> : typ * typ -> typ;
+  val mk_ssumT : typ * typ -> typ;
+  val mk_sprodT : typ * typ -> typ;
+  val mk_uT : typ -> typ;
+  val oneT : typ;
+  val trT : typ;
+  val mk_maybeT : typ -> typ;
+  val mk_ctupleT : typ list -> typ;
+  val mk_TFree : string -> typ;
+  val pcpoS : sort;
+
+  (* Creating HOLCF terms *)
+  val %: : string -> term;
+  val %%: : string -> term;
+  val ` : term * term -> term;
+  val `% : term * string -> term;
+  val /\ : string -> term -> term;
+  val UU : term;
+  val TT : term;
+  val FF : term;
+  val mk_up : term -> term;
+  val mk_sinl : term -> term;
+  val mk_sinr : term -> term;
+  val mk_stuple : term list -> term;
+  val mk_ctuple : term list -> term;
+  val mk_fix : term -> term;
+  val mk_iterate : term * term * term -> term;
+  val mk_fail : term;
+  val mk_return : term -> term;
+  val cproj : term -> 'a list -> int -> term;
+  val list_ccomb : term * term list -> term;
+  val con_app : string -> ('a * 'b * string) list -> term;
+  val con_app2 : string -> ('a -> term) -> 'a list -> term;
+  val proj : term -> 'a list -> int -> term;
+  val prj : ('a -> 'b -> 'a) -> ('a -> 'b -> 'a) -> 'a -> 'b list -> int -> 'a;
+  val mk_ctuple_pat : term list -> term;
+  val mk_branch : term -> term;
+
+  (* Creating propositions *)
+  val mk_conj : term * term -> term;
+  val mk_disj : term * term -> term;
+  val mk_imp : term * term -> term;
+  val mk_lam : string * term -> term;
+  val mk_all : string * term -> term;
+  val mk_ex : string * term -> term;
+  val mk_constrain : typ * term -> term;
+  val mk_constrainall : string * typ * term -> term;
+  val === : term * term -> term;
+  val << : term * term -> term;
+  val ~<< : term * term -> term;
+  val strict : term -> term;
+  val defined : term -> term;
+  val mk_adm : term -> term;
+  val mk_compact : term -> term;
+  val lift : ('a -> term) -> 'a list * term -> term;
+  val lift_defined : ('a -> term) -> 'a list * term -> term;
+
+  (* Creating meta-propositions *)
+  val mk_trp : term -> term; (* HOLogic.mk_Trueprop *)
+  val == : term * term -> term;
+  val ===> : term * term -> term;
+  val ==> : term * term -> term;
+  val mk_All : string * term -> term;
+
+  (* Domain specifications *)
+  type arg = (bool * int * DatatypeAux.dtyp) * string option * string;
+  type cons = string * arg list;
+  type eq = (string * typ list) * cons list;
+  val is_lazy : arg -> bool;
+  val rec_of : arg -> int;
+  val sel_of : arg -> string option;
+  val vname : arg -> string;
+  val upd_vname : (string -> string) -> arg -> arg;
+  val is_rec : arg -> bool;
+  val is_nonlazy_rec : arg -> bool;
+  val nonlazy : arg list -> string list;
+  val nonlazy_rec : arg list -> string list;
+  val %# : arg -> term;
+  val /\# : arg * term -> term;
+  val when_body : cons list -> (int * int -> term) -> term;
+  val when_funs : 'a list -> string list;
+  val bound_arg : ''a list -> ''a -> term; (* ''a = arg or string *)
+  val idx_name : 'a list -> string -> int -> string;
+  val app_rec_arg : (int -> term) -> arg -> term;
+
+  (* Name mangling *)
+  val strip_esc : string -> string;
+  val extern_name : string -> string;
+  val dis_name : string -> string;
+  val mat_name : string -> string;
+  val pat_name : string -> string;
+  val mk_var_names : string list -> string list;
+end;
+
+structure Domain_Library : DOMAIN_LIBRARY =
+struct
 
 exception Impossible of string;
 fun Imposs msg = raise Impossible ("Domain:"^msg);
@@ -75,14 +195,19 @@
 
 (* ----- constructor list handling ----- *)
 
-type cons = (string *				(* operator name of constr *)
-	    ((bool*int*DatatypeAux.dtyp)*	(*  (lazy,recursive element or ~1) *)
-	      string option*			(*   selector name    *)
-	      string)				(*   argument name    *)
-	    list);				(* argument list      *)
-type eq = (string *		(* name      of abstracted type *)
-	   typ list) *		(* arguments of abstracted type *)
-	  cons list;		(* represented type, as a constructor list *)
+type arg =
+  (bool * int * DatatypeAux.dtyp) *	(*  (lazy,recursive element or ~1) *)
+  string option *			(*   selector name    *)
+  string;				(*   argument name    *)
+
+type cons =
+  string *				(* operator name of constr *)
+  arg list;				(* argument list      *)
+
+type eq =
+  (string *		(* name      of abstracted type *)
+   typ list) *		(* arguments of abstracted type *)
+  cons list;		(* represented type, as a constructor list *)
 
 fun rec_of arg  = second (first arg);
 fun is_lazy arg = first (first arg);
@@ -96,7 +221,6 @@
 
 (* ----- 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]);
@@ -104,7 +228,6 @@
 val oneT = @{typ one};
 val trT = @{typ tr};
 
-infixr 6 ->>;
 val op ->> = mk_cfunT;
 
 fun mk_TFree s = TFree ("'" ^ s, @{sort pcpo});

--- a/src/HOLCF/Tools/domain/domain_theorems.ML	Mon Apr 27 11:27:19 2009 +0200
+++ b/src/HOLCF/Tools/domain/domain_theorems.ML	Mon Apr 27 07:26:17 2009 -0700
@@ -8,7 +8,14 @@
 
 val HOLCF_ss = @{simpset};
 
-structure Domain_Theorems = struct
+signature DOMAIN_THEOREMS =
+sig
+  val theorems: Domain_Library.eq * Domain_Library.eq list -> theory -> thm list * theory;
+  val comp_theorems: bstring * Domain_Library.eq list -> theory -> thm list * theory;
+end;
+
+structure Domain_Theorems : DOMAIN_THEOREMS =
+struct
 
 val quiet_mode = ref false;
 val trace_domain = ref false;
@@ -608,23 +615,22 @@
 in
   thy
     |> Sign.add_path (Long_Name.base_name dname)
-    |> (snd o PureThy.add_thmss [
-        ((Binding.name "iso_rews" , iso_rews  ), [Simplifier.simp_add]),
-        ((Binding.name "exhaust"  , [exhaust] ), []),
-        ((Binding.name "casedist" , [casedist]), [Induct.cases_type dname]),
-        ((Binding.name "when_rews", when_rews ), [Simplifier.simp_add]),
-        ((Binding.name "compacts", con_compacts), [Simplifier.simp_add]),
-        ((Binding.name "con_rews", con_rews), [Simplifier.simp_add]),
-        ((Binding.name "sel_rews", sel_rews), [Simplifier.simp_add]),
-        ((Binding.name "dis_rews", dis_rews), [Simplifier.simp_add]),
-        ((Binding.name "pat_rews", pat_rews), [Simplifier.simp_add]),
-        ((Binding.name "dist_les", dist_les), [Simplifier.simp_add]),
-        ((Binding.name "dist_eqs", dist_eqs), [Simplifier.simp_add]),
-        ((Binding.name "inverts" , inverts ), [Simplifier.simp_add]),
-        ((Binding.name "injects" , injects ), [Simplifier.simp_add]),
-        ((Binding.name "copy_rews", copy_rews), [Simplifier.simp_add]),
-        ((Binding.name "match_rews", mat_rews), [Simplifier.simp_add])
-       ])
+    |> snd o PureThy.add_thmss [
+        ((Binding.name "iso_rews"  , iso_rews    ), [Simplifier.simp_add]),
+        ((Binding.name "exhaust"   , [exhaust]   ), []),
+        ((Binding.name "casedist"  , [casedist]  ), [Induct.cases_type dname]),
+        ((Binding.name "when_rews" , when_rews   ), [Simplifier.simp_add]),
+        ((Binding.name "compacts"  , con_compacts), [Simplifier.simp_add]),
+        ((Binding.name "con_rews"  , con_rews    ), [Simplifier.simp_add]),
+        ((Binding.name "sel_rews"  , sel_rews    ), [Simplifier.simp_add]),
+        ((Binding.name "dis_rews"  , dis_rews    ), [Simplifier.simp_add]),
+        ((Binding.name "pat_rews"  , pat_rews    ), [Simplifier.simp_add]),
+        ((Binding.name "dist_les"  , dist_les    ), [Simplifier.simp_add]),
+        ((Binding.name "dist_eqs"  , dist_eqs    ), [Simplifier.simp_add]),
+        ((Binding.name "inverts"   , inverts     ), [Simplifier.simp_add]),
+        ((Binding.name "injects"   , injects     ), [Simplifier.simp_add]),
+        ((Binding.name "copy_rews" , copy_rews   ), [Simplifier.simp_add]),
+        ((Binding.name "match_rews", mat_rews    ), [Simplifier.simp_add])]
     |> Sign.parent_path
     |> pair (iso_rews @ when_rews @ con_rews @ sel_rews @ dis_rews @
         pat_rews @ dist_les @ dist_eqs @ copy_rews)
@@ -1004,14 +1010,14 @@
 fun ind_rule (dname, rule) = ((Binding.empty, [rule]), [Induct.induct_type dname]);
 
 in thy |> Sign.add_path comp_dnam
-       |> (snd o (PureThy.add_thmss (map (Thm.no_attributes o apfst Binding.name) [
-		("take_rews"  , take_rews  ),
-		("take_lemmas", take_lemmas),
-		("finites"    , finites    ),
-		("finite_ind", [finite_ind]),
-		("ind"       , [ind       ]),
-		("coind"     , [coind     ])])))
-       |> (snd o (PureThy.add_thmss (map ind_rule (dnames ~~ inducts))))
+       |> snd o PureThy.add_thmss [
+           ((Binding.name "take_rews"  , take_rews   ), [Simplifier.simp_add]),
+           ((Binding.name "take_lemmas", take_lemmas ), []),
+           ((Binding.name "finites"    , finites     ), []),
+           ((Binding.name "finite_ind" , [finite_ind]), []),
+           ((Binding.name "ind"        , [ind]       ), []),
+           ((Binding.name "coind"      , [coind]     ), [])]
+       |> snd o PureThy.add_thmss (map ind_rule (dnames ~~ inducts))
        |> Sign.parent_path |> pair take_rews
 end; (* let *)
 end; (* local *)