src/HOLCF/Pcpo.thy
 changeset 35492 5d200f2d7a4f parent 33523 96730ad673be child 39199 720112792ba0
equal 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>`