src/HOLCF/Representable.thy

  apply (rule below_trans)
   apply (rule monofun_cfun_arg)
   apply (rule emb_prj_below)
  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 {*
   Temporarily relax type constraints for @{term "approx"},

       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"

 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: 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

 unfolding isodefl_def
 apply (simp add: expand_cfun_eq)
 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)"
 apply (rule isodeflI)
 apply (simp add: cast_cfun_typ cast_isodefl)

 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)