merged
authorhuffman
Thu, 19 Nov 2009 20:09:56 -0800
changeset 33803 f5db63bd7aee
parent 33802 48ce3a1063f2 (diff)
parent 33773 ccef2e6d8c21 (current diff)
child 33806 dfca0f0e6397
child 33807 ce8d2e8bca21
merged
--- a/src/HOLCF/Domain.thy	Fri Nov 20 00:54:20 2009 +0100
+++ b/src/HOLCF/Domain.thy	Thu Nov 19 20:09:56 2009 -0800
@@ -5,7 +5,7 @@
 header {* Domain package *}
 
 theory Domain
-imports Ssum Sprod Up One Tr Fixrec
+imports Ssum Sprod Up One Tr Fixrec Representable
 uses
   ("Tools/cont_consts.ML")
   ("Tools/cont_proc.ML")
--- a/src/HOLCF/IsaMakefile	Fri Nov 20 00:54:20 2009 +0100
+++ b/src/HOLCF/IsaMakefile	Thu Nov 19 20:09:56 2009 -0800
@@ -52,6 +52,7 @@
   Pcpo.thy \
   Porder.thy \
   Product_Cpo.thy \
+  Representable.thy \
   Sprod.thy \
   Ssum.thy \
   Sum_Cpo.thy \
@@ -64,11 +65,13 @@
   Tools/cont_proc.ML \
   Tools/Domain/domain_extender.ML \
   Tools/Domain/domain_axioms.ML \
+  Tools/Domain/domain_isomorphism.ML \
   Tools/Domain/domain_library.ML \
   Tools/Domain/domain_syntax.ML \
   Tools/Domain/domain_theorems.ML \
   Tools/fixrec.ML \
   Tools/pcpodef.ML \
+  Tools/repdef.ML \
   holcf_logic.ML \
   document/root.tex
 	@$(ISABELLE_TOOL) usedir -b -g true -r $(OUT)/HOL HOLCF
--- a/src/HOLCF/Representable.thy	Fri Nov 20 00:54:20 2009 +0100
+++ b/src/HOLCF/Representable.thy	Thu Nov 19 20:09:56 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 *}
@@ -159,6 +161,25 @@
  apply simp
 done
 
+text {* Isomorphism lemmas used internally by the domain package: *}
+
+lemma domain_abs_iso:
+  fixes abs and rep
+  assumes REP: "REP('b) = REP('a)"
+  assumes abs_def: "abs \<equiv> (coerce :: 'a \<rightarrow> 'b)"
+  assumes rep_def: "rep \<equiv> (coerce :: 'b \<rightarrow> 'a)"
+  shows "rep\<cdot>(abs\<cdot>x) = x"
+unfolding abs_def rep_def by (simp add: REP)
+
+lemma domain_rep_iso:
+  fixes abs and rep
+  assumes REP: "REP('b) = REP('a)"
+  assumes abs_def: "abs \<equiv> (coerce :: 'a \<rightarrow> 'b)"
+  assumes rep_def: "rep \<equiv> (coerce :: 'b \<rightarrow> 'a)"
+  shows "abs\<cdot>(rep\<cdot>x) = x"
+unfolding abs_def rep_def by (simp add: REP [symmetric])
+
+
 subsection {* Proving a subtype is representable *}
 
 text {*
@@ -671,16 +692,14 @@
           Abs_fin_defl (udom_emb oo
             f\<cdot>(Rep_fin_defl a)\<cdot>(Rep_fin_defl b) oo udom_prj))))"
 
-definition "one_typ = REP(one)"
-definition "tr_typ = REP(tr)"
-definition "cfun_typ = TypeRep_fun2 cfun_map"
-definition "ssum_typ = TypeRep_fun2 ssum_map"
-definition "sprod_typ = TypeRep_fun2 sprod_map"
-definition "cprod_typ = TypeRep_fun2 cprod_map"
-definition "u_typ = TypeRep_fun1 u_map"
-definition "upper_typ = TypeRep_fun1 upper_map"
-definition "lower_typ = TypeRep_fun1 lower_map"
-definition "convex_typ = TypeRep_fun1 convex_map"
+definition "cfun_defl = TypeRep_fun2 cfun_map"
+definition "ssum_defl = TypeRep_fun2 ssum_map"
+definition "sprod_defl = TypeRep_fun2 sprod_map"
+definition "cprod_defl = TypeRep_fun2 cprod_map"
+definition "u_defl = TypeRep_fun1 u_map"
+definition "upper_defl = TypeRep_fun1 upper_map"
+definition "lower_defl = TypeRep_fun1 lower_map"
+definition "convex_defl = TypeRep_fun1 convex_map"
 
 lemma Rep_fin_defl_mono: "a \<sqsubseteq> b \<Longrightarrow> Rep_fin_defl a \<sqsubseteq> Rep_fin_defl b"
 unfolding below_fin_defl_def .
@@ -729,138 +748,130 @@
                    Abs_fin_defl_inverse [unfolded mem_Collect_eq, OF 1])
 qed
 
-lemma cast_cfun_typ:
-  "cast\<cdot>(cfun_typ\<cdot>A\<cdot>B) = udom_emb oo cfun_map\<cdot>(cast\<cdot>A)\<cdot>(cast\<cdot>B) oo udom_prj"
-unfolding cfun_typ_def
+lemma cast_cfun_defl:
+  "cast\<cdot>(cfun_defl\<cdot>A\<cdot>B) = udom_emb oo cfun_map\<cdot>(cast\<cdot>A)\<cdot>(cast\<cdot>B) oo udom_prj"
+unfolding cfun_defl_def
 apply (rule cast_TypeRep_fun2)
 apply (erule (1) finite_deflation_cfun_map)
 done
 
-lemma cast_ssum_typ:
-  "cast\<cdot>(ssum_typ\<cdot>A\<cdot>B) = udom_emb oo ssum_map\<cdot>(cast\<cdot>A)\<cdot>(cast\<cdot>B) oo udom_prj"
-unfolding ssum_typ_def
+lemma cast_ssum_defl:
+  "cast\<cdot>(ssum_defl\<cdot>A\<cdot>B) = udom_emb oo ssum_map\<cdot>(cast\<cdot>A)\<cdot>(cast\<cdot>B) oo udom_prj"
+unfolding ssum_defl_def
 apply (rule cast_TypeRep_fun2)
 apply (erule (1) finite_deflation_ssum_map)
 done
 
-lemma cast_sprod_typ:
-  "cast\<cdot>(sprod_typ\<cdot>A\<cdot>B) = udom_emb oo sprod_map\<cdot>(cast\<cdot>A)\<cdot>(cast\<cdot>B) oo udom_prj"
-unfolding sprod_typ_def
+lemma cast_sprod_defl:
+  "cast\<cdot>(sprod_defl\<cdot>A\<cdot>B) = udom_emb oo sprod_map\<cdot>(cast\<cdot>A)\<cdot>(cast\<cdot>B) oo udom_prj"
+unfolding sprod_defl_def
 apply (rule cast_TypeRep_fun2)
 apply (erule (1) finite_deflation_sprod_map)
 done
 
-lemma cast_cprod_typ:
-  "cast\<cdot>(cprod_typ\<cdot>A\<cdot>B) = udom_emb oo cprod_map\<cdot>(cast\<cdot>A)\<cdot>(cast\<cdot>B) oo udom_prj"
-unfolding cprod_typ_def
+lemma cast_cprod_defl:
+  "cast\<cdot>(cprod_defl\<cdot>A\<cdot>B) = udom_emb oo cprod_map\<cdot>(cast\<cdot>A)\<cdot>(cast\<cdot>B) oo udom_prj"
+unfolding cprod_defl_def
 apply (rule cast_TypeRep_fun2)
 apply (erule (1) finite_deflation_cprod_map)
 done
 
-lemma cast_u_typ:
-  "cast\<cdot>(u_typ\<cdot>A) = udom_emb oo u_map\<cdot>(cast\<cdot>A) oo udom_prj"
-unfolding u_typ_def
+lemma cast_u_defl:
+  "cast\<cdot>(u_defl\<cdot>A) = udom_emb oo u_map\<cdot>(cast\<cdot>A) oo udom_prj"
+unfolding u_defl_def
 apply (rule cast_TypeRep_fun1)
 apply (erule finite_deflation_u_map)
 done
 
-lemma cast_upper_typ:
-  "cast\<cdot>(upper_typ\<cdot>A) = udom_emb oo upper_map\<cdot>(cast\<cdot>A) oo udom_prj"
-unfolding upper_typ_def
+lemma cast_upper_defl:
+  "cast\<cdot>(upper_defl\<cdot>A) = udom_emb oo upper_map\<cdot>(cast\<cdot>A) oo udom_prj"
+unfolding upper_defl_def
 apply (rule cast_TypeRep_fun1)
 apply (erule finite_deflation_upper_map)
 done
 
-lemma cast_lower_typ:
-  "cast\<cdot>(lower_typ\<cdot>A) = udom_emb oo lower_map\<cdot>(cast\<cdot>A) oo udom_prj"
-unfolding lower_typ_def
+lemma cast_lower_defl:
+  "cast\<cdot>(lower_defl\<cdot>A) = udom_emb oo lower_map\<cdot>(cast\<cdot>A) oo udom_prj"
+unfolding lower_defl_def
 apply (rule cast_TypeRep_fun1)
 apply (erule finite_deflation_lower_map)
 done
 
-lemma cast_convex_typ:
-  "cast\<cdot>(convex_typ\<cdot>A) = udom_emb oo convex_map\<cdot>(cast\<cdot>A) oo udom_prj"
-unfolding convex_typ_def
+lemma cast_convex_defl:
+  "cast\<cdot>(convex_defl\<cdot>A) = udom_emb oo convex_map\<cdot>(cast\<cdot>A) oo udom_prj"
+unfolding convex_defl_def
 apply (rule cast_TypeRep_fun1)
 apply (erule finite_deflation_convex_map)
 done
 
 text {* REP of type constructor = type combinator *}
 
-lemma REP_one: "REP(one) = one_typ"
-by (simp only: one_typ_def)
-
-lemma REP_tr: "REP(tr) = tr_typ"
-by (simp only: tr_typ_def)
-
-lemma REP_cfun: "REP('a \<rightarrow> 'b) = cfun_typ\<cdot>REP('a)\<cdot>REP('b)"
+lemma REP_cfun: "REP('a \<rightarrow> 'b) = cfun_defl\<cdot>REP('a)\<cdot>REP('b)"
 apply (rule cast_eq_imp_eq, rule ext_cfun)
-apply (simp add: cast_REP cast_cfun_typ)
+apply (simp add: cast_REP cast_cfun_defl)
 apply (simp add: cfun_map_def)
 apply (simp only: prj_cfun_def emb_cfun_def)
 apply (simp add: expand_cfun_eq ep_pair.e_eq_iff [OF ep_pair_udom])
 done
 
 
-lemma REP_ssum: "REP('a \<oplus> 'b) = ssum_typ\<cdot>REP('a)\<cdot>REP('b)"
+lemma REP_ssum: "REP('a \<oplus> 'b) = ssum_defl\<cdot>REP('a)\<cdot>REP('b)"
 apply (rule cast_eq_imp_eq, rule ext_cfun)
-apply (simp add: cast_REP cast_ssum_typ)
+apply (simp add: cast_REP cast_ssum_defl)
 apply (simp add: prj_ssum_def)
 apply (simp add: emb_ssum_def)
 apply (simp add: ssum_map_map cfcomp1)
 done
 
-lemma REP_sprod: "REP('a \<otimes> 'b) = sprod_typ\<cdot>REP('a)\<cdot>REP('b)"
+lemma REP_sprod: "REP('a \<otimes> 'b) = sprod_defl\<cdot>REP('a)\<cdot>REP('b)"
 apply (rule cast_eq_imp_eq, rule ext_cfun)
-apply (simp add: cast_REP cast_sprod_typ)
+apply (simp add: cast_REP cast_sprod_defl)
 apply (simp add: prj_sprod_def)
 apply (simp add: emb_sprod_def)
 apply (simp add: sprod_map_map cfcomp1)
 done
 
-lemma REP_cprod: "REP('a \<times> 'b) = cprod_typ\<cdot>REP('a)\<cdot>REP('b)"
+lemma REP_cprod: "REP('a \<times> 'b) = cprod_defl\<cdot>REP('a)\<cdot>REP('b)"
 apply (rule cast_eq_imp_eq, rule ext_cfun)
-apply (simp add: cast_REP cast_cprod_typ)
+apply (simp add: cast_REP cast_cprod_defl)
 apply (simp add: prj_cprod_def)
 apply (simp add: emb_cprod_def)
 apply (simp add: cprod_map_map cfcomp1)
 done
 
-lemma REP_up: "REP('a u) = u_typ\<cdot>REP('a)"
+lemma REP_up: "REP('a u) = u_defl\<cdot>REP('a)"
 apply (rule cast_eq_imp_eq, rule ext_cfun)
-apply (simp add: cast_REP cast_u_typ)
+apply (simp add: cast_REP cast_u_defl)
 apply (simp add: prj_u_def)
 apply (simp add: emb_u_def)
 apply (simp add: u_map_map cfcomp1)
 done
 
-lemma REP_upper: "REP('a upper_pd) = upper_typ\<cdot>REP('a)"
+lemma REP_upper: "REP('a upper_pd) = upper_defl\<cdot>REP('a)"
 apply (rule cast_eq_imp_eq, rule ext_cfun)
-apply (simp add: cast_REP cast_upper_typ)
+apply (simp add: cast_REP cast_upper_defl)
 apply (simp add: prj_upper_pd_def)
 apply (simp add: emb_upper_pd_def)
 apply (simp add: upper_map_map cfcomp1)
 done
 
-lemma REP_lower: "REP('a lower_pd) = lower_typ\<cdot>REP('a)"
+lemma REP_lower: "REP('a lower_pd) = lower_defl\<cdot>REP('a)"
 apply (rule cast_eq_imp_eq, rule ext_cfun)
-apply (simp add: cast_REP cast_lower_typ)
+apply (simp add: cast_REP cast_lower_defl)
 apply (simp add: prj_lower_pd_def)
 apply (simp add: emb_lower_pd_def)
 apply (simp add: lower_map_map cfcomp1)
 done
 
-lemma REP_convex: "REP('a convex_pd) = convex_typ\<cdot>REP('a)"
+lemma REP_convex: "REP('a convex_pd) = convex_defl\<cdot>REP('a)"
 apply (rule cast_eq_imp_eq, rule ext_cfun)
-apply (simp add: cast_REP cast_convex_typ)
+apply (simp add: cast_REP cast_convex_defl)
 apply (simp add: prj_convex_pd_def)
 apply (simp add: emb_convex_pd_def)
 apply (simp add: convex_map_map cfcomp1)
 done
 
 lemmas REP_simps =
-  REP_one
-  REP_tr
   REP_cfun
   REP_ssum
   REP_sprod
@@ -944,69 +955,111 @@
 apply (simp add: emb_coerce coerce_prj REP)
 done
 
+lemma isodefl_abs_rep:
+  fixes abs and rep and d
+  assumes REP: "REP('b) = REP('a)"
+  assumes abs_def: "abs \<equiv> (coerce :: 'a \<rightarrow> 'b)"
+  assumes rep_def: "rep \<equiv> (coerce :: 'b \<rightarrow> 'a)"
+  shows "isodefl d t \<Longrightarrow> isodefl (abs oo d oo rep) t"
+unfolding abs_def rep_def using REP by (rule isodefl_coerce)
+
 lemma isodefl_cfun:
   "isodefl d1 t1 \<Longrightarrow> isodefl d2 t2 \<Longrightarrow>
-    isodefl (cfun_map\<cdot>d1\<cdot>d2) (cfun_typ\<cdot>t1\<cdot>t2)"
+    isodefl (cfun_map\<cdot>d1\<cdot>d2) (cfun_defl\<cdot>t1\<cdot>t2)"
 apply (rule isodeflI)
-apply (simp add: cast_cfun_typ cast_isodefl)
+apply (simp add: cast_cfun_defl cast_isodefl)
 apply (simp add: emb_cfun_def prj_cfun_def)
 apply (simp add: cfun_map_map cfcomp1)
 done
 
 lemma isodefl_ssum:
   "isodefl d1 t1 \<Longrightarrow> isodefl d2 t2 \<Longrightarrow>
-    isodefl (ssum_map\<cdot>d1\<cdot>d2) (ssum_typ\<cdot>t1\<cdot>t2)"
+    isodefl (ssum_map\<cdot>d1\<cdot>d2) (ssum_defl\<cdot>t1\<cdot>t2)"
 apply (rule isodeflI)
-apply (simp add: cast_ssum_typ cast_isodefl)
+apply (simp add: cast_ssum_defl cast_isodefl)
 apply (simp add: emb_ssum_def prj_ssum_def)
 apply (simp add: ssum_map_map isodefl_strict)
 done
 
 lemma isodefl_sprod:
   "isodefl d1 t1 \<Longrightarrow> isodefl d2 t2 \<Longrightarrow>
-    isodefl (sprod_map\<cdot>d1\<cdot>d2) (sprod_typ\<cdot>t1\<cdot>t2)"
+    isodefl (sprod_map\<cdot>d1\<cdot>d2) (sprod_defl\<cdot>t1\<cdot>t2)"
 apply (rule isodeflI)
-apply (simp add: cast_sprod_typ cast_isodefl)
+apply (simp add: cast_sprod_defl cast_isodefl)
 apply (simp add: emb_sprod_def prj_sprod_def)
 apply (simp add: sprod_map_map isodefl_strict)
 done
 
+lemma isodefl_cprod:
+  "isodefl d1 t1 \<Longrightarrow> isodefl d2 t2 \<Longrightarrow>
+    isodefl (cprod_map\<cdot>d1\<cdot>d2) (cprod_defl\<cdot>t1\<cdot>t2)"
+apply (rule isodeflI)
+apply (simp add: cast_cprod_defl cast_isodefl)
+apply (simp add: emb_cprod_def prj_cprod_def)
+apply (simp add: cprod_map_map cfcomp1)
+done
+
 lemma isodefl_u:
-  "isodefl d t \<Longrightarrow> isodefl (u_map\<cdot>d) (u_typ\<cdot>t)"
+  "isodefl d t \<Longrightarrow> isodefl (u_map\<cdot>d) (u_defl\<cdot>t)"
 apply (rule isodeflI)
-apply (simp add: cast_u_typ cast_isodefl)
+apply (simp add: cast_u_defl cast_isodefl)
 apply (simp add: emb_u_def prj_u_def)
 apply (simp add: u_map_map)
 done
 
-lemma isodefl_one: "isodefl (ID :: one \<rightarrow> one) one_typ"
-unfolding one_typ_def by (rule isodefl_ID_REP)
-
-lemma isodefl_tr: "isodefl (ID :: tr \<rightarrow> tr) tr_typ"
-unfolding tr_typ_def by (rule isodefl_ID_REP)
-
 lemma isodefl_upper:
-  "isodefl d t \<Longrightarrow> isodefl (upper_map\<cdot>d) (upper_typ\<cdot>t)"
+  "isodefl d t \<Longrightarrow> isodefl (upper_map\<cdot>d) (upper_defl\<cdot>t)"
 apply (rule isodeflI)
-apply (simp add: cast_upper_typ cast_isodefl)
+apply (simp add: cast_upper_defl cast_isodefl)
 apply (simp add: emb_upper_pd_def prj_upper_pd_def)
 apply (simp add: upper_map_map)
 done
 
 lemma isodefl_lower:
-  "isodefl d t \<Longrightarrow> isodefl (lower_map\<cdot>d) (lower_typ\<cdot>t)"
+  "isodefl d t \<Longrightarrow> isodefl (lower_map\<cdot>d) (lower_defl\<cdot>t)"
 apply (rule isodeflI)
-apply (simp add: cast_lower_typ cast_isodefl)
+apply (simp add: cast_lower_defl cast_isodefl)
 apply (simp add: emb_lower_pd_def prj_lower_pd_def)
 apply (simp add: lower_map_map)
 done
 
 lemma isodefl_convex:
-  "isodefl d t \<Longrightarrow> isodefl (convex_map\<cdot>d) (convex_typ\<cdot>t)"
+  "isodefl d t \<Longrightarrow> isodefl (convex_map\<cdot>d) (convex_defl\<cdot>t)"
 apply (rule isodeflI)
-apply (simp add: cast_convex_typ cast_isodefl)
+apply (simp add: cast_convex_defl cast_isodefl)
 apply (simp add: emb_convex_pd_def prj_convex_pd_def)
 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
--- a/src/HOLCF/Tools/Domain/domain_axioms.ML	Fri Nov 20 00:54:20 2009 +0100
+++ b/src/HOLCF/Tools/Domain/domain_axioms.ML	Thu Nov 19 20:09:56 2009 -0800
@@ -6,13 +6,16 @@
 
 signature DOMAIN_AXIOMS =
 sig
-  val copy_of_dtyp : (int -> term) -> Datatype.dtyp -> term
+  val copy_of_dtyp :
+      string Symtab.table -> (int -> term) -> Datatype.dtyp -> term
 
   val calc_axioms :
+      bool -> string Symtab.table ->
       string -> Domain_Library.eq list -> int -> Domain_Library.eq ->
       string * (string * term) list * (string * term) list
 
   val add_axioms :
+      bool ->
       bstring -> Domain_Library.eq list -> theory -> theory
 end;
 
@@ -34,119 +37,124 @@
                  (@{type_name "*"}, @{const_name "cprod_map"}),
                  (@{type_name "u"}, @{const_name "u_map"})];
 
-fun copy_of_dtyp r dt = if DatatypeAux.is_rec_type dt then copy r dt else ID
-and copy r (DatatypeAux.DtRec i) = r i
-  | copy r (DatatypeAux.DtTFree a) = ID
-  | copy r (DatatypeAux.DtType (c, ds)) =
-    case Symtab.lookup copy_tab c of
-      SOME f => list_ccomb (%%:f, map (copy_of_dtyp r) ds)
+fun copy_of_dtyp tab r dt =
+    if DatatypeAux.is_rec_type dt then copy tab r dt else ID
+and copy tab r (DatatypeAux.DtRec i) = r i
+  | copy tab r (DatatypeAux.DtTFree a) = ID
+  | copy tab r (DatatypeAux.DtType (c, ds)) =
+    case Symtab.lookup tab c of
+      SOME f => list_ccomb (%%:f, map (copy_of_dtyp tab r) ds)
     | NONE => (warning ("copy_of_dtyp: unknown type constructor " ^ c); ID);
 
 fun calc_axioms
-      (comp_dname : string)
-      (eqs : eq list)
-      (n : int)
-      (eqn as ((dname,_),cons) : eq)
+    (definitional : bool)
+    (map_tab : string Symtab.table)
+    (comp_dname : string)
+    (eqs : eq list)
+    (n : int)
+    (eqn as ((dname,_),cons) : eq)
     : string * (string * term) list * (string * term) list =
-    let
-
-      (* ----- axioms and definitions concerning the isomorphism ------------------ *)
+  let
 
-      val dc_abs = %%:(dname^"_abs");
-      val dc_rep = %%:(dname^"_rep");
-      val x_name'= "x";
-      val x_name = idx_name eqs x_name' (n+1);
-      val dnam = Long_Name.base_name dname;
+(* ----- axioms and definitions concerning the isomorphism ------------------ *)
 
-      val abs_iso_ax = ("abs_iso", mk_trp(dc_rep`(dc_abs`%x_name') === %:x_name'));
-      val rep_iso_ax = ("rep_iso", mk_trp(dc_abs`(dc_rep`%x_name') === %:x_name'));
+    val dc_abs = %%:(dname^"_abs");
+    val dc_rep = %%:(dname^"_rep");
+    val x_name'= "x";
+    val x_name = idx_name eqs x_name' (n+1);
+    val dnam = Long_Name.base_name dname;
+
+    val abs_iso_ax = ("abs_iso", mk_trp(dc_rep`(dc_abs`%x_name') === %:x_name'));
+    val rep_iso_ax = ("rep_iso", mk_trp(dc_abs`(dc_rep`%x_name') === %:x_name'));
 
-      val when_def = ("when_def",%%:(dname^"_when") == 
-                                List.foldr (uncurry /\ ) (/\x_name'((when_body cons (fn (x,y) =>
-                                                                                        Bound(1+length cons+x-y)))`(dc_rep`Bound 0))) (when_funs cons));
-          
-      val copy_def =
-          let fun r i = proj (Bound 0) eqs i;
-          in ("copy_def", %%:(dname^"_copy") ==
-                          /\ "f" (dc_abs oo (copy_of_dtyp r (dtyp_of_eq eqn)) oo dc_rep)) end;
-
-      (* -- definitions concerning the constructors, discriminators and selectors - *)
+    val when_def = ("when_def",%%:(dname^"_when") == 
+        List.foldr (uncurry /\ ) (/\x_name'((when_body cons (fn (x,y) =>
+          Bound(1+length cons+x-y)))`(dc_rep`Bound 0))) (when_funs cons));
 
-      fun con_def m n (_,args) = let
-        fun idxs z x arg = (if is_lazy arg then mk_up else I) (Bound(z-x));
-        fun parms vs = mk_stuple (mapn (idxs(length vs)) 1 vs);
-        fun inj y 1 _ = y
-          | inj y _ 0 = mk_sinl y
-          | inj y i j = mk_sinr (inj y (i-1) (j-1));
-      in List.foldr /\# (dc_abs`(inj (parms args) m n)) args end;
-          
-      val con_defs = mapn (fn n => fn (con,args) =>
-                                      (extern_name con ^"_def", %%:con == con_def (length cons) n (con,args))) 0 cons;
+    val copy_def =
+      let fun r i = proj (Bound 0) eqs i;
+      in
+        ("copy_def", %%:(dname^"_copy") == /\ "f"
+          (dc_abs oo (copy_of_dtyp map_tab r (dtyp_of_eq eqn)) oo dc_rep))
+      end;
+
+(* -- definitions concerning the constructors, discriminators and selectors - *)
+
+    fun con_def m n (_,args) = let
+      fun idxs z x arg = (if is_lazy arg then mk_up else I) (Bound(z-x));
+      fun parms vs = mk_stuple (mapn (idxs(length vs)) 1 vs);
+      fun inj y 1 _ = y
+        | inj y _ 0 = mk_sinl y
+        | inj y i j = mk_sinr (inj y (i-1) (j-1));
+    in List.foldr /\# (dc_abs`(inj (parms args) m n)) args end;
           
-      val dis_defs = let
-        fun ddef (con,_) = (dis_name con ^"_def",%%:(dis_name con) == 
-                                                list_ccomb(%%:(dname^"_when"),map 
-                                                                                (fn (con',args) => (List.foldr /\#
+    val con_defs = mapn (fn n => fn (con,args) =>
+                                    (extern_name con ^"_def", %%:con == con_def (length cons) n (con,args))) 0 cons;
+          
+    val dis_defs = let
+      fun ddef (con,_) = (dis_name con ^"_def",%%:(dis_name con) == 
+                                              list_ccomb(%%:(dname^"_when"),map 
+                                                                              (fn (con',args) => (List.foldr /\#
       (if con'=con then TT else FF) args)) cons))
-      in map ddef cons end;
-
-      val mat_defs =
-          let
-            fun mdef (con,_) =
-                let
-                  val k = Bound 0
-                  val x = Bound 1
-                  fun one_con (con', args') =
-                      if con'=con then k else List.foldr /\# mk_fail args'
-                  val w = list_ccomb(%%:(dname^"_when"), map one_con cons)
-                  val rhs = /\ "x" (/\ "k" (w ` x))
-                in (mat_name con ^"_def", %%:(mat_name con) == rhs) end
-          in map mdef cons end;
+    in map ddef cons end;
 
-      val pat_defs =
+    val mat_defs =
+      let
+        fun mdef (con,_) =
+          let
+            val k = Bound 0
+            val x = Bound 1
+            fun one_con (con', args') =
+                if con'=con then k else List.foldr /\# mk_fail args'
+            val w = list_ccomb(%%:(dname^"_when"), map one_con cons)
+            val rhs = /\ "x" (/\ "k" (w ` x))
+          in (mat_name con ^"_def", %%:(mat_name con) == rhs) end
+      in map mdef cons end;
+
+    val pat_defs =
+      let
+        fun pdef (con,args) =
           let
-            fun pdef (con,args) =
-                let
-                  val ps = mapn (fn n => fn _ => %:("pat" ^ string_of_int n)) 1 args;
-                  val xs = map (bound_arg args) args;
-                  val r = Bound (length args);
-                  val rhs = case args of [] => mk_return HOLogic.unit
-                                       | _ => mk_ctuple_pat ps ` mk_ctuple xs;
-                  fun one_con (con',args') = List.foldr /\# (if con'=con then rhs else mk_fail) args';
-                in (pat_name con ^"_def", list_comb (%%:(pat_name con), ps) == 
-                                                    list_ccomb(%%:(dname^"_when"), map one_con cons))
-                end
-          in map pdef cons end;
+            val ps = mapn (fn n => fn _ => %:("pat" ^ string_of_int n)) 1 args;
+            val xs = map (bound_arg args) args;
+            val r = Bound (length args);
+            val rhs = case args of [] => mk_return HOLogic.unit
+                                 | _ => mk_ctuple_pat ps ` mk_ctuple xs;
+            fun one_con (con',args') = List.foldr /\# (if con'=con then rhs else mk_fail) args';
+          in (pat_name con ^"_def", list_comb (%%:(pat_name con), ps) == 
+                                              list_ccomb(%%:(dname^"_when"), map one_con cons))
+          end
+      in map pdef cons end;
 
-      val sel_defs = let
-        fun sdef con n arg = Option.map (fn sel => (sel^"_def",%%:sel == 
-                                                              list_ccomb(%%:(dname^"_when"),map 
-                                                                                              (fn (con',args) => if con'<>con then UU else
-                                                                                                                 List.foldr /\# (Bound (length args - n)) args) cons))) (sel_of arg);
-      in map_filter I (maps (fn (con,args) => mapn (sdef con) 1 args) cons) end;
+    val sel_defs = let
+      fun sdef con n arg = Option.map (fn sel => (sel^"_def",%%:sel == 
+                                                            list_ccomb(%%:(dname^"_when"),map 
+                                                                                            (fn (con',args) => if con'<>con then UU else
+                                                                                                               List.foldr /\# (Bound (length args - n)) args) cons))) (sel_of arg);
+    in map_filter I (maps (fn (con,args) => mapn (sdef con) 1 args) cons) end;
 
 
-      (* ----- axiom and definitions concerning induction ------------------------- *)
+(* ----- axiom and definitions concerning induction ------------------------- *)
 
-      val reach_ax = ("reach", mk_trp(proj (mk_fix (%%:(comp_dname^"_copy"))) eqs n
-                                            `%x_name === %:x_name));
-      val take_def =
-          ("take_def",
-           %%:(dname^"_take") ==
-              mk_lam("n",proj
-                           (mk_iterate (Bound 0, %%:(comp_dname^"_copy"), UU)) eqs n));
-      val finite_def =
-          ("finite_def",
-           %%:(dname^"_finite") ==
-              mk_lam(x_name,
-                     mk_ex("n",(%%:(dname^"_take") $ Bound 0)`Bound 1 === Bound 1)));
+    val reach_ax = ("reach", mk_trp(proj (mk_fix (%%:(comp_dname^"_copy"))) eqs n
+                                         `%x_name === %:x_name));
+    val take_def =
+        ("take_def",
+         %%:(dname^"_take") ==
+            mk_lam("n",proj
+                         (mk_iterate (Bound 0, %%:(comp_dname^"_copy"), UU)) eqs n));
+    val finite_def =
+        ("finite_def",
+         %%:(dname^"_finite") ==
+            mk_lam(x_name,
+                   mk_ex("n",(%%:(dname^"_take") $ Bound 0)`Bound 1 === Bound 1)));
 
-    in (dnam,
-        [abs_iso_ax, rep_iso_ax, reach_ax],
-        [when_def, copy_def] @
-        con_defs @ dis_defs @ mat_defs @ pat_defs @ sel_defs @
-        [take_def, finite_def])
-    end; (* let (calc_axioms) *)
+  in (dnam,
+      (if definitional then [reach_ax] else [abs_iso_ax, rep_iso_ax, reach_ax]),
+      (if definitional then [when_def] else [when_def, copy_def]) @
+      con_defs @ dis_defs @ mat_defs @ pat_defs @ sel_defs @
+      [take_def, finite_def])
+  end; (* let (calc_axioms) *)
 
 
 (* legacy type inference *)
@@ -173,16 +181,17 @@
       val ms = map qualify con_names ~~ map qualify mat_names;
     in Fixrec.add_matchers ms thy end;
 
-fun add_axioms comp_dnam (eqs : eq list) thy' =
-    let
-      val comp_dname = Sign.full_bname thy' comp_dnam;
-      val dnames = map (fst o fst) eqs;
-      val x_name = idx_name dnames "x"; 
-      fun copy_app dname = %%:(dname^"_copy")`Bound 0;
-      val copy_def = ("copy_def" , %%:(comp_dname^"_copy") ==
-                                   /\ "f"(mk_ctuple (map copy_app dnames)));
+fun add_axioms definitional comp_dnam (eqs : eq list) thy' =
+  let
+    val comp_dname = Sign.full_bname thy' comp_dnam;
+    val dnames = map (fst o fst) eqs;
+    val x_name = idx_name dnames "x"; 
+    fun copy_app dname = %%:(dname^"_copy")`Bound 0;
+    val copy_def = ("copy_def" , %%:(comp_dname^"_copy") ==
+                                 /\ "f"(mk_ctuple (map copy_app dnames)));
 
-      fun one_con (con,args) = let
+    fun one_con (con,args) =
+      let
         val nonrec_args = filter_out is_rec args;
         val    rec_args = filter is_rec args;
         val    recs_cnt = length rec_args;
@@ -199,37 +208,45 @@
         fun rel_app i ra = proj (Bound(allargs_cnt+2)) eqs (rec_of ra) $ 
                                 Bound (2*recs_cnt-i) $ Bound (recs_cnt-i);
         val capps =
-            List.foldr mk_conj
-                       (mk_conj(
-                        Bound(allargs_cnt+1)===list_ccomb(%%:con,map (bound_arg allvns) vns1),
-                        Bound(allargs_cnt+0)===list_ccomb(%%:con,map (bound_arg allvns) vns2)))
-                       (mapn rel_app 1 rec_args);
-      in List.foldr mk_ex
-                    (Library.foldr mk_conj
-                                   (map (defined o Bound) nonlazy_idxs,capps)) allvns
+          List.foldr
+            mk_conj
+            (mk_conj(
+             Bound(allargs_cnt+1)===list_ccomb(%%:con,map (bound_arg allvns) vns1),
+             Bound(allargs_cnt+0)===list_ccomb(%%:con,map (bound_arg allvns) vns2)))
+            (mapn rel_app 1 rec_args);
+      in
+        List.foldr
+          mk_ex
+          (Library.foldr mk_conj
+                         (map (defined o Bound) nonlazy_idxs,capps)) allvns
       end;
-      fun one_comp n (_,cons) =
-          mk_all(x_name(n+1),
-                 mk_all(x_name(n+1)^"'",
-                        mk_imp(proj (Bound 2) eqs n $ Bound 1 $ Bound 0,
-                               foldr1 mk_disj (mk_conj(Bound 1 === UU,Bound 0 === UU)
-                                               ::map one_con cons))));
-      val bisim_def =
-          ("bisim_def",
-           %%:(comp_dname^"_bisim")==mk_lam("R", foldr1 mk_conj (mapn one_comp 0 eqs)));
-          
-      fun add_one (dnam, axs, dfs) =
-          Sign.add_path dnam
+    fun one_comp n (_,cons) =
+        mk_all (x_name(n+1),
+        mk_all (x_name(n+1)^"'",
+        mk_imp (proj (Bound 2) eqs n $ Bound 1 $ Bound 0,
+        foldr1 mk_disj (mk_conj(Bound 1 === UU,Bound 0 === UU)
+                        ::map one_con cons))));
+    val bisim_def =
+        ("bisim_def", %%:(comp_dname^"_bisim") ==
+                         mk_lam("R", foldr1 mk_conj (mapn one_comp 0 eqs)));
+
+    fun add_one (dnam, axs, dfs) =
+        Sign.add_path dnam
           #> add_defs_infer dfs
           #> add_axioms_infer axs
           #> Sign.parent_path;
 
-      val thy = fold add_one (mapn (calc_axioms comp_dname eqs) 0 eqs) thy';
+    val map_tab = Domain_Isomorphism.get_map_tab thy';
+
+    val thy = thy'
+      |> fold add_one (mapn (calc_axioms definitional map_tab comp_dname eqs) 0 eqs);
 
-    in thy |> Sign.add_path comp_dnam  
-           |> add_defs_infer (bisim_def::(if length eqs>1 then [copy_def] else []))
-           |> Sign.parent_path
-           |> fold add_matchers eqs
-    end; (* let (add_axioms) *)
+  in
+    thy
+    |> Sign.add_path comp_dnam  
+    |> add_defs_infer (bisim_def::(if length eqs>1 then [copy_def] else []))
+    |> Sign.parent_path
+    |> fold add_matchers eqs
+  end; (* let (add_axioms) *)
 
 end; (* struct *)
--- a/src/HOLCF/Tools/Domain/domain_extender.ML	Fri Nov 20 00:54:20 2009 +0100
+++ b/src/HOLCF/Tools/Domain/domain_extender.ML	Thu Nov 19 20:09:56 2009 -0800
@@ -6,14 +6,29 @@
 
 signature DOMAIN_EXTENDER =
 sig
-  val add_domain_cmd: string ->
-                      ((string * string option) list * binding * mixfix *
-                       (binding * (bool * binding option * string) list * mixfix) list) list
-                      -> theory -> theory
-  val add_domain: string ->
-                  ((string * string option) list * binding * mixfix *
-                   (binding * (bool * binding option * typ) list * mixfix) list) list
-                  -> theory -> theory
+  val add_domain_cmd:
+      string ->
+      ((string * string option) list * binding * mixfix *
+       (binding * (bool * binding option * string) list * mixfix) list) list
+      -> theory -> theory
+
+  val add_domain:
+      string ->
+      ((string * string option) list * binding * mixfix *
+       (binding * (bool * binding option * typ) list * mixfix) list) list
+      -> theory -> theory
+
+  val add_new_domain_cmd:
+      string ->
+      ((string * string option) list * binding * mixfix *
+       (binding * (bool * binding option * string) list * mixfix) list) list
+      -> theory -> theory
+
+  val add_new_domain:
+      string ->
+      ((string * string option) list * binding * mixfix *
+       (binding * (bool * binding option * typ) list * mixfix) list) list
+      -> theory -> theory
 end;
 
 structure Domain_Extender :> DOMAIN_EXTENDER =
@@ -23,132 +38,231 @@
 
 (* ----- general testing and preprocessing of constructor list -------------- *)
 fun check_and_sort_domain
-      (dtnvs : (string * typ list) list)
-      (cons'' : (binding * (bool * binding option * typ) list * mixfix) list list)
-      (sg : theory)
+    (definitional : bool)
+    (dtnvs : (string * typ list) list)
+    (cons'' : (binding * (bool * binding option * typ) list * mixfix) list list)
+    (thy : theory)
     : ((string * typ list) *
        (binding * (bool * binding option * typ) list * mixfix) list) list =
-    let
-      val defaultS = Sign.defaultS sg;
-      val test_dupl_typs = (case duplicates (op =) (map fst dtnvs) of 
-                              [] => false | dups => error ("Duplicate types: " ^ commas_quote dups));
-      val test_dupl_cons =
-          (case duplicates (op =) (map (Binding.name_of o first) (flat cons'')) of 
-             [] => false | dups => error ("Duplicate constructors: " 
-                                          ^ commas_quote dups));
-      val test_dupl_sels =
-          (case duplicates (op =) (map Binding.name_of (map_filter second
-                                                                        (maps second (flat cons'')))) of
-             [] => false | dups => error("Duplicate selectors: "^commas_quote dups));
-      val test_dupl_tvars =
-          exists(fn s=>case duplicates (op =) (map(fst o dest_TFree)s)of
-                         [] => false | dups => error("Duplicate type arguments: " 
-                                                     ^commas_quote dups)) (map snd dtnvs);
-      (* test for free type variables, illegal sort constraints on rhs,
-         non-pcpo-types and invalid use of recursive type;
-         replace sorts in type variables on rhs *)
-      fun analyse_equation ((dname,typevars),cons') = 
-          let
-            val tvars = map dest_TFree typevars;
-            val distinct_typevars = map TFree tvars;
-            fun rm_sorts (TFree(s,_)) = TFree(s,[])
-              | rm_sorts (Type(s,ts)) = Type(s,remove_sorts ts)
-              | rm_sorts (TVar(s,_))  = TVar(s,[])
-            and remove_sorts l = map rm_sorts l;
-            val indirect_ok = ["*","Cfun.->","Ssum.++","Sprod.**","Up.u"]
-            fun analyse indirect (TFree(v,s))  =
-                (case AList.lookup (op =) tvars v of 
-                   NONE => error ("Free type variable " ^ quote v ^ " on rhs.")
-                 | SOME sort => if eq_set (op =) (s, defaultS) orelse
-                                   eq_set (op =) (s, sort)
-                                then TFree(v,sort)
-                                else error ("Inconsistent sort constraint" ^
-                                            " for type variable " ^ quote v))
-              | analyse indirect (t as Type(s,typl)) =
-                (case AList.lookup (op =) dtnvs s of
-                   NONE          => if s mem indirect_ok
-                                    then Type(s,map (analyse false) typl)
-                                    else Type(s,map (analyse true) typl)
-                 | SOME typevars => if indirect 
-                                    then error ("Indirect recursion of type " ^ 
-                                                quote (string_of_typ sg t))
-                                    else if dname <> s orelse
-                                            (** BUG OR FEATURE?:
-                                                mutual recursion may use different arguments **)
-                                            remove_sorts typevars = remove_sorts typl 
-                                    then Type(s,map (analyse true) typl)
-                                    else error ("Direct recursion of type " ^ 
-                                                quote (string_of_typ sg t) ^ 
-                                                " with different arguments"))
-              | analyse indirect (TVar _) = Imposs "extender:analyse";
-            fun check_pcpo lazy T =
-                let val ok = if lazy then cpo_type else pcpo_type
-                in if ok sg T then T else error
-                                            ("Constructor argument type is not of sort pcpo: " ^
-                                             string_of_typ sg T)
-                end;
-            fun analyse_arg (lazy, sel, T) =
-                (lazy, sel, check_pcpo lazy (analyse false T));
-            fun analyse_con (b, args, mx) = (b, map analyse_arg args, mx);
-          in ((dname,distinct_typevars), map analyse_con cons') end; 
-    in ListPair.map analyse_equation (dtnvs,cons'')
-    end; (* let *)
+  let
+    val defaultS = Sign.defaultS thy;
+
+    val test_dupl_typs =
+      case duplicates (op =) (map fst dtnvs) of 
+        [] => false | dups => error ("Duplicate types: " ^ commas_quote dups);
+
+    val all_cons = map (Binding.name_of o first) (flat cons'');
+    val test_dupl_cons =
+      case duplicates (op =) all_cons of 
+        [] => false | dups => error ("Duplicate constructors: " 
+                                      ^ commas_quote dups);
+    val all_sels =
+      (map Binding.name_of o map_filter second o maps second) (flat cons'');
+    val test_dupl_sels =
+      case duplicates (op =) all_sels of
+        [] => false | dups => error("Duplicate selectors: "^commas_quote dups);
+
+    fun test_dupl_tvars s =
+      case duplicates (op =) (map(fst o dest_TFree)s) of
+        [] => false | dups => error("Duplicate type arguments: " 
+                                    ^commas_quote dups);
+    val test_dupl_tvars' = exists test_dupl_tvars (map snd dtnvs);
+
+    (* test for free type variables, illegal sort constraints on rhs,
+       non-pcpo-types and invalid use of recursive type;
+       replace sorts in type variables on rhs *)
+    fun analyse_equation ((dname,typevars),cons') = 
+      let
+        val tvars = map dest_TFree typevars;
+        val distinct_typevars = map TFree tvars;
+        fun rm_sorts (TFree(s,_)) = TFree(s,[])
+          | rm_sorts (Type(s,ts)) = Type(s,remove_sorts ts)
+          | rm_sorts (TVar(s,_))  = TVar(s,[])
+        and remove_sorts l = map rm_sorts l;
+        val indirect_ok = ["*","Cfun.->","Ssum.++","Sprod.**","Up.u"]
+        fun analyse indirect (TFree(v,s))  =
+            (case AList.lookup (op =) tvars v of 
+               NONE => error ("Free type variable " ^ quote v ^ " on rhs.")
+             | SOME sort => if eq_set (op =) (s, defaultS) orelse
+                               eq_set (op =) (s, sort)
+                            then TFree(v,sort)
+                            else error ("Inconsistent sort constraint" ^
+                                        " for type variable " ^ quote v))
+          | analyse indirect (t as Type(s,typl)) =
+            (case AList.lookup (op =) dtnvs s of
+               NONE =>
+                 if definitional orelse s mem indirect_ok
+                 then Type(s,map (analyse false) typl)
+                 else Type(s,map (analyse true) typl)
+             | SOME typevars =>
+                 if indirect 
+                 then error ("Indirect recursion of type " ^ 
+                             quote (string_of_typ thy t))
+                 else if dname <> s orelse
+                         (** BUG OR FEATURE?:
+                             mutual recursion may use different arguments **)
+                         remove_sorts typevars = remove_sorts typl 
+                 then Type(s,map (analyse true) typl)
+                 else error ("Direct recursion of type " ^ 
+                             quote (string_of_typ thy t) ^ 
+                             " with different arguments"))
+          | analyse indirect (TVar _) = Imposs "extender:analyse";
+        fun check_pcpo lazy T =
+            let val ok = if lazy then cpo_type else pcpo_type
+            in if ok thy T then T
+               else error ("Constructor argument type is not of sort pcpo: " ^
+                           string_of_typ thy T)
+            end;
+        fun analyse_arg (lazy, sel, T) =
+            (lazy, sel, check_pcpo lazy (analyse false T));
+        fun analyse_con (b, args, mx) = (b, map analyse_arg args, mx);
+      in ((dname,distinct_typevars), map analyse_con cons') end; 
+  in ListPair.map analyse_equation (dtnvs,cons'')
+  end; (* let *)
 
 (* ----- calls for building new thy and thms -------------------------------- *)
 
 fun gen_add_domain
-      (prep_typ : theory -> 'a -> typ)
-      (comp_dnam : string)
-      (eqs''' : ((string * string option) list * binding * mixfix *
-                 (binding * (bool * binding option * 'a) list * mixfix) list) list)
-      (thy''' : theory) =
-    let
-      fun readS (SOME s) = Syntax.read_sort_global thy''' s
-        | readS NONE = Sign.defaultS thy''';
-      fun readTFree (a, s) = TFree (a, readS s);
+    (prep_typ : theory -> 'a -> typ)
+    (comp_dnam : string)
+    (eqs''' : ((string * string option) list * binding * mixfix *
+               (binding * (bool * binding option * 'a) list * mixfix) list) list)
+    (thy''' : theory) =
+  let
+    fun readS (SOME s) = Syntax.read_sort_global thy''' s
+      | readS NONE = Sign.defaultS thy''';
+    fun readTFree (a, s) = TFree (a, readS s);
+
+    val dtnvs = map (fn (vs,dname:binding,mx,_) => 
+                        (dname, map readTFree vs, mx)) eqs''';
+    val cons''' = map (fn (_,_,_,cons) => cons) eqs''';
+    fun thy_type  (dname,tvars,mx) = (dname, length tvars, mx);
+    fun thy_arity (dname,tvars,mx) =
+        (Sign.full_name thy''' dname, map (snd o dest_TFree) tvars, pcpoS);
+    val thy'' =
+      thy'''
+      |> Sign.add_types (map thy_type dtnvs)
+      |> fold (AxClass.axiomatize_arity o thy_arity) dtnvs;
+    val cons'' =
+      map (map (upd_second (map (upd_third (prep_typ thy''))))) cons''';
+    val dtnvs' =
+      map (fn (dname,vs,mx) => (Sign.full_name thy''' dname,vs)) dtnvs;
+    val eqs' : ((string * typ list) *
+        (binding * (bool * binding option * typ) list * mixfix) list) list =
+      check_and_sort_domain false dtnvs' cons'' thy'';
+    val thy' = thy'' |> Domain_Syntax.add_syntax false comp_dnam eqs';
+    val dts  = map (Type o fst) eqs';
+    val new_dts = map (fn ((s,Ts),_) => (s, map (fst o dest_TFree) Ts)) eqs';
+    fun strip ss = Library.drop (find_index (fn s => s = "'") ss + 1, ss);
+    fun typid (Type  (id,_)) =
+        let val c = hd (Symbol.explode (Long_Name.base_name id))
+        in if Symbol.is_letter c then c else "t" end
+      | typid (TFree (id,_)   ) = hd (strip (tl (Symbol.explode id)))
+      | typid (TVar ((id,_),_)) = hd (tl (Symbol.explode id));
+    fun one_con (con,args,mx) =
+        ((Syntax.const_name mx (Binding.name_of con)),
+         ListPair.map (fn ((lazy,sel,tp),vn) =>
+           mk_arg ((lazy, DatatypeAux.dtyp_of_typ new_dts tp),
+                   Option.map Binding.name_of sel,vn))
+                      (args,(mk_var_names(map (typid o third) args)))
+        ) : cons;
+    val eqs : eq list =
+        map (fn (dtnvs,cons') => (dtnvs, map one_con cons')) eqs';
+    val thy = thy' |> Domain_Axioms.add_axioms false comp_dnam eqs;
+    val ((rewss, take_rews), theorems_thy) =
+        thy
+          |> fold_map (fn eq => Domain_Theorems.theorems (eq, eqs)) eqs
+          ||>> Domain_Theorems.comp_theorems (comp_dnam, eqs);
+  in
+    theorems_thy
+      |> Sign.add_path (Long_Name.base_name comp_dnam)
+      |> PureThy.add_thmss
+           [((Binding.name "rews", flat rewss @ take_rews), [])]
+      |> snd
+      |> Sign.parent_path
+  end;
 
-      val dtnvs = map (fn (vs,dname:binding,mx,_) => 
-                          (dname, map readTFree vs, mx)) eqs''';
-      val cons''' = map (fn (_,_,_,cons) => cons) eqs''';
-      fun thy_type  (dname,tvars,mx) = (dname, length tvars, mx);
-      fun thy_arity (dname,tvars,mx) = (Sign.full_name thy''' dname, map (snd o dest_TFree) tvars, pcpoS);
-      val thy'' = thy''' |> Sign.add_types (map thy_type dtnvs)
-                         |> fold (AxClass.axiomatize_arity o thy_arity) dtnvs;
-      val cons'' = map (map (upd_second (map (upd_third (prep_typ thy''))))) cons''';
-      val dtnvs' = map (fn (dname,vs,mx) => (Sign.full_name thy''' dname,vs)) dtnvs;
-      val eqs' : ((string * typ list) * (binding * (bool * binding option * typ) list * mixfix) list) list =
-          check_and_sort_domain dtnvs' cons'' thy'';
-      val thy' = thy'' |> Domain_Syntax.add_syntax comp_dnam eqs';
-      val dts  = map (Type o fst) eqs';
-      val new_dts = map (fn ((s,Ts),_) => (s, map (fst o dest_TFree) Ts)) eqs';
-      fun strip ss = Library.drop (find_index (fn s => s = "'") ss + 1, ss);
-      fun typid (Type  (id,_)) =
-          let val c = hd (Symbol.explode (Long_Name.base_name id))
-          in if Symbol.is_letter c then c else "t" end
-        | typid (TFree (id,_)   ) = hd (strip (tl (Symbol.explode id)))
-        | typid (TVar ((id,_),_)) = hd (tl (Symbol.explode id));
-      fun one_con (con,args,mx) =
-          ((Syntax.const_name mx (Binding.name_of con)),
-           ListPair.map (fn ((lazy,sel,tp),vn) => mk_arg ((lazy,
-                                                           DatatypeAux.dtyp_of_typ new_dts tp),
-                                                          Option.map Binding.name_of sel,vn))
-                        (args,(mk_var_names(map (typid o third) args)))
-          ) : cons;
-      val eqs = map (fn (dtnvs,cons') => (dtnvs, map one_con cons')) eqs' : eq list;
-      val thy = thy' |> Domain_Axioms.add_axioms comp_dnam eqs;
-      val ((rewss, take_rews), theorems_thy) =
-          thy |> fold_map (fn eq => Domain_Theorems.theorems (eq, eqs)) eqs
-              ||>> Domain_Theorems.comp_theorems (comp_dnam, eqs);
-    in
-      theorems_thy
-        |> Sign.add_path (Long_Name.base_name comp_dnam)
-        |> (snd o (PureThy.add_thmss [((Binding.name "rews", flat rewss @ take_rews), [])]))
-        |> Sign.parent_path
-    end;
+fun gen_add_new_domain
+    (prep_typ : theory -> 'a -> typ)
+    (comp_dnam : string)
+    (eqs''' : ((string * string option) list * binding * mixfix *
+               (binding * (bool * binding option * 'a) list * mixfix) list) list)
+    (thy''' : theory) =
+  let
+    fun readS (SOME s) = Syntax.read_sort_global thy''' s
+      | readS NONE = Sign.defaultS thy''';
+    fun readTFree (a, s) = TFree (a, readS s);
+
+    val dtnvs = map (fn (vs,dname:binding,mx,_) => 
+                        (dname, map readTFree vs, mx)) eqs''';
+    val cons''' = map (fn (_,_,_,cons) => cons) eqs''';
+    fun thy_type  (dname,tvars,mx) = (dname, length tvars, mx);
+    fun thy_arity (dname,tvars,mx) =
+      (Sign.full_name thy''' dname, map (snd o dest_TFree) tvars, @{sort rep});
+
+    (* this theory is used just for parsing and error checking *)
+    val tmp_thy = thy'''
+      |> Theory.copy
+      |> Sign.add_types (map thy_type dtnvs)
+      |> fold (AxClass.axiomatize_arity o thy_arity) dtnvs;
+
+    val cons'' : (binding * (bool * binding option * typ) list * mixfix) list list =
+      map (map (upd_second (map (upd_third (prep_typ tmp_thy))))) cons''';
+    val dtnvs' : (string * typ list) list =
+      map (fn (dname,vs,mx) => (Sign.full_name thy''' dname,vs)) dtnvs;
+    val eqs' : ((string * typ list) *
+        (binding * (bool * binding option * typ) list * mixfix) list) list =
+      check_and_sort_domain true dtnvs' cons'' tmp_thy;
+
+    fun mk_arg_typ (lazy, dest_opt, T) = if lazy then mk_uT T else T;
+    fun mk_con_typ (bind, args, mx) =
+        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 thy'' = thy''' |>
+      Domain_Isomorphism.domain_isomorphism
+        (map (fn ((vs, dname, mx, _), eq) =>
+                 (map fst vs, dname, mx, mk_eq_typ eq))
+             (eqs''' ~~ eqs'))
+
+    val thy' = thy'' |> Domain_Syntax.add_syntax true comp_dnam eqs';
+    val dts  = map (Type o fst) eqs';
+    val new_dts = map (fn ((s,Ts),_) => (s, map (fst o dest_TFree) Ts)) eqs';
+    fun strip ss = Library.drop (find_index (fn s => s = "'") ss + 1, ss);
+    fun typid (Type  (id,_)) =
+        let val c = hd (Symbol.explode (Long_Name.base_name id))
+        in if Symbol.is_letter c then c else "t" end
+      | typid (TFree (id,_)   ) = hd (strip (tl (Symbol.explode id)))
+      | typid (TVar ((id,_),_)) = hd (tl (Symbol.explode id));
+    fun one_con (con,args,mx) =
+        ((Syntax.const_name mx (Binding.name_of con)),
+         ListPair.map (fn ((lazy,sel,tp),vn) =>
+           mk_arg ((lazy, DatatypeAux.dtyp_of_typ new_dts tp),
+                   Option.map Binding.name_of sel,vn))
+                      (args,(mk_var_names(map (typid o third) args)))
+        ) : cons;
+    val eqs : eq list =
+        map (fn (dtnvs,cons') => (dtnvs, map one_con cons')) eqs';
+    val thy = thy' |> Domain_Axioms.add_axioms true comp_dnam eqs;
+    val ((rewss, take_rews), theorems_thy) =
+        thy
+          |> fold_map (fn eq => Domain_Theorems.theorems (eq, eqs)) eqs
+          ||>> Domain_Theorems.comp_theorems (comp_dnam, eqs);
+  in
+    theorems_thy
+      |> Sign.add_path (Long_Name.base_name comp_dnam)
+      |> PureThy.add_thmss
+           [((Binding.name "rews", flat rewss @ take_rews), [])]
+      |> snd
+      |> Sign.parent_path
+  end;
 
 val add_domain = gen_add_domain Sign.certify_typ;
 val add_domain_cmd = gen_add_domain Syntax.read_typ_global;
 
+val add_new_domain = gen_add_new_domain Sign.certify_typ;
+val add_new_domain_cmd = gen_add_new_domain Syntax.read_typ_global;
+
 
 (** outer syntax **)
 
@@ -157,47 +271,57 @@
 val _ = OuterKeyword.keyword "lazy";
 
 val dest_decl : (bool * binding option * string) parser =
-    P.$$$ "(" |-- Scan.optional (P.$$$ "lazy" >> K true) false --
-      (P.binding >> SOME) -- (P.$$$ "::" |-- P.typ)  --| P.$$$ ")" >> P.triple1
-      || P.$$$ "(" |-- P.$$$ "lazy" |-- P.typ --| P.$$$ ")"
-      >> (fn t => (true,NONE,t))
-      || P.typ >> (fn t => (false,NONE,t));
+  P.$$$ "(" |-- Scan.optional (P.$$$ "lazy" >> K true) false --
+    (P.binding >> SOME) -- (P.$$$ "::" |-- P.typ)  --| P.$$$ ")" >> P.triple1
+    || P.$$$ "(" |-- P.$$$ "lazy" |-- P.typ --| P.$$$ ")"
+    >> (fn t => (true,NONE,t))
+    || P.typ >> (fn t => (false,NONE,t));
 
 val cons_decl =
-    P.binding -- Scan.repeat dest_decl -- P.opt_mixfix;
+  P.binding -- Scan.repeat dest_decl -- P.opt_mixfix;
 
 val type_var' : (string * string option) parser =
-    (P.type_ident -- Scan.option (P.$$$ "::" |-- P.!!! P.sort));
+  (P.type_ident -- Scan.option (P.$$$ "::" |-- P.!!! P.sort));
 
 val type_args' : (string * string option) list parser =
-    type_var' >> single ||
-              P.$$$ "(" |-- P.!!! (P.list1 type_var' --| P.$$$ ")") ||
-              Scan.succeed [];
+  type_var' >> single
+  || P.$$$ "(" |-- P.!!! (P.list1 type_var' --| P.$$$ ")")
+  || Scan.succeed [];
 
 val domain_decl =
-    (type_args' -- P.binding -- P.opt_infix) --
-                                             (P.$$$ "=" |-- P.enum1 "|" cons_decl);
+  (type_args' -- P.binding -- P.opt_infix) --
+    (P.$$$ "=" |-- P.enum1 "|" cons_decl);
 
 val domains_decl =
-    Scan.option (P.$$$ "(" |-- P.name --| P.$$$ ")") --
-                P.and_list1 domain_decl;
+  Scan.option (P.$$$ "(" |-- P.name --| P.$$$ ")") --
+    P.and_list1 domain_decl;
 
-fun mk_domain (opt_name : string option,
-               doms : ((((string * string option) list * binding) * mixfix) *
-                       ((binding * (bool * binding option * string) list) * mixfix) list) list ) =
-    let
-      val names = map (fn (((_, t), _), _) => Binding.name_of t) doms;
-      val specs : ((string * string option) list * binding * mixfix *
-                   (binding * (bool * binding option * string) list * mixfix) list) list =
-          map (fn (((vs, t), mx), cons) =>
-                  (vs, t, mx, map (fn ((c, ds), mx) => (c, ds, mx)) cons)) doms;
-      val comp_dnam =
-          case opt_name of NONE => space_implode "_" names | SOME s => s;
-    in add_domain_cmd comp_dnam specs end;
+fun mk_domain
+    (definitional : bool)
+    (opt_name : string option,
+     doms : ((((string * string option) list * binding) * mixfix) *
+             ((binding * (bool * binding option * string) list) * mixfix) list) list ) =
+  let
+    val names = map (fn (((_, t), _), _) => Binding.name_of t) doms;
+    val specs : ((string * string option) list * binding * mixfix *
+                 (binding * (bool * binding option * string) list * mixfix) list) list =
+        map (fn (((vs, t), mx), cons) =>
+                (vs, t, mx, map (fn ((c, ds), mx) => (c, ds, mx)) cons)) doms;
+    val comp_dnam =
+        case opt_name of NONE => space_implode "_" names | SOME s => s;
+  in
+    if definitional 
+    then add_new_domain_cmd comp_dnam specs
+    else add_domain_cmd comp_dnam specs
+  end;
 
 val _ =
-    OuterSyntax.command "domain" "define recursive domains (HOLCF)" K.thy_decl
-                        (domains_decl >> (Toplevel.theory o mk_domain));
+  OuterSyntax.command "domain" "define recursive domains (HOLCF)"
+    K.thy_decl (domains_decl >> (Toplevel.theory o mk_domain false));
+
+val _ =
+  OuterSyntax.command "new_domain" "define recursive domains (HOLCF)"
+    K.thy_decl (domains_decl >> (Toplevel.theory o mk_domain true));
 
 end;
 
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOLCF/Tools/Domain/domain_isomorphism.ML	Thu Nov 19 20:09:56 2009 -0800
@@ -0,0 +1,636 @@
+(*  Title:      HOLCF/Tools/domain/domain_isomorphism.ML
+    Author:     Brian Huffman
+
+Defines new types satisfying the given domain equations.
+*)
+
+signature DOMAIN_ISOMORPHISM =
+sig
+  val domain_isomorphism:
+    (string list * binding * mixfix * typ) list -> theory -> theory
+  val domain_isomorphism_cmd:
+    (string list * binding * mixfix * string) list -> theory -> theory
+  val add_type_constructor:
+    (string * term * string * thm  * thm) -> theory -> theory
+  val get_map_tab:
+    theory -> string Symtab.table
+end;
+
+structure Domain_Isomorphism :> DOMAIN_ISOMORPHISM =
+struct
+
+val beta_ss =
+  HOL_basic_ss
+    addsimps simp_thms
+    addsimps [@{thm beta_cfun}]
+    addsimprocs [@{simproc cont_proc}];
+
+val beta_tac = simp_tac beta_ss;
+
+(******************************************************************************)
+(******************************** theory data *********************************)
+(******************************************************************************)
+
+structure DeflData = Theory_Data
+(
+  type T = term Symtab.table;
+  val empty = Symtab.empty;
+  val extend = I;
+  fun merge data = Symtab.merge (K true) data;
+);
+
+structure MapData = Theory_Data
+(
+  type T = string Symtab.table;
+  val empty = Symtab.empty;
+  val extend = I;
+  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
+(
+  type T = thm list;
+  val empty = [];
+  val extend = I;
+  val merge = Thm.merge_thms;
+);
+
+fun add_type_constructor
+  (tname, defl_const, map_name, REP_thm, isodefl_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);
+
+val get_map_tab = MapData.get;
+
+
+(******************************************************************************)
+(******************************* building types *******************************)
+(******************************************************************************)
+
+(* ->> is taken from holcf_logic.ML *)
+fun cfunT (T, U) = Type(@{type_name "->"}, [T, U]);
+
+infixr 6 ->>; val (op ->>) = cfunT;
+
+fun dest_cfunT (Type(@{type_name "->"}, [T, U])) = (T, U)
+  | dest_cfunT T = raise TYPE ("dest_cfunT", [T], []);
+
+fun tupleT [] = HOLogic.unitT
+  | tupleT [T] = T
+  | tupleT (T :: Ts) = HOLogic.mk_prodT (T, tupleT Ts);
+
+val deflT = @{typ "udom alg_defl"};
+
+fun mapT (T as Type (_, Ts)) =
+  Library.foldr cfunT (map (fn T => T ->> T) Ts, T ->> T);     
+
+(******************************************************************************)
+(******************************* building terms *******************************)
+(******************************************************************************)
+
+(* builds the expression (v1,v2,..,vn) *)
+fun mk_tuple [] = HOLogic.unit
+|   mk_tuple (t::[]) = t
+|   mk_tuple (t::ts) = HOLogic.mk_prod (t, mk_tuple ts);
+
+(* builds the expression (%(v1,v2,..,vn). rhs) *)
+fun lambda_tuple [] rhs = Term.lambda (Free("unit", HOLogic.unitT)) rhs
+  | lambda_tuple (v::[]) rhs = Term.lambda v rhs
+  | lambda_tuple (v::vs) rhs =
+      HOLogic.mk_split (Term.lambda v (lambda_tuple vs rhs));
+
+(* continuous application and abstraction *)
+
+fun capply_const (S, T) =
+  Const(@{const_name Rep_CFun}, (S ->> T) --> (S --> T));
+
+fun cabs_const (S, T) =
+  Const(@{const_name Abs_CFun}, (S --> T) --> (S ->> T));
+
+fun mk_cabs t =
+  let val T = Term.fastype_of t
+  in cabs_const (Term.domain_type T, Term.range_type T) $ t end
+
+(* builds the expression (LAM v. rhs) *)
+fun big_lambda v rhs =
+  cabs_const (Term.fastype_of v, Term.fastype_of rhs) $ Term.lambda v rhs;
+
+(* builds the expression (LAM v1 v2 .. vn. rhs) *)
+fun big_lambdas [] rhs = rhs
+  | big_lambdas (v::vs) rhs = big_lambda v (big_lambdas vs rhs);
+
+fun mk_capply (t, u) =
+  let val (S, T) =
+    case Term.fastype_of t of
+        Type(@{type_name "->"}, [S, T]) => (S, T)
+      | _ => raise TERM ("mk_capply " ^ ML_Syntax.print_list ML_Syntax.print_term [t, u], [t, u]);
+  in capply_const (S, T) $ t $ u end;
+
+(* miscellaneous term constructions *)
+
+val mk_trp = HOLogic.mk_Trueprop;
+
+val mk_fst = HOLogic.mk_fst;
+val mk_snd = HOLogic.mk_snd;
+
+fun mk_cont t =
+  let val T = Term.fastype_of t
+  in Const(@{const_name cont}, T --> HOLogic.boolT) $ t end;
+
+fun mk_fix t =
+  let val (T, _) = dest_cfunT (Term.fastype_of t)
+  in mk_capply (Const(@{const_name fix}, (T ->> T) ->> T), t) end;
+
+fun ID_const T = Const (@{const_name ID}, cfunT (T, T));
+
+fun cfcomp_const (T, U, V) =
+  Const (@{const_name cfcomp}, (U ->> V) ->> (T ->> U) ->> (T ->> V));
+
+fun mk_cfcomp (f, g) =
+  let
+    val (U, V) = dest_cfunT (Term.fastype_of f);
+    val (T, U') = dest_cfunT (Term.fastype_of g);
+  in
+    if U = U'
+    then mk_capply (mk_capply (cfcomp_const (T, U, V), f), g)
+    else raise TYPE ("mk_cfcomp", [U, U'], [f, g])
+  end;
+
+fun mk_Rep_of T =
+  Const (@{const_name Rep_of}, Term.itselfT T --> deflT) $ Logic.mk_type T;
+
+fun coerce_const T = Const (@{const_name coerce}, T);
+
+fun isodefl_const T =
+  Const (@{const_name isodefl}, (T ->> T) --> deflT --> HOLogic.boolT);
+
+(* splits a cterm into the right and lefthand sides of equality *)
+fun dest_eqs t = HOLogic.dest_eq (HOLogic.dest_Trueprop t);
+
+fun mk_eqs (t, u) = HOLogic.mk_Trueprop (HOLogic.mk_eq (t, u));
+
+(******************************************************************************)
+(*************** fixed-point definitions and unfolding theorems ***************)
+(******************************************************************************)
+
+fun add_fixdefs
+    (spec : (binding * term) list)
+    (thy : theory) : (thm list * thm list) * theory =
+  let
+    val binds = map fst spec;
+    val (lhss, rhss) = ListPair.unzip (map (dest_eqs o snd) spec);
+    val functional = lambda_tuple lhss (mk_tuple rhss);
+    val fixpoint = mk_fix (mk_cabs functional);
+
+    (* project components of fixpoint *)
+    fun mk_projs (x::[]) t = [(x, t)]
+      | mk_projs (x::xs) t = (x, mk_fst t) :: mk_projs xs (mk_snd t);
+    val projs = mk_projs lhss fixpoint;
+
+    (* convert parameters to lambda abstractions *)
+    fun mk_eqn (lhs, rhs) =
+        case lhs of
+          Const (@{const_name Rep_CFun}, _) $ f $ (x as Free _) =>
+            mk_eqn (f, big_lambda x rhs)
+        | Const _ => Logic.mk_equals (lhs, rhs)
+        | _ => raise TERM ("lhs not of correct form", [lhs, rhs]);
+    val eqns = map mk_eqn projs;
+
+    (* register constant definitions *)
+    val (fixdef_thms, thy) =
+      (PureThy.add_defs false o map Thm.no_attributes)
+        (map (Binding.suffix_name "_def") binds ~~ eqns) thy;
+
+    (* prove applied version of definitions *)
+    fun prove_proj (lhs, rhs) =
+      let
+        val tac = rewrite_goals_tac fixdef_thms THEN beta_tac 1;
+        val goal = Logic.mk_equals (lhs, rhs);
+      in Goal.prove_global thy [] [] goal (K tac) end;
+    val proj_thms = map prove_proj projs;
+
+    (* mk_tuple lhss == fixpoint *)
+    fun pair_equalI (thm1, thm2) = @{thm Pair_equalI} OF [thm1, thm2];
+    val tuple_fixdef_thm = foldr1 pair_equalI proj_thms;
+
+    val cont_thm =
+      Goal.prove_global thy [] [] (mk_trp (mk_cont functional))
+        (K (beta_tac 1));
+    val tuple_unfold_thm =
+      (@{thm def_cont_fix_eq} OF [tuple_fixdef_thm, cont_thm])
+      |> LocalDefs.unfold (ProofContext.init thy) @{thms split_conv};
+
+    fun mk_unfold_thms [] thm = []
+      | mk_unfold_thms (n::[]) thm = [(n, thm)]
+      | mk_unfold_thms (n::ns) thm = let
+          val thmL = thm RS @{thm Pair_eqD1};
+          val thmR = thm RS @{thm Pair_eqD2};
+        in (n, thmL) :: mk_unfold_thms ns thmR end;
+    val unfold_binds = map (Binding.suffix_name "_unfold") binds;
+
+    (* register unfold theorems *)
+    val (unfold_thms, thy) =
+      (PureThy.add_thms o map (Thm.no_attributes o apsnd Drule.standard))
+        (mk_unfold_thms unfold_binds tuple_unfold_thm) thy;
+  in
+    ((proj_thms, unfold_thms), thy)
+  end;
+
+
+(******************************************************************************)
+(****************** deflation combinators and map functions *******************)
+(******************************************************************************)
+
+fun defl_of_typ
+    (tab : term Symtab.table)
+    (T : typ) : term =
+  let
+    fun is_closed_typ (Type (_, Ts)) = forall is_closed_typ Ts
+      | is_closed_typ _ = false;
+    fun defl_of (TFree (a, _)) = Free (Library.unprefix "'" a, deflT)
+      | defl_of (TVar _) = error ("defl_of_typ: TVar")
+      | defl_of (T as Type (c, Ts)) =
+        case Symtab.lookup tab c of
+          SOME t => Library.foldl mk_capply (t, map defl_of Ts)
+        | NONE => if is_closed_typ T
+                  then mk_Rep_of T
+                  else error ("defl_of_typ: type variable under unsupported type constructor " ^ c);
+  in defl_of T end;
+
+fun map_of_typ
+    (tab : string Symtab.table)
+    (T : typ) : term =
+  let
+    fun is_closed_typ (Type (_, Ts)) = forall is_closed_typ Ts
+      | is_closed_typ _ = false;
+    fun map_of (T as TFree (a, _)) = Free (Library.unprefix "'" a, T ->> T)
+      | map_of (T as TVar _) = error ("map_of_typ: TVar")
+      | map_of (T as Type (c, Ts)) =
+        case Symtab.lookup tab c of
+          SOME t => Library.foldl mk_capply (Const (t, mapT T), map map_of Ts)
+        | NONE => if is_closed_typ T
+                  then ID_const T
+                  else error ("map_of_typ: type variable under unsupported type constructor " ^ c);
+  in map_of T end;
+
+
+(******************************************************************************)
+(* prepare datatype specifications *)
+
+fun read_typ thy str sorts =
+  let
+    val ctxt = ProofContext.init thy
+      |> fold (Variable.declare_typ o TFree) sorts;
+    val T = Syntax.read_typ ctxt str;
+  in (T, Term.add_tfreesT T sorts) end;
+
+fun cert_typ sign raw_T sorts =
+  let
+    val T = Type.no_tvars (Sign.certify_typ sign raw_T)
+      handle TYPE (msg, _, _) => error msg;
+    val sorts' = Term.add_tfreesT T sorts;
+    val _ =
+      case duplicates (op =) (map fst sorts') of
+        [] => ()
+      | dups => error ("Inconsistent sort constraints for " ^ commas dups)
+  in (T, sorts') end;
+
+fun gen_domain_isomorphism
+    (prep_typ: theory -> 'a -> (string * sort) list -> typ * (string * sort) list)
+    (doms_raw: (string list * binding * mixfix * 'a) list)
+    (thy: theory)
+    : theory =
+  let
+    val _ = Theory.requires thy "Representable" "domain isomorphisms";
+
+    (* this theory is used just for parsing *)
+    val tmp_thy = thy |>
+      Theory.copy |>
+      Sign.add_types (map (fn (tvs, tname, mx, _) =>
+        (tname, length tvs, mx)) doms_raw);
+
+    fun prep_dom thy (vs, t, mx, typ_raw) sorts =
+      let val (typ, sorts') = prep_typ thy typ_raw sorts
+      in ((vs, t, mx, typ), sorts') end;
+
+    val (doms : (string list * binding * mixfix * typ) list,
+         sorts : (string * sort) list) =
+      fold_map (prep_dom tmp_thy) doms_raw [];
+
+    (* domain equations *)
+    fun mk_dom_eqn (vs, tbind, mx, rhs) =
+      let fun arg v = TFree (v, the (AList.lookup (op =) sorts v));
+      in (Type (Sign.full_name tmp_thy tbind, map arg vs), rhs) end;
+    val dom_eqns = map mk_dom_eqn doms;
+
+    (* check for valid type parameters *)
+    val (tyvars, _, _, _)::_ = doms;
+    val new_doms = map (fn (tvs, tname, mx, _) =>
+      let val full_tname = Sign.full_name tmp_thy tname
+      in
+        (case duplicates (op =) tvs of
+          [] =>
+            if eq_set (op =) (tyvars, tvs) then (full_tname, tvs)
+            else error ("Mutually recursive domains must have same type parameters")
+        | dups => error ("Duplicate parameter(s) for domain " ^ quote (Binding.str_of tname) ^
+            " : " ^ commas dups))
+      end) doms;
+    val dom_binds = map (fn (_, tbind, _, _) => tbind) doms;
+
+    (* declare deflation combinator constants *)
+    fun declare_defl_const (vs, tbind, mx, rhs) thy =
+      let
+        val defl_type = Library.foldr cfunT (map (K deflT) vs, deflT);
+        val defl_bind = Binding.suffix_name "_defl" tbind;
+      in
+        Sign.declare_const ((defl_bind, defl_type), NoSyn) thy
+      end;
+    val (defl_consts, thy) = fold_map declare_defl_const doms thy;
+
+    (* defining equations for type combinators *)
+    val defl_tab1 = DeflData.get thy;
+    val defl_tab2 =
+      Symtab.make (map (fst o dest_Type o fst) dom_eqns ~~ defl_consts);
+    val defl_tab' = Symtab.merge (K true) (defl_tab1, defl_tab2);
+    val thy = DeflData.put defl_tab' thy;
+    fun mk_defl_spec (lhsT, rhsT) =
+      mk_eqs (defl_of_typ defl_tab' lhsT,
+              defl_of_typ defl_tab' rhsT);
+    val defl_specs = map mk_defl_spec dom_eqns;
+
+    (* register recursive definition of deflation combinators *)
+    val defl_binds = map (Binding.suffix_name "_defl") dom_binds;
+    val ((defl_apply_thms, defl_unfold_thms), thy) =
+      add_fixdefs (defl_binds ~~ defl_specs) thy;
+
+    (* define types using deflation combinators *)
+    fun make_repdef ((vs, tbind, mx, _), defl_const) thy =
+      let
+        fun tfree a = TFree (a, the (AList.lookup (op =) sorts a))
+        val reps = map (mk_Rep_of o tfree) vs;
+        val defl = Library.foldl mk_capply (defl_const, reps);
+        val ((_, _, _, {REP, ...}), thy) =
+          Repdef.add_repdef false NONE (tbind, vs, mx) defl NONE thy;
+      in
+        (REP, thy)
+      end;
+    val (REP_thms, thy) = fold_map make_repdef (doms ~~ defl_consts) thy;
+    val thy = RepData.map (fold Thm.add_thm REP_thms) thy;
+
+    (* prove REP equations *)
+    fun mk_REP_eq_thm (lhsT, rhsT) =
+      let
+        val goal = mk_eqs (mk_Rep_of lhsT, mk_Rep_of rhsT);
+        val REP_simps = RepData.get thy;
+        val tac =
+          simp_tac (HOL_basic_ss addsimps REP_simps) 1
+          THEN resolve_tac defl_unfold_thms 1;
+      in
+        Goal.prove_global thy [] [] goal (K tac)
+      end;
+    val REP_eq_thms = map mk_REP_eq_thm dom_eqns;
+
+    (* register REP equations *)
+    val REP_eq_binds = map (Binding.prefix_name "REP_eq_") dom_binds;
+    val (_, thy) = thy |>
+      (PureThy.add_thms o map Thm.no_attributes)
+        (REP_eq_binds ~~ REP_eq_thms);
+
+    (* define rep/abs functions *)
+    fun mk_rep_abs (tbind, (lhsT, rhsT)) thy =
+      let
+        val rep_type = cfunT (lhsT, rhsT);
+        val abs_type = cfunT (rhsT, lhsT);
+        val rep_bind = Binding.suffix_name "_rep" tbind;
+        val abs_bind = Binding.suffix_name "_abs" tbind;
+        val (rep_const, thy) = thy |>
+          Sign.declare_const ((rep_bind, rep_type), NoSyn);
+        val (abs_const, thy) = thy |>
+          Sign.declare_const ((abs_bind, abs_type), NoSyn);
+        val rep_eqn = Logic.mk_equals (rep_const, coerce_const rep_type);
+        val abs_eqn = Logic.mk_equals (abs_const, coerce_const abs_type);
+        val ([rep_def, abs_def], thy) = thy |>
+          (PureThy.add_defs false o map Thm.no_attributes)
+            [(Binding.suffix_name "_rep_def" tbind, rep_eqn),
+             (Binding.suffix_name "_abs_def" tbind, abs_eqn)];
+      in
+        (((rep_const, abs_const), (rep_def, abs_def)), thy)
+      end;
+    val ((rep_abs_consts, rep_abs_defs), thy) = thy
+      |> fold_map mk_rep_abs (dom_binds ~~ dom_eqns)
+      |>> ListPair.unzip;
+
+    (* prove isomorphism and isodefl rules *)
+    fun mk_iso_thms ((tbind, REP_eq), (rep_def, abs_def)) thy =
+      let
+        fun make thm = Drule.standard (thm OF [REP_eq, abs_def, rep_def]);
+        val rep_iso_thm = make @{thm domain_rep_iso};
+        val abs_iso_thm = make @{thm domain_abs_iso};
+        val isodefl_thm = make @{thm isodefl_abs_rep};
+        val rep_iso_bind = Binding.name "rep_iso";
+        val abs_iso_bind = Binding.name "abs_iso";
+        val isodefl_bind = Binding.name "isodefl_abs_rep";
+        val (_, thy) = thy
+          |> Sign.add_path (Binding.name_of tbind)
+          |> (PureThy.add_thms o map Thm.no_attributes)
+              [(rep_iso_bind, rep_iso_thm),
+               (abs_iso_bind, abs_iso_thm),
+               (isodefl_bind, isodefl_thm)]
+          ||> Sign.parent_path;
+      in
+        (((rep_iso_thm, abs_iso_thm), isodefl_thm), thy)
+      end;
+    val ((iso_thms, isodefl_abs_rep_thms), thy) = thy
+      |> fold_map mk_iso_thms (dom_binds ~~ REP_eq_thms ~~ rep_abs_defs)
+      |>> ListPair.unzip;
+
+    (* declare map functions *)
+    fun declare_map_const (tbind, (lhsT, rhsT)) thy =
+      let
+        val map_type = mapT lhsT;
+        val map_bind = Binding.suffix_name "_map" tbind;
+      in
+        Sign.declare_const ((map_bind, map_type), NoSyn) thy
+      end;
+    val (map_consts, thy) = thy |>
+      fold_map declare_map_const (dom_binds ~~ dom_eqns);
+
+    (* defining equations for map functions *)
+    val map_tab1 = MapData.get thy;
+    val map_tab2 =
+      Symtab.make (map (fst o dest_Type o fst) dom_eqns
+                   ~~ map (fst o dest_Const) map_consts);
+    val map_tab' = Symtab.merge (K true) (map_tab1, map_tab2);
+    val thy = MapData.put map_tab' thy;
+    fun mk_map_spec ((rep_const, abs_const), (lhsT, rhsT)) =
+      let
+        val lhs = map_of_typ map_tab' lhsT;
+        val body = map_of_typ map_tab' rhsT;
+        val rhs = mk_cfcomp (abs_const, mk_cfcomp (body, rep_const));
+      in mk_eqs (lhs, rhs) end;
+    val map_specs = map mk_map_spec (rep_abs_consts ~~ dom_eqns);
+
+    (* register recursive definition of map functions *)
+    val map_binds = map (Binding.suffix_name "_map") dom_binds;
+    val ((map_apply_thms, map_unfold_thms), thy) =
+      add_fixdefs (map_binds ~~ map_specs) thy;
+
+    (* prove isodefl rules for map functions *)
+    val isodefl_thm =
+      let
+        fun unprime a = Library.unprefix "'" a;
+        fun mk_d (TFree (a, _)) = Free ("d" ^ unprime a, deflT);
+        fun mk_f (T as TFree (a, _)) = Free ("f" ^ unprime a, T ->> T);
+        fun mk_assm T = mk_trp (isodefl_const T $ mk_f T $ mk_d T);
+        fun mk_goal ((map_const, defl_const), (T as Type (c, Ts), rhsT)) =
+          let
+            val map_term = Library.foldl mk_capply (map_const, map mk_f Ts);
+            val defl_term = Library.foldl mk_capply (defl_const, map mk_d Ts);
+          in isodefl_const T $ map_term $ defl_term end;
+        val assms = (map mk_assm o snd o dest_Type o fst o hd) dom_eqns;
+        val goals = map mk_goal (map_consts ~~ defl_consts ~~ dom_eqns);
+        val goal = mk_trp (foldr1 HOLogic.mk_conj goals);
+        val start_thms =
+          @{thm split_def} :: defl_apply_thms @ map_apply_thms;
+        val adm_rules =
+          @{thms adm_conj adm_isodefl cont2cont_fst cont2cont_snd cont_id};
+        val bottom_rules =
+          @{thms fst_strict snd_strict isodefl_bottom simp_thms};
+        val isodefl_rules =
+          @{thms conjI isodefl_ID_REP}
+          @ isodefl_abs_rep_thms
+          @ IsodeflData.get thy;
+        fun tacf {prems, ...} = EVERY
+          [simp_tac (HOL_basic_ss addsimps start_thms) 1,
+           (* FIXME: how reliable is unification here? *)
+           (* Maybe I should instantiate the rule. *)
+           rtac @{thm parallel_fix_ind} 1,
+           REPEAT (resolve_tac adm_rules 1),
+           simp_tac (HOL_basic_ss addsimps bottom_rules) 1,
+           simp_tac beta_ss 1,
+           simp_tac (HOL_basic_ss addsimps @{thms fst_conv snd_conv}) 1,
+           REPEAT (etac @{thm conjE} 1),
+           REPEAT (resolve_tac (isodefl_rules @ prems) 1 ORELSE atac 1)];
+      in
+        Goal.prove_global thy [] assms goal tacf
+      end;
+    val isodefl_binds = map (Binding.prefix_name "isodefl_") dom_binds;
+    fun conjuncts [] thm = []
+      | conjuncts (n::[]) thm = [(n, thm)]
+      | conjuncts (n::ns) thm = let
+          val thmL = thm RS @{thm conjunct1};
+          val thmR = thm RS @{thm conjunct2};
+        in (n, thmL):: conjuncts ns thmR end;
+    val (isodefl_thms, thy) = thy |>
+      (PureThy.add_thms o map (Thm.no_attributes o apsnd Drule.standard))
+        (conjuncts isodefl_binds isodefl_thm);
+    val thy = IsodeflData.map (fold Thm.add_thm isodefl_thms) thy;
+
+    (* prove map_ID theorems *)
+    fun prove_map_ID_thm
+        (((map_const, (lhsT, _)), REP_thm), isodefl_thm) =
+      let
+        val Ts = snd (dest_Type lhsT);
+        val lhs = Library.foldl mk_capply (map_const, map ID_const Ts);
+        val goal = mk_eqs (lhs, ID_const lhsT);
+        val tac = EVERY
+          [rtac @{thm isodefl_REP_imp_ID} 1,
+           stac REP_thm 1,
+           rtac isodefl_thm 1,
+           REPEAT (rtac @{thm isodefl_ID_REP} 1)];
+      in
+        Goal.prove_global thy [] [] goal (K tac)
+      end;
+    val map_ID_binds = map (Binding.suffix_name "_map_ID") dom_binds;
+    val map_ID_thms =
+      map prove_map_ID_thm
+        (map_consts ~~ dom_eqns ~~ REP_thms ~~ isodefl_thms);
+    val (_, thy) = thy |>
+      (PureThy.add_thms o map Thm.no_attributes)
+        (map_ID_binds ~~ map_ID_thms);
+
+    (* define copy combinators *)
+    val new_dts =
+      map (apsnd (map (fst o dest_TFree)) o dest_Type o fst) dom_eqns;
+    val copy_arg_type = tupleT (map (fn (T, _) => T ->> T) dom_eqns);
+    val copy_args =
+      let fun mk_copy_args [] t = []
+            | mk_copy_args (_::[]) t = [t]
+            | mk_copy_args (_::xs) t =
+              HOLogic.mk_fst t :: mk_copy_args xs (HOLogic.mk_snd t);
+      in mk_copy_args doms (Free ("f", copy_arg_type)) end;
+    fun copy_of_dtyp (T, dt) =
+        if DatatypeAux.is_rec_type dt
+        then copy_of_dtyp' (T, dt)
+        else ID_const T
+    and copy_of_dtyp' (T, DatatypeAux.DtRec i) = nth copy_args i
+      | copy_of_dtyp' (T, DatatypeAux.DtTFree a) = ID_const T
+      | copy_of_dtyp' (T as Type (_, Ts), DatatypeAux.DtType (c, ds)) =
+        case Symtab.lookup map_tab' c of
+          SOME f =>
+          Library.foldl mk_capply
+            (Const (f, mapT T), map copy_of_dtyp (Ts ~~ ds))
+        | NONE =>
+          (warning ("copy_of_dtyp: unknown type constructor " ^ c); ID_const T);
+    fun define_copy ((tbind, (rep_const, abs_const)), (lhsT, rhsT)) thy =
+      let
+        val copy_type = copy_arg_type ->> (lhsT ->> lhsT);
+        val copy_bind = Binding.suffix_name "_copy" tbind;
+        val (copy_const, thy) = thy |>
+          Sign.declare_const ((copy_bind, copy_type), NoSyn);
+        val dtyp = DatatypeAux.dtyp_of_typ new_dts rhsT;
+        val body = copy_of_dtyp (rhsT, dtyp);
+        val comp = mk_cfcomp (abs_const, mk_cfcomp (body, rep_const));
+        val rhs = big_lambda (Free ("f", copy_arg_type)) comp;
+        val eqn = Logic.mk_equals (copy_const, rhs);
+        val ([copy_def], thy) =
+          thy
+          |> Sign.add_path (Binding.name_of tbind)
+          |> (PureThy.add_defs false o map Thm.no_attributes)
+              [(Binding.name "copy_def", eqn)]
+          ||> Sign.parent_path;
+      in ((copy_const, copy_def), thy) end;
+    val ((copy_consts, copy_defs), thy) = thy
+      |> fold_map define_copy (dom_binds ~~ rep_abs_consts ~~ dom_eqns)
+      |>> ListPair.unzip;
+
+  in
+    thy
+  end;
+
+val domain_isomorphism = gen_domain_isomorphism cert_typ;
+val domain_isomorphism_cmd = gen_domain_isomorphism read_typ;
+
+(******************************************************************************)
+(******************************** outer syntax ********************************)
+(******************************************************************************)
+
+local
+
+structure P = OuterParse and K = OuterKeyword
+
+val parse_domain_iso : (string list * binding * mixfix * string) parser =
+  (P.type_args -- P.binding -- P.opt_infix -- (P.$$$ "=" |-- P.typ))
+    >> (fn (((vs, t), mx), rhs) => (vs, t, mx, rhs));
+
+val parse_domain_isos = P.and_list1 parse_domain_iso;
+
+in
+
+val _ =
+  OuterSyntax.command "domain_isomorphism" "define domain isomorphisms (HOLCF)" K.thy_decl
+    (parse_domain_isos >> (Toplevel.theory o domain_isomorphism_cmd));
+
+end;
+
+end;
--- a/src/HOLCF/Tools/Domain/domain_syntax.ML	Fri Nov 20 00:54:20 2009 +0100
+++ b/src/HOLCF/Tools/Domain/domain_syntax.ML	Thu Nov 19 20:09:56 2009 -0800
@@ -7,12 +7,14 @@
 signature DOMAIN_SYNTAX =
 sig
   val calc_syntax:
+      bool ->
       typ ->
       (string * typ list) *
       (binding * (bool * binding option * typ) list * mixfix) list ->
       (binding * typ * mixfix) list * ast Syntax.trrule list
 
   val add_syntax:
+      bool ->
       string ->
       ((string * typ list) *
        (binding * (bool * binding option * typ) list * mixfix) list) list ->
@@ -27,155 +29,176 @@
 infixr 5 -->; infixr 6 ->>;
 
 fun calc_syntax
-      (dtypeprod : typ)
-      ((dname : string, typevars : typ list), 
-       (cons': (binding * (bool * binding option * typ) list * mixfix) list))
+    (definitional : bool)
+    (dtypeprod : typ)
+    ((dname : string, typevars : typ list), 
+     (cons': (binding * (bool * binding option * typ) list * mixfix) list))
     : (binding * typ * mixfix) list * ast Syntax.trrule list =
-    let
-      (* ----- constants concerning the isomorphism ------------------------------- *)
+  let
+(* ----- constants concerning the isomorphism ------------------------------- *)
+    local
+      fun opt_lazy (lazy,_,t) = if lazy then mk_uT t else t
+      fun prod     (_,args,_) = case args of [] => oneT
+                                           | _ => foldr1 mk_sprodT (map opt_lazy args);
+      fun freetvar s = let val tvar = mk_TFree s in
+                         if tvar mem typevars then freetvar ("t"^s) else tvar end;
+      fun when_type (_,args,_) = List.foldr (op ->>) (freetvar "t") (map third args);
+    in
+    val dtype  = Type(dname,typevars);
+    val dtype2 = foldr1 mk_ssumT (map prod cons');
+    val dnam = Long_Name.base_name dname;
+    fun dbind s = Binding.name (dnam ^ s);
+    val const_rep  = (dbind "_rep" ,              dtype  ->> dtype2, NoSyn);
+    val const_abs  = (dbind "_abs" ,              dtype2 ->> dtype , NoSyn);
+    val const_when = (dbind "_when", List.foldr (op ->>) (dtype ->> freetvar "t") (map when_type cons'), NoSyn);
+    val const_copy = (dbind "_copy", dtypeprod ->> dtype  ->> dtype , NoSyn);
+    end;
 
-      local
-        fun opt_lazy (lazy,_,t) = if lazy then mk_uT t else t
-        fun prod     (_,args,_) = case args of [] => oneT
-                                             | _ => foldr1 mk_sprodT (map opt_lazy args);
-        fun freetvar s = let val tvar = mk_TFree s in
-                           if tvar mem typevars then freetvar ("t"^s) else tvar end;
-        fun when_type (_,args,_) = List.foldr (op ->>) (freetvar "t") (map third args);
-      in
-      val dtype  = Type(dname,typevars);
-      val dtype2 = foldr1 mk_ssumT (map prod cons');
-      val dnam = Long_Name.base_name dname;
-      fun dbind s = Binding.name (dnam ^ s);
-      val const_rep  = (dbind "_rep" ,              dtype  ->> dtype2, NoSyn);
-      val const_abs  = (dbind "_abs" ,              dtype2 ->> dtype , NoSyn);
-      val const_when = (dbind "_when", List.foldr (op ->>) (dtype ->> freetvar "t") (map when_type cons'), NoSyn);
-      val const_copy = (dbind "_copy", dtypeprod ->> dtype  ->> dtype , NoSyn);
-      end;
+(* ----- constants concerning constructors, discriminators, and selectors --- *)
+
+    local
+      val escape = let
+        fun esc (c::cs) = if c mem ["'","_","(",")","/"] then "'"::c::esc cs
+                          else      c::esc cs
+          |   esc []      = []
+      in implode o esc o Symbol.explode end;
 
-      (* ----- constants concerning constructors, discriminators, and selectors --- *)
+      fun dis_name_ con =
+          Binding.name ("is_" ^ strip_esc (Binding.name_of con));
+      fun mat_name_ con =
+          Binding.name ("match_" ^ strip_esc (Binding.name_of con));
+      fun pat_name_ con =
+          Binding.name (strip_esc (Binding.name_of con) ^ "_pat");
+      fun con (name,args,mx) =
+          (name, List.foldr (op ->>) dtype (map third args), mx);
+      fun dis (con,args,mx) =
+          (dis_name_ con, dtype->>trT,
+           Mixfix(escape ("is_" ^ Binding.name_of con), [], Syntax.max_pri));
+      (* strictly speaking, these constants have one argument,
+       but the mixfix (without arguments) is introduced only
+           to generate parse rules for non-alphanumeric names*)
+      fun freetvar s n =
+          let val tvar = mk_TFree (s ^ string_of_int n)
+          in if tvar mem typevars then freetvar ("t"^s) n else tvar end;
 
-      local
-        val escape = let
-          fun esc (c::cs) = if c mem ["'","_","(",")","/"] then "'"::c::esc cs
-                            else      c::esc cs
-            |   esc []      = []
-        in implode o esc o Symbol.explode end;
-        fun dis_name_ con     = Binding.name ("is_" ^ strip_esc (Binding.name_of con));
-        fun mat_name_ con     = Binding.name ("match_" ^ strip_esc (Binding.name_of con));
-        fun pat_name_ con     = Binding.name (strip_esc (Binding.name_of con) ^ "_pat");
-        fun con (name,args,mx) = (name, List.foldr (op ->>) dtype (map third args), mx);
-        fun dis (con,args,mx) = (dis_name_ con, dtype->>trT,
-                                 Mixfix(escape ("is_" ^ Binding.name_of con), [], Syntax.max_pri));
-        (* strictly speaking, these constants have one argument,
-         but the mixfix (without arguments) is introduced only
-             to generate parse rules for non-alphanumeric names*)
-        fun freetvar s n      = let val tvar = mk_TFree (s ^ string_of_int n) in
-                                  if tvar mem typevars then freetvar ("t"^s) n else tvar end;
-        fun mk_matT (a,bs,c)  = a ->> List.foldr (op ->>) (mk_maybeT c) bs ->> mk_maybeT c;
-        fun mat (con,args,mx) = (mat_name_ con,
-                                 mk_matT(dtype, map third args, freetvar "t" 1),
-                                 Mixfix(escape ("match_" ^ Binding.name_of con), [], Syntax.max_pri));
-        fun sel1 (_,sel,typ)  = Option.map (fn s => (s,dtype ->> typ,NoSyn)) sel;
-        fun sel (con,args,mx) = map_filter sel1 args;
-        fun mk_patT (a,b)     = a ->> mk_maybeT b;
-        fun pat_arg_typ n arg = mk_patT (third arg, freetvar "t" n);
-        fun pat (con,args,mx) = (pat_name_ con,
-                                 (mapn pat_arg_typ 1 args)
-                                   --->
-                                   mk_patT (dtype, mk_ctupleT (map (freetvar "t") (1 upto length args))),
-                                 Mixfix(escape (Binding.name_of con ^ "_pat"), [], Syntax.max_pri));
+      fun mk_matT (a,bs,c) =
+          a ->> List.foldr (op ->>) (mk_maybeT c) bs ->> mk_maybeT c;
+      fun mat (con,args,mx) =
+          (mat_name_ con,
+           mk_matT(dtype, map third args, freetvar "t" 1),
+           Mixfix(escape ("match_" ^ Binding.name_of con), [], Syntax.max_pri));
+      fun sel1 (_,sel,typ) =
+          Option.map (fn s => (s,dtype ->> typ,NoSyn)) sel;
+      fun sel (con,args,mx) = map_filter sel1 args;
+      fun mk_patT (a,b)     = a ->> mk_maybeT b;
+      fun pat_arg_typ n arg = mk_patT (third arg, freetvar "t" n);
+      fun pat (con,args,mx) =
+          (pat_name_ con,
+           (mapn pat_arg_typ 1 args)
+             --->
+             mk_patT (dtype, mk_ctupleT (map (freetvar "t") (1 upto length args))),
+           Mixfix(escape (Binding.name_of con ^ "_pat"), [], Syntax.max_pri));
+    in
+    val consts_con = map con cons';
+    val consts_dis = map dis cons';
+    val consts_mat = map mat cons';
+    val consts_pat = map pat cons';
+    val consts_sel = maps sel cons';
+    end;
+
+(* ----- constants concerning induction ------------------------------------- *)
+
+    val const_take   = (dbind "_take"  , HOLogic.natT-->dtype->>dtype, NoSyn);
+    val const_finite = (dbind "_finite", dtype-->HOLogic.boolT       , NoSyn);
+
+(* ----- case translation --------------------------------------------------- *)
 
+    local open Syntax in
+    local
+      fun c_ast con mx = Constant (Syntax.const_name mx (Binding.name_of con));
+      fun expvar n     = Variable ("e"^(string_of_int n));
+      fun argvar n m _ = Variable ("a"^(string_of_int n)^"_"^
+                                   (string_of_int m));
+      fun argvars n args = mapn (argvar n) 1 args;
+      fun app s (l,r)  = mk_appl (Constant s) [l,r];
+      val cabs = app "_cabs";
+      val capp = app "Rep_CFun";
+      fun con1 n (con,args,mx) = Library.foldl capp (c_ast con mx, argvars n args);
+      fun case1 n (con,args,mx) = app "_case1" (con1 n (con,args,mx), expvar n);
+      fun arg1 n (con,args,_) = List.foldr cabs (expvar n) (argvars n args);
+      fun when1 n m = if n = m then arg1 n else K (Constant "UU");
+          
+      fun app_var x = mk_appl (Constant "_variable") [x, Variable "rhs"];
+      fun app_pat x = mk_appl (Constant "_pat") [x];
+      fun args_list [] = Constant "_noargs"
+        |   args_list xs = foldr1 (app "_args") xs;
+    in
+    val case_trans =
+        ParsePrintRule
+          (app "_case_syntax" (Variable "x", foldr1 (app "_case2") (mapn case1 1 cons')),
+           capp (Library.foldl capp (Constant (dnam^"_when"), mapn arg1 1 cons'), Variable "x"));
+        
+    fun one_abscon_trans n (con,mx,args) =
+        ParsePrintRule
+          (cabs (con1 n (con,mx,args), expvar n),
+           Library.foldl capp (Constant (dnam^"_when"), mapn (when1 n) 1 cons'));
+    val abscon_trans = mapn one_abscon_trans 1 cons';
+        
+    fun one_case_trans (con,args,mx) =
+      let
+        val cname = c_ast con mx;
+        val pname = Constant (strip_esc (Binding.name_of con) ^ "_pat");
+        val ns = 1 upto length args;
+        val xs = map (fn n => Variable ("x"^(string_of_int n))) ns;
+        val ps = map (fn n => Variable ("p"^(string_of_int n))) ns;
+        val vs = map (fn n => Variable ("v"^(string_of_int n))) ns;
       in
-      val consts_con = map con cons';
-      val consts_dis = map dis cons';
-      val consts_mat = map mat cons';
-      val consts_pat = map pat cons';
-      val consts_sel = maps sel cons';
-      end;
-
-      (* ----- constants concerning induction ------------------------------------- *)
-
-      val const_take   = (dbind "_take"  , HOLogic.natT-->dtype->>dtype, NoSyn);
-      val const_finite = (dbind "_finite", dtype-->HOLogic.boolT       , NoSyn);
-
-      (* ----- case translation --------------------------------------------------- *)
-
-      local open Syntax in
-      local
-        fun c_ast con mx = Constant (Syntax.const_name mx (Binding.name_of con));
-        fun expvar n     = Variable ("e"^(string_of_int n));
-        fun argvar n m _ = Variable ("a"^(string_of_int n)^"_"^
-                                     (string_of_int m));
-        fun argvars n args = mapn (argvar n) 1 args;
-        fun app s (l,r)  = mk_appl (Constant s) [l,r];
-        val cabs = app "_cabs";
-        val capp = app "Rep_CFun";
-        fun con1 n (con,args,mx) = Library.foldl capp (c_ast con mx, argvars n args);
-        fun case1 n (con,args,mx) = app "_case1" (con1 n (con,args,mx), expvar n);
-        fun arg1 n (con,args,_) = List.foldr cabs (expvar n) (argvars n args);
-        fun when1 n m = if n = m then arg1 n else K (Constant "UU");
+        [ParseRule (app_pat (Library.foldl capp (cname, xs)),
+                    mk_appl pname (map app_pat xs)),
+         ParseRule (app_var (Library.foldl capp (cname, xs)),
+                    app_var (args_list xs)),
+         PrintRule (Library.foldl capp (cname, ListPair.map (app "_match") (ps,vs)),
+                    app "_match" (mk_appl pname ps, args_list vs))]
+        end;
+    val Case_trans = maps one_case_trans cons';
+    end;
+    end;
+    val optional_consts =
+        if definitional then [] else [const_rep, const_abs, const_copy];
 
-        fun app_var x = mk_appl (Constant "_variable") [x, Variable "rhs"];
-        fun app_pat x = mk_appl (Constant "_pat") [x];
-        fun args_list [] = Constant "_noargs"
-          |   args_list xs = foldr1 (app "_args") xs;
-      in
-      val case_trans =
-          ParsePrintRule
-            (app "_case_syntax" (Variable "x", foldr1 (app "_case2") (mapn case1 1 cons')),
-             capp (Library.foldl capp (Constant (dnam^"_when"), mapn arg1 1 cons'), Variable "x"));
-
-      fun one_abscon_trans n (con,mx,args) =
-          ParsePrintRule
-            (cabs (con1 n (con,mx,args), expvar n),
-             Library.foldl capp (Constant (dnam^"_when"), mapn (when1 n) 1 cons'));
-      val abscon_trans = mapn one_abscon_trans 1 cons';
-          
-      fun one_case_trans (con,args,mx) =
-          let
-            val cname = c_ast con mx;
-            val pname = Constant (strip_esc (Binding.name_of con) ^ "_pat");
-            val ns = 1 upto length args;
-            val xs = map (fn n => Variable ("x"^(string_of_int n))) ns;
-            val ps = map (fn n => Variable ("p"^(string_of_int n))) ns;
-            val vs = map (fn n => Variable ("v"^(string_of_int n))) ns;
-          in
-            [ParseRule (app_pat (Library.foldl capp (cname, xs)),
-                        mk_appl pname (map app_pat xs)),
-             ParseRule (app_var (Library.foldl capp (cname, xs)),
-                        app_var (args_list xs)),
-             PrintRule (Library.foldl capp (cname, ListPair.map (app "_match") (ps,vs)),
-                        app "_match" (mk_appl pname ps, args_list vs))]
-          end;
-      val Case_trans = maps one_case_trans cons';
-      end;
-      end;
-
-    in ([const_rep, const_abs, const_when, const_copy] @ 
-        consts_con @ consts_dis @ consts_mat @ consts_pat @ consts_sel @
-        [const_take, const_finite],
-        (case_trans::(abscon_trans @ Case_trans)))
-    end; (* let *)
+  in (optional_consts @ [const_when] @ 
+      consts_con @ consts_dis @ consts_mat @ consts_pat @ consts_sel @
+      [const_take, const_finite],
+      (case_trans::(abscon_trans @ Case_trans)))
+  end; (* let *)
 
 (* ----- putting all the syntax stuff together ------------------------------ *)
 
 fun add_syntax
-      (comp_dnam : string)
-      (eqs' : ((string * typ list) *
-               (binding * (bool * binding option * typ) list * mixfix) list) list)
-      (thy'' : theory) =
-    let
-      val dtypes  = map (Type o fst) eqs';
-      val boolT   = HOLogic.boolT;
-      val funprod = foldr1 HOLogic.mk_prodT (map (fn tp => tp ->> tp          ) dtypes);
-      val relprod = foldr1 HOLogic.mk_prodT (map (fn tp => tp --> tp --> boolT) dtypes);
-      val const_copy = (Binding.name (comp_dnam^"_copy"), funprod ->> funprod, NoSyn);
-      val const_bisim = (Binding.name (comp_dnam^"_bisim"), relprod --> boolT, NoSyn);
-      val ctt : ((binding * typ * mixfix) list * ast Syntax.trrule list) list = map (calc_syntax funprod) eqs';
-    in thy'' |> ContConsts.add_consts_i (maps fst ctt @ 
-                                         (if length eqs'>1 then [const_copy] else[])@
-                                         [const_bisim])
-             |> Sign.add_trrules_i (maps snd ctt)
-    end; (* let *)
+    (definitional : bool)
+    (comp_dnam : string)
+    (eqs' : ((string * typ list) *
+             (binding * (bool * binding option * typ) list * mixfix) list) list)
+    (thy'' : theory) =
+  let
+    val dtypes  = map (Type o fst) eqs';
+    val boolT   = HOLogic.boolT;
+    val funprod =
+        foldr1 HOLogic.mk_prodT (map (fn tp => tp ->> tp          ) dtypes);
+    val relprod =
+        foldr1 HOLogic.mk_prodT (map (fn tp => tp --> tp --> boolT) dtypes);
+    val const_copy =
+        (Binding.name (comp_dnam^"_copy"), funprod ->> funprod, NoSyn);
+    val const_bisim =
+        (Binding.name (comp_dnam^"_bisim"), relprod --> boolT, NoSyn);
+    val ctt : ((binding * typ * mixfix) list * ast Syntax.trrule list) list =
+        map (calc_syntax definitional funprod) eqs';
+  in thy''
+       |> ContConsts.add_consts_i
+           (maps fst ctt @ 
+            (if length eqs'>1 then [const_copy] else[])@
+            [const_bisim])
+       |> Sign.add_trrules_i (maps snd ctt)
+  end; (* let *)
 
 end; (* struct *)
--- a/src/HOLCF/Tools/Domain/domain_theorems.ML	Fri Nov 20 00:54:20 2009 +0100
+++ b/src/HOLCF/Tools/Domain/domain_theorems.ML	Thu Nov 19 20:09:56 2009 -0800
@@ -141,6 +141,8 @@
 
 val _ = message ("Proving isomorphism properties of domain "^dname^" ...");
 val pg = pg' thy;
+val map_tab = Domain_Isomorphism.get_map_tab thy;
+
 
 (* ----- getting the axioms and definitions --------------------------------- *)
 
@@ -599,7 +601,8 @@
       val lhs = dc_copy`%"f"`(con_app con args);
       fun one_rhs arg =
           if DatatypeAux.is_rec_type (dtyp_of arg)
-          then Domain_Axioms.copy_of_dtyp (proj (%:"f") eqs) (dtyp_of arg) ` (%# arg)
+          then Domain_Axioms.copy_of_dtyp map_tab
+                 (proj (%:"f") eqs) (dtyp_of arg) ` (%# arg)
           else (%# arg);
       val rhs = con_app2 con one_rhs args;
       val goal = lift_defined %: (nonlazy_rec args, mk_trp (lhs === rhs));
@@ -660,6 +663,7 @@
 fun comp_theorems (comp_dnam, eqs: eq list) thy =
 let
 val global_ctxt = ProofContext.init thy;
+val map_tab = Domain_Isomorphism.get_map_tab thy;
 
 val dnames = map (fst o fst) eqs;
 val conss  = map  snd        eqs;
@@ -727,7 +731,8 @@
           fun mk_take n = dc_take (List.nth (dnames, n)) $ %:"n";
           fun one_rhs arg =
               if DatatypeAux.is_rec_type (dtyp_of arg)
-              then Domain_Axioms.copy_of_dtyp mk_take (dtyp_of arg) ` (%# arg)
+              then Domain_Axioms.copy_of_dtyp map_tab
+                     mk_take (dtyp_of arg) ` (%# arg)
               else (%# arg);
           val lhs = (dc_take dn $ (%%:"Suc" $ %:"n"))`(con_app con args);
           val rhs = con_app2 con one_rhs args;
--- a/src/HOLCF/ex/Domain_Proofs.thy	Fri Nov 20 00:54:20 2009 +0100
+++ b/src/HOLCF/ex/Domain_Proofs.thy	Thu Nov 19 20:09:56 2009 -0800
@@ -16,8 +16,8 @@
 datatypes:
 
 domain 'a foo = Foo1 | Foo2 (lazy 'a) (lazy "'a bar")
-   and 'a bar = Bar (lazy 'a) (lazy "'a baz")
-   and 'a baz = Baz (lazy 'a) (lazy "'a foo convex_pd")
+   and 'a bar = Bar (lazy "'a baz \<rightarrow> tr")
+   and 'a baz = Baz (lazy "'a foo convex_pd \<rightarrow> tr")
 
 *)
 
@@ -28,47 +28,47 @@
 text {* Start with the one-step non-recursive version *}
 
 definition
-  foo_bar_baz_typF ::
+  foo_bar_baz_deflF ::
     "TypeRep \<rightarrow> TypeRep \<times> TypeRep \<times> TypeRep \<rightarrow> TypeRep \<times> TypeRep \<times> TypeRep"
 where
-  "foo_bar_baz_typF = (\<Lambda> a (t1, t2, t3). 
-    ( ssum_typ\<cdot>one_typ\<cdot>(sprod_typ\<cdot>(u_typ\<cdot>a)\<cdot>(u_typ\<cdot>t2))
-    , sprod_typ\<cdot>(u_typ\<cdot>a)\<cdot>(u_typ\<cdot>t3)
-    , sprod_typ\<cdot>(u_typ\<cdot>a)\<cdot>(u_typ\<cdot>(convex_typ\<cdot>t1))))"
+  "foo_bar_baz_deflF = (\<Lambda> a. Abs_CFun (\<lambda>(t1, t2, t3). 
+    ( ssum_defl\<cdot>REP(one)\<cdot>(sprod_defl\<cdot>(u_defl\<cdot>a)\<cdot>(u_defl\<cdot>t2))
+    , u_defl\<cdot>(cfun_defl\<cdot>t3\<cdot>REP(tr))
+    , u_defl\<cdot>(cfun_defl\<cdot>(convex_defl\<cdot>t1)\<cdot>REP(tr)))))"
 
-lemma foo_bar_baz_typF_beta:
-  "foo_bar_baz_typF\<cdot>a\<cdot>t =
-    ( ssum_typ\<cdot>one_typ\<cdot>(sprod_typ\<cdot>(u_typ\<cdot>a)\<cdot>(u_typ\<cdot>(fst (snd t))))
-    , sprod_typ\<cdot>(u_typ\<cdot>a)\<cdot>(u_typ\<cdot>(snd (snd t)))
-    , sprod_typ\<cdot>(u_typ\<cdot>a)\<cdot>(u_typ\<cdot>(convex_typ\<cdot>(fst t))))"
-unfolding foo_bar_baz_typF_def
-by (simp add: csplit_def cfst_def csnd_def)
+lemma foo_bar_baz_deflF_beta:
+  "foo_bar_baz_deflF\<cdot>a\<cdot>t =
+    ( ssum_defl\<cdot>REP(one)\<cdot>(sprod_defl\<cdot>(u_defl\<cdot>a)\<cdot>(u_defl\<cdot>(fst (snd t))))
+    , u_defl\<cdot>(cfun_defl\<cdot>(snd (snd t))\<cdot>REP(tr))
+    , u_defl\<cdot>(cfun_defl\<cdot>(convex_defl\<cdot>(fst t))\<cdot>REP(tr)))"
+unfolding foo_bar_baz_deflF_def
+by (simp add: split_def)
 
 text {* Individual type combinators are projected from the fixed point. *}
 
-definition foo_typ :: "TypeRep \<rightarrow> TypeRep"
-where "foo_typ = (\<Lambda> a. fst (fix\<cdot>(foo_bar_baz_typF\<cdot>a)))"
+definition foo_defl :: "TypeRep \<rightarrow> TypeRep"
+where "foo_defl = (\<Lambda> a. fst (fix\<cdot>(foo_bar_baz_deflF\<cdot>a)))"
 
-definition bar_typ :: "TypeRep \<rightarrow> TypeRep"
-where "bar_typ = (\<Lambda> a. fst (snd (fix\<cdot>(foo_bar_baz_typF\<cdot>a))))"
+definition bar_defl :: "TypeRep \<rightarrow> TypeRep"
+where "bar_defl = (\<Lambda> a. fst (snd (fix\<cdot>(foo_bar_baz_deflF\<cdot>a))))"
 
-definition baz_typ :: "TypeRep \<rightarrow> TypeRep"
-where "baz_typ = (\<Lambda> a. snd (snd (fix\<cdot>(foo_bar_baz_typF\<cdot>a))))"
+definition baz_defl :: "TypeRep \<rightarrow> TypeRep"
+where "baz_defl = (\<Lambda> a. snd (snd (fix\<cdot>(foo_bar_baz_deflF\<cdot>a))))"
 
 text {* Unfold rules for each combinator. *}
 
-lemma foo_typ_unfold:
-  "foo_typ\<cdot>a = ssum_typ\<cdot>one_typ\<cdot>(sprod_typ\<cdot>(u_typ\<cdot>a)\<cdot>(u_typ\<cdot>(bar_typ\<cdot>a)))"
-unfolding foo_typ_def bar_typ_def baz_typ_def
-by (subst fix_eq, simp add: foo_bar_baz_typF_beta)
+lemma foo_defl_unfold:
+  "foo_defl\<cdot>a = ssum_defl\<cdot>REP(one)\<cdot>(sprod_defl\<cdot>(u_defl\<cdot>a)\<cdot>(u_defl\<cdot>(bar_defl\<cdot>a)))"
+unfolding foo_defl_def bar_defl_def baz_defl_def
+by (subst fix_eq, simp add: foo_bar_baz_deflF_beta)
 
-lemma bar_typ_unfold: "bar_typ\<cdot>a = sprod_typ\<cdot>(u_typ\<cdot>a)\<cdot>(u_typ\<cdot>(baz_typ\<cdot>a))"
-unfolding foo_typ_def bar_typ_def baz_typ_def
-by (subst fix_eq, simp add: foo_bar_baz_typF_beta)
+lemma bar_defl_unfold: "bar_defl\<cdot>a = u_defl\<cdot>(cfun_defl\<cdot>(baz_defl\<cdot>a)\<cdot>REP(tr))"
+unfolding foo_defl_def bar_defl_def baz_defl_def
+by (subst fix_eq, simp add: foo_bar_baz_deflF_beta)
 
-lemma baz_typ_unfold: "baz_typ\<cdot>a = sprod_typ\<cdot>(u_typ\<cdot>a)\<cdot>(u_typ\<cdot>(convex_typ\<cdot>(foo_typ\<cdot>a)))"
-unfolding foo_typ_def bar_typ_def baz_typ_def
-by (subst fix_eq, simp add: foo_bar_baz_typF_beta)
+lemma baz_defl_unfold: "baz_defl\<cdot>a = u_defl\<cdot>(cfun_defl\<cdot>(convex_defl\<cdot>(foo_defl\<cdot>a))\<cdot>REP(tr))"
+unfolding foo_defl_def bar_defl_def baz_defl_def
+by (subst fix_eq, simp add: foo_bar_baz_deflF_beta)
 
 text "The automation for the previous steps will be quite similar to
 how the fixrec package works."
@@ -79,13 +79,13 @@
 
 text {* Use @{text pcpodef} with the appropriate type combinator. *}
 
-pcpodef (open) 'a foo = "{x. x ::: foo_typ\<cdot>REP('a)}"
+pcpodef (open) 'a foo = "{x. x ::: foo_defl\<cdot>REP('a)}"
 by (simp_all add: adm_in_deflation)
 
-pcpodef (open) 'a bar = "{x. x ::: bar_typ\<cdot>REP('a)}"
+pcpodef (open) 'a bar = "{x. x ::: bar_defl\<cdot>REP('a)}"
 by (simp_all add: adm_in_deflation)
 
-pcpodef (open) 'a baz = "{x. x ::: baz_typ\<cdot>REP('a)}"
+pcpodef (open) 'a baz = "{x. x ::: baz_defl\<cdot>REP('a)}"
 by (simp_all add: adm_in_deflation)
 
 text {* Prove rep instance using lemma @{text typedef_rep_class}. *}
@@ -97,10 +97,10 @@
 where "emb_foo \<equiv> (\<Lambda> x. Rep_foo x)"
 
 definition prj_foo :: "udom \<rightarrow> 'a foo"
-where "prj_foo \<equiv> (\<Lambda> y. Abs_foo (cast\<cdot>(foo_typ\<cdot>REP('a))\<cdot>y))"
+where "prj_foo \<equiv> (\<Lambda> y. Abs_foo (cast\<cdot>(foo_defl\<cdot>REP('a))\<cdot>y))"
 
 definition approx_foo :: "nat \<Rightarrow> 'a foo \<rightarrow> 'a foo"
-where "approx_foo \<equiv> repdef_approx Rep_foo Abs_foo (foo_typ\<cdot>REP('a))"
+where "approx_foo \<equiv> repdef_approx Rep_foo Abs_foo (foo_defl\<cdot>REP('a))"
 
 instance
 apply (rule typedef_rep_class)
@@ -120,10 +120,10 @@
 where "emb_bar \<equiv> (\<Lambda> x. Rep_bar x)"
 
 definition prj_bar :: "udom \<rightarrow> 'a bar"
-where "prj_bar \<equiv> (\<Lambda> y. Abs_bar (cast\<cdot>(bar_typ\<cdot>REP('a))\<cdot>y))"
+where "prj_bar \<equiv> (\<Lambda> y. Abs_bar (cast\<cdot>(bar_defl\<cdot>REP('a))\<cdot>y))"
 
 definition approx_bar :: "nat \<Rightarrow> 'a bar \<rightarrow> 'a bar"
-where "approx_bar \<equiv> repdef_approx Rep_bar Abs_bar (bar_typ\<cdot>REP('a))"
+where "approx_bar \<equiv> repdef_approx Rep_bar Abs_bar (bar_defl\<cdot>REP('a))"
 
 instance
 apply (rule typedef_rep_class)
@@ -143,10 +143,10 @@
 where "emb_baz \<equiv> (\<Lambda> x. Rep_baz x)"
 
 definition prj_baz :: "udom \<rightarrow> 'a baz"
-where "prj_baz \<equiv> (\<Lambda> y. Abs_baz (cast\<cdot>(baz_typ\<cdot>REP('a))\<cdot>y))"
+where "prj_baz \<equiv> (\<Lambda> y. Abs_baz (cast\<cdot>(baz_defl\<cdot>REP('a))\<cdot>y))"
 
 definition approx_baz :: "nat \<Rightarrow> 'a baz \<rightarrow> 'a baz"
-where "approx_baz \<equiv> repdef_approx Rep_baz Abs_baz (baz_typ\<cdot>REP('a))"
+where "approx_baz \<equiv> repdef_approx Rep_baz Abs_baz (baz_defl\<cdot>REP('a))"
 
 instance
 apply (rule typedef_rep_class)
@@ -161,7 +161,7 @@
 
 text {* Prove REP rules using lemma @{text typedef_REP}. *}
 
-lemma REP_foo: "REP('a foo) = foo_typ\<cdot>REP('a)"
+lemma REP_foo: "REP('a foo) = foo_defl\<cdot>REP('a)"
 apply (rule typedef_REP)
 apply (rule type_definition_foo)
 apply (rule below_foo_def)
@@ -169,7 +169,7 @@
 apply (rule prj_foo_def)
 done
 
-lemma REP_bar: "REP('a bar) = bar_typ\<cdot>REP('a)"
+lemma REP_bar: "REP('a bar) = bar_defl\<cdot>REP('a)"
 apply (rule typedef_REP)
 apply (rule type_definition_bar)
 apply (rule below_bar_def)
@@ -177,7 +177,7 @@
 apply (rule prj_bar_def)
 done
 
-lemma REP_baz: "REP('a baz) = baz_typ\<cdot>REP('a)"
+lemma REP_baz: "REP('a baz) = baz_defl\<cdot>REP('a)"
 apply (rule typedef_REP)
 apply (rule type_definition_baz)
 apply (rule below_baz_def)
@@ -189,15 +189,15 @@
 
 lemma REP_foo': "REP('a foo) = REP(one \<oplus> 'a\<^sub>\<bottom> \<otimes> ('a bar)\<^sub>\<bottom>)"
 unfolding REP_foo REP_bar REP_baz REP_simps
-by (rule foo_typ_unfold)
+by (rule foo_defl_unfold)
 
-lemma REP_bar': "REP('a bar) = REP('a\<^sub>\<bottom> \<otimes> ('a baz)\<^sub>\<bottom>)"
+lemma REP_bar': "REP('a bar) = REP(('a baz \<rightarrow> tr)\<^sub>\<bottom>)"
 unfolding REP_foo REP_bar REP_baz REP_simps
-by (rule bar_typ_unfold)
+by (rule bar_defl_unfold)
 
-lemma REP_baz': "REP('a baz) = REP('a\<^sub>\<bottom> \<otimes> ('a foo convex_pd)\<^sub>\<bottom>)"
+lemma REP_baz': "REP('a baz) = REP(('a foo convex_pd \<rightarrow> tr)\<^sub>\<bottom>)"
 unfolding REP_foo REP_bar REP_baz REP_simps
-by (rule baz_typ_unfold)
+by (rule baz_defl_unfold)
 
 (********************************************************************)
 
@@ -206,41 +206,56 @@
 text {* Define them all using @{text coerce}! *}
 
 definition foo_rep :: "'a foo \<rightarrow> one \<oplus> ('a\<^sub>\<bottom> \<otimes> ('a bar)\<^sub>\<bottom>)"
-where "foo_rep = coerce"
+where "foo_rep \<equiv> coerce"
 
 definition foo_abs :: "one \<oplus> ('a\<^sub>\<bottom> \<otimes> ('a bar)\<^sub>\<bottom>) \<rightarrow> 'a foo"
-where "foo_abs = coerce"
+where "foo_abs \<equiv> coerce"
+
+definition bar_rep :: "'a bar \<rightarrow> ('a baz \<rightarrow> tr)\<^sub>\<bottom>"
+where "bar_rep \<equiv> coerce"
+
+definition bar_abs :: "('a baz \<rightarrow> tr)\<^sub>\<bottom> \<rightarrow> 'a bar"
+where "bar_abs \<equiv> coerce"
 
-definition bar_rep :: "'a bar \<rightarrow> 'a\<^sub>\<bottom> \<otimes> ('a baz)\<^sub>\<bottom>"
-where "bar_rep = coerce"
+definition baz_rep :: "'a baz \<rightarrow> ('a foo convex_pd \<rightarrow> tr)\<^sub>\<bottom>"
+where "baz_rep \<equiv> coerce"
+
+definition baz_abs :: "('a foo convex_pd \<rightarrow> tr)\<^sub>\<bottom> \<rightarrow> 'a baz"
+where "baz_abs \<equiv> coerce"
+
+text {* Prove isomorphism rules. *}
 
-definition bar_abs :: "'a\<^sub>\<bottom> \<otimes> ('a baz)\<^sub>\<bottom> \<rightarrow> 'a bar"
-where "bar_abs = coerce"
+lemma foo_abs_iso: "foo_rep\<cdot>(foo_abs\<cdot>x) = x"
+by (rule domain_abs_iso [OF REP_foo' foo_abs_def foo_rep_def])
+
+lemma foo_rep_iso: "foo_abs\<cdot>(foo_rep\<cdot>x) = x"
+by (rule domain_rep_iso [OF REP_foo' foo_abs_def foo_rep_def])
+
+lemma bar_abs_iso: "bar_rep\<cdot>(bar_abs\<cdot>x) = x"
+by (rule domain_abs_iso [OF REP_bar' bar_abs_def bar_rep_def])
 
-definition baz_rep :: "'a baz \<rightarrow> 'a\<^sub>\<bottom> \<otimes> ('a foo convex_pd)\<^sub>\<bottom>"
-where "baz_rep = coerce"
+lemma bar_rep_iso: "bar_abs\<cdot>(bar_rep\<cdot>x) = x"
+by (rule domain_rep_iso [OF REP_bar' bar_abs_def bar_rep_def])
 
-definition baz_abs :: "'a\<^sub>\<bottom> \<otimes> ('a foo convex_pd)\<^sub>\<bottom> \<rightarrow> 'a baz"
-where "baz_abs = coerce"
+lemma baz_abs_iso: "baz_rep\<cdot>(baz_abs\<cdot>x) = x"
+by (rule domain_abs_iso [OF REP_baz' baz_abs_def baz_rep_def])
+
+lemma baz_rep_iso: "baz_abs\<cdot>(baz_rep\<cdot>x) = x"
+by (rule domain_rep_iso [OF REP_baz' baz_abs_def baz_rep_def])
 
 text {* Prove isodefl rules using @{text isodefl_coerce}. *}
 
 lemma isodefl_foo_abs:
   "isodefl d t \<Longrightarrow> isodefl (foo_abs oo d oo foo_rep) t"
-unfolding foo_abs_def foo_rep_def
-by (rule isodefl_coerce [OF REP_foo'])
+by (rule isodefl_abs_rep [OF REP_foo' foo_abs_def foo_rep_def])
 
 lemma isodefl_bar_abs:
   "isodefl d t \<Longrightarrow> isodefl (bar_abs oo d oo bar_rep) t"
-unfolding bar_abs_def bar_rep_def
-by (rule isodefl_coerce [OF REP_bar'])
+by (rule isodefl_abs_rep [OF REP_bar' bar_abs_def bar_rep_def])
 
 lemma isodefl_baz_abs:
   "isodefl d t \<Longrightarrow> isodefl (baz_abs oo d oo baz_rep) t"
-unfolding baz_abs_def baz_rep_def
-by (rule isodefl_coerce [OF REP_baz'])
-
-text {* TODO: prove iso predicate for rep and abs. *}
+by (rule isodefl_abs_rep [OF REP_baz' baz_abs_def baz_rep_def])
 
 (********************************************************************)
 
@@ -253,20 +268,20 @@
 
 definition
   foo_bar_baz_mapF ::
-  "('a \<rightarrow> 'b)
-     \<rightarrow> ('a foo \<rightarrow> 'b foo) \<times> ('a bar \<rightarrow> 'b bar) \<times> ('a baz \<rightarrow> 'b baz)
-     \<rightarrow> ('a foo \<rightarrow> 'b foo) \<times> ('a bar \<rightarrow> 'b bar) \<times> ('a baz \<rightarrow> 'b baz)"
+    "('a \<rightarrow> 'b) \<rightarrow>
+     ('a foo \<rightarrow> 'b foo) \<times> ('a bar \<rightarrow> 'b bar) \<times> ('b baz \<rightarrow> 'a baz) \<rightarrow>
+     ('a foo \<rightarrow> 'b foo) \<times> ('a bar \<rightarrow> 'b bar) \<times> ('b baz \<rightarrow> 'a baz)"
 where
-  "foo_bar_baz_mapF = (\<Lambda> f (d1, d2, d3).
+  "foo_bar_baz_mapF = (\<Lambda> f. Abs_CFun (\<lambda>(d1, d2, d3).
     (
       foo_abs oo
         ssum_map\<cdot>ID\<cdot>(sprod_map\<cdot>(u_map\<cdot>f)\<cdot>(u_map\<cdot>d2))
           oo foo_rep
     ,
-      bar_abs oo sprod_map\<cdot>(u_map\<cdot>f)\<cdot>(u_map\<cdot>d3) oo bar_rep
+      bar_abs oo u_map\<cdot>(cfun_map\<cdot>d3\<cdot>ID) oo bar_rep
     ,
-      baz_abs oo sprod_map\<cdot>(u_map\<cdot>f)\<cdot>(u_map\<cdot>(convex_map\<cdot>d1)) oo baz_rep
-    ))"
+      baz_abs oo u_map\<cdot>(cfun_map\<cdot>(convex_map\<cdot>d1)\<cdot>ID) oo baz_rep
+    )))"
 
 lemma foo_bar_baz_mapF_beta:
   "foo_bar_baz_mapF\<cdot>f\<cdot>d =
@@ -275,12 +290,12 @@
         ssum_map\<cdot>ID\<cdot>(sprod_map\<cdot>(u_map\<cdot>f)\<cdot>(u_map\<cdot>(fst (snd d))))
           oo foo_rep
     ,
-      bar_abs oo sprod_map\<cdot>(u_map\<cdot>f)\<cdot>(u_map\<cdot>(snd (snd d))) oo bar_rep
+      bar_abs oo u_map\<cdot>(cfun_map\<cdot>(snd (snd d))\<cdot>ID) oo bar_rep
     ,
-      baz_abs oo sprod_map\<cdot>(u_map\<cdot>f)\<cdot>(u_map\<cdot>(convex_map\<cdot>(fst d))) oo baz_rep
+      baz_abs oo u_map\<cdot>(cfun_map\<cdot>(convex_map\<cdot>(fst d))\<cdot>ID) oo baz_rep
     )"
 unfolding foo_bar_baz_mapF_def
-by (simp add: csplit_def cfst_def csnd_def)
+by (simp add: split_def)
 
 text {* Individual map functions are projected from the fixed point. *}
 
@@ -290,7 +305,7 @@
 definition bar_map :: "('a \<rightarrow> 'b) \<rightarrow> ('a bar \<rightarrow> 'b bar)"
 where "bar_map = (\<Lambda> f. fst (snd (fix\<cdot>(foo_bar_baz_mapF\<cdot>f))))"
 
-definition baz_map :: "('a \<rightarrow> 'b) \<rightarrow> ('a baz \<rightarrow> 'b baz)"
+definition baz_map :: "('a \<rightarrow> 'b) \<rightarrow> ('b baz \<rightarrow> 'a baz)"
 where "baz_map = (\<Lambda> f. snd (snd (fix\<cdot>(foo_bar_baz_mapF\<cdot>f))))"
 
 text {* Prove isodefl rules for all map functions simultaneously. *}
@@ -298,17 +313,16 @@
 lemma isodefl_foo_bar_baz:
   assumes isodefl_d: "isodefl d t"
   shows
-  "isodefl (foo_map\<cdot>d) (foo_typ\<cdot>t) \<and>
-  isodefl (bar_map\<cdot>d) (bar_typ\<cdot>t) \<and>
-  isodefl (baz_map\<cdot>d) (baz_typ\<cdot>t)"
+  "isodefl (foo_map\<cdot>d) (foo_defl\<cdot>t) \<and>
+  isodefl (bar_map\<cdot>d) (bar_defl\<cdot>t) \<and>
+  isodefl (baz_map\<cdot>d) (baz_defl\<cdot>t)"
  apply (simp add: foo_map_def bar_map_def baz_map_def)
- apply (simp add: foo_typ_def bar_typ_def baz_typ_def)
- apply (rule parallel_fix_ind
-  [where F="foo_bar_baz_typF\<cdot>t" and G="foo_bar_baz_mapF\<cdot>d"])
+ apply (simp add: foo_defl_def bar_defl_def baz_defl_def)
+ apply (rule parallel_fix_ind)
    apply (intro adm_conj adm_isodefl cont2cont_fst cont2cont_snd cont_id)
   apply (simp only: fst_strict snd_strict isodefl_bottom simp_thms)
  apply (simp only: foo_bar_baz_mapF_beta
-                   foo_bar_baz_typF_beta
+                   foo_bar_baz_deflF_beta
                    fst_conv snd_conv)
  apply (elim conjE)
  apply (intro
@@ -316,7 +330,8 @@
   isodefl_foo_abs
   isodefl_bar_abs
   isodefl_baz_abs
-  isodefl_ssum isodefl_sprod isodefl_one isodefl_u isodefl_convex
+  isodefl_ssum isodefl_sprod isodefl_ID_REP
+  isodefl_u isodefl_convex isodefl_cfun
   isodefl_d
  )
  apply assumption+
@@ -353,23 +368,63 @@
 
 subsection {* Step 5: Define copy functions, prove reach lemmas *}
 
-definition "foo_bar_baz_copy = foo_bar_baz_mapF\<cdot>ID"
-definition "foo_copy = (\<Lambda> f. fst (foo_bar_baz_copy\<cdot>f))"
-definition "bar_copy = (\<Lambda> f. fst (snd (foo_bar_baz_copy\<cdot>f)))"
-definition "baz_copy = (\<Lambda> f. snd (snd (foo_bar_baz_copy\<cdot>f)))"
+text {* Define copy functions just like the old domain package does. *}
+
+definition
+  foo_copy ::
+    "('a foo \<rightarrow> 'a foo) \<times> ('a bar \<rightarrow> 'a bar) \<times> ('a baz \<rightarrow> 'a baz) \<rightarrow>
+       'a foo \<rightarrow> 'a foo"
+where
+  "foo_copy = (\<Lambda> p. foo_abs oo
+        ssum_map\<cdot>ID\<cdot>(sprod_map\<cdot>(u_map\<cdot>ID)\<cdot>(u_map\<cdot>(fst (snd p))))
+          oo foo_rep)"
+
+definition
+  bar_copy ::
+    "('a foo \<rightarrow> 'a foo) \<times> ('a bar \<rightarrow> 'a bar) \<times> ('a baz \<rightarrow> 'a baz) \<rightarrow>
+       'a bar \<rightarrow> 'a bar"
+where
+  "bar_copy = (\<Lambda> p. bar_abs oo
+        u_map\<cdot>(cfun_map\<cdot>(snd (snd p))\<cdot>ID) oo bar_rep)"
+
+definition
+  baz_copy ::
+    "('a foo \<rightarrow> 'a foo) \<times> ('a bar \<rightarrow> 'a bar) \<times> ('a baz \<rightarrow> 'a baz) \<rightarrow>
+       'a baz \<rightarrow> 'a baz"
+where
+  "baz_copy = (\<Lambda> p. baz_abs oo
+        u_map\<cdot>(cfun_map\<cdot>(convex_map\<cdot>(fst p))\<cdot>ID) oo baz_rep)"
+
+definition
+  foo_bar_baz_copy ::
+    "('a foo \<rightarrow> 'a foo) \<times> ('a bar \<rightarrow> 'a bar) \<times> ('a baz \<rightarrow> 'a baz) \<rightarrow>
+     ('a foo \<rightarrow> 'a foo) \<times> ('a bar \<rightarrow> 'a bar) \<times> ('a baz \<rightarrow> 'a baz)"
+where
+  "foo_bar_baz_copy = (\<Lambda> f. (foo_copy\<cdot>f, bar_copy\<cdot>f, baz_copy\<cdot>f))"
 
 lemma fix_foo_bar_baz_copy:
   "fix\<cdot>foo_bar_baz_copy = (foo_map\<cdot>ID, bar_map\<cdot>ID, baz_map\<cdot>ID)"
-unfolding foo_bar_baz_copy_def foo_map_def bar_map_def baz_map_def
-by simp
+unfolding foo_map_def bar_map_def baz_map_def
+apply (subst beta_cfun, simp)+
+apply (subst pair_collapse)+
+apply (rule cfun_arg_cong)
+unfolding foo_bar_baz_mapF_def split_def
+unfolding foo_bar_baz_copy_def
+unfolding foo_copy_def bar_copy_def baz_copy_def
+apply (subst beta_cfun, simp)+
+apply (rule refl)
+done
 
 lemma foo_reach: "fst (fix\<cdot>foo_bar_baz_copy)\<cdot>x = x"
-unfolding fix_foo_bar_baz_copy by (simp add: foo_map_ID)
+unfolding fix_foo_bar_baz_copy fst_conv snd_conv
+unfolding foo_map_ID by (rule ID1)
 
 lemma bar_reach: "fst (snd (fix\<cdot>foo_bar_baz_copy))\<cdot>x = x"
-unfolding fix_foo_bar_baz_copy by (simp add: bar_map_ID)
+unfolding fix_foo_bar_baz_copy fst_conv snd_conv
+unfolding bar_map_ID by (rule ID1)
 
 lemma baz_reach: "snd (snd (fix\<cdot>foo_bar_baz_copy))\<cdot>x = x"
-unfolding fix_foo_bar_baz_copy by (simp add: baz_map_ID)
+unfolding fix_foo_bar_baz_copy fst_conv snd_conv
+unfolding baz_map_ID by (rule ID1)
 
 end