# HG changeset patch
# User huffman
# Date 1267631752 28800
# Node ID bb088a6fafbce703eb4ca825a96fc8f2a882ec11
# Parent  5da670d57118ee1ee45962f4fb0d55e8ea106f33
add_axioms returns an iso_info; add_theorems takes an iso_info as an argument

diff -r 5da670d57118 -r bb088a6fafbc src/HOLCF/Tools/Domain/domain_axioms.ML
--- a/src/HOLCF/Tools/Domain/domain_axioms.ML	Wed Mar 03 07:36:31 2010 -0800
+++ b/src/HOLCF/Tools/Domain/domain_axioms.ML	Wed Mar 03 07:55:52 2010 -0800
@@ -18,8 +18,8 @@
       string Symtab.table -> (int -> term) -> Datatype.dtyp -> term
 
   val add_axioms :
-      (binding * (typ * typ)) list ->
-      theory -> theory
+      (binding * (typ * typ)) list -> theory ->
+      Domain_Take_Proofs.iso_info list * theory
 end;
 
 
@@ -146,7 +146,7 @@
           (map fst dom_eqns ~~ #take_consts take_info) thy;
 
   in
-    thy (* TODO: also return iso_infos, take_info, lub_take_thms *)
+    (iso_infos, thy) (* TODO: also return take_info, lub_take_thms *)
   end;
 
 end; (* struct *)
diff -r 5da670d57118 -r bb088a6fafbc src/HOLCF/Tools/Domain/domain_extender.ML
--- a/src/HOLCF/Tools/Domain/domain_extender.ML	Wed Mar 03 07:36:31 2010 -0800
+++ b/src/HOLCF/Tools/Domain/domain_extender.ML	Wed Mar 03 07:55:52 2010 -0800
@@ -184,13 +184,14 @@
     fun mk_eq_typ (_, cons) = foldr1 mk_ssumT (map mk_con_typ cons);
     val repTs : typ list = map mk_eq_typ eqs';
     val dom_eqns : (binding * (typ * typ)) list = dbinds ~~ (dts ~~ repTs);
-    val thy = Domain_Axioms.add_axioms dom_eqns thy;
+    val (iso_infos, thy) =
+        Domain_Axioms.add_axioms dom_eqns thy;
 
     val ((rewss, take_rews), theorems_thy) =
         thy
-          |> fold_map (fn (eq, (x,cs)) =>
-                Domain_Theorems.theorems (eq, eqs) (Type x, cs))
-             (eqs ~~ eqs')
+          |> fold_map (fn ((eq, (x,cs)), info) =>
+                Domain_Theorems.theorems (eq, eqs) (Type x, cs) info)
+             (eqs ~~ eqs' ~~ iso_infos)
           ||>> Domain_Theorems.comp_theorems (comp_dnam, eqs);
   in
     theorems_thy
@@ -264,9 +265,9 @@
         map (fn (dtnvs,cons') => (dtnvs, map one_con cons')) eqs';
     val ((rewss, take_rews), theorems_thy) =
         thy
-          |> fold_map (fn (eq, (x,cs)) =>
-               Domain_Theorems.theorems (eq, eqs) (Type x, cs))
-             (eqs ~~ eqs')
+          |> fold_map (fn ((eq, (x,cs)), info) =>
+               Domain_Theorems.theorems (eq, eqs) (Type x, cs) info)
+             (eqs ~~ eqs' ~~ iso_infos)
           ||>> Domain_Theorems.comp_theorems (comp_dnam, eqs);
   in
     theorems_thy
diff -r 5da670d57118 -r bb088a6fafbc src/HOLCF/Tools/Domain/domain_theorems.ML
--- a/src/HOLCF/Tools/Domain/domain_theorems.ML	Wed Mar 03 07:36:31 2010 -0800
+++ b/src/HOLCF/Tools/Domain/domain_theorems.ML	Wed Mar 03 07:55:52 2010 -0800
@@ -12,6 +12,7 @@
   val theorems:
     Domain_Library.eq * Domain_Library.eq list
     -> typ * (binding * (bool * binding option * typ) list * mixfix) list
+    -> Domain_Take_Proofs.iso_info
     -> theory -> thm list * theory;
 
   val comp_theorems: bstring * Domain_Library.eq list -> theory -> thm list * theory;
@@ -102,6 +103,7 @@
 fun theorems
     (((dname, _), cons) : eq, eqs : eq list)
     (dom_eqn : typ * (binding * (bool * binding option * typ) list * mixfix) list)
+    (iso_info : Domain_Take_Proofs.iso_info)
     (thy : theory) =
 let
 
@@ -111,11 +113,15 @@
 
 (* ----- getting the axioms and definitions --------------------------------- *)
 
+val ax_abs_iso = #abs_inverse iso_info;
+val ax_rep_iso = #rep_inverse iso_info;
+
+val abs_const = #abs_const iso_info;
+val rep_const = #rep_const iso_info;
+
 local
   fun ga s dn = PureThy.get_thm thy (dn ^ "." ^ s);
 in
-  val ax_abs_iso  = ga "abs_iso"  dname;
-  val ax_rep_iso  = ga "rep_iso"  dname;
   val ax_take_0      = ga "take_0" dname;
   val ax_take_Suc    = ga "take_Suc" dname;
   val ax_take_strict = ga "take_strict" dname;
@@ -123,32 +129,6 @@
 
 (* ----- define constructors ------------------------------------------------ *)
 
-val lhsT = fst dom_eqn;
-
-val rhsT =
-  let
-    fun mk_arg_typ (lazy, sel, T) = if lazy then mk_uT T else T;
-    fun mk_con_typ (bind, args, mx) =
-        if null args then oneT else foldr1 mk_sprodT (map mk_arg_typ args);
-    fun mk_eq_typ (_, cons) = foldr1 mk_ssumT (map mk_con_typ cons);
-  in
-    mk_eq_typ dom_eqn
-  end;
-
-val rep_const = Const(dname^"_rep", lhsT ->> rhsT);
-
-val abs_const = Const(dname^"_abs", rhsT ->> lhsT);
-
-val iso_info : Domain_Take_Proofs.iso_info =
-  {
-    absT = lhsT,
-    repT = rhsT,
-    abs_const = abs_const,
-    rep_const = rep_const,
-    abs_inverse = ax_abs_iso,
-    rep_inverse = ax_rep_iso
-  };
-
 val (result, thy) =
   Domain_Constructors.add_domain_constructors
     (Long_Name.base_name dname) (snd dom_eqn) iso_info thy;