# 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 \<Longrightarrow> adm (\<lambda>x. t x \<noteq> \<bottom>)"
 by (simp add: adm_neq_compact)
 
+text {* Any upward-closed predicate is admissible. *}
+
+lemma adm_upward:
+  assumes P: "\<And>x y. \<lbrakk>P x; x \<sqsubseteq> y\<rbrakk> \<Longrightarrow> 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