# HG changeset patch
# User huffman
# Date 1268079667 28800
# Node ID 3d8da9fac424eae374c3af1011611535fcc7cd11
# Parent  0537c34c6067ee9aa5e839c9c16eae008a2c2306
pass take_info as an argument to comp_theorems

diff -r 0537c34c6067 -r 3d8da9fac424 src/HOLCF/Tools/Domain/domain_axioms.ML
--- a/src/HOLCF/Tools/Domain/domain_axioms.ML	Mon Mar 08 11:58:40 2010 -0800
+++ b/src/HOLCF/Tools/Domain/domain_axioms.ML	Mon Mar 08 12:21:07 2010 -0800
@@ -17,6 +17,7 @@
   val add_axioms :
       (binding * (typ * typ)) list -> theory ->
       (Domain_Take_Proofs.iso_info list
+       * Domain_Take_Proofs.take_info
        * Domain_Take_Proofs.take_induct_info) * theory
 end;
 
@@ -127,7 +128,7 @@
           (map fst dom_eqns ~~ iso_infos) take_info lub_take_thms thy;
 
   in
-    ((iso_infos, take_info2), thy) (* TODO: also return take_info, lub_take_thms *)
+    ((iso_infos, take_info, take_info2), thy)
   end;
 
 end; (* struct *)
diff -r 0537c34c6067 -r 3d8da9fac424 src/HOLCF/Tools/Domain/domain_extender.ML
--- a/src/HOLCF/Tools/Domain/domain_extender.ML	Mon Mar 08 11:58:40 2010 -0800
+++ b/src/HOLCF/Tools/Domain/domain_extender.ML	Mon Mar 08 12:21:07 2010 -0800
@@ -184,7 +184,7 @@
     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 ((iso_infos, take_info2), thy) =
+    val ((iso_infos, take_info, take_info2), thy) =
         Domain_Axioms.add_axioms dom_eqns thy;
 
     val ((rewss, take_rews), theorems_thy) =
@@ -192,7 +192,7 @@
           |> 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) take_info2;
+          ||>> Domain_Theorems.comp_theorems (comp_dnam, eqs) take_info take_info2;
   in
     theorems_thy
       |> Sign.add_path (Long_Name.base_name comp_dnam)
@@ -246,7 +246,7 @@
         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);
     
-    val ((iso_infos, take_info2), thy) = thy |>
+    val ((iso_infos, take_info, take_info2), thy) = thy |>
       Domain_Isomorphism.domain_isomorphism
         (map (fn ((vs, dname, mx, _), eq) =>
                  (map fst vs, dname, mx, mk_eq_typ eq, NONE))
@@ -268,7 +268,7 @@
           |> 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) take_info2;
+          ||>> Domain_Theorems.comp_theorems (comp_dnam, eqs) take_info take_info2;
   in
     theorems_thy
       |> Sign.add_path (Long_Name.base_name comp_dnam)
diff -r 0537c34c6067 -r 3d8da9fac424 src/HOLCF/Tools/Domain/domain_isomorphism.ML
--- a/src/HOLCF/Tools/Domain/domain_isomorphism.ML	Mon Mar 08 11:58:40 2010 -0800
+++ b/src/HOLCF/Tools/Domain/domain_isomorphism.ML	Mon Mar 08 12:21:07 2010 -0800
@@ -11,6 +11,7 @@
        * (binding * binding) option) list ->
       theory ->
       (Domain_Take_Proofs.iso_info list
+       * Domain_Take_Proofs.take_info
        * Domain_Take_Proofs.take_induct_info) * theory
 
   val domain_isomorphism_cmd :
@@ -270,6 +271,7 @@
     (doms_raw: (string list * binding * mixfix * 'a * (binding * binding) option) list)
     (thy: theory)
     : (Domain_Take_Proofs.iso_info list
+       * Domain_Take_Proofs.take_info
        * Domain_Take_Proofs.take_induct_info) * theory =
   let
     val _ = Theory.requires thy "Representable" "domain isomorphisms";
@@ -654,7 +656,7 @@
         Domain_Take_Proofs.add_lub_take_theorems
           (dom_binds ~~ iso_infos) take_info lub_take_thms thy;
   in
-    ((iso_infos, take_info2), thy)
+    ((iso_infos, take_info, take_info2), thy)
   end;
 
 val domain_isomorphism = gen_domain_isomorphism cert_typ;
diff -r 0537c34c6067 -r 3d8da9fac424 src/HOLCF/Tools/Domain/domain_theorems.ML
--- a/src/HOLCF/Tools/Domain/domain_theorems.ML	Mon Mar 08 11:58:40 2010 -0800
+++ b/src/HOLCF/Tools/Domain/domain_theorems.ML	Mon Mar 08 12:21:07 2010 -0800
@@ -17,6 +17,7 @@
 
   val comp_theorems :
       bstring * Domain_Library.eq list ->
+      Domain_Take_Proofs.take_info ->
       Domain_Take_Proofs.take_induct_info ->
       theory -> thm list * theory
 
@@ -211,6 +212,7 @@
     (take_lemmas : thm list)
     (axs_reach : thm list)
     (take_rews : thm list)
+    (take_info : Domain_Take_Proofs.take_info)
     (thy : theory) =
 let
   val dnames = map (fst o fst) eqs;
@@ -229,12 +231,12 @@
     val axs_chain_take = map (ga "chain_take") dnames;
     val lub_take_thms = map (ga "lub_take") dnames;
     val axs_finite_def = map (ga "finite_def") dnames;
-    val take_0_thms = map (ga "take_0") dnames;
-    val take_Suc_thms = map (ga "take_Suc") dnames;
     val cases = map (ga  "casedist" ) dnames;
     val con_rews  = maps (gts "con_rews" ) dnames;
   end;
 
+  val {take_0_thms, take_Suc_thms, ...} = take_info;
+
   fun one_con p (con, args) =
     let
       val P_names = map P_name (1 upto (length dnames));
@@ -610,6 +612,7 @@
 
 fun comp_theorems
     (comp_dnam : string, eqs : eq list)
+    (take_info : Domain_Take_Proofs.take_info)
     (take_induct_info : Domain_Take_Proofs.take_induct_info)
     (thy : theory) =
 let
@@ -645,7 +648,7 @@
 (* prove induction rules, unless definition is indirect recursive *)
 val thy =
     if is_indirect then thy else
-    prove_induction (comp_dnam, eqs) take_lemmas axs_reach take_rews thy;
+    prove_induction (comp_dnam, eqs) take_lemmas axs_reach take_rews take_info thy;
 
 val thy =
     if is_indirect then thy else