# HG changeset patch
# User huffman
# Date 1261086576 28800
# Node ID dbc0fb6e7eae6d039f79aeee050aadb42fae7c5f
# Parent  ca842111d69835c89a13d7e058182e740a8f744c
add lemma INFM_conjI

diff -r ca842111d698 -r dbc0fb6e7eae src/HOL/Library/Infinite_Set.thy
--- a/src/HOL/Library/Infinite_Set.thy	Thu Dec 17 09:33:30 2009 -0800
+++ b/src/HOL/Library/Infinite_Set.thy	Thu Dec 17 13:49:36 2009 -0800
@@ -433,6 +433,13 @@
   "MOST x. P x \<Longrightarrow> MOST x. Q x \<Longrightarrow> MOST x. P x \<and> Q x"
   by (simp add: MOST_conj_distrib)
 
+lemma INFM_conjI:
+  "INFM x. P x \<Longrightarrow> MOST x. Q x \<Longrightarrow> INFM x. P x \<and> Q x"
+  unfolding MOST_iff_cofinite INFM_iff_infinite
+  apply (drule (1) Diff_infinite_finite)
+  apply (simp add: Collect_conj_eq Collect_neg_eq)
+  done
+
 lemma MOST_rev_mp:
   assumes "\<forall>\<^sub>\<infinity>x. P x" and "\<forall>\<^sub>\<infinity>x. P x \<longrightarrow> Q x"
   shows "\<forall>\<^sub>\<infinity>x. Q x"