--- a/src/HOLCF/Representable.thy Tue Oct 19 07:05:04 2010 -0700
+++ b/src/HOLCF/Representable.thy Tue Oct 19 10:13:29 2010 -0700
@@ -18,80 +18,25 @@
lemma emb_prj: "emb\<cdot>((prj\<cdot>x)::'a) = cast\<cdot>DEFL('a)\<cdot>x"
by (simp add: cast_DEFL)
-lemma in_DEFL_iff:
- "x ::: DEFL('a) \<longleftrightarrow> emb\<cdot>((prj\<cdot>x)::'a) = x"
-by (simp add: in_defl_def cast_DEFL)
-
-lemma prj_inverse:
- "x ::: DEFL('a) \<Longrightarrow> emb\<cdot>((prj\<cdot>x)::'a) = x"
-by (simp only: in_DEFL_iff)
-
-lemma emb_in_DEFL [simp]:
- "emb\<cdot>(x::'a) ::: DEFL('a)"
-by (simp add: in_DEFL_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 cfun_eqI, simp add: beta_coerce)
-
-lemma emb_coerce:
- "DEFL('a) \<sqsubseteq> DEFL('b)
- \<Longrightarrow> emb\<cdot>((coerce::'a \<rightarrow> 'b)\<cdot>x) = emb\<cdot>x"
- apply (simp add: beta_coerce)
- apply (rule prj_inverse)
- apply (erule defl_belowD)
- apply (rule emb_in_DEFL)
+lemma emb_prj_emb:
+ fixes x :: "'a"
+ assumes "DEFL('a) \<sqsubseteq> DEFL('b)"
+ shows "emb\<cdot>(prj\<cdot>(emb\<cdot>x) :: 'b) = emb\<cdot>x"
+unfolding emb_prj
+apply (rule cast.belowD)
+apply (rule monofun_cfun_arg [OF assms])
+apply (simp add: cast_DEFL)
done
-lemma coerce_prj:
- "DEFL('a) \<sqsubseteq> DEFL('b)
- \<Longrightarrow> (coerce::'b \<rightarrow> 'a)\<cdot>(prj\<cdot>x) = prj\<cdot>x"
- apply (simp add: coerce_def)
+lemma prj_emb_prj:
+ assumes "DEFL('a) \<sqsubseteq> DEFL('b)"
+ shows "prj\<cdot>(emb\<cdot>(prj\<cdot>x :: 'b)) = (prj\<cdot>x :: 'a)"
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]:
- "DEFL('a) \<sqsubseteq> DEFL('b)
- \<Longrightarrow> coerce\<cdot>((coerce::'a \<rightarrow> 'b)\<cdot>x) = coerce\<cdot>x"
-by (simp add: beta_coerce prj_inverse defl_belowD)
-
-lemma coerce_inverse:
- "emb\<cdot>(x::'a) ::: DEFL('b) \<Longrightarrow> coerce\<cdot>(coerce\<cdot>x :: 'b) = x"
-by (simp only: beta_coerce prj_inverse emb_inverse)
-
-lemma coerce_type:
- "DEFL('a) \<sqsubseteq> DEFL('b)
- \<Longrightarrow> emb\<cdot>((coerce::'a \<rightarrow> 'b)\<cdot>x) ::: DEFL('a)"
-by (simp add: beta_coerce prj_inverse defl_belowD)
-
-lemma ep_pair_coerce:
- "DEFL('a) \<sqsubseteq> DEFL('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
+ apply (rule monofun_cfun_arg [OF assms])
done
text {* Isomorphism lemmas used internally by the domain package: *}
@@ -99,34 +44,33 @@
lemma domain_abs_iso:
fixes abs and rep
assumes DEFL: "DEFL('b) = DEFL('a)"
- assumes abs_def: "abs \<equiv> (coerce :: 'a \<rightarrow> 'b)"
- assumes rep_def: "rep \<equiv> (coerce :: 'b \<rightarrow> 'a)"
+ assumes abs_def: "(abs :: 'a \<rightarrow> 'b) \<equiv> prj oo emb"
+ assumes rep_def: "(rep :: 'b \<rightarrow> 'a) \<equiv> prj oo emb"
shows "rep\<cdot>(abs\<cdot>x) = x"
-unfolding abs_def rep_def by (simp add: DEFL)
+unfolding abs_def rep_def
+by (simp add: emb_prj_emb DEFL)
lemma domain_rep_iso:
fixes abs and rep
assumes DEFL: "DEFL('b) = DEFL('a)"
- assumes abs_def: "abs \<equiv> (coerce :: 'a \<rightarrow> 'b)"
- assumes rep_def: "rep \<equiv> (coerce :: 'b \<rightarrow> 'a)"
+ assumes abs_def: "(abs :: 'a \<rightarrow> 'b) \<equiv> prj oo emb"
+ assumes rep_def: "(rep :: 'b \<rightarrow> 'a) \<equiv> prj oo emb"
shows "abs\<cdot>(rep\<cdot>x) = x"
-unfolding abs_def rep_def by (simp add: DEFL [symmetric])
-
+unfolding abs_def rep_def
+by (simp add: emb_prj_emb DEFL)
subsection {* Proving a subtype is representable *}
text {*
- Temporarily relax type constraints for @{term emb}, and @{term prj}.
+ Temporarily relax type constraints for @{term emb} and @{term prj}.
*}
-setup {* Sign.add_const_constraint
- (@{const_name defl}, SOME @{typ "'a::pcpo itself \<Rightarrow> defl"}) *}
-
-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"}) *}
+setup {*
+ fold Sign.add_const_constraint
+ [ (@{const_name defl}, SOME @{typ "'a::pcpo itself \<Rightarrow> defl"})
+ , (@{const_name emb}, SOME @{typ "'a::pcpo \<rightarrow> udom"})
+ , (@{const_name prj}, SOME @{typ "udom \<rightarrow> 'a::pcpo"}) ]
+*}
lemma typedef_rep_class:
fixes Rep :: "'a::pcpo \<Rightarrow> udom"
@@ -177,16 +121,14 @@
shows "DEFL('a::pcpo) = t"
unfolding assms ..
-text {* Restore original typing constraints *}
-
-setup {* Sign.add_const_constraint
- (@{const_name defl}, SOME @{typ "'a::bifinite itself \<Rightarrow> defl"}) *}
+text {* Restore original typing constraints. *}
-setup {* Sign.add_const_constraint
- (@{const_name emb}, SOME @{typ "'a::bifinite \<rightarrow> udom"}) *}
-
-setup {* Sign.add_const_constraint
- (@{const_name prj}, SOME @{typ "udom \<rightarrow> 'a::bifinite"}) *}
+setup {*
+ fold Sign.add_const_constraint
+ [ (@{const_name defl}, SOME @{typ "'a::bifinite itself \<Rightarrow> defl"})
+ , (@{const_name emb}, SOME @{typ "'a::bifinite \<rightarrow> udom"})
+ , (@{const_name prj}, SOME @{typ "udom \<rightarrow> 'a::bifinite"}) ]
+*}
lemma adm_mem_Collect_in_defl: "adm (\<lambda>x. x \<in> {x. x ::: A})"
unfolding mem_Collect_eq by (rule adm_in_defl)
@@ -258,22 +200,14 @@
apply (simp add: assms)
done
-lemma isodefl_coerce:
- fixes d :: "'a \<rightarrow> 'a"
- assumes DEFL: "DEFL('b) = DEFL('a)"
- shows "isodefl d t \<Longrightarrow> isodefl (coerce oo d oo coerce :: 'b \<rightarrow> 'b) t"
-unfolding isodefl_def
-apply (simp add: cfun_eq_iff)
-apply (simp add: emb_coerce coerce_prj DEFL)
-done
-
lemma isodefl_abs_rep:
fixes abs and rep and d
assumes DEFL: "DEFL('b) = DEFL('a)"
- assumes abs_def: "abs \<equiv> (coerce :: 'a \<rightarrow> 'b)"
- assumes rep_def: "rep \<equiv> (coerce :: 'b \<rightarrow> 'a)"
+ assumes abs_def: "(abs :: 'a \<rightarrow> 'b) \<equiv> prj oo emb"
+ assumes rep_def: "(rep :: 'b \<rightarrow> 'a) \<equiv> prj oo emb"
shows "isodefl d t \<Longrightarrow> isodefl (abs oo d oo rep) t"
-unfolding abs_def rep_def using DEFL by (rule isodefl_coerce)
+unfolding isodefl_def
+by (simp add: cfun_eq_iff assms prj_emb_prj emb_prj_emb)
lemma isodefl_cfun:
"isodefl d1 t1 \<Longrightarrow> isodefl d2 t2 \<Longrightarrow>
--- a/src/HOLCF/Tools/Domain/domain_isomorphism.ML Tue Oct 19 07:05:04 2010 -0700
+++ b/src/HOLCF/Tools/Domain/domain_isomorphism.ML Tue Oct 19 10:13:29 2010 -0700
@@ -104,6 +104,7 @@
infixr 6 ->>;
infix -->>;
+val udomT = @{typ udom};
val deflT = @{typ "defl"};
fun mapT (T as Type (_, Ts)) =
@@ -113,7 +114,9 @@
fun mk_DEFL T =
Const (@{const_name defl}, Term.itselfT T --> deflT) $ Logic.mk_type T;
-fun coerce_const T = Const (@{const_name coerce}, T);
+fun emb_const T = Const (@{const_name emb}, T ->> udomT);
+fun prj_const T = Const (@{const_name prj}, udomT ->> T);
+fun coerce_const (T, U) = mk_cfcomp (prj_const U, emb_const T);
fun isodefl_const T =
Const (@{const_name isodefl}, (T ->> T) --> deflT --> HOLogic.boolT);
@@ -505,9 +508,9 @@
val rep_bind = Binding.suffix_name "_rep" tbind;
val abs_bind = Binding.suffix_name "_abs" tbind;
val ((rep_const, rep_def), thy) =
- define_const (rep_bind, coerce_const (lhsT ->> rhsT)) thy;
+ define_const (rep_bind, coerce_const (lhsT, rhsT)) thy;
val ((abs_const, abs_def), thy) =
- define_const (abs_bind, coerce_const (rhsT ->> lhsT)) thy;
+ define_const (abs_bind, coerce_const (rhsT, lhsT)) thy;
in
(((rep_const, abs_const), (rep_def, abs_def)), thy)
end;
--- a/src/HOLCF/ex/Domain_Proofs.thy Tue Oct 19 07:05:04 2010 -0700
+++ b/src/HOLCF/ex/Domain_Proofs.thy Tue Oct 19 10:13:29 2010 -0700
@@ -200,25 +200,25 @@
subsection {* Step 3: Define rep and abs functions *}
-text {* Define them all using @{text coerce}! *}
+text {* Define them all using @{text prj} and @{text emb}! *}
definition foo_rep :: "'a foo \<rightarrow> one \<oplus> ('a\<^sub>\<bottom> \<otimes> ('a bar)\<^sub>\<bottom>)"
-where "foo_rep \<equiv> coerce"
+where "foo_rep \<equiv> prj oo emb"
definition foo_abs :: "one \<oplus> ('a\<^sub>\<bottom> \<otimes> ('a bar)\<^sub>\<bottom>) \<rightarrow> 'a foo"
-where "foo_abs \<equiv> coerce"
+where "foo_abs \<equiv> prj oo emb"
definition bar_rep :: "'a bar \<rightarrow> ('a baz \<rightarrow> tr)\<^sub>\<bottom>"
-where "bar_rep \<equiv> coerce"
+where "bar_rep \<equiv> prj oo emb"
definition bar_abs :: "('a baz \<rightarrow> tr)\<^sub>\<bottom> \<rightarrow> 'a bar"
-where "bar_abs \<equiv> coerce"
+where "bar_abs \<equiv> prj oo emb"
definition baz_rep :: "'a baz \<rightarrow> ('a foo convex_pd \<rightarrow> tr)\<^sub>\<bottom>"
-where "baz_rep \<equiv> coerce"
+where "baz_rep \<equiv> prj oo emb"
definition baz_abs :: "('a foo convex_pd \<rightarrow> tr)\<^sub>\<bottom> \<rightarrow> 'a baz"
-where "baz_abs \<equiv> coerce"
+where "baz_abs \<equiv> prj oo emb"
text {* Prove isomorphism rules. *}