--- a/src/HOLCF/Bifinite.thy Wed Nov 10 06:02:37 2010 -0800
+++ b/src/HOLCF/Bifinite.thy Wed Nov 10 08:18:32 2010 -0800
@@ -28,8 +28,8 @@
translations "LIFTDEFL('t)" \<rightleftharpoons> "CONST liftdefl TYPE('t)"
class bifinite = predomain + pcpo +
- fixes emb :: "'a::pcpo \<rightarrow> udom"
- fixes prj :: "udom \<rightarrow> 'a::pcpo"
+ fixes emb :: "'a::cpo \<rightarrow> udom"
+ fixes prj :: "udom \<rightarrow> 'a::cpo"
fixes defl :: "'a itself \<Rightarrow> defl"
assumes ep_pair_emb_prj: "ep_pair emb prj"
assumes cast_DEFL: "cast\<cdot>(defl TYPE('a)) = emb oo prj"
@@ -256,6 +256,16 @@
subsection {* Lemma for proving bifinite instances *}
+text {*
+ A class of bifinite domains where @{const liftemb}, @{const liftprj},
+ and @{const liftdefl} are all defined in the standard way.
+*}
+
+class liftdomain = bifinite +
+ assumes liftemb_eq: "liftemb = udom_emb u_approx oo u_map\<cdot>emb"
+ assumes liftprj_eq: "liftprj = u_map\<cdot>prj oo udom_prj u_approx"
+ assumes liftdefl_eq: "liftdefl TYPE('a::cpo) = u_defl\<cdot>DEFL('a)"
+
text {* Temporarily relax type constraints. *}
setup {*
@@ -268,13 +278,13 @@
, (@{const_name liftprj}, SOME @{typ "udom \<rightarrow> 'a::pcpo u"}) ]
*}
-lemma bifinite_class_intro:
+lemma liftdomain_class_intro:
assumes liftemb: "(liftemb :: 'a u \<rightarrow> udom) = udom_emb u_approx oo u_map\<cdot>emb"
assumes liftprj: "(liftprj :: udom \<rightarrow> 'a u) = u_map\<cdot>prj oo udom_prj u_approx"
assumes liftdefl: "liftdefl TYPE('a) = u_defl\<cdot>DEFL('a)"
assumes ep_pair: "ep_pair emb (prj :: udom \<rightarrow> 'a)"
assumes cast_defl: "cast\<cdot>DEFL('a) = emb oo (prj :: udom \<rightarrow> 'a)"
- shows "OFCLASS('a, bifinite_class)"
+ shows "OFCLASS('a, liftdomain_class)"
proof
show "ep_pair liftemb (liftprj :: udom \<rightarrow> 'a u)"
unfolding liftemb liftprj
@@ -282,6 +292,7 @@
show "cast\<cdot>LIFTDEFL('a) = liftemb oo (liftprj :: udom \<rightarrow> 'a u)"
unfolding liftemb liftprj liftdefl
by (simp add: cfcomp1 cast_u_defl cast_defl u_map_map)
+next
qed fact+
text {* Restore original type constraints. *}
@@ -298,7 +309,7 @@
subsection {* The universal domain is bifinite *}
-instantiation udom :: bifinite
+instantiation udom :: liftdomain
begin
definition [simp]:
@@ -321,7 +332,7 @@
instance
using liftemb_udom_def liftprj_udom_def liftdefl_udom_def
-proof (rule bifinite_class_intro)
+proof (rule liftdomain_class_intro)
show "ep_pair emb (prj :: udom \<rightarrow> udom)"
by (simp add: ep_pair.intro)
show "cast\<cdot>DEFL(udom) = emb oo (prj :: udom \<rightarrow> udom)"
@@ -342,7 +353,7 @@
subsection {* Lifted predomains are bifinite *}
-instantiation u :: (predomain) bifinite
+instantiation u :: (predomain) liftdomain
begin
definition
@@ -365,7 +376,7 @@
instance
using liftemb_u_def liftprj_u_def liftdefl_u_def
-proof (rule bifinite_class_intro)
+proof (rule liftdomain_class_intro)
show "ep_pair emb (prj :: udom \<rightarrow> 'a u)"
unfolding emb_u_def prj_u_def
by (rule predomain_ep)
@@ -379,12 +390,9 @@
lemma DEFL_u: "DEFL('a::predomain u) = LIFTDEFL('a)"
by (rule defl_u_def)
-lemma LIFTDEFL_u: "LIFTDEFL('a::predomain u) = u_defl\<cdot>DEFL('a u)"
-by (rule liftdefl_u_def)
-
subsection {* Continuous function space is a bifinite domain *}
-instantiation cfun :: (bifinite, bifinite) bifinite
+instantiation cfun :: (bifinite, bifinite) liftdomain
begin
definition
@@ -407,7 +415,7 @@
instance
using liftemb_cfun_def liftprj_cfun_def liftdefl_cfun_def
-proof (rule bifinite_class_intro)
+proof (rule liftdomain_class_intro)
show "ep_pair emb (prj :: udom \<rightarrow> 'a \<rightarrow> 'b)"
unfolding emb_cfun_def prj_cfun_def
using ep_pair_udom [OF cfun_approx]
@@ -423,10 +431,6 @@
"DEFL('a::bifinite \<rightarrow> 'b::bifinite) = cfun_defl\<cdot>DEFL('a)\<cdot>DEFL('b)"
by (rule defl_cfun_def)
-lemma LIFTDEFL_cfun:
- "LIFTDEFL('a::bifinite \<rightarrow> 'b::bifinite) = u_defl\<cdot>DEFL('a \<rightarrow> 'b)"
-by (rule liftdefl_cfun_def)
-
subsection {* Cartesian product is a bifinite domain *}
text {*
@@ -515,7 +519,7 @@
subsection {* Strict product is a bifinite domain *}
-instantiation sprod :: (bifinite, bifinite) bifinite
+instantiation sprod :: (bifinite, bifinite) liftdomain
begin
definition
@@ -538,7 +542,7 @@
instance
using liftemb_sprod_def liftprj_sprod_def liftdefl_sprod_def
-proof (rule bifinite_class_intro)
+proof (rule liftdomain_class_intro)
show "ep_pair emb (prj :: udom \<rightarrow> 'a \<otimes> 'b)"
unfolding emb_sprod_def prj_sprod_def
using ep_pair_udom [OF sprod_approx]
@@ -555,10 +559,6 @@
"DEFL('a::bifinite \<otimes> 'b::bifinite) = sprod_defl\<cdot>DEFL('a)\<cdot>DEFL('b)"
by (rule defl_sprod_def)
-lemma LIFTDEFL_sprod:
- "LIFTDEFL('a::bifinite \<otimes> 'b::bifinite) = u_defl\<cdot>DEFL('a \<otimes> 'b)"
-by (rule liftdefl_sprod_def)
-
subsection {* Countable discrete cpos are predomains *}
definition discr_approx :: "nat \<Rightarrow> 'a::countable discr u \<rightarrow> 'a discr u"
@@ -650,7 +650,7 @@
subsection {* Strict sum is a bifinite domain *}
-instantiation ssum :: (bifinite, bifinite) bifinite
+instantiation ssum :: (bifinite, bifinite) liftdomain
begin
definition
@@ -673,7 +673,7 @@
instance
using liftemb_ssum_def liftprj_ssum_def liftdefl_ssum_def
-proof (rule bifinite_class_intro)
+proof (rule liftdomain_class_intro)
show "ep_pair emb (prj :: udom \<rightarrow> 'a \<oplus> 'b)"
unfolding emb_ssum_def prj_ssum_def
using ep_pair_udom [OF ssum_approx]
@@ -689,13 +689,9 @@
"DEFL('a::bifinite \<oplus> 'b::bifinite) = ssum_defl\<cdot>DEFL('a)\<cdot>DEFL('b)"
by (rule defl_ssum_def)
-lemma LIFTDEFL_ssum:
- "LIFTDEFL('a::bifinite \<oplus> 'b::bifinite) = u_defl\<cdot>DEFL('a \<oplus> 'b)"
-by (rule liftdefl_ssum_def)
-
subsection {* Lifted countable types are bifinite domains *}
-instantiation lift :: (countable) bifinite
+instantiation lift :: (countable) liftdomain
begin
definition
@@ -718,7 +714,7 @@
instance
using liftemb_lift_def liftprj_lift_def liftdefl_lift_def
-proof (rule bifinite_class_intro)
+proof (rule liftdomain_class_intro)
note [simp] = cont_Rep_lift cont_Abs_lift Rep_lift_inverse Abs_lift_inverse
have "ep_pair (\<Lambda>(x::'a lift). Rep_lift x) (\<Lambda> y. Abs_lift y)"
by (simp add: ep_pair_def)
--- a/src/HOLCF/ConvexPD.thy Wed Nov 10 06:02:37 2010 -0800
+++ b/src/HOLCF/ConvexPD.thy Wed Nov 10 08:18:32 2010 -0800
@@ -460,7 +460,7 @@
using convex_approx finite_deflation_convex_map
unfolding convex_defl_def by (rule cast_defl_fun1)
-instantiation convex_pd :: (bifinite) bifinite
+instantiation convex_pd :: (bifinite) liftdomain
begin
definition
@@ -483,7 +483,7 @@
instance
using liftemb_convex_pd_def liftprj_convex_pd_def liftdefl_convex_pd_def
-proof (rule bifinite_class_intro)
+proof (rule liftdomain_class_intro)
show "ep_pair emb (prj :: udom \<rightarrow> 'a convex_pd)"
unfolding emb_convex_pd_def prj_convex_pd_def
using ep_pair_udom [OF convex_approx]
--- a/src/HOLCF/Library/Defl_Bifinite.thy Wed Nov 10 06:02:37 2010 -0800
+++ b/src/HOLCF/Library/Defl_Bifinite.thy Wed Nov 10 08:18:32 2010 -0800
@@ -609,7 +609,7 @@
subsection {* Algebraic deflations are a bifinite domain *}
-instantiation defl :: bifinite
+instantiation defl :: liftdomain
begin
definition
@@ -633,7 +633,7 @@
instance
using liftemb_defl_def liftprj_defl_def liftdefl_defl_def
-proof (rule bifinite_class_intro)
+proof (rule liftdomain_class_intro)
show ep: "ep_pair emb (prj :: udom \<rightarrow> defl)"
unfolding emb_defl_def prj_defl_def
by (rule ep_pair_udom [OF defl_approx])
--- a/src/HOLCF/Library/Strict_Fun.thy Wed Nov 10 06:02:37 2010 -0800
+++ b/src/HOLCF/Library/Strict_Fun.thy Wed Nov 10 08:18:32 2010 -0800
@@ -173,7 +173,7 @@
apply (erule (1) finite_deflation_sfun_map)
done
-instantiation sfun :: (bifinite, bifinite) bifinite
+instantiation sfun :: (bifinite, bifinite) liftdomain
begin
definition
@@ -196,7 +196,7 @@
instance
using liftemb_sfun_def liftprj_sfun_def liftdefl_sfun_def
-proof (rule bifinite_class_intro)
+proof (rule liftdomain_class_intro)
show "ep_pair emb (prj :: udom \<rightarrow> 'a \<rightarrow>! 'b)"
unfolding emb_sfun_def prj_sfun_def
using ep_pair_udom [OF sfun_approx]
--- a/src/HOLCF/LowerPD.thy Wed Nov 10 06:02:37 2010 -0800
+++ b/src/HOLCF/LowerPD.thy Wed Nov 10 08:18:32 2010 -0800
@@ -453,7 +453,7 @@
using lower_approx finite_deflation_lower_map
unfolding lower_defl_def by (rule cast_defl_fun1)
-instantiation lower_pd :: (bifinite) bifinite
+instantiation lower_pd :: (bifinite) liftdomain
begin
definition
@@ -476,7 +476,7 @@
instance
using liftemb_lower_pd_def liftprj_lower_pd_def liftdefl_lower_pd_def
-proof (rule bifinite_class_intro)
+proof (rule liftdomain_class_intro)
show "ep_pair emb (prj :: udom \<rightarrow> 'a lower_pd)"
unfolding emb_lower_pd_def prj_lower_pd_def
using ep_pair_udom [OF lower_approx]
--- a/src/HOLCF/Representable.thy Wed Nov 10 06:02:37 2010 -0800
+++ b/src/HOLCF/Representable.thy Wed Nov 10 08:18:32 2010 -0800
@@ -104,10 +104,10 @@
assumes liftemb: "(liftemb :: 'a u \<rightarrow> udom) \<equiv> udom_emb u_approx oo u_map\<cdot>emb"
assumes liftprj: "(liftprj :: udom \<rightarrow> 'a u) \<equiv> u_map\<cdot>prj oo udom_prj u_approx"
assumes liftdefl: "(liftdefl :: 'a itself \<Rightarrow> defl) \<equiv> (\<lambda>t. u_defl\<cdot>DEFL('a))"
- shows "OFCLASS('a, bifinite_class)"
+ shows "OFCLASS('a, liftdomain_class)"
using liftemb [THEN meta_eq_to_obj_eq]
using liftprj [THEN meta_eq_to_obj_eq]
-proof (rule bifinite_class_intro)
+proof (rule liftdomain_class_intro)
have emb_beta: "\<And>x. emb\<cdot>x = Rep x"
unfolding emb
apply (rule beta_cfun)
@@ -142,11 +142,6 @@
shows "DEFL('a::pcpo) = t"
unfolding assms ..
-lemma typedef_LIFTDEFL:
- assumes "liftdefl \<equiv> (\<lambda>a::'a::pcpo itself. u_defl\<cdot>DEFL('a))"
- shows "LIFTDEFL('a::pcpo) = u_defl\<cdot>DEFL('a)"
-unfolding assms ..
-
text {* Restore original typing constraints. *}
setup {*
@@ -277,27 +272,14 @@
done
lemma isodefl_u:
- assumes "(liftemb :: 'a u \<rightarrow> udom) = udom_emb u_approx oo u_map\<cdot>emb"
- assumes "(liftprj :: udom \<rightarrow> 'a u) = u_map\<cdot>prj oo udom_prj u_approx"
+ fixes d :: "'a::liftdomain \<rightarrow> 'a"
shows "isodefl (d :: 'a \<rightarrow> 'a) t \<Longrightarrow> isodefl (u_map\<cdot>d) (u_defl\<cdot>t)"
apply (rule isodeflI)
apply (simp add: cast_u_defl cast_isodefl)
-apply (simp add: emb_u_def prj_u_def assms)
+apply (simp add: emb_u_def prj_u_def liftemb_eq liftprj_eq)
apply (simp add: u_map_map)
done
-lemma isodefl_u_u:
- assumes "isodefl (u_map\<cdot>d) (u_defl\<cdot>t)"
- shows "isodefl (u_map\<cdot>(u_map\<cdot>d)) (u_defl\<cdot>(u_defl\<cdot>t))"
-using liftemb_u_def liftprj_u_def assms
-by (rule isodefl_u)
-
-lemma isodefl_cfun_u:
- assumes "isodefl d1 t1" and "isodefl d2 t2"
- shows "isodefl (u_map\<cdot>(cfun_map\<cdot>d1\<cdot>d2)) (u_defl\<cdot>(cfun_defl\<cdot>t1\<cdot>t2))"
-using liftemb_cfun_def liftprj_cfun_def isodefl_cfun [OF assms]
-by (rule isodefl_u)
-
lemma encode_prod_u_map:
"encode_prod_u\<cdot>(u_map\<cdot>(cprod_map\<cdot>f\<cdot>g)\<cdot>(decode_prod_u\<cdot>x))
= sprod_map\<cdot>(u_map\<cdot>f)\<cdot>(u_map\<cdot>g)\<cdot>x"
@@ -315,18 +297,6 @@
apply (simp add: cfcomp1 encode_prod_u_map cast_sprod_defl sprod_map_map)
done
-lemma isodefl_sprod_u:
- assumes "isodefl d1 t1" and "isodefl d2 t2"
- shows "isodefl (u_map\<cdot>(sprod_map\<cdot>d1\<cdot>d2)) (u_defl\<cdot>(sprod_defl\<cdot>t1\<cdot>t2))"
-using liftemb_sprod_def liftprj_sprod_def isodefl_sprod [OF assms]
-by (rule isodefl_u)
-
-lemma isodefl_ssum_u:
- assumes "isodefl d1 t1" and "isodefl d2 t2"
- shows "isodefl (u_map\<cdot>(ssum_map\<cdot>d1\<cdot>d2)) (u_defl\<cdot>(ssum_defl\<cdot>t1\<cdot>t2))"
-using liftemb_ssum_def liftprj_ssum_def isodefl_ssum [OF assms]
-by (rule isodefl_u)
-
subsection {* Constructing Domain Isomorphisms *}
use "Tools/Domain/domain_isomorphism.ML"
@@ -335,14 +305,14 @@
lemmas [domain_defl_simps] =
DEFL_cfun DEFL_ssum DEFL_sprod DEFL_prod DEFL_u
- LIFTDEFL_cfun LIFTDEFL_ssum LIFTDEFL_sprod LIFTDEFL_prod LIFTDEFL_u
+ liftdefl_eq LIFTDEFL_prod
lemmas [domain_map_ID] =
cfun_map_ID ssum_map_ID sprod_map_ID cprod_map_ID u_map_ID
lemmas [domain_isodefl] =
- isodefl_cfun isodefl_ssum isodefl_sprod isodefl_cprod isodefl_u_u
- isodefl_cfun_u isodefl_ssum_u isodefl_sprod_u isodefl_cprod_u
+ isodefl_u isodefl_cfun isodefl_ssum isodefl_sprod
+ isodefl_cprod isodefl_cprod_u
lemmas [domain_deflation] =
deflation_cfun_map deflation_ssum_map deflation_sprod_map
--- a/src/HOLCF/Tools/Domain/domain_isomorphism.ML Wed Nov 10 06:02:37 2010 -0800
+++ b/src/HOLCF/Tools/Domain/domain_isomorphism.ML Wed Nov 10 08:18:32 2010 -0800
@@ -522,19 +522,10 @@
fun make_repdef ((vs, tbind, mx, _, _), defl) thy =
let
val spec = (tbind, map (rpair dummyS) vs, mx);
- val ((_, _, _, {DEFL, LIFTDEFL, liftemb_def, liftprj_def, ...}), thy) =
+ val ((_, _, _, {DEFL, liftemb_def, liftprj_def, ...}), thy) =
Repdef.add_repdef false NONE spec defl NONE thy;
(* declare domain_defl_simps rules *)
val thy = Context.theory_map (RepData.add_thm DEFL) thy;
- val thy = Context.theory_map (RepData.add_thm LIFTDEFL) thy;
- (* declare domain_isodefl rule *)
- val liftemb' = Thm.transfer thy (liftemb_def RS meta_eq_to_obj_eq);
- val liftprj' = Thm.transfer thy (liftprj_def RS meta_eq_to_obj_eq);
- val (_, thy) =
- Global_Theory.add_thm
- ((Binding.suffix_name "_u" (Binding.prefix_name "isodefl_" tbind),
- Drule.zero_var_indexes (@{thm isodefl_u} OF [liftemb', liftprj'])),
- [IsodeflData.add]) thy;
in
(DEFL, thy)
end;
--- a/src/HOLCF/Tools/repdef.ML Wed Nov 10 06:02:37 2010 -0800
+++ b/src/HOLCF/Tools/repdef.ML Wed Nov 10 08:18:32 2010 -0800
@@ -14,8 +14,7 @@
liftemb_def : thm,
liftprj_def : thm,
liftdefl_def : thm,
- DEFL : thm,
- LIFTDEFL : thm
+ DEFL : thm
}
val add_repdef: bool -> binding option -> binding * (string * sort) list * mixfix ->
@@ -44,8 +43,7 @@
liftemb_def : thm,
liftprj_def : thm,
liftdefl_def : thm,
- DEFL : thm,
- LIFTDEFL : thm
+ DEFL : thm
};
(* building types and terms *)
@@ -151,7 +149,7 @@
(*instantiate class rep*)
val lthy = thy
- |> Class.instantiation ([full_tname], lhs_tfrees, @{sort bifinite});
+ |> Class.instantiation ([full_tname], lhs_tfrees, @{sort liftdomain});
val ((_, (_, emb_ldef)), lthy) =
Specification.definition (NONE, (emb_bind, emb_eqn)) lthy;
val ((_, (_, prj_ldef)), lthy) =
@@ -185,25 +183,17 @@
(*other theorems*)
val defl_thm' = Thm.transfer thy defl_def;
- val liftdefl_thm' = Thm.transfer thy liftdefl_def;
val (DEFL_thm, thy) = thy
|> Sign.add_path (Binding.name_of name)
|> Global_Theory.add_thm
((Binding.prefix_name "DEFL_" name,
Drule.zero_var_indexes (@{thm typedef_DEFL} OF [defl_thm'])), [])
||> Sign.restore_naming thy;
- val (LIFTDEFL_thm, thy) = thy
- |> Sign.add_path (Binding.name_of name)
- |> Global_Theory.add_thm
- ((Binding.prefix_name "LIFTDEFL_" name,
- Drule.zero_var_indexes (@{thm typedef_LIFTDEFL} OF [liftdefl_thm'])), [])
- ||> Sign.restore_naming thy;
val rep_info =
{ emb_def = emb_def, prj_def = prj_def, defl_def = defl_def,
liftemb_def = liftemb_def, liftprj_def = liftprj_def,
- liftdefl_def = liftdefl_def,
- DEFL = DEFL_thm, LIFTDEFL = LIFTDEFL_thm };
+ liftdefl_def = liftdefl_def, DEFL = DEFL_thm };
in
((info, cpo_info, pcpo_info, rep_info), thy)
end
--- a/src/HOLCF/UpperPD.thy Wed Nov 10 06:02:37 2010 -0800
+++ b/src/HOLCF/UpperPD.thy Wed Nov 10 08:18:32 2010 -0800
@@ -448,7 +448,7 @@
using upper_approx finite_deflation_upper_map
unfolding upper_defl_def by (rule cast_defl_fun1)
-instantiation upper_pd :: (bifinite) bifinite
+instantiation upper_pd :: (bifinite) liftdomain
begin
definition
@@ -471,7 +471,7 @@
instance
using liftemb_upper_pd_def liftprj_upper_pd_def liftdefl_upper_pd_def
-proof (rule bifinite_class_intro)
+proof (rule liftdomain_class_intro)
show "ep_pair emb (prj :: udom \<rightarrow> 'a upper_pd)"
unfolding emb_upper_pd_def prj_upper_pd_def
using ep_pair_udom [OF upper_approx]
--- a/src/HOLCF/ex/Domain_Proofs.thy Wed Nov 10 06:02:37 2010 -0800
+++ b/src/HOLCF/ex/Domain_Proofs.thy Wed Nov 10 08:18:32 2010 -0800
@@ -94,7 +94,7 @@
text {* Prove rep instance using lemma @{text typedef_rep_class}. *}
-instantiation foo :: (bifinite) bifinite
+instantiation foo :: (bifinite) liftdomain
begin
definition emb_foo :: "'a foo \<rightarrow> udom"
@@ -129,7 +129,7 @@
end
-instantiation bar :: (bifinite) bifinite
+instantiation bar :: (bifinite) liftdomain
begin
definition emb_bar :: "'a bar \<rightarrow> udom"
@@ -164,7 +164,7 @@
end
-instantiation baz :: (bifinite) bifinite
+instantiation baz :: (bifinite) liftdomain
begin
definition emb_baz :: "'a baz \<rightarrow> udom"
@@ -206,34 +206,16 @@
apply (rule defl_foo_def)
done
-lemma LIFTDEFL_foo [domain_defl_simps]:
- "LIFTDEFL('a foo) = u_defl\<cdot>DEFL('a foo)"
-apply (rule typedef_LIFTDEFL)
-apply (rule liftdefl_foo_def)
-done
-
lemma DEFL_bar: "DEFL('a bar) = bar_defl\<cdot>LIFTDEFL('a)"
apply (rule typedef_DEFL)
apply (rule defl_bar_def)
done
-lemma LIFTDEFL_bar [domain_defl_simps]:
- "LIFTDEFL('a bar) = u_defl\<cdot>DEFL('a bar)"
-apply (rule typedef_LIFTDEFL)
-apply (rule liftdefl_bar_def)
-done
-
lemma DEFL_baz: "DEFL('a baz) = baz_defl\<cdot>LIFTDEFL('a)"
apply (rule typedef_DEFL)
apply (rule defl_baz_def)
done
-lemma LIFTDEFL_baz [domain_defl_simps]:
- "LIFTDEFL('a baz) = u_defl\<cdot>DEFL('a baz)"
-apply (rule typedef_LIFTDEFL)
-apply (rule liftdefl_baz_def)
-done
-
text {* Prove DEFL equations using type combinator unfold lemmas. *}
lemma DEFL_foo': "DEFL('a foo) = DEFL(one \<oplus> 'a\<^sub>\<bottom> \<otimes> ('a bar)\<^sub>\<bottom>)"
@@ -306,24 +288,6 @@
"isodefl d t \<Longrightarrow> isodefl (baz_abs oo d oo baz_rep) t"
by (rule isodefl_abs_rep [OF DEFL_baz' baz_abs_def baz_rep_def])
-lemma isodefl_foo_u [domain_isodefl]:
- "isodefl (d :: 'a foo \<rightarrow> _) t \<Longrightarrow> isodefl (u_map\<cdot>d) (u_defl\<cdot>t)"
-using liftemb_foo_def [THEN meta_eq_to_obj_eq]
-using liftprj_foo_def [THEN meta_eq_to_obj_eq]
-by (rule isodefl_u)
-
-lemma isodefl_bar_u [domain_isodefl]:
- "isodefl (d :: 'a bar \<rightarrow> _) t \<Longrightarrow> isodefl (u_map\<cdot>d) (u_defl\<cdot>t)"
-using liftemb_bar_def [THEN meta_eq_to_obj_eq]
-using liftprj_bar_def [THEN meta_eq_to_obj_eq]
-by (rule isodefl_u)
-
-lemma isodefl_baz_u [domain_isodefl]:
- "isodefl (d :: 'a baz \<rightarrow> _) t \<Longrightarrow> isodefl (u_map\<cdot>d) (u_defl\<cdot>t)"
-using liftemb_baz_def [THEN meta_eq_to_obj_eq]
-using liftprj_baz_def [THEN meta_eq_to_obj_eq]
-by (rule isodefl_u)
-
(********************************************************************)
subsection {* Step 4: Define map functions, prove isodefl property *}