# HG changeset patch
# User huffman
# Date 1257864506 28800
# Node ID 27f74e853a54dc20db4a338ccdf32aec6c99a329
# Parent  51091e1041a7506ea3a3497113ac28f847970bc1# Parent  488837bf01d7eb605a4d100bd2611617d659515e
merged

diff -r 488837bf01d7 -r 27f74e853a54 src/HOLCF/Algebraic.thy
--- a/src/HOLCF/Algebraic.thy	Tue Nov 10 14:20:15 2009 +0100
+++ b/src/HOLCF/Algebraic.thy	Tue Nov 10 06:48:26 2009 -0800
@@ -478,6 +478,7 @@
 apply (rule fd_take_covers)
 done
 
+
 subsection {* Defining algebraic deflations by ideal completion *}
 
 typedef (open) 'a alg_defl =
@@ -612,6 +613,8 @@
 interpretation cast: deflation "cast\<cdot>d"
 by (rule deflation_cast)
 
+declare cast.idem [simp]
+
 lemma cast_approx: "cast\<cdot>(approx n\<cdot>A) = defl_approx n (cast\<cdot>A)"
 apply (rule alg_defl.principal_induct)
 apply (rule adm_eq)
@@ -647,6 +650,61 @@
 apply (simp add: below_fin_defl_def)
 done
 
+lemma cast_eq_imp_eq: "cast\<cdot>A = cast\<cdot>B \<Longrightarrow> A = B"
+by (simp add: below_antisym cast_below_imp_below)
+
+lemma cast_strict1 [simp]: "cast\<cdot>\<bottom> = \<bottom>"
+apply (subst inst_alg_defl_pcpo)
+apply (subst cast_alg_defl_principal)
+apply (rule Abs_fin_defl_inverse)
+apply (simp add: finite_deflation_UU)
+done
+
+lemma cast_strict2 [simp]: "cast\<cdot>A\<cdot>\<bottom> = \<bottom>"
+by (rule cast.below [THEN UU_I])
+
+
+subsection {* Deflation membership relation *}
+
+definition
+  in_deflation :: "'a::profinite \<Rightarrow> 'a alg_defl \<Rightarrow> bool" (infixl ":::" 50)
+where
+  "x ::: A \<longleftrightarrow> cast\<cdot>A\<cdot>x = x"
+
+lemma adm_in_deflation: "adm (\<lambda>x. x ::: A)"
+unfolding in_deflation_def by simp
+
+lemma in_deflationI: "cast\<cdot>A\<cdot>x = x \<Longrightarrow> x ::: A"
+unfolding in_deflation_def .
+
+lemma cast_fixed: "x ::: A \<Longrightarrow> cast\<cdot>A\<cdot>x = x"
+unfolding in_deflation_def .
+
+lemma cast_in_deflation [simp]: "cast\<cdot>A\<cdot>x ::: A"
+unfolding in_deflation_def by (rule cast.idem)
+
+lemma bottom_in_deflation [simp]: "\<bottom> ::: A"
+unfolding in_deflation_def by (rule cast_strict2)
+
+lemma subdeflationD: "A \<sqsubseteq> B \<Longrightarrow> x ::: A \<Longrightarrow> x ::: B"
+unfolding in_deflation_def
+ apply (rule deflation.belowD)
+   apply (rule deflation_cast)
+  apply (erule monofun_cfun_arg)
+ apply assumption
+done
+
+lemma rev_subdeflationD: "x ::: A \<Longrightarrow> A \<sqsubseteq> B \<Longrightarrow> x ::: B"
+by (rule subdeflationD)
+
+lemma subdeflationI: "(\<And>x. x ::: A \<Longrightarrow> x ::: B) \<Longrightarrow> A \<sqsubseteq> B"
+apply (rule cast_below_imp_below)
+apply (rule cast.belowI)
+apply (simp add: in_deflation_def)
+done
+
+text "Identity deflation:"
+
 lemma "cast\<cdot>(\<Squnion>i. alg_defl_principal (Abs_fin_defl (approx i)))\<cdot>x = x"
 apply (subst contlub_cfun_arg)
 apply (rule chainI)
@@ -659,6 +717,8 @@
 apply (simp add: cast_alg_defl_principal Abs_fin_defl_inverse finite_deflation_approx)
 done
 
+subsection {* Bifinite domains and algebraic deflations *}
+
 text {* This lemma says that if we have an ep-pair from
 a bifinite domain into a universal domain, then e oo p
 is an algebraic deflation. *}
diff -r 488837bf01d7 -r 27f74e853a54 src/HOLCF/Bifinite.thy
--- a/src/HOLCF/Bifinite.thy	Tue Nov 10 14:20:15 2009 +0100
+++ b/src/HOLCF/Bifinite.thy	Tue Nov 10 06:48:26 2009 -0800
@@ -114,6 +114,11 @@
 lemma cprod_map_Pair [simp]: "cprod_map\<cdot>f\<cdot>g\<cdot>(x, y) = (f\<cdot>x, g\<cdot>y)"
 unfolding cprod_map_def by simp
 
+lemma cprod_map_map:
+  "cprod_map\<cdot>f1\<cdot>g1\<cdot>(cprod_map\<cdot>f2\<cdot>g2\<cdot>p) =
+    cprod_map\<cdot>(\<Lambda> x. f1\<cdot>(f2\<cdot>x))\<cdot>(\<Lambda> x. g1\<cdot>(g2\<cdot>x))\<cdot>p"
+by (induct p) simp
+
 lemma ep_pair_cprod_map:
   assumes "ep_pair e1 p1" and "ep_pair e2 p2"
   shows "ep_pair (cprod_map\<cdot>e1\<cdot>e2) (cprod_map\<cdot>p1\<cdot>p2)"
@@ -202,6 +207,11 @@
 lemma cfun_map_beta [simp]: "cfun_map\<cdot>a\<cdot>b\<cdot>f\<cdot>x = b\<cdot>(f\<cdot>(a\<cdot>x))"
 unfolding cfun_map_def by simp
 
+lemma cfun_map_map:
+  "cfun_map\<cdot>f1\<cdot>g1\<cdot>(cfun_map\<cdot>f2\<cdot>g2\<cdot>p) =
+    cfun_map\<cdot>(\<Lambda> x. f2\<cdot>(f1\<cdot>x))\<cdot>(\<Lambda> x. g1\<cdot>(g2\<cdot>x))\<cdot>p"
+by (rule ext_cfun) simp
+
 lemma ep_pair_cfun_map:
   assumes "ep_pair e1 p1" and "ep_pair e2 p2"
   shows "ep_pair (cfun_map\<cdot>p1\<cdot>e2) (cfun_map\<cdot>e1\<cdot>p2)"
diff -r 488837bf01d7 -r 27f74e853a54 src/HOLCF/ConvexPD.thy
--- a/src/HOLCF/ConvexPD.thy	Tue Nov 10 14:20:15 2009 +0100
+++ b/src/HOLCF/ConvexPD.thy	Tue Nov 10 06:48:26 2009 -0800
@@ -515,6 +515,18 @@
 lemma convex_map_approx: "convex_map\<cdot>(approx n)\<cdot>xs = approx n\<cdot>xs"
 by (induct xs rule: convex_pd_induct, simp_all)
 
+lemma ep_pair_convex_map: "ep_pair e p \<Longrightarrow> ep_pair (convex_map\<cdot>e) (convex_map\<cdot>p)"
+apply default
+apply (induct_tac x rule: convex_pd_induct, simp_all add: ep_pair.e_inverse)
+apply (induct_tac y rule: convex_pd_induct, simp_all add: ep_pair.e_p_below monofun_cfun)
+done
+
+lemma deflation_convex_map: "deflation d \<Longrightarrow> deflation (convex_map\<cdot>d)"
+apply default
+apply (induct_tac x rule: convex_pd_induct, simp_all add: deflation.idem)
+apply (induct_tac x rule: convex_pd_induct, simp_all add: deflation.below monofun_cfun)
+done
+
 
 subsection {* Conversions to other powerdomains *}
 
diff -r 488837bf01d7 -r 27f74e853a54 src/HOLCF/Fix.thy
--- a/src/HOLCF/Fix.thy	Tue Nov 10 14:20:15 2009 +0100
+++ b/src/HOLCF/Fix.thy	Tue Nov 10 06:48:26 2009 -0800
@@ -179,6 +179,28 @@
 apply (simp add: step)
 done
 
+lemma parallel_fix_ind:
+  assumes adm: "adm (\<lambda>x. P (fst x) (snd x))"
+  assumes base: "P \<bottom> \<bottom>"
+  assumes step: "\<And>x y. P x y \<Longrightarrow> P (F\<cdot>x) (G\<cdot>y)"
+  shows "P (fix\<cdot>F) (fix\<cdot>G)"
+proof -
+  from adm have adm': "adm (split P)"
+    unfolding split_def .
+  have "\<And>i. P (iterate i\<cdot>F\<cdot>\<bottom>) (iterate i\<cdot>G\<cdot>\<bottom>)"
+    by (induct_tac i, simp add: base, simp add: step)
+  hence "\<And>i. split P (iterate i\<cdot>F\<cdot>\<bottom>, iterate i\<cdot>G\<cdot>\<bottom>)"
+    by simp
+  hence "split P (\<Squnion>i. (iterate i\<cdot>F\<cdot>\<bottom>, iterate i\<cdot>G\<cdot>\<bottom>))"
+    by - (rule admD [OF adm'], simp, assumption)
+  hence "split P (\<Squnion>i. iterate i\<cdot>F\<cdot>\<bottom>, \<Squnion>i. iterate i\<cdot>G\<cdot>\<bottom>)"
+    by (simp add: thelub_Pair)
+  hence "P (\<Squnion>i. iterate i\<cdot>F\<cdot>\<bottom>) (\<Squnion>i. iterate i\<cdot>G\<cdot>\<bottom>)"
+    by simp
+  thus "P (fix\<cdot>F) (fix\<cdot>G)"
+    by (simp add: fix_def2)
+qed
+
 subsection {* Recursive let bindings *}
 
 definition
diff -r 488837bf01d7 -r 27f74e853a54 src/HOLCF/HOLCF.thy
--- a/src/HOLCF/HOLCF.thy	Tue Nov 10 14:20:15 2009 +0100
+++ b/src/HOLCF/HOLCF.thy	Tue Nov 10 06:48:26 2009 -0800
@@ -7,6 +7,7 @@
 theory HOLCF
 imports
   Domain ConvexPD Algebraic Universal Sum_Cpo Main
+  Representable
 uses
   "holcf_logic.ML"
   "Tools/adm_tac.ML"
diff -r 488837bf01d7 -r 27f74e853a54 src/HOLCF/LowerPD.thy
--- a/src/HOLCF/LowerPD.thy	Tue Nov 10 14:20:15 2009 +0100
+++ b/src/HOLCF/LowerPD.thy	Tue Nov 10 06:48:26 2009 -0800
@@ -491,4 +491,16 @@
 lemma lower_map_approx: "lower_map\<cdot>(approx n)\<cdot>xs = approx n\<cdot>xs"
 by (induct xs rule: lower_pd_induct, simp_all)
 
+lemma ep_pair_lower_map: "ep_pair e p \<Longrightarrow> ep_pair (lower_map\<cdot>e) (lower_map\<cdot>p)"
+apply default
+apply (induct_tac x rule: lower_pd_induct, simp_all add: ep_pair.e_inverse)
+apply (induct_tac y rule: lower_pd_induct, simp_all add: ep_pair.e_p_below monofun_cfun)
+done
+
+lemma deflation_lower_map: "deflation d \<Longrightarrow> deflation (lower_map\<cdot>d)"
+apply default
+apply (induct_tac x rule: lower_pd_induct, simp_all add: deflation.idem)
+apply (induct_tac x rule: lower_pd_induct, simp_all add: deflation.below monofun_cfun)
+done
+
 end
diff -r 488837bf01d7 -r 27f74e853a54 src/HOLCF/Representable.thy
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOLCF/Representable.thy	Tue Nov 10 06:48:26 2009 -0800
@@ -0,0 +1,995 @@
+(*  Title:      HOLCF/Representable.thy
+    Author:     Brian Huffman
+*)
+
+header {* Representable Types *}
+
+theory Representable
+imports Algebraic Universal Ssum Sprod One ConvexPD
+begin
+
+subsection {* Class of representable types *}
+
+text "Overloaded embedding and projection functions between
+      a representable type and the universal domain."
+
+class rep = bifinite +
+  fixes emb :: "'a::pcpo \<rightarrow> udom"
+  fixes prj :: "udom \<rightarrow> 'a::pcpo"
+  assumes ep_pair_emb_prj: "ep_pair emb prj"
+
+interpretation rep!:
+  pcpo_ep_pair
+    "emb :: 'a::rep \<rightarrow> udom"
+    "prj :: udom \<rightarrow> 'a::rep"
+  unfolding pcpo_ep_pair_def
+  by (rule ep_pair_emb_prj)
+
+lemmas emb_inverse = rep.e_inverse
+lemmas emb_prj_below = rep.e_p_below
+lemmas emb_eq_iff = rep.e_eq_iff
+lemmas emb_strict = rep.e_strict
+lemmas prj_strict = rep.p_strict
+
+
+subsection {* Making @{term rep} the default class *}
+
+text {*
+  From now on, free type variables are assumed to be in class
+  @{term rep}, unless specified otherwise.
+*}
+
+defaultsort rep
+
+subsection {* Representations of types *}
+
+text "A TypeRep is an algebraic deflation over the universe of values."
+
+types TypeRep = "udom alg_defl"
+translations "TypeRep" \<leftharpoondown> (type) "udom alg_defl"
+
+definition
+  Rep_of :: "'a::rep itself \<Rightarrow> TypeRep"
+where
+  "Rep_of TYPE('a::rep) =
+    (\<Squnion>i. alg_defl_principal (Abs_fin_defl
+      (emb oo (approx i :: 'a \<rightarrow> 'a) oo prj)))"
+
+syntax "_REP" :: "type \<Rightarrow> TypeRep"  ("(1REP/(1'(_')))")
+translations "REP(t)" \<rightleftharpoons> "CONST Rep_of TYPE(t)"
+
+lemma cast_REP:
+  "cast\<cdot>REP('a::rep) = (emb::'a \<rightarrow> udom) oo (prj::udom \<rightarrow> 'a)"
+proof -
+  let ?a = "\<lambda>i. emb oo approx i oo (prj::udom \<rightarrow> 'a)"
+  have a: "\<And>i. finite_deflation (?a i)"
+    apply (rule rep.finite_deflation_e_d_p)
+    apply (rule finite_deflation_approx)
+    done
+  show ?thesis
+    unfolding Rep_of_def
+    apply (subst contlub_cfun_arg)
+    apply (rule chainI)
+    apply (rule alg_defl.principal_mono)
+    apply (rule Abs_fin_defl_mono [OF a a])
+    apply (rule chainE, simp)
+    apply (subst cast_alg_defl_principal)
+    apply (simp add: Abs_fin_defl_inverse a)
+    apply (simp add: expand_cfun_eq lub_distribs)
+    done
+qed
+
+lemma emb_prj: "emb\<cdot>((prj\<cdot>x)::'a::rep) = cast\<cdot>REP('a)\<cdot>x"
+by (simp add: cast_REP)
+
+lemma in_REP_iff:
+  "x ::: REP('a::rep) \<longleftrightarrow> emb\<cdot>((prj\<cdot>x)::'a) = x"
+by (simp add: in_deflation_def cast_REP)
+
+lemma prj_inverse:
+  "x ::: REP('a::rep) \<Longrightarrow> emb\<cdot>((prj\<cdot>x)::'a) = x"
+by (simp only: in_REP_iff)
+
+lemma emb_in_REP [simp]:
+  "emb\<cdot>(x::'a::rep) ::: REP('a)"
+by (simp add: in_REP_iff)
+
+subsection {* Coerce operator *}
+
+definition coerce :: "'a \<rightarrow> 'b"
+where "coerce = prj oo emb"
+
+lemma beta_coerce: "coerce\<cdot>x = prj\<cdot>(emb\<cdot>x)"
+by (simp add: coerce_def)
+
+lemma prj_emb: "prj\<cdot>(emb\<cdot>x) = coerce\<cdot>x"
+by (simp add: coerce_def)
+
+lemma coerce_strict [simp]: "coerce\<cdot>\<bottom> = \<bottom>"
+by (simp add: coerce_def)
+
+lemma coerce_eq_ID [simp]: "(coerce :: 'a \<rightarrow> 'a) = ID"
+by (rule ext_cfun, simp add: beta_coerce)
+
+lemma emb_coerce:
+  "REP('a) \<sqsubseteq> REP('b)
+   \<Longrightarrow> emb\<cdot>((coerce::'a \<rightarrow> 'b)\<cdot>x) = emb\<cdot>x"
+ apply (simp add: beta_coerce)
+ apply (rule prj_inverse)
+ apply (erule subdeflationD)
+ apply (rule emb_in_REP)
+done
+
+lemma coerce_prj:
+  "REP('a) \<sqsubseteq> REP('b)
+   \<Longrightarrow> (coerce::'b \<rightarrow> 'a)\<cdot>(prj\<cdot>x) = prj\<cdot>x"
+ apply (simp add: coerce_def)
+ apply (rule emb_eq_iff [THEN iffD1])
+ apply (simp only: emb_prj)
+ apply (rule deflation_below_comp1)
+   apply (rule deflation_cast)
+  apply (rule deflation_cast)
+ apply (erule monofun_cfun_arg)
+done
+
+lemma coerce_coerce [simp]:
+  "REP('a) \<sqsubseteq> REP('b)
+   \<Longrightarrow> coerce\<cdot>((coerce::'a \<rightarrow> 'b)\<cdot>x) = coerce\<cdot>x"
+by (simp add: beta_coerce prj_inverse subdeflationD)
+
+lemma coerce_inverse:
+  "emb\<cdot>(x::'a) ::: REP('b) \<Longrightarrow> coerce\<cdot>(coerce\<cdot>x :: 'b) = x"
+by (simp only: beta_coerce prj_inverse emb_inverse)
+
+lemma coerce_type:
+  "REP('a) \<sqsubseteq> REP('b)
+   \<Longrightarrow> emb\<cdot>((coerce::'a \<rightarrow> 'b)\<cdot>x) ::: REP('a)"
+by (simp add: beta_coerce prj_inverse subdeflationD)
+
+lemma ep_pair_coerce:
+  "REP('a) \<sqsubseteq> REP('b)
+   \<Longrightarrow> ep_pair (coerce::'a \<rightarrow> 'b) (coerce::'b \<rightarrow> 'a)"
+ apply (rule ep_pair.intro)
+  apply simp
+ apply (simp only: beta_coerce)
+ apply (rule below_trans)
+  apply (rule monofun_cfun_arg)
+  apply (rule emb_prj_below)
+ apply simp
+done
+
+subsection {* Proving a subtype is representable *}
+
+text {*
+  Temporarily relax type constraints for @{term "approx"},
+  @{term emb}, and @{term prj}.
+*}
+
+setup {* Sign.add_const_constraint
+  (@{const_name "approx"}, SOME @{typ "nat \<Rightarrow> 'a::cpo \<rightarrow> 'a"}) *}
+
+setup {* Sign.add_const_constraint
+  (@{const_name emb}, SOME @{typ "'a::pcpo \<rightarrow> udom"}) *}
+
+setup {* Sign.add_const_constraint
+  (@{const_name prj}, SOME @{typ "udom \<rightarrow> 'a::pcpo"}) *}
+
+lemma typedef_rep_class:
+  fixes Rep :: "'a::pcpo \<Rightarrow> udom"
+  fixes Abs :: "udom \<Rightarrow> 'a::pcpo"
+  fixes t :: TypeRep
+  assumes type: "type_definition Rep Abs {x. x ::: t}"
+  assumes below: "op \<sqsubseteq> \<equiv> \<lambda>x y. Rep x \<sqsubseteq> Rep y"
+  assumes emb: "emb = (\<Lambda> x. Rep x)"
+  assumes prj: "prj = (\<Lambda> x. Abs (cast\<cdot>t\<cdot>x))"
+  assumes approx:
+    "(approx :: nat \<Rightarrow> 'a \<rightarrow> 'a) = (\<lambda>i. prj oo cast\<cdot>(approx i\<cdot>t) oo emb)"
+  shows "OFCLASS('a, rep_class)"
+proof
+  have adm: "adm (\<lambda>x. x \<in> {x. x ::: t})"
+    by (simp add: adm_in_deflation)
+  have emb_beta: "\<And>x. emb\<cdot>x = Rep x"
+    unfolding emb
+    apply (rule beta_cfun)
+    apply (rule typedef_cont_Rep [OF type below adm])
+    done
+  have prj_beta: "\<And>y. prj\<cdot>y = Abs (cast\<cdot>t\<cdot>y)"
+    unfolding prj
+    apply (rule beta_cfun)
+    apply (rule typedef_cont_Abs [OF type below adm])
+    apply simp_all
+    done
+  have emb_in_deflation: "\<And>x::'a. emb\<cdot>x ::: t"
+    using type_definition.Rep [OF type]
+    by (simp add: emb_beta)
+  have prj_emb: "\<And>x::'a. prj\<cdot>(emb\<cdot>x) = x"
+    unfolding prj_beta
+    apply (simp add: cast_fixed [OF emb_in_deflation])
+    apply (simp add: emb_beta type_definition.Rep_inverse [OF type])
+    done
+  have emb_prj: "\<And>y. emb\<cdot>(prj\<cdot>y :: 'a) = cast\<cdot>t\<cdot>y"
+    unfolding prj_beta emb_beta
+    by (simp add: type_definition.Abs_inverse [OF type])
+  show "ep_pair (emb :: 'a \<rightarrow> udom) prj"
+    apply default
+    apply (simp add: prj_emb)
+    apply (simp add: emb_prj cast.below)
+    done
+  show "chain (approx :: nat \<Rightarrow> 'a \<rightarrow> 'a)"
+    unfolding approx by simp
+  show "\<And>x::'a. (\<Squnion>i. approx i\<cdot>x) = x"
+    unfolding approx
+    apply (simp add: lub_distribs)
+    apply (subst cast_fixed [OF emb_in_deflation])
+    apply (rule prj_emb)
+    done
+  have cast_cast_approx:
+    "\<And>i x. cast\<cdot>t\<cdot>(cast\<cdot>(approx i\<cdot>t)\<cdot>x) = cast\<cdot>(approx i\<cdot>t)\<cdot>x"
+    apply (rule cast_fixed)
+    apply (rule subdeflationD)
+    apply (rule approx.below)
+    apply (rule cast_in_deflation)
+    done
+  show "\<And>(i::nat) (x::'a). approx i\<cdot>(approx i\<cdot>x) = approx i\<cdot>x"
+    unfolding approx
+    apply simp
+    apply (simp add: emb_prj)
+    apply (simp add: cast_cast_approx)
+    done
+  show "\<And>i::nat. finite {x::'a. approx i\<cdot>x = x}"
+    apply (rule_tac B="(\<lambda>x. prj\<cdot>x) ` {x. cast\<cdot>(approx i\<cdot>t)\<cdot>x = x}"
+           in finite_subset)
+    apply (clarsimp simp add: approx)
+    apply (drule_tac f="\<lambda>x. emb\<cdot>x" in arg_cong)
+    apply (rule image_eqI)
+    apply (rule prj_emb [symmetric])
+    apply (simp add: emb_prj)
+    apply (simp add: cast_cast_approx)
+    apply (rule finite_imageI)
+    apply (simp add: cast_approx_fixed_iff)
+    apply (simp add: Collect_conj_eq)
+    apply (simp add: finite_fixes_approx)
+    done
+qed
+
+text {* Restore original typing constraints *}
+
+setup {* Sign.add_const_constraint
+  (@{const_name "approx"}, SOME @{typ "nat \<Rightarrow> 'a::profinite \<rightarrow> 'a"}) *}
+
+setup {* Sign.add_const_constraint
+  (@{const_name emb}, SOME @{typ "'a::rep \<rightarrow> udom"}) *}
+
+setup {* Sign.add_const_constraint
+  (@{const_name prj}, SOME @{typ "udom \<rightarrow> 'a::rep"}) *}
+
+lemma typedef_REP:
+  fixes Rep :: "'a::rep \<Rightarrow> udom"
+  fixes Abs :: "udom \<Rightarrow> 'a::rep"
+  fixes t :: TypeRep
+  assumes type: "type_definition Rep Abs {x. x ::: t}"
+  assumes below: "op \<sqsubseteq> \<equiv> \<lambda>x y. Rep x \<sqsubseteq> Rep y"
+  assumes emb: "emb = (\<Lambda> x. Rep x)"
+  assumes prj: "prj = (\<Lambda> x. Abs (cast\<cdot>t\<cdot>x))"
+  shows "REP('a) = t"
+proof -
+  have adm: "adm (\<lambda>x. x \<in> {x. x ::: t})"
+    by (simp add: adm_in_deflation)
+  have emb_beta: "\<And>x. emb\<cdot>x = Rep x"
+    unfolding emb
+    apply (rule beta_cfun)
+    apply (rule typedef_cont_Rep [OF type below adm])
+    done
+  have prj_beta: "\<And>y. prj\<cdot>y = Abs (cast\<cdot>t\<cdot>y)"
+    unfolding prj
+    apply (rule beta_cfun)
+    apply (rule typedef_cont_Abs [OF type below adm])
+    apply simp_all
+    done
+  have emb_in_deflation: "\<And>x::'a. emb\<cdot>x ::: t"
+    using type_definition.Rep [OF type]
+    by (simp add: emb_beta)
+  have prj_emb: "\<And>x::'a. prj\<cdot>(emb\<cdot>x) = x"
+    unfolding prj_beta
+    apply (simp add: cast_fixed [OF emb_in_deflation])
+    apply (simp add: emb_beta type_definition.Rep_inverse [OF type])
+    done
+  have emb_prj: "\<And>y. emb\<cdot>(prj\<cdot>y :: 'a) = cast\<cdot>t\<cdot>y"
+    unfolding prj_beta emb_beta
+    by (simp add: type_definition.Abs_inverse [OF type])
+  show "REP('a) = t"
+    apply (rule cast_eq_imp_eq, rule ext_cfun)
+    apply (simp add: cast_REP emb_prj)
+    done
+qed
+
+
+subsection {* Instances of class @{text rep} *}
+
+subsubsection {* Universal Domain *}
+
+text "The Universal Domain itself is trivially representable."
+
+instantiation udom :: rep
+begin
+
+definition emb_udom_def [simp]: "emb = (ID :: udom \<rightarrow> udom)"
+definition prj_udom_def [simp]: "prj = (ID :: udom \<rightarrow> udom)"
+
+instance
+ apply (intro_classes)
+ apply (simp_all add: ep_pair.intro)
+done
+
+end
+
+subsubsection {* Lifted types *}
+
+instantiation lift :: (countable) rep
+begin
+
+definition emb_lift_def:
+  "emb = udom_emb oo (FLIFT x. Def (to_nat x))"
+
+definition prj_lift_def:
+  "prj = (FLIFT n. if (\<exists>x::'a::countable. n = to_nat x)
+                    then Def (THE x::'a. n = to_nat x) else \<bottom>) oo udom_prj"
+
+instance
+ apply (intro_classes, unfold emb_lift_def prj_lift_def)
+ apply (rule ep_pair_comp [OF _ ep_pair_udom])
+ apply (rule ep_pair.intro)
+  apply (case_tac x, simp, simp)
+ apply (case_tac y, simp, clarsimp)
+done
+
+end
+
+subsubsection {* Representable type constructors *}
+
+text "Functions between representable types are representable."
+
+instantiation "->" :: (rep, rep) rep
+begin
+
+definition emb_cfun_def: "emb = udom_emb oo cfun_map\<cdot>prj\<cdot>emb"
+definition prj_cfun_def: "prj = cfun_map\<cdot>emb\<cdot>prj oo udom_prj"
+
+instance
+ apply (intro_classes, unfold emb_cfun_def prj_cfun_def)
+ apply (intro ep_pair_comp ep_pair_cfun_map ep_pair_emb_prj ep_pair_udom)
+done
+
+end
+
+text "Strict products of representable types are representable."
+
+instantiation "**" :: (rep, rep) rep
+begin
+
+definition emb_sprod_def: "emb = udom_emb oo sprod_map\<cdot>emb\<cdot>emb"
+definition prj_sprod_def: "prj = sprod_map\<cdot>prj\<cdot>prj oo udom_prj"
+
+instance
+ apply (intro_classes, unfold emb_sprod_def prj_sprod_def)
+ apply (intro ep_pair_comp ep_pair_sprod_map ep_pair_emb_prj ep_pair_udom)
+done
+
+end
+
+text "Strict sums of representable types are representable."
+
+instantiation "++" :: (rep, rep) rep
+begin
+
+definition emb_ssum_def: "emb = udom_emb oo ssum_map\<cdot>emb\<cdot>emb"
+definition prj_ssum_def: "prj = ssum_map\<cdot>prj\<cdot>prj oo udom_prj"
+
+instance
+ apply (intro_classes, unfold emb_ssum_def prj_ssum_def)
+ apply (intro ep_pair_comp ep_pair_ssum_map ep_pair_emb_prj ep_pair_udom)
+done
+
+end
+
+text "Up of a representable type is representable."
+
+instantiation "u" :: (rep) rep
+begin
+
+definition emb_u_def: "emb = udom_emb oo u_map\<cdot>emb"
+definition prj_u_def: "prj = u_map\<cdot>prj oo udom_prj"
+
+instance
+ apply (intro_classes, unfold emb_u_def prj_u_def)
+ apply (intro ep_pair_comp ep_pair_u_map ep_pair_emb_prj ep_pair_udom)
+done
+
+end
+
+text "Cartesian products of representable types are representable."
+
+instantiation "*" :: (rep, rep) rep
+begin
+
+definition emb_cprod_def: "emb = udom_emb oo cprod_map\<cdot>emb\<cdot>emb"
+definition prj_cprod_def: "prj = cprod_map\<cdot>prj\<cdot>prj oo udom_prj"
+
+instance
+ apply (intro_classes, unfold emb_cprod_def prj_cprod_def)
+ apply (intro ep_pair_comp ep_pair_cprod_map ep_pair_emb_prj ep_pair_udom)
+done
+
+end
+
+text "Upper powerdomain of a representable type is representable."
+
+instantiation upper_pd :: (rep) rep
+begin
+
+definition emb_upper_pd_def: "emb = udom_emb oo upper_map\<cdot>emb"
+definition prj_upper_pd_def: "prj = upper_map\<cdot>prj oo udom_prj"
+
+instance
+ apply (intro_classes, unfold emb_upper_pd_def prj_upper_pd_def)
+ apply (intro ep_pair_comp ep_pair_upper_map ep_pair_emb_prj ep_pair_udom)
+done
+
+end
+
+text "Lower powerdomain of a representable type is representable."
+
+instantiation lower_pd :: (rep) rep
+begin
+
+definition emb_lower_pd_def: "emb = udom_emb oo lower_map\<cdot>emb"
+definition prj_lower_pd_def: "prj = lower_map\<cdot>prj oo udom_prj"
+
+instance
+ apply (intro_classes, unfold emb_lower_pd_def prj_lower_pd_def)
+ apply (intro ep_pair_comp ep_pair_lower_map ep_pair_emb_prj ep_pair_udom)
+done
+
+end
+
+text "Convex powerdomain of a representable type is representable."
+
+instantiation convex_pd :: (rep) rep
+begin
+
+definition emb_convex_pd_def: "emb = udom_emb oo convex_map\<cdot>emb"
+definition prj_convex_pd_def: "prj = convex_map\<cdot>prj oo udom_prj"
+
+instance
+ apply (intro_classes, unfold emb_convex_pd_def prj_convex_pd_def)
+ apply (intro ep_pair_comp ep_pair_convex_map ep_pair_emb_prj ep_pair_udom)
+done
+
+end
+
+subsection {* Finite deflation lemmas *}
+
+text "TODO: move these lemmas somewhere else"
+
+lemma finite_compact_range_imp_finite_range:
+  fixes d :: "'a::profinite \<rightarrow> 'b::cpo"
+  assumes "finite ((\<lambda>x. d\<cdot>x) ` {x. compact x})"
+  shows "finite (range (\<lambda>x. d\<cdot>x))"
+proof (rule finite_subset [OF _ prems])
+  {
+    fix x :: 'a
+    have "range (\<lambda>i. d\<cdot>(approx i\<cdot>x)) \<subseteq> (\<lambda>x. d\<cdot>x) ` {x. compact x}"
+      by auto
+    hence "finite (range (\<lambda>i. d\<cdot>(approx i\<cdot>x)))"
+      using prems by (rule finite_subset)
+    hence "finite_chain (\<lambda>i. d\<cdot>(approx i\<cdot>x))"
+      by (simp add: finite_range_imp_finch)
+    hence "\<exists>i. (\<Squnion>i. d\<cdot>(approx i\<cdot>x)) = d\<cdot>(approx i\<cdot>x)"
+      by (simp add: finite_chain_def maxinch_is_thelub)
+    hence "\<exists>i. d\<cdot>x = d\<cdot>(approx i\<cdot>x)"
+      by (simp add: lub_distribs)
+    hence "d\<cdot>x \<in> (\<lambda>x. d\<cdot>x) ` {x. compact x}"
+      by auto
+  }
+  thus "range (\<lambda>x. d\<cdot>x) \<subseteq> (\<lambda>x. d\<cdot>x) ` {x. compact x}"
+    by clarsimp
+qed
+
+lemma finite_deflation_upper_map:
+  assumes "finite_deflation d" shows "finite_deflation (upper_map\<cdot>d)"
+proof (intro finite_deflation.intro finite_deflation_axioms.intro)
+  interpret d: finite_deflation d by fact
+  have "deflation d" by fact
+  thus "deflation (upper_map\<cdot>d)" by (rule deflation_upper_map)
+  have "finite (range (\<lambda>x. d\<cdot>x))" by (rule d.finite_range)
+  hence "finite (Rep_compact_basis -` range (\<lambda>x. d\<cdot>x))"
+    by (rule finite_vimageI, simp add: inj_on_def Rep_compact_basis_inject)
+  hence "finite (Pow (Rep_compact_basis -` range (\<lambda>x. d\<cdot>x)))" by simp
+  hence "finite (Rep_pd_basis -` (Pow (Rep_compact_basis -` range (\<lambda>x. d\<cdot>x))))"
+    by (rule finite_vimageI, simp add: inj_on_def Rep_pd_basis_inject)
+  hence "finite (upper_principal ` Rep_pd_basis -` (Pow (Rep_compact_basis -` range (\<lambda>x. d\<cdot>x))))" by simp
+  hence "finite ((\<lambda>xs. upper_map\<cdot>d\<cdot>xs) ` range upper_principal)"
+    apply (rule finite_subset [COMP swap_prems_rl])
+    apply (clarsimp, rename_tac t)
+    apply (induct_tac t rule: pd_basis_induct)
+    apply (simp only: upper_unit_Rep_compact_basis [symmetric] upper_map_unit)
+    apply (subgoal_tac "\<exists>b. d\<cdot>(Rep_compact_basis a) = Rep_compact_basis b")
+    apply clarsimp
+    apply (rule imageI)
+    apply (rule vimageI2)
+    apply (simp add: Rep_PDUnit)
+    apply (rule image_eqI)
+    apply (erule sym)
+    apply simp
+    apply (rule exI)
+    apply (rule Abs_compact_basis_inverse [symmetric])
+    apply (simp add: d.compact)
+    apply (simp only: upper_plus_principal [symmetric] upper_map_plus)
+    apply clarsimp
+    apply (rule imageI)
+    apply (rule vimageI2)
+    apply (simp add: Rep_PDPlus)
+    done
+  moreover have "{xs::'a upper_pd. compact xs} = range upper_principal"
+    by (auto dest: upper_pd.compact_imp_principal)
+  ultimately have "finite ((\<lambda>xs. upper_map\<cdot>d\<cdot>xs) ` {xs::'a upper_pd. compact xs})"
+    by simp
+  hence "finite (range (\<lambda>xs. upper_map\<cdot>d\<cdot>xs))"
+    by (rule finite_compact_range_imp_finite_range)
+  thus "finite {xs. upper_map\<cdot>d\<cdot>xs = xs}"
+    by (rule finite_range_imp_finite_fixes)
+qed
+
+lemma finite_deflation_lower_map:
+  assumes "finite_deflation d" shows "finite_deflation (lower_map\<cdot>d)"
+proof (intro finite_deflation.intro finite_deflation_axioms.intro)
+  interpret d: finite_deflation d by fact
+  have "deflation d" by fact
+  thus "deflation (lower_map\<cdot>d)" by (rule deflation_lower_map)
+  have "finite (range (\<lambda>x. d\<cdot>x))" by (rule d.finite_range)
+  hence "finite (Rep_compact_basis -` range (\<lambda>x. d\<cdot>x))"
+    by (rule finite_vimageI, simp add: inj_on_def Rep_compact_basis_inject)
+  hence "finite (Pow (Rep_compact_basis -` range (\<lambda>x. d\<cdot>x)))" by simp
+  hence "finite (Rep_pd_basis -` (Pow (Rep_compact_basis -` range (\<lambda>x. d\<cdot>x))))"
+    by (rule finite_vimageI, simp add: inj_on_def Rep_pd_basis_inject)
+  hence "finite (lower_principal ` Rep_pd_basis -` (Pow (Rep_compact_basis -` range (\<lambda>x. d\<cdot>x))))" by simp
+  hence "finite ((\<lambda>xs. lower_map\<cdot>d\<cdot>xs) ` range lower_principal)"
+    apply (rule finite_subset [COMP swap_prems_rl])
+    apply (clarsimp, rename_tac t)
+    apply (induct_tac t rule: pd_basis_induct)
+    apply (simp only: lower_unit_Rep_compact_basis [symmetric] lower_map_unit)
+    apply (subgoal_tac "\<exists>b. d\<cdot>(Rep_compact_basis a) = Rep_compact_basis b")
+    apply clarsimp
+    apply (rule imageI)
+    apply (rule vimageI2)
+    apply (simp add: Rep_PDUnit)
+    apply (rule image_eqI)
+    apply (erule sym)
+    apply simp
+    apply (rule exI)
+    apply (rule Abs_compact_basis_inverse [symmetric])
+    apply (simp add: d.compact)
+    apply (simp only: lower_plus_principal [symmetric] lower_map_plus)
+    apply clarsimp
+    apply (rule imageI)
+    apply (rule vimageI2)
+    apply (simp add: Rep_PDPlus)
+    done
+  moreover have "{xs::'a lower_pd. compact xs} = range lower_principal"
+    by (auto dest: lower_pd.compact_imp_principal)
+  ultimately have "finite ((\<lambda>xs. lower_map\<cdot>d\<cdot>xs) ` {xs::'a lower_pd. compact xs})"
+    by simp
+  hence "finite (range (\<lambda>xs. lower_map\<cdot>d\<cdot>xs))"
+    by (rule finite_compact_range_imp_finite_range)
+  thus "finite {xs. lower_map\<cdot>d\<cdot>xs = xs}"
+    by (rule finite_range_imp_finite_fixes)
+qed
+
+lemma finite_deflation_convex_map:
+  assumes "finite_deflation d" shows "finite_deflation (convex_map\<cdot>d)"
+proof (intro finite_deflation.intro finite_deflation_axioms.intro)
+  interpret d: finite_deflation d by fact
+  have "deflation d" by fact
+  thus "deflation (convex_map\<cdot>d)" by (rule deflation_convex_map)
+  have "finite (range (\<lambda>x. d\<cdot>x))" by (rule d.finite_range)
+  hence "finite (Rep_compact_basis -` range (\<lambda>x. d\<cdot>x))"
+    by (rule finite_vimageI, simp add: inj_on_def Rep_compact_basis_inject)
+  hence "finite (Pow (Rep_compact_basis -` range (\<lambda>x. d\<cdot>x)))" by simp
+  hence "finite (Rep_pd_basis -` (Pow (Rep_compact_basis -` range (\<lambda>x. d\<cdot>x))))"
+    by (rule finite_vimageI, simp add: inj_on_def Rep_pd_basis_inject)
+  hence "finite (convex_principal ` Rep_pd_basis -` (Pow (Rep_compact_basis -` range (\<lambda>x. d\<cdot>x))))" by simp
+  hence "finite ((\<lambda>xs. convex_map\<cdot>d\<cdot>xs) ` range convex_principal)"
+    apply (rule finite_subset [COMP swap_prems_rl])
+    apply (clarsimp, rename_tac t)
+    apply (induct_tac t rule: pd_basis_induct)
+    apply (simp only: convex_unit_Rep_compact_basis [symmetric] convex_map_unit)
+    apply (subgoal_tac "\<exists>b. d\<cdot>(Rep_compact_basis a) = Rep_compact_basis b")
+    apply clarsimp
+    apply (rule imageI)
+    apply (rule vimageI2)
+    apply (simp add: Rep_PDUnit)
+    apply (rule image_eqI)
+    apply (erule sym)
+    apply simp
+    apply (rule exI)
+    apply (rule Abs_compact_basis_inverse [symmetric])
+    apply (simp add: d.compact)
+    apply (simp only: convex_plus_principal [symmetric] convex_map_plus)
+    apply clarsimp
+    apply (rule imageI)
+    apply (rule vimageI2)
+    apply (simp add: Rep_PDPlus)
+    done
+  moreover have "{xs::'a convex_pd. compact xs} = range convex_principal"
+    by (auto dest: convex_pd.compact_imp_principal)
+  ultimately have "finite ((\<lambda>xs. convex_map\<cdot>d\<cdot>xs) ` {xs::'a convex_pd. compact xs})"
+    by simp
+  hence "finite (range (\<lambda>xs. convex_map\<cdot>d\<cdot>xs))"
+    by (rule finite_compact_range_imp_finite_range)
+  thus "finite {xs. convex_map\<cdot>d\<cdot>xs = xs}"
+    by (rule finite_range_imp_finite_fixes)
+qed
+
+subsection {* Type combinators *}
+
+definition
+  TypeRep_fun1 ::
+    "((udom \<rightarrow> udom) \<rightarrow> ('a \<rightarrow> 'a))
+      \<Rightarrow> (TypeRep \<rightarrow> TypeRep)"
+where
+  "TypeRep_fun1 f =
+    alg_defl.basis_fun (\<lambda>a.
+      alg_defl_principal (
+        Abs_fin_defl (udom_emb oo f\<cdot>(Rep_fin_defl a) oo udom_prj)))"
+
+definition
+  TypeRep_fun2 ::
+    "((udom \<rightarrow> udom) \<rightarrow> (udom \<rightarrow> udom) \<rightarrow> ('a \<rightarrow> 'a))
+      \<Rightarrow> (TypeRep \<rightarrow> TypeRep \<rightarrow> TypeRep)"
+where
+  "TypeRep_fun2 f =
+    alg_defl.basis_fun (\<lambda>a.
+      alg_defl.basis_fun (\<lambda>b.
+        alg_defl_principal (
+          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"
+
+lemma Rep_fin_defl_mono: "a \<sqsubseteq> b \<Longrightarrow> Rep_fin_defl a \<sqsubseteq> Rep_fin_defl b"
+unfolding below_fin_defl_def .
+
+lemma cast_TypeRep_fun1:
+  assumes f: "\<And>a. finite_deflation a \<Longrightarrow> finite_deflation (f\<cdot>a)"
+  shows "cast\<cdot>(TypeRep_fun1 f\<cdot>A) = udom_emb oo f\<cdot>(cast\<cdot>A) oo udom_prj"
+proof -
+  have 1: "\<And>a. finite_deflation (udom_emb oo f\<cdot>(Rep_fin_defl a) oo udom_prj)"
+    apply (rule ep_pair.finite_deflation_e_d_p [OF ep_pair_udom])
+    apply (rule f, rule finite_deflation_Rep_fin_defl)
+    done
+  show ?thesis
+    by (induct A rule: alg_defl.principal_induct, simp)
+       (simp only: TypeRep_fun1_def
+                   alg_defl.basis_fun_principal
+                   alg_defl.basis_fun_mono
+                   alg_defl.principal_mono
+                   Abs_fin_defl_mono [OF 1 1]
+                   monofun_cfun below_refl
+                   Rep_fin_defl_mono
+                   cast_alg_defl_principal
+                   Abs_fin_defl_inverse [unfolded mem_Collect_eq, OF 1])
+qed
+
+lemma cast_TypeRep_fun2:
+  assumes f: "\<And>a b. finite_deflation a \<Longrightarrow> finite_deflation b \<Longrightarrow>
+                finite_deflation (f\<cdot>a\<cdot>b)"
+  shows "cast\<cdot>(TypeRep_fun2 f\<cdot>A\<cdot>B) = udom_emb oo f\<cdot>(cast\<cdot>A)\<cdot>(cast\<cdot>B) oo udom_prj"
+proof -
+  have 1: "\<And>a b. finite_deflation
+           (udom_emb oo f\<cdot>(Rep_fin_defl a)\<cdot>(Rep_fin_defl b) oo udom_prj)"
+    apply (rule ep_pair.finite_deflation_e_d_p [OF ep_pair_udom])
+    apply (rule f, (rule finite_deflation_Rep_fin_defl)+)
+    done
+  show ?thesis
+    by (induct A B rule: alg_defl.principal_induct2, simp, simp)
+       (simp only: TypeRep_fun2_def
+                   alg_defl.basis_fun_principal
+                   alg_defl.basis_fun_mono
+                   alg_defl.principal_mono
+                   Abs_fin_defl_mono [OF 1 1]
+                   monofun_cfun below_refl
+                   Rep_fin_defl_mono
+                   cast_alg_defl_principal
+                   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
+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
+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
+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
+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
+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
+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
+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
+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)"
+apply (rule cast_eq_imp_eq, rule ext_cfun)
+apply (simp add: cast_REP cast_cfun_typ)
+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)"
+apply (rule cast_eq_imp_eq, rule ext_cfun)
+apply (simp add: cast_REP cast_ssum_typ)
+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)"
+apply (rule cast_eq_imp_eq, rule ext_cfun)
+apply (simp add: cast_REP cast_sprod_typ)
+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)"
+apply (rule cast_eq_imp_eq, rule ext_cfun)
+apply (simp add: cast_REP cast_cprod_typ)
+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)"
+apply (rule cast_eq_imp_eq, rule ext_cfun)
+apply (simp add: cast_REP cast_u_typ)
+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)"
+apply (rule cast_eq_imp_eq, rule ext_cfun)
+apply (simp add: cast_REP cast_upper_typ)
+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)"
+apply (rule cast_eq_imp_eq, rule ext_cfun)
+apply (simp add: cast_REP cast_lower_typ)
+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)"
+apply (rule cast_eq_imp_eq, rule ext_cfun)
+apply (simp add: cast_REP cast_convex_typ)
+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
+  REP_cprod
+  REP_up
+  REP_upper
+  REP_lower
+  REP_convex
+
+subsection {* Isomorphic deflations *}
+
+definition
+  isodefl :: "('a::rep \<rightarrow> 'a) \<Rightarrow> udom alg_defl \<Rightarrow> bool"
+where
+  "isodefl d t \<longleftrightarrow> cast\<cdot>t = emb oo d oo prj"
+
+lemma isodeflI: "(\<And>x. cast\<cdot>t\<cdot>x = emb\<cdot>(d\<cdot>(prj\<cdot>x))) \<Longrightarrow> isodefl d t"
+unfolding isodefl_def by (simp add: ext_cfun)
+
+lemma cast_isodefl: "isodefl d t \<Longrightarrow> cast\<cdot>t = (\<Lambda> x. emb\<cdot>(d\<cdot>(prj\<cdot>x)))"
+unfolding isodefl_def by (simp add: ext_cfun)
+
+lemma isodefl_strict: "isodefl d t \<Longrightarrow> d\<cdot>\<bottom> = \<bottom>"
+unfolding isodefl_def
+by (drule cfun_fun_cong [where x="\<bottom>"], simp)
+
+lemma isodefl_imp_deflation:
+  fixes d :: "'a::rep \<rightarrow> 'a"
+  assumes "isodefl d t" shows "deflation d"
+proof
+  note prems [unfolded isodefl_def, simp]
+  fix x :: 'a
+  show "d\<cdot>(d\<cdot>x) = d\<cdot>x"
+    using cast.idem [of t "emb\<cdot>x"] by simp
+  show "d\<cdot>x \<sqsubseteq> x"
+    using cast.below [of t "emb\<cdot>x"] by simp
+qed
+
+lemma isodefl_ID_REP: "isodefl (ID :: 'a \<rightarrow> 'a) REP('a)"
+unfolding isodefl_def by (simp add: cast_REP)
+
+lemma isodefl_REP_imp_ID: "isodefl (d :: 'a \<rightarrow> 'a) REP('a) \<Longrightarrow> d = ID"
+unfolding isodefl_def
+apply (simp add: cast_REP)
+apply (simp add: expand_cfun_eq)
+apply (rule allI)
+apply (drule_tac x="emb\<cdot>x" in spec)
+apply simp
+done
+
+lemma isodefl_bottom: "isodefl \<bottom> \<bottom>"
+unfolding isodefl_def by (simp add: expand_cfun_eq)
+
+lemma adm_isodefl:
+  "cont f \<Longrightarrow> cont g \<Longrightarrow> adm (\<lambda>x. isodefl (f x) (g x))"
+unfolding isodefl_def by simp
+
+lemma isodefl_lub:
+  assumes "chain d" and "chain t"
+  assumes "\<And>i. isodefl (d i) (t i)"
+  shows "isodefl (\<Squnion>i. d i) (\<Squnion>i. t i)"
+using prems unfolding isodefl_def
+by (simp add: contlub_cfun_arg contlub_cfun_fun)
+
+lemma isodefl_fix:
+  assumes "\<And>d t. isodefl d t \<Longrightarrow> isodefl (f\<cdot>d) (g\<cdot>t)"
+  shows "isodefl (fix\<cdot>f) (fix\<cdot>g)"
+unfolding fix_def2
+apply (rule isodefl_lub, simp, simp)
+apply (induct_tac i)
+apply (simp add: isodefl_bottom)
+apply (simp add: prems)
+done
+
+lemma isodefl_coerce:
+  fixes d :: "'a \<rightarrow> 'a"
+  assumes REP: "REP('b) = REP('a)"
+  shows "isodefl d t \<Longrightarrow> isodefl (coerce oo d oo coerce :: 'b \<rightarrow> 'b) t"
+unfolding isodefl_def
+apply (simp add: expand_cfun_eq)
+apply (simp add: emb_coerce coerce_prj REP)
+done
+
+lemma isodefl_cfun:
+  "isodefl d1 t1 \<Longrightarrow> isodefl d2 t2 \<Longrightarrow>
+    isodefl (cfun_map\<cdot>d1\<cdot>d2) (cfun_typ\<cdot>t1\<cdot>t2)"
+apply (rule isodeflI)
+apply (simp add: cast_cfun_typ 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)"
+apply (rule isodeflI)
+apply (simp add: cast_ssum_typ 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)"
+apply (rule isodeflI)
+apply (simp add: cast_sprod_typ cast_isodefl)
+apply (simp add: emb_sprod_def prj_sprod_def)
+apply (simp add: sprod_map_map isodefl_strict)
+done
+
+lemma isodefl_u:
+  "isodefl d t \<Longrightarrow> isodefl (u_map\<cdot>d) (u_typ\<cdot>t)"
+apply (rule isodeflI)
+apply (simp add: cast_u_typ 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)"
+apply (rule isodeflI)
+apply (simp add: cast_upper_typ 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)"
+apply (rule isodeflI)
+apply (simp add: cast_lower_typ 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)"
+apply (rule isodeflI)
+apply (simp add: cast_convex_typ cast_isodefl)
+apply (simp add: emb_convex_pd_def prj_convex_pd_def)
+apply (simp add: convex_map_map)
+done
+
+end
diff -r 488837bf01d7 -r 27f74e853a54 src/HOLCF/Sprod.thy
--- a/src/HOLCF/Sprod.thy	Tue Nov 10 14:20:15 2009 +0100
+++ b/src/HOLCF/Sprod.thy	Tue Nov 10 06:48:26 2009 -0800
@@ -245,6 +245,16 @@
   "x \<noteq> \<bottom> \<Longrightarrow> y \<noteq> \<bottom> \<Longrightarrow> sprod_map\<cdot>f\<cdot>g\<cdot>(:x, y:) = (:f\<cdot>x, g\<cdot>y:)"
 by (simp add: sprod_map_def)
 
+lemma sprod_map_map:
+  "\<lbrakk>f1\<cdot>\<bottom> = \<bottom>; g1\<cdot>\<bottom> = \<bottom>\<rbrakk> \<Longrightarrow>
+    sprod_map\<cdot>f1\<cdot>g1\<cdot>(sprod_map\<cdot>f2\<cdot>g2\<cdot>p) =
+     sprod_map\<cdot>(\<Lambda> x. f1\<cdot>(f2\<cdot>x))\<cdot>(\<Lambda> x. g1\<cdot>(g2\<cdot>x))\<cdot>p"
+apply (induct p, simp)
+apply (case_tac "f2\<cdot>x = \<bottom>", simp)
+apply (case_tac "g2\<cdot>y = \<bottom>", simp)
+apply simp
+done
+
 lemma ep_pair_sprod_map:
   assumes "ep_pair e1 p1" and "ep_pair e2 p2"
   shows "ep_pair (sprod_map\<cdot>e1\<cdot>e2) (sprod_map\<cdot>p1\<cdot>p2)"
diff -r 488837bf01d7 -r 27f74e853a54 src/HOLCF/Ssum.thy
--- a/src/HOLCF/Ssum.thy	Tue Nov 10 14:20:15 2009 +0100
+++ b/src/HOLCF/Ssum.thy	Tue Nov 10 06:48:26 2009 -0800
@@ -226,6 +226,15 @@
 lemma ssum_map_sinr [simp]: "x \<noteq> \<bottom> \<Longrightarrow> ssum_map\<cdot>f\<cdot>g\<cdot>(sinr\<cdot>x) = sinr\<cdot>(g\<cdot>x)"
 unfolding ssum_map_def by simp
 
+lemma ssum_map_map:
+  "\<lbrakk>f1\<cdot>\<bottom> = \<bottom>; g1\<cdot>\<bottom> = \<bottom>\<rbrakk> \<Longrightarrow>
+    ssum_map\<cdot>f1\<cdot>g1\<cdot>(ssum_map\<cdot>f2\<cdot>g2\<cdot>p) =
+     ssum_map\<cdot>(\<Lambda> x. f1\<cdot>(f2\<cdot>x))\<cdot>(\<Lambda> x. g1\<cdot>(g2\<cdot>x))\<cdot>p"
+apply (induct p, simp)
+apply (case_tac "f2\<cdot>x = \<bottom>", simp, simp)
+apply (case_tac "g2\<cdot>y = \<bottom>", simp, simp)
+done
+
 lemma ep_pair_ssum_map:
   assumes "ep_pair e1 p1" and "ep_pair e2 p2"
   shows "ep_pair (ssum_map\<cdot>e1\<cdot>e2) (ssum_map\<cdot>p1\<cdot>p2)"
diff -r 488837bf01d7 -r 27f74e853a54 src/HOLCF/Up.thy
--- a/src/HOLCF/Up.thy	Tue Nov 10 14:20:15 2009 +0100
+++ b/src/HOLCF/Up.thy	Tue Nov 10 06:48:26 2009 -0800
@@ -303,6 +303,9 @@
 lemma u_map_up [simp]: "u_map\<cdot>f\<cdot>(up\<cdot>x) = up\<cdot>(f\<cdot>x)"
 unfolding u_map_def by simp
 
+lemma u_map_map: "u_map\<cdot>f\<cdot>(u_map\<cdot>g\<cdot>p) = u_map\<cdot>(\<Lambda> x. f\<cdot>(g\<cdot>x))\<cdot>p"
+by (induct p) simp_all
+
 lemma ep_pair_u_map: "ep_pair e p \<Longrightarrow> ep_pair (u_map\<cdot>e) (u_map\<cdot>p)"
 apply default
 apply (case_tac x, simp, simp add: ep_pair.e_inverse)
diff -r 488837bf01d7 -r 27f74e853a54 src/HOLCF/UpperPD.thy
--- a/src/HOLCF/UpperPD.thy	Tue Nov 10 14:20:15 2009 +0100
+++ b/src/HOLCF/UpperPD.thy	Tue Nov 10 06:48:26 2009 -0800
@@ -486,4 +486,16 @@
 lemma upper_map_approx: "upper_map\<cdot>(approx n)\<cdot>xs = approx n\<cdot>xs"
 by (induct xs rule: upper_pd_induct, simp_all)
 
+lemma ep_pair_upper_map: "ep_pair e p \<Longrightarrow> ep_pair (upper_map\<cdot>e) (upper_map\<cdot>p)"
+apply default
+apply (induct_tac x rule: upper_pd_induct, simp_all add: ep_pair.e_inverse)
+apply (induct_tac y rule: upper_pd_induct, simp_all add: ep_pair.e_p_below monofun_cfun)
+done
+
+lemma deflation_upper_map: "deflation d \<Longrightarrow> deflation (upper_map\<cdot>d)"
+apply default
+apply (induct_tac x rule: upper_pd_induct, simp_all add: deflation.idem)
+apply (induct_tac x rule: upper_pd_induct, simp_all add: deflation.below monofun_cfun)
+done
+
 end
diff -r 488837bf01d7 -r 27f74e853a54 src/HOLCF/ex/Domain_Proofs.thy
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOLCF/ex/Domain_Proofs.thy	Tue Nov 10 06:48:26 2009 -0800
@@ -0,0 +1,375 @@
+(*  Title:      HOLCF/ex/Domain_Proofs.thy
+    Author:     Brian Huffman
+*)
+
+header {* Internal domain package proofs done manually *}
+
+theory Domain_Proofs
+imports HOLCF
+begin
+
+defaultsort rep
+
+(*
+
+The definitions and proofs below are for the following recursive
+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")
+
+*)
+
+(********************************************************************)
+
+subsection {* Step 1: Define the new type combinators *}
+
+text {* Start with the one-step non-recursive version *}
+
+definition
+  foo_bar_baz_typF ::
+    "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))))"
+
+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)
+
+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 bar_typ :: "TypeRep \<rightarrow> TypeRep"
+where "bar_typ = (\<Lambda> a. fst (snd (fix\<cdot>(foo_bar_baz_typF\<cdot>a))))"
+
+definition baz_typ :: "TypeRep \<rightarrow> TypeRep"
+where "baz_typ = (\<Lambda> a. snd (snd (fix\<cdot>(foo_bar_baz_typF\<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 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 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)
+
+text "The automation for the previous steps will be quite similar to
+how the fixrec package works."
+
+(********************************************************************)
+
+subsection {* Step 2: Define types, prove class instances *}
+
+text {* Use @{text pcpodef} with the appropriate type combinator. *}
+
+pcpodef (open) 'a foo = "{x. x ::: foo_typ\<cdot>REP('a)}"
+by (simp_all add: adm_in_deflation)
+
+pcpodef (open) 'a bar = "{x. x ::: bar_typ\<cdot>REP('a)}"
+by (simp_all add: adm_in_deflation)
+
+pcpodef (open) 'a baz = "{x. x ::: baz_typ\<cdot>REP('a)}"
+by (simp_all add: adm_in_deflation)
+
+text {* Prove rep instance using lemma @{text typedef_rep_class}. *}
+
+instantiation foo :: (rep) rep
+begin
+
+definition emb_foo :: "'a foo \<rightarrow> udom"
+where "emb_foo = (\<Lambda> x. Rep_foo x)"
+
+definition prj_foo :: "udom \<rightarrow> 'a foo"
+where "prj_foo = (\<Lambda> y. Abs_foo (cast\<cdot>(foo_typ\<cdot>REP('a))\<cdot>y))"
+
+definition approx_foo :: "nat \<Rightarrow> 'a foo \<rightarrow> 'a foo"
+where "approx_foo = (\<lambda>i. prj oo cast\<cdot>(approx i\<cdot>(foo_typ\<cdot>REP('a))) oo emb)"
+
+instance
+apply (rule typedef_rep_class)
+apply (rule type_definition_foo)
+apply (rule below_foo_def)
+apply (rule emb_foo_def)
+apply (rule prj_foo_def)
+apply (rule approx_foo_def)
+done
+
+end
+
+instantiation bar :: (rep) rep
+begin
+
+definition emb_bar :: "'a bar \<rightarrow> udom"
+where "emb_bar = (\<Lambda> x. Rep_bar x)"
+
+definition prj_bar :: "udom \<rightarrow> 'a bar"
+where "prj_bar = (\<Lambda> y. Abs_bar (cast\<cdot>(bar_typ\<cdot>REP('a))\<cdot>y))"
+
+definition approx_bar :: "nat \<Rightarrow> 'a bar \<rightarrow> 'a bar"
+where "approx_bar = (\<lambda>i. prj oo cast\<cdot>(approx i\<cdot>(bar_typ\<cdot>REP('a))) oo emb)"
+
+instance
+apply (rule typedef_rep_class)
+apply (rule type_definition_bar)
+apply (rule below_bar_def)
+apply (rule emb_bar_def)
+apply (rule prj_bar_def)
+apply (rule approx_bar_def)
+done
+
+end
+
+instantiation baz :: (rep) rep
+begin
+
+definition emb_baz :: "'a baz \<rightarrow> udom"
+where "emb_baz = (\<Lambda> x. Rep_baz x)"
+
+definition prj_baz :: "udom \<rightarrow> 'a baz"
+where "prj_baz = (\<Lambda> y. Abs_baz (cast\<cdot>(baz_typ\<cdot>REP('a))\<cdot>y))"
+
+definition approx_baz :: "nat \<Rightarrow> 'a baz \<rightarrow> 'a baz"
+where "approx_baz = (\<lambda>i. prj oo cast\<cdot>(approx i\<cdot>(baz_typ\<cdot>REP('a))) oo emb)"
+
+instance
+apply (rule typedef_rep_class)
+apply (rule type_definition_baz)
+apply (rule below_baz_def)
+apply (rule emb_baz_def)
+apply (rule prj_baz_def)
+apply (rule approx_baz_def)
+done
+
+end
+
+text {* Prove REP rules using lemma @{text typedef_REP}. *}
+
+lemma REP_foo: "REP('a foo) = foo_typ\<cdot>REP('a)"
+apply (rule typedef_REP)
+apply (rule type_definition_foo)
+apply (rule below_foo_def)
+apply (rule emb_foo_def)
+apply (rule prj_foo_def)
+done
+
+lemma REP_bar: "REP('a bar) = bar_typ\<cdot>REP('a)"
+apply (rule typedef_REP)
+apply (rule type_definition_bar)
+apply (rule below_bar_def)
+apply (rule emb_bar_def)
+apply (rule prj_bar_def)
+done
+
+lemma REP_baz: "REP('a baz) = baz_typ\<cdot>REP('a)"
+apply (rule typedef_REP)
+apply (rule type_definition_baz)
+apply (rule below_baz_def)
+apply (rule emb_baz_def)
+apply (rule prj_baz_def)
+done
+
+text {* Prove REP equations using type combinator unfold lemmas. *}
+
+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)
+
+lemma REP_bar': "REP('a bar) = REP('a\<^sub>\<bottom> \<otimes> ('a baz)\<^sub>\<bottom>)"
+unfolding REP_foo REP_bar REP_baz REP_simps
+by (rule bar_typ_unfold)
+
+lemma REP_baz': "REP('a baz) = REP('a\<^sub>\<bottom> \<otimes> ('a foo convex_pd)\<^sub>\<bottom>)"
+unfolding REP_foo REP_bar REP_baz REP_simps
+by (rule baz_typ_unfold)
+
+(********************************************************************)
+
+subsection {* Step 3: Define rep and abs functions *}
+
+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"
+
+definition foo_abs :: "one \<oplus> ('a\<^sub>\<bottom> \<otimes> ('a bar)\<^sub>\<bottom>) \<rightarrow> 'a foo"
+where "foo_abs = coerce"
+
+definition bar_rep :: "'a bar \<rightarrow> 'a\<^sub>\<bottom> \<otimes> ('a baz)\<^sub>\<bottom>"
+where "bar_rep = coerce"
+
+definition bar_abs :: "'a\<^sub>\<bottom> \<otimes> ('a baz)\<^sub>\<bottom> \<rightarrow> 'a bar"
+where "bar_abs = coerce"
+
+definition baz_rep :: "'a baz \<rightarrow> 'a\<^sub>\<bottom> \<otimes> ('a foo convex_pd)\<^sub>\<bottom>"
+where "baz_rep = coerce"
+
+definition baz_abs :: "'a\<^sub>\<bottom> \<otimes> ('a foo convex_pd)\<^sub>\<bottom> \<rightarrow> 'a baz"
+where "baz_abs = coerce"
+
+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'])
+
+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'])
+
+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. *}
+
+(********************************************************************)
+
+subsection {* Step 4: Define map functions, prove isodefl property *}
+
+text {* Start with the one-step non-recursive version. *}
+
+text {* Note that the type of the map function depends on which
+variables are used in positive and negative positions. *}
+
+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)"
+where
+  "foo_bar_baz_mapF = (\<Lambda> f (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
+    ,
+      baz_abs oo sprod_map\<cdot>(u_map\<cdot>f)\<cdot>(u_map\<cdot>(convex_map\<cdot>d1)) oo baz_rep
+    ))"
+
+lemma foo_bar_baz_mapF_beta:
+  "foo_bar_baz_mapF\<cdot>f\<cdot>d =
+    (
+      foo_abs oo
+        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
+    ,
+      baz_abs oo sprod_map\<cdot>(u_map\<cdot>f)\<cdot>(u_map\<cdot>(convex_map\<cdot>(fst d))) oo baz_rep
+    )"
+unfolding foo_bar_baz_mapF_def
+by (simp add: csplit_def cfst_def csnd_def)
+
+text {* Individual map functions are projected from the fixed point. *}
+
+definition foo_map :: "('a \<rightarrow> 'b) \<rightarrow> ('a foo \<rightarrow> 'b foo)"
+where "foo_map = (\<Lambda> f. fst (fix\<cdot>(foo_bar_baz_mapF\<cdot>f)))"
+
+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)"
+where "baz_map = (\<Lambda> f. snd (snd (fix\<cdot>(foo_bar_baz_mapF\<cdot>f))))"
+
+text {* Prove isodefl rules for all map functions simultaneously. *}
+
+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)"
+ 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 (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
+                   fst_conv snd_conv)
+ apply (elim conjE)
+ apply (intro
+  conjI
+  isodefl_foo_abs
+  isodefl_bar_abs
+  isodefl_baz_abs
+  isodefl_ssum isodefl_sprod isodefl_one isodefl_u isodefl_convex
+  isodefl_d
+ )
+ apply assumption+
+done
+
+lemmas isodefl_foo = isodefl_foo_bar_baz [THEN conjunct1]
+lemmas isodefl_bar = isodefl_foo_bar_baz [THEN conjunct2, THEN conjunct1]
+lemmas isodefl_baz = isodefl_foo_bar_baz [THEN conjunct2, THEN conjunct2]
+
+text {* Prove map ID lemmas, using isodefl_REP_imp_ID *}
+
+lemma foo_map_ID: "foo_map\<cdot>ID = ID"
+apply (rule isodefl_REP_imp_ID)
+apply (subst REP_foo)
+apply (rule isodefl_foo)
+apply (rule isodefl_ID_REP)
+done
+
+lemma bar_map_ID: "bar_map\<cdot>ID = ID"
+apply (rule isodefl_REP_imp_ID)
+apply (subst REP_bar)
+apply (rule isodefl_bar)
+apply (rule isodefl_ID_REP)
+done
+
+lemma baz_map_ID: "baz_map\<cdot>ID = ID"
+apply (rule isodefl_REP_imp_ID)
+apply (subst REP_baz)
+apply (rule isodefl_baz)
+apply (rule isodefl_ID_REP)
+done
+
+(********************************************************************)
+
+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)))"
+
+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
+
+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)
+
+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)
+
+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)
+
+end
diff -r 488837bf01d7 -r 27f74e853a54 src/HOLCF/ex/ROOT.ML
--- a/src/HOLCF/ex/ROOT.ML	Tue Nov 10 14:20:15 2009 +0100
+++ b/src/HOLCF/ex/ROOT.ML	Tue Nov 10 06:48:26 2009 -0800
@@ -4,4 +4,4 @@
 *)
 
 use_thys ["Dnat", "Stream", "Dagstuhl", "Focus_ex", "Fix2", "Hoare",
-  "Loop", "Fixrec_ex", "Powerdomain_ex", "Domain_ex"];
+  "Loop", "Fixrec_ex", "Powerdomain_ex", "Domain_ex", "Domain_Proofs"];