--- a/src/HOLCF/Algebraic.thy Tue Oct 19 10:13:29 2010 -0700
+++ b/src/HOLCF/Algebraic.thy Tue Oct 19 11:07:42 2010 -0700
@@ -211,43 +211,4 @@
lemma cast_strict2 [simp]: "cast\<cdot>A\<cdot>\<bottom> = \<bottom>"
by (rule cast.below [THEN UU_I])
-subsection {* Deflation membership relation *}
-
-definition
- in_defl :: "udom \<Rightarrow> defl \<Rightarrow> bool" (infixl ":::" 50)
-where
- "x ::: A \<longleftrightarrow> cast\<cdot>A\<cdot>x = x"
-
-lemma adm_in_defl: "adm (\<lambda>x. x ::: A)"
-unfolding in_defl_def by simp
-
-lemma in_deflI: "cast\<cdot>A\<cdot>x = x \<Longrightarrow> x ::: A"
-unfolding in_defl_def .
-
-lemma cast_fixed: "x ::: A \<Longrightarrow> cast\<cdot>A\<cdot>x = x"
-unfolding in_defl_def .
-
-lemma cast_in_defl [simp]: "cast\<cdot>A\<cdot>x ::: A"
-unfolding in_defl_def by (rule cast.idem)
-
-lemma bottom_in_defl [simp]: "\<bottom> ::: A"
-unfolding in_defl_def by (rule cast_strict2)
-
-lemma defl_belowD: "A \<sqsubseteq> B \<Longrightarrow> x ::: A \<Longrightarrow> x ::: B"
-unfolding in_defl_def
- apply (rule deflation.belowD)
- apply (rule deflation_cast)
- apply (erule monofun_cfun_arg)
- apply assumption
-done
-
-lemma rev_defl_belowD: "x ::: A \<Longrightarrow> A \<sqsubseteq> B \<Longrightarrow> x ::: B"
-by (rule defl_belowD)
-
-lemma defl_belowI: "(\<And>x. x ::: A \<Longrightarrow> x ::: B) \<Longrightarrow> A \<sqsubseteq> B"
-apply (rule cast_below_imp_below)
-apply (rule cast.belowI)
-apply (simp add: in_defl_def)
-done
-
end
--- a/src/HOLCF/Representable.thy Tue Oct 19 10:13:29 2010 -0700
+++ b/src/HOLCF/Representable.thy Tue Oct 19 11:07:42 2010 -0700
@@ -59,6 +59,25 @@
unfolding abs_def rep_def
by (simp add: emb_prj_emb DEFL)
+subsection {* Deflations as sets *}
+
+definition defl_set :: "defl \<Rightarrow> udom set"
+where "defl_set A = {x. cast\<cdot>A\<cdot>x = x}"
+
+lemma adm_defl_set: "adm (\<lambda>x. x \<in> defl_set A)"
+unfolding defl_set_def by simp
+
+lemma defl_set_bottom: "\<bottom> \<in> defl_set A"
+unfolding defl_set_def by simp
+
+lemma defl_set_cast [simp]: "cast\<cdot>A\<cdot>x \<in> defl_set A"
+unfolding defl_set_def by simp
+
+lemma defl_set_subset_iff: "defl_set A \<subseteq> defl_set B \<longleftrightarrow> A \<sqsubseteq> B"
+apply (simp add: defl_set_def subset_eq cast_below_cast [symmetric])
+apply (auto simp add: cast.belowI cast.belowD)
+done
+
subsection {* Proving a subtype is representable *}
text {*
@@ -76,34 +95,28 @@
fixes Rep :: "'a::pcpo \<Rightarrow> udom"
fixes Abs :: "udom \<Rightarrow> 'a::pcpo"
fixes t :: defl
- assumes type: "type_definition Rep Abs {x. x ::: t}"
+ assumes type: "type_definition Rep Abs (defl_set t)"
assumes below: "op \<sqsubseteq> \<equiv> \<lambda>x y. Rep x \<sqsubseteq> Rep y"
assumes emb: "emb \<equiv> (\<Lambda> x. Rep x)"
assumes prj: "prj \<equiv> (\<Lambda> x. Abs (cast\<cdot>t\<cdot>x))"
assumes defl: "defl \<equiv> (\<lambda> a::'a itself. t)"
shows "OFCLASS('a, bifinite_class)"
proof
- have adm: "adm (\<lambda>x. x \<in> {x. x ::: t})"
- by (simp add: adm_in_defl)
have emb_beta: "\<And>x. emb\<cdot>x = Rep x"
unfolding emb
apply (rule beta_cfun)
- apply (rule typedef_cont_Rep [OF type below adm])
+ apply (rule typedef_cont_Rep [OF type below adm_defl_set])
done
have prj_beta: "\<And>y. prj\<cdot>y = Abs (cast\<cdot>t\<cdot>y)"
unfolding prj
apply (rule beta_cfun)
- apply (rule typedef_cont_Abs [OF type below adm])
+ apply (rule typedef_cont_Abs [OF type below adm_defl_set])
apply simp_all
done
- have emb_in_defl: "\<And>x::'a. emb\<cdot>x ::: t"
+ have prj_emb: "\<And>x::'a. prj\<cdot>(emb\<cdot>x) = x"
using type_definition.Rep [OF type]
- by (simp add: emb_beta)
- have prj_emb: "\<And>x::'a. prj\<cdot>(emb\<cdot>x) = x"
- unfolding prj_beta
- apply (simp add: cast_fixed [OF emb_in_defl])
- apply (simp add: emb_beta type_definition.Rep_inverse [OF type])
- done
+ unfolding prj_beta emb_beta defl_set_def
+ by (simp add: type_definition.Rep_inverse [OF type])
have emb_prj: "\<And>y. emb\<cdot>(prj\<cdot>y :: 'a) = cast\<cdot>t\<cdot>y"
unfolding prj_beta emb_beta
by (simp add: type_definition.Abs_inverse [OF type])
@@ -130,9 +143,6 @@
, (@{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)
-
use "Tools/repdef.ML"
subsection {* Isomorphic deflations *}
--- a/src/HOLCF/Tools/repdef.ML Tue Oct 19 10:13:29 2010 -0700
+++ b/src/HOLCF/Tools/repdef.ML Tue Oct 19 11:07:42 2010 -0700
@@ -84,12 +84,11 @@
|> the_default (Binding.prefix_name "Rep_" name, Binding.prefix_name "Abs_" name);
(*set*)
- val in_defl = @{term "in_defl :: udom => defl => bool"};
- val set = HOLogic.Collect_const udomT $ Abs ("x", udomT, in_defl $ Bound 0 $ defl);
+ val set = @{const defl_set} $ defl;
(*pcpodef*)
- val tac1 = rtac @{thm CollectI} 1 THEN rtac @{thm bottom_in_defl} 1;
- val tac2 = rtac @{thm adm_mem_Collect_in_defl} 1;
+ val tac1 = rtac @{thm defl_set_bottom} 1;
+ val tac2 = rtac @{thm adm_defl_set} 1;
val ((info, cpo_info, pcpo_info), thy) = thy
|> Pcpodef.add_pcpodef def (SOME name) typ set (SOME morphs) (tac1, tac2);
--- a/src/HOLCF/ex/Domain_Proofs.thy Tue Oct 19 10:13:29 2010 -0700
+++ b/src/HOLCF/ex/Domain_Proofs.thy Tue Oct 19 11:07:42 2010 -0700
@@ -82,14 +82,14 @@
text {* Use @{text pcpodef} with the appropriate type combinator. *}
-pcpodef (open) 'a foo = "{x. x ::: foo_defl\<cdot>DEFL('a)}"
-by (simp_all add: adm_in_defl)
+pcpodef (open) 'a foo = "defl_set (foo_defl\<cdot>DEFL('a))"
+by (rule defl_set_bottom, rule adm_defl_set)
-pcpodef (open) 'a bar = "{x. x ::: bar_defl\<cdot>DEFL('a)}"
-by (simp_all add: adm_in_defl)
+pcpodef (open) 'a bar = "defl_set (bar_defl\<cdot>DEFL('a))"
+by (rule defl_set_bottom, rule adm_defl_set)
-pcpodef (open) 'a baz = "{x. x ::: baz_defl\<cdot>DEFL('a)}"
-by (simp_all add: adm_in_defl)
+pcpodef (open) 'a baz = "defl_set (baz_defl\<cdot>DEFL('a))"
+by (rule defl_set_bottom, rule adm_defl_set)
text {* Prove rep instance using lemma @{text typedef_rep_class}. *}