# HG changeset patch
# User huffman
# Date 1201919200 -3600
# Node ID 97d00128072b11f6abb67997972f00c600a3ed9c
# Parent  278025d5282dd19eef9bbdd5e25c7d2fc83e9125
cleaned up

diff -r 278025d5282d -r 97d00128072b src/HOLCF/CompactBasis.thy
--- 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)"