src/HOL/Library/Infinite_Set.thy
changeset 27407 68e111812b83
parent 27368 9f90ac19e32b
child 27487 c8a6ce181805
     1.1 --- a/src/HOL/Library/Infinite_Set.thy	Tue Jul 01 01:09:03 2008 +0200
     1.2 +++ b/src/HOL/Library/Infinite_Set.thy	Tue Jul 01 01:19:08 2008 +0200
     1.3 @@ -1,4 +1,4 @@
     1.4 -(*  Title:      HOL/Infnite_Set.thy
     1.5 +(*  Title:      HOL/Library/Infinite_Set.thy
     1.6      ID:         $Id$
     1.7      Author:     Stephan Merz
     1.8  *)
     1.9 @@ -209,10 +209,9 @@
    1.10  lemma range_inj_infinite:
    1.11    "inj (f::nat \<Rightarrow> 'a) \<Longrightarrow> infinite (range f)"
    1.12  proof
    1.13 -  assume "inj f"
    1.14 -    and  "finite (range f)"
    1.15 +  assume "finite (range f)" and "inj f"
    1.16    then have "finite (UNIV::nat set)"
    1.17 -    by (auto intro: finite_imageD simp del: nat_infinite)
    1.18 +    by (rule finite_imageD)
    1.19    then show False by simp
    1.20  qed
    1.21  
    1.22 @@ -374,7 +373,7 @@
    1.23    Inf_many  (binder "\<exists>\<^sub>\<infinity>" 10) and
    1.24    Alm_all  (binder "\<forall>\<^sub>\<infinity>" 10)
    1.25  
    1.26 -lemma INF_EX:
    1.27 +lemma INFM_EX:
    1.28    "(\<exists>\<^sub>\<infinity>x. P x) \<Longrightarrow> (\<exists>x. P x)"
    1.29    unfolding Inf_many_def
    1.30  proof (rule ccontr)
    1.31 @@ -390,7 +389,7 @@
    1.32  lemma ALL_MOST: "\<forall>x. P x \<Longrightarrow> \<forall>\<^sub>\<infinity>x. P x"
    1.33    by (simp add: MOST_iff_finiteNeg)
    1.34  
    1.35 -lemma INF_mono:
    1.36 +lemma INFM_mono:
    1.37    assumes inf: "\<exists>\<^sub>\<infinity>x. P x" and q: "\<And>x. P x \<Longrightarrow> Q x"
    1.38    shows "\<exists>\<^sub>\<infinity>x. Q x"
    1.39  proof -
    1.40 @@ -401,19 +400,48 @@
    1.41  qed
    1.42  
    1.43  lemma MOST_mono: "\<forall>\<^sub>\<infinity>x. P x \<Longrightarrow> (\<And>x. P x \<Longrightarrow> Q x) \<Longrightarrow> \<forall>\<^sub>\<infinity>x. Q x"
    1.44 -  unfolding Alm_all_def by (blast intro: INF_mono)
    1.45 +  unfolding Alm_all_def by (blast intro: INFM_mono)
    1.46 +
    1.47 +lemma INFM_disj_distrib:
    1.48 +  "(\<exists>\<^sub>\<infinity>x. P x \<or> Q x) \<longleftrightarrow> (\<exists>\<^sub>\<infinity>x. P x) \<or> (\<exists>\<^sub>\<infinity>x. Q x)"
    1.49 +  unfolding Inf_many_def by (simp add: Collect_disj_eq)
    1.50 +
    1.51 +lemma MOST_conj_distrib:
    1.52 +  "(\<forall>\<^sub>\<infinity>x. P x \<and> Q x) \<longleftrightarrow> (\<forall>\<^sub>\<infinity>x. P x) \<and> (\<forall>\<^sub>\<infinity>x. Q x)"
    1.53 +  unfolding Alm_all_def by (simp add: INFM_disj_distrib del: disj_not1)
    1.54  
    1.55 -lemma INF_nat: "(\<exists>\<^sub>\<infinity>n. P (n::nat)) = (\<forall>m. \<exists>n. m<n \<and> P n)"
    1.56 +lemma MOST_rev_mp:
    1.57 +  assumes "\<forall>\<^sub>\<infinity>x. P x" and "\<forall>\<^sub>\<infinity>x. P x \<longrightarrow> Q x"
    1.58 +  shows "\<forall>\<^sub>\<infinity>x. Q x"
    1.59 +proof -
    1.60 +  have "\<forall>\<^sub>\<infinity>x. P x \<and> (P x \<longrightarrow> Q x)"
    1.61 +    using prems by (simp add: MOST_conj_distrib)
    1.62 +  thus ?thesis by (rule MOST_mono) simp
    1.63 +qed
    1.64 +
    1.65 +lemma not_INFM [simp]: "\<not> (INFM x. P x) \<longleftrightarrow> (MOST x. \<not> P x)"
    1.66 +unfolding Alm_all_def not_not ..
    1.67 +
    1.68 +lemma not_MOST [simp]: "\<not> (MOST x. P x) \<longleftrightarrow> (INFM x. \<not> P x)"
    1.69 +unfolding Alm_all_def not_not ..
    1.70 +
    1.71 +lemma INFM_const [simp]: "(INFM x::'a. P) \<longleftrightarrow> P \<and> infinite (UNIV::'a set)"
    1.72 +  unfolding Inf_many_def by simp
    1.73 +
    1.74 +lemma MOST_const [simp]: "(MOST x::'a. P) \<longleftrightarrow> P \<or> finite (UNIV::'a set)"
    1.75 +  unfolding Alm_all_def by simp
    1.76 +
    1.77 +lemma INFM_nat: "(\<exists>\<^sub>\<infinity>n. P (n::nat)) = (\<forall>m. \<exists>n. m<n \<and> P n)"
    1.78    by (simp add: Inf_many_def infinite_nat_iff_unbounded)
    1.79  
    1.80 -lemma INF_nat_le: "(\<exists>\<^sub>\<infinity>n. P (n::nat)) = (\<forall>m. \<exists>n. m\<le>n \<and> P n)"
    1.81 +lemma INFM_nat_le: "(\<exists>\<^sub>\<infinity>n. P (n::nat)) = (\<forall>m. \<exists>n. m\<le>n \<and> P n)"
    1.82    by (simp add: Inf_many_def infinite_nat_iff_unbounded_le)
    1.83  
    1.84  lemma MOST_nat: "(\<forall>\<^sub>\<infinity>n. P (n::nat)) = (\<exists>m. \<forall>n. m<n \<longrightarrow> P n)"
    1.85 -  by (simp add: Alm_all_def INF_nat)
    1.86 +  by (simp add: Alm_all_def INFM_nat)
    1.87  
    1.88  lemma MOST_nat_le: "(\<forall>\<^sub>\<infinity>n. P (n::nat)) = (\<exists>m. \<forall>n. m\<le>n \<longrightarrow> P n)"
    1.89 -  by (simp add: Alm_all_def INF_nat_le)
    1.90 +  by (simp add: Alm_all_def INFM_nat_le)
    1.91  
    1.92  
    1.93  subsection "Enumeration of an Infinite Set"