src/HOLCF/Up.thy
changeset 25789 c0506ac5b6b4
parent 25788 30cbe0764599
child 25827 c2adeb1bae5c
     1.1 --- a/src/HOLCF/Up.thy	Wed Jan 02 19:51:29 2008 +0100
     1.2 +++ b/src/HOLCF/Up.thy	Wed Jan 02 20:23:49 2008 +0100
     1.3 @@ -86,6 +86,22 @@
     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"
    1.26 @@ -154,6 +170,55 @@
    1.27  instance u :: (cpo) cpo
    1.28  by intro_classes (rule cpo_up)
    1.29  
    1.30 +lemma up_directed_lemma:
    1.31 +  "directed (S::'a::dcpo u set) \<Longrightarrow>
    1.32 +    (directed (Iup -` S) \<and> S <<| Iup (lub (Iup -` S))) \<or>
    1.33 +    S = {Ibottom}"
    1.34 +apply (case_tac "\<exists>x. Iup x \<in> S")
    1.35 +apply (rule disjI1)
    1.36 +apply (subgoal_tac "directed (Iup -` S)")
    1.37 +apply (rule conjI, assumption)
    1.38 +apply (rule is_lubI)
    1.39 +apply (rule is_ubI)
    1.40 +apply (case_tac x, simp, simp)
    1.41 +apply (erule is_ub_thelub', simp)
    1.42 +apply (case_tac u)
    1.43 +apply (erule exE)
    1.44 +apply (drule (1) is_ubD)
    1.45 +apply simp
    1.46 +apply simp
    1.47 +apply (erule is_lub_thelub')
    1.48 +apply (rule is_ubI, simp)
    1.49 +apply (drule (1) is_ubD, simp)
    1.50 +apply (rule directedI)
    1.51 +apply (erule exE)
    1.52 +apply (rule exI)
    1.53 +apply (erule vimageI2)
    1.54 +apply simp
    1.55 +apply (drule_tac x="Iup x" and y="Iup y" in directedD2, assumption+)
    1.56 +apply (erule bexE, rename_tac z)
    1.57 +apply (case_tac z)
    1.58 +apply simp
    1.59 +apply (rule_tac x=a in bexI)
    1.60 +apply simp
    1.61 +apply simp
    1.62 +apply (rule disjI2)
    1.63 +apply (simp, safe)
    1.64 +apply (case_tac x, simp, simp)
    1.65 +apply (drule directedD1)
    1.66 +apply (clarify, rename_tac x)
    1.67 +apply (case_tac x, simp, simp)
    1.68 +done
    1.69 +
    1.70 +lemma dcpo_up: "directed (S::'a::dcpo u set) \<Longrightarrow> \<exists>x. S <<| x"
    1.71 +apply (frule up_directed_lemma, safe)
    1.72 +apply (erule exI)
    1.73 +apply (rule exI, rule is_lub_singleton)
    1.74 +done
    1.75 +
    1.76 +instance u :: (dcpo) dcpo
    1.77 +by intro_classes (rule dcpo_up)
    1.78 +
    1.79  subsection {* Lifted cpo is pointed *}
    1.80  
    1.81  lemma least_up: "\<exists>x::'a u. \<forall>y. x \<sqsubseteq> y"