--- a/src/HOLCF/Representable.thy Mon Mar 01 11:15:18 2010 -0800
+++ b/src/HOLCF/Representable.thy Mon Mar 01 16:36:25 2010 -0800
@@ -182,15 +182,10 @@
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)"
+ assumes abs_iso: "\<And>x. rep\<cdot>(abs\<cdot>x) = x"
+ assumes rep_iso: "\<And>y. abs\<cdot>(rep\<cdot>y) = y"
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
+by (rule ep_pair.deflation_e_d_p) (simp add: ep_pair.intro assms)
subsection {* Proving a subtype is representable *}