implement map_of_typ using Pattern.rewrite_term

--- a/src/HOLCF/Tools/Domain/domain_isomorphism.ML	Tue Nov 09 04:47:46 2010 -0800
+++ b/src/HOLCF/Tools/Domain/domain_isomorphism.ML	Tue Nov 09 05:23:34 2010 -0800
@@ -55,20 +55,13 @@
   val description = "theorems like DEFL('a t) = t_defl$DEFL('a)"
 )
 
-structure MapIdData = Named_Thms
-(
-  val name = "domain_map_ID"
-  val description = "theorems like foo_map$ID = ID"
-);
-
 structure IsodeflData = Named_Thms
 (
   val name = "domain_isodefl"
   val description = "theorems like isodefl d t ==> isodefl (foo_map$d) (foo_defl$t)"
 );
 
-val setup =
-  RepData.setup #> MapIdData.setup #> IsodeflData.setup
+val setup = RepData.setup #> IsodeflData.setup
 
 
 (******************************************************************************)
@@ -656,9 +649,8 @@
       map prove_map_ID_thm
         (map_consts ~~ dom_eqns ~~ DEFL_thms ~~ isodefl_thms);
     val (_, thy) = thy |>
-      (Global_Theory.add_thms o map Thm.no_attributes)
+      (Global_Theory.add_thms o map (rpair [Domain_Take_Proofs.map_ID_add]))
         (map_ID_binds ~~ map_ID_thms);
-    val thy = fold (Context.theory_map o MapIdData.add_thm) map_ID_thms thy;
 
     (* definitions and proofs related to take functions *)
     val (take_info, thy) =
@@ -676,7 +668,7 @@
           list_ccomb (map_const, map mk_ID (filter is_cpo (snd (dest_Type lhsT))));
         val rhs = mk_tuple (map mk_map_ID (map_consts ~~ dom_eqns));
         val goal = mk_trp (mk_eq (lhs, rhs));
-        val map_ID_thms = MapIdData.get (ProofContext.init_global thy);
+        val map_ID_thms = Domain_Take_Proofs.get_map_ID_thms thy;
         val start_rules =
             @{thms thelub_Pair [symmetric] ch2ch_Pair} @ chain_take_thms
             @ @{thms pair_collapse split_def}

--- a/src/HOLCF/Tools/Domain/domain_take_proofs.ML	Tue Nov 09 04:47:46 2010 -0800
+++ b/src/HOLCF/Tools/Domain/domain_take_proofs.ML	Tue Nov 09 05:23:34 2010 -0800
@@ -59,6 +59,8 @@
   val get_map_tab : theory -> (string * bool list) Symtab.table
   val add_deflation_thm : thm -> theory -> theory
   val get_deflation_thms : theory -> thm list
+  val map_ID_add : attribute
+  val get_map_ID_thms : theory -> thm list
   val setup : theory -> theory
 end;
 
@@ -134,6 +136,12 @@
   val description = "theorems like deflation a ==> deflation (foo_map$a)"
 );
 
+structure Map_Id_Data = Named_Thms
+(
+  val name = "domain_map_ID"
+  val description = "theorems like foo_map$ID = ID"
+);
+
 fun add_map_function (tname, map_name, bs) =
     MapData.map (Symtab.insert (K true) (tname, (map_name, bs)));
 
@@ -143,7 +151,10 @@
 val get_map_tab = MapData.get;
 fun get_deflation_thms thy = DeflMapData.get (ProofContext.init_global thy);
 
-val setup = DeflMapData.setup;
+val map_ID_add = Map_Id_Data.add;
+val get_map_ID_thms = Map_Id_Data.get o ProofContext.init_global;
+
+val setup = DeflMapData.setup #> Map_Id_Data.setup;
 
 (******************************************************************************)
 (************************** building types and terms **************************)
@@ -183,30 +194,15 @@
 
 fun map_of_typ (thy : theory) (sub : (typ * term) list) (T : typ) : term =
   let
-    val map_tab = get_map_tab thy;
-    fun auto T = T ->> T;
-    fun map_of T =
-        case AList.lookup (op =) sub T of
-          SOME m => (m, true) | NONE => map_of' T
-    and map_of' (T as (Type (c, Ts))) =
-        (case Symtab.lookup map_tab c of
-          SOME (map_name, ds) =>
-          let
-            val Ts' = map snd (filter fst (ds ~~ Ts));
-            val map_type = map auto Ts' -->> auto T;
-            val (ms, bs) = map_split map_of Ts';
-          in
-            if exists I bs
-            then (list_ccomb (Const (map_name, map_type), ms), true)
-            else (mk_ID T, false)
-          end
-        | NONE => (mk_ID T, false))
-      | map_of' T = (mk_ID T, false);
+    val thms = get_map_ID_thms thy;
+    val rules = map (Thm.concl_of #> HOLogic.dest_Trueprop #> HOLogic.dest_eq) thms;
+    val rules' = map (apfst mk_ID) sub @ map swap rules;
   in
-    fst (map_of T)
+    mk_ID T
+    |> Pattern.rewrite_term thy rules' []
+    |> Pattern.rewrite_term thy rules []
   end;
 
-
 (******************************************************************************)
 (********************* declaring definitions and theorems *********************)
 (******************************************************************************)