# HG changeset patch # User huffman # Date 1199374177 -3600 # Node ID 8aea40e25aa88b1e1fec796973f9a8c6dd29b98d # Parent 331d8ce79ee2f2f126f83921df3cccd0e1f60769 new lemma adm_upward diff -r 331d8ce79ee2 -r 8aea40e25aa8 src/HOLCF/Adm.thy --- a/src/HOLCF/Adm.thy Thu Jan 03 10:27:40 2008 +0100 +++ b/src/HOLCF/Adm.thy Thu Jan 03 16:29:37 2008 +0100 @@ -188,6 +188,13 @@ lemma adm_not_UU: "cont t \ adm (\x. t x \ \)" by (simp add: adm_neq_compact) +text {* Any upward-closed predicate is admissible. *} + +lemma adm_upward: + assumes P: "\x y. \P x; x \ y\ \ P y" + shows "adm P" +by (rule admI, drule spec, erule P, erule is_ub_thelub) + lemmas adm_lemmas [simp] = adm_not_free adm_conj adm_all2 adm_ball2 adm_disj adm_imp adm_iff adm_less adm_eq adm_not_less