src/HOLCF/Pcpo.thy
changeset 35492 5d200f2d7a4f
parent 33523 96730ad673be
child 39199 720112792ba0
equal deleted inserted replaced
35491:92e0028a46f2 35492:5d200f2d7a4f
    88 
    88 
    89 lemma lub_equal:
    89 lemma lub_equal:
    90   "\<lbrakk>chain X; chain Y; \<forall>k. X k = Y k\<rbrakk>
    90   "\<lbrakk>chain X; chain Y; \<forall>k. X k = Y k\<rbrakk>
    91     \<Longrightarrow> (\<Squnion>i. X i) = (\<Squnion>i. Y i)"
    91     \<Longrightarrow> (\<Squnion>i. X i) = (\<Squnion>i. Y i)"
    92   by (simp only: expand_fun_eq [symmetric])
    92   by (simp only: expand_fun_eq [symmetric])
       
    93 
       
    94 lemma lub_eq:
       
    95   "(\<And>i. X i = Y i) \<Longrightarrow> (\<Squnion>i. X i) = (\<Squnion>i. Y i)"
       
    96   by simp
    93 
    97 
    94 text {* more results about mono and = of lubs of chains *}
    98 text {* more results about mono and = of lubs of chains *}
    95 
    99 
    96 lemma lub_mono2:
   100 lemma lub_mono2:
    97   "\<lbrakk>\<exists>j. \<forall>i>j. X i = Y i; chain X; chain Y\<rbrakk>
   101   "\<lbrakk>\<exists>j. \<forall>i>j. X i = Y i; chain X; chain Y\<rbrakk>