src/HOLCF/Up.thy
changeset 27413 3154f3765cc7
parent 27310 d0229bc6c461
child 27414 95ec4bda5bb9
     1.1 --- a/src/HOLCF/Up.thy	Tue Jul 01 01:28:44 2008 +0200
     1.2 +++ b/src/HOLCF/Up.thy	Tue Jul 01 02:19:53 2008 +0200
     1.3 @@ -154,7 +154,7 @@
     1.4  
     1.5  lemma up_chain_lemma:
     1.6    "chain Y \<Longrightarrow>
     1.7 -   (\<exists>A. chain A \<and> lub (range Y) = Iup (lub (range A)) \<and>
     1.8 +   (\<exists>A. chain A \<and> (\<Squnion>i. Y i) = Iup (\<Squnion>i. A i) \<and>
     1.9     (\<exists>j. \<forall>i. Y (i + j) = Iup (A i))) \<or> (Y = (\<lambda>i. Ibottom))"
    1.10  apply (rule disjCI)
    1.11  apply (simp add: expand_fun_eq)
    1.12 @@ -168,7 +168,7 @@
    1.13  
    1.14  lemma cpo_up: "chain (Y::nat \<Rightarrow> 'a u) \<Longrightarrow> \<exists>x. range Y <<| x"
    1.15  apply (frule up_chain_lemma, safe)
    1.16 -apply (rule_tac x="Iup (lub (range A))" in exI)
    1.17 +apply (rule_tac x="Iup (\<Squnion>i. A i)" in exI)
    1.18  apply (erule_tac j="j" in is_lub_range_shift [THEN iffD1, standard])
    1.19  apply (simp add: is_lub_Iup cpo_lubI)
    1.20  apply (rule exI, rule lub_const)