# HG changeset patch
# User huffman
# Date 1258663082 28800
# Node ID 364bc92ba08165206eb9e025a78693d89f5a0558
# Parent  5beafabffa079b4af033b3cc3ca1c8f04f46d140
set up domain_isomorphism package in Representable.thy

diff -r 5beafabffa07 -r 364bc92ba081 src/HOLCF/Representable.thy
--- a/src/HOLCF/Representable.thy	Thu Nov 19 12:31:55 2009 -0800
+++ b/src/HOLCF/Representable.thy	Thu Nov 19 12:38:02 2009 -0800
@@ -5,8 +5,10 @@
 header {* Representable Types *}
 
 theory Representable
-imports Algebraic Universal Ssum Sprod One ConvexPD
-uses ("Tools/repdef.ML")
+imports Algebraic Universal Ssum Sprod One ConvexPD Fixrec
+uses
+  ("Tools/repdef.ML")
+  ("Tools/Domain/domain_isomorphism.ML")
 begin
 
 subsection {* Class of representable types *}
@@ -1029,4 +1031,35 @@
 apply (simp add: convex_map_map)
 done
 
+subsection {* Constructing Domain Isomorphisms *}
+
+use "Tools/Domain/domain_isomorphism.ML"
+
+setup {*
+  fold Domain_Isomorphism.add_type_constructor
+    [(@{type_name "->"}, @{term cfun_defl}, @{const_name cfun_map},
+        @{thm REP_cfun}, @{thm isodefl_cfun}),
+
+     (@{type_name "++"}, @{term ssum_defl}, @{const_name ssum_map},
+        @{thm REP_ssum}, @{thm isodefl_ssum}),
+
+     (@{type_name "**"}, @{term sprod_defl}, @{const_name sprod_map},
+        @{thm REP_sprod}, @{thm isodefl_sprod}),
+
+     (@{type_name "*"}, @{term cprod_defl}, @{const_name cprod_map},
+        @{thm REP_cprod}, @{thm isodefl_cprod}),
+
+     (@{type_name "u"}, @{term u_defl}, @{const_name u_map},
+        @{thm REP_up}, @{thm isodefl_u}),
+
+     (@{type_name "upper_pd"}, @{term upper_defl}, @{const_name upper_map},
+        @{thm REP_upper}, @{thm isodefl_upper}),
+
+     (@{type_name "lower_pd"}, @{term lower_defl}, @{const_name lower_map},
+        @{thm REP_lower}, @{thm isodefl_lower}),
+
+     (@{type_name "convex_pd"}, @{term convex_defl}, @{const_name convex_map},
+        @{thm REP_convex}, @{thm isodefl_convex})]
+*}
+
 end