# HG changeset patch
# User huffman
# Date 1268069823 28800
# Node ID 7a15e181bf3be5982b2fe9c2c8b4df45b8fae6f5
# Parent  f87132febfac789dc0d5f6bbb931e1150dc493d4
move proofs of reach and take lemmas to domain_take_proofs.ML

diff -r f87132febfac -r 7a15e181bf3b src/HOLCF/Tools/Domain/domain_axioms.ML
--- a/src/HOLCF/Tools/Domain/domain_axioms.ML	Mon Mar 08 09:33:05 2010 -0800
+++ b/src/HOLCF/Tools/Domain/domain_axioms.ML	Mon Mar 08 09:37:03 2010 -0800
@@ -120,6 +120,11 @@
         fold_map axiomatize_lub_take
           (map fst dom_eqns ~~ #take_consts take_info) thy;
 
+    (* prove additional take theorems *)
+    val (take_info2, thy) =
+        Domain_Take_Proofs.add_lub_take_theorems
+          (map fst dom_eqns ~~ iso_infos) take_info lub_take_thms thy;
+
   in
     (iso_infos, thy) (* TODO: also return take_info, lub_take_thms *)
   end;
diff -r f87132febfac -r 7a15e181bf3b src/HOLCF/Tools/Domain/domain_isomorphism.ML
--- a/src/HOLCF/Tools/Domain/domain_isomorphism.ML	Mon Mar 08 09:33:05 2010 -0800
+++ b/src/HOLCF/Tools/Domain/domain_isomorphism.ML	Mon Mar 08 09:37:03 2010 -0800
@@ -644,6 +644,10 @@
         fold_map prove_lub_take
           (dom_binds ~~ take_consts ~~ map_ID_thms ~~ dom_eqns) thy;
 
+    (* prove additional take theorems *)
+    val (take_info2, thy) =
+        Domain_Take_Proofs.add_lub_take_theorems
+          (dom_binds ~~ iso_infos) take_info lub_take_thms thy;
   in
     (iso_infos, thy)
   end;
diff -r f87132febfac -r 7a15e181bf3b src/HOLCF/Tools/Domain/domain_take_proofs.ML
--- a/src/HOLCF/Tools/Domain/domain_take_proofs.ML	Mon Mar 08 09:33:05 2010 -0800
+++ b/src/HOLCF/Tools/Domain/domain_take_proofs.ML	Mon Mar 08 09:37:03 2010 -0800
@@ -29,6 +29,10 @@
   val define_take_functions :
     (binding * iso_info) list -> theory -> take_info * theory
 
+  val add_lub_take_theorems :
+    (binding * iso_info) list -> take_info -> thm list ->
+    theory -> unit * theory
+
   val map_of_typ :
     theory -> (typ * term) list -> typ -> term
 
@@ -425,4 +429,50 @@
     (result, thy)
   end;
 
+fun add_lub_take_theorems
+    (spec : (binding * iso_info) list)
+    (take_info : take_info)
+    (lub_take_thms : thm list)
+    (thy : theory) =
+  let
+
+    (* retrieve components of spec *)
+    val dom_binds = map fst spec;
+    val iso_infos = map snd spec;
+    val dom_eqns = map (fn x => (#absT x, #repT x)) iso_infos;
+    val dnames = map Binding.name_of dom_binds;
+    val {chain_take_thms, deflation_take_thms, ...} = take_info;
+
+    (* prove take lemmas *)
+    fun prove_take_lemma ((chain_take, lub_take), dname) thy =
+      let
+        val take_lemma =
+            Drule.export_without_context
+              (@{thm lub_ID_take_lemma} OF [chain_take, lub_take]);
+      in
+        add_qualified_thm "take_lemma" (dname, take_lemma) thy
+      end;
+    val (take_lemma_thms, thy) =
+      fold_map prove_take_lemma
+        (chain_take_thms ~~ lub_take_thms ~~ dnames) thy;
+
+    (* prove reach lemmas *)
+    fun prove_reach_lemma ((chain_take, lub_take), dname) thy =
+      let
+        val thm =
+            Drule.export_without_context
+              (@{thm lub_ID_reach} OF [chain_take, lub_take]);
+      in
+        add_qualified_thm "reach" (dname, thm) thy
+      end;
+    val (reach_thms, thy) =
+      fold_map prove_reach_lemma
+        (chain_take_thms ~~ lub_take_thms ~~ dnames) thy;
+
+    val result = ();
+
+  in
+    (result, thy)
+  end;
+
 end;
diff -r f87132febfac -r 7a15e181bf3b src/HOLCF/Tools/Domain/domain_theorems.ML
--- a/src/HOLCF/Tools/Domain/domain_theorems.ML	Mon Mar 08 09:33:05 2010 -0800
+++ b/src/HOLCF/Tools/Domain/domain_theorems.ML	Mon Mar 08 09:37:03 2010 -0800
@@ -631,28 +631,9 @@
 
 local
   fun ga s dn = PureThy.get_thm thy (dn ^ "." ^ s);
-  val axs_chain_take = map (ga "chain_take") dnames;
-  val axs_lub_take   = map (ga "lub_take"  ) dnames;
-  fun take_thms ((ax_chain_take, ax_lub_take), dname) thy =
-    let
-      val dnam = Long_Name.base_name dname;
-      val take_lemma =
-          Drule.export_without_context
-            (@{thm lub_ID_take_lemma} OF [ax_chain_take, ax_lub_take]);
-      val reach =
-          Drule.export_without_context
-            (@{thm lub_ID_reach} OF [ax_chain_take, ax_lub_take]);
-      val thy =
-          thy |> Sign.add_path dnam
-              |> snd o PureThy.add_thms [
-                 ((Binding.name "take_lemma", take_lemma), []),
-                 ((Binding.name "reach"     , reach     ), [])]
-              |> Sign.parent_path;
-    in ((take_lemma, reach), thy) end;
 in
-  val ((take_lemmas, axs_reach), thy) =
-      fold_map take_thms (axs_chain_take ~~ axs_lub_take ~~ dnames) thy
-      |>> ListPair.unzip;
+  val take_lemmas = map (ga "take_lemma") dnames;
+  val axs_reach   = map (ga "reach"     ) dnames;
 end;
 
 val take_rews =