# HG changeset patch
# User huffman
# Date 1213822991 -7200
# Node ID 5ebfb7f25ebb40926402d23eb5f9e377714fd35a
# Parent  a2db1e37977894d97f13956244ae4636053e3612
add lemma compact_imp_principal to locale ideal_completion

diff -r a2db1e379778 -r 5ebfb7f25ebb src/HOLCF/CompactBasis.thy
--- a/src/HOLCF/CompactBasis.thy	Wed Jun 18 22:32:06 2008 +0200
+++ b/src/HOLCF/CompactBasis.thy	Wed Jun 18 23:03:11 2008 +0200
@@ -371,6 +371,16 @@
  apply (clarify, simp add: P)
 done
 
+lemma compact_imp_principal: "compact x \<Longrightarrow> \<exists>a. x = principal a"
+apply (drule adm_compact_neq [OF _ cont_id])
+apply (drule admD2 [where Y="\<lambda>n. completion_approx n\<cdot>x"])
+apply (simp add: chain_completion_approx)
+apply (simp add: lub_completion_approx)
+apply (erule exE, erule ssubst)
+apply (cut_tac i=i and x=x in completion_approx_eq_principal)
+apply (clarify, erule exI)
+done
+
 end
 
 
diff -r a2db1e379778 -r 5ebfb7f25ebb src/HOLCF/ConvexPD.thy
--- a/src/HOLCF/ConvexPD.thy	Wed Jun 18 22:32:06 2008 +0200
+++ b/src/HOLCF/ConvexPD.thy	Wed Jun 18 23:03:11 2008 +0200
@@ -236,12 +236,7 @@
 
 lemma compact_imp_convex_principal:
   "compact xs \<Longrightarrow> \<exists>t. xs = convex_principal t"
-apply (drule bifinite_compact_eq_approx)
-apply (erule exE)
-apply (erule subst)
-apply (cut_tac n=i and xs=xs in approx_eq_convex_principal)
-apply fast
-done
+by (rule convex_pd.compact_imp_principal)
 
 lemma convex_principal_induct:
   "\<lbrakk>adm P; \<And>t. P (convex_principal t)\<rbrakk> \<Longrightarrow> P xs"
diff -r a2db1e379778 -r 5ebfb7f25ebb src/HOLCF/LowerPD.thy
--- a/src/HOLCF/LowerPD.thy	Wed Jun 18 22:32:06 2008 +0200
+++ b/src/HOLCF/LowerPD.thy	Wed Jun 18 23:03:11 2008 +0200
@@ -188,12 +188,7 @@
 
 lemma compact_imp_lower_principal:
   "compact xs \<Longrightarrow> \<exists>t. xs = lower_principal t"
-apply (drule bifinite_compact_eq_approx)
-apply (erule exE)
-apply (erule subst)
-apply (cut_tac n=i and xs=xs in approx_eq_lower_principal)
-apply fast
-done
+by (rule lower_pd.compact_imp_principal)
 
 lemma lower_principal_induct:
   "\<lbrakk>adm P; \<And>t. P (lower_principal t)\<rbrakk> \<Longrightarrow> P xs"
diff -r a2db1e379778 -r 5ebfb7f25ebb src/HOLCF/UpperPD.thy
--- a/src/HOLCF/UpperPD.thy	Wed Jun 18 22:32:06 2008 +0200
+++ b/src/HOLCF/UpperPD.thy	Wed Jun 18 23:03:11 2008 +0200
@@ -186,12 +186,7 @@
 
 lemma compact_imp_upper_principal:
   "compact xs \<Longrightarrow> \<exists>t. xs = upper_principal t"
-apply (drule bifinite_compact_eq_approx)
-apply (erule exE)
-apply (erule subst)
-apply (cut_tac n=i and xs=xs in approx_eq_upper_principal)
-apply fast
-done
+by (rule upper_pd.compact_imp_principal)
 
 lemma upper_principal_induct:
   "\<lbrakk>adm P; \<And>t. P (upper_principal t)\<rbrakk> \<Longrightarrow> P xs"