--- a/src/HOL/HOLCF/Domain.thy Thu Jan 06 21:06:18 2011 +0100
+++ b/src/HOL/HOLCF/Domain.thy Thu Jan 06 16:52:35 2011 -0800
@@ -105,7 +105,7 @@
assumes defl: "defl \<equiv> (\<lambda> a::'a itself. t)"
assumes liftemb: "(liftemb :: 'a u \<rightarrow> udom u) \<equiv> u_map\<cdot>emb"
assumes liftprj: "(liftprj :: udom u \<rightarrow> 'a u) \<equiv> u_map\<cdot>prj"
- assumes liftdefl: "(liftdefl :: 'a itself \<Rightarrow> _) \<equiv> (\<lambda>t. pdefl\<cdot>DEFL('a))"
+ assumes liftdefl: "(liftdefl :: 'a itself \<Rightarrow> _) \<equiv> (\<lambda>t. liftdefl_of\<cdot>DEFL('a))"
shows "OFCLASS('a, domain_class)"
proof
have emb_beta: "\<And>x. emb\<cdot>x = Rep x"
@@ -233,9 +233,9 @@
unfolding isodefl_def
by (simp add: cfun_eq_iff assms prj_emb_prj emb_prj_emb)
-lemma isodefl'_pdefl: "isodefl d t \<Longrightarrow> isodefl' d (pdefl\<cdot>t)"
+lemma isodefl'_liftdefl_of: "isodefl d t \<Longrightarrow> isodefl' d (liftdefl_of\<cdot>t)"
unfolding isodefl_def isodefl'_def
-by (simp add: cast_pdefl u_map_oo liftemb_eq liftprj_eq)
+by (simp add: cast_liftdefl_of u_map_oo liftemb_eq liftprj_eq)
lemma isodefl_sfun:
"isodefl d1 t1 \<Longrightarrow> isodefl d2 t2 \<Longrightarrow>
@@ -326,7 +326,7 @@
lemmas [domain_isodefl] =
isodefl_u isodefl_sfun isodefl_ssum isodefl_sprod
- isodefl_cfun isodefl_prod isodefl_prod_u isodefl'_pdefl
+ isodefl_cfun isodefl_prod isodefl_prod_u isodefl'_liftdefl_of
lemmas [domain_deflation] =
deflation_cfun_map deflation_sfun_map deflation_ssum_map
--- a/src/HOL/HOLCF/Library/Defl_Bifinite.thy Thu Jan 06 21:06:18 2011 +0100
+++ b/src/HOL/HOLCF/Library/Defl_Bifinite.thy Thu Jan 06 16:52:35 2011 -0800
@@ -657,7 +657,7 @@
"(liftprj :: udom u \<rightarrow> 'a defl u) = u_map\<cdot>prj"
definition
- "liftdefl (t::'a defl itself) = pdefl\<cdot>DEFL('a defl)"
+ "liftdefl (t::'a defl itself) = liftdefl_of\<cdot>DEFL('a defl)"
instance proof
show ep: "ep_pair emb (prj :: udom \<rightarrow> 'a defl)"
--- a/src/HOL/HOLCF/Library/Option_Cpo.thy Thu Jan 06 21:06:18 2011 +0100
+++ b/src/HOL/HOLCF/Library/Option_Cpo.thy Thu Jan 06 16:52:35 2011 -0800
@@ -280,7 +280,7 @@
lemma isodefl_option [domain_isodefl]:
assumes "isodefl' d t"
- shows "isodefl' (option_map d) (sum_liftdefl\<cdot>(pdefl\<cdot>DEFL(unit))\<cdot>t)"
+ shows "isodefl' (option_map d) (sum_liftdefl\<cdot>(liftdefl_of\<cdot>DEFL(unit))\<cdot>t)"
using isodefl_sum [OF isodefl_LIFTDEFL [where 'a=unit] assms]
unfolding isodefl'_def liftemb_option_def liftprj_option_def liftdefl_eq
by (simp add: cfcomp1 u_map_map encode_option_option_map)
--- a/src/HOL/HOLCF/Powerdomains.thy Thu Jan 06 21:06:18 2011 +0100
+++ b/src/HOL/HOLCF/Powerdomains.thy Thu Jan 06 16:52:35 2011 -0800
@@ -78,7 +78,7 @@
"(liftprj :: udom u \<rightarrow> 'a upper_pd u) = u_map\<cdot>prj"
definition
- "liftdefl (t::'a upper_pd itself) = pdefl\<cdot>DEFL('a upper_pd)"
+ "liftdefl (t::'a upper_pd itself) = liftdefl_of\<cdot>DEFL('a upper_pd)"
instance proof
show "ep_pair emb (prj :: udom \<rightarrow> 'a upper_pd)"
@@ -111,7 +111,7 @@
"(liftprj :: udom u \<rightarrow> 'a lower_pd u) = u_map\<cdot>prj"
definition
- "liftdefl (t::'a lower_pd itself) = pdefl\<cdot>DEFL('a lower_pd)"
+ "liftdefl (t::'a lower_pd itself) = liftdefl_of\<cdot>DEFL('a lower_pd)"
instance proof
show "ep_pair emb (prj :: udom \<rightarrow> 'a lower_pd)"
@@ -144,7 +144,7 @@
"(liftprj :: udom u \<rightarrow> 'a convex_pd u) = u_map\<cdot>prj"
definition
- "liftdefl (t::'a convex_pd itself) = pdefl\<cdot>DEFL('a convex_pd)"
+ "liftdefl (t::'a convex_pd itself) = liftdefl_of\<cdot>DEFL('a convex_pd)"
instance proof
show "ep_pair emb (prj :: udom \<rightarrow> 'a convex_pd)"
--- a/src/HOL/HOLCF/Representable.thy Thu Jan 06 21:06:18 2011 +0100
+++ b/src/HOL/HOLCF/Representable.thy Thu Jan 06 16:52:35 2011 -0800
@@ -34,11 +34,11 @@
syntax "_LIFTDEFL" :: "type \<Rightarrow> logic" ("(1LIFTDEFL/(1'(_')))")
translations "LIFTDEFL('t)" \<rightleftharpoons> "CONST liftdefl TYPE('t)"
-definition pdefl :: "udom defl \<rightarrow> udom u defl"
- where "pdefl = defl_fun1 ID ID u_map"
+definition liftdefl_of :: "udom defl \<rightarrow> udom u defl"
+ where "liftdefl_of = defl_fun1 ID ID u_map"
-lemma cast_pdefl: "cast\<cdot>(pdefl\<cdot>t) = u_map\<cdot>(cast\<cdot>t)"
-by (simp add: pdefl_def cast_defl_fun1 ep_pair_def finite_deflation_u_map)
+lemma cast_liftdefl_of: "cast\<cdot>(liftdefl_of\<cdot>t) = u_map\<cdot>(cast\<cdot>t)"
+by (simp add: liftdefl_of_def cast_defl_fun1 ep_pair_def finite_deflation_u_map)
class "domain" = predomain_syn + pcpo +
fixes emb :: "'a \<rightarrow> udom"
@@ -48,7 +48,7 @@
assumes cast_DEFL: "cast\<cdot>(defl TYPE('a)) = emb oo prj"
assumes liftemb_eq: "liftemb = u_map\<cdot>emb"
assumes liftprj_eq: "liftprj = u_map\<cdot>prj"
- assumes liftdefl_eq: "liftdefl TYPE('a) = pdefl\<cdot>(defl TYPE('a))"
+ assumes liftdefl_eq: "liftdefl TYPE('a) = liftdefl_of\<cdot>(defl TYPE('a))"
syntax "_DEFL" :: "type \<Rightarrow> logic" ("(1DEFL/(1'(_')))")
translations "DEFL('t)" \<rightleftharpoons> "CONST defl TYPE('t)"
@@ -60,7 +60,7 @@
by (intro ep_pair_u_map ep_pair_emb_prj)
show "cast\<cdot>LIFTDEFL('a) = liftemb oo (liftprj::udom\<^sub>\<bottom> \<rightarrow> 'a\<^sub>\<bottom>)"
unfolding liftemb_eq liftprj_eq liftdefl_eq
- by (simp add: cast_pdefl cast_DEFL u_map_oo)
+ by (simp add: cast_liftdefl_of cast_DEFL u_map_oo)
qed
text {*
@@ -229,7 +229,7 @@
"(liftprj :: udom u \<rightarrow> udom u) = u_map\<cdot>prj"
definition
- "liftdefl (t::udom itself) = pdefl\<cdot>DEFL(udom)"
+ "liftdefl (t::udom itself) = liftdefl_of\<cdot>DEFL(udom)"
instance proof
show "ep_pair emb (prj :: udom \<rightarrow> udom)"
@@ -271,7 +271,7 @@
"(liftprj :: udom u \<rightarrow> 'a u u) = u_map\<cdot>prj"
definition
- "liftdefl (t::'a u itself) = pdefl\<cdot>DEFL('a u)"
+ "liftdefl (t::'a u itself) = liftdefl_of\<cdot>DEFL('a u)"
instance proof
show "ep_pair emb (prj :: udom \<rightarrow> 'a u)"
@@ -308,7 +308,7 @@
"(liftprj :: udom u \<rightarrow> ('a \<rightarrow>! 'b) u) = u_map\<cdot>prj"
definition
- "liftdefl (t::('a \<rightarrow>! 'b) itself) = pdefl\<cdot>DEFL('a \<rightarrow>! 'b)"
+ "liftdefl (t::('a \<rightarrow>! 'b) itself) = liftdefl_of\<cdot>DEFL('a \<rightarrow>! 'b)"
instance proof
show "ep_pair emb (prj :: udom \<rightarrow> 'a \<rightarrow>! 'b)"
@@ -346,7 +346,7 @@
"(liftprj :: udom u \<rightarrow> ('a \<rightarrow> 'b) u) = u_map\<cdot>prj"
definition
- "liftdefl (t::('a \<rightarrow> 'b) itself) = pdefl\<cdot>DEFL('a \<rightarrow> 'b)"
+ "liftdefl (t::('a \<rightarrow> 'b) itself) = liftdefl_of\<cdot>DEFL('a \<rightarrow> 'b)"
instance proof
have "ep_pair encode_cfun decode_cfun"
@@ -386,7 +386,7 @@
"(liftprj :: udom u \<rightarrow> ('a \<otimes> 'b) u) = u_map\<cdot>prj"
definition
- "liftdefl (t::('a \<otimes> 'b) itself) = pdefl\<cdot>DEFL('a \<otimes> 'b)"
+ "liftdefl (t::('a \<otimes> 'b) itself) = liftdefl_of\<cdot>DEFL('a \<otimes> 'b)"
instance proof
show "ep_pair emb (prj :: udom \<rightarrow> 'a \<otimes> 'b)"
@@ -475,9 +475,9 @@
apply (rule cfun_eqI, case_tac x, simp)
apply (rename_tac y, case_tac "prod_prj\<cdot>y", simp)
done
- show 5: "LIFTDEFL('a \<times> 'b) = pdefl\<cdot>DEFL('a \<times> 'b)"
+ show 5: "LIFTDEFL('a \<times> 'b) = liftdefl_of\<cdot>DEFL('a \<times> 'b)"
by (rule cast_eq_imp_eq)
- (simp add: cast_liftdefl cast_pdefl cast_DEFL 2 3 4 u_map_oo)
+ (simp add: cast_liftdefl cast_liftdefl_of cast_DEFL 2 3 4 u_map_oo)
qed
end
@@ -512,7 +512,7 @@
"(liftprj :: udom u \<rightarrow> unit u) = u_map\<cdot>prj"
definition
- "liftdefl (t::unit itself) = pdefl\<cdot>DEFL(unit)"
+ "liftdefl (t::unit itself) = liftdefl_of\<cdot>DEFL(unit)"
instance proof
show "ep_pair emb (prj :: udom \<rightarrow> unit)"
@@ -590,7 +590,7 @@
"(liftprj :: udom u \<rightarrow> ('a \<oplus> 'b) u) = u_map\<cdot>prj"
definition
- "liftdefl (t::('a \<oplus> 'b) itself) = pdefl\<cdot>DEFL('a \<oplus> 'b)"
+ "liftdefl (t::('a \<oplus> 'b) itself) = liftdefl_of\<cdot>DEFL('a \<oplus> 'b)"
instance proof
show "ep_pair emb (prj :: udom \<rightarrow> 'a \<oplus> 'b)"
@@ -628,7 +628,7 @@
"(liftprj :: udom u \<rightarrow> 'a lift u) = u_map\<cdot>prj"
definition
- "liftdefl (t::'a lift itself) = pdefl\<cdot>DEFL('a lift)"
+ "liftdefl (t::'a lift itself) = liftdefl_of\<cdot>DEFL('a lift)"
instance proof
note [simp] = cont_Rep_lift cont_Abs_lift Rep_lift_inverse Abs_lift_inverse
--- a/src/HOL/HOLCF/Tools/domaindef.ML Thu Jan 06 21:06:18 2011 +0100
+++ b/src/HOL/HOLCF/Tools/domaindef.ML Thu Jan 06 16:52:35 2011 -0800
@@ -136,7 +136,7 @@
val liftdefl_eqn =
Logic.mk_equals (liftdefl_const newT,
Abs ("t", Term.itselfT newT,
- mk_capply (@{const pdefl}, defl_const newT $ Logic.mk_type newT)))
+ mk_capply (@{const liftdefl_of}, defl_const newT $ Logic.mk_type newT)))
val name_def = Binding.suffix_name "_def" name
val emb_bind = (Binding.prefix_name "emb_" name_def, [])
--- a/src/HOL/HOLCF/ex/Domain_Proofs.thy Thu Jan 06 21:06:18 2011 +0100
+++ b/src/HOL/HOLCF/ex/Domain_Proofs.thy Thu Jan 06 16:52:35 2011 -0800
@@ -30,15 +30,15 @@
"udom defl \<rightarrow> udom defl \<times> udom defl \<times> udom defl \<rightarrow> udom defl \<times> udom defl \<times> udom defl"
where
"foo_bar_baz_deflF = (\<Lambda> a. Abs_cfun (\<lambda>(t1, t2, t3).
- ( ssum_defl\<cdot>DEFL(one)\<cdot>(sprod_defl\<cdot>(u_defl\<cdot>(pdefl\<cdot>a))\<cdot>(u_defl\<cdot>(pdefl\<cdot>t2)))
- , u_defl\<cdot>(pdefl\<cdot>(sfun_defl\<cdot>(u_defl\<cdot>(pdefl\<cdot>t3))\<cdot>DEFL(tr)))
- , u_defl\<cdot>(pdefl\<cdot>(sfun_defl\<cdot>(u_defl\<cdot>(pdefl\<cdot>(convex_defl\<cdot>t1)))\<cdot>DEFL(tr))))))"
+ ( ssum_defl\<cdot>DEFL(one)\<cdot>(sprod_defl\<cdot>(u_defl\<cdot>(liftdefl_of\<cdot>a))\<cdot>(u_defl\<cdot>(liftdefl_of\<cdot>t2)))
+ , u_defl\<cdot>(liftdefl_of\<cdot>(sfun_defl\<cdot>(u_defl\<cdot>(liftdefl_of\<cdot>t3))\<cdot>DEFL(tr)))
+ , u_defl\<cdot>(liftdefl_of\<cdot>(sfun_defl\<cdot>(u_defl\<cdot>(liftdefl_of\<cdot>(convex_defl\<cdot>t1)))\<cdot>DEFL(tr))))))"
lemma foo_bar_baz_deflF_beta:
"foo_bar_baz_deflF\<cdot>a\<cdot>t =
- ( ssum_defl\<cdot>DEFL(one)\<cdot>(sprod_defl\<cdot>(u_defl\<cdot>(pdefl\<cdot>a))\<cdot>(u_defl\<cdot>(pdefl\<cdot>(fst (snd t)))))
- , u_defl\<cdot>(pdefl\<cdot>(sfun_defl\<cdot>(u_defl\<cdot>(pdefl\<cdot>(snd (snd t))))\<cdot>DEFL(tr)))
- , u_defl\<cdot>(pdefl\<cdot>(sfun_defl\<cdot>(u_defl\<cdot>(pdefl\<cdot>(convex_defl\<cdot>(fst t))))\<cdot>DEFL(tr))))"
+ ( ssum_defl\<cdot>DEFL(one)\<cdot>(sprod_defl\<cdot>(u_defl\<cdot>(liftdefl_of\<cdot>a))\<cdot>(u_defl\<cdot>(liftdefl_of\<cdot>(fst (snd t)))))
+ , u_defl\<cdot>(liftdefl_of\<cdot>(sfun_defl\<cdot>(u_defl\<cdot>(liftdefl_of\<cdot>(snd (snd t))))\<cdot>DEFL(tr)))
+ , u_defl\<cdot>(liftdefl_of\<cdot>(sfun_defl\<cdot>(u_defl\<cdot>(liftdefl_of\<cdot>(convex_defl\<cdot>(fst t))))\<cdot>DEFL(tr))))"
unfolding foo_bar_baz_deflF_def
by (simp add: split_def)
@@ -62,13 +62,13 @@
text {* Unfold rules for each combinator. *}
lemma foo_defl_unfold:
- "foo_defl\<cdot>a = ssum_defl\<cdot>DEFL(one)\<cdot>(sprod_defl\<cdot>(u_defl\<cdot>(pdefl\<cdot>a))\<cdot>(u_defl\<cdot>(pdefl\<cdot>(bar_defl\<cdot>a))))"
+ "foo_defl\<cdot>a = ssum_defl\<cdot>DEFL(one)\<cdot>(sprod_defl\<cdot>(u_defl\<cdot>(liftdefl_of\<cdot>a))\<cdot>(u_defl\<cdot>(liftdefl_of\<cdot>(bar_defl\<cdot>a))))"
unfolding defl_apply_thms by (subst fix_eq, simp add: foo_bar_baz_deflF_beta)
-lemma bar_defl_unfold: "bar_defl\<cdot>a = u_defl\<cdot>(pdefl\<cdot>(sfun_defl\<cdot>(u_defl\<cdot>(pdefl\<cdot>(baz_defl\<cdot>a)))\<cdot>DEFL(tr)))"
+lemma bar_defl_unfold: "bar_defl\<cdot>a = u_defl\<cdot>(liftdefl_of\<cdot>(sfun_defl\<cdot>(u_defl\<cdot>(liftdefl_of\<cdot>(baz_defl\<cdot>a)))\<cdot>DEFL(tr)))"
unfolding defl_apply_thms by (subst fix_eq, simp add: foo_bar_baz_deflF_beta)
-lemma baz_defl_unfold: "baz_defl\<cdot>a = u_defl\<cdot>(pdefl\<cdot>(sfun_defl\<cdot>(u_defl\<cdot>(pdefl\<cdot>(convex_defl\<cdot>(foo_defl\<cdot>a))))\<cdot>DEFL(tr)))"
+lemma baz_defl_unfold: "baz_defl\<cdot>a = u_defl\<cdot>(liftdefl_of\<cdot>(sfun_defl\<cdot>(u_defl\<cdot>(liftdefl_of\<cdot>(convex_defl\<cdot>(foo_defl\<cdot>a))))\<cdot>DEFL(tr)))"
unfolding defl_apply_thms by (subst fix_eq, simp add: foo_bar_baz_deflF_beta)
text "The automation for the previous steps will be quite similar to
@@ -110,7 +110,7 @@
"(liftprj :: udom u \<rightarrow> 'a foo u) \<equiv> u_map\<cdot>prj"
definition
- "liftdefl \<equiv> \<lambda>(t::'a foo itself). pdefl\<cdot>DEFL('a foo)"
+ "liftdefl \<equiv> \<lambda>(t::'a foo itself). liftdefl_of\<cdot>DEFL('a foo)"
instance
apply (rule typedef_domain_class)
@@ -145,7 +145,7 @@
"(liftprj :: udom u \<rightarrow> 'a bar u) \<equiv> u_map\<cdot>prj"
definition
- "liftdefl \<equiv> \<lambda>(t::'a bar itself). pdefl\<cdot>DEFL('a bar)"
+ "liftdefl \<equiv> \<lambda>(t::'a bar itself). liftdefl_of\<cdot>DEFL('a bar)"
instance
apply (rule typedef_domain_class)
@@ -180,7 +180,7 @@
"(liftprj :: udom u \<rightarrow> 'a baz u) \<equiv> u_map\<cdot>prj"
definition
- "liftdefl \<equiv> \<lambda>(t::'a baz itself). pdefl\<cdot>DEFL('a baz)"
+ "liftdefl \<equiv> \<lambda>(t::'a baz itself). liftdefl_of\<cdot>DEFL('a baz)"
instance
apply (rule typedef_domain_class)