store deflation thms for map functions in theory data

--- a/src/HOLCF/Powerdomains.thy	Sun Feb 28 18:12:08 2010 -0800
+++ b/src/HOLCF/Powerdomains.thy	Sun Feb 28 18:33:57 2010 -0800
@@ -298,13 +298,16 @@
 setup {*
   fold Domain_Isomorphism.add_type_constructor
     [(@{type_name "upper_pd"}, @{term upper_defl}, @{const_name upper_map},
-        @{thm REP_upper}, @{thm isodefl_upper}, @{thm upper_map_ID}),
+        @{thm REP_upper}, @{thm isodefl_upper}, @{thm upper_map_ID},
+          @{thm deflation_upper_map}),
 
      (@{type_name "lower_pd"}, @{term lower_defl}, @{const_name lower_map},
-        @{thm REP_lower}, @{thm isodefl_lower}, @{thm lower_map_ID}),
+        @{thm REP_lower}, @{thm isodefl_lower}, @{thm lower_map_ID},
+          @{thm deflation_lower_map}),
 
      (@{type_name "convex_pd"}, @{term convex_defl}, @{const_name convex_map},
-        @{thm REP_convex}, @{thm isodefl_convex}, @{thm convex_map_ID})]
+        @{thm REP_convex}, @{thm isodefl_convex}, @{thm convex_map_ID},
+          @{thm deflation_convex_map})]
 *}
 
 end

--- a/src/HOLCF/Representable.thy	Sun Feb 28 18:12:08 2010 -0800
+++ b/src/HOLCF/Representable.thy	Sun Feb 28 18:33:57 2010 -0800
@@ -755,20 +755,20 @@
 
 setup {*
   fold Domain_Isomorphism.add_type_constructor
-    [(@{type_name "->"}, @{term cfun_defl}, @{const_name cfun_map},
-        @{thm REP_cfun}, @{thm isodefl_cfun}, @{thm cfun_map_ID}),
+    [(@{type_name "->"}, @{term cfun_defl}, @{const_name cfun_map}, @{thm REP_cfun},
+        @{thm isodefl_cfun}, @{thm cfun_map_ID}, @{thm deflation_cfun_map}),
 
-     (@{type_name "++"}, @{term ssum_defl}, @{const_name ssum_map},
-        @{thm REP_ssum}, @{thm isodefl_ssum}, @{thm ssum_map_ID}),
+     (@{type_name "++"}, @{term ssum_defl}, @{const_name ssum_map}, @{thm REP_ssum},
+        @{thm isodefl_ssum}, @{thm ssum_map_ID}, @{thm deflation_ssum_map}),
 
-     (@{type_name "**"}, @{term sprod_defl}, @{const_name sprod_map},
-        @{thm REP_sprod}, @{thm isodefl_sprod}, @{thm sprod_map_ID}),
+     (@{type_name "**"}, @{term sprod_defl}, @{const_name sprod_map}, @{thm REP_sprod},
+        @{thm isodefl_sprod}, @{thm sprod_map_ID}, @{thm deflation_sprod_map}),
 
-     (@{type_name "*"}, @{term cprod_defl}, @{const_name cprod_map},
-        @{thm REP_cprod}, @{thm isodefl_cprod}, @{thm cprod_map_ID}),
+     (@{type_name "*"}, @{term cprod_defl}, @{const_name cprod_map}, @{thm REP_cprod},
+        @{thm isodefl_cprod}, @{thm cprod_map_ID}, @{thm deflation_cprod_map}),
 
-     (@{type_name "u"}, @{term u_defl}, @{const_name u_map},
-        @{thm REP_up}, @{thm isodefl_u}, @{thm u_map_ID})]
+     (@{type_name "u"}, @{term u_defl}, @{const_name u_map}, @{thm REP_up},
+        @{thm isodefl_u}, @{thm u_map_ID}, @{thm deflation_u_map})]
 *}
 
 end

--- a/src/HOLCF/Tools/Domain/domain_isomorphism.ML	Sun Feb 28 18:12:08 2010 -0800
+++ b/src/HOLCF/Tools/Domain/domain_isomorphism.ML	Sun Feb 28 18:33:57 2010 -0800
@@ -22,7 +22,7 @@
     (string list * binding * mixfix * string * (binding * binding) option) list
       -> theory -> theory
   val add_type_constructor:
-    (string * term * string * thm  * thm * thm) -> theory -> theory
+    (string * term * string * thm  * thm * thm * thm) -> theory -> theory
   val get_map_tab:
     theory -> string Symtab.table
 end;
@@ -58,37 +58,31 @@
   fun merge data = Symtab.merge (K true) data;
 );
 
-structure RepData = Theory_Data
-(
-  type T = thm list;
-  val empty = [];
-  val extend = I;
-  val merge = Thm.merge_thms;
-);
-
-structure IsodeflData = Theory_Data
-(
+structure Thm_List : THEORY_DATA_ARGS =
+struct
   type T = thm list;
   val empty = [];
   val extend = I;
   val merge = Thm.merge_thms;
-);
+end;
+
+structure RepData = Theory_Data (Thm_List);
 
-structure MapIdData = Theory_Data
-(
-  type T = thm list;
-  val empty = [];
-  val extend = I;
-  val merge = Thm.merge_thms;
-);
+structure IsodeflData = Theory_Data (Thm_List);
+
+structure MapIdData = Theory_Data (Thm_List);
+
+structure DeflMapData = Theory_Data (Thm_List);
 
 fun add_type_constructor
-  (tname, defl_const, map_name, REP_thm, isodefl_thm, map_ID_thm) =
+  (tname, defl_const, map_name, REP_thm,
+   isodefl_thm, map_ID_thm, defl_map_thm) =
     DeflData.map (Symtab.insert (K true) (tname, defl_const))
     #> MapData.map (Symtab.insert (K true) (tname, map_name))
     #> RepData.map (Thm.add_thm REP_thm)
     #> IsodeflData.map (Thm.add_thm isodefl_thm)
-    #> MapIdData.map (Thm.add_thm map_ID_thm);
+    #> MapIdData.map (Thm.add_thm map_ID_thm)
+    #> DeflMapData.map (Thm.add_thm defl_map_thm);
 
 val get_map_tab = MapData.get;
 

--- a/src/HOLCF/ex/Strict_Fun.thy	Sun Feb 28 18:12:08 2010 -0800
+++ b/src/HOLCF/ex/Strict_Fun.thy	Sun Feb 28 18:33:57 2010 -0800
@@ -232,8 +232,8 @@
 
 setup {*
   Domain_Isomorphism.add_type_constructor
-    (@{type_name "sfun"}, @{term sfun_defl}, @{const_name sfun_map},
-        @{thm REP_sfun}, @{thm isodefl_sfun}, @{thm sfun_map_ID})
+    (@{type_name "sfun"}, @{term sfun_defl}, @{const_name sfun_map}, @{thm REP_sfun},
+       @{thm isodefl_sfun}, @{thm sfun_map_ID}, @{thm deflation_sfun_map})
 *}
 
 end