src/HOLCF/Up.thy
changeset 25906 2179c6661218
parent 25898 d8f17d8cf9d4
child 25911 cc3f00949986
     1.1 --- a/src/HOLCF/Up.thy	Mon Jan 14 20:04:40 2008 +0100
     1.2 +++ b/src/HOLCF/Up.thy	Mon Jan 14 20:28:59 2008 +0100
     1.3 @@ -177,55 +177,6 @@
     1.4  instance u :: (cpo) cpo
     1.5  by intro_classes (rule cpo_up)
     1.6  
     1.7 -lemma up_directed_lemma:
     1.8 -  "directed (S::'a::dcpo u set) \<Longrightarrow>
     1.9 -    (directed (Iup -` S) \<and> S <<| Iup (lub (Iup -` S))) \<or>
    1.10 -    S = {Ibottom}"
    1.11 -apply (case_tac "\<exists>x. Iup x \<in> S")
    1.12 -apply (rule disjI1)
    1.13 -apply (subgoal_tac "directed (Iup -` S)")
    1.14 -apply (rule conjI, assumption)
    1.15 -apply (rule is_lubI)
    1.16 -apply (rule is_ubI)
    1.17 -apply (case_tac x, simp, simp)
    1.18 -apply (erule is_ub_thelub', simp)
    1.19 -apply (case_tac u)
    1.20 -apply (erule exE)
    1.21 -apply (drule (1) is_ubD)
    1.22 -apply simp
    1.23 -apply simp
    1.24 -apply (erule is_lub_thelub')
    1.25 -apply (rule is_ubI, simp)
    1.26 -apply (drule (1) is_ubD, simp)
    1.27 -apply (rule directedI)
    1.28 -apply (erule exE)
    1.29 -apply (rule exI)
    1.30 -apply (erule vimageI2)
    1.31 -apply simp
    1.32 -apply (drule_tac x="Iup x" and y="Iup y" in directedD2, assumption+)
    1.33 -apply (erule bexE, rename_tac z)
    1.34 -apply (case_tac z)
    1.35 -apply simp
    1.36 -apply (rule_tac x=a in bexI)
    1.37 -apply simp
    1.38 -apply simp
    1.39 -apply (rule disjI2)
    1.40 -apply (simp, safe)
    1.41 -apply (case_tac x, simp, simp)
    1.42 -apply (drule directedD1)
    1.43 -apply (clarify, rename_tac x)
    1.44 -apply (case_tac x, simp, simp)
    1.45 -done
    1.46 -
    1.47 -lemma dcpo_up: "directed (S::'a::dcpo u set) \<Longrightarrow> \<exists>x. S <<| x"
    1.48 -apply (frule up_directed_lemma, safe)
    1.49 -apply (erule exI)
    1.50 -apply (rule exI, rule is_lub_singleton)
    1.51 -done
    1.52 -
    1.53 -instance u :: (dcpo) dcpo
    1.54 -by intro_classes (rule dcpo_up)
    1.55 -
    1.56  subsection {* Lifted cpo is pointed *}
    1.57  
    1.58  lemma least_up: "\<exists>x::'a u. \<forall>y. x \<sqsubseteq> y"