# HG changeset patch
# User huffman
# Date 1258592278 28800
# Node ID b8efeea2cebd2719e39af1e47de3fc6add9b0a76
# Parent  9121ea165a4007acf4aec57ec05a437f9f36c8c2
remove one_typ and tr_typ; add abs/rep lemmas

diff -r 9121ea165a40 -r b8efeea2cebd src/HOLCF/Representable.thy
--- a/src/HOLCF/Representable.thy	Wed Nov 18 16:14:28 2009 -0800
+++ b/src/HOLCF/Representable.thy	Wed Nov 18 16:57:58 2009 -0800
@@ -159,6 +159,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,8 +690,6 @@
           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"
@@ -787,12 +804,6 @@
 
 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)
@@ -859,8 +870,6 @@
 done
 
 lemmas REP_simps =
-  REP_one
-  REP_tr
   REP_cfun
   REP_ssum
   REP_sprod
@@ -944,6 +953,14 @@
 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)"
@@ -979,12 +996,6 @@
 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)
diff -r 9121ea165a40 -r b8efeea2cebd src/HOLCF/ex/Domain_Proofs.thy
--- a/src/HOLCF/ex/Domain_Proofs.thy	Wed Nov 18 16:14:28 2009 -0800
+++ b/src/HOLCF/ex/Domain_Proofs.thy	Wed Nov 18 16:57:58 2009 -0800
@@ -32,13 +32,13 @@
     "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))
+    ( ssum_typ\<cdot>REP(one)\<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))))
+    ( ssum_typ\<cdot>REP(one)\<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
@@ -58,7 +58,7 @@
 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)))"
+  "foo_typ\<cdot>a = ssum_typ\<cdot>REP(one)\<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)
 
@@ -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\<^sub>\<bottom> \<otimes> ('a baz)\<^sub>\<bottom>"
-where "bar_rep = coerce"
+where "bar_rep \<equiv> coerce"
 
 definition bar_abs :: "'a\<^sub>\<bottom> \<otimes> ('a baz)\<^sub>\<bottom> \<rightarrow> 'a bar"
-where "bar_abs = coerce"
+where "bar_abs \<equiv> coerce"
 
 definition baz_rep :: "'a baz \<rightarrow> 'a\<^sub>\<bottom> \<otimes> ('a foo convex_pd)\<^sub>\<bottom>"
-where "baz_rep = coerce"
+where "baz_rep \<equiv> coerce"
 
 definition baz_abs :: "'a\<^sub>\<bottom> \<otimes> ('a foo convex_pd)\<^sub>\<bottom> \<rightarrow> 'a baz"
-where "baz_abs = coerce"
+where "baz_abs \<equiv> coerce"
+
+text {* Prove isomorphism rules. *}
+
+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])
+
+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])
+
+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])
 
 (********************************************************************)
 
@@ -316,7 +331,7 @@
   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_d
  )
  apply assumption+