# HG changeset patch # User huffman # Date 1286200717 25200 # Node ID 0b8e19f588a472701183a1322b95286ecb55874a # Parent d841744718fec1775f7f582a9077a3376ebfb0e0 new lemmas about lub diff -r d841744718fe -r 0b8e19f588a4 src/HOLCF/Adm.thy --- a/src/HOLCF/Adm.thy Mon Oct 04 06:45:57 2010 -0700 +++ b/src/HOLCF/Adm.thy Mon Oct 04 06:58:37 2010 -0700 @@ -171,6 +171,10 @@ "\compact x; chain Y; x \ (\i. Y i)\ \ \i. x \ Y i" unfolding compact_def adm_def by fast +lemma compact_below_lub_iff: + "\compact x; chain Y\ \ x \ (\i. Y i) \ (\i. x \ Y i)" +by (fast intro: compactD2 elim: below_trans is_ub_thelub) + lemma compact_chfin [simp]: "compact (x::'a::chfin)" by (rule compactI [OF adm_chfin]) diff -r d841744718fe -r 0b8e19f588a4 src/HOLCF/Pcpo.thy --- a/src/HOLCF/Pcpo.thy Mon Oct 04 06:45:57 2010 -0700 +++ b/src/HOLCF/Pcpo.thy Mon Oct 04 06:58:37 2010 -0700 @@ -33,6 +33,9 @@ "\chain S; range S <| x\ \ (\i. S i) \ x" by (blast dest: cpo intro: lubI [THEN is_lub_lub]) +lemma lub_below_iff: "chain S \ (\i. S i) \ x \ (\i. S i \ x)" + by (simp add: is_lub_below_iff [OF cpo_lubI] is_ub_def) + lemma lub_range_mono: "\range X \ range Y; chain Y; chain X\ \ (\i. X i) \ (\i. Y i)" diff -r d841744718fe -r 0b8e19f588a4 src/HOLCF/Porder.thy --- a/src/HOLCF/Porder.thy Mon Oct 04 06:45:57 2010 -0700 +++ b/src/HOLCF/Porder.thy Mon Oct 04 06:58:37 2010 -0700 @@ -139,6 +139,9 @@ lemma is_lubI: "\S <| x; \u. S <| u \ x \ u\ \ S <<| x" unfolding is_lub_def by fast +lemma is_lub_below_iff: "S <<| x \ x \ u \ S <| u" + unfolding is_lub_def is_ub_def by (metis below_trans) + text {* lubs are unique *} lemma unique_lub: "\S <<| x; S <<| y\ \ x = y"