# HG changeset patch
# User huffman
# Date 1287511662 25200
# Node ID 9d061b3d8f46e2de7df1f22d6a4d9733ffc9b60b
# Parent  81e6b89d8f58aad37d665ce27f03d24876c7eae6
replace 'in_defl' relation and '_ ::: _' syntax with 'defl_set' function

diff -r 81e6b89d8f58 -r 9d061b3d8f46 src/HOLCF/Algebraic.thy
--- 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
diff -r 81e6b89d8f58 -r 9d061b3d8f46 src/HOLCF/Representable.thy
--- 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 *}
diff -r 81e6b89d8f58 -r 9d061b3d8f46 src/HOLCF/Tools/repdef.ML
--- 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);
 
diff -r 81e6b89d8f58 -r 9d061b3d8f46 src/HOLCF/ex/Domain_Proofs.thy
--- 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}. *}