fixrec and repdef modules import holcf_library

--- a/src/HOLCF/Fixrec.thy	Tue Mar 02 17:34:03 2010 -0800
+++ b/src/HOLCF/Fixrec.thy	Tue Mar 02 18:16:28 2010 -0800
@@ -6,7 +6,9 @@
 
 theory Fixrec
 imports Sprod Ssum Up One Tr Fix
-uses ("Tools/fixrec.ML")
+uses
+  ("Tools/holcf_library.ML")
+  ("Tools/fixrec.ML")
 begin
 
 subsection {* Maybe monad type *}
@@ -603,6 +605,7 @@
 
 subsection {* Initializing the fixrec package *}
 
+use "Tools/holcf_library.ML"
 use "Tools/fixrec.ML"
 
 setup {* Fixrec.setup *}

--- a/src/HOLCF/Representable.thy	Tue Mar 02 17:34:03 2010 -0800
+++ b/src/HOLCF/Representable.thy	Tue Mar 02 18:16:28 2010 -0800
@@ -8,7 +8,6 @@
 imports Algebraic Universal Ssum Sprod One Fixrec
 uses
   ("Tools/repdef.ML")
-  ("Tools/holcf_library.ML")
   ("Tools/Domain/domain_take_proofs.ML")
   ("Tools/Domain/domain_isomorphism.ML")
 begin
@@ -778,7 +777,6 @@
 
 subsection {* Constructing Domain Isomorphisms *}
 
-use "Tools/holcf_library.ML"
 use "Tools/Domain/domain_take_proofs.ML"
 use "Tools/Domain/domain_isomorphism.ML"
 

--- a/src/HOLCF/Tools/fixrec.ML	Tue Mar 02 17:34:03 2010 -0800
+++ b/src/HOLCF/Tools/fixrec.ML	Tue Mar 02 18:16:28 2010 -0800
@@ -22,10 +22,15 @@
 structure Fixrec :> FIXREC =
 struct
 
+open HOLCF_Library;
+
+infixr 6 ->>;
+infix -->>;
+infix 9 `;
+
 val def_cont_fix_eq = @{thm def_cont_fix_eq};
 val def_cont_fix_ind = @{thm def_cont_fix_ind};
 
-
 fun fixrec_err s = error ("fixrec definition error:\n" ^ s);
 fun fixrec_eq_err thy s eq =
   fixrec_err (s ^ "\nin\n" ^ quote (Syntax.string_of_term_global thy eq));
@@ -34,23 +39,6 @@
 (***************************** building types ****************************)
 (*************************************************************************)
 
-(* ->> is taken from holcf_logic.ML *)
-fun cfunT (T, U) = Type(@{type_name cfun}, [T, U]);
-
-infixr 6 ->>; val (op ->>) = cfunT;
-
-fun dest_cfunT (Type(@{type_name cfun}, [T, U])) = (T, U)
-  | dest_cfunT T = raise TYPE ("dest_cfunT", [T], []);
-
-fun maybeT T = Type(@{type_name "maybe"}, [T]);
-
-fun dest_maybeT (Type(@{type_name "maybe"}, [T])) = T
-  | dest_maybeT T = raise TYPE ("dest_maybeT", [T], []);
-
-fun tupleT [] = HOLogic.unitT
-  | tupleT [T] = T
-  | tupleT (T :: Ts) = HOLogic.mk_prodT (T, tupleT Ts);
-
 local
 
 fun binder_cfun (Type(@{type_name cfun},[T, U])) = T :: binder_cfun U
@@ -64,12 +52,10 @@
 fun strip_cfun T : typ list * typ =
   (binder_cfun T, body_cfun T);
 
-fun cfunsT (Ts, U) = List.foldr cfunT U Ts;
-
 in
 
-fun matchT (T, U) =
-  body_cfun T ->> cfunsT (binder_cfun T, U) ->> U;
+fun matcherT (T, U) =
+  body_cfun T ->> (binder_cfun T -->> U) ->> U;
 
 end
 
@@ -86,43 +72,8 @@
 fun chead_of (Const(@{const_name Rep_CFun},_)$f$t) = chead_of f
   | chead_of u = u;
 
-fun capply_const (S, T) =
-  Const(@{const_name Rep_CFun}, (S ->> T) --> (S --> T));
-
-fun cabs_const (S, T) =
-  Const(@{const_name Abs_CFun}, (S --> T) --> (S ->> T));
-
-fun mk_cabs t =
-  let val T = Term.fastype_of t
-  in cabs_const (Term.domain_type T, Term.range_type T) $ t end
-
-fun mk_capply (t, u) =
-  let val (S, T) =
-    case Term.fastype_of t of
-        Type(@{type_name cfun}, [S, T]) => (S, T)
-      | _ => raise TERM ("mk_capply " ^ ML_Syntax.print_list ML_Syntax.print_term [t, u], [t, u]);
-  in capply_const (S, T) $ t $ u end;
-
 infix 0 ==;  val (op ==) = Logic.mk_equals;
 infix 1 ===; val (op ===) = HOLogic.mk_eq;
-infix 9 `  ; val (op `) = mk_capply;
-
-(* builds the expression (LAM v. rhs) *)
-fun big_lambda v rhs =
-  cabs_const (Term.fastype_of v, Term.fastype_of rhs) $ Term.lambda v rhs;
-
-(* builds the expression (LAM v1 v2 .. vn. rhs) *)
-fun big_lambdas [] rhs = rhs
-  | big_lambdas (v::vs) rhs = big_lambda v (big_lambdas vs rhs);
-
-fun mk_return t =
-  let val T = Term.fastype_of t
-  in Const(@{const_name Fixrec.return}, T ->> maybeT T) ` t end;
-
-fun mk_bind (t, u) =
-  let val (T, mU) = dest_cfunT (Term.fastype_of u);
-      val bindT = maybeT T ->> (T ->> mU) ->> mU;
-  in Const(@{const_name Fixrec.bind}, bindT) ` t ` u end;
 
 fun mk_mplus (t, u) =
   let val mT = Term.fastype_of t
@@ -130,31 +81,9 @@
 
 fun mk_run t =
   let val mT = Term.fastype_of t
-      val T = dest_maybeT mT
+      val T = dest_matchT mT
   in Const(@{const_name Fixrec.run}, mT ->> T) ` t end;
 
-fun mk_fix t =
-  let val (T, _) = dest_cfunT (Term.fastype_of t)
-  in Const(@{const_name fix}, (T ->> T) ->> T) ` t end;
-
-fun mk_cont t =
-  let val T = Term.fastype_of t
-  in Const(@{const_name cont}, T --> HOLogic.boolT) $ t end;
-
-val mk_fst = HOLogic.mk_fst
-val mk_snd = HOLogic.mk_snd
-
-(* builds the expression (v1,v2,..,vn) *)
-fun mk_tuple [] = HOLogic.unit
-|   mk_tuple (t::[]) = t
-|   mk_tuple (t::ts) = HOLogic.mk_prod (t, mk_tuple ts);
-
-(* builds the expression (%(v1,v2,..,vn). rhs) *)
-fun lambda_tuple [] rhs = Term.lambda (Free("unit", HOLogic.unitT)) rhs
-  | lambda_tuple (v::[]) rhs = Term.lambda v rhs
-  | lambda_tuple (v::vs) rhs =
-      HOLogic.mk_split (Term.lambda v (lambda_tuple vs rhs));
-
 
 (*************************************************************************)
 (************* fixed-point definitions and unfolding theorems ************)
@@ -292,7 +221,7 @@
           | result_type (Type (@{type_name "fun"},[_,T])) (x::xs) = result_type T xs
           | result_type T _ = T;
         val v = Free(n, result_type T vs);
-        val m = Const(match_name c, matchT (T, fastype_of rhs));
+        val m = Const(match_name c, matcherT (T, fastype_of rhs));
         val k = big_lambdas vs rhs;
       in
         (m`v`k, v, n::taken)
@@ -340,7 +269,7 @@
     val msum = foldr1 mk_mplus (map (unLAM arity) ms);
     val (Ts, U) = LAM_Ts arity (hd ms)
   in
-    reLAM (rev Ts, dest_maybeT U) (mk_run msum)
+    reLAM (rev Ts, dest_matchT U) (mk_run msum)
   end;
 
 (* this is the pattern-matching compiler function *)

--- a/src/HOLCF/Tools/repdef.ML	Tue Mar 02 17:34:03 2010 -0800
+++ b/src/HOLCF/Tools/repdef.ML	Tue Mar 02 18:16:28 2010 -0800
@@ -20,32 +20,28 @@
 structure Repdef :> REPDEF =
 struct
 
+open HOLCF_Library;
+
+infixr 6 ->>;
+infix -->>;
+
 (** type definitions **)
 
 type rep_info =
   { emb_def: thm, prj_def: thm, approx_def: thm, REP: thm };
 
-(* building terms *)
+(* building types and terms *)
 
-fun adm_const T = Const (@{const_name adm}, (T --> HOLogic.boolT) --> HOLogic.boolT);
-fun mk_adm (x, T, P) = adm_const T $ absfree (x, T, P);
-
-fun below_const T = Const (@{const_name below}, T --> T --> HOLogic.boolT);
-
-val natT = @{typ nat};
 val udomT = @{typ udom};
 fun alg_deflT T = Type (@{type_name alg_defl}, [T]);
-fun cfunT (T, U) = Type (@{type_name cfun}, [T, U]);
-fun emb_const T = Const (@{const_name emb}, cfunT (T, udomT));
-fun prj_const T = Const (@{const_name prj}, cfunT (udomT, T));
-fun approx_const T = Const (@{const_name approx}, natT --> cfunT (T, T));
+fun emb_const T = Const (@{const_name emb}, T ->> udomT);
+fun prj_const T = Const (@{const_name prj}, udomT ->> T);
+fun approx_const T = Const (@{const_name approx}, natT --> (T ->> T));
 
-fun LAM_const (T, U) = Const (@{const_name Abs_CFun}, (T --> U) --> cfunT (T, U));
-fun APP_const (T, U) = Const (@{const_name Rep_CFun}, cfunT (T, U) --> (T --> U));
-fun cast_const T = Const (@{const_name cast}, cfunT (alg_deflT T, cfunT (T, T)));
+fun cast_const T = Const (@{const_name cast}, alg_deflT T ->> T ->> T);
 fun mk_cast (t, x) =
-  APP_const (udomT, udomT)
-  $ (APP_const (alg_deflT udomT, cfunT (udomT, udomT)) $ cast_const udomT $ t)
+  capply_const (udomT, udomT)
+  $ (capply_const (alg_deflT udomT, udomT ->> udomT) $ cast_const udomT $ t)
   $ x;
 
 (* manipulating theorems *)
@@ -99,12 +95,12 @@
     (*definitions*)
     val Rep_const = Const (#Rep_name info, newT --> udomT);
     val Abs_const = Const (#Abs_name info, udomT --> newT);
-    val emb_eqn = Logic.mk_equals (emb_const newT, LAM_const (newT, udomT) $ Rep_const);
-    val prj_eqn = Logic.mk_equals (prj_const newT, LAM_const (udomT, newT) $
+    val emb_eqn = Logic.mk_equals (emb_const newT, cabs_const (newT, udomT) $ Rep_const);
+    val prj_eqn = Logic.mk_equals (prj_const newT, cabs_const (udomT, newT) $
       Abs ("x", udomT, Abs_const $ mk_cast (defl, Bound 0)));
     val repdef_approx_const =
       Const (@{const_name repdef_approx}, (newT --> udomT) --> (udomT --> newT)
-        --> alg_deflT udomT --> natT --> cfunT (newT, newT));
+        --> alg_deflT udomT --> natT --> (newT ->> newT));
     val approx_eqn = Logic.mk_equals (approx_const newT,
       repdef_approx_const $ Rep_const $ Abs_const $ defl);