src/HOL/Library/Infinite_Set.thy
changeset 34112 ca842111d698
parent 30663 0b6aff7451b2
child 34113 dbc0fb6e7eae
     1.1 --- a/src/HOL/Library/Infinite_Set.thy	Thu Dec 17 07:02:13 2009 -0800
     1.2 +++ b/src/HOL/Library/Infinite_Set.thy	Thu Dec 17 09:33:30 2009 -0800
     1.3 @@ -371,21 +371,38 @@
     1.4    Inf_many  (binder "\<exists>\<^sub>\<infinity>" 10) and
     1.5    Alm_all  (binder "\<forall>\<^sub>\<infinity>" 10)
     1.6  
     1.7 -lemma INFM_EX:
     1.8 -  "(\<exists>\<^sub>\<infinity>x. P x) \<Longrightarrow> (\<exists>x. P x)"
     1.9 -  unfolding Inf_many_def
    1.10 -proof (rule ccontr)
    1.11 -  assume inf: "infinite {x. P x}"
    1.12 -  assume "\<not> ?thesis" then have "{x. P x} = {}" by simp
    1.13 -  then have "finite {x. P x}" by simp
    1.14 -  with inf show False by simp
    1.15 -qed
    1.16 +lemma INFM_iff_infinite: "(INFM x. P x) \<longleftrightarrow> infinite {x. P x}"
    1.17 +  unfolding Inf_many_def ..
    1.18 +
    1.19 +lemma MOST_iff_cofinite: "(MOST x. P x) \<longleftrightarrow> finite {x. \<not> P x}"
    1.20 +  unfolding Alm_all_def Inf_many_def by simp
    1.21 +
    1.22 +(* legacy name *)
    1.23 +lemmas MOST_iff_finiteNeg = MOST_iff_cofinite
    1.24 +
    1.25 +lemma not_INFM [simp]: "\<not> (INFM x. P x) \<longleftrightarrow> (MOST x. \<not> P x)"
    1.26 +  unfolding Alm_all_def not_not ..
    1.27  
    1.28 -lemma MOST_iff_finiteNeg: "(\<forall>\<^sub>\<infinity>x. P x) = finite {x. \<not> P x}"
    1.29 -  by (simp add: Alm_all_def Inf_many_def)
    1.30 +lemma not_MOST [simp]: "\<not> (MOST x. P x) \<longleftrightarrow> (INFM x. \<not> P x)"
    1.31 +  unfolding Alm_all_def not_not ..
    1.32 +
    1.33 +lemma INFM_const [simp]: "(INFM x::'a. P) \<longleftrightarrow> P \<and> infinite (UNIV::'a set)"
    1.34 +  unfolding Inf_many_def by simp
    1.35 +
    1.36 +lemma MOST_const [simp]: "(MOST x::'a. P) \<longleftrightarrow> P \<or> finite (UNIV::'a set)"
    1.37 +  unfolding Alm_all_def by simp
    1.38 +
    1.39 +lemma INFM_EX: "(\<exists>\<^sub>\<infinity>x. P x) \<Longrightarrow> (\<exists>x. P x)"
    1.40 +  by (erule contrapos_pp, simp)
    1.41  
    1.42  lemma ALL_MOST: "\<forall>x. P x \<Longrightarrow> \<forall>\<^sub>\<infinity>x. P x"
    1.43 -  by (simp add: MOST_iff_finiteNeg)
    1.44 +  by simp
    1.45 +
    1.46 +lemma INFM_E: assumes "INFM x. P x" obtains x where "P x"
    1.47 +  using INFM_EX [OF assms] by (rule exE)
    1.48 +
    1.49 +lemma MOST_I: assumes "\<And>x. P x" shows "MOST x. P x"
    1.50 +  using assms by simp
    1.51  
    1.52  lemma INFM_mono:
    1.53    assumes inf: "\<exists>\<^sub>\<infinity>x. P x" and q: "\<And>x. P x \<Longrightarrow> Q x"
    1.54 @@ -404,30 +421,88 @@
    1.55    "(\<exists>\<^sub>\<infinity>x. P x \<or> Q x) \<longleftrightarrow> (\<exists>\<^sub>\<infinity>x. P x) \<or> (\<exists>\<^sub>\<infinity>x. Q x)"
    1.56    unfolding Inf_many_def by (simp add: Collect_disj_eq)
    1.57  
    1.58 +lemma INFM_imp_distrib:
    1.59 +  "(INFM x. P x \<longrightarrow> Q x) \<longleftrightarrow> ((MOST x. P x) \<longrightarrow> (INFM x. Q x))"
    1.60 +  by (simp only: imp_conv_disj INFM_disj_distrib not_MOST)
    1.61 +
    1.62  lemma MOST_conj_distrib:
    1.63    "(\<forall>\<^sub>\<infinity>x. P x \<and> Q x) \<longleftrightarrow> (\<forall>\<^sub>\<infinity>x. P x) \<and> (\<forall>\<^sub>\<infinity>x. Q x)"
    1.64    unfolding Alm_all_def by (simp add: INFM_disj_distrib del: disj_not1)
    1.65  
    1.66 +lemma MOST_conjI:
    1.67 +  "MOST x. P x \<Longrightarrow> MOST x. Q x \<Longrightarrow> MOST x. P x \<and> Q x"
    1.68 +  by (simp add: MOST_conj_distrib)
    1.69 +
    1.70  lemma MOST_rev_mp:
    1.71    assumes "\<forall>\<^sub>\<infinity>x. P x" and "\<forall>\<^sub>\<infinity>x. P x \<longrightarrow> Q x"
    1.72    shows "\<forall>\<^sub>\<infinity>x. Q x"
    1.73  proof -
    1.74    have "\<forall>\<^sub>\<infinity>x. P x \<and> (P x \<longrightarrow> Q x)"
    1.75 -    using prems by (simp add: MOST_conj_distrib)
    1.76 +    using assms by (rule MOST_conjI)
    1.77    thus ?thesis by (rule MOST_mono) simp
    1.78  qed
    1.79  
    1.80 -lemma not_INFM [simp]: "\<not> (INFM x. P x) \<longleftrightarrow> (MOST x. \<not> P x)"
    1.81 -unfolding Alm_all_def not_not ..
    1.82 +lemma MOST_imp_iff:
    1.83 +  assumes "MOST x. P x"
    1.84 +  shows "(MOST x. P x \<longrightarrow> Q x) \<longleftrightarrow> (MOST x. Q x)"
    1.85 +proof
    1.86 +  assume "MOST x. P x \<longrightarrow> Q x"
    1.87 +  with assms show "MOST x. Q x" by (rule MOST_rev_mp)
    1.88 +next
    1.89 +  assume "MOST x. Q x"
    1.90 +  then show "MOST x. P x \<longrightarrow> Q x" by (rule MOST_mono) simp
    1.91 +qed
    1.92  
    1.93 -lemma not_MOST [simp]: "\<not> (MOST x. P x) \<longleftrightarrow> (INFM x. \<not> P x)"
    1.94 -unfolding Alm_all_def not_not ..
    1.95 +lemma INFM_MOST_simps [simp]:
    1.96 +  "\<And>P Q. (INFM x. P x \<and> Q) \<longleftrightarrow> (INFM x. P x) \<and> Q"
    1.97 +  "\<And>P Q. (INFM x. P \<and> Q x) \<longleftrightarrow> P \<and> (INFM x. Q x)"
    1.98 +  "\<And>P Q. (MOST x. P x \<or> Q) \<longleftrightarrow> (MOST x. P x) \<or> Q"
    1.99 +  "\<And>P Q. (MOST x. P \<or> Q x) \<longleftrightarrow> P \<or> (MOST x. Q x)"
   1.100 +  "\<And>P Q. (MOST x. P x \<longrightarrow> Q) \<longleftrightarrow> ((INFM x. P x) \<longrightarrow> Q)"
   1.101 +  "\<And>P Q. (MOST x. P \<longrightarrow> Q x) \<longleftrightarrow> (P \<longrightarrow> (MOST x. Q x))"
   1.102 +  unfolding Alm_all_def Inf_many_def
   1.103 +  by (simp_all add: Collect_conj_eq)
   1.104 +
   1.105 +text {* Properties of quantifiers with injective functions. *}
   1.106 +
   1.107 +lemma INFM_inj:
   1.108 +  "INFM x. P (f x) \<Longrightarrow> inj f \<Longrightarrow> INFM x. P x"
   1.109 +  unfolding INFM_iff_infinite
   1.110 +  by (clarify, drule (1) finite_vimageI, simp)
   1.111  
   1.112 -lemma INFM_const [simp]: "(INFM x::'a. P) \<longleftrightarrow> P \<and> infinite (UNIV::'a set)"
   1.113 -  unfolding Inf_many_def by simp
   1.114 +lemma MOST_inj:
   1.115 +  "MOST x. P x \<Longrightarrow> inj f \<Longrightarrow> MOST x. P (f x)"
   1.116 +  unfolding MOST_iff_cofinite
   1.117 +  by (drule (1) finite_vimageI, simp)
   1.118 +
   1.119 +text {* Properties of quantifiers with singletons. *}
   1.120 +
   1.121 +lemma not_INFM_eq [simp]:
   1.122 +  "\<not> (INFM x. x = a)"
   1.123 +  "\<not> (INFM x. a = x)"
   1.124 +  unfolding INFM_iff_infinite by simp_all
   1.125 +
   1.126 +lemma MOST_neq [simp]:
   1.127 +  "MOST x. x \<noteq> a"
   1.128 +  "MOST x. a \<noteq> x"
   1.129 +  unfolding MOST_iff_cofinite by simp_all
   1.130  
   1.131 -lemma MOST_const [simp]: "(MOST x::'a. P) \<longleftrightarrow> P \<or> finite (UNIV::'a set)"
   1.132 -  unfolding Alm_all_def by simp
   1.133 +lemma INFM_neq [simp]:
   1.134 +  "(INFM x::'a. x \<noteq> a) \<longleftrightarrow> infinite (UNIV::'a set)"
   1.135 +  "(INFM x::'a. a \<noteq> x) \<longleftrightarrow> infinite (UNIV::'a set)"
   1.136 +  unfolding INFM_iff_infinite by simp_all
   1.137 +
   1.138 +lemma MOST_eq [simp]:
   1.139 +  "(MOST x::'a. x = a) \<longleftrightarrow> finite (UNIV::'a set)"
   1.140 +  "(MOST x::'a. a = x) \<longleftrightarrow> finite (UNIV::'a set)"
   1.141 +  unfolding MOST_iff_cofinite by simp_all
   1.142 +
   1.143 +lemma MOST_eq_imp:
   1.144 +  "MOST x. x = a \<longrightarrow> P x"
   1.145 +  "MOST x. a = x \<longrightarrow> P x"
   1.146 +  unfolding MOST_iff_cofinite by simp_all
   1.147 +
   1.148 +text {* Properties of quantifiers over the naturals. *}
   1.149  
   1.150  lemma INFM_nat: "(\<exists>\<^sub>\<infinity>n. P (n::nat)) = (\<forall>m. \<exists>n. m<n \<and> P n)"
   1.151    by (simp add: Inf_many_def infinite_nat_iff_unbounded)