src/HOLCF/Up.thy
changeset 27414 95ec4bda5bb9
parent 27413 3154f3765cc7
child 29138 661a8db7e647
     1.1 --- a/src/HOLCF/Up.thy	Tue Jul 01 02:19:53 2008 +0200
     1.2 +++ b/src/HOLCF/Up.thy	Tue Jul 01 02:50:29 2008 +0200
     1.3 @@ -93,22 +93,6 @@
     1.4  apply simp
     1.5  done
     1.6  
     1.7 -lemma is_lub_Iup': "\<lbrakk>directed S; S <<| x\<rbrakk> \<Longrightarrow> (Iup ` S) <<| Iup x"
     1.8 -apply (rule is_lubI)
     1.9 -apply (rule ub_imageI)
    1.10 -apply (subst Iup_less)
    1.11 -apply (erule (1) is_ubD [OF is_lubD1])
    1.12 -apply (case_tac u)
    1.13 -apply (drule directedD1, erule exE)
    1.14 -apply (drule (1) ub_imageD)
    1.15 -apply simp
    1.16 -apply simp
    1.17 -apply (erule is_lub_lub)
    1.18 -apply (rule is_ubI)
    1.19 -apply (drule (1) ub_imageD)
    1.20 -apply simp
    1.21 -done
    1.22 -
    1.23  text {* Now some lemmas about chains of @{typ "'a u"} elements *}
    1.24  
    1.25  lemma up_lemma1: "z \<noteq> Ibottom \<Longrightarrow> Iup (THE a. Iup a = z) = z"