src/HOLCF/Tools/Domain/domain_isomorphism.ML

--- a/src/HOLCF/Tools/Domain/domain_isomorphism.ML	Sat Feb 27 20:56:19 2010 -0800
+++ b/src/HOLCF/Tools/Domain/domain_isomorphism.ML	Sat Feb 27 21:38:24 2010 -0800
@@ -6,9 +6,18 @@
 
 signature DOMAIN_ISOMORPHISM =
 sig
+  type iso_info =
+    {
+      repT : typ,
+      absT : typ,
+      rep_const : term,
+      abs_const : term,
+      rep_inverse : thm,
+      abs_inverse : thm
+    }
   val domain_isomorphism:
     (string list * binding * mixfix * typ * (binding * binding) option) list
-      -> theory -> theory
+      -> theory -> iso_info list * theory
   val domain_isomorphism_cmd:
     (string list * binding * mixfix * string * (binding * binding) option) list
       -> theory -> theory
@@ -298,6 +307,16 @@
 (******************************************************************************)
 (* prepare datatype specifications *)
 
+type iso_info =
+  {
+    repT : typ,
+    absT : typ,
+    rep_const : term,
+    abs_const : term,
+    rep_inverse : thm,
+    abs_inverse : thm
+  }
+
 fun read_typ thy str sorts =
   let
     val ctxt = ProofContext.init thy
@@ -320,7 +339,7 @@
     (prep_typ: theory -> 'a -> (string * sort) list -> typ * (string * sort) list)
     (doms_raw: (string list * binding * mixfix * 'a * (binding * binding) option) list)
     (thy: theory)
-    : theory =
+    : iso_info list * theory =
   let
     val _ = Theory.requires thy "Representable" "domain isomorphisms";
 
@@ -467,6 +486,22 @@
       |> fold_map mk_iso_thms (dom_binds ~~ REP_eq_thms ~~ rep_abs_defs)
       |>> ListPair.unzip;
 
+    (* collect info about rep/abs *)
+    val iso_info : iso_info list =
+      let
+        fun mk_info (((lhsT, rhsT), (repC, absC)), (rep_iso, abs_iso)) =
+          {
+            repT = rhsT,
+            absT = lhsT,
+            rep_const = repC,
+            abs_const = absC,
+            rep_inverse = rep_iso,
+            abs_inverse = abs_iso
+          };
+      in
+        map mk_info (dom_eqns ~~ rep_abs_consts ~~ iso_thms)
+      end
+
     (* declare map functions *)
     fun declare_map_const (tbind, (lhsT, rhsT)) thy =
       let
@@ -683,11 +718,11 @@
       fold_map prove_reach_thm (reach_thm_projs ~~ map_ID_thms ~~ dom_eqns);
 
   in
-    thy
+    (iso_info, thy)
   end;
 
 val domain_isomorphism = gen_domain_isomorphism cert_typ;
-val domain_isomorphism_cmd = gen_domain_isomorphism read_typ;
+val domain_isomorphism_cmd = snd oo gen_domain_isomorphism read_typ;
 
 (******************************************************************************)
 (******************************** outer syntax ********************************)