--- a/src/HOLCF/Pcpodef.thy Tue Oct 11 23:22:12 2005 +0200
+++ b/src/HOLCF/Pcpodef.thy Tue Oct 11 23:23:39 2005 +0200
@@ -156,6 +156,22 @@
apply (erule cont_f [THEN contE])
done
+subsection {* Proving subtype elements are compact *}
+
+theorem typedef_compact:
+ fixes Abs :: "'a::cpo \<Rightarrow> 'b::cpo"
+ assumes type: "type_definition Rep Abs A"
+ and less: "op \<sqsubseteq> \<equiv> \<lambda>x y. Rep x \<sqsubseteq> Rep y"
+ and adm: "adm (\<lambda>x. x \<in> A)"
+ shows "compact (Rep k) \<Longrightarrow> compact k"
+proof (unfold compact_def)
+ have cont_Rep: "cont Rep"
+ by (rule typedef_cont_Rep [OF type less adm])
+ assume "adm (\<lambda>x. \<not> Rep k \<sqsubseteq> x)"
+ with cont_Rep have "adm (\<lambda>x. \<not> Rep k \<sqsubseteq> Rep x)" by (rule adm_subst)
+ thus "adm (\<lambda>x. \<not> k \<sqsubseteq> x)" by (unfold less)
+qed
+
subsection {* Proving a subtype is pointed *}
text {*
--- a/src/HOLCF/pcpodef_package.ML Tue Oct 11 23:22:12 2005 +0200
+++ b/src/HOLCF/pcpodef_package.ML Tue Oct 11 23:23:39 2005 +0200
@@ -29,6 +29,7 @@
val typedef_pcpo = thm "typedef_pcpo";
val typedef_lub = thm "typedef_lub";
val typedef_thelub = thm "typedef_thelub";
+val typedef_compact = thm "typedef_compact";
val cont_Rep = thm "typedef_cont_Rep";
val cont_Abs = thm "typedef_cont_Abs";
val Rep_strict = thm "typedef_Rep_strict";
@@ -119,8 +120,9 @@
([(("adm_" ^ name, admissible'), []),
(("cont_" ^ Rep_name, cont_Rep OF cpo_thms), []),
(("cont_" ^ Abs_name, cont_Abs OF cpo_thms), []),
- (("lub_" ^ name, typedef_lub OF cpo_thms), []),
- (("thelub_" ^ name, typedef_thelub OF cpo_thms), [])])
+ (("lub_" ^ name, typedef_lub OF cpo_thms), []),
+ (("thelub_" ^ name, typedef_thelub OF cpo_thms), []),
+ (("compact_" ^ name, typedef_compact OF cpo_thms), [])])
|>> Theory.parent_path;
in (theory', defs) end;