# HG changeset patch
# User huffman
# Date 1201811840 -3600
# Node ID f9647c040b58102329d57c1790d3dc66c095a424
# Parent  ca6876116bb432345b4a01dbe0cfb97b5e80d6bf
add lemma cpo_lubI

diff -r ca6876116bb4 -r f9647c040b58 src/HOLCF/Pcpo.thy
--- a/src/HOLCF/Pcpo.thy	Thu Jan 31 21:23:14 2008 +0100
+++ b/src/HOLCF/Pcpo.thy	Thu Jan 31 21:37:20 2008 +0100
@@ -19,6 +19,9 @@
 
 text {* in cpo's everthing equal to THE lub has lub properties for every chain *}
 
+lemma cpo_lubI: "chain (S::nat \<Rightarrow> 'a::cpo) \<Longrightarrow> range S <<| lub (range S)"
+by (fast dest: cpo elim: lubI)
+
 lemma thelubE: "\<lbrakk>chain S; (\<Squnion>i. S i) = (l::'a::cpo)\<rbrakk> \<Longrightarrow> range S <<| l"
 by (blast dest: cpo intro: lubI)