Compactness subsection with some new lemmas
authorhuffman
Thu Jan 10 05:36:03 2008 +0100 (2008-01-10)
changeset 258802c6cabe7a47c
parent 25879 98b93782c3b1
child 25881 d80bd899ea95
Compactness subsection with some new lemmas
src/HOLCF/Adm.thy
     1.1 --- a/src/HOLCF/Adm.thy	Thu Jan 10 05:15:43 2008 +0100
     1.2 +++ b/src/HOLCF/Adm.thy	Thu Jan 10 05:36:03 2008 +0100
     1.3 @@ -17,10 +17,6 @@
     1.4    adm :: "('a::cpo \<Rightarrow> bool) \<Rightarrow> bool" where
     1.5    "adm P = (\<forall>Y. chain Y \<longrightarrow> (\<forall>i. P (Y i)) \<longrightarrow> P (\<Squnion>i. Y i))"
     1.6  
     1.7 -definition
     1.8 -  compact :: "'a::cpo \<Rightarrow> bool" where
     1.9 -  "compact k = adm (\<lambda>x. \<not> k \<sqsubseteq> x)"
    1.10 -
    1.11  lemma admI:
    1.12     "(\<And>Y. \<lbrakk>chain Y; \<forall>i. P (Y i)\<rbrakk> \<Longrightarrow> P (\<Squnion>i. Y i)) \<Longrightarrow> adm P"
    1.13  by (unfold adm_def, fast)
    1.14 @@ -31,12 +27,6 @@
    1.15  lemma admD: "\<lbrakk>adm P; chain Y; \<forall>i. P (Y i)\<rbrakk> \<Longrightarrow> P (\<Squnion>i. Y i)"
    1.16  by (unfold adm_def, fast)
    1.17  
    1.18 -lemma compactI: "adm (\<lambda>x. \<not> k \<sqsubseteq> x) \<Longrightarrow> compact k"
    1.19 -by (unfold compact_def)
    1.20 -
    1.21 -lemma compactD: "compact k \<Longrightarrow> adm (\<lambda>x. \<not> k \<sqsubseteq> x)"
    1.22 -by (unfold compact_def)
    1.23 -
    1.24  text {* improved admissibility introduction *}
    1.25  
    1.26  lemma admI2:
    1.27 @@ -58,9 +48,6 @@
    1.28  
    1.29  lemmas adm_chfin = chfin [THEN adm_max_in_chain, standard]
    1.30  
    1.31 -lemma compact_chfin: "compact (x::'a::chfin)"
    1.32 -by (rule compactI, rule adm_chfin)
    1.33 -
    1.34  subsection {* Admissibility of special formulae and propagation *}
    1.35  
    1.36  lemma adm_not_free: "adm (\<lambda>x. t)"
    1.37 @@ -171,10 +158,43 @@
    1.38  apply (erule is_ub_thelub)
    1.39  done
    1.40  
    1.41 +subsection {* Compactness *}
    1.42 +
    1.43 +definition
    1.44 +  compact :: "'a::cpo \<Rightarrow> bool" where
    1.45 +  "compact k = adm (\<lambda>x. \<not> k \<sqsubseteq> x)"
    1.46 +
    1.47 +lemma compactI: "adm (\<lambda>x. \<not> k \<sqsubseteq> x) \<Longrightarrow> compact k"
    1.48 +unfolding compact_def .
    1.49 +
    1.50 +lemma compactD: "compact k \<Longrightarrow> adm (\<lambda>x. \<not> k \<sqsubseteq> x)"
    1.51 +unfolding compact_def .
    1.52 +
    1.53 +lemma compactI2:
    1.54 +  "(\<And>Y. \<lbrakk>chain Y; x \<sqsubseteq> lub (range Y)\<rbrakk> \<Longrightarrow> \<exists>i. x \<sqsubseteq> Y i) \<Longrightarrow> compact x"
    1.55 +unfolding compact_def adm_def by fast
    1.56 +
    1.57 +lemma compactD2:
    1.58 +  "\<lbrakk>compact x; chain Y; x \<sqsubseteq> lub (range Y)\<rbrakk> \<Longrightarrow> \<exists>i. x \<sqsubseteq> Y i"
    1.59 +unfolding compact_def adm_def by fast
    1.60 +
    1.61 +lemma compact_chfin [simp]: "compact (x::'a::chfin)"
    1.62 +by (rule compactI [OF adm_chfin])
    1.63 +
    1.64 +lemma compact_imp_max_in_chain:
    1.65 +  "\<lbrakk>chain Y; compact (\<Squnion>i. Y i)\<rbrakk> \<Longrightarrow> \<exists>i. max_in_chain i Y"
    1.66 +apply (drule (1) compactD2, simp)
    1.67 +apply (erule exE, rule_tac x=i in exI)
    1.68 +apply (rule max_in_chainI)
    1.69 +apply (rule antisym_less)
    1.70 +apply (erule (1) chain_mono3)
    1.71 +apply (erule (1) trans_less [OF is_ub_thelub])
    1.72 +done
    1.73 +
    1.74  text {* admissibility and compactness *}
    1.75  
    1.76  lemma adm_compact_not_less: "\<lbrakk>compact k; cont t\<rbrakk> \<Longrightarrow> adm (\<lambda>x. \<not> k \<sqsubseteq> t x)"
    1.77 -by (unfold compact_def, erule adm_subst)
    1.78 +unfolding compact_def by (rule adm_subst)
    1.79  
    1.80  lemma adm_neq_compact: "\<lbrakk>compact k; cont t\<rbrakk> \<Longrightarrow> adm (\<lambda>x. t x \<noteq> k)"
    1.81  by (simp add: po_eq_conv adm_imp adm_not_less adm_compact_not_less)