--- a/src/HOLCF/Representable.thy Sun Feb 28 18:33:57 2010 -0800
+++ b/src/HOLCF/Representable.thy Sun Feb 28 19:39:50 2010 -0800
@@ -180,6 +180,18 @@
shows "abs\<cdot>(rep\<cdot>x) = x"
unfolding abs_def rep_def by (simp add: REP [symmetric])
+lemma deflation_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 "deflation d \<Longrightarrow> deflation (abs oo d oo rep)"
+unfolding abs_def rep_def
+apply (rule ep_pair.deflation_e_d_p)
+apply (rule ep_pair_coerce, simp add: REP)
+apply assumption
+done
+
subsection {* Proving a subtype is representable *}