--- a/src/HOLCF/CompactBasis.thy Fri Feb 01 18:01:06 2008 +0100
+++ b/src/HOLCF/CompactBasis.thy Sat Feb 02 03:26:40 2008 +0100
@@ -93,13 +93,23 @@
apply (simp add: refl)
done
-lemma finite_directed_has_lub: "\<lbrakk>finite S; directed S\<rbrakk> \<Longrightarrow> \<exists>u. S <<| u"
+lemma finite_directed_contains_lub:
+ "\<lbrakk>finite S; directed S\<rbrakk> \<Longrightarrow> \<exists>u\<in>S. S <<| u"
apply (drule (1) directed_finiteD, rule subset_refl)
apply (erule bexE)
-apply (rule_tac x=z in exI)
+apply (rule rev_bexI, assumption)
apply (erule (1) is_lub_maximal)
done
+lemma lub_finite_directed_in_self:
+ "\<lbrakk>finite S; directed S\<rbrakk> \<Longrightarrow> lub S \<in> S"
+apply (drule (1) finite_directed_contains_lub, clarify)
+apply (drule thelubI, simp)
+done
+
+lemma finite_directed_has_lub: "\<lbrakk>finite S; directed S\<rbrakk> \<Longrightarrow> \<exists>u. S <<| u"
+by (drule (1) finite_directed_contains_lub, fast)
+
lemma is_ub_thelub0: "\<lbrakk>\<exists>u. S <<| u; x \<in> S\<rbrakk> \<Longrightarrow> x \<sqsubseteq> lub S"
apply (erule exE, drule lubI)
apply (drule is_lubD1)
@@ -301,23 +311,6 @@
apply (rule basis_fun_lemma2, erule principal_mono)
done
-lemma finite_directed_contains_lub:
- "\<lbrakk>finite S; directed S\<rbrakk> \<Longrightarrow> \<exists>u\<in>S. S <<| u"
-apply (drule (1) directed_finiteD, rule subset_refl)
-apply (erule bexE)
-apply (rule rev_bexI, assumption)
-apply (erule (1) is_lub_maximal)
-done
-
-lemma lub_finite_directed_in_self:
- "\<lbrakk>finite S; directed S\<rbrakk> \<Longrightarrow> lub S \<in> S"
-apply (drule (1) directed_finiteD, rule subset_refl)
-apply (erule bexE)
-apply (drule (1) is_lub_maximal)
-apply (drule thelubI)
-apply simp
-done
-
lemma basis_fun_take_eq_principal:
"\<exists>a\<in>approxes x.
basis_fun (\<lambda>a. principal (take i a))\<cdot>x = principal (take i a)"