add lemma compact_imp_principal to locale ideal_completion
authorhuffman
Wed Jun 18 23:03:11 2008 +0200 (2008-06-18)
changeset 272675ebfb7f25ebb
parent 27266 a2db1e379778
child 27268 1d8c6703c7b1
add lemma compact_imp_principal to locale ideal_completion
src/HOLCF/CompactBasis.thy
src/HOLCF/ConvexPD.thy
src/HOLCF/LowerPD.thy
src/HOLCF/UpperPD.thy
     1.1 --- a/src/HOLCF/CompactBasis.thy	Wed Jun 18 22:32:06 2008 +0200
     1.2 +++ b/src/HOLCF/CompactBasis.thy	Wed Jun 18 23:03:11 2008 +0200
     1.3 @@ -371,6 +371,16 @@
     1.4   apply (clarify, simp add: P)
     1.5  done
     1.6  
     1.7 +lemma compact_imp_principal: "compact x \<Longrightarrow> \<exists>a. x = principal a"
     1.8 +apply (drule adm_compact_neq [OF _ cont_id])
     1.9 +apply (drule admD2 [where Y="\<lambda>n. completion_approx n\<cdot>x"])
    1.10 +apply (simp add: chain_completion_approx)
    1.11 +apply (simp add: lub_completion_approx)
    1.12 +apply (erule exE, erule ssubst)
    1.13 +apply (cut_tac i=i and x=x in completion_approx_eq_principal)
    1.14 +apply (clarify, erule exI)
    1.15 +done
    1.16 +
    1.17  end
    1.18  
    1.19  
     2.1 --- a/src/HOLCF/ConvexPD.thy	Wed Jun 18 22:32:06 2008 +0200
     2.2 +++ b/src/HOLCF/ConvexPD.thy	Wed Jun 18 23:03:11 2008 +0200
     2.3 @@ -236,12 +236,7 @@
     2.4  
     2.5  lemma compact_imp_convex_principal:
     2.6    "compact xs \<Longrightarrow> \<exists>t. xs = convex_principal t"
     2.7 -apply (drule bifinite_compact_eq_approx)
     2.8 -apply (erule exE)
     2.9 -apply (erule subst)
    2.10 -apply (cut_tac n=i and xs=xs in approx_eq_convex_principal)
    2.11 -apply fast
    2.12 -done
    2.13 +by (rule convex_pd.compact_imp_principal)
    2.14  
    2.15  lemma convex_principal_induct:
    2.16    "\<lbrakk>adm P; \<And>t. P (convex_principal t)\<rbrakk> \<Longrightarrow> P xs"
     3.1 --- a/src/HOLCF/LowerPD.thy	Wed Jun 18 22:32:06 2008 +0200
     3.2 +++ b/src/HOLCF/LowerPD.thy	Wed Jun 18 23:03:11 2008 +0200
     3.3 @@ -188,12 +188,7 @@
     3.4  
     3.5  lemma compact_imp_lower_principal:
     3.6    "compact xs \<Longrightarrow> \<exists>t. xs = lower_principal t"
     3.7 -apply (drule bifinite_compact_eq_approx)
     3.8 -apply (erule exE)
     3.9 -apply (erule subst)
    3.10 -apply (cut_tac n=i and xs=xs in approx_eq_lower_principal)
    3.11 -apply fast
    3.12 -done
    3.13 +by (rule lower_pd.compact_imp_principal)
    3.14  
    3.15  lemma lower_principal_induct:
    3.16    "\<lbrakk>adm P; \<And>t. P (lower_principal t)\<rbrakk> \<Longrightarrow> P xs"
     4.1 --- a/src/HOLCF/UpperPD.thy	Wed Jun 18 22:32:06 2008 +0200
     4.2 +++ b/src/HOLCF/UpperPD.thy	Wed Jun 18 23:03:11 2008 +0200
     4.3 @@ -186,12 +186,7 @@
     4.4  
     4.5  lemma compact_imp_upper_principal:
     4.6    "compact xs \<Longrightarrow> \<exists>t. xs = upper_principal t"
     4.7 -apply (drule bifinite_compact_eq_approx)
     4.8 -apply (erule exE)
     4.9 -apply (erule subst)
    4.10 -apply (cut_tac n=i and xs=xs in approx_eq_upper_principal)
    4.11 -apply fast
    4.12 -done
    4.13 +by (rule upper_pd.compact_imp_principal)
    4.14  
    4.15  lemma upper_principal_induct:
    4.16    "\<lbrakk>adm P; \<And>t. P (upper_principal t)\<rbrakk> \<Longrightarrow> P xs"