--- a/src/HOLCF/Product_Cpo.thy Wed Nov 17 08:47:58 2010 -0800
+++ b/src/HOLCF/Product_Cpo.thy Wed Nov 17 11:07:02 2010 -0800
@@ -276,6 +276,13 @@
shows "cont (\<lambda>x. case p of (a, b) \<Rightarrow> f x a b)"
using assms by (cases p) auto
+text {* Admissibility of predicates on product types. *}
+
+lemma adm_prod_case [simp]:
+ assumes "adm (\<lambda>x. P x (fst (f x)) (snd (f x)))"
+ shows "adm (\<lambda>x. case f x of (a, b) \<Rightarrow> P x a b)"
+unfolding prod_case_beta using assms .
+
subsection {* Compactness and chain-finiteness *}
lemma fst_below_iff: "fst (x::'a \<times> 'b) \<sqsubseteq> y \<longleftrightarrow> x \<sqsubseteq> (y, snd x)"