# HG changeset patch # User huffman # Date 1261071210 28800 # Node ID ca842111d69835c89a13d7e058182e740a8f744c # Parent 1b015caba46cf6a26a238681836be933e9119bd5 added lemmas about INFM/MOST diff -r 1b015caba46c -r ca842111d698 src/HOL/Library/Infinite_Set.thy --- a/src/HOL/Library/Infinite_Set.thy Thu Dec 17 07:02:13 2009 -0800 +++ b/src/HOL/Library/Infinite_Set.thy Thu Dec 17 09:33:30 2009 -0800 @@ -371,21 +371,38 @@ Inf_many (binder "\\<^sub>\" 10) and Alm_all (binder "\\<^sub>\" 10) -lemma INFM_EX: - "(\\<^sub>\x. P x) \ (\x. P x)" - unfolding Inf_many_def -proof (rule ccontr) - assume inf: "infinite {x. P x}" - assume "\ ?thesis" then have "{x. P x} = {}" by simp - then have "finite {x. P x}" by simp - with inf show False by simp -qed +lemma INFM_iff_infinite: "(INFM x. P x) \ infinite {x. P x}" + unfolding Inf_many_def .. + +lemma MOST_iff_cofinite: "(MOST x. P x) \ finite {x. \ P x}" + unfolding Alm_all_def Inf_many_def by simp + +(* legacy name *) +lemmas MOST_iff_finiteNeg = MOST_iff_cofinite + +lemma not_INFM [simp]: "\ (INFM x. P x) \ (MOST x. \ P x)" + unfolding Alm_all_def not_not .. -lemma MOST_iff_finiteNeg: "(\\<^sub>\x. P x) = finite {x. \ P x}" - by (simp add: Alm_all_def Inf_many_def) +lemma not_MOST [simp]: "\ (MOST x. P x) \ (INFM x. \ P x)" + unfolding Alm_all_def not_not .. + +lemma INFM_const [simp]: "(INFM x::'a. P) \ P \ infinite (UNIV::'a set)" + unfolding Inf_many_def by simp + +lemma MOST_const [simp]: "(MOST x::'a. P) \ P \ finite (UNIV::'a set)" + unfolding Alm_all_def by simp + +lemma INFM_EX: "(\\<^sub>\x. P x) \ (\x. P x)" + by (erule contrapos_pp, simp) lemma ALL_MOST: "\x. P x \ \\<^sub>\x. P x" - by (simp add: MOST_iff_finiteNeg) + by simp + +lemma INFM_E: assumes "INFM x. P x" obtains x where "P x" + using INFM_EX [OF assms] by (rule exE) + +lemma MOST_I: assumes "\x. P x" shows "MOST x. P x" + using assms by simp lemma INFM_mono: assumes inf: "\\<^sub>\x. P x" and q: "\x. P x \ Q x" @@ -404,30 +421,88 @@ "(\\<^sub>\x. P x \ Q x) \ (\\<^sub>\x. P x) \ (\\<^sub>\x. Q x)" unfolding Inf_many_def by (simp add: Collect_disj_eq) +lemma INFM_imp_distrib: + "(INFM x. P x \ Q x) \ ((MOST x. P x) \ (INFM x. Q x))" + by (simp only: imp_conv_disj INFM_disj_distrib not_MOST) + lemma MOST_conj_distrib: "(\\<^sub>\x. P x \ Q x) \ (\\<^sub>\x. P x) \ (\\<^sub>\x. Q x)" unfolding Alm_all_def by (simp add: INFM_disj_distrib del: disj_not1) +lemma MOST_conjI: + "MOST x. P x \ MOST x. Q x \ MOST x. P x \ Q x" + by (simp add: MOST_conj_distrib) + lemma MOST_rev_mp: assumes "\\<^sub>\x. P x" and "\\<^sub>\x. P x \ Q x" shows "\\<^sub>\x. Q x" proof - have "\\<^sub>\x. P x \ (P x \ Q x)" - using prems by (simp add: MOST_conj_distrib) + using assms by (rule MOST_conjI) thus ?thesis by (rule MOST_mono) simp qed -lemma not_INFM [simp]: "\ (INFM x. P x) \ (MOST x. \ P x)" -unfolding Alm_all_def not_not .. +lemma MOST_imp_iff: + assumes "MOST x. P x" + shows "(MOST x. P x \ Q x) \ (MOST x. Q x)" +proof + assume "MOST x. P x \ Q x" + with assms show "MOST x. Q x" by (rule MOST_rev_mp) +next + assume "MOST x. Q x" + then show "MOST x. P x \ Q x" by (rule MOST_mono) simp +qed -lemma not_MOST [simp]: "\ (MOST x. P x) \ (INFM x. \ P x)" -unfolding Alm_all_def not_not .. +lemma INFM_MOST_simps [simp]: + "\P Q. (INFM x. P x \ Q) \ (INFM x. P x) \ Q" + "\P Q. (INFM x. P \ Q x) \ P \ (INFM x. Q x)" + "\P Q. (MOST x. P x \ Q) \ (MOST x. P x) \ Q" + "\P Q. (MOST x. P \ Q x) \ P \ (MOST x. Q x)" + "\P Q. (MOST x. P x \ Q) \ ((INFM x. P x) \ Q)" + "\P Q. (MOST x. P \ Q x) \ (P \ (MOST x. Q x))" + unfolding Alm_all_def Inf_many_def + by (simp_all add: Collect_conj_eq) + +text {* Properties of quantifiers with injective functions. *} + +lemma INFM_inj: + "INFM x. P (f x) \ inj f \ INFM x. P x" + unfolding INFM_iff_infinite + by (clarify, drule (1) finite_vimageI, simp) -lemma INFM_const [simp]: "(INFM x::'a. P) \ P \ infinite (UNIV::'a set)" - unfolding Inf_many_def by simp +lemma MOST_inj: + "MOST x. P x \ inj f \ MOST x. P (f x)" + unfolding MOST_iff_cofinite + by (drule (1) finite_vimageI, simp) + +text {* Properties of quantifiers with singletons. *} + +lemma not_INFM_eq [simp]: + "\ (INFM x. x = a)" + "\ (INFM x. a = x)" + unfolding INFM_iff_infinite by simp_all + +lemma MOST_neq [simp]: + "MOST x. x \ a" + "MOST x. a \ x" + unfolding MOST_iff_cofinite by simp_all -lemma MOST_const [simp]: "(MOST x::'a. P) \ P \ finite (UNIV::'a set)" - unfolding Alm_all_def by simp +lemma INFM_neq [simp]: + "(INFM x::'a. x \ a) \ infinite (UNIV::'a set)" + "(INFM x::'a. a \ x) \ infinite (UNIV::'a set)" + unfolding INFM_iff_infinite by simp_all + +lemma MOST_eq [simp]: + "(MOST x::'a. x = a) \ finite (UNIV::'a set)" + "(MOST x::'a. a = x) \ finite (UNIV::'a set)" + unfolding MOST_iff_cofinite by simp_all + +lemma MOST_eq_imp: + "MOST x. x = a \ P x" + "MOST x. a = x \ P x" + unfolding MOST_iff_cofinite by simp_all + +text {* Properties of quantifiers over the naturals. *} lemma INFM_nat: "(\\<^sub>\n. P (n::nat)) = (\m. \n. m P n)" by (simp add: Inf_many_def infinite_nat_iff_unbounded)