# HG changeset patch
# User huffman
# Date 1199939763 -3600
# Node ID 2c6cabe7a47c2def2a61b1597443e2f94807a2d7
# Parent  98b93782c3b130bcdaee286c0aa8369ab43bdabf
Compactness subsection with some new lemmas

diff -r 98b93782c3b1 -r 2c6cabe7a47c src/HOLCF/Adm.thy
--- a/src/HOLCF/Adm.thy	Thu Jan 10 05:15:43 2008 +0100
+++ b/src/HOLCF/Adm.thy	Thu Jan 10 05:36:03 2008 +0100
@@ -17,10 +17,6 @@
   adm :: "('a::cpo \<Rightarrow> bool) \<Rightarrow> bool" where
   "adm P = (\<forall>Y. chain Y \<longrightarrow> (\<forall>i. P (Y i)) \<longrightarrow> P (\<Squnion>i. Y i))"
 
-definition
-  compact :: "'a::cpo \<Rightarrow> bool" where
-  "compact k = adm (\<lambda>x. \<not> k \<sqsubseteq> x)"
-
 lemma admI:
    "(\<And>Y. \<lbrakk>chain Y; \<forall>i. P (Y i)\<rbrakk> \<Longrightarrow> P (\<Squnion>i. Y i)) \<Longrightarrow> adm P"
 by (unfold adm_def, fast)
@@ -31,12 +27,6 @@
 lemma admD: "\<lbrakk>adm P; chain Y; \<forall>i. P (Y i)\<rbrakk> \<Longrightarrow> P (\<Squnion>i. Y i)"
 by (unfold adm_def, fast)
 
-lemma compactI: "adm (\<lambda>x. \<not> k \<sqsubseteq> x) \<Longrightarrow> compact k"
-by (unfold compact_def)
-
-lemma compactD: "compact k \<Longrightarrow> adm (\<lambda>x. \<not> k \<sqsubseteq> x)"
-by (unfold compact_def)
-
 text {* improved admissibility introduction *}
 
 lemma admI2:
@@ -58,9 +48,6 @@
 
 lemmas adm_chfin = chfin [THEN adm_max_in_chain, standard]
 
-lemma compact_chfin: "compact (x::'a::chfin)"
-by (rule compactI, rule adm_chfin)
-
 subsection {* Admissibility of special formulae and propagation *}
 
 lemma adm_not_free: "adm (\<lambda>x. t)"
@@ -171,10 +158,43 @@
 apply (erule is_ub_thelub)
 done
 
+subsection {* Compactness *}
+
+definition
+  compact :: "'a::cpo \<Rightarrow> bool" where
+  "compact k = adm (\<lambda>x. \<not> k \<sqsubseteq> x)"
+
+lemma compactI: "adm (\<lambda>x. \<not> k \<sqsubseteq> x) \<Longrightarrow> compact k"
+unfolding compact_def .
+
+lemma compactD: "compact k \<Longrightarrow> adm (\<lambda>x. \<not> k \<sqsubseteq> x)"
+unfolding compact_def .
+
+lemma compactI2:
+  "(\<And>Y. \<lbrakk>chain Y; x \<sqsubseteq> lub (range Y)\<rbrakk> \<Longrightarrow> \<exists>i. x \<sqsubseteq> Y i) \<Longrightarrow> compact x"
+unfolding compact_def adm_def by fast
+
+lemma compactD2:
+  "\<lbrakk>compact x; chain Y; x \<sqsubseteq> lub (range Y)\<rbrakk> \<Longrightarrow> \<exists>i. x \<sqsubseteq> Y i"
+unfolding compact_def adm_def by fast
+
+lemma compact_chfin [simp]: "compact (x::'a::chfin)"
+by (rule compactI [OF adm_chfin])
+
+lemma compact_imp_max_in_chain:
+  "\<lbrakk>chain Y; compact (\<Squnion>i. Y i)\<rbrakk> \<Longrightarrow> \<exists>i. max_in_chain i Y"
+apply (drule (1) compactD2, simp)
+apply (erule exE, rule_tac x=i in exI)
+apply (rule max_in_chainI)
+apply (rule antisym_less)
+apply (erule (1) chain_mono3)
+apply (erule (1) trans_less [OF is_ub_thelub])
+done
+
 text {* admissibility and compactness *}
 
 lemma adm_compact_not_less: "\<lbrakk>compact k; cont t\<rbrakk> \<Longrightarrow> adm (\<lambda>x. \<not> k \<sqsubseteq> t x)"
-by (unfold compact_def, erule adm_subst)
+unfolding compact_def by (rule adm_subst)
 
 lemma adm_neq_compact: "\<lbrakk>compact k; cont t\<rbrakk> \<Longrightarrow> adm (\<lambda>x. t x \<noteq> k)"
 by (simp add: po_eq_conv adm_imp adm_not_less adm_compact_not_less)