# HG changeset patch
# User huffman
# Date 1129065819 -7200
# Node ID 8631dfe017a820c772d51530db3d5c8313bb741b
# Parent  e18fc1a9a0e054a6c0750ae4e62fb3f3d12b3002
added theorem typedef_compact

diff -r e18fc1a9a0e0 -r 8631dfe017a8 src/HOLCF/Pcpodef.thy
--- 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 {*
diff -r e18fc1a9a0e0 -r 8631dfe017a8 src/HOLCF/pcpodef_package.ML
--- 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;